On the one hand, a statistical programming language is similar to a traditional programming language, but with libraries providing statistical functions. Examples are Mathematica, MATLAB, and the omnipresent R. On the other hand, probabilistic programming aims at providing a model of a probabilistic function or distribution as a program written in a programming language. As an example, WebPPL is a probabilistic extension of JavaScript. Essentially, we define a probabilistic function not mathematically, but as a program that computes an output using a sample from a specific given distribution function. Statistical probabilistic programming aims at their seamless combination.

When writing a program in a traditional programming language, each one of its executions must provide an output for each given input. However, when reasoning about programs, we usually cannot compute all the possible executions and use other techniques. A very common one is compositionality. That is, we obtain properties of a given program by composing properties of its inner parts.

But when writing a probabilistic program, there is no given input--we are not interested in specific data, but in input distribution functions. That is, the notion of an execution in a traditional program is related not to a concrete execution of the probabilistic program, but to executing the program many times using specific input data taken from an uncertainty distribution and extrapolating the probability associated to the output generated from each input. But reasoning about probabilistic programs becomes much more difficult, and compositionality is a must.

This paper explores how the commutativity property of compositionality fails in statistical probabilistic programming and provides a denotational semantics for statistical probabilistic programming with recursive types. The authors use quasi-Borel predomains, which are “a mixture of chain-complete partial orders (CPOs) and quasi-Borel spaces.”

The main language is statistical FPC (SFPC), a statistical variant of fixed-point calculus (FPC), including sum, product, function, and recursive types; real numbers and measurable functions from reals into reals; a construct for testing real numbers for zero; a construct for random numbers; and a construct for soft constraints.