# HG changeset patch # User Christian Urban # Date 1360054675 0 # Node ID b27f4bd98078a39dd2f71a9f58eaf93b9f5e52e8 # Parent 11fd52dceb9b03e652ccd4a05f45a621e074f34f updated diff -r 11fd52dceb9b -r b27f4bd98078 Paper/Paper.thy --- 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\)#os) = (2 * R\ + 9)#(layout_of os)" - and "layout_of ((Dec R\ o\)#os) = (2 * R\ + 16)#(layout_of os)" - and "layout_of ((Goto o\)#os) = 1#(layout_of os)" + and "layout_of ((Dec R\ i)#os) = (2 * R\ + 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\"} & increment register $R$ by one\\ - & $\mid$ & @{term "Dec R\ o\"} & if content of $R$ is non-zero,\\ + @{text "i"} & $::=$ & @{term "Inc R\"} & increment register $R$ by one\\ + & $\mid$ & @{term "Dec R\ i"} & if content of $R$ is non-zero,\\ & & & then decrement it by one\\ - & & & otherwise jump to statement $o$\\ - & $\mid$ & @{term "Goto o\"} & 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\" and e="o\", THEN eq_reflection]} + @{thm clear.simps[where n="R\" 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 "\"}. - 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 "\"} & @{thm (rhs) layout(1)}\\ + @{thm (lhs) layout(2)} & @{text "\"} & @{thm (rhs) layout(2)}\\ + @{thm (lhs) layout(3)} & @{text "\"} & @{thm (rhs) layout(3)}\\ + @{thm (lhs) layout(4)} & @{text "\"} & @{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\"} 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 "\"} & @{thm (rhs) findnth.simps(1)}\\ + @{thm (lhs) findnth.simps(2)} & @{text "\"}\\ + \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\"}, - %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\ 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. *} diff -r 11fd52dceb9b -r b27f4bd98078 paper.pdf Binary file paper.pdf has changed