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 configurations of the composed path are those of the two paths up to their states.
• Turing.MultiTapeTM.transformsTapes_seq: transformations compose, bounds adding.

noncomputable def 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.

def Turing.MultiTapeTM.Sequential.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) : Cfg k Symbol (State₀ ⊕ State₁) input

A configuration of the first phase: a configuration of tm₀, with a halted state mapped to the initial state of the second phase. Under this map, the whole first phase of seq mirrors the run of tm₀, including its halting step.

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

A configuration of the second phase. Under this map, the second phase of seq mirrors the run of tm₁.

theorem Turing.MultiTapeTM.Sequential.step_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) (h : cfg.state ≠ none) : step (leftCfg tm₁ cfg) = leftCfg tm₁ (step cfg)

theorem Turing.MultiTapeTM.Sequential.step_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) : step (rightCfg cfg) = rightCfg (step cfg)

@[simp]

theorem Turing.MultiTapeTM.Sequential.forgetState_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).forgetState = cfg.forgetState

@[simp]

theorem Turing.MultiTapeTM.Sequential.forgetState_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).forgetState = cfg.forgetState

theorem Turing.MultiTapeTM.Sequential.leftCfg_of_halt {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} (h : cfg.state = none) : leftCfg tm₁ cfg = rightCfg (cfg.withState (some tm₁.q₀))

A halted configuration of the first phase is the start of the second phase.

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₀)) (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 ∧ ∀ c ∈ p, (∃ c₀ ∈ p₀, c.forgetState = c₀.forgetState) ∨ ∃ c₁ ∈ p₁, c.forgetState = c₁.forgetState

Sequential composition of runs. A run path of tm₀ to a halted configuration, followed by a run path of tm₁ to a halted configuration started where tm₀ halted, gives a run path of seq of at most as many steps, whose configurations are those of the two paths up to their states.

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.