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 "=".
- 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.
- An atom can be unified only with the same atom.
- 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.
- 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