24 tm_wf0 ("wf") and |
24 tm_wf0 ("wf") and |
25 is_even ("iseven") and |
25 is_even ("iseven") and |
26 tcopy_init ("copy\<^bsub>begin\<^esub>") and |
26 tcopy_init ("copy\<^bsub>begin\<^esub>") and |
27 tcopy_loop ("copy\<^bsub>loop\<^esub>") and |
27 tcopy_loop ("copy\<^bsub>loop\<^esub>") and |
28 tcopy_end ("copy\<^bsub>end\<^esub>") and |
28 tcopy_end ("copy\<^bsub>end\<^esub>") and |
|
29 step0 ("step") and |
|
30 steps0 ("steps") and |
29 (* abc_lm_v ("lookup") and |
31 (* abc_lm_v ("lookup") and |
30 abc_lm_s ("set") and*) |
32 abc_lm_s ("set") and*) |
31 haltP ("stdhalt") and |
33 haltP ("stdhalt") and |
32 tcopy ("copy") and |
34 tcopy ("copy") and |
33 tape_of_nat_list ("\<ulcorner>_\<urcorner>") and |
35 tape_of_nat_list ("\<ulcorner>_\<urcorner>") and |
208 Turing machines---consequently if the Turing machines are simpler, then the coding |
210 Turing machines---consequently if the Turing machines are simpler, then the coding |
209 functions are simpler too. Unfortunately, the restrictiveness also makes |
211 functions are simpler too. Unfortunately, the restrictiveness also makes |
210 it harder to design programs for these Turing machines. In order |
212 it harder to design programs for these Turing machines. In order |
211 to construct a universal Turing machine we therefore do not follow |
213 to construct a universal Turing machine we therefore do not follow |
212 \cite{AspertiRicciotti12}, instead follow the proof in |
214 \cite{AspertiRicciotti12}, instead follow the proof in |
213 \cite{Boolos87} by relating abacus machines to Turing machines and in |
215 \cite{Boolos87} by translating abacus machines to Turing machines and in |
214 turn recursive functions to abacus machines. The universal Turing |
216 turn recursive functions to abacus machines. The universal Turing |
215 machine can then be constructed as a recursive function. |
217 machine can then be constructed as a recursive function. |
216 |
218 |
217 \smallskip |
219 \smallskip |
218 \noindent |
220 \noindent |
240 ``gliding'' over a potentially infinite tape. Boolos et |
242 ``gliding'' over a potentially infinite tape. Boolos et |
241 al~\cite{Boolos87} only consider tapes with cells being either blank |
243 al~\cite{Boolos87} only consider tapes with cells being either blank |
242 or occupied, which we represent by a datatype having two |
244 or occupied, which we represent by a datatype having two |
243 constructors, namely @{text Bk} and @{text Oc}. One way to |
245 constructors, namely @{text Bk} and @{text Oc}. One way to |
244 represent such tapes is to use a pair of lists, written @{term "(l, |
246 represent such tapes is to use a pair of lists, written @{term "(l, |
245 r)"}, where @{term l} stands for the tape on the left-hand side of the |
247 r)"}, where @{term l} stands for the tape on the left-hand side of |
246 head and @{term r} for the tape on the right-hand side. We have the |
248 the head and @{term r} for the tape on the right-hand side. We have |
247 convention that the head, abbreviated @{term hd}, of the right-list is |
249 the convention that the head, abbreviated @{term hd}, of the |
248 the cell on which the head of the Turing machine currently operates. This can |
250 right-list is the cell on which the head of the Turing machine |
249 be pictured as follows: |
251 currently scannes. This can be pictured as follows: |
250 % |
252 % |
251 \begin{center} |
253 \begin{center} |
252 \begin{tikzpicture} |
254 \begin{tikzpicture} |
253 \draw[very thick] (-3.0,0) -- ( 3.0,0); |
255 \draw[very thick] (-3.0,0) -- ( 3.0,0); |
254 \draw[very thick] (-3.0,0.5) -- ( 3.0,0.5); |
256 \draw[very thick] (-3.0,0.5) -- ( 3.0,0.5); |
425 \begin{center} |
427 \begin{center} |
426 @{thm tm_wf.simps[where p="p" and off="0::nat", simplified, THEN eq_reflection]} |
428 @{thm tm_wf.simps[where p="p" and off="0::nat", simplified, THEN eq_reflection]} |
427 \end{center} |
429 \end{center} |
428 |
430 |
429 \noindent |
431 \noindent |
430 The first says that @{text p} must have at least an instruction for the starting |
432 The first states that @{text p} must have at least an instruction for the starting |
431 state; the second that @{text p} has a @{term Bk} and @{term Oc} instruction for every |
433 state; the second that @{text p} has a @{term Bk} and @{term Oc} instruction for every |
432 state, and the third that every next-state is one of the states mentioned in |
434 state, and the third that every next-state is one of the states mentioned in |
433 the program or being the @{text 0}-state. |
435 the program or being the @{text 0}-state. |
434 |
436 |
435 We need to be able to sequentially compose Turing machine programs. Given our |
437 We need to be able to sequentially compose Turing machine programs. Given our |
522 |
524 |
523 Before we can prove the undecidability of the halting problem for |
525 Before we can prove the undecidability of the halting problem for |
524 Turing machines, we need to analyse two concrete Turing machine |
526 Turing machines, we need to analyse two concrete Turing machine |
525 programs and establish that they are correct, that is they are |
527 programs and establish that they are correct, that is they are |
526 ``doing what they are supposed to be doing''. This is usually left |
528 ``doing what they are supposed to be doing''. This is usually left |
527 out in the informal computability literature, for example |
529 out in the informal literature, for example \cite{Boolos87}. One program |
528 \cite{Boolos87}. One program we prove correct is the @{term dither} |
530 we prove correct is the @{term dither} program shown in \eqref{dither} |
529 program shown in \eqref{dither} and the other program @{term |
531 and the other program @{term "tcopy"} is defined as |
530 "tcopy"} is defined as |
|
531 |
532 |
532 \begin{center} |
533 \begin{center} |
533 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} |
534 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} |
534 @{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def} |
535 @{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def} |
535 \end{tabular} |
536 \end{tabular} |
536 \end{center} |
537 \end{center} |
537 |
538 |
538 \noindent |
539 \noindent |
539 whose three components are given in Figure~\ref{copy}. |
540 whose three components are given in Figure~\ref{copy}. |
|
541 |
|
542 |
|
543 |
|
544 |
|
545 |
540 To prove the correctness, we derive some Hoare-style reasoning rules for |
546 To prove the correctness, we derive some Hoare-style reasoning rules for |
541 Turing machine programs. A \emph{Hoare-triple} for a terminating Turing |
547 Turing machine programs. A \emph{Hoare-triple} for a terminating Turing |
542 machine program is defined as |
548 machine program is defined as |
543 |
549 |
544 \begin{center} |
550 \begin{center} |
545 @{thm Hoare_halt_def} |
551 @{thm Hoare_halt_def} |
546 \end{center} |
552 \end{center} |
547 |
553 |
|
554 A \emph{Hoare-pair} for a non-terminating Turing machine program is defined |
|
555 as |
|
556 |
548 \begin{center} |
557 \begin{center} |
549 @{thm Hoare_unhalt_def} |
558 @{thm Hoare_unhalt_def} |
550 \end{center} |
559 \end{center} |
|
560 |
|
561 |
|
562 |
551 |
563 |
552 In the following we will consider the following Turing machine program |
564 In the following we will consider the following Turing machine program |
553 that makes a copies a value on the tape. |
565 that makes a copies a value on the tape. |
554 |
566 |
555 |
567 |