Documentation

Complexity.Computability.Complexity.Classes.Promise.Randomized

Randomized reductions with one-sided error on promise problems #

For randomized hardness results in metacomplexity Ilango, Section 2, p. 34:11, Ilango, Loff and Oliveira, Section 4.2, Lemmas 15–16, pp. 22:20–22:23, Hirahara, ECCC TR22-119, Lemma 8.3, p. 26 and Theorem 8.5, pp. 30–31, a randomized polynomial-time many-one reduction with one-sided error (PromiseProblem.RPReducible, and the threshold-indexed generalization PromiseProblem.RPReducibleWithError) is a uniform strict PPT program R : α → ProbComp β that maps every yes-instance of X exclusively into Y.yes and maps every no-instance of X into Y.no with probability at least 2 / 3 (or s a).

Following the terminology of Ilango, Section 2, p. 34:11, RPReducible errs only on no-instances (the coRP error orientation): in metacomplexity reductions, upper bounds on circuit or Kolmogorov complexity hold deterministically for every random choice on yes-instances while lower bounds on no-instances hold with high probability. Consequently, PromiseCoRP and PromiseBPP are closed under RPReducible (PromiseProblem.RPReducible.mem_PromiseCoRP, PromiseProblem.RPReducible.mem_PromiseBPP, PromiseProblem.NP_subset_coRP_of_forall_rpReducible, PromiseProblem.NP_subset_BPP_of_forall_rpReducible), whereas the dual RP error orientation (zero error on no-instances, bounded error on yes-instances, as in [Valiant and Vazirani, pp. 86–87] [VV86]) is expressed via promise-problem complement as RPReducibleWithError encA encB s Xᶜ Yᶜ (PromiseProblem.rpReducibleWithError_compl_iff, PromiseProblem.RPReducible.mem_PromiseRP_of_compl).

Because outer measures are non-negative, the soundness inequality in RPReducibleWithError holds vacuously at any no-instance a with s a ≤ 0; in particular, the additive composition lemma PromiseProblem.RPReducibleWithError.trans_add (which produces threshold s₁ a + s₂ - 1) gives a non-trivial soundness bound at a only when 1 < s₁ a + s₂.

Main definitions #

Main results #

References #

Randomized reductions with one-sided error #

source
def Cslib.Complexity.PromiseProblem.RPReducibleWithError {α β : Type} (encA : α ↪ List Bool) (encB : β ↪ List Bool) (s : α → ℝ) (X : PromiseProblem α) (Y : PromiseProblem β) :
Prop

A randomized polynomial-time many-one reduction with one-sided error and soundness threshold s : α → ℝ from a promise problem X to a promise problem Y (library generalization of the fixed-threshold reduction of Ilango, Section 2, p. 34:11 to support general constant or subconstant soundness thresholds as in Ilango, Loff and Oliveira, Section 4.2, Lemmas 15–16, pp. 22:20–22:23 and Hirahara, ECCC TR22-119, Lemma 8.3, p. 26 and Theorem 8.5, pp. 30–31): a uniform strict PPT program R : α → ProbComp β such that:

  • Completeness (no false negatives on X.yes): for every a ∈ X.yes, every supported output of R a lies in Y.yes;
  • Soundness (s a on X.no): for every a ∈ X.no, R a outputs an instance in Y.no with probability at least s a.

This is the coRP error orientation (error only on no-instances); the dual RP error orientation (error only on yes-instances) is RPReducibleWithError encA encB s Xᶜ Yᶜ (rpReducibleWithError_compl_iff). Because outer measures are non-negative, the soundness condition at a ∈ X.no holds vacuously whenever s a ≤ 0. Instances outside X.yes ∪ X.no are unconstrained.

Instances For
    source
    @[reducible, inline]
    abbrev Cslib.Complexity.PromiseProblem.RPReducible {α β : Type} (encA : α ↪ List Bool) (encB : β ↪ List Bool) (X : PromiseProblem α) (Y : PromiseProblem β) :
    Prop

    A randomized polynomial-time many-one reduction with one-sided error from a promise problem X to a promise problem Y, with the standard soundness threshold 2 / 3 Ilango, Section 2, p. 34:11: a uniform strict PPT program R : α → ProbComp β mapping every yes-instance of X exclusively into Y.yes and mapping every no-instance of X into Y.no with probability at least 2 / 3. Following [Ila20a], this has one-sided error on no-instances (coRP orientation); see RPReducible.mem_PromiseCoRP and rpReducibleWithError_compl_iff.

    Instances For
      source
      theorem Cslib.Complexity.PromiseProblem.rpReducibleWithError_iff_probability {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {X : PromiseProblem α} {Y : PromiseProblem β} {s : α → ℝ} [DecidablePred fun (x : β) => x ∈ Y.no] :
      RPReducibleWithError encA encB s X Y ↔ ∃ (R : α → ProbComp β), Probability.IsPPTOn encA encB R ∧ (∀ a ∈ X.yes, ∀ b ∈ (R a).eval.support, b ∈ Y.yes) ∧ ∀ a ∈ X.no, s a ≤ (((fun (b : β) => decide (b ∈ Y.no)) <$> R a).eval true).toReal

      Characterization of RPReducibleWithError using the Pr[...] event notation.

      source
      theorem Cslib.Complexity.PromiseProblem.rpReducible_iff_probability {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {X : PromiseProblem α} {Y : PromiseProblem β} [DecidablePred fun (x : β) => x ∈ Y.no] :
      RPReducible encA encB X Y ↔ ∃ (R : α → ProbComp β), Probability.IsPPTOn encA encB R ∧ (∀ a ∈ X.yes, ∀ b ∈ (R a).eval.support, b ∈ Y.yes) ∧ ∀ a ∈ X.no, 2 / 3 ≤ (((fun (b : β) => decide (b ∈ Y.no)) <$> R a).eval true).toReal

      Characterization of RPReducible using the Pr[...] event notation.

      source
      theorem Cslib.Complexity.PromiseProblem.rpReducibleWithError_iff_toOuterMeasure_eq_one {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {X : PromiseProblem α} {Y : PromiseProblem β} {s : α → ℝ} :
      RPReducibleWithError encA encB s X Y ↔ ∃ (R : α → ProbComp β), Probability.IsPPTOn encA encB R ∧ (∀ a ∈ X.yes, ((R a).eval.toOuterMeasure Y.yes).toReal = 1) ∧ ∀ a ∈ X.no, s a ≤ ((R a).eval.toOuterMeasure Y.no).toReal

      Equivalence of support-based completeness and probability-one completeness for RPReducibleWithError.

      source
      theorem Cslib.Complexity.PromiseProblem.rpReducible_iff_toOuterMeasure_eq_one {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {X : PromiseProblem α} {Y : PromiseProblem β} :
      RPReducible encA encB X Y ↔ ∃ (R : α → ProbComp β), Probability.IsPPTOn encA encB R ∧ (∀ a ∈ X.yes, ((R a).eval.toOuterMeasure Y.yes).toReal = 1) ∧ ∀ a ∈ X.no, 2 / 3 ≤ ((R a).eval.toOuterMeasure Y.no).toReal

      Equivalence of support-based completeness and probability-one completeness for RPReducible Ilango, Section 2, p. 34:11.

      source
      theorem Cslib.Complexity.PromiseProblem.RPReducibleWithError.mono {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {X : PromiseProblem α} {Y : PromiseProblem β} {s₁ s₂ : α → ℝ} (h : RPReducibleWithError encA encB s₁ X Y) (hs : ∀ a ∈ X.no, s₂ a ≤ s₁ a) :
      RPReducibleWithError encA encB s₂ X Y

      Lowering the soundness threshold preserves RPReducibleWithError.

      source
      theorem Cslib.Complexity.PromiseProblem.rpReducibleWithError_compl_iff {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {X : PromiseProblem α} {Y : PromiseProblem β} {s : α → ℝ} :
      RPReducibleWithError encA encB s Xᶜ Yᶜ ↔ ∃ (R : α → ProbComp β), Probability.IsPPTOn encA encB R ∧ (∀ a ∈ X.no, ∀ b ∈ (R a).eval.support, b ∈ Y.no) ∧ ∀ a ∈ X.yes, s a ≤ ((R a).eval.toOuterMeasure Y.yes).toReal

      Complement-duality identity for RPReducibleWithError (library identity): a randomized reduction between the complement promise problems Xᶜ and Yᶜ with threshold s is a randomized reduction from X to Y in the dual one-sided error orientation, mapping no-instances exclusively into Y.no and mapping yes-instances into Y.yes with probability at least s a. When s a is an inverse-polynomial threshold such as 1 / (4 * n), this represents the unamplified one-sided orientation of Valiant and Vazirani [Valiant and Vazirani, Section 1, Theorem 1.1, pp. 86–87] [VV86], Goldreich, Section 6.2.

      source
      theorem Cslib.Complexity.PromiseProblem.rpReducible_iff_exists_seeded {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {X : PromiseProblem α} {Y : PromiseProblem β} :
      RPReducible encA encB X Y ↔ ∃ (p : Polynomial ℕ) (f : α × List Bool → β), Turing.MultiTapeTM.ComputableInPolyTime f (Turing.MultiTapeTM.encPair encA Turing.MultiTapeTM.encBits) encB ∧ (∀ a ∈ X.yes, ∀ (r : Fin (Polynomial.eval (encA a).length p) → Bool), f (a, List.ofFn r) ∈ Y.yes) ∧ ∀ a ∈ X.no, 2 * 2 ^ Polynomial.eval (encA a).length p ≤ 3 * {r : Fin (Polynomial.eval (encA a).length p) → Bool | f (a, List.ofFn r) ∈ Y.no}.card

      Seeded-function characterization of RPReducible Ilango, Section 2, p. 34:11: X is RPReducible to Y if and only if there are a polynomial p and a function f : α × List Bool → β, computable in polynomial time with respect to encPair encA encBits and encB, such that for every a ∈ X.yes and every random string r of length p(|a|) we have f(a, r) ∈ Y.yes, and for every a ∈ X.no at least two thirds of the random strings r of length p(|a|) satisfy f(a, r) ∈ Y.no.

      Lifting deterministic reductions and structural closure #

      source
      theorem Cslib.Complexity.PromiseProblem.PolyTimeReducible.rpReducibleWithError {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {X : PromiseProblem α} {Y : PromiseProblem β} (h : PolyTimeReducible encA encB X Y) :
      RPReducibleWithError encA encB (fun (x : α) => 1) X Y

      Every deterministic polynomial-time reduction of promise problems lifts to a randomized reduction with soundness 1 (zero error).

      source
      theorem Cslib.Complexity.PromiseProblem.PolyTimeReducible.rpReducible {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {X : PromiseProblem α} {Y : PromiseProblem β} (h : PolyTimeReducible encA encB X Y) :
      RPReducible encA encB X Y

      Every deterministic polynomial-time reduction of promise problems is a randomized one-sided reduction (RPReducible).

      source
      theorem Cslib.Complexity.PolyTimeReducible.rpReducible_ofSet {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {A : Set α} {B : Set β} (h : PolyTimeReducible encA encB A B) :
      PromiseProblem.RPReducible encA encB (PromiseProblem.ofSet A) (PromiseProblem.ofSet B)

      Every deterministic polynomial-time reduction between decision problems gives an RPReducible reduction between their promise problems.

      source
      theorem Cslib.Complexity.PromiseProblem.RPReducibleWithError.refl {α : Type} (encA : α ↪ List Bool) (X : PromiseProblem α) :
      RPReducibleWithError encA encA (fun (x : α) => 1) X X

      Every promise problem reduces to itself by a zero-error randomized reduction.

      source
      theorem Cslib.Complexity.PromiseProblem.RPReducible.refl {α : Type} (encA : α ↪ List Bool) (X : PromiseProblem α) :
      RPReducible encA encA X X

      Every promise problem is RPReducible to itself.

      source
      theorem Cslib.Complexity.PromiseProblem.RPReducibleWithError.of_subset {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {X : PromiseProblem α} {Y Y' : PromiseProblem β} {s : α → ℝ} (h : RPReducibleWithError encA encB s X Y) (hyes : Y.yes ⊆ Y'.yes) (hno : Y.no ⊆ Y'.no) :
      RPReducibleWithError encA encB s X Y'

      Enlarging the target promise preserves RPReducibleWithError.

      source
      theorem Cslib.Complexity.PromiseProblem.RPReducible.of_subset {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {X : PromiseProblem α} {Y Y' : PromiseProblem β} (h : RPReducible encA encB X Y) (hyes : Y.yes ⊆ Y'.yes) (hno : Y.no ⊆ Y'.no) :
      RPReducible encA encB X Y'

      Enlarging the target promise preserves RPReducible.

      source
      theorem Cslib.Complexity.PromiseProblem.RPReducibleWithError.trans {α β γ : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {X : PromiseProblem α} {Y : PromiseProblem β} {Z : PromiseProblem γ} {s₁ : α → ℝ} {s₂ : ℝ} (hXY : RPReducibleWithError encA encB s₁ X Y) (hYZ : RPReducibleWithError encB encC (fun (x : β) => s₂) Y Z) (hs₂ : 0 ≤ s₂) :
      RPReducibleWithError encA encC (fun (a : α) => s₁ a * s₂) X Z

      Composition of randomized one-sided reductions (multiplicative soundness, library lemma): composing a reduction from X to Y with soundness s₁ a and a reduction from Y to Z with uniform soundness s₂ yields a reduction from X to Z with soundness s₁ a * s₂.

      source
      theorem Cslib.Complexity.PromiseProblem.RPReducibleWithError.trans_add {α β γ : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {X : PromiseProblem α} {Y : PromiseProblem β} {Z : PromiseProblem γ} {s₁ : α → ℝ} {s₂ : ℝ} (hXY : RPReducibleWithError encA encB s₁ X Y) (hYZ : RPReducibleWithError encB encC (fun (x : β) => s₂) Y Z) (hs₂ : s₂ ≤ 1) :
      RPReducibleWithError encA encC (fun (a : α) => s₁ a + s₂ - 1) X Z

      Composition of randomized one-sided reductions (additive error accounting, library lemma): composing a reduction from X to Y with soundness s₁ a (error 1 - s₁ a) and a reduction from Y to Z with soundness s₂ (error 1 - s₂) yields a reduction from X to Z with soundness s₁ a + s₂ - 1. Note that when s₁ a + s₂ ≤ 1, the resulting threshold s₁ a + s₂ - 1 ≤ 0 holds vacuously by non-negativity of outer measure.

      source
      theorem Cslib.Complexity.PromiseProblem.RPReducibleWithError.of_computableInPolyTime {α β γ : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {X : PromiseProblem α} {Y : PromiseProblem β} {Z : PromiseProblem γ} {s : β → ℝ} {f : α → β} (hf : Turing.MultiTapeTM.ComputableInPolyTime f encA encB) (hyes : Set.MapsTo f X.yes Y.yes) (hno : Set.MapsTo f X.no Y.no) (hYZ : RPReducibleWithError encB encC s Y Z) :
      RPReducibleWithError encA encC (fun (a : α) => s (f a)) X Z

      Precomposing an RPReducibleWithError reduction with an explicit deterministic polynomial-time reduction f from X to Y pulls back its soundness threshold along f.

      source
      theorem Cslib.Complexity.PromiseProblem.PolyTimeReducible.trans_rpReducibleWithError {α β γ : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {X : PromiseProblem α} {Y : PromiseProblem β} {Z : PromiseProblem γ} {s : ℝ} (hXY : PolyTimeReducible encA encB X Y) (hYZ : RPReducibleWithError encB encC (fun (x : β) => s) Y Z) :
      RPReducibleWithError encA encC (fun (x : α) => s) X Z

      Precomposing an RPReducibleWithError reduction at a uniform threshold with a deterministic polynomial-time reduction preserves its soundness threshold. Because PolyTimeReducible existentially quantifies over the reduction function f, the output threshold cannot refer to f a; for an instance-dependent threshold fun a => s (f a), use RPReducibleWithError.of_computableInPolyTime with an explicit f.

      source
      theorem Cslib.Complexity.PromiseProblem.RPReducibleWithError.trans_polyTimeReducible {α β γ : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {X : PromiseProblem α} {Y : PromiseProblem β} {Z : PromiseProblem γ} {s : α → ℝ} (hXY : RPReducibleWithError encA encB s X Y) (hYZ : PolyTimeReducible encB encC Y Z) :
      RPReducibleWithError encA encC s X Z

      Postcomposing an RPReducibleWithError reduction with a deterministic polynomial-time reduction preserves its soundness threshold.

      source
      theorem Cslib.Complexity.PromiseProblem.PolyTimeReducible.trans_rpReducible {α β γ : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {X : PromiseProblem α} {Y : PromiseProblem β} {Z : PromiseProblem γ} (hXY : PolyTimeReducible encA encB X Y) (hYZ : RPReducible encB encC Y Z) :
      RPReducible encA encC X Z

      Precomposing an RPReducible reduction with a deterministic polynomial-time reduction yields an RPReducible reduction.

      source
      theorem Cslib.Complexity.PromiseProblem.RPReducible.trans_polyTimeReducible {α β γ : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {X : PromiseProblem α} {Y : PromiseProblem β} {Z : PromiseProblem γ} (hXY : RPReducible encA encB X Y) (hYZ : PolyTimeReducible encB encC Y Z) :
      RPReducible encA encC X Z

      Postcomposing an RPReducible reduction with a deterministic polynomial-time reduction yields an RPReducible reduction.

      Closure of PromiseCoRP, PromiseBPP and PromiseRP under RPReducible #

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

      PromiseCoRP is closed under RPReducible (library lemma): if X reduces to Y by a randomized one-sided reduction and Y ∈ PromiseCoRP encB, then X ∈ PromiseCoRP encA.

      source
      theorem Cslib.Complexity.PromiseProblem.RPReducible.mem_PromiseCoRP_of_mem_PromiseP {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {X : PromiseProblem α} {Y : PromiseProblem β} (hXY : RPReducible encA encB X Y) (hY : Y ∈ PromiseP encB) :
      X ∈ PromiseCoRP encA

      If X is RPReducible to Y and Y ∈ PromiseP encB, then X ∈ PromiseCoRP encA.

      source
      theorem Cslib.Complexity.PromiseProblem.RPReducible.mem_coRP_of_ofSet {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {Y : PromiseProblem β} {A : Set α} (hAY : RPReducible encA encB (ofSet A) Y) (hY : Y ∈ PromiseCoRP encB) :
      A ∈ coRP encA

      If a decision problem A is RPReducible to Y and Y ∈ PromiseCoRP encB, then A ∈ coRP encA.

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

      PromiseBPP is closed under RPReducible (library lemma; on the promise classes of Goldreich, Definition 1.2, amplifying as in Sipser, Lemma 10.5): if X reduces to Y by a randomized one-sided reduction and Y ∈ PromiseBPP encB, then X ∈ PromiseBPP encA.

      source
      theorem Cslib.Complexity.PromiseProblem.RPReducible.mem_BPP_of_ofSet {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {Y : PromiseProblem β} {A : Set α} (hAY : RPReducible encA encB (ofSet A) Y) (hY : Y ∈ PromiseBPP encB) :
      A ∈ BPP encA

      If a decision problem A is RPReducible to Y and Y ∈ PromiseBPP encB, then A ∈ BPP encA.

      source
      theorem Cslib.Complexity.PromiseProblem.RPReducible.mem_PromiseRP_of_compl {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {X : PromiseProblem α} {Y : PromiseProblem β} (hXY : RPReducible encA encB Xᶜ Yᶜ) (hY : Y ∈ PromiseRP encB) :
      X ∈ PromiseRP encA

      PromiseRP is closed under dual (Xᶜ to Yᶜ) RPReducible reductions (library lemma).

      source
      theorem Cslib.Complexity.PromiseProblem.RPReducible.mem_PromiseBPP_of_compl {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {X : PromiseProblem α} {Y : PromiseProblem β} (hXY : RPReducible encA encB Xᶜ Yᶜ) (hY : Y ∈ PromiseBPP encB) :
      X ∈ PromiseBPP encA

      PromiseBPP is closed under dual (Xᶜ to Yᶜ) RPReducible reductions.

      source
      theorem Cslib.Complexity.PromiseProblem.RPReducible.mem_RP_of_compl_ofSet {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {Y : PromiseProblem β} {A : Set α} (hAY : RPReducible encA encB (ofSet A)ᶜ Yᶜ) (hY : Y ∈ PromiseRP encB) :
      A ∈ RP encA

      If a decision problem A reduces to Y in the dual one-sided error orientation (RPReducible encA encB (ofSet A)ᶜ Yᶜ) and Y ∈ PromiseRP encB, then A ∈ RP encA.

      source
      theorem Cslib.Complexity.PromiseProblem.NP_subset_coRP_of_forall_rpReducible {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {Y : PromiseProblem β} (hHard : ∀ A ∈ NP encA, RPReducible encA encB (ofSet A) Y) (hY : Y ∈ PromiseCoRP encB) :
      NP encA ⊆ coRP encA

      If every problem in NP encA reduces to Y via RPReducible and Y ∈ PromiseCoRP encB, then NP encA ⊆ coRP encA (library lemma).

      source
      theorem Cslib.Complexity.PromiseProblem.NP_subset_BPP_of_forall_rpReducible {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {Y : PromiseProblem β} (hHard : ∀ A ∈ NP encA, RPReducible encA encB (ofSet A) Y) (hY : Y ∈ PromiseBPP encB) :
      NP encA ⊆ BPP encA

      If every problem in NP encA reduces to Y via RPReducible and Y ∈ PromiseBPP encB, then NP encA ⊆ BPP encA (library lemma).