Documentation

Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Oracle

Fair-coin machines with external oracle calls #

runOracle fixes the coin program of the common machine interpreter and exposes its word-based external channels. The two effects use disjoint query types: external handlers cannot choose the machine's private coins. Every live instruction draws one fresh fair bit; query writing and reply reading still use ordinary machine instructions.

Main definitions #

Main results #

References #

Adapts the oracle run from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8 to the common machine and typed sum interface.

source
noncomputable def Turing.MultiTapePTM.runOracle {k : ℕ} {Symbol State Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Symbol State Operation) (fuel : ℕ) (input : List Symbol) :
Cslib.ProbOracleComp (fun (x : Operation × List Symbol) => List Symbol) (List Symbol)

Use private fair coins and submit each channel's accumulated word to the external oracle.

Instances For
    source
    theorem Turing.MultiTapePTM.length_output_runOracle_le {k : ℕ} {Symbol State Operation OracleState : Type} [DecidableEq Operation] (machine : MultiTapePTM k Symbol State Operation) (oracle : Operation × List Symbol → StateT OracleState PMF (List Symbol)) (fuel : ℕ) (input output : List Symbol) (s s' : OracleState) (h : (output, s') ∈ ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) (machine.runOracle fuel input)).run s).support) :
    output.length ≤ fuel

    Arbitrarily long oracle replies cannot bypass the cost of writing the output.

    source
    theorem Turing.MultiTapePTM.run_interpret_runOracle_ofDeterministic {k : ℕ} {Symbol State Operation OracleState : Type} [DecidableEq Operation] (machine : MultiTapeTM k Symbol State) (oracle : Operation × List Symbol → StateT OracleState PMF (List Symbol)) (fuel : ℕ) (input : List Symbol) (s : OracleState) :
    (Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) ((ofDeterministic machine).runOracle fuel input)).run s = PMF.pure ((MultiTapeTM.runFrom (machine.initCfg input) fuel).output, s)

    A deterministic run ignores the external oracle and preserves its full private state.

    source
    def Turing.MultiTapePTM.ofClosed {k : ℕ} {Symbol State Operation : Type} (machine : MultiTapePTM k Symbol State) :
    MultiTapePTM k Symbol State Operation

    A closed fair-coin machine with external channels that it never reads or writes.

    Instances For
      source
      theorem Turing.MultiTapePTM.runOracle_ofClosed {k : ℕ} {Symbol State Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Symbol State) (fuel : ℕ) (input : List Symbol) :
      machine.ofClosed.runOracle fuel input = Cslib.ProbOracleComp.sample (machine.runClosed fuel input)

      Running a closed machine with external channels samples its closed run: the program makes no external call, so it preserves every external oracle state.

      source
      theorem Turing.MultiTapePTM.runOracle_eq_sample_runClosed {k : ℕ} {Symbol State : Type} (machine : MultiTapePTM k Symbol State) (fuel : ℕ) (input : List Symbol) :
      machine.runOracle fuel input = Cslib.ProbOracleComp.sample (machine.runClosed fuel input)

      A machine without external channels never calls the external oracle: its oracle run is its sampled closed run.

      source
      theorem Turing.MultiTapePTM.run_interpret_runOracle_ofClosed {k : ℕ} {State Operation OracleState : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool State) (oracle : Operation × List Bool → StateT OracleState PMF (List Bool)) (fuel : ℕ) (input : List Bool) (s : OracleState) :
      (Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) (machine.ofClosed.runOracle fuel input)).run s = PMF.map (fun (x : List Bool) => (x, s)) (machine.runClosed fuel input).eval

      A closed machine's oracle run preserves every external oracle state and has the closed output distribution.