Unification

Every time a statically typed language accepts your code without complaint, a small miracle has just happened. The compiler looked at something like f(x) = x + 1 and silently figured out that $x$ must be a number — not because you said so, but because it solved an equation over symbolic expressions. The engine doing that work is unification.

The question unification answers is deceptively simple: given two terms built from function symbols, constants, and variables, is there a way to substitute values for the variables so that the two terms become syntactically identical? Not equal in some deep semantic sense — just letter-for-letter the same.

J. A. Robinson answered that question in 1965 with a clean, recursive algorithm. Feed it f(X, b) and f(a, Y), and it will tell you: substitute X = a and Y = b. That substitution — the most general unifier (MGU) — is the unique most-flexible answer. It commits to as little as possible, leaving variables unbound wherever freedom remains.

The MGU is unique up to renaming variables, so unification has one right answer or none. When no substitution can reconcile two terms they are simply non-unifiable, and the algorithm reports failure cleanly.

Enter two first-order terms below — use lowercase letters for constants and function symbols, and uppercase letters or ? prefix for variables (e.g. f(X, g(b)) and f(a, Y)). Press Unify and watch Robinson's algorithm work through the equation set step by step, composing substitutions until both terms match.

<div class="demo-wrap">
  <div class="inputs">
    <div class="field">
      <label for="term1">{{term1_label}}</label>
      <input id="term1" type="text" value="f(X, g(b))" spellcheck="false" autocomplete="off"/>
    </div>
    <div class="field">
      <label for="term2">{{term2_label}}</label>
      <input id="term2" type="text" value="f(a, g(Y))" spellcheck="false" autocomplete="off"/>
    </div>
    <div class="btn-row">
      <button id="unify-btn" type="button">{{btn_unify}}</button>
      <button id="reset-btn" type="button" class="ghost">{{btn_reset}}</button>
    </div>
  </div>
  <div id="result-area" class="result-area hidden"></div>
  <div id="steps-area" class="steps-area"></div>
</div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; margin: 0; color: #1a1a2e; }
.demo-wrap { padding: .2rem .1rem; }
.inputs { display: flex; flex-direction: column; gap: .6rem; }
.field { display: flex; flex-direction: column; gap: .25rem; }
label { font-size: .82rem; font-weight: 600; color: #4a4a6a; }
input { font: 600 15px ui-monospace, monospace; padding: .45rem .7rem;
        border: 1.5px solid #b0b8d0; border-radius: 8px; outline: none;
        background: #f4f6fa; color: #1a1a2e; transition: border-color .15s; }
input:focus { border-color: #4c6ef5; }
.btn-row { display: flex; gap: .5rem; margin-top: .3rem; }
button { font: 600 14px system-ui; padding: .45rem 1rem; border-radius: 8px;
         cursor: pointer; border: 1.5px solid #4c6ef5; transition: all .15s; }
button:not(.ghost) { background: #4c6ef5; color: #fff; }
button:not(.ghost):hover { background: #3b5bdb; }
button.ghost { background: #fff; color: #4c6ef5; }
button.ghost:hover { background: #eef2ff; }
.result-area { margin-top: .8rem; padding: .6rem .8rem; border-radius: 10px;
               font: 600 14px ui-monospace, monospace; }
.result-area.ok { background: #d3f9d8; color: #1c6b31; border: 1px solid #8ed9a0; }
.result-area.fail { background: #ffe3e3; color: #b91c1c; border: 1px solid #f5a0a0; }
.result-area.hidden { display: none; }
.steps-area { margin-top: .7rem; display: flex; flex-direction: column; gap: .4rem; }
.step { background: #f0f3ff; border-left: 3px solid #4c6ef5; border-radius: 0 8px 8px 0;
        padding: .4rem .7rem; font-size: .84rem; opacity: 0; transform: translateY(6px);
        transition: opacity .25s, transform .25s; }
.step.show { opacity: 1; transform: none; }
.step .action { font-weight: 700; color: #4c6ef5; }
.step .terms { font: 600 13px ui-monospace; color: #222; margin-top: .15rem; }
.step .sub { font: 13px ui-monospace; color: #555; }
.step.fail-step { border-color: #e03131; background: #fff0f0; }
.step.fail-step .action { color: #c92a2a; }

// Code not found

Notice what the algorithm commits to at each step: it only binds a variable when forced, and the final substitution is always the most general one — any other unifier can be obtained from it by substituting further.

Unification sits at a rare sweet spot: hard enough to be useful, easy enough to be practical.

• Robinson's original algorithm (1965) is correct but can be exponential in the worst case due to repeated variable lookups creating redundant term copies.
• Near-linear time (Paterson & Wegman, 1978): by representing terms as directed acyclic graphs and using a union-find data structure, unification runs in O(n α(n)) time — essentially linear, where α is the inverse Ackermann function.
• First-order unification is decidable: the algorithm always terminates with either the MGU or a "no unifier exists" verdict. This tractability is what makes type inference in languages like Haskell, OCaml, and Rust fast at compile time.
• Higher-order unification is undecidable: as soon as function variables can appear in function-position (second-order and beyond), the problem becomes equivalent to the halting problem. Huet's algorithm for the simply-typed lambda calculus is semi-decidable: it may run forever without finding an answer.
• E-unification (modulo equations like commutativity) ranges from decidable to undecidable depending on the equational theory. This is an active research area in theorem proving.

The practical takeaway: first-order unification is solved. Every modern type system and logic programming language relies on its guaranteed termination and near-linear cost.

Unification is not a niche technique — it is the skeleton of several major areas of computer science:

• Type inference (Hindley-Milner): languages like Haskell, OCaml, ML, and Rust infer types by generating unification constraints from expressions and solving them. If unification succeeds, the program is type-correct without annotations. If it fails, you get a type error. The algorithm runs at compile time, in near-linear time.
• Logic programming (Prolog): every step of Prolog's execution is a unification. When Prolog tries to match a goal parent(tom, X) against a rule parent(tom, bob) :- true, it unifies the two heads, binding X = bob, and continues. Backtracking plus unification is the entirety of the language's runtime.
• Automated theorem proving: resolution-based provers (the foundation of systems like SPASS, Vampire, and E) apply Robinson's resolution principle: two clauses can be combined if one contains a literal that unifies with the negation of a literal in the other. Unification determines which literals match.
• Pattern matching in compilers: structural pattern matching in modern languages (Rust, Scala, Erlang) is a restricted form of unification — matching a value against a pattern corresponds to a one-sided unification where only the pattern side has variables.
• Constraint solving and AI: SAT solvers, constraint logic programming, and AI planning systems all build on forms of symbolic matching whose roots are in Robinson's algorithm.

Learn unification and you have learned the operating principle of an entire family of tools that reason about symbolic structure.

Robinson's unification algorithm is a quiet giant. Published in 1965 as part of the resolution principle for automated theorem proving, it turned out to be the engine behind typed programming languages, logic programming, and symbolic AI — fields that did not yet exist when he wrote the paper.

The core insight is one of those rare beautiful ideas: instead of asking whether two things are equal, ask whether there is a substitution that makes them equal. That question has a unique most-general answer, always terminates for first-order terms, and runs in near-linear time. Three properties that together make it deployable everywhere.

The next time your compiler tells you "type mismatch," that is unification reporting failure. The next time it accepts your code without a single annotation, that is unification succeeding silently — finding the most general assignment of types to variables so that every constraint is satisfied at once. A problem whose solution fits in a page, powering tools that run billions of times a day.