# HG changeset patch # User Christian Urban # Date 1359125878 -3600 # Node ID eb589fa73fc14c20556eb68f2c0cb00310653c78 # Parent bc54c5e648d73528c6cd9d9cf18b05aa231dbab3 updated diff -r bc54c5e648d7 -r eb589fa73fc1 Paper/Paper.thy --- a/Paper/Paper.thy Thu Jan 24 18:59:49 2013 +0100 +++ b/Paper/Paper.thy Fri Jan 25 15:57:58 2013 +0100 @@ -133,14 +133,15 @@ formalisation of Turing machines, as well as abacus machines (a kind of register machines) and recursive functions. To see the difficulties involved with this work, one has to understand that Turing machine -programs can be completely \emph{unstructured}, behaving -similar to Basic programs involving the infamous goto \cite{Dijkstra68}. This precludes in the -general case a compositional Hoare-style reasoning about Turing -programs. We provide such Hoare-rules for when it \emph{is} possible to -reason in a compositional manner (which is fortunately quite often), but also tackle -the more complicated case when we translate abacus programs into -Turing programs. This reasoning about Turing machine programs is -usually completely left out in the informal literature, e.g.~\cite{Boolos87}. +programs can be completely \emph{unstructured}, behaving similar to +Basic programs involving the infamous goto \cite{Dijkstra68}. This +precludes in the general case a compositional Hoare-style reasoning +about Turing programs. We provide such Hoare-rules for when it +\emph{is} possible to reason in a compositional manner (which is +fortunately quite often), but also tackle the more complicated case +when we translate abacus programs into Turing programs. This +reasoning about concrete Turing machine programs is usually +left out in the informal literature, e.g.~\cite{Boolos87}. %To see the difficulties %involved with this work, one has to understand that interactive @@ -230,7 +231,8 @@ model and undecidability result, we are able to formalise other results: we describe a proof of the computational equivalence of single-sided Turing machines, which is not given in \cite{Boolos87}, -but needed for formalising the undecidability proof of Wang's tiling problem. {\it citation} +but needed for example for formalising the undecidability proof of +Wang's tiling problem \cite{Robinson71}. %We are not aware of any other %formalisation of a substantial undecidability problem. *} @@ -266,6 +268,7 @@ \draw[fill] (1.35,0.1) rectangle (1.65,0.4); \draw[fill] (0.85,0.1) rectangle (1.15,0.4); \draw[fill] (-0.35,0.1) rectangle (-0.65,0.4); + \draw[fill] (-1.65,0.1) rectangle (-1.35,0.4); \draw (-0.25,0.8) -- (-0.25,-0.8); \draw[<->] (-1.25,-0.7) -- (0.75,-0.7); \node [anchor=base] at (-0.8,-0.5) {\small left list}; @@ -522,7 +525,9 @@ \caption{Copy machine}\label{copy} \end{figure} - {\it tapes in standard form} + {\it + As in \cite{Boolos87} we often need to restrict tapes to be in standard + form.} Before we can prove the undecidability of the halting problem for our Turing machines, we need to analyse two concrete Turing machine @@ -530,7 +535,7 @@ ``doing what they are supposed to be doing''. Such correctness proofs are usually left out in the informal literature, for example \cite{Boolos87}. One program we need to prove correct is the @{term dither} program shown in \eqref{dither} - and the other program is @{term "tcopy"} is defined as + and the other program is @{term "tcopy"} defined as \begin{center} \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} @@ -554,7 +559,7 @@ \begin{center} \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}} \begin{tabular}[t]{@ {}l@ {}} - @{thm (lhs) Hoare_halt_def} @{text "\"}\\[1mm] + \colorbox{mygrey}{@{thm (lhs) Hoare_halt_def}} @{text "\"}\\[1mm] \hspace{5mm}@{text "\"} @{term "(l, r)"}.\\ \hspace{7mm}if @{term "P (l, r)"} holds then\\ \hspace{7mm}@{text "\"} @{term n}. such that\\ @@ -562,7 +567,7 @@ \hspace{7mm}@{text "Q holds_for (steps (1, (l, r)) p n)"} \end{tabular} & \begin{tabular}[t]{@ {}l@ {}} - @{thm (lhs) Hoare_unhalt_def} @{text "\"}\\[1mm] + \colorbox{mygrey}{@{thm (lhs) Hoare_unhalt_def}} @{text "\"}\\[1mm] \hspace{5mm}@{text "\"} @{term "(l, r)"}.\\ \hspace{7mm}if @{term "P (l, r)"} holds then\\ \hspace{7mm}@{text "\"} @{term n}. @{text "\ is_final (steps (1, (l, r)) p n)"} @@ -577,9 +582,57 @@ more uniformly (only using Hoare-triples), we prefer our definitions because we can derive simple Hoare-rules for sequentially composed Turing programs. In this way we can reason about the correctness of @{term "tcopy_init"}, - for example, completely separately from @{term "tcopy_loop"}. + for example, completely separately from @{term "tcopy_loop"} and @{term "tcopy_end"}. - It is rather straightforward to prove that the Turing program + \begin{center} + \begin{tabular}{lcl} + \multicolumn{1}{c}{start tape}\\ + \begin{tikzpicture} + \draw[very thick] (-2,0) -- ( 0.75,0); + \draw[very thick] (-2,0.5) -- ( 0.75,0.5); + \draw[very thick] (-0.25,0) -- (-0.25,0.5); + \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); + \draw[very thick] (-0.75,0) -- (-0.75,0.5); + \draw[very thick] ( 0.75,0) -- ( 0.75,0.5); + \draw[very thick] (-1.25,0) -- (-1.25,0.5); + \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); + \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); + \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4); + \node [anchor=base] at (-1.7,0.2) {\ldots}; + \end{tikzpicture} + & \raisebox{2.5mm}{$\;\;\large\Rightarrow\;\;$} & + \begin{tikzpicture} + \draw[very thick] (-2,0) -- ( 0.75,0); + \draw[very thick] (-2,0.5) -- ( 0.75,0.5); + \draw[very thick] (-0.25,0) -- (-0.25,0.5); + \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); + \draw[very thick] (-0.75,0) -- (-0.75,0.5); + \draw[very thick] ( 0.75,0) -- ( 0.75,0.5); + \draw[very thick] (-1.25,0) -- (-1.25,0.5); + \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); + \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); + \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4); + \node [anchor=base] at (-1.7,0.2) {\ldots}; + \end{tikzpicture}\\ + + \begin{tikzpicture} + \draw[very thick] (-2,0) -- ( 0.25,0); + \draw[very thick] (-2,0.5) -- ( 0.25,0.5); + \draw[very thick] (-0.25,0) -- (-0.25,0.5); + \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); + \draw[very thick] (-0.75,0) -- (-0.75,0.5); + \draw[very thick] (-1.25,0) -- (-1.25,0.5); + \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); + \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); + \node [anchor=base] at (-1.7,0.2) {\ldots}; + \end{tikzpicture} + & \raisebox{2.5mm}{$\;\;\large\Rightarrow\;\;$} & + \raisebox{2.5mm}{loops} + \end{tabular} + \end{center} + + + It is straightforward to prove that the Turing program @{term "dither"} satisfies the following correctness properties \begin{center} diff -r bc54c5e648d7 -r eb589fa73fc1 Paper/document/root.bib --- a/Paper/document/root.bib Thu Jan 24 18:59:49 2013 +0100 +++ b/Paper/document/root.bib Fri Jan 25 15:57:58 2013 +0100 @@ -74,4 +74,25 @@ number = {3}, year = {1968}, pages = {147-148} -} \ No newline at end of file +} + + + +@Book{Berger66, + author = {R.~Berger}, + title = {{T}he {U}ndecidability of the {D}omino {P}roblem}, + journal = {Memoirs of the American Mathematical Society}, + year = {1966} +} + + +@Article{Robinson71, + author = {R.~M.~Robinson}, + title = {{U}ndecidability and {N}onperiodicity for {T}ilings of the {P}lane}, + journal = {Inventiones Mathematicae}, + year = {1971}, + volume = {12}, + pages = {177--209} +} + + diff -r bc54c5e648d7 -r eb589fa73fc1 Paper/document/root.tex --- a/Paper/document/root.tex Thu Jan 24 18:59:49 2013 +0100 +++ b/Paper/document/root.tex Fri Jan 25 15:57:58 2013 +0100 @@ -10,6 +10,7 @@ \usepackage{pdfsetup} \usepackage{tikz} \usepackage{pgf} +\usepackage{color} %% for testing \usepackage{endnotes} @@ -19,6 +20,9 @@ \urlstyle{rm} \isabellestyle{it} +% gray boxes +\definecolor{mygrey}{rgb}{.80,.80,.80} + % mathpatir \mprset{sep=0.8em} \mprset{center=false} diff -r bc54c5e648d7 -r eb589fa73fc1 paper.pdf Binary file paper.pdf has changed diff -r bc54c5e648d7 -r eb589fa73fc1 thys/uncomputable.thy --- a/thys/uncomputable.thy Thu Jan 24 18:59:49 2013 +0100 +++ b/thys/uncomputable.thy Fri Jan 25 15:57:58 2013 +0100 @@ -1075,47 +1075,36 @@ abbreviation "dither_unhalt_inv \ \(l, r). (\n. l = Bk \ n) \ r = [Oc]" -lemma dither_unhalt_state: +lemma dither_loops_aux: "(steps0 (1, Bk \ m, [Oc]) dither stp = (1, Bk \ m, [Oc])) \ (steps0 (1, Bk \ m, [Oc]) dither stp = (2, Oc # Bk \ m, []))" apply(induct stp) - apply(simp add: steps.simps) - apply(simp add: step_red) - apply(auto simp: step.simps fetch.simps dither_def numeral) + apply(auto simp: steps.simps step.simps dither_def numeral) done -lemma dither_unhalt_rs: - shows "\ is_final (steps0 (1, Bk \ m, [Oc]) dither stp)" -using dither_unhalt_state[of m stp] -by auto - lemma dither_loops: shows "{dither_unhalt_inv} dither \" apply(rule Hoare_unhaltI) -using dither_unhalt_rs -apply(auto) -done +using dither_loops_aux +apply(auto simp add: numeral) +by (metis Suc_neq_Zero is_final_eq) + -lemma dither_halt_rs: - "\stp. steps0 (1, Bk \ m, [Oc, Oc]) dither stp = (0, Bk \ m, [Oc, Oc])" +lemma dither_halts_aux: + shows "steps0 (1, Bk \ m, [Oc, Oc]) dither 3 = (0, Bk \ m, [Oc, Oc])" unfolding dither_def -apply(rule_tac x = "3" in exI) -apply(simp add: steps.simps step.simps fetch.simps numeral) -done - +by (simp add: steps.simps step.simps numeral) lemma dither_halts: shows "{dither_halt_inv} dither {dither_halt_inv}" apply(rule Hoare_haltI) -using dither_halt_rs +using dither_halts_aux apply(auto) by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases) -section {* - The final diagnal arguments to show the undecidability of Halting problem. -*} +section {* The diagnal argument below shows the undecidability of Halting problem *} text {* @{text "haltP tp x"} means TM @{text "tp"} terminates on input @{text "x"} @@ -1124,8 +1113,7 @@ definition haltP :: "tprog \ nat list \ bool" where - "haltP p lm = (\n a b c. steps (Suc 0, [], ) p n = (0, Bk\a, Oc\b @ Bk\c))" - + "haltP p lm \ \n a b c. steps (Suc 0, [], ) p n = (0, Bk \ a, Oc \ b @ Bk \ c)" abbreviation "haltP0 p lm \ haltP (p, 0) lm"