27 where the law of excluded middle ensures that \mbox{@{term "P \<or> \<not>P"}} |
27 where the law of excluded middle ensures that \mbox{@{term "P \<or> \<not>P"}} |
28 is always provable no matter whether @{text P} is constructed by |
28 is always provable no matter whether @{text P} is constructed by |
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. |
32 represented as inductively defined predicates too. |
33 |
33 |
34 The only satisfying way out is to formalise a theory of |
34 The only satisfying way out in a theorem prover based on classical |
35 computability. Norrish provided such a formalisation for the HOL4 |
35 logic is to formalise a theory of computability. Norrish provided such |
36 theorem prover. He choose the $\lambda$-calculus as the starting point |
36 a formalisation for the HOL4 theorem prover. He choose the |
37 for his formalisation, because of its ``simplicity'' \cite[Page |
37 $\lambda$-calculus as the starting point for his formalisation |
38 297]{Norrish11}. Part of his formalisation is a clever infrastructure |
38 of computability theory, |
39 for reducing $\lambda$-terms. He also established the computational |
39 because of its ``simplicity'' \cite[Page 297]{Norrish11}. Part of his |
40 equivalence between the lambda-calculus and recursive functions. |
40 formalisation is a clever infrastructure for reducing |
41 Nevertheless he concluded that it would be appealing to have |
41 $\lambda$-terms. He also established the computational equivalence |
42 formalisations of more operational models of computations such as |
42 between the $\lambda$-calculus and recursive functions. Nevertheless he |
43 Turing machines or register machines. One reason is that many proofs |
43 concluded that it would be ``appealing'' to have formalisations for more |
44 in the literature refer to them. He noted however that in the context |
44 operational models of computations, such as Turing machines or register |
45 of theorem provers \cite[Page 310]{Norrish11}: |
45 machines. One reason is that many proofs in the literature refer to |
|
46 them. He noted however that in the context of theorem provers |
|
47 \cite[Page 310]{Norrish11}: |
46 |
48 |
47 \begin{quote} |
49 \begin{quote} |
48 \it``If register machines are unappealing because of their |
50 \it``If register machines are unappealing because of their |
49 general fiddliness, Turing machines are an even more |
51 general fiddliness, Turing machines are an even more |
50 daunting prospect.'' |
52 daunting prospect.'' |
51 \end{quote} |
53 \end{quote} |
52 |
54 |
53 \noindent |
55 \noindent |
54 In this paper |
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) |
|
58 and recursive functions. Theorem provers are at their best when the data-structures |
|
59 at hand are ``structurally'' defined (like lists, natural numbers, |
|
60 regular expressions, etc). The reason why reasoning about Turing machines |
|
61 is challenging is because they are essentially ... |
|
62 |
|
63 |
|
64 For this we followed mainly the informal |
|
65 proof given in the textbook \cite{Boolos87}. |
55 |
66 |
56 |
67 |
57 |
68 |
58 |
69 |
59 ``In particular, the fact that the universal machine operates with a |
70 ``In particular, the fact that the universal machine operates with a |