Randomized, interactive and quantum complexity

Probabilistic classes (RP, BPP), Arthur–Merlin and interactive proofs (AM, MA, IP = PSPACE, graph (non)isomorphism), BPP versus nonuniform and alternating classes, randomized reductions (Valiant–Vazirani), and quantum classes BQP and QMA.

TheoremAdleman's theorem: BPP is contained in P/poly#●ready to prove

Every decision problem in BPP lies in P/poly.

public theorem_wanted adleman :
    BPP ⊆ PPoly

def BPP : DecisionComplexityClass :=
  {L | ∃ p : Polynomial ℕ, ∃ R : List Bool × List Bool → Bool, IsPolyTime R ∧
    ∀ x,
      (L x = true →
        3 * Set.ncard {r : Fin (p.eval x.length) → Bool | R (x, List.ofFn r) = true} ≥
          2 * 2 ^ (p.eval x.length)) ∧
      (L x = false →
        3 * Set.ncard {r : Fin (p.eval x.length) → Bool | R (x, List.ofFn r) = true} ≤
          2 ^ (p.eval x.length))}

CSLibExt/Computability/Complexity/Classes.lean:199

def PPoly : DecisionComplexityClass :=
  {L | ∃ p : Polynomial ℕ, ∃ advice : ℕ → List Bool,
    (∀ n, (advice n).length ≤ p.eval n) ∧
    ∃ R : List Bool × List Bool → Bool, IsPolyTime R ∧
    ∀ x, L x ↔ R (x, advice x.length) = true}

CSLibExt/Computability/Complexity/Classes.lean:222

Sources

L. Adleman, "Two theorems on random polynomial time", Proceedings of the Nineteenth Annual Symposium on Foundations of Computer Science (FOCS 1978), 75-83.

Uses 4

Statement usesBPP · Polynomial time with polynomial advice · Complexity classes · Decision problems

TheoremIP = PSPACE (Shamir)#●ready to prove

The class \(\mathsf{IP}\) of decision problems that have interactive proofs (a polynomial-time verifier using polynomially many rounds and random coins, with completeness at least \(2/3\) and soundness at most \(1/3\) against every prover) equals the class \(\mathrm{PSPACE}\) of decision problems whose languages are decided by multi-tape Turing machines in polynomial space.

public theorem_wanted ip_eq_pspace :
    IP = PSPACE

def IP : DecisionComplexityClass :=
  {L | ∃ s r q : Polynomial ℕ,
    ∃ Vmsg : List Bool × List Bool × List (List Bool) → List Bool,
    ∃ Vdec : List Bool × List Bool × List (List Bool) → Bool,
    IsPolyTime Vmsg ∧ IsPolyTime Vdec ∧
    ∀ x,
      (L x = true →
        ∃ P : List (List Bool) → List Bool,
          3 * Set.ncard {coins : Fin (s.eval x.length) → Bool |
            IPGame (q.eval x.length) Vmsg Vdec P x (List.ofFn coins)
              (r.eval x.length) [] = true} ≥
            2 * 2 ^ (s.eval x.length)) ∧
  ⋯

CSLibExt/Computability/Complexity/Classes.lean:368

def PSPACE : DecisionComplexityClass :=
  {L | langOf L ∈ Cslib.Turing.MultiTapeTM.Classes.PSPACE}

CSLibExt/Computability/Complexity/Classes.lean:117

Sources

A. Shamir, "IP = PSPACE", Journal of the ACM 39 (1992), 869-877 (FOCS 1990); see also C. Lund, L. Fortnow, H. Karloff, and N. Nisan, "Algebraic methods for interactive proof systems", Journal of the ACM 39 (1992), 859-868.

Uses 3

Statement usesThe class IP · Polynomial space for decision problems · Complexity classes

TheoremSipser-Gács-Lautemann: BPP is in \(\Sigma_2^p\) and \(\Pi_2^p\)#●ready to prove

Every decision problem in BPP lies in \(\Sigma_2^p\) and in \(\Pi_2^p\), the classes of the polynomial hierarchy defined by two alternating blocks of polynomially bounded quantifiers, beginning with \(\exists\) and with \(\forall\) respectively.

public theorem_wanted sipser_gacs_lautemann :
    BPP ⊆ SigmaK 2 ∧ BPP ⊆ PiK 2

def BPP : DecisionComplexityClass :=
  {L | ∃ p : Polynomial ℕ, ∃ R : List Bool × List Bool → Bool, IsPolyTime R ∧
    ∀ x,
      (L x = true →
        3 * Set.ncard {r : Fin (p.eval x.length) → Bool | R (x, List.ofFn r) = true} ≥
          2 * 2 ^ (p.eval x.length)) ∧
      (L x = false →
        3 * Set.ncard {r : Fin (p.eval x.length) → Bool | R (x, List.ofFn r) = true} ≤
          2 ^ (p.eval x.length))}

CSLibExt/Computability/Complexity/Classes.lean:199

def SigmaK (k : ℕ) : DecisionComplexityClass :=
  {L | ∃ p : Polynomial ℕ, ∃ R : List Bool × List (List Bool) → Bool, IsPolyTime R ∧
    ∀ x, L x ↔ AltQuant (fun n => p.eval n) k true R x}

CSLibExt/Computability/Complexity/Classes.lean:313

def PiK (k : ℕ) : DecisionComplexityClass :=
  {L | ∃ p : Polynomial ℕ, ∃ R : List Bool × List (List Bool) → Bool, IsPolyTime R ∧
    ∀ x, L x ↔ AltQuant (fun n => p.eval n) k false R x}

CSLibExt/Computability/Complexity/Classes.lean:318

Sources

M. Sipser, "A complexity theoretic approach to randomness", Proceedings of the Fifteenth Annual ACM Symposium on Theory of Computing (STOC 1983), 330-335; P. Gács (unpublished); C. Lautemann, "BPP and the polynomial hierarchy", Information Processing Letters 17 (1983), 215-217.

Uses 5

Statement usesBPP · The universal levels of the polynomial hierarchy · The class \(\Sigma_k^p\) · Complexity classes · Decision problems

3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.