Unification is a procedure to establish whether two terms , that eventually contain uninstantiated variables , can be made identical by eventually substituting appropriate (other) terms for some of these uninstantiated variables, and, if they can, to find these appropriate substitutes.

Examples:

· Terms f(g(X),Y,Z) and f(g(Y),a,f(Y)) unify successfully. The substitute for both X and Y is a , and that for Z is f(a) .

· Terms f(a,X) and f(X,b) will not unify.

· Terms f(Egg,Hen) and f(egg(Hen),hen(Egg)) will not unify.

Sometimes unification is called matching . Strictly speaking, matching differs from unification in that one of the terms is more pattern-like, i.e. variables to be substituted are expected to occur there. The other term, thatmatches the pattern or not , is expected to contain the substitutes.

In a goal, successful unification causes uninstantiated variables to get instantiated to the substitute terms found by unification.

To avoid misunderstanding of unification , one must keep in mind that:

Þ Variables in terms to be unified may have the same name, yet be distinct. For example, goal(Variable, f)) , Variable uninstantiated, will successfully unify with the head of rule

goal(g, Variable) :- write(Variable).

The call to write will cause f to appear as output.

Þ Unification processes terms as if all the earlier instantiated variables that terms may happen to contain were substituted by the corresponding (other) terms. For example, the last goal in the question,

?- X = f(Y), Z = g(f(a)), g(X) = Z.

will actually make the interpreter try to unify g(f(Y)) and g(f(a)) .

Þ The variables that occur uninstantiated in terms to be unified, and eventually get instantiated after unification, need not belong to the context of the clause , that launched unification. For example, trying to satisfy goal(f(Y),g(f(a)) by applying the rule

goal(X, Z) :- X = Z, Y = b, write(Y).

will succeed by causing both a to instantiate Y from the goal and b to instantiate Y from the body of the rule.

Þ In Strawberry Prolog occur check is always on. That is, instantiating a variable to a term that contains the variable is impossible. Although instantiating, e.g. X to f(X) , may seem tempting and even sound from a somewhat more abstract viewpoint, Strawberry Prolog sticks to the inductive definition of term, and it is violated by the outcome f(f(f(...))) of this sort of 'successful unification'.