--- a/Paper/Paper.thy Thu Feb 07 04:56:01 2013 +0000
+++ b/Paper/Paper.thy Thu Feb 07 05:12:55 2013 +0000
@@ -1398,9 +1398,9 @@
unexpected since \cite{Boolos87} is a classic textbook which has
undergone several editions (we used the fifth edition). The central
idea about Turing machines is that when started with standard tapes
- they compute a partial arithmetic function. The inconsitency is
- when they define when this function should \emph{not} return a
- result. They write in Chapter 3 \cite[Page 32]{Boolos87}:
+ they compute a partial arithmetic function. The inconsitency arises
+ when they define the case when this function should \emph{not} return a
+ result. They write in Chapter 3, Page 32:
\begin{quote}\it
``If the function that is to be computed assigns no value to the arguments that
@@ -1410,7 +1410,7 @@
\noindent
Interestingly, they do not implement this definition when constructing
- their universal Turing machine. On page 93, a recursive function
+ their universal Turing machine. In Chapter 8, on page 93, a recursive function
@{term stdh} is defined as:
\begin{equation}\label{stdh_def}
@@ -1419,16 +1419,16 @@
\noindent
where @{text "stat(conf(m, x, t))"} computes the current state of the
- simulated Turing machine, and the @{text "nstd(conf(m, x, t))"} returns @{text 1}
+ simulated Turing machine, and @{text "nstd(conf(m, x, t))"} returns @{text 1}
if the tape content is non-standard. If either one evaluates to
- nonzero, then @{text "stdh(m, x, t)"} will be nonzero, because of the $+$
- operation. One the same page, a function @{text "halt(m, x)"} is defined
+ something that is not zero, then @{text "stdh(m, x, t)"} will be not zero, because of
+ the $+$-operation. One the same page, a function @{text "halt(m, x)"} is defined
in terms of @{text stdh} for computing the steps the Turing machine needs to
- execute before it halts. According to this definition, the simulated
+ execute before it halts (in case it halts at all). According to this definition, the simulated
Turing machine will continue to run after entering the @{text 0}-state
with a non-standard tape. The consequence of this inconsistency is
- that there exists Turing machines that compute non-values
- according to Chapter 3, but returns a proper result according to
+ that there exist Turing machines that given some arguments do not compute a value
+ according to Chapter 3, but return a proper result according to
the definition in Chapter 8. One such Turing machine is:
%This means that if you encode the plus function but only give one argument,
@@ -1441,13 +1441,17 @@
%but not with chap 3. For example:
\begin{center}
- @{term "[(L, (0::nat)), (L, 2), (R, 2), (R, 0)]"}
+ @{term "counter_example \<equiv> [(L, (0::nat)), (L, 2), (R, 2), (R, 0)]"}
\end{center}
\noindent
- If started with @{term "([], [Oc])"} it halts with the
+ If started with standard tape @{term "([], [Oc])"}, it halts with the
non-standard tape @{term "([Oc], [])"} according to the definition in Chapter 3---so no
- result is calculated; but with the standard tape @{term "([], [Oc])"} according to def Chapter 8.
+ result is calculated; but with the standard tape @{term "([], [Oc])"} according to the
+ definition in Chapter 8. We solve this inconsitency in our formalisation by
+ setting up our definitions so that the @{text counter_example} Turing machine does not
+ produce any result, but loops forever fetching @{term Nop}s in state @{text 0}.
+
*}
(*