W Hu

Z Y Yin

Professor

C Dano

P Y Hicher

Numerical study of crushable granular materials

Keywords: Granular materials, grain breakage, elasto-plasticity, critical state, grain size distribution

The paper aims to develop an elasto-plastic model considering particle crushing. For this purpose, the relationship between the grain size distributions, the position of the critical state line and the plastic work is investigated using experimental results on Cambria sand. The constitutive equations describe two yield mechanisms (isotropic and deviatoric) accounting for particle crushing, which in return affects the position of the critical state line in the e -log(p') diagram. The model is then used to simulate triaxial tests under different loading conditions (drained compression and extension) with high stress levels. All comparisons between experimental results and simulations demonstrate that the model can reproduce with good accuracy the mechanical behavior of granular materials with particle crushing.

INTRODUCTION

Particle crushing occurred along both compression and shearing stress paths, especially under high confining stress (e.g. within earth dams, deep well shafts). This phenomenon is however more intense during shearing. The influence of particle crushing on the mechanical behavior of granular materials has been widely investigated in the past decades.

To account for particle crushing effect, different modeling methods were proposed in the literature. For instance, [START_REF] Russell | A bounding surface plasticity model for sands exhibiting particle crushing[END_REF] used a threesegment type critical state line (CSL) to describe the behavior of crushable granular materials. Salim and Indraranatna (2004) proposed flow rules and yield functions which integrate the effects of particle crushing. [START_REF] Daouadji | An elastoplastic model for granular materials taking into account grain breakage[END_REF] proposed a revisited Cam-Clay yield surface in which the hardening parameter (consolidation effective pressure) is made dependent on the plastic work. It implies a shift of the position of the critical state line in the e -log (p') diagram where e is the current void ratio and p' the mean effective stress. Later on, Muir [START_REF] Muir Wood | Changing grading of soil: effect on critical state[END_REF] and [START_REF] Muir Wood | Particle crushing and deformation behaviour[END_REF] also considered the shift of the CSL with grain gradation, through a grading state index (I G ) which changes with the position of a so-called crushing surface.

Here, an elasto-plastic model based on a Mohr-Coulomb yield criterion for the shearing mechanism, in which the void ratio at critical state is a function of plastic work, is developed. .

In what follows, an analysis of published experimental results aims at establishing relationships between CSL, particle crushing and energy consumption. The model is finally verified by simulating tests on Cambria sand specimens under different loading conditions and high confining stresses.

CONSTITUTIVE MODEL

For the elastic part of the model, the isotropic hypo-elasticity assumption is adopted. For modeling the plastic behavior, the proposed approach uses two yield surfaces for shear and compression components respectively. Thus the framework of the proposed approach is similar to that of the double-hardening or double-yield-surface models by [START_REF] Vermeer | A double hardening model for sand[END_REF].

Elastic part

The elastic strain increments were deducted by using elastic law:

d d d ; d 3 e e v d p q K G ε ε = = (1)
where G and K are the hypo-elastic shear and bulk moduli respectively and are defined as follows (Richart et al. [20]):

( ) ( ) 2 0 2.97 ' 1 n at e p G G e p -   =   +   (2) ( ) ( ) 2 0 2.97 ' 1 n at e p K K e p -   =   +   (3)
where G 0 , K 0 and n are elastic parameters; p at is the atmospheric pressure used as reference pressure (p at = 101.325 kPa) and p' the mean effective stress. For Cambria sand, K 0 = 26.3 MPa and n = 0.4 were calibrated from isotropic compression test, and G 0 = 35 MPa was calibrated from the initial part of the stress strain curve (e.g., ε 1 < 0.1 %) resulting from drained triaxial compression tests.

Shear yield criterion

As many models relevant for sand behavior, the shear mechanism is represented by a linear yield function in the (p'-q) plot where q is the deviatoric stress. The shear yield function is written as follows:

S f H η = - ( 4
)
where η is the stress ratio q/p'; H is the hardening parameter defined by a hyperbolic function in the Hε d p plane, similarly to [START_REF] Yin | Micromechanical modelling for effect of inherent anisotropy on cyclic behaviour of sand[END_REF], given as:

p p d p p d p M H M p G K ε ε = ′ + (5)
where G p is used to control the initial slope of the hyperbolic curve η-ε d p . Eq. ( 5) guarantees that the stress ratio will approach the peak value M p .

In order to take into account the dilation or contraction during the shear sliding, the Roscoe-type stress-dilatancy equation is used:

( ) p v pt p d d D M d ε η ε = - ( 6
)
where D is a soil parameter. M pt is the slope of the phase transformation line in the (p' -q) diagram.

Normal compression criterion

In order to describe the compressible behavior of crushable granular materials, a second yield surface is added. The second yield function is assumed to be as follows:

N y f p p ′ = - (7)
where p y is the hardening parameter controlling the size of the second yield surface. The yield surface expands with the plastic volumetric strain. The hardening rule of the Modified Cam Clay model is adopted:

p v y y p d dp p c ε = (8)
An associated flow rule is adopted for the normal compression.

In order to interpolate M between its values M c (for compression) and M e (for extension) by means of the Lode angle et al., 2000), the following relationships is assumed:

1 3 3 / 2 2 1 3 3 sin 6 3 2 6 J J -  -π - π ≤ θ = ≤       (Sheng
( )

1 4 4 4 4 2 1 1 sin 3 c c M M c c µ θ     = + + -     (9)
where c=(3-sinφ µ )/(3+sinφ µ ) assuming the same constant volume friction angle φ µ for compression and extension conditions.

( )

2 2 1 3 2 3 J I I = +
and ( )

3 3 1 1 2 3 2 9 27 27 J I I I I = + +
are respectively the second and third invariants of the deviator stress tensor with I 1 =σ' 1 +σ' 2 +σ' 3 ,

I 2 =σ' 1 σ' 2 + σ' 2 σ' 3 + σ' 3 σ' 1 , I 3 =σ' 1 σ' 2 σ' 3 under axi- symmetric triaxial conditions.

Density state effect

The density state of soil is defined as the ratio e c /e, where e c is the critical void ratio and e is the current void ratio of soil at current p'.

According to [START_REF] Biarez | Elementary Mechanics of Soil Behaviors[END_REF], the peak friction angle φ p (relating to M p = 6sinφ p /(3sinφ p ) for triaxial compression) relates to the intrinsic friction angle φ µ (relating to the critical state value M=6sinφ µ /(3-sinφ µ ) for triaxial compression) and density state of soil (e c /e): (10) The parameter M p is therefore obtained through the critical state M and density state e c /e. Eq. ( 10) means that in a loose structure, the "peak" frictional angle φ p is smaller than φ µ . On the other hand, a dense structure provides a higher degree of interlocking. Thus, the peak frictional angle φ p is greater than φ µ . When the loading stress reaches the peak frictional angle φ p , the dense structure dilates and the degree of interlocking relaxes. As a consequence, the peak frictional angle is reduced, which results in a strainsoftening phenomenon.

M pt is the slope of phase transformation line for sand which is assumed as follows: [START_REF] Hardin | Crushing of soil particles[END_REF] proposed a breakage index to quantify the amount of particle crushing. The index is based on the changes in particle size as the key measure. [START_REF] Einav | Breakage mechanics-Part I: Theory[END_REF] modified the breakage index, termed as B r , based on the changes on the overall grain size distribution as follows:

BREAKAGE ANALYSIS

Definition of breakage index

( ) ( ) ( ) ( ) 0 0 ( ) (log( )) ( ) (log( )) M m M m d d p r d t u d F d F d d d B B B F d F d d d - = = - ∫ ∫ (12)
where B p is the area between the curves of original size distribution and current grain size distribution; B t is the total area between the curves of original size distribution and an assumed limit grain size distribution of fractal form. F 0 (d) and F u (d) represent the initial gradation before particle crushing and the fractal distribution with high quantities of particle crushing respectively; F(d) is the current gradation during loading during which particle crushing occurs; d is the grain size; d M and d m are respectively the maximum grain size and the minimum grain size. The gradation can be expressed as:

( )

( ) / M F d d d α = ( 13
)
where α is a material constant.

Influence of plastic work on the evolution of gradation

In this section, results of drained triaxial compression tests on Cambria sand [START_REF] Yamamuro | Drained sand behavior in axisymmetric tests at high pressures[END_REF][START_REF] Lade | Significance of particle crushing in granular materials[END_REF] were analyzed to investigate the relationship between the breakage index B r and the modified plastic work w p representing energy consumption. Cambria sand is a coarse and uniform sand consisting of sub-angular to well-rounded grains. The diameter of the grains varies from 0.83 to 2 mm. The maximum void ratio is 0.792 and the minimum void ratio is 0.503. The specific gravity is 2.69.

The modified plastic work is expressed as follows:

p p p v d w p d qd ε ε ′ = + ∫ ( 14
)
where p' = (σ' 1 +2σ' 3 )/3 with σ' 1 and σ' 3 representing principle stresses; q is the deviatoric stress: q = σ' 1σ' 3 ; dε v p and dε d p are the volumetric and deviatoric plastic strain increments respectively: dε v p = dε 1 p +2dε 3 p and dε d p = 2(dε 1 p -dε 3 p )/3; <F> is the MacCauley function such as: <F> = 0 for F < 0 and <F> = F for F>0. Using this MacCauley function, the shear induced dilation (dε v p <0) is not accounted in the modified plastic work. As a result, the gradation cannot be influenced by dilation when using this modified plastic work to link with. The values of breakage index B r for different tests were measured. For each test, the modified plastic work w p was also calculated based on the stress strain curves. The breakage index B r is then plotted against w p in Figure 1(a) showing that the value of B r increases with the modified plastic work. Based on Figure 1(a), the hyperbolic function is proposed for the relationship between B r and w p , as follows:

p r p w B w χ = + ( 15
)
where χ is a material constant controlling the evolution rate of gradation. For Cambria sand, χ = 15000 is obtained.

Influence of gradation on the position of critical state line

The critical state void ratio e c is a function of the mean effective stress p'. The relationship has traditionally been written as Eq. ( 16). The location of the CSL in the e -log(p') plane depends on three parameters e ref , λ and p' ref :

ln c ref ref p e e p λ   ′ = -       (16)
where p ref = 100 kPa is assigned. The couple (e ref ; p' ref determine a reference point in the e -log(p')' plane, and λ determines the slope of the CSL.

According to [START_REF] Biarez | Elementary Mechanics of Soil Behaviors[END_REF], the position of CSL moves down in the e-log(p') plan with the increase of the coefficient of uniformity C u (d 60 /d 10 ) based on experimental tests on sub-angular Hostun sand. The movement of CSL has also been discussed by Muir Wood and Maeda (2008) using discrete element analysis which agrees with [START_REF] Biarez | Elementary Mechanics of Soil Behaviors[END_REF]. However, there is no relationship available between the position of CSL and the gradation based on experiments. From the concept of CSL (at critical state, the material remains at a constant volume while it is subjected to a continuous distortion), if the CSL can move, it is no longer CSL. We note that, in this paper, we still use this term but representing the temporary position of CSL for a grading curve.

Drained compression tests on Cambria sand up to failure by [START_REF] Yamamuro | Drained sand behavior in axisymmetric tests at high pressures[END_REF] were used to investigate the movement of CSL with the gradation. For each drained compression test, the void ratio at failure with the mean effective stress p' was measured and considered as a temporary critical state corresponding to a gradation. The reference void ratio e ref representing the temporary position of CSL was then obtained by Eq. ( 16). Based on all drained compression tests, e ref is plotted against the breakage index B r , as shown in Figure 1 where e ref0 and e refu is the initial and ultimate reference critical state void ratios respectively; ρ is a material constant relating to the movement rate of CSL with breakage index due to particle crushing. For Cambria sand, e ref0 = 0.59 and λ = 0.006 were obtained from drained triaxial compression tests under low confining stresses (less than 1 MPa) for which [START_REF] Yamamuro | Drained sand behavior in axisymmetric tests at high pressures[END_REF] indicated that only slight grain crushing occurred. e refu = 0.13 and ρ = 0.16 were obtained from Figure 1(b).

According to experimental investigations, Eq. ( 15) and Eq. ( 17) were proposed and can be used for Eq. ( 16). Therefore, particle crushing can influence directly the position of CSL, which results in the change of the density state e c /e. All terms relating to e c /e (e.g., φ p , φ pt , H etc.) are then influenced. The particle crushing is then incorporated into the model. The effect of particle crushing or the influence of some selected parameters are shown in Figure 2.

TEST SIMULATIONS

All determined values of constitutive parameters are summarized in Table 1, and will be subsequently used for simulations along different stress paths.

SIMULATIONS OF DRAINED TESTS IN COMPRESSION AND EXTENSION

Figure 3 shows comparisons between experimental results and simulations for drained triaxial tests in compression with confining stresses varying from 2.1 to 52 MPa. Good agreement was achieved for all comparisons. The model well captured the mechanical behavior of sand influenced by particle crushing:

(1) Under low confining stress (2.1 MPa), the sample exhibits a dilative behavior. (2) For higher confining stresses, the samples present a contractive behavior. This disappearance of dilation is related to more particle crushing occurred under high stresses (2.1-26 MPa). For tests under confining stresses from 2.1 to 26 MPa, the contraction increases with the increase of confining stress. (3) However, for tests under confining stresses from 26 to 52 MPa, volumetric strain decreases with the increase of confining stress. [START_REF] Yamamuro | Drained sand behavior in axisymmetric tests at high pressures[END_REF] indicated that this effect is caused by the increase in the amount of volumetric contraction and particle crushing during isotropic consolidation. Lower void ratios are obtained with increasing confining stress, which in turn allows less volumetric contraction during shearing. This trend was well captured by the model incorporating particle crushing. The increase of particle crushing during isotropic loading results in a low amount of crushable sand left during shearing stage (see Fig. 1a: the change of B r becomes stable for high plastic work). As a result, the contraction of sample caused by particle crushing is reduced. Using all parameters determined from drained compression tests, the model has also been applied to simulate the drained extension tests on Cambria sand with confining stress varying from 6 to 42MPa by [START_REF] Bopp | Relative density effects on undrained sand behavior at high pressures[END_REF]. Good agreement was achieved between experimental results and simulations, as shown in Figure 4. The model well captured the stress strain response and the volumetric strain response for different confining stress levels.

Conclusions

Experimental investigations were carried out on the evolution of gradation with the modified plastic work and on the evolution of the position of CSL with the gradation. Based on this, two constitutive equations were proposed for the relationship between the breakage index, the modified plastic work and the reference critical state void ratio. Relating these two equations with the function of CSL, a double-yield surface model accounting for the influence of particle crushing has been proposed.

Triaxial tests on Cambria sand were used to validate the proposed model. The model parameters can be easily determined from one isotropic compression test and several drained compression tests. Using determined parameters, different tests including drained tests in compression and extension, undrained tests in compression and extension were simulated by the proposed model. The grain size distributions for all tests were also predicted. All comparisons between experiments and simulations demonstrate that the model can accurately describe the mechanical behavior of granular materials with particle crushing, as well as the evolution of grain size distribution during loading.

  Eq. (11) suggests that the dense packing has smaller phase transformation angle than the loose packing, which results in the same effect than the one formulated by Muir[START_REF] Muir Wood | Particle crushing and deformation behaviour[END_REF].

  (b) from which a hyperbolic curve is raised as follows:

Figure 1 .

 1 Figure 1. Particle crushing effect: (a) Evolution of breakage index versus modified plastic work, and (b) Evolution of reference critical state void ratio versus breakage index

Figure 2 .

 2 Figure 2. Parametric study for particle crushing related parameters: (a) for isotropic compression test and (b)-(c) deviatoric stress and volumetric strain versus major principle strain respectively for drained compression test with constant confining stress of 26MPa

Figure 3 .

 3 Figure 3. Comparisons between experimental data and simulations for drained triaxial compression tests: (a-c) deviatoric stress versus major principle strain; (b-d) volumetric strain versus major principle strain

Figure 4 .

 4 Figure 4. Comparisons between experimental results and simulations for drained triaxial extension tests: (a) deviatoric stress versus major principle strain, and (b) volumetric strain versus major principle strain

Table 1 .

 1 Values of the constitutive parameters for Cambria sand specimens.


Emmanuel Hainry
email: hainry@loria.fr

Romain Péchoux
email: pechoux@loria.fr

Higher-order interpretations for higher-order complexity

We design an interpretation-based theory of higher-order functions that is well-suited for the complexity analysis of a standard higher-order functional language à la ml. We manage to express the interpretation of a given program in terms of a least fixpoint and we show that when restricted to functions bounded by higher-order polynomials, they characterize exactly classes of tractable functions known as Basic Feasible Functions at any order.

Introduction

The study of program higher-order properties remains a challenging and open issue in computer science. For example, Church-Turing's thesis does not hold at higher order and there are no complexity equivalences between computational models at higher order. As a consequence, several distinct and most of the time incomparable classes are candidate for the notion of polynomial time computation at higher order. Two of the most common definitions are the class of polynomially computable real functions by Ker-I Ko [START_REF] Ker | Complexity Theory of Real Functions[END_REF] defined for first-order functions over real numbers (that can be seen as order 2 functions over natural numbers) using machines and that was extended by Cook and Kawamura for functions at any order [START_REF] Kawamura | Complexity theory for operators in analysis[END_REF], and the class of Basic Feasible Functional (bff i ) at order i by Irwin, Kapron and Royer [START_REF] Irwin | On characterizations of the basic feasible functionals (part II)[END_REF].

As highlighted by Férée in his PhD manuscript [START_REF] Férée | Complexité d'ordre supérieur et analyse récursive[END_REF], the classes bff i cannot capture some functions that can be considered to be polynomial time computable because they suffer from not accounting for the size of their higher-order arguments. However they have been demonstrated to be robust, they characterize exactly the well-known classes fptime and bff at order 1 and order 2, and have already been characterized in various ways, e.g. [START_REF] Cook | Characterizations of the basic feasible functionals of finite type[END_REF]. An important argument in favor of the bff i classes is that they offer the only programming language-based alternative (BTLP, ITLP, ... -see [START_REF] Irwin | On characterizations of the basic feasible functionals (part II)[END_REF] for an overview) for characterizing higher-order complexity. One could argue that natural programs are hard to represent in such languages unless artificial size bounds are provided. This is indeed an important issue that is solved by the present work which will separate the language, a standard higher-order language à la ml, from the size bounds, provided by static analysis.

For that purpose, we develop a theory of higher-order interpretations. These interpretations are an extension of usual (polynomial) interpretation methods used to show the termination of programs [START_REF] Manna | On the termination of Markov algorithms[END_REF][START_REF] Lankford | On proving term rewriting systems are noetherian[END_REF]. However this theory is a novel and uniform extension to higher-order functional programs: the definition works at any order on a simple programming language and no extra constraints are required. The only restriction lies in the reduction strategy that is enforced to be left-most outermost as our language includes operators with non-strict interpretations that could break some of the system properties if a reduction occurs under a context. We also show that these interpretations can be elegantly expressed in terms of a least fixpoint. To our knowledge, there are only two interesting lines of work that are related to our approach. In [START_REF] Van De Pol | Termination proofs for higher-order rewrite systems[END_REF], Van De Pol introduced higher-order interpretation for showing the termination of term rewrite systems. In [START_REF] Baillot | Higher-order interpretations and program complexity[END_REF], Baillot and Dal Lago introduce higher-order interpretations for complexity analysis of term rewrite systems. These two studies are restricted to variant of higher-order term rewrite systems whereas the current work applies to a functional language. While [START_REF] Van De Pol | Termination proofs for higher-order rewrite systems[END_REF] only deals with termination properties, [START_REF] Baillot | Higher-order interpretations and program complexity[END_REF] is restricted to first-order complexity in contrast, our work characterizes higher-order complexity classes. Moreover [START_REF] Baillot | Higher-order interpretations and program complexity[END_REF] uses linear typing based extra information on functions to be applied to defunctionalized higher-order terms whereas we illustrate with an example in Section 6 that our methodology can be applied homogeneously to such a case with no need of extra or external analysis.

After defining the functional language, we present the new notion of higher-order interpretation and its properties. Next, we briefly recall the bff i classes and their main characterizations, including a characterization based on the BTLP programming language of [START_REF] Irwin | On characterizations of the basic feasible functionals (part II)[END_REF]. We then demonstrate a characterization of these classes using higher-order polynomials: The soundness relies on interpretation properties: the reduction length is bounded by the interpretation of the initial term. The completeness is demonstrated by simulating a BTLP procedure, performing a compilation from procedures to terms after some program transformations. In the last section of the paper, we briefly discuss expressivity issues, the synthesis problem and possible extensions to polynomial space.

Functional language

Syntax. The language considered in this paper consists in a lambda calculus with constructors, primitive operators, a case construct for pattern matching and a letRec instruction for (recursive) function definitions. It can be seen as an extension of PCF to inductive data types. A term of our language is defined by the following syntax:

M, N ::= x | c | op | M N | λx.M | letRec f = M | case M of c 1 ( - → x 1 ) → M 1 |...|c n ( -→ x n ) → M n
In the above syntax, c, c 1 , • • • , c n are constructor symbols of fixed arity and op is an operator of fixed arity. Given a constructor or operator symbol b, we write ar(b) = n whenever b is of arity n. Let x, f be variables of a fixed set X and -→ x i be a sequence of ar(c i ) variables. The free variables F V (M) of a term M are defined as usual.

For simplicity, we will assume that bound variables have distinct names in order to avoid name clashes. Finally, a closed term will consists in a term M such that F V (M) = ∅ (i.e. with no free variables). A substitution

{N 1 /x 1 , • • • , N n /x n } is a partial function mapping variables x 1 , • • • , x n to terms N 1 , • • • , N n .
As usual, the result of applying the capture-free substitution Semantics. The semantics of our language is described by a relation → S between two terms defined by

{N 1 /x 1 , • • • , N n /x n } to a term M is denoted M{N 1 /x 1 , • • • , N n /x n } or M{ - → N / - → x }
→ S =→ β ∪ → case ∪ → op ∪ → letRec • → β is the standard β-reduction defined by: λx.M N → β M{N/x},
• → case corresponds to pattern matching and is defined by:

case c j ( - → N j ) of . . . | c j ( - → x j ) → M j | . . . → case M j { - → N j / - → x j },
• → letRec is a fixpoint evaluation defined by:

letRec f = M → letRec M{letRec f = M/f},
• → op is an operator evaluation defined by:

op M 1 . . . M n → op M,
provided that op is a primitive operator of arity n whose semantics op , fixed by the language implementation, is a total function that satisfies op (M 1 , . . . , M n ) = M.

In the particular case, where the pattern matching on the case first argument fails (i.e. ¬∃j, M = c j ( -→ N j )), we extend the relation → α , α ∈ {β, case, letRec, op}, by:

if M → α N then case M of . . . → α case N of . . . .
In what follows, we will fix a left-most outermost evaluation strategy with respect to → {β,case,letRec,op} , noted ⇒. Let ⇒ k be the k-fold self-composition of the relation ⇒ with respect to such a strategy. Moreover, let |M ⇒ k N| be the number of reductions distinct from → op in a given a derivation M ⇒ k N. |M ⇒ k N| ≤ k always holds. M is a notation for the term computed by M (if it exists), i.e. ∃k, M ⇒ k M and ∃N, M ⇒ N. A (first-order) value v is defined inductively by either In what follows, we will consider only well-typed terms. The type system assigns types to all the syntactic constructions of the language and ensures that a program does not go wrong. Notice that the typing discipline does not prevent a program from diverging. The type system is described in Figure 1 and proves judgments of the shape Γ; ∆ M :: T meaning that the term M has type T under the variable and constructor (and operator) symbol contexts Γ and ∆ respectively ; a variable (a constructor or operator symbol) context being a partial function that assigns types to variables (respectively constructors or operators). As usual, the input type and output type of constructors and operators of arity n will be restricted to basic types. Consequently, their types are of the shape b 1 -→ . . . -→ b n -→ b. A well-typed term will consist in a term M such that ∅; ∆ M :: T (Consequently, it is mandatory for a term to be closed in order to be well-typed).

v = c, if ar(c) = 0, or v = c - → v , for ar(c) > 0 values - → v , otherwise.
Definition 1 (Order). Given a term M of type T, i.e. ∅; ∆ M :: T, the order of M, denoted ord(M), is equal to the order of T, denoted ord(T) and defined inductively by:

ord(b) = 0, if b ∈ B, ord(T -→ T ) = max(ord(T) + 1, ord(T )) otherwise.
Example 1. Consider the following term M that maps a function to a list given as inputs:

letRec f = λg.λx.case x of c(y, z) → c(g y)(f g z) | nil → nil
Suppose that [Nat] is the base type for lists of natural numbers of constructor set

C [Nat] = {nil, c}. The term M can be typed by (Nat -→ Nat) -→ [Nat] -→ [Nat]. Consequently, ord(M) = 2. Γ(x) = T Γ; ∆ x :: T (Var) ∆(c) = T Γ; ∆ c :: T (Cons) ∆(op) = T Γ; ∆ op :: T (Op) Γ; ∆ M :: T 1 -→ T 2 Γ; ∆ N :: T 1 Γ; ∆ M N :: T 2 (App) Γ, x :: T 1 ; ∆ M :: T 2 Γ; ∆ λx.M :: T 1 → T 2 (Abs) Γ, f :: T; ∆ M :: T Γ; ∆ letRec f = M :: T (Let) Γ; ∆ M :: b Γ; ∆ c i :: - → b i -→ b Γ, - → x i :: - → b i ; ∆ M i :: T (1 ≤ i ≤ n) Γ; ∆ case M of c 1 ( - → x 1 ) → M 1 |...|c n ( -→ x n ) → M n :: T (Case)

Interpretations

In this section, we define the interpretation tools that will allow us to control the complexity of closed terms of our language.

Interpretations of types

We briefly recall some basic definitions that are very close to the notions used in denotational semantics (See [START_REF] Winskel | The formal semantics of programming languages: an introduction[END_REF]) since, as we shall see later, our notion of interpretation also allows us to obtain fixpoints. Let (N, ≤, , ) be the set of natural numbers equipped with the usual ordering ≤, a max operator and min operator and let N be N ∪ { }, where ∀n ∈ N, n ≤ , n = n = and n = n = n. The strict order relation over natural numbers < will also be used in the sequel and is extended in a somewhat unusual manner, by < .

The interpretation of a type is defined inductively by:

b = N, if b is a basic type, T -→ T = T -→ ↑ T , otherwise,
where T -→ ↑ T denotes the set of total strictly monotonic functions from T to T . A function F from the set A to the set B being strictly monotonic if for each

X, Y ∈ A, X < A Y implies F (X) < B F (Y )
, where < A is the usual pointwise ordering induced by < and defined by:

n < N m iff n < m F < A-→ ↑ B G iff ∀X ∈ A, F (X) < B G(X) Example 2. The type T = (Nat -→ Nat) -→ [Nat] -→ [Nat] of the term letRec f = M in Example 1 is interpreted by: T = (N -→ ↑ N) -→ ↑ (N -→ ↑ N).
In what follows, given a sequence -→ R of m terms in the interpretation domain and a sequence -→ T of k types, the notation

- → R ∈ -→ T means that both k = m and ∀i ∈ [1, m], R i ∈ T i .

Interpretations of terms

Each closed term of type T will be interpreted by a functional in T . The application is denoted as usual whereas we use the notation Λ for abstraction on this function space in order to avoid confusion between terms of our calculus and objects of the interpretation domain. Variables in the interpretation domain will be denoted using upper case letters. Moreover, we will sometimes use Church typing discipline in order to highlight the type of the bound variable in a lambda abstraction.

An important distinction between the terms of our language and the objects of the interpretation domain lies in the fact that beta-reduction is considered as an equivalence relation on (closed terms of) the interpretation domain, i.e. (ΛX.F ) G = F {G/X} underlying that (ΛX.F ) G and F {G/X} are distinct notations that represent the same higher-order function. The same property holds for η-reduction, i.e. ΛX.(F X) and F denote the same function. In other words, closed terms of the application domain are considered as extensional objects whereas terms of the language are considered as intensional objects.

Since we are interested in complete lattices, we need to complete each type T by a lower bound ⊥ T and an upper bound T as follows:

⊥ N = 0 N = ⊥ T-→T = ΛX T .⊥ T T-→T = ΛX T .
T We can show by an easy structural induction on types that for each

F ∈ T , ⊥ T ≤ T F ≤ T T .
Notice that for each type T it also holds that T < T T , by an easy induction. In the same spirit, we extend inductively the max and min operators (and ) over N to arbitrary higher-order functions F, G of type T -→ ↑ T by:

T -→ ↑ T (F, G) = ΛX T . T (F (X), G(X)) T -→ ↑ T (F, G) = ΛX T . T (F (X), G(X))
In the following, we use the notations ⊥, , ≤, <, and instead of ⊥ T , T , ≤ T , < T , T and T , respectively, when T is clear from the typing context.

Lemma 1. For each type T, ( T , ≤, , , , ⊥) is a complete lattice.

Proof. Consider a subset S of elements in T and define S = F ∈S F . By definition, we have F ≤ S, for any F ∈ S. Now consider some G such that for all F ∈ S, F ≤ G. We have for all

F ∈ S, F (X) ≤ G(X). Consequently, ∀X, S(X) = F ∈S F (X) ≤ G(X)
and S is a supremum. The same holds for the infimum. Now we need to define a unit (or constant) cost function for any interpretation of type T in order to take the cost of recursive calls into account. For that purpose, let + denote natural number addition extended to N by ∀n,

+ n = n + = .
For each type T , we define inductively a dyadic sum function ⊕ T by:

X N ⊕ N Y N = X + Y F ⊕ T-→T G = ΛX T .(F (X) ⊕ T G(X))
Let us also define the constant function n T , for each type T and each integer n ≥ 1, by: Once again, we will omit the type when it is unambiguous using the notation n⊕ to denote the function n T ⊕ T when T is clear from the typing context. We have the following result:

n N = n n T-→T = ΛX T .n T • f ρ = ρ(f), if f ∈ X , • c ρ = 1 ⊕ (ΛX 1 . . . . .ΛX n . n i=1 X i ), if ar(c) = n, • MN ρ = M ρ N ρ , • λx.M ρ = 1 ⊕ (Λ x ρ . M ρ ), • case M of c 1 ( - → x 1 ) → M 1 |...|c n ( -→ x n ) → M n ρ = 1 ⊕ 1≤i≤n { M i ρ { -→ R i / --→ x i ρ } | ∀ -→ R i s.t. M ρ ≥ c i ρ -→ R i }, • letRec f = M ρ = {F ∈ T | F ≥ 1 ⊕ (Λ f ρ . M ρ )F }.
Lemma 2. For all F , F < 1 ⊕ F .
Proof. By induction on the strict order < T . For the base case, we have

n < N 1 N ⊕ N n = n + 1.
Suppose it holds for any order ≤ k and take an order k + 1 function F of type T -→ T . For all X of type T, we have that F X < T 1 T ⊕ T F X, by Induction Hypothesis. Consequently F = ΛX.F X < T→T ΛX.1 T ⊕ T F X = 1 T→T ⊕ T→T F . Now we are ready to define the notions of variable assignment and interpretation of a term M: Definition 2 (Interpretation). A variable assignment, denoted ρ, is a map associating to each f ∈ X of type T a variable F of type T . Given a variable assignment ρ, an interpretation is the extension of ρ to well-typed terms, mapping each term of type T to an object in T and defined in Figure 2, where op ρ is a sup-interpretation, i.e. a total function such that:

∀M 1 , . . . , ∀M n , op M 1 . . . M n ρ ≥ op (M 1 , . . . , M n ) ρ .
See [START_REF] Péchoux | Synthesis of sup-interpretations: a survey[END_REF] for more details about sup-interpretations. As operator sup-interpretations are fixed, an interpretations should also be indexed by some mapping m assigning a sup-interpretation to each operator of the language. To simplify the formalism, we will omit this mapping in what follows.

Notice that, contrarily to other program constructs, operators may have non monotonic interpretations. This is the reason why we have fixed a left-most outermost strategy (we never reduce the operator operands) and operators are supposed to be total functions.

Existence of an interpretation

The interpretation of a term is always defined. Indeed, in Definition 2, letRec f = M ρ is defined in terms of the least fixpoint of the function ΛX T .1 ⊕ T ((Λ f ρ . M ρ ) X) and, consequently, we obtain the following result as a direct consequence of Knaster-Tarski [START_REF] Tarski | A lattice-theoretical fixpoint theorem and its applications[END_REF][START_REF] Kirk | Handbook of metric fixed point theory[END_REF] Fixpoint Theorem: Proposition 1. Each term M of type T has an interpretation.

Proof. By Lemma 1, L = ( T , ≤, , , , ⊥) is a complete lattice. The function

F = ΛX T .1 ⊕ T ((Λ f ρ . M ρ )X) : L → L
is monotonic. Indeed, both constructor terms and letrec terms of type T are interpreted over a space of monotonic functions T . Moreover monotonicity is preserved by application, abstraction and the and operators. Applying Knaster-Tarski, we obtain that F admits a least fixpoint, which is exactly {X ∈ T | X ≥ F X}.

Intermediate lemmata

We now show intermediate lemmata by structural induction on terms Lemma 3. For all M, N, x such that x :: T; ∆ M :: T , ∅; ∆ N :: T, we have

M ρ { N ρ / x ρ } = M{N/x} ρ .
Lemma 4. For all M, N, x such that x :: T; ∆ M :: T , ∅; ∆ N ::

T, we have λx.M N ρ > M{N/x} ρ . Proof. λx.M N ρ = λx.M ρ N ρ By Definition 2 = Λ x ρ .1 ⊕ M ρ N ρ By Definition 2 = 1 ⊕ M ρ { N ρ / x ρ } By definition of = = 1 ⊕ M{N/x} ρ By Lemma 3 > M{N/x} ρ By Lemma 2
and so the conclusion.

Lemma 5. For all M, we have: if

M ⇒ N then M ρ ≥ N ρ . Moreover if |M ⇒ N| = 1 then M ρ > N ρ . Proof. If |M ⇒ N| = 0 then M = op M 1 . . . M n → op op (M 1 , . . . , M n ) = N,
for some operator op and terms M 1 , . . . , M n and consequently, by Definition of interpretations we have op M 1 . . .

M n ρ ≥ op (M 1 , . . . , M n ) ρ .
If |M ⇒ N| = 1 then the reduction does not involve a → op (i.e. an operator evaluation). By Lemma 4, in the case of a β-reduction and, by induction, Lemmata 3 and 2 and Definition 2 for the other cases. e.g. For a letrec reduction, we have: if The first inequality holds since we are only considering higher-order functions F satisfying F ≥ 1 ⊕ (Λ f ρ . N ρ )F . The second inequality holds because Λ f ρ . N ρ is a monotonic function (as the interpretation domain only consists of such functions).

M = letRec f = M → letRec M {M/f} = N then: M ρ = {F ∈ T | F ≥ 1 ⊕ (Λ f ρ . N ρ )F } ≥ {1 ⊕ Λ f ρ . N ρ F | F ≥ 1 ⊕ (Λ f ρ . N ρ )F } ≥ 1 ⊕ Λ f ρ . N ρ {F | F ≥ 1 ⊕ (Λ f ρ . N ρ )F } = 1 ⊕ (Λ f ρ . N ρ ) M ρ = 1 ⊕ N ρ { M ρ / f ρ } = 1 ⊕ N{M/f} ρ , by Lemma 3 > N{M/f} ρ , by Lemma 2 M ρ = {F ∈ T | F ≥ 1 ⊕ (Λ f ρ . λx.case x of +1(y) → +1(+1(f y))| 0 → 0 ρ )F } = {F ∈ T | F ≥ 2 ⊕ ((Λ f ρ .Λ x ρ . case x of +1(y) → +1(+1(f y))| 0 → 0 ρ )F )} = {F ∈ T | F ≥ 3 ⊕ ((Λ f ρ .Λ x ρ .( x ρ ≥ +1(y) ρ +1(+1(f y)) ρ ) ( x ρ ≥ 0 ρ 0 ρ ))F )} = {F ∈ T | F ≥ 3 ⊕ ((Λ f ρ .Λ x ρ .( x ρ ≥1⊕ y ρ 2 ⊕ ( f ρ y ρ )) ( x ρ ≥1 1))F )} = {F ∈ T | F ≥ 3 ⊕ (Λ x ρ .( x ρ ≥1⊕ y ρ 2 ⊕ (F y ρ )) (1))} = {F ∈ T | F ≥ 3 ⊕ (Λ x ρ .(2 ⊕ (F ( x ρ -1))) (1))}, x ρ -1 ≥ 0 = {F ∈ T | F ≥ ΛX.(5 ⊕ (F (X -1))) (4)} = ΛX.5X + 4
Corollary 1. For all terms, M, - → N , such that ∅; ∆ M - → N :: T, if M - → N ⇒ k M then M ρ - → N ρ ≥ |M - → N ⇒ k M | ⊕ M ρ .
As basic operators can be considered as constant time computable objects the following Corollary also holds:

letRec f = λx.case x of +1(y) → +1(+1(f y)) | 0 → 0
We can see in Figure 3 how the interpretation rules of Figure 2 are applied on such a term. At the end we search for the minimal strictly monotonic function F greater than ΛX.(5 ⊕ (F (X -1))) 4, for X > 1. That is ΛX.5X ⊕ 4. Notice that such an interpretation is not tight as one should have expected the interpretation of such a program to be ΛX.2X ⊕ k for some constant k. This interpretation underlies that each iteration step, distinct from the base case, counts for 5 (1 for the recursive call, 1 for the application, 1 for pattern matching and 2 for the extraconstructors added) and the base case counts for 4 (letrec call, application, pattern matching and one constructor). Consequently, we have a bound on both size of terms and reduction length though this upper bound is not that accurate. This is not that surprising as this technique suffers from the same issues as methods based on first-order interpretations.

Relaxing interpretations

For a given program it is somewhat difficult to find an interpretation that can be expressed in an easy way. This difficulty lies in the homogeneous definition of the considered interpretations using a max (for the case construct) and a min (for the letrec construct). Indeed, it is sometimes difficult to eliminate the constraint (parameters) of a max generated by the interpretation of a case. Moreover, it is a hard task to find the fixpoint of the interpretation of a letrec. All this can be relaxed as follows:

• finding an upper-bound of the max by eliminating constraint in the case construct interpretation,

• taking a particular function satisfying the inequality in the letrec construct interpretation.

In both cases, we will no longer compute an exact interpretation of the term but rather an upper bound of the interpretation.

Lemma 7. Given a set of functions S and a function F ∈ S, the following inequality always holds F ≥ {G|G ∈ S}.

This relaxation is highly desirable in order to find "lighter" upper-bounds on the interpretation of a term. Moreover, it is a reasonable approximation as we are interested in worst case complexity.

Obviously, it is possible by relaxing too much to attain the interpretation T , which gives nothing interesting. We can see in the first four lines of Figure 4 how the interpretation rules of Figure 2 are applied on such a term. In the penultimate line, we obtain an upper-bound on the interpretation by approximating the case interpretation, substituting x ρ -1 to both y ρ and z ρ . This is the first step of relaxation where we find an upper bound for the max. The inequality:

a = x ρ≥1⊕ y ρ + z) ρ F ( y ρ , z ρ ) ≤ x ρ ≥1⊕ y ρ, x ρ ≥1⊕ z) ρ F ( y ρ , z ρ ) = b holds for any monotonic function F . Consequently, {F | F ≥ b} ≤ {F | F ≥ a}.
In the last line, we obtain an upper-bound on the interpretation by approximating the letrec interpretation, just checking that the function Λ g ρ .Λ x ρ .(5 ⊕ ( g ρ x ρ )) × x ρ , where × is the usual multiplication symbol over natural numbers, satisfies the inequality

F ≥ 5 ⊕ (Λ g ρ .Λ x ρ .(( g ρ ( x ρ -1)) + (F g ρ ( x ρ -1)))).

Higher-Order Polynomial Interpretations

At the present time, the interpretation of a term of type T can be any total functional over T . In the next section, we will concentrate our efforts to study polynomial time at higher order. Consequently, we need to restrict the shape of the admissible interpretations. For that purpose, we introduce higher-order polynomials which are the higher-order counterpart to polynomials in this theory of complexity. Let P i denote a polynomial of order i and let X i denote an order i variable. Higher-order (order 1 and order i+1) polynomials can be defined by the following grammar:

M ρ = {F ∈ T | F ≥ 1 ⊕ (Λ f ρ . λg.λx.case x of c(y, z) → c(g y)(f g z)| nil → nil ρ )F } = {F | F ≥ 3 ⊕ ((Λ f ρ .Λ g ρ .Λ x ρ . case x of c(y, z) → c(g y)(f g z)| nil → nil ρ )F )} = {F | F ≥ 4 ⊕ ((Λ f ρ .Λ g ρ .Λ x ρ . ( nil ρ , x ρ ≥ c(y,z) ρ ( c(g y)(f g z) ρ )))F )} = {F | F ≥ 4 ⊕ ((Λ f ρ .Λ g ρ .Λ x ρ . (1, x ρ ≥1⊕ y ρ+ z) ρ (1 ⊕ ( g ρ y ρ ) + ( f ρ g ρ z ρ ))))F )} = {F | F ≥ 5 ⊕ (Λ g ρ .Λ x ρ . x ρ ≥1⊕ y ρ + z) ρ (( g ρ y ρ ) + (F g ρ z ρ )))} ≤ {F | F ≥ 5 ⊕ (Λ g ρ .Λ x ρ .(( g ρ ( x ρ -1)) + (F g ρ ( x ρ -1))))} ≤ Λ g ρ .Λ x ρ .(5 ⊕ ( g ρ x ρ )) × x ρ
P 1 ::= c|X 0 |P 1 + P 1 |P 1 × P 1 P i+1 ::= P i |P i+1 + P i+1 |P i+1 × P i+1 |X i (P i+1 )
where c represents constants in N.

Clearly, the set of order i polynomials is strictly included in the set of order i+1 polynomials by the above definition. Moreover, by definition, a higher-order polynomial P i+1 has variables of order at most i. If -→ X is the sequence of such variables ordered by decreasing order, we will treat the polynomial P i+1 as total functions Λ -→ X .P i+1 ( -→ X ). We are now ready to define the class of functions computed by terms admitting an interpretation that is (higher-order) polynomially bounded: Definition 4. Let fp i , i > 0, be the class of polynomial functionals at order i that consist in functionals computed by closed terms M over the basic type C Nat and such that:

• ord(M) = i
• M ρ is bounded by an order i polynomial (i.e. ∃P i , M ρ ≤ P i ).

Safe Feasible Functionals

The class of tractable type 2 functionals has been introduced by Constable [3] and Mehlhorn [START_REF] Mehlhorn | Polynomial and abstract subrecursive classes[END_REF]. It was later named bff for the class of Basic Feasible Functionals and characterized in terms of function algebra [START_REF] Cook | Characterizations of the basic feasible functionals of finite type[END_REF][START_REF] Irwin | On characterizations of the basic feasible functionals (part I)[END_REF]. We choose to define the class through a characterization by Bounded Typed Loop Programs from [START_REF] Irwin | On characterizations of the basic feasible functionals (part II)[END_REF] which extends the original bff to any order.

Basic Feasible Functionals and Bounded Typed Loop Programs

Definition 5 (BTLP). A Bounded Typed Loop Program (BTLP) is a non-recursive and wellformed procedure defined by the grammar of Figure 5.

::= v D := E; | Loop v D 0 with v D 1 do {I * } (Expressions) E ::= 1 | v D | v D 0 + v D 1 | v D 0 -v D 1 | v D 0 #v D 1 | v τ1×...×τn→D (A τ1 1 , . . . , A τn n ) (Arguments) A ::= v | λv 1 , . . . , v n .v(v 1 . . . , v m ) with v / ∈ {v 1 , . . . , v n } Figure 5: BTLP grammar
The well-formedness assumption is given by the following constraints: Each procedure is supposed to be well-typed with respect to simple types over D, the set of natural numbers of dyadic representation over {0, 1} (0 ≡ , 1 ≡ 0, 2 ≡ 1, 3 ≡ 00, . . .). When needed, types are explicitly mentioned in variables' superscript. Each variable of a BTLP procedure is bound by either the procedure declaration parameter list, a local variable declaration or a lambda abstraction. In a loop statement, the guard variables v 0 and v 1 cannot be assigned to within I * . In what follows v 1 will be called the loop bound.

The operational semantics of BTLP procedures is standard: parameters are passed by callby-value. +, -and # denote addition, proper subtraction and smash function (i.e. x#y = 2 |x|×|y| , the size |x| of the number x being the size of its dyadic representation), respectively. Each loop statement is evaluated by iterating |v 0 |-many times the loop body instruction under the following restriction: if an assignment v := E is to be executed within the loop body, we check if the value obtained by evaluating E is of size smaller than the size of the loop bound |v 1 |. If not then the result of evaluating this assignment is to assign 0 to v.

We are now ready to provide a definition of Basic Feasible Functionals at any order:

Definition 6 (bff i ). For any i ≥ 1, bff i is the class of order i functionals computable by a BTLP procedure1 .

It is straightforward that bff 1 = FPtime (the class of first-order polynomial time computable functions) and bff 2 =bff.

Safe Feasible Functionals

Now we restrict the domain of bff i classes to inputs in bff k for k < i, the obtained classes are named sff for Safe Feasible Functionals.

Definition 7 (sff i ). sff 1 is defined to be the class of order 1 functionals computable by BTLP a procedure and, for any i ≥ 1, sff i+1 is the class of order i + 1 functionals computable by BTLP a procedure on the input domain sff i . In other words,

sff 1 =bff 1 , ∀i ≥ 1, sff i+1 =bff i+1 sffi
This is not a huge restriction since we want an arbitrary term of a given complexity class at order i to compute over terms that are already in classes of the same family at order k, for k < i. Consequently, programs can be built in a constructive way component by component. Another strong argument in favor of this domain restriction is that the partial evaluation of a functional at order i will, at the end, provide a function in N -→ N that is shown to be in bff 1 (=FPtime).

A characterization of Safe Feasible Functionals of any order

Theorem 1. For any order i ≥ 1, the class of functions in fp i over fp k , k < i, is exactly the class of functionals in sff i . In other words,

sff i ≡ fp i (∪ k≤i fp k ) , for all i ≥ 1.
Proof. This Theorem is proved by induction on the order. For any order i, it can be split in two directions called Soundness(i) and Completeness(i):

• Soundness(i): Any term M whose interpretation is bounded by an order i polynomial, computes a function in sff i .

• Completeness(i): Any BTLP procedure P of order i can be encoded by a term M computing the same function and admitting a polynomial interpretation of order i.

We start to show that Soundness(1) holds. Consider that the term M has an interpretation bounded by a polynomial P 1 . For any value v, we have, by Corollary 1, that the computing time of M on input v bounded by M v ρ . Consequently, using Lemma 6, we have that:

M v ρ = M ρ v ρ = M ρ (|v|) ≤ P 1 (|v|).
Hence M belongs to FPtime = sff 1 . Completeness(1) holds as a direct consequence of Theorem 4 of [START_REF] Bonfante | Algorithms with polynomial interpretation termination proof[END_REF] showing the completeness of polynomial interpretations of Kind(0) for confluent TRS with respect to the complexity class FPtime. Kind(0) means that constructor symbol interpretations are enforced to be linear functions of the shape Σ n i=1 X i + α, α ≥ 1. Just notice that interpretations in our framework are of Kind(0) and that each term rewrite rule admitting an interpretation can be encoded easily into an equivalent term of order 1 admitting an interpretation (up to some additive constant). Now, we suppose that Soundness(k) and Completeness(k) hold for any k ≤ i. Let M be an order i + 1 term of interpretation M ρ bounded by the order i + 1 polynomial P i+1 , i.e. M ρ ≤ P i+1 . We know that on input N, M normalizes in O( M N ρ ), by Corollary 1. Since N computes a functional N ∈ sff i , by induction (Completeness(i)) there is a polynomial P i such that N ρ ≤ P i . Consequently, we obtain that the maximal number of reduction steps is bounded polynomially in the input size by:

M N ρ = M ρ N ρ ≤ P i+1 • P i
that is, by a polynomial Q i+1 of order i + 1 defined by Q i+1 = P i+1 • P i . Consequently, Soundness(i + 1) holds. For Completeness(i + 1), we demonstrate using program transformations that any loop can be encoded by a first-order term whose runtime remains polynomial in the input size. For that purpose, we proceed in two steps:

1. first, we transform each BTLP procedure into a standard loop-based higher-order imperative procedure with explicit bounds, no nested loops and no procedure call. Instead of being checked dynamically the "with v D 1 " bound is performed using a local chkbd operator functional term. For that purpose, we suppose that the target term language includes constructors for dyadic numbers ( , 0 and 1), a constructor for tuples . . . , all the imperative operators as basic prefix operators (+, -, #, . . .), min operators D n computing the min of the sizes of n dyadic numbers and a chkbd operator of arity 2 such that chkbd(M, N) = M if | M | ≤ | N | (and otherwise). All these operators are extended to be total functions in the term language: they return on input terms for which they are undefined. Moreover, we also require that each procedure given as input is alpha renamed so that all parameters and local variables of a given procedure have the same name and are indexed by natural numbers. The compiling process is described in Figure 8, defining comp, comi n , come that respectively compile procedures, instructions and expressions. The comi compiling process is indexed by the number of variables in the program n. For notational convenience, let λ v 1 , . . . , v n . be a shorthand notation for λs.case s of v 1 , . . . , v n → and let π n r be a shorthand notation for the r-th projection λ v 1 , . . . , v n .v r . The compilation procedure works as follows:

• Any loop-based procedure of the shape v(v 1 , . . . , v m ) Var v m+1 , . . . , v n ; I * Return v r will be transformed into a term of type τ 1 × . . . × τ n → τ r , provided that τ i is the type of v i and that τ 1 × . . . × τ n is the type for n-ary tuples of the shape v 1 , . . . , v n . • Each instruction within a procedure of type τ 1 × . . . × τ n → τ r will have type τ 1 × . . . × τ n → τ 1 ×. . .×τ n . Consequently, two sequential instructions I 1 I 2 within a procedure of n variables will be compiled into a term application of the shape comi n (I 2 ) comi n (I 1 ) and instruction type is preserved by composition. • For loop compilation, we make use of a letrec of type

D → τ 1 × . . . × τ n → τ 1 × . . . × τ n .
The first argument is a counter and is fed with a copy of the loop counter v i so that the obtained term has the expected type τ 1 × . . . × τ n → τ 1 × . . . × τ n . Notice that this compilation preserves both the semantics and its asymptotic complexity of the initial BTLP procedure.

Finally, we have transformed a BTLP procedure into a term preserving the semantics and the asymptotic complexity (reduction length). Moreover, each higher-order expression in a tuple can be encoded by a first-order term using defunctionalization and we let the reader check that the operators in {+, -, #, ×, cut, D n , chkbd} admit the following polynomial supinterpretations

+ ρ = ΛX.ΛY.X + Y, -ρ = ΛX.ΛY.X, # ρ = ΛX.ΛY.X × Y, × ρ = ΛX.ΛY.X + Y, cut ρ = ΛX. (X -1, 0), D n ρ = ΛX 1 . . . . .ΛX n . N (X 1 , . . . , X n ),
f = λ t.λs.case t of → s j(t) → f t (comi n (I * ) s) vi) comi n (if v D i { I * 1 } else { I * 2 }) = λ v1, . . . , vn .case vi of → comi n (I * 2 ) | j(t) → comi n (I * 1 ) with j ∈ {0, 1} come(c) = c, c ∈ {1, v D } come(v D 0 op v D 1 ) = op v0 v1, op ∈ {+, -, #, ×} come(cut(v D )) = cut v come(chkbd(E, {vj 1 , . . . , vjr})) = chkbd come(E) ( D r vj 1 . . . vj r ) come(v(A1, . . . , An)) = v come(A1) . . . come(An) come(λv1, . . . , vn.v(v 1 . . . , v m )) = λv1. . . . λvn.(. . . (v v 1 ) . . . v m ) . . .)

Results and perspectives

In this paper, we have introduced a theory for higher-order interpretations that can be used to deal with higher-order complexity classes. This is a novel approach but there are still some important issues to discuss.

• Expressivity: the expressivity of interpretations is as usual their main drawback: As for first-order interpretations, a lot of interesting terms computing polynomial time functions will not have any polynomial interpretation, i.e. its interpretation will sometimes be , although the function will be computed by another algorithm (term) admitting a finite interpretation. It should be possible to relax the tool and to extend it to more complex data structures such as streams and infinite trees. At least, the presented paper has shown that the tool expressivity can be extended to higher order. Moreover, we manage to give a uniform framework for complexity analysis of exponential programs behaving polynomially. As an illustrative example, consider the term M by: letRec fold = λg.λx.case x of c(y, z) → g (fold g z)| nil → nil

The interpretation of M has to satisfy the following inequality:

{F | F ≥ ΛG.ΛX.4 ⊕ (1 ( X≥1 (G(F G (X -1))))}

Clearly, this inequality does not admit any polynomial interpretation as it is at least exponential in X. Now consider the term M (λx.1 + (1 + (x)). The term λx.1 + (1 + (x)) can be given the interpretation ΛX.X ⊕ 3. We have to find a function F such that F (ΛX.X ⊕ 3) ≥ ΛY.4 ⊕ (1 ( Y ≥1 (F (ΛX.X ⊕ 3) (Y -1)) ⊕ 3)). This inequality is satisfied by the function F such that F (ΛX.X ⊕ 3) Y = (7 × Y ) ⊕ 4 and consequently M has an interpretation. This highlights the fact that a term may have an interpretation even if some of its subterms might not have any. As expected, any term admitting an interpretation of the shape ΛX.X ⊕ β, for some constant β, will have an interpretation when applied as first operand of this fold function.

• Synthesis: it has been well known for a long time that the synthesis problem that consists in finding the sup-interpretation of a given term is undecidable in general for first-order terms using interpretations over natural numbers (see [START_REF] Péchoux | Synthesis of sup-interpretations: a survey[END_REF] for a survey). As a consequence this problem is also undecidable for higher order. However it is also well-known that it will become decidable if programs are defunctionalized (up to a first-order term) using polynomial functions over real numbers.

• Space: space issues were not discussed in this paper as there is no theory for higher-order polynomial space. In analogy with the usual first-order theory, a suitable definition for higher-order space complexity classes could be to consider terminating terms admitting a nonstrict polynomial interpretation. By nonstrict, we mean, for example, that the last rule of Figure 2 can be replaced by:

letRec f = M ρ = 1 ⊕ {F ∈ T | F ≥ (Λ f ρ . M ρ )F }
Thus termination is lost as the term letRec f = f could be interpreted by 1 ⊕ ΛF.F . This is the reason why we need to restrict the class to terminating terms. However a result equivalent to Lemma 5 holds: we still keep a non-strict upper bound on the interpretation of any derived term.

  when the substituting terms are clear from the context.

  Type system. We fix a set B of basic inductive types b described by their constructor set C b . For example, the type of natural numbers Nat is described by C Nat = {0, +1}. The set of simple types is defined by T ::= b | T -→ T, with b ∈ B. As usual -→ associates to the right.

Figure 1 :

 1 Figure 1: Type system

Figure 2 :

 2 Figure 2: Interpretation of a term of type T

Figure 3 :

 3 Figure 3: Example of interpretation

Corollary 2 .Lemma 6 .Example 3 .

 263 For all terms, M, -→ N , such that ∅; ∆ M -→ N :: b, with b ∈ B, if M -→ N ρ = then M -→ N terminates in a number of reduction steps in O( M -→ N ρ ). The size |v| of a value v is defined by |c| = 1 and |M N| = |M| + |N|. For any value v, such that ∅; ∆ v :: b, with b ∈ B, we have v = |v|. Consider the following term M :: Nat -→ Nat computing the double of a unary number given as input:

Example 4 .

 4 Consider the term M of Example 1: letRec f = λg.λx.case x of c(y, z) → c(g y)(f g z) | nil → nil

Figure 4 :

 4 Figure 4: Example of interpretation

(

  Procedures) P ::= Procedure v τ1×...×τn→D (v τ1 1 , . . . , v τn n ) P * V I * Return v D r (Declarations) V ::= Var v D 1 , . . . , v D n ; (Instructions) I

  chkbd ρ = ΛX.ΛY.Y . By Completeness(1), there exists a term computing the same function and admitting a polynomial interpretation. Consider the following simple BTLP procedure as an illustrative example for the program transformation in the proof of Theorem 1: Procedure mult (x , y ) Var z , b ; z := ; b := x # y ; Loop x with b do { z := z + y ;} Return z The transformation process is easy as there is no procedure call and no nested loop and we obtain the following loop program: Procedure mult (x , y ) var z , b ; z := ; b := x # y ; loop x { z := chkbd ( z +y ,{ b });} Return z comp(Procedure v(v1, . . . , vm) Var vm+1, . . . , vn; I * Return vr) = λs.π n r (comi n (I * ) s) comi n (I1 . . . I k ) = comi n (I k ) . . . comi n (I1) comi n (vi := E; ) = λ v1, . . . , vn . v1, . . . , vi-1, come(E), vi+1, . . . , vn comi n (loop vi {I * }) = λ v1, . . . , vn .( letRec

Figure 8 : 3 

 83 Figure 8: Compiler from loop programs to terms

As demonstrated in[START_REF] Irwin | On characterizations of the basic feasible functionals (part II)[END_REF], all types in the procedure can be restricted to be of order at most i without any distinction.

Acknowledgments. The authors would like to thank the anonymous reviewers for their comments and suggestions to improve this paper.

BTLP

in sff 1 provided that the input E is computable in polynomial time and whose semantics is defined by:

where E is the dyadic number obtained after the evaluation of expression E and X is a finite set of variables. For example, Loop x with w do {y := y + z; } is transformed into loop x{y := chkbd(y + z, {w}); }. Figures 6 and7 present some translations to get rid of, respectively, nested loops and sequential loops. They use the same operators as BTLP (in particular #), but also standard multiplication ×. They also use a new cut operator that is defined as removing the first character of its argument. Last, the notation (I) v which propagates to all assignments in I translating them using chkbd such as x := E (resp. x := chkbd(E, X)) being translated into x := chkbd(E, {v}) (resp.

x := chkbd(E, {v} ∪ X)). Procedure calls are eliminated by unfolding procedure bodies after a careful alpha-conversion. Nested loop elimination terminates as each application consumes one loop while unfolding terminates as there are no recursive calls by definition of BTLP. Notice that this program transformation preserves both the semantics and the asymptotic complexity of the initial BTLP procedure.

2. second, we compile each standard loop-based higher-order imperative procedure into a