Editing Unification (computer science) (section)

==Higher-order unification==
[[File:Goldfarb4a svg.svg|thumb|300px|In Goldfarb's<ref name="Goldfarb.1981"/> reduction of [[Hilbert's 10th problem]] to second-order unifiability, the equation <math>X_1 * X_2 = X_3</math> corresponds to the depicted unification problem, with function variables <math>F_i</math> corresponding to <math>X_i</math> and <math>G</math> [[fresh variable|fresh]].]] 
Many applications require one to consider the unification of typed lambda-terms instead of first-order terms.  Such unification is often called ''higher-order unification''. Higher-order unification is [[Undecidable problem|undecidable]],<ref name="Goldfarb.1981">{{cite journal| author=Warren D. Goldfarb| author-link=Warren D. Goldfarb| title=The Undecidability of the Second-Order Unification Problem| journal=TCS| year=1981| volume=13| issue=2| pages=225–230| doi=10.1016/0304-3975(81)90040-2| doi-access=free}}</ref><ref>{{cite journal| author=Gérard P. Huet| title=The Undecidability of Unification in Third Order Logic| journal=Information and Control| year=1973| volume=22| issue=3| pages=257–267 |doi=10.1016/S0019-9958(73)90301-X| doi-access=free}}</ref><ref>Claudio Lucchesi: The Undecidability of the Unification Problem for Third Order Languages (Research Report CSRR 2059; Department of Computer Science, University of Waterloo, 1972)</ref> and such unification problems do not have most general unifiers. For example, the unification problem { ''f''(''a'',''b'',''a'') ≐ ''d''(''b'',''a'',''c'') }, where the only variable is ''f'', has the
solutions {''f'' ↦ λ''x''.λ''y''.λ''z''. ''d''(''y'',''x'',''c'')  }, {''f'' ↦ λ''x''.λ''y''.λ''z''. ''d''(''y'',''z'',''c'')  },
{''f'' ↦ λ''x''.λ''y''.λ''z''. ''d''(''y'',''a'',''c'')  }, {''f'' ↦ λ''x''.λ''y''.λ''z''. ''d''(''b'',''x'',''c'')  },
{''f'' ↦ λ''x''.λ''y''.λ''z''. ''d''(''b'',''z'',''c'')  } and {''f'' ↦ λ''x''.λ''y''.λ''z''. ''d''(''b'',''a'',''c'')  }. A well studied branch of higher-order unification is the problem of unifying simply typed lambda terms modulo the equality determined by αβη conversions. [[Gérard Huet]] gave a [[semi-decidable]] (pre-)unification algorithm<ref>Gérard Huet: (1 June 1975) [https://www.semanticscholar.org/paper/A-Unification-Algorithm-for-Typed-lambda-Calculus-Huet/32b1b03b5450ac1f286933f44939e71e5068e8d3 A Unification Algorithm for typed Lambda-Calculus], ''[[Theoretical Computer Science (journal)|Theoretical Computer Science]]'' </ref> that allows a systematic search of the space of unifiers (generalizing the unification algorithm of Martelli-Montanari<ref name="Martelli.Montanari.1982"/> with rules for terms containing higher-order variables) that seems to work sufficiently well in practice.  Huet<ref>[http://portal.acm.org/citation.cfm?id=695200 Gérard Huet: Higher Order Unification 30 Years Later]</ref> and Gilles Dowek<ref>Gilles Dowek: Higher-Order Unification and Matching. Handbook of Automated Reasoning 2001: 1009–1062</ref> have written articles surveying this topic.

Several subsets of higher-order unification are well-behaved, in that they are decidable and have a most-general unifier for solvable problems. One such subset is the previously described first-order terms. '''Higher-order pattern unification''', due to Dale Miller,<ref>{{cite journal|first1=Dale|last1=Miller|title=A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification|journal=Journal of Logic and Computation|volume=1|issue=4|year=1991|pages=497–536|url=http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/jlc91.pdf|doi=10.1093/logcom/1.4.497}}</ref> is another such subset. The higher-order logic programming languages [[λProlog]] and [[Twelf]] have switched from full higher-order unification to implementing only the pattern fragment; surprisingly pattern unification is sufficient for almost all programs, if each non-pattern unification problem is suspended until a subsequent substitution puts the unification into the pattern fragment. A superset of pattern unification called functions-as-constructors unification is also well-behaved.<ref>{{cite journal |last1=Libal |first1=Tomer |last2=Miller |first2=Dale |title=Functions-as-constructors higher-order unification: extended pattern unification |journal=Annals of Mathematics and Artificial Intelligence |date=May 2022 |volume=90 |issue=5 |pages=455–479 |doi=10.1007/s10472-021-09774-y|doi-access=free}}</ref> The Zipperposition theorem prover has an algorithm integrating these well-behaved subsets into a full higher-order unification algorithm.<ref name=Vukmirovic>{{cite journal |last1=Vukmirović |first1=Petar |last2=Bentkamp |first2=Alexander |last3=Nummelin |first3=Visa |title=Efficient Full Higher-Order Unification |journal=Logical Methods in Computer Science |date=14 December 2021 |volume=17 |issue=4 |pages=6919 |doi=10.46298/lmcs-17(4:18)2021|doi-access=free |arxiv=2011.09507 }}</ref>

In computational linguistics, one of the most influential theories of [[elliptical construction]] is that ellipses are represented by free variables whose values are then determined using Higher-Order Unification. For instance, the semantic representation of "Jon likes Mary and Peter does too" is  {{math| like(''j'', ''m'') &and; R(''p'') }} and the value of R (the semantic representation of the ellipsis) is determined by the equation {{math| like(''j'', ''m'') {{=}} R(''j'')  }}. The process of solving such equations is called Higher-Order Unification.<ref>{{cite book| first1 = Claire | last1 = Gardent |author1-link=Claire Gardent| first2 = Michael | last2 = Kohlhase | first3 = Karsten | last3 = Konrad | author2-link=Michael Kohlhase| chapter=A Multi-Level, Higher-Order Unification Approach to Ellipsis| title=Submitted to European [[Association for Computational Linguistics]] (EACL)<!---according to http://page.mi.fu-berlin.de/cbenzmueller/papers/R8.pdf--->| year=1997|citeseerx = 10.1.1.55.9018}}</ref>

[[Wayne Snyder]] gave a generalization of both higher-order unification and E-unification, i.e. an algorithm to unify lambda-terms modulo an equational theory.<ref>{{cite book | author=Wayne Snyder | contribution=Higher order E-unification | title=Proc. 10th Conference on Automated Deduction | publisher=Springer | series=LNAI | volume=449 | pages=573–587 |date=Jul 1990 | title-link=Conference on Automated Deduction }}</ref>