The complexity classes RP and coRP

Lax666725.OneSidedError · concepts/Lax666725/OneSidedError.lean · lax-666725

definition

Loading review…

Sign in with ORCID

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    A binary language belongs to RP\mathrm{RP} if a polynomial-time probabilistic machine never accepts a nonmember and accepts each member with probability at least 2/32/3. It belongs to coRP\mathrm{coRP} if its complement belongs to RP\mathrm{RP}.

    The success threshold 2/32/3 is a standard constant-error convention for RP\mathrm{RP}; it gives the same class as the customary threshold 1/21/2. The complement is taken among binary words, not among languages.

    Concept map
    3 concepts; 2 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax666725.ProbabilisticMachines
    2
    3/-!
    4---
    5title: The complexity classes RP and coRP
    6type: definition
    7---
    8A binary language belongs to RP\mathrm{RP} if a polynomial-time
    9probabilistic machine never accepts a nonmember and accepts each member
    10with probability at least 2/32/3. It belongs to coRP\mathrm{coRP} if its
    11complement belongs to RP\mathrm{RP}.
    12
    13The success threshold 2/32/3 is a standard constant-error convention for
    14RP\mathrm{RP}; it gives the same class as the customary threshold 1/21/2.
    15The complement is taken among binary words, not among languages.
    16-/
    17
    18namespace Lax666725.OneSidedError
    19
    20open Lax434930.PolynomialTime ProbabilisticMachines
    21
    22def RP : Set Language :=
    23 {L | ∃ A : Procedure Bool, ∀ x,
    24 (∀ r, A.eval x r = true → x ∈ L) ∧
    25 (x ∈ L → (2 / 3 : ℚ) ≤ A.probability x (fun b => b = true))}
    26
    27def coRP : Set Language := {L | Lᶜ ∈ RP}
    28
    29end Lax666725.OneSidedError
    30

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…