The encoded step simulates the abstract one

⚠️ Unreviewed by Bolton

Complexity.savStep is Savitch's recursion written on a bitstring, so that it lands in FP; Complexity.Sav.step is the same recursion on an inductive state, where it can be reasoned about. This file writes the encoding down and proves the square commutes.

Main definitions

• Complexity.encFrm, Complexity.encSst — the encoding of a frame and a state
• Complexity.savSem — the abstract step the encoded one simulates

Main results

• Complexity.savStep_encSst — one encoded step is one abstract step
• Complexity.savStep_iterate_encSst — hence so is any number of them

Flags as booleans

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

The base reachability test, as a boolean.

Equations

• Complexity.baseReachB tm R u v = (Complexity.baseReach tm R u v).headD false

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

The base acceptance test, as a boolean.

Equations

• Complexity.baseAccB tm R rl u = (Complexity.baseAcc tm R rl u).headD false

theorem Complexity.baseReach_eq {k : ℕ} (tm : NTM k) (R u v : List Bool) : baseReach tm R u v = [baseReachB tm R u v]

theorem Complexity.baseAcc_eq {k : ℕ} (tm : NTM k) (R rl u : List Bool) : baseAcc tm R rl u = [baseAccB tm R rl u]

The encoding

def Complexity.encOpt : Option Bool → List Bool

A returned value on the tape.

Equations

• Complexity.encOpt none = []
• Complexity.encOpt (some b) = [b]

@[simp]

theorem Complexity.encOpt_none : encOpt none = []

@[simp]

theorem Complexity.encOpt_some (b : Bool) : encOpt (some b) = [b]

def Complexity.encFrm (f : Sav.Frm) : List Bool

A frame on the tape.

Equations

• Complexity.encFrm f = Complexity.mkFrame [f.kind] [f.ph] f.lvl f.u f.v f.m

def Complexity.encSst (R : List Bool) (s : Sav.Sst) : List Bool

A state on the tape.

Equations

• Complexity.encSst R s = Complexity.mkSt [s.done] [s.ans] R (Complexity.encOpt s.ret) (Complexity.encStack (List.map Complexity.encFrm s.stk))

noncomputable def Complexity.savSem {k : ℕ} (tm : NTM k) (R : List Bool) : Sav.Sst → Sav.Sst

The abstract step the encoded one runs.

Equations

• Complexity.savSem tm R = Complexity.Sav.step (Complexity.baseReachB tm R) (fun (u : List Bool) => Complexity.baseAccB tm R (Complexity.savRuler k R) u) (Complexity.savZero k R)

The square commutes

@[simp]

theorem Complexity.stDone_encSst (R : List Bool) (s : Sav.Sst) : stDone (encSst R s) = [s.done]

@[simp]

theorem Complexity.stAns_encSst (R : List Bool) (s : Sav.Sst) : stAns (encSst R s) = [s.ans]

@[simp]

theorem Complexity.stR_encSst (R : List Bool) (s : Sav.Sst) : stR (encSst R s) = R

@[simp]

theorem Complexity.stRet_encSst (R : List Bool) (s : Sav.Sst) : stRet (encSst R s) = encOpt s.ret

@[simp]

theorem Complexity.stStk_encSst (R : List Bool) (s : Sav.Sst) : stStk (encSst R s) = encStack (List.map encFrm s.stk)

@[simp]

theorem Complexity.frKind_encFrm (f : Sav.Frm) : frKind (encFrm f) = [f.kind]

@[simp]

theorem Complexity.frPh_encFrm (f : Sav.Frm) : frPh (encFrm f) = [f.ph]

@[simp]

theorem Complexity.frLvl_encFrm (f : Sav.Frm) : frLvl (encFrm f) = f.lvl

@[simp]

theorem Complexity.frU_encFrm (f : Sav.Frm) : frU (encFrm f) = f.u

@[simp]

theorem Complexity.frV_encFrm (f : Sav.Frm) : frV (encFrm f) = f.v

@[simp]

theorem Complexity.frM_encFrm (f : Sav.Frm) : frM (encFrm f) = f.m

theorem Complexity.savStep_encSst {k : ℕ} (tm : NTM k) (R : List Bool) (s : Sav.Sst) (hne : s.stk = [] → s.ret ≠ none) : savStep tm (encSst R s) = encSst R (savSem tm R s)

One encoded step is one abstract step. The side condition rules out the one shape the encoding cannot express: an empty stack with nothing returning.

Iterating

theorem Complexity.encSst_ne_nil (R : List Bool) (s : Sav.Sst) : encSst R s ≠ []

theorem Complexity.savStep_iterate {k : ℕ} (tm : NTM k) (R : List Bool) (j : ℕ) (s : Sav.Sst) : Sav.StkOk s → (savStep tm)^[j] (encSst R s) = encSst R ((savSem tm R)^[j] s)

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

The root frame the recursion starts from.

Equations

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

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

The state Complexity.savInit builds, decoded.

Equations

• Complexity.savInitSst tm qp lp x = { done := false, ans := false, ret := none, stk := [Complexity.savRoot tm qp lp x] }

theorem Complexity.savInit_eq {k : ℕ} (tm : NTM k) (qp lp : Polynomial ℕ) (x : List Bool) : savInit tm qp lp x = encSst (savR qp x) (savInitSst tm qp lp x)

theorem Complexity.savSem_iterate_stkOk {k : ℕ} (tm : NTM k) (R : List Bool) (j : ℕ) (s : Sav.Sst) : Sav.StkOk s → Sav.StkOk ((savSem tm R)^[j] s)

theorem Complexity.savInitSst_stkOk {k : ℕ} (tm : NTM k) (qp lp : Polynomial ℕ) (x : List Bool) : Sav.StkOk (savInitSst tm qp lp x)

theorem Complexity.savG_iterate {k : ℕ} (tm : NTM k) (qp lp : Polynomial ℕ) (x : List Bool) (j : ℕ) : (savG tm qp lp)^[j + 1] (pair [] x) = pair (encSst (savR qp x) ((savSem tm (savR qp x))^[j] (savInitSst tm qp lp x))) x

The packed orbit is the abstract one.

theorem Complexity.headD_pair_encSst (R : List Bool) (s : Sav.Sst) (x : List Bool) : (pair (encSst R s) x).headD false = s.done

The head of a packed state is its done flag.

How long an encoded state is

theorem Complexity.encStack_length_le (fs : List (List Bool)) (B : ℕ) : (∀ f ∈ fs, f.length ≤ B) → (encStack fs).length ≤ fs.length * (2 * B + 2)

theorem Complexity.encFrm_length_le {Lmax Wm : ℕ} {f : Sav.Frm} (hl : f.lvl.length ≤ Lmax) (hs : Sav.FrmSize Wm f) : (encFrm f).length ≤ 2 * Lmax + 5 * Wm + 14

theorem Complexity.encSst_length_le {Lmax Wm : ℕ} (R : List Bool) (s : Sav.Sst) (h : Sav.StkSize Lmax Wm s.stk) : (encSst R s).length ≤ 2 * R.length + (Lmax + 1) * (2 * (2 * Lmax + 5 * Wm + 14) + 2) + 14

An encoded state is polynomially long.