--- 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)