Native measure semantics for polynomial free monads

This module interprets a polynomial free program directly as a Mathlib Measure. Each operation is assigned a probability measure on its answer type, and PFunctor.FreeM.denote recursively composes those measures with Measure.bind when the continuation is almost everywhere measurable. An unmeasurable continuation denotes zero. This convention makes the fold subprobabilistic without depending on Mathlib's arbitrary default for an unmeasurable pushforward.

Measure α becomes a type only after α receives a MeasurableSpace, so this interpretation is an explicit fold rather than an unrestricted Lean monad morphism. The measurable-continuation boundary remains visible in the general laws. Discrete answer types discharge the internal measurability obligations while leaving the result space arbitrary.

Main definitions

• PFunctor.IsMeasureSpec assigns a probability measure to each operation.
• PFunctor.IsMeasureSpec.uniformOfFiniteNonempty assigns the native uniform measure to every finite, nonempty answer type.
• PFunctor.FreeM.denote is the measure denoted by a free program.

Main statements

• PFunctor.FreeM.denote_lift identifies the denotation of one operation.
• PFunctor.FreeM.denote_bind_of_discrete and PFunctor.FreeM.denote_map_of_discrete give the discrete Giry composition laws.
• PFunctor.FreeM.denote_bind_bind_prod_mk_eq_prod identifies two independent executions with Mathlib's product measure.

class PFunctor.IsMeasureSpec (P : PFunctor.{uA, u}) [(a : P.A) → MeasurableSpace (P.B a)] : Type (max u uA)

Per-operation answer measures for a polynomial interface.

The measurable structure on answer types is a separate parameter rather than a field, mirroring Mathlib's separation of MeasurableSpace from the measures carried on it. Answer types need not be discrete.

• toMeasure (a : P.A) : MeasureTheory.Measure (P.B a)

  The distribution of answers to an operation.

• isProbabilityMeasure (a : P.A) : MeasureTheory.IsProbabilityMeasure (toMeasure a)

  Answering an operation is lossless.

@[reducible]

noncomputable def PFunctor.IsMeasureSpec.uniformOfFiniteNonempty (P : PFunctor.{uA, u}) [∀ (a : P.A), Finite (P.B a)] [∀ (a : P.A), Nonempty (P.B a)] [(a : P.A) → MeasurableSpace (P.B a)] : P.IsMeasureSpec

Construct native uniform measure semantics from finite, nonempty answer types.

This is deliberately not an instance: measure semantics remain an explicit choice at each use site, and are never inferred merely from finiteness.

noncomputable def PFunctor.FreeM.denote {P : PFunctor.{uA, u}} [(a : P.A) → MeasurableSpace (P.B a)] [P.IsMeasureSpec] {α : Type v} [MeasurableSpace α] : P.FreeM α → MeasureTheory.Measure α

The measure denoted by a polynomial free program. A measurable continuation uses Giry bind; an unmeasurable continuation denotes zero. Probability-mass preservation requires measurability.

@[simp]

theorem PFunctor.FreeM.denote_pure {P : PFunctor.{uA, u}} [(a : P.A) → MeasurableSpace (P.B a)] [P.IsMeasureSpec] {α : Type v} [MeasurableSpace α] (x : α) : (pure x).denote = MeasureTheory.Measure.dirac x

theorem PFunctor.FreeM.denote_liftBind {P : PFunctor.{uA, u}} [(a : P.A) → MeasurableSpace (P.B a)] [P.IsMeasureSpec] {α : Type v} [MeasurableSpace α] (a : P.A) (cont : P.B a → P.FreeM α) (h : AEMeasurable (fun (b : P.B a) => (cont b).denote) (IsMeasureSpec.toMeasure a)) : (liftBind a cont).denote = (IsMeasureSpec.toMeasure a).bind fun (b : P.B a) => (cont b).denote

theorem PFunctor.FreeM.denote_liftBind_of_not_aemeasurable {P : PFunctor.{uA, u}} [(a : P.A) → MeasurableSpace (P.B a)] [P.IsMeasureSpec] {α : Type v} [MeasurableSpace α] (a : P.A) (cont : P.B a → P.FreeM α) (h : ¬AEMeasurable (fun (b : P.B a) => (cont b).denote) (IsMeasureSpec.toMeasure a)) : (liftBind a cont).denote = 0

An unmeasurable operation continuation has zero denotation.

@[simp]

theorem PFunctor.FreeM.denote_lift {P : PFunctor.{uA, u}} [(a : P.A) → MeasurableSpace (P.B a)] [P.IsMeasureSpec] (a : P.A) : (lift a).denote = IsMeasureSpec.toMeasure a

A one-operation program denotes its configured answer measure.

theorem PFunctor.FreeM.isProbabilityMeasure_denote_liftBind {P : PFunctor.{uA, u}} [(a : P.A) → MeasurableSpace (P.B a)] [P.IsMeasureSpec] {α : Type v} [MeasurableSpace α] (a : P.A) (cont : P.B a → P.FreeM α) (hMeasurable : AEMeasurable (fun (b : P.B a) => (cont b).denote) (IsMeasureSpec.toMeasure a)) (hProbability : ∀ᵐ (b : P.B a) ∂IsMeasureSpec.toMeasure a, MeasureTheory.IsProbabilityMeasure (cont b).denote) : MeasureTheory.IsProbabilityMeasure (liftBind a cont).denote

A one-operation program is a probability measure whenever its continuation is an almost-everywhere measurable family of probability measures.

This is the continuous composition boundary. For discrete answer types the hypotheses are automatic; for a genuinely continuous oracle they are precisely the obligations represented by a Mathlib Kernel.

Giry composition laws

instance PFunctor.FreeM.isProbabilityMeasure_denote {P : PFunctor.{uA, u}} [(a : P.A) → MeasurableSpace (P.B a)] [P.IsMeasureSpec] {α : Type v} [∀ (a : P.A), DiscreteMeasurableSpace (P.B a)] [MeasurableSpace α] (program : P.FreeM α) : MeasureTheory.IsProbabilityMeasure program.denote

Every program over discrete answer types denotes a probability measure, independently of the measurable space on its output.

theorem PFunctor.FreeM.denote_bind {P : PFunctor.{uA, u}} [(a : P.A) → MeasurableSpace (P.B a)] [P.IsMeasureSpec] {α : Type v} {β : Type w} [∀ (a : P.A), DiscreteMeasurableSpace (P.B a)] [MeasurableSpace α] [MeasurableSpace β] (program : P.FreeM α) (f : α → P.FreeM β) (hf : Measurable fun (x : α) => (f x).denote) : (program.bind f).denote = program.denote.bind fun (x : α) => (f x).denote

denote preserves bind when the denoted continuation is measurable. Discrete answer types discharge the recursive measurability obligation inside the free program.

theorem PFunctor.FreeM.denote_bind_of_discrete {P : PFunctor.{uA, u}} [(a : P.A) → MeasurableSpace (P.B a)] [P.IsMeasureSpec] {α : Type v} {β : Type w} [∀ (a : P.A), DiscreteMeasurableSpace (P.B a)] [MeasurableSpace α] [DiscreteMeasurableSpace α] [MeasurableSpace β] (program : P.FreeM α) (f : α → P.FreeM β) : (program.bind f).denote = program.denote.bind fun (x : α) => (f x).denote

denote preserves bind unconditionally when the program's result type is discrete.

theorem PFunctor.FreeM.denote_map_of_measurable {P : PFunctor.{uA, u}} [(a : P.A) → MeasurableSpace (P.B a)] [P.IsMeasureSpec] {α : Type v} {β : Type w} [∀ (a : P.A), DiscreteMeasurableSpace (P.B a)] [MeasurableSpace α] [MeasurableSpace β] (program : P.FreeM α) (f : α → β) (hf : Measurable f) : (map f program).denote = MeasureTheory.Measure.map f program.denote

denote turns a measurable map of program outputs into the pushforward measure.

theorem PFunctor.FreeM.denote_map_of_discrete {P : PFunctor.{uA, u}} [(a : P.A) → MeasurableSpace (P.B a)] [P.IsMeasureSpec] {α : Type v} {β : Type w} [∀ (a : P.A), DiscreteMeasurableSpace (P.B a)] [MeasurableSpace α] [DiscreteMeasurableSpace α] [MeasurableSpace β] (program : P.FreeM α) (f : α → β) : (map f program).denote = MeasureTheory.Measure.map f program.denote

denote preserves every output map from a discrete result type.

theorem PFunctor.FreeM.denote_bind_bind_prod_mk_eq_prod {P : PFunctor.{uA, u}} [(a : P.A) → MeasurableSpace (P.B a)] [P.IsMeasureSpec] {α : Type v} {β : Type w} [∀ (a : P.A), DiscreteMeasurableSpace (P.B a)] [MeasurableSpace α] [DiscreteMeasurableSpace α] [MeasurableSpace β] (left : P.FreeM α) (right : P.FreeM β) : (left.bind fun (x : α) => right.bind fun (y : β) => pure (x, y)).denote = left.denote.prod right.denote

Sequentially running two programs whose second execution does not depend on the first result denotes the product of their measures.

theorem PFunctor.FreeM.denote_apply_univ_le_one {P : PFunctor.{uA, u}} [(a : P.A) → MeasurableSpace (P.B a)] [P.IsMeasureSpec] {α : Type u} [MeasurableSpace α] (program : P.FreeM α) : program.denote Set.univ ≤ 1

Every free program denotes a subprobability measure. Measurable continuations preserve the mass bound through integration; unmeasurable continuations have zero denotation.

@[instance_reducible, instance 20]

noncomputable instance PFunctor.FreeM.instEvalDistSemanticsFreeM {P : PFunctor.{uA, u}} [(a : P.A) → MeasurableSpace (P.B a)] [P.IsMeasureSpec] : EvalDistSemantics P.FreeM

The direct free-monad fold supplies measure semantics for a measure-valued specification.

@[instance 20]

instance PFunctor.FreeM.instLawfulPureEvalDistSemanticsFreeM {P : PFunctor.{uA, u}} [(a : P.A) → MeasurableSpace (P.B a)] [P.IsMeasureSpec] : LawfulPureEvalDistSemantics P.FreeM

The direct free-monad measure fold preserves pure without any discreteness assumption on oracle answers.

theorem PFunctor.FreeM.evalDist_eq_denote {P : PFunctor.{uA, u}} [(a : P.A) → MeasurableSpace (P.B a)] [P.IsMeasureSpec] {α : Type u} [MeasurableSpace α] (program : P.FreeM α) : 𝒟[program] = program.denote

With a measure specification in scope, primary notation is definitionally the direct free-monad measure fold. 𝒟[…] is the public head: this is a transport lemma, not a simp rule, so the 𝒟-keyed laws below and in Defs.Measure are the ones simp uses.

@[simp]

theorem PFunctor.FreeM.evalDist_lift {P : PFunctor.{uA, u}} [(a : P.A) → MeasurableSpace (P.B a)] [P.IsMeasureSpec] (a : P.A) : 𝒟[lift a] = IsMeasureSpec.toMeasure a

A one-operation program denotes its configured answer measure.

theorem PFunctor.FreeM.isProbabilityMeasure_evalDist_lift {P : PFunctor.{uA, u}} [(a : P.A) → MeasurableSpace (P.B a)] [P.IsMeasureSpec] (a : P.A) : MeasureTheory.IsProbabilityMeasure 𝒟[lift a]

A single operation denotes a probability measure, including for continuous answer spaces.

theorem PFunctor.FreeM.evalDist_liftBind {P : PFunctor.{uA, u}} [(a : P.A) → MeasurableSpace (P.B a)] [P.IsMeasureSpec] {α : Type u} [MeasurableSpace α] (a : P.A) (cont : P.B a → P.FreeM α) (h : AEMeasurable (fun (b : P.B a) => (cont b).denote) (IsMeasureSpec.toMeasure a)) : 𝒟[liftBind a cont] = (IsMeasureSpec.toMeasure a).bind fun (b : P.B a) => 𝒟[cont b]

An operation with an almost everywhere measurable continuation denotes Giry bind.

theorem PFunctor.FreeM.lintegral_evalDist_liftBind {P : PFunctor.{uA, u}} [(a : P.A) → MeasurableSpace (P.B a)] [P.IsMeasureSpec] {α : Type u} [MeasurableSpace α] (a : P.A) (cont : P.B a → P.FreeM α) (hcont : AEMeasurable (fun (b : P.B a) => 𝒟[cont b]) (IsMeasureSpec.toMeasure a)) {g : α → ENNReal} (hg : AEMeasurable g 𝒟[liftBind a cont]) : ∫⁻ (y : α), g y ∂𝒟[liftBind a cont] = ∫⁻ (b : P.B a), ∫⁻ (y : α), g y ∂𝒟[cont b] ∂IsMeasureSpec.toMeasure a

Integrating a single operation uses the tower law under AE-measurable continuation and valuation hypotheses, including for continuous query answers.

theorem PFunctor.FreeM.evalDist_lift_bind_pure {P : PFunctor.{uA, u}} [(a : P.A) → MeasurableSpace (P.B a)] [P.IsMeasureSpec] {α : Type u} [MeasurableSpace α] (a : P.A) (f : P.B a → α) (hf : Measurable f) : 𝒟[do let b ← lift a pure (f b)] = MeasureTheory.Measure.map f 𝒟[lift a]

A measurable pure function after one operation pushes forward its answer measure. No discreteness assumption on the answer space is needed.

instance PFunctor.FreeM.instIsProbabilityMeasureEvalDist {P : PFunctor.{uA, u}} [(a : P.A) → MeasurableSpace (P.B a)] [P.IsMeasureSpec] {α : Type u} [∀ (a : P.A), DiscreteMeasurableSpace (P.B a)] [MeasurableSpace α] (program : P.FreeM α) : MeasureTheory.IsProbabilityMeasure 𝒟[program]

@[instance 20]

instance PFunctor.FreeM.instLawfulEvalDistSemanticsFreeM {P : PFunctor.{uA, u}} [(a : P.A) → MeasurableSpace (P.B a)] [P.IsMeasureSpec] [∀ (a : P.A), DiscreteMeasurableSpace (P.B a)] : LawfulEvalDistSemantics P.FreeM

Over a discrete-answer interface, the direct measure semantics satisfies the Giry monad laws.