# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1360213975 0
# Node ID 1834acc6fd76e8c1cd34028b6162ecfd41037a06
# Parent  9b9e0d37fc19cba507da2584e044db09b579c7df
updated paper

diff -r 9b9e0d37fc19 -r 1834acc6fd76 Paper/Paper.thy
--- 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}. 
+  
 *}
 
 (*
diff -r 9b9e0d37fc19 -r 1834acc6fd76 paper.pdf
Binary file paper.pdf has changed