Unification (computer science)

Given two input terms s and t, syntactic unification is the process which attempts to find a substitution that structurally identifies s and t. If such a substitution exists, we call this substitution a unifier of s and t.

In theory, any pair of input terms may have infinitely many unifiers. However, for most applications of unification, it is sufficient to consider the most general unifier (mgu). In some sense, the mgu is the 'simplest' possible unifier of two terms, and therefore the most useful.

In particular, first-order unification is the syntactic unification of first-order terms, i.e. terms built from variable and function symbols. Higher-order unification, on the other hand, is the unification of higher-order terms (terms containing some higher-order variables).

The theoretical properties of a particular unification algorithm depend upon the variety of term used as input. First-order unification, for instance, is decidable, efficiently so, and all unifiable terms have (unique, up to variable renamings) most general unifiers. Higher-order unification, on the other hand, is generally undecidable and lacks most general unifiers, though Huet's higher-order unification algorithm seems to work sufficiently well in practice.

Aside from syntactic unification, another form of unification, called semantic unification (equational-unification, E-unification) is also widely used. Syntactic unification attempts to find a substitution making the two input terms structurally identical. However, semantic unification attempts to make the two input terms equal modulo some equational theory. Some particularly important equational theories have been widely studied in the literature. For instance, AC-unification is the unification of terms modulo associativity and commutativity.

Unification is a significant tool in computer science. First-order unification is especially widely used in logic programming, programming language type system design, especially in type inferencing algorithms based on the Hindley-Milner type system, and automated reasoning. Higher-order unification is also widely used in proof assistants, for example Isabelle and Twelf, and restricted forms of higher-order unification are used in some programming language implementations, such as lambdaProlog. Semantic unification is widely used in SMT solvers.

The first formal investigation of unification can be attributed to J. A. Robinson, who used first-order 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.

Definition of unification for first-order logic

Let p and q be sentences in first-order logic.

UNIFY(p,q) = U where subst(U,p) = subst(U,q)

Where subst(U,p) means the result of applying substitution U on the sentence p. Then U is called a unifier for p and q. The unification of p and q is the result of applying U to both of them.

Let L be a set of sentences, for example, L = {p,q}. A unifier U is called a most general unifier for L if, for all unifiers U' of L, there exists a substitution s such that applying s to the result of applying U to L gives the same result as applying U' to L:

subst(U',L) = subst(s,subst(U,L)).

Unification in logic programming and type theory

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:

1. A variable which is uninstantiated—i.e. no previous unifications were performed on it—can be unified with an atom, a term, or another uninstantiated 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.
2. Two atoms can only be unified if they are identical.
3. 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.

In type theory, the analogous statements are:

1. 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.
2. Two type constants unify only if they are the same type.
3. Two type constructions unify only if they are applications of the same type constructor and all of their component types recursively unify.

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.

French computer scientist Gérard Huet gave an algorithm for unification in simply typed lambda calculus in 1973. There have been many developments in unification theory since then.

Higher-order unification

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 like(j; m)R(p) and the value of R (the semantic representation of the ellipsis) is determined by the equation like(j; m) = R(j). The process of solving such equations is called Higher-Order Unification.

Examples of unification

In the convention of Prolog, atoms begin with lowercase letters.

• A, A : Succeeds (tautology)
• A, B, abc : Both A and B are unified with the atom abc
• abc, B, A : As above (unification is symmetric)
• abc, abc : Unification succeeds
• abc, xyz : Fails to unify because the atoms are different
• f(A), f(B) : A is unified with B
• f(A), g(B) : Fails because the heads of the terms are different
• f(A), f(B, C) : Fails to unify because the terms have different arity
• f(g(A)), f(B) : Unifies B with the term g(A)
• f(g(A), A), f(B, xyz) : Unifies A with the atom xyz and B with the term g(xyz)
• A, f(A) : Infinite unification, A is unified with f(f(f(f(...)))). In proper first-order logic and many modern Prolog dialects this is forbidden (and enforced by the occurs check)
• A, abc, xyz, X: Fails to unify; effectively abc = xyz

See also

• Admissible rule
• Semantic Unification
• Explicit substitution in lambda calculus

References

• F. Baader and T. Nipkow, Term Rewriting and All That. Cambridge University Press, 1998.
• F. Baader and W. Snyder, Unification Theory. In J.A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume I, pages 447–533. Elsevier Science Publishers, 2001.
• Joseph Goguen, What is Unification?.
• Alex Sakharov. "Unification". MathWorld.