# 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

θ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 ◊