Documentation

Complexity.Computability.Probabilistic.Oracle.SingleOracle

Routing a single-channel oracle program #

Route every query of a single-channel word-oracle program to one named channel, preserving the complete stateful interaction and its strict polynomial-time realization.

Main definitions #

Main results #

source
def Cslib.Probability.WordOracleComp.singleOracle {ι α : Type} (i₀ : ι) (p : WordOracleComp Unit α) :
WordOracleComp ι α

Route all word-oracle queries of a single-channel program to channel i₀ : ι.

Instances For
    source
    theorem Cslib.Probability.WordOracleComp.singleOracle_map {ι α β : Type} (i₀ : ι) (f : α → β) (p : WordOracleComp Unit α) :
    singleOracle i₀ (f <$> p) = f <$> singleOracle i₀ p
    source
    theorem Cslib.Probability.WordOracleComp.run_interpret_singleOracle {ι α State : Type} (i₀ : ι) (oracle : ι × List Bool → StateT State PMF (List Bool)) (p : WordOracleComp Unit α) (s : State) :
    (OracleComp.interpret (ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle) (singleOracle i₀ p)).run s = (OracleComp.interpret (ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) fun (q : Unit × List Bool) => oracle (i₀, q.2)) p).run s

    Interpreting WordOracleComp.singleOracle i₀ p against oracle is equivalent to interpreting p against fun q => oracle (i₀, q.2).

    source
    theorem Cslib.Probability.IsOraclePPTOn.singleOracle {ι α β : Type} [DecidableEq ι] [Finite ι] (i₀ : ι) {input : α ↪ List Bool} {output : β ↪ List Bool} {program : α → WordOracleComp Unit β} (h : IsOraclePPTOn input output program) :
    IsOraclePPTOn input output fun (a : α) => WordOracleComp.singleOracle i₀ (program a)

    Routing a strict oracle-PPT single-channel program to channel i₀ : ι preserves IsOraclePPTOn.