The counting class #P

#P (sharp-P) is the class of functions that count the accepting leaves of a polynomial-time nondeterministic computation tree.

This is deliberately distinct from NTM.acceptCount, which counts fixed-length choice strings for probabilistic semantics. If a machine halts early, all extensions of that random string must retain their multiplicity when computing a probability, but the halted computation is only one leaf of a nondeterministic tree. NTM.acceptLeafCount implements the latter convention and is invariant under extending any clock by which every path has halted.

Main definitions and results

• SharpP — the counting class
• NTM.acceptCount_le — a machine has at most 2 ^ T accepting fixed-clock choice strings among the 2 ^ T length-T strings
• NTM.acceptLeafCount_eq_of_le_of_allPathsHaltIn — accepting-leaf counts do not depend on the choice of a sufficient clock
• SharpP.le_two_pow — every #P function is bounded by 2 ^ T(|x|) for its polynomial clock T

def Complexity.NTM.acceptLeafCountFrom {n : ℕ} (tm : NTM n) : ℕ → Cfg n tm.Q → ℕ

Count accepting leaves in the nondeterministic computation tree rooted at c, truncated after at most T transitions. A halted configuration contributes one leaf, rather than one copy for every unused suffix of the choice string.

Equations

• One or more equations did not get rendered due to their size.
• tm.acceptLeafCountFrom 0 x✝ = if tm.halted x✝ ∧ x✝.output.cells 1 = Complexity.Γ.one then 1 else 0

def Complexity.NTM.acceptLeafCount {n : ℕ} (tm : NTM n) (x : List Bool) (T : ℕ) : ℕ

Number of accepting leaves reached from the initial configuration within T transitions. Unlike acceptCount, this counts an early-halting path once.

Equations

• tm.acceptLeafCount x T = tm.acceptLeafCountFrom T (tm.initCfg x)

theorem Complexity.NTM.acceptLeafCountFrom_le {n : ℕ} (tm : NTM n) (c : Cfg n tm.Q) (T : ℕ) : tm.acceptLeafCountFrom T c ≤ 2 ^ T

An accepting computation tree of height at most T has at most 2 ^ T leaves.

theorem Complexity.NTM.acceptLeafCount_le {n : ℕ} (tm : NTM n) (x : List Bool) (T : ℕ) : tm.acceptLeafCount x T ≤ 2 ^ T

A machine has at most 2 ^ T accepting leaves within T transitions.

theorem Complexity.NTM.acceptLeafCount_eq_of_le_of_allChoicesHalt {n : ℕ} (tm : NTM n) (x : List Bool) {T T' : ℕ} (hle : T ≤ T') (hhalt : ∀ (choices : Fin T → Bool), tm.halted (tm.trace T choices (tm.initCfg x))) : tm.acceptLeafCount x T' = tm.acceptLeafCount x T

Once every path has halted by T, extending the observation clock to any T' ≥ T leaves the accepting-leaf count unchanged.

theorem Complexity.NTM.acceptLeafCount_eq_of_le_of_allPathsHaltIn {n : ℕ} {T T' : ℕ → ℕ} (tm : NTM n) (hle : ∀ (m : ℕ), T m ≤ T' m) (hhalt : tm.AllPathsHaltIn T) (x : List Bool) : tm.acceptLeafCount x (T' x.length) = tm.acceptLeafCount x (T x.length)

A pointwise-larger sufficient clock gives the same accepting-leaf count.

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 leaves 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 accepting-leaf count. Unlike fixed-clock PTM probability, unused choice bits after an early halt do not duplicate a computation leaf.

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. The textbook alternative characterization (accepting minus rejecting paths of a single polynomial-time nondeterministic machine) is not formalized here.

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.