The complexity classes RP and coRP
Lax666725.OneSidedError · concepts/Lax666725/OneSidedError.lean · lax-666725
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
A binary language belongs to if a polynomial-time probabilistic machine never accepts a nonmember and accepts each member with probability at least . It belongs to if its complement belongs to .
The success threshold is a standard constant-error convention for ; it gives the same class as the customary threshold . The complement is taken among binary words, not among languages.
Concept map
Lean source view on GitHub
| 1 | import Lax666725.ProbabilisticMachines |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: The complexity classes RP and coRP |
| 6 | type: definition |
| 7 | --- |
| 8 | A binary language belongs to if a polynomial-time |
| 9 | probabilistic machine never accepts a nonmember and accepts each member |
| 10 | with probability at least . It belongs to if its |
| 11 | complement belongs to . |
| 12 | |
| 13 | The success threshold is a standard constant-error convention for |
| 14 | ; it gives the same class as the customary threshold . |
| 15 | The complement is taken among binary words, not among languages. |
| 16 | -/ |
| 17 | |
| 18 | namespace Lax666725.OneSidedError |
| 19 | |
| 20 | open Lax434930.PolynomialTime ProbabilisticMachines |
| 21 | |
| 22 | def 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 | |
| 27 | def coRP : Set Language := {L | Lᶜ ∈ RP} |
| 28 | |
| 29 | end Lax666725.OneSidedError |
| 30 |
Builds on
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments