1168 example the second instruction the jump @{term "Goto 0"} in @{term clear} means |
1168 example the second instruction the jump @{term "Goto 0"} in @{term clear} means |
1169 we jump back to the first instruction closing the loop. Like with our |
1169 we jump back to the first instruction closing the loop. Like with our |
1170 Turing machines, we fetch instructions from an abacus program such |
1170 Turing machines, we fetch instructions from an abacus program such |
1171 that a jump out of ``range'' behaves like a @{term "Nop"}-action. In |
1171 that a jump out of ``range'' behaves like a @{term "Nop"}-action. In |
1172 this way it is easy to define a function @{term steps} that |
1172 this way it is easy to define a function @{term steps} that |
1173 executes @{term n} instructions of an abacus program. |
1173 executes @{term n} instructions of an abacus program. By convention |
|
1174 the value calculated by an abacus program is stored in the |
|
1175 last register (the register with the highest index). |
1174 |
1176 |
1175 The main point of abacus programs is to be able to translate them to |
1177 The main point of abacus programs is to be able to translate them to |
1176 Turing machine programs. Registers and their content are represented by |
1178 Turing machine programs. Registers and their content are represented by |
1177 standard tapes. |
1179 standard tapes. |
1178 Because of the jumps in abacus programs, it |
1180 Because of the jumps in abacus programs, it |
1227 with @{text 16} states. |
1229 with @{text 16} states. |
1228 |
1230 |
1229 Finally, having a turing machine for each abacus instruction we need |
1231 Finally, having a turing machine for each abacus instruction we need |
1230 to ``stitch'' the Turing machines together into one so that each |
1232 to ``stitch'' the Turing machines together into one so that each |
1231 Turing machine component transitions to next one, just like in |
1233 Turing machine component transitions to next one, just like in |
1232 are needed to translate each abacus instructionabacus |
1234 the abacus programs. One last problem to overcome is that an abacus |
1233 programs. While generating the Turing machine program for an abacus |
1235 program is assumed to calculate a value stored in the last |
|
1236 register. That means we have to append a Turing machine that |
|
1237 ``mops up'' the tape (cleaning all @{text Oc}s) except for the |
|
1238 last number represented on the tape. |
|
1239 |
|
1240 While generating the Turing machine program for an abacus |
1234 program is not too difficult to formalise, the problem is that it |
1241 program is not too difficult to formalise, the problem is that it |
1235 contains @{text Goto}s all over the place. The unfortunate result is |
1242 contains @{text Goto}s all over the place. The unfortunate result is |
1236 are needed to translate each abacus instructionthat we cannot |
1243 are needed to translate each abacus instructionthat we cannot |
1237 use our Hoare-rules for reasoning about sequentially composed |
1244 use our Hoare-rules for reasoning about sequentially composed |
1238 programs. Instead we have to treat the Turing machine as one ``block'' |
1245 programs. Instead we have to treat the Turing machine as one ``block'' |