Frédéric Chazal
email: frederic.chazal@inria.fr

Ilaria Giulini
email: ilaria.giulini@me.com

Bertrand Michel
email: bertrand.michel@ec-nantes.fr

Data driven estimation of Laplace-Beltrami operator

Approximations of Laplace-Beltrami operators on manifolds through graph Laplacians have become popular tools in data analysis and machine learning. These discretized operators usually depend on bandwidth parameters whose tuning remains a theoretical and practical problem. In this paper, we address this problem for the unnormalized graph Laplacian by establishing an oracle inequality that opens the door to a well-founded data-driven procedure for the bandwidth selection. Our approach relies on recent results by Lacour and Massart [LM15] on the so-called Lepski's method.

Introduction

The Laplace-Beltrami operator is a fundamental and widely studied mathematical tool carrying a lot of intrinsic topological and geometric information about the Riemannian manifold on which it is defined. Its various discretizations, through graph Laplacians, have inspired many applications in data analysis and machine learning and led to popular tools such as Laplacian EigenMaps [START_REF] Belkin | Laplacian eigenmaps for dimensionality reduction and data representation[END_REF] for dimensionality reduction, spectral clustering [START_REF] Von | A tutorial on spectral clustering[END_REF], or semi-supervised learning [START_REF] Belkin | Semi-supervised learning on riemannian manifolds[END_REF], just to name a few.

During the last fifteen years, many efforts, leading to a vast literature, have been made to understand the convergence of graph Laplacian operators built on top of (random) finite samples to Laplace-Beltrami operators. For example pointwise convergence results have been obtained in [START_REF] Belkin | Towards a theoretical foundation for laplacian-based manifold methods[END_REF] (see also [START_REF] Belkin | Towards a theoretical foundation for laplacian-based manifold methods[END_REF]) and [START_REF] Hein | Graph laplacians and their convergence on random neighborhood graphs[END_REF], and a (uniform) functional central limit theorem has been established in [START_REF] Giné | Empirical graph laplacian approximation of laplace-beltrami operators: Large sample results[END_REF]. Spectral convergence results have also been proved by [START_REF] Belkin | Convergence of laplacian eigenmaps[END_REF] and [START_REF] Von Luxburg | Consistency of spectral clustering[END_REF]. More recently, [START_REF] Ting | An analysis of the convergence of graph laplacians[END_REF] analyzed the asymptotic of a large family of graph Laplacian operators by taking the diffusion process approach previously proposed in [START_REF] Nadler | Diffusion maps, spectral clustering and reaction coordinates of dynamical systems[END_REF].

Graph Laplacians depend on scale or bandwidth parameters whose choice is often left to the user. Although many convergence results for various metrics have been established, little is known about how to rigorously and efficiently tune these parameters in practice. In this paper we address this problem in the case of unnormalized graph Laplacian. More precisely, given a Riemannian manifold M of known dimension d and a function f : M → R , we consider the standard unnormalized graph Laplacian operator defined by

∆h f (y) = 1 nh d+2 i K y -X i h [f (X i ) -f (y)] , y ∈ M,
30th Conference on Neural Information Processing Systems (NIPS 2016), Barcelona, Spain.

where h is a bandwidth, X 1 , . . . , X n is a finite point cloud sampled on M on which the values of f can be computed, and K is the Gaussian kernel: for y ∈ R m

K(y) = 1 (4π) d/2 e -y 2 m /4 , (1)
where y m is the Euclidean norm in the ambiant space R m .

In this case, previous results (see for instance [START_REF] Giné | Empirical graph laplacian approximation of laplace-beltrami operators: Large sample results[END_REF]) typically say that the bandwidth parameter h in ∆h should be taken of the order of n -1 d+2+α for some α > 0, but in practice, for a given point cloud, these asymptotic results are not sufficient to choose h efficiently. In the context of neighbor graphs [START_REF] Ting | An analysis of the convergence of graph laplacians[END_REF] proposes self-tuning graphs by choosing h locally in terms of the distances to the k-nearest neighbor, but note that k still need to be chosen and moreover as far as we know there is no guarantee for such method to be rate-optimal. More recently a data driven method for spectral clustering has been proposed in [START_REF] Rieser | A topological approach to spectral clustering[END_REF]. Cross validation [AC + 10] is the standard approach for tuning parameters in statistics and machine learning. Nevertheless, the problem of choosing h in ∆h is not easy to rewrite as a cross validation problem, in particular because there is no obvious contrast corresponding to the problem (see [AC + 10]).

The so-called Lepski's method is another popular method for selecting the smoothing parameter of an estimator. The method has been introduced by Lepski [Lep92b, [START_REF] Ov Lepskii | Asymptotically minimax adaptive estimation. ii. schemes without optimal adaptation: Adaptive estimators[END_REF][START_REF] Oleg | On problems of adaptive estimation in white gaussian noise[END_REF] for kernel estimators and local polynomials for various risks and several improvements of the method have then been proposed, see [LMS97, GL09, GL + 08]. In this paper we adapt Lepski's method for selecting h in the graph Laplacian estimator ∆h . Our method is supported by mathematical guarantees: first we obtain an oracle inequality -see Theorem 3.1 -and second we obtain the correct rate of convergence -see Theorem 3.3 -already proved in the asymptotical studies of [START_REF] Belkin | Towards a theoretical foundation for laplacian-based manifold methods[END_REF] and [START_REF] Giné | Empirical graph laplacian approximation of laplace-beltrami operators: Large sample results[END_REF] for non data-driven choices of the bandwidth. Our approach follows the ideas recently proposed in [START_REF] Lacour | Minimal penalty for goldenshluger-lepski method[END_REF], but for the specific problem of Laplacian operators on smooth manifolds. In this first work about the data-driven estimation of Laplace-Beltrami operator, we focus as in [START_REF] Belkin | Towards a theoretical foundation for laplacian-based manifold methods[END_REF] and [START_REF] Giné | Empirical graph laplacian approximation of laplace-beltrami operators: Large sample results[END_REF] on the pointwise estimation problem: we consider a smooth function f on M and the aim is to estimate ∆f for the L 2 -norm • 2,M on M ⊂ R m . The data driven method presented here may be adapted and generalized for other types of risks (uniform norms on functional family and convergence of the spectrum) and other types of graph Laplacian operators, this will be the subject of future works.

The paper is organized as follows: Lepski's method is introduced in Section 2. The main results are stated in Section 3 and a sketch of their proof is given in Section 4 (the complete proofs are given in the supplementary material). A numerical illustration and a discussion about the proposed method are given in Sections 5 and 6 respectively. 2 Lepski's procedure for estimating the Laplace-Beltrami operator All the Riemannian manifolds considered in the paper are smooth compact d-dimensional submanifolds (without boundary) of R m endowed with the Riemannian metric induced by the Euclidean structure of R m . Recall that, given a compact d-dimensional smooth Riemannian manifold M with volume measure µ, its Laplace-Beltrami operator is the linear operator ∆ defined on the space of smooth functions on M as ∆(f ) = -div(∇f ) where ∇f is the gradient vector field and div the divergence operator. In other words, using the Stoke's formula, ∆ is the unique linear operator satisfying

M ∇f 2 dµ = M ∆(f )f dµ.
Replacing the volume measure µ by a distribution P which is absolutely continuous with respect to µ, the weighted Laplace-Beltrami operator ∆ P is defined as

∆ P f = ∆f + 1 p ∇p, ∇f , (2)
where p is the density of P with respect to µ. The reader may refer to classical textbooks such as, e.g., [START_REF] Rosenberg | The Laplacian on a Riemannian manifold: an introduction to analysis on manifolds[END_REF] or [START_REF] Grigoryan | Heat kernel and analysis on manifolds[END_REF] for a general and detailed introduction to Laplace operators on manifolds.

In the following, we assume that we are given n points X 1 , . . . , X n sampled on M according to the distribution P. Given a smooth function f on M , the aim is to estimate ∆ P f , by selecting an estimator in a given finite family of graph Laplacian ( ∆h f ) h∈H , where H is a finite family of bandwidth parameters.

Lepski's procedure is generally presented as a method for selecting bandwidth in an adaptive way. More generally, this method can be seen as an estimator selection procedure.

Lepski's procedure

We first shortly explain the ideas of Lepski's method. Consider a target quantity s, a collection of estimators (ŝ h ) h∈H and a loss function (•, •). A standard objective when selecting ŝh is trying to minimize the risk E (s, ŝh ) among the family of estimators. In most settings, the risk of an estimator can be decomposed into a bias part and a variance part. Of course neither the risk, the bias nor the variance of an estimator are known in practice. However in many cases, the variance term can be controlled quite precisely. Lepski's method requires that the variance of each estimator ŝh can be tightly upper bounded by a quantity v(h). In most cases, the bias can be written as (s, sh ) where sh corresponds to some (deterministic) averaged version of ŝh . It thus seems natural to estimate (s, sh ) by (ŝ h , ŝh ) for some h smaller than h. The later quantity incorporates some randomness while the bias does not. The idea is to remove the "random part" of the estimation by considering [ (ŝ h , ŝh ) -v(h) -v(h )] + , where [ ] + denotes the positive part. The bias term is estimated by considering all pairs of estimators (s h , ŝh ) through the quantity

sup h ≤h [ (ŝ h , ŝh ) -v(h) -v(h )] + .
Finally, the estimator minimizing the sum of the estimated bias and variance is selected, see eq. (3) below.

In our setting, the control of the variance of the graph Laplacian estimators ∆h is not tight enough to directly apply the above described method. To overcome this issue, we use a more flexible version of Lepski's method that involves some multiplicative coefficients a and b introduced in the variance and bias terms. More precisely, let

V (h) = V f (h) be an upper bound for E[ (E[ ∆h ] -∆h )f 2 2,M ]
. The bandwidth ĥ selected by our Lepski's procedure is defined by

ĥ = ĥf = arg min h∈H {B(h) + bV (h)} (3)
where

B(h) = B f (h) = max h ≤h, h ∈H ( ∆h -∆h )f 2 2,M -aV (h ) + (4)
with 0 < a ≤ b. The calibration of the constants a and b in practice is beyond the scope of this paper, but we suggest a heuristic procedure inspired from [START_REF] Lacour | Minimal penalty for goldenshluger-lepski method[END_REF] in section 5.

Variance of the graph Laplacian for smooth functions

In order to control the variance term, we consider for this paper the set F of smooth functions f : M → R uniformly bounded up to the third order. For some constant C F > 0 , let

F = f ∈ C 3 (M, R) , f (k) ∞ ≤ C F , k = 0, . . . , 3 (5)
Here, by f (k) ∞ ≤ C F we mean that in any normal coordinate systems all the partial derivatives of order k of f are bounded by C F .

We introduce some notation before giving the variance term for f ∈ F. Define

D α = 1 (4π) d R d C u α+2 d 2 + C 1 u α d e -u 2 d /4 du (6) Dα = 1 (4π) d/2 R d C u α+2 d 4 + C 1 u α d e -u 2 d /8 du (7)
where d is the euclidean norm in R d and where C and C 1 are geometric constants that only depend on the metric structure of M (see Lemma 6.1 in the appendices). We also introduce the d-dimensional Gaussian kernel on R d :

K d (u) = 1 (4π) d/2 e -u 2 d /4 , u ∈ R d
and we denote by • p,d the L p -norm on R d . The next proposition provides an explicit bound V (h) on the variance term. Let

ω d = 3 × 2 d/2-1 (8)
and

α d (h) = h 2 D 4 + 3 2 ω d K d 2 2,d + 2µ(M ) (4π) d + h 4 D 6 4 . (9)
We first need to control the variance of ∆h f over F. This will be possible by considering Taylor Young expansions of f in normal coordinates. For that purpose, for technical reasons following from Lemma 6.1, we constrain the parameter h to satisfy the following inequality

2 √ d + 4h log(h -1 ) 1/2 ≤ ρ(M ), (10)
where ρ(M ) is a geometric constant that only depends on the reach and the injectivity radius of M. Proposition 2.1. Given h ∈ H and for any f ∈ F, we have

V (h) := 2C 2 F nh d+2 w d K d 2 2,d + α d (h) ≤ E[ (E[ ∆h ] -∆h )f 2 2,M ].
For the proof we refer to section 6.1.

Results

We now give the main result of the paper: an oracle inequality for the estimator ∆ĥ , or in other words, a bound on the risk that shows that the performance of the estimator is almost as good as it would be if we knew the risks of each estimator. In particular it performs an (almost) optimal trade-off between the variance term V (h) and the approximation term

D(h) = D f (h) = max (p∆ P -E[ ∆h ])f 2,M , sup h ≤h (E[ ∆h ] -E[ ∆h ])f 2,M ≤ 2 sup h ≤h (p∆ P -E[ ∆h ])f 2,M .
Theorem 3.1. According to the notation introduced in the previous section, let = √ a/2 -1 and

δ(h) = h ≤h max exp - min{ 2 , } √ n 24 , exp - 2 3 γ d (h )
and

γ d (h) = 1 h d p ∞ ω d K d 2 2,d + α d (h) (ω d K d 1,d + β d (h)) 2
where α d is defined by (9) and where

β d (h) = h ω d K d 1,d + 2µ(M ) (4π) d/2 + h 2 D3 + h 3 D4 2 . ( 11
)
Given f ∈ C 2 (M, R), with probability at least 1 -2 h∈H δ(h),

(p∆ P -∆ĥ )f 2,M ≤ inf h∈H 3D(h) + (1 + √ 2) bV (h) .
Broadly speaking, Theorem 3.1 says that there exists an event of large probability for which the estimator selected by Lepski's method is almost as good as the best estimator in the collection. Note that the size of the bandwidth family H has an impact on the probability term 1 -2 h∈H δ(h). If H is not too large, an oracle inequality for the risk of ∆ĥ f can be easily deduced from the later result. Henceforth we assume that f ∈ F. We first give a control on the approximation term D(h).

Proposition 3.2. Assume that the density p is C 2 . It holds that

D(h) ≤ γ C F h
where C F is defined in eq. (5) and γ > 0 is a constant depending on M , p ∞ , p ∞ and p ∞ , where p (k) ∞ denotes the supremum of the absolute value of the partial derivatives of p in any normal coordinates system.

We consider the following grid of bandwidths:

H = e -k , log log(n) ≤ k ≤ log(n) .
Note that this choice ensures that Condition (10) is always satisfied for n large enough. The previous results lead to the pointwise rate of convergence of the graph Laplacian selected by Lepski's method: Theorem 3.3. Assume that the density p is C 2 . For any f ∈ F, we have

E (p∆ P -∆ĥ )f 2,M n -1 d+4 . ( 12
)
4 Sketch of the proof of Theorem 3.1

We observe that the following inequality holds

(p∆ P -∆ĥ )f 2,M ≤ D(h) + (E[ ∆h ] -∆h )f 2,M + 2 (B(h) + bV (h)). (13)
Indeed, for h ∈ H,

(p∆ P -∆ĥ )f 2,M ≤ (p∆ P -E[ ∆h ])f 2,M + (E[ ∆h ] -∆h )f 2,M + ( ∆h -∆ĥ )f 2,M ≤ D(h) + (E[ ∆h ] -∆h )f 2,M + ( ∆h -∆ĥ )f 2,M .

By definition of B(h), for any

h ≤ h, ( ∆h -∆h )f 2 2,M ≤ B(h) + aV (h ) ≤ B(max{h, h }) + aV (min{h, h }),
so that, according to the definition of ĥ in eq. ( 3) and recalling that a ≤ b,

( ∆ĥ -∆h )f 2 2,M ≤ 2 [B(h) + aV (h)] ≤ 2 [B(h) + bV (h)
] which proves eq. ( 13).

We are now going to bound the terms that appear in eq. ( 13). The bound for D(h) is already given in Proposition 3.2, so that in the following we focus on B(h) and (E[ ∆h ] -∆h )f 2,M . More precisely the bounds we present in the next two propositions are based on the following lemma from [START_REF] Lacour | Minimal penalty for goldenshluger-lepski method[END_REF].

Lemma 4.1. Let X 1 , . . . , X n be an i.i.d. sequence of variables. Let S a countable set of functions and let η

(s) = 1 n i [g s (X i ) -E[g s (X i )]]
for any s ∈ S. Assume that there exist constants θ and v g such that for any s ∈ S

g s ∞ ≤ θ and Var[g s (X)] ≤ v g . Denote H = E[sup s∈ S η(s)]. Then for any > 0 and any H ≥ H P sup s∈ S η(s) ≥ (1 + )H ≤ max exp - 2 nH 2 6v g , exp - min{ 2 , }nH 24 θ . Proposition 4.2. Let = √ a 2 -1. Given h ∈ H, define δ 1 (h) = h ≤h max exp - min{ 2 , } √ n 24 , exp - 2 3 γ d (h ) . With probability at least 1 -δ 1 (h) B(h) ≤ 2D(h) 2 . Proposition 4.3. Let ˜ = √ a -1. Given h ∈ H, define δ 2 (h) = max exp - min{˜ 2 , ˜ } √ n 24 , exp - ˜ 2 3 γ d (h) . With probability at least 1 -δ 2 (h) (E[ ∆h ] -∆h )f 2,M ≤ aV (h).
Combining the above propositions with eq. ( 13), we get that, for any h ∈ H, with probability at least

1 -(δ 1 (h) + δ 2 (h)), (p∆ P -∆ĥ )f 2,M ≤ D(h) + aV (h) + 4D(h) 2 + 2bV (h) ≤ 3D(h) + (1 + √ 2) bV (h)
where we have used the fact that a ≤ b. Taking a union bound on h ∈ H we conclude the proof.

Numerical illustration

In this section we illustrate the results of the previous section on a simple example. In section 5.1, we describe a practical procedure when the data set X is sampled according to the uniform measure on M . A numerical illustration us given in Section 5.2 when M is the unit 2-dimensional sphere in R 3 .

Practical application of the Lepksi's method

Lepski's method presented in Section 2 can not be directly applied in practice for two reasons. First, we can not compute the L 2 -norm 2,M on M , the manifold M being unknown. Second, the variance terms involved in Lepski's method are not completely explicit.

Regarding the first issue, we can approximate 2,M by splitting the data into two samples: an estimation sample X 1 for computing the estimators and a validation sample X 2 for evaluating this norm. More precisely, given two estimators ∆h f and ∆h f computed using X 1 , the quantity ( ∆h -∆h )f 2 2,M /µ(M ) is approximated by the averaged sum

1 n2 x∈X2 | ∆h f (x) -∆h f (x)| 2
, where n 2 is the number of points in X 2 . We use these approximations to evaluate the bias terms B(h) defined by (4).

The second issue comes from the fact that the variance terms involved in Lepski's method depend on the metric properties of the manifold and on the sampling density, which are both unknown. Theses variance terms are thus only known up to a multiplicative constant. This situation contrasts with more standard frameworks for which a tight and explicit control on the variance terms can be proposed, as in [START_REF] Ov Lepskii | Asymptotically minimax adaptive estimation. i: Upper bounds. optimally adaptive estimates[END_REF][START_REF] Ov Lepskii | Asymptotically minimax adaptive estimation. ii. schemes without optimal adaptation: Adaptive estimators[END_REF][START_REF] Oleg | On problems of adaptive estimation in white gaussian noise[END_REF]. To address this second issue, we follow the calibration strategy recently proposed in [START_REF] Lacour | Minimal penalty for goldenshluger-lepski method[END_REF] (see also [START_REF] Lacour | Estimator selection: a new method with applications to kernel density estimation[END_REF]). In practice we remove all the multiplicative constants from V (h): all these constants are passed into the terms a and b. This means that we rewrite Lepski's method as follows: ĥ

(a, b) = arg min h∈H B(h) + b 1 nh 4 where B(h) = max h ≤h, h ∈H ( ∆h -∆h )f 2 2,M -a 1 nh 4 + .
We choose a and b according to the following heuristic:

1. Take b = a and consider the sequence of selected models: ĥ(a, a), 2. Starting from large values of a, make a decrease and find the location a 0 of the main bandwidth jump in the step function a → ĥ(a, a),

3. Select the model ĥ(a 0 , 2a 0 ).

The justification of this calibration method is currently the subject of mathematical studies ( [START_REF] Lacour | Minimal penalty for goldenshluger-lepski method[END_REF]). Note that a similar strategy called "slope heuristic" has been proposed for calibrating 0 penalties in various settings by strong mathematical results, see for instance [BM07, AM09, BMM12].

Illustration on the sphere

In this section we illustrate the complete method on a simple example with data points generated uniformly on the sphere S 2 in R 3 . In this case, the weighted Laplace-Beltrami operator is equal to the (non weighted) Laplace-Beltrami operator on the sphere.

We consider the function f (x, y, z) = (x 2 + y 2 + z) sin x cos x. The restriction of this function on the sphere has the following representation in spherical coordinates:

f (θ, φ) = (sin 2 φ + cos φ) sin(sin φ cos θ) cos(sin φ cos θ).
It is well known that the Laplace-Beltrami operator on the sphere satisfies (see Section 3 in [START_REF] Grigoryan | Heat kernel and analysis on manifolds[END_REF]):

∆ S 2 u = 1 sin 2 φ ∂ 2 u ∂θ 2 + 1 sin φ ∂ ∂φ sin φ ∂u ∂φ
for any smooth polar function u. This allows us to derive an analytic expression of ∆ S 2 f .

We sample n 1 = 10 6 points on the sphere for computing the graph Laplacians and we use n = 10 3 points for approximating the norms ( ∆h -∆h ) f 2 2,M . We compute the graph Laplacians for bandwidths in a grid H between 0.001 and 0.8 (see fig. 1). The risk of each graph Laplacian is estimated by a standard Monte Carlo procedure (see fig. 2).

Figure 1: Choosing h is crucial for estimating ∆ S 2 f : small bandwidth overfits ∆ S 2 f whereas large bandwidth leads to almost constant approximation functions of ∆ S 2 f . Figure 3 illustrates the calibration method. On this picture, the x-axis corresponds to the values of a and the y-axis represents the bandwidths. The blue step function represents the function a → ĥ(a, a). The red step function gives the model selected by the rule a → ĥ(a, 2a). Following the heuristics given in Section 5.1, one could take for this example the value a 0 ≈ 3.5 (location of the bandwidth jump for the blue curve) which leads to select the model ĥ(a 0 , 2a 0 ) ≈ 0.2 (red curve).

Discussion

This paper is a first attempt for a complete and well-founded data driven method for inferring Laplace-Beltrami operators from data points. Our results suggest various extensions and raised some questions of interest. For instance, other versions of the graph Laplacian have been studied in the literature (see for instance [START_REF] Hein | Graph laplacians and their convergence on random neighborhood graphs[END_REF][START_REF] Belkin | Towards a theoretical foundation for laplacian-based manifold methods[END_REF]), for instance when data is not sampled uniformly. It would be relevant to propose a bandwidth selection method for these alternative estimators also.

From a practical point of view, as explained in section 5, there is a gap between the theory we obtain in the paper and what can be done in practice. To fill this gap, a first objective is to prove an oracle inequality in the spirit of Theorem 3.1 for a bias term defined in terms of the empirical norms Tuning bandwidths for the estimation of the spectrum of the Laplace-Beltrami operator is a difficult but important problem in data analysis. We are currently working on the adaptation of our results to the case of operator norms and spectrum estimation.

Appendix: the geometric constants C and C 1

The following classical lemma (see, e.g. [START_REF] Giné | Empirical graph laplacian approximation of laplace-beltrami operators: Large sample results[END_REF][Prop. 2.2 and Eq. 3.20]) relates the constants C and C 1 introduced in Equations ( 6) and (7) to the geometric structure of M . Lemma 6.1. There exist constants C, C 1 > 0 and a positive real number r > 0 such that for any x ∈ M , and any v ∈ T x M such that v ≤ r,

det(g ij )(v) -1 ≤ C 1 v 2 d and 1 2 v 2 d ≤ v 2 d -C v 4 d ≤ E x (v) -x 2 m ≤ v 2 d ( 14
) where E x : T x M → M is the exponential map and (g i,j ) i,j ∈ {1, • • • , d} are the components of the metric tensor in any normal coordinate system around x.

Although the proof of the lemma is beyond the scope of this paper, notice that one can indeed give explicit bounds on r and C in terms of the reach and injectivity radius of the submanifold M .

Appendix: Proofs

For the sake of simplicity, we introduce the renormalized kernel

H h (y) = 1 h d+2 K (y/h) = 1 h d+2 (4π) d/2 e -y 2 m /4h 2 , y ∈ R m ,
so that ∆h rewrites as

∆h f (y) = 1 n n i=1 H h (y -X i ) [f (X i ) -f (y)]
where we recall that X 1 , . . . , X n is a finite point cloud (i.i.d.) sampled on M . Note that the expectation ∆ h of ∆h satisfies

∆ h f (y) = E ∆h f (y) = H h (y -x) [f (x) -f (y)] dP(x).
We present a technical result that is useful in the following and whose proof is postpone to section 6.5.

Lemma 6.2. Let x ∈ M and h ∈ H. According to the notation introduced in section 2.2 and in section 3

M |H h (y -x)(f (x) -f (y))| dµ(y) ≤ C F h w d K d 1,d + β d (h) =: I 1 (h) (15)
Moreover M |H h (y -x)(f (x) -f (y))| 2 dµ(y) ≤ 2C 2 F h d+2 w d K d 2 2,d + α d (h) =: I 2 (h). (16)
We also observe the following facts.

Remark 6.3. Given t ∈ R and s, q > 0,

t q e -t 2 /s 2 ≤ λe -t 2 /2s 2 where λ = s q q q/2 e -q/2 . Remark 6.4. Given a, b > 0, e -(a-b) -e -a ≤ be -a/2 so that, under the assumptions of Lemma 6.1, given s > 0,

e -Ex(v)-x 2 m /s 2 -e -v 2 d /s 2 ≤ e -( v 2 d -C v 4 d )/s 2 -e -v 2 d /s 2 ≤ C v 4 d s 2 e -v 2 d /2s 2 .

Proof of Proposition 2.1

In order to get the bound

V (h) for E[ (E[ ∆h ] -∆h )f 2 2,M ]
we observe that, according to the definition of ∆h and using the fact that the sample is i.i.d.,

E[ (E[ ∆h ] -∆h )f 2 2,M ] ≤ 1 n E |H h (y -X)(f (X) -f (y)| 2 dµ(y) ≤ 1 n I 2 (h)
where the last line follows from Lemma 6.2.

Proof of Theorem 3.1

According to the sketch of the proof provided in section 4, we only need to prove Proposition 4.2 and Proposition 4.3.

Proof of Proposition 4.2

Recalling the definition of B(h), since, for any h ≤ h,

( ∆h -∆h )f 2 2,M ≤ 2 ( ∆h -∆ h + ∆ h -∆h )f 2 2,M + (∆ h -∆ h )f 2 2,M ≤ 2 ( ∆h -∆ h + ∆ h -∆h )f 2 2,M + D(h) 2
we get

B(h) ≤ max h ≤h 2 ( ∆h -∆ h + ∆ h -∆h )f 2 2,M + 2D(h) 2 -aV (h ) + .
Thus it is sufficient to prove that

2 ( ∆h -∆ h + ∆ h -∆h )f 2 2,M ≤ aV (h ).
We can write

( ∆h -∆ h + ∆ h -∆h )f 2,M = sup t∈B 2,M (1)
η(f, t)

where B 2,M (1) = t ∈ L 2 (M ) | t 2,M = 1 , η(f, t) = t, ( ∆h -∆ h + ∆ h -∆h )f = 1 n n i=1 g t,f (X i ) -E[g t,f (X)]
and

g t,f (x) = t(y) [H h (y -x) -H h (y -x)] (f (x) -f (y)) dµ(y).
Since the function t → η(f, t) is continuous on B 2,M (1), we consider t ∈ T where T is a countable set of B 2,M (1). In order to apply Lemma 4.1 we need to compute the quantities θ, v g and H.

Lemma 6.5. Let t ∈ T . With the same notation as in Lemma 6.2

g t,f ∞ ≤ 2 I 2 (h ) 1/2 =: θ Var[g t,f (X)] ≤ 4 p ∞ I 1 (h ) 2 =: v g E sup t∈T η(f, t) ≤ 2 √ n I 2 (h ) 1/2 =: H.
Proof. Using the Cauchy-Schwarz inequality and the fact that t ∈ B 2,M we get

|g t,f (x)| ≤ t 2,M (H h (y -x) -H h (y -x)) (f (x) -f (y)) 2 dµ(y) 1/2 ≤ 2 H h (y -x)(f (x) -f (y)) 2 dµ(y) + 2 H h (y -x)(f (x) -f (y)) 2 dµ(y) 1/2 .
According to Lemma 6.2 and recalling that h ≤ h we get

|g t,f (x)| ≤ 2I 2 (h ) + 2I 2 (h) 1/2 ≤ 2 I 2 (h ) 1/2
which proves the first bound. To prove the second inequality we observe that, by the Cauchy-Schwarz inequality,

Var[g t,f (X)] ≤ E g t,f (X) 2 = E t(y) [(H h -H h )(y -X)] (f (X) -f (y)) dµ(y) 2 ≤ E t(y) 2 ((H h -H h )(y -X)) (f (X) -f (y)) dµ(y) × × ((H h -H h )(y -X)) (f (X) -f (y)) dµ(y) .
According to Lemma 6.2

((H h -H h )(y -X)) (f (X) -f (y)) dµ(y) ≤ I 1 (h ) + I 1 (h) ≤ 2 I 1 (h )
so that, recalling that the distribution P has a density p with respect to µ,

Var[g t,f (X)] ≤ 2 I 1 (h ) E t(y) 2 ((H h -H h )(y -X)) (f (X) -f (y)) dµ(y) ≤ 2 I 1 (h ) t(y) 2 ((H h -H h )(y -X)) (f (X) -f (y)) p(x) dµ(x)dµ(y) ≤ 2 p ∞ I 1 (h ) t(y) 2 |(H h -H h )(y -X)(f (X) -f (y))| dµ(x) dµ(y).
Using again Lemma 6.2 and the fact that t ∈ B 2,M we conclude that

Var[g t,f (X)] ≤ 4 p ∞ I 1 (h ) 2 .
To get the last inequality we follow the proof of Proposition 2.1. We observe that

E sup t∈T η(f, t) 2 = E ( ∆h -∆h )f -E ( ∆h -∆h )f 2 2,M ≤ 1 n E |(H h -H h )(y -X)(f (X) -f (y))| 2 dµ(y) .
According to Lemma 6.2,

E sup t∈T η(f, t) 2 ≤ 2 n (I 2 (h ) + I 2 (h)) ≤ 4 n I 2 (h )
which concludes the proof.

According to Lemma 4.1, with probability at least 1 max exp -

2 nH 2 6vg , exp -min{ 2 , }nH 24θ , ( ∆h -∆ h + ∆ h -∆h )f 2,M ≤ (1 + )H where H θ = 1 √ n and H 2 v g = I 2 (h ) nI 1 (h ) = 2 n p ∞ h d ω d K d 2 2,d + α d (h ) (ω d K d 1,d + β d (h )) 2 = 2γ d (h ) n .
Moreover, by definition, H 2 ≤ 4V (h ), so that choosing such that a ≥ 4(1 + ) 2 we get that with

probability at least 1 -max exp -min{ 2 , } √ n 24 , exp - 2 3 γ d (h ) 2 ( ∆h -∆ h + ∆ h -∆h )f 2 2,M ≤ 4(1 + ) 2 V (h ) ≤ aV (h ).
In particular we choose = √ a/2 -1. The result follows taking a union bound on h .

Proof of Proposition 4.3

The proof follows the one of Proposition 4.2. We can write

(∆ h -∆h )f 2,M = sup t∈B 2,M (1) η(f, t)
where

η(f, t) = 1 n n i=1 gt,f (X i ) -E[g t,f (X i )]
and gt,f (x) = t(y)H h (y -x)(f (x) -f (y)) dµ(y).

Moreover we observe that we can consider t ∈ T where T ⊂ B 2,M (1) is a countable set. Lemma 6.6. Let t ∈ T . With the notation of Lemma 6.2

gt,f ∞ ≤ I 2 (h) 1/2 =: θ Var[g t,f (X)] ≤ p ∞ I 1 (h) 2 =: ṽg E sup t∈T η(f, t) ≤ 1 √ n I 2 (h) 1/2 =: H.
Proof. We proceed as in the proof of Lemma 6.5. By the Cauchy-Schwarz inequality and Lemma 6.2, recalling that t ∈ B 2,M , we get

|g t,f (x)| ≤ t 2,M |H h (y -x)(f (x) -f (y))| 2 dµ(y) 1/2 ≤ I 2 (h) 1/2
which proves the first inequality. To get the second one, we observe that

Var[g t,f (X)] ≤ E gt,f (X) 2 ≤ E t(y) 2 H h (y -X)(f (X) -f (y)) dµ(y) × H h (y -X)(f (X) -f (y)) dµ(y) ≤ p ∞ I 1 (h) 2 .
To prove the last inequality we observe that

E sup t∈T η(f, t) 2 = E ∆h f -E ∆h f 2 2,M ≤ 1 n E |H h (y -X)(f (X) -f (y))| 2 dµ(y) ≤ 1 n I 2 (h). According to Lemma 4.1, with probability at least 1 - max exp -˜ 2 n H2 6ṽg , exp -min{˜ 2 ,˜ }n H 24 θ
, we have

(∆ h -∆h )f 2,M ≤ (1 + ˜ ) H
where

H/ θ = 1/ √ n and H2 /ṽ g = I 2 (h) n p ∞ I 1 (h) = 2 n p ∞ h d 2ω d K d 2 2,d + α d (h) (2ω d K d 1,d + β d (h)) 2 = 2γ d (h) n .
Moreover, since H2 = V (h), choosing such that a ≥ (1 + ˜ ) 2 we get that with probability at least

1 -max exp -min{˜ 2 ,˜ } √ n 24 , exp -˜ 2 3 γ d (h) (∆ h -∆h )f 2 2,M ≤ aV (h).
In particular choosing ˜ = √ a -1 we conclude the proof.

Proof of Proposition 3.2

We first prove that, given

x ∈ M , |p(x)∆ P f (x) -∆ h f (x)| ≤ Φ F (h ) (17) where Φ F (h ) = h C F 5τ d p ∞ 3 + p ∞ + p ∞ + p ∞ D3 + 2 (4π) d/2 + h 2 C F 35 4 p ∞ τ d + p ∞ + D4 p ∞ 2 + 1 2 h 3 C F D5 p ∞ 3 + p ∞ + p ∞ + 1 4 h 4 C F p ∞ D6 + κ d C F ( p ∞ + p ∞ /2) (4π) d/2 (4(d + 3)) d/2 log(h -1 ) d/2 h d+3 + κ d-1 C F p ∞ (4π) d/2 (4(d + 3)) (d-1)/2 log(h -1 ) (d-1)/2 h d+2 with τ d = 1 (4π) d/2 R d e -u 2 d /8 du κ d+σ = 2 Γ (d + σ + 1)/2 F d+σ ( 2(d + σ)), σ ∈ Z, and
F d+σ (x) = ∞ x t d+σ+1 e -t 2 /4 dt x d+σ e -x 2 /4 . ( 18
) Introduce B = y ∈ M | y -x m < Lh log(h -1 ) 1/2
with L > 0 to be chosen and observe that

∆ h f (x) = 1 h d+2 (4π) d/2 B + B c e -y-x 2 m /4h 2 (f (y) -f (x)) dP(y) =: I B f (x) + I B c f (x).
We first recall that the distribution P has a density p with respect to µ. Moreover on B, in the x-normal coordinates, µ has a density det(g ij ) and the Taylor expansion of f is

f (E x (v)) -f (x) = f (E x (v)) -f (E x (0)) = f (x), v + 1 2 f (x)v, v + 1 6 f (ξ)(v, v, v)
for a suitable ξ = ξ(x) ∈ M and where f (k) denotes the k-th derivate with respect to v of f • E x (v).

Thus we can write

I B f (x) = 1 h d+2 (4π) d/2 B e -y-x 2 m /4h 2 (f (y) -f (x)) dP(y) = 1 h d+2 (4π) d/2 E -1 x (B) e -Ex(v)-x 2 m /4h 2 f (x), v + 1 2 f (x)v, v p(E x (v)) det(g ij )(v) dv + 1 6h d+2 (4π) d/2 E -1 x (B) e -Ex(v)-x 2 m /4h 2 f (ξ)(v, v, v) p(E x (v)) det(g ij )(v) dv.
Using now the Taylor expansion of p in x-normal coordinates

p(E x (v)) = p(x) + p (x), v + 1 2 p (ζ)v, v
for a suitable ζ = ζ(x) ∈ M and where as before p (k) denotes k-th derivate of p • E x , we have that

|∆ h f (x) -p(x)∆ P f (x)| ≤ I 1 f (x) + I 2 f (x) + I 3 f (x) + I 4 f (x) + I 5 f (x) + I 6 f (x) + I B c f (x)
where, denoting by

S(u) = f (x), u p (x), u + p(x) 2 f (x)u, u , (19)
I 1 f (x) = 1 h d+2 (4π) d/2 E -1 x (B) e -Ex(v)-x 2 m /4h 2 S(v) det(g ij )(v) dv -p(x)∆ P f (x) I 2 f (x) = 1 h d+2 (4π) d/2 E -1 x (B) e -Ex(v)-x 2 m /4h 2 p(x) f (x), v det(g ij )(v) dv I 3 f (x) = 1 2h d+2 (4π) d/2 E -1 x (B) e -Ex(v)-x 2 m /4h 2 f (x), v p (ζ)v, v det(g ij )(v) dv I 4 f (x) = 1 2h d+2 (4π) d/2 E -1 x (B) e -Ex(v)-x 2 m /4h 2 f (x)v, v p (x), v det(g ij )(v) dv I 5 f (x) = 1 4h d+2 (4π) d/2 E -1 x (B) e -Ex(v)-x 2 m /4h 2 f (x)v, v p (ζ)v, v det(g ij )(v) dv I 6 f (x) = 1 6h d+2 (4π) d/2 E -1 x (B) e -Ex(v)-x 2 m /4h 2 f (ξ)(v, v, v) p(E x (v)) det(g ij )(v) dv .
Let us now bound each term separately. We first observe that by definition

I B c f (x) ≤ 2C F h d+2-L 2 /4 (4π) d/2 .
For the proofs of Lemma 6.7 and Lemma 6.8 we refer to section 6.6. Lemma 6.7. It holds

I 1 f (x) ≤ C F ( p ∞ + p ∞ /2) κ d (4π) d/2 L d log(h -1 ) d/2 h L 2 /4 + D4 h 2 .
Lemma 6.8. It holds

I 2 f (x) ≤ C F p ∞ κ d-1 (4π) d/2 L d-1 log(h -1 ) (d-1)/2 h L 2 /4-1 + D3 h I 3 f (x) ≤ C F p ∞ h 5τ d + D5 2 h 2 I 4 f (x) ≤ C F p ∞ h 5τ d + D5 2 h 2 I 5 f (x) ≤ C F p ∞ h 2 35 4 τ d + D6 4 h 2 I 6 f (x) ≤ C F p ∞ h 5τ d 3 + D5 6 h 2 .
We choose L = 2 √ d + 3 and we note that Condition 10 is then satisfied. This concludes the proof.

Proof of Theorem 3.3

We first prove the following lemma: Lemma 6.9. Assume that the density p of P is in C 1 (M, R + ). For f ∈ F, we have

E (p∆ P -∆ĥ )f 2 2,M ≤ 2 inf h∈H 9D(h) 2 + (1 + √ 2) 2 bV (h) + 2 C 2 F h∈H δ(h) 1 h d+2 min w d K d 2 2,d + α d (h max ) + 9 p ∞ + p ∞ /2 2 µ(M )τ 2 d , (20)
where we recall that

τ d = 1 (4π) d/2 R d e -u 2 d /8 du.
Proof. Let A be the set on which the oracle inequality in Theorem 3.1 holds true. Then

E (p∆ P -∆ĥ )f 2 2,M ≤ E (p∆ P -∆ĥ )f 2 2,M 1 A + 2E p∆ P f 2 2,M + ∆ĥ f 2 2,M 1 A c . ( 21
)
Observe that to bound the first term, it is sufficient to use Theorem 3.1. Thus we only have to consider the second term. According to eq. ( 2), we can rewrite the weighted Laplace-Beltrami operator in x-normal coordinates as

∆ P f (x) = 1 (4π) d/2 e -u 2 d /4 p (x), u p(x) f (x), u + 1 2 f (x)u, u du, so that p∆ P f 2 2,M = 1 (4π) d e -u 2 d /4 p (x), u f (x), u + p(x) 2 f (x)u, u du 2 dµ(x) ≤ C 2 F ( p ∞ + p ∞ /2) 2 µ(M ) (4π) d e -u 2 d /4 u 2 d du 2 ≤ 9C 2 F ( p ∞ + p ∞ /2) 2 µ(M )τ 2 d
where in the last line we have used remark 6.3 with s = 2, q = 2 so that λ ≤ 3. Moreover for any h ∈ H by Lemma 6.2

∆h f 2 2,M ≤ 1 n 2 n i=1 H h (• -X i ) (f (X i ) -f (•)) 2,M 2 ≤ I 2 (h) ≤ 2C 2 F h d+2 min w d K d 2 2,d + α d (h max ) .
Hence

E p∆ P f 2 2,M + ∆ĥ f 2 2,M 1 A c ≤ C 2 F 1 h d+2 min w d K d 2 2,d + α d (h max ) + 9 p ∞ + p ∞ /2 2 µ(M )τ 2 d h∈H δ(h).
We now prove Theorem 3.3. Note that

γ d (h ) ≥ C d h d with C d = 1 p ∞ ω d K d 2 2,d +α d (hmin) (ω d K d 1,d +β d (hmax)) 2 . Thus, h∈H δ(h) ≤ h∈H h ≤h max exp - min{ 2 , } √ n 24 , exp - C d c 2 h d ≤ |H| 2 exp - min{ 2 , } C d h d max
where C d > 0 is a constant and |H| denotes the cardinality of the bandwidth set H. For

H = e -k , log log(n) ≤ k ≤ log(n) ,
we get that the second term in eq. ( 20) is negligible with respect to the first one. Finally, observe that combining Proposition 3.2 with the definition of the variance term V (h), the optimal trade-off in Lemma 6.9 is given by h ∼ n -1 d+4 , which concludes the proof.

6.5 Proof of Lemma 6.2

In order to prove eq. ( 15), we consider

B = B x (h) = {y ∈ M | y -x m < Lh log(h -1 ) 1/2 } ⊂ M
where L > 0 has to be chosen and we observe that

1 h d+2 (4π) d/2 B∪B c e -y-x 2 m /4h 2 |f (x) -f (y)| dµ(y).
We first look at the integral on B and we consider the x-normal coordinates. Taking into account that the measure µ has a density detg ij in the x-normal coordinates, we get

1 h d+2 (4π) d/2 B e -y-x 2 m /4h 2 |f (x) -f (y)| dµ(y) = 1 h d+2 (4π) d/2 E -1 x (B) e -Ex(v)-x 2 m /4h 2 |f (x) -f (E x (v))| detg ij (v) dv ≤ 1 h d+2 (4π) d/2 E -1 x (B) e -Ex(v)-x 2 m /4h 2 |f (x) -f (E x (v))| (1 + C 1 v 2 d ) dv
where in the last line we have used eq. ( 14). Using the Taylor expansion of f in x-normal coordinates

f (E x (v)) -f (x) = f (E x (v)) -f (E x (0)) = f (x), v + 1 2 f (ξ)v, v (22)
where ξ = ξ(x) ∈ M and f ( k) denotes the k-th derivate with respect to v of f • E x (v) the above chain of inequalities is bounded by

1 h d+2 (4π) d/2 E -1 x (B) e -Ex(v)-x 2 m /4h 2 | f (x), v | (1 + C 1 v 2 d ) dv + 1 2 E -1 x (B) e -Ex(v)-x 2 m /4h 2 | f (ξ)v, v | (1 + C 1 v 2 d ) dv ≤ C F h d+2 (4π) d/2 E -1 x (B) e -Ex(v)-x 2 m /4h 2 v d (1 + C 1 v 2 d ) dv + 1 2 E -1 x (B) e -Ex(v)-x 2 m /4h 2 v 2 d (1 + C 1 v 2 d ) dv
where in the last line we have used the fact f ∈ F is uniformly bounded up to the third order. We now consider the two terms separately. We write

1 h d+2 (4π) d/2 E -1 x (B) e -Ex(v)-x 2 m /4h 2 v d (1 + C 1 v 2 d ) dv = 1 h d+2 (4π) d/2 E -1 x (B) e -v 2 d /4h 2 v d dv + R 1
where, according to remark 6.4,

R 1 = 1 (4π) d/2 h d+2 E -1 x (B) e -Ex(v)-x 2 m /4h 2 -e -v 2 d /4h 2 v d dv + C 1 (4π) d/2 h d+2 E -1 x (B) e -Ex(v)-x 2 m /4h 2 v 3 d dv ≤ 1 (4π) d/2 h d+2 R d C v 5 d 4h 2 + C 1 v 3 d e -v 2 d /8h 2 dv = h D3
and by remark 6.3

1 (4π) d/2 h d+2 E -1 x (B) e -v 2 d /4h 2 v d dv ≤ 3 2(4π) d/2 h d+1 R d e -v 2 d /8h 2 dv = 3 × 2 d/2 2(4π) d/2 h R d e -u 2 d /4 dv = 3 × 2 d/2-1 K d 1,d h .
Similarly, the second term can be written as

1 h d+2 (4π) d/2 E -1 x (B) e -Ex(v)-x 2 m /4h 2 v 2 d (1 + C 1 v 2 d ) dv = 1 h d+2 (4π) d/2 E -1 x (B) e -v 2 d /4h 2 v 2 d dv + R 2
where, according to remark 6.4,

R 2 = 1 (4π) d/2 h d+2 E -1 x (B) e -Ex(v)-x 2 m /4h 2 -e -v 2 d /4h 2 v 2 d dv + C 1 (4π) d/2 h d+2 E -1 x (B) e -Ex(v)-x 2 m /4h 2 v 4 d dv ≤ h 2 D4
and by remark 6.3

1 (4π) d/2 h d+2 E -1 x (B) e -v 2 d /4h 2 v 2 d dv ≤ 3 × 2 d/2 K d 1,d .
This proves that, on B,

1 h d+2 (4π) d/2 B e -y-x 2 m /4h 2 |f (x) -f (y)| dµ(y) ≤ C F ω d K d 1,d h + ω d K d 1,d + h D3 + h 2 D4 2
where we recall the definition of ω d = 3 × 2 d/2-1 in eq. ( 8). We now consider the integral on B c . According to the definition of B

1 h d+2 (4π) d/2 B e -y-x 2 m /4h 2 |f (x) -f (y)| dµ(y) ≤ 2C F µ(M ) (4π) d/2 h d+2-L 2 /4 . Choosing L = 2 √ d + 2 so that d + 2 -L 2 /4 = 0 we prove eq. ( 15
). In a similar way we prove eq. ( 16). We consider again the ball B defined as above and we write

1 h 2d+4 (4π) d B∪B c e -y-x 2 m /2h 2 |f (x) -f (y)| 2 dµ(y).
Proceeding as above, on B we consider the x-normal coordinates and according to eq. ( 14) we get

1 h 2d+4 (4π) d B e -y-x 2 m /2h 2 |f (x) -f (y)| 2 dµ(y) ≤ 1 h 2d+4 (4π) d E -1 x (B) e -Ex(v)-x 2 m /2h 2 |f (x) -f (E x (v))| 2 (1 + C 1 v 2 d ) dv.
Using the Taylor expansion of f in eq. ( 22) we bound the above quantity by

2 h 2d+4 (4π) d E -1 x (B) e -Ex(v)-x 2 m /2h 2 f (x), v 2 (1 + C 1 v 2 d ) dv + 1 4 E -1 x (B) e -Ex(v)-x 2 m /2h 2 f (ξ)v, v 2 (1 + C 1 v 2 d ) dv ≤ 2C 2 F h 2d+4 (4π) d E -1 x (B) e -Ex(v)-x 2 m /2h 2 v 2 (1 + C 1 v 2 d ) dv + 1 4 E -1 x (B) e -Ex(v)-x 2 m /2h 2 v 4 (1 + C 1 v 2 d ) dv
where in the last line we have used the fact that f ∈ F. We observe that the first term can be written as

1 h 2d+4 (4π) d E -1 x (B) e -Ex(v)-x 2 m /2h 2 v 2 (1 + C 1 v 2 d ) dv = 1 h 2d+4 (4π) d E -1 x (B) e -v 2 d /2h 2 v 2 dv + R 1
where, by remark 6.4,

R 1 = 1 (4π) d h 2d+4 E -1 x (B) e -Ex(v)-x 2 m /2h 2 -e -v 2 d /2h 2 v 2 d dv + C 1 (4π) d h 2d+4 E -1 x (B) e -Ex(v)-x 2 m /2h 2 v 4 d dv ≤ 1 (4π) d h 2d+4 E -1 x (B) C v 6 d 2h 2 + C 1 v 4 d e -v 2 d /4h 2 dv ≤ D 4 h d
and according to remark 6.3 with s 2 = 2h 2 and q = 2 so that λ

≤ 3h 2 2 , 1 (4π) d h 2d+4 E -1 x (B) e -v 2 d /2h 2 v 2 d dv ≤ 3 2(4π) d h 2d+2 R d e -v 2 d /4h 2 dv = 3 × 2 d/2 2(4π) d h d+2 R d e -u 2 d /2 du = 3 × 2 d/2-1 K d 2 2,d h d+2 .
Moreover the second term writes

1 h 2d+4 (4π) d E -1 x (B) e -Ex(v)-x 2 m /2h 2 v 4 (1 + C 1 v 2 d ) dv = 1 h 2d+4 (4π) d E -1 x (B) e -v 2 d /2h 2 v 4 dv + R 2
where, using again remark 6.4,

R 2 = 1 (4π) d h 2d+4 E -1 x (B) e -Ex(v)-x 2 m /2h 2 -e -v 2 d /2h 2 v 4 d dv + C 1 (4π) d h 2d+4 E -1 x (B) e -Ex(v)-x 2 m /2h 2 v 6 d dv ≤ 1 (4π) d h 2d+4 R d C v 8 d 2h 2 + C 1 v 6 d e -v 2 d /4h 2 dv = D 6 h d-2
and by remark 6.3 with λ ≤ 9h 4 ,

1 (4π) d h 2d+4 E -1 x (B) e -v 2 d /2h 2 v 4 d dv ≤ 9 × 2 d/2 K d 2 2,d h d .
Then on B we have

1 h 2d+4 (4π) d B e -y-x 2 m /2h 2 |f (x) -f (y)| 2 dµ(y) ≤ 2C 2 F ω d K d 2 2,d h d+2 + D 4 + 3ω d K d 2 2,d /2 h d + D 6 4h d-2 while on B c 1 h 2d+4 (4π) d B c e -y-x 2 m /2h 2 |f (x) -f (y)| 2 dµ(y) ≤ 4C 2 F µ(M ) (4π) d h 2d+4-L 2 /2 .
Thus choosing L = 2(d + 4) so that 2d + 4 -L 2 /2 = d we conclude the proof.

6.6 Proofs of the technical lemmas in section 6.3 6.6.1 Proof of Lemma 6.7

According to eq. ( 14),

I 1 f (x) ≤ 1 h d+2 (4π) d/2 E -1 x (B)
e -Ex(v)-x 2 m /4h 2 S(v) dv -p(x)∆ P f (x)

+ C 1 h d+2 (4π) d/2 E -1 x (B) e -Ex(v)-x 2 m /4h 2 S(v) v 2 d dv ≤ 1 h d+2 (4π) d/2 E -1 x (B)
R 1 ≤ C F ( p ∞ + p ∞ /2) h d+2 (4π) d/2 E -1 x (B) e -v 2 d /8h 2 v 2 d C v 4 d 4h 2 + C 1 v 2 d dv ≤ C F ( p ∞ + p ∞ /2) D4 h 2 .
Moreover according to eq. (2) we can rewrite the weighted Laplace-Beltrami operator in x-normal coordinates as

∆ P f (x) = 1 (4π) d/2
e -u 2 d /4

p (x), u p(x) f (x), u + 1 2 f (x)u, u du, so that p(x)∆ P f (x) = 1 (4π) d/2 e -u 2 d /4 S(u) du.

Hence, denoting

B := v ∈ R d | v d < Lh log(h -1 ) 1/2 ⊂ E -1 x (B).
we get

1 h d+2 (4π) d/2 E -1 x (B) e -v 2 d /4h 2 S(v) dv -p(x)∆ P f (x) = 1 h d+2 (4π) d/2 (E -1 x (B)) c e -v 2 d /4h 2 S(v) dv ≤ C F ( p ∞ + p ∞ /2) h d+2 (4π) d/2 Bc e -v 2 d /4h 2 v 2 d dv ≤ C F ( p ∞ + p ∞ /2) (4π) d/2 { u d >L log(h -1 ) 1/2 } e -u 2 d /4 u 2 d du ≤ κ d C F ( p ∞ + p ∞ /2) (4π) d/2 L d log(h -1 ) d/2 h L 2 /4
which concludes the proof.

6.6.2 Proof of Lemma 6.8

By eq. ( 14) Observe that, by remark 6.3 and eq. ( 14),

I 2 f (x) ≤ p ∞ h d+2 (4π) d/2 E -1 x (B) e -Ex(v)-x 2 m /4h 2 f (x), v 1 + C 1 v 2 d dv ≤ p ∞ h d+2 (4π) d/2 E -1 x (B)
R 2 ≤ C F p ∞ h d+2 (4π) d/2 E -1 x (B) e -Ex(v)-x 2 m /4h 2 -e -v 2 d /4h 2 v d dv + C 1 E -1 x (B) e -Ex(v)-x 2 m /4h 2 v 3 d dv ≤ C F p ∞ h d+2 (4π) d/2 E -1 x (B) v d e -v 2 d /8h 2 C v 4 d 4h 2 + C 1 v 2 d dv ≤ C F p ∞ D3 h
where in the last line we have used the definition of Dα introduced in eq. ( 7). Moreover, observe that

Then we get

p ∞ h d+2 (4π) d/2 E -1 x (B) e -v 2 d /4h 2 f (x), v dv = p ∞ h d+2 (4π) d/2 E -1 x (B) c e -v 2 d /4h 2 f (x), v dv ≤ p ∞ h d+2 (4π) d/2 Bc e -v 2 d /4h 2 f (x), v dv ≤ C F p ∞ h d+2 (4π) d/2 Bc e -v 2 d /4h 2 v d dv ≤ C F p ∞ h (4π) d/2 { u d >L log(h -1 ) 1/2 } e -u 2 d /4 u d dv ≤ κ d-1 C F p ∞ (4π) d/2 L d-1 log(h -1 ) (d-1)/2 h L 2 /4-1 .
Similarly we can bound I 3 f (x). By eq. ( 14) we have

I 3 f (x) ≤ C F p ∞ 2h d+2 (4π) d/2 E -1 x (B) e -Ex(v)-x 2 m /4h 2 v 3 d 1 + C 1 v 2 d dv = C F p ∞ 2h d+2 (4π) d/2 E -1 x (B) e -v 2 d /4h 2 v 3 d dv + R 3
where, according to remark 6.3,

R 3 = C F p ∞ 2h d+2 (4π) d/2 E -1 x (B) e -Ex(v)-x 2 m /4h 2 -e -v 2 d /4h 2 v 3 d dv + C 1 E -1 x (B) e -Ex(v)-x 2 m /4h 2 v 5 d dv ≤ 1 2 C F p ∞ D5 h 3
and by remark 6.3 with s = 2h and q = 3 so that λ ≤ 10h 3

C F p ∞ 2h d+2 (4π) d/2 E -1 x (B) e -v 2 d /4h 2 v 3 d dv ≤ 5C F p ∞ τ d h .
The bounds for I 4 f (x), I 5 f (x), I 6 f (x) are obtained in the same way.

Figure 2 :

 2 Figure 2: Estimation of the risk of each graph Laplacian operator: the oracle Laplacian is for approximatively h = 0.15.

Figure 3 :

 3 Figure 3: Bandwidth jump heuristic: find the location of the jump (blue curve) and deduce the selected bandwidth with the red curve.

e -v 2 d /4h 2 Swhere

 22 (v) dv -p(x)∆ P f (x) + R 1 d+2 (4π) d/2 E -1 x (B) e -Ex(v)-x 2 m /4h 2 v 2 d S(v) dv . Since |S(t)| ≤ C F ( p ∞ + p ∞ /2) t 2d by remark 6.3

e -v 2 d /4h 2 f

 22 (x), v dv + R 2 where R 2 = p ∞ h d+2 (4π) d/2

R d e -v 2 d /4h 2 f

 22 (x), v dv = 0 and defineB := v ∈ R d | v d < Lh log(h -1 ) 1/2 ⊂ E -1 x (B).

Acknowledgments

The authors are grateful to Pascal Massart for helpful discussions on Lepski's method and to Antonio Rieser forhis careful reading and for pointing a technical bug in a preliminary version of this work. This work was supported by the ANR project TopData ANR-13-BS01-0008 and ERC Gudhi No. 339025


Karim Nour
email: karim.nour@univ-smb.fr

Mohamad Ziadeh

A revised completeness result for the simply typed λµ-calculus using realizability semantics

Introduction

Since it was realised that the Curry-Howard isomorphism can be extended to the case of classical logic (cf. [START_REF] Murthy | An evaluation semantics for classical proofs[END_REF] and [START_REF] Griffin | A formulae-as-types notion of control[END_REF]), several calculi have appeared aiming to give an encoding of proofs formulated either in classical natural deduction or in classical sequent calculus. One of them was the λµ-calculus presented by Parigot in [START_REF] Parigot | Free Deduction: An Analysis of "Computations[END_REF], which stands very close in nature to the λ-calculus itself. It uses new kinds of variables, the µ-variables, not active at the moment, but to which the current continuation can be passed over. Eliminating cuts with these new formulas leads to the introduction of a new reduction rule : the so-called µ-rule. The result is a calculus, the λµ-calculus [START_REF] Parigot | λµ-calculus: An algorithm interpretation of classical natural deduction[END_REF], which is in relation with classical natural deduction. In addition, more simplification rules, for example the ρ-and θ-rules, are defined by Parigot [START_REF] Parigot | λµ-calculus: An algorithm interpretation of classical natural deduction[END_REF][START_REF] Parigot | Classical proofs as programs[END_REF]). Parigot showed that the λµ-calculus is strongly normalizing in [START_REF] Parigot | Proofs of strong normalization for second order classical natural deduction[END_REF], he gave a proof of the result with the help of the Tait-Girard reducibility method [START_REF] Girard | Proofs and types[END_REF][START_REF] Tait | A realizability interpretation of the theory of species[END_REF]. An arithmetical proof of the same result was presented by David and Nour in [2].

The idea of the realizability semantics is to associate to each type a set of terms which realize this type. Under this semantics, an atomic type is interpreted as a set of λ-terms saturated by a certain relation. Then, an arrow type receives the intuitive interpretation of a functional space. For example, a term which realizes the type N → N is a function from N to N. Realizability semantics has been a powerful method for establishing the strong normalization of type systems à la Tait and Girard [START_REF] Tait | A realizability interpretation of the theory of species[END_REF][START_REF] Girard | Proofs and types[END_REF]. The realizability of a type system enables one to also show the soundness of the system in the sense that the interpretation of a type contains all the terms that have this type. Soundness has been an important method for characterizing the computational behaviour of typed terms through their types as has been illuminative in the work of Krivine. It is also interesting to find the class of types for which the converse of soundness holds i.e., to find the types A for which the realizability interpretation contains exactly, in a certain sense, the terms typable by A. This property is called completeness and has not yet been studied for every type system.

Hindley [START_REF] Hindley | The completeness theorem for typing λ-terms[END_REF][START_REF] Hindley | Curry's type-rules are complete with respect to the F-semantics too[END_REF][START_REF] Hindley | Basic Simple Type Theory[END_REF] was the first to study the completeness of a simple type system and he showed that all the types of that system have the completeness property. Then, he generalised his completeness proof for an intersection type system [START_REF] Hindley | The simple semantics for Coppo-Dezani-Sallé types[END_REF]. [START_REF] Labib-Sami | Typer avec (ou sans) types auxiliaires[END_REF] has established completeness for a class of types in Girard-Reynolds's system F known as the strictly positive types. [START_REF] Farkh | Un résultat de complétude pour les types ∀ + du système F . CRAS[END_REF][START_REF] Farkh | Résultats de complètude pour des classes de types du système AF 2[END_REF] generalised the result of [START_REF] Labib-Sami | Typer avec (ou sans) types auxiliaires[END_REF] for the larger class which includes all the positive types and also for the second order functional arithmetic. [1] established by a different method using Kripke models the completeness for the simply typed λ-calculus. Finally [START_REF] Kamareddine | A completeness result for a realizability semantics for an intersection type system[END_REF] established the soundness and completeness for a strict non linear intersection type system with a universal type.

In [START_REF] Nour | A semantical proof of strong normalization theorem for full propositional classical natural deduction[END_REF], Nour and Saber adapted Parigot's method and established a short semantical proof of the strong normalization of classical natural deduction with disjunction as primitive. In general all the known semantical proofs of strong normalization use a variant of the reducibility candidates based on a correctness result, which has been important also for characterizing computational behavior of some typed terms, as it was done in J.-L. Krivine's works [START_REF] Krivine | Opérateurs de mise en mémoire et traduction de Gödel[END_REF]. This inspired K. Nour and K. Saber to define a general semantics for classical natural deduction in [START_REF] Nour | A Semantics of Realizability for the Classical Propositional Natural Deduction[END_REF] and gave such characterizations. In [START_REF] Nour | A completeness result for the simply typed lambda-mu calculus[END_REF], Nour and Saber proposed a realizability semantics for the simply typed λµ-calculus and proved a completeness theorem. This semantics is inspired by the strong normalization proof of Parigot's λµ-calculus, which consists in rewriting each reducibility candidate as a double orthogonal. In [START_REF] Van Bakel | A Filter Model for the λµ-Calculus[END_REF], van Bakel, Barbanera and de'Liguoro prove the completeness of the λµ-calculus with intersection types using filter models.

The semantics proposed in [START_REF] Nour | A completeness result for the simply typed lambda-mu calculus[END_REF] has several defaults. First of all, there is a mistake in the proof of the correctness lemma (the case of the typing rule (⊥) in the proof of Lemma 3.3) which is not correctable. This comes essentially from the permission to have µ-variables in the sequence of terms by adopting Saurin's interpretation. This mistake makes the semantics less interesting even though the proof of completeness remains correct. Besides, although the statement of Lemma 4.2 of [START_REF] Nour | A completeness result for the simply typed lambda-mu calculus[END_REF] is correct, the proposed proof is false. The correction of these mistakes, mainly the first, needs the introduction of another realizability semantics which is completely different from the one proposed in [START_REF] Nour | A completeness result for the simply typed lambda-mu calculus[END_REF].

In the present work we provide another realizability semantics for the simply typed λµ-calculus, by changing the concept of saturation. For this, we add an important and an indispensable modification to the notion of µ-saturation using more bottom sets. The saturation conditions give a very satisfactory correctness result. The completeness model gives also more intuition about the models that we consider.

This paper is organized as follows. Section 2 is an introduction to the simply typed λµ-calculus. We also define the semantics and prove its correctness. Section 3 is devoted to the completeness result.

2 The simply typed λµ-calculus

The syntax of the system

In this paper, we use the λµ-calculus à la de Groote which is more expressive than Parigot's original version. In [START_REF] Ph | An environment machine for the lambda-mu-calculus[END_REF], de Groote has proposed a new version of the λµ-calculus by modifying its syntax. Namely, in the construction of terms the distinction between named and unnamed terms has disappeared and the term forming rules has became more flexible: a µ-operator can be followed now by any kind of term (in the untyped version), not necessarily by a term beginning with a µ -variable.

Definition 2.1 (Terms and reductions)

1. Let V and A be two infinite sets of disjoint alphabets for distinguishing λvariables and µ-variables. The λµ-terms are given by the following grammar:

T := V | λV.T | (T T ) | µA.T | (A T )
2. The complexity of a term is defined by c

(x) = 0, c(λx.t) = c(µα.t) = c((α t)) = c(t) + 1 and c((u v)) = c(u) + c(v) + 1.
3. The basic reduction rules are ⊲ β and ⊲ µ .

• (λx.u v) ⊲ β u[x := v] • (µα.u v) ⊲ µ µα.u[α := * v]
where u[α := * v] is obtained from u by replacing inductively each subterm in the form (α w) in u by (α (w v)).

4. Let ⊲ stand for the compatible closure of the union of the rules given above, and, as usual, ⊲ * denotes the reflexive transitive closure of ⊲, and ≃ the equivalence relation induced by ⊲ * . We also denote by t ⊲ n t ′ that t ⊲ * t ′ and the length of this reduction (number of reduced redexes) is n. A term is said to be normal if it does not contain a redex. A term t is called strongly normalizable, if there is no infinite reduction sequence starting from t.

We find in the current literature of the λµ-calculus other simplification rules such as: ⊲ θ , ⊲ ρ , ⊲ ν , ⊲ η , ⊲ µ ′ , . . . These rules allow to get less normal forms (see [START_REF] Nour | La valeur d'un entier classique en lambda-mu-calcul[END_REF][START_REF] Parigot | λµ-calculus: An algorithm interpretation of classical natural deduction[END_REF][START_REF] Parigot | Proofs of strong normalization for second order classical natural deduction[END_REF][START_REF] Py | Confluence en λµ-calcul[END_REF]). In this paper, we do not need these rules for our completeness result.

Definition 2.2 (Types and typing rules)

1. Types are formulas of the propositional logic built from the infinite set of propositional variables P = {X, Y, Z, . . . } and a constant of type ⊥, using the connective →.

2. The complexity of a type is defined by c(⊥) = c(X) = 0 and c(A → B) = c(A) + c(B) + 1.

3. Let A 1 , A 2 , . . . , A n , A be types, we denote the type

A 1 → (• • • → (A n → A) . . . ) by A 1 , . . . , A n → A. Γ ⊢ t :⊥; ∆, α : A Γ ⊢ µα.t : A; ∆ µ Γ ⊢ t : A; ∆, α : A Γ ⊢ (α t) :⊥; ∆, α : A ⊥
We denote this typed system by S µ .

We have the following results (for more details, see [2,[START_REF] Parigot | Proofs of strong normalization for second order classical natural deduction[END_REF][START_REF] Py | Confluence en λµ-calcul[END_REF]). 4. The leftmost reduction (denoted by ⊲ l ) consits in reducing the redex nearest to the left of the term. We can also see it as an iteration of the head reduction: once we find the head normal form, we reduce the arguments of the head variable.

Lemma 2.1 The leftmost reduction of a normalizing term terminates.

Proof See [START_REF] Py | Confluence en λµ-calcul[END_REF].

The previous lemma allows one to define a notion of length for normalizing terms.

Definition 2.4 Let t be a normalizing term. We define l(t) as the number of leftmost reductions needed to find the normal form of t.

We need to define the concept of simultaneous substitution to be able to present the correctness lemma. Definition 2.5 Let t, u 1 , . . . , u n be terms, v1 , . . . , vm finite sequences of terms, and σ the simultaneous substitution [(x i := u i ) 1≤i≤n ; (α j := * vj ) 1≤j≤m ] which is not an object of the syntax. Then tσ is obtained from the term t by replacing each x i by u i and replacing inductively each subterm of the form (α j u) in t by (α j (u vj )).

Lemma 2.2 If t ⊲ * t ′ and σ a simultaneous substitution, then tσ ⊲ * t ′ σ. Proof It suffies to check the property for one step of reduction. Then we proceed by induction on c(t).

The semantics of the system

In this section, we define the realizability semantics and we prove its correctness lemma. We begin by the definition of the saturation of sets of terms and then the operation between these sets which will serve to interpret the arrow on types.

Definition 2.6

1. We say that a set of terms S is saturated if for all terms u and v, if v ⊲ * u and u ∈ S, then v ∈ S.

2. Consider two sets of terms K and L, we define a new set of terms

K L = {t ∈ T / ∀ u ∈ K ; (t u) ∈ L}.
3. We denote T <ω as the set of finite sequences of terms. Let L be a set of terms and X ⊆ T <ω , then we define a new set of terms

X L = {t ∈ T / ∀ ū ∈ X ; (t ū) ∈ L}.
Lemma 2.3 If L is a saturated set and X ⊆ T <ω , then X L is also a saturated one.

Proof

Let u and v be terms such that v ⊲ * u and u ∈ X L.

Then ∀ w ∈ X , (u w) ∈ L and (v w) ⊲ * (u w). Since L is a saturated set, we have ∀ w ∈ X , (v w) ∈ L, thus v ∈ X L.
Now, we are going to define the realizability model for the system S µ . For that, we need many bottom sets (⊥ ⊥ i ) i∈I including a particular one denoted by ⊥ ⊥ 0 . We also need several sets of µ-variables (C i ) i∈I which allow to pass from bottoms to ⊥ ⊥ 0 and vice versa. We also allow that the models have particular sets (R j ) j∈J satisfying some properties. In order to obtain the completeness theorem, it is possible to take from the beginning I = IN without considering the sets (R j ) j∈J . However, the flexibility to have I ⊆ IN and some sets (R j ) j∈J will allow to have more models. This will also allow the use of the correctness lemma in order to study the computational behaviour of some typed terms (cf. the example given at the end of this section, Theorem 2.4).

Definition 2.7

1. A model M of S µ is defined by giving three subsets (C i ) i∈I , (⊥ ⊥ i ) i∈I , (R j ) j∈J where :

• I, J are subsets of N such that 0 ∈ I,

• (C i ) i∈I a sequence of disjoint infinite subsets of µ-variables,

• (⊥ ⊥ i ) i∈I and (R j ) j∈J sequences of non-empty saturated subsets of terms such that

• ∀ i ∈ I, if α i ∈ C i and u ∈ ⊥ ⊥ 0 then µα i .u ∈ ⊥ ⊥ i (i.e. if, for some α i ∈ C i , u[α := α i ] ∈ ⊥ ⊥ 0 , then µα.u ∈ ⊥ ⊥ i ), • ∀ i ∈ I, if α i ∈ C i and u i ∈ ⊥ ⊥ i , then (α i u i ) ∈ ⊥ ⊥ 0 , • ∀ j ∈ J, ∃ i ∈ I, ∃ X j ⊆ T <ω , such that R j = X j ⊥ ⊥ i . 2. If M = (C i ) i∈I , (⊥ ⊥ i ) i∈I , (R j
) j∈J is a model of S µ , we denote by |M| the smallest set containing the sets ⊥ ⊥ i and R j and closed under the constructor .

We will see further that we did not need to get the subsets (R j ) j∈J to have the correcteness lemma. We allow a model to have such sets to enrich the concept of model and give the possibility of interpreting the types with more options. Now we are going to prove that every element of a realizability model can be written as the orthogonal of a set of sequence terms. This property is essential to interpret the µ-variables and announce the generalized correctness lemma (Lemma 2.6). The difficulty here with respect to the semantics proposed in [START_REF] Nour | A semantical proof of strong normalization theorem for full propositional classical natural deduction[END_REF][START_REF] Nour | A Semantics of Realizability for the Classical Propositional Natural Deduction[END_REF][START_REF] Nour | A completeness result for the simply typed lambda-mu calculus[END_REF] is the presence of several bottoms. As for the orthogonal of an element of a model, we will choose the convenient bottom which has the smallest index (Lemma 2.5).

Lemma 2.4 Let

M = (C i ) i∈I , (⊥ ⊥ i ) i∈I , (R j ) j∈J be

a model and G ∈ |M|.

There exists a set X G ⊆ T <ω and i

∈ I such that G = X G ⊥ ⊥ i .
Proof By induction on G.

-

If G = ⊥ ⊥ i , take X G = {φ}.
-If G = R j , then, by definition of R j , G = X j ⊥ ⊥ i and we take X G = X j .

-

If G = G 1 G 2 , then, by induction hypothesis, G 2 = X G2 ⊥ ⊥ i where X G2 ⊆ T <ω , and take X G = {uv / u ∈ G 1 and v ∈ X G2 }. Definition 2.8 If M = (C i ) i∈I , (⊥ ⊥ i ) i∈I , (R j ) j∈J is a model and G ∈ |M|, let • w(G) the smallest integer i such that G = X ⊥ ⊥ i for some X ⊆ T <ω , • G ⊥ = {X ⊆ T <ω / G = X ⊥ ⊥ w(G) }. Lemma 2.5 Let M = (C i ) i∈I , (⊥ ⊥ i ) i∈I , (R j ) j∈J be a model and G ∈ |M|, then G = G ⊥ ⊥ ⊥ w(G) . Proof ⊆ : Let t ∈ G. If ū ∈ G ⊥ , then ū ∈ X ⊆ T <ω and G = X ⊥ ⊥ w(G) , thus (t ū) ∈ ⊥ ⊥ w(G) . Therefore t ∈ G ⊥ ⊥ ⊥ w(G) . ⊇ : By Lemma 2.4, we have G = X ⊥ ⊥ w(G) for some X ⊆ T <ω , then X ⊆ G ⊥ . Let t ∈ G ⊥ ⊥ ⊥ w(G) . We have ∀ ū ∈ X , ū ∈ G ⊥ , then (t ū) ∈ ⊥ ⊥ w(G) . Therefore t ∈ G.
We can now interpret the types in a model and also give the definition of the general interpretation of a type. Definition 2.9

1. Let M = (C i ) i∈I , (⊥ ⊥ i ) i∈I , (R j ) j∈J be a model. The correctness lemma is sort of a validation of the notion of models that we considered. It states that a term of a type A is within the general interpretation of A. As for the semantics defined in [START_REF] Nour | A completeness result for the simply typed lambda-mu calculus[END_REF], the proof of the correctness lemma is false and the mistake is difficult to find. It is the case of the typing rule (⊥) which is problematic. The mistake comes from the permission to have µ-variables in the sequence of terms by adopting Saurin's interpretation.

Lemma 2.6 (General correctness lemma)

Let M = (C i ) i∈I , (⊥ ⊥ i ) i∈I , (R j ) j∈J be a model, I an M-interpretation, Γ = {x k : A k } 1≤k≤n , ∆ = {α r : B r } 1≤r≤m such that α r ∈ C w(I(Br)) (1 ≤ r ≤ m), u k ∈ I(A k ) (1 ≤ k ≤ n), vr ∈ (I(B r )) ⊥ (1 ≤ r ≤ m)) and σ = [(x k := u k ) 1≤k≤n ; (α r := * vr ) 1≤r≤m ]. If Γ ⊢ u : A ; ∆, then uσ ∈ I(A).
Proof By induction on the derivation, we consider the last rule used. We can now state and prove the correctness lemma.

Corollary 2.1 (Correctness lemma) Let A be a type and t a closed term. If ⊢ t : A, then, t ∈ |A|.

Proof

Let M be a model and I an M-interpretation. Since ⊢ t : A, then, by the general correctness lemma, t ∈ I(A). This is true for any model M and for any M-interpretation I, therefore t ∈ |A|.

According to the cases → i and µ of the proof of Lemma 2.6, we observe that the saturation conditions can be weakened as follows. We do not need the saturation by anti-reduction but only the saturation by weak-head anti-reduction.

A set of terms S is saturated if :

• for all terms u, v, w, if (u[x := v] w) ∈ S, then (λx.u vw) ∈ S.

• for all terms u, v, if µα.u[α := * v] ∈ S, then (µα.u v) ∈ S.

We take an example from [START_REF] Nour | A completeness result for the simply typed lambda-mu calculus[END_REF] to show that it is sometimes useful not to have in a model an infinite number of bottoms as well as the relevance of the sets (R j ) j∈J . Let e = λx.µα.x, then we have ⊢ e :⊥→ X and for all finite sequence of terms t ū, (e t ū) ⊲ * µα.t. We will prove this general result.

Theorem 2.4 Let E be a closed term of type ⊥→ X, then, for each finite sequence of distinct λ-variables x ȳ, (E x ȳ) ⊲ * µ.x where µ.x denote the variable x preceded by µ-abstractions and µ-applications.

Proof

Let x ȳ be a finite sequence of distinct λ-variables,

C 0 = A, ⊥ ⊥ 0 = {t ∈ T / t ⊲ * µ.x}, R = {ȳ} ⊥ ⊥ 0 , M = C 0 , ⊥ ⊥ 0 , R and I the interpretation such that I(X) = R. By Corollary 2.1, E ∈ I(⊥→ X) = ⊥ ⊥ 0
({ȳ} ⊥ ⊥ 0 ). Since x ∈ ⊥ ⊥ 0 and ȳ ∈ {ȳ}, we have (E x ȳ) ∈ ⊥ ⊥ 0 , and finally (E x ȳ) ⊲ * µ.x.

The model that we considered in the previous proof only contains ⊥ ⊥ 0 and the set R is necessary to find the computational behavior of the term E.

The completeness result

Before presenting our completeness result, we need some definitions and some technical results.

Some results

Lemma 3.1 is very intuitive. It states that, for a variable y, if the term (t y) is normalizable, then t is also normalizable. The proof of this result in λ-calculus is very simple because a reduction of (t y) will automatically give a reduction of t (the variable y interacts only when t reduces to a λ-abstraction λx.t ′ and we get in this case t ′ [x := y)). The situation in λµ-calculus is completly different. If the term t is reduced to a µ-abstraction µα.t ′ and we reduce the term (µα.t ′ y), we get µα.t ′ [α := * y], the variable y can be found in several sub-terms of t ′ and may also create other redex. Hence the need for a detailed and comprehensive proof of Lemma 3.1. Note also that the proof of this result in [START_REF] Nour | A completeness result for the simply typed lambda-mu calculus[END_REF] is not correct. Lemma 3.1 Let t be a term and y a variable. If (t y) is normalizable, then t is also normalizable.

Proof

By induction on the pair (l, c) (for the lexicographical order) where l = l((t y)) and c = c(t).

1. If t does not begin with λ or µ, then (t y) ⊲ l (t ′ y) where t ⊲ l t ′ . By induction hypothesis (l decreases), t ′ is normalizable, then t is also normalizable.

2. If t begins with a µ, then t = µα. λµ.(u ū).

• If u = (λx.v w), then On the other hand, t ⊲ l µα. λµ.(v[x := w] ū) = t ′ and (t ′ y) ⊲ l t ′′ , then (t ′ y) is normalizable, therefore, by induction hypothesis (l decreases), t ′ is normalizable, thus t is also normalizable.

• If u = (µβ.v w), then (t y) ⊲ l µα. λµ.(µβ.v[α := * y] w[x := * y] ū[α := * y])⊲ l µα. λµ.(µβ.v[α := * y][β := * w[α := * y]] ū[α := * y]) = µα. λµ.(µβ.v[β := * w[α := * y]] ū[α := * y)] = t ′′ .
On the other hand, t ⊲ l µα. λµ.(µβ.v[β := * w] ū) = t ′ and (t ′ y) ⊲ l t ′′ , then (t ′ y) is normalizable, therefore, by induction hypothesis (l decreases), t ′ is normalizable, thus t is also normalizable.

• If u = x, then (t y) ⊲ l µα. λµ.(x u 1 [α := * y] . . . u n [α := * y]).
The term u i [α := * y] is normalizable and (µα.u i y) ⊲ l µα.u i [α := * y], then (µα.u i y) is normalizable and, by induction hypothesis (l does not decrease but c decreases), µα.u i is normalizable, thus u i is also normalizable. We deduce that t is also normalizable.

• If u = (β u ′ ), then (t y) ⊲ l µα. λµ.((β u ′ [α := * y]) u 1 [α := * y] . . . u n [α := * y]).
As in the previous case, we prove that the terms u ′ , u 1 , . . . , u n are normalizable, then t is also normalizable.

• If u = (α u ′ ), then (t y) ⊲ l µα. λµ.((α (u ′ [α := * y] y)) u 1 [α := * y] . . . u n [α := * y]).
As in the previous case, we prove that the terms (u ′ y),u 1 , . . . , u n are normalizable, then, by induction hypothesis (l does not decrease but c decreases), u ′ , u 1 , . . . , u n are normalizable, then t is also normalizable.

If t begins with λ, we do the same proof

In the technical results that we prove in this section, a particular kind of redex appears (the argument of λ-abstraction or µ-abstraction is a variable). It is therefore helpful to understand what is happening by reducing these redexes. Lemma 3.2 will not be used in other proofs but will explain what happens at this special reduction. Definition 3.1 Let y be a variable. A y-redex is a β-redex or a µ-redex having y as an argument i.e. a term of the form (λx.t y) or (µα.t y). Lemma 3.2 Let t be a normal term and y a variable such that y ∈ F V (t).

If (t y) ⊲ + t ′ , then each redex in t ′ is a y-redex preceded by a µ-variable.

Proof By induction the number n of steps to reduce (t y) to t ′ .

1. If n = 1, then t is of the form λx.u or µα.u.

• If t = λx.u, then t ′ = u[x := y] which is normal.

• If t = µα.u, then t ′ = µα.u[α := * y]. Since u is normal, every new redex of u[α := * y] is of the form (v y) preceded by α.

2. If (t y) ⊲ n+1 t ′ , then (t y) ⊲ n t ′′ ⊲ t ′ . By induction, each redex in t ′′ is a y-redex preceded by a µ-variable. We examine the reduction t ′′ ⊲ t ′ .

• If the reduced y-redex of t ′′ is of the form (λx.u y), then the redexes of t ′ are the same in t ′′ except the redex that we contracted.

• If the reduced y-redex of t ′′ is of the form (µβ.u y), then y has evolved from being an argument to this redex, to become an argument for each subterm, of this redex, preceded by β ; so a new y-redex preceded by a µ-variable has been created and the initial redex could not get a new argument as it is locked by β.

Lemmas 3.3 and 3.4 will allow us to rebuild the typing in the proof of the completeness theorem. These results are quite technical and to prove them we have to generalize the needed results. For example, in Lemma 3.3, we need two substitutions σ and δ in order to prove Lemma 3.4 and also in Lemma 3.4, we need a simultaneous substitution because the length of such a substitution may increase (case (b)-1).

Lemma 3.3 Let t be a normal term, y a λ-variables such that y ∈ F V (t), σ = [(β j := * y) 1≤j≤m ], δ = [(α i := * y) 1≤i≤n ] and u = tσ. If Γ, y : A ⊢ uδ : C; (α i : B i ) 1≤i≤n , ∆, then Γ, y : A ⊢ u : C; (α i : A → B i ) 1≤i≤n , ∆.

Proof

By induction on the normal term t. As t is normal and tσδ is typable, t is restricted to the following forms : λx.t ′ , µα.t ′ , (x t 1 . . . t k ) and (γ t ′ ).

1. If t = λx.t ′ , then u = λx.u ′ where u ′ = t ′ σ, C = D → E and Γ, y : A, x : D ⊢ u ′ δ : E; (α i : B i ) i , ∆. By induction hypothesis, we have Γ, y : A, x : D ⊢ u ′ : E; (α i : A → B i ) i , ∆, then Γ, y : A, x : D ⊢ u ′ : E; (α i : A → B i ) i , ∆, thus Γ, y : A ⊢ λx.u ′ : D → E; (α i : A → B i ) i , ∆ and finally Γ, y : A ⊢ u : C; (α i : A → B i ) i , ∆. 2. If t = µα.t ′ , then u = µα.u ′ where u ′ = t ′ σ and Γ, y : A ⊢ u ′ δ :⊥; α : C, (α i : B i ) i , ∆. By induction hypothesis, we have Γ, y : A ⊢ u ′ :⊥; α : A → C, (α i : A → B i ) i , ∆, thus Γ, y : A, ⊢ µα.u ′ : A → C; (α i : A → B i ) i , ∆, and finally Γ, y : A ⊢ u : C; (α i : A → B i ) i , ∆. 3. If t = (x t 1 . . . t k ), then u = (x u 1 . . . u k ) where, for 1 ≤ r ≤ k, u r = t r σ, x has the type C 1 , . . . , C k → C and, for 1 ≤ r ≤ k, Γ, y : A ⊢ u r δ : C r ; (α i : B i ) i , ∆.
By induction hypothesis, we have, for 1 ≤ r ≤ k, Γ, y :

A ⊢ u r : C r ; (α i : A → B i ) i , ∆, then Γ, y : A ⊢ (x u 1 . . . u r ) : C; (α i : A → B i ) i , ∆ and finally Γ, y : A ⊢ u : C; (α i : A → B i ) i , ∆.
4. If t = (γ t ′ ) where γ = α i and γ = β j , then u = (γ u ′ ) where u ′ = t ′ σ, C =⊥, γ has the type D and Γ, y :

A ⊢ u ′ δ : D; (α i : B i ) i , ∆. By induction hypothesis, we have Γ, y : A ⊢ u ′ : D; (α i : A → B i ) i , ∆, then Γ, y : A ⊢ (γ u ′ ) :⊥; (α i : A → B i ) i , ∆ and finally Γ, y : A ⊢ u : C; (α i : A → B i ) i , ∆. 5. If t = (γ t ′ ) where γ = β k (1 ≤ k ≤ m), then u = (γ (u ′ y)) where u ′ = t ′ σ, C =⊥, γ has the type D and Γ, y : A ⊢ (u ′ δ y) : D; (α i : B i ) i , ∆, thus Γ, y : A ⊢ u ′ δ : A → D; (α i : B i ) i , ∆. By induction hypothesis, we have Γ, y : A ⊢ u ′ : A → D; (α i : A → B i ) i , ∆, then Γ, y : A ⊢ (γ (u ′ y)) :⊥; (α i : A → B i ) i , ∆ and finally Γ, y : A ⊢ u : C; (α i : A → B i ) i , ∆. 6. If t = (γ t ′ ) where γ = α k (1 ≤ k ≤ n), then u = (γ u ′ ) where u ′ = t ′ σ, uδ = (γ (u ′ δ y), C =⊥ and Γ, y : A ⊢ (u ′ δ y) : B k ; (α i : B i ) i , ∆, then Γ, y : A ⊢ u ′ δ : A → B k ; (α i : B i ) i , ∆.
By induction hypothesis, we have Γ, y :

A ⊢ u ′ : A → B k ; (α i : A → B i ) i , ∆, then Γ, y : A ⊢ (γ u ′ ) :⊥; (α i : A → B i ) i , ∆ and finally Γ, y : A ⊢ u : C; (α i : A → B i ) i , ∆.

Completeness model

We will now prove that if t is in the general interpretation of a type A, then t has the type A. For this, we will construct a particular term model M in which, we will get the equivalence between "having the type A" and "being within the type A" (see Lemma 3.6). The construction of this model looks like the constructions of the completeness models of the papers [START_REF] Hindley | The simple semantics for Coppo-Dezani-Sallé types[END_REF][START_REF] Hindley | The completeness theorem for typing λ-terms[END_REF][START_REF] Hindley | Curry's type-rules are complete with respect to the F-semantics too[END_REF][START_REF] Hindley | Basic Simple Type Theory[END_REF][START_REF] Labib-Sami | Typer avec (ou sans) types auxiliaires[END_REF][START_REF] Farkh | Un résultat de complétude pour les types ∀ + du système F . CRAS[END_REF][START_REF] Farkh | Résultats de complètude pour des classes de types du système AF 2[END_REF][START_REF] Kamareddine | A completeness result for a realizability semantics for an intersection type system[END_REF][START_REF] Nour | A completeness result for the simply typed lambda-mu calculus[END_REF]. We start with enumerating infinite sets of variables (which will be parameters of this model), then enumerating sets of types and finally fixing two infinite contexts (by associating enumerated types to enumerated variables) in which the terms will be typed. This will allow to define the bottoms and the variable sets associated to the models. Note that in this completeness model we don't need the sets (R j ) j∈J .

Definition 3.2 1. Let V 1 = {x i / i ∈ N} (resp., V 2 = {α i / i ∈
N} be an enumeration of an infinite set of λ-variables (resp., µ-variables). We put

V = V 1 V 2 . 2. Let T 1 = {A i / i ∈ N} and T 2 = {B i / i ∈ N} be enumerations of all types
where each type comes infinitely many times.

3. We define G = {x i : A i / i ∈ N} and D = {α i : B i / i ∈ N}.

4. Let u be a term, such that F V (u) ⊆ V, the contexts G u (resp. D u ) are defined as the restrictions of G (resp. D) at the declarations containing the variables of F V (u). 6. Let P = {X i / i ∈ N} be an enumeration of {⊥} ∪P. We assume that X 0 =⊥.

For each

i ∈ N, let ⊥ ⊥ i = {t / G ⊢ * t : X i ; D} and
C i = {α ∈ V 2 / (α : X i ) ∈ D}. Lemma 3.5 M = (C i ) i∈N , (⊥ ⊥ i ) i∈N , ∅ is a model for S µ .
Proof It is easy to show that (⊥ ⊥ i ) i∈N is a sequence of saturated subsets of terms.

• ∀ i ∈ N, if α ∈ C i and u ∈ ⊥ ⊥ 0 , then (α : X i ) ∈ D and G ⊢ * u :⊥; D, therefore G ⊢ * µα.u : X i ; D, thus µα.u ∈ ⊥ ⊥ i . • ∀ i ∈ N, if α ∈ C i and u ∈ ⊥ ⊥ i , then (α : X i ) ∈ D and G ⊢ * u : X i ; D, therefore G ⊢ * (α u) :⊥; D, thus (α u) ∈ ⊥ ⊥ 0 .
Observe that the model M is parameterized by the two infinite sets of variables and the enumerations. We need just these infinite sets of variables and not all the variables. This is an important remark since it will serve us in the proof of compleness theorem (Theorem 3.1).

Definition 3.3 We define the M-interpretation I as follows

∀ i ∈ N, I(X i ) = ⊥ ⊥ i .
The following lemma is the generalized version of the completeness theorem. It states the equivalence between "a term t is of type A in the fixed contexts" and "a term t belongs to the interpretation of the type A in the model M". The proof is done by simultaneous induction and uses the technical lemmas from the beginning of this section. Lemma 3.6 Let A be a type and t a term.

1. If G ⊢ * t : A ; D, then t ∈ I(A). 2. If t ∈ I(A), then G ⊢ * t : A ; D.
Proof By a simultaneous induction on c(A). We can now state and prove the completeness theorem. Theorem 3.1 (Completeness theorem) Let A be a type and t a term.

We have t ∈ |A| iff there exists a closed term t ′ such that t ⊲ * t ′ and ⊢ t ′ : A. Proof ⇐: By Corollary 2.1, t ′ ∈ |A|, then, t ∈ |A| because |A| is saturated.

⇒: We consider an infinite set of λ and µ variables Ω which contains none of the free variables of t, then from this set we build the completeness model as described in Definition 3.2. If t ∈ |A|, then t ∈ I(A), hence by (2) of Lemma 3.6 and by the fact that F V (t ′ ) ⊆ F V (t), we have t ⊲ * t ′ and ⊢ t ′ : A.

Here are some direct and unexpected consequences of the completeness theorem.

Corollary 3.1 Let A be a type and t a term.

1. If t ∈ |A|, then t is normalizable.

2. If t ∈ |A|, then there exists a closed term t ′ such that t ≃ t ′ .

3. The set |A| is closed under equivalence.

Proof

(1) and ( 2) are direct consequences of Theorems 2.3 and 3.1. (3) can be deduced from Theorem 3.1 and Lemma 2.6.

Future work

Throughout this work we have seen that the propositional types of the system S µ are complete for a realizability semantics. Two questions will be interesting to study.

1. The models that we have considered in this paper are sufficient to get correctness and completeness results: the saturation conditions that we have imposed in these models allow to have these two results. It will be interesting to understand more this kind of models: for example, build models with more bottoms to study the computational behaviour of some typed terms.

2. What about the types of the second order typed λµ-calculus? We know that, for the system F , the ∀ + -types (types with positive quantifiers) are complete for a realizability semantics (see [START_REF] Farkh | Un résultat de complétude pour les types ∀ + du système F . CRAS[END_REF][START_REF] Labib-Sami | Typer avec (ou sans) types auxiliaires[END_REF]). But for the classical system F , we cannot easily generalize this result. We think we need to add more restrictions on the positions of ∀ in the ∀ + -types to obtain the smallest class of types that we suppose can be proved to be complete.

  (a) An M-interpretation I is a function X → I(X) from the set of propositional variables P to |M| which we extend for any formula as follows: I(⊥) = ⊥ ⊥ 0 and I(A → B) = I(A) I(B). (b) For any type A, we denote |A| M = {I(A) / I an M-interpretation} the interpretation of A in the model M. 2. For any type A, we denote |A| = {|A| M / M a model} the general interpretation of A .

ax:

  In this case u = x k and A = A k , then uσ = u k ∈ I(A). → i : In this case u = λx.v and A = B → C such that Γ, x : B ⊢ v : C ; ∆. Let w ∈ I(B) and δ = σ + [x := w], by induction hypothesis, vδ ∈ I(C). Since (λx.vσ w) ⊲ * vδ, then (λx.vσ w) ∈ I(C). Therefore λx.vσ ∈ I(B) I(C) and finally uσ ∈ I(A).→ e : In this case u = (u 1 u 2 ), Γ ⊢ u 1 : B → A ; ∆ and Γ ⊢ u 2 : B ; ∆. By induction hypothesis, u 1 σ ∈ I(B) I(A) and u 2 σ ∈ I(B), therefore (u 1 σ u 2 σ) ∈ I(A), i.e. uσ ∈ I(A). µ: In this case u = µα.v and Γ ⊢ v :⊥ ; α : A, ∆. We can assume that α is a new variable which belongs to C w(I(A)) (there is always such a variable because the sets C i are infinite). Let v ∈ (I(A)) ⊥ and δ = σ + [α := * v]. By induction hypothesis, vδ ∈ ⊥ ⊥ 0 , then µα.vδ ∈ ⊥ ⊥ w(I(A)) . Since (µα.vσ v) ⊲ * µα.vδ, then, (µα.vσ v) ∈ ⊥ ⊥ w(I(A)) . We deduce that for all v ∈ (I(A)) ⊥ , (µα.vσ v) ∈ ⊥ ⊥ w(I(A)) , therefore µα.vσ ∈ I(A), i.e. uσ ∈ I(A). ⊥: In this case u = (α r v), A =⊥ and Γ ⊢ v : B r ; ∆. By induction hypothesis, vσ ∈ I(B r ), hence (vσ vr ) ∈ ⊥ ⊥ w(I(Br)) , therefore (α r (vσ vr )) ∈ ⊥ ⊥ 0 , i.e. uσ ∈ I(A).

(

  t y) ⊲ l µα. λµ.(λx.v[α := * y] w[α = * y] ū[α := * y])⊲ l µα. λµ.(v[α := * y][x := w[α := * y]] ū[α := * y]) = µα. λµ.(v[x := w][α := * y] ū[α := * y]) = t ′′ .

Lemma 3 . 4

 34 Let t be a normal term, y a λ-variable such that y ∈ F V (t) and σ = [(α i := * y) 1≤i≤n ]. (b) If t = µβ.u, then (tσ y) ⊲ µβ.u[σ, β := * y] ⊲ * t ′ , therefore, t ′ = µβ.u ′ , u ′ is the normal form of u[σ, β := * y] and Γ, y : A ⊢ u ′ :⊥; β : C, ∆. By induction hypothesis (2), we have Γ, y : A ⊢ uσ[β := * y] :⊥; β : C, ∆, then, by Lemma 3.3, Γ, y : A ⊢ uσ :⊥; β : A → C, ∆, thus Γ, y : A ⊢ µβ.uσ : A → C; ∆, and finally Γ, y : A ⊢ tσ : A → C; ∆. (c) If t = (x u 1 . . . u m ), then t ′ = (x u ′ 1 . . . u ′ m y) where, for 1 ≤ j ≤ m, u ′ j is the normal form of u j σ, x has the type C 1 , . . . , C n , A → C and, for 1 ≤ j ≤ m, Γ, y : A ⊢ u ′ j : C j ; ∆. By induction hypothesis (2), we have Γ, y : A ⊢ u j σ : C j ; ∆, then Γ, y : A ⊢ (x u 1 σ . . . u n σ) : A → C; ∆ and finally Γ, y : A ⊢ tσ : A → C; ∆. 2. As t is normal and t ′′ is typable, t is restricted to the following forms λx.u, µβ.u, (x u 1 . . . u m ) and (β u). (a) If t = λx.u, then t ′′ = λx.u ′′ where u ′′ is the normal form of uσ, C = D → E and Γ, y : A, x : D ⊢ u ′′ : E; ∆. By induction hypothesis (2), we have Γ, y : A, x : D ⊢ uσ : E; ∆, then Γ, y : A ⊢ λx.uσ : D → E; ∆ and finally Γ, y : A ⊢ tσ : C; ∆. (b) If t = µβ.u, then t ′′ = µβ.u ′′ where u ′′ is the normal form of uσ and Γ, y : A ⊢ u ′′ :⊥; β : C, ∆. By induction hypothesis (2), we have Γ, y : A ⊢ uσ :⊥; β : C, ∆, then Γ, y : A ⊢ µβ.uσ : C; ∆ and finally Γ, y : A ⊢ tσ : C; ∆. (c) If t = (x u 1 . . . u m ), then t ′′ = (x u ′′ 1 . . . u ′′ m ) where, for 1 ≤ j ≤ m, u ′′ j is the normal form of u j σ, x has the type C 1 , . . . , C m → C and, for 1 ≤ j ≤ m, Γ, y : A ⊢ u ′′ j : C j ; ∆. By induction hypothesis (2), we have, for 1 ≤ j ≤ m, Γ, y : A ⊢ u j σ : C j ; ∆, then Γ, y : A ⊢ (x u 1 σ . . . u m σ) : C; ∆ and finally Γ, y : A ⊢ tσ : C; ∆. (d) If t = (β u) where β = α j , then t ′′ = (β u ′′ ) where u ′′ is the normal form of uσ, C =⊥, β has the type D and Γ, y : A ⊢ u ′′ : D; ∆. By induction hypothesis (2), we have Γ, y : A ⊢ uσ : D; ∆, then Γ, y : A ⊢ (β uσ) :⊥; ∆ and finally Γ, y : A ⊢ tσ : C; ∆. (e) If t = (α j u) (1 ≤ j ≤ n), then t ′′ = (α j u ′′ ) where u ′′ is the normal form of (u j σ y), C =⊥ and Γ, y : A ⊢ u ′′ : B; ∆. By induction hypothesis (1), we have Γ, y : A ⊢ uσ : A → B; ∆, then Γ, y : A ⊢ (α j (uσ y)) :⊥; ∆ and finally Γ, y : A ⊢ tσ : C; ∆.

5 .

 5 The notation G ⊢ u : C; D means that G u ⊢ u : C; D u , we denote G ⊢ * u : C; D iff there exists a term u ′ , such that u ⊲ * u ′ and G ⊢ u ′ : C; D.

1 .

 1 (a) If A = X or ⊥, the result is immediate from the definition of I.(b) If A = B → C, then t ⊲ * t ′ such that: G ⊢ t ′ : B → C ; D. Let u ∈ I(B).By induction hypothesis (2), we have G ⊢ * u : B ; D, this implies that u ⊲ * u ′ and G ⊢ u ′ : B ; D. Hence G ⊢ (t ′ u ′ ) : C ; D, so, by the fact that (t u) ⊲ * (t ′ u ′ ), we have G ⊢ * (t u) : C ; D, then, by induction hypothesis (1), (t u) ∈ I(C). Therefore t ∈ I(B → C).

2 .

 2 (a) If A = X or ⊥, the result is immediate from the definition of I. (b) If A = B → C and t ∈ I(B)I(C), let y be a λ-variable such y ∈ F V (t) and (y : B) ∈ G. We have y : B ⊢ y : B, hence, by induction hypothesis (1), y ∈ I(B), then, (t y) ∈ I(C). By induction hypothesis (2), G ⊢ * (t y) : C ; D, then (t y) ⊲ * u such that G ⊢ u : C ; D and, by the Lemma 3.1, t is a normalizable term. Let t ′ (resp. u ′ ) be the normal form of t (resp. of u).So (t ′ y) ⊲ * u ′ , by Lemma 3.4, G ⊢ t ′ : B → C ; D, then G ⊢ * t : B → C ; D,Note that the item 1 of Lemma 3.6 can not be deduced from the correctness lemma. This comes from the presence of contexts G and D to type a reduced of term t.

  Theorem 2.1 (Confluence result) If t ⊲ * t 1 and t ⊲ * t 2 , then there exists t 3 such that t 1 ⊲ * t 3 and t 2 ⊲ * t 3 . If Γ ⊢ t : A; ∆ and t ⊲ * t ′ then Γ ⊢ t ′ : A; ∆.

	Theorem 2.2 (Subject reduction) Theorem 2.3 (Strong normalization) If Γ ⊢ t : A; ∆, then t is strongly nor-
	malizable.
	We need some specific definitions and notations.
	Definition 2.3
	1. Let t be a term. The term λµ.t denotes the term t preceded by a sequence of
	λ and µ abstractions.
	2. Let t be a term and v a finite sequence of terms (the empty sequence is denoted
	by ∅). The term (t v) is defined by (t ∅) = t and (t uū) = ((t u) ū).
	3. Let us recall that a term t either has a head redex (i.e. t = λµ.(u v) where u
	is a redex called the head redex), or is in head normal form (i.e. t = λµ.(x v)
	or t = λµ.

(α u v) where x and α are variables called the head variable).

Proofs are presented in natural deduction system with several conclusions, such that formulas in the left-hand-side of ⊢ are indexed by λ-variables and those in right-hand-side of ⊢ are indexed by µ-variables, except one which is indexed by a term. Let t be a λµ-term, A a type, Γ = {x i : A i } 1≤i≤n and ∆ = {α j : B j } 1≤j≤m contexts, using the following rules, we will define "t typed with type A in the contexts Γ and ∆" and we denote it Γ ⊢ t : A ; ∆.Γ ⊢ x i : A i ; ∆ ax 1 ≤ i ≤ n Γ, x : A ⊢ t : B; ∆ Γ ⊢ λx.t : A → B; ∆ → i Γ ⊢ u : A → B; ∆ Γ ⊢ v : A; ∆ Γ ⊢ (u v) : B; ∆ → e

Acknowledgements. We wish to thank P. Battyányi and N. Bernard for the numerous corrections and suggestions.


Plato's Dogma

Western tradition has from the very start put forward a demanding definition of knowledge.

To know, having a true belief is not enough. Of course, true belief is a part of the story, but something else is requested. One wants, for example, to avoid to say that knowledge of the time could arise from the lucky observation, at midday, of a brocken clock whose hands are blocked on twelve o'clock. Beyond true belief, good reasons for having such a belief are requested to be considered as possessing knowledge. Plato's claim, in Meno 96c, is that others' testimony should not be counted among these good reasons.

Knowledge requires impact of the known on the knower and others' help cannot replace that impact : to know Larissa's way, I have to experience that at first hand by travelling this way. The transmission of the information by people who have that experience doesn't provide knowledge. In short, second-hand knowledge isn't properly knowledge. This assertion raises obvious problems on the way of understanding scientific knowledge in the frame of contemporary digital networks.

The aim of this paper is, neither to contest Plato's claim -Plato has visibly put the finger on an important distinction -, nor to solve the problem it raises, namely to propose an original solution for the equation Knowledge = True Belief + X. I just want to argue that the exclusion of other's contribution is unrealistic, should knowledge be considered as humanly attainable : human life is too short for Platonic, solitary knowledge. I'd like also to establish that cooperation, in the domain of knowledge, has two specific features that make it both achievable and productive : on one hand, it escapes the well-known difficulties raised by the Prisoner's dilemma, on the other hand sharing knowledge is more creative than any other sort of sharing.

The feasibility of epistemic cooperation

2.1 The general difficulty of cooperation has its roots in the link between two propositions : (i) Individuals clearly recognise the benefits they can gain from cooperation, which is prima facie a recommandable attitude (ii) They also realise that they could receive those same benefits by refraining from cooperating themselves, so that they have good reasons for defection In short, people feel inclined to be defectors while they perceive the interest of cooperation and this situation tend to make cooperation impossible, though desirable.

For the sake of concreteness, the following example can be proposed to explain the problem, which has been exposed in formal terms by A.W. Tucker back in 1951. Two cars are crossing at night and the drivers have the choice between keeping strong lights () and moving to weak lights (). Reasoning from the viewpoint of the first driver :

(i) Better to be offensive than been betrayed, for I'll see better this way : (,) > (,) (ii) For the same reason, better to betray than to cooperate : (,) > (,)

In any case, the rational choice is to keep strong lights, hence the following gains table :

   0/0 2/-1  -1/2
1/1 One that basis, the actual choice of both drivers will be to keep strong lights, while each of them would win more if they cooperate by moving both to weak lights, which is the social optimum, ie the maximal gain for the group : (,) > (,) > (,) > (,) 2.2 Things are different with epistemic cooperation, namely information exchange. That difference rests on the fact that information is a good which is kept when it's given. Give an euro, you don't have it longer. Give a piece of information ϕ , it is still available to you. That constrat feature has two tremendous consequences :

(i) The silence of the defector is at no cost for the cooperator : (,) ⊁ (,ϕ) (ii) Nothing is gained by informational treason : (,ψ) ⊁ (ϕ,ψ) Thus, whatever the other decides, the choice of opening him the data one possesses is not irrational. For information sharing, the gains table is this :

 ψ  0/0 1/0 ϕ 0/1 1/1
That means that, in the realm of information, social optimum is reachable. Epistemic cooperation is easy :

(,ψ) ≥ (ϕ,ψ) > (,) ≥ (ϕ,)

The productivity of epistemic cooperation

A general property of sharing is this : every item possessed by the group after the sharing is an item that some member of the group possessed before the sharing. Information performances of human epistemic achievements. The objective of philosophy and social sciences should be, rather than the pursuit of epistemic ideals that are clearly beyond the reach of finite creatures, to reflect on the concrete modalities of accomplishment and improvement of that cooperation in actual societies and organisations, especially to understand the contemporary move of opening the data.

sharing does better: the cooperative group knows more than any of its members before information exchange : if a knows that ϕ and if b knows that ϕ → ψ, then they know together that ψ, while none of them got this information before the exchange. By reference to mathematics, in which this kind of cooperation is of constant use -real mathematics are typically a typically non-Platonistic activity, for never start from axioms, but we use freely the results of our predecessors as lemmas -, I suggest to call that « lemmatic productivity ».

Well-known results in contemporary proof theory (Gödel, Boolos) shows that this use of lemmas, namely this use of cooperative knowledge among mathematicians, results in a huge speed-up : there are direct (« solitary », Platonistic) proofs that are longer by a factor of a tower of exponentials that team, lemmatic proofs. In other words, there are pieces of mathematical knowledge that weren't available to human beings if they would process according to Plato's standards.

To summarize, cooperative knowledge is both feasible and productive. Its rejection,