The configuration graph and its bounded reachability rounds

The space-bounded containments — NL ⊆ P, NL ⊆ coNL, Savitch's theorem — all read a computation as a walk in the configuration graph: the nondeterministic step relation on configurations. This file holds the three definitions those arguments share, so that theorem statements about them can be read without opening any proof internals.

Main definitions

• NTM.Succ — one nondeterministic step, as a relation on configurations
• NTM.ReachesCfg — its reflexive-transitive closure
• NTM.reachSet — the configurations reached within a fixed number of rounds of successor-closure, i.e. the state of a breadth-first search after that many rounds
• NTM.ReachesCfgIn, NTM.ReachesCfgLe — reachability in exactly, and in at most, a given number of steps; the step count is what Savitch's recursion halves
• logWindow — a concrete O(log n) search window
• TM.spaceTimeBound — the configuration count of a space-bounded deterministic machine, which bounds its running time (PSPACE ⊆ EXP)

def Complexity.logWindow (C D n : ℕ) : ℕ

The search window of a log-space machine. A machine's own space function is an arbitrary O(log n) function, which a program cannot evaluate; this concrete bound can be computed from the input length alone, and enlarging the window is harmless.

Equations

• Complexity.logWindow C D n = C * Nat.log 2 n + D

def Complexity.NTM.Succ {k : ℕ} (tm : NTM k) (c c' : Cfg k tm.Q) : Prop

One step of the configuration graph: a non-halted configuration has the two successors its transition functions produce.

Equations

• tm.Succ c c' = (c.state ≠ tm.qhalt ∧ ∃ (b : Bool), c' = tm.stepCfg b c)

def Complexity.NTM.ReachesCfg {k : ℕ} (tm : NTM k) : Cfg k tm.Q → Cfg k tm.Q → Prop

Reachability in the configuration graph.

Equations

• tm.ReachesCfg = Relation.ReflTransGen tm.Succ

inductive Complexity.NTM.ReachesCfgIn {k : ℕ} (tm : NTM k) : ℕ → Cfg k tm.Q → Cfg k tm.Q → Prop

Reachability in exactly t steps of the configuration graph.

• refl {k : ℕ} {tm : NTM k} (c : Cfg k tm.Q) : tm.ReachesCfgIn 0 c c

  No steps: a configuration reaches itself.

• head {k : ℕ} {tm : NTM k} {c c' c'' : Cfg k tm.Q} {t : ℕ} (hstep : tm.Succ c c') (hrest : tm.ReachesCfgIn t c' c'') : tm.ReachesCfgIn (t + 1) c c''

  One step followed by a shorter walk.

def Complexity.NTM.ReachesCfgLe {k : ℕ} (tm : NTM k) (t : ℕ) (c c' : Cfg k tm.Q) : Prop

Reachability in at most t steps. Halted configurations have no successors, so a walk cannot be padded and the bounded notion is genuinely weaker than the exact one.

Equations

• tm.ReachesCfgLe t c c' = ∃ s ≤ t, tm.ReachesCfgIn s c c'

def Complexity.NTM.reachSet {k : ℕ} (tm : NTM k) (c₀ : Cfg k tm.Q) : ℕ → Set (Cfg k tm.Q)

The configurations reachable from c₀ within t rounds of successor-closure.

Equations

• tm.reachSet c₀ 0 = {c₀}
• tm.reachSet c₀ t.succ = tm.reachSet c₀ t ∪ {c' : Complexity.Cfg k tm.Q | ∃ c ∈ tm.reachSet c₀ t, tm.Succ c c'}

def Complexity.TM.spaceTimeBound {k : ℕ} (tm : TM k) (f : ℕ → ℕ) (n : ℕ) : ℕ

The exponential configuration bound of a space-f machine: the number of states, times the n + f n + 2 input-head positions, times, for each of the k work tapes and the output tape, a head position within the window and window contents over the four-letter alphabet. A decider that stays within space f halts within this many steps (TM.decidesInTime_of_decidesInSpace).

Equations

• tm.spaceTimeBound f n = Fintype.card tm.Q * ((n + f n + 2) * (((f n + 1) * 4 ^ (f n + 1)) ^ k * ((f n + 2) * 4 ^ (f n + 2))))