{'fraction_non_alphanumeric': 0.06291946308724833, 'fraction_numerical': 0.00955198398681267, 'mean_word_length': 3.424654858035947, 'pattern_counts': {'":': 0, '<': 4, '<?xml version=': 0, '>': 4, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 56, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Probabilistic Stable Functions on Discrete Cones are Power Series (long version)

We study the category Cstabm of measurable cones and measurable stable functions, which is a denotational model of an higher-order language with continuous probabilities and full recursion. We look at Cstabm as a model for discrete probabilities, by showing the existence of a cartesian closed, full and faithful functor which embeds probabilistic coherence spaces (a fully abstract denotational model of an higher-order language with full recursion and discrete probabilities) into Cstabm. The proof is based on a generalization of Bernstein's theorem from real analysis allowing to see stable functions between discrete cones as generalized power series.


Introduction
Probabilistic reasoning allows us to describe the behavior of systems with inherent uncertainty, or on which we have an incomplete knowledge. To handle statistical models, one can employ probabilistic programming languages: they give us tools to build, evaluate and transform them. While for some applications it is enough to consider discrete probabilities, we sometimes want to model systems where the underlying space of events has inherent continuous aspects: for instance in hybrid control systems [1], as used e.g. in flight management. In the machine learning community [11,9], statistical models are also used to express our beliefs about the world, that we may then update using Bayesian inference-the ability to condition values of variables via observations.
As a consequence, several probabilistic continuous languages have been introduced and studied, such as Church [10], Anglican [18], as well as formal operational semantics for them [2]. Giving a fully abstract denotational semantics to a higher-order probabilistic language with full recursion, however, has proved to be harder than in the non-probabilistic case. For discrete probabilities, there have been two such fully abstract models: in [4], Danos and Harmer introduced a fully abstract denotational semantics of a probabilistic extension of idealized Algol, based on game semantics; and in [3] Ehrhard, Pagani and Tasson showed that the category Pcoh of probabilistic coherence spaces gives a fully abstract model for PCF ⊕ , a discrete probabilistic variant of Plotkin's PCF.
While there is currently no known fully abstract denotational semantics for a higher-order language with full recursion and continuous probabilities, several denotational models have been introduced. The pioneering work of Kozen [12] gave a denotational semantics to a first-order while-language endowed with a random real number generator. In [17], Staton et al give a denotational semantics to an higher-order language: they first develop a distributive category based on measurable spaces as a model of the first-order fragment of their language, and then extend it into a cartesian closed category using a standard construction based on the functor category.
Recently, Ehrhard, Pagani and Tasson introduced in [7] the category Cstab m , as a denotational model of an extension of PCF with continuous probabilities. It is presented as a refinement with measurability constraints of the category Cstab of abstract cones and so-called stable functions between cones, consisting in a generalization of absolutely monotonous functions from real analysis.
Here, we look at the category Cstab m from the point of view of discrete probabilities. It was noted in [7] that there is a natural way to see any probabilistic coherent space as an object of Cstab. In this work, we show that this connection leads to a full and faithful functor F from Pcoh ! -the Kleisli category of Pcoh-into Cstab. It is done by showing that every stable function between probabilistic coherent spaces can be seen as a power series, using the extension to an abstract setting of Bernstein's theorem for absolutely monotonous functions shown by McMillan [14]. We then show that the functor F we have built is cartesian closed, i.e. respects the cartesian closed structure of Pcoh ! . In the last part, we turn F into a functor F m : Pcoh ! → Cstab m , and we show that F m too is cartesian closed.
To sum up, the contribution of this paper is to show that there is a cartesian closed full embedding from Pcoh ! into Cstab m . Since Pcoh ! is known to be a fully abstract denotational model of PCF ⊕ , a corollary of this result is that Cstab m too is a fully abstract model of PCF ⊕ .

Discrete and Continuous Probabilistic Extension of PCF:
an Overview.
The operator ⊕ is the fair probabilistic choice operator, Y is a recursion operator, and n ranges over natural numbers. The ifz construct tests if its first argument (of type N ) is 0, reduces to its second argument if it is the case, and to its third otherwise. We endow this language with a natural operational semantics [6], that we choose to be call-by-name. However, for expressiveness we need to be able to simulate a call-by-value discipline on terms of ground type N : it is enabled by the let-construct. We can see that the kind of probabilistic behavior captured by PCF ⊕ is discrete, in the sense that it manipulates distributions on countable sets. In [3], Ehrhard and Danos introduced a model of Linear Logic designed to lead to denotational models for discrete higher-order probabilistic computation: the category Pcoh of probabilistic coherence spaces (PCSs). It was indeed shown in [6] that Pcoh ! , the Kleisli category of Pcoh is a fully abstract model of PCF ⊕ , while the Eilenberg-Moore Category of Pcoh is a fully abstract model of a probabilistic variant of Levy's call-by-push-value calculus.
We are going to illustrate here on examples the ideas behind the denotational semantics of PCF ⊕ in Pcoh ! . The basic idea is that the denotation of a program consists of a vector on R X + , where X is the countable sets of possible outcomes. For instance, the denotation of the program 0 ⊕ 1 of type N is the vector x ∈ R N + , with x 0 = 1 2 , x 1 = 1 2 , and x k = 0 for k ∈ {0, 1}. Morphisms in Pcoh ! , on the other hand, can be seen as analytic functions (i.e. power series) between real vector spaces. Let us look at the denotation of the simple PCF ⊕ program below.
M := λx N · (0 ⊕ ifz(x, 1, ifz(x, 0, Ω))) , where Ω is the usual encoding of a never terminating term using the recursion operator. The denotation of M consists of the following function R N + → R N + : We can see that f (x) k corresponds indeed to the probability of obtaining k if we pass to M a term N with x as denotation. Observe that f here is a polynomial in x; however since we have recursion in our language, there are programs that do an unbounded number of calls to their arguments: then their denotations are not polynomials anymore, but they are still analytic functions. The analytic nature of Pcoh ! morphisms plays a key role in the proof of full abstraction for PCF ⊕ .
Observe that this way of building a model for PCF ⊕ is utterly dependent on the fact that we consider discrete probabilities over a countable sets of values. In recent years, however, there has been much focus on continuous probabilities in higher-order languages. The aim is to be able to handle classical mathematical distributions on reals, as for instance normal or Gaussian distributions, that are widely used to build generic physical or statistical models, as well as transformations over these distributions.
We illustrate the basic idea here by presenting the language PCF sample , following [7], that can be seen as the continuous counterpart to the discrete language PCF ⊕ . It is a typed language, with types generated as A ::= R | A → A, and terms generated as follows: where r is any real number, and f is in a fixed countable set of measurable functions R n → R. The constant sample stands for the uniform distribution over [0,1]. Observe that admitting every measurable functions as primitive in the language allows to encode every distribution that can be obtained in a measurable way from the uniform distribution, for instance Gaussian or normal distributions. This language is actually expressive enough to simulate other probabilistic features, as for instance Bayesian conditioning, as highlighted in [7]. Moreover, we can argue it is also more general than PCF ⊕ : first it allows to encode integers (since N ⊆ R) and basic arithmetic operations over them. Secondly, since the orders operator ≥: R × R → {0, 1} ⊆ R is measurable, we can construct in PCF sample terms like this one: ifz (≥(sample,  1 2 ), M, N ), which encodes a fair choice between M and N . We see, however, that Pcoh ! cannot be a model for PCF sample : indeed it doesn't even seem possible to write a probabilistic coherence space for the real type. In [7], Ehrhard, Pagani and Tasson introduced the cartesian closed category Cstab m of measurable cones and measurable stables functions, and showed that it provides an adequate and sound denotational model for PCF sample . The denotation of the base type R is taken as the set of finite measures over reals, and the denotation of higher-order types is then built naturally using the cartesian closed structure. From there, it is natural to ask ourselves: how good Cstab m is as a model of probabilistic higherorder languages ?
The present paper is devoted to give a partial answer to this question: in the case where we restrict ourselves to a discrete fragment of PCF sample . To make more precise what we mean, let us consider a continuous language with an explicit discrete fragment which has both R and N as base types: we consider the language PCF ⊕,sample with all syntactic constructs of both PCF ⊕ and PCF sample , as well as an operator real with the typing rule: designed to enable the continuous constructs to act on the discrete fragment, by giving a way to see any distribution on N as a distribution on R. We see that we can indeed extend in a natural way the denotational semantics of PCF sample given in [7] to PCF sample,⊕ : in the same way that the denotational semantics of R is taken as the set of all finite measures on R, we take the denotational semantics of N as the set Meas(N) of all finite measures over N. We take as denotational semantics of the operator real the function: We will see later that this function is indeed a morphism in Cstab m (Meas(N), Meas(R)). What we would like to know is: what is the structure of the sub-category of Cstab m given by the discrete types of PCF sample, ⊕ , i.e the one generated inductively by N Cstabm , ⇒, × ?
The starting point of our work is the connection highlighted in [7] between PCSs and complete cones: every PCSs can be seen as a complete cone, in such a way that the denotational semantics of N in Pcoh ! becomes the set of finite measures over N. We formalize this connection by a functor F m : Pcoh ! → Cstab m . However, to be able to use Pcoh ! to obtain information about the discrete types sub-category of Cstab m , we need to know whether this connection is preserved at higher-order types: does the ⇒ construct in Cstab m make some wild functions not representable in Pcoh ! to appear, e.g. not analytic? The main technical part of this paper consists in showing that this is not the case, meaning that the functor F m is full and faithful, and cartesian closed. It tells us that the discrete types sub-category of Cstab m has actually the same structure as the subcategory of Pcoh ! generated by N Pcoh , ⇒ and ×. Since Pcoh ! is a fully abstract model of PCF ⊕ , it tells us that the discrete fragment of PCF sample,⊕ is fully abstract in Cstab m .

Cones and Stable Functions
The category of measurable cones and measurable, stable functions (Cstab m ), was introduced by Ehrhard, Pagani, Tasson in [7] in the aim to give a model for PCF sample .
They actually introduced it as a refinement of the category of complete cones and stable functions, denoted Cstab. Stable functions on cones are a generalization of well-known absolutely monotonic functions in real analysis: they are those functions f : [0, ∞) → R + which are infinitely differentiable, and such that moreover all their derivatives are non-negative. The relevance of such functions comes from a result due to Bernstein: every absolutely monotonic function coincides with a power series. Moreover, it is possible to characterize absolutely monotonic functions without explicitly asking for them to be differentiable: it is exactly those functions such that all the socalled higher-order differences, which are quantities defined only by sum and subtraction of terms of the form f (x), are non-negative. (see [19], chapter 4). The definition of pre-stable functions in [7] generalizes this characterization.
In this section, we first recall basic facts about cones and stable functions, all extracted from [7]. Then we will prove a generalization of Bernstein's theorem for pre-stable functions over a particular class of cones, which is the main technical contribution of this paper. We will do that following the work of McMillan on a generalization of Bernstein's theorem for functions ranging over abstract domains endowed with partition systems, see [14].

Cones
The use of a notion of cones in denotational semantics to deal with probabilistic behavior goes back to Kozen in [12]. We take here the same definition of cone as in [7].
Definition 1 A cone C is a R + -semimodule given together with an R + valued function · C called norm of C, and verifying: The most immediate example of cone is the non-negative real half-line, when we take as norm the identity. Another example is the positive quadrant in a 2-dimensional plan, endowed with the euclidian norm. In a way, the notion of cones is the generalization of the idea of a space where all elements are non-negative. This analogy gives us a generic way to define a pre-order, using the + of the cone structure.
Definition 2 Let be C a cone. Then we define a partial order C on C by: x C y if there exists z ∈ C, with y = x + z.
We define BC as the set of elements in C of norm smaller or equal to 1. We will sometimes call it the unit ball of C. Moreover, we will also be interested in the open unit ball B • C, defined as the set of elements of C of norm smaller than 1.
In [7], the authors restrict themselves to cones verifying a completeness criterion: it allows them to define the denotation of the recursion operator in PCF sample , thus enforcing the existence of fixpoints.
Definition 3 A cone C is said to be: • sequentially complete if any non-decreasing sequence (x n ) n∈N of elements of BC has a least upper bound sup n∈N x n ∈ BC.
• directed complete if for any directed subset D of BC, D has a least upper bound sup D ∈ BC.
• a lattice cone if any two elements x, y of C have a least upper bound x ∨ y.
Observe that a directed-complete cone is always sequentially complete.
Lemma 1 Let be C a lattice cone. Then it holds that: • Any two element x, y of C have a greatest lower bound x ∧ y.
• Decomposition Property: if z ≤ x + y, there there exists z 1 , z 2 ∈ C such that z = z 1 + z 2 , and z 1 ≤ x, and z 2 ≤ y.
Proof. Recall that, if a ≥ b, we denote by a − b the element c such that a = b + c.
• We consider z = x + y − (x ∨ y), and we show that z is indeed the greatest lower bound of x and y.
We illustrate Definition 3 by giving the complete cone used in [7] as the denotational semantics of the base type R in PCF sample .

Example 1
We take Meas(R) as the set of finite measures over R, and the norm as µ Meas(R) = µ(R). Meas(R) is a directed-complete cone. For every r ∈ R, the denotational semantics of the term r in [7] is δ r , the Dirac measure with respect to r defined by taking δ r (U ) = 1 if r ∈ U , and δ r (U ) = 0 otherwise.
In a similar way, we define Meas(X) as the directed-complete cone of finite measures over X, for any measurable space X. In [7], the authors ask for the cones they consider only to be sequentially complete. It is due to the fact they want to add measurability requirements to their cones, and as a rule, sequential completeness interacts better with measurability than directed completeness since measurable sets are closed under countable unions, but not general unions. We illustrate this point in the example below.
Example 2 Let be A a measurable space, and µ a finite measure on A. We consider the cone of measurable functions A → R + . We take f = A f dµ. Lebesgues Monotone Convergence Theorem shows that this cone is sequentially complete, but it is not directed complete.
In this work however, we are only interested in cones arising from probabilistic coherence spaces in a way we will develop in Section 4. Since those cones have an underlying discrete structure, we will be able to show that they are actually directed complete. We will need this information, since we will apply McMillan's results [14] obtained in the more general framework of abstract domains with partitions, in which he asks for directed completeness. That's because directed completness allows to also enforce the existence of infinum, as stated in the lemma below, whose proof can be found in the long version.

Lemma 2
If a cone C is: • sequentially complete, then every non-increasing sequence (x n ) n∈N has a greatest lower bound inf(x n ) n∈N .
• directed complete, then for every D ⊆ C directed for the reverse order, D has a greatest lower bound inf D.
Proof. We do the proof when C is directed complete, but it is exactly the same in the sequentially complete case. Let be D a reverse directed set. If all elements of D are zero, then inf D = 0. Otherwise, let be x > 0 ∈ D. We consider the subset It is easy to see it is a directed subset of BC, which means that, since C is directed complete, it has a supremum. So we can take z = x C · (x − sup E), and we show that it is the least upper bound of D.
It is shown in [7] that the addition and multiplication by a scalar are Scott-continuous in complete cones, in a sequential sense. In directed complete cones, it holds also in a directed sense.
Lemma 3 The addition + : C × C → C and the scalar multiplication · : R + × C → C are Scott-continuous: • for any directed subsets D and E of C, and K of R + : • for any reverse directed subsets D, E of C, and K of R + :

Pre-Stable Functions between Cones
As said before, the notion of pre-stable function is a generalization of the notion of absolutely monotonic real functions. More precisely, the idea is to define so-called higher-order differences, and to specify that they must be all non-negative. First, we want to be able to talk about those u = (u 1 , . . . , u n ), such that x + u i C ≤ 1 for a fixed x ∈ BC, and n ∈ N. To that end, we introduce a cone C n x whose unit ball is exactly such elements. It is an adaptation of the definition given in [7] for the case where n = 1, and we show in the same way that it is indeed a cone.
Definition 4 (Local Cone) Let be C a cone, n ∈ N, and x ∈ B • C. We call n-local cone at x, and we denote C n x the cone C n endowed with the following norm: We can show that whenever C is a directed-complete cone, C n x is also directed-complete. For n ∈ N, we use P + (n) (respectively P − (n)) for the set of all subsets I of {1, . . . , n} such that n − card(I) is even (respectively odd).
We are now ready to introduce higher-order differences. Since we have only explicit addition, not subtraction, we define separately the positive part ∆ n + and the negative part ∆ n − of those differences: For f : BC → D, x ∈ BC, u ∈ BC n x , and ǫ ∈ {−, +}, we define:

Definition 5
We say that f : BC → D is pre-stable if, for every n ∈ N, for every x ∈ BC, u ∈ BC n x , it holds that: Observe that the quantity ∆ n f (x | u) is actually symmetric in u, i.e. stable under permutations of the coordinates of u.
Definition 6 A function f : BC → D is called a stable function from C to D if it is pre-stable, sequentially Scott-continuous, and moreover there exists λ ∈ R + such that f (BC) ⊆ λ · BD.
Definition 7 Cstab is the category whose objects are sequentially complete cones, and morphisms from C to D are the stable functions f from C to D such that f (BC) ⊆ BD.
It was shown in [7] that it is possible to endow Cstab with a cartesian closed structure. The product cone is defined as i∈I It was also shown in [7] that these cones are indeed sequentially complete, and that the lub in C ⇒ D is computed pointwise. We will use also the cone of pre-stable functions from C to D, which is also sequentially complete.

A generalization of Bernstein's theorem for pre-stable functions
We are now going to show an analogue of Bernstein's Theorem for pre-stable functions on directedcomplete cones. The idea is to first define an analogue of derivatives for pre-stable functions, and to show that pre-stable functions can be written as the infinite sum generated by an analogue of Taylor expansion on B • C. This result is actually an application of McMillan's work [14] in the setting of abstract domains. Here, we give the main steps of the construction directly on cones, and highlight some properties of the Taylor series which are true for cones, but not in the general framework McMillan considered.

Derivatives of a pre-stable function
We are now going, following McMillan [14], to construct derivatives for pre-stable functions on directed complete cones. This construction is based on the use of a notion of partition: a partition of x ∈ BC is a multiset π = [u 1 , . . . , u n ] ∈ M f (C) such that x = 1≤i≤n y i . We write π ∼ x when the multiset π is a partition of x. We will denote by + the usual union on multiset: [y 1 , . . . , y n ] + [z 1 , . . . , z m ] = [y 1 , . . . , y n , z 1 , . . . , z m ]. We call P(x) the set of partitions of x.
Observe that when π 1 and π 2 are partition of x, π 2 ≤ π 1 means that π 1 is a more finely grained decomposition of x. If u is an n-tuple in BC, we extend the refinement order to P( u) = P(u 1 ) × . . . × P(u n ).
Lemma 4 Let be C a lattice cone. Then for every x ∈ C, P(x) is a directed set.
Proof. We are going to use the following notion: we say that two non-zero elements x and y of C are orthogonal, and we note x ⊥ y, if x ∧ y = 0. Let be π 1 , π 2 ∈ P(x). We first show that it cannot exist z ∈ π 1 which is orthogonal to all the element of π 2 . Indeed, suppose that it is the case: we take y 1 , . . . , y n such that π 2 = [y 1 , . . . , y n ]. Then by hypothesis, z ≤ x = 1≤i≤n y i . We can now use the decomposition property from Lemma 1. It means that z = 1≤i≤n z i , with z i ≤ y i . But since for all i, z ⊥ y i , it folds that z i = 0 for all i, and so z = 0, and we have a contradiction. Now, we are going to present a procedure to construct a partition π of x with π ≤ π 1 , and π ≤ π 2 . We can suppose that all elements of π 1 and π 2 are non-zero. We start form π = [], θ 1 = π 1 , θ 2 = π 2 , and w = x, v = 0. Through the procedure, we guarantee: • all the elements of Θ 1 and Θ 2 are non-zero; • π + Θ 1 ≤ π 1 , and π + Θ 2 ≤ π 2 (for the refinment order).
Then at each step of the procedure, if θ 1 is non empty, we do the following: let θ 1 = [a 1 , . . . , a n ], and θ 2 = [b 1 , . . . , b m ]. Then we know that there is a j, such that a 1 and b j are not orthogonal. We modify the variables as follows: [a 2 , . . . , a n ] otherwise.
At every step of the procedure presented above, the quantity: decreases. Indeed: • or we remove either a 1 of Θ 1 , or b j of Θ 2 , and then the statement above holds.
• or we replace a 1 by ( . Moreover, the pairs that were orthoganal before are still orthogonal: indeed for every z with z ⊥ a 1 it holds that z ⊥ a 1 − a 1 ∧ b j , and the same for b j . As a consequence, the procedure will terminates. It means that we reach a state where Θ 1 is empty, and all the invariants presented above hold. Then we see that π ∈ P(x), and π ≤ π 1 , π 2 .
We are going to illustrate the procedure above on a very basic example. We consider the cone consisting of the positive quadrant of R 2 , endowed by the order defined as: x ≤ y if x 1 ≤ y 1 , and x 2 ≤ y 2 . We take two partitions of a vector x ∈ R 2 : π 1 = [b 1 , b 2 ], and π 2 = [a 1 , a 2 ], where a 1 , a 2 , b 1 , b 2 are taken as pictured in Figure 1a. We are going to apply our procedure in order to obtain a refinment of both π 1 and π 2 . At the beginning, we have Θ 1 = π 1 , Θ 2 = π 2 , w = x, v = 0.
• The first step is represented in Figure 1a. Observe that the procedure is actually nondeterministic: we may choose any (a, b) with a ∈ π 1 , b ∈ π 2 , and a and b not orthonal. Here, we choose to start from (b 1 , a 1 ). We take v = a 1 ∧ b 1 (and we represent it by a red vector in Figure 1a): it is going to be the first element of our new partition π. Accordingly, we take π = [v]. We know update the partition Θ 1 and Figure 1a.
• The second step is represented in Figure 1b. Observe that now a ′ 1 and b ′ 1 are orthogonal, so we have to choose another pair. Here, we choose (b ′ 1 , a 2 ). As before, we add to π the glb of b ′ 1 and a 2 : Observe that now (as can be seen on Figure 1b So when we update the partition Θ 1 and Θ 2 , we take: Figure 1b.
• By doing again two steps of the procedure, we see that the final partition π is [ We cen see by looking at Figure 1b that it is indeed a refinment of both π 1 and π 2 ..
Step of the Procedure Figure 1: Illustration of the Proof of Lemma4 Observe that, as a consequence, the refinement preorder turnsalso P( u) into a directed set.
Definition 9 (from [14]) Let C be a lattice cone, D a cone, and let f : BC → D be a pre-stable function. Then for every x ∈ BC, and u = (u 1 , . . . , u n ) ∈ BC n x , we define Φ f,n x, u : P( u) → D as: It holds (see [14] for more details) that Φ f,n x, u is a non-increasing function whenever f is prestable (it is shown in Lemma 3.2 of [14] by looking at the definition of higher-order differences). Since P( u) is a directed set, Φ f,n x, u has a greatest lower bound whenever D is a directed-complete lattice cone.
Definition 10 (from [14]) Let be C a lattice cone, D a directed-complete lattice cone, and f : BC → D a pre-stable function. Let be u ∈ BC n x . Then the derivative of f in x at rank n towards the direction u is the function D n f (x | ·) : BC n x → D defined as We are now going to illustrate Definition 10 on a basic case where we take f : R + → R + , in order to highlight the link with differentiation in real analysis.

Example 3
We take C and D as the positive real half-line, and x ∈ [0, 1[. Let be h such that x + h ≤ 1. Then: We know already, since f is pre-stable hence absolutely monotone as function on reals, that f is convex, and moreover differentiable (see [19]). From there, by considering a particular family of partitions, we can show that Proof. First, let π be any partition of y. Since f is differentiable and convex, it holds that: As a consequence, we see that for any partition π of h, it holds that To show the reverse inequality, it is enough to consider the particular family of partition π n = [ h n , . . . , h n ] of h: we see that Proof. The proof is given in Lemma 3.31 in [14]. It comes almost directly from Definition 10.
We have seen in Example 3 that our so-called derivatives of pre-stable functions play the same role as the differential of a differentiable function, which are actually linear operators df n x : R n → R. While the abstract domains considered in [14] do not have to be R + semi-modules, so have no notion of linearity, we are able to show in the complete cone case that the D n f are linear in the sense of Lemma 6 below.
in the sense that, for each of its arguments, it commutes with the sum and multiplication by a scalar.
• For any u ∈ B(C n x ), the function f ∈ Cstab(C, D) → D n f (x | u) ∈ D is linear and directed Scott-continuous.
Proof. We are going to use the following auxiliary lemma: Lemma 7 (from [14]) Let C and D be two directed cones, and f : C → D linear and nondecreasing, such that moreover for all subset F of C directed for the reverse order, Since E is directed, F is directed for the reverse order, and as a consequence:inf f (F ) = f (inf F ). But we see that inf F = 0. Therefore, since f is linear, f (inf F ) = 0. As a consequence (and again by linearity of We are now going to show Lemma 6. The additivity is given by Lemma 3.72 of [14]. The commutation with scalar multiplication is not proved on this form in [14] because they have a more general notion of a system of partition. We first show that the result holds when λ is a rational number. To do that, we use the fact that π = [ x n , . . . , x n ] is always a partition of x. Then, let λ ∈ R + and u = (u 1 , . . . , u n ) such that both u and v = (u 1 , . . . , λu i , . . . , u n ) are in BC n x . Let be r = (r m ) m∈N , q = (q m ) m∈N two sequences of rational number such that r tends to λ by below, and q tends to λ by above. We see that: We take N such that for every m ≥ N , q m ≤ 2 · λ: since D n f (x | ·) is non-decreasing, we see that: Applying now the linearity for rational numbers, we see that for every m ≥ N : As a consequence: and by Scott-continuity of ·, it tells us that • We show now that f ∈ Cstab(C, D) → D n f (x | u) ∈ D is linear and Scott-continuous. It is immediate that it is linear, since every one of the f → ∆ n f (x | u) is. We are now going to use 7 to show the Scott-continuity: it tells us that we have only to check that for every Observe that: The linearity of the derivatives means that for every x ∈ B • C, we can extend D n f (x | ·) to a function C x n → D. We will use implicitly this extension in the following, especially in Definition 11.

Taylor Series for pre-stable functions
We have seen above that the D n f are a notion of differential for pre-stable functions. Following further this idea, and the work of McMillan [14], we define an analogue to the Taylor expansion. In all this section C and D are going to be directed complete lattice cones, and f : BC → D a pre-stable function.

Definition 11
Let be x ∈ B • C. We call Taylor partial sum of f in x at the rank N the function The next step consists in establishing that the T N f are actually a non-increasing bounded sequence in the cone of pre-stable functions from C to D, which will allow us to define the Taylor series of f , as the supremum of the T N f (see the long version for more details on the proof).
To that end, we are first going to establish an alternative characterization of the Taylor series, which is the one used in [14], in the framework of abstract domains. It consists in substituting each of the D n f (x | y, . . . , y) with its expression given by Lemma 8 below. The validity of Lemma 10, and thus the equivalence of the two definitions, depends on the fact we work with directed-complete cones.
• We first show that A ≥ D k f (x | y, . . . , y). For every n ∈ N, it holds that π = ( 1 n · y, . . . , 1 n · y) is a partition of y. Therefore for every n ∈ N: The sequence n! (n−k)!·n k tends to 1 when n tends to infinity (see in the long version). By Scott-continuity, it means that A ≥ D k f (x | y, . . . , y).
With this characterization, [14] shows that the sequence of functions (x ∈ BC 1 y → T f n (x | y)) is bounded by (x ∈ BC 1 y → f (x + y)) in the cone of pre-stable functions from C 1 x to D.
Proof. Let be x ∈ B • C and y ∈ BC x . We are able to express f (x + y) by using f (x) and finite differences on any partition of y: indeed, for every partition π of y, it holds that: Proof. It is an algebraic calculation, done in [14]. We give here the proof for n = 2. Let π = [y 1 , y 2 ] a partition of y. Then we see that: Moreover we are also able to express the derivatives of f at x towards the direction y also using the partitions of y (it is the sense of Lemma 8). Accordingly: Using Lemma 5, we see that it implies: We can now use the Scott continuity of + and ·, and we obtain: We can now conclude using (1): The proof of the pre-stability of the function can be found in [14]. It is based on the fact that each one of the above inequality can be seen as an inequality in the cone of pre-stable functions.
Since we have shown that the partial sum of the Taylor series of f was a bounded non-decreasing sequence in the complete cone of pre-stable functions from C 1 x to D, we can now define the Taylor series of f as its supremum.

Definition 12
We define T f (x | ·) : BC 1 x → D the Taylor series of f in x, and Rf (x | ·) : BC 1 x → D the Remainder of f in x as:

Extended Bernstein's theorem
Our goal from here is to show that for any x ∈ B • C, Rf (0 | x) = 0. We recall here the main steps of the proof of [14]. It is based on two technical lemmas, that analyze more precisely the behavior of the remainder of f . The first one is actually a summary of several technical results shown separately in [14].

Lemma 10
Let be x ∈ B • C. Then it holds that both: are pre-stable functions. Moreover Rf x (0) = 0, and for every x ∈ BC 1 y , it holds that T (Rf y )(0 | x) = 0.
Proof. We give here only sketches of the proofs. The detailed proof can be found in [14].
• For Rf y , it is a consequence of the fact that both f y : (x ∈ BC 1 y → f (x + y) and T f y : y → T f (x | y) are pre-stable functions, with T f y ≤ f y in the cone of pre-stable functions, and Rf y = f y − T f y .
• The pre-stability of Rf x is stated in Theorem 4.1. of [14]. It is based on a previous technical lemma shown in [14], which says it is sufficient for a function to be pre-stable, to have all its differences in 0 to be non-negative. Then the idea is to fix x, and to consider for every N ∈ N, the function g N : It is then possible to show that for any n ∈ N, and u ∈ BC n y , . By a computation on the ∆ n (T f N x )(0 | u), we see that the ∆ n g N (0 | u) are non-negative. Then, we conclude using the fact that Rf x (y) = inf N ∈N T f N x (y).
• The fact that Rf x (0) = 0 is a direct consequence of the n-linearity of the map u → D n f (x | u) for n ≥ 1.
• The fact that T (Rf y )(0 | x) = 0 is shown in [14] in Lemma 5.26. It is based on the fact that the Scott-continuity of f → D n f (x | u) allows us to show that if we take g(y) = D n f (x | u), then D k g(x | v) = D n+k f (y 0 | u, v), and from there to compute the Taylor series of Rf y .
The second technical lemma gives us a way to decompose Rf (x | y) into smaller pieces. It is stated in Theorem 5.3 in [14].

Lemma 11
Let be x, y such that x + y ∈ BC. Then Rf (0 | x + y) ≤ Rf (y | x) + Rf (x | y), and furthermore Rf (0 | x + y) ≥ Rf (x | y), and Rf (0 | x + y) ≥ Rf (y | x), and moreover all the inequality are in the cone of pre-stable functions.
Proof. We give here a brief sketch of the proof of the first statement. More details can be found in [14]. We introduce the function Rf +x : y ∈ BC 1 x → Rf (0 | x + y). The proof is based on the fact that it is possible to establish (see [14]): and R(Rf +x )(0 | y) = R(Rf x )(0 | y) As a consequence, we can write: (2) and (3) = Rf +x (y) + T (Rf x )(0 | y) + R(R x f )(0 | y) ≥ Rf +x (y) = Rf (0 | x + y), and we see that we have also shown that the difference is pre-stable. The other two statement are shown in a similar way.
We use Lemma 11 to show the a more involved upper bound on Rf (0 | x).
Proof. For every x ∈ BC, we denote g x : y ∈ BC 1 x → f (x + y). From the definitions of the D n , we see that it holds that Rg x (0 | y) = Rf (x | y).
We are now ready to show the main result of this section. Proof. Let be x ∈ BC. First, we consider the partition π = [ x N , . . . , x N ] of x, with N taken such as x + x N ∈ BC. We know that such an N exists since x is in the open unit ball B • C. We use Lemma 12 on Rf (0 | x), and the partition π, and it tells us that: Observe that the above expression is valid, since for every u i in a partition π of x N , x + u i ∈ BC. We know, by Lemma 10 that Rf (x | 0) = 0. Therefore, we can rewrite (4) as: Moreover, we are able to express the right part of (5) by the finite differences of the pre-stable function Rf x ; indeed for each i, By the definition of derivatives (see Definition 10), we see that We see now that combining (5), (6) and (7) leads us to . Moreover, we know that for every y ∈ BC 1 x , D 1 Rf x (0 | y) ≤ T (Rf x )(0 | y). Hence by using again Lemma 10, which says that T (Rf x )(0 | x N ) = 0, it holds that Rf (0 | x) = 0.

Cstab is a conservative extension of Pcoh !
Probabilistic coherence spaces (PCS) were introduced by Ehrhard and Danos in [3] as a model of higher-order probabilistic computation. It was successful in giving a fully abstract model both of PCF ⊕ , and of a discrete probabilistic extension of Levy's Call-by-Push-Value. In this section, we present briefly basic definitions from [3] and highlight an embedding from PCSs into cones.

Probabilistic Coherence Spaces
The definition of the PCS model of Linear Logic follows the tradition initiated by Girard with Coherence Spaces in [8], and followed for instance by Ehrhard in [5] when defining hypercoherence spaces. A coherent space interpreting a type can be seen as a symmetric graph, and the interpretation of a program of this type is a clique of this graph. Interestingly, such a graph A can be alternatively characterized by giving its set of vertices (that we will call web), and a family of subsets of this web, meant to be the family of the cliques of A. Then we know that an arbitrary family of subsets of a given web arises indeed as a family of cliques for some graph when some duality criterion is verified. PCSs are designed to express probabilistic behavior of programs. As a consequence, a clique is not a subset of the web anymore, but a quantitative way to associate a non-negative real coefficient to every element in the web.

Definition 13 (Pre-Probabilistic Coherent Spaces) A Pre-PCS is a pair X = (|X|, P X),
where |X| is a countable set called web of X, P X is a subset of ⊆ R |X| + whose elements are called cliques of X.
We need here to introduce some notations to deal with infinite dimensional R-vector spaces. Given a countable web A, and a an element of A, we denote e a the vector in R A + which is 1 in a, and 0 elsewhere. We are also going to introduce a scalar product on vectors in R A + : if u, v ∈ R A + , we will denote u, v = a∈|X| u a v a ∈ R ∪ {∞}. Moreover, if A and B are countable sets, x ∈ R A×B + , and u ∈ R A + , we denote by x · u the vector in (R + ∪ {∞}) B given by (x · u) b = a∈A x a,b u a for every b ∈ B.
We are going to give examples of pre-PCS modeling discrete data-types. First, we define a pre-PCS 1 to correspond to unit type. Since unit-type programs have only one possible outcome (that they can reach or not), 1 has only one vertex: |1| = {⋆}. We want the denotation of a unit-type program to express its probability of termination: we take the set of cliques P 1 as the interval [0, 1].
Let us now look at what happens when we consider programs of type N : a program can now have a countable numbers of possible outcomes, so the web will consist of N, and cliques will be sub-distributions on these vertices. We now need to give a quantitative bi-duality criterion, to specify which one of the P X ⊆ R |X| + are indeed valid families of cliques. To do that, we first define a duality operator : if X = (|X|, P X) is a pre-PCS, we define the pre-PCS (X) ⊥ = (|X|, {u ∈ R |X| + , ∀v ∈ P X, u, v ≤ 1}). We are now ready to give conditions on pre-PCSs to actually be PCS: Definition 14 (Probabilistic Coherent Spaces) A pre-PCS X is a PCS if ((X) ⊥ ) ⊥ = X and moreover the following two conditions hold: • ∀a ∈ |X|, there exists λ > 0 such that λe a ∈ P X.
• ∀a ∈ |X|, there exists M ≥ 0, such that for every u ∈ P X, u a ≤ M .
We may see easily that both 1 and N Pcoh are indeed PCSs.
As highlighted in Example 4.4 from [7], we can associate in a generic way a cone to any PCS. The idea is that we consider the extension of the space of cliques by all uniform scaling by positive reals. We formalize this idea in Definition 15 below.

Definition 15
Let be X a PCS. We define a cone C X as the R + semi-module {α · x s.t. α ≥ 0, x ∈ P X} where the + is the usual addition on vectors. We endow it with · CX defined by: It is easily seen that it is indeed a cone (the proof uses the so-called technical conditions from Definition 14). Moreover, we can see that BC X consists exactly of the set P X of cliques of X. Looking at the cone order CX , as defined in Definition 2, we see that it coincides on P X with the pointwise order in R |X| + . It is relevant since we know already from [3] that P X is a bounded-complete and ω-continuous cpo with respect to this pointwise order.

Lemma 13
For every PCS X, it holds that C X is a directed-complete lattice cone.
Proof. To show that C X is directed complete, we use the fact that P X is a complete partial order. To show that it is a lattice, we see that x ∨ y can be defined as: (x ∨ y) a = max x a , y a ∀a ∈ |X|.

The Category Pcoh.
Intuitively a morphism in Pcoh(X, Y ) is a linear map from R |X| + to R |Y | + preserving the cliques.
Definition 16 (Morphisms of PCSs) Let be X, Y two PCSs. A morphism of PCSs between X and Y is a matrix x ∈ R |X|×|Y | + such that for every u ∈ P X, it holds that x · u ∈ P Y .
We now illustrate Definition 16 by looking at the morphisms from Bool to itself: they are the x ∈ R {t,f}×{t,f} + such that x t,t + x t,f ≤ 1, and similarly x f,t + x f,f ≤ 1. We see that they are exactly those matrices specifying the transitions for a probabilistic Markov chain with two states t and f.
We call Pcoh in the following the category of PCS and morphisms of PCS. In [3], it is endowed with the structure of a model of linear logic. We are only going to recall here partly the exponential structure, since our main focus will be on the Kleisli category associated to Pcoh.
In [3], the construction of the exponential was done by defining a functor !, as well as dereliction and digging making Pcoh a Seely category, and consequently a model of linear logic. Here, we are only going to recall explicitly the effect of ! on PCSs. We denote by M f (|X|) the set of finite multisets over the web of X, and we take it as the web of the PCS !X. If µ ∈ M f (A), we call support of µ, and we denote Supp(µ), the set of elements a is A such that a appears in µ. Moreover, we will use the following notation: for every x ∈ R |X| + , and µ ∈ M f (|X|), we denote

Definition 17
Let be X a PCS. We define the promotion of x ∈ P X, as the element

The Kleisli Category of Probabilistic Coherence Spaces
The idea, as usual, is that morphisms in the Kleisli category can use several times their argument, while morphisms in the original category are linear. The Kleisli category for Pcoh, denoted Pcoh ! , has also PCSs for objects, while Pcoh ! (X, Y ) = Pcoh(!X, Y ). We give here a direct characterization of Pcoh ! morphisms.
, if and only if for every x ∈ P X, f · x ! ∈ P Y .
What Lemma 14 tells us is that any f ∈ Pcoh ! (X, Y ) is entirely characterized by the map f : x ∈ P X → f · x ! ∈ P Y . We denote by E X,Y the set of all maps P X → P Y that are equal to a f with f ∈ Pcoh ! (X, Y ). It has been shown in [3] that (·) is actually a bijection from Pcoh ! (X, Y ) to E X,Y .
Observe that we can see the maps in E X,Y as entire series, in the sense that they can be written as the supremum of a sequence of polynomials. Indeed, for any morphism f , and x ∈ P X, we can write: As the Kleisli category of the comonad ! in a Seely category, Pcoh ! is a cartesian closed category. We give here explicitely the construction of the product and arrow constructs: if X and

A fully faithful functor
Recall that Definition 15 gave a way to see a PCS as a cone. Moreover, as stated in Proposition 2 below, a morphism in Pcoh ! can also be seen as a stable function, in the sense that E X,Y ⊆ Cstab(C X , C Y ).
Proposition 2 Let be f ∈ Pcoh ! (X, Y ). Then f is a stable function from C X to C Y .
Proof. We know from [3] that f : P X → P Y is sequentially Scott-continuous with respect to the orders CX , CY . Moreover f is pre-stable: it comes from the fact that f can be written as a power series with all its coefficients non-negative. Finally, we have to show that f (BC X ) ⊆ BC Y ). Since BC X = P X, BC X = P X, and moreover f is a morphism in Pcoh ! (X, Y ), we see that the result holds.
Thus we can define a functor F : Pcoh ! → Cstab, by taking F X = C X , and F f = f . Our goal now is to show that F is full and faithful, which will make Pcoh ! a full subcategory of Cstab. As mentioned before, it was shown in [3] that · is a bijection from Pcoh ! (X, Y ) to E X,Y . It tells us directly that F is indeed faithful. In the remainder of this section, we are going to show that F is actually also full, hence makes Cstab a conservative extension of Pcoh ! .
In the following, we fix X and Y two PCSs, and g ∈ Cstab(F X, F Y ). Our goal is to show that there exists f ∈ Pcoh ! (X, Y ) such that f = g. First, recall that we have shown in Lemma 13 that for every PCS Z, the cone F Z is a directed complete lattice cone. It means that all results in Section 3.3 can be used here: in particular, g has higher-order derivatives D n g, which makes Definition 18 below valid.
We have to show now that f ∈ Pcoh ! (X, Y ), and that f coincides with g on P X. The key observation here is that we have actually built f in such a way that it is going to coincide with T g(0 | ·)-the Taylor series of g defined in Definition 12. We first show it for the elements of P X with finite support, by using finite additivity of the D k g(0 | ·).

Lemma 15
Let be x ∈ P X, such that Supp(x) = {a ∈ P X | x a > 0} is finite. Then it holds that f · x ! is finite (i.e for every b ∈ |Y |, (f · x ! ) b < ∞), and moreover f · x ! = T g(0 | x).
Proof. Let A = {a 1 , . . . , a m } ⊆ |X| be the set Supp(x). For any b ∈ |Y |, we can deduce from the definition of f that: where M k f (A) stands for the set of multisets over A of cardinality k. Looking at the definition of α µ , we see that this implies: By Lemma 6, we know that D k g(0 | ·) is k-linear. As a consequence, and since x = m i=1 x ci · e ci and that moreover A is finite, we see that (8) implies the result: We are now going to apply the generalized Bernstein's theorem, as stated in Proposition 1, to the stable function g from F X to F Y . It tells us that: Combining (9) with Lemma 15, we obtain that: We can now use (10) to show that f and g coincide on P X: the key point is that the subset of elements in P X of norm smaller than 1 and finite support is dense, and that moreover g is Scott-continuous.
Proof. Let be x ∈ P X. We define a sequence (y n ) n ∈ N of elements in P X, by taking: where we have fixed λ an arbitrary enumeration of the elements of |X|-λ exists since it is a countable set. Observe the the sequence (y n ) n∈N is non-decreasing, with x = sup n∈N y n . Moreover, for every n, y n has finite support and y n CX < 1 . It means that for every y n , we can use (10): we see that g(y n ) = f · y ! n . Since g is a morphism in Cstab, g is sequentially Scott-continuous, hence: g(x) = sup n∈N g(y n ).
Moreover, we know from [3] that both x → x ! and x → u · x are Scott continuous. It means that: Combining (11) and (12), we obtain f · x ! = g(x). Since g(BC X ) ⊆ BC Y , it implies also that f (P X) ⊆ P Y . Thus by Lemma 14 f ∈ Pcoh ! (X, Y ).
Since we have indeed been able to show in Lemma 16 that for any fixed stable function g in Cstab(F X, F Y ), there exists an f ∈ Pcoh ! (X, Y ) such that F f = g, we have indeed shown that F is full.

F preserves the cartesian structure.
We want now to give a stronger guarantee on the functor F : we want to show that it is a cartesian closed functor, meaning that it embeds the cartesian closed category Pcoh ! into the cartesian closed category Cstab in such a way that: • F preserves the product: for every family (X i ) i∈I of PCSs, F ( • F preserves function spaces: for every X, Y PCSs, Lemma 17 F preserves cartesian products. Proof. We fix a family I = (X i ) i∈I of PCSs. In order to construct an isomorphism, we have a canonical candidate, given by: Let us now see that Ψ I is an isomorphism, . Looking at the definition of cartesian product in Pcoh ! defined in Section 4.3, and the one of cartesian product in Cstab, defined in Section 3.2, we see that for every x ∈ BF ( Pcoh ! i∈I X i ): Ψ I (x) = (y i ) i∈I where ∀i ∈ I, ∀a ∈ |X i |, (y i ) a = x (i,a) .
We want now to show that Ψ I has an inverse. The only candidate is Θ I : y ∈ B( Cstab i∈I F X i ) → Θ(y) ∈ (F ( Pcoh ! i∈I X i )), defined by: ∀i ∈ I, a ∈ |X i |, Θ(y) i,a = (y i ) a . We see immediately that Θ I is linear, hence pre-stable, and that moreover it is Scott-continuous. Besides, it is also preserves the unit ball, since ∀y ∈ BD, Θ I (y) F ( Pcoh ! i∈I Xi) = y Cstab i∈I F Xi . We show now that Θ I preserves the unit ball: Thus Θ I is a morphism in Cstab.
Lemma 18 F preserves function spaces.
Proof. Let X, Y two PCSs. As previously, there is a canonical candidate for the isomorphism: we define Υ X,Y as the currying in Cstab of the morphism: where Θ X⇒Y,X is as defined in the proof of Lemma 17 above.
Unfolding the definition, we see that actually: Since we have shown that F is full and faithful, we can consider Ξ X,Y the inverse function of Υ X,Y . Recall from the proof of the fullness of F in Section 4.4 that for every µ = [a 1 , . . . , a k ] ∈ M f (|X|), and b ∈ |Y |: Recall from Lemma 6 that for any u ∈ B(C k x ), the function f ∈ Cstab(F X, F Y ) → D k f (x | u) ∈ F Y is linear and Scott-continuous. As a consequence, Ξ X,Y too is linear and Scott-continuous.
To know that Ξ X,Y is stable, we have still to show that it is bounded: we are actually going to show that it preserves the norm. Indeed, for every f ∈ B(F X ⇒ F Y ), we see using the definition of the norm on a cone obtained from a PCS (see Definition 15), that: It was shown in [3] that: We see that (r · Ξ X,Y (f )) · x ! = r · f (x) since Ξ X,Y has been defined as the inverse of Υ X,Y . It means that we can rewrite (15) as: Since for every PCS Z, it holds that P Z = BF Z, we can now use (16) to rewrite (14) as: Looking now at the definition of the norm in the cone F X ⇒ F Y , we can complete the proof using (17) and the homogeneity of the norm. Indeed: As a direct consequence of Lemma 17 and Lemma 18, we can state the following theorem: Theorem 1 F is full and faithful, and it respects the cartesian closed structures.

Adding Measurability Requirements
In [7], the authors developed a sound and adequate model of PCF sample based on stable functions. However, as explained in more details in [7], they need to add to their morphisms some measurability requirements, both on cones and on functions between them, since the denotational semantics of the let(x, M, N ) construct uses an integral, to model the fact that M is evaluated before being passed as argument to N . We call measurable functions R n → R k the functions measurable when both R n and R k are endowed with the Borel Σ-algebra associated with the standard topology of R. The relevant properties of the class of measurable functions R n → R k is that they are closed by arithmetic operations, composition, and pointwise limit, see for example Chapter 21 of [16].

The category Cstab m
Cstab m is built as a refinement of the category Cstab. The objects of Cstab m are going to be complete cones, endowed with a family of measurability tests.
If C is a complete cone, we denote by C ′ the set of linear and Scott-continuous functions C → R + .

Definition 19
A measurable cone (MC) is a pair consisting of a cone C, and a collection of measurability tests (M n (C)) n∈N ), where for every n, M n (C) ⊆ C ′ R n , such that: • for every n ∈ N, 0 ∈ M n (C); • for every n, p ∈ N, if l ∈ M n (C), and h : R p → R n is a measurable function, then l • h ∈ M p (C); • for any l ∈ M n (C), and x ∈ C, the function u ∈ R n → l(u)(x) ∈ R is measurable.
Example 5 (from [7]) Let X be a measurable space. We endow the cone of finite measures Meas(X) with the family M(X) of measurable tests defined as: where Σ X is the set of all measurable subsets of X. Observe that in this case, the measurable tests correspond to the measurable sets. In the following, we will denote Meas(X) the measurable cone (Meas(X), (M n (X)) n∈N ).
We define now measurable paths, which are meant to be the admissible ways to send R n into a MC C.
Definition 20 (Measurable Paths) Let be (C, (M n (C)) n∈N ) a measurable cone. A measurable path of arity n at C is a function γ : R n → C, such that γ(R n ) is bounded in C, and for every k ∈ N, for every l ∈ M k (C), the function ( r, s) ∈ R k+n → l( r)(γ( s)) ∈ R + is a measurable function.
We denote Paths n (C) the set of measurable paths of arity n for the MC C . When a measurable path γ verify γ(R n ) ⊆ BC , we say it is unitary. Using measurable paths, the authors of [7] add measurability requirements to their definition of stable functions.
Definition 21 Let be C, D two MCs. A stable function f : BC → D is measurable if for all unitary γ ∈ Paths n (C), f • γ ∈ Paths n (D).
The category Cstab m is therefore the category whose objects are MCs, and whose morphisms are measurable stable functions between MCs.
Example 6 Recall the function real Cstabm defined in Section 2: We can see that real Cstabm is a measurable function from Meas(N) into Meas(R). Moreover it is linear and Scott-continuous, and norm-preserving, which makes it a morphism in Cstab m .
In the same way, taking Meas(N) as the denotational semantics of type N , we could complete the denotationnal semantics given in [7] for PCF sample in Cstab m into a denotational semantics for PCF ⊕,sample .
Observe that real Cstabm would not be measurable, if we endowed Meas(N) with for instance {0} as measurability tests instead of M(N): indeed in that case, every γ : R n → Meas(N) would be a measurability path. As a consequence, to be a measurable function, real Cstabm should verify: for every arbitrary function γ : R n → Meas(N), real Cstabm • γ is a measurable path on Meas(R). However, we can see this is not the case, for instance by considering γ of the form γ(s) = α(s) · {0} 1 , where α : R → R + is not Borel measurable.
In [7], the cartesian closed structure of Cstab m is derived from that of Cstab by endowing its exponentials and products with the measurability tests presented in Figure 2.

Pcoh ! is a full subcategory of Cstab m
We want now to convert the functor F : Pcoh ! → Cstab into a functor F m : Pcoh ! → Cstab m . To build F m , we are going to endow each F X with measurability tests, in such a way that F (f ) will be a measurable stable function for any morphism f ∈ Pcoh ! . Observe that this requirement does not determine uniquely the choice of measurability tests. For instance, it would be verified if we choose {0} as measurability tests for every F X. However, as explained in Section 2, we want also F m (N Pcoh ) to be isomorphic to N Cstabm : we would like to be able to inject any discrete distribution on N into a distribution on R. A natural way to ensure this is to use the discrete structure of the web to give the following definition of the MC arising from a PCS.

Definition 22
For any X ∈ Pcoh, we define C X as the measurable cone C X endowed with the family M n (X) n∈N of measurability tests defined as M n (X) = {0} ∪ {ǫ a | a ∈ |X|}, where ǫ a ( r, x) = x a .
We see that the ǫ a are indeed linear (i.e commuting with linear combinations), and moreover Scottcontinuous: hence they are indeed element of C ′ X . It is easy to verify that the other conditions are verified, and so C X is indeed a MC.

Lemma 19
Let be X a PCS. Then Paths n (C X ) is the set of those γ : R n → C X such that: • ∃λ ∈ R, γ(R n ) ⊆ λBC X • ∀a ∈ |X|, γ a : r ∈ R n → γ( r) a ∈ R + is measurable.
Two MCs with the same underlying cone, but different measurability tests may be isomorphic in Cstab: it is enough for them to have the same measurable paths. It is what happens in the example below, where we consider C N Pcoh and Meas(N). It is actually also what happens at higher-order types, as we will explain in Section 5.3.

Example 7
The two measurable cones C N Pcoh and Meas(N) have the same underlying cone, but they do not have the same measurable tests. Indeed: But we can prove that they have the same measurable paths. It is immediate that Paths n (Meas(N)) ⊆ Paths n (C N Pcoh ), since M n (C N Pcoh ) is a subset of M n (Meas(N)). We detail now the proof of the reverse inclusion. Let γ ∈ Paths n (C N Pcoh ). We have to show: for every U ⊆ N, the function is Borel measurable.
Since the class of Borel measurable functions are closed by finite sum and pointwise limit, it leads to the result.
Lemma 20 Let X, Y be two PCSs, and f ∈ Pcoh Proof. We have to show that F f preserves measurable paths. Let γ a unitary path in Paths n (C X ): our goal is to show that f • γ ∈ Paths n (C Y ). Recall that Lemma 19 gives us a characterization of Paths n (C Y ). Since γ and F f are bounded, we see immediately that F f • γ is bounded. Let b be in |Y |. We see that: Since γ ∈ Paths n (C X ), it holds that γ a : R n → R + is measurable for all a ∈ |X|. We conclude by using the fact that the class of measurable functions R n → R + is closed under multiplication, finite sums and limit of non-decreasing sequences: it tells us that r ∈ R n → (F f • γ) b ( r) ∈ R + is measurable, and the result folds.

Theorem 2
The functor F m : Pcoh ! → Cstab m defined as F m X = C X , and F m f = F f , is full and faithful.
Proof. Observe that we can decompose the functor F as F = Forget • F m , where Forget is the forgetful functor from Cstab m to Cstab. We know from Section 4.4 that F is full and faithful. Moreover, it holds that Forget is faithful. From there, we are able to deduce the result: • F m is faithful: it is implied by the fact that F is faithful.
• F m is full: indeed suppose that it is not the case: then there exist two PCSs X, Y , and f ∈ Cstab m (F m X, F m Y , such that f is not in the image by F m of Pcoh(X, Y ). Then we consider g ∈ Cstab(F X, F Y ) defined by g = Forget(f ). Since Forget is faithful, there is no other f ′ such that g = Forget(f ′ ): it means that g is not in the image by Forget • F m of Pcoh(X, Y ). But since F = Forget • F m is full, we have a contradiction.

F m is cartesian closed.
We want now to show that just as F , F m is cartesian closed. Since the forgetful functor from Cstab m to Cstab is cartesian closed, we see that we have only to show that the Cstab-morphisms Ψ I , Θ I , Υ X,Y and Ξ X,Y defined in Lemmas 17 and Lemma 18 proofs, are also morphisms in Cstab m .
Lemma 21 Let X be a PCS, C any measurable cone, and f ∈ Cstab(Forget(C), F X). We suppose that for every unitary γ ∈ Paths n (C): Then it holds that f ∈ Cstab m (C, F m X).
Proof. Since we already know that f is a morphism in Cstab, hence we have only to show that it preserves measurable paths. Let γ be unitary in Paths n (C). We are going to use Lemma 19 to show that f • γ is a measurable path for F m X. The second condition in Lemma 19 holds by hypothesis. The first condition also holds: since both f and γ are bounded, f • γ is bounded too. So Lemma 19 tells us that f • γ ∈ Paths n (F m X).
Lemma 22 For all I = (X i ) i∈I a finite family of PCSs, Proof.
• Recall that Ψ I is defined canonically in Equation (13) as Ψ I = F (π i ) | i ∈ I , where · is the cartesian product on morphisms in Cstab. Since the cartesian product on morphisms in Cstab m is the same as the one in Cstab (see [7]), and moreover F (π i ) = F m (π i ), we see that Ψ I is also a morphism of Cstab m .
• Using Lemma 21, we see that it is enough to show that for all γ in Paths n ( Cstabm i∈I F m X i ), for all (i, a i ) ∈ | Pcoh ! i∈I X i |, (Θ I • γ) (i,ai) is measurable. By looking at the definition of Θ I , we see that (Θ I • γ) (i,ai) ( r) = (γ( r) i ) a . We see now that we can construct a measurability test m ∈ M 0 ( Cstabm i∈I F m X i ) such that (γ( r) i ) a = m(·)(γ( r)): it is enough to take m = ⊕ j∈I l j , with l j = 0 if j = i, and l i = ǫ ai . Since γ is a measurability test, it means that r ∈ R n → m(·)(γ( r)) ∈ R + is measurable, and so the result holds.
Lemma 22 allows us to see that F m is a cartesian functor. We want now to show that it also respects the ⇒ construct. First, we show that the Cstab morphism Υ X,Y is also a morphism in Cstab m .
Lemma 23 For all X, Y PCSs, Proof. Recall that Υ X,Y is defined using currying in Cstab, Θ X⇒Y,X , and the eval morphism in Cstab. Since currying and structural morphisms are the same in Cstab m as in Cstab, and moreover we have shown in Lemma 22 that Θ X⇒Y,X is a morphism in Cstab, we have the result.
We show now that Ξ X,Y is also a Cstab m morphism, by using Lemma 21. To do that, we need to show that (Ξ X,Y • γ) µ,b is Borel measurable for every (µ, b) ∈ |X ⇒ Y |. Our proof strategy is the following: first we show that it can be written as a higher-order partial derivative of a (Borel) measurable function, and then we show that under some conditions on the domain, the partial derivative of a Borel measurable function is again Borel measurable.
Proof. We take Using Lemma 19, we see that indeed δ ∈ Paths p (F m X). Observe that ψ f δ ( t) = ν|Supp(ν)⊆{a1,...,an} f ν,b · t ν . From there, by using therorems of real analysis for normally convergent series of functions, we can deduce the result (the complete proof may be found in the long version).
Proof. Since γ is a measurable path, we know that for every p ∈ N, and l ∈ Paths p (F m X), ǫ b ⊲ l is a measurability test on F m X ⇒ F m Y , and therefore: ( r, u) ∈ R p+n → (ǫ b ⊲ l( r))(γ( u)) ∈ R + is measurable.
We are going to apply (18) to a particular measurable path on F m X. Let p be the cardinality of Supp(µ), and {a 1 , . . . , a p } = Supp(µ). We define l µ : R p → F m X as: l µ : r ∈ R p → 1≤i≤m r i · e ai if r i ≥ 0∀i and 1≤i≤m r i ≤ 1; 0 otherwise. We see that l µ (R p ) is bounded in F m X, and moreover for every a ∈ |X|, the function r ∈ R p → l µ ( r) a ∈ R + is measurable. Using the characterization of Paths p (F m X) in Lemma 19, we see that l µ is in Paths p (F m X). Thus we can apply (18) with l = l µ . Observe that (ǫ b ⊲ l µ ( r))(γ( u)) = (γ( u)(l µ ( r))) b . Therefore (18) tells us that φ µ,b : R p+n → R + is measurable, with φ µ,b defined as φ µ,b : ( r, u) ∈ R p+n → γ( u)(l µ ( r)) b ∈ R + . We define J ⊆ R p as [0, 1 p [ p . We are going to look at the restriction of the function φ µ,b to J × R n : indeed we are going to show that φ µ,b has partial derivatives on that interval. We define ψ µ,b : J × R n → R + as the restriction of φ µ,b to J × R n . Since φ µ,b is a measurable function, and J × R n a measurable subset of R p+n , ψ µ,b also is measurable.
Lemma 25 below (which is proved in the long version) is key: it says that we can recover the coefficients of the power series ψ µ,b by looking at its partial derivatives. We will then show that we can do it in a measurable way. Proof. Since l µ ( r) = 1≤i≤p r i · e i for r ∈ J, we see that: For a fixed s, we can see it as a generalization of entire series in real analysis. There are well-known results about the differentiation of such series: for instance, a uniformly convergent entire series is differentiable on its (open) domain of convergence. Here, we are going to show the counterpart of some properties on entire series, on what we call multisets series of p real variables: those are the series of the form S( r) = ν∈M f (1,...,p) a ν · r ν where r ∈ R p .
First, we observe that for each r, we can look at S( r) as an infinite sum over natural numbers: ..,m)|card(µ)=n a µ · r µ ).
We recall here a classical result of real analysis on power series, that we will use in the following.
Lemma 26 [Derivation of a series] Let f n : I → R be a sequence of functions from a bounded interval I. We suppose that f (x) = n∈N f n (x) is convergent for every x ∈ I, and moreover for each n ∈ N, f n is derivable and n∈N f ′ n is uniformly convergent on I. Then f is derivable, and moreover f ′ = n∈N f ′ n .
Lemma 27 Let p ∈ N, and S( r) = ν∈M f ({1,...,p}) a ν · r ν with non-negative coefficients a µ , such that S is convergent on an interval I = [−c, c] p , with c > 0. Then there exists 0 < b < c, such that the function g : r ∈] − b, b[ p → S( r) ∈ R is partially derivable in each of the r i variables, and moreover: Proof. We take b = c 2 , and set J =] − b, b[. To simplify the notations, we suppose here that i = 1, but the proof is the same in other cases. We want to show that for any fixed u ∈ J p−1 , the function h u : r → g(r, u) is derivable on J. Let us fix u ∈] − b, b[ p−1 . We are going to use Lemma 26 on h u . We see that h u (r) = n∈N h n (r), where h n (r) = ( ν∈M f (2,...,p) a ν+[1 n ] · u ν ) · r n , where [1 n ] is the multiset consisting of n occurrences of 1. We see that for every n ∈ N, the function h n is derivable on J, and: h ′ n (r) = ( ν∈M f (2,...,p) a ν+[1 n ] · u ν ) · n · r n−1 .
We see now that the series n∈N h ′ n is uniformly convergent on J: for every r ∈ J, it holds that: |h ′ n (r)| ≤ ( We end the proof of Lemma 25 by using Lemma 28 for each u ∈ R n on the multiset series given by S u ( r) = ν∈M f ({1,...,p}) (Ξ X,Y γ( u)) ν,b · r ν .
We see that it is indeed absolutely convergent on I =] − 1 p , 1 p [ p , using the fact that for r ∈ [0, 1 p ] p , S u ( r) = ψ µ,b ( r, u) for r ∈ R p .
Proof. We take α µ , δ, c as given by Lemma 24. Since ǫ b ⊲ δ is a measurability tests for F m X ⇒ F m Y , we see that the function ( t, s) ∈ R p+n → ψ γ( s) δ ( t) = (ǫ b ⊲ δ)( t)(γ( s)) ∈ R + is measurable. Since K = [0, c[ p ×R n is a measurable subset of R p+n , the restriction (that we denote φ) of this function to K is measurable too. Moreover, observe that Ξ X,Y • γ( s) ∈ P (X ⇒ Y ) and Ξ X,Y • γ( s) = γ( s). It tells us that we can apply Lemma 24, and we see that: (observe that this partial derivatives exists since it exists for ψ γ(s) δ for every fixed s). We are now going to show that every partial derivative of φ, when it exists, is measurable too. It is based of the fact that the class of real-valued measurable functions is closed by addition, multiplication by a scalar and pointwise limit. Indeed, there exists a poitive sequence (r n ) n∈N in [0, c[ which tends towards 0. As a consequence, the partial derivative of φ with respect to t 1 (for instance) may be written as: ∂φ ∂t1 (0, t, s) = lim n→∞ f n ( t, s), with f n ( t, s) = φ((rn, t), s)−φ((0, t), s) rn . It tells us that (( t, s) ∈ R p−1+n → ∂φ ∂t1 (0, t, s)) is the pointwise limit of a sequence of measurable functions, hence is measurable. By iterating this reasonning, we see that it is also the case for higher-order partial derivatives (when they exists), and (20) allows us to conclude the proof.
Lemma 30 For all X, Y PCSs, Ξ X,Y ∈ Cstab m (F m X ⇒ F m Y, F m (X ⇒ Y )).
Theorem 3 F m is a cartesian closed full and faithful functor.

Conclusion
Our full embedding of Pcoh ! into Cstab implies that every stable function f from P X to P Y can be characterized by an element Ξ X,Y (f ) ∈ R M f (|X|)×|Y | , that has to be seen as a power series. It gives us a concrete representation of stable functions on discrete cones, similar to the notion of trace introduced by Girard in [8] for stable functions on quantitative domains. There are well-known real analysis results on power series, as for instance the uniqueness theorem-any power series which is null on an open subset has all its coefficients equal to 0-on which is based the proof of full abstraction for PCF ⊕ in Pcoh ! [6]. While we have not been able to extend such a concrete representation to cones which are not directed-complete, as for instance the cone Meas(R) ⇒ m Meas(R), our result could hopefully be a first step in this direction. This kind of characterization could lead to a way towards a full abstraction result for the continuous language PCF sample in Cstab m , and more generally gives us new tools to reason about continuous probabilistic programs.