Space of a sequential run

The additions of Christian Reitwiessner's branch crei/tidy-universal and of cslib PR #1111 to Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Sequential: sequential runs read through Turing.MultiTapeTM.runFrom, with their space, and sequential composition of transformations given by equations.

Main results

• Turing.MultiTapeTM.runFrom_seq: runs compose.
• Turing.MultiTapeTM.withState_runFrom_seq: invariants of a sequential run.
• Turing.MultiTapeTM.space_seq_le: the space of a sequential run is at most that of its phases.
• Turing.MultiTapeTM.TransformsTapes.seq_eq: sequential composition of transformations given by equations.
• Turing.MultiTapeTM.exists_runPath_seq_space_le: the composed path visits at most the cells of the two paths combined.

theorem Turing.MultiTapeTM.exists_runPath_seq_space_le {k : ℕ} {Symbol : Type u_1} {State₀ : Type u_2} {State₁ : Type u_3} {input : List Symbol} {tm₀ : MultiTapeTM k Symbol State₀} {tm₁ : MultiTapeTM k Symbol State₁} {p₀ : tm₀.RunPath input} (h₀ : (RelSeries.last p₀).Halted) {p₁ : tm₁.RunPath input} (h₁ : RelSeries.head p₁ = (RelSeries.last p₀).withState (some tm₁.q₀)) : ∃ (p : (tm₀.seq tm₁).RunPath input), RelSeries.head p = Cfg.mapState (handOver tm₁.q₀) (RelSeries.head p₀) ∧ RelSeries.last p = Cfg.mapState (Option.map Sum.inr) (RelSeries.last p₁) ∧ p.length ≤ p₀.length + p₁.length ∧ p.space ≤ p₀.space + p₁.space

Space of a sequential run. The run path of seq composed from two run paths visits at most the cells of the two paths combined.

theorem Turing.MultiTapeTM.HaltsAt.runFrom_seq {k : ℕ} {Symbol : Type u_1} {State₀ : Type u_2} {State₁ : Type u_3} {input : List Symbol} {tm₀ : MultiTapeTM k Symbol State₀} {tm₁ : MultiTapeTM k Symbol State₁} {cfg : Cfg k Symbol State₀ input} {u : ℕ} (h : tm₀.HaltsAt cfg u) (n : ℕ) : runFrom (Cfg.mapState (handOver tm₁.q₀) cfg) (u + n) = Cfg.mapState (Option.map Sum.inr) (runFrom ((runFrom cfg u).withState (some tm₁.q₀)) n)

If tm₀ halts at step u, then from step u on seq mirrors tm₁, started where tm₀ halted.

theorem Turing.MultiTapeTM.runFrom_seq {k : ℕ} {Symbol : Type u_1} {State₀ : Type u_2} {State₁ : Type u_3} {input : List Symbol} {tm₀ : MultiTapeTM k Symbol State₀} {tm₁ : MultiTapeTM k Symbol State₁} {cfg mid : Cfg k Symbol State₀ input} {fin : Cfg k Symbol State₁ input} {t₀ t₁ : ℕ} (h₀ : runFrom cfg t₀ = mid) (hmid : mid.Halted) (h₁ : runFrom (mid.withState (some tm₁.q₀)) t₁ = fin) (hfin : fin.Halted) : runFrom (Cfg.mapState (handOver tm₁.q₀) cfg) (t₀ + t₁) = Cfg.mapState (Option.map Sum.inr) fin

Sequential composition of runs. If tm₀ has halted in mid by step t₀, and tm₁, started where tm₀ halted, has halted in fin by step t₁, then the composed machine has halted in fin by step t₀ + t₁. Each machine may halt earlier than its bound; in particular tm₀ need not be running at every step before t₀.

theorem Turing.MultiTapeTM.withState_runFrom_seq {k : ℕ} {Symbol : Type u_1} {State₀ : Type u_2} {State₁ : Type u_3} {input : List Symbol} {tm₀ : MultiTapeTM k Symbol State₀} {tm₁ : MultiTapeTM k Symbol State₁} {P : Cfg k Symbol Unit input → Prop} {cfg mid : Cfg k Symbol State₀ input} {t₀ : ℕ} (h₀ : runFrom cfg t₀ = mid) (hmid : mid.Halted) (hP₀ : ∀ m < t₀, P ((runFrom cfg m).withState (some ()))) (hP₁ : ∀ (n : ℕ), P ((runFrom (mid.withState (some tm₁.q₀)) n).withState (some ()))) (m : ℕ) : P ((runFrom (Cfg.mapState (handOver tm₁.q₀) cfg) m).withState (some ()))

Invariants of a sequential run. If tm₀ has halted in mid by step t₀, then a property of a configuration apart from its control state holds throughout the run of the composed machine if it holds before step t₀ of the run of tm₀ and throughout the run of tm₁ started where tm₀ halted. The property is stated on the configurations in the state some (), which keeps the input head, the work tapes, the work-tape heads and the output.

theorem Turing.MultiTapeTM.space_seq_le {k : ℕ} {Symbol : Type u_1} {State₀ : Type u_2} {State₁ : Type u_3} {input : List Symbol} {tm₀ : MultiTapeTM k Symbol State₀} {tm₁ : MultiTapeTM k Symbol State₁} {cfg mid : Cfg k Symbol State₀ input} {t₀ t₁ : ℕ} (h₀ : runFrom cfg t₀ = mid) (hmid : mid.Halted) (h₁ : (runFrom (mid.withState (some tm₁.q₀)) t₁).Halted) : (MultiTapeNTM.RunPath.ofDeterministic (tm₀.seq tm₁) (Cfg.mapState (handOver tm₁.q₀) cfg) (t₀ + t₁)).space ≤ (MultiTapeNTM.RunPath.ofDeterministic tm₀ cfg t₀).space + (MultiTapeNTM.RunPath.ofDeterministic tm₁ (mid.withState (some tm₁.q₀)) t₁).space

If tm₀ has halted in mid after t₀ steps and tm₁, started from mid, has halted after t₁ steps, then in t₀ + t₁ steps tm₀.seq tm₁ uses at most the space of the two runs combined.

theorem Turing.MultiTapeTM.TransformsTapes.seq_eq {k : ℕ} {Symbol : Type u_1} {State₀ : Type u_2} {State₁ : Type u_3} {tm₀ : MultiTapeTM k Symbol State₀} {tm₁ : MultiTapeTM k Symbol State₁} {P : List Symbol → (Fin k → List Symbol) → Prop} {ws₁ ws₂ : Fin k → List Symbol} {e₀ e₁ : List Symbol} {t₀ s₀ t₁ s₁ : ℕ} (h₀ : tm₀.TransformsTapes P (fun (x : List Symbol) (x_1 ws' : Fin k → List Symbol) (e : List Symbol) => ws' = ws₁ ∧ e = e₀) t₀ s₀) (h₁ : tm₁.TransformsTapes (fun (x : List Symbol) (ws : Fin k → List Symbol) => ws = ws₁) (fun (x : List Symbol) (x_1 ws' : Fin k → List Symbol) (e : List Symbol) => ws' = ws₂ ∧ e = e₁) t₁ s₁) : (tm₀.seq tm₁).TransformsTapes P (fun (x : List Symbol) (x_1 ws' : Fin k → List Symbol) (e : List Symbol) => ws' = ws₂ ∧ e = e₀ ++ e₁) (t₀ + t₁) (s₀ + s₁)

Sequential composition of transformations given by equations. If the first machine leaves the words ws₁ and emits e₀, and the second takes ws₁ to ws₂ emitting e₁, the composed machine leaves ws₂ and emits e₀ ++ e₁.