Editing Post correspondence problem (section)

==Proof sketch of undecidability ==

The most common proof for the undecidability of PCP describes an instance of PCP that can simulate the computation of an arbitrary [[Turing machine]] on a particular input. A match will occur if and only if the input would be accepted by the Turing machine. Because [[Halting problem|deciding if a Turing machine will accept an input is a basic undecidable problem]], PCP cannot be decidable either. The following discussion is based on [[Michael Sipser]]'s textbook ''Introduction to the Theory of Computation''.<ref name="sipser05">{{cite book|author = Michael Sipser|author-link = Michael Sipser| year = 2005 | title = Introduction to the Theory of Computation | edition = 2nd | publisher = Thomson Course Technology | isbn = 0-534-95097-3 | chapter = A Simple Undecidable Problem | pages = 199&ndash;205}}</ref>

In more detail, the idea is that the string along the top and bottom will be a [[computation history]] of the Turing machine's computation. This means it will list a string describing the initial state, followed by a string describing the next state, and so on until it ends with a string describing an accepting state. The state strings are separated by some separator symbol (usually written #). According to the definition of a Turing machine, the full state of the machine consists of three parts:
* The current contents of the tape.
* The current state of the [[finite-state machine]] which operates the tape head.
* The current position of the tape head on the tape.
Although the tape has infinitely many cells, only some finite prefix of these will be non-blank. We write these down as part of our state. To describe the state of the finite control, we create new symbols, labelled ''q''<sub>1</sub> through ''q''<sub>''k''</sub>, for each of the finite-state machine's ''k'' states. We insert the correct symbol into the string describing the tape's contents at the position of the tape head, thereby indicating both the tape head's position and the current state of the finite control. For the alphabet {0,1}, a typical state might look something like:

101101110''q''<sub>7</sub>00110.

A simple computation history would then look something like this:

''q''<sub>0</sub>101#1''q''<sub>4</sub>01#11''q''<sub>2</sub>1#1''q''<sub>8</sub>10.

We start out with this block, where ''x'' is the input string and ''q''<sub>0</sub> is the start state:

{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" | &nbsp;
|-
| bgcolor="#87E6FF" width="40" | ''q''<sub>0</sub>''x''#
|}

The top starts out "lagging" the bottom by one state, and keeps this lag  until the very end stage. Next, for each symbol ''a'' in the tape alphabet, as well as #, we have a "copy" block, which copies it unmodified from one state to the next:

{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" | ''a''
|-
| bgcolor="#87E6FF" width="40" | ''a''
|}

We also have a block for each position transition the machine can make, showing how the tape head moves, how the finite state changes, and what happens to the surrounding symbols. For example, here the tape head is over a 0 in state 4, and then writes a 1 and moves right, changing to state 7:

{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" | ''q''<sub>4</sub>0
|-
| bgcolor="#87E6FF" width="40" | 1''q''<sub>7</sub>
|}

Finally, when the top reaches an accepting state, the bottom needs a chance to finally catch up to complete the match. To allow this, we extend the computation so that once an accepting state is reached, each subsequent machine step will cause a symbol near the tape head to vanish, one at a time, until none remain. If ''q''<sub>''f''</sub> is an accepting state, we can represent this with the following transition blocks, where ''a'' is a tape alphabet symbol:

{{col-begin|width=auto}}
{{col-break|align=center}}
{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" | ''q''<sub>''f''</sub>''a''
|-
| bgcolor="#87E6FF" width="40" | ''q''<sub>''f''</sub>
|}
{{col-break|gap=5px|align=center}}
{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" | ''aq''<sub>''f''</sub>
|-
| bgcolor="#87E6FF" width="40" | ''q''<sub>''f''</sub>
|}
{{col-end}}

There are a number of details to work out, such as dealing with boundaries between states, making sure that our initial tile goes first in the match, and so on, but this shows the general idea of how a static tile puzzle can simulate a Turing machine computation.

The previous example

''q''<sub>0</sub>101#1''q''<sub>4</sub>01#11''q''<sub>2</sub>1#1''q''<sub>8</sub>10.

is represented as the following solution to the Post correspondence problem:

{{col-begin|width=auto}}
{{col-break|align=center}}
{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" | &nbsp;
|-
| bgcolor="#87E6FF" width="40" | ''q''<sub>0</sub>101#
|}
{{col-break|gap=5px|align=center}}
{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" |''q''<sub>0</sub>1
|-
| bgcolor="#87E6FF" width="40" | 1 ''q''<sub>4</sub>
|}
{{col-break|gap=5px|align=center}}
{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" | 0
|-
| bgcolor="#87E6FF" width="40" | 0
|}
{{col-break|gap=5px|align=center}}
{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" | 1
|-
| bgcolor="#87E6FF" width="40" | 1
|}
{{col-break|gap=5px|align=center}}
{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" | #
|-
| bgcolor="#87E6FF" width="40" | #
|}
{{col-break|gap=5px|align=center}}
{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" | 1
|-
| bgcolor="#87E6FF" width="40" | 1
|}
{{col-break|gap=5px|align=center}}
{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" | ''q''<sub>4</sub> 0
|-
| bgcolor="#87E6FF" width="40" | 1 ''q''<sub>2</sub>
|}
{{col-break|gap=5px|align=center}}
{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" | 1
|-
| bgcolor="#87E6FF" width="40" | 1
|}
{{col-break|gap=5px|align=center}}
{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" | #
|-
| bgcolor="#87E6FF" width="40" | #
|}
{{col-break|gap=5px|align=center}}
{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" | 1
|-
| bgcolor="#87E6FF" width="40" | 1
|}
{{col-break|gap=5px|align=center}}
{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" | 1 ''q''<sub>2</sub>1
|-
| bgcolor="#87E6FF" width="40" | ''q''<sub>8</sub>10
|}
{{col-break|gap=5px|align=center}}
{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" | #
|-
| bgcolor="#87E6FF" width="40" | #
|}
{{col-break|gap=5px|align=center}}
{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" | 1 ''q''<sub>8</sub>
|-
| bgcolor="#87E6FF" width="40" | ''q''<sub>8</sub>
|}
{{col-break|gap=5px|align=center}}
{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" | 1
|-
| bgcolor="#87E6FF" width="40" | 1
|}
{{col-break|gap=5px|align=center}}
{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" | 0
|-
| bgcolor="#87E6FF" width="40" | 0
|}
{{col-break|gap=5px|align=center}}
{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" | #
|-
| bgcolor="#87E6FF" width="40" | #
|}
{{col-break|gap=5px|align=center}}
{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" | q''<sub>8</sub> 1
|-
| bgcolor="#87E6FF" width="40" | ''q''<sub>8</sub>
|}
{{col-break|gap=5px|align=center}}
{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" | 0
|-
| bgcolor="#87E6FF" width="40" | 0
|}
{{col-break|gap=5px|align=center}}
{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" | #
|-
| bgcolor="#87E6FF" width="40" | #
|}
{{col-break|gap=5px|align=center}}
{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" | ''q''<sub>8</sub> 0
|-
| bgcolor="#87E6FF" width="40" | ''q''<sub>8</sub>
|}
{{col-break|gap=5px|align=center}}
{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" | #
|-
| bgcolor="#87E6FF" width="40" | #
|}
{{col-break|gap=5px|align=center}}
{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" | ''q''<sub>8</sub>
|-
| bgcolor="#87E6FF" width="40" | &nbsp;
|}
{{col-break|gap=5px|align=center}}
{| class="wikitable" style="text-align:center;"
| bgcolor="#55FF83" width="40" | #
|-
| bgcolor="#87E6FF" width="40" | #
|}
{{col-break|gap=5px|align=center}}
...
{{col-end}}