Randomized complexity classes

This file defines the randomized complexity classes BPP, RP, coRP, ZPP, and PP, along with the time-parameterized classes BPTIME, RTIME, and PPTIME, and the predicate NTM.IsPPT.

A PTM (probabilistic Turing machine) is an NTM where the two transition functions are selected uniformly at random. Acceptance probability is defined via NTM.acceptProb.

Helper predicates

The acceptance-probability conditions shared across classes are factored into NTM.AcceptsWithProb (lower-bounding acceptance on yes-instances) and NTM.RejectsWithProb (upper-bounding acceptance on no-instances).

def Complexity.NTM.AcceptsWithProb {n : ℕ} (tm : NTM n) (L : Language) (T : ℕ → ℕ) (c : ℚ) : Prop

The PTM accepts every x ∈ L with probability at least c within T(|x|) steps.

Equations

• tm.AcceptsWithProb L T c = ∀ x ∈ L, tm.acceptProb x (T x.length) ≥ c

def Complexity.NTM.RejectsWithProb {n : ℕ} (tm : NTM n) (L : Language) (T : ℕ → ℕ) (s : ℚ) : Prop

The PTM accepts every x ∉ L with probability at most s within T(|x|) steps.

Equations

• tm.RejectsWithProb L T s = ∀ x ∉ L, tm.acceptProb x (T x.length) ≤ s

def Complexity.NTM.IsPPT {n : ℕ} (tm : NTM n) : Prop

An NTM is probabilistic polynomial-time (PPT) if there exist a time bound f and degree d such that every computation path halts within f(|x|) steps and f(n) = O(n^d). This is the central notion in cryptographic security definitions.

Equations

• tm.IsPPT = ∃ (f : ℕ → ℕ) (d : ℕ), tm.AllPathsHaltIn f ∧ Complexity.BigO f fun (x : ℕ) => x ^ d

def Complexity.BPTIME (T : ℕ → ℕ) : Set Language

BPTIME(T) is the class of languages decidable by a PTM in time O(T(n)) with two-sided bounded error (accept probability ≥ 2/3 on yes-instances, ≤ 1/3 on no-instances).

Equations

• One or more equations did not get rendered due to their size.

def Complexity.BPP : Set Language

BPP is the class of languages decidable by a PTM in polynomial time with two-sided bounded error: BPP = ⋃_k BPTIME(n^k).

Equations

• Complexity.BPP = ⋃ (k : ℕ), Complexity.BPTIME fun (x : ℕ) => x ^ k

def Complexity.RTIME (T : ℕ → ℕ) : Set Language

RTIME(T) is the class of languages decidable by a PTM in time O(T(n)) with one-sided error: yes-instances accepted with probability ≥ 1/2, no-instances never accepted (accept probability 0).

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RP : Set Language

RP is the class of languages decidable by a PTM in polynomial time with one-sided error: RP = ⋃_k RTIME(n^k).

Equations

• Complexity.RP = ⋃ (k : ℕ), Complexity.RTIME fun (x : ℕ) => x ^ k

def Complexity.coRP : Set Language

coRP is the class of languages whose complements are in RP. Equivalently: yes-instances always accepted (probability 1), no-instances accepted with probability ≤ 1/2.

Equations

• Complexity.coRP = Complexity.complClass Complexity.RP

def Complexity.ZPP : Set Language

ZPP (zero-error probabilistic polynomial time) is RP ∩ coRP. A language is in ZPP iff it has a PTM with zero-error expected polynomial running time.

Equations

• Complexity.ZPP = Complexity.RP ∩ Complexity.coRP

def Complexity.PPTIME (T : ℕ → ℕ) : Set Language

PPTIME(T) is the class of languages decidable by a PTM in time O(T(n)) with unbounded error: x ∈ L iff the PTM accepts with probability strictly greater than 1/2.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.PP : Set Language

PP (probabilistic polynomial time) is the class of languages decidable by a PTM in polynomial time with unbounded error: PP = ⋃_k PPTIME(n^k).

Equations

• Complexity.PP = ⋃ (k : ℕ), Complexity.PPTIME fun (x : ℕ) => x ^ k