Nondeterministic logarithmic space is within polynomial time

A nondeterministic machine within space s is decided deterministically within time 2 ^ O(log₂ n + s) by breadth-first search through its reachable views (Turing.MultiTapeNTM.RecognizesInSpace.mem_DTIME). Within logarithmic space this time is polynomial (Cslib.Complexity.DTIME_two_pow_mul_log2_succ_subset). So NL ⊆ P Sipser, Section 8.5, and with Cslib.Complexity.L_subset_NL the chain L ⊆ NL ⊆ P.

Main results

• Cslib.Complexity.mem_P_of_recognizesInSpace: logspace recognizers, whose branches need not halt, are within polynomial time.
• Cslib.Complexity.NL_subset_P: nondeterministic logarithmic space is within polynomial time.

References

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

theorem Cslib.Complexity.mem_P_of_recognizesInSpace {α : Type} {enc : α ↪ List Bool} {k : ℕ} {State : Type} [Finite State] {ntm : Turing.MultiTapeNTM k Bool State} {A : Set α} {c : ℕ} (h : ntm.RecognizesInSpace enc A fun (a : α) => c * ((enc a).length.log2 + 1)) : A ∈ P enc

Logspace recognizers are within polynomial time: a problem recognized by a nondeterministic machine within logarithmic space, whose branches need not halt, is in P, by breadth-first search through the polynomially many reachable views.

theorem Cslib.Complexity.NL_subset_P {α : Type} {enc : α ↪ List Bool} : NL enc ⊆ P enc

Nondeterministic logarithmic space is within polynomial time: breadth-first search through the polynomially many reachable views decides acceptance.