--- a/Paper/Paper.thy	Fri Mar 29 01:36:45 2013 +0000
+++ b/Paper/Paper.thy	Fri Mar 29 02:40:38 2013 +0000
@@ -280,36 +280,39 @@
 %formalise in Isabelle/HOL computability arguments about the
 %algorithms. 
 
+%Suppose you want to mechanise a proof for whether a predicate @{term P}, 
+%say, is decidable or not. Decidability of @{text P} usually
+%amounts to showing whether \mbox{@{term "P \<or> \<not>P"}} holds. But this
+%does \emph{not} work in 
 
-\noindent
-Suppose you want to mechanise a proof for whether a predicate @{term
-P}, say, is decidable or not. Decidability of @{text P} usually
-amounts to showing whether \mbox{@{term "P \<or> \<not>P"}} holds. But this
-does \emph{not} work in Isabelle/HOL and other HOL theorem provers,
-since they are based on classical logic where the law of excluded
-middle ensures that \mbox{@{term "P \<or> \<not>P"}} is always provable no
-matter whether @{text P} is constructed by computable means. We hit on
-this limitation previously when we mechanised the correctness proofs
-of two algorithms \cite{UrbanCheneyBerghofer11,WuZhangUrban12}, but
-were unable to formalise arguments about decidability or undecidability.
+
+%Since Isabelle/HOL and other HOL theorem provers,
+%are based on classical logic where the law of excluded
+%middle ensures that \mbox{@{term "P \<or> \<not>P"}} is always provable no
+%matter whether @{text P} is constructed by computable means. We hit on
+%this limitation previously when we mechanised the correctness proofs
+%of two algorithms \cite{UrbanCheneyBerghofer11,WuZhangUrban12}, but
+%were unable to formalise arguments about decidability or undecidability.
 
 %The same problem would arise if we had formulated
 %the algorithms as recursive functions, because internally in
 %Isabelle/HOL, like in all HOL-based theorem provers, functions are
 %represented as inductively defined predicates too.
 
-The only satisfying way out of this problem in a theorem prover based
-on classical logic is to formalise a theory of computability. Norrish
-provided such a formalisation for HOL4. He choose the
-$\lambda$-calculus as the starting point for his formalisation because
-of its ``simplicity'' \cite[Page 297]{Norrish11}.  Part of his
-formalisation is a clever infrastructure for reducing
-$\lambda$-terms. He also established the computational equivalence
-between the $\lambda$-calculus and recursive functions.  Nevertheless
-he concluded that it would be appealing to have formalisations for
-more operational models of computations, such as Turing machines or
-register machines.  One reason is that many proofs in the literature
-use them.  He noted however that \cite[Page 310]{Norrish11}:
+\noindent
+The motivation of this paper is to bring the ability to reason
+about results from computability theory, for example decidability of the halting problem,
+to the theorem prover Isabelle/HOL.  Norrish formalised computability
+theory in HOL4. He choose the $\lambda$-calculus as the starting point
+for his formalisation because of its ``simplicity'' \cite[Page
+297]{Norrish11}.  Part of his formalisation is a clever infrastructure
+for reducing $\lambda$-terms. He also established the computational
+equivalence between the $\lambda$-calculus and recursive functions.
+Nevertheless he concluded that it would be appealing to have
+formalisations for more operational models of computations, such as
+Turing machines or register machines.  One reason is that many proofs
+in the literature use them.  He noted however that \cite[Page
+310]{Norrish11}:
 
 \begin{quote}
 \it``If register machines are unappealing because of their 
@@ -410,6 +413,10 @@
 \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 by translating from a recursive function. 
+The part of mechanising the translation of recursive function to register 
+machines has already been done by Zammit in HOL \cite{Zammit99}, 
+although his register machines use a slightly different instruction
+set than the one described in \cite{Boolos87}.
 
 \smallskip
 \noindent
@@ -1244,7 +1251,7 @@
 
   \noindent
   This time the Hoare-triple states that @{term tcontra} terminates 
-  with the ``output'' @{term "<(1::nat)>"}. In both case we come
+  with the ``output'' @{term "<(1::nat)>"}. In both cases we come
   to a contradiction, which means we have to abandon our assumption 
   that there exists a Turing machine @{term H} which can in general decide 
   whether Turing machines terminate.
@@ -1519,7 +1526,7 @@
   unexpected since \cite{Boolos87} is a classic textbook which has
   undergone several editions (we used the fifth edition; the material 
   containing the inconsistency was introduced in the fourth edition
-  \cite{BoolosFourth}). The central
+  of this book). The central
   idea about Turing machines is that when started with standard tapes
   they compute a partial arithmetic function.  The inconsistency arises
   when they define the case when this function should \emph{not} return a
@@ -1740,6 +1747,11 @@
   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/}.
+  \medskip
+
+  \noindent
+  {\bf Acknowledgements:} We are very grateful for the extremely helpful
+  comments by the anonymous reviewers.
 *}
 
 

--- a/Paper/document/root.bib	Fri Mar 29 01:36:45 2013 +0000
+++ b/Paper/document/root.bib	Fri Mar 29 02:40:38 2013 +0000
@@ -143,3 +143,9 @@
 }
 
 
+@phdthesis{Zammit99,
+author = {V.~Zammit},
+title = {{O}n the {R}eadability of {M}achine {C}heckable {F}ormal {P}roofs},
+year = {1999},
+school = {University of Kent}}
+

--- a/Paper/document/root.tex	Fri Mar 29 01:36:45 2013 +0000
+++ b/Paper/document/root.tex	Fri Mar 29 02:40:38 2013 +0000
@@ -50,16 +50,21 @@
 
 \begin{abstract}
 We present a formalised theory of computability in the theorem prover
-Isabelle/HOL. This theorem prover is based on classical logic which
-precludes \emph{direct} reasoning about computability: every boolean
-predicate is either true or false because of the law of excluded
-middle. The only way to reason about computability in a classical
-theorem prover is to formalise a concrete model of computation.  We
-formalise Turing machines and relate them to abacus machines and
-recursive functions. We also formalise a universal Turing machine and
-Hoare-style reasoning techniques that allow us to reason about Turing machine
-programs. Our theory can be used to formalise other computability
-results. %We give one example about the computational equivalence of 
+Isabelle/HOL. 
+%This theorem prover is based on classical logic which
+%precludes \emph{direct} reasoning about computability: every boolean
+%predicate is either true or false because of the law of excluded
+%middle. The only way to reason about computability in a classical
+%theorem prover is to formalise a concrete model of computation.  
+Following the textbook by Boolos et al, we formalise Turing machines
+and relate them to abacus machines and recursive functions. We ``tie
+the know'' between these three computational models by formalising a
+universal function and obtaining from it a universal Turing machine by
+our verified translation from recursive functions to abacus programs
+and from abacus programs to Turing machine programs.  Hoare-style reasoning techniques allow us
+to reason about Turing machine and abacus programs. Our theory can be
+used to formalise other computability results.
+%We give one example about the computational equivalence of 
 %single-sided Turing machines. 
 %{\it we give one example about the undecidability of Wang's tiling problem, whose proof uses
 %the notion of a universal Turing machine.}

Binary file paper.pdf has changed