14 %\renewcommand{\isastyle}{\isastyleminor} |
14 %\renewcommand{\isastyle}{\isastyleminor} |
15 |
15 |
16 |
16 |
17 \begin{document} |
17 \begin{document} |
18 |
18 |
19 \title{A Formalised Theory of Turing Machines in Isabelle/HOL} |
19 \title{Formalising Computability Theory in Isabelle/HOL} |
20 |
20 |
21 |
21 |
22 \author{ |
22 \author{ |
23 \IEEEauthorblockN{Jian Xu, Xingyuan Zhang} |
23 \IEEEauthorblockN{Jian Xu, Xingyuan Zhang} |
24 \IEEEauthorblockA{PLA University of Science and Technology Nanjing, China} |
24 \IEEEauthorblockA{PLA University of Science and Technology Nanjing, China} |
29 |
29 |
30 \maketitle |
30 \maketitle |
31 |
31 |
32 |
32 |
33 \begin{abstract} |
33 \begin{abstract} |
34 Isabelle/HOL is an interactive theorem prover based on classical |
34 We present a formalised theory of computability in the |
35 logic. While classical reasoning allow users to take convenient |
35 theorem prover Isabelle/HOL. This theorem prover is based on classical |
36 shortcuts in some proofs, it precludes \emph{direct} reasoning about |
36 logic which precludes \emph{direct} reasoning about computability: every |
37 decidability: every boolean predicate is either true or false |
37 boolean predicate is either true or false because of the law of excluded |
38 because of the law of excluded middle. The only way to reason |
38 middle. The only way to reason about computability in a classical theorem |
39 about decidability in a classical theorem prover, like Isabelle/HOL, |
39 prover is to formalise a concrete model for computation. |
40 is to formalise a concrete model for computation. In this paper |
40 We formalise Turing machines and relate them to abacus machines and recursive |
41 we formalise Turing machines and relate them to register machines. |
41 functions. Our theory can be used to formalise other computability results: |
42 |
42 we give one example about the undecidability of Wang tilings, whose proof uses |
|
43 the notion of a universal Turing machine. |
43 \end{abstract} |
44 \end{abstract} |
44 |
45 |
45 \begin{IEEEkeywords} |
46 \begin{IEEEkeywords} |
46 Turing Machines, Decidability, Isabelle/HOL; |
47 Turing Machines, Computability, Isabelle/HOL, Wang tilings |
47 \end{IEEEkeywords} |
48 \end{IEEEkeywords} |
48 |
49 |
49 |
50 |
50 \IEEEpeerreviewmaketitle |
51 \IEEEpeerreviewmaketitle |
51 |
52 |