Successful-output measure semantics for exceptional computations

An ExceptT ε m computation denotes the pullback of its underlying Except ε α-valued measure along the measurable embedding Except.ok. Errors are therefore missing successful mass, while the effect-preserving denotation remains available by observing mx.run directly.

The construction uses Mathlib's Measure.comap; no transformer-specific measure operation is needed. Native pure, map, and bind laws inherit the base monad's measure laws. Successful-output measurability suffices for the full bind law, without requiring the error family to be measurable.

@[instance_reducible, instance 20]

noncomputable instance instEvalDistSemanticsExceptT {ε : Type u} [MeasurableSpace ε] {m : Type u → Type v} [EvalDistSemantics m] : EvalDistSemantics (ExceptT ε m)

Interpret successful ExceptT results by pulling the run measure back along Except.ok.

theorem ExceptT.evalDist_eq_comap_ok {ε : Type u} [MeasurableSpace ε] {m : Type u → Type v} [EvalDistSemantics m] {α : Type u} [MeasurableSpace α] (mx : ExceptT ε m α) : 𝒟[mx] = MeasureTheory.Measure.comap Except.ok 𝒟[mx.run]

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

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

The successful-output measure of an exceptional computation on an event is the run measure of the corresponding Except.ok outcomes.

@[simp]

theorem ExceptT.evalDist_apply_univ {ε : Type u} [MeasurableSpace ε] {m : Type u → Type v} [EvalDistSemantics m] {α : Type u} [MeasurableSpace α] (mx : ExceptT ε m α) : 𝒟[mx] Set.univ = 𝒟[mx.run] (Set.range Except.ok)

The total successful mass of an exceptional computation is the mass of its ok branch.

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

Pure exceptional computations have Dirac successful-output semantics.

@[instance 20]

instance instLawfulPureEvalDistSemanticsExceptT {ε : Type u} [MeasurableSpace ε] {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulPureEvalDistSemantics m] : LawfulPureEvalDistSemantics (ExceptT ε m)

Native exceptional semantics preserves pure whenever the base semantics does.

@[simp]

theorem ExceptT.evalDist_throw {ε : Type u} [MeasurableSpace ε] {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulPureEvalDistSemantics m] {α : Type u} [MeasurableSpace α] (error : ε) : 𝒟[throw error] = 0

Throwing an exception carries no successful-output mass.

@[simp]

theorem ExceptT.evalDist_liftM {ε : Type u} [MeasurableSpace ε] {m : Type u → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type u} [MeasurableSpace α] (mx : m α) : 𝒟[liftM mx] = 𝒟[mx]

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

instance ExceptT.isProbabilityMeasure_evalDist_liftM {ε : Type u} [MeasurableSpace ε] {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]

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

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

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

theorem ExceptT.evalDist_bind {ε : Type u} [MeasurableSpace ε] {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (mx : ExceptT ε m α) (f : α → ExceptT ε 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 exceptional denotations.

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

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

@[instance 20]

instance instLawfulEvalDistSemanticsExceptT {ε : Type u} [MeasurableSpace ε] {m : Type u → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] : LawfulEvalDistSemantics (ExceptT ε m)

Native exceptional 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.