The counting class #P

#P (sharp-P) is the class of functions that count the accepting computation paths of a polynomial-time nondeterministic machine, defined here directly on the existing NTM.acceptCount path semantics (roadmap track L5).

Main definitions and results

• SharpP — the counting class
• NTM.acceptCount_le — a machine has at most 2 ^ T accepting paths among the 2 ^ T length-T choice sequences
• SharpP.le_two_pow — every #P function is bounded by 2 ^ T(|x|) for its polynomial clock T

theorem Complexity.NTM.acceptCount_le {n : ℕ} (N : NTM n) (x : List Bool) (T : ℕ) : N.acceptCount x T ≤ 2 ^ T

The number of accepting choice sequences is at most the total number of choice sequences, 2 ^ T: it is the cardinality of a subset of the 2 ^ T length-T random strings.

def Complexity.SharpP : Set (List Bool → ℕ)

#P (sharp-P): the class of functions f : List Bool → ℕ counting the accepting computation paths of a polynomial-time nondeterministic machine. f ∈ SharpP when some NTM halts on every path within a polynomial time bound T and f x equals its number of accepting length-T(|x|) choice sequences. Mirrors the existential shape of NP, but counts paths (NTM.acceptCount) rather than merely asserting one exists.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.SharpP.le_two_pow {f : List Bool → ℕ} (hf : f ∈ SharpP) : ∃ (T : ℕ → ℕ), (∃ (k : ℕ), BigO T fun (x : ℕ) => x ^ k) ∧ ∀ (x : List Bool), f x ≤ 2 ^ T x.length

Every #P function is bounded by 2 ^ T(|x|) for its polynomial clock T: a witness that #P functions have at-most-exponential values.

def Complexity.GapP : Set (List Bool → ℤ)

GapP: the class of integer-valued functions expressible as the difference of two #P functions (equivalently, accepting minus rejecting paths of a polynomial-time nondeterministic machine).

Equations

• Complexity.GapP = {h : List Bool → ℤ | ∃ (f : List Bool → ℕ) (g : List Bool → ℕ), f ∈ Complexity.SharpP ∧ g ∈ Complexity.SharpP ∧ ∀ (x : List Bool), h x = ↑(f x) - ↑(g x)}

theorem Complexity.GapP.neg_mem {h : List Bool → ℤ} (hh : h ∈ GapP) : (fun (x : List Bool) => -h x) ∈ GapP

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