Arthur Charguéraud
email: arthur.chargueraud@inria.fr

Pretty-Big-Step Semantics

In spite of the popularity of small-step semantics, big-step semantics remain used by many researchers. However, big-step semantics suffer from a serious duplication problem, which appears as soon as the semantics account for exceptions and/or divergence. In particular, many premises need to be copy-pasted across several evaluation rules. This duplication problem, which is particularly visible when scaling up to full-blown languages, results in formal definitions growing far bigger than necessary. Moreover, it leads to unsatisfactory redundancy in proofs. In this paper, we address the problem by introducing pretty-bigstep semantics. Pretty-big-step semantics preserve the spirit of big-step semantics, in the sense that terms are directly related to their results, but they eliminate the duplication associated with big-step semantics.

Introduction

There are two traditional approaches to formalizing the operational semantics of a programming language: small-step semantics [START_REF] Plotkin | A structural approach to operational semantics[END_REF], and big-step semantics [START_REF] Kahn | Natural semantics[END_REF]. In small-step semantics, the subterm in evaluation position is reduced step by step and these transitions are reflected at the top level. In big-step semantics, a term is directly related to its result, and the behavior of a term is expressed in terms of the behavior of its subterms. While provably equivalent, these two approaches are fundamentally different in terms of how evaluation rules are stated and how proofs are conducted.

This paper describes and proposes a solution to a severe limitation of big-step semantics: the fact that a number of rules and premises need to be duplicated in order to handle exceptions and divergence. In particular, this limitation typically discourages the use of big-step semantics in mechanized definitions of large-scale languages. Before trying to address this limitation of the big-step semantics, we may ask ourselves: Why should we care about big-step semantics? Why not just use small-step semantics all the time?

To find out whether big-step semantics are still being used, we opened up proceedings from recent programming language conferences. We counted the number of research papers making use of a big-step semantics. In ICFP '11, 5 papers were describing results based on a big-step semantics, out of 8 papers that had an operational semantics. In POPL '11, there were 7 out of 23. In ICFP'12, there were 5 out of 9. An immediate conclusion that we can draw from these rough statistics is that big-step is not dead.

A closer look at the papers involved reveals that the choice of the operational semantics usually depends on the topic covered by the paper. Papers on type systems nearly always use a small-step semantics to conduct a soundness proof in Wright and Felleisen's style [START_REF] Wright | A syntactic approach to type soundness[END_REF]. Papers describing a machine-level language typically use a small-step relation to describe transitions between pairs of machine configurations. Papers concerned with concurrent languages are also almost exclusively described using small-step semantics. Furthermore, a majority of the mechanized definitions of full-blown programming languages that have been developed in recent years were based on small-step semantics.

There are, however, topics for which the use of a big-step semantics appears to prevail. Cost semantics, which associate a cost to the evaluation of every expression, are mainly presented as big-step relations. Program logics often have soundness and completeness proofs that are easier to conduct with respect to a big-step relation. In particular, there are cases of completeness proofs, such as that developed in the author's thesis [START_REF] Charguéraud | Characteristic Formulae for Mechanized Program Verification[END_REF], that need to be conducted by induction over a big-step derivation; any attempt to build the completeness proof with respect to a small-step semantics amounts to re-proving on-the-fly the equivalence between small-step and big-step semantics. Moreover, there are compiler transformations that are easier to prove correct with respect to big-step semantics, in particular for transformations introducing so-called "administrative redexes", which typically clutter simulation diagrams based on small-step semantics.

Big-step semantics are also widely used in informal descriptions. For example, the reference manual of a programming language typically contain sentences of the form "to evaluate if e1 then e2 else e3, first evaluate e1; if the result is true, then evaluate e2; otherwise, evaluate e3." None of the many reference manuals that we have looked at contains a sentence of the form "if e1 takes a step to expression e1 then if e1 then e2 else e3 takes a step to if e1 then e2 else e3." Thus, we speculate that it would be easier to convince the standards committee in charge of a given programming language of the adequacy of a big-step formalization than to convince them of the adequacy of a small-step formalization.

Given that there are a number of important applications for which big-step semantics seem to have an edge on small-step semantics, any significant improvement to big-step semantics should be considered as a valuable contribution.

In this paper, we focus on a critical issue associated with big-step semantics: the amount of duplication involved in the statement of the evaluation rules. To illustrate the extent of the problem, consider a C-style for-loop of the form "for ( ; t 1 ; t 2 ) { t 3 }", that is, a for-loop where the initialization expression has already been executed. We use the notation "for t 1 t 2 t 3 " to describe such a loop. We next formalize its big-step semantics. For terminating executions, the evaluation judgment takes the form t /m1 ⇒ v /m2 , asserting that, in a store m 1 , the evaluation of t terminates on the value v in a store m 2 . The two rules at the top of Figure 1 describe the regular execution of a loop. When the loop condition t 1 evaluates to false, the loop terminates. Otherwise, if t 1 evaluates to true, we evaluate the body t 3 of the loop, and obtain the unit value, written tt. We then evaluate the stepping expression t 2 , and start over.

t1 /m 1 ⇒ false /m 2 for t1 t2 t3 /m 1 ⇒ tt /m 2 t1 /m 1 ⇒ true /m 2 t3 /m 2 ⇒ tt /m 3 t2 /m 3 ⇒ tt /m 4 for t1 t2 t3 /m 4 ⇒ tt /m 5 for t1 t2 t3 /m 1 ⇒ tt /m 5 t1 /m 1 ⇒ exn /m 2 for t1 t2 t3 /m 1 ⇒ exn /m 2 t1 /m 1 ⇒ true /m 2 t3 /m 2 ⇒ exn /m 3 for t1 t2 t3 /m 1 ⇒ exn /m 3 t1 /m 1 ⇒ true /m 2 t3 /m 2 ⇒ tt /m 3 t2 /m 3 ⇒ exn /m 4 for t1 t2 t3 /m 1 ⇒ exn /m 4 t1 /m 1 ⇒ true /m 2 t3 /m 2 ⇒ tt /m 3 t2 /m 3 ⇒ tt /m 4 for t1 t2 t3 /m 4 ⇒ exn /m 5 for t1 t2 t3 /m 1 ⇒ exn /m 5 t1 /m 1 ⇒ ∞ for t1 t2 t3 /m 1 ⇒ ∞ co t1 /m 1 ⇒ true /m 2 t3 /m 2 ⇒ ∞ for t1 t2 t3 /m 1 ⇒ ∞ co t1 /m 1 ⇒ true /m 2 t3 /m 2 ⇒ tt /m 3 t2 /m 3 ⇒ ∞ for t1 t2 t3 /m 1 ⇒ ∞ co t1 /m 1 ⇒ true /m 2 t3 /m 2 ⇒ tt /m 3 t2 /m 3 ⇒ tt /m 4 for t1 t2 t3 /m 4 ⇒ ∞ for t1 t2 t3 /m 1 ⇒ ∞ co
Fig. 1. Big-step rules for C loops of the form "for ( ; t1 ; t2) { t3 }", written "for t1 t2 t3".

The four rules at the bottom-left of Figure 1 describe the case of an exception being raised during the execution of the loop. These rules are expressed using another inductive judgment, written t /m1 ⇒ exn /m2 . They capture the fact that the exception may be triggered during the evaluation of any of the subexpressions, or during the subsequent iterations of the loop. The four rules at the bottom-right of Figure 1 describe the case of the loop diverging. These rules rely on a coinductive big-step judgment, written t /m ⇒ ∞ [START_REF] Cousot | Inductive definitions, semantics and abstract interpretation[END_REF][START_REF] Leroy | Coinductive big-step operational semantics[END_REF]. "Coinductive" means that a derivation tree for a judgment of the form t /m ⇒ ∞ may be infinite.

The amount of duplication in Figure 1 is overwhelming. There are two distinct sources of duplication. First, the rules for exceptions and the rules for divergence are extremely similar. Second, a number of evaluation premises are repeated across many of the rules. For example, even if we ignore the rules for divergence, the premise t 1/m 1 ⇒ true /m2 appears 4 times. Similarly, t 3/m 2 ⇒ tt /m3 appears 3 times and t 2/m 3 ⇒ tt /m4 appears 2 times. This pattern is quite typical in bigstep semantics for constructs with several subterms.

One may wonder whether the rules from Figure 1 can be factorized. The only obvious factorization consists of merging the regular evaluation judgment (t /m1 ⇒ v /m2 ) with the judgment for exceptions (t /m1 ⇒ exn /m2 ), using a single evaluation judgment that relates a term to a behavior, which consists of either a value or an exception. This factorization, quite standard in big-step semantics, here only saves one evaluation rule: the second rule from the top of Figure 1 would be merged with the rule at the bottom-left corner. It is, however, not easy to factorize the evaluation judgment with the divergence judgment, because one is inductive while the other is coinductive. Another trick sometimes used to reduce the amount of duplication is to define the semantics of a for-loop in terms of other language constructs, using the encoding "if t 1 then (t 3 ; t 2 ; for t 1 t 2 t 3 ) else tt". Yet, this approach does not support break and continue instructions, so it cannot be applied in general. In summary, just to define the semantics of for-loops, even if we merge the two inductive judgments, we need at least 9 evaluation rules with a total number of 21 evaluation premises. We will show how to achieve a much more concise definition, using only 6 rules with 7 evaluation premises.

With the pretty-big-step semantics introduced in this paper, we are able to eliminate the two sources of duplication associated with big-step definitions. First, we eliminate the duplication of premises. To that end, we break down evaluation rules into simpler rules, each of them evaluating at most one subterm. This transformation introduces a number of intermediate terms and increases the number of evaluation rules, but it eliminates the need for duplicating premises across several rules. Overall, the size of the formal definitions usually decreases.

Second, we set up the set of evaluation rules in such a way that it characterizes either terminating executions or diverging executions, depending on whether we consider an inductive or a coinductive interpretation for this set of rules. In contrast to Cousot and Cousot's bi-inductive semantics [START_REF] Cousot | Bi-inductive structural semantics[END_REF][START_REF] Cousot | Bi-inductive structural semantics[END_REF], which are based on the construction of a least fixed point of the set of evaluation rules with respect to a non-standard ordering that corresponds neither to induction nor coinduction, our definitions are based on the standard notions of induction and coinduction (as provided, e.g., by Coq).

Furthermore, we show that, when adding traces to the pretty-big-semantics, the coinductive judgment suffices to describe both terminating and diverging executions. Our definitions syntactically distinguish finite traces from infinite traces. This approach leads to rules that are, in our opinion, simpler to understand and easier to reason about than rules involving possibly-infinite traces (coinductive lists), as used by Nakata and Uustalu [START_REF] Nakata | Trace-based coinductive operational semantics for while[END_REF] and Danielsson [START_REF] Anders | Operational semantics using the partiality monad[END_REF].

In theory, the fact that we are able to capture the semantics through a single judgment means that we should be able to establish, through a single proof, that a program transformation correctly preserves both terminating and diverging behaviors. Unfortunately, the guard condition implemented in existing proof assistants such as Coq or Agda prevents us from conducting such reasoning. Workarounds are possible, but the encodings involved are so tedious that it would not be realistic to use them in practice. For this reason, we have to postpone the construction of proofs based on pretty-big-step trace semantics.

In this paper, we also investigate the formalization of type soundness proofs. Interestingly, the pretty-big-step semantics allows for a generic error rule that replaces all the error rules that are typically added manually to the semantics. This generic error rule is based on a progress judgment, whose definition can be derived in a simple and very systematic way from the set of evaluation rules.

To demonstrate the ability of the pretty-big-step to accommodate realistic languages, we formalized a large fragment of Caml Light. Compared with the bigstep semantics, the pretty-big-step semantics has a size reduced by about 40%. This paper is organized as follows. In §2, we explain how to turn a big-step semantics into its pretty-big-step counterpart. In §3, we discuss error rules and type soundness proofs. In §4, we show how to extend the semantics with traces. In §5, we explain how to handle more advanced language constructs and report on the formalization of core-Caml. We then discuss related work ( §6), and conclude ( §7). All the definitions and proofs from this paper have been formalized in Coq and put online at: http://arthur.chargueraud.org/research/2012/pretty.

2 Pretty-big-step semantics

Decomposition of big-step rules

We present the pretty-big-step semantics using the call-by-value λ-calculus. The grammar of values and terms are as follows.

v := int n | abs x t t := val v | var x | app t t
Thereafter, we leave the constructor val implicit, writing simply v instead of val v whenever a term is expected. (In Coq, we register val as a coercion.) We recall the definition of the standard big-step judgment, which is written

t ⇒ v. v ⇒ v t 1 ⇒ abs x t t 2 ⇒ v [x → v] t ⇒ v app t 1 t 2 ⇒ v
The rules of the pretty-big-step semantics are obtained by decomposing the rules above into more atomic rules that consider the evaluation of at most one subterm at a time. A first attempt at such a decomposition consists of replacing the evaluation rule for applications with the following three rules.

t 1 ⇒ v 1 app v 1 t 2 ⇒ v app t 1 t 2 ⇒ v t 2 ⇒ v 2 app v 1 v 2 ⇒ v app v 1 t 2 ⇒ v [x → v] t ⇒ v app (abs x t) v ⇒ v
These rules, without further constraints, suffer from an overlapping problem. For example, consider the term app v 1 t 2 . This term is subject to the application of the second rule, which evaluates t 2 . However, it is also subject to application of the first rule, whose first premise would reduce v 1 to itself and whose second premise would be identical to the conclusion of the rule. The fact that two different rules can be applied to a same term means that the evaluation judgment is not syntax-directed and thus not very convenient to work with. Even worse, the fact that an evaluation rule can be applied without making progress is problematic when considering a coinductive interpretation of the evaluation rules; typically, one could prove, by applying the first reduction rule infinitely many times, that any term of the form app v 1 t 2 diverges.

Cousot and Cousot [START_REF] Cousot | Bi-inductive structural semantics[END_REF][START_REF] Cousot | Bi-inductive structural semantics[END_REF], who use a similar decomposition of the big-step rules as shown above, prevent the overlapping of the rules by adding sideconditions. For example, the evaluation rule that reduces app t 1 t 2 has a sidecondition enforcing t 1 to not be already a value. However, such side-conditions are numerous and they need to be discharged in formal proofs.

Instead of using side-conditions, we ensure that the three evaluation rules introduced above are always applied one after the other by introducing intermediate terms, whose grammar is shown below. Observe that intermediate terms are not defined as an extension of the grammar of regular terms, but as a new grammar that embeds that of regular terms. This presentation avoids polluting the syntax of source terms with purely-semantical entities.

e := trm t | app1 v t | app2 v v
We extend the evaluation judgment to intermediate terms, defining an inductive judgment of the form e ⇓ v. In the particular case where e describes a regular term, the judgment takes the form (trm t) ⇓ v. Thereafter, we leave the constructor trm implicit and thus simply write t ⇓ v. The predicate e ⇓ v is defined inductively by the rules shown below. The evaluation of an application app t 1 t 2 takes three step. First, we reduce t 1 into v 1 and obtain the term app1 v 1 t 2 . Second, we reduce t 2 into v 2 and obtain the term app2 v 1 v 2 . Third, assuming v 1 to be of the form abs x t, we proceed to the β-reduction and evaluate

[x → v] t in order to obtain some final result v . v ⇓ v t 1 ⇓ v 1 app1 v 1 t 2 ⇓ v app t 1 t 2 ⇓ v t 2 ⇓ v 2 app2 v 1 v 2 ⇓ v app1 v 1 t 2 ⇓ v [x → v] t ⇓ v app2 (abs x t) v ⇓ v
The definitions above provide an adequate reformulation of the big-step semantics by which complex rules have been decomposed into a larger number of more elementary rules. This decomposition avoids the duplication of premises when adding support for exceptions and divergence. Observe that the intermediate terms introduced in the process correspond to the intermediate states of an interpreter. For example, the form app1 v 1 t 2 corresponds to the state of the interpreter after the evaluation of the first let-binding in the code

"let v 1 = eval t 1 in let v 2 = eval t 2 in let (abs x t) = v 1 in eval ([x → v 2 ] t)".

Treatment of exceptions

We now extend the source language with value-carrying exceptions and exception handlers. The term raise t builds an exception and throws it. The term try t 1 t 2 is an exception handler with body t 1 and handler t 2 . Its semantics is as follows. If t 1 produces a regular value, then try t 1 t 2 returns this value. However, if t 1 raises an exception carrying a value v 1 , then try t 1 t 2 reduces to app t 2 v 1 .

To describe the fact that a term can produce either a regular value or an exception carrying a value, the evaluation judgment is generalized to the form e ⇓ b, where b denotes a behavior, built according to the grammar below.

b := ret v | exn v
Because we generalize the form of the judgment, we also need to generalize the form of the intermediate terms. For example, consider the evaluation of an application app t 1 t 2 . First, we evaluate t 1 into a behavior b 1 . We then obtain the intermediate term app1 b 1 t 2 . To evaluate this later term, we need to distinguish two cases. On the one hand, if b 1 is of the form ret v 1 , then we should evaluate the second branch t 2 . On the other hand, if b 1 is of the form exn v, then we should directly propagate exn v. The updated grammar of intermediate terms, augmented with intermediate forms for raise and try, is as follows.

e := trm t | app1 b t | app2 v b | raise1 b | try1 b t
The definition of e ⇓ b follows a similar pattern as previously. It now also includes rules for propagating exceptions. For example, app1 (exn v) t evaluates to exn v. Moreover, the definition includes rules for evaluating raise and try. For example, to evaluate try t 1 t 2 , we first evaluate t 1 into a behavior b 1 , and then we evaluate the term try1 b 1 t 2 . In the rules shown below, the constructor ret is left implicit.

v ⇓ v t1 ⇓ b1 app1 b1 t2 ⇓ b app t1 t2 ⇓ b app1 (exn v) t ⇓ exn v t2 ⇓ b2 app2 v1 b2 ⇓ b app1 v1 t2 ⇓ b app2 v (exn v) ⇓ exn v [x → v] t ⇓ b app2 (abs x t) v ⇓ b t ⇓ b1 raise1 b1 ⇓ b raise t ⇓ b raise1 v ⇓ exn v raise1 (exn v) ⇓ exn v t1 ⇓ b1 try1 b1 t2 ⇓ b try t1 t2 ⇓ b try1 v t ⇓ v app t v ⇓ b try1 (exn v) t ⇓ b

Treatment of divergence

The above set of rules only describes terminating evaluations. To specify diverging evaluations, we are going to generalize the grammar of behaviors and to consider a coinductive interpretation of the same set of rules as that describing terminating evaluations. First, we introduce the notion of outcome: the outcome of an execution is either to terminate on a behavior b (i.e., to return a value or an exception), or to diverge. We explicitly materialize the divergence outcome with a constant, called div. An outcome, written o, is thus described as follows: o := ter b | div.

We update accordingly the grammar of intermediate terms. For example, consider the evaluation of an application app t 1 t 2 . First, we evaluate t 1 into some outcome o 1 (a value, an exception, or divergence). We then consider the term app1 o 1 t 2 , whose evaluation depends on o 1 . If o 1 describes a value v 1 , we can continue as usual by evaluating t 2 . However, if o 1 describes an exception or the constant div, then the term app1 o 1 t 2 directly propagates the outcome o 1 . To capture the fact that app1 o 1 t 2 returns o 1 both when o 1 describes divergence or an exception, we use an auxiliary predicate, called abort. The predicate abort o 1 asserts that o 1 "breaks the normal control flow" in the sense that o 1 is either of the form exn v or is equal to div. We are then able to factorize the rules propagating exceptions and divergence into a single abort rule, as shown below.

b := ret v | exn v o := ter b | div e := trm t | app1 o t | app2 v o | raise1 o | try1 o t abort (exn v) abort div v ⇓ v t1 ⇓ o1 app1 o1 t2 ⇓ o app t1 t2 ⇓ o abort o app1 o t ⇓ o t2 ⇓ o2 app2 v1 o2 ⇓ o app1 v1 t2 ⇓ o abort o app2 v o ⇓ o [x → v] t ⇓ o app2 (abs x t) v ⇓ o t ⇓ o1 raise1 o1 ⇓ o raise t ⇓ o abort o raise1 o ⇓ o raise1 v ⇓ exn v t1 ⇓ o1 try1 o1 t2 ⇓ o try t1 t2 ⇓ o try1 v t ⇓ v app t v ⇓ o try1 (exn v) t ⇓ o abort o ∀v. o = exn v try1 o t ⇓ o
abort o 1 app1 o 1 t 2 ⇓ o 1
For describing terminating evaluations, we use an inductive judgment of the form e ⇓ o. The particular form e ⇓ ter b, simply written e ⇓ b, corresponds to the same evaluation judgment as that defined previously. For describing diverging evaluations, we use a coevaluation judgment, written e ⇓ co o, which is defined by taking a coinductive interpretation of the same set of rules as that defining the inductive judgment e ⇓ o. The particular form e ⇓ co div asserts that the execution of e diverges.

The complete set of rules defining both e ⇓ o and e ⇓ co o appears in Figure 2. One novelty is the last rule, which is used to propagate divergence out of exception handlers. The rule captures the fact that try1 div t produces the outcome div, but it is stated in a potentially more general way that will be useful when adding errors as a new kind of behavior. Remark: in Coq, we currently need to copy-paste all the rules in order to build one inductive definition and one coinductive definition, however it would be easy to implement a Coq plug-in to automatically generate the coinductive definition from the inductive one.

Properties of the judgments

While we are ultimately only interested in the forms e ⇓ b and e ⇓ co div, our definitions syntactically allow for the forms e ⇓ div and e ⇓ co b. It is worth clarifying their interpretation. For the former, the situation is quite simple: the form e ⇓ div is derivable only when e is an intermediate term that carries a div. In particular, t ⇓ div is never derivable. Lemma 1. For any term t, t ⇓ div → False.

The interpretation of the form e ⇓ co b is more subtle. On the one hand, the coinductive judgment contains the inductive one, because any finite derivation is also a potentially-infinite derivation. It is trivial to prove the following lemma. On the other hand, due to coinduction, it is sometimes possible to derive e ⇓ co b even when e diverges. For example, consider ω = app δ δ, where δ = abs x (app x x); one can prove by coinduction that, for any outcome o, the relation ω ⇓ co o holds. Nevertheless, the coevaluation judgment is relatively well-behaved, in the sense that if e ⇓ co o holds, then either e terminates on some behavior b, or e diverges. This property is formalized in the next lemma. We have proved in Coq that the pretty-big-step semantics shown in Figure 2 yields an operational semantics adequate with respect to the standard big-step evaluation judgment for terminating programs (t ⇒ b) and with respect to the coinductive big-step evaluation judgment (t ⇒ ∞ ) introduced by Leroy and Grall [START_REF] Leroy | Coinductive big-step operational semantics[END_REF][START_REF] Leroy | Coinductive big-step operational semantics[END_REF] for diverging programs. (The proof requires the excluded middle.)

Theorem 1 (Equivalence with big-step semantics). For any term t, and for any behavior b (describing either a value or an exception), t ⇓ b if and only if t ⇒ b and t ⇓ co div if and only if t ⇒ ∞ .

All the results presented so far can be generalized to non-deterministic semantics. In the particular case of a deterministic semantics, such as our call-by-value λ-calculus, we can express the determinacy property as follows.

Lemma 4 (Determinacy).

∀eo

1 o 2 . e ⇓ o 1 ∧ e ⇓ co o 2 → o 1 = o 2
As corollaries, we can prove that if a given term e evaluates to a behavior o 1 , then it cannot evaluate to a different behavior o 2 and it cannot diverge.

3 Error rules and type soundness proofs

Explicit error rules

When considering a deterministic language, one can express the type soundness theorem in the form "if a term is well-typed, then it either terminates or diverges". However, for a non-deterministic language, such a statement does not ensure soundness, because a term could execute safely in some execution but get stuck in other executions. For a non-deterministic big-step semantics, the traditional approach to proving type soundness consists of adding explicit error rules to the semantics, and then proving a theorem of the form "if a term is well-typed, then it cannot evaluate to an error".

Adding error rules to a pretty-big-step semantics turns out to be much easier than for a big-step semantics, because we are able to reuse the abort rules for propagating errors to the top level. To describe stuck terms in our language, it suffices to add a behavior err, to state that it satisfies the predicate abort, and to add two error rules, one for variables and one for stuck applications.

The generic error rule

A classic problem with the introduction of explicit error rules for proving type soundness is that the theorem can be compromised if an error rule is missing. Indeed, if we remove a few error rules, then it makes it easier to prove that "if a term is well-typed, then it cannot evaluate to an error". So, the omission of an error rule may hide a flaw in the type system that we want to prove sound. For a language as simple as the λ-calculus, the error rules are few. However, for a more realistic language, they can be numerous. In such a case, it becomes fairly easy to forget a rule and thereby compromise the adequacy of the type soundness theorem. One could hope to be able to prove (say, in Coq) that a semantics is not missing any error rules. Yet, as far as we know, there is no way of formally stating this property. (The formulation "every term either evaluates to a value or to an error, or diverges" is not appropriate, due to non-determinism.)

In what follows, we explain how a pretty-big-step semantics can be equipped with a generic error rule, which directly captures the intuition that "a term should evaluate to an error if no other evaluation rule can be applied". Remark: this intuition was at the source of the work by Gunter and Rémy [START_REF] Gunter | A proof-theoretic assessment of runtime type errors[END_REF] on partial proof semantics, which consists of a specialized proof theory that allows describing derivation trees with exactly one unproved leaf; our approach at handling error rules in a generic manner can be viewed as a realization of Gunter and Rémy's idea of partial proofs within a standard proof theory.

The generic error rule is defined in terms of the progress judgment, written e ↓, which asserts that there exists at least one pretty-big-step evaluation rule whose conclusion matches the term e. The rules defining the progress judgment can be derived in a systematic manner from the pretty-big-step evaluation rules, as described next. An evaluation rule has a conclusion of the form e ⇓ o, a number of evaluation premises and some other premises. The corresponding progress rule is obtained by changing the conclusion to e ↓ (i.e., dropping the outcome o) and by removing all the evaluation premises. The progress judgment associated with the semantics described in Figure 2 is defined in Figure 3.

Then, the generic error rule, shown below, simply asserts that "if a term e cannot make progress (e ↓ is false) then e should evaluate to an error".

¬ (e ↓) e ⇓ err v ↓ app t1 t2 ↓ abort o app1 o t2 ↓ app1 v1 t2 ↓ abort o app2 v o ↓ app2 (abs x t) v ↓ raise t ↓ abort o raise1 o ↓ raise1 v ↓ try t1 t2 ↓ try1 v t ↓ try1 (exn v) t ↓ abort o ∀v. o = exn v try1 o t ↓ Fig. 3. Progress judgment.
We have proved in Coq that using the generic error rule yields evaluation and coevaluation judgments that are equivalent to those obtained with the traditional approach to introducing explicit error rules.

There are two main benefits to using the generic error rule. First, deriving the progress rules from the evaluation rules is easier than deriving explicit error rules. Indeed, instead of having to find out which rules are needed to complete the semantics, we can apply to each of the evaluation rules a very systematic process -so systematic that we believe it could be automated by a Coq plug-in. Second, forgetting a progress rule does not compromise the type soundness theorem. Indeed, omitting a progress rule makes it easier to prove that a term evaluates to an error, and therefore makes it harder (if not impossible) to prove the statement of the type soundness theorem. To be fair, it should be acknowledged that adding arbitrary progress rules can compromise type soundness. That said, we believe that it is much more unlikely for a researcher to add arbitrary progress rules than to omit a few legitimate rules.

Type soundness proofs

To give an example of a type soundness proof, we equip our λ-calculus with simple types. For simplicity, we enforce exceptions to carry only values of type int. A source program can be typed using the standard typing judgment, of the form E t : T . We write t : T when the typing context E is empty. The typing rules for terms are standard, so we do not show them.

To prove type soundness, we first need to consider a typing judgment for intermediate terms, written e : T , and another one for outcomes, written o : T . The proposition o : T asserts that the outcome o describes either a value of type T , or an exception carrying a value of type int, or the outcome div. Note that err, the error outcome, is never well-typed. The rules defining the new typing judgments appear in Figure 4. The type soundness theorem states that "if a closed term is well-typed, then it cannot evaluate to an error".

Theorem 2 (Type soundness). For any t and T , t : T → ¬ t ⇓ err. and observe that err : T is equivalent to False. There are two particularly interesting cases in the proof. First, when the evaluation rule is an abort rule, we need to exploit the fact that a well-typed outcome satisfying abort admits any type. Formally: ( o : T ) ∧ (abort o) → ( o : T ). Second, when the evaluation rule is the error rule, we need to establish that if a term is well-typed then it must satisfy the progress judgment. Formally: ( e : T ) (e ↓).

All the other proof cases are straightforward. Compared with the big-step semantics, the pretty-big-step semantics leads to a type soundness proof that involves a slightly larger number of cases, however these proof cases are typically simpler, due to the fact that the evaluation rules have at most two premises. In practice, we have found that having simpler proof cases makes the proofs easier to complete and easier to automate.

In summary, the pretty-big-step semantics, by reusing its abort rules, reduces the amount of work needed for adding error behaviors. It also allows for a generic error rule that makes it faster and less error-prone to add all the error rules. Moreover, even though it requires additional typing rules for intermediate terms, it leads to proofs that involve cases that are simpler and easier to automate.

Traces

Traces are typically used to record the interactions of a program with its environment, for example i/o operations. In what follows, we show how to extend the pretty-big-step evaluation rules with traces. A trace describes a sequence of effects. Here, an effect, written α, describes a read operation (in n), or a write operation (out n), or the absence of an operation ( ). We use the effect to make the evaluation rules productive with respect to traces. Productivity is needed in particular to ensure that a diverging program that does not perform any i/o cannot be associated with arbitrary traces. A trace can be finite or infinite. A finite trace, written τ , consists of a list of effects. An infinite trace, written σ, consists of a stream of effects (i.e., an infinite list). The outcome of a program can be either "termination on a value with a finite trace" or "divergence with an infinite trace". These definitions are summarized below.

α := | in n | out n o := ter τ b | div σ (τ list of α, and σ stream of α)
In several evaluation rules, we need to append a finite trace to the head of a finite or an infinite trace. We write τ •τ and τ •σ the corresponding concatenation With traces, the inductive interpretation of the rules is no longer needed because, thanks to the productivity of the rules with respect to the trace, a diverging expression cannot coevaluate to a terminating behavior. We have: Lemma 5. For any finite trace τ , (e ⇓ co ter τ v) ⇔ (e ⇓ ter τ v).

abort (ter τ (exn v)) abort (div σ) v ⇓ ter [ ] v t1 ⇓ o1 app1 o1 t2 ⇓ o app t1 t2 ⇓ [ ] • o abort o app1 o t ⇓ [ ] • o t2 ⇓ o2 app2 v1 o2 ⇓ o app1 (ter τ v1) t2 ⇓ [ ] • τ • o abort o app2 v o ⇓ [ ] • o [x → v] t ⇓ o app2 (abs x t) (ter τ v) ⇓ [ ] • τ • o t ⇓ o1 read1 o1 ⇓ o read t ⇓ [ • o abort o read1 o ⇓ [ ] • o read1 (ter τ tt) ⇓ ter ([ ] • τ • [in n]) n t ⇓ o1 write1 o1 ⇓ o write t ⇓ [ ] • o abort o write1 o ⇓ [ ] • o write1 (ter τ n) ⇓ ter ([ ] • τ • [out n]) tt
An important consequence of Lemma 5 is that, when the semantics includes traces, we do not need the inductive judgment (e ⇓ o) anymore. In theory, all our reasoning can be conducted using solely the coevaluation judgment. In particular, we should be able to prove a program transformation correct with respect to both terminating and diverging programs through a single coinductive proof. In practice, though, coinductive reasoning in proof assistants such as Coq or Agda remains problematic because they only accept statement of theorems whose conclusion is a coinductive judgment and where all applications of the coinduction hypothesis are guarded by constructors. As soon as we fall out of this basic pattern, we need to resort to heavy encodings in order to transform the statement and the proof in the appropriate form.

The verification of program transformations, one important applications of formal semantics, almost systematically departs from the basic pattern. Their correctness proof typically relies on a simulation diagram establishing that any behavior exhibited by the compiled code is indeed a behavior of the original code. Consider for example a source-to-source translation, written • . Its correctness would typically be captured by a statement of the form

( t ⇓ co o) → ∃o . (o ≈ o) ∧ (t ⇓ co o ),
n • [α] • o ≈ m • [α] • o .
) Intuitively, such a statement could be established by coinduction, performing a case analysis on the derivation of t ⇓ co o and, in each case, picking the right o to build the proof of t ⇓ co o .

Unfortunately, this form of reasoning currently cannot be mechanized in Coq because the conclusion of the statement is not just a coinductive judgment; indeed, the conclusion starts with an existential quantifier and a conjunction. One possible work-around consists in defining o as a function of o and t (this definition is non-constructive), and then proving o ≈ o and t ⇓ co o , through two independent proofs. These two proofs have a chance of satisfying the guard condition because they conclude on coinductive judgments. Yet, overall, the workaround described here is extremely unpleasant. First, defining the function that produces o amounts to building the core of a proof term by hand. Second, the process requires one to go three times over the structure of the intended proof: once for the function definition, and once for each of the two coinductive proofs.

We must therefore acknowledge that, with the support for coinduction currently provided by Coq, mechanizing proofs based on pretty-big-step trace semantics appears to be unrealistic in practice. Nevertheless, we hope that further developments of proof assistants could allow us to conduct the intended reasoning without resorting to painful encodings, either by automating the generation of the encoding, or by somehow relaxing the guard condition. We should then be able to reason about both terminating and diverging programs in a single pass.

Scaling up to real languages

So far, we have only considered a toy λ-calculus with exceptions. In this section, we explain how to set up pretty-big-step rules for more advanced programming language constructs, such as effectful operations, tuples of arbitrary arity, and C-style for loops. We also show how to handle constructs for which the order of evaluation of the subterms needs to remain deliberately unspecified.

Factorization of the abort evaluation rules

The pretty-big-step semantics of a realistic language may involve a fair number of intermediate terms. For each intermediate term, we typically need to introduce an abort rule, i.e., a rule with a premise of the form abort o, to propagate exceptions, divergence and errors. Fortunately, it is possible to factorize all the abort rules using the generic abort rule. This rule formalizes the following intuition: if an intermediate term e is not an exception handler and if one of its arguments is an outcome o that satisfies the predicate abort, then e should directly evaluate to o. The definition of the generic abort rule relies on an auxiliary function, called getout. It is defined in such a way that getout e returns the outcome contained in e (there is at most one), except for exception handlers, which are treated specially. Formally:

getout (app1 o t) ≡ Some o getout (app2 v o) ≡ Some o getout (raise1 o) ≡ Some o getout (trm t) ≡ None getout (try1 o t) ≡ None
The generic abort rule, shown below, replaces the three abort rules from Figure 2.

getout e = Some o abort o e ⇓ o
Throughout the rest of this section, when we introduce new intermediate terms, we assume the definition of getout to be extended accordingly.

Side effects

We now extend the source language with side effects. When the evaluation of a term terminates, it produces not just a value or an exception, but also an updated memory store. We therefore update the grammar of outcomes as follows.

o := ter m b | div
The pretty-big-step evaluation judgment now takes the form e /m ⇓ o, asserting that the evaluation of the term e in the store m has o for outcome. In particular, the proposition t /m ⇓ ter m b corresponds to the traditional big-step judgment t /m ⇒ b /m and, similarly, the proposition t /m ⇓ div corresponds to t /m ⇒ ∞ . The evaluation rules are extended so as to take memory stores into account. For example, the first rules for reducing applications are as shown below. Observe that the intermediate term app1 o 1 t 2 is evaluated in the store m in which t 1 was evaluated, and not yet in the store produced by t 1 . Indeed, at this point, we do not yet know whether the evaluation of t 1 terminates or diverges. In the particular case where t 1 terminates, the store produced by the evaluation of t 1 can be pulled out of the outcome o 1 and used for the evaluation of t 2 .

t 1 /m ⇓ o 1 app1 o 1 t 2 /m ⇓ o app t 1 t 2 /m ⇓ o t 2 /m ⇓ o 2 app2 v 1 o 2 /m ⇓ o app1 (ter m v 1 ) t 2 /m ⇓ o
We end this section with an example of a rule that modifies the store. Consider a term ref t 1 . Its evaluation goes through an intermediate term ref1 o 1 . If o 1 is a value, then a memory cell is allocated at a fresh location. The updated store is then returned together with the address of the new memory cell.

t 1 /m ⇓ o 1 ref1 o 1 /m ⇓ o ref t 1 /m ⇓ o l / ∈ dom(m) ref1 (ter m v) /m ⇓ ter (m[l → v]) l
Other rules accessing and updating the memory store follow a similar pattern.

C-style for loops

We now come back to the example of C-style for loops described in the introduction, revisiting the evaluation rules from Figure 1 using a pretty-big-step semantics. We introduce a single intermediate term, written "for i o t 1 t 2 t 3 ", where i ∈ {1, 2, 3}. The pretty-big-step evaluation rules, shown below, are significantly more concise than their big-step counterpart. Note that we included an abort rule, even though it would typically be covered by the generic abort rule ( §5.1).

List of subterms

Consider a tuple expression, written tuple t, where t denotes a list of terms of arbitrary length, and assume a left-to-right evaluation order. The semantics needs to describe the fact that if one of the subterms of the tuple raises an exception or diverge, then the remaining subterms should not be evaluated. In what follows, we describe a technique for evaluating an ordered list of subterms in a way that is not specific to tuples, so that we are able to reuse the same rules for reducing other language constructs that involve lists of subterms (e.g., records).

We introduce an intermediate term, written list1 t v K, where v represents the list of values that have already been produced, t represents the list of terms remaining to be evaluated, and K denotes the continuation describing what term to transition to once all the subterms have been evaluated. Here, K is a logical function that takes a list of values as arguments and produces an intermediate term. In practice, K is usually a partially-applied constructor.

To evaluate tuple t, we evaluate list1 t nil (tuple1), where the continuation tuple1 indicates that, when we get the list of values v describing the results of the terms t, we should evaluate the term tuple1 v. This latter term will immediately evaluate to the value vtuple v. The corresponding evaluation rules are:

list1 t nil (tuple1) /m ⇓ o tuple t /m ⇓ o tuple1 v /m ⇓ ter m (vtuple v)
It remains to describe the rules involved in the evaluation of list1 t v K. If t is empty, we apply (in the logic) the continuation K to v and obtain the term from which to continue the evaluation. Otherwise, t is of the form t 1 :: t. In this case, we evaluate the head term t 1 , obtaining some outcome o, and we then evaluate the term list2 o t v K. If o corresponds to a value, we can save this value at the tail of the list v and continue. Otherwise, we can apply the generic abort rule to propagate this outcome directly, skipping the evaluation of the remaining terms t. The corresponding evaluation rules are shown below.

(K v) /m ⇓ o list1 nil v K /m ⇓ o t 1 /m ⇓ o 1 list2 o 1 t v K /m ⇓ o list1 (t 1 :: t) v K /m ⇓ o list1 t (v + + [v 1 ]) K /m ⇓ o list2 (ter m v 1 ) t v K /m ⇓ o

Unspecified order of evaluation

Some programming languages choose to deliberately not specify the order of evaluation of the subterms of particular language constructs. For example, Caml does not specify the order of evaluation of the arguments of a function call. In what follows, we explain how to describe the semantics of a list of subterms without specifying the order of evaluation. We use a list r whose items are either values or unevaluated terms. Formally, r := Trm t | Val v, and r := list r.

We start from an intermediate term ulist1 t K, where, as previously, t denotes the list of subterms and K is a logical function that denotes the continuation. To evaluate ulist1 t K, we evaluate another intermediate term, ulist2 r K, where r is obtained by mapping the constructor Trm to all the elements of t. Then, we pick any unevaluated term from the list r and evaluate it. We repeat this process until either the evaluation of one of the term diverges or produces an exception, or until all the items in r are values. The rules, shown below, involve an intermediate term of the form ulist3 r 1 o r 2 K, where o denotes the outcome that has just been produced, and where r 1 and r 2 denote the prefix and the suffix of r, respectively.

ulist2 (map (Trm) t) K /m ⇓ o ulist1 t K /m ⇓ o t 1 /m ⇓ o 1 ulist3 r 1 o 1 r 2 K /m ⇓ o ulist2 (r 1 + + [Trm t 1 ] + + r 2 ) K /m ⇓ o ulist2 (r 1 + + [Val v 1 ] + + r 2 ) K /m ⇓ o ulist3 r 1 (ter m v 1 ) r 2 K /m ⇓ o (K v) /m ⇓ o ulist2 (map (Val) v) K /m ⇓ o

Formalization of core-Caml

To assess the ability of the pretty-big-step semantics to scale up to a realistic programming language, we formalized the semantics of core-Caml, both in bigstep and in pretty-big-step style. By core-Caml, we refer to the subset of Caml Light made of booleans, integers, tuples, algebraic data types, mutable records, boolean operators (lazy and, lazy or, negation), integer operators (negation, addition, subtraction, multiplication, division), comparison operator, functions, recursive functions, applications, sequences, let-bindings, conditionals (with optional else branch), for loops and while loops, pattern matching (with nested patterns, as patterns, or patterns, and when clauses), raise construct, try-with construct with pattern matching, and assertions. (The features missing from Caml Light are: floats, mutual recursion, recursive values, with construct for records, and arrays. Objects and modules are not covered either.)

Translating the big-step semantics into a pretty-big-step one following the ideas described in this paper was straightforward and took little time. Apart from adapting the rules, the only extra work required consisted of the definition of outcomes and of the abort predicate (4 lines), the definition of the 28 intermediate terms, and the definition of the auxiliary function getout using a simple pattern matching with 22 cases (one case per intermediate term carrying an outcome).

The table shown below quantifies the improvement. It reports on the number of evaluation rules, the number of evaluation premises, and the number of tokens (excluding head quantified variables, which are typically omitted in paper definitions). It shows that switching to the pretty-big-step semantics reduced the number of the evaluation rules by 38%, reduced the total number of evaluation premises by more than a factor of 2, and reduced the total size of the evaluation rules (as counted by the number of tokens) by 40%. Cousot and Cousot [START_REF] Cousot | Inductive definitions, semantics and abstract interpretation[END_REF] proposed a coinductive big-step characterization of divergence for λ-terms. Leroy and Grall [START_REF] Leroy | Coinductive big-step operational semantics[END_REF][START_REF] Leroy | Coinductive big-step operational semantics[END_REF] showed how to represent coinductive big-step semantics in a theorem prover such as Coq, and used this semantics to prove that nontrivial program transformations preserve diverging behaviors. They justify the need to introduce separate coinductive rules by observing that naively taking the coinductive interpretation of the standard evaluation rules yields a coevaluation judgment that does not properly characterizes diverging terms. Indeed, there exist terms that diverge but do not coevaluate. Leroy and Grall also explained how to extend their semantics with traces, using two judgments: t ⇒ v/τ asserts that the execution of t produces the value v and a finite trace τ (a list), and t ⇒ ∞ /σ asserts that the execution of t diverges producing an infinite trace σ (a stream). We have shown in this paper, among other things, how to factorize these two separate judgments into a single one. Following up on earlier work [START_REF] Cousot | Inductive definitions, semantics and abstract interpretation[END_REF], Cousot and Cousot further developed the notion of bi-inductive semantics [START_REF] Cousot | Bi-inductive structural semantics[END_REF][START_REF] Cousot | Bi-inductive structural semantics[END_REF]. These semantics are able to characterize both terminating and diverging executions using a common set of inference rules. Their approach is based on the construction of a least fixed point of a set of evaluation rules with respect to a non-standard ordering, which corresponds neither to induction nor coinduction. By contrast, we have shown in this paper how to achieve the same goal using only the standard notions of induction and coinduction. In their work, Cousot and Cousot also decompose the evaluation rule for application in separate rules. However, their decomposition does not go as far as ours. For example, two of their rules perform the evaluation of the left branch of an application, whereas with the pretty-big-step semantics we only need one such rule.

Nakata and Uustalu [START_REF] Nakata | Trace-based coinductive operational semantics for while[END_REF] propose a coinductive relation that provides a bigstep semantics for both terminating and diverging programs, using possiblyinfinite traces (coinductive lists) that record all the intermediate memory states of an execution. Formally, they define traces coinductively: φ := m | m ::: φ. Their (coinductive) big-step evaluation judgment takes the form t /m ⇒ φ. Its definition, whose key rules are shown below, is mutually-recursive with another judgment, t/φ * ⇒ φ . The definition is quite subtle. It is explained next.

t 1/m ⇒ φ t 2 /(m ::: φ) * ⇒ φ (t 1 ; t 2 ) /m ⇒ φ t /m ⇒ φ t/ m * ⇒ φ t/φ * ⇒ φ t/(m ::: φ) * ⇒ (m ::: φ )
To evaluate a sequence (t 1 ; t 2 ), we first evaluate t 1 and obtain a trace φ. Using the relation t 2 /(m ::: φ) * ⇒ φ , we ensure that the trace φ produced by t 1 corresponds to the prefix of the trace φ associated with the term (t 1 ; t 2 ). If the trace φ is finite, then we reach the judgment t 2 / m * ⇒ φ , where m denotes the state produced by t 1 and where φ corresponds to what remains of the trace φ after stripping its prefix φ. We can then proceed to the evaluation of t 2 in m . Otherwise, if the trace φ is infinite, then the third rule shown above applies indefinitely, ensuring that the trace φ associated with the term (t 1 ; t 2 ) is equal (up to bisimilarity) to the trace φ produced by t 1 .

The manipulation of traces involved with the pretty-big-step semantics is, in our opinion, much simpler for several reasons. First, instead of working with potentially-infinite lists, we use a syntactic disjunction between finite traces and infinite traces, so it is always clear whether we are describing a finite or an infinite execution. Second, we do not need to use an auxiliary, mutually-coinductive judgment to traverse traces; instead, we use a simpler concatenation operation that only needs to traverse finite traces. Third, applying Nakata and Uustalu's approach to a λ-calculus instead of a simple imperative language would require all the rules to be stated in continuation-passing style, because the judgment t/φ * ⇒ φ would need to be generalized to the form K/φ * ⇒ φ , where K denotes a continuation that expects the result of the previous computation (that is, the result stored at the end of the trace φ) and produces the term to continue the evaluation from. Such a systematic use of continuations would likely result in fairly obfuscated rules.

Danielsson [START_REF] Anders | Operational semantics using the partiality monad[END_REF] revisits Nakata and Uustalu's work by defining a corecursive function that yields a big-step semantics for both terminating and diverging programs. This function produces a value of type (Maybe Value) ⊥ , where the Maybe indicates the possibility of an error and where the bottom represents the partiality monad. The partiality monad involves two constructors: one that carries a value, and one that "delays" the exhibition of a value. Formally, the coinductive definition is A ⊥ := now A | later (A ⊥ ). The partiality monad thus corresponds to a degenerated version of potentially-infinite traces, where the spine of a trace does not carry any information; only the tail of a trace, if any, carries a value. Note that, to accommodate non-deterministic semantics, the type (Maybe Value) ⊥ needs to be further extended with the non-determinism monad.

In summary, Danielsson's semantics for the λ-calculus consists of a reference interpreter, defined in a formal logic. (It is actually not so straightforward to convince the checker of the guard condition that the definition of the interpreter indeed yields a productive function.) Note that this interpreter should only be used for specification, not for execution, because it is quite inefficient: each bind operation needs to traverse the trace that carries the result that it is binding. Specifying the semantics of a language via an interpreter departs quite significantly from the traditional statement of a big-step semantics as a relation between a term and a result. We find that pretty-big-step semantics remains much more faithful to big-step semantics, and is thus more likely to be accepted as the reference semantics of a programming language. Moreover, some forms of reasoning, such as reasoning by inversion, are typically easier to conduct when the definition is a relation than when it is a function.

Conclusion

In this paper, we addressed the duplication problem associated with big-step semantics by introducing pretty-big-step semantics. Pretty-big-semantics rely on four key ingredients: (1) a breakdown of complex rules into a larger number of simpler rules, (2) a grammar of intermediate terms for ensuring that rules are applied in the appropriate order, (3) an explicit constant div to represent divergence, and (4) an inductive and a coinductive interpretation of the same set of reduction rules. Pretty-big-step semantics accommodate the introduction of a generic error rule for conducting type soundness proofs, and they scale up to realistic programming languages. Moreover, they can easily be extended with traces, in which case the behavior of both terminating and diverging programs is adequately captured by the coinductive evaluation judgment alone.

Fig. 2 .

 2 Fig. 2. Pretty-big-step semantics: e ⇓ o (inductive) and e ⇓ co div (coinductive), with the constructors val, trm, ret and ter left implicit in the rules.

Lemma 2 .

 2 For any term e and outcome o, e ⇓ o → e ⇓ co o.

Lemma 3 .

 3 For any term e and outcome o, e ⇓ co o → e ⇓ o ∨ e ⇓ co div.

b

  := . . . | err abort err var x ⇓ err ∀xt. v1 = abs x t app2 v1 v2 ⇓ err

Fig. 4 .

 4 Fig. 4. Typing rules for outcomes and intermediate terms.

Fig. 5 .

 5 Fig. 5. Pretty-big-step semantics with traces.

  where o ≈ o asserts that o and o describe the same behavior and contain traces that are bisimilar up to insertion or deletion of a finite number of between every two items of the traces. (The equivalence relation ≈ is defined coinductively, by a single rule with premise o ≈ o and with conclusion

t1 /m ⇓ o1 for 1

 1 o1 t1 t2 t3 /m ⇓ o for t1 t2 t3 /m ⇓ o for 1 (ret m false) t1 t2 t3 /m ⇓ ret m tt t3 /m ⇓ o3 for 2 o3 t1 t2 t3 /m ⇓ o for 1 (ret m true) t1 t2 t3 /m ⇓ o t2 /m ⇓ o2 for 3 o2 t1 t2 t3 /m ⇓ o for 2 (ret m tt) t1 t2 t3 /m ⇓ o for t1 t2 t3 /m ⇓ o for 3 (ret m tt) t1 t2 t3 /m ⇓ o abort o for i o t1 t2 t3 /m ⇓ o

Acknowledgments I am grateful to Xavier Leroy for very useful feedback.


Eric Cancès

François Castella

Philippe Chartier

Erwan Faou

Frédéric Legoll

Claude Le Bris

Gabriel Turinici

F R A N Çois Castella

Édéric Legoll

Long-time averaging for integrable Hamiltonian dynamics

Keywords:

come

Introduction

Consider a Hamiltonian dynamics in R d × R d ṗ(t)=-∇ q H(p(t),q(t)),p(0) = p 0 , q(t)= ∇ p H(p(t),q(t)),q(0) = q 0 .

(

) 1
Let M (p 0 ,q 0 ) be the manifold {(p, q) ∈ R 2d | H(p, q)=H(p 0 ,q 0 )}. The solution of ( 1) is a dynamical system on M (p 0 ,q 0 )w i t ht h e invariant measure dρ(p, q)= dσ(p, q) ∇H(p, q) 2 , where dσ(p, q) is the measure induced on M (p 0 ,q 0 ) by the Euclidean measure of R 2d ,a n d • 2 the Euclidean norm in R 2d .

It is a common problem to estimate the space average of an observable A over the manifold M (p 0 ,q 0 ) M (p 0 ,q 0 ) A(p, q)dρ(q, p) M (p 0 ,q 0 ) dρ(q, p) ,

through the limit of the time average lim

T →∞ 1 T T 0 A(p(t),q(t))dt, (3)
where (p(t),q(t)) is the solution of (1). Our wish is here to give a sound ground to (and in some cases improve [START_REF] Cancè S | High-order averaging schemes with error bounds for thermodynamical properties calculations by MD simulations[END_REF]) the numerical simulations of (3) commonly used in the field of molecular dynamics. The conditions under which the two quantities ( 2) and (3) coincide are not known in general and it is out of the scope of this paper to investigate them. In contrast, in the case of an integrable system, a well-known result of Arnold [START_REF] Arnold | Mathematical methods of classical mechanics[END_REF] states that, under a non-resonant condition on the frequency vector associated with the initial condition, the space average of a continuous function on the manifold S(p 0 ,q 0 )={(p, q) ∈ R d × R d ; I 1 (p, q)=I 1 (p 0 ,q 0 ),...,I d (p, q)=I d (p 0 ,q 0 )}, [START_REF] Cancè S | High-order averaging schemes with error bounds for thermodynamical properties calculations by MD simulations[END_REF] where I 1 ,...,I d are the d invariants of the problem (1), coincide with the long-time average of this function. Moreover, if the frequencies satisfy a diophantine condition, the convergence is of order T -1 .Integrable and near-integrable systems under some diophantine condition will thus constitute a natural framework for the present work.

In the following, we consider a completely integrable Hamiltonian system [START_REF] Arnold | Small denominators and problems of stability of motion in classical and celestial mechanics[END_REF] in the sense of the Arnold-Liouville theorem [START_REF] Arnold | Mathematical methods of classical mechanics[END_REF][START_REF] Hairer | Geometric numerical integration[END_REF]: There exist d invariants I 1 = H, I 2 ,...,I d in involution (i.e. their Poisson Bracket {I i ,I j } = 0) such that their gradient are everywhere independent, and the trajectories of the system remain bounded. Under these conditions, there exist action-angles variables (a, θ) in a neighborhood U of S(p 0 ,q 0 ). We have (p, q)=ψ(a, θ), where ψ is a symplectic transformation ψ : D × T d ∋ (a, θ) → (p, q) ∈ U, with T d =(R/2πZ) d the standard d-dimensional flat torus, and D a neighborhood in R d of the point a 0 such that (a 0 ,θ 0 )=ψ -1 (p 0 ,q 0 ). By definition of action-angle variables, the Hamiltonian H(p, q)o f (1) writes H(p, q)=K(a) in the coordinates (a, θ), and thus the dynamics reads ȧ(t)=0, θ(t)=ω(a(t)), [START_REF] Hairer | Geometric numerical integration[END_REF] where ω = ∂K/∂a is the frequency vector associated with the problem. The solution of this system for initial data (a 0 ,θ 0 )simplywrites a(t)=a 0 and θ(t)=ω(a 0 )t + θ 0 .

For fixed (a 0 ,θ 0 )=ψ(p 0 ,q 0 ), the image of S(p 0 ,q 0 )b yψ -1 is the torus {a 0 }×T d . On this torus, the measure dθ is invariant by the flow of [START_REF] Hairer | Geometric numerical integration[END_REF]. Considering the pull-back of this measure by the transformation ψ, we thus get a measure dµ(p, q)o nS(p 0 ,q 0 )w h i c h is invariant by the flow of (1). For any function A(p, q) defined on S(p 0 ,q 0 ) we define the space average:

A := S(p 0 ,q 0 ) A(p, q)dµ(p, q) S(p 0 ,q 0 ) dµ(p, q) = 1 (2π) d T d A • ψ(a 0 ,θ)dθ (6)
For a fixed time T ,t h etime average is defined as

A (T ):= 1 T T 0 A(p(t),q(t))dt. (7)
In a first step, we will investigate the extent to which the convergence of the time average [START_REF] Kolmogorov | General theory of dynamical systems and classical mechanics[END_REF] toward the space average (6) can be accelerated through the use of weighted integrals of the form

A ϕ (T ):= T 0 ϕ t T A(p(t),q(t))dt T 0 ϕ t T dt , ( 8
)
where ϕ is a smooth function with compact support in [0, 1] (later on, we will refer to ϕ as the filter function). In a second step, we will consider the time-discretization of (8), i.e. the discretization of both the integral through Riemann sums and the trajectory with symplectic integrators. In particular, we will derive estimates of the convergence with respect to T and the size h of the time-grid, which are in perfect agreement with the numerical experiments conducted in [START_REF] Cancè S | High-order averaging schemes with error bounds for thermodynamical properties calculations by MD simulations[END_REF].

4E r i c C a n c ès et al.

The complete analysis of the d-dimensional harmonic oscillator

In this section, we illustrate the main ideas of the paper in the rather simple situation of the d-dimensional harmonic oscillator, where most of the analysis can be conducted in an explicit way. Hereafter, H(p, q) is thus the Hamiltonian function from R d × R d to R defined as

H(p, q)= 1 2 d k=1 (ω 2 k q 2 k + p 2 k ), (9)
and the corresponding dynamics is governed by the equations

ṗk = -ω 2 k q k qk = p k ,k=1,...,d.
The exact trajectory lies on the d-dimensional manifold S(p 0 ,q 0 )d efined by [START_REF] Cancè S | High-order averaging schemes with error bounds for thermodynamical properties calculations by MD simulations[END_REF] where the I k (p, q)= 1 2 ω 2 k q 2 k + p 2 k are the conserved energies of the d oscillators. Hence, denoting r 0 k = 2I k (p 0 ,q 0 ), k =1 ,...,d and z =( ω 1 q 1 + ip 1 ,...,ω d q d + ip d ) the aggregated vector of rescaled positions and momenta, the exact solution is of the form

z(t)= r 0 1 e i(ω 1 t+φ 1 ) ,...,r 0 d e i(ω d t+φ d ) , (10)
where φ =( φ 1 ,...,φ d ) depends on the initial conditions (p 0 ,q 0 ). As a consequence, the space average (6) we wish to approximate may be written here as:

A = 1 (2π) d T d (A • Θ)(r 0 ,θ)dθ,
where Θ(r 0 ,θ)=( r 0 1 ω 1 cos(θ 1 ),r 0 1 sin(θ 1 ),...,

r 0 d ω d cos(θ d ),r 0 d sin(θ d ))
. As for the time-average [START_REF] Kolmogorov | General theory of dynamical systems and classical mechanics[END_REF], it reads:

A (T )= 1 T T 0 (A • Θ)(r 0 ,ωt+ φ)dt.
In order to estimate the rate of convergence of ( 7) toward (6), we expand A • Θ in Fourier series (the conditions under which this expansion is valid will be detailed in the following sections):

(A • Θ)(r 0 ,θ)= α∈Z d A • Θ(r 0 ,α)e iα•θ ,
where α • θ = α 1 θ 1 + ...+ α d θ d and with:

A • Θ(r 0 ,α)= 1 (2π) d T d (A • Θ)(r 0 ,θ)e -iα•θ dθ.
In particular, A • Θ(r 0 , 0) = A . Hence, we have:

| A -A (T )|≤ 1 T α∈Z d ,α =0 2| A • Θ(r 0 ,α)| |α • ω| . ( 11
)
This infinite sum can then be bounded if we assume, on one hand, that the vector of frequencies ω =( ω 1 ,...,ω d )s a t i s fi e sSiegel's diophantine condition

∃ γ, ν > 0, ∀ α ∈ Z d , |α • ω| >γ|α| -ν , (12)
and on the other hand, that the Fourier coefficients decay sufficiently rapidly. This relatively poor rate of convergence (1/T )m a yn o wb e considerably improved by considering iterated averages of the form:

A k (T ):= 1 T k T 0 ... T 0 (A • Θ)(r 0 , (t 1 + ...+ t k ) ω + φ)dt 1 ...dt k .
(13) Using Fourier expansions as in [START_REF] Suzuki | Higher-order decomposition theory of exponential operators and its applications to QMC and nonlinear dynamics[END_REF], we indeed obtain in a very similar way the following error estimate for (13):

| A -A k (T )|≤ 1 T k α∈Z d ,α =0 2| A • Θ(r 0 ,α)| |α • ω| k , (14)
and under slightly more stringent bounds on the | A • Θ(r 0 ,α)|, (14) leads to a rate of convergence of 1/T k . Inspired by these computations, and noticing that (13) is a special case of (8) (more precisely A k (T/k)= A ϕ (T )w i t hϕ ≡ χ * k [0,1/k] ,t h ek th -convolution of the characteristic function of [0, 1/k]), we will consider in the sequel more general filter-functions and demonstrate that the rate of convergence can be further improved. Now, a natural question that arises is whether the techniques exposed above are amenable to numerical computations, when both the trajectory z(t) and the integrals [START_REF] Kolmogorov | General theory of dynamical systems and classical mechanics[END_REF] or (13) are approximated using numerical schemes. In the case of the harmonic oscillator, it turns out that the numerical trajectory z h (t n ) (i.e. the approximation at time t n = nh of z(t n )), as soon as the underlying scheme is a symplectic (or symmetric) Runge-Kutta method [START_REF] Chan | Extrapolation of symplectic methods for Hamiltonian problems[END_REF], may be interpreted as the exact solution of a harmonic oscillator with modified 6E r i c C a n c ès et al.

frequencies ω h k = ω k Θ(hω k ). In particular, the numerical trajectory lies on the same manifold S(q 0 ,p 0 ) as the exact one. For the velocity-Verlet scheme, the numerical trajectory would lie on an invariant torus O(h 2 )-close to S(q 0 ,p 0 ). This situation is more typical of what happens for general integrable Hamiltonian systems. In our situation, we have:

z h (t n )= r 0 1 e i(ω 1 Θ(hω 1 )tn+φ 1 ) ,...,r 0 d e i(ω d Θ(hω d )tn+φ d ) ,
where Θ is a smooth function defined by

Θ(y)= 1 y arctan R(iy) -R(-iy) i(R(iy)+R(-iy)) , R (z)
b e i n gt h estability function of the method (in fact, Θ is realanalytic as soon as R has no pole on the imaginary axis and satisfies Θ(y)=1+O(y r )w h e r er denotes the order of convergence of the Runge-Kutta method). As a consequence, the Riemann sum associated with (13) (note that (15) with k = 1 corresponds to ( 7)) reads, for T = nh, n ∈ N,

A Rie k (T ):= 1 n k n-1 j 1 =0 ... n-1 j k =0 (A • Θ)(r 0 , (j 1 + ...+ j k )hωΘ(ωh)+φ), (15)
where ωΘ(ωh)=(ω 1 Θ(ω 1 h),...,ω d Θ(ω d h)), so that using once again Fourier expansions, we get straightforwardly:

| A -A Rie k (T )|≤ 1 n k α∈Z d ,α =0 | A • Θ(r 0 ,α)| e inhα•(ωΘ(ωh)) -1 e ihα•(ωΘ(ωh)) -1 k .
(16) Bounding the above infinite sum now requires to bound the term |e inx -1|/|e ix -1| for x of the form x = hα • (ωΘ(ωh)). To this aim, we use the following two inequalities

∃ C 0 ,x 0 > 0, ∀ n ∈ N, ∀|x|≤x 0 , e inx -1 e ix -1 ≤ C 0 1 |x| , (17)
∀ n ∈ N, ∀ x ∈ R, e inx -1 e ix -1 ≤ n, (18)
according to whether |x| is small (17) or not (18). The bound we are looking for is now based on the following lemma:

Lemma 1 Assume that the vector of frequencies ω satisfies the diophantine condition (12) and the Runge-Kutta method is of order r.

Then, there exist strictly positive constants c and h 0 such that

∀ h ≤ h 0 ∀ α ∈ Z d , |α • (ωΘ(ωh))|≤ γ 2 |α| -ν =⇒|α|≥ch -r ν+1 .
Proof. Assume that there exists α ∈ Z d such that

|α • (ωΘ(ωh))|≤ γ 2 |α| -ν .
Then, from Θ(hω k )=1+O(|hω k | r ), we obtain for h sufficiently small:

γ 2 |α| -ν ≥|ω • α|-C|α||hω| r , ≥ γ|α| -ν -C|α||hω| r ,
where C is the strictly positive constant contained in the term O (note that if Θ ≡ 1, although the constant C is zero, there is no α violating condition (12) and the lemma remains valid). Hence,

|α|≥ γ 2C|ω| r h -r 1 ν+1
.

But for |α|≤ch -r/(ν+1) we have |hα • ωΘ(ωh)|≤ch 1-r/(ν+1) for a constant c independent of h. Hence if ν>r-1, then for small enough h we have |hα • ωΘ(ωh)|≤x 0 defined in (17). Now we can split the sum in (16) into

1≤|α|≤ch -r ν+1 | A • Θ(r 0 ,α)| C k 0 n k h k |α • (ωΘ(ωh))| k + |α|≥ch -r ν+1 | A • Θ(r 0 ,α)|. ( 19
)
Using the estimate of Lemma 1 for the first term and assuming that the Fourier coefficients decay sufficiently rapidly, it then follows that

| A -A Rie k (T )| = O 1 T k + h r . (20)
This seems to be the best possible estimate attainable, since the term in 1/T k is the intrinsic error component of the iterated-average, whereas the term h r inevitably comes into play when using a numerical scheme of order r. It is worth noticing that there is no secular component in the numerical error h r owing to the symplecticity of the time-integrator.

8E r i c C a n c ès et al.

Our aim in next sections is now to prove estimates that generalize (20) in the following two directions: 1. for filtered-averages with general filter functions; 2. for integrable Hamiltonian system with bounded trajectories.

Approximation of the average: The continuous case

The function ϕ considered in Formula ( 8) is somewhat arbitrary. The most commonly used function in practice is ϕ ≡ 1, which corresponds to the usual time-average as defined in [START_REF] Kolmogorov | General theory of dynamical systems and classical mechanics[END_REF], for which convergence when T tends to infinity is rather slow (with rate 1/T ). For the harmonic oscillator, we have seen that the use of iterated-averages (which can be seen as a special case of filtered-averages) allows for a significant acceleration of the convergence. Theorem 1 below shows that with increasingly smooth functions ϕ satisfying appropriate zero boundary conditions, it is possible to improve the rate of convergence to 1/T k for any integer k>1, not only for the harmonic oscillator, but for a general integrable Hamiltonian system. It is then natural to investigate what happens in the limit when k tends to infinity. To this aim, we shall consider, as an example of infinitely differentiable functions ϕ with compact support [0, 1] that satisfy ϕ (k) (0) = ϕ (k) (1) = 0 for any k ∈ N, the function ξ defined below:

ξ :[0, 1] -→ [0, +∞[ x -→ exp - 1 x(1 -x) . (21)
In the sequel, we shall assume that the estimates

ξ (k) L 1 := 1 0 |ξ (k) (x)|dx ≤ µβ k k δk , (22)
ξ (k) L ∞ := sup x∈[0,1] |ξ (k) (x)|≤µβ k k δk , (23)
hold for some strictly positive constants µ, β and δ. The existence of such constants will be shown in Lemma 3.

Theorem 1 Consider the completely integrable system (1),a n da ssume that the diophantine condition (12) is satisfied for ω(a 0 ) defined in (5) by the initial condition (q 0 ,p 0 ),w i t h(q 0 ,p 0 )=ψ(a

0 ,θ 0 ).C o n - sider a function A ∈ C 0 (R d , R d ) (the observable).
Recall that to this function we associate the space-average A ,t h etime-average A (T ) and the filtered time-average A ϕ (T ) respectively defined in (6), ( 7) and (8),w h e r eϕ ∈ C 0 (0, 1) is a filter function (assumed to be positive). Then we have the following convergence estimates:

1. If A is real analytic on R d × R d , then there exists a constant c depending on A, d, ν and γ such that

| A (T ) -A | ≤ c T .
2. If ϕ is C k+1 (0, 1) with ϕ (j) (0) = ϕ (j) (1) = 0 for all j =0,...,k-1, and if A is real analytic on R d × R d , then there exist positive constants c 0 and R depending on A, ϕ, d, ν and γ, such that (here ν ∈ N, though a similar formula holds for general ν using the Γ function)

| A ϕ (T ) -A | ≤ c 0 R k+1 (ν(k +1)+1)! T k+1 × (|ϕ (k) (0)| + |ϕ (k) (1)| + ϕ (k+1) L 1 ) ϕ L 1 .
3. If ξ defined in (21) is taken as the filter function and if A is real analytic on R d × R d , then there exist strictly positive constants c 1 , κ and ρ depending on A, d, ν and γ, such that

| A ξ (T ) -A | ≤ c 1 e -κT 1/ρ .
Proof. Statement 1. is proved in Arnold [START_REF] Arnold | Mathematical methods of classical mechanics[END_REF]. It may also be obtained as a special case of 2. with ϕ ≡ 1. Now, if A is real-analytic on R d ×R d , then so is A • ψ on the d-dimensional torus T d and we can expand it as a Fourier series

(A • ψ)(a 0 ,α)= α ∈ Z d A • ψ(a 0 ,α)e iα • θ ,
with exponentially decaying coefficients:

∀ α ∈ Z d , | A • ψ(a 0 ,α)|≤Ce -|α| C
, where C is a strictly positive real constant. The integral over T d of the first coefficient of the series (α = 0) is straightforwardly identified as the space-average

A • ψ(a 0 , 0) = 1 (2π) d T d (A • ψ)(a 0 ,θ)dθ. Writing T 0 ϕ t T dt = T ϕ L 1 := χ -1
, the error can be computed as follows:

A ϕ (T ) -A = χ α ∈ Z d ,α =0 A • ψ(a 0 ,α) T 0 ϕ t T e iα•(θ 0 +tω(a 0 )) dt(24) = χ α ∈ Z d ,α =0 A • ψ(a 0 ,α)e i(α•θ 0 ) T 0 ϕ t T e it(α•ω(a 0 )) dt.
Now, the running term of the series can be integrated by parts

T 0 ϕ t T e it(α•ω(a 0 )) dt = ϕ t T e it(α•ω(a 0 )) i(α • ω(a 0 )) T 0 - 1 Ti(α • ω(a 0 )) T 0 ϕ ′ t T e it(α•ω(a 0 )) dt.
Integrating repeatedly by parts, this last term writes

e iT (α•ω(a 0 )) ϕ(1) -ϕ(0) i(α • ω(a 0 )) - 1 Ti(α • ω(a 0 )) T 0 ϕ ′ t T e it(α•ω(a 0 )) dt = ... = (-1) k (Ti(α • ω(a 0 ))) k T 0 ϕ (k) t T e it(α•ω(a 0 )) dt,
and eventually,

T 0 ϕ t T e it(α•ω(a 0 )) dt = (-1) k (Ti(α • ω(a 0 ))) k+1 T ϕ (k) t T e it(α•ω(a 0 )) T 0 - (-1) k (Ti(α • ω(a 0 ))) k+1 T 0 ϕ (k+1) t T e it(α•ω(a 0 )) dt.
Inserting this expression in equation ( 24) and taking the moduli of both sides, we finally get the bound

| A ϕ (T ) -A | ≤ (|ϕ (k) (0)| + |ϕ (k) (1)| + ϕ (k+1) L 1 ) T k+1 ϕ L 1 × α∈Z d ,α =0 | A • ψ(a 0 ,α)| |α • ω(a 0 )| k+1
It remains to justify the convergence of the series considered above (and to bound its limit). This is a consequence of the diophantine condition |α • ω(a 0 )|≤ γ |α| ν ,w h i c hg i v e sh e r e

α∈Z d ,α =0 | A • ψ(a 0 ,α)| |α • ω(a 0 )| k+1 ≤ α∈Z d ,α =0 Ce -|α| C |α| γ 1/ν ν(k+1) , ≤ Cη ν(k+1) α∈Z d ,α =0 e -|α| C |α| ηγ 1/ν ν(k+1)
.

We now take η = 2C γ 1/ν so that 1/(γ 1/ν η)=1/(2C)a n dw eo b t a i n :

α∈Z d ,α =0 | A • ψ(a 0 ,α)| |α • ω(a 0 ))| k+1 ≤ Cη ν(k+1) (ν(k +1)+1)! α∈Z d e -|α| 2C , ≤ C(2C) ν(k+1) (8C) d γ k+1 (ν(k +1)+1)!,
where we have used x n ≤ e x (n + 1)!. Statement 3. is a consequence of Statement 2. with a suitably chosen k:s i n c eξ (k) (0) = ξ (k) (1) = 0 for any k ∈ N, we have indeed that for all k ≥ 0:

| A ξ (T ) -A | ≤ c 1 r 1 T k+1 (k +1) δ(k+1) (ν(k +1)+1)!,
with c 1 = c 0 µ and r 1 = Rβ, µ and β being the constants of ( 22). Now let ν be the nearest integer to ν toward infinity. This gives:

| A ξ (T ) -A | ≤ c 1 r 1 ν ν T k+1 (k +1) (δ+ν)(k+1) , ≤ c 1 e f (k+1) , where f (ℓ)=ℓ[log(r 1 ν ν /T )+(δ +ν)log(ℓ)]. The minimum of f for positive ℓ is attained for ℓ = 1 e T r 1 ν ν 1/(ν+δ)
and is worth

f min = - (δ +ν) e T r 1 ν ν 1 (δ+ν)
. Remark 1 In the proof of Theorem 1, one gets c 0 = C(8C) d , R = (2C) ν /γ, c 1 = µc 0 , κ = -(δ +ν)e -1 ν-ν ν+δ and ρ =( δ +ν), where ν = ν + 1. The values of these constants rely heavily on the sharpness of estimates (22) and it is likely that they might be improved. Nevertheless, the convergence behavior would be essentially the same for large dimensions: even if ξ was analytic, one would get ρ =1+ν.More noticeably, since almost all frequencies ω(a 0 ) satisfy the diophantine condition for some γ as soon as ν>d-1, we may think of ν as being d and thus δ as being approximately 1 + d. The rate of convergence thus directly depends on the dimension of the phase-space.

Semi-discrete averages

We now wish to investigate whether the estimates of Theorem 1 persist when one replaces the integrals by Riemann sums. It turns out, quite remarkably, that its proof can be almost readily adapted, if one assumes the additional non-resonance condition [START_REF] Hairer | Geometric numerical integration[END_REF], i.e. if, given a step-size h, there exist positive constants γ * and ν * such that for all α ∈ Z d , the following estimate holds:

1 -e iα • hω(a 0 ) h ≥ γ * |α| -ν * . ( 25
)
Though this condition might appear very restrictive at first glance, the probability of picking an h ∈ [0,h 0 ] violating (25) goes to zero with h 0 , whenever the diophantine condition is satisfied, γ * ≤ γ and ν * >ν+ d + 1. For a precise statement of this result, we refer to Lemma 6.3. in Chapter X of [START_REF] Hairer | Geometric numerical integration[END_REF] (see also [START_REF] Shang | Resonant and Diophantine step sizes in computing invariant tori of Hamiltonian systems[END_REF]).

Theorem 2 Assume that the conditions of Theorem 1 and condition (25) are satisfied and let T = nh > 0 for a given integer n ≥ 2.L e t us further define the Riemann sums corresponding to the continuous time-average

A Rie (T ):= 1 n n-1 j=0
A(q(jh),p(jh)), and the filtered time-average

A Rie ϕ (T ):= n-1 j=0 ϕ( j n )A(q(jh),p(jh)) n-1 j=0 ϕ( j n )
, where ϕ ∈ C 0 (0, 1) is the filter function. Then we have the following convergence estimates:

1. If A is real analytic on R d × R d , then there exists a constant c * depending on A, d, ν * and γ * such that

A Rie (T ) -A ≤ c * T .
2. If ϕ is C k+1 (0, 1) with ϕ (j) (0) = ϕ (j) (1) = 0 for all j =0,...,k-1, and if A is real analytic on R d ×R d , then there exist strictly positive constants c * 0 and R * depending on A, ϕ, d, ν * and γ * , such that

A Rie ϕ (T ) -A ≤ c * 0 (R * ) k+1 k k (ν * (k +1)+1)! T k+1 (|ϕ (k) (0)| + |ϕ (k) (1)| + ϕ (k+1) L ∞ ) ϕ L 1 .

If ξ is taken as the filter function and if

A is real analytic on R d × R d , then there exist strictly positive constants c * 1 , κ * and ρ * depending on A, d, ν * and γ * , such that

A Rie ξ (T ) -A ≤ c * 1 e -κ * T 1/ρ * .
Remark 2 In the proof of Theorem 2, one gets

c * 0 =2 εe 2 C(8C) d , R * =( 2 C) ν * /γ * , c * 1 = µc * 0 , κ * = -(δ +1+ν * )e -1 (ν * ) - ν *
ν * +δ+1 and ρ * =(δ +1+ν * ), where ν * = ν * +1 and where

ε = ϕ L 1 sup n≥2   n-1 j=0 (1/n)ϕ(j/n)   -1 .
It is worth noticing that these constants do not depend on the stepsize h.

Proof. Statement 1. is a special case of Statement 2. with ϕ ≡ 1, so that we focus on the error estimate for the filtered average. Expanding (A • ψ) in Fourier series as in Theorem 1 and denoting S n = n-1 j=0 (1/n)ϕ(j/n), we have:

A Rie ϕ (T ) -A = 1 nS n α ∈ Z d ,α =0 A • ψ(a 0 ,α)e i(α • θ 0 ) × n-1 j=0 ϕ j n e iα • jhω(a 0 ) . (26)
We use the following result, whose proof is given in Appendix:

Lemma 2 For a given filter-function ϕ in C k+1 (0, 1) with ϕ (j) (0) = ϕ (j) (1) = 0 for all j =0 ,...,k -1, and a given integer n ≥ k +2, let ϕ j be the real numbers defined by ϕ j = ϕ(j/n) for j =0,...,n.I f b =1is a complex number of modulus 1, then we have the estimate

0≤j≤n-1 ϕ j b j ≤ 2e 2 k k n k |1 -b| k+1 |ϕ (k) (0)| + |ϕ (k) (1)| + ϕ (k+1) L ∞
Using this lemma with b = e iα•hω(a 0 ) , we obtain:

A Rie ϕ (T ) -A ≤ 2e 2 k k n k+1 S n |ϕ (k) (0)| + |ϕ (k) (1)| + ϕ (k+1) L ∞ × α ∈ Z d ,α =0 Ce -|α|/C |1 -e iα • hω(a 0 ) | k+1
We now use condition (25) and obtain:

α ∈ Z d ,α =0 Ce -|α|/C |1 -e iα • hω(a 0 ) | k+1 ≤ C h k+1 α ∈ Z d ,α =0 e -|α|/C |α| ν * (k+1) (γ * ) k+1 , ≤ C(2C) ν * (k+1) (8C) d h k+1 (γ * ) k+1 (ν * (k +1)+1)!.
This proves Statement 2. Statement 3. can then be obtained as in Theorem 1.

Fully discrete averages

We now consider a symplectic discretization of the exact trajectory of [START_REF] Arnold | Small denominators and problems of stability of motion in classical and celestial mechanics[END_REF]. Two types of results exist, according to whether we use results on invariant tori of symplectic integrators [START_REF] Kolmogorov | On conservation of conditionally periodic motions under small perturbations of the Hamiltonian[END_REF][START_REF] Hairer | Geometric numerical integration[END_REF] or ultraviolet cutoff theory [START_REF] Arnold | Small denominators and problems of stability of motion in classical and celestial mechanics[END_REF][START_REF] Hairer | Geometric numerical integration[END_REF]. Given that the strong non-resonance condition (25) already appears for semi-discrete averages, we will only detail results using KAM tori in the spirit of [START_REF] Hairer | Geometric numerical integration[END_REF][START_REF] Shang | Resonant and Diophantine step sizes in computing invariant tori of Hamiltonian systems[END_REF].

In action-angles variables, the Hamiltonian H(p, q)=K(a)d epends only on a. Without loss of generality, we may assume that a 0 =0,sothatw ecanwrite

K(a)=c + ω • a + 1 2 a T M (a)a,
where ω = ω(0). We assume that M is non degenerate in the sense that ∃ α>0, M (0

)v ≥α v for v ∈ R d , (27)
so that Kolmogorov-Arnold-Moser theory can be applied (see [START_REF] Kolmogorov | On conservation of conditionally periodic motions under small perturbations of the Hamiltonian[END_REF][START_REF] Kolmogorov | General theory of dynamical systems and classical mechanics[END_REF][START_REF] Arnold | Small denominators and problems of stability of motion in classical and celestial mechanics[END_REF][START_REF] Moser | On invariant curves of area-preserving mappings of an annulus[END_REF]).

We consider a symplectic integrator Φ h of order r applied to the problem (1) with a stepsize h.T h en u m e r i c a ls o l u t i o ni sw r i t t e n (p n ,q n ) ∈ R d for n ≥ 0. For a function A defined in a neighborhood of S(p 0 ,q 0 )a n df o rT = nh, we define the filtered numerical time-average

A Rie ϕ,h (T ):= n-1 j=0 ϕ( j n )A(q j ,p j ) n-1 j=0 ϕ( j n ) . (28)
Under these conditions, we can apply Theorems 6.1 and 6.2 of [START_REF] Hairer | Geometric numerical integration[END_REF] (see also [START_REF] Shang | KAM theorem of symplectic algorithms for Hamiltonian systems[END_REF][START_REF] Shang | Resonant and Diophantine step sizes in computing invariant tori of Hamiltonian systems[END_REF]): For small enough h, there exists a symplectic analytic transformation ψ h :( b, ϕ) → (a, θ), O(h r )-close to the identity, such that ψ

-1 h • Φ h • ψ h :(b, ϕ) → ( b, ϕ)i sg i v e nb y b = b -h ∂S h ∂ ϕ (b, ϕ)a n d ϕ = ϕ + h ∂S h ∂b (b, ϕ) with S h (b, ϕ)=c h + ω • b + 1 2 b T M h (b, ϕ)b,
where c h ∈ R and M h is analytic and bounded with respect to h.I n coordinates (b, ϕ), we thus have

ψ -1 h • Φ h • ψ h :(b, ϕ) → (b, ϕ + hω)+O(h b ) (29)
Based on this transformation, we have the following result:

Theorem 3 Consider a symplectic integrator Φ h of order r and of stepsize h applied to (1) under the conditions of Theorem 1. Assume that (27) holds, and suppose that ω and h satisfy the conditions (12) and (25). Then we have the following estimates:

1. If ϕ is C k+1 with ϕ (j) (0) = ϕ (j) (1) = 0 for all j =0 ,...,k -1 and if A is real analytic on R d , then there exist constants C and h 0 depending on A, γ * , ν * , d, k, ϕ, and there exist (p 0 , q0 ) in an h r -neighborhood of (p 0 ,q 0 ) such that if the numerical trajectory starts with (p 0 , q0 ), then we have

∀h ≤ h 0 ∀ T = nh ≥ 0, | A Rie ϕ,h (T ) -A | ≤ C 1 T k+1 + h r (30) 2.
If ξ is taken as the filter function, if A is real analytic, then there exist constants C, h 0 , κ and ρ depending on A, γ * , ν * , d, k,a n d there exist (p 0 , q0 ) in an h r -neighborhood of (p 0 ,q 0 ) such that if the numerical trajectory starts with (p 0 , q0 ), then we have

∀h ≤ h 0 ∀ T = nh ≥ 0, | A Rie ξ,h (T ) -A | ≤ C e -κT 1/ρ + h r (31)
Proof. Using (29), we have for all n

ψ -1 h • Φ n h • ψ h :(b, ϕ) → (b, ϕ + nhω)+O(nh b ) Consider the points (b n ,ϕ n )=ψ -1 h • ψ -1 (p n ,q n )
, and suppose that the point (p 0 ,q 0 ) is such that b 0 = 0. Then using the previous formula, we have

∀ n ≥ 0,b n = b 0 =0 and ϕ n = ϕ 0 + nhω.

Now we have with S

n = n-1 j=0 (1/n)ϕ(j/n), A Rie ϕ,h (T ):= 1 nS n n-1 j=0 ϕ( j n )A • ψ • ψ h (b j ,ϕ j ),
and using the Fourier expansion of

A • ψ • ψ h , A Rie ϕ,h (T ):= 1 nS n α∈Z d A • ψ • ψ h (0,α)e iα•ϕ 0 n-1 j=0 ϕ( j n )e iα•jhω .
As ψ h is an analytic function O(h r )-close to the identity, we have

A • ψ • ψ h (0, 0) = A + O(h r ),
and the Fourier coefficients A • ψ • ψ h (0,α) decay exponentially with respect to α, uniformly with respect to h. Thus the same proof as in Theorem 2 shows the result.

Remark 3 For the iterated averages, as defined in Section 2:

A Rie k,h (T ):= 1 n k n-1 j 1 =0 ••• n-1 j k =0
A(q J ,p J ),k≥ 0,

where J = j 1 + •••j k , we would get, using the result of Section X.4 in [START_REF] Hairer | Geometric numerical integration[END_REF], and by similar computations as in ( 16) and (19),

| A Rie k,h (T ) -A | ≤ C 1 T k + h r (33)
over exponentially long time-interval.

Remarks on the implementation and numerical experiments

Though optimal with respect to the rate of convergence, the filter function ξ does not seem to allow for the derivation of an error estimate: Given that the values of the constant C in (31) is out of reach, the value of n for which

R ϕ n := n j=0 ϕ(j/n)A j n ϕ L 1
becomes sufficiently close (up to user's tolerance) to its limit as n goes to infinity can not be determined in advance. An update formula for R ϕ n from n to n+1 thus appears of much use and this should guide the choice of ϕ. In order to get such a formula, we study the dependence in T of

a(T )= T 0 ϕ t T A(p(t),q(t))dt.
Differentiating with respect to T leads to

da(T ) dT = ϕ(1)A(p(T ),q(T )) - 1 T T 0 t T ϕ ′ t T A(p(t),q(t))dt.( 34
)
To be of practical use, it is thus necessary that xϕ ′ (x)i so ft h ef o r m αϕ(x)( w h e r eα is an arbitrary constant) so that (34) becomes an ordinary differential equation for a(T ). The only admissible solutions are thus monomials in x. We thus consider the following polynomial filter functions

ϕ p (x)=x p (1 -x) p ,p∈ N. ( 35
)
Denoting for p and n in N the elementary Riemann sums

S p n = n j=0 j n p A j ,
it is easy to get the desired update formula We now consider the application of our method to the 3-dimensional Kepler problem with Hamiltonian

S p 0 =0andS p n = A n +(1-1/n) p S p n-1 ,n ≥ 1. Now, since
H(p, q)=p 2 1 + p 2 2 + p 2 3 - 1 q 2 1 + q 2 2 + q 2 3 .
Besides the Hamiltonian, this system has three other invariants, the so-called angular momenta

L 1 = q 2 p 3 -q 3 p 2 ,L 2 = q 1 p 3 -q 3 p 1 and L 3 = q 2 p 1 -q 1 p 2 ,
= L 2 1 + L 2 2 + L 2 3 .
Our goal is here to estimate the average over the manifold S = {(p, q) ∈ R 6 ; L 1 (p, q)=L 1 (p 0 ,q 0 ),L 2 (p, q)=L 2 (p 0 ,q 0 ), L 3 (p, q)=L 3 (p 0 ,q 0 ),H(p, q)=H(p 0 ,q 0 )} of the quantity r = q 2 1 + q 2 2 + q 2 3 , for it is known to have the following analytical expression r = 3+2H(p 0 ,q 0 ) L(p 0 ,q 0 ) 2 4 |H(p 0 ,q 0 )| .

For p 0 =( 0 , 1.1, 0.5) T and q 0 =( 0 .9, 0, 0) T this leads to r = 1.376630029154519.

To this aim, we consider the Verlet method as basic step and use the 8 th -order 15-stages composition of [START_REF] Suzuki | Higher-order decomposition theory of exponential operators and its applications to QMC and nonlinear dynamics[END_REF]. On Figure 1 are represented the errors | r ϕp (T ) -r | in logarithmic scale for two different step-sizes. On the left of the figure, the three curves all reach a plateau corresponding to the incompressible h-error term. Refining the step-size removes this plateau (or at least shifts it to the left, see the right graphics). In both cases, the predicted rate of convergence in 1/T p+1 is clearly observed (it corresponds to a slope of p +1 for ϕ p ).

Appendix: some technical results

In this appendix section, we collect a few technical results used in the paper.

Lemma 3 Let ξ be the function defined on [0, 1] by ξ(x)=e -1

x(1-x) . There exist strictly positive constants µ ≤ 1, β ≤ (2 √ 3+6)/e 2 and δ ≤ 3 such that the following estimates hold for all k ∈ N * :

ξ (k) L 1 := 1 0 |ξ (k) (x)|dx ≤ µβ k k δk , ξ (k) L ∞ =s u p x∈[0,1] |ξ (k) (x)|≤µβ k k δk .
Proof. Looking for an expression of ξ

(k) (x)o ft h ef o r m ξ (k) (x)= P k (x) [Π(x)] 2k e -1 x(1-x) ,
where Π(x)=x(1 -x)a n dw h e r eP k is a polynomial, we easily find the recurrence relation: A bound can then be obtained as follows: let ε 0 = -1+ √ 3 2

P 0 ≡ 1a n dP k+1 = Π ′ (1 -2kΠ) P k + P ′ k Π 2 ,k≥ 0, (36)
, ε = ε 0 k and r =1/2. Then it is easy to check that for all 0 ≤ i ≤ k,w eh a v e

C( 1 2 + i ε 0 k ,k-i, ε 0 k ) ≤ √ 3 2 [k -i +1]+ 1 √ 3 -1 k + i +1, ≤ √ 3+3 2 (k +1),
and hence,

k i=0 C(r + iε, k -i, ε) ≤ [ √ 3+3 2 (k +1)] k+1 .
Taking into account that P 0 ≡ 1, we obtain

∀ k ∈ N * , sup z∈B 1/2 |P k (z)|≤[ √ 3+3 2 k] k .
It remains to bound

1 [Π(x)] 2k e -1
x (1-x) .D e n o t i n gY = 1

x(1-x) ,w eh a v e : Proof of lemma 2. Let us denote by ∇ the operator of backward divided differences defined by: ∀ j ∈{0,...,n}, ∇ 0 ϕ j = ϕ j , ∀ j ∈{m +1,...,n}, ∇ m+1 ϕ j = ∇ m ϕ j -∇ m ϕ j-1 .

The sum in the statement can then be written as Denoting h =1 /n, it is well-known that, for all n -1 ≤ j ≥ k +1, there exists ζ j,k+1 ∈ [(j -k -1)h, jh] ⊂ [0, 1] such that we have:

∇ k+1 ϕ j = ϕ (k+1) (ζ j,k+1 )h k+1
Hence, we can bound the second term in (37) as follows: Gathering the contributions of all terms then gives the result.

  k p kx p+k and ϕ p L 1 = (p!) 2 (2p +1)! the approximation we seek for can be obtained as the linear combination R

Fig. 1 .

 1 Fig. 1. Error in the averages for p =1, 3, 5 for the 3D-Kepler problem

  We now look for bounds on balls B r of radius r>0 and center z =1/2+0i ∈ C. The bounds for Π and Π ′ read sup z∈Br |Π(z)|≤(r 2 +1/4), sup z∈Br |Π ′ (z)|≤r, and the Cauchy integral representation of P ′ k leads to∀ ε>0, sup z∈Br |P ′ k (z)|≤ r + ε ε sup z∈B r+ε |P k (z)|.Inserting these bounds in (36) we get:sup z∈Br |P k+1 (z)|≤r[k(2r 2 -1/2) + 1] sup z∈Br |P k (z)| +(r 2 +1/4) 2 r + ε ε sup z∈B r+ε |P k (z)|, ≤ r[k(2r 2 -1/2) + 1] + r + ε ε (r 2 +1/4) 2 sup z∈B r+ε |P k (z)|. Denoting C(r, k, ε):=r[k(2r 2 -1/2) + 1] + r+ε ε (r 2 +1/4) 2 , we finally get sup z∈Br |P k+1 (z)|≤C(r, k, ε)s u p z∈B r+ε |P k (z)|, ≤ C(r, k, ε)C(r + ε, k -1,ε)s u p z∈B r+2ε |P k-1 (z)|,≤ k i=0 C(r + iε, k -i, ε) sup z∈B r+(k+1)ε |P 0 (z)|.

  x)] 2k e -1 x(1-x) =s u p Y ≥4 e -Y Y 2k ≤ e -2k (2k)!

( 1 ( 1 -

 11 ∇ϕ j )b j = ..., = k m=0 b m ∇ m ϕ m -b n ∇ m ϕ n-ϕ j )b j .

e 2 k

 2 ϕ j )b j ≤ ϕ (k+1) L ∞ h k+1 (n -k -2).In order to estimate the first sum, we notice that, for 0≤ m ≤ k ≤ n -2, ∇ m ϕ m = ϕ (m) (ζ m,m )h m for some ζ m,m ∈ [0,mh] and a Taylor-Lagrange expansion of ϕ (m) (ζ m,m ) at order k +1-m gives ∇ m ϕ m = ζ k m,m h k (k -m)! ϕ (k) (0) + ζ k+1 m,m h k+1 (k +1-m)! ϕ (k+1) (η m )for some η m ∈ [0,mh] ⊂ [0, 1]. Hence, we have:k m=0 b m (1 -b) m ∇ m ϕ m ≤|ϕ (k) (0)| k k h k |1k h k |1 -b| k+1 |ϕ (k) (0)| + h ϕ (k+1)L ∞ . Similarly we have:∇ m ϕ n-1 = ϕ (m) (ζ n-1,m )h m for some ζ n-1,m ∈ [1 -(m +1)h, 1 -h] ⊂ [0, 1], so that k m=0 b n (1 -b) m ∇ m ϕ n-1 ≤ 2e 2 k k h k |1 -b| k+1 |ϕ (k) (1)| + h ϕ (k+1) L ∞ .

Acknowledgements The authors are glad to thank Christian Lubich for stimulating discussions on the subject of this paper, particularly for suggesting the use of general filtered averages rather than just iterated averages. We also gratefully acknowledge the financial support of INRIA through the contract grant "Action de Recherche Concertée" PRESTISSIMO.