Savitch's theorem: NPSPACE = PSPACE

Every problem decided by a nondeterministic machine within polynomial space is decided by a deterministic machine within polynomial space: Savitch's decider (Turing.MultiTapeNTM.savitchDecide), which runs his midpoint recursion with an explicit stack on the codes of the finite views of the nondeterministic machine. With the converse inclusion, NPSPACE = PSPACE Sipser, remark after Definition 8.6. Both classes are machine-defined: the deterministic class by plain total decision within polynomial space, the nondeterministic class by accepting computation paths, with every computation path within the space bound and every branch halting. The simulation uses only the space bound and acceptance, so it applies to recognizers, whose branches may run forever (Cslib.Complexity.mem_PSPACE_of_recognizesInSpace).

Main results

• Cslib.Complexity.mem_PSPACE_of_recognizesInSpace: Savitch's theorem for recognizers, whose branches need not halt.
• Cslib.Complexity.NPSPACE_subset_PSPACE: Savitch's theorem for polynomial space.
• Cslib.Complexity.NPSPACE_eq_PSPACE: the two classes are equal.

References

• M. Sipser, Introduction to the Theory of Computation, Theorem 8.5 and the remark after Definition 8.6
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 4.2

theorem Cslib.Complexity.mem_PSPACE_of_recognizesInSpace {α : Type} {enc : α ↪ List Bool} {k : ℕ} {State : Type} [Finite State] {ntm : Turing.MultiTapeNTM k Bool State} {A : Set α} {s : α → ℕ} (hs : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (enc a).length) s) (hA : ntm.RecognizesInSpace enc A s) : A ∈ PSPACE enc

Savitch's theorem for recognizers: a problem recognized by a nondeterministic machine within polynomial space, whose branches need not halt, is in PSPACE.

theorem Cslib.Complexity.NPSPACE_subset_PSPACE {α : Type} {enc : α ↪ List Bool} : NPSPACE enc ⊆ PSPACE enc

Savitch's theorem for polynomial space: every problem decided by a nondeterministic machine within polynomial space is decided by a deterministic machine within polynomial space, namely Savitch's decider Sipser, Theorem 8.5.

theorem Cslib.Complexity.NPSPACE_eq_PSPACE {α : Type} {enc : α ↪ List Bool} : NPSPACE enc = PSPACE enc

NPSPACE = PSPACE Sipser, remark after Definition 8.6.