The enumerator's loop

⚠️ Unreviewed by Bolton

The pass of PolyExists.bodyTM and the counting loop's own test are the two obligations of NTM.tallyLoop_hoareTime_of_hoare_indexed. The test is the same machine the path-counting machine of PP ⊆ PSPACE uses — TM.tallyTestTM compares the counter with the horizon and publishes the answer, and its contract is generic in the bank — so only the body has to be matched to the loop's state.

That matching is an identity: the loop's state at index v names the counter v and the two tallies of PolyExists.enumP below, over the bank PolyExists.enumRest at v + 1, which is exactly PolyExists.enumBank.

Main results

• PolyExists.enumP — the predicate the loop tallies: does the witness this count denotes work?
• PolyExists.enumBody_hoareTime — the pass, as the loop rule's body obligation
• PolyExists.enumTest_hoareTime — the test, as the loop rule's test obligation
• PolyExists.enumLoop_hoareTime — the two composed: the loop's contract

noncomputable def Complexity.PolyExists.enumP (L' : Language) (x : List Bool) (v : ℕ) : Bool

The predicate the enumerator's loop tallies: whether the witness a count denotes puts the pair in the matrix language. The count is shifted by one — the witness at count v is the one v + 1 denotes — which is what makes every witness of the admitted lengths appear.

Equations

• Complexity.PolyExists.enumP L' x v = decide (Complexity.pair x (Complexity.dropTop (v + 1)) ∈ L')

theorem Complexity.PolyExists.enumP_iff (L' : Language) (x : List Bool) (v : ℕ) : enumP L' x v = true ↔ pair x (dropTop (v + 1)) ∈ L'

theorem Complexity.PolyExists.tally_succ_pos (P : ℕ → Bool) (v : ℕ) : (NTM.tally P v + if P v = true then 1 else 0) = NTM.tally P (v + 1)

One more tally step, in the shape the pass produces.

theorem Complexity.PolyExists.tally_succ_neg (P : ℕ → Bool) (v : ℕ) : (NTM.tally (fun (u : ℕ) => !P u) v + if P v = true then 0 else 1) = NTM.tally (fun (u : ℕ) => !P u) (v + 1)

And the same for the failing tally, whose bump is the complementary one.

theorem Complexity.PolyExists.enumBody_hoareTime {k : ℕ} (M : TM k) {L' : Language} {T S : ℕ → ℕ} (hdec : M.DecidesInTime L' T) (hdecS : M.DecidesInSpace L' S) (x : List Bool) (N H v : ℕ) (I : Tape) (hI : TM.Parked I) (hISI : I.StartInvariant) (hIhead : I.head = 1) (hIz : I.cells 0 = Γ.start) (B Hb : ℕ) (hB : 1 + TM.pairInputWorkTime x (dropTop (v + 1)) ≤ B) (hB1 : 1 ≤ B) (hHb1 : 1 ≤ Hb) (hHS : (pair x (dropTop (v + 1))).length + S (pair x (dropTop (v + 1))).length + 2 ≤ Hb) (hHbH : Hb + 1 ≤ H) (hpairH : (pair x (dropTop (v + 1))).length + 1 ≤ H) : (bodyTM M).HoareTime (NTM.tallyPre (cIdx k) (aIdx k) (rIdx k) I (enumRest k x N H (v + 1)) (enumP L' x) v) (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = I ∧ 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)) ∧ out = TM.blankTape) (bodyTime k x T H Hb B v (NTM.tally (enumP L' x) v) (NTM.tally (fun (u : ℕ) => !enumP L' x u) v))

The pass, as the loop rule's body obligation. The loop's state at index v is the bank the pass starts from, and the state the pass leaves is the loop's state at v + 1.

theorem Complexity.PolyExists.enumRest_cells_zero (k : ℕ) (x : List Bool) (N H v : ℕ) (i : Fin (enumTapes k)) : (enumRest k x N H v i).cells 0 = Γ.start

@[simp]

theorem Complexity.PolyExists.enumRest_res (k : ℕ) (x : List Bool) (N H v : ℕ) : enumRest k x N H v (resIdx k) = TM.blankTape

theorem Complexity.PolyExists.enumTest_hoareTime {L' : Language} (k : ℕ) (x : List Bool) (N H v : ℕ) (I : Tape) (hI : TM.Parked I) (hIz : I.cells 0 = Γ.start) (B : ℕ) (hB : 1 + 1 + TM.binaryEqTime (v + 1).bits N.bits ≤ B) : (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k)).HoareTime (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = I ∧ 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)) ∧ out = TM.blankTape) (NTM.tallyPost (cIdx k) (aIdx k) (rIdx k) I (enumRest k x N H (v + 1 + 1)) (enumP L' x) N (v + 1)) (TM.binaryEqTime (v + 1).bits N.bits + 1 + (3 * (max (3 * (B + 3) + 1) (TM.resetBinaryWorkTime B 1) + 1) + 1))

The test, as the loop rule's test obligation. The counting machine's own test serves the enumerator unchanged: its contract is generic in the bank, and the enumerator's bank meets it.

def Complexity.PolyExists.testTime (B N v : ℕ) : ℕ

The test's running time at one index.

Equations

• Complexity.PolyExists.testTime B N v = Complexity.TM.binaryEqTime (v + 1).bits N.bits + 1 + (3 * (max (3 * (B + 3) + 1) (Complexity.TM.resetBinaryWorkTime B 1) + 1) + 1)

theorem Complexity.PolyExists.enumLoop_hoareTime {k : ℕ} (M : TM k) {L' : Language} {T S : ℕ → ℕ} (hdec : M.DecidesInTime L' T) (hdecS : M.DecidesInSpace L' S) (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 bBody bTest : ℕ) (hB1 : 1 ≤ B) (hHb1 : 1 ≤ Hb) (hpair : ∀ v < N, 1 + TM.pairInputWorkTime x (dropTop (v + 1)) ≤ B) (hspace : ∀ v < N, (pair x (dropTop (v + 1))).length + S (pair x (dropTop (v + 1))).length + 2 ≤ Hb) (hHbH : Hb + 1 ≤ H) (hlenH : ∀ v < N, (pair x (dropTop (v + 1))).length + 1 ≤ H) (hbodyB : ∀ v < N, bodyTime k x T H Hb B v (NTM.tally (enumP L' x) v) (NTM.tally (fun (u : ℕ) => !enumP L' x u) v) ≤ bBody) (heqB : ∀ v < N, 1 + 1 + TM.binaryEqTime (v + 1).bits N.bits ≤ B) (htestB : ∀ v < N, testTime B N v ≤ bTest) : ((bodyTM M).loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).HoareTime (NTM.tallyPre (cIdx k) (aIdx k) (rIdx k) I (enumRest k x N H 1) (enumP L' x) 0) (NTM.tallyPost (cIdx k) (aIdx k) (rIdx k) I (enumRest k x N H (N + 1)) (enumP L' x) N N) (N * (bBody + bTest + 5))

The enumerator's loop. Every count below the horizon is tested, the tallies come out as the two counts of PolyExists.enumP, and the loop's state ends at the horizon.