The reachability search as a finite computation on codes

⚠️ Unreviewed by Bolton

Complexitylib.Classes.Containments.Internal.BoundedReach reduces membership to a bounded breadth-first search in the configuration graph, but the rounds there are Set (Cfg k tm.Q) — a specification, not a computation. This file replays the same search on the codes of Complexitylib.Classes.Containments.Internal.ConfigCount: a round is a Finset operation on a finite type, so the whole search is a finite, decidable iteration.

The bridge is a decoder. cfgCode forgets nothing about a configuration that respects the space window, so it has a left inverse there, and the successor of a code is simply the code of the successor of the configuration it denotes.

For a log-space machine the code type has polynomially many elements, so a round set is a polynomially sized object and the search runs for polynomially many rounds — this is the data structure a polynomial-time implementation manipulates.

Main definitions

• decodeCfg — rebuild a configuration from its code
• NTM.codeSucc, NTM.codeRound, NTM.reachCodes — the search, on Finsets of codes

Main results

• decodeCfg_cfgCode — decoding inverts coding inside the window
• NTM.mem_reachCodes_iff — the code search computes exactly the specified rounds
• NTM.mem_iff_exists_mem_reachCodes — membership as a finite search
• logWindow_bigO — the concrete window is still O(log n)
• NL_finite_search — for NL, a finite search whose window, round count, and accept test are all explicit arithmetic in the input length

def Complexity.decodeCfg {k : ℕ} {Q : Type} (x : List Bool) (S : ℕ) (a : Code Q k x.length S) : Cfg k Q

Rebuild a configuration from its code. The input tape is restored from the input itself — it is read-only — and each work and output cell beyond the window is restored to the blank that the window invariant guarantees is there.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.decodeCfg_cfgCode {k : ℕ} {Q : Type} {x : List Bool} {S : ℕ} {c : Cfg k Q} (hw : Windowed x S c) (hs : c.WithinDecisionSpace x.length S) : decodeCfg x S (cfgCode x.length S c) = c

Decoding inverts coding on the configurations the search meets. Inside the space window the clamps in cfgCode are inert and the cells it drops are the ones Windowed pins down, so nothing is lost.

def Complexity.NTM.codeSucc {k : ℕ} (tm : NTM k) (x : List Bool) (S : ℕ) (a : Code tm.Q k x.length S) : Finset (Code tm.Q k x.length S)

The codes of the successors of the configuration a code denotes.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.NTM.codeRound {k : ℕ} (tm : NTM k) (x : List Bool) (S : ℕ) (F : Finset (Code tm.Q k x.length S)) : Finset (Code tm.Q k x.length S)

One round of the search: keep what is known and add every successor code.

Equations

• tm.codeRound x S F = F ∪ F.biUnion (tm.codeSucc x S)

def Complexity.NTM.reachCodes {k : ℕ} (tm : NTM k) (x : List Bool) (S : ℕ) (a₀ : Code tm.Q k x.length S) : ℕ → Finset (Code tm.Q k x.length S)

The search: t rounds of successor-closure starting from a single code.

Equations

• tm.reachCodes x S a₀ 0 = {a₀}
• tm.reachCodes x S a₀ t.succ = tm.codeRound x S (tm.reachCodes x S a₀ t)

theorem Complexity.NTM.mem_reachCodes_iff {k : ℕ} {tm : NTM k} {x : List Bool} {S : ℕ} {c₀ : Cfg k tm.Q} (hs : ∀ (c : Cfg k tm.Q), tm.ReachesCfg c₀ c → c.WithinDecisionSpace x.length S) (hw : ∀ (c : Cfg k tm.Q), tm.ReachesCfg c₀ c → Windowed x S c) (t : ℕ) (a : Code tm.Q k x.length S) : a ∈ tm.reachCodes x S (cfgCode x.length S c₀) t ↔ ∃ c ∈ tm.reachSet c₀ t, cfgCode x.length S c = a

The code search computes exactly the specified rounds. Every code in round t is the code of a configuration in round t, and conversely.

theorem Complexity.NTM.mem_iff_exists_mem_reachCodes {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 ↔ ∃ a ∈ tm.reachCodes x (S x.length) (cfgCode x.length (S x.length) (tm.initCfg x)) N, (decodeCfg x (S x.length) a).state = tm.qhalt ∧ (decodeCfg x (S x.length) a).output.cells 1 = Γ.one

Membership is a finite search over codes. Every quantifier is over a finite type and every operation is a Finset operation, so this is an algorithm — what remains for NL ⊆ P is to bound its cost.

theorem Complexity.logWindow_bigO (C D : ℕ) : BigO (logWindow C D) fun (n : ℕ) => Nat.log 2 n

The concrete window is still a logarithmic bound, so the code count over it stays polynomial.

theorem Complexity.NL_finite_search {L : Language} (hL : L ∈ NL) : ∃ (k : ℕ) (tm : NTM k) (C : ℕ) (D : ℕ) (A : ℕ) (B : ℕ), ∀ (x : List Bool), x ∈ L ↔ ∃ a ∈ tm.reachCodes x (logWindow C D x.length) (cfgCode x.length (logWindow C D x.length) (tm.initCfg x)) (A * (x.length + 1) ^ B), (decodeCfg x (logWindow C D x.length) a).state = tm.qhalt ∧ (decodeCfg x (logWindow C D x.length) a).output.cells 1 = Γ.one

A language in NL is a finite search of polynomially many rounds. Every quantity in this statement is an explicit arithmetic function of the input length and finitely many machine constants: the window is logWindow C D |x|, the round count is A · (|x| + 1) ^ B, the rounds are Finsets of codes over that window, and the accept test is a decidable property of a single code. No trace, choice sequence, machine time bound, or asymptotic quantifier survives. This is the specification a polynomial-time implementation has to run; what remains for NL ⊆ P is to account for its cost.