feat(MultiTapeTM): concatenate the outputs of two machines

Cslib.lean

@@ -46,9 +46,11 @@ public import Cslib.Computability.Languages.OmegaLanguage
 public import Cslib.Computability.Languages.OmegaRegularLanguage
 public import Cslib.Computability.Languages.RegularLanguage
 public import Cslib.Computability.Languages.SafetyLiveness
+public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Concat
 public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic
 public import Cslib.Computability.Machines.Turing.MultiTape.NormalForms.RewindInput
 public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Basic
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Concat
 public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.ExtendTapes
 public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.InputFromWorkTape
 public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.InputFromWorkTape.Defs

Cslib/Computability/Machines/Turing/MultiTape/Combinators/Concat.lean

@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Mathlib.Basic.Finite.Sum
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Concat
+
+/-!
+# Complexity of a concatenation of two functions
+
+If `f` and `g` are computable, then so is any function whose encoded result is the encoded result
+of `f` followed by the encoded result of `g`. The bounds are the sums of the two bounds, plus one
+input rewind in time and a constant in space.
+
+The result is stated for an arbitrary function `h` together with the assumption that its encoding
+is the concatenation of the two encodings, rather than for a fixed pairing. That way it covers
+whatever the caller happens to be encoding — a pair, a list, a tagged union — and the caller is
+the one who has to know that the concatenation of the two encodings is again injective. The pair
+is the typical case and is spelled out in `computableInTimeAndSpace_pair`.
+
+Note that nothing has to be assumed about how the two encodings compose beyond `henc`: the machine
+never inspects the concatenation. It writes the first encoded result to the output tape, and then
+writes the second one after it, so the concatenation is produced simply by not resetting the output
+tape in between.
+
+## Main results
+
+* `Turing.MultiTapeTM.computableInTimeAndSpace_concat`: the complexity of a concatenation.
+* `Turing.MultiTapeTM.computableInTimeAndSpace_pair`: the special case of a pair.
+-/
+
+@[expose] public section
+
+namespace Turing.MultiTapeTM
+
+variable {α β γ δ : Type*}
+
+/-- **Complexity of a concatenation.** If `f` and `g` are computable and the encoded result of `h`
+is the encoded result of `f` followed by the encoded result of `g`, then `h` is computable in the
+sum of the two times plus the length of the input, and in the sum of the two spaces plus a
+constant.
+
+The machine runs the machine for `f`, rewinds the input head, and runs the machine for `g` on fresh
+work tapes; the length of the input in the time bound is the cost of that rewind. The intermediate
+results are never stored: both machines write straight to the output tape, which is append-only, so
+their outputs end up concatenated. The constant in the space bound is the number of work tapes of
+the two machines, each of which contributes the one cell its head is parked on while the other
+machine runs; the rewind itself costs no space. -/
+theorem computableInTimeAndSpace_concat
+    {f : α → β} {g : α → γ} {h : α → δ}
+    {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {encD : δ ↪ List Bool}
+    {tf sf tg sg : α → ℕ}
+    (henc : ∀ x, encD (h x) = encB (f x) ++ encC (g x))
+    (hf : ComputableInTimeAndSpace f encIn encB tf sf)
+    (hg : ComputableInTimeAndSpace g encIn encC tg sg) :
+    ∃ c, ComputableInTimeAndSpace h encIn encD
+      (fun x => tf x + tg x + (encIn x).length + 2)
+      (fun x => sf x + sg x + c) := by
+  obtain ⟨k₀, State₀, hfinite₀, tm₀, htm₀⟩ := hf
+  obtain ⟨k₁, State₁, hfinite₁, tm₁, htm₁⟩ := hg
+  refine ⟨k₀ + k₁, k₀ + k₁, (State₀ ⊕ RewindState) ⊕ State₁, inferInstance,
+    concat tm₀ tm₁, fun x => ?_⟩
+  obtain ⟨t₀, ht₀, s₀, hs₀, hcomp₀⟩ := htm₀ x
+  obtain ⟨t₁, ht₁, s₁, hs₁, hcomp₁⟩ := htm₁ x
+  obtain ⟨t, htle, s, hsle, hcomp⟩ := computesInTimeAndSpace_concat tm₀ tm₁ hcomp₀ hcomp₁
+  have htbound : t ≤ tf x + tg x + (encIn x).length + 2 := by omega
+  have hsbound : s ≤ sf x + sg x + (k₀ + k₁) := by omega
+  exact ⟨t, htbound, s, hsbound, henc x ▸ hcomp⟩
+
+/-- **Complexity of computing a pair.** The special case of `computableInTimeAndSpace_concat` in
+which the two results are packed into a pair, encoded by concatenating the two encodings. It is up
+to the caller to provide such an encoding; this needs the encoding of the first component to
+determine where it ends, as a prefix-free or length-prefixed encoding does. -/
+theorem computableInTimeAndSpace_pair
+    {f : α → β} {g : α → γ}
+    {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool}
+    {encPair : β × γ ↪ List Bool} {tf sf tg sg : α → ℕ}
+    (henc : ∀ p : β × γ, encPair p = encB p.1 ++ encC p.2)
+    (hf : ComputableInTimeAndSpace f encIn encB tf sf)
+    (hg : ComputableInTimeAndSpace g encIn encC tg sg) :
+    ∃ c, ComputableInTimeAndSpace (fun x => (f x, g x)) encIn encPair
+      (fun x => tf x + tg x + (encIn x).length + 2)
+      (fun x => sf x + sg x + c) :=
+  computableInTimeAndSpace_concat (fun x => henc (f x, g x)) hf hg
+
+end Turing.MultiTapeTM

Cslib/Computability/Machines/Turing/MultiTape/Combinators/README.md

@@ -0,0 +1,11 @@
+# Function combinators
+
+These modules state the complexity of a function built from other functions. They are the reusable
+interface: a caller combines `ComputableInTimeAndSpace` facts without ever mentioning tapes, head
+positions or configurations. The machines behind them come from [Plumbing](../Plumbing) and
+[NormalForms](../NormalForms).
+
+- `Concat` computes a function whose encoded result is the concatenation of the encoded results of
+  two functions, of which the pair is the typical case. The two machines write straight to the
+  append-only output tape, so no intermediate result is ever stored; the cost over the two machines
+  is one rewind of the input tape in time, and one idle cell per work tape in space.

Cslib/Computability/Machines/Turing/MultiTape/NormalForms/README.md

@@ -7,3 +7,8 @@ The transformation adds at most the input length plus two steps, including on em
 
 The `HaltsWithInputAtStart` predicate states the property at every halting time, so padded runs
 also satisfy it. The construction does not require the original machine to be total.
+
+`rewindInput_halts_spaceUsed` bundles the normal form with its cost, so a combinator that needs to
+feed one input to two machines never has to unfold the rewind. Only the time bound grows: the
+rewind moves no work-tape head, so it visits no cell that was not visited already, and the space
+bound is preserved exactly.

Cslib/Computability/Machines/Turing/MultiTape/NormalForms/RewindInput.lean

@@ -27,6 +27,10 @@ variable {k : ℕ} {Symbol State : Type*} {input : List Symbol}
 def rewindInput (tm : MultiTapeTM k Symbol State) : MultiTapeTM k Symbol (State ⊕ RewindState) :=
   tm.seq (rewind .input)
 
+/-- The normalized machine starts in the original machine's initial configuration. -/
+lemma initCfg_rewindInput (tm : MultiTapeTM k Symbol State) (input : List Symbol) :
+    tm.rewindInput.initCfg input = Sequential.left (rewind .input) (tm.initCfg input) := rfl
+
 /-- Exact input-rewind execution from any configuration, once the first machine reaches its
 least halting time. Everything other than the input head and control state is preserved. -/
 lemma runFrom_rewindInput (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input)
@@ -52,6 +56,43 @@ lemma rewindInput_halts (tm : MultiTapeTM k Symbol State) (t : ℕ)
   · rw [tm.runFrom_eq_of_halt (tm.initCfg input) hu hhaltu]
     exact runFrom_rewindInput tm (tm.initCfg input) u hhaltu hactiveu
 
+/-- **Normalizing costs no space.** The rewind moves no work-tape head, so every cell the
+normalized machine visits was already visited by the original one. This is what makes the normal
+form free to use inside a combinator: only the time bound grows. -/
+lemma spaceUsed_rewindInput_le (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input)
+    (u v : ℕ) (hhalt : (tm.runFrom cfg u).state = none)
+    (hactive : ∀ m < u, (tm.runFrom cfg m).state ≠ none) :
+    tm.rewindInput.spaceUsed (Sequential.left (rewind .input) cfg) (u + v) ≤
+      tm.spaceUsed cfg u := by
+  refine spaceUsed_le_of_workTapePos_mem _ _ (u + v) u fun m _ i => ?_
+  rcases Nat.lt_or_ge m u with hm | hm
+  · rw [rewindInput,
+      Sequential.runFrom_left tm (rewind .input) cfg m fun r hr => hactive r (by omega)]
+    exact mem_visitedByTapeHead.mpr ⟨m, by omega, rfl⟩
+  · obtain ⟨j, rfl⟩ := Nat.exists_eq_add_of_le hm
+    rw [rewindInput, runFrom_seq tm (rewind .input) cfg u j hhalt hactive]
+    simp only [Sequential.right, Cfg.withState_workTapePos, Rewind.runFrom_input_workTapePos,
+      Cfg.withState_workTapePos]
+    exact mem_visitedByTapeHead.mpr ⟨u, by omega, rfl⟩
+
+/-- The normal form together with its cost: the run takes at most the input length plus two extra
+steps, and uses no extra space at all. The bound accepts padded native halting times. -/
+lemma rewindInput_halts_spaceUsed (tm : MultiTapeTM k Symbol State) (t : ℕ)
+    (hhalt : (tm.runFrom (tm.initCfg input) t).state = none) :
+    ∃ t' ≤ t + input.length + 2,
+      tm.rewindInput.runFrom (tm.rewindInput.initCfg input) t' =
+          Sequential.right (Rewind.inputCfg (tm.runFrom (tm.initCfg input) t) none 1) ∧
+        tm.rewindInput.spaceUsed (tm.rewindInput.initCfg input) t' ≤
+          tm.spaceUsed (tm.initCfg input) t := by
+  obtain ⟨u, hu, hhaltu, hactiveu⟩ := exists_minimal_halting_time tm (tm.initCfg input) t hhalt
+  refine ⟨u + ((tm.runFrom (tm.initCfg input) u).inputPos.val - 1 + 2), ?_, ?_, ?_⟩
+  · have := (tm.runFrom (tm.initCfg input) u).inputPos.isLt
+    omega
+  · rw [tm.runFrom_eq_of_halt (tm.initCfg input) hu hhaltu]
+    exact runFrom_rewindInput tm (tm.initCfg input) u hhaltu hactiveu
+  · exact (spaceUsed_rewindInput_le tm (tm.initCfg input) u _ hhaltu hactiveu).trans
+      (spaceUsed_mono tm (tm.initCfg input) hu)
+
 /-- Every halting run from an initial configuration has its input head at the initial position. -/
 def HaltsWithInputAtStart (tm : MultiTapeTM k Symbol State) : Prop :=
   ∀ (input : List Symbol) (t : ℕ), (tm.runFrom (tm.initCfg input) t).state = none →

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

@@ -6,7 +6,7 @@ Authors: Christian Reitwiessner, Samuel Schlesinger
 
 module
 
-public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic
+public import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas
 
 /-! # Configuration state replacement
 
@@ -63,6 +63,68 @@ lemma Cfg.withState_withState {cfg : Cfg k Symbol State input} {State' State'' :
 lemma Cfg.withState_self {cfg : Cfg k Symbol State input} :
     cfg.withState cfg.state = cfg := rfl
 
+/-- The configuration `cfg` with `o` prepended to the output produced so far. -/
+def Cfg.prependOutput (o : List Symbol) (cfg : Cfg k Symbol State input) :
+    Cfg k Symbol State input :=
+  { cfg with output := o ++ cfg.output }
+
+@[simp]
+lemma Cfg.prependOutput_state {o : List Symbol} {cfg : Cfg k Symbol State input} :
+    (cfg.prependOutput o).state = cfg.state := rfl
+
+@[simp]
+lemma Cfg.prependOutput_inputPos {o : List Symbol} {cfg : Cfg k Symbol State input} :
+    (cfg.prependOutput o).inputPos = cfg.inputPos := rfl
+
+@[simp]
+lemma Cfg.prependOutput_workTapes {o : List Symbol} {cfg : Cfg k Symbol State input} :
+    (cfg.prependOutput o).workTapes = cfg.workTapes := rfl
+
+@[simp]
+lemma Cfg.prependOutput_workTapePos {o : List Symbol} {cfg : Cfg k Symbol State input} :
+    (cfg.prependOutput o).workTapePos = cfg.workTapePos := rfl
+
+@[simp]
+lemma Cfg.prependOutput_output {o : List Symbol} {cfg : Cfg k Symbol State input} :
+    (cfg.prependOutput o).output = o ++ cfg.output := rfl
+
+@[simp]
+lemma Cfg.prependOutput_inputSymbol {o : List Symbol} {cfg : Cfg k Symbol State input} :
+    (cfg.prependOutput o).inputSymbol = cfg.inputSymbol := rfl
+
+@[simp]
+lemma Cfg.prependOutput_workTapeSymbols {o : List Symbol} {cfg : Cfg k Symbol State input} :
+    (cfg.prependOutput o).workTapeSymbols = cfg.workTapeSymbols := rfl
+
+/-- A step does not depend on the output accumulated so far, since the output tape is write-only
+and a step only appends to it. -/
+lemma step_prependOutput (tm : MultiTapeTM k Symbol State) (o : List Symbol)
+    (cfg : Cfg k Symbol State input) :
+    tm.step (cfg.prependOutput o) = (tm.step cfg).prependOutput o := by
+  cases hs : cfg.state with
+  | none => simp [step, Cfg.prependOutput, hs]
+  | some q =>
+    have hstate : (cfg.prependOutput o).state = some q := hs
+    unfold step
+    rw [hstate, hs, Cfg.prependOutput_inputSymbol, Cfg.prependOutput_workTapeSymbols]
+    apply Cfg.ext <;> simp [List.append_assoc]
+
+/-- A whole run does not depend on the output accumulated before it. This is what lets a machine
+be run after another one has already written part of the output. -/
+lemma runFrom_prependOutput (tm : MultiTapeTM k Symbol State) (o : List Symbol)
+    (cfg : Cfg k Symbol State input) (n : ℕ) :
+    tm.runFrom (cfg.prependOutput o) n = (tm.runFrom cfg n).prependOutput o := by
+  induction n with
+  | zero => rfl
+  | succ n ih => rw [runFrom_succ_eq_step', ih, step_prependOutput, runFrom_succ_eq_step']
+
+/-- Prepending output does not change the space used. -/
+lemma spaceUsed_prependOutput (tm : MultiTapeTM k Symbol State) (o : List Symbol)
+    (cfg : Cfg k Symbol State input) (n : ℕ) :
+    tm.spaceUsed (cfg.prependOutput o) n = tm.spaceUsed cfg n :=
+  spaceUsed_eq_of_workTapePos _ _ n fun m _ => by
+    rw [runFrom_prependOutput, Cfg.prependOutput_workTapePos]
+
 /-- A family of configurations with the prescribed steps agrees with `runFrom`. -/
 lemma runFrom_eq_of_step (tm : MultiTapeTM k Symbol State)
     (path : ℕ → Cfg k Symbol State input) (n : ℕ)