The configuration graph of a nondeterministic machine

⚠️ Unreviewed by Bolton

Space-bounded computation is graph reachability: a nondeterministic machine accepts exactly when some accepting configuration is reachable from the initial one along the two-successor relation. This file sets up that translation, which NL ⊆ P, NL ⊆ coNL and Savitch's theorem all rest on — each then differs only in how it searches the graph.

The definitions themselves live in Complexitylib.Classes.Containments.Defs.

Main results

• NTM.reachesCfg_trace — every configuration a trace passes through is reachable
• NTM.exists_trace_of_reachesCfg — every reachable configuration is the end of some trace
• NTM.succ_iff — an edge of the graph is a step of one of the two NTM.branchTMs

theorem Complexity.NTM.succ_iff {k : ℕ} (tm : NTM k) (c c' : Cfg k tm.Q) : tm.Succ c c' ↔ ∃ (b : Bool), (tm.branchTM b).step c = some c'

The configuration graph is the union of the two deterministic steps. Its edges are the steps of NTM.branchTM, so the deterministic machinery for a single step applies to them.

theorem Complexity.NTM.reachesCfg_refl {k : ℕ} (tm : NTM k) (c : Cfg k tm.Q) : tm.ReachesCfg c c

theorem Complexity.NTM.reachesCfg_head {k : ℕ} {tm : NTM k} {c c' c'' : Cfg k tm.Q} (h : tm.Succ c c'') (h' : tm.ReachesCfg c'' c') : tm.ReachesCfg c c'

theorem Complexity.NTM.reachesCfg_trace {k : ℕ} (tm : NTM k) (T : ℕ) (choices : Fin T → Bool) (c : Cfg k tm.Q) : tm.ReachesCfg c (tm.trace T choices c)

A trace stays inside the configuration graph.

theorem Complexity.NTM.exists_trace_of_reachesCfg {k : ℕ} {tm : NTM k} {c c' : Cfg k tm.Q} (h : tm.ReachesCfg c c') : ∃ (t : ℕ) (choices : Fin t → Bool), tm.trace t choices c = c'

Every reachable configuration ends some trace.

The window invariant along the graph

theorem Complexity.Windowed.stepCfg {k : ℕ} {tm : NTM k} {x : List Bool} {S : ℕ} {c : Cfg k tm.Q} (b : Bool) (hw : Windowed x S c) (hspace : c.WithinDecisionSpace x.length S) : Windowed x S (tm.stepCfg b c)

A nondeterministic step of a machine whose heads stay inside the window preserves the window invariant.

theorem Complexity.windowed_of_reachesCfg {k : ℕ} {tm : NTM k} {x : List Bool} {S : ℕ} {c₀ c : Cfg k tm.Q} (hspace : ∀ (c' : Cfg k tm.Q), tm.ReachesCfg c₀ c' → c'.WithinDecisionSpace x.length S) (hw : Windowed x S c₀) (h : tm.ReachesCfg c₀ c) : Windowed x S c

Along the configuration graph, the window invariant is inherited as long as every configuration met respects the space bound.

Acceptance is reachability

theorem Complexity.mem_iff_exists_accepting_reachable {k : ℕ} {tm : NTM k} {L : Language} {f : ℕ → ℕ} (hdec : tm.DecidesInSpace L f) (x : List Bool) : x ∈ L ↔ ∃ (c : Cfg k tm.Q), tm.ReachesCfg (tm.initCfg x) c ∧ tm.halted c ∧ c.output.cells 1 = Γ.one

A space-bounded machine accepts exactly when an accepting configuration is reachable. This is the bridge every log-space graph argument starts from: membership in the language is a property of the configuration graph alone, with no reference to time or choice sequences.