## A Unification Algorithm for the lambda-Pi-Calculus

**David Pym**
*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.

*LFCS report ECS-LFCS-92-229*

Previous |

Index |

Next