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 O(f(n)) time, then the singletape TM has a worst-time complexity of 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

Cite

× 
@article{Multitape_To_Singletape_TM-AFP,
  author  = {Christian Dalvit and René Thiemann},
  title   = {A Verified Translation of Multitape Turing Machines into Singletape Turing Machines},
  journal = {Archive of Formal Proofs},
  month   = {November},
  year    = {2022},
  note    = {\url{https://isa-afp.org/entries/Multitape_To_Singletape_TM.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: