From d19c32f2c25b970ea4d4bb8a108d8378b987165f Mon Sep 17 00:00:00 2001 From: crei Date: Sat, 1 Aug 2026 10:20:26 +0200 Subject: [PATCH 1/2] Prove time upper-bounds for space-bounded classes. Proves bounds on the number of configurations reachable in bounded space and proves complexity-class inclusions from that: DSPACE(s) \subseteq DTIME(n * 2^(O(s)) --- Cslib.lean | 4 + .../Machines/Turing/MultiTape/Classes.lean | 113 ++++++ .../Turing/MultiTape/ConfigBound.lean | 343 ++++++++++++++++++ .../Turing/MultiTape/Deterministic.lean | 133 ++++++- .../Turing/MultiTape/SpaceInTime.lean | 213 +++++++++++ .../Machines/Turing/MultiTape/TapeLemmas.lean | 144 ++++++++ 6 files changed, 932 insertions(+), 18 deletions(-) create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Classes.lean create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/SpaceInTime.lean create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean diff --git a/Cslib.lean b/Cslib.lean index d67431976..3b6f86625 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -40,7 +40,11 @@ public import Cslib.Computability.Languages.MyhillNerode public import Cslib.Computability.Languages.OmegaLanguage public import Cslib.Computability.Languages.OmegaRegularLanguage public import Cslib.Computability.Languages.RegularLanguage +public import Cslib.Computability.Machines.Turing.MultiTape.Classes +public import Cslib.Computability.Machines.Turing.MultiTape.ConfigBound public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic +public import Cslib.Computability.Machines.Turing.MultiTape.SpaceInTime +public import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas public import Cslib.Computability.Machines.Turing.SingleTape.Defs public import Cslib.Computability.Machines.Turing.SingleTape.Deterministic public import Cslib.Computability.Machines.Turing.SingleTape.NonDeterministic diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Classes.lean b/Cslib/Computability/Machines/Turing/MultiTape/Classes.lean new file mode 100644 index 000000000..4a56a44e6 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Classes.lean @@ -0,0 +1,113 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +public import Mathlib.Order.Monotone.Defs + +import Mathlib.Tactic.Ring +public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic + +/-! +# Complexity classes for deterministic multi-tape Turing machines + +This file defines the resource-bounded complexity classes for deterministic multi-tape Turing +machines on top of `DecidableInTimeAndSpace`. + +## Design + +The primitives `DTIME` and `DSPACE` are defined using a single bound function `ℕ → ℕ` but allow +for `O`-fuzzyness. Using this fuzzyness is justified by the space and time compression / speedup +results which are not proven here. Once we have better machinery, we can prove them and potentially +move to exact bounds. + +The classes are always relative to a `Symbol` alphabet. + +## Important Declarations + +* `DTIME` - the class of languages decidable in time `O(t(n))` for some function `t : ℕ → ℕ`. +* `DSPACE` - the class of languages decidable in space `O(s(n))` for some function `s : ℕ → ℕ`. + +Some named complexity classes are defined in the `Classes` namespace: + +* `P`, `E`, `EXP` +* `L`, `PSPACE`, `ESPACE`, `EXPSPACE` +-/ + +@[expose] public section + +open Cslib + +namespace Turing.MultiTapeTM + +variable {Symbol : Type} [Inhabited Symbol] + +/-- Monotonicity of `DecidableInTimeAndSpace` in the time bound. -/ +lemma DecidableInTimeAndSpace.mono_time {L : Language Symbol} {s : ℕ → ℕ} : + Monotone (DecidableInTimeAndSpace L · s) := by + intro t₁ t₂ h hd + obtain ⟨k, sym, state, emb, tm, hcomp⟩ := hd + refine ⟨k, sym, state, emb, tm, fun input => ?_⟩ + obtain ⟨t', ht', s', hs', hcs⟩ := hcomp input + exact ⟨t', ht'.trans (h _), s', hs', hcs⟩ + +/-- Monotonicity of `DecidableInTimeAndSpace` in the space bound. -/ +lemma DecidableInTimeAndSpace.mono_space {L : Language Symbol} {t : ℕ → ℕ} : + Monotone (DecidableInTimeAndSpace L t ·) := by + intro s₁ s₂ h hd + obtain ⟨k, sym, state, emb, tm, hcomp⟩ := hd + refine ⟨k, sym, state, emb, tm, fun input => ?_⟩ + obtain ⟨t', ht', s', hs', hcs⟩ := hcomp input + exact ⟨t', ht', s', hs'.trans (h _), hcs⟩ + +/-- The complexity class of languages decidable in time linear in `t` by a deterministic multi-tape +Turing machine, disregarding the space requirement. -/ +def DTIME (t : ℕ → ℕ) := + {L : Language Symbol | ∃ c₁ c₂ : ℕ, ∃ s, DecidableInTimeAndSpace L (c₁ * t · + c₂) s} + +/-- The complexity class of languages decidable in space linear in `s` by a deterministic multi-tape +Turing machine, for some time bound. -/ +def DSPACE (s : ℕ → ℕ) := + {L : Language Symbol | ∃ c₁ c₂ : ℕ, ∃ t, DecidableInTimeAndSpace L t (c₁ * s · + c₂)} + +/-- `DTIME` is monotone in the time bound. -/ +lemma DTIME_mono {t₁ t₂ : ℕ → ℕ} (h : t₁ ≤ t₂) : + DTIME (Symbol := Symbol) t₁ ⊆ DTIME t₂ := by + rintro L ⟨c₁, c₂, s, hs⟩ + exact ⟨c₁, c₂, s, hs.mono_time fun n => by gcongr; exact h n⟩ + +/-- `DSPACE` is monotone in the space bound. -/ +lemma DSPACE_mono {s₁ s₂ : ℕ → ℕ} (h : ∀ n, s₁ n ≤ s₂ n) : + DSPACE s₁ ⊆ (DSPACE s₂ : Set (Language Symbol)) := by + rintro L ⟨c₁, c₂, t, ht⟩ + exact ⟨c₁, c₂, t, ht.mono_space fun n => by gcongr; exact h n⟩ + +namespace Classes + +/-- Deterministic polynomial time. -/ +def P : Set (Language Symbol) := ⋃ k, DTIME (· ^ k) + +/-- Deterministic exponential time (linear exponent). -/ +def E : Set (Language Symbol) := ⋃ k, DTIME fun n => 2 ^ (k * n) + +/-- Deterministic exponential time (polynomial exponent). -/ +def EXP : Set (Language Symbol) := ⋃ k, DTIME fun n => 2 ^ (n ^ k) + +/-- Deterministic logarithmic space. -/ +def L : Set (Language Symbol) := DSPACE Nat.log2 + +/-- Deterministic polynomial space. -/ +def PSPACE : Set (Language Symbol) := ⋃ k, DSPACE fun n => n ^ k + +/-- Deterministic exponential space. -/ +def ESPACE : Set (Language Symbol) := ⋃ k, DSPACE fun n => 2 ^ (k * n) + +/-- Deterministic exponential space. -/ +def EXPSPACE : Set (Language Symbol) := ⋃ k, DSPACE fun n => 2 ^ (n ^ k) + +end Classes + +end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean b/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean new file mode 100644 index 000000000..fb2244f0f --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean @@ -0,0 +1,343 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +public import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas +public import Mathlib.Data.Fintype.BigOperators +public import Mathlib.Data.Fintype.Pi +public import Mathlib.Data.Fintype.Prod +public import Mathlib.Data.Fintype.Option +public import Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset + +/-! +# A bound on the number of reachable configurations in bounded space + +For a deterministic multi-tape Turing machine that uses at most `s` cells of work-tape space, the +number of distinct configurations it can be in is bounded by an explicit function of `s` (and the +machine's parameters). This is the counting fact underlying, for instance, the collapse of very +small space classes and the inclusion `PSPACE ⊆ EXP`. + +The configuration type `Cfg` is split into the input head position and the *storage* part +(`Storage`), i.e. the state, the work tape contents and head positions. This split can be used +to show the collapse of small space-bounded classes. + + +## Important Definitions + +The key lemmas in this file are: + +* `MultiTapeTM.card_storages_le` bounds the number of *storage configurations* only, disregarding + the input head position. The function used for the bound is `storageBound Symbol State k s`. +* `MultiTapeTM.card_configs_le` additionally tracks the input head position, giving the bound + `(n + 2) * storageBound Symbol State k s` on the number of full configurations of an input of + length `n`. +* `MultiTapeTM.card_configs_le_pow` restates the previous bound as `(n + 2) * a * 2 ^ (c * s)` + for constants `a` and `c` depending only on the machine, so it can be used to time-bound + space-bounded machines. + +## Design + +Starting from the all-blank tapes with +every head at `0` and moving by at most one cell per step, a computation in which tape `i` has +visited at most `sᵢ` cells keeps that tape's head position and every non-blank cell within the +per-tape window `[-sᵢ, sᵢ]`. +Hence a storage configuration is determined by finite data over these +windows, and counting it gives the per-tape product `∏ᵢ (2 sᵢ + 1) · (|Symbol|+1)^(2 sᵢ + 1)`. Since +the tapes share the total space budget (`∑ᵢ sᵢ ≤ s`), this collapses to `storageBound`, whose +alphabet exponent is the *total* space (`2s + k`) rather than `k · s` — matching the textbook +`|State| · |Symbol|^{O(s)} · poly(s)` count. The full-configuration bound needed for time-bounding +space-bounded machines then follows by pairing the storage count with the `(n + 2)` possible +input-head positions. + +We lose a factor of `2 * k` by simplifying the windows to `[-sᵢ, sᵢ]` instead of the actually used +area, but this is absorbed by the `O(s)` exponent in the final bound. The `+2` in `(n + 2)` is +needed because the input head is allowed to move one step off the input in either direction by +the model. +-/ + +@[expose] public section + +open Cslib + +namespace Turing.MultiTapeTM + +variable {k : ℕ} +variable {State Symbol : Type*} +variable {input : List Symbol} +variable {tm : MultiTapeTM k Symbol State} + +/-- The state and work-tape data of a machine, with the cells and head position of tape `i` indexed +by an arbitrary type `ι i`. If you add the input tape position and use `ι i = ℤ`, this is equivalent +to `Cfg` (cf. `Cfg.storage`). +The index set is useful for cardinality arguments if we have a bound on the tape cells that +are actually used. +The input head position is not included because this is useful for arguments below logarithmic +space. -/ +@[ext] +structure Storage (Symbol State : Type*) {k : ℕ} (ι : Fin k → Type*) where + /-- the state of the TM (cf. `Cfg.state`) -/ + state : Option State + /-- the contents of work tape `i` (cf. `Cfg.workTapes`) -/ + workTapes (i : Fin k) : ι i → Option Symbol + /-- the position of the head on work tape `i` (cf. `Cfg.workTapePos`) -/ + workTapePos (i : Fin k) : ι i + +/-- A `Storage` is just a product of its fields; this equivalence is used for counting. -/ +def Storage.equivProd (Symbol State : Type*) (ι : Fin k → Type*) : + Storage Symbol State ι ≃ + Option State × ((i : Fin k) → ι i → Option Symbol) × ((i : Fin k) → ι i) where + toFun x := (x.state, x.workTapes, x.workTapePos) + invFun := fun ⟨state, workTapes, workTapePos⟩ => ⟨state, workTapes, workTapePos⟩ + +instance (Symbol State : Type*) [Fintype Symbol] [Fintype State] + (ι : Fin k → Type*) [∀ i, Fintype (ι i)] [∀ i, DecidableEq (ι i)] : + Fintype (Storage Symbol State ι) := + Fintype.ofEquiv _ (Storage.equivProd Symbol State ι).symm + +/-- A `Storage` over the unrestricted index type `ℤ` for every tape, as extracted from a full +configuration by `Cfg.storage`. -/ +abbrev UnboundedStorage (Symbol State : Type*) (k : ℕ) := + Storage Symbol State (fun _ : Fin k => ℤ) + +/-- This function maps a `Cfg` to `Storage`, using `ℤ` as the index type for the tapes. -/ +def Cfg.storage (c : Cfg k Symbol State input) : UnboundedStorage Symbol State k := + ⟨c.state, c.workTapes, c.workTapePos⟩ + +/-- For a fixed input, a configuration is fully determined by its input-head position together with +its `storage`. Hence counting distinct configurations reduces to counting `(inputPos, storage)` +pairs. -/ +lemma inputPos_storage_injective (input : List Symbol) : + Function.Injective + (fun c : Cfg k Symbol State input => (c.inputPos.val, c.storage)) := by + intro c₁ c₂ h + simp only [Cfg.storage, Prod.mk.injEq, Storage.mk.injEq] at h + obtain ⟨hip, hstate, hwt, hwp⟩ := h + exact Cfg.ext hstate (Fin.ext hip) hwt hwp + + +/-- The window `[-s, s]` of tape positions allotted to a tape that uses `s` cells. -/ +def Storage.window (s : ℕ) : Finset ℤ := Finset.Icc (-(s : ℤ)) s + +@[scoped grind =] +lemma Storage.mem_window {s : ℕ} {z : ℤ} : z ∈ Storage.window s ↔ z.natAbs ≤ s := by + simp only [Storage.window, Finset.mem_Icc] + omega + +@[simp] +lemma Storage.card_window (s : ℕ) : (Storage.window s).card = 2 * s + 1 := by + rw [Storage.window, Int.card_Icc] + omega + +/-- A bounded storage configuration: a `Storage` whose tape `i` is restricted to the finite window +`[-(w i), w i]`. Storage configurations of a computation that visits at most the window of each +tape embed injectively into this finite type (`Storage.toBounded`), so its cardinality bounds the +number of reachable storage configurations. -/ +abbrev BoundedStorage (Symbol State : Type*) {k : ℕ} (w : Fin k → ℕ) := + Storage Symbol State (fun i => Storage.window (w i)) + +/-- A storage fits in the per-tape windows `w`: on each tape `j`, the head position and every +non-blank cell have absolute value `≤ w j`. -/ +structure Storage.FitsIn (x : UnboundedStorage Symbol State k) (w : Fin k → ℕ) : Prop where + /-- the head position on every tape lies within its window -/ + pos_le : ∀ j, (x.workTapePos j).natAbs ≤ w j + /-- every non-blank cell on every tape lies within its window -/ + cell_le : ∀ j z, x.workTapes j z ≠ none → z.natAbs ≤ w j + +/-- Restriction of a storage over `ℤ` to the finite windows `w` (with heads outside their window +clamped to `0`). -/ +def Storage.toBounded (x : UnboundedStorage Symbol State k) (w : Fin k → ℕ) : + BoundedStorage Symbol State w where + state := x.state + workTapes j z := x.workTapes j z.1 + workTapePos j := + if h : x.workTapePos j ∈ Storage.window (w j) then ⟨x.workTapePos j, h⟩ + else ⟨0, Storage.mem_window.mpr (Nat.zero_le _)⟩ + +/-- The restriction is injective on storages that fit in the windows. -/ +lemma Storage.toBounded_injOn (w : Fin k → ℕ) : + Set.InjOn (Storage.toBounded (Symbol := Symbol) (State := State) · w) {x | x.FitsIn w} := by + rintro x ⟨hxp, hxc⟩ y ⟨hyp, hyc⟩ hxy + simp only [Storage.toBounded, Storage.mk.injEq] at hxy + obtain ⟨hstate, htapes, hpos⟩ := hxy + refine Storage.ext hstate (funext₂ fun j z => ?_) (funext fun j => ?_) + · by_cases hz : z ∈ Storage.window (w j) + · exact congrFun (congrFun htapes j) ⟨z, hz⟩ + · grind + · have := congrFun hpos j + grind [Subtype.ext_iff] + +/-- The number of storages over finite position types is the per-tape product of +"cell contents × head position" counts. -/ +lemma card_storage [Fintype Symbol] [Fintype State] + (ι : Fin k → Type*) [∀ i, Fintype (ι i)] [∀ i, DecidableEq (ι i)] : + Fintype.card (Storage Symbol State ι) + = (Fintype.card State + 1) + * ∏ i, Fintype.card (ι i) * (Fintype.card Symbol + 1) ^ Fintype.card (ι i) := by + rw [Fintype.card_congr (Storage.equivProd Symbol State ι)] + simp only [Fintype.card_prod, Fintype.card_option, Fintype.card_pi, Finset.prod_const, + Finset.card_univ, Finset.prod_mul_distrib] + ring + +/-- An upper bound on the number of storage configurations a `k`-tape machine can be in while using +at most `s` cells of total work-tape space, over the given alphabet and state set. The `(2s+1)^k` +factor counts the possible head positions; the dominant factor `(|Symbol|+1)^(2s+k)` uses the +*total* space `s` in the exponent (the `k` tapes share the space budget), matching the textbook +`|State| · |Symbol|^{O(s)} · poly(s)` count. -/ +def storageBound (Symbol State : Type*) [Fintype Symbol] [Fintype State] (k s : ℕ) : ℕ := + (Fintype.card State + 1) * ((2 * s + 1) ^ k * (Fintype.card Symbol + 1) ^ (2 * s + k)) + +/-- `storageBound` grows at most exponentially in the space `s`: there exist constants `a` and `c` +(depending on the machine's alphabet, state set and tape count) with +`storageBound Symbol State k s ≤ a * 2 ^ (c * s)` for all `s`. The multiplicative constant `a` is +needed since `storageBound … 0` is a nonzero constant while `2 ^ 0 = 1`; it is harmless downstream +because the complexity classes absorb constant factors. This is what lets a `storageBound`-based +configuration count be phrased as `2 ^ (O(s))`. -/ +lemma storageBound_le_pow [Fintype Symbol] [Fintype State] (k : ℕ) : + ∃ a c : ℕ, ∀ s, storageBound Symbol State k s ≤ a * 2 ^ (c * s) := by + set syms := Fintype.card Symbol + 1 with hB + set states := Fintype.card State + 1 with hQ + -- The strategy is to bound each factor of `storageBound` by a power of `2`, using `B ≤ 2 ^ B` + -- and `2 * s + 1 ≤ 2 ^ (s + 1)`. Collecting the exponents then yields + -- `(s + 1) * k + B * (2 * s + k)`, which splits into the constant part `B * k + k` + -- (absorbed into `a`) and the part `(2 * B + k) * s` linear in `s` (which is `c * s`). + refine ⟨states * 2 ^ (syms * k + k), 2 * syms + k, fun s => ?_⟩ + have hB2 : syms ≤ 2 ^ syms := Nat.lt_two_pow_self.le + have h2s1 : 2 * s + 1 ≤ 2 ^ (s + 1) := by + have : s < 2 ^ s := Nat.lt_two_pow_self + rw [pow_succ] + omega + calc storageBound Symbol State k s + = states * ((2 * s + 1) ^ k * syms ^ (2 * s + k)) := rfl + -- bound both bases by powers of `2` + _ ≤ states * ((2 ^ (s + 1)) ^ k * (2 ^ syms) ^ (2 * s + k)) := by + gcongr <;> exact Nat.zero_le _ + -- collect everything into a single exponent + _ = states * 2 ^ ((s + 1) * k + syms * (2 * s + k)) := by rw [← pow_mul, ← pow_mul, ← pow_add] + -- split the exponent into its constant part and its part linear in `s` + _ = states * 2 ^ ((syms * k + k) + (2 * syms + k) * s) := by ring_nf + _ = states * 2 ^ (syms * k + k) * 2 ^ ((2 * syms + k) * s) := by rw [pow_add, mul_assoc] + +/-- The per-tape product is bounded by `storageBound`: each tape uses at most the total space `s`, +and the tapes together use at most `s`, which collapses the alphabet exponent to `2s + k`. -/ +lemma card_boundedStorage_le [Fintype Symbol] [Fintype State] + (w : Fin k → ℕ) (s : ℕ) (hsum : ∑ i, w i ≤ s) : + Fintype.card (BoundedStorage Symbol State w) ≤ storageBound Symbol State k s := by + have hle : ∀ i, w i ≤ s := fun i => + (Finset.single_le_sum (fun i _ => Nat.zero_le (w i)) (Finset.mem_univ i)).trans hsum + rw [card_storage, storageBound] + simp only [Fintype.card_coe, Storage.card_window] + rw [Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum] + have hsc : ∑ i : Fin k, (2 * w i + 1) = 2 * (∑ i, w i) + k := by + simp [two_mul, Finset.sum_add_distrib] + gcongr + · simpa using Finset.prod_le_pow_card Finset.univ (fun i => 2 * w i + 1) (2 * s + 1) + fun i _ => by have := hle i; omega + · omega + · omega + +/-- The storage of any configuration reached within `T` steps fits in the windows given by the +per-tape space usage up to step `T`. -/ +lemma storage_fitsIn + (T : ℕ) + {t : ℕ} + (ht : t ≤ T) : + (tm.configs (tm.initCfg input) t).storage.FitsIn + (fun i => tm.spaceUsedByTape (tm.initCfg input) T i) := by + -- The bounds at step `t` extend to the window at step `T ≥ t` by monotonicity of space usage. + refine ⟨fun j => le_trans ?_ (tm.spaceUsedByTape_mono _ j ht), + fun j z hz => le_trans ?_ (tm.spaceUsedByTape_mono _ j ht)⟩ + · -- The head position at step `t` is visited, and the initial head position is `0`, so the + -- displacement bound is a bound on the position itself. + simpa [Cfg.storage] using tm.natAbs_le_spaceUsedByTape_of_mem_visited + (tm.mem_visitedByTapeHead_self (tm.initCfg input) t j) + · exact content_natAbs_le_spaceUsedByTape t z hz + + +open scoped Classical in +/-- For any multi-tape Turing machine that uses at most space `s` up to step `t`, the number +of storage configurations (configurations disregarding the input head positions) up to step `t` +is at most `storageBound Symbol State k s` (independent of `t`). -/ +theorem card_storages_le + [Fintype Symbol] [Fintype State] + (t s : ℕ) + (hs : tm.spaceUsed (tm.initCfg input) t ≤ s) : + ((Finset.range (t + 1)).image + (fun t' => (tm.configs (tm.initCfg input) t').storage)).card + ≤ storageBound Symbol State k s := by + have hsum : ∑ i, tm.spaceUsedByTape (tm.initCfg input) t i ≤ s := hs + calc ((Finset.range (t + 1)).image + (fun t' => (tm.configs (tm.initCfg input) t').storage)).card + ≤ Fintype.card + (BoundedStorage Symbol State (fun i => tm.spaceUsedByTape (tm.initCfg input) t i)) := by + rw [← Finset.card_univ] + refine Finset.card_le_card_of_injOn + (Storage.toBounded · (fun i => tm.spaceUsedByTape (tm.initCfg input) t i)) + (fun x _ => Finset.mem_univ _) ?_ + refine Set.InjOn.mono ?_ + (Storage.toBounded_injOn (fun i => tm.spaceUsedByTape (tm.initCfg input) t i)) + intro x hx + simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, Finset.mem_range] at hx + obtain ⟨t', ht, rfl⟩ := hx + exact storage_fitsIn t (by omega) + _ ≤ storageBound Symbol State k s := + card_boundedStorage_le (fun i => tm.spaceUsedByTape (tm.initCfg input) t i) s hsum + + +open scoped Classical in +/-- The number of distinct configurations a multi-tape Turing machine with space bound `s` +can reach is at most `(n + 2) * storageBound Symbol State k s`, where `n` is the input length. +The `(n + 2)` factor accounts for the input-head position; the `storageBound` factor accounts for +everything else (`storage`). -/ +theorem card_configs_le + [Fintype Symbol] [Fintype State] + (t s : ℕ) + (hs : tm.spaceUsed (tm.initCfg input) t ≤ s) : + ((Finset.range (t + 1)).image (tm.configs (tm.initCfg input))).card + ≤ (input.length + 2) * storageBound Symbol State k s := by + -- Counting configurations reduces to counting `(inputPos, storage)` pairs, since the map to such + -- pairs is injective for a fixed input. + rw [← Finset.card_image_of_injective _ (inputPos_storage_injective input), Finset.image_image] + -- The pair image lies in the product of the input-head range with the storage image, so its + -- cardinality is bounded by `(n + 2)` times the storage count from `card_storages_le`. + calc ((Finset.range (t + 1)).image (fun t' => + ((tm.configs (tm.initCfg input) t').inputPos.val, + (tm.configs (tm.initCfg input) t').storage))).card + ≤ (Finset.range (input.length + 2) ×ˢ (Finset.range (t + 1)).image + (fun t' => (tm.configs (tm.initCfg input) t').storage)).card := by + refine Finset.card_le_card fun x hx => ?_ + simp only [Finset.mem_image, Finset.mem_range] at hx + obtain ⟨t, ht, rfl⟩ := hx + simp only [Finset.mem_product, Finset.mem_range, Finset.mem_image] + exact ⟨(tm.configs (tm.initCfg input) t).inputPos.isLt, t, ht, rfl⟩ + _ = (input.length + 2) * ((Finset.range (t + 1)).image + (fun t => (tm.configs (tm.initCfg input) t).storage)).card := by + rw [Finset.card_product, Finset.card_range] + _ ≤ (input.length + 2) * storageBound Symbol State k s := + Nat.mul_le_mul_left _ (card_storages_le t s hs) + +open scoped Classical in +/-- The number of distinct configurations reachable in space `s` is at most `2 ^ (O(s))`, up to the +`(n + 2)` factor for the input-head position: there are constants `a` and `c` (depending only on +the machine's alphabet, state set and tape count) that bound the configuration count for *every* +input and step count. This is the form used to time-bound space-bounded machines. -/ +theorem card_configs_le_pow + [Finite Symbol] [Finite State] : + ∃ a c : ℕ, ∀ (input : List Symbol) (t s : ℕ), + tm.spaceUsed (tm.initCfg input) t ≤ s → + ((Finset.range (t + 1)).image (tm.configs (tm.initCfg input))).card + ≤ (input.length + 2) * a * 2 ^ (c * s) := by + have : Fintype Symbol := Fintype.ofFinite Symbol + have : Fintype State := Fintype.ofFinite State + obtain ⟨a, c, hpow⟩ := storageBound_le_pow (Symbol := Symbol) (State := State) k + refine ⟨a, c, fun input t s hs => ?_⟩ + calc ((Finset.range (t + 1)).image (tm.configs (tm.initCfg input))).card + ≤ (input.length + 2) * storageBound Symbol State k s := + tm.card_configs_le t s hs + _ ≤ (input.length + 2) * (a * 2 ^ (c * s)) := Nat.mul_le_mul_left _ (hpow s) + _ = (input.length + 2) * a * 2 ^ (c * s) := by ring + +end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index 9e083b3d0..345377caa 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean @@ -255,6 +255,14 @@ def initCfg (input : List Symbol) : Cfg k Symbol State input := If the Turing machine halts, it will stay at the halting configuration. -/ def configs (cfg : Cfg k Symbol State input) (t : ℕ) : Cfg k Symbol State input := tm.step^[t] cfg +lemma configs_succ_eq_step {cfg : Cfg k Symbol State input} {t : ℕ} : + tm.configs cfg (t + 1) = tm.configs (tm.step cfg) t := by + simp [configs, Function.iterate_succ_apply] + +lemma configs_succ_eq_step' {cfg : Cfg k Symbol State input} {t : ℕ} : + tm.configs cfg (t + 1) = tm.step (tm.configs cfg t) := by + simp [configs, Function.iterate_succ_apply'] + /-- Any number of steps run from a halting configuration results in the same configuration. -/ @[simp, scoped grind =] lemma iter_step_eq_of_halt {cfg : Cfg k Symbol State input} {n : ℕ} (h_halt : cfg.state = none) : @@ -278,17 +286,35 @@ lemma workTapePos_step_le (c : Cfg k Symbol State input) (i : Fin k) : simp only [add_sub_cancel_left, abs_le, SignType.cast] grind +/-- A step changes the contents of a work tape at most at the current head position. -/ +lemma step_workTapes_eq_of_ne + (cfg : Cfg k Symbol State input) + (j : Fin k) + (z : ℤ) + (hz : z ≠ cfg.workTapePos j) : + (tm.step cfg).workTapes j z = cfg.workTapes j z := by + unfold step + cases hst : cfg.state with + | none => simp_all + | some q => + rcases hw : ((tm.tr q cfg.inputSymbol cfg.workTapeSymbols).workActions j).1 <;> simp_all + end Cfg section Space /-! Now we define space usage and add some helper lemmas. -/ +/-- The set of positions visited by the head of work tape `i` in the computation starting from +configuration `cfg` up to step `t`. -/ +def visitedByTapeHead (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : Finset ℤ := + (Finset.range (t + 1)).image fun t' => (tm.configs cfg t').workTapePos i + /-- The number of work tape cells touched by the head of tape `i` in the computation starting from configuration `cfg` up to step `t`. -/ def spaceUsedByTape (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : ℕ := - ((List.range (t + 1)).map fun t' => (tm.configs cfg t').workTapePos i).toFinset.card + (tm.visitedByTapeHead cfg t i).card /-- The number of work tape cells touched by a computation starting from configuration @@ -304,23 +330,10 @@ lemma spaceUsed_zero_tapes_eq_zero (cfg : Cfg k Symbol State input) (t : ℕ) (h subst h_zero simp -/-- The number of cells touched by a single work tape grows by at most one each step. -/ -lemma spaceUsedByTape_le (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : - tm.spaceUsedByTape cfg t i ≤ t + 1 := by - calc - tm.spaceUsedByTape cfg t i - _ ≤ ((List.range (t + 1)).map _).length := List.toFinset_card_le _ - _ = t + 1 := by simp - -/-- -The space used by a computation is bounded linearly by the number of steps. --/ -lemma spaceUsed_linear (cfg : Cfg k Symbol State input) (t : ℕ) : - tm.spaceUsed cfg t ≤ k * t + k := by - calc tm.spaceUsed cfg t - = ∑ i, (tm.spaceUsedByTape cfg t i) := by rfl - _ ≤ ∑ i, (t + 1) := Finset.sum_le_sum (fun i _ => tm.spaceUsedByTape_le cfg t i) - _ = k * t + k := by simp [Nat.mul_succ] +/-- Each tape's space usage is bounded by the total space used. -/ +lemma spaceUsedByTape_le_spaceUsed (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : + tm.spaceUsedByTape cfg t i ≤ tm.spaceUsed cfg t := + Finset.single_le_sum (fun _ _ => Nat.zero_le _) (Finset.mem_univ i) end Space @@ -377,6 +390,16 @@ lemma outputString_add_eq_append rw [show (t₁ + (t + 1)) = (t₁ + t) + 1 by omega] simp [outputString_succ, ih, configs, ← Function.iterate_add_apply, Nat.add_comm] +/-- The output does not change after the machine has halted. -/ +lemma outputString_eq_of_halt + (tm : MultiTapeTM k Symbol State) + (cfg : Cfg k Symbol State input) {τ t : ℕ} (hle : τ ≤ t) + (hhalt : (tm.configs cfg τ).state = none) : + tm.outputString cfg t = tm.outputString cfg τ := by + conv_lhs => rw [← Nat.sub_add_cancel hle, Nat.add_comm] + rw [outputString_add_eq_append, outputString_halt _ _ hhalt] + simp + /-- A proof that the Turing machine `tm` on input `input` outputs `output` in at most `t` steps and uses exactly `s` space. Note that this does not require the alphabet or state set to be finite. -/ @@ -475,6 +498,80 @@ lemma halting_step_unique rw [Function.iterate_add_apply, tm.iter_step_eq_of_halt halts₁] exact halts₁ +/-- Running `a + d` steps equals running `a` steps from the configuration reached after `d`. -/ +lemma configs_add (cfg : Cfg k Symbol State input) (a d : ℕ) : + tm.configs cfg (a + d) = tm.step^[a] (tm.configs cfg d) := by + unfold configs; rw [Function.iterate_add_apply] + +/-- Once a machine has halted at step `m`, its configuration is unchanged at any later step `n`. -/ +lemma halt_mono (cfg : Cfg k Symbol State input) {m n : ℕ} (h : m ≤ n) + (hm : (tm.configs cfg m).state = none) : + tm.configs cfg n = tm.configs cfg m := by + obtain ⟨d, rfl⟩ := Nat.exists_eq_add_of_le h + rw [Nat.add_comm, tm.configs_add, tm.iter_step_eq_of_halt hm] + +/-- If a deterministic machine revisits a non-halting configuration, it never halts: revisiting a +configuration makes the run periodic, so if some step were halting, the frozen halting +configuration would still be around at the next return to the repeated (non-halting) +configuration. -/ +lemma not_halts_of_repeat_nonhalt (cfg : Cfg k Symbol State input) + {t₁ t₂ : ℕ} (hne : t₁ ≠ t₂) + (heq : tm.configs cfg t₁ = tm.configs cfg t₂) + (hnh : (tm.configs cfg t₂).state ≠ none) : + ∀ t, (tm.configs cfg t).state ≠ none := by + wlog hlt : t₁ < t₂ generalizing t₁ t₂ + · exact this hne.symm heq.symm (heq ▸ hnh) (by omega) + intro t ht + -- The run returns to `configs t₁` every `t₂ - t₁` steps. + have hperiod : ∀ n, tm.configs cfg (t₁ + n * (t₂ - t₁)) = tm.configs cfg t₁ := by + intro n + induction n with + | zero => simp + | succ n ih => + rw [show t₁ + (n + 1) * (t₂ - t₁) = (t₂ - t₁) + (t₁ + n * (t₂ - t₁)) by grind, + tm.configs_add, ih, ← tm.configs_add, show t₂ - t₁ + t₁ = t₂ by omega, ← heq] + -- A halting step `t` freezes the run, so the return to `configs t₁` after step `t` + -- would make `configs t₁` halting as well — contradiction. + have hle : t ≤ t₁ + t * (t₂ - t₁) := + (Nat.le_mul_of_pos_right t (by omega)).trans (Nat.le_add_left _ _) + have h₁ : (tm.configs cfg t₁).state = none := by + rw [← hperiod t, tm.halt_mono cfg hle ht] + exact ht + rw [heq] at h₁ + exact hnh h₁ + +open scoped Classical in +/-- A deterministic machine that halts does so within a number of steps bounded by the number of +distinct configurations it visits. If it is halted by step `T₀`, then it is already halted at some +step `τ` no larger than the count of distinct configurations reached within `T₀` steps: otherwise +the first `card + 1` configurations would be non-halting and, being more numerous than the distinct +configurations available, two would coincide, making the machine loop forever by +`not_halts_of_repeat_nonhalt`. Together with `card_configs_le` this turns a space bound into a +time bound. -/ +lemma exists_halt_le_card_image (tm : MultiTapeTM k Symbol State) (input : List Symbol) {T₀ : ℕ} + (h : (tm.configs (tm.initCfg input) T₀).state = none) : + ∃ τ ≤ ((Finset.range (T₀ + 1)).image (tm.configs (tm.initCfg input))).card, + τ ≤ T₀ ∧ (tm.configs (tm.initCfg input) τ).state = none := by + classical + set f := tm.configs (tm.initCfg input) with hf + have hex : ∃ m, (f m).state = none := ⟨T₀, h⟩ + have hm0h : (f (Nat.find hex)).state = none := Nat.find_spec hex + have hfind : Nat.find hex ≤ T₀ := Nat.find_le h + refine ⟨Nat.find hex, ?_, hfind, hm0h⟩ + have hnh : ∀ x ∈ Finset.range (Nat.find hex), (f x).state ≠ none := fun x hx => + Nat.find_min hex (Finset.mem_range.1 hx) + have hinj : Set.InjOn f (Finset.range (Nat.find hex)) := by + intro x _ y hy hxy + by_contra hne + exact tm.not_halts_of_repeat_nonhalt (tm.initCfg input) hne hxy (hnh y (Finset.mem_coe.1 hy)) + (Nat.find hex) hm0h + have hsub : (Finset.range (Nat.find hex)).image f ⊆ (Finset.range (T₀ + 1)).image f := + Finset.image_subset_image (by + intro x hx; simp only [Finset.mem_range] at hx ⊢; omega) + calc Nat.find hex = ((Finset.range (Nat.find hex)).image f).card := by + rw [Finset.card_image_of_injOn hinj, Finset.card_range] + _ ≤ ((Finset.range (T₀ + 1)).image f).card := Finset.card_le_card hsub + end MultiTapeTM end Turing diff --git a/Cslib/Computability/Machines/Turing/MultiTape/SpaceInTime.lean b/Cslib/Computability/Machines/Turing/MultiTape/SpaceInTime.lean new file mode 100644 index 000000000..e1c6cdcae --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/SpaceInTime.lean @@ -0,0 +1,213 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +public import Cslib.Computability.Machines.Turing.MultiTape.ConfigBound +public import Cslib.Computability.Machines.Turing.MultiTape.Classes + +import Mathlib.Tactic.Ring + +/-! +# From space bounds to time bounds + +A deterministic machine that decides a language in space `s` cannot repeat a configuration before +halting, so the number of steps is bounded by the number of reachable configurations. Combined with +the configuration count of `ConfigBound`, this yields the inclusion +`DSPACE(s) ⊆ DTIME(2^{O(s)})`. + +Two forms are provided: + +* `space_subset_time_general` makes no assumption on `s` and keeps the input-length factor + `n`, which counts the read-only input-head positions. This factor is essential in general: + for `s = O(1)` the class is the regular languages, decided in `Θ(n)` time, so the constant base + `2 ^ (c * s n)` cannot absorb it. +* `space_subset_time` is the textbook statement `DSPACE(s) ⊆ DTIME(2^{O(s)})`, valid under the + assumption `s(n) ≥ log n`, under which the input-length factor is absorbed into the exponential. + +Both are stated as `DSPACE s ⊆ ⋃ c, DTIME (fun n => ... 2 ^ (c * s n))`: the union over the constant +`c` is exactly the `O` in `2^{O(s)}`. + +Two inclusions for specific complexity classes are derived from this: + +* `logspace_subset_p` shows `L ⊆ P` +* `pspace_subset_exp` shows `PSPACE ⊆ EXP` + +-/ + +@[expose] public section + +open Cslib + +namespace Turing.MultiTapeTM + +open scoped Classical in +/-- A Turing machine that computes `output` in `t` steps using space at most `σ` already computes +it within `(input.length + 2) * storageBound Symbol State k σ` steps, using no more space. -/ +lemma ComputesInTimeAndSpace.truncate + {Symbol State : Type} [Fintype Symbol] [Fintype State] + {k : ℕ} + {tm : MultiTapeTM k Symbol State} + {input output : List Symbol} + {t s σ : ℕ} + (h : tm.ComputesInTimeAndSpace input output t s) + (hσ : s ≤ σ) : + ∃ t' ≤ (input.length + 2) * storageBound Symbol State k σ, + ∃ s' ≤ s, tm.ComputesInTimeAndSpace input output t' s' := by + obtain ⟨hhalt, hout, hspace⟩ := h + obtain ⟨τ, hτcard, hτle, hτhalt⟩ := exists_halt_le_card_image tm input hhalt + rw [tm.outputString_eq_of_halt (tm.initCfg input) hτle hτhalt] at hout + exact ⟨τ, hτcard.trans (card_configs_le t σ (hspace.trans_le hσ)), + tm.spaceUsed (tm.initCfg input) τ, (spaceUsed_mono tm _ hτle).trans hspace.le, + hτhalt, hout, rfl⟩ + +/-- General form of the space-to-time inclusion, making no assumption on `s`. The input-length +factor `n` accounts for the read-only input-head positions and cannot be dropped in general. For +`n = 0` the factor vanishes, so the additive constant of `DTIME` covers that single input (its +bound depends on `s 0`, which is fine since `s` is fixed before the constants are chosen). -/ +theorem space_subset_time_general + {Symbol : Type} [Inhabited Symbol] + (s : ℕ → ℕ) : + DSPACE s ⊆ ⋃ c, DTIME (Symbol := Symbol) (fun n => n * 2 ^ (c * s n)) := by + rintro L ⟨c₁, c₂, tBound, kk, sym, state, emb, tm, hcomp⟩ + obtain ⟨a, c, hSB⟩ := storageBound_le_pow (Symbol := Fin sym) (State := Fin state) kk + -- The same machine witnesses the time bound; the exponent constant is `c * c₁`, while `c₂` + -- (the additive space constant) and `a` (from `storageBound_le_pow`) are absorbed into the + -- multiplicative constant of `DTIME` (via `n + 2 ≤ 3 * n` for `n ≥ 1`); the `n = 0` input is + -- covered by the additive constant. + refine Set.mem_iUnion.2 ⟨c * c₁, + 3 * (a * 2 ^ (c * c₂)), 2 * (a * 2 ^ (c * c₂)) * 2 ^ (c * c₁ * s 0), + fun n => c₁ * s n + c₂, kk, sym, state, emb, tm, fun input => ?_⟩ + set n := input.length with hn + obtain ⟨t, -, σ, hσ, hcomp'⟩ := hcomp input + -- Truncate the computation to the configuration-count bound... + obtain ⟨t', ht', s', hs', hc⟩ := hcomp'.truncate (σ := c₁ * s n + c₂) hσ + refine ⟨t', ?_, s', hs'.trans hσ, hc⟩ + -- ...and bound the configuration count by the exponential. + have h1 : t' ≤ (n + 2) * (a * 2 ^ (c * c₂) * 2 ^ (c * c₁ * s n)) := by + calc t' + ≤ (n + 2) * storageBound (Fin sym) (Fin state) kk (c₁ * s n + c₂) := by simpa [hn] using ht' + _ ≤ (n + 2) * (a * 2 ^ (c * (c₁ * s n + c₂))) := by gcongr; exact hSB _ + _ = (n + 2) * (a * 2 ^ (c * c₂) * 2 ^ (c * c₁ * s n)) := by + rw [show c * (c₁ * s n + c₂) = c * c₂ + c * c₁ * s n by ring, pow_add]; ring + rcases Nat.eq_zero_or_pos n with h0 | hpos + · rw [h0] at h1 ⊢ + calc t' ≤ 2 * (a * 2 ^ (c * c₂) * 2 ^ (c * c₁ * s 0)) := h1 + _ ≤ _ := by simp [mul_assoc] + · calc t' ≤ (n + 2) * (a * 2 ^ (c * c₂) * 2 ^ (c * c₁ * s n)) := h1 + _ ≤ 3 * n * (a * 2 ^ (c * c₂) * 2 ^ (c * c₁ * s n)) := + Nat.mul_le_mul_right _ (by omega) + _ = 3 * (a * 2 ^ (c * c₂)) * (n * 2 ^ (c * c₁ * s n)) := by ring + _ ≤ _ := Nat.le_add_right _ _ + +/-- If `log₂ n ≤ m` then `n < 2 ^ (m + 1)`. This is the arithmetic core of the `s ≥ log` hypothesis +used to absorb the input-length factor into the exponential. -/ +lemma lt_two_pow_succ_of_log2_le {n m : ℕ} (h : Nat.log2 n ≤ m) : n < 2 ^ (m + 1) := by + rcases Nat.eq_zero_or_pos n with rfl | hn + · exact pow_pos (by norm_num) _ + · rw [← Nat.log2_lt (by omega)]; omega + +/-- The textbook space-to-time inclusion `DSPACE(s) ⊆ DTIME(2^{O(s)})`, under the standard +assumption `s(n) ≥ log n`, here expressed as `Nat.log2 n ≤ s n`. It follows from +`space_subset_time_general` by absorbing the input-length factor into the exponential +(`n < 2 ^ (s n + 1)`). -/ +theorem space_subset_time + {Symbol : Type} [Inhabited Symbol] (s : ℕ → ℕ) (hs : s ≥ Nat.log2) : + DSPACE s ⊆ ⋃ c, DTIME (Symbol := Symbol) (fun n => 2 ^ (c * s n)) := by + intro L hL + obtain ⟨c, hc⟩ := Set.mem_iUnion.1 (space_subset_time_general s hL) + obtain ⟨c₁, c₂, s', hd⟩ := hc + refine Set.mem_iUnion.2 ⟨c + 1, 2 * c₁, c₂, s', hd.mono_time fun n => ?_⟩ + have hlt : n < 2 ^ (s n + 1) := lt_two_pow_succ_of_log2_le (hs n) + calc c₁ * (n * 2 ^ (c * s n)) + c₂ + ≤ c₁ * (2 ^ (s n + 1) * 2 ^ (c * s n)) + c₂ := by gcongr + _ = 2 * c₁ * 2 ^ ((c + 1) * s n) + c₂ := by + rw [← pow_add, show s n + 1 + c * s n = (c + 1) * s n + 1 by ring, pow_succ]; ring + +open Classes + +/-- `2 ^ log₂ n ≤ n + 1` for all `n`, including `n = 0` (where both sides are `1`). -/ +lemma two_pow_log2_le_succ (n : ℕ) : 2 ^ Nat.log2 n ≤ n + 1 := by + rcases Nat.eq_zero_or_pos n with rfl | hn + · simp + · exact (Nat.log2_self_le hn.ne').trans n.le_succ + +/-- `(n + 1) ^ c ≤ 2 ^ c * n ^ c + 1` for all `n, c`: the `n = 0` case forces the `+ 1`, while for +`n ≥ 1` it follows from `n + 1 ≤ 2 * n`. -/ +lemma succ_pow_le (n c : ℕ) : (n + 1) ^ c ≤ 2 ^ c * n ^ c + 1 := by + rcases Nat.eq_zero_or_pos n with rfl | hn + · simp + · calc (n + 1) ^ c ≤ (2 * n) ^ c := Nat.pow_le_pow_left (by omega) c + _ = 2 ^ c * n ^ c := mul_pow .. + _ ≤ 2 ^ c * n ^ c + 1 := Nat.le_succ _ + +/-- The inclusion `L ⊆ P`: every log-space decidable language is decidable in polynomial time. -/ +theorem logspace_subset_p {Symbol : Type} [Inhabited Symbol] : + L (Symbol := Symbol) ⊆ P := by + intro L hL + obtain ⟨c, hc⟩ := Set.mem_iUnion.1 (space_subset_time Nat.log2 le_rfl hL) + obtain ⟨c₁, c₂, s, hd⟩ := hc + refine Set.mem_iUnion.2 ⟨c, c₁ * 2 ^ c, c₁ + c₂, s, hd.mono_time fun n => ?_⟩ + calc c₁ * 2 ^ (c * Nat.log2 n) + c₂ + = c₁ * (2 ^ Nat.log2 n) ^ c + c₂ := by rw [mul_comm c, pow_mul] + _ ≤ c₁ * (n + 1) ^ c + c₂ := + Nat.add_le_add_right (Nat.mul_le_mul_left c₁ + (Nat.pow_le_pow_left (two_pow_log2_le_succ n) c)) c₂ + _ ≤ c₁ * (2 ^ c * n ^ c + 1) + c₂ := + Nat.add_le_add_right (Nat.mul_le_mul_left c₁ (succ_pow_le n c)) c₂ + _ = c₁ * 2 ^ c * n ^ c + (c₁ + c₂) := by ring + +/-- `n ≤ n ^ k` for all `n` when `k ≥ 1`. -/ +lemma Nat.le_self_pow_of_pos {n k : ℕ} (hk : 1 ≤ k) : n ≤ n ^ k := by + rcases n with _ | n + · simp + · calc n + 1 ≤ (n + 1) ^ 1 := by rw [pow_one] + _ ≤ (n + 1) ^ k := Nat.pow_le_pow_right (by omega) hk + +/-- `c * n ^ k ≤ n ^ (k + 1) + c ^ (k + 1)` for all `n, c, k`: if `n ≥ c` the first summand alone +dominates, and if `n < c` the second summand alone dominates. -/ +lemma mul_pow_le_pow_succ_add (c n k : ℕ) : c * n ^ k ≤ n ^ (k + 1) + c ^ (k + 1) := by + rcases le_total c n with h | h + · calc c * n ^ k ≤ n * n ^ k := Nat.mul_le_mul_right _ h + _ = n ^ (k + 1) := by rw [pow_succ'] + _ ≤ n ^ (k + 1) + c ^ (k + 1) := Nat.le_add_right _ _ + · calc c * n ^ k ≤ c * c ^ k := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left h k) + _ = c ^ (k + 1) := by rw [pow_succ'] + _ ≤ n ^ (k + 1) + c ^ (k + 1) := Nat.le_add_left _ _ + +/-- The inclusion `PSPACE ⊆ EXP`. For space bound `n ^ 0 = 1` (constant space), the input-length +factor from `space_subset_time_general` is absorbed via `n ≤ 2 ^ n`. For space bound `n ^ (k + 1)` +(`k ≥ 0`), `space_subset_time` applies since `log₂ n ≤ n ≤ n ^ (k + 1)`, and the exponent +`c * n ^ (k + 1)` is absorbed into `n ^ (k + 2)` via `mul_pow_le_pow_succ_add`. -/ +theorem pspace_subset_exp {Symbol : Type} [Inhabited Symbol] : + PSPACE (Symbol := Symbol) ⊆ EXP := by + intro L hL + obtain ⟨k, hLk⟩ := Set.mem_iUnion.1 hL + rcases k with _ | k + · -- constant space + simp only [pow_zero] at hLk + obtain ⟨c, hc⟩ := Set.mem_iUnion.1 (space_subset_time_general (fun _ => 1) hLk) + obtain ⟨c₁, c₂, s, hd⟩ := hc + refine Set.mem_iUnion.2 ⟨1, c₁ * 2 ^ c, c₂, s, hd.mono_time fun n => ?_⟩ + calc c₁ * (n * 2 ^ (c * 1)) + c₂ + = c₁ * (n * 2 ^ c) + c₂ := by rw [mul_one] + _ ≤ c₁ * (2 ^ n * 2 ^ c) + c₂ := + Nat.add_le_add_right (Nat.mul_le_mul_left c₁ + (Nat.mul_le_mul_right _ n.lt_two_pow_self.le)) c₂ + _ = c₁ * 2 ^ c * 2 ^ (n ^ 1) + c₂ := by rw [pow_one]; ring + · -- space bound `n ^ (k + 1)` + have hlog : Nat.log2 ≤ (fun n => n ^ (k + 1)) := + fun n => (Nat.log2_le_self n).trans (Nat.le_self_pow_of_pos (by omega)) + obtain ⟨c, hc⟩ := Set.mem_iUnion.1 (space_subset_time (fun n => n ^ (k + 1)) hlog hLk) + obtain ⟨c₁, c₂, s, hd⟩ := hc + refine Set.mem_iUnion.2 ⟨k + 2, c₁ * 2 ^ (c ^ (k + 2)), c₂, s, hd.mono_time fun n => ?_⟩ + have key : c * n ^ (k + 1) ≤ n ^ (k + 2) + c ^ (k + 2) := mul_pow_le_pow_succ_add c n (k + 1) + calc c₁ * 2 ^ (c * n ^ (k + 1)) + c₂ + ≤ c₁ * 2 ^ (n ^ (k + 2) + c ^ (k + 2)) + c₂ := + Nat.add_le_add_right (Nat.mul_le_mul_left c₁ (Nat.pow_le_pow_right (by norm_num) key)) c₂ + _ = c₁ * 2 ^ (c ^ (k + 2)) * 2 ^ (n ^ (k + 2)) + c₂ := by rw [pow_add]; ring + +end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean new file mode 100644 index 000000000..269ff1704 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean @@ -0,0 +1,144 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic + +/-! +# Tape head visitation and space-usage lemmas + +This file collects lemmas about the set of positions visited by a work-tape head +(`MultiTapeTM.visitedByTapeHead`) and the resulting space-usage measures +(`MultiTapeTM.spaceUsedByTape`, `MultiTapeTM.spaceUsed`) that are not needed to state the core +definitions in `Deterministic.lean`, but are reusable building blocks for counting and bounding +arguments elsewhere (e.g. `ConfigBound.lean`). + +The key geometric facts are `MultiTapeTM.natAbs_le_spaceUsedByTape_of_mem_visited` and +`MultiTapeTM.content_natAbs_le_spaceUsedByTape`: starting from the all-blank tapes with every head +at `0` and moving by at most one cell per step, a computation in which tape `i` has visited at most +`sᵢ` cells keeps that tape's head position and every non-blank cell within `sᵢ` of the origin. +-/ + +@[expose] public section + +namespace Turing.MultiTapeTM + +variable {k : ℕ} +variable {State Symbol : Type*} +variable {input : List Symbol} +variable {tm : MultiTapeTM k Symbol State} +variable {cfg : Cfg k Symbol State input} + +lemma mem_visitedByTapeHead {t : ℕ} {i : Fin k} {z : ℤ} : + z ∈ tm.visitedByTapeHead cfg t i ↔ ∃ t' < t + 1, (tm.configs cfg t').workTapePos i = z := by + simp [visitedByTapeHead] + +lemma mem_visitedByTapeHead_self (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : + (tm.configs cfg t).workTapePos i ∈ tm.visitedByTapeHead cfg t i := + tm.mem_visitedByTapeHead.mpr ⟨t, by omega, rfl⟩ + +/-- The set of positions visited by a tape head is monotone in the number of steps. -/ +lemma visitedByTapeHead_mono (cfg : Cfg k Symbol State input) (i : Fin k) + {t t' : ℕ} (h : t ≤ t') : + tm.visitedByTapeHead cfg t i ⊆ tm.visitedByTapeHead cfg t' i := by + apply Finset.image_subset_image + grind + +/-- Discrete intermediate value: Starting from configuration `cfg`, every position between the +initial head position of tape `i` and the one after `t` steps is part of the "visited set" at +step `t`. -/ +lemma uIcc_subset_visitedByTapeHead (cfg : Cfg k Symbol State input) (i : Fin k) (t : ℕ) : + Finset.uIcc (cfg.workTapePos i) ((tm.configs cfg t).workTapePos i) + ⊆ tm.visitedByTapeHead cfg t i := by + induction t with + | zero => simpa [configs] using tm.mem_visitedByTapeHead_self cfg 0 i + | succ t ih => + intro z hz + have hstep : |(tm.configs cfg (t + 1)).workTapePos i - (tm.configs cfg t).workTapePos i| ≤ 1 := + configs_succ_eq_step' (tm := tm) ▸ tm.workTapePos_step_le _ i + have hmono := tm.visitedByTapeHead_mono cfg i (Nat.le_succ t) + have hself := tm.mem_visitedByTapeHead_self cfg (t + 1) i + grind [Finset.mem_uIcc] + +/-- If a work tape cell is changed after `t` steps, it must have been visited by the tape head. -/ +lemma mem_visitedByTapeHead_of_workTapes_ne + (j : Fin k) + (t : ℕ) + (z : ℤ) + (h : (tm.configs cfg t).workTapes j z ≠ cfg.workTapes j z) : + z ∈ tm.visitedByTapeHead cfg t j := by + induction t with + | zero => exact absurd (by simp [configs]) h + | succ t ih => + rw [configs_succ_eq_step'] at h + by_cases hz : z = (tm.configs cfg t).workTapePos j + · exact hz ▸ tm.visitedByTapeHead_mono cfg j (Nat.le_succ t) + (tm.mem_visitedByTapeHead_self cfg t j) + · rw [tm.step_workTapes_eq_of_ne _ j z hz] at h + exact tm.visitedByTapeHead_mono cfg j (Nat.le_succ t) (ih h) + +/-- Every position visited by the head of tape `i` lies within `spaceUsedByTape … i` of the +head's starting position: by the discrete intermediate value property, the whole interval between +the two positions has been visited, and `spaceUsedByTape` counts the visited positions. -/ +lemma natAbs_le_spaceUsedByTape_of_mem_visited + {i : Fin k} + {z : ℤ} + {t : ℕ} + (hz : z ∈ tm.visitedByTapeHead cfg t i) : + (z - cfg.workTapePos i).natAbs ≤ tm.spaceUsedByTape cfg t i := by + obtain ⟨t', ht', rfl⟩ := tm.mem_visitedByTapeHead.mp hz + have h1 := Finset.card_le_card + ((tm.uIcc_subset_visitedByTapeHead cfg i t').trans + (tm.visitedByTapeHead_mono cfg i (show t' ≤ t by omega))) + rw [Int.card_uIcc] at h1 + unfold spaceUsedByTape + omega + +/-- Every non-blank cell on work tape `i` lies within `spaceUsedByTape … i t` of the origin. -/ +lemma content_natAbs_le_spaceUsedByTape + {i : Fin k} + (t : ℕ) + (z : ℤ) + (h : (tm.configs (tm.initCfg input) t).workTapes i z ≠ none) : + z.natAbs ≤ tm.spaceUsedByTape (tm.initCfg input) t i := by + -- The work tapes start out blank, so any non-blank cell has been visited by the head; the + -- initial head position is `0`, so the displacement bound is a bound on the position itself. + simpa using tm.natAbs_le_spaceUsedByTape_of_mem_visited + (tm.mem_visitedByTapeHead_of_workTapes_ne i t z h) + +/-- The number of cells touched by a single work tape grows by at most one each step. -/ +lemma spaceUsedByTape_le (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : + tm.spaceUsedByTape cfg t i ≤ t + 1 := by + calc + tm.spaceUsedByTape cfg t i + _ ≤ (Finset.range (t + 1)).card := Finset.card_image_le + _ = t + 1 := Finset.card_range _ + +/-- The space used by a computation is bounded linearly by the number of steps. -/ +lemma spaceUsed_linear (cfg : Cfg k Symbol State input) (t : ℕ) : + tm.spaceUsed cfg t ≤ k * t + k := by + calc tm.spaceUsed cfg t + = ∑ i, (tm.spaceUsedByTape cfg t i) := by rfl + _ ≤ ∑ 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 a single tape is monotone in the number of steps. -/ +lemma spaceUsedByTape_mono + (tm : MultiTapeTM k Symbol State) + (cfg : Cfg k Symbol State input) + (i : Fin k) : + Monotone (tm.spaceUsedByTape cfg · i) := by + intro t t' h + exact Finset.card_le_card (tm.visitedByTapeHead_mono cfg i h) + +/-- The total space used is monotone in the number of steps. -/ +lemma spaceUsed_mono (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) : + Monotone (tm.spaceUsed cfg ·) := by + intro t t' h + exact Finset.sum_le_sum (fun i _ => spaceUsedByTape_mono tm cfg i h) + +end Turing.MultiTapeTM From 6cda8b53452f740ff75dcea94a68f885b1fe6a23 Mon Sep 17 00:00:00 2001 From: crei Date: Sat, 1 Aug 2026 11:11:59 +0200 Subject: [PATCH 2/2] Add references. --- .../Machines/Turing/MultiTape/Classes.lean | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Classes.lean b/Cslib/Computability/Machines/Turing/MultiTape/Classes.lean index 4a56a44e6..78d1d9393 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Classes.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Classes.lean @@ -19,12 +19,14 @@ machines on top of `DecidableInTimeAndSpace`. ## Design -The primitives `DTIME` and `DSPACE` are defined using a single bound function `ℕ → ℕ` but allow -for `O`-fuzzyness. Using this fuzzyness is justified by the space and time compression / speedup -results which are not proven here. Once we have better machinery, we can prove them and potentially -move to exact bounds. +The general classes `DTIME` and `DSPACE` are defined using a single bound function `ℕ → ℕ` but allow +for `O`-fuzzyness. Some textbooks use exact bounds ([Papadimitriou94]), while others use a +definition similar to this one ([AroraBarak09], [Sipser2013]). The fuzzy definition is justified by +the space and time compression / speedup theorems (which are not proven here) and allow for +easier proofs and simpler theorem statements. Once we have better machinery, we can prove the +compression / speedup theorems and potentially move to exact bounds. -The classes are always relative to a `Symbol` alphabet. +The classes are always relative to an alphabet `Symbol`. ## Important Declarations @@ -35,6 +37,13 @@ Some named complexity classes are defined in the `Classes` namespace: * `P`, `E`, `EXP` * `L`, `PSPACE`, `ESPACE`, `EXPSPACE` + +## References + +* [C. Papadimitriou, *Computational Complexity*][Papadimitriou94] +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09] +* [M. Sipser, *Introduction to the Theory of Computation*][Sipser2013] + -/ @[expose] public section