1218 |
1218 |
1219 \noindent |
1219 \noindent |
1220 This gives us a list of natural numbers specifying how many states |
1220 This gives us a list of natural numbers specifying how many states |
1221 are needed to translate each abacus instruction. This information |
1221 are needed to translate each abacus instruction. This information |
1222 is needed in order to calculate the state where the Turing machine program |
1222 is needed in order to calculate the state where the Turing machine program |
1223 of one abacus instruction ends and the next starts. |
1223 of one abacus instruction starts. |
|
1224 |
|
1225 {\it add something here about address} |
|
1226 |
1224 The @{text Goto} |
1227 The @{text Goto} |
1225 instruction is easiest to translate requiring only one state, namely |
1228 instruction is easiest to translate requiring only one state, namely |
1226 the Turing machine program: |
1229 the Turing machine program: |
1227 |
1230 |
1228 \begin{center} |
1231 \begin{center} |
1313 \end{tabular} |
1316 \end{tabular} |
1314 \end{center} |
1317 \end{center} |
1315 |
1318 |
1316 \noindent |
1319 \noindent |
1317 where @{text n} indicates the function expects @{term n} arguments |
1320 where @{text n} indicates the function expects @{term n} arguments |
1318 (@{text z} and @{term s} expect one argument), and @{text rs} stands |
1321 (in \cite{Boolos87} both @{text z} and @{term s} expect one |
1319 for a list of recursive functions. Since we know in each case |
1322 argument), and @{text rs} stands for a list of recursive |
1320 the arity, say @{term l}, we can define an inductive evaluation relation that |
1323 functions. Since we know in each case the arity, say @{term l}, we |
1321 relates a recursive function @{text r} and a list @{term ns} of natural numbers of length @{text l}, |
1324 can define an inductive evaluation relation that relates a recursive |
1322 to what the result of the recursive function is, say @{text n}. We omit the |
1325 function @{text r} and a list @{term ns} of natural numbers of |
1323 definition of @{term "rec_calc_rel r ns n"}. Because of space reasons, we also omit the |
1326 length @{text l}, to what the result of the recursive function is, |
1324 definition of translating |
1327 say @{text n}. We omit the definition of @{term "rec_calc_rel r ns |
1325 recursive functions into abacus programs. We can prove, however, the following |
1328 n"}. Because of space reasons, we also omit the definition of |
1326 theorem about the translation: If |
1329 translating recursive functions into abacus programs. We can prove, |
1327 @{thm (prem 1) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and r="n"]} |
1330 however, the following theorem about the translation: If @{thm (prem |
1328 holds for the recursive function @{text r}, then the following Hoare-triple holds |
1331 1) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and |
|
1332 r="n"]} holds for the recursive function @{text r}, then the |
|
1333 following Hoare-triple holds |
1329 |
1334 |
1330 \begin{center} |
1335 \begin{center} |
1331 @{thm (concl) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and r="n"]} |
1336 @{thm (concl) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and r="n"]} |
1332 \end{center} |
1337 \end{center} |
1333 |
1338 |