The wipe loop

TM.forRegTM drives a body an exact number of times off a dedicated unary fuel register. Running TM.wipeStepTM through it, fueled by a register holding v marks unrelated to any targeted tape's content, blanks the v cells starting at each target's head, whatever was there (cells 1 … v when the head is parked at cell 1; see TM.wipedTape_cells_of_head_one).

Main results

• TM.wipedTape — the closed form of v wipe steps applied to a tape
• TM.wipeLoop_hoareTime — the loop's contract

def Complexity.TM.wipedTape (t : Tape) (i : ℕ) : Tape

Wipe-step applied i times to t, in closed form.

Equations

• Complexity.TM.wipedTape t i = (fun (s : Complexity.Tape) => s.writeAndMove Complexity.Γw.blank.toΓ Complexity.Dir3.right)^[i] t

@[simp]

theorem Complexity.TM.wipedTape_zero (t : Tape) : wipedTape t 0 = t

theorem Complexity.TM.wipedTape_succ (t : Tape) (i : ℕ) : wipedTape t (i + 1) = (wipedTape t i).writeAndMove Γw.blank.toΓ Dir3.right

theorem Complexity.TM.wipedTape_head (t : Tape) (i : ℕ) : (wipedTape t i).head = t.head + i

Wiping advances the head one cell per step.

theorem Complexity.TM.wipedTape_cells_of_head_one {t : Tape} (hh : t.head = 1) (H j : ℕ) : (wipedTape t H).cells j = if 1 ≤ j ∧ j ≤ H then Γ.blank else t.cells j

What wiping does. From a head parked at cell 1, wiping H times blanks exactly cells 1 … H and leaves every other cell alone.

theorem Complexity.TM.initNil_cells (j : ℕ) : (Tape.init []).cells j = if j = 0 then Γ.start else Γ.blank

The canonical blank tape's cells, spelled out.

theorem Complexity.TM.wipedTape_eq_blank {t : Tape} (H : ℕ) (hh : t.head = 1) (h0 : t.cells 0 = Γ.start) (hfar : ∀ (j : ℕ), H < j → t.cells j = Γ.blank) : wipedTape t H = { head := H + 1, cells := (Tape.init []).cells }

Wiping really blanks the tape. A tape parked at cell 1 whose content is confined to cells 1 … H becomes literally the blank tape (head at H + 1) after H wipe steps — this is where the content-agnostic wipe pays off: no assumption is made about where inside 1 … H the nonblank cells sit.

theorem Complexity.TM.wipedTape_parked {t : Tape} (h : Parked t) (i : ℕ) : Parked (wipedTape t i)

Wiping preserves Parked-ness: the head only advances, and every written or untouched cell beyond the marker stays off ▷.

theorem Complexity.TM.parked_parkedBlank : Parked ((Tape.init []).move Dir3.right)

A fresh output tape ((Tape.init []).move Dir3.right) is Parked.

theorem Complexity.TM.outAcc_nil_of_parkedBlank : OutAcc [] ((Tape.init []).move Dir3.right)

A fresh output tape satisfies the empty output accumulator.

theorem Complexity.TM.eq_parkedBlank_of_outAcc_nil {t : Tape} (h : OutAcc [] t) : t = (Tape.init []).move Dir3.right

The only tape satisfying the empty output accumulator is the fresh parked blank tape.

theorem Complexity.TM.regIterCells_parked (v i : ℕ) : Parked { head := i + 2, cells := regCells v }

The register-shaped tape at iteration i is Parked.

theorem Complexity.TM.wipeLoop_hoareTime {n : ℕ} (targets : List (Fin n)) (r : Fin n) (hr : r ∉ targets) (v : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (hinp₀ : Parked inp₀) (hother : ∀ (j : Fin n), j ≠ r → Parked (work₀ j)) : ((wipeStepTM targets).forRegTM r).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = Function.update work₀ r (regTape v) ∧ out = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = Function.update (fun (j : Fin n) => if j ∈ targets then wipedTape (work₀ j) v else work₀ j) r (regTape v) ∧ out = (Tape.init []).move Dir3.right) (v * 3 + (v + 2))

The wipe loop. Fueled by a register at r holding v marks (r disjoint from targets), forRegTM (wipeStepTM targets) r turns every tape in targets into wipedTape of it: the v cells starting at its head are blanked and the head ends v cells further right. Every other tape — including the fuel register itself — is left exactly as it was.