Lesson 7.1 — Unification: Robinson, Martelli–Montanari, union-find, and the occurs check¶
Techniques: Robinson's algorithm — disagreement pairs and composed substitutions (Robinson 1965 [Rob65]); the Martelli–Montanari rule system — unification as rewriting a set of equations to solved form (Martelli & Montanari 1982 [MM82]); union-find unification over term graphs, almost linear (Huet 1976 [Hue76]; linear: Paterson & Wegman 1978 [PW78]); the occurs check — why
x ≐ f(x)has no finite solution, when to test it, and what omitting it buys (rational trees) · Pebble implements: union-find over numeric type variables ininferTypes(exercise E2); the lab's Algorithm J unifies in place (labs/ch07-hm, L2) · Drills:unification· Prerequisites: Lesson 6.4 (matching, Algorithm 6.4.6) · Time: 4 hours
Every inference algorithm in this chapter reduces "what type does this expression have?" to "which types make these equations true?". An application f x whose function has type \(\alpha\) and whose argument has type \(\beta\) produces the equation \(\alpha \doteq \beta \to \gamma\); a literal 1 in a position of type \(\delta\) produces \(\delta \doteq \mathsf{int}\). Solving such systems is unification, and it is older than type inference: Robinson invented it in 1965 for resolution theorem proving. This lesson develops it on plain first-order terms, where the algorithms are easiest to see, and the rest of the chapter uses it on types. Lesson 6.4's matching was the one-sided special case (only the pattern had variables); here both sides do.
1. Problem and motivation¶
Robinson's algorithm¶
The problem. Given terms built from function symbols and variables, and a set of equations \(s_i \doteq t_i\) between them, find a substitution that makes each pair syntactically identical — and among all such substitutions, one from which every other can be obtained by further substitution, the most general unifier (MGU). Robinson needed it for the resolution rule: to resolve \(P(x, f(y))\) against \(\neg P(g(z), x)\), the prover must find the most general instance of both atoms [Rob65, §5]. His paper gives the algorithm (find the first place the two terms disagree, bind a variable there, repeat) and proves that it computes an MGU whenever a unifier exists. Type checkers inherited it through Hindley [Hin69] and Milner [Mil78]; Clang's template argument deduction is its one-sided cousin (§7).
Martelli–Montanari¶
The problem. Robinson's algorithm is a loop around a mutable substitution, which makes both its correctness proof and its cost hard to read off. Martelli and Montanari [MM82] recast unification as rewriting a set of equations with six local rules (delete, decompose, conflict, swap, eliminate, check) until the set is in solved form, which is the MGU. The rules separate what unification does from in which order and with which data structures it is done, so the same presentation covers Robinson's order, lazy orders, and the efficient multi-equation algorithm of their paper; it is also how unification is extended to equational theories [BS01]. Constraint-based inference (Lesson 7.4) and GHC's constraint solver (§7) are organized the same way: a store of equations rewritten by rules.
Union-find unification¶
The problem. Both previous presentations substitute terms into terms. On the family of §5 that doubles term sizes at every step, so even deciding whether a unifier exists costs exponential time with trees. Huet [Hue76] observed that unification only needs to know which terms have been made equal: represent each term once, as a node of a graph, keep equivalence classes of nodes in a union-find structure, and merge classes instead of substituting. That makes unification almost linear, \(O(n\,\alpha(n))\); Paterson and Wegman made it strictly linear [PW78]. This is the representation of every production inference engine (OCaml, GHC, rustc, Swift) and of the Pebble checker you write in exercise E2.
The occurs check¶
The problem. \(x \doteq f(x)\) has no solution among finite terms: any \(\theta\) would need \(\lvert \theta x \rvert = \lvert \theta x \rvert + 1\). A unifier must therefore reject binding a variable to a term that contains it. The test is the occurs check, and it is the difference between inference that rejects fun x -> x x and inference that "succeeds" with an infinite type. It costs time — done eagerly, it makes unification quadratic — so Prolog systems omit it by default, and OCaml offers -rectypes to allow the cyclic (rational) solutions instead of rejecting them. When and whether to perform it is a design decision with consequences for soundness and error messages.
2. Definitions and algorithms¶
Definition 7.1.1 (Terms)
A signature \(\Sigma\) is a set of function symbols, each with an arity \(n \ge 0\) (constants have arity 0). With a countable set \(V\) of variables (written \(x, y, z, u, v, w\)), the terms \(T(\Sigma, V)\) are the least set containing \(V\) and every \(f(t_1, \dots, t_n)\) with \(f \in \Sigma\) of arity \(n\) and \(t_i \in T(\Sigma, V)\). \(\mathrm{vars}(t)\) is the set of variables occurring in \(t\); \(\lvert t \rvert\) is the number of symbol and variable occurrences (its size as a tree). Types are terms: \(\Sigma = \{\mathsf{int}/0, \mathsf{bool}/0, {\to}/2, {\times}/2, \mathsf{list}/1\}\), and \(\alpha \to \mathsf{int}\) is \({\to}(\alpha, \mathsf{int})\).
Definition 7.1.2 (Substitution)
A substitution \(\theta\) is a map \(V \to T(\Sigma, V)\) with \(\theta x \ne x\) for finitely many \(x\), its domain \(\mathrm{dom}(\theta)\); it is written \([x_1 \mapsto t_1, \dots, x_n \mapsto t_n]\) and extended to terms homomorphically: \(\theta f(t_1, \dots, t_n) = f(\theta t_1, \dots, \theta t_n)\). The composition \(\theta_2 \theta_1\) applies \(\theta_1\) first: \((\theta_2\theta_1) t = \theta_2(\theta_1 t)\). \(\theta\) is idempotent if \(\theta\theta = \theta\), equivalently if no variable of \(\mathrm{dom}(\theta)\) occurs in any \(\theta x\).
Definition 7.1.3 (Unifier, generality, MGU)
A unification problem is a finite set \(E = \{s_1 \doteq t_1, \dots, s_k \doteq t_k\}\). A substitution \(\theta\) is a unifier of \(E\) if \(\theta s_i = \theta t_i\) for every \(i\); \(U(E)\) is the set of unifiers. \(\theta\) is more general than \(\theta'\), written \(\theta \preceq \theta'\), if \(\theta' = \rho\theta\) for some substitution \(\rho\). A most general unifier (MGU) of \(E\) is a \(\theta \in U(E)\) with \(\theta \preceq \theta'\) for every \(\theta' \in U(E)\). MGUs are unique up to a renaming of variables.
The running example
(\(f, h\) binary, \(g\) unary, \(a, b\) constants.) \(\theta_0 = [x \mapsto g(b),\ z \mapsto g(v),\ y \mapsto v,\ u \mapsto b,\ w \mapsto a]\) unifies \(E_0\): both sides of the first equation become \(h(g(b), g(v), g(v))\). So does \(\theta_0' = [x \mapsto g(b), z \mapsto g(a), y \mapsto a, v \mapsto a, u \mapsto b, w \mapsto a]\), but \(\theta_0' = [v \mapsto a]\,\theta_0\), so \(\theta_0 \preceq \theta_0'\) and not conversely: \(\theta_0'\) is not most general. Two variants fail: \(E_{\mathrm{occ}} = \{h(x, g(y), z) \doteq h(g(z), z, g(x))\}\) and \(E_{\mathrm{clash}} = \{f(u, a) \doteq f(b, u)\}\).
Definition 7.1.4 (Solved form)
\(E\) is in solved form if \(E = \{x_1 \doteq t_1, \dots, x_n \doteq t_n\}\) where the \(x_i\) are pairwise distinct variables and no \(x_i\) occurs in any \(t_j\). Its associated substitution is \(\theta_E = [x_1 \mapsto t_1, \dots, x_n \mapsto t_n]\), which is idempotent.
Lemma 7.1.5 (A solved form is its own MGU)
If \(E\) is in solved form, \(\theta_E\) is an idempotent MGU of \(E\); moreover \(\theta' = \theta'\theta_E\) for every unifier \(\theta'\) of \(E\).
Proof
\(\theta_E\) unifies \(E\): \(\theta_E x_i = t_i\), and \(\theta_E t_i = t_i\) because no \(x_j\) occurs in \(t_i\). Generality: let \(\theta'\) unify \(E\). For \(x_i \in \mathrm{dom}(\theta_E)\): \(\theta'\theta_E x_i = \theta' t_i = \theta' x_i\), the last step because \(\theta'\) unifies \(x_i \doteq t_i\). For any other variable \(y\): \(\theta'\theta_E y = \theta' y\). So \(\theta' = \theta'\theta_E\), hence \(\theta_E \preceq \theta'\) with \(\rho = \theta'\). Idempotence: \(\theta_E\theta_E x_i = \theta_E t_i = t_i\).
Robinson's algorithm¶
Definition 7.1.6 (Disagreement pair)
For terms \(s \ne t\), the disagreement pair \(D(s, t)\) is found by walking both trees in preorder, left to right, from the roots: at the first position where the two subterms \(s', t'\) differ in their head (one is a variable, or the function symbols or arities differ), \(D(s, t) = (s', t')\).
Algorithm 7.1.7 (Robinson)
- Input: a unification problem \(E = \{s_1 \doteq t_1, \dots, s_k \doteq t_k\}\).
- Output: an idempotent MGU \(\theta\) of \(E\), or failure (
clashoroccurs). - Precondition: none; terms are trees.
- Postcondition: on success \(\theta s_i = \theta t_i\) for all \(i\) and \(\theta \preceq \theta'\) for every unifier \(\theta'\) (Theorem 7.1.14); failure only if \(U(E) = \emptyset\).
- Invariant: \(\theta\) is idempotent and \(U(E) = \{\, \theta' \mid \theta' \in U(\theta E) \text{ and } \theta' = \theta'\theta \,\}\), i.e. every unifier of \(E\) factors through \(\theta\) (Lemma 7.1.13).
function Robinson(E):
θ ← [] # the identity
loop:
pick the first i with θ s_i ≠ θ t_i # all unified: done
if none: return θ
(s', t') ← D(θ s_i, θ t_i) # Definition 7.1.6
if neither s' nor t' is a variable:
fail "clash" # different symbols
(x, r) ← (s', t') if s' is a variable else (t', s')
if x ∈ vars(r):
fail "occurs" # the occurs check
θ ← [x ↦ r] θ # compose: θ stays idempotent
Martelli–Montanari¶
Algorithm 7.1.8 (Martelli–Montanari rule system, deterministic strategy)
- Input: a unification problem \(E\).
- Output: a solved form \(S\) equivalent to \(E\) (so \(\theta_S\) is an MGU by Lemma 7.1.5), or failure.
- Precondition: none.
- Postcondition: \(U(S) = U(E)\) on success; \(U(E) = \emptyset\) on failure (Theorem 7.1.15).
- Invariant: \(U(\mathit{todo} \cup \mathit{solved}) = U(E)\); \(\mathit{solved}\) is in solved form and none of its left-hand variables occurs in \(\mathit{todo}\) (Lemma 7.1.16).
The six rules, each rewriting one equation \(e\) of the store:
| Rule | Equation | Effect |
|---|---|---|
| delete | \(t \doteq t\) | remove it |
| decompose | \(f(s_1..s_n) \doteq f(t_1..t_n)\) | replace it by \(s_1 \doteq t_1, \dots, s_n \doteq t_n\) |
| conflict | \(f(\dots) \doteq g(\dots)\), \(f \ne g\) or arities differ | fail clash |
| swap | \(t \doteq x\), \(t\) not a variable | replace it by \(x \doteq t\) |
| check | \(x \doteq t\), \(x \in \mathrm{vars}(t)\), \(t \ne x\) | fail occurs |
| eliminate | \(x \doteq t\), \(x \notin \mathrm{vars}(t)\) | apply \([x \mapsto t]\) to every other equation; keep \(x \doteq t\) as solved |
function MM(E):
todo ← E as a list; solved ← []
while todo is not empty:
(l ≐ r) ← pop the first equation of todo
if l = r: continue # delete
if l, r are both applications:
if head(l) ≠ head(r) or arity(l) ≠ arity(r): fail "clash" # conflict
push l_i ≐ r_i (i = 1..n) at the front of todo, in order; continue # decompose
if l is an application: push r ≐ l at the front; continue # swap
# now l is a variable x
if x ∈ vars(r): fail "occurs" # check
todo ← [x ↦ r] todo # eliminate
solved ← [x ↦ r] solved (right-hand sides only); append x ≐ r to solved
return solved
Union-find unification¶
Definition 7.1.9 (Term graph, classes, schema)
A term graph has one node per variable and one node per occurrence of an application, labelled with its symbol and pointing to its argument nodes in order. A union-find structure partitions the nodes into classes; \(\mathrm{find}(n)\) returns its class's representative, \(\mathrm{union}(a, b)\) merges two classes. Each class has at most one designated schema: an application node of the class (undefined if the class contains only variables). Reading back a node \(n\): if \(\mathrm{find}(n)\)'s class has a schema \(f(n_1, \dots, n_k)\), the term is \(f(\text{read}(n_1), \dots, \text{read}(n_k))\); otherwise it is a chosen variable of the class.
Algorithm 7.1.10 (Union-find unification, after Huet)
- Input: a unification problem \(E\), built as a term graph (shared variables are one node).
- Output: an MGU read back from the classes, or failure.
- Precondition: union by rank and path compression in
union/find. - Postcondition: on success, every \(s_i\) and \(t_i\) read back to the same term under the substitution \(x \mapsto \text{read}(x)\), which is an MGU; failure iff \(U(E) = \emptyset\) (Theorem 7.1.17).
- Invariant: two nodes are in the same class only if every unifier of \(E\) maps their terms to equal terms (classes are forced equalities); every pair of nodes that must be equal is either already in one class or still on the stack (both are established in the proof of Theorem 7.1.17).
function UnifyUF(E):
build the term graph; stack ← [(node(s_i), node(t_i)) for each equation]
while stack is not empty:
(a, b) ← pop stack
ra ← find(a); rb ← find(b)
if ra = rb: continue # already equal
sa ← schema(ra); sb ← schema(rb)
if sa and sb are both defined:
if symbol(sa) ≠ symbol(sb) or arity differs: fail "clash"
r ← union(ra, rb); schema(r) ← sa # merge BEFORE recursing
push (arg_i(sa), arg_i(sb)) for i = 1..arity
else:
r ← union(ra, rb); schema(r) ← sa if defined else sb
if the graph "class → classes of its schema's arguments" has a cycle:
fail "occurs" # deferred occurs check
return [x ↦ read(x) for every variable x with read(x) ≠ x]
Merging the two classes before pushing the argument pairs guarantees termination even on inputs that would produce cycles, because every non-trivial step reduces the number of classes.
The occurs check¶
Definition 7.1.11 (Occurs check; rational trees)
The occurs check for a binding \(x \mapsto t\) tests \(x \in \mathrm{vars}(t)\) (after dereferencing bound variables). A rational tree is a possibly infinite tree with finitely many distinct subtrees; it is represented by a finite, possibly cyclic, graph. Unification over rational trees omits the occurs check: \(x \doteq f(x)\) then has the solution \(x = f(f(f(\dots)))\).
Algorithm 7.1.12 (Occurs check, eager and deferred)
- Input: eager: a variable \(x\) and a term (graph node) \(t\); deferred: the final class graph of Algorithm 7.1.10.
- Output: eager: whether \(x\) occurs in \(t\); deferred: whether some class reaches itself.
- Precondition: eager: bound variables are dereferenced through the current substitution or
find. - Postcondition: "occurs" iff no finite unifier exists for the bindings made (Lemma 7.1.18).
- Invariant: eager: the visited set contains only nodes reachable from \(t\); deferred: DFS colours (white, grey, black), a grey node is on the current path.
function Occurs(x, t): # eager, called before binding x ↦ t
t ← dereference(t)
if t is a variable: return t = x
return any Occurs(x, t_i) for the arguments t_i of t
function HasCycle(classes): # deferred, once, at the end
colour every class white
for each class c: if colour(c) = white and Visit(c): return true
return false
function Visit(c):
colour(c) ← grey
for each argument class d of schema(c):
if colour(d) = grey: return true # back edge: c reaches itself
if colour(d) = white and Visit(d): return true
colour(c) ← black; return false
3. Worked examples¶
The drill oracle (tools/course/lib/hm.py: robinson, martelli_montanari, union_find_unify) produced every table below.
Robinson's algorithm¶
Algorithm 7.1.7 on \(E_0\); each row composes one binding onto \(\theta\):
| step | equation | disagreement pair | action | \(\theta\) after the step |
|---|---|---|---|---|
| 1 | (1) | \(x\) / \(g(u)\) | bind \(x \mapsto g(u)\) | \([x \mapsto g(u)]\) |
| 2 | (1) | \(g(y)\) / \(z\) | bind \(z \mapsto g(y)\) | \([x \mapsto g(u), z \mapsto g(y)]\) |
| 3 | (1) | \(y\) / \(v\) | bind \(y \mapsto v\) | \([x \mapsto g(u), z \mapsto g(v), y \mapsto v]\) |
| 4 | (2) | \(u\) / \(b\) | bind \(u \mapsto b\) | \([x \mapsto g(b), z \mapsto g(v), y \mapsto v, u \mapsto b]\) |
| 5 | (2) | \(a\) / \(w\) | bind \(w \mapsto a\) | \([x \mapsto g(b), z \mapsto g(v), y \mapsto v, u \mapsto b, w \mapsto a]\) |
| 6 | — | — | every equation unified (equation (3) became \(g(g(b)) \doteq g(g(b))\) at step 4) | same |
- Step 2: after \(x \mapsto g(u)\) the first difference of equation (1) is the second argument, \(g(y)\) against \(z\); the variable is on the right, so \(z\) is bound.
- Step 3: composing \([y \mapsto v]\) also rewrites the range: \(z \mapsto g(y)\) becomes \(z \mapsto g(v)\). That rewrite is what keeps \(\theta\) idempotent — and what costs time on large terms (§5).
Martelli–Montanari¶
Algorithm 7.1.8 on \(E_0\); one row per rule application, with the whole store:
| step | rule | equation | worklist after | solved after |
|---|---|---|---|---|
| 1 | decompose | \(h(x, g(y), z) \doteq h(g(u), z, g(v))\) | \(x \doteq g(u)\), \(g(y) \doteq z\), \(z \doteq g(v)\), (2), (3) | — |
| 2 | eliminate | \(x \doteq g(u)\) | \(g(y) \doteq z\), \(z \doteq g(v)\), (2), \(g(g(u)) \doteq g(g(u))\) | \(x \doteq g(u)\) |
| 3 | swap | \(g(y) \doteq z\) | \(z \doteq g(y)\), \(z \doteq g(v)\), (2), \(g(g(u)) \doteq g(g(u))\) | \(x \doteq g(u)\) |
| 4 | eliminate | \(z \doteq g(y)\) | \(g(y) \doteq g(v)\), (2), \(g(g(u)) \doteq g(g(u))\) | \(x \doteq g(u)\), \(z \doteq g(y)\) |
| 5 | decompose | \(g(y) \doteq g(v)\) | \(y \doteq v\), (2), \(g(g(u)) \doteq g(g(u))\) | \(x \doteq g(u)\), \(z \doteq g(y)\) |
| 6 | eliminate | \(y \doteq v\) | (2), \(g(g(u)) \doteq g(g(u))\) | \(x \doteq g(u)\), \(z \doteq g(v)\), \(y \doteq v\) |
| 7 | decompose | \(f(u, a) \doteq f(b, w)\) | \(u \doteq b\), \(a \doteq w\), \(g(g(u)) \doteq g(g(u))\) | unchanged |
| 8 | eliminate | \(u \doteq b\) | \(a \doteq w\), \(g(g(b)) \doteq g(g(b))\) | \(x \doteq g(b)\), \(z \doteq g(v)\), \(y \doteq v\), \(u \doteq b\) |
| 9 | swap | \(a \doteq w\) | \(w \doteq a\), \(g(g(b)) \doteq g(g(b))\) | unchanged |
| 10 | eliminate | \(w \doteq a\) | \(g(g(b)) \doteq g(g(b))\) | \(\dots\), \(w \doteq a\) |
| 11 | delete | \(g(g(b)) \doteq g(g(b))\) | — | \(x \doteq g(b)\), \(z \doteq g(v)\), \(y \doteq v\), \(u \doteq b\), \(w \doteq a\) |
- Every rule fires at least once. Step 4 is the interesting eliminate: substituting \(z \mapsto g(y)\) into the pending \(z \doteq g(v)\) turns it into \(g(y) \doteq g(v)\), a new decomposable equation.
- Step 2 rewrote equation (3) into a trivial one, removed by delete at step 11 — the final no-change step.
- The solved form is \(\theta_0\) exactly; Robinson found the same substitution.
Try it
./course drill unification --seed 7 --difficulty hard --solution prints this three-algorithm trace for a random system; --difficulty medium includes failing systems.
Union-find unification¶
Algorithm 7.1.10 on \(E_0\) (step = one pop of the stack; the classes are shown as they grow):
| step | pair popped | action | classes afterwards (non-singleton) |
|---|---|---|---|
| 1 | \(h(x, g(y), z)\), \(h(g(u), z, g(v))\) | same symbol: union, push 3 argument pairs | \(\{h_1, h_2\}\) |
| 2 | \(x\), \(g(u)\) | union (schema \(g(u)\)) | \(\{x, g(u)\}\) |
| 3 | \(g(y)\), \(z\) | union (schema \(g(y)\)) | \(\{z, g(y)\}\) |
| 4 | \(z\), \(g(v)\) | schemas \(g(y)\), \(g(v)\): union, push \((y, v)\) | \(\{z, g(y), g(v)\}\) |
| 5 | \(y\), \(v\) | union | \(\{y, v\}\) |
| 6 | \(f(u, a)\), \(f(b, w)\) | union, push \((u, b)\), \((a, w)\) | \(\{f_1, f_2\}\) |
| 7 | \(u\), \(b\) | union (schema \(b\)) | \(\{u, b\}\) |
| 8 | \(a\), \(w\) | union (schema \(a\)) | \(\{w, a\}\) |
| 9 | \(g(x)\), \(g(g(u))\) | union, push \((x, g(u)')\) | \(\{g(x), g(g(u))\}\) |
| 10 | \(x\), \(g(u)'\) | \(g(u)'\) is the inner node of equation (3), not the node of step 2: schemas \(g(u)\), \(g(u)'\) agree; union, push \((u, u)\) | \(\{x, g(u), g(u)'\}\) |
| 11 | \(u\), \(u\) | same class | unchanged |
| 12 | — | cycle check: acyclic; read back | — |
Step 10 shows why the term graph has one node per occurrence of an application: the two \(g(u)\) are distinct nodes until unification merges them, while the variable \(u\) is a single node from the start. The read-back gives \(x \mapsto g(b)\), \(u \mapsto b\), \(w \mapsto a\), \(z \mapsto g(y)\), \(v \mapsto y\): the class \(\{y, v\}\) picked \(y\) as its representative variable where Martelli–Montanari chose \(v\). The two substitutions are equal up to the renaming \(y \leftrightarrow v\), as Definition 7.1.3 allows.
The occurs check¶
\(E_{\mathrm{occ}} = \{h(x, g(y), z) \doteq h(g(z), z, g(x))\}\) under Martelli–Montanari:
| step | rule | equation | worklist after | solved after |
|---|---|---|---|---|
| 1 | decompose | \(h(x, g(y), z) \doteq h(g(z), z, g(x))\) | \(x \doteq g(z)\), \(g(y) \doteq z\), \(z \doteq g(x)\) | — |
| 2 | eliminate | \(x \doteq g(z)\) | \(g(y) \doteq z\), \(z \doteq g(g(z))\) | \(x \doteq g(z)\) |
| 3 | swap | \(g(y) \doteq z\) | \(z \doteq g(y)\), \(z \doteq g(g(z))\) | \(x \doteq g(z)\) |
| 4 | eliminate | \(z \doteq g(y)\) | \(g(y) \doteq g(g(g(y)))\) | \(x \doteq g(g(y))\), \(z \doteq g(y)\) |
| 5 | decompose | \(g(y) \doteq g(g(g(y)))\) | \(y \doteq g(g(y))\) | unchanged |
| 6 | check | \(y \doteq g(g(y))\) | fail occurs |
— |
Robinson reaches the same verdict at its third disagreement pair (\(y\) / \(g(g(y))\)). The union-find algorithm performs no check during the loop: it merges \(\{x, g(z)\}\), \(\{z, g(y), g(x)\}\) and then \(\{y, x\}\) (5 steps), and the final cycle test finds \(x \to z \to y = x\) through the schemas \(g(z)\) and \(g(y)\). \(E_{\mathrm{clash}}\) fails at its second decomposed equation, \(a \doteq b\), in all three algorithms.
4. Invariants and correctness¶
Robinson's algorithm¶
Lemma 7.1.13 (Robinson's invariant)
Before every iteration, \(\theta\) is idempotent and every unifier \(\theta'\) of \(E\) satisfies \(\theta' = \theta'\theta\).
Proof
Initialization: \(\theta = []\). Maintenance: suppose the invariant holds and the step binds \(x \mapsto r\), where \((x, r)\) or \((r, x)\) is the disagreement pair of \(\theta s_i, \theta t_i\). Let \(\theta'\) unify \(E\). By the invariant \(\theta' = \theta'\theta\), so \(\theta'\) unifies \(\theta s_i \doteq \theta t_i\) too, and therefore also the subterms at the disagreement position: \(\theta' x = \theta' r\). Then for every variable \(y\): if \(y = x\), \(\theta'[x \mapsto r]y = \theta' r = \theta' x\); otherwise \(\theta'[x \mapsto r] y = \theta' y\). So \(\theta' = \theta'[x \mapsto r]\), and \(\theta' = \theta'\theta = \theta'[x \mapsto r]\theta\). Idempotence: \(x \notin \mathrm{dom}(\theta)\) because \(x\) occurs in \(\theta s_i\) or \(\theta t_i\) and \(\theta\) is idempotent; \(x \notin \mathrm{vars}(r)\) by the occurs check; composing replaces \(x\) by \(r\) in the range of \(\theta\), so after the step no domain variable occurs in the range.
Theorem 7.1.14 (Robinson is correct and terminates)
Algorithm 7.1.7 terminates. If it returns \(\theta\), then \(\theta\) is an idempotent MGU of \(E\). If it fails, \(E\) has no unifier.
Proof
Termination: each iteration binds a variable \(x\) that occurs in \(\theta E\) and removes it from \(\theta E\) for good (the new \(\theta\) maps \(x\) to \(r\), which does not contain \(x\), and idempotence keeps \(x\) out of every range). The number of distinct variables of \(\theta E\) therefore decreases strictly, so there are at most \(\lvert \mathrm{vars}(E) \rvert\) iterations. Success: the loop exits only when \(\theta\) unifies every equation, and by Lemma 7.1.13 every unifier \(\theta'\) equals \(\theta'\theta\), so \(\theta \preceq \theta'\). Failure by clash: a disagreement pair \(f(\dots)\) / \(g(\dots)\) with \(f \ne g\) (or different arities) cannot be made equal by any substitution, which never changes the head of an application; since every unifier of \(E\) unifies \(\theta E\) (Lemma 7.1.13), there is none. Failure by occurs: \(x \ne r\) with \(x \in \mathrm{vars}(r)\), so \(r\) is an application strictly containing \(x\), and \(\lvert \theta' r \rvert > \lvert \theta' x \rvert\) for every \(\theta'\); no unifier exists (Lemma 7.1.18).
Martelli–Montanari¶
Theorem 7.1.15 (Martelli–Montanari: soundness, completeness, termination)
Every rule except conflict and check preserves the set of unifiers of the store. Algorithm 7.1.8 terminates; it returns a solved form \(S\) with \(U(S) = U(E)\) (so \(\theta_S\) is an MGU by Lemma 7.1.5) or fails, and it fails only when \(U(E) = \emptyset\).
Proof
Rules preserve \(U\): delete — \(t \doteq t\) is satisfied by every substitution. Decompose — \(\theta f(\bar s) = \theta f(\bar t)\) iff \(\theta s_i = \theta t_i\) for all \(i\), by the homomorphic definition of application. Swap — equality is symmetric. Eliminate — if \(\theta x = \theta t\) then for any term \(r\), \(\theta r = \theta([x \mapsto t] r)\) (induction on \(r\): the only difference is at occurrences of \(x\), where both sides give \(\theta t\)); so a \(\theta\) satisfying \(x \doteq t\) satisfies an equation iff it satisfies its rewritten form. Conflict and check detect empty \(U\): a substitution never changes the head symbol of an application, and \(\lvert \theta t \rvert > \lvert \theta x \rvert\) when \(x\) occurs strictly inside \(t\). Termination (the measure of [MM82, Theorem 2.3], adapted to the list strategy): order triples \((n_1, n_2, n_3)\) lexicographically, with \(n_1\) the number of variables that occur in \(\mathit{todo}\) and are not left-hand sides of \(\mathit{solved}\), \(n_2\) the total size of the terms in \(\mathit{todo}\), and \(n_3\) the number of equations in \(\mathit{todo}\) of the form \(t \doteq x\) with \(t\) not a variable. Eliminate removes every occurrence of \(x\) from \(\mathit{todo}\) and never adds one, so \(n_1\) drops. Delete and decompose do not increase \(n_1\) and decrease \(n_2\) (decompose drops two symbol occurrences). Swap leaves \(n_1, n_2\) unchanged and decreases \(n_3\). The triples are well-founded. Result: at exit \(\mathit{todo} = \emptyset\), and by Lemma 7.1.16 \(\mathit{solved}\) is in solved form with \(U(\mathit{solved}) = U(E)\).
Lemma 7.1.16 (The store invariant of Algorithm 7.1.8)
Before each iteration: \(U(\mathit{todo} \cup \mathit{solved}) = U(E)\); \(\mathit{solved}\) is in solved form; no left-hand variable of \(\mathit{solved}\) occurs in \(\mathit{todo}\).
Proof
Initially \(\mathit{solved}\) is empty. The rules other than eliminate change only \(\mathit{todo}\) and preserve \(U\) (Theorem 7.1.15), and they introduce no variables, so the third clause is kept. Eliminate on \(x \doteq t\) with \(x \notin \mathrm{vars}(t)\): \(x\) is not a left-hand side of \(\mathit{solved}\) (by the third clause, since \(x\) occurs in \(\mathit{todo}\)); after substituting \([x \mapsto t]\) everywhere, \(x\) occurs nowhere else, and the old left-hand sides do not occur in \(t\) (third clause), so appending \(x \doteq t\) keeps the solved form; \(U\) is preserved by the eliminate argument of Theorem 7.1.15.
Union-find unification¶
Theorem 7.1.17 (Union-find unification is correct)
Algorithm 7.1.10 terminates after at most \(N - 1\) unions, where \(N\) is the number of nodes. It fails iff \(U(E) = \emptyset\), and on success the read-back substitution is an MGU of \(E\).
Proof sketch (full proof: [Hue76]; textbook version: [BS01])
Termination: every popped pair either finds its roots equal (no push) or performs one union, which decreases the number of classes; a union pushes at most \(k\) pairs (\(k\) the maximum arity), so at most \((N - 1)k + \lvert E \rvert\) pairs are ever pushed. Soundness of the classes (the first invariant of the box): a pair is pushed only if it is an equation of \(E\) or corresponding arguments of two schemas already forced equal; by induction on the steps, every unifier maps the two nodes to equal terms, and equality is transitive, so whole classes are forced. Clash: two forced-equal nodes with different head symbols admit no unifier. Completeness of the classes (the second invariant): every pair that the congruence closure of \(E\) would identify is pushed at the moment its parents are merged, because the merge pushes all argument pairs of the two schemas; at exit, the classes are closed under decomposition. Occurs: a cycle through schemas means some class \(c\) has a schema whose argument chain returns to \(c\), so every unifier maps a term to a strict subterm of itself — impossible (Lemma 7.1.18). If the graph is acyclic, read-back terminates and the substitution maps both sides of each equation to the read-back of their common class: it is a unifier, and it is most general because it identifies only forced classes and invents no symbols.
The occurs check¶
Lemma 7.1.18 (No finite solution to a cycle)
If \(x \ne t\) and \(x \in \mathrm{vars}(t)\), then \(x \doteq t\) has no unifier over finite terms. Over rational trees it has exactly one solution for \(x\) once the other variables of \(t\) are fixed, if \(t\) is not a variable.
Proof
Finite terms: \(t\) is an application containing \(x\) at some depth \(d \ge 1\), so for any \(\theta\), \(\theta x\) is a proper subterm of \(\theta t\) and \(\lvert \theta t \rvert \ge \lvert \theta x \rvert + d > \lvert \theta x \rvert\); they cannot be equal. Rational trees: the equation \(x = t[x]\) is a guarded recursive definition (each occurrence of \(x\) is below a function symbol); unfolding it defines the tree level by level, and any two solutions agree up to every depth \(d\) by induction on \(d\), hence are equal. This is why ocaml -rectypes can give fun x -> x x the type ('a -> 'b as 'a) -> 'b (§7).
Skipping the check is not an optimization, it changes the language
Without an occurs check, a unifier over finite terms produces cyclic terms that the rest of the compiler assumes cannot exist: printing loops, type equality loops, and the soundness proof of Lesson 7.2 fails. Prolog accepts this trade-off (its default unification omits the check), OCaml exposes it as a flag with a separate theory (equi-recursive types). A type checker that forgets it by accident is simply wrong.
5. Complexity¶
| Technique | Time (worst) | Time (typical) | Space | Variables |
|---|---|---|---|---|
| Robinson (trees, composed \(\theta\)) | exponential: \(\Omega(2^n)\) on \(E_n\) below | fast for small types | exponential output | \(n\) equations of \(E_n\) (input size \(\Theta(n)\)) |
| Martelli–Montanari (trees) | exponential on \(E_n\) (eliminate copies terms) | as Robinson | exponential | the same |
| Union-find (Huet) | \(O(N\,\alpha(N) \cdot k)\) | near-linear | \(O(N)\) | \(N\) nodes of the term graph, \(k\) max arity, \(\alpha\) inverse Ackermann |
| Paterson–Wegman | \(O(N)\) | slower constants than Huet in practice | \(O(N)\) | as above |
| Occurs check | eager: \(O(\lvert t \rvert)\) per binding, \(O(N^2)\) total; deferred: one \(O(N)\) DFS | eager dominates on long chains | \(O(N)\) | \(N\) nodes |
Justification. Robinson and MM on trees: on the pathological family below, the MGU itself, written as trees, has \(2^{n+1} - 1\) nodes for \(x_n\), so any algorithm that builds tree-shaped substitutions spends \(\Omega(2^n)\). Union-find: by Theorem 7.1.17 there are at most \(N - 1\) unions and \((N - 1)k + \lvert E \rvert\) pushes; each pop does two finds, so \(O(Nk)\) finds and unions, each \(O(\alpha(N))\) amortized with union by rank and path compression [Tar75]; the final DFS visits each class and schema edge once, \(O(Nk)\). Eager occurs check: at most one binding per variable, each check traverses at most \(N\) nodes: \(O(N^2)\). Deferring it to one DFS is what keeps Huet's bound.
Pathological family. \(E_n = \{\, x_1 \doteq f(x_0, x_0),\ x_2 \doteq f(x_1, x_1),\ \dots,\ x_n \doteq f(x_{n-1}, x_{n-1}) \,\}\) has input size \(4n\) symbol occurrences. Let \(s(i) = \lvert \theta x_i \rvert\) in the MGU: \(s(0) = 1\) and \(s(i) = 2 s(i-1) + 1\), so \(s(n) = 2^{n+1} - 1\). Martelli–Montanari, eliminating \(x_1, x_2, \dots\) in order, substitutes a term of size \(s(i-1)\) into the remaining equations at step \(i\), doing \(\Theta(2^i)\) work, \(\Theta(2^n)\) in all. Union-find creates \(2n + 1\) variable and application nodes, performs \(n\) unions and never copies: \(\Theta(n)\). The test test_exponential_family in tools/course/tests/test_ch07.py checks both sizes for \(n = 10\). Type inference meets this family whenever types are duplicated by instantiation (Lesson 7.3 §5); OCaml, which unifies with sharing, compiles the 14-level pair tower of Lesson 7.3 in 0.38 s, but ocamlc -i needs 6.1 s to print its interface of 850 896 characters (measured on the course container with OCaml 4.14.1; Lesson 7.3 §7).
6. Variants and refinements¶
Robinson's algorithm¶
- Triangular substitutions [BS01]: keep bindings \(x \mapsto t\) without applying them to earlier ranges; look variables up by chasing bindings. Trade-off: binding is \(O(1)\) and nothing is copied, but every lookup walks a chain; this is Prolog's (the WAM's) representation.
- One-sided matching (Lesson 6.4, Algorithm 6.4.6; Clang's template deduction, §7): only one side has variables, so no occurs check is needed and the result is unique. Trade-off: less general — it cannot relate two unknowns.
- Structure sharing: apply Robinson over a DAG so that composed substitutions share subterms. Trade-off: saves space, not time, unless equal subterms are also remembered as equal — which is union-find.
Martelli–Montanari¶
- Multi-equations [MM82, §4–5]: group all terms known equal to a set of variables into one "multiequation" and choose the next one to eliminate by counting references, avoiding repeated substitution. Trade-off: efficient, but the bookkeeping is heavy compared with union-find.
- E-unification [BS01]: add rules for an equational theory (associativity-commutativity, Boolean rings); the rule system extends where Robinson's loop does not. Trade-off: MGUs may not exist (infinitely many incomparable unifiers) and the problem may be undecidable.
- Constraint stores with other relations (Lesson 7.4): keep the rule system but let the store contain class constraints and implications (HM(X), OutsideIn(X)). Trade-off: more expressive, harder to guarantee principal solutions.
Union-find unification¶
- Paterson–Wegman linear unification [PW78]: process the term DAG in a topological order so that each node is unified once. Trade-off: \(O(N)\) worst case, but more complex and slower in practice than Huet's almost-linear algorithm.
- Rank- or level-directed linking: when two variables meet, link the one with the deeper level to the shallower (Lesson 7.3, Rémy [Rem92]); this makes generalization a level comparison. Trade-off: one integer per variable, and every unification must maintain levels.
- Undoable union-find (rustc's inference tables, Swift's solver, §7): record every link in a trail so that a failed speculative branch can be rolled back. Trade-off: no path compression across snapshots, some memory for the trail; necessary for overload resolution by search (Lesson 7.5).
The occurs check¶
- Omitting it (Prolog by default; ISO Prolog provides
unify_with_occurs_check/2for the checked version) [BS01]. Trade-off: linear-time unification and cyclic terms; unsound for first-order logic and for type systems that assume finite types. - Rational-tree unification / equi-recursive types [Hue76]: accept cyclic solutions and treat them as infinite types (
ocaml -rectypes). Trade-off: more programs type-check, including many that are mistakes; errors appear far from the cause. - Deferred cycle detection (Algorithm 7.1.12's
HasCycle) [Hue76]: one linear DFS instead of a check per binding. Trade-off: the failure is detected late, so the error message must be reconstructed from the cycle.
7. In real compilers¶
Robinson's algorithm¶
Clang deduces template arguments by structurally matching each parameter type against its argument type: DeduceTemplateArgumentsByTypeMatch in clang/lib/Sema/SemaTemplateDeduction.cpp recurses through pointers, references, function types and template specializations like Robinson's disagreement search, records one deduced value per template parameter, and returns TemplateDeductionResult::Inconsistent when a parameter receives two different values [CLANG-Deduce]. It is one-sided per argument (the argument types are known), which is why no occurs check appears. GHC's pure unifier for instance matching (GHC.Core.Unify) and the course's oracle hm.robinson are two-sided.
Template argument deduction in Clang 23: decomposition and inconsistent bindings
Reproduce (clang 23.1.2):
mkdir -p cc && cat > cc/deduce.cpp <<'EOF'
#include <utility>
template <class T> T pick(T a, T b) { return a < b ? b : a; }
template <class T, class U> void same(std::pair<T, U>, std::pair<U, T>) {}
int main() {
auto x = pick(1, 2); // T = int
same(std::pair<int, char>{}, std::pair<char, int>{}); // T = int, U = char
auto y = pick(1, 2.5); // T = int and T = double
same(std::pair<int, char>{}, std::pair<int, char>{}); // U = char vs U = int
}
EOF
clang++-23 -std=c++23 -fsyntax-only cc/deduce.cpp
Output (complete):
cc/deduce.cpp:8:14: error: no matching function for call to 'pick'
8 | auto y = pick(1, 2.5); // T = int and T = double
| ^~~~
cc/deduce.cpp:2:22: note: candidate template ignored: deduced conflicting types for parameter 'T' ('int' vs. 'double')
2 | template <class T> T pick(T a, T b) { return a < b ? b : a; }
| ^
cc/deduce.cpp:9:5: error: no matching function for call to 'same'
9 | same(std::pair<int, char>{}, std::pair<int, char>{}); // U = char vs U = int
| ^~~~
cc/deduce.cpp:3:34: note: candidate template ignored: deduced conflicting types for parameter 'U' ('char' vs. 'int')
3 | template <class T, class U> void same(std::pair<T, U>, std::pair<U, T>) {}
| ^
2 errors generated.
What to notice: same solves \(\{\mathit{pair}(T, U) \doteq \mathit{pair}(\mathsf{int}, \mathsf{char}),\ \mathit{pair}(U, T) \doteq \mathit{pair}(\mathsf{int}, \mathsf{char})\}\): decomposition gives \(T \doteq \mathsf{int}\), \(U \doteq \mathsf{char}\), \(U \doteq \mathsf{int}\), \(T \doteq \mathsf{char}\), and the first conflict found is on \(U\) — the "clash" of Theorem 7.1.14, reported with both values. (On Linux, add --gcc-install-dir=… if your clang does not find a C++ standard library.)
Martelli–Montanari¶
GHC's constraint solver keeps equalities in a work list and rewrites them with rules: canEqNC in compiler/GHC/Tc/Solver/Canonical.hs decomposes an equality between two applications of the same type constructor into equalities between the arguments, reports a mismatch between different constructors, orients equalities so that a variable is on the left, and hands tv ~ ty to the inert set, which substitutes it into other constraints — decompose, conflict, swap and eliminate [GHC-Canonical]. The error message still names the whole types from which the failing equation was decomposed.
Decomposition in GHC 9.4: the failing equation inside two larger types
Reproduce (GHC 9.4.7):
mkdir -p hs && cat > hs/Decomp.hs <<'EOF'
module Decomp where
same :: (a, [a]) -> Int
same _ = 0
use :: Int
use = same (True, [length "ab"])
EOF
LC_ALL=C ghc -fno-code hs/Decomp.hs
Output (the [1 of 1] Compiling line removed):
hs/Decomp.hs:5:20: error:
* Couldn't match expected type `Bool' with actual type `Int'
* In the expression: length "ab"
In the expression: [length "ab"]
In the first argument of `same', namely `(True, [length "ab"])'
|
5 | use = same (True, [length "ab"])
| ^^^^^^^^^^^
What to notice: the constraint \((a, [a]) \sim (\mathsf{Bool}, [\mathsf{Int}])\) is decomposed into \(a \sim \mathsf{Bool}\) (eliminated first) and \([a] \sim [\mathsf{Int}]\), which after substitution decomposes to \(\mathsf{Bool} \sim \mathsf{Int}\) — a conflict. GHC reports the innermost failing pair and lists the enclosing expressions it came from: the rows of the §3 trace, read backwards.
Union-find unification¶
OCaml unifies in place: Ctype.unify in typing/ctype.ml links a type variable node to the other type (link_type) instead of building substitutions, and the type graph is shared [OCAML-Ctype]. rustc keeps its inference variables in union-find tables from the ena crate — one table for general type variables, and separate ones for integer and float literal variables (int_unification_table in compiler/rustc_infer/src/infer/mod.rs) [RUSTC-Infer]. LLVM has a general union-find, EquivalenceClasses in llvm/include/llvm/ADT/EquivalenceClasses.h (leader pointers with path compression in getLeader), used by several passes to merge equivalent values [LLVM-EqClasses].
Sharing in OCaml 4.14's unifier: a type that is small in memory and huge on paper
Reproduce (OCaml 4.14.1):
mkdir -p ml && for n in 4 6 8 10 12; do
{ echo "let x0 = fun z -> z"; for i in $(seq 1 $n); do echo "let x$i = (x$((i-1)), x$((i-1)))"; done; } > ml/tower$n.ml
printf 'n=%-3s %8s characters\n' $n "$(ocamlc -i ml/tower$n.ml | sed -n "/^val x$n /,\$p" | wc -c)"
done
Output (complete):
n=4 253 characters
n=6 1105 characters
n=8 4689 characters
n=10 22848 characters
n=12 101998 characters
What to notice: each let doubles the printed type of the last binding (the factor exceeds 4 per two levels because the variable names 'a, …, 'ba, … grow longer), yet the unifier never copies it: x_i's type is one pair node pointing twice to x_(i-1)'s — the term graph of Definition 7.1.9. The cost of printing is the tree size \(2^{n+1}\) of §5; the cost of unifying is the graph size.
The occurs check¶
Every production type checker for finite types performs it: OCaml's Ctype.occur [OCAML-Ctype], GHC's occurs check when a variable is about to be filled (checkTyEqRhs-style checks in GHC.Tc.Utils.Unify [GHC-Unify]), rustc's generalizer before instantiating a type variable [RUSTC-Infer]. OCaml's -rectypes switches to rational trees.
The occurs check in OCaml 4.14 and SML/NJ 110.79, and OCaml's rational trees
Reproduce (OCaml 4.14.1, SML/NJ 110.79):
mkdir -p ml sml
echo 'let self_apply = fun x -> x x' > ml/occurs.ml
ocamlc -i ml/occurs.ml
ocamlc -rectypes -i ml/occurs.ml
echo 'val self_apply = fn x => x x' > sml/occurs.sml
sml sml/occurs.sml < /dev/null
Output (the SML/NJ banner and its final Uncaught exception lines removed):
File "ml/occurs.ml", line 1, characters 28-29:
1 | let self_apply = fun x -> x x
^
Error: This expression has type 'a -> 'b
but an expression was expected of type 'a
The type variable 'a occurs inside 'a -> 'b
val self_apply : ('a -> 'b as 'a) -> 'b
[opening sml/occurs.sml]
sml/occurs.sml:1.27-1.30 Error: operator is not a function [circularity]
operator: 'Z
in expression:
x x
What to notice: the equation is \(\alpha \doteq \alpha \to \beta\) (the type of x must be a function taking x); OCaml's check names it exactly ("occurs inside"). With -rectypes the same unifier skips the check and prints the rational solution with an as binder — the cyclic graph of Definition 7.1.11. SML/NJ calls the same failure a "circularity".
8. Comparison¶
| Technique | Power / precision | Speed (asymptotic · practical) | Output / error quality | Implementation effort | Typical use |
|---|---|---|---|---|---|
| Robinson's algorithm | Computes an MGU or proves none exists (Theorem 7.1.14) | Exponential on \(E_n\) with trees · fine for small types | Reports the first disagreement pair: two concrete subterms | Lowest: one loop, one substitution | Textbooks, theorem provers, one-sided template deduction (Clang) |
| Martelli–Montanari | Same solutions, with a proof that separates rules from strategy (Theorem 7.1.15); extends to E-unification and constraint stores | Exponential with trees; efficient with multi-equations [MM82] · rule-at-a-time | The failing rule and equation, and the history of rewrites that produced it | Low for the rules; strategy and data structures chosen separately | Specifications, GHC's canonicalizer, constraint solvers |
| Union-find unification | Same solutions (Theorem 7.1.17), on shared graphs | \(O(N\,\alpha(N) k)\) · near-linear; the §5 family in linear time | Failures found on classes; messages must re-read the terms | Medium: union-find, schemas, read-back, cycle check | OCaml, GHC, rustc (ena), Swift, Pebble's inferTypes (E2) |
| The occurs check | Excludes exactly the cyclic solutions (Lemma 7.1.18) | Eager: \(O(N^2)\) total; deferred: \(O(N)\) | Eager: at the offending binding; deferred: needs reconstruction | Low | Every type checker for finite types; omitted by Prolog; relaxed by -rectypes |
Choose Robinson for a first implementation, for one-sided matching, and when types are tiny. Choose Martelli–Montanari as the specification of any solver you write and when you need to extend unification with new rules. Choose union-find for a production inference engine: it is the only one of the three with near-linear behavior on shared types, and the one every compiler in §7 uses. Perform the occurs check unless your type system has recursive types by design; defer it to a cycle check if bindings dominate your profile.
9. Assessment¶
| Technique | Quiz ids | Drill | Flashcard tag | Exercises |
|---|---|---|---|---|
| Robinson's algorithm | unify-mgu, find-clang-deduction |
unification (Robinson table in --solution) |
robinson |
— |
| Martelli–Montanari | mm-rule-sequence, mm-termination-measure |
unification |
martelli-montanari |
— |
| Union-find unification | uf-unions, find-llvm-equivalence-classes |
unification (union-find summary) |
union-find-unification |
E2 (Pebble's numeric variables); lab L2 |
| The occurs check | occurs-verdict, occurs-rectypes |
unification (fail: occurs answers) |
occurs-check |
lab L1 (ErrorKind::Occurs) |
References¶
See the chapter references.