feat(MultiTapeTM): compose machines with time and space bounds

Cslib.lean

@@ -46,7 +46,22 @@ 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.Comp
 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.Composition
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Composition.Defs
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Composition.Layout
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Composition.Rewind
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Composition.Simulation
+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
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.OutputToWorkTape
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Rewind
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Sequential
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.TapeContents
 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/Combinators/Comp.lean

@@ -0,0 +1,82 @@
+/-
+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.Composition
+
+/-!
+# Complexity of composed functions
+
+Bounds depend on the actual input. Composition adds the component costs at `a` and `f a`, plus
+the length of the encoded intermediate result. No monotonicity assumption is needed. Bounds on
+encoded input length are recovered by weakening this pointwise statement.
+-/
+
+@[expose] public section
+
+namespace Turing.MultiTapeTM
+
+variable {α β γ : Type*}
+
+/-- Compose machine realizations of functions at their actual input-indexed bounds. -/
+theorem comp_computesFunInTimeAndSpace
+    {k₀ k₁ : ℕ} {Symbol State₀ State₁ : Type*}
+    (tm₀ : MultiTapeTM k₀ Symbol State₀) (tm₁ : MultiTapeTM k₁ Symbol State₁)
+    {encA : α ↪ List Symbol} {encB : β ↪ List Symbol} {encC : γ ↪ List Symbol}
+    {f : α → β} {g : β → γ} {tf sf : α → ℕ} {tg sg : β → ℕ}
+    (hf : ComputesFunInTimeAndSpace tm₀ encA encB f tf sf)
+    (hg : ComputesFunInTimeAndSpace tm₁ encB encC g tg sg) :
+    ComputesFunInTimeAndSpace (comp tm₀ tm₁) encA encC (g ∘ f)
+      (fun a => tf a + ((encB (f a)).length + 3) + 2 * tg (f a))
+      (fun a => sf a + ((encB (f a)).length + 2) + sg (f a)) := by
+  intro a
+  obtain ⟨t₀, ht₀, s₀, hs₀, hc₀⟩ := hf a
+  obtain ⟨t₁, ht₁, s₁, hs₁, hc₁⟩ := hg (f a)
+  obtain ⟨t, ht, s, hs, hc⟩ := comp_computesInTimeAndSpace tm₀ tm₁ hc₀ hc₁
+  exact ⟨t, by dsimp only; omega, s, by dsimp only; omega, hc⟩
+
+/-- Function composition preserves computability, with explicit pointwise time and space bounds. -/
+theorem computableInTimeAndSpace_comp
+    {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool}
+    {f : α → β} {g : β → γ} {tf sf : α → ℕ} {tg sg : β → ℕ}
+    (hf : ComputableInTimeAndSpace f encA encB tf sf)
+    (hg : ComputableInTimeAndSpace g encB encC tg sg) :
+    ComputableInTimeAndSpace (g ∘ f) encA encC
+      (fun a => tf a + ((encB (f a)).length + 3) + 2 * tg (f a))
+      (fun a => sf a + ((encB (f a)).length + 2) + sg (f a)) := by
+  obtain ⟨k₀, State₀, hfinite₀, tm₀, h₀⟩ := hf
+  obtain ⟨k₁, State₁, hfinite₁, tm₁, h₁⟩ := hg
+  let := Fintype.ofFinite State₀
+  let := Fintype.ofFinite RewindState
+  let := Fintype.ofFinite (InputState State₁)
+  exact ⟨compositionTapeCount k₀ k₁, CompositionState State₀ State₁, inferInstance,
+    comp tm₀ tm₁, comp_computesFunInTimeAndSpace tm₀ tm₁ h₀ h₁⟩
+
+/-- Length-based bounds follow from the pointwise theorem and an intermediate-length bound. -/
+theorem computableInTimeAndSpaceOfLength_comp
+    {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool}
+    {f : α → β} {g : β → γ} {tf sf tg sg L : ℕ → ℕ}
+    (hf : ComputableInTimeAndSpaceOfLength f encA encB tf sf)
+    (hg : ComputableInTimeAndSpaceOfLength g encB encC tg sg)
+    (hL : ∀ a, (encB (f a)).length ≤ L (encA a).length)
+    (htg : Monotone tg) (hsg : Monotone sg) :
+    ComputableInTimeAndSpaceOfLength (g ∘ f) encA encC
+      (fun n => tf n + (L n + 3) + 2 * tg (L n))
+      (fun n => sf n + (L n + 2) + sg (L n)) := by
+  apply (computableInTimeAndSpace_comp hf hg).mono
+  · intro a
+    have := hL a
+    have := htg (hL a)
+    dsimp only
+    omega
+  · intro a
+    have := hL a
+    have := hsg (hL a)
+    dsimp only
+    omega
+
+end Turing.MultiTapeTM

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

@@ -0,0 +1,14 @@
+# Complexity of functions
+
+The primary bounds depend on the actual input, with separate encodings for the input and output
+of a function. `ComputableInTimeAndSpace` hides the realizing machine and fixes the machine
+alphabet to `Bool`; `ComputesFunInTimeAndSpace` exposes a realization over an arbitrary alphabet.
+`ComputableInTimeAndSpaceOfLength` specializes bounds to the encoded input length.
+
+`Comp` proves that if `f` and `g` are computable, then so is `g ∘ f`, with time
+`tf a + (encB (f a)).length + 3 + 2 * tg (f a)` and space
+`sf a + (encB (f a)).length + 2 + sg (f a)`. This pointwise theorem requires no monotonicity.
+A separate corollary derives length-based bounds from an intermediate-length bound and
+monotonicity of the second function's bounds.
+
+The executable transformations and their `runFrom` proofs live in [Plumbing](../Plumbing).

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

@@ -1,17 +1,14 @@
 /-
 Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Christian Reitwiessner
+Authors: Christian Reitwiessner, Samuel Schlesinger
 -/
 
 module
 
-public import Mathlib.Data.Finset.Max
-public import Mathlib.Data.Int.Interval
 public import Mathlib.Algebra.Order.Group.Abs
 public import Mathlib.Algebra.Order.Group.Int
 public import Mathlib.Algebra.Order.BigOperators.Group.Finset
-public import Mathlib.Computability.Language
 public import Mathlib.Basic.Sign.Defs
 public import Cslib.Foundations.Data.RelatesInSteps
 
@@ -74,8 +71,10 @@ We define a number of structures and concepts related to multi-tape Turing machi
 * `spaceUsed`: the number of tape cells touched by work tape heads, our main space measure
 * `ComputesInTimeAndSpace`: a proof that a specific TM computes an output from an input in a certain
     number of steps and using a certain number of tape cells
-* `ComputableInTimeAndSpace`: a proof that there is a multi-tape TM that computes a function
-    (on strings) respecting a time and space bound in the input length.
+* `ComputesFunInTimeAndSpace`: a machine computes a function between specified encodings,
+    respecting time and space bounds on each actual input.
+* `ComputableInTimeAndSpace`: such a machine exists with binary alphabet and finitely many states.
+* `ComputableInTimeAndSpaceOfLength`: the specialization to bounds on encoded input length.
 * `DecidableInTimeAndSpace`: a proof that a TM decides a language within a certain time
     and space bound.
 
@@ -294,6 +293,20 @@ lemma runFrom_of_halt (cfg : Cfg k Symbol State input) (h : cfg.state = none) {n
   | succ d ih =>
     rw [runFrom_succ_eq_step', ih, step_of_halt h]
 
+/-- Once a run has halted, every later time denotes the same configuration. -/
+lemma runFrom_eq_of_halt (cfg : Cfg k Symbol State input) {τ t : ℕ} (hle : τ ≤ t)
+    (hhalt : (tm.runFrom cfg τ).state = none) :
+    tm.runFrom cfg t = tm.runFrom cfg τ := by
+  obtain ⟨d, rfl⟩ := Nat.exists_eq_add_of_le hle
+  rw [runFrom_add, runFrom_of_halt _ hhalt]
+
+/-- Halting is monotone in the number of execution steps. -/
+lemma runFrom_state_eq_none_mono (cfg : Cfg k Symbol State input) :
+    Monotone fun t => (tm.runFrom cfg t).state = none := by
+  intro τ t hle hhalt
+  rw [runFrom_eq_of_halt cfg hle hhalt]
+  exact hhalt
+
 @[simp]
 lemma outputSymbol_of_halt {cfg : Cfg k Symbol State input} (h_halt : cfg.state = none) :
     tm.outputSymbol cfg = none := by
@@ -369,9 +382,28 @@ lemma runFrom_output_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).output = (tm.runFrom cfg τ).output := by
-  conv_lhs => rw [← Nat.sub_add_cancel hle, Nat.add_comm]
-  rw [runFrom_add, runFrom_of_halt _ hhalt]
+    (tm.runFrom cfg t).output = (tm.runFrom cfg τ).output :=
+  congrArg Cfg.output (tm.runFrom_eq_of_halt cfg hle hhalt)
+
+/-- Output length is monotone because a machine only appends output symbols. -/
+lemma runFrom_output_length_mono
+    (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) :
+    Monotone fun t => (tm.runFrom cfg t).output.length := by
+  apply monotone_nat_of_le_succ
+  intro t
+  rw [runFrom_succ_eq_step', step_output, List.length_append]
+  exact Nat.le_add_right _ _
+
+/-- A run can append at most one output symbol per step. -/
+lemma runFrom_output_length_le
+    (tm : MultiTapeTM k Symbol State)
+    (cfg : Cfg k Symbol State input) (t : ℕ) :
+    (tm.runFrom cfg t).output.length ≤ cfg.output.length + t := by
+  induction t with
+  | zero => simp
+  | succ t ih =>
+      rw [runFrom_succ_eq_step', step_output, List.length_append]
+      grind [Option.toList]
 
 /-- A proof that the Turing machine `tm` on input `input` outputs `output` in at most `t` steps
 and uses exactly `s` space.
@@ -384,43 +416,67 @@ def ComputesInTimeAndSpace
   (tm.runFrom (tm.initCfg input) t).output = output ∧
   tm.spaceUsed (tm.initCfg input) t = s
 
-/-- A proof that the Turing machine `tm` computes the function `f` such that on all inputs of
-length `n` it uses at most `t n` steps and `s n` space. It assumes an embedding function
-from the input/output alphabet into the machine alphabet.
-Note that this does not require the alphabet or state set to be finite. -/
-def ComputesFunInTimeAndSpace
+/-- The output of a computation is no longer than its running time. -/
+lemma output_length_le_time
+    {tm : MultiTapeTM k Symbol State} {input output : List Symbol} {t s : ℕ}
+    (h : ComputesInTimeAndSpace tm input output t s) :
+    output.length ≤ t := by
+  obtain ⟨-, hout, -⟩ := h
+  rw [← hout]
+  simpa using tm.runFrom_output_length_le (tm.initCfg input) t
+
+/-- A machine computes `f` between the supplied encodings, with bounds depending on the input.
+The machine's alphabet and state type need not be finite. -/
+def ComputesFunInTimeAndSpace {α β : Type*}
     (tm : MultiTapeTM k Symbol State)
-    {IOSymbol : Type*}
-    (f : List IOSymbol → List IOSymbol)
-    (toMachineSymbol : IOSymbol ↪ Symbol)
-    (t s : ℕ → ℕ) : Prop :=
-  ∀ input, ∃ t' ≤ t input.length, ∃ s' ≤ s input.length,
-  ComputesInTimeAndSpace tm (input.map toMachineSymbol) ((f input).map toMachineSymbol) t' s'
-
-/-- The main definition of complexity of multi-tape Turing machines:
-A proof that the function `f` is computable by some multi-tape Turing machine `tm` (with finite
-work alphabet and finite state set) via an alphabet embedding function `toMachineSymbol`,
-such that on all inputs of length `n`, `tm` uses at most `t n` steps and at most `s n` space. -/
-def ComputableInTimeAndSpace
-    {IOSymbol : Type*}
-    (f : List IOSymbol → List IOSymbol)
+    (encIn : α ↪ List Symbol) (encOut : β ↪ List Symbol)
+    (f : α → β) (t s : α → ℕ) : Prop :=
+  ∀ a, ∃ t' ≤ t a, ∃ s' ≤ s a,
+    ComputesInTimeAndSpace tm (encIn a) (encOut (f a)) t' s'
+
+/-- A function is computable within the input-indexed bounds by a machine with binary alphabet
+and finitely many states. Input and output types may have different encodings. -/
+def ComputableInTimeAndSpace {α β : Type*}
+    (f : α → β) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool)
+    (t s : α → ℕ) : Prop :=
+  ∃ (k : ℕ) (State : Type) (_ : Finite State) (tm : MultiTapeTM k Bool State),
+    ComputesFunInTimeAndSpace tm encIn encOut f t s
+
+/-- Length-based complexity is the specialization to bounds on the encoded input length. -/
+abbrev ComputableInTimeAndSpaceOfLength {α β : Type*}
+    (f : α → β) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool)
     (t s : ℕ → ℕ) : Prop :=
-  ∃ (k sym state : ℕ) (toMachineSymbol : _) (tm : MultiTapeTM k (Fin sym) (Fin state)),
-  ComputesFunInTimeAndSpace tm f toMachineSymbol t s
+  ComputableInTimeAndSpace f encIn encOut
+    (fun a => t (encIn a).length) (fun a => s (encIn a).length)
+
+/-- Resource bounds can be weakened independently on every input. -/
+theorem ComputesFunInTimeAndSpace.mono {α β : Type*}
+    {tm : MultiTapeTM k Symbol State} {encIn : α ↪ List Symbol} {encOut : β ↪ List Symbol}
+    {f : α → β} {t s t' s' : α → ℕ}
+    (h : ComputesFunInTimeAndSpace tm encIn encOut f t s)
+    (ht : ∀ a, t a ≤ t' a) (hs : ∀ a, s a ≤ s' a) :
+    ComputesFunInTimeAndSpace tm encIn encOut f t' s' := fun a => by
+  obtain ⟨u, hu, v, hv, hc⟩ := h a
+  exact ⟨u, hu.trans (ht a), v, hv.trans (hs a), hc⟩
+
+/-- Computability is monotone in its input-indexed resource bounds. -/
+theorem ComputableInTimeAndSpace.mono {α β : Type*}
+    {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {t s t' s' : α → ℕ}
+    (h : ComputableInTimeAndSpace f encIn encOut t s)
+    (ht : ∀ a, t a ≤ t' a) (hs : ∀ a, s a ≤ s' a) :
+    ComputableInTimeAndSpace f encIn encOut t' s' := by
+  obtain ⟨k, State, hfinite, tm, htm⟩ := h
+  exact ⟨k, State, hfinite, tm, htm.mono ht hs⟩
 
 open Classical in
-/-- The indicator function of a language. -/
-noncomputable def indicator {Symbol : Type*} [Inhabited Symbol] (L : Language Symbol) :
-    List Symbol → List Symbol
-  | x => if x ∈ L then [default] else []
-
-/-- A language is decidable in time `t` and space `s` if and only if its indicator function
-is computable in time `t` and space `s`. -/
-def DecidableInTimeAndSpace
-    {IOSymbol : Type} [Inhabited IOSymbol]
-    (L : Language IOSymbol)
-    (t s : ℕ → ℕ) : Prop :=
-  ComputableInTimeAndSpace (indicator L) t s
+/-- The Boolean indicator function of a set. -/
+noncomputable def indicator {α : Type*} (L : Set α) : α → Bool :=
+  fun x => if x ∈ L then true else false
+
+/-- A set is decidable within the given input-indexed bounds when its Boolean indicator is. -/
+def DecidableInTimeAndSpace {α : Type*} (L : Set α) (enc : α ↪ List Bool)
+    (t s : α → ℕ) : Prop :=
+  ComputableInTimeAndSpace (indicator L) enc ⟨fun b => [b], by intro a b h; simpa using h⟩ t s
 
 /-- This lemma translates between the relational notion and the iterated step notion. The latter
 can be more convenient especially for deterministic machines as we have here. -/
@@ -448,6 +504,16 @@ def haltsAtStep (tm : MultiTapeTM k Symbol State) (input : List Symbol) (t : ℕ
   (tm.runFrom (tm.initCfg input) t).state.isNone &&
   !(tm.runFrom (tm.initCfg input) (t - 1)).state.isNone
 
+/-- Every padded halting run has a least halting time. -/
+lemma exists_minimal_halting_time (tm : MultiTapeTM k Symbol State)
+    (cfg : Cfg k Symbol State input) (t : ℕ)
+    (hhalt : (tm.runFrom cfg t).state = none) :
+    ∃ τ ≤ t, (tm.runFrom cfg τ).state = none ∧
+      ∀ m < τ, (tm.runFrom cfg m).state ≠ none := by
+  let hExists : ∃ n, (tm.runFrom cfg n).state = none := ⟨t, hhalt⟩
+  refine ⟨Nat.find hExists, Nat.find_min' hExists hhalt, Nat.find_spec hExists, ?_⟩
+  exact fun _ hm => Nat.find_min hExists hm
+
 /-- If a Turing machine halts, the time step is uniquely determined. -/
 lemma halting_step_unique
     {tm : MultiTapeTM k Symbol State}

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

@@ -0,0 +1,9 @@
+# Machine normal forms
+
+`RewindInput` transforms any machine into one whose halting runs have the native input head at
+position one. It sequences the original machine with the shared rewind controller from
+[Plumbing](../Plumbing). Output, work-tape contents, and work-tape head positions are retained.
+The transformation adds at most the input length plus two steps, including on empty input.
+
+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.