Documentation

CslibFrontier.Languages.Probabilistic.QueriesWith

The requests of a deterministic run #

Answering every call q of an oracle program by answer q runs it deterministically: OracleComp.interpret (m := Id) answer program. OracleComp.queriesWith answer program lists the requests made along that run, in order. Only their answers matter (OracleComp.interpret_id_congr): this locality underlies oracle constructions and adversary arguments, which fix the answers to the requests a program makes and leave every other answer free.

A program with a query budget of n makes at most n requests along every run (OracleComp.IsQueryBounded.length_queriesWith_le), and the result of a run whose answers are all possible is a possible result (OracleComp.interpret_id_mem_supportWith).

Main definitions #

Main results #

source
def Cslib.OracleComp.queriesWith {ι α : Type} {spec : OracleSpec ι} (answer : (q : ι) → spec q) :
OracleComp spec α → List ι

The requests made by program, in order, when every call q is answered by answer q.

Instances For
    source
    @[simp]
    theorem Cslib.OracleComp.queriesWith_pure {ι α : Type} {spec : OracleSpec ι} (answer : (q : ι) → spec q) (a : α) :
    queriesWith answer (pure a) = []
    source
    @[simp]
    theorem Cslib.OracleComp.queriesWith_query {ι : Type} {spec : OracleSpec ι} (answer : (q : ι) → spec q) (q : ι) :
    queriesWith answer (query q) = [q]
    source
    @[simp]
    theorem Cslib.OracleComp.queriesWith_query_bind {ι α : Type} {spec : OracleSpec ι} (answer : (q : ι) → spec q) (q : ι) (next : spec q → OracleComp spec α) :
    queriesWith answer (query q >>= next) = q :: queriesWith answer (next (answer q))
    source
    @[simp]
    theorem Cslib.OracleComp.interpret_id_query_bind {ι α : Type} {spec : OracleSpec ι} (answer : (q : ι) → spec q) (q : ι) (next : spec q → OracleComp spec α) :
    interpret answer (query q >>= next) = interpret answer (next (answer q))

    Answering the first call and continuing.

    source
    theorem Cslib.OracleComp.queriesWith_bind {ι α β : Type} {spec : OracleSpec ι} (answer : (q : ι) → spec q) (program : OracleComp spec α) (next : α → OracleComp spec β) :
    queriesWith answer (program >>= next) = queriesWith answer program ++ queriesWith answer (next (interpret answer program))

    A sequence makes the requests of its first part, then those of the continuation selected by the first result.

    source
    @[simp]
    theorem Cslib.OracleComp.queriesWith_map {ι α β : Type} {spec : OracleSpec ι} (answer : (q : ι) → spec q) (f : α → β) (program : OracleComp spec α) :
    queriesWith answer (f <$> program) = queriesWith answer program

    Postprocessing the result makes no request.

    source
    theorem Cslib.OracleComp.interpret_id_congr {ι α : Type} {spec : OracleSpec ι} (answer answer' : (q : ι) → spec q) (program : OracleComp spec α) (h : ∀ q ∈ queriesWith answer program, answer' q = answer q) :
    interpret answer' program = interpret answer program ∧ queriesWith answer' program = queriesWith answer program

    Locality. Answer functions that agree on the requests made under one of them give the same result and the same requests.

    source
    theorem Cslib.OracleComp.IsQueryBounded.length_queriesWith_le {ι α : Type} {spec : OracleSpec ι} (answer : (q : ι) → spec q) {program : OracleComp spec α} {n : ℕ} (h : program.IsQueryBounded n) :
    (queriesWith answer program).length ≤ n

    A program with a query budget of n makes at most n requests along every run.

    source
    theorem Cslib.OracleComp.interpret_id_mem_supportWith {ι α : Type} {spec : OracleSpec ι} {possible : (q : ι) → Set (spec q)} {answer : (q : ι) → spec q} (h : ∀ (q : ι), answer q ∈ possible q) (program : OracleComp spec α) :
    interpret answer program ∈ supportWith possible program

    A run whose every answer is possible has a possible result.