Universal Turing Machine

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.