**This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.**

### Abstract

This entry formalises results from computability theory,
for example recursive functions,
undecidability of the halting problem, the existence of a
universal Turing machine and so on. This formalisation is the AFP entry
corresponding to the paper Mechanising Turing Machines and Computability Theory
in Isabelle/HOL from ITP 2013. The main book used for this formalisation is
by Boolos, Burgess, and Jeffrey on *Computability and Logic*.

Joosten contributed by making the files ready for the
AFP in 2019. His need for a formalisation of Turing Machines arose from
realising that the current formalisation of saturation graphs
(also in the AFP) was missing a key undecidability result
present in his paper on *Finding models through graph saturation*.

Regensburger contributed in 2022 by adding definitions for concepts like Turing Decidability, Turing Computability and Turing Reducibility for problem reduction. He also enhanced the result about the undecidability of the General Halting Problem given in the original AFP entry by first proving the undecidability of the Special Halting Problem and then proving its reducibility to the general problem. The original version of this AFP entry did only prove a weak form of the undecidability theorem. The main motivation behind this contribution is to make the AFP entry accessible for bachelor and master students.

### License

### History

- September 7, 2022
- Franz Regensburger added substantial material and made some modifications.

- January 16, 2019
- Sebastiaan Joosten made the code ready for the AFP.

### Topics

### Session Universal_Turing_Machine

- Turing
- Turing_aux
- BlanksDoNotMatter
- ComposableTMs
- ComposedTMs
- Numerals
- Numerals_Ex
- Turing_Hoare
- SemiIdTM
- Turing_HaltingConditions
- OneStrokeTM
- WeakCopyTM
- StrongCopyTM
- TuringDecidable
- TuringReducible
- SimpleGoedelEncoding
- HaltingProblems_K_H
- HaltingProblems_K_aux
- TuringComputable
- DitherTM
- CopyTM
- TuringUnComputable_H2
- TuringUnComputable_H2_original
- Abacus_Mopup
- Abacus
- Abacus_alt_Compile
- Abacus_Hoare
- Rec_Def
- Rec_Ex
- Recursive
- Recs_alt_Def
- Recs_alt_Ex
- UF
- UTM
- GeneratedCode