Putting every head back where a stage expects it

A simulated machine leaves its heads wherever its run ended — possibly on the left marker, since a machine may halt immediately after stepping left onto it. Everything downstream wants heads parked past the marker, and the tapes a stage will read again want them back at cell one.

TM.parkRewindTM does both: one parking step for every tape, then a rewind of the input tape and of each named work tape. It is the stage that separates a simulation from whatever reads its results.

Main results

• TM.parkRewindTM — park everything, then rewind the input and the named work tapes
• TM.parkRewindTM_hoareTime — its contract, through fully pinned tape states
• TM.parkRewindWorkTM, TM.parkRewindWorkTM_hoareTime — the same for the work tapes alone, leaving the input head where the stage left it

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

Park every head past the marker, then rewind the input tape and the named work tapes to cell one.

Equations

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

def Complexity.TM.parkTape (t : Tape) : Tape

A tape with its marker only at cell zero, parked at max head 1.

Equations

• Complexity.TM.parkTape t = { head := max t.head 1, cells := t.cells }

theorem Complexity.TM.parkTape_eq_self {t : Tape} (h : 1 ≤ t.head) : parkTape t = t

Parking a tape whose head is already off the left marker changes nothing.

theorem Complexity.TM.parkTape_parked {t : Tape} (h : t.StartInvariant) : Parked (parkTape t)

theorem Complexity.TM.rewound_parked {t : Tape} (h : t.StartInvariant) : Parked { head := 1, cells := t.cells }

theorem Complexity.TM.parkRewindTM_hoareTime {n : ℕ} (targets : List (Fin n)) (hnodup : targets.Nodup) (B : ℕ) (hB : 1 ≤ B) (I₀ : Tape) (W₀ : Fin n → Tape) (O₀ : Tape) (hI : I₀.StartInvariant) (hW : ∀ (i : Fin n), (W₀ i).StartInvariant) (hO : O₀.StartInvariant) (hIB : I₀.head ≤ B) (hWB : ∀ j ∈ targets, (W₀ j).head ≤ B) : (parkRewindTM targets).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 = { head := 1, cells := I₀.cells } ∧ (work = fun (j : Fin n) => if j ∈ targets then { head := 1, cells := (W₀ j).cells } else parkTape (W₀ j)) ∧ out = parkTape O₀) (1 + 1 + (2 * (max (B + 2) (targets.length * (B + 3) + 1) + 1) + 1))

The cleanup stage's contract. Every head ends parked; the input tape and the named work tapes end at cell one, with their contents untouched. Only Tape.StartInvariant is asked of the starting tapes — a head may still be sitting on the marker, which is exactly the state a halted simulation can leave behind.

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

Park every head past the marker, then rewind only the named work tapes. The input tape keeps its head — a stage whose input head is itself part of the state being simulated cannot afford to have it rewound.

Equations

• Complexity.TM.parkRewindWorkTM targets = Complexity.TM.skipTM.seqTM (Complexity.TM.bigSeqTM (List.map Complexity.TM.rewindWorkTM targets))

theorem Complexity.TM.parkRewindWorkTM_hoareTime {n : ℕ} (targets : List (Fin n)) (hnodup : targets.Nodup) (B : ℕ) (hB : 1 ≤ B) (I₀ : Tape) (W₀ : Fin n → Tape) (O₀ : Tape) (hI : I₀.StartInvariant) (hW : ∀ (i : Fin n), (W₀ i).StartInvariant) (hO : O₀.StartInvariant) (hWB : ∀ j ∈ targets, (W₀ j).head ≤ B) : (parkRewindWorkTM targets).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 = parkTape I₀ ∧ (work = fun (j : Fin n) => if j ∈ targets then { head := 1, cells := (W₀ j).cells } else parkTape (W₀ j)) ∧ out = parkTape O₀) (1 + 1 + (targets.length * (B + 3) + 1))

The work-only cleanup stage's contract. The named work tapes end at cell one with their contents untouched; every other head ends merely parked.