Emmanuel Hainry
email: hainry@loria.fr

Romain Péchoux
email: pechoux@loria.fr

Types for controlling heap and space in Java

A type system is introduced for a strict but expressive subset of Java in order to infer resource upper bounds on both the heap-space and the stack-space requirements of typed programs. This type system is inspired by previous works on Implicit Computational Complexity, using tiering and non-interference techniques. The presented methodology has several advantages. First, it provides explicit polynomial upper bounds to the programmer, hence avoiding OutOfMemory and StackOverFlow errors. Second, type checking is decidable in linear time. Last, it has a good expressivity as it analyzes most object oriented features like overload, inheritance, and also handles flow statements controlled by objects.

Introduction

In the last decade, the development of embedded systems and mobile computing has led to a renewal of interest in predicting program resource consumption. This kind of problematic is highly challenging for popular object oriented programming languages which come equipped with environments for applications running on mobile and other embedded devices (e.g. Dalvik, Java ME or Java Card).

The current paper tackles such an issue by introducing a type system for a compile-time analysis of both heap and stack space requirements of Java-like programs thus avoiding OutOfMemory and StackOverFlow errors, respectively. The analyzed programs form a strict but expressive subset of Java, named core Java which features traits like recurrence, while loops, inheritance, override, overload. Core Java will be presented in a theoretically oriented manner in order to highlight the theoretical soundness of our results. It can be seen as a language strictly more expressive than Featherweight Java [START_REF] Igarashi | Featherweight java: a minimal core calculus for java and GJ[END_REF] enriched with features like variable updates and while loops.

The type system combines ideas coming from tiering discipline, used for complexity analysis of function algebra [START_REF] Bellantoni | A new recursion-theoretic characterization of the poly-time functions[END_REF][START_REF] Leivant | Lambda calculus characterizations of poly-time[END_REF], together with ideas coming from non-interference, used for secure information flow analysis [START_REF] Volpano | A sound type system for secure flow analysis[END_REF]. It is inspired by two previous works: the seminal paper [START_REF] Marion | A type system for complexity flow analysis[END_REF], initiating imperative programs type-based complexity analysis using secure information flow, which provides a characterization of polynomial time computable functions; and the paper [START_REF] Hainry | Type-based complexity analysis for fork processes[END_REF], extending previous analysis to C processes with a fork/wait mechanism, which provides a characterization of polynomial space computable functions, but this work differs on a number of points. First, it is an extension to the object-oriented paradigm (although imperative feature can be dealt with). In particular, it characterizes the complexity of recursive and non-recursive method calls whereas previous works where restricted to while loops. Second, it studies program intensional properties (like heap and stack) whereas previous papers were focusing on the extensional part (characterizing function spaces). Consequently, it is closer to a programmer's expectations. Third, it provides explicit big O polynomial upper bounds while the two aforementioned studies were only certifying algorithms to compute a function belonging to some fixed complexity class.

In our setting, the heap is represented by a directed graph where nodes are object addresses and arrows map an object address to its attribute addresses. The type system splits variables in two tiers: tier 0 and tier 1. While tier 1 variables are pointers to nodes of the initial heap, tier 0 variables may point to newly created addresses. Information may flow from tier 1 to tier 0.But our type system precludes flows from 0 to 1. Naively, tier 1 variables are the ones that can be used either as guards of a while loop or as a recursive argument in a method call whereas tier 0 variables are just used as a storage for computed data. The idea for the polynomial upper bound relies on the fact that if the input graph structure has size n then the number of distinct possible configurations for k tier 1 variables is at most O(n k ).

There are several related works on the complexity of imperative and object oriented languages. On imperative languages, the papers [START_REF] Niggl | Certifying polynomial time and linear/polynomial space for imperative programs[END_REF][START_REF] Moyen | Resource control graphs[END_REF][START_REF] Jones | A flow calculus of wp-bounds for complexity analysis[END_REF] study theoretically the heap-space complexity of core-languages using type systems based on a matrix calculus. On OO programming languages, the papers [START_REF] Hofmann | Type-based amortised heap-space analysis[END_REF][START_REF] Hofmann | Efficient type-checking for amortised heap-space analysis[END_REF] control the heap-space consumption using type systems based on amortized complexity introduced in previous works on functional languages [START_REF] Hofmann | Static prediction of heap space usage for first-order functional programs[END_REF][START_REF] Jost | Static determination of quantitative resource usage for higher-order programs[END_REF][START_REF] Beringer | Automatic certification of heap consumption[END_REF]. Though similar, our result differs on several points.First, our analysis is not restricted to linear heap-space upper bounds. Second, it also applies to stack-space upper bounds. Last but not least, our language is not restricted to the expressive power of method calls and includes a while statement, controlling the interlacing of such a purely imperative feature with functional features like recurrence being a very hard task from a complexity perspective. Another interesting line of research is based on the analysis of heap-space and time consumption of Java bytecode [START_REF] Albert | Costa: Design and implementation of a cost and termination analyzer for java bytecode[END_REF][START_REF] Albert | Cost analysis of object-oriented bytecode programs[END_REF][START_REF] Cachera | Certified memory usage analysis[END_REF]. The results from [START_REF] Albert | Costa: Design and implementation of a cost and termination analyzer for java bytecode[END_REF][START_REF] Albert | Cost analysis of object-oriented bytecode programs[END_REF] make use of abstract interpretations to infer efficiently symbolic upper bounds on resource consumption of Java programs. A constraint-based static analysis is used in [START_REF] Cachera | Certified memory usage analysis[END_REF] and focuses on certifying memory bounds for Java Card. Our analysis can be seen as a complementary approach since we try to obtain practical upper bounds through a cleaner theoretically oriented treatment. Consequently, this approach allows us to deal with our typing discipline on the original Java code without considering the corresponding Java bytecode. A complex type-system that allows the programmer to verify linear properties on heap-space is presented in [START_REF] Chin | Memory usage verification for OO programs[END_REF]. Our result in contrast presents a very simple type system that however guarantees a polynomial bound.

In a similar vein, characterizing complexity classes below polynomial time is studied in [START_REF] Hofmann | Pointer programs and undirected reachability[END_REF][START_REF] Hofmann | Pure pointer programs with iteration[END_REF]. This work relies on a programming language called PURPLE combining imperative statements together with pointers on a fixed graph structure. Although not directly related, our type system was inspired by this work. This work is independent from termination analysis but our main result relies on such analysis. Indeed, the polynomial bounds on both the stack and the heap of typed programs provided by Theorem 1 only hold for a terminating computation. Consequently, our analysis can be combined with termination analysis in order to certify the upper bounds on any input. Possible candidates for the imperative fragment are Size Change Termination [START_REF] Ben-Amram | Size-change termination, monotonicity constraints and ranking functions[END_REF][START_REF] Ben-Amram | On the termination of integer loops[END_REF], tools like Terminator [START_REF] Cook | Terminator: Beyond safety[END_REF] based on Transition predicate abstraction [START_REF] Podelski | Transition predicate abstraction and fair termination[END_REF] or symbolic complexity bound generation based on abstract interpretations, see [START_REF] Gulwani | Speed: Symbolic complexity bound analysis[END_REF][START_REF] Gulwani | Speed: precise and efficient static estimation of program computational complexity[END_REF] for example.

Core Java syntax

We start to introduce the syntax of the considered core Java language a strict but expressive subset of Java. Expressions, instructions, methods, constructors and classes are defined by the grammar of Figure 1 [e] denotes some optional element e and E denotes a sequence of expressions E 1 , . . . , E n . ';' denotes the empty instruction. This syntax does not include a for instruction as it can be simulated with a while. Also notice that there is no attribute access in our syntax using the '.' operator. Getters will be needed, as if all attributes were private. On the opposite, methods and classes are public.

, with x ∈ V, op ∈ O, C ∈ C, m ∈ E ::= x | null | this | true | false| op(E ) | new C(E ) | E .m(E ) I ::= ; | [τ ] x:=E ; | I1 I2 | while(E ){I }| if(E ){I1}else{I2} | E .
Definition 1. A core Java program is a collection of classes together with exactly one executable: Exe{main(){τ 1 x 1 := E 1 ; . . . ; τ n x n := E n ; I }}. In an executable, the instruction τ 1 x 1 := E 1 ; . . . ; τ n x n := E n ; is called the initialization instruction whereas I is called the computational instruction.

We adopt OO nomenclature regarding attributes, parameters, signatures, and local variables. Also let C.A denote the set of the attributes of the class. We write m ∈ C to denote that the method name m is declared in C.

Throughout the paper, we assume that programs are well-formed, meaning that there does not appear undefined class names or variables, no multiply declared variables, no name clashes (variable names and class names are unique), signatures of methods are respected by the implementations.

Core Java pointer graph semantics

In this section, we provide a pointer graph semantics of core Java programs for representing the memory heap.

Pointer graph

Definition 2. A pointer graph G P is a directed graph G = (V, A) together with a mapping P. The nodes in V are references labeled by class names and the arrows in A link to references to the attributes and are labeled by the attribute name. Let l be the node label mapping from V to C and i be the arrow label mapping from A to ∪ C∈C C.A. The partial mapping P : V ∪ {this} → V is called a pointer mapping. Let dom(P) to be domain of P.

This graph explicits the arborescent nature of objects: each constructor call creates a new node with arrows to its attributes, thus implementing the dynamic binding principle. Fig. 2 illustrates the pointer graph associated to a sequence of instantiations. Both the graph and the pointer mapping symbolized by snake arrows are represented.

Pointer stack

When calling a method, references to the parameters are pushed on the pointer stack which contains pointer mappings. Definition 3. A pointer stack S G is a LIFO structure of pointer mappings S corresponding to the same directed graph G. Given a pointer stack S G , define S to be the top pointer mapping of S.

Intuitively, the pointer mappings of a pointer stack S G map method parameters to the references of the arguments on which they are applied.

Memory configuration

A primitive store σ is a partial mapping σ : V → {true, false} associating a boolean value to some variable of primitive data type in V. Definition 4. A memory configuration C is a quadruple G, P, S, σ such that G P is a pointer graph, S G is a pointer stack and σ is a primitive store. The initial configuration C 0 is defined by C 0 = ({&null}, ∅), ∅, [], ∅ where ∅ is used both for empty set and empty mapping, [] denotes the empty pointer stack, and &null is the reference of the null object.

Meta-language and flattening

The semantics of core Java programs will be defined on a meta-language with flat expressions and instructions, and special meta-instructions push and pop.

ME ::= x | null | this | true | false | op(x 1 , . . . , x n ) | new C(x 1 , . . . , x n ) | y.m(x 1 , . . . , x n ) MI ::= ; | [τ ] x:=ME ; | MI 1 MI 2 | x.m(y 1 , . . . , y n ); | while(x){MI } | if(x){MI 1 }else{MI 2 } | pop; | push(P); |
Flattening an instruction I into a meta-instruction I will consist in adding fresh intermediate variables for each complex parameter. This procedure is standard and does not change the semantics.

Program semantics

Informally, the small step semantics → of core Java relates a pair (C, MI ) of memory configuration C and meta-instruction MI to another pair (C , MI ). Let → * (respectively → + ) be its reflexive and transitive (respectively transitive) closure. In the special case where (C, MI ) → * (C , ), we say that the metainstruction MI terminates on memory configuration C.

Definition 5. A program of executable Exe{main(){τ 1 x 1 := E 1 ; . . . ; τ n x n := E n ; I }} terminates if the following conditions hold: 1. (C 0 , τ 1 x 1 := E 1 ; . . . ; τ n x n := E n ;) → * (C, ) 2. (C, I ) → * (C , )
The memory configuration C is called the input.

Given a memory configuration C = G, P, S, σ , let C(x), intuitively the value of x, be defined by: C

(x) = σ(x) if x ∈ dom(σ); C(x) = S(x) if x ∈ dom( S); C(x) = P(x) if x ∈ dom(P) and let C[µ : x → v], µ ∈ {σ, P, S}, be a notation for the memory configuration C that is equal to C but on µ where C (x) = v. Moreover (C, ; MI ) → (C, MI ) (C, [τ ] x:=null; MI ) → (C[P : x → &null], MI ) (C, [τ ] x:=w; MI ) → (C[σ : x → w], MI ) w ∈ {true, false} (C, [τ ] x:=y; MI ) → (C[µ : x → C(y)], MI ) µ ∈ {σ, P, S} (C, [τ ] x:=this; MI ) → (C[P : x → (S)(this)], MI ) (C, [τ ] x:=op(y 1 , . . . , y n ); MI ) → (C[σ : x → op (C(y 1 ), . . . , C(y n ))], MI ) (C, [τ ] x:=new C(y 1 , . . . , y n ); MI ) → (C[V : v → C][A : (v, C(y i )) → zi][P : x → v], MI )
where v is a fresh node and C.A = {z1, . . . , zn} (v,w)) = x). We define dom(C) = dom(P) dom( S) dom(σ) and op to be the function computed by the language implementation of operator op.

(C, [[τ ] x:=]y n+1 .m(y 1 , . . . , y n ); MI ) → (C, push({this → C(y n+1 ), zi → C(y i )}); MI [x:=z; ] pop; MI ) with τ m(τ1 z1, . . . τn zn){MI [return z; ]} (C, push(P); MI ) → (C[S : push(P)], MI ) (C, pop; MI ) → (C[S : pop], MI ) (C, while(x){MI } MI ) → (C, MI while(x){MI } MI ) if C(x) = true (C, while(x){MI } MI ) → (C, MI ) if C(x) = false (C, if(x){MI true}else{MI false} MI ) → (C, MI w MI ) if C(x) = w ∈ {true, false}
The rules of → are defined formally in Figure 3.

4 Type system

Tiered types

The set of base types T is defined to be the set including a reference type C for each class name C and the special type void and the primitive type boolean. In other words, T = {void, boolean} ∪ C. Tiers are elements of the lattice ({0, 1}, ∨, ∧) where ∧ and ∨ are the greatest lower bound and least upper bound operators, respectively. The induced order, denoted , is such that 0 1. In what follows, let α, β, . . . denote tiers in {0, 1}. The minimum ∧ i∈S α i of a finite set is defined in a standard way.

A tiered type is a pair τ (α) consisting of a type τ ∈ T together with a tier α ∈ {0, 1}. Given a tiered type, we define the two projections π 1 and π 2 as follows: π 1 (τ (α)) = τ and π 2 (τ (α)) = α.

Environments

An attribute typing environment δ m C for a method m of class C maps each attribute v ∈ C.A to a tiered type. A local variable and parameter typing environment δ g maps each non-attribute variable in V to a tiered type. A typing environment ∆ is a list containing the unions δ m C δ g for each attribute typing environment and the local variable and parameter typing environment. Let ∆(m C ) denote δ m C δ g . A contextual typing environment Γ = (m C , ∆) is a pair consisting in a method and a typing environment. The method m C indicates in which context the attributes should be typed, in other words the δ m C is considered. We will write ( , ∆) when the context is empty. ∆( ) represents the local variable and parameter typing environment δ g .

Intuitively, tier 0 will be used to type variables whose corresponding stored values might increase during a computation whereas tier 1 will be used to type variables used in the guard of a while loop or as a recursive argument of a method call. Consequently, the values stored in a tier 1 variable will not be allowed to increase during a computation. Given a typing environment ∆ = (..., δ, ...) and a tier α, let ∆ α be the list of (..., δ α , ...) where δ α is the restriction of δ to variables or attributes of tier α, that is such that π 2 (δ(x)) = α).

Well-typed programs

Operator signature The language is restricted to operators whose return type is boolean. An operator of arity n comes equipped with a signature of the shape τ 1 × • • • × τ n → boolean, fixed by the language implementation. In the type system, the notation op ::

τ 1 × • • • × τ n → boolean denotes that op has signatureτ 1 × • • • × τ n → boolean.
Judgments Expressions and instructions will be typed using tiered types whereas constructors and methods of arity n have types of the shape:

τ 1 (α 1 ) × . . . × τ n (α n ) → τ (α) and C(β) × τ 1 (α 1 ) × . . . × τ n (α n ) → τ (α)
respectively. Given a contextual typing environment Γ , there are four kinds of typing judgments:

-The judgment Γ E : τ (α) means that expression E corresponds to values of tiered type τ (α). -The judgment Γ I : void(α) is similar but the type is enforced to be void, meaning that instructions have no return value.

-The judgment Γ K C : τ 1 (α 1 ) × • • • × τ n (α n ) → C(0)
enforces the output of a constructor to be of the correct type C and to be of tier 0, this important tiering restriction will prevent object instantiation in variables of tier 1.

-The last judgment Γ M C : C(β)×τ 1 (α 1 )ו • •×τ n (α n ) → τ (α) for methods is similar but unrestricted.
Well-typedness Let us now introduce the notion of well-typed program. Intuitively, a well-typed program has an executable whose initialization instruction is only constrained by types and whose computational instruction is both constrained on types and tiers. The type system propagates these constraints on all the classes, methods and instructions used within these instructions.

Definition 6 (Well-typed program). Given a program of executable Exe and a typing variable environment Γ = ( , ∆), the judgment Γ Exe : means that the program is well-typed wrt Γ .

Typing rules

Expressions The typing rules for expressions are provided in Figure 4. Rules (True), (False), (Null) and (Var) are self-explanatory. The (Self ) rule explicits that the self reference this belongs to class C and has a tier lower than the minimum of the attributes' tiers under the typing environment ∆(m C ), denoted by ∆(m C ) and defined formally by:

∆(m C ) = ∧ x∈C.A (π 2 (∆(m C )(x))).
This entails that an object of tier 1 has no attribute of tier 0, in other words, no arrow will go from a node corresponding to tier 1 to a node of tier 0.

Rule (Op) describes how to type an operator applied to n arguments. The arguments must be of types corresponding to the operator signature. The operands must be of the same tier α which will also be the tier of the whole expression. It prevents information to flow from a tier to the other.

Rule (New) describes the typing of object instantiation. It checks that the constructor arguments have tiered types τ i (β i ) of the same types τ i and of tier not lower than the admissible tiers α i in the constructor typing judgment. Note that the new instance has tier 0 since its creation makes the memory grow.

Rule (Call) represents how to type method calls of the shape E .m(E 1 , . . . , E n ). First, we check that the tiered type C(β) of the self reference in the method m matches the tiered type of the instance E . Simultaneously, the current method in the contextual typing environment is updated to m C . We check that the arguments' tiered-types agree with the parameters' tiered-types in m's signature. An important point to stress is that the tier of the evaluated expression (or instruction) in a method call matches the tier of the return variable in the method, hence avoiding forbidden information flows.

Instructions The typing rules for instructions are provided in Figure 5.

Rule (Ass) explains how to type an assignment: it is an instruction, hence of type void. It is only possible to assign an expression E to a variable x if both the types match and the tier β of E is higher than the tier α of x. The tier of the instruction will be α. This rule implies that information may flow from tier 1 to tier 0 but not the contrary.

(True) (m C , ∆) true : boolean(1) (False) (m C , ∆) false : boolean(1) (Null) (m C , ∆) null : C(1) α ∆(m C ) (Self ) (m C , ∆) this : C(α) ∆(m C )(x) = τ (α) (Var) (m C , ∆) x : τ (α) ∀i, (m C , ∆) Ei : τi(α) op :: τ1 × • • • × τn → boolean (Op) (m C , ∆) op(E1, . . . , En) : boolean(α) ∀i (m C , ∆) Ei : τi(βi) αi βi ( , ∆) C(. . . τi y i . . .){. . . xi := y i ; . . .} : τ1(α1) × • • • × τn(αn) → C(0) (New) (m C , ∆) new C(E1, . . . , En) : C(0) ∀i (m C 1 1 , ∆) Ei : τi(βi) αi βi (m C , ∆) m : C(β) × τ1(α1) × • • • × τn(αn) → τ (α) (m C 1 1 , ∆) E : C(β) (Call) (m C 1 1 , ∆) E .m(E1, . . . , En) : τ (α)
Fig. 4: Type system for core Java: Expressions Rule (Seq) types the sequence of two instructions I 1 and I 2 . The sequence's tier will be the maximum of the tiers of I 1 and I 2 .

(m C , ∆) x : τ (α) (m C , ∆) E : τ (β) α β (Ass) (m C , ∆) [τ ] x:=E ; : void(α) (m C , ∆) I : void(α) α β (Sub) (m C , ∆) I : void(β) ∀i, (m C , ∆) Ii : void(αi) (Seq) (m C , ∆) I1 I2 : void(α1 ∨ α2) (m C , ∆) E : boolean(1) (m C , ∆) I : void(1) (Wh) (m C , ∆) while(E ){I } : void(1) (Skip) (m C , ∆) ; : void(0) (m C , ∆) E : boolean(α) ∀i, (m C , ∆) Ii : void(α) (If ) (m C , ∆) if(E ){I1}else{I2} : void(α)
} : τ1(α1) × • • • × τn(αn) → C(0) (m C , ∆) this : C(β) ∀i, (m C , ∆) xi : τi(αi) (m C , ∆) I : void(α) (M void C ) ( , ∆) void m(τ1 x1, . . . , τn xn){I } : C(β) × τ1(α1) × • • • × τn(αn) → void(α) (m C , ∆) this : C(β) ∀i, (m C , ∆) xi : τi(αi) (m C , ∆) x : τ (α) (m C , ∆) I : void(α) (MC) ( , ∆) τ m(τ1 x1, . . . , τn xn){I return x; } : C(β) × τ1(α1) × • • • × τn(αn) → τ (α) ( ,
Rule (If ) describes the typing discipline for a if(E ){I 1 }else{I 2 } statement. E needs to be a boolean expression of tier α. I 1 and I 2 are instructions, hence of type void, with the same tier α. This prevents assignments of tier 1 variables in the instructions I 1 and I 2 to be controlled by a tier 0 expression.

Rule (Skip) is standard. Rule (Wh) is the most important typing rule as it will constrain the use of while loops. In a statement while(E ){I }, the guard of the loop E must be a boolean expression of tier 1 so that the guard is controlled. The instruction I , of type void, has to be of tier 1 since we expect the guard variables to be modified (i.e. assigned to). The whole statement is an instruction of type void and tier 1.

Methods, constructors and executable The typing rules for constructors and methods are provided in Figure 6.

Rule (K C ) describes the typing of a constructor definition. Constructors are of fixed form, so the only thing to check is that the parameters are of the desired tiered types. As explained in Rule (New) the output tier can only be 0.

Rules (M void C ) and (M C ) show how to type method definitions. In both cases, the types and number of parameters need to match the method signature, the instruction I in the body of the method needs to be of type void(α), i.e. the tier matches the output tier so that there is no forbidden information flow.

Finally, typing an executable is done through the rule (Main) and consists in verifying that the initialization instruction respects types and that the computational instruction (denoted by instruction I ) is of tier 1. Notice that no tier constraints are checked in the initialization instruction: this means that we do not control the complexity of this latter instruction ; the main reason for this choice is that this instruction is considered to be building the program input. In opposition, the computational instruction I is considered to be the computational part of the program and has to respect the tiering discipline.

5 Upper bound on the stack size and the heap size

Definitions

In this section, we state our main result showing that well-formed and typed programs have both pointer stack size and pointer graph size bounded polynomially by the input size under termination and safety assumptions. Moreover, precise upper bounds can be extracted. For that purpose, we need to define the notion of size for pointer stack, pointer graph and memory configuration.

Definition 7 (Sizes).

-The size of a pointer graph G P is defined to be the number of nodes in G and denoted |G P |.

-The size of a pointer stack S G is defined to be the number of pointer mappings in the stack S and denoted |S G |. -The size of a memory configuration G, P, S, σ is equal to

|G P | + |S G | + |dom(P)| + |dom(σ)|.
Since a pointer graph contains both references to the objects (the nodes) and references to the attribute instances (the arrows), it would make sense to bound both the number of nodes and the number of arrows in order to control the heap-space, for a practical application. Notice that the outdegree of a node is bounded by a constant of the program (the maximum number of attributes in a class) and, consequently, bounding the number of nodes is sufficient to obtain a big O bound. The size of a pointer stack is very close to the size of the Java Virtual Machine stack since it counts the number of nested method calls.

Given two methods M C and M C of respective signatures s and s and respective names m and m , define the relation on method signatures by s s if m is called in M C , i.e. in the body of M C (this check is fully static as long as we do not consider inheritance). Let + be its transitive closure. A method of signature s is recursive if s + s holds. Given two method signatures s and s , s ≡ s holds if both s + s and s + s hold. Given a signature s, the equivalence class [s] is defined as usual by [s] = {s | s ≡ s}. When the signature s of a given method M C of name m is clear from the context, we will write [m] as an abuse of notation for [s] and say that M C is a recursive method. Finally, we write s + s if s + s holds and s + s does not hold.

The notion of level of a meta-instruction is introduced to compute an upper bound on the number of recursive steps for a method call evaluation. Definition 8 (Level). Let the level λ of a method signature be defined as follows:

-λ(s) = 1 if s / ∈ [s] -λ(s) = max{1 + λ(s ) | s + s } otherwise.
By abuse of notation, we will write λ(m) when the signature of m is clear from the context. For a given program, we denote the maximal level of a method by λ.

The notion of intricacy corresponds to the number of nested while loops in a meta-instruction and will be used to compute the requested upper bounds. Definition 9 (Intricacy). Let the intricacy ν of a meta-instruction be defined as follows:

-ν(; ) = ν(pop; ) = ν(push(P); ) = ν(x:=ME ; ) = 0 -ν(MI MI ) = max(ν(MI ), ν(MI )) -ν(if(x){MI }else{MI }) = max(ν(MI ), ν(MI )) -ν(while(x){MI }) = 1 + ν(MI )
Moreover, let ν be the maximal intricacy of a meta-instruction within a given program.

Notice that both intricacy ν and level λ are bounded by the size of their corresponding program.

Safety restriction on recursive methods

Now we put some aside restrictions on recursive methods to ensure that their computations remain polynomially bounded. Recursive methods will be restricted to have only one recursive call and no while loop in their body (to prevent exponential growth) and must have tier 1 input (as the guard of a while) and output (to prevent a recursive dependence on a tier 0 variable).

Definition 10 (Safety).

A well-typed program with respect to a typing environment ∆ is safe if for each recursive method M C = τ m(. . .){MI [return x; ]}:

there is exactly one call to some m ∈ [m] in MI , there is no while loop inside MI , i.e. ν(MI ) = 0, and the following judgment can be derived:

( , ∆) M C : C(1) × τ 1 (1) × • • • × τ n (1) → τ (1).
Remark 1. A program is safe wrt a typing environment ∆ iff its flattened version is safe wrt a typing environment ∆ ⊇ ∆.

Main results

The presented type system allows us to infer polynomial upper bounds on the stack and the heap of safe programs. In the following theorem, we use n 1 to denote the number of variables and attributes of tier 1 in the whole program, that is #dom(δ 1 i ) for a typing environment ∆ = (..., δ i , ...) Theorem 1. If a core Java program of computational instruction I is safe wrt to typing environment ∆ and terminates on input C then for each memory configuration C and meta-instruction MI s. As a corollary, if the program terminates on all input configurations, then we may infer a polynomial time upper bound on its execution time.

Corollary 1. If a core Java program of computational instruction I is safe wrt to typing environment ∆ and terminates on input C then it does terminate in time O(|C| n1((ν+1)λ) ).

Another corollary is that tier 1 variables remain polynomially bounded without assuming termination. It means we can guarantee security properties on the data stored in such variables even if we are unable to prove program termination. where |C (x)| denotes the size of the subgraph of nodes reachable from node C (x) whenever x is of reference type.

Another direct result is that our characterization is complete with respect to the class of functions computable in polynomial time as a direct consequence of Marion's result [START_REF] Marion | A type system for complexity flow analysis[END_REF] since both our language and type system can be viewed as an extension of the considered imperative language. This means that our type system has a good expressivity.

Finally, we show the decidability of type inference wrt our type system:

Proposition 1 (Type inference). Deciding if there exists a variable typing environment Γ such that typing rules are satisfied can be done in time linear in the size of the program.

An illustrating example

Let us apply our framework to a simple class BList for encoding binary integers as binary lists (with the least significant bit in head). Tiers are made explicit in the code: The notation x α means that x has tier α under the considered contextual typing environment Γ , i.e. Γ x : τ (α), for some τ , whereas I : α means that Γ I : void(α). The constructor BList can be typed by boolean(α) × Blist(β) → BList(0), with α, β ∈ {0, 1}, depending on the typing environment, by rule (K C ).

9 BList getQueue () { return queue ; }

The method getQueue can be typed by BList(1) → BList(1) or BList(0) → BList(1) if ∆(getQueue BList )(queue)=1 and by BList(0) → BList(0) if ∆(getQueue BList )(queue)=0, by rules (M C ) and (Self).

The type BList(1) → BList(0) is prohibited by rule (Self) since the tier of the current object 1 has to be lower than the minimum tier of its arguments 0. The method setQueue can be given the types BList(1) × BList(1) → void(1),

BList(0) × BList(1) → void(α), or BList(0) × BList(0) → void(α), α ∈ {0, 1}.
The input type BList(1) × BList(0) is prohibited since the tier of parameter q (0) has to be greater than the tier of the attribute queue, by rule (Ass); but this latter tier has to be greater than the tier of the current object (1), by rule (Self). Finally, the output tier corresponds to the tier of the typed instruction by rule (M C ). Consequently, it also corresponds to the tier of the attribute queue by rule (Ass) and is enforced to be 1 when the current object has type 1, by the rule (Self). Notice that it can be 1 whenever the object current tier is 0 using the subtyping rule (Sub).

11 boolean getValue () { return value ; } getValue can be given the types BList(1) → boolean(1), BList(0) → boolean [START_REF] Albert | Costa: Design and implementation of a cost and termination analyzer for java bytecode[END_REF] or BList(0) → boolean(0) (the explanations are the same than for the getQueue getter).

12 BList double () { 13

BList n 0 = new BList ( f a l s e , t h i s ); 14 return n 0 ; 15 }

The method double can be typed by BList(0) → BList(0) or BList(1) → BList(0). Indeed the local variable n is enforced to be of tier 0 by a combination of rules (K C ) and (Ass). Consequently, the method output type is BList(0) since it has to match the type of the returned variable. Finally, there is no constraint on the current object admissibile types since it is left unchanged by the method. The method decrement is recursive. Consequently, the type BList(1) → void(1) is mandatory by safety. This enforces the tier of the each attribute to be 1 by rule (Self). Finally, the method body can be typed using a combination of rules (Ass), (If) and (Call). In the concat method, the presence of the method call o.getQueue() in the guard of the while loop enforces its ouput tier to be 1 by rules (Wh), (Null) and (Op). Consequently, the type of getQueue has to be BList(1) → BList(1) under the considered contextual typing environment (see the admissible types of getQueue). It also enforces the object o to be of tier 1. Consequently, the current object this is also enforced to be of tier 1 by rule (Ass) and the tier of the parameter other is enforced to be 1 (see the setQueue admissible types). Consequently, the only admissible type for concat is BList(1) × BList(1) → void(1), using rule (Seq). The local variables b1 and b2 are enforced to be of tier 1 by rule (Wh). Consequently, this and other are also of tier 1 using twice rule (Ass). Consequently, the methods getValue and getQueue will be typed by BList(1) → boolean [START_REF] Albert | Costa: Design and implementation of a cost and termination analyzer for java bytecode[END_REF] and BList(1) → BList(1), respectively. Finally, the local variable can be given the type boolean(1) or boolean(0) (in this latter case, the subtyping rule (Sub) will ne needed) and, consequently, the admissible types for isEqual are BList(1) × BList(1) → boolean(α), α ∈ {0, 1}.

Conclusion

This work presents a simple type-system (it can be checked in linear time) that provides explicit polynomial upper bounds on the heap and stack size of an object oriented program allowing (recursive) method calls. As the system is purely static, the bounds are not as tight as may be desirable. It would indeed be possible to refine the framework to obtain a better exponent at the price of a non-uniform formula (for example not considering all tier 1 variables but only those modified in each while loop or recursive method would reduce the computed complexity). OO features, such as inheritance, abstract classes, interfaces and static attributes and methods, were not considered here, but we claim that they can also be treated by our analysis. Moreover, constructs that breaks the control flow like break, return and continue can also be considered in our fragment (they have to be constrained to be of tier 1 so that if such an instruction is to be executed, then we know that it does not depend on tier 0 expressions). Also note that the safety condition can be alleviated on recursive methods by ensuring that only one recursive call is reachable in the execution of the method body.

Fig. 1 :

 1 Fig. 1: Syntax of core Java

Fig. 2 :

 2 Fig. 2: Example of a pointer graph

Lemma 1 .

 1 Define the size |I | of an instruction I (respectively meta-instruction |MI |) to be the number of symbols in I (resp. MI ). For each instruction I , we have |I | = O(|I |).

Fig. 3 :

 3 Fig. 3: Semantics of core Java

Fig. 5 :

 5 Fig. 5: Type system for core Java: Instructions

  ∆) I : void(1) ∀i, ( , ∆) xi : τi(αi) ∀i, ( , ∆) Ei : τi(βi) (Main) ( , ∆) Exe{main(){τ1 x1 := E1; . . . ; τn xn := En; I }} :

Fig. 6 :

 6 Fig. 6: Type system for core Java: Constructors, methods and executable

  t. (C, I ) → * (C , MI ) we have: |C | = O(|C| n1((ν+1)λ) ). In other words, if C = G, P, S, σ then both |G P | and |S G | are in O(|C| n1((ν+1)λ) ).

Corollary 2 .

 2 If a core Java program of computational instruction I is safe wrt to typing environment ∆ then, on input C, for each memory configuration C , meta-instruction MI s.t. (C, I ) → * (C , MI ) and variable x ∈ dom(δ 1 g ) we have: |C (x)| = O(|C| n1((ν+1)λ) ).

10

  void setQueue ( BList q ) { queue = q ; }

26

  void concat ( BList other 1 ) { 27 BList o 1 = t h i s 1 ;: 1 28 while ( o 1 . getQueue () != n u l l ) { o 1 = o 1 . getQueue ();: 1 } 29 o 1 . setQueue ( other 1 );: 1 30 }

31 1 34

 1 boolean isEqual ( BList other 1 ) { 32 boolean res 0 = true ; : 1 // using ( Sub ) 33BList b1 1 = t h i s 1 ; :BList b2 1 = other 1 ; : 1 35 while ( b1 1 != n u l l && b2 1 != n u l l ) { 36 i f ( b1 1. getValue () != b2 1 . getValue ()) { res 0 = f a l s e ;: 1 } 37 b1 1 = b1 1 . getQueue ();:1 38 b2 1 = b2 1 . getQueue ();: 1 39 } 40 i f ( b1 1 != n u l l || b2 1 != n u l l ) { res 0 = f al s e ;: 1 } 41 return res 0 ; 42 } 43 }


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

Bounding Reactions in the π-calculus using Interpretations

We present a new resource static analysis for the π-calculus that provides upper bounds on the number of reactions that might occur at runtime for a given process. This work is complementary to previous results on termination of processes by capturing strictly more processes, since it captures all the strongly normalizing processes, and by providing precise upper bounds on the number of communications on each channel. For that purpose, it combines interpretation methods, inspired by polynomial interpretations introduced in order to study the complexity of term rewrite systems, with a notion of resource process that mimics reaction keeping information about resource consumption in terms of communication. We also show that presented analysis is general and can be easily adapted to study space properties of processes (for example, upper bounds on the size of the maximal value sent on a given channel during reaction).

Introduction

Motivations. This work belongs to the Implicit Computational Complexity (ICC) research line whose aim is to characterize complexity classes without referring to machines. In the last two decades, contributions have tried to extend the characterizations to several computational paradigms such as function algebra [START_REF] Bellantoni | A new recursion-theoretic characterization of the polytime functions[END_REF][START_REF] Leivant | A foundational delineation of poly-time[END_REF], lambda-calculi [START_REF] Leivant | Lambda calculus characterizations of poly-time[END_REF][START_REF] Gaboardi | A soft type assignment system for λcalculus[END_REF][START_REF] Baillot | Soft lambda-calculus: a language for polynomial time computation[END_REF], light and soft linear logics [START_REF] Girard | Light linear logic[END_REF][START_REF] Gaboardi | A Logical Account of PSPACE[END_REF], term rewrite systems [START_REF] Bonfante | Quasi-interpretations a way to control resources[END_REF] and imperative programs [START_REF] Jones | A flow calculus of mwp-bounds for complexity analysis[END_REF][START_REF] Moyen | Resource control graphs[END_REF], to mention a few. Surprisingly, only a few works have been carried out on resource control and analysis of concurrent models. Such a lack mainly relies on the fact that most of these models do not deal with functions as computational objects. However most of these concurrent models have their own notions of time and space in analogy with sequential models. More specifically for the π-calculus, it has been commonly accepted that the time can be seen as the maximal number of possible communications between processes. Contribution. In this paper, we try to tackle the problem of (first-order) πcalculus time analysis by finding, if possible, an upper bound on the number of possible reactions on each channel. For that purpose, we extend (polynomial)

The financial support of ANR Complice and Inria Associate team Cristal is gratefully acknowledged.

interpretations [START_REF] Manna | On the termination of Markov algorithms[END_REF][START_REF] Lankford | On proving term rewriting systems are noetherian[END_REF], a well-known termination tool for Term Rewrite Systems to a process calculus. The considered process calculus mainly consists in the classical π-calculus where replication is replaced by the ability to call processes recursively through the use of a case construct. Processes in P(N) are considered with respect to a fixed set of names N. The analysis is performed in two steps as illustrated by the following diagram:

P(N) [-] / / R(N) - / / N N∪{ * }
The first step corresponds to the interpretation [-], an assignment mapping each process in P(N) to a resource process in R(N). Resource processes are processes with extra prefixes, recording reactions on each channel, and without process call. Consequently, they are strongly normalizing since they have neither the ability to replicate, nor the ability to recurse. The interpretation enjoys some simulation properties on resource processes guaranteeing that a resource process will have at least as many resources (in terms of reaction) as the initial process it represents. In the second step, we interpret each resource process by a function of the resource algebra N N∪{ * } using the semantics -. Such a function maps each channel in N to a natural number in N, the upper bound on its possible reactions.

* is a special symbol for process calls that takes account of the recursive calls performed by the studied process.

Results. Our main result (Theorem 1) is that, for a given process P , the function [P ] provides upper bounds on both the number of reactions, for each channel, and the number of recursive calls occurring in a reduction of P . In other words, for a given channel x, [P ] (x) will be an upper bound on the number of reactions based on a communication on channel x. Moreover, we show that the presented analysis is complete for strongly normalizing processes, if no restriction is made on resource processes (Theorem 2) and can be extended to study space properties of processes. Another interest of our results lies in the transfer and use of well-known termination techniques for term rewrite systems to π-calculus. Related works. Time properties of processes have been deeply studied in the last decade adapting well-known ICC complexity classes characterizations based on type systems [START_REF] Deng | Ensuring termination by typability[END_REF][START_REF] Sangiorgi | Termination of processes[END_REF][START_REF] Demangeon | Termination in higher-order concurrent calculi[END_REF], linear logics [START_REF] Igarashi | Type reconstruction for linear -calculus with i/o subtyping[END_REF][START_REF] Yoshida | Strong normalisation in the pi-calculus[END_REF][START_REF] Lago | Light logics and higher-order processes[END_REF] and access control [START_REF] Kobayashi | Resource usage analysis for the πcalculus[END_REF]. Contrarily to the present work, most of these studies are global and do not allow the analyzer to infer precise upper bounds on the use of each channel. An important point to stress is that the results presented in this paper have a greater expressivity than all the aforementioned studies, that are mostly tractable in polynomial time. In opposition, our work captures all the strongly normalizing processes. The pros are a greater expressivity, the cons are that our framework needs to be restricted in order to be effective. However we think that it opens a new line of research since decidable fragments are already delineated by considering restricted function spaces as discussed in the last section of the paper.

Another branch of research [START_REF] Nielson | Shape analysis for mobile ambients[END_REF][START_REF] Hansen | Abstract interpretation of mobile ambients[END_REF], has tried to count the number of occurrences of processes during computation sequences using abstract interpretations and relational domains [START_REF] Feret | Occurrence counting analysis for the pi-calculus[END_REF]. In the same direction, some studies [START_REF] Kobayashi | Static analysis of communication for asynchronous concurrent programming languages[END_REF][START_REF] Terauchi | Inferring channel buffer bounds via linear programming[END_REF] have tried to infer buffer upper bounds of concurrent imperative programs communicating via buffered channels. In the same spirit, [START_REF] König | Analysing input/output-capabilities of mobile processes with a generic type system[END_REF] proposes an analysis that infers lower and upper bounds on the number of active channels using a type system combined to a lattice ordered monoid. The problems tackled in these papers are more related to space consumption analysis during process reaction and, consequently, orthogonal to the present study, though clearly related.

In another direction, Hennessy [START_REF] Hennessy | A calculus for costed computations[END_REF] and Pym [START_REF] Collinson | A logical and computational theory of located resource[END_REF] that have developed variants of the π-calculus where channels come equipped with a notion of resource. Reactions may only occur when there is enough resource in the owning channel. These studies provide a dynamic analysis of system behaviors depending on whether it has been fed with enough resources, whereas the work presented in this paper is inherently static by trying to give an approximation of resources needed by a process before reduction.

Outline. The syntax and semantics of processes is introduced in Section 2. Section 3 describes the first step of our static analysis by introducing resource processes, particular processes without recursive calls, and defining interpretations and their properties. Section 4 describes the second step, a semantics that gives a meaning to resource processes on a resource algebra. Some intermediate lemmata show that resources decrease during reactions. We show (Theorem 1) that the resource algebra function corresponding to a process provides upper bounds on the number of its reactions, for each channel, and that the analysis is complete for strongly normalizing processes (Theorem 2). Moreover, some more toy examples (and a counter-example) are developed in order to help the reader to grasp the presented methodology. Section 5 discusses some extension of the presented methodology to space upper bounds. Sections 6 deals with the interpretation inference problem and shows that the presented methodology opens a lot of perspectives in the study of process time and space complexity properties.

Preliminaries

Syntax of processes. The extended concurrent model considered in this paper merely consists in the classical simply typed π-calculus constructs of [START_REF] Milner | Communicating and mobile systems: the π-calculus[END_REF], inaction, input, output, parallel composition, sum and restriction where replication is replaced by the ability to call process definitions and where values are extended to inductive data types. For simplicity, our study will be restricted to integer data type. For that purpose, let V = {l, m, n, . . .} be a set of integer variables. Moreover, let Op be a set of basic operators op of fixed arity over integers. We consider a (possibly infinite) set N = {a, b, c, . . . , x, y, w, . . .} of names and a distinguished element τ for reaction (i.e. N ∩ {τ } = ∅). We also assume a fixed set F = {F, G, . . .} of process symbols of fixed arity. In what follows, let -→ t be a notation for the sequence t 1 , • • • , t n when n is clear from the context. Expressions in E, values in V and processes in P(N) are defined by the grammar of Figure 2. For a given process P , define fn(P ), bn(P ) and n(P ) to be respectively the free names, bound names and names of the process P . Define also fv (P ) to be the free integer variables in P . A closed process is a process such that fv (P ) = ∅. Let V be the set of ground values, i.e. v ∈ V if fv (v) = ∅.

A process call F ( -→ v ) corresponds to the application of the process symbol F .

Each process symbol F comes with exactly one process definition of the shape:

F ( - → X ) = Case - → X of - → v 1 → P 1 , . . . , - → v k → P k
We will assume that the distinct rules in a process definition are non-overlapping. Moreover, we will assume that ∀i, fv

(P i ) ⊆ fv ( - → v i ).
For convenience, the notation F ( -→ v i ) = P i will be used to denote the i-th pattern matching rule. Definitions may be recursive. Consequently, the presented framework is at least as expressive as the π-calculus since the definition F () = F ()|P encodes the replication !P . We will sometimes use the notation µ to denote either the input prefix x(y) or the output prefix xv when there is no need to distinguish prefixes. Moreover, let ν be a notation for either the restriction νx or the empty restriction, depending on the context. Finally, for readability, we will omit inaction, that is we write µ instead of µ.0. Given a process P , D(P ) is the set of process symbols called either in P or (inductively) in the definition of process symbols called in P .

The structural congruence ≡ is defined as the least congruence relation on processes that satisfies:

-0 + P ≡ P , P + Q ≡ Q + P , (P + Q) + R ≡ P + (Q + R), -0 | P ≡ P , P | Q ≡ Q | P , (P | Q) | R ≡ P | (Q | R), -(νx)(νy)P ≡ (νy)(νx)P , (νx)0 ≡ 0, -(νx)(P | Q) ≡ ((νx)P ) | Q, if x / ∈ fn(Q).
For simplicity, we will suppose that all considered processes have already been carefully alpha-converted.

Operational semantics. We do not provide an explicit operational semantics for expressions and we suppose that each operator corresponds to some fixed total function op over ground values. We provide an annotated operational semantics for processes, a slight change of usual operational semantics. It consists in the transition system described in Figure 2. A transition has the shape P α → Q, where α is a transition label that is equal to:

xw if the transition corresponds to an input of the name w with respect to input prefix x(y) (rule (In)), νxw if the transition corresponds to an output of the name w with respect to output prefix xw (rules (Out) and (Open)),

τ (χ), χ ∈ N ∪ { * } if the transition corresponds to a reaction (rules (Com) and (Close)), in this case χ ∈ N, or to a process call (rule (App)), in this case χ = * . Notice that n(τ (x)) = f n(τ (x)) = ∅, meaning that a name in a reaction is just an annotation and not a free name. χ plays the role of label recording either the reacting channel or the application of a process definition, whenever χ = * (In) x(y).P

xw → P {w/y} (Out) xw.P xw → P P α → P bn(α) ∩ fn(Q) = ∅ (Par) P | Q α → P | Q P α → P Q ≡ P P ≡ Q (Var) Q α →Q P α → P x / ∈ n(α) (Res) (νx)P α → (νx)P P xw → P x = w (Open) (νw)P (νw)xw → P P xw → P Q xw → Q (Com) P | Q τ (x) → P | Q P (νw)xw → P Q xw → Q w / ∈ fn(Q) (Close) P | Q τ (x) → (νw)(P | Q ) - → vi σ = - → v F ( - → vi ) = Pi (App) F ( - → v ) τ ( * ) → Piσ P α → P (Sum) P + Q α → P

Fig. 2. Annotated operational semantics

Let D be a notation for N ∪ { * }. Note that the (App) rule of Figure 2 uses a standard notion of substitution σ, a mapping from free names and free variables to values of the same type. Among substitutions, we distinguish the ground substitutions, substitution mapping variables to ground values in V. Let SN τ (χ) be the set of processes P such that each sequence of reduction starting from the closed process P σ has a finite number of transitions labeled by τ (χ), for any substitution σ : f v(P ) → N. For a given total function f : N → N, let SN τ (χ) (f ) be the set of processes P such that for each substitution σ : f v(P ) → N, if ∀n ∈ fv (P ), nσ ≤ k then P σ has at most f (k) transitions labeled by τ (χ). For each f : N → N and each χ ∈ D, the following inclusion holds SN τ (χ) (f ) ⊂ SN τ (χ) . Moreover, we define SN = ∩ χ∈D SN τ (χ) and we write P ∈ SN τ (χ) (f (k)) as an abuse of notation for P ∈ SN τ (χ) (f ). Notice that the definition of SN is standard since process syntax prevents us from building a diverging process with a finite number of reactions on an infinite number of channel names.

Example 1. Consider the process fac(m, a) and the process definition:

fac(n, r) = Case n of 0 → r 1 m + 1 → (νr )(fac(m, r ) | r (x).r x × (m + 1) )
For each substitution σ such that nσ = k, k ∈ N, and rσ = a, a ∈ N, fac(n, r)σ computes k! through k communications on internal channels r , k + 1 recursive calls of the process symbol fac and outputs the result on channel a. Indeed, we have the following sequence of reductions:

fac(n, r)σ = fac(k, a) τ ( * ) → . . . τ ( * ) → k+1 times . . . τ (r ) → . . . τ (r ) → k times a (k -1)! × k Consequently, we have fac(n, r) ∈ SN τ ( * ) (k+1), fac(n, r) ∈ SN τ (r ) (k),fac(n, r) ∈ SN τ (r) (0) and fac(n, r) ∈ SN .

Resource analysis by interpretation

A resource analysis based on interpretation methods in order to control the time complexity of process computations is presented in this section.

Resource processes

Resource processes will be the codomain of the first interpretation. They mainly consist in processes with no process call and with extra input prefixes of the shape τ n χ , with χ ∈ D and n ∈ N, and are defined by the following grammar:

R(N) R, S ::= 0 | τ n χ .R | µ.R | R|R | R + R | (νx)R
Intuitively, a resource process τ n χ .R will be able to perform n transitions labeled by τ (χ). The notions of names, bounded names, free names, and free variables are defined in a standard way. Resource processes structural congruence is similar to process structural congruence but extended by τ 0 χ .R ≡ R. In what follows, a context C[ -→ ] is a resource process with exactly one occurrence of each hole i .

Let C[ -→ R ] be the resource process obtained by filling the holes -→ with -→ R . Resource process operational semantics is defined by the rules of Figure 2 and is extended by the following rule:

1 (T n+1 ) τ n+1 χ .R τ (χ) → τ n χ .R Definition 1.
The partial preorder on resource processes is a simulation de-

fined by R R if ∀S ∈ R(N) s.t. R α → S , ∃S ∈ R(N) s.t. R α → S and S S . 2
Lemma 1. The relation enjoys the following properties:

(1) ∀σ, if R S then Rσ Sσ (Stability by substitution)

(2) ∀C[ - → ], if ∀i, - → R - → S then , C[ - → R ] C[ - → S ] (Stability by context)

Process assignment

An assignment consists in annotations provided by the analyzer on the resources consumed by process symbols and is defined as follows:

Definition 2 (Assignment). Given a process P s.t. |(νr )τ n r |r n! is an assignment. The informal meaning of this assignment is that the process fac(n, r) will react at most n times on internal names r , perform at most n + 1 transitions labeled by τ ( * ) and output at most once the value n! on channel r. Notice that all the internal channels r under a restriction in the initial process are abstracted as a whole. However we still infer upper bounds since n is, by definition, an upper bound on the number of reactions of each internal channel. Notice also that internal names are treated as constant names and, consequently, do not need to appear in the parameters of the assignment. Definition 3 (Process assignment). Given an assignment [-], a process assignment is a map from P(N) to R(N) defined inductively by: Structural congruence and reaction are preserved on resource processes: Proof. By induction on the annotated semantics.

D(P ) = {F 1 , • • • , F m }, an assignment [-] is a total map from D(P ) to V → R(N) assigning to each process definition F i of arity n a total function [F i ] such that for each v 1 , • • • , v n ∈ V, [F i ](v 1 , • • • , v n ) ∈ R(N).
[0] = 0 [(νx)P ] = (νx)[P ] [P + Q] = [P ] + [Q] [F ( - → v )] = [F ]( - → v ) [P | Q] = [P ] | [Q] [
Lemma 2. If P ≡ Q then [P ] ≡ [Q].

Interpretation

Now we introduce the notion of interpretation, the cornerstone of the presented analysis. Interpretations enforce the semantics of assignments to satisfy inequalities that allow the analyzer to infer upper bounds on reactions.

Definition 4 (Interpretation). Given a process P , an assignment [-] is an interpretation of P if for each process definition F ∈ D(P ) of the shape:

F ( - → X ) = Case - → X of - → v 1 → P 1 , . . . , - → v k → P k
for each ground substitution σ the following holds:

∀i ∈ {1, . . . , k}, [F ( - → v i )σ] τ 1 * .[P i σ]
In such a case, we say that P has interpretation [-].

The informal meaning of an interpretation is that the process call has more resources than its evaluation since is the simulation preorder. The prefix τ 1 * is needed since one τ ( * ) transition has already been done when process call the computation is under consideration.

Example 4. Consider the process fac(n, r) and the assignment [-] of Example 3: We start to state an obvious lemma showing that interpretations are preserved under τ reductions: Proof. This result is straightforward as a consequence of Definition 4 though both processes are not in the same domains. Resource algebra will be used to compute the resource upper bounds of the presented analysis. The resource algebra is the set of total functions N D mapping each annotation χ ∈ D to a natural number k ∈ N.

[fac](0, r) = τ 0 r | r 0! | τ 1 * ≡ r 1 | τ 1 * τ 1 * .r 1 = τ 1 * .[r 1 ] Since τ 0 r .0 ≡ 0 [fac](m + 1, r) = (νr )τ m+1 r | τ m+2 * | r (m + 1)!
Let k A , k ∈ N, A ⊆ D be a notation for the characteristic function of A defined by:

k A (χ) = k, ∀χ ∈ A 0, ∀χ ∈ D -A
In what follows, let δ 0 be a notation for the function defined by ∀χ ∈ D, δ 0 (χ) = 0. The commutative operator ⊗ is defined by:

∀χ ∈ D, (δ ⊗ δ )(χ) = δ(χ) + δ (χ)
where (N, +, 0) is the usual commutative monoid over natural numbers. Note that δ 0 is the neutral element for ⊗ since δ⊗δ 0 = δ. Moreover, we have k A ⊗k A = (k + k ) A . The commutative operator ⊕ is defined in the same way by:

∀χ ∈ D, (δ ⊕ δ )(χ) = max(δ(χ), δ (χ))
where (N, max, 0) is the usual commutative monoid over natural numbers.

Lemma 7. (N D , ⊗, ⊕) is a max-plus algebra.

The resource algebra underlies a poset structure (N D , ), where is defined by δ δ iff δ ⊕ δ = δ.

Resource process semantics

We introduce a semantics of resource processes -, a partial map from R(N) to N D . For that purpose, we define the reachability relation between resource processes. Given a resource process R and a name χ ∈ D, define the set of reachable

processes Reach χ (R) from R through χ by Reach χ (R) = {S | R τ (χ)
→ S}. Finally, define the set of reachable processes from R by Reach(R) = ∪ χ∈D Reach χ (R).

Definition 5 (Resource Process semantics). The resource process semantics -is defined by:

R = ⊕{1 {χ} ⊗ S | ∀χ ∈ D, ∀S ∈ Reach χ (R)} if Reach(R) = ∅ R = δ 0 otherwise Lemma 8. If R S then R S .
Proof. There are two cases to consider:

-If Reach(S) = ∅ then by definition of the resource process semantics -:

S = ⊕{1 {χ} ⊗ S | ∀χ ∈ D, ∀S ∈ Reach χ (S)}
However for each S ∈ Reach χ (S), there exists R ∈ Reach χ (R) such that R S , by definition of . Suppose by induction hypothesis (I.H.) that R S . We obtain that:

S = ⊕{1 {χ} ⊗ S | ∀S s.t. S τ (χ) → S } By definition of - ⊕{1 {χ} ⊗ R | ∀R s.t. R τ (χ) → R }) (I.H.) and monotonicity of ⊕, ⊗ = R Since R ∈ Reach χ (R) -If Reach(S) = ∅ then S = δ 0 R .

Bounded reactions and completeness of the analysis

Theorem 1. Given a process P having interpretation [-], we have: Proof. Soundness: By Theorem 1, P ∈ SN τ (χ) ( [P ] (χ)), ∀χ ∈ D. Consequently, P ∈ ∩ χ∈D SN τ (χ) ( [P ] (χ)) ⊂ SN . Completeness: If P ∈ SN then the traces of P are finite. From these traces, we can rebuild a resource process simulating P . We do exactly the same for all the P i appearing in the right hand side of a definition. The simulation inequalities are clearly satisfied since for each trace t i of P i , τ ( * ).t i is a trace of P .

∀χ P ∈ SN τ (χ) ( [P ] (χ)). Proof. By Lemma 9, if P τ (χ) → P , χ ∈ D, then [P ] 1 χ ⊗ [P ] . Consequently, [P ] (χ) ≥ (1 χ ⊗ [P ] )(χ) = 1 + [P ] (χ). Moreover, if P τ (χ ) → P , χ = χ then [P ] (χ) ≥ (1 χ ⊗ [P ] )(χ) = [P ] (χ).

Examples

In this section we illustrate some toy examples and one counter-example to help the reader to understand the interpretation based method.

5.

Consider the process fac(n, r) of Example 1 wrt to the closed substitution σ such that nσ = k and rσ = a, we have:

[fac(n, r)σ] = [fac(k, a)] = (νr )τ k r | τ k+1 * | a k! Consequently, [fac(k, a)] = k {r } ⊗ (k + 1) { * } and: fac(a, k) ∈ SN τ (r ) ( [fac(k, a)] (r )) = SN τ (r ) (k) By Theorem 1 fac(a, k) ∈ SN τ ( * ) ( [fac(k, a)] ( * )) = SN τ ( * ) (k + 1) fac(a, k) ∈ SN τ (r) ( [fac(k, a)] (r)) = SN τ (r) (0)
which means that the process fac(k, a) may react at most k times on the internal channels r , may call processes at most k + 1 times and will never react on a (note that r occurs freely here since internal channels are abstracted as a whole).

Notice that k can be abstracted as the identity function mapping each integer k to itself. Clearly fac(a, k) ∈ SN , by Theorem 2.

Example 6. Consider the process F (a, k) with respect to the process definition:

F (c, n) = Case c, n of c, 0 → c 0 c, m + 1 → c m + 1 | F (c, m) It admits the following interpretation [F ](c, n) = τ n+1 * | c 0 | . . . | c n since: [F (c, 0)] = τ 1 * | c 0 ≥ τ 1 * .c 0 = τ 1 * .[c 0 ] [F (c, m + 1)] = τ m+2 * | c 0 | . . . | c m + 1 τ 1 * .(c m + 1 | τ m+1 * | c 0 | . . . | c m ) τ 1 * .[c m + 1 | F (c, m)] Moreover, [F (a, k)] = τ k+1 * | a 0 | . . . | a k = (k + 1) { * } . Consequently, F (a, k) ∈ SN τ ( * ) (k + 1) and F (a, k) ∈ SN τ (a) (0).
Example 7. Consider the process F (a, k) with respect to the process definition:

F (c, n) = Case c, n of c, 0 → c 0 c, m + 1 → F (c, m) + F (c, m) It admits the following interpretation [F ](c, n) = τ n+1 * | c 0 since: [F (c, 0)] = τ 1 * | c 0 τ 1 * .c 0 = τ 1 * .[c 0 ] [F (c, m + 1)] = τ m+2 * | c 0 τ 1 * .((τ m+1 * | c 0 ) + (τ m+1 * | c 0 )) = τ 1 * .[F (c, m) + F (c, m)] Moreover, [F (a, k)] = τ k+1 * | a 0 = (k + 1) { * } and F (a, k) ∈ SN τ ( * ) (k + 1) and F (a, k) ∈ SN τ (a) (0).
Example 8. Consider the process F (a, k) with respect to the process definition:

F (c, n) = Case c, n of c, 0 → c 0 c, m + 1 → F (c, m) | F (c, m) It admits the following interpretation [F ](c, n) = τ 2 2n * | c 0 | . . . | c 0 2 n+1 times since: [F (c, 0)] = τ 1 * | c 0 | c 0 τ 1 * .c 0 = τ 1 * .[c 0 ] [F (c, m + 1)] = τ 2 2m+4 * | c 0 | . . . | c 0 2 m+2 times

Extension to space upper bounds

In this section, we show that playing on the parameters of the analysis (language, simulation, semantics,. . . ), we may infer several other challenging results about resource consumption of processes. In particular, interpretations also allow us to infer upper bounds about the maximal size of the values sent on each channel during a communication. For that purpose, we put an extra annotation, an upper bound on the integer value sent, on the rule (Com) of Figure 2 as follows:

P xw → P Q xw → Q (Com) P | Q τ (x(#w)) → P | Q with #w = 0, if w ∈ D w, if w ∈ N
The rule (Close) can be annotated in a similar manner. Moreover, these annotation are extended to resource processes by τ n+1 χ(k) .R τ (χ(k))

→ τ n χ(k) .R and to the preorder in a standard way. The aim of these new annotations is to keep record of the integer value sent on a given channel or 0 by default (if a name has been sent or if a process definition has been applied).

Define Reach χ(k) (R) = {S | R τ (χ(k))
→ S}. We are now ready to introduce a new semantics -, a partial map from R(N) to N D , for space analysis:

R = ⊕{k {χ} ⊕ S | ∀χ ∈ D, ∀k ∈ N, ∀S ∈ Reach χ(k) (R)} if Reach(R) = ∅ R = δ 0 otherwise
Now we obtain an upper bound on each integer value sent during reaction: Remark 1. Note that the preorder might be seen as too restrictive for space control. Indeed it requires the simulating resource process to output exactly the same integers as the simulated process. Since we are only interested in an upper bound, can be replaced by a finer relation defined as follows: Given two labels α and β, β α holds if either β = α or β = νxn, α = νxm, n, m ∈ N, x ∈ N and n ≥ m. The partial preorder on resource processes is a simulation 6 Some words on inference.

defined by R R if ∀S ∈ R(N) s.t. R α → S , ∃S ∈ R(N) s.t. R β → S,
An important issue related to the presented analysis is interpretation inference which consists in finding an assignment that is an interpretation of a given process P . Interpretation inference is clearly undecidable in general since finding an interpretation is as difficult as the halting problem (see Theorem 2). The undecidability of such a problem lies in the fact that one needs to guess functions f from N to N as annotations of the resource processes (for example, τ f (n) *

) and to check the simulation preorder for each process definition. Note that the difficulty of this latter check lies in the parametric definition and not in the simulation itself since resource processes are strongly normalizing (they have neither the ability to recurse, nor the ability to replicate). This result is not surprising if we compare our notion of interpretation to the notion of polynomial interpretation for term rewrite systems, also known to be an undecidable tool. As for polynomial interpretations, the inference problem will become decidable if we restrict the class of functions under consideration (max-plus, bounded polynomials, ...).

For a given process P such that D(P ) = {F 1 , • • • , F n }, the inferred assignments [F i ]( -→ n , -→ a ) have the shape:

ν -→ r (τ

f i r 1 ( - → n ) r1 | . . . |τ f i r l ( - → n ) r l )|τ f i a 1 ( - → n ) a1 | . . . |τ f i a k ( - → n ) a k |τ f i * ( - → n ) * |f i a1 (a 1 , - → n )| . . . |f i a k (a k , - → n )
where -→ r = r 1 , • • • , r l corresponds to the names of P under a restriction, f v(P ) = { -→ n } and { -→ a } = {a 1 , • • • , a k } = f n(P ). Consequently, the interpretation inference consists in finding all the functions f i χ : N k → N and checking inequalities. As demonstrated for polynomial interpretation, this problem becomes decidable for small classes of functions (it is NP-difficult for some max-plus algebra [START_REF] Amadio | Synthesis of max-plus quasi-interpretations[END_REF]).

Conclusion.

The work presented in this paper is the most intuitive and simplest version in the set of all possible applications. Indeed we claim that playing on the parameters of the analysis (language, simulation, semantics,. . . ), we may infer several other challenging results about resource consumption of processes:

the analysis may be extended in a simple way to other inductive data structures such as lists, trees... the framework can be extended in order to capture processes that do not terminate but still have bounded reactions on some channels. -Finally, we can capture complexity classes, such as FPtime, in a classical way by restricting the considered processes to processes computing functions.

EFig. 1 .

 1 Fig. 1. Syntax of processes

Example 2 .

 2 Consider the process fac(k, a) of Example 1: We have D(fac(k, a)) = {fac}. Consequently, the function [-] such that [fac](n, r) = τ n+1 *

Example 3 .

 3 µ.P ] = µ.[P ] Consider the subprocess (νr )(fac(m, r )|r (x).r x × (m + 1) ) of Example 1 together with the assignment [fac](n, r) = (νr )τ n r |τ n+1 * |r n! : [(νr )(fac(m, r ) | r (x).r x × (m + 1) )] = (νr )[fac(m, r ) | r (x).r x × (m + 1) ] = (νr )([fac](m, r ) | [r (x).r x × (m + 1) ]) = (νr )(((νr )τ m r | τ m+1 * | r m! ) | (r (x).r x × (m + 1) )

Lemma 3 .

 3 Given a process P and an assignment [-], ∀α ∈ {νxw, xw, τ (x)}, if P α → P then [P ] α → [P ].

τ 1 *

 1 .[(νr )(fac(m, r ) | r (x).r x × (m + 1) )] = τ 1 * .(νr )(((νr )τ m r | τ m+1 * | r m! ) | (r (x).r x × (m + 1) ) By Example 3 Note that the above inequality for simulation holds since the traces of τ 1 * .(νr )(((νr )τ m r | τ m+1 * | r m! ) | (r (x).r x × (m + 1) ) are strictly included in the traces of [fac](m + 1, r). Consequently, [-] is an interpretation of the process fac(n, r).

Lemma 4 .Lemma 5 .

 45 Given a closed process P having interpretation [-], if P τ ( * ) → P then [-] is also an interpretation of P .Proof. There are no new process definitions introduced in P . Consequently, the inequalities of Definition 4 remain valid.Another interesting result is that [P ] is an over approximation of P : Given a closed process P having interpretation [-], [P ] strongly simulates P , i.e. [P ] P .

Lemma 6 .

 6 Given a closed process P having interpretation [-], if P τ ( * ) → P then [P ] τ 1 * .[P ]. Proof. By Lemma 5 and by induction on the τ ( * ) → transitions. 4 Resource algebra for bounded reaction 4.1 Resource algebra.

Lemma 9 (-

 9 Resource consumption). Given a closed process P having interpretation [-], if P τ (χ) → P , χ ∈ D, then [P ] 1 χ ⊗ [P ] . Proof. There are two cases to consider: If χ ∈ N then, by Lemma 3, we have [P ] τ (χ) → [P ]. Consequently, [P ] ∈ Reach χ ([P ]) = ∅. By definition of -, we obtain that [P ] 1 {χ} ⊗ [P ] . -If χ = * then, by Lemma 6, [P ] τ 1 * .[P ]. Consequently, by Lemma 8, we obtain that [P ] τ 1 * .[P ] 1 { * } ⊗ [P ] , by definition of -.

  Consequently, there are at most [P ] (χ) reactions labeled by χ. Theorem 2. A process P has interpretation [-] if and only if P ∈ SN .

τ 1 *Example 9 .

 19 .((τ 2 2m+2 * | c 0 | . . . | c 0 2 m+1 times ) | (τ 2 2m+2 * | c 0 | . . . | c 0 2 m+1 times)) = τ 1 * .[F (c, m) | F (c, m)] Moreover, [F (a, k)] = (2 2k ) { * } and F (a, k) ∈ SN τ ( * ) (2 2k) and F (a, k) ∈ SN τ (a) (0). As a counter-example consider the process definition:bip() = bip() | P for some process P . Clearly there is no assignment[-] such that [bip()] τ 1 * .[bip() | P ] since [bip()] τ 1 * .[bip()]does not hold, for any[-], which is reasonable since the process bip() does not terminate (See Theorem 2).Example 10. Consider the process F (a, b, i, j) wrt the process definition:F (a, b, n, m) = Case a, b, n, m of a, b, 0, 0 → 0 a, b, 0, m + 1 → F (a, b, m + 1, m) a, b, n + 1, m → (a(x).bx | av) + F (a, b, n, m) It admits the following interpretation [F ](a, b, n, m) = τ n+(m+1) 2 * | (a(x).bx | av) since: [F (a, b, 0, 0)] = τ 1 * + (a(x).bx | av) ≥ τ 1 * .0 = τ 1 * .[0] [F (a, b, 0, m + 1)] = τ (m+2) 2 * | (a(x).bx | av) τ 1 * .(τ m+1+(m+1) 2 * | (a(x).bx | av)) = τ 1 * .[F (a, b, m + 1, m)] [F (a, b, n + 1, m)] = τ n+1+(m+1) 2 * | (a(x).bx | av) τ 1 * .((τ n+(m+1) 2 * | (a(x).bx | av)) + (a(x).bx | av) = τ 1 * .[F (a, b, n, m) + a(x).bx | av]Moreover, [F (a, b, i, j)] = (i + (j + 1) 2 ) { * } + 1 {a} . Consequently, F (a, b, i, j) ∈ SN τ ( * ) (k + (k + 1) 2 ) and F (a, b, i, j) ∈ SN τ (a) (1).

Theorem 3 (

 3 Space upper bound). Given a closed process P 0 of interpretation [-], for each sequence of reduction P 0 τ (χ1(n1)) → P 1 . . .

τExample 11 .

 11 (χ k (n k ))→P k , we have[P 0 ] (χ i ) ≥ n i .Proof. There are two cases to consider:-If χ i+1 ∈ N then, by Lemma 3 3 , we have [P i ] τ (χi+1(ni+1)) → [P i+1 ] and [P i+1 ] ∈ Reach χ(ni+1) ([P i ]) = ∅. By definition of -, we obtain that [P i ] n i+1 {χi+1} ⊕ [P i+1 ] and, consequently, [P 0 ] (χ i+1 ) ≥ [P i ] (χ i+1 ) ≥ n i+1, by transitivity and by definition of ⊕. -If χ i+1 = * then trivially n i+1 = 0 (by definition of the # operator) and the result holds. For the process fac of Example 5, the assignment: [fac](k, a) = (νr )τ 2 r (1) | τ 1 r (2) | . . . | τ 1 r ((k-1)!) | τ k+1 * (0) | a k! is an interpretation and, consequently, we have [fac(k, a)] = (k -1)! {r } which means that (k -1)! is an upper bound on the values sent on the internal names r whereas 0 is an upper bound on the values sent on all the other names (indeed, the value on a has not been sent yet).

  S S and β α. We claim that Theorem 3 holds if we substitute for in the definition of interpretations. Turning back to Example 11, the interpretation of fac can be set to [fac](k, a) = (νr )τ k r ((k-1)!) | τ k+1 * (0) | a k! .

Notice that rule (App) of Figure

is meaningless for resource processes since they do not involve process calls.[START_REF] Baillot | Soft lambda-calculus: a language for polynomial time computation[END_REF] we recall that α ∈ {xv, x(y), τ (χ)} as in the annotated operational semantics.

This Lemma trivially remains valid for the new annotations.


James W Dufty
email: dufty@phys.ufl.edu

Ilya V Pogorelov

Bernard Talin

Annette Calisti

Nonlinear response of electron dynamics to a positive ion

Keywords: numbers: 52.65.Yy, 52.25.Vy, 05.10.-a

Electric field dynamics at a positive ion imbedded in an electron gas is considered using a semiclassical description. The dependence of the field autocorrelation function on charge number is studied for strong ion-electron coupling via MD simulation. The qualitative features for larger charge numbers are a decreasing correlation time followed by an increasing anticorrelation. Stopping power and related transport coefficients determined by the time integral of this correlation function result from the competing effects of increasing initial correlations and decreasing dynamical correlations. An interpretation of the MD results is obtained from an effective single particle model showing good agreement with the simulation results.

Introduction

The total electric field at a particle in a plasma determines the dominant radiative and transport properties of that particle. The properties of fields due to positive ions at a positive particle have been studied in some detail for both the static distribution of fields [START_REF] Dufty | Strongly Coupled Plasmas[END_REF] and the dynamics of the electric field autocorrelation function [START_REF] Boercker | [END_REF]3]. The latter poses a real challenge since finite charge on the site at which the field is considered precludes the use of standard linear response methods. The corresponding study of fields at a positive ion due to electrons has been considered more recently for the simplest case of a single ion of charge number Z in an semiclassical electron gas. The static properties (electron charge density, electron microfield distribution) have been discussed in some detail elsewhere [4]. Here, attention is focused on the dynamics via the electric field autocorrelation function. The case of opposite sign electron fields at a positive ion is qualitatively different from same sign ion fields, since in the former case electrons are attracted to the ion leading to strong electron-ion coupling for the enhanced close configurations. It is difficult a priori to predict the qualitative features of the correlation function due to this inherent strong coupling. Consequently, the analysis here has been based on MD simulation of the correlation function followed by an attempt to model and interpret the observed results. The simulations represent classical mechanics for Coulomb interactions with the ion-electron potential modified at short distances to represent quantum diffraction effects. The details have been discussed elsewhere [4] and will not be repeated here. There are only three dimensionless parameters: the charge number of the ion, Z, the electron-electron coupling constant Γ, and the de Broglie wavelength relative to the interelectron distance, δ. The electron-ion coupling is measured by the maximum value of the magnitude of the regularized ion-electron potential at the origin, σ = ZΓ/δ. In this brief report results are reported for Γ = 0.1 and σ =0 .25Z, with Z =8 , 20, 30, and 40. The corresponding density and temperature are n =2 .5 × 10 22 cm -3 and T =7.9 × 10 5 K.

The primary observations from the simulations of the field autocorrelation function for increasing charge number are: 1) an increase in the initial value, 2) a decrease in the correlation time, and 3) an increasing anticorrelation at longer times. The stopping power for the ion by the electron gas is proportional to the time integral of the field autocorrelation function in the limit of large ion mass [5]. This same integral determines the self-diffusion and friction coefficients in this same limit [START_REF] Dufty | Physics of Strongly Coupled Plasmas[END_REF]. The nonlinear dependence of these properties on Z is therefore the result of competition between the increase of the integral due to 1) and the decrease due to 2) and 3). The results from simulation show that the latter two dynamical effects dominate the former static effect. To interpret this, a simple model for the field correlation function is proposed such that the initial correlations are given exactly, but the dynamics is determined approximately from a single electron-ion trajectory. The model reproduces well the MD simulation results and suggests an interpretation of 2) and 3).

MD simulation of field dynamics

The system considered consists of N e electrons with charge -e, an infinitely massive positive ion with charge Ze placed at the origin, and a rigid uniform positive background for overall charge neutrality. The regularized electron-ion potential is chosen to be V (r)=-Ze 2 1 -e -r/δ /r where δ = 2πh 2 /m e k B T 1/2 is the electron thermal de Broglie wavelength. For values of r >> δ the potential becomes Coulomb, while for r << δ the Coulomb singularity is removed and V (r) →-Ze 2 /δ. This is the simplest phenomenological form representing the short range effects of the uncertainty principle [START_REF] Minoo | [END_REF]. Dimensionless variables are based on scaling coordinates with the average electron-electron distance, r 0 , defined in terms of the electron density n e by 4πn e r 3 0 /3 = 1, and scaling time with the inverse electron plasma frequency. The electron electric field at the ion is obtained from the total regularized potential

E = -∇ 0 V ({r i0 })= N i=1 e (r i0 ) (1)
where r i0 = r ir 0 is the position of the i th electron relative to the ion, and

V ({r i0 })= N i=1 V (r i0 ), e (r i0 )=e r i0 r 2 i0 (1 -1+ r i0 δ e -ri0/δ ) (2)
The dimensionless field autocorrelation function is defined by

C(t)= r 4 0 e 2 < E (t) •E >. (3)
The brackets denote an average over the classical Gibbs ensemble for the composite electron-ion system at equilibrium. The results for C(t) from MD simulation are shown in Figure 1 for Z =8, 20, 30, and 40. The initial value increases approximately as a third order polynomial in Z [4]. The correlation time t c is defined to be the time at which the correlation function first goes to zero, C(t c ) = 0, and is seen to decrease as Z increases. Finally, in all cases there is anticorrelation (C(t) < 0) for t > t c . The physical basis for the increase in the initial value is easy to understand. As Z increases, the electron density near the ion increases and the magnitude of the field increases for these more probable closer configurations. An explanation for the correlation time and anticorrelation is more difficult, and is the objective of the following sections. First, some consequences of this behavior are illustrated.

Stopping power, friction, and self-diffusion

The case of an infinitely massive ion considered here leads to exact relationships between transport coefficients characterizing three physically different phenomena: 1) the low velocity stopping power S for a particle injected in the electron gas, 2) the friction coefficient ξ for the resistence to a particle being pulled through the gas, and 3) the self-diffusion coefficient D of a particle at equilibrium with the gas. The exact relationship is [START_REF] Dufty | Physics of Strongly Coupled Plasmas[END_REF]

m 0 ξ =(βD) -1 = S(v)/v = βZ 2 r -4 0 ∞ 0 dtC(t) (4)
This Green-Kubo representation allows determination of these transport properties from an equilibrium MD simulation. Previous simulations of stopping power have studied the nonequilibrium state of the injected particle, measuring directly the energy degradation [8]. As discussed below, (4) provides the basis for additional interpretation of the results.

Figure 2 shows the dimensionless stopping power obtained from the results of Figure 1 as a function of Z. Also shown is the Born approximation ∝ Z 2 , valid for small Z. Previous simulations [8] and some experiments [9] suggest a crossover at larger Z to a weaker growth ∝ Z 2 . The data in Figure 2 has been fit to a such a crossover function showing consistency with these earlier results. This behavior is somewhat puzzling in light of the strong growth of the initial value C(0) ≈ Z 3 at large Z. Making this explicit, the stopping power can be expressed as

S(v)/v ∝ Z 5 ∞ 0 dtf (t),f (t)=C(t)/C(0) (5)
Evidently, the dynamical effects of the normalized correlation function f (t) decrease the stopping power as ∼ Z -3.5 for large Z. A possible explanation for this is given in the following section.

Single particle dynamics

Consider again the initial covariance C(0) for which three representations can be given

C(0) = 3 4π dre (r) • g ie (r)e (r)+ 3 4π dr g ie (r, r )e (r ) = 3 4πZΓ drg ie (r)∇•e (r) = 3 4π drg ie (r)e mf (r) •e (r) (6)
The first equality expresses the covariance in terms of the one and two electron correlations with the ion, g ie (r) and g ie (r, r ) respectively. The second equality exploits the relationship for the field to the Gibbs factor βU ({r i0 })=ZΓV ({r i0 }) and an integration by parts. This second representation requires only the one electron correlation function. The third representation is obtained from the second by an integration by parts to identify the mean force field e mf (r)=∇ ln g ie (r). The third equality of ( 6) is similar to the first with apparent neglect of the two electron-ion correlations. However, these latter contributions are incorporated exactly in the mean force field e mf (r). This suggests a corresponding model for finite times

C(t) → 3 4π dvdrφ(v)g ie (r)e mf (r) •e (r(t)) (7)
where φ(v) is the normalized Maxwellian and r(t) is a single electron trajectory in the presence of the ion, generated by the potential associated with g ie (r) for stationarity. Further details and a justification based on the Vlasov equation will be given elsewhere.

Clearly, the initial covariance is given exactly by this approximation. For practical purposes g ie (r) and the associated field and potential are represented here by the nonlinear Debye-Huckel approximation with effective charge number and screening length adjusted to fit the MD data. Figure 3 shows a comparison of ( 7) with the MD results of Fig. 1 for Z = 8 and Z = 30. The agreement is very good, indicating that the dominant Z dependence is captured by the initial correlations and the single particle dynamics.

Discussion

The good agreement of the simple model in the previous section suggests that the decrease in correlation time and build up of anticorrelation can be understood in terms of one electron dynamics. As Z increases the probability of close electron ion configurations increase. The electron is subjected to greater acceleration toward the ion and the time to reverse its sign decreases. This is the effect of decreasing correlation time. Once the field has reversed sign there is anticorrelation. Since the closer configurations imply larger field values the magnitude of this anticorrelation also increases with increasing Z. It remains to quantify this picture but the single electron dynamics appear to provide qualitative confirmation. A more complete discussion will be provided elsewhere.

Figure 1 .

 1 Figure 1. Field autocorrelation function for Z =8 , 20, 30, 40 at Γ = 0.1 and δ =0 .4.

Figure 2 .

 2 Figure 2. Stopping power S(v)/v for Z =8, 20, 30, 40 at Γ = 0.1 and δ =0.4.

Figure 3 .

 3 Figure 3. Comparison of C(t) from MD and from Eq.7 for Z = 8 and 30 at Γ = 0.1 and δ =0 .4.

Acknowledgments

Support for this research has been provided by the U.S. Department of Energy Grant No. DE-FG03-98DP00218. J. Dufty is grateful for the support and hospitality of the University of Provence.