A Verified Translation of Multitape Turing Machines into Singletape Turing Machines

Christian Dalvit and RenĂ© Thiemann đŸ“§

November 30, 2022

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

We define single- and multitape Turing machines (TMs) and verify a translation from multitape TMs to singletape TMs. In particular, the following results have been formalized: the accepted languages coincide, and whenever the multitape TM runs in $\mathcal{O}(f(n))$ time, then the singletape TM has a worst-time complexity of $\mathcal{O}(f(n)^2 + n)$. The translation is applicable both on deterministic and non-deterministic TMs.

License

BSD License

Topics

Session Multitape_To_Singletape_TM