equal
deleted
inserted
replaced
1212 \end{center} |
1212 \end{center} |
1213 |
1213 |
1214 \noindent |
1214 \noindent |
1215 This gives us a list of natural numbers specifying how many states |
1215 This gives us a list of natural numbers specifying how many states |
1216 are needed to translate each abacus instruction. This information |
1216 are needed to translate each abacus instruction. This information |
1217 is needed in order to calculate the state where the Turing program |
1217 is needed in order to calculate the state where the Turing machine program |
1218 code of one abacus instruction ends and the next starts. |
1218 of one abacus instruction ends and the next starts. |
1219 The @{text Goto} |
1219 The @{text Goto} |
1220 instruction is easiest to translate requiring only one state, namely |
1220 instruction is easiest to translate requiring only one state, namely |
1221 the Turing machine program: |
1221 the Turing machine program: |
1222 |
1222 |
1223 \begin{center} |
1223 \begin{center} |
1258 Turing machine component transitions to next one, just like in |
1258 Turing machine component transitions to next one, just like in |
1259 the abacus programs. One last problem to overcome is that an abacus |
1259 the abacus programs. One last problem to overcome is that an abacus |
1260 program is assumed to calculate a value stored in the last |
1260 program is assumed to calculate a value stored in the last |
1261 register (the one with the highest register). That means we have to append a Turing machine that |
1261 register (the one with the highest register). That means we have to append a Turing machine that |
1262 ``mops up'' the tape (cleaning all @{text Oc}s) except for the |
1262 ``mops up'' the tape (cleaning all @{text Oc}s) except for the |
1263 @{term Oc}s of the last number represented on the tape. This needs |
1263 @{term Oc}s of the last register represented on the tape. This needs |
1264 a Turing machine program with @{text "2 * R + 12"} states, assuming @{text R} |
1264 a Turing machine program with @{text "2 * R + 12"} states, assuming @{text R} |
1265 is the number of registers to be ``cleaned''. |
1265 is the number of registers to be ``cleaned''. |
1266 |
1266 |
1267 While generating the Turing machine program for an abacus program is |
1267 While generating the Turing machine program for an abacus program is |
1268 not too difficult to formalise, the problem is that it contains |
1268 not too difficult to formalise, the problem is that it contains |
1534 |
1534 |
1535 We therefore have formalised Turing machines in the first place and the main |
1535 We therefore have formalised Turing machines in the first place and the main |
1536 computability results from Chapters 3 to 8 in the textbook by Boolos |
1536 computability results from Chapters 3 to 8 in the textbook by Boolos |
1537 et al \cite{Boolos87}. For this we did not need to implement |
1537 et al \cite{Boolos87}. For this we did not need to implement |
1538 anything on the ML-level of Isabelle/HOL. While formalising the six chapters |
1538 anything on the ML-level of Isabelle/HOL. While formalising the six chapters |
1539 \cite{Boolos87} we have found an inconsistency in Boolos et al's |
1539 of \cite{Boolos87} we have found an inconsistency in Boolos et al's |
1540 definitions of what function a Turing machine calculates. In |
1540 definitions of what function a Turing machine calculates. In |
1541 Chapter 3 they use a definition that states a function is undefined |
1541 Chapter 3 they use a definition that states a function is undefined |
1542 if the Turing machine loops \emph{or} halts with a non-standard |
1542 if the Turing machine loops \emph{or} halts with a non-standard |
1543 tape. Whereas in Chapter 8 about the universal Turing machine, the |
1543 tape. Whereas in Chapter 8 about the universal Turing machine, the |
1544 Turing machines will \emph{not} halt unless the tape is in standard |
1544 Turing machines will \emph{not} halt unless the tape is in standard |