Editing Unification (computer science) (section)

==Syntactic unification of first-order terms==
[[File:Triangle diagram of syntactic unification svg.svg|thumb|Schematic triangle diagram of syntactically unifying terms ''t''<sub>1</sub> and ''t''<sub>2</sub> by a substitution σ]]
''Syntactic unification of first-order terms'' is the most widely used unification framework.
It is based on ''T'' being the set of ''first-order terms'' (over some given set ''V'' of variables, ''C'' of constants and ''F''<sub>''n''</sub> of ''n''-ary function symbols) and on ≡ being ''syntactic equality''.
In this framework, each solvable unification problem {{math|{{mset|''l''<sub>1</sub> ≐ ''r''<sub>1</sub>, ..., ''l''<sub>''n''</sub> ≐ ''r''<sub>''n''</sub>}}}} has a complete, and obviously minimal, [[Singleton (mathematics)|singleton]] solution set {{math|1={{mset|''σ''}}}}.
Its member {{mvar|σ}} is called the '''most general unifier''' (''mgu'') of the problem.
The terms on the left and the right hand side of each potential equation become syntactically equal when the mgu is applied i.e. {{math|1=''l''<sub>1</sub>''σ'' = ''r''<sub>1</sub>''σ'' ∧ ... ∧ ''l''<sub>''n''</sub>''σ'' = ''r''<sub>''n''</sub>''σ''}}.
Any unifier of the problem is subsumed<ref group=note>formally: each unifier τ satisfies {{math|1=∀''x'': ''xτ'' = (''xσ'')''ρ''}} for some substitution ρ</ref> by the mgu {{mvar|σ}}.
The mgu is unique up to variants: if ''S''<sub>1</sub> and ''S''<sub>2</sub> are both complete and minimal solution sets of the same syntactical unification problem, then ''S''<sub>1</sub> = { ''σ''<sub>1</sub> } and ''S''<sub>2</sub> = { ''σ''<sub>2</sub> } for some substitutions {{math|1=''σ''<sub>1</sub>}} and {{math|1=''σ''<sub>2</sub>,}} and {{math|1=''xσ''<sub>1</sub>}} is a variant of {{math|1=''xσ''<sub>2</sub>}} for each variable ''x'' occurring in the problem.

For example, the unification problem { ''x'' ≐ ''z'', ''y'' ≐ ''f''(''x'') } has a unifier { ''x'' ↦ ''z'', ''y'' ↦ ''f''(''z'') }, because
:{|
|-
| align="right" | ''x''
| { ''x'' ↦ ''z'', ''y'' ↦ ''f''(''z'') }
| =
| align="center" | ''z''
| =
| align="right" | ''z''
| { ''x'' ↦ ''z'', ''y'' ↦ ''f''(''z'') }
|, and
|-
| align="right" | ''y''
| { ''x'' ↦ ''z'', ''y'' ↦ ''f''(''z'') }
| =
| align="center" | ''f''(''z'')
| =
| align="right" | ''f''(''x'')
| { ''x'' ↦ ''z'', ''y'' ↦ ''f''(''z'') }
| .
|}

This is also the most general unifier.
Other unifiers for the same problem are e.g. { ''x'' ↦ ''f''(''x''<sub>1</sub>), ''y'' ↦ ''f''(''f''(''x''<sub>1</sub>)), ''z'' ↦ ''f''(''x''<sub>1</sub>) }, { ''x'' ↦ ''f''(''f''(''x''<sub>1</sub>)), ''y'' ↦ ''f''(''f''(''f''(''x''<sub>1</sub>))), ''z'' ↦ ''f''(''f''(''x''<sub>1</sub>)) }, and so on; there are infinitely many similar unifiers.

As another example, the problem ''g''(''x'',''x'') ≐ ''f''(''y'') has no solution with respect to ≡ being literal identity, since any substitution applied to the left and right hand side will keep the outermost ''g'' and ''f'', respectively, and terms with different outermost function symbols are syntactically different.

===Unification algorithms===
{{Quote box|title=Robinson's 1965 unification algorithm
|quote={{hidden begin}}
Symbols are ordered such that variables precede function symbols.
Terms are ordered by increasing written length; equally long terms 
are ordered [[lexicographically]].{{refn|{{harvtxt|Robinson|1965}} nr.2.5, 2.14, p.25}} For a set ''T'' of terms, its disagreement 
path ''p'' is the lexicographically least path where two member terms   
of ''T'' differ. Its disagreement set is the set of [[subterms]] starting at ''p'', 
formally: {{math|{ ''t''[[term (logic)#Operations with terms|{{pipe}}<sub>''p''</sub>]] : <math>t\in T</math> }}}.{{refn|{{harvtxt|Robinson|1965}} nr.5.6, p.32}}

''Algorithm:''{{refn|{{harvtxt|Robinson|1965}} nr.5.8, p.32}}
<code><br>
Given a set ''T'' of terms to be unified<br>
Let <math>\sigma</math> initially be the [[identity substitution]]<br>
<code>do forever</code><br>
&nbsp; &nbsp; <code>if</code> <math>T\sigma</math> is a [[singleton set]] <code>then</code><br>
&nbsp; &nbsp; &nbsp; &nbsp; <code>return</code> <math>\sigma</math><br>
&nbsp; &nbsp; <code>fi</code><br>
&nbsp; &nbsp; let ''D'' be the disagreement set of <math>T\sigma</math><br>
&nbsp; &nbsp; let ''s'', ''t'' be the two lexicographically least terms in ''D''<br>
&nbsp; &nbsp; <code>if</code> ''s'' is not a variable <code>or</code> ''s'' occurs in ''t'' <code>then</code><br>
&nbsp; &nbsp; &nbsp; &nbsp; <code>return</code> "NONUNIFIABLE"<br>
&nbsp; &nbsp; <code>fi</code> <br>
&nbsp; &nbsp;  <math>\sigma := \sigma \{ s \mapsto t \}</math><br>
<code>done</code>
</code>
{{hidden end}}
}}
[[Jacques Herbrand]] discussed the basic concepts of unification and sketched an algorithm in 1930.<ref>J. Herbrand: Recherches sur la théorie de la démonstration. ''Travaux de la société des Sciences et des Lettres de Varsovie'', Class III, Sciences Mathématiques et Physiques, 33, 1930.</ref><ref>{{cite thesis | type=Ph.D. thesis | url=http://www.numdam.org/issue/THESE_1930__110__1_0.pdf | author=Jacques Herbrand | title=Recherches sur la théorie de la demonstration | institution=Université de Paris | series=A | volume=1252 | year=1930 }} Here: p.96-97</ref><ref name="HerbrandLectures">{{cite report | author1=Claus-Peter Wirth |  author2=Jörg Siekmann | author3= Christoph Benzmüller | author4= Serge Autexier | title=Lectures on Jacques Herbrand as a Logician | institution=DFKI | type=SEKI Report | number=SR-2009-01 | year=2009 | arxiv=0902.4682 }} Here: p.56</ref> But most authors attribute the first unification algorithm to [[John Alan Robinson]] (cf. box).<ref name="Robinson.1965">{{cite journal | first1=J.A.|last1=Robinson | title=A Machine-Oriented Logic Based on the Resolution Principle | journal=Journal of the ACM | volume=12 | number=1 | pages=23–41 |date=Jan 1965 | doi=10.1145/321250.321253| s2cid=14389185 | doi-access=free }}; Here: sect.5.8, p.32</ref><ref>{{cite journal | author=J.A. Robinson | title=Computational logic: The unification computation | journal=Machine Intelligence | volume=6 | pages=63–72 | url=https://aitopics.org/download/classics:E35191E8 | year=1971 }}</ref>{{#tag:ref|Robinson used first-order syntactical unification as a basic building block of his [[Resolution (logic)|resolution]] procedure for first-order logic, a great step forward in [[automated reasoning]] technology, as it eliminated one source of [[combinatorial explosion]]: searching for instantiation of terms.<ref>{{cite book | author=David A. Duffy | title=Principles of Automated Theorem Proving | location=New York | publisher=Wiley | year=1991 | isbn=0-471-92784-8}} Here: Introduction of sect.3.3.3 ''"Unification"'', p.72.</ref>|group=note}} Robinson's algorithm had worst-case exponential behavior in both time and space.<ref name="HerbrandLectures"/><ref name="Champeaux">{{cite journal | url=https://raw.githubusercontent.com/ddccc/Unification/a5975a47bca1be3f7bf0afe9ad3595a707a29ea4/LinUnify3.pdf | doi=10.1007/s10817-022-09635-1 | first1=Dennis|last1=de Champeaux | title=Faster Linear Unification Algorithm | journal=Journal of Automated Reasoning | volume=66 | pages=845&ndash;860 | date=Aug 2022 | issue=4 }}</ref> Numerous authors have proposed more efficient unification algorithms.<ref>Per {{harvtxt|Martelli|Montanari|1982}}:
* {{cite report | author=Lewis Denver Baxter | title=A practically linear unification algorithm | publisher=Univ. of Waterloo, Ontario | type=Res. Report | volume=CS-76-13 | url=https://cs.uwaterloo.ca/research/tr/1976/CS-76-13.pdf |date=Feb 1976 }}
* {{cite thesis | author=Gérard Huet | title=Resolution d'Equations dans des Langages d'Ordre 1,2,...ω | publisher=Universite de Paris VII | type=These d'etat |date=Sep 1976 | author-link=Gérard Huet }}
* {{cite report | first1=Alberto|last1=Martelli | first2=Ugo|last2=Montanari | name-list-style=amp | title=Unification in linear time and space: A structured presentation | publisher=Consiglio Nazionale delle Ricerche, Pisa | type=Internal Note | volume=IEI-B76-16 | url=http://puma.isti.cnr.it/publichtml/section_cnr_iei/cnr_iei_1976-B4-041.html | archive-url=https://web.archive.org/web/20150115070153/http://puma.isti.cnr.it/publichtml/section_cnr_iei/cnr_iei_1976-B4-041.html | url-status=dead | archive-date=2015-01-15 | date=Jul 1976 }}
* {{cite conference | doi=10.1145/800113.803646 | url= | first1=M.S. |last1=Paterson |first2= M.N. |last2= Wegman | title=Linear unification | editor1-first=Ashok K. |editor1-last=Chandra |editor2-first= Detlef |editor2-last= Wotschke  |editor3-first= Emily P. |editor3-last=Friedman  |editor4-first= Michael A.|editor4-last= Harrison  | conference=Proceedings of the eighth annual ACM [[Symposium on Theory of Computing]] (STOC) | publisher=ACM | pages=181&ndash;186 | date=May 1976 |doi-access=free }}
* {{cite journal | first1=M.S. |last1=Paterson |author1-link=Michael Stewart Paterson |first2= M.N. |last2= Wegman | title=Linear unification | journal=J. Comput. Syst. Sci. | volume=16 | number=2 | pages=158–167 |date=Apr 1978 | doi = 10.1016/0022-0000(78)90043-0 | doi-access=free }}
* {{cite book | author=J.A. Robinson | chapter=Fast unification | editor=[[Woodrow W. Bledsoe]], Michael M. Richter | title=Proc. Theorem Proving Workshop Oberwolfach | series=Oberwolfach Workshop Report | volume=1976/3 | date=Jan 1976 | author-link=J.A. Robinson }}
* {{cite journal | author=M. Venturini-Zilli | title=Complexity of the unification algorithm for first-order expressions |journal= Calcolo | volume=12 |number=4 |pages= 361–372 |date= Oct 1975 | doi=10.1007/BF02575754| s2cid=189789152 }}</ref> Algorithms with worst-case linear-time behavior were discovered independently by {{harvtxt|Martelli|Montanari|1976}} and {{harvtxt|Paterson|Wegman|1976}}{{refn|Independent discovery is stated in {{harvtxt|Martelli|Montanari|1982}} sect.1, p.259. The journal publisher received {{harvtxt|Paterson|Wegman|1978}} in Sep.1976.|group=note}} {{harvtxt|Baader|Snyder|2001}} uses a similar technique as Paterson-Wegman, hence is linear,<ref>{{cite book |last1=Baader |first1=Franz |last2=Snyder |first2=Wayne |chapter=Unification Theory |title=Handbook of Automated Reasoning|title-link=Handbook of Automated Reasoning |date=2001 |pages=445–533 |doi=10.1016/B978-044450813-3/50010-2|isbn=978-0-444-50813-3 |chapter-url=https://www.cs.bu.edu/fac/snyder/publications/UnifChapter.pdf}}</ref> but like most linear-time unification algorithms is slower than the Robinson version on small sized inputs due to the overhead of preprocessing the inputs and postprocessing of the output, such as construction of a [[directed acyclic graph|DAG]] representation. {{harvtxt|de Champeaux|2022}} is also of linear complexity in the input size but is competitive with the Robinson algorithm on small size inputs. The speedup is obtained by using an [[object-oriented programming|object-oriented]] representation of the predicate calculus that avoids the need for pre- and post-processing, instead making variable objects responsible for creating a substitution and for dealing with aliasing. de Champeaux claims that the ability to add functionality to predicate calculus represented as programmatic [[Object (computer science)|object]]s provides opportunities for optimizing other logic operations as well.<ref name="Champeaux"/>

The following algorithm is commonly presented and originates from {{harvtxt|Martelli|Montanari|1982}}.<ref group=note>Alg.1, p.261. Their rule ''(a)'' corresponds to rule ''swap'' here, ''(b)'' to ''delete'', ''(c)'' to both ''decompose'' and ''conflict'', and ''(d)'' to both ''eliminate'' and ''check''.</ref> Given a finite set <math>G = \{ s_1 \doteq t_1, ..., s_n \doteq t_n \}</math> of potential equations,
the algorithm applies rules to transform it to an equivalent set of equations of the form
{ ''x''<sub>1</sub> ≐ ''u''<sub>1</sub>, ..., ''x''<sub>''m''</sub> ≐ ''u''<sub>''m''</sub> }
where ''x''<sub>1</sub>, ..., ''x''<sub>''m''</sub> are distinct variables and ''u''<sub>1</sub>, ..., ''u''<sub>''m''</sub> are terms containing none of the ''x''<sub>''i''</sub>.
A set of this form can be read as a substitution.
If there is no solution the algorithm terminates with ⊥; other authors use "Ω",  or "''fail''" in that case.
The operation of substituting all occurrences of variable ''x'' in problem ''G'' with term ''t'' is denoted ''G'' {''x'' ↦ ''t''}.
For simplicity, constant symbols are regarded as function symbols having zero arguments.

:{|
| align="right" | <math>G \cup \{ t \doteq t \}</math>
| <math>\Rightarrow</math>
| <math>G</math>
|
| &nbsp; &nbsp; ''delete''
|-
| align="right" | <math>G \cup \{ f(s_0, ..., s_k) \doteq f(t_0, ..., t_k) \}</math>
| <math>\Rightarrow</math> 
| <math>G \cup \{ s_0 \doteq t_0, ..., s_k \doteq t_k \}</math>
|
| &nbsp; &nbsp; ''decompose''
|-
| align="right" | <math>G \cup \{ f(s_0, \ldots,s_k) \doteq g(t_0,...,t_m) \}</math>
| <math>\Rightarrow</math>
| <math>\bot</math>
| align="right" | if <math>f \neq g</math> or <math>k \neq m</math>
| &nbsp; &nbsp; ''conflict''
|-
| align="right" | <math>G \cup \{ f(s_0,...,s_k) \doteq x \}</math>
| <math>\Rightarrow</math>
| <math>G \cup \{ x \doteq f(s_0,...,s_k) \}</math>
|
| &nbsp; &nbsp; ''swap''
|-
| align="right" | <math>G \cup \{ x \doteq t \}</math>
| <math>\Rightarrow</math>
| <math>G\{x \mapsto t\} \cup \{ x \doteq t \}</math>
| align="right" | if <math>x \not\in \text{vars}(t)</math> and <math>x \in \text{vars}(G)</math>
| &nbsp; &nbsp; ''eliminate''<ref group="note">Although the rule keeps ''x'' ≐ ''t'' in ''G'', it cannot loop forever since its precondition ''x''∈''vars''(''G'') is invalidated by its first application. More generally, the algorithm is guaranteed to terminate always, see [[#Proof of termination|below]].</ref>
|-
| align="right" | <math>G \cup \{ x \doteq f(s_0,...,s_k) \}</math>
| <math>\Rightarrow</math>
| <math>\bot</math>
| align="right" | if <math>x \in \text{vars}(f(s_0,...,s_k))</math>
| &nbsp; &nbsp; ''check''
|}

====Occurs check====
{{main|Occurs check}}
An attempt to unify a variable ''x'' with a term containing ''x'' as a strict subterm ''x'' ≐ ''f''(..., ''x'', ...) would lead to an infinite term as solution for ''x'', since ''x'' would occur as a subterm of itself.
In the set of (finite) first-order terms as defined above, the equation ''x'' ≐ ''f''(..., ''x'', ...) has no solution; hence the ''eliminate'' rule may only be applied if ''x'' ∉ ''vars''(''t'').
Since that additional check, called ''occurs check'', slows down the algorithm, it is omitted e.g. in most Prolog systems.
From a theoretical point of view, omitting the check amounts to solving equations over infinite trees, see [[#Unification of infinite terms]] below.

====Proof of termination====
For the proof of termination of the algorithm consider a triple <math>\langle n_{var}, n_{lhs}, n_{eqn}\rangle</math>
where {{math|''n''<sub>''var''</sub>}} is the number of variables that occur more than once in the equation set, {{math|''n''<sub>''lhs''</sub>}} is the number of function symbols and constants
on the left hand sides of potential equations, and {{math|''n''<sub>''eqn''</sub>}} is the number of equations.
When rule ''eliminate'' is applied, {{math|''n''<sub>''var''</sub>}} decreases, since ''x'' is eliminated from ''G'' and kept only in { ''x'' ≐ ''t'' }.
Applying any other rule can never increase {{math|''n''<sub>''var''</sub>}} again.
When rule ''decompose'', ''conflict'', or ''swap'' is applied, {{math|''n''<sub>''lhs''</sub>}} decreases, since at least the left hand side's outermost ''f'' disappears.
Applying any of the remaining rules ''delete'' or ''check'' can't increase {{math|''n''<sub>''lhs''</sub>}}, but decreases {{math|''n''<sub>''eqn''</sub>}}.
Hence, any rule application decreases the triple <math>\langle n_{var}, n_{lhs}, n_{eqn}\rangle</math> with respect to the [[lexicographical order]], which is possible only a finite number of times.

[[Conor McBride]] observes<ref>{{cite journal|last=McBride|first=Conor|title=First-Order Unification by Structural Recursion|journal=Journal of Functional Programming|date=October 2003|volume=13|issue=6|pages=1061–1076|doi=10.1017/S0956796803004957|url=http://strictlypositive.org/unify.ps.gz|access-date=30 March 2012|issn=0956-7968|citeseerx=10.1.1.25.1516|s2cid=43523380 }}</ref> that "by expressing the structure which unification exploits" in a [[dependently typed]] language such as [[Epigram (programming language)|Epigram]], [[Robinson's unification algorithm]] can be made [[recursive on the number of variables]], in which case a separate termination proof becomes unnecessary.

===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}}

===Application: unification in logic programming===
The concept of unification is one of the main ideas behind [[logic programming]]. Specifically, unification is a basic building block of [[Resolution (logic)|resolution]], a rule of inference for determining formula satisfiability. In [[Prolog]], the equality symbol <code>=</code> implies first-order syntactic unification. It represents the mechanism of binding the contents of variables and can be viewed as a kind of one-time assignment.

In Prolog:
# A [[variable (programming)|variable]] can be unified with a constant, a term, or another variable, thus effectively becoming its alias. In many modern Prolog dialects and in [[first-order logic]], a variable cannot be unified with a term that contains it; this is the so-called ''[[occurs check]]''.
# Two constants can be unified only if they are identical.
# Similarly, a term can be unified with another term if the top function symbols and [[arities]] of the terms are identical and if the parameters can be unified simultaneously. Note that this is a recursive behavior.
# Most operations, including <code>+</code>, <code>-</code>, <code>*</code>, <code>/</code>, are not evaluated by <code>=</code>. So for example <code>1+2 = 3</code> is not satisfiable because they are syntactically different. The use of integer arithmetic constraints <code>#=</code> introduces a form of E-unification for which these operations are interpreted and evaluated.<ref>{{cite web |title=Declarative integer arithmetic |url=https://www.swi-prolog.org/pldoc/man?section=clpfd-integer-arith |website=SWI-Prolog |access-date=18 February 2024}}</ref>

=== Application: type inference ===
[[Type inference]] algorithms are typically based on unification, particularly [[Hindley–Milner type system|Hindley-Milner]] type inference which is used by the functional languages [[Haskell (programming language)|Haskell]] and [[ML (programming language)|ML]]. For example, when attempting to infer the type of the Haskell expression <code>True : ['x']</code>, the compiler will use the type <code>a -> [a] -> [a]</code> of the list construction function <code>(:)</code>, the type <code>Bool</code> of the first argument <code>True</code>, and the type <code>[Char]</code> of the second argument <code>['x']</code>. The polymorphic type variable <code>a</code> will be unified with <code>Bool</code> and the second argument <code>[a]</code> will be unified with <code>[Char]</code>. <code>a</code> cannot be both <code>Bool</code> and <code>Char</code> at the same time, therefore this expression is not correctly typed.

Like for Prolog, an algorithm for type inference can be given:

# Any type variable unifies with any type expression, and is instantiated to that expression.  A specific theory might restrict this rule with an occurs check.
# Two type constants unify only if they are the same type.
# Two type constructions unify only if they are applications of the same type constructor and all of their component types recursively unify.

=== Application: Feature Structure Unification ===
{{see also|Feature structure}}

Unification has been used in different research areas of computational linguistics.<ref>Jonathan Calder, Mike Reape, and Hank Zeevat,, [https://www.aclweb.org/anthology/E89-1032 An algorithm for generation in unification categorial grammar]. In Proceedings of the 4th Conference of the European Chapter of the Association for Computational Linguistics, pages 233-240, Manchester, England (10–12 April), University of Manchester Institute of Science and Technology, 1989.</ref><ref>Graeme Hirst and David St-Onge, [http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.8426] Lexical chains as representations of context for the detection and correction of malapropisms, 1998.</ref>