theorem
SpaceComplexity.LADDER_DFA_in_SPACE_n2
{α σ : Type}
[Fintype α]
[DecidableEq α]
[Fintype σ]
[DecidableEq σ]
(B : DFA α σ)
:
InSPACE (fun (n : ℕ) => n ^ 2) (LADDER_DFA_Lang B)
Theorem (Sipser, Lecture 17). LADDER_DFA ∈ SPACE(n²).
Applying Savitch's Theorem (NSPACE(f(n)) ⊆ SPACE(f(n)²)) to the linear-space NTM bound
LADDER_DFA ∈ NSPACE(n) gives a deterministic decision procedure using O(n²) space.
Intuitively: a recursive procedure for the bounded ladder problem uses O(n) space per level
and O(log t) = O(n) recursion depth, for a total of O(n²) space.
theorem
SpaceComplexity.LADDER_DFA_in_PSPACE
{α σ : Type}
[Fintype α]
[DecidableEq α]
[Fintype σ]
[DecidableEq σ]
(B : DFA α σ)
:
Theorem (Sipser, Lecture 17). LADDER_DFA ∈ PSPACE. This follows immediately from
LADDER_DFA ∈ SPACE(n²) since PSPACE = ⋃_k SPACE(n^k).