Running the matrix machine inside the enumerator

⚠️ Unreviewed by Bolton

One iteration of the enumerator runs the machine deciding the matrix language on the pair it has just built. TM.applyTM reads that pair off a work tape and writes the verdict onto another, and TM.placeWorkTM 3 7 puts the whole thing where the layout says: the matrix machine's own tapes at 3 … k + 2, the pair it reads at PolyExists.yIdx, the verdict at PolyExists.vIdx, and the enumerator's own tapes untouched on either side.

The contract below is the placed form of TM.applyTM_hoareTime_decide_space_frame — the space-bounded one, since the width it reports is what the body's wipe has to clear. Besides the verdict it records what the next iteration needs: the registers came through unchanged, and every tape of the block is parked inside a window of width H with nothing written beyond it — which is what makes the wipe that follows finite.

Main results

• PolyExists.matrixTM — the placed evaluator, and PolyExists.matrixEntry the tapes it starts on
• PolyExists.matrixTM_hoareTime — its contract, with the frame the loop body needs
• PolyExists.matrixTM_keepsWindowOn — its window, from the matrix machine's space bound

def Complexity.PolyExists.matrixTM {k : ℕ} (M : TM k) : TM (enumTapes k)

The matrix machine, reading its input from a work tape and writing its verdict onto another, placed where the enumerator's layout wants it.

Equations

• Complexity.PolyExists.matrixTM M = Complexity.TM.placeWorkTM 3 7 M.applyTM

def Complexity.PolyExists.matrixEntry {k : ℕ} (M : TM k) (extras : Fin (enumTapes k) → Tape) (y : List Bool) (I : Tape) : Fin (enumTapes k) → Tape

The tapes the placed evaluator is entered with: its own block loaded with the pair y, and the enumerator's own tapes carried through as they are.

Equations

• Complexity.PolyExists.matrixEntry M extras y I i = if h : Complexity.TM.placeWorkInMiddle 3 (k + 2) i then M.applyPre y I (Complexity.TM.placeWorkCoord 3 (k + 2) i h) else extras i

theorem Complexity.PolyExists.placeWorkCoord_vIdx (k : ℕ) (h : TM.placeWorkInMiddle 3 (k + 2) (vIdx k)) : TM.placeWorkCoord 3 (k + 2) (vIdx k) h = Fin.last (k + 1)

The verdict tape is the placed image of the evaluator's result tape.

theorem Complexity.PolyExists.vIdx_inMiddle (k : ℕ) : TM.placeWorkInMiddle 3 (k + 2) (vIdx k)

theorem Complexity.PolyExists.yIdx_inMiddle (k : ℕ) : TM.placeWorkInMiddle 3 (k + 2) (yIdx k)

theorem Complexity.PolyExists.matrixTM_hoareTime {k : ℕ} (M : TM k) {L : Language} {T S : ℕ → ℕ} (hdec : M.DecidesInTime L T) (hdecS : M.DecidesInSpace L S) (y : List Bool) (I : Tape) (hI : TM.Parked I) (hISI : I.StartInvariant) (extras : Fin (enumTapes k) → Tape) (hinv : ∀ (i : Fin (3 + (k + 2) + 7)), ¬TM.placeWorkInMiddle 3 (k + 2) i → (extras i).StartInvariant) (hhead : ∀ (i : Fin (3 + (k + 2) + 7)), ¬TM.placeWorkInMiddle 3 (k + 2) i → 1 ≤ (extras i).head) (H : ℕ) (hHS : y.length + S y.length + 2 ≤ H) : (matrixTM M).HoareTime (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = I ∧ work = matrixEntry M extras y I ∧ out = TM.parkedBlank) (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = I ∧ out = TM.parkedBlank ∧ (y ∈ L → (work (vIdx k)).cells 1 = Γ.one) ∧ (y ∉ L → (work (vIdx k)).cells 1 = Γ.zero) ∧ (∀ (i : Fin (3 + (k + 2) + 7)), ¬TM.placeWorkInMiddle 3 (k + 2) i → work i = extras i) ∧ ∀ (i : Fin (3 + (k + 2) + 7)), TM.placeWorkInMiddle 3 (k + 2) i → (work i).StartInvariant ∧ (work i).head ≤ H ∧ ∀ (j : ℕ), H < j → (work i).cells j = Γ.blank) (T y.length)

One evaluation of the matrix machine, contracted. From the placed entry tapes the stage halts inside the matrix machine's own time bound, publishes its verdict on y in cell one of the verdict tape, returns every tape outside its block untouched, and leaves its own block parked inside a window of width H.

theorem Complexity.PolyExists.matrixTM_keepsWindowOn {k : ℕ} (M : TM k) {L : Language} {S : ℕ → ℕ} (hdecS : M.DecidesInSpace L S) (hne : M.qstart ≠ M.qhalt) (y : List Bool) (I : Tape) (hISI : I.StartInvariant) (extras : Fin (enumTapes k) → Tape) (hinv : ∀ (i : Fin (3 + (k + 2) + 7)), ¬TM.placeWorkInMiddle 3 (k + 2) i → (extras i).StartInvariant) (hhead : ∀ (i : Fin (3 + (k + 2) + 7)), ¬TM.placeWorkInMiddle 3 (k + 2) i → 1 ≤ (extras i).head) {inputLength space : ℕ} (hextraW : ∀ (i : Fin (3 + (k + 2) + 7)), ¬TM.placeWorkInMiddle 3 (k + 2) i → (extras i).head ≤ space) (hspace : y.length + S y.length + 2 ≤ space) (hIhead : max I.head 1 ≤ inputLength + (y.length + S y.length + 1) + 1) : (matrixTM M).KeepsWindowOn (fun (c : Cfg (enumTapes k) (matrixTM M).Q) => c.state = (matrixTM M).qstart ∧ c.input = I ∧ c.work = matrixEntry M extras y I ∧ c.output = TM.parkedBlank) inputLength space

The evaluating stage's window. The matrix machine's own space bound is what limits it — its running time is exponential and would limit nothing.