Executing Monads as Probabalistic Computations

This file defines a structure ExecutionMethod spec m to provide a way to specify how to run a monadic computation as a ProbComp (and in particular get probability distributions on outputs of the computation). Definitions like SignatureAlg extend this to allow them to be defined over arbitrary monads. This means that definitions like "IND-CPA secure" are always relative to the execution method.

ExecutionMethod.default handles the case where spec := probSpec, in which case the "execution function" is just id.

structure ExecutionMethod (m : Type u → Type v) : Type (max (u + 1) v)

An ExecutionMethod m provides a way to map computations in the monad m into ProbComp. In particular it allows computations in m

• exec {α : Type u} : m α → ProbComp α
• lift_probComp {α : Type u} : ProbComp α → m α
• exec_lift_probComp {α : Type u} (px : ProbComp α) : self.exec (self.lift_probComp px) = px

def ExecutionMethod.default : ExecutionMethod ProbComp

Execute a computation in ProbComp via ProbComp, by using the identity function.

Equations

• ExecutionMethod.default = { exec := fun {α : Type ?u.2} => id, lift_probComp := fun {α : Type ?u.2} => id, exec_lift_probComp := @ExecutionMethod.default.proof_1 }