Clearing a binary work tape

This module exposes a literal-frame contract for erasing a canonical Boolean work tape and returning its head to cell one. It also records the one-way-output discipline of the clearing, rewinding, and composite machines.

Main results

• clearWorkTM_hoareTime_frame — clear and rewind with a full external frame.
• clearWorkTM_hoareTimeSpace_frame — the corresponding all-prefix space contract.
• clearWorkTM_isTransducer — clearing never moves the output head left.

theorem Complexity.TM.clearWorkTM_hoareTime_frame {n : ℕ} (idx : Fin n) (bits : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (htarget : work₀ idx = (Tape.init (List.map Γ.ofBool bits)).move Dir3.right) (hinp : Parked inp₀) (hother : ∀ (i : Fin n), i ≠ idx → Parked (work₀ i)) (hout : Parked out₀) : (clearWorkTM idx).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₀ ∧ work = Function.update work₀ idx ((Tape.init []).move Dir3.right) ∧ out = out₀) (clearWorkTimeBound bits.length)

Clearing a canonical Boolean work tape preserves the input, output, and every unrelated work tape literally, and resets the target to the standard parked blank tape within 2 * bits.length + 5 steps.

theorem Complexity.TM.clearWorkTM_hoareTimeSpace_frame {n : ℕ} (idx : Fin n) (bits : List Bool) (inputLength initialSpace : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (htarget : work₀ idx = (Tape.init (List.map Γ.ofBool bits)).move Dir3.right) (hinp : Parked inp₀) (hother : ∀ (i : Fin n), i ≠ idx → Parked (work₀ i)) (hout : Parked out₀) (hinitial : { state := (clearWorkTM idx).qstart, input := inp₀, work := work₀, output := out₀ }.WithinAuxSpace inputLength initialSpace) : (clearWorkTM idx).HoareTimeSpace (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₀ ∧ work = Function.update work₀ idx ((Tape.init []).move Dir3.right) ∧ out = out₀) (clearWorkTimeBound bits.length) inputLength (initialSpace + clearWorkTimeBound bits.length)

Time-and-space form of clearWorkTM_hoareTime_frame. Starting from an initialSpace budget, one extra cell per possible transition yields an honest all-reachable bound.

theorem Complexity.TM.blankWorkTM_isTransducer {n : ℕ} (idx : Fin n) : (blankWorkTM idx).IsTransducer

Blanking a work tape never moves the output head left.

theorem Complexity.TM.rewindWorkTM_isTransducer {n : ℕ} (idx : Fin n) : (rewindWorkTM idx).IsTransducer

Rewinding a work tape never moves the output head left.

theorem Complexity.TM.clearWorkTM_isTransducer {n : ℕ} (idx : Fin n) : (clearWorkTM idx).IsTransducer

Clearing and rewinding a work tape never moves the output head left.