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.
Given two terms S and T, they unify if there exists a substitution s such that Ss =Ts, where Ss (resp.) Ts denotes the result of applying s to S (resp. T). The most general unifer of two terms S and T is a substitution m such that
  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