Probabilistic classes of promise problems

The probabilistic promise classes PromiseBPP, PromiseRP and PromiseCoRP, defined in CslibFrontier.Computability.Complexity.Classes.BPP and CslibFrontier.Computability.Complexity.Classes.RP together with the error conditions they share with BPP, RP and coRP, follow Goldreich's semantic definitions Goldreich, Definition 1.2 and Section 6.2, requiring bounded or one-sided error only on instances in the promise. They contain the lifted classes promiseClass (BPP enc), promiseClass (RP enc) and promiseClass (coRP enc).

Each class is equivalent to its uniform strict PPT program characterization (mem_PromiseBPP_iff_exists_isPPTOn, mem_PromiseRP_iff_exists_isPPTOn, mem_PromiseCoRP_iff_exists_isPPTOn) via saved-coin replay (IsPPTOn.exists_seeded_evaluator, IsPPTOn.exists_total_seeded_evaluator), and is closed under deterministic polynomial-time promise reductions (PromiseProblem.PolyTimeReducible.mem_PromiseBPP, PromiseProblem.PolyTimeReducible.mem_PromiseRP, PromiseProblem.PolyTimeReducible.mem_PromiseCoRP).

Main results

• Cslib.Complexity.mem_PromiseCoRP_iff: a seeded-verifier characterization of PromiseCoRP.
• Cslib.Complexity.promiseClass_BPP_subset_PromiseBPP, Cslib.Complexity.promiseClass_RP_subset_PromiseRP, Cslib.Complexity.promiseClass_coRP_subset_PromiseCoRP: inclusion of the lifts of BPP, RP and coRP.
• Cslib.Complexity.compl_mem_PromiseRP_iff, Cslib.Complexity.compl_mem_PromiseCoRP_iff: complement relations between PromiseRP and PromiseCoRP.
• Cslib.Complexity.PromiseP_subset_PromiseRP, Cslib.Complexity.PromiseP_subset_PromiseCoRP, Cslib.Complexity.PromiseP_subset_PromiseBPP.
• Cslib.Complexity.probability_sampleList_verifier: acceptance probability of sampling a uniform random word for a seeded verifier.
• Cslib.Complexity.mem_PromiseBPP_iff_exists_isPPTOn, Cslib.Complexity.mem_PromiseRP_iff_exists_isPPTOn, Cslib.Complexity.mem_PromiseCoRP_iff_exists_isPPTOn: characterizations by uniform strict PPT programs.
• Cslib.Complexity.PromiseProblem.PolyTimeReducible.mem_PromiseBPP, Cslib.Complexity.PromiseProblem.PolyTimeReducible.mem_PromiseRP, Cslib.Complexity.PromiseProblem.PolyTimeReducible.mem_PromiseCoRP: closure of probabilistic promise classes under deterministic polynomial-time reductions.

References

• O. Goldreich, On promise problems: a survey

theorem Cslib.Complexity.mem_PromiseCoRP_iff {α : Type} {enc : α ↪ List Bool} {Q : PromiseProblem α} : Q ∈ PromiseCoRP enc ↔ ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool ∧ (∀ a ∈ Q.yes, ∀ (r : Fin (Polynomial.eval (enc a).length p) → Bool), V (a, List.ofFn r) = true) ∧ ∀ a ∈ Q.no, 2 ^ Polynomial.eval (enc a).length p ≤ 2 * {r : Fin (Polynomial.eval (enc a).length p) → Bool | V (a, List.ofFn r) = false}.card

A promise problem is in PromiseCoRP when a polynomial-time verifier accepts every random string on every yes-instance and rejects at least half on every no-instance.

theorem Cslib.Complexity.promiseClass_BPP_subset_PromiseBPP {α : Type} {enc : α ↪ List Bool} : promiseClass (BPP enc) ⊆ PromiseBPP enc

Every promise problem separated by a language in BPP is in PromiseBPP.

theorem Cslib.Complexity.promiseClass_RP_subset_PromiseRP {α : Type} {enc : α ↪ List Bool} : promiseClass (RP enc) ⊆ PromiseRP enc

Every promise problem separated by a language in RP is in PromiseRP.

theorem Cslib.Complexity.promiseClass_coRP_subset_PromiseCoRP {α : Type} {enc : α ↪ List Bool} : promiseClass (coRP enc) ⊆ PromiseCoRP enc

Every promise problem separated by a language in coRP is in PromiseCoRP.

theorem Cslib.Complexity.compl_mem_PromiseRP_iff {α : Type} {enc : α ↪ List Bool} {Q : PromiseProblem α} : Qᶜ ∈ PromiseRP enc ↔ Q ∈ PromiseCoRP enc

A promise problem's complement is in PromiseRP exactly when the problem is in PromiseCoRP.

theorem Cslib.Complexity.compl_mem_PromiseCoRP_iff {α : Type} {enc : α ↪ List Bool} {Q : PromiseProblem α} : Qᶜ ∈ PromiseCoRP enc ↔ Q ∈ PromiseRP enc

A promise problem's complement is in PromiseCoRP exactly when the problem is in PromiseRP.

theorem Cslib.Complexity.PromiseP_subset_PromiseRP {α : Type} {enc : α ↪ List Bool} : PromiseP enc ⊆ PromiseRP enc

Every promise problem in PromiseP is in PromiseRP.

theorem Cslib.Complexity.PromiseP_subset_PromiseCoRP {α : Type} {enc : α ↪ List Bool} : PromiseP enc ⊆ PromiseCoRP enc

Every promise problem in PromiseP is in PromiseCoRP.

theorem Cslib.Complexity.PromiseP_subset_PromiseBPP {α : Type} {enc : α ↪ List Bool} : PromiseP enc ⊆ PromiseBPP enc

Every promise problem in PromiseP is in PromiseBPP.

theorem Cslib.Complexity.probability_sampleList_verifier {α : Type} (V : α × List Bool → Bool) (a : α) (n : ℕ) : (((fun (w : List Bool) => V (a, w)) <$> BitString.sampleList n).eval true).toReal = ↑(acceptCount V a n) / 2 ^ n

The program sampling a random string for a seeded verifier accepts with the accepted fraction of the strings.

theorem Cslib.Complexity.mem_PromiseBPP_iff_exists_isPPTOn {α : Type} {enc : α ↪ List Bool} {Q : PromiseProblem α} : Q ∈ PromiseBPP enc ↔ ∃ (M : α → ProbComp Bool), Probability.IsPPTOn enc Turing.MultiTapeTM.encBool M ∧ (∀ a ∈ Q.yes, 2 / 3 ≤ ((M a).eval true).toReal) ∧ ∀ a ∈ Q.no, 2 / 3 ≤ ((not <$> M a).eval true).toReal

Probabilistic-program characterization of PromiseBPP: a promise problem is in PromiseBPP exactly when a uniform strict PPT Boolean program accepts every yes-instance with probability at least 2 / 3 and rejects every no-instance with probability at least 2 / 3.

theorem Cslib.Complexity.mem_PromiseRP_iff_exists_isPPTOn {α : Type} {enc : α ↪ List Bool} {Q : PromiseProblem α} : Q ∈ PromiseRP enc ↔ ∃ (M : α → ProbComp Bool), Probability.IsPPTOn enc Turing.MultiTapeTM.encBool M ∧ (∀ a ∈ Q.yes, 1 / 2 ≤ ((M a).eval true).toReal) ∧ ∀ a ∈ Q.no, true ∉ (M a).eval.support

Probabilistic-program characterization of PromiseRP: a promise problem is in PromiseRP exactly when a uniform strict PPT Boolean program accepts every yes-instance with probability at least 1 / 2 and never accepts a no-instance.

theorem Cslib.Complexity.mem_PromiseCoRP_iff_exists_isPPTOn {α : Type} {enc : α ↪ List Bool} {Q : PromiseProblem α} : Q ∈ PromiseCoRP enc ↔ ∃ (M : α → ProbComp Bool), Probability.IsPPTOn enc Turing.MultiTapeTM.encBool M ∧ (∀ a ∈ Q.yes, false ∉ (M a).eval.support) ∧ ∀ a ∈ Q.no, 1 / 2 ≤ ((not <$> M a).eval true).toReal

Probabilistic-program characterization of PromiseCoRP: a promise problem is in PromiseCoRP exactly when a uniform strict PPT Boolean program never rejects a yes-instance and rejects every no-instance with probability at least 1 / 2.

theorem Cslib.Complexity.PromiseProblem.PolyTimeReducible.mem_PromiseBPP {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {X : PromiseProblem α} {Y : PromiseProblem β} (h : PolyTimeReducible encA encB X Y) (hY : Y ∈ PromiseBPP encB) : X ∈ PromiseBPP encA

PromiseBPP is closed under polynomial-time reductions.

theorem Cslib.Complexity.PromiseProblem.PolyTimeReducible.mem_PromiseRP {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {X : PromiseProblem α} {Y : PromiseProblem β} (h : PolyTimeReducible encA encB X Y) (hY : Y ∈ PromiseRP encB) : X ∈ PromiseRP encA

PromiseRP is closed under polynomial-time reductions.

theorem Cslib.Complexity.PromiseProblem.PolyTimeReducible.mem_PromiseCoRP {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {X : PromiseProblem α} {Y : PromiseProblem β} (h : PolyTimeReducible encA encB X Y) (hY : Y ∈ PromiseCoRP encB) : X ∈ PromiseCoRP encA

PromiseCoRP is closed under polynomial-time reductions.