Paper/Paper.thy
changeset 150 3c504ca0ce95
parent 149 199cf7ce1169
child 151 0941e450e8c2
equal deleted inserted replaced
149:199cf7ce1169 150:3c504ca0ce95
  1369 
  1369 
  1370   Analysing the universal Turing machine constructed in \cite{Boolos87} more carefully
  1370   Analysing the universal Turing machine constructed in \cite{Boolos87} more carefully
  1371   we can strengthen this result slightly by observing that @{text m} is at most
  1371   we can strengthen this result slightly by observing that @{text m} is at most
  1372   2 in the output tape. This observation allows one to construct a UTM that works
  1372   2 in the output tape. This observation allows one to construct a UTM that works
  1373   entirely on the left-tape by composing it with a machine that drags the tape
  1373   entirely on the left-tape by composing it with a machine that drags the tape
  1374   two cells to the right. A corolary is that one-sided Turing machines (where the
  1374   two cells to the right. A corollary is that one-sided Turing machines (where the
  1375   tape only extends to the right) are as powerful as our two-sided Turing machines. 
  1375   tape only extends to the right) are computationally as powerful as our two-sided 
  1376 
  1376   Turing machines. So our undecidability proof for the halting problem extends
  1377   While formalising the chapter about universal Turing machines in \cite{Boolos87}
  1377   also to one-sided Turing machines, which is needed for example in order to
       
  1378   formalise the undecidability of Wang's tiling problem \cite{Robinson71}.
       
  1379 
       
  1380   While formalising the chapter about universal Turing machines in \cite{Boolos87},
  1378   we noticed that they use their definition about what function Turing machines
  1381   we noticed that they use their definition about what function Turing machines
  1379   calculate. They write in Chapter 3 \cite[Page 32]{Boolos87}:
  1382   calculate. They write in Chapter 3 \cite[Page 32]{Boolos87}:
  1380 
  1383 
  1381   \begin{quote}\it
  1384   \begin{quote}\it
  1382   ``If the function that is to be computed assigns no value to the arguments that 
  1385   ``If the function that is to be computed assigns no value to the arguments that