Wenwen Jian
email: wwjian16@fudan.edu.cn

Sergei Kuksin
email: sergei.kuksin@imj-prg.fr

Yuan Wu

THE BOGOLYUBOV-KRYLOV AVERAGING

come

Introduction

The classical Bogolyubov-Krylov averaging method is a method for approximated analysis of nonlinear oscillating process. Among a number of its equivalent or closely related formulations, we choose the following. In the space R N , let us consider the differential equation of the form

∂v ∂t + Av = P (v), v(0) = v 0 , 0 < ≤ 1, (1.1)
where A is a linear operator with pure imaginary eigenvalues without Jordan cells, and P (v) is a nonlinearity. The task is to study the behavior of solutions for (1.1) on time-interval of order -1 . Let us firstly pass to the slow time τ = t and rewrite the equation as

∂v ∂τ + -1 Av = P (v), v(0) = v 0 , (1.2)
where now τ is a time-variable of order one. Secondly, in equation (1.2), let us pass to the interaction representation variables 1 a(τ ) = e -1 τ A v(τ ), (1.3) and rewrite the equation as ∂a ∂τ = e -1 τ A P (e --1 τ A a), a(0) = v 0 . (1.4)

The Bogolyubov-Krylov averaging theorem is the following result: Theorem 1.1. Assume that the vector-field P is locally Lipschitz continuous. Then 1) the limit

P (a) = lim T →±∞ 1 |T | T 0 e
-1 sA P (e --1 sA a)ds (1.5) exists for all a ∈ R n .

2) There exists θ = θ(|v 0 |) > 0, such that for |τ | ≤ θ, a solution a (τ ) of equation (1.4) is o(1)-close, as → 0, to a solution of the equation ∂a ∂τ = P (a), a(0) = v 0 .

1 under this name the change of variable (2.3) is known in physics.

1

We stress that the only restriction imposed on the spectrum of the operator A is that it is pure imaginary. Theorem 1.1 and related results were proved by Bogolyubov-Krylov in a number of works in 1930's. The research was summarized in the book [START_REF] Bogoliubov | Asymptotic Methods in the Theory of Non-linear Oscillations[END_REF], also see in [START_REF] Arnold | Mathematical Aspects of Classical and Celestial Mechanics[END_REF]. In our work we present a proof of Theorem 1.1, based on a variation of the Bogolyubov-Krylov argument, developed recently for the purposes of partial differential equations in [START_REF] Huang | An averaging theorem for nonlinear Schrödinger equations with small nonlinearities[END_REF][START_REF] Huang | Time-averaging for weakly nonlinear CGL equations with arbitrary potentials[END_REF]. It allows to prove the averaging theorem above under minimal restrictions on the smoothness of the nonlinearity P -only its Lipschitz continuity is required -and it generalizes to a class of perturbative problems in PDEs. Theorem 1.1 is proved in Sections 3-4. In Section 5, we discuss its applications to the case when (1.2) is a Hamiltonian system. We remind that the Bogolyubov-Krylov averaging method was the first rigorously justified averaging theory. Before the work of Bogolyubov-Krylov the method of averaging existed as a heuristic theory, after that other rigorous averaging theories were created, see in [START_REF] Arnold | Mathematical Aspects of Classical and Celestial Mechanics[END_REF]. In particular, now the method of averaging applies to equations with added stochasticity. The approach of our work, enriched with the ideas of the seminal work [START_REF] Khasminski | On the avaraging principle for Ito stochastic differential equations[END_REF], suits well to the situation when the stochasticity is added to the problem in the form a stochastic force; both in the ODE and PDE settings. See the second half of the paper [START_REF] Huang | Time-averaging for weakly nonlinear CGL equations with arbitrary potentials[END_REF] and references in that work.

Our paper is based on the lecture notes for a course that SK was teaching at a CIMPA School on Dynamical Systems in Kathmandu (October 25 -November 5, 2018), which was attended by WJ and YW.

Notation. Abbreviation l.h.s. (r.h.s.) stands for "left hand side" ("right hand side"). By R + (by Z + ) we denote the set of non-negative real numbers (non-negative integers), denote by B R the open ball B R = {v| : |v| < R}, R > 0, and by BR -its closure.

Acknowledgements. SK was supported by the grant 18-11-00032 of Russian Science Foundation. WJ and YW were supported by the National Natural Science Foundation of China (No. 11790272 and No. 11421061).

preliminaries

Consider again equation (1.2), and assume that the linear operator A has N eigenvalues, counted with their geometrical multiplicities. Assume also that these eigenvalues are pure imaginary. Then they go in pairs ±iλ j , where 0 = λ j ∈ R (see [START_REF] Gelfand | Lectures on Linear Algebra[END_REF]). So N is an even number, N = 2n. The imposed restrictions on A are equivalent to the following conditions (see [START_REF] Gelfand | Lectures on Linear Algebra[END_REF]): KerA = {0} and in R 2n exists a basis {e + 1 , e - 1 , e + 2 , e - 2 , ..., e + n , e - n } such that in the corresponding coordinates {x 1 , y 1 , x 2 , y 2 , ..., x n , y n }, the matrix of the linear operator A has the form

           0 -λ 1 λ 1 0 0 . . . 0 0 0 -λ 2 λ 2 0 . . . 0 . . . . . . . . . . . . 0 0 . . . 0 -λ n λ n 0            . (2.1)
Thus, the original unperturbed linear system (1.1)| =0 reads:

               ẋ1 -λ 1 y 1 = 0, ẏ1 + λ 1 x 1 = 0, • • • ẋn -λ n y n = 0, ẏn + λ n x n = 0. (2.2)
Note that this linear system can be written in the 2) can be written more compactly if we introduce in the space R 2n a complex structure and write A and the perturbation P in its terms. Corresponding construction is performed in this section and is used below to prove Theorem 1.1; the complex language allows to shorten the proof significantly. Vectors in the space R 2n are caracterised by the coordinates (x 1 , y 1 , x 2 , y 2 , ..., x n , y n ). Let us introduce in R 2n a complex structure by denoting

         z 1 = x 1 + iy 1 , z 2 = x 2 + iy 2 , . . . z n = x n + iy n . (2.3)
Then the real space R 2n becomes a space of complex sequences z = (z 1 , z 2 , ..., z n ) with z j ∈ C. That is, we have achieved that R 2n C n . In the complex notation, the Euclidean scalar product

•, • in R 2n C n reads z, z = ( j z j z j ) =: (z • z ). (2.4)
For the real numbers λ 1 , λ 2 , ..., λ n as in (2.2) let us consider the linear operator

diag{iλ j } : C n → C n , (z 1 , z 2 , ..., z n ) → (iλ 1 z 1 , iλ 2 z 2 , ..., iλ n z n ).
In the real coordinates (x 1 , y 1 , x 2 , y 2 , ..., x n , y n ) it reads

(x 1 , y 1 , x 2 , y 2 , ..., x n , y n ) → (-λ 1 y 1 , λ 1 x 1 , -λ 2 y 2 , λ 2 x 2 , ..., -λ n y n , λ n x n ).
That is, in the complex coordinates the operator A with the matrix (2.1) is the operator diag{iλ j }, so the system of linear equations (1.1)| =0 = (2.2) reduces to the diagonal complex system vj + iλ j v j = 0, 1 ≤ j ≤ n. In the complex notation the perturbed system (1.1) reads

vj + iλ j v j = P j (v), v(0) = v 0 , v = (v 1 , v 2 , ..., v n ) ∈ C n . (2.5)
Below we assume that the vector-field P is locally Lipschitz, i.e. its restrictions to bounded balls B R , R > 0, are Lipschitz-continuous. The case of polynomial vector-field P will be for us of special interest, and we start with its brief discussion. Definition 2.1. A complex function F : C n → C is a polynomial if it can be written as

F (z) = 0≤|α|,|β|≤M C αβ z α zβ , where α = (α 1 , α 2 , ...α n ), β = (β 1 , β 2 , ...β n ) ∈ Z n + are multi-indices with the norm |α| = |α 1 | + |α 2 | + • • • + |α n |, C αβ
are some complex numbers, and

z α = n j=1 z αj j , zβ = n j=1 zβj j .
Definition 2.2. A vector-field P (z) is polynomial if every its component P j is a polynomial function.

We recall that for a function f (z) (real or complex) of a complex variable z = x + iy, the derivatives ∂f /∂z and ∂f /∂ z are defined as ∂f ∂z = 1 2 ( ∂f ∂x -i ∂f ∂y ) and ∂f ∂ z = 1 2 ( ∂f ∂x + i ∂f ∂y ). The lemma below follows by elementary calculation:

Lemma 2.3. Let z ∈ C and consider a complex polynomial F (z) = M m,n=1 C mn z m zn . Then ∂F ∂z = M m,n=1 mC mn z m-1 zn , and ∂F ∂ z = M m,n=1 nC mn z m zn-1 . If F : C n → R is a real-valued C 1 -smooth function, then ∂F ∂zj = ∂F ∂ zj , for any 1 ≤ j ≤ n. Example 2.4. For n = 1, consider the system of equations (2.6) ẋ -ωy = 2 x(x 2 -y 2 ), ẏ + ωx = 4 yx 2 .
Now λ = ω and in the complex coordinate v = x + iy the system reads

(2.7) v + iλv = (v 2 v + v 3 ).
Let us come back to the general case of locally Lipschitz vector-fields P .

Definition 2.5. Let X : R + → R + be a non-decreasing continuous function and f :

C n → C n be a continuous vector-field. We say that f ∈ Lip X (C n , C n ), if for any R ≥ 0, |f | B R ≤ X(R) and Lipf | B R ≤ X(R).
Example 2.6. Let P : C n → C n be a C 1 -smooth vector-field. For v ∈ C n we denote by dP (v) the differential of P at v (this is a linear over real numbers map from

C n to C n ). Denote X(R; P ) = max sup B R dP (v) , sup B R |P (v)| .
Then X defines a continuous function of R ≥ 0, and P ∈ Lip X (C n , C n ). Indeed, the continuity of X is obvious, while the second property follows from the mean-value theorem which implies that

|P (u 2 ) -P (u 1 )| ≤ X(R; P )|u 2 -u 1 | if u 1 , u 2 ∈ B R . Lemma 2.7. Let P ∈ Lip X (C n , C n ) and v 0 ∈ BR . Denote θ = R X(2R)
. Then a solution v(t) of (2.5) exists for |t| ≤ -1 θ and stays in the ball B2R .

Proof. Since P is a locally Lipschitz vector-field, then a solution v(t) of equation (2.5) exists till the blow-up time. Taking the scalar product of equation (2.5) with v(t) (see (2.4)), we get

1 2 d dt |v(t)| 2 = -i diag(λ j )v, v + P (v), v = P (v), v . Denote T = inf t ∈ [0, -1 θ] : |v(t)| ≥ 2R
, where T equals -1 θ if the set under the inf-sign is empty. Then for 0 < t ≤ T we have 1 2

d dt |v(t)| 2 ≤ |v||P (v)| ≤ X(2R)|v|.
Thus, d dt |v(t)| ≤ X(2R) and |v(t)| ≤ R + X(2R)t < 2R for all 0 < t < -1 θ. So T = -1 θ and the result follows. 2.2. Slow time and interaction representation. Denote τ = t. Then ∂v ∂t = ∂v ∂τ , so equations (2.5) reduce to

∂v j ∂τ + i -1 λ j v j = P j (v), 1 ≤ j ≤ n. (2.8)
Let us substitute in (2.8)

v j (τ ) = e -i -1 λj τ a j (τ ), 1 ≤ j ≤ n. (2.9) Then (2.8) becomes ȧj = e i -1 λj τ P j (v), 1 ≤ j ≤ n. (2.10) Denote a(τ ) = (a 1 (τ ), a 2 (τ ), ..., a n (τ )) ∈ C n . For a real vector w = (w 1 , w 2 , ..., w n ) ∈ R n let Φ w be the rotation operator Φ w : C n → C n , Φ w = diag{e iw1 , e iw2 , ..., e iwn }.
It is easy to see that

(Φ w ) -1 = Φ -w , Φ w1 • Φ w2 = Φ w1+w2 , Φ 0 = id,
and that each Φ w is a unitary transformation. Denote by Λ the vector (λ 1 , λ 2 , ..., λ n ) ∈ R n . Then (2.9) can be written as v(τ ) = Φ -τ -1 Λ a(τ ), or a(τ ) = Φ τ -1 Λ v(τ ). Thus, the system (2.10) reads as

∂a ∂τ = Φ τ -1 Λ • P (Φ -τ -1 Λ a(τ )), |τ | ≤ θ, (2.11)
with the initial condition

a(0) = v 0 , |v 0 | =: R. (2.12) Note that |a j (τ )| = |v j (τ )|, ∀τ, 1 ≤ j ≤ n. (2.13)

Averaging of vector-fields

We recall that a diffeomorphism G : R 2n → R 2n transforms a vector-field W on R 2n to the vector-field [START_REF] Arnold | Geometrical Methods in the Theory of Ordinary Differential Equations[END_REF]. Accordingly, a linear isomorphism Φ Λt , t ∈ R, transforms the vector-field P to

(G * W )(v) = dG(u)(W (u)), u = G -1 (v), see in
((Φ Λt ) * P )(v) = Φ Λt • P (Φ -Λt v).
Our goal in this section is to study the averaging in t of the vector-field above.

For a continuous vector-field P on C n and a vector Λ ∈ (R \ {0}) n , we denote The vector-field P is called the averaging of a field P in the direction of a vector Λ, and P T (a) is called the partial averaging. The latter always exists. Our goal in this section is to prove that the former also exists, if the mapping P is locally Lipschitz. To indicate the dependence of the two introduced objects on Λ, sometimes we will write them as • Λ and

P (a) = lim T →±∞ 1 |T | T 0 Φ Λt • P (Φ -Λt
• T Λ . We recall that being written in the special basis the matrix of operator A takes the form (2.1), and that after introducing in R 2n the complex structure (2.3) the matrix becomes diag{iλ j }. Since Φ Λt = exp(diag{iλ j }t), then the definition of P agrees with that in (1.5).

Lemma 3.1. If P ∈ Lip X (C n , C n ), then P T ∈ Lip X (C n , C n ) for any T = 0. Proof. If a ∈ BR , then Φ -Λt a ∈ BR . Since P ∈ Lip X (C n , C n ), one obtains |P (Φ -Λt a)| ≤ X(R),
for each t, and then

|y t (a)| ≤ X(R), ∀t. (3.4)
Similarly, for any a 1 , a 2 ∈ BR , we have

|y t (a 2 ) -y t (a 1 )| = |P (Φ -Λt a 2 ) -P (Φ -Λt a 1 )| (3.5) ≤ X(R)|Φ -Λt a 2 -Φ -Λt a 1 | ≤ X(R)|a 2 -a 1 |, ∀t.
From (3.4) and (3.5), one obtains

| P T (a)| ≤ sup |t|≤|T | |y t (a)| ≤ X(R),
and

| P T (a 2 ) -P T (a 1 )| ≤ sup |t|≤|T | |y t (a 2 ) -y t (a 1 )| ≤ X(R)|a 2 -a 1 |. Thus, P T ∈ Lip X (C n , C n ) for T = 0.
Lemma 3.2 (The main lemma of averaging). For any Λ ∈ (R \ {0}) n and P ∈ Lip X (C n , C n ), the limit of (3.1) exists for any a ∈ C n , and P ∈ Lip X (C n , C n ). If a ∈ BR , then the rate of convergence in (3.1) depends only on R, Λ and P .

Before proving the general case of Lemma 3.2, we firstly consider the case when P is a polynomial vector-field. Then,

P j (v) = 0≤|α|,|β|≤N C αβ j v α vβ , 1 ≤ j ≤ n, (3.6)
and one has

y t j (v) = e iλj t 0≤|α|,|β|≤N C αβ j i (e -iλit v i ) αi i (e iλit vi ) βi = 0≤|α|,|β|≤N C αβ j e it(λj -Λ•α+Λ•β) v α vβ .
It follows that

P T j (v) = 0≤|α|,|β|≤N C αβ j 1 |T | T 0 e it(λj -Λ•α+Λ•β) dt v α vβ . Definition 3.3. A pair (α, β) is called (Λ, j)-resonant if λ j -Λ • α + Λ • β = 0.
The resonant part of the polynomial vector-field (3.6) is another polynomial vector-field P res (v) such that

P res j (v) = pair (α,β) is (Λ,j)-resonant, 0≤|α|,|β|≤N C αβ j v α vβ for 1 ≤ j ≤ n.
Example 3.4. For equation (2.7) in Example 2.4, we have

P (v) = v 2 v + v 3 =: P 1 (v) + P 2 (v). The monomial P 1 is resonant since ω -ω • 2 + ω = 0. So now P res (v) = P 1 (v).
Note that

1 |T | T 0 e -it(λj -Λ•α+Λ•β) dt = 1, if (α, β) is (Λ, j)-resonant, 1 -iT (λj -Λ•α+Λ•β) (e -iT (λj -Λ•α+Λ•β) -1), otherwise. So, lim T →±∞ 1 |T | T 0 e -it(λj -Λ•α+Λ•β) dt = 1, if (α, β) is (Λ, j)-resonant, 0, otherwise. (3.7)
Thus, we have

P T j (v) -----→ T →±∞ P res j (v). (3.8)
Therefore, in the polynomial case the limit in (3.1) exists. Lemma 3.5. If P (v) ∈ Lip X (C n , C n ) is a polynomial vector-field of the form (3.6), then the limit P in (3.1) exists for all a ∈ C n , equals to the resonant part P res of P and satisfies P ∈ Lip X (C n , C n ). Moreover, if a ∈ BR , then the rate of convergence (3.1) depends only on R, Λ and P .

Proof. The existence of the limit P already is proved, and its Lischitz continuity easily follows Lemma 3.1. The second assertion holds since the rate of convergence in (3.7) and (3.8) depends only on the indicated quantities. We omit the details.

Now we begin to prove Lemma 3.2.

Proof. To show that the limit exists we have to verify that 1

|T |

T 0 e iλj t •P j (Φ -Λt a)dt converges to a limit as T → ±∞. It suffices to show that for any ξ > 0, there exists T = T (ξ, R, Λ, P ) > 0, such that (3.9)

| P T1 j (a) -P T2 j (a)| ≤ ξ, if |T 1 |, |T 2 | ≥ T .
For any j consider the restriction of P j to the closed ball BR . By the Stone-Weierstrass theorem, there exist N and a polynomial P N j (a) of degree N , depending only on R and P , such that

|P j (a) -P N j (a)| ≤ ξ 4 , ∀a ∈ BR .
We have got a polynomial vector field P N , for which the assertions of Lemma 3.2 already are proved.

Since Φ -Λt a ∈ BR for any t, then |y t j (a; P j ) -y t j (a;

P N j )| ≤ ξ 4 , ∀t, ∀a ∈ BR .
| P T1 j (a) -P N j (a)| ≤ ξ 2 , ∀|T 1 | ≥ T .
The same is true for T 2 . Therefore (3.9) follows, and the convergence (3.1) is established. The inclusion P ∈ Lip X is a consequence of Lemma 3.1, while the last assertion the lemma directly follows from the proof. The lemma is proved.

Example 3.6. Let λ j > 0 for all j and P j be an anti-holomorphic polynomial

P j (v) = |β|≤N C β j vβ .
Then no pair (0, β) is (Λ, j)-resonant and P = 0. 2) If P = diag(a 1 , . . . , a n ), a j ∈ C, then P = P .

3) The mapping v → P (v) commutes with all operators Φ Λθ , θ ∈ R.

4) The mapping

(C n × (R \ {0}) n ) (v, Λ) → P Λ (v) is measurable. So for every v the averaging P Λ (v) is a measurable function of Λ.
Proof. Properties 1) and 2) are obvious. Let us prove 3), assuming for definiteness that T > 0.

We have:

P (Φ Λθ a) = lim T →+∞ 1 T T 0 Φ Λt • P (Φ -Λt Φ Λθ a)dt = Φ Λθ lim T →+∞ 1 T T 0 Φ Λ(t-θ) • P (Φ -Λ(t-θ) a)dt = Φ Λθ lim T →+∞ 1 T T -θ -θ Φ Λt • P (Φ -Λt a)dt = Φ Λθ lim T →+∞ 1 T T 0 + 0 -θ - T T -θ Φ Λt • P (Φ -Λt a)dt = Φ Λθ P (a).
To prove 4), we note that for T > 0 the mappings (a, Λ) → P T Λ (a) are continuous, so measurable. By Lemma 3.2, the mapping in question is a point-wise limit, as T → ∞, of the measurable mappings above; so it also is measurable (see [START_REF] Rudin | Real and Complex Analysis[END_REF], Theorem 1.14).

Averaging for solutions of equation (2.11)

In this section we get our main result, describing the behaviour, as → 0, of solutions of equation (2.11) on time-intervals |τ | ≤ const, where const does not depend on . In view of (2.11), this also describes the behaviour of the amplitudes |v j (τ )| of solutions (2.8), and accordingly, the behaviour of the amplitudes of solutions for (2.5) on long time-intervals |t| ≤ const -1 .

Let in eq. (2.8) P ∈ Lip X (C n , C n ) for some function X as in Definition 2.5, and let v(τ ) be its solution such that v(0

) = v 0 . Denote |v 0 | = R. Then by Lemma 2.7, v(τ ) ∈ B2R for |τ | ≤ θ = R X(2R) . For |τ | ≤ θ the curve a (τ ) = Φ τ -1 Λ v(τ ) satisfies (2.
11), (2.12) and |a j (τ )| = |v j (τ )| for each j. So for |τ | ≤ θ we have:

(4.1) |a (τ )| ≤ 2R, | ∂a ∂τ | ≤ |P (Φ -τ -1 Λ a(τ ))| ≤ X(2R)
. Consider the collection of curves a (the solutions of equation (2.11)),

a ∈ C([-θ, θ], C n ), ∈ (0, 1].
By (4.1) and the Arzela-Ascoli theorem, the family {a , 0

< ≤ 1} is precompact in C([-θ, θ], C n ).
So there exists a sequence j → 0, such that (4.2)

a j → a 0 in C([-θ, θ], C n ), as j → 0, for some curve a 0 ∈ C([-θ, θ], C n ). By (4.1), |a (τ 1 ) -a (τ 2 )| ≤ X(2R)|τ 1 -τ 2 |.
Passing in this relation to the limit as j → 0, we obtain

(4.3) |a 0 (τ 1 ) -a 0 (τ 2 )| ≤ X(2R)|τ 1 -τ 2 |, ∀τ 1 , τ 2 ∈ [-θ, θ].
Now we address the following problem: does the limit a 0 depend on { j }? If it does not, then how to describe it?

A solution a (τ ) of (2.11) satisfies the relation

(4.4) a (τ ) = v 0 + τ 0 Φ s -1 Λ • P (Φ -s -1 Λ a (s))ds, ∀|τ | ≤ θ,
and the estimates (4.1). From Lemma 3.2,

(4.5) 1 |T | T 0 Φ t -1 Λ • P (Φ -t -1 Λ a (t))dt = P (a) + o(1), as T → ±∞,
where o(1) does not depend on v 0 if v 0 ∈ BR . Consider the following effective equation

(4.6) a(τ ) = v 0 + τ 0 P (a(s))ds, that is ∂ ∂τ a(τ ) = P (a(τ )), a(0) = v 0 .
Since P is locally Lipschitz, then a solution for (4.6) is unique and exists at least for small |τ |.

Lemma 4.1. The curve a 0 (τ ) is a solution of (4.6) for |τ | ≤ θ.

To prove the lemma we first perform some additional constructions. Assume for definiteness that τ ≥ 0, i.e. 0 ≤ τ ≤ θ, and consider an intermediate scale

L = √ ; then L 1. Denote N = [ θ L ]. Let b j = jL, 0 ≤ j ≤ N , b N +1 = θ and j = [b j-1 , b j ], 1 ≤ j ≤ N + 1. Then | 1 | = • • • = | N | = L, 0 ≤ | N +1 | < L.
Let the curves y t (a), t ∈ R, be defined as in (3.2) with a = a . Lemma 4.2. For any

0 ≤ |τ | ≤ θ, denote I(τ ) = τ 0 G(a (s), s -1 )ds, where G(a (s), s -1 ) = y s -1 (a (s))-P (a (s)). Then uniformly in τ ∈ [0, θ] we have |I(τ )| ≤ κ( ), where κ( ) → 0 as → 0, does not depend on v 0 if |v 0 | ≤ R. Proof. Denote I j (τ ) = j G(a (s), s -1 )ds, 1 ≤ j ≤ N + 1. Then |I| ≤ N +1 j=1 |I j |.
The term I N +1 is trivially small. Now consider I j with 1 ≤ j ≤ N . We have

|I j | ≤ bj bj-1 (G(a (s), s -1 ) -G(a (b j-1 ), s -1 ))ds + bj bj-1 G(a (b j-1 ), s -1 )ds =: I 1 j + I 2 j .
Consider the term

I 1 j . Since |s -b j-1 | ≤ L, then by (4.1), we have |a (s) -a (b j-1 )| ≤ LX(2R).
As for any t, y t and P both belong to Lip χ , then 2 . Now consider the term I 2 j . We have

I 1 j ≤ 2LX(2R) • LX(2R) = 2L 2 (X(2R))
I 2 j = bj bj-1 y s -1 (a (b j-1 ))ds - bj bj-1 P (a (b j-1 ))ds = bj-1+L bj-1 Φ Λ -1 τ • P (Φ -Λ -1 τ a (b j-1 ))dτ -L P (a (b j-1 )) = L 0 Φ Λ -1 bj-1 Φ Λ -1 τ • P (Φ -Λ -1 τ Φ -Λ -1 bj-1 a (b j-1 ))dτ -L P (a (b j-1 )) = Φ Λ -1 bj-1 L 0 Φ Λ -1 τ • P (Φ -Λ -1 τ z)dτ -L P (a (b j-1 )) ,
where z := Φ -Λ -1 bj-1 a (b j-1 ) ∈ B2R . Making in the last inequality the substitution -1 τ = t and noting that dτ = dt = L 2 dt, we obtain:

I 2 j = Φ Λ -1 bj-1 L L -1 L -1 0 Φ Λt • P (Φ -Λt z)dt -L P (a (b j-1 )) = LΦ Λ -1 bj-1 P L -1 (z) -L P (a (b j-1 )) .
From (4.5), P L -1 (z) = P (z) + o(1) as → 0. Since by item 3) of Proposition 3.7

P (z) = P (Φ -Λ -1 bj-1 a (b j-1 )) = Φ -Λ -1 bj-1 P (a (b j-1 )),
and as by Lemma 3.2 the o(1) above does not depend on z ∈ B2R , then

I 2 j = |L P (a (b j-1 )) + L • o(1) -L P (a (b j-1 ))| = L • o(1). So |I j | ≤ L • o(1) + 2L 2 (X(2R)) 2 = L • o(1)
, and therefore,

|I| ≤ N j=1 |I j | ≤ N L • o(1) ≤ θ • o(1) =: κ( ).
The lemma is proved. The term (4.7) → 0 as j → 0 in view of (4.2), the term (4.8)=0 by (4.4), the term (4.9)≤ κ( ) by Lemma 4.2 and (4.10)≤ τ X(2R)|a j -a 0 | → 0 as j → 0 by (4.2). Passing to the limit as j → 0, we see that A(τ ) ≡ 0. Therefore, a 0 (τ ) is a solution of (4.6) for 0 ≤ |τ | ≤ θ. Lemma 4.1 is proved.

Since a solution of eq. (4.4) is unique, then the convergence (4.2) holds as → 0, not only as j → 0. Thus we have proved

∂ ∂τ v = v 2 v.
In the real variables and the fast time the equation reads ẋ = x(x 2 + y 2 ), ẏ = y(x 2 + y 2 ).

For x 0 = 1, y 0 = 0 its solution is x(t) = (1 -2 t) -1/2 , y(t) = 0. So for |t| ≤ 1

4

-1 the solution of (2.6) with initial data (1, 0) satisfies

x 2 (t) + y 2 (t) 1/2 = (1 -2 t) -1/2 + o(1)
as → 0.

Hamiltonian equations

Let us provide the space R 2n ∼ C n with the usual symplectic structure, given by the form ω 2 = dx j ∧ dy j . Then a real-valued Hamiltonian

H = h 2 (z, z) + h(z, z), h 2 = - 1 2 λ j |z j | 2 , h ∈ C 1 (C n ),
gives rise to the Hamiltonian system żj = -iλ j z

j + 2i ∂h ∂ zj , 1 ≤ j ≤ n,
which we rewrite as Lemma 5.1. Let y t (a) be defined as in (3.2). Then

∂z ∂τ + i -1 diag(λ j )z = 2i ∂h ∂ z := P (z). (5.1) Assume that P is locally Lipschitz. It means that h ∈ C 1,1 loc = {u(z) ∈ C 1 (C n ) : u z ,
y t j (a) = 2i ∂ ∂ā j h(Φ -Λt a). Proof. Denote Φ -Λt a = v, i.e., v j = e -iλj t a j . Then 2i ∂h(v(a)) ∂ā j = 2i ∂h(v(a)) ∂v j • ∂v j ∂ā j = 2i ∂h(v(a))
∂v j e iλj t = 2ie iλj t ∂h(Φ -Λt a) ∂v j = e iλj t P j (Φ -Λt a) = y t j (a), since 2i ∂h ∂ vj = P j (v). From Lemma 5.1, (5.2)

P T j (a) = 2i |T | T 0 ∂ ∂ā j h(Φ -Λt a)dt = 2i ∂ ∂ā j h T (a),
where we denoted h T (a) = 1

|T |

T 0 h(Φ -Λt a)dt. For the same reason as in Section 3 (see there Lemma 3.2), since h is a locally Lipschitz function, then the limit

(5.3) lim T →±∞ h T (a) =: h (a)
exists and is locally Lipschitz (this limit is the averaging of the function h in the direction Λ).

Repeating the proof of Proposition 3.7.3) we get that h (a) is invariant with respect to the rotations Φ Λθ :

h (Φ Λθ a) = h (a) ∀θ, ∀a. (5.4)
We claim that h is a C 1 -function and (5.5) 2i ∂ ∂ā j h (a) = P j (a), for every j. Indeed, by the second assertion of Lemma 2.3 and (5.2)

P T j (a) = -2i ∂ ∂a j h T (a).
From here and (5.2) we conclude that h T is a C 1 function, and for each j the derivative (∂/∂x j ) h T is a complex linear combination of P T j and P T j . So by Lemma 3.1, for any bounded domain B in C n functions (∂/∂x j ) h T are uniformly in T > 0 bounded and Lipschitz on B. Same is true for (∂/∂y j ) h T , for all j. Now the uniform in B convergence of P T j to P j implies the uniform convergence of (∂/∂x j ) h T and (∂/∂y j ) h T to limits, for all j. In view of the uniform in B convergence of h T to h we get that h is C 1 -smooth and satisfies (5.5).

We have proved Theorem 5.2. If equation (2.5) has the hamiltonian form (5.1), where the real Hamiltonian h belongs to the space C 1,1 loc , then the effective equation (4.6) also is hamiltonian: the vector field P has the hamiltonian form (5.5), where the Hamiltonian h ∈ C 1,1 loc is defined in (5.3). Let us take any h ∈ C 1,1 loc and assume that the vector Λ is non-resonant, that is Λ • s = 0 for some s ∈ Z n implies that s = 0. Let us introduce in C n the action-angle coordinates (I, ϕ) with I ∈ R n + , ϕ ∈ T n , where for a vector z = (z 1 , . . . , z n ) with z j = r j e iϕj we have I = (I 1 , . . . , I n ), I j = 1 2 r2 j , and ϕ = (ϕ 1 , . . . , ϕ n ). Then ω 2 = dI ∧ dϕ, and Φ Λt (I, ϕ) = (I, ϕ + Λt).

Since now the curve t → ϕ + Λt is dense in T n for each ϕ, then (5.4) implies that h does not depend on the angles ϕ. 2 That is, the Hamiltonian h is integrable, and the effective equation reads İ = 0, φ = ∇ I h (I).

So its solutions a(τ ) are such that |a j (τ )| 2 = const, and Theorem 4. loc , then 2i∂ z h ∈ Lip X (C n , C n ) for a function X as in Definition 2.5. For m ∈ N we write 2i∂ z h(z) = O(z m ), if -m 2i∂ z h( z) ∈ Lip X (C n , C n ) for all 0 < ≤ 1, for a suitable function X, independent from . For example, if h is a polynomial (5.6) such that the coefficients m αβ are nonzero only for |α| + |β| ≥ M , then 2i∂ z h = O(z M -1 ). Consider the equation (5.7) ż + i diag(λ j )z = 2i∂ z h, where 2i∂ z h ∈ O(z m ). To study its small solutions we substitute z = w and get for w(t) equation ( 5.1) with := m-1 . We see that if the frequency vector Λ is non-resonant and z(t) is a solution of (5.7) with small initial data z(0) = w 0 , then |z j (t)| 2 -2 |w 0j | 2 = o( 2 ) for |t| ≤ 1-m θ, where θ = θ(|w 0 |). In [START_REF] Giorgilli | Effective stability for a Hamiltonian system near an elliptic equilibrium point, with an application to the restricted three-body problem[END_REF] a more delicate argument is used to show that if the frequency vector Λ satisfies certain diophantine condition and the Hamiltonian h is analytic, then the stability interval is much bigger -it is exponentially long in terms of -a for some positive a. Our result is significantly weaker, but it only requires that the vector Λ is nonresonant and the Hamiltonian vector-field 2i∂ z h is Lipschitz-continuous. We note that the result of [START_REF] Giorgilli | Effective stability for a Hamiltonian system near an elliptic equilibrium point, with an application to the restricted three-body problem[END_REF] generalises to PDEs, e.g. see [START_REF] Bambusi | An averaging theorem for quasilinear Hamiltonian PDEs[END_REF], as well as Theorem 1.1 (and Corollary 5.4), see [START_REF] Huang | An averaging theorem for nonlinear Schrödinger equations with small nonlinearities[END_REF][START_REF] Huang | Time-averaging for weakly nonlinear CGL equations with arbitrary potentials[END_REF].

  a)dt, (3.1) if the limit exists (for T < 0 we understand T 0 . . . dt as the integral 0 T . . . dt). Denote y t (a) = Φ Λt • P (Φ -Λt a), (3.2) and for T = 0 set P T (a)

4 ,

 4 ∀| T | ≥ T . From (3.10) and (3.11),

3. 1 .Proposition 3 . 7 .

 137 Properties of the operator • . Let P and Q be locally Lipschitz vector-fields on C n . Then 1) (linearity): aP + bQ = a P + b Q for any a, b ∈ R.

Proof of Lemma 4 . 1 . 0 P 0 P 0 P 0 P

 410000 Consider A(τ ) := a 0 (τ ) -v 0 -τ (a 0 (s))ds = a 0 (τ ) -a j (τ ) (4.7) + a j (τ ) -v 0 -τ 0 y(a j (τ ), s -1 j )ds (4.8) + τ 0 y(a j (τ ), s -1 j )ds -τ (a j (s))ds (4.9) + τ (a j (s))ds -τ (a 0 (s))ds.(4.10)

Theorem 4 . 3 .Corollary 4 . 4 .Example 4 . 5 .

 434445 Let a (τ ), |τ | ≤ θ, be a solution of (4.4). Then a (τ ) → a 0 (τ ), uniformly for |τ | ≤ θ, where a 0 (τ ) is a solution of (4.6). Theorem 4.3 proves the second assertion of Theorem 1.1, whose first assertion was already established in Lemma 3.2. Since |v j (τ )| ≡ |a j (τ )|, then Theorem 4.3 implies: The solution v (t) of (2.5) satisfies sup |t|≤ -1 θ |v j (t)| -|a 0 j ( t)| → 0 as → 0, ∀j. By Examples 2.4 and 3.4, the effective equation for the system (2.6), written in the complex variable v and the slow time τ , is

  u z are locally Lipschitz functions}. Then (5.1) is a special case of equation (2.11).

Example 5 . 3 .

 53 If h is a real polynomial, (5.6) h(a) = α,β∈Z n + m αβ a α āβ , m αβ = m αβ , then h (a) = Λ•α=Λ•β m αβ a α āβ .

3 implies Corollary 5 . 4 .

 54 If the frequency vector Λ is non-resonant and h ∈ C 1,1 loc , then a solution z(t) of equation (5.1) satisfies sup |t|≤ -1 θ |z j (t)| 2 -|z j0 | 2 = o(1) as → 0, for a suitable θ which depends on |z 0 |. If h ∈ C 1,1

For example, if h is the polynomial (5.6), then h (a) = mααa α āα .


Ugo Dal Lago

Francesco Gavazzo

On Bisimilarity in Lambda Calculi with Continuous Probabilistic Choice

Applicative bisimiliarity is a coinductively-de ned program equivalence in which programs are tested as argument-passing processes. Starting with the seminal work by Abramsky, applicative bisimiliarity has been proved to be a powerful technique for higher-order program equivalence. Recently, applicative bisimiliarity has also been generalised to lambda calculi with algebraic e ects, and with discrete probabilistic choice in particular. In this paper, we show that applicative bisimiliarity behaves well in a lambda-calculus in which probabilistic choice is available in a more general form, namely through an operator for sampling of values from continuous distributions. Our main result shows that applicative bisimilarity is sound for contextual equivalence, hence providing a new reasoning principle for higher-order probabilistic languages.

Introduction

Program equivalence and re nement are central concepts in program semantics: giving meaning to programs has the positive e ect of allowing one to compare programs and to dub them equivalent whenever having the same semantics. But what comes rst, the chicken or the egg? After all, any equivalence relation between program phrases implicitly gives meaning to a program through their equivalence class.

Among the many possible notions of program equivalence, Morris' style contextual equivalence [START_REF] Morris | Lambda calculus models of programming languages[END_REF] has been considered as somehow canonical, being the largest, and thus coarsest, adequate and compatible relation between programs: by construction, one cannot do any better than that when trying to identify programs behaving the same. As such, contextual equivalence is accepted as the reference notion of equivalence in an higher-order scenario. When proving that two programs are actually equivalent, however, the universal quanti cation over all contexts (i.e. over all program environments) in the de nition of contextual equivalence makes the proof burdensome, if not impossible.

This has stimulated the development of alternative techniques for program equivalence which, in one way or another, get rid of the aforementioned universal quanti cation. Examples are logical relations G. [START_REF] Plotkin | Lambda-de nability and logical relations[END_REF]; [START_REF] Reynolds | Types, abstraction and parametric polymorphism[END_REF]; [START_REF] Sieber | Reasoning about sequential functions via logical relations[END_REF], applicative bisimilarity [START_REF] Abramsky | The lazy lambda calculus[END_REF], and denotational semantics [START_REF] Scott | Outline of a mathematical theory of computation[END_REF]; [START_REF] Scott | Toward a mathematical semantics for computer languages[END_REF]. Traditionally, the rst step in studying the nature of these notions of program equivalence consists, again, in proving compatibility and adequacy, from which inclusion in contextual equivalence easily follows. In some cases this comes more or less by de nition, while in other cases, like the one of applicative bisimilarity, proofs of compatibility are nontrivial, and are typically carried out in indirect ways, by methodologies like the so-called Howe's method [START_REF] Howe | Proving congruence of bisimulation in functional programming languages[END_REF]. Starting from Abramsky's pioneering work on applicative bisimilarity [START_REF] Abramsky | The lazy lambda calculus[END_REF], coinduction has been proved to be a useful methodology for program equivalence in the context of pure λ-calculi.

All these (and others) techniques, give purely functional programming languages a clean semantics which makes it relatively easy to reason about them. Injecting various forms of e ects (such as I/O, exceptions, or nondeterminism) complicates the matter considerably. Some of the aforementioned techniques for program equivalence have been proved to be remarkably robust in this respect, with contributions ranging from extensions encompassing speci c notions of e ect [START_REF] Bizjak | Step-indexed logical relations probability[END_REF]; Dal [START_REF] Dal Lago | On coinductive equivalences for higher-order probabilistic functional programs[END_REF]; De [START_REF] De Liguoro | Non deterministic extensions of untyped lambda-calculus[END_REF]; [START_REF] Jones | Probabilistic non-determinism[END_REF]; S. [START_REF] Lassen | Relational reasoning about functions and nondeterminism[END_REF] to more abstract notions in which e ects of a certain kind (e.g. algebraic e ects G. D. [START_REF] Plotkin | Lambda-de nability and logical relations[END_REF]Power (2001, 2002)) are proved to work well in a given semantic framework [START_REF] Biernacki | Handle with care: relational interpretation of algebraic e ects and handlers[END_REF]; [START_REF] Dal Lago | E ectful applicative bisimilarity: Monads, relators, and howe's method[END_REF]; [START_REF] Goubault-Larrecq | Logical relations for monadic types[END_REF] ;[START_REF] Johann | A generic operational metatheory for algebraic e ects[END_REF]; [START_REF] Simpson | Behavioural equivalence via modalities for algebraic e ects[END_REF].

One kind of e ect which has received a lot of attention recently [START_REF] Staton | Commutative semantics for probabilistic programming[END_REF], but whose impact to the traditional techniques for program equivalence has been studied only marginally, is continuous probabilistic choice, i.e. the operation of sampling from continuous distributions. This by itself poses a challenge to the de nition of an operational semantics, and thus to operationally-based techniques. Concerning the latter, the only contributions the authors are aware of are those by [START_REF] Culpepper | Contextual equivalence for probabilistic programs with continuous random variables and scoring[END_REF]; [START_REF] Wand | Contextual equivalence for a probabilistic language with continuous random variables and recursion[END_REF] on logical relations for a probabilistic λ-calculus with continuous distributions and scoring.

In this paper, we show that applicative (bi)simulation remains a sound methodology for program equivalence and re nement in presence of sampling from continuous distributions. We do it for a λ-calculus endowed with a very liberal recursive type system.

Noticeably, probabilistic bisimulation has been rst de ned in the abstract setting of discrete probabilistic transition systems, also known as labelled Markov chains [START_REF] Larsen | Bisimulation through probabilistic testing[END_REF], and later generalised to Markov decision processes [START_REF] Blute | Bisimulation for labelled markov processes[END_REF]. The main technical di culty one faces when trying to turn probabilistic bisimulation into a notion of equivalence for higher-order programs consists in coming up with a sensible notion of lifting, allowing to turn a relation between programs into a relation between program (sub)distributions [START_REF] Panangaden | Probabilistic bisimulation[END_REF]: there is a fundamental tension between the properties one typically gets from the aforementioned abstract notions of bisimilarity, and those one needs in the proofs of congruence. This paper shows that there is indeed a point in which the two meet.

The rest of the paper is organised as follows. We begin our analysis with an example of a simple program transformation. Proving correctness of such a transformation, however, is nontrivial and requires the design of suitable operational techniques. We then introduce our main vehicle calculus, namely a probabilistic callby-value λ-calculus with sum and recursive types (Section 2), as well as its operational semantics (Section 2). Section 4 introduces the relational calculus we will use to study notions of program equivalence and re nement. We instantiate such a framework to de ne contextual equivalence and approximation (Section 5), and applicative (bi)simulation (Section 6). We prove soundness of applicative (bi)similarity in Section 6. We conclude this paper with a short discussion on full abstraction (Section 7).

Warming Up

Before entering into the technicalities of our anlaysis, we discuss a simple, yet nontrivial example of program equivalence in presence of continuous distributions. This way, we also introduce some features of the languages we are going to study.

We consider higher-order functional languages enriched with primitives for real-valued (measurable) functions and for sampling from continuous (and discrete) distributions. For instance, the program normal µ σ samples a real number from the normal distribution with mean (encoded by the numeral) µ and standard deviation σ . Similarly, we can write a program poisson µ which samples a real number from the Poisson distribution with rate µ.

We can also take advantage of the higher-order nature of functional languages, and use arbitrary programs e µ , e σ to compute the mean and standard deviation of the normal distribution:

let x µ = e µ in (let x σ = e σ in (normal x µ x 2 σ )).
Notice that e µ , e σ may be de ned sampling from other distributions as in:

let x µ = (poisson e λ 1 ) in (let x σ = (poisson e λ 2 ) in (normal x µ x 2 σ )).
This immediately raises the question of whether the order in which we evaluate (independent) expressions matter. That is, we ask whether the equivalence

let x 1 = e 1 in (let x 2 = e 2 in e 3 ) ≡ let x 2 = e 2 in (let x 1 = e 1 in e 3 )
holds, assuming the variable x 1 not to be free in e 2 , and similarity for x 2 and e 1 . Such an equivalence is known as commutativity, and has been studied in [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] by means of denotational methods, and in [START_REF] Culpepper | Contextual equivalence for probabilistic programs with continuous random variables and scoring[END_REF]; [START_REF] Wand | Contextual equivalence for a probabilistic language with continuous random variables and recursion[END_REF] by means of logical relations (in both cases, however, the target language also includes primitives for conditioning).

Let us now look at a more sophisticated example. Consider the following instances of the combinators map append, and zipwith:

map : (unit → real) → list (unit) → list (real) append : list (real) → list (real) → list (real) zipwith : (real → real) → list (real) → list (real) → list (real)
where map is the usual combinator for mapping functions on lists, append is the usual function for appending lists, and zipwith is a combinator taking as input a binary operation and two lists (which, for the sake of the argument, we assume to have the same length), and returning the list obtained by the pointwise application of the operation to the elements occurring at the same position in both lists. Let now zs be a list of n elements of type unit (we use zs to generate lists of random numbers), and let us write λ.e : unit → real for the thunk of a program e : real. Proving the correctness of the above transformation requires to combine denotational reasoning about probability measures with operational reasoning about program behaviour. On the one hand, the two programs above are values, so that looking at their computational behaviour in isolation is useless: in order to understand what these programs do we have to test them against any possible input the environment can pass them (which might have a probabilistic behaviour itself). On the other hand, such programs are somehow related by basic results in statistics (notably, given random variables with normal probability distribution

X 1 ∼ N (µ 1 , σ 2 1 ) and X 2 ∼ N (µ 2 , σ 2 2 ), we have X 1 + X 2 ∼ N (µ 1 + µ 2 , σ 2 1 + σ 2 2 )
). As we will see, the techniques we develop in this paper give a handy proof of correctness of the above program transformation.

Now that the reader has some insights on the kind of problems we aim to solve in this work, we can start our formal analysis of program equivalence and re nement.

A Calculus with Continuous Probabilities: Syntax

The target language of this work is a probabilistic ne-grain call-by-value [START_REF] Levy | Modelling environments in call-by-value programming languages[END_REF] with nite sums and recursive types reminiscent of probabilistic PCF Ehrhard, Pagani, and Tasson (2018); [START_REF] Park | A probabilistic language based upon sampling functions[END_REF]. The syntax and static semantics of Λ P is de ned in Figure 1.

Types of Λ P are built starting from a countable set of type variables (denoted by the letter α in Figure 1) and the basic type real for real numbers, using nite sum, arrow, and recursive type constructors. In particular, in a type of the form i ∈I τ i we assume the letter I to stand for a nite set whose elements are denoted by î, , . . .. We write void and unit for the empty sum type and void → void, respectively.

Terms of Λ P are divided in two classes: values and expressions (also called computations). Intuitively, a value is the result of a computation, whereas an expression is a value producer, i.e. a term that once evaluated may produce a value (the evaluation process might not terminate) as well as side e ects (the latter being probabilistic). Accordingly, computations must be explicitly sequenced by means of the sequencing constructor let x =in -.

We use judgments of the form Γ Λ e : τ for expressions, and Γ V : τ for values. In a judgment of the form Γ Λ e : τ (resp. Γ V : τ ), Γ denotes an environment, i.e. a nite sequence x 1 : τ 1 , . . . , x n : τ n of distinct variables with associated closed types (we denote by • the empty environment), τ is a closed type, and e (resp. ) is an expression (resp. value) with free variables among Γ. Notice that we work with closed types only. We use the letter e (possibly with sup-and subscripts) to denote expressions, and (possibly with supand subscripts) to denote values. We also refer to sequents Γ Λ τ as computation or expression sequents, and to Γ V τ as value sequents. When the distinction between values and expressions is not relevant, we generically refer to terms.

Each real number r is represented in Λ P by the value r. Additionally, Λ P is parametric with respect to a N-indexed family C of countable sets C n , each of which contains (symbols for) measurable functions from R n to R. In particular, we assume standard real-valued arithmetic operations to be in C. We use letters F , G, . . . to denote elements in C n . Notice that a function F ∈ C n has values as arguments, rather than expressions. Indeed, we can encode the expression F (e 1 , . . . , e n ) as1 let

x 1 = e 1 in (let x 2 = e 2 in . . . (let x n = e n in F (x 1 , . . . , x n ))).
Finally, the expression sample stands for the uniform distribution over the unit interval, which is nothing but the Lebesgue measure λ on [0, 1]. As it is shown in e.g. [START_REF] Ehrhard | Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming[END_REF]; [START_REF] Park | A probabilistic language based upon sampling functions[END_REF], starting from sample it is possible to de ne several probabilistic measures (e.g. binomial, geometric, and exponential distribution) using functions in C.

Example 1. Given closed terms e µ , e σ of type real (encoding mean µ and standard deviation σ ) we represent the normal distribution with mean µ and standard deviation σ as the Λ P expression normal e µ e σ , where the term normal std encodes the normal distribution with mean 0 and standard deviation 1. Notice that the expressions e µ , e σ may be themselves de ned in terms of other distributions:

normal std let x = sample in (let = sample in ( -2 log(x ) cos(2π ))) normal e µ e σ let x µ = e µ , x σ = e σ , = normal std in ((x σ * ) + x µ ).
We adopt the standard syntactical conventions as in [START_REF] Barendregt | The lambda calculus: its syntax and semantics[END_REF], notably the so-called variable convention. In particular, we denote by FV (e) (resp. FV ( )) the collection of free variables of e (resp. ) (notice that, e.g., in a term of the form case of {fold x → e} the variable x is bound in e). We refer to closed expressions as programs. We denote by e[ /x] (resp. [ /x]) the capture-free substitution of the value for all free occurrences of x in e (resp. ) and identify terms up to renaming of bound variables. We extend the aforementioned conventions to types. For instance, we denote by τ 1 [τ 2 /α] the result of capture-avoiding substitution of the type τ 2 for the type variable α in τ 1 . Finally, we use the notation Λ and V to denote the collections of all typable expressions and values, respectively.

A Calculus with Continuous Probabilities: Semantics

The dynamic semantics of Λ P is given by a type-indexed family of evaluation functionsτ mapping programs of type τ to sub-probability measures over values of type τ . The collection of such measures can be abstractly described using the sub-Giry monad G [START_REF] Giry | A categorical approach to probability theory[END_REF], so that the evaluation functionτ will map a program e ∈ Λ τ to a sub-probability measure e τ ∈ G(V τ ). Additionally, since GX carries a measurable space structure whenever X does, we would likeτ to be a measurable function. For that to make sense, however, we rst need to make Λ a measurable space itself. We follow [START_REF] Ehrhard | Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming[END_REF]; [START_REF] Sangiorgi | Environmental bisimulations for higher-order languages[END_REF]; [START_REF] Staton | Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints[END_REF] and rely on the measurable space structure of R n and coproducts in Meas, the category of measurable spaces2 . Before entering into the details we recall some useful mathematical preliminaries.

Mathematical Preliminaries: Stochastic Kernels and the Giry Monad

In this section we recall some mathematical preliminaries which are needed in order to give Λ P dynamic semantics. Unfortunately, there is no hope to be comprehensive, and thus we assume the reader to be familiar with basic measure theory [START_REF] Pollard | A user's guide to measure theoretic probability[END_REF], domain theory [START_REF] Abramsky | Domain theory[END_REF], and category theory [START_REF] Maclane | Categories for the working mathematician[END_REF].

We denote by Meas the category of measurable spaces and measurable functions, by Set the category of sets and functions, and by ωCppo the category of ω-cppo and continuous functions. Given a measurable space (X , Σ X ) with a measure µ on it and a function f : X → [0, ∞], we denote by X f dµ or X f (x )µ (dx ) the number in [0, ∞] obtained by Lebesgue integrating f over X with respect to µ (when clear from the context, we will omit the subscript X ).

In order to deal with nontermination, we work with sub-probability distributions rather than with full distributions. For instance, the measure Ω associated to the purely divergent expression Ω will naturally assign 0 to any measurable sets of values. Mathematically, this means working with the sub-Giry monad rather than with the (full) Giry monad.

De ntion 1. The sub-Giry functor G : Meas → Meas maps a measurable space (X , Σ X ) to (GX , Σ GX ), where GX is the set of all sub-probability measures on X , and Σ GX is the least σ -algebra making the Σ Xindexed family of maps eval

A : G(X ) → [0, 1], de ned by eval A (ν ) = ν (A), measurable. Measurable functions f : X → Y are mapped to G f : GX → GY , where (G f )(ν ) ∈ GX = ν ( f -1 (-)).
The functor G carries a monad structure, with unit η X : X → GX given by Dirac measures (recall that for any x ∈ X , the Dirac measure δ x on X is de ned as δ x (A) = 1 if x ∈ A, and δ x (A) = 0, otherwise), and multiplication µ X : GGX → GX de ned as µ

X (M )(A) = GX eval A (x )M (dx ), for A ∈ Σ X . Equivalently, we can use G to build a Kleisli triple MacLane (1971) de ning 3 f † (ν )(B) = f (x )(B)ν (dx ), for f : X → GY .
Actually, Fubini's Theorem implies that G has the structure of a commutative monad, with double strength dst X ,Y : GX × GY → G(X × Y ) mapping measures µ ∈ GX , ν ∈ GY to their product measure µ ⊗ ν .

A measurable function f : X → GY is also called a (stochastic) kernel Panangaden (1999) from X to Y , as we can uncurry f obtaining a map f : X × Σ Y → [0, 1]. We write Kern for the Kleisli category of G. The category Kern enjoys several nice properties [START_REF] Panangaden | The category of markov kernels[END_REF]. In particular, the collection of measurable functions from X to GY carries an ω-cppo structure under the pointwise order (i.e. f if and only if ∀x ∈ X . ∀A ∈ Σ Y . f (x )(A) ≤ (x )(A)). The bottom element ⊥ is de ned as the always zero distribution, whereas the least upper bound of an ω-chain ( f n ) n ≥0 is de ned as sup n f n . Additionally, the monotone convergence theorem and the very de nition of Lebesgue integration give the following identities: sup n f n dν = sup n f n dν , f d (sup n ν n ) = sup n f dν n . Abstractly, this means that Kern is ωCppoenriched [START_REF] Kelly | Basic concepts of enriched category theory[END_REF]. Finally, we recall that Meas is cartesian (although not cartesian closed) and that Kern has countable coproducts. For a countable family (X i , Σ X i ) of measurable spaces we denote by i (X i , Σ X i ) its coproduct.

Evaluation Semantics

We de ne a (type-indexed) mapτ : Λ τ → G(V τ ) associating to each program e ∈ Λ τ a (sub)probability measure over values in V τ . We rely on the ωCppo-enrichment of Kern to deal with non-termination.

De ntion 2. De ne the type-indexed family of (N-indexed) maps - (n) τ : Λ τ → G(V τ ) as follows (for readability, we omit type annotations in - (n) ):

e (0) (A) = 0 (n+1) (A) = δ (A) F (r 1 , . . . , r n ) (n+1) (A) = F(r 1 , . . . , r n ) (n) (A) sample (n+1) (A) = λ{r | r ∈ A} (λx.e) (n+1) (A) = e[ /x] (n) (A) let x = e 1 in e 2 (n+1) (A) = e 2 [ /x] (n) e 1 (n) (d ) case î, of { i, x → e i } (n+1) (A) = e î [ /x] (n) (A) case (fold ) of {fold x → e} (n+1) (A) = e[ /x] (n) (A).
Lemma 1. For any type τ and natural number n, the map - (n) τ is a kernel.

Sketch. First of all, we notice that for the statement of Lemma 1 to make sense, we rst need to make Λ τ (as well as V τ ) a measurable space. This can be done as in [START_REF] Ehrhard | Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming[END_REF]; [START_REF] Staton | Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints[END_REF], taking advantages of coproducts in Meas. By observing that for any expression Γ, x : τ 1 Λ e : τ 2 , the map e[-/x] :

V Γ τ 1 → Λ Γ τ 2 is measurable, one can easily show -(n) to be measurable.
Additionally, we see that e (n) τ is actually an ω-chain in G(V τ ), so that we can de ne e τ as sup n e (n) τ . In particular, due to ωCppo-enrichment of Kern, we can replace all the occurrences of - (n) in De nition 2 with -. As usual, where possible we omit type subscripts in -.

Having de ned the operational behaviour of programs, we can nally move to the study of notions of program equivalence and re nement.

Probabilistic Equivalence and Re nement

In the next sections we de ne notions of program equivalence and re nement for Λ P . Speci cally, we introduce (probabilistic) contextual equivalence and approximation, and (probabilistic) applicative (bi)similarity. Our main result states that applicative similarity (resp. bisimilarity) is a sound proof technique for contextual approximation (resp. equivalence).

Studying notions of program equivalence and re nement, it is useful to x a proper notation and vocabulary for program relations. We do so following [START_REF] Gordon | A tutorial on co-induction and functional programming[END_REF]; S. [START_REF] Lassen | Relational reasoning about functions and nondeterminism[END_REF].

Relational Calculus

We use letter R, S, . . . to range over relations and write Rel(X , Y ) for the set of relations over X and Y . We call elements of Rel(X , X ) endorelations. Given a relation R ⊆ X ×Y and set A ⊆ X , we denote by R

[A] the R-image of A, i.e. { ∈ Y | ∃x ∈ A. (x, ) ∈ R}. For relations R ⊆ X × Y , S ⊆ Y × Z ,
we write S • R for their composition, and denote by = X the equality relation on X . As usual, an endorelation

R ∈ Rel(X , X ) is re exive if = X ⊆ R, transitive if R • R ⊆ R,
and symmetric if R ⊆ R, where R denotes the converse or transpose of R. We also recall that Rel(X , X ) carries a complete lattice structure with order given by set-theoretic inclusion.

Relational reasoning about programs oftentimes require to reason about open terms. It is thus useful to work with families of relations relating expressions typable within the same sequent. We refer to such (families of) relations as term relations.

De ntion 3. A term relation R associates to each computation sequent Γ Λ τ (resp. value sequent Γ V τ ) a relation Γ Λ -R -: τ (resp. Γ V -R -: τ ) between its inhabitants.
Formally, a term relation is thus an element in the set

Rel = Γ τ Rel(Λ Γ τ , Λ Γ τ ) × Rel(V Γ τ , V Γ τ ).
The latter inherits a complete lattice structure from Rel(Λ Γ τ , Λ Γ τ ) and Rel(V Γ τ , V Γ τ ) pointwise, this way allowing one to de ne term relations both inductively and coinductively. Concerning notation, we write R ⊆ S if:

∀Γ, e 1 , e 2 . Γ Λ e 1 R e 2 =⇒ Γ Λ e 1 S e 2 , ∀Γ, 1 , 2 . Γ V 1 R 2 =⇒ Γ V 1 S 2 .
Example 2. The identity term relation is de ned by the (0-ary) rules: Γ Λ e = Λ e : τ , Γ V = V : τ . Given term relations R, S, we de ne S • R as follows:

Γ Λ e 1 R e 2 : τ Γ Λ e 2 S e 3 : τ Γ Λ e 1 (S • R) e 3 : τ Γ V 1 R 2 : τ Γ V 2 S 3 : τ Γ V 1 (S • R) 3 : τ
The notions of a preorder and equivalence term relation are de ned as usual. In fact, we say that a term relation R is re exive if = ⊆ R, transitive if R • R ⊆ R, and symmetric if R ⊆ R (where R is de ned in the obvious way).

Oftentimes we will be interested in de ning relations between programs only. We denote by Rel 0 the subspace τ Rel(Λ τ , Λ τ ) × Rel(V τ , V τ ) of Rel, and refer to its elements as closed term relations. Every closed term relation R ∈ Rel 0 induces a term relation, called the open extension of R, as follows: given Γ Λ e : τ , let γ range over closed substitutions for Γ (i.e. for any variable (x i :

τ i ) ∈ Γ, γ (x i ) ∈ V τ i ). De ne: Γ Λ e 1 R e 2 : τ ⇐⇒ ∀γ . • Λ e 1 γ R e 2 γ : τ .
A similar de nition can be given for values. Given a closed term relation R, we sometimes write (R Λ , R V ) to denote the (type-indexed families of) relations de ning its action on expressions and values.

We tacitly require term relations to be closed under weakening, meaning that the following hold.

Γ Λ e 1 R e 2 : τ Γ, x : τ Λ e 1 R e 2 : τ

Γ V 1 R 2 : τ Γ, x : τ V 1 R 2 : τ
Notice that the open extension of a closed relation is indeed closed under weakening.

In order to formalise compositional reasoning about program behaviour, we introduce the notion of a compatible term relation, i.e. of a term relation closed under term constructors of Λ P .

De ntion 4. Given a term relation R, its compatible re nement R is de ned by the rules in Figure 2 In particular, a term relation is compatible if and only if it is a pre-xed point of -. It is not hard to prove that the identity term relation of Example 2 is a pre-xed point of -, and actually the least such. As a consequence, any compatible relation is re exive.

. A term relation R is compatible if R ⊆ R, and a closed term relation is compatible if its open extension is. Λ e i R e i : τ (∀i ∈ I ) Γ Λ case of { i, x → e i } R case of { i, x → e i } : τ Γ V R V : µα.τ 1 Γ, x : τ 1 [µα.τ 1 /α] Λ e R e : τ 2 Γ Λ case of {fold x → e} R case of {fold x → e } : τ 2
Lemma 2. The collection of compatible λ-term relations ordered by ⊆ has a complete lattice .

Lemma 2 allows us to de ne compatible λ-term relations both inductively and coinductively. Another central notion dealing with term relation is the one of substitutivity.

De ntion 5.

1. A term relation R is value-substitutive if the following hold:

Γ, x : τ 1 Λ e 1 R e 2 : τ 2 • V : τ 1 Γ Λ e 1 [ /x] R e 2 [ /x] : τ 2 Γ, x : τ 1 V 1 R 2 • V : τ 1 Γ V 1 [ /x] R 2 [ /x] : τ 2 2. A term relation R is substitutive if the following hold: Γ, x : τ 1 Λ e 1 R e 2 : τ 2 • V 1 R 2 : τ 1 Γ Λ e 1 [ 1 /x] R e 2 [ 2 /x] : τ 2 Γ, x : τ 1 V u 1 R u 2 : τ 2 • V 1 R 2 : τ 1 Γ V u 1 [ 1 /x] R u 2 [ 2 /x] : τ 2 A closed relation is (value) substitutive if
its open extension is. Moreover, we notice that the open extension of a closed term relation is trivially value-substitutive.

Contextual Approximation and Equivalence

Contextual equivalence [START_REF] Morris | Lambda calculus models of programming languages[END_REF] equates programs that behave the same in any possible environment. The notion of an environment is formalised by means of contexts, which are, roughly speaking, terms with a hole to be lled in with the program we aim to test. In order to avoid syntactic bureaucracy, we follow [START_REF] Gordon | A tutorial on co-induction and functional programming[END_REF]; S. [START_REF] Lassen | Relational reasoning about functions and nondeterminism[END_REF] and give a property-based de nition of contextual equivalence and approximation based on the notion of (pre)adequacy. For readability, from now on we write R for V real ∈ Σ real .

De ntion 6. Given a term relation R, we say that R is preadequate (resp. adequate) if:

• Λ e 1 R e 2 : real =⇒ e 1 (R) ≤ e 2 (R);

(resp. • Λ e 1 R e 2 : real =⇒ e 1 (R) = e 2 (R)).

De ntion 7. Contextual approximation ctx (resp. contextual equivalence ctx ) is the largest compatible and preadequate (resp. adequate) term relation.

De nition 7 is not well-posed, as it is not clear whether such largest term relations exist. In fact, (pre)adequacy is not a monotone property, meaning that we cannot de ne ctx (resp. ctx ) as the greatest xed point of the (non-monotone) endofuction on Rel induced by De nition 7. Nonetheless, we see that the the union of compatible (pre)adequate term relations is itself a compatible (pre)adequate term relation.

Additionally, De nition 7 gives a proof principle for contextual approximation (resp. equivalence) resembling a coinduction proof principle. In order to prove that a term relation R is included in ctx (resp. ctx ), it is su cient to show that R is preadequate (resp. adequate) and compatible. Using such a proof principle it is a straightforward exercise to prove that ctx is a precongruence and that ctx is a congruence term relation.

Example 3. Contextual equivalence gives the structural equalities in Figure 3, as well the quasi-denotational law: ∀e 1 , e 2 ∈ Λ τ . e 1 = e 2 =⇒ • Λ e 1 ctx e 2 : τ . The quasi-denotational law can be used to export powerful results from measure theory, for instance (we slightly abuse notation by desequencing some computations):

let x 1 = (normal e µ 1 e 2 σ 1 in (let x 2 = (normal e µ 2 e 2 σ 2 ) in (x 1 + x 2 )) ctx normal (e µ 1 + e µ 2 ) (e 2 σ 1 + e 2 σ 2 )
Combining such laws with the structural equivalences in Figure 3 we can prove non-trivial program equivalences. For instance, recalling the program transformation studied in Section 1.1, we see that contextual equivalence gives correctness of the following program transformation, which avoid a list traversing.

let xs = map (λ. normal e µ 1 e 2 σ 1 ) zs s = map (λ. normal e µ 2 e 2 σ 2 ) zs in append x (zipwith (+) xs s) ctx let xs = map (λ. normal (e µ 1 + e µ 2 ) (e 2 σ 1 + e 2 σ 2 )) zs in append x xs
Similarly, we can prove the correctness of the program transformation studied in Section 1.1. Proving such equivalences and laws from rst principles, however, is highly non-trivial. We will obtain these results relying on our notion of applicative bisimulation. 6 Applicative (Bi)simulation

Abramsky's applicative bisimilarity [START_REF] Abramsky | The lazy lambda calculus[END_REF] tests programs as argument-passing processes, i.e. by allowing the environment to interact with a program by passing it arbitrary inputs only. In a probabilistic setting, however, the result of a program is not a value, but a subdistribution of values, meaning that we have to re ne the conceptual apparatus behind applicative bisimilarity to take into account probabilistic behaviours. Following [START_REF] Hughes | Simulations in coalgebra[END_REF]; [START_REF] Levy | Similarity quotients as nal coalgebras[END_REF]; [START_REF] Thijs | Simulation and xpoint semantics[END_REF], we look at notions of (bi)simulation in terms of relation lifting operations. Suppose we are given a term relation R such that Λ e 1 R e 2 . How should we relate e 1 , e 2 ∈ GV τ ? Answering such a question means nothing more than nding a proper way to lift R V to GV τ × GV τ .

Probabilistic Relation Lifting

From an abstract perspective, what we need in order to de ne applicative (bi)similarity is to nd a lifting from Rel(X , Y ) to Rel(GX , GY ). The literature on probabilistic equivalence abounds of such notions of lifting (the interested reader can consult [START_REF] Panangaden | Probabilistic bisimulation[END_REF] for an overview, and [START_REF] Katsumata | Codensity lifting of monads and its dual[END_REF] for a more technical treatment). For our purposes, the kind of lifting we are in is one that allows applicative (bi)similarity: 1. To be de nable by coinduction; 2. To be a preorder (resp. equivalence) term relation; 3. To be a compatible and (pre)adequate term relation, and thus a sound proof technique for contextual approximation/equivalence.

The collection of notions of lifting satisfying these requirements has been identi ed in Dal [START_REF] Dal Lago | E ectful applicative bisimilarity: Monads, relators, and howe's method[END_REF] with the one of relators or lax extension [START_REF] Barr | Relational algebras[END_REF]; [START_REF] Thijs | Simulation and xpoint semantics[END_REF].

Unfortunately, nding non-trivial relators for the Giry monad has been proved to be extremely di cult, as the latter lacks some fundamental structural properties (notably, it does not preserve weak pullbacks Panangaden ( 2011)). Nonetheless, as rst argued in [START_REF] Van Breugel | Domain theory, testing and simulation for labelled markov processes[END_REF], restricting the attention from arbitrary binary relations to re exive endorelations allows one to de ne well-behaved notions of relation lifting for G.

At this point it is instructive to recall the standard notion of relation lifting proposed for G (see, e.g., [START_REF] Katsumata | Codensity lifting of monads and its dual[END_REF]), and the kind of problems one faces when working with it. We also remark that the notions of lifting we are going to analyse are actually meant to model notions of program re nement, rather than equivalence. In fact, applicative bisimilarity can be de ned in terms of applicative similarity, and compatibility of the former follows from compatibility of the latter.

De ntion 8. Given measurable spaces (X , Σ X ), (Y , Σ Y ), and a relation R ⊆ X × Y between them, we de ne ΓR ⊆ GX × GY as follows:

ΓR = {(ν 1 , ν 2 ) | ∀A ∈ Σ X . ∀B ∈ Σ Y . R [A] ⊆ B =⇒ ν 1 (A) ≤ ν 2 (B)}.
The map Γ : Rel(X , Y ) → Rel(GX , GY ) satis es many interesting properties (see e.g. [START_REF] Katsumata | Codensity lifting of monads and its dual[END_REF]), but fails to satisfy the inclusion ΓS • ΓR ⊆ Γ(S • R), which we refer to as quasi transitivity. Quasi transitivity ensures applicative similarity to be transitive. Most importantly, it is a central ingredient in Howe's method [START_REF] Howe | Proving congruence of bisimulation in functional programming languages[END_REF]; [START_REF] Pitts | Howe's method for higher-order languages[END_REF], the standard technique used to prove applicative (bi)similarity to be compatible.

A counterexample to quasi transitivity of Γ is given in Katsumata et al. (2018) (Example 4.15), taking advantage of the sets X and Y to be distinct (notably, taking X and Y to be the discrete and indiscrete space over the two-elements set, respectively). However, as we are interested in term relations, we can look at endorelations only. Moreover, as observed in [START_REF] Van Breugel | Domain theory, testing and simulation for labelled markov processes[END_REF], working with re exive endorelations (which still form a complete lattice), it is possible to re ne Γ in such a way to guarantee quasi transitivity.

De ntion 9. Given a measurable space (X , Σ X ), and a re exive relation R ⊆ X × X , de ne ΓR ⊆ GX × GX as follows4 :

ΓR = {(ν 1 , ν 2 ) | ∀A ∈ Σ X . R [A] ⊆ A =⇒ ν 1 (A) ≤ ν 2 (A)}.
Lemma 3. Let Rel = (X , X ) denote the complete lattice of endorelations on X . Then Γ : Rel = (X , X ) → Rel = (GX , GX ) satis es the following properties, for all R, S ∈ Rel = (X , X ).

= GX ⊆ Γ(= X ) (quasi re exivity) ΓS • ΓR ⊆ Γ(S • R). (quasi transitivity) R ⊆ S =⇒ ΓR ⊆ ΓS. (monotonicity)
The proof of Lemma 3 is straightforward. Remarkably, we can give another characterisation of Γ.

Proposition 1. Given µ, ν ∈ GX and R ∈ Rel = (X , X ), we have:

µ ΓR ν ⇐⇒ ∀f : (X , R) 1 - → ([0, 1], ≤). X f dµ ≤ X f dν, where f : (X , R) 1 - → ([0, 1], ≤) means that f is a measurable function (notice that 1] G{ * }) such that x R implies f (x ) ≤ f ( ).
The proof of Proposition 1 goes essentially as in Katsumata et al. (2018) (Proposition 4.4). See also [START_REF] Sato | Approximate relational hoare logic for continuous random samplings[END_REF]. Using Proposition 1 we can show that Γ is well-behaved with respect to the monad structure of G, and thus that it nicely interacts with sequencing (observe that

let x = e 1 in e 2 (A) = e 2 [ /x] (A) e 1 (d ) = e 2 [-/x] † e 1 (A)). Lemma 4. Given R ∈ Rel = (X , X ), S ∈ Rel = (Y , Y )
, and measurable functions f , : X → Y , the following hold, for all x, ∈ X and µ, ν ∈ GX

x R =⇒ δ x ΓR δ (dirac) (∀x 1 , x 2 ∈ X . x 1 R x 2 =⇒ f (x 1 ) ΓS (x 2 )) =⇒ (µ ΓR ν =⇒ f † (µ) ΓS † (ν )) (bind)
Finally, Γ nicely interacts with the ωCppo-enrichment of G, allowing the following induction principle.

Lemma 5. For any relation R ∈ Rel = (X , X ), any ω-chain (µ n ) n ≥0 in GX , and any ν ∈ GX , if µ n ΓR ν holds for all n ≥ 0, then sup n µ n ΓR ν .

We can now rely on Γ to de ne a suitable notion of applicative (bi)simulation.

Applicative Similarly and Bisimilarity

We are now ready to formally de ne our notion of an applicative (bi)simulation.

De ntion 10. A re exive closed term relation R = (R Λ , R V ) is an applicative simulation if the following conditions hold:

• Λ e 1 R e 2 : τ =⇒ e 1 ΓR V e 2 (app eval) • V r 1 R r 2 : real =⇒ r 1 = r 2 (app num) • V λx.e 1 R λx.e 2 : τ 1 → τ 2 =⇒ ∀ ∈ V τ . • Λ e 1 [ /x] R e 2 [ /x] : τ 2 (app abs) • V î, î R ,  =⇒ î =  ∧ • V î R  : τ î (app inj) • V fold 1 R fold 1 : µα.τ =⇒ • V 1 R 2 : τ [µα.τ /α]. (app fold)
Applicative similarity A is de ned as the largest applicative simulation, whereas applicative bisimilarity A is the largest symmetric applicative simulation.

To see that A indeed exists, we de ne the endofunction [-] on the complete lattice Rel 0 as follows:

• Λ e 1 [R] e 2 ⇐⇒ e 1 ΓR V e 2 • V r 1 [R] r 2 : real ⇐⇒ r 1 = r 2 • V λx.e 1 [R] λx.e 2 : τ 1 → τ 2 ⇐⇒ ∀ ∈ V τ . • Λ e 1 [ /x] R e 2 [ /x] : τ 2 • V î, î [R] ,  ⇐⇒ î =  ∧ • V î R  : τ î • V fold 1 [R] fold 1 : µα.τ ⇐⇒ • V 1 R 2 : τ [µα.τ /α].
We see that R is an applicative simulation if and only if R ⊆ [R]. Besides, Γ being monotone, [-] is monotone as well, and thus it has a greatest xed point which is A .

Remark 1. Notice that we have not required R V ⊆ R Λ for an applicative simulation R = (R Λ , R V ). However, it is straightforward to see that given such a simulation R, we can always extend R Λ adding the pairs of values ( 1 , 2 ) ∈ R V still obtaining a simulation. This directly follows from condition (dirac). In particular, A V ⊆ A Λ .

similarity being de ned coinductively, it comes with an associated coinduction proof principle, which can be formally given as follows:

∃R. R ⊆ [R] • Λ e 1 R e 2 : τ • Λ e 1 A e 2 : τ ∃R. R ⊆ [R] • V 1 R 2 : τ • V 1 A 2 : τ
An easy application of the coinduction proof principle allows us to prove A to be a preorder term relation. Lemma 6. Applicative similarity is re exive and transitive. Sketch. By coinduction, relying on the properties (quasi re exivity) and (quasi transitivity).

Additionally, we see that A = A ∩ ( A ) , so that A is an equivalence term relation. In order to ensure compositionality, we need to prove A and A to be compatible term relations. We rst prove that applicative similarity is compatible, i.e. A ⊆ A . To achieve such a goal, we use Howe's technique [START_REF] Howe | Proving congruence of bisimulation in functional programming languages[END_REF]; [START_REF] Pitts | Howe's method for higher-order languages[END_REF].

De ntion 11. Given a closed term relation R, the Howe extension of R is the term relation R H de ned as the least solution to the equation:

ρ = R o • ρ,
where R o denotes the open extension of R. Such a solution exists, since both -o andare monotone endofunctions. More explicitly, we can inductively de ne R H by:

Γ Λ e 1 R H e 3 : τ Γ Λ e 3 R e 2 : τ Γ Λ e 1 R H e 2 : τ

Γ V 1 R H 3 : τ Γ V 3 R 2 : τ Γ V 1 R H 2 : τ
Notice that R H is not only the least solution to the equation ρ = R o • ρ, but actually to the inclusion R o • ρ ⊆ ρ S. [START_REF] Lassen | Relational reasoning about functions and nondeterminism[END_REF]; [START_REF] Levy | In nitary howe's method[END_REF]. The Howe extension of a re exive and transitive (closed) term relation enjoys several interesting properties. In particular, it is a re exive, compatible, and substitutive term relation.

Lemma 7. Let R be re exive and transitive closed term relation. Then the following hold:

1. R o ⊆ R H . 2. R o • R H ⊆ R H
3. R H is compatible, and thus re exive.

4. R H is substitutive.

The proof of Lemma 7 is standard, and the reader is referred to S. [START_REF] Lassen | Relational reasoning about functions and nondeterminism[END_REF]; [START_REF] Pitts | Howe's method for higher-order languages[END_REF] for details. We are nally ready to prove our rst main result, namely that applicative similarity is a precongruence term relation. To achieve such a goal, we prove that ( A ) H (restricted to closed terms) is an applicative simulation, and it is thus contained in A . Since by Lemma 7 we have the opposite inclusion, we will conclude ( A ) H = A .

Lemma 8 (Key Lemma). Given a re exive and transitive closed term relation R, if R is an applicative simulation, then so is R H (restricted to closed expressions and values). Sketch. By Lemma 7, R H is re exive, and thus a possible candidate simulation. It is easy to see that R H V (restricted to closed values) satis es conditions (app num)-(app fold). It thus remain to prove (app eval), i.e.

• Λ e 1 R e 2 : τ =⇒ e 1 ΓR H V e 2 . Since e 1 = sup n e 1 n) we can appeal to Lemma 5, and the statement: • Λ e 1 R H e 2 : τ =⇒ ∀n ≥ 0. e 1 (n) ΓR H V e 2 . We proceed by induction on n. The base case is trivial. The inductive step is proved by case analysis on the derivation of • Λ e 1 R H e 2 : τ , which in turn gives a case analysis on R H . A central role is played by the inclusion ΓR • ΓR H ⊆ ΓR H (which directly follows from Lemma 7 by monotonicity of Γ). Sequencing is handled as in Dal [START_REF] Dal Lago | E ectful applicative bisimilarity: Monads, relators, and howe's method[END_REF], relying on property (bind), whereas the cases for measurable functions and numerals follows by condition (dirac). All other cases follow by induction hypothesis, relying on substitutivity of R H . Theorem 1. Applicative similarity is a precongruence term relation and a sound proof technique for contextual approximation.

Proof. It is su cient to show that A is compatible and preadequate. By Lemma 8 and Lemma 7 we know that ( A ) H = A when restricted to closed terms. This also holds on arbitrary terms, since ( A ) H is substitutive and, dealing with closed values only, sequential and simultaneous substitution coincide. As a consequence, the open extension of applicative similarity coincides with ( A ) H , and thus it is compatible. To see that A is preadequate, simply observe that A

V [R] = R.
Finally, since A = A ∩( A ) , we see that A is compatible and adequate, and thus a sound proof technique for contextual equivalence.

Theorem 2. Applicative bisimilarity A is a congruence term relation and a sound proof technique for contextual equivalence.

Finally, we observe that we can use A to prove the equalities and laws in Example 3. In particular, the commutativity equation follows by commutativity of G, whereas the soundness of the program transformation of Section 1.1 can be proved combining the quasi-denotational law with congruence properties of A , by passing the two programs an arbitrary value as input.

Digression: Towards Full Abstraction

Theorem 2 states that applicative bisimilarity is sound for contextual equivalence: is it also fully abstract (i.e.

A = ctx )? In [START_REF] Crubillé | On probabilistic applicative bisimulation and call-by-value lambda-calculi[END_REF] this question is answered in the a rmative for a λ-calculus with sampling from discrete probability distributions. Such a result is proved going through testing equivalence De Nicola and Hennessy (1983); [START_REF] Larsen | Bisimulation through probabilistic testing[END_REF], showing that tests can be implemented as λ-term contexts (meaning that testing equivalence includes contextual equivalence), on one hand, and that applicative bisimilarity coincides with testing equivalence, on the other hand.

The latter result has been proved in full generality in [START_REF] Van Breugel | Domain theory, testing and simulation for labelled markov processes[END_REF] relying on nontrivial results from domain theory, category theory, and measurable space theory. Remarkably, the equivalence between bisimilarity and testing equivalence holds not only for Markov chains, but also Markov processes, hence suggesting the possibility of proving full abstraction of applicative bisimilarity also in the continuous case. In fact, it is not hard to see that the operational semantics of Λ P induces a (labelled) Markov process on terms, so that one naturally obtains notions of bisimilarity and testing equivalence for it. However, there is a fundamental di erence between such a Markov process and the ones studied in [START_REF] Van Breugel | Domain theory, testing and simulation for labelled markov processes[END_REF]. The former has uncountably many labels, whereas the latter requires the of labels to be countable.

Indeed, given a state λx.e of the Markov process, in order to model applicative bisimulation we need to consider transitions of the form λx.e -→ e[ /x], meaning that the set of labels of the Markov process needs to contain (at least) all closed values, which are uncountably many.

A natural way to x such a problem is to work with (uncountably many) forms of 'countable' bisimilarity relations A E , where E is a countable set of labels of the Markov process, and to work with E A E in place of A . Showing E A E to be well-behaved, however, turns out to be highly nontrivial and to require the (abstract) identity Γ( i ∈I i ) = i ∈I ΓR. Up to this point, the authors do not know whether such an identity holds, and leave further investigations on full abstraction as future work.

Conclusion

In this paper, we gave a notion of applicative bisimilarity for higher-order languages endowed with an operator performing sampling from continuous distributions. We proved that applicative bisimilarity is adequate and compatible, and thus sound for contextual equivalence. As far as the authors know, this is the rst contribution on coinductive notions of equivalence for continuous probabilistic λ-calculi. We also gave evidence on the e ectiveness of the introduced methodology by proving some nontrivial example equivalences. It is also interesting to notice that we can modify our framework to prove soundness of open (also known as normal form) bisimilarity S. B. [START_REF] Lassen | Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context[END_REF]; [START_REF] Sangiorgi | The lazy lambda calculus in a concurrency scenario[END_REF], along the lines of [START_REF] Lago | E ectful normal form bisimulation[END_REF] (although we should remark that 'standard' open bisimilarity is not very well-suited for typed languages S. B. [START_REF] Lassen | Typed normal form bisimulation[END_REF]).

Related Work Higher-order programming languages featuring sampling from continuous distributions have received quite some attention in the last ten years, due to their use as idioms for bayesian programming. This has stimulated the study of operational [START_REF] Borgström | A lambda-calculus foundation for universal probabilistic programming[END_REF]; [START_REF] Park | A probabilistic language based upon sampling functions[END_REF]; Ramsey and Pfe er (2002) and denotational [START_REF] Ehrhard | Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming[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]; [START_REF] Vákár | A domain theory for statistical probabilistic programming[END_REF] kinds of semantics for these languages. Recently, contextual equivalence and logical relations have been introduced and proved to coincide both in presence and in absence of full recursion by [START_REF] Culpepper | Contextual equivalence for probabilistic programs with continuous random variables and scoring[END_REF]; [START_REF] Wand | Contextual equivalence for a probabilistic language with continuous random variables and recursion[END_REF]. Such logical relations require to test programs against any possible evaluation context, a feature re ected by their characterisation as CIU equivalence [START_REF] Mason | Equivalence in functional languages with e ects[END_REF]. This makes reasoning with and about logical relations quite di cult. However, it is important to stress that such logical relations are de ned for languages with conditioning (which makes program equivalence and semantics considerably harder), a feature not present in Λ P .

Future Work A feature which is absent here, but which is desirable in fully-edged probabilistic programming is conditioning, for example as expressed as a form of scoring. Coming up with an operational semantics for an extension of our λ-calculus with a scoring operator would be relatively easy, through the notion of snite kernel [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]. The latter, however, seem not to carry a monad structure. A better choice might be to work with the monad G(R ∞ ≥0 × -) associating to each expression a probability measures over (measurable sets of) pairs score-value. However, nding a way to compare such measures seems nontrivial. Of course, one can de ne a relation lifting for G(R ∞ ≥0 ×-) composing Γ with the 'canonical' relation lifting for R ∞ ≥0 × -, the latter being nothing but an instance of the output monad. Such a lifting, however, is too ne-grained, as related values are required to have the same score. A better lifting of a relation R might be obtained requiring the expectations of the scores in R-closed measurable subsets of R ∞ ≥0 ×to be equal. Proving such a notion of lifting to be well-behaved is, however, nontrivial.

Finally, a further extension of the present work is the design of behavioural distances for probabilistic languages, possibly along the lines of de Amorim, Gaboardi, Hsu, [START_REF] De Amorim | A semantic account of metric preservation[END_REF]; [START_REF] Gavazzo | Quantitative behavioural reasoning for higher-order e ectful programs: Applicative distances[END_REF]; [START_REF] Reed | Distance makes the types grow stronger: a calculus for di erential privacy[END_REF].

Figure 1 :

 1 Figure 1: Static semantics of Λ P .

Figure 2 :

 2 Figure 2: Compatible re nement.

(Figure 3 :

 3 Figure 3: Structural identities.

This encoding re ects the standard semantics of operations, where to evaluate an expression of the form F (e 1 , . . . , e n ) one rst sequentially evaluates its arguments, proceeding from left to right.

Γ, x : τ V x : τΓ V : τ Γ Λ : τ r ∈ R Γ V r : real Γ Λ sample : real Γ V 1 : real • • • Γ V n : real F ∈ C n Γ Λ F ( 1 , . . . , n ) : real Γ, x : τ 1 Λ e : τ 2 Γ V λx.e : τ 1 → τ 2 Γ V 1 : τ 1 → τ 2 Γ V 2 : τ 2 Γ Λ 1 2 : τ 2 Γ Λ e 1 : τ 1 Γ, x : τ 1 Λ e 2 : τ 2 Γ Λ let x = e 1 in e 2 : τ 2 Γ V : τ î Γ V î, : i ∈I τ i Γ V : i ∈I τ i Γ, x : τ i Λ e i : τ (∀i ∈ I ) Γ Λ case of { i, x → e i } : τ Γ V : τ [µα.τ /α] Γ V fold : µα.τ Γ V : µα.τ 1 Γ, x : τ 1 [µα.τ 1 /α] Λ e : τ 2 Γ Λ case of {fold x → e} : τ 2

Another approach is given in[START_REF] Borgström | A lambda-calculus foundation for universal probabilistic programming[END_REF], where the set of terms inherits a measurable structure from a syntax-oriented metric.

Notice that the function mapping an element x in X to f (x )(A) ∈ [0, 1] is integrable.

Γ, x : τ V x R x : τ Γ V 1 R 2 : τ Γ Λ 1 R 2 : τ Γ V r R r : real Γ Λ sample R sample : real Γ V 1 R 1 : real • • • Γ V n R n : real Γ Λ F ( 1 , . . . , n ) R F ( 1 , . . . , n ) : real Γ, x : τ 1 Λ e 1 R e 2 : τ 2 Γ V λx.e 1 R λx.e 2 : τ 1 → τ 2 Γ V 1 R 1 : τ 1 → τ 2 Γ V 2 R 2 : τ 1 Γ Λ 1 2 R 1 2 : τ 2 Γ Λ e 1 R e 1 : τ 1 Γ, x : τ 1 Λ e 2 R e 2 : τ 2 Γ Λ let x = e 1 in e 2 R let x = e 1 in e 2 : τ 2 Γ V 1 R 2 : τ î Γ V î, 1 R î, 2 : i ∈I τ i Γ V 1 R 2 : τ [µα.τ /α] Γ V fold 1 R fold 2 : µα.τ Γ V R : i ∈I τ i Γ, x : τ i

Notice that R being re exive, R[A] ⊆ A implies R[A] = A.