Blanking a group of tapes and putting their heads back

TM.resetTapes_hoareTime blanks its targets by walking a fixed height across them, which leaves every head parked at the far end of the walk. A loop that reuses those tapes needs them back at cell one, so the wipe is followed by one more rewind.

The wipe is content-agnostic: nothing is assumed about where inside the wiped region the non-blank cells sit, only that nothing lies beyond it. That is what makes it the right tool for cleaning up after a simulation, whose tapes can hold anything at all.

Main results

• TM.wipeRewindTM — blank the named tapes and return their heads to cell one
• TM.wipeRewindTM_hoareTime — its contract, landing on a fully named bank

def Complexity.TM.blankTape : Tape

The blank tape parked at cell one — what a wiped-and-rewound tape becomes.

Equations

• Complexity.TM.blankTape = (Complexity.Tape.init []).move Complexity.Dir3.right

theorem Complexity.TM.blankTape_parked : Parked blankTape

theorem Complexity.TM.blankTape_startInvariant : blankTape.StartInvariant

def Complexity.TM.wipeRewindTM {n : ℕ} (targets : List (Fin n)) (r : Fin n) : TM n

Blank the named tapes, then put their heads back at cell one.

Equations

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

theorem Complexity.TM.wipeRewindTM_hoareTime {n : ℕ} (targets : List (Fin n)) (hnodup : targets.Nodup) (r : Fin n) (hr : r ∉ targets) (H : ℕ) (I₀ : Tape) (W₀ : Fin n → Tape) (O₀ : Tape) (hinpSI : I₀.StartInvariant) (hinpP : Parked I₀) (hout0 : O₀ = blankTape) (hworkSI : ∀ (j : Fin n), j ≠ r → (W₀ j).StartInvariant) (htargetHead : ∀ j ∈ targets, (W₀ j).head ≤ H) (htargetFar : ∀ j ∈ targets, ∀ (i : ℕ), H < i → (W₀ j).cells i = Γ.blank) (hworkR : W₀ r = regTape H) (hother : ∀ (j : Fin n), j ≠ r → j ∉ targets → Parked (W₀ j)) : (wipeRewindTM targets r).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = I₀ ∧ work = W₀ ∧ out = O₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = I₀ ∧ (work = fun (j : Fin n) => if j ∈ targets then blankTape else W₀ j) ∧ out = O₀) (targets.length * (H + 4) + H * 4 + 8 + 1 + (targets.length * (H + 4) + 1))

The wipe stage's contract. The targets come back blank and parked at cell one, the register that drove the walk is unchanged, and every other tape is untouched.