# HG changeset patch # User Christian Urban # Date 1360211280 0 # Node ID 2c0d79801e3683cefdb34d3688f3a5fb44aa0b62 # Parent 0941e450e8c293f2d5d3615646ffcdaf22c9a102 updated paper diff -r 0941e450e8c2 -r 2c0d79801e36 Paper/Paper.thy --- 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], )"} will terminate with the standard tape @{term "(Bk \ k, @ Bk \ 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) \ 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. *} (* diff -r 0941e450e8c2 -r 2c0d79801e36 Paper/document/root.tex --- a/Paper/document/root.tex Thu Feb 07 03:40:23 2013 +0000 +++ b/Paper/document/root.tex Thu Feb 07 04:28:00 2013 +0000 @@ -59,8 +59,8 @@ recursive functions. We also formalise a universal Turing machine and Hoare-style reasoning techniques that allow us to reason about Turing machine programs. Our theory can be used to formalise other computability -results. We give one example about the computational equivalence of -single-sided Turing machines. +results. %We give one example about the computational equivalence of +%single-sided Turing machines. %{\it we give one example about the undecidability of Wang's tiling problem, whose proof uses %the notion of a universal Turing machine.} \end{abstract} diff -r 0941e450e8c2 -r 2c0d79801e36 paper.pdf Binary file paper.pdf has changed