tm: comparison Paper/Paper.thy

equal deleted inserted replaced

-:36d7c284a38d
+:7fa1b8e88d76
 section {* Conclusion *}
 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
+\cite{Boolos87} we have found an inconsistency in Bolos et al's
-of definitions of what function a Turing machine calculates. In
+definitions of what function a Turing machine calculates. In
-Chapter 3 they use a definition such that the function is undefined
+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
 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.
-The most closely related work is by Norrish \cite{Norrish11}, and
+The most closely related work is by Norrish \cite{Norrish11}, and by
-Asperti and Ricciotti \cite{AspertiRicciotti12}. Norrish formalises
+Asperti and Ricciotti \cite{AspertiRicciotti12}. Norrish mentions
-computability theory using $\lambda$-terms. For this he introduced a
+that formalising Turing machines would be a ``daunting prospect''
-clever rewriting technology based on combinators and de-Bruijn
+\cite[Page 310]{Norrish11}. While $\lambda$-terms indeed lead to
-indices for rewriting modulo $\beta$-equivalence (in order to avoid
+some slick mechanised proofs, our experience is that Turing machines
-explicit $\alpha$-renamings). He mentions that formalising Turing
+are not too daunting if one is only concerned with formalising the
-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
+times of a mechanised proof pearl about the Myhill-Nerode
-theorem. So our conclusion is it not as daunting as we imagined
+theorem. So our conclusion is it not as daunting as we estimated
-reading the paper by Norrish \cite{Norrish11}. The work involved
+when reading the paper by Norrish \cite{Norrish11}. The work
-with constructing a universal Turing machine via recursive
+involved with constructing a universal Turing machine via recursive
-functions and abacus machines, on the other hand, is not a
+functions and abacus machines, on the other hand, is not a project
-project one wants to undertake too many times (our formalisation
+one wants to undertake too many times (our formalisation of abacus
-of abacus machines and their correct translation is approximately
+machines and their correct translation is approximately 4300 loc;
-4300 loc; \ldots)
+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
 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 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
+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
+as exercise to the reader, as for example \cite{Boolos87}, deeming
-too easy for wasting space. However, as far as we are aware all
+it to be just a chore. However, as far as we are aware all informal
-informal presentation leave out any correctness proofs---do the
+presentations leave out any arguments why these Turing machines
-Turing machines really perform the task they are supposed to do.
+should be correct.  This means the reader or formalsiser is left
-This means we have to find appropriate invariants and measures
+with the task of finding appropriate invariants and measures for
-that can be established for showing correctness and termination.
+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
+relatively straightforward and much smaller than for example the
-the invariants by Myreen for a correctness proof of a garbage
+invariants used by Myreen in a correctness proof of a garbage collector
-collector \cite[Page 76]{}. The invariant needed for the abacus proof,
+written in machine code \cite[Page 76]{Myreen09}. Howvere, the invariant
-where Hoare-style reasoning does not work, is similar in size as
+needed for the abacus proof, where Hoare-style reasoning does not work, is
-the one by Myreen and finding a sufficiently strong one took
+similar in size as the one by Myreen and finding a sufficiently
-us, like Myreen, something on the magnitude of weeks.
+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
+Our reasoning about the invariants is not much supported by the
-connection between our work and recent work \cite{Jensen13}
+automation in Isabelle. There is however a tantalising connection
-on verifying X86 assembly code. They observed a similar phenomenon
+between our work and very recent work \cite{Jensen13} on verifying
-with assembly programs that Hoare-style reasoning is sometimes
+X86 assembly code. They observed a similar phenomenon with assembly
-possible, but sometimes not. In order to ease their reasoning they
+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.
+Hoare-rules can be provided for special cases.  It remains to be
-It remains to be seen whether their specification logic
+seen whether their specification logic for assembly code can make it
-for assembly code can make it easier to reason about our Turing
+easier to reason about our Turing programs. That would be an
-programs. That would be an attractive result, because Turing
+attractive result, because Turing machine programs are very much
-machine programs are
+like assmbly programs and it would connect some very classic work on
+Turing machines with very cutting-edge work on machine code
-The code of our formalisation is available from the Mercurial repository at
+verification. In order to try out such ideas, our formalisation provides the
-\url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/tm/}
+``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/}.
 *}
 (*<*)

changeset 138	7fa1b8e88d76
parent 136	8fa9e018abe4
child 140	7f5243700f25