The class PP

PP is defined like BPP (Cslib.Complexity.BPP), through deterministic polynomial-time machines that read a random string, but with unbounded error Gill: A ∈ PP enc when there are a polynomial p and a function V : α × List Bool → Bool, computable in polynomial time on inputs encPair enc encBits (a, r) = frame (enc a) ++ r, such that a ∈ A exactly when more than half of the random strings r of length p (enc a).length give V (a, r) = true. The probability is written as a count (Cslib.Complexity.acceptCount), as in BPP and #P, so PP consists of the problems decided by comparing a function in #P with half the number of certificates.

A bounded-error decider accepts the members of its problem with probability at least 2 / 3 and the others with probability at most 1 / 3, so it decides by majority: BPP ⊆ PP with the same verifier (BPP_subset_PP).

Gill requires a strict majority on members, as here; the variant with a non-strict majority defines the same class (Cslib.Complexity.mem_PP_iff_decidesByNonstrictMajority). The characterisation by fair-coin machines deciding by strict majority within polynomial time is Cslib.Complexity.mem_PP_iff_exists_mem_PPTIME, in CslibFrontier.Computability.Complexity.Classes.PP.Time.

Main definitions

• Cslib.Complexity.DecidesByMajority: the majority condition.
• Cslib.Complexity.PP.

Main results

• Cslib.Complexity.PromiseProblem.SolvesWithBoundedError.solvedBy_majority: bounded error gives a strict-majority solver on the promise.
• Cslib.Complexity.DecidesWithBoundedError.decidesByMajority: bounded error gives a majority.
• Cslib.Complexity.BPP_subset_PP.

References

• J. Gill, Computational complexity of probabilistic Turing machines
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

def Cslib.Complexity.DecidesByMajority {α : Type} (enc : α ↪ List Bool) (p : Polynomial ℕ) (V : α × List Bool → Bool) (A : Set α) : Prop

V decides A by majority, using random strings whose length is p evaluated at the length of the encoded instance: a ∈ A exactly when more than half of the random strings r give V (a, r) = true.

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

The problems decided by majority by polynomial-time machines reading polynomially long random strings, with respect to the encoding enc of instances Gill.

theorem Cslib.Complexity.mem_PP {α : Type} {enc : α ↪ List Bool} {A : Set α} : A ∈ PP enc ↔ ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool ∧ DecidesByMajority enc p V A

theorem Cslib.Complexity.PromiseProblem.SolvesWithBoundedError.solvedBy_majority {α : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {V : α × List Bool → Bool} {Q : PromiseProblem α} (h : SolvesWithBoundedError enc p V Q) : Q.SolvedBy fun (a : α) => decide (2 ^ Polynomial.eval (enc a).length p < 2 * acceptCount V a (Polynomial.eval (enc a).length p))

A bounded-error verifier solves its promise problem by strict majority. Ties reject, and there is no error-margin requirement outside the promise.

theorem Cslib.Complexity.DecidesWithBoundedError.decidesByMajority {α : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {V : α × List Bool → Bool} {A : Set α} (h : DecidesWithBoundedError enc p V A) : DecidesByMajority enc p V A

Bounded error gives a majority: a decider that is right on at least two thirds of the random strings accepts the members of its problem, and only them, on more than half.

theorem Cslib.Complexity.BPP_subset_PP {α : Type} {enc : α ↪ List Bool} : BPP enc ⊆ PP enc

BPP ⊆ PP.