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	Substitution	Variable-to-term map
≐	U+2250	Equation	To-be-unified pair
mgu	—	MGU	Most general unifier
∘	U+2218	Composition	Substitution composition

Metatheory. First-order unification is decidable and unitary (an mgu exists whenever a unifier does). Higher-order unification is undecidable; E-unification varies from unitary to infinitary by theory. Dual notion: anti-unification (generalization).

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

Limitations. Naive algorithm exponential; occurs-check adds cost. Higher-order case undecidable. Equational unification can be intractable or infinitary.