Space of run paths and of halted runs

The additions of Christian Reitwiessner's branch crei/tidy-universal and of cslib PR #1111 to Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas.

MultiTapeTM.space (the space of the first t steps from a configuration) is read through the cells each head visits: the visited set is monotone, splits along a run, stops growing once the machine halts, and depends only on the head positions.

MultiTapeNTM.RunPath.space_le_mul_time_add_one bounds the space of any run path by its length.

MultiTapeTM.runsInSpace_of_runPath turns the space of a single run path to a halted configuration into a space bound for every computation path, since a deterministic machine stays where it is after halting.

Main results

• Turing.MultiTapeNTM.RunPath.space_le_mul_time_add_one.
• Turing.MultiTapeTM.mem_of_last_halted, Turing.MultiTapeTM.runsInSpace_of_runPath.
• Turing.MultiTapeTM.space_add_le, Turing.MultiTapeTM.space_eq_of_halt, Turing.MultiTapeTM.space_eq_of_workTapePos: the space of a run, split, after halting, and of runs with the same head positions.
• Turing.MultiTapeTM.runsInSpace_of_halted: a space bound on a halted run bounds every computation path.
• Turing.MultiTapeTM.exists_runPath_iff_runFrom: a run path to a halted configuration is the run of the given number of steps, with its space.
• Turing.MultiTapeTM.exists_visitedByTapeHead_eq_Icc, Turing.MultiTapeTM.workTapes_runFrom_eq_of_notMem_visitedByTapeHead: the visited cells of a work-tape head form an interval, and unvisited cells keep their contents.

theorem Turing.MultiTapeNTM.RunPath.space_le_mul_time_add_one {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (p : ntm.RunPath input) : p.space ≤ k * (p.time + 1)

Each head visits at most one cell per configuration, so a path visits at most k * (time + 1) cells.

Space of halted runs

theorem Turing.MultiTapeTM.mem_of_last_halted {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} {p q : tm.RunPath input} (hp : (RelSeries.last p).Halted) (hq : RelSeries.head q = RelSeries.head p) (c : Cfg k Symbol State input) : c ∈ q → c ∈ p

Every configuration on a path from the head of a path that ends halted lies on that path: after halting, a deterministic machine stays where it is.

theorem Turing.MultiTapeTM.runsInSpace_of_runPath {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} {s : ℕ} {p : tm.RunPath input} (hhead : RelSeries.head p = tm.initCfg input) (hp : (RelSeries.last p).Halted) (hs : p.space ≤ s) : tm.RunsInSpace input s

A run path from the initial configuration to a halted configuration, using at most s cells, bounds the space of every computation path by s.

Space of runs

theorem Turing.MultiTapeTM.space_eq_sum_spaceUsedByTape {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 = ∑ i : Fin k, spaceUsedByTape cfg t i

The space of a run is the sum of the space used by each tape.

theorem Turing.MultiTapeTM.space_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 : ℕ) => space cfg x

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

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 : space 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.space_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 (-↑σ) ↑σ) : space 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.space_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 : ℕ) : space cfg (a + b) ≤ space cfg a + space (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.space_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) : space cfg t = space 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.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.space_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) : space cfg t = space cfg τ

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

theorem Turing.MultiTapeTM.space_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) : space cfg u ≤ k

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

Space of computation paths

theorem Turing.MultiTapeTM.computationPath_space_eq_space {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} (p : tm.ComputationPath input) : p.space = space (tm.initCfg input) p.time

The space of a computation path is the space of the run of the same length.

theorem Turing.MultiTapeTM.runsInSpace_of_halted {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} {t s : ℕ} (hhalt : (runFrom (tm.initCfg input) t).Halted) (hs : space (tm.initCfg input) t ≤ s) : tm.RunsInSpace input s

A machine that has halted by step t, using at most s cells, uses at most s cells on every computation path.

Run paths to halted configurations as runs

theorem Turing.MultiTapeTM.exists_runPath_iff_runFrom {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} {cfg cfg' : Cfg k Symbol State input} (h : cfg'.Halted) {t s : ℕ} : (∃ (p : tm.RunPath input), RelSeries.head p = cfg ∧ RelSeries.last p = cfg' ∧ p.time ≤ t ∧ p.space ≤ s) ↔ runFrom cfg t = cfg' ∧ space cfg t ≤ s

A run path from cfg to a halted configuration cfg' within t steps and s cells is the run of t steps from cfg, which ends in cfg' and uses at most s cells.

theorem Turing.MultiTapeTM.exists_visitedByTapeHead_eq_Icc {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} (c : Cfg k Symbol State input) (n : ℕ) (i : Fin k) : ∃ (L : ℤ) (R : ℤ), visitedByTapeHead c n i = Finset.Icc L R

The cells visited by a head up to step n form an interval.

theorem Turing.MultiTapeTM.workTapes_runFrom_eq_of_notMem_visitedByTapeHead {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} {c : Cfg k Symbol State input} {n : ℕ} {i : Fin k} {x : ℤ} (hx : x ∉ visitedByTapeHead c n i) : (runFrom c n).workTapes i x = c.workTapes i x

A cell the head of a tape never visits keeps its contents.