Formalizing O(n lg n) efficient universal Turing macine

Stream: maths

[Johannes Choo]

I'm aware of formalizations of universal Turing machines (UTMs), but I'm unaware of attempts to formalize that O(n lg n) universal simulation of TMs is possible. This is a fundamental result in TCS, but TMs are always tedious and to my knowledge its methods are not that relevant to contemporary research, hence the lack of visibility. https://en.wikipedia.org/wiki/Universal_Turing_machine#Efficiency . If it is indeed yet to be formalized anywhere, I'd like to see what it would take to formalize this result, especially since the recent formalization of some Busy Beaver results in Coq may be instructive to me on how to formalize in a well-structured waylow-level behavior of TMs.

[Johannes Choo]

I'm wondering if someone is aware of the existence of a formalization of this result (efficient UTM simulation), or if someone has pointers for me to search if this is something that has been done.

[Shreyas Srinivas]

As you point out, it is rather tedious to do which is why even on pen and paper, books tend to gloss over the construction of TMs as much as possible. There is a formalisation of Turing machines, but not of the encoding of TM + input into a UTM

[Shreyas Srinivas]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Computability/TuringMachine.html

[Shreyas Srinivas]

The way mathlib proves the undecidability of halting is by moving from Turing machines to partial recursive functions

[Shreyas Srinivas]

That being said, TMs are certainly not ignored in modern research. They're just always in the ambient context. For example, when one speaks of DLOGTIME-uniform AC0, it is implied that the Generator runs in DLOGTIME on a Turing machine.

[Johannes Choo]

Thanks for the link. Regarding my last comment, I misspoke, and didn't mean to say that TMs and their behavior itself isn't relevant to modern TCS; since indeed the details of TM variants are important in complexity theory. I meant to say that the typical construction of the O(n lg n) efficient TM and its data structure was probably not of research interest (correct me if I'm mistaken in that).

[Shreyas Srinivas]

I think efficiency issues really depend on what you want to accomplish with Turing machines. Independent of the universal TM simulation, there are many cases where you can't miss the log factors. This is true in space complexity and circuit complexity lower bounds in the logspace realm. Simulating UTMs with log n overhead is a special case of efficient simulations in general.

[Shreyas Srinivas]

I'd say it is still a useful building block in complexity research. It's one of the details that will be brushed under the carpet in most papers that refer to things like logspace reductions for example

[Johannes Choo]

Aah, I see, thanks

[Shreyas Srinivas]

One useful line of work is to work on composable TMs. There is an open PR that is looking to be adopted mathlib4#7172

[Johannes Choo]

Shreyas Srinivas said:

One useful line of work is to work on composable TMs. There is an open PR that is looking to be adopted mathlib4#7172

Thanks for the reference. I have been thinking about it in the back of my head while focused elsewhere, and indeed to make things manageable I think I would like to have a notion of composition on (TM, tape, arbitrary properties), I'm thinking something like Hoare logic on imperative pseudocode.