Higher-Order Unification with Dependent Function Types

Roughly fifteen years ago, Huet developed a complete semidecision algorithm for unification in the simply typed lambda-calculus (lambda). In spite of the undecidability of this problem, his algorithm is quite usable in practice. Since then, many imortant applications have come about in such areas as theorem proving, type inference, program transformation, and machine learning. Another development is the discovery that by enriching lambda to include dependent function types, the resulting calculus (lambda pi) forms the basis of a very elegant and expressive Logical Framework, encompassing the syntax, rules, and proofs for a wide class of logics. This paper presents an algorithm in the spirit of Huet’s, for unification in lambda pi. This algorithm gives us the best of both worlds: the automation previously possible in lambda. And the greatly enriched expressive power of lambda pi. It can used to considerable advantage in many of the current applications of Huet’s algorithm, and has important new applications as well. These include automated and semi-automated theorem proving in encoded logics, and automatic type inference in a variety of encoded languages.