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
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:
- If there is an equation of the form:
then exit with failure (not unifiable).
- f=g where f and g are different
atomic terms, or
- 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
- f(...) = g(...) where f and g are different functors, or
- f(a1, a2, ..., aN) =
g(b1, b2, ..., bM)
where N and M are different.
- If there is an equation of the form X = X, X being a
variable, then remove it.
- If there is an equation of the form c = c, c being a
atomic term, then remove it.
- 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.
- 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,
- If there is an equation of the form X = t where:
then substitute in all other equations every occurrence of the variable X
by the term t.
- X is a variable and t a term in which the
variable does not occur, and
- the variable X occurs in some other equation,
- 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.
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.
- Apply rule 4 to get X = Y, X = g(Y), X = a
- Apply rule 6 to get X = Y, Y = f(Y), Y = a
- Now rule 7 applies to the second equation.
Author: J.P.E. Hodgson
Saint Joseph's University
Philadelphia PA 19131
Last Changed: 20 January 1999