The Post Correspondence Problem

Imagine a box of dominoes, but instead of dots each tile carries two short strings of letters: one printed along the top, one along the bottom. You may use each kind of domino as often as you like, and you place them left to right in any order.

The challenge sounds like a children's game. Read the whole top row as one long word. Read the whole bottom row as one long word. Can you arrange the tiles so the two words come out exactly the same?

For some boxes the answer is an easy yes — you stumble onto a match in seconds. For others the answer is no, and no amount of effort will ever produce a match. The unsettling part is the question lurking underneath: is there a general method that, handed any box, always tells you which case you're in? In 1946 the answer turned out to be a flat, permanent no.

Below is a small box of dominoes. Click a tile to append it to your sequence; the top string and the bottom string grow as you go. Your goal: make the full top string identical to the full bottom string.

<p class="hint">{{hint}}</p>
<div id="tiles" class="tiles"></div>
<div class="seq-wrap">
  <div class="row"><span class="lbl">{{lbl_top}}</span><code id="top" class="strip"></code></div>
  <div class="row"><span class="lbl">{{lbl_bot}}</span><code id="bot" class="strip"></code></div>
</div>
<div class="status" id="status">{{pick_prompt}}</div>
<div class="btns">
  <button id="check" type="button">{{btn_check}}</button>
  <button id="auto" type="button">{{btn_auto}}</button>
  <button id="undo" type="button" class="ghost">{{btn_undo}}</button>
  <button id="reset" type="button" class="ghost">{{btn_reset}}</button>
</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 .7rem; line-height: 1.45; }
.tiles { display: flex; gap: .5rem; flex-wrap: wrap; margin: .4rem 0 .9rem; }
.tile { cursor: pointer; border: 1px solid #1d3557; border-radius: 8px; overflow: hidden;
        min-width: 54px; text-align: center; transition: transform .08s; background: #fff; }
.tile:hover { transform: translateY(-2px); }
.tile .t { background: #e8eef3; color: #1d3557; padding: .3rem .5rem; font: 700 16px ui-monospace, monospace; }
.tile .b { background: #fbe9ec; color: #c92f3c; padding: .3rem .5rem; font: 700 16px ui-monospace, monospace; border-top: 1px solid #cdd9e3; }
.seq-wrap { background: #f5f7f9; border: 1px solid #e1e7ec; border-radius: 8px; padding: .6rem .7rem; }
.row { display: flex; align-items: center; gap: .6rem; margin: .25rem 0; }
.lbl { width: 58px; font-size: .8rem; color: #667; font-weight: 600; }
.strip { font: 700 17px ui-monospace, monospace; letter-spacing: 1px; word-break: break-all; min-height: 1.3em; }
#top { color: #1d3557; } #bot { color: #c92f3c; }
.status { font-size: 1rem; font-weight: 600; margin: .6rem 0; min-height: 1.4em; }
.status.ok { color: #0a7d33; } .status.bad { color: #c92f3c; }
.btns { display: flex; gap: .5rem; flex-wrap: wrap; }
button { font: 600 14px system-ui, sans-serif; padding: .45rem .9rem; border: 1px solid #1d3557;
         background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }

// Code not found

Notice the asymmetry. Checking a finished sequence is instant — just compare two strings, character by character. Finding a winning sequence is the hard part. The strings drift in and out of alignment, the search tree branches forever, and there is no length you can safely stop at: a match might need three tiles or three thousand. Press Auto-search to let the computer try every short sequence — and watch it keep going without ever being able to declare "no solution exists."

How hard is the Post correspondence problem? It is not merely slow — it is undecidable. This puts it in a different category from problems like SAT or the travelling salesman, which are hard but still solvable in principle.

• Checking a proposed sequence is trivial: concatenate the tops, concatenate the bottoms, compare. Linear time.
• Searching can be automated, but the search never terminates on a no instance. You can keep finding longer and longer candidates, yet you can never prove that no match exists.
• It is undecidable. In 1946, the logician Emil Post proved that no algorithm can take an arbitrary set of dominoes and correctly answer "is there a matching sequence?" for every possible box. There is no clever method, no faster computer, no future breakthrough that fixes this — the limit is mathematical, not technological.
• The proof reduces from the halting problem. Post (and later, cleaner constructions) showed how to encode the entire step-by-step run of a Turing machine into a set of dominoes, so that a match exists exactly when the machine halts. Since halting is undecidable, so is the domino puzzle.

That is the punchline. A question a child could understand turns out to be equivalent to deciding whether an arbitrary program ever stops. The dominoes are a disguise; underneath is the bedrock undecidability discovered by Turing and Church.

The Post correspondence problem rarely appears in production code, yet it is one of the most useful problems in theory — because it is the standard lever for proving that other problems are impossible to automate:

• Formal languages: deciding whether a context-free grammar is ambiguous, or whether two context-free languages intersect, is proven undecidable by reducing from PCP.
• Compilers and parsers: the impossibility results above explain why no tool can perfectly detect every grammar ambiguity — your parser generator warns you instead of deciding for you.
• Verification and type systems: many "does this program have property X?" questions inherit undecidability through a PCP-style reduction, marking the boundary where checkers must approximate.
• Teaching computability: because the rules are so concrete, PCP is the friendliest gateway to undecidability after the halting problem itself.

Whenever a textbook says "this problem is undecidable," there is a good chance a chain of dominoes is doing the heavy lifting in the proof.

The Post correspondence problem is a small miracle of simplicity: a few dominoes, one rule, and a question anyone can grasp in a sentence. Yet behind that friendly face sits a hard wall. No algorithm — now or ever — can decide every instance. Checking a match stays effortless; deciding whether a match exists is forbidden ground.

So the next time your auto-search keeps stacking tiles without ever saying "impossible," remember it isn't being lazy. It has run straight into the halting problem wearing a domino costume — and there is no method, anywhere in mathematics, that can settle the question for it.