Documentation

VCVio.EvalDist.Basic

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

Instances For

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

@[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 α) :

have 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)

Instances

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

Probability that a computation mx returns the value x.

Equations

Instances For

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

Probability that a computation mx outputs a value satisfying p.

Equations

Instances For

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

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

Equations

Instances For

def «termPr[=_|_]» :

Lean.ParserDescr

Probability that a computation returns a particular output.

Equations

Instances For

def «termPr[_|_]» :

Lean.ParserDescr

Probability that a computation returns a value satisfying a predicate.

Equations

Instances For

def «termPr[⊥|_]» :

Lean.ParserDescr

Probability that a computation fails to return a value.

Equations

Instances For

def probEventBinding1 :

Lean.ParserDescr

Probability that a computation returns a value satisfying a predicate.

Equations

Instances For

def probEventBinding2 :

Lean.ParserDescr

Probability that a computation returns a value satisfying a predicate.

Equations

Instances For

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} :

@[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} :

@[simp]

theorem not_one_lt_probEvent {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalDist m] {mx : m α} {p : α → Prop} :

@[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

@[simp]

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

@[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

@[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 α) :