T Crolard

E Polonowski

P Valarcher

Extending the Loop Language with Higher-Order Procedural Variables

Keywords: int, unit, τ = [ ], C[ ] t

We extend Meyer and Ritchie's Loop language with higher-order procedures and procedural variables and we show that the resulting programming language (called Loop ω ) is a natural imperative counterpart of Gödel System T. The argument is two-fold:

1. we define a translation of the Loop ω language into System T and we prove that this translation actually provides a lock-step simulation, 2. using a converse translation, we show that Loop ω is expressive enough to encode any term of System T.

Moreover, we define the "iteration rank" of a Loop ω program, which corresponds to the classical notion of "recursion rank" in System T, and we show that both translations preserve ranks. Two applications of these results in the area of implicit complexity are described.

(types) τ

Introduction

Primitive recursive functionals of finite type are representable as terms of the simply typed λ-calculus equipped with a type of natural numbers and primitive recursion at all types. This calculus (called System T) was first introduced by Gödel in its proof-theoretic study of Peano arithmetic (see its Dialectica paper on the consistency of arithmetic [Gödel, 1958], reproduced with English translation in [Gödel, 1990]).

Moreover, System T is well suited to give a formal semantics to constructs found in (higher-order) programming languages [START_REF] Girard | Proofs and Types[END_REF].

The Loop language [START_REF] Meyer | The complexity of loop programs[END_REF]] is a core imperative language in which programs consist only of assignments, sequences, and bounded loops. Meyer and Ritchie's proved in particular that Loop programs compute exactly the class of primitive recursive functions. The Loop language has since been widely studied in the literature (see for instance the textbooks [START_REF] Davis | Computability, Complexity and Languages[END_REF]] and [Calude, 1988]).

In this paper, we introduce a statically typed extension of the Loop language (called Loop ω ) with higher-order procedures and procedural variables and we argue that this programming language is a natural imperative counterpart of Gödel System T. The argument is two-fold:

1. we define a translation of the Loop ω language into System T and we prove that this translation actually provides a lock-step simulation, 2. using a converse translation, we show that Loop ω is expressive enough to encode any term of System T.

The first result is the main contribution of this paper: we prove that Loop ω is not only extensionally equivalent to System T, but also intensionally. In order to develop this point, we need to give some details about the formal semantics of Loop ω . The overall design of the language follows mostly the principles advocated in [Schmidt, 1994]. The operational semantics of Loop ω is presented first as a natural semantics (also called "bigstep" semantics) in the style of [Kahn, 1987]. Then a transition semantics (also called "small-step" semantics [Plotkin, 1981]) tailored of the lock-step simulation and which refines the natural semantics is defined. The simulation theorem states that each evaluation step of a Loop ω program (according to the transition semantics) is mapped to one reduction step of the transformed program in System T (using a call-by-value strategy). As a corollary of this theorem, we obtain that all Loop ω programs are always terminating.

Note that Loop ω is a genuine imperative language with first-class procedures (true closures) and mutable procedural variables (aka function pointers). For instance, any Loop ω can easily be written using C# syntax (where anonymous first-class procedures are called delegates [ISO, 2003]) and then compiled with a C# compiler. However, it is a "pure" imperative language in the following sense: its type system forbids side-effects, parameterinduced aliasing (which are controversial features known to complicate the semantics). Moreover the type system forbids the well-known back-patching technique which exploits procedural variables to define arbitrary recursive procedures [Landin, 1964] (and Loop ω is thus a "total" programming language as advocated in [Turner, 2004]). As a consequence of these choices, both semantics presented in this paper are simple but rather unusual for imperative languages: they are both location-free semantics (see [Donahue, 1977], [Plotkin, 1981] and [START_REF] Felleisen | A calculus for assignments in higher-order languages[END_REF]) and they rely crucially on the distinction between mutable and read-only (immutable) variables.

The second result is obtained by defining a converse translation (from System T into Loop ω ) and proving that the composition the two translations yields the identity in System T (up to βπ-equivalence). Since both translations are syntax directed (compositional) and type-preserving, we can be even more specific about the correspondence between a functional program and its imperative counterpart. Recall that a major result concerning System T from [Kreisel, 1951] states that functions on the natural numbers that are definable in this system correspond exactly to functions that are provably total in first-order Peano arithmetic (see also the survey [START_REF] Avigad | Gödel's functional ("dialectica") interpretation[END_REF] or the textbook [Schütte, 1967]). More precisely, that there is a syntactic hierarchy of fragments T n of System T such that the class of functions representable in T n is identical to the class of functions provably recursive in the fragment of Peano arithmetic where induction is restricted to Σ n+1 formulas. In particular, T 0 corresponds to the class of primitive recursive functions.

We define thus a similar hierarchy of fragments Loop n of Loop ω and we show that both translations relate programs of Loop n and terms of T n . As a corollary, we obtain that the functions representable in a language with higher-order procedures but without procedural variables (which is a sub-language of Loop 0 ) are primitive recursive. This corollary generalizes thus previous results presented in [START_REF] Crolard | On the Expressive Power of the Loop Language[END_REF] where Meyer and Ritchie's Loop language was translated into T 0 . On the other hand, the Ackermann function which is known not to be primitive recursive is representable in T 1 and thus also in Loop 1 . As far as we know, Loop ω is the first total imperative language allowing to program the Ackermann function.

Applications. A first application of these results is extensional: we derive a new characterization of the class of Csillag-Kalmar elementary functions (the class E 3 in Grzegorczyk hierarchy). In [START_REF] Beckmann | Characterizing the elementary recursive functions by a fragment of Gödel's T[END_REF], such a characterization is based on a syntactic restriction on terms of a variant of Gödel System T. As a corollary of various properties of our two translations we provide an imperative counterpart of this restriction. In particular, we obtain that any Loop ω program in which any bound of loop is a readonly input variable is elementary.

A second application is intensional and is related to the so-called minimum problem. In [START_REF] Colson | System T, call-by-value and the minimum problem[END_REF]], the authors proved that in call-by-value System T, any algorithm which computes a non-trivial binary function (where trivial means constant or projection plus constant), has a time-complexity which is at least linear in one of the inputs. As a consequence of this property, there is no term that computes the minimum of two natural numbers n and m in time O(min(n,m)). As a corollary of the lock-step simulation we obtain a similar negative result for Loop ω programs.

Related works.

There has been a lot of work on the semantics of Algol (major contributions are collected in [O'Hearn and Tennent, 1997]) and this work has influenced the design of most modern programming languages. For instance, the Loop ω language is very close in spirit to the language partially described in [Reynolds, 1978] whose purpose was in particular to show that it is possible to avoid aliasing while retaining Algol-like higherorder procedures. More generally, our work can also be seen as providing a denotational semantics for an imperative language using a λ-calculus and thus follows the Scott-Strachey tradition [Stoy, 1977].

The idea of translating an imperative program into a functional one actually goes back to [McCarthy, 1960]. However, our translation is somewhat closer to the state monad [Moggi, 1991, Wadler, 1990] used to encode a mutable state (or references) in a pure functional language. Although this encoding is usually global and thus changes the type of all terms, a local encoding can be obtained if an effect system [START_REF] Gifford | Integrating functional and imperative programming[END_REF] is used for the source language (instead of a conventional type system). A simulation based on such an encoding is described in [Wadler, 1998].

Similarly, in [START_REF] Filliâtre | Verification of non-functional programs using interpretations in type theory[END_REF], the author defines a monadic translation of simply-typed functional programs with references (annotated with Floyd-Hoare assertions) into a type theory. Their translation provides the core of the proof technique developed afterward for imperative programs [START_REF] Filliâtre | Multi-prover verification of C programs[END_REF]. Although similar to the one described in this paper, their translation is only considered in the context of program verification (no simulation is defined).

Finally, compiling one programming language into another in order to derive complexity properties is a common approach. The reader is referred for instance to [Jones, 1997] for various applications of this technique.

Plan of the paper. In Section 2, we present our variant of Gödel System T. In Section 3, we describe the Loop ω language (syntax, type system and semantics). In Section 4, we show how to translate Loop ω programs into functional programs and we prove the simulation theorem. In Section 5, we define the converse translation, and we use it to prove that Loop ω is as expressive as System T. Finally, in Section 6, we describe the two applications.

Gödel System T

Gödel System T is usually defined as the simply typed λ-calculus extended with a type of natural numbers and with primitive recursion at all types. We consider in this paper a variant of System T with product types (tuples and n-ary functions) and a constant-time predecessor operation. Moreover, since we are mainly interested here in the call-by-value evaluation strategy, we formulate this system directly as a context semantics (a set of reduction rules together with an inductive definition of evaluation contexts). As usual, we consider terms up to α-conversion and the set FId (t) of free identifiers of a term t is defined in the standard way. The rewriting system is summarized in Figure 2.1, where variables x, x 1 , , x n range over a set of identifiers and t[v 1 /x 1 , , v n /x n ] denotes the usual capture-avoiding substitution. We also recall the type system in Figure 2.2 and we consider only well-typed terms in the sequel.

Remark 2.1. In order to distinguish the successor S (which is a constructor) from the successor seen as an operation (whose evaluation should imply a reduction step), we use the keyword succ as an abbreviation for λx.S(x). Note that we also consider a primitive constant-time predecessor (called pred) for complexity reasons: although this function is clearly definable in System T its complexity would be at least linear under the call-byvalue evaluation strategy [START_REF] Colson | System T, call-by-value and the minimum problem[END_REF]]. More details on this question are given in Section 6.2 and Appendix A.

Notation 2.2. We use the more verbose syntax fn (x G : σ G ) ⇒ t instead of simply λx G .t

whenever we wish to make the types explicit. Moreover, we write τ G × as an abbreviation for τ 1 × × τ n and we consider unit as the special case of τ G × obtained when n = 0.

Remark 2.3. As usual [Landin, 1964], we write let (x 1 , , x n ) = u in t be an abbreviation for the redex λ(x 1 , , x n ).t u. The following typing rule and evaluation rule can be obtained:

Γ ⊢ u: (τ 1 × × τ n ) Γ, x 1 : τ 1 , x n : τ n ⊢ t: σ Γ ⊢ let (x 1 , , x n ) = u in t: σ C[let (x 1 , , x n ) = (v 1 , , v n ) in t] C[t[v 1 /x 1 , , v n /x n ]]
Finally, note that let (x 1 , , x n ) = [ ] in t is an evaluation context.

Let us recall the well-known infinite syntactic hierarchy of fragment T n of Gödel System T. We call "recursion rank" of a term t the maximum degree of the types of the recursors which occur in t, where the degree of a type is defined as follows:

Definition 2.4. The degree ∂(τ ) of a type τ is defined inductively by:

-∂(int ) = 0 -∂(σ → τ ) = max (∂(σ) + 1, ∂(τ )) -∂(τ 1 × × τ n ) = max (∂(τ 1 ), , ∂(τ n ))
Remark 2.5. Using standard type isomorphisms, any type is isomorphic either to unit or to some type which does not contain unit . Thus we may consider without restriction that τ does not contain unit in the above definition.

Definition 2.6. The fragment T n of System T is defined as the set of terms with recursion rank less or equal to n.

Example: the Ackermann function

Our running example in this paper is the Ackermann function. This function is known not to be primitive recursive [Peter, 1968] but it can be represented in System T, for instance as follows: ack (m, n) = (rec(m, λy.succ(y), λi.λh.λy.rec(y, (h S(0)), λj.λk.(h k))) n)

It is well-known (see [START_REF] Avigad | Gödel's functional ("dialectica") interpretation[END_REF]] for instance) that functions of type N k → N that can be represented by a term of T 0 correspond exactly to primitive recursive functions. Not surprisingly, the term given in the above definition does not belong to T 0 but to T 1 (the outermost rec in the above definition has type int → int and thus has degree 1).

The higher-order Loop language

In this section, we present the Loop ω language. First, we describe the syntax and the type system, then we detail the semantics of the language. Since the structured operational semantics is tailored for the lock-step simulation, we first present the natural semantics. Our purpose is to give evidence that the various syntactic constructs have the usual semantics. In particular, this semantics extends the usual semantics for first order Loop programs with full-fledged higher-order procedures.

However natural semantics relates a program and an initial store directly to some final store and thus describes only the evaluation of terminating programs. In particular, it fails to distinguish between a non-terminating program and a run-time error. For this reason, we also define a transition semantics which refines the natural semantics. We use the transition semantics for proving the soundness of type systems and the simulation theorem (in order to derive that Loop ω programs are always terminating).

Both semantics are location-free semantics. The benefit is clear: this kind of semantics is simpler than a traditional two-level semantics (where the environment binds variables to locations and the store maps locations to values). The main drawback is the difficulty to account for advanced features such as variable aliasing. However, for our purpose, a location-free semantics is sufficient. A discussion on this subject can be found in [Plotkin, 1981] p. 70 (see also [START_REF] Felleisen | A calculus for assignments in higher-order languages[END_REF], [Donahue, 1977] and [Reynolds, 1981]).

Syntax

The syntax of imperative types and phrase types is the following:

σ, τ ::= int | proc (in τ G ; out σ G ) T ::= τ | comm | seq
Note that we consider only two formal parameter modes in and out (borrowed from Ada [START_REF] Dod | The Programming Language Ada[END_REF]) which specify "abstractly" the direction of data flow between caller and callee (without implying a specific parameter-passing mechanism).

The raw syntax of imperative programs is given below. There is nothing particular to this syntax except that we annotate each block {s} x G with a list of variables x G (see Remark 3.2). In the following grammar, x, y, z range over a set of identifiers, q ¯ranges over natural numbers (i.e., constant literals) and ε denotes the empty sequence.

G : τ G ; out z G : σ G ) {s} z G (expression) e ::= y | q ¯| a (procedure) p ::= y | a (value)
w ::= q ¯| a Remark 3.1. Note that the body of a procedure is annotated exactly by its out parameters. Besides, since anonymous procedures are not very popular in imperative languages, we use in the examples the more conventional notation for declaring local (named) procedures:

proc p(in y G : τ G ; out z G : σ G ) {s 1 } z G ; s 2
Following Landin's correspondence principle [Landin, 1964], this notation is defined as an abbreviation for a constant declaration:

cst p = proc (in y G : τ G ; out z G : σ G ) {s 1 } z G ; s 2

Type system

The type system of Loop ω may be seen as a simple effect system [Gifford andLucassen, 1986, Talpin and[START_REF] Talpin | [END_REF] since it is able to guarantee the absence of side-effects, aliasing and fix-points in well-typed programs. Its main feature is the distinction between mutable variables and read-only variables. More formally, a typing environment has the form Γ; Ω where Γ and Ω are (possibly empty) lists of pairs x: τ (x ranges over variables and τ over types). Γ stands for read-only variables (constants and in parameters) and Ω stands for mutable variables (local variables and out parameters). The type system is given in Figure 3.1. As usual, we consider programs up to renaming of bound variables, where the notion of free variable of a command is defined in the standard way.

x: τ ∈ Γ; Ω Γ; Ω ⊢ x: τ (t.env) Γ; Ω ⊢ q ¯: int (t.num) Γ; Ω ⊢ ε: seq (t.seq-i) Γ; Ω ⊢ c: comm Γ; Ω ⊢ s: seq Γ; Ω ⊢ c ; s : seq (t.seq-ii) Γ; Ω ⊢ e: τ Γ, y: τ ; Ω ⊢ s: seq Γ; Ω ⊢ cst y = e; s : seq (t.cst) Γ; Ω ⊢ e: τ Γ; y: τ , Ω ⊢ s: seq s ε Γ; Ω ⊢ var y: τ 4 e; s : seq (t.var) x G ⊂ Ω Γ; x G : σ G ⊢ s: seq Γ; Ω ⊢ {s} x G : comm (t.comm) y: int ∈ Ω Γ; Ω ⊢ inc(y): comm (t.inc) y: int ∈ Ω Γ; Ω ⊢ dec(y): comm (t.dec) y: τ ∈ Ω Γ; Ω ⊢ e: τ Γ; Ω ⊢ y 4 e: comm (t.assign) x G ⊂ Ω Γ; Ω ⊢ e: int Γ, y: int; x G : σ G ⊢ s: seq Γ; Ω ⊢ for y 4 1 to e {s} x G : comm (t.for) z G ∅ Γ, y G : τ G ; z G : σ G ⊢ s: seq Γ; Ω ⊢ proc (in y G : τ G ; out z G : σ G ){s} z G : proc (in τ G ; out σ G ) (t.proc) Γ; Ω ⊢ p: proc (in τ G ; out σ G ) Γ; Ω ⊢ e G : τ G r G : σ G ∈ Ω Γ; Ω ⊢ p(e G ; r

Remark 3.2. (scoping rules).

As usual for C -like languages, the scope of a constant (rule t.cst) or a variable (rule t.var) extends from the point of declaration to the end of the block containing the declaration. Moreover, the type system guarantees that in a block {s} x G , the variables x G are visible and they contain all the free mutable variables occurring in the sequence. For simplicity, we assume that these annotations are supplied by the programmer, but missing annotations can automatically be inferred as follows:

a block or a loop is annotated by its free mutable variables, the body of a procedure is annotated by its out parameters.

Remark 3.3. (no aliasing).

In order to avoid parameter-induced aliasing problems, we assume that all r i are pairwise distinct in rule (t.call). Indeed, we will see that in our semantics, mutable variables directly denote values and consequently different variables cannot refer to the same location in the store. However, aliasing is known to be problematic for most aspects of programming languages (see for instance [START_REF] Gellerich | Parameter-induced aliasing in ada[END_REF]] and [START_REF] Filliâtre | Verification of non-functional programs using interpretations in type theory[END_REF]) and we regard the absence of parameter-induced aliasing in Loop ω more as a feature than as a limitation.

Remark 3.4. (no side-effects). Rule (t.proc) implies that the only mutable variables which may occur inside the body of a procedure are its out parameters and its local mutable variables. This is enough to guarantee the absence of side-effects (i.e., modification of non-local variables). The purpose of this restriction is mainly to simplify the semantics of the language. However, side-effects can still be simulated in most cases by passing the non-local variable as an explicit in out parameter. This simulation is often referred to as the "state-passing transform" (see for instance [Filinski, 1994] and [Wadler, 1990]).

Remark 3.5. (no fix-points). Rule (t.proc) also forbids the reading of non-local mutable variables: this is necessary to prevents the definition of fix-points in the language. Indeed, there is a well-known technique called "tying the recursive knot" [Landin, 1964] which takes advantage of higher-order mutable variables (or function pointers) to define arbitrary recursive functions. This technique is used for instance in Scheme's semantics of the letrec construct [START_REF] Kelsey | Revised 5 report on the algorithmic language Scheme[END_REF]. Here is such a definition of a fix-point in the Loop ω syntax, where fix : proc (out int ) is a mutable variable, but this command is not typable in Loop ω (since fix occurs in the body of f ):

{ var f : proc (out int ) := proc (out x : int){ fix (x ); } x ; fix := f ; } fix
On the other hand, local procedures are not required to be closed: non-local read-only variable (such as in parameters of enclosing procedures) are allowed. We shall see that this is sufficient to encode a pure functional language.

Natural semantics

Since the evaluation relation in only defined for well-typed states, we also need to define the notion of well-typed store. Definition 3.6. A store µ is a finite mapping from (mutable) variables to closed imperative values (i.e., integer literals and procedures). A state is a pair (c, µ) consisting of a command c and µ. Definition 3.7. (store typing). We say that µ is typable in Ω, which we write as Ω ⊢ µ, if and only if for all x: τ ∈ Ω, x ∈ dom(µ) and ∅; ∅ ⊢ µ(x): τ. Definition 3.8. (state typing). We say that a state (c, µ) is typable in Ω, which we write as Ω ⊢ (c, µ), if and only if ∅; Ω ⊢ c: comm and Ω ⊢ µ.

Note that expressions do not require any evaluation (since they are either variables or values), but only fetching the corresponding value from the store whenever the expression is a mutable variable. We introduce thus the following notation: Notation 3.9. Given a store µ, let ϕ µ be the trivial extension of µ to expressions defined as follows ϕ µ (x) = µ(x) if x is a variable and ϕ µ (w) = w otherwise. In the sequel, we write e = µ w for ϕ µ (e) = w.

In order to assign default values to out parameters, we define a closed imperative value for each imperative type. Definition 3.10. For each type σ, we define inductively a default closed imperative value ǫ(σ) as follows:

-ǫ(int) = 0 -ǫ(proc (in τ G ; out σ G )) = proc (in y G : τ G ; out z: σ G ){} z G
Lemma 3.11. The typing judgment ∅; ∅ ⊢ ǫ(σ): σ is derivable.

Remark 3.12. Default values could be dispensed with using standard data-flow analysis (see [Appel, 1998] for instance). This technique (also called liveness analysis) allows to determine whether there is a potential execution path on which a variable is used before it has been assigned an initial value. We preferred not to complicate the static analysis of Loop ω programs although such an analysis is certainly convenient from a practical standpoint.

Remark 3.13. In the sequel, we shall allow for uninitialized local variables: they are assumed to be implicitly initialized by the default value corresponding to their type. More precisely, var y: τ ; s is an abbreviation for: var y: τ 4 ǫ(τ ); s.

Notation 3.14. Let c be a command. We write c[x ← w] for the substitution of a readonly variable x by a closed imperative value w and c[y z] for the renaming of a mutable variable y by a mutable variable z. The formal definitions are given in Appendix B.

We are now ready to define the natural semantics of Loop ω . The inductive definition of the evaluation relation written ⇓ is summarized in Figure 3.2 (where µ[y ← w] denotes the store obtained by replacing the value of variable y in µ by w and (µ, y ← w) denotes the store obtained by extending the store µ with a new variable y mapped to w). Remark 3.15. We rely on the renaming and substitution meta-operations in rule (N.call) in order to avoid building closures in the semantics. Besides, in parameters are passed by copy (i.e., by value) whereas out parameters are passed by reference. Note that since parameter-induced aliasing is forbidden, this latter choice has no consequence on the denotational semantics of the language (but it is important from a complexity standpoint).

(s, µ)⇓ µ ′ ({s} z G , µ)⇓ µ ′ (n.block) (s, µ)⇓ µ ′ (({} z G ; s), µ)⇓ µ ′ (n.seq-i) (c, µ)⇓ µ ′ (s, µ ′ )⇓ µ ′′ ((c; s), µ)⇓ µ ′′ (n.seq-ii) (s, µ)⇓ µ ′ (({var y: τ 4 e; } z G ; s), µ)⇓ µ ′ (n.var-i) e = µ w (s, (µ, y ← w))⇓(µ ′ , y ← w ′ )) ((var y: τ 4 e; s), µ))⇓ µ ′ (n.var-ii) e = µ w (s, µ[y ← w])⇓ µ ′ ((y 4 e; s), µ)⇓ µ ′ (n.assign) µ(y) = q (inc(y), µ))⇓ µ[y ← q + 1] (n.inc) µ(y) = q (dec(y), µ)⇓ µ[y ← q -˙1] (n.dec) e G = µ w G , p = µ proc (in y G : σ G ; out z G : τ G ){s} z G ({s[y G ← w G ][z G r G ]} r G , µ[r G ← ǫ(τ G )])⇓µ ′ (p(e G ; r G ), µ)⇓ µ ′ (n.call) e = µ w (s[y ← w], µ)⇓ µ ′ ((cst y = e; s), µ)⇓ µ ′ (n.cst) e = µ 0 (for y 4 1 to e {s} z G , µ)⇓ µ (n.for-i) e = µ q + 1 (for y 4 1 to q ¯{s} z G , µ)⇓ µ ′ ({s} z G [y ← q + 1], µ ′ )⇓ µ ′′

Transition semantics

As expected, the transition semantics of Loop ω is given by a transition system which defines inductively a binary relation between states [Plotkin, 1981]. The main design choices were influenced by the expected cost of each command. For instance, this explains the rule (s.assign) where the assignment is dealt with directly inside the sequence. Similarly, the notation = µ allows us to hide the cost of fetching the value of a variable from the store. The transition semantics is summarized in Figure 3.3.

Remark 3.16. This semantics is clearly deterministic since there is always at most one rule which can be applied (depending on the content of the store and the shape of the command). Moreover, the only case where no rule can be applied corresponds to the final state (when the program is reduced to an empty block).

Remark 3.17. It is worth mentioning that rules (s.var-i) and (s.var-ii) allows to give a simple semantics to local variable without dealing with an explicit stack. Although this is usual in natural semantics, this technique is not widespread in transition semantics. The ingenious idea consisting in updating a local variable directly in the source (in rule s.varii) is attributed to Eugene Fink in [Reynolds, 1998] p. 130. This technique is however well-known in functional language semantics [START_REF] Felleisen | A calculus for assignments in higher-order languages[END_REF].

As expected, the "subject reduction" property holds for the transition semantics. The proof of the following theorem is given in Appendix B.

Theorem 3.18. For any environment Ω and any state (c, µ), we have that ∅; Ω ⊢ (c, µ) and (c, µ) (c ′ , µ ′ ) implies ∅; Ω ⊢ (c ′ , µ ′ ) and dom(µ) = dom(µ ′ ).

Moreover, the equivalence of the natural and transition semantics for Loop ω can be proved by establishing the following two usual lemmas.

({s} x G , µ) ({s ′ } x G , µ ′ ) and ({s ′ } x G , µ ′ )⇓ µ ′′ then ({s} x G , µ)⇓ µ ′′ .

Lock-step simulation

In this section, we show how to translate a Loop ω program into a term of System T and we prove the simulation theorem. Then we exhibit a hierarchy of fragments Loop n which is an imperative counterpart of the fragments T n of Gödel System T. Finally, we introduce the notion of "singular" Loop ω program whose translation does not require the product type in System T.

Translation

In order to translate default imperative values, we shall need corresponding default functional values.

(s, µ) (s ′ , µ ′ ) ({s} z G , µ) ({s ′ } z G , µ ′ ) (s.block) (({} z G ; s), µ) (s, µ) (s.seq-i) (c, µ) (c ′ , µ ′ ) ((c; s), µ) ((c ′ ; s), µ ′ ) (s.seq-ii) e = µ w (s, (µ, y ← w)) (ε, (µ ′ , y ← w ′ )) ((var y: τ 4 e; s), µ) (ε, µ ′ ) (s.var-i) e = µ w (s, (µ, y ← w)) (s ′ , (µ ′ , y ← w ′ ))
((var y: τ 4 e; s), µ) ((var y: τ δ(int

4 w ′ ; s ′ ), µ ′ ) (s.var-ii) e = µ w ((y 4 e; s), µ) (s, µ[y ← w]) (s.assign) µ(y) = q (inc(y), µ) (y 4 q + 1, µ) (s.inc) µ(y) = q (dec(y), µ) (y 4 q -˙1, µ) (s.dec) e G = µ w G p = µ proc (in y G : σ G ; out z G : τ G ){s} z G (p(e G ; r G ), µ) ({s[y G ← w G ][z G r G ]} r G , µ[r G ← ǫ(τ G )]) (s.call) e = µ w ((cst y = e; s), µ) (s[y ← w], µ) (s.cst) e = µ 0 (for y 4 1 to e {s} z G , µ) ({} z G , µ) (s.for-i) e = µ q + 1 (for y 4 1 to e {s} z G , µ) ({for y 4 1 to q ¯{s} z G ; s[y ← q + 1]} z G , µ) (s.for-ii)
) = 0 -δ(σ → τ ) = fn (x: σ) ⇒ δ(τ ) -δ(σ 1 × × σ n ) = (δ(σ 1 ), , δ(σ n ))
We also write δ(σ G ) as an abbreviation for (δ(σ 1 ), , δ(σ n )).

Lemma 4.2. The typing judgment ⊢ δ(σ): σ is derivable.

We are now ready to define the translation of imperative types. Note that the translation of a procedure type encode exactly the data-flow specified by the formal parameter modes in and out (and this is sufficient since side-effects are not allowed). Definition 4.3. The translations σ ⋆ of an imperative type σ is defined inductively as follows:

-int ⋆ = int -proc (in σ G ; out τ G ) ⋆ = (σ G ⋆ ) × → (τ G ⋆ ) × Moreover, if Γ is x 1 : τ 1 , , x n : τ n , we define Γ ⋆ as x 1 : τ 1 ⋆ , , x n : τ n ⋆ .
The intuition behind the translation of imperative programs is the following: a block

{c 1 ; ; c n } x G is translated into: let x G 1 = c 1 ⋆ in let x G n = c n ⋆ in x G
where each x G i ⊆ x G corresponds to the "output" of command c i and x G is the output of the block. Note in particular that the same identifier is used again and again in order to simulate imperative updates. For instance, the block {inc(x); inc(x)} x is translated as:

let x = succ(x) in let x = succ(x) in x
Let us now give the formal definition of the translation and then present a complete example. n ¯⋆ = S n (0) The following theorem states that translation ( ) ⋆ is type-preserving (its proof is given in Appendix C). Theorem 4.7. For any environments Γ and Ω, any expression e and any block {s} x G we have:

-y ⋆ = y -(proc (in y G : σ G ; out z G : τ G ){s} z G ) ⋆ = fn (y G : σ G ⋆ ) ⇒ {s} z G ⋆ [δ(τ G ⋆ )/z G ] -{s} x G ⋆ = (s) x G ⋆ -(ε) x G ⋆ = x G -(var y: τ 4 e; s) x G ⋆ = (s) x G ⋆ [e ⋆ /y] -(cst y = e; s) x G ⋆ = let y = e ⋆ in (s) x G ⋆ -(y 4 e; s) x G ⋆ = let y = e ⋆ in (s) x G ⋆ -(inc(y); s) x G ⋆ = let y = succ(y) in (s) x G ⋆ -(dec(y); s) x G ⋆ = let y = pred(y) in (s) x G ⋆ -(p(e G ; z G ); s) x G ⋆ = let z G = p ⋆ e G ⋆ in (s) x G ⋆ -({s 1 } z G ; s 2 ) x G ⋆ = let z G = {s 1 } z G ⋆ in (s 2 ) x G ⋆ -(for y 4 1 to e {s 1 } z G ; s 2 ) x G ⋆ = let z G = rec(e ⋆ , z G , λy.λz G .{s 1 } z G ⋆ ) in (s 2 ) x G ⋆
-Γ; Ω ⊢ e: τ implies Γ ⋆ , Ω ⋆ ⊢ e ⋆ : τ ⋆ -Γ; Ω, x G : σ G ⊢ s: seq implies Γ ⋆ , Ω ⋆ , x G : σ G ⋆ ⊢ (s) x G ⋆ : (σ G ⋆ ) × -Γ; x G : σ G ⊢ {s} x G : comm implies Γ ⋆ , x G : σ G ⋆ ⊢ {s} x G ⋆ : (σ G ⋆ ) ×

Example: the Ackermann function

Here is an implementation of the Ackermann function as an anonymous procedure of Loop ω . This program was actually programmed by hand, but we shall see in Section By applying translation ( ) ⋆ , we obtain the following anonymous function. For clarity, we use Standard ML derived forms [START_REF] Milner | The Definition of Standard ML[END_REF] Note that although we could prove by hand that this functional program is equivalent to the term ack given in Section 2.1, we shall see that this property is mostly an application of the main theorem of Section 5.

Simulation theorem

Let us prove the main theorem which states that for any block {s} x G , the evaluation of {s} x G runs in lock-step with the reduction of {s} x G ⋆ . We first need some preliminary substitution lemmas: Notation 4.8. If µ is a store and x G ⊂ dom(µ), we write µ(x G ) for (µ(x 1 ), , µ(x n )).

Moreover, if v G = (v 1 , , v k ) we write v G ⋆ for the tuple (v 1 ⋆ , , v k ⋆ ).
Lemma 4.9. For any block {s} z G such that Γ; z

G : τ G ⊢ {s} z G : comm, the following equality holds: {s} z G ⋆ [δ(τ G )/z G ] = {s[z G r G ]} r G ⋆ [δ(τ G )/r G ].
Lemma 4.10. For any command c, any read-only variable x and any closed imperative value w, we have

(c[x G ← w G ]) ⋆ = c ⋆ [w G ⋆ /x G ].
Lemma 4.11. If e = µ w then either e = w or e is some variable x i with µ(x i ) = w and

then c ⋆ [µ(x G ) ⋆ /x G ] = c ⋆ [w ⋆ /x i ][µ(x G ) ⋆ /x G ].
Theorem 4.12. For any well-typed state (s, µ), if x G = dom(µ) and z G ⊆ x G we have:

(s, µ) (s ′ , µ ′ ) implies (s) z G ⋆ [µ(x G ) ⋆ /x G ] (s ′ ) z G ⋆ [µ ′ (x G ) ⋆ /x G ]
Proof. By induction on the derivation of (s, µ) (s ′ , µ ′ ). For brevity, we write v

G for µ(x G ) and v G ′ for µ ′ (x G ). • (s.block) (s) z G ⋆ [v G ⋆ /x G ] (s ′ ) z G ⋆ [v G ′ ⋆ /x G ] {s} z G ⋆ [v G ⋆ /x G ]) {s ′ } z G ⋆ [v G ′ ⋆ /x G ] Indeed: {s} z G ⋆ [v G ⋆ /x G ] = (s) z G ⋆ [v G ⋆ /x G ] (s ′ ) z G ⋆ [v G ′ ⋆ /x G ] by induction hypothesis (since z G ⊆ x G ) = {s ′ } z G ⋆ [v G ′ ⋆ /x G ] • (s.seq-i) ({} y G ; s) z G ⋆ [v G ⋆ /x G ] (s) z G ⋆ [v G ⋆ /x G ]
Indeed:

({} y G ; s) z G ⋆ [v G ⋆ /x G ] = (let y G = {} y G ⋆ in (s) z G ⋆ )[v G ⋆ /x G ] = (let y G = y G in (s) z G ) ⋆ [v G ⋆ /x G ] (s) z G ⋆ [v G ⋆ /x G ] • (s.seq-ii) c ⋆ [v G ⋆ /x G ] c ′ ⋆ [v G ′ ⋆ /x G ] (c; s) z G ⋆ [v G ⋆ /x G ] (c ′ ; s) z G ⋆ [v G ′ ⋆ /x G ] Indeed, if r G = O(c)
as defined in Remark 4.5, we have:

(c; s) z G ⋆ [v G ⋆ /x G ] = (let r G = c ⋆ in (s) z G ⋆ )[v G ⋆ /x G ] = (let r G = c ⋆ [v G ⋆ /x G ] in (s) z G ⋆ )[v G ⋆ /x G ] (let r G = c ′ ⋆ [v G ′ ⋆ /x G ] in (s) z G ⋆ )[v G ⋆ /x G ] by induction hypothesis = (let r G = c ′ ⋆ [v G ′ ⋆ /x G ] in (s) z G ⋆ )[v G ′ ⋆ /x G ] since µ ⋆ (y) = µ ′⋆ (y) for any y r G = (let r G = c ′ ⋆ in (s) z G ⋆ )[v G ′ ⋆ /x G ] = (c ′ ; s) z G ⋆ [v G ′ ⋆ /x G ] • (s.var-i) (s) z G ⋆ [v ⋆ /x G , w ⋆ /y] (ε) z G ⋆ [v ′ ⋆ /x G , w ′ ⋆ /y] (var y: τ 4 e; s) z G ⋆ [v G ⋆ /x G ] (ε) z G ⋆ [v G ′ ⋆ /x G ]
Since e = µ w, by lemma 4.11:

(var y: τ 4 e; s) z G ⋆ [v G ⋆ /x G ] = ((ε) z G ⋆ [e ⋆ /y])[v G ⋆ /x G ] = ((s) z G ⋆ [w ⋆ /y])[v G ⋆ /x G ] (ε) z G ⋆ [w ⋆ /y ′ ][v G ′ ⋆ /x G ] by induction hypothesis (since z G ⊆ x G ⊆ x G , y) = ((ε) z G ⋆ [v G ′ ⋆ /x G ] since y z G • (s.var-ii) (s) z G ⋆ [v ⋆ /x G , w ⋆ /y] (s ′ ) z G ⋆ [v ′ ⋆ /x G , w ′ ⋆ /y] (var y: τ 4 e; s) z G ⋆ [v G ⋆ /x G ] (var y: τ 4 w ′ ; s ′ ) z G ⋆ [v G ′ ⋆ /x G ]
Since e = µ w, by lemma 4.11:

(var y: τ 4 e; s) z G ⋆ [v G ⋆ /x G ] = ((s) z G ⋆ [e ⋆ /y])[v G ⋆ /x G ] = ((s) z G ⋆ [w ⋆ /y])[v G ⋆ /x G ] ((s ′ ) z G ⋆ [w ′ ⋆ /y])[v G ′ ⋆ /x G ] by induction hypothesis (since z G ⊆ x G ⊆ {x G , y}) = (var y: τ 4 w ′ ; s ′ ) z G ⋆ [v G ′ ⋆ /x G ] • (s.assign) (y 4 e; s) z G ⋆ [v G ⋆ /x G ] (s) z G ⋆ [v G ′ ⋆ /x G ] with v G ′ = µ[y ← w](x G ). Since e = µ w, by lemma 4.11: (y 4 e; s) z G ⋆ [v G ⋆ /x G ] = (let y = e ⋆ in (s) z G ⋆ )[v G ⋆ /x G ] = (let y = w ⋆ in (s) z G ⋆ )[v G ⋆ /x G ] (s) z G ⋆ [w ⋆ /y][v G ⋆ /x G ] = (s) z G ⋆ [v G ′ ⋆ /x G ] • (s.inc) (inc(y)) ⋆ [v G ⋆ /x G ] q + 1 ⋆ [v G ⋆ /x G ] Indeed, since µ(y) = q ¯: (inc(y)) ⋆ [v G ⋆ /x G ] = succ(y)[v G ⋆ /x G ] = succ(S q (0)) (S q+1 (0))) = q + 1 ⋆ • (s.dec) This case is similar to (s.inc). • (s.call) p(e G , r G ) ⋆ [v G ⋆ /x G ] {s[z G r G ][y G ← w G ]} r G ⋆ [v G ′ ⋆ /x G ]
where v

G ′ = µ ′ (x G ) = µ[r G ← ǫ(τ G )](x G ). By Lemma 4.11, since e G = µ w G and p = µ proc (in y G : σ G ; out z G : τ G ){s} z G : p(e G , r G ) ⋆ [v G ⋆ /x G ] = (p ⋆ e G ⋆ )[v G ⋆ /x G ] = (proc (in y G : σ G ; out z G : τ G ){s} z G ) ⋆ w G ⋆ )[v G ⋆ /x G ] = (fn (y G : σ G ⋆ ) ⇒ {s} z G ⋆ [δ(τ G ⋆ )/z G ]) w G ⋆ )[v G ⋆ /x G ] {s} z G ⋆ [δ(τ G ⋆ )/z G ][w G ⋆ /y G ][v G ⋆ /x G ] = {s[z G r G ]} r G ⋆ [δ(τ G ⋆ )/r G ][w G ⋆ /y G ][v G ⋆ /x G ] by Lemma 4.9 = {s[z G r G ]} r G ⋆ [w G ⋆ /y G ][ǫ(τ G ) ⋆ /r G ][v G ⋆ /x G ] by Lemma 4.6 = {s[z G r G ][y G ← w G ]} r G ⋆ [ǫ(τ G ) ⋆ /r G ][v G ⋆ /x G ] by Lemma 4.10 = {s[z G r G ][y G ← w G ]} r G ⋆ [v G ′ ⋆ /x G ] since r G ⊆ x G . • (s.cst) (cst y = e; s) z G ⋆ [v G ⋆ /x G ] (s[y ← w]) z G ⋆ [v G ⋆ /x G ]
Since e = µ w, by Lemma 4.11:

(cst y = e; s) z G ⋆ [v G ⋆ /x G ] = (let y = e ⋆ in (s) z G ⋆ )[v G ⋆ /x G ] = (let y = w ⋆ in (s) z G ⋆ )[v G ⋆ /x G ] ((s) z G ⋆ [w ⋆ /y])[v G ⋆ /x G ] = (s[y ← w]) z G ⋆ [v G ⋆ /x G ] by Lemma 4.10
• (s.for-i)

(for y 4 1 to e {s} z G ) ⋆ [v G ⋆ /x G ] {} z G ⋆ [v G ⋆ /x G ]
Since e = µ 0, by Lemma 4.11:

(for y 4 1 to e {s} z G ) ⋆ [v G ⋆ /x G ] = rec(e ⋆ , z G , λy.λz G .{s} z G ⋆ )[v G ⋆ /x G ] = rec(0, z G , λy.λz G .{s} z G ⋆ )[v G ⋆ /x G ] z G [v G ⋆ /x G ] = {} z G ⋆ [v G ⋆ /x G ] • (s.for-ii) (for y 4 1 to e {s} z G ⋆ )[v G ⋆ /x G ] {for y 4 1 to q ¯{s} z G ; s[y ← q + 1]} z G ⋆ [v G ⋆ /x G ]
Since e = µ q + 1, by Lemma 4.11: Proof. Indeed, since System T is strongly normalizing (see [START_REF] Girard | Proofs and Types[END_REF] for instance).

(for y 4 1 to e {s} z G ) ⋆ [v G ⋆ /x G ] = rec(e ⋆ , z G , λy.λz G .{s} z G ⋆ )[v G ⋆ /x G ] = rec(S q+1 (0), z G , λy.λz G .{s} z G ⋆ )[v G ⋆ /x G ] ((λz G .{s} z G ⋆ [S q+1 (0)/y]) rec(S q (0), z G , λy.λz G .{s} z G ⋆ ))[v G ⋆ /x G ] = (let z G = rec(S q (0), z G , λy.λz G .{s} x G ⋆ ) in {s[y ← q + 1]} z G ⋆ )[v G ⋆ /x G ] = (let z G = (for y 4 1 to q ¯{s} z G ) ⋆ in {s[y ← q + 1]} z G ⋆ )[v G ⋆ /x G ] = {for y 4 1 to q ¯{s} z G ; s[y ← q + 1]} z G ⋆ [v G ⋆ /x G ]
Let us now focus on the imperative counterpart of the hierarchy of fragment T n of Gödel System T. We define first the level of an imperative type and then the "iteration rank" of a Loop ω program as follows: Definition 4.14. The level ℓ(τ ) of an imperative type τ is defined inductively by:

-ℓ(int) = 0 -ℓ(proc (in y G : σ G ; out z G : τ G ){s} z G ) = max (ℓ(σ G ) + 1, ℓ(τ G )) where ℓ(τ G ) = max (ℓ(τ 1 ), , ℓ(τ n )).
Definition 4.15. We call "iteration rank" of a Loop ω program p the maximum level of the types of mutable variables which annotate a loop of p. Definition 4.16. The fragment Loop n of Loop ω is defined as the set of programs with iteration rank less than n. Lemma 4.17. For any imperative types τ

G, ∂((τ G ⋆ ) × ) = ℓ(τ G ).
Proposition 4.18. For any Loop ω program p, the iteration rank of p is the same as the recursion rank of p ⋆ . Proof. Indeed, since for any loop which occurs in p with mutable variables z G : τ G we have:

(for y 4 1 to e {s} z G ) ⋆ = rec(e ⋆ , z G , λy.λz G .{s} z G ⋆ )
where this recursor has type (τ G ⋆ ) × and ∂((τ G ⋆ ) × ) = ℓ(τ G ) by lemma 4.17.

Remark 4.19. A function computable in the fragment Loop 0 is thus computable in T 0 , hence it is primitive recursive. Consequently, adding only higher-order procedures (without procedural variables) to the Loop language does not increase its expressive power.

In the next section, we shall be interested in Loop ω programs which are translated into terms which contain no pairing and no pattern matching. The following lemma is straightforward (by definition of the translation). Definition 4.20. We call "singular" a Loop ω program in which all procedures have exactly one in parameter and one out parameter and all blocks are annotated by exactly one mutable variable. Lemma 4.21. For any singular Loop ω program p, the term p ⋆ contains no product types (no tuples and no pattern matching).

Expressiveness

In this section, we show how to represent any functional of Gödel's system T by some Loop ω program. However, since there is no direct counterpart to pattern-matching in Loop ω , we consider in this section a variant of System T with explicit pairing function and projections. On the other hand, it is straightforward to encode a (lazy) pair as an anonymous procedure with no input parameter (a thunk). Definition 5.1. We define (σ * τ ) as unit → (σ × τ ) and call S the set of types built inductively from int using the type constructors → and * . Definition 5.2. For any terms t: σ, u: τ we write < t, u > : σ * τ as an abbreviation for the term fn () ⇒ (t, u). Moreover, we define π σ,τ 1 : σ * τ → σ and π σ,τ 2 : σ * τ → τ as the following abbreviations:

π σ,τ 1 (z) = let (x, y) = z() in x and π σ,τ 2 (z) = let (x, y) = z() in y Lemma 5.3.
The following reduction rules are derivable (where v, w are values):

π σ,τ 1 < v, w > ⋆ v π σ,τ 2 < v, w > ⋆ w
Definition 5.4. For any type σ ∈ S the translation σ ⋄ is defined as follows:

-

int ⋄ = int -(σ → τ ) ⋄ = proc (in σ ⋄ ; out τ ⋄ ) -(σ * τ ) ⋄ = proc (out σ ⋄ , τ ⋄ )
Lemma 5.5. For any type σ ∈ S, we have (σ ⋄ ) ⋆ = σ.

We are now ready to translate terms of System T into Loop ω programs. More precisely, a term t of type σ is translated into a command c with exactly one free mutable r variable of type σ ⋄ for the result (i.e., O(c) = r). For simplicity, we shall define the translation only for terms that obey some syntactic criterion: Definition 5.6. We call V and L the subset of values and terms of System T defined by the following syntax:

v, w : : = x | S n (0) | λx.t | < t, u > t, u : : = v | succ(v) | pred(v) | rec(v, u, λy.λz.t) | (v w) | (t v) | (v u) | π σ,τ 1 (v) | π σ,τ 2 (v)
Remark 5.7. Clearly, terms of L can be seen as terms of System T since succ, π σ,τ 1 , π σ,τ 2 and < t, u > are just macro-definitions. Conversely, any term of System T (as defined in figure 2.1) is clearly equivalent to a term of L. Indeed, the requirements that v be a value in any sub-term of the form π σ,τ 1 (v), π σ,τ 2 (v) or rec(v, u, λy.λz.t) and that either t or u be a value in an application (t u) are easily fulfilled by naming intermediate results when necessary (using a β-redex to simulate a let). Definition 5.8. For any value v in V and any term t in L such that Γ ⊢ t: σ, the translation v ⋄ and t r ⋄ where r is a fresh variable of type σ ⋄ are defined by mutual induction as follows (the types of the terms are written as superscript when required):

-S n (0) ⋄ = n - y ⋄ = y -(fn x: τ ⇒ t ω ) ⋄ = proc (in x: τ ⋄ ; out y: ω ⋄ ) t y ⋄ -( < t, u > ) ⋄ = proc (out x: σ ⋄ , y: τ ⋄ ){t x ⋄ ; u y ⋄ } x, y -(v) r ⋄ = r 4 v ⋄ -succ(v) r ⋄ = {r 4 v ⋄ ; inc(r)} r -pred(v) r ⋄ = {r 4 v ⋄ ; dec(r)} r -rec(v, u, λy.λz.t) r ⋄ = {u r ⋄ ; for y 4 1 to v ⋄ {cst z = r; t r ⋄ } r } r -(v w) r ⋄ = v ⋄ (w ⋄ ; r) -(v u τ ) r ⋄ = {var y: τ ⋄ ; u y ⋄ ; v ⋄ (y; r)} r -(t τ →ω v) r ⋄ = {var x: (τ → ω) ⋄ ; t x ⋄ ; x(v ⋄ ; r)} r -π σ,τ 1 (v) r ⋄ = {var y: τ ⋄ ; v ⋄ (r, y)} r -π σ,τ 2 (v) r ⋄ = {var x: σ ⋄ ; v ⋄ (x, r)} r
Remark 5.9. In Definition 5.8, we tried to reach a compromise between the simplicity of the translation and the effort required to prepare the term before its translation. It is however possible to generalize the above translation to arbitrary terms of System T (without restricting them to L). We obtain thus essentially the body of the imperative version of the Ackermann function given in Section 2.1 (apart from non-mandatory blocks and constant declarations).

Note that all identifiers of the source term are mapped to read-only variables (hence the introduction of a constant declaration in the translation of a recursor). This property ensures that mutable variables do not occur in the body of procedures in the resulting Loop ω program: the only mutable variables are fresh variables introduced during the translation.

Lemma 5.11. Given a term t ∈ L such that Γ ⊢ t: σ and a fresh mutable variable r of type σ ⋄ we have Γ ⋄ ; r: σ ⋄ ⊢ t r ⋄ : comm.

Proof. By induction on t.

For any term t ∈ L, the fresh mutable variable r in t r ⋄ is always initialized before it is read, and thus r is not free in (t r ⋄ ) ⋆ . This property is stated more formally by the following lemma. Lemma 5.12. Given a term t ∈ L such that Γ ⊢ t: σ and a fresh mutable variable r of type σ ⋄ we have r FId ((t r ⋄ ) ⋆ ).

Proof. By induction on t.

Let us write ։ for the reflexive, transitive and contextual closure (with respect to arbitrary contexts) of the following general βπ-reduction rule (where t 1 , , t n are not necessarily values):

let (x 1 , , x n ) = (t 1 , , t n ) in u u[t 1 /x 1 , , t n /x n ]
As expected, the translated (t r ⋄ ) ⋆ of a term t requires several "administrative" reductions in order to recover the original term. Theorem 5.13. Given a term t ∈ L such that Γ ⊢ t: σ and a fresh mutable variable r of type σ ⋄ we have (t r ⋄ ) ⋆ ։ t.

Proof. By mutual induction, we prove that for any value v ∈ V such that Γ ⊢ v: τ we have (v ⋄ ) ⋆ ։ v and for any term t ∈ L such that Γ ⊢ t: σ and any fresh mutable variable r of type σ ⋄ we have (t r ⋄ ) ⋆ ։ t.

• (S n (0) ⋄ ) ⋆ = n ¯⋆ = S n (0) • (y ⋄ ) ⋆ = y ⋆ = y • ((fn x: τ ⇒ t ω ) ⋄ ) ⋆ = (proc(in x: τ ⋄ ; out y: ω ⋄ ) t y ⋄ ) ⋆ = fn (x: τ ) ⇒ (t y ⋄ ) ⋆ [δ(ω)/y] = fn (x: τ ) ⇒ (t y ⋄ ) ⋆ since y FId ((t y ⋄ ) ⋆ ) ։ fn x: τ ⇒ t by induction hypothesis. • ( < t, u > r ⋄ ) ⋆ = (proc(out x: σ ⋄ , y: τ ⋄ ){t x ⋄ ; u y ⋄ } x, y ) ⋆ = (fn () ⇒ let x = (t x ⋄ ) ⋆ in let y = (u y ⋄ ) ⋆ in (x, y)) ։ fn () ⇒ ((t x ⋄ ) ⋆ , (u y ⋄ ) ⋆ ) ։ < t, u > by induction hypothesis. • ((v) r ⋄ ) ⋆ = (r 4 v ⋄ ) ⋆ = (v ⋄ ) ⋆ ։ v by induction hypothesis. • (succ(v) r ⋄ ) ⋆ = {r 4 v ⋄ ; inc(r)} r ⋆ = let r = (v ⋄ ) ⋆ in let r = succ(r) in r ։ let r = succ((v ⋄ ) ⋆ ) in r ։ succ((v ⋄ ) ⋆ )
։ succ(v) by induction hypothesis.

• The case of pred is similar to succ.

• (rec(v, u, λy.λz.t) r ⋄ ) ⋆ = {u r ⋄ ; for y 4 1 to v ⋄ {cst z = r; t r ⋄ } r } r ⋆ = let r = (u r ⋄ ) ⋆ in let r = rec((v ⋄ ) ⋆ , r, λy.λr.let z = r in (t r ⋄ ) ⋆ ) in r ։ let r = rec((v ⋄ ) ⋆ , (u r ⋄ ) ⋆ , λy.λz.let z = z in (t r ⋄ ) ⋆ ) in r since r FId ((t r ⋄ ) ⋆ ) ։ rec((v ⋄ ) ⋆ , (u r ⋄ ) ⋆ , x, λz.λy.(t r ⋄ ) ⋆ ) ։ rec(v, u, λz.λy.t) by induction hypothesis. • ((v τ →σ w) r ⋄ ) ⋆ = (v ⋄ (w ⋄ ; r)) ⋆ = (v ⋄ ) ⋆ (w ⋄ ) ⋆ ։ (v w) by induction hypothesis. • ((t τ →σ v) r ⋄ ) ⋆ = {var p: (τ → σ) ⋄ ; t p ⋄ ; p(v ⋄ ; r)} r ⋆ = (let p = (t p ⋄ ) ⋆ in let r = p (v ⋄ ) ⋆ in r)[δ(τ → σ)/p] = let p = (t p ⋄ ) ⋆ in let r = p (v ⋄ ) ⋆ in r since p FId ((t p ⋄ ) ⋆ ) ։ (t p ⋄ ) ⋆ (v ⋄ ) ⋆ ։ (t v) by induction hypothesis. • ((v τ →σ u) r ⋄ ) ⋆ = {var y: τ ⋄ ; u y ⋄ ; v(y; r)} r ⋆ = (let y = (u y ⋄ ) ⋆ in let r = (v ⋄ ) ⋆ y in r)[δ(τ )/y] = let y = (u y ⋄ ) ⋆ in let r = (v ⋄ ) ⋆ y in r since y FId ((u y ⋄ ) ⋆ ) ։ (v ⋄ ) ⋆ (u y ⋄ ) ⋆ ։ (v u) by induction hypothesis. • (π σ,τ 1 (v) r ⋄ ) ⋆ = = {var y: τ ⋄ ; v ⋄ (r, y)} r ⋆ = (let (r, y) = (v ⋄ ) ⋆ () in r)[δ(τ )/y] = let (r, y) = (v ⋄ ) ⋆ () in r since y FId ((v ⋄ ) ⋆ ) ։ let (r, y) = v() in r by induction hypothesis. = π σ,τ 1 (v) by definition of π σ,τ 1 .
• The case of π σ,τ 2 is similar to π σ,τ 1 .

Lemma 5.14. For any functional type τ, ∂(τ ⋄ ) = ℓ(τ ).

Proposition 5.15. Given a term t ∈ L such that Γ ⊢ t: σ and a fresh mutable variable p of type σ ⋄ , the iteration rank of t p ⋄ is the same as the recursion rank of t.

Proof. Indeed, any occurrence of a recursor type τ in t is translated as follows:

rec(x, u, λy.λz.s) r ⋄ = {u r ⋄ ; for y 4 1 to x {cst z = r; s r

⋄ } r } r
where r is a mutable variable of type τ ⋄ . We can conclude since r occurs inside a loop and ∂(τ ⋄ ) = ℓ(τ ) by lemma 5.14.

Remark 5.16. Note that a term with no product types (no pairs and no projections) is translated into a singular Loop ω program.

Applications

Characterizing elementary functions

A first application of the results of this paper is extensional: we give a new characterization of the class of Csillag-Kalmar elementary recursive functions (the class E 3 in Grzegorczyk hierarchy). In [START_REF] Beckmann | Characterizing the elementary recursive functions by a fragment of Gödel's T[END_REF], the authors consider a variant of System T with an explicit discriminator D and an iterator I instead of a recursor and they prove the following theorem: Theorem 6.1. [START_REF] Beckmann | Characterizing the elementary recursive functions by a fragment of Gödel's T[END_REF] The set of terms of System T which contain no λ-abstraction of the form λx I(t, ) where x occurs in t compute exactly the class of elementary recursive functions.

It is well-known that both operators D and I are special cases of the recursor where D(n, a, b) ≡ rec(n, a, λi.λx.b) and I(n, b, λy.a) ≡ rec(n, b, λi.λy.a) where x, i are fresh identifiers. On the imperative side, these operators correspond respectively to the standard compound statements if then else and loop n { } (where there is no iteration variable available inside the body of the loop).

Given a term t, their restriction amounts to requiring that in any sub-term I(u, ) of t the free identifiers of u are actually free identifiers of t (input identifiers). Let us now define the imperative counterpart of this restriction. Definition 6.2. We call "elementary" any singular Loop ω program p such that Γ; r: int ⊢ p: comm and any loop has the form {var n: int; {s 1 } n ; loop n {s 2 } z } z where the only free read-only variables of s 1 are in Γ. Remark 6.3. In this definition, the loop statement corresponds to a macro-definition for a for loop in which the iteration variable does not occur. Note also that if then else statements are allowed without restriction in p. In particular, we obtain that any Loop ω program in which any bound of loop is a read-only input variable is elementary.

As a corollary of Theorems 4.12 and 5.13 we obtain the following result: Since the only free read-only variables of {s 1 } n ⋆ are input variables, the term p ⋆ computes thus an elementary function. Conversely, for any term t: σ of System T which obeys Beckmann and Weirmann's restriction, the term t r ⋄ (where r is a fresh mutable variable of type σ ⋄ ) is an elementary singular Loop ω programs (see remark 5.9). Remark 6.5. If x is an identifier in rec(x, z , λy.λz.{s} z ⋆ ) there is no need for introducing the local variable n in its imperative translation and we obtain thus the following simpler form loop x {s} z . As a special case, we obtain thus that any Loop ω program in which any bound of a loop is an input read-only variable is elementary. Actually, we conjecture that such programs are sufficient to represent any elementary function (a proof of this result would follow step by step the proof given for System T in Section 4 of [START_REF] Beckmann | Characterizing the elementary recursive functions by a fragment of Gödel's T[END_REF]).

Remark 6.6. For simplicity, we restricted ourselves to singular Loop ω programs since [START_REF] Beckmann | Characterizing the elementary recursive functions by a fragment of Gödel's T[END_REF] do not consider product types. However, since their result is extensional, any encoding of product types in System T (which does not use the recursor) would allow to generalize the above corollary to non-singular elementary Loop ω programs. Such an encoding is the following:

The product σ × τ is defined by induction on σ and then on τ . Firstly, int × int is encoded as int → int where t, u int ×int ≡ λb.D(b, t, u) and with π int ×int 1 (p) ≡ (p 0) and π int ×int 2 (p) ≡ (p S(0)). Now int × (σ → ς) is defined as σ → (int × ς) and (σ → ς) × τ as σ → (ς × τ ). The corresponding pairing functions and projections are summarized below. It is straightforward to prove that π 1 t, u = t and π 2 t, u = u for any types σ, τ (note however that the η-rule is required).

The minimum problem

The second application is intensional and is related to the so-called minimum problem. In [START_REF] Colson | System T, call-by-value and the minimum problem[END_REF]], the authors proved that in call-by-value System T, any algorithm which computes a non-trivial binary function (where trivial means constant or projection plus constant), has a time-complexity which is at least linear in one of the inputs. As a consequence, they obtain the following result: Theorem 6.7. [START_REF] Colson | System T, call-by-value and the minimum problem[END_REF]] There is no term of call-by-value System T which computes the minimum of two natural numbers with time-complexity O(min(n, m)).

Remark 6.8. It is worth noticing that this property depends strongly on the reduction rules used for the recursor (and not only on the strategy). For instance, the property does not hold if we consider the following reduction rule for rec (which is derivable in call-byname, but not in call-by-value):

rec(S(n), v, λx.λy.t) t[n/x, rec(n, b, λx.λy.t)/y] Indeed, since we consider weak reduction and since y may occurs under the scope of a λabstraction in t, there no reason that rec(n, b, λx.λy.t) be the next redex to contract. In fact, one can easily show that call-by-name evaluation can be simulated under call-byvalue evaluation using this rule and the usual thunk-based encoding [START_REF] Hatcliff | Thunks and the lambda-calculus[END_REF]].

| for y 4 1

 4 to e {s} x G | y 4 e | inc(y) | dec(y) | p(e G ; y G ) (sequence) s ::= ε | c ; s | cst y = e; s | var y: τ 4 e; s (anonymous procedure) a ::= proc (in y

Figure 3 . 1 .

 31 Figure 3.1. Imperative type system

(for y 4 1

 4 Figure 3.2. Natural semantics

Lemma 3. 19 .

 19 The relation ({s} x G , µ) ⋆ ({} x G , µ ′ ) is closed under the defining conditions of the ⇓ relation. Lemma 3.20. The ⇓ relation is closed under head expansion: if

Figure

  Figure 3.3. Transition semantics Definition 4.1. For each type σ, we define inductively a default closed value δ(σ) as follows:

Definition 4 . 4 .

 44 For any expression e, block b, sequence s and variables x G, the translations e ⋆ , b ⋆ and (s) x G ⋆ into terms of System T are defined by mutual induction as follows:

Remark 4 . 5 .

 45 It is possible to factor out the translation of commands in the above definition. Indeed, the translation of a non-empty block {c; s} x G always follows the same pattern: {c; s} x G ⋆ = let z G = c ⋆ in {s} x G ⋆ where z G is a list of "output" variables of depending on the command c. The translation c ⋆ of a command c together with its output variables O(c) are summarized in the following table:

6 .

 6 For any imperative type σ, we have ǫ(σ) ⋆ = δ(σ ⋆ ).

  for declaring several functions (keyword fun) and values (keyword val) within a unique let. fn (m: int, n: int) ⇒ let fun next (y: int ) = let val p = y val p = succ(p) in p end val g = next val g = rec(m, g, λi.λg.let val h = g fun aux (y: int) = let val p = h S (0) val p = rec(y, p, λj.λp.let val p = h p in p end) in p end val g = aux in g end) val r = g n in r end

Corollary 4 .

 4 13. All programs of Loop ω are terminating.

Corollary 6 . 4 .

 64 The elementary singular Loop ω programs compute exactly the class of elementary recursive functions.Proof. Indeed, let p be and elementary singular Loop ω program. For any occurrence of a loop statement in p we have:{var n: int; {s 1 } n ; loop n {s 2 } z } z ⋆ = let n = {s 1 } n ⋆ in let z = rec(n, z , λz.λy.{s 2 } z ⋆ ) in z ։ rec({s 1 } n ⋆ , z , λy.λz.{s 2 } z ⋆ ) = I({s 1 } n ⋆ , z , λz.{s 2 } z ⋆ )

  t, u int ×(σ→ς) = λx: σ. t, (u x) int ×ς t, u (σ→ς)×τ = λx: σ. (t x), u ς ×τ π int ×(σ→ς)

  5 how to get almost the same program from the definition of ack in System T.

	proc (in m:int , n: int ; out r : int) {
	proc next (in y: int ; out p: int ) {
	p := y;
	inc(p);
	} p ;
	var g : proc (in int ; out int );
	g := next ;
	for i := 1 to m {
	cst h = g;
	proc aux (in y: int ; out p: int ) {
	h(1, p);
	for j := 1 to y {
	h(p; p);
	} p ;
	} p ;
	g := aux ;
	} g ;
	g(n, r );
	} r ;

C[t[S(v 1 )/x] rec(v 1 , v 2 , λx.t)] C[λ(x 1 , , x n ).t (v 1 , , v n )] C[t[v 1 /x 1 , , v n /x n ]] Figure 2.1. Gödel System T x: τ ∈ Γ Γ ⊢ x: τ (ident) Γ ⊢ 0: int (zero) Γ ⊢ t: int Γ ⊢ S(t): int (succ) Γ ⊢ t: int Γ ⊢ pred(t): int (pred) Γ ⊢ t 1 : τ 1 Γ ⊢ t n : τ n Γ ⊢ (t 1 , , t n ): τ 1 × × τ n (tuple) Γ, x 1 : τ 1 , , x n : τ n ⊢ t: σ Γ ⊢ λ(x 1 , , x n ).t : (τ 1 × × τ n ) → σ (abs) Γ ⊢ t 1 : σ → τ Γ ⊢ t 2 : σ Γ ⊢ t 1 t 2 : τ (app) Γ ⊢ t 1 : int Γ ⊢ t 2 : τ Γ ⊢ t 3 : int → τ → τ Γ ⊢ rec(t 1 , t 2 , t 3 ): τ (rec)Figure 2.2. Functional type system

G ⋆ and then Ω ⋆ , x G : σ G ⋆ , z G : (τ G ′ ⋆ ) × = Ω ⋆ , x G : σ G ⋆ .We can then build the following typing derivation :Γ ⋆ , Ω ⋆ , x G : σ G ⋆ ⊢ p ⋆ : (τ G ⋆ ) × → (τ G ′ ⋆ ) × Γ ⋆ , Ω ⋆ , x G : σ G ⋆ ⊢ e G ⋆ : τ G ⋆ Γ ⋆ , Ω ⋆ , x G : σ G ⋆ ⊢ p ⋆ e G ⋆ : (τ G ′ ⋆ ) × Γ ⋆ , Ω ⋆ , x G : σ

Acknowledgments

We are grateful to Olivier Danvy for many fruitful discussions on the topics presented in this article and to Neil Jones for his early support. We also would like to thank the anonymous referees for their helpful comments.

Appendix A Ultimate Obstinacy

In this appendix, we show that (non-trivial) terms of System T are "ultimately obstinate" (this terminology is borrowed from [Colson, 1991]) even in the presence a one-step predecessor operation and product types. However, since the techniques developed in [START_REF] Colson | System T, call-by-value and the minimum problem[END_REF] do not seem to generalize easily to this case, we present here a direct proof of this result.

We first extend the syntax of terms and values with an infinite number of constants ⊥ i k of type N and we supplement our set of reduction rules with the following rule:

We denote by ⊥ this extended rewriting system. Intuitively, a constant ⊥ i k represents a "sufficiently large" natural number (on which the predecessor can be applied at least k times). The strong normalization of reduction ⊥ * for well-typed terms is a consequence of the following lemma (since the reduction is strongly normalizing for well-typed terms). /x 1 , , ⊥ n kn /x n ] for some terms t, u then t[0/x 1 , , 0/x n ] u[0/x 1 , , 0/x n ].

Since terms now possibly contain constants ⊥ i k of type N , even a well-typed term can get stuck during evaluation (the term cannot be evaluated further) although it is not yet a value. This lemma allows us to split the set of terms into constant, trivial and ultimately obstinate terms.

Lemma A.2. Given a well-typed term t of type N with free variables x 1 , , x n of type N, if t[⊥ 1 0 /x 1 , , ⊥ n 0 /x n ] ⊥ p v where v is in normal form then one of the following cases holds:

v is a value S k (0) (we say that t is "constant") v is a value S k (⊥ i m ) with m p (we say that t is "trivial")

)] and m p (we say that t is "ultimately obstinate") Proof. By inspection of normal forms (and then by induction on the derivation to show that m p).

Definition A.3. The S-substitution t S(⊥ i )/⊥ i is the homomorphic extension of the basic function defined as follows:

We write t S p (⊥ i )/⊥ i for the generalized S-substitution defined by induction on p with t S 0 (⊥ i )/⊥ i = t and t S p+1

Proof. Check that S-substitution commutes with the reduction rules given in Figure 2.1 and with the rule

].

The following lemma (together with Lemma A.1) allows us to apply Lemma A.2 on genuine natural numbers.

Lemma A.5. Given a well-typed term t with constants

Proof. Apply Lemma A.4 repeatedly p times for each ⊥ i .

Lemma A.6. (constant terms) Given a well-typed constant term t: N with free variables x 1 , , x n of type N, there exist k, p ∈ N such that for any p 1 0, , p n 0, t[S p1 (0)/ x 1 , , S pn (0)/x n ] p S k (0).

Lemma A.7. (trivial terms) Given a well-typed trivial term t: N with free variables x 1 , , x n of type N, there exist i, m, p, k with 1 i n and m p such that for any p 1 0, , p n 0, t[S p1 (0)/x 1 , , S pn (0)/x n ] p S pi -˙m+k (0).

x n ] and p, k, m be such that t ′ p S k (⊥ i m ) by Lemma A.2. By Lemma A.5,

we conclude by Lemma A.1 that t[S p1 (0)/x 1 , , S pn (0)/x n ] p S k (S pi -˙m(0)).

Remark A.8. Clearly, trivial terms compute only functions definable (with the usual mathematical notation) as (x 1 , , x n ) (x i -˙m) + k (for some constants m, k).

Lemma A.9. Given an evaluation context

Theorem A.10. (ultimately obstinate terms) Given an ultimately obstinate term t of type N with free variables x 1 , , x n of type N, there exist i, m ∈ N with 1 i n such that for any p 1 p, , p n p, t[S p1 (0)/x 1 , , S pn (0)/x n ] reaches its normal form in at least p i reductions steps.

)] by Lemma A.9 and we can conclude since p m and thus p + p im p i .

Appendix B Subject reduction for Loop ω

B.1 Substitution and renaming

Recall that renaming is only defined for mutable variables and that the imperative substitution is only defined for read-only variables. Since we consider commands up to α-conversion, we may assume that no variable capture can occur.

Definition B.1. The renaming meta-operation on commands, sequences and expressions, denoted respectively by c

= dec(y) Proof. By definition of store typing.

B.3 Proof of Theorem 3.18

Theorem 3.18. For any environment Ω and any state (c, µ), we have that

and dom(µ) = dom(µ ′ ).

Proof. By induction on the derivation of (c, µ) (c ′ , µ ′ ), and then by analysis of the typing derivation. • (s.inc): we have Ω ⊢ µ and y: int ∈ Ω ∅; Ω ⊢ inc(y): comm then we easily get Ω ⊢ µ and y: int ∈ Ω ∅; Ω ⊢ q + 1: int ∅; Ω ⊢ y 4 q + 1: comm • (s.dec): similar to above.

• (s.call): we have Ω ⊢ µ and

q + 1]: seq. We clearly have Ω ⊢ µ and the following rule is easily derivable:

Proof. By induction on e, s, and {s} x G .

• e = n ¯. We have:

Γ; Ω ⊢ n ¯: int and then

• e = y. We have: y: τ ∈ Γ, Ω Γ; Ω ⊢ y: τ and then

We build the following typing derivation:

G ⊢ s: seq is derivable, we obtain by induction hypothesis the required typing derivation

• s = ε. We have:

• s = var y: τ 4 e; s ′ with s ′ ε. We have:

• s = cst y = e; s ′ . We have:

We build then the following typing derivation :

• s = y 4 e; s ′ . We have:

We build then the following typing derivation :

• s = inc(y); s ′ . We have:

We can then build the following typing derivation :

• s = dec(y); s ′ . Similar to the previous case.

• s = p(e G ; z G ); s ′ . We have:

We can then build the following typing derivation :

. By induction hypothesis, we obtain Γ ⋆ , y: τ ⋆ , z G : τ G ′ ⋆ ⊢ {s ′ } z G ⋆ : (τ G ′ ⋆ ) × and Γ ⋆ , Ω ⋆ , x G : σ G ⋆ ⊢ e ⋆ : τ ⋆ and Γ ⋆ , Ω ⋆ , x G : σ G ⋆ ⊢ (s ′′ ) x G ⋆ : (σ G ⋆ ) × . We build then the following typing derivation :


Laurentiu Pasol
email: laurentiu.pasol@espci.fr

Xavier Chateau
email: xavier.chateau@lcpc.fr

André Zaoui

Elastic modulus of a colloidal suspension of rigid spheres at rest

Keywords: rheology, colloidal suspension, elastical modulus Mots-clés : rhéologie, suspension colloïdale, module d'élasticité

may come

Elastic modulus of a colloidal suspension of rigid spheres at rest

Laurentiu Pasol, Xavier Chateau

Introduction

The macroscopic rheological properties of a colloidal suspension are the counterpart at the macroscopic scale of phenomena occurring at the length scale of the particles. The forces applied to the particles originate from different phenomena: colloidal forces, hydrodynamic interactions, Brownian motions, etc. The intensity of these forces depends upon several parameters as the temperature, the size of the particles, the separation gap between particles, or the pH of the suspending fluid.

At the macroscopic scale, the elastic modulus is one of the parameters which characterize the suspension behavior. It has been recognized from a long time that its value depends in particular upon the interactions between particles. The problem of the transition from the microscale to the macroscale in view of the prediction of the macroscopic properties of the suspension has been the matter of intensive research for decades. The main underlying motivation for this work is to predict the overall behavior of the suspension from the description of the particles properties. Most of the results have been obtained in the framework of statistical physics. For example Zwanzig and Mountain computed the high frequency shear modulus of a simple monoatomic fluid where only binary interactions are likely to occur in the absence of Brownian motion and hydrodynamic forces [START_REF] Zwanzig | High-Frequency Elastic Moduli of Simple Fluids[END_REF]. Wagner generalized this results in order to account for Brownian motion and hydrodynamic interaction by means of a linear theory [START_REF] Wagner | The High-Frequency Shear Modulus of Colloidal Suspensions and the Effects of Hydrodynamic Interactions[END_REF]. He showed that Zwanzig and Mountain results are still valid when hydrodynamic interactions between particles are negligible. For concentrated suspensions Lionberger and Russel showed that long-range hydrodynamic interactions can be neglected, the main contribution coming from the lubrification forces [START_REF] Lionberger | High frequency modulus of hard spher colloids[END_REF]. Brady developed in [START_REF] Brady | The rheological behavior of concentrated colloidal dispersions[END_REF] a theory accounting for specific interparticle force laws and their influence on the suspension rheology in the linear regime in the framework of a mechanical approach. Divergence of the viscosity at random close packing density was recovered and the value of the exponent is predicted as a function of the interparticles forces (Brownian hard spheres or particle interacting through strongly repulsive colloidal forces).

The difficulty encounted to experimentally measure colloidal forces also motivated interest in this field, mainly for elasticity. The idea is to use theoretical results obtained in the framework of change of scale methods in order to determine microscopic properties of the suspension from the measurement of macroscopic elastic modulus. Such a method was proposed in [START_REF] Bergenholtz | Colloidal charge determination in concentrated liquid dispersions using torsional resonance oscillation[END_REF] to estimate the effective surface charge of particles of a concentrated suspension from the measurement of the high-frequency elastic modulus.

In most of these works, the suspension is modeled as a fluid. From a practical point a view, it is well known that concentrated colloidal suspensions often exhibit a yield stress: they flow and behave like a fluid only when submitted to a stress above the yield stress. Otherwise, the behave like a solid. In the solid state, a colloidal suspension can be seen as a disordered solid in which the particles form a connected network. As long as the applied forces are not big enough to trigger off finite displacement of the particles from their rest position, the overall mechanical properties of the suspension can be predicted in the framework of change of scale methods pertaining to heterogeneous solid materials.

In this paper, we show that it is possible to perform such approach in order to estimate elastic modulus for a colloidal suspension. For simplicity, we restrict ourselves to the situations where hydrodynamic interactions and Brownian motions are neglected. As a consequence, our results are valid only for naughtvelocity loading in the solid regime (quasistatic elastic behavior) or hight-frequency loading in the fluid regime.

The paper is organized as follows. We begin by recalling the relation linking the Cauchy stress tensor to the interaction force. Then, we compute the macroscopic strain-stress behavior law in the linear regime. Finally, a new estimate for the elastic shear modulus of the suspension is obtained before we conclude.

Cauchy tensor for a colloidal suspension at rest

We consider a monodiperse suspension of spherical particles with radius a distributed in an incompressible Newtonian fluid. Particles interact through colloidal interaction forces. The suspension is at rest both at the microscopic and the macroscopic scales, so that hydrodynamic interaction forces are negligible. It is assumed that no forces from outside are applied on the particles or on the fluid.

Consider a representative elementary volume (r.e.v.) of the suspension occupying the geometrical domain V and containing N particles (N ≫ 1). The macroscopic Cauchy stress tensor σ can be computed from the knowledge of the microscopic quantities using the classical Batchelor equation [START_REF] Batchelor | The stress system in a suspension of force-free particles[END_REF][START_REF] Batchelor | The effect of brownian motion on the bulk stress in a suspension of spherical particles[END_REF]:

σ = 1 V V σdV = - 1 V V f pδdV + 1 V N i=1 s i (1)
where p denotes the fluid pressure, δ the second order unit tensor, V f the geometrical domain filled by the fluid and s i the stresslet of the particle i, equal to

s i = 1 2 Ai (σ • n ⊗ (x -x i ) + (x -x i ) ⊗ σ • n) dS = Ai (x -x i ) ⊗ σ • ndS (2)
with σ, the cauchy stress tensor field in the particles, x i the center of particle i and A i the boundary of the domain occupied by the particle i. In equation 2, n denotes the outer unit normal to the domain A i and x the position vector in the studied configuration.

We consider only stable colloidal dispersions where interaction forces dominate Brownian effects. Then the particles form a disordered network. The only contribution of particle i to the stress tensor is the stresslet s i . Thanks to the assumption that no external forces apply on the particles, the strain tensor σ is symmetric and so is the macroscopic Cauchy stress tensor. Furthermore, the fluid pressure is uniform over the domain occupied by the fluid in the representative elementary volume. As it is classical, it is assumed that interparticle forces derive from a potential [START_REF] Russel | Colloidal Dispersions[END_REF]. Then, F j→i , the force applied by particle j to particle i reads F j→i = -∂ψ ∂xi (x ij ) where x ij = x jx i denotes the vector connecting the center of particle i to the center of particle j. It is advisable to note here that when the interparticle forces are described by force vectors, the Batchelor's equation 1 is no more valid. Putting the equilibrium equation for both the whole r.e.v. and each particle in equation 1 allows to compute the macroscopic Cauchy stress tensor as a function of the interparticle forces and the fluid pressure [START_REF] Batchelor | The effect of brownian motion on the bulk stress in a suspension of spherical particles[END_REF][START_REF] Russel | Colloidal Dispersions[END_REF][START_REF] Chateau | Micromechanics of unsaturated granular media[END_REF]

σ = -pδ - 1 V N i<j F i→j ⊗ x ij (3)
This relation can also be obtained in the framework of a micromechanical approach to the behavior of a heterogeneous material [10]. It is recalled that mechanical homogenization techniques aim at finding the overall behavior of a system in a form of relationship between macroscopic stress and strain tensors from the response of the r.e.v. to a mechanical loading in which one of the two macroscopic tensors acts like a loading parameter. As the mechanical behavior of the suspension does not depend on the value of the fluid pressure, it is assumed that p is naught in the sequel.

Of course, one has to consider an arbitrary realization of the material system to compute the equation 3. In order to obtain results which do not depend on the particular selected realization, it is necessary to average the equation 3 over all the possible realizations of the system. Let C N = {x 1 , x 2 , ..., x N } denotes a particular realization for the centers of the N particles embedded in the r.e.v. and let P N (x 1 , x 2 , ..., x N ) denotes the probability of finding simultaneously the particle centers in x 1 , x 2 , ..., x N . As the particles are indistinguishable the probability to find simultaneously the center of one particle in x 1 and the center of another particle in x 2 reads

p 2 (x 1 , x 2 ) = 1 (N -2)! V N -2 P N (C N )dx 3 . . . dx N = n 2 g(r) (4)
where r = x 1x 2 and n = N/V denotes the number density of particles in the representative elementary volume. The second equality of equation 4 is only valid for statistically homogeneous suspensions. It is assumed that this condition is fulfilled in the sequel. g is the the radial distribution function [START_REF] Hansen | Theory of simple liquids[END_REF].

Averaging the stress tensor equation 3 with the probability p 2 (x 1 , x 2 ) defined by 4 yields

< σ >= - n 2 2 V r ⊗ F (r) g(r) dV (r) (5)
where the convention F (r) = F 2→1 (r) has be used to simplify the notations.

Elastic modulus

In order to identify the tangent moduli of the suspension, a macroscopic linearized strain ε is applied to the representative elementary volume occupying the geometrical domain V 0 in the undeformed configuration. A particle located at X i in the reference configuration moves to the position x i in the deformed configuration. Such a macroscopic loading can be defined by the so-called Hashin boundary condition according to which the displacement of particles located on the boundary of the r.e.v. is prescribed, equal to ε•X i . As the particles are rigid, the macroscopic loading must comply with the incompressibility condition δ : ε = 0. It is worth noting that for each realization of the suspension, local material heterogeneities are responsible for microscopic fluctuations of the displacement around the linear field ε • X.

Up to the first order in ε, the Cauchy stress tensor on the deformed configuration reads

< σ >=< π 0 > - n 2 2 V0 R ⊗ F dg 0 dR • A : ε + A : ε ⊗ F + R ⊗ dF dR • A : ε g 0 dV (6)
with

< π 0 >= - n 2 2 V0 R ⊗ F (R) g 0 (R) dV (7)
π 0 denotes the Piola-Kirchhoff stress tensor on the underformed configuration [START_REF] Germain | Cours de mécanique des milieux continus[END_REF][START_REF] Salençon | Handbook of continuum mechanics. General concepts[END_REF]. < π 0 > is equal to the Cauchy stress tensor in the undeformed configuration. It is worth noting that quantities F , g 0 and A are function of the position vector R (the dependence have been omitted for simplicity). The relative displacement concentration tensor defined by A(R) = dR/dε allows to compute the relative displacement r -R = x 2x 1 -(X 2 -X 1 ) of two particles induced by the loading ε.

Explicitly knowing the third order tensor A(R) would allow to compute the behavior law linking the Cauchy stress tensor to the linearized strain tensor ε. It is assumed in the sequel that the behavior of the suspension is linear elastic at the macroscopic scale. Then, the macroscopic state law reads [START_REF] Salençon | Handbook of continuum mechanics. General concepts[END_REF]

σ = π 0 + ε • π 0 + π 0 • ε + C : ε = π 0 + L(π 0 ) : ε (8)
where L(π 0 ) denotes the tangent tensor and C the elastic tensor. It is recalled that the tensor L(π 0 ) is generally not equal to the elastic tensor C and does not satisfy the classical property of definite positivity [START_REF] Salençon | Handbook of continuum mechanics. General concepts[END_REF]. Comparing equation 6 with the second egality 8 allows to compute L.

L = - n 2 2 V0 R ⊗ F ⊗ dg 0 dR • A + g 0 R ⊗ dF dR • A + F ⊗ 1↔2 A dV (9)
with F ⊗ 1↔2 A = F j A ikℓ e i ⊗e j ⊗e k ⊗e ℓ . The elastic tensor C can be easily computed by combinig equations 8 and 9.

In the sequel, it is assumed that the suspension is isotropic in the undeformed configuration. Then the radial distribution function reads g 0 (R) = g 0 (|R|) = g 0 (R). Moreover, it is also assumed that the interparticle forces are central, which writes ψ(R) = ψ(R). The interparticle forces read

F = - 1 R dψ dR R (10)
Putting equation 10 into expression 5 yields the value of the stress tensor in the undeformed configuration

< π 0 >= 2π 3 n 2 ∞ R=2a R 3 dψ(R) dR g 0 (R)dR δ (11)
In equation 11, it was assumed that R is unbounded whereas one would expect that the r.e.v. is of finite extent. Insofar as the r.e.v. must be large enough to be of typical composition and that its overall properties do not depend ont its size, the macroscopic behavior of the suspension can be defined only if the decay of the interparticle forces for large R is strong enough that the contribution of long range forces is negligible. When these conditions are fulfilled, it is possible to simplify the computation of quantities defined as an average over the r.e.v. by assuming that the r.e.v. is unbounded. The same truncature process is used in the sequel of the paper. As the stress tensor in the reference configuration is isotropic, the internal force is characterized by a pressure, equal (up to the fluctuation term nk B T ) to the osmotic pressure of a colloidal system classically defined in the framework of statistical mechanics [START_REF] Russel | Colloidal Dispersions[END_REF]. Thanks to the fact that the initial configuration is isotropic and the interparticle forces are central, we obtain

dg 0 dR = 1 R dg 0 dR R (12)
The tensor field A depends upon the morphological properties of the suspension in the undeformed configuration. As it is not possible to compute A from a practical point of view, we purpose to compute the overall properties of the suspension using the classical choice ∀R, A(R) : ε = ε • R leading to the popular "mean field theory". Using this particular localization field allows to obtain only estimates of the overall properties of the suspension because this choice defines the solution of the problem under consideration only in particular situation (uniform radial distribution function, periodic lattice, . . . ) Combining this estimate with the relations 6, 12 and the incompressibility condition ε : δ = 0 yields the following behavior law of the suspension

< τ >= 2G s ε, with G s = 3φ 2 40πa 6 ∞ R=2a d dR R 4 dψ dR (X)g 0 (R) dR (13)
where φ = n4πa 3 /3 denotes the volumic fraction and τ = σ -(δ : σ)/3δ the deviatoric part of the Cauchy stress tensor. It can be shown that the "solid modulus" 13 is no more than the classical Voigt estimate one can obtain using the uniform strain field as a trial field in a variational approch to the problem under consideration. Then, equation 13 defines an upper bound of the real solid shear modulus of the suspension.

It is reminded that classically, the actual configuration is taken as the reference configuration to compute the elastic moduli tensor [START_REF] Wagner | The High-Frequency Shear Modulus of Colloidal Suspensions and the Effects of Hydrodynamic Interactions[END_REF]. This result can be recovered by performing exactly the same computations than above on the undeformed configuration. This approach yields the "liquid" elastic shear estimate

< τ >= 2G ℓ ε, with G ℓ = 3φ 2 40πa 6 ∞ R=2a d dR R 4 dψ dR (R) g 0 (R)dR (14)
The difference between the two estimates comes from the fact that the radial distribution function is derived with respect to R in equation 13 and not in equation 14. It is possible to obtain the "liquid" estimate from the "solid" one by assuming the radial distribution function conservation in the course of deformation. Then, it is shown from equation 6 that, up to the first order of ε, the Cauchy stress tensor reads

< σ >=< π 0 > - n 2 2 V0 d [R ⊗ F ] dε : ε g 0 (R)dV (R) (15)
(it is always assumed that the material is incompressible). Considering one more time that the suspension is isotropic in the reference configuration, one readily obtains from equation 15 the estimate 14 for the elastic shear modulus of the suspension in the framework of a mean field theory.

Conclusions

We have obtained a new expression for the elastic shear modulus of a colloidal suspension modeled as a solid. This expression allows to estimate the elastic modulus of a yield stress suspension submitted to a load smaller than the yield stress. This result was obtained in the framework of an homogenization approach to the behavior of a colloidal suspension considered as a discrete solid medium. Even if this approach relies on assumptions rather different from those classically performed to obtain estimates for the overall properties of suspensions in the framework of statistical mechanics, it is worth noting that classical results can also be recovered. Thus, we have shown that our estimate coincides with the classical high-frequency modulus estimate when the actual configuration is taken as the reference. From our point of view, this result was recovered by modeling the suspension as a "liquid", ie a suspension without a yield stress. In this situation, it is not possible to define an "undeformed" configuration and the actual configuration is taken as the reference. To our opinion, this similarity is a strong indication that both approaches are consistent one to the other.

Furthermore, it has been recalled that the tangent modulus is not equal to the elastic modulus when the stress applied to the material in the reference configuration and the elastic modulus are of the same order of magnitude.

LMSGC de l'Institut Navier (Université Paris Est) is UMR 113 of the CNRS associated with the ENPC and the LCPC.

Support from the Agence Nationale de la Recherche (ANR) is acknowledged (grant ANR-05-JCJC-0214).


Abdelhamid Belghit
email: abelghit@univ-lr.fr

Abdelhamid Belghit Heat Transfer

Prof A Belghit

HEAT TRANSFER BY SIMULTANEOUS RADIATION-CONDUCTION AND CONVECTION IN A HIGH TEMPERATURE PACKED BED

Keywords: Radiative, Transfer, packed bed, Case

établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

The gasification of coal is a very important economical operation. It is performed at relatively high temperatures, between 700°C and 1300°C. The produced gas, consisting primarily of CO and H 2 , can be used as a feedstock for many chemical processes (Gregg et al. [START_REF] Gregg | Lawrence Livermore Laboratory[END_REF], Aiman et al. [START_REF] Aiman | UCRL prepint 84610[END_REF], Taylor et al. [START_REF] Taylor | [END_REF], Belghit et al. [4]).

A moving bed reactor, for gasifying coconut charcoal with CO 2 was experimentally studied (Taylor et al. [START_REF] Taylor | [END_REF], Belghit et al. [5]). Experiments were carried out on a vertical solar furnace ( Fig. 1).

Any serious technical evaluation of this process schould be based on a rigorous and precise functioning model of the gasification reactor. Belghit et al. [4], presented a numerical model for the moving bed pertinent to the case where the total rate is determined by mass transfer control, Rosseland's approximation was utilised for analysis the radiative transfer.

In the present paper, we propose a rigorous model for the behaviour of the reactor in mixed control, which explicitly takes in to account the radiative exchange in the porous medium. Case's normal-mode expansion technique [START_REF] Özisik | Radiative transfer, and interaction with conduction and convection[END_REF] is used to obtain solutions to the radiative transfer problem for the packed bed. The comparison between the radiative heat transfer and the exchanges by conduction and forced convection is analysed.

Analysis

The heat and mass transfer equations for porous medium are written on a macroscale. Therefore, its geometry is caracterized by parameters such as porosity ε and contact surface ratio: A=6(1-ε)/d for solid (carbon) particles supposed spherical and pure. The gasification reaction is:

C + CO 2 → 2CO ET81-2
To simplify the heat and mass transfer equations (Luikov [7], Szekely et al. [START_REF] Szekely | Gas-Solid Reactions[END_REF]), it is assumed that the flow rate is fully established, the side effect is negligible in the reactor considered as a straight cylinder with a constant section, the reactor is considered adiabatic and composed of a stack of identical and spherical nonporous carbon particles. In addition the flow is assumed one-dimensional, this effect being confirmed for (D o /d)>8. The gas is taken as ideal. Moreover, the viscous friction can be neglected compared with other exchange modes (conduction, radiation and forced convection). The heat transfer equations are given by [START_REF] Belghit | [END_REF]:

-for the gas:

θ σ θ λ θ ρ + ∂ ∂ ∂ ∂ = ∂ ∂ ) ( X X X v c p (1)
-for the solid:

0 ) ( ) ( * = + ∂ Τ ∂ - ∂ ∂ - ∂ Τ ∂ ∂ ∂ Τ σ ρ λ X v c X X Q X X s pc c r s (2)
In these equations, the terms θ σ , represent heat production (convection) and σ T represent heat (convection) and masse production (diffusion and chemical reaction), in the control volume. They may be expressed as:

) ( ) 1 ( 6 ) ( θ ε ε θ ε σ θ - Τ - = - Τ = h d h A , ) ( ) 1 ( 6 ) ( 6 ) ( 2 s CO C C x kg H d h d s - + ∆ - - Τ - = Τ θ σ
The energy equation for solid includes the net radiative heat flux density Q r (τ) which is related to the intensity L(τ, µ) by:

∫ - Τ = 1 1 ) , ( 2 ) ( µ µ τ π τ d L Q (3)
where L(τ, µ) satisfies the equation of radiation transfer.

Equation of radiative transfer

The equation of radiative transfer for one-dimensional, emitting, absorbing, isotropically scattering, gray media can be written in the form:

∫ - + Τ - = + ∂ ∂ 1 1 4 2 ' ) ' , ( 2
) ( ' ) 1 ( ) , ( ) , ( µ µ τ ω π τ σ ω µ τ τ µ τ µ d L n L L (4)
With the boundary conditions:

i F o L φ µ = ′ = 0 ) , ( µ>0 for τ=0 (5) ET81-3 ) , ( ) , ( µ µ - ∞ = - ∞ p L L µ>0 for τ ∞ → (6)
The solution of equation ( 4) can be written in the form [10]:

∫ + + = - - 1 0 0 0 ) , ( ) , ( ) ( ) , ( ) ( ) , ( 0 µ τ µ φ µ φ µ τ τ τ p n n L dn e n n A e n n A L (7)
where A(n 0 ) and A(n), n∈[0,1] are the expansion coefficients, L p (τ, µ) is a particular solution of equation ( 4), and φ(-n 0 ,µ) and φ(-n,µ) are the normal modes

[ ] µ µ µ φ µ d o L F n W n N n A p ) , ( ) , ( ) ( ) ( 1 ) ( 0 0 1 0 0 0 - ′ - = ∫ { } µ µ µ φ µ d o L F n W n N n w n n A p ) , ( ) , ( ) ( ) ( ) ( ) ( 0 1 0 - ′ =

∫

The expansion coefficients A(n 0 ) and A(n) can be determined by constaining the solution equation [START_REF] Luikov | Heat and Mass Transfer[END_REF] to meet the boundary conditions equations ( 5) and ( 6), and by utilizing the orthogonality property of the normal modes and various normalisation integrals as described in reference [10] provided that a particular solution L p (τ, µ) is available. To determine a particular solution it is assumed that the inhomogeneous term is represented as a polynomial in t in the form [START_REF] Radhouani | [END_REF]:

∑ = + - = Τ N m m m e 0 ) ( 4 ) ( π τ α τ
and that the coefficients α m are determined by the method of Gauss-Seidel. Noting a that a particular solution L p (τ, µ) for an inhomogeneous term of the form T 4 (τ) is given as [13]:

∑ = + - - + + ′ - = M m m m p m D m e m n L 0 ) ( 2 ) ( ) ( ) ( ) 1 ( ) , ( µ π π α π σ ω µ τ π τ
with: D(m) = 1-ω(m+π)th -1 (1/(m+π)). Then we have: 1+m)DS(m). Then, we obtain:

      + + ′ - - = ∑ = ) ( ) ( ) ( ) 1 ( ) 2 ( ) ( 1 ) ( ) 2 ( ) 1 ( 0 2 ' 0 0 0 0 m DS m DP m D n F n n N n A m m M m m γ α γ α α π σ ω ω    + - + -    + - + + ′ - - = ∑ = 2 0 ) 1 ( ) 1 ( 0 ) 2 ( 0 ) 1 ( 0 2 ' 0 ( ) ( ) ( ) ( ) ( ) 1 ( ) 2 ( ) ( ) ( ) ( n n n n n m DS n n m DP m D n F n n N n W n n A m m M m m γ γ γ α γ α α π σ ω ω with: DS(m) = (1+m)D(m) et DP(m) = (
-The intensity of radiation

dn e n n A e n n A L n n ∫ - - + = 1 0 0 0 ) , ( ) ( ) , ( ) ( ) , ( 0 τ τ µ φ µ φ µ τ ) ( ) ) ( 1 ) 1 ( ) ( 0 2 2 m D e m m n m m M m π τ α π µ π µ π σ ω + - = ∑       + + + + ′ - + (8)
-The net radiation flux:

∫ - - + - -      - = 1 0 0 0 0 0 ) ( ) ( ) ( ) 1 ( 2 ) ( 0 0 dn e n nA n e n A n e n A n Q n n r τ π τ ω π τ ∑ ∫ = + -      ′ + - - m m m m n m DP e n dn e n nA 0 ) ( 1 0 2 ) ( 3 2 ) ( π τ τ α π σ (9)
Then dQ r (τ)/dτ can be obtained by differentiating expression for Q r (τ) with respect to τ :

          ′ + + - - = ∑ ∫ = + - - - M m m m n n r m DS e n dn e n A e n A d dQ 0 ) ( 2 1 0 0 ) ( 3 2 ) ( ) ( ) 1 ( 2 ) ( 0 π τ τ α π σ ω π τ τ where τ is : x d X ′ = ∫ 0 τ
, and X is the axial coordinate.

The set of equations ( 1) and ( 2) may be written as:

) ( ) 1 ( 6 ) ( θ ε ε θ λ θ ρ - Τ - + ∂ ∂ ∂ ∂ = ∂ h d X X dX v c p (10) ) ( ) 1 ( 6 ) ( 6 ) ( ) ( 2 s co g s pc c s C C x d Hk h d X v c X X s - + ∆ + - Τ + ∂ Τ ∂ = ∂ Τ ∂ ∂ ∂ * θ ρ λ           ′ + + - - ∑ ∫ = + - - - M m m X m n X n X m DS e n dn e n A e n A 0 ) ( 2 1 0 0 ) ( 3 2 ) ( ) ( ) 1 ( 2 0 π α π σ ω π (11)
-Boundary conditions [START_REF] Belghit | [END_REF]:

-At: X = 0: therefore an energy balance on the front (X=0) gives

0 4 0 4 0 ) ( X S s g i g i g ∂ Τ ∂ - - Τ = = Φ * λ θ σ ε φ α α (12)
0 1 = ∂ ∂ = ∂ ∂ = ∂ ∂ = ∂ ∂ = ∂ Τ ∂ X v X C X C X X θ ( 15
)
The value of the total emissivity ε g is determined by the correlation for (Borodulya et al [14]) :

ε g = ε P 0.
485 which is valid when the porosity is about 0.4; ε p is the emissivity of the material in the solid state.

With the hypothesis that a thermodynamic equilibrium exists, it becomes : α g = ε g .

Parameters:

Heat and mass transfer coefficients Heat and mass transfer coefficients h and k g are evaluated by empirical correlation's to Nusselt and Sherwood numbers (Gunn [15]), for 0.35≤ε≤1 and Re≤10 5 : Nu = (7 -10ε + 5ε 2 )(1 + 0.7 Re 0.2 Pr 1/3 ) + (1.33 -2.4ε + 1.2ε 2 )Re 0.7 Pr 1/3 Sh = (7 -10ε + 5ε 2 )(1 + 0.7 Re 0.2 c1 /3 ) + (1.33 -2.4ε + 1.2ε 2 )Re 0.7 Sc 1/3

Effective thermal conductivity of the packed bed

To calculate the effective thermal conductivity of the packed bed, the correlation is used [16]: β and φ are parameters which depend on the geometric characteristics of porous medium; β a is function of the particles arrangement and varies between 0.9 and 1; 0.9 corresponds to a close arrangement and 1 to a lose one.

ET81-5 ) 1 ( ) 1 (
φ is given as : φ = 6.486 10 -1 -0.417 10 -1 (λ s /λ) + 1.585 10 -3 (λ s /λ) 2 -0.285 10 -4 (λ s /λ) 3 + 0.238 10 -6 (λ s /λ) 4 -0.752 10 -9 (λ s /λ) 5

Numerical methods

The system of coupled and non linear differential equations (10)[START_REF] Case | Linear Transport Theory[END_REF] with the imposed boundary conditions [START_REF] Radhouani | [END_REF](13)(14)(15), are solved by using primarily the control volume method of (Patankar [START_REF] Patankar | Numerical Heat Transfer and Fluid Flow[END_REF]), for the energy equations. The system of algebraic equations obtained after discretization of the different model equations, all with a tridiagonal matrix, are solved by the Thomas's algorithm (Patankar [17]) , using and under-relaxation process for the prime model variables. A stability study leads to ∆X + = ∆X/L =0.005 corresponding to a spacestep of 1mm (L = 200mm) and to under-relaxation coefficients as follow: the temperature of the solid: 0.22.

The precision of the calculations is equal to 10 -4.

Results

The proposed theoretical model allows the determination of gas and solid characteristics along the reactor, both of which depend on the physical properties of the fluid and the radiative and physical properties of the solid.

Temperature profiles

Fig. 2 shows the dimensionless temperature profiles in the gas and solid (T + =T/θ 0 ; θ + =θ/θ 0 ) as a function of the dimensionless distance X + =X/L from the warm front of the reactor with the following parameters: φ i = 1000W, θ 0 =300K, d L = 0.001m, v 0 = 0.08m/s, ε = 0.45, L = 0.2m, K = 1820 m -1 , L = 0.2 m. Fig. 2. Temperature distributions for the gas and the solid along the packed bed, T + = T/θ 0 ; θ + = θ/θ 0 ET81-6 It is noted that there are two temperature zones: the first corresponds to the heating of gas by the porous medium exposed to concentrated external incident radiation, and the second to an equilibrium thermal zone between the gas and solid phases.

In the solid, the temperature gradient is very high because the effective thermal conductivity of the porous bed is low (λ s *=0.3 W/m.K) and also due to the radiative transfer influence.

Analysis of heat transfer a) Evolution of dimensionless numbers

To illustrate the different heat and mass exchanges, we represent in Fig. 3 the evolution of dimensionless numbers: Re, Pr, Sc, Nu et Sh. We note that prandtl number remains nearly constant and varies in the interval of 0.788 to 0.636. the Nusselt and Sherwood numbers persuit the same evolution between 4.6 and 6, but the Reynolds number varies from a value near 0 to 0.9. where K (m -1 ) is the extinction coefficient per unit volume of the packed bed.

The interaction between these modes of transfer is evaluated by defining a parameter which is a function of the two conductivities, known as the conduction-to-radiation parameter and expressed as:

3 * ' 4 Τ = n K N s σ λ
A value of N = 0.79 is found when the average control parameters are: φ i = 1000W, v 0 = 0.08 m/s, d L = 0.001 m, K = 1820 m -1 ,n' = 1, L = 0.2 m, θ 0 = 300K. Doornink and herring [START_REF] Doornink | [END_REF], showed that for N≤5, radiative heat his implied the coupling of these two energy exchange modes in current model.

Fig. 1 .

 1 Fig. 1. Packed bed reactor for solar gasification.

Fig 3 .

 3 Fig 3. Dimensionless variables profiles (Nu, Re, Sh, pr and Sch).b) Interaction radiation-conductionTo know the contribution of all heat transfer modes taking place in the reactor, in the domain of high temperatures, we have tried to determine then by calculating the flux densities of radiation Q r , conduction Q od and convection Q cv . If convective transfer is characterized by the coefficient h and conduction transfer in the packed bed by an effective thermal conductivity λ s *, radiative transfer may also be characterized by a radiative conductivity: K r

7 --

 7 c) Evolution of heat flux densities-The net radiative heat flux Q r : is given by expression (9); ET81-The conductive heat flux : is given by Fourier's law : The convective heat flux : Qcv = P.cp.v.TThe figure4shows the evolution of these parameters. We note the importance of radiative transfer in comparison with the other modes of heat transfer. The flux density Q r decreases slowly from 1.033 10 6 to 8.145 10 5 W .m -2 . For the conductive flux density, we note especially a of its value besides the hot surface (at X = 0). This fact explains the greet value of the temperature gradient observed near this one in Fig.2. We note a significant increase of the convective flux density from 3.64 10 4 to 4.798 10 4 W.m -2 . This phenomenon is explained by the creation CO during the reaction whose overall degree of conversion of carbon is relatively high.

  Fig 4.Fig.5

Fig 4 .Fig 5 .λ 2 µ 3 σ 4 τ

 45234 Fig 4. Heat flux density (Q r , Q cd and Q cv ) profiles along the packed bed Fig 5. Ratios of heat flux density profiles: Q r /Q cd et (2) : Q r /Q cv