TM0 Sequential Composition

This file defines sequential composition of TM0 machines and proves that the composed machine halts iff M₁ halts and M₂ halts on M₁'s output tape.

Main definitions

• TM0Seq.compose — compose two TM0 machines sequentially
• TM0Seq.evalCfg — evaluate a TM0 returning the full config
• TM0Seq.compose_phase2_respects — phase 2 bisimulation
• TM0Seq.compose_dom_iff — full correctness theorem

Architecture

The composed machine compose M₁ M₂ uses states Λ₁ ⊕ Λ₂:

• In Sum.inl q₁ states: runs M₁. When M₁ halts, immediately tries M₂'s first step.
• In Sum.inr q₂ states: runs M₂.

The key correctness theorem says: if M₁ always halts on input l and produces output tape Tape.mk₁ l', then the composed machine halts on l iff M₂ halts on l'.

def TM0Seq.evalCfg {Γ : Type} [Inhabited Γ] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (l : List Γ) : Part (Turing.TM0.Cfg Γ Λ)

Evaluate a TM0 machine and return the full output configuration (state + tape), rather than just the tape as TM0.eval does.

Equations

• TM0Seq.evalCfg M l = Turing.eval (Turing.TM0.step M) (Turing.TM0.init l)

theorem TM0Seq.evalCfg_dom_iff {Γ : Type} [Inhabited Γ] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (l : List Γ) : (evalCfg M l).Dom ↔ (Turing.TM0.eval M l).Dom

evalCfg has the same Dom as TM0.eval.

def TM0Seq.evalFromCfg {Γ : Type} [Inhabited Γ] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (cfg : Turing.TM0.Cfg Γ Λ) : Part (Turing.TM0.Cfg Γ Λ)

Evaluate a TM0 from an arbitrary configuration.

Equations

• TM0Seq.evalFromCfg M cfg = Turing.eval (Turing.TM0.step M) cfg

theorem TM0Seq.evalFromCfg_init {Γ : Type} [Inhabited Γ] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (l : List Γ) : evalFromCfg M (Turing.TM0.init l) = evalCfg M l

evalFromCfg from the initial config equals evalCfg.

noncomputable def TM0Seq.compose {Γ Λ₁ : Type} [Inhabited Λ₁] {Λ₂ : Type} [Inhabited Λ₂] (M₁ : Turing.TM0.Machine Γ Λ₁) (M₂ : Turing.TM0.Machine Γ Λ₂) : Turing.TM0.Machine Γ (Λ₁ ⊕ Λ₂)

Sequential composition of TM0 machines. When M₁ halts (returns none), we immediately invoke M₂ from its default state on the current tape symbol.

Equations

• One or more equations did not get rendered due to their size.
• TM0Seq.compose M₁ M₂ (Sum.inr q₂) a = match M₂ q₂ a with | some (q₂', s) => some (Sum.inr q₂', s) | none => none

theorem TM0Seq.compose_step_inl {Γ : Type} [Inhabited Γ] {Λ₁ : Type} [Inhabited Λ₁] {Λ₂ : Type} [Inhabited Λ₂] (M₁ : Turing.TM0.Machine Γ Λ₁) (M₂ : Turing.TM0.Machine Γ Λ₂) (c₁ c₁' : Turing.TM0.Cfg Γ Λ₁) (h : Turing.TM0.step M₁ c₁ = some c₁') : Turing.TM0.step (compose M₁ M₂) { q := Sum.inl c₁.q, Tape := c₁.Tape } = some { q := Sum.inl c₁'.q, Tape := c₁'.Tape }

theorem TM0Seq.compose_phase1_reaches {Γ : Type} [Inhabited Γ] {Λ₁ : Type} [Inhabited Λ₁] {Λ₂ : Type} [Inhabited Λ₂] (M₁ : Turing.TM0.Machine Γ Λ₁) (M₂ : Turing.TM0.Machine Γ Λ₂) (c₁ : Turing.TM0.Cfg Γ Λ₁) (l : List Γ) (h : Turing.Reaches (Turing.TM0.step M₁) (Turing.TM0.init l) c₁) : Turing.Reaches (Turing.TM0.step (compose M₁ M₂)) (Turing.TM0.init l) { q := Sum.inl c₁.q, Tape := c₁.Tape }

theorem TM0Seq.compose_step_on_halt {Γ : Type} [Inhabited Γ] {Λ₁ : Type} [Inhabited Λ₁] {Λ₂ : Type} [Inhabited Λ₂] (M₁ : Turing.TM0.Machine Γ Λ₁) (M₂ : Turing.TM0.Machine Γ Λ₂) (q₁ : Λ₁) (T : Turing.Tape Γ) (h : Turing.TM0.step M₁ { q := q₁, Tape := T } = none) : Turing.TM0.step (compose M₁ M₂) { q := Sum.inl q₁, Tape := T } = Option.map (fun (c₂ : Turing.TM0.Cfg Γ Λ₂) => { q := Sum.inr c₂.q, Tape := c₂.Tape }) (Turing.TM0.step M₂ { q := default, Tape := T })

theorem TM0Seq.compose_phase2_respects {Γ : Type} [Inhabited Γ] {Λ₁ : Type} [Inhabited Λ₁] {Λ₂ : Type} [Inhabited Λ₂] (M₁ : Turing.TM0.Machine Γ Λ₁) (M₂ : Turing.TM0.Machine Γ Λ₂) : Turing.Respects (Turing.TM0.step M₂) (Turing.TM0.step (compose M₁ M₂)) fun (c₂ : Turing.TM0.Cfg Γ Λ₂) (c : Turing.TM0.Cfg Γ (Λ₁ ⊕ Λ₂)) => c.q = Sum.inr c₂.q ∧ c.Tape = c₂.Tape

theorem TM0Seq.compose_phase2_dom {Γ : Type} [Inhabited Γ] {Λ₁ : Type} [Inhabited Λ₁] {Λ₂ : Type} [Inhabited Λ₂] (M₁ : Turing.TM0.Machine Γ Λ₁) (M₂ : Turing.TM0.Machine Γ Λ₂) (T : Turing.Tape Γ) : (evalFromCfg M₂ { q := default, Tape := T }).Dom ↔ (Turing.eval (Turing.TM0.step (compose M₁ M₂)) { q := Sum.inr default, Tape := T }).Dom

Phase 2 preserves Dom: evalFromCfg of M₂ from ⟨default, T⟩ halts iff the composed machine from ⟨Sum.inr default, T⟩ halts.

theorem TM0Seq.compose_eval_split {Γ : Type} [Inhabited Γ] {Λ₁ : Type} [Inhabited Λ₁] {Λ₂ : Type} [Inhabited Λ₂] (M₁ : Turing.TM0.Machine Γ Λ₁) (M₂ : Turing.TM0.Machine Γ Λ₂) (l : List Γ) (h₁ : (evalCfg M₁ l).Dom) : have c₁ := (evalCfg M₁ l).get h₁; Turing.eval (Turing.TM0.step (compose M₁ M₂)) (Turing.TM0.init l) = Turing.eval (Turing.TM0.step (compose M₁ M₂)) { q := Sum.inl c₁.q, Tape := c₁.Tape }

theorem TM0Seq.compose_eval_at_halt {Γ : Type} [Inhabited Γ] {Λ₁ : Type} [Inhabited Λ₁] {Λ₂ : Type} [Inhabited Λ₂] (M₁ : Turing.TM0.Machine Γ Λ₁) (M₂ : Turing.TM0.Machine Γ Λ₂) (q₁ : Λ₁) (T : Turing.Tape Γ) (h : Turing.TM0.step M₁ { q := q₁, Tape := T } = none) : (Turing.eval (Turing.TM0.step (compose M₁ M₂)) { q := Sum.inl q₁, Tape := T }).Dom ↔ (evalFromCfg M₂ { q := default, Tape := T }).Dom

theorem TM0Seq.compose_dom_of_parts {Γ : Type} [Inhabited Γ] {Λ₁ : Type} [Inhabited Λ₁] {Λ₂ : Type} [Inhabited Λ₂] (M₁ : Turing.TM0.Machine Γ Λ₁) (M₂ : Turing.TM0.Machine Γ Λ₂) (l : List Γ) (h₁ : (evalCfg M₁ l).Dom) (h₂ : (evalFromCfg M₂ { q := default, Tape := ((evalCfg M₁ l).get h₁).Tape }).Dom) : (Turing.TM0.eval (compose M₁ M₂) l).Dom

theorem TM0Seq.compose_dom_left {Γ : Type} [Inhabited Γ] {Λ₁ : Type} [Inhabited Λ₁] {Λ₂ : Type} [Inhabited Λ₂] (M₁ : Turing.TM0.Machine Γ Λ₁) (M₂ : Turing.TM0.Machine Γ Λ₂) (l : List Γ) (h : (Turing.TM0.eval (compose M₁ M₂) l).Dom) : (evalCfg M₁ l).Dom

theorem TM0Seq.compose_dom_right {Γ : Type} [Inhabited Γ] {Λ₁ : Type} [Inhabited Λ₁] {Λ₂ : Type} [Inhabited Λ₂] (M₁ : Turing.TM0.Machine Γ Λ₁) (M₂ : Turing.TM0.Machine Γ Λ₂) (l : List Γ) (h₁ : (evalCfg M₁ l).Dom) (h : (Turing.TM0.eval (compose M₁ M₂) l).Dom) : (evalFromCfg M₂ { q := default, Tape := ((evalCfg M₁ l).get h₁).Tape }).Dom

theorem TM0Seq.compose_dom_iff {Γ : Type} [Inhabited Γ] {Λ₁ : Type} [Inhabited Λ₁] {Λ₂ : Type} [Inhabited Λ₂] (M₁ : Turing.TM0.Machine Γ Λ₁) (M₂ : Turing.TM0.Machine Γ Λ₂) (l : List Γ) (h₁ : (evalCfg M₁ l).Dom) : (Turing.TM0.eval (compose M₁ M₂) l).Dom ↔ (evalFromCfg M₂ { q := default, Tape := ((evalCfg M₁ l).get h₁).Tape }).Dom

Correctness of sequential composition.

If M₁ halts on input l, then the composed machine halts on l iff M₂ halts on M₁'s output tape.

theorem TM0Seq.compose_dom_iff' {Γ : Type} [Inhabited Γ] {Λ₁ : Type} [Inhabited Λ₁] {Λ₂ : Type} [Inhabited Λ₂] (M₁ : Turing.TM0.Machine Γ Λ₁) (M₂ : Turing.TM0.Machine Γ Λ₂) (l l' : List Γ) (h₁ : (evalCfg M₁ l).Dom) (h_tape : ((evalCfg M₁ l).get h₁).Tape = Turing.Tape.mk₁ l') : (Turing.TM0.eval (compose M₁ M₂) l).Dom ↔ (Turing.TM0.eval M₂ l').Dom

Compose Output Tape Tracking

theorem TM0Seq.evalCfg_step_none {Γ : Type} [Inhabited Γ] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (l : List Γ) (h : (evalCfg M l).Dom) : Turing.TM0.step M ((evalCfg M l).get h) = none

theorem TM0Seq.compose_eval_from_halt_tape {Γ : Type} [Inhabited Γ] {Λ₁ : Type} [Inhabited Λ₁] {Λ₂ : Type} [Inhabited Λ₂] (M₁ : Turing.TM0.Machine Γ Λ₁) (M₂ : Turing.TM0.Machine Γ Λ₂) (q₁ : Λ₁) (T : Turing.Tape Γ) (h_halt : Turing.TM0.step M₁ { q := q₁, Tape := T } = none) (h₂ : (evalFromCfg M₂ { q := default, Tape := T }).Dom) : ∃ c ∈ Turing.eval (Turing.TM0.step (compose M₁ M₂)) { q := Sum.inl q₁, Tape := T }, c.Tape = ((evalFromCfg M₂ { q := default, Tape := T }).get h₂).Tape

theorem TM0Seq.compose_eval_tape_mem {Γ : Type} [Inhabited Γ] {Λ₁ : Type} [Inhabited Λ₁] {Λ₂ : Type} [Inhabited Λ₂] (M₁ : Turing.TM0.Machine Γ Λ₁) (M₂ : Turing.TM0.Machine Γ Λ₂) (l l' : List Γ) (h₁ : (evalCfg M₁ l).Dom) (h₁_tape : ((evalCfg M₁ l).get h₁).Tape = Turing.Tape.mk₁ l') (h₂ : (evalCfg M₂ l').Dom) : ∃ c ∈ Turing.eval (Turing.TM0.step (compose M₁ M₂)) (Turing.TM0.init l), c.Tape = ((evalCfg M₂ l').get h₂).Tape

theorem TM0Seq.compose_evalCfg_tape {Γ : Type} [Inhabited Γ] {Λ₁ : Type} [Inhabited Λ₁] {Λ₂ : Type} [Inhabited Λ₂] (M₁ : Turing.TM0.Machine Γ Λ₁) (M₂ : Turing.TM0.Machine Γ Λ₂) (l l' : List Γ) (h₁ : (evalCfg M₁ l).Dom) (h₁_tape : ((evalCfg M₁ l).get h₁).Tape = Turing.Tape.mk₁ l') (h₂ : (evalCfg M₂ l').Dom) (h_comp : (evalCfg (compose M₁ M₂) l).Dom) : ((evalCfg (compose M₁ M₂) l).get h_comp).Tape = ((evalCfg M₂ l').get h₂).Tape