A Complete Unification Algorithm for Associative-Commutative Functions

A COMPLETE UNIFICATION ALGORITHM FOR

ASSOCIATIVE ·COMMUTATIVE FUNcTIONS*

Mark E. Stickel Department of Computer Science Carnegie-Mellon University Pittsburgh, Pennsylvania

An important component of mechanical theorem provinc systems are unification algorithms which find most general sul!stitutions which, when applied to two expresssions, make them equivalent. Functions which are associative and commutative (such as the arithmetic addition and multiplication functions) are often the subject of mechanical theorem proving. An algorithm which unifies terms whose function is associative and commutative is presented here. The algorithm eliminates the need for axiomatizing the usoeiativity and commutativity properties and returns 1 complete set of unifiers without recourse to the · indefinite generation of variants and instances of the terms beinc unified required by previous solutions to the problem.

lntrodudjop

At the core of many theorem provinc systems is a

unification algorithm which returns for 1 pair of input expressions a set of unifyinc substitutions, assignments to the variables of the expressions which make the two expressions equivalent. Typical is the unifiution alcorilhm of Robinson [6] for unifying atomic formulas of the first order predicate calculus in resolution theorem provinc [I].

This work treats the case of unifying terms of the first order predicate calculus where the function is associative and commutative. Such functions are mathematically important and thus of interest to developers of theorem proving programs. Examples of such functions are the arithmetic: eddition and multiplication functions.

The case where the function is simply commutative is easily handled by a trivial extension to Robinson's unifiution algorithm which unifies the arguments of one term ·cains! permutations of the arguments of the other term.

The case where the function is simply associative is quite difficult and we know of no general · solution. Suggestive of the difficulty of this problem is the fact that there may be an infinite number of unifiers for a pair of terms. For example, the terms f(u) and f(ax) where I is associative, a is a constant, and x is 1 variable has unifiers with x·a, X"f(aa), x·f(aaa), 00 00 (We represent the argument lists of associative functions with no extra parentheses, i.e., f(ibc) rather than f(af(be)) or f(f(ab)e).)

Two principal approaches to handling associativity or commut.tivity are available. The first, standard approach is to represent the terms conventionally, i.e., f(af(be)) or f(f(ab)c) rather than f(abe), and axiomalize the associativity or commutativity properly. The associativity axiom would be f(xf(yz))=f(f(xy)z) and the commutativity axiom would be f(xy)=f(yx). These axioms could be applied using some equality inference rules such as paramodulalion [5].

*Research supported by the National Science Foundation (GJ-28457X2) and by the Advanced Research Projects Agency of the Secretary of the Office, of · Defense (F44620-73-C-007 4).

The second approach represents associative functions as functions with an arbitrary number of arguments, i.e., uses f(abc) rather than f(af(bc)) or f(f(ab)c). Special purpose unification algorithms are provided for terms whose functions are associative, commutative, or both. Examples of this approach in first order predicate calculus theorem proving are the work of Nevins [2] and Slagle [8]. The algorithms for associativity, and for associativity and commutativity are incomplete, i.e., they fail to return all the unifiers in some cases. An example of this approach in the area of programming lanauaaes for problem solving is the use "' the associative data type tuple or vector and associative, and commutative data type b1g in the QA4 and QLISP languages [7 ,4]. Again, in this ease the algorithms for pattern matching (unifying) these expressions 1re incomplete. In both these cases, the incomplete algorithms can be augmented by a process which alters the input expressions to cause the unification algorithm applied to the altered expressions to return 1dditional unifiers. The addition of this process (Slagle's widening operation for the first order predicate calculus [8] and Stickel's variable splitting operation for expressions of QA4 and QLISP [9]) results in completeness. Widening and variable splitting are both operations that must be performed on one or both input expressions an arbitrary number of times, replacing single variables of the expressions uniformly by two variables; it iJ essentially (repeated) paramodulation by the functionally reflexive axiom.

An example of the latter approach· is the unification of f(abz) and f(xy) where f is associative and commutative. The special purpose unification algorithm would return the unifiers {x .... a, y .... f(bz)}, {x .... b, yf-f(az)}, {x .. z, y .. f(ab)}, {x .. f(bz), y .. a}, {xH(IZ), yf-b}, and {x .. f(ab), y .. z}. But this is an incomplete set of unifiers since the possibility that the value of z is not wholly contained in either the value of x or the value of y is not represented. After performing 1 widenin& operation on f(abz) resulting in f(abz 1 z2) by instantiatinc z by f(zl z 2 ), additional new unifiers such 11 {x .. f(az 1 ), yo-f(bz 2 ), z .... f(z 1 z2>l and {x .... f(abz 1 ), y .. z2, z .. f(z 1 z 2 )} are returned by the unification algorithm.

Related to this approach, though different in detail, is Plotkin's work on the theory of building in equational theories [3] of which associativity and commutativity are examples. In the case of associ1tivity, Plotkin retains terms in 1 normal form: right associative form, although it could equivalently h1ve been our unparenthesized form. His equivalent of the widening rule, the replacement of 1 variable by two new variables, is applied continually inside the unification algorithm rether than being used outside it. Thus his unification algorithm may generate en infinite number of unifiers as opposed to a unification algorithm r;uaranteed to produce a finite number of unifiers and 1 potentially infinite process (widening) for altering inputs to the unification alr;orithm to obtein additional unifiers. The difference in approaches seems to be principally one of ora1niution of the seerch process.

In this paper, we present 1 new speci1l purpose unificetion 1lgorilhm which we call the AC unification algorithm for terms whose functions 1r1 1ssoci1!ive 1nd commutative which returns a complete set of unifiers. This elr;orithm eliminetes the need for 1xiom1lizina 1ssoci1livity and commutativity and 1lso eliminates the cost of continually applyinr; these axioms which often results in much unnecessary or redundant compul1!ion. It 1lso elimin1tes the need for usinr; the process of widening or v1riable splitting whose necessity (for discoverinr; a complete set of unifiers in the case of unifyin& 1ny p1rlicul1r p1ir of expressions) is

difficult to ascertain.

Terminology

Qefjnjtjon. A !.atm. is defined to be

(l ) 1 constant,

(2) a variable, or

(3) a function symbol succeeded by 1 list of terms (the arr;umenta of the function).

We sh1ll use the symbols a, b, 1nd c to represent constants, x, y, and z (possibly indexed) to represent variables, 1nd I to represent 1 function which is ISSOC:iative and commutative.

Qefjnj!jon. A sybs!j!y!jon component is In ordered pair of a variable v and 1 term I written IS v .. t. A substitution component denotes the assicnment of the term to the variable' or the replacement of the veri1ble by the term.

Qefinjlipn. A sybstj!y!jon is a set of substitution components with distinct first elements, i.e., distinct variables being aubatiluted for. Applying 1 substitution to en expression results in the replacement of those veriables of the expre11ion included among the first elements of the substitution components by the corresponding terms. The substitution components 1re epplied to the expression in parallel end no Vlriable occurrence in the second element of a aubatitution component will be repl1ced even if the variable occurs as the first element in another substitution component. Subalitutiona will be represented by the aymbola w and I . The application of substitution I to expression A is denoted by AI. The composition of substitution· lw denotes the substitution whose effect is the nme 11 first 1pplying aubstitution I, then applyinr; aub1titution w, i.e., A(lw) · (All­ for every expre11ion A.

Qafjnjtjon. A Ulli1xi.n1 sybs!j!yljpn or llllifW: of two expreniona ia a substitution which when epplied to the two expre11ions results in equivalent expreasions. In ordinery unification, two expressions are equivalent if 1nd only if they are identical . In unification of argument li1!1 of commul1live functions, two expressions are equivelent if they heve the same function symbol and the nme ergumenl1 in the ume or different order.

Oefjnjtjpn. T arm 1 is an ~ of term t, end I is 1

r;aneraljza!jpn of s, if there exists 1 substitution I such lh1!

!las.

Similarly, substitution I is an instance (generalization) of substitution tt if, for every term t, II is . 10 inslence (r;eneralizalion) of Itt.

The AC Unjfjcaljon Algorj!hm

We present here an algorithm for unifyinr; two terms whose function is associative and commutative. Terms will be represented 11 if the function had 1n arbitrery number of arr;uments with no superfluous parentheses.

We will assume that the argument lists of the two terms beinr; unified have no common arguments. Thi1 presents no difficulty since no unifiers are lost and efficiency is gained if common arr;umenl1 are elimineted immedi1lely. This is done by removinr; common arguments 1 peir at I lime, one from each of the argument lists. For example, before unifying f(xxyabc) and f(bbbcz), the b's common to the two terms ere removed yieldinr; f(xxyac) end f(bbcz), 1nd the c's common to the two new terms are removed yieldinr; f(xxye) and f(bbz) . An example of the utility of immedi1!ely removinr; common arr;uments is the unification of f(r;(x)y) and f(r;(K)g(a)). If the g(K)'s conimon to !he two terms are immediately removed, the unification algorithm will return the most r;eneral unifier {y .. g(a)}. If the common g(x)'s ere retained, unification will likely result in the generetion of the additional less r;eneral unifier {x .. e,y .. g(e)}.

The alr;orithm will be expressed pertielly in terms of an algorithm for the complete unific1tion of terms with an associative and commutative function with only variables II arr;uments. The result of unifying such terms is an assignment to each veriable of the terms some sequence of terms. Each variable is assir;ned a term I; (whose 141nction symbol is not f) or a term f(t 1 nl...tmnm) (with n; occurrenc11 of term I; as arguments of f). For such 10 assiKnment to be 1 unifier, the only requirement is that for 11ch term I; used in any assilnment there ere the same number of occurrences of that term occurring as err;uments of I in each of the unified terms instantiated by the assignment. For exemple, in uniiying f(x 1 x 1 x 2 x 3 ) end f(y 1 y 1 y 2 ), if term tis part of 10me assignment to one of the variables, then 2 limes the number of occurrences of I in the assignment for x 1 plus the number of occurrences of I in the usignment for x2 plus the number of occurrences of I in the assilnmenl for x3 must equal 2 times the number of occurrences of I in the essiKnment for y 1 plus the number of oc:currencea of I in the essir;nment for Y2· For example, (xl .. f(bb), x2 .. f(eb), x3 .. 1, Y1 ... b, y 2 ~f(aabbb)) is a unifier of f(x1xlx2x3) and ICYJYIY2) s1nce there are 2 a's and 5 b's in the instantielions of f(xl x1.x2x3l

and f(yl y 1 y 2 ) with the unified term beinr; f(eabbbbb).

With each pair of terms with 10 essoc:i1tive 1nd commutative function with only verieble arr;uments is associeted 1 single equelion representing the number end multiplicity of variables in eech term. For aXImple, the equation 2x 1 ·x 2 ·x 3 · 2y 1 ·y2 is associated with the peir of terms given above. This equation succinlly representa the condition for 1 substitution to be 1 unifier: the! the sum of the number of occurrences of eny term in the velue of each varieble multiplied by the multiplicity of the verieble in the term must be equel for the two Ierma.

Non-ner;etive inler;r al solutions to 1uch equation· ceo be used to represent unifiers. The solutions must be non-negative integral since each variable must be assigned 1 non-negative integral number of occurrences of each term.

In order to generate all the solutions to the problem of unifying the two terms, it is necessary to be able to represent all the solutions to the equation derived from the terms. Every non-negative integral solution to the equation is representable as a sum of elements of a particular finite set of non-negative integral solutions to the equation, i.e., every non-negative integral solution to the equation is a sum (equivalently, a sum with non-negative integral weights) of elements of a particular finite set of non-negative intural solutions. The finite set of non-negative integral solutions by whose addition the entire non-negative integral solution space is spanned is generable by generating in ascending order of value solutions to the equation, eliminating those solutions composable from those previously generated. This process can be made finite by placing 1 bound on the maximum solution value which will be used; such 1 maximum is proved in 1 later lemma to eliminate no needed solutions.

Consider the equation 2x1·x2·x 3 · 2y 1 ·y 2 . Solutions to the equation are:

Associated w.ith each solution above is a new variable (in the rightmost column). The assignment of as many occurrences of that variable as specified in the solution to each of the variables of the original term results in a partial solution to the unification of the the original terms. In particular, the assignment of 2 occurrences of variable z 3 to x3 and I occurrence to y 1 results in an equal number of occurrences of variable z 3 in each of f(x 1 x 1 x2x3) and f(yl Y2l·

Every non-negative integral solution to the equation is a (non-negative integer weighted) sum of the 7 solutions presented above, i.e.; every solution is representable as x1·z6·z7, x2·z2·z4·2z5, x 3 ·z 1 ·2z 3 ·z 4 , y 1 =z 3 ·z 4 ·zs·z 7 , Y2·z 1 ·z2·2z6 for some non-ne~ative inte~ral values of z1, ... ,z6. However, not every solution to the equation is 1 solution to the unification problem for which the equation was derived. There is an additional constraint that each variable of lhe original terms must be have at least one term in its value; it cannot have zero terms in its value.

Hence, we must form that subset of the 2 7 ·128 sums for which each element of the 5-luple is non-zero. (II is not necessary to consider sums in which any solution has a coefficient other than 0 or I since such solutions (in the unification problem) are already representable since the solution's inclusion with coefficient I introduces a variable which can have as its value an arbitrary number of terms as arguments of f thus simulating the case of the coefficient being greater than 1.) There are 69 such sums including for example (representing the sum by the set of its indices) (2,3,6 }, (1,2,3,6 }, and (4,6} with associated unifiers (x 1+-z6, x2+-z2, x3+-f(z3z3l, y 1+-z3, y2+-f(z2z6z6)}, (x 1 +-z 6 , x 2 +-z 2 , x 3 +-t<z 1 z 3 z 3 ), y 1 +-z 3 , y 2 +-f(z 1 z 2 z 6 z 6 )},and

(x 1 o-z 6 , x 2 +-z 4 , x 3 +-z 4 , y 1 +-z 4 , y 2 +-t(z 6 z 6 )}.

Note that if a variable could have as its value zero terms rather than one or more terms as in the first order predicate calculus, it would be unnecessary to form this subset of 2n (where n is the number of solutions) sums. Only the sum of all the solutions would be required since any variable present in this sum could have value zero, and the variables in the corresponding unifier could be matched against zero terms. This is the situation wilh fragment variables in the bag data type in QA4 and QLISP [7,4] (see [9]).

To be more precise in the definition of the algorithm, the algorithm consists of the following steps:

• I . Form an equation from the two terms where the coefficient of each var iable in the equation is equal to the multiplicity of the corresponding variable in the term.
• Generate all non-negative integral solutions to the equation eliminating all those solutions composable from other solutions.
• Associate with each solution a new variable.
• For each sum of the solutions (no solution occurring in the sum more than once) with no zero components assemble 1 unifier composed of assignments to the oric;inal variahlei with as many of each new variable as specified by the solution element in the sum associated with the new variable and the original variable.

Now we present the complete algorithm for unifying general terms with associative and commutative functions using the algorithm for the variable only case above. We ere here concerned with terms whose function is associative and commutative with arbitrary arguments, i.e., arguments that may contain ordinary (non-associative, non-commutative) functions or f or other functions which are associative and commutative. We assume the presence of ordinary unification to deal with those aspects of the unification problem not dealt with explicitly here.

First, when unifying two terms, two new terms with only variable arguments are formed by uniformly replacing distinct arguments by new variables. These new terms have only variable arc;umenls and are generalizations of the original two terms. For example, in unifying f(xxya) and f(bbz), we form generalizations f(x1x1x2x3l and f(Y1Y1Y2l with substitution (x 1 +-x, x 2 +-y, x3 .. 1, yl+-b, y2+-z} instantiatinc; the new terms to the ori~inalterms.

Next, using the previous algorithm for the variable only case, we unify the generalizations of the original terms. This has already been done for the example above resultin& in 69 unifiers as stated previously.

Now we have the c;eneralizations of the two original terms, a substitution to instantiate them to the original terms, and a complete set of their, unifiers. Every unifier of the original. terms is 1 simultaneous instance of the substitution to instantiate the generalizations to the original terms and a unifier of the generalizations. So all that is necess~ry to get all the unifiers of the original terms is to unify (for each variable being substituted for) the value in the substitution and the value in the unifiers.

In the example, x3 must have value 1 end y 1 must have value b. Thus, any unifier of f(x 1 x 1 x 2 x 3 ) and f(y 1 y 1 Y2l which assigns to x3 or Y2 a non-variable, i.e., a term of the form f( ... ) may be immediately excluded from consideration since the unification of it with the assignment including x 3 +-a and y 1 +-b will fail. (This constraint could be applied durin~t the ~teneration of sums of solutions to the equation rather than afterwards.) This constraint eliminates 63 of the 69 unifiers, leaving sums (I) {4,6}, (2) {2,4,6}, (3) {1,5,6}, (4) {1,2,5,6}, (5) {1,2,7}, and (6) {1,2,6,7} with associated unifiers

(I) {x 1+-z6, x2+-z4, x3+-z4, y 1+-z4, y2+-f(z6z6)},

(2) {x 1 .... z 6 , x 2 +-f(z 2 z 4 ), x 3 +-z 4 , y 1 +-z4, y2+-f(z2z6z6)},

(3) {x 1 +-z 6 , x 2 +-f(z 5 z 5 ), x 3 +-z 1 , y 1 +-z5, y2+-f(zlz6z6)},

(4) {x 1 +-z 6 , x 2 +-Hz 2 z 5 z 5 ), x 3 +-z 1 , y 1 +-z 5 , y 2 +-Hz 1 z 2 z6z6)},

(5) {x 1 +-z 7 , x 2 +-z 2 , x3+-z1, y l+-z 7 , y 2 ... f(zl z2)}, and

(6) {x 1 +-f(z 6 z 7 ), x 2 +-z 2 , x 3 +-z 1 , y 1 ... z7, Y2 ... f(z1 z2z6z6)}.

Unifying each of these with {x1 ... x, x2 ... y, x3 ... a, Y1 ... b, y 2 ... z}, we obtain

(I) no unifier since z 4 .... and z 4 ... b are not unifiable,

(2) no unifier since z 4 .... and z 4 ... b are not unifiable,

(3) fx+-z6, yH(bb), zH(az6z6)} (· fy ... f(bb), z ... f(axx)}),

(4) {x+-z 6 , y+-f(bbz2), z ... f(az2z6z6)1 (· {y ... f(bbz 2 ), zH(az2xx)}),

(5) {x ... b, y ... z2, z+-f(az2ll (· lx+-b, zf-f(ay))}), and

(6) {xH(bz 6 ), y .... z 2 , z+-f(az2z6z6)1

(· {xH(bz 6 ), z+-f(ayz 6 z6)}). This is a complete set of unifiers of f(xxya) and f(bbz).

Since x 3 and y 1 of the variable only case correspond to a and b respectively, and a and b are not unifiable, any sum including solution 4 to the equation 2x1·x2·x3 · 2y1·Y2 can be excluded from consideration since it would require (as in (1) and (2) above) the unification of 1 and b. As with the constraint on variables corresponding to non-variable terms not being assigned more than one variable (terms of the form f( ... )) in the variable only case, this latter constraint on solutions can be appl ied during the generation of unifiers in the variable only case rather than afterwards. Elimination of solution 4 before generation of the 2 11 sums, and elimination of sums which do not meet the first constraint would result in the formation only of unifiers (3), (4), (5), and (6) of the variable only case, each of which has 1 corresponding unifier in the &eneral case.

More precisely, the algorithm consists of the following steps:

1. Form ceneraliutions of the two terms replacing each distinct argument by 1 new variable.
2. Use the algorithm for the variable only case to generate unifiers for the generalizations of the two terms. The variable only case algorithm may be constrained to eliminate the genertlion of unifiers assigning more than one term to variables whose value must be a single term, and the generation of unifiers which will require the later unification of terms which are obviously not unifiable.
3. 3 . Unify for each variable in the substitution from step I and the unifiers from step 2 the variable values and return the resultin& assignments for vari1blas of the original terms. This is a complete set of unifiers of the original terms.

Proof of Termination Soundness, and Comple!tnas;a of !he AC Unification Algorithm

We. will first establish the validity of eliminating ar&uments common to the two terms. This will be done by proving that any unifier of the terms is 1 unifier of the terms with 1 peir of common arguments removed and vice versa.

Thaorem. Let s 1 , ... ,sm,t 1 , ... ,In ba terms w.ith si·t j for some i,j. Let I be a unifier of f(s 1 ... sm) and f(t 1 ... In), an<l let " be a unifier of Hs1 ... si-1 si·1 ... sm) and f(tl ... tj-1 'i·1 ... tn>· Then (1) 1 is a unifier of f(s 1 ... si-lsi·l ... sm) and f(t1 ... tj·l'j·l ... tn), and (2)" is a unifier of f(s1 ... sm) and f(t 1 ... In).

Proof.

I. f(silf(s 1 ... si_1 si.1 ... sm)l) · f(s l · .. sm)l · f(t 1 ... tn)l · f(tjlf(t1 ... tj-1 tj·l ... tn)l), and si,.tl . Th~rafore f(s 1 ... si-1 si·l ... sm)l · f(t 1 ... tj-l tj·1 · .. tn)1 arid I 11 a umher of f(s 1 ... si-1 si·1 · .. sm) and f(t I ... l;-11j·l ... In).

2. f(s1 ... si-lsi+l "·sm)" · f(t 1 ... tj·I'J·I "·tn)" and sitt·t j'· Therefore f(si"f(s 1 ... si-1 si·l ... sm)tt) · f(s l · .. sm), · f(t 1 ... tn)" · f(t;ttHil ... ti-ltj·l ... tn)") and " is a unifier of f(sl ... sm) and f(t 1 ... In>· 1,1EO.

Tha lemma beiow establishes that every non-negative integral solut ion to an equation of the form ·1 x 1· ... 1mxm · b1y1· ... ·bnYn is composabla as a (non-negative integral weighted) sum of a fixed finite set of non-negiltive integrel solutions. It also establishes a solution value within which all the non-negative integr~l solutions in the set may be found ..

L.Amm.l.. Every non-negative integral solution (x 1 , ... ,xm,Y 1 , ... ,y n> to the equation ·1 x 1· ... ·amxm b 1 y 1 · ... ·bny n with positive integral coefficients ·1 , ... ,am,b 1 , ... ,bn is an additive linear combination of non-negative integral solutions with value al x1· ... ·amxm (·b1y1· ... ·bnYnl less than or equal to the maximum of m and n times the maximum of the least common multiples of pairs of numbers one from al , ... ,am and one from b 1 , ... ,bn.

Proof. Assume with no loss of generality that the least common multiple (lcm) of a 1 and b 1 is the maximum of the leu! common multiples and that m~n.

Proof by induction on the value of 1 solution k.

k·O. The solution with k·O with x 1 ·0, ... , xm·O, y 1·0, ... , y n·O is genarable 11 the additive line1r ~ombination of non-negative integral solutions with value less than or equal to m*lcm(a 1 ,b 1 ) with zero coefficienta.

Assume the lemma is true for every non-negative integral solution with value less than or equal to k. Prove it is true for k.

Case I . k 5 m*lcm(a 1 ,b 1 ). In this usa, the solution is included among the non-negative integral solutions with value less than or equal to m·lcm(a 1 ,b 1) and the lemma is true.

Cese 2. k > m·lcm(a1,bl). Since a1x1· ... ·amxm · k > m*lcm(al ,b 1 ), and each ai·xi>O, at least one aixi must ~· greater than lcm(a 1 ,b 1 ), and xi must be greater than lc:m(a 1 ,b 1 )/ai . Similarly, since blyl· ... ·bnYn · k > m*lcm(a1 ,b1 ), and each b;Y·>O, and n5m, at least one bjYj must be greater than lcm(a 1 .~ 1 ), and Yj must ba greater tlian lcm(a 1 ,b 1 )/b·. Consider the solution with xi·lcm(ai,b·)/ai, Ytlcm(ai,bl)/b;, and all other v~ri ables zero. This is just the solution in -lowest terms involving only xi and Yj and h11 value lcm(ai,bj) S lcm(a1 ,b1 ). Since lcm(al ,bl )/ai ~ lcm(ai,b;ll·i and lcm(a1 ,b1 )/b; ~ lcm(ai,b;l/b; by the maximality of lcm(a 1 ,b 1 ), the solution involving only xi and y j can be subtracted from the solution with value k leavin~ 1 non-negative integral solution as result . But this difference solution has value k·lcm(ai,bj) < k and is thus composable from solutions with value less than or equal to m*lcm(al ,b 1 ). Therefore, the solution with value k > m*lcm(al ,b 1) is the sum of some solution involving only xi end Yj with value less than or equal to lcm(a 1 ,b 1 ) and some other set of solutions with value less than or equal to m*lcm(al ,b 1) and the lemma is true for this case. QED.

The lemma proves an upper bound on solution values that must be examined in the determination of a complete set of non-negative integral solutions which span the non-negative integral solution space by addition. We believe that tighter bounds can be proved. Although a proof for a tighter bound would be desirable, it should be noted that a lower proven bound would not reduce the number of found solutions theoretically necessary, but only decreases the cost of computing them, and would have no effect on the form or number of unifiers returned by the algorithm. This is true since any additional solutions discovered using a higher bound than necessary must be composable from solutions bounded by any proven lower bound and would therefore be recognized as redundant and be omitted.

The maximum of the least common multiples of the coefficients one from the left side and one from the right side of the equation is 1 lower bound on solution values which must be examined, i.e., solutions with at least this value must be examined. This is because one of the needed solutions not otherwise generable is the solution involving only the variables with those two coefficients with meximum least common multiple and having Vllue equal to the maximum least common multiple.

Theorem. The AC unification algorithm for terms with associative and commutative function with only variables as aq~uments always terminates, is sound (returns no substitutions which are not unifiers), and is complete (every unifior is an instance of a returned unifier).

Proof. The algorithm is guaranteed to terminate since it performs a finite number of operations on the finite number of non-negative integral solutions generated from the equation corresponding to the two terms. The generation of these solutions is finite due to the trial solution values being bounded.

The algorithm is sound since each solution of the derived equation causes the introduction into each of the instantiated terms of an equal number of new varieble occurrences. Thus, the two instantiated terms have the same number of occurrences of each new variable and are therefore unified.

Any unifier must assign to each variable 1 term of the form ti (whose function symbol is not f) or a term f(t 1 n l ... tm11m) (with ni occurrences of term ti as arguments of f) . Let k be the cardinality of the set of such terms ti in any solut ion to the unification of a pair of terms with only variables as arguments. The two instantiated terms must have an equal number of occurrences of each of these k terms as arguments of f. That is, a 1 ci 1 · ... ·arncim = b 1 di 1 · ... ·bndin (I ~i~k) where m is the number of distinct variables in the first term being unified, n is the number of distinct variables in the second term, I · is the .multiplicity of the jth variable in the first term, bj is \he multiplicity of the jth variable in the second term, c 1 .i is the number of occurrences of term i in variable j in ne first term, and dij is the number of occurrences of term i in variable j .in the second term.

Each tuple (ci 1 , ... ,cim·di 1 , ... ,din) is a solution to the equation a 1 x 1 · ... ·amxm = b 1 y 1 · ... ·bny n corresponding to the terms being unified. It can thus (accordin~ to the lemma) be formed as the sum of certain non-negative integral solutions to the equation weighted by positive integers.

Consider the unifier corresponding to the sum of all those solutions to the equation which are required in the formation of any of the tuples (ci 1 , ... ,cim·di 1 , ... ,din). We will show that the hypothesized unifier is an instance of this unifier returned by lhe algorilhm.

Include in the value of the new variable associated with each of these solutions a number of occurrences of term i equ·l to the coefficient of the solution in the weighted sum. This will result in the proper assignment of cij occurrences of term i to eech variable j of the first term end dij occurrences of term i to each variable j of the secona term.

Do this for each of the k terms in the solution. Let no other or edditionel terms be included in the values of the new variables.

This assignment of terms in the solution to new variables associated with equation solutions generated in the unification process results in the correct number cij or dij' of each term being assigned to each variable of the original wo terms.

Thus, any solution to the unification of two terms with only variables as arguments is an instance of a returned unifier and the algorithm is complete. QED.

Theorem. The AC unification algorithm for general terms with associative and commutative function always terminates, is sound, and is complete.

Proof. Let s and I be any two terms being unified. Let s* and t* be the terms resulting from replacinr; each distinct term by a new variable. s* 1nd t* are generalizations of s and I respectively, i.e., s*l·s 1nd t*lcl for some I of the form { ... ,xi .. ci, ... } where each xi is a new variable and each ci is the term in s or I it repl1ces in c* or t*.

Let {orj} denote the unifiers of s* 1nd t* returned by the unification al~orithm for terms with usociative 1nd commutative function with only variables as ar~uments. Each "j is of the form { ... ,Kj'"di, ... } where each xi is a variable of s* or t* and di is the term assigned to it by the unification algorithm. Accordin~t to the previous theorem, unific1tion ·terminates, is sound, and is complete for this c1se.

Simultaneous instances of I and "j represent unifiers of s and I since s*l·s, t*l=l, and s*"t'*·j·

Unifying each ci with each di of a returned unifier " . of s* and t* results in (by the assumption of termination, soundness, and completeness of the recursive call on the unification algorithm for terms of lesser complexity) a complete set of unifiers for the original terms s and I. QED.

We have presented an algorithm for unifying general terms with associative and commutative function. We have proven that the algorithm is gueranteed to terminate, is sound, and is complete.

The advantages of this elgorilhm as compared to other epproaches to unifying such terms are that the associativity and commutativity properties need not be axiometized and the! ell the unifiers of a pair of such terms are immediately returned . eliminating the unnecesury and redundant compulelion often occurring in other approaches which generate only some of the unifiers at each step with no indication of when all the unifiers heve been generated.

Bibliamphy

• Chang, C. L. and Lee, R. C. T. Symbolic· l.otic ami Mnchnrricol Tlwtort!ln ProtJirrg. Acedemic Press, New York, 1973.
• 2 Nevins, A. J. A human oriented logic for automatic theorem proving.}. IJCM 21, 4 (Oct. 1974), 606·621.
• 3 Plotkin, G. D. Building-in equelionel theories. In Meltzer, B. and Michie, D. (Eds.). Machine /rut!lligertce 7, Edinburgh University Press, Edinburgh, 1972, pp. 73·90.
• 4 Reboh, R. and Secerdoti, E. A preliminary QL!SP manual. T ec:hnic:al Note 81, Artificial Intelligence Center, Stanford Researc:h Institute, Menlo Park, Calif., Aug. 1973.
• 5 Robinson, G. end Wos, L. Peramodulalion and theorem·proving in firsl·order theories with equality. In Meltzer, B. and Michie, D. (Eds.). M ar.hirrf! I ruelligerrce 4, Edinburgh University Press, Edinburr;h, 1969, pp. 135-150.
• 6 Robinson, J. A. A mac:hine·oriented logic based on the resolution principle. }. IJCM 12, I (Jan. 1965), 23·41.
• 7 Rulifson, J. F., Derksen, J. A. and Waldinger, R. J. QA4: 1 procedural calculus for intuitive reasoning. Technical Note 73, Artificial Intelligence Center, Stanford Research Institute, Menlo Park, Calif., Nov. 1972.
• 8 Slagle, J. R. Automated theorem-proving for theories with aimplifiers, commutativity, and associativity. } . IJC41 21, 4 (Ott. 1974), 622-642.
• 9 Stickel, M. E. Unific:ation alr;orithms for artificial intelligence languar;es. Chapter of incomplete Ph.D. Dissertation, Department of Computer Science, Cernegie·Mellon University, Pittsburgh, Penn.