Email Gateway (Dec 01 2022 at 21:38): Email Gateway (Dec 01 2022 at 21:38):From: Gerwin Klein <kleing@unsw.edu.au>
A Verified Translation of Multitape Turing Machines Into Singletape Turing Machines
by Christian Dalvit and René Thiemann
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.
https://www.isa-afp.org/entries/Multitape_To_Singletape_TM.html
Enjoy!
Gerwin
Last updated: Jan 04 2025 at 20:18 UTC