Acceptance is a bounded search in the configuration graph

⚠️ Unreviewed by Bolton

Complexitylib.Classes.Containments.Internal.ConfigGraph turns acceptance into reachability, and Complexitylib.Classes.Containments.Internal.ReachSet turns reachability into a fixpoint whose round count is the number of configuration codes. This file joins the two for a space-bounded machine: the codes of Complexitylib.Classes.Containments.Internal.ConfigCount separate the reachable configurations, so the search terminates after Fintype.card (Code …) rounds — and for a log-space machine that count is polynomial.

The result is the specification NL ⊆ P has to implement: a language in NL is exactly a polynomially bounded breadth-first search in the configuration graph, with no residual reference to nondeterminism, traces, or time.

Main results

• NTM.DecidesInSpace.mono — deciding in space is monotone in the bound
• NTM.withinDecisionSpace_of_reachesCfg — the space bound holds along the whole graph
• NTM.cfgCode_inj_of_reachesCfg — codes separate the reachable configurations
• NTM.mem_iff_exists_mem_reachSet — membership is a search of enough rounds
• NL_bounded_reachability_internal — for NL the round count is polynomially bounded
• NL_subset_P_of_search_internal — the containment, modulo one machine

theorem Complexity.NTM.DecidesInSpace.mono {k : ℕ} {tm : NTM k} {L : Language} {S S' : ℕ → ℕ} (hle : ∀ (n : ℕ), S n ≤ S' n) (h : tm.DecidesInSpace L S) : tm.DecidesInSpace L S'

Deciding in space S is deciding in any larger space bound.

theorem Complexity.NTM.withinDecisionSpace_of_reachesCfg {k : ℕ} {tm : NTM k} {L : Language} {S : ℕ → ℕ} (hdec : tm.DecidesInSpace L S) (x : List Bool) {c : Cfg k tm.Q} (h : tm.ReachesCfg (tm.initCfg x) c) : c.WithinDecisionSpace x.length (S x.length)

The space bound holds at every configuration of the graph. DecidesInSpace states the bound along traces no longer than the halting time; past that time a trace is frozen, so the bound propagates to every reachable configuration.

theorem Complexity.NTM.windowed_of_reachesCfg_init {k : ℕ} {tm : NTM k} {L : Language} {S : ℕ → ℕ} (hdec : tm.DecidesInSpace L S) (x : List Bool) {c : Cfg k tm.Q} (h : tm.ReachesCfg (tm.initCfg x) c) : Windowed x (S x.length) c

The initial configuration and everything reachable from it stays inside the window.

theorem Complexity.NTM.cfgCode_inj_of_reachesCfg {k : ℕ} {tm : NTM k} {L : Language} {S : ℕ → ℕ} (hdec : tm.DecidesInSpace L S) (x : List Bool) {c c' : Cfg k tm.Q} (hc : tm.ReachesCfg (tm.initCfg x) c) (hc' : tm.ReachesCfg (tm.initCfg x) c') (heq : cfgCode x.length (S x.length) c = cfgCode x.length (S x.length) c') : c = c'

Codes separate the reachable configurations. This is what bounds the search: distinct reachable configurations have distinct codes, of which there are only finitely many.

theorem Complexity.NTM.mem_iff_exists_mem_reachSet {k : ℕ} {tm : NTM k} {L : Language} {S : ℕ → ℕ} (hdec : tm.DecidesInSpace L S) (x : List Bool) {N : ℕ} (hN : Fintype.card (Code tm.Q k x.length (S x.length)) ≤ N) : x ∈ L ↔ ∃ c ∈ tm.reachSet (tm.initCfg x) N, tm.halted c ∧ c.output.cells 1 = Γ.one

Membership is a bounded breadth-first search. An input is in the language exactly when an accepting configuration shows up within any number of rounds of successor-closure from the initial configuration that reaches the number of codes. Nothing here mentions traces, choices, or time.

theorem Complexity.NL_bounded_reachability_internal {L : Language} (hL : L ∈ NL) : ∃ (k : ℕ) (tm : NTM k) (A : ℕ) (B : ℕ), ∀ (x : List Bool), x ∈ L ↔ ∃ c ∈ tm.reachSet (tm.initCfg x) (A * (x.length + 1) ^ B), tm.halted c ∧ c.output.cells 1 = Γ.one

A language in NL is a polynomially bounded reachability search. This is the specification a polynomial-time decision procedure has to implement: run the successor-closure for A · (|x| + 1) ^ B rounds and look for an accepting configuration.

theorem Complexity.NL_subset_P_of_search_internal (h : ∀ (k : ℕ) (tm : NTM k) (S : ℕ → ℕ) (L₀ : Language) (A B : ℕ), tm.DecidesInSpace L₀ S → (BigO S fun (n : ℕ) => Nat.log 2 n) → ∃ (k' : ℕ) (M : TM k') (q : Polynomial ℕ), M.DecidesInTime {x : List Bool | ∃ c ∈ tm.reachSet (tm.initCfg x) (A * (x.length + 1) ^ B), tm.halted c ∧ c.output.cells 1 = Γ.one} fun (n : ℕ) => Polynomial.eval n q) : NL ⊆ P

NL ⊆ P, reduced to the existence of one machine. The hypothesis carries the log-space witness for tm: without it the search language is not decidable at all, let alone in polynomial time, since the configuration graph would be unbounded.