diff -r 8c7f10b3da7b -r 49f8e5cf82c5 Paper/Paper.thy --- a/Paper/Paper.thy Thu Jan 24 00:20:26 2013 +0100 +++ b/Paper/Paper.thy Thu Jan 24 10:53:43 2013 +0100 @@ -96,7 +96,7 @@ is always provable no matter whether @{text P} is constructed by computable means. We hit this limitation previously when we mechanised the correctness proofs of two algorithms \cite{UrbanCheneyBerghofer11,WuZhangUrban12}, -but were unable to formalise arguments about computability. +but were unable to formalise arguments about decidability. %The same problem would arise if we had formulated %the algorithms as recursive functions, because internally in @@ -218,7 +218,8 @@ occupied cells. We mechanise the undecidability of the halting problem and prove the correctness of concrete Turing machines that are needed in this proof; such correctness proofs are left out in the informal literature. -We construct the universal Turing machine from \cite{Boolos87} by +For reasoning about Turing machine programs we derive Hoare-rules. +We also construct the universal Turing machine from \cite{Boolos87} by relating recursive functions to abacus machines and abacus machines to Turing machines. Since we have set up in Isabelle/HOL a very general computability model and undecidability result, we are able to formalise other @@ -425,12 +426,47 @@ state, and the third that every next-state is one of the states mentioned in the program or being the @{text 0}-state. - A \emph{configuration} @{term c} of a Turing machine is a state together with - a tape. This is written as @{text "(s, (l, r))"}. If we have a - configuration and a program, we can calculate - what the next configuration is by fetching the appropriate action and next state - from the program, and by updating the state and tape accordingly. - This single step of execution is defined as the function @{term step} + We need to be able to sequentially compose Turing machine programs. Given our + concrete representation, this is relatively straightforward, if + slightly fiddly. We use the following two auxiliary functions: + + \begin{center} + \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} + @{thm (lhs) shift.simps} @{text "\"} @{thm (rhs) shift.simps}\\ + @{thm (lhs) adjust.simps} @{text "\"} @{thm (rhs) adjust.simps}\\ + \end{tabular} + \end{center} + + \noindent + The first adds @{text n} to all states, exept the @{text 0}-state, + thus moving all ``regular'' states to the segment starting at @{text + n}; the second adds @{term "Suc(length p div 2)"} to the @{text + 0}-state, thus redirecting all references to the ``halting state'' + to the first state after the program @{text p}. With these two + functions in place, we can define the \emph{sequential composition} + of two Turing machine programs @{text "p\<^isub>1"} and @{text "p\<^isub>2"} + + \begin{center} + @{thm tm_comp.simps[where ?p1.0="p\<^isub>1" and ?p2.0="p\<^isub>2", THEN eq_reflection]} + \end{center} + + \noindent + %This means @{text "p\<^isub>1"} is executed first. Whenever it originally + %transitioned to the @{text 0}-state, it will in the composed program transition to the starting + %state of @{text "p\<^isub>2"} instead. All the states of @{text "p\<^isub>2"} + %have been shifted in order to make sure that the states of the composed + %program @{text "p\<^isub>1 \ p\<^isub>2"} still only ``occupy'' + %an initial segment of the natural numbers. + + 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 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 + action and next state from the program, and by updating the state + and tape accordingly. This single step of execution is defined as + the function @{term step} \begin{center} \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} @@ -463,38 +499,19 @@ 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 have to define how to compose two Turing machine programs. Given our setup, this is - relatively straightforward, if slightly fiddly. We use the following two - auxiliary functions: + 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 \begin{center} - \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} - @{thm (lhs) shift.simps} @{text "\"} @{thm (rhs) shift.simps}\\ - @{thm (lhs) adjust.simps} @{text "\"} @{thm (rhs) adjust.simps}\\ - \end{tabular} + @{thm Hoare_halt_def} \end{center} - \noindent - The first adds @{text n} to all states, exept the @{text 0}-state, - thus moving all ``regular'' states to the segment starting at @{text - n}; the second adds @{term "Suc(length p div 2)"} to the @{text - 0}-state, thus redirecting all references to the ``halting state'' - to the first state after the program @{text p}. With these two - functions in place, we can define the \emph{sequential composition} - of two Turing machine programs @{text "p\<^isub>1"} and @{text "p\<^isub>2"} - \begin{center} - @{thm tm_comp.simps[where ?p1.0="p\<^isub>1" and ?p2.0="p\<^isub>2", THEN eq_reflection]} + @{thm Hoare_unhalt_def} \end{center} - \noindent - %This means @{text "p\<^isub>1"} is executed first. Whenever it originally - %transitioned to the @{text 0}-state, it will in the composed program transition to the starting - %state of @{text "p\<^isub>2"} instead. All the states of @{text "p\<^isub>2"} - %have been shifted in order to make sure that the states of the composed - %program @{text "p\<^isub>1 \ p\<^isub>2"} still only ``occupy'' - %an initial segment of the natural numbers. - In the following we will consider the following Turing machine program that makes a copies a value on the tape.