Abstract: We present a unification algorithm for the lambda-Pi-calculus, the lambda calculus with first-order dependent function types. Our algorithm is an extension of Huet's algorithm for the simply-typed lambda calculus to first-order dependent function types.
In the simply-typed lambda calculus one attempts to unify a pair of terms of the same type: in the lambda-Pi-calculus types are dependent on terms so one must unify not only terms, but their types as well. Accordingly, we identify a suitable notion of similarity of types, and only attempt to unify a pair of terms of similar type: if the types are not similar then they are not unifiable. Since Huet's algorithm does not enumerate all of the unifiers of a given pair of terms, the strategy of first unifying pairs of types - by identifying suitable pairs of subterms for unification - is not complete. Accordingly, we must unify terms and their types simultaneously, taking care to maintain all of the conditions that are necessary to ensure the well-formedness of the resulting calculated substitution.
Our notion of substitution is an algebraic one: substitutions are morphisms of lambda-Pi-contexts. However, in order to define our algorithm we must work with psubstitutions and pcontexts - substitutions and contexts, respectively, in which variables are replaced by terms of similar, not B(n)-equal type.Previous | Index | Next