Denotational Semantics for Output Distributions

This file defines a typeclass for monads that can be canonically embedded in the SPMF monad. We require this embedding respect the basic monad laws.

We also define a number of specific cases:

• Pr[= x | mx] / probOutput mx x for odds of mx returning x
• Pr[p | mx] / probEvent mx p for odds of mx's result satisfying p
• Pr[e | x ← mx] where x is free in the expression e
• Pr{x ← mx}[e] where x is free in the expression e
• Pr[⊥ | mx] / probFailure mx for odds of mx resulting in failure

For the last case, we assume mx has an OptionT transformer to represent the failure. In future it may be nice to generalize to any AlternativeMonad using an additional typeclass (note that it can't extend the existing one as it outputs in an SPMF).

@[reducible]

def SPMF : Type u → Type u

Subprobability distribution.

Equations

• SPMF = OptionT PMF

theorem SPMF.tsum_run_some_eq_one_sub {α : Type u} (p : SPMF α) : ∑' (x : α), (OptionT.run p) (some x) = 1 - (OptionT.run p) none

@[simp]

theorem SPMF.tsum_run_some_ne_top {α : Type u} (p : SPMF α) : ∑' (x : α), (OptionT.run p) (some x) ≠ ⊤

theorem SPMF.run_none_eq_one_sub {α : Type u} (p : SPMF α) : (OptionT.run p) none = 1 - ∑' (x : α), (OptionT.run p) (some x)

@[simp]

theorem SPMF.run_none_ne_top {α : Type u} (p : SPMF α) : (OptionT.run p) none ≠ ⊤

theorem SPMF.ext {α : Type u} {p q : SPMF α} (h : ∀ (x : α), (OptionT.run p) (some x) = (OptionT.run q) (some x)) : p = q

theorem SPMF.ext_iff {α : Type u} {p q : SPMF α} : p = q ↔ ∀ (x : α), (OptionT.run p) (some x) = (OptionT.run q) (some x)

instance SPMF.instFunLikeENNReal {α : Type u} : FunLike (SPMF α) α ENNReal

Equations

• SPMF.instFunLikeENNReal = { coe := fun (sp : SPMF α) (x : α) => (OptionT.run sp) (some x), coe_injective' := ⋯ }

@[simp]

theorem SPMF.apply_eq_run_some {α : Type u} (p : SPMF α) (x : α) : p x = (OptionT.run p) (some x)

theorem SPMF.apply'_none_eq_run {α : Type u} (p : SPMF α) : let p' := p; p' none = (OptionT.run p) none

class HasEvalDist (m : Type u → Type v) [Monad m] : Type (max (u + 1) v)

The monad m has a well-behaved embedding into the SPMF monad. TODO: modify this to extend MonadHom to get some lemmas for free.

• evalDist {α : Type u} (mx : m α) : SPMF α
• evalDist_pure {α : Type u} (x : α) : evalDist (pure x) = pure x
• evalDist_bind {α β : Type u} (mx : m α) (my : α → m β) : evalDist (mx >>= my) = do let x ← evalDist mx evalDist (my x)

def probOutput {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] (mx : m α) (x : α) : ENNReal

Probability that a computation mx returns the value x.

Equations

• Pr[=x|mx] = (evalDist mx) x

noncomputable def probEvent {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] (mx : m α) (p : α → Prop) : ENNReal

Probability that a computation mx outputs a value satisfying p.

Equations

• Pr[p|mx] = (OptionT.run (evalDist mx)).toOuterMeasure (some '' {x : α | p x})

def probFailure {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] (mx : m α) : ENNReal

Probability that a compuutation mx will fail to return a value.

Equations

• Pr[⊥|mx] = (OptionT.run (evalDist mx)) none

def «termPr[=_|_]» : Lean.ParserDescr

Probability that a computation returns a particular output.

Equations

• One or more equations did not get rendered due to their size.

def «termPr[_|_]» : Lean.ParserDescr

Probability that a computation returns a value satisfying a predicate.

Equations

• One or more equations did not get rendered due to their size.

def «termPr[⊥|_]» : Lean.ParserDescr

Probability that a computation fails to return a value.

Equations

• One or more equations did not get rendered due to their size.

def probEventBinding1 : Lean.ParserDescr

Probability that a computation returns a value satisfying a predicate.

Equations

• One or more equations did not get rendered due to their size.

def probEventBinding2 : Lean.ParserDescr

Probability that a computation returns a value satisfying a predicate.

Equations

• One or more equations did not get rendered due to their size.

theorem probOutput_def {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] (mx : m α) (x : α) : Pr[=x|mx] = (OptionT.run (evalDist mx)) (some x)

theorem probEvent_def {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] (mx : m α) (p : α → Prop) : Pr[p|mx] = (OptionT.run (evalDist mx)).toOuterMeasure (some '' {x : α | p x})

theorem probFailure_def {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] (mx : m α) : Pr[⊥|mx] = (OptionT.run (evalDist mx)) none

@[simp]

theorem evalDist_comp_pure {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] : evalDist ∘ pure = pure

@[simp]

theorem evalDist_comp_pure' {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] (f : α → β) : evalDist ∘ pure ∘ f = pure ∘ f

@[simp]

theorem probOutput_pure {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] [DecidableEq α] (x y : α) : Pr[=x|pure y] = if x = y then 1 else 0

@[simp]

theorem evalDist_map {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] [LawfulMonad m] (mx : m α) (f : α → β) : evalDist (f <$> mx) = f <$> evalDist mx

@[simp]

theorem evalDist_comp_map {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] [LawfulMonad m] (mx : m α) : (evalDist ∘ fun (f : α → β) => f <$> mx) = fun (f : α → β) => f <$> evalDist mx

@[simp]

theorem evalDist_seq {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] [LawfulMonad m] (mf : m (α → β)) (mx : m α) : evalDist (mf <*> mx) = evalDist mf <*> evalDist mx

@[simp]

theorem evalDist_ite {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] (p : Prop) [Decidable p] (mx mx' : m α) : evalDist (if p then mx else mx') = if p then evalDist mx else evalDist mx'

theorem probEvent_eq_tsum_indicator {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] (mx : m α) (p : α → Prop) : Pr[p|mx] = ∑' (x : α), {x : α | p x}.indicator (fun (x : α) => Pr[=x|mx]) x

theorem probEvent_eq_tsum_ite {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] (mx : m α) (p : α → Prop) [DecidablePred p] : Pr[p|mx] = ∑' (x : α), if p x then Pr[=x|mx] else 0

@[simp]

theorem probFailure_add_tsum_probOutput {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] (oa : m α) : Pr[⊥|oa] + ∑' (x : α), Pr[=x|oa] = 1

@[simp]

theorem tsum_probOutput_add_probFailure {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] (oa : m α) : ∑' (x : α), Pr[=x|oa] + Pr[⊥|oa] = 1

@[simp]

theorem probOutput_le_one {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] {mx : m α} {x : α} : Pr[=x|mx] ≤ 1

@[simp]

theorem probOutput_ne_top {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] {mx : m α} {x : α} : Pr[=x|mx] ≠ ⊤

@[simp]

theorem probOutput_lt_top {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] {mx : m α} {x : α} : Pr[=x|mx] < ⊤

@[simp]

theorem not_one_lt_probOutput {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] {mx : m α} {x : α} : ¬1 < Pr[=x|mx]

@[simp]

theorem tsum_probOutput_le_one {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] {mx : m α} : ∑' (x : α), Pr[=x|mx] ≤ 1

@[simp]

theorem tsum_probOutput_ne_top {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] {mx : m α} : ∑' (x : α), Pr[=x|mx] ≠ ⊤

@[simp]

theorem probEvent_le_one {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] {mx : m α} {p : α → Prop} : Pr[p|mx] ≤ 1

@[simp]

theorem probEvent_ne_top {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] {mx : m α} {p : α → Prop} : Pr[p|mx] ≠ ⊤

@[simp]

theorem probEvent_lt_top {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] {mx : m α} {p : α → Prop} : Pr[p|mx] < ⊤

@[simp]

theorem not_one_lt_probEvent {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] {mx : m α} {p : α → Prop} : ¬1 < Pr[p|mx]

@[simp]

theorem probFailure_le_one {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] {mx : m α} : Pr[⊥|mx] ≤ 1

@[simp]

theorem probFailure_ne_top {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] {mx : m α} : Pr[⊥|mx] ≠ ⊤

@[simp]

theorem probFailure_lt_top {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] {mx : m α} : Pr[⊥|mx] < ⊤

@[simp]

theorem not_one_lt_probFailure {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] {mx : m α} : ¬1 < Pr[⊥|mx]

@[simp]

theorem one_le_probOutput_iff {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] {mx : m α} {x : α} : 1 ≤ Pr[=x|mx] ↔ Pr[=x|mx] = 1

@[simp]

theorem one_le_probEvent_iff {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] {mx : m α} {p : α → Prop} : 1 ≤ Pr[p|mx] ↔ Pr[p|mx] = 1

@[simp]

theorem one_le_probFailure_iff {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] {mx : m α} : 1 ≤ Pr[⊥|mx] ↔ Pr[⊥|mx] = 1

theorem probOutput_bind_eq_tsum {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] (mx : m α) (my : α → m β) (y : β) : Pr[=y|mx >>= my] = ∑' (x : α), Pr[=x|mx] * Pr[=y|my x]

theorem probOutput_true_eq_probEvent {α : Type} {m : Type → Type u} [Monad m] [HasEvalDist m] (mx : m α) (p : α → Prop) : Pr[=True|do let x ← mx pure (p x)] = Pr[p|mx]

instance SPMF.hasEvalDist : HasEvalDist SPMF

Add instance for SPMF just to give access to notation.

Equations

• SPMF.hasEvalDist = { evalDist := fun {α : Type ?u.4} => id, evalDist_pure := @SPMF.hasEvalDist._proof_1, evalDist_bind := @SPMF.hasEvalDist._proof_2 }

@[simp]

theorem SPMF.evalDist_eq {α : Type u} (p : SPMF α) : evalDist p = p

@[simp]

theorem SPMF.probOutput_eq {α : Type u} (p : SPMF α) : probOutput p = ⇑p

@[simp]

theorem SPMF.probEvent_eq {α : Type u} (p : SPMF α) : probEvent p = ⇑(OptionT.run p).toOuterMeasure ∘ Set.image some

@[simp]

theorem SPMF.probFailure_eq {α : Type u} (p : SPMF α) : Pr[⊥|p] = (OptionT.run p) none

noncomputable instance PMF.hasEvalDist : HasEvalDist PMF

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PMF.evalDist_eq {α : Type u} (p : PMF α) : evalDist p = liftM p

@[simp]

theorem PMF.probOutput_eq {α : Type u} (p : PMF α) : probOutput p = ⇑p

@[simp]

theorem PMF.probEvent_eq {α : Type u} (p : PMF α) : probEvent p = ⇑p.toOuterMeasure

@[simp]

theorem PMF.probFailure_eq {α : Type u} (p : PMF α) : Pr[⊥|p] = 0