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 <<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