diff -r 07730607b0ca -r 38d8e0e37b7d Paper/Paper.thy --- a/Paper/Paper.thy Thu Feb 07 01:00:55 2013 +0000 +++ b/Paper/Paper.thy Thu Feb 07 03:01:51 2013 +0000 @@ -1,6 +1,6 @@ (*<*) theory Paper -imports "../thys/recursive" +imports "../thys/UTM" begin @@ -1329,6 +1329,33 @@ with the standard tape @{term "([Bk, Bk], )"} will terminate with the standard tape @{term "(Bk \ k, @ Bk \ l)"} for some @{text k} and @{text l}. + Having + + we can prove that if + + \begin{center} + @{thm (prem 3) UTM_halt_lemma2} + \end{center} + then + + \begin{center} + @{thm (concl) UTM_halt_lemma2} + \end{center} + + under the assumption that @{text p} + is well-formed and the arguments are not empty. + + + \begin{center} + @{thm (prem 2) UTM_unhalt_lemma2} + \end{center} + then + + \begin{center} + @{thm (concl) UTM_unhalt_lemma2} + \end{center} + + and the also the definition of the universal function (we refer the reader to our formalisation). @@ -1358,6 +1385,7 @@ but with @{term "([], [Oc])"} according to def Chap 8 *} +(* section {* XYZ *} text {* @@ -1406,6 +1434,7 @@ \] 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. *} +*) (* section {* Wang Tiles\label{Wang} *} @@ -1432,39 +1461,39 @@ 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 + anything on the ML-level of Isabelle/HOL. While formalising the six chapters \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 - form. Following in the footsteps of another paper \cite{Nipkow98} - formalising the results from a semantics textbook, we could - therefore have titled our paper ``Boolos et al are (almost) + form. If the title had not already been taken \cite{Nipkow98}, 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 use definitions that make our 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. + prover where the @{term steps}-function needs to be total. - 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'' + %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 ``\emph{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 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 + theorem. So our conclusion is that it not as daunting for this part of the + work 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 + functions and abacus machines, we agree, 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). + recursive functions 5000 loc and the universal Turing machine 10000 loc). Our work was also very much inspired by the formalisation of Turing machines by Asperti and Ricciotti \cite{AspertiRicciotti12} in the @@ -1481,38 +1510,38 @@ 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 for example \cite{Boolos87}, deeming + as exercise to the reader, 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 + should be correct. This means the reader 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 used by Myreen in a correctness proof of a garbage collector - written in machine code \cite[Page 76]{Myreen09}. Howvere, the invariant + written in machine code \cite[Page 76]{Myreen09}. However, 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 not much supported by the - automation in Isabelle. There is however a tantalising connection + automation beyond the standard automation tools available in Isabelle/HOL. + 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 + X86 assembly code that might change that. 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 + sometimes it is not. In order to ease their reasoning, they introduced a more primitive specification logic, on which 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 + like assembly programs and it would connect some very classic work on + Turing machines to 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/}. + Mercurial repository at \url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/tm/}. *}