Paper/Paper.thy
changeset 154 9b9e0d37fc19
parent 153 a4601143db90
child 155 1834acc6fd76
equal deleted inserted replaced
153:a4601143db90 154:9b9e0d37fc19
  1390   %tape only extends to the right) are computationally as powerful as our two-sided 
  1390   %tape only extends to the right) are computationally as powerful as our two-sided 
  1391   %Turing machines. So our undecidability proof for the halting problem extends
  1391   %Turing machines. So our undecidability proof for the halting problem extends
  1392   %also to one-sided Turing machines, which is needed for example in order to
  1392   %also to one-sided Turing machines, which is needed for example in order to
  1393   %formalise the undecidability of Wang's tiling problem \cite{Robinson71}.
  1393   %formalise the undecidability of Wang's tiling problem \cite{Robinson71}.
  1394 
  1394 
  1395   While formalising the chapter in  \cite{Boolos87} about universal Turing machines, an
  1395   While formalising the chapter in \cite{Boolos87} about universal
  1396   unexpected outcome is that we identified an inconsistency in
  1396   Turing machines, an unexpected outcome of our work is that we
  1397   their use of a definition. It is unexpected since it is a classic textbook which has
  1397   identified an inconsistency in their use of a definition. This is
  1398   undergone several editions. The main idea is that every Turing machine started with
  1398   unexpected since \cite{Boolos87} is a classic textbook which has
  1399   a standard tape computes a
  1399   undergone several editions (we used the fifth edition). The central
  1400   partial arithmetic function.  The inconsitency is when they define
  1400   idea about Turing machines is that when started with standard tapes
  1401   when this function should \emph{not} return a result. They write in Chapter
  1401   they compute a partial arithmetic function.  The inconsitency is
  1402   3 \cite[Page 32]{Boolos87}:
  1402   when they define when this function should \emph{not} return a
       
  1403   result. They write in Chapter 3 \cite[Page 32]{Boolos87}:
  1403 
  1404 
  1404   \begin{quote}\it
  1405   \begin{quote}\it
  1405   ``If the function that is to be computed assigns no value to the arguments that 
  1406   ``If the function that is to be computed assigns no value to the arguments that 
  1406   are represented initially on the tape, then the machine either will never halt, 
  1407   are represented initially on the tape, then the machine either will never halt, 
  1407   or will halt in some nonstandard configuration\ldots''
  1408   or will halt in some nonstandard configuration\ldots''