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.forgetState_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₀)) (hp₁ : (RelSeries.last p₁).Halted) : ∃ (p : (tm₀.seq tm₁).RunPath input), RelSeries.head p = Sequential.leftCfg tm₁ (RelSeries.head p₀) ∧ RelSeries.last p = Sequential.rightCfg (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.Sequential.runFrom_rightCfg {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) (n : ℕ) : runFrom (rightCfg cfg) n = rightCfg (runFrom cfg n)

The second phase of seq mirrors the run of tm₁.

theorem Turing.MultiTapeTM.Sequential.runFrom_leftCfg {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) (n : ℕ) (h : ∀ m < n, (runFrom cfg m).state ≠ none) : runFrom (leftCfg tm₁ cfg) n = leftCfg tm₁ (runFrom cfg n)

While tm₀ is running, seq mirrors it.

@[simp]

theorem Turing.MultiTapeTM.Sequential.workTapePos_leftCfg {k : ℕ} {Symbol : Type u_1} {State₀ : Type u_2} {State₁ : Type u_3} {input : List Symbol} {tm₁ : MultiTapeTM k Symbol State₁} (cfg : Cfg k Symbol State₀ input) : (leftCfg tm₁ cfg).workTapePos = cfg.workTapePos

@[simp]

theorem Turing.MultiTapeTM.Sequential.workTapePos_rightCfg {k : ℕ} {Symbol : Type u_1} {State₀ : Type u_2} {State₁ : Type u_3} {input : List Symbol} (cfg : Cfg k Symbol State₁ input) : (rightCfg cfg).workTapePos = cfg.workTapePos

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 (Sequential.leftCfg tm₁ cfg) (u + n) = Sequential.rightCfg (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 (Sequential.leftCfg tm₁ cfg) (t₀ + t₁) = Sequential.rightCfg 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.forgetState_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).forgetState) (hP₁ : ∀ (n : ℕ), P (runFrom (mid.withState (some tm₁.q₀)) n).forgetState) (m : ℕ) : P (runFrom (Sequential.leftCfg tm₁ cfg) m).forgetState

Invariants of a sequential run. If tm₀ has halted in mid by step t₀, then a property of the state-free part of a configuration 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.

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) : space (Sequential.leftCfg tm₁ cfg) (t₀ + t₁) ≤ space cfg t₀ + space (mid.withState (some tm₁.q₀)) t₁

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