1179 The main point of abacus programs is to be able to translate them to |
1179 The main point of abacus programs is to be able to translate them to |
1180 Turing machine programs. Registers and their content are represented by |
1180 Turing machine programs. Registers and their content are represented by |
1181 standard tapes. Because of the jumps in abacus programs, it |
1181 standard tapes. Because of the jumps in abacus programs, it |
1182 seems difficult to build a Turing machine programs out of components |
1182 seems difficult to build a Turing machine programs out of components |
1183 using our @{text "\<oplus>"}-operation shown in the previous section. |
1183 using our @{text "\<oplus>"}-operation shown in the previous section. |
1184 To overcome this difficulty, we calculate a \emph{layout} as follows |
1184 To overcome this difficulty, we calculate a \emph{layout} of an |
|
1185 abacus program as follows |
1185 |
1186 |
1186 \begin{center} |
1187 \begin{center} |
1187 \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} |
1188 \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} |
1188 @{thm (lhs) layout(1)} & @{text "\<equiv>"} & @{thm (rhs) layout(1)}\\ |
1189 @{thm (lhs) layout(1)} & @{text "\<equiv>"} & @{thm (rhs) layout(1)}\\ |
1189 @{thm (lhs) layout(2)} & @{text "\<equiv>"} & @{thm (rhs) layout(2)}\\ |
1190 @{thm (lhs) layout(2)} & @{text "\<equiv>"} & @{thm (rhs) layout(2)}\\ |
1201 \begin{center} |
1202 \begin{center} |
1202 @{thm (rhs) tgoto.simps[where n="i"]} |
1203 @{thm (rhs) tgoto.simps[where n="i"]} |
1203 \end{center} |
1204 \end{center} |
1204 |
1205 |
1205 \noindent |
1206 \noindent |
1206 where @{term "i"} is the corresponding state in the Turing machine program |
1207 where @{term "i"} is the state in the Turing machine program |
1207 to jump to. For translating the instruction @{term Inc} |
1208 to jump to. For translating the instruction @{term Inc}, |
1208 one has to remember that the content of the registers are encoded |
1209 one has to remember that the content of the registers are encoded |
1209 in the Turing machine as standard tape. Therefore the translated Turing machine |
1210 in the Turing machine as standard tape. Therefore the translated Turing machine |
1210 needs to first find the number corresponding to the register @{text "R"}. This needs a machine |
1211 needs to first find the number corresponding to the register @{text "R"}. This needs a machine |
1211 with @{term "(2::nat) * R\<iota>"} states and can be constructed as follows: |
1212 with @{term "(2::nat) * R\<iota>"} states and can be constructed as follows: |
1212 |
1213 |
1218 \end{tabular} |
1219 \end{tabular} |
1219 \end{center} |
1220 \end{center} |
1220 |
1221 |
1221 \noindent |
1222 \noindent |
1222 Then we need to increase the ``number'' on the tape by one, |
1223 Then we need to increase the ``number'' on the tape by one, |
1223 and adjust the following registers. By adjusting we only need to |
1224 and adjust the following ``registers''. By adjusting we only need to |
1224 replace the first @{term Oc} of each number by @{term Bk} and the last |
1225 replace the first @{term Oc} of each number by @{term Bk} and the last |
1225 one from @{term Bk} to @{term Oc}. |
1226 one from @{term Bk} to @{term Oc}. |
1226 Finally we need to transition the head of the |
1227 Finally, we need to transition the head of the |
1227 Turing machine back into the standard position. This requires a Turing machine |
1228 Turing machine back into the standard position. This requires a Turing machine |
1228 with 9 states (we omit the details). Similarly for the translation of @{term Dec}, where the |
1229 with 9 states (we omit the details). Similarly for the translation of @{term Dec}, where the |
1229 translated Turing machine needs to first check whether the content of the |
1230 translated Turing machine needs to first check whether the content of the |
1230 corresponding register is @{text 0}. For this we have a Turing machine program |
1231 corresponding register is @{text 0}. For this we have a Turing machine program |
1231 with @{text 16} states. |
1232 with @{text 16} states (again details are omitted). |
1232 |
1233 |
1233 Finally, having a Turing machine for each abacus instruction we need |
1234 Finally, having a Turing machine for each abacus instruction we need |
1234 to ``stitch'' the Turing machines together into one so that each |
1235 to ``stitch'' the Turing machines together into one so that each |
1235 Turing machine component transitions to next one, just like in |
1236 Turing machine component transitions to next one, just like in |
1236 the abacus programs. One last problem to overcome is that an abacus |
1237 the abacus programs. One last problem to overcome is that an abacus |
1237 program is assumed to calculate a value stored in the last |
1238 program is assumed to calculate a value stored in the last |
1238 register. That means we have to append a Turing machine that |
1239 register. That means we have to append a Turing machine that |
1239 ``mops up'' the tape (cleaning all @{text Oc}s) except for the |
1240 ``mops up'' the tape (cleaning all @{text Oc}s) except for the |
1240 last number represented on the tape. |
1241 @{term Oc}s of the last number represented on the tape. |
1241 |
1242 |
1242 While generating the Turing machine program for an abacus |
1243 While generating the Turing machine program for an abacus program is |
1243 program is not too difficult to formalise, the problem is that it |
1244 not too difficult to formalise, the problem is that it contains |
1244 contains @{text Goto}s all over the place. The unfortunate result is |
1245 @{text Goto}s all over the place. The unfortunate result is that we |
1245 are needed to translate each abacus instruction that we cannot |
1246 cannot use our Hoare-rules for reasoning about sequentially composed |
1246 use our Hoare-rules for reasoning about sequentially composed |
1247 programs (for this the programs need to be independent). Instead we |
1247 programs. Instead we have to treat the Turing machine as one |
1248 have to treat the translated Turing machine as one ``big block'' and |
1248 are needed to translate each abacus instruction``block'' |
1249 prove as invariant that it performs |
1249 and show as invariant that it performs the same operations |
1250 the same operations as the abacus program. For this we have to show |
1250 as the abacus program. For this we have to show that for each |
1251 that for each configuration of an abacus machine the @{term |
1251 configuration of an abacus machine the @{term step}-function |
1252 step}-function is simulated by zero or more steps in our translated |
1252 is simulated by zero or more steps in our constructed Turing |
1253 Turing machine. This leads to a rather large ``monolithic'' |
1253 machine. This leads to a rather large ``monolithic'' |
1254 correctness proof (4600 loc and 380 sublemmas) that on the |
1254 correctness proof (4600 loc and 380 sublemmas) that on the conceptual |
1255 conceptual level is difficult to break down into smaller components. |
1255 level is difficult to break down into smaller components. |
|
1256 |
1256 |
1257 %We were able to simplify the proof somewhat |
1257 %We were able to simplify the proof somewhat |
1258 *} |
1258 *} |
1259 |
1259 |
1260 |
1260 |