UNIFICATION the one substitution that makes two terms equal
Given two terms with variables — say f(X, b) and f(a, Y) — is there a single assignment that makes them literally the same term? Unification returns the most general one (here {X→a, Y→b}) — committing to exactly what the terms force and no more. It is the hidden engine under Prolog, Hindley-Milner (dart 135), term rewriting, and theorem proving; every logical variable that gets solved is one unification step.
THE TECHNIQUE walk in lockstep; bind; occurs-check
Same functor and arity → recurse on argument pairs. A variable meets a term → bind it (after the occurs-check: the variable must not appear inside the term, or you would build an infinite term). Two different constants → fail. Below: a clean success, a symbol clash, and an occurs-check failure. live demo
HISTORY & CREDIT Herbrand had it in 1930
“Robinson invented unification” — the idea is hisHerbrand’s (1930 thesis, term-equation systems). Robinson (1965) named it and put it at the center of machine proof. cited
1930 · Jacques Herbrand — an algorithm for solving systems of equations between first-order terms, 35 years before the name. 1965 · J. Alan Robinson — resolution, whose heart is unification computing the most general unifier with the occurs-check. Correct, but worst-case exponential (the MGU written as a tree can blow up 2n). 1972–74 · Prolog (Colmerauer, Kowalski) is built on it — but its default =/2omits the occurs-check for speed, trading soundness (you can “unify” X with f(X)). 1978 / 1982 · linear unification has two parents: Paterson & Wegman (the truly O(n) DAG algorithm) and Martelli & Montanari (the transformation-rule form, near-linear with union-find) — the blow-up was a representation choice, not an inherent cost.
“Most general” is a technical claim: the MGU is the least element (up to renaming) in the lattice of unifiers — every other unifier is an instance of it. Robinson, 1965
RECOMMEND FOR I-13 a term is a flat tagged array; subst threads
A first-order term is a flat node array (var / const), the substitution is an f64 array of bindings, and the three cases land exactly:
$ i13 run unify.i13 # vars X=-1 Y=-2 ; consts a=101 b=102 ; subst threaded
f(X,b) ~ f(a,Y) -> ok=1, subst {X=101(a), Y=102(b)} the MGU
f(X,X) ~ f(a,b) -> ok=0 FAIL: X bound to a, then a != b (consistency)
X ~ f(X) -> ok=0 FAIL: occurs-check (X inside f(X) would be infinite)
Recommend: the scoped unifier is LIT — variables are negative f64 codes, constants positive; the substitution is an f64 array indexed by variable id; resolve dereferences a bound var by recursion; binding is a value-semantic array update (verified f(X,b)~f(a,Y) → X=a, Y=b; and f(X,X)~f(a,b) → FAIL by the same-variable consistency check). Note: the frontier is arbitrary nested terms — a general term is a tree of nodes (a node arena, PS-015), and the full occurs-check walks that tree. The demo animates the node-pool unifier incl. occurs-check; the compiler grounds the bind + clash + consistency on flat argument arrays. It is the engine dart 135 (Hindley-Milner) runs on.