19 set ("") and |
19 set ("") and |
20 W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and |
20 W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and |
21 W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and |
21 W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and |
22 update2 ("update") and |
22 update2 ("update") and |
23 tm_wf0 ("wf") and |
23 tm_wf0 ("wf") and |
24 is_even ("iseven") and |
24 (*is_even ("iseven") and*) |
25 tcopy_init ("copy\<^bsub>begin\<^esub>") and |
25 tcopy_init ("copy\<^bsub>begin\<^esub>") and |
26 tcopy_loop ("copy\<^bsub>loop\<^esub>") and |
26 tcopy_loop ("copy\<^bsub>loop\<^esub>") and |
27 tcopy_end ("copy\<^bsub>end\<^esub>") and |
27 tcopy_end ("copy\<^bsub>end\<^esub>") and |
28 step0 ("step") and |
28 step0 ("step") and |
29 steps0 ("steps") and |
29 steps0 ("steps") and |
30 exponent ("_\<^bsup>_\<^esup>") and |
30 exponent ("_\<^bsup>_\<^esup>") and |
31 (* abc_lm_v ("lookup") and |
31 (* abc_lm_v ("lookup") and |
32 abc_lm_s ("set") and*) |
32 abc_lm_s ("set") and*) |
33 haltP ("stdhalt") and |
33 haltP ("stdhalt") and |
34 tcopy ("copy") and |
34 tcopy ("copy") and |
35 tape_of_nat_list ("\<ulcorner>_\<urcorner>") and |
35 tape_of ("\<langle>_\<rangle>") and |
36 tm_comp ("_ \<oplus> _") and |
36 tm_comp ("_ \<oplus> _") and |
37 DUMMY ("\<^raw:\mbox{$\_$}>") |
37 DUMMY ("\<^raw:\mbox{$\_$}>") |
38 |
38 |
39 declare [[show_question_marks = false]] |
39 declare [[show_question_marks = false]] |
40 |
40 |
68 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" |
68 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" |
69 ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
69 ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
70 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") |
70 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") |
71 "_asm" :: "prop \<Rightarrow> asms" ("_") |
71 "_asm" :: "prop \<Rightarrow> asms" ("_") |
72 |
72 |
73 |
73 lemma nats2tape: |
|
74 shows "<([]::nat list)> = []" |
|
75 and "<[n]> = Oc \<up> (n + 1)" |
|
76 and "ns \<noteq> [] \<Longrightarrow> <n#ns> = Oc \<up> (n + 1) @ [Bk] @ <ns>" |
|
77 apply(auto simp add: tape_of_nl_abv tape_of_nat_list.simps) |
|
78 apply(case_tac ns) |
|
79 apply(auto) |
|
80 done |
74 |
81 |
75 (*>*) |
82 (*>*) |
76 |
83 |
77 section {* Introduction *} |
84 section {* Introduction *} |
78 |
85 |
254 convention that the head, abbreviated @{term hd}, of the right-list |
261 convention that the head, abbreviated @{term hd}, of the right-list |
255 is the cell on which the head of the Turing machine currently |
262 is the cell on which the head of the Turing machine currently |
256 scannes. This can be pictured as follows: |
263 scannes. This can be pictured as follows: |
257 % |
264 % |
258 \begin{center} |
265 \begin{center} |
259 \begin{tikzpicture} |
266 \begin{tikzpicture}[scale=0.9] |
260 \draw[very thick] (-3.0,0) -- ( 3.0,0); |
267 \draw[very thick] (-3.0,0) -- ( 3.0,0); |
261 \draw[very thick] (-3.0,0.5) -- ( 3.0,0.5); |
268 \draw[very thick] (-3.0,0.5) -- ( 3.0,0.5); |
262 \draw[very thick] (-0.25,0) -- (-0.25,0.5); |
269 \draw[very thick] (-0.25,0) -- (-0.25,0.5); |
263 \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); |
270 \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); |
264 \draw[very thick] (-0.75,0) -- (-0.75,0.5); |
271 \draw[very thick] (-0.75,0) -- (-0.75,0.5); |
272 \draw[fill] (0.85,0.1) rectangle (1.15,0.4); |
279 \draw[fill] (0.85,0.1) rectangle (1.15,0.4); |
273 \draw[fill] (-0.35,0.1) rectangle (-0.65,0.4); |
280 \draw[fill] (-0.35,0.1) rectangle (-0.65,0.4); |
274 \draw[fill] (-1.65,0.1) rectangle (-1.35,0.4); |
281 \draw[fill] (-1.65,0.1) rectangle (-1.35,0.4); |
275 \draw (-0.25,0.8) -- (-0.25,-0.8); |
282 \draw (-0.25,0.8) -- (-0.25,-0.8); |
276 \draw[<->] (-1.25,-0.7) -- (0.75,-0.7); |
283 \draw[<->] (-1.25,-0.7) -- (0.75,-0.7); |
277 \node [anchor=base] at (-0.8,-0.5) {\small left list}; |
284 \node [anchor=base] at (-0.85,-0.5) {\small left list}; |
278 \node [anchor=base] at (0.35,-0.5) {\small right list}; |
285 \node [anchor=base] at (0.40,-0.5) {\small right list}; |
279 \node [anchor=base] at (0.1,0.7) {\small head}; |
286 \node [anchor=base] at (0.1,0.7) {\small head}; |
280 \node [anchor=base] at (-2.2,0.2) {\ldots}; |
287 \node [anchor=base] at (-2.2,0.2) {\ldots}; |
281 \node [anchor=base] at ( 2.3,0.2) {\ldots}; |
288 \node [anchor=base] at ( 2.3,0.2) {\ldots}; |
282 \end{tikzpicture} |
289 \end{tikzpicture} |
283 \end{center} |
290 \end{center} |
514 final state) and remains there performing @{text Nop}-actions until |
521 final state) and remains there performing @{text Nop}-actions until |
515 @{text n} is reached. |
522 @{text n} is reached. |
516 |
523 |
517 \begin{figure}[t] |
524 \begin{figure}[t] |
518 \begin{center} |
525 \begin{center} |
519 \begin{tabular}{@ {}p{3.6cm}@ {\hspace{4mm}}p{3.6cm}@ {\hspace{4mm}}p{3.6cm}@ {}} |
526 \begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {\hspace{3mm}}c} |
520 @{thm (lhs) tcopy_init_def} @{text "\<equiv>"} & |
527 \begin{tabular}{@ {}l@ {}} |
521 @{thm (lhs) tcopy_loop_def} @{text "\<equiv>"} & |
528 @{thm (lhs) tcopy_init_def} @{text "\<equiv>"}\\ |
|
529 @{text "["}@{text "(W0, 0), (R, 2), (R, 3),"}\\ |
|
530 \phantom{@{text "["}}@{text "(R, 2), (W1, 3), (L, 4),"}\\ |
|
531 \phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"} |
|
532 \end{tabular} |
|
533 & |
|
534 \begin{tabular}{@ {}p{3.6cm}@ {}} |
|
535 @{thm (lhs) tcopy_loop_def} @{text "\<equiv>"}\\ |
|
536 @{thm (rhs) tcopy_loop_def}\\ |
|
537 \end{tabular} |
|
538 & |
|
539 \begin{tabular}{@ {}p{3.6cm}@ {}} |
522 @{thm (lhs) tcopy_end_def} @{text "\<equiv>"}\\ |
540 @{thm (lhs) tcopy_end_def} @{text "\<equiv>"}\\ |
523 @{thm (rhs) tcopy_init_def} & |
|
524 @{thm (rhs) tcopy_loop_def} & |
|
525 @{thm (rhs) tcopy_end_def} |
541 @{thm (rhs) tcopy_end_def} |
|
542 \end{tabular} |
526 \end{tabular} |
543 \end{tabular} |
527 \end{center} |
544 \end{center} |
528 \caption{Copy machine}\label{copy} |
545 \caption{Copy machine}\label{copy} |
529 \end{figure} |
546 \end{figure} |
530 |
547 |
533 the right list contains some ``clusters'' of @{text "Oc"}s separted by single |
550 the right list contains some ``clusters'' of @{text "Oc"}s separted by single |
534 blanks. To make this formal we define the following function |
551 blanks. To make this formal we define the following function |
535 |
552 |
536 \begin{center} |
553 \begin{center} |
537 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} |
554 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} |
538 @{thm (lhs) tape_of_nat_list.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) tape_of_nat_list.simps(1)}\\ |
555 @{thm (lhs) nats2tape(1)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(1)}\\ |
539 @{thm (lhs) tape_of_nat_list.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) tape_of_nat_list.simps(2)}\\ |
556 @{thm (lhs) nats2tape(2)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(2)}\\ |
540 @{thm (lhs) tape_of_nat_list.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) tape_of_nat_list.simps(3)} |
557 @{thm (lhs) nats2tape(3)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(3)} |
541 \end{tabular} |
558 \end{tabular} |
542 \end{center} |
559 \end{center} |
543 |
560 |
544 \noindent |
561 \noindent |
545 A standard tape is then of the form @{text "(Bk\<^isup>l,\<langle>n\<^isub>1,...,n\<^isub>m\<rangle>)"} for some @{text l} |
562 A standard tape is then of the form @{text "(Bk\<^isup>l,\<langle>[n\<^isub>1,...,n\<^isub>m]\<rangle>)"} for some @{text l} |
546 and @{text "n\<^isub>i"}. Note that the head in a standard tape ``points'' to the |
563 and @{text "n\<^isub>i"}. Note that the head in a standard tape ``points'' to the |
547 leftmost @{term "Oc"} on the tape. |
564 leftmost @{term "Oc"} on the tape. Note also that @{text 0} is represented by |
548 |
565 a single filled cell, @{text 1} by two filled cells and so on. |
549 |
566 |
550 Before we can prove the undecidability of the halting problem for our |
567 Before we can prove the undecidability of the halting problem for our |
551 Turing machines, we need to analyse two concrete Turing machine |
568 Turing machines, we need to analyse two concrete Turing machine |
552 programs and establish that they are correct---that means they are |
569 programs and establish that they are correct---that means they are |
553 ``doing what they are supposed to be doing''. Such correctness proofs are usually left |
570 ``doing what they are supposed to be doing''. Such correctness proofs are usually left |
604 |
621 |
605 \begin{center} |
622 \begin{center} |
606 \begin{tabular}{l@ {\hspace{3mm}}lcl} |
623 \begin{tabular}{l@ {\hspace{3mm}}lcl} |
607 & \multicolumn{1}{c}{start tape}\\[1mm] |
624 & \multicolumn{1}{c}{start tape}\\[1mm] |
608 \raisebox{2.5mm}{halting case:} & |
625 \raisebox{2.5mm}{halting case:} & |
609 \begin{tikzpicture} |
626 \begin{tikzpicture}[scale=0.9] |
610 \draw[very thick] (-2,0) -- ( 0.75,0); |
627 \draw[very thick] (-2,0) -- ( 0.75,0); |
611 \draw[very thick] (-2,0.5) -- ( 0.75,0.5); |
628 \draw[very thick] (-2,0.5) -- ( 0.75,0.5); |
612 \draw[very thick] (-0.25,0) -- (-0.25,0.5); |
629 \draw[very thick] (-0.25,0) -- (-0.25,0.5); |
613 \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); |
630 \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); |
614 \draw[very thick] (-0.75,0) -- (-0.75,0.5); |
631 \draw[very thick] (-0.75,0) -- (-0.75,0.5); |
618 \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); |
635 \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); |
619 \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4); |
636 \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4); |
620 \node [anchor=base] at (-1.7,0.2) {\ldots}; |
637 \node [anchor=base] at (-1.7,0.2) {\ldots}; |
621 \end{tikzpicture} |
638 \end{tikzpicture} |
622 & \raisebox{2.5mm}{$\;\;\large\Rightarrow\;\;$} & |
639 & \raisebox{2.5mm}{$\;\;\large\Rightarrow\;\;$} & |
623 \begin{tikzpicture} |
640 \begin{tikzpicture}[scale=0.9] |
624 \draw[very thick] (-2,0) -- ( 0.75,0); |
641 \draw[very thick] (-2,0) -- ( 0.75,0); |
625 \draw[very thick] (-2,0.5) -- ( 0.75,0.5); |
642 \draw[very thick] (-2,0.5) -- ( 0.75,0.5); |
626 \draw[very thick] (-0.25,0) -- (-0.25,0.5); |
643 \draw[very thick] (-0.25,0) -- (-0.25,0.5); |
627 \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); |
644 \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); |
628 \draw[very thick] (-0.75,0) -- (-0.75,0.5); |
645 \draw[very thick] (-0.75,0) -- (-0.75,0.5); |
633 \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4); |
650 \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4); |
634 \node [anchor=base] at (-1.7,0.2) {\ldots}; |
651 \node [anchor=base] at (-1.7,0.2) {\ldots}; |
635 \end{tikzpicture}\\ |
652 \end{tikzpicture}\\ |
636 |
653 |
637 \raisebox{2.5mm}{non-halting case:} & |
654 \raisebox{2.5mm}{non-halting case:} & |
638 \begin{tikzpicture} |
655 \begin{tikzpicture}[scale=0.9] |
639 \draw[very thick] (-2,0) -- ( 0.25,0); |
656 \draw[very thick] (-2,0) -- ( 0.25,0); |
640 \draw[very thick] (-2,0.5) -- ( 0.25,0.5); |
657 \draw[very thick] (-2,0.5) -- ( 0.25,0.5); |
641 \draw[very thick] (-0.25,0) -- (-0.25,0.5); |
658 \draw[very thick] (-0.25,0) -- (-0.25,0.5); |
642 \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); |
659 \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); |
643 \draw[very thick] (-0.75,0) -- (-0.75,0.5); |
660 \draw[very thick] (-0.75,0) -- (-0.75,0.5); |