โ† back to index

Bimonadality of Probability Monads (Support as Monad Morphism)

Fritz, Perrone, Rezagholi ยท 2021 ยท arxiv arXiv:1910.03752

Prereqs: ๐Ÿž Fritz 2020 (Markov categories, support). 5 min.

The map "which outcomes are possible?" โ€” dropping probabilities and keeping only the support โ€” is a monad morphism. It respects composition: the support of a composed pipeline equals the composition of supports.

The possibilistic shadow

Every probability distribution has a possibilistic shadow: forget the weights, keep only which outcomes can happen. This maps the probability monad P to the powerset monad ๐’ซ. The shadow is a monad morphism โ€” it preserves pure and bind.

0.5 a 0 b 0.3 c 0 d 0.2 e support = (a, c, e). Zero-probability outcomes are not in the support.
Scheme

support_pure โ€” pure maps to singleton

The pure (return) of the probability monad wraps a value in a point-mass distribution: pure(x) = {x: 1.0}. Its shadow is a singleton set: {x}. That's exactly the pure of the powerset monad. So support preserves pure.

Scheme

Confidence: Exact. This is the unit law for the monad morphism.

support_bind โ€” support commutes with bind

This is the key theorem. If you compose two stochastic functions and then take the support, you get the same result as taking each support first and then composing the set-valued functions. In notation: supp(f >=> g) = supp(f) >=>_๐’ซ supp(g). Support is a monad morphism because it preserves the monad multiplication (bind).

Scheme

Confidence: Simplified. Finite sets, not measurable spaces. Same algebraic law.

Why possibilistic reasoning is sound

Because support is a monad morphism, you can reason about reachability (what can happen) without tracking exact probabilities. If a state is unreachable through a composed system, it's unreachable through each stage individually. Possibilistic gating โ€” reject impossible outcomes โ€” doesn't need exact probability computation.

Scheme

The monad morphism square

A monad morphism ฯƒ: T โ†’ S satisfies two laws: ฯƒ โˆ˜ ฮท_T = ฮท_S (preserve pure) and ฯƒ โˆ˜ ฮผ_T = ฮผ_S โˆ˜ (ฯƒฯƒ) (preserve multiplication). Support satisfies both. The first says "point mass โ†’ singleton." The second says "support of bind = bind of supports."

Scheme

Confidence: Exact. These are the defining equations, computed over finite lists.

Notation reference

Paper Scheme Meaning
P(X)list of (val . prob)Probability monad
๐’ซ(X)list of valPowerset monad
ฯƒ : P โ†’ ๐’ซsupportSupport = monad morphism
ฮทprob-pure / powerset-pureUnit (return)
ฮผapply append (flatten)Multiplication (join)
f >=> g(kleisli f g)Kleisli composition
Neighbors

Other paper pages

Foundations (Wikipedia)

Translation notes

All examples use finite lists of pairs as distributions. The paper works over arbitrary measurable spaces with the Giry monad, and support becomes a measurable map between ฯƒ-algebras. For example: the support_bind demonstration on this page composes two functions over small symbol sets. In the paper, the same law applies to Markov kernels between wpPolish spaces โ€” where "support" means the topological support of a probability measure, and the proof requires measurable selection theorems. The algebraic structure (support commutes with Kleisli composition) is identical. The measure theory is not.

Ready for the real thing? arxiv Read the paper. Start at ยง3 for the support monad morphism, ยง4 for the bimonadality result.

Framework connection: The possibilistic shadow justifies the Natural Framework's Filter stage doing reachability-based gating without exact probabilities. (jkAmbient Category)