In logic and computer science, specifically automated reasoning, unification is an algorithmic process of solving equations between symbolic expressions, each of the form Left-hand side = Right-hand side. For example, using x,y as variables, and taking f to be an uninterpreted function, the singleton 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 over first-order terms and equivalence is syntactic. This version of unification has a unique "best" answer and is used in logic programming and programming language type system implementation, especially in Hindley–Milner based type inference algorithms. In higher-order unification, possibly restricted to higher-order pattern unification, terms may include lambda expressions, and equivalence is up to beta-reduction. This version is used in proof assistants and higher-order logic programming, for example Isabelle, Twelf, and lambdaProlog. 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 in SMT solvers, term rewriting algorithms, and cryptographic protocol analysis.
Formal definition A unification problem is a finite set of equations to solve, where are in the set 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.
Prerequisites Formally, a unification approach presupposes An infinite set of variables. For higher-order unification, it is convenient to choose disjoint from the set of lambda-term bound variables. A set of terms such that . For first-order unification, is usually the set of first-order terms (terms built from variable and function symbols). For higher-order unification consists of first-order terms and lambda terms (terms containing some higher-order variables). A mapping , assigning to each term the set of free variables occurring in . A theory or equivalence relation on , indicating which terms are considered equal. For first-order E-unification, reflects the background knowledge about certain function symbols; for example, if is considered commutative, if results from by swapping the arguments of at some (possibly all) occurrences. E.g. a ⊕ (b ⊕ f(x)) ≡ a ⊕ (f(x) ⊕ b) ≡ (b ⊕ f(x)) ⊕ a ≡ (f(x) ⊕ b) ⊕ a 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 if and 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 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 in Reverse Polish 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 an instance of that term . As a first-order example, applying the substitution to the term yields
Generalization, specialization If a term 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 , since
and
However, is not 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 ⊕ is idempotent, that is, if always , then the term is more general than ,since and vice versa,since although and are of different structure.
A substitution is more special than, or subsumed 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 , . For instance is subsumed by , using , but is not subsumed by , as is not an instance of .
Solution set
A substitution σ is a solution of the unification problem E if for . 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. 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. For first-order syntactical unification, Martelli and Montanari 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 Fn of n-ary function symbols) and on ≡ being syntactic equality. In this framework, each solvable unification problem has a complete, and obviously minimal, singleton solution set . Its member 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. . Any unifier of the problem is subsumedformally: each unifier τ satisfies for some substitution ρ by the mgu . The mgu is unique up to variants: if S1 and S2 are both complete and minimal solution sets of the same syntactical unification problem, then S1 = { σ1 } and S2 = { σ2 } for some substitutions and and is a variant of for each variable x occurring in the problem.
For example, the unification problem { x ≐ z, y ≐ f(x) } has a unifier { x ↦ z, y ↦ f(z) }, because
| align="right" | x | { x ↦ z, y ↦ f(z) }
| align="center" | z
| align="right" | z | { x ↦ z, y ↦ f(z) } |, and |- | align="right" | y | { x ↦ z, y ↦ f(z) }
| align="center" | f(z)
| align="right" | f(x) | { x ↦ z, y ↦ f(z) } | .
This is also the most general unifier. Other unifiers for the same problem are e.g. { x ↦ f(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 problem g(x,x) ≐ f(y) has no solution with respect to ≡ being literal identity, since any substitution applied to the left and right hand side will keep the outermost g and f, respectively, and terms with different outermost function symbols are syntactically different.
Unification algorithms
Jacques Herbrand discussed the basic concepts of unification and sketched an algorithm in 1930.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. Here: p.96-97 Here: p.56 But most authors attribute the first unification algorithm to John Alan Robinson (cf. box).; Here: sect.5.8, p.32 Robinson's algorithm had worst-case exponential behavior in both time and space. Numerous authors have proposed more efficient unification algorithms.Per :
Algorithms with worst-case linear-time behavior were discovered independently by and uses a similar technique as Paterson-Wegman, hence is linear, but like most linear-time unification algorithms is slower than the Robinson version on small sized inputs due to the overhead of preprocessing the inputs and postprocessing of the output, such as construction of a DAG representation. is also of linear complexity in the input size but is competitive with the Robinson algorithm on small size inputs. The speedup is obtained by using an object-oriented representation of the predicate calculus that avoids the need for pre- and post-processing, instead making variable objects responsible for creating a substitution and for dealing with aliasing. de Champeaux claims that the ability to add functionality to predicate calculus represented as programmatic objects provides opportunities for optimizing other logic operations as well.
The following algorithm is commonly presented and originates from .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. Given a finite set of potential equations, the algorithm applies rules to transform it to an equivalent set of equations of the form