tm: comparison Paper/Paper.thy

equal deleted inserted replaced

-:8f89170bb076
+:e0a7ee9842d6
 %made us realise that important details were left out in the informal
 %model for the latter. However, in both cases we were unable to
 %formalise in Isabelle/HOL computability arguments about the
 %algorithms.
+%Suppose you want to mechanise a proof for whether a predicate @{term P},
-\noindent
+%say, is decidable or not. Decidability of @{text P} usually
-Suppose you want to mechanise a proof for whether a predicate @{term
+%amounts to showing whether \mbox{@{term "P \<or> \<not>P"}} holds. But this
-P}, say, is decidable or not. Decidability of @{text P} usually
+%does \emph{not} work in
-amounts to showing whether \mbox{@{term "P \<or> \<not>P"}} holds. But this
-does \emph{not} work in Isabelle/HOL and other HOL theorem provers,
-since they are based on classical logic where the law of excluded
+%Since Isabelle/HOL and other HOL theorem provers,
-middle ensures that \mbox{@{term "P \<or> \<not>P"}} is always provable no
+%are based on classical logic where the law of excluded
-matter whether @{text P} is constructed by computable means. We hit on
+%middle ensures that \mbox{@{term "P \<or> \<not>P"}} is always provable no
-this limitation previously when we mechanised the correctness proofs
+%matter whether @{text P} is constructed by computable means. We hit on
-of two algorithms \cite{UrbanCheneyBerghofer11,WuZhangUrban12}, but
+%this limitation previously when we mechanised the correctness proofs
-were unable to formalise arguments about decidability or undecidability.
+%of two algorithms \cite{UrbanCheneyBerghofer11,WuZhangUrban12}, but
+%were unable to formalise arguments about decidability or undecidability.
 %The same problem would arise if we had formulated
 %the algorithms as recursive functions, because internally in
 %Isabelle/HOL, like in all HOL-based theorem provers, functions are
 %represented as inductively defined predicates too.
-The only satisfying way out of this problem in a theorem prover based
+\noindent
-on classical logic is to formalise a theory of computability. Norrish
+The motivation of this paper is to bring the ability to reason
-provided such a formalisation for HOL4. He choose the
+about results from computability theory, for example decidability of the halting problem,
-$\lambda$-calculus as the starting point for his formalisation because
+to the theorem prover Isabelle/HOL.  Norrish formalised computability
-of its ``simplicity'' \cite[Page 297]{Norrish11}.  Part of his
+theory in HOL4. He choose the $\lambda$-calculus as the starting point
-formalisation is a clever infrastructure for reducing
+for his formalisation because of its ``simplicity'' \cite[Page
-$\lambda$-terms. He also established the computational equivalence
+297]{Norrish11}.  Part of his formalisation is a clever infrastructure
-between the $\lambda$-calculus and recursive functions.  Nevertheless
+for reducing $\lambda$-terms. He also established the computational
-he concluded that it would be appealing to have formalisations for
+equivalence between the $\lambda$-calculus and recursive functions.
-more operational models of computations, such as Turing machines or
+Nevertheless he concluded that it would be appealing to have
-register machines.  One reason is that many proofs in the literature
+formalisations for more operational models of computations, such as
-use them.  He noted however that \cite[Page 310]{Norrish11}:
+Turing machines or register machines.  One reason is that many proofs
+in the literature use them.  He noted however that \cite[Page
+310]{Norrish11}:
 \begin{quote}
 \it``If register machines are unappealing because of their
 general fiddliness,\\ Turing machines are an even more
 daunting prospect.''
 to construct a universal Turing machine we therefore do not follow
 \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.
+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
+set than the one described in \cite{Boolos87}.
 \smallskip
 \noindent
 {\bf Contributions:} We formalised in Isabelle/HOL Turing machines
 following the description of Boolos et al \cite{Boolos87} where tapes
 \end{tabular}
 \end{center}
 \noindent
 This time the Hoare-triple states that @{term tcontra} terminates
-with the ``output'' @{term "<(1::nat)>"}. In both case we come
+with the ``output'' @{term "<(1::nat)>"}. In both cases we come
 to a contradiction, which means we have to abandon our assumption
 that there exists a Turing machine @{term H} which can in general decide
 whether Turing machines terminate.
 *}
 Turing machines, an unexpected outcome of our work is that we
 identified an inconsistency in their use of a definition. This is
 unexpected since \cite{Boolos87} is a classic textbook which has
 undergone several editions (we used the fifth edition; the material
 containing the inconsistency was introduced in the fourth edition
-\cite{BoolosFourth}). The central
+of this book). The central
 idea about Turing machines is that when started with standard tapes
 they compute a partial arithmetic function.  The inconsistency arises
 when they define the case when this function should \emph{not} return a
 result. Boolos at al write in Chapter 3, Page 32:
 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
+\noindent
+{\bf Acknowledgements:} We are very grateful for the extremely helpful
+comments by the anonymous reviewers.
 *}
 (*<*)

changeset 233	e0a7ee9842d6
parent 232	8f89170bb076
child 234	ca2ea835c363