Bundled Probability Semantics

This file defines bundled semantics for monads that factor through an internal semantic monad before being externally observed.

The existing classes HasEvalSPMF and HasEvalPMF say that a monad already has an SPMF or PMF denotation. That is convenient when the monad itself is the semantic object, but it is too rigid for constructions whose natural semantics has hidden internal structure.

The main new idea here is to split semantics into two stages:

1. interpret: map computations in the user-facing monad into an internal semantic monad
2. observe: forget the internal bookkeeping and expose only the probabilistic behavior

This is useful when the internal semantics carries extra state or other information that should not be visible at the final security-game interface. Typical examples include:

• oracle caches modeled by hidden state
• auxiliary logs or bookkeeping used only for the semantics
• semantic monads that are more structured than the surface monad being specified

The generic factoring pattern is captured by SemanticsVia. The probability-specific notions SPMFSemantics and PMFSemantics are then specializations where the observation target is respectively SPMF or PMF.

These semantics are deliberately bundled rather than typeclasses so that a construction can carry its intended semantics locally without forcing a single global instance on the ambient monad.

Design Note

The fields are intentionally minimal:

• Sem is the internal semantic monad
• interpret embeds the surface computation into that internal semantics
• observe discards the internal structure and returns the external semantic object

Notably, observation is not required to be a monad morphism. That is important: running a stateful semantics from a fixed initial state is a perfectly reasonable observation, but it is not itself a monad homomorphism. The bundling here leaves room for that style of semantics.

structure SemanticsVia (m : Type u → Type v) [Monad m] (Obs : Type u → Type x) : Type (max (max (max (u + 1) v) (w + 1)) x)

Bundled semantics for m obtained by factoring through an internal semantic monad.

SemanticsVia m Obs packages the very general pattern:

1. interpret a computation in the surface monad m into some internal semantic monad Sem
2. observe the resulting internal computation as an external semantic object Obs α

The observation target Obs is intentionally generic. In this file we mainly care about the cases Obs = SPMF and Obs = PMF, but the same factoring pattern could later be reused for other kinds of denotational semantics such as sets of outcomes, traces, or quantum objects.

The important asymmetry is that interpret is required to be a monad morphism, while observe is not. This lets us model semantics where running the internal computation requires fixing hidden state or discarding auxiliary structure before exposing the final denotation.

• Sem : Type u → Type w

  Internal monad used to give denotational meaning to computations in m.

• instMonadSem : Monad self.Sem

  Monad structure on the internal semantic monad.

• interpret : m →ᵐ self.Sem

  Interpret a surface computation into the internal semantic monad.

• observe {α : Type u} : self.Sem α → Obs α

  Observe the internal semantic computation as an external semantic object, forgetting any hidden internal structure.

def SemanticsVia.denote {m : Type u → Type v} [Monad m] {Obs : Type u → Type x} {α : Type u} (sem : SemanticsVia m Obs) (mx : m α) : Obs α

The external denotation of mx under a bundled semantics factorization.

structure SPMFSemantics (m : Type u → Type v) [Monad m] extends SemanticsVia m SPMF : Type (max (max (u + 1) (u_1 + 1)) v)

Bundled subprobabilistic semantics for a monad m.

This is the specialization of SemanticsVia where the external observation target is SPMF. Computations in m are therefore interpreted as subprobability distributions on outputs, possibly with failure mass.

• Sem : Type u → Type u_1
• instMonadSem : Monad self.Sem
• interpret : m →ᵐ self.Sem
• observe {α : Type u} : self.Sem α → SPMF α

@[implicit_reducible]

instance instMonadSemSPMF {m : Type u → Type v} [Monad m] (sem : SPMFSemantics m) : Monad sem.Sem

The internal semantic monad of an SPMFSemantics carries the inherited monad structure.

def SPMFSemantics.observeSPMF {m : Type u → Type v} [Monad m] (sem : SPMFSemantics m) {α : Type u} : sem.Sem α → SPMF α

The observation map of an SPMFSemantics, specialized to SPMF.

def SPMFSemantics.evalDist {m : Type u → Type v} [Monad m] {α : Type u} (sem : SPMFSemantics m) (mx : m α) : SPMF α

The subdistribution denoted by mx under the bundled semantics sem.

This first moves mx into the internal semantic monad via interpret, and then collapses the internal structure to the externally visible SPMF via observeSPMF.

def SPMFSemantics.probFailure {m : Type u → Type v} [Monad m] {α : Type u} (sem : SPMFSemantics m) (mx : m α) : ENNReal

The probability that mx fails to return a value under sem.

Since SPMFSemantics is subprobabilistic, failure is represented by the missing mass of the resulting SPMF, equivalently the probability of none in the underlying Option-valued PMF.

@[simp]

theorem SPMFSemantics.probFailure_le_one {m : Type u → Type v} [Monad m] {α : Type u} (sem : SPMFSemantics m) (mx : m α) : sem.probFailure mx ≤ 1

Failure probability under an SPMFSemantics is always at most 1.

def SPMFSemantics.ofHasEvalSPMF (m : Type u → Type v) [Monad m] [HasEvalSPMF m] : SPMFSemantics m

Package an ordinary HasEvalSPMF instance as a bundled SPMFSemantics.

This is the bridge back to the old style where the surface monad itself already carries its subprobabilistic denotation. In that case the internal semantic monad is just m itself, the interpreter is the identity monad morphism, and observation is HasEvalSPMF.toSPMF.

@[simp]

theorem SPMFSemantics.ofHasEvalSPMF_evalDist {m : Type u → Type v} [Monad m] {α : Type u} (mx : m α) [HasEvalSPMF m] : (SPMFSemantics.ofHasEvalSPMF m).evalDist mx = (fun {α : Type u} (x : m α) => HasEvalSPMF.toSPMF.toFun α x) mx

@[simp]

theorem SPMFSemantics.ofHasEvalSPMF_probFailure {m : Type u → Type v} [Monad m] {α : Type u} (mx : m α) [HasEvalSPMF m] : (SPMFSemantics.ofHasEvalSPMF m).probFailure mx = Pr[⊥ | mx]

structure PMFSemantics (m : Type u → Type v) [Monad m] extends SemanticsVia m PMF : Type (max (max (u + 1) (u_1 + 1)) v)

Bundled total probabilistic semantics for a monad m.

This is the specialization of SemanticsVia where the external observation target is PMF. There is therefore no failure mass in the resulting denotation.

• Sem : Type u → Type u_1
• instMonadSem : Monad self.Sem
• interpret : m →ᵐ self.Sem
• observe {α : Type u} : self.Sem α → PMF α

@[implicit_reducible]

instance instMonadSemPMF {m : Type u → Type v} [Monad m] (sem : PMFSemantics m) : Monad sem.Sem

The internal semantic monad of a PMFSemantics carries the inherited monad structure.

def PMFSemantics.observePMF {m : Type u → Type v} [Monad m] (sem : PMFSemantics m) {α : Type u} : sem.Sem α → PMF α

The observation map of a PMFSemantics, specialized to PMF.

def PMFSemantics.evalDist {m : Type u → Type v} [Monad m] {α : Type u} (sem : PMFSemantics m) (mx : m α) : PMF α

The total distribution denoted by mx under the bundled semantics sem.

noncomputable def PMFSemantics.toSPMFSemantics {m : Type u → Type v} [Monad m] (sem : PMFSemantics m) : SPMFSemantics m

Forget that a total semantics is total, yielding the underlying subprobabilistic semantics.

This simply postcomposes observation with the canonical embedding PMF α → SPMF α. The resulting SPMFSemantics has zero failure probability, but it can now be consumed by APIs that are stated in terms of subprobabilistic semantics.

def PMFSemantics.ofHasEvalPMF (m : Type u → Type v) [Monad m] [HasEvalPMF m] : PMFSemantics m

Package an ordinary HasEvalPMF instance as a bundled PMFSemantics.

As with SPMFSemantics.ofHasEvalSPMF, this recovers the familiar case where the surface monad already comes with a total probabilistic denotation.

@[simp]

theorem PMFSemantics.ofHasEvalPMF_evalDist {m : Type u → Type v} [Monad m] {α : Type u} (mx : m α) [HasEvalPMF m] : (PMFSemantics.ofHasEvalPMF m).evalDist mx = (fun {α : Type u} (x : m α) => HasEvalPMF.toPMF.toFun α x) mx