What the worklist search finds

⚠️ Unreviewed by Bolton

The invariant of the search: the visited string is a list of distinct records, each the code of a configuration reachable from the initial one; the initial code is among them; and every record the counter has passed has both of its successors recorded.

Once the counter has passed every record — which it has after as many steps as there are configurations, since the records are distinct — the recorded codes are closed under the graph's steps, so every reachable configuration's code is there.

Main definitions

• Complexity.recordWidth — the width of one record
• Complexity.SearchOk — the invariant

Main results

• Complexity.memFlag_records — the scan decides membership in the record list
• Complexity.searchStepPair_ok — one step preserves the invariant
• Complexity.SearchOk.mem_of_reachesCfg — a saturated search has found everything

Records

def Complexity.recordWidth (k W : ℕ) : ℕ

The width of one record: a whole code.

Equations

• Complexity.recordWidth k W = Complexity.codeBlocks k * (Complexity.Cobham.blockRuler W).length

theorem Complexity.recordWidth_pos (k W : ℕ) : 0 < recordWidth k W

theorem Complexity.wideRuler_blockRuler_length (k W : ℕ) : (wideRuler (codeBlocks k) (Cobham.blockRuler W)).length = recordWidth k W

theorem Complexity.blockAt_records (k W : ℕ) (bs : List (List Bool)) (hbs : ∀ b ∈ bs, b.length = recordWidth k W) (i : ℕ) (hi : i < bs.length) : blockAt (wideRuler (codeBlocks k) (Cobham.blockRuler W)) bs.flatten i = bs[i]

The records of a concatenation are its blocks.

theorem Complexity.length_flatten_records (k W : ℕ) (bs : List (List Bool)) (hbs : ∀ b ∈ bs, b.length = recordWidth k W) : bs.flatten.length = bs.length * recordWidth k W

theorem Complexity.memFlag_records (k W : ℕ) (bs : List (List Bool)) (hbs : ∀ b ∈ bs, b.length = recordWidth k W) (u : List Bool) : memFlag (wideRuler (codeBlocks k) (Cobham.blockRuler W)) u bs.flatten = [true] ↔ u ∈ bs

The scan decides membership in the record list.

Appending a record

theorem Complexity.addBlock_nodup (k W : ℕ) (bs : List (List Bool)) (hbs : ∀ b ∈ bs, b.length = recordWidth k W) (b : List Bool) (hnd : bs.Nodup) (hm : memFlag (wideRuler (codeBlocks k) (Cobham.blockRuler W)) b bs.flatten = [false]) : (bs ++ [b]).Nodup

The appended record was not there before.

The invariant

noncomputable def Complexity.codesOf {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (W : ℕ) (cs : List (Cfg k Q)) : List (List Bool)

The records of a list of configurations.

Equations

• Complexity.codesOf W cs = List.map (Complexity.Cobham.cfgCode W) cs

theorem Complexity.codesOf_recordWidth {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (W : ℕ) (cs : List (Cfg k Q)) (b : List Bool) : b ∈ codesOf W cs → b.length = recordWidth k W

@[simp]

theorem Complexity.codesOf_length {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (W : ℕ) (cs : List (Cfg k Q)) : (codesOf W cs).length = cs.length

theorem Complexity.codesOf_getElem {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (W : ℕ) (cs : List (Cfg k Q)) (i : ℕ) (hi : i < cs.length) : (codesOf W cs)[i] = Cobham.cfgCode W cs[i]

@[simp]

theorem Complexity.codesOf_append {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (W : ℕ) (cs : List (Cfg k Q)) (c : Cfg k Q) : codesOf W (cs ++ [c]) = codesOf W cs ++ [Cobham.cfgCode W c]

def Complexity.SearchOk {k : ℕ} (tm : NTM k) (x : List Bool) (W : ℕ) (r V : List Bool) : Prop

The search state is sound: the visited string is the concatenation of the codes of finitely many reachable configurations, no two of them coded alike; the initial code is there; and every record the counter has passed has both successors recorded.

Equations

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

theorem Complexity.searchOk_init {k : ℕ} (tm : NTM k) (x : List Bool) (W : ℕ) : SearchOk tm x W [] (Cobham.cfgCode W (tm.initCfg x))

The initial state is sound.

One step preserves the invariant

theorem Complexity.exists_succ_code {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) {c : Cfg k tm.Q} (hc : tm.ReachesCfg (tm.initCfg x) c) (β : Bool) : ∃ (c' : Cfg k tm.Q), tm.ReachesCfg (tm.initCfg x) c' ∧ nstepFn tm β (Cobham.blockRuler W) (Cobham.cfgCode W c) = Cobham.cfgCode W c'

The two encoded successors of a reachable configuration are codes of reachable configurations.

theorem Complexity.searchOk_add {k : ℕ} (tm : NTM k) (x : List Bool) (W : ℕ) (cs : List (Cfg k tm.Q)) (hnd : (codesOf W cs).Nodup) (hreach : ∀ d ∈ cs, tm.ReachesCfg (tm.initCfg x) d) {c : Cfg k tm.Q} (hc : tm.ReachesCfg (tm.initCfg x) c) : ∃ (cs' : List (Cfg k tm.Q)), addBlock (wideRuler (codeBlocks k) (Cobham.blockRuler W)) (Cobham.cfgCode W c) (codesOf W cs).flatten = (codesOf W cs').flatten ∧ (codesOf W cs').Nodup ∧ (∀ d ∈ cs', tm.ReachesCfg (tm.initCfg x) d) ∧ (cs' = cs ∨ cs' = cs ++ [c]) ∧ Cobham.cfgCode W c ∈ codesOf W cs'

Adding one successor keeps every part of the invariant.

theorem Complexity.append_cases_prefix {α : Type} {cs cs' : List α} {c : α} (h : cs' = cs ∨ cs' = cs ++ [c]) : (∀ y ∈ cs, y ∈ cs') ∧ cs.length ≤ cs'.length ∧ ∀ (i : ℕ) (hi : i < cs.length) (hi' : i < cs'.length), cs'[i] = cs[i]

A list only grows at the end.

theorem Complexity.searchStepPair_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) (r V : List Bool) (h : SearchOk tm x W r V) : SearchOk tm x W (searchStepPair tm (codeBlocks k) (Cobham.blockRuler W) (r, V)).1 (searchStepPair tm (codeBlocks k) (Cobham.blockRuler W) (r, V)).2

One step of the search preserves the invariant.

A saturated search has found everything

theorem Complexity.searchOk_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) (r V : List Bool) (h : SearchOk tm x W r V) (hsat : V.length ≤ r.length * recordWidth k W) {c : Cfg k tm.Q} (hc : tm.ReachesCfg (tm.initCfg x) c) : memFlag (wideRuler (codeBlocks k) (Cobham.blockRuler W)) (Cobham.cfgCode W c) V = [true]

Once the counter has passed every record, the search is complete.

How long the visited string can get

theorem Complexity.searchOk_length_le {k : ℕ} (tm : NTM k) {L : Language} {S : ℕ → ℕ} (hdec : tm.DecidesInSpace L S) (x : List Bool) (W : ℕ) (r V : List Bool) (h : SearchOk tm x W r V) : V.length ≤ Fintype.card (Code tm.Q k x.length (S x.length)) * recordWidth k W

The visited string is bounded by the configuration count. The records are distinct and each is the code of a reachable configuration, and distinct configurations of the graph have distinct codes in the finite type of Complexitylib.Classes.Containments.Internal.ConfigCount.