--- a/Paper/Paper.thy	Wed Feb 06 13:28:01 2013 +0000
+++ b/Paper/Paper.thy	Wed Feb 06 14:06:18 2013 +0000
@@ -1366,23 +1366,23 @@
 
 text {*
   In previous works we were unable to formalise results about
-  computability because in a Isabelle/HOL we cannot represent the
+  computability because in Isabelle/HOL we cannot represent the
   decidability of a predicate @{text P}, say, as the formula @{term "P
   \<or> \<not>P"}. For reasoning about computability we need to formalise a
   concrete model of computations. We could have followed Norrish
   \cite{Norrish11} using the $\lambda$-calculus as the starting point,
   but then we would have to reimplement his infrastructure for
   reducing $\lambda$-terms on the ML-level. We would still need to
-  connect his work to Turing machines for proofs that make use of them
+  connect his work to Turing machines for proofs that make essential use of them
   (for example the proof of Wang's tiling problem \cite{Robinson71}).
 
   We therefore have formalised Turing machines and the main
   computability results from Chapters 3 to 8 in the textbook by Boolos
   et al \cite{Boolos87}.  For this we did not need to implement
   anything on the ML-level of Isabelle/HOL. While formalising
-  \cite{Boolos87} have found an inconsistency in Bolos et al's usage
-  of definitions of what function a Turing machine calculates. In
-  Chapter 3 they use a definition such that the function is undefined
+  \cite{Boolos87} we have found an inconsistency in Bolos et al's 
+  definitions of what function a Turing machine calculates. In
+  Chapter 3 they use a definition that states a function is undefined
   if the Turing machine loops \emph{or} halts with a non-standard
   tape. Whereas in Chapter 8 about the universal Turing machine, the
   Turing machines will \emph{not} halt unless the tape is in standard
@@ -1396,26 +1396,22 @@
   non-standard, but very much suited to a formalisation in a theorem
   prover where the @{term steps}-function need to be total.
 
-  The most closely related work is by Norrish \cite{Norrish11}, and
-  Asperti and Ricciotti \cite{AspertiRicciotti12}. Norrish formalises
-  computability theory using $\lambda$-terms. For this he introduced a
-  clever rewriting technology based on combinators and de-Bruijn
-  indices for rewriting modulo $\beta$-equivalence (in order to avoid
-  explicit $\alpha$-renamings). He mentions that formalising Turing
-  machines would be a ``daunting prospect'' \cite[Page
-  310]{Norrish11}. While $\lambda$-terms indeed lead to some slick
-  mechanised proofs, our experience is that Turing machines are not
-  too daunting if one is only concerned with formalising the
+  The most closely related work is by Norrish \cite{Norrish11}, and by
+  Asperti and Ricciotti \cite{AspertiRicciotti12}. Norrish mentions
+  that formalising Turing machines would be a ``daunting prospect''
+  \cite[Page 310]{Norrish11}. While $\lambda$-terms indeed lead to
+  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 longer than a mechanised proof pearl about the Myhill-Nerode
-  theorem. So our conclusion is it not as daunting as we imagined
-  reading the paper by Norrish \cite{Norrish11}. The work involved
-  with constructing a universal Turing machine via recursive 
-  functions and abacus machines, on the other hand, is not a
-  project one wants to undertake too many times (our formalisation
-  of abacus machines and their correct translation is approximately 
-  4300 loc; \ldots)
+  times of a mechanised proof pearl about the Myhill-Nerode
+  theorem. So our conclusion is it not as daunting 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, on the other hand, 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 XX loc and the universal Turing machine XX loc).
   
   Our work was also very much inspired by the formalisation of Turing
   machines by Asperti and Ricciotti \cite{AspertiRicciotti12} in the
@@ -1426,40 +1422,44 @@
   complexity theory. They formalised a universal Turing machine
   (which differs from ours by using a more general alphabet), but did
   not describe an undecidability proof. Given their definitions and
-  infrastructure, we expect this should not be too difficult for them.
+  infrastructure, we expect however this should not be too difficult 
+  for them.
   
-  For us the most interesting aspect of our work are the correctness 
-  proofs for some Turing machines. Informal presentation of computability
+  For us the most interesting aspect 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, as \cite{Boolos87} for example, deeming it 
-  too easy for wasting space. However, as far as we are aware all
-  informal presentation leave out any correctness proofs---do the 
-  Turing machines really perform the task they are supposed to do. 
-  This means we have to find appropriate invariants and measures
-  that can be established for showing correctness and termination.
+  as exercise to the reader, as 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 or formalsiser is left
+  with the task of finding appropriate invariants and measures for
+  showing 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 by Myreen for a correctness proof of a garbage
-  collector \cite[Page 76]{}. 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, something on the magnitude of weeks. 
+  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}. Howvere, 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
+  weeks.
 
-  Our reasoning about the invariants is also not very much 
-  supported by the automation in Isabelle. There is however a tantalising 
-  connection between our work and recent work \cite{Jensen13}
-  on verifying X86 assembly code. They observed a similar phenomenon
-  with assembly programs that Hoare-style reasoning is sometimes
-  possible, but sometimes not. In order to ease their reasoning they
+  Our reasoning about the invariants is not much supported by the
+  automation in Isabelle. There is however a tantalising connection
+  between our work and very recent work \cite{Jensen13} on verifying
+  X86 assembly code. They observed a similar phenomenon with assembly
+  programs that 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
-  for special cases Hoare-rules can be provided.
-  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 attractive result, because Turing 
-  machine programs are 
-
-  The code of our formalisation is available from the Mercurial repository at
-  \url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/tm/}
+  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
+  attractive result, because Turing machine programs are very much
+  like assmbly programs and it would connect some very classic work on
+  Turing machines with very cutting-edge work on machine code
+  verification. In order to try out such ideas, our formalisation provides the
+  ``playground''. The code of our formalisation is available from the
+  Mercurial repository at\\
+  \url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/tm/}.
 *}
 
 

--- a/Paper/document/root.bib	Wed Feb 06 13:28:01 2013 +0000
+++ b/Paper/document/root.bib	Wed Feb 06 14:06:18 2013 +0000
@@ -1,3 +1,12 @@
+
+
+@PhdThesis{Myreen09,
+  author =	 {M.~O.~Myreen},
+  title = 	 {{F}ormal {V}erification of {M}achine-{C}ode {P}rograms},
+  year = 	 2009,
+  school =  {University of Cambridge}
+}
+
 @article{Nipkow98,
   author={T.~Nipkow},
   title={{W}inskel is (almost) {R}ight: {T}owards a {M}echanized {S}emantics {T}extbook},

Binary file paper.pdf has changed