## 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