Almost-wide probabilistic polynomial time

We use the constant-error, power-of-two characterization of AWPP from Fenner: a GapP function divided by 2 ^ p(n) lies in [2/3, 1] on members and [0, 1/3] on nonmembers. Integer inequalities avoid division and rounding. The counting functions are verifier-based. Uniform error reduction is proved in Complexity/Computability/Complexity/Classes/AWPP/Amplification.lean, and PP-lowness for the strict adaptive oracle-verifier model in Complexity/Computability/Complexity/Classes/AWPP/Lowness.lean.

Main definitions

• AWPP: bounded-error GapP ratios with a length-dependent dyadic denominator.

Main results

• BPP_subset_AWPP, SPP_subset_AWPP, AWPP_subset_PP.
• compl_mem_AWPP, PolyTimeReducible.mem_AWPP: complement and reduction closure.
• mem_AWPP_of_polyTime_exponent: padding input-dependent dyadic denominators.

References

• S. Fenner, PP-Lowness and a Simple Definition of AWPP

def Cslib.Complexity.AWPP {α : Type} (enc : α ↪ List Bool) : Set (Set α)

A GapP ratio in [0, 1], at least 2/3 on members and at most 1/3 otherwise, Fenner's characterization of AWPP Fenner.

theorem Cslib.Complexity.BPP_subset_AWPP {α : Type} {enc : α ↪ List Bool} : BPP enc ⊆ AWPP enc

Acceptance counts are GapP functions, so bounded-error computation gives an AWPP ratio.

theorem Cslib.Complexity.SPP_subset_AWPP {α : Type} {enc : α ↪ List Bool} : SPP enc ⊆ AWPP enc

The characteristic GapP function has denominator one.

theorem Cslib.Complexity.compl_mem_AWPP {α : Type} {enc : α ↪ List Bool} {A : Set α} (hA : A ∈ AWPP enc) : Aᶜ ∈ AWPP enc

Subtracting the gap from its dyadic denominator exchanges yes and no instances.

theorem Cslib.Complexity.AWPP_subset_PP {α : Type} {enc : α ↪ List Bool} : AWPP enc ⊆ PP enc

The sign of twice the gap minus the denominator recognizes the language in PP.

theorem Cslib.Complexity.mem_AWPP_of_polyTime_exponent {α : Type} {enc : α ↪ List Bool} {A : Set α} {g : α → ℤ} {r : α → ℕ} (hg : g ∈ GapP enc) (hr : Turing.MultiTapeTM.ComputableTidilyInPolyTime r enc Turing.MultiTapeTM.encUnary) (hA : ∀ (a : α), (0 ≤ g a ∧ g a ≤ 2 ^ r a) ∧ (a ∈ A → 2 * 2 ^ r a ≤ 3 * g a) ∧ (a ∉ A → 3 * g a ≤ 2 ^ r a)) : A ∈ AWPP enc

An efficiently computed unary exponent can be padded to a polynomial in input length. Multiplying numerator and denominator by the same power of two preserves the ratio.

theorem Cslib.Complexity.PolyTimeReducible.mem_AWPP {α : Type} {enc : α ↪ List Bool} {A : Set α} {β : Type} {encB : β ↪ List Bool} {B : Set β} (h : PolyTimeReducible enc encB A B) (hB : B ∈ AWPP encB) : A ∈ AWPP enc

Polynomial-time many-one reductions preserve AWPP after dyadic denominator padding.