--- a/Paper.thy	Sun Jan 06 23:50:24 2013 +0000
+++ b/Paper.thy	Tue Jan 08 01:21:02 2013 +0000
@@ -60,33 +60,33 @@
 theorem provers, like Isabelle/HOL, are at their best when the
 data-structures at hand are ``structurally'' defined, like lists,
 natural numbers, regular expressions, etc. Such data-structures come
-convenient reasoning infrastructures (for
+with convenient reasoning infrastructures (for
 example induction principles, recursion combinators and so on).  But
 this is \emph{not} the case with Turing machines (and also not with
 register machines): underlying their definition is a set of states
 together with a transition function, both of which are not
 structurally defined.  This means we have to implement our own
 reasoning infrastructure in order to prove properties about them. This
-leads to annoyingly lengthy and fiddly formalisations.  We noticed
-first the difference between both structural and non-structural
+leads to annoyingly fiddly formalisations.  We noticed
+first the difference between both, structural and non-structural,
 ``worlds'' when formalising the Myhill-Nerode theorem, where regular
 expressions fared much better than automata \cite{WuZhangUrban11}.
 However, with Turing machines there seems to be no alternative if one
 wants to formalise the great many proofs from the literature that use them.
 We will analyse one example---undecidability of Wang tilings---in 
-detail in Section~\ref{Wang}. The standard proof of this property uses 
+Section~\ref{Wang}. The standard proof of this property uses 
 the notion of \emph{universal Turing machines}.
 
 We are not the first who formalised Turing machines in a theorem
 prover: we are aware of the preliminary work by Asperti and Ricciotti
 \cite{AspertiRicciotti12}. They describe a complete formalisation of Turing
-machines in the Matita theorem prover, including an universal Turing
+machines in the Matita theorem prover, including a universal Turing
 machine. They report 
 that the informal proofs from which they started are not 
 ``sufficiently accurate to be directly used as a guideline for 
 formalization'' \cite[Page 2]{AspertiRicciotti12}. For our formalisation 
 we followed the proofs from the textbook \cite{Boolos87} and found that the description
-is quite detailed. Some details are left out however: for 
+there is quite detailed. Some details are left out however: for 
 example, it is only shown how the universal
 Turing machine is constructed for Turing machines computing unary 
 functions. We had to figure out a way to generalize this result to
@@ -99,7 +99,7 @@
 The main difference between our formalisation and the one by Asperti and
 Ricciotti  is that their universal Turing 
 machine uses a different alphabet than the machines it simulates. They
-write \cite[Page XXX]{AspertiRicciotti12}:
+write \cite[Page 23]{AspertiRicciotti12}:
 
 \begin{quote}\it
 ``In particular, the fact that the universal machine operates with a
@@ -112,7 +112,7 @@
 where Turing machines (and our
 universal Turing machine) operates on tapes that contain only blank
 or filled cells (respectively represented by 0 and 1---or in our 
-formalisation by @{term Bk} or @{term Oc}).
+formalisation by @{term Bk} and @{term Oc}).
 
 
 

--- a/document/root.tex	Sun Jan 06 23:50:24 2013 +0000
+++ b/document/root.tex	Tue Jan 08 01:21:02 2013 +0000
@@ -16,7 +16,7 @@
 
 \begin{document}
 
-\title{A Formalised Theory of Turing Machines in Isabelle/HOL}
+\title{Formalising Computability Theory in Isabelle/HOL}
 
 
 \author{
@@ -31,19 +31,20 @@
 
 
 \begin{abstract}
-Isabelle/HOL is an interactive theorem prover based on classical 
-logic. While classical reasoning allow users to take convenient 
-shortcuts in some proofs, it precludes \emph{direct} reasoning about 
-decidability: every boolean predicate is either true or false
-because of the law of excluded middle. The only way to reason
-about decidability in a classical theorem prover, like Isabelle/HOL,
-is to formalise a concrete model for computation. In this paper
-we formalise Turing machines and relate them to register machines.
-
+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 for computation. 
+We formalise Turing machines and relate them to abacus machines and recursive
+functions. Our theory can be used to formalise other computability results:
+we give one example about the undecidability of Wang tilings, whose proof uses
+the notion of a universal Turing machine.
 \end{abstract}
 
 \begin{IEEEkeywords}
-Turing Machines, Decidability, Isabelle/HOL;
+Turing Machines, Computability, Isabelle/HOL, Wang tilings
 \end{IEEEkeywords}
 
 

Binary file paper.pdf has changed