The polynomial hierarchy is in `BP·⊕P` #

The first half of Toda's theorem Toda, Arora and Barak, Section 17.4: every problem in the polynomial hierarchy is decided with bounded error by the parity of a number of witnesses of a polynomial-time verifier (Cslib.Complexity.PH_subset_BPOp_ParityP).

Random parity representations #

A predicate P a u of instances a and strings u of length ℓ (ℓ, like every length here, a polynomial of the length of the encoded instance) is represented with error 2 ^ (-e) by a verifier W, random strings of length ρ and witnesses of length ζ (Cslib.Complexity.Toda.IsRandomParityRep) when for every a and u, all but a 2 ^ (-e) fraction of the random strings r have an odd number of witnesses z with W (a, u ++ r ++ z) exactly when P a u. Representations are built along the quantifier prefix of a verifier of the hierarchy, from the innermost quantifier out:

A polynomial-time predicate of u is represented without randomness by itself (Cslib.Complexity.Toda.isRandomParityRep_base).
Negation adds one witness (Cslib.Complexity.Toda.IsRandomParityRep.not), as ⊕P is closed under complement.
An existential quantifier over strings w of length m, appended to u, is the randomized isolation step of CslibFrontier.Computability.Complexity.Classes.Toda.Isolation (Cslib.Complexity.Toda.IsRandomParityRep.exists): from a representation of the inner predicate with error 2 ^ (-(e + m + 1)), the same random string r serving every w, the verifier Cslib.Complexity.Toda.existsVerifier reads further seeds for 4 (e + 1) (m + 3) trials and represents the quantified predicate with error 2 ^ (-e).

A universal quantifier is a negated existential one. Since the error of the inner representation can be chosen after the outer one, every predicate given by alternating quantifiers is represented with every polynomial error (Cslib.Complexity.Toda.exists_isRandomParityRep_alternation). Error 1 / 4 gives BP·⊕P, after padding the witnesses to a polynomial of the length of the encoded pair of instance and random string.

Main definitions #

Cslib.Complexity.Toda.IsRandomParityRep: random parity representations.
Cslib.Complexity.Toda.notVerifier, Cslib.Complexity.Toda.existsVerifier: the verifiers of negation and of the existential quantifier.

Main results #

Cslib.Complexity.Toda.IsRandomParityRep.not, Cslib.Complexity.Toda.IsRandomParityRep.exists: the quantifier steps.
Cslib.Complexity.Toda.exists_isRandomParityRep_alternation: representations of alternating quantifiers with every error.
Cslib.Complexity.PH_subset_BPOp_ParityP: PH ⊆ BP·⊕P.

References #

Random parity representations #

source

def Cslib.Complexity.Toda.IsRandomParityRep {α : Type} (enc : α ↪ List Bool) (ℓ e ρ ζ : Polynomial ℕ) (W : α × List Bool → Bool) (P : α → List Bool → Prop) :

Prop

W represents P with error 2 ^ (-e) at prefix length ℓ, with random strings of length ρ and witnesses of length ζ, all polynomials of the length of the encoded instance: for every instance a and string u of length ℓ, all but a 2 ^ (-e) fraction of the random strings r have an odd number of witnesses z with W (a, u ++ r ++ z) = true exactly when P a u.

Instances For

source

theorem Cslib.Complexity.Toda.IsRandomParityRep.congr {α : Type} {enc : α ↪ List Bool} {ℓ e ρ ζ : Polynomial ℕ} {W : α × List Bool → Bool} {P Q : α → List Bool → Prop} (h : IsRandomParityRep enc ℓ e ρ ζ W P) (hPQ : ∀ (a : α) (u : List Bool), u.length = Polynomial.eval (enc a).length ℓ → (P a u ↔ Q a u)) :

IsRandomParityRep enc ℓ e ρ ζ W Q

A representation of P represents every predicate agreeing with P on strings of length ℓ.

source

theorem Cslib.Complexity.Toda.isRandomParityRep_base {α : Type} {enc : α ↪ List Bool} (ℓ e : Polynomial ℕ) (V : α × List Bool → Bool) :

IsRandomParityRep enc ℓ e 0 0 (fun (x : α × List Bool) => V (x.1, List.take (Polynomial.eval (enc x.1).length ℓ) x.2)) fun (a : α) (u : List Bool) => V (a, u) = true

The base case: a verifier of u, reading the first ℓ bits, represents itself without randomness and with one witness, the empty one.

Negation #

source

def Cslib.Complexity.Toda.notVerifier {α : Type} (enc : α ↪ List Bool) (ℓ ρ : Polynomial ℕ) (W : α × List Bool → Bool) (x : α × List Bool) :

Bool

The verifier of the negation: succVerifier applied after the prefix and the random string, accepting one more witness.

Instances For

source

theorem Cslib.Complexity.Toda.IsRandomParityRep.not {α : Type} {enc : α ↪ List Bool} {ℓ e ρ ζ : Polynomial ℕ} {W : α × List Bool → Bool} {P : α → List Bool → Prop} (h : IsRandomParityRep enc ℓ e ρ ζ W P) :

IsRandomParityRep enc ℓ e ρ (ζ + 1) (notVerifier enc ℓ ρ W) fun (a : α) (u : List Bool) => ¬P a u

Negation adds one witness, with the same error.

The existential quantifier #

source

def Cslib.Complexity.Toda.trialVerifier {α : Type} (W : α × List Bool → Bool) (a : α) (u r : List Bool) (M level : ℕ) (seed block : List Bool) :

Bool

One trial on a block w ++ z of M + ζ bits: w passes the Valiant–Vazirani test of level level with seed seed, and W accepts u ++ w ++ r ++ z.

Instances For

source

def Cslib.Complexity.Toda.trialsVerifier {α : Type} (W : α × List Bool → Bool) (a : α) (u r seeds : List Bool) (M Z T B : ℕ) (y : List Bool) :

Bool

All trials: the j-th of the T rows of M + Z + 1 bits of y is accepted by succTest of the j-th trial, at level j % (M + 3), with the j-th seed of B bits.

Instances For

source

def Cslib.Complexity.Toda.existsVerifier {α : Type} (enc : α ↪ List Bool) (ℓ m ρ ζ e : Polynomial ℕ) (W : α × List Bool → Bool) (x : α × List Bool) :

Bool

The verifier of the existential quantifier over strings of length m: after the prefix u of length ℓ come the inner random string r of length ρ and the seeds of T = 4 (e + 1) (m + 3) trials of B = (m + 2) (m + 1) bits each; the witnesses are accepted by succTest of all trials.

Instances For

source

Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => trialVerifier W (a x) (u x) (r x) (M x) (level x) (seed x) (block x)) input Turing.MultiTapeTM.encBool

source

Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => trialsVerifier W (a x) (u x) (r x) (seeds x) (M x) (Z x) (T x) (B x) (y x)) input Turing.MultiTapeTM.encBool

source

theorem Cslib.Complexity.Toda.IsRandomParityRep.exists {α : Type} {enc : α ↪ List Bool} {ℓ m ρ ζ e : Polynomial ℕ} {W : α × List Bool → Bool} {P : α → List Bool → Prop} (h : IsRandomParityRep enc (ℓ + m) (e + m + 1) ρ ζ W P) :

IsRandomParityRep enc ℓ e (ρ + 4 * (e + 1) * (m + 3) * ((m + 2) * (m + 1))) (4 * (e + 1) * (m + 3) * (m + ζ + 1) + 1) (existsVerifier enc ℓ m ρ ζ e W) fun (a : α) (u : List Bool) => ∃ (w : List Bool), w.length = Polynomial.eval (enc a).length m ∧ P a (u ++ w)

The existential quantifier. From a representation of P at prefix length ℓ + m with error 2 ^ (-(e + m + 1)), existsVerifier represents ∃ w, |w| = m ∧ P a (u ++ w) at prefix length ℓ with error 2 ^ (-e), reading 4 (e + 1) (m + 3) (m + 2) (m + 1) more random bits and witnesses of 4 (e + 1) (m + 3) (m + ζ + 1) + 1 bits.

Alternating quantifiers #

source

theorem Cslib.Complexity.Toda.exists_isRandomParityRep_alternation {α : Type} {enc : α ↪ List Bool} {V : α × List Bool → Bool} (hV : Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (ps : List (Polynomial ℕ)) (q : Bool) (ℓ e : Polynomial ℕ) :

∃ (ρ : Polynomial ℕ) (ζ : Polynomial ℕ) (W : α × List Bool → Bool), Turing.MultiTapeTM.ComputableInPolyTime W (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool ∧ IsRandomParityRep enc ℓ e ρ ζ W fun (a : α) (u : List Bool) => Alternation q (List.map (fun (p : Polynomial ℕ) => Polynomial.eval (enc a).length p) ps) fun (w : List Bool) => V (a, u ++ w) = true

Alternating quantifiers are represented with every error. For a polynomial-time verifier V and certificate lengths ps, the alternating quantifiers over ps applied to V (a, u ++ ·) have a polynomial-time random parity representation at every prefix length ℓ with every error 2 ^ (-e).