# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1360129756 0
# Node ID f47f1ef313d105ace9df79332e9e529e2952f1d3
# Parent  ca7fb6848715e487bbd97a5fb81597a26aa5ec6d
updated

diff -r ca7fb6848715 -r f47f1ef313d1 Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Feb 06 04:39:08 2013 +0000
+++ b/Paper/Paper.thy	Wed Feb 06 05:49:16 2013 +0000
@@ -1326,7 +1326,32 @@
 
   and the also the definition of the
   universal function (we refer the reader to our formalisation).
+
+  \cite[Page 32]{Boolos87}
+
+  \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}
   
+  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
+
+  But in the definition of the universal function the TMs will never stop
+  with non-standard tapes. 
+
+  SO the following TM calculates something according to def from chap 8,
+  but not with chap 3. For example:
+  
+  \begin{center}
+  @{term "[(L, 0), (L, 2), (R, 2), (R, 0)]"}
+  \end{center}
+
+  If started with @{term "([], [Oc])"} it halts with the
+  non-standard tape @{term "([Oc], [])"} according to the definition in Chap 3;
+  but with @{term "([], [Oc])"} according to def Chap 8
+
 *}
 
 (*
diff -r ca7fb6848715 -r f47f1ef313d1 paper.pdf
Binary file paper.pdf has changed