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.transformsTapes_seq: transformations compose, bounds adding.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• Turing.MultiTapeTM.Sequential.leftCfg tm₁ cfg = Turing.Cfg.mapState (fun (st : Option State₀) => some (st.elim (Sum.inr tm₁.q₀) Sum.inl)) cfg

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

Equations

• Turing.MultiTapeTM.Sequential.rightCfg cfg = Turing.Cfg.mapState (Option.map Sum.inr) cfg

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)

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.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) → 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), P₀ input ws → Q₀ input ws ws' → P₁ input ws') : (tm₀.seq tm₁).TransformsTapes P₀ (fun (input : List Symbol) (ws ws'' : Fin k → List Symbol) => ∃ (ws' : Fin k → List Symbol), Q₀ input ws ws' ∧ Q₁ input ws' ws'') (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.