Encyclopedia > Unification

  Article Content


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

Succeeds (tautology)
A=B, B=abc
Both A and B are unified with the atom abc
xyz=C, C=D
Unification is symmetric
Unification succeeds
Fails to unify, atoms are different
A is unified with B
Fails, the heads of terms are different
Fails to unify, because terms have different arity
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)
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

... - Wikipedia <<Up     Contents Autocracy Autocracy is a form of government which resides in the absolute power of a single individual. The term ...

This page was created in 28.2 ms