The simulation in the space of the simulated machine

A zipper holds a cell only at a position its head has visited, and the visited positions of a head that moves by at most one cell per step form an interval around 0. So the configuration of the simulation after j steps takes space linear in the number of visited cells, times the size of a symbol, plus the length of the input head in binary (Turing.MultiTapeTM.Universal.length_eCfg_le_space). For the description of a machine, the visited cells are those of the machine (Turing.MultiTapeTM.Universal.simSpace_desc).

Main definitions

• Turing.MultiTapeTM.Universal.simSpace: the number of cells visited by the simulation.
• Turing.MultiTapeTM.Universal.Tape.Covered: the cells of a zipper are at given positions.
• Turing.MultiTapeTM.Universal.cfgSpaceBound: the bound on the size of a configuration.

Main results

• Turing.MultiTapeTM.Universal.length_eCfg_le_of_covered: the size of a configuration whose zippers are covered by sets of positions, in their total size.
• Turing.MultiTapeTM.Universal.length_eCfg_le_space: the size of the configuration, in the visited cells.
• Turing.MultiTapeTM.Universal.simSpace_desc: for descriptions of machines, the visited cells are the space of the machine.

Zippers within the visited positions

structure Turing.MultiTapeTM.Universal.Tape.Covered (t : Tape) (V : Set ℤ) : Prop

The cells of the zipper t are at positions in V.

• left (k : ℕ) : k < t.left.length → t.head - 1 - ↑k ∈ V
• right (k : ℕ) : k < t.right.length → t.head + ↑k ∈ V

theorem Turing.MultiTapeTM.Universal.Tape.Covered.mono {t : Tape} {V W : Set ℤ} (h : t.Covered V) (hVW : V ⊆ W) : t.Covered W

theorem Turing.MultiTapeTM.Universal.Tape.Covered.apply {t : Tape} {V : Set ℤ} (h : t.Covered V) (hh : t.head ∈ V) (a : Option (Option ℕ) × SignType) (ha : (t.apply a).head ∈ V) : (t.apply a).Covered V

An action keeps a zipper covered, if the heads before and after are covered.

A step on a single work tape

theorem Turing.MultiTapeTM.Universal.Act.apply_tape (a : Act) (x : List ℕ) (c : SCfg) (i : ℕ) : ∃ (ta : Option (Option ℕ) × SignType), (a.apply x c).workTapes.getD i Tape.blank = (c.workTapes.getD i Tape.blank).apply ta

An action applies a tape action to every work tape.

Visited positions

def Turing.MultiTapeTM.Universal.run (d : Desc) (x : List ℕ) (j : ℕ) : SCfg

The configuration of the simulation after j steps.

def Turing.MultiTapeTM.Universal.headAt (d : Desc) (x : List ℕ) (j i : ℕ) : ℤ

The head of work tape i after j steps.

def Turing.MultiTapeTM.Universal.visited (d : Desc) (x : List ℕ) (j i : ℕ) : Finset ℤ

The positions visited by the head of work tape i up to step j.

def Turing.MultiTapeTM.Universal.simSpace (d : Desc) (x : List ℕ) (j : ℕ) : ℕ

The number of work-tape cells visited by the simulation up to step j.

theorem Turing.MultiTapeTM.Universal.run_succ (d : Desc) (x : List ℕ) (j : ℕ) : run d x (j + 1) = (step d x (run d x j)).1

One more step of the simulation.

The size of the configuration

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.cfgSpaceBound (D X k S : ℕ) : ℕ

The bound on the size of a configuration for a description of length D, an input of length X, k work tapes and S cells.

theorem Turing.MultiTapeTM.Universal.length_eCfg_le_of_covered {D X j k S : ℕ} {c : SCfg} (hinv : Inv D X j c) (hk : c.workTapes.length = k) {V : ℕ → Finset ℤ} (hc : ∀ i < k, (c.workTapes.getD i Tape.blank).Covered ↑(V i)) (hh : ∀ i < k, (c.workTapes.getD i Tape.blank).head.natAbs < (V i).card) (hS : ∑ i ∈ Finset.range k, (V i).card ≤ S) : (eCfg c).length ≤ cfgSpaceBound D X k S

The size of a configuration whose zippers are covered by sets of positions that hold their heads: linear in the total size of the sets and the number of work tapes, times the size of a symbol, plus the length of the position of the input head in binary.

theorem Turing.MultiTapeTM.Universal.length_eCfg_le_space (d : Desc) (x : List ℕ) (j : ℕ) : (eCfg (run d x j)).length ≤ 2 * descLen d + 3 + 2 * (encNat (x.length + 1)).length + 1 + 3 * (2 * descLen d + 5) * 2 * simSpace d x j + d.tapes

The size of the configuration after j steps, in the number of visited cells: linear in the visited cells and the number of work tapes, times the size of a symbol, plus the length of the position of the input head in binary.

Descriptions of machines

theorem Turing.MultiTapeTM.Universal.simSpace_desc {k : ℕ} {Symbol State : Type} [Fintype State] [Fintype Symbol] (eS : State ↪ ℕ) (eY : Symbol ↪ ℕ) (tm : MultiTapeTM k Symbol State) (x : List Symbol) (j : ℕ) : simSpace (desc eS eY tm) (List.map (⇑eY) x) j = (MultiTapeNTM.RunPath.ofDeterministic tm (tm.initCfg x) j).space

The space of the simulation of the description of a machine is the space of the machine.