# HG changeset patch # User Christian Urban # Date 1359236772 0 # Node ID cf6e89b5f702942bf47545d8c673ada866179b09 # Parent 046c9ecf91509c7836a5bd7e5e9c7bda13ceb076 updated paper diff -r 046c9ecf9150 -r cf6e89b5f702 Paper/Paper.thy --- a/Paper/Paper.thy Sat Jan 26 12:00:21 2013 +0000 +++ b/Paper/Paper.thy Sat Jan 26 21:46:12 2013 +0000 @@ -524,30 +524,118 @@ \begin{figure}[t] \begin{center} \begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {\hspace{3mm}}c} - \begin{tabular}{@ {}l@ {}} + \begin{tabular}[t]{@ {}l@ {}} @{thm (lhs) tcopy_init_def} @{text "\"}\\ - @{text "["}@{text "(W0, 0), (R, 2), (R, 3),"}\\ - \phantom{@{text "["}}@{text "(R, 2), (W1, 3), (L, 4),"}\\ - \phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"} + \hspace{2mm}@{text "["}@{text "(W\<^bsub>Bk\<^esub>, 0), (R, 2), (R, 3),"}\\ + \hspace{2mm}\phantom{@{text "["}}@{text "(R, 2), (W1, 3), (L, 4),"}\\ + \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"} + \end{tabular} + & + \begin{tabular}[t]{@ {}l@ {}} + @{thm (lhs) tcopy_loop_def} @{text "\"}\\ + \hspace{2mm}@{text "["}@{text "(R, 0), (R, 2), (R, 3),"}\\ + \hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>Bk\<^esub>, 2), (R, 3), (R, 4),"}\\ + \hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>Oc\<^esub>, 5), (R, 4), (L, 6),"}\\ + \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (L, 6), (L, 1)"}@{text "]"} \end{tabular} & - \begin{tabular}{@ {}l@ {}} - @{thm (lhs) tcopy_loop_def} @{text "\"}\\ - @{text "["}@{text "(R, 0), (R, 2), (R, 3),"}\\ - \phantom{@{text "["}}@{text "(W0, 2), (R, 3), (R, 4),"}\\ - \phantom{@{text "["}}@{text "(W1, 5), (R, 4), (L, 6),"}\\ - \phantom{@{text "["}}@{text "(L, 5), (L, 6), (L, 1)"}@{text "]"} + \begin{tabular}[t]{@ {}l@ {}} + @{thm (lhs) tcopy_end_def} @{text "\"}\\ + \hspace{2mm}@{text "["}@{text "(L, 0), (R, 2), (W\<^bsub>Oc\<^esub>, 3),"}\\ + \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (R, 2), (R, 2),"}\\ + \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (W\<^bsub>Bk\<^esub>, 4), (R, 0),"}\\ + \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5)"}@{text "]"} \end{tabular} - & - \begin{tabular}{@ {}p{3.6cm}@ {}} - @{thm (lhs) tcopy_end_def} @{text "\"}\\ - @{thm (rhs) tcopy_end_def} - \end{tabular} - \end{tabular} + \end{tabular}\\[2mm] + + \begin{tikzpicture}[scale=0.7] + \node [anchor=base] at (2.2,0.1) {\small$\Rightarrow$}; + \node [anchor=base] at (5.6,0.1) {\small$\Rightarrow$}; + \node [anchor=base] at (10.5,0.1) {\small$\Rightarrow$}; + \node [anchor=base] at (2.2,-0.5) {\small@{term "tcopy_init"}}; + \node [anchor=base] at (5.6,-0.5) {\small@{term "tcopy_loop"}}; + \node [anchor=base] at (10.5,-0.5) {\small@{term "tcopy_end"}}; + + + \begin{scope}[shift={(0.5,0)}] + \draw[very thick] (-0.25,0) -- ( 1.25,0); + \draw[very thick] (-0.25,0.5) -- ( 1.25,0.5); + \draw[very thick] (-0.25,0) -- (-0.25,0.5); + \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); + \draw[very thick] ( 0.75,0) -- ( 0.75,0.5); + \draw[very thick] ( 1.25,0) -- ( 1.25,0.5); + \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); + \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); + \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4); + \draw[fill] ( 0.85,0.1) rectangle (1.15,0.4); + \end{scope} + + \begin{scope}[shift={(2.9,0)}] + \draw[very thick] (-0.25,0) -- ( 2.25,0); + \draw[very thick] (-0.25,0.5) -- ( 2.25,0.5); + \draw[very thick] (-0.25,0) -- (-0.25,0.5); + \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); + \draw[very thick] ( 0.75,0) -- ( 0.75,0.5); + \draw[very thick] ( 1.25,0) -- ( 1.25,0.5); + \draw[very thick] ( 1.75,0) -- ( 1.75,0.5); + \draw[very thick] ( 2.25,0) -- ( 2.25,0.5); + \draw[rounded corners=1mm] (0.15,-0.1) rectangle (0.85,0.6); + \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); + \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4); + \draw[fill] ( 0.85,0.1) rectangle (1.15,0.4); + \draw[fill] ( 1.85,0.1) rectangle (2.15,0.4); + \end{scope} + + \begin{scope}[shift={(6.8,0)}] + \draw[very thick] (-0.75,0) -- ( 3.25,0); + \draw[very thick] (-0.75,0.5) -- ( 3.25,0.5); + \draw[very thick] (-0.75,0) -- (-0.75,0.5); + \draw[very thick] (-0.25,0) -- (-0.25,0.5); + \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); + \draw[very thick] ( 0.75,0) -- ( 0.75,0.5); + \draw[very thick] ( 1.25,0) -- ( 1.25,0.5); + \draw[very thick] ( 1.75,0) -- ( 1.75,0.5); + \draw[very thick] ( 2.25,0) -- ( 2.25,0.5); + \draw[very thick] ( 2.75,0) -- ( 2.75,0.5); + \draw[very thick] ( 3.25,0) -- ( 3.25,0.5); + \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); + \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); + \draw[fill] ( 2.35,0.1) rectangle (2.65,0.4); + \draw[fill] ( 2.85,0.1) rectangle (3.15,0.4); + \draw[fill] ( 1.85,0.1) rectangle (2.15,0.4); + \end{scope} + + \begin{scope}[shift={(11.7,0)}] + \draw[very thick] (-0.75,0) -- ( 3.25,0); + \draw[very thick] (-0.75,0.5) -- ( 3.25,0.5); + \draw[very thick] (-0.75,0) -- (-0.75,0.5); + \draw[very thick] (-0.25,0) -- (-0.25,0.5); + \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); + \draw[very thick] ( 0.75,0) -- ( 0.75,0.5); + \draw[very thick] ( 1.25,0) -- ( 1.25,0.5); + \draw[very thick] ( 1.75,0) -- ( 1.75,0.5); + \draw[very thick] ( 2.25,0) -- ( 2.25,0.5); + \draw[very thick] ( 2.75,0) -- ( 2.75,0.5); + \draw[very thick] ( 3.25,0) -- ( 3.25,0.5); + \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); + \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); + \draw[fill] ( 2.35,0.1) rectangle (2.65,0.4); + \draw[fill] ( 2.85,0.1) rectangle (3.15,0.4); + \draw[fill] ( 1.85,0.1) rectangle (2.15,0.4); + \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4); + \draw[fill] ( 0.85,0.1) rectangle (1.15,0.4); + \end{scope} + \end{tikzpicture}\\[-8mm]\mbox{} \end{center} - \caption{Copy machine}\label{copy} + \caption{The components of the \emph{copy Turing machine} (above). If started + with the tape @{term "([], <[(3::nat)]>)"} the first machine adds @{term "[Bk, Oc]"} at + the end of the right tape; the second then ``moves'' all @{term Oc}s except the + first from the beginning of the tape to the end; the third ``refills'' the original + block of @{term "Oc"}s. The result is the tape @{term "([Bk], <[(3::nat, 3::nat)]>)"}.} + \label{copy} \end{figure} + We often need to restrict tapes to be in \emph{standard form}, which means the left list of the tape is either empty or only contains @{text "Bk"}s, and the right list contains some ``clusters'' of @{text "Oc"}s separted by single @@ -692,9 +780,9 @@ In the following we will consider the following Turing machine program that makes a copies a value on the tape. - + - + diff -r 046c9ecf9150 -r cf6e89b5f702 paper.pdf Binary file paper.pdf has changed