Statistical programming with categorical measure theory & LazyPPL

Swaraj Dash, Younesse Kaddar, Hugo Paquet, Sam Staton

Probabilistic Programming

Bayes’ law

• sample: prior
• observe: likelihood, conditioning on the observed datapoints $d$
• infer/normalize: posterior, inference from effects (observations $d$) to causes (parameters $x$)

Demo

Semantically

Inference:

• pick a parameter $p$ by sampling a point from the area under the curve of the weight function $l$
• use this parameter $p$ to determine a result $r(p)$.

Problems

• $\cal Meas$ not cartesian closed:

  • no function space like Double -> Double

• Not known if there is a strong monad of measures

  • the category of s-finite kernels is distributive symmetric monoidal
  • but is it a Kleisli category?

Inverse Transform Sampling

Noise outsourcing lemma: The law of every Borel-valued random variable can be obtained as a pushforward of the uniform measure $[0,1]$.

Given a parameterized probability distribution $k：A → {\cal P} (B)$, there is a function $f： A × [0, 1] → B$ such that for all $a$,

Quasi-Borel Spaces

• $Ω$: fixed uncountable standard Borel space

  • LazyPPL: infinite rose trees, with splitting $γ：Ω ≅ Ω × Ω$

• quasi-Borel space $X$: set $M_X ⊆ X^{Ω}$ of random elements

• $Qbs$: cartesian closed, commutative monad of measures

  • LazyPPL: Prob vs Meas ⟶ two Kleisli categories
  • Laziness in program evaluation: monoidal category $\cal Kl(\texttt{Prob})$ has a terminal unit

Proba and Measure Kernels

• Prob: Probability kernels $f：X × Ω → Y$ modulo equivalence

  • Composition: $X × Ω \xrightarrow {X × γ} X × Ω × Ω \xrightarrow {f × Ω} Y × Ω \xrightarrow {g} Z$
  • Monad on $Qbs$: $X ↦ X^Ω$

• Meas: Measure kernels $[0, \infty] \xleftarrow{l} X × Ω \xrightarrow{f} Y$ mod equiv

  • Composition: compose the proba kernels, multiply the weights
  • Monad on $Qbs$: $X ↦ (X × ℝ)^Ω$

Correspondence

Demo

• Poisson point process
• Piecewise regression
• Program induction
• Wiener process
• More on https://lazyppl.bitbucket.io/!