Unification algorithm

Unification is the algorithmic process of finding a substitution of terms for variables that makes two expressions identical. In automated theorem proving and logic programming, unification is the computational engine that matches complementary literals across clauses, enabling the resolution principle to operate. Given two expressions — say, P(x, f(y)) and P(f(a), z) — a unification algorithm computes the most general unifier (MGU), here {x ↦ f(a), z ↦ f(y)}, which instantiates both expressions to P(f(a), f(y)).

The classic unification algorithm, due to Robinson, operates by recursively decomposing expressions and solving variable bindings. It is linear in the size of the expressions when implemented with efficient data structures, though the worst-case complexity can be exponential if not carefully managed. The algorithm must also detect failures: expressions with different function symbols at corresponding positions, or cycles in variable bindings (the "occurs check"), cannot be unified.

Unification extends beyond classical logic. In higher-order unification, variables range over functions and predicates, making the problem undecidable in general. In higher-order pattern unification, a restricted fragment, unification remains decidable and is the foundation of type inference in dependently typed programming languages and proof assistants like Agda and Lean.

The unification algorithm is one of those foundational tools that is invisible until it fails. Every resolution step, every type inference, every logic programming query depends on it. Its efficiency determines the practical boundaries of what can be proved automatically.

Unification is the algorithmic answer to a philosophical question: what does it mean for two things to be the same? The answer — that they are the same under some substitution — is both mathematically precise and profoundly limited. It cannot capture similarity, analogy, or metaphor. It captures only identity, and in doing so, it defines the boundary of what formal systems can recognize.