--- a/Paper/Paper.thy Thu Feb 07 03:40:23 2013 +0000
+++ b/Paper/Paper.thy Thu Feb 07 04:28:00 2013 +0000
@@ -328,15 +328,16 @@
universal Turing machine from \cite{Boolos87} by translating recursive
functions to abacus machines and abacus machines to Turing
machines. When formalising the universal Turing machine,
-we stumbled upon an inconsistence use of the definition of
-what function a Turing machine calculates. Since we have set up in
-Isabelle/HOL a very general computability model and undecidability
-result, we are able to formalise other results: we describe a proof of
-the computational equivalence of single-sided Turing machines, which
-is not given in \cite{Boolos87}, but needed for example for
-formalising the undecidability proof of Wang's tiling problem
-\cite{Robinson71}. %We are not aware of any other %formalisation of a
-substantial undecidability problem.
+we stumbled upon an inconsistent use of the definition of
+what function a Turing machine calculates.
+%Since we have set up in
+%Isabelle/HOL a very general computability model and undecidability
+%result, we are able to formalise other results: we describe a proof of
+%the computational equivalence of single-sided Turing machines, which
+%is not given in \cite{Boolos87}, but needed for example for
+%formalising the undecidability proof of Wang's tiling problem
+%\cite{Robinson71}. %We are not aware of any other %formalisation of a
+%substantial undecidability problem.
*}
section {* Turing Machines *}
@@ -1310,10 +1311,10 @@
for a list of recursive functions. Since we know in each case
the arity, say @{term l}, we can define an inductive evaluation relation that
relates a recursive function @{text r} and a list @{term ns} of natural numbers of length @{text l},
- to what the result of the recursive function is, say @{text n}---we omit the straightforward
+ to what the result of the recursive function is, say @{text n}. We omit the
definition of @{term "rec_calc_rel r ns n"}. Because of space reasons, we also omit the
definition of translating
- recursive functions into abacus programs. We can prove the following
+ recursive functions into abacus programs. We can prove, however, the following
theorem about the translation: If
@{thm (prem 1) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and r="n"]}
holds for the recursive function @{text r}, then the following Hoare-triple holds
@@ -1323,17 +1324,17 @@
\end{center}
\noindent
- for the Turing machine. This
+ for the translated Turing machine @{term "translate r"}. This
means that if the recursive function @{text r} with arguments @{text ns} evaluates
- to @{text n}, then the corresponding Turing machine @{term "tm_of_rec r"} if started
+ to @{text n}, then the translated Turing machine if started
with the standard tape @{term "([Bk, Bk], <ns::nat list>)"} will terminate
with the standard tape @{term "(Bk \<up> k, <n::nat> @ Bk \<up> l)"} for some @{text k} and @{text l}.
Having recursive functions under our belt, we can construct an universal
- function and consider the translated (universal) Turing machine @{term UTM}.
+ function and consider its translated (universal) Turing machine, written @{term UTM}.
Suppose
- a Turing program is well-formed and @{term p} when started with the standard
- tape containing the arguments @{term arg}, produces a standard tape
+ a Turing program @{term p} is well-formed and when started with the standard
+ tape containing the arguments @{term args}, will produce a standard tape
with ``output'' @{term n}. This assumption can be written as the
Hoare-triple
@@ -1342,9 +1343,9 @@
\end{center}
\noindent
- where we assume the @{term args} are non-empty, then the universal Turing
+ where we assume the @{term args} stand for a non-empty list. Then the universal Turing
machine @{term UTM} started with the code of @{term p} and the arguments
- @{term args} calculates the same result:
+ @{term args} calculates the same result, namely
\begin{center}
@{thm (concl) UTM_halt_lemma2}
@@ -1367,19 +1368,24 @@
@{thm (concl) UTM_unhalt_lemma2}
\end{center}
- Analysing the universal Turing machine constructed in \cite{Boolos87} more carefully
- we can strengthen this result slightly by observing that @{text m} is at most
- 2 in the output tape. This observation allows one to construct a universal Turing machine that works
- entirely on the left-tape by composing it with a machine that drags the tape
- two cells to the right. A corollary is that one-sided Turing machines (where the
- tape only extends to the right) are computationally as powerful as our two-sided
- Turing machines. So our undecidability proof for the halting problem extends
- also to one-sided Turing machines, which is needed for example in order to
- formalise the undecidability of Wang's tiling problem \cite{Robinson71}.
+ %Analysing the universal Turing machine constructed in \cite{Boolos87} more carefully
+ %we can strengthen this result slightly by observing that @{text m} is at most
+ %2 in the output tape. This observation allows one to construct a universal Turing machine that works
+ %entirely on the left-tape by composing it with a machine that drags the tape
+ %two cells to the right. A corollary is that one-sided Turing machines (where the
+ %tape only extends to the right) are computationally as powerful as our two-sided
+ %Turing machines. So our undecidability proof for the halting problem extends
+ %also to one-sided Turing machines, which is needed for example in order to
+ %formalise the undecidability of Wang's tiling problem \cite{Robinson71}.
- While formalising the chapter about universal Turing machines in \cite{Boolos87},
- we noticed that they use their definition about what function Turing machines
- calculate. They write in Chapter 3 \cite[Page 32]{Boolos87}:
+ While formalising the chapter in \cite{Boolos87} about universal Turing machines, an
+ unexpected outcome is that we identified an inconsistency in
+ their use of a definition. It is unexpected since it is a classic textbook which has
+ undergone several editions. The main idea is that every Turing machine started with
+ a standard tape computes 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}:
\begin{quote}\it
``If the function that is to be computed assigns no value to the arguments that
@@ -1388,25 +1394,45 @@
\end{quote}
\noindent
- Interestingly, they do not implement this definition when considering
- their universal Turing machine.
-
- 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
+ Interestingly, they do not implement this definition when constructing
+ their universal Turing machine. 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}
+ 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
+ in terms of @{text stdh} for computing the steps the Turing machine needs to
+ execute before it halts. 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
+ the definition in Chapter 8. One such Turing machine is:
- But in the definition of the universal function the TMs will never stop
- with non-standard tapes.
+ %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:
+ %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::nat)), (L, 2), (R, 2), (R, 0)]"}
\end{center}
+ \noindent
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
+ 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.
*}
(*