Probabilistic programs with oracles

OracleComp spec α is a terminating program with typed oracle calls described by the specification spec : OracleSpec ι, which gives the response type spec q of each query q : ι. A specification is the data of a polynomial functor, and programs are its PFunctor.FreeM, so they use ordinary do notation, and a program lives in the universe of its queries, responses, and result.

Randomness is not a separate effect. unifSpec is the interface answering n with a uniform element of Fin (n + 1), and ProbComp is OracleComp unifSpec. Any other distribution is reached by interpreting an interface with that distribution, so the base language has no primitive beyond uniform choice from a finite range.

OracleComp.interpret runs a program in any monad by answering each call with a handler in that monad. Into PMF it gives the output distribution of a program with a memoryless probabilistic oracle; into StateT State m it threads a hidden oracle state through the calls; into another OracleComp it replaces each call by a program over another interface, as needed for reductions; and into a writer monad it logs the queries. It is PFunctor.FreeM.liftM, so it preserves sequencing, and interpretations compose.

Neither termination nor a bound on the number of queries asserts computational efficiency. Computational efficiency requires a separate machine-realizability predicate. Unbounded loops and nontermination are outside this language; bounded iteration uses Lean recursion.

References

This is the design of Devon Tuma, Quang Dao, and collaborators' VCVio: OracleSpec, OracleComp, and unifSpec are their definitions, and OracleComp.interpret is their simulateQ.

@[reducible, inline]

abbrev Cslib.OracleSpec (ι : Type u) : Type (max u (v + 1))

An oracle specification: the response type of each query in ι.

@[reducible, inline]

abbrev Cslib.OracleComp {ι : Type u} (spec : OracleSpec ι) (α : Type v) : Type (max u v)

Terminating programs with typed oracle calls described by spec.

def Cslib.OracleComp.query {ι : Type u} {spec : OracleSpec ι} (q : ι) : OracleComp spec (spec q)

Make one oracle call. Later queries may depend on the answer.

def Cslib.OracleComp.interpret {ι : Type u} {spec : OracleSpec ι} {α : Type v} {m : Type v → Type w} [Monad m] (oracle : (q : ι) → m (spec q)) (program : OracleComp spec α) : m α

Run a program in the monad m, answering each oracle call with oracle.

@[simp]

theorem Cslib.OracleComp.interpret_pure {ι : Type u} {spec : OracleSpec ι} {α : Type v} {m : Type v → Type w} [Monad m] (oracle : (q : ι) → m (spec q)) (a : α) : interpret oracle (pure a) = pure a

@[simp]

theorem Cslib.OracleComp.interpret_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type v} {m : Type v → Type w} [Monad m] [LawfulMonad m] (oracle : (q : ι) → m (spec q)) (program : OracleComp spec α) (next : α → OracleComp spec β) : interpret oracle (program >>= next) = do let a ← interpret oracle program interpret oracle (next a)

@[simp]

theorem Cslib.OracleComp.interpret_query {ι : Type u} {spec : OracleSpec ι} {m : Type v → Type w} [Monad m] [LawfulMonad m] (oracle : (q : ι) → m (spec q)) (q : ι) : interpret oracle (query q) = oracle q

@[simp]

theorem Cslib.OracleComp.interpret_map {ι : Type u} {spec : OracleSpec ι} {α β : Type v} {m : Type v → Type w} [Monad m] [LawfulMonad m] (oracle : (q : ι) → m (spec q)) (f : α → β) (program : OracleComp spec α) : interpret oracle (f <$> program) = f <$> interpret oracle program

@[simp]

theorem Cslib.OracleComp.interpret_query_eq_self {ι : Type u} {spec : OracleSpec ι} {α : Type v} (program : OracleComp spec α) : interpret query program = program

Answering each call by itself leaves the program unchanged.

theorem Cslib.OracleComp.interpret_interpret {ι : Type u} {spec : OracleSpec ι} {α : Type v} {m : Type v → Type w} [Monad m] [LawfulMonad m] {ι' : Type u} {spec' : OracleSpec ι'} (handler : (q : ι) → OracleComp spec' (spec q)) (oracle : (q : ι') → m (spec' q)) (program : OracleComp spec α) : interpret oracle (interpret handler program) = interpret (fun (q : ι) => interpret oracle (handler q)) program

Interpretations compose: interpreting a program whose calls were replaced by programs over another interface is interpreting the original calls through the replacements. No fresh state is introduced between calls.

theorem Cslib.OracleComp.run_interpret_readOnly {ι : Type u} {spec : OracleSpec ι} {α State : Type v} {m : Type v → Type w} [Monad m] [LawfulMonad m] (oracle : (q : ι) → State → m (spec q)) (program : OracleComp spec α) (s : State) : (interpret (fun (q : ι) (s : State) => (fun (a : spec q) => (a, s)) <$> oracle q s) program).run s = (fun (a : α) => (a, s)) <$> interpret (fun (q : ι) => oracle q s) program

An oracle may consult a fixed private environment without changing it. Its stateful execution agrees with interpreting the program against that environment.

theorem Cslib.OracleComp.run_interpret_stateless {ι : Type u} {spec : OracleSpec ι} {α State : Type v} {m : Type v → Type w} [Monad m] [LawfulMonad m] (oracle : (q : ι) → m (spec q)) (program : OracleComp spec α) (s : State) : (interpret (fun (q : ι) (s : State) => (fun (a : spec q) => (a, s)) <$> oracle q) program).run s = (fun (a : α) => (a, s)) <$> interpret oracle program

Adding an untouched private state to a memoryless oracle does not change the result.

@[reducible, inline]

abbrev Cslib.unifSpec : OracleSpec ℕ

The uniform sampling interface: the query n is answered by a uniform element of Fin (n + 1).

@[reducible, inline]

abbrev Cslib.ProbComp (α : Type) : Type

Probabilistic programs whose only randomness is uniform choice from a finite range.

def Cslib.ProbComp.unifFin (n : ℕ) : ProbComp (Fin (n + 1))

Draw a uniform element of Fin (n + 1).

noncomputable def Cslib.ProbComp.uniform (α : Type) [Fintype α] [Nonempty α] : ProbComp α

Uniform sampling from a nonempty finite type, through an enumeration of it.

noncomputable def Cslib.ProbComp.unifOracle (n : ℕ) : PMF (Fin (n + 1))

The oracle answering each query uniformly.

noncomputable def Cslib.ProbComp.eval {α : Type} (program : ProbComp α) : PMF α

The distribution denoted by a closed probabilistic program.

@[simp]

theorem Cslib.ProbComp.eval_pure {α : Type} (a : α) : (pure a).eval = PMF.pure a

@[simp]

theorem Cslib.ProbComp.eval_bind {α β : Type} (program : ProbComp α) (next : α → ProbComp β) : (program >>= next).eval = program.eval.bind fun (a : α) => (next a).eval

@[simp]

theorem Cslib.ProbComp.eval_map {α β : Type} (f : α → β) (program : ProbComp α) : (f <$> program).eval = PMF.map f program.eval

@[simp]

theorem Cslib.ProbComp.eval_unifFin (n : ℕ) : (unifFin n).eval = Probability.PMF.uniformOfFintype (Fin (n + 1))

@[simp]

theorem Cslib.ProbComp.eval_uniform (α : Type) [Fintype α] [Nonempty α] : (uniform α).eval = Probability.PMF.uniformOfFintype α

Sampling through an enumeration is uniform on the type.