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, Definition 2.7.

def Cslib.Complexity.ManyOneReducibleBy {α : Type u} {β : Type v} (Good : (α → β) → Prop) (A : Set α) (B : Set β) : Prop

A many-one reduces to B by an admissible map: some f satisfying Good has a ∈ A ↔ f a ∈ B for every a.

theorem Cslib.Complexity.ManyOneReducibleBy.refl {α : Type u} {Good : (α → α) → Prop} (hid : Good id) (A : Set α) : ManyOneReducibleBy Good A A

Every problem reduces to itself when the identity is admissible.

theorem Cslib.Complexity.ManyOneReducibleBy.trans {α : Type u} {β : Type v} {γ : Type w} {A : Set α} {B : Set β} {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

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 Cslib.Complexity.ManyOneReducibleBy.mono {α : Type u} {β : Type v} {Good : (α → β) → Prop} {A : Set α} {B : Set β} {Good' : (α → β) → Prop} (hle : ∀ (f : α → β), Good f → Good' f) (h : ManyOneReducibleBy Good A B) : ManyOneReducibleBy Good' A B

More admissible maps give more reductions.

theorem Cslib.Complexity.ManyOneReducibleBy.compl {α : Type u} {β : Type v} {Good : (α → β) → Prop} {A : Set α} {B : Set β} (h : ManyOneReducibleBy Good A B) : ManyOneReducibleBy Good Aᶜ Bᶜ

A reduction from A to B is also a reduction from Aᶜ to Bᶜ.

theorem Cslib.Complexity.ManyOneReducibleBy.mem_compl {α : Type u} {β : Type v} {Good : (α → β) → Prop} {A : Set α} {B : Set β} {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

If reductions preserve membership from D to C, they also preserve membership in the complement classes {B | Bᶜ ∈ D} and {A | Aᶜ ∈ C}.

theorem Cslib.Complexity.ManyOneReducibleBy.lift {α : Type u} {β : Type v} {Good : (α → β) → Prop} {A : Set α} {B : Set β} {α' : Type w} {β' : Type x} {Good' : (α' → β') → Prop} (dec : α' → Option α) (dec' : β' → Option β) (hsim : ∀ (f : α → β), Good f → ∃ (F : α' → β'), Good' F ∧ ∀ (y : α'), dec' (F y) = Option.map f (dec y)) (h : ManyOneReducibleBy Good A B) : ManyOneReducibleBy Good' {y : α' | ∃ (a : α), a ∈ A ∧ dec y = some a} {z : β' | ∃ (b : β), b ∈ B ∧ dec' z = some b}

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.