Toda's theorem

Toda's theorem Toda, Arora and Barak, Section 17.4: the polynomial hierarchy lies in BP·⊕P (Cslib.Complexity.PH_subset_BPOp_ParityP), which lies in polynomial time with an oracle for a function in #P (Cslib.Complexity.BPOp_ParityP_subset_PWithSharpPOracle), so PH ⊆ P^#P (Cslib.Complexity.PH_subset_PWithSharpPOracle), for the class P^#P of Cslib.Complexity.PWithSharpPOracle: one polynomial-time oracle program, correct against every oracle language answering the bits of a function in #P.

One bit of a #P value

For a problem in BP·⊕P, decided with bounded error by the parity of the number f r of witnesses of a verifier on random strings r of length R, Complexity.Computability.Complexity.Classes.Toda.Counting gives a function in #P on the same instances whose bit R + 1 says whether more than half of the random strings have f r odd (Cslib.Complexity.exists_SharpP_testBit_of_mem_BPOp_ParityP). The program deciding the problem in P^#P (Cslib.Complexity.mem_PWithSharpPOracle_of_testBit) asks for this bit with a single query, as in Toda's PH ⊆ P^#P[1]; the class PWithSharpPOracle itself does not count queries.

Main results

• Cslib.Complexity.exists_SharpP_testBit_of_mem_BPOp_ParityP: a problem in BP·⊕P is decided by a bit at a polynomial position of a function in #P.
• Cslib.Complexity.BPOp_ParityP_subset_PWithSharpPOracle: BP·⊕P ⊆ P^#P.
• Cslib.Complexity.PH_subset_PWithSharpPOracle: Toda's theorem, PH ⊆ P^#P.

References

• S. Toda, PP is as hard as the polynomial-time hierarchy
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

BP·⊕P ⊆ P^#P

theorem Cslib.Complexity.exists_SharpP_testBit_of_mem_BPOp_ParityP {α : Type} {enc : α ↪ List Bool} {L : Set α} (hL : L ∈ BPOp enc (ParityP (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits))) : ∃ f ∈ SharpP enc, ∃ (p : Polynomial ℕ), ∀ (a : α), a ∈ L ↔ (f a).testBit (Polynomial.eval (enc a).length p) = true

A problem in BP·⊕P is one bit of a #P value: for a problem decided with bounded error, using random strings of length R = p (enc a).length, by the parity of a verifier's number of witnesses, some function in #P has bit R + 1 set exactly at the members of the problem.

theorem Cslib.Complexity.BPOp_ParityP_subset_PWithSharpPOracle {α : Type} {enc : α ↪ List Bool} : BPOp enc (ParityP (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits)) ⊆ PWithSharpPOracle enc

BP·⊕P ⊆ P^#P: a problem decided with bounded error by a problem in ⊕P about pairs of an instance and a random string is in P^#P, decided by a program asking for one bit of a function in #P.

theorem Cslib.Complexity.PH_subset_PWithSharpPOracle {α : Type} {enc : α ↪ List Bool} : PH enc ⊆ PWithSharpPOracle enc

Toda's theorem: PH ⊆ P^#P. Every problem in the polynomial hierarchy is decided by a polynomial-time oracle program, asking for one bit of a function in #P, against every oracle language answering the bits of that function.