A complete transformation system for polymorphic higher-order unification

Polymorphic higher-order unification is a method for unifying terms in the poly\-mor\-phi\-cally typed $\lambda$-calculus, that is, given a set of pairs of terms $S_0 = \{s_1 = t_2,\ldots,s_n = t_n\}$, called a unification problem, finding a substitution $\sigma$ such that $\sigma(s_i)$ and $\sigma(t_i)$ are equivalent under the conversion rules of the calculus for all $i$, $1\leq i\leq n$. I present the method as a transformation system, i.e.\ as a set of schematic rules $U \Rightarrow U'$ such that any unification problem $\delta({U})$ can be transformed into $\delta({U'})$ where $\delta$ is an instantiation of the meta-level variables in $U$ and $U'$. By successive use of transformation rules one possibly obtains a solved unification problem with obvious unifier. I show that the transformation system is correct and complete, i.e.\if $\delta({U}) \Rightarrow \delta({U'})$ is an instance of a transformation rule, then the set of all unifiers of $\delta({U'})$ is a subset of the set of all unifiers of $\delta({U})$ and if $\cal U$ is the set of all unification problems that can be obtained from successive applications of transformation rules from an unification problem $U$, then the union of the set of all unifiers of all unification problems in $\cal U$ is the set of all unifiers of $U$. The transformation rules presented here are essentially different from those in Gallier and Snyder (1989) or Nipkow (1990). The correctness and completeness proofs are in lines with those of Gallier and Snyder (1989)