Abstract

"The unification of simply typed [lambda]-terms modulo the rules of [beta]- and [eta]-conversions is often called 'higher-order' unification because of the possible presence of variables of functional type. This kind of unification is undecidable in general and if unifiers exist, most general unifiers may not exist. In this paper, we show that such unification problems can be coded as a query of the logic programming language L[subscript lambda] in a natural and clear fashion. In a sense, the translation only involves explicitly axiomatizing in L[subscript lambda] the notions of equality and substitution of the simply typed [lambda]-calculus: the rest of the unification process can be viewed as simply an interpreter of L[subscript lambda] searching for proofs using those axioms."