Executing Computations

This file defines a function runIO for executing a ProbComp in the IO monad. We add this embedding as a MonadLift instance, so #eval notation works.

def OracleComp.runIO {α : Type} (oa : ProbComp α) : IO α

Represent a ProbComp via the IO monad, allowing actual execution.

@[implicit_reducible]

instance OracleComp.instMonadLiftProbCompIO : MonadLift ProbComp IO

Automatic lifting of probabalistic computations into IO.

def OracleComp.test1 : ProbComp (ℕ × ℕ × ℕ)

def OracleComp.test2 (n : ℕ) : ProbComp (List ℕ)

def OracleComp.test3 (n : ℕ) : ProbComp (List ℕ)

def OracleComp.test4 (n : ℕ) : ProbComp (List ℕ)