Chaining a sequence of stages through pinned tape states

A machine assembled from many subroutines is a TM.bigSeqTM of stages, each carrying the tape state from one pinned configuration to the next. TM.bigSeqTM_hoareTime already chains stages, but only through the EmitPred state shape, whose output component is a written list. A stage that leaves a counter tape half-scanned, or two tallies at different values, does not fit that shape.

The rule below chains through arbitrary pinned states — a fixed input tape, a family of work banks, and a family of output tapes — asking only that every pinned tape be Parked, which is what makes the phase transitions between stages no-ops.

Main results

• TM.bigSeqTM_hoareTime_pinned_gen — the chain rule for arbitrary pinned tape states, input tape included
• TM.bigSeqTM_hoareTime_pinned — the same with a fixed input tape

theorem Complexity.TM.bigSeqTM_hoareTime_pinned_gen {n : ℕ} (ms : List (TM n)) (I : ℕ → Tape) (W : ℕ → Fin n → Tape) (O : ℕ → Tape) (b : ℕ) : (∀ (k : ℕ), Parked (I k)) → (∀ (k : ℕ) (i : Fin n), Parked (W k i)) → (∀ (k : ℕ), Parked (O k)) → (∀ (k : ℕ) (hk : k < ms.length), ms[k].HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = I k ∧ work = W k ∧ out = O k) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = I (k + 1) ∧ work = W (k + 1) ∧ out = O (k + 1)) b) → (bigSeqTM ms).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = I 0 ∧ work = W 0 ∧ out = O 0) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = I ms.length ∧ work = W ms.length ∧ out = O ms.length) (ms.length * (b + 1) + 1)

Chaining stages through pinned tape states. Stage k carries the pinned state k to the pinned state k + 1; the fold carries state 0 to state ms.length. Every pinned tape is required Parked, which makes the phase transition between consecutive stages a no-op.

The input tape is indexed too. A stage may move the input head — a rewind does — and then the next stage's precondition names a different input tape, so a single fixed one will not do.

theorem Complexity.TM.bigSeqTM_hoareTime_pinned {n : ℕ} (ms : List (TM n)) (I : Tape) (W : ℕ → Fin n → Tape) (O : ℕ → Tape) (b : ℕ) (hI : Parked I) (hW : ∀ (k : ℕ) (i : Fin n), Parked (W k i)) (hO : ∀ (k : ℕ), Parked (O k)) (hms : ∀ (k : ℕ) (hk : k < ms.length), ms[k].HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = I ∧ work = W k ∧ out = O k) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = I ∧ work = W (k + 1) ∧ out = O (k + 1)) b) : (bigSeqTM ms).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = I ∧ work = W 0 ∧ out = O 0) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = I ∧ work = W ms.length ∧ out = O ms.length) (ms.length * (b + 1) + 1)

The chain rule with a fixed input tape, the common case: no stage moves the input head.