Binary file Literature/document.pdf has changed

--- a/Paper.thy	Tue Jan 08 01:21:02 2013 +0000
+++ b/Paper.thy	Wed Jan 09 13:35:09 2013 +0000
@@ -60,46 +60,49 @@
 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
-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 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 
-Section~\ref{Wang}. The standard proof of this property uses 
-the notion of \emph{universal Turing machines}.
+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 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 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 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
-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
-$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 
-functions. But the general ideas for how to do this are clear enough in 
-\cite{Boolos87}.
+\cite{AspertiRicciotti12}. They describe a complete formalisation of
+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 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 $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 functions. But the general ideas for
+how to do this are clear enough in \cite{Boolos87}. However, one
+aspect that is completely left out from the informal description in
+\cite{Boolos87}, and similar ones we are aware of, are arguments why certain Turing
+machines are correct. We will introduce Hoare-style proof rules
+which help us with such correctness arguments of Turing machines.
 
-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 23]{AspertiRicciotti12}:
+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
+23]{AspertiRicciotti12}:
 
 \begin{quote}\it
 ``In particular, the fact that the universal machine operates with a
@@ -108,25 +111,57 @@
 \end{quote}
 
 \noindent
-In this paper we follow the approach by Boolos et al \cite{Boolos87}
-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} and @{term Oc}).
+In this paper we follow the approach by Boolos et al \cite{Boolos87},
+which goes back to Post \cite{Post36}, where all Turing machines
+operate on tapes that contain only blank or filled cells (represented 
+by @{term Bk} and @{term Oc}, respectively, in our
+formalisation). Traditionally the content of a cell can be any
+character from a finite alphabet. Although computationally
+equivalennt, the more restrictive notion of Turing machines make
+the reasoning more uniform. Unfortunately, it also makes it
+harder to design programs for Turing machines. Therefore
+in order to construct a \emph{universal Turing machine} we follow
+the proof in \cite{Boolos87} by relating abacus machines to
+turing machines and in turn recursive functions to abacus machines. 
 
-
-
+\medskip
 \noindent
 {\bf Contributions:} 
 
 *}
 
-section {* Formalisation *}
+section {* Turing Machines *}
 
 text {*
+
+  Tapes
+
+  %\begin{center}
+  %\begin{tikzpicture}
+  %%
+  %\end{tikzpicture}
+  %\end{center}
+  
+  An action is defined as 
+
+  \begin{center}
+  \begin{tabular}{rcll}
+  @{text "a"} & $::=$  & @{term "W0"} & write blank (@{term Bk})\\
+  & $\mid$ & @{term "W1"} & write occupied (@{term Oc})\\
+  & $\mid$ & @{term L} & move left\\
+  & $\mid$ & @{term R} & move right\\
+  & $\mid$ & @{term Nop} & do nothing\\
+  \end{tabular}
+  \end{center}
+
+  For showing the undecidability of the halting problem, we need to consider
+  two specific Turing machines.
   
 *}
 
+section {* Abacus Machines *}
+
+section {* Recursive Functions *}
 
 section {* Wang Tiles\label{Wang} *}
 
@@ -138,7 +173,8 @@
 section {* Related Work *}
 
 text {*
-  The most closely related work is by Norrish. He bases his approach on 
+  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)

--- a/document/root.bib	Tue Jan 08 01:21:02 2013 +0000
+++ b/document/root.bib	Wed Jan 09 13:35:09 2013 +0000
@@ -54,3 +54,15 @@
   series    = {LNCS},
   volume    = {6898}
 }
+
+
+@Article{Post36,
+  author =       {E.~Post},
+  title =        {{F}inite {C}ombinatory {P}rocesses-{F}ormulation 1},
+  journal =      {Journal of Symbolic Logic},
+  year =         {1936},
+  volume =       {1},
+  number =       {3},
+  pages =        {103--105}
+}
+

Binary file paper.pdf has changed