What Savitch's recursion computes

⚠️ Unreviewed by Bolton

Complexity.Sav.rchB and Complexity.Sav.accB are the values the abstract machine returns, defined purely on bitstrings: a level-n reachability question is answered by trying every string of the enumeration's width as a midpoint. This file identifies them with reachability in the configuration graph, for as long as the strings involved are codes of configurations reachable from the start.

The two directions are both easy once the statement is right. Soundness follows because a midpoint that passes the first half is itself the code of a reachable configuration, so the induction hypothesis applies to it; completeness follows because the enumeration is every string of the code width, and a code has exactly that width.

Main results

• Complexity.baseReachB_cfgCode, Complexity.baseAccB_cfgCode — the base tests
• Complexity.rchB_cfgCode, Complexity.accB_cfgCode — the recursion

The bottom of the enumeration

@[simp]

theorem Complexity.binValLE_savZero (k : ℕ) (R : List Bool) : binValLE (savZero k R) = 0

The base tests as propositions

theorem Complexity.baseReachB_eq_true_iff {k : ℕ} (tm : NTM k) (R u v : List Bool) : baseReachB tm R u v = true ↔ u = v ∨ nstepFn tm false R u = v ∨ nstepFn tm true R u = v

theorem Complexity.baseAccB_eq_true_iff {k : ℕ} (tm : NTM k) (R rl u : List Bool) : baseAccB tm R rl u = true ↔ acceptFlag (Cobham.stateCode tm.qhalt) R rl u = [true] ∨ acceptFlag (Cobham.stateCode tm.qhalt) R rl (nstepFn tm false R u) = [true] ∨ acceptFlag (Cobham.stateCode tm.qhalt) R rl (nstepFn tm true R u) = [true]

One step of the graph

theorem Complexity.NTM.eq_of_reachesCfgIn_of_halted {k : ℕ} {tm : NTM k} {s : ℕ} {c c' : Cfg k tm.Q} (h : tm.ReachesCfgIn s c c') (hh : c.state = tm.qhalt) : c' = c

theorem Complexity.NTM.eq_of_reachesCfgLe_of_halted {k : ℕ} {tm : NTM k} {t : ℕ} {c c' : Cfg k tm.Q} (h : tm.ReachesCfgLe t c c') (hh : c.state = tm.qhalt) : c' = c

theorem Complexity.NTM.reachesCfg_of_reachesCfgIn {k : ℕ} {tm : NTM k} {s : ℕ} {c c' : Cfg k tm.Q} (h : tm.ReachesCfgIn s c c') : tm.ReachesCfg c c'

theorem Complexity.NTM.reachesCfg_of_reachesCfgLe {k : ℕ} {tm : NTM k} {t : ℕ} {c c' : Cfg k tm.Q} (h : tm.ReachesCfgLe t c c') : tm.ReachesCfg c c'

theorem Complexity.NTM.reachesCfgLe_one_iff {k : ℕ} (tm : NTM k) (c c' : Cfg k tm.Q) : tm.ReachesCfgLe 1 c c' ↔ c' = c ∨ c.state ≠ tm.qhalt ∧ ∃ (b : Bool), c' = tm.stepCfg b c

The recursion against the graph

theorem Complexity.baseReachB_cfgCode {k : ℕ} (tm : NTM k) {L : Language} {S : ℕ → ℕ} (hdec : tm.DecidesInSpace L S) (x : List Bool) (W : ℕ) (hq : Fintype.card tm.Q ≤ Cobham.blockWidth W) (hW : x.length + S x.length + 1 ≤ W) {c : Cfg k tm.Q} (hc : tm.ReachesCfg (tm.initCfg x) c) (v : List Bool) : baseReachB tm (Cobham.blockRuler W) (Cobham.cfgCode W c) v = true ↔ ∃ (c' : Cfg k tm.Q), tm.ReachesCfgLe 1 c c' ∧ v = Cobham.cfgCode W c'

theorem Complexity.baseAccB_cfgCode {k : ℕ} (tm : NTM k) {L : Language} {S : ℕ → ℕ} (hdec : tm.DecidesInSpace L S) (x : List Bool) (W : ℕ) (hq : Fintype.card tm.Q ≤ Cobham.blockWidth W) (hW : x.length + S x.length + 1 ≤ W) {c : Cfg k tm.Q} (hc : tm.ReachesCfg (tm.initCfg x) c) : baseAccB tm (Cobham.blockRuler W) (savRuler k (Cobham.blockRuler W)) (Cobham.cfgCode W c) = true ↔ ∃ (c' : Cfg k tm.Q), tm.ReachesCfgLe 1 c c' ∧ c'.state = tm.qhalt ∧ c'.output.cells 1 = Γ.one

theorem Complexity.rchB_cfgCode {k : ℕ} (tm : NTM k) {L : Language} {S : ℕ → ℕ} (hdec : tm.DecidesInSpace L S) (x : List Bool) (W : ℕ) (hq : Fintype.card tm.Q ≤ Cobham.blockWidth W) (hW : x.length + S x.length + 1 ≤ W) (n : ℕ) (c : Cfg k tm.Q) : tm.ReachesCfg (tm.initCfg x) c → ∀ (v : List Bool), Sav.rchB (baseReachB tm (Cobham.blockRuler W)) (savZero k (Cobham.blockRuler W)) n (Cobham.cfgCode W c) v = true ↔ ∃ (c' : Cfg k tm.Q), tm.ReachesCfgLe (2 ^ n) c c' ∧ v = Cobham.cfgCode W c'

The recursion decides bounded reachability.

theorem Complexity.accB_cfgCode {k : ℕ} (tm : NTM k) {L : Language} {S : ℕ → ℕ} (hdec : tm.DecidesInSpace L S) (x : List Bool) (W : ℕ) (hq : Fintype.card tm.Q ≤ Cobham.blockWidth W) (hW : x.length + S x.length + 1 ≤ W) (n : ℕ) (c : Cfg k tm.Q) : tm.ReachesCfg (tm.initCfg x) c → (Sav.accB (baseReachB tm (Cobham.blockRuler W)) (fun (u : List Bool) => baseAccB tm (Cobham.blockRuler W) (savRuler k (Cobham.blockRuler W)) u) (savZero k (Cobham.blockRuler W)) n (Cobham.cfgCode W c) = true ↔ ∃ (c' : Cfg k tm.Q), tm.ReachesCfgLe (2 ^ n) c c' ∧ c'.state = tm.qhalt ∧ c'.output.cells 1 = Γ.one)

The recursion decides bounded acceptance.