### 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

BSD 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

- Logic/Computability
- Computer science/Automata and formal languages

### 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

## Cite

×

Universal_Turing_Machine-AFP

    @article{Universal_Turing_Machine-AFP,
      author  = {Jian Xu and Xingyuan Zhang and Christian Urban and Sebastiaan J. C. Joosten and Franz Regensburger},
      title   = {Universal Turing Machine},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/Universal_Turing_Machine.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Feb 12, 2019 : Isabelle2018