diff --git a/Cslib.lean b/Cslib.lean index 34a0d27be..e75bf0e4d 100644 --- a/Cslib.lean +++ b/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 diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Combinators/Comp.lean b/Cslib/Computability/Machines/Turing/MultiTape/Combinators/Comp.lean new file mode 100644 index 000000000..56e3b2daf --- /dev/null +++ b/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 diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Combinators/README.md b/Cslib/Computability/Machines/Turing/MultiTape/Combinators/README.md new file mode 100644 index 000000000..ceed2c98c --- /dev/null +++ b/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). diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index cc54495a3..a83a9b879 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/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} diff --git a/Cslib/Computability/Machines/Turing/MultiTape/NormalForms/README.md b/Cslib/Computability/Machines/Turing/MultiTape/NormalForms/README.md new file mode 100644 index 000000000..dadf3ffbe --- /dev/null +++ b/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. diff --git a/Cslib/Computability/Machines/Turing/MultiTape/NormalForms/RewindInput.lean b/Cslib/Computability/Machines/Turing/MultiTape/NormalForms/RewindInput.lean new file mode 100644 index 000000000..1accf2fac --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/NormalForms/RewindInput.lean @@ -0,0 +1,83 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Rewind +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Sequential + +/-! +# Halting with the input head rewound + +`rewindInput` follows an arbitrary machine with the native-input rewind controller. It preserves +all work tapes, work-tape head positions, and output, and halts with the input head at position one. +The overhead is at most the input length plus two, including for empty input. +-/ + +@[expose] public section + +namespace Turing.MultiTapeTM + +variable {k : ℕ} {Symbol State : Type*} {input : List Symbol} + +/-- Normalize a machine to halt with its input head at the initial position. -/ +def rewindInput (tm : MultiTapeTM k Symbol State) : MultiTapeTM k Symbol (State ⊕ RewindState) := + tm.seq (rewind .input) + +/-- 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) + (u : ℕ) (hhalt : (tm.runFrom cfg u).state = none) + (hactive : ∀ m < u, (tm.runFrom cfg m).state ≠ none) : + tm.rewindInput.runFrom (Sequential.left (rewind .input) cfg) + (u + ((tm.runFrom cfg u).inputPos.val - 1 + 2)) = + Sequential.right (Rewind.inputCfg (tm.runFrom cfg u) none 1) := by + rw [rewindInput, runFrom_seq tm (rewind .input) cfg u _ hhalt hactive] + exact congrArg Sequential.right (Rewind.runFrom_input (tm.runFrom cfg u)) + +/-- Any halting computation can be normalized to finish with its input head reset. +The bound accepts padded native halting times. -/ +lemma rewindInput_halts (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) := 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 + +/-- 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 → + (tm.runFrom (tm.initCfg input) t).inputPos = 1 + +/-- The transformed machine satisfies the normal form at every halting time, including padding. -/ +lemma rewindInput_haltsWithInputAtStart (tm : MultiTapeTM k Symbol State) : + HaltsWithInputAtStart tm.rewindInput := by + intro input t ht + have hnative : (tm.runFrom (tm.initCfg input) t).state = none := by + by_contra hn + have hactive (m : ℕ) (hm : m < t) : (tm.runFrom (tm.initCfg input) m).state ≠ none := + fun h => hn (tm.runFrom_state_eq_none_mono (tm.initCfg input) (by omega) h) + have hleft := Sequential.runFrom_left tm (rewind .input) (tm.initCfg input) t hactive + change ((tm.seq (rewind .input)).runFrom + (Sequential.left (rewind .input) (tm.initCfg input)) t).state = none at ht + rw [hleft] at ht + simp [Sequential.left] at ht + obtain ⟨s, _, hfinal⟩ := rewindInput_halts tm t hnative + have hs : (tm.rewindInput.runFrom (tm.rewindInput.initCfg input) s).state = none := by + rw [hfinal] + rfl + rcases Nat.le_total t s with hle | hle + · have heq := tm.rewindInput.runFrom_eq_of_halt (tm.rewindInput.initCfg input) hle ht + exact congrArg Cfg.inputPos (heq.symm.trans hfinal) + · rw [tm.rewindInput.runFrom_eq_of_halt (tm.rewindInput.initCfg input) hle hs, hfinal] + rfl + +end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Basic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Basic.lean new file mode 100644 index 000000000..ab83d4d1e --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Basic.lean @@ -0,0 +1,76 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. 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.Deterministic + +/-! # Configuration state replacement + +`Cfg.withState` changes the control state, possibly changing its type, and preserves all tapes, +head positions, and accumulated output. +-/ + +@[expose] public section + +namespace Turing.MultiTapeTM + +variable {k : ℕ} {State Symbol : Type*} {input : List Symbol} + +/-- The configuration `cfg` with its state replaced by `q`, possibly over a different state +type. -/ +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⟩ + +@[simp] +lemma Cfg.withState_state {cfg : Cfg k Symbol State input} {State' : Type*} + {q : Option State'} : (cfg.withState q).state = q := rfl + +@[simp] +lemma Cfg.withState_inputPos {cfg : Cfg k Symbol State input} {State' : Type*} + {q : Option State'} : (cfg.withState q).inputPos = cfg.inputPos := rfl + +@[simp] +lemma Cfg.withState_workTapes {cfg : Cfg k Symbol State input} {State' : Type*} + {q : Option State'} : (cfg.withState q).workTapes = cfg.workTapes := rfl + +@[simp] +lemma Cfg.withState_workTapePos {cfg : Cfg k Symbol State input} {State' : Type*} + {q : Option State'} : (cfg.withState q).workTapePos = cfg.workTapePos := rfl + +@[simp] +lemma Cfg.withState_output {cfg : Cfg k Symbol State input} {State' : Type*} + {q : Option State'} : (cfg.withState q).output = cfg.output := rfl + +@[simp] +lemma Cfg.withState_inputSymbol {cfg : Cfg k Symbol State input} {State' : Type*} + {q : Option State'} : (cfg.withState q).inputSymbol = cfg.inputSymbol := rfl + +@[simp] +lemma Cfg.withState_workTapeSymbols {cfg : Cfg k Symbol State input} {State' : Type*} + {q : Option State'} : (cfg.withState q).workTapeSymbols = cfg.workTapeSymbols := rfl + +@[simp] +lemma Cfg.withState_withState {cfg : Cfg k Symbol State input} {State' State'' : Type*} + {q : Option State'} {q' : Option State''} : + (cfg.withState q).withState q' = cfg.withState q' := rfl + +@[simp] +lemma Cfg.withState_self {cfg : Cfg k Symbol State input} : + cfg.withState cfg.state = cfg := rfl + +/-- 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 : ℕ) + (hstep : ∀ r < n, tm.step (path r) = path (r + 1)) : + tm.runFrom (path 0) n = path n := by + induction n with + | zero => rfl + | succ n ih => + rw [runFrom_succ_eq_step', ih (fun r hr => hstep r (by omega)), hstep n (by omega)] + +end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Composition.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Composition.lean new file mode 100644 index 000000000..0562c2f63 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Composition.lean @@ -0,0 +1,370 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Composition.Rewind + +import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas +import Mathlib.Algebra.BigOperators.Fin + +/-! +# Correctness and resource bounds for multi-tape composition + +`comp_haltsWithOutput` gives operational correctness. `comp_computesInTimeAndSpace` composes +individual computations, charging the rewind and extra tape to the actual intermediate output +length. The function-level interface is in `MultiTape.Combinators.Comp`. + +The first machine takes one composite step per native step; the second takes two. The bounds +include the intermediate tape and both blank boundary cells. They permit padded halting times. +As in `MultiTapeTM`, these results do not require finite alphabets or state types. +-/ + +@[expose] public section + +namespace Turing.MultiTapeTM + +open Composition + +variable {k₀ k₁ : ℕ} +variable {Symbol State₀ State₁ : Type*} + +variable (tm₀ : MultiTapeTM k₀ Symbol State₀) (tm₁ : MultiTapeTM k₁ Symbol State₁) + +/-- +After both component machines halt, the composite machine halts with the output of the second +machine. + +If the first machine halts on `input` at exactly time `u` having produced `out₀`, and the second +machine has halted on input `out₀` by time `v` having produced `out₁`, then after +`u + (out₀.length + 3) + 2 * v` steps — the first machine's run, a rewind of the intermediate +output, and a two-steps-per-step simulation of the second machine — the composite machine on +`input` has halted with output exactly `out₁`. +-/ +theorem comp_haltsWithOutput + {input out₀ out₁ : List Symbol} {u v : ℕ} + (hhalt₀ : (tm₀.runFrom (tm₀.initCfg input) u).state = none) + (hactive₀ : ∀ m < u, (tm₀.runFrom (tm₀.initCfg input) m).state ≠ none) + (hout₀ : (tm₀.runFrom (tm₀.initCfg input) u).output = out₀) + (hhalt₁ : (tm₁.runFrom (tm₁.initCfg out₀) v).state = none) + (hout₁ : (tm₁.runFrom (tm₁.initCfg out₀) v).output = out₁) : + ((comp tm₀ tm₁).runFrom ((comp tm₀ tm₁).initCfg input) + (u + (out₀.length + 3) + 2 * v)).state = none ∧ + ((comp tm₀ tm₁).runFrom ((comp tm₀ tm₁).initCfg input) + (u + (out₀.length + 3) + 2 * v)).output = out₁ := by + subst out₀ + subst out₁ + have hfinal := runFrom_secondPhase tm₀ tm₁ + (tm₀.runFrom (tm₀.initCfg input) u) + (tm₁.initCfg (tm₀.runFrom (tm₀.initCfg input) u).output) v + rw [← runFrom_to_secondInit tm₀ tm₁ input u hhalt₀ hactive₀, ← runFrom_add] at hfinal + rw [hfinal] + simp only [embedSecond, hhalt₁, and_self] + +/-- Final first-component configuration used throughout the resource analysis. -/ +@[simp] private abbrev firstFinalCfg + (tm₀ : MultiTapeTM k₀ Symbol State₀) (input : List Symbol) (u : ℕ) : + Cfg k₀ Symbol State₀ input := + tm₀.runFrom (tm₀.initCfg input) u + +/-- Initial second-component configuration for the output of the first component. -/ +private abbrev secondInitCfg + (tm₀ : MultiTapeTM k₀ Symbol State₀) + (tm₁ : MultiTapeTM k₁ Symbol State₁) + (input : List Symbol) (u : ℕ) : + Cfg k₁ Symbol State₁ (firstFinalCfg tm₀ input u).output := + tm₁.initCfg (firstFinalCfg tm₀ input u).output + +/-- Second-component configuration after `m` simulated steps. -/ +private abbrev secondCfgAt + (tm₀ : MultiTapeTM k₀ Symbol State₀) + (tm₁ : MultiTapeTM k₁ Symbol State₁) + (input : List Symbol) (u m : ℕ) : + Cfg k₁ Symbol State₁ (firstFinalCfg tm₀ input u).output := + tm₁.runFrom (secondInitCfg tm₀ tm₁ input u) m + +/-- Duration used to simulate component runs of lengths `u` and `v`. -/ +private abbrev compositionTotalTime + (tm₀ : MultiTapeTM k₀ Symbol State₀) (input : List Symbol) (u v : ℕ) : ℕ := + u + ((firstFinalCfg tm₀ input u).output.length + 3) + 2 * v + +/-- The first component must switch phases at its earliest halting time. -/ +private structure CompositionRunSpec + (tm₀ : MultiTapeTM k₀ Symbol State₀) + (input : List Symbol) (u : ℕ) : Prop where + firstHalted : (firstFinalCfg tm₀ input u).state = none + firstActive : ∀ m < u, (tm₀.runFrom (tm₀.initCfg input) m).state ≠ none + +/-- A named phase witness for a configuration occurring in a complete composite run. -/ +private inductive CompositionCfgPhase + (tm₀ : MultiTapeTM k₀ Symbol State₀) + (tm₁ : MultiTapeTM k₁ Symbol State₁) + (input : List Symbol) (u v : ℕ) + (cfg : Cfg (compositionTapeCount k₀ k₁) Symbol + (CompositionState State₀ State₁) input) : Prop + | first (m : ℕ) (hm : m ≤ u) + (hcfg : cfg = embedFirst tm₀ tm₁ + (tm₀.runFrom (tm₀.initCfg input) m)) + | rewind (s : ℕ) + (hs : s ≤ (firstFinalCfg tm₀ input u).output.length) + (hcfg : cfg = intermediateCfg tm₀ tm₁ + (firstFinalCfg tm₀ input u) + (.inr (.inl .scan)) + (((firstFinalCfg tm₀ input u).output.length : ℤ) - 1 - s)) + | initialClassify + (hcfg : cfg = intermediateCfg tm₀ tm₁ + (firstFinalCfg tm₀ input u) + (.inr (.inr (.classify tm₁.q₀ .right))) 0) + | second (m : ℕ) (hm : m ≤ v) + (hcfg : cfg = embedSecond tm₀ tm₁ + (firstFinalCfg tm₀ input u) + (secondCfgAt tm₀ tm₁ input u m)) + | secondClassify (m : ℕ) (hm : m < v) (boundary : InputBoundary) + (hcfg : cfg = classifyCfg tm₀ tm₁ + (firstFinalCfg tm₀ input u) + (secondCfgAt tm₀ tm₁ input u (m + 1)) + boundary) + +/-- +Every prefix of a complete composite run is in one of the configurations described by +the first simulation, the rewind, the initial classifier, or an even or odd second-phase step. +-/ +private lemma runFrom_composition_cases + (input : List Symbol) (u v r : ℕ) + (hrun : CompositionRunSpec tm₀ input u) + (hr : r ≤ compositionTotalTime tm₀ input u v) : + CompositionCfgPhase tm₀ tm₁ input u v + ((comp tm₀ tm₁).runFrom ((comp tm₀ tm₁).initCfg input) r) := by + by_cases hfirst : r ≤ u + · exact .first r hfirst (runFrom_firstPhase tm₀ tm₁ input r + (fun m hm => hrun.firstActive m (lt_of_lt_of_le hm hfirst))) + obtain ⟨offset, rfl⟩ := Nat.exists_eq_add_of_le (by omega : u ≤ r) + have hprefix := runFrom_firstPhase tm₀ tm₁ input u hrun.firstActive + by_cases hrewind : offset ≤ (firstFinalCfg tm₀ input u).output.length + 1 + · refine .rewind (offset - 1) (by omega) ?_ + rw [runFrom_add, hprefix] + convert runFrom_firstHalt_rewind tm₀ tm₁ + (firstFinalCfg tm₀ input u) hrun.firstHalted (offset - 1) (by omega) using 1 + congr 1 + omega + by_cases hclassify : offset = (firstFinalCfg tm₀ input u).output.length + 2 + · refine .initialClassify ?_ + rw [runFrom_add, hprefix, hclassify] + exact runFrom_firstHalt_classify tm₀ tm₁ _ hrun.firstHalted + obtain ⟨secondSteps, hoffset⟩ := Nat.exists_eq_add_of_le + (by omega : (firstFinalCfg tm₀ input u).output.length + 3 ≤ offset) + have hsecondSteps : secondSteps ≤ 2 * v := by + dsimp only [compositionTotalTime] at hr + omega + have hsecond : + (comp tm₀ tm₁).runFrom ((comp tm₀ tm₁).initCfg input) (u + offset) = + (comp tm₀ tm₁).runFrom + (embedSecond tm₀ tm₁ (firstFinalCfg tm₀ input u) + (secondInitCfg tm₀ tm₁ input u)) secondSteps := by + rw [hoffset, ← Nat.add_assoc, runFrom_add, + runFrom_to_secondInit tm₀ tm₁ input u hrun.firstHalted hrun.firstActive] + rcases Nat.even_or_odd' secondSteps with ⟨m, heven | hodd⟩ + · refine .second m (by omega) ?_ + rw [hsecond, heven] + exact runFrom_secondPhase tm₀ tm₁ _ _ m + · obtain ⟨boundary, hboundary⟩ := runFrom_secondPhase_odd tm₀ tm₁ + (firstFinalCfg tm₀ input u) (secondInitCfg tm₀ tm₁ input u) m + exact .secondClassify m (by omega) boundary (by rw [hsecond, hodd, hboundary]) + +/-! +## Resource bounds and function-level correctness +-/ + + +/-- Decompose composite space usage into the first, intermediate, and second tape blocks. -/ +private lemma compositionSpaceUsed_eq + {input : List Symbol} + (cfg : Cfg (compositionTapeCount k₀ k₁) Symbol + (CompositionState State₀ State₁) input) + (t : ℕ) : + (comp tm₀ tm₁).spaceUsed cfg t = + (∑ i : Fin k₀, (comp tm₀ tm₁).spaceUsedByTape cfg t + (compositionFirstTapeIdx k₁ i)) + + (comp tm₀ tm₁).spaceUsedByTape cfg t + (compositionIntermediateTapeIdx k₀ k₁) + + ∑ i : Fin k₁, (comp tm₀ tm₁).spaceUsedByTape cfg t + (compositionSecondTapeIdx k₀ k₁ i) := by + unfold spaceUsed + rw [Fin.sum_univ_add, Fin.sum_univ_castSucc] + congr 1 + +/-- Every first-component tape position in a complete composite run occurs in the first run. -/ +private lemma exists_firstComponent_tapePos_eq + (input : List Symbol) (u v r : ℕ) + (hrun : CompositionRunSpec tm₀ input u) + (hr : r ≤ compositionTotalTime tm₀ input u v) + (i : Fin k₀) : + ∃ m ≤ u, + ((comp tm₀ tm₁).runFrom + ((comp tm₀ tm₁).initCfg input) r).workTapePos + (compositionFirstTapeIdx k₁ i) = + (tm₀.runFrom (tm₀.initCfg input) m).workTapePos i := by + have hphase := runFrom_composition_cases tm₀ tm₁ input u v r hrun hr + have hidx_ne : i.val ≠ k₀ := by omega + cases hphase with + | first m hm hcfg => + refine ⟨m, hm, ?_⟩ + rw [hcfg] + simp [embedFirst, compositionFirstTapeIdx] + | rewind _ _ hcfg | initialClassify hcfg => + refine ⟨u, le_rfl, ?_⟩ + rw [hcfg] + simp [intermediateCfg, embedFirst, compositionFirstTapeIdx, hidx_ne] + | second _ _ hcfg | secondClassify _ _ _ hcfg => + refine ⟨u, le_rfl, ?_⟩ + rw [hcfg] + simp [classifyCfg, embedSecond, compositionFirstTapeIdx] + +/-- Every second-component tape position in a complete composite run occurs in the second run. -/ +private lemma exists_secondComponent_tapePos_eq + (input : List Symbol) (u v r : ℕ) + (hrun : CompositionRunSpec tm₀ input u) + (hr : r ≤ compositionTotalTime tm₀ input u v) + (i : Fin k₁) : + ∃ m ≤ v, + ((comp tm₀ tm₁).runFrom + ((comp tm₀ tm₁).initCfg input) r).workTapePos + (compositionSecondTapeIdx k₀ k₁ i) = + (secondCfgAt tm₀ tm₁ input u m).workTapePos i := by + have hphase := runFrom_composition_cases tm₀ tm₁ input u v r hrun hr + have hidx_not_lt : ¬ k₀ + 1 + i.val < k₀ := by omega + have hidx_ne : k₀ + 1 + i.val ≠ k₀ := by omega + cases hphase with + | first _ _ hcfg => + refine ⟨0, Nat.zero_le _, ?_⟩ + rw [hcfg] + simp [embedFirst, compositionSecondTapeIdx, secondCfgAt, secondInitCfg, runFrom, + hidx_not_lt, hidx_ne] + | rewind _ _ hcfg | initialClassify hcfg => + refine ⟨0, Nat.zero_le _, ?_⟩ + rw [hcfg] + simp [intermediateCfg, embedFirst, compositionSecondTapeIdx, + secondCfgAt, secondInitCfg, runFrom, hidx_not_lt, hidx_ne] + | second m hm hcfg => + refine ⟨m, hm, ?_⟩ + rw [hcfg] + simp [embedSecond, compositionSecondTapeIdx, hidx_not_lt, hidx_ne] + | secondClassify m hm _ hcfg => + refine ⟨m + 1, by omega, ?_⟩ + rw [hcfg] + simp [classifyCfg, embedSecond, compositionSecondTapeIdx, + hidx_not_lt, hidx_ne] + +/-- Throughout a complete composite run, the intermediate head stays between the two blank cells +immediately outside the first component's output. -/ +private lemma compositionIntermediateTapePos_mem_Icc + (input : List Symbol) (u v r : ℕ) + (hrun : CompositionRunSpec tm₀ input u) + (hr : r ≤ compositionTotalTime tm₀ input u v) : + ((comp tm₀ tm₁).runFrom + ((comp tm₀ tm₁).initCfg input) r).workTapePos + (compositionIntermediateTapeIdx k₀ k₁) ∈ + Finset.Icc (-1) ((firstFinalCfg tm₀ input u).output.length : ℤ) := by + have hphase := runFrom_composition_cases tm₀ tm₁ input u v r hrun hr + cases hphase with + | first m hm hcfg => + have hmoutput := tm₀.runFrom_output_length_mono (tm₀.initCfg input) hm + dsimp only at hmoutput + rw [hcfg] + simp only [tapes, firstFinalCfg, embedFirst, compositionIntermediateTapeIdx_val, + lt_self_iff_false, ↓reduceDIte, Finset.mem_Icc] + constructor <;> omega + | rewind s hs hcfg => + rw [hcfg] + simp only [firstFinalCfg, intermediateCfg, compositionIntermediateTapeIdx_val, + ↓reduceIte, Finset.mem_Icc] at hs ⊢ + constructor <;> omega + | initialClassify hcfg => + rw [hcfg] + simp [intermediateCfg] + | second m _ hcfg => + have hp := (secondCfgAt tm₀ tm₁ input u m).inputPos.isLt + simp only [secondCfgAt, secondInitCfg, firstFinalCfg] at hp + rw [hcfg] + simp only [tapes, firstFinalCfg, embedSecond, compositionIntermediateTapeIdx_val, + lt_self_iff_false, ↓reduceDIte, Finset.mem_Icc] + unfold InputFromWorkTape.virtualInputPos + constructor <;> omega + | secondClassify m _ _ hcfg => + have hp := (secondCfgAt tm₀ tm₁ input u (m + 1)).inputPos.isLt + simp only [secondCfgAt, secondInitCfg, firstFinalCfg] at hp + rw [hcfg] + simp only [tapes, firstFinalCfg, classifyCfg, embedSecond, + compositionIntermediateTapeIdx_val, lt_self_iff_false, ↓reduceDIte, + Finset.mem_Icc] + unfold InputFromWorkTape.virtualInputPos + constructor <;> omega + +/-- The intermediate tape visits at most `output.length + 2` cells in a complete run. -/ +private lemma compositionIntermediateSpace_le + (input : List Symbol) (u v : ℕ) + (hrun : CompositionRunSpec tm₀ input u) : + (comp tm₀ tm₁).spaceUsedByTape + ((comp tm₀ tm₁).initCfg input) + (compositionTotalTime tm₀ input u v) + (compositionIntermediateTapeIdx k₀ k₁) ≤ + (firstFinalCfg tm₀ input u).output.length + 2 := by + calc + _ ≤ (Finset.Icc (-1) ((firstFinalCfg tm₀ input u).output.length : ℤ)).card := by + apply Finset.card_le_card + intro p hp + obtain ⟨r, hr, rfl⟩ := (comp tm₀ tm₁).mem_visitedByTapeHead.mp hp + exact compositionIntermediateTapePos_mem_Icc tm₀ tm₁ input u v r hrun (by omega) + _ = _ := by rw [Int.card_Icc]; omega + +/-- Component tape blocks retain their native space bounds; only the intermediate tape is new. -/ +private lemma CompositionRunSpec.spaceUsed_le + {input : List Symbol} {u v : ℕ} (hrun : CompositionRunSpec tm₀ input u) : + (comp tm₀ tm₁).spaceUsed ((comp tm₀ tm₁).initCfg input) + (compositionTotalTime tm₀ input u v) ≤ + tm₀.spaceUsed (tm₀.initCfg input) u + + ((firstFinalCfg tm₀ input u).output.length + 2) + + tm₁.spaceUsed (secondInitCfg tm₀ tm₁ input u) v := by + rw [compositionSpaceUsed_eq] + apply Nat.add_le_add + · apply Nat.add_le_add + · apply Finset.sum_le_sum + intro i _ + exact spaceUsedByTape_le_of_positions _ _ _ _ _ _ _ _ + (fun r hr => exists_firstComponent_tapePos_eq tm₀ tm₁ input u v r hrun hr i) + · exact compositionIntermediateSpace_le tm₀ tm₁ input u v hrun + · apply Finset.sum_le_sum + intro i _ + exact spaceUsedByTape_le_of_positions _ _ _ _ _ _ _ _ + (fun r hr => exists_secondComponent_tapePos_eq tm₀ tm₁ input u v r hrun hr i) + +/-- Compose two bounded computations, charging the intermediate tape and rewind to the actual +intermediate output length. Component halting times may be padded. -/ +theorem comp_computesInTimeAndSpace + {input middle output : List Symbol} {t₀ s₀ t₁ s₁ : ℕ} + (h₀ : ComputesInTimeAndSpace tm₀ input middle t₀ s₀) + (h₁ : ComputesInTimeAndSpace tm₁ middle output t₁ s₁) : + ∃ t ≤ t₀ + (middle.length + 3) + 2 * t₁, + ∃ s ≤ s₀ + (middle.length + 2) + s₁, + ComputesInTimeAndSpace (comp tm₀ tm₁) input output t s := by + obtain ⟨u, hu, hhaltu, hactiveu⟩ := + exists_minimal_halting_time tm₀ (tm₀.initCfg input) t₀ h₀.1 + have houtu : (firstFinalCfg tm₀ input u).output = middle := + (tm₀.runFrom_output_eq_of_halt _ hu hhaltu).symm.trans h₀.2.1 + have hrun : CompositionRunSpec tm₀ input u := ⟨hhaltu, hactiveu⟩ + have hspace := hrun.spaceUsed_le tm₀ tm₁ (v := t₁) + have hspace₀ := tm₀.spaceUsed_mono (tm₀.initCfg input) hu + dsimp only [compositionTotalTime, secondInitCfg] at hspace + rw [houtu, h₁.2.2] at hspace + dsimp only at hspace₀ + rw [h₀.2.2] at hspace₀ + refine ⟨u + (middle.length + 3) + 2 * t₁, by omega, + (comp tm₀ tm₁).spaceUsed ((comp tm₀ tm₁).initCfg input) + (u + (middle.length + 3) + 2 * t₁), by omega, ?_⟩ + have hcomp := comp_haltsWithOutput tm₀ tm₁ hhaltu hactiveu houtu h₁.1 h₁.2.1 + exact ⟨hcomp.1, hcomp.2, rfl⟩ + +end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Composition/Defs.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Composition/Defs.lean new file mode 100644 index 000000000..2486f0a77 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Composition/Defs.lean @@ -0,0 +1,175 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.ExtendTapes +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.OutputToWorkTape +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.InputFromWorkTape +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Rewind +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Sequential + +/-! +# Composition of deterministic multi-tape Turing machines + +The composite redirects the first machine's output to an intermediate work tape, rewinds it, +and simulates the second machine with that tape as its input. Work tapes occupy disjoint blocks. +A classification step after each simulated input move restores the native boundary behavior. +Both machines use the same alphabet; no extra tape symbols are required. + +`comp` is the executable construction. The `Composition` namespace also contains the +configuration embeddings used by the simulation proofs. +-/ + +@[expose] public section + +namespace Turing.MultiTapeTM + +variable {k₀ k₁ : ℕ} +variable {Symbol State₀ State₁ : Type*} + +/-- Number of work tapes used by the composition of a `k₀`- and a `k₁`-tape machine. -/ +abbrev compositionTapeCount (k₀ k₁ : ℕ) := k₀ + 1 + k₁ + +/-- Physical coordinate of work tape `i` of the first machine. -/ +def compositionFirstTapeIdx (k₁ : ℕ) (i : Fin k₀) : Fin (compositionTapeCount k₀ k₁) := + i.castSucc.castAdd k₁ + +/-- Physical coordinate of the tape containing the intermediate output. -/ +def compositionIntermediateTapeIdx (k₀ k₁ : ℕ) : Fin (compositionTapeCount k₀ k₁) := + (Fin.last k₀).castAdd k₁ + +/-- Physical coordinate of work tape `i` of the second machine. -/ +def compositionSecondTapeIdx (k₀ k₁ : ℕ) (i : Fin k₁) : + Fin (compositionTapeCount k₀ k₁) := + Fin.natAdd (k₀ + 1) i + +@[simp] +lemma compositionFirstTapeIdx_val (k₁ : ℕ) (i : Fin k₀) : + (compositionFirstTapeIdx k₁ i).val = i.val := rfl + +@[simp] +lemma compositionIntermediateTapeIdx_val (k₀ k₁ : ℕ) : + (compositionIntermediateTapeIdx k₀ k₁).val = k₀ := rfl + +@[simp] +lemma compositionSecondTapeIdx_val (k₀ : ℕ) (i : Fin k₁) : + (compositionSecondTapeIdx k₀ k₁ i).val = k₀ + 1 + i.val := rfl + +/-- States of the three sequential phases: output, rewind, and virtual-input execution. -/ +abbrev CompositionState (State₀ State₁ : Type*) := State₀ ⊕ (RewindState ⊕ InputState State₁) + +/-- Assemble the first work-tape block, the intermediate tape, and the second block. +The same layout is used for tape contents and head positions. -/ +@[simp] +def Composition.tapes {α : Type*} (first : Fin k₀ → α) (middle : α) (second : Fin k₁ → α) + (i : Fin (compositionTapeCount k₀ k₁)) : α := + if h : i.val < k₀ then first ⟨i, h⟩ + else if hmiddle : i.val = k₀ then middle + else second ⟨i.val - (k₀ + 1), by have := i.isLt; simp only [compositionTapeCount] at *; omega⟩ + +namespace Composition + +/-- Place the first machine and its output tape before the second work-tape block. -/ +def outputEmbedding (k₀ k₁ : ℕ) : Fin (k₀ + 1) ↪ Fin (compositionTapeCount k₀ k₁) := + ⟨Fin.castAdd k₁, Fin.castAdd_injective (k₀ + 1) k₁⟩ + +/-- Place the virtual input before the second machine's work tapes. -/ +def inputEmbedding (k₀ k₁ : ℕ) : Fin (k₁ + 1) ↪ Fin (compositionTapeCount k₀ k₁) := + ⟨fun i => ⟨k₀ + i.val, by have := i.isLt; simp only [compositionTapeCount]; omega⟩, + fun i j h => Fin.ext (by have := congrArg Fin.val h; dsimp at this; omega)⟩ + +@[simp] +lemma inputEmbedding_val (i : Fin (k₁ + 1)) : + (inputEmbedding k₀ k₁ i).val = k₀ + i.val := rfl + +/-- The first machine, with output redirected and the second tape block left idle. -/ +def outputMachine (tm₀ : MultiTapeTM k₀ Symbol State₀) (k₁ : ℕ) := + tm₀.outputToWorkTape.extendTapes (outputEmbedding k₀ k₁) + +/-- The second machine, with virtual input and the first tape block left idle. -/ +def inputMachine (k₀ : ℕ) (tm₁ : MultiTapeTM k₁ Symbol State₁) := + tm₁.inputFromWorkTape.extendTapes (inputEmbedding k₀ k₁) + +end Composition + +/-- Compose functions by redirecting output, rewinding it, then using it as the next input. -/ +def comp (tm₀ : MultiTapeTM k₀ Symbol State₀) (tm₁ : MultiTapeTM k₁ Symbol State₁) : + MultiTapeTM (compositionTapeCount k₀ k₁) Symbol (CompositionState State₀ State₁) := + (Composition.outputMachine tm₀ k₁).seq + ((rewind (.work (compositionIntermediateTapeIdx k₀ k₁))).seq + (Composition.inputMachine k₀ tm₁)) + +namespace Composition + +/-- Embed a first-machine configuration into the first phase of the composite machine. -/ +def embedFirst + (_tm₀ : MultiTapeTM k₀ Symbol State₀) + (_tm₁ : MultiTapeTM k₁ Symbol State₁) + {input : List Symbol} + (cfg : Cfg k₀ Symbol State₀ input) : + Cfg (compositionTapeCount k₀ k₁) Symbol (CompositionState State₀ State₁) input where + state := match cfg.state with + | some q => some (.inl q) + | none => some (.inr (.inl .start)) + inputPos := cfg.inputPos + workTapes := tapes cfg.workTapes (listTape cfg.output) (fun _ _ => none) + workTapePos := tapes cfg.workTapePos cfg.output.length (fun _ => 0) + output := [] + +/-- Embed a second-machine configuration into the second phase of the composite machine. -/ +def embedSecond + (_tm₀ : MultiTapeTM k₀ Symbol State₀) + (_tm₁ : MultiTapeTM k₁ Symbol State₁) + {firstInput : List Symbol} + (firstCfg : Cfg k₀ Symbol State₀ firstInput) + {secondInput : List Symbol} + (secondCfg : Cfg k₁ Symbol State₁ secondInput) : + Cfg (compositionTapeCount k₀ k₁) Symbol + (CompositionState State₀ State₁) firstInput where + state := match secondCfg.state with + | some q => some (.inr (.inr (.run q (InputFromWorkTape.inputMode secondCfg.inputPos)))) + | none => none + inputPos := firstCfg.inputPos + workTapes := tapes firstCfg.workTapes (listTape secondInput) secondCfg.workTapes + workTapePos := tapes firstCfg.workTapePos + (InputFromWorkTape.virtualInputPos secondCfg.inputPos) secondCfg.workTapePos + output := secondCfg.output + +/-- The intermediate configuration between the moving and classifying halves of a simulated +second-machine step. -/ +def classifyCfg + (_tm₀ : MultiTapeTM k₀ Symbol State₀) + (_tm₁ : MultiTapeTM k₁ Symbol State₁) + {firstInput : List Symbol} + (firstCfg : Cfg k₀ Symbol State₀ firstInput) + {secondInput : List Symbol} + (secondCfg : Cfg k₁ Symbol State₁ secondInput) + (boundary : InputBoundary) : + Cfg (compositionTapeCount k₀ k₁) Symbol + (CompositionState State₀ State₁) firstInput := + { embedSecond _tm₀ _tm₁ firstCfg secondCfg with + state := secondCfg.state.map fun q => (.inr (.inr (.classify q boundary))) } + +/-- A first-phase boundary configuration with a chosen control state and intermediate head +position. -/ +def intermediateCfg + (_tm₀ : MultiTapeTM k₀ Symbol State₀) + (_tm₁ : MultiTapeTM k₁ Symbol State₁) + {input : List Symbol} + (cfg : Cfg k₀ Symbol State₀ input) + (state : CompositionState State₀ State₁) + (pos : ℤ) : + Cfg (compositionTapeCount k₀ k₁) Symbol (CompositionState State₀ State₁) input := + { embedFirst _tm₀ _tm₁ cfg with + state := some state + workTapePos := fun i => + if i.val = k₀ then pos + else (embedFirst _tm₀ _tm₁ cfg).workTapePos i } + +end Composition + +end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Composition/Layout.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Composition/Layout.lean new file mode 100644 index 000000000..5a7308f07 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Composition/Layout.lean @@ -0,0 +1,81 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Composition.Defs + +/-! # Relating the composition tape layout to injected work tapes -/ + +@[expose] public section + +namespace Turing.MultiTapeTM.Composition + +variable {k₀ k₁ : ℕ} {α : Type*} + +/-- Extending the output machine yields the first block and the middle tape. -/ +lemma extend_output (first : Fin k₀ → α) (middle : α) (second : Fin k₁ → α) + (dummyFirst : Fin k₀ → α) (dummyMiddle : α) : + ExtendTapes.extend (outputEmbedding k₀ k₁) (Fin.lastCases middle first) + (tapes dummyFirst dummyMiddle second) = tapes first middle second := by + funext i + refine Fin.addCases (fun j => ?_) (fun j => ?_) i + · change ExtendTapes.extend (outputEmbedding k₀ k₁) _ _ (outputEmbedding k₀ k₁ j) = _ + rw [ExtendTapes.extend_apply] + refine Fin.lastCases ?_ (fun j => ?_) j + · simp [tapes] + · simp [tapes] + · have hj : Fin.natAdd (k₀ + 1) j ∉ Set.range (outputEmbedding k₀ k₁) := by + rintro ⟨a, ha⟩ + have := congrArg Fin.val ha + simp only [outputEmbedding, Function.Embedding.coeFn_mk, + Fin.val_castAdd, Fin.val_natAdd] at this + omega + simp [ExtendTapes.extend, hj, tapes, show ¬k₀ + 1 + j.val < k₀ by omega, + show k₀ + 1 + j.val ≠ k₀ by omega] + +/-- Extending the input machine preserves the first block and fills the remaining tapes. -/ +lemma extend_input (first : Fin k₀ → α) (middle : α) (second : Fin k₁ → α) + (dummyMiddle : α) (dummySecond : Fin k₁ → α) : + ExtendTapes.extend (inputEmbedding k₀ k₁) (Fin.cases middle second) + (tapes first dummyMiddle dummySecond) = tapes first middle second := by + funext i + by_cases hi : i.val < k₀ + · have hn : i ∉ Set.range (inputEmbedding k₀ k₁) := by + rintro ⟨a, ha⟩ + have := congrArg Fin.val ha + change k₀ + a.val = i.val at this + omega + simp [ExtendTapes.extend, hn, tapes, hi] + · let j : Fin (k₁ + 1) := ⟨i.val - k₀, by + have := i.isLt + dsimp [compositionTapeCount] at * + omega⟩ + have hj : inputEmbedding k₀ k₁ j = i := + Fin.ext (by change k₀ + (i.val - k₀) = i.val; omega) + rw [← hj, ExtendTapes.extend_apply] + generalize j = a + refine Fin.cases ?_ (fun a => ?_) a + · simp [tapes] + · simp only [Fin.cases_succ, tapes, inputEmbedding_val, Fin.val_succ, + add_lt_iff_neg_left, not_lt_zero, ↓reduceDIte, Nat.add_eq_left, + Nat.add_eq_zero_iff, one_ne_zero, and_false] + congr 1 + apply Fin.ext + simp + omega + +/-- A constant frame supplies the unused second tape block. -/ +lemma extend_output_const (first : Fin k₀ → α) (middle d : α) : + ExtendTapes.extend (outputEmbedding k₀ k₁) (Fin.lastCases middle first) (fun _ => d) = + tapes first middle (fun _ => d) := by + have hconst : tapes (fun _ : Fin k₀ => d) d (fun _ : Fin k₁ => d) = (fun _ => d) := by + funext i + simp [tapes] + rw [← hconst] + exact extend_output first middle (fun _ => d) (fun _ => d) d + +end Turing.MultiTapeTM.Composition diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Composition/Rewind.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Composition/Rewind.lean new file mode 100644 index 000000000..2a41b4186 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Composition/Rewind.lean @@ -0,0 +1,152 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Composition.Simulation + +/-! # Assembling output redirection, rewind, and input substitution -/ + +@[expose] public section + +namespace Turing.MultiTapeTM.Composition + +variable {k₀ k₁ : ℕ} {Symbol State₀ State₁ : Type*} {input : List Symbol} +variable (tm₀ : MultiTapeTM k₀ Symbol State₀) (tm₁ : MultiTapeTM k₁ Symbol State₁) + +/-- Extend the output machine with the blank second-machine tape block. -/ +def outputLift (cfg : Cfg (k₀ + 1) Symbol State₀ input) := + ExtendTapes.embed (outputEmbedding k₀ k₁) cfg (fun _ _ => none) (fun _ => 0) + +@[simp] +lemma outputLift_embed (cfg : Cfg k₀ Symbol State₀ input) : + outputLift (k₁ := k₁) (OutputToWorkTape.embed cfg) = + ⟨cfg.state, cfg.inputPos, tapes cfg.workTapes (listTape cfg.output) (fun _ _ => none), + tapes cfg.workTapePos cfg.output.length (fun _ => 0), []⟩ := by + apply Cfg.ext <;> try rfl + · exact extend_output_const _ _ _ + · exact extend_output_const _ _ _ + +/-- The first phase is an output-redirection run followed by the generic sequential handoff. -/ +lemma embedFirst_eq (cfg : Cfg k₀ Symbol State₀ input) : + embedFirst tm₀ tm₁ cfg = + Sequential.left ((rewind (.work (compositionIntermediateTapeIdx k₀ k₁))).seq + (inputMachine k₀ tm₁)) (outputLift (OutputToWorkTape.embed cfg)) := by + rw [outputLift_embed] + cases hs : cfg.state <;> simp [embedFirst, hs, Sequential.left, seq, rewind, Cfg.withState] + +/-- Tape extension and output redirection commute with every native run. -/ +lemma runFrom_outputLift (cfg : Cfg k₀ Symbol State₀ input) (n : ℕ) : + (outputMachine tm₀ k₁).runFrom (outputLift (OutputToWorkTape.embed cfg)) n = + outputLift (OutputToWorkTape.embed (tm₀.runFrom cfg n)) := by + simp only [outputMachine, outputLift, ExtendTapes.runFrom_embed, OutputToWorkTape.runFrom_embed] + +/-- The first embedding takes initial configurations to initial configurations. -/ +lemma embedFirst_initCfg (input : List Symbol) : + embedFirst tm₀ tm₁ (tm₀.initCfg input) = (comp tm₀ tm₁).initCfg input := by + apply Cfg.ext <;> try rfl + · funext i p + cases p <;> simp [embedFirst, ite_apply, listTape] + · funext i + simp [embedFirst] + +/-- The first component runs up to its earliest halt. -/ +lemma runFrom_firstPhase (input : List Symbol) (n : ℕ) + (hactive : ∀ m < n, (tm₀.runFrom (tm₀.initCfg input) m).state ≠ none) : + (comp tm₀ tm₁).runFrom ((comp tm₀ tm₁).initCfg input) n = + embedFirst tm₀ tm₁ (tm₀.runFrom (tm₀.initCfg input) n) := by + rw [← embedFirst_initCfg, embedFirst_eq, comp, Sequential.runFrom_left] + · rw [runFrom_outputLift, ← embedFirst_eq] + · intro m hm + rw [runFrom_outputLift] + exact hactive m hm + +/-- Embed the generic rewind phase into the two nested sequential machines. -/ +def rewindLift (cfg : Cfg k₀ Symbol State₀ input) (q : Option RewindState) (pos : ℤ) : + Cfg (compositionTapeCount k₀ k₁) Symbol (CompositionState State₀ State₁) input := + Sequential.right (Sequential.left (inputMachine k₀ tm₁) + (Rewind.workCfg (outputLift (OutputToWorkTape.embed cfg)) + (compositionIntermediateTapeIdx k₀ k₁) q pos)) + +/-- A scanning rewind configuration has exactly the intermediate-tape layout. -/ +lemma rewindLift_scan (cfg : Cfg k₀ Symbol State₀ input) (pos : ℤ) : + rewindLift tm₁ cfg (some .scan) pos = + intermediateCfg tm₀ tm₁ cfg (.inr (.inl .scan)) pos := by + ext i z <;> + simp [rewindLift, Sequential.right, Sequential.left, Rewind.workCfg, Cfg.withState, + intermediateCfg, embedFirst, Function.update_apply, Fin.ext_iff] + +/-- The final rewind configuration enters the initial virtual-input classifier. -/ +lemma rewindLift_halt (cfg : Cfg k₀ Symbol State₀ input) : + rewindLift tm₁ cfg none 0 = + intermediateCfg tm₀ tm₁ cfg (.inr (.inr (.classify tm₁.q₀ .right))) 0 := by + ext i z <;> + simp [rewindLift, Sequential.right, Sequential.left, Rewind.workCfg, Cfg.withState, + inputMachine, extendTapes, inputFromWorkTape, + intermediateCfg, embedFirst, Function.update_apply, Fin.ext_iff] + +/-- The halt of the output machine starts the work-tape rewind at the end of its output. -/ +lemma embedFirst_halt (cfg : Cfg k₀ Symbol State₀ input) (hhalt : cfg.state = none) : + embedFirst tm₀ tm₁ cfg = rewindLift tm₁ cfg (some .start) cfg.output.length := by + ext i z <;> + simp [rewindLift, Sequential.right, Sequential.left, Rewind.workCfg, Cfg.withState, + embedFirst, hhalt, Function.update_apply, Fin.ext_iff] + split_ifs <;> simp_all + omega + +/-- The rewinding prefix is supplied by the standalone work-tape rewind theorem. -/ +lemma runFrom_firstHalt_rewind (cfg : Cfg k₀ Symbol State₀ input) (hhalt : cfg.state = none) + (r : ℕ) (hr : r ≤ cfg.output.length) : + (comp tm₀ tm₁).runFrom (embedFirst tm₀ tm₁ cfg) (r + 1) = + intermediateCfg tm₀ tm₁ cfg (.inr (.inl .scan)) (cfg.output.length - 1 - r) := by + rw [embedFirst_halt tm₀ tm₁ cfg hhalt, rewindLift, comp, Sequential.runFrom_right, + Sequential.runFrom_left] + · rw [runFrom_succ_eq_step, Rewind.step_work_start, + Rewind.runFrom_work_scan _ _ cfg.output (by simp) r hr] + exact rewindLift_scan tm₀ tm₁ cfg _ + · intro m hm + exact Rewind.work_active _ _ cfg.output (by simp) m (by omega) + +/-- The generic work-tape rewind ends at the initial classifier. -/ +lemma runFrom_firstHalt_classify (cfg : Cfg k₀ Symbol State₀ input) (hhalt : cfg.state = none) : + (comp tm₀ tm₁).runFrom (embedFirst tm₀ tm₁ cfg) (cfg.output.length + 2) = + intermediateCfg tm₀ tm₁ cfg (.inr (.inr (.classify tm₁.q₀ .right))) 0 := by + rw [embedFirst_halt tm₀ tm₁ cfg hhalt, rewindLift, comp, Sequential.runFrom_right, + Sequential.runFrom_left] + · rw [Rewind.runFrom_work _ _ cfg.output (by simp)] + exact rewindLift_halt tm₀ tm₁ cfg + · intro m hm + exact Rewind.work_active _ _ cfg.output (by simp) m hm + +/-- The rewound tape is the input-substitution machine's initial classifier configuration. -/ +lemma intermediateCfg_classify_init (cfg : Cfg k₀ Symbol State₀ input) : + intermediateCfg tm₀ tm₁ cfg (.inr (.inr (.classify tm₁.q₀ .right))) 0 = + classifyCfg tm₀ tm₁ cfg (tm₁.initCfg cfg.output) .right := by + ext i p <;> + simp [intermediateCfg, embedFirst, classifyCfg, embedSecond, InputFromWorkTape.virtualInputPos] + split_ifs <;> simp_all + omega + +/-- Output rewind and the initial classifier take the output length plus three steps. -/ +lemma runFrom_firstHalt_to_secondInit (cfg : Cfg k₀ Symbol State₀ input) + (hhalt : cfg.state = none) : + (comp tm₀ tm₁).runFrom (embedFirst tm₀ tm₁ cfg) (cfg.output.length + 3) = + embedSecond tm₀ tm₁ cfg (tm₁.initCfg cfg.output) := by + rw [runFrom_succ_eq_step', runFrom_firstHalt_classify tm₀ tm₁ cfg hhalt, + intermediateCfg_classify_init, step_classify_init] + +/-- The first run and output rewind establish the second machine's initial state. -/ +lemma runFrom_to_secondInit (input : List Symbol) (u : ℕ) + (hhalt : (tm₀.runFrom (tm₀.initCfg input) u).state = none) + (hactive : ∀ m < u, (tm₀.runFrom (tm₀.initCfg input) m).state ≠ none) : + (comp tm₀ tm₁).runFrom ((comp tm₀ tm₁).initCfg input) + (u + ((tm₀.runFrom (tm₀.initCfg input) u).output.length + 3)) = + embedSecond tm₀ tm₁ (tm₀.runFrom (tm₀.initCfg input) u) + (tm₁.initCfg (tm₀.runFrom (tm₀.initCfg input) u).output) := by + rw [runFrom_add, runFrom_firstPhase tm₀ tm₁ input u hactive, + runFrom_firstHalt_to_secondInit tm₀ tm₁ _ hhalt] + +end Turing.MultiTapeTM.Composition diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Composition/Simulation.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Composition/Simulation.lean new file mode 100644 index 000000000..af225c75c --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Composition/Simulation.lean @@ -0,0 +1,86 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Composition.Layout + +/-! # Lifting the generic virtual-input simulation into composition -/ + +@[expose] public section + +namespace Turing.MultiTapeTM.Composition + +variable {k₀ k₁ : ℕ} {Symbol State₀ State₁ : Type*} +variable (tm₀ : MultiTapeTM k₀ Symbol State₀) (tm₁ : MultiTapeTM k₁ Symbol State₁) +variable {firstInput secondInput : List Symbol} + +/-- Extend a virtual-input configuration while retaining the first machine's tapes. -/ +def inputLift (firstCfg : Cfg k₀ Symbol State₀ firstInput) + (cfg : Cfg (k₁ + 1) Symbol (InputState State₁) firstInput) := + ExtendTapes.embed (inputEmbedding k₀ k₁) cfg + (tapes firstCfg.workTapes (fun _ => none) (fun _ _ => none)) + (tapes firstCfg.workTapePos 0 (fun _ => 0)) + +/-- The second-phase embedding is tape extension followed by two sequential state embeddings. -/ +lemma embedSecond_eq (firstCfg : Cfg k₀ Symbol State₀ firstInput) + (cfg : Cfg k₁ Symbol State₁ secondInput) : + embedSecond tm₀ tm₁ firstCfg cfg = + Sequential.right (Sequential.right + (inputLift firstCfg (InputFromWorkTape.embed firstCfg.inputPos cfg))) := by + apply Cfg.ext + · cases hs : cfg.state <;> + simp [embedSecond, Sequential.right, Cfg.withState, inputLift, ExtendTapes.embed, + InputFromWorkTape.embed, hs] + · rfl + · exact (extend_input _ _ _ _ _).symm + · exact (extend_input _ _ _ _ _).symm + · rfl + +/-- The classifier embedding has the same tape extension. -/ +lemma classifyCfg_eq (firstCfg : Cfg k₀ Symbol State₀ firstInput) + (cfg : Cfg k₁ Symbol State₁ secondInput) (boundary : InputBoundary) : + classifyCfg tm₀ tm₁ firstCfg cfg boundary = + Sequential.right (Sequential.right + (inputLift firstCfg (InputFromWorkTape.classifyCfg firstCfg.inputPos cfg boundary))) := by + apply Cfg.ext + · cases hs : cfg.state <;> + simp [embedSecond, classifyCfg, Sequential.right, Cfg.withState, inputLift, + ExtendTapes.embed, InputFromWorkTape.embed, InputFromWorkTape.classifyCfg, hs] + · rfl + · exact (extend_input _ _ _ _ _).symm + · exact (extend_input _ _ _ _ _).symm + · rfl + +/-- Simulation of the second machine, at two composite steps per native step. -/ +lemma runFrom_secondPhase (firstCfg : Cfg k₀ Symbol State₀ firstInput) + (cfg : Cfg k₁ Symbol State₁ secondInput) (n : ℕ) : + (comp tm₀ tm₁).runFrom (embedSecond tm₀ tm₁ firstCfg cfg) (2 * n) = + embedSecond tm₀ tm₁ firstCfg (tm₁.runFrom cfg n) := by + rw [embedSecond_eq, comp, Sequential.runFrom_right, Sequential.runFrom_right] + simp only [inputMachine, inputLift, ExtendTapes.runFrom_embed, InputFromWorkTape.runFrom_embed] + exact (embedSecond_eq tm₀ tm₁ firstCfg _).symm + +/-- Odd composite steps are the intermediate classifier configurations of the input substitution. -/ +lemma runFrom_secondPhase_odd (firstCfg : Cfg k₀ Symbol State₀ firstInput) + (cfg : Cfg k₁ Symbol State₁ secondInput) (n : ℕ) : + ∃ boundary, (comp tm₀ tm₁).runFrom (embedSecond tm₀ tm₁ firstCfg cfg) (2 * n + 1) = + classifyCfg tm₀ tm₁ firstCfg (tm₁.runFrom cfg (n + 1)) boundary := by + obtain ⟨boundary, h⟩ := InputFromWorkTape.runFrom_odd tm₁ firstCfg.inputPos cfg n + refine ⟨boundary, ?_⟩ + rw [embedSecond_eq, comp, Sequential.runFrom_right, Sequential.runFrom_right] + simp only [inputMachine, inputLift, ExtendTapes.runFrom_embed, h] + exact (classifyCfg_eq tm₀ tm₁ firstCfg _ boundary).symm + +/-- The initial classifier establishes the second machine's native initial configuration. -/ +lemma step_classify_init (firstCfg : Cfg k₀ Symbol State₀ firstInput) : + (comp tm₀ tm₁).step (classifyCfg tm₀ tm₁ firstCfg (tm₁.initCfg firstCfg.output) .right) = + embedSecond tm₀ tm₁ firstCfg (tm₁.initCfg firstCfg.output) := by + rw [classifyCfg_eq, comp, Sequential.step_right, Sequential.step_right] + simp only [inputMachine, inputLift, ExtendTapes.step_embed, InputFromWorkTape.step_init] + exact (embedSecond_eq tm₀ tm₁ firstCfg _).symm + +end Turing.MultiTapeTM.Composition diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ExtendTapes.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ExtendTapes.lean new file mode 100644 index 000000000..f9a5ad304 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ExtendTapes.lean @@ -0,0 +1,137 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic +public import Mathlib.Data.Fintype.Inv +public import Mathlib.Data.Fintype.Card + +/-! +# Extending and reindexing work tapes + +`extendTapes` embeds a machine's work tapes along an injection. The extra tapes are idle, and each +native step still takes exactly one step. The configuration embedding permits arbitrary contents +and head positions on the extra tapes, so the transformation also applies to intermediate runs. +-/ + +@[expose] public section + +namespace Turing.MultiTapeTM + +variable {k k' : ℕ} {Symbol State : Type*} {input : List Symbol} + +namespace ExtendTapes + +/-- Extend a tape-indexed family along an injection, using `extra` outside its image. -/ +def extend {α : Type*} (e : Fin k ↪ Fin k') (values : Fin k → α) (extra : Fin k' → α) + (j : Fin k') : α := + if h : j ∈ Set.range e then values (e.invOfMemRange ⟨j, h⟩) else extra j + +@[simp] +lemma extend_apply {α : Type*} (e : Fin k ↪ Fin k') (values : Fin k → α) + (extra : Fin k' → α) (i : Fin k) : extend e values extra (e i) = values i := by + simp [extend] + +/-- Embed a native configuration while retaining arbitrary data on the unused tapes. -/ +def embed (e : Fin k ↪ Fin k') (cfg : Cfg k Symbol State input) + (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) : + Cfg k' Symbol State input where + state := cfg.state + inputPos := cfg.inputPos + workTapes := extend e cfg.workTapes extraTapes + workTapePos := extend e cfg.workTapePos extraPos + output := cfg.output + +end ExtendTapes + +/-- Relabel the work tapes by an injection, leaving every tape outside its image idle. -/ +def extendTapes (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') : + MultiTapeTM k' Symbol State where + q₀ := tm.q₀ + tr q input work := + let out := tm.tr q input (work ∘ e) + ⟨out.inputMove, ExtendTapes.extend e out.workActions (fun _ => (none, 0)), out.outS, out.q'⟩ + +namespace ExtendTapes + +variable (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') +variable (cfg : Cfg k Symbol State input) +variable (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) + +/-- Tape extension preserves a step and every unused tape. -/ +lemma step_embed : + (tm.extendTapes e).step (embed e cfg extraTapes extraPos) = + embed e (tm.step cfg) extraTapes extraPos := by + have hwork : (embed e cfg extraTapes extraPos).workTapeSymbols ∘ e = cfg.workTapeSymbols := by + funext i + simp [embed, Cfg.workTapeSymbols] + cases hs : cfg.state with + | none => simp [step, embed, hs] + | some q => + simp only [step, embed, hs, extendTapes, Cfg.inputSymbol] at hwork ⊢ + rw [hwork] + apply Cfg.ext <;> try rfl + · funext j p + by_cases hj : j ∈ Set.range e + · obtain ⟨i, rfl⟩ := hj + simp only [extend_apply] + · simp [extend, hj] + · funext j + by_cases hj : j ∈ Set.range e + · obtain ⟨i, rfl⟩ := hj + simp only [extend_apply] + · simp [extend, hj] + +/-- Extending the tape count does not change the execution time. -/ +lemma runFrom_embed (n : ℕ) : + (tm.extendTapes e).runFrom (embed e cfg extraTapes extraPos) n = + embed e (tm.runFrom cfg n) extraTapes extraPos := by + induction n with + | zero => rfl + | succ n ih => rw [runFrom_succ_eq_step', ih, step_embed, runFrom_succ_eq_step'] + +/-- An injected tape visits exactly the native tape's positions. -/ +lemma spaceUsedByTape_embed (n : ℕ) (i : Fin k) : + (tm.extendTapes e).spaceUsedByTape (embed e cfg extraTapes extraPos) n (e i) = + tm.spaceUsedByTape cfg n i := by + simp only [spaceUsedByTape, visitedByTapeHead, runFrom_embed] + simp only [embed, extend_apply] + +/-- An unused tape visits just its initial cell. -/ +lemma spaceUsedByTape_extra (n : ℕ) (j : Fin k') (hj : j ∉ Set.range e) : + (tm.extendTapes e).spaceUsedByTape (embed e cfg extraTapes extraPos) n j = 1 := by + simp only [spaceUsedByTape, visitedByTapeHead, runFrom_embed] + simp [embed, extend, hj, Finset.image_const] + +/-- The extra space is exactly one visited cell for each unused tape. -/ +lemma spaceUsed_embed (n : ℕ) : + (tm.extendTapes e).spaceUsed (embed e cfg extraTapes extraPos) n = + tm.spaceUsed cfg n + (k' - k) := by + unfold spaceUsed + rw [← Finset.sum_add_sum_compl (Finset.univ.map e)] + congr 1 + · simp [Finset.sum_map, spaceUsedByTape_embed] + · calc + _ = ∑ j ∈ (Finset.univ.map e)ᶜ, 1 := by + apply Finset.sum_congr rfl + intro j hj + exact spaceUsedByTape_extra tm e cfg extraTapes extraPos n j (by simpa using hj) + _ = k' - k := by simp [Finset.card_compl] + +end ExtendTapes + +/-- Starting with blank work tapes commutes with tape extension. -/ +lemma runFrom_extendTapes (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') + (input : List Symbol) (n : ℕ) : + (tm.extendTapes e).runFrom ((tm.extendTapes e).initCfg input) n = + ExtendTapes.embed e (tm.runFrom (tm.initCfg input) n) (fun _ _ => none) (fun _ => 0) := by + have hinit : (tm.extendTapes e).initCfg input = + ExtendTapes.embed e (tm.initCfg input) (fun _ _ => none) (fun _ => 0) := by + ext i p <;> simp [ExtendTapes.embed, ExtendTapes.extend, extendTapes] + rw [hinit, ExtendTapes.runFrom_embed] + +end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/InputFromWorkTape.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/InputFromWorkTape.lean new file mode 100644 index 000000000..4c25c63fe --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/InputFromWorkTape.lean @@ -0,0 +1,214 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.InputFromWorkTape.Defs + +/-! # Correctness of work-tape input substitution -/ + +@[expose] public section + +namespace Turing.MultiTapeTM.InputFromWorkTape + +variable {k : ℕ} {Symbol State : Type*} +variable (tm : MultiTapeTM k Symbol State) +variable {outerInput input : List Symbol} (p : Fin (outerInput.length + 2)) + +/-- The virtual work-tape position follows the clamped native input-head movement. -/ +private lemma virtualInputPos_move {input : List Symbol} + (p : Fin (input.length + 2)) (move : SignType) : + virtualInputPos (moveInputPos p move) = + virtualInputPos p + (inputMode p).move move := by + cases move with + | zero => simp [InputMode.move] + | neg => + by_cases hleft : p = 0 + · rw [hleft] + simp [inputMode, InputMode.move] + · rw [moveInputPos_neg_of_ne_left p hleft] + unfold virtualInputPos + have hp : 0 < p.val := Nat.pos_of_ne_zero (fun hz => hleft (Fin.ext hz)) + by_cases hright : p.val = input.length + 1 <;> + simp [inputMode, hleft, hright, InputMode.move] <;> omega + | pos => + by_cases hright : p.val = input.length + 1 + · have hp : p = ⟨input.length + 1, by omega⟩ := Fin.ext hright + rw [hp] + simp [inputMode, InputMode.move] + · rw [moveInputPos_pos_of_ne_right p hright] + unfold virtualInputPos + by_cases hleft : p = 0 <;> + simp [inputMode, hleft, hright, InputMode.move] + +/-- The boundary hint selected before a move is left whenever the resulting native position is +the left boundary. -/ +private lemma nextBoundary_eq_left {input : List Symbol} + (p : Fin (input.length + 2)) (move : SignType) + (hmove : moveInputPos p move = 0) : + (inputMode p).nextBoundary move = .left := by + cases move <;> + simp_all [inputMode, InputMode.nextBoundary, moveInputPos] + split_ifs at hmove <;> simp_all + +/-- The boundary hint selected before a move is right whenever the resulting native position is +the right boundary. -/ +private lemma nextBoundary_eq_right {input : List Symbol} + (p : Fin (input.length + 2)) (move : SignType) + (hmove : (moveInputPos p move).val = input.length + 1) : + (inputMode p).nextBoundary move = .right := by + cases move <;> + simp_all [inputMode, InputMode.nextBoundary, moveInputPos] <;> + split_ifs at * <;> simp_all <;> omega + +/-- Classifying the canonical intermediate tape recovers a native input-head mode, provided the +boundary hint agrees at the two blank boundary cells. -/ +private lemma classifyInput_listTape {input : List Symbol} + (p : Fin (input.length + 2)) (boundary : InputBoundary) + (hleft : p = 0 → boundary = .left) + (hright : p.val = input.length + 1 → boundary = .right) : + classifyInput + (listTape input (virtualInputPos p)) boundary = + inputMode p := by + by_cases hp0 : p = 0 + · simp [hp0, hleft hp0, virtualInputPos, inputMode, + classifyInput, InputBoundary.inputMode, listTape] + rfl + · by_cases hpr : p.val = input.length + 1 + · simp [virtualInputPos, hpr, hright hpr, inputMode, hp0, + classifyInput, InputBoundary.inputMode] + · have hp : 0 < p.val := Nat.pos_of_ne_zero (fun hz => hp0 (Fin.ext hz)) + have hi : p.val - 1 < input.length := by omega + have hv : virtualInputPos p = (p.val - 1 : ℕ) := by + unfold virtualInputPos + omega + simp [hv, classifyInput, inputMode, hp0, hpr, hi] + +/-- Classifying the intermediate cell reached by a virtual move recovers the native clamped +input-head mode after that move. -/ +private lemma classifyInput_move {input : List Symbol} + (p : Fin (input.length + 2)) (move : SignType) : + classifyInput + (listTape input + (virtualInputPos p + (inputMode p).move move)) + ((inputMode p).nextBoundary move) = + inputMode (moveInputPos p move) := by + rw [← virtualInputPos_move p move] + apply classifyInput_listTape + · exact nextBoundary_eq_left p move + · exact nextBoundary_eq_right p move + + +/-- The simulated input symbol is exactly the symbol on the virtual tape. -/ +private lemma embed_inputSymbol (cfg : Cfg k Symbol State input) : + (if inputMode cfg.inputPos = .inside then (embed p cfg).workTapeSymbols 0 else none) = + cfg.inputSymbol := by + simp only [Cfg.workTapeSymbols, embed, Fin.cases_zero] + by_cases hleft : cfg.inputPos = 0 + · simp [inputMode, hleft, Cfg.inputSymbol] + · by_cases hright : cfg.inputPos.val = input.length + 1 + · simp [inputMode, hleft, hright, Cfg.inputSymbol] + · have hp : 0 < cfg.inputPos.val := Nat.pos_of_ne_zero (fun hz => hleft (Fin.ext hz)) + have hi : cfg.inputPos.val - 1 < input.length := by omega + have hv : virtualInputPos cfg.inputPos = (cfg.inputPos.val - 1 : ℕ) := by + unfold virtualInputPos + omega + rw [inputSymbolInner (p := cfg.inputPos.val - 1) (by omega) hi] + simp [inputMode, hleft, hright, hv, listTape, hi] + +/-- Classification restores the native boundary mode and changes no tapes. -/ +lemma step_classifyCfg (cfg : Cfg k Symbol State input) (boundary : InputBoundary) + (hmode : classifyInput (listTape input (virtualInputPos cfg.inputPos)) boundary = + inputMode cfg.inputPos) : + tm.inputFromWorkTape.step (classifyCfg p cfg boundary) = embed p cfg := by + cases hs : cfg.state with + | none => simp [step, classifyCfg, embed, hs] + | some q => + ext i z <;> + simp [step, classifyCfg, embed, inputFromWorkTape, hs, Cfg.workTapeSymbols, hmode] + +/-- The moving half of a simulated step performs the native tape actions. -/ +lemma step_embed (cfg : Cfg k Symbol State input) (q : State) (hs : cfg.state = some q) : + tm.inputFromWorkTape.step (embed p cfg) = + classifyCfg p (tm.step cfg) + ((inputMode cfg.inputPos).nextBoundary + (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).inputMove) := by + have hwork : (fun i : Fin k => (embed p cfg).workTapeSymbols i.succ) = cfg.workTapeSymbols := by + funext i + simp [embed, Cfg.workTapeSymbols] + unfold step + rw [show (embed p cfg).state = some (.run q (inputMode cfg.inputPos)) by + simp [embed, hs], hs] + simp only [inputFromWorkTape] + rw [embed_inputSymbol p cfg, hwork] + generalize htr : tm.tr q cfg.inputSymbol cfg.workTapeSymbols = out + simp only [htr] + apply Cfg.ext + · rfl + · simp [classifyCfg, embed] + · funext i z + refine Fin.cases ?_ (fun j => ?_) i + · simp [classifyCfg, embed] + · cases hw : (out.workActions j).1 <;> simp [classifyCfg, embed, hw] + · funext i + refine Fin.cases ?_ (fun j => ?_) i + · simpa [classifyCfg, embed] using (virtualInputPos_move cfg.inputPos out.inputMove).symm + · simp [classifyCfg, embed] + · rfl + +/-- Every native step is simulated in two steps, including after a native halt. -/ +lemma runFrom_two (cfg : Cfg k Symbol State input) : + tm.inputFromWorkTape.runFrom (embed p cfg) 2 = embed p (tm.step cfg) := by + cases hs : cfg.state with + | none => simp [runFrom, step, embed, hs] + | some q => + change tm.inputFromWorkTape.step (tm.inputFromWorkTape.step (embed p cfg)) = _ + rw [step_embed tm p cfg q hs] + apply step_classifyCfg + simpa only [step, hs, virtualInputPos_move] using + classifyInput_move cfg.inputPos (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).inputMove + +/-- The native run is simulated on a work tape with a factor of two in time. -/ +lemma runFrom_embed (cfg : Cfg k Symbol State input) (n : ℕ) : + tm.inputFromWorkTape.runFrom (embed p cfg) (2 * n) = embed p (tm.runFrom cfg n) := by + induction n with + | zero => rfl + | succ n ih => + rw [show 2 * (n + 1) = 2 * n + 2 by omega, runFrom_add, ih, + runFrom_two, runFrom_succ_eq_step'] + +/-- Odd simulation steps are classifier configurations. -/ +lemma runFrom_odd (cfg : Cfg k Symbol State input) (n : ℕ) : + ∃ boundary, tm.inputFromWorkTape.runFrom (embed p cfg) (2 * n + 1) = + classifyCfg p (tm.runFrom cfg (n + 1)) boundary := by + rw [runFrom_add, runFrom_embed] + cases hs : (tm.runFrom cfg n).state with + | none => + refine ⟨.right, ?_⟩ + change tm.inputFromWorkTape.step (embed p (tm.runFrom cfg n)) = _ + rw [runFrom_succ_eq_step', step_of_halt hs] + simp [step, embed, classifyCfg, hs] + | some q => + refine ⟨(inputMode (tm.runFrom cfg n).inputPos).nextBoundary + (tm.tr q (tm.runFrom cfg n).inputSymbol (tm.runFrom cfg n).workTapeSymbols).inputMove, ?_⟩ + change tm.inputFromWorkTape.step (embed p (tm.runFrom cfg n)) = _ + rw [step_embed tm p _ q hs, runFrom_succ_eq_step'] + +/-- The initial classifier enters the native initial configuration, also for empty input. -/ +lemma step_init : + tm.inputFromWorkTape.step (classifyCfg p (tm.initCfg input) .right) = + embed p (tm.initCfg input) := by + apply step_classifyCfg + cases input <;> + simp [classifyInput, inputMode, virtualInputPos, InputBoundary.inputMode, listTape] + +/-- A prepared work tape can replace the native input at any real input position. -/ +lemma runFrom_init (n : ℕ) : + tm.inputFromWorkTape.runFrom (classifyCfg p (tm.initCfg input) .right) (2 * n + 1) = + embed p (tm.runFrom (tm.initCfg input) n) := by + rw [runFrom_succ_eq_step, step_init, runFrom_embed] + +end Turing.MultiTapeTM.InputFromWorkTape diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/InputFromWorkTape/Defs.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/InputFromWorkTape/Defs.lean new file mode 100644 index 000000000..8ed771279 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/InputFromWorkTape/Defs.lean @@ -0,0 +1,126 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Mathlib.Data.Fintype.Prod +public import Mathlib.Data.Fintype.Sum +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.TapeContents +public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic + +/-! +# Substituting a work tape for the input tape + +The first work tape contains the virtual input. The remaining tapes are the native work tapes. +A classifier distinguishes the two blank boundaries, preserving native head clamping without +extending the alphabet. One native step takes two steps, and the real input head stays parked. +-/ + +@[expose] public section + +namespace Turing.MultiTapeTM + +variable {k : ℕ} {Symbol State : Type*} + +/-- Location of the virtual input head during the second phase. -/ +inductive InputMode + | left + | inside + | right +deriving DecidableEq + +instance : Finite InputMode := + Finite.of_injective (fun | .left => (0 : Fin 3) | .inside => 1 | .right => 2) + (by intro a b h; cases a <;> cases b <;> simp_all) + +/-- Boundary toward which a virtual input-head move was made. -/ +inductive InputBoundary + | left + | right + +instance : Finite InputBoundary := + Finite.of_injective (fun | .left => true | .right => false) + (by intro a b h; cases a <;> cases b <;> simp_all) + +/-- Movement of the virtual input head, with outward boundary moves clamped. -/ +def InputMode.move : InputMode → SignType → SignType + | .left, .neg => 0 + | .right, .pos => 0 + | _, move => move + +/-- Boundary to use if the cell reached by a virtual input-head move is blank. -/ +def InputMode.nextBoundary : + InputMode → SignType → InputBoundary + | _, .neg | .left, .zero => .left + | _, _ => .right + +/-- Convert a boundary classifier result to an input mode. -/ +def InputBoundary.inputMode : InputBoundary → InputMode + | .left => .left + | .right => .right + +/-- Control state for the work-tape input simulation. -/ +inductive InputState (State : Type*) + | run (q : State) (mode : InputMode) + | classify (q : State) (boundary : InputBoundary) + +instance [Finite State] : Finite (InputState State) := by + let := Fintype.ofFinite State + let := Fintype.ofFinite InputMode + let := Fintype.ofFinite InputBoundary + apply Finite.of_injective (fun s : InputState State => match s with + | .run q mode => ((q, Sum.inl mode) : State × (InputMode ⊕ InputBoundary)) + | .classify q boundary => (q, Sum.inr boundary)) + intro a b h + cases a <;> cases b <;> simp_all + +/-- Classify the cell reached after a virtual input-head movement. -/ +def classifyInput (cell : Option Symbol) (boundary : InputBoundary) : InputMode := + if cell.isSome then .inside else boundary.inputMode + +/-- Use the first work tape as input, and shift native work tapes one index to the right. +The virtual head starts at cell zero; classification also handles empty input. -/ +def inputFromWorkTape (tm : MultiTapeTM k Symbol State) : + MultiTapeTM (k + 1) Symbol (InputState State) where + q₀ := .classify tm.q₀ .right + tr q _ work := match q with + | .run q mode => + let out := tm.tr q (if mode = .inside then work 0 else none) (fun i => work i.succ) + ⟨0, Fin.cases (none, mode.move out.inputMove) out.workActions, out.outS, + out.q'.map fun q => .classify q (mode.nextBoundary out.inputMove)⟩ + | .classify q boundary => + ⟨0, fun _ => (none, 0), none, some (.run q (classifyInput (work 0) boundary))⟩ + +namespace InputFromWorkTape + +/-- View a native input-head position as a position on the intermediate work tape. -/ +def virtualInputPos {input : List Symbol} (p : Fin (input.length + 2)) : ℤ := + p.val - 1 + +/-- Classify a native input-head position as the left boundary, an input cell, or the right +boundary. -/ +def inputMode {input : List Symbol} + (p : Fin (input.length + 2)) : InputMode := + if p = 0 then .left else if p.val = input.length + 1 then .right else .inside + +/-- Embed a native configuration while parking the real input head at `p`. -/ +def embed {outerInput input : List Symbol} (p : Fin (outerInput.length + 2)) + (cfg : Cfg k Symbol State input) : Cfg (k + 1) Symbol (InputState State) outerInput where + state := cfg.state.map fun q => .run q (inputMode cfg.inputPos) + inputPos := p + workTapes := Fin.cases (listTape input) cfg.workTapes + workTapePos := Fin.cases (virtualInputPos cfg.inputPos) cfg.workTapePos + output := cfg.output + +/-- The classifier configuration between the two halves of a simulated step. -/ +def classifyCfg {outerInput input : List Symbol} (p : Fin (outerInput.length + 2)) + (cfg : Cfg k Symbol State input) (boundary : InputBoundary) : + Cfg (k + 1) Symbol (InputState State) outerInput := + { embed p cfg with state := cfg.state.map fun q => .classify q boundary } + +end InputFromWorkTape + +end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/OutputToWorkTape.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/OutputToWorkTape.lean new file mode 100644 index 000000000..c523f53fe --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/OutputToWorkTape.lean @@ -0,0 +1,95 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.TapeContents +public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic + +/-! +# Redirecting output to a fresh work tape + +`outputToWorkTape` adds one work tape, at index `Fin.last k`, and writes the native output there. +Its head stays immediately after the output. The original work tapes and native input head follow +the original machine exactly; the external output is empty. +-/ + +@[expose] public section + +namespace Turing.MultiTapeTM + +variable {k : ℕ} {Symbol State : Type*} {input : List Symbol} + +/-- Redirect output to a new last work tape without changing the alphabet or control states. -/ +def outputToWorkTape (tm : MultiTapeTM k Symbol State) : MultiTapeTM (k + 1) Symbol State where + q₀ := tm.q₀ + tr q input work := + let out := tm.tr q input (fun i => work i.castSucc) + ⟨out.inputMove, + Fin.lastCases (out.outS.elim (none, 0) (fun s => (some (some s), 1))) out.workActions, + none, out.q'⟩ + +namespace OutputToWorkTape + +/-- Represent a native configuration with its output on the new tape. -/ +def embed (cfg : Cfg k Symbol State input) : Cfg (k + 1) Symbol State input where + state := cfg.state + inputPos := cfg.inputPos + workTapes := Fin.lastCases (listTape cfg.output) cfg.workTapes + workTapePos := Fin.lastCases cfg.output.length cfg.workTapePos + output := [] + +variable (tm : MultiTapeTM k Symbol State) + +/-- Each original transition is one transition of the output-redirected machine. -/ +lemma step_embed (cfg : Cfg k Symbol State input) : + tm.outputToWorkTape.step (embed cfg) = embed (tm.step cfg) := by + have hwork : (fun i : Fin k => (embed cfg).workTapeSymbols i.castSucc) = cfg.workTapeSymbols := by + funext i + simp [embed, Cfg.workTapeSymbols] + cases hs : cfg.state with + | none => simp [step, embed, hs] + | some q => + unfold step + rw [show (embed cfg).state = some q from hs, hs] + simp only [outputToWorkTape] + rw [show (embed cfg).inputSymbol = cfg.inputSymbol from rfl, hwork] + generalize htr : tm.tr q cfg.inputSymbol cfg.workTapeSymbols = out + simp only [htr] + apply Cfg.ext <;> try rfl + · funext i p + refine Fin.lastCases ?_ (fun j => ?_) i + · cases out.outS <;> simp [embed, listTape_append_single] + · cases hw : (out.workActions j).1 <;> simp [embed, hw] + · funext i + refine Fin.lastCases ?_ (fun j => ?_) i + · cases out.outS <;> simp [embed] + · simp [embed] + +/-- Output redirection preserves arbitrary runs, including padded halting times. -/ +lemma runFrom_embed (cfg : Cfg k Symbol State input) (n : ℕ) : + tm.outputToWorkTape.runFrom (embed cfg) n = embed (tm.runFrom cfg n) := by + induction n with + | zero => rfl + | succ n ih => rw [runFrom_succ_eq_step', ih, step_embed, runFrom_succ_eq_step'] + +end OutputToWorkTape + +/-- The output-redirected machine simulates an ordinary run starting with blank work tapes. -/ +lemma runFrom_outputToWorkTape (tm : MultiTapeTM k Symbol State) (input : List Symbol) (n : ℕ) : + tm.outputToWorkTape.runFrom (tm.outputToWorkTape.initCfg input) n = + OutputToWorkTape.embed (tm.runFrom (tm.initCfg input) n) := by + have hinit : tm.outputToWorkTape.initCfg input = OutputToWorkTape.embed (tm.initCfg input) := by + apply Cfg.ext <;> try rfl + · funext i p + refine Fin.lastCases ?_ (fun j => ?_) i + · cases p <;> simp [OutputToWorkTape.embed, listTape] + · simp [OutputToWorkTape.embed] + · funext i + refine Fin.lastCases ?_ (fun j => ?_) i <;> simp [OutputToWorkTape.embed] + rw [hinit, OutputToWorkTape.runFrom_embed] + +end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/README.md b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/README.md new file mode 100644 index 000000000..06315ebfd --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/README.md @@ -0,0 +1,20 @@ +# Machine transformations + +These modules describe executable machines and their effects on configurations and `runFrom`. + +- `Basic` changes a configuration's control state without changing its tapes. +- `Sequential` runs machines with the same work-tape count consecutively. The first halting + transition hands its tapes, head positions, and accumulated output to the second machine. +- `ExtendTapes` places a machine's tapes along any injection. Time is unchanged; each unused tape + contributes one visited cell to space. Arbitrary data on unused tapes is preserved. +- `OutputToWorkTape` redirects output to one fresh tape, including the symbol on a halting step. +- `InputFromWorkTape` simulates the native input on a work tape, preserving boundary clamping. +- `Rewind` shares one controller between native-input and work-tape rewinding. Work-tape rewind + starts immediately after contiguous contents and finishes at their first cell, including when empty. +- `Composition` assembles output redirection, work-tape rewind, and input substitution with `seq` + and tape injections, then proves operational and resource bounds. + +These machines preserve the alphabet. Their run statements also specify the intermediate states +and tape contents needed when using them inside larger machines. Function-level complexity +statements belong in [Combinators](../Combinators); halting normal forms belong in +[NormalForms](../NormalForms). diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Rewind.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Rewind.lean new file mode 100644 index 000000000..e2bc0d968 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Rewind.lean @@ -0,0 +1,177 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.TapeContents +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Basic + +/-! +# Rewinding a tape + +One controller rewinds either the native input head or a selected work-tape head. It first moves +left, scans left through nonblank cells, then moves right and halts. The initial left move handles +a head starting on the right blank boundary, including when the contents are empty. +-/ + +@[expose] public section + +namespace Turing.MultiTapeTM + +variable {k : ℕ} {Symbol State : Type*} {input : List Symbol} + +/-- The head operated by a rewind machine. -/ +inductive RewindHead (k : ℕ) + | input + | work (i : Fin k) + +/-- Enter the contents before scanning for the left blank boundary. -/ +inductive RewindState + | start + | scan + +instance : Finite RewindState := + Finite.of_injective (fun | .start => true | .scan => false) + (by intro a b h; cases a <;> cases b <;> simp_all) + +/-- Rewind the selected head, retaining all tape contents and accumulated output. -/ +def rewind (head : RewindHead k) : MultiTapeTM k Symbol RewindState where + q₀ := .start + tr q input work := + let cell := match head with | .input => input | .work i => work i + let done := match q with | .start => false | .scan => !cell.isSome + let move : SignType := if done then 1 else -1 + ⟨(match head with | .input => move | .work _ => 0), + (fun i => (none, match head with + | .input => 0 + | .work j => if i = j then move else 0)), + none, if done then none else some .scan⟩ + +namespace Rewind + +/-- A rewind configuration at a specified work-tape position. -/ +def workCfg (cfg : Cfg k Symbol State input) (i : Fin k) + (q : Option RewindState) (p : ℤ) : Cfg k Symbol RewindState input := + { cfg.withState q with workTapePos := Function.update cfg.workTapePos i p } + +/-- A rewind configuration at a specified native input position. -/ +def inputCfg (cfg : Cfg k Symbol State input) + (q : Option RewindState) (p : Fin (input.length + 2)) : Cfg k Symbol RewindState input := + { cfg.withState q with inputPos := p } + +/-- The initial work-tape move enters the contents from their right boundary. -/ +lemma step_work_start (cfg : Cfg k Symbol State input) (i : Fin k) (p : ℤ) : + (rewind (.work i)).step (workCfg cfg i (some .start) p) = + workCfg cfg i (some .scan) (p - 1) := by + ext j z <;> simp [step, rewind, workCfg, Cfg.withState, Function.update_apply, sub_eq_add_neg] + split_ifs <;> simp_all + +/-- Scanning a nonblank work-tape cell moves one position left. -/ +lemma step_work_scan (cfg : Cfg k Symbol State input) (i : Fin k) (p : ℤ) + (h : (cfg.workTapes i p).isSome) : + (rewind (.work i)).step (workCfg cfg i (some .scan) p) = + workCfg cfg i (some .scan) (p - 1) := by + have hn := Option.isSome_iff_ne_none.mp h + ext j z <;> + simp [step, rewind, workCfg, Cfg.withState, Cfg.workTapeSymbols, hn, + Function.update_apply, sub_eq_add_neg] + split_ifs <;> simp_all + +/-- Scanning blank finishes with the head one position to its right. -/ +lemma step_work_stop (cfg : Cfg k Symbol State input) (i : Fin k) (p : ℤ) + (h : cfg.workTapes i p = none) : + (rewind (.work i)).step (workCfg cfg i (some .scan) p) = workCfg cfg i none (p + 1) := by + ext j z <;> + simp [step, rewind, workCfg, Cfg.withState, Cfg.workTapeSymbols, h, Function.update_apply] + split_ifs <;> simp_all + +/-- Every prefix of a work-tape rewind traverses exactly the occupied suffix. -/ +lemma runFrom_work_scan (cfg : Cfg k Symbol State input) (i : Fin k) (xs : List Symbol) + (htape : cfg.workTapes i = listTape xs) (r : ℕ) (hr : r ≤ xs.length) : + (rewind (.work i)).runFrom (workCfg cfg i (some .scan) (xs.length - 1)) r = + workCfg cfg i (some .scan) (xs.length - 1 - r) := by + have hstep (s : ℕ) (hs : s < r) := step_work_scan cfg i (xs.length - 1 - s) + (by rw [htape]; exact listTape_isSome xs (by omega) (by omega)) + convert runFrom_eq_of_step (rewind (.work i)) + (fun s => workCfg cfg i (some .scan) (xs.length - 1 - s)) r (fun s hs => ?_) using 1 + · simp + · convert hstep s hs using 1 + congr 1 + omega + +/-- Rewind contiguous work-tape contents from the blank cell immediately after them. +This takes `xs.length + 2` steps and preserves the other heads, all contents, and output. -/ +lemma runFrom_work (cfg : Cfg k Symbol State input) (i : Fin k) (xs : List Symbol) + (htape : cfg.workTapes i = listTape xs) : + (rewind (.work i)).runFrom (workCfg cfg i (some .start) xs.length) (xs.length + 2) = + workCfg cfg i none 0 := by + rw [runFrom_succ_eq_step, step_work_start, runFrom_succ_eq_step', + runFrom_work_scan cfg i xs htape xs.length le_rfl] + rw [show (xs.length : ℤ) - 1 - xs.length = -1 by omega] + simpa using step_work_stop cfg i (-1) (by rw [htape]; rfl) + +/-- The work-tape rewind does not halt before its final move back to the first cell. -/ +lemma work_active (cfg : Cfg k Symbol State input) (i : Fin k) (xs : List Symbol) + (htape : cfg.workTapes i = listTape xs) (r : ℕ) (hr : r < xs.length + 2) : + ((rewind (.work i)).runFrom (workCfg cfg i (some .start) xs.length) r).state ≠ none := by + cases r with + | zero => simp [workCfg] + | succ r => + rw [runFrom_succ_eq_step, step_work_start, runFrom_work_scan cfg i xs htape r (by omega)] + simp [workCfg] + +/-- The first native-input rewind step moves left, with the native boundary clamp. -/ +lemma step_input_start (cfg : Cfg k Symbol State input) (p : Fin (input.length + 2)) : + (rewind .input).step (inputCfg cfg (some .start) p) = + inputCfg cfg (some .scan) (moveInputPos p (-1)) := by + ext i z <;> simp [step, rewind, inputCfg, Cfg.withState] + +/-- A nonboundary native-input position takes one step to the left. -/ +lemma step_input_scan (cfg : Cfg k Symbol State input) (p : Fin (input.length + 2)) + (hp : 0 < p.val) (hlt : p.val ≤ input.length) : + (rewind .input).step (inputCfg cfg (some .scan) p) = + inputCfg cfg (some .scan) (moveInputPos p (-1)) := by + have hleft : p ≠ 0 := by intro h; subst p; simp at hp + have hright : p.val ≠ input.length + 1 := by omega + ext i z <;> + simp [step, rewind, inputCfg, Cfg.withState, Cfg.inputSymbol, hleft, hright] + +/-- At the left blank boundary, move to the initial input position and halt. -/ +lemma step_input_stop (cfg : Cfg k Symbol State input) : + (rewind .input).step (inputCfg cfg (some .scan) 0) = inputCfg cfg none 1 := by + ext i z <;> simp [step, rewind, inputCfg, Cfg.withState, Cfg.inputSymbol, moveInputPos] + +/-- A native input scan reaches its left blank boundary. -/ +lemma runFrom_input_scan (cfg : Cfg k Symbol State input) (n : ℕ) (hn : n ≤ input.length) : + (rewind .input).runFrom (inputCfg cfg (some .scan) ⟨n, by omega⟩) n = + inputCfg cfg (some .scan) 0 := by + induction n with + | zero => rfl + | succ n ih => + rw [runFrom_succ_eq_step, step_input_scan cfg _ (by simp) hn] + have hm : moveInputPos (⟨n + 1, by omega⟩ : Fin (input.length + 2)) (-1) = + ⟨n, by omega⟩ := by + apply Fin.ext + simp [moveInputPos, show n < input.length + 2 by omega] + rw [hm] + exact ih (by omega) + +/-- Rewind the native input from any legal head position. Both blank boundaries and empty input +are allowed. Only the input head and control state change. -/ +lemma runFrom_input (cfg : Cfg k Symbol State input) : + (rewind .input).runFrom (inputCfg cfg (some .start) cfg.inputPos) + (cfg.inputPos.val - 1 + 2) = inputCfg cfg none 1 := by + rw [runFrom_succ_eq_step, step_input_start, runFrom_succ_eq_step'] + have hm : moveInputPos cfg.inputPos (-1) = + (⟨cfg.inputPos.val - 1, by have := cfg.inputPos.isLt; omega⟩ : Fin (input.length + 2)) := by + apply Fin.ext + simp [moveInputPos] + split_ifs <;> simp_all <;> omega + rw [hm, runFrom_input_scan cfg _ (by have := cfg.inputPos.isLt; omega), step_input_stop] + +end Rewind + +end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Sequential.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Sequential.lean new file mode 100644 index 000000000..4915af738 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Sequential.lean @@ -0,0 +1,100 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Basic + +/-! +# Sequential execution on shared tapes + +`seq` runs two machines with the same work-tape count. The transition that would halt the first +machine instead enters the second machine's initial state. Tape contents, head positions, and +accumulated output are carried across, with no extra transition for the handoff. +-/ + +@[expose] public section + +namespace Turing.MultiTapeTM + +variable {k : ℕ} {Symbol State State₀ State₁ : Type*} {input : List Symbol} + +/-- Run two machines on the same tapes, handing off on the first halting transition. -/ +def seq (tm₀ : MultiTapeTM k Symbol State₀) (tm₁ : MultiTapeTM k Symbol State₁) : + MultiTapeTM k Symbol (State₀ ⊕ State₁) where + q₀ := .inl tm₀.q₀ + tr q input work := match q with + | .inl q => + let out := tm₀.tr q input work + ⟨out.inputMove, out.workActions, out.outS, + some (out.q'.elim (.inr tm₁.q₀) Sum.inl)⟩ + | .inr q => + let out := tm₁.tr q input work + ⟨out.inputMove, out.workActions, out.outS, out.q'.map Sum.inr⟩ + +namespace Sequential + +/-- A first-machine configuration; a native halt becomes the second machine's initial state. -/ +def left (tm₁ : MultiTapeTM k Symbol State₁) (cfg : Cfg k Symbol State₀ input) : + Cfg k Symbol (State₀ ⊕ State₁) input := + cfg.withState (some (cfg.state.elim (.inr tm₁.q₀) Sum.inl)) + +/-- A second-machine configuration, including a final halt. -/ +def right (cfg : Cfg k Symbol State₁ input) : Cfg k Symbol (State₀ ⊕ State₁) input := + cfg.withState (cfg.state.map Sum.inr) + +variable (tm₀ : MultiTapeTM k Symbol State₀) (tm₁ : MultiTapeTM k Symbol State₁) + +/-- The left embedding preserves each step before the native halt. -/ +lemma step_left (cfg : Cfg k Symbol State₀ input) (h : cfg.state ≠ none) : + (seq tm₀ tm₁).step (left tm₁ cfg) = left tm₁ (tm₀.step cfg) := by + cases hs : cfg.state with + | none => exact (h hs).elim + | some q => + simp only [step, left, Cfg.withState, seq, hs, Option.elim_some] + rfl + +/-- The right embedding preserves every step, including steps after halting. -/ +lemma step_right (cfg : Cfg k Symbol State₁ input) : + (seq tm₀ tm₁).step (right cfg) = right (tm₁.step cfg) := by + cases hs : cfg.state <;> + simp only [step, right, Cfg.withState, seq, hs, Option.map_some, Option.map_none] + rfl + +/-- The first run is preserved up to its earliest halt. -/ +lemma runFrom_left (cfg : Cfg k Symbol State₀ input) (n : ℕ) + (h : ∀ m < n, (tm₀.runFrom cfg m).state ≠ none) : + (seq tm₀ tm₁).runFrom (left tm₁ cfg) n = left tm₁ (tm₀.runFrom cfg n) := by + induction n with + | zero => rfl + | succ n ih => + rw [runFrom_succ_eq_step', ih (fun m hm => h m (by omega)), + step_left tm₀ tm₁ _ (h n (by omega)), runFrom_succ_eq_step'] + +/-- Once in the second phase, runs are exactly the second machine's runs. -/ +lemma runFrom_right (cfg : Cfg k Symbol State₁ input) (n : ℕ) : + (seq tm₀ tm₁).runFrom (right cfg) n = right (tm₁.runFrom cfg n) := by + induction n with + | zero => rfl + | succ n ih => rw [runFrom_succ_eq_step', ih, step_right, runFrom_succ_eq_step'] + +end Sequential + +/-- Sequential execution splits at the first machine's earliest halt. The second machine receives +all final tapes and head positions, together with the output accumulated so far. -/ +lemma runFrom_seq (tm₀ : MultiTapeTM k Symbol State₀) (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) : + (seq tm₀ tm₁).runFrom (Sequential.left tm₁ cfg) (u + v) = + Sequential.right (tm₁.runFrom ((tm₀.runFrom cfg u).withState (some tm₁.q₀)) v) := by + rw [runFrom_add, Sequential.runFrom_left tm₀ tm₁ cfg u hactive] + rw [show Sequential.left tm₁ (tm₀.runFrom cfg u) = + Sequential.right ((tm₀.runFrom cfg u).withState (some tm₁.q₀)) by + simp [Sequential.left, Sequential.right, Cfg.withState, hhalt]] + exact Sequential.runFrom_right tm₀ tm₁ _ v + +end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/TapeContents.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/TapeContents.lean new file mode 100644 index 000000000..7cd3bc404 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/TapeContents.lean @@ -0,0 +1,55 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Init +public import Mathlib.Algebra.Order.Ring.Nat +public import Mathlib.Algebra.Order.Sub.Basic +public import Mathlib.Algebra.Ring.Int.Defs +public import Mathlib.Data.Finset.Attr +public import Mathlib.Data.Nat.SuccPred + +/-! # Contiguous work-tape contents -/ + +@[expose] public section + +namespace Turing.MultiTapeTM + +variable {Symbol : Type*} + +/-- A tape containing exactly the symbols of `xs` at positions `0, ..., xs.length - 1`. -/ +def listTape (xs : List Symbol) : ℤ → Option Symbol + | .ofNat n => xs[n]? + | .negSucc _ => none + +@[simp] +lemma listTape_ofNat (xs : List Symbol) (n : ℕ) : listTape xs n = xs[n]? := rfl + +@[simp] +lemma listTape_negSucc (xs : List Symbol) (n : ℕ) : listTape xs (.negSucc n) = none := rfl + +/-- Appending one output symbol writes precisely the cell after the existing output. -/ +lemma listTape_append_single (xs : List Symbol) (x : Symbol) : + listTape (xs ++ [x]) = Function.update (listTape xs) (xs.length : ℤ) (some x) := by + funext z + cases z with + | negSucc n => simp [listTape] + | ofNat n => + by_cases h : n = xs.length + · subst n; simp + · by_cases hn : n < xs.length + · simp [List.getElem?_append, hn, h] + · simp [List.getElem?_append, hn, h, show n - xs.length ≠ 0 by omega] + +/-- Every position strictly inside a list tape is nonblank. -/ +lemma listTape_isSome (xs : List Symbol) {p : ℤ} (hp : 0 ≤ p) (hlt : p < xs.length) : + (listTape xs p).isSome := by + lift p to ℕ using hp + simp [listTape] + omega + +end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean index 15145637a..49e7f21ec 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean @@ -7,6 +7,7 @@ Authors: Christian Reitwiessner module public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic +public import Mathlib.Data.Int.Interval /-! # Tape head visitation and space-usage lemmas @@ -132,6 +133,29 @@ lemma spaceUsed_linear (cfg : Cfg k Symbol State input) (t : ℕ) : _ ≤ ∑ i, (t + 1) := Finset.sum_le_sum (fun i _ => tm.spaceUsedByTape_le cfg t i) _ = k * t + k := by simp [Nat.mul_succ] +/-- +The space used by one tape is monotone under inclusion of its visited head positions in the +trajectory of another tape. The hypothesis `hpos` maps every time `r` in the first run to a time +`r'` in the second run at which the two selected tape heads occupy the same position. +-/ +lemma spaceUsedByTape_le_of_positions + {k' : ℕ} {Symbol' State' : Type*} + (tm : MultiTapeTM k Symbol State) (tm' : MultiTapeTM k' Symbol' State') + {input : List Symbol} {input' : List Symbol'} + (cfg : Cfg k Symbol State input) (cfg' : Cfg k' Symbol' State' input') + (t t' : ℕ) (i : Fin k) (i' : Fin k') + (hpos : ∀ r ≤ t, ∃ r' ≤ t', + (tm.runFrom cfg r).workTapePos i = + (tm'.runFrom cfg' r').workTapePos i') : + tm.spaceUsedByTape cfg t i ≤ tm'.spaceUsedByTape cfg' t' i' := by + unfold spaceUsedByTape visitedByTapeHead + apply Finset.card_le_card + intro p hp + simp only [Finset.mem_image, Finset.mem_range] at hp ⊢ + obtain ⟨r, hr, rfl⟩ := hp + obtain ⟨r', hr', hpos'⟩ := hpos r (by omega) + exact ⟨r', by omega, hpos'.symm⟩ + /-- The space used by a single tape is monotone in the number of steps. -/ lemma spaceUsedByTape_mono (tm : MultiTapeTM k Symbol State) diff --git a/CslibTests.lean b/CslibTests.lean index 94af0f156..fb33f54ea 100644 --- a/CslibTests.lean +++ b/CslibTests.lean @@ -18,5 +18,7 @@ import CslibTests.MLL import CslibTests.Modal import CslibTests.Modal.Ideal import CslibTests.Modal.Stlc +import CslibTests.MultiTapeComposition +import CslibTests.MultiTapePlumbing import CslibTests.Reduction import CslibTests.StatefulProcesses diff --git a/CslibTests/MultiTapeComposition.lean b/CslibTests/MultiTapeComposition.lean new file mode 100644 index 000000000..5ac143443 --- /dev/null +++ b/CslibTests/MultiTapeComposition.lean @@ -0,0 +1,68 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Composition +import Mathlib.Tactic.FinCases + +/-! Regression tests for composition: empty output, boundary clamping, final-step output, +disjoint work tapes, and padded component runs. -/ + +namespace CslibTests.MultiTapeComposition + +open Turing.MultiTapeTM + +private def emit (symbol : Option Bool) : Turing.MultiTapeTM 0 Bool Unit where + q₀ := () + tr _ _ _ := ⟨0, Fin.elim0, symbol, none⟩ + +private def probe : Turing.MultiTapeTM 0 Bool (Fin 8) where + q₀ := 0 + tr q input _ := + ⟨(![-1, -1, 1, 1, 1, -1, -1, 1] : Fin 8 → SignType) q, + Fin.elim0, some input.isSome, + if h : q.val + 1 < 8 then some ⟨q.val + 1, h⟩ else none⟩ + +-- Both outward moves clamp; the subsequent inward moves recover the only input symbol. +example : ((comp (emit (some true)) probe).runFrom + ((comp (emit (some true)) probe).initCfg []) 21).output = + [true, false, false, true, false, false, true, false] := by rfl + +-- Empty intermediate output has adjacent blank boundaries and still reaches the second phase. +example : ((comp (emit none) probe).runFrom + ((comp (emit none) probe).initCfg []) 20).output = List.replicate 8 false := by rfl + +-- Output emitted on the halting transition is retained, including when both machines have no tapes. +example : ((comp (emit none) (emit (some true))).runFrom + ((comp (emit none) (emit (some true))).initCfg []) 6).output = [true] := by rfl + +example : ((comp (emit none) (emit (some true))).runFrom + ((comp (emit none) (emit (some true))).initCfg []) 6).state = none := by rfl + +private def writeEmit (symbol : Bool) : Turing.MultiTapeTM 1 Bool Bool where + q₀ := false + tr q _ work := + if q then ⟨0, fun _ => (none, 0), work 0, none⟩ + else ⟨0, fun _ => (some (some symbol), 0), none, some true⟩ + +-- Each component reads its own write; the first component's output does not escape directly. +example : ((comp (writeEmit true) (writeEmit false)).runFrom + ((comp (writeEmit true) (writeEmit false)).initCfg []) 10).output = [false] := by rfl + +example : ((comp (writeEmit true) (writeEmit false)).runFrom + ((comp (writeEmit true) (writeEmit false)).initCfg []) 10).workTapeSymbols = + ![some true, some true, some false] := by + funext i + fin_cases i <;> rfl + +-- The public computation theorem accepts padded halting times for both components. +example : ∃ t ≤ 10 + (0 + 3) + 2 * 12, ∃ s ≤ 0 + (0 + 2) + 0, + ComputesInTimeAndSpace (comp (emit none) (emit (some true))) [] [true] t s := by + apply comp_computesInTimeAndSpace (emit none) (emit (some true)) + (middle := []) (t₀ := 10) (s₀ := 0) (t₁ := 12) (s₁ := 0) + · exact ⟨rfl, rfl, spaceUsed_zero_tapes_eq_zero _ _ rfl⟩ + · exact ⟨rfl, rfl, spaceUsed_zero_tapes_eq_zero _ _ rfl⟩ + +end CslibTests.MultiTapeComposition diff --git a/CslibTests/MultiTapePlumbing.lean b/CslibTests/MultiTapePlumbing.lean new file mode 100644 index 000000000..baa0c4c57 --- /dev/null +++ b/CslibTests/MultiTapePlumbing.lean @@ -0,0 +1,109 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Cslib.Computability.Machines.Turing.MultiTape.NormalForms.RewindInput +import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Comp + +/-! Executable regressions and interface checks for generic TM plumbing. -/ + +namespace CslibTests.MultiTapePlumbing + +open Turing.MultiTapeTM + +private def finish (move : SignType) (symbol : Bool) : Turing.MultiTapeTM 0 Bool Unit where + q₀ := () + tr _ _ _ := ⟨move, Fin.elim0, some symbol, none⟩ + +-- Sequential execution retains the output accumulated by the first machine. +example : (((finish 0 true).seq (finish 0 false)).runFrom + (((finish 0 true).seq (finish 0 false)).initCfg []) 2).output = [true, false] := by rfl + +-- Rewinding works when the native halt is at either boundary, including on empty input. +example : ((finish (-1) true).rewindInput.runFrom + ((finish (-1) true).rewindInput.initCfg [false]) 3).inputPos = 1 := by rfl + +example : ((finish 1 true).rewindInput.runFrom + ((finish 1 true).rewindInput.initCfg [false]) 4).inputPos = 1 := by rfl + +example : ((finish 1 true).rewindInput.runFrom + ((finish 1 true).rewindInput.initCfg []) 3).state = none := by rfl + +example : ((finish 1 true).rewindInput.runFrom + ((finish 1 true).rewindInput.initCfg []) 3).output = [true] := by rfl + +private def filled (xs : List Bool) : Cfg 1 Bool Unit [] := + ⟨none, 1, fun _ => listTape xs, fun _ => xs.length, []⟩ + +-- Work-tape rewind preserves the contents and resets the head, even for empty contents. +example : ((rewind (.work (0 : Fin 1))).runFrom + (Rewind.workCfg (filled []) 0 (some .start) 0) 2).workTapePos 0 = 0 := by rfl + +example : ((rewind (.work (0 : Fin 1))).runFrom + (Rewind.workCfg (filled [true, false]) 0 (some .start) 2) 4).state = none := by rfl + +example : ((rewind (.work (0 : Fin 1))).runFrom + (Rewind.workCfg (filled [true, false]) 0 (some .start) 2) 4).workTapes 0 = + listTape [true, false] := by rfl + +-- Output redirection includes the symbol emitted on the halting transition. +example : ((finish 0 true).outputToWorkTape.runFrom + ((finish 0 true).outputToWorkTape.initCfg []) 1).workTapes 0 0 = some true := by rfl + +example : ((finish 0 true).outputToWorkTape.runFrom + ((finish 0 true).outputToWorkTape.initCfg []) 1).output = [] := by rfl + +private def readInput : Turing.MultiTapeTM 0 Bool Unit where + q₀ := () + tr _ input _ := ⟨0, Fin.elim0, input, none⟩ + +-- Substituted input is read from the work tape, with the real head parked elsewhere. +private def preparedInput (xs : List Bool) : Cfg 1 Bool (InputState Unit) [false] := + InputFromWorkTape.classifyCfg 0 (readInput.initCfg xs) .right + +example : (readInput.inputFromWorkTape.runFrom (preparedInput [true]) 3).output = [true] := by + rfl + +example : (readInput.inputFromWorkTape.runFrom (preparedInput [true]) 3).inputPos = 0 := by rfl + +example : (readInput.inputFromWorkTape.runFrom (preparedInput []) 3).state = none := by rfl + +private def sparse : Fin 1 ↪ Fin 3 := ⟨fun _ => 2, fun _ _ _ => Subsingleton.elim _ _⟩ + +private def writer : Turing.MultiTapeTM 1 Bool Unit where + q₀ := () + tr _ _ _ := ⟨0, fun _ => (some (some true), 1), none, none⟩ + +-- The injection is not an initial-segment inclusion; unused tape data and heads are retained. +example : ((writer.extendTapes sparse).runFrom + (ExtendTapes.embed sparse (writer.initCfg []) + (fun _ _ => some false) (fun _ => 7)) 1).workTapes 0 0 = some false := by rfl + +example : ((writer.extendTapes sparse).runFrom + (ExtendTapes.embed sparse (writer.initCfg []) + (fun _ _ => some false) (fun _ => 7)) 1).workTapePos 0 = 7 := by rfl + +example : ((writer.extendTapes sparse).runFrom + (ExtendTapes.embed sparse (writer.initCfg []) + (fun _ _ => some false) (fun _ => 7)) 1).workTapes 2 0 = some true := by rfl + +private def bit : Bool ↪ List Bool := ⟨fun b => [b], by intro a b h; simpa using h⟩ + +-- Bounds can differ for inputs of the same encoded length; the public combinator needs no +-- monotonicity premise and hides the machine witnesses. +private lemma constant_computable : + ComputableInTimeAndSpace (fun _ : Bool => true) bit bit + (fun b => if b then 1 else 2) (fun _ => 0) := by + refine ⟨0, Unit, inferInstance, finish 0 true, fun b => ⟨1, ?_, 0, le_rfl, ?_⟩⟩ + · cases b <;> decide + · exact ⟨rfl, rfl, spaceUsed_zero_tapes_eq_zero _ _ rfl⟩ + +example : ComputableInTimeAndSpace (fun _ : Bool => true) bit bit + (fun b => (if b then 1 else 2) + 6) (fun _ => 3) := by + have hbit (b : Bool) : bit b = [b] := rfl + simpa [hbit, Nat.add_assoc] using + computableInTimeAndSpace_comp constant_computable constant_computable + +end CslibTests.MultiTapePlumbing