298 %the algorithms as recursive functions, because internally in |
298 %the algorithms as recursive functions, because internally in |
299 %Isabelle/HOL, like in all HOL-based theorem provers, functions are |
299 %Isabelle/HOL, like in all HOL-based theorem provers, functions are |
300 %represented as inductively defined predicates too. |
300 %represented as inductively defined predicates too. |
301 |
301 |
302 \noindent |
302 \noindent |
303 The motivation of this paper is to bring the ability to reason |
303 One concete model of computation are Turing machines. We use them |
304 about results from computability theory, for example decidability of the halting problem, |
304 in the theorem prover Isabelle/HOL for mechanising results from |
305 to the theorem prover Isabelle/HOL. Norrish formalised computability |
305 computability theory, for example the undecidability of the halting problem. |
|
306 Reasoning about decidability is not as straightforward as one might think |
|
307 in Isabelle/HOL and other HOL theorem provers, |
|
308 since they are based on classical logic where the law of excluded |
|
309 middle ensures that \mbox{@{term "P \<or> \<not>P"}} is always provable no |
|
310 matter whether the predicate @{text P} is constructed by computable means. |
|
311 |
|
312 Norrish formalised computability |
306 theory in HOL4. He choose the $\lambda$-calculus as the starting point |
313 theory in HOL4. He choose the $\lambda$-calculus as the starting point |
307 for his formalisation because of its ``simplicity'' \cite[Page |
314 for his formalisation because of its ``simplicity'' \cite[Page |
308 297]{Norrish11}. Part of his formalisation is a clever infrastructure |
315 297]{Norrish11}. Part of his formalisation is a clever infrastructure |
309 for reducing $\lambda$-terms. He also established the computational |
316 for reducing $\lambda$-terms. He also established the computational |
310 equivalence between the $\lambda$-calculus and recursive functions. |
317 equivalence between the $\lambda$-calculus and recursive functions. |