tm: comparison Paper/Paper.thy

equal deleted inserted replaced

-:11fd52dceb9b
+:b27f4bd98078
 inv_begin ("I\<^bsub>cbegin\<^esub>") and
 inv_loop1 ("J\<^isub>1") and
 inv_loop0 ("J\<^isub>0") and
 inv_end1 ("K\<^isub>1") and
 inv_end0 ("K\<^isub>0") and
-measure_begin_step ("M\<^bsub>cbegin\<^esub>")
+measure_begin_step ("M\<^bsub>cbegin\<^esub>") and
+layout_of ("layout") and
+findnth ("find'_nth")
 lemma inv_begin_print:
 shows "s = 0 \<Longrightarrow> inv_begin n (s, tp) = inv_begin0 n tp" and
 "s = 1 \<Longrightarrow> inv_begin n (s, tp) = inv_begin1 n tp" and
 lemma layout:
 shows "layout_of [] = []"
 and   "layout_of ((Inc R\<iota>)#os) = (2 * R\<iota> + 9)#(layout_of os)"
-and   "layout_of ((Dec R\<iota> o\<iota>)#os) = (2 * R\<iota> + 16)#(layout_of os)"
+and   "layout_of ((Dec R\<iota> i)#os) = (2 * R\<iota> + 16)#(layout_of os)"
-and   "layout_of ((Goto o\<iota>)#os) = 1#(layout_of os)"
+and   "layout_of ((Goto i)#os) = 1#(layout_of os)"
 by(auto simp add: layout_of.simps length_of.simps)
 (*>*)
 for making it less laborious to write Turing machine
 programs. Abacus machines operate over a set of registers $R_0$,
 $R_1$, \ldots{} each being able to hold an arbitrary large natural
 number.  We use natural numbers to refer to registers; we also use a natural number
 to represent a program counter and jumping ``addresses''. An abacus
-program is a list of \emph{statements} defined by the datatype:
+program is a list of \emph{instructions} defined by the datatype:
 \begin{center}
 \begin{tabular}{rcl@ {\hspace{10mm}}l}
-@{text "o"} & $::=$  & @{term "Inc R\<iota>"} & increment register $R$ by one\\
+@{text "i"} & $::=$  & @{term "Inc R\<iota>"} & increment register $R$ by one\\
-& $\mid$ & @{term "Dec R\<iota> o\<iota>"} & if content of $R$ is non-zero,\\
+& $\mid$ & @{term "Dec R\<iota> i"} & if content of $R$ is non-zero,\\
 & & & then decrement it by one\\
-& & & otherwise jump to statement $o$\\
+& & & otherwise jump to instruction $i$\\
-& $\mid$ & @{term "Goto o\<iota>"} & jump to statement $o$
+& $\mid$ & @{term "Goto i"} & jump to instruction $i$
 \end{tabular}
 \end{center}
 \noindent
 For example the program clearing the register $R$ (that is setting
 it to @{term "(0::nat)"}) can be defined as follows:
 \begin{center}
-@{thm clear.simps[where n="R\<iota>" and e="o\<iota>", THEN eq_reflection]}
+@{thm clear.simps[where n="R\<iota>" and e="i", THEN eq_reflection]}
 \end{center}
 \noindent
 Running such a program means we start with the first instruction
-then execute one statements after the other, unless there is a jump.  For
+then execute one instructions after the other, unless there is a jump.  For
-example the second statement the jump @{term "Goto 0"} in @{term clear} means
+example the second instruction the jump @{term "Goto 0"} in @{term clear} means
-we jump back to the first statement closing the loop.  Like with our
+we jump back to the first instruction closing the loop.  Like with our
-Turing machines, we fetch statements from an abacus program such
+Turing machines, we fetch instructions from an abacus program such
 that a jump out of ``range'' behaves like a @{term "Nop"}-action. In
 this way it is easy to define a function @{term steps} that
-executes @{term n} statements of an abacus program.
+executes @{term n} instructions of an abacus program.
 The main point of abacus programs is to be able to translate them to
-Turing machine programs. Because of the jumps in abacus programs, it
+Turing machine programs. Registers and their content are represented by
+standard tapes.
+Because of the jumps in abacus programs, it
 seems difficult to build Turing machine programs using @{text "\<oplus>"}.
-To overcome this difficulty we calculate a \emph{layout} as follows
+To overcome this difficulty, we calculate a \emph{layout} as follows
 \begin{center}
-@{thm layout}
+\begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
-\end{center}
+@{thm (lhs) layout(1)} & @{text "\<equiv>"} & @{thm (rhs) layout(1)}\\
+@{thm (lhs) layout(2)} & @{text "\<equiv>"} & @{thm (rhs) layout(2)}\\
+@{thm (lhs) layout(3)} & @{text "\<equiv>"} & @{thm (rhs) layout(3)}\\
+@{thm (lhs) layout(4)} & @{text "\<equiv>"} & @{thm (rhs) layout(4)}\\
-%Running an abacus program means to start
+\end{tabular}
-%A \emph{program} of an abacus machine is a list of such
+\end{center}
-%statements.
-%The \emph{memory} $m$ of an abacus machine holding the values
+\noindent
-%of the registers is represented as a list of natural numbers.
+This gives us a list of natural numbers specifying how many states
-%We have a lookup function for this memory, written @{term "abc_lm_v m R\<iota>"},
+are needed to translate each abacus instruction. The @{text Goto}
-%which looks up the content of register $R$; if $R$
+instruction is easiest to translate requiring only one state in
-%is not in this list, then we return 0. Similarly we
+the corresponding Turing machine:
-%have a setting function, written @{term "abc_lm_s m R\<iota> n"}, which
-%sets the value of $R$ to $n$, and if $R$ was not yet in $m$
+\begin{center}
-%it pads it approriately with 0s.
+@{thm (rhs) tgoto.simps[where n="i"]}
-%Abacus machine halts when it jumps out of range.
+\end{center}
+\noindent
+where @{term "i"} is the corresponding state in the Turing machine program
+to jump to. For translating the instruction @{term Inc}
+one has to remember that the content of the registers are encoded
+in the Turing machine as standard tape. Therefore the translated Turing machine
+needs to first find the number corresponding to the register @{text "R"}. This needs a machine
+with @{term "(2::nat) * R\<iota>"} states and can be constructed as follows:
+\begin{center}
+\begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+@{thm (lhs) findnth.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) findnth.simps(1)}\\
+@{thm (lhs) findnth.simps(2)} & @{text "\<equiv>"}\\
+\multicolumn{3}{@ {}l@ {}}{\hspace{8mm}@{thm (rhs) findnth.simps(2)}}\\
+\end{tabular}
+\end{center}
+\noindent
+Then we need to increase the ``number'' on the tape by one,
+and adjust the following registers. By adjusting we only need to
+replace the first @{term Oc} of each number by @{term Bk} and the last
+one from @{term Bk} to @{term Oc}.
+Finally we need to transition the head of the
+Turing machine back into the standard position. This requires a Turing machine
+with 9 states. Similarly for the translation of @{term Dec}, where the
+translated Turing machine needs to first check whether the content of the
+corresponding register is @{text 0}. For this we have a Turing machine program
+with @{text 16} states.
+Finally, having a turing machine for each abacus instruction we need
+to ``stitch'' the Turing machines together into one so that each
+Turing machine component transitions to next one, just like in
+are needed to translate each abacus instructionabacus
+programs. While generating the Turing machine program for an abacus
+program is not too difficult to formalise, the problem is that it
+contains @{text Goto}s all over the place. The unfortunate result is
+are needed to translate each abacus instructionthat we cannot
+use our Hoare-rules for reasoning about sequentially composed
+programs. Instead we have to treat the Turing machine as one ``block''
+and show as invariant that it performs the same operations
+as the abacus program.
 *}
 section {* Recursive Functions *}

changeset 117	b27f4bd98078
parent 116	11fd52dceb9b
child 118	7d8a1bfb8925