Unification Algorithm

The Unification Algorithm may be thought of as the implementation of a function UNIFY(a,b) which takes as input two atoms a and b and returns either the word SUCCEED, or the word FAIL. Meanwhile the calculation has the effect of gradually transforming the atoms and at the same time building up a substitution θ. At any stage of the calculation, aθ is the current state of the atom which started off as a, and bθ is the current state of the atom which atarted off as b. If the calculation issues in success, the atoms end up united (i.e. rendered identical) and θ is the substitution which has united them.

The UNIFY function makes use of a second function SUB-UNIFY(c,d), where the 'sub' stands for subscriptum. This takes as input two subscripta (possibly empty) and again returns either SUCCEED or FAIL. We now give instructions for calculating UNIFY(a,b) and SUB-UNIFY(c,d). In the following ε stands for the substitution that does nothing (leaves all mutables as they are); and the combination φ•ψ of substitutions means the substitution that results from first making the replacements specified in φ; then following them up with the replacements specified in ψ.

  1. Is the head of b the same as the head of a? If so, go to 2, otherwise to 4
  2. Set θ = ε and calculate SUB-UNIFY(subscriptum of a, subscriptum of b). If the value returned is SUCCEED, go to 3, if FAIL, go to 4.
  3. Output SUCCEED
  4. Output FAIL

And here is SUB-UNIFY(c,d:subscripta):

  1. Do the subscripta have length greater than zero? If not, go to 15
  2. Set integer i=0
  3. Set i=i+1
  4. If i is greater than the length of the subscripta, go to 15
  5. Let s = the ith index of c, t = the ith index of d; so both s and t are terms, mutable or immutable
  6. Is s mutable? If no go to 10
  7. Is t the same as s? If yes, go to 3
  8. Is t a term involving s? If yes, go to 16
  9. Set θ = θ • {s→t}, let atoms a and b be transformed globally by the substitution {s→t}, and go to 3
  10. Is t mutable? If no go to 13
  11. Is s a term involving t? If yes, go to 16
  12. Set θ = θ • {t→s}, let atoms a and b be transformed by the substitution {t→s}, and go to 3
  13. (s and t are both mixed terms.) Are the heads of s and t the same? If no, go to 16
  14. Calculate SUB-UNIFY(subscriptum of s, subscriptum of t). If the output is SUCCEED, go to 3; if FAIL, go to 16
  15. Output SUCCEED
  16. Output FAIL


Lemma 4.13 The 'most general' property

If UNIFY(a,b) is successful then, at the moment of termination of the algorithm, the substitution θ is a most general unifier (m.g.u.) of a and b.


Suppose that the calculation of UNIFY(a,b) is successful. We have seen how, during the calculation, the 'to date' substitution θ is gradually built up by successive instructions of the form 'follow it by {s→t}' or 'follow it by {t→s}' (see steps 9 and 12 above). So θ evolves through a finite sequence of intermediate forms which we may denote

θ0, θ1, ... θk

where θ0 = ε, and θk is the final value taken by θ. Now suppose that φ is another unifier of a and b (i.e. a substitution which renders a and b identical). Our aim is to show that φ is equivalent to a combination of the form

θk • σk.

Clearly, if we put σ0 = φ then

φ = θ0 • σ0.

Now suppose that for some i less than k we have a σi such that

φ = θi • σi ;

and that

θi+1 = θi • {s→t} .

(The case when θi is followed by {t→s} can of course be treated in an exactly similar way.) We seek to show that there must then exist a σi+1 such that

φ = θi+1 • σi+1 = θi • {s→t} • σi+1 .

For this, it will suffice to show that

σi = {s→t} • σi+1 ;

thus {s→t} can be 'peeled off' from the front of σi, like taking off an onion-layer.

Now, the fact that φ = θi • σi unifies the atoms a and b as a whole implies that the terms s and t, which are taken out of atoms a and b at a stage when they have already been transformed by θi, will be unified by σi. Therefore

i = tσi .

To recapitulate the situation: s is a mutable, t is either a mutable or a term not involving s, and s, t are unified by σi. Suppose we let

u = sσi = tσi ;

u may be a term not involving s and t, or it may be t or it may be s. Let us consider the three possibilities in turn:

a) in this case

σi = { u/s , u/t , */x , */y , ... */z }

where x, y, z are various other mutables, and u and the various *'s are terms not involving s, t ... z. Then

σi = { t/s } • { u/t , */x , */y , ... */z }

and we may set

σi+1 = { u/t , */x , */y , ... */z }.

b) In this case u=t, meaning that σi does nothing to t, but eliminates s in favour of t. Thus

σi = {t/s, */x , */y , ... */z } = {t/s}•{*/x , */y , ... */z }

and we may set

σi+1 = { */x , */y , ... */z }.

(In this case the terms * may involve t.)

c) The case of u=s, so σi does nothing to s, but eliminates t in favour of s, so

σi = {s/t , */x , */y , ... */z }.

This time the terms * may involve s but not t. We have to be a bit crafty. Let the terms † be the same as the terms * but with s replaced by t. Then

σi = {t/s , †/x , †/y , ... †/z }•{s/t}

and we may set

σi+1 = {†/x , †/y , ... †/z }•{s/t}.

This concludes the three cases. In sum, from

φ = θi • σi

we may progress to

φ = θi+1 • σi+1 ;

and thus eventually to

φ = θk • σk ,

and the desired property of θ is proved ◊