The enumerator's loop, in space

⚠️ Unreviewed by Bolton

The loop runs exponentially many iterations, so no bound derived from its total running time can be polynomial. What is polynomial is one iteration, and every state the loop returns to has all its heads at cell one — that is what TM.loopTM_keepsWindowOn_phases turns into a window for the whole run.

Main results

• PolyExists.enumTest_keepsWindowOn — the test's window, straight from its running time

theorem Complexity.PolyExists.enumTest_keepsWindowOn {L' : Language} (k : ℕ) (x : List Bool) (N H v : ℕ) (I : Tape) (hI : TM.Parked I) (hIz : I.cells 0 = Γ.start) (hIhead : I.head = 1) (B G : ℕ) (hB : 1 + 1 + TM.binaryEqTime (v + 1).bits N.bits ≤ B) (hG1 : 1 ≤ G) : (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k)).KeepsWindowOn (fun (c : Cfg (enumTapes k) (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k)).Q) => c.state = (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k)).qstart ∧ c.input = I ∧ c.work = enumBank k x N H (v + 1) (NTM.tally (enumP L' x) (v + 1)) (NTM.tally (fun (u : ℕ) => !enumP L' x u) (v + 1)) ∧ c.output = TM.blankTape) x.length (G + testTime B N v)

The loop's test keeps a window. Unlike the body, the test is short: its window is read off its running time.

noncomputable def Complexity.PolyExists.loopPB (L' : Language) (k : ℕ) (x : List Bool) (N H : ℕ) (I : Tape) : TM.TapePred (enumTapes k)

The tapes the loop's body is entered on: the counting state at some count below the horizon.

Equations

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

noncomputable def Complexity.PolyExists.loopPT (L' : Language) (k : ℕ) (x : List Bool) (N H : ℕ) (I : Tape) : TM.TapePred (enumTapes k)

The tapes the loop's test is entered on: what one pass leaves.

Equations

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

noncomputable def Complexity.PolyExists.loopPL (L' : Language) (k : ℕ) (x : List Bool) (N H : ℕ) (I : Tape) : TM.LoopPhase → TM.TapePred (enumTapes k)

The tapes of the rewind-and-check phases: the same bank, with the verdict slot's head on its way back to cell one.

Equations

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

theorem Complexity.PolyExists.loop_hBT {k : ℕ} (M : TM k) {L' : Language} {T S : ℕ → ℕ} (hdec : M.DecidesInTime L' T) (hdecS : M.DecidesInSpace L' S) (x : List Bool) (N H : ℕ) (I : Tape) (hI : TM.Parked I) (hIsi : I.StartInvariant) (hIhead : I.head = 1) (hIz : I.cells 0 = Γ.start) (B Hb : ℕ) (hB1 : 1 ≤ B) (hHb1 : 1 ≤ Hb) (hHbH : Hb + 1 ≤ H) (hpair : ∀ j < N, 1 + TM.pairInputWorkTime x (dropTop (j + 1)) ≤ B) (hspace : ∀ j < N, (pair x (dropTop (j + 1))).length + S (pair x (dropTop (j + 1))).length + 2 ≤ Hb) (hlenH : ∀ j < N, (pair x (dropTop (j + 1))).length + 1 ≤ H) (c c' : Cfg (enumTapes k) ((bodyTM M).loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).Q) : c.state = Sum.inl (bodyTM M).qhalt → (∃ (d : Cfg (enumTapes k) (bodyTM M).Q), d.state = (bodyTM M).qstart ∧ loopPB L' k x N H I d.input d.work d.output ∧ (bodyTM M).reaches d { state := (bodyTM M).qhalt, input := c.input, work := c.work, output := c.output }) → ((bodyTM M).loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).step c = some c' → (bodyTM M).LoopTapeInv (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k)) (loopPB L' k x N H I) (loopPT L' k x N H I) (loopPL L' k x N H I) c'

Leaving the body. When the pass halts, the tapes are the ones the test is entered on.

theorem Complexity.PolyExists.loop_hTL {k : ℕ} (M : TM k) {L' : Language} (x : List Bool) (N H : ℕ) (I : Tape) (hI : TM.Parked I) (hIz : I.cells 0 = Γ.start) (B : ℕ) (hB : ∀ j < N, 1 + 1 + TM.binaryEqTime (j + 1).bits N.bits ≤ B) (c c' : Cfg (enumTapes k) ((bodyTM M).loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).Q) : c.state = Sum.inr (Sum.inr (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k)).qhalt) → (∃ (d : Cfg (enumTapes k) (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k)).Q), d.state = (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k)).qstart ∧ loopPT L' k x N H I d.input d.work d.output ∧ (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k)).reaches d { state := (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k)).qhalt, input := c.input, work := c.work, output := c.output }) → ((bodyTM M).loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).step c = some c' → (bodyTM M).LoopTapeInv (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k)) (loopPB L' k x N H I) (loopPT L' k x N H I) (loopPL L' k x N H I) c'

Leaving the test. Its verdict sits in the slot, and the loop begins rewinding it.

theorem Complexity.PolyExists.outSlot_cells_startInvariant (s : Γw) (t : Tape) (hcells : t.cells = (NTM.outSlot s).cells) : t.StartInvariant

theorem Complexity.PolyExists.loop_hLL {k : ℕ} (M : TM k) {L' : Language} (x : List Bool) (N H : ℕ) (I : Tape) (hI : TM.Parked I) (c c' : Cfg (enumTapes k) ((bodyTM M).loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).Q) (ph : TM.LoopPhase) : c.state = Sum.inr (Sum.inl ph) → loopPL L' k x N H I ph c.input c.work c.output → ((bodyTM M).loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).step c = some c' → (bodyTM M).LoopTapeInv (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k)) (loopPB L' k x N H I) (loopPT L' k x N H I) (loopPL L' k x N H I) c'

The bookkeeping phases. The rewind moves only the output head; the check either halts the loop or starts the next pass on the very same tapes.

theorem Complexity.PolyExists.enumLoop_keepsWindowOn {k : ℕ} (M : TM k) {L' : Language} {T S : ℕ → ℕ} (hdec : M.DecidesInTime L' T) (hdecS : M.DecidesInSpace L' S) (hne : M.qstart ≠ M.qhalt) (x : List Bool) (N H : ℕ) (hN : 1 ≤ N) (I : Tape) (hI : TM.Parked I) (hIsi : I.StartInvariant) (hIhead : I.head = 1) (hIz : I.cells 0 = Γ.start) (B Hb G W : ℕ) (hB1 : 1 ≤ B) (hHb1 : 1 ≤ Hb) (hHbH : Hb + 1 ≤ H) (hpair : ∀ j < N, 1 + TM.pairInputWorkTime x (dropTop (j + 1)) ≤ B) (hspace : ∀ j < N, (pair x (dropTop (j + 1))).length + S (pair x (dropTop (j + 1))).length + 2 ≤ Hb) (hlenH : ∀ j < N, (pair x (dropTop (j + 1))).length + 1 ≤ H) (heqB : ∀ j < N, 1 + 1 + TM.binaryEqTime (j + 1).bits N.bits ≤ B) (hG1 : 1 ≤ G) (hGB : B ≤ G) (hGHb : Hb + 1 ≤ G) (hGpair : ∀ j < N, (pair x (dropTop (j + 1))).length + 1 ≤ G) (hW1 : G + 1 ≤ W) (hW2 : ∀ j < N, G + TM.pairInputWorkTime x (dropTop (j + 1)) ≤ W) (hW3 : G + (1 + 1 + (2 * (max (B + 2) (3 * (B + 3) + 1) + 1) + 1)) ≤ W) (hW4 : ∀ j < N, G + (2 * (pair x (dropTop (j + 1))).length + 5) ≤ W) (hW6 : G + (1 + 1 + (2 * (max (Hb + 2) (1 * (Hb + 3) + 1) + 1) + 1)) ≤ W) (hW8 : ∀ j < N, G + (3 * (max (1 + 1 + max (TM.binarySuccTime (NTM.tally (enumP L' x) j)) (TM.binarySuccTime (NTM.tally (fun (u : ℕ) => !enumP L' x u) j)) + 5) (TM.binarySuccTime j) + 1) + 1) ≤ W) (hW9 : ∀ j < N, G + TM.binaryBumpTime (dropTop (j + 1)) ≤ W) (hW10 : G + ((scratchTargets k).length * (H + 4) + H * 4 + 8 + 1 + ((scratchTargets k).length * (H + 4) + 1)) ≤ W) (hWtest : ∀ j < N, G + testTime B N j ≤ W) (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) : NTM.tallyPre (cIdx k) (aIdx k) (rIdx k) I (enumRest k x N H 1) (enumP L' x) 0 inp work out → ∀ (c : Cfg (enumTapes k) ((bodyTM M).loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).Q), ((bodyTM M).loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).reaches { state := ((bodyTM M).loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).qstart, input := inp, work := work, output := out } c → c.WithinDecisionSpace x.length W

The enumerator's loop keeps a window. The loop runs exponentially many iterations; what bounds its space is one iteration's width, and the fact that every state it returns to has all its heads at cell one.