Time bounds for space-bounded computations

A halting computation within a space bound depending on the encoded input length can be given a time bound depending only on that length, without increasing its space. The bound counts the machine's readable configurations: the input head position and work-tape storage. This is the encoded-function form of the space-to-time inclusion in cslib pull request #767, using the configuration count of Turing.MultiTapeTM.haltsAt_le_card.

Main results

• Turing.MultiTapeTM.ComputableInTimeAndSpace.exists_time_of_length: replace an arbitrary time bound by a bound on the encoded input length.
• Turing.MultiTapeTM.ComputableInTimeAndSpace.exists_time_two_pow: the time is at most (n + 2) * c * 2 ^ (c * s n) for a machine-dependent constant c.

References

• M. Sipser, Introduction to the Theory of Computation, Section 8.4
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 4.1

theorem Turing.MultiTapeTM.ComputableInTimeAndSpace.exists_time_of_length {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} {t : α → ℕ} {s : ℕ → ℕ} (h : ComputableInTimeAndSpace f encIn encOut t fun (a : α) => s (encIn a).length) : ∃ (t' : ℕ → ℕ), ComputableInTimeAndSpaceOfLength f encIn encOut t' s

A computation within space s n halts within a time bound of n. A function computable within space s n on encoded inputs of length n, within any time bound, is computable within the same space and some time bound that depends only on n; for an explicit bound see Turing.MultiTapeTM.ComputableInTimeAndSpace.exists_time_two_pow.

theorem Turing.MultiTapeTM.ComputableInTimeAndSpace.exists_time_two_pow {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} {t : α → ℕ} {s : ℕ → ℕ} (h : ComputableInTimeAndSpace f encIn encOut t fun (a : α) => s (encIn a).length) : ∃ (c : ℕ), ComputableInTimeAndSpaceOfLength f encIn encOut (fun (n : ℕ) => (n + 2) * c * 2 ^ (c * s n)) s

The configuration-counting bound: a function computable within space s n on encoded inputs of length n is computable within the same space and time (n + 2) * c * 2 ^ (c * s n), for a constant c of the machine.