Unification (computer science)

A unification problem is a finite set of equations to solve, where are in the set 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. Prerequisites Formally, a unification approach presupposes • An infinite set V of variables. For higher-order unification, it is convenient to choose V disjoint from the set of lambda-term bound variables. • A set T of terms such that V \subseteq T. For first-order unification, T is usually the set of first-order terms (terms built from variable and function symbols). For higher-order unification T consists of first-order terms and lambda terms (terms containing some higher-order variables). • A mapping \text{vars}\colon T \rightarrow \mathbb{P}(V), assigning to each term t the set \text{vars}(t) \subsetneq V of free variables occurring in t. • A theory or equivalence relation \equiv on T, indicating which terms are considered equal. For first-order E-unification, \equiv reflects the background knowledge about certain function symbols; for example, if \oplus is considered commutative, t\equiv u if u results from t by swapping the arguments of \oplus at some (possibly all) occurrences. 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 t\equiv u if t and 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 \sigma: V\rightarrow T from variables to terms; the notation \{x_1\mapsto t_1, ..., x_k \mapsto t_k\} refers to a substitution mapping each variable x_i to the term t_i, for i=1,...,k, and every other variable to itself; the x_i must be pairwise distinct. Applying that substitution to a term t is written in postfix notation as t \{x_1 \mapsto t_1, ..., x_k \mapsto t_k\}; it means to (simultaneously) replace every occurrence of each variable x_i in the term t by t_i. The result t\tau of applying a substitution \tau to a term t is called an instance of that term t. As a first-order example, applying the substitution to the term Generalization, specialization If a term t has an instance equivalent to a term u, that is, if t\sigma \equiv u for some substitution \sigma, then t is called more general than u, and u is called more special than, or subsumed by, t. For example, x\oplus a is more general than a\oplus b if ⊕ is commutative, since then (x\oplus a) \{x\mapsto b\} = b\oplus a\equiv a\oplus b. 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, f(x_1, a, g(z_1), y_1) is a variant of f(x_2, a, g(z_2), y_2), since f(x_1, a, g(z_1), y_1) \{x_1 \mapsto x_2, y_1 \mapsto y_2, z_1 \mapsto z_2\} = f(x_2, a, g(z_2), y_2) and f(x_2, a, g(z_2), y_2) \{x_2 \mapsto x_1, y_2 \mapsto y_1, z_2 \mapsto z_1\} = f(x_1, a, g(z_1), y_1). However, f(x_1, a, g(z_1), y_1) is not a variant of f(x_2, a, g(x_2), x_2), 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 \equiv, a term may be both more general and more special than a structurally different term. For example, if ⊕ is idempotent, that is, if always x \oplus x \equiv x, then the term x\oplus y is more general than z, and vice versa, although x\oplus y and z are of different structure. A substitution \sigma is more special than, or subsumed by, a substitution \tau if t\sigma is subsumed by t\tau for each term t. We also say that \tau is more general than \sigma. More formally, take a nonempty infinite set V of auxiliary variables such that no equation l_i \doteq r_i in the unification problem contains variables from V. Then a substitution \sigma is subsumed by another substitution \tau if there is a substitution \theta such that for all terms X\notin V, X\sigma \equiv X\tau\theta. Solution set A substitution σ is a solution of the unification problem E if for 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. 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. 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 subsumed 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 : 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 {{Quote box|title=Robinson's 1965 unification algorithm Symbols are ordered such that variables precede function symbols. Terms are ordered by increasing written length; equally long terms are ordered lexicographically. For a set T of terms, its disagreement path p is the lexicographically least path where two member terms of T differ. Its disagreement set is the set of subterms starting at p, formally: {{math|{ tp : t ∈ T }}}. Algorithm: {{pre| Given a set T of terms to be unified Let initially be the identity substitution do forever     if is a singleton set then         return     fi     let D be the disagreement set of     let s, t be the two lexicographically least terms in D     if s is not a variable or s occurs in t then         return "NONUNIFIABLE"     fi     \sigma := \sigma \{ s \mapsto t \} done }} }} Jacques Herbrand discussed the basic concepts of unification and sketched an algorithm in 1930. But most authors attribute the first unification algorithm to John Alan Robinson (cf. box). Robinson's algorithm had worst-case exponential behavior in both time and space. Numerous authors have proposed more efficient unification algorithms. 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. Given a finite set G = \{ s_1 \doteq t_1, ..., s_n \doteq t_n \} of potential equations, the algorithm applies rules to transform it to an equivalent set of equations of the form { x1 ≐ u1, ..., xm ≐ um } where x1, ..., xm are distinct variables and u1, ..., um are terms containing none of the xi. 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. : 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 \langle n_{var}, n_{lhs}, n_{eqn}\rangle where is the number of variables that occur more than once in the equation set, is the number of function symbols and constants on the left hand sides of potential equations, and is the number of equations. When rule eliminate is applied, decreases, since x is eliminated from G and kept only in { x ≐ t }. Applying any other rule can never increase again. When rule decompose, conflict, or swap is applied, decreases, since at least the left hand side's outermost f disappears. Applying any of the remaining rules delete or check can't increase , but decreases . Hence, any rule application decreases the triple \langle n_{var}, n_{lhs}, n_{eqn}\rangle with respect to the lexicographical order, which is possible only a finite number of times. Conor McBride observes 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. representation (rightmost, orange part) is still of linear size. The most general unifier of a syntactic first-order unification problem of size may have a size of . For example, the problem has the most general unifier {{tmath| \{ z \mapsto a, y \mapsto a*a, x \mapsto (a*a)*(a*a), w \mapsto ((a*a)*(a*a))*((a*a)*(a*a)) \} }}, 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. Application: unification in logic programming The concept of unification is one of the main ideas behind logic programming. Specifically, unification is a basic building block of resolution, a rule of inference for determining formula satisfiability. In Prolog, 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: • 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. • Most operations, including +, -, *, /, are not evaluated by =. So for example 1+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. Application: type inference Type inference algorithms are typically based on unification, particularly Hindley-Milner type inference which is used by the functional languages Haskell and ML. For example, when attempting to infer the type of the Haskell expression True : ['x'], the compiler will use the type a -> [a] -> [a] of the list construction function (:), the type Bool of the first argument True, and the type [Char] of the second argument ['x']. The polymorphic type variable a will be unified with Bool and the second argument [a] will be unified with [Char]. a cannot be both Bool and Char at the same time, therefore this expression is not correctly typed. 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. ==Order-sorted unification==

Order-sorted logic allows one to assign a sort, or type, to each term, and to declare a sort s1 a subsort of another sort s2, commonly written as s1 ⊆ s2. 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 s1, s2 their intersection s1 ∩ s2 to be declared, too: if x1 and x2 is a variable of sort s1 and s2, respectively, the equation x1 ≐ x2 has the solution { x1 = x, x2 = x }, where x: s1 ∩ s2. 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. 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. 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==

Background on infinite trees: • • • Unification algorithm, Prolog II: • • Applications: • ==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 and are distinct constants, the equation has no solution with respect to purely syntactic unification, where nothing is known about the operator . However, if the is known to be commutative, then the substitution solves the above equation, since : The background knowledge E could state the commutativity of by the universal equality " for all ". Particular background knowledge sets E 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: • '''''' • ',' • ',,' • ',''''''' (monoid) • '''''' • Boolean rings • Abelian groups, even if the signature is expanded by arbitrary additional symbols (but not axioms) • K4 modal algebras Unification is semi-decidable for the following theories: • ',''''''' • ',,' • Commutative rings can be used to enumerate all solutions of given equations. 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 Rs 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(...) }). 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; v2, v3, ... 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. 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 is a renamed copy of a rewrite rule from R, having no variables in common with a term s, and the subterm is not a variable and is unifiable with via the mgu , then can be narrowed to the term , i.e. to the term , with the subterm at p replaced by . The situation that s can be narrowed to t is commonly denoted as s ↝ t. Intuitively, a sequence of narrowing steps t1 ↝ t2 ↝ ... ↝ tn can be thought of as a sequence of rewrite steps t1 → t2 → ... → tn, but with the initial term t1 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): The last term, v2.v2.nil can be syntactically unified with the original right hand side term a.a.nil. The narrowing lemma 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 and , respectively, such that is an instance of . Formally: whenever holds for some substitution σ, then there exist terms such that and and for some substitution τ. ==Higher-order unification==

gave a semi-decidable (pre-)unification algorithm that allows a systematic search of the space of unifiers (generalizing the unification algorithm of Martelli-Montanari and Gilles Dowek 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, 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. The Zipperposition theorem prover has an algorithm integrating these well-behaved subsets into a full higher-order unification algorithm. 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 and the value of R (the semantic representation of the ellipsis) is determined by the equation . The process of solving such equations is called Higher-Order Unification. 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. ==See also==