The abstract semantics of Savitch's stack machine

⚠️ Unreviewed by Bolton

Complexitylib.Classes.Containments.Internal.SavitchStep writes Savitch's recursion as a polynomial-time function on a bitstring. This file gives the same recursion on an ordinary inductive state — a List of frames rather than a right-nested chain of pairs — where its correctness and its running time can be proved by induction without any encoding in the way.

The machine is parametric in the two base tests it calls, br (is v within one step of u) and ba (is u accepting, or within one step of accepting), and in the all-zero code z, which is both the first midpoint every frame tries and the width the enumeration wraps at.

Main definitions

• Complexity.Sav.Frm, Complexity.Sav.Sst — a frame and the machine's state
• Complexity.Sav.step — one step of the recursion
• Complexity.Sav.rchB, Complexity.Sav.accB — what the recursion computes
• Complexity.Sav.frameVal — the value a frame is going to return
• Complexity.Sav.runBound — the number of steps a level costs

Main results

• Complexity.Sav.run_frame — a frame pushed on the stack is popped again, with its value, within runBound steps, and the done flag stays down throughout

The state

structure Complexity.Sav.Frm : Type

A frame of Savitch's recursion: which subproblem it is working on (kind), which half of the interval it is trying (ph), the level in unary (lvl), the two endpoints (u, v) and the midpoint being tried (m).

• kind : Bool

  true for is an accepting configuration reachable from u, false for is v reachable from u.

• ph : Bool

  false while the first half of the interval is being tried.

• lvl : List Bool

  The level, in unary: 2 ^ lvl.length steps are allowed.

• u : List Bool

  The source endpoint.

• v : List Bool

  The target endpoint; unused by an acceptance frame.

• m : List Bool

  The midpoint being tried, which doubles as the enumeration's counter.

structure Complexity.Sav.Sst : Type

The machine's state: the done flag, the answer, the value a finished subcall is returning (none while descending), and the stack.

• done : Bool

  The bit the space-bounded iteration watches.

• ans : Bool

  The answer, once it is known.

• ret : Option Bool

  The value a finished subcall is returning.

• stk : List Frm

  The stack, top frame first.

One step

def Complexity.Sav.child (z : List Bool) (f : Frm) : Frm

The child a 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.

def Complexity.Sav.baseVal (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (f : Frm) : Bool

The value a level-zero frame returns.

Equations

• Complexity.Sav.baseVal br ba f = if f.kind = true then ba f.u else br f.u f.v

def Complexity.Sav.step (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) (s : Sst) : Sst

One step of Savitch's recursion, on the abstract state.

Equations

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

@[simp]

theorem Complexity.Sav.step_of_done (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) (a : Bool) (r : Option Bool) (stk : List Frm) : step br ba z { done := true, ans := a, ret := r, stk := stk } = { done := a, ans := a, ret := r, stk := stk }

@[simp]

theorem Complexity.Sav.step_of_empty (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) (a : Bool) (r : Option Bool) : step br ba z { done := false, ans := a, ret := r, stk := [] } = { done := true, ans := r.getD false, ret := r, stk := [] }

theorem Complexity.Sav.step_base (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) (a : Bool) (f : Frm) (fs : List Frm) (h : f.lvl = []) : step br ba z { done := false, ans := a, ret := none, stk := f :: fs } = { done := false, ans := a, ret := some (baseVal br ba f), stk := fs }

theorem Complexity.Sav.step_push (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) (a : Bool) (f : Frm) (fs : List Frm) (h : f.lvl ≠ []) : step br ba z { done := false, ans := a, ret := none, stk := f :: fs } = { done := false, ans := a, ret := none, stk := child z f :: f :: fs }

theorem Complexity.Sav.step_ret_true_ph (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) (a : Bool) (f : Frm) (fs : List Frm) (h : f.ph = true) : step br ba z { done := false, ans := a, ret := some true, stk := f :: fs } = { done := false, ans := a, ret := some true, stk := fs }

theorem Complexity.Sav.step_ret_true_of_ph_false (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) (a : Bool) (f : Frm) (fs : List Frm) (h : f.ph = false) : step br ba z { done := false, ans := a, ret := some true, stk := f :: fs } = { done := false, ans := a, ret := none, stk := { kind := f.kind, ph := true, lvl := f.lvl, u := f.u, v := f.v, m := f.m } :: fs }

theorem Complexity.Sav.step_ret_false_over (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) (a : Bool) (f : Frm) (fs : List Frm) (h : bumpOver f.m = true) : step br ba z { done := false, ans := a, ret := some false, stk := f :: fs } = { done := false, ans := a, ret := some false, stk := fs }

theorem Complexity.Sav.step_ret_false_bump (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) (a : Bool) (f : Frm) (fs : List Frm) (h : bumpOver f.m = false) : step br ba z { done := false, ans := a, ret := some false, stk := f :: fs } = { done := false, ans := a, ret := none, stk := { kind := f.kind, ph := false, lvl := f.lvl, u := f.u, v := f.v, m := bumpBits f.m } :: fs }

What the recursion computes

def Complexity.Sav.anyMid (P : List Bool → Bool) : List Bool → ℕ → Bool

Try j successive midpoints, starting at m.

Equations

• Complexity.Sav.anyMid P x✝ 0 = false
• Complexity.Sav.anyMid P x✝ j.succ = (P x✝ || Complexity.Sav.anyMid P (Complexity.bumpBits x✝) j)

@[simp]

theorem Complexity.Sav.anyMid_zero (P : List Bool → Bool) (m : List Bool) : anyMid P m 0 = false

@[simp]

theorem Complexity.Sav.anyMid_succ (P : List Bool → Bool) (m : List Bool) (j : ℕ) : anyMid P m (j + 1) = (P m || anyMid P (bumpBits m) j)

def Complexity.Sav.rchB (br : List Bool → List Bool → Bool) (z : List Bool) : ℕ → List Bool → List Bool → Bool

Reachability within 2 ^ n steps, as the recursion computes it.

Equations

• Complexity.Sav.rchB br z 0 x✝¹ x✝ = br x✝¹ x✝
• Complexity.Sav.rchB br z n.succ x✝¹ x✝ = Complexity.Sav.anyMid (fun (m : List Bool) => Complexity.Sav.rchB br z n x✝¹ m && Complexity.Sav.rchB br z n m x✝) z (2 ^ z.length)

def Complexity.Sav.accB (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) : ℕ → List Bool → Bool

Acceptance within 2 ^ n steps, as the recursion computes it.

Equations

• Complexity.Sav.accB br ba z 0 x✝ = ba x✝
• Complexity.Sav.accB br ba z n.succ x✝ = Complexity.Sav.anyMid (fun (m : List Bool) => Complexity.Sav.rchB br z n x✝ m && Complexity.Sav.accB br ba z n m) z (2 ^ z.length)

def Complexity.Sav.midRem (m : List Bool) : ℕ

The number of midpoints a frame has still to try.

Equations

• Complexity.Sav.midRem m = 2 ^ m.length - Complexity.binValLE m

theorem Complexity.Sav.midRem_pos (m : List Bool) : 0 < midRem m

theorem Complexity.Sav.midRem_le (m : List Bool) : midRem m ≤ 2 ^ m.length

theorem Complexity.Sav.midRem_of_over {m : List Bool} (h : bumpOver m = true) : midRem m = 1

theorem Complexity.Sav.midRem_bump {m : List Bool} (h : bumpOver m = false) : midRem (bumpBits m) + 1 = midRem m

theorem Complexity.Sav.midRem_zero {m : List Bool} (h : binValLE m = 0) : midRem m = 2 ^ m.length

def Complexity.Sav.frameValAux (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) (kind : Bool) (lvl u v m : List Bool) : Bool

The value the frame f is going to return, given the state it is in.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.Sav.frameValAux br ba z kind [] u v m = if kind = true then ba u else br u v

def Complexity.Sav.frameVal (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) (f : Frm) : Bool

The value the frame f is going to return.

Equations

• Complexity.Sav.frameVal br ba z f = Complexity.Sav.frameValAux br ba z f.kind f.lvl f.u f.v f.m

theorem Complexity.Sav.frameVal_of_nil (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) {f : Frm} (h : f.lvl = []) : frameVal br ba z f = baseVal br ba f

theorem Complexity.Sav.frameVal_of_cons (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) {f : Frm} {b : Bool} {t : List Bool} (h : f.lvl = b :: t) : frameVal br ba z f = anyMid (fun (w : List Bool) => rchB br z t.length f.u w && if f.kind = true then accB br ba z t.length w else rchB br z t.length w f.v) f.m (midRem f.m)

theorem Complexity.Sav.frameVal_fresh (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) {f : Frm} (hz : binValLE z = 0) (hm : f.m = z) : frameVal br ba z f = if f.kind = true then accB br ba z f.lvl.length f.u else rchB br z f.lvl.length f.u f.v

A fresh frame — phase zero, midpoint at the bottom of the enumeration — returns exactly the value its level asks for.

The invariant a frame carries

structure Complexity.Sav.FrmOk (br : List Bool → List Bool → Bool) (z : List Bool) (f : Frm) : Prop

A frame is well formed when its midpoint has the enumeration's width and, once its phase has advanced, its first half really did succeed.

• mlen : f.m.length = z.length

  The midpoint is a code.

• phase : f.ph = true → rchB br z (f.lvl.length - 1) f.u f.m = true

  The first half succeeded before the phase advanced.

The number of steps

def Complexity.Sav.runBound (W : ℕ) : ℕ → ℕ

The steps a frame at level n costs, over an enumeration of width W.

Equations

• Complexity.Sav.runBound W 0 = 1
• Complexity.Sav.runBound W n.succ = (2 * 2 ^ W + 1) * (Complexity.Sav.runBound W n + 2)

def Complexity.Sav.mu (f : Frm) : ℕ

How much work a frame has left, within its level.

Equations

• Complexity.Sav.mu f = 2 * Complexity.Sav.midRem f.m + if f.ph = true then 0 else 1

theorem Complexity.Sav.mu_of_ph_true {f : Frm} (h : f.ph = true) : mu f = 2 * midRem f.m

theorem Complexity.Sav.mu_of_ph_false {f : Frm} (h : f.ph = false) : mu f = 2 * midRem f.m + 1

theorem Complexity.Sav.mu_pos (f : Frm) : 0 < mu f

theorem Complexity.Sav.mu_le (z : List Bool) {f : Frm} (h : f.m.length = z.length) : mu f ≤ 2 * 2 ^ z.length + 1

The done flag stays down

def Complexity.Sav.DoneDown (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) (s : Sst) (T : ℕ) : Prop

The done flag is down at every point of the first T steps from s.

Equations

• Complexity.Sav.DoneDown br ba z s T = ∀ j ≤ T, ((Complexity.Sav.step br ba z)^[j] s).done = false

theorem Complexity.Sav.doneDown_zero (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) {s : Sst} (h : s.done = false) : DoneDown br ba z s 0

theorem Complexity.Sav.doneDown_add (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) {s : Sst} {T₁ T₂ : ℕ} (h₁ : DoneDown br ba z s T₁) (h₂ : DoneDown br ba z ((step br ba z)^[T₁] s) T₂) : DoneDown br ba z s (T₁ + T₂)

theorem Complexity.Sav.doneDown_succ (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) {s : Sst} {T : ℕ} (h : DoneDown br ba z s T) (h' : ((step br ba z)^[T + 1] s).done = false) : DoneDown br ba z s (T + 1)

Unfolding a frame's value

@[simp]

theorem Complexity.Sav.child_lvl (z : List Bool) (f : Frm) : (child z f).lvl = List.drop 1 f.lvl

@[simp]

theorem Complexity.Sav.child_m (z : List Bool) (f : Frm) : (child z f).m = z

@[simp]

theorem Complexity.Sav.child_ph (z : List Bool) (f : Frm) : (child z f).ph = false

theorem Complexity.Sav.frameVal_child_of_ph_false (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) (hz : binValLE z = 0) {f : Frm} (h : f.ph = false) : frameVal br ba z (child z f) = rchB br z (f.lvl.length - 1) f.u f.m

theorem Complexity.Sav.frameVal_child_of_ph_true (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) (hz : binValLE z = 0) {f : Frm} (h : f.ph = true) : frameVal br ba z (child z f) = if f.kind = true then accB br ba z (f.lvl.length - 1) f.m else rchB br z (f.lvl.length - 1) f.m f.v

def Complexity.Sav.midVal (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) (n : ℕ) (f : Frm) : Bool

The candidate a frame is currently testing.

Equations

• Complexity.Sav.midVal br ba z n f = (Complexity.Sav.rchB br z n f.u f.m && if f.kind = true then Complexity.Sav.accB br ba z n f.m else Complexity.Sav.rchB br z n f.m f.v)

theorem Complexity.Sav.frameVal_of_last (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) {f : Frm} {b : Bool} {t : List Bool} (hl : f.lvl = b :: t) (hov : bumpOver f.m = true) : frameVal br ba z f = midVal br ba z t.length f

theorem Complexity.Sav.frameVal_of_bump (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) {f : Frm} {b : Bool} {t : List Bool} (hl : f.lvl = b :: t) (hov : bumpOver f.m = false) : frameVal br ba z f = (midVal br ba z t.length f || frameVal br ba z { kind := f.kind, ph := false, lvl := f.lvl, u := f.u, v := f.v, m := bumpBits f.m })

theorem Complexity.Sav.frameVal_of_mid (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) {f : Frm} {b : Bool} {t : List Bool} (hl : f.lvl = b :: t) (h : midVal br ba z t.length f = true) : frameVal br ba z f = true

Runs

def Complexity.Sav.RunsTo (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) (f : Frm) (fs : List Frm) (a : Bool) (T : ℕ) : Prop

The frame f, pushed on top of fs, is popped again with its value after exactly T steps, and the done flag stays down throughout.

Equations

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

theorem Complexity.Sav.runsTo_prepend (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) {f g : Frm} {fs : List Frm} {a : Bool} {T₀ T₁ : ℕ} (hd : DoneDown br ba z { done := false, ans := a, ret := none, stk := f :: fs } T₀) (hs : (step br ba z)^[T₀] { done := false, ans := a, ret := none, stk := f :: fs } = { done := false, ans := a, ret := none, stk := g :: fs }) (hr : RunsTo br ba z g fs a T₁) (hval : frameVal br ba z g = frameVal br ba z f) : RunsTo br ba z f fs a (T₁ + T₀)

A run that begins by re-entering a frame of the same value.

theorem Complexity.Sav.child_phase (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) {f : Frm} {fs : List Frm} {a : Bool} {Tc : ℕ} {s : Sst} (hne : f.lvl ≠ []) (hc : RunsTo br ba z (child z f) (f :: fs) a Tc) (hstep : step br ba z { done := false, ans := a, ret := some (frameVal br ba z (child z f)), stk := f :: fs } = s) (hsdone : s.done = false) : DoneDown br ba z { done := false, ans := a, ret := none, stk := f :: fs } (Tc + 1 + 1) ∧ (step br ba z)^[Tc + 1 + 1] { done := false, ans := a, ret := none, stk := f :: fs } = s

Pushing a frame's child, running it, and processing its return.

Every pushed frame comes back

theorem Complexity.Sav.run_frame (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) (hz : binValLE z = 0) (n : ℕ) (f : Frm) : f.lvl.length = n → FrmOk br z f → ∀ (fs : List Frm) (a : Bool), ∃ T ≤ runBound z.length n, RunsTo br ba z f fs a T

Every pushed frame comes back. A frame at level n is popped again, carrying its value, within runBound steps, and the done flag stays down for the whole of that run.

The enumeration covers every candidate

theorem Complexity.Sav.anyMid_of_lt {P : List Bool → Bool} {m : List Bool} {i j : ℕ} (hij : i < j) (h : P (bumpBits^[i] m) = true) : anyMid P m j = true

theorem Complexity.Sav.exists_of_anyMid {P : List Bool → Bool} {m : List Bool} {j : ℕ} (h : anyMid P m j = true) : ∃ i < j, P (bumpBits^[i] m) = true

theorem Complexity.Sav.anyMid_of_length {P : List Bool → Bool} {z w : List Bool} (hz : binValLE z = 0) (hw : w.length = z.length) (h : P w = true) : anyMid P z (2 ^ z.length) = true

Every string of the enumeration's width is tried.

The stack invariant the encoding needs

def Complexity.Sav.StkOk (s : Sst) : Prop

Nothing is returning only while the stack is nonempty.

Equations

• Complexity.Sav.StkOk s = (s.stk = [] → s.ret ≠ none)

theorem Complexity.Sav.step_stkOk (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) {s : Sst} (h : StkOk s) : StkOk (step br ba z s)

The number of steps is at most exponential in a polynomial

theorem Complexity.Sav.runBound_pos (W n : ℕ) : 0 < runBound W n

theorem Complexity.Sav.runBound_le (W n : ℕ) : runBound W n + 2 ≤ 2 ^ ((W + 3) * n + 2)

The whole run

theorem Complexity.Sav.run_top (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) (hz : binValLE z = 0) (root : Frm) (hok : FrmOk br z root) : ∃ T ≤ runBound z.length root.lvl.length, (∀ j ≤ T, ((step br ba z)^[j] { done := false, ans := false, ret := none, stk := [root] }).done = false) ∧ (step br ba z)^[T + 1] { done := false, ans := false, ret := none, stk := [root] } = { done := true, ans := frameVal br ba z root, ret := some (frameVal br ba z root), stk := [] } ∧ (step br ba z)^[T + 2] { done := false, ans := false, ret := none, stk := [root] } = { done := frameVal br ba z root, ans := frameVal br ba z root, ret := some (frameVal br ba z root), stk := [] }

The recursion terminates with its answer. From the state carrying one frame, the machine keeps its done flag down for T steps, raises it on the next one, and one step later the flag is the answer.

The size of the state

def Complexity.Sav.FrmSize (Wm : ℕ) (f : Frm) : Prop

The three codes a frame carries fit in Wm bits.

Equations

• Complexity.Sav.FrmSize Wm f = (f.u.length ≤ Wm ∧ f.v.length ≤ Wm ∧ f.m.length ≤ Wm)

def Complexity.Sav.StkSize (Lmax Wm : ℕ) : List Frm → Prop

The stack descends exactly one level per frame — which is what bounds its depth — and every frame's codes fit.

Equations

• Complexity.Sav.StkSize Lmax Wm [] = True
• Complexity.Sav.StkSize Lmax Wm (f :: fs) = (fs.length + f.lvl.length = Lmax ∧ Complexity.Sav.FrmSize Wm f ∧ Complexity.Sav.StkSize Lmax Wm fs)

theorem Complexity.Sav.StkSize.length_le {Lmax Wm : ℕ} {stk : List Frm} : StkSize Lmax Wm stk → stk.length ≤ Lmax + 1

theorem Complexity.Sav.StkSize.mem_bound {Lmax Wm : ℕ} {stk : List Frm} : StkSize Lmax Wm stk → ∀ f ∈ stk, f.lvl.length ≤ Lmax ∧ FrmSize Wm f

theorem Complexity.Sav.step_stkSize (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) {Lmax Wm : ℕ} {s : Sst} (hzw : z.length ≤ Wm) (h : StkSize Lmax Wm s.stk) : StkSize Lmax Wm (step br ba z s).stk

theorem Complexity.Sav.iterate_stkSize (br : List Bool → List Bool → Bool) (ba : List Bool → Bool) (z : List Bool) {Lmax Wm : ℕ} (hzw : z.length ≤ Wm) (j : ℕ) (s : Sst) : StkSize Lmax Wm s.stk → StkSize Lmax Wm ((step br ba z)^[j] s).stk