Raw tape storage equals native visited space

The raw two-stack representation retains every visited blank, but stores no unvisited cell. Its absolute window grows by inserting the new head position. Consequently its size is exactly native visited space, even during arbitrarily long computations that revisit old cells.

Main definitions

• Turing.MultiTapeTM.ToTM2.RawTape.window: the stored interval at an absolute head position.
• Turing.MultiTapeTM.ToTM2.RawTape.nativeAction: the work-tape action, including halted stuttering.
• Turing.MultiTapeTM.ToTM2.RawTape.run: raw work tapes along a native machine run.

Main results

• Turing.MultiTapeTM.ToTM2.RawTape.window_run: stored cells are exactly visited cells.
• Turing.MultiTapeTM.ToTM2.RawTape.span_run_eq_spaceUsedByTape: exact per-tape space.
• Turing.MultiTapeTM.ToTM2.RawTape.sum_span_run_le: a native space bound bounds all raw storage.

def Turing.MultiTapeTM.ToTM2.RawTape.window {Symbol : Type u_1} (t : RawTape Symbol) (pos : ℤ) : Finset ℤ

Absolute positions stored by a raw tape with its head at pos.

@[simp]

theorem Turing.MultiTapeTM.ToTM2.RawTape.card_window {Symbol : Type u_1} (t : RawTape Symbol) (pos : ℤ) : (t.window pos).card = t.span

theorem Turing.MultiTapeTM.ToTM2.RawTape.window_step {Symbol : Type u_1} (t : RawTape Symbol) (a : Option (Option Symbol) × SignType) (pos : ℤ) : (t.step a).window (pos + ↑a.2) = insert (pos + ↑a.2) (t.window pos)

A tape step stores precisely its previous window and its new head position.

noncomputable def Turing.MultiTapeTM.ToTM2.RawTape.nativeAction {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (c : Cfg k Symbol State input) (i : Fin k) : Option (Option Symbol) × SignType

The action on work tape i; a halted machine neither writes nor moves.

theorem Turing.MultiTapeTM.ToTM2.RawTape.nativeAction_pos {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (c : Cfg k Symbol State input) (i : Fin k) : (MultiTapeTM.step c).workTapePos i = c.workTapePos i + ↑(nativeAction tm c i).2

The effective action gives the exact new head position, including after halting.

theorem Turing.MultiTapeTM.ToTM2.RawTape.Represents.nativeStep {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {t : RawTape Symbol} {tm : MultiTapeTM k Symbol State} {c : Cfg k Symbol State input} {i : Fin k} (h : t.Represents (c.workTapes i) (c.workTapePos i)) : (t.step (nativeAction tm c i)).Represents ((MultiTapeTM.step c).workTapes i) ((MultiTapeTM.step c).workTapePos i)

Raw tape semantics follows the native step, also at halted configurations.

noncomputable def Turing.MultiTapeTM.ToTM2.RawTape.run {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) (input : List Symbol) : ℕ → Fin k → RawTape Symbol

Raw work-tape states after n native steps from blank work tapes.

@[simp]

theorem Turing.MultiTapeTM.ToTM2.RawTape.run_zero {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) (input : List Symbol) (i : Fin k) : run tm input 0 i = init

theorem Turing.MultiTapeTM.ToTM2.RawTape.represents_run {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) (input : List Symbol) (n : ℕ) (i : Fin k) : (run tm input n i).Represents ((runFrom (tm.initCfg input) n).workTapes i) ((runFrom (tm.initCfg input) n).workTapePos i)

The raw tape along a native run represents the complete native tape and its head.

theorem Turing.MultiTapeTM.ToTM2.RawTape.visited_succ {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (c : Cfg k Symbol State input) (n : ℕ) (i : Fin k) : (MultiTapeNTM.RunPath.ofDeterministic tm c (n + 1)).visitedByTapeHead i = insert ((runFrom c (n + 1)).workTapePos i) ((MultiTapeNTM.RunPath.ofDeterministic tm c n).visitedByTapeHead i)

Advancing a deterministic run by one step inserts the new head position into the visited set.

theorem Turing.MultiTapeTM.ToTM2.RawTape.window_run {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) (input : List Symbol) (n : ℕ) (i : Fin k) : (run tm input n i).window ((runFrom (tm.initCfg input) n).workTapePos i) = (MultiTapeNTM.RunPath.ofDeterministic tm (tm.initCfg input) n).visitedByTapeHead i

Every stored cell has been visited, and every visited cell remains stored.

theorem Turing.MultiTapeTM.ToTM2.RawTape.span_run_eq_spaceUsedByTape {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) (input : List Symbol) (n : ℕ) (i : Fin k) : (run tm input n i).span = (MultiTapeNTM.RunPath.ofDeterministic tm (tm.initCfg input) n).spaceUsedByTape i

Raw tape storage is exactly the number of native visited cells on that tape.

theorem Turing.MultiTapeTM.ToTM2.RawTape.sum_span_run_eq_space {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) (input : List Symbol) (n : ℕ) : ∑ i : Fin k, (run tm input n i).span = (MultiTapeNTM.RunPath.ofDeterministic tm (tm.initCfg input) n).space

Summed raw storage equals native space, with no runtime term.

theorem Turing.MultiTapeTM.ToTM2.RawTape.sum_span_run_le {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {s : ℕ} (hs : tm.RunsInSpace input s) (n : ℕ) : ∑ i : Fin k, (run tm input n i).span ≤ s

A native space certificate bounds raw storage at every time, including after halting.

theorem Turing.MultiTapeTM.ToTM2.RawTape.span_run_le {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {s : ℕ} (hs : tm.RunsInSpace input s) (n : ℕ) (i : Fin k) : (run tm input n i).span ≤ s

Each individual raw tape also fits the native total space bound.