Unification

Terms

1. Constants and variables are terms.
2. A compound term consists of a functor characterized by its name and arity, or number of arguments. Each argument is a term. Syntactically a compound term has the form f(t1, ...., tn) where f is the functor's name and t1, ... , tn are its arguments.

1. Sm = Tm
2. If s is a substitution such that Ss=Ts then there is a substitution t such that s = m.t

The following algorithm produces the mgu if it exists.

The Unification Algorithm

Input

Two terms T1 and T2 to be unified

Output

s, the mgu of T1 and T2 or failure

Algorithm

Initialize s to be empty
Initialize the stack to contain the equation T1 = T2
and failure to be false

while stack not empty and failure equals false do

pop X = Y from the stack

    case
           X is a variable that does not occur in Y:
              substitute Y for X in the stack and in t
              add X = Y to t.

          Y is a variable that does not occur in X:
              substitute X for Y in the stack and in t
              add Y = X to t

	X and Y are identical constants or variables:
                 continue
 
           X is f(X1, ..., Xn) and Y is f(Y1, ... , Yn)
                for some functor f and n > 1:
                push Xi=Yi, i =1, ...n, on the stack
          otherwise:
                set failure to true.

if failure equals true , then output failure
else output t.

Note that this algorithm uses an occurs check so that it will not unify X and f(X).

Return to UG AI home page

Last Changed: 14 August 1995