{'fraction_non_alphanumeric': 0.04786191375054451, 'fraction_numerical': 0.008494264556410629, 'mean_word_length': 4.202738432483475, 'pattern_counts': {'":': 1, '<': 7, '<?xml version=': 0, '>': 6, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 15, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Computable de Finetti measures

We prove a computable version of de Finetti's theorem on exchangeable sequences of real random variables. As a consequence, exchangeable stochastic processes expressed in probabilistic functional programming languages can be automatically rewritten as procedures that do not modify non-local state. Along the way, we prove that a distribution on the unit interval is computable if and only if its moments are uniformly computable.


Introduction
The classical de Finetti theorem states that an exchangeable sequence of real random variables is a mixture of independent and identically distributed (i.i.d.) sequences of random variables. Moreover, there is an (almost surely unique) measure-valued random variable, called the directing random measure, conditioned on which the random sequence is i.i.d. The distribution of the directing random measure is called the de Finetti measure or the mixing measure.
This paper examines the computable probability theory of exchangeable sequences of real-valued random variables. We prove a uniformly computable version of de Finetti's theorem, which implies that computable exchangeable sequences of real random variables have computable de Finetti measures. The classical proofs do not readily effectivize; instead, we show how to directly compute the de Finetti measure (as characterized by the classical theorem) in terms of a computable representation of the distribution of the exchangeable sequence. Along the way, we prove that a distribution on [0, 1] ω is computable if and only if its moments are uniformly computable, which may be of independent interest.
A key step in the proof is to describe the de Finetti measure in terms of the moments of a set of random variables derived from the exchangeable sequence.
When the directing random measure is (almost surely) continuous, we can show that these moments are computable, which suffices to complete the proof of the main theorem in this case. In the general case, we give a proof inspired by a randomized algorithm which succeeds with probability one.

Computable Probability Theory
These results are formulated in the Turing-machine-based bit-model for computation over the reals (for a general survey, see Braverman and Cook [1]). This computational model has been explored both via the type-2 theory of effectivity (TTE) framework for computable analysis, and via effective domain-theoretic representations of measures.
Computable analysis has its origins in in the study of recursive real functions, and can be seen as a way to provide "automated numerical analysis" (for a tutorial, see Brattka, Hertling, and Weihrauch [2]). Effective domain theory has its origins in the semantics of programming languages, where it continues to have many applications (for a survey, see Edalat [3]). Here we use methods from these approaches to transfer a representational result from probability theory to a setting where it can directly transform statistical objects as represented on a computer.
The computable probability measures in the bit-model coincide with those distributions from which we can generate exact samples to arbitrary precision on a computer. As such, our results have direct implications for programming languages which manipulate probability measures on real numbers via exact interfaces. In many areas of statistics and computer science, especially machine learning, one is often concerned with distributions on data structures that are higher-order or are defined using recursion. Probabilistic functional programming languages provide a convenient setting for describing and manipulating such distributions.
Exchangeable sequences play a fundamental role in both statistical models and their implementation on computers. Given a sequential description of an exchangeable process, in which one uses previous samples or sufficient statistics to sample the next element in the sequence, a direct implementation in these languages would need to use non-local communication (to record new samples or update sufficient statistics). This is often implemented by modifying the program's internal state directly (i.e., using mutation), or via some indirect method such as a state monad. The classical de Finetti theorem implies that (for such sequences over the reals) there is an alternative description in which samples are conditionally independent (and so could be implemented without non-local communication), thereby allowing parallel implementations. But the classical result does not imply that there is a program which computes the sequence according to this description. Even when there is such a program, the classical theorem does not provide a method for finding it. The computable de Finetti theorem states that such a program does exist. Moreover, the proof itself provides the method for constructing the desired program. In Section 6 we describe how an implementation of the computable de Finetti theorem uniformly transforms procedures which induce exchangeable stochastic processes into equivalent procedures which do not modify non-local state.
This transformation is of interest beyond its implications for programming language semantics. In statistics and machine learning, it is often desirable to know the representation of an exchangeable stochastic process in terms of its de Finetti measure (for several examples, see Section 6.3). Many such processes in machine learning have very complicated (though computable) distributions, and it is not always feasible to find the de Finetti representation by hand. The computable de Finetti theorem provides a method for automatically obtaining such representations.

de Finetti's Theorem
We assume familiarity with the standard measure-theoretic formulation of probability theory (see, e.g., Billingsley [4] or Kallenberg [5]). Fix a basic probability space (Ω, F, P) and let B R denote the Borel sets of R. Note that we will use ω to denote the set of nonnegative integers (as in logic), rather than an element of the basic probability space Ω (as in probability theory). By a random measure we mean a random element in the space of Borel measures on R, i.e., a kernel from (Ω, F) to (R, B R ). An event A ∈ F is said to occur almost surely (a.s.) if PA = 1. We denote the indicator function of a set B by 1 B . Definition 2.1 (Exchangeable sequence). Let X = {X i } i≥1 be a sequence of real random variables. We say that X is exchangeable if, for every finite set {k 1 , . . . , k j } of distinct indices, (X k 1 , . . . , X k j ) is equal in distribution to (X 1 , . . . , X j ).
Theorem 2.2 (de Finetti [6, Chap. 1.1]). Let X = {X i } i≥1 be an exchangeable sequence of real-valued random variables. There is a random probability measure ν on R such that {X i } i≥1 is conditionally i.i.d. with respect to ν. That is, Moreover, ν is a.s. unique and given by where B ranges over B R . 3 The random measure ν is called the directing random measure. Its distribution (a measure on probability measures), which we denote by µ, is called the de Finetti measure or the mixing measure. As in Kallenberg [6, Chap. 1, Eq. 3], we may take expectations on both sides of (1) to arrive at a characterization of an exchangeable sequence as a mixture of i.i.d. sequences. A Bayesian perspective suggests the following interpretation: exchangeable sequences arise from independent observations from some latent random measure. Posterior analysis follows from placing a prior distribution on ν. For further discussion of the implications of de Finetti's theorem for the foundations of statistical inference, see Dawid [7] and Lauritzen [8].
In 1931, de Finetti [9] proved the classical result for binary exchangeable sequences, in which case the de Finetti measure is simply a mixture of Bernoulli distributions; the exchangeable sequence is equivalent to repeatedly flipping a coin whose weight is drawn from some distribution on [0, 1]. In the 1950s, Hewitt and Savage [10] and Ryll-Nardzewski [11] extended the result to arbitrary realvalued exchangeable sequences. We will refer to this more general version as the de Finetti theorem. Hewitt and Savage [10] provide a history of the early developments, and a discussion of some subsequent extensions can be found in Kingman [12], Diaconis and Freedman [13], and Aldous [14]. A recent book by Kallenberg [6] provides a comprehensive view of the area of probability theory that has grown out of de Finetti's theorem, stressing the role of invariance under symmetries.

Examples
Consider an exchangeable sequence of [0, 1]-valued random variables. In this case, the de Finetti measure is a distribution on the (Borel) measures on [0, 1]. For example, if the de Finetti measure is a Dirac measure on the uniform distribution on [0, 1] (i.e., the distribution of a random measure which is almost surely the uniform distribution), then the induced exchangeable sequence consists of independent, uniformly distributed random variables on [0, 1].
As another example, let p be a random variable, uniformly distributed on [0, 1], and let ν := δ p . Then the de Finetti measure is the uniform distribution on Dirac measures on [0, 1], and the corresponding exchangeable sequence is p, p, . . . , i.e., a constant sequence, marginally uniformly distributed.
As a further example, we consider the stochastic process {X i } i≥1 whose finite marginals are given by where S n := i≤n x i , and where Γ is the Gamma function and α, β are positive real numbers. (One can verify that these marginals satisfy Kolmogorov's extension theorem [5,Theorem 6.16], and so there is a stochastic process {X i } i≥1 with these finite marginals.) Clearly this process is exchangeable, as n and S n are invariant to order. This process can also be described by a sequential scheme known as Pólya's urn [15,Chap. 11.4]. Each X i is sampled in turn according to the conditional distribution This is often described as a urn which starts with α red balls and β black balls, where at each stage, a ball is drawn uniformly at random, and is returned to the urn along with an additional ball of the same color. By de Finetti's theorem, there exists a random coin weight θ with respect to which this process is conditionally independent and P{X i = 1 | θ} = θ for each i. In fact, Furthermore, one can show that here θ is Beta(α, β)-distributed, and so the process given by the marginals (4) is called the Beta-Bernoulli process. Here the de Finetti measure is the distribution of the Bernoulli measure with random coin weight θ.

The Computable de Finetti Theorem
In each of these examples, the de Finetti measure is a computable measure. (In Section 3, we make this and related notions precise. For an explicit computable representation of the Beta-Bernoulli process, see in Section 6.) A natural question to ask is whether computable exchangeable sequences always arise from computable de Finetti measures. In fact, computable de Finetti measures give rise to computable distributions on exchangeable sequences (see Proposition 5.1). Our main result is the converse: every computable distribution on real-valued exchangeable sequences arises from a computable de Finetti measure. Theorem 2.3 (Computable de Finetti). Let χ be the distribution of a realvalued exchangeable sequence X, and let µ be the distribution of its directing random measure ν. Then µ is uniformly computable in χ, and χ is uniformly computable in µ. In particular, χ is computable if and only if µ is computable.
The directing random measure is classically given a.s. by the explicit limiting expression (2). Without a computable handle on the rate of convergence, the limit is not directly computable, and so we cannot use this limit directly to compute the de Finetti measure. However, we are able to reconstruct the de Finetti measure using the moments of a set of derived random variables. 5

Outline of the Proof
Recall that B R denotes the Borel sets of R. Let I R denote the set of open intervals, and let I Q denote the set of open intervals with rational endpoints. Then I Q I R B R . For k ≥ 1 and β ∈ B k R = B R × · · · × B R , we write β(i) to denote the ith coordinate of β.
We will denote by A R k the algebra generated by I k R (i.e., finite unions of open rectangles in R k ), and denote by A Q k the algebra generated by I k Q . Note that be an exchangeable sequence of real random variables, with distribution χ and directing random measure ν. For every γ ∈ B R , we define a [0, 1]-valued random variable V γ := νγ. A classical result in probability theory [5,Lem. 1.17] implies that a Borel measure on R is uniquely characterized by the mass it places on the open intervals with rational endpoints. Therefore, the distribution of the stochastic process {V τ } τ ∈I Q determines the de Finetti measure µ (the distribution of ν).
We can now restate the consequence of de Finetti's theorem described in Eq. (3), in terms of the finite-dimensional marginals of the exchangeable sequence X and the mixed moments of {V β } β∈B R .
As we will show in Lemma 3.5, when χ is computable, we can enumerate all rational lower bounds on quantities of the form where σ ∈ A k Q . We can also enumerate rational upper bounds on (7), provided that X places no mass on the boundary of any σ(i). In particular, if ν is a.s. continuous (i.e., with probability one, ν({x}) = 0 for every x ∈ R), then we can use χ to compute the mixed moments of {V τ } τ ∈A Q .
In Section 4, we show how to computably recover a distribution from its moments. This suffices to recover the de Finetti measure when ν is a.s. continuous, as we show in Section 5.1. In the general case, fixed point masses in ν prevent us from computing the mixed moments. Here we use a proof inspired by a randomized algorithm which almost surely avoids the point masses and recovers the de Finetti measure. For the complete proof, see Section 5.3.

Computable Representations
Before beginning the proof of the computable de Finetti theorem, we first define computable probability measures on various spaces. These definitions follow from more general TTE notions, though we will sometimes derive simpler equivalent representations for the concrete spaces we need (such as the real numbers, Borel measures on reals, and Borel measures on Borel measures on reals). For details, see the original papers, as noted.
We assume familiarity with the standard notions of computability theory and computably enumerable (c.e.) sets (see, e.g., Rogers [16] or Soare [17]). Recall that r ∈ R is called a c.e. real when the set of all rationals less than r is a c.e. set. Similarly, r is a co-c.e. real when the set of all rationals greater than r is c.e. A real r is a computable real when it is both a c.e. and co-c.e. real.
To represent more general spaces, we work in terms of an effectively presented topology. Suppose that S is a second-countable T 0 topological space with subbasis S. For every point in x ∈ S, define the set C x is the unique point that is contained in those subbasis sets that are elements of C x and no others. Since every point in a T 0 space is determined by the subbasis in this way, it is convenient to define representations on topological spaces under the assumption that the space is T 0 . In the specific cases below, we often have much more structure, which we use to simplify the representations.
We now develop these definitions more formally.
Definition 3.1 (Computable topological space). Let S be a second-countable T 0 topological space with a countable subbasis S. Let s : ω → S be an enumeration of S. We say that S is a computable topological space (with respect to s) when the set is c.e. in terms of the s-indices for A, B ∈ S, i.e., is a c.e. subset of ω, where · , · is the standard pairing function.
Computable topological spaces, as defined here, are instances of the computable T 0 spaces defined in Grubba, Schröder, and Weihrauch [18, §3], when the subbasis is replaced by the basis it generates (and the enumeration is extended in a canonical way).
It is often possible to pick a subbasis S (and enumeration s) for which the elemental "observations" that one can computably observe are those of the form x ∈ B, where B ∈ S. Then the set C x = {B ∈ S : x ∈ B} is computably enumerable (with respect to s) when the point x is such that it is eventually noticed to be in each basic open set containing it; we will call such a point x computable. This is one motivation for the definition of computable point in a T 0 space below.
Note that in a T 1 space, two computable points are computably distinguishable, but in a T 0 space, computable points will be, in general, distinguishable only in a computably enumerable fashion. However, this is essentially the best that is possible, if the open sets are the those we can "observe". (For more details on this approach to considering datatypes as topological spaces, in which basic open sets correspond to "observations", see Battenfeld, Schröder, and Simpson [19, §2].) Note that the choice of topology and subbasis are essential; for example, we can recover both computable reals and c.e. reals as instances of "computable point" for appropriate computable topological spaces, as we describe in Section 3.1.

Definition 3.2 (Computable points)
. Let (S, S) be a computable topological space with respect to an enumeration s. We say that a point x ∈ S is computable (with respect to s) when the set is c.e. (in terms of the s-indices for B ∈ S). We call the set (10) the representation of x.
Suppose that A and B are computable objects (either points, as defined here, or computable functions or measures, as defined below). We will say that A is uniformly computable in B, or that A is uniformly computable relative to B, when there is a single program (even as B varies) that computes the representation of A using the representation of B as an oracle (and similarly for computable enumerability). These representations, in turn, can be made into explicit subsets of ω using the relevant enumerations, as in (9).

Representations of Reals
We will use both the standard topology and right order topology on the real line R. The reals under the standard topology are a computable topological space using the basis I Q with respect to the canonical enumeration. The reals under the right order topology are a computable topological space using the basis under the canonical enumeration. Note that the computable points of (R, I Q ) are precisely the computable reals, and the computable points of (R, R < ) are precisely the c.e. reals.

Continuous Real Functions
We now consider computable representations for continuous functions on the reals. Definition 3.3 (Computable real function). Let S and T each be either of I Q or R < , under their canonical enumeration s and t. Let A denote the closure of the set A. Fix k ≥ 1. We say that a continuous function f : is a c.e. set (in terms of the s -indices for A ∈ S k and t-indices for B ∈ T , where s is the canonical enumeration determined by s). We call the set (12) the This definition is computably equivalent to the canonical construction of computable functions between two represented spaces [20,Ch. 6]. Note that when S = T = I Q , this recovers the standard definition of a computable real function. When S = I Q and T = R < , this recovers the standard definition of a lower-semicomputable real function [21].

Representations of Borel Probability Measures
The following representations for probability measures on computable topological spaces are devised from more general TTE representations in Schröder [22] and Bosserhoff [23], and agree with Weihrauch [24] in the case of the unit interval. In particular, the representation for M 1 (S) below is admissible with respect to the weak topology, hence computably equivalent (see Weihrauch [20,Chap. 3]) to the canonical representation for Borel measures given in Schröder [22].
Schröder [22] has also shown the equivalence of this representation for probability measures (as a computable space under the weak topology) with probabilistic processes. A probabilistic process (see Schröder and Simpson [25]) formalizes the notion of a program which uses randomness to sample points in terms of their representations of the form (10).
Let M 1 (S) denote the set of Borel probability measures on a second-countable T 0 topological space S (i.e., the probability measures on the σ-algebra generated by S). Provided that the subbasis S is closed under finite intersection, such measures are determined by the measure they assign to elements of S. Note that Let S be a computable topological space. We will describe a subbasis for M 1 (S) which makes it a computable topological space. Let A S denote the algebra generated by the subbasis S of S (i.e., the closure of S under finite union and complementation). Then, the class of sets where σ ∈ A S and q ∈ Q, is a subbasis for the weak topology on M 1 (S). An effective enumeration of this subbasis can be constructed in a canonical fashion from the enumeration of S and the rationals, making M 1 (S) a computable topological space.
Definition 3.4 (Computable distribution). Let S be a computable topological space with respect to s, and let A S be the algebra generated by the subbasis S, under its canonical enumeration s induced by s. A Borel probability measure η ∈ M 1 (S) is computable (with respect to s) when ηB is a c.e. real, uniformly in the s -index of B ∈ A S . We call the set {(B, q) ∈ A S × Q : ηB > q} the representation of η.
In particular, this implies that the measure of a c.e. open set (i.e., the c.e. union of basic open sets) is a c.e. real (uniformly in the enumeration of the terms in the union), and that the measure of a co-c.e. closed set (i.e., the complement of a c.e. open set) is a co-c.e. real (similarly uniformly); see, e.g., [26, §3.3] for details. Note that on a discrete space, where singletons are both c.e. open and co-c.e. closed, the measure of each singleton is a computable real. But for a general space, it is too strong to require that even basic open sets have computable measure (as it is more than is needed to ensure that exact samples be computably described to arbitrary accuracy).
We will be interested in computable measures η ∈ M 1 (S) where S is either R ω , [0, 1] k , or M 1 (R), topologized as described below.

Measures on Real Vectors and Sequences under the Standard Topology
Consider R ω under the product topology, where R is endowed with its standard topology. Note that R ω is a computable topological space with respect to the canonical enumeration on the basis given by the cylinders σ × R ω for σ ∈ k≥1 I k Q . Using Definition 3.4, we can characterize the class of computable distributions on real sequences. Let x = {x i } i≥1 be a sequence of real-valued random variables (e.g., the exchangeable sequence X, or the derived random variables {V τ } τ ∈I Q under the canonical enumeration of I Q ). Thus, the joint distribution η of x is computable when η(σ×R ω ) = P x ∈ σ×R ω is a c.e. real, uniformly in σ ∈ A Q k . The following simpler representation was shown to be equivalent by Müller [27,Thm. 3.7].
is a c.e. real, uniformly in k ≥ 1 and τ ∈ I k Q . 10 Therefore knowing the measure of the sets in k I k Q k A Q k is sufficient. Note that (14) is precisely the form of the first expression in Corollary 2.5. Note also that one obtains a characterization of the computability of a finite-dimensional vector by embedding it in an initial segment of a sequence.

Measures on Real Vectors and Sequences under the Right Order Topology
Distributions on c.e. reals play an important role when representing measures on measures, because, as Definition 3.4 indicates, measures are themselves represented by collections of c.e. reals lower-bounding the measure of an element of an algebra. The set R k < is a basis for the product of the right order topology on Corollary 3.6 (Computable distribution under the right order topology).
For m, k ≥ 1, let w = (w 1 , . . . , w k ) be a random vector in R k , and let C = (c ij ) ∈ Q m×k . The joint distribution of w is computable under the right order topology when P m i=1 k j=1 {w j > c ij } is a c.e. real, uniformly in C.
Note that the joint distribution of a random vector in R ω is computable under the right order topology when all its restrictions to R k are computable under the right order topology, uniformly in k. Note also that if a distribution on R k is computable under the standard topology, then it is clearly computable under the right order topology. The above representation is used in the next section as well as in Proposition 5.1, where we must compute an integral with respect to a topology that is weaker than the standard topology.

Measures on Borel Measures
The de Finetti measure µ is the distribution of the directing random measure ν, an M 1 (R)-valued random variable. Recall the definition V β := νβ, for β ∈ B R . Then µ is computable (with respect to an enumeration s of the weak topology) when is a c.e. real, uniformly in σ ∈ A k Q and C = (c ij ) ∈ Q m×k . As an immediate consequence of (15) and Corollary 3.6, we obtain the following representation for the de Finetti measure.

Integration
The following lemma is a restatement of an integration result by Schröder [22,Prop. 3.6], which itself generalizes integration results on standard topologies of finite-dimensional Euclidean spaces by Müller [27] and the unit interval by Weihrauch [24]. Define which is a basis for the standard topology on [0, 1], and define which is a basis for the right order topology on [0, 1].

Lemma 3.8 (Integration of bounded lower-semicomputable functions).
Let k ≥ 1 and let S be either I Q or R < . Let be a computable function and let µ be a computable distribution on (R k , S k ). Then is a c.e. real, uniformly in f and µ.
The following result of Müller [27] is an immediate corollary.
be a computable function and let µ be a computable distribution on (R k , I k Q ). Then is a computable real, uniformly in g and µ.

The Computable Moment Problem
One often has access to the moments of a distribution, and wishes to recover the underlying distribution. Let x = (x i ) i∈ω be a random vector in [0, 1] ω with distribution η. Classically, the distribution of x is uniquely determined by the mixed moments of x. We show that the distribution is in fact computable from the mixed moments.
One classical way to pass from the moments of x to its distribution is via the Lévy inversion formula, which maps the characteristic function φ x : R ω → C, given by to the distribution of x. However, even in the finite-dimensional case, the inversion formula involves a limit for which we have no direct handle on the rate of convergence, and so the distribution it defines is not obviously computable. Instead, we use computable versions of Urysohn's lemma and the Weierstrass approximation theorem to compute a representation of a distribution from its moments.
To show that η is computable, it suffices to show that η(σ × [0, 1] ω ) = E 1 σ (x 1 , . . . , x k ) is a c.e. real, uniformly in σ ∈ k≥1 I k Q . We begin by showing how to build sequences of polynomials that converge pointwise from below to indicator functions of the form 1 σ for σ ∈ k≥1 A Q k .

Lemma 4.1 (Polynomial approximations).
There is a computable array p n,σ : n ∈ ω, σ ∈ k≥1 A Q k (23) of rational polynomials where, for n ∈ ω and σ ∈ A Q k , the polynomial p n,σ is in k variables and, for each x ∈ [0, 1] k , we have Proof. Fix n ∈ ω and σ ∈ A Q k . Let U n,σ denote the set of x ∈ σ for which the 1/n-ball centered at x is contained in σ. We will construct (using a procedure that is uniform in n and σ) a rational polynomial p n,σ which satisfies for all x ∈ [0, 1] k , and which satisfies for all x ∈ U n,σ and for all x ∈ [0, 1] k \ σ. Then the values {p n,σ ( x)} n≥1 all equal 1 σ ( x) on x ∈ [0, 1] k \ σ, and also equal 1 σ ( x) for x on an increasing sequence of subsets of σ whose union is σ.
Then by the effective Weierstrass approximation theorem (see Pour-El and Richards [29, p. 45]), we can find (uniformly in n and σ) a polynomial p n,σ with rational coefficients which uniformly approximates f n,σ to within 1/2n on [0, 1] k . This polynomial p n,σ has the desired properties.
Using these polynomials, we can compute the distribution from the moments. The other direction follows from computable integration results.

Theorem 4.2 (Computable moments)
. Let x = (x i ) i∈ω be a random vector in [0, 1] ω with distribution η. Then η is uniformly computable in the mixed moments of {x i } i∈ω , and vice versa. In particular, η is computable if and only if the mixed moments of {x i } i∈ω are uniformly computable.
Proof. Any monic monomial in x 1 , . . . , x k , considered as a real function, computably maps [0, 1] k into [0, 1] (under the standard topology). Furthermore, η restricts to a computable measure on {x i } i≤k . Therefore, by Corollary 3.9, the mixed moments are uniformly computable in η and the index of the monomial.
To prove that η is computable in the mixed moments, we give a proof which relativizes to representation of the mixed moments, and so we assume that the mixed moments of {x i } i∈ω are uniformly computable, without loss of generality. Let k ≥ 1 and σ ∈ I k Q . To establish the computability of η, it suffices to show that is a c.e. real, uniformly in σ. By Lemma 4.1, we are given a uniformly computable sequence of polynomials (p n,σ ) n∈ω which converge pointwise from below to the indicator 1 σ . By the dominated convergence theorem, The expectation E p n,σ (x 1 , . . . , x k ) is a Q-linear combination of moments, hence a computable real. Thus their supremum is a c.e. real.

Proof of the Computable de Finetti Theorem
In the remainder of the paper, let X be a real-valued exchangeable sequence with distribution χ, let ν denote its directing random measure, and let µ denote the de Finetti measure.
Classically, the joint distribution of X is uniquely determined by the de Finetti measure (see Equation 3). We now show that the joint distribution of X is in fact computable from the de Finetti measure.
Proposition 5.1. The distribution χ is uniformly computable in µ.
Proof. We give a proof that relativizes to µ; without loss of generality, assume that µ is computable. In order to show that χ, the distribution of X, is computable, we must show that P k i=1 {X i ∈ σ(i)} is a c.e. real, uniformly in σ ∈ I k Q . Fix σ ∈ I k Q . Note that, by Corollary 2.5, Let η be the joint distribution of (V σ(i) ) i≤k and let f : To complete the proof, we now show that is a c.e. real. Note that the computability of µ implies that η is computable under the right order topology. Furthermore, f is order-preserving, and so is a continuous (and obviously computable) function from ([0, 1] k , I k < ) to ([0, 1], I < ). Therefore, by Lemma 3.8, we have that f dη is a c.e. real.
We will first prove the main theorem under the additional hypothesis that the directing random measure is almost surely continuous. We then sketch a randomized argument which succeeds with probability one. Finally, we present the proof of the main result, which can be seen as a derandomization.

Almost Surely Continuous Directing Random Measures
For k ≥ 1 and ψ ∈ A k R , we say that ψ is an X-continuity set when X i ∈ ∂ψ(i) a.s. for 1 ≤ i ≤ k (informally, X places no mass on the boundary of ψ).
Lemma 5.2. Relative to χ, the mixed moments of {V τ } τ ∈A Q are uniformly c.e. reals and the mixed moments of {V τ } τ ∈A Q are uniformly co-c.e. reals; in particular, if σ ∈ A k Q is an X-continuity set, then the mixed moment E k i=1 V σ(i) is a computable real. 15 Proof. Without loss of generality, we may assume that χ is computable. Let k ≥ 1 and σ ∈ A k Q . By Corollary 2.5, which is a c.e. real because χ is computable. The set σ is a co-c.e. closed set in R k because we can computably enumerate all τ ∈ A k Q contained in the complement of σ. Therefore, is the measure of a co-c.e. closed set, hence a co-c.e. real. When σ is an Xcontinuity set, and so the expectation is a computable real.

Proposition 5.3 (Almost surely continuous case).
Assume that ν is continuous with probability one. Then µ is uniformly computable in χ.
Proof. We give a proof that relativizes to χ; assume without loss of generality that χ is computable. Let k ≥ 1 and consider σ ∈ A k Q . The almost sure continuity of ν implies that X i ∈ ∂σ(i) a.s., i.e., σ is an X-continuity set. Therefore, by Lemma 5.2, the moment E k i=1 V σ(i) is a computable real. The computable moment theorem (Theorem 4.2) then implies that joint distribution of the variables {V τ } τ ∈A Q is computable under the standard topology, and so µ is computable under the weaker right order topology. By Corollary 3.7, this implies that µ is computable.

"Randomized" Proof Sketch
In general, the joint distribution of {V σ } σ∈A Q is not computable under the standard topology because the directing random measure ν may, with nonzero probability, have a fixed point mass on a rational. In this case, the mixed moments of {V τ } τ ∈A Q are c.e., but not co-c.e., reals (relative to χ). In this case, the computable moment theorem (Theorem 4.2) is inapplicable. For arbitrary directing random measures, we give a proof of the computable de Finetti theorem which works regardless of the location of point masses.
Consider the following sketch of a "randomized algorithm": We independently sample a countably infinite set of real numbers A ⊆ R from a computable, absolutely continuous distribution which has support everywhere on the real line (e.g., a Gaussian or Cauchy). Let A A denote the algebra generated by open intervals with endpoints in A. Note that, with probability one (over the draw), 16 A will be dense in R and ν(A) = 0 almost surely, and so X will place no mass on the boundary of any ψ ∈ A A ; suppose we have chosen such an A. Now we can proceed analogously to the case where ν is almost surely continuous, relative to an oracle A which encodes A. We begin by proving an extension of Lemma 5.2 that shows that the mixed moments of variables in terms of the new basis are A-computable, relative to χ.
Definition 5.4. We call ψ ∈ A k R a refinement of ϕ ∈ A k R , and write ψ ϕ, when for all i ≤ k.
Lemma 5.5. Let A be sampled as above. Relative to χ, the mixed moments of {V ζ } ζ∈A A are uniformly A-c.e. reals and the mixed moments of {V ζ } ζ∈A A are uniformly A-co-c.e. reals. In particular, if ψ ∈ A k A is an X-continuity set, then the mixed moment E k i=1 V ψ(i) is an A-computable real relative to χ.
Proof. Fix ψ ∈ A k A . All computability claims are relative to χ. We may A-compute a sequence such that for each n ≥ 1, σ n σ n+1 and m σ m = ψ.
For each n, is a c.e. real, and so their supremum is an A-c.e. real. If ζ, ϕ ∈ A R satisfy ζ ϕ then V ζ ≤ V ϕ (a.s.). Multiplication is continuous, and so the dominated convergence theorem gives us which we have already noted is an A-c.e. real. The co-c.e. result follows similarly from a sequence of nested unions of rational intervals whose intersection is ψ.
The final claim is immediate as in Lemma 5.2.
The proof of the computable moment theorem (Theorem 4.2) relativizes, and so the joint distribution of {V ψ } ψ∈A A is A-computable in χ. This joint distribution also classically determines the de Finetti measure. Moreover, we can A-compute (relative to χ) the desired representation with respect to the original basis. 17 Lemma 5.6. Let A be sampled as above. The de Finetti measure µ is uniformly A-computable in χ.
Proof. We show that the joint distribution of {V τ } τ ∈A Q is A-computable under the right order topology. Let m, k ≥ 1, let C = (c ij ) ∈ Q m×k , and let τ ∈ A k Q . Note that τ is an A-c.e. open set with respect to the basis A k A , and so we can Acomputably enumerate a sequence σ 1 , σ 2 , . . . ∈ A k A such that ∪ n σ n = τ . Without loss of generality, we may assume that σ n ⊆ σ n+1 . Note that V σn(j) ≤ V τ (j) (a.s.) for all n ≥ 1 and j ≤ k. By the continuity of P, The right hand side is the supremum of a uniformly A-computable set of Acomputable reals, relative to χ, hence an A-c.e. real relative to χ.
If we consider A to be a random oracle, then the representation of µ that was computed (relative to χ) using A is also a random variable. However, while A is almost surely noncomputable, the random representation of µ is almost surely constant. Recall that the distribution of the oracle A is computable because we started with a computable distribution on A. Hence we could compute µ by composing the distribution of A with the (almost surely constant) representation of µ.
A proof along these lines could be made precise using a simulation argument to calculate the pushforward measure of the random representation of µ. The basis elements assigned positive probability (and therefore probability one) are precisely those which hold of µ. Instead, in Section 5.3, we complete the proof by explicitly computing the representation of µ in terms of our rational basis. This construction can be seen as a "derandomization" of the above algorithm.
Alternatively, the above sketch could be interpreted as a degenerate probabilistic process (see Schröder and Simpson [25]) which returns a representation of the de Finetti measure with probability one. Schröder [22] shows that representations in terms of probabilistic processes are computably reducible to representations of computable distributions.
The structure of the derandomized argument occurs in other proofs in computable analysis and probability theory. Weihrauch [24,Thm. 3.6] proves a computable integration result via an argument that could likewise be seen as a derandomization of an algorithm which densely subdivides the unit interval at random locations to find continuity sets. Bosserhoff [23,Lem. 2.15] uses a similar argument to compute a basis for a computable metric space, for which every basis element is a continuity set; this suggests an alternative approach to completing our proof. Müller [27,Thm. 3.7] uses a similar construction to find open hypercubes such that for any > 0, the probability on their boundaries is less than . 18 These arguments also resemble the classic proof of the Portmanteau theorem [5,Thm. 4.25], in which an uncountable family of sets with disjoint boundaries is defined, almost all of which are continuity sets.

"Derandomized" Construction
Fix m, k ≥ 1 and let C = (c ij ) ∈ Q m×k . Define to be the indicator function for the set For n ∈ ω, we denote by p n,C the polynomial p n,σ (as defined in Lemma 4.1), where Here, we arbitrarily chose 2 > 1 so that the sequence of polynomials {p n,C } n∈ω converges pointwise from below to 1 C on [0, 1] k . Let x = (x 1 , . . . , x k ) and y = (y 1 , . . . , y k ). We can write where p + n,C and p − n,C are polynomials with positive coefficients. Define the 2kvariable polynomial q n,C ( x, y) := p + n,C ( x) − p − n,C ( y).
We denote by q n,C (V ψ , V ζ ), and similarly with p n,C .
Proposition 5.7. Let n ∈ ω, let k, m ≥ 1, let σ ∈ A k Q , and let C ∈ Q m×k . Then Eq n,C (V σ , V σ ) is a c.e. real relative to χ, uniformly in n, σ and C.
Proof. By Lemma 5.2, relative to χ, each monomial of p + n,C (V σ ) has a c.e. real expectation, and each monomial of p − n,C (V σ ) has a co-c.e. real expectation, and so by the linearity of expectation, Eq n,C (V σ , V σ ) is a c.e. real.
We are now ready to prove the main theorem.
Proof of Theorem 2.3 (Computable de Finetti). The distribution χ is uniformly computable in µ by Proposition 5.1. We now give a proof of the other direction, showing that the joint distribution of {V σ } σ∈A Q is computable, relative to χ, under the right order topology.
Let k, m ≥ 1, let π ∈ A k Q and let C = (c ij ) ∈ Q m×k . For ζ ∈ A k R , let V ζ denote the k-tuple (V ζ(1) , . . . , V ζ(k) ) and similarly for V ζ . Take 1 C to be defined as above in (41). It suffices to show that is a c.e. real relative to χ, uniformly in π and C. We do this by a series of reductions, which results in a supremum over quantities of the form Eq n,C (V σ , V σ ) for σ ∈ A k Q . By Proposition 5.7, these quantities are c.e. reals relative to χ. Note that (42) is an open set in the right order topology on [0, 1] k and so 1 C is an order preserving function. In particular, if ζ, ϕ ∈ A R satisfy ζ ϕ, then V ζ ≤ V ϕ (a.s.), and so for all ψ ∈ A k R such that ψ π. Therefore, by the density of the reals and the dominated convergence theorem, we have that where ψ ranges over A k R . Recall that the polynomials {p n,C } n∈ω converge pointwise from below to 1 C in [0, 1] k . Therefore, by the dominated convergence theorem, Multiplication is continuous, and so the dominated convergence theorem gives us where σ and τ range over A k Q . Therefore, by the linearity of expectation, If ψ is an X-continuity set, then V ψ(i) = V ψ(i) a.s. for i ≤ k, and so Because ν has at most countably many point masses, the ψ ∈ I k R which are X-continuity sets are dense in I k Q . Therefore, Note that {(σ, τ ) : (∃ψ π) σ ψ τ } = {(σ, τ ) : σ π and σ τ }. Hence Again by dominated convergence we have Combining (47) Eq n,C (V σ , V σ ).

Exchangeability in Probabilistic Functional Programming Languages
The computable de Finetti theorem has implications for the semantics of probabilistic functional programming languages, and in particular, gives conditions under which it is possible to remove uses of mutation (i.e., code which modifies a program's internal state). Furthermore, an implementation of the computable de Finetti theorem itself performs this code transformation automatically.
For context, we provide some background on probabilistic functional programming languages. We then describe the code transformation performed by the computable de Finetti theorem, using the example of the Pólya urn and Beta-Bernoulli process discussed earlier. Finally, we discuss partial exchangeability and its role in recent machine learning applications. 21
The semantics of probabilistic programs have been studied extensively in theoretical computer science in the context of randomized algorithms, probabilistic model checking, and other areas. However, the application of probabilistic programs to universal statistical modeling has a somewhat different character from much of the other work on probabilistic programming languages.
In Bayesian analysis, the goal is to use observed data to understand hidden variables in a probabilistic model. This type of inductive reasoning, from evidence to hypothesis, can be thought of as inferring the hidden states of a program that generates the observed output. One speaks of the conditional execution of probabilistic programs, in which they are "run backwards" to sample from the conditional probability distribution given the observed data.
One important difference is the algorithms used for conditional inference. Goodman et al. [32] describe the language Church, which extends Scheme, and which implements approximate conditional execution via Markov chain Monte Carlo (which can be thought of as a random walk over computational histories). Park, Pfenning, and Thrun [31] describe the language λ • , which extends OCaml, and which implements approximate conditional execution by Monte Carlo importance sampling. Ramsey and Pfeffer [38] describe an implementation of the probability monad in Haskell, and develop "measure terms" suitable for implementing the sum-product algorithm, giving a more efficient method for calculating expectations.
These languages also stress the flexibility of representations. In statistics and especially nonparametric statistics, there is an emphasis on higher-order distributions (e.g., distributions on distributions, or distributions on trees), and so it is crucial to work in a language which can express these types. Functional languages with randomness are therefore a natural choice.
The de Finetti theorem gives two different representations for exchangeable sequences, each of which has its own advantages with respect to space and time complexity. In Section 6.3 we provide several examples of the representational changes provided by the de Finetti transformation. Some of these representational issues are also examined in Roy et al. [39]. Mansinghka [40] has also described some uses of exchangeable sequences, and situations where one can exploit conditional independence for improved parallel execution.

Code Transformations
We now describe the code transformation performed by the computable de Finetti theorem. For concreteness, we will explore this connection using Church, a probabilistic functional programming language. Church extends Scheme (a dialect of LISP) with a binary-valued flip procedure, which denotes the Bernoulli distribution. In Church, an expression denotes the distribution induced by evaluation. For example,  [32].) In Scheme, one can modify the state of a non-local variable using mutation via the set! procedure. In other functional programming languages, non-local state may be implemented via other methods. (For example, in Haskell, one could use the state monad.) If an expression modifies its environment (using mutation or otherwise), it might not denote a fixed distribution. For example, a procedure may keep a counter variable and return an increasing sequence of integers on repeated calls.
Consider the Beta-Bernoulli process and the Pólya urn scheme written in Church. (For their mathematical characterization, see Section 2.1.) While these two processes look different, they induce the same distribution on sequences. We two define two procedures, sample-beta-coin and sample-pólya-coin, such that the application of either procedure returns a procedure of no arguments whose application returns (random) binary values. Fix a, b > 0. Consider the following definitions of sample-beta-coin and sample-pólya-coin (and recall that the (λ () . . . ) special form creates a procedure of no arguments): (beta a b))) (λ () (flip weight)) ) ) (ii) (define (sample-pólya-coin) (let ((red a) (total (+ a b)) ) (λ () (let ((x (flip red total ))) (set! red (+ red x)) (set! total (+ total 1)) x ) ) ) The definitions (define my-beta-coin (sample-beta-coin)) (define my-pólya-coin (sample-pólya-coin)) define a procedure my-beta-coin such that repeated applications (my-beta-coin) induce a random binary sequence, and similarly with my-pólya-coin.
Evaluating (my-beta-coin) returns a 1 with probability weight and a 0 otherwise, where the shared weight parameter is itself drawn from a Beta(a, b) distribution on [0, 1]. Note that the sequence of values obtained by evaluating (my-beta-coin) is exchangeable but not i.i.d. (e.g., an initial sequence of ten 1's leads one to predict that the next draw is more likely to be 1 than 0). However, conditioned on the weight (a random variable within the opaque procedure my-beta-coin) the sequence is i.i.d. A second random coin constructed by (define your-beta-coin (sample-beta-coin)) will have a different weight (a.s.) and will generate a sequence that is independent of that generated by my-beta-coin. The sequence induced by repeated applications of my-beta-coin is exchangeable because applications of flip return independent samples.
The code in (ii) implements the Pólya urn scheme with a red balls and b black balls (see [15,Chap. 11.4]), and so the sequence of return values from my-pólya-coin is exchangeable. (One can see that the sequence is exchangeable by noting that its joint distribution depends only on the number of red and black balls and not on their order.) Because the sequence induced by repeated applications of my-pólya-coin is exchangeable, de Finetti's theorem implies that its distribution is equivalent to that induced by i.i.d. draws from some random measure (in particular, the directing random measure). In the case of the Pólya urn scheme, the directing random measure is a random Bernoulli whose weight parameter has a Beta(a, b) distribution. Therefore (sample-beta-coin) denotes the de Finetti measure of the sequence of repeated applications of my-beta-coin (and also of your-beta-coin, incidentally). The distributions of the sequences induced by repeated applications of my-beta-coin and my-pólya-coin are identical.
However, there is an important difference between these two implementations. While (sample-beta-coin) denotes the de Finetti measure, (sample-pólya-coin) does not, because my-pólya-coin does not denote a fixed distribution: the internal state of the procedure my-pólya-coin changes after each iteration, as the sufficient statistics are updated (using the mutation operator set!). Therefore, each element of the sequence of repeated applications of my-pólya-coin is generated from a different distribution. Even though the sequence of applications of my-pólya-coin has the same distribution as those given by repeated applications of my-beta-coin, the procedure my-pólya-coin denotes a probability kernel which depends on the state.
In contrast, my-beta-coin does not modify itself via mutation; after it is randomly initialized, the value of weight does not change during the execution of the program. Therefore, in each run of the program, my-beta-coin denotes a fixed distribution -a particular Bernoulli. The procedure my-beta-coin is precisely the directing random measure of the Beta-Bernoulli process produced by repeated applications of my-beta-coin.
An implementation of the computable de Finetti theorem (Theorem 2.3) transforms (ii) into a procedure which does not use mutation and whose application is equivalent in distribution to the evaluation of (sample-beta-coin). In fact, assuming we know that the code generates a binary sequence (and therefore that the directing random measure will be a random Bernoulli), we can transform the de Finetti measure into a procedure that does not use mutation and whose application is equivalent in distribution to the evaluation of (beta a b).
In the general case, given a program that generates an exchangeable sequence of reals, an implementation of the computable de Finetti proof can generate a mutation-free procedure generated-code such that (define (sample-directing-random-measure) (let ((shared-randomness (uniform 0 1))) (λ () (generated-code shared-randomness)) ) ) defines the de Finetti measure. In addition to their simpler semantics, mutation-free procedures are often desirable for practical reasons. For example, having sampled the directing random measure, an exchangeable sequence of random variables can be efficiently sampled in parallel without the overhead necessary to communicate sufficient statistics.

Partial Exchangeability of Arrays and Other Data Structures
The example above involved binary sequences, but the computable de Finetti theorem can be used to transform implementations of real exchangeable sequences. Consider the following exchangeable sequence whose combinatorial structure is known as the Chinese restaurant process (see Aldous [14]). Let α > 0 be a computable real and let H be a computable distribution on R. For n ≥ 1, each X n is sampled in turn according to the conditional distribution P[X n+1 | X 1 , . . . , X n ] = n n + α The sequence {X n } n≥1 is exchangeable and the directing random measure is a Dirichlet process with parameter αH. Given such a program, we can automatically recover the underlying Dirichlet process prior, samples from which produce random measures whose discrete structure was characterized by Sethuraman's "stick-breaking construction" [41]. Note that the random measure is not produced in the same manner as Sethuraman's construction and certainly is not of closed form. But the resulting mathematical objects have the same structure and distribution. Sequences of random objects other than reals can sometimes be given de Finetti-type representations. For example, the Indian buffet process, defined by Griffiths and Ghahramani [42], is the combinatorial process underlying a setvalued exchangeable sequence that can be written in a way analogous to the Pólya urn in (ii). Just as the Chinese restaurant process gives rise to the Dirichlet process, the Indian buffet process gives rise to a non-homogeneous Beta-Bernoulli process. Unlike in the Chinese restaurant process example, which was a sequence of random reals, the computable de Finetti theorem is not applicable to exchangeable sequences of random sets. The directing random measure was identified as a random Bernoulli process, whose base measure is a Beta process (see Thibaux and Jordan [43]). A non-homogenous Bernoulli process is a sequence of independent (but not necessarily identically distributed) Bernoulli random variables {Z i } i≥1 , and the Bernoulli sequence is the random set {n : Z n = 1}. For the Beta-Bernoulli process, the Bernoulli sequence is almost surely finite. A "stickbreaking construction" of the Beta-Bernoulli process given by Teh, Görür, and Ghahramani [44] is analogous to the code in (i), but gives only a ∆ 1 -index for the Bernoulli sequence, rather than its canonical index (see Soare [17,II.2]). This observation was first noted by Roy et al. [39]. The computability of sampling independent Bernoulli sequences of a Beta-Bernoulli process remains open. However, an Indian buffet process on a discrete base measure can be classically transformed into an exchangeable sequence of integer indices (representing the finite subsets of the discrete support). If we are given such a representation, the computable de Finetti theorem implies the existence of a computable de Finetti measure that gives canonical indices for the sets.
Combinatorial structures other than sequences have been given de Finettitype representational theorems. For example, an array of random variables is called separately (or jointly) exchangeable when its distribution is invariant under (simultaneous) permutations of the rows and columns and their higherdimensional analogues. Nearly fifty years after de Finetti's result, Aldous [45] and Hoover [46] showed that the entries of an infinite array satisfying either separate or joint exchangeability are conditionally i.i.d. These results have been connected with the theory of graph limits by Diaconis and Janson [47] and Austin [48] by considering the adjacency matrix of an exchangeable random graph.
As in the case of the Indian buffet process, structured probabilistic models in machine learning can often be represented in multiple ways, each of which has different advantages (e.g., efficient inference procedures, representational simplicity, compositionality, etc.). The infinite relational model of Kemp et al. [49] can be viewed as a partially exchangeable array, while the hierarchical stochastic block model built with the Mondrian process of Roy and Teh [50] is described using the Aldous-Hoover representation, making the conditional independence explicit. If the computable de Finetti theorem could be extended to partially exchangeable settings, it would provide analogous uniform transformations on a wider range of data structures.