The BP and parity operators

A class operator turns a class C of problems about pairs (a, w) of an instance and a string into a class of problems about instances, by quantifying over the strings w whose length is a polynomial p of the length of the encoded instance Schöning, Toda:

• ⊕·C (Cslib.Complexity.ParityOp): a ∈ L exactly when an odd number of the strings w of length p (enc a).length have (a, w) ∈ L', for some L' ∈ C and polynomial p.
• BP·C (Cslib.Complexity.BPOp): for some L' ∈ C and polynomial p, the pairs (a, r) in L', with r ranging over the strings of length p (enc a).length, decide L with bounded error (Cslib.Complexity.DecidesWithBoundedError): at least two thirds of the random strings r give the right answer.

The problems of C are about pairs encoded by encPair enc encBits, so the polynomials of C are polynomials of the length of the encoded pair, while p is a polynomial of the length of the encoded instance. Every string counted by an operator has length p (enc a).length; problems of C may say anything about other pairs.

BPP is BP·P (Cslib.Complexity.BPOp_P), and ⊕P is defined as ⊕·P (Cslib.Complexity.ParityP). Toda's theorem places the polynomial hierarchy in BP·⊕P.

Main definitions

• Cslib.Complexity.ParityOp: the parity operator ⊕·.
• Cslib.Complexity.BPOp: the bounded-error operator BP·.

Main results

• Cslib.Complexity.ParityOp_mono, Cslib.Complexity.BPOp_mono: the operators are monotone.
• Cslib.Complexity.compl_mem_BPOp: BP·C is closed under complement when C is.
• Cslib.Complexity.BPOp_P: BP·P = BPP.

References

• U. Schöning, Probabilistic complexity classes and lowness
• S. Toda, PP is as hard as the polynomial-time hierarchy
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

def Cslib.Complexity.ParityOp {α : Type} (enc : α ↪ List Bool) (C : Set (Set (α × List Bool))) : Set (Set α)

The parity operator ⊕·C: the problems L such that, for some L' ∈ C and polynomial p, a ∈ L exactly when an odd number of the strings w of length p (enc a).length have (a, w) ∈ L'. The problems of C are about pairs of an instance and a string Toda.

def Cslib.Complexity.BPOp {α : Type} (enc : α ↪ List Bool) (C : Set (Set (α × List Bool))) : Set (Set α)

The bounded-error operator BP·C: the problems L such that, for some L' ∈ C and polynomial p, membership in L' decides L with bounded error using random strings of length p (enc a).length: for every instance a, at least two thirds of the random strings r have (a, r) ∈ L' exactly when a ∈ L. The problems of C are about pairs of an instance and a string Schöning, Toda.

theorem Cslib.Complexity.mem_ParityOp {α : Type} {enc : α ↪ List Bool} {C : Set (Set (α × List Bool))} {L : Set α} : L ∈ ParityOp enc C ↔ ∃ (p : Polynomial ℕ), ∃ L' ∈ C, ∀ (a : α), a ∈ L ↔ Odd (acceptCount (fun (x : α × List Bool) => decide (x ∈ L')) a (Polynomial.eval (enc a).length p))

theorem Cslib.Complexity.mem_BPOp {α : Type} {enc : α ↪ List Bool} {C : Set (Set (α × List Bool))} {L : Set α} : L ∈ BPOp enc C ↔ ∃ (p : Polynomial ℕ), ∃ L' ∈ C, DecidesWithBoundedError enc p (fun (x : α × List Bool) => decide (x ∈ L')) L

theorem Cslib.Complexity.ParityOp_mono {α : Type} {enc : α ↪ List Bool} {C D : Set (Set (α × List Bool))} (h : C ⊆ D) : ParityOp enc C ⊆ ParityOp enc D

The parity operator is monotone.

theorem Cslib.Complexity.BPOp_mono {α : Type} {enc : α ↪ List Bool} {C D : Set (Set (α × List Bool))} (h : C ⊆ D) : BPOp enc C ⊆ BPOp enc D

The bounded-error operator is monotone.

theorem Cslib.Complexity.compl_mem_BPOp {α : Type} {enc : α ↪ List Bool} {C : Set (Set (α × List Bool))} {L : Set α} (hC : ∀ L' ∈ C, L'ᶜ ∈ C) (hL : L ∈ BPOp enc C) : Lᶜ ∈ BPOp enc C

BP·C is closed under complement when C is: the complement of the deciding problem decides the complement with bounded error.

theorem Cslib.Complexity.BPOp_P {α : Type} {enc : α ↪ List Bool} : BPOp enc (P (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits)) = BPP enc

BP·P = BPP: deciding with bounded error by a polynomial-time verifier is deciding with bounded error by membership in a problem in P.