Savitch's machine

⚠️ Unreviewed by Bolton

Everything is in place: Complexity.savG is the polynomial-time function Complexity.SpaceIter.mem_PSPACE_of_iterate wants, Complexity.Sav.run_top says its orbit reaches an answer, Complexity.Sav.runBound_le bounds how long that takes, and Complexity.Sav.StkSize bounds how much room it needs. This file puts them together.

Main results

• Complexity.savitch_mem_PSPACE — a language whose membership is reachability within 2 ^ poly steps of a space-bounded machine is in PSPACE

The run at a fixed input

noncomputable def Complexity.savSemAt {k : ℕ} (tm : NTM k) (qp : Polynomial ℕ) (x : List Bool) : Sav.Sst → Sav.Sst

The abstract step Complexity.savG performs, at the ruler it builds.

Equations

• Complexity.savSemAt tm qp x = Complexity.savSem tm (Complexity.savR qp x)

noncomputable def Complexity.savAns {k : ℕ} (tm : NTM k) (qp lp : Polynomial ℕ) (x : List Bool) : Bool

The answer the recursion returns at x.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.SavRunSpec {k : ℕ} (tm : NTM k) (qp lp : Polynomial ℕ) (x : List Bool) (T : ℕ) : Prop

What a run of T steps at x achieves: the flag stays down, then goes up, then becomes the answer.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.savRun_exists {k : ℕ} (tm : NTM k) (qp lp : Polynomial ℕ) (x : List Bool) : ∃ (T : ℕ), SavRunSpec tm qp lp x T

noncomputable def Complexity.savT {k : ℕ} (tm : NTM k) (qp lp : Polynomial ℕ) (x : List Bool) : ℕ

The number of steps Savitch's recursion takes at x.

Equations

• Complexity.savT tm qp lp x = Classical.choose ⋯

theorem Complexity.savT_spec {k : ℕ} (tm : NTM k) (qp lp : Polynomial ℕ) (x : List Bool) : SavRunSpec tm qp lp x (savT tm qp lp x)

The pieces of the space-bounded iteration

theorem Complexity.frameVal_savRoot {k : ℕ} (tm : NTM k) {L : Language} {S : ℕ → ℕ} (hdec : tm.DecidesInSpace L S) (qp lp : Polynomial ℕ) (hqp : ∀ (n : ℕ), n + S n + 1 ≤ Polynomial.eval n qp) (hcardq : ∀ (n : ℕ), Fintype.card tm.Q ≤ Cobham.blockWidth (Polynomial.eval n qp)) (x : List Bool) (hmem : x ∈ L ↔ ∃ (c : Cfg k tm.Q), tm.ReachesCfgLe (2 ^ Polynomial.eval x.length lp) (tm.initCfg x) c ∧ tm.halted c ∧ c.output.cells 1 = Γ.one) : savAns tm qp lp x = true ↔ x ∈ L

The answer the recursion returns is membership.

The whole containment

theorem Complexity.savitch_mem_PSPACE {k : ℕ} (tm : NTM k) {L : Language} {S : ℕ → ℕ} (hdec : tm.DecidesInSpace L S) (qp lp r w : Polynomial ℕ) (hqp : ∀ (n : ℕ), n + S n + 1 ≤ Polynomial.eval n qp) (hcardq : ∀ (n : ℕ), Fintype.card tm.Q ≤ Cobham.blockWidth (Polynomial.eval n qp)) (hmem : ∀ (x : List Bool), x ∈ L ↔ ∃ (c : Cfg k tm.Q), tm.ReachesCfgLe (2 ^ Polynomial.eval x.length lp) (tm.initCfg x) c ∧ tm.halted c ∧ c.output.cells 1 = Γ.one) (hr : ∀ (n : ℕ), 2 * (2 * (2 * Polynomial.eval n qp + 2) + (Polynomial.eval n lp + 1) * (2 * (2 * Polynomial.eval n lp + 5 * (codeBlocks k * (2 * Polynomial.eval n qp + 2)) + 14) + 2) + 14) + 2 + n ≤ Polynomial.eval n r) (hw : ∀ (n : ℕ), (codeBlocks k * (2 * Polynomial.eval n qp + 2) + 3) * Polynomial.eval n lp + 2 ≤ Polynomial.eval n w) : L ∈ PSPACE

Savitch's machine. A language whose membership is reachability within 2 ^ lp(|x|) steps of a machine bounded by S is in PSPACE.

The containment

noncomputable def Complexity.savWidthPoly (cardQ : ℕ) (p : Polynomial ℕ) : Polynomial ℕ

The polynomial bounding the width of the window Savitch's machine writes on.

Equations

• Complexity.savWidthPoly cardQ p = Polynomial.X + p + Polynomial.C 1 + Polynomial.C cardQ

noncomputable def Complexity.savStatePoly (k : ℕ) (qp lp : Polynomial ℕ) : Polynomial ℕ

The polynomial bounding the length of the state Savitch's machine carries.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.savCountPoly (k : ℕ) (qp lp : Polynomial ℕ) : Polynomial ℕ

The polynomial bounding the logarithm of the number of steps it takes.

Equations

• Complexity.savCountPoly k qp lp = (Polynomial.C (Complexity.codeBlocks k) * (2 * qp + 2) + 3) * lp + 2

theorem Complexity.savWidthPoly_eval (cardQ : ℕ) (p : Polynomial ℕ) (n : ℕ) : Polynomial.eval n (savWidthPoly cardQ p) = n + Polynomial.eval n p + 1 + cardQ

theorem Complexity.savStatePoly_eval (k : ℕ) (qp lp : Polynomial ℕ) (n : ℕ) : Polynomial.eval n (savStatePoly k qp lp) = 2 * (2 * (2 * Polynomial.eval n qp + 2) + (Polynomial.eval n lp + 1) * (2 * (2 * Polynomial.eval n lp + 5 * (codeBlocks k * (2 * Polynomial.eval n qp + 2)) + 14) + 2) + 14) + 2 + n

theorem Complexity.savCountPoly_eval (k : ℕ) (qp lp : Polynomial ℕ) (n : ℕ) : Polynomial.eval n (savCountPoly k qp lp) = (codeBlocks k * (2 * Polynomial.eval n qp + 2) + 3) * Polynomial.eval n lp + 2

theorem Complexity.NPSPACE_subset_PSPACE_internal : NPSPACE ⊆ PSPACE

NPSPACE ⊆ PSPACE (Savitch's theorem).