--- a/Paper/Paper.thy Fri Jan 25 15:57:58 2013 +0100
+++ b/Paper/Paper.thy Fri Jan 25 21:15:09 2013 +0000
@@ -27,6 +27,7 @@
tcopy_end ("copy\<^bsub>end\<^esub>") and
step0 ("step") and
steps0 ("steps") and
+ exponent ("_\<^bsup>_\<^esup>") and
(* abc_lm_v ("lookup") and
abc_lm_s ("set") and*)
haltP ("stdhalt") and
@@ -247,10 +248,12 @@
constructors, namely @{text Bk} and @{text Oc}. One way to
represent such tapes is to use a pair of lists, written @{term "(l,
r)"}, where @{term l} stands for the tape on the left-hand side of
- the head and @{term r} for the tape on the right-hand side. We have
- the convention that the head, abbreviated @{term hd}, of the
- right-list is the cell on which the head of the Turing machine
- currently scannes. This can be pictured as follows:
+ the head and @{term r} for the tape on the right-hand side. We use
+ the notation @{term "Bk \<up> n"} (similarly @{term "Oc \<up> n"}) for lists
+ composed of @{term n} elements of @{term Bk}. We also have the
+ convention that the head, abbreviated @{term hd}, of the right-list
+ is the cell on which the head of the Turing machine currently
+ scannes. This can be pictured as follows:
%
\begin{center}
\begin{tikzpicture}
@@ -304,7 +307,7 @@
We slightly deviate
from the presentation in \cite{Boolos87} by using the @{term Nop} operation; however its use
will become important when we formalise halting computations and also universal Turing
- machines. Given a tape and an action, we can define the
+ machines. Given a tape and an action, we can define the
following tape updating function:
\begin{center}
@@ -361,7 +364,7 @@
%cannot be used as it does not preserve types.} This renaming can be
%quite cumbersome to reason about.
We follow the choice made in \cite{AspertiRicciotti12}
- representing a state by a natural number and the states in a Turing
+ by representing a state with a natural number and the states in a Turing
machine program by the initial segment of natural numbers starting from @{text 0}.
In doing so we can compose two Turing machine programs by
shifting the states of one by an appropriate amount to a higher
@@ -371,7 +374,7 @@
an action and a natural number (the next state). A \emph{program} @{term p} of a Turing
machine is then a list of such pairs. Using as an example the following Turing machine
program, which consists of four instructions
-
+ %
\begin{equation}
\begin{tikzpicture}
\node [anchor=base] at (0,0) {@{thm dither_def}};
@@ -385,7 +388,7 @@
\end{tikzpicture}
\label{dither}
\end{equation}
-
+ %
\noindent
the reader can see we have organised our Turing machine programs so
that segments of two belong to a state. The first component of such a
@@ -401,8 +404,8 @@
\cite{AspertiRicciotti12}, we have chosen a very concrete
representation for programs, because when constructing a universal
Turing machine, we need to define a coding function for programs.
- This can be easily done for our programs-as-lists, but is more
- difficult for the functions used by Asperti and Ricciotti.
+ This can be directly done for our programs-as-lists, but is
+ slightly more difficult for the functions used by Asperti and Ricciotti.
Given a program @{term p}, a state
and the cell being read by the head, we need to fetch
@@ -525,9 +528,21 @@
\caption{Copy machine}\label{copy}
\end{figure}
- {\it
- As in \cite{Boolos87} we often need to restrict tapes to be in standard
- form.}
+ We often need to restrict tapes to be in \emph{standard form}, which means
+ the left list of the tape is either empty or only contains @{text "Bk"}s, and
+ the right list contains some ``clusters'' of @{text "Oc"}s separted by single
+ blanks and can be followed by some blanks. To make this formal we define the
+ following function
+
+ \begin{center}
+ foo
+ \end{center}
+
+ \noindent
+ A standard tape is then of the form @{text "(Bk\<^isup>k,\<langle>n\<^isub>1,...,n\<^isub>m\<rangle> @ Bk\<^isup>l)"} for some @{text k},
+ @{text l} and @{text "n\<^isub>i"}. Note that the head in a standard tape ``points'' to the
+ leftmost @{term "Oc"} on the tape.
+
Before we can prove the undecidability of the halting problem for our
Turing machines, we need to analyse two concrete Turing machine
@@ -549,7 +564,7 @@
notion of total correctness defined in terms of
\emph{Hoare-triples}, written @{term "{P} p {Q}"}. They realise the
idea that a program @{term p} started in state @{term "1::nat"} with
- a tape satisfying @{term P} will after @{text n} steps halt (have
+ a tape satisfying @{term P} will after some @{text n} steps halt (have
transitioned into the halting state) with a tape satisfying @{term
Q}. We also have \emph{Hoare-pairs} of the form @{term "{P} p \<up>"}
realising the case that a program @{term p} started with a tape
@@ -577,7 +592,7 @@
\noindent
We have set up our Hoare-style reasoning so that we can deal explicitly
- with looping and total correctness, rather than have notions for partial
+ with total correctness and non-terminantion, rather than have notions for partial
correctness and termination. Although the latter would allow us to reason
more uniformly (only using Hoare-triples), we prefer our definitions because
we can derive simple Hoare-rules for sequentially composed Turing programs.
@@ -585,8 +600,9 @@
for example, completely separately from @{term "tcopy_loop"} and @{term "tcopy_end"}.
\begin{center}
- \begin{tabular}{lcl}
- \multicolumn{1}{c}{start tape}\\
+ \begin{tabular}{l@ {\hspace{3mm}}lcl}
+ & \multicolumn{1}{c}{start tape}\\[1mm]
+ \raisebox{2.5mm}{halting case:} &
\begin{tikzpicture}
\draw[very thick] (-2,0) -- ( 0.75,0);
\draw[very thick] (-2,0.5) -- ( 0.75,0.5);
@@ -615,7 +631,8 @@
\node [anchor=base] at (-1.7,0.2) {\ldots};
\end{tikzpicture}\\
- \begin{tikzpicture}
+ \raisebox{2.5mm}{non-halting case:} &
+ \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);