From de2fcd2680634f477768f313a611ae3af4eedf59 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 22:46:20 -0400 Subject: [PATCH] refactor(machines): lower the admissible-map reduction kernel --- Complexity.lean | 1 + .../Complexity/Reduction/ManyOne.lean | 74 ++---------- .../Turing/MultiTape/Halting/Reduction.lean | 2 +- .../Computability/Reduction/ManyOne.lean | 112 ++++++++++++++++++ ComplexityTests.lean | 1 + ComplexityTests/ManyOneKernel.lean | 31 +++++ 6 files changed, 153 insertions(+), 68 deletions(-) create mode 100644 Complexity/Computability/Reduction/ManyOne.lean create mode 100644 ComplexityTests/ManyOneKernel.lean diff --git a/Complexity.lean b/Complexity.lean index 9f02a54dd4..cbb542a786 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1239,6 +1239,7 @@ public import Complexity.Computability.RAM.Cost public import Complexity.Computability.RAM.Defs public import Complexity.Computability.RAM.Input public import Complexity.Computability.RAM.Squaring +public import Complexity.Computability.Reduction.ManyOne public import Complexity.Computability.TreeEval.Ary.Basic public import Complexity.Computability.TreeEval.Ary.CookMertz public import Complexity.Computability.TreeEval.Basic diff --git a/Complexity/Computability/Complexity/Reduction/ManyOne.lean b/Complexity/Computability/Complexity/Reduction/ManyOne.lean index acb75a25c2..1a34f298f0 100644 --- a/Complexity/Computability/Complexity/Reduction/ManyOne.lean +++ b/Complexity/Computability/Complexity/Reduction/ManyOne.lean @@ -7,8 +7,7 @@ Authors: Samuel Schlesinger module -- upstream: candidate -public import Complexity.Init -public import Mathlib.Data.Set.Operations +public import Complexity.Computability.Reduction.ManyOne public import Mathlib.Logic.Embedding.Basic import Mathlib.Order.BooleanAlgebra.Set @@ -19,7 +18,9 @@ Most reductions of complexity theory have one shape: a map `f` of an admissible instances of `A` to instances of `B`, preserving membership. Here the admissible maps are an arbitrary predicate `Good` on functions, and `ManyOneReducibleBy Good A B` says that such a map exists. Polynomial-time and logarithmic-space reductions of encoded problems, and first-order -reductions of ordered queries, are instances. +reductions of ordered queries, are instances. The map-parametric kernel and its laws live in +`Complexity.Computability.Reduction.ManyOne`, publicly re-exported here; only class-level helpers +are defined in this module. Reflexivity and transitivity are not assumed: they follow from closure of the admissible maps under the identity and composition (`ManyOneReducibleBy.refl`, `ManyOneReducibleBy.trans`), which @@ -72,70 +73,9 @@ on `Primcodable` types, the instance of this shape for computable maps; it is no namespace Cslib.Complexity -universe u v w x - -variable {α : Type u} {β : Type v} {γ : Type w} - -/-- `A` many-one reduces to `B` by an admissible map: some `f` satisfying `Good` has -`a ∈ A ↔ f a ∈ B` for every `a`. -/ -def ManyOneReducibleBy (Good : (α → β) → Prop) (A : Set α) (B : Set β) : Prop := - ∃ f : α → β, Good f ∧ ∀ a, a ∈ A ↔ f a ∈ B - -variable {Good : (α → β) → Prop} {A : Set α} {B : Set β} - -namespace ManyOneReducibleBy - -/-- Every problem reduces to itself when the identity is admissible. -/ -theorem refl {Good : (α → α) → Prop} (hid : Good id) (A : Set α) : ManyOneReducibleBy Good A A := - ⟨id, hid, fun _ => Iff.rfl⟩ - -/-- Reductions compose when composites of admissible maps are admissible. The three classes of -maps may differ, as they do when admissibility depends on encodings. -/ -theorem trans {Good₁ : (α → β) → Prop} {Good₂ : (β → γ) → Prop} {Good₃ : (α → γ) → Prop} - {C : Set γ} (hcomp : ∀ f g, Good₁ f → Good₂ g → Good₃ (g ∘ f)) - (hAB : ManyOneReducibleBy Good₁ A B) (hBC : ManyOneReducibleBy Good₂ B C) : - ManyOneReducibleBy Good₃ A C := - let ⟨f, hf, hfAB⟩ := hAB - let ⟨g, hg, hgBC⟩ := hBC - ⟨g ∘ f, hcomp f g hf hg, fun a => (hfAB a).trans (hgBC (f a))⟩ - -/-- More admissible maps give more reductions. -/ -theorem mono {Good' : (α → β) → Prop} (hle : ∀ f, Good f → Good' f) - (h : ManyOneReducibleBy Good A B) : ManyOneReducibleBy Good' A B := - let ⟨f, hf, hAB⟩ := h - ⟨f, hle f hf, hAB⟩ - -/-- A reduction from `A` to `B` is also a reduction from `Aᶜ` to `Bᶜ`. -/ -theorem compl (h : ManyOneReducibleBy Good A B) : ManyOneReducibleBy Good Aᶜ Bᶜ := - let ⟨f, hf, hAB⟩ := h - ⟨f, hf, fun a => not_congr (hAB a)⟩ - -/-- If reductions preserve membership from `D` to `C`, they also preserve membership in the -complement classes `{B | Bᶜ ∈ D}` and `{A | Aᶜ ∈ C}`. -/ -theorem mem_compl {C : Set (Set α)} {D : Set (Set β)} - (hCD : ∀ {A : Set α} {B : Set β}, ManyOneReducibleBy Good A B → B ∈ D → A ∈ C) - (h : ManyOneReducibleBy Good A B) (hB : Bᶜ ∈ D) : Aᶜ ∈ C := - hCD h.compl hB - -/-- **Transfer along partial decodings.** Suppose representations `α'` and `β'` partially decode -to `α` and `β`, and every admissible map `f` is simulated by an admissible map `F` of -representations, in that `F` decodes to `f` on decodable inputs and to nothing elsewhere. Then a -reduction of `A` to `B` gives one of the representations of members of `A` to those of members of -`B`. -/ -theorem lift {α' : Type w} {β' : Type x} {Good' : (α' → β') → Prop} - (dec : α' → Option α) (dec' : β' → Option β) - (hsim : ∀ f, Good f → ∃ F, Good' F ∧ ∀ y, dec' (F y) = (dec y).map f) - (h : ManyOneReducibleBy Good A B) : - ManyOneReducibleBy Good' {y | ∃ a ∈ A, dec y = some a} {z | ∃ b ∈ B, dec' z = some b} := by - obtain ⟨f, hf, hAB⟩ := h - obtain ⟨F, hF, hFf⟩ := hsim f hf - refine ⟨F, hF, fun y => ?_⟩ - simp only [Set.mem_ofPred_eq, hFf] - cases dec y with - | none => simp - | some a => simpa using hAB a - -end ManyOneReducibleBy +universe u v w + +variable {α : Type u} {β : Type v} {A : Set α} {B : Set β} /-! ### Complement-class helpers -/ diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Halting/Reduction.lean b/Complexity/Computability/Machines/Turing/MultiTape/Halting/Reduction.lean index dd508fee7d..9a1a437c89 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Halting/Reduction.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Halting/Reduction.lean @@ -7,7 +7,7 @@ Authors: Samuel Schlesinger module -- upstream: candidate -public import Complexity.Computability.Complexity.Reduction.ManyOne +public import Complexity.Computability.Reduction.ManyOne public import Complexity.Computability.Machines.Turing.MultiTape.Halting.Computable /-! diff --git a/Complexity/Computability/Reduction/ManyOne.lean b/Complexity/Computability/Reduction/ManyOne.lean new file mode 100644 index 0000000000..c07cfd2cf9 --- /dev/null +++ b/Complexity/Computability/Reduction/ManyOne.lean @@ -0,0 +1,112 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Mathlib.Data.Set.Operations + +/-! +# Many-one reductions by admissible maps + +`Cslib.Complexity.ManyOneReducibleBy Good A B` asks for a membership-preserving map from `A` to +`B` satisfying an arbitrary predicate `Good`. No machine model, encoding, complexity class, or +closure assumption is built into the definition. The namespace is retained for existing clients. +Polynomial-time, logarithmic-space and computable mapping reductions instantiate this kernel. + +Mathlib's `ManyOneReducible` is specialized to computable maps on `Primcodable` types; it does +not replace this map-parametric notion. + +## Main definitions + +* `Cslib.Complexity.ManyOneReducibleBy`: many-one reducibility by admissible maps. + +## Main results + +* `Cslib.Complexity.ManyOneReducibleBy.refl`, `Cslib.Complexity.ManyOneReducibleBy.trans`: + reflexivity and transitivity from identity and composition closure. +* `Cslib.Complexity.ManyOneReducibleBy.mono`: enlarging the admissible maps preserves reductions. +* `Cslib.Complexity.ManyOneReducibleBy.compl`, `Cslib.Complexity.ManyOneReducibleBy.mem_compl`: + complement reductions and transfer to complement classes. +* `Cslib.Complexity.ManyOneReducibleBy.lift`: transfer along partial decodings. + +## References + +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09], + Definition 2.7. +-/ + +@[expose] public section + +namespace Cslib.Complexity + +universe u v w x + +variable {α : Type u} {β : Type v} {γ : Type w} + +/-- `A` many-one reduces to `B` by an admissible map: some `f` satisfying `Good` has +`a ∈ A ↔ f a ∈ B` for every `a`. -/ +def ManyOneReducibleBy (Good : (α → β) → Prop) (A : Set α) (B : Set β) : Prop := + ∃ f : α → β, Good f ∧ ∀ a, a ∈ A ↔ f a ∈ B + +variable {Good : (α → β) → Prop} {A : Set α} {B : Set β} + +namespace ManyOneReducibleBy + +/-- Every problem reduces to itself when the identity is admissible. -/ +theorem refl {Good : (α → α) → Prop} (hid : Good id) (A : Set α) : ManyOneReducibleBy Good A A := + ⟨id, hid, fun _ => Iff.rfl⟩ + +/-- Reductions compose when composites of admissible maps are admissible. The three classes of +maps may differ, as they do when admissibility depends on encodings. -/ +theorem trans {Good₁ : (α → β) → Prop} {Good₂ : (β → γ) → Prop} {Good₃ : (α → γ) → Prop} + {C : Set γ} (hcomp : ∀ f g, Good₁ f → Good₂ g → Good₃ (g ∘ f)) + (hAB : ManyOneReducibleBy Good₁ A B) (hBC : ManyOneReducibleBy Good₂ B C) : + ManyOneReducibleBy Good₃ A C := + let ⟨f, hf, hfAB⟩ := hAB + let ⟨g, hg, hgBC⟩ := hBC + ⟨g ∘ f, hcomp f g hf hg, fun a => (hfAB a).trans (hgBC (f a))⟩ + +/-- More admissible maps give more reductions. -/ +theorem mono {Good' : (α → β) → Prop} (hle : ∀ f, Good f → Good' f) + (h : ManyOneReducibleBy Good A B) : ManyOneReducibleBy Good' A B := + let ⟨f, hf, hAB⟩ := h + ⟨f, hle f hf, hAB⟩ + +/-- A reduction from `A` to `B` is also a reduction from `Aᶜ` to `Bᶜ`. -/ +theorem compl (h : ManyOneReducibleBy Good A B) : ManyOneReducibleBy Good Aᶜ Bᶜ := + let ⟨f, hf, hAB⟩ := h + ⟨f, hf, fun a => not_congr (hAB a)⟩ + +/-- If reductions preserve membership from `D` to `C`, they also preserve membership in the +complement classes `{B | Bᶜ ∈ D}` and `{A | Aᶜ ∈ C}`. -/ +theorem mem_compl {C : Set (Set α)} {D : Set (Set β)} + (hCD : ∀ {A : Set α} {B : Set β}, ManyOneReducibleBy Good A B → B ∈ D → A ∈ C) + (h : ManyOneReducibleBy Good A B) (hB : Bᶜ ∈ D) : Aᶜ ∈ C := + hCD h.compl hB + +/-- **Transfer along partial decodings.** Suppose representations `α'` and `β'` partially decode +to `α` and `β`, and every admissible map `f` is simulated by an admissible map `F` of +representations, in that `F` decodes to `f` on decodable inputs and to nothing elsewhere. Then a +reduction of `A` to `B` gives one of the representations of members of `A` to those of members of +`B`. -/ +theorem lift {α' : Type w} {β' : Type x} {Good' : (α' → β') → Prop} + (dec : α' → Option α) (dec' : β' → Option β) + (hsim : ∀ f, Good f → ∃ F, Good' F ∧ ∀ y, dec' (F y) = (dec y).map f) + (h : ManyOneReducibleBy Good A B) : + ManyOneReducibleBy Good' {y | ∃ a ∈ A, dec y = some a} {z | ∃ b ∈ B, dec' z = some b} := by + obtain ⟨f, hf, hAB⟩ := h + obtain ⟨F, hF, hFf⟩ := hsim f hf + refine ⟨F, hF, fun y => ?_⟩ + simp only [Set.mem_ofPred_eq, hFf] + cases dec y with + | none => simp + | some a => simpa using hAB a + +end ManyOneReducibleBy + +end Cslib.Complexity diff --git a/ComplexityTests.lean b/ComplexityTests.lean index 6026c26181..4d19e39f6f 100644 --- a/ComplexityTests.lean +++ b/ComplexityTests.lean @@ -231,6 +231,7 @@ import ComplexityTests.MachinePrograms import ComplexityTests.MachineSequential import ComplexityTests.MachineStateMap import ComplexityTests.ManyOne +import ComplexityTests.ManyOneKernel import ComplexityTests.MassProduction import ComplexityTests.MassProduction.Fine import ComplexityTests.MassProduction.HighRate diff --git a/ComplexityTests/ManyOneKernel.lean b/ComplexityTests/ManyOneKernel.lean new file mode 100644 index 0000000000..55b1ce5cfa --- /dev/null +++ b/ComplexityTests/ManyOneKernel.lean @@ -0,0 +1,31 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.Reduction.ManyOne + +/-! The admissible-map API works without importing machines or complexity classes. -/ + +namespace ComplexityTests.ManyOneKernel + +open Cslib.Complexity + +private theorem flip : ManyOneReducibleBy (fun _ => True) + {b : Bool | b = false} {b : Bool | b = true} := + ⟨Bool.not, trivial, fun b => by cases b <;> simp⟩ + +-- Complementing and then composing the flip gives a reduction of a proper, inhabited set to +-- itself. This uses only the lower import, retaining the existing public names. +example : ManyOneReducibleBy (fun _ => True) {b : Bool | b = false} {b : Bool | b = false} := by + have back : ManyOneReducibleBy (fun _ => True) + {b : Bool | b = true} {b : Bool | b = false} := by + have hfalse : ({b : Bool | b = false}ᶜ : Set Bool) = {b : Bool | b = true} := by + ext b; cases b <;> simp + have htrue : ({b : Bool | b = true}ᶜ : Set Bool) = {b : Bool | b = false} := by + ext b; cases b <;> simp + simpa only [hfalse, htrue] using flip.compl + exact flip.trans (fun _ _ _ _ => trivial) back + +end ComplexityTests.ManyOneKernel