# HG changeset patch # User Christian Urban # Date 1360068060 0 # Node ID 1ce74a77fa2a58563107a97c3dc1ad7b1d056a11 # Parent bda7145322637e71449eb243b35ad2fb088b3d46 conclusion diff -r bda714532263 -r 1ce74a77fa2a Paper/Paper.thy --- a/Paper/Paper.thy Tue Feb 05 10:23:08 2013 +0000 +++ b/Paper/Paper.thy Tue Feb 05 12:41:00 2013 +0000 @@ -1278,53 +1278,82 @@ We have formalised the main results from three chapters in the textbook by Boolos et al \cite{Boolos87}. Following in the footsteps of another paper \cite{Nipkow98} formalising the results - from a textbook, we could have titled our paper ``Boolos et al are + from a semantics textbook, we could have titled our paper ``Boolos et al are (almost) Right''. We have not attempted to formalise everything - precisely as Boolos et al present it, but find definitions that make - mechanised proofs manageable. We have found a small inconsitency in - the usage of definitions of \ldots Our interest in this subject + precisely as Boolos et al present it, but use definitions that make + mechanised proofs manageable. For example our definition of the + halting state performing @{term Nop}-operations seems to be non-standard, + but very much suited to a formalisation in a theorem prover where + the @{term steps}-function need to be total. We have found an + inconsitency in + Bolos et al's usage of definitions of \ldots + Our interest in Turing machines arose from correctness proofs about algorithms where we were unable - to formalise argumants about decidability. - + to formalise arguments about decidability but also undecidability + proofs in general (for example Wang's tiling problem \cite{Robinson71}). The most closely related work is by Norrish \cite{Norrish11}, and - Asperti and Ricciotti \cite{AspertiRicciotti12}. Norrish bases his - approach on $\lambda$-terms. For this he introduced a clever rewriting - technology based on combinators and de-Bruijn indices for rewriting - modulo $\beta$-equivalence (to keep it manageable) - - - - \noindent - Later on we need to consider specific Turing machines that - start with a tape in standard form and halt the computation - in standard form. To define a tape in standard form, it is - useful to have an operation %@{ term "tape_of_nat_list DUMMY"} - that translates lists of natural numbers into tapes. - + Asperti and Ricciotti \cite{AspertiRicciotti12}. Norrish formalises + computability theory using $\lambda$-terms. For this he introduced a + clever rewriting technology based on combinators and de-Bruijn + indices for rewriting modulo $\beta$-equivalence (in order to avoid + explicit $\alpha$-renamings). He mentions that formalising Turing + machines would be a ``daunting prospect'' \cite[Page + 310]{Norrish11}. While $\lambda$-terms indeed lead to some slick + mechanised proofs, our experience is that Turing machines are not + too daunting if one is only concerned with formalising the + undecidability of the halting problem for Turing machines. This + took us around 1500 loc of Isar-proofs, which is just one-and-a-half + times longer than a mechanised proof pearl about the Myhill-Nerode + theorem. So our conclusion is it not as daunting as we imagined + reading the paper by Norrish \cite{Norrish11}. The work involved + with constructing a universial Turing machine via recursive + functions and abacus machines, on the other hand, is not a + project one wants to undertake too many times (our formalisation + of abacus machines and their correct translation is approximately + 4300 loc; \ldots) - \noindent - This means the Turing machine starts with a tape containg @{text n} @{term Oc}s - and the head pointing to the first one; the Turing machine - halts with a tape consisting of some @{term Bk}s, followed by a - ``cluster'' of @{term Oc}s and after that by some @{term Bk}s. - The head in the output is pointing again at the first @{term Oc}. - The intuitive meaning of this definition is to start the Turing machine with a - tape corresponding to a value @{term n} and producing - a new tape corresponding to the value @{term l} (the number of @{term Oc}s - clustered on the output tape). + Our work was also very much inspired by the formalisation of Turing + machines by Asperti and Ricciotti \cite{AspertiRicciotti12} in the + Matita theorem prover. It turns out that their notion of + realisability and our Hoare-triples are very similar, however we + differ in some basic definitions for Turing machines. Asperti and + Ricciotti are interested in providing a mechanised foundation for + complexity theory. They formalised a universial Turing machine + (which differs from ours by using a more general alphabet), but did + not describe an undecidability proof. Given their definitions and + infrastructure, we expect this should not be too difficult for them. + + For us the most interesting aspect of our work are the correctness + proofs for some Turing machines. Informal presentation of computability + theory often leave the constructions of particular Turing machines + as excercise to the reader, as \cite{Boolos87} for example, deeming it + too easy for wasting space. However, as far as we are aware all + informal presentation leave out any correctness proofs---do the + Turing machines really perform the task they are supposed to do. + This means we have to find appropriate invariants and measures + that can be establised for showing correctness and termination. + Whenever we can use Hoare-style reasoning, the invariants are + relatively straightforward and much smaller than for example + the invariants by Myreen for a correctness proof of a garbage + collector \cite[Page 76]{}. The invariant needed for the abacus proof, + where Hoare-style reasoning does not work, is similar in size as + the one by Myreen and finding a sufficiently strong one took + us, like Myreen, something on the magnitute of weeks. - - - Magnus: invariants -- Section 5.4.5 on page 75. - - - There is a tantalising connection with recent work \cite{Jensen13} - about verifying X86 assembly code. They observed + Our reasoning about the invariants is also not very much + supported by the automation in Isabelle. There is however a tantalising + connection between our work and recent work \cite{Jensen13} + on verifying X86 assembly code. They observed a similar phenomenon + with assmebly programs that Hoare-style reasoning is sometimes + possible, but sometimes not. In order to ease their reasoning they + introduced a more primitive specification logic, on which + for special cases Hoare-rules can be provided. It remains to be seen whether their specification logic for assmebly code can make it easier to reason about our Turing programs. - + The code of our formalisation is available from the Mercurial repository at + \url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/tm/} *} diff -r bda714532263 -r 1ce74a77fa2a paper.pdf Binary file paper.pdf has changed