Universal Unification and Regular Equational ACFM Theories

UNIVERSAL UNIFICATION AND REGULAR EQUATIONAL ACFM THEORIES

J. Siekmann, P. Szabo

Universitat Karlsruhe lnstitut fUr lnformatik I

D-7500 Karlsruhe, Postfach 6380

ABSTRACT. A universal minimal type conformal mat­ chlng algorithm and a universal minimal unification algorithm based on [FA79J, [SL74J, [LB79J, [HUBOJ are presented for a restricted class of equational theories (the Regular ACFM Theories), i.e. it is shown that the set of most general unifiers is re­ cursively enumerable for this class. The class of Regular ACFM Theories is wide enough to containmost special cases of unification algorithms that have been investigated so far. This paper is a (very) abbreviated version of [SS81cJ, all proofs and most of the technical material are omitted for lack of space . For reasons of consistency with the original paper, the numbering of definitions, lemmas and

theorems has been retained.

1.1 INTRODUCTION

Unification theory is concerned with problems of the following kind: Let f and g be function symbols, a and b constants and let x and y be variables and consider two first order terms built from these sym­ bols; for example:

The first question which arises is whether or not there exist terms which can be substituted for the variables x andy such that t 1 and t 2 become equal: in the example g(a,b) and a are two such terms. We shall write

o 1 = {x+g(a,b), y+a} for such a unifying substitution: o 1 is a unifier of t 1 and t 2 since o1t1 = o1t2.

In addition to the decision problem there is alsothe problem of finding a unification algorithm which generates the unifiers for a given pair t 1 and t 2 . Consider a variation of the above problem, which

arises when we assume that f is commutative:

Now o 1 is still a unifying substitution and more­ over o 2 {y+a} is also a unifier for t 1 and t 2 ,

• (C) f(x,y) = f(y,x) since

But o 2 is more general than o 1 , since o 1 is an in­ stance of o 2 obtained as the composition Aoo 2 with A= {x+g(a,b)}; hence a unification algorithm only

needs to compute o 2 .

There are pairs of terms which have more than one most general unifier (i.e. they are not an instance of any other unifier) under .commutativity, but they always have at most finitely many. This is in con­ trast to the first situation (of free terms), where every pair of terms has at most one most general unifying substitution.

The problem becomes entirely different when we assume that the function denoted by f is asso­ ciative:

• (A) f(x,f(y,z)) = f(f(x,y),z) In that case o 1 is still a unifying but substitution,

But o 4 = {x+f(g(a,b), f(g(a,b), g(a,b})), y+a } is again a unifying substitution and it is not diffi­ cult to see that there are infinitely many unifiers, all of which are most general.

Finally, if we assume that both axioms (A) and (C) hold for f then the situation changes yet againand for any pair of terms there are at most finitely many most general unifiers under {A) and (C).

Many special unification algorithms for common theo­ ries have been developed in the past, since they have important applications in computer science [RSS79J. In particular, they are a crucial compo­

nent of automatic theorem provers and of many programs developed in artificial intelligence. We shan now briefly review a formalism to express problems of the above kind.

1.2 UNIVERSAL UNIFICATION

Let F~ be the initial algebra of free terms whose elements are given a concrete representation by:

• (i) X, the set of variables, is in F~

(ii) for fU"l , the set of function symbols, and

t 1 , .. . ,t 2 EF~ :f(tl' ... ,tn)EFr1 iff rlf = n. [SS8lcJ provides a brief survey of the logical and algebraic background of unification theory. In this abbreviated version it is however sufficient forthe reader to have an intuitive notion of first order terms.

Let o:X~F~ be a mapping which is equal to the iden­ tity mapping almost everywhere. A substitution o :F~~Fn is the homomorphic extension of o and isre­ presented as a finite set of pairs

r is the set of substitutions on F~. If tis a term and o a substitution, let V(t) denote the set of variables occurring in t and define:

DOM( o) .- {xEX: ax * x}

COD(a) :={ox: xEDOM( o)

IV( o) := {xEV(p): p E COD( a)}

An equations= t, s,tEFrl is unifiable (is solvable) in the algebra A iff there exists a homomorphism t; : F~ ~A such that t;s = f;t is valid in A. A set of equations T induces a congruence =Tin F~ andF~/- is the quotient algebra mo~ulo =T. -T

For simplicity of notation we assume we have a box of symbols, GENSYM, at our disposal, out of which we can take an unlimited number of "new" symbols:

We shall adopt the computational proviso that when­ ever GENSYM is referenced by v E GENSYM it is sub­ sequently 'updated' by GENSYM' = GENSYM - {v} and X' = X u {v}. Since F., "" F,.,t we shall not always 0 0 " " keep track of the '-sand just write F~.

A renaming substitution p E REN c r is defined by

( i ) COD( p) c X ;

(ii) vx,yEX: if x * y then px * py

For s,tE Frl : s - 0 t if 3pEREN such that ps = pt.

In order to formalize the accessing of a subterm in a term t let rr(t) be the set of positions in t(i.e. subterm addresses) and we denote a subterm oft at n, by tin. A subterm_ replacement of t by s pt n is ~t. with ~ = [n+sJ. For definitions see [HT80J. For example if t = f(g(a,b),c) then rr(t) = {A,1,2,1.1,1.2} and tl1.2 =b.

A A A We denote replacements by a, p, 6, etc. and substitutions by a, p, 6, etc.

A relation-+ c F~x Frl is Noetherian (terminating) if there are no infinite sequences : s 1 s 2 s 3 .... · t.is the transitive and -the reflexive and transitive closure of~. A relation ~ is aonfluent if for · · every r,s,tE F~ such that r - s and r - t there · · exists a u E F~ such that s - u and t - u. A confluent Noetherian relation is aanoniaal.

We define two important relations ~T and >+T on F~x F~ as follows:

A rewrite system R = {(1 1 ,r 1 ), ... (ln,rn)} is any set of pairs li,riEFn, usually writen as li .. ri, such that V(ri) s V(li), l si sn. For two terms s and t, we say s is paramodulated to t, s J+R t, if there exist nEIT(s), oEL and li·riER such that o(sln) = (o·p)li for some pE REN and COD(p) c GENSYM A A and t =as, where a= [n+(o·p)ri].

For example, for R = {g(x,O) .. 0} we have

• s = f ( g (a ,y) ,b) :r+ f ( 0, b) = t with n = 1 and a = {x+a, y+O}. The renaming sub­ stitution p is used to avoid any conflict between variables.

For two terms s and t, we say s is rewritten to t, s ~R t, if there exist nEIT(s), oEr and li·riER such that sin= (o·p)li for some pE REN and A A COD(p)EGENSYM and t =as, where o=[n+(o·p)ri]. If s and t are the same as in the above example then: s ~R t, since we are not allowed to substi­ tute into s. Occasionally we keep track of the in­ formation by writing s>----+ t and s - t . In [n,i,o] [n,i, o] addition, we use [A,A 0 ,EJ to express the reflexivity of~ resp. ~(i.e. Ao means: no 'rule' is applied). Thus s s for all sE F~. [A,A 0 ,E]

The notation and definitions of term rewrite sy­ stems are consistent with [HT80 J. Suppose for an equational theory T there is a rewrite system RT such that for s,tE F~:

s =T tiff 3pE FS"l such that s <toR p and t 'lkoR p. T T In that case we say T is embedded into R and write T T<---,RT.

For an equational theory T there are techniques to obtain a system RT such that T~RT; moreover for many theories of practical interest it is possible to obtain a rewrite system RT such that ~R is T

canonical [KB70J, [HT80J, [PS81J. Canonical relations ~are an important basis for computations in equational logics, since they define a unique normal . . forom II t II for any t E F S"l ' glVen by t - II t II and ~ s E FS"l such that lit II ~ s. Hence

• (i) s =T t iff llsll = lltll .

An equational theory T is decidable iff s = t is T deci dab 1 e for any s, t E F n· Let ~denote the family of decidable equational theories.

A T-unification p~obZem <S = t >T consists of a pair of terms s, t E F S"l and a theory T E .9[.

A substitution oEr is a T-unifie~ for <S = t > iff T as =T at. The subset of r which unifies <S = t>T is ULT(s,t), the set of unifie~s (for sand t) unde~ T. It is easy to see that UrT is recursively enumerable (r.e.) for any sand t: Since FS"l is r.e. so is r. Now for any 6EL. check if 6s =T 6t (which is deci­ dable since TE .9;'> then 6E urT(s,t) otherwise 6 ~ urT ( s, t ).

The composition of substitutions is defined by the usual composition of mappings: (o·T)t = o(Tt). If W c X, then T-equality is extended to substitutions by

a and T ~ T-equaZ in w. We say a is an instance of T and T is mo~e general than o, in symbols

T sT o(WJ iff 3/..Er T =T /..·o[WJ for some W c X.

If o ST T[WJ and T ST o(WJ then 0 ~T T(WJ, 0 and T are T- equivalent in W.

For r 1 ,r 2 s r we define

r 1 ·r 2 = {ol ·o 2 : o 1 E rl' o 2 E r ) . r 1 ST r 2 [W] iff vo 1 Er 1 3 o 2 Er 2 such that o 1 =T o 2 [WJ, r 1 = T r 2 [W) iff r 1 =T r 2 [W) and r 2 =T r 1 [W].

Universal unification is concerned with two funda­ mental problems:

PROBLEM ONE (Decidability P~oblem)

For a given equational theory T E j[. is it decidable fo~ any s and t whether s and t ~e uni­ fiable unde~ T?

We are interested in classes of theories such that "s and t are unifiable under T" is decidable for every T in that class.

A unifier a for <s = t>T is called a most gene~al unifier (mgu) if for any unifier

6E UrT(s,t): 6 so [WJ, where V(s,t) = W. Since in general a single most general unifier does not exist for <s = t >T , we define ~UrT(s,t), the set of most gene~al unifiers, as:

• (i) ~ur = ur (correctness)
• (ii) Ur=Tr·~Ur [WJ
• (completeness)

(iii) oi \ ok for i*k; oi,okE~Ur

(minimal ity).

From condition (ii) it follows in particular that Ur = r·Ur, i .e. uris a left ideal in the semigroup (r, · ) and Ur is gene~ated by ~UL. For practical applications these conditions are sometime too general and there are additional technical require­ ments on DOM( o), COD(o) and IV( a) for oE ~Ur, which we shall state when the need arises.

PROBLEM TWO (Enume~ation P~oblem)

Fo~ a given equational theory T E .?J;. is

~UrT(s,t) ~ecu~sively enume~able fo~ any s,tE FS"l?

That is, we are interested in algorithms which ge­ nerate all mgus for a given problem <s = t>T . TABLE 1 summarizes the major results that have been obtained for special theories, which consist of combinations of the following equations:

• A (associativity) f(f(x,y),z) = f(x,f(y,z))

C (c011111utativity) D (distributivity) H,E (homomorphism, endomorphism) ( i dempotence) f(x,y) = f(y,x) f(x,g(y,z)) = g(f(x,y),f(x,z)) f(g(x,y),z) = g(f(x,z),f(y,z)) IP(X·Y) = IP(X)*\P(y) f(x,x) = x

Moreover we use the following abbreviations:

QG: Quasi-Groups

AG: Abelian-Groups

HlO: Hilbert's lOth Problem

Sot : Second order terms

Hot: Higher order terms (i.e. ~ 3rd order)

The column under~T indicates whether or not a type conformal algorithm has been presented in the li­ terature. The type of a theory and type conforma­ lity are defined below.

Except for Hilbert's tenth problem, we have not in­ cluded the classical work on equation solving in 'concrete' structures such as rings and fields, which is well known. The relationship of universal unification to these classical results is similar to that of universal algebra to classical algebra.

The central notion IJUI: induces a hierarchy of clasT ses of equational theories .[SSSlbJ.

• (i) A theory Tis unitary if every <S = t >T has at most one mgu. The class of such theories is ~(type one).
• (ii) A theory Tis finitary if it is not unitary and for every <s = t >T IJUI:T always exists and is finite. The class of such theories is .~ ( type w).
• (iii) A theory T is infinitary if IJUI:T always exists and there exists <s = t > T such that IJUI:T is in­ finite. The class of such theories is~ 00 ( type oo ).
• ( i v) A theory T is of type zero if it is not one of the above classes. The class of these theories is~

There are several examples for unitary, finitaryand infinitary theories in the above table. An example of a type zero problem is the unification ofhigher order terms (which, however, usually assumes a syn­ tax different from Fn), since there are infinitely many ascending chains of unifiers under $T [G066J. We define a partial order $T on terms by: s $T t iff 3oEI: satisfying s = ct. A matching problem T <S ~ t> consists of a pair of terms and a theory T TE ~A substitution vEI: is aT-matcher (or oneway unifier) if vs =T t. If s and tare matchable we shall writes $T t (resp. s ~T t). The minimal set of matchers is IJMr , which induces the corresT ponding hierarchy ._1{; 0 , ... 16oo,._lt1J.)·._J~ · A unification aZgol'ithm AT (a matching aZgol'ithm M ) for a theory T is an a 1 gori thm which takes two T terms s and t as input and generates a set ~ c ur (c Mr ) for <S = t > (for <S ~ t > ). A T- T- T T T minimaZ algorithm IJAT (IJ~) is an algorithm which generates IJUI:T (IJMI:T).

For many practical applications this requirement is not strong enough, since it does not imply thatthe algorithm terminates for theories TE ..9?'" u .~· On the other hand, for T E .9". it is sometimes too riw gid, since an algorithm which generates a finite superset of IJUI:T may be far more efficient than the algorithm IJA and for that reason preferable. T

An algorithm A is type confonnaZ iff: T

• (i) AT generates a set ~T with UI:T ~ ~T ~ IJUI:T;
• (ii) AT terminates and ~Tis finite if IJUET is;
• and
• (iii) if IJUI:T is infinite then ~T ~T IJUI:T.
• Similarly: algorithmM is type conformal iff (i)- T (iii) hold with U replaced by M.

A universaZ unification aZgorithm (a univer>saZ matching aZgorithrl) for a class of theories ·-?u -= .~ is an algorithm which takes as input a pair ofterms ( s, t) and a theory T E 3u and generates ~ T 2 IJUI:T ( 2 IJMI:T) for <S = t >T (for <S ~ t >T).

Since urr is trivially r.e . for any TE ~· there is the important requirement that a universal uni­ fication algorithm is either minimal or at least type conformal. The known universal algorithms [FA79J, [LB79J, [HOSOJ are neither minimal nor type conformal; and even some special purpose unification algorithms, although they are minimal, are nottype conformal either.

2. THE CLASS OF ACFM THEORIES

An equational theory T is admissible (A) if the mat­ ching problem forT is decidable. This restriction pertains to all unification problems of practical interest, as otherwise a ~ 1 6 would be undecidable.

For the purpose of this paper we further restrict the admissible theories by requiring that T possess a con[Zuent reduc-tion system, i.e. a canonical (C) system.

The final restriction is the requirement that T constitutes a finitary matching problem (FM), i.e. that TE, /6w.The last restriction is less rigid than it appears: e.g. all special unification prob­ lems in TABLE 1 are in this class. On the otherhand, there exist very simple theories which do not fall into this class: LetT= {g{f(x)) = g(x)l; then <g{y) ~ g(a)> 1 has an infinite matching set:

Mr 1 = {y+a, y+f(a), y+f(f{a)), .... } . The class of equational theories T with T admissib~ and TE, /6.and T<--::>R for a canonical R is the W T T class of ACFM theories.

An equational theory Tis regular iff for every s = tET V(s) = V(t); similarly, a rewrite system R is regular iff for every l·r E R V(l) = V(r). For a regular theory T = {li=r;= 1 ~ i~nl the corresponding regular rewrite system can immediately be obtained as R 1 = { 1 i .. r i , r i .. 1 i : 1 ~isn}, and T <-:> R 1 is ob­ vious.

For regular theories we have an important property concerning the length of terms, in symbols ltl, de­ fined as the number of symbols in t.

To refer to the (least possible) length of rewrites, · let Is-. tl E ~ u {0} denote the smallest n such

that

2. Lemma 1. Let R be a regular rewrite system and mR = max{ lll, lrl: l·rER}. Then for any s,tEFn · · such that s -.R t and Is -.R tl= n ~ 1: lsl~m~·ltl

3. LOCALIZING THE TEST FOR T E, /6w

In order to test an equational theory T for the ACFM property let us assume it is admissible. Weal­ so assume that we have proved T....., R 1 , where R 1 is canonical, e.g. by using the techniques of [HT80J. Then there remains the test for TEJ6 which can w be difficult, since it has to be shown that vs,tEFn: luMr(s,t)IE~.

The test can be localized in the following sense:

3. Theorem 6: Let T be an admissible theory with a regular canonical reduction system R 1 such that T <--:> R 1 · If TE, It"' then there exists a ground sub­ stitution 1, (l.,r.) and {lk,rk)ER such that 1 1 T <li ~Trk>T

has an infinite matching set.

Hence, if there does not exist a pair <l ~ Tr> 1 with an infinite matching set, then TE._,.-#t; .It is an w open problem to find a local (and finite) test set for theories which are not regular.

4. UNIVERSAL UNIFICATION ALGORITHMS IN REGULAR ACFM THEORIES

A universal matching algorithm and a universal uni­ fication algorithm are presented in this section. Both algorithms take a regular ACFM theory T and a pair of terms as input and output the sets uMr 1 and uUr 1 respectively, hence the algorithms are univer­ sal in the sense that a universal Turing machine is 'universal'.

Throughout this section we slightly change the no­ tion of uUr 1 {s,t) by adding the following technical requirement:

In case (iv) is satisfied we shall write uUr 1 r--w and say 'uUY- 1 away from W' [PL72J, [H080J.

Let R be a canonical system. A substitution oEr is called normalized if for all tECOD(o) tis in nor­ mal form (i.e. t = lltiiR). Let [R c r be the set of normalized substitutions and analogously UrR (MrR) the set of normalized unifiers (matchers). We de­ note the normalization of substitutions as for terms, i.e. if oH then lloiiEL

4.1 The Paramodulation Tree

Let>- be the paramodulation relation on F 11 x F 11 as defined in section 1.2 with the additional proviso that we never paramodulate into variables, i.e. if s :>----+ t then slnf!X. The set (t>-)= {[sJ_ 0 :t !.s} [ n , i ,o]

is called the folrow set of>-, factored by the equivalence relation - 0 . Note that (t >-) is finite. For ease of notation we just write s for some re­ presentative of [sJ_ 0 . For a given term t we define the "labe "led parcunodulation tree P t as:

• (i) t (the root) is a node in Pt'
• ( i i ) if s is a node in P t and s E (s >-) then s (the successor) is a node in Pt;
• (iii) the edge (s,s), where s [ . J s, is labeled TT,l,a with the triple [n, i ,a].

The composition 'o' of labels is defined as [ TT 0' i 0 'a 0) 0 [ TT 1' i 1 'a1) = [ ( TT 0' TT 1) ' ( i 0' i 1) 'O 0 oa1) · In analogy to the notion of a derivation word in formal language theory we define the paramodu"lation word L*(Pt,s) for se: Pt by:

• (i) L*(t,t) = (A 0 ,A,£)
• (ii) L*(t,s) = L*(t,s) o (n,i,a) where s=>-s. [n,i,aJ

It is convenient to have selectors \,rr,G on L· defined by : L*(t,s) = (l(t,s), ~(t,s), G(t,s)).

The relationship between T-unification and the para­ modulation tree is shown up by the following con­ struction: for a problem <s = t >T define a term H = h(s,t), where h is a 'new' symbol with nh = 2, and consider PH:

• Theorem: (i) For every h(s,t) e: PH: if a is mgu of s and t then ao 0 e: lJI: ( s, t) T where 0=9(H,h(s,t))
• (ii) For every 15 E UI:T(s,t): there exists h(s,t)e:PH and a mgu of sand t SUCh that 15 ST ao0 where 0= G(H,h(s,t))

The first part of the theorem states that every sub­ stitution which is obtained from a Robinson unifier o for s and t and the labelword component ao0 is a correct unifier for <s = t>T. The second part of the theorem ensures compLeteness: for every .unifier 15 EUI:(s,t) there is a node in PH such that 15 is an instance of the substitution obtained at that node.

The proof of the theorem is immediate fromBirkhoff's theorem. It is also an immediate consequence of the correctness and completeness of paramodulation [WR7~. In the following we are concerned with refinements of the paramodulation tree incorporating those of CHU80J, lFA79J, [LB79J, [SL74J.

Lets be a term and Ps the corresponding paramodu­ lation tree. Then we define a refinement of Ps, the normaLized parcunodulation tree Ps' by: The generation of nodes in P s is stopped in case one of the follo­ wing two criteria is true: A node te: Ps is a "leaf

node iff C1: (t >-) = t'

C2: 0(s,t) ¢ r

The tree thus obtained is Ps.

1. UniversaL Matching ALgorithms in ReguLar ACFM Theories

For a given matching problem <s ~ t >T assume thatT is a regular ACFM theory and let Ps be the norma­ lized paramodulation tree for s. We extend the no­ tion of leaf nodes by the following criteria: se: ps is also a "leaf node if:

• C3: MI:(s,t) = t', i.e. t tT s, which is decidable since T is admissible.

We shall write ~Ps(t), the minimaL parcunodulation tree for s relative tot, if C3 is applied toPs and <s ~ t >T is the given matching problem.

The set of rna tchers obtai ned from ~P s ( t) is the most general set of matchers for s and t up to renaming :

Since T is an ACFM theory ~UI: is finite, and hence ~Ps(t) is finite except for the fact that there may be an infinite path in ~Ps(t) which is not termi­ nated by C3 (i.e. there are infinitely many T-equi­ valent matchers for <s ~ t > along the path). T

We have limited ourselves to regular ACFM theories, since they are applicable in most cases of interest An equational theory T is often separated into sub­ theories T = E u R such that R allows for a canoni­ cal reduction and for each s = te: E Var(s) = Var(t) holds, and interest is in (finite) unification al­ gorithms forE; see also [HT80J, [PS81J. All theo­ ries in TABLE 1 of section 1 are regular.

For nonregular ACFM theories the situation is notas simple and we suspect that a terminating universal matching algorithm does not exist. For many special cases a terminating matching algorithm is of course possible even in the nonregular case.

1. Universal Unification ALgorithms in ReguLar ACFM Theories

The universal unification algorithm of this section is based on the matching algorithm of 4.2 and onthe solvability of equations in the (rn,T)-algebra,wh~ n = {(o,2)}. For given substitutions o,tEr we should like to know if there is a third substitution oEr such that 6 = oot. That is, we are interested in T the solvability of equations in (rn,T): (i) 6 = vot , where 6,tEr and vis a variable T

ranging over substitution.

We say (i) has a most general set of solutions ~Mr (6,t) iff for every y such that 6 = yot there T T exists oE ~MrT(6,t) such that a ~T y.

4. Lerma 10. is wellknown, but with an unnecessarily complicated proof, in the case T = D [VA75J, since it is used to advantage in the connection graph proof procedure [K075J . We are now ready to state the main result of this paper.

The enumeration of ~ur (s,t) is based on the normaT lized paramodulation tree Pas defined in section 4.1. The check for minimality is based on the (one­ sided) ~P-tree.

~- Theorem 12: Let T be a regular ACFM theory. For ~ny s,tE Fn and W = V(s,t),

~ur (s,t) ~W is recursively enumerable. T

The proof of 4 Theorem 12 is constructive and hence specifies a universal unification algorithm. The proof is based on lemmas and technical material, which we had to omit for lack of space, see [SS81cJ. Note that the universal unification algorithm based on 4. theorem 12 may not terminate.

If a decision procedure is known for T-unifiability the paramodulation tree can be pruned considerably by an application of this procedure to each node: in case of nonunifiability the node is a leaf node. How­ ever even under this additional termination crite­ rion the paramodulation tree may grow indefinitely even if T E .¥.. which is to be expected in genera 1, w since we do not assume ~ur to be recursive. For certain classes of theories termination is of course possible.

5. CONCLUSION

We have presented theorems for a universal matching algorithm and a universal unification algorithm for regular ACFM theories. Both algorithms based on these theorems generate a complete minimal set of unifiers (of matchers) and termination of the mat­ ching algorithm is shown.

For nonregular ACFM theories the matching algorithm may not terminate and we suspect that uniform ter­ mination is unattainable.

Since most known special purpose unification algo­ rithms are based on regular ACFM theories and since this class allows for a comparatively simple uni­ versal unification algorithm, we believe this class may come to play a prominent rOle (similar to cer­ tain classes, like SLR(1), in formal language theo­ ry).

On the other hand, the 'abstract' universal algo­ rithm does not represent a practical solution for a given theory T, because of its gross inefficiency.

This contribution is of theoreticaZ relevance in that it exhibits a class of theories which possesses an r.e. set ~ur . This result can be applied in T practice for the design of an actual algorithm: So far the design of a special purpose unification al­ gorithm was more of an art than a science sincefor a given theory there was no indication whatsoever of how the algorithm might work. In fact the algo­ rithms in TABLE 1 of section 1 all operate on en­ tirely different principles.

The next 700 Uni fication ALgorithms

On the basis of the "abstract" universal unifi­ cation algorithm it is possible to find a concrete algorithm much more easily by first isolating the crucial parts in the abstract algorithm and then designing a practical and efficient solution. The universal algorithm has been successfully applied to a special case [RS78J, yielding a minimal al­ gorithm [SS81aJ, which in addition is much simpler than the one previously known. A collection of canonical theories [HU80aJ is a valuable source for this purpose and has already been used to find the first unification algorithm for Abelian group theo­ ry and quasi group theory [LA79J, [HU80J.