1328 means that if the recursive function @{text r} with arguments @{text ns} evaluates |
1328 means that if the recursive function @{text r} with arguments @{text ns} evaluates |
1329 to @{text n}, then the translated Turing machine if started |
1329 to @{text n}, then the translated Turing machine if started |
1330 with the standard tape @{term "([Bk, Bk], <ns::nat list>)"} will terminate |
1330 with the standard tape @{term "([Bk, Bk], <ns::nat list>)"} will terminate |
1331 with the standard tape @{term "(Bk \<up> k, <n::nat> @ Bk \<up> l)"} for some @{text k} and @{text l}. |
1331 with the standard tape @{term "(Bk \<up> k, <n::nat> @ Bk \<up> l)"} for some @{text k} and @{text l}. |
1332 |
1332 |
1333 Having recursive functions under our belt, we can construct an universal |
1333 Having recursive functions under our belt, we can construct a universal |
1334 function and consider its translated (universal) Turing machine, written @{term UTM}. |
1334 function, written @{text UF}. This universal function acts like an interpreter for Turing machines. |
|
1335 It takes two arguments: one is the code of the Turing machine to be interpreted and the |
|
1336 other is the ``packed version'' of the arguments of the Turing machine. |
|
1337 We can then consider how this universal function is translated to a |
|
1338 Turing machine and from this construct the universal Turing machine, |
|
1339 written @{term UTM}. @{text UTM} is defined as |
|
1340 the composition of the Turing machine that packages the arguments and |
|
1341 the translated recursive |
|
1342 function @{text UF}: |
|
1343 |
|
1344 \begin{center} |
|
1345 @{text "UTM \<equiv> arg_coding \<oplus> (translate UF)"} |
|
1346 \end{center} |
|
1347 |
|
1348 \noindent |
1335 Suppose |
1349 Suppose |
1336 a Turing program @{term p} is well-formed and when started with the standard |
1350 a Turing program @{term p} is well-formed and when started with the standard |
1337 tape containing the arguments @{term args}, will produce a standard tape |
1351 tape containing the arguments @{term args}, will produce a standard tape |
1338 with ``output'' @{term n}. This assumption can be written as the |
1352 with ``output'' @{term n}. This assumption can be written as the |
1339 Hoare-triple |
1353 Hoare-triple |
1341 \begin{center} |
1355 \begin{center} |
1342 @{thm (prem 3) UTM_halt_lemma2} |
1356 @{thm (prem 3) UTM_halt_lemma2} |
1343 \end{center} |
1357 \end{center} |
1344 |
1358 |
1345 \noindent |
1359 \noindent |
1346 where we assume the @{term args} stand for a non-empty list. Then the universal Turing |
1360 where we require that the @{term args} stand for a non-empty list. Then the universal Turing |
1347 machine @{term UTM} started with the code of @{term p} and the arguments |
1361 machine @{term UTM} started with the code of @{term p} and the arguments |
1348 @{term args} calculates the same result, namely |
1362 @{term args}, calculates the same result, namely |
1349 |
1363 |
1350 \begin{center} |
1364 \begin{center} |
1351 @{thm (concl) UTM_halt_lemma2} |
1365 @{thm (concl) UTM_halt_lemma2} |
1352 \end{center} |
1366 \end{center} |
1353 |
1367 |
1500 In previous works we were unable to formalise results about |
1514 In previous works we were unable to formalise results about |
1501 computability because in Isabelle/HOL we cannot represent the |
1515 computability because in Isabelle/HOL we cannot represent the |
1502 decidability of a predicate @{text P}, say, as the formula @{term "P |
1516 decidability of a predicate @{text P}, say, as the formula @{term "P |
1503 \<or> \<not>P"}. For reasoning about computability we need to formalise a |
1517 \<or> \<not>P"}. For reasoning about computability we need to formalise a |
1504 concrete model of computations. We could have followed Norrish |
1518 concrete model of computations. We could have followed Norrish |
1505 \cite{Norrish11} using the $\lambda$-calculus as the starting point, |
1519 \cite{Norrish11} using the $\lambda$-calculus as the starting point for computability theory, |
1506 but then we would have to reimplement his infrastructure for |
1520 but then we would have to reimplement his infrastructure for |
1507 reducing $\lambda$-terms on the ML-level. We would still need to |
1521 reducing $\lambda$-terms on the ML-level. We would still need to |
1508 connect his work to Turing machines for proofs that make essential use of them |
1522 connect his work to Turing machines for proofs that make essential use of them |
1509 (for example the proof of Wang's tiling problem \cite{Robinson71}). |
1523 (for example the undecidability proof for Wang's tiling problem \cite{Robinson71}). |
1510 |
1524 |
1511 We therefore have formalised Turing machines and the main |
1525 We therefore have formalised Turing machines and the main |
1512 computability results from Chapters 3 to 8 in the textbook by Boolos |
1526 computability results from Chapters 3 to 8 in the textbook by Boolos |
1513 et al \cite{Boolos87}. For this we did not need to implement |
1527 et al \cite{Boolos87}. For this we did not need to implement |
1514 anything on the ML-level of Isabelle/HOL. While formalising the six chapters |
1528 anything on the ML-level of Isabelle/HOL. While formalising the six chapters |