522 @{text n} is reached. |
522 @{text n} is reached. |
523 |
523 |
524 \begin{figure}[t] |
524 \begin{figure}[t] |
525 \begin{center} |
525 \begin{center} |
526 \begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {\hspace{3mm}}c} |
526 \begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {\hspace{3mm}}c} |
527 \begin{tabular}{@ {}l@ {}} |
527 \begin{tabular}[t]{@ {}l@ {}} |
528 @{thm (lhs) tcopy_init_def} @{text "\<equiv>"}\\ |
528 @{thm (lhs) tcopy_init_def} @{text "\<equiv>"}\\ |
529 @{text "["}@{text "(W0, 0), (R, 2), (R, 3),"}\\ |
529 \hspace{2mm}@{text "["}@{text "(W\<^bsub>Bk\<^esub>, 0), (R, 2), (R, 3),"}\\ |
530 \phantom{@{text "["}}@{text "(R, 2), (W1, 3), (L, 4),"}\\ |
530 \hspace{2mm}\phantom{@{text "["}}@{text "(R, 2), (W1, 3), (L, 4),"}\\ |
531 \phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"} |
531 \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"} |
532 \end{tabular} |
532 \end{tabular} |
533 & |
533 & |
534 \begin{tabular}{@ {}l@ {}} |
534 \begin{tabular}[t]{@ {}l@ {}} |
535 @{thm (lhs) tcopy_loop_def} @{text "\<equiv>"}\\ |
535 @{thm (lhs) tcopy_loop_def} @{text "\<equiv>"}\\ |
536 @{text "["}@{text "(R, 0), (R, 2), (R, 3),"}\\ |
536 \hspace{2mm}@{text "["}@{text "(R, 0), (R, 2), (R, 3),"}\\ |
537 \phantom{@{text "["}}@{text "(W0, 2), (R, 3), (R, 4),"}\\ |
537 \hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>Bk\<^esub>, 2), (R, 3), (R, 4),"}\\ |
538 \phantom{@{text "["}}@{text "(W1, 5), (R, 4), (L, 6),"}\\ |
538 \hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>Oc\<^esub>, 5), (R, 4), (L, 6),"}\\ |
539 \phantom{@{text "["}}@{text "(L, 5), (L, 6), (L, 1)"}@{text "]"} |
539 \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (L, 6), (L, 1)"}@{text "]"} |
540 \end{tabular} |
540 \end{tabular} |
541 & |
541 & |
542 \begin{tabular}{@ {}p{3.6cm}@ {}} |
542 \begin{tabular}[t]{@ {}l@ {}} |
543 @{thm (lhs) tcopy_end_def} @{text "\<equiv>"}\\ |
543 @{thm (lhs) tcopy_end_def} @{text "\<equiv>"}\\ |
544 @{thm (rhs) tcopy_end_def} |
544 \hspace{2mm}@{text "["}@{text "(L, 0), (R, 2), (W\<^bsub>Oc\<^esub>, 3),"}\\ |
545 \end{tabular} |
545 \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (R, 2), (R, 2),"}\\ |
546 \end{tabular} |
546 \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (W\<^bsub>Bk\<^esub>, 4), (R, 0),"}\\ |
547 \end{center} |
547 \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5)"}@{text "]"} |
548 \caption{Copy machine}\label{copy} |
548 \end{tabular} |
|
549 \end{tabular}\\[2mm] |
|
550 |
|
551 \begin{tikzpicture}[scale=0.7] |
|
552 \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 (10.5,0.1) {\small$\Rightarrow$}; |
|
555 \node [anchor=base] at (2.2,-0.5) {\small@{term "tcopy_init"}}; |
|
556 \node [anchor=base] at (5.6,-0.5) {\small@{term "tcopy_loop"}}; |
|
557 \node [anchor=base] at (10.5,-0.5) {\small@{term "tcopy_end"}}; |
|
558 |
|
559 |
|
560 \begin{scope}[shift={(0.5,0)}] |
|
561 \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) -- (-0.25,0.5); |
|
564 \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); |
|
565 \draw[very thick] ( 0.75,0) -- ( 0.75,0.5); |
|
566 \draw[very thick] ( 1.25,0) -- ( 1.25,0.5); |
|
567 \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); |
|
568 \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); |
|
569 \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4); |
|
570 \draw[fill] ( 0.85,0.1) rectangle (1.15,0.4); |
|
571 \end{scope} |
|
572 |
|
573 \begin{scope}[shift={(2.9,0)}] |
|
574 \draw[very thick] (-0.25,0) -- ( 2.25,0); |
|
575 \draw[very thick] (-0.25,0.5) -- ( 2.25,0.5); |
|
576 \draw[very thick] (-0.25,0) -- (-0.25,0.5); |
|
577 \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); |
|
578 \draw[very thick] ( 0.75,0) -- ( 0.75,0.5); |
|
579 \draw[very thick] ( 1.25,0) -- ( 1.25,0.5); |
|
580 \draw[very thick] ( 1.75,0) -- ( 1.75,0.5); |
|
581 \draw[very thick] ( 2.25,0) -- ( 2.25,0.5); |
|
582 \draw[rounded corners=1mm] (0.15,-0.1) rectangle (0.85,0.6); |
|
583 \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); |
|
584 \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4); |
|
585 \draw[fill] ( 0.85,0.1) rectangle (1.15,0.4); |
|
586 \draw[fill] ( 1.85,0.1) rectangle (2.15,0.4); |
|
587 \end{scope} |
|
588 |
|
589 \begin{scope}[shift={(6.8,0)}] |
|
590 \draw[very thick] (-0.75,0) -- ( 3.25,0); |
|
591 \draw[very thick] (-0.75,0.5) -- ( 3.25,0.5); |
|
592 \draw[very thick] (-0.75,0) -- (-0.75,0.5); |
|
593 \draw[very thick] (-0.25,0) -- (-0.25,0.5); |
|
594 \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); |
|
595 \draw[very thick] ( 0.75,0) -- ( 0.75,0.5); |
|
596 \draw[very thick] ( 1.25,0) -- ( 1.25,0.5); |
|
597 \draw[very thick] ( 1.75,0) -- ( 1.75,0.5); |
|
598 \draw[very thick] ( 2.25,0) -- ( 2.25,0.5); |
|
599 \draw[very thick] ( 2.75,0) -- ( 2.75,0.5); |
|
600 \draw[very thick] ( 3.25,0) -- ( 3.25,0.5); |
|
601 \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); |
|
602 \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); |
|
603 \draw[fill] ( 2.35,0.1) rectangle (2.65,0.4); |
|
604 \draw[fill] ( 2.85,0.1) rectangle (3.15,0.4); |
|
605 \draw[fill] ( 1.85,0.1) rectangle (2.15,0.4); |
|
606 \end{scope} |
|
607 |
|
608 \begin{scope}[shift={(11.7,0)}] |
|
609 \draw[very thick] (-0.75,0) -- ( 3.25,0); |
|
610 \draw[very thick] (-0.75,0.5) -- ( 3.25,0.5); |
|
611 \draw[very thick] (-0.75,0) -- (-0.75,0.5); |
|
612 \draw[very thick] (-0.25,0) -- (-0.25,0.5); |
|
613 \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); |
|
614 \draw[very thick] ( 0.75,0) -- ( 0.75,0.5); |
|
615 \draw[very thick] ( 1.25,0) -- ( 1.25,0.5); |
|
616 \draw[very thick] ( 1.75,0) -- ( 1.75,0.5); |
|
617 \draw[very thick] ( 2.25,0) -- ( 2.25,0.5); |
|
618 \draw[very thick] ( 2.75,0) -- ( 2.75,0.5); |
|
619 \draw[very thick] ( 3.25,0) -- ( 3.25,0.5); |
|
620 \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); |
|
621 \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); |
|
622 \draw[fill] ( 2.35,0.1) rectangle (2.65,0.4); |
|
623 \draw[fill] ( 2.85,0.1) rectangle (3.15,0.4); |
|
624 \draw[fill] ( 1.85,0.1) rectangle (2.15,0.4); |
|
625 \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4); |
|
626 \draw[fill] ( 0.85,0.1) rectangle (1.15,0.4); |
|
627 \end{scope} |
|
628 \end{tikzpicture}\\[-8mm]\mbox{} |
|
629 \end{center} |
|
630 \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 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 block of @{term "Oc"}s. The result is the tape @{term "([Bk], <[(3::nat, 3::nat)]>)"}.} |
|
635 \label{copy} |
549 \end{figure} |
636 \end{figure} |
|
637 |
550 |
638 |
551 We often need to restrict tapes to be in \emph{standard form}, which means |
639 We often need to restrict tapes to be in \emph{standard form}, which means |
552 the left list of the tape is either empty or only contains @{text "Bk"}s, and |
640 the left list of the tape is either empty or only contains @{text "Bk"}s, and |
553 the right list contains some ``clusters'' of @{text "Oc"}s separted by single |
641 the right list contains some ``clusters'' of @{text "Oc"}s separted by single |
554 blanks. To make this formal we define the following function |
642 blanks. To make this formal we define the following function |