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.

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.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.

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 : ℕ), spaceUsed 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.MultiTapeTM.visitedByTapeHead_subset {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} {S : Finset ℤ} (h : ∀ m ≤ t, (runFrom cfg m).workTapePos i ∈ S) : visitedByTapeHead cfg t i ⊆ S

Every position the head takes up to step t lies in S, so the whole visited set does. This is Finset.image_subset_iff for the visited set, and the workhorse behind the space bounds below.

theorem Turing.MultiTapeTM.spaceUsedByTape_le_card {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} {S : Finset ℤ} (h : ∀ m ≤ t, (runFrom cfg m).workTapePos i ∈ S) : spaceUsedByTape cfg t i ≤ S.card

A set containing every position of a head bounds the space used by its tape.

theorem Turing.MultiTapeTM.visitedByTapeHead_subset_Icc {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} (cfg : Cfg k Symbol State input) {t s : ℕ} {i : Fin k} (h0 : cfg.workTapePos i = 0) (hs : spaceUsed cfg t ≤ s) : visitedByTapeHead cfg t i ⊆ Finset.Icc (-↑s) ↑s

A run that starts with the head of tape i at cell 0 and uses at most s cells keeps that head within [-s, s].

theorem Turing.MultiTapeTM.spaceUsed_le_of_visited_subset_Icc {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} (cfg : Cfg k Symbol State input) (t : ℕ) {σ : ℕ} (h : ∀ (i : Fin k), visitedByTapeHead cfg t i ⊆ Finset.Icc (-↑σ) ↑σ) : spaceUsed cfg t ≤ 2 * k * σ + k

A run whose heads all stay within [-σ, σ] uses at most 2 * σ + 1 cells per tape.

theorem Turing.MultiTapeTM.spaceUsedByTape_le_one {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} (h : ∀ m ≤ t, (runFrom cfg m).workTapePos i = cfg.workTapePos i) : spaceUsedByTape cfg t i ≤ 1

A head that never moves uses a single cell.

theorem Turing.MultiTapeTM.visitedByTapeHead_add {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} (cfg : Cfg k Symbol State input) (a b : ℕ) (i : Fin k) : visitedByTapeHead cfg (a + b) i = visitedByTapeHead cfg a i ∪ visitedByTapeHead (runFrom cfg a) b i

The cells a run visits are the ones visited by its two halves.

theorem Turing.MultiTapeTM.spaceUsed_add_le {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} (cfg : Cfg k Symbol State input) (a b : ℕ) : spaceUsed cfg (a + b) ≤ spaceUsed cfg a + spaceUsed (runFrom cfg a) b

Splitting a run into two phases can only overcount the cells it visits, since the two phases may revisit each other's cells.

theorem Turing.MultiTapeTM.spaceUsed_eq_of_workTapePos {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} {State' : Type u_3} {input' : List Symbol} {tm' : MultiTapeTM k Symbol State'} (cfg : Cfg k Symbol State input) (cfg' : Cfg k Symbol State' input') (t : ℕ) (h : ∀ m ≤ t, (runFrom cfg m).workTapePos = (runFrom cfg' m).workTapePos) : spaceUsed cfg t = spaceUsed cfg' t

Space usage only depends on where the work-tape heads are at each step, so two runs whose head positions agree use the same space. This is what lets a machine be replaced by a simulation of it.

theorem Turing.MultiTapeTM.spaceUsed_le_of_workTapePos_embedding {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} {k' : ℕ} {State' : Type u_3} {input' : List Symbol} {tm' : MultiTapeTM k' Symbol State'} (e : Fin k ↪ Fin k') (cfg : Cfg k Symbol State input) (cfg' : Cfg k' Symbol State' input') {t : ℕ} (b : ℕ) (he : ∀ m ≤ t, ∀ (j : Fin k), (runFrom cfg m).workTapePos j = (runFrom cfg' m).workTapePos (e j)) (hrest : ∀ l ∉ Set.range ⇑e, spaceUsedByTape cfg' t l ≤ b) : spaceUsed cfg' t ≤ spaceUsed cfg t + (k' - k) * b

Space of a simulation. If the heads of tm' on the tapes e j follow the heads of tm on the tapes j, and each remaining tape of tm' visits at most b cells, then tm' uses the space of tm plus at most b cells per remaining tape.

theorem Turing.MultiTapeTM.visitedByTapeHead_eq_of_halt {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} (cfg : Cfg k Symbol State input) {τ t : ℕ} (hle : τ ≤ t) (hhalt : (runFrom cfg τ).state = none) (i : Fin k) : visitedByTapeHead cfg t i = visitedByTapeHead cfg τ i

After the machine has halted the heads no longer move, so the visited set stops growing.

theorem Turing.MultiTapeTM.spaceUsed_eq_of_halt {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} (cfg : Cfg k Symbol State input) {τ t : ℕ} (hle : τ ≤ t) (hhalt : (runFrom cfg τ).state = none) : spaceUsed cfg t = spaceUsed cfg τ

After the machine has halted the heads no longer move, so the space usage stops growing.

theorem Turing.MultiTapeTM.spaceUsed_le_of_workTapePos_const {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} (cfg : Cfg k Symbol State input) (u : ℕ) (h : ∀ m ≤ u, (runFrom cfg m).workTapePos = cfg.workTapePos) : spaceUsed cfg u ≤ k

A run that never moves a work-tape head visits one cell per tape.

Output already present

theorem Turing.MultiTapeTM.step_prependOutput {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} (cfg : Cfg k Symbol State input) (pre : List Symbol) : step (cfg.prependOutput pre) = (step cfg).prependOutput pre

A machine never reads its output tape, so a word already present there is simply carried along by a step.

theorem Turing.MultiTapeTM.runFrom_prependOutput {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} (cfg : Cfg k Symbol State input) (pre : List Symbol) (n : ℕ) : runFrom (cfg.prependOutput pre) n = (runFrom cfg n).prependOutput pre

A word already on the output tape is inert. The run is the run without it, with the word prepended to whatever the machine emits.

theorem Turing.MultiTapeTM.spaceUsed_prependOutput {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} (cfg : Cfg k Symbol State input) (pre : List Symbol) (n : ℕ) : spaceUsed (cfg.prependOutput pre) n = spaceUsed cfg n

A word already on the output tape does not affect the space used.