## Encyclopedia > Unification

Article Content

# Unification

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. 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.
2. An atom can be unified only with the same atom.
3. A term is unified with another term, if the heads and arities of the terms are identic and the parameters are unified (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.

### 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(...)))).
A=abc, xyz=X, A=X
Fails to unify; effectively abc=xyz

All Wikipedia text is available under the terms of the GNU Free Documentation License

Search Encyclopedia
 Search over one million articles, find something about almost anything!

Featured Article
 Autocracy ... - Wikipedia <