Improving the Efficiency of Higher Order Unification

Abstract

The sources of inefficiency in currently existing higher order unification algorithms are investigated. Aside from such theoretical difficulties as the undecidability of unification in third order logic, and the existence of infinite unifiers and the lack of a polynomial bound on the number of applicationsof the "imitation" rule even in the monadic subcase of second order unification, the current algorithms suffer from a built-in inefficiency due to their introduction and subsequent elimination of many auxiliary functional variables, and to the nondirected nature of the substitutions made by the "projection" rule. It is argued that a procedure based on attempting to match the argument or arguments of a functional or predicate variable with the subterms of the other formula in the unification can decide the possibility of unification and generate the resulting unifiers much more directly than the theoretically complete algorithm.