Probability Semantics for Polynomial Free Monads

This module equips an arbitrary polynomial functor with per-operation probability semantics and interprets its free monad in PMF. It also provides the syntax-only support interpretation in SetM. The API is independent of OracleSpec; oracle computations inherit it through their underlying polynomial functor.

class PFunctor.IsProbabilitySpec (P : PFunctor.{uA, u}) : Type (max u uA)

Per-operation probability distributions for a polynomial interface.

• toPMF : Handler PMF P

  The distribution of directions available at an operation.

class PFunctor.IsUniformSpec (P : PFunctor.{uA, u}) extends P.IsProbabilitySpec : Type (max u uA)

A finitely branching polynomial interface whose operation responses use the canonical uniform distribution.

• toPMF : Handler PMF P
• fintype (a : P.A) : Fintype (P.B a)

  Every direction type is finite.

• inhabited (a : P.A) : Inhabited (P.B a)

  Every direction type is inhabited.

• toPMF_eq_uniform (operation : P.A) : IsProbabilitySpec.toPMF operation = PMF.uniformOfFintype (P.B operation)

  Each operation uses the canonical uniform distribution on directions.

@[reducible]

noncomputable def PFunctor.IsUniformSpec.ofFintypeInhabited (P : PFunctor.{uA, u}) [hF : (a : P.A) → Fintype (P.B a)] [hI : (a : P.A) → Inhabited (P.B a)] : P.IsUniformSpec

Construct uniform probability semantics from finite, inhabited direction types. This is deliberately not an instance: probability semantics remain an explicit opt-in.

@[instance_reducible]

noncomputable instance PFunctor.FreeM.instMonadLiftTPMF {P : PFunctor.{uA, u}} [P.IsProbabilitySpec] : MonadLiftT P.FreeM PMF

Interpret a polynomial free program using its per-operation probability distributions.

instance PFunctor.FreeM.instLawfulMonadLiftTPMF {P : PFunctor.{uA, u}} [P.IsProbabilitySpec] : LawfulMonadLiftT P.FreeM PMF

@[instance_reducible]

instance PFunctor.FreeM.instMonadLiftTSetM {P : PFunctor.{uA, u}} : MonadLiftT P.FreeM SetM

Interpret support syntactically by allowing every direction at every operation. This does not require probability or finiteness assumptions.

instance PFunctor.FreeM.instLawfulMonadLiftTSetM {P : PFunctor.{uA, u}} : LawfulMonadLiftT P.FreeM SetM

theorem PFunctor.FreeM.evalSPMF_eq_liftM {P : PFunctor.{uA, u}} {α : Type u} [P.IsProbabilitySpec] (program : P.FreeM α) : 𝒮[program] = liftM (FreeM.liftM IsProbabilitySpec.toPMF program)

The distribution semantics of a polynomial free program is its universal fold into PMF.

theorem PFunctor.FreeM.support_eq_liftM {P : PFunctor.{uA, u}} {α : Type u} (program : P.FreeM α) : support program = (FreeM.liftM (fun (x : P.A) => Set.univ) program).run

The support semantics of a polynomial free program is its universal fold with every operation direction available.

@[simp]

theorem PFunctor.FreeM.evalSPMF_lift {P : PFunctor.{uA, u}} [P.IsProbabilitySpec] (operation : P.A) : 𝒮[lift operation] = liftM (IsProbabilitySpec.toPMF operation)

A single operation evaluates to its configured direction distribution.

theorem PFunctor.FreeM.evalSPMF_lift_eq_uniform {P : PFunctor.{uA, u}} [h : P.IsUniformSpec] (operation : P.A) : 𝒮[lift operation] = liftM (PMF.uniformOfFintype (P.B operation))

A single operation on a uniform polynomial interface evaluates to the canonical uniform distribution on its directions.

theorem PFunctor.FreeM.support_lift_eq_univ {P : PFunctor.{uA, u}} (operation : P.A) : support (lift operation) = Set.univ

Every direction of a single operation belongs to its SetM-fold support.

This name distinguishes VCVio's denotational support from PolyFun's structural MonadAttach.support_lift theorem.

@[instance 100]

instance PFunctor.FreeM.instEvalDistCompatible {P : PFunctor.{uA, u}} [uniform : P.IsUniformSpec] : EvalDistCompatible P.FreeM

Syntactic support and distribution support agree for a uniformly interpreted polynomial free monad.

For an oracle spec this is reached explicitly, not by synthesis: OracleComp.instEvalDistCompatible supplies the IsUniformSpec premise through OracleSpec.IsUniformSpec.toPFunctor, which is deliberately a definition rather than an instance so that nothing unifies against the reducible head spec.toPFunctor. Keep it that way — promoting that conversion would make this instance and the oracle-level one both applicable to the same goal.