48 \maketitle |
48 \maketitle |
49 |
49 |
50 |
50 |
51 \begin{abstract} |
51 \begin{abstract} |
52 We present a formalised theory of computability in the theorem prover |
52 We present a formalised theory of computability in the theorem prover |
53 Isabelle/HOL. This theorem prover is based on classical logic which |
53 Isabelle/HOL. |
54 precludes \emph{direct} reasoning about computability: every boolean |
54 %This theorem prover is based on classical logic which |
55 predicate is either true or false because of the law of excluded |
55 %precludes \emph{direct} reasoning about computability: every boolean |
56 middle. The only way to reason about computability in a classical |
56 %predicate is either true or false because of the law of excluded |
57 theorem prover is to formalise a concrete model of computation. We |
57 %middle. The only way to reason about computability in a classical |
58 formalise Turing machines and relate them to abacus machines and |
58 %theorem prover is to formalise a concrete model of computation. |
59 recursive functions. We also formalise a universal Turing machine and |
59 Following the textbook by Boolos et al, we formalise Turing machines |
60 Hoare-style reasoning techniques that allow us to reason about Turing machine |
60 and relate them to abacus machines and recursive functions. We ``tie |
61 programs. Our theory can be used to formalise other computability |
61 the know'' between these three computational models by formalising a |
62 results. %We give one example about the computational equivalence of |
62 universal function and obtaining from it a universal Turing machine by |
|
63 our verified translation from recursive functions to abacus programs |
|
64 and from abacus programs to Turing machine programs. Hoare-style reasoning techniques allow us |
|
65 to reason about Turing machine and abacus programs. Our theory can be |
|
66 used to formalise other computability results. |
|
67 %We give one example about the computational equivalence of |
63 %single-sided Turing machines. |
68 %single-sided Turing machines. |
64 %{\it we give one example about the undecidability of Wang's tiling problem, whose proof uses |
69 %{\it we give one example about the undecidability of Wang's tiling problem, whose proof uses |
65 %the notion of a universal Turing machine.} |
70 %the notion of a universal Turing machine.} |
66 \end{abstract} |
71 \end{abstract} |
67 |
72 |