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 t₁ = t₂ 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(a₁, a₂, ..., a_N) = g(b₁, b₂, ..., b_M) 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(a₁, a₂, ..., a_N) = f(b₁, b₂, ..., b_N) then replace it by the set of equations a_i = b_i.
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

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.