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 ψ.

- Is the head of b the same as the head of a? If so, go to 2, otherwise to 4
- 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.
- Output SUCCEED
- Output FAIL

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

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

- 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.

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 ◊