Documentation

CslibFrontier.Computability.Complexity.Classes.SharpP.Completeness

Parsimonious reductions and #P-completeness #

A parsimonious reduction from a counting function f : α → ℕ to g : β → ℕ is a function r : α → β, computable in polynomial time, that preserves counts exactly: f a = g (r a) for every instance a Valiant, Arora and Barak, Section 17.3. A counting function is #P-hard when every function in #P, with any encoding of its instances, reduces to it parsimoniously, and #P-complete when it also belongs to #P.

Parsimonious reductions compose (ParsimoniousReducible.trans) and #P is closed under them (ParsimoniousReducible.mem_SharpP, from exact-count precomposition SharpP.comp_mem).

Main definitions #

Main results #

References #

source
def Cslib.Complexity.ParsimoniousReducible {α β : Type} (encA : α ↪ List Bool) (encB : β ↪ List Bool) (f : α → ℕ) (g : β → ℕ) :
Prop

f reduces parsimoniously to g: some r, computable in polynomial time with respect to encA and encB, satisfies f a = g (r a) for every a.

Instances For
    source
    def Cslib.Complexity.SharpPHard {β : Type} (encB : β ↪ List Bool) (g : β → ℕ) :
    Prop

    Every function in #P, with any encoding of its instances, reduces parsimoniously to g. This is HardUnder for ParsimoniousReducible.

    Instances For
      source
      def Cslib.Complexity.SharpPComplete {β : Type} (encB : β ↪ List Bool) (g : β → ℕ) :
      Prop

      g is in #P and every function in #P reduces parsimoniously to it. This is CompleteUnder for ParsimoniousReducible (sharpPComplete_iff_completeUnder), with its second conjunct stated as SharpPHard.

      Instances For
        source
        theorem Cslib.Complexity.sharpPHard_iff_hardUnder {β : Type} {encB : β ↪ List Bool} {g : β → ℕ} :
        SharpPHard encB g ↔ HardUnder (fun {α : Type} (enc : α ↪ List Bool) => ParsimoniousReducible enc encB) (@SharpP) g

        #P-hardness is hardness for #P under ParsimoniousReducible.

        source
        theorem Cslib.Complexity.sharpPComplete_iff_completeUnder {β : Type} {encB : β ↪ List Bool} {g : β → ℕ} :
        SharpPComplete encB g ↔ CompleteUnder (fun {α : Type} (enc : α ↪ List Bool) => ParsimoniousReducible enc encB) (@SharpP) encB g

        #P-completeness is completeness for #P under ParsimoniousReducible.

        source
        theorem Cslib.Complexity.ParsimoniousReducible.refl {α : Type} (encA : α ↪ List Bool) (f : α → ℕ) :
        ParsimoniousReducible encA encA f f

        Every counting function reduces parsimoniously to itself by the identity function.

        source
        theorem Cslib.Complexity.ParsimoniousReducible.trans {α β γ : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {f : α → ℕ} {g : β → ℕ} {h : γ → ℕ} (hfg : ParsimoniousReducible encA encB f g) (hgh : ParsimoniousReducible encB encC g h) :
        ParsimoniousReducible encA encC f h

        Parsimonious reductions compose.

        source
        theorem Cslib.Complexity.ParsimoniousReducible.mem_SharpP {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {f : α → ℕ} {g : β → ℕ} (hfg : ParsimoniousReducible encA encB f g) (hg : g ∈ SharpP encB) :
        f ∈ SharpP encA

        #P is closed under parsimonious reductions.

        source
        theorem Cslib.Complexity.SharpPHard.trans {β γ : Type} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {g : β → ℕ} {h : γ → ℕ} (hg : SharpPHard encB g) (hgh : ParsimoniousReducible encB encC g h) :
        SharpPHard encC h

        #P-hardness transfers along a parsimonious reduction.