Documentation

CslibFrontier.Computability.Complexity.Classes.Oracle.Counting

Polynomial time with a #P oracle #

The oracle classes of Cslib.Complexity.PWithOracle query languages. The values of a function f : β → ℕ are queried bit by bit: the code encPair encβ encNat (b, i) asks for bit i of f b, under an encoding encβ of the arguments of f. An oracle language answers the bits of f (Cslib.Complexity.AnswersBits) when it contains every code exactly when the requested bit is 1; it may answer other words arbitrarily. The bit graph of f (Cslib.Complexity.bitGraph), which contains the codes of the bits 1 and nothing else, answers the bits of f.

P^#P relative to the encoding enc of instances (Cslib.Complexity.PWithSharpPOracle) consists of the problems L decided by one deterministic oracle program, strict oracle PPT as in Cslib.Complexity.ComputableInPolyTimeWithOracle, that is correct against every oracle language answering the bits of some function f ∈ #P, for some encoded type of arguments of f. As for Cslib.Complexity.RPWithPromiseOracle, the program is fixed before the oracle, and the answers on words that are not codes are arbitrary, so the program only learns bits of f; in particular the oracle does not reveal which words are codes, however hard that is to decide. Taking the bit graph as the oracle language, such a problem is in polynomial time relative to the bit graph of a function in #P (Cslib.Complexity.mem_PWithOracle_bitGraph). The class does not count queries; it contains P (Cslib.Complexity.P_subset_PWithSharpPOracle), and a problem decided by one bit, at a polynomial position, of a function in #P on its own instances is in it, by a program making one query (Cslib.Complexity.mem_PWithSharpPOracle_of_testBit).

Main definitions #

Main results #

References #

source
def Cslib.Complexity.AnswersBits {β : Type} (encβ : β ↪ List Bool) (f : β → ℕ) (A : Set (List Bool)) :
Prop

The oracle language A answers the bits of f : β → ℕ under the encoding encβ: the code encPair encβ encNat (b, i) is in A exactly when bit i of f b is 1. Words that are not codes may be in A or not.

Instances For
    source
    def Cslib.Complexity.bitGraph {β : Type} (encβ : β ↪ List Bool) (f : β → ℕ) :
    Set (List Bool)

    The bit graph of f : β → ℕ: the codes encPair encβ encNat (b, i) such that bit i of f b is 1, and no other word.

    Instances For
      source
      theorem Cslib.Complexity.answersBits_bitGraph {β : Type} (encβ : β ↪ List Bool) (f : β → ℕ) :
      AnswersBits encβ f (bitGraph encβ f)

      The bit graph answers the bits.

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

      P^#P Arora and Barak, Chapter 17: the problems L such that, for some type β with encoding encβ and some f ∈ SharpP encβ, one deterministic oracle program, strict oracle PPT on the encoding enc of instances, decides L against every oracle language answering the bits of f. Answers on words that are not codes are arbitrary.

      Instances For
        source
        theorem Cslib.Complexity.mem_PWithOracle_bitGraph {α : Type} {enc : α ↪ List Bool} {L : Set α} (hL : L ∈ PWithSharpPOracle enc) :
        ∃ (β : Type) (encβ : β ↪ List Bool), ∃ f ∈ SharpP encβ, L ∈ PWithOracle (bitGraph encβ f) enc

        P^#P lies in polynomial time relative to a #P bit graph: against the bit graph of its function, the program of a problem in P^#P decides it.

        source
        theorem Cslib.Complexity.P_subset_PWithSharpPOracle {α : Type} {enc : α ↪ List Bool} :
        P enc ⊆ PWithSharpPOracle enc

        P ⊆ P^#P: a polynomial-time decider makes no query.

        source
        theorem Cslib.Complexity.mem_PWithSharpPOracle_of_testBit {α : Type} {enc : α ↪ List Bool} {L : Set α} {f : α → ℕ} (hf : f ∈ SharpP enc) {p : Polynomial ℕ} (h : ∀ (a : α), a ∈ L ↔ (f a).testBit (Polynomial.eval (enc a).length p) = true) :
        L ∈ PWithSharpPOracle enc

        One bit of a #P value is in P^#P: a problem decided by the bit at a polynomial position of a function in #P on its own instances is in P^#P. The program asks for that bit, with one query.