Nondeterministic space within deterministic exponential time

A nondeterministic machine within space s is simulated deterministically within time 2 ^ O(log₂ n + s) Arora and Barak, Section 4.1 Sipser, Section 8.4: list the views reachable from the initial view by breadth-first search until no new view appears (Turing.MultiTapeNTM.reachableViews), and test whether one of them is accepting. The simulation holds for recognizers (Turing.MultiTapeNTM.RecognizesInSpace), whose branches need not halt; the class Cslib.Complexity.NSPACE uses the deciding form, so the inclusion holds for it a fortiori. The space bound need not be constructible: the search stops by itself, and the bound enters only the analysis. Arora and Barak state the theorem for space-constructible bounds, the convention they adopt for space classes; Sipser counts the configurations of a machine within space f(n). The sources are about deciders on strings; the statements here also cover nonhalting recognizers and arbitrary encoded instances.

Main results

• Turing.MultiTapeNTM.RecognizesInSpace.mem_DTIME: a problem recognized within space s is in DTIME (2 ^ (c * (log₂ n + s n + 1))).
• Cslib.Complexity.exists_mem_DTIME_of_mem_NSPACE: NSPACE s ⊆ DTIME (2 ^ O(log₂ n + s n)).
• Cslib.Complexity.exists_mem_DTIME_of_mem_NSPACE_of_log2_le: NSPACE s ⊆ DTIME (2 ^ O(s n)) when log₂ n ≤ s n.

References

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

theorem Turing.MultiTapeNTM.RecognizesInSpace.mem_DTIME {α : Type} {enc : α ↪ List Bool} {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} {A : Set α} {s : ℕ → ℕ} (h : ntm.RecognizesInSpace enc A fun (a : α) => s (enc a).length) : ∃ (c : ℕ), A ∈ Cslib.Complexity.DTIME enc fun (n : ℕ) => 2 ^ (c * (n.log2 + s n + 1))

Space-bounded nondeterministic recognizers are within exponential time Arora and Barak, Section 4.1 Sipser, Section 8.4: a problem recognized by a nondeterministic machine within space s n, whose branches need not halt, is decided deterministically within time 2 ^ (c * (log₂ n + s n + 1)) for a constant c of the machine. The space bound need not be constructible.

theorem Cslib.Complexity.exists_mem_DTIME_of_mem_NSPACE {α : Type} {enc : α ↪ List Bool} {s : ℕ → ℕ} {A : Set α} (h : A ∈ NSPACE enc s) : ∃ (c : ℕ), A ∈ DTIME enc fun (n : ℕ) => 2 ^ (c * (n.log2 + s n + 1))

Nondeterministic space is within deterministic exponential time Arora and Barak, Section 4.1 Sipser, Section 8.4: NSPACE s ⊆ DTIME (2 ^ O(log₂ n + s n)). The space bound need not be constructible.

theorem Cslib.Complexity.exists_mem_DTIME_of_mem_NSPACE_of_log2_le {α : Type} {enc : α ↪ List Bool} {s : ℕ → ℕ} {A : Set α} (hs : ∀ (n : ℕ), n.log2 ≤ s n) (h : A ∈ NSPACE enc s) : ∃ (c : ℕ), A ∈ DTIME enc fun (n : ℕ) => 2 ^ (c * s n)

Nondeterministic space is within deterministic exponential time above logarithmic space Arora and Barak, Section 4.1 Sipser, Section 8.4: NSPACE s ⊆ DTIME (2 ^ O(s n)) when log₂ n ≤ s n. The space bound need not be constructible.