diff -r 49f8e5cf82c5 -r a673539f2f75 Paper/Paper.thy --- a/Paper/Paper.thy Thu Jan 24 10:53:43 2013 +0100 +++ b/Paper/Paper.thy Thu Jan 24 11:38:07 2013 +0100 @@ -23,6 +23,9 @@ update2 ("update") and tm_wf0 ("wf") and is_even ("iseven") and + tcopy_init ("copy\<^bsub>begin\<^esub>") and + tcopy_loop ("copy\<^bsub>loop\<^esub>") and + tcopy_end ("copy\<^bsub>end\<^esub>") and (* abc_lm_v ("lookup") and abc_lm_s ("set") and*) haltP ("stdhalt") and @@ -166,7 +169,7 @@ Turing machine. They report that the informal proofs from which they started are \emph{not} ``sufficiently accurate to be directly usable as a guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For -our formalisation we followed mainly the proofs from the textbook +our formalisation we follow mainly the proofs from the textbook \cite{Boolos87} and found that the description there is quite detailed. Some details are left out however: for example, it is only shown how the universal Turing machine is constructed for Turing @@ -352,9 +355,9 @@ %states.\footnote{The usual disjoint union operation in Isabelle/HOL %cannot be used as it does not preserve types.} This renaming can be %quite cumbersome to reason about. - We followed the choice made in \cite{AspertiRicciotti12} + We follow the choice made in \cite{AspertiRicciotti12} representing a state by a natural number and the states in a Turing - machine programme by the initial segment of natural numbers starting from @{text 0}. + machine program by the initial segment of natural numbers starting from @{text 0}. In doing so we can compose two Turing machine programs by shifting the states of one by an appropriate amount to a higher segment and adjusting some ``next states'' in the other. @@ -367,7 +370,10 @@ \begin{equation} \begin{tikzpicture} \node [anchor=base] at (0,0) {@{thm dither_def}}; - \node [anchor=west] at (-1.5,-0.42) {$\underbrace{\hspace{21mm}}_{\text{1st state}}$}; + \node [anchor=west] at (-1.5,-0.64) + {$\underbrace{\hspace{21mm}}_{\text{\begin{tabular}{@ {}l@ {}}1st state\\[-2mm] + = starting state\end{tabular}}}$}; + \node [anchor=west] at ( 1.1,-0.42) {$\underbrace{\hspace{17mm}}_{\text{2nd state}}$}; \node [anchor=west] at (-1.5,0.65) {$\overbrace{\hspace{10mm}}^{\text{@{term Bk}-case}}$}; \node [anchor=west] at (-0.1,0.65) {$\overbrace{\hspace{6mm}}^{\text{@{term Oc}-case}}$}; @@ -460,7 +466,7 @@ A \emph{configuration} @{term c} of a Turing machine is a state together with a tape. This is written as @{text "(s, (l, r))"}. We - say a configuration is \emph{final} if @{term "s = (0::nat)"} and we + say a configuration \emph{is final} if @{term "s = (0::nat)"} and we say a predicate @{text P} \emph{holds for} a configuration if @{text "P (l, r)"} holds. If we have a configuration and a program, we can calculate what the next configuration is by fetching the appropriate @@ -491,18 +497,49 @@ \end{tabular} \end{center} + \noindent Recall our definition of @{term fetch} (shown in + \eqref{fetch}) with the default value for the @{text 0}-state. In + case a Turing program takes according to the usual textbook + definition \cite{Boolos87} less than @{text n} steps before it + halts, then in our setting the @{term steps}-evaluation does not + actually halt, but rather transitions to the @{text 0}-state (the + final state) and remains there performing @{text Nop}-actions until + @{text n} is reached. + + \begin{figure}[t] + \begin{center} + \begin{tabular}{@ {}p{3.6cm}@ {\hspace{4mm}}p{3.6cm}@ {\hspace{4mm}}p{3.6cm}@ {}} + @{thm (lhs) tcopy_init_def} @{text "\"} & + @{thm (lhs) tcopy_loop_def} @{text "\"} & + @{thm (lhs) tcopy_end_def} @{text "\"}\\ + @{thm (rhs) tcopy_init_def} & + @{thm (rhs) tcopy_loop_def} & + @{thm (rhs) tcopy_end_def} + \end{tabular} + \end{center} + \caption{Copy machine}\label{copy} + \end{figure} + + Before we can prove the undecidability of the halting problem for + Turing machines, we need to analyse two concrete Turing machine + programs and establish that they are correct, that is they are + ``doing what they are supposed to be doing''. This is usually left + out in the informal computability literature, for example + \cite{Boolos87}. One program we prove correct is the @{term dither} + program shown in \eqref{dither} and the other program @{term + "tcopy"} is defined as + + \begin{center} + \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} + @{thm (lhs) tcopy_def} & @{text "\"} & @{thm (rhs) tcopy_def} + \end{tabular} + \end{center} + \noindent - Recall our definition of @{term fetch} (shown in \ref{fetch}) with the default value for - the @{text 0}-state. In case a Turing program takes in \cite{Boolos87} less - then @{text n} steps before it halts, then in our setting the @{term steps}-evaluation - does not actually halt, but rather transitions to the @{text 0}-state and - remains there performing @{text Nop}-actions until @{text n} is reached. - - Before we can prove the undecidability of the halting problem for Turing machines, - we need to analyse two concrete Turing machine programs and establish that - they ``doing what they are supposed to be doing''. To do so we will derive - some Hoare-style reasoning rules for Turing machine programs. A \emph{Hoare-triple} - for a terminating Turing machine program is defined as + whose three components are given in Figure~\ref{copy}. + To prove the correctness, we derive some Hoare-style reasoning rules for + Turing machine programs. A \emph{Hoare-triple} for a terminating Turing + machine program is defined as \begin{center} @{thm Hoare_halt_def} @@ -515,22 +552,10 @@ In the following we will consider the following Turing machine program that makes a copies a value on the tape. - \begin{figure} - \begin{center} - \begin{tabular}{@ {}p{3.6cm}@ {\hspace{4mm}}p{3.6cm}@ {\hspace{4mm}}p{3.6cm}@ {}} - @{thm tcopy_init_def} & - @{thm tcopy_loop_def} & - @{thm tcopy_end_def} - \end{tabular} - \end{center} - \end{figure} + - \begin{center} - \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}p{6.9cm}@ {}} - @{thm (lhs) tcopy_def} & @{text "\"} & @{thm (rhs) tcopy_def} - \end{tabular} - \end{center} + assertion holds for all tapes @@ -594,7 +619,7 @@ \end{center} \noindent - The second opcode @{term "Goto 0"} in this programm means we + The second opcode @{term "Goto 0"} in this program means we jump back to the first opcode, namely @{text "Dec R o"}. The \emph{memory} $m$ of an abacus machine holding the values of the registers is represented as a list of natural numbers.