--- a/Paper/Paper.thy Fri Apr 05 09:18:17 2013 +0100
+++ b/Paper/Paper.thy Mon Apr 22 08:26:16 2013 +0100
@@ -300,14 +300,13 @@
%represented as inductively defined predicates too.
\noindent
-One concete model of computation are Turing machines. We use them
-in the theorem prover Isabelle/HOL for mechanising results from
-computability theory, for example the undecidability of the halting problem.
-Reasoning about decidability is not as straightforward as one might think
-in Isabelle/HOL and other HOL theorem provers,
-since they are based on classical logic where the law of excluded
-middle ensures that \mbox{@{term "P \<or> \<not>P"}} is always provable no
-matter whether the predicate @{text P} is constructed by computable means.
+We like to enable Isabelle/HOL users to reason about computability
+theory. Reasoning about decidability of predicates, for example, is not as
+straightforward as one might think in Isabelle/HOL and other HOL
+theorem provers, since they are based on classical logic where the law
+of excluded middle ensures that \mbox{@{term "P \<or> \<not>P"}} is always
+provable no matter whether the predicate @{text P} is constructed by
+computable means.
Norrish formalised computability
theory in HOL4. He choose the $\lambda$-calculus as the starting point
@@ -419,7 +418,7 @@
\cite{AspertiRicciotti12}, instead follow the proof in
\cite{Boolos87} by translating abacus machines to Turing machines and in
turn recursive functions to abacus machines. The universal Turing
-machine can then be constructed by translating from a recursive function.
+machine can then be constructed by translating from a (universal) recursive function.
The part of mechanising the translation of recursive function to register
machines has already been done by Zammit in HOL \cite{Zammit99},
although his register machines use a slightly different instruction
@@ -675,14 +674,9 @@
\noindent
where @{term "read r"} returns the head of the list @{text r}, or if
- @{text r} is empty it returns @{term Bk}. It is impossible in
- Isabelle/HOL to lift the @{term step}-function in order to realise a
- general evaluation function for Turing machines programs. The reason
- is that functions in HOL-based provers need to be terminating, and
- clearly there are programs that are not.\footnote{There is the alternative
- to use partial functions, which do not necessarily need to terminate, but
- this does not provide us with a useful induction principle \cite{Krauss10}.} We can however define a
- recursive evaluation function that performs exactly @{text n} steps:
+ @{text r} is empty it returns @{term Bk}.
+ We lift this definition to an evaluation function that performs
+ exactly @{text n} steps:
\begin{center}
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
@@ -1657,17 +1651,19 @@
text {*
In previous works we were unable to formalise results about
- 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 for computability theory,
- but then we would still 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 essential use of them
- (for example the undecidability proof for Wang's tiling problem \cite{Robinson71}).
+ computability because in Isabelle/HOL we cannot, for example,
+ 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 for computability theory, but then we would have
+ to reimplement on the ML-level his infrastructure for rewriting
+ $\lambda$-terms modulo $\beta$-equality: HOL4 has a simplifer that
+ can rewrite terms modulo an arbitrary equivalence relation, which
+ Isabelle unfortunately does not yet have. Even though we would
+ still need to connect $\lambda$-terms somehow to Turing machines for
+ proofs that make essential use of them (for example the
+ undecidability proof for Wang's tiling problem \cite{Robinson71}).
We therefore have formalised Turing machines in the first place and the main
computability results from Chapters 3 to 8 in the textbook by Boolos
@@ -1679,33 +1675,31 @@
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. If the title had not already been taken in \cite{Nipkow98}, we could
- have titled our paper ``Boolos et al are (almost)
- Right''. We have not attempted to formalise everything precisely as
+ form. Like Nipkow \cite{Nipkow98} observed with his formalisation
+ of a textbook, we found that 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 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 ``\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. As a point of
- comparison, the halting problem
- 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 that this part is 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, we agree, is not a project
- one wants to undertake too many times (our formalisation of abacus
- machines and their correct translation is approximately 4600 loc;
- recursive functions 2800 loc and the universal Turing machine 10000 loc).
+ 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. As a point of comparison, the halting
+ problem 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 that this part is 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, we
+ agree, is not a project one wants to undertake too many times (our
+ formalisation of abacus machines and their correct translation is
+ approximately 4600 loc; recursive functions 2800 loc and the
+ universal Turing machine 10000 loc).
Our work is also very much inspired by the formalisation of Turing
machines of Asperti and Ricciotti \cite{AspertiRicciotti12} in the
@@ -1738,21 +1732,22 @@
weeks.
Our reasoning about the invariants is not much supported by the
- automation beyond the standard automation tools available in Isabelle/HOL.
- There is however a tantalising connection
- between our work and very recent work by Jensen et al \cite{Jensen13} on verifying
- X86 assembly code that might change that. They observed a similar phenomenon with assembly
- programs where 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
- 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. Myreen ??? That would be an
- attractive result, because Turing machine programs are very much
- 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
+ automation beyond the standard automation tools available in
+ Isabelle/HOL. There is however a tantalising connection between our
+ work and very recent work by Jensen et al \cite{Jensen13} on
+ verifying X86 assembly code that might change that. They observed a
+ similar phenomenon with assembly programs where 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 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 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/}.
\medskip