--- a/Paper/Paper.thy	Tue Feb 05 10:23:08 2013 +0000
+++ b/Paper/Paper.thy	Tue Feb 05 12:41:00 2013 +0000
@@ -1278,53 +1278,82 @@
   We have formalised the main results from three chapters in the
   textbook by Boolos et al \cite{Boolos87}.  Following in the
   footsteps of another paper \cite{Nipkow98} formalising the results
-  from a textbook, we could have titled our paper ``Boolos et al are
+  from a semantics textbook, we could have titled our paper ``Boolos et al are
   (almost) Right''. We have not attempted to formalise everything
-  precisely as Boolos et al present it, but find definitions that make
-  mechanised proofs manageable. We have found a small inconsitency in
-  the usage of definitions of \ldots Our interest in this subject
+  precisely as Boolos et al present it, but use definitions that make
+  mechanised proofs manageable. For example our definition of the 
+  halting state performing @{term Nop}-operations seems to be non-standard, 
+  but very much suited to a formalisation in a theorem prover where
+  the @{term steps}-function need to be total. We have found an 
+  inconsitency in
+  Bolos et al's usage of definitions of \ldots 
+  Our interest in Turing machines 
   arose from correctness proofs about algorithms where we were unable
-  to formalise argumants about decidability.
-
+  to formalise arguments about decidability but also undecidability
+  proofs in general (for example Wang's tiling problem \cite{Robinson71}).
 
   The most closely related work is by Norrish \cite{Norrish11}, and
-  Asperti and Ricciotti \cite{AspertiRicciotti12}. Norrish bases his
-  approach on $\lambda$-terms. For this he introduced a clever rewriting
-  technology based on combinators and de-Bruijn indices for rewriting
-  modulo $\beta$-equivalence (to keep it manageable)
-
-
-
-  \noindent
-  Later on we need to consider specific Turing machines that 
-  start with a tape in standard form and halt the computation
-  in standard form. To define a tape in standard form, it is
-  useful to have an operation %@{ term "tape_of_nat_list DUMMY"} 
-  that translates lists of natural numbers into tapes. 
-
+  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
+  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 universial 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)
   
-  \noindent
-  This means the Turing machine starts with a tape containg @{text n} @{term Oc}s
-  and the head pointing to the first one; the Turing machine
-  halts with a tape consisting of some @{term Bk}s, followed by a 
-  ``cluster'' of @{term Oc}s and after that by some @{term Bk}s.
-  The head in the output is pointing again at the first @{term Oc}.
-  The intuitive meaning of this definition is to start the Turing machine with a
-  tape corresponding to a value @{term n} and producing
-  a new tape corresponding to the value @{term l} (the number of @{term Oc}s
-  clustered on the output tape).
+  Our work was 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
+  complexity theory. They formalised a universial 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.
+  
+  For us the most interesting aspect of our work are the correctness 
+  proofs for some Turing machines. Informal presentation of computability
+  theory often leave the constructions of particular Turing machines
+  as excercise 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 establised for showing correctness and termination.
+  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 magnitute of weeks. 
 
-
-  
-  Magnus: invariants -- Section 5.4.5 on page 75.
-
-
-  There is a tantalising connection with recent work \cite{Jensen13}
-  about verifying X86 assembly code. They observed 
+  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 assmebly programs that Hoare-style reasoning is sometimes
+  possible, but sometimes 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 assmebly code can make it easier to reason about our Turing
   programs.
-  
+  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/}
 *}
 
 

Binary file paper.pdf has changed