Successful-output measure semantics for optional computations

An OptionT computation denotes the pullback of its underlying Option-valued measure along the measurable embedding some. This effect-native construction supplies the primary semantics; finite-distribution lifts remain available for explicit compatibility observations.

Native map and monad laws use the base monad's measure laws. The full bind law only requires measurability of the successful-output family. A pullback space recording the full continuation outcomes refines the selected source space, and the map law transports its measure back.

@[instance_reducible, instance 20]

noncomputable instance instEvalDistSemanticsOptionT {m : Type u → Type v} [EvalDistSemantics m] : EvalDistSemantics (OptionT m)

Interpret successful OptionT results by pulling the run measure back along some.

theorem OptionT.evalDist_eq_comap_some {m : Type u → Type v} [EvalDistSemantics m] {α : Type u} [MeasurableSpace α] (mx : OptionT m α) : 𝒟[mx] = MeasureTheory.Measure.comap some 𝒟[mx.run]

Unfold the native successful-output semantics to Mathlib's pullback along some.

theorem OptionT.evalDist_apply {m : Type u → Type v} [EvalDistSemantics m] {α : Type u} [MeasurableSpace α] (mx : OptionT m α) {event : Set α} : 𝒟[mx] event = 𝒟[mx.run] (some '' event)

The successful-output measure of an optional computation on an event is the run measure of the corresponding some outcomes.

@[simp]

theorem OptionT.evalDist_apply_univ {m : Type u → Type v} [EvalDistSemantics m] {α : Type u} [MeasurableSpace α] (mx : OptionT m α) : 𝒟[mx] Set.univ = 𝒟[mx.run] {value : Option α | value.isSome = true}

The successful mass of an optional computation is the mass of present values in its run.

theorem OptionT.evalDist_pure {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulPureEvalDistSemantics m] {α : Type u} [MeasurableSpace α] (x : α) : 𝒟[pure x] = MeasureTheory.Measure.dirac x

Pure optional computations have Dirac successful-output semantics.

@[instance 20]

instance instLawfulPureEvalDistSemanticsOptionT {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulPureEvalDistSemantics m] : LawfulPureEvalDistSemantics (OptionT m)

Native optional semantics preserves pure whenever the base semantics does.

theorem OptionT.evalDist_failure {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulPureEvalDistSemantics m] {α : Type u} [MeasurableSpace α] : 𝒟[failure] = 0

Optional failure has no successful-output mass.

@[instance 20]

instance instLawfulFailureEvalDistSemanticsOptionT {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulPureEvalDistSemantics m] : LawfulFailureEvalDistSemantics (OptionT m)

Native optional failure has zero measure whenever the base semantics preserves pure.

@[simp]

theorem OptionT.evalDist_lift {m : Type u → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type u} [MeasurableSpace α] (mx : m α) : 𝒟[OptionT.lift mx] = 𝒟[mx]

Lifting a computation into OptionT preserves its successful-output measure.

instance OptionT.isProbabilityMeasure_evalDist_lift {m : Type u → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type u} [MeasurableSpace α] (mx : m α) [MeasureTheory.IsProbabilityMeasure 𝒟[mx]] : MeasureTheory.IsProbabilityMeasure 𝒟[OptionT.lift mx]

Lifting a lossless computation into the optional monad preserves its probability measure.

instance OptionT.isProbabilityMeasure_evalDist_liftM {m : Type u → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type u} [MeasurableSpace α] (mx : m α) [MeasureTheory.IsProbabilityMeasure 𝒟[mx]] : MeasureTheory.IsProbabilityMeasure 𝒟[liftM mx]

A monadic lift into the optional monad preserves a known probability measure.

theorem OptionT.evalDist_map {m : Type u → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (mx : OptionT m α) (f : α → β) (hf : Measurable f) : 𝒟[f <$> mx] = MeasureTheory.Measure.map f 𝒟[mx]

A measurable map of successful optional results is the measure pushforward.

theorem OptionT.evalDist_bind {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (mx : OptionT m α) (f : α → OptionT m β) (hf : Measurable fun (x : α) => 𝒟[(f x).run]) : 𝒟[mx >>= f] = 𝒟[mx].bind fun (x : α) => 𝒟[f x]

A measurable family of full run measures suffices to compose native optional denotations.

theorem OptionT.evalDist_bind_of_discrete {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [DiscreteMeasurableSpace α] [MeasurableSpace β] (mx : OptionT m α) (f : α → OptionT m β) : 𝒟[mx >>= f] = 𝒟[mx].bind fun (x : α) => 𝒟[f x]

Discrete intermediate values discharge the run-measurability premise of OptionT.evalDist_bind.

@[instance 20]

instance instLawfulEvalDistSemanticsOptionT {m : Type u → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] : LawfulEvalDistSemantics (OptionT m)

Native optional semantics satisfies the measurable-bind law for successful-output families. The full-run observer refines the source space, whose identity map transports the source measure.

@[simp]

theorem OptionT.dropNone_evalDist_run_bind_guard_apply_univ {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} (mx : m α) (p : α → Prop) [DecidablePred p] : 𝒟[do let x ← mx (guard (p x)).run].dropNone Set.univ = 𝒟[do let x ← mx pure (p x)] {True}

The effect-native successful-output measure of sampling and then guarding is the measure of the corresponding Boolean event. This statement is independent of which global OptionT semantics wins instance synthesis.