Editing Unification (computer science) (section)

===Prerequisites===
Formally, a unification approach presupposes
* An infinite set <math>V</math> of ''variables''. For higher-order unification, it is convenient to choose <math>V</math> disjoint from the set of [[lambda-term bound variables]].
* A set <math>T</math> of ''terms'' such that <math>V \subseteq T</math>. For first-order unification, <math>T</math> is usually the set of [[first-order terms]] (terms built from variable and function symbols).  For higher-order unification <math>T</math> consists of first-order terms and [[lambda terms]] (terms containing some higher-order variables).
* A mapping <math>\text{vars}\colon T \rightarrow</math> [[power set|<math>\mathbb{P}</math>]]<math>(V)</math>, assigning to each term <math>t</math> the set <math>\text{vars}(t) \subsetneq V</math> of ''free variables'' occurring in <math>t</math>.
* A theory or [[equivalence relation]] <math>\equiv</math> on <math>T</math>, indicating which terms are considered equal. For first-order E-unification, <math>\equiv</math> reflects the background knowledge about certain function symbols; for example, if <math>\oplus</math> is considered commutative, <math>t\equiv u</math> if <math>u</math> results from <math>t</math> by swapping the arguments of <math>\oplus</math> at some (possibly all) occurrences. <ref group=note>E.g. ''a'' ⊕ (''b'' ⊕ ''f''(''x'')) ≡ ''a'' ⊕ (''f''(''x'') ⊕ ''b'') ≡ (''b'' ⊕ ''f''(''x'')) ⊕ ''a'' ≡ (''f''(''x'') ⊕ ''b'') ⊕ ''a''</ref> In the most typical case that there is no background knowledge at all, then only literally, or syntactically, identical terms are considered equal. In this case, ≡ is called the ''[[free theory]]'' (because it is a [[free object]]), the ''[[empty theory]]'' (because the set of equational [[sentence (mathematical logic)|sentences]], or the background knowledge, is empty), the ''theory of [[uninterpreted function]]s'' (because unification is done on uninterpreted [[term (logic)|terms]]), or the ''theory of [[Algebraic specification|constructors]]'' (because all function symbols just build up data terms, rather than operating on them). For higher-order unification, usually <math>t\equiv u</math> if <math>t</math> and <math>u</math> are [[alpha equivalent]].

As an example of how the set of terms and theory affects the set of solutions, the syntactic first-order unification problem { ''y'' = ''cons''(2,''y'') } has no solution over the set of [[finite terms]]. However, it has the single solution { ''y'' ↦ ''cons''(2,''cons''(2,''cons''(2,...))) } over the set of [[Tree (set theory)|infinite tree]] terms. Similarly, the semantic first-order unification problem { ''a''⋅''x'' = ''x''⋅''a'' } has each substitution of the form { ''x'' ↦ ''a''⋅...⋅''a'' } as a solution in a [[semigroup]], i.e. if (⋅) is considered [[associative]]. But the same problem, viewed in an [[abelian group]], where  (⋅) is considered also [[commutative]], has any substitution at all as a solution.

As an example of higher-order unification, the singleton set { ''a'' = ''y''(''x'') } is a syntactic second-order unification problem, since ''y'' is a function variable. One solution is { ''x'' ↦ ''a'', ''y'' ↦ ([[identity function]]) }; another one is { ''y'' ↦ ([[constant function]] mapping each value to ''a''), ''x'' ↦ ''(any value)'' }.