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.HaltsAt.runFrom_seq: once tm₀ halts, seq mirrors tm₁.
• Turing.MultiTapeTM.runFrom_seq: runs compose; each machine only has to have halted by the end of its time bound.
• Turing.MultiTapeTM.forgetState_runFrom_seq: invariants of the state-free part of a configuration compose, which bounds the space of the composed run.
• 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.

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

@[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.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.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.