David Ginsbourger

Joint Work with Janis Janusevkis

Rodolphe Le Riche

Dealing with asynchronicity in parallel Gaussian Process based global optimization *

During the last decade, Kriging-based sequential algorithms like EGO and its variants have become reference optimization methods in computer experiments. Such algorithms rely on the iterative maximization of a sampling criterion, the expected improvement (EI), which takes advantage of Kriging conditional distributions to make an explicit trade-off between promizing and uncertain search space points. We have recently worked on a multipoints EI criterion meant to simultaneously choose several points, which is useful for instance in synchronous parallel computation. Here we propose extensions of these works to asynchronous parallel optimization and focus on a variant of EI, EEI, for the case where some new evaluation(s) have to be done while the reponses of previously simulations are not all known yet. In particular, different issues regarding EEI's maximization are addressed, and a proxy strategy is proposed.

Introduction

Sampling criteria such as the Expected Improvement (EI) allow sequentially choosing evaluation points in Gaussian Process (GP) based optimization algorithms. A major strength of using EI in a sequential procedure is that it progressively integrates available observations (points and responses), and thus avoids resampling at already explored points, at least in the case of noise-free simulations.

Recent works deal with the adaptation of EI for parallel Kriging-based optimization.

In particular, a multipoints version of EI, called q-EI (or simply EI when there is no ambiguity), has been proposed for synchronous parallel Kriging-based optimization. q-EI measures the joint potential of a given additional q-points design of experiments. So, a natural parallelization of EI algorithms for q synchronous processors is to maximize q-EI at each iteration, with update of the Kriging metamodel (including possible re-estimation of covariance parameters) whenever new observations are assimilated. However, maximizing q-EI is in most cases unaffordable, all the more so that the dimension of inputs d and the number of points q increase. Furthermore, evaluating q-EI when q ≥ 3 bases on a Monte Carlo method relying on GP conditional simulations, which would make this intermediate optimization problem noisy and potentially very time consuming. Heuristic strategies such as the Constant Liar (CL) and the Kriging Believer (KB) have been proposed in [START_REF] Ginsbourger | Computational Intelligence in Expensive Optimization Problems, chapter "Kriging is well-suited to parallelize optimization[END_REF] to circumvent the computational difficulties associated with q-EI maximization, by turning it into a stepwise maximization with virtual intermediate observation values.

In this report, we focus on the case of asynchronous parallel Kriging-based optimization, i.e. where sampling decisions have to be made before all previously started simulations have produced their result. Hence we have to distinguish between already visited points, currently visited (or "busy") points, and candidate points for forthcoming simulations. Having to take busy points into account within GP modeling sends back to similar problems encountered in the heuristic strategies mentioned above, so that we take advantage of previous work on that topic, and revisit those heuristic strategies in a more general manner.

After some necessary definitions concerning the EI criterion with (partially or completely) enriched information, a variant of EI is proposed for the case where a processor did not give its result yet. Relying on conditional simulations, EEI proves to be a sensible criterion, but practically not straightforward to maximize. A special variant of CL with random lie is then investigated to generate a finite set of candidate EEI maximizers, and gives surprisingly excellent results on the basis of a first 1-dimensional toy example. Some research perspectives and a rich bibliography close this report, and set a framework for additional testing and developements to be made in forthcoming project phases.

Injecting incomplete information in EI criteria

EI with (partially) enriched information

The regular EI is defined as follows

EI(x) = E (min(Y (X)) -Y (x)) + |A , (1)
where (.) + = max(0, .), and A = {Y (X) = y} is the event summing up all currently available observation points and corresponding responses.

Let us now assume that an evaluation of y at point x busy ∈ D (say at an EI global maximizer, assumed unique for convenience) has been started, that the result is not known yet, and that one wishes to determine the next most promizing point (in terms of EI) where to perform an evaluation using a newly available processor.

Ignoring that an evaluation is going on at x busy may cause loosing crucial information for the next evaluation(s). However, it is not possible to add the event Y (x busy ) = y(x busy ) to A since y(x busy ) is not kwown yet.

Question 1 How is it possible to inject the partial knowledge that an evaluation is going on at x busy in the EI criterion without knowing y(x busy )?

Before giving a probabilistic answer to that question, let us introduce some necessary additional concepts and notations.

Definition 1 Given X, y, A as above, and an additional point x add ∈ D together with its corresponding response y add , we denote by EI with enriched information the function

x ∈ D -→ EI(x; x add , y add ) := E (min(Y (X), y add ) -Y (x)) + |A, Y (x add ) = y add (2)
This modification of the EI criterion basically amounts to updating the underlying conditioning event A to Y (X) = y, Y (x add ) = y(x add ) . As a consequence, the EI with enriched information is 0 at x add whatever the observation value y add . This property will be useful in the sequel since we will actually often be in situations where the value of y add is unkown.

A probabilistic answer to question 1 is to continue treating the unknown y(x busy ) as a random variable Y (x busy ), but to insert it in on the side of conditioning events by plugging it in the previously defined EI with enriched information.

Definition 2 Let us define the EI with partially enriched information as EI(x; x busy ) : = EI(x; x busy , Y (x busy ))

= E min(Y (X), Y (x busy )) -Y (x) + |A, Y (x busy ) (3)
For any given fixed x ∈ D, EI(x; x busy ) is hence a function of the random variable Y (x busy ), thus inheriting from its randomness. Indeed, the classical EI formula can be developed, and the randomness of the obtained expression appears clearly through the instances of Y (x busy ) in the current minimum and in the Kriging mean.

Y sim i ∼ L(Y (x busy )|A) 3: EI i (x) = EI(x; x busy , Y sim i ) 4: end for 5: EEI(x) = 1 n sim n sim i EI i (x)
Thus, a straightforward way of getting statistical estimates of EEI(x; x busy ) (pointwise, for given x ∈ D, or of the whole function EEI(.; x busy )) is to base on Monte Carlo drawings, as in alg. 2.1. Obviously, the reliability of such a Monte Carlo approximation of EEI will depend on the invested number of drawings n sim . To be more precise, on can state that for any fixed x ∈ D, the estimator EEI(x) obtained above is unbiased, and has a variance given by a formula of a well-known kind:

Var EEI(x) = 1 n sim EI(.; x busy , y busy ) -EEI(x) 2 f Y (x busy )|A (y busy )dy busy (7)

Main example

Let us consider a deterministic one-dimensional function,

y : x ∈ [0, 1] -→ y(x) = sin(10x + 1) (1 + x) + 2cos(5x) × x 4 ∈ R, (8)
and first approximate it using a Kriging model based on y's observation at a three-points design X = {0, 0.475, 0.95}. The chosen Simple Kriging model is centered, has a Matérn covariance structure with regularity coefficient ν = 3 2 , unit variance, and range parameter θ = 0.5 √ 3 . The objective function, the Kriging mean predictor, and the corresponding Expected Improvement function are represented on figure 2.1. This very simple example will enable us to get a first illustration of the previously discussed notions, and to put the finger on some related problems, in a surprisingly rather general way (despite the lowdimensional framework). Let us now detail the example. First, we consider the Kriging predictor and the EI function of figure 2.1, both in blue. Assume that a first processor is vacant, and that one wishes to use it to perform a fourth simulation. It is then natural to perform this additional simulation at the point maximizing the current version of EI, that is to say at the point 0.698 magnified by an orange dashed line on figure 2.1.

Let us now pretend that the evaluation of y at the latter point is getting started at a currently available processor, say proc 1 , and set x busy = 0.698. Assume further that a second processor, proc 2 , is becoming available while proc 1 is still busy with the computation of y(x busy ). The main issue here is obviously to choose x new , the point at which to evaluate y with proc 2 , in such a way that the all available information is optimally used.

Computing the EEI criterion of eq. 6 by means of a procedure such as alg. 2.1 will lead us to makes conditional simulations of Y (x new ) knowing the past observations. Before averaging out a whole collection of EI curves obtained by this means and maximizing the obtained EEI estimate, let us first focus on a single conditional simulation and detail the underlying mechanism. Figure 2.2 illustrates the effect of enriching EI with a simulated observation. The latter is represented by a green point on the upper graph, as well as the new (virtual) Kriging mean predictor. In the same color, the curve on the lower graph stands for the corresponding EI with enriched information. As mentioned earlier, this updated EI is null at x busy . Furthermore, since the simulated value of Y (x new ) is particularly low, and hence appealing in our minimization context, EI is now pointing to values of x close to x busy (note the EI values of smaller magnitude than at the previous step). However, choosing the global maximizer of this EI for x new does not completely make sense. Indeed, the simulated value of Y (x new ) is arbitrary, and another simulated value would maybe lead to discard this point and go for a candidate x new in a different zone of the input space.

It seems therefore necessary to propagate the uncertainty concerning the new EI function by integrating it over the possible scenarii concerning the value of Y (x new ), or at least to circumvent the problems associated to this unkown value and its variability by using some adapted heuristic. Here we propose at first to use brute force: simulating 100 values of Y (x new ) conditional on the past, calculate the 100 associated EI with enriched information, A natural surrogate for EEI maximization is to maximize its Monte Carlo estimate EEI, such as represented on figure 2.3 (lower graph, see maximization result above). However, n sim has to be chosen sufficiently large in order to guarantee a good approximation of EEI, which may cause high computational costs. Furthermore, based on figure 2.4 above, one can imagine that a small set of carefully selected EI's might lead the user to a simplified description of this family of curves, yielding an efficient proxy for EEI maximization. Let us now explore these questions in some more detail.

3 Maximization of the EEI and related problems 3.1 Direct approach: maximizing the mean of a random function

A bit of theory and bibliography

Maximizing the previously introduced EEI criterion is in fact a special case of a classic stochastic optimization problem, i.e. the maximization of an expectation function such as

x ∈ D -→ E[Q(x, ζ)], (9)
where Q is a function depending on x and on the scalar-or vector-valued random variable ζ), and the distribution of ζ is assumed known or at least reproducible by simulation.

Such problems are commonly solved in practice thanks to approximations of

E[Q(x, ζ)] by finite averages of the form 1 N N i=1 Q(x, ζ (i) )
, where N and the ζ (i) are chosen in order to get a good trade-off between the sample size (N , wished small) and a good approximation of the distribution of ζ by a uniform discrete law over the N -sample {ζ (1) , . . . , ζ (N ) }.

One natural idea is to generate {ζ (1) , . . . , ζ (N ) } by Monte Carlo, i.e. to draw by simulation a N -sample of variables independently following the distribution of ζ. This is what Shapiro calls SAA (Sample Average Approximation). To quote him, " The term sample average approximation method was coined in [START_REF] Kleywegt | The sample average approximation method for stochastic discrete optimization[END_REF], although this approach was used long before that paper under various names. Statistical properties of the SAA method are discussed in [START_REF] Shapiro | Stochastic Programming[END_REF] and complexity of two and multi-stage stochastic programming in [START_REF] Shapiro | Continuous Optimization: Current Trends and Applications, chapter On complexity of stochastic programming problems[END_REF] . . . Rates of convergence of Monte Carlo and Quasi-Monte Carlo estimates of the expected values are discussed in [START_REF] Niederreiter | Random Number Generation and Quasi-Monte Carlo Methods[END_REF]. Numerical experiments with the SAA method are reported in [START_REF] Linderoth | The empirical behavior of sampling methods for stochastic programming[END_REF][START_REF] Mak | Monte carlo bounding techniques for determining solution quality in stochastic programs[END_REF][START_REF] Verweij | The sample average approximation method applied to stochastic routing problems: a computational study[END_REF], for example. " Such an approach makes sense, and without going into difficult detail concerning the different kinds of stochastic convergence, the law of large numbers ensures (under specific conditions) that the Sample Average Approximation will resemble the expectation objective function E[Q(x, ζ)] always more as N grows, and that so will do their respctive maxima and maximizers. See e.g. [START_REF] Van Der | Asymptotic Statistics[END_REF] for a discussion on sufficient conditions for the sequence of proxy maximizers to converge to the actual maximizer in a suitable way.

Anyway, even under conditions where nice asymptotic properties might be guaranteed, the major question to answer in practice is the number of Monte Carlo simulations N needed to ensure that arg min 1

N N i=1 Q(x, ζ (i) ) is a reasonable approximation of arg min E[Q(x, ζ)].
A theoretical study of this would certainly be very demanding, and is somehow out of scope here. However, we will come back in the next section to our previous example, and propose some illustrations related to these convergence questions.

Back to the main example

Before focusing on the estimation of EEI and on the maximization of the obtained estimate, let us brievly study the variability of the maximum and maximizer of EI with enriched information when y busy randomly varies following the distribution defined by density 5. The y busy values used here are the same as on figures 2.3 and 2.4. The variability shown by the upper left histogram of fig. 3.1 illustrates the fact that the value of y busy significantly influences the EI with enriched information and its maximum. Indeed, a very low value of y busy changes the current minimum, and makes it harder to exceed. On the other hand, a very high value of y busy does not affect the current minimum but may locally attract the Kriging predictor, and prevents from any improvement in the close neighbourhood of x busy . However, depending on the rigidity of the covariance kernel used, such high y busy values might cause some low overshooting and could magnify the value of EI in farther areas. Finally, medium values of y busy , in particular slightly above the current minimum, are susceptible of keeping the EI maximum at the same order of magnitude as earlier. higher values of y busy tendencially matching with minimizers on the left, while smaller y busy seem pushing the maximizer of the enriched EI closer to x busy . Note that a reverse trend is similarly visible on the first cluster, which may presumably be imputed to some kind of rigidity effect, as evocated earlier: a very high y busy value would drastically lower EI in the close neighbourhood of x busy , but the associated curvature in the Kriging predictor would also create a steeper hill, moving the maximizer of the enriched x busy to the right of the left cluster. Finally, the right cluster corresponds to the lowest simulated values of y busy , with a similar slope to the one of the first cluster. A moderatly small value of y busy causes a slight decrease of the current minimum response, and sends the maximizer of the enriched EI to a zone with high variance, the right of the third cluser. As y busy decreases further, however, the influence of this very appealing value at x busy reaches the third cluster, progressively moving the maximizer of the enriched EI to the left of the cluster. The right graph of fig. 3.2 represents the evolution of the maximum of the enriched EI as y busy increases. Contrarily to the previous graph, this scatter plot seems to stem from a continuous function, which makes sense from a mathematical point of view. Indeed, the enriched EI is a continuous function of y busy , and hence absolutely continuous over any compact set. One can show that the maximum of EI with enriched information is consequently a continuous function of y busy . As could already be felt on the basis of the previous graphs, only the range of medium values of y busy breaks the monotonicty of this function. Indeed, for very small values of y busy , there isn't much room for improvement. Then, the maximum increases until y busy reaches the actual current minimum (red vertical line on the right graph of fig. 3.2). At this stage, the maximum of the enriched EI starts decreasing with increasing y busy : higher y busy now do not change anything to the minimum of reference, but do pull the response surface up in the neighbourhood of the maximizer of the enriched EI, hence affecting its maximum negatively through the increasing Kriging mean predictor. At a certain point, however, the maximizer of the enriched EI jumps to the left cluster, and the associated maximum starts again to increase with y busy . This last effect seems due to the previously evocated rigidity artifact, a higher observation value at x busy causing deeper valleys in the surrounding clusters.

We now continue with the maximization of the estimated EEI, and with an investigation concerning the number of y busy simulations needed here to achieve a good result. In order to see in what measure this early stability is due to the particular sample drawn in the previous example, let us generate other samples at random following the same distribution and observe the variability of the new estimated EEI maxima and maximizers. We follow for each simulated sample the same nesting scheme as above. Despite the particularly good results obtained in the previous example (stability for a sample of size greater than 8), the boxplots of fig. 3.4 are here to signify that this first attempt was rather lucky, and that significantly larger samples were nedeed in order to guarantee a sucessful approximate EEI maximization with high probability. On the left graph, the boxplots confirm again that we had been lucky in the previous experiment: here, we need to invest about 100 y busy simulations to get rid of approximate EEI maximizers landing in the right cluster (upper points in lower graph). As we can see on the right graph of figure 3.5, investing 20 conditional simulations leads to the good cluster (i.e. near to the actual EEI maximizer) in about 80% of the cases. This leaves 20% of misleading approximate optimization results, which a reasonable user may choose not to accept. Always on the same graph, increasing the sample size to 50 leads to a probability of about 95% to get an approximate optimizer in the good cluster, while the 100% probability level seems to be reached for a sample of 100 simulated y busy values. Working with an average of so many EI functions can be computationally very demanding, so that reliable and efficient methods involving a limited number of y busy values might be appealing. We address this issue in the following section, where encouraging results are obtained in the modest present framework case of a unique busy processor.

3.2 Towards reducing to a limited number of scenarii 3.2.1 Theory: per un pugno di quantili . . . In the last section, we proposed to approximate EEI by averaging several EI criteria with enriched information, where the unkown response y busy was randomly simulated following the "Kriging conditional distribution" of Y (x busy )|A.

Here we depart from this Monte Carlo approach by deterministically choosing a representative subset of y busy values, and restricting the EEI maximization to the maximizers of the different EI enriched with the latter y busy values.

The approach proposed here to get a subset of y busy values representing well the Kriging conditional distribution is to select quantiles of it. We focus on quantiles of level α, α varying regularly between 0.05 and 0.95 with a finesse depending on the chosen number of subset points. Denoting n quant this number of points, the proposed protocole reads:

1. Calculate n quant quantiles of Y (x busy )|A 2. For y busy equal to each of these quantiles, maximize the enriched EI 3. For each of the obtained maximizers, estimate EEI (possibly with the same n quant y busy values as earlier)

4. Choose the enriched EI maximizer with highest estimated EEI Such a technique should a priori not be expected to work well. In fact, in a general stochastic optimization framework, nothing guarantees that the maximum of an expected function will be reached at the maximizer of some of the underlying realizations. It is even easy to build counter-examples: consider for instance the piecewise linear function f 1 over [-1, 1] with slope 2 over [-1, 0] and slope 1 over [-1, 0], f 2 similarly defined with slopes -1 and -2, and f being a random function equal to f 1 or f 2 with probability one half. It is then clear that f 1 takes its global maximum (1) at 1, f 2 takes its global maximum (1) at -1, but none of these points is a maximizer of the expectation of f . indeed, the expectation value of f at these two points is -1, while the latter takes the value 0 (its maximum) at 0, which is not a maximum of f 1 nor f 2 . Note that a variant of this counter-example with positive functions may be constructed by a simple vertical translation.

Coming back to our EI functions with enriched information, things are going much better than in the counter-example above. Indeed, it is quite unlikely that a point being a EI maximizer for some value of y busy becomes dramatically bad for another y busy value. Furthermore, it is natural to suspect that a point maximizing EI with a high EI value for some y busy is a good one for EEI. If however the high potential of a point would be due to an artifact and rely on the precise y busy value considered in the enriched EI, then we could expect that the fact of averaging enriched EI values over several y busy candidates would smooth this outlier out and cancel the dominantion of this point. Even if we are not convinced that this method should work in every situation, the example below shows quite encouraging results. Before coming to any general conclusions however, the latter have to be questioned and complemented by further investigations.

Back to the main example

Let us first choose n quant = 10 and detail review the protocole above in the framework of our main example. We recall that the EEI maximizer obtained by Monte Carlo with a 100-sample over a 200-elements grid was 0.3467337. Now, we replace the Monte-Carlo sample by the 10 quantiles of Y (x busy )|A with respective levels 0.05, 0.1, . . . , 0.9, 0.95: been restricted in all cases to 200 points. Furthermore, this good finding might be highly depending on the number of quantiles, and even be non monotonic in n quant , which could lead to serious practical issues in the a priori choice of n quant . So let us go one step deeper, and investigate the influence of n quant on the approximate EEI maximizer obtained by the proposed method. Here below are the results obtained by repeating the quantile approximation and optimization method for n quant varying from 1 to 30:

> quantiles [1] -
> maximizers [1] 0.7487437 0.3618090 0.3618090 0.3467337 0.3517588 0.3517588 0.3467337 [START_REF] Barton | Minimization algorithms for functions with random noise[END_REF] 0.3517588 0.3467337 0.3467337 0.3467337 0.3467337 0.3467337 0.3467337 [START_REF] Casey | The scenario generation algorithm for multistage stochastic linear programming[END_REF] 0.3467337 0.3467337 0.3467337 0.3467337 0.3467337 0.3467337 0.3467337 [START_REF] Deák | Two-stage stochastic problems with correlated normal variables: computational experiences[END_REF] 0.3467337 0.3467337 0.3467337 0.3467337 0.3467337 0.3467337 0.3467337 [START_REF] Floudas | A review of recent advances in global optimization[END_REF] 0.3467337 0.3467337

We observe that after a first point (0.7487437) in the third cluster, all followers belong to the first cluster, and are close neighbours of 0.3467337. Starting from n quant = 9, they are even all equal to 0.3467337. Compared to the variability observed on fig. 3.4 for the case of Monte Carlo EEI estimation, the "quantile method" provides a deterministic result, free of any variability, and with very good performances on this example in terms of locating the EEI correctly based on a small number of scenarii. Indeed, 2 or 3 quantile values are necessary to locate the EEI maximizer in the right zone ("first cluster"), while n quant ≥ 9 guarantees the same result as found by Monte Carlo with a 100-elements sample (search restricted to a 200-points grid). Despite the impressively good results obtained on this example, one has also to notice and remember that n quant = 1 does lead to a sub-optimal cluster, which means in essence that plugging in the Kriging mean prediction (i.e. the KB strategy) as a proxy to the unknown y busy response is clearly not the best thing to do.

Conclusion and research perspectives

A variant of the EI criterion, EEI, has been proposed for the case of asynchronous Krigingbased parallel optimization. Here we have restricted our attention to the canonical situation where one processor is free while another one is still busy with the evaluation of the objective function at a candidate point x busy . The unkown response at x busy can be simulated conditional on the available information, hence providing a means to estimate EEI.

Estimating EEI by conditional simulations amounts to averaging several enriched EI criteria obtained with the simulated response values at x busy , i.e. applying several times a Liar strategy with a random lie generated by Monte Carlo. Maximizing the estimated EEI may then become quite computationally demanding, all the more so as the number of simulations gets large when it comes to approximating the actual EEI well. Here we relate that to a classical stochastic optimization problem, referred to as Sample Average Approximation in the litterature, and propose to simplify it by summarizing the conditional distribution of the unkown reponse(s) by a small set of representative scenarii.

The idea of reducing to a few scenarii is not new, and what is proposed here is just a first draft of what could be developed for EEI maximization. In our main example, summarizing the unkown reponse distribution by a few quantiles has given sensible results, and a good picture of the full Monte Carlo results (with 100 drawings) with a lower computationnal cost (10 evaluations). Moreover, restricting EEI maximization to the maximizers of the enriched EI criteria obtained by the "quantile method" has delivered the same results as by maximizing the 100-drawings Monte Carlo EEI estimate over a 200-points grid. This is a quite unexpected outcome, to be urgently investigated with further test configurations. Apart from a bigger scale testing, and the generalization to multiple busy and vacant processors, supplementary research could be done on several aspects including:

• a fine study of the impact of y busy on the enriched EI and its maximizer(s),

• applying curve classification to the EI functions obtained with many y busy values,

• distinguishing regions of low EI variation, in particular in higher dimensions.

The final report will include further tests and theoretical considerations related to the questions above. A further study of several articles listed in the following bibliography -and with the help of [START_REF] Maarten | Stochastic programming bibliography[END_REF]-is expected to shed some more light on existing tricks in Monte Carlo methods and scenarii selection for stochastic optimization.

Figure 2 . 1 :

 21 Figure 2.1: A first Kriging model, with maximization of the Expected Improvement.

Figure 2 . 2 :

 22 Figure 2.2: Evolution of EI afer one conditional simulation at x busy .

Figure 2 . 3 :

 23 Figure 2.3: 100 conditional simulations at x busy and the corresponding EEI estimate.

Figure 2 . 4 :

 24 Figure 2.4: 100 simulations of the Expected Improvement with enriched information, based on the simulated Y (x new ) of figure 2.3.

Figure 3 . 1 :

 31 Figure 3.1: Left: histograms of the minima and minimizers of the 100 EI with simulated enriched information represented on figure 2.4. Right: joint distribution.

Figure 3 . 2 :

 32 Figure 3.2: Left: Dependence bewteen the location of the maximizer of the enriched EI and y busy . Right: maximum of the enriched EI as a function of y busy .

Figure 3 . 3 :

 33 Figure 3.3: Evolution of EEI maxima and maximizers with progressively growing sample Fig. 3.3 shows how the maximum and the global maximizer of the estimated EEI evolves, when the sample size of y busy values used for the estimation of EEI varies. Here, only the 100 values previously simulated are used, and the increasing number of y busy values means that nested subsets of that 100 values are progressively considered (the first one, the two

Figure 3 . 4 :

 34 Figure 3.4: Boxplots retracing the evolution of EEI maxima and maximizers with progressively growing sample (1 to 20 here), when the sample is drawn 100 times at random.

Figure 3 . 5 :

 35 Figure 3.5: Left: boxplots retracing the evolution of EEI maxima and maximizers with progressively growing sample (1 to 100 here, 100 sample realizations). Right: proportion of approximate EEI maximizers in the first cluster in function of the sample size.

Figure 3 . 6 :

 36 Figure 3.6: Left: maximizers and maxima of the enriched EI criteria associated with the 10 quantile-based y busy values mentioned above. Right: enriched EI

  Since the function EI(.; x busy ) is consequently a random function, it does not make sense to maximize it in order to derive the next most promizing point x new .

	Question 2 Indeed, what would it mean to maximize a random function?
	Several alternatives are possible, such as maximizing quantiles of it conditional on the
	current information, or basically focus on the following conditional expectation function
	Definition 3 The expectation of EI(.; x busy ) conditional on A is denoted by
		EEI(.; x busy ) := E[EI(.; x busy )|A]	(4)
	Denoting by f Y (x busy )|A (.) the probability density function (pdf) of Y (x busy ) conditional
	on A, which is deduced from the standard gaussian pdf φ by an affine change of variable,
	f Y (x busy )|A (y busy ) =	1 s(x busy )	φ	y busy -m(x busy ) s(x busy )	(whenever s(x busy ) = 0 )	(5)
	we may in fact explicitely derive the latter conditional expectation in integral form:
	EEI(.; x busy ) = EI(.; x busy , y busy )f Y (x busy )|A (y busy )dy busy	(6)
	Now, EI(.; x busy , y busy ) depends on y busy in a quite complicated non-linear way, and there
	is no hope of getting an analytical expression for EEI, even though f Y (x busy )|A is known and
	rather simple. However, coming back to its probabilistic definition, EEI can be approxi-
	mated by averaging out the EI(.; x busy , y busy )'s obtained when drawing a sufficiently high
	number of y busy candidate values generated by using the conditional law of Y (x busy )|A.
	Algorithm 1 Estimate EEI using MC simulations
	1: for i ← 1, n sim do
	2:

  We notice that the seventh is exactly the previous EEI maximizer, and that the three following candidates are in its immediate neighbourhood. These values are plotted against the corresponding enriched EI values on the left graph of fig.3.6. We can observe that the three clusters are well represented, even if the associated enriched EI estimates do not respect the order observed in fig 3.2. This is due to the the approximation of these enriched EI on the basis of 10 y busy values only.We now restrict our attention to the 10 previously derived maximizers, and compute EEI estimates obtained at these points, enriched EI averages over the same 10 y busy values. The right graph of fig 3.2 represents the 10 enriched EI values obtained for each one of the 10 points. The four last points seem to clearly dominate the others in terms of median EI, which would not be necessarily the case for other metrics penalizing uncertainty. Here we give the estimated EEI values obtained by the "quantile approximation":

	1.52060808 -1.11769068 -0.87799880 -0.68650068 -0.51454523 -0.34811045
	[7] -0.17615500 0.01534313 0.25503501 0.65795240
	Maximizing the 10 obtained enriched EI criteria, we get the following candidates:
	> EI_maximizers
	[1] 0.7487437 0.7688442 0.7788945 0.7939698 0.5929648 0.5728643 0.3467337
	[8] 0.3517588 0.3567839 0.3618090
	> EEI_values
	[1] 0.03858103 0.04777052 0.05104971 0.05436474 0.05516403 0.05399162
	[7] 0.07446641 0.07434650 0.07404384 0.07355171
	And the point maximizing this rough EEI estimate among the 10 candidate points is the
	7 th , i.e. 0.3467337. This excellent result might seem relatively surprising, in particular
	its precision. But one may not forget that the search (enriched EI maximization) has


Hervé Grall
email: hgrall@mines-nantes.fr

Proving fixed points *

We propose a method to characterize the fixed points described in Tarski's theorem for complete lattices. The method is deductive: the least and greatest fixed points are "proved" in some inference system defined from deduction rules. We also apply the method to two other fixed point theorems, a generalization of Tarski's theorem to chain-complete posets and Bourbaki-Witt's theorem. Finally, we compare the method with the traditional iterative method resorting to ordinals and the original impredicative method used by Tarski.

We are interested in fixed points of maps defined over partially ordered sets (abbreviated as posets). Consider Tarski's fixed point theorem. Asserting the existence of fixed points under certain conditions, it is proved according to one of these two methods. In the impredicative method, the fixed points are characterized by a property (expressing extremality) using a quantification over a domain that includes the fixed point itself. In the iterative method, the fixed points are iteratively computed by using a transfinite induction. The impredicative method corresponds to a logical specification that is essentially not constructive 1 . As for the iterative method, it seems to be more constructive, in that it corresponds to an iteration. However, first, it assumes the machinery of ordinals and second, it therefore requires a specific computation for limit ordinals, the next value being then computed from an infinite set of preceding values.

Is there a proof method that not only is not impredicative, but also does not resort to ordinals? In this paper, we positively answer by proposing an alternative method, where fixed points are (inductively) proved in inference systems: this is a deductive method. It corresponds to a proof construction, using forward chaining for deduction rules, as used in logic programming, for instance in Datalog, a query language for deductive databases.

The paper is organized as follows. After recalling Tarski's theorem, the first section deals with inference systems, and their interpretations, either inductive or coinductive. In the second section, we introduce the deductive method, and apply it to different fixed point theorems: Tarski's theorem, its generalization to chain-complete posets and Bourbaki-Witt's theorem. Finally, we compare the deductive method with the iterative and impredicative methods.

Induction and Coinduction for Inference Systems

Generally speaking, following Aczel's classical presentation [START_REF] Aczel | An introduction to inductive definitions[END_REF], an inference system over a set U of judgments is a set of deduction rules. A deduction rule is an ordered pair (A, c), where A ⊆ U is the set of premises or antecedents and c ∈ U is the conclusion. A rule is usually written as follows:

A . c
Its intuitive interpretation is that the judgment c can be deduced from the set of judgments A.

Fixed Point Approach. The first way to assign a definitional meaning to an inference system is to consider the fixed points of the associated inference operator.

Indeed there exists a canonical Galois connection between the set of inference systems over U ordered by inclusion and the set of isotone (order-preserving) maps from 2 U to 2 U ordered point-wise. If Φ is an inference system over U , then the associated operator ϕ : 2 U → 2 U is defined as follows:

ϕ(S) = {c ∈ U | ∃ A ⊆ S . (A, c) ∈ Φ}.
The application of ϕ to S gives the conclusions that can be inferred in one step from S by using the inference rules: ϕ is thus called the inference operator associated to the system Φ. For instance, if S is the empty set, then ϕ(S) is the set of the axioms of the inference system, in other words the conclusions of the rules without premises. Conversely, given an isotone operator ϕ : 2 U → 2 U , the inference system containing all the rules (A, c), with c ∈ ϕ(A), and only these rules, belongs to the inverse image of ϕ: this is the greatest element of the inverse image of ϕ.

Let Φ be an inference system and ϕ its associated inference operator. Since the powerset 2 U is a complete lattice, by applying Tarski's fixed point theorem [10, p. 286], we obtain that the inference operator ϕ possesses both a least fixed point and a greatest fixed point.

We recall here Tarski's fixed point theorem, with two proofs following the impredicative and the iterative methods respectively.

Theorem 1 (Tarski). Let (E , ≤) be a complete lattice. Let η : E → E be an isotone map over E . Then η has a least fixed point lfp η and a greatest fixed point gfp η.

Impredicative method. Let S = {x ∈ E | η(x) ≤ x} and x in S. Since η is isotone, we have η2 (x) ≤ η(x), hence η(x) ∈ S. Since E is a complete lattice, S has a greatest lower bound, ∧ S. We have ∧ S ≤ x, hence η(∧ S) ≤ η(x) by isotony. Therefore η(∧ S) is a lower bound of S, hence η(∧ S) ≤ ∧ S, and ∧ S ∈ S. Then η(∧ S) ∈ S, hence ∧ S ≤ η(∧ S). Finally, ∧ S is a fixed point. Since all fixed point belongs to S, we can deduce the first equality, and by duality, the second one. This characterization of the least and greatest fixed points as the smallest η-closed 2 set and the greatest η-consistent3 set respectively can be found in original Tarski's paper [START_REF] Tarski | A lattice-theoretical fixpoint theorem and its applications[END_REF].

Iterative method. Let (∆ α (η)) α and (∇ α (η)) α be the sequences defined over ordinals as follows:

∆ α (η) = η( β |β <α ∆ β (η)) and ∇ α (η) = η( β |β <α ∇ β (η)).
By transfinite induction, we have for any ordinal α, ∆ α (η) ≤ η(∆ α (η)) and the sequence (∆ β (η)) β <α is increasing. Assume for contradiction that the sequence is strictly increasing. We get an injective map from the class of ordinals into a set, which is a contradiction, by Hartogs' lemma. Consider the smallest ordinal λ such that there exists β > λ satisfying ∆ λ (η) = ∆ β (η). By transfinite induction, we have that the sequence (∆ α (η)) α is stationary from rank λ . Moreover, ∆ λ (η) is a fixed point of η. Since by transfinite induction we have that any fixed point is an upper bound of the sequence (∆ α (η)) α , we deduce the first equality. By duality, we deduce the second one.

Grall

Deductive Method. In contrast with the fixed point approach, the deductive method starts from the proofs admissible in an inference system. These proofs are represented as trees, called proof trees. These are trees whose nodes are labeled with judgments in U and such that for all nodes n, the label c of n and the labels A of the sons of n correspond to an inference rule (A, c) in Φ. The conclusion of a proof is the label of its root node. A proof d is well-founded if it has no infinite branch; d is ill-founded otherwise. Note that an ill-founded proof is always infinite. A well-founded proof is finite if and only if it only uses rules with a finite set of premises.

In the deductive method, the inductive interpretation of the inference system Φ is the set ∆(Φ) of the conclusions of the well-founded proofs, while the coinductive interpretation is the set ∇(Φ) of the conclusions of all the proofs, ill-founded or well-founded. The following theorem shows that the interpretations defined using fixed points and using proofs coincide.

Theorem 2 (Inductive and coinductive interpretations). Let Φ be an inference system and ϕ the associated inference operator. Then:

lfp ϕ = ∆(Φ) and gfp ϕ = ∇(Φ).
Proof. It is easy to show that ∆(Φ) and ∇(Φ) satisfy ϕ(∆(Φ)) ⊆ ∆(Φ) and ∇(Φ) ⊆ ϕ(∇(Φ)) respectively. By Tarski's theorem, we deduce lfp ϕ ⊆ ∆(Φ) and ∇(Φ) ⊆ gfp ϕ.

Assume a set S satisfying ϕ(S) ⊆ S. An induction over well-founded proofs d shows that the conclusion of d is in S, hence ∆(Φ) ⊆ S. Since lfp ϕ satisfies the assumption, the inclusion ∆(Φ) ⊆ lfp ϕ follows.

Finally, assume a set S satisfying S ⊆ ϕ(S). For any judgment j in S, there exists a rule (K j , j) in Φ, where K j ⊆ S. We define a system of guarded recursive equations, with variables (x j ) j∈S .

x j = (x k ) k∈K j j
The solution σ of this system is such that for all j ∈ S, the derivation σ (x j ) is valid in Φ and proves j. Therefore, S ⊆ ∇(Φ). Since gfp ϕ satisfies the assumption, the inclusion gfp ϕ ⊆ ∇(Φ) follows.

The equality for the inductive case is proved by Aczel [START_REF] Aczel | An introduction to inductive definitions[END_REF]. The equality for the coinductive case is proved in the author's PhD dissertation [6, p. 77]. Starting from this theorem, Leroy and the author show in their article about coinductive operational semantics [8, Sect. 2] how the deductive method accounts for induction and coinduction in the proof assistant Coq: for a concrete example, see the proof of Lemma 5 [START_REF] Leroy | Coinductive big-step operational semantics[END_REF]Sect. 3], where the same proposition is proved following the impredicative method, the deductive method and in Coq.

Generalization of the Deductive Method

Theorem 2 asserts that the least and greatest fixed points of an isotone map over a powerset, a particular complete lattice, can also be defined as the inductive and coinductive interpretations of an inference system. We first generalize to any complete lattice, and then to more powerful fixed point theorems.

Tarski's Theorem Revisited. Given an isotone map η over a complete lattice (E , ≤), how can we define an inference system Φ over E , or equivalently an inference operator ϕ : 2 E → 2 E , whose inductive and coinductive interpretations produce the least and greatest fixed points of η?

A first attempt, defining ϕ(S) as the image of S with η, trivially fails, since the least fixed point would be the empty set. However, a well-known result [4, Th. I.5.3] allows a complete lattice to be embedded in its powerset. Indeed, let γ : 2 E → {≤ x | x ∈ E } be the closure operator from the powerset of E to the set {≤ x | x ∈ E } of principal order ideals defined as follows: γ(S) =≤ (∨ S) 4 . Let δ : {≤ x | x ∈ E } → 2 E be its adjoint embedding: δ (≤ x) =≤ x. Now, the isomorphism ι from E to {≤ x | x ∈ E } is defined as follows: ι(x) =≤ x. Finally, thanks to the embedding via a closure operator, we can associate to the map η the operator ϕ : 2 E → 2 E , equal to δ • ι • η • ι -1 • γ : we have ϕ(S) =≤ η(∨ S). It turns out that this operator has the intended properties with respect to fixed points. It suffices to use the associated inference system to get the following theorem.

Theorem 3 (Tarski revisited). Let (E , ≤) be a complete lattice. Let η : E → E be an isotone map over E . Consider the inference system Φ over E containing all the rules, and only these rules, of the following form: S s S ⊆ E , s ≤ η(∨ S) .

Then:

≤ (lfp η) = ∆(Φ) and ≤ (gfp η) = ∇(Φ).
Proof. It is easy to show that the inference operator ϕ associated to

Φ is equal to δ • ι • η • ι -1 • γ,
with the preceding notation. As ≤ (lfp η) = lfp ϕ and ≤ (gfp η) = gfp ϕ, we can conclude by applying Theorem 2.

Two Other Fixed Point Theorems. The deductive characterization of fixed points is still pertinent when we consider two other well-known fixed point theorems, where the assumptions for the poset and the map are weakened.

A poset is chain-complete if any chain, including the empty chain, has a least upper bound5 . Tarski's theorem can be extended to chain-complete posets, as shown for instance by Markowsky [9,Th. 9]. We again resort to the preceding inference system to characterize the least fixed point, with two restrictions: we only consider chains as premises and greatest judgments as conclusions.

Theorem 4 (Fixed point theorem for chain-complete poset). Let (E , ≤) be a chain-complete poset and η : E → E an isotone map. Let Φ be the inference system over E containing all the rules, and only these rules, of the following form: C

η(∨C) C ⊆ E ,C chain .
Then η has a least fixed point lfp η satisfying:

≤ (lfp η) = ≤ ∆(Φ).
Proof. We first show that ∆(Φ) is a chain, precisely that for any x 1 and any x 2 in ∆(Φ), we have x 1 ≤ x 2 or x 2 ≤ x 1 . We proceed by induction over well-founded proofs. Consider a well-founded proof ended with the rule (C 1 , η(∨C 1 ). Assume as inductive hypothesis that for any y 1 ∈ C 1 and any y 2 ∈ ∆(Φ), we have y 1 ≤ y 2 or y 2 ≤ y 1 . Let x 2 be in ∆(Φ). There exists a chain C 2 included in ∆(Φ) such that x 2 = η(∨C 2 ).

There are two cases. First, assume ∃ y 1 ∈ C 1 . ∀ y 2 ∈ C 2 . y 2 ≤ y 1 . We therefore have, for some y 1 in C 1 and for all y 2 in C 2 : y 2 ≤ y 1 , y 2 ≤ ∨C 1 and ∨C 2 ≤ ∨C 1 . We deduce by monotony x 2 ≤ η(∨C 1 ).

Proving Fixed Points

Grall

Second, assume ∀ y 1 ∈ C 1 . ∃ y 2 ∈ C 2 . ¬(y 2 ≤ y 1 ). We therefore have, for all y 1 in C 1 and some dependent point y 2 in C 2 : y 1 ≤ y 2 (inductive hypothesis), y 1 ≤ ∨C 2 and ∨C 1 ≤ ∨C 2 . We deduce by monotony η(∨C 1 ) ≤ x 2 .

Since ∆(Φ) is a chain, ∆(Φ), η(∨ ∆(Φ)) is a rule. We have η(∨ ∆(Φ)) ∈ ∆(Φ), hence η(∨ ∆(Φ)) ≤ ∨ ∆(Φ) and then η 2 (∨ ∆(Φ)) ≤ η(∨ ∆(Φ)) by monotony. Assume x is η-closed: η(x) ≤ x. It is easy to show by induction over well-founded proofs that x is an upper bound of ∆(Φ). We deduce that first ∨ ∆(Φ) ≤ η(∨ ∆(Φ)) and second ∨ ∆(Φ) is the least fixed point of η.

Finally ≤ (lfp η) = ≤ ∆(Φ) since ∨ ∆(Φ) ∈ ∆(Φ).
Actually, as shown by Markowsky [9, Th. 9], the preceding theorem can be considered as a corollary of Bourbaki-Witt's theorem [START_REF] Bourbaki | Théorie des ensembles : Fascicule de résultats[END_REF]. We also give a proof of this theorem by using the same inference system as in Theorem 4.

Theorem 5 (Bourbaki-Witt). Let E be a chain-complete poset and η : E → E an expansive6 map. Let Φ be the inference system over E containing all the rules, and only these rules, of the following form:

C η(∨C) C ⊆ E ,C chain .
Then η has a fixed point fp η satisfying:

≤ (fp η) = ≤ ∆(Φ).
Proof. We show that ∆(Φ) is a chain, which allows to conclude. Indeed, if ∆(Φ) is a chain, the inference rule

∆(Φ), η(∨ ∆(Φ)) belongs to Φ. From η(∨ ∆(Φ)) ∈ ∆(Φ), we deduce η(∨ ∆(Φ)) ≤ ∨ ∆(Φ). Since η is expansive, we deduce that ∨ ∆(Φ) is a fixpoint of η. Moreover, ∨ ∆(Φ) belongs to ∆(Φ). Therefore ≤ ∆(Φ) =≤ (∨ ∆(Φ)).
To show that ∆(Φ) is a chain, we introduce the notion of useful proofs. A well-founded proof, say ended by the rule (C, η(∨C)), is said useful if for any well-founded proof, say ended by the rule (D, η(∨ D)), we have:

(∨ D < ∨C) ⇒ (η(∨ D) ≤ ∨C).
Two crucial properties about usefulness can be asserted. First, for any useful proof ended by (C, η(∨C)) and any well-founded proof ended by (D, η(∨ D)), we have either η(∨C) = η(∨ D), η(∨C) ≤ ∨ D or η(∨ D) ≤ ∨C. Second, all well-founded proofs are useful. Thanks to these properties, it is easy to conclude that ∆(Φ) is a chain. Indeed, let x 1 and x 2 be in ∆(Φ). There exists two well-founded proofs, respectively ended by (C 1 , η(∨C 1 )) and (C 2 , η(∨C 2 )), such that x 1 = η(∨C 1 ) and x 2 = η(∨C 2 ). Since the former proof is useful, we have by applying the first property either

x 1 = x 2 , x 1 ≤ ∨C 2 or x 2 ≤ ∨C 1 . Since η is expansive, we deduce x 1 ≤ x 2 or x 2 ≤ x 1 .
Let us prove the two properties about usefulness. Suppose that a useful proof ends by the rule (C, η(∨C)). We prove by induction that for any wellfounded proof, say ended by (D, η(∨ D)), we have either

η(∨C) = η(∨ D), η(∨C) ≤ ∨ D or η(∨ D) ≤ ∨C.
Let us consider a proof concluded by the rule D, η(∨ D) and where the sub-proof of each premise y in D is ended by the rule D y , y . Assume the inductive hypothesis: for any y in D, we have either η(∨C) = y, η(∨C) ≤ ∨ D y or y ≤ ∨C. There are three cases. First, suppose that there exists y in D such that η(∨C) = y. We deduce η(∨C) ≤ ∨ D. Otherwise, second, suppose there exists y in D such that η(∨C) ≤ ∨ D y . Since η is expansive, we have η(∨C) ≤ y, hence η(∨C) ≤ ∨ D.

Proving Fixed Points Grall Otherwise, third, for all y in D, we have y ≤ ∨C. We deduce ∨ D ≤ ∨C. If ∨ D = ∨C, we deduce η(∨C) = η(∨ D). Otherwise, we have ∨ D < ∨C. Since the proof ended by (C, η(∨C)) is useful, we deduce η(∨ D) ≤ ∨C.

Let us prove that all well-founded proofs are useful. We proceed by induction over well-founded proofs. Let us consider a proof concluded by the rule C, η(∨C) and where the sub-proof of each premise x in C is concluded by the rule C x , x Assume the inductive hypothesis: for all x in C, the sub-proof with conclusion x is useful. Let us consider a well-founded proof ended by (D, η(∨ D)), and suppose ∨ D < ∨C. We have to show η(∨ D) ≤ ∨C. The inductive hypothesis and the first property give for any x in C either x = η(∨ D), x ≤ ∨ D or η(∨ D) ≤ ∨C x . We first notice that there exists x in C such that either x = η(∨ D) or η(∨ D) ≤ ∨C x . Otherwise, we would have for any x in C, x ≤ ∨ D, hence ∨C ≤ ∨ D, contradiction. There are two cases. First, suppose there exists x in C such that x = η(∨ D). We deduce η(∨ D) ≤ ∨C. Otherwise, second, there exists x in C such that η(∨ D) ≤ ∨C x . Since η is expansive, we deduce by transitivity η(∨ D) ≤ x, hence η(∨ D) ≤ ∨C.

The notion of useful proofs comes from the notion of extreme points, which is standard in the proof of the Bourbaki-Witt's theorem following the impredicative method, as given for instance in Lang's book [7, pp. 881-884].

Comparison of the Methods. Tarski's theorem and its two extensions to chain-complete posets are usually proved with the iterative method or the impredicative method, two methods that are not clearly connected. We now suggest that the deductive method allows these two methods to be connected.

First, to each inference system Φ used in Theorems 3, 4 and 5, we can associate an inference operator ϕ over 2 E . Thus, the inductive interpretation ∆(Φ) of Φ can also be defined as the smallest ϕ-closed set, as expressed in Theorems 1 and 2. It turns out that the definition of a ϕ-closed set is very akin to the definition of an admissible set, as found in the standard proof of Bourbaki-Witt's theorem following the impredicative method [7, pp. 881-884].

Second, the deductive method can be considered as an abstraction of the iterative method: it abstracts away from the iterative process involved in proof construction. The following proposition precisely describes their relationship in the case of Tarski's theorem. The height of a well-founded proof tree d is defined as follows: it is the least ordinal greater than the height of each immediate proof sub-tree of d. Given an inference system Φ over E and an ordinal α, we say that x ∈ E has complexity α if there is a well-founded proof of x with height less or equal to α. We denote by ∆ α (Φ) the set of all x with complexity α.

Proposition 1. Let (E , ≤) be a complete lattice and η : E → E an isotone map over E . Consider the transfinite sequence (∆ α (η)) α defined as follows:

∆ α (η) = η( β |β <α ∆ β (η)).
Consider the inference system Φ containing all the rules, and only these rules, of the following form:

S s S ⊆ E , s ≤ η(∨ S) .
Then, for any ordinal α:

≤ ∆ α (η) = ∆ α (Φ).
Proof. We proceed by transfinite induction for both inclusions.

Grall

Assume x ≤ ∆ α (η). Assume as inductive hypothesis that for any β < α, we have ≤ ∆ β (η) ⊆ ∆ β (Φ). Since {∆ β (η) | β < α}, x is a rule, we deduce that x belongs to ∆ α (Φ).

Assume x ∈ ∆ α (Φ). Assume as inductive hypothesis that for any β < α, we have ∆ β (Φ) ⊆≤ ∆ β (η). There exists a well-founded proof of x with height less or equal to α. This proof ends with a rule (S, x), with x ≤ η(∨ S). Each s in S belongs for some β < α to ∆ β (Φ), hence by the inductive hypothesis to ≤ ∆ β (η). We deduce ∨ S ≤ β |β <α ∆ β (η), then by monotony η(∨ S) ≤ ∆ α (η) and finally x ≤ ∆ α (η).

An analogous proposition holds for the two other fixed point theorems.

Conclusion

We have presented a method to characterize the fixed points described in fixed point theorems for complete lattices and chain-complete posets. The method is deductive: the fixed points are "proved" in some inference system. The techniques used in the proofs of these theorems is consistent with the method: they are based on induction over well-founded proofs. Finally, we have sketched a comparison between the deductive method and the two traditional methods, impredicative and iterative. In brief, given an inference system, the impredicative method essentially corresponds to the characterization à la Tarski using the inference operator associated to the inference system, whereas the iterative method corresponds to an iterative construction of the well-founded proofs in the inference system. The connection that we have suggested deserves a further exploration, which we reserve to future work.

We have already experienced the deductive method in a work about coinductive operational semantics [START_REF] Leroy | Coinductive big-step operational semantics[END_REF]. It turns out that the method is well-suited to the proof assistant Coq, which uses a calculus of inductive and coinductive constructions, an extension of type theory. The fixed points were expressed through inference systems and defined over powerset lattices. A motivation of the present work was to extend the method to fixed points defined in Coq over complete lattices or chain-complete posets. The iterative method resorts to ordinals, which are rarely used in Coq. Indeed, either they require to encode set theory, which is expensive, or they are implemented as constructive ordinals, which is restrictive. As for the impredicative method, it does not really fit with the calculus of inductive and coinductive constructions. Thus, the deductive method is a good candidate. A major problem to be solved is the use of classical logic. First, since the fixed points defined may have a non-terminating behavior, for instance when the fixed point is a function possibly divergent, adding classical logic axioms to the constructive logic of Coq is needed. In the same way, in the preceding proofs of the fixed point theorems, we have used the law of excluded middle. Second, as explained in the recent proposal of Bertot and Komendantsky [START_REF] Bertot | Fixed point semantics and partial recursion in Coq[END_REF], the addition of classical logic axioms should allow not only to reason about a fixed point with a terminating or non-terminating behavior, but also to extract a program computing the fixed point from the proof that the fixed point satisfies its specification, following the Curry-Howard correspondence.

We say that x is η-closed if η(x) ≤ x.

We say that x is η-consistent if x ≤ η(x).

Here, and in the following, given x ∈ E , we denote by ≤ x the principal order ideal {y ∈ E | y ≤ x}. Likewise, if X ⊆ E , we denote by ≤ X the union x∈X (≤ x).

A chain-complete poset has therefore a bottom element, ∨ / 0.

A map η : E → E is expansive (also inflationary, progressive) if any point is η-consistent: ∀ x ∈ E . x ≤ η(x).

Acknowledgments I would like to thank the anonymous reviewers of the workshop FICS 2010 for their feedback and for a correction (in Proposition 1).