1281   from a textbook, we could have titled our paper ``Boolos et al are

  1281   from a semantics textbook, we could have titled our paper ``Boolos et al are

  1283   precisely as Boolos et al present it, but find definitions that make

  1283   precisely as Boolos et al present it, but use definitions that make

  1284   mechanised proofs manageable. We have found a small inconsitency in

  1284   mechanised proofs manageable. For example our definition of the 

  1285   the usage of definitions of \ldots Our interest in this subject

  1285   halting state performing @{term Nop}-operations seems to be non-standard, 

  1286   but very much suited to a formalisation in a theorem prover where

  1287   the @{term steps}-function need to be total. We have found an 

  1288   inconsitency in

  1289   Bolos et al's usage of definitions of \ldots 

  1290   Our interest in Turing machines 

  1287   to formalise argumants about decidability.

  1292   to formalise arguments about decidability but also undecidability

  1288 

  1293   proofs in general (for example Wang's tiling problem \cite{Robinson71}).

  1291   Asperti and Ricciotti \cite{AspertiRicciotti12}. Norrish bases his

  1296   Asperti and Ricciotti \cite{AspertiRicciotti12}. Norrish formalises

  1292   approach on $\lambda$-terms. For this he introduced a clever rewriting

  1297   computability theory using $\lambda$-terms. For this he introduced a

  1293   technology based on combinators and de-Bruijn indices for rewriting

  1298   clever rewriting technology based on combinators and de-Bruijn

  1294   modulo $\beta$-equivalence (to keep it manageable)

  1299   indices for rewriting modulo $\beta$-equivalence (in order to avoid

  1295 

  1300   explicit $\alpha$-renamings). He mentions that formalising Turing

  1296 

  1301   machines would be a ``daunting prospect'' \cite[Page

  1297 

  1302   310]{Norrish11}. While $\lambda$-terms indeed lead to some slick

  1298   \noindent

  1303   mechanised proofs, our experience is that Turing machines are not

  1299   Later on we need to consider specific Turing machines that 

  1304   too daunting if one is only concerned with formalising the

  1300   start with a tape in standard form and halt the computation

  1305   undecidability of the halting problem for Turing machines.  This

  1301   in standard form. To define a tape in standard form, it is

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

  1302   useful to have an operation %@{ term "tape_of_nat_list DUMMY"} 

  1307   times longer than a mechanised proof pearl about the Myhill-Nerode

  1303   that translates lists of natural numbers into tapes. 

  1308   theorem. So our conclusion is it not as daunting as we imagined

  1304 

  1309   reading the paper by Norrish \cite{Norrish11}. The work involved

  1310   with constructing a universial Turing machine via recursive 

  1311   functions and abacus machines, on the other hand, is not a

  1312   project one wants to undertake too many times (our formalisation

  1313   of abacus machines and their correct translation is approximately 

  1314   4300 loc; \ldots)

  1306   \noindent

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

  1307   This means the Turing machine starts with a tape containg @{text n} @{term Oc}s

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

  1308   and the head pointing to the first one; the Turing machine

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

  1309   halts with a tape consisting of some @{term Bk}s, followed by a 

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

  1310   ``cluster'' of @{term Oc}s and after that by some @{term Bk}s.

  1320   differ in some basic definitions for Turing machines. Asperti and

  1311   The head in the output is pointing again at the first @{term Oc}.

  1321   Ricciotti are interested in providing a mechanised foundation for

  1312   The intuitive meaning of this definition is to start the Turing machine with a

  1322   complexity theory. They formalised a universial Turing machine

  1313   tape corresponding to a value @{term n} and producing

  1323   (which differs from ours by using a more general alphabet), but did

  1314   a new tape corresponding to the value @{term l} (the number of @{term Oc}s

  1324   not describe an undecidability proof. Given their definitions and

  1315   clustered on the output tape).

  1325   infrastructure, we expect this should not be too difficult for them.

  1316 

  1317 

  1319   Magnus: invariants -- Section 5.4.5 on page 75.

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

  1320 

  1328   proofs for some Turing machines. Informal presentation of computability

  1321 

  1329   theory often leave the constructions of particular Turing machines

  1322   There is a tantalising connection with recent work \cite{Jensen13}

  1330   as excercise to the reader, as \cite{Boolos87} for example, deeming it 

  1323   about verifying X86 assembly code. They observed 

  1331   too easy for wasting space. However, as far as we are aware all

  1332   informal presentation leave out any correctness proofs---do the 

  1333   Turing machines really perform the task they are supposed to do. 

  1334   This means we have to find appropriate invariants and measures

  1335   that can be establised for showing correctness and termination.

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

  1337   relatively straightforward and much smaller than for example 

  1338   the invariants by Myreen for a correctness proof of a garbage

  1339   collector \cite[Page 76]{}. The invariant needed for the abacus proof,

  1340   where Hoare-style reasoning does not work, is similar in size as 

  1341   the one by Myreen and finding a sufficiently strong one took

  1342   us, like Myreen, something on the magnitute of weeks. 

  1343 

  1344   Our reasoning about the invariants is also not very much 

  1345   supported by the automation in Isabelle. There is however a tantalising 

  1346   connection between our work and recent work \cite{Jensen13}

  1347   on verifying X86 assembly code. They observed a similar phenomenon

  1348   with assmebly programs that Hoare-style reasoning is sometimes

  1349   possible, but sometimes not. In order to ease their reasoning they

  1350   introduced a more primitive specification logic, on which

  1351   for special cases Hoare-rules can be provided.

  1327   

  1355   The code of our formalisation is available from the Mercurial repository at

  1356   \url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/tm/}