diff -r 965df91a24bc -r 44e9d0c24fbc Paper.thy --- a/Paper.thy Sun Dec 30 22:15:54 2012 +0000 +++ b/Paper.thy Thu Jan 03 00:44:20 2013 +0000 @@ -29,20 +29,22 @@ computable means. 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. +represented as inductively defined predicates too. -The only satisfying way out is to formalise a theory of -computability. Norrish provided such a formalisation for the HOL4 -theorem prover. He choose the $\lambda$-calculus as the starting point -for his formalisation, because of its ``simplicity'' \cite[Page -297]{Norrish11}. Part of his formalisation is a clever infrastructure -for reducing $\lambda$-terms. He also established the computational -equivalence between the lambda-calculus and recursive functions. -Nevertheless he concluded that it would be appealing to have -formalisations of more operational models of computations such as -Turing machines or register machines. One reason is that many proofs -in the literature refer to them. He noted however that in the context -of theorem provers \cite[Page 310]{Norrish11}: +The only satisfying way out in a theorem prover based on classical +logic is to formalise a theory of computability. Norrish provided such +a formalisation for the HOL4 theorem prover. He choose the +$\lambda$-calculus as the starting point for his formalisation +of computability theory, +because of its ``simplicity'' \cite[Page 297]{Norrish11}. Part of his +formalisation is a clever infrastructure for reducing +$\lambda$-terms. He also established the computational equivalence +between the $\lambda$-calculus and recursive functions. Nevertheless he +concluded that it would be ``appealing'' to have formalisations for more +operational models of computations, such as Turing machines or register +machines. One reason is that many proofs in the literature refer to +them. He noted however that in the context of theorem provers +\cite[Page 310]{Norrish11}: \begin{quote} \it``If register machines are unappealing because of their @@ -51,7 +53,16 @@ \end{quote} \noindent -In this paper +In this paper we took on this daunting prospect and provide a formalisation +of Turing machines, as well as Abacus machines (a kind of register machine) +and recursive functions. Theorem provers are at their best when the data-structures +at hand are ``structurally'' defined (like lists, natural numbers, +regular expressions, etc). The reason why reasoning about Turing machines +is challenging is because they are essentially ... + + +For this we followed mainly the informal +proof given in the textbook \cite{Boolos87}. @@ -71,7 +82,7 @@ section {* Formalisation *} text {* - + *}