Inlogic andcomputer science, specificallyautomated reasoning,unification is an algorithmic process ofsolving equations between symbolicexpressions, each of the formLeft-hand side = Right-hand side. For example, usingx,y,z as variables, and takingf to be anuninterpreted function, thesingleton equation set {f(1,y) =f(x,2) } is a syntactic first-order unification problem that has the substitution {x↦ 1,y ↦ 2 } as its only solution.
Conventions differ on what values variables may assume and which expressions are considered equivalent. In first-order syntactic unification, variables range overfirst-order terms and equivalence is syntactic. This version of unification has a unique "best" answer and is used inlogic programming and programming languagetype system implementation, especially inHindley–Milner basedtype inference algorithms. In higher-order unification, possibly restricted tohigher-order pattern unification, terms may include lambda expressions, and equivalence is up to beta-reduction. This version is used inproof assistants and higher-order logic programming, for exampleIsabelle,Twelf, andlambdaProlog. Finally, in semantic unification or E-unification, equality is subject to background knowledge and variables range over a variety of domains. This version is used inSMT solvers,term rewriting algorithms, andcryptographic protocol analysis.
Aunification problem is a finite setE={l1 ≐r1, ...,ln ≐rn } of equations to solve, whereli,ri are in the set ofterms orexpressions. Depending on which expressions or terms are allowed to occur in an equation set or unification problem, and which expressions are considered equal, several frameworks of unification are distinguished. If higher-order variables, that is, variables representingfunctions, are allowed in an expression, the process is calledhigher-order unification, otherwisefirst-order unification. If a solution is required to make both sides of each equation literally equal, the process is calledsyntactic orfreeunification, otherwisesemantic orequational unification, orE-unification, orunification modulo theory.
If the right side of each equation is closed (no free variables), the problem is called (pattern)matching. The left side (with variables) of each equation is called thepattern.[1]
Formally, a unification approach presupposes
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 offinite terms. However, it has the single solution {y ↦cons(2,cons(2,cons(2,...))) } over the set ofinfinite 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 asemigroup, i.e. if (⋅) is consideredassociative. But the same problem, viewed in anabelian group, where (⋅) is considered alsocommutative, 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, sincey is a function variable. One solution is {x ↦a,y ↦ (identity function) }; another one is {y ↦ (constant function mapping each value toa),x ↦(any value) }.
Asubstitution is a mapping from variables to terms; the notation refers to a substitution mapping each variable to the term, for, and every other variable to itself; the must be pairwise distinct.Applying that substitution to a term is written inpostfix notation as; it means to (simultaneously) replace every occurrence of each variable in the term by. The result of applying a substitution to a term is called aninstance of that term.As a first-order example, applying the substitution{x ↦h(a,y),z ↦b } to the term
| yields | |||||
If a term has an instance equivalent to a term, that is, if for some substitution, then is calledmore general than, and is calledmore special than, orsubsumed by,. For example, is more general than if ⊕ iscommutative, since then.
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 calledvariants, orrenamings of each other.For example,is a variant of,sinceandHowever, isnot a variant of, 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, a term may be both more general and more special than a structurally different term.For example, if ⊕ isidempotent, that is, if always, then the term is more general than,[note 2] and vice versa,[note 3] although and are of different structure.
A substitution ismore special than, orsubsumed by, a substitution if is subsumed by for each term. We also say that is more general than. More formally, take a nonempty infinite set of auxiliary variables such that no equation in the unification problem contains variables from. Then a substitution is subsumed by another substitution if there is a substitution such that for all terms,.[2]For instance is subsumed by, using, but is not subsumed by, as is not an instance of.[3]
A substitution σ is asolution of the unification problemE ifliσ ≡riσ for. Such a substitution is also called aunifier ofE.For example, if ⊕ isassociative, the unification problem {x ⊕a ≐a ⊕x } has the solutions {x ↦a}, {x ↦a ⊕a}, {x ↦a ⊕a ⊕a}, etc., while the problem {x ⊕a ≐a } has no solution.
For a given unification problemE, a setS of unifiers is calledcomplete if each solution substitution is subsumed by some substitution inS. A complete substitution set always exists (e.g. the set of all solutions), but in some frameworks (such as unrestricted higher-order unification) the problem of determining whether any solution exists (i.e., whether the complete substitution set is nonempty) is undecidable.
The setS is calledminimal if none of its members subsumes another one. Depending on the framework, a complete and minimal substitution set may have zero, one, finitely many, or infinitely many members, or may not exist at all due to an infinite chain of redundant members.[4] Thus, in general, unification algorithms compute a finite approximation of the complete set, which may or may not be minimal, although most algorithms avoid redundant unifiers when possible.[2] For first-order syntactical unification, Martelli and Montanari[5] gave an algorithm that reports unsolvability or computes a single unifier that by itself forms a complete and minimal substitution set, called themost general unifier.
Syntactic unification of first-order terms is the most widely used unification framework.It is based onT being the set offirst-order terms (over some given setV of variables,C of constants andFn ofn-ary function symbols) and on ≡ beingsyntactic equality.In this framework, each solvable unification problem{l1 ≐r1, ...,ln ≐rn} has a complete, and obviously minimal,singleton solution set{σ}.Its memberσ is called themost 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.l1σ =r1σ ∧ ... ∧lnσ =rnσ.Any unifier of the problem is subsumed[note 4] by the mguσ.The mgu is unique up to variants: ifS1 andS2 are both complete and minimal solution sets of the same syntactical unification problem, thenS1 = {σ1 } andS2 = {σ2 } for some substitutionsσ1 andσ2, andxσ1 is a variant ofxσ2 for each variablex occurring in the problem.
For example, the unification problem {x ≐z,y ≐f(x) } has a unifier {x ↦z,y ↦f(z) }, because
| x | {x ↦z,y ↦f(z) } | = | z | = | z | {x ↦z,y ↦f(z) } | , and |
| y | {x ↦z,y ↦f(z) } | = | f(z) | = | 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(x1),y ↦f(f(x1)),z ↦f(x1) }, {x ↦f(f(x1)),y ↦f(f(f(x1))),z ↦f(f(x1)) }, and so on; there are infinitely many similar unifiers.
As another example, the problemg(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 outermostg andf, respectively, and terms with different outermost function symbols are syntactically different.
Symbols are ordered such that variables precede function symbols.Terms are ordered by increasing written length; equally long terms are orderedlexicographically.[6] For a setT of terms, its disagreement pathp is the lexicographically least path where two member terms ofT differ. Its disagreement set is the set ofsubterms starting atp, formally:{t|p :t ∈T}.[7]
Algorithm:[8]
Given a setT of terms to be unifiedLetσ initially be theidentity substitutiondo forever ifTσ is asingleton set then returnσ fi letD be the disagreement set ofTσ lets,t be the two lexicographically least terms inD ifs is not a variable ors occurs int then return "NONUNIFIABLE" fi done
Jacques Herbrand discussed the basic concepts of unification and sketched an algorithm in 1930.[9][10][11] But most authors attribute the first unification algorithm toJohn Alan Robinson (cf. box).[12][13][note 5] Robinson's algorithm had worst-case exponential behavior in both time and space.[11][15] Numerous authors have proposed more efficient unification algorithms.[16] Algorithms with worst-case linear-time behavior were discovered independently byMartelli & Montanari (1976) andPaterson & Wegman (1976)[note 6]Baader & Snyder (2001) uses a similar technique as Paterson-Wegman, hence is linear,[17] 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 aDAG representation.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 anobject-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 programmaticobjects provides opportunities for optimizing other logic operations as well.[15]
The following algorithm is commonly presented and originates fromMartelli & Montanari (1982).[note 7] Given a finite set of potential equations,the algorithm applies rules to transform it to an equivalent set of equations of the form{x1 ≐u1, ...,xm ≐um }wherex1, ...,xm are distinct variables andu1, ...,um are terms containing none of thexi.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 variablex in problemG with termt is denotedG {x ↦t}.For simplicity, constant symbols are regarded as function symbols having zero arguments.
| delete | |||||
| decompose | |||||
| if or | conflict | ||||
| swap | |||||
| if and | eliminate[note 8] | ||||
| if | check |
An attempt to unify a variablex with a term containingx as a strict subtermx ≐f(...,x, ...) would lead to an infinite term as solution forx, sincex would occur as a subterm of itself.In the set of (finite) first-order terms as defined above, the equationx ≐f(...,x, ...) has no solution; hence theeliminate rule may only be applied ifx ∉vars(t).Since that additional check, calledoccurs 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.
For the proof of termination of the algorithm consider a triplewherenvar is the number of variables that occur more than once in the equation set,nlhs is the number of function symbols and constantson the left hand sides of potential equations, andneqn is the number of equations.When ruleeliminate is applied,nvar decreases, sincex is eliminated fromG and kept only in {x ≐t }.Applying any other rule can never increasenvar again.When ruledecompose,conflict, orswap is applied,nlhs decreases, since at least the left hand side's outermostf disappears.Applying any of the remaining rulesdelete orcheck can't increasenlhs, but decreasesneqn.Hence, any rule application decreases the triple with respect to thelexicographical order, which is possible only a finite number of times.
Conor McBride observes[18] that "by expressing the structure which unification exploits" in adependently typed language such asEpigram,Robinson's unification algorithm can be maderecursive on the number of variables, in which case a separate termination proof becomes unnecessary.
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 logicaland operator.Formathematical notation,x,y,z are used as variables,f,g as function symbols, anda,b as constants.
| Prolog notation | Mathematical notation | Unifying substitution | Explanation |
|---|---|---|---|
a = a | {a =a } | {} | Succeeds. (tautology) |
a = b | {a =b } | ⊥ | a andb do not match |
X = X | {x =x } | {} | Succeeds. (tautology) |
a = X | {a =x } | {x ↦a } | x is unified with the constanta |
X = Y | {x =y } | {x ↦y } | x andy are aliased |
f(a,X) = f(a,b) | {f(a,x) =f(a,b) } | {x ↦b } | function and constant symbols match,x is unified with the constantb |
f(a) = g(a) | {f(a) =g(a) } | ⊥ | f andg do not match |
f(X) = f(Y) | {f(x) =f(y) } | {x ↦y } | x andy are aliased |
f(X) = g(Y) | {f(x) =g(y) } | ⊥ | f andg do not match |
f(X) = f(Y,Z) | {f(x) =f(y,z) } | ⊥ | Fails. Thef function symbols have different arity |
f(g(X)) = f(Y) | {f(g(x)) =f(y) } | {y ↦g(x) } | Unifiesy with the term |
f(g(X),X) = f(Y,a) | {f(g(x),x) =f(y,a) } | {x ↦a,y ↦g(a) } | Unifiesx with constanta, andy with the term |
X = f(X) | {x =f(x) } | should be ⊥ | Returns ⊥ in first-order logic and many modern Prolog dialects (enforced by theoccurs check). Succeeds in traditional Prolog and in Prolog II, unifyingx with infinite term |
X = Y, Y = a | {x =y,y =a } | {x ↦a,y ↦a } | Bothx andy are unified with the constanta |
a = Y, X = Y | {a =y,x =y } | {x ↦a,y ↦a } | As above (order of equations in set doesn't matter) |
X = a, b = X | {x =a,b =x } | ⊥ | Fails.a andb do not match, sox can't be unified with both |
The most general unifier of a syntactic first-order unification problem ofsizen may have a size of2n. For example, the problem has the most general unifier, cf. picture. In order to avoid exponential time complexity caused by such blow-up, advanced unification algorithms work ondirected acyclic graphs (dags) rather than trees.[19]
The concept of unification is one of the main ideas behindlogic programming. Specifically, unification is a basic building block ofresolution, a rule of inference for determining formula satisfiability. InProlog, the equality symbol= 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:
+,-,*,/, are not evaluated by=. So for example1+2 = 3 is not satisfiable because they are syntactically different. The use of integer arithmetic constraints#= introduces a form of E-unification for which these operations are interpreted and evaluated.[20]Type inference algorithms are typically based on unification, particularlyHindley-Milner type inference which is used by the functional languagesHaskell andML. For example, when attempting to infer the type of the Haskell expressionTrue : ['x'], the compiler will use the typea -> [a] -> [a] of the list construction function(:), the typeBool of the first argumentTrue, and the type[Char] of the second argument['x']. The polymorphic type variablea will be unified withBool and the second argument[a] will be unified with[Char].a cannot be bothBool andChar at the same time, therefore this expression is not correctly typed.
Like for Prolog, an algorithm for type inference can be given:
Unification has been used in different research areas of computational linguistics.[21][22]
Order-sorted logic allows one to assign asort, ortype, to each term, and to declare a sorts1 asubsort of another sorts2, commonly written ass1 ⊆s2. For example, when reаsoning about biological creatures, it is useful to declare a sortdog to be a subsort of a sortanimal. Wherever a term of some sorts is required, a term of any subsort ofs may be supplied instead.For example, assuming a function declarationmother:animal →animal, and a constant declarationlassie:dog, the termmother(lassie) is perfectly valid and has the sortanimal. In order to supply the information that the mother of a dog is a dog in turn, another declarationmother:dog →dog may be issued; this is calledfunction overloading, similar tooverloading in programming languages.
Walther gave a unification algorithm for terms in order-sorted logic, requiring for any two declared sortss1,s2 their intersections1 ∩s2 to be declared, too: ifx1 andx2 is a variable of sorts1 ands2, respectively, the equationx1 ≐x2 has the solution {x1 =x,x2 =x }, wherex:s1 ∩s2.[23]After incorporating this algorithm into a clause-based automated theorem prover, he could solve a benchmark problem by translating it into order-sorted logic, thereby boiling it down an order of magnitude, as many unary predicates turned into sorts.
Smolka generalized order-sorted logic to allow forparametric polymorphism.[24]In his framework, subsort declarations are propagated to complex type expressions.As a programming example, a parametric sortlist(X) may be declared (withX being a type parameter as in aC++ template), and from a subsort declarationint ⊆float the relationlist(int) ⊆list(float) is automatically inferred, meaning that each list of integers is also a list of floats.
Schmidt-Schauß generalized order-sorted logic to allow for term declarations.[25]As an example, assuming subsort declarationseven ⊆int andodd ⊆int, a term declaration like ∀i :int. (i +i) :even allows to declare a property of integer addition that could not be expressed by ordinary overloading.
![[icon]](/mt/?noimg=&dark=on&url=https%3a%2f%2fen.wikipedia.org%2fwiki%2fFile%3aWiki_letter_w_cropped.svg) | This sectionneeds expansion. You can help byadding to it.(December 2021) |
Background on infinite trees:
Unification algorithm, Prolog II:
Applications:
E-unification is the problem of finding solutions to a given set ofequations,taking into account some equational background knowledgeE.The latter is given as a set of universalequalities.For some particular setsE, equation solvingalgorithms (a.k.a.E-unification algorithms) have been devised;for others it has been proven that no such algorithms can exist.
For example, ifa andb are distinct constants,theequation has no solutionwith respect to purelysyntactic unification,where nothing is known about the operator.However, if the is known to becommutative,then the substitution{x ↦b,y ↦a} solves the above equation,since
| | {x ↦b,y ↦a} | ||
| = | | bysubstitution application | |
| = | | by commutativity of | |
| = | | {x ↦b,y ↦a} | by (converse) substitution application |
The background knowledgeE could state the commutativity of by the universal equality" for allu,v".
| ∀u,v,w: | | = | | A | Associativity of |
| ∀u,v: | | = | | C | Commutativity of |
| ∀u,v,w: | | = | | Dl | Left distributivity of over |
| ∀u,v,w: | | = | | Dr | Right distributivity of over |
| ∀u: | | = | u | I | Idempotence of |
| ∀u: | | = | u | Nl | Left neutral elementn with respect to |
| ∀u: | | = | u | Nr | Right neutral elementn with respect to |
It is said thatunification is decidable for a theory, if a unification algorithm has been devised for it that terminates forany input problem.It is said thatunification issemi-decidable for a theory, if a unification algorithm has been devised for it that terminates for anysolvable input problem, but may keep searching forever for solutions of an unsolvable input problem.
Unification is decidable for the following theories:
Unification is semi-decidable for the following theories:
If there is aconvergent term rewriting systemR available forE,theone-sided paramodulation algorithm[37]can be used to enumerate all solutions of given equations.
| G ∪ {f(s1,...,sn) ≐f(t1,...,tn) } | ;S | ⇒ | G ∪ {s1 ≐t1, ...,sn ≐tn } | ;S | decompose | |
| G ∪ {x ≐t } | ;S | ⇒ | G {x ↦t } | ;S{x↦t} ∪ {x↦t} | if the variablex doesn't occur int | eliminate |
| G ∪ {f(s1,...,sn) ≐t } | ;S | ⇒ | G ∪ {s1 ≐ u1, ...,sn ≐ un,r ≐t } | ;S | iff(u1,...,un) →r is a rule fromR | mutate |
| G ∪ {f(s1,...,sn) ≐y } | ;S | ⇒ | G ∪ {s1 ≐y1, ...,sn ≐yn,y ≐f(y1,...,yn) } | ;S | ify1,...,yn are new variables | imitate |
Starting withG being the unification problem to be solved andS being the identity substitution, rules are applied nondeterministically until the empty set appears as the actualG, in which case the actualS is a unifying substitution. Depending on the order the paramodulation rules are applied, on the choice of the actual equation fromG, and on the choice ofR's rules inmutate, different computations paths are possible. Only some lead to a solution, while others end at aG ≠ {} where no further rule is applicable (e.g.G = {f(...) ≐g(...) }).
| 1 | app(nil,z) | →z |
| 2 | app(x.y,z) | →x.app(y,z) |
For an example, a term rewrite systemR is used defining theappend operator of lists built fromcons andnil; wherecons(x,y) is written in infix notation asx.y for brevity; e.g.app(a.b.nil,c.d.nil) →a.app(b.nil,c.d.nil) →a.b.app(nil,c.d.nil) →a.b.c.d.nil demonstrates the concatenation of the listsa.b.nil andc.d.nil, employing the rewrite rule 2,2, and 1. The equational theoryE corresponding toR is thecongruence closure ofR, both viewed as binary relations on terms.For example,app(a.b.nil,c.d.nil) ≡a.b.c.d.nil ≡app(a.b.c.d.nil,nil). The paramodulation algorithm enumerates solutions to equations with respect to thatE when fed with the exampleR.
A successful example computation path for the unification problem {app(x,app(y,x)) ≐a.a.nil } is shown below. To avoid variable name clashes, rewrite rules are consistently renamed each time before their use by rulemutate;v2,v3, ... are computer-generated variable names for this purpose. In each line, the chosen equation fromG is highlighted in red. Each time themutate rule is applied, the chosen rewrite rule (1 or2) is indicated in parentheses. From the last line, the unifying substitutionS = {y ↦nil,x ↦a.nil } can be obtained. In fact,app(x,app(y,x)) {y↦nil,x↦a.nil } =app(a.nil,app(nil,a.nil)) ≡app(a.nil,a.nil) ≡a.app(nil,a.nil) ≡a.a.nil solves the given problem.A second successful computation path, obtainable by choosing "mutate(1), mutate(2), mutate(2), mutate(1)" leads to the substitutionS = {y ↦a.a.nil,x ↦nil }; it is not shown here. No other path leads to a success.
| Used rule | G | S | |
|---|---|---|---|
| {app(x,app(y,x)) ≐a.a.nil } | {} | ||
| mutate(2) | ⇒ | {x ≐v2.v3,app(y,x) ≐v4,v2.app(v3,v4) ≐a.a.nil } | {} |
| decompose | ⇒ | {x ≐v2.v3,app(y,x) ≐v4,v2 ≐a,app(v3,v4) ≐a.nil } | {} |
| eliminate | ⇒ | {app(y,v2.v3) ≐v4,v2 ≐a,app(v3,v4) ≐a.nil } | {x ↦v2.v3 } |
| eliminate | ⇒ | {app(y,a.v3) ≐v4,app(v3,v4) ≐a.nil } | {x ↦a.v3 } |
| mutate(1) | ⇒ | {y ≐nil,a.v3 ≐v5,v5 ≐v4,app(v3,v4) ≐a.nil } | {x ↦a.v3 } |
| eliminate | ⇒ | {y ≐nil,a.v3 ≐v4,app(v3,v4) ≐a.nil } | {x ↦a.v3 } |
| eliminate | ⇒ | {a.v3 ≐v4,app(v3,v4) ≐a.nil } | {y ↦nil,x ↦a.v3 } |
| mutate(1) | ⇒ | {a.v3 ≐v4,v3 ≐nil,v4 ≐v6,v6 ≐a.nil } | {y ↦nil,x ↦a.v3 } |
| eliminate | ⇒ | {a.v3 ≐v4,v3 ≐nil,v4 ≐a.nil } | {y ↦nil,x ↦a.v3 } |
| eliminate | ⇒ | {a.nil ≐v4,v4 ≐a.nil } | {y ↦nil,x ↦a.nil } |
| eliminate | ⇒ | {a.nil ≐a.nil } | {y ↦nil,x ↦a.nil } |
| decompose | ⇒ | {a ≐a,nil ≐nil } | {y ↦nil,x ↦a.nil } |
| decompose | ⇒ | {nil ≐nil } | {y ↦nil,x ↦a.nil } |
| decompose | ⇒ | {} | {y ↦nil,x ↦a.nil } |
IfR is aconvergent term rewriting system forE,an approach alternative to the previous section consists in successive application of "narrowing steps";this will eventually enumerate all solutions of a given equation.A narrowing step (cf. picture) consists in
Formally, ifl →r is arenamed copy of a rewrite rule fromR, having no variables in common with a terms, and thesubterms|p is not a variable and is unifiable withl via themguσ, thens can benarrowed to the termt =sσ[rσ]p, i.e. to the termsσ, with the subterm atpreplaced byrσ. The situation thats can be narrowed tot is commonly denoted ass ↝t.Intuitively, a sequence of narrowing stepst1 ↝t2 ↝ ... ↝tn can be thought of as a sequence of rewrite stepst1 →t2 → ... →tn, but with the initial termt1 being further and further instantiated, as necessary to make each of the used rules applicable.
Theabove example paramodulation computation corresponds to the following narrowing sequence ("↓" indicating instantiation here):
| app( | x | ,app(y, | x | )) | |||||||||||||
| ↓ | ↓ | x ↦v2.v3 | |||||||||||||||
| app( | v2.v3 | ,app(y, | v2.v3 | )) | → | v2.app(v3,app( | y | ,v2.v3)) | |||||||||
| ↓ | y ↦nil | ||||||||||||||||
| v2.app(v3,app( | nil | ,v2.v3)) | → | v2.app( | v3 | ,v2. | v3 | ) | |||||||||
| ↓ | ↓ | v3 ↦nil | |||||||||||||||
| v2.app( | nil | ,v2. | nil | ) | → | v2.v2.nil |
The last term,v2.v2.nil can be syntactically unified with the original right hand side terma.a.nil.
Thenarrowing lemma[38] ensures that whenever an instance of a terms can be rewritten to a termt by a convergent term rewriting system, thens andt can be narrowed and rewritten to a terms′ andt′, respectively, such thatt′ is an instance ofs′.
Formally: wheneversσ→∗t holds for some substitution σ, then there exist termss′,t′ such thats↝∗s′ andt→∗t′ ands′τ =t′ for some substitution τ.
Many applications require one to consider the unification of typed lambda-terms instead of first-order terms. Such unification is often calledhigher-order unification. Higher-order unification isundecidable,[39][40][41] 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 isf, has thesolutions {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 asemi-decidable (pre-)unification algorithm[42] that allows a systematic search of the space of unifiers (generalizing the unification algorithm of Martelli-Montanari[5] with rules for terms containing higher-order variables) that seems to work sufficiently well in practice. Huet[43] and Gilles Dowek[44] 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,[45] is another such subset. The higher-order logic programming languagesλProlog andTwelf 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.[46] The Zipperposition theorem prover has an algorithm integrating these well-behaved subsets into a full higher-order unification algorithm.[2]
In computational linguistics, one of the most influential theories ofelliptical 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 like(j,m) ∧ R(p) and the value of R (the semantic representation of the ellipsis) is determined by the equation like(j,m) = R(j). The process of solving such equations is called Higher-Order Unification.[47]
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.[48]
{{cite book}}: CS1 maint: multiple names: authors list (link)