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

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

### Session Multitape_To_Singletape_TM

- TM_Common
- Multitape_TM
- Singletape_TM
- STM_Renaming
- Multi_Single_TM_Translation

## Cite

×

Multitape_To_Singletape_TM-AFP

    @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:

- Sep 13, 2023 : Isabelle2023
- Dec 1, 2022 : Isabelle2022