Now we shall apply the parsing and wellfoundedness properties of term algebras to the unification algorithm of Remark 1.7.7. Our approach is a new one, which begins from an idea in universal algebra, and carries this through directly to a very efficient implementation.
The most general unifier has a universal property, which may be viewed in two ways: it is the equaliser in the category \Clone_{L}^{x} of contexts and substitutions (Example 5.1.3(b)) , and also the coequaliser of free algebras. The connection between these points of view is the fact that the clone Cn^{×}_{L}([x_{1}:\typeX_{1},¼,x_{n}:\typeX_{n}],[y:Y]) is the free algebra on n generators (Theorem 4.6.7).
The most general unifier is not the coequaliser amongst all algebras.
EXAMPLE 6.5.1 Consider a unary operation s and two variables x and y. Then as a unification problem the equation s(x) = s(y) implies x = y, but the coequaliser as an algebra is essentially ``N with two zeros.'' []
Recall that the products in Cn^{×}_{L} must be preserved in any interpretation of the theory L in a category. The equalisers are not preserved because terms may have equal value without being provably so in the theory.
We shall discuss coequalisers amongst arbitrary algebras in Section 7.4, and characterise the subcategory of free algebras in Proposition 7.5.3(a). Section 8.2 constructs a version of the classifying category which does have some equalisers (and so whose interpretations preserve them).
For our work in this section we need first to restore the generators which we discarded in Definition 6.1.1. The recursion scheme for them is the universal property. The generators do not behave as extra constants as we said in Definition 6.1.1, because the homomorphism which solves the problem may send them to arbitrary terms in the target algebra Q.
NOTATION 6.5.2 Write h_{G}:G® FG for the inclusion of the generators G into the free algebra which they generate.
omitted diagram environment
Then any function f:G® Q to another algebra extends uniquely to a homomorphism p:FG® Q with h_{G};p = f. []
Unification For any homomorphism f:A® Q of algebras, the kernel pair {(a,b)f(a) = f(b)} is an equivalence relation on A and is closed under its operationsymbols (Proposition 5.6.4). In a unification problem the kernel pair is also closed under parse :
LEMMA 6.5.3 Let f:A® Q be a homomorphism from any algebra to an equationally free one (so even if A is free, f may send generators to expressions).
If f(\opr_{A}([(u)\vec])) = f(\ops_{A}([(v)\vec])) then r = s and "j:ar[r].f(\termu_{j}) = f(\termv_{j}).
omitted diagram environment
PROOF: Since f is a homomorphism,

So two expressions are unifiable iff their outermost operationsymbols agree and the corresponding pairs of subexpressions are each unifiable, but all by the same assignment to the generators. For unification to be possible, we must therefore be able to distinguish the generators and operationsymbols from one another, cf Example 6.2.5.
REMARK 6.5.4 Besides parse, the congruence is also closed under the operations r Î W and the axioms for an equivalence relation.



It turns out that the other cases can be avoided:
LEMMA 6.5.5 Let p:FG® Q be a homomorphism from a free algebra to any algebra. Then ( cf Lemma 1.3.8)

PROOF: By structural induction on v, considering x, y, z and r([(w)\vec]). []
REMARK 6.5.6 The previous Remark makes useful optimisations, as they avoid the need to compare or copy terms, providing a parallel, in situ algorithm which unifies terms almost as fast as they can be read. The terms may be represented in Polish notation (Example 6.2.7), but it is more usual to code each instance of an operation as a record consisting of the operationsymbol together with pointers to records for each immediate subexpression (Remark 1.1.1). The pending equations are then held as pairs of pointers to these records. The program needs to store the equivalence relation E on generators, together with the equations R between generators and (pointers to) subterms.
The given and subsequently generated equations [(u)\vec] = [(v)\vec] do not need to be stored, since each may be dealt with as a subprocess:
LEMMA 6.5.7 The unification algorithm (applied to any finite set of equations between terms for a finitary free theory) terminates.
PROOF: Consider the total number of generators and operationsymbols in the outstanding equations, including the terms assigned by R to the generators. The generators listed in E and R are not counted. The operationsymbol r in case (b), or the generators x and y in cases (c) and (d), are deducted from this count at each step, so the program terminates by Proposition 2.6.2. (In fact only the outermost operationsymbol of u in case (c) is considered more than once, cf Remark 6.5.4(a).) []
THEOREM 6.5.8 The algorithm provides the most general unifier.
PROOF: The unification step continues to be applicable as long as there remains any equation relating a term to a term, possibly via generators. So when the iteration terminates, the outstanding equations consist of an equivalence relation E: G\leftharpoondown \rightharpoonup G together with a system of equations R:G\leftharpoondown \rightharpoonup FG such that, for x,y Î G and u,v Î FG,

omitted diagram environment
We want to partition the set G = D+I into dependent and independent generators, the former being the support of R.
Define x < y on G if x\not º yÙx Î FV(v)ÙyR = v. If there is any unifier p:FG® Q then x < yÞ p(x)\prec\prec p(y), by structural induction on v, where \prec \prec is the transitive closure of the subexpression relation in Q. Since \prec \prec is well founded (Theorems 6.3.13 and 3.8.11(b)) , < must be too (Proposition 2.6.2). In particular the relation < must have no cycles, which, by substitution, would lead to the situation x = u(x).
Since G is finite and < is decidable, to verify wellfoundedness it is enough to make the occurs check, for such loops (Exercise 2.36).
By < recursion, dependent variables may now be eliminated from R using Lemma 6.5.5. Then we have one equation for each generator, which expresses it as a term in F I, the independent variables standing for themselves, so the lefthand triangle commutes:
omitted diagram environment
With a little diagramchasing we see that FI is the required coequaliser.
Each step of the execution has replaced one unification problem by another which is equivalent to it, the last being an assignment of terms to independent variables, which has a coequaliser. Since the latter is unique up to unique isomorphism, the algorithm is confluent, despite being slightly non deterministic. []