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 ψ.
And here is SUB-UNIFY(c,d:subscripta):
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
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 ◊