The worklist search over encoded configurations

⚠️ Unreviewed by Bolton

The configuration graph of a space-bounded machine is searched by a worklist: a visited string holds the codes found so far, one fixed-width record each, and a counter says which record is expanded next. One step expands one record — it appends each of its two successors that is not already there — and advances the counter. Running the loop for as many steps as there are configurations expands everything, since the counter passes every record the search will ever hold.

The encoding is the one Cobham's theorem already uses: Cobham.cfgCode packs a configuration into 2(k+2)+1 fixed-width blocks and Cobham.stepFn is the encoded step of a deterministic machine, so NTM.branchTM supplies the two successors.

Main definitions

• Complexity.nstepFn — the encoded successor along one branch
• Complexity.addBlock — append a record unless it is already there
• Complexity.searchStepPair — one worklist step, on the unpacked state
• Complexity.searchStep — the same on the packed state

Main results

• Complexity.searchStep_pack — the packed step is the unpacked step
• Complexity.searchStep_mem_FP — one step is polynomial-time

Rulers for a whole code

def Complexity.wideRuler (m : ℕ) (R : List Bool) : List Bool

A code's width, as a ruler: m copies of the block ruler.

Equations

• Complexity.wideRuler m R = (List.replicate m R).flatten

@[simp]

theorem Complexity.wideRuler_length (m : ℕ) (R : List Bool) : (wideRuler m R).length = m * R.length

theorem Complexity.wideRulerFn_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) (m : ℕ) : (fun (z : List Bool) => wideRuler m (a z)) ∈ FP

Every constant number of copies of a polynomial-time value is polynomial-time.

def Complexity.fitCode (m : ℕ) (R b : List Bool) : List Bool

Normalise a would-be code to exactly the code width.

Equations

• Complexity.fitCode m R b = Complexity.padTo (Complexity.wideRuler m R) b

@[simp]

theorem Complexity.fitCode_length (m : ℕ) (R b : List Bool) : (fitCode m R b).length = m * R.length

theorem Complexity.fitCode_of_length (m : ℕ) (R b : List Bool) (h : b.length = m * R.length) : fitCode m R b = b

A value already of the code width is unchanged.

theorem Complexity.fitCodeFn_mem_FP {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) (m : ℕ) : (fun (z : List Bool) => fitCode m (a z) (b z)) ∈ FP

The encoded successors

noncomputable def Complexity.nstepFn {k : ℕ} (tm : NTM k) (b : Bool) (R z : List Bool) : List Bool

The encoded successor of a configuration along branch b.

Equations

• Complexity.nstepFn tm b R z = Complexity.Cobham.stepFn (tm.branchTM b) R z

theorem Complexity.nstepFnFn_mem_FP {k : ℕ} (tm : NTM k) (b : Bool) {a c : List Bool → List Bool} (ha : a ∈ FP) (hc : c ∈ FP) : (fun (z : List Bool) => nstepFn tm b (a z) (c z)) ∈ FP

One step of the search

def Complexity.addBlock (R b V : List Bool) : List Bool

Append a record to the visited string unless it is already there.

Equations

• Complexity.addBlock R b V = Complexity.Cobham.selectHead (Complexity.memFlag R b V) V (V ++ b)

theorem Complexity.addBlock_eq_self (R b V : List Bool) (h : memFlag R b V = [true]) : addBlock R b V = V

theorem Complexity.addBlock_eq_append (R b V : List Bool) (h : memFlag R b V = [false]) : addBlock R b V = V ++ b

theorem Complexity.addBlockFn_mem_FP {a b c : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) (hc : c ∈ FP) : (fun (z : List Bool) => addBlock (a z) (b z) (c z)) ∈ FP

def Complexity.curBlock (m : ℕ) (R r V : List Bool) : List Bool

The record the counter points at.

Equations

• Complexity.curBlock m R r V = Complexity.blockAt (Complexity.wideRuler m R) V r.length

theorem Complexity.curBlockFn_mem_FP {a b c : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) (hc : c ∈ FP) (m : ℕ) : (fun (z : List Bool) => curBlock m (a z) (b z) (c z)) ∈ FP

def Complexity.guardRuler (m : ℕ) (R r : List Bool) : List Bool

The visited string must be at least this long for the record to exist.

Equations

• Complexity.guardRuler m R r = List.replicate ((false :: r).length * (Complexity.wideRuler m R).length) false

theorem Complexity.guardRulerFn_mem_FP {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) (m : ℕ) : (fun (z : List Bool) => guardRuler m (a z) (b z)) ∈ FP

@[simp]

theorem Complexity.guardRuler_length (m : ℕ) (R r : List Bool) : (guardRuler m R r).length = (r.length + 1) * (m * R.length)

noncomputable def Complexity.searchBody {k : ℕ} (tm : NTM k) (m : ℕ) (R r V : List Bool) : List Bool

Expanding one record: append each successor that is not already there.

Equations

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

theorem Complexity.searchBodyFn_mem_FP {k : ℕ} (tm : NTM k) (m : ℕ) {a b c : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) (hc : c ∈ FP) : (fun (z : List Bool) => searchBody tm m (a z) (b z) (c z)) ∈ FP

noncomputable def Complexity.searchStepPair {k : ℕ} (tm : NTM k) (m : ℕ) (R : List Bool) (s : List Bool × List Bool) : List Bool × List Bool

One step of the worklist search, on the unpacked state (counter, visited). The counter is a ruler whose length is the index of the record to expand.

Equations

• Complexity.searchStepPair tm m R s = if (Complexity.guardRuler m R s.1).length ≤ s.2.length then (false :: s.1, Complexity.searchBody tm m R s.1 s.2) else (false :: s.1, s.2)

def Complexity.searchPack (R r V : List Bool) : List Bool

The packed search state: the ruler, the counter and the visited string.

Equations

• Complexity.searchPack R r V = Complexity.pair R (Complexity.pair r V)

@[simp]

theorem Complexity.searchPack_length (R r V : List Bool) : (searchPack R r V).length = 2 * R.length + 2 * r.length + V.length + 4

noncomputable def Complexity.searchStep {k : ℕ} (tm : NTM k) (m : ℕ) (z : List Bool) : List Bool

One step of the worklist search, on the packed state.

Equations

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

theorem Complexity.searchStep_pack {k : ℕ} (tm : NTM k) (m : ℕ) (R r V : List Bool) : searchStep tm m (searchPack R r V) = searchPack R (searchStepPair tm m R (r, V)).1 (searchStepPair tm m R (r, V)).2

The packed step is the unpacked step.

theorem Complexity.searchStep_iterate {k : ℕ} (tm : NTM k) (m : ℕ) (R : List Bool) (s : List Bool × List Bool) (n : ℕ) : (searchStep tm m)^[n] (searchPack R s.1 s.2) = searchPack R ((searchStepPair tm m R)^[n] s).1 ((searchStepPair tm m R)^[n] s).2

The packed iteration is the unpacked one.

theorem Complexity.searchStep_mem_FP {k : ℕ} (tm : NTM k) (m : ℕ) : searchStep tm m ∈ FP

One search step is polynomial-time.