--- a/Paper/Paper.thy Thu Jan 24 18:59:49 2013 +0100
+++ b/Paper/Paper.thy Fri Jan 25 15:57:58 2013 +0100
@@ -133,14 +133,15 @@
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 Turing machine
-programs can be completely \emph{unstructured}, behaving
-similar to Basic programs involving the infamous goto \cite{Dijkstra68}. This precludes in the
-general case a compositional Hoare-style reasoning about Turing
-programs. We provide such Hoare-rules for when it \emph{is} possible to
-reason in a compositional manner (which is fortunately quite often), but also tackle
-the more complicated case when we translate abacus programs into
-Turing programs. This reasoning about Turing machine programs is
-usually completely left out in the informal literature, e.g.~\cite{Boolos87}.
+programs can be completely \emph{unstructured}, behaving similar to
+Basic programs involving the infamous goto \cite{Dijkstra68}. This
+precludes in the general case a compositional Hoare-style reasoning
+about Turing programs. We provide such Hoare-rules for when it
+\emph{is} possible to reason in a compositional manner (which is
+fortunately quite often), but also tackle the more complicated case
+when we translate abacus programs into Turing programs. This
+reasoning about concrete Turing machine programs is usually
+left out in the informal literature, e.g.~\cite{Boolos87}.
%To see the difficulties
%involved with this work, one has to understand that interactive
@@ -230,7 +231,8 @@
model and undecidability result, we are able to formalise other
results: we describe a proof of the computational equivalence
of single-sided Turing machines, which is not given in \cite{Boolos87},
-but needed for formalising the undecidability proof of Wang's tiling problem. {\it citation}
+but needed for example for formalising the undecidability proof of
+Wang's tiling problem \cite{Robinson71}.
%We are not aware of any other
%formalisation of a substantial undecidability problem.
*}
@@ -266,6 +268,7 @@
\draw[fill] (1.35,0.1) rectangle (1.65,0.4);
\draw[fill] (0.85,0.1) rectangle (1.15,0.4);
\draw[fill] (-0.35,0.1) rectangle (-0.65,0.4);
+ \draw[fill] (-1.65,0.1) rectangle (-1.35,0.4);
\draw (-0.25,0.8) -- (-0.25,-0.8);
\draw[<->] (-1.25,-0.7) -- (0.75,-0.7);
\node [anchor=base] at (-0.8,-0.5) {\small left list};
@@ -522,7 +525,9 @@
\caption{Copy machine}\label{copy}
\end{figure}
- {\it tapes in standard form}
+ {\it
+ As in \cite{Boolos87} we often need to restrict tapes to be in standard
+ form.}
Before we can prove the undecidability of the halting problem for our
Turing machines, we need to analyse two concrete Turing machine
@@ -530,7 +535,7 @@
``doing what they are supposed to be doing''. Such correctness proofs are usually left
out in the informal literature, for example \cite{Boolos87}. One program
we need to prove correct is the @{term dither} program shown in \eqref{dither}
- and the other program is @{term "tcopy"} is defined as
+ and the other program is @{term "tcopy"} defined as
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
@@ -554,7 +559,7 @@
\begin{center}
\begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}
\begin{tabular}[t]{@ {}l@ {}}
- @{thm (lhs) Hoare_halt_def} @{text "\<equiv>"}\\[1mm]
+ \colorbox{mygrey}{@{thm (lhs) Hoare_halt_def}} @{text "\<equiv>"}\\[1mm]
\hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\
\hspace{7mm}if @{term "P (l, r)"} holds then\\
\hspace{7mm}@{text "\<exists>"} @{term n}. such that\\
@@ -562,7 +567,7 @@
\hspace{7mm}@{text "Q holds_for (steps (1, (l, r)) p n)"}
\end{tabular} &
\begin{tabular}[t]{@ {}l@ {}}
- @{thm (lhs) Hoare_unhalt_def} @{text "\<equiv>"}\\[1mm]
+ \colorbox{mygrey}{@{thm (lhs) Hoare_unhalt_def}} @{text "\<equiv>"}\\[1mm]
\hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\
\hspace{7mm}if @{term "P (l, r)"} holds then\\
\hspace{7mm}@{text "\<forall>"} @{term n}. @{text "\<not> is_final (steps (1, (l, r)) p n)"}
@@ -577,9 +582,57 @@
more uniformly (only using Hoare-triples), we prefer our definitions because
we can derive simple Hoare-rules for sequentially composed Turing programs.
In this way we can reason about the correctness of @{term "tcopy_init"},
- for example, completely separately from @{term "tcopy_loop"}.
+ for example, completely separately from @{term "tcopy_loop"} and @{term "tcopy_end"}.
- It is rather straightforward to prove that the Turing program
+ \begin{center}
+ \begin{tabular}{lcl}
+ \multicolumn{1}{c}{start tape}\\
+ \begin{tikzpicture}
+ \draw[very thick] (-2,0) -- ( 0.75,0);
+ \draw[very thick] (-2,0.5) -- ( 0.75,0.5);
+ \draw[very thick] (-0.25,0) -- (-0.25,0.5);
+ \draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
+ \draw[very thick] (-0.75,0) -- (-0.75,0.5);
+ \draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
+ \draw[very thick] (-1.25,0) -- (-1.25,0.5);
+ \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
+ \draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
+ \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
+ \node [anchor=base] at (-1.7,0.2) {\ldots};
+ \end{tikzpicture}
+ & \raisebox{2.5mm}{$\;\;\large\Rightarrow\;\;$} &
+ \begin{tikzpicture}
+ \draw[very thick] (-2,0) -- ( 0.75,0);
+ \draw[very thick] (-2,0.5) -- ( 0.75,0.5);
+ \draw[very thick] (-0.25,0) -- (-0.25,0.5);
+ \draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
+ \draw[very thick] (-0.75,0) -- (-0.75,0.5);
+ \draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
+ \draw[very thick] (-1.25,0) -- (-1.25,0.5);
+ \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
+ \draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
+ \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
+ \node [anchor=base] at (-1.7,0.2) {\ldots};
+ \end{tikzpicture}\\
+
+ \begin{tikzpicture}
+ \draw[very thick] (-2,0) -- ( 0.25,0);
+ \draw[very thick] (-2,0.5) -- ( 0.25,0.5);
+ \draw[very thick] (-0.25,0) -- (-0.25,0.5);
+ \draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
+ \draw[very thick] (-0.75,0) -- (-0.75,0.5);
+ \draw[very thick] (-1.25,0) -- (-1.25,0.5);
+ \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
+ \draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
+ \node [anchor=base] at (-1.7,0.2) {\ldots};
+ \end{tikzpicture}
+ & \raisebox{2.5mm}{$\;\;\large\Rightarrow\;\;$} &
+ \raisebox{2.5mm}{loops}
+ \end{tabular}
+ \end{center}
+
+
+ It is straightforward to prove that the Turing program
@{term "dither"} satisfies the following correctness properties
\begin{center}