Unification

Unification is an algorithm for instantiating, or giving values to, variables in such as way as to make two given terms be equal. The given terms are the inputs to the algorithm, and the output (if the algorithm succeeds) is a substitution, or assignment of terms to (finitely many) variables. We will first consider a few examples, and then give the algorithm in general. Incidentally, the subject of this page is first-order unification. The first-order part distinguishes this basic algorithm from generalizations such as lambda unification.

Example 1. Suppose we want f(x) = f(g(y)). Then we "unify f(x) and f(g(y))", which means we call the unification algorithm with those two terms as inputs, and we get as output the substitution that assigns x the value g(y). We write that substitution as [x:g(y)].

When we want to mention "some substitution" as opposed to a specific substitution, we usually use a lower-case Greek letter, often σ or τ. To apply a substitution σ to a term t, we write tσ. Thus if t is f(x) and σ is [x:g(y)], then tσ is f(g(y)). You might think that this should be written σ(t) instead, but tσ is traditional. Then composition of substitutions can be written without parentheses, as in tστ, which is the result of first applying σ and then τ to the term t. With this notation, we can state the purpose of the unification algorithm: Given two terms t and s, the algorithm should find and return a substitution σ such that tσ = sσ, if such a σ exists. Otherwise it should fail. (In practice, failing would be indicated by returning some special value that could not possibly be a substitution.) A substitution σ such that tσ = sσ is called a unifier of t and s.

Example 2. Suppose we want f(x,g(3)) = f(g(y),x). To unify these two terms, we first unify x with g(y). That results in [x: g(y)]. Then, we apply that substitution to the second arguments before unifying them. So we have to unify g(3) and g(y), not g(3) and x. These terms unify with result [y:3] We compose that substitution with the one we got from unifying the first arguments, so the final answer is [ x: g(y), y:3] .

Example 3. Suppose we want x = f(x). The algorithm must fail, since it is impossible for any term t to satisfy t = f(t). (To prove this, observe that if d is the depth of t, i.e. its height as a tree, then d would equal d+1.) Similarly, unification must fail whenever it attempts to unify a variable x with a term that contains x (and is not just x itself). This part of the algorithm is called the occurs check. It is the most expensive (in terms of time) part of the algorithm!

Example 4. Suppose we want x = t for a term t that does not contain x. Then the algorithm returns [x = t].

Example 5. Suppose we want 2 + 2 = 4. Unification fails. Two constant terms unify only if they are identical. Unification does not "know" anything about arithmetic. As far as unification is concerned, 2 and 4 are just arbitrary symbols like b and c.

Example 6. Suppose we want f(x,y) = f(y,x). Then first we unify x and y, getting [x:y], and then, applying that substitution to the second arguments, there is nothing further to do, so that is the answer.

Example 7. Suppose we want x + y = y + x. Again, unification knows no special properties of +, so this example is just example 6 in disguise, and the answer is [x:y].

Let us reconsider example 1. Observe that in addition to the given unifier [x:g(y)], there are many others, for example [x:g(3), y:3] and [x:g(c), y:c] for any constant c. This leads us to the following concept:

A substitution σ is more general than substitution τ if for some substitution η we have τ = σ η. That is, τ works by first doing σ and then making further substitutions. A most general unifier of two terms t and s is a substitution σ which is more general than any unifier of t and s. (Note that any substitution is more general than itself, by taking η to be the identity or "empty" substitution.) Now finally we can state the purpose of the unification algorithm: given two terms t and s, it returns a most general unifier of t and s, if t and s have any unifier at all, or fail if t and s cannot be unified.

It is not quite obvious that this is possible--if such an algorithm can be found, it implies that if t and s unify at all, then they have a most general unifier. This was proved by J. Robinson, who first gave the unification algorithm.

Here is the algorithm:

unify(t,s) {
if t is a variable x then
   if s contains x return fail;
   else return [x:s];

if s is a variable x then
   if t contains x return fail;
   else return [x:t];

if either t or s is a constant then return [] if they are identical and fail if not;

if t and s do not have the same main symbol f and the same number of arguments then return fail;
σ = []; // the empty substitution
n = number of arguments of t;
for(i=1, i ≤ n; i++)
  { τ = unify(arg(i,t)σ, arg(i,s)σ);
    σ = στ
  }
}

Note how the substitution is built up as we go through the arguments of t from left to right, continually applying the substitution we have found so far. It is a very good exercise to implement the unification algorithm in your favorite computer language. You will first have to define appropriate data structures for term and substitution. It is very easy to implement this algorithm in a classical AI language such as LISP, SCHEME, or Prolog. But it isn't so hard in C, C++ or Java either. What is more difficult is to implement it efficiently, so that not a lot of space and is wasted constructing terms by applying substitutions that end up not working. That, however, is another subject--this page is only intended to explain the algorithm, not to discuss its efficient implementation.