Unification: Matching Terms with Variables

in progressThis lesson is still being built - content, demos, and checkpoints may change before release.

Unification

Loading interactive demo…

The two terms are drawn as trees side by side, function symbols over their arguments and variables as hollow nodes, and redrawn after every binding with the bindings applied, so the trees grow alike as unification proceeds. Below them, the pending strip is the stack of pairs still to compare and the bindings strip the substitution so far.Take the tour, or press and explore. Legend:

The panel beside the stage is the real Unifier class from the published library executing in your browser, with the current line highlighted.

The two subterms under comparison, and the pair just taken off the stack.
The variable just bound and the term it stands for; a finished unifier.
A clash or a failed occurs check; the tapped variable wherever it still occurs.
A bound variable in the strip.
A variable not yet bound, hollow.

compared counts the pairs taken off the stack, bindings the variables bound so far, pending the pairs still on the stack, result whether the terms unified or why they could not. Tap a variable to light it.

The code panel shows bare executable code by default. The bar above it names the file (hover the name for the full published path); options holds the toggles: comments, the tracer instrumentation that produces this visualization, and verbose names for the terse identifiers (display only: the default is the byte-exact published file). The view switch adds plain-English narration: both interleaves it with the code, pseudo shows only the pseudocode. hide code collapses the panel; the rail it leaves behind brings it back.

Keys: Space play/pause · ←/→ step · Home/End jump · R reset · F fullscreen · G guided tour

Terms and substitutions. A term is a variable, or a function symbol applied to terms; a constant is a symbol with no arguments. A substitution $\sigma$ maps variables to terms, and $t\sigma$ is $t$ with every variable replaced. A substitution unifies $s$ and $t$ when $s\sigma = t\sigma$ . Among unifiers there is a most general one, $\mu$ : every other unifier is $\mu$ followed by some further substitution. Unification finds $\mu$ or reports there is none.

The algorithm. Keep a stack of pairs, starting with $(s, t)$ , and a substitution, starting empty. Pop a pair and apply the substitution to both sides. If they are identical, drop them. If one is a variable $X$ not occurring in the other side $u$ , bind $X = u$ . If both are applications $f(s_1 \dots s_n)$ and $g(t_1 \dots t_m)$ , they must have $f = g$ and $n = m$ , else clash; then push the pairs $(s_i, t_i)$ . When the stack empties, the substitution is $\mu$ .

The occurs check. $X$ against $f(X)$ has no finite solution: any term $u$ for $X$ would need $u = f(u)$ , which is longer than itself. Refusing the binding keeps every term finite and the algorithm terminating. It costs a walk over $u$ at every binding, which is why Prolog omits it and lets cyclic terms happen; the stage's occurs-check pair binds $X = Y$ first, so the check must look through the substitution to see $Y$ inside $f(Y)$ .

Why bindings feed forward. The success pair binds $X = a$ on the first argument, and the second argument pair is then read as $g(a, b)$ against $g(Y, Z)$ : the substitution is applied before every comparison. Without this, $X$ could later be bound to something else and the result would not be a unifier at all.

Cost. Applying the substitution in full can blow up: a chain $X_1 = g(X_0, X_0), X_2 = g(X_1, X_1), \dots$ doubles in size at each step, and Robinson's algorithm written this way takes exponential time on such inputs. Sharing subterms as a graph, Paterson and Wegman's algorithm is linear. Prolog implementations sit between: structure sharing, a trail for undoing bindings on backtracking, and no occurs check.

Choices worth reading closely in the implementation (the code panel's comments and tracer checkboxes reveal the full published file):

Bindings are applied on the way in, not kept as a growing substitution to compose: each popped pair is rewritten under the current bindings, and applySubstitution follows a binding to a bound variable through to the end.
The stack is pushed last argument first, so the leftmost argument pair is compared next and the trace reads left to right.
One failure flag ends the loop instead of an early return, so the trace has one failed event with the reason, and the bindings made before the failure are kept in the result.
Variables are uppercase, Prolog's convention, shared with the logic programming lesson; the predicate logic lesson used the textbook's lowercase letters through the same parser.

Resolution for first-order logic needs to match a literal against its negation when both contain variables, and the match must be as general as possible or the proof search misses proofs. John Alan Robinson's 1965 paper gave the algorithm: compare the two terms symbol by symbol, bind a variable to whatever it faces, refuse to bind a variable to a term containing it, and the result is the most general unifier or a definite failure. The same procedure matches a Prolog goal to a clause head, solves the type equations of Hindley-Milner inference, and finds a redex in term rewriting.

1930Jacques Herbrand - His thesis contains, in passing, a procedure for solving equations between terms that is unification in all but name.source
1965John Alan Robinson - Defines unification, proves the most general unifier exists and is unique up to renaming, and makes it the engine of resolution.source
1969J. Roger Hindley - Uses unification to infer the principal type of a combinator; Robin Milner rediscovers it for ML in 1978.source
1976Michael Paterson and Mark Wegman - A linear-time unification algorithm on term graphs, where Robinson's can take exponential space on shared subterms.source
1982Alain Colmerauer - Prolog II drops the occurs check on purpose and gives rational, cyclic terms a meaning instead of forbidding them.source

Used today

Logic programming - Every step of a Prolog query unifies the current goal with a clause head; the bindings are the answer and the failures drive backtracking.
Type inference - A compiler generates type equations from the program and unifies them; the most general unifier is the most general type.
Pattern matching and rewriting - A rule's left-hand side is matched against a term by one-way unification; term rewriting systems and computer algebra run on it.

terms

compared: 5
bindings: 3 of 3
pending: 0
result: unified

unifier.ts

import type { Tracer } from "../trace";import { applySubstitution, occursIn, sameTerm, termText, type Term } from "./terms";export type UnifyFailure = "clash" | "occurs";export interface UnifyResult {  unified: boolean;  /** The most general unifier when unified, else the bindings made before the failure. */  bindings: Map<string, Term>;  substitution: Map<string, Term>;  failure: UnifyFailure | null;  /** Pairs compared. */  steps: number;}/** The most pairs a run compares: the occurs check keeps real runs finite, this keeps a broken term from looping. */export const MAX_UNIFY_STEPS = 200;/** * Robinson's unification: find a substitution for the variables that * makes two terms identical, and the most general such one. A stack * of pairs starts with the two terms. Each pair is compared with the * bindings so far applied: identical sides need nothing; a variable * against a term binds, unless the variable occurs inside the term, * which would need an infinite term; two function symbols must agree * in name and arity, and then their arguments pair up. The occurs * check is what Prolog omits for speed, and why it can build cyclic * terms. * * Time: O(n^2) in the terms' size with this representation. Space: * O(n). */export class Unifier {  constructor(private readonly tracer?: Tracer) {}  unify(a: Term, b: Term): UnifyResult {    const bindings = new Map<string, Term>();    const substitution = new Map<string, Term>();    const pending: [Term, Term][] = [[a, b]];    const pairsToUnify: [Term, Term][] = [[a, b]];    let failure: UnifyFailure | null = null;    let steps = 0;    while (pending.length > 0 && failure === null && steps < MAX_UNIFY_STEPS) {    while (pairsToUnify.length > 0 && failure === null && steps < MAX_UNIFY_STEPS) {      const [rawLeft, rawRight] = pending.pop()!;      const [rawLeft, rawRight] = pairsToUnify.pop()!;      const left = applySubstitution(rawLeft, bindings);      const left = applySubstitution(rawLeft, substitution);      const right = applySubstitution(rawRight, bindings);      const right = applySubstitution(rawRight, substitution);      steps += 1;      const same = sameTerm(left, right);      // ▸ take the next pair, with the bindings so far applied      this.tracer?.emit("compare", { left: termText(left), right: termText(right), same, pending: pending.length });      this.tracer?.emit("compare", { left: termText(left), right: termText(right), same, pairsToUnify: pairsToUnify.length });      if (same) continue;      if (left.kind === "variable" || right.kind === "variable") {        const [name, term] = left.kind === "variable" ? [left.name, right] : [right.name, left];        if (occursIn(name, term)) {          // ▸ the variable is inside the term: no finite solution          this.tracer?.emit("occurs-check", { variable: name, term: termText(term) });          failure = "occurs";          continue;        }        bindings.set(name, term);        substitution.set(name, term);        // ▸ a variable against a term: bind it        this.tracer?.emit("bind", { variable: name, term: termText(term), bindings: Unifier.text(bindings) });        this.tracer?.emit("bind", { variable: name, term: termText(term), substitution: Unifier.text(substitution) });        continue;      }      if (left.name !== right.name || left.args.length !== right.args.length) {        // ▸ different symbols: no binding can fix that        this.tracer?.emit("clash", { left: termText(left), right: termText(right) });        failure = "clash";        continue;      }      // ▸ same symbol and arity: the arguments pair up      this.tracer?.emit("decompose", { symbol: left.name, arity: left.args.length, pending: pending.length + left.args.length });      this.tracer?.emit("decompose", { symbol: left.name, arity: left.args.length, pairsToUnify: pairsToUnify.length + left.args.length });      // Pushed last to first, so the leftmost argument pair is compared next.      for (let i = left.args.length - 1; i >= 0; i--) pending.push([left.args[i]!, right.args[i]!]);      for (let i = left.args.length - 1; i >= 0; i--) pairsToUnify.push([left.args[i]!, right.args[i]!]);    }    if (failure === null) {      // ▸ no pairs left: the bindings are the most general unifier      this.tracer?.emit("unified", { bindings: Unifier.text(bindings), count: bindings.size, steps });      this.tracer?.emit("unified", { substitution: Unifier.text(substitution), count: substitution.size, steps });      return { unified: true, bindings, failure: null, steps };      return { unified: true, substitution, failure: null, steps };    }    // ▸ the terms have no unifier    this.tracer?.emit("failed", { reason: failure, steps });    return { unified: false, bindings, failure, steps };    return { unified: false, substitution, failure, steps };  }  /** The substitution as text, each binding with the others applied: `{X = a, Y = g(a)}`. */  static text(bindings: ReadonlyMap<string, Term>): string {  static text(substitution: ReadonlyMap<string, Term>): string {    return `{${[...bindings].map(([name, term]) => `${name} = ${termText(applySubstitution(term, bindings))}`).join(", ")}}`;    return `{${[...bindings].map(([name, term]) => `${name} = ${termText(applySubstitution(term, substitution))}`).join(", ")}}`;  }}

bindings =: {X = a, Y = a, Z = b}
steps =: 5

Unified by {X = a, Y = a, Z = b} in 5 comparisons.

import type { Tracer } from "../trace";import { applySubstitution, occursIn, sameTerm, termText, type Term } from "./terms";export type UnifyFailure = "clash" | "occurs";export interface UnifyResult { unified: boolean; /** The most general unifier when unified, else the bindings made before the failure. */ bindings: Map<string, Term>; substitution: Map<string, Term>; failure: UnifyFailure | null; /** Pairs compared. */ steps: number;}/** The most pairs a run compares: the occurs check keeps real runs finite, this keeps a broken term from looping. */export const MAX_UNIFY_STEPS = 200;/** * Robinson's unification: find a substitution for the variables that * makes two terms identical, and the most general such one. A stack * of pairs starts with the two terms. Each pair is compared with the * bindings so far applied: identical sides need nothing; a variable * against a term binds, unless the variable occurs inside the term, * which would need an infinite term; two function symbols must agree * in name and arity, and then their arguments pair up. The occurs * check is what Prolog omits for speed, and why it can build cyclic * terms. * * Time: O(n^2) in the terms' size with this representation. Space: * O(n). */export class Unifier { constructor(private readonly tracer?: Tracer) {} unify(a: Term, b: Term): UnifyResult { const bindings = new Map<string, Term>(); const substitution = new Map<string, Term>(); const pending: [Term, Term][] = [[a, b]]; const pairsToUnify: [Term, Term][] = [[a, b]]; let failure: UnifyFailure | null = null; let steps = 0; while (pending.length > 0 && failure === null && steps < MAX_UNIFY_STEPS) { while (pairsToUnify.length > 0 && failure === null && steps < MAX_UNIFY_STEPS) { const [rawLeft, rawRight] = pending.pop()!; const [rawLeft, rawRight] = pairsToUnify.pop()!; const left = applySubstitution(rawLeft, bindings); const left = applySubstitution(rawLeft, substitution); const right = applySubstitution(rawRight, bindings); const right = applySubstitution(rawRight, substitution); steps += 1; const same = sameTerm(left, right); // ▸ take the next pair, with the bindings so far applied this.tracer?.emit("compare", { left: termText(left), right: termText(right), same, pending: pending.length }); this.tracer?.emit("compare", { left: termText(left), right: termText(right), same, pairsToUnify: pairsToUnify.length }); if (same) continue; if (left.kind === "variable" || right.kind === "variable") { const [name, term] = left.kind === "variable" ? [left.name, right] : [right.name, left]; if (occursIn(name, term)) { // ▸ the variable is inside the term: no finite solution this.tracer?.emit("occurs-check", { variable: name, term: termText(term) }); failure = "occurs"; continue; } bindings.set(name, term); substitution.set(name, term); // ▸ a variable against a term: bind it this.tracer?.emit("bind", { variable: name, term: termText(term), bindings: Unifier.text(bindings) }); this.tracer?.emit("bind", { variable: name, term: termText(term), substitution: Unifier.text(substitution) }); continue; } if (left.name !== right.name || left.args.length !== right.args.length) { // ▸ different symbols: no binding can fix that this.tracer?.emit("clash", { left: termText(left), right: termText(right) }); failure = "clash"; continue; } // ▸ same symbol and arity: the arguments pair up this.tracer?.emit("decompose", { symbol: left.name, arity: left.args.length, pending: pending.length + left.args.length }); this.tracer?.emit("decompose", { symbol: left.name, arity: left.args.length, pairsToUnify: pairsToUnify.length + left.args.length }); // Pushed last to first, so the leftmost argument pair is compared next. for (let i = left.args.length - 1; i >= 0; i--) pending.push([left.args[i]!, right.args[i]!]); for (let i = left.args.length - 1; i >= 0; i--) pairsToUnify.push([left.args[i]!, right.args[i]!]); } if (failure === null) { // ▸ no pairs left: the bindings are the most general unifier this.tracer?.emit("unified", { bindings: Unifier.text(bindings), count: bindings.size, steps }); this.tracer?.emit("unified", { substitution: Unifier.text(substitution), count: substitution.size, steps }); return { unified: true, bindings, failure: null, steps }; return { unified: true, substitution, failure: null, steps }; } // ▸ the terms have no unifier this.tracer?.emit("failed", { reason: failure, steps }); return { unified: false, bindings, failure, steps }; return { unified: false, substitution, failure, steps }; } /** The substitution as text, each binding with the others applied: `{X = a, Y = g(a)}`. */ static text(bindings: ReadonlyMap<string, Term>): string { static text(substitution: ReadonlyMap<string, Term>): string { return `{${[...bindings].map(([name, term]) => `${name} = ${termText(applySubstitution(term, bindings))}`).join(", ")}}`; return `{${[...bindings].map(([name, term]) => `${name} = ${termText(applySubstitution(term, substitution))}`).join(", ")}}`; }}