Threshold languages of #P functions

DefinitionThreshold language of a counting function#✓fully proved

For a function \(f\) from bitstrings to natural numbers, the threshold language of \(f\) is the decision problem that accepts a bitstring \(y\) exactly when decoding \(y\) with the canonical bitstring encoding of pairs of a bitstring and a natural number succeeds and gives a pair \((x, k)\) with \(k \le f(x)\); bitstrings that do not decode are rejected.

noncomputable def thresholdLang (f : List Bool → ℕ) :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun y =>
  match MetaMathlibExt.BitstringEncoding.bitDecode (α := List Bool × ℕ) y with
  | some (x, k) => decide (k ≤ f x)
  | none => false

Uses 9 · Used by 1

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Decision problems

Used byThreshold languages of #P functions are in PSPACE

TheoremThreshold languages of #P functions are in PSPACE#●ready to prove

For every function \(f\) in \(\#P\), the threshold language of \(f\), which accepts a bitstring exactly when it decodes, under the canonical bitstring encoding of pairs, to a pair \((x, k)\) of a bitstring \(x\) and a natural number \(k\) with \(k \le f(x)\), is in PSPACE.

public theorem_wanted sharpP_threshold_pspace :
    ∀ f ∈ SharpP, thresholdLang f ∈ PSPACE

Sources

• L. G. Valiant, "The complexity of enumeration and reliability problems" (1979); S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Theorem 9.3 (#P ⊆ PSPACE in the threshold-language form).

Uses 5

Statement usesPolynomial space for decision problems · The counting class \(\#P\) · Threshold language of a counting function · Complexity classes · Decision problems

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.