Prerequisites

Formally, a unification approach presupposes

• An infinite set ${\displaystyle V}$ of variables. For higher-order unification, it is convenient to choose ${\displaystyle V}$ disjoint from the set of lambda-term bound variables.
• A set ${\displaystyle T}$ of terms such that ${\displaystyle V\subseteq T}$. For first-order unification, ${\displaystyle T}$ is usually the set of first-order terms (terms built from variable and function symbols). For higher-order unification ${\displaystyle T}$ consists of first-order terms and lambda terms (terms containing some higher-order variables).
• A mapping vars: ${\displaystyle T\rightarrow }$ ${\displaystyle \mathbb {P} }$${\displaystyle (V)}$, assigning to each term ${\displaystyle t}$ the set ${\displaystyle {\text{vars}}(t)\subsetneq V}$ of free variables occurring in ${\displaystyle t}$.
• A theory or equivalence relation ${\displaystyle \equiv }$ on ${\displaystyle T}$, indicating which terms are considered equal. For first-order E-unification, ${\displaystyle \equiv }$ reflects the background knowledge about certain function symbols; for example, if ${\displaystyle \oplus }$ is considered commutative, ${\displaystyle t\equiv u}$ if ${\displaystyle u}$ results from ${\displaystyle t}$ by swapping the arguments of ${\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 ${\displaystyle t\equiv u}$ if ${\displaystyle t}$ and ${\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 ${\displaystyle \sigma :V\rightarrow T}$ from variables to terms; the notation ${\displaystyle \{x_{1}\mapsto t_{1},...,x_{k}\mapsto t_{k}\}}$ refers to a substitution mapping each variable ${\displaystyle x_{i}}$ to the term ${\displaystyle t_{i}}$, for ${\displaystyle i=1,...,k}$, and every other variable to itself; the ${\displaystyle x_{i}}$ must be pairwise distinct. Applying that substitution to a term ${\displaystyle t}$ is written in postfix notation as ${\displaystyle t\{x_{1}\mapsto t_{1},...,x_{k}\mapsto t_{k}\}}$; it means to (simultaneously) replace every occurrence of each variable ${\displaystyle x_{i}}$ in the term ${\displaystyle t}$ by ${\displaystyle t_{i}}$. The result ${\displaystyle t\tau }$ of applying a substitution ${\displaystyle \tau }$ to a term ${\displaystyle t}$ is called an instance of that term ${\displaystyle t}$. As a first-order example, applying the substitution { x ↦ h(a,y), z ↦ b } to the term

	${\displaystyle f(}$	${\displaystyle {\textbf {x}}}$	${\displaystyle ,a,g(}$	${\displaystyle {\textbf {z}}}$	${\displaystyle ),y)}$
yields
	${\displaystyle f(}$	${\displaystyle {\textbf {h}}({\textbf {a}},{\textbf {y}})}$	${\displaystyle ,a,g(}$	${\displaystyle {\textbf {b}}}$	${\displaystyle ),y).}$

Generalization, specialization

If a term ${\displaystyle t}$ has an instance equivalent to a term ${\displaystyle u}$, that is, if ${\displaystyle t\sigma \equiv u}$ for some substitution ${\displaystyle \sigma }$, then ${\displaystyle t}$ is called more general than ${\displaystyle u}$, and ${\displaystyle u}$ is called more special than, or subsumed by, ${\displaystyle t}$. For example, ${\displaystyle x\oplus a}$ is more general than ${\displaystyle a\oplus b}$ if ⊕ is commutative, since then ${\displaystyle (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, ${\displaystyle f(x_{1},a,g(z_{1}),y_{1})}$ is a variant of ${\displaystyle f(x_{2},a,g(z_{2}),y_{2})}$, since

$${\displaystyle 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

$${\displaystyle 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, ${\displaystyle f(x_{1},a,g(z_{1}),y_{1})}$ is not a variant of ${\displaystyle 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 ${\displaystyle \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 ${\displaystyle x\oplus x\equiv x}$, then the term ${\displaystyle x\oplus y}$ is more general than ${\displaystyle z}$,^{[note 2]} and vice versa,^{[note 3]} although ${\displaystyle x\oplus y}$ and ${\displaystyle z}$ are of different structure.

A substitution ${\displaystyle \sigma }$ is more special than, or subsumed by, a substitution ${\displaystyle \tau }$ if ${\displaystyle t\sigma }$ is subsumed by ${\displaystyle t\tau }$ for each term ${\displaystyle t}$. We also say that ${\displaystyle \tau }$ is more general than ${\displaystyle \sigma }$. More formally, take a nonempty infinite set ${\displaystyle V}$ of auxiliary variables such that no equation ${\displaystyle l_{i}\doteq r_{i}}$ in the unification problem contains variables from ${\displaystyle V}$. Then a substitution ${\displaystyle \sigma }$ is subsumed by another substitution ${\displaystyle \tau }$ if there is a substitution ${\displaystyle \theta }$ such that for all terms ${\displaystyle X\notin V}$, ${\displaystyle X\sigma \equiv X\tau \theta }$.^[7] For instance ${\displaystyle \{x\mapsto a,y\mapsto a\}}$ is subsumed by ${\displaystyle \tau =\{x\mapsto y\}}$, using ${\displaystyle \theta =\{y\mapsto a\}}$, but ${\displaystyle \sigma =\{x\mapsto a\}}$ is not subsumed by ${\displaystyle \tau =\{x\mapsto y\}}$, as ${\displaystyle f(x,y)\sigma =f(a,y)}$ is not an instance of ${\displaystyle f(x,y)\tau =f(y,y)}$.^[8]

Solution set

A substitution σ is a solution of the unification problem E if l_iσ ≡ r_iσ for ${\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.

A unification algorithm

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,^{[14][15][16][17][18][19]} and states that linear-time algorithms were discovered independently by Martelli, Montanari (1976)^[16] and Paterson, Wegman (1976,^[20] 1978^[17]).^{[note 6]}

Given a finite set ${\displaystyle 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 { x₁ ≐ u₁, ..., x_m ≐ u_m } where x₁, ..., x_m are distinct variables and u₁, ..., 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.

${\displaystyle G\cup \{t\doteq t\}}$	${\displaystyle \Rightarrow }$	${\displaystyle G}$		delete
${\displaystyle G\cup \{f(s_{0},...,s_{k})\doteq f(t_{0},...,t_{k})\}}$	${\displaystyle \Rightarrow }$	${\displaystyle G\cup \{s_{0}\doteq t_{0},...,s_{k}\doteq t_{k}\}}$		decompose
${\displaystyle G\cup \{f(s_{0},\ldots ,s_{k})\doteq g(t_{0},...,t_{m})\}}$	${\displaystyle \Rightarrow }$	${\displaystyle \bot }$	if ${\displaystyle f\neq g}$ or ${\displaystyle k\neq m}$	conflict
${\displaystyle G\cup \{f(s_{0},...,s_{k})\doteq x\}}$	${\displaystyle \Rightarrow }$	${\displaystyle G\cup \{x\doteq f(s_{0},...,s_{k})\}}$		swap
${\displaystyle G\cup \{x\doteq t\}}$	${\displaystyle \Rightarrow }$	${\displaystyle G\{x\mapsto t\}\cup \{x\doteq t\}}$	if ${\displaystyle x\not \in {\text{vars}}(t)}$ and ${\displaystyle x\in {\text{vars}}(G)}$	eliminate[note 7]
${\displaystyle G\cup \{x\doteq f(s_{0},...,s_{k})\}}$	${\displaystyle \Rightarrow }$	${\displaystyle \bot }$	if ${\displaystyle x\in {\text{vars}}(f(s_{0},...,s_{k}))}$	check

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 ${\displaystyle g(x)}$
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 ${\displaystyle g(a)}$
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=f(f(f(f(...)))).
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

Two terms with an exponentially larger tree for their least common instance. Its dag representation (rightmost, orange part) is still of linear size.

The most general unifier of a syntactic first-order unification problem of size n may have a size of 2ⁿ. For example, the problem ${\displaystyle (((a*z)*y)*x)*w\doteq w*(x*(y*(z*a)))}$ has the most general unifier ${\displaystyle \{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.^[22]

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:

1. 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.
2. Two constants can be unified only 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.

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:

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.

Application: Feature Structure Unification

Unification has been used in different research areas of computational linguistics.^[23][24]

Particular background knowledge sets E

Used naming conventions

∀ u,v,w:	${\displaystyle u*(v*w)}$	=	${\displaystyle (u*v)*w}$	A	Associativity of ${\displaystyle *}$
∀ u,v:	${\displaystyle u*v}$	=	${\displaystyle v*u}$	C	Commutativity of ${\displaystyle *}$
∀ u,v,w:	${\displaystyle u*(v+w)}$	=	${\displaystyle u*v+u*w}$	Dl	Left distributivity of ${\displaystyle *}$ over ${\displaystyle +}$
∀ u,v,w:	${\displaystyle (v+w)*u}$	=	${\displaystyle v*u+w*u}$	Dr	Right distributivity of ${\displaystyle *}$ over ${\displaystyle +}$
∀ u:	${\displaystyle u*u}$	=	u	I	Idempotence of ${\displaystyle *}$
∀ u:	${\displaystyle n*u}$	=	u	Nl	Left neutral element n with respect to ${\displaystyle *}$
∀ u:	${\displaystyle u*n}$	=	u	Nr	Right neutral element n with respect to ${\displaystyle *}$

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:

• A^[28]
• A,C^[29]
• A,C,I^[30]
• A,C,N_l^{[note 8][30]}
• A,I^[31]
• A,N_l,N_r (monoid)^[32]
• C^[33]
• Boolean rings^[34][35]
• Abelian groups, even if the signature is expanded by arbitrary additional symbols (but not axioms)^[36]
• K4 modal algebras^[37]

Unification is semi-decidable for the following theories:

• A,D_l,D_r^[38]
• A,C,D_l^{[note 8][39]}
• Commutative rings^[36]

One-sided paramodulation

If there is a convergent term rewriting system R available for E, the one-sided paramodulation algorithm^[40] 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₂, v₃, ... 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

Triangle diagram of narrowing step s ↝ t at position p in term s, with unifying substitution σ (bottom row), using a rewrite rule l → r (top row)

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 l → r is a renamed copy of a rewrite rule from R, having no variables in common with a term s, and the subterm s|_p is not a variable and is unifiable with l via the mgu σ, then s can be narrowed to the term t = sσ[rσ]_p, i.e. to the term sσ, with the subterm at p replaced by rσ. The situation that s can be narrowed to t is commonly denoted as s ↝ t. Intuitively, a sequence of narrowing steps t₁ ↝ t₂ ↝ ... ↝ t_n can be thought of as a sequence of rewrite steps t₁ → t₂ → ... → t_n, but with the initial term t₁ 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₂.v₂.nil can be syntactically unified with the original right hand side term a.a.nil.

The narrowing lemma^[41] 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 s′ and t′, respectively, such that t′ is an instance of s′.

Formally: whenever sσ →∗ t holds for some substitution σ, then there exist terms s′, t′ such that s ↝∗ s′ and t →∗ t′ and s′ τ = t′ for some substitution τ.