tm: comparison Paper/Paper.thy

equal deleted inserted replaced

-:7f5243700f25
+:4d7a568bd911
 In this paper we take on this daunting prospect and provide a
 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 containing the infamous gotos \cite{Dijkstra68}. This
+Basic programs containing 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
 turn recursive functions to abacus machines. The universal Turing
 machine can then be constructed as a recursive function.
 \smallskip
 \noindent
-{\bf Contributions:} We formalised in Isabelle/HOL Turing machines following the
+{\bf Contributions:} We formalised in Isabelle/HOL Turing machines
-description of Boolos et al \cite{Boolos87} where tapes only have blank or
+following the description of Boolos et al \cite{Boolos87} where tapes
-occupied cells. We mechanise the undecidability of the halting problem and
+only have blank or occupied cells. We mechanise the undecidability of
-prove the correctness of concrete Turing machines that are needed
+the halting problem and prove the correctness of concrete Turing
-in this proof; such correctness proofs are left out in the informal literature.
+machines that are needed in this proof; such correctness proofs are
-For reasoning about Turing machine programs we derive Hoare-rules.
+left out in the informal literature.  For reasoning about Turing
-We also construct the universal Turing machine from \cite{Boolos87} by
+machine programs we derive Hoare-rules.  We also construct the
-translating recursive functions to abacus machines and abacus machines to
+universal Turing machine from \cite{Boolos87} by translating recursive
-Turing machines. Since we have set up in Isabelle/HOL a very general computability
+functions to abacus machines and abacus machines to Turing
-model and undecidability result, we are able to formalise other
+machines. When formalising the universal Turing machine,
-results: we describe a proof of the computational equivalence
+we stumbled upon an inconsistence use of the definition of
-of single-sided Turing machines, which is not given in \cite{Boolos87},
+what function a Turing machine calculates. Since we have set up in
-but needed for example for formalising the undecidability proof of
+Isabelle/HOL a very general computability model and undecidability
-Wang's tiling problem \cite{Robinson71}.
+result, we are able to formalise other results: we describe a proof of
-%We are not aware of any other
+the computational equivalence of single-sided Turing machines, which
-%formalisation of a substantial undecidability problem.
+is not given in \cite{Boolos87}, 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.
 *}
 section {* Turing Machines *}
 text {* \noindent
 @{thm (lhs) nats2tape(3)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(3)}
 \end{tabular}}\label{standard}
 \end{equation}
 %
 \noindent
-A \emph{standard tape} is then of the form @{text "(Bk\<^isup>l,\<langle>[n\<^isub>1,...,n\<^isub>m]\<rangle>)"} for some @{text l}
+A \emph{standard tape} is then of the form @{text "(Bk\<^isup>k,\<langle>[n\<^isub>1,...,n\<^isub>m]\<rangle> @ Bk\<^isup>l)"} for some @{text k},
+@{text l}
 and @{text "n\<^bsub>1...m\<^esub>"}. Note that the head in a standard tape ``points'' to the
 leftmost @{term "Oc"} on the tape. Note also that the natural number @{text 0}
 is represented by a single filled cell on a standard tape, @{text 1} by two filled cells and so on.
 Before we can prove the undecidability of the halting problem for
 \end{tabular}
 \end{center}
 \noindent
 This invariant depends on @{term n} representing the number of
-@{term Oc}s@{text "+1"} (or encoded number) on the tape. It is not hard (26
+@{term Oc}s on the tape. It is not hard (26
 lines of automated proof script) to show that for @{term "n >
 (0::nat)"} this invariant is preserved under the computation rules
 @{term step} and @{term steps}. This gives us partial correctness
 for @{term "tcopy_begin"}.

changeset 141	4d7a568bd911
parent 140	7f5243700f25
child 142	21c7139ffa07