From 5f4d9265d8e4f5a02338a9c8c8976d903548541f Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 5 Sep 2026 11:33:29 -0400 Subject: [PATCH 1/3] feat(MultiTapeTM): compose machines with time and space bounds --- Cslib.lean | 4 + .../Turing/MultiTape/Composition.lean | 491 ++++++++++++++++++ .../Turing/MultiTape/Composition/Defs.lean | 319 ++++++++++++ .../Turing/MultiTape/Composition/Rewind.lean | 318 ++++++++++++ .../MultiTape/Composition/Simulation.lean | 352 +++++++++++++ .../Turing/MultiTape/Deterministic.lean | 60 ++- .../Machines/Turing/MultiTape/TapeLemmas.lean | 24 + CslibTests.lean | 1 + CslibTests/MultiTapeComposition.lean | 68 +++ 9 files changed, 1632 insertions(+), 5 deletions(-) create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Composition.lean create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Composition/Defs.lean create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Composition/Rewind.lean create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Composition/Simulation.lean create mode 100644 CslibTests/MultiTapeComposition.lean diff --git a/Cslib.lean b/Cslib.lean index 34a0d27be..485eb15eb 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -46,6 +46,10 @@ 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.Composition +public import Cslib.Computability.Machines.Turing.MultiTape.Composition.Defs +public import Cslib.Computability.Machines.Turing.MultiTape.Composition.Rewind +public import Cslib.Computability.Machines.Turing.MultiTape.Composition.Simulation public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic public import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas public import Cslib.Computability.Machines.Turing.SingleTape.Defs diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Composition.lean b/Cslib/Computability/Machines/Turing/MultiTape/Composition.lean new file mode 100644 index 000000000..2b7984f6e --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Composition.lean @@ -0,0 +1,491 @@ +/- +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.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. `comp_computesFunInTimeAndSpace_of_length_le` lifts this result to functions with a +separate output-length bound; `comp_computesFunInTimeAndSpace` uses the first time bound instead. + +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 hmid : + (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)) := + runFrom_to_secondInit tm₀ tm₁ input u hhalt₀ hactive₀ + have hfinal : + (comp tm₀ tm₁).runFrom ((comp tm₀ tm₁).initCfg input) + (u + ((tm₀.runFrom (tm₀.initCfg input) u).output.length + 3) + 2 * v) = + embedSecond tm₀ tm₁ + (tm₀.runFrom (tm₀.initCfg input) u) + (tm₁.runFrom + (tm₁.initCfg ((tm₀.runFrom (tm₀.initCfg input) u).output)) v) := by + rw [(comp tm₀ tm₁).runFrom_add ((comp tm₀ tm₁).initCfg input) + (u + ((tm₀.runFrom (tm₀.initCfg input) u).output.length + 3)) (2 * v)] + rw [hmid] + exact runFrom_secondPhase tm₀ tm₁ + (tm₀.runFrom (tm₀.initCfg input) u) + (tm₁.initCfg ((tm₀.runFrom (tm₀.initCfg input) u).output)) v + rw [hfinal] + constructor + · change Option.map _ + (tm₁.runFrom + (tm₁.initCfg ((tm₀.runFrom (tm₀.initCfg input) u).output)) v).state = none + rw [hhalt₁] + rfl + · rfl + +/-- 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) + .rewind + (((firstFinalCfg tm₀ input u).output.length : ℤ) - 1 - s)) + | initialClassify + (hcfg : cfg = intermediateCfg tm₀ tm₁ + (firstFinalCfg tm₀ input u) + (.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 : CompositionBoundary) + (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 +-/ + +namespace Composition + +/-- Time bound produced by sequentially composing computations with bounds `T₀` and `T₁`. -/ +def timeBound (T₀ T₁ : ℕ → ℕ) (n : ℕ) : ℕ := + 2 * T₀ n + 3 + 2 * T₁ (T₀ n) + +/-- Space bound produced by sequential composition, including its intermediate work tape. -/ +def spaceBound (T₀ S₀ S₁ : ℕ → ℕ) (n : ℕ) : ℕ := + S₀ n + (T₀ n + 2) + S₁ (T₀ n) + +/-- Sequential composition preserves monotonicity of time bounds. -/ +lemma timeBound_mono {T₀ T₁ : ℕ → ℕ} (hT₀ : Monotone T₀) (hT₁ : Monotone T₁) : + Monotone (timeBound T₀ T₁) := by + intro m n hmn + have hT₀mn := hT₀ hmn + have hT₁mn := hT₁ hT₀mn + simp only [timeBound] + omega + +/-- Sequential composition preserves monotonicity of space bounds. -/ +lemma spaceBound_mono {T₀ S₀ S₁ : ℕ → ℕ} + (hT₀ : Monotone T₀) (hS₀ : Monotone S₀) (hS₁ : Monotone S₁) : + Monotone (spaceBound T₀ S₀ S₁) := by + intro m n hmn + have hT₀mn := hT₀ hmn + have hS₀mn := hS₀ hmn + have hS₁mn := hS₁ hT₀mn + simp only [spaceBound] + omega + +end Composition + +/-- 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 => + refine ⟨u, le_rfl, ?_⟩ + rw [hcfg] + simp [intermediateCfg, embedFirst, compositionFirstTapeIdx, hidx_ne] + | initialClassify hcfg => + refine ⟨u, le_rfl, ?_⟩ + rw [hcfg] + simp [intermediateCfg, embedFirst, compositionFirstTapeIdx, hidx_ne] + | second _ _ hcfg => + refine ⟨u, le_rfl, ?_⟩ + rw [hcfg] + simp [embedSecond, compositionFirstTapeIdx] + | 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 => + refine ⟨0, Nat.zero_le _, ?_⟩ + rw [hcfg] + simp [intermediateCfg, embedFirst, compositionSecondTapeIdx, + secondCfgAt, secondInitCfg, runFrom, hidx_not_lt, hidx_ne] + | 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 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 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 + unfold spaceUsedByTape + have hsub : + (comp tm₀ tm₁).visitedByTapeHead + ((comp tm₀ tm₁).initCfg input) + (compositionTotalTime tm₀ input u v) + (compositionIntermediateTapeIdx k₀ k₁) ⊆ + Finset.Icc (-1) ((firstFinalCfg tm₀ input u).output.length : ℤ) := by + intro p hp + simp only [visitedByTapeHead, Finset.mem_image, Finset.mem_range] at hp + obtain ⟨r, hr, rfl⟩ := hp + exact compositionIntermediateTapePos_mem_Icc tm₀ tm₁ input u v r + hrun (by simpa [compositionTotalTime] using hr) + calc ((comp tm₀ tm₁).visitedByTapeHead + ((comp tm₀ tm₁).initCfg input) + (compositionTotalTime tm₀ input u v) + (compositionIntermediateTapeIdx k₀ k₁)).card + ≤ (Finset.Icc (-1) ((firstFinalCfg tm₀ input u).output.length : ℤ)).card := + Finset.card_le_card hsub + _ = (firstFinalCfg tm₀ input u).output.length + 2 := 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⟩ + +/-- Function composition with a separate bound on intermediate output length. +This avoids charging a long first computation's running time as intermediate space. -/ +theorem comp_computesFunInTimeAndSpace_of_length_le + {IOSymbol : Type*} {f g : List IOSymbol → List IOSymbol} + (embedding : IOSymbol ↪ Symbol) {T₀ S₀ T₁ S₁ L : ℕ → ℕ} + (h₀ : ComputesFunInTimeAndSpace tm₀ f embedding T₀ S₀) + (h₁ : ComputesFunInTimeAndSpace tm₁ g embedding T₁ S₁) + (hL : ∀ input, (f input).length ≤ L input.length) + (hT₁ : Monotone T₁) (hS₁ : Monotone S₁) : + ComputesFunInTimeAndSpace (comp tm₀ tm₁) (g ∘ f) embedding + (fun n => T₀ n + (L n + 3) + 2 * T₁ (L n)) + (fun n => S₀ n + (L n + 2) + S₁ (L n)) := by + intro input + obtain ⟨t₀, ht₀, s₀, hs₀, hc₀⟩ := h₀ input + obtain ⟨t₁, ht₁, s₁, hs₁, hc₁⟩ := h₁ (f input) + obtain ⟨t, ht, s, hs, hc⟩ := comp_computesInTimeAndSpace tm₀ tm₁ hc₀ hc₁ + simp only [List.length_map] at ht hs + have hlength := hL input + have htime := hT₁ hlength + have hspace := hS₁ hlength + exact ⟨t, by dsimp only; omega, s, by dsimp only; omega, hc⟩ + +/-- Function composition with bounds expressed only in terms of component time and space. +The first time bound also bounds intermediate output length. -/ +theorem comp_computesFunInTimeAndSpace + {IOSymbol : Type*} {f g : List IOSymbol → List IOSymbol} + (embedding : IOSymbol ↪ Symbol) {T₀ S₀ T₁ S₁ : ℕ → ℕ} + (h₀ : ComputesFunInTimeAndSpace tm₀ f embedding T₀ S₀) + (h₁ : ComputesFunInTimeAndSpace tm₁ g embedding T₁ S₁) + (hT₁ : Monotone T₁) (hS₁ : Monotone S₁) : + ComputesFunInTimeAndSpace (comp tm₀ tm₁) (g ∘ f) embedding + (Composition.timeBound T₀ T₁) (Composition.spaceBound T₀ S₀ S₁) := by + have hlength (input) : (f input).length ≤ T₀ input.length := by + obtain ⟨t, ht, s, _, hc⟩ := h₀ input + simpa only [List.length_map] using (output_length_le_time hc).trans ht + change ComputesFunInTimeAndSpace _ _ _ + (fun n => 2 * T₀ n + 3 + 2 * T₁ (T₀ n)) (fun n => S₀ n + (T₀ n + 2) + S₁ (T₀ n)) + simpa only [two_mul, Nat.add_assoc] + using comp_computesFunInTimeAndSpace_of_length_le tm₀ tm₁ embedding h₀ h₁ hlength hT₁ hS₁ + +end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Composition/Defs.lean b/Cslib/Computability/Machines/Turing/MultiTape/Composition/Defs.lean new file mode 100644 index 000000000..56e7f4c83 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Composition/Defs.lean @@ -0,0 +1,319 @@ +/- +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 + +/-! +# 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 + +/-- Location of the virtual input head during the second phase. -/ +inductive CompositionInputMode + | left + | inside + | right +deriving DecidableEq + +/-- Boundary toward which a virtual input-head move was made. -/ +inductive CompositionBoundary + | left + | right + +/-- Control states of a composed multi-tape Turing machine. -/ +inductive CompositionState (State₀ State₁ : Type*) + | first (q : State₀) + | rewindStart + | rewind + | second (q : State₁) (mode : CompositionInputMode) + | classify (q : State₁) (boundary : CompositionBoundary) + +/-- Assemble the first work-tape block, the intermediate tape, and the second block. +The same layout is used for tape contents, head positions, and transition actions. -/ +@[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⟩ + +/-- A work-tape action that neither writes nor moves. -/ +def idleWorkAction : Option (Option Symbol) × SignType := (none, 0) + +/-- Movement of the virtual input head, with outward boundary moves clamped. -/ +def CompositionInputMode.move : CompositionInputMode → 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 CompositionInputMode.nextBoundary : + CompositionInputMode → SignType → CompositionBoundary + | _, .neg | .left, .zero => .left + | _, _ => .right + +/-- Convert a boundary classifier result to an input mode. -/ +def CompositionBoundary.inputMode : CompositionBoundary → CompositionInputMode + | .left => .left + | .right => .right + +/-- Read the work symbols seen by the first component machine. -/ +def compositionFirstWorkSymbols + (work : Fin (compositionTapeCount k₀ k₁) → Option Symbol) : + Fin k₀ → Option Symbol := + fun i => work (compositionFirstTapeIdx k₁ i) + +/-- Read the work symbols seen by the second component machine. -/ +def compositionSecondWorkSymbols + (work : Fin (compositionTapeCount k₀ k₁) → Option Symbol) : + Fin k₁ → Option Symbol := + fun i => work (compositionSecondTapeIdx k₀ k₁ i) + +/-- Embed the first component's work actions and redirect its output to the intermediate tape. -/ +def compositionFirstWorkActions + (actions : Fin k₀ → Option (Option Symbol) × SignType) + (outS : Option Symbol) : + Fin (compositionTapeCount k₀ k₁) → + Option (Option Symbol) × SignType := + Composition.tapes actions + (match outS with | none => idleWorkAction | some s => (some (some s), 1)) + (fun _ => idleWorkAction) + +/-- Park every tape except the intermediate tape and move that tape by `move`. -/ +def compositionMoveIntermediate (move : SignType) : + Fin (compositionTapeCount k₀ k₁) → + Option (Option Symbol) × SignType := + Composition.tapes (fun _ => idleWorkAction) (none, move) (fun _ => idleWorkAction) + +/-- Embed the second component's work actions and move the intermediate virtual-input tape. -/ +def compositionSecondWorkActions + (inputMove : SignType) + (actions : Fin k₁ → Option (Option Symbol) × SignType) : + Fin (compositionTapeCount k₀ k₁) → + Option (Option Symbol) × SignType := + Composition.tapes (fun _ => idleWorkAction) (none, inputMove) actions + +/-- Classify a virtual-input cell after moving onto it. -/ +def compositionClassifyMode + (cell : Option Symbol) + (boundary : CompositionBoundary) : CompositionInputMode := + if cell.isSome then .inside else boundary.inputMode + +/-- Sequential composition of two deterministic multi-tape Turing machines. -/ +def comp + (tm₀ : MultiTapeTM k₀ Symbol State₀) + (tm₁ : MultiTapeTM k₁ Symbol State₁) : + MultiTapeTM (compositionTapeCount k₀ k₁) Symbol + (CompositionState State₀ State₁) where + q₀ := .first tm₀.q₀ + tr q input work := + match q with + | .first q₀ => + let out := tm₀.tr q₀ input (compositionFirstWorkSymbols work) + { + inputMove := out.inputMove + workActions := compositionFirstWorkActions out.workActions out.outS + outS := none + q' := some (match out.q' with + | some q' => .first q' + | none => .rewindStart) + } + | .rewindStart => + { + inputMove := 0 + workActions := compositionMoveIntermediate (-1) + outS := none + q' := some .rewind + } + | .rewind => + if (work (compositionIntermediateTapeIdx k₀ k₁)).isSome then + { + inputMove := 0 + workActions := compositionMoveIntermediate (-1) + outS := none + q' := some .rewind + } + else + { + inputMove := 0 + workActions := compositionMoveIntermediate 1 + outS := none + q' := some (.classify tm₁.q₀ .right) + } + | .second q₁ mode => + let inputMove := mode.move + let out := tm₁.tr q₁ + (if mode = .inside then work (compositionIntermediateTapeIdx k₀ k₁) else none) + (compositionSecondWorkSymbols work) + { + inputMove := 0 + workActions := compositionSecondWorkActions (inputMove out.inputMove) out.workActions + outS := out.outS + q' := out.q'.map fun q' => .classify q' (mode.nextBoundary out.inputMove) + } + | .classify q₁ boundary => + { + inputMove := 0 + workActions := fun _ => idleWorkAction + outS := none + q' := some (.second q₁ + (compositionClassifyMode (work (compositionIntermediateTapeIdx k₀ k₁)) boundary)) + } + +namespace Composition + +/-- 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 => + simp only [listTape] + rw [List.getElem?_append] + by_cases h : n = xs.length + · subst n + simp + · by_cases hn : n < xs.length + · simp [hn, h] + · have hle : xs.length ≤ n := Nat.le_of_not_gt hn + have hlt : xs.length < n := lt_of_le_of_ne hle (Ne.symm h) + have hsub : n - xs.length ≠ 0 := by omega + simp [h, hn, hsub] + +/-- 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 (.first q) + | none => some .rewindStart + inputPos := cfg.inputPos + workTapes := tapes cfg.workTapes (listTape cfg.output) (fun _ _ => none) + workTapePos := tapes cfg.workTapePos cfg.output.length (fun _ => 0) + output := [] + +/-- 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)) : CompositionInputMode := + if p = 0 then .left else if p.val = input.length + 1 then .right else .inside + +/-- 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 (.second q (inputMode secondCfg.inputPos)) + | none => none + inputPos := firstCfg.inputPos + workTapes := tapes firstCfg.workTapes (listTape secondInput) secondCfg.workTapes + workTapePos := tapes firstCfg.workTapePos + (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 : CompositionBoundary) : + Cfg (compositionTapeCount k₀ k₁) Symbol + (CompositionState State₀ State₁) firstInput := + { embedSecond _tm₀ _tm₁ firstCfg secondCfg with + state := secondCfg.state.map fun q => .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/Composition/Rewind.lean b/Cslib/Computability/Machines/Turing/MultiTape/Composition/Rewind.lean new file mode 100644 index 000000000..501fe5e41 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Composition/Rewind.lean @@ -0,0 +1,318 @@ +/- +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.Composition.Simulation + +/-! +# First-phase simulation and handoff + +The first machine runs in lockstep with the composite. Its output is rewound to the left +boundary, then classified to establish the second machine's initial configuration. +-/ + +@[expose] public section + +namespace Turing.MultiTapeTM.Composition + +variable {k₀ k₁ : ℕ} +variable {Symbol State₀ State₁ : Type*} + +variable (tm₀ : MultiTapeTM k₀ Symbol State₀) (tm₁ : MultiTapeTM k₁ Symbol State₁) + +/-- The first-phase embedding sends an initial configuration to the composite initial +configuration. -/ +private lemma embedFirst_initCfg (input : List Symbol) : + embedFirst tm₀ tm₁ (tm₀.initCfg input) = + (comp tm₀ tm₁).initCfg input := by + apply Cfg.ext + · rfl + · rfl + · funext i p + by_cases hfirst : i.val < k₀ + · simp [embedFirst, hfirst] + · by_cases hmiddle : i.val = k₀ + · cases p <;> simp [embedFirst, hmiddle, listTape] + · simp [embedFirst, hfirst, hmiddle] + · funext i + simp [embedFirst] + · rfl + +/-- The first-phase embedding preserves the symbol read from the real input. -/ +@[simp] +private lemma embedFirst_inputSymbol {input : List Symbol} + (cfg : Cfg k₀ Symbol State₀ input) : + (embedFirst tm₀ tm₁ cfg).inputSymbol = cfg.inputSymbol := rfl + +/-- The first-phase embedding preserves every symbol read from a first-machine work tape. -/ +private lemma compositionFirstWorkSymbols_embedFirst {input : List Symbol} + (cfg : Cfg k₀ Symbol State₀ input) : + compositionFirstWorkSymbols + (embedFirst tm₀ tm₁ cfg).workTapeSymbols = + cfg.workTapeSymbols := by + funext i + simp [compositionFirstWorkSymbols, Cfg.workTapeSymbols, embedFirst, + compositionFirstTapeIdx] + +/-- One first-machine step is one composite first-phase step. A halt of the first machine enters +the rewind phase instead of halting the composite machine. -/ +private lemma step_embedFirst {input : List Symbol} + (cfg : Cfg k₀ Symbol State₀ input) (hactive : cfg.state ≠ none) : + (comp tm₀ tm₁).step (embedFirst tm₀ tm₁ cfg) = + embedFirst tm₀ tm₁ (tm₀.step cfg) := by + cases hstate : cfg.state with + | none => exact absurd hstate hactive + | some q => + have hinput := embedFirst_inputSymbol tm₀ tm₁ cfg + have hwork := compositionFirstWorkSymbols_embedFirst tm₀ tm₁ cfg + unfold step + rw [show (embedFirst tm₀ tm₁ cfg).state = + some (.first q) by simp [embedFirst, hstate]] + rw [hstate] + simp only [comp] + rw [hinput, hwork] + generalize htr : tm₀.tr q cfg.inputSymbol cfg.workTapeSymbols = trOut + obtain ⟨inputMove, workActions, outS, q'⟩ := trOut + simp only [htr] + apply Cfg.ext + · cases q' <;> rfl + · rfl + · funext i p + by_cases hfirst : i.val < k₀ + · cases hwrite : (workActions ⟨i.val, hfirst⟩).1 <;> + simp [embedFirst, compositionFirstWorkActions, hfirst, hwrite] + · by_cases hmiddle : i.val = k₀ + · cases outS with + | none => + simp [embedFirst, compositionFirstWorkActions, hmiddle, + idleWorkAction] + | some s => + simp [embedFirst, compositionFirstWorkActions, hmiddle, + listTape_append_single] + · simp [embedFirst, compositionFirstWorkActions, hfirst, hmiddle, + idleWorkAction] + · funext i + by_cases hfirst : i.val < k₀ + · simp [embedFirst, compositionFirstWorkActions, hfirst] + · by_cases hmiddle : i.val = k₀ + · cases outS <;> + simp [embedFirst, compositionFirstWorkActions, hmiddle, + idleWorkAction] + · simp [embedFirst, compositionFirstWorkActions, hfirst, hmiddle, + idleWorkAction] + · rfl + +/-- Simulation of the first component up to a time at which it has not halted earlier. -/ +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 + induction n with + | zero => simpa using (embedFirst_initCfg tm₀ tm₁ input).symm + | succ n ih => + rw [tm₀.runFrom_succ_eq_step', (comp tm₀ tm₁).runFrom_succ_eq_step', + ih (fun m hm => hactive m (by omega))] + exact step_embedFirst tm₀ tm₁ + (tm₀.runFrom (tm₀.initCfg input) n) (hactive n (by omega)) + +/-- At position zero, the post-rewind classifier configuration is the classifier half of the +second machine's initial configuration. -/ +private lemma intermediateCfg_classify_init {input : List Symbol} + (cfg : Cfg k₀ Symbol State₀ input) : + intermediateCfg tm₀ tm₁ cfg + (.classify tm₁.q₀ .right) 0 = + classifyCfg tm₀ tm₁ cfg (tm₁.initCfg cfg.output) .right := by + apply Cfg.ext + · rfl + · rfl + · funext i p + by_cases hfirst : i.val < k₀ + · simp [intermediateCfg, embedFirst, classifyCfg, + embedSecond, hfirst] + · by_cases hmiddle : i.val = k₀ + · simp [intermediateCfg, embedFirst, classifyCfg, + embedSecond, hmiddle] + · simp [intermediateCfg, embedFirst, classifyCfg, + embedSecond, hfirst, hmiddle] + · funext i + by_cases hfirst : i.val < k₀ + · have hmiddle : i.val ≠ k₀ := by omega + simp [intermediateCfg, embedFirst, classifyCfg, + embedSecond, virtualInputPos, hfirst, hmiddle] + · by_cases hmiddle : i.val = k₀ <;> + simp [intermediateCfg, embedFirst, classifyCfg, + embedSecond, virtualInputPos, hfirst, hmiddle] + · rfl + +/-- Entering the rewind phase moves the intermediate head one cell to the left. -/ +private lemma step_rewindStart {input : List Symbol} + (cfg : Cfg k₀ Symbol State₀ input) (hhalt : cfg.state = none) : + (comp tm₀ tm₁).step (embedFirst tm₀ tm₁ cfg) = + intermediateCfg tm₀ tm₁ cfg .rewind + (cfg.output.length - 1) := by + apply Cfg.ext + · simp [step, embedFirst, intermediateCfg, comp, hhalt] + · simp [step, embedFirst, intermediateCfg, comp, hhalt] + · funext i p + by_cases hmiddle : i.val = k₀ <;> + simp [step, embedFirst, intermediateCfg, comp, hhalt, + compositionMoveIntermediate, idleWorkAction, hmiddle] + · funext i + by_cases hmiddle : i.val = k₀ + · simp [step, embedFirst, intermediateCfg, comp, hhalt, + compositionMoveIntermediate, idleWorkAction, hmiddle] + omega + · simp [step, embedFirst, intermediateCfg, comp, hhalt, + compositionMoveIntermediate, idleWorkAction, hmiddle] + · simp [step, embedFirst, intermediateCfg, comp, hhalt] + +/-- One rewind step over a nonblank intermediate cell. -/ +private lemma step_rewind_some {input : List Symbol} + (cfg : Cfg k₀ Symbol State₀ input) (pos : ℤ) + (hcell : (listTape cfg.output pos).isSome) : + (comp tm₀ tm₁).step + (intermediateCfg tm₀ tm₁ cfg .rewind pos) = + intermediateCfg tm₀ tm₁ cfg .rewind (pos - 1) := by + apply Cfg.ext + · simp [step, intermediateCfg, embedFirst, comp, + Cfg.workTapeSymbols, hcell, compositionMoveIntermediate, idleWorkAction] + · simp [step, intermediateCfg, embedFirst, comp, + Cfg.workTapeSymbols, hcell] + · funext i p + by_cases hmiddle : i.val = k₀ <;> + simp [step, intermediateCfg, embedFirst, comp, + Cfg.workTapeSymbols, hcell, compositionMoveIntermediate, idleWorkAction, hmiddle] + · funext i + by_cases hmiddle : i.val = k₀ + · simp [step, intermediateCfg, embedFirst, comp, + Cfg.workTapeSymbols, hcell, compositionMoveIntermediate, idleWorkAction, hmiddle] + omega + · simp [step, intermediateCfg, embedFirst, comp, + Cfg.workTapeSymbols, hcell, compositionMoveIntermediate, idleWorkAction, hmiddle] + · simp [step, intermediateCfg, embedFirst, comp, + Cfg.workTapeSymbols, hcell] + +/-- The blank just left of the intermediate output ends rewinding and moves the head to cell +zero for classification. -/ +private lemma step_rewind_none {input : List Symbol} + (cfg : Cfg k₀ Symbol State₀ input) (pos : ℤ) + (hcell : listTape cfg.output pos = none) : + (comp tm₀ tm₁).step + (intermediateCfg tm₀ tm₁ cfg .rewind pos) = + intermediateCfg tm₀ tm₁ cfg + (.classify tm₁.q₀ .right) (pos + 1) := by + apply Cfg.ext + · simp [step, intermediateCfg, embedFirst, comp, + Cfg.workTapeSymbols, hcell] + · simp [step, intermediateCfg, embedFirst, comp, + Cfg.workTapeSymbols, hcell] + · funext i p + by_cases hmiddle : i.val = k₀ <;> + simp [step, intermediateCfg, embedFirst, comp, + Cfg.workTapeSymbols, hcell, compositionMoveIntermediate, idleWorkAction, hmiddle] + · funext i + by_cases hmiddle : i.val = k₀ <;> + simp [step, intermediateCfg, embedFirst, comp, + Cfg.workTapeSymbols, hcell, compositionMoveIntermediate, idleWorkAction, hmiddle] + · simp [step, intermediateCfg, embedFirst, comp, + Cfg.workTapeSymbols, hcell] + +/-- A canonical list tape is nonblank at every position inside the represented list. -/ +private lemma listTape_isSome_of_lt (xs : List Symbol) {r : ℕ} (h : r < xs.length) : + (listTape xs ((xs.length : ℤ) - 1 - r)).isSome := by + have hp : (xs.length : ℤ) - 1 - r = (xs.length - 1 - r : ℕ) := by omega + rw [hp] + simp [listTape] + omega + +/-- Rewinding scans exactly the cells occupied by the intermediate output. -/ +private lemma runFrom_rewind {input : List Symbol} + (cfg : Cfg k₀ Symbol State₀ input) + (r : ℕ) (hr : r ≤ cfg.output.length) : + (comp tm₀ tm₁).runFrom + (intermediateCfg tm₀ tm₁ cfg .rewind + ((cfg.output.length : ℤ) - 1)) r = + intermediateCfg tm₀ tm₁ cfg .rewind + ((cfg.output.length : ℤ) - 1 - r) := by + induction r with + | zero => simp [runFrom] + | succ r ih => + rw [(comp tm₀ tm₁).runFrom_succ_eq_step', ih (by omega)] + have hcell : + (listTape cfg.output ((cfg.output.length : ℤ) - 1 - r)).isSome := by + simpa using + (listTape_isSome_of_lt cfg.output + (r := r) (show r < cfg.output.length by omega)) + convert step_rewind_some tm₀ tm₁ cfg + ((cfg.output.length : ℤ) - 1 - r) hcell using 1 + congr 1 + omega + +/-- The prefix of the post-halting phase that consists of entering and running the rewind loop. -/ +lemma runFrom_firstHalt_rewind {input : List Symbol} + (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 .rewind + ((cfg.output.length : ℤ) - 1 - r) := by + rw [(comp tm₀ tm₁).runFrom_succ_eq_step, step_rewindStart tm₀ tm₁ cfg hhalt] + exact runFrom_rewind tm₀ tm₁ cfg r hr + +/-- The configuration immediately after the rewind loop is the initial classifier +configuration at intermediate-tape position zero. -/ +lemma runFrom_firstHalt_classify {input : List Symbol} + (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 + (.classify tm₁.q₀ .right) 0 := by + rw [show cfg.output.length + 2 = (cfg.output.length + 1) + 1 by omega, + (comp tm₀ tm₁).runFrom_succ_eq_step'] + rw [runFrom_firstHalt_rewind tm₀ tm₁ cfg hhalt cfg.output.length le_rfl] + rw [show (cfg.output.length : ℤ) - 1 - cfg.output.length = -1 by omega] + simpa using step_rewind_none tm₀ tm₁ cfg (-1) (by rfl) + +/-- After rewinding, one classification step enters the second machine's initial configuration. -/ +private lemma step_intermediateCfg_classify_init {input : List Symbol} + (cfg : Cfg k₀ Symbol State₀ input) : + (comp tm₀ tm₁).step + (intermediateCfg tm₀ tm₁ cfg + (.classify tm₁.q₀ .right) 0) = + embedSecond tm₀ tm₁ cfg (tm₁.initCfg cfg.output) := by + rw [intermediateCfg_classify_init] + apply step_classifyCfg + cases cfg.output <;> + simp [compositionClassifyMode, inputMode, virtualInputPos, + CompositionBoundary.inputMode, listTape] + +/-- Starting from a halted first-machine configuration, rewinding and initialization take exactly +the output length plus three steps. -/ +private lemma runFrom_firstHalt_to_secondInit {input : List Symbol} + (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 [show cfg.output.length + 3 = (cfg.output.length + 2) + 1 by omega, + (comp tm₀ tm₁).runFrom_succ_eq_step', runFrom_firstHalt_classify tm₀ tm₁ cfg hhalt] + exact step_intermediateCfg_classify_init tm₀ tm₁ cfg + +/-- Running the first phase and rewinding its output reaches the second machine's initial +configuration. -/ +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 [(comp tm₀ tm₁).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/Composition/Simulation.lean b/Cslib/Computability/Machines/Turing/MultiTape/Composition/Simulation.lean new file mode 100644 index 000000000..464a7b8a0 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Composition/Simulation.lean @@ -0,0 +1,352 @@ +/- +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.Composition.Defs + +/-! +# Second-phase simulation + +The virtual input tape follows the native clamped input head. Two composite steps simulate +one second-machine step, including after the second machine has halted. +-/ + +@[expose] public section + +namespace Turing.MultiTapeTM.Composition + +variable {k₀ k₁ : ℕ} +variable {Symbol State₀ State₁ : Type*} + +variable (tm₀ : MultiTapeTM k₀ Symbol State₀) (tm₁ : MultiTapeTM k₁ Symbol State₁) + +/-- The virtual input cell in a second-phase embedding is exactly the native input symbol. -/ +private lemma embedSecond_inputSymbol + {firstInput : List Symbol} + (firstCfg : Cfg k₀ Symbol State₀ firstInput) + {secondInput : List Symbol} + (secondCfg : Cfg k₁ Symbol State₁ secondInput) : + (if inputMode secondCfg.inputPos = .inside then + (embedSecond tm₀ tm₁ firstCfg secondCfg).workTapeSymbols + (compositionIntermediateTapeIdx k₀ k₁) + else none) = secondCfg.inputSymbol := by + simp only [tapes, Cfg.workTapeSymbols, embedSecond, compositionIntermediateTapeIdx] + by_cases hleft : secondCfg.inputPos = 0 + · simp [inputMode, hleft, Cfg.inputSymbol] + · by_cases hright : secondCfg.inputPos.val = secondInput.length + 1 + · simp [inputMode, hleft, hright, Cfg.inputSymbol] + · have hp : 0 < secondCfg.inputPos.val := + Nat.pos_of_ne_zero (fun hz => hleft (Fin.ext hz)) + have hi : secondCfg.inputPos.val - 1 < secondInput.length := by omega + have hmode : inputMode secondCfg.inputPos = .inside := by + simp [inputMode, hleft, hright] + simp only [hmode, ↓reduceIte] + rw [inputSymbolInner (p := secondCfg.inputPos.val - 1) (by omega) hi] + have hz : ((secondCfg.inputPos.val : ℤ) - 1) = + (secondCfg.inputPos.val - 1 : ℕ) := by omega + rw [show virtualInputPos secondCfg.inputPos = + (secondCfg.inputPos.val : ℤ) - 1 by rfl, hz] + simp [listTape, hi] + +/-- A second-phase embedding preserves every symbol read from a second-machine work tape. -/ +private lemma compositionSecondWorkSymbols_embedSecond + {firstInput : List Symbol} + (firstCfg : Cfg k₀ Symbol State₀ firstInput) + {secondInput : List Symbol} + (secondCfg : Cfg k₁ Symbol State₁ secondInput) : + compositionSecondWorkSymbols + (embedSecond tm₀ tm₁ firstCfg secondCfg).workTapeSymbols = + secondCfg.workTapeSymbols := by + funext i + have hlt : ¬k₀ + 1 + i.val < k₀ := by omega + have hne : k₀ + 1 + i.val ≠ k₀ := by omega + simp [compositionSecondWorkSymbols, Cfg.workTapeSymbols, embedSecond, + compositionSecondTapeIdx, hlt, hne] + +/-- 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 [CompositionInputMode.move] + | neg => + by_cases hleft : p = 0 + · rw [hleft] + simp [inputMode, CompositionInputMode.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, CompositionInputMode.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, CompositionInputMode.move] + · rw [moveInputPos_pos_of_ne_right p hright] + unfold virtualInputPos + by_cases hleft : p = 0 <;> + simp [inputMode, hleft, hright, CompositionInputMode.move] + +/-- The boundary hint selected before a move is left whenever the resulting native position is +the left boundary. -/ +private lemma compositionNextBoundary_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 with + | zero => + have hp : p = 0 := by simpa using hmove + simp [hp, inputMode, CompositionInputMode.nextBoundary] + | neg => rfl + | pos => + by_cases hright : p.val = input.length + 1 + · have hp : p = ⟨input.length + 1, by omega⟩ := Fin.ext hright + rw [hp] at hmove + simp at hmove + · rw [moveInputPos_pos_of_ne_right p hright] at hmove + have hp := congrArg Fin.val hmove + simp at hp + +/-- The boundary hint selected before a move is right whenever the resulting native position is +the right boundary. -/ +private lemma compositionNextBoundary_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 with + | zero => + have hright : p.val = input.length + 1 := by simpa using hmove + have hleft : p ≠ 0 := by + intro h + rw [h] at hright + simp at hright + simp [inputMode, hright, hleft, CompositionInputMode.nextBoundary] + | pos => rfl + | neg => + by_cases hleft : p = 0 + · rw [hleft] at hmove + simp at hmove + · rw [moveInputPos_neg_of_ne_left p hleft] at hmove + simp at hmove + have hp : 0 < p.val := Nat.pos_of_ne_zero (fun hz => hleft (Fin.ext hz)) + 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 compositionClassifyMode_listTape {input : List Symbol} + (p : Fin (input.length + 2)) (boundary : CompositionBoundary) + (hleft : p = 0 → boundary = .left) + (hright : p.val = input.length + 1 → boundary = .right) : + compositionClassifyMode + (listTape input (virtualInputPos p)) boundary = + inputMode p := by + by_cases hp0 : p = 0 + · have hb := hleft hp0 + rw [hp0] + have hv : virtualInputPos (0 : Fin (input.length + 2)) = -1 := by + unfold virtualInputPos + simp + rw [hv] + simp [compositionClassifyMode, inputMode, hb, CompositionBoundary.inputMode] + rfl + · by_cases hpr : p.val = input.length + 1 + · have hb := hright hpr + have hp : p = ⟨input.length + 1, by omega⟩ := Fin.ext hpr + rw [hp] + have hv : virtualInputPos + (⟨input.length + 1, by omega⟩ : Fin (input.length + 2)) = input.length := by + unfold virtualInputPos + omega + rw [hv] + simp [compositionClassifyMode, inputMode, hb, CompositionBoundary.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 + rw [hv] + simp [compositionClassifyMode, 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 compositionClassifyMode_move {input : List Symbol} + (p : Fin (input.length + 2)) (move : SignType) : + compositionClassifyMode + (listTape input + (virtualInputPos p + (inputMode p).move move)) + ((inputMode p).nextBoundary move) = + inputMode (moveInputPos p move) := by + rw [← virtualInputPos_move p move] + apply compositionClassifyMode_listTape + · exact compositionNextBoundary_eq_left p move + · exact compositionNextBoundary_eq_right p move + +/-- The classifying half of a simulated second-machine step only restores the native input mode. -/ +lemma step_classifyCfg + {firstInput : List Symbol} + (firstCfg : Cfg k₀ Symbol State₀ firstInput) + {secondInput : List Symbol} + (secondCfg : Cfg k₁ Symbol State₁ secondInput) + (boundary : CompositionBoundary) + (hmode : + compositionClassifyMode + (listTape secondInput (virtualInputPos secondCfg.inputPos)) boundary = + inputMode secondCfg.inputPos) : + (comp tm₀ tm₁).step + (classifyCfg tm₀ tm₁ firstCfg secondCfg boundary) = + embedSecond tm₀ tm₁ firstCfg secondCfg := by + cases hstate : secondCfg.state with + | none => + simp [step, classifyCfg, embedSecond, hstate] + | some q => + apply Cfg.ext + · simp [step, classifyCfg, embedSecond, comp, hstate, + Cfg.workTapeSymbols, compositionIntermediateTapeIdx, hmode] + · simp [step, classifyCfg, embedSecond, comp, hstate] + · funext i p + simp [step, classifyCfg, embedSecond, comp, hstate, + idleWorkAction] + · funext i + simp [step, classifyCfg, embedSecond, comp, hstate, + idleWorkAction] + · simp [step, classifyCfg, embedSecond, comp, hstate] + +/-- The moving half of a simulated second-machine step performs all native tape actions and enters +the classifier state. -/ +private lemma step_embedSecond + {firstInput : List Symbol} + (firstCfg : Cfg k₀ Symbol State₀ firstInput) + {secondInput : List Symbol} + (secondCfg : Cfg k₁ Symbol State₁ secondInput) + (q : State₁) (hstate : secondCfg.state = some q) : + (comp tm₀ tm₁).step + (embedSecond tm₀ tm₁ firstCfg secondCfg) = + classifyCfg tm₀ tm₁ firstCfg (tm₁.step secondCfg) + ((inputMode secondCfg.inputPos).nextBoundary + (tm₁.tr q secondCfg.inputSymbol secondCfg.workTapeSymbols).inputMove) := by + have hinput := embedSecond_inputSymbol + tm₀ tm₁ firstCfg secondCfg + have hwork := compositionSecondWorkSymbols_embedSecond + tm₀ tm₁ firstCfg secondCfg + unfold step + rw [show + (embedSecond tm₀ tm₁ firstCfg secondCfg).state = + some (.second q (inputMode secondCfg.inputPos)) by + simp [embedSecond, hstate]] + rw [hstate] + simp only [comp] + rw [hinput, hwork] + generalize htr : tm₁.tr q secondCfg.inputSymbol secondCfg.workTapeSymbols = out + obtain ⟨inputMove, workActions, outS, q'⟩ := out + simp only [htr] + apply Cfg.ext + · cases q' <;> rfl + · simp [classifyCfg, embedSecond] + · funext i p + by_cases hfirst : i.val < k₀ + · simp [classifyCfg, embedSecond, compositionSecondWorkActions, + hstate, hfirst, idleWorkAction] + · by_cases hmiddle : i.val = k₀ + · simp [classifyCfg, embedSecond, compositionSecondWorkActions, + hstate, hmiddle] + · let j : Fin k₁ := ⟨i.val - (k₀ + 1), by + have hi := i.isLt + simp only [compositionTapeCount] at hi + omega⟩ + cases hwrite : (workActions j).1 with + | none => + simp [classifyCfg, embedSecond, + compositionSecondWorkActions, hstate, hfirst, hmiddle, + j, hwrite] + | some s => + simp [classifyCfg, embedSecond, + compositionSecondWorkActions, hstate, hfirst, hmiddle, j, hwrite] + · funext i + by_cases hfirst : i.val < k₀ + · simp [classifyCfg, embedSecond, compositionSecondWorkActions, + hstate, hfirst, idleWorkAction] + · by_cases hmiddle : i.val = k₀ + · simp only [tapes, embedSecond, hstate, hmiddle, lt_self_iff_false, ↓reduceDIte, + compositionSecondWorkActions, classifyCfg] + exact (virtualInputPos_move secondCfg.inputPos inputMove).symm + · simp [classifyCfg, embedSecond, compositionSecondWorkActions, + hstate, hfirst, hmiddle] + · rfl + +/-- One native second-machine step is exactly two steps of the composite machine. -/ +private lemma runFrom_two_embedSecond + {firstInput : List Symbol} + (firstCfg : Cfg k₀ Symbol State₀ firstInput) + {secondInput : List Symbol} + (secondCfg : Cfg k₁ Symbol State₁ secondInput) : + (comp tm₀ tm₁).runFrom + (embedSecond tm₀ tm₁ firstCfg secondCfg) 2 = + embedSecond tm₀ tm₁ firstCfg (tm₁.step secondCfg) := by + cases hstate : secondCfg.state with + | none => simp [runFrom, embedSecond, step, hstate] + | some q => + change (comp tm₀ tm₁).step + ((comp tm₀ tm₁).step (embedSecond tm₀ tm₁ firstCfg secondCfg)) = _ + rw [step_embedSecond tm₀ tm₁ firstCfg secondCfg q hstate] + apply step_classifyCfg + unfold step + rw [hstate] + generalize htr : tm₁.tr q secondCfg.inputSymbol secondCfg.workTapeSymbols = out + obtain ⟨inputMove, workActions, outS, q'⟩ := out + simp only [htr] + rw [virtualInputPos_move] + exact compositionClassifyMode_move secondCfg.inputPos inputMove + +/-- Simulation of the second machine, at a cost of two composite steps per native step. -/ +lemma runFrom_secondPhase + {firstInput : List Symbol} + (firstCfg : Cfg k₀ Symbol State₀ firstInput) + {secondInput : List Symbol} + (secondCfg : Cfg k₁ Symbol State₁ secondInput) + (n : ℕ) : + (comp tm₀ tm₁).runFrom + (embedSecond tm₀ tm₁ firstCfg secondCfg) (2 * n) = + embedSecond tm₀ tm₁ firstCfg + (tm₁.runFrom secondCfg n) := by + induction n with + | zero => simp [runFrom] + | succ n ih => + rw [show 2 * (n + 1) = 2 * n + 2 by omega, runFrom_add, ih, + runFrom_two_embedSecond, runFrom_succ_eq_step'] + +/-- The odd-numbered composite steps of the second phase are precisely the intermediate +classifier configurations. -/ +lemma runFrom_secondPhase_odd + {firstInput : List Symbol} + (firstCfg : Cfg k₀ Symbol State₀ firstInput) + {secondInput : List Symbol} + (secondCfg : Cfg k₁ Symbol State₁ secondInput) + (n : ℕ) : + ∃ boundary, + (comp tm₀ tm₁).runFrom + (embedSecond tm₀ tm₁ firstCfg secondCfg) (2 * n + 1) = + classifyCfg tm₀ tm₁ firstCfg + (tm₁.runFrom secondCfg (n + 1)) boundary := by + rw [runFrom_add, runFrom_secondPhase] + cases hstate : (tm₁.runFrom secondCfg n).state with + | none => + refine ⟨.right, ?_⟩ + change (comp tm₀ tm₁).step + (embedSecond tm₀ tm₁ firstCfg (tm₁.runFrom secondCfg n)) = _ + rw [runFrom_succ_eq_step', step_of_halt hstate] + simp [step, embedSecond, classifyCfg, hstate] + | some q => + refine ⟨(inputMode (tm₁.runFrom secondCfg n).inputPos).nextBoundary + (tm₁.tr q (tm₁.runFrom secondCfg n).inputSymbol + (tm₁.runFrom secondCfg n).workTapeSymbols).inputMove, ?_⟩ + change (comp tm₀ tm₁).step + (embedSecond tm₀ tm₁ firstCfg (tm₁.runFrom secondCfg n)) = _ + rw [step_embedSecond tm₀ tm₁ firstCfg _ q hstate, runFrom_succ_eq_step'] + +end Turing.MultiTapeTM.Composition diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index cc54495a3..426a1567d 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean @@ -6,8 +6,6 @@ Authors: Christian Reitwiessner 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 @@ -294,6 +292,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 +381,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,6 +415,15 @@ def ComputesInTimeAndSpace (tm.runFrom (tm.initCfg input) t).output = output ∧ tm.spaceUsed (tm.initCfg input) t = s +/-- 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 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. @@ -448,6 +488,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/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..726844cab 100644 --- a/CslibTests.lean +++ b/CslibTests.lean @@ -18,5 +18,6 @@ import CslibTests.MLL import CslibTests.Modal import CslibTests.Modal.Ideal import CslibTests.Modal.Stlc +import CslibTests.MultiTapeComposition import CslibTests.Reduction import CslibTests.StatefulProcesses diff --git a/CslibTests/MultiTapeComposition.lean b/CslibTests/MultiTapeComposition.lean new file mode 100644 index 000000000..cbcf41d57 --- /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.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 From a6d30db4766d7557c6fddf62434f8bbbdd31da21 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 5 Sep 2026 11:56:55 -0400 Subject: [PATCH 2/3] refactor(MultiTapeTM): golf composition proofs --- .../Turing/MultiTape/Composition.lean | 92 +++---------- .../Turing/MultiTape/Composition/Defs.lean | 12 +- .../Turing/MultiTape/Composition/Rewind.lean | 121 ++++-------------- .../MultiTape/Composition/Simulation.lean | 95 +++----------- 4 files changed, 65 insertions(+), 255 deletions(-) diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Composition.lean b/Cslib/Computability/Machines/Turing/MultiTape/Composition.lean index 2b7984f6e..dcaf584aa 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Composition.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Composition.lean @@ -58,34 +58,12 @@ theorem comp_haltsWithOutput (u + (out₀.length + 3) + 2 * v)).output = out₁ := by subst out₀ subst out₁ - have hmid : - (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)) := - runFrom_to_secondInit tm₀ tm₁ input u hhalt₀ hactive₀ - have hfinal : - (comp tm₀ tm₁).runFrom ((comp tm₀ tm₁).initCfg input) - (u + ((tm₀.runFrom (tm₀.initCfg input) u).output.length + 3) + 2 * v) = - embedSecond tm₀ tm₁ - (tm₀.runFrom (tm₀.initCfg input) u) - (tm₁.runFrom - (tm₁.initCfg ((tm₀.runFrom (tm₀.initCfg input) u).output)) v) := by - rw [(comp tm₀ tm₁).runFrom_add ((comp tm₀ tm₁).initCfg input) - (u + ((tm₀.runFrom (tm₀.initCfg input) u).output.length + 3)) (2 * v)] - rw [hmid] - exact runFrom_secondPhase tm₀ tm₁ - (tm₀.runFrom (tm₀.initCfg input) u) - (tm₁.initCfg ((tm₀.runFrom (tm₀.initCfg input) u).output)) v + 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] - constructor - · change Option.map _ - (tm₁.runFrom - (tm₁.initCfg ((tm₀.runFrom (tm₀.initCfg input) u).output)) v).state = none - rw [hhalt₁] - rfl - · rfl + simp only [embedSecond, hhalt₁, and_self] /-- Final first-component configuration used throughout the resource analysis. -/ @[simp] private abbrev firstFinalCfg @@ -214,22 +192,13 @@ def spaceBound (T₀ S₀ S₁ : ℕ → ℕ) (n : ℕ) : ℕ := /-- Sequential composition preserves monotonicity of time bounds. -/ lemma timeBound_mono {T₀ T₁ : ℕ → ℕ} (hT₀ : Monotone T₀) (hT₁ : Monotone T₁) : Monotone (timeBound T₀ T₁) := by - intro m n hmn - have hT₀mn := hT₀ hmn - have hT₁mn := hT₁ hT₀mn - simp only [timeBound] - omega + exact ((hT₀.const_mul' 2).add monotone_const).add ((hT₁.comp hT₀).const_mul' 2) /-- Sequential composition preserves monotonicity of space bounds. -/ lemma spaceBound_mono {T₀ S₀ S₁ : ℕ → ℕ} (hT₀ : Monotone T₀) (hS₀ : Monotone S₀) (hS₁ : Monotone S₁) : Monotone (spaceBound T₀ S₀ S₁) := by - intro m n hmn - have hT₀mn := hT₀ hmn - have hS₀mn := hS₀ hmn - have hS₁mn := hS₁ hT₀mn - simp only [spaceBound] - omega + exact (hS₀.add (hT₀.add monotone_const)).add (hS₁.comp hT₀) end Composition @@ -268,19 +237,11 @@ private lemma exists_firstComponent_tapePos_eq refine ⟨m, hm, ?_⟩ rw [hcfg] simp [embedFirst, compositionFirstTapeIdx] - | rewind _ _ hcfg => + | rewind _ _ hcfg | initialClassify hcfg => refine ⟨u, le_rfl, ?_⟩ rw [hcfg] simp [intermediateCfg, embedFirst, compositionFirstTapeIdx, hidx_ne] - | initialClassify hcfg => - refine ⟨u, le_rfl, ?_⟩ - rw [hcfg] - simp [intermediateCfg, embedFirst, compositionFirstTapeIdx, hidx_ne] - | second _ _ hcfg => - refine ⟨u, le_rfl, ?_⟩ - rw [hcfg] - simp [embedSecond, compositionFirstTapeIdx] - | secondClassify _ _ _ hcfg => + | second _ _ hcfg | secondClassify _ _ _ hcfg => refine ⟨u, le_rfl, ?_⟩ rw [hcfg] simp [classifyCfg, embedSecond, compositionFirstTapeIdx] @@ -305,12 +266,7 @@ private lemma exists_secondComponent_tapePos_eq rw [hcfg] simp [embedFirst, compositionSecondTapeIdx, secondCfgAt, secondInitCfg, runFrom, hidx_not_lt, hidx_ne] - | rewind _ _ hcfg => - refine ⟨0, Nat.zero_le _, ?_⟩ - rw [hcfg] - simp [intermediateCfg, embedFirst, compositionSecondTapeIdx, - secondCfgAt, secondInitCfg, runFrom, hidx_not_lt, hidx_ne] - | initialClassify hcfg => + | rewind _ _ hcfg | initialClassify hcfg => refine ⟨0, Nat.zero_le _, ?_⟩ rw [hcfg] simp [intermediateCfg, embedFirst, compositionSecondTapeIdx, @@ -379,27 +335,13 @@ private lemma compositionIntermediateSpace_le (compositionTotalTime tm₀ input u v) (compositionIntermediateTapeIdx k₀ k₁) ≤ (firstFinalCfg tm₀ input u).output.length + 2 := by - unfold spaceUsedByTape - have hsub : - (comp tm₀ tm₁).visitedByTapeHead - ((comp tm₀ tm₁).initCfg input) - (compositionTotalTime tm₀ input u v) - (compositionIntermediateTapeIdx k₀ k₁) ⊆ - Finset.Icc (-1) ((firstFinalCfg tm₀ input u).output.length : ℤ) := by - intro p hp - simp only [visitedByTapeHead, Finset.mem_image, Finset.mem_range] at hp - obtain ⟨r, hr, rfl⟩ := hp - exact compositionIntermediateTapePos_mem_Icc tm₀ tm₁ input u v r - hrun (by simpa [compositionTotalTime] using hr) - calc ((comp tm₀ tm₁).visitedByTapeHead - ((comp tm₀ tm₁).initCfg input) - (compositionTotalTime tm₀ input u v) - (compositionIntermediateTapeIdx k₀ k₁)).card - ≤ (Finset.Icc (-1) ((firstFinalCfg tm₀ input u).output.length : ℤ)).card := - Finset.card_le_card hsub - _ = (firstFinalCfg tm₀ input u).output.length + 2 := by - rw [Int.card_Icc] - omega + 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 diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Composition/Defs.lean b/Cslib/Computability/Machines/Turing/MultiTape/Composition/Defs.lean index 56e7f4c83..dc133928b 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Composition/Defs.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Composition/Defs.lean @@ -227,17 +227,11 @@ lemma listTape_append_single (xs : List Symbol) (x : Symbol) : cases z with | negSucc n => simp [listTape] | ofNat n => - simp only [listTape] - rw [List.getElem?_append] by_cases h : n = xs.length - · subst n - simp + · subst n; simp · by_cases hn : n < xs.length - · simp [hn, h] - · have hle : xs.length ≤ n := Nat.le_of_not_gt hn - have hlt : xs.length < n := lt_of_le_of_ne hle (Ne.symm h) - have hsub : n - xs.length ≠ 0 := by omega - simp [h, hn, hsub] + · simp [List.getElem?_append, hn, h] + · simp [List.getElem?_append, hn, h, show n - xs.length ≠ 0 by omega] /-- Embed a first-machine configuration into the first phase of the composite machine. -/ def embedFirst diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Composition/Rewind.lean b/Cslib/Computability/Machines/Turing/MultiTape/Composition/Rewind.lean index 501fe5e41..24bae8014 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Composition/Rewind.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Composition/Rewind.lean @@ -29,18 +29,11 @@ configuration. -/ private lemma embedFirst_initCfg (input : List Symbol) : embedFirst tm₀ tm₁ (tm₀.initCfg input) = (comp tm₀ tm₁).initCfg input := by - apply Cfg.ext - · rfl - · rfl + apply Cfg.ext <;> try rfl · funext i p - by_cases hfirst : i.val < k₀ - · simp [embedFirst, hfirst] - · by_cases hmiddle : i.val = k₀ - · cases p <;> simp [embedFirst, hmiddle, listTape] - · simp [embedFirst, hfirst, hmiddle] + cases p <;> simp [embedFirst, ite_apply, listTape] · funext i simp [embedFirst] - · rfl /-- The first-phase embedding preserves the symbol read from the real input. -/ @[simp] @@ -86,13 +79,9 @@ private lemma step_embedFirst {input : List Symbol} · cases hwrite : (workActions ⟨i.val, hfirst⟩).1 <;> simp [embedFirst, compositionFirstWorkActions, hfirst, hwrite] · by_cases hmiddle : i.val = k₀ - · cases outS with - | none => - simp [embedFirst, compositionFirstWorkActions, hmiddle, - idleWorkAction] - | some s => - simp [embedFirst, compositionFirstWorkActions, hmiddle, - listTape_append_single] + · cases outS <;> + simp [embedFirst, compositionFirstWorkActions, hmiddle, + idleWorkAction, listTape_append_single] · simp [embedFirst, compositionFirstWorkActions, hfirst, hmiddle, idleWorkAction] · funext i @@ -127,27 +116,10 @@ private lemma intermediateCfg_classify_init {input : List Symbol} intermediateCfg tm₀ tm₁ cfg (.classify tm₁.q₀ .right) 0 = classifyCfg tm₀ tm₁ cfg (tm₁.initCfg cfg.output) .right := by - apply Cfg.ext - · rfl - · rfl - · funext i p - by_cases hfirst : i.val < k₀ - · simp [intermediateCfg, embedFirst, classifyCfg, - embedSecond, hfirst] - · by_cases hmiddle : i.val = k₀ - · simp [intermediateCfg, embedFirst, classifyCfg, - embedSecond, hmiddle] - · simp [intermediateCfg, embedFirst, classifyCfg, - embedSecond, hfirst, hmiddle] - · funext i - by_cases hfirst : i.val < k₀ - · have hmiddle : i.val ≠ k₀ := by omega - simp [intermediateCfg, embedFirst, classifyCfg, - embedSecond, virtualInputPos, hfirst, hmiddle] - · by_cases hmiddle : i.val = k₀ <;> - simp [intermediateCfg, embedFirst, classifyCfg, - embedSecond, virtualInputPos, hfirst, hmiddle] - · rfl + ext i p <;> + simp [intermediateCfg, embedFirst, classifyCfg, embedSecond, virtualInputPos] + split_ifs <;> simp_all + omega /-- Entering the rewind phase moves the intermediate head one cell to the left. -/ private lemma step_rewindStart {input : List Symbol} @@ -155,21 +127,10 @@ private lemma step_rewindStart {input : List Symbol} (comp tm₀ tm₁).step (embedFirst tm₀ tm₁ cfg) = intermediateCfg tm₀ tm₁ cfg .rewind (cfg.output.length - 1) := by - apply Cfg.ext - · simp [step, embedFirst, intermediateCfg, comp, hhalt] - · simp [step, embedFirst, intermediateCfg, comp, hhalt] - · funext i p - by_cases hmiddle : i.val = k₀ <;> - simp [step, embedFirst, intermediateCfg, comp, hhalt, - compositionMoveIntermediate, idleWorkAction, hmiddle] - · funext i - by_cases hmiddle : i.val = k₀ - · simp [step, embedFirst, intermediateCfg, comp, hhalt, - compositionMoveIntermediate, idleWorkAction, hmiddle] - omega - · simp [step, embedFirst, intermediateCfg, comp, hhalt, - compositionMoveIntermediate, idleWorkAction, hmiddle] - · simp [step, embedFirst, intermediateCfg, comp, hhalt] + ext i p <;> + simp [step, embedFirst, intermediateCfg, comp, hhalt, + compositionMoveIntermediate, idleWorkAction] <;> + split_ifs <;> simp_all <;> omega /-- One rewind step over a nonblank intermediate cell. -/ private lemma step_rewind_some {input : List Symbol} @@ -178,24 +139,10 @@ private lemma step_rewind_some {input : List Symbol} (comp tm₀ tm₁).step (intermediateCfg tm₀ tm₁ cfg .rewind pos) = intermediateCfg tm₀ tm₁ cfg .rewind (pos - 1) := by - apply Cfg.ext - · simp [step, intermediateCfg, embedFirst, comp, - Cfg.workTapeSymbols, hcell, compositionMoveIntermediate, idleWorkAction] - · simp [step, intermediateCfg, embedFirst, comp, - Cfg.workTapeSymbols, hcell] - · funext i p - by_cases hmiddle : i.val = k₀ <;> - simp [step, intermediateCfg, embedFirst, comp, - Cfg.workTapeSymbols, hcell, compositionMoveIntermediate, idleWorkAction, hmiddle] - · funext i - by_cases hmiddle : i.val = k₀ - · simp [step, intermediateCfg, embedFirst, comp, - Cfg.workTapeSymbols, hcell, compositionMoveIntermediate, idleWorkAction, hmiddle] - omega - · simp [step, intermediateCfg, embedFirst, comp, - Cfg.workTapeSymbols, hcell, compositionMoveIntermediate, idleWorkAction, hmiddle] - · simp [step, intermediateCfg, embedFirst, comp, - Cfg.workTapeSymbols, hcell] + ext i p <;> + simp [step, intermediateCfg, embedFirst, comp, Cfg.workTapeSymbols, + hcell, compositionMoveIntermediate, idleWorkAction, sub_eq_add_neg] <;> + split_ifs <;> simp_all /-- The blank just left of the intermediate output ends rewinding and moves the head to cell zero for classification. -/ @@ -206,21 +153,10 @@ private lemma step_rewind_none {input : List Symbol} (intermediateCfg tm₀ tm₁ cfg .rewind pos) = intermediateCfg tm₀ tm₁ cfg (.classify tm₁.q₀ .right) (pos + 1) := by - apply Cfg.ext - · simp [step, intermediateCfg, embedFirst, comp, - Cfg.workTapeSymbols, hcell] - · simp [step, intermediateCfg, embedFirst, comp, - Cfg.workTapeSymbols, hcell] - · funext i p - by_cases hmiddle : i.val = k₀ <;> - simp [step, intermediateCfg, embedFirst, comp, - Cfg.workTapeSymbols, hcell, compositionMoveIntermediate, idleWorkAction, hmiddle] - · funext i - by_cases hmiddle : i.val = k₀ <;> - simp [step, intermediateCfg, embedFirst, comp, - Cfg.workTapeSymbols, hcell, compositionMoveIntermediate, idleWorkAction, hmiddle] - · simp [step, intermediateCfg, embedFirst, comp, - Cfg.workTapeSymbols, hcell] + ext i p <;> + simp [step, intermediateCfg, embedFirst, comp, Cfg.workTapeSymbols, + hcell, compositionMoveIntermediate, idleWorkAction] <;> + split_ifs <;> simp_all /-- A canonical list tape is nonblank at every position inside the represented list. -/ private lemma listTape_isSome_of_lt (xs : List Symbol) {r : ℕ} (h : r < xs.length) : @@ -243,13 +179,8 @@ private lemma runFrom_rewind {input : List Symbol} | zero => simp [runFrom] | succ r ih => rw [(comp tm₀ tm₁).runFrom_succ_eq_step', ih (by omega)] - have hcell : - (listTape cfg.output ((cfg.output.length : ℤ) - 1 - r)).isSome := by - simpa using - (listTape_isSome_of_lt cfg.output - (r := r) (show r < cfg.output.length by omega)) - convert step_rewind_some tm₀ tm₁ cfg - ((cfg.output.length : ℤ) - 1 - r) hcell using 1 + convert step_rewind_some tm₀ tm₁ cfg _ + (listTape_isSome_of_lt cfg.output (r := r) (by omega)) using 1 congr 1 omega @@ -272,8 +203,7 @@ lemma runFrom_firstHalt_classify {input : List Symbol} (embedFirst tm₀ tm₁ cfg) (cfg.output.length + 2) = intermediateCfg tm₀ tm₁ cfg (.classify tm₁.q₀ .right) 0 := by - rw [show cfg.output.length + 2 = (cfg.output.length + 1) + 1 by omega, - (comp tm₀ tm₁).runFrom_succ_eq_step'] + rw [(comp tm₀ tm₁).runFrom_succ_eq_step'] rw [runFrom_firstHalt_rewind tm₀ tm₁ cfg hhalt cfg.output.length le_rfl] rw [show (cfg.output.length : ℤ) - 1 - cfg.output.length = -1 by omega] simpa using step_rewind_none tm₀ tm₁ cfg (-1) (by rfl) @@ -298,8 +228,7 @@ private lemma runFrom_firstHalt_to_secondInit {input : List Symbol} (comp tm₀ tm₁).runFrom (embedFirst tm₀ tm₁ cfg) (cfg.output.length + 3) = embedSecond tm₀ tm₁ cfg (tm₁.initCfg cfg.output) := by - rw [show cfg.output.length + 3 = (cfg.output.length + 2) + 1 by omega, - (comp tm₀ tm₁).runFrom_succ_eq_step', runFrom_firstHalt_classify tm₀ tm₁ cfg hhalt] + rw [(comp tm₀ tm₁).runFrom_succ_eq_step', runFrom_firstHalt_classify tm₀ tm₁ cfg hhalt] exact step_intermediateCfg_classify_init tm₀ tm₁ cfg /-- Running the first phase and rewinding its output reaches the second machine's initial diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Composition/Simulation.lean b/Cslib/Computability/Machines/Turing/MultiTape/Composition/Simulation.lean index 464a7b8a0..2ca92416c 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Composition/Simulation.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Composition/Simulation.lean @@ -99,19 +99,9 @@ private lemma compositionNextBoundary_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 with - | zero => - have hp : p = 0 := by simpa using hmove - simp [hp, inputMode, CompositionInputMode.nextBoundary] - | neg => rfl - | pos => - by_cases hright : p.val = input.length + 1 - · have hp : p = ⟨input.length + 1, by omega⟩ := Fin.ext hright - rw [hp] at hmove - simp at hmove - · rw [moveInputPos_pos_of_ne_right p hright] at hmove - have hp := congrArg Fin.val hmove - simp at hp + cases move <;> + simp_all [inputMode, CompositionInputMode.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. -/ @@ -119,23 +109,9 @@ private lemma compositionNextBoundary_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 with - | zero => - have hright : p.val = input.length + 1 := by simpa using hmove - have hleft : p ≠ 0 := by - intro h - rw [h] at hright - simp at hright - simp [inputMode, hright, hleft, CompositionInputMode.nextBoundary] - | pos => rfl - | neg => - by_cases hleft : p = 0 - · rw [hleft] at hmove - simp at hmove - · rw [moveInputPos_neg_of_ne_left p hleft] at hmove - simp at hmove - have hp : 0 < p.val := Nat.pos_of_ne_zero (fun hz => hleft (Fin.ext hz)) - omega + cases move <;> + simp_all [inputMode, CompositionInputMode.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. -/ @@ -147,31 +123,18 @@ private lemma compositionClassifyMode_listTape {input : List Symbol} (listTape input (virtualInputPos p)) boundary = inputMode p := by by_cases hp0 : p = 0 - · have hb := hleft hp0 - rw [hp0] - have hv : virtualInputPos (0 : Fin (input.length + 2)) = -1 := by - unfold virtualInputPos - simp - rw [hv] - simp [compositionClassifyMode, inputMode, hb, CompositionBoundary.inputMode] + · simp [hp0, hleft hp0, virtualInputPos, inputMode, + compositionClassifyMode, CompositionBoundary.inputMode, listTape] rfl · by_cases hpr : p.val = input.length + 1 - · have hb := hright hpr - have hp : p = ⟨input.length + 1, by omega⟩ := Fin.ext hpr - rw [hp] - have hv : virtualInputPos - (⟨input.length + 1, by omega⟩ : Fin (input.length + 2)) = input.length := by - unfold virtualInputPos - omega - rw [hv] - simp [compositionClassifyMode, inputMode, hb, CompositionBoundary.inputMode] + · simp [virtualInputPos, hpr, hright hpr, inputMode, hp0, + compositionClassifyMode, CompositionBoundary.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 - rw [hv] - simp [compositionClassifyMode, inputMode, hp0, hpr, hi] + simp [hv, compositionClassifyMode, inputMode, hp0, hpr, hi] /-- Classifying the intermediate cell reached by a virtual move recovers the native clamped input-head mode after that move. -/ @@ -202,20 +165,11 @@ lemma step_classifyCfg (classifyCfg tm₀ tm₁ firstCfg secondCfg boundary) = embedSecond tm₀ tm₁ firstCfg secondCfg := by cases hstate : secondCfg.state with - | none => - simp [step, classifyCfg, embedSecond, hstate] + | none => simp [step, classifyCfg, embedSecond, hstate] | some q => - apply Cfg.ext - · simp [step, classifyCfg, embedSecond, comp, hstate, - Cfg.workTapeSymbols, compositionIntermediateTapeIdx, hmode] - · simp [step, classifyCfg, embedSecond, comp, hstate] - · funext i p - simp [step, classifyCfg, embedSecond, comp, hstate, - idleWorkAction] - · funext i + ext i p <;> simp [step, classifyCfg, embedSecond, comp, hstate, - idleWorkAction] - · simp [step, classifyCfg, embedSecond, comp, hstate] + Cfg.workTapeSymbols, compositionIntermediateTapeIdx, hmode, idleWorkAction] /-- The moving half of a simulated second-machine step performs all native tape actions and enters the classifier state. -/ @@ -259,14 +213,9 @@ private lemma step_embedSecond have hi := i.isLt simp only [compositionTapeCount] at hi omega⟩ - cases hwrite : (workActions j).1 with - | none => - simp [classifyCfg, embedSecond, - compositionSecondWorkActions, hstate, hfirst, hmiddle, - j, hwrite] - | some s => - simp [classifyCfg, embedSecond, - compositionSecondWorkActions, hstate, hfirst, hmiddle, j, hwrite] + cases hwrite : (workActions j).1 <;> + simp [classifyCfg, embedSecond, compositionSecondWorkActions, + hstate, hfirst, hmiddle, j, hwrite] · funext i by_cases hfirst : i.val < k₀ · simp [classifyCfg, embedSecond, compositionSecondWorkActions, @@ -295,13 +244,9 @@ private lemma runFrom_two_embedSecond ((comp tm₀ tm₁).step (embedSecond tm₀ tm₁ firstCfg secondCfg)) = _ rw [step_embedSecond tm₀ tm₁ firstCfg secondCfg q hstate] apply step_classifyCfg - unfold step - rw [hstate] - generalize htr : tm₁.tr q secondCfg.inputSymbol secondCfg.workTapeSymbols = out - obtain ⟨inputMove, workActions, outS, q'⟩ := out - simp only [htr] - rw [virtualInputPos_move] - exact compositionClassifyMode_move secondCfg.inputPos inputMove + simpa only [step, hstate, virtualInputPos_move] using + compositionClassifyMode_move secondCfg.inputPos + (tm₁.tr q secondCfg.inputSymbol secondCfg.workTapeSymbols).inputMove /-- Simulation of the second machine, at a cost of two composite steps per native step. -/ lemma runFrom_secondPhase From 2091c98c3e795d7c3703b36be0bcdc87de7a0dd0 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 5 Sep 2026 17:00:19 -0400 Subject: [PATCH 3/3] refactor(MultiTapeTM): compose reusable machine transformations --- Cslib.lean | 19 +- .../Turing/MultiTape/Combinators/Comp.lean | 82 +++++ .../Turing/MultiTape/Combinators/README.md | 14 + .../Turing/MultiTape/Composition/Defs.lean | 313 ------------------ .../Turing/MultiTape/Composition/Rewind.lean | 247 -------------- .../MultiTape/Composition/Simulation.lean | 297 ----------------- .../Turing/MultiTape/Deterministic.lean | 90 ++--- .../Turing/MultiTape/NormalForms/README.md | 9 + .../MultiTape/NormalForms/RewindInput.lean | 83 +++++ .../Turing/MultiTape/Plumbing/Basic.lean | 76 +++++ .../MultiTape/{ => Plumbing}/Composition.lean | 77 +---- .../MultiTape/Plumbing/Composition/Defs.lean | 175 ++++++++++ .../Plumbing/Composition/Layout.lean | 81 +++++ .../Plumbing/Composition/Rewind.lean | 152 +++++++++ .../Plumbing/Composition/Simulation.lean | 86 +++++ .../MultiTape/Plumbing/ExtendTapes.lean | 137 ++++++++ .../MultiTape/Plumbing/InputFromWorkTape.lean | 214 ++++++++++++ .../Plumbing/InputFromWorkTape/Defs.lean | 126 +++++++ .../MultiTape/Plumbing/OutputToWorkTape.lean | 95 ++++++ .../Turing/MultiTape/Plumbing/README.md | 20 ++ .../Turing/MultiTape/Plumbing/Rewind.lean | 177 ++++++++++ .../Turing/MultiTape/Plumbing/Sequential.lean | 100 ++++++ .../MultiTape/Plumbing/TapeContents.lean | 55 +++ CslibTests.lean | 1 + CslibTests/MultiTapeComposition.lean | 2 +- CslibTests/MultiTapePlumbing.lean | 109 ++++++ 26 files changed, 1868 insertions(+), 969 deletions(-) create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Combinators/Comp.lean create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Combinators/README.md delete mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Composition/Defs.lean delete mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Composition/Rewind.lean delete mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Composition/Simulation.lean create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/NormalForms/README.md create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/NormalForms/RewindInput.lean create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Basic.lean rename Cslib/Computability/Machines/Turing/MultiTape/{ => Plumbing}/Composition.lean (81%) create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Composition/Defs.lean create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Composition/Layout.lean create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Composition/Rewind.lean create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Composition/Simulation.lean create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ExtendTapes.lean create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Plumbing/InputFromWorkTape.lean create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Plumbing/InputFromWorkTape/Defs.lean create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Plumbing/OutputToWorkTape.lean create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Plumbing/README.md create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Rewind.lean create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Sequential.lean create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Plumbing/TapeContents.lean create mode 100644 CslibTests/MultiTapePlumbing.lean diff --git a/Cslib.lean b/Cslib.lean index 485eb15eb..e75bf0e4d 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -46,11 +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.Composition -public import Cslib.Computability.Machines.Turing.MultiTape.Composition.Defs -public import Cslib.Computability.Machines.Turing.MultiTape.Composition.Rewind -public import Cslib.Computability.Machines.Turing.MultiTape.Composition.Simulation +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/Composition/Defs.lean b/Cslib/Computability/Machines/Turing/MultiTape/Composition/Defs.lean deleted file mode 100644 index dc133928b..000000000 --- a/Cslib/Computability/Machines/Turing/MultiTape/Composition/Defs.lean +++ /dev/null @@ -1,313 +0,0 @@ -/- -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 - -/-! -# 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 - -/-- Location of the virtual input head during the second phase. -/ -inductive CompositionInputMode - | left - | inside - | right -deriving DecidableEq - -/-- Boundary toward which a virtual input-head move was made. -/ -inductive CompositionBoundary - | left - | right - -/-- Control states of a composed multi-tape Turing machine. -/ -inductive CompositionState (State₀ State₁ : Type*) - | first (q : State₀) - | rewindStart - | rewind - | second (q : State₁) (mode : CompositionInputMode) - | classify (q : State₁) (boundary : CompositionBoundary) - -/-- Assemble the first work-tape block, the intermediate tape, and the second block. -The same layout is used for tape contents, head positions, and transition actions. -/ -@[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⟩ - -/-- A work-tape action that neither writes nor moves. -/ -def idleWorkAction : Option (Option Symbol) × SignType := (none, 0) - -/-- Movement of the virtual input head, with outward boundary moves clamped. -/ -def CompositionInputMode.move : CompositionInputMode → 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 CompositionInputMode.nextBoundary : - CompositionInputMode → SignType → CompositionBoundary - | _, .neg | .left, .zero => .left - | _, _ => .right - -/-- Convert a boundary classifier result to an input mode. -/ -def CompositionBoundary.inputMode : CompositionBoundary → CompositionInputMode - | .left => .left - | .right => .right - -/-- Read the work symbols seen by the first component machine. -/ -def compositionFirstWorkSymbols - (work : Fin (compositionTapeCount k₀ k₁) → Option Symbol) : - Fin k₀ → Option Symbol := - fun i => work (compositionFirstTapeIdx k₁ i) - -/-- Read the work symbols seen by the second component machine. -/ -def compositionSecondWorkSymbols - (work : Fin (compositionTapeCount k₀ k₁) → Option Symbol) : - Fin k₁ → Option Symbol := - fun i => work (compositionSecondTapeIdx k₀ k₁ i) - -/-- Embed the first component's work actions and redirect its output to the intermediate tape. -/ -def compositionFirstWorkActions - (actions : Fin k₀ → Option (Option Symbol) × SignType) - (outS : Option Symbol) : - Fin (compositionTapeCount k₀ k₁) → - Option (Option Symbol) × SignType := - Composition.tapes actions - (match outS with | none => idleWorkAction | some s => (some (some s), 1)) - (fun _ => idleWorkAction) - -/-- Park every tape except the intermediate tape and move that tape by `move`. -/ -def compositionMoveIntermediate (move : SignType) : - Fin (compositionTapeCount k₀ k₁) → - Option (Option Symbol) × SignType := - Composition.tapes (fun _ => idleWorkAction) (none, move) (fun _ => idleWorkAction) - -/-- Embed the second component's work actions and move the intermediate virtual-input tape. -/ -def compositionSecondWorkActions - (inputMove : SignType) - (actions : Fin k₁ → Option (Option Symbol) × SignType) : - Fin (compositionTapeCount k₀ k₁) → - Option (Option Symbol) × SignType := - Composition.tapes (fun _ => idleWorkAction) (none, inputMove) actions - -/-- Classify a virtual-input cell after moving onto it. -/ -def compositionClassifyMode - (cell : Option Symbol) - (boundary : CompositionBoundary) : CompositionInputMode := - if cell.isSome then .inside else boundary.inputMode - -/-- Sequential composition of two deterministic multi-tape Turing machines. -/ -def comp - (tm₀ : MultiTapeTM k₀ Symbol State₀) - (tm₁ : MultiTapeTM k₁ Symbol State₁) : - MultiTapeTM (compositionTapeCount k₀ k₁) Symbol - (CompositionState State₀ State₁) where - q₀ := .first tm₀.q₀ - tr q input work := - match q with - | .first q₀ => - let out := tm₀.tr q₀ input (compositionFirstWorkSymbols work) - { - inputMove := out.inputMove - workActions := compositionFirstWorkActions out.workActions out.outS - outS := none - q' := some (match out.q' with - | some q' => .first q' - | none => .rewindStart) - } - | .rewindStart => - { - inputMove := 0 - workActions := compositionMoveIntermediate (-1) - outS := none - q' := some .rewind - } - | .rewind => - if (work (compositionIntermediateTapeIdx k₀ k₁)).isSome then - { - inputMove := 0 - workActions := compositionMoveIntermediate (-1) - outS := none - q' := some .rewind - } - else - { - inputMove := 0 - workActions := compositionMoveIntermediate 1 - outS := none - q' := some (.classify tm₁.q₀ .right) - } - | .second q₁ mode => - let inputMove := mode.move - let out := tm₁.tr q₁ - (if mode = .inside then work (compositionIntermediateTapeIdx k₀ k₁) else none) - (compositionSecondWorkSymbols work) - { - inputMove := 0 - workActions := compositionSecondWorkActions (inputMove out.inputMove) out.workActions - outS := out.outS - q' := out.q'.map fun q' => .classify q' (mode.nextBoundary out.inputMove) - } - | .classify q₁ boundary => - { - inputMove := 0 - workActions := fun _ => idleWorkAction - outS := none - q' := some (.second q₁ - (compositionClassifyMode (work (compositionIntermediateTapeIdx k₀ k₁)) boundary)) - } - -namespace Composition - -/-- 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] - -/-- 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 (.first q) - | none => some .rewindStart - inputPos := cfg.inputPos - workTapes := tapes cfg.workTapes (listTape cfg.output) (fun _ _ => none) - workTapePos := tapes cfg.workTapePos cfg.output.length (fun _ => 0) - output := [] - -/-- 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)) : CompositionInputMode := - if p = 0 then .left else if p.val = input.length + 1 then .right else .inside - -/-- 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 (.second q (inputMode secondCfg.inputPos)) - | none => none - inputPos := firstCfg.inputPos - workTapes := tapes firstCfg.workTapes (listTape secondInput) secondCfg.workTapes - workTapePos := tapes firstCfg.workTapePos - (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 : CompositionBoundary) : - Cfg (compositionTapeCount k₀ k₁) Symbol - (CompositionState State₀ State₁) firstInput := - { embedSecond _tm₀ _tm₁ firstCfg secondCfg with - state := secondCfg.state.map fun q => .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/Composition/Rewind.lean b/Cslib/Computability/Machines/Turing/MultiTape/Composition/Rewind.lean deleted file mode 100644 index 24bae8014..000000000 --- a/Cslib/Computability/Machines/Turing/MultiTape/Composition/Rewind.lean +++ /dev/null @@ -1,247 +0,0 @@ -/- -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.Composition.Simulation - -/-! -# First-phase simulation and handoff - -The first machine runs in lockstep with the composite. Its output is rewound to the left -boundary, then classified to establish the second machine's initial configuration. --/ - -@[expose] public section - -namespace Turing.MultiTapeTM.Composition - -variable {k₀ k₁ : ℕ} -variable {Symbol State₀ State₁ : Type*} - -variable (tm₀ : MultiTapeTM k₀ Symbol State₀) (tm₁ : MultiTapeTM k₁ Symbol State₁) - -/-- The first-phase embedding sends an initial configuration to the composite initial -configuration. -/ -private 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-phase embedding preserves the symbol read from the real input. -/ -@[simp] -private lemma embedFirst_inputSymbol {input : List Symbol} - (cfg : Cfg k₀ Symbol State₀ input) : - (embedFirst tm₀ tm₁ cfg).inputSymbol = cfg.inputSymbol := rfl - -/-- The first-phase embedding preserves every symbol read from a first-machine work tape. -/ -private lemma compositionFirstWorkSymbols_embedFirst {input : List Symbol} - (cfg : Cfg k₀ Symbol State₀ input) : - compositionFirstWorkSymbols - (embedFirst tm₀ tm₁ cfg).workTapeSymbols = - cfg.workTapeSymbols := by - funext i - simp [compositionFirstWorkSymbols, Cfg.workTapeSymbols, embedFirst, - compositionFirstTapeIdx] - -/-- One first-machine step is one composite first-phase step. A halt of the first machine enters -the rewind phase instead of halting the composite machine. -/ -private lemma step_embedFirst {input : List Symbol} - (cfg : Cfg k₀ Symbol State₀ input) (hactive : cfg.state ≠ none) : - (comp tm₀ tm₁).step (embedFirst tm₀ tm₁ cfg) = - embedFirst tm₀ tm₁ (tm₀.step cfg) := by - cases hstate : cfg.state with - | none => exact absurd hstate hactive - | some q => - have hinput := embedFirst_inputSymbol tm₀ tm₁ cfg - have hwork := compositionFirstWorkSymbols_embedFirst tm₀ tm₁ cfg - unfold step - rw [show (embedFirst tm₀ tm₁ cfg).state = - some (.first q) by simp [embedFirst, hstate]] - rw [hstate] - simp only [comp] - rw [hinput, hwork] - generalize htr : tm₀.tr q cfg.inputSymbol cfg.workTapeSymbols = trOut - obtain ⟨inputMove, workActions, outS, q'⟩ := trOut - simp only [htr] - apply Cfg.ext - · cases q' <;> rfl - · rfl - · funext i p - by_cases hfirst : i.val < k₀ - · cases hwrite : (workActions ⟨i.val, hfirst⟩).1 <;> - simp [embedFirst, compositionFirstWorkActions, hfirst, hwrite] - · by_cases hmiddle : i.val = k₀ - · cases outS <;> - simp [embedFirst, compositionFirstWorkActions, hmiddle, - idleWorkAction, listTape_append_single] - · simp [embedFirst, compositionFirstWorkActions, hfirst, hmiddle, - idleWorkAction] - · funext i - by_cases hfirst : i.val < k₀ - · simp [embedFirst, compositionFirstWorkActions, hfirst] - · by_cases hmiddle : i.val = k₀ - · cases outS <;> - simp [embedFirst, compositionFirstWorkActions, hmiddle, - idleWorkAction] - · simp [embedFirst, compositionFirstWorkActions, hfirst, hmiddle, - idleWorkAction] - · rfl - -/-- Simulation of the first component up to a time at which it has not halted earlier. -/ -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 - induction n with - | zero => simpa using (embedFirst_initCfg tm₀ tm₁ input).symm - | succ n ih => - rw [tm₀.runFrom_succ_eq_step', (comp tm₀ tm₁).runFrom_succ_eq_step', - ih (fun m hm => hactive m (by omega))] - exact step_embedFirst tm₀ tm₁ - (tm₀.runFrom (tm₀.initCfg input) n) (hactive n (by omega)) - -/-- At position zero, the post-rewind classifier configuration is the classifier half of the -second machine's initial configuration. -/ -private lemma intermediateCfg_classify_init {input : List Symbol} - (cfg : Cfg k₀ Symbol State₀ input) : - intermediateCfg tm₀ tm₁ cfg - (.classify tm₁.q₀ .right) 0 = - classifyCfg tm₀ tm₁ cfg (tm₁.initCfg cfg.output) .right := by - ext i p <;> - simp [intermediateCfg, embedFirst, classifyCfg, embedSecond, virtualInputPos] - split_ifs <;> simp_all - omega - -/-- Entering the rewind phase moves the intermediate head one cell to the left. -/ -private lemma step_rewindStart {input : List Symbol} - (cfg : Cfg k₀ Symbol State₀ input) (hhalt : cfg.state = none) : - (comp tm₀ tm₁).step (embedFirst tm₀ tm₁ cfg) = - intermediateCfg tm₀ tm₁ cfg .rewind - (cfg.output.length - 1) := by - ext i p <;> - simp [step, embedFirst, intermediateCfg, comp, hhalt, - compositionMoveIntermediate, idleWorkAction] <;> - split_ifs <;> simp_all <;> omega - -/-- One rewind step over a nonblank intermediate cell. -/ -private lemma step_rewind_some {input : List Symbol} - (cfg : Cfg k₀ Symbol State₀ input) (pos : ℤ) - (hcell : (listTape cfg.output pos).isSome) : - (comp tm₀ tm₁).step - (intermediateCfg tm₀ tm₁ cfg .rewind pos) = - intermediateCfg tm₀ tm₁ cfg .rewind (pos - 1) := by - ext i p <;> - simp [step, intermediateCfg, embedFirst, comp, Cfg.workTapeSymbols, - hcell, compositionMoveIntermediate, idleWorkAction, sub_eq_add_neg] <;> - split_ifs <;> simp_all - -/-- The blank just left of the intermediate output ends rewinding and moves the head to cell -zero for classification. -/ -private lemma step_rewind_none {input : List Symbol} - (cfg : Cfg k₀ Symbol State₀ input) (pos : ℤ) - (hcell : listTape cfg.output pos = none) : - (comp tm₀ tm₁).step - (intermediateCfg tm₀ tm₁ cfg .rewind pos) = - intermediateCfg tm₀ tm₁ cfg - (.classify tm₁.q₀ .right) (pos + 1) := by - ext i p <;> - simp [step, intermediateCfg, embedFirst, comp, Cfg.workTapeSymbols, - hcell, compositionMoveIntermediate, idleWorkAction] <;> - split_ifs <;> simp_all - -/-- A canonical list tape is nonblank at every position inside the represented list. -/ -private lemma listTape_isSome_of_lt (xs : List Symbol) {r : ℕ} (h : r < xs.length) : - (listTape xs ((xs.length : ℤ) - 1 - r)).isSome := by - have hp : (xs.length : ℤ) - 1 - r = (xs.length - 1 - r : ℕ) := by omega - rw [hp] - simp [listTape] - omega - -/-- Rewinding scans exactly the cells occupied by the intermediate output. -/ -private lemma runFrom_rewind {input : List Symbol} - (cfg : Cfg k₀ Symbol State₀ input) - (r : ℕ) (hr : r ≤ cfg.output.length) : - (comp tm₀ tm₁).runFrom - (intermediateCfg tm₀ tm₁ cfg .rewind - ((cfg.output.length : ℤ) - 1)) r = - intermediateCfg tm₀ tm₁ cfg .rewind - ((cfg.output.length : ℤ) - 1 - r) := by - induction r with - | zero => simp [runFrom] - | succ r ih => - rw [(comp tm₀ tm₁).runFrom_succ_eq_step', ih (by omega)] - convert step_rewind_some tm₀ tm₁ cfg _ - (listTape_isSome_of_lt cfg.output (r := r) (by omega)) using 1 - congr 1 - omega - -/-- The prefix of the post-halting phase that consists of entering and running the rewind loop. -/ -lemma runFrom_firstHalt_rewind {input : List Symbol} - (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 .rewind - ((cfg.output.length : ℤ) - 1 - r) := by - rw [(comp tm₀ tm₁).runFrom_succ_eq_step, step_rewindStart tm₀ tm₁ cfg hhalt] - exact runFrom_rewind tm₀ tm₁ cfg r hr - -/-- The configuration immediately after the rewind loop is the initial classifier -configuration at intermediate-tape position zero. -/ -lemma runFrom_firstHalt_classify {input : List Symbol} - (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 - (.classify tm₁.q₀ .right) 0 := by - rw [(comp tm₀ tm₁).runFrom_succ_eq_step'] - rw [runFrom_firstHalt_rewind tm₀ tm₁ cfg hhalt cfg.output.length le_rfl] - rw [show (cfg.output.length : ℤ) - 1 - cfg.output.length = -1 by omega] - simpa using step_rewind_none tm₀ tm₁ cfg (-1) (by rfl) - -/-- After rewinding, one classification step enters the second machine's initial configuration. -/ -private lemma step_intermediateCfg_classify_init {input : List Symbol} - (cfg : Cfg k₀ Symbol State₀ input) : - (comp tm₀ tm₁).step - (intermediateCfg tm₀ tm₁ cfg - (.classify tm₁.q₀ .right) 0) = - embedSecond tm₀ tm₁ cfg (tm₁.initCfg cfg.output) := by - rw [intermediateCfg_classify_init] - apply step_classifyCfg - cases cfg.output <;> - simp [compositionClassifyMode, inputMode, virtualInputPos, - CompositionBoundary.inputMode, listTape] - -/-- Starting from a halted first-machine configuration, rewinding and initialization take exactly -the output length plus three steps. -/ -private lemma runFrom_firstHalt_to_secondInit {input : List Symbol} - (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 [(comp tm₀ tm₁).runFrom_succ_eq_step', runFrom_firstHalt_classify tm₀ tm₁ cfg hhalt] - exact step_intermediateCfg_classify_init tm₀ tm₁ cfg - -/-- Running the first phase and rewinding its output reaches the second machine's initial -configuration. -/ -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 [(comp tm₀ tm₁).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/Composition/Simulation.lean b/Cslib/Computability/Machines/Turing/MultiTape/Composition/Simulation.lean deleted file mode 100644 index 2ca92416c..000000000 --- a/Cslib/Computability/Machines/Turing/MultiTape/Composition/Simulation.lean +++ /dev/null @@ -1,297 +0,0 @@ -/- -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.Composition.Defs - -/-! -# Second-phase simulation - -The virtual input tape follows the native clamped input head. Two composite steps simulate -one second-machine step, including after the second machine has halted. --/ - -@[expose] public section - -namespace Turing.MultiTapeTM.Composition - -variable {k₀ k₁ : ℕ} -variable {Symbol State₀ State₁ : Type*} - -variable (tm₀ : MultiTapeTM k₀ Symbol State₀) (tm₁ : MultiTapeTM k₁ Symbol State₁) - -/-- The virtual input cell in a second-phase embedding is exactly the native input symbol. -/ -private lemma embedSecond_inputSymbol - {firstInput : List Symbol} - (firstCfg : Cfg k₀ Symbol State₀ firstInput) - {secondInput : List Symbol} - (secondCfg : Cfg k₁ Symbol State₁ secondInput) : - (if inputMode secondCfg.inputPos = .inside then - (embedSecond tm₀ tm₁ firstCfg secondCfg).workTapeSymbols - (compositionIntermediateTapeIdx k₀ k₁) - else none) = secondCfg.inputSymbol := by - simp only [tapes, Cfg.workTapeSymbols, embedSecond, compositionIntermediateTapeIdx] - by_cases hleft : secondCfg.inputPos = 0 - · simp [inputMode, hleft, Cfg.inputSymbol] - · by_cases hright : secondCfg.inputPos.val = secondInput.length + 1 - · simp [inputMode, hleft, hright, Cfg.inputSymbol] - · have hp : 0 < secondCfg.inputPos.val := - Nat.pos_of_ne_zero (fun hz => hleft (Fin.ext hz)) - have hi : secondCfg.inputPos.val - 1 < secondInput.length := by omega - have hmode : inputMode secondCfg.inputPos = .inside := by - simp [inputMode, hleft, hright] - simp only [hmode, ↓reduceIte] - rw [inputSymbolInner (p := secondCfg.inputPos.val - 1) (by omega) hi] - have hz : ((secondCfg.inputPos.val : ℤ) - 1) = - (secondCfg.inputPos.val - 1 : ℕ) := by omega - rw [show virtualInputPos secondCfg.inputPos = - (secondCfg.inputPos.val : ℤ) - 1 by rfl, hz] - simp [listTape, hi] - -/-- A second-phase embedding preserves every symbol read from a second-machine work tape. -/ -private lemma compositionSecondWorkSymbols_embedSecond - {firstInput : List Symbol} - (firstCfg : Cfg k₀ Symbol State₀ firstInput) - {secondInput : List Symbol} - (secondCfg : Cfg k₁ Symbol State₁ secondInput) : - compositionSecondWorkSymbols - (embedSecond tm₀ tm₁ firstCfg secondCfg).workTapeSymbols = - secondCfg.workTapeSymbols := by - funext i - have hlt : ¬k₀ + 1 + i.val < k₀ := by omega - have hne : k₀ + 1 + i.val ≠ k₀ := by omega - simp [compositionSecondWorkSymbols, Cfg.workTapeSymbols, embedSecond, - compositionSecondTapeIdx, hlt, hne] - -/-- 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 [CompositionInputMode.move] - | neg => - by_cases hleft : p = 0 - · rw [hleft] - simp [inputMode, CompositionInputMode.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, CompositionInputMode.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, CompositionInputMode.move] - · rw [moveInputPos_pos_of_ne_right p hright] - unfold virtualInputPos - by_cases hleft : p = 0 <;> - simp [inputMode, hleft, hright, CompositionInputMode.move] - -/-- The boundary hint selected before a move is left whenever the resulting native position is -the left boundary. -/ -private lemma compositionNextBoundary_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, CompositionInputMode.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 compositionNextBoundary_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, CompositionInputMode.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 compositionClassifyMode_listTape {input : List Symbol} - (p : Fin (input.length + 2)) (boundary : CompositionBoundary) - (hleft : p = 0 → boundary = .left) - (hright : p.val = input.length + 1 → boundary = .right) : - compositionClassifyMode - (listTape input (virtualInputPos p)) boundary = - inputMode p := by - by_cases hp0 : p = 0 - · simp [hp0, hleft hp0, virtualInputPos, inputMode, - compositionClassifyMode, CompositionBoundary.inputMode, listTape] - rfl - · by_cases hpr : p.val = input.length + 1 - · simp [virtualInputPos, hpr, hright hpr, inputMode, hp0, - compositionClassifyMode, CompositionBoundary.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, compositionClassifyMode, 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 compositionClassifyMode_move {input : List Symbol} - (p : Fin (input.length + 2)) (move : SignType) : - compositionClassifyMode - (listTape input - (virtualInputPos p + (inputMode p).move move)) - ((inputMode p).nextBoundary move) = - inputMode (moveInputPos p move) := by - rw [← virtualInputPos_move p move] - apply compositionClassifyMode_listTape - · exact compositionNextBoundary_eq_left p move - · exact compositionNextBoundary_eq_right p move - -/-- The classifying half of a simulated second-machine step only restores the native input mode. -/ -lemma step_classifyCfg - {firstInput : List Symbol} - (firstCfg : Cfg k₀ Symbol State₀ firstInput) - {secondInput : List Symbol} - (secondCfg : Cfg k₁ Symbol State₁ secondInput) - (boundary : CompositionBoundary) - (hmode : - compositionClassifyMode - (listTape secondInput (virtualInputPos secondCfg.inputPos)) boundary = - inputMode secondCfg.inputPos) : - (comp tm₀ tm₁).step - (classifyCfg tm₀ tm₁ firstCfg secondCfg boundary) = - embedSecond tm₀ tm₁ firstCfg secondCfg := by - cases hstate : secondCfg.state with - | none => simp [step, classifyCfg, embedSecond, hstate] - | some q => - ext i p <;> - simp [step, classifyCfg, embedSecond, comp, hstate, - Cfg.workTapeSymbols, compositionIntermediateTapeIdx, hmode, idleWorkAction] - -/-- The moving half of a simulated second-machine step performs all native tape actions and enters -the classifier state. -/ -private lemma step_embedSecond - {firstInput : List Symbol} - (firstCfg : Cfg k₀ Symbol State₀ firstInput) - {secondInput : List Symbol} - (secondCfg : Cfg k₁ Symbol State₁ secondInput) - (q : State₁) (hstate : secondCfg.state = some q) : - (comp tm₀ tm₁).step - (embedSecond tm₀ tm₁ firstCfg secondCfg) = - classifyCfg tm₀ tm₁ firstCfg (tm₁.step secondCfg) - ((inputMode secondCfg.inputPos).nextBoundary - (tm₁.tr q secondCfg.inputSymbol secondCfg.workTapeSymbols).inputMove) := by - have hinput := embedSecond_inputSymbol - tm₀ tm₁ firstCfg secondCfg - have hwork := compositionSecondWorkSymbols_embedSecond - tm₀ tm₁ firstCfg secondCfg - unfold step - rw [show - (embedSecond tm₀ tm₁ firstCfg secondCfg).state = - some (.second q (inputMode secondCfg.inputPos)) by - simp [embedSecond, hstate]] - rw [hstate] - simp only [comp] - rw [hinput, hwork] - generalize htr : tm₁.tr q secondCfg.inputSymbol secondCfg.workTapeSymbols = out - obtain ⟨inputMove, workActions, outS, q'⟩ := out - simp only [htr] - apply Cfg.ext - · cases q' <;> rfl - · simp [classifyCfg, embedSecond] - · funext i p - by_cases hfirst : i.val < k₀ - · simp [classifyCfg, embedSecond, compositionSecondWorkActions, - hstate, hfirst, idleWorkAction] - · by_cases hmiddle : i.val = k₀ - · simp [classifyCfg, embedSecond, compositionSecondWorkActions, - hstate, hmiddle] - · let j : Fin k₁ := ⟨i.val - (k₀ + 1), by - have hi := i.isLt - simp only [compositionTapeCount] at hi - omega⟩ - cases hwrite : (workActions j).1 <;> - simp [classifyCfg, embedSecond, compositionSecondWorkActions, - hstate, hfirst, hmiddle, j, hwrite] - · funext i - by_cases hfirst : i.val < k₀ - · simp [classifyCfg, embedSecond, compositionSecondWorkActions, - hstate, hfirst, idleWorkAction] - · by_cases hmiddle : i.val = k₀ - · simp only [tapes, embedSecond, hstate, hmiddle, lt_self_iff_false, ↓reduceDIte, - compositionSecondWorkActions, classifyCfg] - exact (virtualInputPos_move secondCfg.inputPos inputMove).symm - · simp [classifyCfg, embedSecond, compositionSecondWorkActions, - hstate, hfirst, hmiddle] - · rfl - -/-- One native second-machine step is exactly two steps of the composite machine. -/ -private lemma runFrom_two_embedSecond - {firstInput : List Symbol} - (firstCfg : Cfg k₀ Symbol State₀ firstInput) - {secondInput : List Symbol} - (secondCfg : Cfg k₁ Symbol State₁ secondInput) : - (comp tm₀ tm₁).runFrom - (embedSecond tm₀ tm₁ firstCfg secondCfg) 2 = - embedSecond tm₀ tm₁ firstCfg (tm₁.step secondCfg) := by - cases hstate : secondCfg.state with - | none => simp [runFrom, embedSecond, step, hstate] - | some q => - change (comp tm₀ tm₁).step - ((comp tm₀ tm₁).step (embedSecond tm₀ tm₁ firstCfg secondCfg)) = _ - rw [step_embedSecond tm₀ tm₁ firstCfg secondCfg q hstate] - apply step_classifyCfg - simpa only [step, hstate, virtualInputPos_move] using - compositionClassifyMode_move secondCfg.inputPos - (tm₁.tr q secondCfg.inputSymbol secondCfg.workTapeSymbols).inputMove - -/-- Simulation of the second machine, at a cost of two composite steps per native step. -/ -lemma runFrom_secondPhase - {firstInput : List Symbol} - (firstCfg : Cfg k₀ Symbol State₀ firstInput) - {secondInput : List Symbol} - (secondCfg : Cfg k₁ Symbol State₁ secondInput) - (n : ℕ) : - (comp tm₀ tm₁).runFrom - (embedSecond tm₀ tm₁ firstCfg secondCfg) (2 * n) = - embedSecond tm₀ tm₁ firstCfg - (tm₁.runFrom secondCfg n) := by - induction n with - | zero => simp [runFrom] - | succ n ih => - rw [show 2 * (n + 1) = 2 * n + 2 by omega, runFrom_add, ih, - runFrom_two_embedSecond, runFrom_succ_eq_step'] - -/-- The odd-numbered composite steps of the second phase are precisely the intermediate -classifier configurations. -/ -lemma runFrom_secondPhase_odd - {firstInput : List Symbol} - (firstCfg : Cfg k₀ Symbol State₀ firstInput) - {secondInput : List Symbol} - (secondCfg : Cfg k₁ Symbol State₁ secondInput) - (n : ℕ) : - ∃ boundary, - (comp tm₀ tm₁).runFrom - (embedSecond tm₀ tm₁ firstCfg secondCfg) (2 * n + 1) = - classifyCfg tm₀ tm₁ firstCfg - (tm₁.runFrom secondCfg (n + 1)) boundary := by - rw [runFrom_add, runFrom_secondPhase] - cases hstate : (tm₁.runFrom secondCfg n).state with - | none => - refine ⟨.right, ?_⟩ - change (comp tm₀ tm₁).step - (embedSecond tm₀ tm₁ firstCfg (tm₁.runFrom secondCfg n)) = _ - rw [runFrom_succ_eq_step', step_of_halt hstate] - simp [step, embedSecond, classifyCfg, hstate] - | some q => - refine ⟨(inputMode (tm₁.runFrom secondCfg n).inputPos).nextBoundary - (tm₁.tr q (tm₁.runFrom secondCfg n).inputSymbol - (tm₁.runFrom secondCfg n).workTapeSymbols).inputMove, ?_⟩ - change (comp tm₀ tm₁).step - (embedSecond tm₀ tm₁ firstCfg (tm₁.runFrom secondCfg n)) = _ - rw [step_embedSecond tm₀ tm₁ firstCfg _ q hstate, runFrom_succ_eq_step'] - -end Turing.MultiTapeTM.Composition diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index 426a1567d..a83a9b879 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean @@ -1,7 +1,7 @@ /- 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 @@ -9,7 +9,6 @@ module 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 @@ -72,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. @@ -424,43 +425,58 @@ lemma output_length_le_time rw [← hout] simpa using tm.runFrom_output_length_le (tm.initCfg input) t -/-- 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 +/-- 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. -/ 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/Composition.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Composition.lean similarity index 81% rename from Cslib/Computability/Machines/Turing/MultiTape/Composition.lean rename to Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Composition.lean index dcaf584aa..0562c2f63 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Composition.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Composition.lean @@ -6,7 +6,7 @@ Authors: Samuel Schlesinger module -public import Cslib.Computability.Machines.Turing.MultiTape.Composition.Rewind +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Composition.Rewind import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas import Mathlib.Algebra.BigOperators.Fin @@ -16,8 +16,7 @@ import Mathlib.Algebra.BigOperators.Fin `comp_haltsWithOutput` gives operational correctness. `comp_computesInTimeAndSpace` composes individual computations, charging the rewind and extra tape to the actual intermediate output -length. `comp_computesFunInTimeAndSpace_of_length_le` lifts this result to functions with a -separate output-length bound; `comp_computesFunInTimeAndSpace` uses the first time bound instead. +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. @@ -113,17 +112,17 @@ private inductive CompositionCfgPhase (hs : s ≤ (firstFinalCfg tm₀ input u).output.length) (hcfg : cfg = intermediateCfg tm₀ tm₁ (firstFinalCfg tm₀ input u) - .rewind + (.inr (.inl .scan)) (((firstFinalCfg tm₀ input u).output.length : ℤ) - 1 - s)) | initialClassify (hcfg : cfg = intermediateCfg tm₀ tm₁ (firstFinalCfg tm₀ input u) - (.classify tm₁.q₀ .right) 0) + (.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 : CompositionBoundary) + | secondClassify (m : ℕ) (hm : m < v) (boundary : InputBoundary) (hcfg : cfg = classifyCfg tm₀ tm₁ (firstFinalCfg tm₀ input u) (secondCfgAt tm₀ tm₁ input u (m + 1)) @@ -179,28 +178,6 @@ private lemma runFrom_composition_cases ## Resource bounds and function-level correctness -/ -namespace Composition - -/-- Time bound produced by sequentially composing computations with bounds `T₀` and `T₁`. -/ -def timeBound (T₀ T₁ : ℕ → ℕ) (n : ℕ) : ℕ := - 2 * T₀ n + 3 + 2 * T₁ (T₀ n) - -/-- Space bound produced by sequential composition, including its intermediate work tape. -/ -def spaceBound (T₀ S₀ S₁ : ℕ → ℕ) (n : ℕ) : ℕ := - S₀ n + (T₀ n + 2) + S₁ (T₀ n) - -/-- Sequential composition preserves monotonicity of time bounds. -/ -lemma timeBound_mono {T₀ T₁ : ℕ → ℕ} (hT₀ : Monotone T₀) (hT₁ : Monotone T₁) : - Monotone (timeBound T₀ T₁) := by - exact ((hT₀.const_mul' 2).add monotone_const).add ((hT₁.comp hT₀).const_mul' 2) - -/-- Sequential composition preserves monotonicity of space bounds. -/ -lemma spaceBound_mono {T₀ S₀ S₁ : ℕ → ℕ} - (hT₀ : Monotone T₀) (hS₀ : Monotone S₀) (hS₁ : Monotone S₁) : - Monotone (spaceBound T₀ S₀ S₁) := by - exact (hS₀.add (hT₀.add monotone_const)).add (hS₁.comp hT₀) - -end Composition /-- Decompose composite space usage into the first, intermediate, and second tape blocks. -/ private lemma compositionSpaceUsed_eq @@ -314,7 +291,7 @@ private lemma compositionIntermediateTapePos_mem_Icc rw [hcfg] simp only [tapes, firstFinalCfg, embedSecond, compositionIntermediateTapeIdx_val, lt_self_iff_false, ↓reduceDIte, Finset.mem_Icc] - unfold virtualInputPos + unfold InputFromWorkTape.virtualInputPos constructor <;> omega | secondClassify m _ _ hcfg => have hp := (secondCfgAt tm₀ tm₁ input u (m + 1)).inputPos.isLt @@ -323,7 +300,7 @@ private lemma compositionIntermediateTapePos_mem_Icc simp only [tapes, firstFinalCfg, classifyCfg, embedSecond, compositionIntermediateTapeIdx_val, lt_self_iff_false, ↓reduceDIte, Finset.mem_Icc] - unfold virtualInputPos + unfold InputFromWorkTape.virtualInputPos constructor <;> omega /-- The intermediate tape visits at most `output.length + 2` cells in a complete run. -/ @@ -390,44 +367,4 @@ theorem comp_computesInTimeAndSpace have hcomp := comp_haltsWithOutput tm₀ tm₁ hhaltu hactiveu houtu h₁.1 h₁.2.1 exact ⟨hcomp.1, hcomp.2, rfl⟩ -/-- Function composition with a separate bound on intermediate output length. -This avoids charging a long first computation's running time as intermediate space. -/ -theorem comp_computesFunInTimeAndSpace_of_length_le - {IOSymbol : Type*} {f g : List IOSymbol → List IOSymbol} - (embedding : IOSymbol ↪ Symbol) {T₀ S₀ T₁ S₁ L : ℕ → ℕ} - (h₀ : ComputesFunInTimeAndSpace tm₀ f embedding T₀ S₀) - (h₁ : ComputesFunInTimeAndSpace tm₁ g embedding T₁ S₁) - (hL : ∀ input, (f input).length ≤ L input.length) - (hT₁ : Monotone T₁) (hS₁ : Monotone S₁) : - ComputesFunInTimeAndSpace (comp tm₀ tm₁) (g ∘ f) embedding - (fun n => T₀ n + (L n + 3) + 2 * T₁ (L n)) - (fun n => S₀ n + (L n + 2) + S₁ (L n)) := by - intro input - obtain ⟨t₀, ht₀, s₀, hs₀, hc₀⟩ := h₀ input - obtain ⟨t₁, ht₁, s₁, hs₁, hc₁⟩ := h₁ (f input) - obtain ⟨t, ht, s, hs, hc⟩ := comp_computesInTimeAndSpace tm₀ tm₁ hc₀ hc₁ - simp only [List.length_map] at ht hs - have hlength := hL input - have htime := hT₁ hlength - have hspace := hS₁ hlength - exact ⟨t, by dsimp only; omega, s, by dsimp only; omega, hc⟩ - -/-- Function composition with bounds expressed only in terms of component time and space. -The first time bound also bounds intermediate output length. -/ -theorem comp_computesFunInTimeAndSpace - {IOSymbol : Type*} {f g : List IOSymbol → List IOSymbol} - (embedding : IOSymbol ↪ Symbol) {T₀ S₀ T₁ S₁ : ℕ → ℕ} - (h₀ : ComputesFunInTimeAndSpace tm₀ f embedding T₀ S₀) - (h₁ : ComputesFunInTimeAndSpace tm₁ g embedding T₁ S₁) - (hT₁ : Monotone T₁) (hS₁ : Monotone S₁) : - ComputesFunInTimeAndSpace (comp tm₀ tm₁) (g ∘ f) embedding - (Composition.timeBound T₀ T₁) (Composition.spaceBound T₀ S₀ S₁) := by - have hlength (input) : (f input).length ≤ T₀ input.length := by - obtain ⟨t, ht, s, _, hc⟩ := h₀ input - simpa only [List.length_map] using (output_length_le_time hc).trans ht - change ComputesFunInTimeAndSpace _ _ _ - (fun n => 2 * T₀ n + 3 + 2 * T₁ (T₀ n)) (fun n => S₀ n + (T₀ n + 2) + S₁ (T₀ n)) - simpa only [two_mul, Nat.add_assoc] - using comp_computesFunInTimeAndSpace_of_length_le tm₀ tm₁ embedding h₀ h₁ hlength hT₁ hS₁ - 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/CslibTests.lean b/CslibTests.lean index 726844cab..fb33f54ea 100644 --- a/CslibTests.lean +++ b/CslibTests.lean @@ -19,5 +19,6 @@ 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 index cbcf41d57..5ac143443 100644 --- a/CslibTests/MultiTapeComposition.lean +++ b/CslibTests/MultiTapeComposition.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Samuel Schlesinger -/ -import Cslib.Computability.Machines.Turing.MultiTape.Composition +import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Composition import Mathlib.Tactic.FinCases /-! Regression tests for composition: empty output, boundary clamping, final-step output, 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