Tape head visitation and space-usage lemmas

This file collects lemmas about the set of positions visited by a work-tape head (MultiTapeTM.visitedByTapeHead) and the resulting space-usage measures (MultiTapeTM.spaceUsedByTape, MultiTapeTM.space) and how the tape head positions influence the cells that are modified on a tape.

MultiTapeTM.exists_spaceUsedByTape_max shows that a computation whose space usage is bounded attains its per-tape space usage at a single step, which makes a bound that holds at every point in time usable as a bound for the whole run.

theorem Turing.MultiTapeTM.step_workTapes_eq_of_ne {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} (cfg : Cfg k Symbol State input) (j : Fin k) (z : ℤ) (hz : z ≠ cfg.workTapePos j) : (step cfg).workTapes j z = cfg.workTapes j z

If the work tape head is not at position z, then the tape does not change there.

theorem Turing.MultiTapeTM.mem_visitedByTapeHead {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} {cfg : Cfg k Symbol State input} {t : ℕ} {i : Fin k} {z : ℤ} : z ∈ visitedByTapeHead cfg t i ↔ ∃ t' < t + 1, (runFrom cfg t').workTapePos i = z

theorem Turing.MultiTapeTM.mem_visitedByTapeHead_self {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : (runFrom cfg t).workTapePos i ∈ visitedByTapeHead cfg t i

theorem Turing.MultiTapeTM.visitedByTapeHead_mono {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} (cfg : Cfg k Symbol State input) (i : Fin k) {t t' : ℕ} (h : t ≤ t') : visitedByTapeHead cfg t i ⊆ visitedByTapeHead cfg t' i

The set of positions visited by a tape head is monotone in the number of steps.

theorem Turing.MultiTapeTM.uIcc_workTapePos_subset_visitedByTapeHead {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} (cfg : Cfg k Symbol State input) (i : Fin k) (t : ℕ) : Finset.uIcc (cfg.workTapePos i) ((runFrom cfg t).workTapePos i) ⊆ visitedByTapeHead cfg t i

Starting from configuration cfg, every position between the initial head position of tape i and the one after t steps is part of the "visited set" at step t.

theorem Turing.MultiTapeTM.mem_visitedByTapeHead_of_workTapes_ne {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} {cfg : Cfg k Symbol State input} (j : Fin k) (t : ℕ) (z : ℤ) (h : (runFrom cfg t).workTapes j z ≠ cfg.workTapes j z) : z ∈ visitedByTapeHead cfg t j

If a work tape cell is changed after t steps, it must have been visited by the tape head.

theorem Turing.MultiTapeTM.natAbs_le_spaceUsedByTape_of_mem_visited {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} {cfg : Cfg k Symbol State input} {i : Fin k} {z : ℤ} {t : ℕ} (hz : z ∈ visitedByTapeHead cfg t i) : (z - cfg.workTapePos i).natAbs ≤ spaceUsedByTape cfg t i

Every position visited by the head of tape i lies within spaceUsedByTape … i of the head's starting position.

theorem Turing.MultiTapeTM.content_natAbs_le_spaceUsedByTape {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} {i : Fin k} (t : ℕ) (z : ℤ) (h : (runFrom (tm.initCfg input) t).workTapes i z ≠ none) : z.natAbs ≤ spaceUsedByTape (tm.initCfg input) t i

Every non-blank cell on work tape i lies within spaceUsedByTape … i t of the origin.

theorem Turing.MultiTapeTM.spaceUsedByTape_le {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : spaceUsedByTape cfg t i ≤ t + 1

The number of cells visited by a single work-tape head grows by at most one each step.

theorem Turing.MultiTapeTM.space_linear {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} (cfg : Cfg k Symbol State input) (t : ℕ) : space cfg t ≤ k * t + k

The space used by a computation is bounded linearly by the number of steps.

theorem Turing.MultiTapeTM.spaceUsedByTape_mono {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (i : Fin k) : Monotone fun (x : ℕ) => spaceUsedByTape cfg x i

The space used by a single tape is monotone in the number of steps.

theorem Turing.MultiTapeTM.exists_spaceUsedByTape_max {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} (cfg : Cfg k Symbol State input) {s : ℕ} (hs : ∀ (t : ℕ), space cfg t ≤ s) : ∃ (T : ℕ), ∀ (t : ℕ) (i : Fin k), spaceUsedByTape cfg t i ≤ spaceUsedByTape cfg T i

A computation whose total space usage stays below a bound reaches a step T at which the space usage of every tape is maximal. This turns a bound that holds at every point in time into a bound for the whole run.

theorem Turing.MultiTapeNTM.RunPath.inWindow_of_space_le {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} {p : tm.RunPath input} {s : ℕ} (h0 : ∀ (i : Fin k), (RelSeries.head p).workTapePos i = 0) (hs : p.space ≤ s) : p.InWindow s

A run path that starts with every head at cell 0 and visits at most s cells keeps its heads within [-s, s].