Unification (computer science)
From Wikipedia, the free encyclopedia
In logic and computer science, unification is an algorithmic process of solving equations between symbolic expressions. For example, using x,y,z as variables, the singleton equation set { cons(x,cons(x,nil)) = cons(2,y) } is a syntactic first-order unification problem that has the substitution { x ↦ 2, y ↦ cons(2,nil) } as its only solution.
A unification algorithm was first discovered by Jacques Herbrand,^{[1]}^{[2]}^{[3]} while a first formal investigation can be attributed to John Alan Robinson,^{[4]}^{[5]} who used first-order syntactical unification as a basic building block of his 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. Today, automated reasoning is still the main application area of unification. Syntactical first-order unification is used in logic programming and programming language type system implementation, especially in Hindley–Milner based type inference algorithms. Semantic unification is used in SMT solvers, term rewriting algorithms and cryptographic protocol analysis. Higher-order unification is used in proof assistants, for example Isabelle and Twelf, and restricted forms of higher-order unification (higher-order pattern unification) are used in some programming language implementations, such as lambdaProlog, as higher-order patterns are expressive, yet their associated unification procedure retains theoretical properties closer to first-order unification.
Formal definition
A unification problem is a finite set Template:Math of equations to solve, where Template:Math are in the set Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle T} of terms or expressions. 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 representing functions, are allowed in an expression, the process is called higher-order unification, otherwise first-order unification. If a solution is required to make both sides of each equation literally equal, the process is called syntactic or free unification, otherwise semantic or equational unification, or E-unification, or unification 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 the pattern.^{[6]}
Prerequisites
Formally, a unification approach presupposes
- An infinite set Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle V} of variables. For higher-order unification, it is convenient to choose Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle V} disjoint from the set of lambda-term bound variables.
- A set Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle T} of terms such that Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle V \subseteq T} . For first-order unification, Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle T} is usually the set of first-order terms (terms built from variable and function symbols). For higher-order unification Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle T} consists of first-order terms and lambda terms (terms containing some higher-order variables).
- A mapping vars: Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle T \rightarrow} Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbb{P}} Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle (V)} , assigning to each term Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t} the set Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \text{vars}(t) \subsetneq V} of free variables occurring in Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t} .
- A theory or equivalence relation Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \equiv} on Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle T} , indicating which terms are considered equal. For first-order E-unification, Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \equiv} reflects the background knowledge about certain function symbols; for example, if Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \oplus} is considered commutative, Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t\equiv u} if Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle u} results from Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t} by swapping the arguments of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \oplus} at some (possibly all) occurrences. ^{[note 1]} 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 sentences, or the background knowledge, is empty), the theory of uninterpreted functions (because unification is done on uninterpreted terms), or the theory of constructors (because all function symbols just build up data terms, rather than operating on them). For higher-order unification, usually Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t\equiv u} if Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t} and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle u} 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 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) }.
Substitution
A substitution is a mapping Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \sigma: V\rightarrow T} from variables to terms; the notation Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \{x_1\mapsto t_1, ..., x_k \mapsto t_k\}} refers to a substitution mapping each variable Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x_i} to the term Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t_i} , for Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle i=1,...,k} , and every other variable to itself; the Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x_i} must be pairwise distinct. Applying that substitution to a term Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t} is written in postfix notation as Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t \{x_1 \mapsto t_1, ..., x_k \mapsto t_k\}} ; it means to (simultaneously) replace every occurrence of each variable Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x_i} in the term Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t} by Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t_i} . The result Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t\tau} of applying a substitution Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \tau} to a term Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t} is called an instance of that term Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t} . As a first-order example, applying the substitution Template:Math to the term
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle f(} | Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \textbf{x}} | Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle , a, g(} | Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \textbf{z}} | Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle ), y)} | |
yields | |||||
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle f(} | Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \textbf{h}(\textbf{a}, \textbf{y})} | Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle , a, g(} | Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \textbf{b}} | Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle ), y).} |
Generalization, specialization
If a term Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t} has an instance equivalent to a term , that is, if for some substitution , then is called more general than , and is called more special than, or subsumed by, . For example, is more general than if ⊕ is commutative, 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 called variants, or renamings of each other. For example, is a variant of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle f(x_{2},a,g(z_{2}),y_{2})} , since
For arbitrary , a term may be both more general and more special than a structurally different term. For example, if ⊕ is idempotent, that is, if always Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x\oplus x\equiv x} , then the term Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x\oplus y} is more general than Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle z} ,^{[note 2]} and vice versa,^{[note 3]} although Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x\oplus y} and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle z} are of different structure.
A substitution Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \sigma } is more special than, or subsumed by, a substitution Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \tau } if Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t\sigma } is subsumed by Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t\tau } for each term Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t} . We also say that Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \tau } is more general than Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \sigma } . More formally, take a nonempty infinite set Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle V} of auxiliary variables such that no equation Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle l_{i}\doteq r_{i}} in the unification problem contains variables from Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle V} . Then a substitution Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \sigma } is subsumed by another substitution Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \tau } if there is a substitution Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \theta} such that for all terms Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle X\notin V} , Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle X\sigma \equiv X\tau\theta} .^{[7]} For instance Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \{x \mapsto a, y \mapsto a \}} is subsumed by Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \tau = \{x\mapsto y\}} , using Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \theta=\{y\mapsto a\}} , but Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \sigma = \{x\mapsto a\}} is not subsumed by Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \tau = \{x\mapsto y\}} , as Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle f(x, y)\sigma = f(a, y)} is not an instance of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle f(x, y) \tau = f(y, y)} .^{[8]}
Solution set
A substitution σ is a solution of the unification problem E if Template:Math for Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle i = 1, ..., n} . Such a substitution is also called a unifier of E. For example, if ⊕ is associative, 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 problem E, a set S of unifiers is called complete if each solution substitution is subsumed by some substitution in S. 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 set S is called minimal 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.^{[9]} 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.^{[7]} For first-order syntactical unification, Martelli and Montanari^{[10]} gave an algorithm that reports unsolvability or computes a single unifier that by itself forms a complete and minimal substitution set, called the most general unifier.
Syntactic unification of first-order terms
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_{n} of n-ary function symbols) and on ≡ being syntactic equality. In this framework, each solvable unification problem Template:Math has a complete, and obviously minimal, singleton solution set Template:Math. Its member Template: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. Template:Math. Any unifier of the problem is subsumed^{[note 4]} by the mgu Template:Mvar. The mgu is unique up to variants: if S_{1} and S_{2} are both complete and minimal solution sets of the same syntactical unification problem, then S_{1} = { σ_{1} } and S_{2} = { σ_{2} } for some substitutions Template:Math and Template:Math and Template:Math is a variant of Template:Math 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
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(x_{1}), y ↦ f(f(x_{1})), z ↦ f(x_{1}) }, { x ↦ f(f(x_{1})), y ↦ f(f(f(x_{1}))), z ↦ f(f(x_{1})) }, 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.
A unification algorithm
Page Template:Quote box/styles.css has no content.
Symbols are ordered such that variables precede function symbols. Terms are ordered by increasing written length; equally long terms are ordered lexicographically.Template:Refn 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: Template:Math}.Template:Refn
Algorithm:Template:Refn
Given a set T of terms to be unified
Let Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \sigma} initially be the identity substitution
do forever
if
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle T\sigma} is a singleton setthen
return
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \sigma}
fi
let D be the disagreement set of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle T\sigma}
let s, t be the two lexicographically least terms in D
if
s is not a variableor
s occurs in tthen
return
"NONUNIFIABLE"
fi
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \sigma := \sigma \{ s \mapsto t \}}
done
The first algorithm given by Robinson (1965) was rather inefficient; cf. box. The following faster algorithm originated from Martelli, Montanari (1982).^{[note 5]} This paper also lists preceding attempts to find an efficient syntactical unification algorithm,^{[11]}^{[12]}^{[13]}^{[14]}^{[15]}^{[16]} and states that linear-time algorithms were discovered independently by Martelli, Montanari (1976)^{[13]} and Paterson, Wegman (1976,^{[17]} 1978^{[14]}).Template:Refn
Given a finite set of potential equations, the algorithm applies rules to transform it to an equivalent set of equations of the form { x_{1} ≐ u_{1}, ..., x_{m} ≐ u_{m} } where x_{1}, ..., x_{m} are distinct variables and u_{1}, ..., u_{m} are terms containing none of the x_{i}. 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.
delete decompose if or conflict swap if and eliminate^{[note 6]} if check
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 where Template:Math is the number of variables that occur more than once in the equation set, Template:Math is the number of function symbols and constants on the left hand sides of potential equations, and Template:Math is the number of equations. When rule eliminate is applied, Template:Math decreases, since x is eliminated from G and kept only in { x ≐ t }. Applying any other rule can never increase Template:Math again. When rule decompose, conflict, or swap is applied, Template:Math decreases, since at least the left hand side's outermost f disappears. Applying any of the remaining rules delete or check can't increase Template:Math, but decreases Template:Math. Hence, any rule application decreases the triple with respect to the lexicographical order, which is possible only a finite number of times.
Conor McBride observes^{[18]} that "by expressing the structure which unification exploits" in a dependently typed language such as 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.
Prolog notation | Mathematical notation | Unifying substitution | Explanation |
---|---|---|---|
a = a |
{ a = a } | {} | Succeeds. (tautology) |
a = b |
{ a = b } | ⊥ | a and b do not match |
X = X |
{ x = x } | {} | Succeeds. (tautology) |
a = X |
{ a = x } | { x ↦ a } | x is unified with the constant a |
X = Y |
{ x = y } | { x ↦ y } | x and y 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 constant b |
f(a) = g(a) |
{ f(a) = g(a) } | ⊥ | f and g do not match |
f(X) = f(Y) |
{ f(x) = f(y) } | { x ↦ y } | x and y are aliased |
f(X) = g(Y) |
{ f(x) = g(y) } | ⊥ | f and g do not match |
f(X) = f(Y,Z) |
{ f(x) = f(y,z) } | ⊥ | Fails. The f function symbols have different arity |
f(g(X)) = f(Y) |
{ f(g(x)) = f(y) } | { y ↦ g(x) } | Unifies y with the term Template:Tmath |
f(g(X),X) = f(Y,a) |
{ f(g(x),x) = f(y,a) } | { x ↦ a, y ↦ g(a) } | Unifies x with constant a, and y with the term Template:Tmath |
X = f(X) |
{ 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 |
X = Y, Y = a |
{ x = y, y = a } | { x ↦ a, y ↦ a } | Both x and y are unified with the constant a |
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 and b do not match, so x can't be unified with both |
The most general unifier of a syntactic first-order unification problem of size Template:Mvar may have a size of Template:Math. For example, the problem Template:Tmath has the most general unifier Template:Tmath, cf. picture. In order to avoid exponential time complexity caused by such blow-up, advanced unification algorithms work on directed acyclic graphs (dags) rather than trees.Template:Refn
Application: unification in logic programming
The concept of unification is one of the main ideas behind logic programming, best known through the language Prolog. It represents the mechanism of binding the contents of variables and can be viewed as a kind of one-time assignment. In Prolog, this operation is denoted by the equality symbol =
, but is also done when instantiating variables (see below). It is also used in other languages by the use of the equality symbol =
, but also in conjunction with many operations including +
, -
, *
, /
. Type inference algorithms are typically based on unification.
In Prolog:
- A 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.
Application: type inference
Unification is used during type inference for languages with type systems based on Hindley-Milner, including the functional languages Haskell and ML. On one hand, the programmer does not need to provide type information for every function, on the other hand it is used to detect typing errors. The Haskell expression True : ['x', 'y', 'z']
is not correctly typed. The list construction function (:)
is of type a -> [a] -> [a]
, and for the first argument True
the polymorphic type variable a
has to be unified with True
's type, Bool
. The second argument, ['x', 'y', 'z']
, is of type [Char]
, but a
cannot be both Bool
and Char
at the same time.
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
Unification has been used in different research areas of computational linguistics.^{[19]}^{[20]}
Order-sorted unification
Order-sorted logic allows one to assign a sort, or type, to each term, and to declare a sort s_{1} a subsort of another sort s_{2}, commonly written as s_{1} ⊆ s_{2}. For example, when reаsoning about biological creatures, it is useful to declare a sort dog to be a subsort of a sort animal. Wherever a term of some sort s is required, a term of any subsort of s may be supplied instead. For example, assuming a function declaration mother: animal → animal, and a constant declaration lassie: dog, the term mother(lassie) is perfectly valid and has the sort animal. In order to supply the information that the mother of a dog is a dog in turn, another declaration mother: dog → dog may be issued; this is called function overloading, similar to overloading in programming languages.
Walther gave a unification algorithm for terms in order-sorted logic, requiring for any two declared sorts s_{1}, s_{2} their intersection s_{1} ∩ s_{2} to be declared, too: if x_{1} and x_{2} is a variable of sort s_{1} and s_{2}, respectively, the equation x_{1} ≐ x_{2} has the solution { x_{1} = x, x_{2} = x }, where x: s_{1} ∩ s_{2}. ^{[21]} 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 for parametric polymorphism. ^{[22]} In his framework, subsort declarations are propagated to complex type expressions. As a programming example, a parametric sort list(X) may be declared (with X being a type parameter as in a C++ template), and from a subsort declaration int ⊆ float the relation list(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. ^{[23]} As an example, assuming subsort declarations even ⊆ int and odd ⊆ 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.
Unification of infinite terms
This section needs expansion. You can help by adding to it. (December 2021) |
Background on infinite trees:
- B. Courcelle (1983). "Fundamental Properties of Infinite Trees". Theoret. Comput. Sci. 25 (2): 95–169. doi:10.1016/0304-3975(83)90059-2.
- Michael J. Maher (Jul 1988). "Complete Axiomatizations of the Algebras of Finite, Rational and Infinite Trees". Proc. IEEE 3rd Annual Symp. on Logic in Computer Science, Edinburgh. pp. 348–357.
- Joxan Jaffar; Peter J. Stuckey (1986). "Semantics of Infinite Tree Logic Programming". Theoretical Computer Science. 46: 141–158. doi:10.1016/0304-3975(86)90027-7.
Unification algorithm, Prolog II:
- A. Colmerauer (1982). K.L. Clark; S.-A. Tarnlund (eds.). Prolog and Infinite Trees. Academic Press.
- Alain Colmerauer (1984). "Equations and Inequations on Finite and Infinite Trees". In ICOT (ed.). Proc. Int. Conf. on Fifth Generation Computer Systems. pp. 85–99.
Applications:
- Francis Giannesini; Jacques Cohen (1984). "Parser Generation and Grammar Manipulation using Prolog's Infinite Trees". Journal of Logic Programming. 1 (3): 253–265. doi:10.1016/0743-1066(84)90013-X.
E-unification
E-unification is the problem of finding solutions to a given set of equations, taking into account some equational background knowledge E. The latter is given as a set of universal equalities. For some particular sets E, equation solving algorithms (a.k.a. E-unification algorithms) have been devised; for others it has been proven that no such algorithms can exist.
For example, if Template:Mvar and Template:Mvar are distinct constants, the equation Template:Tmath has no solution with respect to purely syntactic unification, where nothing is known about the operator Template:Tmath. However, if the Template:Tmath is known to be commutative, then the substitution Template:Math solves the above equation, since
Template:Tmath Template:Math = Template:Tmath by substitution application = Template:Tmath by commutativity of Template:Tmath = Template:Tmath Template:Math by (converse) substitution application
The background knowledge E could state the commutativity of Template:Tmath by the universal equality "Template:Tmath for all Template:Math".
Particular background knowledge sets E
Template:Math | Template:Tmath | = | Template:Tmath | Template:Mvar | Associativity of Template:Tmath |
Template:Math | Template:Tmath | = | Template:Tmath | Template:Mvar | Commutativity of Template:Tmath |
Template:Math | Template:Tmath | = | Template:Tmath | Template:Mvar | Left distributivity of Template:Tmath over Template:Tmath |
Template:Math | Template:Tmath | = | Template:Tmath | Template:Mvar | Right distributivity of Template:Tmath over Template:Tmath |
Template:Math | Template:Tmath | = | Template:Mvar | Template:Mvar | Idempotence of Template:Tmath |
Template:Math | Template:Tmath | = | Template:Mvar | Template:Mvar | Left neutral element Template:Mvar with respect to Template:Tmath |
Template:Math | Template:Tmath | = | Template:Mvar | Template:Mvar | Right neutral element Template:Mvar with respect to Template:Tmath |
It is said that unification is decidable for a theory, if a unification algorithm has been devised for it that terminates for any input problem. It is said that unification is semi-decidable for a theory, if a unification algorithm has been devised for it that terminates for any solvable input problem, but may keep searching forever for solutions of an unsolvable input problem.
Unification is decidable for the following theories:
- Template:Mvar^{[24]}
- Template:Mvar,Template:Mvar^{[25]}
- Template:Mvar,Template:Mvar,Template:Mvar^{[26]}
- Template:Mvar,Template:Mvar,Template:Mvar^{[note 7]}^{[26]}
- Template:Mvar,Template:Mvar^{[27]}
- Template:Mvar,Template:MvarTemplate:MvarTemplate:Mvar (monoid)^{[28]}
- Template:Mvar^{[29]}
- Boolean rings^{[30]}^{[31]}
- Abelian groups, even if the signature is expanded by arbitrary additional symbols (but not axioms)^{[32]}
- K4 modal algebras^{[33]}
Unification is semi-decidable for the following theories:
- Template:Mvar,Template:MvarTemplate:MvarTemplate:Mvar^{[34]}
- Template:Mvar,Template:Mvar,Template:Mvar^{[note 7]}^{[35]}
- Commutative rings^{[32]}
One-sided paramodulation
If there is a convergent term rewriting system R available for E, the one-sided paramodulation algorithm^{[36]} can be used to enumerate all solutions of given equations.
G ∪ { f(s_{1},...,s_{n}) ≐ f(t_{1},...,t_{n}) } | ; S | ⇒ | G ∪ { s_{1} ≐ t_{1}, ..., s_{n} ≐ t_{n} } | ; S | decompose | |
G ∪ { x ≐ t } | ; S | ⇒ | G { x ↦ t } | ; S{x↦t} ∪ {x↦t} | if the variable x doesn't occur in t | eliminate |
G ∪ { f(s_{1},...,s_{n}) ≐ t } | ; S | ⇒ | G ∪ { s_{1} ≐ u_{1}, ..., s_{n} ≐ u_{n}, r ≐ t } | ; S | if f(u_{1},...,u_{n}) → r is a rule from R | mutate |
G ∪ { f(s_{1},...,s_{n}) ≐ y } | ; S | ⇒ | G ∪ { s_{1} ≐ y_{1}, ..., s_{n} ≐ y_{n}, y ≐ f(y_{1},...,y_{n}) } | ; S | if y_{1},...,y_{n} are new variables | imitate |
Starting with G being the unification problem to be solved and S being the identity substitution, rules are applied nondeterministically until the empty set appears as the actual G, in which case the actual S is a unifying substitution. Depending on the order the paramodulation rules are applied, on the choice of the actual equation from G, and on the choice of R's rules in mutate, different computations paths are possible. Only some lead to a solution, while others end at a G ≠ {} 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 system R is used defining the append operator of lists built from cons and nil; where cons(x,y) is written in infix notation as x.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 lists a.b.nil and c.d.nil, employing the rewrite rule 2,2, and 1. The equational theory E corresponding to R is the congruence closure of R, 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 that E when fed with the example R.
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 rule mutate; v_{2}, v_{3}, ... are computer-generated variable names for this purpose. In each line, the chosen equation from G is highlighted in red. Each time the mutate rule is applied, the chosen rewrite rule (1 or 2) is indicated in parentheses. From the last line, the unifying substitution S = { 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 substitution S = { 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 ≐ v_{2}.v_{3}, app(y,x) ≐ v_{4}, v_{2}.app(v_{3},v_{4}) ≐ a.a.nil } | {} |
decompose | ⇒ | { x ≐ v_{2}.v_{3}, app(y,x) ≐ v_{4}, v_{2} ≐ a, app(v_{3},v_{4}) ≐ a.nil } | {} |
eliminate | ⇒ | { app(y,v_{2}.v_{3}) ≐ v_{4}, v_{2} ≐ a, app(v_{3},v_{4}) ≐ a.nil } | { x ↦ v_{2}.v_{3} } |
eliminate | ⇒ | { app(y,a.v_{3}) ≐ v_{4}, app(v_{3},v_{4}) ≐ a.nil } | { x ↦ a.v_{3} } |
mutate(1) | ⇒ | { y ≐ nil, a.v_{3} ≐ v_{5}, v_{5} ≐ v_{4}, app(v_{3},v_{4}) ≐ a.nil } | { x ↦ a.v_{3} } |
eliminate | ⇒ | { y ≐ nil, a.v_{3} ≐ v_{4}, app(v_{3},v_{4}) ≐ a.nil } | { x ↦ a.v_{3} } |
eliminate | ⇒ | { a.v_{3} ≐ v_{4}, app(v_{3},v_{4}) ≐ a.nil } | { y ↦ nil, x ↦ a.v_{3} } |
mutate(1) | ⇒ | { a.v_{3} ≐ v_{4}, v_{3} ≐ nil, v_{4} ≐ v_{6}, v_{6} ≐ a.nil } | { y ↦ nil, x ↦ a.v_{3} } |
eliminate | ⇒ | { a.v_{3} ≐ v_{4}, v_{3} ≐ nil, v_{4} ≐ a.nil } | { y ↦ nil, x ↦ a.v_{3} } |
eliminate | ⇒ | { a.nil ≐ v_{4}, v_{4} ≐ 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 } |
Narrowing
If R is a convergent term rewriting system for E, 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
- choosing a nonvariable subterm of the current term,
- syntactically unifying it with the left hand side of a rule from R, and
- replacing the instantiated rule's right hand side into the instantiated term.
Formally, if Template:Math is a renamed copy of a rewrite rule from R, having no variables in common with a term s, and the subterm Template:Math is not a variable and is unifiable with Template:Mvar via the mgu Template:Mvar, then Template:Mvar can be narrowed to the term Template:Math, i.e. to the term Template:Mvar, with the subterm at p replaced by Template:Mvar. The situation that s can be narrowed to t is commonly denoted as s ↝ t. Intuitively, a sequence of narrowing steps t_{1} ↝ t_{2} ↝ ... ↝ t_{n} can be thought of as a sequence of rewrite steps t_{1} → t_{2} → ... → t_{n}, but with the initial term t_{1} being further and further instantiated, as necessary to make each of the used rules applicable.
The above example paramodulation computation corresponds to the following narrowing sequence ("↓" indicating instantiation here):
app( | x | ,app(y, | x | )) | |||||||||||||
↓ | ↓ | x ↦ v_{2}.v_{3} | |||||||||||||||
app( | v_{2}.v_{3} | ,app(y, | v_{2}.v_{3} | )) | → | v_{2}.app(v_{3},app( | y | ,v_{2}.v_{3})) | |||||||||
↓ | y ↦ nil | ||||||||||||||||
v_{2}.app(v_{3},app( | nil | ,v_{2}.v_{3})) | → | v_{2}.app( | v_{3} | ,v_{2}. | v_{3} | ) | |||||||||
↓ | ↓ | v_{3} ↦ nil | |||||||||||||||
v_{2}.app( | nil | ,v_{2}. | nil | ) | → | v_{2}.v_{2}.nil |
The last term, v_{2}.v_{2}.nil can be syntactically unified with the original right hand side term a.a.nil.
The narrowing lemma^{[37]} ensures that whenever an instance of a term s can be rewritten to a term t by a convergent term rewriting system, then s and t can be narrowed and rewritten to a term Template:Math and Template:Math, respectively, such that Template:Math is an instance of Template:Math.
Formally: whenever Template:Math holds for some substitution σ, then there exist terms Template:Math such that Template:Math and Template:Math and Template:Math for some substitution τ.
Higher-order unification
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,^{[38]}^{[39]}^{[40]} 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^{[41]} that allows a systematic search of the space of unifiers (generalizing the unification algorithm of Martelli-Montanari^{[10]} with rules for terms containing higher-order variables) that seems to work sufficiently well in practice. Huet^{[42]} and Gilles Dowek^{[43]} 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,^{[44]} 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.^{[45]} The Zipperposition theorem prover has an algorithm integrating these well-behaved subsets into a full higher-order unification algorithm.^{[7]}
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 Template:Math and the value of R (the semantic representation of the ellipsis) is determined by the equation Template:Math. The process of solving such equations is called Higher-Order Unification.^{[46]}
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.^{[47]}
See also
- Rewriting
- Admissible rule
- Explicit substitution in lambda calculus
- Mathematical equation solving
- Dis-unification: solving inequations between symbolic expression
- Anti-unification: computing a least general generalization (lgg) of two terms, dual to computing a most general instance (mgu)
- Subsumption lattice, a lattice having unification as meet and anti-unification as join
- Ontology alignment (use unification with semantic equivalence)
Notes
- ↑ E.g. a ⊕ (b ⊕ f(x)) ≡ a ⊕ (f(x) ⊕ b) ≡ (b ⊕ f(x)) ⊕ a ≡ (f(x) ⊕ b) ⊕ a
- ↑ since
- ↑ since Template:Math
- ↑ formally: each unifier τ satisfies Template:Math for some substitution ρ
- ↑ 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.
- ↑ 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 below.
- ↑ ^{a} ^{b} in the presence of equality Template:Mvar, equalities Template:Mvar and Template:Mvar are equivalent, similar for Template:Mvar and Template:Mvar
References
- ↑ 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.
- ↑ Template:Cite report Here: p.56
- ↑ Template:Cite thesis Here: p.96-97
- ↑ J.A. Robinson (Jan 1965). "A Machine-Oriented Logic Based on the Resolution Principle". Journal of the ACM. 12 (1): 23–41. doi:10.1145/321250.321253. S2CID 14389185.; Here: sect.5.8, p.32
- ↑ J.A. Robinson (1971). "Computational logic: The unification computation". Machine Intelligence. 6: 63–72.
- ↑ Dowek, Gilles (1 January 2001). "Higher-order unification and matching". Handbook of automated reasoning. Elsevier Science Publishers B. V. pp. 1009–1062. ISBN 978-0-444-50812-6. Archived from the original on 15 May 2019. Retrieved 15 May 2019.
- ↑ ^{a} ^{b} ^{c} Vukmirović, Petar; Bentkamp, Alexander; Nummelin, Visa (14 December 2021). "Efficient Full Higher-Order Unification". Logical Methods in Computer Science. 17 (4): 6919. arXiv:2011.09507. doi:10.46298/lmcs-17(4:18)2021.
- ↑ Apt, Krzysztof R. (1997). From logic programming to Prolog (1. publ ed.). London Munich: Prentice Hall. p. 24. ISBN 013230368X.
- ↑ Fages, François; Huet, Gérard (1986). "Complete Sets of Unifiers and Matchers in Equational Theories". Theoretical Computer Science. 43: 189–200. doi:10.1016/0304-3975(86)90175-1.
- ↑ ^{a} ^{b} Martelli, Alberto; Montanari, Ugo (Apr 1982). "An Efficient Unification Algorithm". ACM Trans. Program. Lang. Syst. 4 (2): 258–282. doi:10.1145/357162.357169. S2CID 10921306.
- ↑ Template:Cite report
- ↑ Template:Cite thesis
- ↑ ^{a} ^{b} Template:Cite report
- ↑ ^{a} ^{b} Michael Stewart Paterson and M.N. Wegman (Apr 1978). "Linear unification". J. Comput. Syst. Sci. 16 (2): 158–167. doi:10.1016/0022-0000(78)90043-0.
- ↑ J.A. Robinson (Jan 1976). "Fast unification". In Woodrow W. Bledsoe, Michael M. Richter (ed.). Proc. Theorem Proving Workshop Oberwolfach. Oberwolfach Workshop Report. Vol. 1976/3.Template:Dead link
- ↑ M. Venturini-Zilli (Oct 1975). "Complexity of the unification algorithm for first-order expressions". Calcolo. 12 (4): 361–372. doi:10.1007/BF02575754. S2CID 189789152.
- ↑ Paterson, M.S.; Wegman, M.N. (May 1976). Chandra, Ashok K.; Wotschke, Detlef; Friedman, Emily P.; Harrison, Michael A. (eds.). Linear unification. Proceedings of the eighth annual ACM Symposium on Theory of Computing (STOC). ACM. pp. 181–186. doi:10.1145/800113.803646.
- ↑ McBride, Conor (October 2003). "First-Order Unification by Structural Recursion". Journal of Functional Programming. 13 (6): 1061–1076. CiteSeerX 10.1.1.25.1516. doi:10.1017/S0956796803004957. ISSN 0956-7968. S2CID 43523380. Retrieved 30 March 2012.
- ↑ Jonathan Calder, Mike Reape, and Hank Zeevat,, 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.
- ↑ Graeme Hirst and David St-Onge, [1] Lexical chains as representations of context for the detection and correction of malapropisms, 1998.
- ↑ Walther, Christoph (1985). "A Mechanical Solution of Schubert's Steamroller by Many-Sorted Resolution" (PDF). Artif. Intell. 26 (2): 217–224. doi:10.1016/0004-3702(85)90029-3. Archived from the original (PDF) on 2011-07-08. Retrieved 2013-06-28.
- ↑ Smolka, Gert (Nov 1988). Logic Programming with Polymorphically Order-Sorted Types (PDF). Int. Workshop Algebraic and Logic Programming. LNCS. Vol. 343. Springer. pp. 53–70. doi:10.1007/3-540-50667-5_58.
- ↑ Schmidt-Schauß, Manfred (Apr 1988). Computational Aspects of an Order-Sorted Logic with Term Declarations. Lecture Notes in Artificial Intelligence (LNAI). Vol. 395. Springer.
- ↑ Gordon D. Plotkin, Lattice Theoretic Properties of Subsumption, Memorandum MIP-R-77, Univ. Edinburgh, Jun 1970
- ↑ Mark E. Stickel, A Unification Algorithm for Associative-Commutative Functions, Journal of the Association for Computing Machinery, vol.28, no.3, pp. 423–434, 1981
- ↑ ^{a} ^{b} F. Fages, Associative-Commutative Unification, J. Symbolic Comput., vol.3, no.3, pp. 257–275, 1987
- ↑ Franz Baader, Unification in Idempotent Semigroups is of Type Zero, J. Automat. Reasoning, vol.2, no.3, 1986
- ↑ J. Makanin, The Problem of Solvability of Equations in a Free Semi-Group, Akad. Nauk SSSR, vol.233, no.2, 1977
- ↑ F. Fages (1987). "Associative-Commutative Unification" (PDF). J. Symbolic Comput. 3 (3): 257–275. doi:10.1016/s0747-7171(87)80004-4. S2CID 40499266.
- ↑ Martin, U., Nipkow, T. (1986). "Unification in Boolean Rings". In Jörg H. Siekmann (ed.). Proc. 8th CADE. LNCS. Vol. 230. Springer. pp. 506–513.
{{cite book}}
: CS1 maint: multiple names: authors list (link) - ↑ A. Boudet; J.P. Jouannaud; M. Schmidt-Schauß (1989). "Unification of Boolean Rings and Abelian Groups". Journal of Symbolic Computation. 8 (5): 449–477. doi:10.1016/s0747-7171(89)80054-9.
- ↑ ^{a} ^{b} Baader and Snyder (2001), p. 486.
- ↑ F. Baader and S. Ghilardi, Unification in modal and description logics, Logic Journal of the IGPL 19 (2011), no. 6, pp. 705–730.
- ↑ P. Szabo, Unifikationstheorie erster Ordnung (First Order Unification Theory), Thesis, Univ. Karlsruhe, West Germany, 1982
- ↑ Jörg H. Siekmann, Universal Unification, Proc. 7th Int. Conf. on Automated Deduction, Springer LNCS vol.170, pp. 1–42, 1984
- ↑ N. Dershowitz and G. Sivakumar, Solving Goals in Equational Languages, Proc. 1st Int. Workshop on Conditional Term Rewriting Systems, Springer LNCS vol.308, pp. 45–55, 1988
- ↑ Fay (1979). "First-Order Unification in an Equational Theory". Proc. 4th Workshop on Automated Deduction. pp. 161–167.
- ↑ ^{a} ^{b} Warren D. Goldfarb (1981). "The Undecidability of the Second-Order Unification Problem". TCS. 13 (2): 225–230. doi:10.1016/0304-3975(81)90040-2.
- ↑ Gérard P. Huet (1973). "The Undecidability of Unification in Third Order Logic". Information and Control. 22 (3): 257–267. doi:10.1016/S0019-9958(73)90301-X.
- ↑ Claudio Lucchesi: The Undecidability of the Unification Problem for Third Order Languages (Research Report CSRR 2059; Department of Computer Science, University of Waterloo, 1972)
- ↑ Gérard Huet: A Unification Algorithm for typed Lambda-Calculus []
- ↑ Gérard Huet: Higher Order Unification 30 Years Later
- ↑ Gilles Dowek: Higher-Order Unification and Matching. Handbook of Automated Reasoning 2001: 1009–1062
- ↑ Miller, Dale (1991). "A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification" (PDF). Journal of Logic and Computation. 1 (4): 497–536. doi:10.1093/logcom/1.4.497.
- ↑ Libal, Tomer; Miller, Dale (May 2022). "Functions-as-constructors higher-order unification: extended pattern unification". Annals of Mathematics and Artificial Intelligence. 90 (5): 455–479. doi:10.1007/s10472-021-09774-y.
- ↑ Gardent, Claire; Kohlhase, Michael; Konrad, Karsten (1997). "A Multi-Level, Higher-Order Unification Approach to Ellipsis". Submitted to European Association for Computational Linguistics (EACL). CiteSeerX 10.1.1.55.9018.
- ↑ Wayne Snyder (Jul 1990). "Higher order E-unification". Proc. 10th Conference on Automated Deduction. LNAI. Vol. 449. Springer. pp. 573–587.
Further reading
- Franz Baader and Wayne Snyder (2001). "Unification Theory" Template:Webarchive. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, volume I, pages 447–533. Elsevier Science Publishers.Template:Dead link
- Gilles Dowek (2001). "Higher-order Unification and Matching" Template:Webarchive. In Handbook of Automated Reasoning.
- Franz Baader and Tobias Nipkow (1998). Term Rewriting and All That. Cambridge University Press.
- Franz Baader and Template:Ill (1993). "Unification Theory". In Handbook of Logic in Artificial Intelligence and Logic Programming.
- Jean-Pierre Jouannaud and Claude Kirchner (1991). "Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification". In Computational Logic: Essays in Honor of Alan Robinson.
- Nachum Dershowitz and Jean-Pierre Jouannaud, Rewrite Systems, in: Jan van Leeuwen (ed.), Handbook of Theoretical Computer Science, volume B Formal Models and Semantics, Elsevier, 1990, pp. 243–320
- Jörg H. Siekmann (1990). "Unification Theory". In Claude Kirchner (editor) Unification. Academic Press.
- Kevin Knight (Mar 1989). "Unification: A Multidisciplinary Survey" (PDF). ACM Computing Surveys. 21 (1): 93–124. CiteSeerX 10.1.1.64.8967. doi:10.1145/62029.62030. S2CID 14619034.
- Gérard Huet and Derek C. Oppen (1980). "Equations and Rewrite Rules: A Survey". Technical report. Stanford University.
- Raulefs, Peter; Siekmann, Jörg; Szabó, P.; Unvericht, E. (1979). "A short survey on the state of the art in matching and unification problems". ACM SIGSAM Bulletin. 13 (2): 14–20. doi:10.1145/1089208.1089210. S2CID 17033087.
- Claude Kirchner and Hélène Kirchner. Rewriting, Solving, Proving. In preparation.
- Pages with TemplateStyles errors
- Pages with math errors
- Pages with math render errors
- CS1: long volume value
- CS1 maint: multiple names: authors list
- Articles to be expanded from December 2021
- Articles with invalid date parameter in template
- All articles to be expanded
- Articles using small message boxes
- Unification (computer science)
- Automated theorem proving
- Logic programming
- Rewriting systems
- Logic in computer science
- Type theory