Editing Unification (computer science) (section)

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