Introduction

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 xx 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.

Try It

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">Term 1</label>
      <input id="term1" type="text" value="f(X, g(b))" spellcheck="false" autocomplete="off"/>
    </div>
    <div class="field">
      <label for="term2">Term 2</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">Unify</button>
      <button id="reset-btn" type="button" class="ghost">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; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Robinson's Unification Algorithm (1965)
// Terms are represented as: { type:'var', name } | { type:'const', name } | { type:'fun', name, args[] }
// The algorithm maintains an equation set and a substitution (environment).
// At each step it picks an equation and applies one of the standard rules:
//   Delete: s = s           -> remove
//   Decompose: f(s1..sn)=f(t1..tn) -> add s1=t1,..,sn=tn
//   Swap: non-var = var     -> swap to var = non-var
//   Eliminate: X = t (X not in t, X not in domain) -> add X->t to substitution
//   Conflict: f(..) = g(..) or arity mismatch -> FAIL
//   Occur check: X = t where X in t -> FAIL

const EXAMPLES = [
  ['f(X, g(b))', 'f(a, g(Y))'],
  ['h(X, X)', 'h(f(a), f(a))'],
  ['f(X, Y)', 'f(g(Y), g(X))'],
  ['f(X)', 'g(X)'],
  ['f(X, X)', 'f(a, b)']
];

// โ”€โ”€ Parser โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€
function tokenize(s) {
  s = s.replace(/\s+/g,'');
  const toks = [];
  let i = 0;
  while (i < s.length) {
    if (s[i] === '(' || s[i] === ')' || s[i] === ',') { toks.push(s[i++]); continue; }
    let j = i;
    while (j < s.length && s[j] !== '(' && s[j] !== ')' && s[j] !== ',') j++;
    toks.push(s.slice(i, j)); i = j;
  }
  return toks;
}

function isVar(name) { return /^[A-Z?]/.test(name); }

function parse(s) {
  const toks = tokenize(s);
  let pos = 0;
  function parseTerm() {
    const name = toks[pos++];
    if (pos < toks.length && toks[pos] === '(') {
      pos++; // consume '('
      const args = [];
      while (toks[pos] !== ')') {
        args.push(parseTerm());
        if (toks[pos] === ',') pos++;
      }
      pos++; // consume ')'
      return { type: 'fun', name, args };
    }
    return isVar(name) ? { type:'var', name } : { type:'const', name };
  }
  const result = parseTerm();
  if (pos !== toks.length) throw new Error('Unexpected tokens');
  return result;
}

function termStr(t) {
  if (t.type === 'var') return t.name;
  if (t.type === 'const') return t.name;
  return t.name + '(' + t.args.map(termStr).join(', ') + ')';
}

// โ”€โ”€ Substitution application โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€
function applySubst(subst, term) {
  if (term.type === 'var') return subst[term.name] ? applySubst(subst, subst[term.name]) : term;
  if (term.type === 'const') return term;
  return { type:'fun', name:term.name, args: term.args.map(a => applySubst(subst, a)) };
}

// โ”€โ”€ Occurs check โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€
function occurs(varName, term) {
  if (term.type === 'var') return term.name === varName;
  if (term.type === 'const') return false;
  return term.args.some(a => occurs(varName, a));
}

// โ”€โ”€ Main unification (produces step log) โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€
function unify(t1, t2) {
  const steps = [];
  const subst = {};
  const equations = [[t1, t2]];

  function log(action, lhs, rhs, extra) {
    steps.push({ action, lhs: termStr(lhs), rhs: termStr(rhs), extra: extra || null });
  }

  const MAX = 60;
  let iter = 0;
  while (equations.length > 0 && iter++ < MAX) {
    const [s, t] = equations.shift();
    const sa = applySubst(subst, s), ta = applySubst(subst, t);

    // Delete
    if (termStr(sa) === termStr(ta)) {
      log('Delete (identical)', sa, ta, null);
      continue;
    }
    // Swap: non-var = var
    if (sa.type !== 'var' && ta.type === 'var') {
      log('Swap', sa, ta, null);
      equations.unshift([ta, sa]);
      continue;
    }
    // Eliminate: var = term
    if (sa.type === 'var') {
      if (occurs(sa.name, ta)) {
        log('Occur check FAIL', sa, ta, fmt('Variable %name% occurs in %termStr%', { name: sa.name, termStr: termStr(ta) }));
        return { ok: false, steps, reason: fmt('Occur check: %name% appears inside %termStr%', { name: sa.name, termStr: termStr(ta) }) };
      }
      log(fmt('Bind %name% = %termStr%', { name: sa.name, termStr: termStr(ta) }), sa, ta, null);
      // apply new binding to all existing equations
      for (let i = 0; i < equations.length; i++)
        equations[i] = [applySubst({[sa.name]: ta}, equations[i][0]),
                        applySubst({[sa.name]: ta}, equations[i][1])];
      // apply to existing subst values
      for (const k in subst) subst[k] = applySubst({[sa.name]: ta}, subst[k]);
      subst[sa.name] = ta;
      continue;
    }
    // Decompose or Conflict
    if (sa.type === 'fun' && ta.type === 'fun') {
      if (sa.name !== ta.name || sa.args.length !== ta.args.length) {
        log('Conflict', sa, ta, 'Different functor or arity');
        return { ok: false, steps, reason: fmt('%termStr% and %termStr2% have different functors/arities', { termStr: termStr(sa), termStr2: termStr(ta) }) };
      }
      log(fmt('Decompose %name%(%length%)', { name: sa.name, length: sa.args.length }), sa, ta, null);
      for (let i = 0; i < sa.args.length; i++) equations.unshift([sa.args[i], ta.args[i]]);
      continue;
    }
    // Constant conflict
    log('Conflict', sa, ta, 'Constants differ');
    return { ok: false, steps, reason: termStr(sa) + ' โ‰  ' + termStr(ta) };
  }
  return { ok: true, steps, subst };
}

// โ”€โ”€ UI โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€
const t1El = document.getElementById('term1');
const t2El = document.getElementById('term2');
const resultArea = document.getElementById('result-area');
const stepsArea = document.getElementById('steps-area');

function showResult(msg, ok) {
  resultArea.textContent = msg;
  resultArea.className = 'result-area ' + (ok ? 'ok' : 'fail');
}

function run() {
  stepsArea.innerHTML = '';
  resultArea.className = 'result-area hidden';
  let t1, t2;
  try { t1 = parse(t1El.value.trim()); } catch(e) { showResult(fmt('Parse error in Term 1: %message%', { message: e.message }), false); return; }
  try { t2 = parse(t2El.value.trim()); } catch(e) { showResult(fmt('Parse error in Term 2: %message%', { message: e.message }), false); return; }

  const res = unify(t1, t2);

  // Render steps with delay
  res.steps.forEach((step, i) => {
    const div = document.createElement('div');
    div.className = 'step' + (step.action.includes('FAIL') || step.action.includes('Conflict') ? ' fail-step' : '');
    div.innerHTML =
      '<div class="action">' + step.action + '</div>' +
      '<div class="terms">' + step.lhs + ' = ' + step.rhs + '</div>' +
      (step.extra ? '<div class="sub">' + step.extra + '</div>' : '');
    stepsArea.appendChild(div);
    setTimeout(() => div.classList.add('show'), 60 + i * 120);
  });

  setTimeout(() => {
    if (res.ok) {
      const pairs = Object.entries(res.subst).map(([k,v]) => k + ' โ†’ ' + termStr(v));
      if (pairs.length === 0) showResult('โœ“ Terms are already identical. MGU = {} (identity substitution).', true);
      else showResult(fmt('โœ“ MGU = { %pairs% }', { pairs: pairs.join(', ') }), true);
    } else {
      showResult(fmt('โœ— Not unifiable: %reason%', { reason: res.reason }), false);
    }
  }, 80 + res.steps.length * 120);
}

document.getElementById('unify-btn').addEventListener('click', run);
document.getElementById('reset-btn').addEventListener('click', () => {
  const ex = EXAMPLES[Math.floor(Math.random() * EXAMPLES.length)];
  t1El.value = ex[0]; t2El.value = ex[1];
  stepsArea.innerHTML = ''; resultArea.className = 'result-area hidden';
});

// Run on load with default values
run();
Result
Console

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.

The Real Complexity

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.

Where It Matters

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.

Conclusion

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.

Share this article

Pick a channel โ€” or use your device's native share sheet.

Comments

Loading comments...

https://www.kipuhub.com/en/article/unification/Content licensed under CC BY-NC 4.0.