Unification with extended patterns

An extension of Miller's algorithm for β₀-unification of typed λ-terms is presented. The extension considered is the addition of products and polymorphism to β₀-unification; the new unification problem is termed β₀π-unification. Miller's pattern restriction is generalized by allowing repeated occurrences of variables to appear as arguments to free function variables, provided such variables are prefixed by distinct sequences of projections. This extended pattern restriction has several applications, including the definition of higher-order explicit substitutions. The algorithm is verified to terminate, and is shown to be sound and complete.