# HG changeset patch # User Christian Urban <christian dot urban at kcl dot ac dot uk> # Date 1360159578 0 # Node ID 7fa1b8e88d76f53d0705033e4c18c76054f3ece2 # Parent 36d7c284a38d5d28d739226d683f06047d044749 updated diff -r 36d7c284a38d -r 7fa1b8e88d76 Paper/Paper.thy --- a/Paper/Paper.thy Wed Feb 06 13:28:01 2013 +0000 +++ b/Paper/Paper.thy Wed Feb 06 14:06:18 2013 +0000 @@ -1366,23 +1366,23 @@ text {* In previous works we were unable to formalise results about - computability because in a Isabelle/HOL we cannot represent the + computability because in Isabelle/HOL we cannot represent the decidability of a predicate @{text P}, say, as the formula @{term "P \<or> \<not>P"}. For reasoning about computability we need to formalise a concrete model of computations. We could have followed Norrish \cite{Norrish11} using the $\lambda$-calculus as the starting point, but then we would have to reimplement his infrastructure for reducing $\lambda$-terms on the ML-level. We would still need to - connect his work to Turing machines for proofs that make use of them + connect his work to Turing machines for proofs that make essential use of them (for example the proof of Wang's tiling problem \cite{Robinson71}). We therefore have formalised Turing machines and the main computability results from Chapters 3 to 8 in the textbook by Boolos et al \cite{Boolos87}. For this we did not need to implement anything on the ML-level of Isabelle/HOL. While formalising - \cite{Boolos87} have found an inconsistency in Bolos et al's usage - of definitions of what function a Turing machine calculates. In - Chapter 3 they use a definition such that the function is undefined + \cite{Boolos87} we have found an inconsistency in Bolos et al's + definitions of what function a Turing machine calculates. In + Chapter 3 they use a definition that states a function is undefined if the Turing machine loops \emph{or} halts with a non-standard tape. Whereas in Chapter 8 about the universal Turing machine, the Turing machines will \emph{not} halt unless the tape is in standard @@ -1396,26 +1396,22 @@ non-standard, but very much suited to a formalisation in a theorem prover where the @{term steps}-function need to be total. - The most closely related work is by Norrish \cite{Norrish11}, and - 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 + The most closely related work is by Norrish \cite{Norrish11}, and by + Asperti and Ricciotti \cite{AspertiRicciotti12}. Norrish 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 universal 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) + times of a mechanised proof pearl about the Myhill-Nerode + theorem. So our conclusion is it not as daunting as we estimated + when reading the paper by Norrish \cite{Norrish11}. The work + involved with constructing a universal 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; + recursive functions XX loc and the universal Turing machine XX loc). Our work was also very much inspired by the formalisation of Turing machines by Asperti and Ricciotti \cite{AspertiRicciotti12} in the @@ -1426,40 +1422,44 @@ complexity theory. They formalised a universal 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. + infrastructure, we expect however 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 + For us the most interesting aspect of our work are the correctness + proofs for Turing machines. Informal presentations of computability theory often leave the constructions of particular Turing machines - as exercise 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 established for showing correctness and termination. + as exercise to the reader, as for example \cite{Boolos87}, deeming + it to be just a chore. However, as far as we are aware all informal + presentations leave out any arguments why these Turing machines + should be correct. This means the reader or formalsiser is left + with the task of finding appropriate invariants and measures for + showing correctness and termination of these Turing machines. 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 magnitude of weeks. + relatively straightforward and much smaller than for example the + invariants used by Myreen in a correctness proof of a garbage collector + written in machine code \cite[Page 76]{Myreen09}. Howvere, 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 for his, something on the magnitude of + weeks. - 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 assembly programs that Hoare-style reasoning is sometimes - possible, but sometimes not. In order to ease their reasoning they + Our reasoning about the invariants is not much supported by the + automation in Isabelle. There is however a tantalising connection + between our work and very recent work \cite{Jensen13} on verifying + X86 assembly code. They observed a similar phenomenon with assembly + programs that Hoare-style reasoning is sometimes possible, but + sometimes it is 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 assembly code can make it easier to reason about our Turing - programs. That would be an attractive result, because Turing - machine programs are - - 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/} + Hoare-rules can be provided for special cases. It remains to be + seen whether their specification logic for assembly code can make it + easier to reason about our Turing programs. That would be an + attractive result, because Turing machine programs are very much + like assmbly programs and it would connect some very classic work on + Turing machines with very cutting-edge work on machine code + verification. In order to try out such ideas, our formalisation provides the + ``playground''. 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 36d7c284a38d -r 7fa1b8e88d76 Paper/document/root.bib --- a/Paper/document/root.bib Wed Feb 06 13:28:01 2013 +0000 +++ b/Paper/document/root.bib Wed Feb 06 14:06:18 2013 +0000 @@ -1,3 +1,12 @@ + + +@PhdThesis{Myreen09, + author = {M.~O.~Myreen}, + title = {{F}ormal {V}erification of {M}achine-{C}ode {P}rograms}, + year = 2009, + school = {University of Cambridge} +} + @article{Nipkow98, author={T.~Nipkow}, title={{W}inskel is (almost) {R}ight: {T}owards a {M}echanized {S}emantics {T}extbook}, diff -r 36d7c284a38d -r 7fa1b8e88d76 paper.pdf Binary file paper.pdf has changed