Patrick Baillot
email: patrick.baillot@ens-lyon.fr

Ugo Dal Lago
email: dallago@cs.unibo.it

Higher-order Interpretations and Program Complexity (Long Version)

. This fits in the area of implicit computational complexity, which aims at giving machine-free characterizations of complexity classes. Here we extend this approach to the higher-order setting. For that we consider the notion of simply typed term rewriting systems [2], we define higher-order polynomial interpretations (HOPI) for them and give a criterion based on HOPIs to ensure that a program can be executed in polynomial time. In order to obtain a criterion which is flexible enough to validate some interesting programs using higher-order primitives, we introduce a notion of polynomial quasiinterpretations, coupled with a simple termination criterion based on linear types and path-like orders.

Introduction

The problem of statically analyzing the performance of programs can be attacked in many different ways. One of them consists in inferring complexity properties of programs early in development cycle, when the latter are still expressed in high-level programming languages, like functional or object oriented idioms. And in this scenario, results from an area known as implicit computational complexity (ICC in the following) can be useful: they consist in characterizations of complexity classes in terms of paradigmatic programming languages (λ-calculus, term rewriting systems, etc.) or logical systems (proof-nets, natural deduction, etc.), from which static analysis methodologies can be distilled. Examples are type systems, path-orderings and variations on the interpretation method. The challenge here is defining ICC systems which are not only simple, but also intensionally powerful: many natural programs among those with bounded complexity, should be recognized as such by the ICC system, i.e., are actually programs of the system.

One of the most fertile direction in ICC is indeed the one in which programs are term rewriting systems (TRS in the following) [START_REF] Bonfante | Algorithms with polynomial interpretation termination proof[END_REF][START_REF] Bonfante | Quasi-interpretations a way to control resources[END_REF], whose complexity can be kept under control by way of variations of the powerful techniques developed to check termination of TRS, namely path orderings [START_REF] Plaisted | A recursively defined ordering for proving termination of term rewriting systems[END_REF][START_REF] Dershowitz | Orderings for term-rewriting systems[END_REF], dependency pairs and the interpretation method [START_REF] Lankford | On proving term rewriting systems are noetherian[END_REF]. Many different complexity classes have been characterized this way, from polynomial time to polynomial space, to exponential time to logarithmic space. And remarkably, many of the introduced characterizations are intensionally very powerful, in particular when the interpretation method is relaxed and coupled with recursive path orderings, like in quasi-interpretations [START_REF] Bonfante | Quasi-interpretations a way to control resources[END_REF].

The results cited above are very interesting and indeed represent the state-of-the art in resource analysis when programs are first-order functional programs, i.e. when functions are not firstclass citizens. If the class of programs of interest includes higher-order functional programs, the techniques above can only be applied if programs are either defunctionalized or somehow put in first-order form, for example by applying a translation scheme due to the second author and Simone Martini [START_REF] Lago | On constructor rewrite systems and the lambda-calculus[END_REF]. There is strong evidence, however, that first-order programs obtained as results of one of this translations schemes are difficult to prove to have bounded complexity with traditional TRS techniques.

Another possibility consists in generalizing TRS techniques to systems of higher-order rewriting, which come in many different flavours [START_REF] Jouannaud | A computation model for executable higher-order algebraic specification languages[END_REF][START_REF] Klop | Combinatory reduction systems: Introduction and survey[END_REF][START_REF] Yamada | Confluence and termination of simply typed term rewriting systems[END_REF]. The majority of the introduced higher-order generalization of rewriting are quite powerful but also complex from a computational point of view, being conceived to model not only programs but also proofs involving quantifiers. As an example, even computing the reduct of a term modulo a reduction rule can in some cases be undecidable. Higher-order generalizations of TRS techniques [START_REF] Jouannaud | The higher-order recursive path ordering[END_REF], in turn, reflect the complexity of the languages on top of which they are defined. Summing up, devising ICC systems this way seems quite hard.

In this paper, we consider one of the simplest higher-order generalizations of TRSs, namely Yamada's simply-typed term rewriting systems (STTRSs in the following), we define a system of higher-order polynomial interpretations for them and prove that, following [START_REF] Bonfante | Algorithms with polynomial interpretation termination proof[END_REF], this allows to exactly characterize, among others, the class of polynomial time computable functions. We show, however, that this way the class of (higher-order) programs which can be given a polynomial interpretation does not include interesting and natural examples, like foldl, and that this problem can be overcome by switching to another technique, designed along the lines of quasi-interpretations [START_REF] Bonfante | Quasi-interpretations a way to control resources[END_REF]. This is the subject of sections 4 and 5 below.

Another problem we address in this paper is related to the expressive power of simply-typed term rewriting systems. Despite their simplicity, simply-typed term rewriting systems subsume the simply typed lambda calculus and extensions of it with full recursion, like PCF. This can be proved following [START_REF] Lago | On constructor rewrite systems and the lambda-calculus[END_REF] and is the subject of Section 3.

2 Simply-Typed Term Rewriting Systems

Definitions and Notations

We recall here the definition of a STTRS, following [START_REF] Yamada | Confluence and termination of simply typed term rewriting systems[END_REF][START_REF] Aoto | Termination of simply typed term rewriting by translation and labelling[END_REF]. We will actually consider as programs a subclass of STTRSs, basically those where rules only deal with the particular case of a function symbol applied to a sequence of patterns. For first-order rewrite systems this corresponds to the notion of constructor rewrite system.

We consider a denumerable set of base types, which we call data-types and we shall denote as D, E, . . .. Types are defined by the following grammar:

A, B ::= D | A 1 × • • • × A n → A.
A functional type is a type which contains an occurrence of →. Some examples of base types are the type NAT of tally integers, and the type W 2 of binary words.

We denote by F the set of function symbols (or just functions), C that of constructors and X that of variables. Constructors c ∈ C have a type of the form

D 1 × • • • × D n → D. Functions f ∈ F,
on the other hand, can have any functional type. Variables x ∈ X can have any type. Terms are typed and defined by the following grammar:

t, t i := x A | c A | f A | (t A1ו••×An→A t A1 1 . . . t An n ) A where x A ∈ X , c A ∈ C, f A ∈ F.
We denote by T the set of terms. Observe how application is primitive and is in general treated differently from other function symbols. This is what make STTRSs different from ordinary TRSs. We define the size |t| of a term t as the number of symbols (elements of F ∪ C ∪ X ) it contains.

To simplify the writing of terms we will often elide their type. We will also write (t s) for (t s 1 . . . s n ). Therefore any term t is of the form (. . .

((α s 1 ) s 2 ) . . . s k ) where k ≥ 0, α ∈ X ∪ C ∪ F.
To simplify notation we will use the following convention: any term t is of the form (. . . ((s s 1 ) s 2 ) . . . s k ) will be written ((s s 1 . . . s k )). Observe however that, e.g., if t has type

A 1 × A 2 → (B 1 × B 2 → B), t i type A i for i = 1, 2, s i type B i for i = 1, 2,
then both (t t 1 t 2 ) and ((t t 1 t 2 ) s 1 s 2 ) are well-typed (with type B 1 × B 2 → B and B, respectively), but (t t 1 ) and (t t 1 t 2 s 1 ) are not well-typed.

A crucial class of terms are patterns, which in particular are used in defining rewriting rules. Formally, a pattern is a term generated by the following grammar:

p, p i := x A | (c D1×...×Dn→D p D1 1 . . . p Dn n ).
P is the set of all patterns. Observe that if a pattern has a functional type then it must be a variable. We consider rewriting rules in the form t → s satisfying the following two constraints:

1. t and s are terms of the same type A, F V (s) ⊆ F V (t), and any variable appears at most once in t. 2. t must have the form ((f p 1 . . . p k )) where each p i for i ∈ 1, . . . , k consists of patterns only. The rule is said to be a rule defining f, while the total number of patterns in p 1 , . . . , p k is the arity of the rule. Now, a simply-typed term rewriting system is a set R of orthogonal rewriting rules such that for every function symbol f, every rule defining f has the same arity, which is said to be the arity of f. A program P = (f, R) is given by a STTRS R and a chosen function symbol f ∈ F.

In the next section, a notion of reduction will be given which crucially relies on the concept of a value. More specifically, only values will be passed as arguments to functions. Formally, we say that a term is a value if either: 1. it has a type D and it has the form (c v 1 . . . v n ), where v 1 , . . . , v n are themselves values. 2. it has functional type A and is of the form ((f, v 1 . . . v n )), where the terms in v 1 , . . . v n are themselves values and the total number of terms in v 1 , . . . , v n is strictly smaller than the arity of f. We denote values as v, u and their set by V.

STTRSs: Dynamics

The dynamical process underlying a program is formalized through a rewriting relation. Preliminary to that are proper notions of unification and substitution, which are the subject of this section.

A substitution σ is a mapping from variables to values with a finite domain, and such that σ(x A ) has type A. A substitution σ is extended in the natural way to a function from V to T , that we shall also write σ. The image of a term t will be denoted tσ. Contexts are defined as terms but with the proviso that they must contain exactly one occurrence of a special constant • A (hole), for a type A. They are denoted as C, D . . . If C is a context with hole • A , and t is a term of type A, then C{t} is the term obtained from C by replacing the occurrence of • A by t.

Consider a STTRS R. We say that s reduces to t, denoted as s → R t, if there exists a rule l → r of R, a context C and a substitution σ such that s = C{lσ} and t = C{rσ}. When there is no ambiguity on R we will simply write → instead of → R .

Please notice that one of the advantages of STTRSs over similar formalisms (like [START_REF] Jouannaud | A computation model for executable higher-order algebraic specification languages[END_REF]) is precisely the simplicity of the underlying unification mechanism, which does not involve any notion of binding and is thus computationally simpler than higher-order matching. There is a price to pay in terms of expressivity, obviously. In the next section, however, we show how STTRSs are expressive enough to capture standard typed λ-calculi.

Typed λ-calculi as STTRSs

The goal of this Section is to illustrate the fact that the choice of the STTRS framework as higherorder calculus is not too restrictive: indeed we will show that we can simulate in it PCF equipped with weak reduction (i.e. where one does not reduce in the scope of abstractions). This is achieved using ideas developed for encodings of the λ-calculus into first-order rewrite systems [START_REF] Lago | On constructor rewrite systems and the lambda-calculus[END_REF].

A Few Words About PCF

We assume a total order ≤ on X . PCF types are defined as follows:

A, B ::= NAT | A → A.
PCF terms, on the other hand, are defined as follows:

M, N ::=x A | (λx A .M B ) A→B | (M A→B N A ) B | fix ((A→B)→A→B)→A→B | n NAT | succ NAT →NAT | pred NAT →NAT | (ifz M A N A ) NAT →A
where n ranges over the natural numbers. We omit types in terms whenever this does not cause ambiguity. A PCF value is any term different from an application. PCF values are indicated with metavariables like V and W . A call-by-value operational semantics for PCF can be expressed by way of some standard reduction rules:

(λx.M )V -→ M {V /x} fix V -→ V (λx.(fix V )x) succ n -→ n + 1 pred 0 -→ 0 pred n + 1 -→ n (ifz M N ) 0 -→ M (ifz M N ) n + 1 -→ N
The reduction rules above can be propagated to any applicative context by the rules below

M -→ N M L -→ N L M -→ N LM -→ LN

PCF as a STTRS

PCF can be turned into a STTRS R PCF with infinitely many function symbols. First, for each term M of type B, with free variables x 1 ≤ x 2 ≤ . . . ≤ x n of types A 1 , . . . , A n , and x of type A, we introduce a function abs M,x of F, with type

A 1 × • • • × A n → (A → B).
Then, for each pair of terms M, N of type B, both with free variables among x 1 ≤ x 2 ≤ . . . ≤ x n of types A 1 , . . . , A n , and x of type A, we introduce a function ifz M,N of F, with type

A 1 × • • • × A n → (NAT → B).
We also need function symbols for succ, pred and fix. Now, the translation M is defined by induction on M :

x = x; M N = ( M N ); λx.M = (abs M,x x 1 . . . x n ), if F V (M ) = x 1 ≤ . . . ≤ x n ; fix ((A→B)→A→B)→A→B = fix ((A→B)→A→B)→A→B ; n = s(s(. . . (s n times (0)) . . .)) succ = succ; pred = pred; ifz M N = (ifz M,N x 1 . . . x n ), if F V (M ) ∪ F V (N ) = x 1 ≤ . . . ≤ x n .
A converse translation [•] can be easily defined.

Lemma 1 If M is a PCF term of type A, then M is a well-typed term, of type A.

The rules of R PCF are the following:

((abs M,x x 1 . . . x n ) x) → M ;
(fix x) → (x (abs yz,z (fix x)));

(succ x) → (s x); (pred 0) → 0;

(pred (s x)) → x; ((ifz M,N x 1 . . . x n ) 0) → M ; ((ifz M,N x 1 . . . x n ) (s x)) → N . A term is said to be canonical if either it is a value or it is in the form ((f t 1 . . . t n s 1 . . . s m )),
where n is the arity of f, t 1 , . . . , t n are values and and s 1 , . . . , s m are themselves canonical. The following are technical intermediate results towards Theorem 7

Lemma 2 For every PCF term M , [ M ] = M .
Proof : By induction on the structure of M . Lemma 3 For every closed PCF term M , M is canonical. Moreover, if t is canonical and t → s, then s is canonical.

Proof : The fact M is always canonical can be proved by induction on the structure of M . The fact canonicity is preserved by reduction is a consequence of the adoption of a call-by-value notion of reduction.

Lemma 4 A canonical term t is a normal form iff [t] is a normal form.
Proof : Again, a simple induction of t.

Lemma 5 If t is canonical and t → s, then [t] → [s]. Lemma 6 If M -→ N , t is canonical and [t] = M , then t → s, where [s] = N .
Theorem 7 (Term Reducibility) Let M be a closed PCF term. The following two conditions are equivalent: 1. M -→ * N where N is in normal form; 2. M → * t where [t] = N and t is in normal form.

Proof : Suppose M -→ n N , where N is in normal form. Then, by applying Lemma 6, we obtain a term t such that M → n t and [t] = N . By Lemma 3, t is canonical and, by Lemma 4, it is in normal form. Now, suppose M → n t where [t] = N and t is in normal form. By applying n times Lemma 5, we obtain Even if the STTRS we have just defined is infinite and involves infinitely many function symbols, one can prove that any closed PCF program M of type NAT → NAT only needs a finite set of function symbols to be simulated, namely those function symbols corresponding to subterms of M .

[ M ] -→ n [t] = N . But [ M ] = M by
In the following it will also be instructive to consider a source language which is less expressive than PCF: Gödel's T, equipped with weak reduction. For that, remove in the source language the constant fix, and replace it with a constant rec with type scheme A → (NAT → A → A) → NAT → A and the following reduction rules:

rec x f 0 -→ x; rec x f n + 1 -→ (f n (rec x f n)).
We translate it to a STTRS R T similar to R PCF : one adds a function symbol rec A→(NAT →A→A)→NAT →A and the following new STTRS rules:

(((rec x) f ) 0) → x; (((rec x) f ) (s y)) → ((f y) (((rec x) f ) y)).
This encoding of system T then enjoys properties similar to the encoding of PCF.

Higher-Order Polynomial Interpretations

We want to demonstrate how first-order rewriting-based techniques for ICC can be adapted to the higher-order setting. Our goal is to devise criteria ensuring a complexity bound on programs of first-order types but using subprograms of higher-order types. A typical application will be to find out under which conditions a higher-order functional program such as e.g. map, iteration or foldl, fed with a (first-order) polynomial time program produces a polynomial time program.

As a first illustrative step we consider the approach based on polynomial interpretations from [START_REF] Bonfante | Algorithms with polynomial interpretation termination proof[END_REF], which offers the advantage of simplicity. We thus build a theory of higher-order polynomial interpretations for STTRSs. It can be seen as a particular concrete instantiation of the methodology proposed in [START_REF] Yamada | Confluence and termination of simply typed term rewriting systems[END_REF] for proving termination by interpretation.

Higher-order polynomials (HOPs) take the form of terms in a typed λ-calculus whose only base type is that of natural numbers. To each of those terms can be assigned a strictly monotonic function in a category FSPOS with products and functions. So, the whole process can be summarized by the following diagram:

STTRSs [•] / / HOPs • / / FSPOS

Higher-Order Polynomials

Let us consider types built over a single base type N:

A, B ::= N | A → A. A n → B stands for the type A → . . . → A n times → B.
Let C P be the following set of constants:

C P = {+ : N 2 → N, × : N 2 → N} ∪ {n : N | n ∈ N ⋆ }.
Observe that in C P we have constants of type N only for strictly positive integers. We consider the following grammar of Church-typed terms

M := x A | c A | (M A→B N A ) B | (λx A .M B ) A→B
where c A ∈ C P and in (λx A .M B ) we require that x occurs free in M . A higher-order polynomial (HOP) is a term of this grammar, which is in β-normal form. We use an infix notation for + and ×. HOP contexts (or simply contexts) are defined as HOPs but with the proviso that they must contain exactly one occurrence of a special constant • A (hole), for a type A. They are denoted as C, D . . . If C is a HOP context with hole • A , and M is a HOP of type A, then C{M } is the HOP obtained from C by replacing the occurrence of • A by M and reducing to the β normal form. We assume given the usual set-theoretic interpretation of types and terms, denoted as A and M : if M has type A and F V (M ) = {x A1 1 , . . . , x An n }, then M is a map from A 1 × . . . × A n to A . We denote by ≡ the equivalence relation which identifies terms which denote the same function, e.g. we have: λx.(2

× ((3 + x) + y)) ≡ λx.(6 + (2 × x + 2 × y)).
Noticeably, even if HOPs can be built using higher-order functions, the first order fragment only contains polynomials:

Lemma 8 If M is a HOP of type N n → N and such that F V (M ) = {y 1 : N, . . . , y k : N}, then the function M is a polynomial function.

Proof : We proceed by induction on M :

• if M = x or M = +, × or n: the result is trivial; • if M = λx A .M B
1 : then we have A = N and the type B is of the form N, . . . , N → N , so by i.h. on M 1 the property is true for M 1 , hence for M ; • otherwise M is an application. As M is in β-normal form, there exists n ≥ 0 such that:

• M is of the form M = (N M 1 . . . M n ),
• and N = x A , +, × or n. Now, if N = + or ×, then for any 1 ≤ i ≤ n we have that M i is of type N , so by i.h. on M i it satisfies the property, therefore M represents a polynomial function. If N = x A , then as x A is free in M , by assumption we know that A = N , thus n = 0 and the property is valid.

Similarly if N = n. This concludes the proof.

A HOP substitution θ is a map from variables to HOPs, with finite domain. We will simply speak of substitution if there is no ambiguity. For any HOP M and HOP substitution θ, M θ is the HOP defined in the expected way.

Semantic Interpretation.

Now, we consider a subcategory FSPOS of the category SPOS of strict partial orders as objects and strictly monotonic total functions as morphisms. Objects of FSPOS are the following:

• N is the domain of strictly positive integers, equiped with the natural strict order ≺ N , • 1 is the trivial order with one point; • if σ, τ are objects, then σ × τ is obtained by the product ordering, • σ → τ is the set of strictly monotonic total functions from σ to τ , equipped with the following strict order: f ≺ σ→τ g if for any a of σ we have f (a) ≺ τ g(a).

We denote by τ the reflexive closure of ≺ τ . FSPOS is a subcategory of SET with all the necessary structure to interpret types. A ≺ denotes the semantics of A as an object of FSPOS. We choose to set N ≺ = N . Notice that any element of e ∈ A ≺ can be easily mapped onto an element e ↓ of A . What about terms? Actually, FSPOS can again be shown to be sufficiently rich:

Proposition 9 Let M be a HOP of type A with free variables x A1 1 , . . . , x An n . Then for every e ∈ A 1 × . . . × A n ≺ , there is exactly one f ∈ A ≺ such that f ↓= M (e ↓). Moreover, this correspondence is strictly monotone and thus defines an element of A 1 × . . . × A n → A ≺ which we denote as M ≺ .

Proof : We proceed by induction on the construction of M :

• M = x A : trivial; • M = c A ∈ C P :
this holds because as we have interpreted N as N ⋆ the terms + and × denote strictly monotonic functions (note that it would not have been the case for × if we had interpreted N as N); • M = λx.M ′ : by definition we know that x is free in M ′ . Let us denote by x A1 1 , . . . , x An n the free variables of M ′ and w.l.o.g. assume x = x n . By i.h. we have

M ′ ≺ ∈ A 1 × . . . × A n → A ≺ .
For (e 1 , . . . , e n-1 ) in A 1 ×. . .×A n-1 ≺ we then consider the map

f from A n ≺ to A ≺ defined by f (e n ) = M ′ ≺ (e 1 , . . . , e n ). As M ′ ≺ ∈ A 1 ×. . .×A n → A ≺ we have that f ∈ A n → A ≺
and satisfies the property. Suppose now that f ′ ∈ A n → A ≺ is defined in a similar way from (e ′ 1 , . . . , e ′ n-1 ) ∈ A 1 × . . . × A n-1 ≺ such that (e 1 , . . . , e n-1 ) ≺ (e ′ 1 , . . . , e ′ n-1 ). Then we have that if e n ∈ A n ≺ , then (e 1 , . . . , e n-1 , e n ) ≺ (e ′ 1 , . . . , e ′ n-1 , e n ), thus M ′ ≺ (e 1 , . . . , e n-1 , e n ) ≺ M ′ ≺ (e ′ 1 , . . . , e ′ n-1 , e n ). This shows that f ≺ f ′ . Therefore we have obtained a strictly monotonic correspondence from A 1 × . . . × A n-1 ≺ to A n → A ≺ , which completes the claim.

• M = M A→B 1 M A 2 :
this is the crucial case. By i.h. M 1 ≺ and M 2 ≺ have been defined. Denote by x A1 1 , . . . , x An n the free variables of M . Take e = (e 1 , . . . , e n ) ∈ A 1 × . . . × A n ≺ . By abuse of notation we will simply write M 1 ≺ (e) instead of M 1 ≺ (e i1 , . . . , e i k ) where x i1 , . . . , x i k are the free variables of M 1 . Similarly for M 2 ≺ (e). Now we define f as f = M 1 ≺ (e)( M 2 ≺ (e)). We have that f ∈ B ≺ and f ↓= M (e ↓). Now let us show that this correspondence is strictly monotone. If n = 0 it is trivial, so let us assume n ≥ 1. Take e, e ′ two elements of

A 1 × . . . × A n ≺ with e ≺ e ′ . Let f = M 1 ≺ (e)( M 2 ≺ (e)) and f ′ = M 1 ≺ (e ′ )( M 2 ≺ (e ′ )).
Let us distinguish two subcases:

• if there exists i in {1, . . . , n} such that e i ≺ e ′ i and x i ∈ F V (M 1 ): then by i.h. on M 1 we have M 1 ≺ (e) ≺ A→B M 1 ≺ (e ′ ); moreover by h.i. we have: M 2 ≺ (e) A M 2 ≺ (e ′ ) (note the non-strict ordering). From these two inequalities, by definition of ≺ A→B we can deduce:

M 1 ≺ (e)( M 2 ≺ (e)) ≺ B M 1 ≺ (e ′ )( M 2 ≺ (e ′ )).
• Otherwise: we know that there exists i in {1, . . . , n} such that e i ≺ e ′ i , and x i is free in M so it must be free in M 2 . So by i.h. on M 2 we have M 2 ≺ (e) ≺ A M 2 ≺ (e ′ ); besides we know that M 1 ≺ (e) = M 1 ≺ (e ′ ). We know that M 1 ≺ (e) belongs to A → B ≺ so it is strictly monotonic, so we deduce that:

M 1 ≺ (e)( M 2 ≺ (e)) ≺ B M 1 ≺ (e ′ )( M 2 ≺ (e ′ )).
So in both subcases we have concluded that f ≺ f ′ , which completes the proof of the claim. This concludes the proof.

Lemma 10 Let M be a HOP and θ a HOP substitution with F V (M ) = {x A1 1 , . . . , x An n } and F V (M θ) = {y B1 1 , . . . , y Bm m }. Then, for every i ∈ {1, . . . , m} the function

f i = θ(x i ) ≺ is a strictly monotonic map. Moreover, we have M θ ≺ = M ≺ • (f 1 , . . . , f n ).
Proof : For i ∈ {1, . . . , m} we have f i = θ(x i ) ≺ . We know that θ(x i ) is a HOP, and

F V (θ(x i )) ⊆ F V (M θ). Let = {y B k 1 k1 , . . . , y B k i
ki } be the free variables of θ(x i ). Then f i belongs to B k1 ≺ × . . . × B ki ≺ → A i ≺ . We can then prove the second statement by induction on M . As an illustration let us just examine here the base cases:

• The case where M = c A is trivial because n = 0 and M θ = M . • In the case where M is a variable we have n = 1 and

M = x A1 1 . Then M θ ≺ = θ(x 1 ) ≺ = f 1 = id A1 • f 1 .
This concludes the proof.

Applying the same substitution to two HOPs having the same type preserve the properties of the underlying interpretation:

Lemma 11 If M A , N A are HOPs such that F V (M ) ⊆ F V (N ), θ is a HOP substitution and if M ≺ ≺ N ≺ , then M θ ≺ ≺ N θ ≺ .

Assignments and Polynomial Interpretations

We consider X , C and F as in Sect. 2. To each variable x A we associate a variable x A where A is obtained from A by replacing each occurrence of base type by the base type N and by curryfication. We will sometimes write x (resp. A) instead of x (resp. A) when it is clear from the context.

An assignement

[ • ] is a map from C ∪ F to HOPs such that if f ∈ C ∪ F, [f ] is a closed HOP, of type A 1 , . . . , A n → A. Now, for t ∈ T we define [t] by induction on t: • if t ∈ X , then [t] is f ; • if t ∈ C ∪ F, [t] is already defined; • otherwise, if t = (t 0 t 1 . . . t n ) then [t] ≡ (. . . ([t 0 ][t 1 ]) . . . [t n ]).
Observe that in practice, computing [t] will in general require to do some β-reduction steps.

Lemma 12 Let t ∈ T of type A and F V (t) = {y 1 : A 1 , . . . , y n : A n }, then: [t] is a HOP, of type A, and F V ([t]) = {y 1 : A 1 , . . . , y n : A n }.

A Complexity Criterion

Proving a STTRS to have an interpretation is not enough to guarantee its time complexity to be polynomial. To ensure that, we need to impose some constraints on the way constructors are interpreted.

We say that the assignment

[ • ] is additive if any constructor c of type D 1 × • • • × D n → D 0
, where n ≥ 0, is interpreted by a HOP M c whose semantic interpretation M c ≺ is a polynomial function of the form:

P (y 1 , . . . , y n ) = n i=1 y i + γ c , with γ c ≥ 1.
Additivity ensures that the interpretation of first-order values is proportional to their size: Lemma 18 Let [ • ] be an additive assignment. Then there exists γ ≥ 1 such that for any value v of type D, where D is a data type, we have v ≺ ≤ γ • |v|.

The base type W n denotes the data-type of n-ary words, whose constructors are empty and c 1 , . . . , c n . A function f : ({0, 1} * ) m → {0, 1} is said to be representable by a STTRS R if there is a function symbol f of type W m 2 → W 2 in R which computes f in the obvious way. We are now ready to prove the main result about polyomial interpretations, namely that they enforce reduction lengths to be bounded in an appropriate way:

Theorem 19 Let R be a STTRS with an additive polynomial interpretation [ • ]. Consider g a function symbol of type W 2 × • • • × W 2 → W 2 .
We have: there exists a polynomial P such that, for any w 1 , . . . , w n ∈ {0, 1} ⋆ , any reduction of (g w 1 . . . w n ) has length bounded by P (|w 1 |, . . . , |w n |). This holds more generally for g of type D 1 , . . . , D n → D.

Proof : By Prop. 17 we know that any reduction sequence has length bounded by: (g w 1 . . . w n ) ≺ = g ≺ ( w 1 ≺ , . . . , w n ≺ ). By Lemma 8 there exists a polynomial function Q such that g ≺ computes Q. Moreover by Lemma 18 there exists γ ≥ 1 such that: w i ≺ ≤ γ|w i |. So by defining P as the polynomial function such that P (y 1 , . . . , y n ) = Q(γy 1 , . . . , γy n ), we have that the length of the reduction sequence is bounded by P (|w 1 |, . . . , |w n |).

Corollary 20

The functions on binary words representable by STTRSs admitting an additive polynomial interpretation are exactly the polytime functions.

Proof : We have two inclusions to prove: from left to right (complexity soundness), and from right to left (completeness):

• Complexity soundness. Assume F is represented by a program g with type W 2 ו • •×W 2 →
W 2 admitting an additive polynomial interpretation. Then by Theorem 19 we know that for any w 1 , . . . , w n ∈ {0, 1} ⋆ , any reduction of (g w 1 . . . w n ) has a polynomial number of steps. By a result in [START_REF] Lago | Derivational complexity is an invariant cost model[END_REF], derivational complexity is an invariant cost model for TRSs, via graph rewriting. This result can be easily generalized to STTRSs. • Completeness. Let F be a polytime function on binary words. It has been shown in [START_REF] Bonfante | Algorithms with polynomial interpretation termination proof[END_REF] (Theorem 4, Sect. 4.2) that there exists a first-order rewrite system with an additive polynomial interpretation which computes F . Actually the rewrite systems considered in this paper are not assumed to be typed, but it can be checked that the rewrite systems used to simulate polynomial time Turing machines are typable and can be seen as simply typed term rewrite systems in our sense. Moreover when restricting to first-order typed rewrite systems, our notions of polynomial interpretation and of additive polynomial interpretation coincide with the notions they consider. Therefore F can be represented by a simply typed term rewriting system program with an additive polynomial interpretation. This concludes the proof.

Examples

Consider the STTRS defined by the following rules:

(1) (map f nil) → nil (2) (map f (cons x xs)) → (cons (f x) (map f xs))
with the following types:

f : D 1 → D 2 , map : (D 1 → D 2 ) × L(D 1 ) → L(D 2 ), nil : L(D i ), cons : D i × L(D i ) → L(D i ) for i = 1, 2.
Here D i and L(D i ) for i = 1, 2 are base types. For simplicity we use just one cons and one nil notation for both types D 1 , D 2 .

The interpretation below was given in [START_REF] Yamada | Confluence and termination of simply typed term rewriting systems[END_REF] for proving termination, but here we show that it also gives a polynomial time bound. To simplify the reading of HOPs we use infix notations for +, omit some brackets (because anyway we have associativity and commutativity for the denotations) and the symbol ×, write F (n) for the application of a function and k instead of k. Now, we choose the following assignment of HOPs:

[nil] = 2 : N [cons] = λn.λm.(n + m + 1) : N → N → N [map] = λF.λn.nF (n) : (N → N) → N → N
Instead of the last line we will often write

[map](F, n) = nF (n).
We use as notations

[f ] = F , [x] = n, [xs] = m.
We then get the following interpretations of terms:

[map f nil] = 2F (2) [map f cons(x, xs)]] = (n + m + 1)F (n + m + 1) [cons(f (x), (map f xs))] = 1 + F (n) + mF (m)
One can check that the condition r ≺ ≺ l ≺ holds for (1) and [START_REF] Yamada | Confluence and termination of simply typed term rewriting systems[END_REF]. We thus have an additive polynomial interpretation for map, therefore Corollary 20 applies and we can conclude that for any f also satisfying the criterion, (map f) computes a polynomial time function. Now, one might want to apply the same method to an iterator iter, of type (D → D) × D → NAT → D, which when fed with arguments f , d, n iterates f for n times starting from d. However there is no additive polynomial interpretation for this program . . . which is normal because iter can produce an exponential-size function when it is fed with a polynomial time function, e.g. a function double : NAT → NAT .

One way to overcome this issue could be to show that iter does admit a valid polynomial interpretation, provided its domain is restricted to some particular functions, admitting a small polynomial interpretation, of the form λn.(n + c), for some constant c.

This could be enforced by considering a refined type systems for HOPs. But the trouble is that there are very few programs which admit a polynomial interpretation of this form! Intuitively the problem is that polynomial interpretations need to bound simultaneously the execution time and the size of the intermediate values obtained. In the sequel we will see how to overcome this issue. The first step will take the form of a termination criterion defined by a linear type system for STTRSs together with a path-like order, to be described in Section 5.1 below. The second step consists in shifting from a semantic world of strictly monotonic functions to one of monotonic functions. This corresponds to a picture like the following, and is the subject of sections 5.2 and 5.3.

f A ∈ N F Γ | ∆ ⊢ f : A c A ∈ C Γ | ∆ ⊢ c : A Γ | x : A, ∆ ⊢ x : A x : D, Γ | ∆ ⊢ x : D f A1,...,An→B ∈ RF, with arity n Γ | ∅ ⊢ s i : A i Γ | ∆ ⊢ ((f s 1 . . . s n )) : B Γ | ∆ ⊢ t : A 1 × . . . × A n → B Γ | ∆ i ⊢ s i : A i Γ | ∆, ∆ 1 , . . . , ∆ n ⊢ (t s 1 . . . s n ) : B
STTRSs [•] / / HOMPs • / / FPOS

The Termination Criterion

The termination criterion has two ingredients: a typing ingredient and a syntactic ingredient, expressed using the order ⊏. Is it restrictive for expressivity? Let us comment first on the syntactic ingredient:

• First consider the embedding of simply typed λ-calculus given by the restriction of the embedding of PCF of Section 3. The function symbols used are abs M,x for all typed term M and variable x. We define the order ⊏ by: abs M,x ⊏ abs N,y if λy.N is a subterm of M.

We write f ⊏ t if f ⊏ g for any function g in t. The STTRS encoding of M then satisfies the following condition, for any rule ((f p 1 . . . p k )) → s:

s ⊏ f (1)
As the order ⊏ defined is well-founded, this implies the termination of this STTRS program. • Now consider System T. We have seen that System T with weak reduction can also be embedded into a STTRS. Forget about functions pred, succ, ifz for simplification, and consider the new function rec. We extend ⊏ by setting: f ⊏ rec for any function f distinct from rec. Then in the STTRS encoding of a system T term M , each rule ((f p 1 . . . p k )) → s satisfies either condition 1 or the following condition 2: there are a term r and sequences of patterns q 1 , . . . , q k such that for any i, j, q i,j is subterm of p i,j , there exist i 0 , j 0 s.t. q i0,j0 = p i0,j0 and s = r{x/((f q 1 . . . q k ))}, and r ⊏ f

So the syntactic ingredient is fairly expressive, since it will allow to validate system T programs.

As to the full termination criterion, including the typing ingredient, we believe it is general enough to embed Hofmann's system SLR [START_REF] Hofmann | A mixed modal/linear lambda calculus with applications to Bellantoni-Cook safe recursion[END_REF], which is a restriction of system T based on safe recursion and using linear types, and which characterizes the class of polytime functions.

Formally, the class F needs to be split into two disjoint classes RF and N F. The intended meaning is that functions in N F will not be defined in a recursive way, while functions in RF can. We further assume given a strict order ⊏ on F which is well-founded. The rules of a linear type system for STTRS terms are in Figure 1. A program satisfies the termination criterion if every rule ((f p 1 . . . p k )) → s satisfies:

T S ((f t 1 ...tn)) (X) =1 +       tj ∈ F O j ≤ arity(f) T St j (X)       +       tj ∈ HO j ≤ arity(f) n • X • T St j (X)       +   j≥arity(f)+1 T St j (X)   +   s∈R(f) n • X • T Ss(X)   , if f ∈ RF T S ((f t 1 ...tn)) (X) =1 +   1≤j≤n T St j (X)   +   s∈R(f) T Ss(X)   , if f ∈ N F T S ((c t 1 ...tn)) (X) =1 +   1≤j≤n T St j (X)   , T S ((x t 1 ...tn)) (X) =1 +   1≤j≤n T St j (X)   ; T Sv(X) =1, if v is a first order value, Figure 2: The Definition of T S (•) (X)
1. either f ∈ RF, there are a term r and sequences of patterns q 1 , . . . , q k such that for any i, j, q i,j is subterm of p i,j , there exist i 0 , j 0 s.t. q i0,j0 = p i0,j0 and Γ | x : B, ∆ ⊢ r : B, s = r{x/((f q 1 . . . q k ))}, and r ⊏ f; 2. or f ∈ N F, s is typable, and s ⊏ f. Observe that because of the typability condition in 1., this termination criterion implies that there is at most one recursive call in the right-hand.side s of a rule.

By a standard reducibility argument, one get the following:

Theorem 21 If a program satisfies the termination criterion, then any of its terms is strongly normalizing.

In the rest of this section, we show that all that matters for the time complexity of STTRSs satisfying the termination criterion is the size of first-order values that can possibly appear along the reduction of terms. In other words, we are going to prove that if the latter is bounded, then the complexity of the starting term is known, modulo a fixed polynomial. Showing this lemma, which will be crucial in the following, requires introducing many auxiliary definitions and results. Given a term t and a natural number n ∈ N, n is said to be a bound of first order values for t if for every reduct s of t, if s contains a first-order value v, then |v| ≤ n.

Lemma 22

If n ∈ N is a bound of first-order values for t and t → * s, then n is also a bound of first-order values for s.

Suppose a function symbol f takes n base arguments. Then f is said to have base values bounded by a function q :

N n → N if (f t 1 . . . t n ) has q(|t 1 |, . . . , |t n |)
as a bound of its first-order values whenever t 1 , . . . , t n are first-order values. Given a term t, its definitional depth is the maximum, over any function symbol f appearing in t, of the length of the longest descending ⊏-chain starting from f. The definitional depth of t is denoted as ∂(t). Given a function symbol f, R(f) denotes the set of terms appearing in the right-hand side of rules for f, not taking into account recursive calls. More formally, r belongs to R(f) if there is a rule ((f p 1 . . . p k )) → s such that s = r{x/((f q 1 . . . q k ))} (where x might not occur in r) and r ⊏ f. For every term t, define its space-time weight as a polynomial T S t (X) on the indeterminate X, by induction on (∂(t), |t|), following the lexicographic order, as in Figure 2. We denote here by FO (resp. HO) the arguments t j of f of base type (resp. functional type). The collapsed size ||t|| of a term t is its size, where however all first-order values count for 1. It is defined formally by:

||v|| = 1, if v is a first-order value, ||(t 0 t 1 . . . t n )|| = i=0 ||t i ||, ||α|| = 1, if α = x, c or f.
For instance ||(s (s x))|| = 3 and ||(s (s 0))|| = 1. We define a rewrite relation ⇒ which is like →, except that whenever a recursive function symbol is unfolded, it is unfolded completely in just one rewrite step.

We are now ready to explain why the main result of this section holds. First of all, T S t (X) is an upper bound on the collapsed size of t, a result which can be proved by induction: Lemma 23 For every n and for every t, T S t (n) ≥ ||t||.

Proof : A simple induction on t.

Moreover, T S t (X) decreases along any ⇒ step if X is big enough:

Lemma 24 If n is a bound of first-order values for t, and t ⇒ s, then T S t (n) > T S s (n).

Proof : Suppose that t ⇒ s and let ((f r 1 . . . r m )) be the redex fired in t to produce s. Then we can say that there is p such that

T S t (n) = T S ((f r1...rm)) (n) + p; T S s (n) = T S q (n) + p.
Let us now distinguish two cases:

• If f ∈ RF, then q is obtained by at most m • n rewrite steps from ((f r 1 . . . r m )) and does not contain any instance of f anymore. By an easy combinatorial argument, one realizes that, indeed,

T S q (n) ≤      rj ∈ HO j ≤ arity(f) m • n • T S rj (X)      +   s∈R(f) m • n • T S s (X)  
which, by definition, is strictly smaller than T S ((f r1...rm)) (n).

• if f ∈ N F, then q is such that ((f r 1 . . . r m )) ⇒ q. As a consequence T S ((f r1...rm)) (n) = 1 +   1≤j≤m T S rj (n)   +   w∈R(f)
T S w (n)   while q, containing possibly at most one instance of each higher-order value in r 1 , . . . , r m , is such that:

T S q (n) ≤   1≤j≤m T S rj (n)   +   w∈R(f) T S w (n)   .
This concludes the proof.

It is now easy to reach our goal:

Proposition 25 Suppose that R satisfies the termination criterion. Moreover, suppose that f has base values bounded by a function q : N n → N. Proof : Let us first prove the following statement: if (f t 1 . . . t n ) ⇒ m s, then there is q polynomial such that m, ||s|| ≤ p(q(|t 1 |, . . . , |t n |)) Actually, the polynomial we are looking for is precisely

q(X) =   s∈R(f) n • X • T S s (X)   + n.
Indeed, observe that by definition

T S (f t1...tn) (X) = q(X)
and that, by lemmas 24 and 23, this is both a quantity that decreases at any reduction step and which bounds from above the collapsed size of any reduct of (f t 1 . . . t n ). Now, observe that:

• If m is a bound of first order values for t, then |t| ≤ m • ||t||;

• If m is a bound of first order values for t, then the number of "real" →-reduction steps corresponding to each ⇒-reduction step from t is bounded by m • k, where k is the maximum arity of function symbols in the underlying STTRS; • Call-by-value is a strongly confluent rewrite relation, and as a consequence the possible number of reduction steps from a term does not depend on the specific reduction order. Similarly for the size of reducts. This concludes the proof.

To convince yourself that linearity is needed to get a result like Proposition 25, consider the following STTRS, whose terms cannot be typed in our linear type systems:

((comp x y) z) → (x(yz) (autocomp x) → (comp x x) (id x) → x (expid 0) → id (expid (s x)) → (autocomp (expid x))
Both the term id and (expid t) (for every value t of type NAT ) can be given type NAT → NAT . Actually, they all are the same function, extensionally. But try to see what happens if expid is applied to natural numbers of growing sizes: there is an exponential blowup going on which does not find any counterpart in any first-order value.

Higher-Order Max-Polynomials

We want to refine the type system for higher-order polynomials, in order to be able to use types to restrict the domain of functionals. The grammar of types is now the following one: We now consider the following new set of constructors:

D P = {+ : N ⊸ N ⊸ N, max : N ⊸ N ⊸ N, × : N → N → N} ∪ {n : N | n ∈ N ⋆ }, Then M = [(f x 1 . . . x n )]M 1 .
. . M k is a HOMP of type N with free variables x i of type N , for i ∈ 1, . . . , n. By Lemma 27 we deduce from that that there exists a polynomial q such that:

y i ≤ M ≤ (y 1 , .
. . , y n ) ≤ q(y 1 , . . . , y n ), for i = 1, . . . , n.

Moreover we have:

([t] M 1 . . . M k ) ≤ = ([t ′ ] M 1 . . . M k ) ≤ ( t 1 ≤ , . . . , t n ≤ ) = M ≤ ( t 1 ≤ , . . . , t n ≤ ) ≤ q( t 1 ≤ , . . . , t n ≤ ) ≤ q(α|t 1 |, . . . , α|t n |)
for some α, because [ • ] is an additive quasi-interpretation, thanks to Lemma 30. So finally there is a polynomial p such that:

([t] M 1 . . . M k ) ≤ ≤ p(
. . . M k ≤ = [s ′ ] M 1 . . . M k ≤ ( r ≤ ) ≥ r ≤ .
So finally by combining the two inequalities we obtained we get

r ≤ ≤ [s] M 1 . . . M k ≤ ≤ p(|t 1 |, . . . , |t n |).
And here is the main result of this Section:

Theorem 33 If a program P has an additive quasi-interpretation, P satisfies the termination criterion and f has arity n with base arguments, then there is a polynomial p :

N n → N such that if (f t 1 . . . t n ) → m s, then m, |s| ≤ p(|t 1 |, . . . , |t n |). So if f has a type D 1 , . . . , D n → D then it is Ptime.
Proof : A consequence of Proposition 32 and of Proposition 25. Notice how Theorem 33 is proved by first observing that terms of STTRSs having a quasiinterpretation are bounded by natural numbers which are not too big with respect to the input, thus relying on the termination criterion to translate these bounds to complexity bounds.

Examples

Consider the program foldl given by:

(1) (foldl f b nil) → b (2) (foldl f b (cons x xs)) → (f x (foldl f b xs)) with types: foldl : (D × E → E) × E × L(D) → E f : D × E → E nil : L(E) cons : E × L(E) → L(E)
Now, we choose as assignment: where for the two last steps we used φ(1, 1) ≥ 1 and φ(1, 1) ≥ c (by ( * )). So r ≤ ≤ l ≤ also holds for (2) and we have an additive quasi-interpretation.

[nil] = 1 : N [cons](n, m) = n + m + 1 : N → N → N [foldl](φ, p, n) = p + nφ(1, 1) : (N ⊸ N ⊸ N) → N → N → N
As to the termination criterion, it is satisfied because in (2) xs is a strict sub-pattern of cons(x, xs) and the term f (x, y) can be typed in the linear type system as required.

Summing up, we can apply Theorem 33 and conclude that: if the termination criterion is satisfied by all functions, if t D×E→E , b E are terms and [t] is a HOMP with type N ⊸ N ⊸ N, then (foldl t b) is a polynomial time program of type L(D) → E.

Discussion and Relation with Other ICC Systems

The authors believe that the interest of the present work does not lie much in bringing yet another ready-to-use ICC system but rather in offering a new framework in which to design ICC systems and prove their complexity properties. Indeed, considered as an ICC system our setting presents two limitations: 1. given a program one needs to find an assignment and to check that it is a valid quasiinterpretation, which in general will be difficult to automatize; 2. the termination criterion currently does not allow to reuse higher-order arguments in full generality. To overcome 2. we think it will be possible to design more liberal termination criteria, and to overcome 1. one possibility consists in defining type systems such that if a program is well-typed, then it admits a quasi-interpretation, and for which one could devise type-inference algorithms.

Related and Further Work

Let us first compare our approach to other frameworks for proving complexity soundness results.

At first-order, we have already emphasized the fact that our setting is an extension of the quasi-interpretation approach of [START_REF] Bonfante | Quasi-interpretations a way to control resources[END_REF] (see also [START_REF] Amadio | Synthesis of max-plus quasi-interpretations[END_REF] for the relation with non-size-increasing, at firstorder). We could examine whether the various flavours they consider on the termination criteria and the interpretations (e.g. sup-interpretations) could suggest ideas in our higher-order setting.

At higher-order, various approaches based on realizability have been used [START_REF] Hofmann | A mixed modal/linear lambda calculus with applications to Bellantoni-Cook safe recursion[END_REF][START_REF] Lago | Realizability models and implicit complexity[END_REF][START_REF] Brunel | Church => Scott = Ptime: an application of resource sensitive realizability[END_REF]. While these approaches were developed for logics or System T-like languages, our setting is adapted to a language with recursion and pattern-matching. We think it might also be easier to use in practice.

Let us now discuss the relations with other ICC systems. Several variants of system T based on restriction of recursion and linearity conditions [START_REF] Hofmann | A mixed modal/linear lambda calculus with applications to Bellantoni-Cook safe recursion[END_REF][START_REF] Bellantoni | Higher type recursion, ramification and polynomial time[END_REF][START_REF] Lago | The geometry of linear higher-order recursion[END_REF] have been proposed which characterize polynomial time. Another system [START_REF] Hofmann | Linear types and non-size-increasing polynomial time computation[END_REF] with a linear type system for non-size-increasing computation offers more intensional expressivity. We believe we should be able to embed these systems in our approach, but leave this for future work. With respect to the first group of works, we offer the same benefit as [START_REF] Hofmann | Linear types and non-size-increasing polynomial time computation[END_REF], that is to say the nesting of recursions thanks to the distinction of non-size-increasing functions. With respect to [START_REF] Hofmann | Linear types and non-size-increasing polynomial time computation[END_REF], the advantages we bring are the use of recursively defined functions generalizing the System T recursor and a slightly more general handling of higher-order arguments, allowing for instance to validate the foldl program. Some other works are based on type systems built out of variants of linear logic [START_REF] Baillot | Light types for polynomial time computation in lambda calculus[END_REF][START_REF] Gaboardi | A soft type assignment system for lambdacalculus[END_REF][START_REF] Baillot | A polytime functional language from light linear logic[END_REF]. They are less expressive for first-order functions but offer more liberal disciplines for handling higher-order arguments. In future work we will examine if they could suggest a more flexible termination condition for our setting, maybe itself based on quasi-interpretations, following [START_REF] Lago | Linear dependent types and relative completeness[END_REF].

  Lemma 2 and N is a normal form by Lemma 4, since M and t are canonical by Lemma 3.

Figure 1 :

 1 Figure 1: A Linear Type System for STTRS terms.

S

  ::= N | S ⊸ S A ::= S | A → A Types of the first (resp. second) grammar are called linear types (resp. types) and denoted as R, S . . . (resp. A, B, C . . . ). The linear function type ⊸ is a subtype of →, i.e., one can define a relation ⊑ between types by stipulating that S ⊸ R ⊑ S → R and by closing the rule above in the usual way, namely by imposing that A → B ⊑ C → D whenever C ⊑ A and B ⊑ D.

  Observe the ⊸ in the type of the first argument of [foldl] which is the way to restrict the domain of arguments. We denote[b] = p, [x] = n, [xs] = m, [f ] = φ.We then obtain the following interpretations of terms:[foldl f b nil] = p + 1φ(1, 1) [b] = p [foldl f b cons(x, xs)] = p + (n + m + 1)φ(1, 1) [f (x, (foldl f b xs)))] = φ(n, (p + mφ(1, 1)))The condition r ≤ ≤ l ≤ holds for (1), because we have:p ≤ p + φ(1, 1)holds for any p. As to rule (2) consider φ ∈ (N × N ⊸ N ), n, p and m in N . So we know that there exists c ≥ 0 such that:c ≤ φ(x 1 , x 2 ) ≤ x 1 + x 2 + c, for any x 1 , x 2 ∈ N . ( * )Then we have: φ(n, (p + mφ(1, 1))) ≤ n + p + mφ(1, 1) + c by ( * ), ≤ nφ(1, 1) + p + mφ(1, 1) + c, ≤ p + (n + m + 1)φ(1, 1).

  Then, there is a polynomial p : N → N such that if t 1 , . . . , t n are first-order values and (f t 1 . . . t n ) → m s, then m, |s| ≤ p(q(|t 1 |, . . . , |t n |)).

  |t 1 |, . . . , |t n |). Now, as t → * s, by Lemma 31 we have t ≤≥ s ≤ . Therefore [t] M 1 . . . M k ≤ ≥ [s] M 1 . . . M k ≤ . So we get: [s] M 1 . . . M k ≤ ≤ p(|t 1 |, . . . , |t n |).Besides, by assumption we know that s can be written as s = s ′ {y/r}. By Lemma 27 we have[s ′ ] M 1 . . . M k ≤ (y) ≥ y, because ([s ′ ] M 1 . . . M k ) hastype N and only one free variable y which is also of type N . Therefore we get [s] M 1

Beyond Interpretations: Quasi-InterpretationsThe previous section has illustrated our approach. However we have seen that the intensional expressivity of higher-order polynomial interpretations is too limited. In the first-order setting this problem has been overcome by decomposing into two distinct conditions the rôle played by polynomial interpretations[START_REF] Marion | Efficient First Order Functional Program Interpreter with Time Bound Certifications[END_REF][START_REF] Bonfante | Quasi-interpretations a way to control resources[END_REF]: (i) a termination condition, (ii) a condition enforcing a bound on the size of values occurring during the computation. In[START_REF] Bonfante | Quasi-interpretations a way to control resources[END_REF], this has been implemented by using: for (i) some specific recursive path orderings, and for (ii) a notion of quasi-interpretation. We will examine how this methodology can be extended to the higher-order setting.

Conclusions

We have advocated the usefulness of Simply Typed Term Rewriting Systems to smoothly extend notions from first-order rewrite systems to the higher-order setting. Our main contribution is a new framework for studying ICC systems for higher-order languages. While up to now quite distinct techniques had been successful for providing expressive criteria for Ptime complexity at first-order and at higher-order respectively, our approach allows to take advantage simultaneously of these techniques: interpretation methods on the one hand, and semantic domains and type systems on the other. We have illustrated the strength of this framework by designing an ICC system for Ptime based on a termination criterion and on quasi-interpretations, which allows to give some sufficient conditions for programs built with higher-order functionals (like foldl) to work in bounded time. We think this setting should allow in future work to devise new systems for ensuring complexity bounds for higher-order languages, which would be more expressive algorithmically.

Proof : This follows from the definition of [t], by induction on t.

We extend the notion of assignments to contexts by setting: Let us now consider the semantic interpretation. If t ∈ T of type A and F V (t) = {y 1 : A 1 , . . . , y n : A n }, we will simply denote by t ≺ the element [t] ≺ of A 1 × . . . × A n → A ≺ .

Lemma 15 Let M , N be HOPs such that M ≺ ≺ N ≺ and C be a HOP context such that C{M } and C{N } are well-defined. Then we have that C{M } ≺ ≺ C{N } ≺ . The same statement holds if we replace HOPs M , N by terms t, s and the HOP context by a context. Now, we say that an assignment [ • ] is a higher polynomial interpretation (HOPI) or simply a polynomial interpretation for R iff for any l → r ∈ R, we have that r ≺ ≺ l ≺ . Note that in the particular case where the program only contains first-order functions, this notion of higher-order polynomial interpretation coincides with the classical one for first-order rewrite systems. In the following we assume that [ • ] is a polynomial interpretation for the program P. A key property is the following, which tells you that the intepretation of terms strictly decreases along any reduction step:

Proof : Suppose s → t, then by definition there exists a rule l → r of R, a context C and a substitution σ such that s = C{lσ} and t = C{rσ}. As [ • ] is a polynomial interpretation we have r ≺ ≺ l ≺ . We then get: Then by Lemma 15 (second statement) we get:

which ends the proof.

As a consequence, the interpretation of terms (of base type) is itself a bound on the length of reduction sequences: Proposition 17 Let t be a closed term of base type D. Then [t] has type N and any reduction sequence of t has length bounded by t ≺ .

Proof : It is sufficient to observe that by Lemma 16 any reduction step on t makes t ≺ decrease for ≺, and that as t is closed and of type N the order ≺ here is ≺ N , which is the ordinary (strict) order on integers. and we consider the following grammar of Church-typed terms

where c A ∈ D P . We also require that:

One can check that this class of Church-typed terms is preserved by β-reduction. A higherorder max-polynomial (HOMP) is a term defined above and which is in β-normal form. The interpretations M , and the equivalence relation ≡ are defined in a similar way as before. We define the following objects and constructions on objects:

• N is the domain of strictly positive integers, equipped with the natural order, denoted here ≤ N , • 1 is the trivial order with one point; • if σ, τ are objects, then σ × τ is obtained by the product ordering, • σ ⇒ τ is the set of monotonic total functions from σ to τ , equipped with the extensional order: f ≤ σ⇒τ g if for any a of σ we have f (a) ≤ τ g(a). This way, one obtains a subcategory FPOS of the category POS with partial orders as objects and monotonic total functions as morphisms.

Given an object σ of the category FPOS and an element e ∈ σ, the size |e| of e is defined as follows: We denote by A ≤ the semantics of A as an object of FPOS, where N is mapped to N , → is mapped to ⇒ and ⊸ to ⊸. As before, any element of e ∈ A ≤ can be mapped onto an element e ↓ of A . We define M ≤ for any HOMP M in the natural way.

Proposition 26 Let M be a closed HOMP of type A. Then M ≤ ∈ A ≤ . Moreover, if A is a linear type S, then the size of M ≤ is defined.

Lemma 27 If M is a HOMP of type N m → N (with m arguments) and such that F V (M ) = {y 1 : N, . . . , y k : N}, then the function M is bounded by a polynomial and satisfies: ∀i ∈ {1, k + m}, ( M (x 1 , . . . , x k ))(x k+1 , . . . , x k+m ) ≥ x i .

Proof : We prove the statement by induction on M : • If M = x then the statement holds.

• If M = n, +, max or ×, then the statement is obviously also true (note that for × we are using the fact that the base domain is N * and not N). • If M is an application, it can be written as M = (. . . (M 0 ) M 1 ) . . . ) M n ) where M 0 is not an application and n ≥ 1. Moreover M 0 cannot be an abstraction since M is in β-normal form, and it cannot be a variable y since M can only have free variables of type N. So M 0 = c for c = +, max or ×, and therefore n ≤ 2. We obtain that the M i s for 1 ≤ i ≤ 2 are of type N hence also satisfy the hypothesis, and thus by i.h. they satisfy the claim. Therefore the claim is also valid for M . • Finally the only possibility left is M = λx.M 1 . By definition of HOMPs we know then that x is a free variable of M 1 of type N, and as M 1 satisfies the hypothesis, by i.h. we know that M 1 satisfies the claim. Therefore the claim is valid for M .

This concludes the proof. The following will be useful to obtain the Subterm Property:

Lemma 28 For every type A there is a closed HOMP of type A.

Proof : By induction on A:

• If A is simply N, then the required HOMP is simply 1;

where the HOMPs M j i exist by induction hypothesis.

Higher-Order Quasi-Interpretations

Now, a HOMP assignment [ • ] is defined by: for any

a closed HOMP M ) with a type B, where B is obtained from A by: • replacing each occurrence of a base type D by N,

• replacing each occurrence of → in A by either → or ⊸. For instance if A = (D 1 → D 2 ) → D 3 we can take for B any of the types: (N ⊸ N) → N, (N → N) → N, etc. In the sequel we will write A for any of these types B. Then [ • ] is extended inductively to all t ∈ T as for HOP assignments.

Lemma 29 Let t ∈ T of type A and F V (t) = {y 1 : A 1 , . . . , y n : A n }, then: [t] is a HOMP, with a type A, and F V ([t]) = {y 1 : A 1 , . . . , y n : A n } for some types A i , 1 ≤ i ≤ n.

Additive HOMP assignments are defined just as additive HOP assignments.

Lemma 30 Let [ • ] be an additive HOMP assignment. Then there exists γ ≥ 1 such that for any value v of type D, where D is a data type, we have v ≺ ≤ γ • |v|. Now, we say that an assignment [ • ] is a quasi-interpretation for R if for any rule l → r of R, it holds that l ≤ ≥ r ≤ . Observe that contrarily to the case of polynomial interpretations these inequations are not strict, and moreover they are stated with respect to the new domains, taking into account the distinction between the two connectives → and ⊸.

The interpretation of a term does not, like in the strict case, necessarily decrease along a reduction step. However, it cannot increase:

Proof : [Sketch] This can be done in a way analogous to what has been done for polynomial interpretations with Lemma 16, using intermediary lemmas for substitutions and contexts similar to lemmas 14 and 15, but it is actually easier because here we are not considering a strict order.

The previous lemma, together with the possibility of forming HOMPs of arbitrary type (Lemma 28) implies the following, crucial, property:

Proposition 32 (Subterm Property) Suppose that an STTRS R has an additive quasi-interpretation [ • ]. Then, for every function symbol f of arity n with base arguments, there is a polynomial p : N n → N such that if (f t 1 . . . Proof : Denote t = (f t n . . . t n ). Its type A can be written as A = A 1 , . . . , A k → D, where D is a base type. By Lemma 28, for any i ∈ 1, . . . , k there is a closed HOMP M i of type A i . Consider now t ′ = (f x 1 . . . x n ) where for i ∈ 1, . . . , n, x i is a free variable of same type as t i .


Marc-Olivier Killijian

Matthieu Roy
email: roy@laas.fr

Gaetan Severac
email: gaetan.severac@onera.fr

The ARUM Experimentation Platform : an Open Tool to evaluate Mobile Systems Applications

published or not. The documents may come

Fig. 1 A picture of the the ARUM Platform Indeed, current evaluation strategies for distributed and mobile systems can be split in five categories:

• Simulators. Simulators are cheap and fast to set up, with almost no limitation in the number of nodes. Due to their scalability and simplicity, they are well suited for initial testing. Furthermore, they may speed up development of theoretical researches because since they allow a perfect monitoring and repeatability [START_REF] Stojmenovic | Simulations in wireless sensor and ad hoc networks: matching and advancing models, metrics, and solutions[END_REF][START_REF] Boleng | A survey of mobility models for ad hoc network research[END_REF]. Nevertheless, simulation is based on models of the running environment, and thus cannot reflect the real complexity of natural environments, particularly for radio communication and mobility pattern [START_REF] Chin | Implementation experience with manet routing protocols[END_REF][START_REF] Cavin | On the accuracy of manet simulators[END_REF][START_REF] Elyes | Impact of the Physical Layer Modeling on the Accuracy and Scalability of Wireless Network Simulation[END_REF]] . • Emulators. Emulators are built to physically reproduce connections events using real wired network hardware [START_REF] Matthes | Massive: An emulation environment for mobile ad-hoc networks[END_REF][START_REF] Pužar | Neman: A network emulator for mobile ad-hoc networks[END_REF]. They provide features interesting for protocol implementation but they still use simulation to reproduce wireless communication behaviour and mobility [START_REF] Beuran | Qomb: A wireless network emulation testbed[END_REF]. • Testbeds. The ARUM platform we present in this paper can be classified in this category. Testbeds are closer to reality thanks to the use of real hardware. They exist since years now, from the historical MIT RoofNet [START_REF] Aguayo | Mit roofnet: Construction of a production quality ad-hoc network[END_REF], to the more recent MoteLab2 service. Ideal to finalize and validate applications before real-life experimentations, testbeds provide much more realistic results than emulators or simulators. But they are also expensive, time consuming and limited by the physical resources/hardware used [START_REF] Kropff | A survey on real world and emulation testbeds for mobile ad hoc networks[END_REF]. Because of those limitations, only a few of them implement real mobility. To the best of our knowledge, two platforms using mobile robots have been recently developed: MINT [START_REF] Mitchell | Testbed design and localization in mint-2: A miniaturized robotic platform for wireless protocol development and emulation[END_REF] and Mobile Emulab [START_REF] Johnson | Mobile emulab: a robotic wireless sensor network testbed[END_REF].

Original solutions that emulate mobility can also be found in the literature, like MOBNET [START_REF] Kun Chan Lan | Mobnet: the design and implementation of a network mobility testbed for nemo protocol[END_REF] which varies the transmission power levels of fixed access points.

It is interesting to notice that most of these platforms have to deal with large variations in the communication noise level because of environment perturbations.

Such difficulties can be problematic during applications development phases, but they are representative of conditions encountered in the real life. • Hybrid simulators use both simulated networks and real devices, taking advantages and disadvantages of each [START_REF] Osterlind | Sensornet checkpointing: Enabling repeatability in testbeds and realism in simulations[END_REF][START_REF] Zhou | Twine: A hybrid emulation testbed for wireless networks and applications[END_REF]. They are particularly suited to study, at a low cost, the interconnection of some real devices to a huge network, the latter being simulated. • Real live experiments. This is, obviously, the more realistic kind of experimentation, but they present inherent technical problems which can bring more technical difficulties than scientific benefits [START_REF] Kiess | A survey on real-world implementations of mobile ad-hoc networks[END_REF][START_REF] Langendoen | Murphy loves potatoes: experiences from a pilot sensor network deployment in precision agriculture[END_REF]. They are absolutely necessary for commercial applications, because it is impossible to truly simulate real environment yet. Yet, they are very expensive, error-prone, and they do not provide repeatability of experiments, due to the wide variability of real environments. As such, such platforms are not used in the context of research and education.

Fig. 2 Accuracy of evaluation solutions for mobile systems depending on their respective costs Among all these technologies, there is no good or wrong solutions, the best choice depends on a specific needs and available resources, as shown in Figure 2.

In our case, both for scientific and for demonstration reasons, we decided to implement a testbed, the ARUM platform. Indeed our primary goal was to complement simulation and allow realistic evaluation of mobile systems, at a laboratory scale. It finally appeared to be a good platform for demonstration and education, since the platform can be used pedagogically to present various aspects and problems raised by mobile systems. The work describe here is an application of mini-robots to research, in a field different from robotics. However the solutions tested and implemented here can be applied to several important problems in multi-robotic field (e.g. positioning, mobility, communication...).

Design

To complete the goals presented in previous section, we designed an experimental evaluation platform composed of mobile devices. We dispose of a room of approximately 100m 2 to emulate systems of different sizes, hence we decided to scale every parameter of the system to fit within our physical constrains. Technically speaking, each mobile device is built with : a programmable mobile hardware able to carry the device itself, a lightweight processing unit equipped with one or several wireless network interfaces and a positioning device. Hardware modelling required a reduction or increase of scale to be able to conduct experiments within the laboratory. To obtain a realistic environment, all services have been modified according to the same scale factor. In our case, we considered vehicular ad-hoc network experiments [START_REF] Killijian | Data backup for mobile nodes : a cooperative middleware and experimentation platform[END_REF]. A typical GPS embedded in a moving car is accurate to within 5-20m. So, for our 100m 2 indoor environment to be a scaled down representation of a 250000m 2 outdoor environment (a scale reduction factor of 50), the indoor positioning accuracy needs to be 10 -40cm. Table 1 summarizes the required change in scale for all peripherals of a node.

We understand here that to meet those requirements some parts of the development were much more important. The focus was put on the reduced Wi-Fi interfaces, the precise positioning and the node mobility.The different parts of the platform will be detailed in the following section.

3 Technical solutions

Mobility

To reproduce mobile systems conditions, the devices used in the platform must be mobile. But when conducting experiments, a human operator cannot be behind each device, so mobility has to be automated. This is why we considered the use of simple small robots in order to carry around the platform devices. The task of these robots is to implement the mobility of the nodes following a movement scenario. A node, represented in figure 3, is implemented in the system using a laptop computer that is carried by a simple robotic platform, that includes all hardware devices, the software under testing and the software in charge of controlling robots movements. Notice that software under testing and control software are totally independent, there are running on the same computer for practical reasons only.

For the mobile platform we use Lynxmotion 4WD rover. We selected it instead of other smaller robot (e.g. Lego Mindstorm) because this rover is able to carry a payload of 2 Kg during a few hours, running at a maximum speed of 1m/s. It is also relatively cheap (cf. table 2) and easy to build. We equipped it with infra-red proximity sensors to avoid collision, a top deck to support the laptop, a positioning system and a modified Wi-Fi interface.

The motion control software, running on the carried laptop, communicates speeds orders (linear speed and angular speed) to the robot. The mobility patterns are drawn by an operator for each mobile robot, using a dedicated software, that sends it to the mobile nodes control software. This enables flexibility -each node has its own mobility pattern -and repeatability -a pattern can be saved and replayed.

Localization

Positioning is a critical point of the platform. Firstly, we need to reproduce the kind of information produced by actual market solutions such as GPS, pondered by our scale factor. Secondly, we need a precise and real-time position of the mobile node to allow an accurate motion control of the robot. Our specifications required a precision within the centimetre and a minimum refresh of 2 Hz. Several technologies are currently available for indoor location [START_REF] Hightower | A survey and taxonomy of location systems for ubiquitous computing[END_REF], mostly based either on scene analysis (e.g. using motion capture systems) or on triangulation (of RF and ultrasound [START_REF] Smith | Tracking moving devices with the cricket location system[END_REF] or wireless communication interfaces [START_REF] Correal | An uwb relative location system[END_REF]). During the building of the platform, we tried four different solutions.

We first tested the Cricket system [START_REF] Smith | Tracking moving devices with the cricket location system[END_REF], developed by MIT. Cricket is based on simultaneous ultrasound/RF messages and triangulation. Beacons fixed on the celling send periodically RF message with their ID and position, and, in the time, they send an equivalent message by ultrasounds. The flight time of the RF message is insignificant compare to that of the ultrasound. So the receiver, embedded on the mobile robot, can estimate the flight time of the ultrasound messages and and calculate, with at least 3 different messages received, its position. This position is then send to the mobile node via a serial connection. In theory, this system is very efficient, but in practice we were confronted to important limitations due to ultrasound disturbances. The ultrasound speed in the air can change depending of the temperature, so the results obtained can vary in the same way, and the ultrasound are also very sensitive to noise and perturbations. Neon lights was perturbing the systems and robots vibration, when they were moving, generated a lot of disturbances in the results. Finally we had to abandon this technology. To reach our desired level of accuracy for indoor positioning, we then used a dedicated motion capture technology that tracks objects based on real-time analysis of images captured by fixed infra-red cameras. The Cortex system3 is able to localize objects at the millimetre scale. This technology uses a set of infra-red cameras, placed around the room, that track infra-red-visible tags. All cameras are connected to a server that computes, based on all cameras images, the position of every tag in the system. We equipped our small robots with such tags to get their positioning information. The figure 4 shows compared results of the ultrasounds and infra-red systems. Although the precision attained was more than enough for our needs, the system has some drawbacks: the whole system is very expensive (in the order of 100kEuros), calibration is a tedious task, and infra-red signals cannot cross obstacles such as humans.

The localization system currently used is the Hagisonic StarGazer technology4 . It is also based on infra-red camera but they are small and embedded on-board on the mobile robots. They locate themselves by tracking statically placed infra-red-visible tags. With Hagisonic, a camera needs to see only one single tag to be able to calculate its position and the precision is about a few millimetres, with a frequency of 10 Hz. So this technology, more affordable, was plenty satisfying our requirements.

An Ultra-Wide-Band-based localization system (UWB), by Ubisense5 , has also been deployed and used for the experiments. Localization is performed by 4 sensors, placed in the room at each corner, that listen for signals sent by small tags that emit impulses in a wide spectrum. Such impulses can traverse human bodies and small obstacles, so the whole system is robust to external perturbation, but, from our preliminary measurements, attainable precision is about 10cm. The next step will be to couple this technology with the Hagisonic camera system, resulting in a localization system with better properties: it will be relatively cheap, robust to external perturbations such as obstacles, and will have most of the time a precision about the order of a centimetre.

To keep our experimental platform positioning system generic, despite the numerous different technologies used, we developed a position server, accessible via the supervision wireless network of the experimentation room. Two kinds of clients can communicate with it, using standard XML messages. A client can be a position provider (Cortex, Hagisonic, UWB...) and send to the server the position of one or several mobiles or the client can be a position consumer (supervision application, motion control software...) and ask to the server the position of one or several mobiles. Using this strategy, it is possible to change the technology of one system, provider or consumer of position, and the modification will remain transparent to all the other devices.

Scenario Drawing Interface

To have adequate experimental conditions, the mobile nodes of the platform need to follow and repeat defined mobility scenario. But first, an operator has to define the mobility scenario. We developed a graphical user interface to draw, configure, visualize and manage mobility patterns. Now the interface is a complete program composed of 7 different tabs, figure 5 shows a screen-shot. The Point tab where users can define passage points on a map. The Route tab to edit robots routes using the passage points previously created, the trajectory will be calculate from those routes, it is also possible to specify time constraints and add some pauses in the route execution. The Simulation tab permits to see an overview of the robots movements, you can select the different routes you want to visualise. The Rovers tab is used to configure the TCP/IP connexion attributes to communicate with the robots. You can select the route each robot will execute in the Association tab. The Upload tab is designed to send the routes to the corresponding robots and start, stop or pause their executions. Finally the Remote Control tab allows to manually control a robot, with a virtual joystick, and give the possibility to dynamically define a route from its movements. The interface is coded in Java and can be run on any computer connected to the supervision network. The mobility scenarios and movement orders are send to the mobile node via "Java Remote Method Invocation" (Java RMI).

Motion control and trajectory computing

As you can see on figure 6, the mobility scenarios defined with the GUI are sent to the robot via Java Remote Method Invocation" (Java RMI). A robot control program, coded in Java, receives a scenario description or the movements orders from the scenario drawing interface. This program is running on the embedded computer of the mobile node. The mobility scenarios are then converted into commands and sent to the robot motion control environment. This environment is composed of GenoM6 modules in charge of computing the final trajectory and controlling the robot speed to follow it. Proximity infra-red captors are continuously polled to stop the robot if an obstacle is detected.

We chose the GenoM environment, developed at the LAAS-CNRS laboratory, because it is an open source solution, already functional and still maintained by the robotic community. GenoM is a tool to design real-time software architectures. It is more specifically dedicated to complex on-board systems, such as autonomous mobile robots or satellites. It allows to encapsulate the operational functions on independent modules that manage their execution. The functions are dynamically started, interrupted or (re)parametrized upon asynchronous requests sent to the modules. A final reply that qualifies how the service has been executed is associated to every request. The modules are automatically produced by GenoM using a common generic model of module and a synthetic description of the considered module. At the end a set of modules composes an open, communicant and controllable system. Such environment can be very powerful and it used in our laboratory to control complex robots. In this platform, where the environment is controlled, the mobility is very simply implemented and we only used two GenoM modules. The module "Pilo", to compute the final trajectory (using Euler spirals) and the module "Loco" which controls the robot speed to follow the trajectory. The "Loco" module uses the position system to get in real time the position of the mobile node and send required linear and angular speed orders to the motors control card of the robot, through a serial connexion.

Reduced wireless communication

The communication range of the participants (mobile nodes and infrastructure access-points) has to be scaled according to the experiment being conducted. For our first experimentation, the scale factor had to be 50 (cf. Table 1) but, ideally, the communication range should be variable. Some Wi-Fi network interface drivers propose an API for reducing their transmission power. But the implementation of this feature is often rather limited, or ineffective, at a single room scale. A satisfying solution consists in using signal attenuators 7 placed between the Wi-Fi network interfaces and their antennas. The necessary capacity of the attenuators depends on many parameters such as the power of the Wi-Fi interfaces and the efficiency of the antennas, but also on the speed of the robot movements, the room environment, etc. As it is impossible to predict or calculate the Wi-Fi radio wave propagation we conducted empirical experimentation [START_REF] Killijian | Experimental evaluation of ubiquitous systems: Why and how to reduce wifi communication range[END_REF] to establish the relationship between signal attenuation and communication range, figure 7 show a picture of an experimentation. This experiment involves two laptops mounted on a mobile robot platforms and using an external Wi-Fi interface to communicate with each other. One of the two nodes is static and the other one moves back and forth. Equivalent attenuators are attached between each external Wi-Fi interface and its antenna. The mobile platform moves along a line, stops every 20cm for 5min and performs a measurement at every stop, figure 7. For each measurement, the moving laptop joins the ad-hoc network created by the fixed one, measures the communication throughput and then leaves the ad-hoc network. The time for joining the network is logged, as is the measured throughput. A complete experiment is composed of 100 repetitions of a return trip along the 5m line. This data is logged and statistically analysed off-line, leading to figure such as the one presented on figure 8. To validate that those attenuated results correspond to real Wi-Fi propagation behaviour, we reproduce the same experiment, outdoor, without attenuation and we obtain exactly the same kind of graphic shape, distances range excepted of course. Thanks to those multiple results we can now use the adequate attenuation depending on the specification of the experiments and we can certify that this will be representative to real Wi-Fi connexion conditions.

Supervision network

For the communications between the collaborative algorithms tested on the platform, the attenuated Wi-Fi interfaces previously presented are used. So the internal wireless card of the embedded computers is available for monitoring. Connected to a LAN access point, it provides direct access to each computer without disrupting the current experiment. This system is used to send monitoring information to the robot (e.g. position, commands, ...) and to retrieve data from the mobile nodes in real time, allowing a dynamically overview and analysis of the tested algorithms.

Implementation and Price

It is interesting to consider that all the different parts of a mobiles nodes (localization, trajectory planning, robot control, communication, ...) are connected thought clearly defined and documented interface, so it is easy and fast to change one of this part to make the platform evolve, without re-designing everything (cf. figure 6). For example we envisage buying a new localization system and changing the Lynxmotion robot for a Roomba8 development mobile platform. Anyone interested in reproducing our evaluation platform in a laboratory can reuse some parts of interest and modify others. Full documentation and sources of the platform are available at: http://projects.laas.fr/ARUM/. As an indication, Table 2

Experimentation and Lessons Learnt

To evaluate our ARUM platform, we experiment the Distributed Black-Box application, or DBB for short. This work was conducted in the course of the European project HIDENETS 9 . The application developed provides a virtual device, whose semantics is similar to avionics black-boxes, that tracks cars history in a way that can be replayed in the event of a car accident. It ensures information is securely stored using replication mechanisms, by means of exchanging positions between cars. This architecture is a partial implementation of the HIDENETS architecture and has been detailed in the project deliverable [START_REF]Hidenets. revised reference model[END_REF].

The ARUM platform was used to emulate the network of communicating cars. Through this work, the global performance of the evaluation platform was validated. The modularity and repeatability of the mobility patterns was used to test and improve the DBB algorithms in controlled situations. The use of real, power reduced Wi-Fi interfaces allowed realistic results; we monitored during the experiment wireless signal variations similar to real wireless network behaviour in difficult conditions (maximum range limit, noise perturbation, obstacle, ...).

A very precise positioning system was used both by the tested cooperative algorithms and the robot motion control software, without disturbances. With hindsight we have to admit that, even if we get positive results, we had to deal with a lot of contingencies. The total labour cost of the platform development was more consequent than expected. Some parts of the development would have been impossible to reduce -attenuated Wi-Fi scaling, positioning systems tests -but if we had to rebuild all from scratch we would probably choose a mobile robotic platform that already has motion control implemented -such as the Roomba Devel platform.

However, now that the platform is finished and validated, it can be used as a tool "out of the box"; anyone can come to the laboratory to implement algorithms on the mobile nodes. As showed in Section 3, it is possible to interface any code with the different parts of the mobile node -communication, positioning, monitoring, ... -and to easily program a mobility pattern. All the parts of the platform are segmented by software interfaces, defined in the documentation 10 , so it can quickly be handled and adapted by anybody interested. Additionally the sources of each software module can be downloaded to build a similar platform in another laboratory.

Even if it is not the primary function of this platform, we noticed that the versatility and the easiness of use of this platform makes it an interesting educational tool. All the different parts of it, presented in Section 3, can be used, studied and replaced by students. The localization, the mobility scenario computing, the motion control and trajectory calculation or the reduces wireless communication, could support interesting university work.

Conclusion

This article started by pointing out the difficulties of evaluation of application for mobile devices systems. It presented the difficulties encountered to emulate a realistic mobile network environment at a laboratory scale. Those observations motivated the development of a testbed platform designed to evaluate distributed applications. Thanks to use of mini-robots, this platform, named ARUM, appears to provide an interesting compromise between resources consumption (in terms of manpower) and accuracy of results, appropriate to complement simulation. The whole architecture is described part by part to ease reuse by researchers or in an educational context, while reducing the waste of time and money in development and tests.

Fig. 3 A

 3 Fig. 3 A Mobile Node Picture, without the embedded computer

Fig. 4

 4 Fig. 4 Comparative results of Ultrasounds (left) and Infra-red (right) positioning systems. A robot is tracked by the two different systems while following the same circuit drew on the floor

Fig. 5

 5 Fig. 5 Screen-shot of the mobility scenario drawing interface

Fig. 6

 6 Fig. 6 Mobile Node architecture Overview

Fig. 7

 7 Fig. 7 The attenuation WiFi experiments

Fig. 8

 8 Fig. 8 The attenuation WiFi experiments

Table 1

 1 Scale needs

	Device	Real Accuracy	Scaled Accuracy
	Wireless	range: 100m	range: 2m
	GPS	5m	10cm
	Node size	a few meters	a few decimeters
	Node speed	a few m/s	less than 1m/s

Table 2

 2 sums the actual price of the different parts of a mobile node. Platform devices Costs

	Device	Price ($)
	Linxmotion mobile Platform Kit	1 000
	Hagisonic IR Camera	1000
	Wireless WiFi interface	50
	Attenuators	70
	Laptop	1200
	Serial-USB Adaptors	30
	Total	3350

Harvard Sensor Network Testbed -http://motelab.eecs.harvard.edu

Marc-Olivier Killijian, Matthieu Roy, and Gaetan Severac

Cortex Motion Capture -http://www.motionanalysis.com

Hagisonic -http://www.hagisonic.com/

Ubisense -http://www.ubisense.net/en/products/precise-real-time-location.html

GenoM -https://softs.laas.fr/openrobots/wiki/genom

An attenuator is an electronic device that reduces the amplitude or power of a signal without appreciably distorting its waveform.

Roomba Devel -http://www.irobot.com/images/consumer/hacker/roombascispecmanual.pdf

HIghly DEpendable ip-based NETworks and Services -http://www.hidenets.aau.dk/

ARUM platform -http://projects.laas.fr/ARUM/