The tape of Savitch's stack machine

⚠️ Unreviewed by Bolton

Savitch's procedure is a recursion of polynomial depth, so it is a stack machine whose stack is polynomially bounded. This file fixes how that stack is written on a single bitstring, and gives every field's reader and writer inside the polynomial-time algebra.

A frame carries the subproblem a level of the recursion is working on:

• kind — [false] for is v reachable from u, [true] for is some accepting configuration reachable from u;
• ph — [false] while the first half of the interval is being tried, [true] while the second is;
• lvl — the level, in unary: 2 ^ |lvl| steps are allowed;
• u, v — the two endpoints (v is unused by an acceptance frame);
• m — the midpoint being tried, which doubles as the enumeration's counter.

A stack is a right-nested chain of pairs, empty stack being the empty string; pair is never empty, so the two are told apart by a single flag.

The state carries the done flag (which is the bit Complexity.SpaceIter watches), the answer, the block ruler the codes are written against, the value a finished subcall is returning ([] while descending), and the stack.

Main definitions

• Complexity.mkFrame and Complexity.frKind, … — a frame and its fields
• Complexity.encStack, Complexity.stkTop, Complexity.stkRest — the stack
• Complexity.mkSt and Complexity.stDone, … — the state and its fields

Main results

• the _mk simp lemmas — every reader inverts the constructor
• Complexity.mkFrameFn_mem_FP, Complexity.mkStFn_mem_FP, and the readers' — all of it is in FP

Frames

def Complexity.mkFrame (kind ph lvl u v m : List Bool) : List Bool

A frame of Savitch's recursion.

Equations

• Complexity.mkFrame kind ph lvl u v m = Complexity.pair kind (Complexity.pair ph (Complexity.pair lvl (Complexity.pair u (Complexity.pair v m))))

def Complexity.frKind (f : List Bool) : List Bool

Which subproblem the frame is working on.

Equations

• Complexity.frKind f = Complexity.pairFst f

def Complexity.frPh (f : List Bool) : List Bool

Which half of the interval the frame is trying.

Equations

• Complexity.frPh f = Complexity.pairFst (Complexity.pairSnd f)

def Complexity.frLvl (f : List Bool) : List Bool

The frame's level, in unary.

Equations

• Complexity.frLvl f = Complexity.pairFst (Complexity.pairSnd (Complexity.pairSnd f))

def Complexity.frU (f : List Bool) : List Bool

The frame's source endpoint.

Equations

• Complexity.frU f = Complexity.pairFst (Complexity.pairSnd (Complexity.pairSnd (Complexity.pairSnd f)))

def Complexity.frV (f : List Bool) : List Bool

The frame's target endpoint.

Equations

• Complexity.frV f = Complexity.pairFst (Complexity.pairSnd (Complexity.pairSnd (Complexity.pairSnd (Complexity.pairSnd f))))

def Complexity.frM (f : List Bool) : List Bool

The midpoint the frame is trying.

Equations

• Complexity.frM f = Complexity.pairSnd (Complexity.pairSnd (Complexity.pairSnd (Complexity.pairSnd (Complexity.pairSnd f))))

@[simp]

theorem Complexity.frKind_mk (kind ph lvl u v m : List Bool) : frKind (mkFrame kind ph lvl u v m) = kind

@[simp]

theorem Complexity.frPh_mk (kind ph lvl u v m : List Bool) : frPh (mkFrame kind ph lvl u v m) = ph

@[simp]

theorem Complexity.frLvl_mk (kind ph lvl u v m : List Bool) : frLvl (mkFrame kind ph lvl u v m) = lvl

@[simp]

theorem Complexity.frU_mk (kind ph lvl u v m : List Bool) : frU (mkFrame kind ph lvl u v m) = u

@[simp]

theorem Complexity.frV_mk (kind ph lvl u v m : List Bool) : frV (mkFrame kind ph lvl u v m) = v

@[simp]

theorem Complexity.frM_mk (kind ph lvl u v m : List Bool) : frM (mkFrame kind ph lvl u v m) = m

@[simp]

theorem Complexity.mkFrame_length (kind ph lvl u v m : List Bool) : (mkFrame kind ph lvl u v m).length = 2 * kind.length + 2 * ph.length + 2 * lvl.length + 2 * u.length + 2 * v.length + m.length + 10

Stacks

def Complexity.encStack : List (List Bool) → List Bool

A stack of frames, top first.

Equations

• Complexity.encStack [] = []
• Complexity.encStack (f :: fs) = Complexity.pair f (Complexity.encStack fs)

@[simp]

theorem Complexity.encStack_nil : encStack [] = []

@[simp]

theorem Complexity.encStack_cons (f : List Bool) (fs : List (List Bool)) : encStack (f :: fs) = pair f (encStack fs)

def Complexity.stkTop (S : List Bool) : List Bool

The frame on top of the stack.

Equations

• Complexity.stkTop S = Complexity.pairFst S

def Complexity.stkRest (S : List Bool) : List Bool

The stack below the top frame.

Equations

• Complexity.stkRest S = Complexity.pairSnd S

@[simp]

theorem Complexity.stkTop_pair (f g : List Bool) : stkTop (pair f g) = f

@[simp]

theorem Complexity.stkRest_pair (f g : List Bool) : stkRest (pair f g) = g

theorem Complexity.stkTop_cons (f : List Bool) (fs : List (List Bool)) : stkTop (encStack (f :: fs)) = f

theorem Complexity.stkRest_cons (f : List Bool) (fs : List (List Bool)) : stkRest (encStack (f :: fs)) = encStack fs

theorem Complexity.encStack_eq_nil_iff (fs : List (List Bool)) : encStack fs = [] ↔ fs = []

A stack is empty exactly when its encoding is.

@[simp]

theorem Complexity.encStack_length (fs : List (List Bool)) : (encStack fs).length = List.foldr (fun (f : List Bool) (n : ℕ) => 2 * f.length + 2 + n) 0 fs

The state

def Complexity.mkSt (d a R ret stk : List Bool) : List Bool

The machine's state: the done flag, the answer, the block ruler, the value a finished subcall is returning, and the stack.

Equations

• Complexity.mkSt d a R ret stk = Complexity.pair d (Complexity.pair a (Complexity.pair R (Complexity.pair ret stk)))

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

The done flag — the bit the iteration watches.

Equations

• Complexity.stDone s = Complexity.pairFst s

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

The answer, once the recursion has produced one.

Equations

• Complexity.stAns s = Complexity.pairFst (Complexity.pairSnd s)

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

The block ruler the configuration codes are written against.

Equations

• Complexity.stR s = Complexity.pairFst (Complexity.pairSnd (Complexity.pairSnd s))

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

The value a finished subcall is returning; [] while descending.

Equations

• Complexity.stRet s = Complexity.pairFst (Complexity.pairSnd (Complexity.pairSnd (Complexity.pairSnd s)))

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

The stack.

Equations

• Complexity.stStk s = Complexity.pairSnd (Complexity.pairSnd (Complexity.pairSnd (Complexity.pairSnd s)))

@[simp]

theorem Complexity.stDone_mk (d a R ret stk : List Bool) : stDone (mkSt d a R ret stk) = d

@[simp]

theorem Complexity.stAns_mk (d a R ret stk : List Bool) : stAns (mkSt d a R ret stk) = a

@[simp]

theorem Complexity.stR_mk (d a R ret stk : List Bool) : stR (mkSt d a R ret stk) = R

@[simp]

theorem Complexity.stRet_mk (d a R ret stk : List Bool) : stRet (mkSt d a R ret stk) = ret

@[simp]

theorem Complexity.stStk_mk (d a R ret stk : List Bool) : stStk (mkSt d a R ret stk) = stk

@[simp]

theorem Complexity.mkSt_length (d a R ret stk : List Bool) : (mkSt d a R ret stk).length = 2 * d.length + 2 * a.length + 2 * R.length + 2 * ret.length + stk.length + 8

theorem Complexity.mkSt_headD (b : Bool) (a R ret stk : List Bool) : (mkSt [b] a R ret stk).headD false = b

The head bit of the state is the done flag.

theorem Complexity.mkSt_ne_nil (d a R ret stk : List Bool) : mkSt d a R ret stk ≠ []

A state is never empty.

The readers and the constructors are polynomial-time

theorem Complexity.fstBlockOf_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => pairFst (a z)) ∈ FP

theorem Complexity.sndBlockOf_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => pairSnd (a z)) ∈ FP

theorem Complexity.frKindFn_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => frKind (a z)) ∈ FP

theorem Complexity.frPhFn_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => frPh (a z)) ∈ FP

theorem Complexity.frLvlFn_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => frLvl (a z)) ∈ FP

theorem Complexity.frUFn_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => frU (a z)) ∈ FP

theorem Complexity.frVFn_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => frV (a z)) ∈ FP

theorem Complexity.frMFn_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => frM (a z)) ∈ FP

theorem Complexity.mkFrameFn_mem_FP {kf pf lf uf vf mf : List Bool → List Bool} (hk : kf ∈ FP) (hp : pf ∈ FP) (hl : lf ∈ FP) (hu : uf ∈ FP) (hv : vf ∈ FP) (hm : mf ∈ FP) : (fun (z : List Bool) => mkFrame (kf z) (pf z) (lf z) (uf z) (vf z) (mf z)) ∈ FP

theorem Complexity.stkTopFn_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => stkTop (a z)) ∈ FP

theorem Complexity.stkRestFn_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => stkRest (a z)) ∈ FP

theorem Complexity.stDoneFn_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => stDone (a z)) ∈ FP

theorem Complexity.stAnsFn_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => stAns (a z)) ∈ FP

theorem Complexity.stRFn_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => stR (a z)) ∈ FP

theorem Complexity.stRetFn_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => stRet (a z)) ∈ FP

theorem Complexity.stStkFn_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => stStk (a z)) ∈ FP

theorem Complexity.mkStFn_mem_FP {df af Rf rf sf : List Bool → List Bool} (hd : df ∈ FP) (ha : af ∈ FP) (hR : Rf ∈ FP) (hr : rf ∈ FP) (hs : sf ∈ FP) : (fun (z : List Bool) => mkSt (df z) (af z) (Rf z) (rf z) (sf z)) ∈ FP