Difference Unification

1 Introduction

Motivation and Context

Heuristics for judging similarity between terms and sub­ sequently reducing differences have been applied to auto­ mated deduction since the 1950s when Newell, Shaw, and Simon built their "logic machine" [NSS63] for a proposi­ tional calculus. Their intent was to simulate the be­ havior of a human on the same task. More recently, in resolution theorem proving, a similar theme of dif­ ference identification and reduction appears in [BS88; Dig85; Mor69]. In this work a partial unification results in a special kind of resolution step (E or RUE-resolution) where the failure to unify completely produces new in­ equalities that represent the differences between the two terms. This leads to a controlled application of equal­ ity reasoning where paramodulation is used only when needed. The intention was not to design a human ori­ ented problem solving strategy, but rather, to use differ- Toby Walsh Dept. of AI, University of Edinburgh, 80 S. Bridge, Edinburgh, Scotland ( tw@aisb.ed.ac. uk)

· This research was partially funded by the German Min­ istry for Research and Technology (BMFT) under grant ITS 9102 and a SERC postdoctoral fellowship. The responsibil­ ity for the contents of this publication lies with the authors. We thank the Edinburgh Mathematical Reasoning Group for their encouragement and criticism, in particular Alan Bundy and Andrew Ireland.

ence identification and reduction as a means of reorder­ ing a potentially infinite search space.

Here we report on research sharing both these cog­ nitive and pragmatic aims. We have developed a gen­ eral procedure called difference unification for identify­ ing differences between two terms. Difference unification extends unification in that it decides if terms are syntac­ tically equal not only by giving assignments for variables but also by computing what incompatible term struc­ ture must be removed. This incompatible term struc­ ture, called wave-fronts, is marked by annotations which are used to direct a special kind of rewriting called rip­ pling; rippling seeks to reduce the differences between the terms by moving the wave-fronts "out of the way" while not disturbing the unannotated parts of the terms .

Related Work

This research is the outgrowth of previous work at Ed­ inburgh in inductive theorem proving. There Bundy [Bun88; BS+92] suggested that in proofs by mathemat­ ical induction, the induction conclusion could be proven from the induction hypothesis by rippling on the in­ duction conclusion. Rippling has been employed in the OYSTER/CLAM prover. A similar kind of rewriting was developed independently by Hutter [Hut90], from ideas in [Bun88], and employed in the INKA system. Both systems have enjoyed a high degree of success stem­ ming from several desirable properties of rippling. These include (see [BS+92]) that rippling involves very little search and rippling always terminates since wave-fronts are only moved in some desired (well-founded) way - usually to the top of the term.

Research Contributions

Motivated by a desire to apply ril?pling outside of induc­ tive theorem proving, in lBW92J we introduced differ­ ence matching which extends matching to annotate the matched term so it can be rewritten using rippling. We list there, as well as in [WNB92] several applications of this idea. In this report we take another step forward . Our contributions are several fold. First we extend dif­ ference matching to difference unification whereby sub­ stitutions and annotations are returned for both terms. The rule based algorithm we give uses conventional uni­ fication in a transparent way whereby other additions to unification, such as equations or higher order patterns, can be easily made. We prove the algorithm given is both sound and complete with respect to its specifica­ tion. Second, unlike difference matching, difference uni­ fication can return a large number of matches which we are not interested in; there may be exponentially many ways to annotate two identical terms. Hence, we de­ marcate two restricted classes of useful answers (which we call strongly and weakly minimal). Further, we give a novel search strategy (a meta-interpreter) that finds answers in these classes with minimal search. Third, we give a thorough analysis of the complexity of dif­ ference unification and subproblems. Finally, we pro­ vide examples of how difference unification can be used. In doing so, we present a new paradigm for theorem proving/problem solving whereby proof proceeds by al­ ternating between annotating differences and reducing them. This combination is different from previous work combining rippling and difference matching since here successful rippling does not guarantee successful rewrit­ ing of one term with another; rather, it must be seen as one step, in possibly many, of difference reduction. This, along with differences from traditional rewrite based the­ orem proving, is developed in the next section.

2 Applications

2.1 Normalization

We begin with a simple example that both introduces notation and illustrates how difference unification can be used to apply rippling in a new way: as an itera­ tive difference reduction technique. In rippling's original role in inductive theorem proving, successfully rippling the goal always allows use of the induction hypothesis. More particularly, in an inductive proof the induction conclusion is an image of the induction hypotheses ex­ cept for the appearance of certain function symbols ap­ plied to the induction variable in the conclusion. The rest of the induction conclusion, which is an exact im­ age of the induction hypothesis, is called the skeleton. The function symbols that must be moved are the wave­ fronts. For example, if we wish to prove p(x) for all natural numbers, we assume p( n) and attempt to show p( s( n)) . The hypothesis and the conclusion are identical except for the successor function s(.) applied to the in­ duction variable n. We mark this wave-front by placing a box around it and underlining the subterm contained in the skeleton, PQ s(!!) 1). Rippling then applies just those rewrite rules, called wave-rules, which move the difference out of the way leaving behind the skeleton. In their simplest form, wave-rules are rewrite rules of the form aq !3(1.) I) => I p(~) I· By design, the skeleton a(!) remains unaltered by their application. If rippling succeeds then the conclusion p~ s(!!) p is rewritten us­ ing wave-rules into some function of p(n); that is, into !(~) (!may be the identity). At this point we can ca upon the induction hypothesis.

An analogous situation occurs in difference matching. If we can match two terms, annotating one with wave­ fronts, then successful rippling allows rewriting one to the other. However, this fails with difference unification as both terms are annotated. For example, consider the associative (infix) function symbol+. The following are wave-rules( capital letters represent variables and lower case letters constants and bound variables).

As previously noted, rippling terminates because wave­ fronts in the rewrite rules must match those in the rewrit­ ten term and these are only moved in some well-founded direction. We may therefore rewrite with the associativ­ ity of + in both directions. Consider proving

If we difference unify the left hand side of this equa­ tion with the right, there are 10 annotated answers cor­ responding to the 6 ways of selecting any 2 constants from the 2 terms and 4 ways of selecting any one. In general, we prefer only those with minimal amounts of annotation. Furthermore, as wave-rules only exist to rip­ ple these minimal annotations, rippling would not find proofs for the others. Picking minimal annotations (for­ mally defined in §3) narrows the choice to 2:

Both of these will lead to proofs by rippling (the first giving a left associative normal form, the second giving a right) . In what follows we concentrate on the first. The left hand side of this equation is completely rippled-out: no more wave-rules need (or can) be applied since the wave-fronts are already outermost. The right hand side ripples with (2) yielding

and now both terms are rippled-out . Though rippling is done, we have not succeeded in proving the terms equal since the wave-fronts themselves differ.

One might conclude that rippling has not accom­ plished anything but that would be false . It has reduced the "inner difference" between these terms: each now contain a copy of the previous skeleton a+ b intact . Dif­ ference unifying ( (a + b) + c) + d against (a + b) + ( c + d) reveals this. There are 12 annotations in total, but only 3 are minimal, and only one of these can be rippled:

We have made progress since these terms have a larger skeleton. As before the left hand side is rippled-out; rip­ pling on the right with (2) yields the left hand side, so we are done. This example illustrates a general phe­ nomenon: iterating difference unification and rippling successively decreases the difference between two terms.

This combination can be very effective. In associa­ tive reasoning each iteration of difference unification and rippling increases the skeleton and hence terminates suc­ cessfully. Of course, exhaustive application of one of the associativity rules would also suffice, but there are ad­ vantages in using difference unification and rippling. To begin with, one needn't completely normalize terms, rip­ pling proceeds only as far as is required to reduce the difference. Moreover, as both left and right associativity may be used, fewer rewrite steps may be required. More significantly, there are theories where we need both and where normalization would therefore loop. The combi­ nation of difference unification and rippling is often an effective heuristic in theories where rewrite based proce­ dures do not exist; the next example, aside from being more general, illustrate this.

2.2 Series

Difference unification and rippling have proved also very useful in summing series. Consider, for example, the problem of finding a closed form sum for

using the standard result (such results are computed au­ tomatically in [WNB92])

We encode the problem of finding a closed form sum as the task of proving a theorem of the form,

where the existential witness S is restricted to be in closed form. To prove this theorem, we first eliminate the existential quantifier. The standard'form method [WNB92] then difference unifies the dequantified goal with (5) giving the minimal annotations

To ripple these differences away we use the wave-rules:

where C and D are constant with respect to j. Note that {6) could not be used in a procedure based on ex­ haustive rewriting since, like associativity when used in both directions, it would loop.

The standard form method first applies wave-rule (6) to the goal dividing its wave-front into two,

then wave-rule {7),

and finally {8), after which rippling no longer applies,

We therefore re-difference unify goal and hypothesis to give, as with the associativity example, a larger skeleton,

Rippling, though unable to move the differences up com­ pletely, has reduced the inner difference. Indeed, the dif­ ference has been so reduced that we can now substitute the standard result into the goal,

The standard form method now difference unifies against the standard result for the sum of the first n integers, and ripples with (7) to complete the proof.

2.3 Other applications

We have explored a number of other applications of dif­ ference unification that, for lack of space, we cannot de­ velop here. For example, in [BW92a; BBH93) we show how difference unification can be used to guide rewriting in so called proof by consistency techniques. Other re­ searchers have also explored applications of these ideas. Hutter has recently reported on applying associative commutative difference unification and rippling to solve SAMs lemma in the INKA system [CH92j.

3 Specification

To specify difference unification we must be more precise about the representation of annotations. As in [BW92] annotations are represented in a normal form in which every wavefront has an immediate subterm deleted (i.e. all wavefronts are one functor thick); this is without loss of generality as "thicker" wavefronts can be represented by nested wavefronts. In addition, rather than superim­ posing a particular representation on terms, annotations will be abstracted out and represented separately; this makes it much easier to specify and describe a differ­ ence unification algorithm (although we will continue to use the "box-and-hole" for aiding visualisation of anno­ tation sets) . Annotations will therefore be represented by the set of positions of the wave-holes; as the wave­ fronts are always one functor thick, the position of the wave-hole uniquely determines the wavefront. Positions are defined recursively as follows: the set of positions in the term t is Pos(t) where Pos(f(s1, ... , sn)) equals {A} U {i.p 11:::; i:::; n 1\ p E Pos(si)}. So A represents the empty sequence and "." concatenation. The sub­ term of a term t at position pis tfp where tf A = t and f(sl , ... , sn)fi.p = sifp. For example, annotations for f(gQ ~(~j b) l),j g(Q.) J> are given by the set {1.1.1, 2.1}. In what o ows we on y work with sets of annotations that are well-formed with respect to given terms. That is ad­ dresses refer only to positions inside the expression tree, and no two addresses differ only in the final address po­ sition (which would correspond to a wave-front with two wave-holes) .

A few remaining auxiliary definitions are needed. By recursion on terms it is simple to define a function skel(t, At) which takes a term t and a set of annotations for that term At, and returns the unannotated part of the term. For example, the skeleton of f(gQ f(S!, b) I), I g(Q.) p is f(g(a), b). We say that q extends p iff q = p.i, or q extends some r and r extends p.

Difference unification is a relation, du(s, t, A., At, u), that satisfies the property

where u is a most general unifier. Note that this is rather different from the much harder homomorphic embedding problem [NS87] where the substitution is applied before deleting function symbols possibly including those intro­ duced by the substitution.

As in the examples, we often demand a minimality condition on the annotations. Annotations are minimal if they are the least amount of annotation necessary to make terms unifiable (just as a most general unifier is the least amount of substitution needed to make the terms identical). There is a choice though concerning whether annotations are minimal with respect to a given sub­ stitution, or with respect to all possible substitutions. This choice has important consequences both for ap­ plications of difference unification, and as we will later demonstrate, for the algorithm's search properties.

Definition 1 (weak minimality) A. and At are weakly minimal annotations of s and t and 0' iff ...,3A~ c A., A~ c At with u( skel( s, A~)) = u( skel( t, Am Definition 2 (strong minimality) A. and At are strongly minim.al annotations of s and t iff ...,3A~, A~ with (A~ c A.,A~ ~At) or (A~ ~A., A~ cAt) and skel(s,A~) unifiable with skel(t,AD

For example,~ f(X) I, /(a)} is weakly minimal with sub­ stitution {!(a)/ X} but not strongly minimal, whilst ~ f(X) 1.1 /(Y) I} is neither weakly minimal nor strongly minimal (the only strongly minimal difference unification is no annotation). A simple consequence of the defini­ tions is that strongly minimal solutions are also weakly minimal and in the ground case (e.g., wave-rule parsing) they coincide. Note that all difference matches (variables and annotations only on one of the two terms) are weakly minimal. As we illustrated in the applications, we can often avoid many useless difference unifiers by restricting our attention just to minimal difference unifiers.

4 Algorithm

As is common practice in the unification community (e.g., [JK91]), we give an algorithm for difference uni­ fication by means of transformation rules and (in the next section) a search strategy for applying these rules. To difference unify s with t, we reduce the quadruple ({s = t /A, A},{},{},{}} to ({}, u, A,, At} where u is a set of substitutions, and A, and At are the annotations of s and t. The notation "/" marks positions of terms within s and t; these record annotation addresses.

The rules for difference unification are given in Fig­ ure 1. The predicates valid, (p) and validt (p) are de­ fined relative to the input terms s and t and are defined asp E Pos(s~ and p E Pos(t) respectively.

These rules need to be applied non-deterministically. For example, in difference unifying f(x, a) with f(g(a), .x) if we apply DECOMPOSE and ELIMINATEL committing to {g(a)fx}, we fail to get a solution. The rules are closely related to rules for matching, differ­ ence matching and unification. Matching is implemented by DELETE, DECOMPOSE, ELIMINATEL; difference matching is implemented by DELETE, DECOMPOSE, ELIMINATEL, HIDEL; and unification is imple­ mented by DELETE, DECOMPOSE, ELIMINATEL, ELIMINATER· Therefore matching and unification are special cases of difference unification. Note that unifi­ cation can also use rules, often called CONFLICT and CHECK, which cause unification to fail immediately when the outermost functions disagree or an occurs check error happens. In difference unification we can­ not use such rules and must fail only when the search space has been exhaustively traversed. The IMITATEL. and IMITATER rules can also be used in unification, although ELIMINATEL and ELIMINATER will always work (more efficiently) in their place without losing the completeness of unification. Difference unification does, however, need IMITATEL and IMITATER for complete­ ness: consider difference unifying X and f(g(a)), re­ turning the substitution {f(a)/X} and the annotations !Q g(S!) p. The DUNIFY rules can be seen as the merg­ ing of the rules for unification and the rules DELETE, DECOMPOSE, HIDEL, and HIDER which add an arbi­ trary annotation; since the rules for recursing through the term structure are common to both these rule sets, their merging is more efficient than a naive "generate annotations" and "unify skeletons" .

DELETE (S U {s =sIp, q}, u,A,,A,) ::} (S, u,A,,A,) DECOMPOSE {S U {/(sl, ... , Sn) = /(h, ... , tn) I p, q}, u, A,, At} ::} {SU {s; = t; I p.i,q.i II~ i ~ n}, u,A,,A,) ELIMINATEL (S u {X= tIp, q}, u, A., A,) '* (S[X ...... t],u o {tiX},A,,A,) if -.occurs(X,t) ELIMINATE& (S u {s =X I p, q}, u,A,,A,) '* (S[X ...... s], u o {siX}, A,, A,) if -.occurs( X, s) IMITATEL (S u {X= /(tt, ... , tn) I p, q}, u, A., At} '* (S[X ...... /(Xt, ... , Xn)] U {X; = t; I p.i, q.i I I ~ i ~ n }, u o {f(Xt, ... , Xn)l X}, A,, A,,) if Vi E [I, n] valid,(q.i} IMITATE& {S U {f(s1, ... , sn) =X I p, q}, u, A,, At}::} {S[X ...... /(Xt, ... ,Xn)] U {s; =X;/ p.i, q.i II ~ i ~ n}, u o {f(Xt, ... , Xn)l X}, A,, A,,) if Vi E [I, n] valid, (p.i) (S U {/(st, ... ,sn) = tl p,q},u,A,,A,) ::} (S U {s; = tl p.i, q}, u,A. U {p.i},At} if valid,(p.i) (S U {s = /(t1, ... ,tn) I p,q}, u,A,,A,) ::} (S U {s = t; I p,q.i}, u,A,,A, U {q.i}) if valid,(q.i)

These rules have been implemented in Prolog. The following table gives 8 out of the 24 results of difference unifying (X+ Y) + Z with X+ (Y + Z). Note that for readability we have merged adjacent wavefronts in the "box and hole" presentation.

The first three annotations are strongly minimal and give the only wave-rules (oriented appropriately). The fourth, fifth and sixth annotations are neither weakly nor strongly minimal. The last two annotations are weakly but not strongly minimal. This once again demonstrates that difference unification is not unitary, even when re­ stricted to strong or weak minimality.

The following is a sample execution trace of the first result . It results from applying the rules: HIDEL, DECOMPOSE, DELETE, HIDE&, and DELETE.

({(X+ Y) + Z =X+ (Y + Z) I A, A},{},{},{}) ({X+ y =X+ (Y + Z) I l.A, A}, {I},{},{}) ({X= X) I 1.1, I, y = y + z I 1.2, 2}, {I},{},{}) ({Y = y + z I 1.2, 2}, {I}, {},{}} ({Y = y I 1.2, 2.I}, {I}, {2.I}, {}) ({},{I}, {2.I},{})

5 Left-first Search

The transformation rules, when exhaustively and non­ deterministically applied, generate all possible difference unifications, not just those that are weakly or strongly minimal. This is both time consuming and almost always unnecessary. We have therefore implemented a search al­ gorithm (i.e., a meta-interpreter) for traversing the space defined by these rules so that we are guaranteed to en­ counter just the weakly or strongly minimal difference unifications. In the strongly minimal case, potent ially an exponential amount of search is saved .

We first describe the structure of the search space. Nodes correspond to the quadruples giving the current state. Arcs to the left result from applying one of the unification rules: DELETE, DECOMPOSE, IMITATEL, IMITATE&, ELIMINATEL, and ELIMINATE&. Arcs to the right result from applying a hiding rule: HIDEL and HIDER. The key to returning minimal difference unifi­ cations is observing that a non-minimal difference uni­ fication uses more applications of the hiding rules than a minimal one, though it may use a greater, lesser or equal number of unification rules. Thus, in searching the tree we want to minimize right arcs since each adds more annotation. We call a search algorithm which does this left-first search. At the n + 1-th ply of the search we explore all those nodes whose path back to the root includes n right arcs. This search strategy returns min­ imal cost solutions where hiding rules (right-rules) have (unit) cost and other rules (left-rules) having no cost . We have implemented a meta-interpreter that performs this search as follows. Given a set of nodes N, left*{N) returns the set of nodes reachable from the nodes in N by taking any number of left arcs. The function right(N) returns the set of nodes reachable from the nodes in N by taking one right arc. Finally solutions(N) returns any answers in the set of nodes N . Figure 2 gives the algorithm and illustrates the order in which nodes in a binary tree are explored under left-first search.

For strongly minimal difference unifications, this algo­ rithm returns the first set of answers and stops. For weakly minimal difference unifications, we must save the answers generated, and continues to search comparing new answers for weak minimality against previous ones. Unfortunately, to return all the weakly minimal differ­ ence unifications we must search the whole tree. The advantage of left-first search is that we can immediately tell whether an answer is weakly minimal.

6 Properties

Let us introduce some notation that will be used to prove properties of difference unification and the DUNIFY rule set. We write (E,u,A,,A1} ~ (E',u',A~,AD to in­ dicate that there is a derivation D (that is, a possi­ bly empty sequence of DUNIFY rule applications) which function left-first(Start);

Nodes := left*({Start}};

loop:

Ans := solutions(Nodes); if Ans ::/; {} then return Ans; Node := left*(right{Nodes}}; goto loop;

transforms {E,u,A,,At} into {E',u',A~,AD.

We now sketch proofs of soundness and completeness; that is, proofs that the rules return all and only the difference unifiers. Full proofs are given in [BW92a].

Theorem 1 (Soundness)

If {s=tiA,A},{},{},{}) ::fb {{},u,A,,At} then du(s , t, A,, At, u).

Proof (sketch): We first establish a lemma: D' Du If (s=tiA,A,{},{},{}) ::::::::} (E,u,A,,At} => ({},u',A~,A~} then for all s' = t' lp,q E E,

where strip is a function that "adjusts" an annota­ tion set by deleting prefixes from addresses. That is, strip( A, A)= A and strip(A,p) = {q I p.q E A} . Sound­ ness follows from the lemma provided the unifier u is a most general unifier. This holds since we can construct a derivation which unifies skel(s, A,) and skel(t, At) by deleting every hide rule from D and applying the remain­ ing unification rules. This builds the same unifier u and, as the underlying unification algorithm returns mgus, it follows that u is a mgu.

The lemma follows by induction on the length of D". The base case is trivial. In the step case, unification rules are easily seen to preserve sound solutions. The HIDEL rule replaces an equation like f(sl, ... sn) =tIp, q by s; = t I p.i, q and adds p.i to A,. By definition, skel(f(sl,····sn),strip(A~,p)) = s;, and by hypothe­ sis, u'(skel(s;, strip(A~,p.i))) = u'(skel(t, strip(A~, q))). Conclude that u'(skel(f(s1, .. . ,sn),strip(A~,p))) u'(skel(t, strip(A~, q))) and the theorem follows. HIDEa is analogous. 0

Theorem 2 (Completeness) If du( s, t, A,, At, u) D then ({s = t I A, A},{},{},{})=>({}, u, A,, At)·

Proof (sketch): It suffices to consider the DUNIFY rules with DELETE restricted to delete only equations between atoms and ELIMINATEL and ELIMINATEa re­ stricted to cases when the non-variable term is atomic. These restricted rules are complete for unification and so (without the hiding rules) return u as a mgu for skel(s, A,) and skel(t, At)· The theorem follows by show­ ing that the unification rules applied in computing this unifier can be applied (in the same order) to compute the same unifier for s and t while being interleaved with hiding rules which hide the addresses in A, and At. This in turn follows from our restrictions on the deletion and elimination rule; they guarantee that every term posi­ tion in Pos(s) and Pos(t) eventually appears in some equation in the derivation D. Since elements of A, are a subset of Pos(s) corresponding to addresses of function arguments in s, and likewise for At, appropriate hiding rule can always be applied. 0

The soundness and completeness arguments only rely on the underlying unification algorithm being sound, complete, and "decompositional" in the sense that ev­ ery position in the original terms eventually appears in the course of the derivation. Hence, if we replace the un­ derlying unification algorithm with something stronger, e.g., incorporating equations that preserve these proper­ ties for some, equational theory, then again we will have a sound and complete algorithm with respect to that the­ ory. We suspect that there are many natural applications of equational difference unification, e.g., the previously mentioned work of Hutter.

Theorem 3 (Termination) The DUNIFY rule set al­ ways terminates.

Proof (sketch): Given input s and t, use a lex­ icographic ordering on the triple (I, V, F) were I is IPos(s)l + IPos(t)l - I', I' is the number of imitation steps performed in a sequence of rule applications, V is the number of distinct variables in the (current) equation set, and F is the number of function symbols (including constants) in the (current) equation set. 0

7 Complexity

DUNIFY has been given as a set of rules. If they are ap­ plied non-deterministically, it is easy to see that it can take exponential time to find a solution to a problem as we may, using the hide and imitate rules, consider all the ways of hiding function symbols. 1 A term of size n (n function symbols) has O(n) interior (neither con­ stants or variables) function symbols that can be hidden in 0(2n) different ways; hence, naive execution can be exponential. It is natural to ask whether this the best that we can do, and which are the tractible cases. In asking such questions we must distinguish between the problem of generating all solutions and that of generat­ ing a solution or knowing if one exists. The first problem is easily seen to require exponential size even in the very restricted of case of ground difference matching.

1 Also note that unification algorithms which explicitly represent substitutions are not efficient. This can, how­ ever, be avoided by using a. rule-based approach such as [JK91] at the cost of rules with rather more complicated side­ conditions.

Theorem 4 There are difference matching problems re­ quiring exponential time.

Proof: Consider difference matching {s, t} where s = r(a) and t = P"(a) (fm(a) is the m-fold application off to a) . The solutions correspond to choosing n out of 2n occurrence of f in t to hide. That is there are (2n!)/((n!) 2 ) which is 0(2"). Note that all of these are strongly minimal. 0

Problems generating exponential numbers of solutions are exceptional as they involve unusual amounts of re­ peated structure. In general, there are far fewer matches and unifiers; so it is interesting to investigate the com­ plexity of returning a single solution, or determining if one exists. The first problem is polynomial time solvable for ground terms.

Theorem 5 Given terms s and t we can determine if s difference matches t (s may be annotated with skeleton t) or s difference unifies with t in polynomial time.

Proof (sketch): In [NS87] an algorithm based on dy­ namic programming is given for solving the homomor­ phic embedding problem of one ground term into another in polynomial time. This problem is the same problem as ground difference matching. It is easy to modify this idea to provide an algorithm for ground difference uni­ fication. Furthermore, these algorithms can be easily modified to return sets of answers as well as indicating if answers exist [BW92a] . 0 .

As a side note, observe that while the above ground difference unification algorithm can be easily modified to yield minimal answers, there is a trivial linear time al­ gorithm for determining difference unifiability although it does not give minimal answers. That is" s and t will difference unify iff they share at least one constant (of arity 0) . In the non-ground case, s and t are difference unifiable iff they share one constant or if either contains a variable. In this respect, difference unification is, per­ haps surprisingly, easier than difference matching.

In general, difference unification and all its subprob­ lems are trivially in NP since we can guess annotations and then unify or match resulting skeletons in polyno­ mial time. In the nonground case, when variables are added determining the existence of a solution is NP hard.

Theorem 6 Difference unifying s and t, with annota­ tion on only one side is NP hard.

The proof is given in [BW92a] and uses a reduction from 3SAT similar to that used in the proof of the NP hard­ ness of set-matching given in [KN86].

8 Conclusions

In [Rob89], J .A. Robinson presented a simple account of unification in terms of difference reduction. He observed:

"Unifiers remove differences ... We repeatedly re­ duce the difference between the two given expressions by applying to them an arbitrary reduction of the dif­ ference and accumulate the product of these reductions.

This process eventually halts when the difference is no longer negotiable [via an assignment}, at which point the outcome depends on whether the difference is empty or nonempty."

In this light, our research can be seen as a direct ex­ tension of Robinson's notion of difference reduction: we reduce differences not just by variable assignment, but also by term structure annotation. What makes our ex­ tended notion of unification tenable, indeed attractive, is that this annotation is precisely what is required for rippling to remove this difference.