Arthur–Merlin and Merlin–Arthur classes

TheoremAM is contained in \(\Pi_2^p\) (Babai)#●ready to prove

Every decision problem in the Arthur–Merlin class \(\mathsf{AM}\) lies in \(\Pi_2^p\), the second universal level of the polynomial hierarchy.

public theorem_wanted am_subset_pi2 :
    AM ⊆ PiK 2

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

CSLibExt/Computability/Complexity/Classes.lean:327

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

L. Babai, "Trading group theory for randomness", Proceedings of the Seventeenth Annual ACM Symposium on Theory of Computing (STOC 1985), 421-429; see also O. Goldreich and D. Zuckerman and the set lower-bound protocol of Goldwasser-Sipser.

Uses 4

Statement usesThe class \(\mathsf{AM}\) (Arthur–Merlin) · The universal levels of the polynomial hierarchy · Complexity classes · Decision problems

TheoremMA is contained in AM#●ready to prove

Every decision problem in the class \(\mathsf{MA}\) is in the class \(\mathsf{AM}\).

public theorem_wanted ma_subset_am :
    MA ⊆ AM

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

CSLibExt/Computability/Complexity/Classes.lean:649

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

CSLibExt/Computability/Complexity/Classes.lean:327

Sources

L. Babai, "Trading group theory for randomness", Proceedings of the Seventeenth Annual ACM Symposium on Theory of Computing (STOC 1985), 421-429; S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Theorem 8.2 (MA ⊆ AM).

Uses 4

Statement usesThe class \(\mathsf{AM}\) (Arthur–Merlin) · The class MA (Merlin–Arthur) · Complexity classes · Decision problems

TheoremMA is contained in PH#●ready to prove

Every decision problem in the class \(\mathsf{MA}\) is in the polynomial hierarchy \(\mathsf{PH}\).

public theorem_wanted ma_subset_ph :
    MA ⊆ PH

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

CSLibExt/Computability/Complexity/Classes.lean:649

def PH : DecisionComplexityClass := ⋃ k, SigmaK k

CSLibExt/Computability/Complexity/Classes.lean:323

Sources

L. Babai, "Trading group theory for randomness", Proceedings of the Seventeenth Annual ACM Symposium on Theory of Computing (STOC 1985), 421-429 (MA ⊆ AM, AM ⊆ Π₂); L. J. Stockmeyer, "The polynomial-time hierarchy", Theoretical Computer Science 3 (1977), 1-22 (PH); S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Theorem 5.4 (PH ⊆ PSPACE) and Chapter 8.

Uses 4

Statement usesThe class MA (Merlin–Arthur) · The polynomial hierarchy · Complexity classes · Decision problems

3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.