President Michel Cosnard

Gilles De Keulenaer

This report is the sole result of the unit's evaluation by the expert committee, the composition of which is specified below. The assessments contained herein are the expression of an independent and collegial reviewing by the committee.

UNIT PRESENTATION

INTRODUCTION HISTORY AND GEOGRAPHICAL LOCATION OF THE UNIT

The new MASCOT research unit will be a merger of the former UMR-S 942 and UMR-S 1165. The unit will be located in Hôpital Lariboisière and in Bobigny University.

MANAGEMENT TEAM

The director of the unit will be Mr Alexandre Mebazaa and the deputy director Mr Alain Cohan Solal.

HCERES NOMENCLATURE

SVE6 Santé Publique, Épidémiologie, Recherche Clinique.

SCIENTIFIC DOMAIN

The new MASCOT Unit is a merger of two previously successful research teams, to develop an original research program aiming at identifying biotargets derived from biomarkers in cardiovascular disease, cancer and cardio-oncological medical issues. The Mascot unit will consist of 2 teams, unified around the translation of biomarkers into biotherapies.

Team 1, named "Biotargets for cardiovascular dysfunction" will investigate new targets and biotherapies in cardiovascular diseases, especially in acute cardiac diseases.

Team 2, named "Cardiovascular biotargets in oncology" will study biomarkers of toxicity and resistance to anti-cancer agents in endothelium and cancer stem cells in order develop therapies to improve anticancer safety and efficacy.

UNIT WORKFORCE

Unit

GLOBAL ASSESSMENT OF THE UNIT

Over the past 5 years, the two merging teams made independently solid scientific discoveries with regard to the metabolism of natriuretic peptides, biomarkers in acute cardiac care, biotargets of cardiovascular fibrosis, cancer heterogeneity, cancer drug resistance and brain metastasis. These research activities are exemplified by the level of publication in high impact factor journals, some of them being renowned as breakthroughs, by the number of review papers, of invited conference, of international collaboration. The PhD students are contributory to the outputs of the teams and could be more numerous regarding the number of authorised scientists. This research resulted in significant interactions with industry, showing significant translational potential of the scientific activities.

By allying both teams in the new MASCOT unit, new research opportunities are created; clinical and basic scientific expertise in two fields of medicine (with overlapping interests in biomarkers and biotargets) will be combined. The strength of the MASCOT team will be a unique intellectual and technical cross-fertilization, finding direct clinical applications in the new clinical field of cardio-oncology, and in the vascular origin of cancer drug resistance and metastasis. The research program is ambitious, involving both clinical and basic scientific approaches. The MASCOT unit may become an attraction pole for researchers with divergent scientific expertise. Its establishment is strongly supported by official representatives from INSERM, Universities and Hospital.

The challenge of MASCOT will be to realize the above projects and scientific program with a high ratio of clinicians vs permanent researchers, which may be considered as a weakness. Also, the current geographical spread of the two teams between Bobigny and Lariboisière will make the collaboration of the two teams more challenging.

The evaluation reports of Hceres are available online: www.hceres.com

Evaluation of clusters of higher education and research institutions Evaluation of higher education and research institutions Evaluation of research Evaluation of doctoral schools Evaluation of programmes International evaluation and accreditation

HCERES scientific officer: Mr Serge BRIANÇON Representatives of supervising institutions and bodies:

	Unit name:	cardiovascular MArkers in Stressed COndiTions
	Unit acronym:	MASCOT
	Requested label:
	Application type:	Restructuration
	Current number:
	Head of the unit (until 31/12/2018):	Mr Alain COHEN SOLAL (Unit U942); Ms Anne JANIN (Unit 1165)
	Project leader (2019-2023):	Mr Alexandre MEBAZAA
	Number of teams or themes: 2
	COMMITTEE MEMBERS
		Ms Inès AMADO, Itmo biotechnology Aviesan
		Mr Jean-Luc DUMAS, Faculté de médecine, Université Paris 13
		Ms Bénédicte ISABEY, GH Lariboisière Fernand-Widal
		Ms Laurence LHOMME, INSERM
		Mr Jean-Luc TANDONNET, Hôpitaux Universitaires Paris Seine-Saint-Denis
		Ms Sylvie ROUSSET, Université Paris Diderot
		Mr Philippe RUZNIEWSKI, Faculté de médecine, Université Paris Diderot

Chair:

Mr Gilles De KEULENAER, Université d'Anvers, Belgique Experts: Mr Benoit LEPAGE, CHU Toulouse (representative of INSERM CSS) Ms Huguette LOUIS, Université de Lorraine (supporting personnel) Mr Gilles PAGES, Université de Nice Mr Emmanuel SAMAIN, Université de Besançon (representative of CNU) Ms Isabelle SOUBEYRAN, Institut Bergonié Bordeaux cardiovascular MArkers in Stressed COndiTions, MASCOT, U Paris 7, INSERM, Mr Alexandre MEBAZAA


President Michel Cosnard

Bruno Weber

The president of HCERES "countersigns the evaluation reports set up by the experts committees and signed by their chairman." (Article 8, paragraph 5); 2 The evaluation reports "are signed by the chairman of the expert committee". (Article 11, paragraph 2).

This report is the sole result of the unit's evaluation by the expert committee, the composition of which is specified below. The assessments contained herein are the expression of an independent and collegial reviewing by the committee.

UNIT PRESENTATION

SCIENTIFIC DOMAIN

Among the many methods applied in the unit today are molecular analyses, intracellular recording, cellular imaging, multielectrode recordings, behavioural assessments and informatics. These methods are used to study a wide range of neuroscience topics, spanning from memory systems, brain-machine interface, sleep and neuropathology of pain and neurodegeneration such as Alzheimer's and Parkinson's disease.

There is a thematic convergence of the teams, which all work on brain plasticity and neuromodulation, and their implications in the disease physiology. The teams use complementary techniques, approaches and organisms.

Team 1 -Genes and Dynamics of Memory Systems (GDMS) -Learning and memory in the fruitfly, with a novel strong focus on the interaction between memory and energy metabolism.

Team 2 -Genes, Circuits, Rhythms and Neuropathology (GCRN) -Investigations on the role of neurotransmitters, in particular dopamine, in the drosophila brain with a particular focus on Parkinson's disease pathophysiology.

Team 3 -Memory, Oscillations and Brain States (MOBS) -The group investigates neuronal mechanisms of memory consolidation during sleep.

Team 4 -Brain-Computer Interfaces (BCI) team -Brain computer interfaces to investigate neurophysiological processes in feedback learning and to develop new neurofeedback applications in patients.

INTRODUCTION

  HISTORY AND GEOGRAPHICAL LOCATION OF THE UNIT Neurobiology research was established at ESPCI in 1995 under the drive of Mr Pierre-Gilles dE GENNES, ESPCI director and Nobel prize laureate. Mr Jean ROSSIER was appointed as the first director of the Neurobiology laboratory. In 2004, Mr Jacques PROST, ESPCI director, and Mr Claude BOCCARA, scientific director, invited Mr Thomas PREAT to join ESPCI. His team moved in in 2006, coming from the Institut Alfred Fessard (CNRS, Gif-sur-Yvette). Under the direction of Mr Serge BIRMAN there was a transition period between the old structure run by Mr Jean ROSSIER and the new laboratory composed of autonomous teams. Since January 2012 Mr Thomas PREAT acts as director of the unit, which is now called laboratory of Brain Plasticity. ESPCI is located in central Paris and is a major institution of higher education (a French "Grande école d'ingénieurs"), consisting of 9 units, one of which is the Brain Plasticity unit. MANAGEMENT TEAM Mr Thomas PREAT, director of unit. No deputy. HCERES NOMENCLATURE SVE4_1 Neurologie.

Team 5 -

 5 Pain and Neural Adaptation (PNA) -Using the mouse for investigating pain

HCERES scientific officer: Ms Catherine HEURTEAUX Representatives of supervising institutions and bodies:

	Unit name:	Brain Plasticity
	Unit acronym:
	Requested label:	UMR
	Application type:	Renewal
	Current number:	8249
	Head of the unit (2017-2018):	Mr Thomas PREAT
	Project leader (2019-2023):	Mr Thomas PREAT
	Number of teams or themes: Five
	COMMITTEE MEMBERS
	Chair:	Mr Bruno WEBER, University of Zurich, Switzerland
	Experts:	Mr Olivier BERTRAND, Université de Lyon
		Mr Michaël DEMARQUE, Institut des Neurosciences Paris-Saclay
		(representative of CoNRS)
		Mr Alain ESCHALIER, Université Clermont Auvergne
		Mr Alberto FERRUS, Cajal Institute Madrid, Spain
		Ms Ilona GRUNWALD KADOW, Technical University of Munich, Germany
		Mr Yann HUMEAU, IINS, CNRS/Université de Bordeaux
		Mr Rémi SOUCHON, INSERM (supporting personnel)
		Mr Jean-François JOANNY, ESPCI
		Mr Bernard POULAIN, CNRS

GLOBAL ASSESSMENT OF THE UNIT

The Brain Plasticity unit -consisting of five teams -is a top level scientific institute with complementary approaches and animal models. In particular, teams 1 and 3 are world leaders in their fields. The questions addressed by the teams are situated within a common framework that refers to brain plasticity and neuromodulation. Scientific output of the unit as a whole is excellent, in several teams outstanding, with numerous scientific papers published in high impact journals. Two teams are financially supported by the most prestigious ERC grants. Some teams of the unit perform outstandingly outside the academic field, e.g. have strong links to industry and strong media coverage. The unit will be restructured due to the departure of a team leader. The upcoming major building and reconstruction activities at ESPCI will pose a great challenge to the unit. A good strategy and above all a strong communication between the ESPCI direction and the unit before and during this period is therefore of high importance.

The evaluation reports of Hceres are available online : www.hceres.com

Evaluation of clusters of higher education and research institutions Evaluation of higher education and research institutions Evaluation of research Evaluation of doctoral schools Evaluation of programmes Evaluation abroad


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

Romain Péchoux
email: romain.pechoux@loria.fr

Resource Analysis by Sup-interpretation

We propose a new method to control memory resources by static analysis. For this, we introduce the notion of sup-interpretation which bounds from above the size of function outputs. We establish a criteria for which the stack frame size is polynomially bounded. The criteria analyses terminating as well as non-terminating programs. This method applies to first order functional programming with pattern matching. This work is related to quasi-interpretations but we are now able to determine resources of different algorithms and it is easier to perform an analysis with this new tools.

Introduction

This paper deals with general investigation on program complexity analysis. It introduces the notion of sup-interpretation, a new tool that provides an upper bound on the size of every stack frame if the program is non-terminating, and establishes an upper bound on the size of function outputs if the program is terminating.

A sup-interpretation of a program is a partial assignment of function symbols, which ranges over reals and which bounds the size of the computed values.

The practical issue is to provide program static analysis in order to guarantee space resources that a program consumes during an execution. There is no need to say that this is crucial for at least many critical applications, and have strong impact in computer security. There are several approaches which are trying to solve the same problem. The first protection mechanism is by monitoring computations. However, if the monitor is compiled with the program, it could crash unpredictably by memory leak. The second is the testing-based approach, which is complementary to static analysis. Indeed, testing provides a lower bound on the memory while static analysis gives an upper bound. The gap between both bounds is of some value in practical applications (See [START_REF] Regehr | Say no to stack overflow[END_REF] for an interesting discussion). Lastly, the third approach is type checking done by a bytecode verifier. In an untrusted environment (like embedded systems), the type protection policy (Java or .Net) does not allow dynamic allocation. Our approach is an attempt to control resources, and provide a proof certificate, of a high-level language in such a way that the compiled code is safe wrt memory overflow. Thus, we capture and deal with memory allocation features. Similar approaches are the one by Hofmann [START_REF] Hofmann | Linear types and non-size-increasing polynomial time computation[END_REF][START_REF] Hofmann | A type system for bounded space and functional in-place update[END_REF] and the one by Aspinall and Compagnoni [START_REF] Aspinall | Heap bounded assembly language[END_REF].

For that purpose we consider first order functional programming language with pattern matching but we firmly believe that such a method could be applied to other languages such as resource bytecode verifier by following the lines of [START_REF] Amadio | A functional scenario for bytecode verification of resource bounds[END_REF], language with synchronous cooperative threads as in [START_REF] Amadio | Resource control for synchronous cooperative threads[END_REF] or first order functional language including streams as in [START_REF] Frankau | Stream processing hardware from functional language specifications[END_REF] .

The notion of sup-interpretation can be seen as a kind of annotation provided in the code by the programmer. Sup-interpretations strongly inherit from the notion of quasi-interpretation developed by Bonfante, Marion and Moyen in [START_REF] Bonfante | On lexicographic termination ordering with space bound certifications[END_REF][START_REF] Bonfante | Quasi-interpretation a way to control resources[END_REF][START_REF] Marion | Efficient first order functional program interpreter with time bound certifications[END_REF]. Consequently the notion of sup-interpretation comes from the notion of polynomial interpretation used to prove termination of programs in [START_REF] Dershowitz | Termination of rewriting[END_REF][START_REF] Lankford | On proving term rewriting systems are noetherien[END_REF] and more recently in [START_REF] Bonfante | Algorithms with polynomial interpretation termination proof[END_REF][START_REF] Lucas | Polynomials over the reals in proofs of termination: from theory to practice[END_REF]. Quasi-interpretation, like sup-interpretation, provides a bound over function outputs by static analysis for first order functional programs and allows the programmer to find a bound on the size of every stack frame. Quasiinterpretation was developed with the aim to pay more attention to the algorithmic aspects of complexity than to the functional (or extensional) one and then it is part of study of the implicit complexity of programs.

However the notions of sup-interpretation and quasi-interpretation differ for two reasons. First, the sup-interpretations are partial assignments which do not satisfy the subterm property, and this allows to capture a larger class of algorithms. In fact, programs computing logarithm or division admits a supinterpretation but have no quasi-interpretation. Second, the sup-interpretation is a partial assignment over the set of function symbols of a program, whereas the quasi-interpretation is a total assignment on function symbols. On the other hand, sup-interpretations come with a companion, which is a weight to measure argument size of recursive calls involved in a program run. In order to obtain a polynomial space bound, some constraints are developed over weights and sup-interpretations using the underlying notion of dependency pairs by Arts and Giesl [START_REF] Arts | Termination of term rewriting using dependency pairs[END_REF]. The dependency pairs were initially introduced for proving termination of term rewriting systems automatically. Even if this paper no longer focuses on termination, the notion of dependency pair is used for forcing the program to compute in polynomial space. There is a very strong relation between termination and computational complexity. Indeed, in order to prove some complexity bounds and termination, we need to control the arguments occurring in a function recursive call. Since we try to control together the arguments of a recursive call, the sup-interpretation is closer to the dependency pairs method than to the size-change principle method of [START_REF] Chin | The size-change principle for program termination[END_REF] which consider the arguments of a recursive call separately (See more rencently [START_REF] Hugh | Affined-based size-change termination[END_REF]). Section 2 introduces the first order functional language and its semantics. Section 3 defines the main notions of sup-interpretation and weight used to bound the size of a program outputs. Section 4 presents the notion of fraternity used to control the size of values added by recursive calls. In section 5, we define the notion of polynomial and additive assignments for sup-interpretations and weights. Finally, section 6 introduces the notion of friendly programs and the main theorems of this paper providing a polynomial bound on the values computed by friendly programs. The full paper with all proofs is available at http://www.loria.fr/ ∼ pechoux. The appendix of the full paper presents examples of friendly programs, an example of non-friendly program and some examples over streams.

First Order Functional Programming

Syntax of Programs

We define a generic first order functional programming language. The vocabulary Σ = Cns, Op, Fct is composed of three disjoint domains of symbols. The arity of a symbol is the number n of arguments that it takes. The set of programs are defined by the following grammar.

Programs p ::= def 1 , • • • , def m Definitions def ::= f(x 1 , • • • , x n ) = e f Expression e ::= x | c(e 1 , • • • , e n ) | op(e 1 , • • • , e n ) | f(e 1 , • • • , e n ) | Case e 1 , • • • , e n of p 1 → e 1 . . . p → e Patterns p ::= x | c(p 1 , • • • , p n )
where c ∈ Cns is a constructor, op ∈ Op is an operator, f ∈ Fct is a function symbol, and p i is a sequence of n patterns. Throughout, we generalize this notation to expressions and we write e to express a sequence of expressions, that is e = e 1 , . . . , e n , for some n clearly determined by the context. The set of variables Var is disjoint from Σ and x ∈ Var. In a definition, e f is called the body of f. A variable of e f is either a variable in the parameter list x 1 , • • • , x n of the definition of f or a variable which occurs in a pattern of a case definition. In a case expression, patterns are not overlapping. The program's main function symbol is the first function symbol in the program's list of definitions. We usually don't make the distinction between this main symbol and the program symbol p.

Lastly, it is convenient, because it avoids tedious details, to restrict case definitions in such a way that an expression involved in a Case expression does not contain nested Case (In other words, an expression e j does not contain an expression Case ). This is not a severe restriction since a program involving nested Case can be transformed in linear time in its size into an equivalent program without the nested case construction.

Semantics

The set Values is the constructor algebra freely generated from Cns.

Values v ::= c | c(v 1 , • • • , v n ) c ∈ Cns Put Values * = Values ∪ {Err}
where Err is the value associated to an error. Each operator op of arity n is interpreted by a function op from Values n to Values * . Operators are essentially basic partial functions like destructors or characteristic functions of predicates like =. The destructor tl illustrates the purpose of Err when it satisfies tl(nil) = Err.

The computational domain is Values # = Values ∪ {Err, ⊥} where ⊥ means that a program is non-terminating. The language has a closure-based call-byvalue semantics which is displayed in Figure 1. A few comments are necessary. A substitution σ is a finite function from variables to Values. The application of a substitution σ to an expression e is noted eσ. The meaning of e ↓ w is that e evaluates to the value w of Values * . If no rule is applicable, then an error occurs, and e ↓ Err. So, a program p computes a partial function p :

t1 ↓ w1 . . . tn ↓ wn c ∈ Cns and ∀i, wi = Err c(t1, • • • , tn) ↓ c(w1, • • • , wn) t1 ↓ w1 . . . tn ↓ wn op ∈ Op and ∀i, wi = Err op(t1, • • • , tn) ↓ op (w1, • • • , wn) e ↓ u ∃σ, i : piσ = u eiσ ↓ w Case and u = Err Case e of p1 → e1 . . . p → e ↓ w e1 ↓ w1 . . . en ↓ wn f(x1, • • • , xn) = e f e f σ ↓ w where σ(xi) = wi f(e1, • • • , en) ↓ w = Err and w = Err
Values n → Values # defined as follows. For all v i ∈ Values, p (v 1 , • • • , v n ) = w iff p(v 1 , • • • , v n ) ↓ w. Otherwise p (v 1 , • • • , v n ) = ⊥. Throughout, we shall say that p (v 1 , • • • , v n ) is defined when p (v 1 , • • • , v n ) is a constructor term of Values.
3 Sup-interpretations

Partial Assignment

A partial assignment θ is a partial mapping from a vocabulary Σ such that for each symbol f of arity n, in the domain of θ, it yields a partial function θ(f ) : (R) n -→ R. The domain of a partial assignment θ is noted dom(θ). Because it is convenient, we shall always assume that partial assignments that we consider, are defined on constructors and operators. That is Cns ∪ Op ⊆ dom(θ).

An expression e is defined over dom(θ) if each symbol belongs to dom(θ) or is a variable of Var. Take a denumerable sequence X 1 , . . . , X n , . . .. Assume that an expression e is defined over dom(θ) and has n variables. The partial assignment of e wrt θ is the extension of the assignment θ to the expression e that we write θ * (e). It denotes a function from R n to R and is defined as follows:

1. If x i is a variable of Var, let θ * (x i ) = X i 2. If b is a 0-ary symbol of Σ, then θ * (b) = θ(b).
θ * (f (e 1 , • • • , e n )) = θ(f )(θ * (e 1 ), . . . , θ * (e n ))

Sup-interpretation Definition 1 (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 f ∈ dom(θ), the function θ(f

) satisfies ∀i = 1, . . . , n X i ≥ Y i ⇒ θ(f )(X 1 , • • • , X n ) ≥ θ(f )(Y 1 , • • • , Y n ) 2. For each v ∈ Values, θ * (v) ≥ |v|
The size of an expression e is noted |e| and is defined by |c| = 0 where c is a 0-ary symbol and |b(e 1 , . . . , e n )| = 1 + i |e i | where b is a n-ary symbol.

For each symbol f ∈ dom(θ) of arity n and for each value

v 1 , . . . , v n of Values, if f (v 1 , . . . , v n ) is defined, that is f (v 1 , . . . , v n ) ∈ Values, then θ * (f (v 1 , . . . , v n )) ≥ θ * ( f (v 1 , . . . , v n ))
Now an expression e admits a sup-interpretation θ if e is defined over dom(θ).

The sup-interpretation of e wrt θ is θ * (e).

Intuitively, the sup-interpretation is a special program interpretation. Instead of yielding the program denotation, a sup-interpretation provides an approximation from above of the size of the outputs of the function denoted by the program. It is worth noticing that sup-interpretations are a complexity measure in the sense of Blum [START_REF] Blum | A machine-independent theory of the complexity of recursive functions[END_REF].

Lemma 1. Let e be an expression with no variable and which admits a supinterpretation θ.

Assume that e is defined. We then have In this example, the function half computes n/2 on an entry of size n. So by taking θ(S)(X) = X+1 and θ(half)(X) = X/2, we define a sup-interpretation of the function symbol half. In fact, both functions are monotonic. For every unary value v of size n, θ * (v) = n ≥ n = |v| by definition of θ(S), so that condition 2 on sup-interpretation is satisfied. Finally, it remains to check that for every value v, θ * (half(v)) ≥ θ * ( half(v) ). For a value v of size n, we have by definition of

θ * ( e ) ≤ θ * (e)
θ * that θ * (half(v)) = θ * (v)/2 = n/2 and θ * ( half(v) ) = half(v) = n/2 .
Since n/2 ≥ n/2 , condition 3 of sup-interpretation is satisfied. Notice that such a sup-interpretation is not a quasi-interpretation (a fortiori not an interpretation for proof termination) since it does not have the subterm property (see below for a definition of this property).

Weight

The weight allows us to control the size of the arguments in recursive calls. A weight is an assignment having the subterm property but no longer giving a bound on the size of a value computed by a function. Intuitively, whereas the sup-interpretation controls the size of the computed values, the weight can be seen as a control point for the computation of recursive calls.

Definition 2 (Weight).

A weight ω is a partial assignment which ranges over Fct. To a given function symbol f of arity n it assigns a total function ω f from R n to R which satisfies:

1. ω f is weakly monotonic. ∀i = 1, . . . , n, X i ≥ Y i ⇒ ω f (. . . , X i , . . .) ≥ ω f (. . . , Y i , . . .) 2. ω f has the subterm property ∀i = 1, . . . , n, ω f (. . . , X i , . . .) ≥ X i
The weight of a function is often taken to be the maximum or the sum functions.

The monotonicity property combined with the fact that a weight ranges over function symbols ensures suitable properties on the number of occurrences of a loop in a program when we consider the constraints given in section 6. Moreover, the subterm property allows to control the size of each argument in a recursive call, in opposition to the size-change principle as mentioned in the introduction.

Fraternities

In this section we define fraternities which are an important notion based on dependency pairs, that Arts and Giesl [START_REF] Arts | Termination of term rewriting using dependency pairs[END_REF] introduced to prove termination automatically. Fraternities allow to tame the size of arguments of recursive calls.

A context is an expression C[ 1 , • • • , r ] containing one occurrence of each i . Here, we suppose that the i 's are new symbols which are not in Σ nor in Var. -If e f is a compositional expression (that is with no case definition inside it), then

The substitution of each i by an expression d

i is noted C[d 1 , • • • , d r ]. Definition 3. Assume that f(x 1 , • • • , x n ) = e f is
e f = C[d]. In this case, p 1 = x 1 . . . p n = x n . -Otherwise, e f = Case e 1 , • • • , e n of q 1 → e 1 .
. . q → e , then there is a position j such that e j = C[d]. In this case, p 1 = q j,1 . . . p n = q j,n where q j = q j,1 . . . q j,n .

At first glance, this definition may look a bit tedious. However, it is convenient in order to predict the computational data flow involved. Indeed, an expression is activated by

f(p 1 , • • • , p n ) when f(v 1 , • • • , v n
) is called and each v i matches the corresponding pattern p i . The notion of activated expression provides a precedence ≥ Fct on function symbols. Indeed, set f ≥ Fct g if there are e and p such that g(e) is activated by f(p). Then, take the reflexive and transitive closure of ≥ Fct , that we also note ≥ Fct . It is not difficult to establish that ≥ Fct is a preorder. Next, say that f ≈ Fct g if f ≥ Fct g and inversely g ≥ Fct f. Lastly, f > Fct g if f ≥ Fct g and g ≥ Fct f does not hold.

Intuitively, f ≥ Fct g means that f calls g in some executions. And f ≈ Fct g means that f and g call themselves recursively.

Say that an expression d activated by

f(p 1 , • • • , p n ) is maximal if there is no context C[ ], distinct from the empty context, such that C[d] is activated by f(p 1 , • • • , p n ).

Definition 4. In a program p, an expression

d = C[g 1 (e 1 ), . . . , g r (e r )] activated by f(p 1 , • • • , p n ) is a fraternity if 1. d is maximal 2. For each i ∈ {1, r}, g i ≈ Fct f.

For every function symbol h that appears in the context

C[ 1 , • • • , r ], we have f > Fct h.
All along, we suppose that there is no nested fraternities, which means that a fraternity d does not contain any fraternity inside it. This restriction prevents definitions of the shape f(S(x)) = f(f(x)). This restriction is not too strong since such functions are not that natural in a programming perspective and either they have to be really restricted or they rapidly generate complex functions like the Ackermann one. The following examples illustrate typical fraternity constructions. This program admits two fraternities minus(u, v) and S[q(minus(z, u), S(u))] since q > Fct minus.

= f, u 1 , • • • , u n and η 2 = g, v 1 , • • • , v k are two states. Assume also that C[g(e 1 , • • • , e k )] is activated by f(p 1 , • • • , p n ). A transition is a triplet η 1 C[ ] η 2 such that:
1. There is a substitution σ such that p i σ = u i for i = 1, . . . , n, 2. and e j σ = v j for j = 1...k.

We call such a graph a call-tree of f over values u 1 , . . . , u n if f, u 1 , • • • , u n is its root. A state may be seen as a stack frame. A call-tree of root f, u 1 , • • • , u n represents all the stack frames which will be pushed on the stack when we compute f(u 1 , . . . , u n ).

Polynomial Assignments

Definition 6. A partial assignment θ is polynomial if for each symbol f of arity n of dom(θ), θ(f ) is bounded by a polynomial of R[X 1 , • • • , X n ]. A polynomial sup-interpretation is a polynomial assignment. A polynomial weight ω of arity n is a weight which is bounded by some polynomial of R[X 1 , • • • , X n ]. An assignment of c ∈ dom(θ) is additive if θ(c)(X 1 , • • • , X n ) = n i=1 X i + α c α c ≥ 1
If the polynomial assignment of each constructor is additive then the assignment is additive. Throughout the following paper we consider additive assignments. As a consequence we have the following lemma: Lemma 2. There is a constant α such that for each value v of Values, the inequality is satisfied :

|v| ≤ θ * (v) ≤ α|v|

Local Criteria to Control Space Resources

Definition 7 (Friendly). A program p is friendly iff there is a polynomial sup-interpretation θ and a polynomial weight ω such that for each fraternity expression d = C[g 1 (e 1 ), . . . , g r (e r )] activated by f(p

1 • • • , p n ) we have, θ * (C[ 1 , . . . , r ]) = max i=1..r ( i + R i (Y 1 , . . . , Y m ))
with R i polynomials where each Y i corresponds to a variable occurring in C.

Moreover, for each i ∈ {1, r}, we have that for each substitution σ,

ω f (θ * (p 1 σ), . . . , θ * (p n σ)) ≥ ω g i (θ * (e i,1 σ), . . . , θ * (e i,m σ)) Moreover, if ∃σ ω f (θ * (p 1 σ), . . . , θ * (p n σ)) = ω g i (θ * (e i,1 σ), . . . , θ * (e i,m σ)) Then R i (Y 1 , . . . , Y m ) is the null polynomial.
Example 4. The program of example 2 is friendly. We take θ(S)(X) = X + 1 and θ(half)(X) = X/2. The contexts of the two fraternities involved in this program are S[ ], thus having a sup-interpretation θ * (S[ ]) = + 1. We have to find ω log and ω half such that for every σ:

ω log (θ * (S(yσ))) > ω log (θ * (half(S(yσ)))) ω half (θ * (S(S(yσ)))) > ω half (θ * (yσ))
Both inequalities are satisfied by taking ω log (X) = ω half (X) = X. Thus the program is friendly.

Example 5. The program of example 3 is friendly by taking θ(S)(X) = X + 1, θ(minus)(X, Y ) = X, ω minus (X, Y ) = max(X, Y ) and ω q (X, Y ) = X + Y . An example of an unfriendly program is given in the full paper. The next result strengthens Theorem above. Indeed it claims that even if a program is not terminating then the intermediate values are polynomially bounded. This is quite interesting because non-terminating process are common, and moreover it is not difficult to introduce streams with a slight modification of the above Theorem, which is essentially based on the semantics change.

Theorem 2. Assume that p is a friendly program. For each function symbol f of p there is a polynomial R such that for every node g,

u 1 , • • • , u m of the call-tree of root f, v 1 , • • • , v n , max j=1..m (|u j |) ≤ R(max(|v 1 |, ..., |v n |)) even if f(v 1 , . . . , v n ) is not defined.
Proof. The proof is in the full paper and is a consequence of previous theorem since in every state of the call-tree, the values are computed and thus bounded polynomially.

Remark 1. As mentioned above, this theorem holds for non-terminating programs and particularly for a class of programs including streams. For that purpose we have to give a new definition of substitutions over streams. In fact, it would be meaningless to consider a substitution over stream variables. Thus stream variables are never substituted and the sup-interpretation of a stream l is taken to be a new variable L as in the definition of the sup-interpretations.

Example 6 (Streams)

. Let e::l be a stream with :: a stream constructor symbol, e an expression (the head of the stream) and l a stream variable (the tail of the stram) and suppose that we have already defined a semantics over streams in a classical way. addstream(x, y) = Case x, y of z :: l, u :: l → add(z, u) :: addstream(l, l ) Then this (merging) program is friendly by taking θ * (l) = L, θ(add)(X, Y ) = X + Y , θ * (x :: l) = θ * (x) + L + 1 and ω addstream (X, Y ) = X + Y . Thus a variant of theorem 2 holds. The variation comes from the fact that it would be non-sense to consider streams as inputs, since the size of a stream is unbounded. Consequently, the inputs are chosen to be a restricted number of stream heads. In the same way, every mapping program over streams of the shape:

f(x) = Case x of z :: l → g(z) :: f(l)
is friendly if g represents a friendly program. Thus the variant of theorem 2 also applies. Moreover for all these programs we know that the values computed in the output streams (i.e. in the heads of right-hand side definition) are polynomially bounded in the size of some of the inputs (heads) since the computations involve only friendly functions over non-stream datas (else some parts of the program will never be evaluated). Finally an example of non-friendly program is:

f(x) = Case x of z :: l → f(z :: z :: l)
In fact, this program does not fit our requirements since it adds infinitely the head of the stream to its argument, computing thus an unbounded value.

Conclusion and Perspectives

The notion of sup-interpretation allows to check that the size of the outputs of a friendly program is bounded polynomially by the size of it inputs. It allows to capture algorithms admitting no quasi-interpretations (division, logarithm, gcd . . . ). So, our experiments show that is not too difficult to find sup-interpretations for the following reasons. First, we have to guess sup-interpretations and weights of only some, and not all, symbols. Second, a quasi-interpretations for those symbol works pretty well in most of the cases. And so we can use tools to synthesize quasiinterpretations [START_REF] Amadio | Max-plus quasi-interpretations[END_REF][START_REF] Bonfante | Synthesis of quasiinterpretations[END_REF]. Our works is related to semi-automatic procedure to analyse complexity, see for example Benzinger [START_REF] Benzinger | Automated higher-order complexity analysis[END_REF] for programs extracted from Nuprl or Debray et al. for logic programs [START_REF] Debray | Cost analysis of logic programs[END_REF].

Sup-interpretation should be easier to synthesize than quasi-interpretations since we have to find fewer assignments. Moreover it is not so hard to find a supinterpretation, since quasi-interpretation often defines a sup-interpretation, except in the case of additive contexts. Indeed, consider the program f(c(x, y)) = c(f(x), f(y)) defined over binary trees. It admits the identity function as quasiinterpretation. However it does not admit a sup-interpretation since its context should have an additive sup-interpretation. Which is clearly impossible in the friendly criteria. Hopefully this drawback only relies on the friendly criteria and not on the sup-interpretation itself. We are currently working on a more general criteria which should be able to capture such programs and whose aim is to capture entirely the class of programs admitting a quasi-interpretation. As a consequence every quasi-interpretation satisfying the friendly criteria is a sup-interpretation. A programmer is also interested in bounding the total number of stack frames. This issue is partially tackled in the full paper by showing that cycles of the call-tree corresponding to friendly programs with strict inequalities in the friendly criteria have a number of occurrences bounded by a polynomial in the size of the inputs. Since every occurence of a cycle is composed of a bounded number of states (which depends directly on the size of the program) and since every cycle occurs a polynomial number of times, we know that the corresponding call-tree will have a number of states bounded polynomially in the size of the inputs. Consequently, for such programs, both stack frame sizes and the number of stack-frames are polynomially bounded by the size of the inputs. The corresponding termination result strongly inherits in a natural way from the dependency pairs method of Arts and Giesl [START_REF] Arts | Termination of term rewriting using dependency pairs[END_REF]. However, it differs in the sense that the monotonicity of the quasi-ordering and the inequalities over definitions (rules) of a program are replaced by the notion of supinterpretation combined to weights. Consequently, it shares the same advantages and disadvantages than the dependency pairs method compared to termination methods such as size-change principle by Jones et al. [START_REF] Chin | The size-change principle for program termination[END_REF], failing on programs admitting no polynomial orderings (Ackermann function, for example), and managing to prove termination on programs where the size-change principle fails. For a more detailed comparison between both termination criteria see [START_REF] Thiemann | Size-change termination for term rewriting[END_REF]. Finally, an open question concerns characterization of time complexity classes with the use of such a tool, particularly, the characterization of polynomial time by determining a restriction on sup-interpretations.

M

  . Hagiya and P. Wadler (Eds.): FLOPS 2006, LNCS 3945, pp. 163-176, 2006. c Springer-Verlag Berlin Heidelberg 2006

Fig. 1 .

 1 Fig. 1. Call by value semantics of ground expressions wrt a program p

3 .

 3 If e is a sequence of n expressions, then θ * (e) = max(θ * (e 1 ), . . . , θ * (e n )) 4. If e is a Case expression of the shape Case e of p 1 → e 1 . . . p → e , θ * (e) = max(θ * (e), θ * (e 1 ), . . . , θ * (e )) 5. If f is a symbol of arity n > 0 and e 1 , • • • , e n are expressions, then

Corollary 1 .

 1 Proof. The proof is done by structural induction on expression. The base case is a consequence of Condition 2 of Definition 1.Take an expression e = f (e 1 , • • • , e n ) that has a sup-interpretation θ. By induction hypothesis (IH), we have θ * (e i ) ≥ θ * ( e i ). Now,θ * (e) = θ(f )(θ * (e 1 ), ..., θ * (e n )) by definition of θ * ≥ θ(f )(θ * ( e 1 ), ..., θ * ( e n ))by 1 of Dfn 1 and (IH) = θ * (f ( e 1 , ..., e n )) by definition of θ * ≥ θ * ( f ( e 1 , ..., e n )) by 3 of Dfn 1 = θ * ( e ) Given an expression e, we define e thus: e = | e | if e is defined 0 otherwise Let e be an expression with no variable and which admits a supinterpretation θ. Assume that e is defined. We then have e ≤ θ * (e) Proof. θ * (e) ≥ θ * ( e ) by Lemma 1 ≥ e by Condition 2 of Dfn 1 Example 1. half(x) = Case x of 0 → 0 S(0) → 0 S(S(y)) → S(half(y))

Example 2 .

 2 Consider the program log computing log 2 (n) + 1 on an entry of size n and using the program half of example 1. log(x) = Case x of 0 → 0 S(y) → S(log(half(S(y)))) half(x) = Case x of 0 → 0 S(0) → 0 S(S(y)) → S(half(y)) This program admits two fraternities S(log[half(S(y))]) and S[half(y)] since log > Fct half. Take S(log[half(S(y))]), this fraternity is decomposed into a context S(log[ ]) and an expression half(S(y)). Example 3 (division). Consider the following definitions that encode the division n/m on two entries of sizes n and m > 0: minus(x, y) = Case x, y of 0, z → 0 S(z), 0 → S(z) S(u), S(v) → minus(u, v)q(x, y) = Case x, y of 0, S(z) → 0 S(z), S(u) → S(q(minus(z, u), S(u)))

Theorem 1 .

 1 Assume that p is a friendly program. For each function symbol f of p there is a polynomial P such that for every value v 1 , . . . , v n ,f(v 1 , . . . , v n ) ≤ P (max(|v 1 |, ..., |v n |))Proof. The proof can be found in the full paper. It begins by assigning a polynomial P f to every function symbol f of a friendly program. This polynomial is the sum of a bound on the size of values added by the contexts of recursive calls and of a bound on the size of values added by the calls which are no longer recursive. Then it checks both bounds thus showing that the values computed by the program are polynomially bounded. The programs presented in examples 2 and 3 are examples of friendly programs and thus computing polynomially bounded values. More examples of friendly programs can be found in the appendix of the full paper.

  a definition of a program. An expression d is activated by f(p 1 , • • • , p n ) where the p i 's are patterns if there is a context with one hole C[ ] such that:

  Definition 5. A state is a tuple f, u 1 , • • • , u n where f is a function symbol of arity n and u 1 , . . . , u n are values. Assume that η 1