One step of Savitch's stack machine

⚠️ Unreviewed by Bolton

The recursion of Savitch's theorem, written as a single polynomial-time function on the stack of Complexitylib.Classes.Containments.Internal.SavitchFrame.

A step does exactly one of five things.

• Publish — the done flag is set, so the answer is copied into the flag the iteration reads.
• Finish — the stack is empty, so the root's return value is the answer and the done flag goes up.
• Bottom out — the top frame's level is zero, so its subproblem is one step of the configuration graph; the frame is popped with its verdict.
• Descend — the top frame pushes the half of its interval it is currently trying.
• Return — a subcall has come back: a success either advances the frame to its second half or finishes it, and a failure advances the midpoint, giving up when the enumeration wraps.

Main definitions

• Complexity.baseReach, Complexity.baseAcc — the two base cases
• Complexity.savStep — one step of the recursion
• Complexity.savInit — the state the recursion starts from
• Complexity.savG — the function SpaceIter.mem_PSPACE_of_iterate iterates

Main results

• Complexity.savStep_mem_FP, Complexity.savG_mem_FP — a step is polynomial-time

Reading the state

def Complexity.savTop (s : List Bool) : List Bool

The frame on top of the state's stack.

Equations

• Complexity.savTop s = Complexity.stkTop (Complexity.stStk s)

def Complexity.savRest (s : List Bool) : List Bool

The stack below the top frame.

Equations

• Complexity.savRest s = Complexity.stkRest (Complexity.stStk s)

def Complexity.savRuler (k : ℕ) (R : List Bool) : List Bool

The wide ruler a whole configuration code is measured against.

Equations

• Complexity.savRuler k R = Complexity.wideRuler (Complexity.codeBlocks k) R

def Complexity.savZero (k : ℕ) (R : List Bool) : List Bool

The all-zero code: the first midpoint the enumeration tries.

Equations

• Complexity.savZero k R = Complexity.padTo (Complexity.savRuler k R) []

@[simp]

theorem Complexity.savZero_length (k : ℕ) (R : List Bool) : (savZero k R).length = codeBlocks k * R.length

The base cases

noncomputable def Complexity.baseReach {k : ℕ} (tm : NTM k) (R u v : List Bool) : List Bool

The base case of a reachability frame: v is u, or one step from it.

Equations

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

noncomputable def Complexity.baseAcc {k : ℕ} (tm : NTM k) (R rl u : List Bool) : List Bool

The base case of an acceptance frame: an accepting configuration is u, or one step from it.

Equations

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

theorem Complexity.baseReach_flag {k : ℕ} (tm : NTM k) (R u v : List Bool) : baseReach tm R u v = [true] ∨ baseReach tm R u v = [false]

theorem Complexity.baseAcc_flag {k : ℕ} (tm : NTM k) (R rl u : List Bool) : baseAcc tm R rl u = [true] ∨ baseAcc tm R rl u = [false]

The step

noncomputable def Complexity.savChild (k : ℕ) (s : List Bool) : List Bool

The child the top frame pushes: the first half of its interval while its phase is zero, the second half afterwards.

Equations

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

noncomputable def Complexity.savAdvance (s : List Bool) : List Bool

A failed subcall: try the next midpoint, or give up if the enumeration has wrapped.

Equations

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

noncomputable def Complexity.savReturn (s : List Bool) : List Bool

A returning subcall.

Equations

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

noncomputable def Complexity.savDescend {k : ℕ} (tm : NTM k) (s : List Bool) : List Bool

A descending step: bottom out, or push the half being tried.

Equations

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

noncomputable def Complexity.savStep {k : ℕ} (tm : NTM k) (s : List Bool) : List Bool

One step of Savitch's recursion.

Equations

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

The initial state

noncomputable def Complexity.savR (qp : Polynomial ℕ) (x : List Bool) : List Bool

The block ruler of the window, as a function of the input.

Equations

• Complexity.savR qp x = Complexity.polyRuler (2 * qp + 2) x

theorem Complexity.savR_eq (qp : Polynomial ℕ) (x : List Bool) : savR qp x = Cobham.blockRuler (Polynomial.eval x.length qp)

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

The state Savitch's recursion starts from: one acceptance frame, at the top level, on the code of the initial configuration.

Equations

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

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

The function the space-bounded iteration runs. The running state is the first component and the input the second, so the very first call — on pair [] x — is the one that builds the initial state.

Equations

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

@[simp]

theorem Complexity.savG_pair {k : ℕ} (tm : NTM k) (qp lp : Polynomial ℕ) (s x : List Bool) : savG tm qp lp (pair s x) = pair (Cobham.selectHead (emptyFlag s) (savInit tm qp lp x) (savStep tm s)) x

theorem Complexity.savG_nil {k : ℕ} (tm : NTM k) (qp lp : Polynomial ℕ) (x : List Bool) : savG tm qp lp (pair [] x) = pair (savInit tm qp lp x) x

theorem Complexity.savG_step {k : ℕ} (tm : NTM k) (qp lp : Polynomial ℕ) (s x : List Bool) (hs : s ≠ []) : savG tm qp lp (pair s x) = pair (savStep tm s) x

The step is polynomial-time

theorem Complexity.savRulerFn_mem_FP (k : ℕ) {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => savRuler k (a z)) ∈ FP

theorem Complexity.savZeroFn_mem_FP (k : ℕ) {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => savZero k (a z)) ∈ FP

theorem Complexity.baseReachFn_mem_FP {k : ℕ} (tm : NTM k) {Rf uf vf : List Bool → List Bool} (hR : Rf ∈ FP) (hu : uf ∈ FP) (hv : vf ∈ FP) : (fun (z : List Bool) => baseReach tm (Rf z) (uf z) (vf z)) ∈ FP

theorem Complexity.baseAccFn_mem_FP {k : ℕ} (tm : NTM k) {Rf rlf uf : List Bool → List Bool} (hR : Rf ∈ FP) (hrl : rlf ∈ FP) (hu : uf ∈ FP) : (fun (z : List Bool) => baseAcc tm (Rf z) (rlf z) (uf z)) ∈ FP

theorem Complexity.savStep_mem_FP {k : ℕ} (tm : NTM k) : savStep tm ∈ FP

theorem Complexity.savRFn_mem_FP (qp : Polynomial ℕ) {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => savR qp (a z)) ∈ FP

theorem Complexity.savInitFn_mem_FP {k : ℕ} (tm : NTM k) (qp lp : Polynomial ℕ) {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => savInit tm qp lp (a z)) ∈ FP

theorem Complexity.savG_mem_FP {k : ℕ} (tm : NTM k) (qp lp : Polynomial ℕ) : savG tm qp lp ∈ FP