Documentation

VCVio.EvalDist.Defs.AlternativeMonad

Denotational Semantics Over AlternativeMonad. #

This file defines HasEvalSet.LawfulFailure, a type-class refining MonadLiftT m SetM when given an AlternativeMonad instance on the base monad, enforcing that failure maps to the empty sub-distribution. Compatibility conditions then force the correct semantics for evalDist, recorded in the *_failure simp lemmas below.

source
class HasEvalSet.LawfulFailure (m : Type u → Type v) [AlternativeMonad m] [MonadLiftT m SetM] :
Prop

Refinement of MonadLiftT m SetM when given an AlternativeMonad instance on the base monad, enforcing that failure maps to the empty sub-distribution. Compatibility conditions then force the correct semantics for evalDist, see below.

Instances
    source
    @[simp]
    theorem support_failure {m : Type u → Type v} [AlternativeMonad m] {α : Type u} [MonadLiftT m SetM] [HasEvalSet.LawfulFailure m] :
    support failure = ∅
    source
    @[simp]
    theorem finSupport_failure {m : Type u → Type v} [AlternativeMonad m] {α : Type u} [MonadLiftT m SetM] [HasEvalSet.LawfulFailure m] [HasEvalFinset m] [DecidableEq α] :
    finSupport failure = ∅
    source
    @[simp]
    theorem probOutput_failure {m : Type u → Type v} [AlternativeMonad m] {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] [HasEvalSet.LawfulFailure m] (x : α) :
    Pr[= x | failure] = 0
    source
    @[simp]
    theorem probEvent_failure {m : Type u → Type v} [AlternativeMonad m] {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] [HasEvalSet.LawfulFailure m] (p : α → Prop) :
    probEvent failure p = 0
    source
    @[simp]
    theorem probFailure_failure {m : Type u → Type v} [AlternativeMonad m] {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] [HasEvalSet.LawfulFailure m] :
    Pr[⊥ | failure] = 1
    source
    @[simp]
    theorem evalDist_failure {m : Type u → Type v} [AlternativeMonad m] {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] [HasEvalSet.LawfulFailure m] :
    𝒟[failure] = SPMF.mk (PMF.pure none)