# HG changeset patch # User Christian Urban # Date 1357305030 0 # Node ID dd400b5797e1118cf625d971116c103102dae849 # Parent 3d84f4dd6a01bd791e377858a103a87302ef4722 updated diff -r 3d84f4dd6a01 -r dd400b5797e1 Paper.thy --- a/Paper.thy Thu Jan 03 00:53:14 2013 +0000 +++ b/Paper.thy Fri Jan 04 13:10:30 2013 +0000 @@ -31,7 +31,7 @@ Isabelle/HOL, like in all HOL-based theorem provers, functions are represented as inductively defined predicates too. -The only satisfying way out in a theorem prover based on classical +The only satisfying way out of this problem 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 @@ -42,7 +42,7 @@ 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 +machines. One reason is that many proofs in the literature use them. He noted however that in the context of theorem provers \cite[Page 310]{Norrish11}: @@ -55,9 +55,24 @@ \noindent 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 +and recursive functions. To see the difficulties involved with this work one +has to understantd that interactive theorem provers, like Isabelle/HOL, 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 +regular expressions, etc). For them, they come with a convenient reasoning +infrastructure (for example induction principles, recursion combinators and so on). +But this is not the case with Turing machines (and also register machines): +underlying their definition is a set of states +together with a transition function, both of which are not structurally defined. +This means we have to implement our own reasoning infrastructure. This often +leads to annoyingly lengthy and detailed formalisations. We noticed first +the difference between both ``worlds'' when formalising the Myhill-Nerode +theorem ??? where regular expressions fared much better than automata. +However, with Turing machines there seems to be no alternative, because they +feature frequently in proofs. We will analyse one case, Wang tilings, at the end +of the paper, which uses also the notion of a Universal Turing Machine. + +The reason why reasoning about Turing machines is challenging is because they are essentially ... diff -r 3d84f4dd6a01 -r dd400b5797e1 paper.pdf Binary file paper.pdf has changed