Improving the Efficiency of Higher Order Unification

IMPROVING THE EFFICIENCY OF HIGHER ORDER UNIFICATION

Jared L. Darlington Institut fUr Informatik University of Bonn, Germany

functional variables, and (b) because of the nondirected nature of the substitu­ tions made by the projection rule. The new function svrnbols referred to in· (a) appear to play - an essential role in the unification of certain pairs of formulae -- for example, where the head of one for­ mula is a higher order variable 'f' which occurs also within the other formula but not within an argument of another vari­ able 'g' -- but there are many cases in which thev merelv delay the unification process · · For example, suppose one is

unifying

in second order logic, where

f is a va.riable, A and K are constants, and n is any positive integer. The usual unification procedure based on imitation and projection (see for example Huet 1975, Winterstein 1976, and Jensen and Pietrzy­ kowski 1976, the last of whom also use other rules) introduces and eliminates for this example n new functional variables of type (i-ti), and after n+1 imitations and an equal number of projections generates

the two unifiers

In general, if one is unifying e 1 and e 2 in second order logic, where

type(e ) = type(e ) , and f is a functional or predicate vari~ble with

(o = "truth value"), the

Imitation rule

yields for f

Abstract

The sources of inefficiency in cur­ rently existing higher order unification algorithms are investigated. Aside from such theoretical difficulties as the un­ decidability of unification in third order logic, and the existence of infinite uni­ fiers and the lack of a polynomial bound on the number of applicationsof the "imi­ tation" rule even in the monadic subcase of second order unification, the current algorithms suffer from a built-in ineffi­ ciency due to their introduction and sub­ sequent elimination of many auxiliary functional variables, and to the nondirec­ ted 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.

Descriptive Terms

Higher order logic, resolution, theorem proving, unification

The recent interest in developing linear and near-linear unification algo­ rithms for first order languages (see for example Huet 1976, Paterson and Wegman 1976, and work referred to by them) has, with few exceptions, not been matched by a corresponding effort to improve the efficiency of higher order unification. A linear unification algorithm is of course out of the question for higher or­ der logic in general, for not only is unification known to be undecidable in third order logic (Huet 1973; Lucchesi 1972), but even in the monadic subcase of second order logic it has been shown (by Winterstein 1976) that there exists no polynomial upper bound on the number of applications of the "imitation" rule which together with the "projection" rule plays an essential role in a complete higher order unification algorithm. Although linear bounds on the number of their ap­ plications do exist in some cases (Win­ terstein 1976), the two above-mentioned rules are inherently inefficient, (a) be­ cause of their introduction and subse­ quent elimination of many auxiliary

<f, "f\u 1 P(q 1 (u 1 , · · · I where the q, are new variables with J

resulting in the "successor node"

while the

Projection rule

generates rn substitutions for f

(f, ·.. urn. with type(uk) = i,

resulting in rn successor nodes

If n=3 in Example 1, imitation-cum-pro­ jection qenerates the tree shown in Figure 1 below. It is clear that each increase of 1 in n, the number of K's, adds one new function svrnbol q. and there­ fore one imitation and one nro~ection, without addinq anv unifiers. One reason for this waste of effort is that imita­ tion-curn-nrojection as it is ordinarily used does not take account of the fact that nrojecting f onto one of its arqu­ ments ak, in the unification of e 1 and e 2 in second order lo~ic, succeeds it and onlv if the resulting successor node f(ak, e 2 )J is unifiable. Imitation-curn­ proJeCt1on, however, first makes the Pro­ jection substitutions for f and then com­ nares the results with e 2 . In comparison with imitation, projection is in this re­ spect less like unification, which should ideallv make onlv substitutions that are in some wav directed bv the other formula in the unification, and more like some of the pre-resolution first order Herbrand proof ' nrocedures that, instead of unifi­ cation, emploved substitution for vari­ ables followed by comoarison of the resulting formulae.

Fig. 1. Unification tree for Example 1 (n=3) given bv imitation-cum-projection.

To see how unification mav be per­ formed more efficientlv in examples like the preceding, let us consider the unifi­ cation of

where the tvpes are as before, and where f is "monadic" and does not occur in e 2 · For every subformula t of e , the unifi­ cation tree includes some n~de containing the pair

where g. is either f (if t is e 2 ) or is a variablJ introduced into the tree by imi­ tation (see for example Figure 1). Applv­ ing imitation to every g. produces the unifier · . J

as in unifier (i) of Example 1 , but apply­ ing projection to a g. leads to a success­ ful unification if and onlv if

leads to a successful unification. This suggests that one may "screen out" in ad­ vance projections that are bound to fail, by first checking the unifiability of a 1 with the various subterms t in e 2 . In Example 1, there is clearlv just one pro­ jection that can succfied, since there is just one subterm of K A, namely 'A', that the argument 'A' of f matches, leading to the unifier (ii). Here, the match of A with A is trivial, but in other cases a fair amount of work may be reauired com­ pletely to unify an argument a of f with a subterm t of e 2 , especially lf either or both contain functional variables. It is therefore more efficient to set up a "search pattern" corresponding to a 1 , but based on less than complete unification, that will "match" just- those subterms of e 2 that are potentially unifiable with a 1 wnile ignoring the obviously impossible cases , such as those in which a and t begin with opposing constants. ~pecifi­ cally:

• P1: If a 1 is flexible (i.e. has a vari­ able head) , then

PATTERN any term of type i.

P2: If not, then

PATTERN any flexible term or any term with the same head as a~

A program based on this idea and coded in SNOBOL4 is being experimented with on the IBM 360/50 at the GMD/Bonn. Earlier pro­ grams performed the pattern matching by means of complete unification of a 1 with each subterm t of e , a technique that was called "f-matchfnq", and tli.e ·current method is a refinement of this techniaue. Moreover, it can be incorporated into any program that uses imitation and projec­ tion. In cases where it is applicable, it has the advantages of introducing no new functional variables and of screening out a priori impossible projections in advance.

To explain the method in greater detail, we start with a node

of a unification tree, containing one or more unification pairs <A ,B ) where each Ai is of the same tvp~ a~ B . Imi­ tation-cuM-projection generates ~uccessor nodes toN. bv choosing a pair <A.,B .) from N according to some criteriorl arld applying imitation and projection to A. and B. in all possible·wavs. The uniff­ catiorl substitutions resulting from each application are then applied to all the pairs inN, thereby generating a succes­ sor node after all possible "lambda nor­ malisations" and simplifications have been made. If no unification substitu­ tions are apPlicable to any pair inN, it is labelled either 'S' for "success" or 'F' for "failure", as the case mav be. If the pair singled out from N is

the simnlified Procedure first checks whether the pair P bears a subscriPt u .. If so, it Procee~s directlv to the genJr­ ation of nodes N 1 , described below, hut if not it adds a subscript u. toP, where u . is a variable not occurrirlg inN or its ntedecessors, and will serve as the vari­ able to be used in subseauent lambda ab­ stractions. It then generates a successor node N 0 from P, based on the substitution

that results from imitation alone (in Ex­ ample 1, this is unifier (i)). For each subterm t of e 2 that PAtTERN matches, it next generates a node N 1 that results from replacing P in N by < a 1 , t > , and a unification substitution

where e~ results from replacing the matched term t by u .. In Example 1, there is just one su~term t that PATTERN matches, namely 'A', producing the successor node f< A, A)J and the cor­ resnonding unification substitution (ii).

At the time of generating each N~, the proce~ure examines the lambda txoression for f to see whether a node N 2 can be generlted, as follows: if there is some subterm appearing befote the first lambda­ bound vatiable u. in e 2 (this cannot hap­ pen ifte2 is monadic) , then a successor node N 2 Is generated bv renlacing P in N bv

J t otherwise. The nodes N~ correspond to anplving more than one orojection in the unification of P, in case a 1 is simultan­ eously unifiable with two or more subterms of e 2 and mav therefore be reolaced bv the same u. in the lambda expression. Thetre­ strictfon on the generation of nodes N 2 (don't scan past au.) is necessary to prevent multiple derivations of the same unifier. Without it, for example, the unifier

would be generated many times over.

The procedure for aeneratinq suc­ cessor nodes just described mav be com­ pared with imitation-cum-orojection in the unification of

It may be seen from Figures 2 and 3 that both nrocedures generate the same six unifiers for Example 2, namely

but the simplified procedure gets them considerable more directlv, generating a tree of depth two instead of deeth five.

(The apparent eaualitv in size of the dia­ grams in Figures 2 and 3 is due to the fact that, in order to save soace, the unification substitutions have been omit­ ted from Figure 2.) After generating the first success node, N , in Figure 3 above, the simplified procedHre then searches in 'P(KA,B)' for possible matches for 'qA'; since qA is a flexible term, the search pattern will match anv term of tvpe i, namely 'KA', 'A' or 'B', generating the three N 1 -nodes l<gA, KA)L ~<gA, A)l and {<gA, B)l , with their corresponding sub­ stitutions for f. Since one of these f's, namely

has a term 'KA' appearing before u 1 , a node N 2 is generated in an attempt to get a value for f containing two or more oc­ currences of u 1 , namely

but this is not oossihle since 'B' will not match any part of 'KA'; in other words, 'gA' will not simultaneously match 'B' and some part of 'KA'. The three N 1 -nodes are then nrocessed in the same way as the root node, resulting in five success nodes. The procedure mav also be apnlied to cases where f is nonmonadic, namely

Here, however, it is necessarv to annlv the oroct:dure m times , searchincr separate­ ly in e 2 for a match for each argument ai. It is fair to sav that, as the deqree of f increases, the advantages of our proce­ dure vis-a-vis irnitation~cum-nrojection hecome nrogressivelv less. Furthermore, it will not handle all cases in which the same functional or nredicate variable oc­ curs in both terms to be unified , such as

in second order logic, which generates in­ finite unifiers, but even here our nroce­ dure generates two unifiers, namelv

This type of case, however, does not arise in the annlications of second (and higher) order theorem nrovin0 that we have been making, such as to automatic orogram svn­ thesis (Darlinaton 1976) and to nroofs of theorems in to~ology. The simplified oro­ cedure has in fact been extended to per­ form certain unifications in third and higher order logic, though we do not at nresent have a general characterisation of the limits of its annlicabilitv beyond second order logic. Within second order logic itself, it appears to be eauivalent to imitation-cum-projection for unifica­ tions whose trees contain no pairs of the sort found in Example 3, where the same higher order variable occurs in both e 1 and e . The argument in outline is that each ~uccessful path containing n projec­ tions (n ~ O) in an imitation-cum-projec­ tion tree corresponds uniquely to a suc­ cessful path containing n N 1 - and N 2 -nodes in the simplified tree.

A practical result of the simplified procedure is, in its application to "con­ strained resolution" (Huet 1973a) , to de­ cide more quickly that only one unifier is possible in a given case, and therefore to reduce the number of constraints that need be generated. For example, if a par­ ticular resolvent is based on the unifica­ tion of 'fA' with a complex e , con­ strained resolution would nor~ally decide that there exists no "most general uni­ fier" in this case and therefore generate only a skeletal resolvent with ~fA,e 2 1 attached to it as a "constraint" to be unified later. If, however, e 2 con­ tains ·nothing that 'A' will match, then there is only one possible unifier, namely (f, ~u.e ) , and no constraint need be generate~. Alternatively, if 'A' matches only one term t of e , then (f, )u.e ) may be taken as "the;l unifier, leavi~g out (f, ~u.e ) , since unifiers of this sort, based 6n imitation alone, seldom if ever lead to "useful" inferences -- for example, imitation alone will not permit the derivation by resolution of P(B) from P(A), A = B, and x 1 y V ~f(A) V f(B), which requires the unifier <f, Au.Pu). Similar heuristics are employed by BUlow (1976), who does a certain amount of "look-ahead" during higher order resolu­ tion in order to rule out branches result­ ing from nonproductive or impossible imi­ tations or projections, thereby reducing the number of constraints. Another proce­ dure related to ours is Bledsoe's (1977) method for finding values of set vari­ ables, equivalently monadic predicate variables, in topology, program verifica­ tion and other theorem proving domains, where the full power of imitation-cum­ projection is not required. In view of the theoretical difficulties in achieving significant improvements in higher order inference in general, research of this sort into improving its efficiency in im­ portant special cases is particularly vital if the inclusion of higher order features in automatic theorem provers, be they based on resolution or natural deduction, is to become a practical proposition.