Successful-output measures for deterministic computations

Id returns its unique value with Dirac measure. Option and Except assign Dirac measure to successful values and zero measure to failures. Error values need no measurable structure when only successful outputs are observed. These interpretations satisfy the measurable Giry laws.

@[instance_reducible, instance 20]

noncomputable instance instEvalDistSemanticsId : EvalDistSemantics Id

A deterministic total computation denotes its Dirac output measure.

@[simp]

theorem Id.evalDist_eq_dirac {α : Type u} [MeasurableSpace α] (mx : Id α) : 𝒟[mx] = MeasureTheory.Measure.dirac mx.run

The unique returned value determines a deterministic computation's measure.

instance Id.isProbabilityMeasure_evalDist {α : Type u} [MeasurableSpace α] (mx : Id α) : MeasureTheory.IsProbabilityMeasure 𝒟[mx]

Every deterministic total computation denotes a probability measure.

@[instance 20]

instance instLawfulEvalDistSemanticsId : LawfulEvalDistSemantics Id

Deterministic total computations respect the measurable Giry laws.

@[instance_reducible, instance 20]

noncomputable instance instEvalDistSemanticsOption : EvalDistSemantics Option

A deterministic optional result denotes zero on failure and a Dirac measure on success.

@[simp]

theorem Option.evalDist_none {α : Type u} [MeasurableSpace α] : 𝒟[none] = 0

An absent optional result has no successful-output mass.

@[instance 20]

instance instLawfulFailureEvalDistSemanticsOption : LawfulFailureEvalDistSemantics Option

Deterministic optional failure has zero successful-output measure.

@[simp]

theorem Option.evalDist_some {α : Type u} [MeasurableSpace α] (x : α) : 𝒟[some x] = MeasureTheory.Measure.dirac x

A present optional result has its Dirac output measure.

instance Option.isProbabilityMeasure_evalDist_some {α : Type u} [MeasurableSpace α] (x : α) : MeasureTheory.IsProbabilityMeasure 𝒟[some x]

A present optional result denotes a probability measure.

@[instance 20]

instance instLawfulEvalDistSemanticsOption : LawfulEvalDistSemantics Option

Deterministic optional computations respect the measurable Giry laws.

@[instance_reducible, instance 20]

noncomputable instance instEvalDistSemanticsExcept {ε : Type u} : EvalDistSemantics (Except ε)

A deterministic exceptional result assigns mass only to its successful output.

@[simp]

theorem Except.evalDist_error {ε : Type u} {α : Type v} [MeasurableSpace α] (error : ε) : 𝒟[Except.error error] = 0

An exceptional result has no successful-output mass.

@[simp]

theorem Except.evalDist_ok {ε : Type u} {α : Type v} [MeasurableSpace α] (x : α) : 𝒟[ok x] = MeasureTheory.Measure.dirac x

A successful exceptional result has its Dirac output measure.

instance Except.isProbabilityMeasure_evalDist_ok {ε : Type u} {α : Type v} [MeasurableSpace α] (x : α) : MeasureTheory.IsProbabilityMeasure 𝒟[ok x]

A successful exceptional result denotes a probability measure.

@[instance 20]

instance instLawfulEvalDistSemanticsExcept {ε : Type u} : LawfulEvalDistSemantics (Except ε)

Deterministic exceptional computations respect the measurable Giry laws.