## Project "Contraintes" Prolog Web Pages: Unification

One of the interesting outcomes of the standardization process was the realization that not everybody agreed on what is meant by unification. The ISO standard therefor provides a (non-deterministic) algorithm, the ``Herbrand Algorithm'' that computes the most general unifier (MGU) of a set of equations.

The standard does not specify how the algorithm is to be implemented. It requires that (at least in the case of unify_with_occurs_check/2 the result shall be as specified by the Herbrand algorithm.

### The Herbrand Algorithm for an MGU

Given a set of equations of the form t1 = t2 apply in any order one of the following non-exclusive steps:

1. If there is an equation of the form:
1. f=g where f and g are different atomic terms, or
2. f=g where f is an atomic term and g is a compound term, or f is a compound term and g is an atomic term, or
3. f(...) = g(...) where f and g are different functors, or
4. f(a1, a2, ..., aN) = g(b1, b2, ..., bM) where N and M are different.
then exit with failure (not unifiable).
2. If there is an equation of the form X = X, X being a variable, then remove it.
3. If there is an equation of the form c = c, c being a atomic term, then remove it.
4. If there is an equation of the form f(a1, a2, ..., aN) = f(b1, b2, ..., bN) then replace it by the set of equations ai = bi.
5. If there is an equation of the form t = X, X being a variable and t a non-variable term, then replace it by the equation X = t,
6. If there is an equation of the form X = t where:
1. X is a variable and t a term in which the variable does not occur, and
2. the variable X occurs in some other equation,
then substitute in all other equations every occurrence of the variable X by the term t.
7. If there is an equation of the form X = t such that X is a variable and t a non-variable term which contains this variable, then exit with failure (not unifiable, positive occurs check.
8. If no other step is applicable, then exit with success (unifiable).

### Example of a positive occurs check

The equation f(X,X,X) = f(Y,g(Y),a) is not unifiable being subject to a positive occurs check. It leads to an attempt to unify Y with g(Y). This is seen as follows.
1. Apply rule 4 to get X = Y, X = g(Y), X = a
2. Apply rule 6 to get X = Y, Y = f(Y), Y = a
3. Now rule 7 applies to the second equation.

Author: J.P.E. Hodgson
Saint Joseph's University