Tape head visitation and space-usage lemmas for multi-input machines

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

It is the multi-input counterpart, lemma for lemma, of the vendored CSLib file MIPRE.Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas.

theorem Turing.MultiInputTM.step_workTapes_eq_of_ne {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : Fin i → List Symbol} {tm : MultiInputTM i w Symbol State} (cfg : Cfg i w Symbol State input) (d : Fin w) (z : ℤ) (hz : z ≠ cfg.workTapePos d) : (step cfg).workTapes d z = cfg.workTapes d z

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

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

theorem Turing.MultiInputTM.mem_visitedByTapeHead_self {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : Fin i → List Symbol} {tm : MultiInputTM i w Symbol State} (cfg : Cfg i w Symbol State input) (t : ℕ) (d : Fin w) : (configs cfg t).workTapePos d ∈ visitedByTapeHead cfg t d

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

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

theorem Turing.MultiInputTM.uIcc_workTapePos_subset_visitedByTapeHead {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : Fin i → List Symbol} {tm : MultiInputTM i w Symbol State} (cfg : Cfg i w Symbol State input) (d : Fin w) (t : ℕ) : Finset.uIcc (cfg.workTapePos d) ((configs cfg t).workTapePos d) ⊆ visitedByTapeHead cfg t d

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

theorem Turing.MultiInputTM.mem_visitedByTapeHead_of_workTapes_ne {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : Fin i → List Symbol} {tm : MultiInputTM i w Symbol State} {cfg : Cfg i w Symbol State input} (d : Fin w) (t : ℕ) (z : ℤ) (h : (configs cfg t).workTapes d z ≠ cfg.workTapes d z) : z ∈ visitedByTapeHead cfg t d

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

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

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

theorem Turing.MultiInputTM.content_natAbs_le_spaceUsedByTape {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : Fin i → List Symbol} {tm : MultiInputTM i w Symbol State} {d : Fin w} (t : ℕ) (z : ℤ) (h : (configs (initCfg input) t).workTapes d z ≠ none) : z.natAbs ≤ spaceUsedByTape (initCfg input) t d

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

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

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

theorem Turing.MultiInputTM.spaceUsed_linear {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : Fin i → List Symbol} {tm : MultiInputTM i w Symbol State} (cfg : Cfg i w Symbol State input) (t : ℕ) : spaceUsed cfg t ≤ w * t + w

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

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

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

theorem Turing.MultiInputTM.spaceUsed_mono {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : Fin i → List Symbol} (tm : MultiInputTM i w Symbol State) (cfg : Cfg i w Symbol State input) : Monotone fun (x : ℕ) => spaceUsed cfg x

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