Introduction

Every programmer knows the small anxiety of a refactor: you rewrite a function to be cleaner or faster, and you believe it does the same thing — but does it, on every input? That question — do two programs always produce identical outputs? — is program equivalence.

The obvious check is to test: run both on a bunch of inputs and compare. If they ever disagree, they're not equivalent. But if they always agree on your tests... you've proven nothing. There are infinitely many possible inputs, and a difference might hide at exactly the one you didn't try — the value 42, or every input above a million.

And here's the deep result: there is no general procedure that can decide, for arbitrary programs, whether they're equivalent. The problem is undecidable — a direct relative of the halting problem. Not slow: impossible.

Spot the Difference

Try it. Pick a pair of small programs that look like they might do the same thing. Type an input and compare their outputs, or let the demo auto-test a range. Hunt for a value where they disagree.

<p class="hint">Pick two programs that look alike. Test an input to compare their outputs, or auto-test a range. A single mismatch proves they differ — but matching every test you try proves <b>nothing</b>.</p>
<select id="pair" class="pair"></select>
<div class="progs">
  <pre class="prog" id="pa"></pre>
  <pre class="prog" id="pb"></pre>
</div>
<div class="row">
  <label>input x = <input id="x" type="number" value="3" /></label>
  <button id="test" type="button">Test</button>
  <button id="auto" type="button">Auto-test −50…200</button>
</div>
<div id="out" class="out"></div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; }
.hint { font-size: .9rem; color: #444; margin: 0 0 .8rem; line-height: 1.45; }
.pair { font: 600 14px system-ui; padding: .4rem .6rem; border: 1px solid #bbb; border-radius: 8px; margin-bottom: .7rem; width: 100%; max-width: 340px; }
.progs { display: grid; grid-template-columns: 1fr 1fr; gap: .6rem; margin-bottom: .8rem; }
.prog { background: #1d2733; color: #e6edf3; border-radius: 8px; padding: .7rem .8rem; font: 600 12.5px ui-monospace, monospace; white-space: pre-wrap; margin: 0; line-height: 1.5; min-height: 84px; }
.row { display: flex; gap: .5rem; align-items: center; flex-wrap: wrap; margin-bottom: .7rem; }
label { font: 600 14px system-ui; color: #1d3557; }
input { font: 700 15px ui-monospace, monospace; width: 6rem; padding: .35rem .5rem; border: 1px solid #bbb; border-radius: 7px; }
button { font: 600 13px system-ui, sans-serif; padding: .5rem .9rem; border: 1px solid #457b9d; background: #457b9d; color: #fff; border-radius: 8px; cursor: pointer; }
.out { font: 600 14px system-ui; line-height: 1.6; min-height: 2.4em; }
.out .ok { color: #0a7d33; } .out .bad { color: #c0392b; font-weight: 800; }
.out code { font-family: ui-monospace, monospace; background: #eef1f4; padding: .05rem .3rem; border-radius: 4px; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Program equivalence: deciding if two programs always agree is undecidable.
// Testing can only ever find a difference, never prove sameness — a sneaky
// input (here 42, or anything above 1000) can hide the disagreement.
const PAIRS = [
  { name: 'double a number', a: 'function f(x) {\n  return 2 * x;\n}', b: 'function g(x) {\n  return x + x;\n}', f: x => 2 * x, g: x => x + x },
  { name: 'square (one has a bug)', a: 'function f(x) {\n  return x * x;\n}', b: 'function g(x) {\n  if (x === 42)\n    return 1729;\n  return x * x;\n}', f: x => x * x, g: x => x === 42 ? 1729 : x * x },
  { name: 'absolute value', a: 'function f(x) {\n  return Math.abs(x);\n}', b: 'function g(x) {\n  return x < 0 ? -x : x;\n}', f: x => Math.abs(x), g: x => x < 0 ? -x : x },
  { name: 'identity (off by one when big)', a: 'function f(x) {\n  return x;\n}', b: 'function g(x) {\n  if (x > 1000)\n    return x + 1;\n  return x;\n}', f: x => x, g: x => x > 1000 ? x + 1 : x }
];
let cur = 0;

function show() {
  const p = PAIRS[cur];
  document.getElementById('pa').textContent = p.a;
  document.getElementById('pb').textContent = p.b;
  document.getElementById('out').innerHTML = '';
}

function test() {
  const p = PAIRS[cur]; const x = +document.getElementById('x').value;
  const a = p.f(x), b = p.g(x);
  const out = document.getElementById('out');
  if (a === b) out.innerHTML = fmt('<span>f(%x%) = <code>%a%</code>, g(%x%) = <code>%b%</code> — <span class="ok">match.</span> (Still no proof of equivalence.)</span>', { x: x, a: a, b: b });
  else out.innerHTML = fmt('<span>f(%x%) = <code>%a%</code>, g(%x%) = <code>%b%</code> — <span class="bad">DIFFER! Found a counterexample → not equivalent.</span></span>', { x: x, a: a, b: b });
}

function auto() {
  const p = PAIRS[cur]; let diff = null;
  for (let x = -50; x <= 200; x++) { if (p.f(x) !== p.g(x)) { diff = x; break; } }
  const out = document.getElementById('out');
  if (diff !== null) out.innerHTML = fmt('<span class="bad">Mismatch at x = %diff%</span> — f = <code>%f%</code>, g = <code>%g%</code>. Definitely <b>not</b> equivalent.', { diff: diff, f: p.f(diff), g: p.g(diff) });
  else out.innerHTML = '<span class="ok">No difference found in −50…200.</span> Tempting to call them equal — but that proves nothing. The disagreement (if any) could hide at a larger input. There’s no finite test that settles it.';
}

function init() {
  const sel = document.getElementById('pair');
  sel.innerHTML = PAIRS.map((p, i) => '<option value="' + i + '">' + p.name + '</option>').join('');
  sel.addEventListener('change', () => { cur = +sel.value; show(); });
  document.getElementById('test').addEventListener('click', test);
  document.getElementById('auto').addEventListener('click', auto);
  document.getElementById('x').addEventListener('keydown', e => { if (e.key === 'Enter') test(); });
  show();
}
init();
Result
Console

Some pairs really are equivalent; others hide a difference at one sneaky input. When your tests all match, notice the trap: it feels like proof, but it isn't. You'd have to test every input to be sure — and for real programs, that's infinitely many. That gap is the whole point.

The Hard Part

Equivalence is undecidable, and the reason is elegant:

  • Testing can only disprove. A mismatch shows non-equivalence, but no finite set of passing tests proves equivalence over infinitely many inputs.
  • It reduces from halting. If you could decide equivalence, you could decide halting: compare a program against one that trivially halts, and equivalence would tell you whether the first halts. Since halting is undecidable, so is equivalence.
  • Rice's theorem seals it. Essentially any non-trivial question about a program's behavior (not its text) is undecidable — and "does it behave like this other program?" is exactly that kind of question.
  • Restrict to win. On finite-state or loop-free programs, equivalence becomes decidable — that's why hardware circuits can be checked exactly. The undecidability comes from unbounded loops and memory.
  • Practice approximates. Bounded equivalence checking verifies agreement up to some input size or loop depth; SMT solvers and formal methods prove equivalence for specific, well-structured cases (and compilers use this to validate optimizations).

So program equivalence is the verification engineer's version of the halting wall: provably no universal tool, only partial methods that work within limits.

Where It Matters

The question "do these behave the same?" is everywhere in software and hardware:

  • Compilers: every optimization must preserve behavior — equivalence checking validates that the optimized code matches the original.
  • Refactoring tools: automated rewrites that promise to keep behavior identical.
  • Hardware verification: checking a chip design matches its specification — decidable for finite circuits, and a billion-dollar industry.
  • Formal verification: proving safety-critical software (avionics, medical) meets its spec.
  • Security: confirming a patch fixes a bug without changing intended behavior.

Because the general problem is undecidable, all of these live on restricted languages, bounded checks and clever solvers — getting certainty where it's possible and high confidence where it isn't.

Conclusion

Program equivalence is the halting problem wearing a programmer's everyday worry. Each test you run can only ever catch a difference, never certify sameness — and the one input that would expose a bug may be the one you never thought to try. In full generality, no tool can settle it, because the question is fundamentally undecidable.

But the story isn't bleak. Restrict the programs — no unbounded loops, finite state — and equivalence becomes decidable, which is why your CPU's design was verified down to the gate. The lesson echoes the rest of this site: when a problem is provably impossible in general, progress comes from drawing a smaller, well-chosen box where the impossible becomes routine.

Share this article

Pick a channel — or use your device's native share sheet.

Comments

Loading comments...

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