--- a/Paper/Paper.thy Mon Feb 04 23:12:17 2013 +0000
+++ b/Paper/Paper.thy Tue Feb 05 08:57:55 2013 +0000
@@ -83,7 +83,9 @@
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:
@@ -154,8 +156,8 @@
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 ((Goto o\<iota>)#os) = 1#(layout_of os)"
+ and "layout_of ((Dec R\<iota> i)#os) = (2 * R\<iota> + 16)#(layout_of os)"
+ and "layout_of ((Goto i)#os) = 1#(layout_of os)"
by(auto simp add: layout_of.simps length_of.simps)
@@ -1140,15 +1142,15 @@
$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\\
- & $\mid$ & @{term "Dec R\<iota> o\<iota>"} & if content of $R$ is non-zero,\\
+ @{text "i"} & $::=$ & @{term "Inc R\<iota>"} & increment register $R$ by one\\
+ & $\mid$ & @{term "Dec R\<iota> i"} & if content of $R$ is non-zero,\\
& & & then decrement it by one\\
- & & & otherwise jump to statement $o$\\
- & $\mid$ & @{term "Goto o\<iota>"} & jump to statement $o$
+ & & & otherwise jump to instruction $i$\\
+ & $\mid$ & @{term "Goto i"} & jump to instruction $i$
\end{tabular}
\end{center}
@@ -1157,42 +1159,87 @@
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
- example the second statement the jump @{term "Goto 0"} in @{term clear} means
- we jump back to the first statement closing the loop. Like with our
- Turing machines, we fetch statements from an abacus program such
+ then execute one instructions after the other, unless there is a jump. For
+ example the second instruction the jump @{term "Goto 0"} in @{term clear} means
+ we jump back to the first instruction closing the loop. Like with our
+ 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}
+ \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+ @{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)}\\
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ This gives us a list of natural numbers specifying how many states
+ are needed to translate each abacus instruction. The @{text Goto}
+ instruction is easiest to translate requiring only one state in
+ the corresponding Turing machine:
\begin{center}
- @{thm layout}
+ @{thm (rhs) tgoto.simps[where n="i"]}
+ \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.
- %Running an abacus program means to start
- %A \emph{program} of an abacus machine is a list of such
- %statements.
- %The \emph{memory} $m$ of an abacus machine holding the values
- %of the registers is represented as a list of natural numbers.
- %We have a lookup function for this memory, written @{term "abc_lm_v m R\<iota>"},
- %which looks up the content of register $R$; if $R$
- %is not in this list, then we return 0. Similarly we
- %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$
- %it pads it approriately with 0s.
- %Abacus machine halts when it jumps out of range.
*}