Documentation

CslibFrontier.Computability.Complexity.Classes.BPP

The classes BPP and promise-BPP #

BPP is defined through deterministic polynomial-time machines that read a random string Arora and Barak, Section 7.1: A ∈ BPP enc when there are a polynomial p and a function V : α × List Bool → Bool, computable in polynomial time on inputs encPair enc encBits (a, r) = frame (enc a) ++ r, such that for every instance a, at least two thirds of the random strings r of length p (enc a).length give the right answer: V (a, r) = true exactly when a ∈ A.

The bounded-error condition is stated once, for promise problems (Cslib.Complexity.PromiseProblem.SolvesWithBoundedError): the right answer is required only on the yes-instances and the no-instances Goldreich, Definition 1.2. A decision problem A is the promise problem PromiseProblem.ofSet A, so DecidesWithBoundedError enc p V A is (ofSet A).SolvesWithBoundedError enc p V, and A ∈ BPP enc is, by definition, ofSet A ∈ PromiseBPP enc (Cslib.Complexity.ofSet_mem_PromiseBPP). Results proved for PromiseBPP specialize to BPP in this way.

The probability is written as a count over the random strings, which are functions Fin (p (enc a).length) → Bool. The characterisation by probabilistic machines (Cslib.Complexity.mem_BPP_iff_exists_mem_BPTIME) is proved in CslibFrontier.Computability.Complexity.Classes.Time.

Main definitions #

Main results #

References #

source
@[reducible, inline]
abbrev Cslib.Complexity.BoundedErrorAt {α : Type} (enc : α ↪ List Bool) (p : Polynomial ℕ) (V : α × List Bool → Bool) (a : α) (b : Bool) :
Prop

V gives the answer b with bounded error on the instance a, using random strings whose length is p evaluated at the length of the encoded instance: at least two thirds of the random strings r of length p (enc a).length give V (a, r) = b.

Instances For
    source
    theorem Cslib.Complexity.boundedErrorAt_true_iff {α : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {V : α × List Bool → Bool} {a : α} :
    BoundedErrorAt enc p V a true ↔ 2 * 2 ^ Polynomial.eval (enc a).length p ≤ 3 * acceptCount V a (Polynomial.eval (enc a).length p)

    Bounded error towards true is acceptance of at least two thirds of the random strings.

    source
    theorem Cslib.Complexity.boundedErrorAt_false_iff {α : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {V : α × List Bool → Bool} {a : α} :
    BoundedErrorAt enc p V a false ↔ 3 * acceptCount V a (Polynomial.eval (enc a).length p) ≤ 2 ^ Polynomial.eval (enc a).length p

    Bounded error towards false is acceptance of at most one third of the random strings.

    source
    theorem Cslib.Complexity.BoundedErrorAt.congr {α : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {V W : α × List Bool → Bool} {a : α} {b : Bool} (h : BoundedErrorAt enc p V a b) (hVW : ∀ (r : Fin (Polynomial.eval (enc a).length p) → Bool), V (a, List.ofFn r) = W (a, List.ofFn r)) :
    BoundedErrorAt enc p W a b

    Bounded error at an instance depends only on the verifier's values on strings of length p(|a|).

    source
    theorem Cslib.Complexity.BoundedErrorAt.not {α : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {V : α × List Bool → Bool} {a : α} {b : Bool} (h : BoundedErrorAt enc p V a b) :
    BoundedErrorAt enc p (fun (x : α × List Bool) => !V x) a !b

    Negating the verifier negates the bounded-error answer at a.

    source
    def Cslib.Complexity.PromiseProblem.SolvesWithBoundedError {α : Type} (enc : α ↪ List Bool) (p : Polynomial ℕ) (V : α × List Bool → Bool) (Q : PromiseProblem α) :
    Prop

    V solves the promise problem Q with bounded error, using random strings whose length is p evaluated at the length of the encoded instance: for every yes-instance at least two thirds of the random strings are accepted, and for every no-instance at least two thirds are rejected Goldreich, Definition 1.2. Nothing is required on instances outside the promise.

    Instances For
      source
      theorem Cslib.Complexity.PromiseProblem.SolvesWithBoundedError.compl {α : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {V : α × List Bool → Bool} {Q : PromiseProblem α} (h : SolvesWithBoundedError enc p V Q) :
      SolvesWithBoundedError enc p (fun (x : α × List Bool) => !V x) Qᶜ

      Negating the verifier solves the complement promise problem with bounded error.

      source
      def Cslib.Complexity.DecidesWithBoundedError {α : Type} (enc : α ↪ List Bool) (p : Polynomial ℕ) (V : α × List Bool → Bool) (A : Set α) :
      Prop

      V decides A with bounded error, using random strings whose length is p evaluated at the length of the encoded instance: it solves the promise problem ofSet A with bounded error. For every instance a, at least two thirds of the random strings r give the right answer, V (a, r) = true for members of A and V (a, r) = false for the others.

      Instances For
        source
        theorem Cslib.Complexity.DecidesWithBoundedError.compl {α : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {V : α × List Bool → Bool} {A : Set α} (h : DecidesWithBoundedError enc p V A) :
        DecidesWithBoundedError enc p (fun (x : α × List Bool) => !V x) Aᶜ

        Negating the verifier decides the complement with bounded error.

        source
        def Cslib.Complexity.PromiseBPP {α : Type} (enc : α ↪ List Bool) :
        Set (PromiseProblem α)

        The promise problems solved with bounded error by polynomial-time algorithms reading polynomially long random strings, with respect to the encoding enc of instances Goldreich, Definition 1.2.

        Instances For
          source
          def Cslib.Complexity.BPP {α : Type} (enc : α ↪ List Bool) :
          Set (Set α)

          The problems decided with bounded error by polynomial-time machines reading polynomially long random strings, with respect to the encoding enc of instances Gill, Arora and Barak, Section 7.1.

          Instances For
            source
            theorem Cslib.Complexity.mem_PromiseBPP_iff {α : Type} {enc : α ↪ List Bool} {Q : PromiseProblem α} :
            Q ∈ PromiseBPP enc ↔ ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool ∧ PromiseProblem.SolvesWithBoundedError enc p V Q

            Membership in PromiseBPP unfolded to a polynomial coin bound and a polynomial-time bounded-error solver.

            source
            theorem Cslib.Complexity.mem_BPP {α : Type} {enc : α ↪ List Bool} {A : Set α} :
            A ∈ BPP enc ↔ ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool ∧ DecidesWithBoundedError enc p V A
            source
            @[simp]
            theorem Cslib.Complexity.ofSet_mem_PromiseBPP {α : Type} {enc : α ↪ List Bool} {A : Set α} :
            PromiseProblem.ofSet A ∈ PromiseBPP enc ↔ A ∈ BPP enc

            A decision problem, as a promise problem, is in PromiseBPP exactly when it is in BPP; this holds by definition.

            source
            theorem Cslib.Complexity.compl_mem_PromiseBPP {α : Type} {enc : α ↪ List Bool} {Q : PromiseProblem α} (hQ : Q ∈ PromiseBPP enc) :
            Qᶜ ∈ PromiseBPP enc

            PromiseBPP is closed under complement.

            source
            theorem Cslib.Complexity.compl_mem_BPP {α : Type} {enc : α ↪ List Bool} {A : Set α} (hA : A ∈ BPP enc) :
            Aᶜ ∈ BPP enc

            BPP is closed under complement.

            source
            theorem Cslib.Complexity.BPP_eq_preimage_compl_BPP {α : Type} (enc : α ↪ List Bool) :
            BPP enc = compl ⁻¹' BPP enc

            BPP equals its preimage under complement.

            source
            theorem Cslib.Complexity.P_subset_BPP {α : Type} {enc : α ↪ List Bool} :
            P enc ⊆ BPP enc

            P ⊆ BPP: a decider is a bounded-error verifier ignoring its random string, of length 0.