tm: comparison Paper/Paper.thy

equal deleted inserted replaced

-:6a584d61820f
+:b4b789a59086
 it harder to design programs for these Turing machines. In order
 to construct a universal Turing machine we therefore do not follow
 \cite{AspertiRicciotti12}, instead follow the proof in
 \cite{Boolos87} by translating abacus machines to Turing machines and in
 turn recursive functions to abacus machines. The universal Turing
-machine can then be constructed as a recursive function.
+machine can then be constructed by translating from a recursive function.
 \smallskip
 \noindent
 {\bf Contributions:} We formalised in Isabelle/HOL Turing machines
 following the description of Boolos et al \cite{Boolos87} where tapes
 universal Turing machine from \cite{Boolos87} by translating recursive
 functions to abacus machines and abacus machines to Turing
 machines. This works essentially like a small, verified compiler
 from recursive functions to Turing machine programs.
 When formalising the universal Turing machine,
-we stumbled upon an inconsistent use of the definition of
+we stumbled in \cite{Boolos87} upon an inconsistent use of the definition of
 what partial function a Turing machine calculates.
 %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 @{text 0}-state is special in that it will be used as the
 ``halting state''.  There are no instructions for the @{text
 0}-state, but it will always perform a @{term Nop}-operation and
 remain in the @{text 0}-state.  Unlike Asperti and Riccioti
 \cite{AspertiRicciotti12}, we have chosen a very concrete
-representation for programs, because when constructing a universal
+representation for Turing machine programs, because when constructing a universal
 Turing machine, we need to define a coding function for programs.
 This can be directly done for our programs-as-lists, but is
 slightly more difficult for the functions used by Asperti and Ricciotti.
 Given a program @{term p}, a state
-and the cell being read by the head, we need to fetch
+and the cell being scanned by the head, we need to fetch
 the corresponding instruction from the program. For this we define
 the function @{term fetch}
 \begin{equation}\label{fetch}
 \mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
 some slick mechanised proofs, our experience is that Turing machines
 are not too daunting if one is only concerned with formalising the
 undecidability of the halting problem for Turing machines.  This
 took us around 1500 loc of Isar-proofs, which is just one-and-a-half
 times of a mechanised proof pearl about the Myhill-Nerode
-theorem. So our conclusion is that it not as daunting for this part of the
+theorem. So our conclusion is that this part is not as daunting
-work as we estimated when reading the paper by Norrish \cite{Norrish11}. The work
+as we estimated when reading the paper by Norrish \cite{Norrish11}. The work
 involved with constructing a universal Turing machine via recursive
 functions and abacus machines, we agree, is not a project
 one wants to undertake too many times (our formalisation of abacus
 machines and their correct translation is approximately 4300 loc;
 recursive functions 5000 loc and the universal Turing machine 10000 loc).
-Our work was also very much inspired by the formalisation of Turing
+Our work is also very much inspired by the formalisation of Turing
 machines by Asperti and Ricciotti \cite{AspertiRicciotti12} in the
 Matita theorem prover. It turns out that their notion of
 realisability and our Hoare-triples are very similar, however we
 differ in some basic definitions for Turing machines. Asperti and
 Ricciotti are interested in providing a mechanised foundation for
 (which differs from ours by using a more general alphabet), but did
 not describe an undecidability proof. Given their definitions and
 infrastructure, we expect however this should not be too difficult
 for them.
-For us the most interesting aspect of our work are the correctness
+For us the most interesting aspects of our work are the correctness
 proofs for Turing machines. Informal presentations of computability
 theory often leave the constructions of particular Turing machines
 as exercise to the reader, for example \cite{Boolos87}, deeming
 it to be just a chore. However, as far as we are aware all informal
 presentations leave out any arguments why these Turing machines
 should be correct.  This means the reader is left
 with the task of finding appropriate invariants and measures for
-showing correctness and termination of these Turing machines.
+showing the correctness and termination of these Turing machines.
 Whenever we can use Hoare-style reasoning, the invariants are
 relatively straightforward and much smaller than for example the
 invariants used by Myreen in a correctness proof of a garbage collector
 written in machine code \cite[Page 76]{Myreen09}. However, the invariant
 needed for the abacus proof, where Hoare-style reasoning does not work, is
 similar in size as the one by Myreen and finding a sufficiently
-strong one took us, like Myreen for his, something on the magnitude of
+strong one took us, like Myreen, something on the magnitude of
 weeks.
 Our reasoning about the invariants is not much supported by the
 automation beyond the standard automation tools available in Isabelle/HOL.
 There is however a tantalising connection
 between our work and very recent work \cite{Jensen13} on verifying
 X86 assembly code that might change that. They observed a similar phenomenon with assembly
-programs that Hoare-style reasoning is sometimes possible, but
+programs where Hoare-style reasoning is sometimes possible, but
 sometimes it is not. In order to ease their reasoning, they
 introduced a more primitive specification logic, on which
 Hoare-rules can be provided for special cases.  It remains to be
 seen whether their specification logic for assembly code can make it
 easier to reason about our Turing programs. That would be an

changeset 159	b4b789a59086
parent 158	6a584d61820f
child 162	a63c3f8d7234