Editing Unification (computer science) (section)

===Generalization, specialization===
If a term <math>t</math> has an instance equivalent to a term <math>u</math>, that is, if <math>t\sigma \equiv u</math> for some substitution <math>\sigma</math>, then <math>t</math> is called ''more general'' than <math>u</math>, and <math>u</math> is called ''more special'' than, or ''subsumed'' by, <math>t</math>. For example, <math>x\oplus a</math> is more general than <math>a\oplus b</math> if ⊕ is [[Commutative property|commutative]], since then <math>(x\oplus a) \{x\mapsto b\} = b\oplus a\equiv a\oplus b</math>.

If ≡ is literal (syntactic) identity of terms, a term may be both more general and more special than another one only if both terms differ just in their variable names, not in their syntactic structure; such terms are called ''variants'', or ''renamings'' of each other.
For example, 
<math>f(x_1, a, g(z_1), y_1)</math>
is a variant of 
<math>f(x_2, a, g(z_2), y_2)</math>,
since
<math display="block">f(x_1, a, g(z_1), y_1) \{x_1 \mapsto x_2, y_1 \mapsto y_2, z_1 \mapsto z_2\} = f(x_2, a, g(z_2), y_2) </math>
and
<math display="block">f(x_2, a, g(z_2), y_2) \{x_2 \mapsto x_1, y_2 \mapsto y_1, z_2 \mapsto z_1\} = f(x_1, a, g(z_1), y_1).</math>
However, <math>f(x_1, a, g(z_1), y_1)</math> is ''not'' a variant of  <math>f(x_2, a, g(x_2), x_2)</math>, since no substitution can transform the latter term into the former one.
The latter term is therefore properly more special than the former one.

For arbitrary <math>\equiv</math>, a term may be both more general and more special than a structurally different term.
For example, if ⊕ is [[idempotent]], that is, if always <math>x \oplus x \equiv x</math>, then the term <math>x\oplus y</math> is more general than <math>z</math>,<ref group=note>since <math>(x\oplus y) \{x\mapsto z, y \mapsto z\} = z\oplus z \equiv z</math></ref> and vice versa,<ref group=note>since {{math|1=''z'' {{mset|''z'' ↦ ''x'' ⊕ ''y''}} = ''x'' ⊕ ''y''}}</ref> although <math>x\oplus y</math> and <math>z</math> are of different structure.

A substitution <math>\sigma</math> is ''more special'' than, or ''subsumed'' by, a substitution <math>\tau</math> if <math>t\sigma</math> is subsumed by <math>t\tau</math> for each term <math>t</math>.  We also say that <math>\tau</math> is more general than <math>\sigma</math>. More formally, take a nonempty infinite set <math>V</math> of auxiliary variables such that no equation <math>l_i \doteq r_i</math> in the unification problem contains variables from <math>V</math>. Then a substitution <math>\sigma</math> is subsumed by another substitution <math>\tau</math> if there is a substitution <math>\theta</math> such that for all terms <math>X\notin V</math>, <math>X\sigma \equiv X\tau\theta</math>.<ref name=Vukmirovic/>
For instance <math> \{x \mapsto a, y \mapsto a \}</math> is subsumed by <math>\tau = \{x\mapsto y\}</math>, using <math>\theta=\{y\mapsto a\}</math>, but 
<math>\sigma = \{x\mapsto a\}</math> is not subsumed by <math>\tau = \{x\mapsto y\}</math>, as <math>f(x, y)\sigma = f(a, y)</math> is not an instance of
<math>f(x, y) \tau = f(y, y)</math>.<ref>{{cite book |last1=Apt |first1=Krzysztof R. |title=From logic programming to Prolog |date=1997 |publisher=Prentice Hall |location=London Munich |isbn=013230368X |edition=1. publ |url=https://homepages.cwi.nl/~apt/book.ps|page=24}}</ref>