Paper/Paper.thy
changeset 149 199cf7ce1169
parent 146 0f52b971cc03
child 150 3c504ca0ce95
equal deleted inserted replaced
148:6ffd6880dad7 149:199cf7ce1169
  1365 
  1365 
  1366   \begin{center}
  1366   \begin{center}
  1367   @{thm (concl) UTM_unhalt_lemma2} 
  1367   @{thm (concl) UTM_unhalt_lemma2} 
  1368   \end{center}
  1368   \end{center}
  1369 
  1369 
  1370   \noindent
  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
       
  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
       
  1374   two cells to the right. A corolary is that one-sided Turing machines (where the
       
  1375   tape only extends to the right) are as powerful as our two-sided Turing machines. 
       
  1376 
  1371   While formalising the chapter about universal Turing machines in \cite{Boolos87}
  1377   While formalising the chapter about universal Turing machines in \cite{Boolos87}
  1372   we noticed that they use their definition about what function Turing machines
  1378   we noticed that they use their definition about what function Turing machines
  1373   calculate. They write in Chapter 3 \cite[Page 32]{Boolos87}:
  1379   calculate. They write in Chapter 3 \cite[Page 32]{Boolos87}:
  1374 
  1380 
  1375   \begin{quote}\it
  1381   \begin{quote}\it