The classes RP and coRP, and their promise versions

RP is defined like BPP (Cslib.Complexity.BPP), through deterministic polynomial-time machines that read a random string, but with one-sided error Arora and Barak, Section 7.3: A ∈ RP enc when there are a polynomial p and a function V : α × List Bool → Bool, computable in polynomial time on inputs frame (enc a) ++ r, such that for every member a of A at least half of the random strings r of length p (enc a).length are accepted, and for every non-member none is. coRP contains the complements of problems in RP.

As for BPP, the one-sided error condition is stated once, for promise problems (Cslib.Complexity.PromiseProblem.SolvesWithOneSidedError) Goldreich, Section 6.2, and A ∈ RP enc is, by definition, ofSet A ∈ PromiseRP enc (Cslib.Complexity.ofSet_mem_PromiseRP). Since an accepted random string is a certificate, PromiseRP ⊆ PromiseNP and RP ⊆ NP. ZPP, with ZPP = RP ∩ coRP, is defined in Cslib.Complexity.ZPP.

The error 1 / 2 can be made exponentially small Arora and Barak, Chapter 7: for a polynomial q, run the solver on q(n) independent blocks of random bits, where n is the length of the encoded instance, and accept when some run accepts (Cslib.Complexity.repeatAny). A yes-instance is then rejected on at most a 2 ^ (-q(n)) fraction of the random strings (Cslib.Complexity.PromiseProblem.SolvesWithOneSidedErrorExponent), and a no-instance is still never accepted. Two runs reject a yes-instance with probability at most 1 / 4, so PromiseRP ⊆ PromiseBPP, and RP ⊆ BPP.

Main definitions

• Cslib.Complexity.PromiseProblem.SolvesWithOneSidedError: the one-sided error condition, and its specialization Cslib.Complexity.DecidesWithOneSidedError to decision problems.
• Cslib.Complexity.PromiseRP, Cslib.Complexity.PromiseCoRP, Cslib.Complexity.RP, Cslib.Complexity.coRP.
• Cslib.Complexity.PromiseProblem.SolvesWithOneSidedErrorExponent: one-sided error at most 2 ^ (-q(n)), and its specialization Cslib.Complexity.DecidesWithOneSidedErrorExponent.

Main results

• Cslib.Complexity.mem_PromiseRP_iff: unfolding PromiseRP to a polynomial-time verifier.
• Cslib.Complexity.ofSet_mem_PromiseRP, Cslib.Complexity.ofSet_mem_PromiseCoRP.
• Cslib.Complexity.PromiseProblem.SolvesWithOneSidedError.exists_certificate, Cslib.Complexity.DecidesWithOneSidedError.isVerifier, Cslib.Complexity.RP_subset_NP, Cslib.Complexity.PromiseRP_subset_PromiseNP, Cslib.Complexity.coRP_subset_coNP.
• Cslib.Complexity.PromiseProblem.SolvesWithOneSidedError.repeatAny: repetition reduces the error to 2 ^ (-q(n)).
• Cslib.Complexity.mem_PromiseRP_iff_forall_solvesWithOneSidedErrorExponent, Cslib.Complexity.mem_RP_iff_forall_decidesWithOneSidedErrorExponent: error reduction for PromiseRP and RP.
• Cslib.Complexity.PromiseRP_subset_PromiseBPP, Cslib.Complexity.PromiseCoRP_subset_PromiseBPP, Cslib.Complexity.RP_subset_BPP, Cslib.Complexity.coRP_subset_BPP.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• O. Goldreich, On promise problems: a survey

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

V solves the promise problem Q with one-sided error, using random strings whose length is p evaluated at the length of the encoded instance: for every yes-instance at least half of the random strings are accepted, and for every no-instance none is Goldreich, Section 6.2. Nothing is required on instances outside the promise.

theorem Cslib.Complexity.PromiseProblem.SolvesWithOneSidedError.exists_certificate {α : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {V : α × List Bool → Bool} {Q : PromiseProblem α} (h : SolvesWithOneSidedError enc p V Q) : (∀ a ∈ Q.yes, ∃ (w : List Bool), w.length = Polynomial.eval (enc a).length p ∧ V (a, w) = true) ∧ ∀ a ∈ Q.no, ∀ (w : List Bool), w.length = Polynomial.eval (enc a).length p → V (a, w) = false

A one-sided-error solver for a promise problem is a polynomial-time verifier on the promise: a random string accepted on a yes-instance is a certificate, and no certificate of the right length is accepted on a no-instance.

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

V decides A with one-sided error, using random strings whose length is p evaluated at the length of the encoded instance: it solves the promise problem ofSet A with one-sided error. For every member a of A at least half of the random strings are accepted, and for every non-member none is.

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

The promise problems solved with one-sided error (no false positives on no-instances) by polynomial-time algorithms reading polynomially long random strings Goldreich, Section 6.2.

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

The promise problems solved with one-sided error (no false negatives on yes-instances) by polynomial-time algorithms reading polynomially long random strings: those whose complements are in PromiseRP Goldreich, Section 6.2.

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

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

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

The problems whose complements are in RP Arora and Barak, Section 7.3.

theorem Cslib.Complexity.mem_PromiseRP_iff {α : Type} {enc : α ↪ List Bool} {Q : PromiseProblem α} : Q ∈ PromiseRP enc ↔ ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool ∧ PromiseProblem.SolvesWithOneSidedError enc p V Q

Membership in PromiseRP unfolded to a polynomial coin bound and a polynomial-time one-sided-error solver.

theorem Cslib.Complexity.mem_RP {α : Type} {enc : α ↪ List Bool} {A : Set α} : A ∈ RP enc ↔ ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool ∧ DecidesWithOneSidedError enc p V A

theorem Cslib.Complexity.mem_coRP {α : Type} {enc : α ↪ List Bool} {A : Set α} : A ∈ coRP enc ↔ Aᶜ ∈ RP enc

@[simp]

theorem Cslib.Complexity.ofSet_mem_PromiseRP {α : Type} {enc : α ↪ List Bool} {A : Set α} : PromiseProblem.ofSet A ∈ PromiseRP enc ↔ A ∈ RP enc

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

@[simp]

theorem Cslib.Complexity.ofSet_mem_PromiseCoRP {α : Type} {enc : α ↪ List Bool} {A : Set α} : PromiseProblem.ofSet A ∈ PromiseCoRP enc ↔ A ∈ coRP enc

A decision problem, as a promise problem, is in PromiseCoRP exactly when it is in coRP.

theorem Cslib.Complexity.DecidesWithOneSidedError.isVerifier {α : Type} {enc : α ↪ List Bool} {A : Set α} {p : Polynomial ℕ} {V : α × List Bool → Bool} (h : DecidesWithOneSidedError enc p V A) : IsVerifier enc p V A

A random string accepted by a one-sided-error decider is a certificate: one-sided error gives a verifier.

theorem Cslib.Complexity.PromiseRP_subset_PromiseNP {α : Type} {enc : α ↪ List Bool} : PromiseRP enc ⊆ PromiseNP enc

PromiseRP ⊆ PromiseNP: a random string accepted by a one-sided-error solver is a certificate.

theorem Cslib.Complexity.RP_subset_NP {α : Type} {enc : α ↪ List Bool} : RP enc ⊆ NP enc

RP ⊆ NP: a random string accepted by a one-sided-error decider is a certificate.

theorem Cslib.Complexity.coRP_subset_coNP {α : Type} {enc : α ↪ List Bool} : coRP enc ⊆ coNP enc

coRP ⊆ coNP.

Error reduction

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

V solves the promise problem Q with one-sided error at most 2 ^ (-q(n)), using random strings whose length is p evaluated at the length n of the encoded instance: for every yes-instance the rejected random strings make up at most a 2 ^ (-q(n)) fraction, and for every no-instance none is accepted. Nothing is required on instances outside the promise.

theorem Cslib.Complexity.PromiseProblem.SolvesWithOneSidedError.repeatAny {α : Type} {enc : α ↪ List Bool} {Q : PromiseProblem α} {p : Polynomial ℕ} {V : α × List Bool → Bool} (h : SolvesWithOneSidedError enc p V Q) (q : Polynomial ℕ) : SolvesWithOneSidedErrorExponent enc q (q * p) (Complexity.repeatAny enc q p V) Q

Error reduction for one-sided error: the repetition argument of Arora and Barak, Chapter 7, which the book states for languages, applied to promise problems. The disjunction of q(n) runs of a one-sided-error solver, on independent blocks of random bits, rejects a yes-instance on at most a 2 ^ (-q(n)) fraction of the random strings, and never accepts a no-instance.

theorem Cslib.Complexity.PromiseProblem.SolvesWithOneSidedErrorExponent.solvesWithOneSidedError {α : Type} {enc : α ↪ List Bool} {Q : PromiseProblem α} {q p : Polynomial ℕ} {V : α × List Bool → Bool} (h : SolvesWithOneSidedErrorExponent enc q p V Q) (hq : ∀ (n : ℕ), 1 ≤ Polynomial.eval n q) : SolvesWithOneSidedError enc p V Q

One-sided error at most 2 ^ (-q(n)) ≤ 1 / 2 is one-sided error.

theorem Cslib.Complexity.PromiseProblem.SolvesWithOneSidedErrorExponent.solvesWithErrorExponent {α : Type} {enc : α ↪ List Bool} {Q : PromiseProblem α} {q p : Polynomial ℕ} {V : α × List Bool → Bool} (h : SolvesWithOneSidedErrorExponent enc q p V Q) : SolvesWithErrorExponent enc q p V Q

One-sided error at most 2 ^ (-q(n)) is error at most 2 ^ (-q(n)).

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

V decides A with one-sided error at most 2 ^ (-q(n)), using random strings whose length is p evaluated at the length n of the encoded instance: it solves ofSet A with that error. For every member a of A the rejected random strings make up at most a 2 ^ (-q(n)) fraction, and for every non-member none is accepted.

theorem Cslib.Complexity.mem_PromiseRP_iff_forall_solvesWithOneSidedErrorExponent {α : Type} {enc : α ↪ List Bool} {Q : PromiseProblem α} : Q ∈ PromiseRP enc ↔ ∀ (q : Polynomial ℕ), ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool ∧ PromiseProblem.SolvesWithOneSidedErrorExponent enc q p V Q

Error reduction for PromiseRP, the promise-problem form of the RP error reduction of Arora and Barak, Chapter 7: a promise problem is in PromiseRP exactly when, for every polynomial q, it is solved in polynomial time with one-sided error at most 2 ^ (-q(n)).

theorem Cslib.Complexity.mem_RP_iff_forall_decidesWithOneSidedErrorExponent {α : Type} {enc : α ↪ List Bool} {A : Set α} : A ∈ RP enc ↔ ∀ (q : Polynomial ℕ), ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool ∧ DecidesWithOneSidedErrorExponent enc q p V A

Error reduction for RP Arora and Barak, Chapter 7: a problem is in RP exactly when, for every polynomial q, it is decided in polynomial time with one-sided error at most 2 ^ (-q(n)).

theorem Cslib.Complexity.PromiseRP_subset_PromiseBPP {α : Type} {enc : α ↪ List Bool} : PromiseRP enc ⊆ PromiseBPP enc

PromiseRP ⊆ PromiseBPP, the promise-problem form of RP ⊆ BPP Arora and Barak, Chapter 7: two runs of a one-sided-error solver reject a yes-instance with probability at most 1 / 4.

theorem Cslib.Complexity.PromiseCoRP_subset_PromiseBPP {α : Type} {enc : α ↪ List Bool} : PromiseCoRP enc ⊆ PromiseBPP enc

PromiseCoRP ⊆ PromiseBPP: PromiseBPP is closed under complement.

theorem Cslib.Complexity.RP_subset_BPP {α : Type} {enc : α ↪ List Bool} : RP enc ⊆ BPP enc

RP ⊆ BPP Arora and Barak, Chapter 7: two runs of a one-sided-error decider reject a member with probability at most 1 / 4.

theorem Cslib.Complexity.coRP_subset_BPP {α : Type} {enc : α ↪ List Bool} : coRP enc ⊆ BPP enc

coRP ⊆ BPP: BPP is closed under complement.