Editing Unification (computer science) (section)

===Examples of syntactic unification of first-order terms===
In the Prolog syntactical convention a symbol starting with an upper case letter is a variable name; a symbol that starts with a lowercase letter is a function symbol; the comma is used as the logical ''and'' operator.
For mathematical notation, ''x,y,z'' are used as variables, ''f,g'' as function symbols, and ''a,b'' as constants.
{| class="wikitable"
|-
! Prolog notation !! Mathematical notation !! Unifying substitution !! Explanation
|-
| <code> a = a </code> || { ''a'' = ''a'' } ||  {}  || Succeeds. ([[Tautology (logic)|tautology]])
|-
| <code> a = b </code> || { ''a'' = ''b'' }  || ⊥ || ''a'' and ''b'' do not match
|-
| <code> X = X </code> || { ''x'' = ''x'' } || {} || Succeeds. ([[Tautology (logic)|tautology]])
|-
| <code> a = X </code> || { ''a'' = ''x'' }  || { ''x'' ↦ ''a'' } || ''x'' is unified with the constant ''a''
|-
| <code> X = Y </code> || { ''x'' = ''y'' }  || { ''x'' ↦ ''y'' } || ''x'' and ''y'' are aliased
|-
| <code> f(a,X) = f(a,b) </code> || { ''f''(''a'',''x'') = ''f''(''a'',''b'') } ||  { ''x'' ↦ ''b'' } || function and constant symbols match, ''x'' is unified with the constant ''b''
|-
| <code> f(a) = g(a) </code> || { ''f''(''a'') = ''g''(''a'') }  || ⊥ || ''f'' and ''g'' do not match
|-
| <code> f(X) = f(Y) </code> || { ''f''(''x'') = ''f''(''y'') } || { ''x'' ↦ ''y'' } || ''x'' and ''y'' are aliased
|-
| <code> f(X) = g(Y) </code> || { ''f''(''x'') = ''g''(''y'') } || ⊥ || ''f'' and ''g'' do not match
|-
| <code> f(X) = f(Y,Z) </code> || { ''f''(''x'') = ''f''(''y'',''z'') } || ⊥ || Fails. The ''f'' function symbols have different arity
|-
| <code> f(g(X)) = f(Y) </code> || { ''f''(''g''(''x'')) = ''f''(''y'') } || { ''y'' ↦ ''g''(''x'') } || Unifies ''y'' with the term {{tmath|g(x)}}
|-
| <code> f(g(X),X) = f(Y,a) </code> || { ''f''(''g''(''x''),''x'') = ''f''(''y'',''a'') } || { ''x'' ↦ ''a'', ''y'' ↦ ''g''(''a'') } || Unifies ''x'' with constant ''a'', and ''y'' with the term {{tmath|g(a)}}
|-
| <code> X = f(X) </code> || { ''x'' = ''f''(''x'') } || should be ⊥ || Returns ⊥ in first-order logic and many modern Prolog dialects (enforced by the ''[[occurs check]]'').
Succeeds in traditional Prolog and in Prolog II, unifying ''x'' with infinite term <code>x=f(f(f(f(...))))</code>.
|-
| <code> X = Y, Y = a </code> || { ''x'' = ''y'', ''y'' = ''a'' } || { ''x'' ↦ ''a'', ''y'' ↦ ''a'' } || Both ''x'' and ''y'' are unified with the constant ''a''
|-
| <code> a = Y, X = Y </code> || { ''a'' = ''y'', ''x'' = ''y'' } || { ''x'' ↦ ''a'', ''y'' ↦ ''a'' } || As above (order of equations in set doesn't matter)
|-
| <code> X = a, b = X </code> || { ''x'' = ''a'', ''b'' = ''x'' }  || ⊥ || Fails. ''a'' and ''b'' do not match, so ''x'' can't be unified with both
|}

[[File:Unification exponential blow-up svg.svg|thumb|Two terms with an exponentially larger tree for their least common instance. Its [[directed acyclic graph|dag]] representation (rightmost, orange part) is still of linear size.]]
The most general unifier of a syntactic first-order unification problem of [[Term (logic)#Operations with terms|size]] {{mvar|n}} may have a size of {{math|2<sup>''n''</sup>}}. For example, the problem {{tmath| (((a*z)*y)*x)*w \doteq w*(x*(y*(z*a))) }} has the most general unifier {{tmath| \{ z \mapsto a,  y \mapsto a*a,  x \mapsto (a*a)*(a*a),  w \mapsto ((a*a)*(a*a))*((a*a)*(a*a)) \} }}, cf. picture. In order to avoid exponential time complexity caused by such blow-up, advanced unification algorithms work on [[directed acyclic graph]]s (dags) rather than trees.{{refn|e.g. {{harvtxt|Paterson|Wegman|1978}} sect.2, p.159}}