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, X2 and Y3 can be unified to Z6 by taking X = Z3 and Y = Z2.
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 "=".
; 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=xyzUnification in Prolog
Due to its declarative nature, the order in a sequence of unifications doesn't play (usually) any role.Examples of unification