Reachability as a bounded fixpoint

⚠️ Unreviewed by Bolton

Breadth-first search closes a set of configurations under the successor relation. reachSet is that closure after a fixed number of rounds, and the theorem below says a polynomial number of rounds already suffices: the rounds strictly grow until they stabilize, and they cannot grow past the number of configurations available.

This is the specification a polynomial-time search has to implement — the counting it needs comes from Complexitylib.Classes.Containments.Internal.LogSpaceBound.

reachSet itself is defined in Complexitylib.Classes.Containments.Defs.

Main results

• NTM.reachSet_mono, NTM.reachSet_stabilizes — the rounds grow and then stop
• NTM.reachSet_finite — each round is a finite set
• NTM.exists_stabilizing_round — they stop within the number of configuration codes
• NTM.reachesCfg_iff_mem_reachSet — enough rounds compute exactly reachability
• NTM.reachesCfg_iff_mem_reachSet — with enough rounds the fixpoint is exactly reachability

theorem Complexity.NTM.reachSet_succ {k : ℕ} (tm : NTM k) (c₀ : Cfg k tm.Q) (t : ℕ) : tm.reachSet c₀ (t + 1) = tm.reachSet c₀ t ∪ {c' : Cfg k tm.Q | ∃ c ∈ tm.reachSet c₀ t, tm.Succ c c'}

theorem Complexity.NTM.reachSet_subset_succ {k : ℕ} (tm : NTM k) (c₀ : Cfg k tm.Q) (t : ℕ) : tm.reachSet c₀ t ⊆ tm.reachSet c₀ (t + 1)

theorem Complexity.NTM.reachSet_mono {k : ℕ} (tm : NTM k) (c₀ : Cfg k tm.Q) {s t : ℕ} (h : s ≤ t) : tm.reachSet c₀ s ⊆ tm.reachSet c₀ t

theorem Complexity.NTM.reachesCfg_of_mem_reachSet {k : ℕ} (tm : NTM k) (c₀ : Cfg k tm.Q) (t : ℕ) {c : Cfg k tm.Q} : c ∈ tm.reachSet c₀ t → tm.ReachesCfg c₀ c

Every element of a round is reachable.

theorem Complexity.NTM.mem_reachSet_of_reachesCfg {k : ℕ} {tm : NTM k} {c₀ c : Cfg k tm.Q} (h : tm.ReachesCfg c₀ c) : ∃ (t : ℕ), c ∈ tm.reachSet c₀ t

Reachability in t steps lands in round t.

theorem Complexity.NTM.reachSet_stabilizes {k : ℕ} (tm : NTM k) (c₀ : Cfg k tm.Q) {s : ℕ} (h : tm.reachSet c₀ (s + 1) ⊆ tm.reachSet c₀ s) (m : ℕ) : tm.reachSet c₀ (s + m) = tm.reachSet c₀ s

Once a round adds nothing, no later round does either.

theorem Complexity.NTM.reachSet_finite {k : ℕ} (tm : NTM k) (c₀ : Cfg k tm.Q) (t : ℕ) : (tm.reachSet c₀ t).Finite

Each round is a finite set: it starts as a singleton and each round adds at most two successors per member.

The rounds stabilize within the configuration count

theorem Complexity.NTM.exists_stabilizing_round {k : ℕ} {α : Type} [Fintype α] (tm : NTM k) (c₀ : Cfg k tm.Q) (g : Cfg k tm.Q → α) (hinj : ∀ {c c' : Cfg k tm.Q}, tm.ReachesCfg c₀ c → tm.ReachesCfg c₀ c' → g c = g c' → c = c') : ∃ s ≤ Fintype.card α, tm.reachSet c₀ (s + 1) ⊆ tm.reachSet c₀ s

The rounds stabilize by the number of codes. As long as the rounds keep growing they consume a fresh code each time, and there are only Fintype.card α of those.

theorem Complexity.NTM.reachesCfg_iff_mem_reachSet' {k : ℕ} {α : Type} [Fintype α] (tm : NTM k) (c₀ : Cfg k tm.Q) (g : Cfg k tm.Q → α) (hinj : ∀ {c c' : Cfg k tm.Q}, tm.ReachesCfg c₀ c → tm.ReachesCfg c₀ c' → g c = g c' → c = c') (c : Cfg k tm.Q) : tm.ReachesCfg c₀ c ↔ c ∈ tm.reachSet c₀ (Fintype.card α)

With enough rounds the fixpoint is exactly reachability. The number of rounds needed is the number of codes, so a polynomial code count makes this a polynomial-round search.

theorem Complexity.NTM.reachesCfg_iff_mem_reachSet {k : ℕ} {α : Type} [Fintype α] (tm : NTM k) (c₀ : Cfg k tm.Q) (g : Cfg k tm.Q → α) (hinj : ∀ {c c' : Cfg k tm.Q}, tm.ReachesCfg c₀ c → tm.ReachesCfg c₀ c' → g c = g c' → c = c') {N : ℕ} (hN : Fintype.card α ≤ N) (c : Cfg k tm.Q) : tm.ReachesCfg c₀ c ↔ c ∈ tm.reachSet c₀ N

Running extra rounds is harmless. An implementation computes a round count it can evaluate rather than the exact number of codes; any count that reaches the bound is correct.