Unification, substitution sets, and the most general unifier

Why matching needs an algorithm

Modus ponens requires the antecedent of a rule to *match* a known fact. In propositional logic matching is trivial — two formulas are identical or they are not. In predicate calculus, variables make matching non-trivial: $man(X)$ should match $man(socrates)$ by binding $X = socrates$. Unification is the algorithm that finds the variable substitutions making two expressions *syntactically identical* — it is the computational core of Prolog and of resolution.

Substitutions and the mgu

A substitution binds variables to terms, written $\{socrates/X\}$ ("$socrates$ for $X$"). The set of bindings carried through a chain of inferences is the substitution set, and consistency must hold across it: once $X$ is bound to $socrates$, every later $X$ in scope is $socrates$.

When several substitutions could unify two expressions, we want the most general unifier (mgu) — the *least committed* one, introducing fresh variables rather than arbitrary constants. Unifying $p(X)$ with $p(Y)$: the substitution $\{fred/X, fred/Y\}$ works but needlessly forces both to $fred$; the mgu $\{Z/X, Z/Y\}$ only forces them to be *equal*, leaving every future match open. Any other unifier can be obtained from the mgu by a further substitution. The mgu is unique up to renaming variables.

The algorithm (list form) and the occurs check

The textbook writes expressions as lists with the predicate/function name as head, so $p(X, f(Y))$ is ['p', 'X', ['f', 'Y']] — this erases the predicate/function distinction and makes matching pure list recursion. The cases:

1. Identical expressions unify with the empty substitution {}.
2. A variable $V$ not occurring in the other expression $E$ unifies via $\{E/V\}$.
3. Two lists unify by recursively unifying their heads, applying that substitution to the tails, recursively unifying the tails, and composing the two substitution sets.

The two failure cases are mismatched constants (e.g. a vs b) and the occurs check: a variable may not unify with a term *containing that same variable* — $X$ with $f(X)$ would build the infinite term $f(f(f(\dots)))$. The occurs check guards against it.

Substitution composition $SS'$ applies $S'$ to the bindings of $S$ then adds $S'$; it is associative but not commutative — order matters.

Worked example: unify $p(X, f(Y))$ with $p(a, f(b))$

Heads p = p ✓. First arg: $X$ vs $a$ → bind $\{a/X\}$. Apply to the rest, then second arg: $f(Y)$ vs $f(b)$ → heads f=f, then $Y$ vs $b$ → bind $\{b/Y\}$. Compose: the mgu is $\{a/X, b/Y\}$, i.e. {X: a, Y: b}. By contrast $p(X, X)$ vs $p(a, b)$ binds $X = a$ from the first argument, but then the second argument needs $X = b$ — inconsistent — so unification returns FAIL. The Python implementation below prints exactly that.