Fredrik Dahlqvist
email: f.dahlqvist@ucl.ac.uk

Alexandra Silva
email: alexandra.silva@ucl.ac.uk

Vincent Danos
email: vincent.danos@ens.fr

Ilias Garnier
email: ilias.garnier@ens.fr

Borel Kernels and their Approximation, Categorically

Keywords: Borel Kernels and their Approximation, Categorically Probabilistic programming, probabilistic semantics, Markov process, Bayesian inference, approximation

de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Finding a good category in which to study probabilistic programs is a subject of active research [START_REF] Clerc | Pointless learning[END_REF][START_REF] Kozen | Kolmogorov Extension, Martingale Convergence, and Compositionality of Processes[END_REF][START_REF] Staton | Commutative semantics for probabilistic programming[END_REF][START_REF] Staton | Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints[END_REF]. In this paper we present a dagger symmetric monoidal category of kernels whose dagger-structure is given by Bayesian inversion. The advantages of this new category are two-fold.

Firstly, the most important new construct introduced by probabilistic programming, viz. Bayesian inversion, is interpreted completely straightforwardly by the †-operation which is native to our category. In particular we never leave Pre-print, March 2018 the world of kernels and we therefore do not require any normalization construct. Consider for example the following simple Bayesian inference problem in Anglican ( [START_REF] Wood | A New Approach to Probabilistic Programming Inference[END_REF])

( defquery example
( let [ x ( sample ( normal 0 1))] ( observe ( normal x 1) 0.5) ( > x 1)))

The semantics of this program is build easily and compositionally in our category:

• The second line builds a Borel space equipped with a normally distributed probability measure -an object (R, µ) of our category. • The (normal x 1) instruction builds a Borel kernel -a morphism f : (R, µ) → (R, ν ) in our category. • The observe statement builds the Bayesian inverse of the kernel -the morphism f † : (R, ν ) → (R, µ) in our †-category. • Finally, the kernel f † is evaluated, i.e. the denotation of the program above is f † (0.5)(]1, ∞[).

The functoriality of † ensures compositionality. Second, since Bayesian inference problems are in general very hard to compute (although the one given above has an analytical solution), it makes sense to seek approximate solutions, i.e. approximate denotations to probabilistic programs. As we will show, our category of kernels comes equipped with a generic and endogenous approximating scheme which relies on its involutive structure and on the structure of standard Borel spaces. Moreover, this approximation scheme can be shown to converge for any choice of kernel for a natural choice of topology.

Main contributions.

2. We introduce the category BL σ of Banach lattices and σorder continuous positive operators as well as the Köthe dual functor (-) σ : BL op σ → BL σ ( §3). These will play a central role in studying convergence of our approximation schemes. [START_REF] Bogachev | Measure Theory I[END_REF]. We provide the first 2 categorical understanding of the Radon-Nikodym and the Riesz representation theorems. These arise as natural transformations between two functors relating kernels and Banach lattices ( §4). 4. We show how the †-structure of Krn can be exploited to approximate kernels by averaging ( §5). Due to an important structural feature of Krn (Th. 1) every kernel in Krn can be approximated by kernels on finite spaces. 5. We show a natural class of approximations schemes where the sequence of approximating kernels converges to the kernel to be approximated. The notion of convergence is given naturally by moving to BL σ and considering convergence in the Strong Operator Topology ( §6). 6. We apply our theory of kernel approximations to two practical applications ( §7). First, we show how Bayesian inference can be performed approximately by showing that the †-operation commutes with taking approximations. Secondly, we consider the case of ProbNetKAT, a language developed in [START_REF] Foster | Probabilistic netkat[END_REF][START_REF] Smolka | Cantor meets Scott: Domain-theoretic foundations for probabilistic network programming[END_REF] to probabilistically reason about networks. ProbNetKAT includes a Kleene star operator (-) * with a complex semantics which has proved hard to approximate. We show that (-) * can be approximated, and that the approximation converges.

All the proofs can be found in the Appendix.

Related work. Quasi-Borel sets have recently been proposed as a semantic framework for higher-order probabilistic programs in [START_REF] Staton | Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints[END_REF]. The main differences with our approach are: (i) unlike [START_REF] Staton | Commutative semantics for probabilistic programming[END_REF][START_REF] Staton | Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints[END_REF] we never leave the realm of kernels, and in particular we never need to worry about normalization. This makes the interpretation of observe statements, i.e. of Bayesian inversion, simpler and more natural. However, (ii) unlike the quasi-Borel sets of [START_REF] Staton | Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints[END_REF], our category is not Cartesian closed. We can therefore not give a semantics to all higher-order programs. This shortcoming is partly mitigated by the fact that the category of Polish space, on which our category ultimately rests, does have access to many function spaces, in particular all the spaces of functions whose domain is locally compact. We can thus in principle provide a semantics to higher-order programs, provided that λ-abstraction is restricted to locally compact spaces like the reals and the integers, although this won't be investigated in this paper.

The approximation of probabilistic kernels has been a topic of investigation in theoretical computer science for nearly twenty years (see e.g. [START_REF] Chaput | Approximating Markov Processes by averaging[END_REF][START_REF] Danos | Conditional expectation and the approximation of labelled Markov processes[END_REF][START_REF] Desharnais | Metrics for labelled Markov processes[END_REF][START_REF] Desharnais | Approximating labeled Markov processes[END_REF]), and for much longer in the mathematical literature (e.g. [START_REF] Choo-Whan | Approximation theorems for Markov operators[END_REF]). Our results build 2 To the best of our knowledge. on the formalism developed in [START_REF] Chaput | Approximating Markov Processes by averaging[END_REF] with the following differences: (i) we can approximate kernels, their associated stochastic operator (backward predicate transformer), or their associated Markov operator (forward state transformer) with equivalent ease, and move freely across the three formalisms. (ii) Given a kernel f : X Y , we can define its approximation f ′ : X ′ → Y ′ along any quotients X ′ of X and Y ′ of Y as in [START_REF] Chaput | Approximating Markov Processes by averaging[END_REF], but we can also 'internalize' the approximation as a kernel f * : X → Y of the original type. Morally f ′ and f * are the same approximation, but the second approximant, being of the same type as the original kernel, can be compared with it. In particular it becomes possible to study the convergence of ever finer approximations, which we do in Section 6. Finally, (iii) we opt to work with Banach lattices rather than the normed cones of [START_REF] Chaput | Approximating Markov Processes by averaging[END_REF][START_REF] Selinger | Towards a semantics for higher-order quantum computation[END_REF] because it allows us to formulate the operator side of the theory very naturally, and it connects to a large body of classic mathematical results ( [START_REF] Aliprantis | [END_REF][START_REF] Zaanen | Introduction to operator theory in Riesz spaces[END_REF]) which have been used in the semantics of probabilistic programs as far back as Kozen's seminal [START_REF] Kozen | Semantics of probabilistic programs[END_REF].

A category of Borel kernels

In [START_REF] Clerc | Pointless learning[END_REF] the first three authors presented a category of Borel kernels similar in spirit to the construction of this section, but with a major shortcoming. As we will shortly see, our category Krn of Borel kernels can be equipped with an involutive functor -a dagger operation † in the terminology of [START_REF] Selinger | Dagger compact closed categories and completely positive maps[END_REF] -which captures the notion of Bayesian inversion and is absolutely crucial to everything that follows. In [START_REF] Clerc | Pointless learning[END_REF] this operation had merely been identified as a map, i.e. not even as a functor. In this section we show that Bayesian inversion does indeed define a †-structure on a more sophisticatedbut measure-theoretically very natural -category of kernels.

Standard Borel spaces and the Giry monad

A standard Borel space -or SB space for short -is a measurable space (X , S) for which there exists a Polish topology T on X whose Borel sets are the elements of S, i.e. such that S = σ (T ) (see e.g. [START_REF] Kechris | Classical descriptive set theory[END_REF] for an overview). Let us write SB for the category of standard Borel spaces and measurable maps.

One key structural feature of SB is the following: Theorem 1. Every SB object is a limit of a countable codirected diagram of finite spaces.

The Giry monad was originally defined in two variants [START_REF] Giry | A Categorical Approach to Probability Theory[END_REF]: -As an endofunctor G Pol of Pol, the category of Polish spaces, one sets G Pol (X , T ) to be the space of Borel probability measures over X together with the weak topology. This space is Polish [START_REF] Kechris | Classical descriptive set theory[END_REF]Th 17.23], and the Portmanteau Theorem [START_REF] Kechris | Classical descriptive set theory[END_REF]Th 17.20]) gives multiple characterizations of the weak topology.

-As an endofunctor G Meas of Meas, the category of measurable spaces, one sets G Meas (X , S) to be the set of probability measures on X together with the initial σ -algebra for the maps ev A : G Meas (X , S) → R, µ → µ(A), A ∈ S.

In both cases the Giry monad is defined on an arrow f : X → Y as the map f * which sends a measure µ on X to the pushforward measure f * µ on Y , defined as G(f

)(µ)(B) = f * µ(B) := µ(f -1 (B)) for B a measurable subset of Y .
We want to define the Giry monad on the category SB of standard Borel spaces (and measurable maps), and the two versions of the Giry monad described above offer us natural ways to do this: given an SB space (X , σ (T )) we can either compute G Pol (X , T ) and take the associated standard Borel space, or directly compute G Meas (X , σ (T )). Fortunately, the two methods agree.

Theorem 2 ([16], Th 17.24). Let B : Pol → SB denote the functor sending a Polish space (X , T ) to its associated SB-space (X , σ (T )) and leaving morphisms unchanged, then

G Meas • B = B • G Pol .
We define the Giry monad on SB spaces to be the endofunctor G : SB → SB defined by either of the two equivalent constructions above. The monadic data of G is given at each SB space X by the unit δ X : X → GX , x → δ x , the Dirac δ measure at x, and the multiplication m X : G 2 X → GX , P → λA.

∫ GX ev A dP. We refer the reader to [START_REF] Giry | A Categorical Approach to Probability Theory[END_REF] for proofs that δ X and m X are measurable.

The construction of Krn

Let us denote by SB G the Kleisli category associated with the Giry monad (G, δ, m). We denote Kleisli arrows, i.e. Markov kernels, by X Y , and we call such an arrow deterministic if it can be factorized as an ordinary measurable function followed by the unit δ . Kleisli composition is denoted by •. The category * ↓ SB G has arrows * X as objects, where * is the one point SB space (the terminal object in SB). An arrow from µ : *

X to ν : * Y is a SB G arrow f : X Y such that ν = f • µ, i.e. such that ν(A) = ∫ X f (x)(A)
dµ for any measurable subset A of Y . This situation will be denoted in short by f : (X , µ) (Y , ν ), and we will call a pair (X , µ) a measured SB space.

We want to construct a quotient of * ↓ SB G , such that two * ↓ SB G arrows are identified if they disagree on a null set w.r.t. the measure on their domain. For д, д ′ :

(X , µ) (Y , ν ), we define N (д, д ′ ) = {x ∈ X | д(x) д ′ (x)}. Lemma 3. N (д, д ′ ) is a measurable set.
We now define a relation ∼ on Hom((X , µ), (Y , ν )) by saying that for any two arrows д, д ′ :

(X , µ) (Y , ν), д ∼ д ′ if µ(N (д, д ′ )) = 0.
This clearly defines an equivalence relation on Hom((X , µ), (Y , ν )). In order to perform the quotient of the category * ↓ SB G modulo ∼, we need to check that it is compatible with composition.

Proposition 4. If д ∼ д ′ , then h • д • f ∼ h • д ′ • f . Definition 5.
Let Krn be the category obtained by quotienting * ↓ SB G hom-sets with ∼.

The following Theorem is of great practical use and generalizes the well-known result for deterministic arrows.

Theorem 6 (Change of Variables in Krn). Let f : (X , µ) (Y , ν ) be a Krn-morphism. For any measurable function ϕ :

Y → R, if ϕ is ν-integrable, then ϕ • f (x) = ∫ Y ϕ d f (x) is µ-integrable and ∫ Y ϕ dν = ∫ X ϕ • f dµ
The symmetric monoidal structure of Krn is defined on a pair of objects (X , µ), (Y , ν ) by the Cartesian product and the product of measure, i.e.

(X , µ) ⊗ (Y , ν ) = (X ×Y , µ ⊗ν ). On pairs of morphisms f : (X , µ) (Y , ν ) and f ′ : (X ′ , µ ′ ) (Y ′ , ν ′ ) it is defined by (f ⊗ f ′ )(x, x ′ ) := f (x) ⊗ f ′ (x ′ ).
The unitors, associator and braiding transformations are given by the obvious bijections.

The dagger structure of Krn

Krn has an extremely powerful inversion principle: Theorem 7 (Measure Disintegration Theorem, [START_REF] Kechris | Classical descriptive set theory[END_REF], 17.35). Let f : (X , µ) (Y , ν) be a deterministic Krn-morphism, there exists a unique morphism

f † µ : (Y , ν ) (X , µ) such that f • f † µ = id (Y ,ν ) . (1)
The kernel f † µ is called the disintegration of µ along f . As our notation suggests, the disintegration depends fundamentally on the measure µ over the domain, however we will omit this subscript when there is no ambiguity. The following lemma relates disintegrations to conditional expectations. Lemma 8 ([8]). Let f : (X , µ) → (Y , ν ) be a deterministic Krn-morphism, and let ϕ : X → R be measurable, then µ-a.e.

ϕ • f † • f = E [ϕ | σ (f )]
We can extend the definition of (-) † to any Krn-morphism f : (X , µ) (Y , ν) in a functorial way, although f † will not in general be a right inverse to f . The construction of f † is detailed in [START_REF] Clerc | Pointless learning[END_REF], but let us briefly recall how it works. The category SB has products which are built in the same way as in Meas via the product of σ -algebras 3 . Given any kernel f : (X , µ) (Y , ν ), we can canonically construct a probability measure γ f on the product X × Y of SB-space by defining it on the rectangles of X × Y as

γ f (A × B) = ∫ x ∈X 1 A (x) • f (x)(B) dµ.
(2)

Equivalently, γ f = (δ X ⊗ f ) • ∆ X • µ, where ∆ X : X → X × X is the diagonal map. Letting π X : X × Y → X and π Y : X × Y → Y be the canonical projections, we observe that Gπ X (γ f ) = µ and Gπ Y (γ f ) = ν : in other words, γ f is a coupling of µ and ν . The disintegration of γ f along π Y is a kernel π † Y : (Y , ν) → (X × Y , γ f ).
Finally we define:

f † = π X • π † Y . (3)
The following Krn diagram sums up the situation:

(X , µ) π † X $ , f ) (X × Y , γ f ) π Y $ , π X d l (Y , ν ) π † Y e l f † ì where π † X is explicitly given by (δ X ⊗ f ) • ∆ X .
The following property characterizes the action of (-) † on Krn-morphisms:

Theorem 9. For all f : (X , µ) (Y , ν ), f † : (Y , ν ) (X , µ)
is the unique Krn morphism satisfying for all measurable sets A ⊆ X , B ⊆ Y the following equation:

∫ x ∈X 1 A (x) • f (x)(B) dµ = ∫ y ∈Y f † (y)(A) • 1 B (y) dν (4)
In view of Eq. ( 4), we will call f † the Bayesian inversion of f , and refer to (-) † as the Bayesian inversion operation on Krn. It will be crucial throughout the rest of this paper. It is important to see that f † absolutely depends on the choice of µ and not only on f seen as a function. We can now improve on [START_REF] Clerc | Pointless learning[END_REF] and show that (-) † is indeed a †-operation in the strict categorical meaning of the term.

Theorem 10. Krn is a dagger symmetric monoidal category, with (-) † given by Bayesian inversion.

Banach lattices

It is well-known that kernels can alternatively be seen as predicate -i.e. real-valued function -transformers, or as state -i.e. probability measure -transformers. The latter perspective was adopted by Kozen in [START_REF] Kozen | Semantics of probabilistic programs[END_REF] to describe the denotational semantics of probabilistic programs (without conditioning). We shall see in this section and the next, that the predicate and state transformer perspectives are dual to one another in the category of Banach lattices, a framework incidentally also used in [START_REF] Kozen | Semantics of probabilistic programs[END_REF]. For an introduction to the theory of Banach lattices we refer the reader to e.g. [START_REF] Aliprantis | [END_REF][START_REF] Zaanen | Introduction to operator theory in Riesz spaces[END_REF].

An ordered real vector space V is a real vector space together with a partial order ≤ which is compatible with the linear structure in the sense that for all u, v, w ∈ V , λ ∈ R + u ≤ v ⇒ u + w ≤v + w and u ≤ v ⇒ λu ≤ λv An ordered vector space (V , ≤) is called a Riesz space if the poset structure forms a lattice. A vector v in a Riesz space (V , ≤) is called positive if 0 ≤ v, and its absolute value |v | is defined as |v | = v ∨ (-v). A Riesz space (V , ≤) is σ -order complete if every non-empty countable subset of V which is order bounded has a supremum.

A normed Riesz space is a Riesz space (V , ≤) equipped with a lattice norm, i.e. a map ∥•∥ : V → R such that:

|v | ≤ |w | implies ∥v ∥ ≤ ∥w ∥ .

(5) A normed Riesz space is called a Banach lattice if it is (norm-) complete, i.e. if every Cauchy sequence (for the norm ∥•∥) has a limit in V .

Example 11. For each measured space (X , µ) -and in particular Krn-objects -and each 1 ≤ p ≤ ∞, the space L p (X , µ) is a Riesz space with the pointwise order. When it is equipped with the usual L p -norm, it is a Banach lattice. This fact is often referred to as the Riesz-Fischer theorem (see [START_REF] Aliprantis | [END_REF]Th 13.5]). We will say that p, q ∈ N ∪ {∞} are Hölder conjugate if either of the following conditions hold: (i) 1 < p, q < ∞ and 1 p + 1 q = 1, or (ii) p = 1 and q = ∞, or (iii) p = ∞ and q = 1.

Theorem 12 (Lemma 16.1 and Theorem 16.2 of [START_REF] Zaanen | Introduction to operator theory in Riesz spaces[END_REF]). Every Banach lattice is σ -order complete.

There are two very natural modes of 'convergence' in a Banach lattice: order convergence and norm convergence. The latter is well-known, the former less so. An order bounded sequence {v n } n ∈N in a σ -complete Riesz space (and thus in a Banach lattice) converges in order to v if either of the following equivalent conditions holds:

v = lim inf n v n := n n ≤m v m , v = lim sup n v n := n n ≤m v m .
For a monotone increasing sequence v n , this definition simplifies to v = n v n , which is often written v n ↑ v.

In a general σ -complete Riesz space, order and norm convergence are disjoint concepts, i.e. neither implies the other (see [START_REF] Zaanen | Introduction to operator theory in Riesz spaces[END_REF]Ex. 15.2] for two counter-examples). However if a sequence converges both in order and in norm then the limits are the same (see [START_REF] Zaanen | Introduction to operator theory in Riesz spaces[END_REF]Th. 15.4]). Moreover, for monotone sequences norm convergence implies order convergence:

Proposition 13 ([27] Theorem 15.3). If {v n } n ∈N is an in- creasing sequence in a normed Riesz space and if v n converges to v in norm (notation v n → v), then v n ↑ v.
In a Banach lattice we have the following stronger property. Proposition 14 (Lemma 16.1 and Theorem 16.2 of [START_REF] Zaanen | Introduction to operator theory in Riesz spaces[END_REF]). If {v n } n ∈N is a sequence of positive vectors in a Banach lattice such that sup n ∥v n ∥ converges, then n v n exists and

∥ n v n ∥ = n ∥v n ∥.
It can also happen that order convergence implies norm convergence. A lattice norm on a Riesz space is called σorder continuous if v n ↓ 0 (v n is a decreasing sequence whose infimum is 0) implies ∥v n ∥ ↓ 0.

Example 15. For 1 ≤ p < ∞, the L p -norm is σ -order continuous, and thus order convergence and norm convergence coincide. However, for p = ∞ this is not the case as the following simple example shows. Consider the sequence of essentially bounded functions v n = 1 [n,+∞[ : it is decreasing for the order on L ∞ (R, λ) with the constant function 0 as its infimum, i.e. v n ↓ 0. However ∥v n ∥ = 1 for all n.

Many types of morphisms between Banach lattices are considered in the literature but most are at least linear and positive, that is to say they send positive vectors to positive vectors. From now on, we will assume that all morphisms are positive (linear) operators. Other than that, we will only mention two additional properties, corresponding to the two modes of convergence which we have examined. The first notion is very well-known: a linear operator T : V → W between normed vector spaces is called norm-bounded if there exists C ∈ R such that ∥Tv ∥ ≤ C ∥v ∥ for every v ∈ V . The following result is familiar: Theorem 16. An operator T : V → W between normed vector spaces is norm-bounded iff it is continuous.

Thus norm-bounded operators preserve norm-convergence. The corresponding order-convergence concept is defined as follows: an operator T : V → W between σ -order complete Riesz spaces is said to be σ -order continuous if whenever v n ↑ v, Tv = Tv n . It follows that we can consider two types of dual spaces on a Banach lattice V : on the one hand we can consider the norm-dual:

V * = { f : V → R | f is norm-continuous} and the σ -order-dual: V σ = { f : V → R | f is σ -order continuous}
The latter is sometimes known as the Köthe dual of V (see [START_REF] Dieudonné | Sur les espaces de Köthe[END_REF][START_REF] Zaanen | Introduction to operator theory in Riesz spaces[END_REF]). The two types of duals coincide for a large class of Banach spaces of interest to us.

Theorem 17. If a Banach lattice V admits a strictly positive linear functional and has a σ -order-continuous norm, then

V * = V σ .
Example 18. The result above can directly be applied to our running example: given a measured space (X , µ) and an integer 1 ≤ p < ∞, the Lebesgue integral provides a strictly positive functional on L p (X , µ), and we already know from Example 15 that L p (X , µ) has a σ -order-continuous norm. It follows that L p (X , µ) * = L p (X , µ) σ Moreover, it is well-known that if (p, q) are Hölder conjugate and 1 < p, q < ∞, then L p (X , µ) * = L q (X , µ), and thus

L p (X , µ) σ = L q (X , µ). It is also known that L 1 (X , µ) * = L ∞ (X , µ), and thus L 1 (X , µ) σ = L ∞ (X , µ).
However Theorem 17 does not hold for L ∞ (X , µ) since the L ∞ -norm is not σ -order continuous, as was shown in Example 15. It is well-known that L ∞ (X , µ) * L 1 (X , µ), and in fact L ∞ (X , µ) * can be concretely described as the Banach lattice ba(X , µ) of charges (i.e. finitely additive finite signed measures) which are absolutely continuous w.r.t, µ on X (see [START_REF] Dunford | Linear operators I[END_REF]IV.8.16]). However, as is shown in e.g. [START_REF] Chaput | Approximating Markov Processes by averaging[END_REF][START_REF] Zaanen | Introduction to operator theory in Riesz spaces[END_REF] L

∞ (X , µ) σ = L 1 (X , µ) (6)
As Examples 15 and 18 show, the (-) σ operation brings a lot of symmetry to the relationship between L p -spaces since L p (X , µ) σ = L q (X , µ) for any Hölder conjugate pair 1 ≤ p ≤ ∞. For this reason we will consider the category BL σ whose objects are Banach lattices and whose morphisms are σ -order continuous positive operators. Note that the Köthe dual of a Banach lattice is a Banach lattice, and it easily follows that (-) σ in fact defines a contravariant functor BL op σ → BL σ which acts on morphisms by pre-composition. As we will now see, BL σ is the category in which predicate and state transformers are most naturally defined.

From Borel kernels to Banach lattices

The functors S p and T p . For 1 ≤ p ≤ ∞, the operation which associates to a Krn-object (X , µ) the space L p (X , µ) can be thought of as either a contravariant or a covariant functor. We define the functors S p : Krn → BL op σ , 1 ≤ p ≤ ∞ as expected on objects, and on Krn-morphisms f : X Y via the well-known 'predicate transformer' perspective:

S p (f ) : L p (Y , ν ) → L p (X , µ), ϕ → λx . ∫ Y ϕ d f (x) = ϕ • f
For a proof that this defines a functor see [START_REF] Clerc | Pointless learning[END_REF]. We define the covariant functors

T p : Krn → BL σ , 1 ≤ p ≤ ∞ as T p = S p • (-) † . The functor M ≪• . An ideal of a Riesz space V is a sub- vector space U ⊆ V with the property that if |u | ≤ |v | and v ∈ U then u ∈ U . An ideal U is called a band when for every subset D ⊆ U if D exists in V , then it also belongs to U .
Every band in a Banach lattice is itself a Banach lattice. Of particular importance is the band B v generated by a singleton {v}, which can be described explicitly as

B v = {w ∈ V | (|w | ∧ n |v |) ↑ |w |} Example 19.
Let X be an SB-space and ca(X ) denote the set of measures of bounded variation on X . It can be shown ([2, Th 10.56]) that ca(X ) is a Banach lattice. The linear structure on ca(X ) is as expected, the Riesz space structure is given by

(µ ∨ ν )(A) = sup{µ(B) + ν (A \ B) | B measurable , B ⊆ A}
and the dual definition for the meet operation. The norm is given by the total variation i.e.

∥µ ∥ = sup n i |µ(A i )| {A 1 , . . . , A n } a meas. partition of X
Given µ ∈ ca(X ), the band B µ generated by µ is just the set of measures of bounded variation which are absolutely continuous w.r.t. µ. In particular B µ is a Banach lattice.

We can now define the functor M ≪• : Krn → BL σ by:

M ≪• (X , µ) := B µ M ≪• f : M ≪• (X , µ) → M ≪• (Y , ν ), ρ → f • ρ We will usually write M ≪• (X , µ) as M ≪µ (X ). Proposition 20. Let f : (X , µ)
(Y , ν ) be a Krn arrow. Let ρ be a finite measure on X such that ρ ≪ µ. Then f • ρ ≪ ν, and thus M ≪• defines a functor.

Radon-Nikodym is natural. We now present a first pair of natural transformations which will establish a natural isomorphism between the functors T 1 and M ≪• . First, we define the Radon-Nikodym transformation rn : M ≪• → T 1 at each Krn-object (X , µ) by the map rn (X, µ) : M ≪µ (X ) → L 1 (X , µ), rn (X, µ) (ρ) = dρ dµ where d ρ /d µ is of course the Radon-Nikodym derivative of ρ w.r.t. µ. The fact that this transformation defines a positive operator between Banach lattices is simply a restatement of the usual Radon-Nikodym theorem [13, III.10.7.], combined with the well-known linearity property of the Radon-Nikodym derivative. To see that it is also σ -order-continuous, consider a monotone sequence µ n ↑ µ converging in order to µ in M ≪ν (X ). This means that for any measurable set

A of X , lim n→∞ µ n (A) = µ(A). Since ( d µ n/d ν ) n ∈N is bounded in L 1 -norm the function д = n d µ n/d ν
exists and is simply the pointwise limit д(x) = lim n→∞ d µ n/d ν (x). It now follows from the monotone convergence theorem (MCT) that

∫ A дdν = ∫ A lim n→∞ dµ n dν dν = lim n→∞ ∫ A dµ n dν dν = lim n→∞ µ n (A) = µ(A)
in other words, д = d µ /dν and rn is well-defined. That rn is also natural has -to our knowledge -never been published.

Theorem 21. The Radon-Nikodym transformation is natural.

Secondly, we define the Measure Representation transformation mr :

T 1 → M ≪• at each Krn-object (X , µ) by the map mr (X, µ) : T 1 (X , µ) → M ≪• (X , µ) defined as mr (X, µ) (f )(B X ) = ∫ B X f dµ
This is a very well-known construction in measure theory, and the fact that mr (X, µ) is a σ -order continuous operator between Banach lattices is immediate from the linearity of integrals and the MCT.

Theorem 22. The Measure Representation transformation is natural.

Riesz representations are natural. We now present a second pair of natural transformations which will establish a natural isomorphism between (-) σ • S ∞ and M ≪• . First, we define the Riesz Representation transformation rr :

(-) σ • S ∞ → M ≪• at each Krn-object (X , µ) by the map rr (X, µ) : (-) σ • S ∞ (X , µ) → M ≪• (X , µ) defined as rr (X, µ) (F )(B X ) = F (1 B X )
This construction is key to a whole collection of results in functional analysis commonly known as Riesz Representation Theorems (see [START_REF] Aliprantis | [END_REF] Chapter 14 for an overview). One can readily check that the Riesz Representation transformation is well-defined: rr (X, µ) (F )(∅) = F (0) = 0 and the σ -additivity of rr (X, µ) (F ) follows from the σ -order-continuity of F . To see that rr (X, µ) (F ) ≪ µ, assume that µ(B X ) = 0, then clearly 1 B X = 0 µ-a.e., i.e. 1 B X = 0 in L ∞ (X , µ), and thus F (1 B X ) = 0.

Theorem 23. The Riesz Representation transformation is natural.

Finally, we define the Functional Representation transformation fr at each Krn-object (X , µ) by the map fr (X, µ) :

M ≪• (X , µ) → (-) σ • S ∞ (X , µ) by fr (X, µ) (µ)(ϕ) = ∫ X ϕdµ
This construction is also completely standard in measure theory, although it has never to our knowledge been seen as a natural transformation.

Theorem 24. The Functional Representation transformation is well-defined, i.e. fr (X, µ) is a σ -order continuous positive operator, and is natural.

Natural Isomorphisms

We have now defined the following four natural transformations:

T 1 mr + 3 M ≪• rn k s fr + 3 (S ∞ ) σ rr k s
In fact, both pairs form natural isomorphisms, and these can be restricted to arbitrary Hölder conjugate pairs (p, q). Theorem 25. rn and mr are inverse of one another, in particular there exists a natural isomorphism between M ≪µ (X ) and L 1 (X , µ).

Theorem 26. rr and fr are inverse of each other, in particular there exists a natural isomorphism between M ≪µ (X ) and (L ∞ (X , µ)) σ .

We can now conclude that the isomorphism proved in Theorem 6 of [START_REF] Clerc | Pointless learning[END_REF] is in fact natural.

Corollary 27. There exists a natural isomorphism between

T 1 := S 1 • (-) † and (-) σ • S ∞ .
We can in fact restrict this result to any Hölder conjugate pair (p, q): Theorem 28. For 1 ≤ p ≤ ∞ with Hölder conjugate q, the natural transformation rn • rr restricts to a natural transformation (-

) σ • S q → T p .
The correspondence between the various categories and functors discussed in this section are summarized as follows:

BL σ BL op σ (-) σ = = rr + 3 rn + 3 fr k s Krn op S 1 a a mr k s Krn (-) † < < S ∞ a a M ≪• O O (7)

Approximations

In this section we develop a scheme for approximating kernels which follows naturally from the †-structure of Krn. Consider f : (X , µ) (Y , ν ) and a pair of deterministic maps p : (X , µ) → (X ′ , p * µ) and q : (Y , ν ) → (Y ′ , q * ν ) (typically these maps coarsen the spaces X and Y ).

(X , µ) f , 2 f p,q , 2 p s (Y , ν ) q s (X ′ , p * µ) , 2 p † µ s U ^fp,q , 2 (Y ′ , q * ν ) q † ν s U ^(8)
The †-structure of Krn allows us to define the new kernels

f p,q := q † ν • q • f • p † µ • p : X Y (9)
f p,q := q • f • p † µ : X ′ Y ′ (10)
The supscript notation is meant to indicate that the approximation lives 'upstairs' in Diagram [START_REF] Dahlqvist | Bayesian Inversion by Omega-Complete Cone Duality[END_REF] and conversely for the subscripts. Intuitively, f p,q and f p,q take the average of f over the fibres given by p, q according to µ and ν (see Section 7 for concrete calculations). The advantage of ( 10) is that we can approximate a kernel on a huge space by a kernel on a, say, finite one. The advantage of ( 9) is that although it is more complicated, it is morally equivalent and has the same type as f , which means that we can compare it to f .

A very simple consequence of our definition is that Bayesian inversion commutes with approximations. We shall use this in §7.1 to perform approximate Bayesian inference.

Theorem 29. Let f : (X , µ) (Y , ν ), let p : X → X ′ and q : Y → Y ′ n be a pair of deterministic maps, then (f † ) q,p = (f p,q ) † and (f † ) q,p = (f p,q ) †

In practice we will often consider endo-kernels f : X X with a single coarsening map p : X → X ′ to a finite space. In this case (9) simplifies greatly.

Proposition 30. Under the situation described above

f p := p † ν • p • f • p † µ • p = f • p † µ • p (11)
In the case covered by Proposition 30, the interpretation of f p is very natural: for each x ∈ X the measure f (x) is approximated by its average over the fibre to which x belongs, conditioned on being in the fibre. For fibres with strictly positive µ-probability, this is simply 11) also covers the case of µ-null fibres. Note also that in the case where f p = f , the map p corresponds to what is known as a strong functional bisimulation for f .

f p (x)(A) = ∫ y ∈p -1 (p(x )) f (y)(A) dµ µ(p -1 (p(x)) However (
Approximating is non-expansive. It is well-known that conditional expectations are non-expansive and we know from Lemma 8 that pre-composing by p † µ •p as in ( 11) amounts to conditioning. The following lemma is an easy consequence.

Lemma 31. Let f : (X , µ) (Y , ν ) and q : X → X ′ be a deterministic quotient, then for all 1 ≤ p ≤ ∞ and ϕ ∈ L p (Y , ν)

S p f q (ϕ) p ≤ S p f (ϕ) p
Compositionality of approximations In the case where we wish to approximate a composite kernel д • f , it might be convenient, for modularity reasons, to approximate f and д separately. This does not entail any loss of information provided the quotient maps are hemi-bisimulations, in the following sense. Let p : X → X ′ , q : Y → Y ′ , r : Z → Z ′ be deterministic quotients and let f :

(X , µ) (Y , ν ), д : (Y , ν )
(Z , ρ) be composable kernels. We say that q is a left hemi-bisimulation for f if f = q † • q • f , and conversely that it is a right hemi-bisimulation for д if д = д • q † • q holds. In either case, one can verify using Theorems 7 and 29 that approximation commutes with composition, i.e. that (д • f ) p,r = д q,r • f p,q .

Discretization schemes We will use [START_REF] Desharnais | Metrics for labelled Markov processes[END_REF] and [START_REF] Desharnais | Approximating labeled Markov processes[END_REF] to build sequences of arbitrarily good approximations of kernels. For this we introduce the following terminology.

Definition 32. We define a discretization scheme for an SBspace X to be a countable co-directed diagram (ccd) of finite spaces for which X is a cone (not necessarily a limit).

If (X i ) i ∈I is a discretization scheme of X and p i : X → X i are the maps making X a cone, then it follows from the definition that if i < j, σ (p i ) ⊆ σ (p j ) where σ (p i ) is the σ -algebra generated by p i . For each i ∈ I the finite quotient p i defines a measurable partition of X whose disjoint components p -1 i ({k}), k ∈ X i we will call cells.

By Theorem 1 every SB-space has a discretization scheme for which it is not just a cone but a limit.

In practice we will work with discretization schemes linearly ordered by N. In this case the sequence (X , σ (p n )) n ∈N defines what probabilists call a filtration and we will denote the approximation f p n given by [START_REF] Desharnais | Approximating labeled Markov processes[END_REF] simply by f n .

Convergence

We now turn to the question of convergence of approximations. There appears to be little literature on the subject of the convergence of approximations of Markov kernels. One rare reference is [START_REF] Choo-Whan | Approximation theorems for Markov operators[END_REF]. Via the functor S p defined above in Sections 3 and 4 we can seek a topology in terms of the operators associated to a sequence of kernels. Indeed, following [START_REF] Choo-Whan | Approximation theorems for Markov operators[END_REF], we will prove convergence results for the Strong Operator Topology (SOT).

Definition 33. We will say that a sequence of kernels f n : X Y converges to f : X Y in strong operator topology, and write

f n -→ s f , if S 1 f n converges to S 1 f in the strong operator topology, i.e. if lim n→∞ ∥S 1 f n (ϕ) -S 1 f (ϕ)∥ 1 = 0
Proving convergence. We start with the following key lemma which is a consequence of Lévy's upward convergence Theorem ([25, Th. 14.2]) .

Lemma 34. Let f : (X , µ) (Y , ν ) be a Krn-morphism and let p n : X → X n , n ∈ N be a discretization scheme such that for B X the Borel σ -algebra of X we have

B X = σ n σ (p n )
and let A ⊆ Y be measurable, then for

f n := f • p † n • p n lim n→∞ f n (x)(A) = f (x)(A) for µ-almost every x ∈ X . Moreover, lim n→∞ ∥S 1 f n (1 A ) -S 1 f (1 A )∥ 1 = 0
Theorem 35 (Convergence of Approximations Theorem).

Under the conditions of Lemma 34, for µ-almost every x ∈ X lim

n→∞ f n (x)(A) = f (x)(A)
for all Borel subsets A. Moreover,

lim n→∞ ∥S 1 f n (ϕ) -S 1 f (ϕ)∥ 1 = 0 for any ϕ ∈ L 1 (X , ν ). In other words f n -→ s f .
Note that operators of the shape S p f n obtained from a discretization scheme are finite rank operators. Thus, we, in fact, also obtained a theorem to approximate stochastic operators by stochastic operators of finite rank for the SOT topology. In general, we cannot hope for convergence in the stronger norm topology since the identity operator -which is stochastic -is a limit of operators of finite rank in the norm topology iff the space is finite dimensional.

Note also that the various relationships established in Section 4 allow us to move from an approximation of a kernel to an approximation of the corresponding Markov operator. Since a discretization scheme making f n -→ s f will also make (f † ) n -→ s f † , it follows from Theorem 25 that we get a finite rank approximation of the Markov operator M ≪• (f ).

Applications

Approximate Bayesian Inference

Consider again the inference problem from the introduction. There one needed to invert f (x) = N (x, 1) with prior µ = N (0, 1). We can use Theorem 29 to see how our approximate Bayesian inverse compares to the exact solution which in this simple case is known to be f † µ (0.5) = N (1/4, 1/2). To do this, we use a doubly indexed discretization scheme: q mn : R → 2 × m × n + 2 defining a window of width 2m centred at 0 divided in 2mn equal intervals; with the remaining intervals (-∞, -m] and (m, ∞) each sent to a point (hence the +2 above). Since all classes induced by q mn have positive µ-mass, approximants can be computed simply as:

f m,n ([k])([l]) = µ[k] -1 ∫ x ∈[k ] N (x, 1)([l]) dµ
where [k], [l] range over classes of q mn . The corresponding stochastic matrices are shown in Fig. 2 and 3 for m, n = 5, 3 and 6, 10 respectively.

Since these approximants are finite, their Bayesian inverse can be computed directly by Bayes theorem (i.e. taking the adjoint of the stochastic matrices):

f m,n † ([l])([k]) = µ[k] • f m,n ([k])([l]) ν [l] (12)
with ν = f * (µ). Commutation of inversion and approximation guarantees that the f m,n † converge to f † . Indeed, Fig. 1 shows the the Lebesgue density of f m,n † (0.5) for m, n = 3, 2 (in dashed blue) and 7, 5 (dashed red). The latter approximant is already hardly distinguishable from the exact solution (solid black).

It must be emphasized that this example is meant only as an illustration and does not constitute a universal solution to the irreducibly hard (not even computable in general [START_REF] Ackerman | Noncomputable Conditional Distributions[END_REF]) problem of performing Bayesian inversion. Also, not all quotients are equally convenient: what makes the approach computationally tractable is that the fibres are easily described and the measure conveniently evaluated on such fibres.

Approximating the Kleene star of ProbNetKAT

ProbNetKAT ( [START_REF] Foster | Probabilistic netkat[END_REF][START_REF] Smolka | Cantor meets Scott: Domain-theoretic foundations for probabilistic network programming[END_REF]) is a probabilistic network specification language extending Kleene Algebras with Tests ( [START_REF] Kozen | Kleene algebra with tests[END_REF]) with network primitives and a binary probabilistic choice operator ⊕ λ , λ ∈ [0, 1]. For the purpose of the example shown here we will not need to introduce the full syntax and semantics of ProbNetKAT, rather we will focus on a single ProbNetKAT program which we will call cantor and is given by: cantor := p; (dup; p) * where p := π 0 ! ⊕1 /2 π 1 ! (13) The program acts on sets of finite sequences of 0 and 1, which can be thought of as packet histories. We will write H for the set {0, 1} * of all packet histories and H n for the set of histories of length as most n. A ProbNetKAT program is always interpreted as a kernel 2 H → G2 H . Programs with both dup and * revealed to be quite complex from the earliest development of the language. As we will describe, cantor denotes a continuous distribution and hence having a way to approximate it is crucial for practical uses of the language. The denotation of π 0 ! on a single sequence {(a 0 , . . . , a n )} is: π 0 ! ({(a 0 , . . . , a n )}) = δ {(0,a 1 , ...,a n )} in other words π 0 ! overwrites the first entry in the sequence with 0. Similarly, π 1 ! overwrites the first entry with 1. This semantics is extended to sets of sequences in the obvious way by taking direct images. The semantics of p is thus: p (a) = 0.5δ π 0 ! (a) + 0.5δ π 1 ! (a) The denotation of dup is given on singleton histories by dup ({(a 0 , . . . , a n )}) = δ {(a 0 ,a 0 , ...,a n )} i.e. dup shifts the history to the right and duplicates the first entry. Again, this is extended to sets of histories by taking direct images. The sequential composition operator ; is interpreted by Kleisli composition.

The interpretation of the Kleene star is more involved, and we here describe it categorically. To avoid any confusion we will not use Kleisli arrows in this construction, i.e. all kernels will be explicitly typed as kernels. Note first that the infinite product (2 H ) ω can be defined as the limit of the ccd given by the maps q n+1,n : (2 H ) n+1 → (2 H ) n dropping the last component. By Bochner's theorem ( [START_REF] Dahlqvist | Giry and the Machine[END_REF]) this also holds of G((2 H ) ω ). Next, consider any program r. We turn 2 H into a cone for the diagram with limit G((2 H ) ω ) via the inductively defined maps:

a 1 = η ⊗ r • ∆ 1 : 2 H → G(2 H × 2 H ) (14)
a n = a n-1 ⊗ r • ∆ n : (2 H ) n → G((2 H ) n × 2 H ) (15) where ∆ n : (2 H ) n → (2 H ) n × 2 H is the map copying the last entry. It is easy to check q n+1,n • a n • a n-1 • . . . • a 1 = a n-1 • . . . • a 1 ,
n := a n • . . . • a 1 : 2 H → G(2 H ) n makes 2 H a cone for lim ← -- G(2 H ) n .
There must therefore exist a unique morphism

r ∞ : 2 H → G (2 H ) ∞ .
For each input, this kernel builds a distribution on the sample paths of the discrete-time stochastic processes associated with r and this input. We now define

r * := G • r ∞ where : (2 H ) ∞ → 2 H
is the map taking infinitary unions. Since the definition above makes sense for any kernel f on 2 H , we will overload the Kleene star and put

f * := G •f ∞ .
Given the input (0), a sample path of cantor will draw uniformly a history of size 1, then a history of size 2 whose suffix matches the size 1 history drawn at the previous step, and so on for every integer. The distribution cantor (0) associates to a measurable collection of sets of histories A the probability that the union of a sample path from (0) belongs to A. For example cantor (0){A | (01) ∈ A} = 1 /4, since there's a 1 /4 chance that a sample path will have drawn (01) amongst the histories of size 2. We start by turning 2 H into a Krn-object. Consider the countable directed diagram given by all injections i mn :

H m → H n , n > m, then H = lim --→
H n , and it follows that 2 H = lim ← --2 H n since 2 -turns colimits into limits. We know from Bochner's theorem that G2 H = lim ← --G2 H n , and we use this fact to place a canonical measure on 2 H as follows: since each 2 H n is finite with cardinality c n := 2 n i 2 i = 2 2 n+1 -1 , and can thus be equipped with the uniform measure 1 /c n , we can find a limit measure µ on 2 H with the pleasing property that for all history truncating maps p n : 2 H → 2 H n , the pushforward µ n := (p n ) * µ is the uniform measure on H n . It is clear that these maps define a discretization scheme on 2 H which satisfies the condition of Theorem 35. We will now show that if f n -→ s f , then (f n ) * -→ s f * . To prove this we need the following lemma which is interesting in its own right.

Lemma 36. The monoidal structure of Krn is continuous for the SOT, i.e. f n -→ s f and д n -→ s д implies f n ⊗ д n -→ s f ⊗ д.

Theorem 37. Under the set-up described above, for any kernel f :

(2 H , µ) (2 H , ν ) we have (f n ) * -→ s f *
The advantage of working over finite spaces is that (f n ) * can, in principle at least, be computed for kernels defined in ProbNetKAT. Let us examine this in the case of cantor and of the discretization scheme p n : 2 H → 2 H n .

In the case n = 3 the underlying Markov chain has 2 7 states, but has an interesting property which means we need not consider them all: when we compute p ; (dup; p) 3 ∞ , the process necessarily lands in an ergodic component of the chain consisting of the singletons of histories of length exactly 3. The reason is that once the process reaches histories of length 3 it starts randomly re-writing the histories, and with probability 1 any two histories will eventually get re-written to the same thing. Once a set of histories has decreased in cardinality by one, it can never go back, thus eventually any set of histories gets re-written to a single length 3 history, and then loops among length 3 singletons indefinitely. The situation is represented from the initial state (0) in Figure 4 where, for clarity's sake, the ergodic component is symbolized by common double-sided arrows to a new state.

Conclusion

We have presented a framework for the exact and approximate semantics of first-order probabilistic programming. The semantics can be read off either in terms of kernels between measured spaces, or in terms of operators between L p spaces. Either forms come with related involutive structures: Bayesian inversion for (measured) kernels between Standard Borel spaces, and Köthe duality for positive linear and σcontinuous operators between Banach lattices. Functorial relations between both forms can themselves be related by way of natural isomorphisms. Our main result is the convergence of general systems of finite approximants in terms of the strong operator topology (the SOT theorem). Thus, in principle, one can compute arbitrarily good approximations of the semantics of a probabilistic program of interest for any given (measurable) query. Future work may allow one to derive stronger notions of convergences given additional Lipschitz control on kernels, or to develop approximation schemes that are adapted to the measured kernel of interest.

More ambitiously perhaps, one could investigate whether MCMC sampling schemes commonly used to perform approximate Bayesian inference in the context of probabilistic programming could be seen as randomized approximations of the type considered in this paper.

A Appendix

Proof of Theorem 1. This is a consequence of the Isomorphism Theorem (Theorem 15.6 of [START_REF] Kechris | Classical descriptive set theory[END_REF]): two SB spaces are isomorphic iff they have the same cardinality. Uncountable SB spaces are thus all isomorphic to the Cantor space 2 N which is the limit of the countable co-directed diagram (2 n ) n ∈N with the connecting morphisms p n+1,n : 2 n+1 → 2 n truncating binary words of length n + 1 at length n. Similarly all SB-spaces of cardinality ℵ 0 are isomorphic to the one-point compactification of N, which is the limit of the countable co-directed diagram (n) n ∈N with the connecting morphisms p n+1,n : n + 1 → n, i → min(i, n). The case of finite SB spaces is trivial.

■

Proof of Lemma 3. By Dinkyn's π -λ theorem, two finite measures are equal if and only if they agree on a π -system generating the σalgebra. Any standard Borel space admits such a countable πsystem (any countable basis for a Polish topology generating the σ -algebra). Let {B n } n ∈N be such a π -system. Then, for all

x ∈ X , д(x) д ′ (x) ⇔ ∃n.д(x)(B n ) д ′ (x)(B n ). Hence, N (д, д ′ ) = ∪ n {x ∈ X | д(x)(B n ) д ′ (x)(B n )} = ∪ n {x ∈ X | ev B n (д(x)) ev B n (д ′ (x))} = ∪ n (ev B n • д -ev B n • д ′ ) -1 (R \ {0}) By definition of the measurable structure of G(Y ), ev B n • д - ev B n • д ′ is measurable, hence N (д, д ′ ) is also measurable. ■ Proof of Proposition 4. We first show that if д ∼ д ′ , then h • д ∼ h • д ′ .
Clearly, for any space V and any deterministic function u :

Y → V , N (u •д, u •д ′ ) ⊆ N (д, д ′ ). By definition of the Kleisli category, h • д = m Z • G(h) • д and similarly for h • д ′ . Taking u = m Z • G(h), we obtain that µ(N (h • д, h • д ′ )) ≤ µ(N (д, д ′ )). It is now enough to show that λ(N (д • f , д ′ • f )) = 0. Let us reason contrapositively. We have: λ(N (д • f , д ′ • f )) > 0 ⇔ ∫ w ∈W 1 N (д•f ,д ′ •f ) (w) dλ > 0 → ∫ w ∈W n ∈N 1 (д•f )(w )(B n ) (д ′ •f )(w )(B n ) dλ > 0 ∃n → ∫ w ∈W 1 (д•f )(w )(B n ) (д ′ •f )(w )(B n ) dλ > 0 → ∫ w ∈W |(д • f )(w)(B n ) -(д ′ • f )(w)(B n )| dλ > 0 ⇔ ∫ w ∈W ∫ x ∈X |д(x)(B n ) -д ′ (x)(B n )| d f (w) dλ > 0 ⇔ ∫ x ∈X |д(x)(B n ) -д ′ (x)(B n )| dµ > 0 ∃X + ⊆X → ∫ x ∈X + д(x)(B n ) -д ′ (x)(B n ) dµ > 0 → ∫ x ∈X + 1 д(-)(B n )>д ′ (-)(B n ) (x) dµ > 0 → ∫ x ∈X + 1 N (д,д ′ ) (x) dµ > 0 The last line implies µ(N (д, д ′ )) > 0, a contradiction. ■ Proof of Theorem 6.
If ϕ is ν -integrable, there exists a monotone sequence {ϕ n } of simple functions such that ϕ n ↑ ϕ and

∫ Y ϕ n dν → ∫ Y ϕdν < ∞. By definition each ϕ n = k i=0 α i 1 B i ,

and by unravelling the definition we have

∫ Y 1 B i dν = ν (B i ) = ∫ X f (x)(B i )dµ = ∫ X ∫ Y 1 B i d f (x)dµ = ∫ X (1 B i • f )dµ From which it follows that ∫ Y ϕ n dν = ∫ X ∫ Y k i=0 α i 1 B i d f (x)dµ = ∫ X (ϕ n • f )dµ
and the result follows from the Monotone Convergence Theorem (MCT).

■

Proof of Theorem 9.

It follows by definition of f † and from the disintegration theorem that

∫ y ∈Y f † (y)(A) • 1 B (y) dν = γ f (A × B), (16)
from which Eq. 4 follows easily. It remains to prove that this uniquely characterizes f † . Let us reason contrapositively. Assume there exists д :

(Y , ν ) (X , µ) verifying for all A, B measurable ∫ y ∈Y д(y)(A) • 1 B (y) = γ f (A × B)
as in Eq. 16 and such that ν (N (f † , д)) > 0 (assuming we take some representative of f † ). Let {A n } n ∈N be a countable π -system generating the σ -algebra of X . It is enough to test equality of measures on X on this π -system. Therefore,

N (f † , д) = ∪ n {y | f † (y)(A n ) д(y)(A n )}. Since ν(N (f † , д)) > 0, there must exist a k ∈ N such that ν ({y | f † (y)(A k ) д(y)(A k )}) > 0. Therefore, N + k = {y | f † (y)(A k ) > д(y)(A k )} must also have positive measure for ν . But then, ∫ y ∈Y д(y)(A k ) • 1 N + k (y) γ f (A k × N + k ), a contradiction.

■

Proof of Theorem 10.

Let us first show that (-) † is a functor Krn → Krn op , i.e. that id † (X, µ) = id (X, µ) and that for any f :

(X , µ) (Y , ν ) and д : (Y , ν ) (Z , ρ) we have (д • f ) † = f † • д † . Let (X , µ
) be an object of Krn and id X, µ the corresponding identity. By Th. 9, it is enough to prove, for all A, A ′ measurable subsets of X , that

∫ x ∈X 1 A (x) • id X, µ (x)(A ′ ) dµ = ∫ x ∈X id X, µ (x)(A) • 1 A ′ (x) dµ.
We have:

∫ x ∈X 1 A (x)•id X, µ (x)(A ′ ) dµ = ∫ x ∈X 1 A (x)•1 A ′ dµ = µ(A∩A ′ )
The same calculation on the right hand side of the first equation yields trivially the same result. Hence the equality is verified. Now, on to compatibility w.r.t. composition. In sight of Th. 9, it is enough to show that for all

A ⊆ X , C ⊆ Z , ∫ x ∈X (д • f )(x)(C) • 1 A (x) dµ = ∫ z ∈Z 1 C (z) • (f † •д † )(z)(A) dρ
In the following, for X a measurable space, we denote by SF (X ) the set of simple functions over X (finite linear combinations of indicator functions of measurable sets). We will use repeatedly the monotone convergence theorem (MCT). The left hand side of the above equation can be re-written as: 2) is by Th. 9 and

∫ x ∈X ∫ y ∈Y д(y)(C) d f (x) • 1 A (x) dµ (1) = ∫ x ∈X ∫ y ∈Y lim n→∞ д n (y) d f (x) • 1 A (x) dµ (2) = ∫ x ∈X lim n→∞ ∫ y ∈Y д n (y) d f (x) • 1 A (x) dµ where (1) is because д n ↑ д(-)(C), д n ∈ SF (Y ) and (2) by monotone convergence. Note that the n-indexed family x → ∫ y ∈Y д n (y) d f (x) is pointwise increasing. Therefore, ( * ) lim n→∞ ∫ x ∈X ∫ y ∈Y д n (y) d f (x) • 1 A (x) dµ (1) = lim n→∞ ∫ x ∈X k n i=1 α n i f (x)(C n i ) • 1 A (x) dµ = lim n→∞ k n i=1 α n i ∫ x ∈X f (x)(C n i ) • 1 A (x) dµ (2) = lim n→∞ k n i=1 α n i ∫ y ∈Y 1 C n i (y) • f † (y)(A) dν ( * ) = ∫ y ∈Y д(y)(C) • f † (y)(A) dν (3) = ∫ y ∈Y д(y)(C) • lim n f n (y) dν ( * ) = lim n k n i=1 β n i ∫ y ∈Y д(y)(C) • 1 D n i (y) dν (2) = lim n k n i=1 β n i ∫ z ∈Z 1 C (z) • д † (z)(D n i ) dρ = lim n ∫ z ∈Z 1 C (z) • ∫ y ∈Y k n i=1 β n i 1 D n i (y) dд † (z) dρ ( * ) = ∫ z ∈Z 1 C (z) • ∫ y ∈Y f † (y)(C) dд † (z) dρ = ∫ z ∈Z 1 C (z) • (f † • д † )(z)(A) dρ where ( * ) is by monotone convergence, (1) is because д n ∈ SF (Y ), (
(3) is because f n ↑ f † (-)(A), f n ∈ SF (Y ).
We have proved the sought identity.

Finally let us show that (-) † is involutive, i.e. that for any f : (X , µ) (Y , ν ), (f † ) † = f . This follows easily by two applications of Th. 9): we have

∫ x ∈X 1 A (x) • (f † ) † (x)(B) dµ = ∫ y ∈Y f † (y)(A) • 1 B (y) dν = ∫ x ∈X 1 A (x) • f (x)(B) dµ; and since adjoints are unique, f = (f † ) † .
The fact that (f ⊗ д) † = f † ⊗ д † follows immediately from the definitions and the property of disintegrations given by Th. 9. The fact that the associator, unitors and braiding transformations are unitary follows immediately from the fact that they are deterministic isomorphisms and Th. 7.

■

Proof of Proposition 20. Let B ⊆ Y be a measurable set. By definition, we have

(f • ρ)(B) = ∫ X ev B • f dρ where we recall that ev B : G(X ) → R + is the evaluation morphism. Let { f B n } n ∈N be an increasing chain of simple functions converging pointwise to ev B • f such that for each n, f B n = k n i=1 α n i 1 A n i with α n i ≥ 0. By the MCT, (f • ρ)(B) = lim n ∫ X f B n dρ = lim n k n i=1 α n i ρ(A n i ).
Similarly,

ν (B) = (f • µ)(B) = lim n ∫ X f B n dµ = lim n k n i=1 α n i µ(A n i ).
Notice that since the integral is linear and the sequence { f B n } n is increasing, the sequences { ∫ X f B n dρ} n and { ∫ X f B n dµ} n are also increasing. Assume ν (B) = 0. Then for all n, ∫ X f B n dµ = 0. We deduce that for all n, for all 1 ≤ i ≤ k n , either α n i = 0 or µ(A n i ) = 0. Using that ρ ≪ µ, we deduce that for all 1 ≤ i ≤ k n , either α n i = 0 or ρ(A n i ) = 0, from which we conclude that for all n, ∫ X f B n dρ = 0 and finally, (f • ρ)(B) = 0. Hence, f • ρ ≪ ν .

■

Proof of Theorem 21. We start by proving the following Lemma Lemma 38. For any f :

(X , µ) (Y , ν ), ϕ ∈ L 1 (Y , ν ), and B X ⊆ X measurable ∫ B X ∫ Y ϕd f (x) dµ = ∫ Y ϕ(y)f † (y)(B X ) dν
Proof. We start by showing the equation on characteristic functions.

If B Y is measurable in Y , we have ∫ B X ∫ Y 1 B Y d f (x) dµ = ∫ B X f (x)(B Y ) dµ = ∫ Y 1 B Y (y)f † (y)(B X ) dν Eq. ( 4
)
Since ϕ is measurable and integrable, there exists a sequence ϕ n ↑ ϕ of simple functions such that lim n ∫ Y ϕ n dν < ∞, and the results follows by the linearity of integration and the MCT.

□

We can now prove the naturality of rn. Let f : (X , µ) (Y , ν ) be a morphism in Krn; we have on the one hand

rn (Y , µ) • M ≪• (f )(ρ)(y) = rn (Y,ν ) ( ∫ X f (x)(-) dρ)(y) = d ∫ X f (x)(-)dρ dν (y) ( * )
and on the other

T 1 (f † ) • rn (X, µ) (ρ)(y) = T p (f † ) dρ dµ (y) = ∫ X dρ dµ d f † (y) ( * * )
To show the equality of these two maps in L 1 (Y , ν) it is enough to show that they are equal ν-a.e. To see this, we show that ( * * ) satisfies the condition to be the Radon-Nikodym derivative ( * ). Let B Y be a measurable subset of Y . We have from the well-known property of Radon-Nikodym derivatives:

∫ B Y d ∫ X f (x)(-) dρ dν dν = ∫ x ∈X f (x)(B Y ) dρ Moreover, we have ∫ B Y ∫ X dρ dµ d f † (y) dν (1) = ∫ x ∈X dρ dµ (x)f (x)(B Y ) dµ (2) = ∫ x ∈X f (x)(B) dρ
where (1) is by Lemma 38 and (2) is a well-known property of Radon-Nikodym derivatives.

have

M ≪• f • rr (X, µ) (F )(B Y ) = ∫ X f (x)(B Y ) d(rr (X, µ) (F )) = F (f (•)(B Y )) Lemma 40 = F ( ∫ X 1 B Y d f (•)) = F (1 B Y • f ) = rr (Y ,ν ) (F (-• f ))(B Y ) = rr (Y ,ν ) • (T 1 f ) σ (F )(B Y ) ■ Proof of Theorem 24.
We start by showing that fr is well defined. The linearity of fr (X, µ) is easily checked on simple functions and extended by the CMT. Positivity is also immediate. For the σ -order continuity, let µ m ↑ µ, ϕ ∈ L ∞ (X , µ), and ϕ n ↑ ϕ be a monotone approximation of ϕ by simple functions. We need to show that

lim m→∞ ∫ X ϕ dµ m = ∫ X ϕ dµ
For note first that the doubly indexed series ∫ X ϕ n dµ m is monotonically increasing in m, since the µ m are monotonically increasing. Note also that the differences which concludes the proof that fr is well-defined. We now prove naturality. Let f : (X , µ) (Y , ν ) be a Krn-morphism, ρ ∈ M ≪µ (X ) and ϕ ∈ S ∞ (Y , ν ) we then have

d mn := ∫ X ϕ n dµ m+1 - ∫ X ϕ n dµ m are monotonically increasing in n. Indeed we have ∫ X ϕ n+1 dµ m+1 - ∫ X ϕ n+1 dµ m - ∫ X ϕ n dµ m+1 - ∫ X ϕ n dµ m = ∫ X (ϕ n+1 -ϕ n ) dµ m+1 - ∫ X (ϕ n+1 -ϕ n ) dµ m >
fr (Y ,ν ) • M ≪• f (ρ)(ϕ) = ∫ Y ϕ d(M ≪• f (ρ)(ϕ)) = ∫ Y (ϕ • f ) dρ Theorem 6 = S ∞ (f ) ∫ Y (-) dρ (ϕ) = S ∞ (f ) • fr (X, µ) (ρ)(ϕ) ■ Proof of Theorem 25.
The fact that rn (X, µ) and mr (X, µ) are inverse of each other is just a restatement of the two well-known equalities for Radon-Nikodym derivatives:

d ∫ -ϕ dµ dµ = ϕ and ∫ B X dρ dµ dµ = ρ(B X ) ■ Proof of Theorem 26.
Let (X , µ) be a Krn-object, let F ∈ (L ∞ (X , µ)) σ and let ϕ ∈ L ∞ (X , µ). We have

fr (X, µ) • rr (X, µ) (F )(ϕ) = ∫ X ϕ d(rr (X, µ) (F )) = F (ϕ)
where the last equality follows from Lemma 40. Similarly, we have

rr (X, µ) •fr (X, µ) (ρ)(B X ) = fr (X, µ) (ρ)(1 B X ) = ∫ X 1 B X dρ = ρ(B X )

■

Proof of Theorem 28.

The case p = 1 has been treated already, for the case of 1 < p < ∞, see for example the proof of Theorem 4.4.1 of [START_REF] Bogachev | Measure Theory I[END_REF]. Finally for the case of p = ∞, see Proposition 3.3 of [START_REF] Chaput | Approximating Markov Processes by averaging[END_REF].

■

Proof of Proposition 30. Note in (11) that we disintegrate p with respect to two different measures. For notational clarity let us define the endokernels a := p † µ • p b := p † ν • p The kernel a associates to each x ∈ X in a fibre p -1 ({i}) the measure π † µ (i) supported by this fibre. In particular it is constant on each fibre, and similarly for b. We can now compute:

f p (x)(A) := b • f • a(x)(A) = ∫ y ∈X b(y)(A) d(f • a)(x) (1)
= i ∈X ′ ∫ y ∈p -1 (i) b(y)(A) d(f • a)(x) (2)
= i ∈X ′ p † ν (i)(A ∩ p -1 (i))f • a(x)(p -1 (i)) = i ∈X ′ p † ν (i)(A ∩ p -1 (i)) ∫ y ∈X f (y)(p -1 (i)) da(x) (3)
= i ∈X ′ p † ν (i)(A ∩ p -1 (i)) ∫ y ∈p -1 (p(x )) f (y)(p -1 (i)) dp † µ (p(x))
where (1) follows by decomposing X in fibres, (2) is because b(y)(A) is constant on fibres, and (3) uses the fact that a(x) := p † µ (p(x)) is supported on the fibre of p(x). We can considerably simplify the expression above. Note first that by definition of the disintegration

ν (A ∩ p -1 (i)) = p † ν (i)(A ∩ p -1 (i))ν(p -1 (i)) (17) Similarly, by definition of the disintegration, for i, j ∈ X ′ ∫ p -1 (j) f (x)(p -1 (i)) dµ = ∫ X 1 p -1 (j) (x)f (x)(p -1 (i)) dµ = k ∈X ′ µ(p -1 (k)) ∫ p -1 (k ) 1 p -1 (j) (x)f (x)(p -1 (i)) dp † µ (k) = µ(p -1 (j)) ∫ p -1 (j) f (x)(p -1 (i)) dp † µ (j) (18)
where the last step uses the fact that p † µ (k) is supported by the fibre over k. By multiplying the LHS of ( 17), [START_REF] Kozen | Kleene algebra with tests[END_REF] we get

ν (A ∩ p -1 (i)) ∫ p -1 (j) f (x)(p -1 (i))dµ = ∫ X f (x)(A ∩ p -1 (i))dµ ∫ p -1 (j) f (x)(p -1 (i)) dµ = ∫ p -1 (j) f (x)(A ∩ p -1 (i)) dµ ∫ X f (x)(p -1 (i)) dµ = µ(p -1 (j)) ∫ p -1 (j) f (x)(A ∩ p -1 (i)) dp † µ (j) ∫ X f (x)(p -1 (i)) dµ = µ(p -1 (j))ν (p -1 (A)) ∫ p -1 (j) f (x)(A ∩ p -1 (i)) dp † µ (j) (19)
It now follows from [START_REF] Kozen | Semantics of probabilistic programs[END_REF], [START_REF] Kozen | Kleene algebra with tests[END_REF], and (19) that

µ(p -1 (j))ν (p -1 (A)) ∫ p -1 (j) f (x)(A ∩ p -1 (i)) dp † µ (j) = p † ν (i)(A ∩ p -1 (i))ν (p -1 (i))µ(p -1 (j)) ∫ p -1 (j) f (x)(p -1 (i)) dp † µ (j) Which simplifies to ∫ p -1 (j) f (x)(A ∩ p -1 (i)) dp † µ (j) = p † ν (i)(A ∩ p -1 (i)) ∫ p -1 (j) f (x)(p -1 (i)) dp † µ (j) (20)
We can now use [START_REF] Selinger | Towards a semantics for higher-order quantum computation[END_REF] to get b

• f • a(x)(A) = i ∈X ′ ∫ p -1 (π (x )) f (x)(A ∩ p -1 (i)) dp † µ (p(x)) = ∫ p -1 (p(x )) f (x)(A) dp † µ (p(x)) = f • a(x)(A) (21)

■

Proof of Lemma 34.

The map f (-)(A) : X → R defines a random variable, and the discretization scheme defines a filtration σ (p n ) ⊆ σ (p n+1 ) whose union is B X . Following Lemma 8 and Proposition 30 we have

f n (x)(A) := f (x)(A) • p † n • p n = E [f (x)(A) | σ (p n )] We thus have a sequence f n (-)(A) of random variables X → R which is adapted to the filtration σ (p n ), n ∈ N by construction. We can now compute for any m < n E [f n (x)(A) | σ (p m )] =f (x)(A) • p † n • p n • p † m • p m (1) = f (x)(A) • p † n • p n • (p nm • p n ) † • p m (2) = f (x)(A) • p † n • p n • p † n • p † nm • p m (3) = f (x)(A) • p † m • p m = f m (x)(A)
where (1) is by definition (??), (2) is by Thm [START_REF] Desharnais | Metrics for labelled Markov processes[END_REF] and (3) is by Theorem [START_REF] Dahlqvist | Giry and the Machine[END_REF]. We have thus shown that f n (-)(A) is a martingale for the filtration generated by the discretization scheme, and the result now follows from Lévy's upward convergence Theorem ([25, Th. 14

.2]) since f (x)(A) = E [f (x)(A) | σ ( n σ (p n ))]. ■ Proof of Theorem 35.
Let (B n ) n ∈N be a countable basis for the Borel σ -algebra of X , which we assume w.l.o.g. is closed under finite unions and intersections. It follows from Lemma 34 that for each

B n , lim k f k (x)(B n ) = f (x)(B n ) for all x ∈ X \ N n where µ(N n ) = 0. It follows that for every x ∈ X \ i N i lim k →∞ f k (x)(B n ) = f (x)(B n )
for all basic Borel sets B n , and µ( i N i ) = 0. Now we use the πλ-lemma with (B n ) n ∈N as our π -system. We define

L := {C | f n (x)(C) → f (x)(C) for all x ∈ X \ ∪ i N i } and show that it is a λ-system. Clearly each B n ∈ L. Suppose C ∈ L, it is then immediate that C c ∈ L. Now consider a sequence C i ∈ L with C i ⊆ C i+1 , and let C ∞ := ∪ ∞ i=1 C i . We want to show that lim n f n (x)(C ∞ ) = lim n lim m f n (x)(C m ) ( * ) = lim m lim n f n (x)(C m ) = lim m f (x)(C m ) = f (x)(C ∞ )
where ( * ) is the only step we need to justify. To show that the iterated limits can be switched, note first that since

| f n (x)(C m ) -f (x)(C ∞ )| = | f n (x)(C m ) -f (x)(C m ) + f (x)(C m ) -f (x)(C ∞ )| ≤ | f n (x)(C m ) -f (x)(C m )| + | f (x)(C m ) -f (x)(C ∞ )| since the two terms converge separately, for any ϵ > 0 we can find N > 0 s. th. for all m, n ≥ N , | f n (x)(C m ) -f (x)(C ∞ )| < ϵ /2 + ϵ /2 = ϵ. Thus lim (m,n)→∞ f n (x)(C m ) = f (x)(C ∞ ).
Now note also that for all m 0 ∈ N the sequence

f n (x)(C m 0 ) converges to f (x)(C m 0 ) (by definition of L), and it is not hard to see that f (x)(C m ) converges to f (x)(C ∞ ). Conversely for all n 0 ∈ N, the sequence f n 0 (x)(C m ) converges to f n 0 (C ∞ ) (by virtue of f n 0 (x) being a measure). For ϵ /2 > 0 we can find N > 0 such that for all m, n > N , | f n (x)(C m ) -f (x)(C ∞ )| < ϵ /2. We can also find M > 0 such that for all m > M, | f n (x)(C m ) -f n (x)(C ∞ )| < ϵ /2.
By taking the maximum of N and M it is clear that for all m, n above this maximum

| f n (x)(C ∞ ) -f (x)(C ∞ )| ≤ | f n (x)(C ∞ ) -f n (x)(C m )| + | f n (x)(C m ) -f (x)(C ∞ )| < ϵ We have thus shown that lim m→∞ lim n→∞ f n (x)(C m ) = lim (m,n)→∞ f n (x)(C m ) = f (x)(C ∞ ) = lim n→∞ lim m→∞ f n (x)(C m ).
Thus L is a λ-system, and it follows from the πλ-lemma that σ ((B n ) n ∈N ) ⊆ L which concludes the proof of pointwise almost everywhere convergence.

For the proof of L 1 -convergence we start by showing that lim which concludes the proof of [START_REF] Smolka | Cantor meets Scott: Domain-theoretic foundations for probabilistic network programming[END_REF]. To extend the result to simple functions and then to arbitrary functions ϕ ∈ L 1 (X , ν ) is routine.

■

Proof of Lemma 36. Let f n , f : (X 1 , µ 1 ) (Y 1 , ν 1 ), д n , д : (X 2 , µ 2 ) (Y 2 , ν 2 ), we need to show that for any ϕ

∈ L 1 (Y 1 × Y 2 , ν 1 ⊗ ν 2 ) ∫ X 1 ×X 2 ∫ Y 1 ×Y 2 ϕ(y 1 , y 2 )d(f n ⊗ д n )(x 1 , x 2 )- (23)
∫ Y 1 ×Y 2 ϕ(y 1 , y 2 )d(f ⊗ д)(x 1 , x 2 ) dµ 1 ⊗ dµ 2 → 0
To show this it is enough to show that ∫

Y 1 ×Y 2 ϕ(y 1 , y 2 ) d(f n ⊗ д n )(x 1 , x 2 ) → ∫ Y 1 ×Y 2 ϕ(y 1 , y 2 ) d(f ⊗ д)(x 1 , x 2 )
pointwise almost everywhere and that

sup n ∫ Y 1 ×Y 2 ϕ(y 1 , y 2 )d(f n ⊗ д n )(x 1 , x 2 ) 1 < ∞ (24)
Since in these circumstances pointwise convergence almost everywhere implies L 1 -convergence.

To show [START_REF] Staton | Commutative semantics for probabilistic programming[END_REF] we proceed as usual: we start with simple functions and use monotone convergence. Let us first consider any measurable A ⊆ Y 1 × Y 2 , then ∫

(y 1 ,y 2 )∈Y 1 ×Y 2 1 A (y 1 , y 2 ) d(f n ⊗ д n )(x 1 , x 2 ) = ∫ y 1 ∈Y 1 д n (x 2 )({y 2 | (y 1 , y 2 ) ∈ A}) d f n (x 1 ) (1)
→

∫ y 1 ∈Y 1 д(x 2 )({y 2 | (y 1 , y 2 ) ∈ A}) d f n (x 1 ) = ∫ (y 1 ,y 2 )∈Y 1 ×Y 2 1 A (y 1 , y 2 ) d(f ⊗ д)(x 1 , x 2 )
where (1) is by assumption on f n , д n , Theorem 35 and dominated convergence. The result extends completely straightforwardly to all simple functions. Finally for an arbitrary ϕ ∈ L 1 (Y 1 × Y 2 , ν 1 ⊗ ν 2 ) we construct a monotone approximating sequence of simple functions s i ↑ ϕ and use the usual 3ϵ argument to conclude.

To show [START_REF] Staton | Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints[END_REF] we suppose w.l.o.g. that ϕ(x, y) ≥ 0 and compute using Fubini and Lemma 31 ∫

Y 1 ×Y 2 ϕ(y 1 , y 2 ) d(f n ⊗ д n )(x 1 , x 2 ) 1 = ∫ X 1 ∫ X 2 ∫ Y 1 ∫ Y 2 ϕ(y 1 , y 2 ) dд n (x 2 ) d f n (x 1 ) dµ 2 dµ 1 = ∫ X 1 ∫ Y 1 ∫ X 2 ∫ Y 2 ϕ(y 1 , y 2 ) dд n (x 2 ) dµ 2 d f n (x 1 ) dµ 1 ≤ ∫ X 1 ∫ Y 1 ∫ X 2 ∫ Y 2 ϕ(y 1 , y 2 ) dд(x 2 ) dµ 2 d f n (x 1 ) dµ 1 = ∫ X 2 ∫ Y 2 ∫ X 1 ∫ Y 1 ϕ(y 1 , y 2 ) d f n (x 1 ) dµ 1 dд(x 2 ) dµ 2 ≤ ∫ X 2 ∫ Y 2 ∫ X 1 ∫ Y 1 ϕ(y 1 , y 2 ) dд(x 2 ) d f (x 1 ) dµ 1 dµ 2 = ∫ Y 1 ×Y 2 ϕ(y 1 , y 2 ) d(f ⊗ д)(x 1 , x 2 ) 1 < ∞
The last step is by definition of ν 1 , ν 2 .

■

Proof of Theorem 37. By definition of (-) * we need to show that f n ∞ -→ s f ∞ and that post-composing with G is continuous for the SOT. In fact, we can shown both by proving that composition is jointly continuous for the SOT and operators in the image of S p . Note that in general composition is not jointly continuous for the SOT, but stochastic operators form a bounded set of operators and on these composition is jointly continuous in the SOT. Assume д n -→ s д for kernels д n , д : (X , µ) (Y , ν ) and h n -→ s h for kernels h n , h : (Y , ν ) (Z , ρ). We then have for any ϕ ∈ L 1 (Z , ρ):

∥S 1 д n (S 1 h n (ϕ)) -S 1 д(S 1 h(ϕ))∥ = ∥(S 1 n -S 1 д)(S 1 h(ϕ)) + (S 1 д n (S 1 h n (ϕ) -S 1 h(ϕ)))∥ ≤ ∥(S 1 д n -S 1 д)(S 1 h(ϕ))∥ + ∥(S 1 д n (S 1 h n (ϕ) -S 1 h(ϕ)))∥

≤ ∥S 1 д n -S 1 д)(S 1 (h(ϕ))∥ + ∥S 1 д n ∥ ∥S 1 h n (ϕ) -S 1 h(ϕ)∥ where the last step follows from Hölder's inequality and the fact that S 1 д n , being a stochastic operator, is bounded.

Continuity under post-composition by G now follows easily. For the continuity of the (-) ∞ construction, we first work inductively on the construction of the maps a k defined in ( 14) and [START_REF] Giry | A Categorical Approach to Probability Theory[END_REF]. We denote by a n k the kernels generated by f n and a k those generated by f , k ∈ N. By definition ( 14 Having shown that the maps b n k defining f n ∞ converge to the maps b k defining f ∞ we now show that S p f n ∞ (ϕ) -S p f ∞ (ϕ) 1 converges to 0 for any ϕ ∈ L 1 ((2 H ) ω , µ ω ). As usual we start with simple functions: let ϕ = i α i 1 B i be a simple function. For any B i we have

B i ⊆ ∞ k π k [B i ] ⇒ µ ∞ (B i ) ≤ ∞ k µ(π k )
and thus there can only exist finitely many indices for which the corresponding projection of B i has not got full measure. Since the simple function is a finite sum, this means that ϕ is defined by measurable sets with non-trivial measure on only a finite set of coordinates. Let N be the largest of these coordinates, we then have:

S p f n ∞ (ϕ) -Lp f op f ∞ (ϕ) 1 = ∫ 2 H ∫ (2 H ) ω ϕ d f n ∞ (x) - ∫ (2 H ) ω ϕ d f ∞ (x) dµ = ∫ 2 H ∫ (2 H ) N ϕ db n N (x) - ∫ (2 H ) N ϕ db(x) dµ
and the result follows from [START_REF] Williams | Probability with martingales[END_REF]. Extending to arbitrary maps is completely straightforward.

■

Figure 1 .

 1 Figure 1. Approximate posteriors

Figure 2 .Figure 3 .

 23 Figure 2. Log-likelihood of f 5,3

  and the diagram described by the morphisms

  b

Figure 4 .

 4 Figure 4. p ; (dup; p) 3 ∞ ) starting at (0)

  0 since the sequences ϕ n and µ m are monotonically increasing. Since d mn is monotonically increasing in n we can apply the CMT to d mn seen as a function of m w.r.t. the counting measure, i.e.

n→∞ S p f n ( 1 AX|X|

 1 ) -S p (1 A ) 1 = 0[START_REF] Smolka | Cantor meets Scott: Domain-theoretic foundations for probabilistic network programming[END_REF] for any Borel subset A. For this we use exactly the same reasoning as above. The only difference is that we need to check thatlim n→∞ ∫ f n (x)(C ∞ )f (x)(C ∞ )| dµ = 0For this we use the fact that we have just shownf n (x)(C ∞ ) → f (x)(C ∞ ) pointwise almost everywhere, and that | f n (x)(C ∞ )f (x)(C ∞ )| ≤ 1 with 1 µ-integrable. It follows by dominated convergence that lim n→∞ ∫ f n (x)(C ∞ )f (x)(C ∞ )| dµ = ∫ X lim n→∞ | f n (x)(C ∞ )f (x)(C ∞ )| dµ = 0

) a n 1 =

 1 η ⊗ f n • ∆ 1 and it follows from Lemma 36 and SOT continuity of composition that a n 1 -→ s a 1 . Now assuming that a n k-1 -→ s a k -1 , the exact same argument show that a n k -→ s a k . Finally, the joint continuity of composition givesb n k := a n k • . . . • a n 1 -→ s b k := a k • . . . • a 1 (25) for every k ∈ N.

Unlike the category Krn which does not have products.

■

Proof of Theorem 22. We start with the following elementary lemma.

Proof. The proof of naturality now follows easily: it is enough to show the equality in the case where ψ = 1 B X for a measurable subset B X of X , and the result then extends to all measurable functions by linearity of integrals and the MCT.

We have

□

To show naturality we now let f :

Again, we start with a simple but helpful Lemma.

Lemma 40. Let F ∈ (S ∞ (X , µ) σ and ϕ ∈ S ∞ (X , µ), then

Proof. Starting with characteristic functions, let ϕ = 1 B for some measurable subset B of X . We then have

We can then extend the result to simple functions by linearity and then to all functions in L ∞ (X , µ) by the MCT. □

To show naturality we now let f : (X , µ) (Y , ν ) be a Krnmorphism, F ∈ (S ∞ (X , µ)) σ and B Y measurable in Y . We


B Kribaa

Z Rouabah

C Le Loirec

C Champion

N Bouarissa
email: nbouarissa@yahoo.fr

Positron backscattering from solid targets: Modeling of scattering processes via various approaches

Monte Carlo simulation of 1-4 keV positron backscattering from semi-infinite solid targets ranging from Be (z = 4) to Au (z = 79) with normal angle of incidence is here reported. In our study, the elastic and inelastic scattering cross sections are modeled by using various approaches based on either a classical or a quantum mechanical treatment. Calculations of positron backscattering coefficient are then reported for the solid targets of interest. The results obtained show a fairly good agreement with the data available in the literature. The dependence of the positron backscattering coefficient versus the atomic number of the solid target of interest has been investigated. In this respect, polynomial functions are proposed which does not require any recourse to Monte Carlo calculations.

Introduction

Modeling the transport of low energy positrons in solid targets is of great importance for studying solid surfaces and defect profiles [START_REF] Schultz | Interaction of positron beams with surfaces thin films, and interfaces[END_REF][START_REF] Ishii | Positrons at Metallic Surfaces[END_REF][START_REF] Puska | Theory of positrons in solids and on solid surfaces[END_REF]Dupasquier and Mills, 1995;Nieminen, 1995). Recent advances in this field have been directed towards understanding of the processes by which positrons slow down in solids. The ultimate fate of positrons in condensed matter is obviously annihilation in the nanosecond timescale. However, during that time a rich variety of physical phenomena occur whose knowledge is of prime importance for determining the particle ranges as well as the backscattering coefficients [START_REF] Bouarissa | Backscattering of slow positron from semi-infinite aluminium[END_REF][START_REF] Bouarissa | A computer simulation of slow positron implantation depths in aluminium[END_REF]. With respect to the slow-positron-beam experiments, the essential point is that a large fraction of positrons can diffuse back to the surface and then be emitted into the vacuum either as free positron or as Positronium (Ps) [START_REF] Boev | Electron and positron energy levels in solids[END_REF]. It is clear that the backscattering process must be sensitively determined by the details of the elastic and inelastic scattering interactions [START_REF] Massoumi | Positron and electron backscattering from solids[END_REF][START_REF] Bouarissa | Transport of electrons and positrons impinging on solid targets: a comparative study performed by using a Monte Carlo simulation[END_REF]. In this context, we refer the interested reader to the recent reviews and monographs dealing with positrons as condensed matter and near-surface probes [START_REF] Schultz | Interaction of positron beams with surfaces thin films, and interfaces[END_REF][START_REF] Ishii | Positrons at Metallic Surfaces[END_REF][START_REF] Puska | Theory of positrons in solids and on solid surfaces[END_REF]Dupasquier and Mills, 1995;Nieminen, 1995). To study the penetration of charged particles in solids, the Monte-Carlo (MC) codes appears as the best-suited tools since able to model step by step, interaction after interaction the full history of the incident particle as well as that of all the secondary species created along the primary track in matter [START_REF] Shimizu | Monte Carlo modelling of electron-solid interactions[END_REF][START_REF] Dapor | Monte Carlo simulation of the energy deposited by few keV electrons penetrating in thick targets[END_REF][START_REF] Dapor | Monte Carlo simulation of backscattered electrons and energy from thick targets and surface films[END_REF][START_REF] Dapor | Electron-Beam Interactions With Solids: Application of the Monte Carlo Method to Electron Scattering Problems[END_REF][START_REF] Sobol | The Monte Carlo Method[END_REF][START_REF] Jensen | Positron beams for solids and surfaces[END_REF][START_REF] Rouabah | Monte Carlo simulation of electron slowing down in indium[END_REF]. Thus, by comparing the parameters obtained from the Monte Carlo simulation with experiments, one can get information about the accuracy of the modeling of the scattering processes used in the simulation.

The current work aims at studying backscattering of 1-4 keV positrons from solid targets ranging from Be to Au. To do that, the modeling of elastic and inelastic scattering cross sections was provided by using a variety of classical and quantum approaches. As an application, positron backscattering coefficients have been determined for a large set of solid targets including materials such as Ti, Fe, and Sn, which have never been investigated, to the best of or knowledge. Comparisons with experiment show a fairly good agreement and point out the accuracy of both the classical and the quantum mechanical approaches.

Theoretical details

In the first approach used in the present work and referred to as PW1, the elastic scattering is modeled by using the Rutherford differential cross section, modified to account the electronic screening [START_REF] Valkealahti | Monte Carlo calculations of keV electron and positron slowing down in solids[END_REF], where the numerical coefficient in the Nigam atomic screening factor is taken to be a variable that depends on the positron energy before each collision, as suggested by [START_REF] Bouarissa | Backscattering of slow positron from semi-infinite aluminium[END_REF]. In this respect, the numerical coefficient in the Nigam atomic screening factor referred to as [START_REF] Bouarissa | Backscattering of slow positron from semi-infinite aluminium[END_REF] has been determined for several selected solid targets ranging from Be to Au in the positron primary energy range of 1-4 keV. Our results give the following expressions:

(E) = -0.305 × 10 -10 E 3 + 0.2517 × 10 -6 E 2 -0.0007E + 3.258 (for Be)

(1)

(E) = -1.44 × 10 -10 E 3 + 1.32 × 10 -6 E 2 -0.0042E + 9.23 (for Al + Si) (2) (E) = -1.82 × 10 -10 E 3 + 1.586 × 10 -6 E 2 -0.00488E + 9.455 (for Ti) (3) (E) = -2.49 × 10 -10 E 3 + 2.285 × 10 -6 E 2 -0.00745E + 14.27 (for Fe) (4) (E) = -3.35 × 10 -10 E 3 + 3.20 × 10 -6 E 2 -0.011E + 22.26 (for Cu) (5) (E) = -1.9 × 10 -10 E 3 + 1.94 × 10 -6 E 2 -0.00754E + 17.83 (for Zn) (6)
(E) = -1.69 × 10 -10 E 3 + 0.4059 × 10 -6 E 2 -0.00336E + 14.97 (for Sn)

(E) = -1.46 × 10 -10 E 3 + 1.82 × 10 -6 E 2 -0.009E + 23.18 (for Au) (7)
For inelastic processes, both core and valence electron excitations are treated by using Gryzinski excitation function expressions (Gryzinski, 1965a,b,c). To calculate the total inelastic scattering cross section, we have followed the procedure of Bouarissa described in details in [START_REF] Bouarissa | Monte Carlo Simulation of Positron Penetration in Metals[END_REF].

In the second approach used in the present work (referred to as PW2), the elastic scattering is treated by using the analytical approximation as independently developed by [START_REF] Baro | Simplified Monte Carlo simulation of elastic electron scattering in limited media[END_REF][START_REF] Baro | An algorithm for Monte Carlo simulation of the penetration and energy loss of electrons and positrons in matter[END_REF] and by [START_REF] Miotello | Slow electrons impinging on dielectric solids. II. Implantation profiles electron mobility, and recombination processes[END_REF]. In this approximation, the transport cross-section has been calculated for each target element of interest using the approximation of [START_REF] Rouabah | Study on electron scattering in solid targets using accurate transport cross-sections[END_REF]. Similarly to the first approach of the present contribution, the inelastic scattering has been treated using Gryzinski excitation function expressions as described by [START_REF] Bouarissa | Monte Carlo Simulation of Positron Penetration in Metals[END_REF].

The third approach used in the present work (referred to as PW3) consists in treating the elastic scattering by using the same method as that described in the second approach of this contribution, whereas the inelastic scattering has been handled by substituting the Gryzinski's formula, in our Monte Carlo code with the Ashley's differential inverse inelastic mean free path as described in Ashley's optical-model [START_REF] Ashley | Interaction of low-energy electrons with condensed matter: stopping powers and inelastic mean free paths from optical data[END_REF][START_REF] Ashley | Energy loss rate and inelastic mean free path of low-energy electrons and positrons in condensed matter[END_REF]. Finally, the fourth approach used in the present work (referred to as PW4) is based on the PENE-LOPE code. The latter is a Monte Carlo code of general purpose that permits us to simulate the coupled transport of photons, electrons and positrons in matter with a very good accuracy at low energies [START_REF] Salvat | PENELOPE-A Code System for Monte Carlo Simulation of Electron and Photon Transport[END_REF][START_REF] Sempau | Experimental benchmarks of the Monte Carlo code PENELOPE[END_REF]. The electrons and positrons are simulated using a mixed scheme where interactions are classified into hard and soft. Hard events are simulated step by step and involve angular deflection or energy losses above user-defined cutoffs whereas soft events occurring between two hard collisions are simulated by means of an artificial single event. We used the 2006 release of the code [START_REF] Salvat | PENELOPE-A Code System for Monte Carlo Simulation of Electron and Photon Transport[END_REF].

Simulation procedure

The Monte Carlo simulation is probably the most powerful theoretical method for investigating the charged-particle-solid interaction problem. Besides, it also provides a physical insight of the details of the investigation process in addition to their results. Initially positrons lose rapidly their energy in a solid target. Energy is lost to electron excitations, including target atom ionizations and collective plasmon-like processes. Phonon excitations take over at lower energies, which eventually lead to positron thermalization [START_REF] Puska | Theory of positrons in solids and on solid surfaces[END_REF]. The thermal stage ends when the positron annihilates with an electron. The basic idea of the Monte Carlo simulation is to simulate trajectories of the positron penetrating into solid targets. The positron-host atom interaction is incorporated into the Monte Carlo framework via the cross sections for the different scattering processes. The simulation uses uniform random numbers belonging to the range [0-1].

In the present paper, a Monte Carlo simulation program that has essentially the same general structure as that of [START_REF] Bouarissa | Monte Carlo Simulation of Positron Penetration in Metals[END_REF] has been used for the PW1, PW2 and PW3 approaches. In all cases, we follow the positron until its energy becomes smaller than an energy cut-off here taken to be 20 eV. As a matter of fact, the choice of this energy does not have much effect, since the path length travelled by the positron between 20 eV and near thermal energy is insignificant compared to the implantation depth [START_REF] Baker | Median penetration depths and implantation profiles for low energy positrons in Al[END_REF]. All results obtained from these approaches are for semiinfinite medium with a planar surface with normal incidence of the positrons. 10 4 particle histories are used in each simulation run for each system.

As regards the PW4 approach, the simulation is controlled by parameters fixed for the various materials used in the geometry:

(i) E abs is the absorption energy, namely, the energy at which the track evolution is stopped. The kinetic energy of the particle is then locally deposited. (ii) C 1 is the average angular deflection between two hard elastic collisions. (iii) C 2 is the maximal fractional energy loss between two hard elastic collisions. (iv) W CC is the energy cut-off for hard inelastic interactions. (v) W CR is the energy cut-off for hard bremsstrahlung emission. We used the 2006 release of the code [START_REF] Salvat | PENELOPE-A Code System for Monte Carlo Simulation of Electron and Photon Transport[END_REF].

The TABLES.F program, which produces tables of interaction properties for arbitrary materials is used to determine the positron range and stopping powers in the different investigated materials. A complete simulation is performed to get the backscattering [START_REF] Dapor | Elastic scattering calculations for electrons and positrons in solid targets[END_REF].

coefficient of each material. Primary positrons impinge normally on semi-infinite material slabs with a given energy (from 1 to 4 keV). We used the same parameters as those reported by [START_REF] Sempau | Experimental benchmarks of the Monte Carlo code PENELOPE[END_REF] in their benchmark of PENELOPE. E abs for positrons is set equal to 0.05% of the beam energy. In all cases, W CC and W CR are equal to E abs (positron) and E abs (photon), respectively. For photons, we set E abs equal to one tenth of the incident beam energy.

The parameters C 1 and C 2 are set equal to 0.05. The backscattering coefficients are calculated by the code.

Results

Many of the positrons implanted in the primary beam may reach the entrance surface prior to their annihilation, either before or after thermalization. Several scenarios are then possible (Puska andNieminen, 1994, 1995). The versatility of scenarios implies that positrons can be used to extract useful information of material properties near surfaces and interfaces. Besides, backscattering coefficients of positrons impinging on solid targets may provide stringent tests on the accuracy of the description of the scattering processes.

In the present work, the backscattering coefficients for 1-4 keV positron backscattered from semi-infinite selected target materials ranging from Be (z = 4) to Au (z = 79) have been calculated at normal incidence using the Monte Carlo simulation technique. Our results obtained using the different mentioned approaches, namely, PW1, PW2, PW3 and PW4 are given in Tables 1-6. Also shown for comparison are the experimental and previous theoretical data available in the literature. Note that the present calculated positron backscattering coefficients regarding the various materials of interest obtained using the different approaches are generally in reasonably good agreement with the experimental data reported in [START_REF] Coleman | Positron backscattering from elemental solids[END_REF]. In terms of theoretical calculations, our results agree generally well with those reported in [START_REF] Dapor | Elastic scattering calculations for electrons and positrons in solid targets[END_REF] [START_REF] Dapor | Elastic scattering calculations for electrons and positrons in solid targets[END_REF]. [START_REF] Dapor | Elastic scattering calculations for electrons and positrons in solid targets[END_REF]. and [START_REF] Jensen | Monte Carlo simulation of the transport of fast electrons and positrons in solids[END_REF]. When comparing between the different approaches used in the present contribution, one can note that the values of the positron backscattering coefficients obtained from the PW1, PW2 and PW3 approaches based on the classical treatment are generally close to those calculated from the PW4 approach based on the quantum treatment. Furthermore, the PW1, PW2 and PW3 values are in some cases better than those of PW4 as compared to experiment. This suggests that the approaches used in the calculation of the elastic and inelastic scattering cross sections and the stochastically description of positron transport implied by the Monte Carlo method are compatible with the experiments. It should be noted that for some solid targets of interest, no comparison has been made with the experimental or previous theoretical [START_REF] Jensen | Monte Carlo simulation of the transport of fast electrons and positrons in solids[END_REF]. c [START_REF] Dapor | Elastic scattering calculations for electrons and positrons in solid targets[END_REF].

data in the literature. In these cases, our results are predictions and may serve for reference for future works. Interestingly as well, one notes that the positron backscattering coefficient depends on both the solid target and the positron primary energy. Generally, the positron backscattering coefficient increases with increasing its primary energy for all elements of interest. The behavior is almost most common for all used approaches (classical and quantum ones) in the current work. Furthermore, it is consistent with the results of the previous theoretical models of positron implantation in solid targets [START_REF] Dapor | Elastic scattering calculations for electrons and positrons in solid targets[END_REF][START_REF] Jensen | Monte Carlo simulation of the transport of fast electrons and positrons in solids[END_REF] as well as with the available experimental data reported in the literature [START_REF] Coleman | Positron backscattering from elemental solids[END_REF] within the experimental uncertainty. It is to be noted that the positron backscattering coefficient is much smaller than the electrons backscattering coefficient [START_REF] Hannachi | Electron backscattering from solid targets: elastic scattering calculations[END_REF]. This can be traced back to the difference of the elastic scattering cross section of crystal atoms for positrons and electrons.

In Fig. 1 we show the variation of the positron backscattering coefficient denoted by versus the atomic number z of the solid targets of interest for various positron primary energies in the range 1-4 keV obtained from the PW4 approach. In this respect, we have tentatively suggested expressions that give the dependence of the positron backscattering coefficient on z for all solid targets under investigation in the following form: Equations ( 9)-( 12) are generalized and expressed as,

E = 1 keV (z) = 7.79 × 10 -7 z 3 -1.17 × 10 -4 z 2 + 0.55 × 10 -2 z + 0.022 (9) E = 2 keV Á (z) = 1.48 × 10 -6 z 3 -2.24 × 10 -4 z 2 + 1.04 × 10 -2 z + 0.002 (10) E = 3 keV Á (z) = 1.51 × 10 -6 z 3 -2.33 × 10 -4 z 2 + 1.15 × 10 -2 z -0.004 (11) E = 4 keV Á (z) = 1.73 × 10 -6 z 3 -2.72 × 10 -4 z 2 + 1.37 × 10 -2 z -0.017 (12)
Á (z, E) = a (E) × z 3 + b (E) × z 2 + c (E) × z + d (E) (13)
The determined coefficients a(E), b(E), c(E) and d(E) are summarized in Table 7. In view of this table, it seems that the coefficients a(E) and c(E) increase with increasing the positron primary energy from 1 up to 4 keV which is not the case for b(E) and d(E) that decrease when increasing the positron primary energy.

Equations ( 9)-( 13) provide the prediction of low-energy positron backscattering coefficients for a large set of solid targets ranging from Be (z = 4) to Au (z = 79) without requiring any recourse to the Monte Carlo calculations.

Conclusion

A Monte Carlo simulation of positron slowing down in selected solid targets ranging from Be to Au in the primary energy range 1-4 keV has been performed. Various approaches based on both classical and quantum treatments have been used for describing the elastic and inelastic scattering cross sections. Our results in terms of positron backscattering coefficient show that all used approaches give results that are in reasonably good agreement with the available experimental and previous theoretical data reported in the literature. It is found that the positron backscattering coefficient versus the atomic number z of the materials of interest can be fitted with polynomial functions for given positron primary energies within the range 1-4 keV.

Fig. 1 .

 1 Fig. 1. Positron backscattering coefficient as a function of the atomic number of solid targets.

Table 1

 1 Backscattering coefficients of 1-4 keV positrons impinging in semi-infinite Al target.

	Energy (keV) Al				Exp a	Theo b	Theo c
		PW1	PW2	PW3	PW4
	1	0.0697	0.076	0.078	0.0814	0.069 0.086	0.109
	2	0.076	0.081	0.076	0.0965		0.099
	3	0.0779	0.085	0.088	0.108	0.086 0.107	0.115
	4	0.093	0.0852	0.113	0.111		0.112

a

[START_REF] Coleman | Positron backscattering from elemental solids[END_REF]

. b

[START_REF] Jensen | Monte Carlo simulation of the transport of fast electrons and positrons in solids[END_REF]

. c

Table 2

 2 Backscattering coefficients of 1-4 keV positrons impinging in semi-infinite Cu target.

	Energy (keV)	Cu				Exp a	Theo c
		PW1	PW2	PW3	PW4
	1	0.150	0.172	0.184	0.0895	0.135	0.156
	2	0.150	0.162	0.173	0.138
	3	0.151	0.161	0.168	0.160	0.194	0.1194
	4	0.179	0.170	0.172	0.179

a

[START_REF] Coleman | Positron backscattering from elemental solids[END_REF]

. c

Table 3

 3 Backscattering coefficients of 1-4 keV positrons impinging in semi-infinite Be and Si targets.

	Energy (keV)	Be		Theo c	Si
		PW1	PW4		PW1	PW4
	1	0.0408	0.0346	0.042	0.0871	0.0881
	2	0.0312	0.0326		0.0992	0.107
	3	0.0470	0.0351	0.038	0.126	0.116
	4	0.0310	0.0301		0.141	0.125
	c

Table 4

 4 Backscattering coefficients of 1-4 keV positrons impinging in semi-infinite Ti and Fe targets.

	Energy (keV)	Ti		Fe
		PW1	PW4	PW1	PW4
	1	0.108	0.104	0.109	0.0964
	2	0.150	0.160	0.163	0.141
	3	0.201	0.191	0.211	0.155
	4	0.231	0.223	0.234	0.170

Table 5

 5 Backscattering coefficients of 1-4 keV positrons impinging in semi-infinite Zn and Sn targets.

	Energy (keV)	Zn		Exp a	Sn
		PW1	PW4		PW1	PW4
	1	0.090	0.0925	0.089	0.120	0.108
	2	0.116	0.131		0.189	0.151
	3	0.132	0.156	0.125	0.218	0.187
	4	0.155	0.174		0.221	0.241
	a Coleman et al. (1992).

Table 7

 7 Coefficients a(E), b(E), c(E) and d(E) for each positron incident energy in the range 1-4 keV.

	Positron incident	a(E)	b(E)	c(E)	d(E)
	energy (keV)
	1	7.79 × 10 -7	-1.17 × 10 -4	0.55 × 10 -2	0.022
	2	1.48 × 10 -6	-2.24 × 10 -4	1.04 × 10 -2	0.002
	3	1.51 × 10 -6	-2.33 × 10 -4	1.15 × 10 -2	-0.004
	4	1.73 × 10 -6	-2.72 × 10 -4	1.37 × 10 -2	-0.017