Unification - Definition and Overview

See also: Unification Church

Unification can also refer to the German reunification of East and West Germany.

In mathematical logic, in particular as applied to computer science, a unification of two terms is a join (in the lattice sense) with respect to a specialisation order. That is, we suppose a preorder on a set of terms, for which t* ≤ t means that t* is obtained from t by substituting some term(s) for one or more free variables in t. The unification u of s and t, if it exists, is a term that is a substitution instance of both s and t; and such that any common substitution instance of s and t is also an instance of u.

For example, with polynomials, X² and Y³ can be unified to Z⁶ by taking X = Z³ and Y = Z².

Unification in Prolog

The concept of unification is one of the main ideas behind Prolog. It represents the mechanism of binding the contents of variables and can be viewed as a kind of one-time assignment. In Prolog, this operation is denoted by symbol "=".

1. In traditional Prolog, an uninstantiated variable X (i.e. no previous unification were performed on it) can be unified with an uninstantiated variable (and effectively becomes its alias), an atom or a term. In many modern Prolog dialects and in first-order logic calculi, a variable cannot be unified with a term that contains it (the so called occurs-check).
2. A Prolog-atom can be unified only with the same atom.
3. Similarly, a term can be unified with another term, if the top function symbol and arities of the terms are identical and the parameters can be unified simultaneously (note that this is a recursive behaviour).

Due to its declarative nature, the order in a sequence of unifications doesn't play (usually) any role.

Note that in the terminology of first-order logic, an atom is a basic proposition (and is unified similarly to a Prolog term).

Examples of unification

A = A 

Succeeds (tautology)

A = B, B = abc 

Both A and B are unified with the atom abc

xyz = C, C = D 

Unification is symmetric

abc = abc 

Unification succeeds

abc = xyz 

Fails to unify, atoms are different

f(A) = f(B) 

A is unified with B

f(A) = g(B) 

Fails, the heads of terms are different

f(A) = f(B, C) 

Fails to unify, because terms have different arity

f(g(A)) = f(B) 

Unifies B with the term g(A)

f(g(A), A) = f(B, xyz) 

Unifies A with the atom xyz and B with the term g(xyz)

A = f(A) 

Infinite unification, A is unified with f(f(f(f(...)))). In proper first-order logic and many modern Prolog dialects this is forbidden (and enforced by a so-called occurs-check)

A = abc, xyz = X, A = X 

Fails to unify; effectively abc = xyz