# A Type Theory for Probability Density Functions

Abstract

There has been great interest in creating probabilistic programming languages to simplify the coding of statistical tasks; however, there still does not exist a formal language that simultaneously provides (1) continuous probability distributions, (2) the ability to naturally express custom probabilistic models, and (3) probability density functions (PDFs). This collection of features is necessary for mechanizing fundamental statistical techniques. We formalize the first probabilistic language that exhibits these features, and it serves as a foundational framework for extending the ideas to more general languages. Particularly novel are our type system for absolutely continuous (AC) distributions (those which permit PDFs) and our PDF calculation procedure, which calculates PDFs for a large class of AC distributions. Our formalization paves the way toward the rigorous encoding of powerful statistical reformulations.

Citation
Sooraj Bhat, Ashish Agarwal, Richard Vuduc, Alexander Gray (2012). A Type Theory for Probability Density Functions, Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012. ACM SIGPLAN Notices 47(1):545-556.

Errata
In Figure 10, the P-PLUS rule should be:
$\frac{{\Upsilon;\Lambda} \vdash {\varepsilon_1} \perp {\varepsilon_2} \qquad\{{\Upsilon;\Lambda} \vdash {\varepsilon_i} \leadsto {\delta_i}\}_{i=1,2}} {{\Upsilon;\Lambda} \vdash {\varepsilon_1+\varepsilon_2} \leadsto {\lambda {x:\mathsf{R}}\centerdot \int\lambda {t:\mathsf{R}}\centerdot\ \delta_1\ t * \delta_2\ (x – t)}}$
The $$t$$ and $$x$$ were accidentally transposed. Many thanks to Chung-chieh “Ken” Shan for finding this.

This entry was posted in Presentations, Publications and tagged , . Bookmark the permalink.

### One Response to A Type Theory for Probability Density Functions

1. Very nice. I am attending your talk at POPL right now. I would like to related work I have done in the past (MFPS’2009 in Oxford, published in ENTCS):
http://www.cs.bham.ac.uk/~mhe/papers/mma-mfps-revised.pdf

That paper also adds a type of distributions (using the probabilistic powerdomain as the denotational semantics), and can compute integration and semi-decide probabilitistic testing. There was a problem left open at the end, which Jean Goubault-Larrecq and Daniele Varacca solved in a LICS’2012 paper: http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GLV-lics2011.pdf