From 20f3f0cd093cb256f9dd0c62df6842bd401a5c14 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Thu, 5 Mar 2026 22:57:17 -0500 Subject: [PATCH 1/2] refactor(Computability): improve SingleTapeTM composition API Move Symbol typeclass assumptions into SingleTapeTM fields, reducing repeated section-level assumptions. Add core transition lemmas: determinism of TransitionRelation, no_step_from_halt, and reachable_steps_le_halting_steps for bounding chain lengths to halting endpoints. Introduce monotoneEnvelope for running maxima, with proofs of monotonicity, pointwise bounds, and comparison with monotone upper bounds. Add TimeComputable.toMonotone and rewrite TimeComputable.comp to internalize monotonicity handling, removing the external monotonicity parameter from composition. Update PolyTimeComputable.comp accordingly. --- .../Machines/SingleTapeTuring/Basic.lean | 199 +++++++++++++----- 1 file changed, 147 insertions(+), 52 deletions(-) diff --git a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean index 4f31c153..4435bf6e 100644 --- a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean +++ b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean @@ -89,11 +89,15 @@ end SingleTapeTM A single-tape Turing machine over the alphabet of `Option Symbol` (where `none` is the blank `BiTape` symbol). -/ -structure SingleTapeTM Symbol [Inhabited Symbol] [Fintype Symbol] where +structure SingleTapeTM Symbol where + /-- Inhabited instance for the alphabet -/ + [SymbolInhabited : Inhabited Symbol] + /-- Finiteness of the alphabet -/ + [SymbolFintype : Fintype Symbol] /-- type of state labels -/ (State : Type) /-- finiteness of the state type -/ - [stateFintype : Fintype State] + [StateFintype : Fintype State] /-- Initial state -/ (q₀ : State) /-- Transition function, mapping a state and a head symbol to a `Stmt` to invoke, @@ -112,11 +116,11 @@ the step function that lets the machine transition from one configuration to the and the intended initial and final configurations. -/ -variable [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) +variable (tm : SingleTapeTM Symbol) instance : Inhabited tm.State := ⟨tm.q₀⟩ -instance : Fintype tm.State := tm.stateFintype +instance : Fintype tm.State := tm.StateFintype instance inhabitedStmt : Inhabited (Stmt Symbol) := inferInstance @@ -186,8 +190,6 @@ end Cfg open Cfg -variable [Inhabited Symbol] [Fintype Symbol] - /-- The `TransitionRelation` corresponding to a `SingleTapeTM Symbol` is defined by the `step` function, @@ -196,6 +198,42 @@ which maps a configuration to its next configuration, if it exists. @[scoped grind =] def TransitionRelation (tm : SingleTapeTM Symbol) (c₁ c₂ : tm.Cfg) : Prop := tm.step c₁ = some c₂ +/-- The transition relation is deterministic: each configuration has at most +one successor, since `step` is a function. -/ +lemma TransitionRelation_deterministic (tm : SingleTapeTM Symbol) + (a b c : tm.Cfg) (hab : tm.TransitionRelation a b) (hac : tm.TransitionRelation a c) : + b = c := by + simp only [TransitionRelation] at hab hac + rw [hab] at hac + exact Option.some.inj hac + +/-- No transitions from a halted configuration (state = none). -/ +lemma no_step_from_halt (tm : SingleTapeTM Symbol) (cfg cfg' : tm.Cfg) + (h : cfg.state = none) : ¬tm.TransitionRelation cfg cfg' := by + simp only [TransitionRelation, step] + cases cfg with | mk state tape => subst h; simp + +/-- In a deterministic relation where the endpoint has no successors, +any chain starting from the same origin has length at most `n`. -/ +lemma reachable_steps_le_halting_steps (tm : SingleTapeTM Symbol) + {a b : tm.Cfg} {n : ℕ} (hab : RelatesInSteps tm.TransitionRelation a b n) + (hhalt : ∀ cfg', ¬tm.TransitionRelation b cfg') + {c : tm.Cfg} {m : ℕ} (hac : RelatesInSteps tm.TransitionRelation a c m) : + m ≤ n := by + induction m generalizing a n with + | zero => omega + | succ k ih => + obtain ⟨a', ha_a', hac'⟩ := hac.succ' + match n, hab with + | 0, hab => + have := hab.zero; subst this + exact absurd ha_a' (hhalt a') + | n'+1, hab => + obtain ⟨a'', ha_a'', hab'⟩ := hab.succ' + have := TransitionRelation_deterministic tm a a' a'' ha_a' ha_a'' + subst this + exact Nat.succ_le_succ (ih hab' hac') + /-- A proof of `tm` outputting `l'` on input `l`. -/ def Outputs (tm : SingleTapeTM Symbol) (l l' : List Symbol) : Prop := ReflTransGen tm.TransitionRelation (initCfg tm l) (haltCfg tm l') @@ -220,6 +258,8 @@ lemma output_length_le_input_length_add_time (tm : SingleTapeTM Symbol) (l l' : section Computers +variable [Inhabited Symbol] [Fintype Symbol] + /-- A Turing machine computing the identity. -/ def idComputer : SingleTapeTM Symbol where State := PUnit @@ -374,6 +414,38 @@ end compComputerLemmas end Computers +/-! +## Monotone Envelope + +The running maximum of a function, used to convert arbitrary time bounds +into monotone time bounds without changing the underlying Turing machine. +-/ + +/-- The running maximum of `f`: `monotoneEnvelope f n = max (f 0) (f 1) ⋯ (f n)`. -/ +def monotoneEnvelope (f : ℕ → ℕ) : ℕ → ℕ + | 0 => f 0 + | n + 1 => max (monotoneEnvelope f n) (f (n + 1)) + +theorem monotoneEnvelope_mono (f : ℕ → ℕ) : Monotone (monotoneEnvelope f) := by + intro a b hab + induction hab with + | refl => exact le_refl _ + | step _ ih => exact le_trans ih (le_max_left _ _) + +theorem le_monotoneEnvelope (f : ℕ → ℕ) (n : ℕ) : f n ≤ monotoneEnvelope f n := by + cases n with + | zero => exact le_refl _ + | succ n => exact le_max_right _ _ + +theorem monotoneEnvelope_le_of_le_monotone {f g : ℕ → ℕ} + (hle : ∀ n, f n ≤ g n) (hg : Monotone g) (n : ℕ) : + monotoneEnvelope f n ≤ g n := by + induction n with + | zero => exact hle 0 + | succ n ih => + simp only [monotoneEnvelope] + exact max_le (le_trans ih (hg (Nat.le_succ n))) (hle (n + 1)) + /-! ## Time Computability @@ -401,6 +473,15 @@ def TimeComputable.id : TimeComputable (Symbol := Symbol) id where time_bound _ := 1 outputsFunInTime _ := ⟨1, le_rfl, RelatesInSteps.single rfl⟩ +/-- Convert a `TimeComputable` to one with a monotone time bound, +using the same TM but replacing the time bound with its monotone envelope. -/ +def TimeComputable.toMonotone {f : List Symbol → List Symbol} + (hf : TimeComputable f) : TimeComputable f where + tm := hf.tm + time_bound := monotoneEnvelope hf.time_bound + outputsFunInTime a := RelatesWithinSteps.of_le + (hf.outputsFunInTime a) (le_monotoneEnvelope hf.time_bound a.length) + /-- Time bounds for `compComputer`. @@ -410,46 +491,44 @@ The `compComputer` of two machines which have time bounds is bounded by * added to the time taken by the second machine on the output size of the first machine (which is itself bounded by the time taken by the first machine) -Note that we require the time function of the second machine to be monotone; -this is to ensure that if the first machine returns an output -which is shorter than the maximum possible length of output for that input size, -then the time bound for the second machine still holds for that shorter input to the second machine. +The time bound of the second machine is automatically made monotone using +`monotoneEnvelope`, so the caller does not need to supply a monotonicity proof. -/ def TimeComputable.comp {f g : List Symbol → List Symbol} - (hf : TimeComputable f) (hg : TimeComputable g) - (h_mono : Monotone hg.time_bound) : - (TimeComputable (g ∘ f)) where - tm := compComputer hf.tm hg.tm - -- perhaps it would be good to track the blow up separately? - time_bound l := (hf.time_bound l) + hg.time_bound (max 1 l + hf.time_bound l) - outputsFunInTime a := by - have hf_outputsFun := hf.outputsFunInTime a - have hg_outputsFun := hg.outputsFunInTime (f a) - simp only [OutputsWithinTime, initCfg, compComputer_q₀_eq, Function.comp_apply, - haltCfg] at hg_outputsFun hf_outputsFun ⊢ - -- The computer reduces a to f a in time hf.time_bound a.length - have h_a_reducesTo_f_a : - RelatesWithinSteps (compComputer hf.tm hg.tm).TransitionRelation - (initialCfg hf.tm hg.tm a) - (intermediateCfg hf.tm hg.tm (f a)) - (hf.time_bound a.length) := - comp_left_relatesWithinSteps hf.tm hg.tm a (f a) - (hf.time_bound a.length) hf_outputsFun - -- The computer reduces f a to g (f a) in time hg.time_bound (f a).length - have h_f_a_reducesTo_g_f_a : - RelatesWithinSteps (compComputer hf.tm hg.tm).TransitionRelation - (intermediateCfg hf.tm hg.tm (f a)) - (finalCfg hf.tm hg.tm (g (f a))) - (hg.time_bound (f a).length) := - comp_right_relatesWithinSteps hf.tm hg.tm (f a) (g (f a)) - (hg.time_bound (f a).length) hg_outputsFun - -- Therefore, the computer reduces a to g (f a) in the sum of those times. - have h_a_reducesTo_g_f_a := RelatesWithinSteps.trans h_a_reducesTo_f_a h_f_a_reducesTo_g_f_a - apply RelatesWithinSteps.of_le h_a_reducesTo_g_f_a - refine Nat.add_le_add_left ?_ (hf.time_bound a.length) - · apply h_mono - -- Use the lemma about output length being bounded by input length + time - exact output_length_le_input_length_add_time hf.tm _ _ _ (hf.outputsFunInTime a) + (hf : TimeComputable f) (hg : TimeComputable g) : + (TimeComputable (g ∘ f)) := + let hg' := hg.toMonotone + { tm := compComputer hf.tm hg'.tm + -- perhaps it would be good to track the blow up separately? + time_bound := fun l => (hf.time_bound l) + hg'.time_bound (max 1 l + hf.time_bound l) + outputsFunInTime := fun a => by + have hf_outputsFun := hf.outputsFunInTime a + have hg_outputsFun := hg'.outputsFunInTime (f a) + simp only [OutputsWithinTime, initCfg, compComputer_q₀_eq, Function.comp_apply, + haltCfg] at hg_outputsFun hf_outputsFun ⊢ + -- The computer reduces a to f a in time hf.time_bound a.length + have h_a_reducesTo_f_a : + RelatesWithinSteps (compComputer hf.tm hg'.tm).TransitionRelation + (initialCfg hf.tm hg'.tm a) + (intermediateCfg hf.tm hg'.tm (f a)) + (hf.time_bound a.length) := + comp_left_relatesWithinSteps hf.tm hg'.tm a (f a) + (hf.time_bound a.length) hf_outputsFun + -- The computer reduces f a to g (f a) in time hg'.time_bound (f a).length + have h_f_a_reducesTo_g_f_a : + RelatesWithinSteps (compComputer hf.tm hg'.tm).TransitionRelation + (intermediateCfg hf.tm hg'.tm (f a)) + (finalCfg hf.tm hg'.tm (g (f a))) + (hg'.time_bound (f a).length) := + comp_right_relatesWithinSteps hf.tm hg'.tm (f a) (g (f a)) + (hg'.time_bound (f a).length) hg_outputsFun + -- Therefore, the computer reduces a to g (f a) in the sum of those times. + have h_a_reducesTo_g_f_a := RelatesWithinSteps.trans h_a_reducesTo_f_a h_f_a_reducesTo_g_f_a + apply RelatesWithinSteps.of_le h_a_reducesTo_g_f_a + refine Nat.add_le_add_left ?_ (hf.time_bound a.length) + · apply monotoneEnvelope_mono + -- Use the lemma about output length being bounded by input length + time + exact output_length_le_input_length_add_time hf.tm _ _ _ (hf.outputsFunInTime a) } end TimeComputable @@ -468,6 +547,17 @@ section PolyTimeComputable open Polynomial +/-- Evaluation of a polynomial with natural number coefficients is monotone. -/ +private theorem poly_eval_nat_mono (p : Polynomial ℕ) : Monotone (fun n => p.eval n) := by + intro a b hab + induction p using Polynomial.induction_on' with + | add p q ihp ihq => + simp only [eval_add] + exact Nat.add_le_add (ihp) (ihq) + | monomial n c => + simp only [eval_monomial] + exact Nat.mul_le_mul_left c (pow_le_pow_left' hab n) + variable [Inhabited Symbol] [Fintype Symbol] /-- A Turing machine + a polynomial time function + @@ -479,27 +569,32 @@ structure PolyTimeComputable (f : List Symbol → List Symbol) extends TimeCompu bounds : ∀ n, time_bound n ≤ poly.eval n /-- A proof that the identity map on Symbol is computable in polytime. -/ -noncomputable def PolyTimeComputable.id : PolyTimeComputable (Symbol := Symbol) id where +noncomputable def PolyTimeComputable.id : @PolyTimeComputable (Symbol := Symbol) id where toTimeComputable := TimeComputable.id poly := 1 bounds _ := by simp [TimeComputable.id] --- TODO remove `h_mono` assumption --- by developing function to convert PolyTimeComputable into one with monotone time bound /-- A proof that the composition of two polytime computable functions is polytime computable. + +The monotonicity of time bounds is handled internally via `monotoneEnvelope`, +so no monotonicity assumption is needed from the caller. -/ noncomputable def PolyTimeComputable.comp {f g : List Symbol → List Symbol} - (hf : PolyTimeComputable f) (hg : PolyTimeComputable g) - (h_mono : Monotone hg.time_bound) : + (hf : PolyTimeComputable f) (hg : PolyTimeComputable g) : PolyTimeComputable (g ∘ f) where - toTimeComputable := TimeComputable.comp hf.toTimeComputable hg.toTimeComputable h_mono + toTimeComputable := TimeComputable.comp hf.toTimeComputable hg.toTimeComputable poly := hf.poly + hg.poly.comp (1 + X + hf.poly) bounds n := by - simp only [TimeComputable.comp, eval_add, eval_comp, eval_X, eval_one] + simp only [TimeComputable.comp, TimeComputable.toMonotone, eval_add, eval_comp, eval_X, + eval_one] apply add_le_add · exact hf.bounds n - · exact (h_mono (add_le_add (by omega) (hf.bounds n))).trans (hg.bounds _) + · calc monotoneEnvelope hg.time_bound (max 1 n + hf.time_bound n) + _ ≤ hg.poly.eval (max 1 n + hf.time_bound n) := + monotoneEnvelope_le_of_le_monotone hg.bounds (poly_eval_nat_mono hg.poly) _ + _ ≤ hg.poly.eval (1 + n + hf.poly.eval n) := + poly_eval_nat_mono hg.poly (add_le_add (by omega) (hf.bounds n)) end PolyTimeComputable From 439ab0b62b2a3b5e2110c8e285bdccf15db93fe8 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Thu, 5 Mar 2026 22:57:32 -0500 Subject: [PATCH 2/2] feat(Computability): add complexity classes P, NP, coNP, PSPACE and reductions Define the fundamental complexity classes using single-tape Turing machines, namespaced under Cslib.Complexity. Classes/Core.lean: shared language-level definitions Decides and Verifies. Classes/Time.lean: P, NP, CoNP, PNeNP, and foundational results P_subset_NP and NP_subset_CoNP_iff. Classes/Space.lean: OutputsWithinSpace, SpaceBoundedComputable, PSPACE, and P_subset_PSPACE (a TM running in time t uses at most t work cells). Reductions.lean: polynomial-time many-one reductions (PolyTimeReduces), NPHard, NPComplete, with reflexivity, transitivity, downward closure under P, and NPHard.p_eq_np. --- Cslib.lean | 2 + Cslib/Computability/Complexity/Classes.lean | 11 ++ .../Complexity/Classes/Core.lean | 50 +++++++ .../Complexity/Classes/Space.lean | 133 ++++++++++++++++++ .../Complexity/Classes/Time.lean | 103 ++++++++++++++ .../Computability/Complexity/Reductions.lean | 125 ++++++++++++++++ 6 files changed, 424 insertions(+) create mode 100644 Cslib/Computability/Complexity/Classes.lean create mode 100644 Cslib/Computability/Complexity/Classes/Core.lean create mode 100644 Cslib/Computability/Complexity/Classes/Space.lean create mode 100644 Cslib/Computability/Complexity/Classes/Time.lean create mode 100644 Cslib/Computability/Complexity/Reductions.lean diff --git a/Cslib.lean b/Cslib.lean index a9d5ffc3..1bcab64d 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -30,6 +30,8 @@ public import Cslib.Computability.Languages.OmegaLanguage public import Cslib.Computability.Languages.OmegaRegularLanguage public import Cslib.Computability.Languages.RegularLanguage public import Cslib.Computability.Machines.SingleTapeTuring.Basic +public import Cslib.Computability.Complexity.Classes +public import Cslib.Computability.Complexity.Reductions public import Cslib.Computability.URM.Basic public import Cslib.Computability.URM.Computable public import Cslib.Computability.URM.Defs diff --git a/Cslib/Computability/Complexity/Classes.lean b/Cslib/Computability/Complexity/Classes.lean new file mode 100644 index 00000000..dea3e412 --- /dev/null +++ b/Cslib/Computability/Complexity/Classes.lean @@ -0,0 +1,11 @@ +/- +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.Complexity.Classes.Core +public import Cslib.Computability.Complexity.Classes.Time +public import Cslib.Computability.Complexity.Classes.Space diff --git a/Cslib/Computability/Complexity/Classes/Core.lean b/Cslib/Computability/Complexity/Classes/Core.lean new file mode 100644 index 00000000..0eb6cae0 --- /dev/null +++ b/Cslib/Computability/Complexity/Classes/Core.lean @@ -0,0 +1,50 @@ +/- +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.SingleTapeTuring.Basic + +@[expose] public section + +/-! +# Complexity Class Core Definitions + +This file contains shared language-level definitions used by both +time and space complexity classes. + +## Main Definitions + +* `Decides f L` — `f` decides language `L` (non-empty output means accept) +* `Verifies verify L p` — `verify` verifies language `L` with polynomial witness bound `p` +-/ + +variable {Symbol : Type} + +namespace Cslib.Complexity + +/-- +A function `f : List Symbol → List Symbol` **decides** a language `L` when +membership in `L` corresponds to `f` producing non-empty output. +-/ +def Decides (f : List Symbol → List Symbol) (L : Set (List Symbol)) : Prop := + ∀ x, x ∈ L ↔ f x ≠ [] + +/-- +A verifier `verify` **verifies** a language `L` with polynomial witness bound `p` when +membership in `L` is equivalent to the existence of a short witness `w` such that +`verify (x ++ w)` produces non-empty output. +-/ +-- TODO: The verifier receives `x ++ w` as a bare concatenation, so it cannot +-- distinguish the input/witness boundary. A more robust formulation would use +-- a two-tape machine with a separate read-only witness tape. +def Verifies (verify : List Symbol → List Symbol) (L : Set (List Symbol)) + (p : Polynomial ℕ) : Prop := + ∀ x, x ∈ L ↔ ∃ w : List Symbol, w.length ≤ p.eval x.length ∧ verify (x ++ w) ≠ [] + +end Cslib.Complexity + +end diff --git a/Cslib/Computability/Complexity/Classes/Space.lean b/Cslib/Computability/Complexity/Classes/Space.lean new file mode 100644 index 00000000..79f5550c --- /dev/null +++ b/Cslib/Computability/Complexity/Classes/Space.lean @@ -0,0 +1,133 @@ +/- +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.Complexity.Classes.Time + +@[expose] public section + +/-! +# Space Complexity Classes + +This file defines space-bounded computation and the complexity class **PSPACE**. + +## Main Definitions + +* `OutputsWithinSpace` — TM outputs on input using at most `s` additional work cells +* `SpaceBoundedComputable f s` — `f` is computable within space `s` +* `PSPACE` — languages decidable in polynomial space + +## Main Results + +* `P_subset_PSPACE` — P ⊆ PSPACE + +## References + +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraB2009] +-/ + +open Turing SingleTapeTM Polynomial Relation + +variable {Symbol : Type} + +namespace Cslib.Complexity + +/-- The work space used by a configuration on input `l`: total tape space +minus the initial input footprint `max 1 l.length`. -/ +def Cfg.work_space_used (tm : SingleTapeTM Symbol) (l : List Symbol) (cfg : tm.Cfg) : ℕ := + SingleTapeTM.Cfg.space_used tm cfg - max 1 l.length + +/-- A TM `tm` **outputs** `l'` on input `l` using at most `s` additional work cells +throughout the computation. This combines the time-based reachability +with a space bound: every configuration along the computation path +uses at most `s` work space beyond the initial input footprint. -/ +def OutputsWithinSpace (tm : SingleTapeTM Symbol) + (l l' : List Symbol) (s : ℕ) : Prop := + ∃ t : ℕ, tm.OutputsWithinTime l l' t ∧ + ∀ cfg : tm.Cfg, + ReflTransGen tm.TransitionRelation (tm.initCfg l) cfg → + Cfg.work_space_used tm l cfg ≤ s + +/-- A function `f` is **space-bounded computable** with space bound `s` +if there exists a TM computing `f` that uses at most `s(|x|)` additional +work cells on input `x`. -/ +structure SpaceBoundedComputable + (f : List Symbol → List Symbol) (s : ℕ → ℕ) where + /-- The underlying Turing machine -/ + tm : SingleTapeTM Symbol + /-- Proof that the machine computes `f` within space `s` -/ + outputsInSpace : ∀ a, + OutputsWithinSpace tm a (f a) (s a.length) + +/-- **PSPACE** is the class of languages decidable by a Turing machine +using polynomial work space. -/ +def PSPACE : Set (Set (List Symbol)) := + { L | ∃ f : List Symbol → List Symbol, + ∃ p : Polynomial ℕ, + Nonempty (SpaceBoundedComputable f (fun n => p.eval n)) ∧ + Decides f L } + +-- TODO: Define L (LOGSPACE) using multi-tape Turing machines with a +-- read-only input tape. The single-tape model allows overwriting input +-- cells, giving O(n) writable space instead of O(log n). + +/-- Any configuration reachable during a halting computation has its space +bounded by the initial space plus the halting time. -/ +private lemma space_bounded_of_time_bounded (tm : SingleTapeTM Symbol) + (l l' : List Symbol) (t : ℕ) + (htime : tm.OutputsWithinTime l l' t) + (cfg : tm.Cfg) + (hreach : ReflTransGen tm.TransitionRelation (tm.initCfg l) cfg) : + Cfg.space_used tm cfg ≤ max 1 l.length + t := by + -- Convert ReflTransGen to RelatesInSteps. + obtain ⟨m, hm⟩ := ReflTransGen.relatesInSteps hreach + -- Extract the halting computation. + obtain ⟨t', ht'_le, ht'⟩ := htime + -- `haltCfg` has no successors. + have hhalt : ∀ cfg', ¬tm.TransitionRelation (tm.haltCfg l') cfg' := + fun cfg' => no_step_from_halt tm _ cfg' rfl + -- By determinism, m ≤ t' ≤ t. + have hm_le := reachable_steps_le_halting_steps tm ht' hhalt hm + -- Space grows by at most 1 per step. + have hspace := RelatesInSteps.apply_le_apply_add hm (Cfg.space_used tm) + fun a b hstep => Cfg.space_used_step a b (Option.mem_def.mp hstep) + rw [Cfg.space_used_initCfg] at hspace + omega + +/-- Any configuration reachable during a halting computation uses at most `t` +work cells beyond the initial input footprint. -/ +private lemma work_space_bounded_of_time_bounded (tm : SingleTapeTM Symbol) + (l l' : List Symbol) (t : ℕ) + (htime : tm.OutputsWithinTime l l' t) + (cfg : tm.Cfg) + (hreach : ReflTransGen tm.TransitionRelation (tm.initCfg l) cfg) : + Cfg.work_space_used tm l cfg ≤ t := by + have htotal := space_bounded_of_time_bounded tm l l' t htime cfg hreach + apply (Nat.sub_le_iff_le_add).2 + simpa [Cfg.work_space_used, Nat.add_comm, Nat.add_left_comm, + Nat.add_assoc] using htotal + +/-- **P ⊆ PSPACE**: every language decidable in polynomial time is also +decidable in polynomial space. + +A TM running in time `t` can use at most `t` additional work cells +beyond the initial input footprint (at most one new cell per step). +So a polynomial time bound gives a polynomial work-space bound. -/ +public theorem P_subset_PSPACE : + P (Symbol := Symbol) ⊆ PSPACE := by + intro L ⟨f, ⟨hf⟩, hDecides⟩ + refine ⟨f, hf.poly, ⟨{ + tm := hf.tm + outputsInSpace := fun a => + ⟨hf.time_bound a.length, hf.outputsFunInTime a, fun cfg hreach => + le_trans + (work_space_bounded_of_time_bounded hf.tm a (f a) (hf.time_bound a.length) + (hf.outputsFunInTime a) cfg hreach) + (hf.bounds a.length)⟩ + }⟩, hDecides⟩ + +end Cslib.Complexity diff --git a/Cslib/Computability/Complexity/Classes/Time.lean b/Cslib/Computability/Complexity/Classes/Time.lean new file mode 100644 index 00000000..b5b4a3ce --- /dev/null +++ b/Cslib/Computability/Complexity/Classes/Time.lean @@ -0,0 +1,103 @@ +/- +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.Complexity.Classes.Core + +@[expose] public section + +/-! +# Time Complexity Classes + +This file defines the fundamental time complexity classes **P**, **NP**, and **coNP** +using single-tape Turing machines, and states the **P ≠ NP** conjecture. + +## Main Definitions + +* `P` — the class **P** of languages decidable in polynomial time +* `NP` — the class **NP** of languages verifiable in polynomial time +* `CoNP` — the class **coNP**, complements of **NP** languages +* `PNeNP` — the proposition **P ≠ NP** + +## Main Results + +* `P_subset_NP` — **P ⊆ NP** +-/ + +open Turing SingleTapeTM + +variable {Symbol : Type} + +namespace Cslib.Complexity + +/-- +**P** is the class of languages decidable by a polynomial-time Turing machine. + +We use `Nonempty (PolyTimeComputable f)` because `PolyTimeComputable` is a structure +(carrying computational data), while set membership requires a `Prop`. +-/ +def P : Set (Set (List Symbol)) := + { L | ∃ f, Nonempty (PolyTimeComputable f) ∧ Decides f L } + +/-- +**NP** is the class of languages for which membership can be verified +in polynomial time given a polynomial-length witness (certificate). +-/ +def NP : Set (Set (List Symbol)) := + { L | ∃ verify p, Nonempty (PolyTimeComputable verify) ∧ Verifies verify L p } + +/-- +**coNP** is the class of languages whose complements are in **NP**. +-/ +def CoNP : Set (Set (List Symbol)) := + { L | Lᶜ ∈ NP } + +/-- +The **P ≠ NP** conjecture states that the complexity classes P and NP are distinct. +This is stated as a `Prop` definition rather than an axiom. +-/ +def PNeNP : Prop := P (Symbol := Symbol) ≠ NP + +end Cslib.Complexity + +end + +open Cslib.Complexity + +namespace Cslib.Complexity + +/-- +**P ⊆ NP**: Every language decidable in polynomial time is also verifiable +in polynomial time. + +*Proof sketch*: Given a polytime decider `f` for `L`, use `f` as a verifier +that ignores the witness. The witness is taken to be empty (`[]`), +and the polynomial witness bound is `0`. +-/ +public theorem P_subset_NP + {Symbol : Type} : + P (Symbol := Symbol) ⊆ NP := by + intro L ⟨f, hf, hDecides⟩ + refine ⟨f, 0, hf, fun x => ?_⟩ + simp only [Polynomial.eval_zero] + constructor + · intro hx + exact ⟨[], Nat.le_refl 0, by rwa [List.append_nil, ← hDecides]⟩ + · rintro ⟨w, hw, hverify⟩ + rw [hDecides] + have : w = [] := List.eq_nil_of_length_eq_zero (Nat.le_zero.mp hw) + rwa [this, List.append_nil] at hverify + +/-- **NP ⊆ coNP ↔ ∀ L ∈ NP, Lᶜ ∈ NP**. This is just the unfolding of +the definitions: coNP is defined as `{L | Lᶜ ∈ NP}`, so `NP ⊆ coNP` +means every NP language has its complement in NP. -/ +public theorem NP_subset_CoNP_iff + {Symbol : Type} : + NP (Symbol := Symbol) ⊆ CoNP ↔ + ∀ L ∈ NP (Symbol := Symbol), Lᶜ ∈ NP := by rfl + +end Cslib.Complexity diff --git a/Cslib/Computability/Complexity/Reductions.lean b/Cslib/Computability/Complexity/Reductions.lean new file mode 100644 index 00000000..f6ff9dc1 --- /dev/null +++ b/Cslib/Computability/Complexity/Reductions.lean @@ -0,0 +1,125 @@ +/- +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.Complexity.Classes.Time + +@[expose] public section + +/-! +# Polynomial-Time Reductions and NP-Completeness + +This file defines polynomial-time many-one reductions between languages, +and uses them to define NP-hardness and NP-completeness. + +## Main Definitions + +* `PolyTimeReduces L₁ L₂` — `L₁` poly-time reduces to `L₂` +* `NPHard L` — every NP language poly-time reduces to `L` +* `NPComplete L` — `L` is NP-hard and in NP + +## Main Results + +* `PolyTimeReduces.refl` — reflexivity +* `PolyTimeReduces.trans` — transitivity +* `PolyTimeReduces.mem_P` — downward closure under P +* `NPHard.p_eq_np` — if any NP-hard language is in P then P = NP + +## References + +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraB2009] +-/ + +open Turing SingleTapeTM + +variable {Symbol : Type} + +namespace Cslib.Complexity + +/-- +A language `L₁` **polynomial-time reduces** to `L₂` if there exists a +polynomial-time computable function `f` such that +for all `x`, `x ∈ L₁ ↔ f x ∈ L₂`. + +This is also called a **many-one** or **Karp** reduction. +-/ +def PolyTimeReduces (L₁ L₂ : Set (List Symbol)) : Prop := + ∃ f, Nonempty (PolyTimeComputable f) ∧ ∀ x, x ∈ L₁ ↔ f x ∈ L₂ + +/-- +A language `L` is **NP-hard** if every language in NP polynomial-time +reduces to `L`. +-/ +def NPHard (L : Set (List Symbol)) : Prop := + ∀ L' ∈ NP (Symbol := Symbol), PolyTimeReduces L' L + +/-- +A language `L` is **NP-complete** if it is NP-hard and in NP. +-/ +def NPComplete (L : Set (List Symbol)) : Prop := + NPHard L ∧ L ∈ NP + +end Cslib.Complexity + +end + +open Turing SingleTapeTM Cslib.Complexity + +variable {Symbol : Type} + +namespace Cslib.Complexity + +/-- `≤ₚ` is reflexive: every language reduces to itself via the identity. -/ +theorem PolyTimeReduces.refl + [Inhabited Symbol] + [Finite Symbol] + (L : Set (List Symbol)) : PolyTimeReduces L L := + let _ : Fintype Symbol := Fintype.ofFinite Symbol + ⟨id, ⟨PolyTimeComputable.id⟩, fun _ => Iff.rfl⟩ + +/-- `≤ₚ` is transitive: if `L₁ ≤ₚ L₂` and `L₂ ≤ₚ L₃` then `L₁ ≤ₚ L₃`. -/ +theorem PolyTimeReduces.trans + {L₁ L₂ L₃ : Set (List Symbol)} + (h₁₂ : PolyTimeReduces L₁ L₂) + (h₂₃ : PolyTimeReduces L₂ L₃) : + PolyTimeReduces L₁ L₃ := by + obtain ⟨f, ⟨hf⟩, hf_mem⟩ := h₁₂ + obtain ⟨g, ⟨hg⟩, hg_mem⟩ := h₂₃ + let _ : Inhabited Symbol := hf.toTimeComputable.tm.SymbolInhabited + let _ : Fintype Symbol := hf.toTimeComputable.tm.SymbolFintype + exact ⟨g ∘ f, ⟨hf.comp hg⟩, + fun x => (hf_mem x).trans (hg_mem (f x))⟩ + +/-- If `L₁ ≤ₚ L₂` and `L₂ ∈ P` then `L₁ ∈ P`. -/ +theorem PolyTimeReduces.mem_P + {L₁ L₂ : Set (List Symbol)} + (hred : PolyTimeReduces L₁ L₂) + (hL₂ : L₂ ∈ P (Symbol := Symbol)) : + L₁ ∈ P := by + obtain ⟨f, ⟨hf⟩, hf_mem⟩ := hred + obtain ⟨g, ⟨hg⟩, hg_dec⟩ := hL₂ + let _ : Inhabited Symbol := hf.toTimeComputable.tm.SymbolInhabited + let _ : Fintype Symbol := hf.toTimeComputable.tm.SymbolFintype + refine ⟨g ∘ f, ⟨hf.comp hg⟩, fun x => ?_⟩ + simp only [Function.comp] + exact (hf_mem x).trans (hg_dec (f x)) + +/-- If any NP-hard language is in P, then P = NP. + +This is the fundamental theorem connecting NP-completeness to the +P vs NP question. -/ +theorem NPHard.p_eq_np + {L : Set (List Symbol)} + (hL : NPHard L) + (hP : L ∈ P (Symbol := Symbol)) : + P (Symbol := Symbol) = NP := by + apply Set.eq_of_subset_of_subset + · exact P_subset_NP + · intro L' hL' + exact (hL L' hL').mem_P hP + +end Cslib.Complexity