tm: comparison Paper/Paper.thy

equal deleted inserted replaced

-:8c7f10b3da7b
+:49f8e5cf82c5
 in Isabelle/HOL and other HOL theorem provers, since they are based on classical logic
 where the law of excluded middle ensures that \mbox{@{term "P \<or> \<not>P"}}
 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
 %Isabelle/HOL, like in all HOL-based theorem provers, functions are
 %represented as inductively defined predicates too.
 {\bf Contributions:} We formalised in Isabelle/HOL Turing machines following the
 description of Boolos et al \cite{Boolos87} where tapes only have blank or
 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
 results: we describe a proof of the computational equivalence
 of single-sided Turing machines, which is not given in \cite{Boolos87},
 The first says that @{text p} must have at least an instruction for the starting
 state; the second that @{text p} has a @{term Bk} and @{term Oc} instruction for every
 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
+We need to be able to sequentially compose Turing machine programs. Given our
-a tape. This is written as @{text "(s, (l, r))"}. If we have a
+concrete representation, this is relatively straightforward, if
-configuration and a program, we can calculate
+slightly fiddly. We use the following two auxiliary functions:
-what the next configuration is by fetching the appropriate action and next state
-from the program, and by updating the state and tape accordingly.
+\begin{center}
-This single step of execution is defined as the function @{term step}
+\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+@{thm (lhs) shift.simps} @{text "\<equiv>"} @{thm (rhs) shift.simps}\\
+@{thm (lhs) adjust.simps} @{text "\<equiv>"} @{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 \<oplus> 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}
 @{text "step (s, (l, r)) p"} & @{text "\<equiv>"} & @{text "let (a, s') = fetch p s (read r)"}\\
 & & @{text "in (s', update (l, r) a)"}
 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 have to define how to compose two Turing machine programs. Given our setup, this is
+we need to analyse two concrete Turing machine programs and establish that
-relatively straightforward, if slightly fiddly. We use the following two
+they ``doing what they are supposed to be doing''. To do so we will derive
-auxiliary functions:
+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@ {}}
+\begin{center}
-@{thm (lhs) shift.simps} @{text "\<equiv>"} @{thm (rhs) shift.simps}\\
+@{thm Hoare_halt_def}
-@{thm (lhs) adjust.simps} @{text "\<equiv>"} @{thm (rhs) adjust.simps}\\
+\end{center}
-\end{tabular}
-\end{center}
+\begin{center}
+@{thm Hoare_unhalt_def}
-\noindent
+\end{center}
-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 \<oplus> 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.
 \begin{figure}

changeset 72	49f8e5cf82c5
parent 71	8c7f10b3da7b
child 73	a673539f2f75