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, constructing |
185 detailed. Some details are left out however: for example, constructing |
186 the \emph{copy Turing program} is left as an excerise; also the |
186 the \emph{copy Turing program} is left as an excerise to the reader; also |
187 book only shows how the universal Turing machine is constructed for Turing |
187 \cite{Boolos87} only shows how the universal Turing machine is constructed for Turing |
188 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 |
189 generalise this result to $n$-ary functions. Similarly, when compiling |
189 generalise this result to $n$-ary functions. Similarly, when compiling |
190 recursive functions to abacus machines, the textbook again only shows |
190 recursive functions to abacus machines, the textbook again only shows |
191 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 |
192 formalisation we need arbitrary functions. But the general ideas for |
192 formalisation we need arbitrary functions. But the general ideas for |
257 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, |
258 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 |
259 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 |
260 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 |
261 composed of @{term n} elements of @{term Bk}s. We also have the |
261 composed of @{term n} elements of @{term Bk}s. We also have the |
262 convention that the head, abbreviated @{term hd}, of the right-list |
262 convention that the head, abbreviated @{term hd}, of the right list |
263 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 |
264 scannes. This can be pictured as follows: |
264 scannes. This can be pictured as follows: |
265 % |
265 % |
266 \begin{center} |
266 \begin{center} |
267 \begin{tikzpicture}[scale=0.9] |
267 \begin{tikzpicture}[scale=0.9] |
327 @{thm (lhs) update.simps(5)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(5)}\\ |
327 @{thm (lhs) update.simps(5)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(5)}\\ |
328 \end{tabular} |
328 \end{tabular} |
329 \end{center} |
329 \end{center} |
330 |
330 |
331 \noindent |
331 \noindent |
332 The first two clauses replace the head of the right-list |
332 The first two clauses replace the head of the right list |
333 with a new @{term Bk} or @{term Oc}, respectively. To see that |
333 with a new @{term Bk} or @{term Oc}, respectively. To see that |
334 these two clauses make sense in case where @{text r} is the empty |
334 these two clauses make sense in case where @{text r} is the empty |
335 list, one has to know that the tail function, @{term tl}, is defined |
335 list, one has to know that the tail function, @{term tl}, is defined |
336 such that @{term "tl [] == []"} holds. The third clause |
336 such that @{term "tl [] == []"} holds. The third clause |
337 implements the move of the head one step to the left: we need |
337 implements the move of the head one step to the left: we need |
338 to test if the left-list @{term l} is empty; if yes, then we just prepend a |
338 to test if the left-list @{term l} is empty; if yes, then we just prepend a |
339 blank cell to the right-list; otherwise we have to remove the |
339 blank cell to the right list; otherwise we have to remove the |
340 head from the left-list and prepend it to the right-list. Similarly |
340 head from the left-list and prepend it to the right list. Similarly |
341 in the fourth clause for a right move action. The @{term Nop} operation |
341 in the fourth clause for a right move action. The @{term Nop} operation |
342 leaves the the tape unchanged. |
342 leaves the the tape unchanged. |
343 |
343 |
344 %Note that our treatment of the tape is rather ``unsymmetric''---we |
344 %Note that our treatment of the tape is rather ``unsymmetric''---we |
345 %have the convention that the head of the right-list is where the |
345 %have the convention that the head of the right list is where the |
346 %head is currently positioned. Asperti and Ricciotti |
346 %head is currently positioned. Asperti and Ricciotti |
347 %\cite{AspertiRicciotti12} also considered such a representation, but |
347 %\cite{AspertiRicciotti12} also considered such a representation, but |
348 %dismiss it as it complicates their definition for \emph{tape |
348 %dismiss it as it complicates their definition for \emph{tape |
349 %equality}. The reason is that moving the head one step to |
349 %equality}. The reason is that moving the head one step to |
350 %the left and then back to the right might change the tape (in case |
350 %the left and then back to the right might change the tape (in case |
627 \draw[fill] ( 0.85,0.1) rectangle (1.15,0.4); |
627 \draw[fill] ( 0.85,0.1) rectangle (1.15,0.4); |
628 \end{scope} |
628 \end{scope} |
629 \end{tikzpicture}\\[-8mm]\mbox{} |
629 \end{tikzpicture}\\[-8mm]\mbox{} |
630 \end{center} |
630 \end{center} |
631 \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 |
632 with the tape @{term "([], <[(2::nat)]>)"} the first machine adds @{term "[Bk, Oc]"} at |
632 with the tape @{term "([], <[2::nat]>)"} the first machine appends @{term "[Bk, Oc]"} at |
633 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 |
634 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 |
635 block of @{term "Oc"}s. The result is the tape @{term "([Bk], <[(2::nat, 2::nat)]>)"}.} |
635 block of @{term "Oc"}s. The resulting tape is @{term "([Bk], <[2::nat, 2::nat]>)"}.} |
636 \label{copy} |
636 \label{copy} |
637 \end{figure} |
637 \end{figure} |
638 |
638 |
639 |
639 |
640 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 |