What a space bound says about the tape, not just the head

⚠️ Unreviewed by Bolton

Cfg.WithinDecisionSpace bounds head positions. A caller that has to clear up after a subroutine needs more: it needs to know that nothing was written past the window, so that a wipe of that width suffices. That follows, since a step writes only under its head — but it has to be carried along the run.

Bounding the same thing by the running time instead would be a disaster here: a space-bounded machine may run for exponentially many steps, and a wipe of exponential width is not a wipe a polynomial-space machine can afford.

Main results

• TM.work_cells_far_of_reachesIn — a run whose heads stay inside S writes nothing past S

theorem Complexity.TM.work_cells_far_of_reachesIn {n : ℕ} {tm : TM n} (S : ℕ) {t : ℕ} {c c' : Cfg n tm.Q} : tm.reachesIn t c c' → (∀ (d : Cfg n tm.Q), tm.reaches c d → ∀ (i : Fin n), (d.work i).head ≤ S) → (∀ (i : Fin n) (p : ℕ), S < p → (c.work i).cells p = Γ.blank) → ∀ (i : Fin n) (p : ℕ), S < p → (c'.work i).cells p = Γ.blank

A run that stays inside a window writes nothing outside it. Each step writes only under its head, and every head along the run is inside the window, so a cell beyond it still holds what it did at the start.