Resetting a binary work tape #
This module exposes the framed time and space contracts for rewinding an arbitrary canonical binary cursor and clearing it to the standard blank tape.
theorem
Complexity.TM.rewindBinaryWorkTM_hoareTime_frame
{n : ℕ}
(idx : Fin n)
(bits : List Bool)
(headBound : ℕ)
(inp₀ : Tape)
(work₀ : Fin n → Tape)
(out₀ : Tape)
(htarget : (work₀ idx).HasBinaryContent bits)
(htargetStart : (work₀ idx).cells 0 = Γ.start)
(htargetHead : 1 ≤ (work₀ idx).head ∧ (work₀ idx).head ≤ headBound)
(hinput : Parked inp₀)
(hother : ∀ (i : Fin n), i ≠ idx → Parked (work₀ i))
(houtput : Parked out₀)
:
(rewindWorkTM 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 idx = (Tape.init (List.map Γ.ofBool bits)).move Dir3.right ∧ (∀ (i : Fin n), i ≠ idx → work i = work₀ i) ∧ out = out₀)
(headBound + 2)
Rewind canonical binary contents to cell one while preserving the complete external tape frame.
theorem
Complexity.TM.resetBinaryWorkTM_hoareTime_frame
{n : ℕ}
(idx : Fin n)
(bits : List Bool)
(headBound : ℕ)
(inp₀ : Tape)
(work₀ : Fin n → Tape)
(out₀ : Tape)
(htarget : (work₀ idx).HasBinaryContent bits)
(htargetStart : (work₀ idx).cells 0 = Γ.start)
(htargetHead : 1 ≤ (work₀ idx).head ∧ (work₀ idx).head ≤ headBound)
(hinput : Parked inp₀)
(hother : ∀ (i : Fin n), i ≠ idx → Parked (work₀ i))
(houtput : Parked out₀)
:
(resetBinaryWorkTM 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₀)
(resetBinaryWorkTime headBound bits.length)
Rewind and clear canonical binary contents while preserving the complete external tape frame.
theorem
Complexity.TM.resetBinaryWorkTM_prefix_withinAuxSpace
{n : ℕ}
(idx : Fin n)
(headBound bitLength inputLength initialSpace time : ℕ)
(start current : Cfg n (resetBinaryWorkTM idx).Q)
(hinitial : start.WithinAuxSpace inputLength initialSpace)
(hreach : (resetBinaryWorkTM idx).reachesIn time start current)
(htime : time ≤ resetBinaryWorkTime headBound bitLength)
:
current.WithinAuxSpace inputLength (initialSpace + resetBinaryWorkTime headBound bitLength)
Coarse all-prefix auxiliary-space envelope for binary reset.
Binary reset preserves one-way output safety.