B Durand

P Bailly

F Delvare

D Picart

A friction test between steel and a brittle material at high contact pressures and high sliding velocities

Our aim is to characterize the interface behaviour between an aggregate material and steel. This work focuses on contact pressures and sliding velocities reaching 100 MPa and 10 m/s. The set-up consists in a cylindrical sample of the aggregate material which slips into a steel tube. The tube is both a confinement vessel and a sliding surface. Thanks to confinement, the material can be tested under high stresses without failure. The interface pressure is generated by an axial compression. The sample is pressed on a spring, so it can be simultaneously compressed and rubbed on the tube. The set-up has been tested in the case of a quasi-static loading and the 100 MPa pressure has been reached. Then the set-up was mounted on a Split Hopkinson Pressure Bar device in order to reach higher velocities. Numerical simulations have been realized to check the feasibility and the relevance of this dynamic test. These results are analysed and compared to the experimental ones.

Introduction

The ignition of a plastic bonded explosive submitted to an impact depends strongly on the contact conditions at the boundaries. As a result, a perfect knowledge of the interface behaviour is necessary to predict exactly the evolution of such a set [START_REF] Picart | Ignition of a HMX-based PBX submitted to impact: strain localisation and boundary condition[END_REF][START_REF] Hoffman | Aspect of the tribology of the plastic bonded explosive LX-04[END_REF][START_REF] Dickson | Frictional Heating and Ignition of Energetic Materials[END_REF][START_REF] Gruau | Ignition of a confined high explosive under low velocity impact[END_REF]. The aim, to take up this challenge, is to design a device to study the friction between steel and an explosive under the conditions of an impact: contacts pressures and sliding velocities reaching respectively 100 MPa and 10 m/s.

A specific apparatus is required to simultaneously obtain high pressures and high velocities. Several techniques have been developed to measure friction coefficients under these conditions: explosively driven friction test [START_REF] Kim | Nanostructures generated by explosively driven friction: Experiments and molecular dynamics simulations[END_REF], plate impact [START_REF] Rajagopalan | Novel experimental techniques for investigating time resolved high speed friction[END_REF], torsional Kolsky bar set-up [START_REF] Rajagopalan | Novel experimental techniques for investigating time resolved high speed friction[END_REF][START_REF] Rajagopalan | An experimental method to study high speed sliding characteristics during forward and reverse slip[END_REF][START_REF] Huang | Dynamic tribological response of SiC fracture surfaces[END_REF][START_REF] Huang | Dynamic Friction of SiC Surfaces: A Torsional Kolsky Bar Tribometer Study[END_REF], dynamometer ring with a rectangular specimen launched by a gas gun or a hydraulic machine [START_REF] Philippon | An experimental study of friction at high sliding velocities[END_REF] and pin-on-disk apparatus [START_REF] Dickson | Frictional Heating and Ignition of Energetic Materials[END_REF].

For safety reasons, the presented experiments have been carried out with an inert material, denoted I1, whose mechanical properties are close to explosives ones. It is a fine powder mixed with a binder which has been compacted. Its mechanical behaviour has been previously studied [START_REF] Bailly | Dynamic behavior of an aggregate material at simultaneous high pressure and strain rate: SHPB triaxial tests[END_REF]. Its elastic properties are a 0.4 Poisson's ratio and a 3 GPa Young's modulus. It is a quasi-brittle material with a Drucker-Prager's threshold. Let σ, P and Q respectively denoting the stress tensor, the hydrostatic pressure and the octahedral scission:

P = 1 3 tr(σ) ( 1 ) Q = 1 3 σ -PI : σ -PI ( 2
)
where I is the identity tensor The behaviour remains elastic if the following criterion is respected:

Q + BP < A (3)
The cohesive stress A depends on the strain rate. It varies from 12 MPa at low strain rates to 40 MPa at the strain rates reached during Split Hopkinson Pressure Bar (SHPB) tests, typically 100 s -1 . The internal friction coefficient B is equal to 0.3. In the case of a uniaxial compressive loading, the criterion corresponds to a maximum axial stress of 30 MPa at low strain rates and 100 MPa at the strain rates reached during SHPB tests. As the material has a brittle behaviour, contact pressures higher than the compressive strength can lead to an unexpected fracture and thus to erroneous measurements. Quasi-oedometric tests consist in confining a cylindrical sample in a rigid ring [START_REF] Bailly | Dynamic behavior of an aggregate material at simultaneous high pressure and strain rate: SHPB triaxial tests[END_REF][START_REF] Forquin | An experimental method of measuring the confined compression strenght of geomaterials[END_REF][START_REF] Forquin | Influence of free water on the quasi-static and dynamic of strength of concrete in confined compression tests[END_REF] and applying high stresses on brittle materials without reaching their shear resistance criterions. Indeed, under increasing magnitudes of hydrostatic pressures, materials with a Drucker-Prager's threshold can reach higher octahedral scissions.

The proposed set-up is thus based on a quasi-oedometric configuration. A SHPB device is used to obtain the high velocities.

Set-up

A previous study of the influence of the sliding velocity on the friction has been performed [START_REF] Durand | Caractérisation du comportement à l'interface entre un matériau agrégataire et un acier sous forte pression et à grande vitesse, 20 iéme Congrès Franc ¸ais de Mécanique[END_REF]. The axial compression of the sample was applied by a clamping screw but the interface pressure remained too low (the screw breaks). A new system has been designed in order to reach higher interface pressure (figure 1): the specimen is now pressed on a spring, so it can be simultaneously compressed and rubbed on the tube. The spring is a washers assembly. Its flexibility allows a sufficient displacement to ensure the same friction conditions on the entire interface. It must be highlighted that unlike classical tribometers, such a system allows to obtain the normal pressure and the friction with the same actuator.

The two longitudinal strain gauges glued on the aluminium rod are diametrically opposed to eliminate the flexural strains caused by dissymmetry. The aggregate

Experimental results and numerical analysis

The confined friction set-up is mounted on a testing machine and on a SHPB system. Friction tests are conducted at different sliding velocities.

Both tests are modelled with the finite element method to identify friction parameters. The simulations were performed using ABAQUS CAE with an axisymmetry assumption.

Quasi-static test

Thanks to the spring flexibility, the sliding velocities reached at the friction interface are of the order of the velocity imposed by the machine to the assembly, i.e. 1 mm/min.

The testing machine sensor indicates the force applied by the machine F m . Moreover, the strains measurements on the aluminium rod provide the value of the normal force in this component, denoted F ro . Experimental measurements are displayed on figure 2.

Figure 2 shows F ro as a linear function of F m . The value of ratio is linked to the interface behaviour.

Numerical simulations are performed using an implicit code. A Coulomb's friction law is imposed at the interface between the specimen and the tube: the ratio between the tangential stress and the normal pressure is assumed equal to a constant coefficient f during a friction process. The simulations also show a linear dependence of the force applied by the machine on the normal force in the rod. The numerical relation between the forces ratio and the friction coefficient f is determined and presented on figure 3. This numerical relation enables to determine the friction coefficient from the experimental value of the force ratio. f = 0.18 is obtained with F ro /F m = 0.383 as on figure 2.

Numerical simulations are run with this value of the friction coefficient to check the model validity. The external circumferential strains of the tube ε tu are calculated and these numerical results are compared to the corresponding measurements.

Figure 4 shows that the experimental and the numerical values of the strain ε tu are in good agreement.

Finite element calculations have been performed using an elacticity assumption. As the aggregate material has a low strength, failure can occur and can lead to an erreneous 01017-p.2 calculation. Q+BP must therefore be calculated in the sample to verify the assumption. According to finite element simulations, the criterion (3) is respected everywhere in the specimen. It confirms the elasticity assumption consistency.

The contact pressure is numerically determined at the interface. A strongly heterogeneous distribution is obtained. Figure 6 shows that pressure has reached the desired order of magnitude. The high value of the Poisson's ratio is an advantage.

Dynamic test

The static test analysis showed that high pressure can be generated with this configuration. Our aim is now to combine high pressure and high velocity. The friction setup is then mounted on a SHPB device. Bars are made of aluminium (Young's modulus equal to 74 GPa and Poisson's ratio equal to 0.33) and have a diameter of 40 mm. The striker, the input bar and the output bar have respectively a length of 1.25 m, 3 m and 1.8 m. The way the new apparatus is assembled is detailed on figure 7.

The impact of the striker results in an incident compressive wave ε i in the input bar. Wave reverberations occur in the set-up and it results in a transmitted wave ε t in the output bar and in a reflected wave ε r in the input bar. The incident and the reflected longitudinal strain waves have to be measured at a place where they are separated in the time. The gauge is therefore glued at the middle of the input bar. The circumferential strain on the tube ε tu is also recorded (figure 1).

The incident strain wave depends only on the impact velocity and on the characterics of the striker and of the input bar. It does not depend on phenomena occurring in the friction set-up. The other strains depend on the set-up behaviour: they can be seen as the mechanical response of the friction set-up to the imposed incident strain.

Finite element simulations of the experiment have been performed using ABAQUS. Several friction coefficients f have been used to study the influence of the friction on the mechanical response.

Figures 8-10 represent the numerical strains which should be experimentally measured. Several friction conditions have been used with the same incident wave. The value of the friction coefficient has a noticeable influence on the mechanical response of the set-up.

The dynamic friction coefficient is identified by fitting as well as possible the numerical and the experimental results. The following figures give some comparisons between the experimental strains and the numerical ones obtained with f = 0.4 which seems to be the best fit. Additional simulations of the experiment with no contact 01017-p.3 between the spring and the cap (figure 1) were also performed to understand the influence of the spring.

EPJ Web of Conferences

Comparisons between the numerical results obtained with and without the spring-cap contact on figures 11-13 show that spring stretching has not an immediate influence on the mechanical response. At the beginning of the test, the compression of the sample is actually due to the inertia of the rod and the spring.

The numerical results obtained with f = 0.4 are in good agreement with the experimental results but only at the beginning of the signals. The analysis of the tube strain and the reflected strain displays that the experimental and the numerical results begin to differ slightly before the appearance of the spring-cap contact influence. It is very noticeable in the case of the reflected wave. The discrepancy between experiment and simulation could therefore be explained by a non adapted modelling of the spring stretching. However, the beginnings of the experimental signals prove that the dynamic friction coefficient is higher than the static one. Indeed, the numerical simulation with f = 0.2 close to the static coefficient f = 0.18 gives different results from those obtained with f = 0.4 which are the closest to dynamic experiment.

The interface pressure is between 20 and 120 MPa (figure 14). According to the simulations, sliding velocities are heterogeneous at the very beginning to the test. They

EPJFig. 1 .

 1 Fig. 1. Sketch of the confined friction set-up.

Fig. 2 .Fig. 3 .Fig. 4 .

 234 Fig. 2. Experimental evolutions of F m and F ro respectively the force applied by the machine and the normal force in the rod.

DYMAT 2012 Fig. 5 .Fig. 6 .

 201256 Fig. 5. Sketch of the sample with the values of Q+BP at the maximal load. The maximal value is approximatively 11 MPa.

Fig. 7 .

 7 Fig. 7. Schematic of the friction set-up mounted between the bars.

Fig. 8 .

 8 Fig. 8. Numerical evolution of the strain at the middle of the input bar. The first part corresponds to the incident wave and the second ones to the reflected waves, depending of f magnitude.

Fig. 9 .Fig. 10 .Fig. 11 .

 91011 Fig. 9. Numerical evolution of the strain of the output bar at the position of the gauge (500 mm from the set-up). The waves correspond to the transmitted waves, depending on f magnitude.

Fig. 12 .

 12 Fig. 12. Numerical and experimental evolutions of the strain of the output bar (at the position of the gauge).

Fig. 13 .

 13 Fig. 13. Numerical and experimental evolutions of the circumferential strain on the tube (at the position of the gauge).

Fig. 14 .

 14 Fig. 14. Numerical evolution of the pressure (extreme values along the interface).

reach an approximate value of 2-3 m/s before the appearance of the spring-cap contact influence.

A satisfactory equilibrium of the specimen is shown on figure 15.

Conclusion

In quasi-static loading conditions, the tribometer enables a reliable identification of the interface behaviour between the aggregate material and steel. High interface pressures can be easily generated during the friction process thanks to the original configuration.

An increase of the friction with the sliding velocity is established. It is coherent with [START_REF] Durand | Caractérisation du comportement à l'interface entre un matériau agrégataire et un acier sous forte pression et à grande vitesse, 20 iéme Congrès Franc ¸ais de Mécanique[END_REF]. The experiments performed during our first study and those presented in this paper show how it is difficult to apply simultaneously high pressures and high velocities. Indeed, in [START_REF] Durand | Caractérisation du comportement à l'interface entre un matériau agrégataire et un acier sous forte pression et à grande vitesse, 20 iéme Congrès Franc ¸ais de Mécanique[END_REF], velocities were of the order of 10 m/s but mean pressures did not exceed 20 MPa. On the contrary, in this paper, pressures reach 100 MPa but velocities drop to 2-3 m/s.

Simulations and experiments analyses show that the tribometer presented here could be improved in dynamics. Firstly, the use of a spring to simultaneously compress and rub the sample on the tube is not so relevant. Indeed, as wave propagation is not immediate, the influence of the spring stretching is strongly delayed. Moreover, phenomena linked to wave propagation make the behaviour of the spring complex during the stretching phase.


Jean-Yves Marion
email: jean-yves.marion@loria.frromain.pechoux@loria.fr

Romain Péchoux

A characterization of polynomial complexity classes using dependency pairs

The dependency pair method has already shown its power in proving termination of term rewriting systems. We adapt this framework using polynomial assignments in order to characterize with two distinct criteria the set of the functions computable in polynomial time and the set of the functions computable in polynomial space. To our knowledge, this is a first attempt to capture complexity classes using of the dependency pair method. The characterizations presented are inspired by previous works on implicit computational complexity, and, particularly, by the notions of quasi-interpretation and sup-interpretation. Both criteria are decidable so that we can synthesize resource upper-bounds.

Introduction

The dependency pair method has been introduced in [START_REF] Arts | Termination of term rewriting using dependency pairs[END_REF] in order to prove the termination of programs automatically. The dependency pair method is a complete termination criterion. In other words, the termination of any terminating program or, more precisely, of any term rewriting system, can be demonstrated with the help of such a criterion. However, undecidability of termination forces to specialize this method through applications. Nowadays, almost all termination provers, among others AProVE [START_REF] Giesl | AProVE 1.2: Automatic termination proofs in the dependency pair framework[END_REF], CiME [START_REF] Contejean | Proving Termination of Rewriting with CiME[END_REF] and TTT [START_REF] Hirokawa | Tyrolean termination tool[END_REF], take advantage of such applications.

One of the key challenges is to improve these termination tools in order to analyze the computational complexity of programs automatically. Indeed, there is a strong relation between termination and computational complexity. In order to predict the complexity of the function computed by a program, we first have to prove that it terminates and, then, to put drastic restrictions on either its syntax or its semantics. The motivations behind such an analysis are to provide resource certificates by static analysis. For example, a resource certificate can give the guarantee to the programmer that no buffer overflow occurs during the execution of a program.

Throughout the paper, we focus our attention on the dependency pair method using polynomial assignments. Polynomial assignments are strongly related to polynomial interpretations of [START_REF] Lankford | On proving term rewriting systems are noetherien[END_REF][START_REF] Manna | On the termination of Markov algorithms[END_REF] and, more recently, of [START_REF] Bonfante | Algorithms with polynomial interpretation termination proof[END_REF][START_REF] Cichon | Polynomial interpretations and the complexity of algorithms[END_REF]. However, we no longer consider polynomials over natural numbers but polynomials over real numbers. Since the set of real numbers is no longer well-founded, we can add constraints on the shape of considered polynomials for preserving termination. The subterm property of [START_REF] Dershowitz | Orderings for term-rewriting systems[END_REF], i.e. ∀i ∈ {1, n} f(x 1 , • • • , x n ) > x i , is an example of such a constraint. Nevertheless, this condition is a serious drawback when analyzing the complexity of algorithms since it approximates functions too largely. Hopefully, it is demonstrated in [START_REF] Lucas | Polynomials over the reals in proofs of termination: from theory to practice[END_REF] that this condition can be replaced by a suitable quasi-ordering. Polynomial assignments are also inspired by quasi-interpretations [START_REF] Bonfante | Quasi-interpretations, a way to control resources[END_REF] and sup-interpretations [START_REF] Marion | Resource analysis by sup-interpretation[END_REF]. These two notions provide upper bounds on the size of the values computed by a function symbol. The sup-interpretation is only a generalization of the quasi-interpretation without the subterm property and, as a consequence, allows to capture more algorithms. It is demonstrated in [START_REF] Bonfante | Quasi-interpretations, a way to control resources[END_REF][START_REF] Marion | Sup-interpretations, a semantic method for static analysis of program resources[END_REF] that these notions combined with the product extension and the lexicographic extension of Recursive Path Orderings (RPO) characterize the set of functions computable in polynomial time and, respectively, the set of functions computable in polynomial space. Moreover, sup-interpretations allow to characterize the set of functions computable in alternating logarithmic time [START_REF] Bonfante | A characterization of alternating log time by first order functional programs[END_REF].

In this paper, we make a step forward in the study of relations between computational complexity and termination by giving two new characterizations of the sets of functions computable in polynomial time and in polynomial space with the help of polynomial assignments over reals without the subterm property. To our knowledge, this is a first attempt to capture complexity classes using of the dependency pair method. As demonstrated by Tarski, first order theory over reals is decidable and so are our criteria whenever we consider polynomials of bounded degree. Another consequence is that we obtain heuristics for synthesizing sup-interpretations.

The paper is organized as follows. Section 2 describes the syntax and the semantics of the language. Section 3 introduces the dependency pairs and dependency pair graph. Section 4 defines the polynomial assignments which are used in the characterizations. Sections 5 and 6 provide two distinct criteria which correspond to the characterization of the set of function computable in polynomial space and, respectively, the set of functions computable in polynomial time. Finally, it is stated in the last Section that both criteria provide a natural way for synthesizing sup-interpretations.

Syntax and semantics of first order programs

A program is defined formally as a quadruple X , C, F, R with X , C and F finite disjoint sets which represent respectively the variables, the constructor symbols and the function symbols and R a finite set of rules defined in Figure 1.

The set of rules induces a rewriting relation →. The relation * → is the reflexive and transitive closure of →. Throughout the paper, we only consider programs having disjoint and linear patterns. So each program is confluent [START_REF] Huet | Confluent reductions: Abstract properties and applications to term rewriting systems[END_REF].

The domain of computation of a program X , C, F, R is the constructor algebra T (C). A ground substitution σ is a mapping from variables to values of

(Values) T (C) v ::= c | c(v1, • • • , vn) (Terms) T (C, F, X ) t ::= c | x | c(t1, • • • , tn) | f(t1, • • • , tn) (Patterns) P p ::= c | x | c(p1, • • • , pn) (Rules) R r ::= f(p1, • • • , pn) → t
where x ∈ X , f ∈ F , and c ∈ C. The size |t| of a term t is defined to be the number of symbols of arity strictly greater than 0 occurring in t.

Example 1. Consider the following program which computes the logarithm function:

log(0) → 0 half(0) → 0 log(S(0)) → 0 half(S(0)) → 0 log(S(S(y))) → S(log(S(half(y))))
half(S(S(y))) → S(half(y))

We have for every natural number n, log(S n (0)) = S log(n) (0) where S n+1 (0) = S(S n (0)) and S 0 (0) = 0.

A context is an expression C[ 1 , • • • , r ]
with only one occurrence of each i , where the i are fresh symbols. The substitution of each i by an expression

d i is noted C[d 1 , • • • , d r ].
Example 2. The substitution of the variable by half(y) in the context C[ ] = S(log(S( ))) is equal to S(log(S(half(y)))). Now, we define the notion of call-tree which corresponds to the tree of function calls in one execution of a program.

Definition 1. A state is a tuple f, v 1 , • • • , v n where f is a function sym- bol of arity n and v 1 , . . . , v n are values. Assume that η 1 = f, v 1 , • • • , v n and η 2 = g, u 1 , • • • , u m are two states. Assume also that we have f(p 1 , • • • , p n ) → C[g(e 1 , • • • , e m )] ∈ R with C[ ] a context. A transition between two states η 1 and η 2 , noted η 1 η 2 ,

is defined by:

1. There is a ground substitution σ such that p i σ = v i for i = 1, . . . , n 2. and e j σ = u j for j = 1, . . . , m.

We call such a tree a call-tree of f from values u 1 , . . . ,

u n if f, v 1 , • • • , v n is its root.
A state may be seen as a stack frame since it contains a function call and its respective arguments. A call-tree of root f, v 1 , • • • , v n represents all the stack frames which will be pushed on the stack when we compute f(v 1 , . . . , v n ). We will sometimes refer to + as the transitive closure of .

The size of a state is the sum of the sizes of its values. Given a call-tree and two of its states f,

t 1 , • • • , t n and g, u 1 , • • • , u m , such that f, t 1 , • • • , t n + g, u 1 , • • • , u m , then f, t 1 , • • • , t n + g, u 1 , • • • , u m is called a branch of the call-tree.
The size of a branch is defined to be the sum of the sizes of all its states. The length of a branch is the number of states in the branch. Finally, the size of the call-tree is the sum of the sizes of all its states.

The Dependency Pair Method

In this section, we briefly review the notion of dependency pair introduced by Arts and Giesl [START_REF] Arts | Termination of term rewriting using dependency pairs[END_REF] in order to analyze the termination of programs automatically. Definition 3 (Dependency pair graph). We define the dependency pair graph of a program X , C, F, R by:

Definition 2 (Dependency pair). Given a program X , C, F, R , a depen- dency pair < f(p 1 , • • • , p n ), g(e 1 , • • • , e m ) > is a couple satisfying f, g ∈ F and there is a context C[ ] such that f(p 1 , • • • , p n ) → C[g(e 1 , • • • , e m )] ∈ R.
-The nodes are the dependency pairs

-Given two dependency pairs u =< f 1 (p 1 , • • • , p n ), f 2 (e 1 , • • • , e m ) > and v =< f 3 (q 1 , • • • , q k ), f 4 (d 1 , • • • , d l ) >, there is an edge from u to v if f 2 = f 3 .
A cycle of dependency pairs is defined to be a cycle in the dependency pair graph. We say that the dependency pair u is involved in a cycle if u belongs to a cycle in the dependency graph.

The notions of dependency pairs and dependency pair graph allow to derive a termination criterion:

Theorem 1 ([1]

). A program p is terminating if there is a well-founded weakly monotonic quasi-ordering ≥ q.o. , closed under substitution, such that:

1. For each rule f(p 1 , • • • , p n ) → e ∈ R, f(p 1 , • • • , p n ) ≥ q.o. e. 2.
For each dependency pair s, t , s ≥ q.o. t 3. For each cycle in the dependency pair graph, there is a dependency pair s, t involved in the cycle such that s > q.o. t

Polynomial and additive assignments

In this section, we define polynomial assignments over real numbers. A polynomial assignment associates a polynomial function to every symbol of a program.

We have chosen to study polynomials over real numbers instead of polynomials over natural numbers since the synthesis of such assignments is decidable, under some restrictions, as an application of [START_REF] Bonfante | Synthesis of quasiinterpretations[END_REF]. Following the terminology of [START_REF] Bonfante | Quasi-interpretations, a way to control resources[END_REF], we define the notion of assignment.

Definition 4 (Assignments). An assignment of a symbol b ∈ F C of arity n is a function b : (R + ) n → R + . We extend assignments -to terms canonically. Given a term t = b(t 1 , • • • , t n ) with m variables, the assignment t is a function (R + ) m → R + defined by the rules:

b(t 1 , • • • , t n ) = b ( t 1 , • • • , t n ) x = X
where X is a fresh variable ranging over reals.

A program assignment is an assignment -defined for each symbol of the program.

Definition 5 (Polynomial assignments). Let Max-Poly{R + } be the set of functions defined to be constant functions over R + , projections, max, +, × and closed by composition. An assignment -is said to be polynomial if for each symbol b ∈ F C, b is a function in Max-Poly{R + }. Now we define the notion of additive assignments which guarantees that the assignment of a value remains affinely bounded by its size.

Definition 6 (Additive assignments

). An assignment of a constructor symbol c of arity n > 0 is additive if

c (X 1 , • • • , X n ) = n i=1 X i + α c , with a constant α c ≥ 1.
An assignment -of a program p is additive if each constructor symbol of p has an additive assignment.

Lemma 1. Given an additive assignment -, there is a constant α such that for each value v, the following inequality is satisfied:

|v| ≤ β v ≤ β α × |v|
Proof. Define α = max c∈C (α c ) where α c is taken to be the constant of definition 6, if c is of strictly positive arity, and α c is equal to the constant c otherwise. The inequalities follow directly by induction on the size of a value.

Since the dependency pair method requires a well-founded quasi-ordering and we are working over real numbers, we first have to restrict the considered inequalities in order to preserve the well-foundedness. Following [START_REF] Lucas | Polynomials over the reals in proofs of termination: from theory to practice[END_REF], we define a well-founded quasi-ordering: Definition 7 ( [START_REF] Lucas | Polynomials over the reals in proofs of termination: from theory to practice[END_REF]). Given a fixed constant β > 0, we define the quasi-ordering ≥ β over R + , and its strict part, by:

-x ≥ β y iff x ≥ y -x > β y iff for every x, y ∈ R + , x ≥ β + y
Definition 8 (Monotonic assignments). An assignment is monotonic if for any symbol b, b is an increasing (not necessarily strictly) function with respect to each variable. That is, for every symbol b and all

X 1 , • • • , X n , Y 1 , • • • , Y n of R + with X i ≥ β Y i , we have b (X 1 , • • • , X n ) ≥ β b (Y 1 , • • • , Y n ).

A criterion for polynomial space computations

We present in this section a criterion using the dependency pair method and polynomial assignments which allows to characterize the set of functions computable in polynomial space.

Definition 9 (polynomial space interpretation). A program X , C, F, R admits a polynomial space interpretation if there is an additive, monotonic and polynomial assignment -such that its dependency pair graph satisfies:

-For each rule f(p 1 , • • • , p n ) → e ∈ R, f(p 1 , • • • , p n ) ≥ β e .
-For each dependency pair s, t , s ≥ β t -For each cycle in the dependency pair graph, there is a dependency pair s, t involved in the cycle such that s > β t

Example 4. The program of Example 1 admits the following polynomial space interpretation:

0 = 0 S (X) = X + 1 half (X) = X/2 log (X) = X
Indeed, for every rule, we check that:

half(0) = 0 ≥ β 0 = 0 half(S(0)) = 1/2 ≥ β 0 = 0 half(S(S(y))) = (Y + 2)/2 ≥ β Y /2 + 1 = S(half(y)) log(0) = 0 ≥ β 0 = 0 log(S(0)) = 1 ≥ β 0 = 0 log(S(S(y))) = Y + 2 ≥ β 2 + Y /2 = S(log(S(half(y))))
Moreover, taking β = 1, for every dependency pair, we have:

half(S(S(y))) = Y /2 + 1 > β Y /2 = half(y) log(S(S(y))) = Y + 2 > β 1 + Y /2 = log(S(half(y))) log(S(S(y))) = Y + 2 ≥ β Y /2 = half(y)
Just notice that the inequalities corresponding to the two cycles in the dependency pair graph are strict.

First, we are going to show that a program whose dependency pair graph admits a polynomial space interpretation is terminating: Theorem 2. Suppose that p is program whose dependency pair graph admits a polynomial space interpretation -, then the program p terminates on all inputs.

Proof. Just define the quasi-ordering ≥ q.o. on terms to be ≥ β . By definition of a polynomial space interpretation the criterion of the dependency pair method is checked. It remains to see that this quasi-ordering is monotonic well-founded and closed by substitution. It is well-founded since the strict inequality > β guarantees a decrease by at least the fixed constant β > 0. It is closed under substitution by definition of assignments. Finally, it is monotonic since assignments are monotonic.

Proposition 1. Given a program p which admits a polynomial space interpretation -, then for every term t and every ground substitution σ such that tσ → * u, we have :

tσ ≥ β u Proof.
P (|v 1 |, • • • , |v n |) ≥ | f(v 1 , • • • , v n ) | Proof. By Theorem 2, the program terminates so that f(v 1 , • • • , v n ) is clearly defined. By Proposition 1, we have f(v 1 , • • • , v n ) ≥ β f(v 1 , • • • , v n ) . We set P ( 1 , • • • , n ) = f (α × 1 , . . . , α × n ) with α the constant of Lemma 1. We obtain that P (|v 1 |, . . . , |v 1 |) ≥ | f(v 1 , • • • , v n ) | by monotonicity of assignments.
Lemma 2. Given a program p admitting a polynomial space interpretationand a call-tree corresponding to one execution of this program and containing a branch of the shape f,

v 1 , • • • , v n + f, u 1 , • • • , u n then: f(v 1 , • • • , v n ) > β f(u 1 , • • • , u n )
Proof. This result is obtained by combining Definition 9, which guarantees that each cycle of a dependency pair graph corresponds to a strict decrease of the polynomial space interpretation, Proposition 1 and the monotonicity of assignments.

Corollary 1. Given a program p admitting a polynomial space interpretation -then every branch of the call-tree of the shape f,

v 1 , • • • , v n + f, u 1 , • • • , u n has a length bounded by γ × f(v 1 , • • • , v n ) , for some constant γ.
Proof. By Lemma 2, we know that two successive calls of the same function symbol corresponds to a strict decrease

f(v 1 , • • • , v n ) > β f(u 1 , • • • , u n ) . It means that f(v 1 , • • • , v n ) ≥ β + f(u 1 , • • • , u n ) . Consequently, we have at most f(v 1 , • • • , v n ) /β
successive states in the branch where the function symbol f occurs. Since the maximal number of dependency pairs involved in a cycle of the dependency pair graph is bounded by the size of the program, which is fixed, we obtain that the branch corresponding to the cycle has a length bounded by

γ × f(v 1 , • • • , v n ) , for some constant γ.
Lemma 3. Given a program p admitting a polynomial space interpretationand a call-tree corresponding to one execution of this program, then the size of each branch of the call-tree is polynomially bounded in the size of the inputs.

Proof. By Theorem 3, we know that every value of a state is polynomially bounded by the size of the inputs. That is, there is a polynomial R such that for every state g,

v 1 , • • • , v m of a call-tree of root f, u 1 , • • • , u n , we have: ∀i ∈ {1, m} , |v i | ≤ R( max j=1..n (|u j |))
So that, the size of each state is bounded by Q(max j=1..n |u j |) with Q(X) = k×R(X) and k the maximal arity of the program. By Corollary 1, we have shown that each cycle starting from g,

v 1 , • • • , v m has at most γ × g(v 1 , • • • , v m ) oc- currences, which is bounded by P g (|v 1 |, • • • , |v n |) = γ × g (α × |v 1 |, . . . , α × |v k |) with α the constant of Lemma 1. Consequently, each cycle starting from g, v 1 , • • • , v m has at most P g (Q(max j=1..n |u j |), . . . , Q(max j=1..n |u j |)) occur- rences. Now define ω(X) = max g∈F (P g (Q(X), . . . , Q(X))).
Let A be the maximal number of cycles in the program (Notice that A is considered as a constant since it only depends on the size of the program). We know that the depth of each branch starting from f,

u 1 , • • • , u n is bounded by A × ω(max j=1..n (|u j |)). Finally, A × ω(max j=1..n (|u j |)) × Q(max j=1..n (|u j |))
is the required polynomial bound on the size of each branch.

Theorem 4. The set of functions computed by programs which admits a polynomial space interpretation is exactly the set of functions computable in polynomial space.

Proof. By Lemma 3, we know that the size of each branch and each state of the call-tree is polynomially bounded in the size of the inputs. Evaluating the program in the depth of the call-tree, we obtain that the set of functions computed by programs which admit a polynomial space interpretation is included in Pspace. The proof of completeness is inspired by a characterization of [START_REF] Bonfante | Quasi-interpretations, a way to control resources[END_REF] using Parallel Register Machines (PRM). Savitch [START_REF] Savitch | Relationship between nondeterministic and deterministic tape classes[END_REF] and Chandra, Kozen and Stockmeyer [START_REF] Chandra | Alternation[END_REF] have shown that the set of functions computed by PRM in polynomial time is exactly the set of functions computable in polynomial space. We let the reader check that the program given in [START_REF] Bonfante | Quasi-interpretations, a way to control resources[END_REF], which simulates PRM by a TRS admits clearly a polynomial space interpretation.

This criterion is an improvement of the previous characterization of [START_REF] Bonfante | Quasi-interpretations, a way to control resources[END_REF] using the notion of quasi-interpretation and Recursive Path Orderings (RPO) with lexicographic and product status. Indeed, our criterion has a greater intensionality since it captures more natural algorithms, like the ones computing the greatest common divisor or the division of two unary numbers, as illustrated in the following example.

Example 5. Consider the following program which computes the greatest common divisor: le(S(x), S(y)) → le(x, y) minus(0, z) → 0 le(S(x), 0) → tt minus(S(z), 0) → S(z) le(0, S(y)) → ff minus(S(u),

S(v)) → minus(u, v) if(tt, u, v) → u if(ff , u, v) → v gcd(0, z) → z gcd(S(z), 0) → S(z) gcd(S(u), S(v)) → if(le(u, v), gcd(minus(v, u), S(u)), gcd(minus(u, v), S(v)))
This program is not terminating by RPO since the last rule calls the function symbol minus on the arguments of a recursive call. However, we let the reader checks that it admits the following polynomial space interpretation:

0 = tt = ff = 0 S (X) = X + 1 le (X, Y ) = minus (X, Y ) = X if (X, Y, Z) = max(Y, Z) gcd (X, Y ) = X + Y

A criterion for polynomial time computations

We present in this section a refinement of the previous criterion which allows to apply the dependency pair method using polynomial assignments in order to capture polynomial time computable functions. First, we define the notion of agglomerated set which allows to control the recursive calls corresponding to the same recursive rule together: Definition 10 (Precedence). We define a precedence ≥ F on function symbols. Set f ≥ F g if there is a rule of the shape f(p) → C[g(e)] ∈ R. Then, take the reflexive and transitive closure of ≥ F , that we also note ≥ F . f ≈ F g if f ≥ F g and inversely g ≥ F f. Lastly, f > F g if f ≥ F g and g ≥ F f does not hold. Intuitively, f ≥ F g means that f calls g in some executions. And f ≈ F g means that f and g call each other recursively. Definition 11 (Agglomerated set). Given a dependency pair < s, t > of the dependency pair graph, we define its agglomerated set A(< s, t >) by:

A(< s, t >)={< s , t > such that s = s = f(p 1 , • • • , p n ), t = g(e 1 , • • • , e m )
and f ≈ F g } Definition 12 (polynomial time interpretation). A program X , C, F, R admits a polynomial time interpretation if there is an additive, monotonic and polynomial assignment -such that its dependency pair graph satisfies:

-For each rule f(p 1 , • • • , p n ) → e ∈ R, f(p 1 , • • • , p n ) ≥ β e .
-For each dependency pair s, t , s ≥ β t -For each agglomerated set A(< s, t >) = {< s, t 1 >, . . . , < s, t n >}, we have s > β n i=1 t i Remark 1. Notice that the last condition corresponds to a resource sharing between the distinct recursive calls. It is very close in the spirit from the resource diamond introduced by Hoffman [START_REF] Hofmann | The strength of Non-Size Increasing computation[END_REF] and from Soft Linear Logic [START_REF] Lafont | Soft linear logic and polynomial time[END_REF]. Moreover, this condition also implies that for every cycle of the dependency pair graph, there is a dependency pair < s, t > such that s > β t since s > β n i=1 t i implies ∀j ∈ {1, n} s > β t j and every polynomial time interpretation is a polynomial space interpretation. Consequently, Proposition 1 and Theorems 3 and 2 hold for polynomial time interpretations. Example 6. Just check that the program of Example 1 admits the following polynomial time interpretation:

0 = 0 S (X) = X + 1 half (X) = X log (X) = X Lemma 4.
Given a program p admitting a polynomial time interpretationand a call-tree corresponding to one execution of this program, then the size of the call-tree is polynomially bounded in the size of the inputs.

Proof. By Theorem 3, we know that every value of a state is polynomially bounded by the size of the inputs. That is, there is a polynomial R such that for every state g,

v 1 , • • • , v m of a call-tree of root f, u 1 , • • • , u n , we have: ∀i ∈ {1, m} , |v i | ≤ R( max j=1..n (|u j |))
If the state g, v 1 , • • • , v m corresponds to a recursive call, then suppose that its corresponding agglomerated set is of the shape

{< g(p 1 , • • • , p n ), f 1 (e 1 ) >, . . . , < g(p 1 , • • • , p n ), f n (e n ) >}
There is a ground substitution σ such that p i σ = v i . The third condition of the polynomial time interpretation implies that: Proof. By Lemma 4, we know that the size of the call-tree is polynomially bounded by the input sizes, and consequently the derivation length is polynomially bounded. Theorem 3 states that the size of any computed value is polynomially bounded by the input sizes. As a consequence, we can apply the proof of the characterization of the polynomial time computable functions with polynomial interpretations of [START_REF] Bonfante | Algorithms with polynomial interpretation termination proof[END_REF], showing that every program can be simulated by a Turing Machine in polynomial time.

g(v 1 , • • • , v n > β n i=1 f i (e i σ)
Conversely, every polynomial interpretation of [START_REF] Bonfante | Algorithms with polynomial interpretation termination proof[END_REF] is a polynomial time interpretation. Indeed, the subterm property and the definition of polynomial interpretations in [START_REF] Bonfante | Algorithms with polynomial interpretation termination proof[END_REF] entail all the conditions of Definition 12. This criterion is an improvement of the characterization of [START_REF] Bonfante | Algorithms with polynomial interpretation termination proof[END_REF] for two reasons. Firstly, we work on real numbers so that we have more flexibility for the choice of the assignments. Moreover, because of Tarski's result assignments of bounded degree over real numbers are decidable so that we have procedure in order to find an assignment which is a polynomial time interpretation. Secondly, we only require a strict inequality for the function calls which correspond to cycles in the dependency pair graph. As a consequence, this criterion has less constraints and captures more algorithms. It also improves the characterization of polynomial time computable functions using Recursive Path Orderings (RPO) with product status and quasi-interpretations in [START_REF] Bonfante | Quasi-interpretations, a way to control resources[END_REF]. Indeed, our criterion has a greater intensionality since it captures more natural algorithms, like the one computing the division of two numbers, as illustrated by the following example. This program is not terminating by RPO with product status since the last rule of quo calls the function minus on the arguments of a recursive call. However, we let the reader checks that it admits the following polynomial time interpretation: 0 = 0 minus (X, Y ) = X S (X) = X + 1 quo (X, Y ) = X + Y

Sup-interpretation synthesis

A sup-interpretation is a tool [START_REF] Marion | Resource analysis by sup-interpretation[END_REF][START_REF] Marion | Sup-interpretations, a semantic method for static analysis of program resources[END_REF] which provides an upper-bound on the size of a value computed by a symbol. In [START_REF] Bonfante | A characterization of alternating log time by first order functional programs[END_REF], we show that sup-interpretations allow to characterize the set of alternating logarithmic time computable functions. We show in this section that polynomial time and space assignments give heuristics to compute polynomial sup-interpretations.

Definition 13 (Sup-interpretation). A sup-interpretation is a partial assignment θ which verifies the three conditions below:

1. The assignment θ is weakly monotonic. That is, for each symbol b in the domain of θ, the function θ(b) is a monotonic function. 2. For each value v of the computational domain T (C), the sup-interpretation of v is greater than the size of v, i.e. θ(v) ≥ |v|. Proof. By Proposition 1, for every polynomial time or polynomial space interpretation we have

f(v 1 , • • • , v n ) ≥ f(v 1 , • • • , v n ) .
Since every polynomial time or polynomial space interpretation is additive, by Lemma 1, we have for every value v, v ≥ |v|. Finally, it remains to see that polynomial time or polynomial space interpretation consist in monotonic assignments.

A consequence of this Theorem is that we have a procedure to compute supinterpretations. Indeed, if we manage to compute a polynomial time or polynomial space assignment then we obtain a sup-interpretation.

Fig. 1 .

 1 Fig. 1. Syntax of the programs

Example 3 .

 3 If we consider the program of Example 1, log(S(S(y))), half(y) is a dependency pair since there is a rule log(S(S(y))) → C[half(y)] with a context C[ ] = S(log(S( ))).

Theorem 3 .

 3 We show this result by induction on the derivation length. Consider a term e = b(e 1 , • • • , e n ) and suppose that b(e 1 , • • • , e n )σ → * u. By induction hypothesis (I.H.), and using a call-by-value evaluation, if e i σ → * u i then e i σ ≥ β u i . We can evaluate programs in such a way since they are confluent. Moreover, suppose that b(u 1 , • • • , u n ) → * u then, by induction hypothesis again, we have b(u 1 , • • • , u n ) ≥ β u . So, that : eσ = β b(e 1 , • • • , e n )σ Since e = b(e 1 , • • • , e n ) = β b ( e 1 σ , . . . , e n σ ) By Definition of -≥ β b ( u 1 , . . . , u n ) By I.H. and Monotonicity = β b(u 1 , • • • , u n ) By Definition of -≥ β u By I.H. again Given a program p admitting a polynomial space interpretation, then for every function symbol f of arity n there is a polynomial such that for every values v 1 , • • • , v n we have:

Example 7 .

 7 Consider the following program which computes the greatest common divisor:minus(0, z) → 0 quo(0, S(z)) → 0 minus(S(z), 0) → S(z)quo(S(y), S(z)) → S(quo(minus(y, z), S(z))) minus(S(u), S(v)) → minus(u, v)

3 .Theorem 6 .

 36 For each symbol b in the domain of θ of arity n and for each valuesv 1 , . . . , v n of T (C), if b(v 1 , . . . , v n ) ∈ T (C), then θ(b(v 1 , . . . , v n )) ≥ θ( b(v 1 , . . . , v n ) ). Every polynomial time or polynomial space interpretation is a supinterpretation.

  Consequently, we can apply at most 1/β × g(v 1 , • • • , v n recursive rules. And the number of states added in the call-tree by the rules corresponding to a cycle in the dependency pair graph is polynomially bounded by the inputs size. Since the number of cycles in the dependency pair graph is bounded by the size of the program, we obtain that the number of states in the call-tree is polynomially bounded by the inputs size. Theorem 5. The set of functions computed by programs which admits a polynomial time interpretation is exactly the set of functions computable in polynomial time.

			By Definition 12
	n
	≥ β +	f i ( e i σ )	By Proposition 1
	i=1


Jean-Yves Marion
email: jean-yves.marion@loria.frromain.pechoux@loria.fr

Romain Péchoux

Resource control of object-oriented programs

A sup-interpretation is a tool which provides an upper bound on the size of a value computed by some symbol of a program. Supinterpretations have shown their interest to deal with the complexity of first order functional programs. For instance, they allow to characterize all the functions bitwise computable in Alogtime. This paper is an attempt to adapt the framework of sup-interpretations to a fragment of oriented-object programs, including distinct encodings of numbers through the use of constructor symbols, loop and while constructs and non recursive methods with side effects. We give a criterion, called brotherly criterion, which ensures that each brotherly program computes objects whose size is polynomially bounded by the inputs sizes.

Introduction

A sup-interpretation is a tool introduced in [START_REF] Marion | Resource analysis by sup-interpretation[END_REF] in order to deal with the Implicit Computational Complexity of first order functional programs. Basically, the sup-interpretation of a first order functional program provides upper bounds on the size of any value computed by some function symbols of the program. The notion of sup-interpretation is a descendant of the notion of quasi-interpretation. See [START_REF] Bonfante | Quasi-interpretation a way to control resources[END_REF] for a survey on quasi-interpretations. It has been demonstrated in [START_REF] Marion | Sup-interpretations, a semantic method for static analysis of program resources[END_REF], that the notion of polynomial sup-interpretation strictly generalizes the notion of polynomial quasi-interpretation. In other words, every polynomial quasi-interpretation is a polynomial sup-interpretation and there are programs which admit a sup-interpretation and no quasiinterpretation. As a consequence, sup-interpretation provides more intentionality than quasi-interpretation, i.e. it allows to capture the complexity of more algorithms. Such a flexibility is very interesting when we consider small complexity classes. For example, in [START_REF] Bonfante | A characterization of alternating log time by first order functional programs[END_REF], sup-interpretations allow to characterize all the functions bitwise computable in alternating logarithmic time. Another interesting consequence develloped in [START_REF] Marion | Resource analysis by sup-interpretation[END_REF] consists in an application of the sup-interpretation tool to termination criteria such as the dependency pairs [START_REF] Arts | Termination of term rewriting using dependency pairs[END_REF] or the size change principle [START_REF] Lee | The size-change principle for program termination[END_REF].

The notion of quasi-interpretation has already been extended to Bytecode verification and to reactive programs. See for example [START_REF] Amadio | A functional scenario for bytecode verification of resource bounds[END_REF][START_REF] Amadio | Resource control for synchronous cooperative threads[END_REF][START_REF] Dal-Zilio | Resource bound certification for a tail-recursive virtual machine[END_REF]. Consequently, a major issue consists in the adaptation of the sup-interpretation analysis to imperative and object-oriented programs. We try to tackle this problem in this paper by enlarging the framework of sup-interpretations to a fragment of object-oriented programs without recursion. Our language is very similar to the language studied in [START_REF] Igarashi | Featherweight Java: A Minimal Core Calculus for Java and GJ[END_REF]. However, since we consider assignments, it is closer to a fragment of [START_REF] Drossopoulou | Describing the semantics of Java and proving type soundness. Formal Syntax and Semantics of Java[END_REF] where we add loop and while constructs. A consequence is that we have to control side effects. Our work is inspired by recent studies on the Implicit Computational Complexity of imperative programs [START_REF] Niggl | Certifying polynomial time and linear/polynomial space for imperative programs[END_REF][START_REF] Kristiansen | The flow of data and the complexity of algorithms[END_REF]. Contrarily to these seminal works, we work on polynomial algebra instead of matrix algebra. There are at least two reasons for such an approach. Firstly, the use of polynomials gives a clearest intuition and pushes aside a lot of technicalities. Secondly, polynomials give more flexibility in order to deal with method calls.

The paper is organized as follows. After introducing our language and the notion of sup-interpretation of an object-oriented program, we give a criterion, called brotherly criterion, which ensures that each brotherly program computes objects whose size is polynomially bounded by the inputs sizes, even if the program is defined with function calls. To our knowledge, previous works on the implicit computational complexity of imperative programs did not support such a flexibility. Consequently, this criteria seems to be a great improvement on the study of the complexity of imperative programs.

2 Object-oriented Programs

Syntax of programs

We consider object-oriented programs. Basically a program is composed by three sets of disjoint symbols X , P and F and a set Class ⊆ F. The set X represents the set of attributes. Throughout the following paper, we use capital letters X, Y, Z, . . . for attributes. The set P is the set of parameters which are passed as arguments of a method. The symbols of Class are the class identifiers. They provide distinct data encodings such as the unary encoding, using the identifier S for a class having one attribute and the identifier for a class without any attribute, or the binary encoding, using the class identifiers 1 and 0. Each function symbol f ∈ F must be defined by one method of some class. A class C ∈ Class is composed by attribute and method declarations, including a particular constructor method, which are described by the following grammar:

Attributes A ::= var X; | var X; A Expressions e ::= x | X | X.f(e 1 , • • • , e n ) | new C(e 1 , • • • , e n ) Commands Cm ::= skip | X := e | Cm 1 ; Cm 2 | loop X {Cm} | if e then
where X ∈ X , x, x 1 , • • • , x n ∈ P, f ∈ F, e 1 , • • • , e n ∈ Expressions and M 1 ; . . . ; M n ∈ Methods.
The method Cons is a special constructor method of the shape C(x 1 , ..., x n ) {X 1 := x 1 ; . . . ; X n := x n } which appears in each class C ∈ Class whenever the class C has n attributes X 1 , • • • , X n . As a consequence, we have Class ⊆ F. This particular method can only be used in a command of the shape X := new C(e 1 , • • • , e n ). All attributes appearing in the methods of a given class Class must belong to the attributes of this class. Finally, we define the main class main to be a special class defined by attributes declarations and commands.

We suppose that the attributes and methods of two distinct classes are pairwise distinct.

For notational convenience, we sometimes refer to e as a sequence of expressions e 1 , • • • , e n , whenever n is clear from the context. Given a program p, we define a precedence ≥ F on function symbols of F. Set f ≥ F g if the method defining f is of the shape f(x) {Cm ; return X; } and the function symbol g appears in Cm. Take the reflexive and transitive closure of ≥ F , that we also note ≥ F . It is not difficult to establish that ≥ F is a preorder. Lastly, we say that f > F g if f ≥ F g and g ≥ F f does not hold. Intuitively, f > F g means that f cannot call g. Throughout the following paper, we suppose that for each method of the shape f(x) {Cm ; return X; } and for each function symbol g which occurs in Cm, f > F g, i.e. there is no recursive call in the program.

For each expression e of a program, we suppose that function symbols f ∈ F -Class appear only in the outermost position of an expression e. This restriction allows to deal with side effects in a clearest fashion. This is not a severe restriction since every program can be transformed efficiently in an equivalent program which does fit this requirement, by adding new attributes for the intermediate computations. For example, a command of the shape X := V.f(U.g(X)) is transformed into Y := U.g(X); X := V.f(Y ) with Y a fresh attribute. For simplicity, we suppose, that no function symbol appears in the expression e of the commands if e then Cm 1 else Cm 2 and while e {Cm}.

The attribute X is not allowed to occur in the command Cm of an iteration of the shape loop X {Cm}. The attribute X is not allowed to occur in a method of the shape f(x) {Cm ; return Y ; }, if the function symbol f appears in the command Cm of an iteration loop X {Cm}. In other words, the program is not allowed to read and to write the attribute X during the execution of a loop X {Cm}. where Cm 1 , • • • , Cm 3 are labels used to refer to commands and add is a method which is not described in the program and which corresponds to the unary or binary addition depending on the kind of defined objects.

Semantics

The domain of computation is the set of objects defined inductively by:

Objects v ::= b | b(v 1 , • • • , v n ) b ∈ Class Given a main class having n attributes X 1 , • • • , X n , an object v i is stored in each X i at any time.
A ground substitution σ represents a store which consists in a total mapping from X to objects in Objects. Given a ground substitution σ and an attribute X, the notation σ {X := u} means that the object stored in Xσ is updated to the object u in σ. A parameter substitution β is a total mapping from P to objects in Objects. Given an expression e and a ground substitution σ, we use the notation e, σ → u, σ whether the expression e evaluates to u and the store σ is updated to σ . We use the notation Cm, σ → σ , if σ is updated to σ during the execution of the command Cm. Given a program p of main class Class main {A; Cm} and a store σ, p computes a store σ defined by Cm, σ → σ .

The operational semantics of our language is inspired by the operational semantics of the java fragment given in [START_REF] Drossopoulou | Describing the semantics of Java and proving type soundness. Formal Syntax and Semantics of Java[END_REF] and is described in Figure 1.

∈ X ∪ P , σ → σ, σ e, σ → u, σ f(x) {Cm ; return Y ; } ∃β, xβ = u Cmβ, σ → σ X.f(e), σ → Y σ , σ e, σ → u, σ C ∈ Class new C(e), σ → C(u), σ e, σ → u, σ X := e → σ {X := u} skip, σ → σ Cm 1 , σ → σ Cm 2 , σ → σ Cm 1 ; Cm 2 , σ → σ e, σ → 1, σ , 0, σ or u, σ with u > 1 if e then Cm 1 else Cm 2 , σ → Cm 1 , σ , Cm 2 , σ or skip, σ with Cm n = Cm; Cm n-1 and Cm 0 = skip loop X i {Cm} , σ → Cm |v i | , σ e, σ → 1, σ or 1, σ
with u = 1 while e {Cm} , σ → Cm; while X {Cm} , σ or skip, σ A program assignment I is defined over an expression e if each symbol of F in e belongs to dom(I). Suppose that the assignment I is defined over an expression e, The partial assignment of e w.r.t. I, that we note I * (e) is the canonical extension of the assignment I defined as follows:

1. If is in X ∪ P, then I * ( ) =

I(C)( 1 , • • • , m ) = m i=1 i + α C where α C ≥ 1
If the assignment of each class symbol of strictly positive arity is additive then the assignment is additive.

Sup-interpretations

Definition 3.5: Given a program p of main class having n attributes X 1 , . . . , X n , a sup-interpretation is an additive assignment θ of p which satisfies:

1. The assignment θ is weakly monotonic. That is, for each symbol b ∈ dom(θ), the function θ(b) satisfies:

∀i, i ≥ i ⇒ θ(b)(. . . , i , . . .) ≥ θ(b)(. . . , i , . . .) 2.
For each function symbol f ∈ dom(θ) -Class of arity m, for each m tuple of objects v, and for each store σ if

X i .f(v), σ → v, σ then θ(f)(θ * (v), θ * (X i σ)) ≥ max(θ * (v), θ * (X i σ ))
Intuitively, the sup-interpretation is a special interpretation of a symbol. Instead of yielding the symbol denotation, a sup-interpretation of a function symbol provides an upper bound on the outputs sizes of the function denoted by the symbol. It is worth noticing that sup-interpretation is a complexity measure in the sense of Blum [START_REF] Blum | A machine-independent theory of the complexity of recursive functions[END_REF].

Example 3.3: Suppose that the method add of Example 2.1 is defined over an encoding of unary numbers using two class constructor symbols S and of respective arity 1 and 0. It admits the following additive and polynomial sup-interpretation θ(add)( 1 , 2 ) = 1 + 2 , θ(S)( ) = +1 and θ( ) = 0. Indeed, this function is monotonic. For every unary number S v ( ), we let the reader check that θ * (S v ( )) = |S v ( )| = v. Moreover, for every unary number S v ( ) and for every store σ such that Xσ = S u ( ), with S n+1 ( ) = S(S n ( )) and S 0 ( ) = , if X.add(S v ( )), σ → S v+u ( ), σ X := S v+u ( ) , then:

θ * (add)(θ * (S v ( )), θ * (S u ( ))) = θ * (S u ( )) + θ * (S v ( ))
By Dfn of θ

= u + v θ * (S v ( )) = v ≥ max(u + v, u) = max(θ * (S u+v ( )), θ * (S u ( )))
So that, Condition 2 of Definition 3.2 is checked. Lemma 3.2: Given a program p of main class having n attributes X 1 , . . . , X n and having a sup-interpretation θ defined over an expression e, then, for each parameter substitution β, θ * (eβ) denotes a function from (R + ) n to R + which satisfies:

For each store σ, if eβ, σ → v, σ then

θ * (eβ)(θ * (X 1 σ), . . . , θ * (X n σ)) ≥ θ * (v) Moreover, if e = X i .f(e 1 , • • • , e n ),
we have:

θ * (eβ)(θ * (X 1 σ), . . . , θ * (X n σ)) ≥ θ * (X i σ ) Example 3.4: Consider the program of Example 2.1. As demonstrated in Example 3.2, θ(add)( 1 , 2 ) = 1 + 2 , θ(S)( ) = +1
and θ( ) = 0 define a sup-interpretation for the method add. The method move admits the following sup-interpretation θ(move)(x, y, ) = x + y + and θ(Position)(x, y) = x + y + 1. Indeed, θ(move) and θ(Position) are monotonic and, for each store σ = {U := u, V := Position(S u 1 ( ), S u 2 ( )), W := S w ( ), Z := z}, we have:

V.move(w, w), σ → S u 1 +w ( ), σ V := Position(S u 1 +w ( ), S u 2 +w ( )) Since θ * (S n ( )) = n = |S n ( )|, we have to check Condition 2 of Definition 3.2:

θ * (V.move(W σ, W σ))(θ * (u, Position(S u 1 ( ), S u 2 ( )), S w ( ), z)) = θ(move)(θ * (W σ), θ * (W σ), V )(θ * (u, Position(S u 1 ( ), S u 2 ( )), S w ( ), z)) = θ(move)(θ * (W σ), θ * (W σ), θ * (Position(S u 1 ( ), S u 2 ( )))) = θ * (W σ) + θ * (W σ) + θ * (Position(S u 1 ( ), S u 2 ( ))) = θ * (S w ( )) + θ * (S w ( )) + u 1 + u 2 + 1 ≥ max(w + u 1 , 2 × w + u 1 + u 2 + 1)
= max(θ * (S u 1 +w ( )), θ * (Position(S u 1 +w ( ), S u 2 +w ( ))))

Weights

Now, we are going to define the notion of weight which allows to control the size of the objects held by the attributes during loop and while iterations. Basically, a weight is a partial mapping over commands. The weights depend strongly on the considered command, so that we have to make the distinction between commands.

For that purpose, define the relation over commands by Cm 1 Cm

• if there are Cm 2 and Cm 3 such that Cm = Cm 2 ; Cm 1 ; Cm 3 ,

• Cm = if e then Cm 2 else Cm 3 and Cm 1 Cm 2 or Cm 1 Cm 3 ,

• Cm = loop X {Cm 2 } and Cm 1 Cm 2 ,

• or Cm = while e {Cm 2 } and Cm 1 Cm 2 , and its reflexive and transitive closure, that we also note . defines a partial ordering over commands. The strict relation is defined by Cm 1 Cm if Cm 1 Cm and Cm 1 = Cm Definition 3.6: A command Cm is said to be:

• flat if there is no Cm 1 of the shape Cm 1 = while e {Cm 2 } or Cm 1 = loop X {Cm 2 } such that Cm Cm 2 .

• 4 Criteria to control resources

Brotherly criterion

The brotherly criterion gives constraints on weights and sup-interpretations in order to bound the size of the objects computed by the program by some polynomial in the size of the inputs. Definition 4.8: A program having a main class with n attributes X 1 , • • • , X n is brotherly if there are a polynomial sup-interpretation and a polynomial weight such that:

1. For every flat, minimum and looped command Cm of the main class, we have: -For every expression of the shape X j .f(e 1 , • • • , e m ) occurring in Cm:

ω Cm (T +1, X 1 , • • • , X n ) ≥ ω Cm (T, X 1 , .
. . , X j-1 , θ * (e)(X), X j+1 , . . . , X n ) -For every assignment X i := e Cm, we have:

ω Cm (T +1, X 1 , • • • , X n ) ≥ ω Cm (T, X 1 , . . . , X i-1 , θ * (e)(X), X i+1 , . . . , X n )
with T is a fresh variable.

2. For every flat, minimum and whiled command Cm of the main class, we have: -For every expression of the shape X j .f(e 1 , • • • , e m ) occurring in Cm:

ω Cm (X 1 , • • • , X n ) ≥ ω Cm (X 1 , . . . , X j-1 , θ * (e)(X), X j+1 , . . . , X n ) -For every assignment X i := e Cm, we have:

ω Cm (X 1 , • • • , X n ) ≥ ω Cm (X 1 , .
. . , X i-1 , θ * (e)(X), X i+1 , . . . , X n )

Intuitively, the first condition ensures that the size of the objects held by the attributes remains polynomially bounded. The fresh variable T can be seen as a temporal factor which takes into account the number of iterations allowed in a loop. Such a number is polynomially bounded by the size of the objects held by the attributes. The second condition on whiled commands is very similar, however there is no more temporal factor, since we have no piece of information about the termination of a whiled command. ω Cm (T + 1, X 1 , X 2 , X 3 ) ≥ ω Cm (T, X 1 , X 2 , θ * (X 3 .add(X 2 )))

with T is a fresh variable. Since θ(add)( 1 , 2 ) = 1 + 2 is a sup-interpretation of the method add, previous inequality is satisfied by taking ω Cm (T, 1 , 2 , 3 ) = T × 3 + 1 + 2 and the program is brotherly.

Example 2 . 1 :

 21 Here is an example of a program of our language: Class Position { var X; var Y ; Position(x, y) {X := x; Y := y; } move(x, y) {X := X.add(x); Y := Y.add(y) ; return X; } getX() {skip ; return X; } } Class main { var W ; var U ; var V ; Var Z; Cm 1 : V := new Position(W, U ); Cm 2 : Z := V.move(W, W ); Cm 3 : U := V.getX(); }

Figure 1 : 2 . 2 : 1 AssignmentsDefinition 3 . 1 :

 122131 Figure 1: Call-by-value semantics

2 .

 2 If e is a sequence of expressions e 1 , • • • , e k , I * (e) = I * (e 1 ), . . . , I * (e k ).

3 . 4 . 3 . 2 : 3 . 3 :

 343233 If C is a symbol in Class of arity m and e 1 , • • • , e m are expressions, then, we have: I * (new C(e 1 , • • • , e m )) = I(C)(I * (e 1 ), . . . , I * (e m )) If f ∈ F -Class is a symbol of arity m and e 1 , • • • , e m are expressions, then, we have:I * (X.f(e 1 , • • • , e m )) = I(f)(I * (e 1 ), . . . , I * (e m ), X)Notice that the assignment I * (e) of an expression e with m parameters x occurring in a class C having n attributes denotes a function from (R + ) n+m → R + . Consequently, we use the notation I * (e)(X 1 , • • • , X n , x) when we apply such a function.Definition Let Max-Poly {R + } be the set of functions defined to be constant functions in R + , projections, max, +, × and closed by composition. Given a class with n attributes, an assignment I is said to be polynomial if for every symbol b of dom(I), I(b) is a function of Max-Poly {R + }.Definition The assignment of a class symbol C ∈ Class of arity m > 0 is additive if

Definition 3 . 4 : 3 . 1 :

 3431 The size of an expression e is noted |e| and defined by |e| = 0 if e is a 0-ary symbol and |b(e 1 , . . . , e m )| = 1 + i |e i | if e = b(e 1 , . . . , e m ) with m > 0.Lemma Given a program p having an additive assignment I, there is a constant α such that for each object v ∈ Objects, the following inequality is satisfied:|v| ≤ I * (v) ≤ α × |v|Proof: Define α = max c∈C (β c ) where β c is taken to be the constant α c of definition 3.1 if c is of strictly positive arity and β c is equal to the constant I * (c) otherwise. The inequalities follow directly by induction on the size of a value.

Theorem 4 . 1 : 1 ;var X 2 ;var X 3 ;

 41123 Given a brotherly program p of main class Class main {A; Cm} having n attributes X 1 , • • • , X n , there exists a polynomial P such that for any store σ if Cm, σ → σ thenP (|X 1 σ|, . . . , |X n σ|) ≥ max i=1..n (|X i σ |)Example 4.5: The program of example 2.1 is brotherly since it admits a polynomial sup-interpretation θ and it has no looped and whiled command.Example 4.6: Consider the following program, over unary numbers:Class main { var X loop X 1 { X 3 := X 3 .add(X 2 ); } ; } Cm = loop X 1 {X 3 := X 3 .add(X 2 )} is the only minimum, flat and looped command. Applying the brotherly criterion, we have to find a polynomial weight ω Cm and a polynomial sup-interpretation θ such that:

  Cm 1 else Cm 2 | while e {Cm}

	Methods	M	::= f(x 1 , ..., x n ) {Cm ; return X; }
	Class	C	::= Class C {A ; Cons ; M 1 ; . . . ; M n ; }
		main ::= Class main {A ; Cm}

  minimum if there are no commands Cm 1 and Cm 2 and no expression e such that Cm = Cm 1 ; Cm 2 or Cm = if e then Cm 1 else Cm 2 • whiled if there is a command Cm 1 = while e {Cm 2 } such that Cm Cm 1 or Cm 1 Cm • looped if if there is a command Cm 1 = loop X {Cm 2 } such that Cm Cm 1 and the command Cm 2 is not whiled. Given a program p having a main class with n attributes, the weight of a command ω is a partial mapping. It assigns to: • every flat, minimum and looped command Cm, a total function ω Cm from (R + ) n+1 to R + • every flat, minimum and whiled command Cm, a total function ω Cm from (R + ) n to R + Cm is weakly monotonic ∀i, i ≥ i ⇒ ω Cm (. . . , i , . . .) ≥ ω Cm (. . . , i , . . .) 2. ω Cm has the subterm property ∀i, ∀ i ∈ R + ω Cm (. . . , i , . . .) ≥ i A weight ω is polynomial if each ω Cm is a function of Max-Poly {R + }.

	Definition 3.7: which satisfy: 1. ω