1209 |
1209 |
1210 \noindent |
1210 \noindent |
1211 This gives us a list of natural numbers specifying how many states |
1211 This gives us a list of natural numbers specifying how many states |
1212 are needed to translate each abacus instruction. This information |
1212 are needed to translate each abacus instruction. This information |
1213 is needed in order to calculate the state where the Turing program |
1213 is needed in order to calculate the state where the Turing program |
1214 code of one abacus instruction ends. |
1214 code of one abacus instruction ends and the next starts. |
1215 The @{text Goto} |
1215 The @{text Goto} |
1216 instruction is easiest to translate requiring only one state, namely |
1216 instruction is easiest to translate requiring only one state, namely |
1217 the Turing machine program: |
1217 the Turing machine program: |
1218 |
1218 |
1219 \begin{center} |
1219 \begin{center} |
1220 @{text "tm_of_Goto l"} @{text "\<equiv>"} @{thm (rhs) tgoto.simps[where n="l"]} |
1220 @{text "translate_Goto l"} @{text "\<equiv>"} @{thm (rhs) tgoto.simps[where n="l"]} |
1221 \end{center} |
1221 \end{center} |
1222 |
1222 |
1223 \noindent |
1223 \noindent |
1224 where @{term "l"} is the state in the Turing machine program |
1224 where @{term "l"} is the state in the Turing machine program |
1225 to jump to. For translating the instruction @{term "Inc R\<iota>"}, |
1225 to jump to. For translating the instruction @{term "Inc R\<iota>"}, |
1237 \end{tabular} |
1237 \end{tabular} |
1238 \end{center} |
1238 \end{center} |
1239 |
1239 |
1240 \noindent |
1240 \noindent |
1241 Then we need to increase the ``number'' on the tape by one, |
1241 Then we need to increase the ``number'' on the tape by one, |
1242 and adjust the following ``registers''. By adjusting we only need to |
1242 and adjust the following ``registers''. For adjusting we only need to |
1243 change the first @{term Oc} of each number to @{term Bk} and the last |
1243 change the first @{term Oc} of each number to @{term Bk} and the last |
1244 one from @{term Bk} to @{term Oc}. |
1244 one from @{term Bk} to @{term Oc}. |
1245 Finally, we need to transition the head of the |
1245 Finally, we need to transition the head of the |
1246 Turing machine back into the standard position. This requires a Turing machine |
1246 Turing machine back into the standard position. This requires a Turing machine |
1247 with 9 states (we omit the details). Similarly for the translation of @{term "Dec R\<iota> l"}, where the |
1247 with 9 states (we omit the details). Similarly for the translation of @{term "Dec R\<iota> l"}, where the |
1285 easily construct a universal Turing machine via a universal |
1285 easily construct a universal Turing machine via a universal |
1286 function. This is different from Norrish \cite{Norrish11} who gives a universal |
1286 function. This is different from Norrish \cite{Norrish11} who gives a universal |
1287 function for Church numbers, and also from Asperti and Ricciotti |
1287 function for Church numbers, and also from Asperti and Ricciotti |
1288 \cite{AspertiRicciotti12} who construct a universal Turing machine |
1288 \cite{AspertiRicciotti12} who construct a universal Turing machine |
1289 directly, but for simulating Turing machines with a more restricted alphabet. |
1289 directly, but for simulating Turing machines with a more restricted alphabet. |
1290 \emph{Recursive functions} @{term r} are defined as the datatype |
1290 \emph{Recursive functions} are defined as the datatype |
1291 |
1291 |
1292 \begin{center} |
1292 \begin{center} |
1293 \begin{tabular}{c@ {\hspace{4mm}}c} |
1293 \begin{tabular}{c@ {\hspace{4mm}}c} |
1294 \begin{tabular}{rcl@ {\hspace{4mm}}l} |
1294 \begin{tabular}{rcl@ {\hspace{4mm}}l} |
1295 @{term r} & @{text "::="} & @{term z} & (zero-functions)\\ |
1295 @{term r} & @{text "::="} & @{term z} & (zero-functions)\\ |
1312 relates a recursive function @{text r} and a list @{term ns} of natural numbers of length @{text l}, |
1312 relates a recursive function @{text r} and a list @{term ns} of natural numbers of length @{text l}, |
1313 to what the result of the recursive function is, say @{text n}---we omit the straightforward |
1313 to what the result of the recursive function is, say @{text n}---we omit the straightforward |
1314 definition of @{term "rec_calc_rel r ns n"}. Because of space reasons, we also omit the |
1314 definition of @{term "rec_calc_rel r ns n"}. Because of space reasons, we also omit the |
1315 definition of translating |
1315 definition of translating |
1316 recursive functions into abacus programs. We can prove the following |
1316 recursive functions into abacus programs. We can prove the following |
1317 theorem about the translation: Assuming |
1317 theorem about the translation: If |
1318 @{thm (prem 1) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and r="n"]} |
1318 @{thm (prem 1) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and r="n"]} |
1319 then the following Hoare-triple holds |
1319 holds for the recursive function @{text r}, then the following Hoare-triple holds |
1320 |
1320 |
1321 \begin{center} |
1321 \begin{center} |
1322 @{thm (concl) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and r="n"]} |
1322 @{thm (concl) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and r="n"]} |
1323 \end{center} |
1323 \end{center} |
1324 |
1324 |
1325 \noindent |
1325 \noindent |
1326 which means that if the recursive function @{text r} with arguments @{text ns} evaluates |
1326 for the Turing machine. This |
|
1327 means that if the recursive function @{text r} with arguments @{text ns} evaluates |
1327 to @{text n}, then the corresponding Turing machine @{term "tm_of_rec r"} if started |
1328 to @{text n}, then the corresponding Turing machine @{term "tm_of_rec r"} if started |
1328 with the standard tape @{term "([Bk, Bk], <ns::nat list>)"} will terminate |
1329 with the standard tape @{term "([Bk, Bk], <ns::nat list>)"} will terminate |
1329 with the standard tape @{term "(Bk \<up> k, <n::nat> @ Bk \<up> l)"} for some @{text k} and @{text l}. |
1330 with the standard tape @{term "(Bk \<up> k, <n::nat> @ Bk \<up> l)"} for some @{text k} and @{text l}. |
1330 |
1331 |
1331 and the also the definition of the |
1332 and the also the definition of the |