“We proceed to prove, on the other hand, that in its full generality the correspondence decision problem is recursively unsolvable, and hence, no doubt, unsolvable in the intuitive sense.”
—Emil L. Post, “A Variant of a Recursively Unsolvable Problem”
The Post Correspondence Problem (PCP) is a particularly interesting problem that appears to have nothing to do with Turing Machines, code, or computation. Named for logician Emil Post, the PCP is a simple problem to state, and does not even seem particularly hard, and yet is provably undecidable!
In the Post Correspondence Problem, you are given a finite collection of pairs of strings, called the PCP instance. The challenge is to determine whether or not there is a finite nonempty sequence of pairs of strings such that
Often the PCP is stated in terms of a set of “dominos” with a top string and a bottom string, e.g.,

with the assumption that you have as many of each kind of domino as you need. The problem is then to decide whether you can put together a finite sequence of dominos such that the characters on the top row spell out the same as the characters on the bottom.
The PCP instance just shown,

has a solution where top
and bottom spell out abcaaabc, namely,

This solution uses all four kinds of domino, but this isn’t required in general. The solution also uses one kind of domino more than once; this is allowed, but also not required.
In contrast, the PCP instance

has no (finite) solution.
In general, how hard is it to take a PCP instance and decide whether or not a solution exists?
Clearly it’s semidecidable. We can check all possible sequences of dominos from shortest to longest; if a solution exists, we will eventually find it. And if no solution exists, we’ll keep trying forever, but that’s fine for semidecidability.
Surprisingly, though, it is not decidable. There is no algorithm that can tell us in finite time whether a solution exists. The proof of undecidability (showing that deciding PCP is as hard as deciding whether Turing Machine halt!) proceeds in two steps: .
The Modified PCP (MPCP) is just like the PCP, except that a solution is required to start with the first domino.
The dominos

have a PCP solution (just take one copy of the last kind of domino and we’re done!) but there is no MPCP solution (which is required to start with a domino of the first kind).
PCP is at least as hard as MPCP:
Proof Sketch: Given any MPCP instance, we can find equivalent PCP instance. The trick is to tweak the domino patterns so that while PCP is theoretically allowed to choose any domino to start its solution, there’s only one kind of domino that could possibly start a solution (i.e., only one kind of domino where the top and bottom start with the same character).
For example, here we turn a MPCP instance (top) into a PCP instance (bottom) such that any PCP solution lets us reconstruct an MPCP problem:

MPCP is at least as hard as deciding halting for Turing Machines:
Proof Sketch: Any Turing Machine running on an input can be converted into a set of dominos, where the first domino sets up the TM in its initial configuration. Any solution to that problem spells out the trace (computation history) of the machine halting on top and on bottom. The trick is that the configurations are offset from bottom to top:

Then, the dominos reflect the possible differences between one configuration and the next (e.g., a domino might have the same symbol on top and bottom to indicate that part of the tape did not change from one configuration to the next, or the domino might show how the configuration around the TM read/write head changes from one configuration to the next.
The simple Turing Machine

moves rightwards over any sequence of 1’s, writes an additional 1 in the following blank square, and halts (and accepts).
The computation of this Turing Machine on input 11 (which goes via
configurations ), can be simulated using
the following MPCP instance:
The first kind of
domino sets up the initial configuration of the machine. The rest of the
first row is used to copy symbols on the tape that don’t change from
one configuration to the next (and optionally make implicit blank cells
explicit). The first two dominos on the second row correspond to the
possible TM transitions (top is before the transition, bottom is after).
Finally the last three dominos are a technical trick to ensure the top
of the sequence can catch up with the bottom of the sequence when the TM
configuration reaches an accepting state.
The unique solution to this instance starts with the first domino (no configuration on top; the initial TM configuration on bottom), and then proceeds (spelling out the first configuration on top and the second configuration on bottom, then the second configuration on top and the third configuration on bottom, and so on):

In general, we can turn the initial state and the transitions of any Turing Machine into a MPCP instance that has a finite solution if and only if the Turing Machine halts. Thus, figuring out whether an arbitrary MPCP instance has a solution is at least as hard as figuring out whether an arbitrary Turing Machine halts on an arbitrary input.
PCP is undecidable.
Proof. , and , and is transitive.