The step bound Savitch's recursion starts from

⚠️ Unreviewed by Bolton

Complexitylib.Classes.Containments.Internal.ReachIn halves a step bound; this file supplies the bound to start from. A machine using polynomial space has at most 2 ^ poly configurations, so reachability is always witnessed within 2 ^ poly steps, and halving that bound bottoms out after poly levels. That is the whole reason Savitch's recursion is affordable: its depth is polynomial and each level stores one configuration, itself of polynomial size.

Main definitions

• codeExpBound — a polynomial dominating the exponent of the configuration count

Main results

• card_Code_le_two_pow_poly — the configuration count is 2 to a polynomial
• NPSPACE_bounded_reachability_internal — membership is reachability within 2 ^ poly steps
• NPSPACE_subset_PSPACE_of_recursion_internal — the containment, modulo one machine

noncomputable def Complexity.codeExpBound (cardQ k : ℕ) (p : Polynomial ℕ) : Polynomial ℕ

A polynomial dominating the exponent of the configuration count of a machine with cardQ states, k work tapes, and space bounded by p.

Equations

• Complexity.codeExpBound cardQ k p = Polynomial.C cardQ + (Polynomial.X + p + Polynomial.C 2) + Polynomial.C (3 * k) * (p + 1) + Polynomial.C 3 * (p + Polynomial.C 2)

theorem Complexity.card_Code_le_two_pow_poly (Q : Type) [Fintype Q] (k : ℕ) (S : ℕ → ℕ) (p : Polynomial ℕ) (hS : ∀ (n : ℕ), S n ≤ Polynomial.eval n p) (n : ℕ) : Fintype.card (Code Q k n (S n)) ≤ 2 ^ Polynomial.eval n (codeExpBound (Fintype.card Q) k p)

The configuration count is 2 to a polynomial.

theorem Complexity.NPSPACE_bounded_reachability_internal {L : Language} (hL : L ∈ NPSPACE) : ∃ (k : ℕ) (tm : NTM k) (q : Polynomial ℕ), ∀ (x : List Bool), x ∈ L ↔ ∃ (c : Cfg k tm.Q), tm.ReachesCfgLe (2 ^ Polynomial.eval x.length q) (tm.initCfg x) c ∧ tm.halted c ∧ c.output.cells 1 = Γ.one

A language in NPSPACE is reachability within 2 ^ poly steps. This is the input to Savitch's recursion: halving the bound 2 ^ q(|x|) bottoms out after q(|x|) levels, so the recursion depth is polynomial.

theorem Complexity.NPSPACE_subset_PSPACE_of_recursion_internal (h : ∀ (k : ℕ) (tm : NTM k) (S : ℕ → ℕ) (L₀ : Language) (m : ℕ) (q : Polynomial ℕ), tm.DecidesInSpace L₀ S → (BigO S fun (x : ℕ) => x ^ m) → ∃ (k' : ℕ) (M : TM k') (r : Polynomial ℕ), (∀ (x : List Bool) (c' : Cfg k' M.Q), M.reaches (M.initCfg x) c' → c'.WithinDecisionSpace x.length (Polynomial.eval x.length r)) ∧ ∀ (x : List Bool), ∃ (c' : Cfg k' M.Q), M.reaches (M.initCfg x) c' ∧ M.halted c' ∧ ((∃ (c : Cfg k tm.Q), tm.ReachesCfgLe (2 ^ Polynomial.eval x.length q) (tm.initCfg x) c ∧ tm.halted c ∧ c.output.cells 1 = Γ.one) → c'.output.cells 1 = Γ.one) ∧ ((¬∃ (c : Cfg k tm.Q), tm.ReachesCfgLe (2 ^ Polynomial.eval x.length q) (tm.initCfg x) c ∧ tm.halted c ∧ c.output.cells 1 = Γ.one) → c'.output.cells 1 = Γ.zero)) : NPSPACE ⊆ PSPACE

NPSPACE ⊆ PSPACE, reduced to the existence of one machine. The hypothesis carries the space witness for tm: without it the configuration graph is unbounded and the step bound 2 ^ q(|x|) is not enough to make the search decidable in polynomial space.