Documentation

CslibFrontier.Computability.Complexity.Classes.SharpP

The counting classes #P and GapP #

#P is defined through polynomial-time verifiers, like NP (Cslib.Complexity.NP) Valiant, Arora and Barak, Chapter 17: f ∈ SharpP enc when there are a polynomial p and a function V : α × List Bool → Bool, computable in polynomial time on inputs encPair enc encBits (a, w) = frame (enc a) ++ w, such that f a is the number of strings w of length p (enc a).length with V (a, w) = true, the count Cslib.Complexity.acceptCount of CslibFrontier.Computability.Complexity.AcceptCount. The problems in NP are exactly the sets where functions in #P are nonzero (mem_NP_iff_exists_SharpP).

GapP consists of the differences of two functions in #P. Fenner, Fortnow and Kurtz define it through the differences between the numbers of accepting and rejecting paths of nondeterministic machines, and show that this gives the differences of functions in #P Fenner, Fortnow and Kurtz; here that characterisation is the definition. Classes.SharpP.Machine proves that both polynomial-clock terminal counts of a fixed finite-control list-choice machine are in #P, and their difference is in GapP. Classes.SharpP.Characterization supplies the actual reverse verifier construction and the bidirectional #P machine characterization. Classes.SharpP.GapMachine supplies balanced signed routing and the corresponding bidirectional GapP characterization.

Main definitions #

Main results #

References #

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

The functions counting the certificates that a polynomial-time verifier accepts, with certificates of polynomial length, with respect to the encoding enc of instances.

Instances For
    source
    def Cslib.Complexity.GapP {α : Type} (enc : α ↪ List Bool) :
    Set (α → ℤ)

    The differences of two functions in #P, with respect to the encoding enc of instances.

    Instances For
      source
      theorem Cslib.Complexity.mem_SharpP {α : Type} {enc : α ↪ List Bool} {f : α → ℕ} :
      f ∈ SharpP enc ↔ ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool ∧ ∀ (a : α), f a = acceptCount V a (Polynomial.eval (enc a).length p)
      source
      theorem Cslib.Complexity.mem_GapP {α : Type} {enc : α ↪ List Bool} {g : α → ℤ} :
      g ∈ GapP enc ↔ ∃ f₁ ∈ SharpP enc, ∃ f₂ ∈ SharpP enc, ∀ (a : α), g a = ↑(f₁ a) - ↑(f₂ a)
      source
      theorem Cslib.Complexity.mem_NP_iff_exists_SharpP {α : Type} {enc : α ↪ List Bool} {A : Set α} :
      A ∈ NP enc ↔ ∃ f ∈ SharpP enc, ∀ (a : α), a ∈ A ↔ 0 < f a

      NP consists of the supports of functions in #P: a problem is in NP exactly when it is the set of instances where some function in #P is nonzero.

      source
      theorem Cslib.Complexity.SharpP.zero_mem {α : Type} {enc : α ↪ List Bool} :
      0 ∈ SharpP enc

      The zero function is in #P: no certificate is accepted.

      source
      theorem Cslib.Complexity.SharpP.exists_le_two_pow {α : Type} {enc : α ↪ List Bool} {f : α → ℕ} (hf : f ∈ SharpP enc) :
      ∃ (p : Polynomial ℕ), ∀ (a : α), f a ≤ 2 ^ Polynomial.eval (enc a).length p

      A function in #P is at most exponential in the length of the encoded instance.

      source
      theorem Cslib.Complexity.GapP.exists_abs_le_two_pow {α : Type} {enc : α ↪ List Bool} {g : α → ℤ} (hg : g ∈ GapP enc) :
      ∃ (p : Polynomial ℕ), ∀ (a : α), |g a| ≤ 2 ^ Polynomial.eval (enc a).length p

      Every function in GapP is bounded in absolute value by 2 ^ p(|x|) for a polynomial p.

      source
      theorem Cslib.Complexity.GapP.natCast_sub_natCast_mem {α : Type} {enc : α ↪ List Bool} {f₁ f₂ : α → ℕ} (hf₁ : f₁ ∈ SharpP enc) (hf₂ : f₂ ∈ SharpP enc) :
      (fun (a : α) => ↑(f₁ a) - ↑(f₂ a)) ∈ GapP enc

      The difference of two functions in #P, cast to the integers, is in GapP.

      source
      theorem Cslib.Complexity.GapP.neg_mem {α : Type} {enc : α ↪ List Bool} {g : α → ℤ} (hg : g ∈ GapP enc) :
      -g ∈ GapP enc

      GapP is closed under negation: exchange the two functions in #P.