Running a loop a fixed number of times

TM.loopTM_hoareTime proves a loop terminates from an invariant and a decreasing variant. A counting loop has a more specific shape: its tape state is indexed by how many iterations have run, the index advances by one each time, and the loop stops at a known count. The rule below packages that shape, so a client supplies only two facts — one iteration advances the index, and the loop halts at the final index — with the fuel bookkeeping discharged here.

The index has to be readable from the tapes, since TM.loopTM_hoareTime's variant is a function of them; in practice it is the counter the loop is iterating.

Main results

• TM.loopTM_hoareTime_indexed — a loop that runs to a known iteration count

theorem Complexity.TM.loopTM_hoareTime_indexed {n : ℕ} (tmBody tmTest : TM n) {E : ℕ → TapePred n} {post : TapePred n} {N b : ℕ} {idx : Tape → (Fin n → Tape) → Tape → ℕ} (hidx : ∀ (j : ℕ) (inp : Tape) (work : Fin n → Tape) (out : Tape), E j inp work out → idx inp work out = j) (hstep : ∀ j < N, ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), E j inp work out → ∃ (inp' : Tape) (work' : Fin n → Tape) (out' : Tape), ∃ t ≤ b, (tmBody.loopTM tmTest).reachesIn t { state := (tmBody.loopTM tmTest).qstart, input := inp, work := work, output := out } { state := (tmBody.loopTM tmTest).qstart, input := inp', work := work', output := out' } ∧ E (j + 1) inp' work' out') (hstop : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), E N inp work out → ∃ (c' : Cfg n (tmBody.loopTM tmTest).Q), ∃ t ≤ b, (tmBody.loopTM tmTest).reachesIn t { state := (tmBody.loopTM tmTest).qstart, input := inp, work := work, output := out } c' ∧ (tmBody.loopTM tmTest).halted c' ∧ post c'.input c'.work c'.output) : (tmBody.loopTM tmTest).HoareTime (E 0) post ((N + 1) * b)

A loop that runs to a known iteration count. E j describes the tapes after j iterations and idx reads the index back off them. Given that one iteration carries E j to E (j + 1) for every j below N, and that the loop halts from E N with post, the loop carries E 0 to post.