180 Turing machine. They report that the informal proofs from which they |
180 Turing machine. They report that the informal proofs from which they |
181 started are \emph{not} ``sufficiently accurate to be directly usable as a |
181 started are \emph{not} ``sufficiently accurate to be directly usable as a |
182 guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For |
182 guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For |
183 our formalisation we follow mainly the proofs from the textbook |
183 our formalisation we follow mainly the proofs from the textbook |
184 \cite{Boolos87} and found that the description there is quite |
184 \cite{Boolos87} and found that the description there is quite |
185 detailed. Some details are left out however: for example, it is only |
185 detailed. Some details are left out however: for example, constructing |
186 shown how the universal Turing machine is constructed for Turing |
186 the \emph{copy Turing program} is left as an excerise; also the |
|
187 book only shows how the universal Turing machine is constructed for Turing |
187 machines computing unary functions. We had to figure out a way to |
188 machines computing unary functions. We had to figure out a way to |
188 generalise this result to $n$-ary functions. Similarly, when compiling |
189 generalise this result to $n$-ary functions. Similarly, when compiling |
189 recursive functions to abacus machines, the textbook again only shows |
190 recursive functions to abacus machines, the textbook again only shows |
190 how it can be done for 2- and 3-ary functions, but in the |
191 how it can be done for 2- and 3-ary functions, but in the |
191 formalisation we need arbitrary functions. But the general ideas for |
192 formalisation we need arbitrary functions. But the general ideas for |
255 constructors, namely @{text Bk} and @{text Oc}. One way to |
256 constructors, namely @{text Bk} and @{text Oc}. One way to |
256 represent such tapes is to use a pair of lists, written @{term "(l, |
257 represent such tapes is to use a pair of lists, written @{term "(l, |
257 r)"}, where @{term l} stands for the tape on the left-hand side of |
258 r)"}, where @{term l} stands for the tape on the left-hand side of |
258 the head and @{term r} for the tape on the right-hand side. We use |
259 the head and @{term r} for the tape on the right-hand side. We use |
259 the notation @{term "Bk \<up> n"} (similarly @{term "Oc \<up> n"}) for lists |
260 the notation @{term "Bk \<up> n"} (similarly @{term "Oc \<up> n"}) for lists |
260 composed of @{term n} elements of @{term Bk}. We also have the |
261 composed of @{term n} elements of @{term Bk}s. We also have the |
261 convention that the head, abbreviated @{term hd}, of the right-list |
262 convention that the head, abbreviated @{term hd}, of the right-list |
262 is the cell on which the head of the Turing machine currently |
263 is the cell on which the head of the Turing machine currently |
263 scannes. This can be pictured as follows: |
264 scannes. This can be pictured as follows: |
264 % |
265 % |
265 \begin{center} |
266 \begin{center} |
550 |
551 |
551 \begin{tikzpicture}[scale=0.7] |
552 \begin{tikzpicture}[scale=0.7] |
552 \node [anchor=base] at (2.2,0.1) {\small$\Rightarrow$}; |
553 \node [anchor=base] at (2.2,0.1) {\small$\Rightarrow$}; |
553 \node [anchor=base] at (5.6,0.1) {\small$\Rightarrow$}; |
554 \node [anchor=base] at (5.6,0.1) {\small$\Rightarrow$}; |
554 \node [anchor=base] at (10.5,0.1) {\small$\Rightarrow$}; |
555 \node [anchor=base] at (10.5,0.1) {\small$\Rightarrow$}; |
555 \node [anchor=base] at (2.2,-0.5) {\small@{term "tcopy_init"}}; |
556 \node [anchor=base] at (2.2,-0.6) {\small$\overbrace{@{term "tcopy_init"}}^{}$}; |
556 \node [anchor=base] at (5.6,-0.5) {\small@{term "tcopy_loop"}}; |
557 \node [anchor=base] at (5.6,-0.6) {\small$\overbrace{@{term "tcopy_loop"}}^{}$}; |
557 \node [anchor=base] at (10.5,-0.5) {\small@{term "tcopy_end"}}; |
558 \node [anchor=base] at (10.5,-0.6) {\small$\overbrace{@{term "tcopy_end"}}^{}$}; |
558 |
559 |
559 |
560 |
560 \begin{scope}[shift={(0.5,0)}] |
561 \begin{scope}[shift={(0.5,0)}] |
561 \draw[very thick] (-0.25,0) -- ( 1.25,0); |
562 \draw[very thick] (-0.25,0) -- ( 1.25,0); |
562 \draw[very thick] (-0.25,0.5) -- ( 1.25,0.5); |
563 \draw[very thick] (-0.25,0.5) -- ( 1.25,0.5); |
626 \draw[fill] ( 0.85,0.1) rectangle (1.15,0.4); |
627 \draw[fill] ( 0.85,0.1) rectangle (1.15,0.4); |
627 \end{scope} |
628 \end{scope} |
628 \end{tikzpicture}\\[-8mm]\mbox{} |
629 \end{tikzpicture}\\[-8mm]\mbox{} |
629 \end{center} |
630 \end{center} |
630 \caption{The components of the \emph{copy Turing machine} (above). If started |
631 \caption{The components of the \emph{copy Turing machine} (above). If started |
631 with the tape @{term "([], <[(3::nat)]>)"} the first machine adds @{term "[Bk, Oc]"} at |
632 with the tape @{term "([], <[(2::nat)]>)"} the first machine adds @{term "[Bk, Oc]"} at |
632 the end of the right tape; the second then ``moves'' all @{term Oc}s except the |
633 the end of the right tape; the second then ``moves'' all @{term Oc}s except the |
633 first from the beginning of the tape to the end; the third ``refills'' the original |
634 first from the beginning of the tape to the end; the third ``refills'' the original |
634 block of @{term "Oc"}s. The result is the tape @{term "([Bk], <[(3::nat, 3::nat)]>)"}.} |
635 block of @{term "Oc"}s. The result is the tape @{term "([Bk], <[(2::nat, 2::nat)]>)"}.} |
635 \label{copy} |
636 \label{copy} |
636 \end{figure} |
637 \end{figure} |
637 |
638 |
638 |
639 |
639 We often need to restrict tapes to be in \emph{standard form}, which means |
640 We often need to restrict tapes to be in \emph{standard form}, which means |