
Unification (computer science)

In logic and computer science, unification is an algorithmic process of solving equations between symbolic expressions.
Depending on which expressions (also called "terms") are allowed to occur in an equation set (also called "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.
A "solution" of a unification problem is denoted as a substitution, that is, a mapping assigning a symbolic value to each variable of the problem's expressions. A unification algorithm should compute for a given problem a "complete", and "minimal" substitution set, that is, a set covering all its solutions, and containing no redundant members. Depending on the framework, a complete and minimal substitution set may have at most one, at most finitely many, or possibly infinitely many members, or may not exist at all. In some frameworks it is generally impossible to decide whether any solution exists. For first-order syntactical unification, Martelli and Montanari gave an algorithm that reports unsolvability or computes a complete and minimal singleton substitution set containing the so-called most general unifier.
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.
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 trees.
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; the same problem, viewed in an abelian group, where (⋅) is considered also commutative, has any substitution at all as a solution.
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)" }.
A unification algorithm was first discovered by Jacques Herbrand, while a first formal investigation can be attributed to John Alan Robinson, 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.
Common formal definitions.
Prerequisites.
Formally, a unification approach presupposes
First-order term.
Given a set formula_1 of variable symbols, a set formula_23 of constant symbols and sets formula_24 of "n"-ary function symbols, also called operator symbols, for each natural number formula_25, the set of (unsorted first-order) terms formula_3 is recursively defined to be the smallest set with the following properties:
For example, if formula_32 is a variable symbol, formula_33 is a constant symbol, and formula_34 is a binary function symbol, then formula_35, and (hence) formula_36 by the first, second, and third term building rule, respectively. The latter term is usually written as formula_37, using infix notation and the more common operator symbol + for convenience.
Substitution.
A substitution is a mapping formula_38 from variables to terms; the notation formula_39 refers to a substitution mapping each variable formula_40 to the term formula_41, for formula_42, and every other variable to itself. Applying that substitution to a term formula_8 is written in postfix notation as formula_44; it means to (simultaneously) replace every occurrence of each variable formula_40 in the term formula_8 by formula_41. The result formula_48 of applying a substitution formula_49 to a term formula_8 is called an instance of that term formula_8.
As a first-order example, applying the substitution to the term 
Generalization, specialization.
If a term formula_8 has an instance equivalent to a term formula_15, that is, if formula_54 for some substitution formula_55, then formula_8 is called more general than formula_15, and formula_15 is called more special than, or subsumed by, formula_8. For example, formula_60 is more general than formula_61 if ⊕ is commutative, since then formula_62.
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, 
formula_63
is a variant of 
formula_64,
since
formula_65
and 
formula_66.
However, formula_63 is "not" a variant of formula_68, 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 formula_11, a term may be both more general and more special than a structurally different term.
For example, if ⊕ is idempotent, that is, if always formula_70, then the term formula_71 is more general than formula_72, and vice versa, although formula_71 and formula_72 are of different structure.
A substitution formula_55 is more special than, or subsumed by, a substitution formula_49 if formula_77 is more special than formula_48 for each term formula_8. We also say that formula_49 is more general than formula_55.
For instance formula_82 is more special than formula_83,
but 
formula_84 is not,
as formula_85 is not more special than
formula_86.
Unification problem, solution set.
A unification problem is a finite set of potential equations, where .
A substitution σ is a solution of that problem if for formula_87. Such a substitution is also called a unifier of the unification problem.
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, a set "S" of unifiers is called complete if each solution substitution is subsumed by some substitution σ ∈ "S"; the set "S" is called minimal if none of its members subsumes another one.
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 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 "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 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"("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.
The first algorithm given by Robinson (1965) was rather inefficient; cf. box.
The following faster algorithm originated from Martelli, Montanari (1982).
This paper also lists preceding attempts to find an efficient syntactical unification algorithm, and states that linear-time algorithms were discovered independently by Martelli, Montanari (1976) and Paterson, Wegman (1978).
Given a finite set formula_88 of potential equations,
the algorithm applies rules to transform it to an equivalent set of equations of the form
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.
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 below.
Proof of termination.
For the proof of termination of the algorithm consider a triple formula_89
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 formula_89 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 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.
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 , 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, 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 codice_1, but is also done when instantiating variables (see below). It is also used in other languages by the use of the equality symbol codice_1, but also in conjunction with many operations including codice_3, codice_4, codice_5, codice_6. Type inference algorithms are typically based on unification.
In Prolog:
Application: type inference.
Unification is used during type inference, for instance in the functional programming language Haskell. 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 codice_7 is not correctly typed. The list construction function codice_8 is of type codice_9, and for the first argument codice_10 the polymorphic type variable codice_11 has to be unified with codice_10's type, codice_13. The second argument, codice_14, is of type codice_15, but codice_11 cannot be both codice_13 and codice_18 at the same time.
Like for Prolog, an algorithm for type inference can be given:
Due to its declarative nature, the order in a sequence of unifications is (usually) unimportant.
Note that in the terminology of first-order logic, an atom is a basic proposition and is unified similarly to a Prolog term.
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.
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:
Unification is semi-decidable for the following theories:
One-sided paramodulation.
If there is a convergent term rewriting system "R" available for "E",
the one-sided paramodulation algorithm
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 "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"(...) }).
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.
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
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 "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):
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" 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.
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". A well studied branch of higher-order unification is the problem of unifying simply typed lambda terms modulo the equality determined by αβη conversions. Such unification problems do not have most general unifiers. While higher-order unification is undecidable, Gérard Huet gave a semi-decidable (pre-)unification algorithm that allows a systematic search of the space of unifiers (generalizing the unification algorithm of Martelli-Montanari with rules for terms containing higher-order variables) that seems to work sufficiently well in practice. Huet and Gilles Dowek have written articles surveying this topic.
Dale Miller has described what is now called "higher-order pattern unification". This subset of higher-order unification is decidable and solvable unification problems have most-general unifiers. Many computer systems that contain higher-order unification, such as the higher-order logic programming languages λProlog and Twelf, often implement only the pattern fragment and not full higher-order unification.
In computational linguistics, one of the most influential theories of ellipsis is that ellipses are represented by free variables whose values are then determined using Higher-Order Unification (HOU). 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.
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") },
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.