Documentation

CslibFrontier.Computability.Complexity.Classes.FewP

Polynomially bounded ambiguity #

FewP allows a polynomial number of accepting certificates on each input, extending the one-witness condition of UP; see Allender and Rubinstein and the explicit acceptance-set definition in Borchert, Hemaspaandra and Rothe, Section 1. This file uses exact-length verifier counts. Classes.FewP.Machine proves the equivalent native finite-machine characterization, with a polynomial bound on accepting occurrence traces.

The containments and closures below are elementary consequences of the definition and the existing SharpP algebra: addition adds the ambiguity bounds, multiplication multiplies them, and polynomial-time precomposition composes a bound with a polynomially bounded output length.

Main definitions #

Main results #

References #

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

A language in NP with a polynomial bound on the number of accepting certificates on every input Allender and Rubinstein. The bound is in the encoded input length, not in the certificate length.

Instances For
    source
    theorem Cslib.Complexity.mem_FewP {α : Type} {enc : α ↪ List Bool} {A : Set α} :
    A ∈ FewP enc ↔ ∃ (p : Polynomial ℕ) (q : Polynomial ℕ) (V : α × List Bool → Bool), Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool ∧ (∀ (a : α), acceptCount V a (Polynomial.eval (enc a).length p) ≤ Polynomial.eval (enc a).length q) ∧ ∀ (a : α), a ∈ A ↔ 0 < acceptCount V a (Polynomial.eval (enc a).length p)

    A verifier characterization with a separate polynomial bound on its accepting count.

    source
    theorem Cslib.Complexity.UP_subset_FewP {α : Type} {enc : α ↪ List Bool} :
    UP enc ⊆ FewP enc

    A bound of one is a polynomial ambiguity bound.

    source
    theorem Cslib.Complexity.FewP_subset_NP {α : Type} {enc : α ↪ List Bool} :
    FewP enc ⊆ NP enc

    Forgetting the ambiguity bound gives NP membership.

    source
    theorem Cslib.Complexity.union_mem_FewP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ FewP enc) (hB : B ∈ FewP enc) :
    A ∪ B ∈ FewP enc

    Union adds the two polynomial ambiguity bounds.

    source
    theorem Cslib.Complexity.inter_mem_FewP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ FewP enc) (hB : B ∈ FewP enc) :
    A ∩ B ∈ FewP enc

    Intersection multiplies the two polynomial ambiguity bounds.

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

    Polynomial-time reductions preserve a polynomial ambiguity bound.