29 computable means. The same problem would arise if we had formulated |
29 computable means. The same problem would arise if we had formulated |
30 the algorithms as recursive functions, because internally in |
30 the algorithms as recursive functions, because internally in |
31 Isabelle/HOL, like in all HOL-based theorem provers, functions are |
31 Isabelle/HOL, like in all HOL-based theorem provers, functions are |
32 represented as inductively defined predicates too. |
32 represented as inductively defined predicates too. |
33 |
33 |
34 The only satisfying way out in a theorem prover based on classical |
34 The only satisfying way out of this problem in a theorem prover based on classical |
35 logic is to formalise a theory of computability. Norrish provided such |
35 logic is to formalise a theory of computability. Norrish provided such |
36 a formalisation for the HOL4 theorem prover. He choose the |
36 a formalisation for the HOL4 theorem prover. He choose the |
37 $\lambda$-calculus as the starting point for his formalisation |
37 $\lambda$-calculus as the starting point for his formalisation |
38 of computability theory, |
38 of computability theory, |
39 because of its ``simplicity'' \cite[Page 297]{Norrish11}. Part of his |
39 because of its ``simplicity'' \cite[Page 297]{Norrish11}. Part of his |
40 formalisation is a clever infrastructure for reducing |
40 formalisation is a clever infrastructure for reducing |
41 $\lambda$-terms. He also established the computational equivalence |
41 $\lambda$-terms. He also established the computational equivalence |
42 between the $\lambda$-calculus and recursive functions. Nevertheless he |
42 between the $\lambda$-calculus and recursive functions. Nevertheless he |
43 concluded that it would be ``appealing'' to have formalisations for more |
43 concluded that it would be ``appealing'' to have formalisations for more |
44 operational models of computations, such as Turing machines or register |
44 operational models of computations, such as Turing machines or register |
45 machines. One reason is that many proofs in the literature refer to |
45 machines. One reason is that many proofs in the literature use |
46 them. He noted however that in the context of theorem provers |
46 them. He noted however that in the context of theorem provers |
47 \cite[Page 310]{Norrish11}: |
47 \cite[Page 310]{Norrish11}: |
48 |
48 |
49 \begin{quote} |
49 \begin{quote} |
50 \it``If register machines are unappealing because of their |
50 \it``If register machines are unappealing because of their |
53 \end{quote} |
53 \end{quote} |
54 |
54 |
55 \noindent |
55 \noindent |
56 In this paper we took on this daunting prospect and provide a formalisation |
56 In this paper we took on this daunting prospect and provide a formalisation |
57 of Turing machines, as well as Abacus machines (a kind of register machine) |
57 of Turing machines, as well as Abacus machines (a kind of register machine) |
58 and recursive functions. Theorem provers are at their best when the data-structures |
58 and recursive functions. To see the difficulties involved with this work one |
|
59 has to understantd that interactive theorem provers, like Isabelle/HOL, are at |
|
60 their best when the data-structures |
59 at hand are ``structurally'' defined (like lists, natural numbers, |
61 at hand are ``structurally'' defined (like lists, natural numbers, |
60 regular expressions, etc). The reason why reasoning about Turing machines |
62 regular expressions, etc). For them, they come with a convenient reasoning |
|
63 infrastructure (for example induction principles, recursion combinators and so on). |
|
64 But this is not the case with Turing machines (and also register machines): |
|
65 underlying their definition is a set of states |
|
66 together with a transition function, both of which are not structurally defined. |
|
67 This means we have to implement our own reasoning infrastructure. This often |
|
68 leads to annoyingly lengthy and detailed formalisations. We noticed first |
|
69 the difference between both ``worlds'' when formalising the Myhill-Nerode |
|
70 theorem ??? where regular expressions fared much better than automata. |
|
71 However, with Turing machines there seems to be no alternative, because they |
|
72 feature frequently in proofs. We will analyse one case, Wang tilings, at the end |
|
73 of the paper, which uses also the notion of a Universal Turing Machine. |
|
74 |
|
75 The reason why reasoning about Turing machines |
61 is challenging is because they are essentially ... |
76 is challenging is because they are essentially ... |
62 |
77 |
63 |
78 |
64 For this we followed mainly the informal |
79 For this we followed mainly the informal |
65 proof given in the textbook \cite{Boolos87}. |
80 proof given in the textbook \cite{Boolos87}. |