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.spaceUsed) and how the tape head positions influence the cells that are modified on a tape.

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, (configs 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) : (configs 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) ((configs 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 : (configs 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 : (configs (initCfg input) t).workTapes i z ≠ none) : z.natAbs ≤ spaceUsedByTape (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 touched by a single work tape grows by at most one each step.

theorem Turing.MultiTapeTM.spaceUsed_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 : ℕ) : spaceUsed 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.spaceUsed_mono {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) : Monotone fun (x : ℕ) => spaceUsed cfg x

The total space used is monotone in the number of steps.