Sequential composition of machines on shared tapes

seq tm₀ tm₁ behaves like tm₀ until tm₀ would halt, at which point it continues as tm₁, started in its initial state on the tapes as tm₀ left them. The state space is State₀ ⊕ State₁, and the halting transition of the first phase is mapped to the initial state of the second, so the handoff costs no extra step.

At the specification level this is transformsTapes_seq: transformations compose, with the time and space bounds adding. The postcondition of TransformsTapes is what makes the proof direct: the first machine halts in a full wordsCfg, which is exactly a starting configuration for the second.

Main results

• Turing.MultiTapeTM.seq: the composed machine.
• Turing.MultiTapeTM.exists_runPath_seq: run paths compose, and the composed path visits only cells that the two paths visit.
• Turing.MultiTapeTM.transformsTapes_seq: transformations compose, bounds adding.

@[reducible, inline]

noncomputable abbrev Turing.MultiTapeTM.seq {k : ℕ} {Symbol : Type u_1} {State₀ : Type u_2} {State₁ : Type u_3} (tm₀ : MultiTapeTM k Symbol State₀) (tm₁ : MultiTapeTM k Symbol State₁) : MultiTapeTM k Symbol (State₀ ⊕ State₁)

The sequential composition of tm₀ and tm₁: it behaves like tm₀ until tm₀ would halt, at which point it switches to the initial state of tm₁ and behaves like tm₁. The switch is folded into the halting transition of tm₀, so it costs no step.

Equations

• tm₀.seq tm₁ = tm₀.combine tm₁ (Turing.MultiTapeTM.handOver tm₁.q₀) (Option.map Sum.inr) (Sum.inl tm₀.q₀)

theorem Turing.MultiTapeTM.exists_runPath_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₀ : 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 ∧ ∀ (i : Fin k), p.visitedByTapeHead i ⊆ p₀.visitedByTapeHead i ∪ p₁.visitedByTapeHead i

Sequential composition of runs. A run path of tm₀ to a halted configuration and a run path of tm₁ started where tm₀ halted combine into a run path of seq: the first path up to its first halted configuration, followed by the second. It takes at most as many steps as the two paths together, and visits only cells that they visit.

theorem Turing.MultiTapeTM.transformsTapes_seq {k : ℕ} {Symbol : Type u_1} {State₀ : Type u_2} {State₁ : Type u_3} {tm₀ : MultiTapeTM k Symbol State₀} {tm₁ : MultiTapeTM k Symbol State₁} {P₀ P₁ : List Symbol → (Fin k → List Symbol) → Prop} {Q₀ Q₁ : List Symbol → (Fin k → List Symbol) → (Fin k → List Symbol) → List Symbol → Prop} {t₀ s₀ t₁ s₁ : ℕ} (h₀ : tm₀.TransformsTapes P₀ Q₀ t₀ s₀) (h₁ : tm₁.TransformsTapes P₁ Q₁ t₁ s₁) (hmid : ∀ (input : List Symbol) (ws ws' : Fin k → List Symbol) (e : List Symbol), P₀ input ws → Q₀ input ws ws' e → P₁ input ws') : (tm₀.seq tm₁).TransformsTapes P₀ (fun (input : List Symbol) (ws ws'' : Fin k → List Symbol) (e : List Symbol) => ∃ (ws' : Fin k → List Symbol) (e₀ : List Symbol) (e₁ : List Symbol), Q₀ input ws ws' e₀ ∧ Q₁ input ws' ws'' e₁ ∧ e = e₀ ++ e₁) (t₀ + t₁) (s₀ + s₁)

Sequential composition of transformations. If the postcondition of the first transformation implies the precondition of the second, the composed machine performs the two transformations one after the other, with the time and space bounds adding and the emitted words concatenating.