From b787ff34dfb33ce86461b5e12723343d6cebc67f Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 5 Sep 2026 17:29:56 -0400 Subject: [PATCH] feat(MultiTapeTM): prove resource bounds for function composition --- Cslib.lean | 1 + .../Turing/MultiTape/Combinators/Comp.lean | 82 +++++ .../Turing/MultiTape/Combinators/README.md | 14 + .../MultiTape/Plumbing/Composition.lean | 318 +++++++++++++++++- .../Turing/MultiTape/Plumbing/README.md | 5 +- .../Machines/Turing/MultiTape/TapeLemmas.lean | 23 ++ CslibTests/MultiTapeComplexity.lean | 11 +- CslibTests/MultiTapeComposition.lean | 10 +- 8 files changed, 456 insertions(+), 8 deletions(-) create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Combinators/Comp.lean create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Combinators/README.md diff --git a/Cslib.lean b/Cslib.lean index a5c23e7fb..e75bf0e4d 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -46,6 +46,7 @@ public import Cslib.Computability.Languages.OmegaLanguage public import Cslib.Computability.Languages.OmegaRegularLanguage public import Cslib.Computability.Languages.RegularLanguage public import Cslib.Computability.Languages.SafetyLiveness +public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Comp public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic public import Cslib.Computability.Machines.Turing.MultiTape.NormalForms.RewindInput public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Basic 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..4eaa2a071 --- /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 two machines that compute encoded functions. -/ +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/Plumbing/Composition.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Composition.lean index 5bdbeda5f..ee6759071 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Composition.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Composition.lean @@ -8,12 +8,19 @@ module public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Composition.Rewind +import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas +import Mathlib.Algebra.BigOperators.Fin + /-! -# Correctness of multi-tape composition +# Correctness and resource bounds for multi-tape composition + +`comp_haltsWithOutput` gives operational correctness. `comp_computesInTimeAndSpace` composes +individual computations, charging the rewind and extra tape to the actual intermediate output +length. The function-level interface is in `MultiTape.Combinators.Comp`. -`comp_haltsWithOutput` proves that the composite machine returns the second machine's output -on the first machine's result. The first phase takes one step per native step; the second takes -two, following a rewind of the intermediate output and one initial classification step. +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 @@ -49,4 +56,307 @@ theorem comp_haltsWithOutput rw [hfinal] simp only [embedSecond, hhalt₁, and_self] +/-- Final first-component configuration used throughout the resource analysis. -/ +@[simp] private abbrev firstFinalCfg + (tm₀ : MultiTapeTM k₀ Symbol State₀) (input : List Symbol) (u : ℕ) : + Cfg k₀ Symbol State₀ input := + tm₀.runFrom (tm₀.initCfg input) u + +/-- Initial second-component configuration for the output of the first component. -/ +private abbrev secondInitCfg + (tm₀ : MultiTapeTM k₀ Symbol State₀) + (tm₁ : MultiTapeTM k₁ Symbol State₁) + (input : List Symbol) (u : ℕ) : + Cfg k₁ Symbol State₁ (firstFinalCfg tm₀ input u).output := + tm₁.initCfg (firstFinalCfg tm₀ input u).output + +/-- Second-component configuration after `m` simulated steps. -/ +private abbrev secondCfgAt + (tm₀ : MultiTapeTM k₀ Symbol State₀) + (tm₁ : MultiTapeTM k₁ Symbol State₁) + (input : List Symbol) (u m : ℕ) : + Cfg k₁ Symbol State₁ (firstFinalCfg tm₀ input u).output := + tm₁.runFrom (secondInitCfg tm₀ tm₁ input u) m + +/-- Duration used to simulate component runs of lengths `u` and `v`. -/ +private abbrev compositionTotalTime + (tm₀ : MultiTapeTM k₀ Symbol State₀) (input : List Symbol) (u v : ℕ) : ℕ := + u + ((firstFinalCfg tm₀ input u).output.length + 3) + 2 * v + +/-- The first component must switch phases at its earliest halting time. -/ +private structure CompositionRunSpec + (tm₀ : MultiTapeTM k₀ Symbol State₀) + (input : List Symbol) (u : ℕ) : Prop where + firstHalted : (firstFinalCfg tm₀ input u).state = none + firstActive : ∀ m < u, (tm₀.runFrom (tm₀.initCfg input) m).state ≠ none + +/-- A named phase witness for a configuration occurring in a complete composite run. -/ +private inductive CompositionCfgPhase + (tm₀ : MultiTapeTM k₀ Symbol State₀) + (tm₁ : MultiTapeTM k₁ Symbol State₁) + (input : List Symbol) (u v : ℕ) + (cfg : Cfg (compositionTapeCount k₀ k₁) Symbol + (CompositionState State₀ State₁) input) : Prop + | first (m : ℕ) (hm : m ≤ u) + (hcfg : cfg = embedFirst tm₀ tm₁ + (tm₀.runFrom (tm₀.initCfg input) m)) + | rewind (s : ℕ) + (hs : s ≤ (firstFinalCfg tm₀ input u).output.length) + (hcfg : cfg = intermediateCfg tm₀ tm₁ + (firstFinalCfg tm₀ input u) + (.inr (.inl .scan)) + (((firstFinalCfg tm₀ input u).output.length : ℤ) - 1 - s)) + | initialClassify + (hcfg : cfg = intermediateCfg tm₀ tm₁ + (firstFinalCfg tm₀ input u) + (.inr (.inr (.classify tm₁.q₀ .right))) 0) + | second (m : ℕ) (hm : m ≤ v) + (hcfg : cfg = embedSecond tm₀ tm₁ + (firstFinalCfg tm₀ input u) + (secondCfgAt tm₀ tm₁ input u m)) + | secondClassify (m : ℕ) (hm : m < v) (boundary : InputBoundary) + (hcfg : cfg = classifyCfg tm₀ tm₁ + (firstFinalCfg tm₀ input u) + (secondCfgAt tm₀ tm₁ input u (m + 1)) + boundary) + +/-- +Every prefix of a complete composite run is in one of the configurations described by +the first simulation, the rewind, the initial classifier, or an even or odd second-phase step. +-/ +private lemma runFrom_composition_cases + (input : List Symbol) (u v r : ℕ) + (hrun : CompositionRunSpec tm₀ input u) + (hr : r ≤ compositionTotalTime tm₀ input u v) : + CompositionCfgPhase tm₀ tm₁ input u v + ((comp tm₀ tm₁).runFrom ((comp tm₀ tm₁).initCfg input) r) := by + by_cases hfirst : r ≤ u + · exact .first r hfirst (runFrom_firstPhase tm₀ tm₁ input r + (fun m hm => hrun.firstActive m (lt_of_lt_of_le hm hfirst))) + obtain ⟨offset, rfl⟩ := Nat.exists_eq_add_of_le (by omega : u ≤ r) + have hprefix := runFrom_firstPhase tm₀ tm₁ input u hrun.firstActive + by_cases hrewind : offset ≤ (firstFinalCfg tm₀ input u).output.length + 1 + · refine .rewind (offset - 1) (by omega) ?_ + rw [runFrom_add, hprefix] + convert runFrom_firstHalt_rewind tm₀ tm₁ + (firstFinalCfg tm₀ input u) hrun.firstHalted (offset - 1) (by omega) using 1 + congr 1 + omega + by_cases hclassify : offset = (firstFinalCfg tm₀ input u).output.length + 2 + · refine .initialClassify ?_ + rw [runFrom_add, hprefix, hclassify] + exact runFrom_firstHalt_classify tm₀ tm₁ _ hrun.firstHalted + obtain ⟨secondSteps, hoffset⟩ := Nat.exists_eq_add_of_le + (by omega : (firstFinalCfg tm₀ input u).output.length + 3 ≤ offset) + have hsecondSteps : secondSteps ≤ 2 * v := by + dsimp only [compositionTotalTime] at hr + omega + have hsecond : + (comp tm₀ tm₁).runFrom ((comp tm₀ tm₁).initCfg input) (u + offset) = + (comp tm₀ tm₁).runFrom + (embedSecond tm₀ tm₁ (firstFinalCfg tm₀ input u) + (secondInitCfg tm₀ tm₁ input u)) secondSteps := by + rw [hoffset, ← Nat.add_assoc, runFrom_add, + runFrom_to_secondInit tm₀ tm₁ input u hrun.firstHalted hrun.firstActive] + rcases Nat.even_or_odd' secondSteps with ⟨m, heven | hodd⟩ + · refine .second m (by omega) ?_ + rw [hsecond, heven] + exact runFrom_secondPhase tm₀ tm₁ _ _ m + · obtain ⟨boundary, hboundary⟩ := runFrom_secondPhase_odd tm₀ tm₁ + (firstFinalCfg tm₀ input u) (secondInitCfg tm₀ tm₁ input u) m + exact .secondClassify m (by omega) boundary (by rw [hsecond, hodd, hboundary]) + +/-! +## Resource bounds and function-level correctness +-/ + + +/-- Decompose composite space usage into the first, intermediate, and second tape blocks. -/ +private lemma compositionSpaceUsed_eq + {input : List Symbol} + (cfg : Cfg (compositionTapeCount k₀ k₁) Symbol + (CompositionState State₀ State₁) input) + (t : ℕ) : + (comp tm₀ tm₁).spaceUsed cfg t = + (∑ i : Fin k₀, (comp tm₀ tm₁).spaceUsedByTape cfg t + (compositionFirstTapeIdx k₁ i)) + + (comp tm₀ tm₁).spaceUsedByTape cfg t + (compositionIntermediateTapeIdx k₀ k₁) + + ∑ i : Fin k₁, (comp tm₀ tm₁).spaceUsedByTape cfg t + (compositionSecondTapeIdx k₀ k₁ i) := by + unfold spaceUsed + rw [Fin.sum_univ_add, Fin.sum_univ_castSucc] + congr 1 + +/-- Every first-component tape position in a complete composite run occurs in the first run. -/ +private lemma exists_firstComponent_tapePos_eq + (input : List Symbol) (u v r : ℕ) + (hrun : CompositionRunSpec tm₀ input u) + (hr : r ≤ compositionTotalTime tm₀ input u v) + (i : Fin k₀) : + ∃ m ≤ u, + ((comp tm₀ tm₁).runFrom + ((comp tm₀ tm₁).initCfg input) r).workTapePos + (compositionFirstTapeIdx k₁ i) = + (tm₀.runFrom (tm₀.initCfg input) m).workTapePos i := by + have hphase := runFrom_composition_cases tm₀ tm₁ input u v r hrun hr + have hidx_ne : i.val ≠ k₀ := by omega + cases hphase with + | first m hm hcfg => + refine ⟨m, hm, ?_⟩ + rw [hcfg] + simp [embedFirst, compositionFirstTapeIdx] + | rewind _ _ hcfg | initialClassify hcfg => + refine ⟨u, le_rfl, ?_⟩ + rw [hcfg] + simp [intermediateCfg, embedFirst, compositionFirstTapeIdx, hidx_ne] + | second _ _ hcfg | secondClassify _ _ _ hcfg => + refine ⟨u, le_rfl, ?_⟩ + rw [hcfg] + simp [classifyCfg, embedSecond, compositionFirstTapeIdx] + +/-- Every second-component tape position in a complete composite run occurs in the second run. -/ +private lemma exists_secondComponent_tapePos_eq + (input : List Symbol) (u v r : ℕ) + (hrun : CompositionRunSpec tm₀ input u) + (hr : r ≤ compositionTotalTime tm₀ input u v) + (i : Fin k₁) : + ∃ m ≤ v, + ((comp tm₀ tm₁).runFrom + ((comp tm₀ tm₁).initCfg input) r).workTapePos + (compositionSecondTapeIdx k₀ k₁ i) = + (secondCfgAt tm₀ tm₁ input u m).workTapePos i := by + have hphase := runFrom_composition_cases tm₀ tm₁ input u v r hrun hr + have hidx_not_lt : ¬ k₀ + 1 + i.val < k₀ := by omega + have hidx_ne : k₀ + 1 + i.val ≠ k₀ := by omega + cases hphase with + | first _ _ hcfg => + refine ⟨0, Nat.zero_le _, ?_⟩ + rw [hcfg] + simp [embedFirst, compositionSecondTapeIdx, secondCfgAt, secondInitCfg, runFrom, + hidx_not_lt, hidx_ne] + | rewind _ _ hcfg | initialClassify hcfg => + refine ⟨0, Nat.zero_le _, ?_⟩ + rw [hcfg] + simp [intermediateCfg, embedFirst, compositionSecondTapeIdx, + secondCfgAt, secondInitCfg, runFrom, hidx_not_lt, hidx_ne] + | second m hm hcfg => + refine ⟨m, hm, ?_⟩ + rw [hcfg] + simp [embedSecond, compositionSecondTapeIdx, hidx_not_lt, hidx_ne] + | secondClassify m hm _ hcfg => + refine ⟨m + 1, by omega, ?_⟩ + rw [hcfg] + simp [classifyCfg, embedSecond, compositionSecondTapeIdx, + hidx_not_lt, hidx_ne] + +/-- Throughout a complete composite run, the intermediate head stays between the two blank cells +immediately outside the first component's output. -/ +private lemma compositionIntermediateTapePos_mem_Icc + (input : List Symbol) (u v r : ℕ) + (hrun : CompositionRunSpec tm₀ input u) + (hr : r ≤ compositionTotalTime tm₀ input u v) : + ((comp tm₀ tm₁).runFrom + ((comp tm₀ tm₁).initCfg input) r).workTapePos + (compositionIntermediateTapeIdx k₀ k₁) ∈ + Finset.Icc (-1) ((firstFinalCfg tm₀ input u).output.length : ℤ) := by + have hphase := runFrom_composition_cases tm₀ tm₁ input u v r hrun hr + cases hphase with + | first m hm hcfg => + have hmoutput := tm₀.runFrom_output_length_mono (tm₀.initCfg input) hm + dsimp only at hmoutput + rw [hcfg] + simp only [tapes, firstFinalCfg, embedFirst, compositionIntermediateTapeIdx_val, + lt_self_iff_false, ↓reduceDIte, Finset.mem_Icc] + constructor <;> omega + | rewind s hs hcfg => + rw [hcfg] + simp only [firstFinalCfg, intermediateCfg, compositionIntermediateTapeIdx_val, + ↓reduceIte, Finset.mem_Icc] at hs ⊢ + constructor <;> omega + | initialClassify hcfg => + rw [hcfg] + simp [intermediateCfg] + | second m _ hcfg => + have hp := (secondCfgAt tm₀ tm₁ input u m).inputPos.isLt + simp only [secondCfgAt, secondInitCfg, firstFinalCfg] at hp + rw [hcfg] + simp only [tapes, firstFinalCfg, embedSecond, compositionIntermediateTapeIdx_val, + lt_self_iff_false, ↓reduceDIte, Finset.mem_Icc] + unfold InputFromWorkTape.virtualInputPos + constructor <;> omega + | secondClassify m _ _ hcfg => + have hp := (secondCfgAt tm₀ tm₁ input u (m + 1)).inputPos.isLt + simp only [secondCfgAt, secondInitCfg, firstFinalCfg] at hp + rw [hcfg] + simp only [tapes, firstFinalCfg, classifyCfg, embedSecond, + compositionIntermediateTapeIdx_val, lt_self_iff_false, ↓reduceDIte, + Finset.mem_Icc] + unfold InputFromWorkTape.virtualInputPos + constructor <;> omega + +/-- The intermediate tape visits at most `output.length + 2` cells in a complete run. -/ +private lemma compositionIntermediateSpace_le + (input : List Symbol) (u v : ℕ) + (hrun : CompositionRunSpec tm₀ input u) : + (comp tm₀ tm₁).spaceUsedByTape + ((comp tm₀ tm₁).initCfg input) + (compositionTotalTime tm₀ input u v) + (compositionIntermediateTapeIdx k₀ k₁) ≤ + (firstFinalCfg tm₀ input u).output.length + 2 := by + calc + _ ≤ (Finset.Icc (-1) ((firstFinalCfg tm₀ input u).output.length : ℤ)).card := by + apply Finset.card_le_card + intro p hp + obtain ⟨r, hr, rfl⟩ := (comp tm₀ tm₁).mem_visitedByTapeHead.mp hp + exact compositionIntermediateTapePos_mem_Icc tm₀ tm₁ input u v r hrun (by omega) + _ = _ := by rw [Int.card_Icc]; omega + +/-- Component tape blocks retain their native space bounds; only the intermediate tape is new. -/ +private lemma CompositionRunSpec.spaceUsed_le + {input : List Symbol} {u v : ℕ} (hrun : CompositionRunSpec tm₀ input u) : + (comp tm₀ tm₁).spaceUsed ((comp tm₀ tm₁).initCfg input) + (compositionTotalTime tm₀ input u v) ≤ + tm₀.spaceUsed (tm₀.initCfg input) u + + ((firstFinalCfg tm₀ input u).output.length + 2) + + tm₁.spaceUsed (secondInitCfg tm₀ tm₁ input u) v := by + rw [compositionSpaceUsed_eq] + apply Nat.add_le_add + · apply Nat.add_le_add + · apply Finset.sum_le_sum + intro i _ + exact spaceUsedByTape_le_of_positions _ _ _ _ _ _ _ _ + (fun r hr => exists_firstComponent_tapePos_eq tm₀ tm₁ input u v r hrun hr i) + · exact compositionIntermediateSpace_le tm₀ tm₁ input u v hrun + · apply Finset.sum_le_sum + intro i _ + exact spaceUsedByTape_le_of_positions _ _ _ _ _ _ _ _ + (fun r hr => exists_secondComponent_tapePos_eq tm₀ tm₁ input u v r hrun hr i) + +/-- Compose two bounded computations, charging the intermediate tape and rewind to the actual +intermediate output length. Component halting times may be padded. -/ +theorem comp_computesInTimeAndSpace + {input middle output : List Symbol} {t₀ s₀ t₁ s₁ : ℕ} + (h₀ : ComputesInTimeAndSpace tm₀ input middle t₀ s₀) + (h₁ : ComputesInTimeAndSpace tm₁ middle output t₁ s₁) : + ∃ t ≤ t₀ + (middle.length + 3) + 2 * t₁, + ∃ s ≤ s₀ + (middle.length + 2) + s₁, + ComputesInTimeAndSpace (comp tm₀ tm₁) input output t s := by + obtain ⟨u, hu, hhaltu, hactiveu⟩ := + exists_minimal_halting_time tm₀ (tm₀.initCfg input) t₀ h₀.1 + have houtu : (firstFinalCfg tm₀ input u).output = middle := + (tm₀.runFrom_output_eq_of_halt _ hu hhaltu).symm.trans h₀.2.1 + have hrun : CompositionRunSpec tm₀ input u := ⟨hhaltu, hactiveu⟩ + have hspace := hrun.spaceUsed_le tm₀ tm₁ (v := t₁) + have hspace₀ := tm₀.spaceUsed_mono (tm₀.initCfg input) hu + dsimp only [compositionTotalTime, secondInitCfg] at hspace + rw [houtu, h₁.2.2] at hspace + dsimp only at hspace₀ + rw [h₀.2.2] at hspace₀ + refine ⟨u + (middle.length + 3) + 2 * t₁, by omega, + (comp tm₀ tm₁).spaceUsed ((comp tm₀ tm₁).initCfg input) + (u + (middle.length + 3) + 2 * t₁), by omega, ?_⟩ + have hcomp := comp_haltsWithOutput tm₀ tm₁ hhaltu hactiveu houtu h₁.1 h₁.2.1 + exact ⟨hcomp.1, hcomp.2, rfl⟩ + end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/README.md b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/README.md index 65091fdda..62419e859 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/README.md +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/README.md @@ -12,4 +12,7 @@ These modules describe executable machines and their effects on configurations a - `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 correctness. + and tape injections, then proves operational and resource bounds. + +These machines preserve the alphabet. Function complexity results belong in +[Combinators](../Combinators); halting normal forms belong in [NormalForms](../NormalForms). diff --git a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean index 1b10ff9e6..49e7f21ec 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean @@ -133,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/MultiTapeComplexity.lean b/CslibTests/MultiTapeComplexity.lean index c396bee0f..2f3c9cf55 100644 --- a/CslibTests/MultiTapeComplexity.lean +++ b/CslibTests/MultiTapeComplexity.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.Deterministic +import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Comp namespace CslibTests.MultiTapeComplexity @@ -16,7 +16,8 @@ private def finish (move : SignType) (symbol : Bool) : Turing.MultiTapeTM 0 Bool 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. +-- 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 @@ -24,4 +25,10 @@ private lemma constant_computable : · 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.MultiTapeComplexity diff --git a/CslibTests/MultiTapeComposition.lean b/CslibTests/MultiTapeComposition.lean index 54c781271..63df7e3ff 100644 --- a/CslibTests/MultiTapeComposition.lean +++ b/CslibTests/MultiTapeComposition.lean @@ -9,7 +9,7 @@ import Mathlib.Data.Fin.VecNotation import Mathlib.Tactic.FinCases /-! Regression tests for composition: empty output, boundary clamping, final-step output, -and disjoint work tapes. -/ +disjoint work tapes, and padded component runs. -/ namespace CslibTests.MultiTapeComposition @@ -58,4 +58,12 @@ example : ((comp (writeEmit true) (writeEmit false)).runFrom 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