MPII91228
A complete transformation system for polymorphic higherorder unification
Hustadt, Ullrich
December 1991, 22 pages.
.
Status: available  back from printing
Polymorphic higherorder 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 metalevel 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).

91228.pdf
 Attachement: MPII91228.dvi (120 KBytes); 91228.pdf (222 KBytes)
URL to this document: https://domino.mpiinf.mpg.de/internet/reports.nsf/NumberView/1991228
BibTeX
@TECHREPORT{Hustadt91,
AUTHOR = {Hustadt, Ullrich},
TITLE = {A complete transformation system for polymorphic higherorder unification},
TYPE = {Research Report},
INSTITUTION = {MaxPlanckInstitut f{\"u}r Informatik},
ADDRESS = {Im Stadtwald, D66123 Saarbr{\"u}cken, Germany},
NUMBER = {MPII91228},
MONTH = {December},
YEAR = {1991},
ISSN = {0946011X},
}