Characterisations and closure properties of PP

PP (Cslib.Complexity.PP) is defined by a strict majority of accepted random strings Gill. This file proves that a non-strict majority defines the same class, that PP is closed under polynomial-time reductions, and the characterisations of PP through #P and GapP Fenner, Fortnow and Kurtz.

• Non-strict majority. A verifier decides A by strict majority exactly when its negation decides the complement Aᶜ by non-strict majority (Cslib.Complexity.decidesByMajority_iff_decidesByNonstrictMajority_compl). Since PP is closed under complement (Cslib.Complexity.compl_mem_PP), the two majority conditions give the same class (Cslib.Complexity.mem_PP_iff_decidesByNonstrictMajority).
• Reductions. For a reduction f from A to B and a verifier W for B reading q(m) random bits on an instance of length m, the verifier for A runs W on f a and the first q (|f a|) random bits. Since |f a| is polynomial in |a|, the random string is padded to a polynomial r(|a|); the ignored bits multiply the counts on both sides of the majority condition by the same power of two.
• #P. A ∈ PP exactly when a ∈ A ↔ 2 ^ q(n) < 2 f(a) for some f ∈ #P and some polynomial q, not necessarily the length of the certificates counted by f, where n is the length of the encoded instance (Cslib.Complexity.mem_PP_iff_exists_SharpP). For f counting the certificates of length k = p(n) that V accepts and j = q(n), the verifier on random strings of length k + j + 2 lets the first bit choose: on true it accepts the 2 f(a) strings formed by a certificate accepted by V, a free bit, and j bits false; on false it accepts the 2 ^ (k + j + 1) - 2 ^ j strings whose first k + 1 bits are not all false. More than half of the strings are accepted exactly when 2 ^ j < 2 f(a).
• GapP. A ∈ PP exactly when A = {a | 0 < g a} for some g ∈ GapP (Cslib.Complexity.mem_PP_iff_exists_GapP).

Main definitions

• Cslib.Complexity.DecidesByNonstrictMajority: the non-strict majority condition.

Main results

• Cslib.Complexity.mem_PP_iff_decidesByNonstrictMajority: non-strict majority defines PP.
• Cslib.Complexity.PolyTimeReducible.mem_PP: PP is closed under polynomial-time reductions.
• Cslib.Complexity.mem_PP_iff_exists_SharpP, Cslib.Complexity.mem_PP_iff_exists_GapP.

References

• J. Gill, Computational complexity of probabilistic Turing machines
• S. Fenner, L. Fortnow, S. Kurtz, Gap-definable counting classes
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

Non-strict majority

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

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

theorem Cslib.Complexity.decidesByMajority_iff_decidesByNonstrictMajority_compl {α : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {V : α × List Bool → Bool} {A : Set α} : DecidesByMajority enc p V A ↔ DecidesByNonstrictMajority enc p (fun (x : α × List Bool) => !V x) Aᶜ

A verifier decides A by strict majority exactly when its negation decides Aᶜ by non-strict majority.

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

Non-strict majority defines PP: a problem is in PP exactly when a polynomial-time verifier accepts the members of the problem, and only them, on at least half of the random strings.

Reductions

theorem Cslib.Complexity.PolyTimeReducible.mem_PP {α : Type} {enc : α ↪ List Bool} {β : Type} {encB : β ↪ List Bool} {A : Set α} {B : Set β} (h : PolyTimeReducible enc encB A B) (hB : B ∈ PP encB) : A ∈ PP enc

PP is closed under polynomial-time reductions. The verifier runs the verifier for the target problem on the reduced instance; the random string is padded to a polynomial in the length of the encoded instance, and the ignored bits multiply both sides of the majority condition by the same power of two.

PP through #P and GapP

theorem Cslib.Complexity.mem_PP_iff_exists_SharpP {α : Type} {enc : α ↪ List Bool} {A : Set α} : A ∈ PP enc ↔ ∃ f ∈ SharpP enc, ∃ (q : Polynomial ℕ), ∀ (a : α), a ∈ A ↔ 2 ^ Polynomial.eval (enc a).length q < 2 * f a

PP through #P: a problem is in PP exactly when, for a function f in #P and a polynomial q, its members are the instances a with 2 ^ q(n) < 2 f(a), where n is the length of the encoded instance. The polynomial q need not be the length of the certificates counted by f.

theorem Cslib.Complexity.mem_PP_iff_exists_GapP {α : Type} {enc : α ↪ List Bool} {A : Set α} : A ∈ PP enc ↔ ∃ g ∈ GapP enc, ∀ (a : α), a ∈ A ↔ 0 < g a

PP through GapP Fenner, Fortnow and Kurtz: a problem is in PP exactly when its members are the instances where some function in GapP is positive.