Bounded-error postselected polynomial time

BPPpath was introduced by Han, Hemaspaandra and Thierauf as the class of languages accepted by polynomial-time nondeterministic threshold machines, with computation paths of possibly different lengths, whose fraction of accepting paths is bounded away from one half. We fix the ratio gap at three quarters; by their error reduction any fixed gap gives the same class, which is not proved here. We state it through its path counts: there are #P functions acc and rej counting the accepting and rejecting paths, with at least one path on every input, such that acc ≥ 3 rej on members and rej ≥ 3 acc on nonmembers. As for SBP (Cslib.Complexity.SBP), these are verifier counts; the equivalence with the machine definition is not proved here.

SBP lies between BPP and BPPpath Böhler, Glaßer and Meister: an SBP count f with an FP threshold k and an amplified gap is turned into the path counts 3f and k. With PP it gives the chain BPP ⊆ SBP ⊆ BPPpath ⊆ PP.

Main definitions

• Cslib.Complexity.BPPpath: bounded-error postselected polynomial time via path counts.

Main results

• Cslib.Complexity.SBP_subset_BPPpath: SBP is contained in BPPpath.
• Cslib.Complexity.BPP_subset_BPPpath, Cslib.Complexity.BPPpath_subset_PP.

References

• Y. Han, L. A. Hemaspaandra, T. Thierauf, Threshold computation and cryptographic security
• E. Böhler, C. Glaßer, D. Meister, Error-bounded probabilistic computations between MA and AM

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

The languages with #P path counts acc (accepting) and rej (rejecting), at least one path on every input, where at least three quarters of the paths accept on members and at least three quarters reject on nonmembers Han, Hemaspaandra and Thierauf.

theorem Cslib.Complexity.mem_BPPpath {α : Type} {enc : α ↪ List Bool} {A : Set α} : A ∈ BPPpath enc ↔ ∃ acc ∈ SharpP enc, ∃ rej ∈ SharpP enc, ∀ (a : α), 0 < acc a + rej a ∧ (a ∈ A → 3 * rej a ≤ acc a) ∧ (a ∉ A → 3 * acc a ≤ rej a)

theorem Cslib.Complexity.SBP_subset_BPPpath {α : Type} {enc : α ↪ List Bool} : SBP enc ⊆ BPPpath enc

SBP ⊆ BPPpath Böhler, Glaßer and Meister. Amplify the SBP gap to sixteen; then 3f accepting paths against k rejecting paths give the ratio three on both sides.

theorem Cslib.Complexity.BPP_subset_BPPpath {α : Type} {enc : α ↪ List Bool} : BPP enc ⊆ BPPpath enc

BPP ⊆ BPPpath, through BPP ⊆ SBP Han, Hemaspaandra and Thierauf.

theorem Cslib.Complexity.BPPpath_subset_PP {α : Type} {enc : α ↪ List Bool} : BPPpath enc ⊆ PP enc

BPPpath ⊆ PP: the integer gap acc - rej is positive exactly on members.