One request to an oracle language

Cslib.Complexity.queryBit w submits the word w and reads the first bit of the reply. Against an oracle language A it returns decide (w ∈ A) and makes exactly the one request w; for a polynomial-time word it is strict oracle PPT, since the word is written on the query buffer and only one bit of the reply is read. The oracle closure rules and the bounded-query classes build their one-request certificates from this program.

Main definitions

• Cslib.Complexity.queryBit: one request, reading one bit of the reply.

Main results

• Cslib.Complexity.interpret_queryBit: against A, the request answers membership in A.
• Cslib.Complexity.queriesWith_queryBit: the program makes exactly one request.
• Cslib.Complexity.isOraclePPTOn_queryBit: one request for a polynomial-time word is strict oracle PPT.

def Cslib.Complexity.queryBit (w : List Bool) : WordQueryComp Unit Bool

One request: submit the word w and read the first bit of the reply.

theorem Cslib.Complexity.interpret_queryBit (A : Set (List Bool)) (w : List Bool) : OracleComp.interpret (languageOracle A) (queryBit w) = decide (w ∈ A)

Against an oracle language, one request answers membership of its word.

@[simp]

theorem Cslib.Complexity.queriesWith_queryBit (answer : Unit × List Bool → List Bool) (w : List Bool) : OracleComp.queriesWith answer (queryBit w) = [((), w)]

One request makes one request.

theorem Cslib.Complexity.isOraclePPTOn_queryBit {α : Type} {req : α → List Bool} {input : α ↪ List Bool} (hreq : Turing.MultiTapeTM.ComputableInPolyTime req input Turing.MultiTapeTM.encBits) : Probability.IsOraclePPTOn input Turing.MultiTapeTM.encBool fun (a : α) => OracleComp.interpret ProbOracleComp.query (queryBit (req a))

One request for a polynomial-time word is strict oracle PPT: the word is written on the query buffer and one bit of the reply is read.