Documentation

CslibFrontier.Computability.Machines.Turing.MultiTape.Universal.WindowedComplexity

The universal function in time O(t log t) #

The universal function (Turing.MultiTapeTM.Universal.universal), on a description d, an input x and a number t of steps in binary, is computed by the windowed simulation (Turing.MultiTapeTM.Universal.Windowed.sim, see Turing.MultiTapeTM.Universal.Windowed.universal_eq_sim) run as a divide-and-conquer recursion (Turing.MultiTapeTM.ComputableInO.divConq). A problem is the description, a number of steps in unary and the windows. A problem of at most one step is solved by a windowed step; a larger one by its first half on the cut windows, pasted back, and then its second half likewise.

Let D be the length of the encoded description and M the largest input symbol. The windows of a problem of n steps, and those it computes, hold O(n) cells, each at most D + M + 1, and there are at most D + 1 of them (Turing.MultiTapeTM.Universal.Windowed.WInv). Cutting and pasting are linear in the encoded windows for each window, so a problem of n ≥ 2 steps costs O((D + M + 2) ^ 3 * (n + 1)) besides its halves, and a problem of at most one step O((D + M + 2) ^ 6). The recursion on t steps then costs O((D + M + 2) ^ 6 * (t + 1) * (log₂ (t + 1) + 1)). The first problem is computed in time linear in the encoded input plus O((D + 1) ^ 3 + (t + 1) * (log₂ (t + 1) + 1)).

The bound covers time and space alike; the space is not bounded separately here. It depends on the largest input symbol M because the input cells hold the symbols in unary.

For a fixed machine on inputs over a fixed alphabet this is the O(t log t) simulation overhead of Arora and Barak, Theorem 1.9, attributed there to Hennie and Stearns, with an additive term for reading the encoded input. It differs from that statement in several ways: the number of steps is an input (a clocked simulation, not a run until the simulated machine halts); the factor is an explicit polynomial in D and M rather than a constant depending on the machine's alphabet, tapes and states; the space is not bounded by the simulated machine's space; and the simulated model is the description format of Turing.MultiTapeTM.Universal.Desc, with a read-only input and an emitted output. The construction is an original divide-and-conquer windowed simulation, not the buffered tapes of Hennie and Stearns.

Main results #

References #

The divide-and-conquer form of the windowed simulation #

The parts #

The cost recurrence #

theorem Turing.MultiTapeTM.Universal.computableInO_universal_nlogn :
ComputableInO universal eIn eOut (fun (i : Desc × List ℕ × ℕ) => (eIn i).length + (descLen i.1 + listMax id i.2.1 + 2) ^ 6 * ((i.2.2 + 1) * (Nat.log 2 (i.2.2 + 1) + 1))) fun (i : Desc × List ℕ × ℕ) => (eIn i).length + (descLen i.1 + listMax id i.2.1 + 2) ^ 6 * ((i.2.2 + 1) * (Nat.log 2 (i.2.2 + 1) + 1))

The universal function in time O(t log t). For a description d of encoded length D, an input x with largest symbol M and t steps given in binary, the universal function is computable in time and space O(N + (D + M + 2) ^ 6 * (t + 1) * (log₂ (t + 1) + 1)), where N is the length of the encoded input (d, x, t).