Evaluation Semantics for ReaderT

This file provides monad homomorphisms for evaluating ReaderT ρ m computations by fixing the environment parameter.

Unlike StateT, ReaderT evaluation at a fixed environment is a valid monad homomorphism because the environment is read-only and doesn't change during computation.

Main definitions

• ReaderT.evalAt ρ0: Monad homomorphism ReaderT ρ m →ᵐ m by evaluation at ρ0
• ReaderT.toSPMF ρ0: Lift MonadLiftT m SPMF through ReaderT at fixed ρ0
• ReaderT.toPMF ρ0: Lift MonadLiftT m PMF through ReaderT at fixed ρ0

Design notes

We do NOT provide global MonadLiftT (ReaderT ρ m) SPMF instances because there's no canonical choice of environment. Instead, users explicitly provide the environment when constructing the evaluation homomorphism.

For cryptographic games with random oracles, the typical pattern is:

1. Generate oracle table with some distribution
2. Use toSPMF/toPMF to evaluate the protocol at that table
3. Compose with the table distribution to get overall game probability

def ReaderT.evalAt {ρ : Type u} {m : Type u → Type v} [Monad m] (ρ0 : ρ) : ReaderT ρ m →ᵐ m

Evaluate a ReaderT computation at a fixed environment ρ0. This is a monad homomorphism because ReaderT is read-only.

@[simp]

theorem ReaderT.evalAt_apply {ρ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (ρ0 : ρ) (mx : ReaderT ρ m α) : (fun {α : Type u} (x : ReaderT ρ m α) => (evalAt ρ0).toFun α x) mx = mx ρ0

@[simp]

theorem ReaderT.evalAt_pure {ρ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (ρ0 : ρ) (x : α) : (fun {α : Type u} (x : ReaderT ρ m α) => (evalAt ρ0).toFun α x) (pure x) = pure x

@[simp]

theorem ReaderT.evalAt_bind {ρ : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} (ρ0 : ρ) (mx : ReaderT ρ m α) (f : α → ReaderT ρ m β) : (fun {α : Type u} (x : ReaderT ρ m α) => (evalAt ρ0).toFun α x) (mx >>= f) = do let x ← (fun {α : Type u} (x : ReaderT ρ m α) => (evalAt ρ0).toFun α x) mx (fun {α : Type u} (x : ReaderT ρ m α) => (evalAt ρ0).toFun α x) (f x)

noncomputable def ReaderT.toSPMF {ρ : Type u} {m : Type u → Type v} [Monad m] (ρ0 : ρ) [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] : ReaderT ρ m →ᵐ SPMF

Lift m → SPMF to a homomorphism ReaderT ρ m →ᵐ SPMF by fixing ρ0.

This allows evaluating reader computations to sub-probability distributions when the base monad m has such an evaluation.

noncomputable def ReaderT.toPMF {ρ : Type u} {m : Type u → Type v} [Monad m] (ρ0 : ρ) [MonadLiftT m PMF] [LawfulMonadLiftT m PMF] : ReaderT ρ m →ᵐ PMF

Lift m → PMF to a homomorphism ReaderT ρ m →ᵐ PMF by fixing ρ0.

@[simp]

theorem ReaderT.toSPMF_pure {ρ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] (ρ0 : ρ) (x : α) : (fun {α : Type u} (x : ReaderT ρ m α) => (toSPMF ρ0).toFun α x) (pure x) = liftM (pure x)

Evaluating pure x at any environment gives the same result as pure x in the base monad.

@[simp]

theorem ReaderT.toSPMF_bind {ρ : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] (ρ0 : ρ) (mx : ReaderT ρ m α) (f : α → ReaderT ρ m β) : (fun {α : Type u} (x : ReaderT ρ m α) => (toSPMF ρ0).toFun α x) (mx >>= f) = do let x ← (fun {α : Type u} (x : ReaderT ρ m α) => (toSPMF ρ0).toFun α x) mx (fun {α : Type u} (x : ReaderT ρ m α) => (toSPMF ρ0).toFun α x) (f x)

Evaluating a bind distributes through the monad homomorphism.

@[simp]

theorem ReaderT.toPMF_pure {ρ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m PMF] [LawfulMonadLiftT m PMF] (ρ0 : ρ) (x : α) : (fun {α : Type u} (x : ReaderT ρ m α) => (toPMF ρ0).toFun α x) (pure x) = liftM (pure x)

@[simp]

theorem ReaderT.toPMF_bind {ρ : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} [MonadLiftT m PMF] [LawfulMonadLiftT m PMF] (ρ0 : ρ) (mx : ReaderT ρ m α) (f : α → ReaderT ρ m β) : (fun {α : Type u} (x : ReaderT ρ m α) => (toPMF ρ0).toFun α x) (mx >>= f) = do let x ← (fun {α : Type u} (x : ReaderT ρ m α) => (toPMF ρ0).toFun α x) mx (fun {α : Type u} (x : ReaderT ρ m α) => (toPMF ρ0).toFun α x) (f x)