--- a/Paper.thy	Fri Jan 04 13:10:30 2013 +0000
+++ b/Paper.thy	Fri Jan 04 22:49:02 2013 +0000
@@ -53,42 +53,62 @@
 \end{quote}
 
 \noindent
-In this paper we took on this daunting prospect and provide a formalisation
-of Turing machines, as well as Abacus machines (a kind of register machine)
-and recursive functions. To see the difficulties involved with this work one
-has to understantd that interactive 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). For them, they come with a convenient reasoning 
-infrastructure (for example induction principles, recursion combinators and so on).
-But this is not the case with Turing machines  (and also 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. This often
-leads to annoyingly lengthy and detailed formalisations.  We noticed first 
-the difference between both ``worlds'' when formalising the Myhill-Nerode 
-theorem ??? where regular expressions fared much better than automata. 
-However, with Turing machines there seems to be no alternative, because they
-feature frequently in proofs. We will analyse one case, Wang tilings, at the end 
-of the paper, which uses also the notion of a Universal Turing Machine.
+In this paper we took on this daunting prospect and provide a
+formalisation of Turing machines, as well as abacus machines (a kind
+of register machines) and recursive functions. To see the difficulties
+involved with this work, one has to understand that interactive
+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
+in theorem provers 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 detailed 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 that use them. We give as
+example one proof---undecidability of Wang tilings---in Section
+\ref{Wang}. The standard proof of this property uses the notion of
+\emph{universal Turing machines}.
 
-The reason why reasoning about Turing machines 
-is challenging is because they are essentially ... 
+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 formalisation of Turing
+machines in the Matita theorem prover. 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 
+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
+$n$-ary functions. Similarly, when compiling recursive functions to 
+abacus machines, the textbook again only shows how it can be done for 
+2- and 3-ary functions, but in the formalisation we need arbitrary 
+function. But the general ideas for how to do this are clear enough in 
+\cite{Boolos87}.
 
+The main difference between our formalisation and the one by Asperti and
+Ricciotti is 
 
-For this we followed mainly the informal
-proof given in the textbook \cite{Boolos87}.
+that their universal machines 
+
+\begin{quote}
+``In particular, the fact that the universal machine operates with a
+different alphabet with respect to the machines it simulates is
+annoying.'' 
+\end{quote}
 
 
 
 
-``In particular, the fact that the universal machine operates with a
-different alphabet with respect to the machines it simulates is
-annoying.'' he writes it is preliminary work \cite{AspertiRicciotti12}
-
-
-Our formalisation follows \cite{Boolos87}
-
 \noindent
 {\bf Contributions:} 
 
@@ -101,7 +121,7 @@
 *}
 
 
-section {* Wang Tiles *}
+section {* Wang Tiles\label{Wang} *}
 
 text {*
   Used in texture mapings - graphics

--- a/document/root.bib	Fri Jan 04 13:10:30 2013 +0000
+++ b/document/root.bib	Fri Jan 04 22:49:02 2013 +0000
@@ -42,4 +42,15 @@
   title     = {{C}omputability and {L}ogic (2.~ed.)},
   publisher = {Cambridge University Press},
   year      = {1987}
-}
\ No newline at end of file
+}
+
+@inproceedings{WuZhangUrban11,
+  author    = {C.~Wu and X.~Zhang and C.~Urban},
+  title     = {{A} {F}ormalisation of the {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions
+               ({P}roof {P}earl)},
+  booktitle = {Proc.~of the 2nd Conference on Interactive Theorem Proving},
+  year      = {2011},
+  pages     = {341--356},
+  series    = {LNCS},
+  volume    = {6898}
+}

Binary file paper.pdf has changed