1229 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 |
1230 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 |
1231 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 |
1232 with @{text 16} states. |
1232 with @{text 16} states. |
1233 |
1233 |
1234 Finally, having a turing machine for each abacus instruction we need |
1234 Finally, having a Turing machine for each abacus instruction we need |
1235 to ``stitch'' the Turing machines together into one so that each |
1235 to ``stitch'' the Turing machines together into one so that each |
1236 Turing machine component transitions to next one, just like in |
1236 Turing machine component transitions to next one, just like in |
1237 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 |
1238 program is assumed to calculate a value stored in the last |
1238 program is assumed to calculate a value stored in the last |
1239 register. That means we have to append a Turing machine that |
1239 register. That means we have to append a Turing machine that |
1241 last number represented on the tape. |
1241 last number represented on the tape. |
1242 |
1242 |
1243 While generating the Turing machine program for an abacus |
1243 While generating the Turing machine program for an abacus |
1244 program is not too difficult to formalise, the problem is that it |
1244 program is not too difficult to formalise, the problem is that it |
1245 contains @{text Goto}s all over the place. The unfortunate result is |
1245 contains @{text Goto}s all over the place. The unfortunate result is |
1246 are needed to translate each abacus instructionthat we cannot |
1246 are needed to translate each abacus instruction that we cannot |
1247 use our Hoare-rules for reasoning about sequentially composed |
1247 use our Hoare-rules for reasoning about sequentially composed |
1248 programs. Instead we have to treat the Turing machine as one ``block'' |
1248 programs. Instead we have to treat the Turing machine as one |
|
1249 are needed to translate each abacus instruction``block'' |
1249 and show as invariant that it performs the same operations |
1250 and show as invariant that it performs the same operations |
1250 as the abacus program. For this we have to show that for each |
1251 as the abacus program. For this we have to show that for each |
1251 configuration of an abacus machine the @{term step}-function |
1252 configuration of an abacus machine the @{term step}-function |
1252 is simulated by zero or more steps in our constructed Turing |
1253 is simulated by zero or more steps in our constructed Turing |
1253 machine. |
1254 machine. This leads to a rather large ``monolithic'' overall |
1254 |
1255 correctness proof that on the conceptual level is difficult to |
1255 |
1256 break down into smaller components. |
|
1257 |
|
1258 %We were able to simplify the proof somewhat |
1256 *} |
1259 *} |
1257 |
1260 |
1258 |
1261 |
1259 section {* Recursive Functions *} |
1262 section {* Recursive Functions and a Universal Turing Machine *} |
1260 |
1263 |
|
1264 text {* |
|
1265 |
|
1266 *} |
|
1267 |
|
1268 (* |
1261 section {* Wang Tiles\label{Wang} *} |
1269 section {* Wang Tiles\label{Wang} *} |
1262 |
1270 |
1263 text {* |
1271 text {* |
1264 Used in texture mapings - graphics |
1272 Used in texture mapings - graphics |
1265 *} |
1273 *} |
1266 |
1274 *) |
1267 |
1275 |
1268 section {* Related Work *} |
1276 section {* Conclusion *} |
1269 |
1277 |
1270 text {* |
1278 text {* |
1271 We have formalised the main results from three chapters in the |
1279 We have formalised the main results from three chapters in the |
1272 textbook by Boolos et al \cite{Boolos87}. Following in the |
1280 textbook by Boolos et al \cite{Boolos87}. Following in the |
1273 footsteps of another paper \cite{Nipkow98} formalising the results |
1281 footsteps of another paper \cite{Nipkow98} formalising the results |
1280 to formalise argumants about decidability. |
1288 to formalise argumants about decidability. |
1281 |
1289 |
1282 |
1290 |
1283 The most closely related work is by Norrish \cite{Norrish11}, and |
1291 The most closely related work is by Norrish \cite{Norrish11}, and |
1284 Asperti and Ricciotti \cite{AspertiRicciotti12}. Norrish bases his |
1292 Asperti and Ricciotti \cite{AspertiRicciotti12}. Norrish bases his |
1285 approach on lambda-terms. For this he introduced a clever rewriting |
1293 approach on $\lambda$-terms. For this he introduced a clever rewriting |
1286 technology based on combinators and de-Bruijn indices for rewriting |
1294 technology based on combinators and de-Bruijn indices for rewriting |
1287 modulo $\beta$-equivalence (to keep it manageable) |
1295 modulo $\beta$-equivalence (to keep it manageable) |
1288 |
1296 |
1289 |
1297 |
1290 |
1298 |