tm: comparison Paper/Paper.thy

equal deleted inserted replaced

-:0941e450e8c2
+:2c0d79801e36
 left out in the informal literature.  For reasoning about Turing
 machine programs we derive Hoare-rules.  We also construct the
 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
+we stumbled upon an inconsistent use of the definition of
-what function a Turing machine calculates. Since we have set up in
+what function a Turing machine calculates.
-Isabelle/HOL a very general computability model and undecidability
+%Since we have set up in
-result, we are able to formalise other results: we describe a proof of
+%Isabelle/HOL a very general computability model and undecidability
-the computational equivalence of single-sided Turing machines, which
+%result, we are able to formalise other results: we describe a proof of
-is not given in \cite{Boolos87}, but needed for example for
+%the computational equivalence of single-sided Turing machines, which
-formalising the undecidability proof of Wang's tiling problem
+%is not given in \cite{Boolos87}, but needed for example for
-\cite{Robinson71}.  %We are not aware of any other %formalisation of a
+%formalising the undecidability proof of Wang's tiling problem
-substantial undecidability problem.
+%\cite{Robinson71}.  %We are not aware of any other %formalisation of a
+%substantial undecidability problem.
 *}
 section {* Turing Machines *}
 text {* \noindent
 where @{text n} indicates the function expects @{term n} arguments
 (@{text z} and @{term s} expect one argument), and @{text rs} stands
 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
 \begin{center}
 @{thm (concl) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and r="n"]}
 \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
+a Turing program @{term p} is well-formed and  when started with the standard
-tape containing the arguments @{term arg}, produces a standard tape
+tape containing the arguments @{term args}, will produce a standard tape
 with ``output'' @{term n}. This assumption can be written as the
 Hoare-triple
 \begin{center}
 @{thm (prem 3) UTM_halt_lemma2}
 \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}
 \end{center}
 \begin{center}
 @{thm (concl) UTM_unhalt_lemma2}
 \end{center}
-Analysing the universal Turing machine constructed in \cite{Boolos87} more carefully
+%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
+%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
+%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
+%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
+%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
+%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
+%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
+%also to one-sided Turing machines, which is needed for example in order to
-formalise the undecidability of Wang's tiling problem \cite{Robinson71}.
+%formalise the undecidability of Wang's tiling problem \cite{Robinson71}.
-While formalising the chapter about universal Turing machines in \cite{Boolos87},
+While formalising the chapter in  \cite{Boolos87} about universal Turing machines, an
-we noticed that they use their definition about what function Turing machines
+unexpected outcome is that we identified an inconsistency in
-calculate. They write in Chapter 3 \cite[Page 32]{Boolos87}:
+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
 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 considering
+Interestingly, they do not implement this definition when constructing
-their universal Turing machine.
+their universal Turing machine. On page 93, a recursive function
+@{term stdh} is defined as:
-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
+\begin{equation}\label{stdh_def}
+@{text "stdh(m, x, t) \<equiv> stat(conf(m, x, t)) + nstd(conf(m, x, t))"}
-But in the definition of the universal function the TMs will never stop
+\end{equation}
-with non-standard tapes.
-SO the following TM calculates something according to def from chap 8,
-but not with chap 3. For example:
+\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:
+%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::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;
+non-standard tape @{term "([Oc], [])"} according to the definition in Chapter 3---so no
-but with @{term "([], [Oc])"} according to def Chap 8
+result is calculated; but with the standard tape @{term "([], [Oc])"} according to def Chapter 8.
 *}
 (*
 section {* XYZ *}

changeset 152	2c0d79801e36
parent 151	0941e450e8c2
child 153	a4601143db90