An unconditional, content-agnostic wipe step

Reusing an opaque machine's scratch tapes across calls needs them genuinely blank in between, but an arbitrary machine may leave gaps — an isolated blank cell with more content beyond it — and a content-driven scanner (TM.blankWorkTM stops at the first blank) under-wipes there. TM.wipeStepTM writes Γ.blank to every targeted tape and advances, unconditionally, never reading what it overwrites; iterated a known number of times it blanks an exact number of cells whatever was there.

Main results

• TM.wipeStepTM — blank one cell of every targeted tape and advance
• TM.wipeStepTM_hoareTime — its one-step contract

inductive Complexity.TM.WipeStepPhase : Type

Control states of the unconditional wipe-step machine.

• running : WipeStepPhase

  Write blank to every targeted tape and advance; then halt.

• done : WipeStepPhase

  Halted.

@[implicit_reducible]

instance Complexity.TM.instDecidableEqWipeStepPhase : DecidableEq WipeStepPhase

Equations

• Complexity.TM.instDecidableEqWipeStepPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.TM.instFintypeWipeStepPhase : Fintype WipeStepPhase

Equations

• Complexity.TM.instFintypeWipeStepPhase = { elems := {Complexity.TM.WipeStepPhase.running, Complexity.TM.WipeStepPhase.done}, complete := ⋯ }

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

One unconditional step: every work tape named in targets is written Γ.blank and its head advances right; every other work tape, the input, and the output are held by readBackWrite/idleDir. Does not inspect the targeted tapes' contents at all.

Equations

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

theorem Complexity.TM.wipeStepTM_hoareTime {n : ℕ} (targets : List (Fin n)) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hinp : Parked inp₀) (hout : Parked out₀) (hother : ∀ i ∉ targets, Parked (work₀ i)) : (wipeStepTM targets).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ out = out₀ ∧ ∀ (i : Fin n), work i = if i ∈ targets then (work₀ i).writeAndMove Γw.blank.toΓ Dir3.right else work₀ i) 1

wipeStepTM's exact one-step Hoare contract. From tapes where every non-targeted work tape, the input, and the output are Parked, one step unconditionally blanks and advances every targeted work tape and preserves everything else exactly.