IP = PSPACE

Every problem in PSPACE reduces to TQBF in polynomial time (Cslib.Complexity.TQBF_pspaceHard), TQBF has an interactive proof (Cslib.Complexity.TQBF_mem_IP), and IP is closed under polynomial-time reductions (Cslib.Complexity.PolyTimeReducible.mem_IP), so PSPACE ⊆ IP. With IP ⊆ PSPACE (Cslib.Complexity.IP_subset_PSPACE) this is the theorem of Shamir Shamir, with the simplification of Shen Shen, following Lund, Fortnow, Karloff and Nisan [LFKN92]; see Arora and Barak, Section 8.3. Every class of the polynomial hierarchy, in particular coNP, has interactive proofs.

The classes are those of the library: IP with private fair coins, a strict polynomial clock for one oracle machine against every stateful prover, completeness 2 / 3 and soundness 1 / 3, and PSPACE decided by one deterministic machine in polynomial space, with respect to any encoding of the instances.

Main results

• Cslib.Complexity.PSPACE_subset_IP, Cslib.Complexity.IP_eq_PSPACE.
• Cslib.Complexity.PH_subset_IP, Cslib.Complexity.coNP_subset_IP.

References

• C. Lund, L. Fortnow, H. Karloff, N. Nisan, Algebraic methods for interactive proof systems
• A. Shamir, IP = PSPACE
• A. Shen, IP = SPACE: simplified proof
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

theorem Cslib.Complexity.PSPACE_subset_IP {α : Type} (enc : α ↪ List Bool) : PSPACE enc ⊆ IP enc

PSPACE ⊆ IP Shamir: every problem in PSPACE reduces to TQBF, which has an interactive proof.

theorem Cslib.Complexity.IP_eq_PSPACE {α : Type} (enc : α ↪ List Bool) : IP enc = PSPACE enc

IP = PSPACE Lund, Fortnow, Karloff and Nisan, Shamir, Shen.

theorem Cslib.Complexity.PH_subset_IP {α : Type} (enc : α ↪ List Bool) : PH enc ⊆ IP enc

Every class of the polynomial hierarchy has interactive proofs.

theorem Cslib.Complexity.coNP_subset_IP {α : Type} (enc : α ↪ List Bool) : coNP enc ⊆ IP enc

coNP ⊆ IP Lund, Fortnow, Karloff and Nisan.