Unifcation is the process of determining whether two expressions can be unified, i.e. made identical by appropriate substitutions for their variables. As we shall see, making this determination is an essential part of top-down evaluation.

A substitution is a finite mapping of variables to terms. In what follows, we write substitutions as sets of replacement rules, like the one shown below. In each rule, the variable to which the arrow is pointing is to be replaced by the term from which the arrow is pointing. In this case, X is to be replaced by a, Y is to be replaced by f(b), and Z is to be replaced by V.

The result of applying a substitution σ to an expression φ is the expression φσ obtained from the original expression by replacing every occurrence of every variable in the domain of the substitution by the term with which it is associated.

A substitution σ is a unifier for an expression φ and an expression ψ if and only if φσ=ψσ, i.e. the result of applying σ to φ is the same as the result of applying σ to ψ. If two expressions have a unifier, they are said to be unifiable.

The expressions p(X,Y) and p(a,V) have a unifier, e.g. {X←a, Y←b, V←b} and are, therefore, unifiable. The results of applying this substitution to the two expressions are shown below.

Note that, although this substitution is a unifier for the two expressions, it is not the only unifier. We do not have to substitute b for Y and V to unify the two expressions. We can equally well substitute c or f(c) or f(W). In fact, we can unify the expressions without changing V at all by simply replacing Y by V.

In considering these alternatives, it should be clear that some substitutions are more general than others. We say that a substitution σ is as general as or more general than a substitution τ if and only if there is another substitution δ such that σδ=τ. For example, the substitution {X←a, Y←V} is more general than {X←a, Y←c, V←b} since there is a substitution {V←c} that, when applied to the former, gives the latter.

In top-down evaluation, we are interested only in unifiers with maximum generality. A most general unifier σ of two expressions has the property that it is general as or more general than any other unifier.

Although it is possible for two expressions to have more than one most general unifier, all of these most general unifiers are structurally the same, i.e. they are unique up to variable renaming. For example, p(X) and p(Y) can be unified by either the substitution {X←Y} or the substitution {Y←X}; and either of these substitutions can be obtained from the other by applying a third substitution. This is not true of the substitutions mentioned earlier.

See below for a version of a Javascript implementation of a procedure for computing a most general unifier of two expressions. The procedure assumes a representation of expressions as sequences of subexpressions. For example, the expression p(X,f(b)) can be thought of as a sequence with three elements, viz. the predicate p, the variable X, and the compound expression f(b).

The procedure also assumes that the two expressions have no variables in common. We can always assure this by renaming the variables in one of the expressions.

We start the procedure with two expressions and a substitution, which is initially the empty substitution. We then recursively process the two expressions, comparing the subexpressions at each point. Along the way, we extend the substitution with variable assignments as described below. If, we fail to unify any pair of subexpression at any point in this process, the procedure as a whole fails. If we finish this recursive comparison of the expressions, the procedure as a whole succeeds, and the accumulated substitution at that point is the most general unifier.

1. If the pattern and the instance are the same, then the procedure succeeds, returning the unmodified substitution as result.


2. If at least one expression is a variable, we proceed as follows. First, we check whether the other expression contains the variable. If the variable occurs within the other expression, we fail. Otherwise, we extend our substitution to include a binding of the variable to the other expression.


3. If either the pattern or the instance is a constant, then the procedure fails.


4. If the pattern and the instance have different lengths, we fail.


5. If one expression is a symbol and the other expression is a different symbol or a compound expression, then the procedure fails.


6. Otherwise, we iterate across the corresponding subexpressions of the two expressions. If we fail to match the subexpressions at any point in this process, the procedure as a whole fails. If we finish this recursive comparison of the espressions, the procedure as a whole succeeds and the accumulated substitution at that point is the resulting unifier.

As an example of this procedure in operation, consider the computation of the most general unifier for the expressions p(X,b) and p(a,Y) with the initial substitution {}. A trace of the execution of the procedure for this case is shown below. We show the beginning of a comparison with a line labelled "Compare" together with the expressions being compared and the input substitution. We show the result of each comparison with a line labelled "Result" (either a substitution where successful or "false" where unsuccessful). The indentation shows the depth of recursion of the procedure.

As another example, consider the process of unifying the expression p(X,X) and the expression p(a,Y). A trace is shown below. The main interest in this example comes in comparing the last argument in the two expressions, viz. X and Y. By the time we reach this point, X is bound to a, so we call the procedure recursively on a and Y, which results in a binding of Y to a.

One noteworthy part of the unification procedure is the test for whether a variable occurs within an expression before the variable is bound to that expression. This test is called an occur check since it is used to check whether or not the variable occurs within the term with which it is being unified. For example, in trying to unify p(X,X) and p(Y,f(Y)), we would not want to bind Y to f(Y), since these expressions can never be made to look alike by substituting and value for Y consistently throughout the expression.