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, CslibFrontier.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 by a problem in ⊕P about pairs of an instance and a random string, there are a function f in #P and a polynomial p such that bit p (enc a).length of f a is set exactly when a is in the problem. In the proof, p is one more than the polynomial length of the random strings.

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. The program of the proof asks for one bit of a function in #P; membership in PWithSharpPOracle does not record the number of queries.

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 has a function in #P and a polynomial-time oracle program that decides the problem against every oracle language answering the bits of that function. The program of the proof asks for one bit of the function; membership in PWithSharpPOracle does not record the number of queries.