natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
The distribution monad is a monad on Set, whose algebras are convex spaces.
It can be thought of as the finitary prototype of a probability monad.
Let $X$ be a set. Define $D X$ as the set whose elements are functions $p:X\to[0,1]$ such that
$p(x)\ne 0$ for only finitely many $x$, and
$\sum_{x\in X} p(x)=1$.
Note that the sum above is finite if one excludes all the zero addenda.
The elements of $D X$ are called finite distributions or finitely-supported probability measures over $X$.
Given a function $f:X\to Y$, one defines the pushforward $D f:D X\to D Y$ as follows. Given $p\in D X$, then $(D f)(p)\in D Y$ is the function
(Note that, up to zero addenda, the sum above is again finite.)
Compare with the pushforward of measures.
This makes $D$ into an endofunctor on Set.
The unit map $\delta:X\to D X$ maps the element $x\in X$ to the function $\delta_x:X\to[0,1]$ given by
Compare with the Dirac measures and valuations.
The multiplication map $E:D D X\to D X$ maps $\xi\in D D X$ to the function $E\xi\in D X$ given by
(Note that, up to zero addenda, the sum above is once again finite.)
The maps $E$ and $\delta$ satisfy the usual monad laws. The resulting monad $(D,E,\delta)$ is known as distribution monad, or finitary Giry monad (in analogy with the Giry monad), or convex combination monad, since the elements of $D X$ can be interpreted as formal convex combinations of elements of $X$.
This can be seen as a discrete, finitary analogue of a probability monad, where one replaces integrals by sums.
The algebras of $D$ are convex spaces.
The monad $D$ is finitary, and commutative.
The Kleisli morphisms of $D$ are (finitary) stochastic maps.
(…)
Giry monad, probabilistic powerdomain?, extended probabilistic powerdomain
Tobias Fritz and Paolo Perrone, Monads, partial evaluations, and rewriting, MFPS 36, 2020 - Section 6. (arXiv)
Bart Jacobs, From probability monads to commutative effectuses, Journal of Logical and Algebraic Methods in Programming 94, 2018.
Tobias Fritz, Convex spaces I: definitions and examples, 2009. (arXiv:0903.5522)
Last revised on May 17, 2020 at 00:32:33. See the history of this page for a list of all contributions to it.