Unification

Origin. Herbrand (1930) implicit; Robinson (1965) gave the explicit algorithm within resolution. Solving term equations by substitution. Core engine of automated deduction and type inference.

Models. Find a substitution making two terms syntactically identical. A most general unifier subsumes all others and is unique up to renaming, so solutions have canonical form.

Formalism.

Terms and substitutions: Terms over variables and function symbols. Substitution σ maps variables to terms; tσ applies it.

Unification problem: Given {s₁ ≐ t₁, ..., sₙ ≐ tₙ}, find σ with sᵢσ = tᵢσ for all i.

Most general unifier: σ is an mgu iff every unifier θ factors as θ = σ ∘ ρ. Unique up to variable renaming.

Robinson algorithm: Scan for leftmost disagreement, bind variable, repeat. Correct but worst-case exponential (term blowup).

Martelli-Montanari rules: delete, decompose, swap, eliminate (variable). Occurs-check on elimination. Near-linear with structure sharing (Paterson-Wegman: linear).

Occurs check: x ≐ f(x) has no finite unifier — fails. Omitting it admits rational (infinite) trees.

Variants: Higher-order unification: undecidable (Huet); pre-unification used. E-unification: modulo an equational theory (AC, etc.), often infinitary.

Symbols.

Symbol	Unicode	Name	Meaning
σ	U+03C3	Sigma / Substitution	Variable-to-term map; tσ is its application
θ	U+03B8	Theta / Unifier	An arbitrary unifier, compared against the mgu
ρ	U+03C1	Rho / Residual	The substitution factoring θ through σ
≐	U+2250	Approaches the limit / Equation	A to-be-unified pair, not an asserted identity
∘	U+2218	Ring operator / Composition	Composition of substitutions
∈	U+2208	Element of	Membership, as in Miller's pattern condition
λ	U+03BB	Lambda	Binder in higher-order unification problems
mgu	—	Most general unifier	Every unifier factors through it
E	—	Equational theory	Theory modulo which unification is performed

Metatheory. First-order unification is decidable and unitary: if a unifier exists, a most general one exists and is unique up to renaming of variables (Robinson 1965). Robinson's algorithm is exponential in time and space, because a most general unifier written out as a term can be exponentially large — the standard witness is the system x₁ ≐ f(x₀,x₀), x₂ ≐ f(x₁,x₁), … — but with dags and structure sharing the problem is linear: Paterson and Wegman (1978) gave a linear algorithm, and Martelli and Montanari (1982) an almost-linear one on a union-find representation. Dwork, Kanellakis and Mitchell (1984) proved unifiability P-complete, so the problem is inherently sequential and is not expected to parallelize. Huet (1973) proved higher-order unification undecidable and Goldfarb (1981) sharpened this to the second-order case; Miller's pattern fragment (1991), where free variables are applied only to distinct bound variables, is decidable and unitary and is what λProlog implements. Equational unification is classified by the size of a minimal complete set of unifiers: unitary, finitary (associative-commutative theories, Stickel), infinitary (associativity alone, Plotkin), or nullary.

Applies to. Resolution and automated theorem proving. Hindley-Milner type inference. Logic programming (SLD resolution). Term rewriting and completion. Pattern matching.

Limitations. The occurs check is what makes unification sound and what implementations discard: solving x ≐ f(x) is correct only over rational infinite trees, and a Prolog that omits the check is unsound for the Herbrand universe it claims to compute in. Syntactic unification is blind to meaning — f(a,b) and f(b,a) do not unify even where f is commutative — so every equational theory that matters must be built in as a separate E-unification problem with its own decidability status and its own unifier cardinality, and the resulting unifier sets can be infinite. Higher-order unification is undecidable, so systems that need it fall back on Huet's pre-unification, which terminates but leaves flex–flex pairs unsolved, or restrict to the pattern fragment and are incomplete outside it. P-completeness rules out substantial parallel speedup. And unification computes a most general common instance only; the dual operation of anti-unification, computing a least general generalization (Plotkin and Reynolds, 1970), is a different algorithm with different properties and is not obtained by running unification backwards.