Closure properties of PP

PP contains NP Gill: on random strings b :: w, accept when b = false and run the verifier on w when b = true, so the majority accepts exactly when some certificate does. PP is closed under complement Gill: with two more random bits, accept on a quarter of the random strings and one more, and on half of them reject what the verifier accepts; the majority accepts exactly when the verifier accepts at most half of its random strings. Hence also coNP ⊆ PP.

Main results

• Cslib.Complexity.P_subset_PP: P ⊆ PP.
• Cslib.Complexity.NP_subset_PP, Cslib.Complexity.coNP_subset_PP.
• Cslib.Complexity.compl_mem_PP, Cslib.Complexity.PP_eq_preimage_compl_PP: closure under complement.

References

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

theorem Cslib.Complexity.NP_subset_PP {α : Type} {enc : α ↪ List Bool} : NP enc ⊆ PP enc

NP ⊆ PP Gill: on random strings b :: w, accept when b = false and run the verifier on w when b = true. The majority accepts exactly when the verifier accepts some certificate.

theorem Cslib.Complexity.P_subset_PP {α : Type} {enc : α ↪ List Bool} : P enc ⊆ PP enc

P ⊆ PP: P ⊆ NP and NP ⊆ PP.

theorem Cslib.Complexity.compl_mem_PP {α : Type} {enc : α ↪ List Bool} {A : Set α} (hA : A ∈ PP enc) : Aᶜ ∈ PP enc

PP is closed under complement Gill. On random strings b₁ :: b₂ :: w, accept when b₁ = b₂ = false and on b₁ = false, b₂ = true only for w all zeros, and reject what the verifier accepts on w when b₁ = true. With acc accepted and rej rejected strings of length m, this accepts 2 ^ m + 1 + 2 * rej of the 4 * 2 ^ m strings, more than half exactly when 2 * acc ≤ 2 ^ m.

theorem Cslib.Complexity.PP_eq_preimage_compl_PP {α : Type} (enc : α ↪ List Bool) : PP enc = compl ⁻¹' PP enc

PP equals its preimage under complement.

theorem Cslib.Complexity.coNP_subset_PP {α : Type} {enc : α ↪ List Bool} : coNP enc ⊆ PP enc

coNP ⊆ PP: NP ⊆ PP and PP is closed under complement.