Primary and discrete compatibility for free-program measure semantics

The dependency-light native fold lives in VCVio.EvalDist.PFunctorMeasure.Core. This module reexports the fold's primary EvalDistSemantics and connects it to the legacy discrete IsProbabilitySpec evaluator.

Main statements

• PFunctor.IsMeasureSpec.Compatible — the measure and probability specifications of an interface agree; IsProbabilitySpec.toMeasureSpec satisfies it definitionally.
• PFunctor.FreeM.denote_eq_toMeasure — under agreement, the fold is the measure of the PMF denotation of VCVio.EvalDist.PFunctor.
• The DiscreteEvalDistCompatible (FreeM P) instance — under agreement, 𝒟[…] satisfies the façade bridge, so evalDist_apply_singleton, evalDist_apply_setOf and lintegral_evalDist read existing Pr[…] facts off the measure denotation.

Agreement with the PMF denotation

For a polynomial interface carrying both interpretations compatibly, the measure denotation is the measure of the PMF denotation. This is what lets a Pr[…] statement proved against VCVio.EvalDist.PFunctor be transported here rather than reproved.

class PFunctor.IsMeasureSpec.Compatible (P : PFunctor.{uA, u}) [(a : P.A) → MeasurableSpace (P.B a)] [probSpec : P.IsProbabilitySpec] [measureSpec : P.IsMeasureSpec] : Prop

The measure and probability interpretations of an interface agree. Instances are explicit (IsProbabilitySpec.toMeasureSpec) or proved per interface, never derived from finiteness alone.

• toMeasure_eq (a : P.A) : toMeasure a = (IsProbabilitySpec.toPMF a).toMeasure

  Every answer measure is the measure of the answer distribution.

theorem PFunctor.FreeM.denote_eq_toMeasure {P : PFunctor.{uA, u}} [(a : P.A) → MeasurableSpace (P.B a)] [P.IsMeasureSpec] {α : Type u} [∀ (a : P.A), DiscreteMeasurableSpace (P.B a)] [P.IsProbabilitySpec] [IsMeasureSpec.Compatible P] [MeasurableSpace α] (program : P.FreeM α) : program.denote = (FreeM.liftM IsProbabilitySpec.toPMF program).toMeasure

@[instance_reducible]

noncomputable def PFunctor.IsProbabilitySpec.toMeasureSpec (P : PFunctor.{uA, u}) [(a : P.A) → MeasurableSpace (P.B a)] [P.IsProbabilitySpec] : P.IsMeasureSpec

Every PMF-valued interpretation induces a measure-valued one, by taking the measure of each answer distribution.

Deliberately not an instance, matching PFunctor.IsUniformSpec.ofFintypeInhabited: measure semantics stay an explicit opt-in rather than being derived silently wherever a PMF interpretation happens to be in scope. Introduce it with letI or a local instance at a use site; it is IsMeasureSpec.Compatible by rfl.

instance PFunctor.IsProbabilitySpec.toMeasureSpec_compatible (P : PFunctor.{uA, u}) [(a : P.A) → MeasurableSpace (P.B a)] [P.IsProbabilitySpec] : IsMeasureSpec.Compatible P

instance PFunctor.FreeM.instDiscreteEvalDistCompatibleOfCompatible {P : PFunctor.{uA, u}} [(a : P.A) → MeasurableSpace (P.B a)] [P.IsMeasureSpec] [∀ (a : P.A), DiscreteMeasurableSpace (P.B a)] [P.IsProbabilitySpec] [IsMeasureSpec.Compatible P] : DiscreteEvalDistCompatible P.FreeM

Under an agreeing measure specification the free-monad fold satisfies the façade bridge, so the generic evalDist_apply_singleton/evalDist_apply_setOf/lintegral_evalDist read existing Pr[…] facts off the measure denotation.