Documentation

CslibFrontier.Computability.Complexity.Classes.SPP

Small-gap polynomial time #

SPP consists of languages whose characteristic function belongs to GapP, following Fenner, Fortnow and Kurtz and Fortnow, Classification 4.4. We use the library's verifier-based counting functions, without claiming a counting-machine characterization. The Boolean closure proofs below are elementary consequences of the GapP ring operations: complement uses 1 - f, intersection f * g, and union De Morgan's law.

Main definitions #

Main results #

References #

source
def Cslib.Complexity.SPP {α : Type} (enc : α ↪ List Bool) :
Set (Set α)

Small-gap polynomial time: a GapP function is one on members and zero on nonmembers Fenner, Fortnow and Kurtz, Fortnow, Classification 4.4.

Instances For
    source
    theorem Cslib.Complexity.mem_SPP {α : Type} {enc : α ↪ List Bool} {A : Set α} :
    A ∈ SPP enc ↔ ∃ f ∈ GapP enc, (∀ (a : α), f a = 0 ∨ f a = 1) ∧ ∀ (a : α), a ∈ A ↔ f a = 1
    source
    theorem Cslib.Complexity.UP_subset_SPP {α : Type} {enc : α ↪ List Bool} :
    UP enc ⊆ SPP enc

    UP ⊆ SPP Fortnow, Corollary 4.11.

    source
    theorem Cslib.Complexity.compl_mem_SPP {α : Type} {enc : α ↪ List Bool} {A : Set α} (hA : A ∈ SPP enc) :
    Aᶜ ∈ SPP enc

    Boolean complement corresponds to subtracting the characteristic function from one.

    source
    theorem Cslib.Complexity.inter_mem_SPP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ SPP enc) (hB : B ∈ SPP enc) :
    A ∩ B ∈ SPP enc

    Intersection multiplies two characteristic functions.

    source
    def Cslib.Complexity.SPP.booleanSubalgebra {α : Type} (enc : α ↪ List Bool) :
    BooleanSubalgebra (Set α)

    SPP as a Boolean subalgebra of Set α.

    Instances For
      source
      @[simp]
      theorem Cslib.Complexity.SPP.coe_booleanSubalgebra {α : Type} {enc : α ↪ List Bool} :
      ↑(booleanSubalgebra enc) = SPP enc
      source
      @[simp]
      theorem Cslib.Complexity.SPP.mem_booleanSubalgebra {α : Type} {enc : α ↪ List Bool} {A : Set α} :
      A ∈ booleanSubalgebra enc ↔ A ∈ SPP enc
      source
      theorem Cslib.Complexity.union_mem_SPP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ SPP enc) (hB : B ∈ SPP enc) :
      A ∪ B ∈ SPP enc

      Union follows from intersection and complement.

      source
      theorem Cslib.Complexity.diff_mem_SPP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ SPP enc) (hB : B ∈ SPP enc) :
      A \ B ∈ SPP enc

      SPP is closed under set difference.

      source
      theorem Cslib.Complexity.symmDiff_mem_SPP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ SPP enc) (hB : B ∈ SPP enc) :
      symmDiff A B ∈ SPP enc

      SPP is closed under symmetric difference.

      source
      theorem Cslib.Complexity.SPP_subset_CeqP {α : Type} {enc : α ↪ List Bool} :
      SPP enc ⊆ CeqP enc

      Subtracting one turns the characteristic function into an exact-zero test.

      source
      theorem Cslib.Complexity.coUP_subset_SPP {α : Type} {enc : α ↪ List Bool} :
      coUP enc ⊆ SPP enc

      Since SPP is closed under complement, coUP is also contained in SPP.

      source
      theorem Cslib.Complexity.SPP_subset_coCeqP {α : Type} {enc : α ↪ List Bool} :
      SPP enc ⊆ coCeqP enc

      SPP is contained in coC=P by complement closure and its C=P containment.

      source
      theorem Cslib.Complexity.PolyTimeReducible.mem_SPP {α : Type} {enc : α ↪ List Bool} {A : Set α} {β : Type} {encB : β ↪ List Bool} {B : Set β} (h : PolyTimeReducible enc encB A B) (hB : B ∈ SPP encB) :
      A ∈ SPP enc

      Polynomial-time many-one reductions preserve the zero-or-one gap.