1 (*<*)

     1 (*<*)

     2 theory Paper

     2 theory Paper

     4 begin

     4 begin

     5 

     5 

     6 

     6 

     7 hide_const (open) s 

     7 hide_const (open) s 

     8 

     8 

  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   and the also the definition of the

  1359   and the also the definition of the

  1333   universal function (we refer the reader to our formalisation).

  1360   universal function (we refer the reader to our formalisation).

  1334 

  1361 

  1335   \cite[Page 32]{Boolos87}

  1362   \cite[Page 32]{Boolos87}

  1336 

  1363 

  1356   If started with @{term "([], [Oc])"} it halts with the

  1383   If started with @{term "([], [Oc])"} it halts with the

  1357   non-standard tape @{term "([Oc], [])"} according to the definition in Chap 3;

  1384   non-standard tape @{term "([Oc], [])"} according to the definition in Chap 3;

  1358   but with @{term "([], [Oc])"} according to def Chap 8

  1385   but with @{term "([], [Oc])"} according to def Chap 8

  1359 *}

  1386 *}

  1360 

  1387 

  1361 section {* XYZ *}

  1389 section {* XYZ *}

  1362 

  1390 

  1363 text {*

  1391 text {*

  1364 One of the main objectives of the paper is the construction and verification of Universal Turing machine (UTM). A UTM takes the code of any Turing machine $M$ and its arguments $a_1, a_2, \ldots, a_n$ as input and computes to the same effect as $M$ does on $a_1, a_2, \ldots, a_n$. That is to say:

  1392 One of the main objectives of the paper is the construction and verification of Universal Turing machine (UTM). A UTM takes the code of any Turing machine $M$ and its arguments $a_1, a_2, \ldots, a_n$ as input and computes to the same effect as $M$ does on $a_1, a_2, \ldots, a_n$. That is to say:

  1365 \begin{enumerate}

  1393 \begin{enumerate}

  1404 \[

  1432 \[

  1405 (0, [Bk, Oc], []) \rightsquigarrow (L, 0) \rightsquigarrow (0, [Bk], [Oc])

  1433 (0, [Bk, Oc], []) \rightsquigarrow (L, 0) \rightsquigarrow (0, [Bk], [Oc])

  1406 \]

  1434 \]

  1407 In summary, according to Chapter 3, the Turing machine in \eqref{contrived_tm} computes non-result and according to Chapter 8, it computes an identify function. 

  1435 In summary, according to Chapter 3, the Turing machine in \eqref{contrived_tm} computes non-result and according to Chapter 8, it computes an identify function. 

  1408 *}

  1436 *}

  1409 

  1438 

  1410 (*

  1439 (*

  1411 section {* Wang Tiles\label{Wang} *}

  1440 section {* Wang Tiles\label{Wang} *}

  1412 

  1441 

  1413 text {*

  1442 text {*

  1430   (for example the proof of Wang's tiling problem \cite{Robinson71}).

  1459   (for example the proof of Wang's tiling problem \cite{Robinson71}).

  1431 

  1460 

  1432   We therefore have formalised Turing machines and the main

  1461   We therefore have formalised Turing machines and the main

  1433   computability results from Chapters 3 to 8 in the textbook by Boolos

  1462   computability results from Chapters 3 to 8 in the textbook by Boolos

  1434   et al \cite{Boolos87}.  For this we did not need to implement

  1463   et al \cite{Boolos87}.  For this we did not need to implement

  1436   \cite{Boolos87} we have found an inconsistency in Bolos et al's 

  1465   \cite{Boolos87} we have found an inconsistency in Bolos et al's 

  1437   definitions of what function a Turing machine calculates. In

  1466   definitions of what function a Turing machine calculates. In

  1438   Chapter 3 they use a definition that states a function is undefined

  1467   Chapter 3 they use a definition that states a function is undefined

  1439   if the Turing machine loops \emph{or} halts with a non-standard

  1468   if the Turing machine loops \emph{or} halts with a non-standard

  1440   tape. Whereas in Chapter 8 about the universal Turing machine, the

  1469   tape. Whereas in Chapter 8 about the universal Turing machine, the

  1441   Turing machines will \emph{not} halt unless the tape is in standard

  1470   Turing machines will \emph{not} halt unless the tape is in standard

  1445   Right''. We have not attempted to formalise everything precisely as

  1473   Right''. We have not attempted to formalise everything precisely as

  1446   Boolos et al present it, but use definitions that make our

  1474   Boolos et al present it, but use definitions that make our

  1447   mechanised proofs manageable. For example our definition of the

  1475   mechanised proofs manageable. For example our definition of the

  1448   halting state performing @{term Nop}-operations seems to be

  1476   halting state performing @{term Nop}-operations seems to be

  1449   non-standard, but very much suited to a formalisation in a theorem

  1477   non-standard, but very much suited to a formalisation in a theorem

  1455   \cite[Page 310]{Norrish11}. While $\lambda$-terms indeed lead to

  1484   \cite[Page 310]{Norrish11}. While $\lambda$-terms indeed lead to

  1456   some slick mechanised proofs, our experience is that Turing machines

  1485   some slick mechanised proofs, our experience is that Turing machines

  1457   are not too daunting if one is only concerned with formalising the

  1486   are not too daunting if one is only concerned with formalising the

  1458   undecidability of the halting problem for Turing machines.  This

  1487   undecidability of the halting problem for Turing machines.  This

  1459   took us around 1500 loc of Isar-proofs, which is just one-and-a-half

  1488   took us around 1500 loc of Isar-proofs, which is just one-and-a-half

  1460   times of a mechanised proof pearl about the Myhill-Nerode

  1489   times of a mechanised proof pearl about the Myhill-Nerode

  1463   involved with constructing a universal Turing machine via recursive

  1492   involved with constructing a universal Turing machine via recursive

  1465   one wants to undertake too many times (our formalisation of abacus

  1494   one wants to undertake too many times (our formalisation of abacus

  1466   machines and their correct translation is approximately 4300 loc;

  1495   machines and their correct translation is approximately 4300 loc;

  1468   

  1497   

  1469   Our work was also very much inspired by the formalisation of Turing

  1498   Our work was also very much inspired by the formalisation of Turing

  1470   machines by Asperti and Ricciotti \cite{AspertiRicciotti12} in the

  1499   machines by Asperti and Ricciotti \cite{AspertiRicciotti12} in the

  1471   Matita theorem prover. It turns out that their notion of

  1500   Matita theorem prover. It turns out that their notion of

  1472   realisability and our Hoare-triples are very similar, however we

  1501   realisability and our Hoare-triples are very similar, however we

  1479   for them.

  1508   for them.

  1480   

  1509   

  1481   For us the most interesting aspect of our work are the correctness

  1510   For us the most interesting aspect of our work are the correctness

  1482   proofs for Turing machines. Informal presentations of computability

  1511   proofs for Turing machines. Informal presentations of computability

  1483   theory often leave the constructions of particular Turing machines

  1512   theory often leave the constructions of particular Turing machines

  1485   it to be just a chore. However, as far as we are aware all informal

  1514   it to be just a chore. However, as far as we are aware all informal

  1486   presentations leave out any arguments why these Turing machines

  1515   presentations leave out any arguments why these Turing machines

  1488   with the task of finding appropriate invariants and measures for

  1517   with the task of finding appropriate invariants and measures for

  1489   showing correctness and termination of these Turing machines.

  1518   showing correctness and termination of these Turing machines.

  1490   Whenever we can use Hoare-style reasoning, the invariants are

  1519   Whenever we can use Hoare-style reasoning, the invariants are

  1491   relatively straightforward and much smaller than for example the

  1520   relatively straightforward and much smaller than for example the

  1492   invariants used by Myreen in a correctness proof of a garbage collector

  1521   invariants used by Myreen in a correctness proof of a garbage collector

  1494   needed for the abacus proof, where Hoare-style reasoning does not work, is

  1523   needed for the abacus proof, where Hoare-style reasoning does not work, is

  1495   similar in size as the one by Myreen and finding a sufficiently

  1524   similar in size as the one by Myreen and finding a sufficiently

  1496   strong one took us, like Myreen for his, something on the magnitude of

  1525   strong one took us, like Myreen for his, something on the magnitude of

  1497   weeks.

  1526   weeks.

  1498 

  1527 

  1499   Our reasoning about the invariants is not much supported by the

  1528   Our reasoning about the invariants is not much supported by the

  1501   between our work and very recent work \cite{Jensen13} on verifying

  1531   between our work and very recent work \cite{Jensen13} on verifying

  1503   programs that Hoare-style reasoning is sometimes possible, but

  1533   programs that Hoare-style reasoning is sometimes possible, but

  1505   introduced a more primitive specification logic, on which

  1535   introduced a more primitive specification logic, on which

  1506   Hoare-rules can be provided for special cases.  It remains to be

  1536   Hoare-rules can be provided for special cases.  It remains to be

  1507   seen whether their specification logic for assembly code can make it

  1537   seen whether their specification logic for assembly code can make it

  1508   easier to reason about our Turing programs. That would be an

  1538   easier to reason about our Turing programs. That would be an

  1509   attractive result, because Turing machine programs are very much

  1539   attractive result, because Turing machine programs are very much

  1512   verification. In order to try out such ideas, our formalisation provides the

  1542   verification. In order to try out such ideas, our formalisation provides the

  1513   ``playground''. The code of our formalisation is available from the

  1543   ``playground''. The code of our formalisation is available from the

  1516 *}

  1545 *}

  1517 

  1546 

  1518 

  1547 

  1519 

  1548 

  1520 (*<*)

  1549 (*<*)