feat(MultiTapeTM): TransformsTapes interface and sequential composition

Cslib.lean

@@ -58,6 +58,8 @@ public import Cslib.Computability.Machines.Turing.MultiTape.Configuration
 public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic
 public import Cslib.Computability.Machines.Turing.MultiTape.DeterministicToNondeterministic
 public import Cslib.Computability.Machines.Turing.MultiTape.Nondeterministic
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Sequential
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.TransformsTapes
 public import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas
 public import Cslib.Computability.Machines.Turing.SingleTape.Defs
 public import Cslib.Computability.Machines.Turing.SingleTape.Deterministic

Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean

@@ -148,6 +148,18 @@ def Cfg.workTapeSymbols (cfg : Cfg k Symbol State input) (i : Fin k) : Option Sy
 /-- A configuration is halted when it has no state to continue from. -/
 abbrev Cfg.Halted (cfg : Cfg k Symbol State input) : Prop := cfg.state = none
 
+/-- The same configuration in a different control state, possibly of a different state type. -/
+@[simps] def Cfg.withState (cfg : Cfg k Symbol State input)
+    {State' : Type*} (q : Option State') : Cfg k Symbol State' input :=
+  ⟨q, cfg.inputPos, cfg.workTapes, cfg.workTapePos, cfg.output⟩
+
+/-- Remap the (optional) state of a configuration through `φ`, leaving the input head, the work
+tapes, the work-tape heads and the output alone. This is the shape of embedding used to place a
+sub-machine's configurations into a larger machine built from it. -/
+@[simps] def Cfg.mapState {State' : Type*} (φ : Option State → Option State')
+    (c : Cfg k Symbol State input) : Cfg k Symbol State' input :=
+  ⟨φ c.state, c.inputPos, c.workTapes, c.workTapePos, c.output⟩
+
 /-- The initial configuration for a starting state and an input string. -/
 @[simp]
 def Cfg.init (q₀ : State) (input : List Symbol) : Cfg k Symbol State input :=

Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean

@@ -191,6 +191,26 @@ lemma runFrom_of_halt (cfg : Cfg k Symbol State input) (h : cfg.state = none) {n
     tm.runFrom cfg n = cfg :=
   Function.iterate_fixed (step_of_halt h) n
 
+/-- Nothing changes after the machine has halted. -/
+lemma runFrom_eq_of_halt
+    (tm : MultiTapeTM k Symbol State)
+    (cfg : Cfg k Symbol State input) {τ t : ℕ} (hle : τ ≤ t)
+    (hhalt : (tm.runFrom cfg τ).state = none) :
+    tm.runFrom cfg t = tm.runFrom cfg τ := by
+  conv_lhs => rw [← Nat.sub_add_cancel hle, Nat.add_comm]
+  rw [runFrom_add, runFrom_of_halt _ hhalt]
+
+/-- Every halted run has a first halting time no later than the supplied one. -/
+lemma exists_minimal_halting_time
+    (tm : MultiTapeTM k Symbol State)
+    (cfg : Cfg k Symbol State input) (t : ℕ)
+    (hhalt : (tm.runFrom cfg t).state = none) :
+    ∃ u ≤ t, (tm.runFrom cfg u).state = none ∧ ∀ s < u, (tm.runFrom cfg s).state ≠ none := by
+  classical
+  have hex : ∃ n, (tm.runFrom cfg n).state = none := ⟨t, hhalt⟩
+  exact ⟨Nat.find hex, Nat.find_min' hex hhalt, Nat.find_spec hex,
+    fun s hs => Nat.find_min hex hs⟩
+
 @[simp]
 lemma outputSymbol_of_halt {cfg : Cfg k Symbol State input} (h_halt : cfg.state = none) :
     tm.outputSymbol cfg = none := by

Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Sequential.lean

@@ -0,0 +1,161 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner and Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner, Samuel Schlesinger
+-/
+
+module
+
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.TransformsTapes
+
+/-!
+# 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.
+-/
+
+@[expose] public section
+
+namespace Turing.MultiTapeTM
+
+variable {k : ℕ} {Symbol State₀ State₁ : Type*} {input : List Symbol}
+
+/-- 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 seq (tm₀ : MultiTapeTM k Symbol State₀) (tm₁ : MultiTapeTM k Symbol State₁) :
+    MultiTapeTM k Symbol (State₀ ⊕ State₁) where
+  q₀ := .inl tm₀.q₀
+  tr q inp work :=
+    match q with
+    | .inl q₀ =>
+      let a := tm₀.tr q₀ inp work
+      { a with state := some (a.state.elim (.inr tm₁.q₀) .inl) }
+    | .inr q₁ =>
+      let a := tm₁.tr q₁ inp work
+      { a with state := a.state.map .inr }
+
+variable {tm₀ : MultiTapeTM k Symbol State₀} {tm₁ : MultiTapeTM k Symbol State₁}
+
+namespace Sequential
+
+/-- 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 leftCfg (tm₁ : MultiTapeTM k Symbol State₁) (cfg : Cfg k Symbol State₀ input) :
+    Cfg k Symbol (State₀ ⊕ State₁) input :=
+  cfg.mapState (fun st => some (st.elim (.inr tm₁.q₀) .inl))
+
+/-- A configuration of the second phase. Under this map, the second phase of `seq` mirrors the
+run of `tm₁`. -/
+def rightCfg (cfg : Cfg k Symbol State₁ input) :
+    Cfg k Symbol (State₀ ⊕ State₁) input :=
+  cfg.mapState (Option.map .inr)
+
+lemma step_leftCfg (cfg : Cfg k Symbol State₀ input) (h : cfg.state ≠ none) :
+    (tm₀.seq tm₁).step (leftCfg tm₁ cfg) = leftCfg tm₁ (tm₀.step cfg) := by
+  obtain ⟨q, hq⟩ := Option.ne_none_iff_exists'.mp h
+  have h1 : (leftCfg tm₁ cfg).state = some (Sum.inl q : State₀ ⊕ State₁) := by
+    simp [leftCfg, Cfg.mapState, hq]
+  simp only [step, h1, hq]
+  rfl
+
+lemma step_rightCfg (cfg : Cfg k Symbol State₁ input) :
+    (tm₀.seq tm₁).step (rightCfg cfg) = rightCfg (tm₁.step cfg) := by
+  cases hq : cfg.state with
+  | none =>
+    have h1 : (rightCfg (State₀ := State₀) cfg).state = none := by simp [rightCfg, Cfg.mapState, hq]
+    simp only [step, h1, hq]
+  | some q =>
+    have h1 : (rightCfg (State₀ := State₀) cfg).state = some (Sum.inr q : State₀ ⊕ State₁) := by
+      simp [rightCfg, hq]
+    simp only [step, h1, hq]
+    rfl
+
+/-- The second phase of `seq` mirrors the run of `tm₁`. -/
+lemma runFrom_rightCfg (cfg : Cfg k Symbol State₁ input) (n : ℕ) :
+    (tm₀.seq tm₁).runFrom (rightCfg cfg) n = rightCfg (tm₁.runFrom cfg n) :=
+  runFrom_comm_of_step rightCfg (fun c => step_rightCfg c) cfg n
+
+/-- While `tm₀` is running, `seq` mirrors it. -/
+lemma runFrom_leftCfg (cfg : Cfg k Symbol State₀ input) (n : ℕ)
+    (h : ∀ m < n, (tm₀.runFrom cfg m).state ≠ none) :
+    (tm₀.seq tm₁).runFrom (leftCfg tm₁ cfg) n = leftCfg tm₁ (tm₀.runFrom cfg n) := by
+  induction n with
+  | zero => rfl
+  | succ n ih =>
+    rw [runFrom_succ_eq_step', runFrom_succ_eq_step', ih fun m hm => h m (by omega),
+      step_leftCfg _ (h n (by omega))]
+
+@[simp]
+lemma workTapePos_leftCfg (cfg : Cfg k Symbol State₀ input) :
+    (leftCfg tm₁ cfg).workTapePos = cfg.workTapePos := rfl
+
+@[simp]
+lemma workTapePos_rightCfg (cfg : Cfg k Symbol State₁ input) :
+    (rightCfg (State₀ := State₀) cfg).workTapePos = cfg.workTapePos := rfl
+
+end Sequential
+
+open Sequential in
+/-- **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. -/
+theorem transformsTapes_seq
+    {P₀ P₁ : (input : List Symbol) → (Fin k → List Symbol) → Prop}
+    {Q₀ Q₁ : (input : List Symbol) → (Fin k → List Symbol) → (Fin k → List Symbol) → Prop}
+    {t₀ s₀ t₁ s₁ : ℕ}
+    (h₀ : TransformsTapes tm₀ P₀ Q₀ t₀ s₀) (h₁ : TransformsTapes tm₁ P₁ Q₁ t₁ s₁)
+    (hmid : ∀ input ws ws', P₀ input ws → Q₀ input ws ws' → P₁ input ws') :
+    TransformsTapes (tm₀.seq tm₁) P₀
+      (fun input ws ws'' => ∃ ws', Q₀ input ws ws' ∧ Q₁ input ws' ws'')
+      (t₀ + t₁) (s₀ + s₁) := by
+  intro input ws out hP₀
+  obtain ⟨τ₀, hτ₀, ws', hrun₀, hQ₀, hspace₀⟩ := h₀ input ws out hP₀
+  obtain ⟨τ₁, hτ₁, ws'', hrun₁, hQ₁, hspace₁⟩ := h₁ input ws' out (hmid input ws ws' hP₀ hQ₀)
+  -- the first halting time of the first machine
+  obtain ⟨u, hu, huhalt, huactive⟩ := exists_minimal_halting_time tm₀
+    (wordsCfg input (some tm₀.q₀) ws out) τ₀ (by simp [hrun₀])
+  have hu_run : tm₀.runFrom (wordsCfg input (some tm₀.q₀) ws out) u =
+      wordsCfg input none ws' out := by
+    rw [← runFrom_eq_of_halt tm₀ _ hu huhalt, hrun₀]
+  -- the first phase mirrors the first machine, ending in the handoff configuration
+  have hleft : ∀ m ≤ u, (tm₀.seq tm₁).runFrom (wordsCfg input (some (tm₀.seq tm₁).q₀) ws out) m
+      = leftCfg tm₁ (tm₀.runFrom (wordsCfg input (some tm₀.q₀) ws out) m) := by
+    intro m hm
+    have : wordsCfg (State := State₀ ⊕ State₁) input (some (tm₀.seq tm₁).q₀) ws out =
+        leftCfg tm₁ (wordsCfg input (some tm₀.q₀) ws out) := rfl
+    rw [this, runFrom_leftCfg _ m fun r hr =>
+      huactive r (by omega)]
+  -- the handoff configuration is the second machine's start, seen through the right embedding
+  have hhandoff : leftCfg tm₁ (tm₀.runFrom (wordsCfg input (some tm₀.q₀) ws out) u) =
+      rightCfg (wordsCfg input (some tm₁.q₀) ws' out) := by
+    rw [hu_run]
+    rfl
+  refine ⟨u + τ₁, by omega, ws'', ?_, ⟨ws', hQ₀, hQ₁⟩, ?_⟩
+  · rw [runFrom_add, hleft u le_rfl, hhandoff, runFrom_rightCfg, hrun₁]
+    rfl
+  · refine le_trans (spaceUsed_add_le _ _ _) (Nat.add_le_add ?_ ?_)
+    · -- the first phase visits what the first machine visits
+      refine le_trans (le_of_eq (spaceUsed_eq_of_workTapePos _ _ u fun m hm => ?_))
+        (le_trans (spaceUsed_mono tm₀ _ hu) hspace₀)
+      rw [hleft m hm, workTapePos_leftCfg]
+    · -- the second phase visits what the second machine visits
+      rw [hleft u le_rfl, hhandoff]
+      refine le_trans (le_of_eq (spaceUsed_eq_of_workTapePos _ _ τ₁ fun m hm => ?_)) hspace₁
+      rw [runFrom_rightCfg, workTapePos_rightCfg]
+
+end Turing.MultiTapeTM

Cslib/Computability/Machines/Turing/MultiTape/Plumbing/TransformsTapes.lean

@@ -0,0 +1,162 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner and Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner, Samuel Schlesinger
+-/
+
+module
+
+public import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas
+
+/-!
+# Machines as transformers of tape words
+
+The interface through which combinators use machines: a machine reads words from its work tapes
+and leaves words on them. A combinator composing such machines talks about words only, never about
+individual cells, head positions or the set of tapes a machine has touched.
+
+Configurations are described by *equalities*: `wordsCfg input q ws out` is the configuration whose
+work tape `i` holds exactly the word `ws i` (contents `tapeOfList (ws i)`, head at the start), with
+the input head at the start of the input and output `out`. A specification
+`TransformsTapes tm P Q t s` says: started on word-holding tapes satisfying `P`, the machine halts
+within `t` steps in the *normal form* `wordsCfg input none ws' out` (every head reset to its
+initial position, tapes blank outside their words, output untouched), with the new words related to
+the old ones by `Q` and using at most `s` work-tape cells. Requiring this normal form is what lets
+specifications compose by rewriting: the halting configuration of one machine is already a valid
+start for the next, so which words survived a step is read off the equation, not re-established cell
+by cell.
+
+## Main definitions
+
+* `Turing.MultiTapeTM.tapeOfList`: the tape holding exactly a given word.
+* `Turing.MultiTapeTM.wordsCfg`: the configuration whose tapes hold given words.
+* `Turing.MultiTapeTM.TransformsTapes`: the specification format described above.
+
+## Main results
+
+* `Turing.MultiTapeTM.TransformsTapes.imp`: strengthen the precondition, weaken the postcondition
+  and raise the bounds.
+* `Turing.MultiTapeTM.exists_transformsTapes_nop`: the machine that does nothing, the first
+  machine of the interface and the check that the format is inhabited as intended.
+-/
+
+@[expose] public section
+
+namespace Turing.MultiTapeTM
+
+variable {k : ℕ} {Symbol State : Type*} {input : List Symbol}
+
+/-- A tape containing exactly the symbols of `xs` at positions `0, ..., xs.length - 1`. -/
+def tapeOfList (xs : List Symbol) : ℤ → Option Symbol
+  | .ofNat n => xs[n]?
+  | .negSucc _ => none
+
+@[simp]
+lemma tapeOfList_ofNat (xs : List Symbol) (n : ℕ) : tapeOfList xs n = xs[n]? := rfl
+
+@[simp]
+lemma tapeOfList_negSucc (xs : List Symbol) (n : ℕ) :
+    tapeOfList xs (.negSucc n) = none := rfl
+
+/-- Appending one symbol writes precisely the cell after the existing word. -/
+lemma tapeOfList_append_single (xs : List Symbol) (x : Symbol) :
+    tapeOfList (xs ++ [x]) = Function.update (tapeOfList xs) (xs.length : ℤ) (some x) := by
+  funext z
+  cases z with
+  | negSucc n => simp [tapeOfList]
+  | ofNat n => grind [tapeOfList]
+
+/-- The blank tape holds the empty word. -/
+@[simp]
+lemma tapeOfList_nil : tapeOfList ([] : List Symbol) = fun _ => none := by
+  funext z
+  cases z <;> simp
+
+/-- The cell at position `0` holds the first symbol of the word. -/
+lemma tapeOfList_zero (xs : List Symbol) : tapeOfList xs 0 = xs.head? := by
+  have h : (0 : ℤ) = ((0 : ℕ) : ℤ) := rfl
+  rw [h, tapeOfList_ofNat]
+  cases xs <;> rfl
+
+/-- The configuration whose work tape `i` holds exactly the word `ws i` with its head at the
+start, whose input head is at the start of the input, in state `q` with output `out`. -/
+@[simps]
+def wordsCfg (input : List Symbol) (q : Option State)
+    (ws : Fin k → List Symbol) (out : List Symbol) : Cfg k Symbol State input :=
+  ⟨q, 1, fun i => tapeOfList (ws i), fun _ => 0, out⟩
+
+/-- Remapping the state of a `wordsCfg` remaps its state and leaves the words alone. -/
+@[simp]
+lemma mapState_wordsCfg {State' : Type*} (φ : Option State → Option State')
+    (input : List Symbol) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) :
+    (wordsCfg input q ws out).mapState φ = wordsCfg input (φ q) ws out := rfl
+
+/-- The initial configuration is the word configuration with blank tapes and no output. -/
+lemma initCfg_eq_wordsCfg (tm : MultiTapeTM k Symbol State) (input : List Symbol) :
+    tm.initCfg input = wordsCfg input (some tm.q₀) (fun _ => []) [] := by
+  refine Cfg.ext rfl rfl ?_ rfl rfl
+  funext i
+  simp [Cfg.init, wordsCfg]
+
+/-- `TransformsTapes tm P Q t s`: started in its initial state on tapes holding words `ws` that
+satisfy the precondition `P`, the machine halts after at most `t` steps in the configuration whose
+tapes hold words `ws'` with `Q input ws ws'`, having used at most `s` work-tape cells.
+
+The bounds are numbers; a specification whose bounds depend on the data is a *family*
+`∀ j, TransformsTapes tm (P j) (Q j) (t j) (s j)` over one fixed machine. -/
+def TransformsTapes (tm : MultiTapeTM k Symbol State)
+    (P : (input : List Symbol) → (Fin k → List Symbol) → Prop)
+    (Q : (input : List Symbol) → (Fin k → List Symbol) → (Fin k → List Symbol) → Prop)
+    (t s : ℕ) : Prop :=
+  ∀ (input : List Symbol) (ws : Fin k → List Symbol) (out : List Symbol), P input ws →
+    ∃ τ ≤ t, ∃ ws',
+      tm.runFrom (wordsCfg input (some tm.q₀) ws out) τ = wordsCfg input none ws' out ∧
+      Q input ws ws' ∧
+      tm.spaceUsed (wordsCfg input (some tm.q₀) ws out) τ ≤ s
+
+/-- A `TransformsTapes` statement can be read with a stronger precondition, a weaker postcondition
+and larger bounds. -/
+theorem TransformsTapes.imp {tm : MultiTapeTM k Symbol State}
+    {P P' : (input : List Symbol) → (Fin k → List Symbol) → Prop}
+    {Q Q' : (input : List Symbol) → (Fin k → List Symbol) → (Fin k → List Symbol) → Prop}
+    {t s t' s' : ℕ} (h : TransformsTapes tm P Q t s)
+    (hP : ∀ input ws, P' input ws → P input ws)
+    (hQ : ∀ input ws ws', P' input ws → Q input ws ws' → Q' input ws ws')
+    (ht : t ≤ t') (hs : s ≤ s') :
+    TransformsTapes tm P' Q' t' s' := by
+  intro input ws out hP'
+  obtain ⟨τ, hτ, ws', hrun, hQ', hspace⟩ := h input ws out (hP input ws hP')
+  exact ⟨τ, hτ.trans ht, ws', hrun, hQ input ws ws' hP' hQ', hspace.trans hs⟩
+
+section Nop
+
+/-- The machine that does nothing: it halts on its first step, leaving the configuration
+unchanged. -/
+private def nop (k : ℕ) (Symbol : Type*) : MultiTapeTM k Symbol Unit where
+  q₀ := ()
+  tr _ _ _ := { inputTape := 0, workTapes := fun _ => (none, 0), output := none, state := none }
+
+private lemma step_nop (ws : Fin k → List Symbol) (out : List Symbol) :
+    (nop k Symbol).step (wordsCfg input (some ()) ws out) = wordsCfg input none ws out := by
+  refine Cfg.ext rfl ?_ ?_ ?_ ?_ <;>
+    simp [step, nop, Action.apply, wordsCfg, SignType.cast]
+
+/-- The machine that does nothing: it halts in one step, leaving every word as it was. Its
+heads never move, so it visits one cell per tape. This is the first machine of the interface: it
+checks that the specification format is inhabited exactly as intended. -/
+theorem exists_transformsTapes_nop (k : ℕ) (Symbol : Type*) :
+    ∃ (State : Type) (_ : Finite State) (tm : MultiTapeTM k Symbol State),
+      TransformsTapes tm (fun _ _ => True) (fun _ ws ws' => ws' = ws) 1 k := by
+  refine ⟨Unit, inferInstance, nop k Symbol, fun input ws out _ => ?_⟩
+  have hrun : (nop k Symbol).runFrom (wordsCfg input (some ()) ws out) 1 =
+      wordsCfg input none ws out := by
+    rw [runFrom_succ_eq_step', runFrom_zero, step_nop]
+  -- the heads never move, so each tape touches only the single cell `0`
+  refine ⟨1, le_rfl, ws, hrun, rfl, spaceUsed_le_of_workTapePos_const _ 1 fun m hm => ?_⟩
+  rcases (by omega : m = 0 ∨ m = 1) with rfl | rfl
+  · rw [runFrom_zero]
+  · rw [hrun]; funext i; simp only [wordsCfg_workTapePos]
+
+end Nop
+
+end Turing.MultiTapeTM