# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1360156895 0
# Node ID 8fa9e018abe48d39f6708ff12b186fab2972e2a1
# Parent  ba63ba7d282b6d3d2159845f67d79f960dd1e96d
updated

diff -r ba63ba7d282b -r 8fa9e018abe4 Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Feb 06 05:58:01 2013 +0000
+++ b/Paper/Paper.thy	Wed Feb 06 13:21:35 2013 +0000
@@ -1365,22 +1365,36 @@
 section {* Conclusion *}
 
 text {*
-  We have formalised the main computability results from Chapters 3 to 8 in the
-  textbook by Boolos et al \cite{Boolos87}.  Following in the
-  footsteps of another paper \cite{Nipkow98} formalising the results
-  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 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 
-  inconsistency 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 arguments about decidability but also undecidability
-  proofs in general (for example Wang's tiling problem \cite{Robinson71}).
+  In previous works we were unable to formalise results about
+  computability because in a 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
+  (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
+  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
+  form. Following in the footsteps of another paper \cite{Nipkow98}
+  formalising the results from a semantics textbook, we could
+  therefore 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 use definitions that make our
+  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.
 
   The most closely related work is by Norrish \cite{Norrish11}, and
   Asperti and Ricciotti \cite{AspertiRicciotti12}. Norrish formalises
diff -r ba63ba7d282b -r 8fa9e018abe4 paper.pdf
Binary file paper.pdf has changed