Running the search to saturation

⚠️ Unreviewed by Bolton

The search is run for as many steps as there are configurations. Each step advances the counter by one, so after that many steps the counter has passed every record — there are at most as many records as configurations — and the search is complete.

Main definitions

• Complexity.polyRuler — a ruler of polynomial length
• Complexity.searchState — the unpacked search state after n steps

Main results

• Complexity.searchState_counter — the counter counts the steps
• Complexity.searchState_ok — the invariant holds throughout
• Complexity.searchState_complete — a long enough run finds every reachable configuration

Rulers of polynomial length

def Complexity.polyRuler (q : Polynomial ℕ) (x : List Bool) : List Bool

A ruler whose length is a polynomial in the input length.

Equations

• Complexity.polyRuler q x = List.replicate (Polynomial.eval x.length q) false

@[simp]

theorem Complexity.polyRuler_length (q : Polynomial ℕ) (x : List Bool) : (polyRuler q x).length = Polynomial.eval x.length q

theorem Complexity.polyRulerFn_mem_FP (q : Polynomial ℕ) {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => polyRuler q (a z)) ∈ FP

theorem Complexity.blockRuler_eq_polyRuler (q : Polynomial ℕ) (x : List Bool) : Cobham.blockRuler (Polynomial.eval x.length q) = polyRuler (2 * q + 2) x

The block ruler of a polynomial window.

The state after n steps

noncomputable def Complexity.searchState {k : ℕ} (tm : NTM k) (R V₀ : List Bool) (n : ℕ) : List Bool × List Bool

The unpacked search state after n steps.

Equations

• Complexity.searchState tm R V₀ n = (Complexity.searchStepPair tm (Complexity.codeBlocks k) R)^[n] ([], V₀)

theorem Complexity.searchState_counter {k : ℕ} (tm : NTM k) (R V₀ : List Bool) (n : ℕ) : (searchState tm R V₀ n).1.length = n

The counter counts the steps.

theorem Complexity.searchState_ok {k : ℕ} (tm : NTM k) {L : Language} {S : ℕ → ℕ} (hdec : tm.DecidesInSpace L S) (x : List Bool) (W : ℕ) (hq : Fintype.card tm.Q ≤ Cobham.blockWidth W) (hW : x.length + S x.length + 1 ≤ W) (n : ℕ) : SearchOk tm x W (searchState tm (Cobham.blockRuler W) (Cobham.cfgCode W (tm.initCfg x)) n).1 (searchState tm (Cobham.blockRuler W) (Cobham.cfgCode W (tm.initCfg x)) n).2

The invariant holds throughout the run.

theorem Complexity.searchState_complete {k : ℕ} (tm : NTM k) {L : Language} {S : ℕ → ℕ} (hdec : tm.DecidesInSpace L S) (x : List Bool) (W : ℕ) (hq : Fintype.card tm.Q ≤ Cobham.blockWidth W) (hW : x.length + S x.length + 1 ≤ W) (n : ℕ) (hn : Fintype.card (Code tm.Q k x.length (S x.length)) ≤ n) {c : Cfg k tm.Q} (hc : tm.ReachesCfg (tm.initCfg x) c) : memFlag (wideRuler (codeBlocks k) (Cobham.blockRuler W)) (Cobham.cfgCode W c) (searchState tm (Cobham.blockRuler W) (Cobham.cfgCode W (tm.initCfg x)) n).2 = [true]

A long enough run finds every reachable configuration.

What the accept scan on the finished search decides

theorem Complexity.acceptScan_sound {k : ℕ} (tm : NTM k) {L : Language} {S : ℕ → ℕ} (hdec : tm.DecidesInSpace L S) (x : List Bool) (W : ℕ) (hq : Fintype.card tm.Q ≤ Cobham.blockWidth W) (hW : x.length + S x.length + 1 ≤ W) (hW1 : 1 ≤ W) (n : ℕ) (ruler : List Bool) (hruler : W ≤ ruler.length) (h : acceptScan k (Cobham.stateCode tm.qhalt) (Cobham.blockRuler W) ruler (searchState tm (Cobham.blockRuler W) (Cobham.cfgCode W (tm.initCfg x)) n).2 = [true]) : ∃ (c : Cfg k tm.Q), tm.ReachesCfg (tm.initCfg x) c ∧ tm.halted c ∧ c.output.cells 1 = Γ.one

The scan fires only on a genuinely accepting configuration.

theorem Complexity.acceptScan_complete {k : ℕ} (tm : NTM k) {L : Language} {S : ℕ → ℕ} (hdec : tm.DecidesInSpace L S) (x : List Bool) (W : ℕ) (hq : Fintype.card tm.Q ≤ Cobham.blockWidth W) (hW : x.length + S x.length + 1 ≤ W) (hW1 : 1 ≤ W) (n : ℕ) (hn : Fintype.card (Code tm.Q k x.length (S x.length)) ≤ n) (ruler : List Bool) (hruler : W ≤ ruler.length) {c : Cfg k tm.Q} (hc : tm.ReachesCfg (tm.initCfg x) c) (hhalt : tm.halted c) (hout : c.output.cells 1 = Γ.one) : acceptScan k (Cobham.stateCode tm.qhalt) (Cobham.blockRuler W) ruler (searchState tm (Cobham.blockRuler W) (Cobham.cfgCode W (tm.initCfg x)) n).2 = [true]

The scan fires whenever an accepting configuration is reachable.

The search as one polynomial-time function

noncomputable def Complexity.initRecord {k : ℕ} (tm : NTM k) (R x : List Bool) : List Bool

The initial record, built straight from the input.

Equations

• Complexity.initRecord tm R x = Complexity.Cobham.initFn (tm.branchTM false) R x

theorem Complexity.initRecord_eq {k : ℕ} (tm : NTM k) (W : ℕ) (x : List Bool) (hx : x.length ≤ W) : initRecord tm (Cobham.blockRuler W) x = Cobham.cfgCode W (tm.initCfg x)

theorem Complexity.initRecordFn_mem_FP {k : ℕ} (tm : NTM k) {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => initRecord tm (a z) (b z)) ∈ FP

noncomputable def Complexity.searchRun {k : ℕ} (tm : NTM k) (R V₀ ruler : List Bool) : List Bool

The packed search, one step per bit of the ruler.

Equations

• Complexity.searchRun tm R V₀ ruler = (Complexity.searchStep tm (Complexity.codeBlocks k))^[ruler.length] (Complexity.searchPack R [] V₀)

theorem Complexity.searchRun_eq {k : ℕ} (tm : NTM k) (R V₀ ruler : List Bool) : searchRun tm R V₀ ruler = searchPack R (searchState tm R V₀ ruler.length).1 (searchState tm R V₀ ruler.length).2

noncomputable def Complexity.searchVisited {k : ℕ} (tm : NTM k) (R V₀ ruler : List Bool) : List Bool

The visited string a search leaves behind.

Equations

• Complexity.searchVisited tm R V₀ ruler = Complexity.pairSnd (Complexity.pairSnd (Complexity.searchRun tm R V₀ ruler))

theorem Complexity.searchVisited_eq {k : ℕ} (tm : NTM k) (R V₀ ruler : List Bool) : searchVisited tm R V₀ ruler = (searchState tm R V₀ ruler.length).2

theorem Complexity.searchVisitedFn_mem_FP {k : ℕ} (tm : NTM k) {Rf V₀f rulerf widthf : List Bool → List Bool} (hR : Rf ∈ FP) (hV₀ : V₀f ∈ FP) (hruler : rulerf ∈ FP) (hwidth : widthf ∈ FP) (hbound : ∀ (x : List Bool), ∀ n ≤ (rulerf x).length, ((searchStep tm (codeBlocks k))^[n] (searchPack (Rf x) [] (V₀f x))).length ≤ (widthf x).length) : (fun (x : List Bool) => searchVisited tm (Rf x) (V₀f x) (rulerf x)) ∈ FP

The search is polynomial-time, given a polynomial bound on its state.

The verdict

noncomputable def Complexity.nlVerdict {k : ℕ} (tm : NTM k) (qp np : Polynomial ℕ) (x : List Bool) : List Bool

The whole decision: search the configuration graph, then scan the visited string for an accepting record.

Equations

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

theorem Complexity.nlVerdict_flag {k : ℕ} (tm : NTM k) (qp np : Polynomial ℕ) (x : List Bool) : nlVerdict tm qp np x = [true] ∨ nlVerdict tm qp np x = [false]

The verdict is a flag.

theorem Complexity.nlVerdict_eq_true_iff {k : ℕ} (tm : NTM k) {L : Language} {S : ℕ → ℕ} (hdec : tm.DecidesInSpace L S) (qp np : Polynomial ℕ) (hqp : ∀ (n : ℕ), n + S n + 1 ≤ Polynomial.eval n qp) (hcardq : ∀ (n : ℕ), Fintype.card tm.Q ≤ Cobham.blockWidth (Polynomial.eval n qp)) (hnp : ∀ (n : ℕ), Fintype.card (Code tm.Q k n (S n)) ≤ Polynomial.eval n np) (x : List Bool) : nlVerdict tm qp np x = [true] ↔ x ∈ L

The verdict decides the language.

theorem Complexity.nlVerdictFn_mem_FP {k : ℕ} (tm : NTM k) {L : Language} {S : ℕ → ℕ} (hdec : tm.DecidesInSpace L S) (qp np wp : Polynomial ℕ) (hqp : ∀ (n : ℕ), n + S n + 1 ≤ Polynomial.eval n qp) (hcardq : ∀ (n : ℕ), Fintype.card tm.Q ≤ Cobham.blockWidth (Polynomial.eval n qp)) (hnp : ∀ (n : ℕ), Fintype.card (Code tm.Q k n (S n)) ≤ Polynomial.eval n np) (hwp : ∀ (n : ℕ), 2 * (2 * Polynomial.eval n qp + 2) + 2 * Polynomial.eval n np + Polynomial.eval n np * recordWidth k (Polynomial.eval n qp) + 4 ≤ Polynomial.eval n wp) : (fun (x : List Bool) => nlVerdict tm qp np x) ∈ FP

The verdict is polynomial-time.

The containment

theorem Complexity.NL_subset_P_internal : NL ⊆ P

NL ⊆ P. A log-space nondeterministic machine's configuration graph has polynomially many nodes, and the worklist search above walks all of it in polynomial time.