Documentation

Complexity.Computability.Complexity.Classes.ZPP

The class ZPP #

ZPP is defined like RP (Cslib.Complexity.RP), through deterministic polynomial-time machines that read a random string, but with zero error: A ∈ ZPP enc when there are a polynomial p and a function V : α × List Bool → Option Bool, computable in polynomial time on inputs frame (enc a) ++ r, such that for every instance a an answer V (a, r) = some b is always right, b = true exactly when a ∈ A, and at least half of the random strings r of length p (enc a).length give an answer (Cslib.Complexity.DecidesWithZeroError). These are the algorithms that never err and say "don't know" with probability at most 1 / 2 Arora and Barak, Section 7.3; the definition through expected polynomial running time defines the same class, but expected running time is not modelled here.

ZPP = RP ∩ coRP Arora and Barak, Section 7.3 (Cslib.Complexity.ZPP_eq_RP_inter_coRP). Answering true only on the answer some true decides a problem in ZPP with one-sided error, and so does answering false only on some false for its complement. Conversely, for one-sided-error deciders of a problem and of its complement, which read disjoint parts of the random string, the first accepting gives the answer some true, the second the answer some false, and neither errs; on a member the first accepts on at least half of the random strings, and on a non-member the second does.

Main definitions #

Main results #

References #

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

V decides A with zero error, using random strings whose length is p evaluated at the length of the encoded instance: for every instance a, an answer V (a, r) = some b is right, b = true exactly when a ∈ A, and at least half of the random strings give an answer.

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

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

    Instances For
      source
      theorem Cslib.Complexity.mem_ZPP {α : Type} {enc : α ↪ List Bool} {A : Set α} :
      A ∈ ZPP enc ↔ ∃ (p : Polynomial ℕ) (V : α × List Bool → Option Bool), Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encBool) ∧ DecidesWithZeroError enc p V A
      source
      theorem Cslib.Complexity.mem_ZPP_iff_tidy {α : Type} {enc : α ↪ List Bool} {A : Set α} :
      A ∈ ZPP enc ↔ ∃ (p : Polynomial ℕ) (V : α × List Bool → Option Bool), Turing.MultiTapeTM.ComputableTidilyInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encBool) ∧ DecidesWithZeroError enc p V A

      Cslib.Complexity.mem_ZPP with a tidy verifier, for proofs that compose machines.

      source
      theorem Cslib.Complexity.DecidesWithZeroError.decidesWithOneSidedError {α : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {V : α × List Bool → Option Bool} {A : Set α} (h : DecidesWithZeroError enc p V A) :
      DecidesWithOneSidedError enc p (fun (x : α × List Bool) => (V x).getD false) A

      Accepting exactly on the answer some true decides the problem with one-sided error.

      source
      theorem Cslib.Complexity.DecidesWithZeroError.compl {α : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {V : α × List Bool → Option Bool} {A : Set α} (h : DecidesWithZeroError enc p V A) :
      DecidesWithZeroError enc p (fun (x : α × List Bool) => Option.map not (V x)) Aᶜ

      Negating the answers decides the complement with zero error.

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

      ZPP is closed under complement.

      source
      theorem Cslib.Complexity.ZPP_subset_RP {α : Type} {enc : α ↪ List Bool} :
      ZPP enc ⊆ RP enc

      ZPP ⊆ RP: accept exactly on the answer some true.

      source
      theorem Cslib.Complexity.ZPP_subset_coRP {α : Type} {enc : α ↪ List Bool} :
      ZPP enc ⊆ coRP enc

      ZPP ⊆ coRP: the complement is in ZPP, hence in RP.

      Splitting random strings #

      RP ∩ coRP ⊆ ZPP #

      source
      theorem Cslib.Complexity.RP_inter_coRP_subset_ZPP {α : Type} {enc : α ↪ List Bool} :
      RP enc ∩ coRP enc ⊆ ZPP enc

      RP ∩ coRP ⊆ ZPP: with one-sided-error deciders V₁ of A and V₂ of its complement, reading the first and the last part of the random string, answer some true when V₁ accepts, some false when V₂ does, and none otherwise.

      source
      theorem Cslib.Complexity.ZPP_eq_RP_inter_coRP {α : Type} {enc : α ↪ List Bool} :
      ZPP enc = RP enc ∩ coRP enc

      ZPP = RP ∩ coRP Arora and Barak, Section 7.3.