Inclusions between complexity classes

The inclusions between the standard classes that papers cite in their preliminaries Arora and Barak, Chapters 2, 4, 5 and 7, Sipser, Chapters 8 and 10. This module proves the inclusions that need several classes at once and imports the narrower modules for the others: P ⊆ BPP is in CslibFrontier.Computability.Complexity.Classes.BPP, the closure properties of PP in CslibFrontier.Computability.Complexity.Classes.PP.Closure, and those of PSPACE in CslibFrontier.Computability.Complexity.Classes.Space.Closure.

• P ⊆ BPP (Cslib.Complexity.P_subset_BPP): a decider ignores its random string.
• NP ⊆ PP (Cslib.Complexity.NP_subset_PP): accept on half of the random strings outright, and on the other half run the verifier, so the majority accepts exactly when some certificate does.
• PP is closed under complement (Cslib.Complexity.compl_mem_PP): 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.
• NP ⊆ PSPACE (Cslib.Complexity.NP_subset_PSPACE): a nondeterministic machine visits at most one new cell per step on each work tape (Turing.MultiTapeNTM.RunsInTime.runsInSpace), so NP is within NPSPACE, which is PSPACE by Savitch's theorem (Cslib.Complexity.NPSPACE_subset_PSPACE).
• PSPACE ⊆ EXP (Cslib.Complexity.PSPACE_subset_EXP): Savitch's decider runs within time exponential in a polynomial (Cslib.Reachability.computableInO_savitch).
• PH ⊆ PSPACE (Cslib.Complexity.PH_subset_PSPACE): PSPACE contains P, is closed under complement (Cslib.Complexity.compl_mem_PSPACE), under polynomial-time reductions (Cslib.Complexity.PolyTimeReducible.mem_PSPACE) and under polynomially bounded existential quantification (Cslib.Complexity.setOf_exists_mem_PSPACE), so it evaluates the alternating quantifiers of every level of the hierarchy one at a time. The existential quantifier over the words w of length ℓ is reachability within two steps from the all-zero word to the all-one word of width ℓ + 1, along edges to true :: w for the accepted w and from every word starting with true to the all-one word; Savitch's algorithm decides it at depth 1, enumerating the candidates in place and reusing the space of the decider for each.

With Cslib.Complexity.P_subset_NP, these give the chain P ⊆ NP ⊆ PSPACE ⊆ EXP. The other inclusions of the chains are elsewhere: P ⊆ PSPACE (Cslib.Complexity.P_subset_PSPACE), NPSPACE = PSPACE (Cslib.Complexity.NPSPACE_eq_PSPACE), RP ⊆ NP (Cslib.Complexity.RP_subset_NP), BPP ⊆ PP (Cslib.Complexity.BPP_subset_PP), BPP ⊆ Σ₂ ∩ Π₂ (Cslib.Complexity.BPP_subset_SigmaP_two_inter_PiP_two), L ⊆ NL ⊆ P (Cslib.Complexity.L_subset_NL, Cslib.Complexity.NL_subset_P), P ⊆ EXP and its strictness (Cslib.Complexity.P_subset_EXP, Cslib.Complexity.P_ssubset_EXP).

Main results

• Cslib.Complexity.NP_subset_NPSPACE, Cslib.Complexity.NP_subset_PSPACE.
• Cslib.Complexity.PSPACE_subset_EXP, Cslib.Complexity.NP_subset_EXP.
• Cslib.Complexity.SigmaP_subset_PSPACE, Cslib.Complexity.PH_subset_PSPACE.
• Cslib.Complexity.SigmaP_subset_EXP, Cslib.Complexity.SigmaP_subset_NEXP.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• M. Sipser, Introduction to the Theory of Computation
• J. Gill, Computational complexity of probabilistic Turing machines
• L. Stockmeyer, The polynomial-time hierarchy

Space

theorem Cslib.Complexity.NP_subset_NPSPACE {α : Type} {enc : α ↪ List Bool} : NP enc ⊆ NPSPACE enc

NP ⊆ NPSPACE: a nondeterministic machine deciding a problem in polynomial time visits at most polynomially many work-tape cells.

theorem Cslib.Complexity.NP_subset_PSPACE {α : Type} {enc : α ↪ List Bool} : NP enc ⊆ PSPACE enc

NP ⊆ PSPACE Arora and Barak, Theorem 4.2: NP ⊆ NPSPACE, and NPSPACE = PSPACE by Savitch's theorem.

theorem Cslib.Complexity.PSPACE_subset_EXP {α : Type} {enc : α ↪ List Bool} : PSPACE enc ⊆ EXP enc

PSPACE ⊆ EXP Arora and Barak, Theorem 4.2, Sipser, Section 8.2: a problem in PSPACE is decided by a nondeterministic machine within polynomial space (Cslib.Complexity.PSPACE_subset_NPSPACE), and Savitch's decider for it runs within time exponential in a polynomial: its codes have polynomial width w, and it runs 2 ^ ((w + 2) * (w + 1)) rounds of polynomial cost (Cslib.Reachability.computableInO_savitch).

theorem Cslib.Complexity.NP_subset_EXP {α : Type} {enc : α ↪ List Bool} : NP enc ⊆ EXP enc

NP ⊆ EXP, through PSPACE.

The polynomial hierarchy

theorem Cslib.Complexity.SigmaP_subset_PSPACE {α : Type} {enc : α ↪ List Bool} (k : ℕ) : SigmaP k enc ⊆ PSPACE enc

Every level of the polynomial hierarchy is within PSPACE.

theorem Cslib.Complexity.PH_subset_PSPACE {α : Type} {enc : α ↪ List Bool} : PH enc ⊆ PSPACE enc

PH ⊆ PSPACE Arora and Barak, Chapter 5, Stockmeyer: the quantifiers of a level of the hierarchy are evaluated one at a time, reusing the space for every certificate.

theorem Cslib.Complexity.SigmaP_subset_EXP {α : Type} {enc : α ↪ List Bool} (k : ℕ) : SigmaP k enc ⊆ EXP enc

Every level of the polynomial hierarchy lies in EXP, via Σₖ ⊆ PSPACE ⊆ EXP.

theorem Cslib.Complexity.SigmaP_subset_NEXP {α : Type} {enc : α ↪ List Bool} (k : ℕ) : SigmaP k enc ⊆ NEXP enc

Every level of the polynomial hierarchy lies in NEXP, via Σₖ ⊆ EXP ⊆ NEXP.