64 %Isabelle/HOL, like in all HOL-based theorem provers, functions are |
64 %Isabelle/HOL, like in all HOL-based theorem provers, functions are |
65 %represented as inductively defined predicates too. |
65 %represented as inductively defined predicates too. |
66 |
66 |
67 The only satisfying way out of this problem in a theorem prover based |
67 The only satisfying way out of this problem in a theorem prover based |
68 on classical logic is to formalise a theory of computability. Norrish |
68 on classical logic is to formalise a theory of computability. Norrish |
69 provided such a formalisation for the HOL4. He choose |
69 provided such a formalisation for the HOL. He choose |
70 the $\lambda$-calculus as the starting point for his formalisation of |
70 the $\lambda$-calculus as the starting point for his formalisation of |
71 computability theory, because of its ``simplicity'' \cite[Page |
71 computability theory, because of its ``simplicity'' \cite[Page |
72 297]{Norrish11}. Part of his formalisation is a clever infrastructure |
72 297]{Norrish11}. Part of his formalisation is a clever infrastructure |
73 for reducing $\lambda$-terms. He also established the computational |
73 for reducing $\lambda$-terms. He also established the computational |
74 equivalence between the $\lambda$-calculus and recursive functions. |
74 equivalence between the $\lambda$-calculus and recursive functions. |
88 In this paper we take on this daunting prospect and provide a |
88 In this paper we take on this daunting prospect and provide a |
89 formalisation of Turing machines, as well as abacus machines (a kind |
89 formalisation of Turing machines, as well as abacus machines (a kind |
90 of register machines) and recursive functions. To see the difficulties |
90 of register machines) and recursive functions. To see the difficulties |
91 involved with this work, one has to understand that Turing machine |
91 involved with this work, one has to understand that Turing machine |
92 programs can be completely \emph{unstructured}, behaving |
92 programs can be completely \emph{unstructured}, behaving |
93 similar to Basic's infamous goto \cite{Dijkstra68}. This precludes in the |
93 similar Basic programs involving the infamous goto \cite{Dijkstra68}. This precludes in the |
94 general case a compositional Hoare-style reasoning about Turing |
94 general case a compositional Hoare-style reasoning about Turing |
95 programs. We provide such Hoare-rules for when it is possible to |
95 programs. We provide such Hoare-rules for when it \emph{is} possible to |
96 reason in a compositional manner (which is fortunately quite often), but also tackle |
96 reason in a compositional manner (which is fortunately quite often), but also tackle |
97 the more complicated case when we translate abacus programs into |
97 the more complicated case when we translate abacus programs into |
98 Turing programs. This aspect of reasoning about computability theory |
98 Turing programs. These difficulties when reasoning about computability theory |
99 is usually completely left out in the informal literature, e.g.~\cite{Boolos87}. |
99 are usually completely left out in the informal literature, e.g.~\cite{Boolos87}. |
100 |
100 |
101 %To see the difficulties |
101 %To see the difficulties |
102 %involved with this work, one has to understand that interactive |
102 %involved with this work, one has to understand that interactive |
103 %theorem provers, like Isabelle/HOL, are at their best when the |
103 %theorem provers, like Isabelle/HOL, are at their best when the |
104 %data-structures at hand are ``structurally'' defined, like lists, |
104 %data-structures at hand are ``structurally'' defined, like lists, |