{ "cells": [ { "cell_type": "markdown", "metadata": { "colab_type": "text", "id": "view-in-github" }, "source": [ "\"Open" ] }, { "attachments": {}, "cell_type": "markdown", "metadata": { "id": "ZP2X2VKqh8Fc" }, "source": [ "# Post's Correspondence Problem\n", "\n", "Post's Correspondence Problem (PCP) was introduced [earlier](content:firstPCP).\n", "We use build on the undecidability of the Halting Problem to prove the undecidability of the PCP for pointed domino sets. In more detail, we saw in [our work on tiling](content:tilingPreparation) that the set of ```1#``` programs which only use R1 and which halt is undecidable. \n", "\n", "```{admonition} Notation\n", ":class: tip\n", "\n", "Let $A$ be the set of ```1#``` programs which are tidy and whose only register is R1. Let\n", "\n", "$$\n", "\\begin{array}{lcl}\n", "K^1 & = & \\{ p \\in A : [\\![p]\\!](\\ )\\!\\!\\downarrow\\}\\\\\n", "K^2& = & \\{ p \\in A : [\\![p]\\!](\\ )\\!\\!\\downarrow\\ \\mbox{ and } [\\![p]\\!](\\ )\\simeq \\varepsilon\\}\\\\\n", "\\end{array}\n", "$$\n", "\n", "We know that $K^1$ is undecidable. It is easy to see that $K^1 \\leq K^2$ via the function $p\\mapsto p + clear$, and so $K^2$ is also undecidable.\n", "\n", "\n", "Let $\\mathbb{D}$ be the set of (codes of) all finite, pointed domino sets $(\\mathcal{D},d_0)$.\n", "Let $K^{\\mathbb{D}}$ be the set of (codes of) domino sets $\\mathcal{D}$ which have a Post word.\n", "\n", "When we talk about domino sets in this section, we always will mean a \n", "finite,\n", "pointed set. And when we talk about a Post word, we always mean a finite word whose concatanations on the top and bottom agree.\n", "```\n", "\n", "Here is our main result on the PCP.\n", "\n", "\n", "```{prf:theorem}\n", ":label: PCP_undecidability\n", "\n", "\n", "${K}^2\\leq_m {K}^{\\mathbb{D}}$. \n", "\n", "That is, there is a total computable function\n", "$\\mathcal{D}: A\\to \\mathbb{D}$\n", "such that \n", "\n", "$$\n", "p\\in {K}^2 \\quadiff \\mathcal{D}(p) \\in {K}^{\\mathbb{D}}\n", "$$\n", "\n", "That is, $\\mathcal{D}(p)$ has a Post word if and only if $[\\![p]\\!](\\ )\\!\\!\\downarrow$.\n", "\n", "As a result, ${K}^{\\mathbb{D}}$ is undecidable.\n", "```\n" ] }, { "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ "## Definition of $\\mathcal{D}$\n", "\n", "Fix a program $p\\in A$. $\\mathcal{D}(p)$ starts with the following dominoes:\n", "\n", "\n", "\n", "Here and below, $K$ is the number of instructions in $p$.\n", "\n", "Whenever instruction $i$ of $p$ is ```1#``` or ```1##```, we have\n", "\n", "\n", "\n", "That is, we use the left domino above when instruction $i$ is ```1#```, and the right domino when it is ```1##```.\n", "Similarly, whenever instruction $i$ is ```1^k ###``` or ```1^k ####```, we have\n", "\n", "\n", "\n", "Finally, whenever instruction $i$ is ```1#####```, we have the three dominoes shown below:\n", "\n", "" ] }, { "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ "## Example\n", "\n", "Let $p$ be the program\n", "\n", "$$\n", "{\\tt 1\\# | 1\\#\\# | 1 \\#^5 | 1^3\\#^3 | 1^2 \\#^4 | 1^3 \\#^4}\n", "$$\n", "\n", "Then $\\mathcal{D}(p)$ is the following set of dominoes:\n", "\n", "\n", "\n", "This domino set has a (unique) Post sequence. It is \n", "\n", "\n", "\n", "The Post word is \n", "\n", "$$\n", "{start} | { 1} {\\tt 1} | {2} {\\tt 1 \\#} | {3} {\\tt 1 \\# } | {5} {\\tt \\# } | {3 } {\\tt \\#} | 6 | 3 | 4 | 7 | {halt}\n", "$$" ] }, { "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ "## Proof\n", "\n", "We now turn to the proof of {prf:ref}`PCP_undecidability`.\n", "\n", "```{admonition} Definition\n", ":class: attention\n", "\n", "Let $p$ be a program. Assume that $[\\![p]\\!](\\ )\\!\\!\\downarrow$, and suppose that the computation goes on for at least $n$ steps without halting. The *$n$-trace* of $p$ is the sequence of words\n", "\n", "$$\n", "1\\ w_1 2\\ w_2 \\cdots i(j)\\ w_j \\cdots i(n)\\ w_n,\n", "$$\n", "\n", "where for $1\\leq j \\leq n$, $i(j)$ is the number of the instruction which is executed in step $j$, and $w(j)$ is the contents of the register after step $j$.\n", "\n", "\n", "The *modified $n$-trace* of $p$ is the sequence of words\n", "\n", "$$\n", "1\\ v_1 2\\ v_2 \\cdots i(j)\\ v_j \\cdots i(n)\\ v_n,\n", "$$\n", "\n", "is defined in almost the same way, with the difference being that if $i(j)$ is ```1#####```, and if $i(j)$ is ```1#####```,\n", "and if at before this instruction ```1#####``` is executed the register is non-empty and has $c_j$ as its first character, then\n", "$v_j= c_j w_j$.\n", "\n", "```\n", "\n", "\n" ] }, { "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ "```{prf:example}\n", ":label: example-modified-trace\n", "\n", "Again we take $p$ to be \n", "\n", "\n", "$$\n", "{\\tt 1\\# | 1\\#\\# | 1 \\#^5 | 1^3\\#^3 | 1^2 \\#^4 | 1^3 \\#^4}\n", "$$\n", "\n", "The $9$-trace is \n", "\n", "$$\n", "1 {\\tt 1} | 2 {\\tt 1 \\#} | 3 {\\tt \\#} | 5 {\\tt \\#} | 3 {\\tt \\varepsilon } | 6 \\varepsilon | 3 \\varepsilon | 4 \\varepsilon | 7 \\varepsilon \n", "$$\n", "\n", "\n", "The modified $9$-trace is\n", "\n", "\n", "$$\n", "1 {\\tt 1} | 2 {\\tt 1 \\#} | 3 {\\tt 1 \\#} | 5 {\\tt \\#} | 3 {\\tt \\# } | 6 \\varepsilon | 3 \\varepsilon | 4 \\varepsilon | 7 \\varepsilon | \n", "$$\n", "\n", "The differences are to be found in the first two segments that start with $3$. That is, instruction $3$ is ```1#####```. The first segment which starts with a $3$ is $3{\\tt 1 \\#}$. In the trace, this is $3{\\tt \\#}$. In the modified trace, we added the ${\\tt 1}$ because before we executed the instruction ```1#####```, the register started with a ${\\tt 1}$. Similar remarks apply to the second of the three segments that start with $3$. \n", "The third such segment does not get an extra character because the register was empty at the time that ```1#####``` was executed. \n", "\n", "Notice that the modified $9$-trace is identical to the Post word in our example above, except for the first and last symbols, $start$ and $halt$.\n", "```" ] }, { "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ "\n", "\n", "```{prf:lemma}\n", ":label: domino_contruction_works\n", "\n", "Fix $p\\in A$, and consider the run of $p$ on empty registers and the tile set $\\mathcal{D}(p)$.\n", "\n", "For all $n\\geq 1$ the following are equivalent:\n", "\n", "1. The run goes on for at least $n$ steps without halting.\n", "\n", "2. There is a (unique) sequence of dominos $d_1 d_2 \\cdots d_r$ with the following properties:\n", "\n", "(a) $d_1 d_2 \\cdots d_r$ contains exactly $n$ instruction dominoes. The first is the starting domino, so it contains $Inst(1)$ on the bottom and $Inst(0) = start$ on the top. For $2\\leq j \\leq n$, the $j$th instruction domino in $d_1 d_2 \\cdots d_r$ contains $Inst(j)$ on the bottom, and it contains $Inst(j-1)$ on the top. The last instruction domino in $d_1 d_2 \\cdots d_r$ has $Inst(n)$ on the bottom and $Inst(n-1)$ on the top. \n", "\n", "\n", "(b) For $1\\leq j < n$, the sequence properly between $Inst(j)$ and $Inst(j+1)$ on the bottom\n", "is the contents of R1 after $j$ steps of the run of $p$ (call this $c_1 c_2 \\cdots c_{\\ell}$), \n", "except that if $Inst(j)$ is ```1#####``` and R1 starts with $d$ before this instruction is executed, then the sequence properly between $Inst(j)$ and $Inst(j+1)$ on the bottom\n", "is $d c_1 c_2 \\cdots c_{\\ell}$.\n", "\n", "(c) For $1 \\leq j < n-1$, the sequence properly between $Inst(j)$ and $Inst(j+1)$ on the top is the same as the sequence\n", "between $Inst(j)$ and $Inst(j+1)$ on the bottom.\n", "\n", "```\n" ] }, { "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ "```{prf:proof}\n", "By induction on $n$. For $n = 0$, we take $r = 1$, and we take $d_1, d_2$ to be the starting dominos.\n", "\n", "Now assume our result for $n$, and we show it for $n+1$. \n", "\n", "\n", "First, assume (1) for $n+1$. Then (1) surely holds for $n$, and so by induction hypothesis, we have (2) for $n$.\n", "Let $d_1 d_2 \\cdots d_r$ be the unique sequence with point (2). We need only need to show that there is a unique continuation\n", "to a sequence $d_1 d_2 \\cdots d_r, d_{r+1}, \\ldots, d_s$ with all parts of (2) for $n+1$. In fact, we only need to worry about \n", "\n", "After $n$ steps of the run of $p$, the contents of the register is the word on the bottom between the $Inst(n)$ on the bottom \n", "and $Inst(n+1)$ on the bottom. Again, we might need to modify this. \n", "\n", "\n", "\n", "In the other direction, assume (2) for $n+1$, and let $d_1, \\ldots, d_r$ be as in (2). We show (1) for $n+1$. Consider the initial subsequence\n", "of $d_1, \\ldots, d_r$ determined by the first $n$ instruction dominoes, and everything that came before any of these. This sequence has the properties\n", "in (2) for $n$. So by induction hypothesis, we also know (1) for $n$. \n", "\n", "\n", "```" ] } ], "metadata": { "colab": { "authorship_tag": "ABX9TyOvMYEc3agFJfWmUgW6ufJT", "include_colab_link": true, "provenance": [] }, "kernelspec": { "display_name": "Python 3", "name": "python3" }, "language_info": { "name": "python" } }, "nbformat": 4, "nbformat_minor": 0 }