APPENDIX TO CHAPTER FOUR

Unification

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

Notes

• SUB-UNIFY calls itself, which makes it a recursive function; but the calls will only be finitely nested, given that the whole calculation of UNIFY is finite, for reasons given below
• The atoms a and b, and the substitution θ are treated as 'global variables' (in computer-speak) which are gradually transformed during the course of the calculation of UNIFY
• Only steps 9 and 12 actually alter the value of θ. θ may be thought of as the answer to the question 'How much substitution so far?'. In steps 9 and 12 θ is augmented by the substitutions {s→t}, or {t→s}, respectively
• The effects of the global transformations of a and b in steps 9 and 12 deserve special attention. Indices that have already been processed (during the calculation of UNIFY to date) may well be affected, if they involve the mutable s (or t, respectively). However, these indices have already been rendered identical (unified) by the calculation, and once identical, they cannot be rendered un-identical by any subsequent substitution. Of course, indices that have not yet been processed are also likely to be affected. Indeed, if s (for example) is replaced by some complicated term not involving s, some of the 'not yet processed' indices may be made considerably more complicated than they were before. Thus the work yet to be done by UNIFY increases...
• ... but not, we hope, in an uncontrolled manner! Indeed, each step of type 9 or 12 eliminates a mutable from both a and b and introduces no new mutables. There is only a finite stock of mutables in a and b, therefore there can only be a finite number of such steps. Therefore the calculation must terminate sooner or later; and it cannot terminate without producing an output of one type or another (i.e. failure or success)
• Steps 8 and 11 lead to failure because a mutable s, say, can never be made one with a mixed term involving s. Direct substitution of the mixed term for s is forbidden by the rules governing substitutions in general. (If only because of the conundrum, Are we supposed to replace the s in the mixed term by the mixed term? ... and so on ad infinitum.) No other substitution brings the two terms any nearer to being identical.
• FAIL only arises when two indices are irrevocably different (or when the atom-heads are different). So UNIFY fails only in cases where a and b really are un-unifiable, and must succeed in all other cases.
• If SUB-UNIFY(c,d,θ) is successful, then by the time the calculation has finished, the subscripta will be identical. Therefore, if UNIFY as a whole is successful, then by the time the calculation has finished, the atoms as a whole will be identical. Thus the θ produced by UNIFY is indeed a unifier.

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.

Proof

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

θ₀, θ₁, ... θ_k

where θ₀ = ε, 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 σ₀ = φ then

φ = θ₀ • σ₀.

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

sσ_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 ◊

---