A Convenient Category for Higher-Order Probability Theory

TL;DR

This paper introduces quasi-Borel spaces as a new mathematical framework that enables higher-order probability modeling, supporting continuous distributions and higher-order functions, thus addressing limitations of traditional measure-theoretic probability.

Contribution

The paper presents quasi-Borel spaces as a novel formalization of probability theory that is cartesian closed and supports higher-order functions and continuous distributions.

Findings

Quasi-Borel spaces form a cartesian closed category for probability.

They support continuous probability distributions.

They enable a cleaner expression of probability constructions and generalize de Finetti's theorem.

Abstract

Higher-order probabilistic programming languages allow programmers to write sophisticated models in machine learning and statistics in a succinct and structured way, but step outside the standard measure-theoretic formalization of probability theory. Programs may use both higher-order functions and continuous distributions, or even define a probability distribution on functions. But standard probability theory does not handle higher-order functions well: the category of measurable spaces is not cartesian closed. Here we introduce quasi-Borel spaces. We show that these spaces: form a new formalization of probability theory replacing measurable spaces; form a cartesian closed category and so support higher-order functions; form a well-pointed category and so support good proof principles for equational reasoning; and support continuous probability distributions. We demonstrate the use of quasi-Borel spaces for higher-order functions and probability by: showing that a well-known construction of probability theory involving random functions gains a cleaner expression; and generalizing de Finetti's theorem, that is a crucial theorem in probability theory, to quasi-Borel spaces.

Equations

$${\int }_{X}f\mathrm{d}\mu \stackrel{\text{def}}{=}\underset{\{U_i\}}{\sup }\sum _i\left(\mu (U_i)\cdot \underset{x\in U_i}{\inf }f(x)\right)\text{,}$$

$${\int }_{X}f\mathrm{d}\mu \stackrel{\text{def}}{=}\left({\int }_X\max (0,f)\mathrm{d}\mu \right)-\left({\int }_X\max (0,-f)\mathrm{d}\mu \right)$$

$$\epsilon :\mathbf{Meas}(\mathbb{R},\mathbb{R})\times \mathbb{R}\to \mathbb{R}\text{with}\epsilon (f,r)=f(r)$$

$$M_{i}=\big{(}X_{i},\{\alpha\circ\iota~{}|~{}\alpha\in N_{i}\}\big{)}$$

$$\int f\mathrm{d}(\alpha ,\mu )\stackrel{\text{def}}{=}{\int }_{\mathbb{R}}(f\circ \alpha )\mathrm{d}\mu \text{.}$$

$${\Sigma }_{M_X}\stackrel{\text{def}}{=}\{U|\forall \alpha \in M_X.{\alpha }^{\text{-1}}(U)\in {\Sigma }_{\mathbb{R}}\}$$

$$\mathbf{Meas}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$M_{\Pi_{i}X_{i}}\stackrel{{\scriptstyle\textup{def}}}{{=}}\textstyle{\Big{\{}f\colon\mathbb{R}\to\prod_{i}X_{i}~{}|~{}\forall i.\,(\pi_{i}\circ f)\in M_{X_{i}}\Big{\}}\text{.}}$$

$$M_{{⨿}_i{X}_i}\stackrel{\text{def}}{=}\{\lambda r.(f(r),{\alpha }_{f(r)}(r))\mid$$

$$({\alpha }_i\in M_{X_i}{)}_{i\in \mathsf{image}(f)}\}\text{,}$$

$$M_{Y^X}\stackrel{\text{def}}{=}\{\alpha :\mathbb{R}\to Y^X\mid \mathsf{uncurry}(\alpha )\in \mathbf{QBS}(\mathbb{R}\times X,Y)\}\text{.}$$

$$(\scalebox{0.5}[1.0]{$>\!>=$})\colon\mathcal{C}(X,T(Y))\to\mathcal{C}(T(X),T(Y))\text{.}$$

$$P(X)$$

$$M_{P(X)}$$

$$\forall r\in \mathbb{R}.\beta (r)=[\alpha ,g(r)]\}\text{,}$$

$$P(X)\cong \{{\alpha }_{\ast }\mu \in G(X,{\Sigma }_{M_X})|\alpha \in M_X,\mu \in G(\mathbb{R})\}$$

$${\eta }_{(X,M_X)}(x)=[\lambda r.x,\mu ]$$

$${\displaystyle\mathit{prior}\stackrel{{\scriptstyle\textup{def}}}{{=}}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@frame\lst@@@set@numbers({\@listingGroup{ltx_lst_keywords3}{\color[rgb]{0.60,0.0,0.0}let}}{\@listingGroup{ltx_lst_space}{ }}[}}}}$$

$$[[prior]]=[\alpha ,\nu \otimes \nu ]\in P({\mathbb{R}}^{\mathbb{R}})\text{.}$$

$$obs\stackrel{\text{def}}{=}$$

$${\displaystyle\dots\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@frame\lst@@@set@numbers({\@listingGroup{ltx_lst_keywords8}{\color[rgb]{0,0.3,0.7}observe}}{\@listingGroup{ltx_lst_space}{ }}({\@listingGroup{ltx_lst_keywords7}{\color[rgb]{0.0,0.6,0.5}normal}}{\@listingGroup{ltx_lst_space}{ }}({\@listingGroup{ltx_lst_identifier}{f}}{\@listingGroup{ltx_lst_space}{ }}5.0){\@listingGroup{ltx_lst_space}{ }}0.5){\@listingGroup{ltx_lst_space}{ }}8.0)}}}}$$

$${\mathit{obs}_{1}\stackrel{{\scriptstyle\textup{def}}}{{=}}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@frame\lst@@@set@numbers({\@listingGroup{ltx_lst_keywords8}{\color[rgb]{0,0.3,0.7}observe}}{\@listingGroup{ltx_lst_space}{ }}({\@listingGroup{ltx_lst_keywords7}{\color[rgb]{0.0,0.6,0.5}normal}}{\@listingGroup{ltx_lst_space}{ }}({\@listingGroup{ltx_lst_identifier}{f}}{\@listingGroup{ltx_lst_space}{ }}1.0){\@listingGroup{ltx_lst_space}{ }}0.5){\@listingGroup{ltx_lst_space}{ }}2.5)}}}}$$

$$[[f:{\mathbb{R}}^{\mathbb{R}}⊢{obs}_1]]=d(f(1.0),2.5)\text{,}$$

$$d(\mu ,x)=\sqrt{\frac{2}{\pi }}{e}^{-2(x-\mu {)}^2}\text{.}$$

$$[[f:{\mathbb{R}}^{\mathbb{R}}⊢obs]]=d(f(1),2.5)$$

$$\cdot d(f(4),6.2)\cdot d(f(5),8.0)\text{.}$$

$$P({\mathrm{id}}_{},[[obs]])([[prior]])\in P({\mathbb{R}}^{\mathbb{R}}\times [0,\infty ))$$

$$norm:P(X\times [0,\infty ))\to P(X)\uplus \{\mathsf{error}\}$$

$$norm([(\alpha ,\beta ),\nu ])\stackrel{\text{def}}{=}\{\begin{array}{ll}[\alpha ,{\nu }_{\beta }/({\nu }_{\beta }(\mathbb{R}))]& \text{if }0\ne {\nu }_{\beta }(\mathbb{R})\ne \infty \\ \mathsf{error}& \text{otherwise}\end{array}$$

$$M_{P(X)}$$

$$q([\mathsf{curry}{f}_{k^{♯}},\upsilon ])(x)$$

$$=[\lambda r.f_{k^{♯}}(r,x),\upsilon ]=k(x)\text{,}$$

$${\mathrm{iid}}_n([\beta ,\nu ])=\left[\left({\prod }_{i=1}^n\beta \circ {\iota }_n\right),\left({\left({\iota }_n^{\text{-1}}\right)}_{\ast }{⨂}_{i=1}^n\nu \right)\right]$$

$$\begin{gathered} {\int }_{r\in \mathbb{R}}\left(\prod _{i=1}^n[\alpha (r{)}_i\in U_i]\right)\mathrm{d}\mu \\ ={\int }_{r\in \mathbb{R}}\prod _{i=1}^n\left({\int }_{s\in \mathbb{R}}\left[\gamma (s)\in U_i\right]\mathrm{d}(k(r))\right)\mathrm{d}\xi \text{.} \end{gathered}$$

Full text

Here we introduce quasi-Borel spaces. We show that these spaces: form a new formalization of probability theory replacing measurable spaces; form a cartesian closed category and so support higher-order functions; form a well-pointed category and so support good proof principles for equational reasoning; and support continuous probability distributions. We demonstrate the use of quasi-Borel spaces for higher-order functions and probability by: showing that a well-known construction of probability theory involving random functions gains a cleaner expression; and generalizing de Finetti’s theorem, that is a crucial theorem in probability theory, to quasi-Borel spaces.

††publicationid: pubid: 978-1-5090-3018-7/17/$31.00  ©2017 IEEE

I Introduction

To express probabilistic models in machine learning and statistics in a succinct and structured way, it pays to use higher-order programming languages, such as Church [16], Venture [24], or Anglican [37]. These languages support advanced features from both programming language theory and probability theory, while providing generic inference algorithms for answering probabilistic queries, such as marginalization and posterior computation, for all models written in the language. As a result, the programmer can succinctly express a sophisticated probabilistic model and explore its properties while avoiding the nontrivial busywork of designing a custom inference algorithm.

This exciting development comes at a foundational price. Programs in these languages may combine higher-order functions and continuous distributions, or even define a probability distribution on functions. But the standard measure-theoretic formalization of probability theory does not handle higher-order functions well, as the category of measurable spaces is not cartesian closed [1]. For instance, the Anglican implementation of Bayesian linear regression in Figure 1 goes beyond the standard measure-theoretic foundation of probability theory, as it defines a probability distribution on functions $\mathbb{R}\to\mathbb{R}$.

\lst@Key

countblanklinestrue[t]\lstKV@SetIf#1\lst@ifcountblanklines

We introduce a new formalization of probability theory that accommodates higher-order functions. The main notion replacing a measurable space is a quasi-Borel space: a set $X$ equipped with a collection of functions $M_{X}\subseteq{[\mathbb{R}\to X]}$ satisfying certain conditions (Def. 7). Intuitively, $M_{X}$ is the set of random variables of type $X$. Here $\mathbb{R}$ means that the randomness of random variables in $M_{X}$ comes from (a probability distribution on) $\mathbb{R}$, one of the best behaving measurable spaces. Thus the primitive notion shifts from measurable subset to random variable, which is traditionally a derived notion. For related ideas see §IX.

Quasi-Borel spaces have good properties and structure.

• •

The category of quasi-Borel spaces is well-pointed, since a morphism is just a structure-preserving function (§III). (This is in contrast to [34, §8]).

• •

The category of quasi-Borel spaces is cartesian closed (§IV), so that it becomes a setting to study probability distributions on higher-order functions.

• •

There is a natural notion of probability measure on quasi-Borel spaces (Def. 10). The space of all probability measures is again a quasi-Borel space, and forms the basis for a commutative monad on the category of quasi-Borel spaces (§V). Thus quasi-Borel spaces form semantics for a probabilistic programming language in the monadic style [26].

We also illustrate the use of quasi-Borel spaces.

• •

Bayesian regression (§VI). Quasi-Borel spaces are a natural setting for understanding programs such as the one in Figure 1: the prior (Lines 2--4) defines a probability distribution over functions f, i.e. a measure on $\mathbb{R}^{\mathbb{R}}$, and the posterior (illustrated in the graph), is again a probability measure on $\mathbb{R}^{\mathbb{R}}$, conditioned by the observations (Lines 5--9).

• •

Randomization (§VII). A key idea of categorical logic is that $\forall\exists$ statements should become statements about quotients of objects. The structure of quasi-Borel spaces allows us to rephrase a crucial randomization lemma in this way. Classically, it says that every probability kernel arises from a random function. In the setting of quasi-Borel spaces, it says that the space of probability kernels $P(\mathbb{R})^{X}$ is a quotient of the space of random functions, $P(\mathbb{R}^{X})$ (Theorem 26). Notice that the higher-order structure of quasi-Borel spaces allows us to succinctly state this result.

• •

De Finetti’s theorem (§VIII). Probability theorists often encounter problems when working with arbitrary probability measures on arbitrary measurable spaces. Quasi-Borel spaces allow us to better manage the source of randomness. For example, de Finetti’s theorem is a foundational result in Bayesian statistics which says that every exchangeable random sequence can be generated by randomly mixing multiple independent and identically distributed sequences. The theorem is known to hold for standard Borel spaces [8] or measurable spaces that arise from good topologies [18], but not for arbitrary measurable spaces [9]. We show that it holds for all quasi-Borel spaces (Theorem 29).

All of this is evidence that quasi-Borel spaces form a convenient category for higher-order probability theory.

II Preliminaries on probability measures and measurable spaces

Definition 1**.**

The Borel sets form the least collection $\Sigma_{\mathbb{R}}$ of subsets of $\mathbb{R}$ that satisfies the following properties:

• •

intervals $(a,b)$ are Borel sets;

• •

complements of Borel sets are Borel;

• •

countable unions of Borel sets are Borel.

The Borel sets play a crucial role in probability theory because of the tight connection between the notion of probability measure and the axiomatization of Borel sets.

Definition 2**.**

A probability measure on $\mathbb{R}$ is a function $\mu\colon\Sigma_{\mathbb{R}}\to[0,1]$ satisfying $\mu(\mathbb{R})=1$ and $\mu(\biguplus S_{i})=\sum\mu(S_{i})$ for any countable sequence of disjoint Borel sets $S_{i}$.

The natural generalization gives measurable spaces.

Definition 3**.**

A $\sigma$-algebra on a set $X$ is a nonempty family of subsets of $X$ that is closed under complements and countable unions. A measurable space is a pair $(X,\Sigma_{X})$ of a set $X$ and a $\sigma$-algebra $\Sigma_{X}$ on it. A probability measure on a measurable space $X$ is a function $\mu\colon\Sigma_{X}\to[0,1]$ satisfying $\mu(X)=1$ and $\mu(\biguplus S_{i})=\sum\mu(S_{i})$ for any countable sequence of disjoint sets $S_{i}\in\Sigma_{X}$.

The Borel sets of the reals form a leading example of a $\sigma$-algebra. Other important examples are countable sets with their discrete $\sigma$-algebra, which contains all subsets. We can characterize these spaces as standard Borel spaces, but first introduce the appropriate structure-preserving maps.

Definition 4**.**

Let $(X,\Sigma_{X})$ and $(Y,\Sigma_{Y})$ be measurable spaces. A measurable function $f\colon X\to Y$ is a function such that ${f}^{\textup{-1}}(U)\in\Sigma_{X}$ when $U\in\Sigma_{Y}$.

Thus a measurable function $f\colon X\to Y$ lets us push-forward a probability measure $\mu$ on $X$ to a probability measure $f_{*}\mu$ on $Y$ by $(f_{*}\mu)(U)=\mu({f}^{\textup{-1}}(U))$. Measurable spaces and measurable functions form a category $\mathbf{Meas}$.

Real-valued measurable functions $f\colon X\to\mathbb{R}$ can be integrated with respect to a probability measure $\mu$ on $(X,\Sigma_{X})$. The integral of a nonnegative function $f$ is

[TABLE]

where $\{U_{i}\}$ ranges over finite partitions of $X$ into measurable subsets. When $f$ may be negative, its integral is

[TABLE]

when those two integrals exist. When it is convenient to make the integrated variable explicit, we write $\int_{x\in U}f(x)\,\mathrm{d}\mu$ for $\int_{X}(\lambda x.\,f(x)\cdot[x\in U])\,\mathrm{d}\mu$, where $U\in\Sigma_{X}$ is a measurable subset and $[\varphi]$ has the value $1$ if $\varphi$ holds and [math] otherwise.

II-A Standard Borel spaces

Proposition 5** (e.g. [23], App. A1).**

For a measurable space $(X,\Sigma_{X})$ the following are equivalent:

• •

$(X,\Sigma_{X})$* is a retract of $(\mathbb{R},\Sigma_{\mathbb{R}})$, that is, there exist measurable $X\xrightarrow{f}\mathbb{R}\xrightarrow{g}X$ such that $g\circ f=\mathrm{id}_{X}$;*

• •

$(X,\Sigma_{X})$* is either measurably isomorphic to $(\mathbb{R},\Sigma_{\mathbb{R}})$ or countable and discrete;*

• •

$X$* has a complete metric with a countable dense subset and $\Sigma_{X}$ is the least $\sigma$-algebra containing all open sets.*

When $(X,\Sigma_{X})$ satisfies any of the above conditions, we call it standard Borel space. These spaces play an important role in probability theory because they enjoy properties that do not hold for general measurable spaces, such as the existence of conditional probability kernels [23, 28] and de Finetti’s theorem for exchangeable random processes [9].

Besides $\mathbb{R}$, another popular uncountable standard Borel space is $(0,1)$ with the $\sigma$-algebra ${\{U\cap(0,1)~{}|~{}U\in\Sigma_{\mathbb{R}}\}}$. As the above proposition indicates, these spaces are isomorphic by, for instance, $\lambda r.\,\frac{1}{(1+e^{-r})}:\mathbb{R}\to(0,1)$.

II-B Failure of cartesian closure

Proposition 6** (Aumann, [1]).**

The category $\mathbf{Meas}$ is not cartesian closed: there is no space of functions $\mathbb{R}\to\mathbb{R}$.

Specifically, the evaluation function

[TABLE]

is never measurable $(\mathbf{Meas}(\mathbb{R},\mathbb{R})\times\mathbb{R},\Sigma\otimes\Sigma_{\mathbb{R}})\to(\mathbb{R},\Sigma_{\mathbb{R}})$ regardless of the choice of $\sigma$-algebra $\Sigma$ on $\mathbf{Meas}(\mathbb{R},\mathbb{R})$. Here, $\Sigma\otimes\Sigma_{\mathbb{R}}$ is the product $\sigma$-algebra, generated by rectangles ${(U\times V)}$ for $U\in\Sigma$ and $V\in\Sigma_{\mathbb{R}}$.

III Quasi-Borel spaces

The typical situation in probability theory is that there is a fixed measurable space $(\Omega,\Sigma_{\Omega})$, called the sample space, from which all randomness originates, and that observations are made in terms of random variables, which are pairs $(X,f)$ of a measurable space of observations $(X,\Sigma_{X})$ and a measurable function $f\colon\Omega\to X$. From this perspective, the notion of measurable function is more important than the notion of measurable space. In some ways, the $\sigma$-algebra $\Sigma_{X}$ is only used as an intermediary to restrain the class of measurable functions $\Omega\to X$.

We now use this idea as a basis for our new notion of space. In doing so, we assume that our sample space $\Omega$ is the real numbers, which makes probabilities behave well.

Definition 7**.**

A quasi-Borel space is a set $X$ together with a set $M_{X}\subseteq[\mathbb{R}\to X]$ satisfying:

• •

$\alpha\circ f\in M_{X}$* if $\alpha\in M_{X}$ and $f\colon\mathbb{R}\to\mathbb{R}$ is measurable;*

• •

$\alpha\in M_{X}$* if $\alpha\colon\mathbb{R}\to X$ is constant;*

• •

*if ${\mathbb{R}=\biguplus_{i\in\mathbb{N}}S_{i}}$, with each set $S_{i}$ Borel, and ${\alpha_{1},\alpha_{2},\ldots\in M_{X}}$, then ${\beta}$ is in ${M_{X}}$, where ${\beta(r)=\alpha_{i}(r)}$ for $r\in S_{i}$. *

The name ‘quasi-Borel space’ is motivated firstly by analogy to quasi-topological spaces (see §IX), and secondly in recognition of the intimate connection to the standard Borel space $\mathbb{R}$ (see also Prop. 15(2)).

Example 8**.**

For every measurable space $(X,\Sigma_{X})$, let $M_{\Sigma_{X}}$ be the set of measurable functions $\mathbb{R}\to X$. Thus $M_{\Sigma_{X}}$ is the set of $X$-valued random variables. In particular: $\mathbb{R}$ itself can be considered as a quasi-Borel space, with $M_{\mathbb{R}}$ the set of measurable functions $\mathbb{R}\to\mathbb{R}$; the two-element discrete space $2$ can be considered as a quasi-Borel space, with $M_{2}$ the set of measurable functions $\mathbb{R}\to 2$, which are exactly the characteristic functions of the Borel sets (Def. 1).

Before we continue, we remark that the notion of quasi-Borel space is invariant under replacing $\mathbb{R}$ with a different uncountable standard Borel space.

Proposition 9**.**

*For any measurable space $(\Omega,\Sigma_{\Omega})$, any measurable isomorphism $\iota\colon\mathbb{R}\to\Omega$, any set $X$, and any set $N$ of functions $\Omega\to X$, the pair $(X,\{\alpha\circ\iota~{}|~{}\alpha\in N\})$ is a quasi-Borel space if and only if: *

• •

$\alpha\circ f\in N$* if $\alpha\in N$ and $f\colon\Omega\to\Omega$ is measurable;*

• •

$\alpha\in N$* if $\alpha\colon\Omega\to X$ is constant;*

• •

*if $\Omega=\biguplus_{i\in\mathbb{N}}S_{i}$, with each set $S_{i}\in\Sigma_{\Omega}$, and $\alpha_{1},\alpha_{2},\ldots\in N$, then $\beta$ is in $N$, where $\beta(r)=\alpha_{i}(r)$ if $r\in S_{i}$. *

By Prop. 5, the measurable spaces isomorphic to $\mathbb{R}$ are the uncountable standard Borel spaces. Note that the choice of isomorphism $\iota$ is not important: it does not appear in the three conditions.

Probability theory typically considers a basic probability measure on the sample space $\Omega$. Each random variable, that is each measurable function $\Omega\to X$, then induces a probability measure on $X$ by pushing forward the basic measure. Quasi-Borel spaces take this idea as an axiomatic notion of probability measure.

Definition 10**.**

A probability measure on a quasi-Borel space $(X,M_{X})$ is a pair $(\alpha,\mu)$ of $\alpha\in M_{X}$ and a probability measure $\mu$ on $\mathbb{R}$ (as in Def. 2).

III-A Morphisms and integration

Definition 11**.**

A morphism of quasi-Borel spaces $(X,M_{X})\to(Y,M_{Y})$ is a function $f\colon X\to Y$ such that $f\circ\alpha\in M_{Y}$ if $\alpha\in M_{X}$. Write \mathbf{QBS}\big{(}(X,M_{X}),(Y,M_{Y})\big{)} for the set of morphisms from $(X,M_{X})$ to $(Y,M_{Y})$.

In particular, elements of $M_{X}$ are precisely morphisms $(\mathbb{R},M_{\mathbb{R}})\to(X,M_{X})$, so M_{X}=\mathbf{QBS}\big{(}(\mathbb{R},M_{\mathbb{R}}),(X,M_{X})\big{)}.

Morphisms compose as functions, and identity functions are morphisms, so quasi-Borel spaces form a category $\mathbf{QBS}$.

Example 12**.**

There are two canonical ways to equip a set $X$ with a quasi-Borel space structure. The first structure $M_{X}^{R}$ consists of all functions $\mathbb{R}\to X$. The second structure $M_{X}^{L}$ consists of all functions $\beta\colon\mathbb{R}\to X$ for which there exist: a countable subset $I\subseteq\mathbb{N}$; a measurable $f\colon\mathbb{R}\to\mathbb{R}$; a partition $\mathbb{R}=\biguplus_{i\in I}S_{i}$ with every $S_{i}$ measurable; and a sequence $(x_{i})_{i\in I}$ in $X$, such that $\beta(r)=x_{i}$ whenever $f(r)\in S_{i}$. These are the right and left adjoints, respectively, to the forgetful functor from $\mathbf{QBS}$ to $\mathbf{Set}$.

Def. 11 is independent of $\mathbb{R}$: the sample space may be any uncountable standard Borel space.

Proposition 13**.**

Consider a measurable space $(\Omega,\Sigma_{\Omega})$ with a measurable isomorphism $\iota\colon\mathbb{R}\to\Omega$. For $i\in{1,2}$, let $X_{i}$ be a set and $N_{i}$ a set of functions $\Omega\to X_{i}$ such that

[TABLE]

are quasi-Borel spaces. A function $g\colon X_{1}\to X_{2}$ is a morphism $(X_{1},M_{1})\to(X_{2},M_{2})$ if and only if $g\circ\alpha\in N_{2}$ for $\alpha\in N_{1}$.

Morphisms between quasi-Borel spaces are analogous to measurable functions between measurable spaces. The crucial properties of measurable functions are that they work well with (probability) measures: we can push-forward these measures, and integrate over them. Morphisms of quasi-Borel spaces also support these constructions.

• •

Pushing forward: if $f\colon X\to Y$ is a morphism and $(\alpha,\mu)$ is a probability measure on $X$ then $f\circ\alpha$ is by definition in $M_{Y}$ and so $(f\circ\alpha,\mu)$ is a probability measure on $Y$.

• •

Integrating: If $f\colon X\to\mathbb{R}$ is a morphism of quasi-Borel spaces and $(\alpha,\mu)$ is a probability measure on $X$, the integral of $f$ with respect to $(\alpha,\mu)$ is

[TABLE]

So integration formally reduces to integration on $\mathbb{R}$.

III-B Relationship to measurable spaces

If we regard a subset $S\subseteq X$ as its characteristic function $\chi_{S}\colon X\to 2$, then we can regard a $\sigma$-algebra on a set $X$ as a set of characteristic functions $F_{X}\subseteq[X\to 2]$ satisfying certain conditions. Thus a measurable space (Def. 3) could equivalently be described as a pair $(X,F_{X})$ of a set $X$ and a collection $F_{X}\subseteq[X\to 2]$ of characteristic functions. Moreover, from this perspective, a measurable function $f\colon(X,F_{X})\to(Y,F_{Y})$ is simply a function $f\colon X\to Y$ such that $\chi\circ f\in F_{X}$ if $\chi\in F_{Y}$. Thus quasi-Borel spaces shift the emphasis from characteristic functions $X\to 2$ to random variables $\mathbb{R}\to X$.

III-B1 Quasi-Borel spaces as structured measurable spaces

A subset $S\subseteq X$ is in the $\sigma$-algebra $\Sigma_{X}$ of a measurable space $(X,\Sigma_{X})$ if and only if its characteristic function $X\to 2$ is measurable. With this in mind, we define a measurable subset of a quasi-Borel space $(X,M_{X})$ to be a subset $S\subseteq X$ such that the characteristic function $X\to 2$ is a morphism of quasi-Borel spaces.

Proposition 14**.**

The collection of all measurable subsets of a quasi-Borel space $(X,M_{X})$ is characterized as

[TABLE]

and forms a $\sigma$-algebra.

Thus we can understand a quasi-Borel space as a measurable space $(X,\Sigma_{X})$ equipped with a class of measurable functions $M_{X}\subseteq[\mathbb{R}\to X]$ determining the $\sigma$-algebra by $\Sigma_{X}=\Sigma_{M_{X}}$ as in (2).

Moreover, every morphism $(X,M_{X})\to(Y,M_{Y})$ is also a measurable function $(X,\Sigma_{M_{X}})\to(Y,\Sigma_{M_{Y}})$ (but the converse does not hold in general).

A probability measure $(\alpha,\mu)$ on a quasi-Borel space $(X,M_{X})$ induces a probability measure $\alpha_{*}\mu$ on the underlying measurable space. Integration as in (1) matches the standard definition for measurable spaces.

III-B2 An adjunction embedding standard Borel spaces

Under some circumstances morphisms of quasi-Borel spaces coincide with measurable functions.

Proposition 15**.**

Let $(Y,\Sigma_{Y})$ be a measurable space.

If $(X,M_{X})$ is a quasi-Borel space, a function $X\to Y$ is a measurable function $(X,\Sigma_{M_{X}})\to(Y,\Sigma_{Y})$ if and only if it is a morphism $(X,M_{X})\to(Y,M_{\Sigma_{Y}})$. 2. 2.

If $(X,\Sigma_{X})$ is a standard Borel space, a function $X\to Y$ is a morphism $(X,M_{\Sigma_{X}})\to(Y,M_{\Sigma_{Y}})$ if and only if it is a measurable function $(X,\Sigma_{X})\to(Y,\Sigma_{Y})$.

Proposition 15(1) means there is an adjunction

[TABLE]

where $L(X,M_{X})=(X,\Sigma_{M_{X}})$ and $R(X,\Sigma_{X})=(X,M_{\Sigma_{X}})$. Proposition 15(2) means that the functor $R$ is full and faithful when restricted to standard Borel spaces. Equivalently, $L(R(X,\Sigma_{X}))=(X,\Sigma_{X})$, that is $\Sigma_{X}=\Sigma_{M_{\Sigma_{X}}}$ for standard Borel spaces $(X,\Sigma_{X})$.

IV Products, coproducts and function spaces

Quasi-Borel spaces support products, coproducts, and function spaces. These basic constructions form the basis for interpreting simple type theory in quasi-Borel spaces.

Proposition 16** (Products).**

If $(X_{i},M_{X_{i}})_{i\in I}$ is a family of quasi-Borel spaces indexed by a set $I$, then $(\prod_{i}X_{i},M_{\Pi_{i}X_{i}})$ is a quasi-Borel space, where $\prod_{i}X_{i}$ is the set product, and

[TABLE]

The projections $\prod_{i}X_{i}\to X_{i}$ are morphisms, and provide the structure of a categorical product in $\mathbf{QBS}$.

Proposition 17** (Coproducts).**

If $(X_{i},M_{X_{i}})_{i\in I}$ is a family of quasi-Borel spaces indexed by a countable set $I$, then $(\coprod_{i}X_{i},M_{\amalg_{i}X_{i}})$ is a quasi-Borel space, where $\coprod_{i}X_{i}$ is the disjoint union of sets,

[TABLE]

and $I$ carries the discrete $\sigma$-algebra. This space has the universal property of a coproduct in the category $\mathbf{QBS}$.

Proof notes.

The third condition of quasi-Borel spaces is needed here. It is a crucial step in showing that for an $I$-indexed family of morphisms $(f_{i}\colon X_{i}\to Z)_{i\in I}$, the copairing $[f_{i}]_{i\in I}\colon\coprod_{i\in I}X_{i}\to Z$ is again a morphism. ∎

Proposition 18** (Function spaces).**

If $(X,M_{X})$ and $(Y,M_{Y})$ are quasi-Borel spaces, so is $(Y^{X},M_{Y^{X}})$, where ${Y^{X}\stackrel{{\scriptstyle\textup{def}}}{{=}}\mathbf{QBS}(X,Y)}$ is the set of morphisms $X\to Y$, and

[TABLE]

The evaluation function $Y^{X}\times X\to Y$ is a morphism and has the universal property of the function space. Thus $\mathbf{QBS}$ is a cartesian closed category.

Proof notes.

The only difficult part is showing that $(Y^{X},M_{Y^{X}})$ satisfies the third condition of quasi-Borel spaces. Prop. 17 is useful here. ∎

IV-A Relationship with standard Borel spaces

Recall that standard Borel spaces can be thought of as a full subcategory of the quasi-Borel spaces, that is, the functor $R\colon\mathbf{Meas}\to\mathbf{QBS}$ is full and faithful (Prop. 15(2)) when restricted to the standard Borel spaces. This full subcategory has the same countable products, coproducts and function spaces (whenever they exist). We may thus regard quasi-Borel spaces as a conservative extension of standard Borel spaces that supports simple type theory.

Proposition 19**.**

The functor $R(X,\Sigma_{X})=(X,M_{\Sigma_{X}})$:

preserves products of standard Borel spaces: $R(\prod_{i}X_{i})=\prod_{i}R(X_{i})$, where $(X_{i},\Sigma_{X_{i}})_{i\in I}$ is a countable family of standard Borel spaces; 2. 2.

preserves spaces of functions between standard Borel spaces whenever they exist: if $(Y,\Sigma_{Y})$ is countable and discrete, and $(X,\Sigma_{X})$ is standard Borel, then $R(X^{Y})=R(X)^{R(Y)}$; 3. 3.

preserves countable coproducts of standard Borel spaces: $R(\coprod_{i}X_{i})=\coprod_{i}R(X_{i})$, where $(X_{i},\Sigma_{X_{i}})_{i\in I}$ is a countable family of standard Borel spaces.

Consequently, a standard programming language semantics in standard Borel spaces can be conservatively embedded in quasi-Borel spaces, allowing higher-order functions while preserving all the type theoretic structure.

We note, however, that in light of Prop. 6, the quasi-Borel space $\mathbb{R}^{\mathbb{R}}$ does not come from a standard Borel space. Moreover, the left adjoint $L\colon\mathbf{QBS}\to\mathbf{Meas}$ does not preserve products in general. For quasi-Borel spaces $(X,M_{X})$ and $(Y,M_{Y})$, we always have $\Sigma_{M_{X}}\otimes\Sigma_{M_{Y}}\subseteq\Sigma_{M_{X\times Y}}$, but not always $\supseteq$. Indeed, $\Sigma_{M_{\mathbb{R}^{\mathbb{R}}}}\otimes\Sigma_{\mathbb{R}}\neq\Sigma_{M_{(\mathbb{R}^{\mathbb{R}}\times\mathbb{R})}}$, by Prop. 6.

V A monad of probability measures

In this section we will show that the probability measures on a quasi-Borel space form a quasi-Borel space again. This gives a commutative monad that generalizes the Giry monad for measurable spaces [15].

V-A Monads

We use the Kleisli triple formulation of monads (see e.g. [26]). Recall that a monad on a category $\mathcal{C}$ comprises

• •

for any object $X$, an object $T(X)$;

• •

for any object $X$, a morphism $\eta\colon X\to T(X)$;

• •

for any objects $X,Y$, a function

[TABLE]

We write (t\scalebox{0.5}[1.0]{>!>=}f) for (\scalebox{0.5}[1.0]{>!>=})(f)(t).

This is subject to the conditions (t\scalebox{0.5}[1.0]{>!>=}\eta)=t, ({\eta(x)}\scalebox{0.5}[1.0]{>!>=}f)=f(x), and t\mathrel{\scalebox{0.5}[1.0]{>!>=}}(\lambda x.\,(f(x)\mathrel{\scalebox{0.5}[1.0]{>!>=}}g))=(t\mathrel{\scalebox{0.5}[1.0]{>!>=}}f)\mathrel{\scalebox{0.5}[1.0]{>!>=}}g.

The intuition is that $T(X)$ is an object of computations returning $X$, that $\eta$ is the computation that returns immediately, and that t\scalebox{0.5}[1.0]{>!>=}f sequences computations, first running computation $t$ and then calling $f$ with the result.

When $\mathcal{C}$ is cartesian closed, a monad is strong if (\scalebox{0.5}[1.0]{>!>=}) internalizes to an operation (\scalebox{0.5}[1.0]{>!>=})\colon(T(Y))^{X}\to(T(Y))^{T(X)}, and then the conditions are understood as expressions in a cartesian closed category.

V-B Kernels and the Giry monad

We recall the notion of probability kernel, which is a measurable family of probability measures.

Definition 20**.**

Let $(X,\Sigma_{X})$ and $(Y,\Sigma_{Y})$ be measurable spaces. A probability kernel from $X$ to $Y$ is a function $k:X\times\Sigma_{Y}\to[0,1]$ such that $k(x,-)$ is a probability measure for all $x\in X$ (Def. 3), and $k(-,U)$ is a measurable function for all $U\in\Sigma_{Y}$ (Def. 4).

We can classify probability kernels as follows. Let $G(X)$ be the set of probability measures on $(X,\Sigma_{X})$. We can equip this set with the $\sigma$-algebra generated by ${\{\mu\in G(X)~{}|~{}\mu(U)<r\}}$, for $U\in\Sigma_{X}$ and $r\in[0,1]$, to form a measurable space $(G(X),\Sigma_{G(X)})$. A measurable function $X\to G(Y)$ amounts to a probability kernel from $X$ to $Y$.

The construction $G$ has the structure of a monad, as first discussed by Giry [15]. A computational intuition is that $G(X)$ is a space of probabilistic computations over $X$, and this provides a semantic foundation for a first-order probabilistic programming language (see e.g. [34]). The unit $\eta\colon X\to G(X)$ lets $\eta(x)$ be the Dirac measure on $x$, with $\eta(x)(U)=1$ if $x\in U$, and $\eta(x)(U)=0$ if $x\not\in U$. If $\mu\in G(X)$ and $k$ is a measurable function $X\to G(Y)$, then (\mu\scalebox{0.5}[1.0]{>!>=}_{G}k) is the measure in $G(Y)$ with (\mu\scalebox{0.5}[1.0]{>!>=}_{G}k)(U)=\int_{x\in X}k(x)(U)\,\mathrm{d}\mu.

V-C Equivalent measures on quasi-Borel spaces

Recall (Def. 10) that a probability measure $(\alpha,\mu)$ on a quasi-Borel space $(X,M_{X})$ is a pair $(\alpha,\mu)$ of a function $\alpha\in M_{X}$ and a probability measure $\mu$ on $\mathbb{R}$. Random variables are often equated when they describe the same distribution. Every probability measure $(\alpha,\mu)$ determines a push-forward measure $\alpha_{*}\mu$ on the corresponding measurable space $(X,\Sigma_{M_{X}})$, that assigns to $U\subseteq X$ the real number $\mu(\alpha^{-1}(U))$. We will identify two probability measures when they define the same push-forward measure, and write $\sim$ for this equivalence relation.

This is a reasonable notion of equality even if we put aside the notion of measurable space, because two probability measures have the same push-forward measure precisely when they have the same integration operator: $(\alpha,\mu)\sim(\alpha^{\prime},\mu^{\prime})$ if and only if $\int f\,\mathrm{d}(\alpha,\mu)=\int f\,\mathrm{d}(\alpha^{\prime},\mu^{\prime})$ for all morphisms ${f\colon(X,M_{X})\to\mathbb{R}}$. Nevertheless, other notions of equivalence could be used.

V-D A probability monad

We now explain how to build a monad of probability measures on the category of quasi-Borel spaces, modulo this notion of equivalence. This monad $P$ will inherit properties from the Giry monad. Technically, the functor $L\colon\mathbf{QBS}\to\mathbf{Meas}$ (Prop. 15) is a ‘monad opfunctor’ taking $P$ to the Giry monad $G$, which means that it extends to a functor from the Kleisli category of $P$ to the Kleisli category of $G$ [36].

On objects

For a quasi-Borel space $(X,M_{X})$, let

[TABLE]

where $[\alpha,\mu]$ denotes the equivalence class. Note that

[TABLE]

as sets, and $l_{X}([\alpha,\mu])=\alpha_{*}\mu$ defines a measurable injection $l_{X}\colon L(P(X))\rightarrowtail G(X,\Sigma_{M_{X}})$.

Monad unit (return)

Recall that the constant functions $(\lambda r.x)$ are all in $M_{X}$. For any probability measure $\mu$ on $\mathbb{R}$, the push-forward measure $(\lambda r.x)_{*}\,\mu$ on $(X,\Sigma_{M_{X}})$ is the Dirac measure on $x$, with $((\lambda r.x)_{*}\,\mu)(U)=1$ if $x\in U$ and [math] otherwise. Thus $(\lambda r.x,\mu)\sim(\lambda r.x,\mu^{\prime})$ for all measures $\mu,\mu^{\prime}$ on $\mathbb{R}$. The unit of $P$ at $(X,M_{X})$ is the morphism $\eta\colon X\to P(X)$ given by

[TABLE]

for an arbitrary probability measure $\mu$ on $\mathbb{R}$.

Bind

To define {(\scalebox{0.5}[1.0]{>!>=})\colon P(Y)^{X}\to(P(Y))^{P(X)}}, suppose $f\colon X\to P(Y)$ is a morphism and $[\alpha,\mu]$ in $P(X)$. Since $f$ is a morphism, there is a measurable $g\colon\mathbb{R}\to G(\mathbb{R})$ and a function $\beta\in M_{Y}$ such that $(f\circ\alpha)(r)=[\beta,g(r)]$. Set ([\alpha,\mu]\mathrel{\scalebox{0.5}[1.0]{>!>=}}f)=[\beta,\mu\mathrel{\scalebox{0.5}[1.0]{>!>=}_{G}}g], where \mu\mathrel{\scalebox{0.5}[1.0]{>!>=}_{G}}g is the bind of the Giry monad. This matches the bind of the Giry monad, since ((\alpha_{*}\mu)\mathrel{\scalebox{0.5}[1.0]{>!>=}_{G}}(l_{Y}\circ f))=\beta_{*}(\mu\mathrel{\scalebox{0.5}[1.0]{>!>=}_{G}}g).

Theorem 21**.**

The data (P,\eta,(\scalebox{0.5}[1.0]{>!>=})) above defines a strong monad on the category $\mathbf{QBS}$ of quasi-Borel spaces.

Proof notes.

The monad laws can be reduced to the laws for the monad $G$ on $\mathbf{Meas}$ [15]. The monad on $\mathbf{QBS}$ is strong because (\scalebox{0.5}[1.0]{>!>=})\colon P(Y)^{X}\to(P(Y))^{P(X)} is a morphism, which is shown by expanding the definitions. ∎

Proposition 22**.**

The monad $P$ satisfies these properties:

*For $f\colon(X,M_{X})\to(Y,M_{Y})$, the functorial action $P(f)\colon P(X)\to P(Y)$ is $[\alpha,\mu]\mapsto[f\circ\alpha,\mu]$. * 2. 2.

It is a commutative monad, i.e. the order of sequencing doesn’t matter: if $p\in P(X)$, $q\in P(Y)$, and $f$ is a morphism $X\times Y\to P(Z)$, then p\mathrel{\scalebox{0.5}[1.0]{>!>=}}\lambda x.\,q\mathrel{\scalebox{0.5}[1.0]{>!>=}}\lambda y.\,f(x,y) equals q\mathrel{\scalebox{0.5}[1.0]{>!>=}}\lambda y.\,p\mathrel{\scalebox{0.5}[1.0]{>!>=}}\lambda x.\,f(x,y). 3. 3.

The faithful functor ${L\colon\mathbf{QBS}\to\mathbf{Meas}}$ with ${L(X,M_{X})=(X,\Sigma_{M_{X}})}$ extends to a faithful functor ${\mathsf{Kleisli}(P)\to\mathsf{Kleisli}(G)}$, i.e. $(L,l)$ is a monad opfunctor **[36]**. 4. 4.

When $(X,\Sigma_{X})$ is a standard Borel space, the map $l_{X}$ of Eq. (3) is a measurable isomorphism.

VI Example: Bayesian regression

We are now in a position to explain the semantics of the Anglican program in Figure 1. The program can be split into three parts: a prior, a likelihood, and a posterior. Recall that Bayes’ law says that the posterior is proportionate to the product of the prior and the likelihood.

Prior

Lines 2--4 define a prior measure on $\mathbb{R}^{\mathbb{R}}$:

[TABLE]

To describe this semantically, observe the following.

Proposition 23**.**

Let $(\Omega,\Sigma_{\Omega})$ be a standard Borel space, and $(X,M_{X})$ a quasi-Borel space. Let $\alpha\colon R(\Omega,\Sigma_{\Omega})\to X$ be a morphism and $\mu$ a probability measure on $(\Omega,\Sigma_{\Omega})$. Any section-retraction pair $(\Omega\xrightarrow{\varsigma}\mathbb{R}\xrightarrow{\rho}\Omega)=\mathrm{id}_{\Omega}$ has a probability measure $[\alpha\circ\rho,\varsigma_{*}\mu]\in P(X)$, that is independent of the choice of $\varsigma$ and $\rho$.

Write $[\alpha,\mu]$ for the probability measure in this case.

Now, the program fragment $\mathit{prior}$ describes the distribution $[\alpha,\nu\otimes\nu]$ in $P(\mathbb{R}^{\mathbb{R}})$ where $\nu$ is the normal distribution on $\mathbb{R}$ with mean [math] and standard deviation $3$, and where $\alpha\colon\mathbb{R}\times\mathbb{R}\to\mathbb{R}^{\mathbb{R}}$ is given by $\alpha(s,b)\stackrel{{\scriptstyle\textup{def}}}{{=}}\lambda r.\,s\cdot r+b$. Informally,

[TABLE]

Figure 2 illustrates this measure $[\alpha,\nu\otimes\nu]$. This denotational semantics can be made compositional, by using the commutative monad structure of $P$ and the cartesian closed structure of the category $\mathbf{QBS}$ (following e.g. [26, 34]), but in this paper we focus on this example rather than spelling out the general case once again.

Likelihood

Lines 5--9 define the likelihood of the observations:

[TABLE]

This program fragment has a free variable $f$ of type $\mathbb{R}^{\mathbb{R}}$. Let us focus on line 5 for a moment:

[TABLE]

Given a function $f\colon\mathbb{R}\to\mathbb{R}$, the likelihood of drawing $2.5$ from a normal distribution with mean $f(1.0)$ and standard deviation $0.5$ is

[TABLE]

where $d\colon\mathbb{R}^{2}\to[0,\infty)$ is the density of the normal distribution function with standard deviation $0.5$:

[TABLE]

Notice that we use a normal distribution to allow for some noise in the measurement. Informally, we are not recording an observation that $f(1.0)$ is exactly $2.5$, since this would make regression impossible; rather, $f(1.0)$ is roughly $2.5$.

Overall, lines 5--9 describe a likelihood weight which is the product of the likelihoods of the five data points, given $f\colon\mathbb{R}^{\mathbb{R}}$.

[TABLE]

Posterior

We follow the recipe for a semantic posterior given in [34]. Putting the prior and likelihood together gives a probability measure in $P(\mathbb{R}^{\mathbb{R}}\times[0,\infty))$ which is found by pushing forward the measure $\llbracket\mathit{prior}\rrbracket\in P(\mathbb{R})$ along the function $(\mathrm{id}_{\,},\,\llbracket\mathit{obs}\rrbracket)\colon\mathbb{R}^{\mathbb{R}}\to\mathbb{R}^{\mathbb{R}}\times[0,\infty)$.

This push-forward measure

[TABLE]

is a measure over pairs $(f,w)$ of functions together with their likelihood weight. We now find the posterior by multiplying the prior and the likelihood, and dividing by a normalizing constant. To do this we define a morphism

[TABLE]

where $\nu_{\beta}\colon\Sigma_{\mathbb{R}}\to[0,\infty]\stackrel{{\scriptstyle\textup{def}}}{{=}}\lambda U.\,\int_{r\in U}(\beta(r))\,\mathrm{d}\nu$. The idea is that if $\beta\colon\mathbb{R}\to[0,\infty)$ and $\nu$ is a probability measure on $\mathbb{R}$ then $\nu_{\beta}$ is always a posterior measure on $\mathbb{R}$, but it is typically not normalized, i.e. $\nu_{\beta}(\mathbb{R})\neq 1$. We normalize it by dividing by the normalizing constant, as long as this division is well-defined.

Now, the semantics of the entire program in Figure 1 is $\mathit{norm}(P(\mathrm{id}_{\,},\,\llbracket\mathit{obs}\rrbracket)\,(\llbracket\mathit{prior}\rrbracket))$, which is a measure in $P(\mathbb{R}^{\mathbb{R}})$. Calculating this posterior using Anglican’s inference algorithm lmh gives the plot in the lower half of Figure 1.

Defunctionalized regression and non-linear regression

Of course, one can do regression without explicitly considering distributions over the space of all measurable functions, by instead directly calculating posterior distributions for the slope $s$ and the intercept $b$. For example, one could defunctionalize the program in Fig. 1 in the style of Reynolds [29]. But defunctionalization is a whole-program transformation. By structuring the semantics using quasi-Borel spaces, we are able to work compositionally, without mentioning $s$ and $b$ explicitly on lines 5--10. The internal posterior calculations actually happen at the level of standard Borel spaces, and so a defunctionalized version would be in some sense equivalent, but from the programming perspective it helps to abstract away from this. The regression program in Fig. 1 is quickly adapted to fit other kinds of functions, e.g. polynomials, or even programs from a small domain-specific language, simply by changing the prior in Lines 2--4.

VII Random functions

We discuss random variables and random functions, starting from the traditional setting. Let $(\Omega,\Sigma_{\Omega})$ be a measurable space with a probability measure. A random variable is a measurable function $(\Omega,\Sigma_{\Omega})\to(X,\Sigma_{X})$. A random function between measurable spaces $(X,\Sigma_{X})$ and $(Y,\Sigma_{Y})$ is a measurable function $(\Omega\times X,\Sigma_{\Omega}\otimes\Sigma_{X})\to(Y,\Sigma_{Y})$.

We can push forward a probability measure on $\Omega$ along a random variable $(\Omega,\Sigma_{\Omega})\to(X,\Sigma_{X})$ to get a probability measure on $X$, but in the traditional setting we cannot push forward a measure along a random function. Measurable spaces are not cartesian closed (Prop. 6), and so we cannot form a measurable space $Y^{X}$ and we cannot curry a random function in general.

Now, if we revisit these definitions in the setting of quasi-Borel spaces, we do have function spaces, and so we can push forward along random functions. In fact, this is somewhat tautologous because a probability measure (Def. 10) on a function space is essentially the same thing as a random function: a probability measure on a function space $(Y,\Sigma_{Y})^{(X,\Sigma_{X})}$ is defined to be a pair $(f,\mu)$ of a probability measure $\mu$ on $\mathbb{R}$, our sample space, and a morphism $f\colon\mathbb{R}\to Y^{X}$; but to give a morphism $\mathbb{R}\to Y^{X}$ is to give a morphism $\mathbb{R}\times X\to Y$ (Prop. 18) as in the traditional definition of random function.

We have already encountered an example of a random function in Section VI: the prior for linear regression is a random function from $\mathbb{R}$ to $\mathbb{R}$ over the measurable space $(\mathbb{R}\times\mathbb{R},\Sigma_{\mathbb{R}}\otimes\Sigma_{\mathbb{R}})$ with the measure $\nu\otimes\nu$. Random functions abound throughout probability theory and stochastic processes. The following section explores their use in the so-called randomization lemma, which is used throughout probability theory. By moving to quasi-Borel spaces, we can state this lemma succinctly (Theorem 26).

VII-A Randomization

An elementary but useful trick in probability theory is that every probability distribution on $\mathbb{R}$ arises as a push-forward of the uniform distribution on $[0,1]$. Even more useful is that this can be done in a parameterized way.

Proposition 24** ([23], Lem. 3.22).**

Let $(X,\Sigma_{X})$ be a measurable space. For any kernel ${k\colon X\times\Sigma_{\mathbb{R}}\to[0,1]}$ there is a measurable function ${f\colon\mathbb{R}\times X\to\mathbb{R}}$ such that ${k(x,U)=\upsilon\{r~{}|~{}f(r,x)\in U\}}$, where $\upsilon$ is the uniform distribution on $[0,1]$.

For quasi-Borel spaces we can phrase this more succinctly: it is a result about a quotient of the space of random functions. We first define quotient spaces.

Proposition 25**.**

Let $(X,M_{X})$ be a quasi-Borel space, let $Y$ be a set, and let $q\colon X\to Y$ be a surjection. Then $(Y,M_{Y})$ is a quasi-Borel space with $M_{Y}=\{q\circ\alpha~{}|~{}\alpha\in M_{X}\}$.

We call such a space a quotient space.

Theorem 26**.**

Let $(X,M_{X})$ be a quasi-Borel space. The space $(P(\mathbb{R}))^{X}$ of kernels is a quotient of the space $P(\mathbb{R}^{X})$ of random functions.

Before proving this theorem, we use Prop. 24 to give an alternative characterization of our probability monad.

Lemma 27**.**

Let $(X,M_{X})$ be a quasi-Borel space. The function $q\colon X^{\mathbb{R}}\to P(X)$ given by $q(\alpha)\stackrel{{\scriptstyle\textup{def}}}{{=}}[\alpha,\upsilon]$ is a surjection, with corresponding quotient space $(P(X),M_{P(X)})$:

[TABLE]

where $\upsilon$ is the uniform distribution on $[0,1]$.

Proof notes.

The direction $(\subseteq)$ follows immediately from Prop. 24. For the direction $(\supseteq)$ we must consider $\gamma\in M_{X^{\mathbb{R}}}$ and show that $(\lambda r\in\mathbb{R}.\,[\gamma(r),\upsilon])$ is in $M_{P(X)}$. This follows by considering the kernel $k\colon\mathbb{R}\to G(\mathbb{R}\times\mathbb{R})$ with $k(r)=\upsilon\otimes\delta_{r}$, so that $[\gamma(r),\upsilon]=[\mathsf{uncurry}(\gamma),k(r)]$. Here we are using Prop. 23. ∎

Proof of Theorem 26.

Consider the evident morphism $q\colon P(\mathbb{R}^{X})\to(P(\mathbb{R}))^{X}$ that comes from the monadic strength. That is, $(q([\alpha,\mu]))(x)=[\lambda r.\,\alpha(r)(x),\mu]$. We show that $q$ is a quotient morphism.

We first show that $q$ is surjective. To give a morphism $k\colon(X,M_{X})\to P(\mathbb{R})$ is to give a measurable function $(X,\Sigma_{M_{X}})\to G(\mathbb{R})$, since $(P(\mathbb{R}),M_{P(\mathbb{R})})\cong(G(\mathbb{R}),M_{\Sigma_{G(\mathbb{R})}})$ (Prop. 22(4))and by using the adjunction between measurable spaces and quasi-Borel spaces (Prop. 15(1)). Directly, we understand a morphism $k\colon(X,M_{X})\to P(\mathbb{R})$ as the kernel $k^{\sharp}\colon X\times\Sigma_{\mathbb{R}}\to[0,1]$ with $k^{\sharp}(x,U)\stackrel{{\scriptstyle\textup{def}}}{{=}}\mu_{x}({\alpha}^{\textup{-1}}_{x}(U))$ whenever $k(x)=[\alpha_{x},\mu_{x}]$. The definition of $k^{\sharp}$ does not depend on the choice of $\alpha_{x},\mu_{x}$.

Now we can use the randomization lemma (Prop. 24) to find a measurable function $f_{k^{\sharp}}\colon\mathbb{R}\times X\to\mathbb{R}$ such that $k^{\sharp}(x,U)=\upsilon\{r\mid f_{k^{\sharp}}(r,x)\in U\}$. In general, if a function ${Y\times X\to Z}$ is jointly measurable then it is also a morphism from the product quasi-Borel space. So $f_{k^{\sharp}}$ is a morphism, and we can form $(\mathsf{curry}{f_{k^{\sharp}}})\colon\mathbb{R}\to\mathbb{R}^{X}$. So,

[TABLE]

and $q$ is surjective, as required.

Finally we show that $M_{(P(\mathbb{R}))^{X}}=\{q\circ\alpha~{}|~{}\alpha\in M_{P(\mathbb{R}^{X})}\}$. We have $(\supseteq)$ since $q$ is a morphism, so it remains to show $(\subseteq)$. Consider $\beta\in M_{(P(\mathbb{R}))^{X}}$. We must show that $\beta=q\circ\alpha$ for some $\alpha\in M_{P(\mathbb{R}^{X})}$. By Prop. 18, $\beta\in M_{(P(\mathbb{R}))^{X}}$ means the uncurried function $(\mathsf{uncurry}\,\beta)\colon\mathbb{R}\times X\to P(\mathbb{R})$ is a morphism. As above, this morphism corresponds to a kernel $(\mathsf{uncurry}\,\beta)^{\sharp}\colon(\mathbb{R}\times X)\times\Sigma_{\mathbb{R}}\to[0,1]$. The randomization lemma (Prop. 24) gives a measurable function $f_{\beta}\colon\mathbb{R}\times(\mathbb{R}\times X)\to\mathbb{R}$ such that $(\mathsf{uncurry}\,\beta)^{\sharp}((r,x),U)=\upsilon\{s\mid f_{\beta}(s,(r,x))\in U\}$. By Prop. 15(1) and the fact that the $\sigma$-algebra of a product quasi-Borel space $\mathbb{R}\times(\mathbb{R}\times X)$ includes the product $\sigma$-algebras $\Sigma_{\mathbb{R}}\otimes\Sigma_{M_{\mathbb{R}\times X}}$, this function $f_{\beta}$ is also a morphism. Define $\gamma\colon\mathbb{R}\to(\mathbb{R}^{X})^{\mathbb{R}}$ by ${\gamma=\lambda r.\,\lambda s.\,\lambda x.\,f_{\beta}(s,(r,x))}$. This is a morphism since we can interpret $\lambda$-calculus in a cartesian closed category. Define $\alpha\colon\mathbb{R}\to P(\mathbb{R}^{X})$ by $\alpha(r)=[\gamma(r),\upsilon]$; this function is in $M_{P(\mathbb{R}^{X})}$ by Lemma 27. A direct calculation now gives $\beta=q\circ\alpha$, as required. ∎

VIII De Finetti’s theorem

De Finetti’s theorem [8] is one of the foundational results in Bayesian statistics. It says that every exchangeable sequence of random observations on $\mathbb{R}$ or another well-behaved measurable space can be modeled accurately by the following two-step process: first choose a probability measure on $\mathbb{R}$ randomly (according to some distribution on probability measures) and then generate a sequence with independent samples from this measure. Limiting observations to values in a well-behaved space like $\mathbb{R}$ in the theorem is important: Dubins and Freedman proved that the theorem fails for a general measurable space [9].

In this section, we show that a version of de Finetti’s theorem holds for all quasi-Borel spaces, not just $\mathbb{R}$. Our result does not contradict Dubins and Freedman’s obstruction; probability measures on quasi-Borel spaces may only use $\mathbb{R}$ as their source of randomness, whereas those on measurable spaces are allowed to use any measurable space for the same purpose. As we will show shortly, this careful choice of random source lets us generalize key arguments in a proof of de Finetti’s theorem [2] to quasi-Borel spaces.

Let $(X,M_{X})$ be a quasi-Borel space and $(X^{n},M_{X^{n}})$ the product quasi-Borel space $\prod_{i=1}^{n}X$ for each positive integer $n$. Recall that $P(X)$ consists of equivalence classes $[\beta,\nu]$ of probability measures $(\beta,\nu)$ on $X$. For $n\geq 1$, define a morphism $\mathrm{iid}_{n}\colon P(X)\to P(X^{n})$ by

[TABLE]

where $\iota_{n}$ is a measurable isomorphism $\mathbb{R}\to\prod_{i=1}^{n}\mathbb{R}$, and $\bigotimes_{i=1}^{n}\nu$ is the product measure formed by $n$ copies of $\nu$. The name $\mathrm{iid}_{n}$ represents ‘independent and identically distributed’. Indeed, $\mathrm{iid}_{n}$ transforms a probability measure $(\beta,\nu)$ on $X$ to the measure of the random sequence in $X^{n}$ that independently samples from $(\beta,\nu)$. The function $\mathrm{iid}_{n}$ is a morphism $P(X)\to P(X^{n})$ because it can also be written in terms of the strength of the monad $P$.

Write $(X^{\omega},M_{X^{\omega}})$ for the countable product $\prod_{i=1}^{\infty}X$.

Definition 28**.**

*A probability measure $(\alpha,\mu)$ on $X^{\omega}$ is exchangeable if for all permutations $\pi$ on positive integers,

$[\alpha,\mu]=[\alpha_{\pi},\mu]$, where $\alpha_{\pi}(r)_{i}\stackrel{{\scriptstyle\textup{def}}}{{=}}\alpha(r)_{\pi(i)}$ for all $r$ and $i$.*

Theorem 29** (Weak de Finetti for quasi-Borel spaces).**

If $(\alpha,\mu)$ is an exchangeable probability measure on $X^{\omega}$, then there exists a probability measure $(\beta,\nu)$ in $P(P(X))$ such that for all $n\geq 1$, the measure ([\beta,\nu]\mathrel{\scalebox{0.5}[1.0]{>!>=}}\mathrm{iid}_{n}) on $P(X^{n})$ equals $P((-)_{1\dots n})(\alpha,\mu)$ when considered as a measure on the product measurable space $(X^{n},\bigotimes_{i=1}^{n}\Sigma_{M_{X}})$. (Here $(-)_{1\dots n}\colon X^{\omega}\to X^{n}$ is $(x)_{1\dots n}\stackrel{{\scriptstyle\textup{def}}}{{=}}(x_{1},\dots,x_{n})$.)

In the theorem, $(\beta,\nu)$ represents a random variable that has a probability measure on $X$ as its value. The theorem says that (every finite prefix of) a sample sequence from $(\alpha,\mu)$ can be generated by first sampling a probability measure on $X$ according to $(\beta,\nu)$, then generating independent $X$-valued samples from the measure, and finally forming a sequence with these samples.

We call the theorem weak for two reasons. First, the $\sigma$-algebra $\Sigma_{M_{X^{n}}}$ includes the product $\sigma$-algebra $\bigotimes_{i=1}^{n}\Sigma_{M_{X}}$, but we do not know that they are equal; two different probability measures in $P(X^{n})$ may induce the same measure on $(X^{n},\bigotimes_{i=1}^{n}\Sigma_{M_{X}})$, although they always induce different measures on $(X^{n},\Sigma_{M_{X^{n}}})$. In the theorem, we equate such measures, which lets us use a standard technique for proving the equality of measures on product $\sigma$-algebras. Second, we are unable to construct a version of $\mathrm{iid}_{n}$ for infinite sequences, i.e. a morphism $P(X)\to P(X^{\omega})$ implementing the independent identically-distributed random sequence. The theorem is stated only for finite prefixes.

The rest of this section provides an overview of our proof of Theorem 29. The starting point is to unpack definitions in the theorem, especially those related to quasi-Borel spaces, and to rewrite the statement of the theorem purely in terms of standard measure-theoretic notions.

Lemma 30**.**

Let $(\alpha,\mu)$ be an exchangeable probability measure on $X^{\omega}$. Then, the conclusion of Theorem 29 holds if and only if there exist a probability measure $\xi\in G(\mathbb{R})$, a measurable function $k\colon\mathbb{R}\to G(\mathbb{R})$, and $\gamma\in M_{X}$ such that for all $n\geq 1$ and all $U_{1},\ldots,U_{n}\in\Sigma_{M_{X}}$,

[TABLE]

Here we express the domain of integration and the integrated variable explicitly to avoid confusion.

Proof.

Let $(\alpha,\mu)$ be an exchangeable probability measure on $X^{\omega}$. We unpack definitions in the conclusion of Theorem 29. The first definition to unpack is the notion of probability measure in $P(P(X))$. Here are the crucial facts that enable this unpacking. First, for every probability measure $(\beta,\nu)$ on $P(X)$, there exist a function $\gamma\colon\mathbb{R}\to X$ in $M_{X}$ and a measurable $k\colon\mathbb{R}\to G(\mathbb{R})$ such that $\beta(r)=[\gamma,k(r)]$ for all $r\in\mathbb{R}$. Second, conversely, for a function $\gamma\in M_{X}$, a measurable $k\colon\mathbb{R}\to G(\mathbb{R})$, and a probability measure $\nu\in G(\mathbb{R})$, the function $(\lambda r.\,[\gamma,k(r)],\nu)$ is a probability measure in $P(P(X))$. Thus, we can look for $(\gamma,k,\nu)$ in the conclusion of the theorem instead of $(\beta,\nu)$.

The second is the definition of [\beta,\nu]\mathrel{\scalebox{0.5}[1.0]{>!>=}}\mathrm{iid}_{n}. Using $(\gamma,k,\nu)$ instead of $(\beta,\nu)$, we find that [\beta,\nu]\mathrel{\scalebox{0.5}[1.0]{>!>=}}\mathrm{iid}_{n} is the measure [(\prod_{i=1}^{n}\gamma)\circ\iota_{n},\;({\iota}^{\textup{-1}}_{n})_{*}\,(\nu\mathrel{\scalebox{0.5}[1.0]{>!>=}}\lambda r.\,\bigotimes_{i=1}^{n}k(r))].

Recall that two measures $p$ and $q$ on the product space $(X^{n},\bigotimes_{i=1}^{n}X)$ are equivalent when $p(U_{1}\times\cdots\times U_{n})$ equals $q(U_{1}\times\cdots\times U_{n})$ for all $U_{1},\ldots,U_{n}\in\Sigma_{M_{X}}$. Thus we must show that $((-)_{1\dots n}\circ\alpha)_{*}\mu)(U_{1}\times\ldots\times U_{n})$ is equal to \big{(}(\prod_{i=1}^{n}\gamma)_{*}\,(\nu\mathrel{\scalebox{0.5}[1.0]{>!>=}}\lambda r.\,\bigotimes_{i=1}^{n}k(r))\big{)}(U_{1}\times\ldots\times U_{n}). This equation is equivalent to the one in the statement of the lemma with $\xi=\nu$. ∎

Thus we just need to show how to construct $\xi$, $k$ and $\gamma$ in Lemma 30 from a given exchangeable probability measure $(\alpha,\mu)$ on $X^{\omega}$. Constructing $\xi$ and $\gamma$ is easy:

[TABLE]

Note that these definitions type-check: $\xi=\mu\in G(\mathbb{R})$, and $\gamma\in M_{X}$ because $\alpha\in M_{X^{\omega}}$ and the first projection $(-)_{1}$ is a morphism $X^{\omega}\to X$.

Constructing $k$ is not that easy. We need to use the fact that $\mu$ is defined over $\mathbb{R}$, a standard Borel space. This fact itself holds because all probability measures on quasi-Borel spaces use $\mathbb{R}$ as their source of randomness. Define measurable functions $\alpha_{e},\alpha_{o}\colon(\mathbb{R},\Sigma_{\mathbb{R}})\to(X^{\omega},\Sigma_{M_{X^{\omega}}})$ by

[TABLE]

Since $\mu$ is a probability measure on $\mathbb{R}$, there exists a measurable function $k^{\prime}\colon(X^{\omega},\Sigma_{M_{X^{\omega}}})\to(G(\mathbb{R}),\Sigma_{G(\mathbb{R})})$, called a conditional probability kernel, such that for all measurable $f\colon\mathbb{R}\to\mathbb{R}$ and $U\in{(\alpha_{e})}^{\textup{-1}}(\Sigma_{M_{X^{\omega}}})$,

[TABLE]

Define $k\stackrel{{\scriptstyle\textup{def}}}{{=}}k^{\prime}\circ\alpha_{e}$.

Our $\xi$, $k$ and $\gamma$ satisfy the requirement in Lemma 30 because of the following three properties, which follow from exchangeability of $(\alpha,\mu)$.

Lemma 31**.**

For all $n\geq 1$ and all $U_{1},\ldots,U_{n}\in\Sigma_{M_{X}}$,

[TABLE]

Proof.

Consider $n\geq 1$ and $U_{1},\ldots,U_{n}\in\Sigma_{M_{X}}$. Pick a permutation $\pi$ on positive integers such that $\pi(i)=2i-1$ for all integers $1\leq i\leq n$. Then, $[\alpha,\mu]=[\alpha_{\pi},\mu]$ by the exchangeability of $(\alpha,\mu)$. Thus

[TABLE]

from which the statement follows. ∎

Lemma 32**.**

For all $U\in\Sigma_{M_{X}}$ and all $i,j\geq 1$,

[TABLE]

holds for $\mu$-almost all $r\in\mathbb{R}$.

Proof.

Consider a measurable set ${U\in\Sigma_{M_{X}}}$ and ${i,j\geq 1}$. The function ${\lambda r.\;\int_{s\in\mathbb{R}}\left[\alpha_{o}(s)_{i}\in U\right]\mathrm{d}(k(r))}:{\mathbb{R}\to\mathbb{R}}$ is a conditional expectation of the indicator function ${\lambda s.\,[\alpha_{o}(s)_{i}\in U]}$ with respect to the probability measure $\mu$ and the $\sigma$-algebra generated by the measurable function $\alpha_{e}\colon\mathbb{R}\to(X^{\omega},\Sigma_{M_{X^{\omega}}})$. By the almost-sure uniqueness of conditional expectation, it suffices to show that $\lambda r.\,\int_{s\in\mathbb{R}}\left[\alpha_{o}(s)_{j}\in U\right]\mathrm{d}(k(r))$ is also a conditional expectation of $\lambda s.\,[\alpha_{o}(s)_{i}\in U]$ with respect to $\mu$ and $\alpha_{e}$. Pick a measurable subset $V\in\Sigma_{M_{X^{\omega}}}$. Then:

[TABLE]

The first equation holds because the function $\lambda r.\,\int_{s\in\mathbb{R}}\left[\alpha_{o}(s)_{j}\in U\right]\mathrm{d}(k(r))$ is a conditional expectation of $\lambda s.\,[\alpha_{o}(s)_{j}\in U]$ with respect to $\mu$ and $\alpha_{e}$. The second equation follows from the exchangeability of $(\alpha,\mu)$. We have just shown that $\lambda r.\,\int_{s\in\mathbb{R}}\left[\alpha_{o}(s)_{j}\in U\right]\mathrm{d}(k(r))$ is a conditional expectation of $\lambda s.\,[\alpha_{o}(s)_{i}\in U]$ with respect to $\mu$ and $\alpha_{e}$. ∎

Lemma 33**.**

For all $n\geq 1$ and all $U_{1},\ldots,U_{n}\in\Sigma_{M_{X}}$,

[TABLE]

holds for $\mu$-almost all $r\in\mathbb{R}$.

Proof notes.

Use induction on $n\geq 1$. There is nothing to prove for the base case $n=1$. To handle the inductive case, assume that $n>1$. Let $U_{1},\ldots,U_{n}$ be subsets in $\Sigma_{M_{X}}$. Define a function $\alpha^{\prime}\colon\mathbb{R}\to X^{\omega}$ as follows:

[TABLE]

Then, $\alpha^{\prime}$ is in $M_{X^{\omega}}$, so that $\alpha^{\prime}$ is a measurable function $(\mathbb{R},\Sigma_{\mathbb{R}})\to(X^{\omega},\Sigma_{M_{X^{\omega}}})$. Thus there exists a measurable $k^{\prime}_{0}\colon(X^{\omega},\Sigma_{M_{X^{\omega}}})\to(G(\mathbb{R}),\Sigma_{G(\mathbb{R})})$, the conditional probability kernel, such that for all measurable functions $f\colon\mathbb{R}\to\mathbb{R}$, $\lambda r.\,\int_{\mathbb{R}}f\,\mathrm{d}((k^{\prime}_{0}\circ\alpha^{\prime})(r))$ is a conditional expectation of $f$ with respect to $\mu$ and the $\sigma$-algebra generated by $\alpha^{\prime}$. Define $k^{\prime}\colon\mathbb{R}\to G(\mathbb{R})=k^{\prime}_{0}\circ\alpha^{\prime}$. Then $k^{\prime}$ is measurable because so are $k^{\prime}_{0}$ and $\alpha^{\prime}$. More importantly, for $\mu$-almost all $r\in\mathbb{R}$,

[TABLE]

The proof of this equality appears in the full version of this paper.

Recall that $k=k_{0}\circ\alpha_{e}$ and $k^{\prime}=k^{\prime}_{0}\circ\alpha^{\prime}$ are defined in terms of conditional expectation. Thus, they inherit all the properties of conditional expectation. In particular, for $\mu$-almost all $r\in\mathbb{R}$ and all measurable $h\colon\mathbb{R}\to\mathbb{R}$,

[TABLE]

Using the assumption (8) and the properties (9), (10) and (11), we complete the proof of the inductive case as follows: for all subsets $V\in{(\alpha_{e})}^{\textup{-1}}(\Sigma_{M_{X^{\omega}}})$,

[TABLE]

The first and the second equalities hold because of (9) and (10). The third equality uses (8), and the fourth the equality in (11). The fifth follows from the induction hypothesis. Our derivation implies that both $\lambda r.\,\int_{s\in\mathbb{R}}\prod_{i=1}^{n}\left[\alpha_{o}(s)_{i}\in U_{i}\right]\mathrm{d}(k(r))$ and $\lambda r.\,\prod_{i=1}^{n}\int_{s\in\mathbb{R}}\left[\alpha_{o}(s)_{i}\in U_{i}\right]\mathrm{d}(k(r))$ are conditional expectations of the same function with respect to $\mu$ and the same $\sigma$-algebra. So, they are equal for $\mu$-almost all inputs $r$. ∎

The following calculation combines these lemmas and shows that $\xi$, $k$ and $\gamma$ satisfy the requirement in Lemma 30:

[TABLE]

This concludes our proof outline for Theorem 29.

IX Related work

IX-A Quasi-topological spaces and categories of functors

Our development of a cartesian closed category from measurable spaces mirrors the development of cartesian closed categories of topological spaces over the years.

For example, quasi-Borel spaces are reminiscent of subsequential spaces [20]: a set $X$ together with a collection of functions $Q\subseteq{[\mathbb{N}\cup\{\infty\}\to X]}$ satisfying some conditions. The functions in $Q$ are thought of as convergent sequences. Another notion of generalized topological space is C-space [38]: a set $X$ together with a collection $Q\subseteq[2^{\mathbb{N}}\to X]$ of ‘probes’ satisfying some conditions; this is a variation on Spanier’s early notion of quasi-topological space [33]. Another reminiscent notion in the context of differential geometry is a diffeological space [3]: a set $X$ together with a set $Q_{U}\subseteq[U\to X]$ of ‘plots’ for each open subset $U$ of $\mathbb{R}^{n}$ satisfying some conditions. These examples all form cartesian closed categories.

A common pattern is that these spaces can be understood as extensional (concrete) sheaves on an established category of spaces. Let $\mathbf{SMeas}$ be the category of standard Borel spaces and measurable functions. There is a functor

$J\colon\mathbf{QBS}\to[{\mathbf{SMeas}}^{\mathrm{op}},\mathbf{Set}]$

with \big{(}J(X,M_{X}))(Y,\Sigma_{Y}\big{)}\stackrel{{\scriptstyle\textup{def}}}{{=}}\mathbf{QBS}\big{(}(Y,M_{\Sigma_{Y}}),(X,M_{X})\big{)}, which is full and faithful by Prop. 15(2). We can characterize those functors that arise in this way.

Proposition 34**.**

Let $F\colon{\mathbf{SMeas}}^{\mathrm{op}}\to\mathbf{Set}$ be a functor. The following are equivalent:

• •

$F$* is naturally isomorphic to $J(X,M_{X})$, for some quasi-Borel space $(X,M_{X})$;*

• •

$F$* preserves countable products and $F$ is extensional: the functions $i_{(X,\Sigma_{X})}\colon F(X,\Sigma_{X})\to\mathbf{Set}(X,F(1))$ are injective, where $(i_{(X,\Sigma_{X})}(\xi))(x)=(F(\ulcorner x\urcorner))(\xi)$, and we consider $x\in X$ as a function $\ulcorner x\urcorner\colon 1\to X$.*

There are similar characterizations of subsequential spaces [20], quasi-topological spaces [10] and diffeological spaces [3]. Prop. 34 is an instance of a general pattern (e.g. [3, 10]); but that is not to say that the definition of quasi-Borel space (Def. 7) arises automatically. The method of extensional presheaves also arises in other models of computation such as finiteness spaces [11] and realizability models [30]. This work appears to be the first application to probability theory, although via Prop. 34 there are connections to Simpson’s probability sheaves [32].

The characterization of Prop. 34 gives a canonical categorical status to quasi-Borel spaces. It also connects with our earlier work [34], which used the cartesian closed category of countable-product-preserving functors in $[{\mathbf{SMeas}}^{\mathrm{op}},\mathbf{Set}]$. Quasi-Borel spaces have several advantages over this functor category. For one thing, they are more concrete, leading to better intuitions for their constructions. For example, measures in [34] are built abstractly from left Kan extensions, whereas for quasi-Borel spaces they have a straightforward concrete definition (Def. 10). For another thing, in contrast to the functor category in [34], quasi-Borel spaces form a well-pointed category: if two morphisms $(X,M_{X})\to(Y,M_{Y})$ are different then they disagree on some point in $X$. From the perspective of semantics of programming languages, where terms in context $\Gamma\vdash t:A$ are interpreted as morphisms $\llbracket t\rrbracket\colon\llbracket\Gamma\rrbracket\to\llbracket A\rrbracket$, well-pointedness is a crucial property. It says that if two open terms are different, $\llbracket t\rrbracket\neq\llbracket u\rrbracket:\llbracket\Gamma\rrbracket\to\llbracket A\rrbracket$, then there is a ground context $\mathcal{C}\colon 1\to\llbracket\Gamma\rrbracket$ that distinguishes them: $\llbracket\mathcal{C}[t]\rrbracket\neq\llbracket\mathcal{C}[u]\rrbracket:1\to\llbracket A\rrbracket$.

Quasi-Borel spaces add objects to make the category of measurable spaces cartesian closed. Another interesting future direction is to add morphisms to make more objects isomorphic, and so find a cartesian closed subcategory [35].

IX-B Domains and valuations

In this paper our starting point has been the standard foundation for probability theory, based on $\sigma$-algebras and probability measures. An alternative foundation for probability is based on topologies and valuations. An advantage of our starting point is that we can reference the canon of work on probability theory. Having said this, an advantage to the approach based on valuations is that it is related to domain theoretic methods, which have already been used to give semantics to programming languages.

Jones and Plotkin [21] showed that valuations form a monad which is analogous to our probability monad. However, there is considerable debate about which cartesian closed category this monad should be based on (e.g. [22, 17]). For a discussion of the concerns in the context of programming languages, see e.g. [13]. One recent proposal is to use Girard’s probabilistic coherence spaces [12]. Another is to use a topological domain theory as a cartesian closed category for analysis and probability ([5, 27, 19]).

Concerns about probabilistic powerdomains have led instead to domains of random variables (e.g. [25, 4, 31]). We cannot yet connect formally with this work, but there are many intuitive links. For example, our measures on quasi-Borel spaces (Def. 10) are reminiscent of continuous random variables on a dcpo.

An additional advantage of a domain theoretic approach is that it naturally supports recursion. We are currently investigating a notion of ‘ordered quasi-Borel space’, by enriching Prop. 34 over dcpo’s.

IX-C Other related work

Our work is related to two recent semantic studies on probabilistic programming languages. The first is Borgström et al.’s operational (not denotational as in this paper) semantics for a higher-order probabilistic programming language with continuous distributions [6], which has been used to justify a basic inference algorithm for the language. Recently, Culpepper and Cobb refined this operational approach using logical relations [7]. The second study is Freer and Roy’s results on a computable variant of de Finetti’s theorem and its implication on exchangeable random processes implemented in higher-order probabilistic programming languages [14]. One interesting future direction is to revisit the results about logical relations and computability in these studies with quasi-Borel spaces, and to see whether they can be extended to spaces other than standard Borel spaces.

X Conclusion

We have shown that quasi-Borel spaces (§III) support higher-order functions (§IV) as well as spaces of probability measures (§V). We have illustrated the power of this new formalism by giving a semantic analysis of Bayesian regression (§VI), by rephrasing the randomization lemma as a quotient-space construction (§VII), and by showing that it supports de Finetti’s theorem (§VIII).

Acknowledgment

We thank Radha Jagadeesan and Dexter Kozen for encouraging us to think about a well-pointed cartesian closed category for probability theory, Vincent Danos and Dan Roy for nudging us to work on de Finetti’s theorem, Mike Mislove for discussions of quasi-Borel spaces, and Martin Escardó for explaining C-spaces, and Alex Simpson for detailed report with many suggestions. This research was supported by a Royal Society Research Fellowship and EPSRC grants EP/L002388/2 and EP/N007387/1, and also by Institute for Information & communications Technology Promotion (IITP) grant funded by the Korea government (MSIP) (No.R0190-16-2011, Development of Vulnerability Discovery Technologies for IoT Software Security).