Documentation

VCVio.EvalDist.Defs.AlternativeMonad

Denotational Semantics Over AlternativeMonad. #

This file defines a type-class for HasEvalSet 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 _.

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

Type-class for HasEvalSet 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} [HasEvalSet m] [HasEvalSet.LawfulFailure m] :
    support failure = ∅
    source
    @[simp]
    theorem finSupport_failure {m : Type u → Type v} [AlternativeMonad m] {α : Type u} [HasEvalSet m] [HasEvalSet.LawfulFailure m] [HasEvalFinset m] [DecidableEq α] :
    finSupport failure = ∅
    source
    @[simp]
    theorem probOutput_failure {m : Type u → Type v} [AlternativeMonad m] {α : Type u} [HasEvalSPMF m] [HasEvalSet.LawfulFailure m] (x : α) :
    Pr[=x | failure] = 0
    source
    @[simp]
    theorem probEvent_failure {m : Type u → Type v} [AlternativeMonad m] {α : Type u} [HasEvalSPMF m] [HasEvalSet.LawfulFailure m] (p : α → Prop) :
    Pr[p | failure] = 0
    source
    @[simp]
    theorem probFailure_failure {m : Type u → Type v} [AlternativeMonad m] {α : Type u} [HasEvalSPMF m] [HasEvalSet.LawfulFailure m] :
    Pr[⊥ | failure] = 1
    source
    @[simp]
    theorem evalDist_failure {m : Type u → Type v} [AlternativeMonad m] {α : Type u} [HasEvalSPMF m] [HasEvalSet.LawfulFailure m] :
    evalDist failure = SPMF.mk (PMF.pure none)