1327 means that if the recursive function @{text r} with arguments @{text ns} evaluates |
1327 means that if the recursive function @{text r} with arguments @{text ns} evaluates |
1328 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 |
1329 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 |
1330 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}. |
1331 |
1331 |
1332 Having |
1332 Having recursive functions under our belt, we can construct an universal |
1333 |
1333 function and consider the translated (universal) Turing machine @{term UTM}. |
1334 we can prove that if |
1334 Suppose |
|
1335 a Turing program is well-formed and @{term p} when started with the standard |
|
1336 tape containing the arguments @{term arg}, produces a standard tape |
|
1337 with ``output'' @{term n}. This assumption can be written as the |
|
1338 Hoare-triple |
1335 |
1339 |
1336 \begin{center} |
1340 \begin{center} |
1337 @{thm (prem 3) UTM_halt_lemma2} |
1341 @{thm (prem 3) UTM_halt_lemma2} |
1338 \end{center} |
1342 \end{center} |
1339 then |
1343 |
|
1344 \noindent |
|
1345 where we assume the @{term args} are non-empty, then the universal Turing |
|
1346 machine @{term UTM} started with the code of @{term p} and the arguments |
|
1347 @{term args} calculates the same result: |
1340 |
1348 |
1341 \begin{center} |
1349 \begin{center} |
1342 @{thm (concl) UTM_halt_lemma2} |
1350 @{thm (concl) UTM_halt_lemma2} |
1343 \end{center} |
1351 \end{center} |
1344 |
1352 |
1345 under the assumption that @{text p} |
1353 \noindent |
1346 is well-formed and the arguments are not empty. |
1354 Similarly, if a Turing program @{term p} started with the |
1347 |
1355 standard tape containing @{text args} loops, which is represented |
|
1356 by the Hoare-pair |
1348 |
1357 |
1349 \begin{center} |
1358 \begin{center} |
1350 @{thm (prem 2) UTM_unhalt_lemma2} |
1359 @{thm (prem 2) UTM_unhalt_lemma2} |
1351 \end{center} |
1360 \end{center} |
1352 then |
1361 |
|
1362 \noindent |
|
1363 then the universal Turing machine started with the code of @{term p} and the arguments |
|
1364 @{term args} will also loop |
1353 |
1365 |
1354 \begin{center} |
1366 \begin{center} |
1355 @{thm (concl) UTM_unhalt_lemma2} |
1367 @{thm (concl) UTM_unhalt_lemma2} |
1356 \end{center} |
1368 \end{center} |
1357 |
1369 |
1358 |
1370 \noindent |
1359 and the also the definition of the |
1371 While formalising the chapter about universal Turing machines in \cite{Boolos87} |
1360 universal function (we refer the reader to our formalisation). |
1372 we noticed that they use their definition about what function Turing machines |
1361 |
1373 calculate. They write in Chapter 3 \cite[Page 32]{Boolos87}: |
1362 \cite[Page 32]{Boolos87} |
|
1363 |
1374 |
1364 \begin{quote}\it |
1375 \begin{quote}\it |
1365 ``If the function that is to be computed assigns no value to the arguments that |
1376 ``If the function that is to be computed assigns no value to the arguments that |
1366 are represented initially on the tape, then the machine either will never halt, |
1377 are represented initially on the tape, then the machine either will never halt, |
1367 or will halt in some nonstandard configuration\ldots'' |
1378 or will halt in some nonstandard configuration\ldots'' |
1368 \end{quote} |
1379 \end{quote} |
1369 |
1380 |
|
1381 \noindent |
|
1382 Interestingly, they do not implement this definition when considering |
|
1383 their universal Turing machine. |
|
1384 |
1370 This means that if you encode the plus function but only give one argument, |
1385 This means that if you encode the plus function but only give one argument, |
1371 then the TM will either loop {\bf or} stop with a non-standard tape |
1386 then the TM will either loop {\bf or} stop with a non-standard tape |
1372 |
1387 |
1373 But in the definition of the universal function the TMs will never stop |
1388 But in the definition of the universal function the TMs will never stop |
1374 with non-standard tapes. |
1389 with non-standard tapes. |