HIGHER-ORDER UNIFICATION VIA COMBINATORS

We present an algorithm for unification in the simply typed lambda cal culus which enumerates complete sets of unifiers using a finitely bran ching search space. In fact, the types of terms may contain type varia bles, so that a solution may involve type-substitution as well as term substitution. The problem is first translated into the problem of uni fication with respect to exstensional equality in combinatory logic, a nd the algorithm is defined in terms of transformations on systems of combinatory terms. These transformations are based on a new method (it self based on systems) for deciding extensional equality between typed combinatory logic terms.