Unification of Simply Typed Lambda-Terms as Logic Programming

Dale Miller

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_lambda in a natural and clear fashion. In a sense, the translation only involves explicitly axiomatizing in L_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_{lambda} searching for proofs using those axioms.

LFCS report ECS-LFCS-91-160

This report was published in the proceedings of the Eighth International Logic Programming Conference, edited by Koichi Furukawa, Paris, France. MIT Press, June 1991, pp. 255 -- 269.

Previous | Index | Next