Barbouche Refka
email: refka.barbouche@gmail.com

FE approximation for an hybrid Naghdi equations for shells with G 1 -midsurface

Keywords: Naghdi's shell model, G 1 -midsurface, hybrid formulation, finite element approximation

Le but de ce travail est de considérer une formulation hybride de la coque de Naghdi avec une surface moyenne G 1 du modèle déjà introduit par H. Le Dret dans [1] et de prouver sa bonne posture. Ici, le déplacement et la rotation de la normale à la surface moyenne sont donnés respectivement en une base cartésienne et une base locale covariante ou contravariante. Cette nouvelle version nous permet, en particulier, d'approximer la solution par des éléments finis conformes avec moins degrés de liberté. Des tests numériques sont donnés pour illustrer l'eficacité de notre approche.

ABSTRACT. The purpose of this present work is to consider an hybrid formulation of Naghdi's shell with G 1 -midsurface of the model already introduced by H. Le Dret in [1] and prove its well-posedness. Here, the displacement and the rotation of the normal to the midsurface are respectively given in Cartesian and local covariant or contravariant basis. This new version enables us, in particular, to approximate by conforming finite elements the solution with less degrees of freedom. Numerical tests are given to illustrate the efficiency of our approach. MOTS-CLÉS : modèle de coque de Naghdi, surface moyenne G 1 , formulation hybride, approximation par éléments finis.

Introduction

The shells and their assemblies are part of a wide variety of elastic structures with big interest for contemporary engineering. Mathematical modeling and numerical analysis of elastic body of three-dimensional problems fail, because of the small thickness parameter relatively small setting [START_REF] Destuyuder | Comparaison entre les modèles tridimensionnels et bidimensionnels de plaques en élasticité[END_REF]. Therefore, it is natural to think about replacing the threedimensional models by bi-dimensional models posed on the middle surface of the shell for reasons of cost calculation [START_REF] Destuyuder | Modélisation des Coques Minces Elastiques[END_REF]. Following the work of [START_REF] Blouza | two finite element approximation of Naghdi's shell model in Cartesian coordinates[END_REF][START_REF] Blouza | Naghdi's shell model : existence, uniqueness and continuous dependance on the midsurface[END_REF][START_REF] Tallec | Analyse numérique d'un modèle de coque de Koiter discrétisé en base cartésienne par éléments finis DKT[END_REF][START_REF] Blouza | Existence et unicité pour le modèle de Naghdi pour une coque peu régulière[END_REF], there has been a renewed interest in this subject for the calculation of shells with C 1 -midsurface, called shells with little regularity, admitting discontinuities of curvatures.

Among shell models with little regularity developed, we find the Naghdi model with G 1 -midsurface introduced in [START_REF] Dret | Well-posedness for Koiter and Naghdi shells with a G1-midsurface[END_REF]. It is a model which takes into account membrane and flexion deformations as well as the effects of transverse shears for homogeneous and isotropic shells with curvatures discontinuities.

These models are often more described via several charts whose surfaces are made up of contiguous patches and the joins between them are called C 1 conditions or more generally G 1 conditions.

In [START_REF] Delfour | Representations of hypersurfaces and minimal smoothness of the midsurface in the theory of shells[END_REF], one can find some examples of G 1 surfaces. For example, to represent a sphere or a torus from a bilipschitzian mapping ϕ from some domain ω in the hyperplane R 2 , we replace ω by a domain with contiguous facets. Each facet will lie in an R 2 -dimensional affine subspace of R 2 and it is K-regular patche as defined in [START_REF] Dret | Well-posedness for Koiter and Naghdi shells with a G1-midsurface[END_REF].

The main result of the present article is to consider mechanical models of shells with such G 1 surfaces by using a formulation without any dual unknown which is inspired from an hybrid formulation introduced to a shell with C 1 join in [START_REF] Blouza | Une formulation hybride du modèle de coque de Naghdi[END_REF]. The conforming approximation of the new hybrid shell model allows us to reduce the number of degrees of freedom since the new formulation is given in terms of displacement and covariant components of the rotation of normal. Therefore, we introduce a new functional framework for the Naghdi model for shells with G 1 -midsurface.

This article is organized as follows. We first recall the geometry of the midsurface and some definitions about G 1 regularity needed to introduce the variational formulation of Naghdi's shell with G 1 -midsurface given in [START_REF] Dret | Well-posedness for Koiter and Naghdi shells with a G1-midsurface[END_REF]. In section 3, we introduce a constraintfree formulation of Naghdi's shell with of G 1 -mid surface instead of the one introduced by [START_REF] Dret | Well-posedness for Koiter and Naghdi shells with a G1-midsurface[END_REF]. We then establish the existence and uniqueness of the solution for a such new model. Section 4 is devoted to the finite element discretization of the hybrid formulation. Let us note that thanks to this constraint-free formulation we only need five degrees of freedom by triangle for computing the solution. Finally, in section 5, we present some numerical tests using FreeFem++ software. We present results of validation for a hyperbolic paraboloid shell and a clamped cylindrical shell. We also show results for two other tests of a basket-handle W 2,∞ -shell and a hat W 2,∞ -shell.

Notation

Greek indices and exponents take their values in the set {1, 2} and Latin indices and exponents take their values in the set {1, 2, 3}. Unless otherwise specified, the summation convention for indices and exponents is assumed.

Let (e 1 , e 2 , e 3 ) be the Cartesian basis of the Euclidean space R 3 . We note u • v the inner product of R 3 , |u| = √ u • v the associate Euclidean norm and u ∧ v the vector product of u and v.

We recall below some definitions and notations introduced in [START_REF] Dret | Well-posedness for Koiter and Naghdi shells with a G1-midsurface[END_REF].

Definition 1.

Let ω be a Lipschitz domain in R 2 and consider a surface chart ϕ : ω → R 3 . We assume that :

1) ϕ is bilipschitz chart, i.e., there exist two constants

0 < C ≤ C such that ∀x, y ∈ ω, C||y -x|| ||ϕ(y) -ϕ(x)|| C ||y -x||. (1)
2) The unit normal vector is defined almost everywhere by

a 3 (x) = ∂ 1 ϕ(x) ∧ ∂ 2 ϕ(x) ||∂ 1 ϕ(x) ∧ ∂ 2 ϕ(x)|| ∈ W 1,∞ (ω; R 3 ). (2)
At this point, it will be convenient to introduce a notational shortcut and recall some definitions of [START_REF] Dret | Well-posedness for Koiter and Naghdi shells with a G1-midsurface[END_REF].

We will say that a surface patch is K-regular if it satisfies (1) and (2).

Definition 2. Let ω 1 =] -1, 0[ 2 and ω 2 =]0, 1[ 2 .
And let S 1 and S 2 be two C 2 -patches such that ϕ 1 (0, x 2 ) = ϕ 2 (0, x 2 ). Then, S 1 and S 2 have a locally G 1 join around a point (0, x), 0 < x < 1, if and only if there exists a neighborhood V x of x such that :

1) Both surfaces have the same tangent plane T x at point ϕ 1 (0, x) for all x ∈ V x .

2) For all unit vectors u = (u 1 , u 2 ) T in R 2 , the angle between the vectors Dϕ 1 (0, x)u and -Dϕ 2 (0, x)u is nonzero.

Let ω be a domain of R 2 such that ω = k i=1 ω i . We consider a shell whose G 1midsurface is given by S =

k i=1 S i = k i=1 ϕ i (ω i )
where S i a subdivision of S into patches and ϕ i ∈ W 2,∞ (ω i ; R 3 ), K-regular is one-to-one mapping such that the vectors a α,i = ∂ α ϕ i , i = 1, ..., k, are linearly independent at each point x ∈ ω i . We let

a 3,i (x) = a 1,i (x) ∧ a 2,i (x) ||a 1,i (x) ∧ a 2,i (x)|| , i = 1, ..., k,
be the unit normal vector on the midsurface at point ϕ i (x). The vectors a i,j define the covariant basis at point ϕ j (x). The regularity of the G 1 -midsurface chart and hypothesis of linear independence on ω j imply that a i,j belong to W 1,∞ (ω j ). The contravariant basis a i k is defined by the relation a i,k • a j k = δ j i,k , where δ k i,k is the Kronecker symbol. In particular a 3,i (x) = a 3 i (x). Note that all these vectors are of class W 1,∞ . We let

a i (x) = |a 1,i (x) ∧ a 2,i (x)| 2 so that a i (x) is the area element of the G 1 -midsurface in the chart ϕ i .
The first and second fundamental forms of the surface are given in covariant components by

a αβ,i (x) = a α,i (x) • a β,i (x), and
b αβ,i (x) = a 3,i (x) • ∂ β a α,i (x) = -a α,i (x) • ∂ β a 3,i (x), since a α,i (x) • a 3,i (x) = 0. Since W 1,∞ is a Banach algebra, it follows that a αβ,i ∈ W 1,∞ (ω i ) and b αβ,i ∈ L ∞ (ω i ).
Finally, the Christoffel symbols are given by

Γ ρ αβ,i = Γ ρ βα,i = a ρ i • ∂ β a α,i , and we have Γ ρ αβ,i ∈ L ∞ (ω i ).
Definition 3. We also assume that ω i and ω j are contiguous, i.e., ω i ∩ ω j = ∅ and ∂ω i ∩ ∂ω j is a segment, we let δ ij denote the common segment on their boundaries. Similarly, given two functions defined on ω i and ω j , which are equal on δ ij if their respective traces on the boundaries agree modulo the translation and rotation that make ω i and ω j contiguous.

A regular midsurface displacement will now consist of k mappings u i = u |ωi ∈ H 1 (ω i ; R 3 ) that are equal on δ ij and the same for their regular rotation of the normal vector r i = r |ωi ∈ H 1 (ω i ; R 3 ), i.e., H 1 -regular mapping from ω i into R 3 given in covariant and Cartesian components by : u j (x) = u i,j (x)a i j (x) = u c i,j (x)e i,j where u i,j = u j • a i,j and u c i,j = u j • e i,j , and r j = r α,j (x)a α j (x) = r c i,j (x)e i,j with the same meaning.

Note that the tangency requirement is easily expressed in covariant coordinates, as it simply reads r 3,j = 0, whereas it becomes r c i,j (x)a c 3,j (x) = 0 in ω j in Cartesian coordinates. Let a αβρσ i ∈ L ∞ (ω i ) be the elasticity tensor, which we assume to satisfy the usual symmetries and to be uniformly strictly positive, i.e., for all symmetric tensor τ αβ,i and almost all x ∈ ω i , we have

a αβρσ i (x)τ αβ,i τ ρσ,i c αβ |τ αβ,i | 2 (3)
with c > 0. To be more specific, we will concentrate on the case of homogeneous, isotropic material with Lamé modulus µ > 0 and λ 0, in which case

a αβρσ i = 2µ(a αβ i a ρσ i + a ασ i a βσ i ) + 4λµ λ + 2µ a αβ i a ρσ i ,
where a αβ i = a α i • a β i are the contravariant components of the first fundamental form. Let e ∈ L ∞ be the thikness of the shell, which we assume to be such that e(x) c > 0 almost everywhere in ω.

In this context, the covariant components of the change of metric tensor read

γ i,αβ (u i ) = 1 2 (∂ α u i • a β,i + ∂ β u i • a α,i ), (4)
the contravariant components of the change of transverse shear tensor read

δ i,α3 (u i , r i ) = 1 2 (∂ α u i • a 3,i + r i • a α,i ), (5)
and the covariant components of the change of curvature tensor read

χ i,αβ (u i , r i ) = 1 2 (∂ α u i • ∂ β a 3,i + ∂ β u i • ∂ α a 3,i + ∂ α r i • a β,i + ∂ β r i • a α,i ), (6)
see [START_REF] Dret | Well-posedness for Koiter and Naghdi shells with a G1-midsurface[END_REF]. Note that all these quantities make sense for shells with little regularity, and are easily expressed with Cartesian coordinates of the unknowns and geometrical data. For instance, we have

∂ α u j • a β,j = ∂ α u c i,j a c β,i,j
and so on.

We assume that the boundary ∂ω ∩ ∂ω i of the chart domain is divided into two parts : γ c i of strictly positive 1-dimensional measure on which the shell is clamped on a part of its edge and a complementary part γ f i on which the shell is subjected to applied tractions and moments.

Let us consider the function space, introduced in [START_REF] Dret | Well-posedness for Koiter and Naghdi shells with a G1-midsurface[END_REF], which is appropriate in the context of shells with little regularity, i.e, with G 1 midsurface :

W = {(u i , r i ) ∈ H 1 (ω i ; R 3 ) 2 , r i • a 3,i = 0 in ω i , u i = u j and r i = r j on δ ij }. (7)
This space is endowed with the natural Hilbert norm

u W = k i=1 u i 2 H 1 (ωi;R 3 ) + r i 2 H 1 (ωi;R 3 ) 1 2 . (8)
The boundary conditions considered are hard clamping conditions on part of the boundary

v i = 0 and s i = 0 on γ c i .
Let us now recall the formulation of Naghdi's problem with G 1 -midsurface. It consists in finding

(u i , r i ) ∈ W such that ∀(v i , s i ) ∈ W, B (u i , r i ), (v i , s i ) = L (v i , s i ) , (9)
where

B (u i , r i ), (v i , s i ) = k i=1 ωi e a αβρσ i [γ i,αβ (u i )γ i,ρσ (v i ) + e 2 12 χ i,αβ (u i , r i )χ i,ρσ (v i , s i )] +4 µ e a αβ i δ i,α3 (u i , r i )δ i,β3 (v i , s i ) √ a i dx (10)
and

L (v i , s i ) = k i=1 ωi P i • v i √ a i dx + γ f i N i • v i + M i s i dγ. ( 11
) Theorem 1. Let P i ∈ L 2 (ω i ; R 3 ) be a given resultant force density, N i ∈ L 2 (γ f i ; R 3 ) an applied traction density, M i ∈ L 2 (γ f i ; R 3
) an applied moment density such that M i • a 3,i = 0 almost everywhere on γ f i and e > 0 the thickness of the shell. Then there exists a unique solution to the problem [START_REF] Bernadou | Méthodes d'éléments finis pour les problème de coques minces[END_REF].

Proof.-See [START_REF] Dret | Well-posedness for Koiter and Naghdi shells with a G1-midsurface[END_REF].

An hybrid version of Naghdi's model with G 1 -midsurface

The purpose of the present section is to consider our constraint-free formulation for Naghdi model for shells with G 1 -midsurface. The unknowns still are the displacement u and rotation r, but instead of considering r i as a vector field as in [START_REF] Dret | Well-posedness for Koiter and Naghdi shells with a G1-midsurface[END_REF], we define it by its covariant or contravariant components as usual in shell theory. For more details one can see Ciarlet ([2]).

We firstly define the tensors (4), ( 5) and ( 6) in a this new framework. It is the object of the following lemma. Let us recall that the covariant derivatives of the tangential components of r α,i are defined by

r α,i|β = ∂ β r α,i -Γ ρ αβ,i r ρ,i . Lemma 4. Let u i ∈ H 1 (ω i ; R 3 ), r α,i ∈ H 1 (ω i ) and ϕ i ∈ W 2,∞ (ω i ).
Then the covariant components of the change of metric tensor read

γ αβ,i (u i ) = 1 2 (∂ α u i • a β,i + ∂ β u i • a α,i ), (12)
the covariant components of the change of transverse shear tensor read

δ α3,i (u i , r α,i ) = 1 2 (∂ α u i • a 3,i + r α,i ) (13)
and the covariant components of the change of curvature tensor read

χ αβ,i (u i , r α,i ) = 1 2 (∂ α u i • ∂ β a 3,i + ∂ β u i • ∂ α a 3,i ) + 1 2 (r α|β,i + r β|α,i ). ( 14
)
These tensors define functions of L 2 (ω i ).

This leads to the following function space :

M = {(u i , r α,i ) ∈ H 1 (ω i ; R 3 ) × H 1 (ω i ) 2 , u i = u j and r α,i = r α,j on δ ij }. ( 15
)
Taking into account the boundary conditions, we thus introduce the Hilbert space

V = {(v i , s α,i ) ∈ M, v i = s α,i = 0 on γ c i }, (16)
and we equipe it with the following norm

(u, r α ) V = k i=1 u i 2 H 1 (ωi;R 3 ) + 2 α=1 k i=1 r α,i 2 H 1 (ωi) 1 2 . ( 17
)
Theorem 2. Let P i ∈ L 2 (ω i ; R 3 ) be a given resultant force density and e > 0 the thickness of the shell. Then there exists a unique solution to the following problem : Find

(u i , r α,i ) ∈ V such that ∀(v i , s α,i ) ∈ V, a (u i , r α,i ), (v i , s α,i ) = l (v i , s α,i ) , (18)
where

a (u i , r α,i ), (v i , s α,i ) = k i=1 ωi {e a αβρσ i [γ αβ,i (u i )γ ρσ,i (v i ) + e 2 12 χ αβ,i (u i , r α,i )χ ρσ,i (v i , s α,i )] +4 µ e a αβ i δ α3,i (u i , r α,i )δ β3,i (v i , s α,i )} √ a i dx (19)
and

l (v i , s α,i ) = k i=1 ωi P i • v i √ a i dx. ( 20
)
The proof is based on the following version of the infinitesimal rigid displacement lemma.

Lemma 5. Let u i ∈ H 1 (ω i ; R 3 ), r α,i ∈ (H 1 (ω i )) 2 and ϕ i ∈ W 2,∞ (ω i ; R 3 ).
(i) If γ αβ,i (u i ) = 0, then there exists a unique ψ ∈ L 2 (ω; R 3 ) such that :

∂ α u i = ψ ∧ ∂ α ϕ i . (ii) If δ α3,i (u i , r α,i ) = 0, then ∂ α u i • a 3,i = -r α,i belong to H 1 (ω i ). Furthermore r α,i = -ε αβ,i ψ • a β i , where ε 11,i = ε 22,i = 0 et ε 12,i = -ε 21,i = √ a i .
(iii) If, in addition to (i) and (ii), χ αβ,i (u i , r α,i ) = 0, then ψ is a constant vector in R 3 and there exists c ∈ R 3 such that

u i (x) = c + ψ ∧ ϕ i (x). Proof.-We notice that if δ α3,i (u i , r α,i ) = 0, then ∂ αβ u i • a 3,i ∈ L 2 (ω i ). Indeed ∂ αβ u i • a 3,i = ∂ β (∂ α u i ) • a 3,i -∂ α u i • ∂ β a 3,i ∈ L 2 (ω i ) as a 3,i ∈ L ∞ (ω i ; R 3 ) and ∂ α u i • a 3,i = -r α,i ∈ H 1 (ω i ). Consequently, χ αβ,i (u i , r α,i ) = -(∂ αβ u i -Γ ρ αβ,i ∂ ρ u i ) • a 3,i = 0.
The results follow the theorem of [START_REF] Blouza | Une formulation hybride du modèle de coque de Naghdi[END_REF]. For conclusion, just use the infinitesimal rigid displacement lemma for shells with minimal regularity, see [START_REF] Anicic | The infinitesimal rigid displacement lemma in Lipschitz coordinates and application to shells with minimal regularity[END_REF] and [START_REF] Blouza | Sur le lemme du mouvement rigide[END_REF]. Lemma 6. There exists a constant C > 0 such that

a (v i , s α,i ), (v i , s α,i ) C k i=1 α,β ||γ αβ,i (v i )|| 2 L 2 (ωi) + α,β ||χ αβ,i (v i , s α,i )|| 2 L 2 (ωi) + α ||δ α3,i (v i , s α,i ))|| 2 L 2 (ωi) 1 2 for all (v i , s α,i ) ∈ H 1 (ω i ; R 3 ) × (H 1 (ω i )) 2 .
Proof.-Thanks to inequality (3) and the fact that

a αβ i (x)η α,i η β,i C α (η α,i ) 2 for all x ∈ ω i .
Lemma 7. We assume that the patches are in W 2,∞ . The bilinear form in (18) is Velliptic.

Proof.-Because of lemma ( 6) and the hypotheses made on the chart ϕ i , the elasticity tensor and the thickness of the shell, it is enough to prove that

|||(v, s α )||| = k i=1 αβ γ αβ,i (v i ) 2 L 2 (ωi) + αβ χ αβ,i (v i , s α,i ) 2 L 2 (ωi) + α δ α3,i (v i , s α,i ) 2 L 2 (ωi) 1 2
(21) is a norm on V bounded from below by a multiple of the natural norm (17) of V . Let us first prove that |||.||| is a norm. Let (v, s α ) ∈ V be such that |||(v, s α )||| = 0. Then, it follows from the infinitesimal rigid displacement lemma 5 that there exists ψ, c ∈ R 3 such that v i (x) = ψ ∧ ϕ i (x) + c. Then, we should consider two cases : FE approximation for an hybrid Naghdi equations for shells with G1-midsurface 52 1) The displacement v i vanishes on γ c i . If ϕ i (γ c i ) is not include in a straight line, it follows that v i = 0 a.e. in ω i , that is to say ψ = c = 0. Consequently, we have s α,i = 0 a.e. in ω i as well.

2) Let us now suppose that ϕ i (γ c i ) is included in a straight line D and that ψ = 0. In this case, ψ is parallel to D hence belongs to the planes spanned by (∂ α ϕ i ) |γ c i for all x ∈ γ c i . Let us pick one such x. Since s α,i = 0 on γ c i and it follows that

∂ α v i = ψ ∧ ∂ α ϕ i , consequently ∂ α v i • a 3,i = ∂ α ϕ i ∧ a 3,i • ψ = 0, on γ c i .
and ψ is orthogonal to the plane spanned by (∂ α ϕ i ) |γ c i , which contradicts the hypothesis. Therefore ψ = 0 and, as before, v i = s α,i = 0 a.e. in ω i . For conclusion we take the remark of [START_REF] Dret | Well-posedness for Koiter and Naghdi shells with a G1-midsurface[END_REF] : if ω i and ω j are two contiguous patches, the equality of traces on δ ij implies that the patched displacement

u : ω -→ R 3 x -→ u i (x) a.e. if x ∈ ω i u j (x) a.e. if x ∈ ω j (22)
and patched rotation 2 where ω is the interior of ω i ∪ ω j . By applying the demonstration made above on u and r α and taking into account the boundary conditions on γ c (corresponds to portions γ c i of ∂ω i ). We obtain u i = 0, ∀i ∈ {1, 2, ...k}, then u = 0 a.e. in ω r α,i = 0, ∀i ∈ {1, 2, ...k}, then r α = 0 a.e. in ω

r α : ω -→ R x -→ r α,i (x) a.e. if x ∈ ω i r α,j (x) a.e. if x ∈ ω j (23) are both in H 1 (ω; R 3 ) × (H 1 (ω))
For the second part of the proof, we argue by contradiction. Let us assume that there exists a sequence

(v n , s α,n ) ∈ V such that (v n , s α,n ) V = 1 but |||(v n , s α,n )||| → 0 when n → +∞. ( 24
)
By extracting a subsequence, we may assume that there exists (v, s α ) ∈ V such that

(v i,n , (s α,i ) n ) (v i , s α,i ) weakly in H 1 (ω i ; R 3 ) × (H 1 (ω i )) 2 and γ αβ,i (v i,n ) γ αβ,i (v i ), χ αβ,i (v i,n , (s α,i ) n ) χ αβ,i (v i , s α,i ) and δ α3,i (v i,n , (s α,i ) n ) δ α3,i (v i , s α,i ),
weakly in L 2 (ω i ). By hypothesis (24), the three tensors tend strongly to zero in L 2 (ω i ), and using lemma 5 and the discussion above, we infer that v i = s α,i = 0. Then, Rellich's lemma implies that v i,n and (s α,i ) n both tend to zero strongly in L 2 .

Let us introduce the two-dimensional vector

(w i,n ) α = v i,n • a α,i . We have, w i,n → 0 in L 2 (ω i ; R 2 ) strongly. Let us define 2e αβ (w) = ∂ α w β + ∂ β w α . It is easy to see that e αβ (w i,n ) = γ αβ,i (v i,n ) + v i,n • ∂ α a β,i → 0 strongly in L 2 (ω i ). (25) Indeed, ∂ α a β,i ∈ L ∞ (ω i ).
Then, by the two-dimensional Korn inequality, we deduce that

w i,n → 0 strongly in H 1 (ω i ; R 2 ). ( 26
)
Next we note that

∂ ρ v i,n • a α,i = ∂ ρ (w i,n ) α -v i,n • ∂ ρ a α,i → 0 strongly in L 2 (ω i ). ( 27
) Indeed, ∂ ρ a α,i ∈ L ∞ (ω i ). Moreover, as (s α,i ) n → 0 in L 2 (ω i ) strongly, and ∂ ρ v i,n • a 3,i = δ ρ3,i (v i,n , s i,n ) -(s α,i
) n , we already know that

∂ ρ v i,n • a 3,i → 0 strongly in L 2 (ω i ). ( 28
)
We deduce that

∂ ρ v i,n → 0 in L 2 (ω i ; R 3 ), (29)
by ( 27) and ( 28). It follows that v i,n → 0 strongly in H 1 (ω i ; R 3 ).

We use a similar argument to prove that (s α,i ) n → 0 strongly in H 1 (ω i ).

Combining now the convergence of v i,n and (s α,i ) n , we see that (v i,n , (s α,i ) n ) V → 0, which contradicts the hypothesis and proves the lemma.

Lemma 8. For all i ∈ {1, 2, . . . , k}, u i ∈ H 1 (ω i ; R 3 ) then u ∈ H 1 (ω; R 3 ). For all i ∈ {1, 2, . . . , k}, r αi ∈ H 1 (ω i ) then r α ∈ H 1 (ω). Proof.-If u i ∈ H 1 (ω i ; R 3 ) such that u i = 0 on γ c
i and u i = u j on δ ij then u ∈ H 1 (ω; R 3 ) and u = 0 on γ c . If r αi ∈ (H 1 (ω i )) 2 such that r αi = 0 on γ c i and r αi = r αj on δ ij then r α ∈ (H 1 (ω i )) 2 and r α = 0 on γ c .

Proof.-(of theorem 2) The bilinear and linear forms of problem (18) are clearly continuous on the space V . We have just shown that the bilinear form is V -elliptic. We use the Lax-Milgram theorem to conclude.

Finite Element Approximation

A finite element formulation

Let us first introduce some notation. Let(T hi ) be a shape-regular family of triangulations of ω i . For a triangle K i in T hi , let h Ki be its diameter and set h i = max Ki h Ki . We denote by S hi the set of vertices in T hi . For any subdomain ∆ i of ω i and for k ≥ 0 we define by P ki (∆ i ) the space of polynomials on ∆ i with degree ≤ k. In what follows, C denotes a constant independent of h i .

The discrete space of admissible displacements and rotations is given by

V h = {(v h,i , s α,h,i ) ∈ M h , v h,i = s α,h,i = 0 on γ c i } (30)
where

M h = {(v h,i , s α,h,i ) ∈ C 0 (ω i ; R 3 )×C 0 (ω i ) 2 , ∀K i ∈ T hi (v h,i , s α,h,i ) |Ki ∈ P 1 (K i ; R 3 )×P 1 (K i ) 2 , v h,i = v h,j and s α,h,i = s α,h,j on δ ij }.
Thus the discrete problem reads :

Find (u h,i , (r α,h,i )) ∈ V h such that ∀(v h,i , s α,h,i ) ∈ V h , a((u h,i , r α,h,i ), (v h,i , s α,h,i )) = l(v h,i , s α,h,i ) (31)
Naturally, this problem has a unique solution.

Convergence

By virtue of the classical properties of Galerkin approximation, we have the following convergence results

Theorem 3. There exists a sequence h → 0 such that

(u i , r α,i ) -(u h,i , r α,h,i ) V → 0 (32)
Proof.-We have u h,i → u i when h → 0 by virtue of properties of Galerkin approximation of a classical variational problem.

If the solution is assumed to have some regularity, the second step of the approximation may of course be controlled via an error estimate.

Proposition 9. Assume that the solution

(u i , r α,i ) of problem (18) belongs to H 2 (ω i , R 3 )× (H 2 (ω i )) 2 .
Then there exists a constant C independent of h, such that

(u i , r α,i ) -(u h,i , r α,h,i ) V ≤ C h (u i , r α,i ) H 2 (ωi,R 3 )×(H 2 (ωi)) 2 (33)
Proof.

-See [START_REF] Ciarlet | The Finite Element Method for Elliptic Problems[END_REF], for example.

Remarks 10. i) The a priori error estimate given in Proposition 9 makes an essential use of a H 2 -regularity of the solution.

ii) For our Hybrid Naghdi's formulation of the present work and also for Cartesian equations where the surface is globally W 2,∞ , the solution regularity is still an open problem.

iii) The solution regularity depends on the regularity of chart defining the shell midsurface. In the case where the chart is of class C 3 , O. Iosifescu in [START_REF] Iosifescu | Regularity for Naghdi's shell equations[END_REF] has established the H 2 -regularity of the solution in a local covariant or contravariant framework. iv) In a recent work [START_REF] Merabet | A mixed discontinuous finite element method for folded Naghdi's shell[END_REF], I. Merabet and S. Nicaise have introduced a new mixed formulation for Nagdhi's shell which is appropriate for folded surfaces and have approximated the solution of the problem using the DK method. The standard a priori error analysis of such methods uses additional regularity on the solution but in [START_REF] Merabet | A mixed discontinuous finite element method for folded Naghdi's shell[END_REF], I. Merabet and S. Nicaise have carried out an error analysis which only requires the regularity of the weak solution.

Numerical experiments

In this section, we implement the discretization of the hybrid approach. We compare it on a literature benchmark for validation. We also apply it to shells with curvature discontinuities where the midsurface is G 1 .

Implementation details

The model formulation only require the knowledge of a α,i , a 3,i , and ∂ α a 3,i . All other quantities, either geometrical like the elasticity tensor or kinematical like the strain tensors, can be expressed by means of dot products involving these quantities. It is convenient to define these vectors as FreeFem++ functions. The dot products are expressed as FreeFem++ macros, which are then combined into other macros that eventually expand to all the other quantities of interest. The net result is that our code automatically constructs the bilinear forms, with minimal user input. This works well if an analytic description of the G 1 -midsurface is available.

We note that with respect to user input and code complexity, our approach compares favorably with classical formulations which require the computation of the covariant and mixed components of the second fundamental form and of the Christoffel symbols of the chart ; see, for example, [START_REF] Bernadou | Méthodes d'éléments finis pour les problème de coques minces[END_REF].

Three-dimensional visualization of the undeformed and deformed shells uses Medit, a free mesh visualization software available at http://www.ann.jussieu.fr/frey/ logiciels/medit.html.

All the tests were run on 4GB HP 15 Notebook laptop.

Numerical validation

We present in this section two tests. The first is a literature benchmark for shell elements. The second is a cylindrical shell.

The hyperbolic paraboloid shell

The midsurface of the hyperbolic paraboloid shell is represented by a chart of class C ∞ .

The reference domain of the midsurface is given by

ω = {(x, y) ∈ R 2 , |x| + |y| < √ 2b},
and the chart is defined by ϕ(x, y) = (x, y, c 2b 2 (x 2 -y 2 )) T , with b = 50 cm and c = 10 cm. The thickness of the shell is e = 0.8 cm.

The shell is clamped on ∂ω and subjected to a uniform pressure q = 0.01 kp/cm 2 . The mechanical data are E = 2.85 × 10 4 kp/cm 2 , ν = 0.4

The reference value for this test is the normal displacement at the center O(0, 0) of the shell. Its value computed by various methods is of -0.024 cm ; see [START_REF] Bernadou | Méthodes d'éléments finis pour les problème de coques minces[END_REF]. Due to the symmetries of the problem, we use the computational domain

ω = {(x, y) ∈ R 2 , 0 < x, 0 < y, x + y < √ 2b},
and enforce the symmetry conditions u 2 = 0, r 2 = 0, on y = 0, and u 1 = 0, r 1 = 0 on x = 0.

These conditions are obtained by expressing the continuity of the three-dimensional Kirchhoff-Love displacement along these edges. In Table 1. the value of normal displacement at O is reported for hybrid and mixed formulation. Those values are given in respect of the number of degrees of freedom.

Tableau 1 -Hybrid formulation vs mixed formulation Formulation Dof u 3 (0, 0) Hybrid 10615 -0.0242544 Mixed 14861 -0.0242545

The numerical results obtained for the reference value are very satisfactory as they are close to -0.024 cm, the value given in the literature. We note that the hybrid method achieves excellent performance in terms of the reference value and with less degrees of freedom, which is in good agreement. For qualitative results we plot the isovalues of u 3 below in Figure [START_REF] Dret | Well-posedness for Koiter and Naghdi shells with a G1-midsurface[END_REF], solution of the hybrid equations.

A clamped cylindrical shell

In this example, we consider a cylindrical shell which is submitted to a uniform pressure load, and clamped only on the top. The opposite side being free. The reference domain of the midsurface is given by ω = {(x, y) ∈ R 2 ; 0 < x < 2πR, 0 < y < H}, and the chart is defined by ϕ(x, y) = (R cos(x), R sin(x), y) t , where H = 20cm and R = 10cm. The thickness of the shell is e = 0.5 cm. The shell is clamped on γ e = {(x, H) ∈ R 2 ; 0 < x < 2πR} and subjected to an internal pressure p = 1kp/cm 2 . The mechanical data are E = 3 × 10 5 kp/cm 2 , and ν = 0.22. The analytic normal displacement solution of the problem is given by : where

K = 3p(1 -ν 2 ) 2e 3 E e 2 R 4 e 2 + 3R 2 (1 -ν 2 ) , µ = √ c 2 -b √ 2 , γ = √ c 2 + b √ 2 , with b = ν R 2 , c 4 = 1 R 4 + 3(1 -ν 2 ) ε 2 R 2 ,

and

(A, B, C, D) = (-0.0001466, -0.0003600, -0.0058966, 0.0061476). We plot in Fig 2 . the exact and approximate solutions of the normal covariant displacement of the midsurface. We thus establish the error between the approximate and exacte solutions in V norm as well as in L 2 norm. In Fig 3 . we show the convergence rates which confirm the theoretical estimates.

Other tests

A basket-handle tunnel

Our next test is a genuine W 2,∞ test with curvature discontinuities. The shell is made of 3 cylindrical parts with different radiuses and C 1 -joins. It is a tunnel-like shell based on a slightly extended 3-circles basket-handle arc.

The mechanical data are given by E = 3 × 10 6 psi, ν = 0.0 and the thickness of the shell e equals 3 in. The shell is submitted to a uniform downward pressure of -0.625 lb/in 2 .

Let us compute the tangent vectors at join point (0, y). We obtain a 11 = ∂ϕ 1 ∂x = (1, 0, 0) t and a 12 = ∂ϕ 2 ∂x = (2, 0, 0) t .

We thus obtain a 11 = 2a 22 .

The reference value for this test is the normal displacement at the center O(0, 0) of the shell. Table 3. present the values of normal displacement at O and the number of degrees of freedom which are obtained from mixed method with C 1 -parametrization, hybrid method with C 1 -parametrization and hybrid method with G 1 -parametrization, using the same geometry with P 1 elements. We note that the hybrid method achieves excellent performance in terms of the reference value and with less degrees of freedom, which is in good agreement. For qualitative results we plot the isovalues of u 3 in figure [START_REF] Tallec | Analyse numérique d'un modèle de coque de Koiter discrétisé en base cartésienne par éléments finis DKT[END_REF], solution of the hybrid equations with G 1 -parametrization.

Conclusion

In this paper we have presented a new version of Naghdi's shell with G 1 -midsurface. We thus introduce an hybrid Naghdi problem in which the unknowns are the displacement u and the rotation r, respectively elements of the spaces H 1 (ω; R 3 ) and (H 1 (ω)) 2 without any functional constraint. For this hybrid model we have derived a finite element scheme for which we have established existence and uniqueness of the solution as well. Its discretization requires less degrees of freedom than the mixed formulation of [START_REF] Blouza | two finite element approximation of Naghdi's shell model in Cartesian coordinates[END_REF].

Figure 1 -

 1 Figure 1 -Qualitative result : Isovalues of u 3 .

u 3 =

 3 K(1 + exp(µy)(A cos(γy) + B sin(γy)) + exp(-µy)(C cos(γy) + D sin(γy)))

Figure 2 -

 2 Figure 2 -Exact and approximate solutions of u 3

Figure 3 -

 3 Figure 3 -Convergence rate for the displacement in V norm (up). Convergence rate for the displacement in L 2 norm (down).

Tableau 3 -

 3 Comparison of resolution methods Formulation Dof u 3 (0, 0) Mixed with C 1 -parametrization 539 -18.1381 Hybrid with C 1 -parametrization 385 -18.1384 Hybrid with G 1 -parametrization 420 -18.1323

The reference domain of the midsurface is given by, ω =

where

and the chart is defined by

Figure 4 -The mesh on the basket-handle midsurface.

Concerning boundary conditions, we consider the case of hard clamping on both rectilinear sides of the shell. The large circle radius is 400 in. and the small circle radius 200 in. (We the whole shell without using the symmetries for better visualization.)

Figure 5 -Qualitative result : Isovalues of u 3 . Now, for the same shell we consider G 1 -parametrization instead of the C 1 one. We thus propose below a G 1 chart on the same reference domain :

Let us compute the tangent vectors at join points (-2π 9 , 0) and ( 2π 9 , 0). On x = (-2π 9 , 0), we get

We thus obtain a 11 = 2a 12 . On x = ( 2π 9 , 0), we obtain

)

and then we find a 13 = 2a 12 .

The reference value for this test is the normal displacement at the center O(0, 0) of the shell. In Table 2. we present the values of normal displacement at O and the number of degrees of freedom which are obtained from mixed method with C 1 -parametrization, hybrid method with C 1 -parametrization and hybrid method with G 1 -parametrization, using the same geometry with P 2 elements. We note that the hybrid method achieves excellent performance in terms of the reference value and with less degrees of freedom, which is in good agreement. Figure [START_REF] Destuyuder | Modélisation des Coques Minces Elastiques[END_REF] presents the initial mesh and for qualitative results we plot the isovalues of u 3 in figure [START_REF] Blouza | two finite element approximation of Naghdi's shell model in Cartesian coordinates[END_REF], solution of the hybrid equations with G 1 -parametrization.

Plate-cylinder

We consider a real test of a W 2,∞ shell with curvature discontinuities. Let a shell formed by a flat part, called plate, and a cylindrical portion, which are connected in a C 1 -way. See figure [START_REF] Blouza | Naghdi's shell model : existence, uniqueness and continuous dependance on the midsurface[END_REF]. To solve the problem of this shell, we use the hybrid method and we compared it with the mixed method . The reference domain of the midsurface is given by ω

[, and the chart is defined by :

FE approximation for an hybrid Naghdi equations for shells with G1-midsurface 60


J Wu
email: jie.wu@math.cnrs.fr

ON A SUM INVOLVING THE EULER TOTIENT FUNCTION

Keywords: Mathematics Subject Classification. 11N36, 11L05. Key words and phrases. Euler totient function, exponential sums

In this short note, we prove that 4 π 2 x log x + O(x)

for x → ∞, where ϕ(n) is the Euler totient function and [t] is the integral part of real t. This improves recent results of Bordellès-Heyman-Shparlinski and of Dai-Pan.

Introduction

As usual, denote by ϕ(n) the Euler totient function and by [t] the integral part of real t. Very recently, Bordellès, Heyman and Shparlinski [START_REF] Bordellès | On a sum involving the Euler function[END_REF] studied the asymptotic behaviour of the summatory function They also posed a question : Is it true that S(x) = 6 π 2 + o(1) x log x as x → ∞ ? Some numerical evidences were given. The aim of this short note is to improve Bordellès, Heyman and Shparlinski's (1.2) and (1.3), by refining their method. Our result is as follows.

Theorem 1. We have

(1.4) 4 π 2 x log x + O(x) S(x) 1 3 + 4 π 2 x log x + O(x) for x → ∞.
For comparaison, we have As indicated by Bordellès, Heyman and Shparlinski in [START_REF] Bordellès | On a sum involving the Euler function[END_REF], the proof of (1.2) is rather elementary. But the lower bound (1.3) uses a much deeper approach relying on the theory of exponential pairs. In particular, to obtain the numerically stronger result, they used the recently discovered exponent pair ( 13 84 +ε, 55 84 +ε) by Bourgain [START_REF] Bourgain | Decoupling, exponential sums and the Riemann zeta function[END_REF]. Let ψ(t)

   1 2 + 3 π 2 ≈ 0.
:= t-[t]-1 2
and δ ∈ {0, 1}. For x 2 and 1 D x, define

(1.5) S δ (x, D) := D<d 2D ϕ(d)ψ x d + δ .
The key of Bordellès, Heyman and Shparlinski's method is to find θ as large as possible such that

(1.6) S δ (x, x θ ) x.
They shew that θ = 2629 4009 ≈ 0.65577 is admissible and obtained the constant θ 6 π 2 in the lower bound (1.3).

Our improvements come from two simple observations:

(a) Firstly we give a more careful treatment for the related exponential sum (see Proposition 2.1 below). This allows us to show that θ = 2 3 ≈ 0.66666 is admissible for (1.6) and to get a better lower. It is worth to note that our argument is simpler and that we do not need to use Bourgain's new exponent pair. In fact we only use the simplest exponent pair ( 12 , 1 2 ), i.e. van der Corput inequality. (b) Our argument about upper bound part is different from [START_REF] Bordellès | On a sum involving the Euler function[END_REF]. In order to improve upper bound (1.2), we introduced exponential sum technique to show that the constant in the upper bound can be improved to 1 -θ + θ 6 π 2 . It should be possible to further improve slightly the constants in Theorem 1 by applying combinatorial identity on the Möbius function and more sophistic methods of multiple exponential sums (see [START_REF] Fouvry | Exponential sums with monomials[END_REF][START_REF] Wu | Almost primes in short intervals[END_REF]).

When we redact our manuscript, we note that Lixia Dai & Hao Pan [START_REF] Dai | Note on a sum involving the Euler function[END_REF] also have remarked (b) above and obtained a better upper bound constant 1380 4009 + 2629 4009 6 π 2 ≈ 0.74288 than (1.2) by using Bordellès, Heyman and Shparlinski's θ = 2629 4009 value.

A key estimate

The aim of this section is to prove the following bound for S δ (x, D), which will play a key role in proof of Theorem 1.

Proposition 2.1. Under the previous notation, we have

(2.1) S δ (x, D) (x κ D 1+λ ) 1/(κ+1) + x κ D -2κ+λ log x + x -1 D 3 ,
where (κ, λ) is an exponent pair.

Two preliminary lemmas.

In order prove Proposition 2.1, we need two standard lemmas in the exponential sum theory. The first one is due to Vaaler (see [START_REF] Graham | Van der Corput's Method of Exponential sums[END_REF]Theorem A.6] or [START_REF] Bordellès | On a sum involving the Euler function[END_REF]Lemma 4.3]). Lemma 2.2. For x 1 and H 1, we have

ψ(x) = - 1 |h| H Φ h H + 1 e(hx) 2πi + R H (x),
where Φ(t) := πt(1 -|t|) cot(πt) + |t| and the error term R H (x) satisfies

|R H (x)| 1 2H + 2 0 |h| H 1 - |h| H + 1 e(hx).
The second lemma is [START_REF] Graham | Van der Corput's Method of Exponential sums[END_REF]Lemma 2.4]. With the help of Lemma 2.3 and noticing the fact that 0 < Φ(t) < 1 (0 < |t| < 1), we can derive

Lemma 2.3. Let L(Q) := J j=1 C j Q c j + K k=1 D k Q -d k , where C j , c j , D k , d k > 0. For any Q Q > 0, there exists some Q 1 ∈ [Q , Q] such that L(Q 1 ) J j=1 K k=1 (C d k j D c j k ) 1/(c j +d k ) + J j=1 C j Q c j + K k=1 D k Q -d k .
S δ (x, D, m, N ) N H + h H 1 h D/m<n N e hx mn + δ for D/m < N 2D/m and 1 H N .
Applying the exponent pair (κ, λ) to the inner sum over n, we find that

S δ (x, D, m, N ) N H + h H 1 h hx mN 2 κ N λ + mN 2 hx H -1 N + x κ H κ m -κ N -2κ+λ + x -1 mN 2 for all H ∈ [1, N ]. According to Lemma 2.3, there is a H ∈ [1, N ] such that S δ (x, D, m, N ) (x κ m -κ N -κ+λ ) 1/(κ+1) + x κ m -κ N -2κ+λ + x -1 mN 2 (x κ D -κ+λ m -λ ) 1/(κ+1) + x κ D -2κ+λ m κ-λ + x -1 D 2 m -1 .
Inserting it into (2.2), we obtain the required result.

Proof of Theorem 1: Upper bound

Let 1 D < √ x be a parameter to be chosen later. We write

(3.1) S(x) = S 1 (x) + S 2 (x) with S 1 (x) := n D ϕ x n , S 2 (x) := D<n x ϕ x n .
A. Upper bound of S 1 (x) We have trivially x/(d+1)<n x/d

(3.2) S 1 (x) n D x n = x log D + O(x).
1 = d x/D ϕ(d) x d -ψ x d - x d + 1 + ψ x d + 1 = x d x/D ϕ(d) d(d + 1) + d x/D ϕ(d) ψ x d + 1 -ψ x d .
It is well known that

n x ϕ(n) = 3 π 2 x 2 + O(x log x), n x ϕ(n) n 2 = 6 π 2 log x + O(1).
With the help of these, it follows that (3.4)

d x ϕ(d) d(d + 1) = d x ϕ(d) d 2 1 + O 1 d = 6 π 2 log x + O(1)
and

(3.5) d √ x ϕ(d) ψ x d + 1 -ψ x d 2 d √ x ϕ(d) x.
It remains to bound

E(x, D) := √ x<d x/D ϕ(d) ψ x d + 1 -ψ x d .
Let D k := x/(2 k D) and let K be the integer such that D K+1 < √ x D K . By a simple dyadic split and by Proposition 2.1 with (κ, λ) = ( 12 , 1 2 ), it follows that

(3.6) |E(x, D)| 1 k K+1 (|S 0 (x, D k )| + |S 1 (x, D k )|) 1 k K+1 x 1/3 D k + x 1/2 D -1/2 k log x + x -1 D 3 k x 1/3 (x/D) + x 1/2 (log x) 2 + x -1 (x/D) 3 x 4/3 D -1 + x 1/2 (log x) 2 + x 2 D -3 .
Inserting (3.4), (3.5) and (3.6) into (3.3), we find

(3.7) S 2 (x) 6 π 2 x log(x/D) + O x 4/3 D -1 + x 1/2 (log x) 2 + x 2 D -3 .

2

 2 + o(1) x log x (x → ∞). (1.3)

2. 2 .

 2 Proof of Proposition 2.1. As usual, denote by µ(n) the Möbius function. By using the relation 2D/m |S δ (x, D, m, N )|, where S δ (x, D, m, N ) :=

B.

  Upper bound of S 2 (x) In order to bound S 2 (x), we put d = [x/n]. Then x/n -1 < d x/n and x/(d + 1) < n x/d.

C. 4 . 2 x( 3 k x 1 / 3 D

 42313 End of the proof Inserting (3.2) and (3.7) into (3.1) and taking D = x 1/3 , we get the required the upper bound in (1.4). Proof of Theorem 1: Lower bound Similar to (3.3), we can write S(x) = log D + O(x) + R(x, D), where R(x, D) := d D ϕ(d) ψ x d + 1 -ψ x d . Let D k := D/2 k and let K be the integer such that D K+1 < 1 D K . By a simple dyadical split and by Proposition 2.1 with (κ, λ) = ( |S 0 (x, D k)| + |S 1 (x, D k )|) 1 k K+1 x 1/3 D k + x 1/2 D -1/2 k log x + x -1 D + x 1/2 (log x) 2 + x -1 D 3 .Inserting (4.2) into (4.1), we findS(x) 6 π 2 x log D + O x 1/3 D + x 1/2 (log x) 2 + x -1 D 3 .The required result follows from the choice of D = x 2/3 .

  80396,

	2629 4009	6 π 2 ≈ 0.39841,	and	  	1 3 + 4 π 2 ≈ 0.73861, 4 π 2 ≈ 0.40528.

Acknowledgements. This work is supported in part by Scientific Research Innovation Team Project Affiliated to Yangtze Normal University (No. 2016XJD01). The author is thankful to Lixia Dai at Nanjing Normal University (China) for drawing his attention to Bordellès, Heyman and Shparlinski's paper [1].


Pierre Clairambault
email: pierre.clairambault@ens-lyon.fr

Hugo Paquet
email: hugo.paquet@cl.cam.ac.uk

Fully Abstract Models of the Probabilistic λ-calculus

Keywords: 2012 ACM Subject Classification Theory of computation → Denotational semantics, Theory of computation → Probabilistic computation Keywords and phrases Game Semantics, Lambda-calculus, Probabilistic programming, Relational model, Full abstraction Digital Object Identifier 10.4230/LIPIcs.CSL.2018.16

published or not. The documents may come   L'archive ouverte pluridisciplinaire

Introduction

The interest in probabilistic programs in recent years, driven in particular by applications in machine learning and statistical modelling, has triggered the need for theoretical foundations, going beyond the pioneering work of Kozen [START_REF] Kozen | Semantics of probabilistic programs[END_REF] and Saheb-Djahromi [START_REF] Saheb-Djahromi | Cpo's of measures for nondeterminism[END_REF]. Although a variety of approaches exist, we focus on the probabilistic λ-calculus Λ + , which extends the pure (untyped) λ-calculus with a probabilistic choice operator. The extension is natural and applications are quick to arise -see for instance [START_REF] Borgström | A Lambda-Calculus Foundation for Universal Probabilistic Programming[END_REF]. But in order for Λ + to become a useful formal model for probabilistic computation, the extensive classical theory of the λ-calculus must be readapted.

Among the existing research in this direction, we are especially interested in the work of Ehrhard, Pagani and Tasson [START_REF] Ehrhard | The computational meaning of probabilistic coherence spaces[END_REF], and of Leventis [START_REF] Leventis | Probabilistic lambda-theories[END_REF][START_REF] Leventis | Probabilistic Böhm Trees and Probabilistic Separation[END_REF]. In [START_REF] Ehrhard | The computational meaning of probabilistic coherence spaces[END_REF], the authors define an operational semantics for Λ + and study a model in the category of probabilistic coherence spaces, an existing model [START_REF] Danos | Probabilistic coherence spaces as a model of higherorder probabilistic computation[END_REF] of Probabilistic PCF. They prove an adequacy theorem for Λ + , and this result also applies to the weighted relational model, of which probabilistic coherence spaces are a refinement.

2

The Probabilistic λ-calculus

Syntax

The set Λ + of terms of the probabilistic λ-calculus is defined by the following grammar, where p ranges over the interval [0, 1] and x over an infinite set Var:

M, N ::= x | λx.M | M N | M + p N.
Write Λ + 0 for the set of closed terms, i.e. those with no free variables. The operator + p represents probabilistic choice, so that a term of the form M + p N has two possible reduction steps: to M , with probability p, and to N , with probability 1 -p. Accordingly, the reduction relation we consider is a Markov process over the set Λ + , and corresponds to a probabilistic variant of the standard head-reduction. It is defined inductively:

(λx.M )N 1 -→ M [N/x] M + p N p -→ M M + p N 1-p --→ N M p -→ M λx.M p -→ λx.M M p -→ M M = λx.P M N p -→ M N
For M, N ∈ Λ + , there may be many reduction paths from M to N . The weight of a path π : M p1 -→ . . . pn -→ N is the product of the transition probabilities: w(π) = n i=1 p i . The probability of M reducing to N is then defined as Pr(M → N ) = π:M → * N w(π).

The normal forms for this reduction are terms of the form λx 0 . . . x n-1 . y M 0 . . . M k-1 , where n, k ∈ N and M i ∈ Λ + for all i. Such terms are called head-normal forms (hnfs). A pure λ-term has at most one hnf called -if it exists -its hnf, though of course, this does not hold in the presence of probabilities.

Given a set H of hnfs, we set Pr(M → H) = H∈H Pr(M → H). The probability of convergence of a term M , denoted Pr ⇓ (M ), is the probability of M reducing to some hnf: Pr ⇓ (M ) = Pr(M → {H ∈ Λ + | H hnf}). Finally we say that two terms M and N are observationally equivalent, written M = obs N , if for all contexts C[ ], Pr ⇓ (C[M ]) = Pr ⇓ (C[N ]).

Probabilistic Böhm trees

Infinitely extensional Böhm trees for pure λ-terms

There are several notions of infinite normal forms for pure λ-terms, including e.g. the Böhm trees [START_REF] Pieter | The lambda calculus[END_REF] and the Lévy-Longo trees, among others. The normal forms for the probabilistic λ-terms considered in this paper build on the infinitely extensional Böhm trees (also called Nakajima trees), which provide a notion of infinitely η-expanded normal form.

The infinitely extensional Böhm tree of M is in general an infinite tree, which can be defined as the limit of a sequence of finite-depth approximants. In fact those approximants will suffice for the purposes of this paper: given a λ-term M and d ∈ N, the tree BT d (M ) is ⊥ if d = 0 or if M has no head-normal form, and

λz 0 . . . z n-1 x 0 x 1 . . . • y BT d-1 (P 0 ) . . . BT d-1 (P k-1 ) BT d-1 (x 0 ) BT d-1 (x 1 ) . . . if d > 0 and M has hnf λz 0 . . . z n-1 .y P 0 . . . P k-1 .
In order to deal with issues of α-renaming, we adopt the same convention as Leventis [START_REF] Leventis | Probabilistic lambda-theories[END_REF], whereby the infinite sequence of abstracted variables at the root of a tree of depth d > 0 is labelled x d 0 , x d 1 , . . . so that any tree is determined by the pair (y, (T n ) n∈N ) of its head variable and sequence of subtrees.

Leventis' probabilistic trees

Infinitely extensional Böhm trees for the λ-calculus have striking properties: they characterise observational equivalence of terms, and as a model they yield the maximal consistent sensible λ-theory (see [START_REF] Pieter | The lambda calculus[END_REF] for details). In his PhD thesis, Leventis [START_REF] Leventis | Probabilistic lambda-theories[END_REF] proposes a notion of probabilistic Böhm tree which plays the same role for Λ + . Intuitively, because a term of C S L 2 0 1 8

16:4

Fully Abstract Models of the Probabilistic λ-calculus the form λx 0 . . . x n-1 .z P 0 . . . P k-1 + p λy 0 . . . y m-1 .w Q 0 . . . Q l-1 has two hnfs, it may be represented by a probability distribution over trees of the form of that above. Accordingly, two different kinds of trees are considered: value trees, representing head-normal forms (without probability distribution at top-level), and probabilistic Böhm trees, representing general terms:

VT 0 = ∅, VT d+1 = (y, (T n ) n∈N ) | y ∈ Var and ∀n ∈ N, T n ∈ PT d and PT d = T : VT d → [0, 1] | t∈VT d T (t) ≤ 1 .
We can then assign trees to individual terms: Definition 2. Given M ∈ Λ + and d ∈ N, its probabilistic Böhm tree of depth d is the tree PT d (M ) ∈ PT d defined as follows:

PT d (M ) : VT d -→ [0, 1] t -→ Pr(M → {H hnf | VT d (H) = t})
where for any hnf H = λz 0 . . . z n-1 .y P 0 . . . P k-1 , the value tree of depth d of H is defined as

VT d (H) = y, PT d-1 (P 0 ) , . . . , PT d-1 (P k-1 ) , PT d-1 x d n , . . . .
Consider for example the term M 1 = λxy.x (y + 1 3 (λz.z)), a head-normal form. Figure 1a outlines the first steps in the construction of its value tree of depth d, for some fixed d ≥ 2; note that we use the symbol δ t to denote the distribution in which t has probability 1, and all other trees 0.

Infinitely extensional probabilistic Böhm trees precisely characterise observational equivalence in Λ + ; writing M = PT N if for every d ∈ N, PT d (M ) = PT d (N ), we have: Theorem 3 (Leventis [16]). For any M, N ∈ Λ + , M = obs N if and only if M = PT N .

So infinitely extensional probabilistic Böhm trees provide a fully abstract interpretation of the probabilistic λ-calculus. We will see now that similar trees arise as probabilistic strategies when interpreting λ-terms in a denotational games model.

Strategies and event structures

Moving towards our game semantics of Λ + , we will first introduce our probabilistic strategies as a more economical, syntax-free presentation of probabilistic Böhm trees. The usual correspondence between Böhm trees and innocent strategies [START_REF] Martin | On full abstraction for PCF: I, II, and III[END_REF][START_REF] Andrew D Ker | Innocent game models of untyped λ-calculus[END_REF] is thus naturally extended to the probabilistic and nondeterministic case.

First, we notice that the precise name given to variables in e.g. Figure 1a does not matter. Techniques like De Bruijn levels or indices do not apply here since we abstract infinitely many variables at each level -however, a variable occurrence is uniquely identified by a pointer to the node where it was abstracted, along with a number n, expressing that the variable

λx d 0 x d 1 x d 2 . . . • x d 0 1 3 δ VT d-1 (x d 1 ) + 2 3 δ VT d-1 (λz.z) δ VT d-1 (x d 2 ) δ VT d-1 (x d 3 ) . . .
where VT d-1 (x d l ) (for l ∈ N) and VT d-1 (λz.z) are

λx d-1 0 x d-1 1 x d-1 2 . . . • x d l δ VT d-2 (x d-1 0 ) δ VT d-2 (x d-1 1 ) . . . λx d-1 0 x d-1 1 x d-1 2 . . . • x d-1 0 δ VT d-2 (x d-1 1 ) δ VT d-2 (x d-1 2
) . . . and so on. ⊕ 0 was the (n + 1)-th introduced at this node. For example, the variable x d 0 is expressed with a pointed to the initial node, along with number 0. As a consequence of this representation, we can omit the abstractions: at each node, there are always countably many variables being introduced, and their name does not matter as they will be referred to differently.

0 i ⊕ 1 ⊕ 0 ⊕ i+1 j k . . . ⊕ j ⊕ k+1 . . . . . .
Next, we split each node of the Böhm tree into two: first a node intuitively carrying the abstractions (the target of pointers -we refer to these nodes as negative), and one carrying the variable occurrence (the source of pointers -we refer to those as positive). Besides bringing us closer to games, this allows us to easily distinguish the two kinds of branching of probabilistic Böhm trees. The different arguments of a variable node form a negative branching: each comes with its own (implicit) distinct set of fresh variables, and a subtree (by convention, we annotate by n the negative node corresponding to the nth argument). In contrast, for a probabilistic choice such as 1 3 1a, the two subtrees start by defining the same variables -so instead we represent this using a positive branching, where we further annotate the first node of each branch with its probability.

δ VT d-1 (x d 1 ) + 2 3 δ VT d-1 (λz.z) in Figure
Altogether, and ignoring the wiggly line for now, the reader may check that the diagram of Figure 1b matches the Böhm tree of Figure 1a according to these conventions (the correspondence will be made formal in Section 4). Read from top to bottom, these diagrams have an interactive flavour: they describe the actions of a player ⊕ depending on those of its opponent . Our formalisation in terms of strategies will follow this intuition.

Probabilistic Böhm trees as probabilistic event structures

Now, we formalise the representation introduced above as a probabilistic strategy in the sense of [START_REF] Winskel | Distributed probabilistic and quantum strategies[END_REF], i.e. a form of probabilistic event structure. In this section we only provide this as a static representation, and leave the mechanism to compose strategies for Section 3. Our strategies (such as the one of Figure 1b) involve a partial order: the dependency relation (going from top to bottom); a relation indicating conflict and generated by probabilistic choice; and an annotation for probabilities. These are naturally formalised as probabilistic concurrent strategies [START_REF] Winskel | Distributed probabilistic and quantum strategies[END_REF] (though for the purposes of this paper we will only make use of sequential such strategies). We first recall the definition of event structures. C S L 2 0 1 8

16:6

Fully Abstract Models of the Probabilistic λ-calculus Definition 4. An event structure [START_REF] Winskel | Events in Computation[END_REF] is a tuple (E, ≤, Con) where E is a set of events, ≤ a partial order indicating causal dependency, and Con a non-empty set of consistent finite subsets of E, such that

[e] = {e | e ≤ e} is finite for all e ∈ E {e} ∈ Con for all e ∈ E Y ⊆ X ∈ Con =⇒ Y ∈ Con X ∈ Con and e ≤ e ∈ X =⇒ X ∪ {e} ∈ Con.
The event structures we consider additionally have a polarity function pol : E → {+, -} indicating for each event whether it is a move of Player (+) or Opponent (-). We call them event structures with polarity (esps).

We fix some notation. Write e e for immediate causality, i.e. e < e with no events in between. Write C(E) for the set of finite configurations of E, i.e. those finite x ⊆ E such that x ∈ Con and x is down-closed: if e ≤ e ∈ x then e ∈ x. If E has polarity, we sometimes annotate an event e to specify its polarity, as in e + , e -. If x, y ∈ C(E), write x ⊆ + y (resp.

x ⊆ -y) if x ⊆ y and every event in y \ x has positive (resp. negative) polarity.

Ignoring probabilities and pointers, the diagram of Figure 1b is an esp: ≤ is the transitive reflexive closure of , and consistent sets are those finite sets whose down-closure do not contain two events related by the immediate conflict

. We now equip esps with probabilities, which comes in the form of a [0, 1]-valued function called a valuation.

For the forest-like event structures required to represent probabilistic λ-terms, it suffices to fix, for each Opponent event, a probability distribution on the Player events that immediately follow, as in Figure 1b. But to compose them we apply the more general machinery of [START_REF] Winskel | Distributed probabilistic and quantum strategies[END_REF], where valuations assign a coefficient to each configuration and not simply to each event. For x ∈ C(E), the coefficient v(x) is the probability that the configuration x will be reached in an execution, provided the Opponent moves in x occur. The following definition is from [START_REF] Winskel | Distributed probabilistic and quantum strategies[END_REF]: Definition 5. A probabilistic event structure with polarity consists of an esp (E, ≤ , Con, pol) and a valuation, that is, a map v :

C(E) → [0, 1] satisfying v(∅) = 1; if x ⊆ -y, then v(x) = v(y); and if y ⊆ + x 1 , . . . , x n , then v(y) ≥ I (-1) |I|+1 v i∈I x i
where I ranges over non-empty subsets of {1, . . . , n} such that i∈I x i is a configuration.

Leaving aside pointers the diagram of Figure 1b represents a probabilistic esp, setting the valuation of a configuration x to be 1 3 (resp. 2 3 ) if it contains the event annotated with 1 3 (resp. 2 3 ), and 1 otherwise -a configuration cannot contain both labelled events. Probabilistic strategies are certain probabilistic esps, equipped with a labelling map into the game they play on. Games are themselves esps, with the following particular shape:

Definition 6. An arena is an esp A which is forest-shaped: if a, b, c ∈ A with a ≤ b and c ≤ b then a ≤ c or c ≤ a; and alternating: if a b then pol(a) = pol(b). race-free: if x ∈ C(A) has x ⊆ -y ∈ C(A) and x ⊆ + z ∈ C(A), then y ∪ z ∈ C(A).
Usually in game semantics, arenas represent types. For our untyped language, strategies representing terms all play on a universal arena U , introduced soon. For now though, we define a probabilistic strategy playing on arbitrary arena A as an esp, labelled by A. Definition 7. A probabilistic strategy on A consists of a probabilistic esp S, and a labelling function σ : S → A on events, preserving polarity, and such that:

(1) σ preserves configurations: for every x ∈ C(S), σx ∈ C(A);

(2) σ is locally injective: if s, s ∈ x ∈ C(S) and σs = σs , then s = s ;

(3) σ is receptive: for x ∈ C(S), if σx ⊆ -y ∈ C(A), there is a unique x ⊆ x ∈ C(S) such that σx = y; (4) σ is courteous: for s, s ∈ S, if s S s and if pol(s) = + or pol(s ) = -, then σs A σs . Conditions ( 1) and ( 2) express that σ is a map of event structures from S to A. Conditions (3) and ( 4) are there to restrict the behaviour of Player: they prevent any further constraints from being put on Opponent events than those already specified by the game.

The diagram of Figure 1b presents a probabilistic strategy σ : S → A -or more precisely the diagram presents S, with the pointers being representations of the immediate dependency in A of positive moves (though we do not display A for lack of space).

Winskel [START_REF] Winskel | Distributed probabilistic and quantum strategies[END_REF], building on previous work [START_REF] Rideau | Concurrent strategies[END_REF], showed how to compose probabilistic strategies and organise them into a category. But his games are affine, and cannot deal with the replication of resources. In recent work [START_REF] Castellan | The Concurrent Game Semantics of Probabilistic PCF[END_REF], we have extended probabilistic strategies with symmetry, that augments the expressivity of esps by allowing interchangeable copies of the same event. In the next section we introduce probabilistic strategies with symmetry, and give the interpretation of Λ + . Because of this replication of resources the interpretation of the term M 1 of Figure 1 will be an expansion of Figure 1b, taking into account Opponent's replications -and in general, our correspondence theorem will associate a probabilistic Böhm tree with its expansion in that sense, formulated as a probabilistic strategy.

3

Game semantics for Λ +

In this section we construct our game semantics for Λ + . The category of games we use is close to our earlier concurrent games model of probabilistic PCF [START_REF] Castellan | The Concurrent Game Semantics of Probabilistic PCF[END_REF], in which we introduce a universal arena inspired from [START_REF] Andrew D Ker | Innocent game models of untyped λ-calculus[END_REF].

Games and strategies with symmetry

Symmetry in event structures [START_REF] Winskel | Event structures with symmetry[END_REF] can be presented via isomorphism families: Definition 8. An isomorphism family on an event structure E is a set E of bijections between configurations of E, such that: E contains all identity bijections, and is closed under composition and inverse of bijections. For every θ :

x ∼ = y ∈ E and x ∈ C(E) such that x ⊆ x, then θ| x ∈ E.
For every θ : x ∼ = y ∈ E and every extension x ⊆ x ∈ C(E), there exists a (non-necessarily unique) y ⊆ y ∈ C(E) and an extension θ ⊆ θ such that θ : x ∼ = y ∈ E.

As usual [START_REF] Winskel | Event structures with symmetry[END_REF], it follows from these axioms that any θ ∈ E is an order-isomorphism, i.e. preserves and reflects the order. An event structure with symmetry is a pair (E, E), with E an isomorphism family on E. If E has polarity, then we ask that every θ ∈ E preserves it, and call (E, E) an event structure with symmetry and polarity (essp).

C S L 2 0 1 8 16:8 Fully Abstract Models of the Probabilistic λ-calculus

We illustrate this definition by presenting as an essp the universal arena -the game that Λ + strategies will play on. It is an infinitely deep tree, with at every level, ω available moves, corresponding to calls from one of the players to a variable in context. There are ω 'symmetric' copies of each move. Formally: Definition 9. The esp (U, ≤, Con, pol) is defined as having: events: U = (N × N) * , finite sequences of ordered pairs; causality: s ≤ t if s is a prefix of t; consistency: no conflicts, Con = P fin (U ); polarity:

pol(s) = -if |s| is even, + if it is odd.
In a pair (m, n) ∈ N × N, m represents the variable address (the subscript in Figure 1b) and n is the copy index of the move (not displayed in Figure 1b).

We now add symmetry to U , following the intuition that different copies of the same move should be interchangeable. The isomorphism family U is generated by an equivalence relation ∼ on events, defined as the smallest equivalence relation satisfying s ∼ s =⇒ s • (m, n) ∼ s • (m, n ) for any s, s ∈ U and m, n, n ∈ N. Then, a bijection θ : x ∼ = y between configurations of U is in U whenever for all e ∈ x, e ∼ θ(e).

The elements of U are reindexing bijections, which may update the copy indices of moves in a configuration. In the sequel, we will identify strategies differing only by the choice of positive copy indices, hence we need to formally identify the bijections in U which do not affect Opponent's copy indices. Because of the dual nature of games we must do the same for Player; thus we define ∼ + and ∼ -to be the smallest equivalence relations on U satisfying:

s ∼ p s =⇒ s • (m, n) ∼ p s • (m, n) (for p ∈ {+, -}) s ∼ + s and |s| is even =⇒ s • (m, n) ∼ + s • (m, n ) s ∼ -s and |s| is odd =⇒ s • (m, n) ∼ -s • (m, n )
for any s, s , m, n, n . Just like ∼ generates U , the relations ∼ + and ∼ -generate isomorphism families U + and U -, respectively.

In general, the compositional mechanism will require all arenas to come with similar data: Definition 10. A ∼-arena is a tuple A = (A, A, A -, A + ) with A an arena, and A, A -, and A + isomorphism families on A, such that A -and A + are subsets of A; if θ ∈ A -∩ A + then θ is an identity bijection; if θ ∈ A -and θ ⊆ -θ ∈ A then θ ∈ A -(where the notation ⊆ -makes sense since bijections preserve polarity); if θ ∈ A + and θ ⊆ + θ ∈ A then θ ∈ A + . In particular, ∼-arenas are certain thin concurrent games, in the terminology of [START_REF] Castellan | The Parallel Intensionally Fully Abstract Games Model of PCF[END_REF][START_REF] Castellan | Concurrent hyland-ong games[END_REF].

Lemma 11. U = (U, U , U -, U + ) is a ∼-arena.

The category PG

We now define a category with objects the ∼-arenas, and morphisms probabilistic ∼-strategies.

Let us first define some constructions on games: if A is a ∼-arena, its dual A ⊥ is the ∼-arena obtained by reversing the polarity of events in A, and swapping the positive and negative isomorphism families. If A and B are ∼-arenas, their parallel composition A B is the tuple (A B, A B, A -B -, A + B + ), where A B is the esp with events A + B (the tagged disjoint union), componentwise causal dependency and polarity, and consistent sets those of the form X A X B for X A ∈ Con A and X B ∈ Con B ; and where the parallel composition A B of isomorphism families A and B comprises bijections of the form θ :

x A x B ∼ = y A y B , defined as θ(1, a) = (1, θ A (a)) and θ(2, b) = (2, θ B (b)) for some θ A : x A ∼
= y A and θ B : x B ∼ = y B in the component iso families. Note that we will often make use of the parallel composition i∈I A i of a family of ∼-arenas; it is defined analogously.

With that in place, a probabilistic ∼-strategy from A to B is a probabilistic ∼strategy on the ∼-arena A ⊥ B. Given σ : S → A ⊥ B and τ : T → B ⊥ C, we can form their interaction as the pullback

T S Π1 u u Π2 ) ) S C σ C ( ( A T A τ u u A B C
in the category of event structures with symmetry (and without polarity). The interaction is probabilistic:

for any configuration x ∈ C(T S), we set v T S (x) = v S ((Π 1 x) S ) × v T ((Π 2 x) T ), where (Π 1 x) S is the S-component of Π 1 x ∈ C(S C
), and likewise for (Π 2 x) T . The resulting map τ σ : T S → A B C is not quite a probabilistic ∼-strategy, because σ and τ play on dual versions of B, making ambiguous the polarity of some events.

So as in [START_REF] Rideau | Concurrent strategies[END_REF][START_REF] Castellan | Symmetry in Concurrent Games[END_REF], the composition of S and T is obtained after hiding those moves of the interaction which act as synchronisation events -the moves e ∈ T S such that (τ σ)e = (2, b) for some b ∈ B. The remaining set of events (so-called visible) induces an event structure T S with all structure inherited from T S, and polarity induced from A ⊥ C. Any configuration x ∈ C(T S) has a unique witness [x] ∈ C(T S). The isomorphism family T S comprises bijections θ : x ∼ = y such that there is θ : [x] ∼ = [y] in T S with θ ⊆ θ . We get a map τ σ : T S → A ⊥ C which satisfies all the conditions for a probabilistic ∼-strategy, with v T S (x) = v T S ([x]) for every x ∈ C(T S).

C S L 2 0 1 8 16:10 Fully Abstract Models of the Probabilistic λ-calculus

Copycat

As usual in game semantics, the identity morphism on a ∼-arena A will be a probabilistic ∼-strategy cc A : C C A → A ⊥ A called copycat, in which Player deterministically copies the behaviour of Opponent -so any Opponent move immediately triggers the corresponding Player move in the dual game, with probability 1. Formally, C C A has the same events, polarity, and consistent subsets as A ⊥ A and the extra immediate causal dependencies

{((1, a), (2, a)) | a ∈ A, pol A ⊥ (a) = -} and {((2, a), (1, a)) | a ∈ A, pol A (a) = -} (from this ≤ C C A is obtained by transitive closure).
Copycat has an isomorphism family C C A which we do not define here for lack of space (it can be found e.g. in [START_REF] Castellan | Concurrent hyland-ong games[END_REF]). Together with the valuation v C C A (x) = 1 for all x ∈ C(C C A ), this turns copycat into a probabilistic ∼-strategy.

Recall that strategies are considered up to weak isomorphism (Definition 13). Doing so crucially relies on the thinness axiom on strategies, which implies [START_REF] Castellan | Concurrent hyland-ong games[END_REF] that weak isomorphism is stable under composition, so that we may perform a quotient and retain a well-defined notion of composition. Though identity and associativity laws for strategies only hold up to isomorphism, the quotient will turn them into strict equalities. So as in [START_REF] Castellan | The Concurrent Game Semantics of Probabilistic PCF[END_REF], we have: Lemma 14. There is a category PG having objects: ∼-arenas morphisms A + → B: weak isomorphism classes of probabilistic ∼-strategies on A ⊥ B.

Categorical structure

PG itself is a compact closed category, but we are interested in the subcategory PG -, where ∼-arenas and strategies are negative (that is, all initial moves are negative), and strategies are moreover well-threaded (meaning that events in S depend on a unique initial move). Finally there is a linear exponential comonad [START_REF] Mellies | Categorical semantics of linear logic[END_REF] ! on PG -. Given A ∈ PG -, the ∼-arena !A is an expanded version of A with countably many copies of every move. Accordingly, the esp !A is simply i∈ω A, and the bijections in !A are those θ : i∈I x i ∼ = j∈J y j such that there exists a permutation π : I ∼ = J and bijections θ i ∈ A with θ((i, a)) = (πi, θ i a) for all (i, a) ∈ i∈I x i . Recall that A is negative, so the set !A + of positive bijections (those in which only Player moves are reindexed) comprises those θ ∈ !A for which I = J and π : I → J is the identity function, and such that each θ i ∈ A + . On the other hand, bijections in !A -can consist of any π : I ∼ = J, so long as θ i ∈ A -for all i.

We leave out all further details of the categorical structure of PG -, including the various constructions on morphisms. It can be shown that PG -, together with the data above, is a model of Intuitionistic Linear Logic. From here it is standard that the Kleisli category for ! is a ccc: → B is the evaluation morphism.

16:11

Interpretation of Λ +

We finally come to our interpretation of Λ + terms as probabilistic strategies. We start by imposing one key new condition on strategies: sequential innocence. The cut-down model will be closer to the language, allowing us to prove a correspondence result in Section 4. We assume from now on that all strategies are negative and well-threaded: Definition 16. A probabilistic ∼-strategy σ : S → A is sequential innocent if a subset X ⊆ S is a configuration if and only if it is an Opponent-branching tree (that is, causality is tree-shaped and if a b and a c in X then pol(a) = +) and σX ∈ C(A); for every x, y, z ∈ C(S) such that x = y ∩ z and y ∪ z ∈ C(S), either v(x) = 0 or

v(y ∪ z) v(x) = v(y) v(x) v(z) v(x) .
Less formally, innocence forces the independence (causal and probabilistic) of Opponentforking branches of the strategy. Sequential innocent probabilistic ∼-strategies are closed under composition, stable under weak isomorphism, and copycat verifies all conditions, so we can consider the subcategory PG si ! of PG ! consisting of those strategies. It is easy to check that PG si ! is still a ccc; it is the category we will use to interpret Λ + , and in what follows we refer to PG si ! -strategies simply as Λ + -strategies.

A reflexive object

Recall the ∼-arena U defined in 3.1. It is a reflexive object, meaning that there are maps λ ∈ PG si ! (U ⇒ U, U) and app ∈ PG si ! (U, U ⇒ U) such that app λ = id U ⇒U . It is easy to see that there is an isomorphism of essps ρ : U ∼ = U ⇒ U. To turn this into a isomorphism is PG si ! , we can lift it to a copycat-like strategy which "plays following ρ". Details of this lifting are omitted but can be found in [START_REF] Castellan | Concurrent hyland-ong games[END_REF].

Closed terms of the probabilistic λ-calculus are interpreted as probabilistic strategies on U. Open terms M with free variables in Γ are interpreted as Λ + -strategies M Γ : U Γ + → U, where U Γ = ˘x∈Γ U. The interpretation of the λ-calculus constructions is standard, using that U is a reflexive object in a ccc:

x Γ = π x , the x th projection λx.M Γ = λ cur( M Γ,x ) M N Γ = ev U ,U app M Γ , N Γ
In order to give an interpretation to the probabilistic choice operator, we must define the sum of two strategies. Let σ : S → (U Γ ) ⊥ U and τ : T → (U Γ ) ⊥ U be Λ + -strategies, and let p ∈ [0, 1]. The essp S + p T has a unique initial Opponent move (as do S and T -wlog call this move ε), and continues as either S or T non-deterministically. That is, it has events C S L 2 0 1 8

16:12

Fully Abstract Models of the Probabilistic λ-calculus {ε} (S \ {ε}) (T \ {ε}), and all structure induced from S and T , with X ∈ Con S+pT iff X ∈ Con S or X ∈ Con T . We define v S+pT (x) to be 1 if x = ∅, {ε}, pv S (x) if x ∈ C(S), and (1 -p)v T (x) if x ∈ C(T ). The obvious map σ + p τ : S + p T → (U Γ ) ⊥ U is a Λ + -strategy, and the interpretation of the syntactic + p is simply M + p N Γ = M Γ + p N Γ . We have: Theorem 17 (Adequacy). For any M ∈ Λ + 0 , writing σ : S → U for M , we have

Pr ⇓ (M ) = x∈C(S) |x + |=1 v S (x),
where x + is the set of positive events of x.

We only state the result at this point; it will follow directly from the interpretation-preserving functor of Section 5 and the adequacy of the weighted relational model for Λ + . A direct corollary of Theorem 17 is the following soundness result:

Lemma 18 (Soundness). For any M, N ∈ Λ + with free variables in Γ, if M Γ = N Γ then M = obs N .
In fact we will prove in Section 5 that the converse, full abstraction, also holds modulo a mild (effective) quotient. It will also follow that the weighted relational model itself is also fully abstract, which was open. These facts rely on Leventis' result [START_REF] Leventis | Probabilistic lambda-theories[END_REF] along with the formal correspondence between strategies and Böhm trees, to which we now move on.

4

The Correspondence Theorem

In [START_REF] Andrew D Ker | Innocent game models of untyped λ-calculus[END_REF], the authors prove an exact correspondence theorem for the pure λ-calculus: infinitely extensional Böhm trees precisely correspond to deterministic innocent strategies on a universal arena. They work in a different games framework, but the analogous phenomenon occurs in ours (the main technical difference, if we were to conduct the proof in the deterministic case, would be the explicit duplication of moves: our strategies are expanded, in order to accommodate Opponent's choice of copy index for every move). For Λ + however, the correspondence is not so exact: although terms M and M + p M have the same probabilistic Böhm tree, they have different interpretations in PG si ! , where each probabilistic choice is recorded as an explicit branching point. 2 In what follows, we identify a class of Böhm tree-like probabilistic strategies for which the exact correspondence does hold, and we show that any strategy can be reduced to a Böhm tree-like one. Two strategies can then be considered equivalent if they reduce to the same.

First, given a Λ + -strategy σ : S → U, define a relation ≈ on the events of S as the smallest equivalence relation such that if s 1 ≈ s 1 , s 1 s 2 , s 1 s 2 and there is an order-isomorphism

ϕ : {s ∈ S | s 2 ≤ s} ∼ = {s ∈ S | s 2 ≤ s } such that σ s ∼ + (σ • ϕ) s for all s ≥ s 2 , then s 2 ≈ s 2 .
Informally, ≈ identifies events coming from the same syntactic construct in two copies of a term in an idempotent probabilistic sum, as in M + p M (where Opponent has played the same copy indices). Definition 19. We say σ is Böhm tree-like if it satisfies (1) for every x ∈ C(S), v S (x) > 0; and (2) for every s, s ∈ S, if s ≈ s then s = s .

P. Clairambault and H. Paquet 16:13

In other words, a Böhm tree-like strategy is one with no redundant branches. Many Λ + -strategies do not satisfy this property, but all can be reduced to one that does: Definition 20. Given a Λ + -strategy σ : S → U, let S bt be the set of ≈-equivalence classes containing at least one event s such that v S ([s]) > 0 (where [s] is the down-closure of s).

It is direct to turn S bt into an essp S bt with structure induced by S. The (partial) quotient map f : S → S bt is then used to push-forward the valuation, i.e.

v S bt (x) = y∈C(S) f y=x v S (y).
Then, σ bt : S bt → U is a Böhm tree-like Λ + -strategy. Write σ = bt τ when σ bt = τ bt .

We can now make formal the connection between Λ + -strategies and probabilistic Böhm trees. To do so we define a bijective map from the set of Böhm tree-like Λ + -strategies of depth d on (U Γ ) ⊥ U, to the set PT We can show by induction on d:

Lemma 22. For every d ∈ N and every Γ ⊆ fin Var there is a bijection

Ψ d Γ : {σ bt | σ ∈ PG si ! (U Γ , U) and depth σ ≤ d} ∼ = -→ PT d Γ .
Proof (sketch). In Section 2.3, we motivated the definition of probabilistic strategies via a geometric correspondence with probabilistic Böhm trees, to be expected in the light of standard definability results in game semantics. However, probabilistic strategies differ from the picture of Section 2.3 due to the necessity for Player to acknowledge Opponent's replications, spawning countably many symmetric copies of branches starting with an Opponent move. It follows however from the axioms of symmetry that events differing only by Opponent's choice of copy indices have isomorphic futures. One can, with no loss of information, focus on a sub-strategy where Opponent performs no duplication, and apply the correspondence explained in Section 2.3.

We now show that this bijection preserves the interpretation of Λ + .

Theorem 23 (Correspondence theorem). For any

M ∈ Λ + and d ∈ N, Ψ d Γ (( M d ) bt ) = PT d (M )
, where M d is the maximal sub-strategy of M with depth ≤ d.

Proof (sketch).

The proof is by induction on d, and follows a similar argument as in the non-probabilistic case [START_REF] Andrew D Ker | Innocent game models of untyped λ-calculus[END_REF], with the additional difficulty of dealing with infinite width: a probabilistic Böhm tree may be a probability distribution with infinite support, and the first level of Player moves in a probabilistic strategy may be infinite. One must therefore consider finite-width approximations.

Probabilistic strategies are traditionally ordered using a probabilistic version of the prefix order: given σ : S → A and τ : T → A we say σ τ if S ⊆ T (i.e. S ⊆ T and all data is inherited), and for all x ∈ C(S), v S (x) ≤ v T (x). However the naive restriction of this order to the set of Böhm tree-like strategies is not sensible, because σ τ does not imply σ bt τ bt . An alternative is given by Leventis [16, p. 111 Under the set PT d Γ is a cpo, and we also call the corresponding order on the set of Böhm tree-like strategies (this automatically makes Ψ d Γ a continuous bijection). Leventis proves the crucial property that for every term M there is a chain t 0 , t 1 , . . . of finite-width trees satisfying PT d (M ) = t i . Replaying his argument in our game semantics, we show that the chain Ψ

d Γ -1 (t i ), i ∈ N has lub ( M d ) bt . We conclude, because Ψ d Γ -1 PT d Γ (M ) = Ψ d Γ -1 i∈N t i = i∈I Ψ d Γ -1 (t i ) = ( M d ) bt .
Using the correspondence it follows easily that:

Lemma 24. For any M, N ∈ Λ + , M = PT N if and only if M = bt N .
Theorem 25 (Full abstraction). The model PG si ! / = bt is fully abstract, i.e. M = obs N if and only if M = bt N .

Weighted Relational Semantics

In this final section, we consider the weighted relational model of Λ + . It lives in the category PRel ! whose objects are sets and whose morphisms are certain matrices with coefficients in the set R + = R + ∪ {∞}. This interpretation of probabilistic λ-terms was first suggested in [START_REF] Ehrhard | The computational meaning of probabilistic coherence spaces[END_REF], where authors consider the category PCoh ! of probabilistic coherence spaces, a refinement (using biorthogonality) of the model PRel ! presented here. PCoh ! has desirable properties (notably, all coefficients are finite) but because there is a faithful functor PCoh ! → PRel ! preserving the interpretation of Λ + , all the results of [START_REF] Ehrhard | The computational meaning of probabilistic coherence spaces[END_REF] hold for the simpler model PRel ! , which we focus on in this paper and proceed to define.

The weighted relational model of Λ +

We use the notation PRel ! to indicate that the model is obtained as the Kleisli category for a comonad !, much like PG ! . The underlying category PRel is a well-known model of intuitionistic linear logic (see e.g. [START_REF] Laird | Weighted relational models of typed lambda-calculi[END_REF]), but we skip its construction and give a direct presentation of PRel ! :

Definition 26. The category PRel ! is defined as follows: objects: sets;

morphisms from X to Y : maps ϕ : M f (X) × Y → R + , where M f (X) is the set of finite multisets of elements of X; composition: for ϕ ∈ PRel ! (X, Y ), ψ ∈ PRel ! (Y, Z), define ψ • ϕ : M f (X) × Z → R + as (ψ • ϕ)(m, c) = p∈M f (Y ) ψ p,c (m b ) b∈p s.t. m= m b b∈p ϕ (m b ,b)
for every m ∈ M f (X) and c ∈ Z. identity: for any set X, and for any m ∈ M f (X) and a ∈ X, define

Relational collapse

We now connect the two models via a functor ↓ : PG si ! → PRel ! , which intuitively forgets the causal information in a strategy, only remembering the states reached during the execution.

If (E, E) is an event structure with symmetry, write ∼ = for the equivalence relation on C(E) defined as x ∼ = y if and only if there is θ : x ∼ = y in E. For A an arbitrary negative ∼-arena, the set ↓ A is then defined as the quotient {x ∈ C(A) | x non-empty}/ ∼ =.

For any A, B, there is a bijection ↓(A ⇒ B) M f (↓ A)×↓ B, enabling morphisms of PG si

Conclusion

An immediate corollary of Theorem 31 is that the probabilistic coherence space model of [START_REF] Ehrhard | The computational meaning of probabilistic coherence spaces[END_REF] is fully abstract, since PCoh ! and PRel ! induce the same equational theory on Λ + terms. Interestingly, the results of this paper should further entail that the interpretation of Λ + in the simpler model of Danos and Harmer [START_REF] Danos | Probabilistic game semantics[END_REF] is also fully abstract, since one can in C S L 2 0 1 8

16:16

Fully Abstract Models of the Probabilistic λ-calculus principle map our strategies functorially to theirs. Note however that since it is not known how to state a notion of probabilistic innocence in Danos and Harmer's model, definability fails and the present work could not have been carried out there.

So using probabilistic concurrent games, we obtain probabilistic analogues of wellestablished results from the theory of the pure λ-calculus: the correspondence between Böhm trees and innocent strategies [START_REF] Andrew D Ker | Innocent game models of untyped λ-calculus[END_REF], and the full abstraction property of the relational model [START_REF] Bucciarelli | Not enough points is enough[END_REF].

Definition 1 .

 1 For each d ∈ N, the sets PT d of probabilistic Böhm trees of depth d and VT d of value trees of depth d are defined as:

( a )

 a As a value tree of depth d ≥ 2.

  As a probabilistic strategy.

Figure 1 3 (

 13 Figure 1 Two interpretations of the term M1 = λxy.x (y + 1 3 (λz.z)).

9 ( 3 )Definition 13 .

 9313 Strategies are in turn equipped with symmetry: Definition 12. A probabilistic essp is an essp S with a valuation v : C(S) → [0, 1], such that for every θ : x ∼ = y in S, v(x) = v(y). A probabilistic ∼-strategy on a ∼-arena A consists of a probabilistic essp S, and a labelling σ : S → A, such that:(1) the underlying map σ : S → A is a strategy;(2) σ preserves symmetry: if θ :x ∼ = y ∈ S then σθ : σx ∼ = σy defined as {(σ s, σ s ) | (s, s ) ∈ θ}, is in A (that is, it is a map of essps (S, S) → (A, A)); σ is ∼-receptive: if θ ∈ S and σθ ⊆ -ψ ∈ A, there is a unique θ ⊆ θ ∈ S s.t. σθ = ψ. (4) S is thin: for θ : x ∼ = y in S with x ⊆ + x∪{s}, there is a unique t ∈ S s.t. θ∪{(s, t)} ∈ S. Finally, before we define our category of games and strategies with symmetry, let us say what it means for strategies to be the same up to Player copy indices: Probabilistic ∼-strategies σ : S → A and τ : T → A are weakly isomorphic if there is an isomorphism of essps ϕ : S → T , such that for any x ∈ C(S), v S (x) = v T (ϕx), and moreover the diagram S σ ϕ / / T τ } } A commutes up to positive symmetry, in the sense that for any x ∈ C(S), the set {(σe, τ (ϕe)) | e ∈ x} is (the graph of) a bijection in A + .

  Let A and B be objects of PG -. Their tensor product A ⊗ B is simply defined as A B. The tensorial unit is the empty ∼-arena, and moreover the tensor is closed: the function space A B has events those of ( min(B) A ⊥ ) B with same polarity. The causal dependency is induced, with extra causal links {((2, b), (1, (b, a))) | b ∈ min(B), a ∈ A}. The function χ : (A B) → A ⊥ B defined as (1, (b, a)) → (1, a) and (2, b) → (2, b) allows us to characterise consistent sets and iso families concisely: Con A B is defined as the largest set making χ a map of esps, and an order-isomorphism θ between configurations of A B is in A B iff χθ ∈ A ⊥ B. PG -also has cartesian products, with A & B defined as A B, only with consistent sets restricted to those of A ∅ and ∅ B. The rest of the structure, including symmetry, is induced from A B by restriction.

Lemma 15 .

 15 There is a cartesian closed category PG - ! having objects: negative ∼-arenas morphisms A + → B: (weak isomorphism classes of) negative and well-threaded probabilistic ∼-strategies on !A ⊥ B. With a slight abuse of notation, we shall keep using for composition in the Kleisli category PG - ! . We use the following notations for the cartesian closed structure: A ⇒ B is the function space !A B, cur is the bijection PG - ! (A & B, C) ∼ = PG - ! (A, B ⇒ C), and ev A,B : (A ⇒ B) & A +

  Γ d of probabilistic Böhm trees of depth d with free variables in Γ. Let us say first what we mean by the depth of a strategy: Definition 21. The depth of a Λ + -strategy σ : S → U, depth(σ), is the maximum number of Player moves in a chain s 0 • • • s n in S, and ∞ if such chains have unbounded length.

PRelM

  id X (m, a) = 1 if m = [a] ! is cartesian closed, with X & Y = X Y and X ⇒ Y = M f (X) × Y .There is a reflexive object D in PRel ! , supporting the interpretation of Λ + , and defined as the least fixed point of the operation mapping X to the set M f (X)(ω) of quasi-finite sequences of finite multisets over X, i.e. with all but finitely many elements equal to [ ]. Concretely, D is the lub of the chain D 0 , D 1 , . . . where D 0 = ∅ and D i+1 = M f (D i ) (ω) for all i. It is the case that D ∼ = D ⇒ D; the set-theoretical bijection and its lifting to a PRel ! isomorphism can be found in[START_REF] Ehrhard | The computational meaning of probabilistic coherence spaces[END_REF].Terms of Λ + are interpreted in the standard way, withM + p N Γ PRel ! (d) = p M Γ PRel ! (d)+ (1 -p) N ΓPRel ! (d) for every d ∈ D. We have:Theorem 27 (Adequacy[START_REF] Ehrhard | The computational meaning of probabilistic coherence spaces[END_REF]). For any M ∈ Λ + 0 , the map M PRel ! : D → R + satisfiesPr ⇓ (M ) =d∈D2 PRel ! (d).

!

  to be mapped to those of PRel ! : if σ : S → !A ⇒ B is a Λ + -strategy and x ∈ ↓(A ⇒ B) (so x is an equivalence class of configurations), the set of witnesses of x is defined as wit S (x) = {z ∈ C(S) | σz ∈ x and the maximal moves of z have polarity +}/ ∼ = . Because v S is invariant under symmetry, we can transport σ to ↓ σ :↓(A ⇒ B) → R + via ↓ σ(x) = z∈wit S (x) v S (z)for each x ∈ ↓(A ⇒ B). One can then easily deduce from the deadlock-free lemma of[START_REF] Castellan | The Concurrent Game Semantics of Probabilistic PCF[END_REF]:Lemma 28. ↓ is a functor PG si ! → PRel ! .Furthermore, ↓ preserves the interpretation of Λ + terms and is well-defined on the quotiented model PG si ! / = bt :Lemma 29. ↓ U ∼ = D and up to this iso, for anyM ∈ Λ + we have ↓ M PG si ! = M PRel ! . Lemma 30. If σ = bt τ then ↓ σ = ↓ τ .Combining the previous two lemmas and the soundness theorem, we finally get:Theorem 31 (Full abstraction). For any M, N ∈ Λ + with free variables in Γ , M = obs N if and only if M PRel ! = N PRel ! .

C S L 2 0 1 8 16:14 Fully Abstract Models of the Probabilistic λ-calculus

  ], who defines an order on the set

	PT d Γ , characterised in this setting as follows: t t iff there exists a strategy σ such that Ψ d Γ -1 (t) = bt σ and σ Ψ d Γ -1 (t ). Intuitively, the branches of σ are those of Ψ d Γ -1 (t),
	duplicated and assigned probability in such a way that they can be extended to those of
	Ψ d Γ	-1 (t ) using the prefix order .

Independently and using a different method, Leventis and Pagani have obtained an alternative proof of full abstraction, but this work is so far unpublished.

In particular, PG si ! does not yield a probabilistic λ-theory in the sense of Leventis[START_REF] Leventis | Probabilistic lambda-theories[END_REF].

Acknowledgements

This work was performed within the framework of the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX-0007) operated by the French National Research Agency (ANR).

1