Another Introduction to Unification

Arthur Nunes-Harwitt

1 Introduction

Robinson introduced the unification algorithm in his work on resolution theorem proving in mathematical logic. This logic is the foundation for more recent developments such as logic programming and type inference. I'd like to develop the unification algorithm in this paper. But first, what is unification?

2 Unification by Example

Unification has to do with showing that two expressions are in some sense the same. Here's a simple example.

i) x + 1

ii) x + 1

Expressions (i) and (ii) are the same, so we say that they unify. Consider another somewhat more interesting example.

iii) x + 1

iv) x + y

In this case expressions (iii) and (iv) are not identical; however, since y is a variable, if we make the assumption that y = 1, then the expressions become identical. The equation y = 1 is called a `unifier', since it allows us to unify expressions (iii) and (iv). Finally, consider one more example.

v) x + z

vi) x + y

Again, the expressions (v) and (vi) are not identical. We could arbitrarily pick the following unifiers: z = 6, y = 6. Then expressions (v) and (vi) would unify. However, this arbitrariness is troubling. We'd really like the `most general unifier'. The most general unifier is the equation y = z. This unifier allows us to unify expressions (v) and (vi) with out making any arbitrary assumptions.

The job of the unification algorithm is to determine whether two expressions are the same given that some assumptions can be made. The algorithm reports whether the expressions can be made to look identical, and it also reports what assumptions were required (i.e. the unifiers) if it is possible.

3 Developing the Unification Algorithm

Now we know what the unification algorithm should do, but it's not at all clear how to implement it. Let's work out the various cases and then try to combine them.

3.1 Unifying Constant Expressions

Now, we must figure out how to determine whether two compound expressions unify. Compound expressions are represented as lists, and lists can be taken apart by looking at the first element, and looking at everything but the first element, which I'll refer to as the `rest' for short. Thus we can say that two compound expressions, represented as a lists, unify, if the first elements of the lists unify, and rests of the lists unify.

Thus, in Scheme, we might write the following code for unifying lists.

(and (unify-const (car exp1) (car exp2)) 
     (unify-const (cdr exp1) (cdr exp2)))

Putting these two parts together, we get the following Scheme procedure.

(define (unify-const exp1 exp2)
   (or (eqv? exp1 exp2)
       (and (pair? exp1) 
            (pair? exp2) 
            (unify-const (car exp1) (car exp2)) 
            (unify-const (cdr exp1) (cdr exp2)))))

Thus we get the follow interaction.

And that was what was desired.

3.2 Unifying Variable Expressions

When thinking about unifying variables, let's start out with simple cases, and then fix them when we consider the more complicated cases.

The first case I want to consider is when the first expression is a variable, the second is a constant, and there is already a (constant) unifier associated with that variable. For example, we want to try to unify x and 1 given that, say, x = 1; or we want to try to unify x and 1 given that, say, x = 2. One way to do this is to look up what the variable is equal to, and then compare that constant to the second expression. Let's call a set of unifiers an environment, and let's call looking up what a variable is equal to, evaluating the variable with respect to some environment.

It is possible to represent a unifier in LISP as a pair in which the first element is the variable, and the second is the value. Then environments could be represented as a list of unifier representations. The following Scheme code implements the unifier and environment abstract data types.

(define (make-unifier var value) (cons var value))
(define (add-unifier unifier env) (cons unifier env))
(define initial-environment '())
(define (eval-exp var env) ; buggy version
   (cdr (assq var env)))

Now we can implement the first simple case in Scheme...

(define (unify-var1 var value env) ; buggy version
   (let ((var-value (eval-exp var env)))
     (unify-const var-value value)))

Thus we get the follow interaction.

And that was what was desired.

(define (eval-exp var env) ; still incomplete
   (let ((binding (assq var env)))
     (if binding (cdr binding) var)))

(define (variable? sym)
   (and (symbol? sym) 
        (char=? #\? (string-ref (symbol->string sym) 0))))

If the variable is not in the environment, the unification is trivially true, since we are free to assume that the variable is equal to that value. Yet, we'd like to return more information than that, since we are now assuming that the variable is equal that value. Let's change the return value convention that we've been using. Up until now, we've been returning true if the unification succeeded and false if it failed. Instead, let's return the environment — our set of assumptions — if unification succeeds and false if it fails. We can then implement this case in Scheme as follows...

(define (unify-var2 var value env) ; still incomplete version
   (let ((var-value (eval-exp var env)))
     (if (variable? var-value)
         (add-unifier (make-unifier var-value value) env)
         (if (unify-const var-value value)
             env
             #f))))

Thus we get the follow interaction.

And that was what was desired.

(define (eval-exp exp env) 
   (if (variable? exp)
       (let ((binding (assq exp env)))
         (if binding (eval-exp (cdr binding) env) exp))
       exp))

(define (unify-var3 exp1 exp2 env) ; still incomplete version
   (let ((var-value1 (eval-exp exp1 env))
         (var-value2 (eval-exp exp2 env)))
     (cond ((variable? var-value1)
            (add-unifier (make-unifier var-value1 var-value2) env))
           ((variable? var-value2)
            (add-unifier (make-unifier var-value2 var-value1) env))
           ((unify-const var-value1 var-value2) env)
           (else #f))))

And so now we can do the following...

Just what we wanted!

3.3 Unifying General Expressions

We've done constant expressions and we've done variable expression; now our job is to put them together. The following is a first attempt.

(define (unify exp1 exp2 env) ; buggy
   (let ((var-value1 (eval-exp exp1 env))
         (var-value2 (eval-exp exp2 env)))
     (cond ((eqv? var-value1 var-value2) env)
           ((variable? var-value1)
            (add-unifier (make-unifier var-value1 var-value2) env))
           ((variable? var-value2)
            (add-unifier (make-unifier var-value2 var-value1) env))
           ((and (pair? var-value1)
                 (pair? var-value2))
            (and (unify (car var-value1) (car var-value2) env) 
                 (unify (cdr var-value1) (cdr var-value2) env)))
           (else #f))))

(define (unify exp1 exp2 env) ; buggy
    (let ((var-value1 (eval-exp exp1 env))
          (var-value2 (eval-exp exp2 env)))
      (cond ((eqv? var-value1 var-value2) env)
            ((variable? var-value1)
             (add-unifier (make-unifier var-value1 var-value2) env))
            ((variable? var-value2)
             (add-unifier (make-unifier var-value2 var-value1) env))
            ((and (pair? var-value1)
                  (pair? var-value2))
             (unify (cdr var-value1)
                    (cdr var-value2)
                    (unify (car var-value1) 
                           (car var-value2) env)))
            (else #f))))

(define failure? not)

(define (unify exp1 exp2 env)
   (if (failure? env)
       #f
       (let ((var-value1 (eval-exp exp1 env))
             (var-value2 (eval-exp exp2 env)))
         (cond ((eqv? var-value1 var-value2) env)
               ((variable? var-value1)
                (add-unifier (make-unifier var-value1 
                                           var-value2) env))
               ((variable? var-value2)
                (add-unifier (make-unifier var-value2 
                                           var-value1) env))
               ((and (pair? var-value1)
                     (pair? var-value2))
                (unify (cdr var-value1)
                       (cdr var-value2)
                       (unify (car var-value1) 
                              (car var-value2) env)))
               (else #f)))))

Let's try it out...

And that's just what we wanted!

Finally, there is one more possibility that we need to consider. Can we unify x and f(x)? It may be possible in some cases, but to be on the safe side let's agree that a variable can't unify with an expression that contains the variable. A variable x occurs within an expression e, if e is a variable that evaluates to x, or e is a compound structure and one of the components of e evaluates to x. Thus, when unifying, we want to make sure, before binding a variable to an expression, that the variable does not occur within the expression.

(define (occurs-within? var exp env)
   (cond ((eq? var (eval-exp exp env)) #t)
         ((pair? exp)
          (or (occurs-within? var (car exp) env)
              (occurs-within? var (cdr exp) env)))
         (else #f)))

(define (unify exp1 exp2 env)
   (if (failure? env)
       #f
       (let ((var-value1 (eval-exp exp1 env))
             (var-value2 (eval-exp exp2 env)))
          (cond ((eqv? var-value1 var-value2) env)
                ((variable? var-value1)
                 (if (occurs-within? var-value1 var-value2 env)
                     #f
                     (add-unifier (make-unifier var-value1 
                                                var-value2) 
                                  env)))
                ((variable? var-value2)
                 (if (occurs-within? var-value2 var-value1 env)
                     #f
                     (add-unifier (make-unifier var-value2 
                                                var-value1) 
                                  env)))
                ((and (pair? var-value1)
                      (pair? var-value2))
                 (unify (cdr var-value1)
                        (cdr var-value2)
                        (unify (car var-value1) 
                               (car var-value2) env)))
                (else #f)))))

With this addition, we have the following.

However, in many implementations of unification, the occurs check is not performed because it makes unification less efficient.

4 Efficient Unification

One big performance loss for the unification algorithm is variable look-up. The environment is searched linearly for a variable. One way one might improve the efficiency of the unification algorithm is to design a more efficient data structure for the environment abstract data type. I am not going to take that approach. (You might want to experiment with that idea, though.) Instead, I am going to completely abandon environments, and use a somewhat different representation.

4.1 Eliminating the Environment

If there is no environment, how will we keep track of unifiers? The new idea is to let the variable keep track of its unifier. Thus we now need a more complicated representation for variables. A variable will now be a cell that contains the unifier value. This cell will initially contain a special `unbound' value. I will represent this cell in Scheme as a Scheme vector. The unbound value will be a somewhat arbitrary but unique value.

(define *unbound* '(unbound))

(define ?; make variable
   (let ((memo '()))
     (lambda (name)
        (cond ((memq name memo) => cadr)
              (else
                (let ((new-var (vector '*variable* name *unbound*)))
                  (set! memo (cons name (cons new-var memo)))
                  new-var))))))

(define (variable? var) 
   (and (vector? var) (eq? (vector-ref var 0) '*variable*)))

(define (var->name var) (vector-ref var 1))

(define (var->value var) (vector-ref var 2))

(define (set-var-value! var val) (vector-set! var 2 val) #t)

(define (clear-var! var) (set-var-value! var *unbound*))

(define (unbound? var) (eq? (var->value var) *unbound*))

(define (eval-exp exp) 
   (if (or (not (variable? exp))
           (unbound? exp))
       exp
       (eval-exp (var->value exp))))

(define (unify! exp1 exp2)
   (let ((var-value1 (eval-exp exp1))
         (var-value2 (eval-exp exp2)))
     (cond ((eqv? var-value1 var-value2) #t)
           ((variable? var-value1)
            (set-var-value! var-value1 var-value2))
           ((variable? var-value2)
            (set-var-value! var-value2 var-value1))
           ((and (pair? var-value1)
                 (pair? var-value2))
            (and (unify! (car var-value1) (car var-value2))
                 (unify! (cdr var-value1) (cdr var-value2))))
           (else #f))))

It's short and sweet. Let's try it out.

It seems to work pretty well. However, there is another optimization we can make.

4.1 Path Compression

With our new representation, we don't have to search through the environment for the value of a variable. However, we may still have to do some searching. If the variable gets bound to another variable, and that variable is bound to still another one, we may have to go down a long chain to find the actual value. If we use the value of that first variable several times, we'll have to search down that chain several times; that seems inefficient! In the procedure eval-exp, we move down the chain. Why not augment this procedure so that the value is propagated back up the chain? (This propagation is called `path compression'.)

(define (eval-exp exp)
   (if (or (not (variable? exp))
           (unbound? exp))
       exp
       (let ((val (eval-exp (var->value exp))))
         (set-var-value! exp val)
         val)))

For the small examples it is hard to tell the difference, but it makes unification a lot faster. One example where the difference shows is the following.

Thus we see that now both variables are directly bound to a. One caveat, though; if unification is part of a PROLOG implementation, this simple path compression won't work. The reason is that during backtracking a variable might become bound to a different value. For example, suppose x and y unify!, and along one path we find that y = 1. If we do the path compression, then x = 1, but if along a different path we discover that y = 2, we're stuck with x = 1. (A possible solution to this problem is to use a stack within the cell.)

Finally, let's see what a truly correct version looks like that includes the occurs check.

(define (occurs-within? var exp)
   (cond ((eq? var (eval-exp exp)) #t)
         ((pair? exp)
          (or (occurs-within? var (car exp))
              (occurs-within? var (cdr exp))))
         (else #f)))

(define (unify! exp1 exp2)
   (let ((var-value1 (eval-exp exp1))
         (var-value2 (eval-exp exp2)))
     (cond ((eqv? var-value1 var-value2) #t)
           ((variable? var-value1)
            (if (occurs-within? var-value1 var-value2)
                #f
                (set-var-value! var-value1 var-value2)))
           ((variable? var-value2)
            (if (occurs-within? var-value2 var-value1)
                #f
                (set-var-value! var-value2 var-value1)))
           ((and (pair? var-value1)
                 (pair? var-value2))
            (and (unify! (car var-value1) (car var-value2)) 
                 (unify! (cdr var-value1) (cdr var-value2))))
           (else #f))))

The unification algorithm is reasonably straightforward. And it also is quite useful, but perhaps this is a good place to stop.

Annotated Bibliography

Abelson, Harold, and Gerald J. Sussman, with Julie Sussman. (1985) Structure and Interpretation of Computer Programs. MIT Press.

Aho, Alfred V., Ravi Sethi, and Jeffery D. Ullman. (1988) Compilers: Principles, Techniques, and Tools. Addison Wesley.

Field, Anthony J., Peter G. Harrison. Functional Programming. Addison Wesley.

Harvey, Brian. (1986) Computer Science Logo Style Volume2: Projects, Styles, and Techniques. MIT Press.

Maier, David, and David S. Warren. (1988) Computing with Logic. Benjamin/Cummings.

Norvig, Peter. (1992) Paradigms of Artificial Intelligence Programming: Case Studies in Common Lisp. Morgan Kaufmann.

Robinson, J. A. (1965) “A Machine-Oriented Logic Based on the Resolution Principle,” Journal of the ACM 12, no. 1:23-41.

Winston, Patrick H., and Bertold K. P. Horn. (1988) Lisp, 3rd ed. Addison-Wesley.