A counting loop whose resting tapes change with the count

⚠️ Unreviewed by Bolton

NTM.tallyLoop_hoareTime_of_hoare pins the tapes the tally state does not name to one bank, the same at every index. That is right for a loop whose only state is its counters — the path-counting machine of PP ⊆ PSPACE — but not for one carrying something alongside them.

The witness enumerator of PH ⊆ PSPACE is such a loop: its witness tape advances with the counter, so the bank it rests in is a function of the count. These are the same two rules with that bank indexed; the proofs are unchanged apart from the index.

Main results

• NTM.tallyLoop_hoareTime_of_hoare_indexed — the loop's contract, with an indexed resting bank
• NTM.tallyLoop_keepsWindow_of_hoare_indexed — its window, one iteration wide

theorem Complexity.NTM.tallyLoop_hoareTime_of_hoare_indexed {n : ℕ} (tmBody tmTest : TM n) (cIdx aIdx rIdx : Fin n) (I : Tape) (rest : ℕ → Fin n → Tape) (P : ℕ → Bool) (mid : ℕ → TM.TapePred n) (N bBody bTest : ℕ) (hN : 1 ≤ N) (hI : TM.Parked I) (hrest : ∀ (v : ℕ) (i : Fin n), TM.Parked (rest v i)) (hbody : ∀ v < N, tmBody.HoareTime (tallyPre cIdx aIdx rIdx I (rest v) P v) (mid v) bBody) (hmid : ∀ (v : ℕ) (inp : Tape) (work : Fin n → Tape) (out : Tape), mid v inp work out → TM.LoopParked inp work out) (htest : ∀ v < N, tmTest.HoareTime (mid v) (tallyPost cIdx aIdx rIdx I (rest (v + 1)) P N (v + 1)) bTest) : (tmBody.loopTM tmTest).HoareTime (tallyPre cIdx aIdx rIdx I (rest 0) P 0) (tallyPost cIdx aIdx rIdx I (rest N) P N N) (N * (bBody + bTest + 5))

The counting loop, with a bank that changes with the count.

theorem Complexity.NTM.tallyLoop_keepsWindow_of_hoare_indexed {n : ℕ} (tmBody tmTest : TM n) (cIdx aIdx rIdx : Fin n) (I : Tape) (rest : ℕ → Fin n → Tape) (P : ℕ → Bool) (mid : ℕ → TM.TapePred n) (N bBody bTest inputLength : ℕ) (hN : 1 ≤ N) (hI : TM.Parked I) (hrest : ∀ (v : ℕ) (i : Fin n), TM.Parked (rest v i)) (hIhead : I.head ≤ inputLength + 1) (hrestHead : ∀ (v : ℕ) (i : Fin n), (rest v i).head ≤ 1) (hbody : ∀ v < N, tmBody.HoareTime (tallyPre cIdx aIdx rIdx I (rest v) P v) (mid v) bBody) (hmid : ∀ (v : ℕ) (inp : Tape) (work : Fin n → Tape) (out : Tape), mid v inp work out → TM.LoopParked inp work out) (htest : ∀ v < N, tmTest.HoareTime (mid v) (tallyPost cIdx aIdx rIdx I (rest (v + 1)) P N (v + 1)) bTest) (inp : Tape) (work : Fin n → Tape) (out : Tape) : tallyPre cIdx aIdx rIdx I (rest 0) P 0 inp work out → ∀ (c : Cfg n (tmBody.loopTM tmTest).Q), (tmBody.loopTM tmTest).reaches { state := (tmBody.loopTM tmTest).qstart, input := inp, work := work, output := out } c → c.WithinDecisionSpace inputLength (1 + (bBody + bTest + 5))

Its window, one iteration wide.