tm: comparison Paper/Paper.thy

equal deleted inserted replaced

-:9b9e0d37fc19
+:1834acc6fd76
 Turing machines, an unexpected outcome of our work is that we
 identified an inconsistency in their use of a definition. This is
 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
+they compute a partial arithmetic function.  The inconsitency arises
-when they define when this function should \emph{not} return a
+when they define the case when this function should \emph{not} return a
-result. They write in Chapter 3 \cite[Page 32]{Boolos87}:
+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
 are represented initially on the tape, then the machine either will never halt,
 or will halt in some nonstandard configuration\ldots''
 \end{quote}
 \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}
 @{text "stdh(m, x, t) \<equiv> stat(conf(m, x, t)) + nstd(conf(m, x, t))"}
 \end{equation}
 \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 $+$
+something that is not zero, then @{text "stdh(m, x, t)"} will be not zero, because of
-operation. One the same page, a function @{text "halt(m, x)"} is defined
+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
+that there exist Turing machines that given some arguments do not compute a value
-according to Chapter 3, but returns a proper result according to
+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,
 %then the TM will either loop {\bf or} stop with a non-standard tape
 %SO the following TM calculates something according to def from chap 8,
 %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}.
 *}
 (*
 section {* XYZ *}

changeset 155	1834acc6fd76
parent 154	9b9e0d37fc19
child 156	7c9dbacc6c7c