Documentation

Complexity.Computability.Complexity.Reduction.ManyOne

Many-one reductions by a class of maps #

Most reductions of complexity theory have one shape: a map f of an admissible kind sends the 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. 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 holds for the machine-defined classes but has to be proved separately for others. A change of representation transfers reductions when each admissible map is simulated, through partial decodings, by an admissible map of representations (ManyOneReducibleBy.lift).

A class of problems is given, as elsewhere in the library, by a set of problems for every type of instances and every encoding of them as bit strings. Since admissibility of a map generally depends on the encodings, hardness is stated for a reducibility R enc A B indexed by the encoding enc of the source instances, such as ManyOneReducibleBy (Good enc) A B: B is hard for a class 𝒞 (HardUnder R 𝒞 B) when every problem A in 𝒞, with any encoding enc, has R enc A B, and complete (CompleteUnder R 𝒞 encB B) when it also belongs to 𝒞. Polynomial-time and logspace hardness and completeness are instances, whose unfoldings mention their own named reducibilities.

Mathlib's ManyOneReducible (Mathlib/Computability/Reduce.lean) is the computable reducibility on Primcodable types, the instance of this shape for computable maps; it is not reused here.

Main definitions #

Main results #

References #

Complement-class helpers #

source
theorem Cslib.Complexity.compl_union_mem {α : Type u} {C : Set (Set α)} {A B : Set α} (hinter : ∀ {A B : Set α}, A ∈ C → B ∈ C → A ∩ B ∈ C) (hA : Aᶜ ∈ C) (hB : Bᶜ ∈ C) :
(A ∪ B)ᶜ ∈ C

De Morgan dual: if C is closed under intersection, {A | Aᶜ ∈ C} is closed under union.

source
theorem Cslib.Complexity.compl_inter_mem {α : Type u} {C : Set (Set α)} {A B : Set α} (hunion : ∀ {A B : Set α}, A ∈ C → B ∈ C → A ∪ B ∈ C) (hA : Aᶜ ∈ C) (hB : Bᶜ ∈ C) :
(A ∩ B)ᶜ ∈ C

De Morgan dual: if C is closed under union, {A | Aᶜ ∈ C} is closed under intersection.

source
theorem Cslib.Complexity.forall_mem_compl_iff {α : Type u} {A : Set α} {P Q : α → Prop} (hPQ : ∀ (a : α), ¬P a ↔ Q a) :
(∀ (a : α), a ∈ Aᶜ ↔ P a) ↔ ∀ (a : α), a ∈ A ↔ Q a

Negating the pointwise membership condition characterizes the complement Aᶜ.

source
theorem Cslib.Complexity.exists_forall_mem_compl_iff {α : Type u} {A : Set α} {ι : Type w} {F : Set ι} {P Q : ι → α → Prop} (hPQ : ∀ (f : ι) (a : α), ¬P f a ↔ Q f a) :
(∃ (f : ι), f ∈ F ∧ ∀ (a : α), a ∈ Aᶜ ↔ P f a) ↔ ∃ (f : ι), f ∈ F ∧ ∀ (a : α), a ∈ A ↔ Q f a

Negating the pointwise membership condition in an existential class characterization gives the characterization of the complement class {A | Aᶜ ∈ C}.

Hardness and completeness #

source
def Cslib.Complexity.HardUnder {P : Type → Type u} {Q : Type v} (R : {α : Type} → (α ↪ List Bool) → P α → Q → Prop) (𝒞 : {α : Type} → (α ↪ List Bool) → Set (P α)) (B : Q) :
Prop

B is hard for the class 𝒞 under the reducibility R: every problem in 𝒞, with any encoding enc of its instances, reduces to B, in that R enc A B.

The type of instances is a strict-implicit argument, inferred from enc when a hardness proof is applied. An ordinary implicit argument would be instantiated as soon as a hardness proof is produced, for example by h.trans r, so that its type would no longer be a hardness statement and (h.trans r).trans r' would not elaborate.

Instances For
    source
    def Cslib.Complexity.CompleteUnder {P : Type → Type u} {β : Type} (R : {α : Type} → (α ↪ List Bool) → P α → P β → Prop) (𝒞 : {α : Type} → (α ↪ List Bool) → Set (P α)) (encB : β ↪ List Bool) (B : P β) :
    Prop

    B is complete for the class 𝒞 under the reducibility R: it is in 𝒞, with the encoding encB, and is 𝒞-hard under R.

    Instances For
      source
      theorem Cslib.Complexity.HardUnder.mono {P : Type → Type u} {Q : Type v} {R R' : {α : Type} → (α ↪ List Bool) → P α → Q → Prop} {𝒞 : {α : Type} → (α ↪ List Bool) → Set (P α)} {B : Q} (hR : ∀ {α : Type} (enc : α ↪ List Bool) (A : P α), R enc A B → R' enc A B) (hB : HardUnder R 𝒞 B) :
      HardUnder R' 𝒞 B

      A weaker reducibility preserves hardness.

      source
      theorem Cslib.Complexity.HardUnder.trans {P : Type → Type u} {Q : Type v} {Q' : Type w} {R : {α : Type} → (α ↪ List Bool) → P α → Q → Prop} {R' : {α : Type} → (α ↪ List Bool) → P α → Q' → Prop} {𝒞 : {α : Type} → (α ↪ List Bool) → Set (P α)} {S : Q → Q' → Prop} {B : Q} {C : Q'} (hRS : ∀ {α : Type} (enc : α ↪ List Bool) (A : P α), R enc A B → S B C → R' enc A C) (hB : HardUnder R 𝒞 B) (hBC : S B C) :
      HardUnder R' 𝒞 C

      Hardness transfers along a reduction S B C that composes with R-reductions to B into R'-reductions to C.

      source
      theorem Cslib.Complexity.CompleteUnder.mono {P : Type → Type u} {β : Type} {R R' : {α : Type} → (α ↪ List Bool) → P α → P β → Prop} {𝒞 : {α : Type} → (α ↪ List Bool) → Set (P α)} {encB : β ↪ List Bool} {B : P β} (hR : ∀ {α : Type} (enc : α ↪ List Bool) (A : P α), R enc A B → R' enc A B) (hB : CompleteUnder R 𝒞 encB B) :
      CompleteUnder R' 𝒞 encB B

      A weaker reducibility preserves completeness.

      source
      theorem Cslib.Complexity.HardUnder.compl {β : Type v} {B : Set β} {R : {α : Type} → (α ↪ List Bool) → Set α → Set β → Prop} {𝒞 𝒟 : {α : Type} → (α ↪ List Bool) → Set (Set α)} (hR : ∀ {α : Type} (enc : α ↪ List Bool) (A : Set α), R enc A B → R enc Aᶜ Bᶜ) (h𝒟𝒞 : ∀ {α : Type} (enc : α ↪ List Bool) (A : Set α), A ∈ 𝒟 enc → Aᶜ ∈ 𝒞 enc) (hB : HardUnder R 𝒞 B) :
      HardUnder R 𝒟 Bᶜ

      If R relates complements and the complement of every problem in 𝒟 is in 𝒞, the complement of a 𝒞-hard problem is 𝒟-hard.

      source
      theorem Cslib.Complexity.CompleteUnder.compl {𝒞 𝒟 : {α : Type} → (α ↪ List Bool) → Set (Set α)} {β : Type} {R : {α : Type} → (α ↪ List Bool) → Set α → Set β → Prop} {encB : β ↪ List Bool} {B : Set β} (hR : ∀ {α : Type} (enc : α ↪ List Bool) (A : Set α), R enc A B → R enc Aᶜ Bᶜ) (h𝒟𝒞 : ∀ {α : Type} (enc : α ↪ List Bool) (A : Set α), A ∈ 𝒟 enc ↔ Aᶜ ∈ 𝒞 enc) (hB : CompleteUnder R 𝒞 encB B) :
      CompleteUnder R 𝒟 encB Bᶜ

      If R relates complements and the problems in 𝒟 are exactly the complements of the problems in 𝒞, the complement of a 𝒞-complete problem is 𝒟-complete.