M G Colucci

D P Van Der Werf

M Charlton
email: m.charlton@swansea.ac.uk

The Temperature and Density Dependence of Positron Annihilation in CO 2 and SF 6

Keywords: numbers: 34.85.+x, 34.50.Ez, 34.90.+q, 78.70.Bj

Positron lifetime experiments have been performed on CO 2 and SF 6 gases at temperatures in the range 297-400 K and at densities up to 10 amagat. The ensemble-averaged Z eff parameter has been extracted at each temperature from the observed density dependence of the annihilation rates. The latter was found to be consistent with annihilation via positron interactions both with single molecules and with pairs. The three-body (positron-plus-two molecules) annihilation coefficient, b, has also been obtained at each temperature. Both Z eff and b are found to be approximately independent of temperature in the range investigated. A simple threebody collision model for b is developed and discussed.

Introduction

The interactions of positrons in various media have been of interest for many years, and positron annihilation spectroscopies have found use as probes of, for instance, local electronic or defect densities in condensed matter and materials science (see e.g. [START_REF] Coleman | Positron Beams and their Applications[END_REF][START_REF] Dupasquier | Positron Spectroscopy of Solids[END_REF][START_REF] Surko | New Directions in Antimatter Chemistry and Physics[END_REF]). However, interest in the fundamental behaviour of positrons in gaseous systems continues to be high, and in particular there is much current activity concerning annihilation in molecular gases. At low gas densities the mean positron annihilation rate, λ e , is expected to vary with the temperature and density of the gas and is usually written [START_REF] Charlton | Positron Physics[END_REF] in terms of the (temperature-dependent) parameter, Z eff , the effective number of electrons available to the positron for annihilation, as

λ e = πr 2 0 cnZ eff . (1)
Here r 0 is the classical radius of the electron, c is the speed of light, n is the number density of gas atoms or molecules and πr 2 0 c/v is the Dirac free positron-electron annihilation cross section, with v the positron speed. The brackets denote an ensemble average over the positron energy distribution, which here will be characteristic of the temperature of the gas.

It has been known from early studies of positron annihilation in molecular gases (see e.g. [START_REF] Paul | [END_REF]6]) that for some molecular species (e.g. hydrocarbons and some of their derivatives) Z eff exceeds the actual number of molecular electrons, Z, by orders of magnitude. More recently, work done under single collision conditions using a positron accumulator, and a narrow energy width beam of positrons derived from it, has identified the presence of resonant features in the annihilation cross sections at low energies which are responsible for the high values of Z eff [7,8]. Some of this work has recently been reviewed [9,10], with [10] including a comprehensive discussion of theoretical models of the annihilation process in high Z eff species [11,12].

Intriguing features are also to be found in the behaviour of positrons in dense gases, typically at densities of the order of 1 amagat (= 2.69 × 10 25 m -3 ) or greater. In particular, the presence of three-body effects has recently been isolated in positronmolecule annihilation in a selection of species at room temperature [13,14]. In [14] it was argued that the three-body process may proceed via a reaction of the type,

e + + M + M → e + MM * → 2γ + M + + M, ( 2
)
where M is a molecule, by analogy with the two-body process,

e + + M → e + M * → 2γ + M + . (3)
For these reactions the intermediate complexes, e + M * and e + MM * are thought to form in those cases for which Z eff Z, which involve temporary binding of the positron to the molecular system. The star in these cases denotes some internal excitation of the complex, since the kinetic energy of the positron must be momentarily distributed therein. Clearly in these instances, annihilation is in competition with break-up of the complex into its original constituents. In Z eff Z species, there are two contributions to the annihilation cross section, so-called resonant and direct [11,12]. The latter will occur for all molecules, irrespective of whether intermediate complexes are formed, but the former, which completely dominates in many cases, must involve temporary resonant attachment.

There are many molecular systems, however, in which Z eff ≈ Z [START_REF] Charlton | Positron Physics[END_REF]6,15], but which still display a wealth of density and temperature-dependent features in their positron annihilation rates (see e.g. [15,16]). In particular, at temperatures below about twice the critical temperature of the gas, positrons can undergo annihilation in clusters of gas atoms or molecules. The clusters may pre-exist in the gas, or perhaps nucleate around the positron. In any case, annihilation rates are enhanced, and at very high densities tend to saturate. At high temperatures it has been found that the annihilation rates for several gases fell gradually below the linear rise predicted by equation [START_REF] Coleman | Positron Beams and their Applications[END_REF]. A binary collision model was developed to explain this behaviour [17], as will be discussed in section 3.

The main motivation for the work presented here was to extend the earlier study of Charlton and co-workers [14] to the species, CO 2 and SF 6 , but at several temperatures in the range 297-400 K. Our density range was restricted to be below ρ = 10 amagat. One aim was to benchmark the behaviour of the three-body annihilation reaction in gases without the added complication of resonant behaviour in the process; i.e. to study species for which Z eff ≈ Z.

We note, following [14], that assuming both reactions ( 2) and ( 3) can occur (with or without the intermediate complex) then the positron annihilation rate must be rewritten as,

λ e = aρ + bρ 2 = ωZ eff ρ + bρ 2 . ( 4
)
Here λ e is in units of µs -1 , with ρ the gas density in units of amagat, and the pre-factor ω = 0.201µ s -1 amagat -1 is the density-normalised Dirac rate for a free electron gas.

Fitting λ e yields the parameter Z eff , characteristic of the two-body e + -M interaction, and the three-body coefficient, b.

In this study we report the first systematic investigation of the temperature dependence of positron annihilation in molecular gases within the context of the threebody model. The remainder of this paper is organised as follows. Experimental details are presented in section 2, with results, discussion and comparisons to previous work given in section 3. Section 4 contains pertinent conclusions.

Experimental details

The positron lifetime spectrometer used was a conventional time-to-amplitudeconverter/multi-channel analyzer based system (see e.g. [START_REF] Charlton | Positron Physics[END_REF]). The positrons were derived from a 150 kBq 22 Na source sandwiched between two kapton foils of 10 µm thickness and mounted in a purpose-built holder in the centre of a gas chamber. The delayed coincidence between the nuclear gamma quantum, with an energy of 1.274 MeV (start signal), and one of the 0.511 MeV photons emitted in the annihilation of the positron (stop signal) was measured. The gamma rays were registered by two plastic scintillatorphotomultiplier tube arrangements located on either side of the chamber. The gas chamber consisted of a stainless steel cylinder, of inner diameter 35 mm and 210 mm in length, into which the sample gases could be admitted at pressures up to 10 atmospheres. For the measurements taken above room temperature the chamber was heated using insulated resistance heater wire wrapped directly around the chamber. The temperature of the outer chamber wall was measured using a thermocouple, and the chamber was allowed to stabilize for several hours following a change of temperature before a new run was started. It was found that the temperature was uniform to within ±5 • C across the cell. The gas pressure was recorded using a Druck PDCR 4010 pressure transducer. Gas densities were computed from the temperatures and pressures using accepted first order virial coefficient corrections [START_REF] Dymond | The Virial Coefficients of Gases -a Critical Compilation[END_REF].

In all cases the lifetime spectra contained a large prompt peak due to positron annihilations in the source holder and at the chamber wall. After this peak the events due to the positrons stopped in the gas could be fitted by two overlapping exponentials with a constant background. For the gases studied here, the faster of these two components was that due to the free positrons (the other was due to the annihilation of ortho-positronium atoms created during slowing down of the positrons in the gas), such that λ e could be extracted at each density/temperature.

Results and Discussion

Examples of the results for the positron annihilation rates in CO 2 and SF 6 at a temperature of 297 K are presented in Figure 1. The fitted lines are those corresponding to equation (4) which allowed values for Z eff and b to be obtained, as summarized in Table 1 for the two gases at each temperature.

The values for Z eff at 297 K are noticeably lower than the textbook values of 53 (CO 2 ) and 97 (SF 6 ) [START_REF] Charlton | Positron Physics[END_REF]15]. The older results were given without uncertainties, based upon previous work [START_REF] Heyland | [END_REF]20], and we note that the data from those experiments were not analyzed taking into account the possibility of three-body effects, which may have led to an overestimate of Z eff .

The values of Z eff and b/ω at the various gas temperatures show that there is no statistically significant variation in either parameter between 297 and 400 K. The present data exhibit similar phenomena to those of Heyland and co-workers [START_REF] Heyland | [END_REF], though the latter are only given in graphical form, and the region below 10 amagat was not studied in detail. The increase in Z eff apparent in the 350 K SF 6 data of [START_REF] Heyland | [END_REF] with respect to their data at lower temperatures is, however, not reproduced here. To the best of our knowledge, the only theoretical work for comparison is that of Gianturco and Mukherjee [21] for the case of CO 2 . These authors used their energy-dependent values for Z eff to compute Z eff for assumed thermal distributions at temperatures of relevance for this experiment. They found Z eff to vary little with temperature and to be ∼ 51, in reasonable accord with experiment.

As briefly mentioned in section 1, Heyland and co-workers [6,17] have provided an empirical model of the behaviour of a density-dependent Z eff , denoted as Z eff (ρ) to incorporate the density-dependent behaviour, in gases at high temperatures, typically more than twice the relevant critical temperature. They noted that data for several gases were of the form Z eff (ρ) = Z eff /(1 + βρ), with β a positive constant. Rearranging by writing λ e = ωρZ eff (ρ), it can be seen that 1/λ e = (1/ωρZ eff + 1/λ l ), where λ l = ωZ eff /β. The latter was interpreted as a limiting annihilation rate in the gas as ρ tended to infinity. This was further described using a binary model in which the probability of annihilation on collision was λ l δt, where δt is a mean duration of the collision. By defining the time between collisions as τ , the annihilation rate can be written as λ e = λ l δt/(τ + δt), such that 1/λ e = τ /(λ l δt + 1/λ l ), which is the same form as that empirically derived, as discussed above. Thus, the high temperature annihilation rate features can be adequately described in a binary-collision model, such that their physical origin is distinct from the many-body effects observed at lower temperatures. This includes the three-body phenomena which are of special concern here.

The positron annihilation rate may be affected by the presence of pre-existing weakly-bound pairs of molecules, as mentioned earlier. Certainly at higher densities and lower temperatures, positron annihilation in clusters is an established phenomenon [START_REF] Charlton | Positron Physics[END_REF]16,[START_REF] Heyland | [END_REF]22,23] for a variety of atomic and molecular species. Annihilation on preexisting clusters would be governed by the attractive van der Waals potential, which is related to the leading order virial coefficient correction for each gas. We have attempted to compare the size of the virial coefficient correction with the three-body annihilation rate, which is effectively a measure of the departure from the classic twobody annihilation relationship. In order to do this we have constructed the ratios (ρ -ρ id )/ρ and bρ 2 /λ e , where ρ id = 273.15P/T is the ideal gas density, with ρ id in amagats and P in atmospheres, at a temperature, T . Given the first order virial coefficient, B, and with ρ =

ρ id /(1 + BP ) it is clear that (ρ -ρ id ) ρ = -BP (5)
and

bρ 2 λ e = 1 + ωZ eff bρ -1 = 1 + ωZ eff T (1 + BP ) 273.15P b -1 . (6)
Using the derived values of b and Z eff from this study (Table 1) and tabulated values of B [START_REF] Dymond | The Virial Coefficients of Gases -a Critical Compilation[END_REF] it can be seen, even in our most extreme case (SF 6 at T = 297 K at a pressure of 10 atmospheres), that bρ 2 /λ e is around five times greater than (ρ -ρ id )/ρ: in most cases the former exceeds the latter by about a factor of ten. Thus, we conclude that the three-body effects we observe are predominantly a feature of the positron-gas interaction, and not a result of positron interactions with pre-existing molecular dimers.

We proceed by constructing a hypothetical three-body annihilation rate, λ 3b , from a two-body scattering rate, nσ t v (where σ t is a total scattering cross section), multiplied by the probability at a given density of having a further molecule within a volume r 3 3b of the positron-molecule system. The origin of the distance r 3b , which parameterises the strength of the interaction of the complex is unknown at present, such that it is added empirically. Given that the fraction of collisions that result in annihilation can be written in terms of an annihilation cross section, σ a , as σ a /σ t , λ 3b can be found as,

λ 3b = (nσ t v)(nr 3 3b )(σ a /σ t ) = n 2 σ a vr 3 3b (7)
By assuming σ a is given by the Dirac cross section (see section 1) multiplied by Z eff (i.e. σ a = πr 2 0 cZ eff /v) equation ( 7) becomes, λ 3b = n 2 πr 2 0 cZ eff r 3 3b .

Thus, the three-body coefficient can be identified as b = πr 2 0 cZ eff r 3 3b . As such, the temperature dependence of b, (and b/ω) should be that of Z eff r 3 3b . Since both Z eff and b have been found to be independent of temperature in the range we have explored, the implication is that r 3b must have a weak, if any, temperature dependence. The observations seem to preclude identifying r 3b as the positron de Broglie wavelength, which would introduce an extra T -1.5 effect. Using the experimental results for b, a value of r 3b ∼ 13 Åcan be derived for both CO 2 and SF 6 . This can be compared to the mean, ideal gas, inter-molecule spacing of 21/ρ 1/3 Å. Thus, the three-body model is expected to break down close to the maximum density we have investigated (around 10 amagat), and the effects of this have been observed previously (see e.g., [START_REF] Heyland | [END_REF]). The reason that, in our analysis, r 3b is the same for both gases is likely to be fortuitous, and is due to the assumption that Z eff can be used to construct λ 3b .

Gribakin [24] has also recently described three-body effects in gases with Z eff Z. His model assumes that the additional contribution to the annihilation in the positronmolecule complex (see equations ( 1) and ( 2)) arises due to collisional stabilization of the complex by a second molecule. An assumption is that b is approximately proportional to Z eff , such that the three-body effect acts upon the complex and is not an extra pathway to annihilation. This is in accord with the simple model given above.

In order to explore further the scaling behaviour of the three-body coefficient and Z eff , we have combined the room temperature data for CO 2 and SF 6 from this study with the room temperature values for a selection of Z eff Z gases from earlier work [13,14]. A log-log plot of b/ω versus Z eff is shown in Figure 2, where the gases have been grouped into two sets, namely those with Z eff ≈ Z and those where Z eff Z. The motivation for this is that the two-body annihilation mechanisms are quite different for the two classes, and involve temporary binding of the positron to the molecule for those with Z eff Z (see equation ( 3)). The lines fitted to the data have similar slopes, having an approximate behaviour as b/ω ∝ Z eff (1.5±0.1) , though there seems to be an offset, or jump, in b/ω between the two groups. The slope suggests a stronger dependence on Z eff than predicted from the two models described above.

Conclusions

We have presented measurements for the gases CO 2 and SF 6 at temperatures between 297 and 400 K of the parameters Z eff and b/ω which, respectively, characterize positron annihilation by two-and three-body mechanisms. Both parameters have been found to have no significant variation with temperature in the current range. A simple, empirical, three-body scattering model has been developed to yield an expression for b, though given present uncertainties in the data, no firm conclusions can be drawn as to its validity. A comparison of all available data for b/ω at room temperature has revealed that this parameter scales roughly as Z eff 1.5 , over a range of Z eff values from around 50 to 15000. The physical basis of this scaling is not understood and is contrary to the simple model developed herein. In addition, there is evidence of an offset in b/ω between those gases in which temporary binding of the positron to the molecule can occur, and the others. Both of these phenomena are worthy of further study, and data for more molecular species may be helpful. It would also be interesting to measure absolute values for the temperature dependencies of Z eff and the three-body coefficient for a range of gases with Z eff Z. In these cases annihilation via the intermediate state in equations ( 2) and (3), in which strong energy-dependent features are known to play a role [7,8,9,10,11,12], would be present. Such a study will be undertaken in our laboratory in the near future.

Figure 1 .

 1 Figure 1. The behaviour of the free positron annihilation rate versus gas density for SF 6 (•) and CO 2 ( ) at T = 297 K. The lines are the fits according to equation (4).

Figure 2 .

 2 Figure 2. Logarithmic plot of b/ω versus Z eff for a number of room temperature gases, as labelled. The fits to the two groups of molecules are explained in the text.

Table 1 .

 1 Values of Z eff and the three-body parameter for four different temperatures for CO 2 and SF 6 . (Here the three-body coefficient is given as b/ω, where ω is defined in the text.)

	T(K)	Z eff		b/ω (amagat -1 )
		CO 2	SF 6	CO 2	SF 6
	297	47.8±1.0	82.6±6.5	2.2±0.2	4.8±0.4
	320	46.5±0.8	75.1±5.0	2.1±0.1	4.0±0.8
	350	48.1±3.6	76.1±6.5	1.9±0.4	2.9±0.8
	400	46.0±1.6	74.8±2.7	2.1±0.2	3.4±0.6

Acknowledgments

The authors are grateful to the technical staff in the Department of Physics at Swansea for their help with the construction of the apparatus. MGC is grateful to the EPSRC for the provision of a postgraduate studentship. We thank Dr. Gleb Gribakin for useful discussions and communications.


Pierre Clairambault
email: p.clairambault@bath.ac.uk

Isomorphisms of types in the presence of higher-order references

We investigate the problem of type isomorphisms in a programming language with higher-order references. We first recall the game-theoretic model of higher-order references by Abramsky, Honda and McCusker. Solving an open problem by Laurent, we show that two finitely branching arenas are isomorphic if and only if they are geometrically the same, up to renaming of moves (Laurent's forest isomorphism). We deduce from this an equational theory characterizing isomorphisms of types in a finitary language L2 with higher order references. We show however that Laurent's conjecture does not hold on infinitely branching arenas, yielding a non-trivial type isomorphism in the extension of L2 with natural numbers.

I. INTRODUCTION

During the development of denotational semantics of programming languages, there was a crucial interest in defining models of computation satisfying particular type equations. For instance, a model of the untyped λ-calculus can be obtained by isolating a reflexive object (that is, an object D such that D ≃ D D ) in a cartesian closed category. In the 80s, some people started to consider the dual problem of finding these equations that must hold in every model of a given language: they were coined type isomorphisms by Bruce and Longo. In [START_REF] Bruce | Provable isomorphisms and domain equations in models of typed languages (preliminary version)[END_REF], they exploited a theorem by Dezani [START_REF] Dezani-Ciancaglini | Characterization of normal forms possessing inverse in the λ-β-η-calculus[END_REF] giving a syntactic characterization of invertible terms in the untyped λ-calculus to prove that that the only isomorphisms of types present in simply typed λ-calculus with respect to βη equality are those induced by the equation A → (B → C) ≃ B → (A → C). Later this was extended to handle such things as products [START_REF] Bruce | Provable isomorphisms of types[END_REF], higher order [START_REF] Bruce | Provable isomorphisms and domain equations in models of typed languages (preliminary version)[END_REF], possibly with unit types [START_REF] Cosmo | Invertibility of terms and valid isomorphisms, a proof theoretic study on second order lambda-calculus with surjective pairing and terminal object[END_REF], or sums [START_REF] Fiore | Remarks on isomorphisms in typed lambda calculi with empty and sum types[END_REF].

The interest in type isomorphisms grew significantly when their practical impact was realized. In [START_REF] Rittri | Using types as search keys in function libraries[END_REF], Rittri proposed to search functions in software libraries using their type modulo isomorphism as a key. He also considered the possibilities offered by matching and unification of types modulo isomorphisms [START_REF] Rittri | Retrieving library functions by unifying types modulo linear isomorphism[END_REF]. A whole line of research has also been dedicated to the study of type isomorphisms and their use for search tools in richer type systems (such as dependent types [START_REF] Barthe | Type isomorphisms and proof reuse in dependent type theory[END_REF]), along with studies about the automatic generation of the corresponding coercions [START_REF] Atanassow | Inferring type isomorphisms generically[END_REF]. Such tools were implemented for several programming languages, let us mention the command line tool camlsearch written by Vouillon for CamlLight.

It is worth noting that even though these tools are written for powerful programming languages featuring complex computational effects such as higher-order references or exceptions, they rely on the theory of isomorphisms in weaker (purely functional) languages, such as the second-order λ-calculus with pairs and unit types for camlsearch. Clearly, all type isomorphisms in λ-calculus are still valid in the presence of computational effects (indeed, the operational semantics are compatible with βη). What is less clear is whether those effects allow the definition of new isomorphisms. However, it seems that syntactic methods deriving from Dezani's theorem on invertible terms in λ-calculus cannot be extended to complex computational effects. The base setting itself is completely different: the dynamics of terms are no longer defined by reduction rules but by operational semantics, the natural equality between terms is no longer convertibility but observational equivalence, so new methods are required.

In [START_REF] Laurent | Classical isomorphisms of types[END_REF], Laurent introduced the idea of applying game semantics to the study of type isomorphisms (although one should mention the precursor characterization of isomorphisms by Berry and Curien [START_REF] Berry | Sequential algorithms on concrete data structures[END_REF] in the category of concrete data structures and sequential algorithms). Exploiting his earlier work on game semantics for polarized linear logic [START_REF] Laurent | Polarized games[END_REF], he found the theory of isomorphisms for LLP from which he deduced (by translations) the isomorphisms for the call-byname and call-by-value λµ-calculus. The core of his analysis is the observation that isomorphisms between arenas A and B in the category Inn [START_REF] Hyland | On full abstraction for PCF: I, II and III[END_REF] of arenas and innocent strategies are in one-to-one correspondence with forest isomorphisms between A and B, so in particular two arenas are isomorphic if and only if their representations as forests are identical up to the renaming of vertices.

From the point of view of computational effects this looks promising, since game semantics are known to accommodate several computational effects such as control operators [START_REF] Laird | Full abstraction for functional languages with control[END_REF], ground type [START_REF] Abramsky | Linearity, Sharing and State: a Fully Abstract Game Semantics for Idealized Algol with active expressions[END_REF] or higher-order references [START_REF] Abramsky | A fully abstract game semantics for general references[END_REF] or even concurrency [START_REF] Laird | A game semantics of the asynchronous π-calculus[END_REF] in one single framework. Moreover, Laurent pointed out in [START_REF] Laurent | Classical isomorphisms of types[END_REF] that the main part of his result, namely the fact that each Inn-isomorphism induces a forest isomorphism, does not really depend on the innocence hypothesis but only on the weaker visibility condition. As a consequence, his method for characterizing isomorphisms still applies to programming languages such as Idealized Algol whose terms can be interpreted as visible strategies [START_REF] Abramsky | Linearity, Sharing and State: a Fully Abstract Game Semantics for Idealized Algol with active expressions[END_REF]. Laurent raised the question whether his result could be proved without the visibility condition, therefore yielding a characterization of isomorphisms in a programming language whose terms have access to higher-order references and hence get interpreted as non-visible strategies [START_REF] Abramsky | A fully abstract game semantics for general references[END_REF].

The contribution of this paper is threefold: (1) We give a new and synthetic reformulation of Laurent's tools to approach

A × B ≃ E B × A A × (B × C) ≃ E (A × B) × C A × unit ≃ E A bool × A → B ≃ E (A → B) × (A → B) var[A] ≃ E (A → unit) × (unit → A) Figure 1. Isomorphisms in L 2
game-theoretically the problem of type isomorphisms, (2) We prove Laurent's conjecture in the case of finitely branching arenas, allowing us to characterize all type isomorphisms in a finitary (integers-free) programming language L 2 with higherorder references by the theory E presented 1 in Figure 1, [START_REF] Abramsky | Call-by-value games[END_REF] We show however a counter-example to the conjecture when dealing with infinitely branching arenas, and the counterexample yields a non-trivial type isomorphism between the types (nat → unit) → (nat → unit) → unit and (nat → unit) → (unit → unit) → unit in the extension of L 2 with natural numbers. So Laurent's conjecture, in the general case, is false.

In Section II we introduce the finitary language L 2 strongly inspired by Abramsky, Honda and McCusker's language L [1], along with its standard game semantics. Then we turn to the problem of isomorphisms of types. In Section III we first give an analysis of isomorphisms in several subcategories of the games model, reproving and extending Laurent's theorem, then we use it to characterize isomorphisms in L 2 . We show how this characterization fails in the presence of natural numbers, and we give a non-trivial type isomorphism in L.

II. THE LANGUAGE L 2 AND ITS GAME SEMANTICS

A. Definition of L 2 a) Basic definitions: We introduce here a finitary variant L 2 of the programming language L with higher-order references modeled by Abramsky, Honda and McCusker in [START_REF] Abramsky | A fully abstract game semantics for general references[END_REF]: it only differs from L in the fact that the type of natural numbers has been replaced with a type for booleans, along with all the associated combinators. The terms and types of L 2 are given by the following grammars.

Γ ⊢ M : var[A] Γ ⊢ N : A Γ ⊢ M := N : unit Γ ⊢ M : A → unit Γ ⊢ N : unit → A Γ ⊢ mkvar M N : var[A]
This language is equipped with a standard big-step callby-value operational semantics. To define it, we temporarily extend the syntax of terms with identifiers for locations, denoted by l. Then, values are formed as follows:

V ::= skip | true | false | λx.M | V, V | l | mkvar V V
The operational semantics of L 2 are then given as an inductively generated relation (L, s)M ⇓ (L ′ , s ′ )V , where s is a partial map from locations in L to values. The rules for λ-calculus, products and booleans are standard (they do not affect the store) and we give in Figure 2 the rules for references. Note that as usual, some store annotations are omitted to aid readability; the rules can be disambiguated as explained in [START_REF] Abramsky | A fully abstract game semantics for general references[END_REF]. For a closed term M without free locations, we write M ⇓ to indicate that (∅, ∅)M ⇓ (L, s)V for some L, s and V . The observational preorder M ≤ N between terms M and N is then defined as usual, by requiring that for all contexts C

[-] such that C[M ] and C[N ] are closed and contain no free location, if C[M ] ⇓ then C[N ] ⇓. The corresponding equivalence relation is denoted by ∼ =.
b) Syntactic extensions: In this core language, one can define all the constructs of a basic imperative programming language. For instance if C 1 has type unit, sequential composition C 1 ; C 2 is given by:

(λd : unit. C 2 ) C 1
This works only because the evaluation of L 2 is call-by-value. Likewise, a variable declaration new x : A in N (where M has type A) can be obtained by

(λx : var[A]. N ) new A
and its initialized variant new x = M in N as expected. As usual with general references one can define a fixed point combinator Y by

λf : (A → B) → (A → B). new y : A → B in y := λa : A. f !y a; !y
This can be easily applied to implement a while loop. We can also use it to build an inhabitant ⊥ to any type A.

c) Bad variables and isomorphisms: The mkvar construct allows to combine arbitrary "write" and "read" methods, forming terms of type var[A] not behaving as reference cells: those are called bad variables. We include bad variable in L 2 for two reasons. First, because games models that allow bad variables are notably simpler than those which do not [START_REF] Murawski | Full Abstraction for Reduced ML[END_REF], for which it is not clear whether our methods apply. Second, because we expect the problem of isomorphisms without bad variables to be far more subtle than what we consider here, because of the observation by O'Hearn that

M 1 ⇓ V 1 M 2 ⇓ V 2 mkvar M 1 M 2 ⇓ mkvar V 1 V 2 (l ∈ L) (L, s) new A ⇓ (L ∪ {l : A}, s) l (L, s)M ⇓ (L ′ , s ′ )l (L ′ , s ′ )N ⇓ (L ′′ , s ′′ )V (L, s)M := N ⇓ (L ′′ , s ′′ (l → V ))skip M ⇓ mkvar V 1 V 2 N ⇓ V V 1 (V ) ⇓ skip M := N ⇓ skip (L, s)M ⇓ (L ′ , s ′ )l s ′ (l) = V (L, s)!M ⇓ (L ′ , s ′ )V M ⇓ mkvar V 1 V 2 V 2 (skip) ⇓ V !M ⇓ V Figure 2.
(x : A ⊢ (λy.N )M ) ∼ = id A (y : B ⊢ (λx.M )N ) ∼ = id B where id A = x : A ⊢ x : A.

B. The games model

We now describe the fully abstract games model of L 2 . Note that except a few details there is nothing new here, as this is precisely the model described in [START_REF] Abramsky | A fully abstract game semantics for general references[END_REF]. We however include the definitions (but no proofs) for the sake of self-completeness.

e) Arenas, plays: Our games have two participants: Player (P) and Opponent (O). Valid plays between O and P are generated by directed graphs called arenas, which are the abstract representation of types. An arena is a tuple

A = M A , λ A , I A , ⊢ A where • M A is a set of moves, • λ A : M A → {O, P } × {Q,
λ A = λ OP A , λ AQ A The function λ A denotes λ A with the O/P part reversed. A move a ∈ M A is a O-move (resp. P -move) if λ A (a) = O (resp. λ A (a) = P ). • I A ⊆ λ A -1 ({OQ}) is a set of initial moves • ⊢ A ⊆ M 2 A is a relation called enabling, which satisfies that if a ⊢ A b, then λ OP A (a) = λ OP A (b), and if λ QA A (b) = A then λ QA A (a) = Q.
We require two additional conditions on arenas: they should be complete (for each question m ∈ M A , there should be an answer n ∈ M A such that m ⊢ A n) and finitely branching (for all a ∈ M A , the set {m ∈ M A | a ⊢ A m} is finite). We consider the usual arrow construction A ⇒ B on arenas, as well as products Π i∈I A i and lifted sums Σ i∈I A i of finite families of arenas. Their definitions can be found, for example, in [START_REF] Abramsky | A fully abstract game semantics for general references[END_REF]. It is obvious that they preserve the fact of being complete and finitely branching. The 0-ary product (the empty arena) is denoted by 1, and will be a terminal object in our category.

If A is an arena, a justified sequence over A is a sequence of moves in M A together with justification pointers: for each non-initial move b, there is a pointer to an earlier move a such that a ⊢ A b. In this case, we say that a justifies b. The transitive closure of the justification relation is called hereditary justification.

f) Notations: The relation ⊑ will denote the prefix ordering on justified sequences. By s ⊑ P t, we mean that s is a P -ending prefix of t. If s is a sequence, then |s| will denote its length. We also define the prefix functions ip and jp by ip(ǫ) = ǫ and ip(sa) = s, and jp(si

) = ǫ if i is initial, jp(s 1 as 2 b) = s 1 a if b is justified by a.
A justified sequence s over A is a legal play if it is:

• Alternating: If s ′ ab ⊑ s, then λ OP A (a) = λ OP A (b).
• Well-bracketed: a question q is answered by a later answer a if q justifies a. A justified sequence s is well-bracketed if each answer is justified by the last unanswered question, that is, the pending question. The set of all legal plays on A is denoted by L A . We will also be interested in the set L ′ A of well-bracketed but not necessarily alternating plays on A, called pre-legal plays.

g) Strategies, composition: A strategy σ on an arena A (denoted σ : A) is a non-empty set of P -ending legal plays on A satisfying prefix-closure, i.e. that for all sab ∈ σ, we have s ∈ σ and determinism, i.e. that if sab, sac ∈ σ, then b = c. As usual, strategies form a category which has arenas as objects, and strategies σ :

A ⇒ B as morphisms from A to B. If σ : A ⇒ B and τ : B ⇒ C are strategies, their composition σ; τ : A ⇒ C is defined as usual by first defining the set of interactions u ∈ I(A, B, C) of plays u ∈ L (A⇒B)⇒C such that u ↾A,B ∈ L A⇒B , u ↾B,C ∈ L B⇒C and u ↾A,C ∈ L A⇒C (
where s ↾A,B is the usual restriction operation essentially taking the subsequence of s in M A and M B , along with the possible natural reassignment of justification pointers). The parallel interaction of σ and τ is then the set

σ||τ = {u ∈ I(A, B, C) | u ↾A,B ∈ σ ∧ u ↾B,C ∈ τ },
and the composition of σ and τ is obtained by the hiding operation, i.e. σ; τ = {u ↾A,C | u ∈ σ||τ }. It is known (e.g. [START_REF] Mccusker | Games and full abstraction for a functional metalanguage with recursive types[END_REF]) that composition is associative. It admits copycat strategies as identities:

id A = {s ∈ L A1⇒A2 | ∀s ′ ⊑ P s, s ′ ↾A1 = s ′ ↾A2 }. If s ∈ L A ,
the current thread of s, denoted ⌈s⌉, is the subsequence of s consisting of all moves hereditarily justified by the same initial move as the last move of s. All strategies we are interested in will be single-threaded, i.e. they only depend on the current thread. Formally, σ :

A is single-threaded if • For all sab ∈ σ, b points in ⌈sa⌉,
• For all sab, t ∈ σ such that ta ∈ L A and ⌈sa⌉ = ⌈ta⌉, we have tab ∈ σ. It is straightforward to prove that single-threaded strategies are stable under composition and that id A is single-threaded. Hence, there is a category Gam of arenas and single-threaded strategies. The category Gam will be the base setting for our analysis. Given arenas A and B, the arena A × B defines a cartesian product of A and B and the construction A ⇒ B extends to a right adjoint A × -⊣ A ⇒ -, hence Gam is cartesian closed and is a model of simply typed λ-calculus. It also has weak coproducts, given by the lifted sum [START_REF] Abramsky | A fully abstract game semantics for general references[END_REF].

h) Views, classes of strategies: In this paper, we are mainly interested in the properties of single-threaded strategies. However, to give a complete account of the context it seems necessary to mention several classes of strategies of interest in this setting. The most important one is certainly the class of innocent strategies, both for historical reasons and because it is at the core of the frequent definability resultsand thus of the full abstraction results -in game semantics. Their definition requires the notion of P -view, defined as usual by induction on plays as follows.

si = i if i ∈ I A sa = s if λ OP A (a) = P s 1 as 2 b = s 1 ab if λ OP A (b) =
O and a justifies b A strategy σ : A is then said to be visible if it always points inside its P -view, that is, for all sab ∈ σ the justifier of b appears in sa . The strategy σ is innocent if it is visible, and if its behaviour only depends on the information contained in its P -view. More formally, whenever sab, t ∈ σ such that ta ∈ L A and sa = ta , we must also have tab ∈ σ. Both visibility and innocence are stable under composition [START_REF] Hyland | On full abstraction for PCF: I, II and III[END_REF], [START_REF] Abramsky | Linearity, Sharing and State: a Fully Abstract Game Semantics for Idealized Algol with active expressions[END_REF], thus let us denote by Vis the category of arenas and visible single-threaded strategies and by Inn the category of arenas and innocent strategies. Both categories inherit the cartesian closed structure of Gam, but strategies in Inn are actually nothing but abstract representation of (η-long βnormal) λ-terms and form a fully complete model of simplytyped λ-calculus. Strategies in Vis have more freedom, they correspond in fact to programs with first-order store [START_REF] Abramsky | Linearity, Sharing and State: a Fully Abstract Game Semantics for Idealized Algol with active expressions[END_REF].

C. Modeling L 2 in Fam f (Gam)
i) Interpretation: The three categories Gam, Vis and Inn are categories of negative games (in which Opponent always plays first), and these are known to model call-byname computation whereas L 2 is call-by-value. We could have modeled it using positive games, following the lines of [START_REF] Honda | Game-theoretic analysis of call-byvalue computation[END_REF]. Instead, we follow [START_REF] Abramsky | A fully abstract game semantics for general references[END_REF] and model L 2 in the free completion Fam(Gam) of Gam with respect to coproducts. This will allow us to first characterize isomorphisms in Gam (result which could be applied to a call-by-name language with state) then deduce from it the isomorphisms in Fam(Gam). In fact we will consider the completion Fam f (Gam) of Gam with respect to finite coproducts, since L 2 has only finite types.

The objects of Fam f (Gam) are finite families

{A i | i ∈ I} of arenas. A map from {A i | i ∈ I} to {B j | j ∈ J} is
the data of a function f : I → J together with a family of strategies {σ i :

A i → B f (i) | i ∈ I}.
As shown in [START_REF] Abramsky | Call-by-value games[END_REF], the cartesian closed structure of Gam extends to Fam f (Gam). Moreover, the weak coproducts in Gam give rise to a strong monad T on Fam f (Gam). Given families

A = {A i | i ∈ I} and B = {B j | j ∈ J}, we define A × B = {A i × B j | (i, j) ∈ I × J} A ⇒ B = {Π i∈I (A i ⇒ B f (i) ) | f : I → J} T A = {Σ i∈I A i }
The singleton family {1} is the terminal object of Fam f (Gam). By abuse of notation, we will still denote it by 1. The other components of the cartesian closed structure of Fam f (Gam) and of the strong monad structure of T follow naturally from these definitions. We skip the details, as all of this is already covered in [START_REF] Abramsky | A fully abstract game semantics for general references[END_REF]. It is known that given a cartesian closed category with a strong monad, one can interpret call-byvalue languages in the Kleisli category of the monad [START_REF] Moggi | Notions of computation and monads[END_REF], and the interpretation of L 2 in Fam f (Gam) follows these lines.

We interpret unit and bool as the families with respectively one and two elements whose components are all empty arenas. Of course we also need to give an interpretation for var[A], along with morphisms for the read and write operations of the reference cell. Once again, we follow the lines of [START_REF] Abramsky | A fully abstract game semantics for general references[END_REF] and consider the type var[A] as the product of its read and write methods, hence we set var[A] = ( A ⇒ T 1)×T A . The interpretation relies on the definition of a morphism

1 → var[A] , that is, if A = {A i | i ∈ I}, a strategy cell : (Π i∈I (A i ⇒ 1 ⊥ ) × Σ i∈I A i ) ⊥
, where A ⊥ = T {A} is the lift operation. Apart from the initial protocol due to the lift, the strategy cell works by associating each read request with the latest write request and playing copycat between them. A more detailed description is given in [START_REF] Abramsky | A fully abstract game semantics for general references[END_REF], and an algebraic definition is obtained in [START_REF] Melliès | An algebraic account of references in game semantics[END_REF]. As proved in [START_REF] Abramsky | A fully abstract game semantics for general references[END_REF], this gives a sound interpretation of L 2 in Fam f (Gam) T . j) Complete plays and full abstraction: A fully abstract model of L 2 is obtained by quotienting Fam f (Gam) T by the usual observational preorder. However, as is often the case with fully abstract game semantics of languages with store, it is effectively presentable: the observational preorder can be characterized directly. Say a play s ∈ L A is complete if it has as many questions and answers, i.e. all questions have been answered. If σ is a strategy on an arena A, then let us denote by comp(σ) the set of complete plays in σ. Take σ, τ :

A → B two morphisms in Fam f (Gam) T , with A = {A i | i ∈ I} and B = {B j | j ∈ J}. Then, σ and τ consist of families {σ i : A i → Σ j∈J B j | i ∈ I} and {τ i : A i → Σ j∈J B j | i ∈ I}.
We then say that σ τ if and only if for all i ∈ I, comp(σ i ) ⊆ comp(τ i ).

Take now two terms M and N of type A, and suppose

A = {A i | i ∈ I}.
Then M and N are morphisms from 1 to T A in Fam f (Gam), i.e. strategies on Σ i∈I A i . Given the full abstraction result of [START_REF] Abramsky | A fully abstract game semantics for general references[END_REF], it is then straightforward to prove the following equivalence:

M ≤ N ⇔ M N
This concrete representation of the observational preorder will be central to our characterization of isomorphisms in L 2 .

III. ISOMORPHISMS IN Gam

We are now going to extend Laurent's tools [START_REF] Laurent | Classical isomorphisms of types[END_REF] to characterize isomorphisms of types for L 2 . We will first recall Laurent's work in the visible and innocent cases, then extend it to characterize isomorphisms in Gam. From there, we will switch to call-by-value and study the isomorphisms in Fam f (Gam), and in its Kleisli category over T .

A. Isomorphisms and zig-zag strategies

We start by giving the definition of (a subtle adaptation of) By extension, we will say that a strategy σ is pre-zig-zag (resp. zig-zag) if all its plays are so. The core of Laurent's theorem is then that all isomorphisms in Vis are zig-zag strategies. His proof does rely on visibility, however it only gets involved to prove that the condition 3 of zig-zag plays is satisfied. The first half of his argument does not use visibility and actually proves that all isomorphisms in Gam are prezig-zag. Here, being mainly interested in Gam, we make this explicit. We need first the following lemma.

LEMMA 1 (Dual pre-zig-zag play). Let s ∈ L A⇒B be a pre-zig-zag play, then there exists an unique pre-zig-zag s ∈ L B⇒A such that s ↾A = s ↾A and s ↾B = s ↾B .

Proof: We define s by induction on s; ǫ = ǫ, and sab = sba. We keep the same pointers, except for the case where a move a in A was justified by an initial move b in B. Then because of the pre-zig-zag condition on s, a is necessarily an initial move in A and is set as the new justifier of b in s. There is no other possible s, since the restrictions on A and B are constrained by the hypotheses and their interleaving is forced by the alternation and the pre-zig-zag conditions on s. If k = 0, this is trivial. Otherwise, suppose this is true up to k ∈ N, and consider sab ∈ σ of length k + 2; let us first prove condition [START_REF] Abramsky | A fully abstract game semantics for general references[END_REF]. Without loss of generality, suppose a ∈ M A . Since s ↾B = s ↾B , by a straightforward zipping argument we can build an interaction u ∈ I(A 1 , B, A 2 ) such that u ↾A1,B = s and u ↾B,A2 = s, moreover since σ, τ form an isomorphism we must have u ↾A1,A2 ∈ id A . Now, we necessarily have b ∈ M B , otherwise u could be extended to uab ∈ σ||τ with uab ↾A1,A2 = u ↾A1,A2 ab which is not a play of the identity, contradiction. Hence sab satisfies condition 1 of pre-zig-zag plays.

To see why it satisfies condition 2, take sba ∈ σ with b in B and a in A. If b is initial in B, then a necessarily points to it since σ is single-threaded. Reciprocally, suppose a points to an initial move in B earlier than b. Then we have s ∈ τ , and by the same zipping argument as above we have an unique u ∈ I(B 1 , A, B 2 ) such that u ↾B1,A = s and u ↾A,B2 = s. Since σ, τ form an isomorphism we also have u ↾B1,B2 ∈ id B . Let us now extend u to u ′ = ub 2 ab 1 in the unique way such that u ′ ↾A,B2 = sba and u ′ ↾B1,A ∈ τ . Note that we are sure that b 1 is a move on B 1 since sab 1 is a play of τ of length k +2 and we already know that these satisfy the condition 1 of pre-zig-zag plays. But we also have u ′ ↾B1,B2 ∈ id B , hence b 2 points in s as b 1 points in s. This means that we have sab ∈ τ , such that a is initial and b points in s, impossible since τ is single-threaded. Hence sba satisfies condition 2 of pre-zig-zag plays.

We have proved that sab is pre-zig-zag, so sab is defined. By induction hypothesis s ∈ τ and the same reasoning as above shows that it extends to sab ∈ τ . The argument is symmetric,

hence {s | s ∈ σ ∧ |s| ≤ k + 2} = {s ∈ τ | |s| ≤ k + 2}.
For the sake of completeness, let us include Laurent's argument which proves that isomorphisms in Vis are zig-zag. Proof: We already know that σ and τ are pre-zig-zag strategies. We show by induction on n ∈ N that for all s ∈ σ, if |s| ≤ n then s ↾A and s ↾B have the same pointers. Take now s ∈ σ, and sab ∈ σ, suppose w.l.o.g. that a ∈ M A . Suppose a points to (s ↾A ) i , then b points to (s ↾B ) i . Indeed, it cannot point to (s ↾B ) j with j > i since that would break visibility for σ. But if it points to (s ↾B ) j with j < i we use the same reasoning on the dual pre-zig-zag play sab and get a contradiction with the fact that τ is visible.

Let us denote by Gam i , Vis i and Inn i the groupoids of arenas and isomorphisms on the respective categories. In the next sections, we use these facts to give more combinatorial representations of Gam i , Vis i and Inn i .

B. Notions of game morphisms

Laurent's isomorphism theorem works by relating isomorphisms in Gam with isomorphisms in a simpler category which has arenas as objects and forest morphisms 2 , i.e. maps on moves that preserve initiality and enabling. Relaxing the visibility conditions requires us to also consider relaxed notions of game morphisms, that we present here. DEFINITION 3. Let A be an arena. A path on A is a play s ∈ L A such that except for the initial move, every move in s points to the previous move. Formally, for all s ′ ab ⊑ s, a justifies b in s. Let P A denote the set of paths on A. A path morphism from A to B is a function φ : P A → P B such that ip • φ = φ • ip and which preserves Q/A labeling: for all sa ∈ P A with φ(sa) = φ(s)b, we have λ QA A (a) = λ QA B (b).

There is a category Path of arenas and path morphisms.

This category Path comes with its own notion of isomorphisms of arenas. Note that whenever A is a forest, this is exactly Laurent's notion of forest isomorphism. We now introduce two weaker notions of morphisms for arenas. In what follows, let us call a legal play on A with only one initial move a thread on A, and denote the set of threads on A by T A . Likewise, let us call a pre-legal play with one initial move a pre-legal thread and let us denote these by T ′ A . DEFINITION 4. Let A, B be arenas, and let φ :

T ′ A → T ′ B We say that φ is a sequential morphism from A to B if ip • φ = φ • ip, and if it preserves Q/A labeling, i.e. for all φ(sa) = φ(s)b we have λ QA A (a) = λ QA B (b).
We say that it is a justified morphism if, additionally, jp • φ = φ • jp. There are two categories Seq of arenas and sequential morphisms and Jus of arenas and justified morphisms.

As above, we will denote by Seq i , Jus i and Path i the groupoids of invertible maps in Seq, Jus and Path. These groupoids will soon appear to be identical to Gam i , Vis i and Inn i . To prove this, we need the following lemma.

LEMMA 4. Let s ∈ T ′

A , and σ : A ⇒ B an isomorphism in Gam. There is then an unique play s ′ ∈ σ such that s ′ ↾A = s. Proof: Remark first that if σ : A ⇒ B and τ : B ⇒ A are inverses then they are both total, i.e. for all s ∈ σ and sa ∈ L A⇒B there must be b such that sab ∈ σ, assuming it is not the case easily leads to a contradiction. We now prove the lemma by induction on s. If s = ǫ, this is trivial. Otherwise, suppose sa ∈ T ′ A and we have by induction hypothesis s ′ ∈ σ such that s ′ ↾A = s. If a is a P -move in A (hence an O-move in A ⇒ B), there is an unique b such that s ′ ab ∈ σ, and we do have s ′ ab ↾A = sa. If a is an O-move in A (hence a P -move in A ⇒ B), then let τ : B ⇒ A be the inverse of σ, since s ′ ∈ σ we have s ′ ∈ τ . Being part of an isomorphism τ is total, hence there is b such that s ′ ab ∈ τ . We deduce from this that s ′ ba ∈ σ, and we have s ′ ba ↾A = sa as needed. This choice is unique: if there is another play t ∈ σ such that t ↾A = sa, then t = t ′ b ′ a (since t is zig-zag). By induction hypothesis we have t ′ = s ′ , thus s ′ b ′ a ∈ σ. From this we deduce that s ′ ab ′ ∈ τ , so b = b ′ by determinism of τ . PROPOSITION 1. If C ≃ D means that two groupoids C and D are isomorphic, then we have:

Gam i ≃ Seq i Vis i ≃ Jus i Proof: Let us first define a functor F : Gam i → Seq i .
It is defined as the identity on arenas. Let σ : A ⇒ B be an isomorphism, and let s ∈ T ′ A then we define φ σ (s) = s ′ ↾B , where s ′ is the unique play on A ⇒ B which existence is ensured by the lemma above. The function φ σ commutes with ip since σ is a pre-zig-zag strategy. To any question it cannot associate an answer, as that would immediately break well-bracketing on σ. But to any answer it cannot associate a question, as that would immediately break well-bracketing on σ -1 . Then we define F (σ) = φ σ . It is obvious that F preserves identities and composition 3 .

Reciprocally, suppose φ : A → B is a sequential isomorphism. We mimic the usual definition of the identity by setting G(φ) = {s ∈ L A⇒B | ∀s ′ ⊑ P s, φ(s ′ ↾A ) = s ′ ↾B } (We apply φ on plays whereas it is normally only defined on threads, however it can be canonically extended to plays, so this is not ambiguous). It is obvious that this construction is functorial, and that it is inverse to F .

We have now an isomorphism Gam i ≃ Seq i which restricts naturally to Vis i and Jus i . Indeed if σ : A ⇒ B is a visible isomorphism, it is a zig-zag strategy therefore s ∈ T ′ A and φ σ (s) have the same pointers, which means that jp•φ σ = φ σ •jp. Reciprocally if φ σ is a justified morphism, all s ∈ σ must be such that s ↾A and s ↾B have the same pointers, therefore σ, being pre-zig-zag, always points in its P -view.

C. Innocent and visible case

In this section, we use the framework described above to recall Laurent's results. We have proved above that isomorphisms in Vis correspond to isomorphisms in Jus, which we are now going to compare with isomorphisms in Path.

LEMMA 5. There is a full functor H : Vis i → Path i .

Proof: We have built in the above section a full and faithful functor (actually an isomorphism) F :

Vis i → Jus i . From a visible isomorphism σ : A ⇒ B we set H(σ) = F (σ) ↾ P A , where f ↾ E ′ restricts a function f : E → F to a subset E ′ ⊆ E of its domain.
The image of a path by F (σ) is always a path since it is a justified morphism, hence H(σ) :

P A → P B .
To see why H is full, suppose we have a path morphism φ : P A → P B . Then φ admits a canonical extension φ * :

T ′ A → T ′ B .
To define φ * (s) we reason by induction on s, and set φ * (ǫ) = ǫ and φ * (sa) = φ * (s)a ′ , where a ′ is the last move of φ(p a ), p a being the path of a in s. The move a ′ keeps the same pointer as a. It is clear that this defines as needed a justified morphism φ * such that H(φ * ) = φ.

This ensures that arenas A and B are isomorphic in Vis if and only if they are isomorphic in Path, i.e. they are geometrically the same. Let us mention that as Laurent proved, this correspondence is one-to-one in the innocent case: one can prove that there is only one innocent zig-zag strategy corresponding to a particular path isomorphism, hence H restricts to an isomorphism of groupoids H ′ :

Inn i → Path i .
k) Faithfulness of H: Note however that H itself is not faithful, because we can exploit non-innocence to build nonuniform isomorphisms, i.e. isomorphisms which change their underlying path isomorphism as the interaction progresses. For an example, consider the arena A = q q 1 q 2 a a a which is the interpretation of (bool → unit) → unit in call-by-value and of unit × unit → unit in call-by-name.

A

+ 3 A q q q 1 q 1 q 1 q 2 q 2 q 1 ; ;

w w w w w w w w w w w ⊆ # # G G G G G G G G G G G Gam i iso / / Seq i ? O O Figure 4.
Relations between all groupoids of isomorphisms Consider now the strategy i : A ⇒ A which behaves as follows. It starts by playing as the identity on A. The first time Opponent plays q 1 or q 2 on the left hand side, it simply copies it. Starting from the second time Opponent plays q 1 or q 2 though, it swaps them. An example play of i is given in Figure 3. Although it is not the identity, i is its own inverse. Its image by H only takes into account the first behaviour or i, thus is the same as for id A : the identity path morphism on A. From this strategy we can extract the following term f : B ⊢ M : B of L 2 , where B = (bool → unit) → unit.

new r := true in λg.f (λb.if !r then r := false; g b else g (not b))

Although M is not the identity it is an involution on B, i.e. we have (λf.M )(M x) ∼ =L 2 x. Such non-trivial involutions cannot be defined using only purely functional behaviour.

We give in Figure 4 a summary of all the groupoids of isomorphisms encountered for the moment, along with their relations. Following it, the question of finding the isomorphisms in Gam boils down to the definition of an arrow from Seq i to Path i in this diagram, which is what we will attempt in the next two subsections.

D. Non-visible isomorphisms by counting

We have seen above that we can build a full functor Vis i → Path i , which allows to characterize isomorphic arenas in Vis. However, this construction relies heavily on visibility. We now investigate how to get rid of it and prove that two arenas A and B are isomorphic in Gam if and only if they are isomorphic in Path. In this subsection, we will describe for pedagogical reasons an intuitive approach to the proof, which relies on counting. However this approach suffers from some defects, hence the full proof (described in the next subsection) will follow slightly different lines.

If a ∈ M A , let us call its arity the quantity ar(a) = |{m ∈ M A | a ⊢ A m}|. On pre-threads s ∈ T ′ A we define:

Q(s) = |s| i=1 ar(s i ) If s ∈ T ′ A , Q(s)
is also the number of ways s can be extended to some sa (let us recall here that as a member of T ′ A , s need not be alternating): the choice of a justifier s i plus a move enabled by s i . These definitions allow to express the following observation. If σ : A ⇒ B is an isomorphism (thus a pre-zig-zag strategy) and s ∈ σ, then Q(s ↾A ) = Q(s ↾B ), because σ being an isomorphism, it must associate each possible extension of s ↾A to an unique extension of s ↾B . But this also means that if sab ∈ σ we have

Q(s ↾A ) + ar(a) = Q(s ↾A a) = Q(s ↾B b) = Q(s ↾B ) + ar(b),
hence ar(a) = ar(b). Thus to each move a, σ must associate a move with the same arity. This is a step in the right direction, but we would like a deeper connection between a and b.

If a ∈ M A , we will use the notation

J a = {m ∈ M A | a ⊢ A m}. Let us define by induction on k the notion of a k- isomorphism between a ∈ M A and b ∈ M B . For any a ∈ M A and b ∈ M B there is automatically a 0-isomorphism i a,b . A (k+1)-isomorphism from a to b is the data of an isomorphism f : J a → J b along with, for all m ∈ J a , a k-isomorphism f m : m → f (m).
We use the notation m ≃ k n to denote the fact that there is a k-isomorphism from m to n. In other words, we have m ≃ k n if the tree of paths of length at most k starting form m is tree-isomorphic to the tree of paths of length at most k starting from n. If k 1 ≤ k 2 , f 1 is a k 1 -isomorphism and f 2 is a k 2 -isomorphism, we say that f 1 is a prefix of f 2 if they agree up to depth k 1 . Note that in particular we have m ≃ 1 n if and only if ar(m) = ar(n), so m ≃ k n is indeed a generalization of ar(m) = ar(n). By induction on k, one can then prove that σ must always associate to each move m a move n such that m ≃ k n : to prove it for k + 1, just apply the counting argument above on ≃ k -equivalence classes. From all these k-isomorphisms, one can then deduce the existence of a path isomorphism between A and B.

This counting argument has several unsatisfying aspects, which are caused by the implicit use of the following lemma.

LEMMA 6 (Slicing of isomorphisms). Suppose E ′ ⊆ E and F ′ ⊆ F are finite sets, and that f : E → F and g : E ′ → F ′ are isomorphisms. Then there is an isomorphism f \ g :

E \ E ′ → F \ F ′ .
The obvious proof of this lemma is by cardinality reasons. However this proof is, computationally speaking, "almost noneffective", in the sense that the isomorphism it produces implicitly depends on the choice of a total ordering for E and F . A consequence of that is that from any isomorphism in Gam we will extract an isomorphism in Path, but we cannot hope its choice to be canonical, for any reasonable meaning of "canonical". Even worse, the witness isomorphisms given by this proof for ≃ k and ≃ k+1 need not agree together. This implies that for infinitely deep arenas, one requires König's lemma to actually build a path isomorphism from a game isomorphism. This means that we cannot deduce from the proof above an algorithm to extract path isomorphisms.

E. Extraction of a path isomorphism

To obtain a more computationally meaningful extraction of a path iso from a game iso, we must replace the proof of Lemma 6 by something else than counting. As formalized in the following proof, the idea is to remark that given the data of Lemma 6, starting from x ∈ E \ E ′ , the sequence

x 0 = f (x) x n+1 = f • g -1 (x n )
must eventually reach F \F ′ , as illustrated in Figure 5, yielding a bijection between E \ E ′ and F \ F ′ . PROPOSITION 2. If φ : A → B is a sequential play isomorphism, then for all sa ∈ T ′ A with φ(sa) = φ(s)b, there is a family (h k s,sa ) k∈N such that for all k, h k s,sa is a k-isomorphism from a to b. This family is coherent, in the following sense: if k 1 ≤ k 2 , h k1 s,sa is a prefix of h k2 s,sa . Proof: We will use the following notations. If s ∈ T ′ A , E s will be the set of atomic extensions of s, that is of plays sa ∈ T ′ A , and F s will be the set of atomic extensions of φ(s). For all plays sa ∈ T ′ A , although strictly speaking E s is not a subset of E sa , we have the following decomposition:

E sa = E s + J a
Indeed, a move extending sa can either point to some s i or to a. Note also that for any s, φ : sa → φ(s)b induces an isomorphism f s : a → b from E s to F s .

For all s ∈ T ′ A and sa ∈ E s , we follow the reasoning illustrated in Figure 5 and consider a bipartite directed graph G s,sa defined as follows: its set of vertices is V = E sa + F sa and its set of edges is

E = {(x, f sa (x)) | x ∈ E sa } + {(y, f -1 s (y)) | y ∈ F s }.
This graph is "deterministic", in the sense that the outwards degree of each vertex is at most one, moreover the only vertices whose outwards degree is 0 are those of J b (where b = f s (a), so F sa = F s + J b ). Moreover G s,sa must be acyclic, since f s and f sa are isomorphisms. Thus from any vertex in J a , there is an unique path in G leading to a vertex in J b ; this induces an isomorphism g s,sa : J a → J b . For each pair (m, g s,sa (m)) we also keep track of the corresponding path p m s,sa = (m, f sa (m), f -1 s (f sa (m)), . . . , g s,sa (m)). It is now time to build the k-isomorphisms, by induction on k. For k = 0 this is obvious. For fixed k + 1 ≥ 1, by induction hypothesis there is for each sa ∈ T ′ A with φ(sa) = φ(s)b a k-isomorphism h k s,sa from a to b. In particular, for fixed sa ∈ T ′ A , consider the graph G s,sa . Each of its edges of the form (x, f sa (x)) are now labeled by the k-isomorphism h k sa,x and all its edges of the form (y, f -1 s (y)) are labeled by (h k s,f -1 s (y) ) -1 . For each pair (m, g s,sa (m)) we can now compose the labels along the path p m s,sa and get a k-isomorphism i m : m → g s,sa (m). We then define h k+1 s,sa = (g s,sa , (i m ) m∈Ja ) which is as needed a (k + 1)isomorphism from a to b.

Note finally that if k 1 ≤ k 2 , h k1 s,sa is a prefix of h k2 s,sa . This is proved by simultaneous induction on k 1 and k 2 . If k 1 = 0 this is obvious. Otherwise, it relies on the fact that the graph G s,sa does not depend on k. Hence h k1+1 s,sa = (g s,sa , (i m ) m∈Ja ) and h k2+1 s,sa = (g s,sa , (j m ) m∈Ja ), and each i m has be obtained from k 1 -isomorphisms in the same way as j m has been obtained from k 2 -isomorphisms, so it immediately boils down to the induction hypothesis.

∈ N a k-isomorphism h k ǫ,i : i → f (i).
Additionally, all these k-isomorphisms are compatible with each other, so they converge to an ωisomorphism h ǫ,i : i → f (i). The iso f together with h ǫ,i for all i define a path isomorphism from A to B. l) Canonicity: For each pair of arenas A, B, we have built a function K A,B : Gam i (A, B) → Path i (A, B). The natural question is then whether, like in the other cases, this function defines a full functor. Unfortunately the answer is no, in fact K A,B is not even functorial. Indeed, the construction is based on the more explicit proof of Lemma 6 illustrated in Figure 5, which is not functorial; one can find sets

E ′ ⊆ E, F ′ ⊆ F and G ′ ⊆ G and isomorphisms E f / / F g / / G and E ′ f ′ / / F ′ g ′ / / G ′ such that (f \ f ′ ); (g \ g ′ ) = (f ; g) \ (f ′ ; g ′ ).
From this it is not hard to find a counterexample to the functoriality of K A,B . It is a bit lengthy to describe it properly though, so we do not include it.

Although not being a functor, K does satisfy some canonicity property: its result is invariant under renaming of moves in A and B. In other terms, K A,B : Gam i (A, B) → Path i (A, B) is natural in A and B, if both Gam i (-, -) and Path i (-, -) are seen as bifunctors from Path op i × Path i to Set (using implicitly the faithful functor from Path i to Gam i of Figure 4).

F. Application to L 2

Our isomorphism theorem most naturally applies to Gam (so to call-by-name languages), but L 2 is modeled in Fam f (Gam), and more precisely in the Kleisli category of the strong monad T , so we have to check how our result extends to this. Let us first relate isomorphisms in Fam f (Gam) T and isomorphisms in Gam using the following lemma.

LEMMA 7. Let A = (A i ) i∈I and B = (B j ) j∈J , then isomorphisms between A and B in Fam f (Gam) T are in one-to-one correspondence with pairs (f, (σ i ) i∈I ) where f : I → J is a bijection and each σ i : A i ⇒ B f (i) is an iso in Gam.

Proof: Imagine σ : A → T (B) and τ : B → T (A) are morphisms in Fam f (Gam) that form an isomorphism in Fam f (Gam) T . Here A and B are families of arenas, so A = (A i ) i∈I , and σ = (σ i ) i∈I with σ i : A i ⇒ T (B). Similarly, we have B = (B j ) j∈J and τ j : B j ⇒ T (A). Then, first note that σ i and τ j necessarily first give an answer to the initial Opponent move in T , i.e. the initial question of the lifted sum in T (B) and T (A). Indeed take i ∈ I, and consider σ i ; τ * : A i → T (A), where τ * : T (B) → T (A) is the lifting of τ : B → T (A). This morphism must be a component of the identity on A in Fam f (Gam) T since σ, τ form an iso. In particular, it does directly answer the initial move in T . However, by definition of τ * : T (B) → T (A) it is strict, i.e. it directly interrogates the left occurrence of T , so σ i must necessarily first answer the initial move in T otherwise we would immediately get a contradiction. This means that each σ i must first choose a component j ∈ J (thus inducing a function f : I → J), then play as σ ′ i : A i ⇒ B j . The same analysis on τ provides a function g : J → I and strategies τ ′ j : B j ⇒ A g(j) , and it is then obvious that since σ, τ form an isomorphism g must be inverse of f and each τ ′ j inverse of σ ′ g(j) . m) Syntactic characterization: Let us prove now that the equational theory E given in Figure 1 Proof: By induction on their normal forms. For types generated by S take A ≃ E bool n × A ′ and B ≃ E bool p × B ′ . By Lemma 7 we have n = p (since A ′ and B ′ , generated by T , must be singletons) and we still have A ′ ≃ Fam f (Gam) T B ′ . The case of types generated by T and U is direct. THEOREM 2. For any types A, B of L 2 whose interpretation give families (A i ) i∈I and (B j ) j∈J the following propositions are equivalent:

(1) A ≃ L2 B (2) (A i ) i∈I ≃ Fam f (Gam) T / ∼ = (B j ) j∈J (3) (A i ) i∈I ≃ Fam f (Gam) T (B j ) j∈J (4) A ≃ E B Proof: (1) ⇒ (2) by soundness and by definition of type isomorphisms in L 2 , (2) ⇒ (3) because the arenas are complete, hence every play of the identity is a prefix of a q q 1 q 2 a a a q ′ q 1 q 2 a a a q q 1 q 2 a a a q ′ q a a

G. Isomorphisms in the presence of nat

As suggested by the importance of counting in the proof, the presence of nat makes it possible to build a non-trivial isomorphism by playing Hilbert's hotel. Consider the programming language L from [START_REF] Abramsky | A fully abstract game semantics for general references[END_REF], obtained from L 2 by replacing bool with nat. This language has a fully abstract interpretation in Fam(Gam ∞ ) T , where Gam ∞ is the category of not necessarily finitely branching arenas, and single-threaded strategies. Proof: By definition of the interpretation of types, this boils down to an isomorphism in Gam ∞ between the two arenas represented in Figure 6. Informally, the isomorphism from left to right can be described as follows. As long as q ′ has not been played, it behaves as the identity. Whenever Opponent plays q ′ , it copies it to the other side. Then if q ′ has only appeared once, there are two available copies of nat → unit on the left side, one nat → unit and one unit → unit on the right side, so Player picks a bijection between N + N and N + 1 and plays accordingly. More generally, if q ′ has appeared n times, there are exactly n + 1 available copies of nat → unit on the left hand side, one copy of nat → unit and n copies of unit → unit on the right hand side, so Player has to follow a bijection between (n + 1)N and N + n. So any choice of a bijection between (n + 1)N and N + n (for all n ∈ N) will provide an isomorphism.

These strategies are not compact so the definability theorem does not apply, however we can nonetheless manually extract corresponding programs from them. We display them in Figure 7, where * denotes the product operation on natural numbers, and div M N outputs the result of the division algorithm on M : nat and N : nat. Unfortunately, these terms are too complex to hope for a reasonably-sized direct proof that their interpretations give the strategies described above or even that they form an isomorphism. This kind of difficulty emphasizes the need for new algebraic methods to manipulate and prove properties of imperative higher-order programs.

LEMMA 2 .

 2 If σ : A ⇒ B, τ : B ⇒ A form an isomorphism in Gam, then they are pre-zig-zag and for all s, s ∈ σ ⇔ s ∈ τ .Proof: Consider an isomorphism σ : A ⇒ B, τ : B ⇒ A in Gam. We will prove by induction on even k ∈ N that all plays of σ, τ whose length is less than k are pre-zig-zag, and that moreover {s | s ∈ σ ∧ |s| ≤ k} = {s ∈ τ | |s| ≤ k}.

LEMMA 3 .

 3 If σ : A ⇒ B, τ : B ⇒ A form an isomorphism in Vis, then σ and τ are zig-zag strategies.

Figure 3 .

 3 Figure 3. A play of the non-trivial involution i on A

Figure 5 .

 5 Figure 5. Slicing of isomorphisms.

THEOREM 1 .

 1 Two finitely branching arenas A and B are Gam-isomorphic if and only if they are Path-isomorphic. Proof: Consider an isomorphism σ : A ⇒ B in Gam. Restricted on plays with only two moves, it gives an isomorphism f : I A → I B . By the previous proposition, there is for each i ∈ I A and for each k

  characterizes the types A and B such that A and B are isomorphic in Fam f (Gam) T . LEMMA 8 (Type normal form). Any type A has an unique representative (up to ≃ E ) generated by the non-terminal S in: S ::= bool n × T T ::= unit | Π i∈I U U ::= T → S Proof: Straightforward. PROPOSITION 3. If A and B are isomorphic in Fam f (Gam) T , then A ≃ E B.

Figure 6 .

 6 Figure 6. Non-trivial isomorphic arenas in Gam∞

PROPOSITION 4 .

 4 There is an isomorphism in Fam(Gam ∞ ) between (nat → unit) → (nat → unit) → unit and (nat → unit) → (unit → unit) → unit .

  Big-step operational semantics for references in L 2 . If A and B are two types of L 2 , we say that A and B are isomorphic, denoted by A ≃ L2 B, if and only if there are two terms x : A ⊢ M : B and y : B ⊢ N : A such that:

	without bad variables, not only var[X] is not functorial, but it
	does not even preserve isomorphisms. However, note that var-
	free isomorphisms are the same with or without bad variables.
	d) Isomorphisms of types: We are now ready to define
	the notion of isomorphism of types in L 2 .
	DEFINITION 1.

  Laurent's zig-zag plays. DEFINITION 2. Let s ∈ L A⇒B be a legal play. It is zig-zag if 1. Each P -move following an O-move in A (resp. in B) is in B (resp. in A), 2. A P -move in A immediately follows an initial O-move in B if and only if it is justified by it, 3. The (not necessarily legal) sequences s ↾A and s ↾B have the same pointers. If s only satisfies the first two conditions, then it is pre-zig-zag.

A ::= unit | bool | A × A | A → A | var[A] M ::= x | λx.M | M M | M, M | fst M | snd M | skip | true | false | if M M M | new A | M := M | !M | mkvar M MThe typing rules for λ-calculus, pairs and booleans are standard. The rules for references follow.Γ ⊢ new A : var[A] Γ ⊢ M : var[A] Γ ⊢!M : A 1 The absence of the equation A → (B → C) ≃ B → (A → C) mentioned in the introduction may seem strange, but is standard in call-byvalue[START_REF] Laurent | Classical isomorphisms of types[END_REF] due to the restriction of the η-rule on values.

Note that in[START_REF] Laurent | Classical isomorphisms of types[END_REF] arenas are forests, which is not the case here.

In fact, this construction can be seen as a particular case of Hyland and Schalk's faithful functor from games to relations[START_REF] Hyland | Games on graphs and sequentially realizable functionals[END_REF], where the relation happens to be functional.

Acknowledgments. We would like to thank Guy McCusker for interesting discussions on the games models for state and for his help to get a term from the strategy described in Proposition 4, and the anonymous referees for their useful comments and suggestions. We also would like to acknowledge the support of (UK) EPSRC grant RC-CM1025.

f : (nat → unit) → (nat → unit) → unit ⊢ new count := 0, func := ⊥ in λg : nat → unit. let x = f (λn. g(n * (!count + 1))) in λh : unit → unit. count := !count + 1;

IV. CONCLUSION

We solved Laurent's conjecture and characterized the isomorphisms of types in L 2 . Surprisingly, we realized that the combination of higher-order references, natural numbers and call-by-value allowed to define new non-trivial type isomorphisms. Note however that if well-bracketing is satisfied, the proof of our core game-theoretic theorem adapts directly to arenas where all moves only enable a finite number of questions, but an arbitrary numbers of answers. As a consequence, there are no non-trivial isomorphisms (i.e. not already present in the λ-calculus) in the call-by-name variant of L, although we can define one using call/cc.

Note that despite the seemingly restricted power of L 2 , our theorem does apply to all real-life programming languages that have a bounded type of integer, such as bool 32 or bool 64 : in this setting, no non-trivial isomorphism can exist. However unbounded natural numbers can be defined using recursive types, so the isomorphism above can be implemented in a call-by-value programming language with recursive types and general references, such as OCAML.

This work can be extended in several different ways. An obvious possibility is to study isomorphisms in the presence of sum types, since the model is already equipped to handle them. We could also try to eliminate bad variables. Murawski and Tzevelekos' games model [START_REF] Murawski | Full Abstraction for Reduced ML[END_REF] of Reduced ML may be a good setting to try that, however it is not clear whether our core results can be reproved in their nominal setting.


Stephane Bernard
email: stephane.bernard@bourges.univ-orleans.fr

Philippe Gillard

Fabrice Foucher

Christine Mounaïm-Rousselle

Stéphane Bernard

MIE And Flame Velocity Of Partially Oxidised Aluminium Dust

Keywords: DUST EXPLOSIONS, MIE, ALUMINIUM OXIDE, FLAME VELOCITY

come   L'archive ouverte pluridisciplinaire

explosion hazards. The prevention of these hazards can be achieved by the characterisation of the dust parameters such as minimum ignition energy (MIE), maximum rate of pressure rise (Kst), maximum explosion pressure.

MIE is usually measured using the well-known Hartmann tube or its modified apparatus such as Mike 3 (described in EN 13821, (2002)).

On the other hand, the flame velocity is an important parameter for combustion codes. Methods to measure the laminar burning velocity can be classified in two groups: the "flame propagation method" and the "stationary method". The flame propagation method generally uses open tubes or closed bombs. Opened tubes [START_REF] Goroshin | Quenching distance of laminar flame in aluminum dust clouds[END_REF], [START_REF] Han | Behaviour of flames propagating through Lycopodium dust clouds in a vertical duct[END_REF], [START_REF] Proust | Flame propagation and combustion in some dust-air mixtures[END_REF]) are filled with dust clouds generated for the most part by fluidized beds at the bottom of the tube or sometimes by a vibrating sieve placed at the top of the tube. In all cases, cloud generation conditions are chosen in order to reach a low level of residual turbulence. Ignition is most often obtained by means of an electric spark, hot wire or sometimes by a small gas burner.

In a spherical bomb, the laminar burning velocity can be evaluated by the pressure time evolution during the combustion propagation and is initially applied to gases by [START_REF] Lewis | Combustion, flames and explosions of gases[END_REF]. In this experiment, dust is injected by blasting (due to its high settling velocity), strongly increasing the turbulence of the cloud. The consequence is that the measured velocity is turbulent. Some authors, [START_REF] Bradley | Burning rates in turbulent fine dust-air explosions[END_REF] and Silvesterini et al. (2008) have managed to obtain laminar burning velocity by optimizing injection parameters in order to reduce turbulence and finally by extrapolating the laminar burning velocity to "zero turbulence".

It appears that dust air mixtures are often assimilated to gaseous mixtures by considering that the particles are able to produce enough volatile matter in the preheated zone of the flame, in order to be mixed with the air surrounding the particle to burn in the flame reaction zone. These concepts are well summarized by [START_REF] Silvestrini | Correlations for flame speed and explosion overpressure of dust clouds inside industrial enclosures[END_REF].

Concerning stationary methods, the flame is stabilized on a nozzle burner or Bunsen burner.

These methods also present some drawbacks: for example, the conditions are very dependent on the burner's characteristics and the experimental set-up must be optimized in order to keep the flame locked at the top of the burner, as reported by [START_REF] Dahoe | Determination of the laminar burning velocity and the Markstein length of powder-air flames[END_REF], [START_REF] Horton | Characteristics of flat, laminar coal dust flames[END_REF] or [START_REF] Kolbe | Laminar burning velocity measurements of stabilized aluminium dust flames[END_REF].

This work presents in the first part the experimental devices built in order to measure the MIE of dust and the flame velocity of dust explosions. In the second part, some preliminary results on this measurement applied to partially oxidised aluminium dust are given and discussed.

Experimental devices for MIE determination

The MIE is determined using a statistical test of [START_REF] Langlie | A reliability test method for one shot items[END_REF] and [START_REF] Bernard | Statistical Method for the Determination of the Ignition Energy of Dust Cloud-Experimental Validation[END_REF] performed in a Hartmann tube (see Figure 1). This tube (1.3L) and its spark generator are described in Baudry et al. (2007). Dust is deposited at the bottom of the tube and a blast of air scatters particles in the tube. After about 100 ms, the spark is triggered at 110 mm from the bottom of the tube. The air tank pressure, the delay between the air blast and the spark and the spark's duration can be modified with our spark generator controller and optimized by [START_REF] Baudry | Etude de l'explosibilité de poussières métalliques[END_REF].

The power supply was designed to produce a spark at nearly constant power (voltage and current intensity are constant). Energy, in such a case, is only proportional to the spark duration. This time could be changed over the range of 1 µs to 1 s. The break-down of the air is obtained by a pulse of high voltage immediately relayed by low voltage. The spark energy value achieved with such an arrangement is in the range from 10 mJ to 500 J, making it possible to measure the ignition energy of the less ignitable dusts.

Figure 1 For the measurement of the MIE, cloud generation is one key to the problem. Homogeneity of the dust dispersion, dust concentration and turbulence of the cloud are the principal parameters which control the dust cloud features and thus the MIE value. This was achieved by controlling the opening time of the valve which could be adjusted between 60 ms to 1 s and optimized to obtain uniform dispersion inside the tube. The lower overpressure in the air tank (0.5 bar) and the delay between the blast and the spark generation minimized the turbulence. The delay time between blast and spark generation could be also adjusted in the range of 0 to 1000 ms. In this study, in agreement with Eckhoff 0, this delay was adjusted to 100 ms.

Flame velocity and measurement

Isobaric measurement

A cylindrical constant volume combustion chamber of 24.32 litters is used. Dust was injected at the bottom of the vessel with a system derived from the Hartmann tube. The explosion was observed by a high speed camera (Photron FastCam APXPCI R2) through two BK7 windows

The ignition of the generated dust cloud was achieved by the spark generator controller which controls both the injection duration and the delay between injection and ignition. The spark was ignited between two elongated tungsten electrodes. Power and duration of the spark could be adjusted with the spark controller in a range of a few mJ to 500 J.

Figure 2 Injections and configuration parameters were optimized by using shadowgraphy techniques in order to observe the cloud generation by [START_REF] Foucher | Flame wall interaction: effect of stretch[END_REF] and [START_REF] Halter | Effect of dilution by Nitrogen and/or Carbon dioxide on methane and iso-octane air flame[END_REF]. It was possible to visualize the dispersion of the particle and their motion. A scattering system with a stretched drop shape was tried, Figure 3a and 3b illustrate the influence of this system. In Figure 3b, agglomerates of powder had totally disappeared and the cloud seemed to be nearly homogenous.

Figure 3

Electrical ignition system

This spark generator device was used both for the Hartmann tube and the constant volume combustion chambers; its design was detailed by [START_REF] Bernard | Statistical Method for the Determination of the Ignition Energy of Dust Cloud-Experimental Validation[END_REF]. In this paper we only recall the electrical scheme (Figure 4) and the time evolution of the voltage and current intensity of the electrical spark (Figure 5). After the arc breakdown, voltage and current intensity were constant, in these conditions and for an arc duration of more than 20 µs the energy was linear with the arc duration. During tests in cylindrical chamber, parameters of the spark were constant and summarised in Table 1. These parameters, and especially spark energy, were chosen to guarantee the explosion of the dust every time. Table1

Image processing

In order to determine the apparent flame velocity of the explosion, Matlab post processing was applied to the frames obtained by the high speed camera during the explosion. The intensity of each pixel was converted into a binary code in order to determine the area of the flame. Figure 6 showed the shape of the flame area. At the beginning of the explosion the flame was nearly spherical (after 10 ms), progressively the shape of the flame was deformed, probably due to convection which increases turbulence and the fact that at a microscopic scale the cloud was not homogenous (macro scale hypothesis) but discrete. The combustion propagates step by step between particles and zones with a rich mixture are probably burnt before the lean zones due to the greater distance between particles. Therefore, propagation was not spherical and it was very difficult to determine a flame radius, stretch rate or other parameters without making strong assumptions about the flame shape.

Firstly, no hypothesis on the flame shape was made and only an equivalent flame radius was estimated by considering the flame area as a disk.

Figure 6 4 Aluminium tested dusts Aluminium powder was provided by the company, "Métaux et Chimie", and referenced F3915.

For this study, this powder was modified by a converting treatment (anodising) in order to generate an oxide coating around the aluminium particles. This method was described by Baudry 0 al. (2007). It allows producing partially oxidised aluminium dust, in batches, in the range 0.5 -20 wt% of oxide. These content were measured by thermogravimetry analysis (TGA). The amount of oxide and residual water are given in Table 2. The dust was previously dried for 4 hours at 200°C. The TGA measurements show that a little content of water remains trapped in the particle and this value increases with the oxide content while this value was near zero for the F3915 where the oxide content is 0.5 wt% and only due to natural oxidation. All oxide content values were determined with accuracy of more than 0.02 wt%, and for a water content of no more than 0.005wt%. Nine different powders were tested and their characteristics are summarized in Table 2.

Table 2 5 Results on MIE measurement

An important parameter for MIE value was the initial mass of aluminium powder lying at the bottom of the Hartman tube. When the overpressure of discharged air was introduced through the nozzle in the lower part of tube, the powder was blown through the volume of the whole vessel.

Knowing the content of oxygen in the relative volume, it was possible to evaluate the equivalence ratio of the dust cloud. This ratio (see eq.1) is a macroscopic parameter and does not describe the reality of the dispersion which in all cases produced gradients of equivalent ratio in the volume. When the mass of Al powder increases from 190 mg to 350 mg, the equivalence ratio grows from 0.7 to 1.6. There is a strong decrease in the MIE energy in the first part of the curve (figure 7), after 1.1 the measurement is slightly intensified. The common shape of MIE for hydrocarbon/air gaseous mixtures is typically a U-curve (see figure 8). In the case of dust/air clouds, the right part of the U-curve was generally difficult to obtain because the energy of the flow needed to produce a good suspension is also enhanced. In such cases, a significant content of the initial powder still remains in the lower part of the test device and the real equivalence ratio of the dust cloud is not the expected one. Nevertheless, when the droplet size distribution of the powder is very narrow, which was the case of the powder d (powder A was sieved between 30 and 50µm), it is possible to observe the U-shape as shown in figure 8. These differences in the MIE values are principally due to the better fluidisation of narrow size distribution powder during the cloud generation.

Figure 8 A lot of studies were focused on aluminium combustion. All of them show the importance of the oxide layer on the particle surface. To ignite the particle, the oxide layer must be cracked by the thermo-mechanical stresses allowing to the oxygen of the air to react with the aluminium vapour by [START_REF] Ermakov | Temperature of Aluminium Particles at the Time of Ignition and Combustion[END_REF][START_REF] Brandford | Ignition and combustion temperatures determined by laser heating. Flammability and sensitivity of materials in oxygen-enriched atmospheres: ASTM STP 910[END_REF]. In this way, the thickness of the oxide layer and consequently the oxide content plays an important role in the ignition phenomenon of the particle. But only a few studies deal with the influence of oxide content on dust sensitivity or flame velocity. One reason is probably the difficulty of producing powder with an aluminium coating in a large range of oxide content to perform studies. In this work, this problem was solved by a sulphuric anodising of the powder by using an electrolytic process, but another problem subsists: oxidised powder is produced in batches so it is difficult to produce more than 30 g of oxidised powder. This content is enough to perform MIE measurement but only allows a few experiments in the combustion chamber. It allows the production of partially oxidised powder with an oxide content of between 1 to 17.2 wt%. The oxide is located on the surface of particles and sometimes some particles stick together. They are dried (200°C for 4 h) and sieved, the part below 50 µm is kept and tested in a Hartmann tube.

Figure 9 The MIE of oxidised aluminium powder was measured for various oxide contents. For each of them the aluminium equivalence ratio was maintained constant and equal to 1. During the test with large oxide content, particles were charged by an electrostatic process and attracted toward the walls of the tube. The use of antistatic adhesive along the tube walls drastically reduces the phenomenon. Langlie tests were also performed for very high oxide content such as 17.2 wt%.

Figure 9 presents the influence of the oxide content on the MIE which increases with the oxide content. For low oxide content, the MIE is quite the same as "non-oxidised" (only natural oxidation) aluminium particles (about 25 to 30 mJ) and is classified as very sensitive to electrostatic ignition. It is interesting to note that the MIE of highly oxidised particles such as 17.1wt% of oxide content is equal to 657 mJ: these particles are classified as sensitive to electrostatic ignition. It was also observed that some powder samples with lower oxide content have higher MIE (1460 mJ for 7.1wt% of oxide content); in this case these powders are classified insensitive to electrostatic ignition. Investigations with ATG show differences on the residual water content trapped in the oxide shell of the particle. It seems that this small content of water increases dust sensitivity. This aspect is significant on powder which contains 17,1wt% of oxide and 4.57wt% of water.

Flame measurement results

Figure 10 shows a typical radius time evolution during the explosion obtained with Matlab post processing. It is possible to discern three parts to this curve. The first one concerns the ignition:

the spark produces a short flash which is recorded by the camera. Secondly the combustion continues but propagates very slowly. This corresponds to the example presented in Figure 6a).

Progressively the flame accelerates: [START_REF] Sun | Structure of flames propagating through aluminum particles cloud and combustion process of particles[END_REF] also noted this acceleration in their apparatus with a similar order of magnitude. Finally after this acceleration, a quasi linear evolution of the radius with time is obtained: the flame velocity is nearly constant. It is in this last part of the curve that the flame velocity can be measured.

Figure 10 The load of aluminium dust injected in the chamber was varied in order to modify the equivalence ratio. Figure 11 illustrates the dependence of the flame velocity with equivalence ratio. A maximum is observed for a load of 4g. This content of powder gives an equivalence ratio of about 0.65 calculated by using the assumption of uniform dust concentration in the chamber.

In fact, the dispersion volume is lower, because we note that, after the cloud generation and when all particles have settled on the circular bottom of the bomb, there are hardly any particles near the walls, while dust deposit is greater near the centre of the bottom. The largest part of the uncovered zone is about 2 cm along the walls of the bomb. Therefore, the effective dispersion volume is lower and represents about 75% of the total volume with a particle concentration higher on the axes than on the edges of the dispersion volume. The maximum of the apparent flame propagation velocity observed is about 0.32 m/s. This value is not the laminar burning velocity: the expansion factor of aluminium combustion must be taken into account. Taking it into account, the value of the velocity obtained (0.015m/s <Su<0.025m/s with an expansion factor of 12) is lower than values (0.39 to 0.49 m/s) found in literature as example [START_REF] Silvestrini | Correlations for flame speed and explosion overpressure of dust clouds inside industrial enclosures[END_REF]. To better estimate the laminar burning velocity, the stretch, turbulence etc. need to be taken into account.

Figure 11 Figure 12 presents the apparent flame velocity with the oxide content of the aluminium dust. The equivalence ratio was fixed at 0.5 for each testing case. The velocity of flame decreases with the increase of the oxide content. It seems to be linear: the flame velocity decrease is of about 40%

when the oxide content is equal to 10wt%.

Figure 12

The great dispersion in measures obtain for Powder A is mainly due, for the greatest and the lowest values, to the absence of the powder scattering device during the cloud generation for these two points. All other points are obtained with the powder scattering device (see Figure 2b).

It is interesting to note that specially oxidised aluminium dust (17.2wt%-powder J) could present a flame velocity value near that of particles with low oxide content (0.5wt%-powder A). As for MIE results, one explanation is the role of the residual water contained in the dust samples (TGA measurement). In different samples, different groups of humidity content were identified. It seems that the humidity content, probably in the alumina shell around the particle, modifies combustion phenomena inducing the increase of the flame velocity.

This last remark is very interesting, whereas the effect of a high humidity level (probably more than 10 or 15 wt%) is to completely agglomerate dust and reduce the cloud generation, but a lower content (no more than 5wt%) increases the flame velocity of oxidised aluminium particles, and probably enhance the severity explosion.

Conclusions

In this study, traditional apparatus (i.e. Hartmann tube) combined with a statistical method developed by ourselves allows measurement of the MIE ignition energy. This experimental method was applied both in the case of organic combustible and aluminium dusts. This work provides new data obtained in the case of aluminium powders where the initial oxide content is controlled. Classical results, such as the influence of the equivalence ratio on the MIE, were confirmed. The influence of the initial oxide content was demonstrated and it was shown that the MIE increases with this parameter. Some dusts with a high oxide content (17.1 wt%) are sensitive to electrostatic ignition and present a hazard in industrial processes.

Flame velocity measurement shows that the flame velocity is reduced with the increase of oxide content, it can also be noticed that cloud generation and particle dispersion play an important role in the reproducibility of experiments. Differences on flame velocity are observed when the residual humidity of water is contained in the oxide shell of the particle. These differences are also identified for MIE. In these two cases, it seems that for a given oxide content, when the water content increases (from 1.4 to 1.7wt% for example) the flame velocity increases (from 0.25 m/s to 0.30 m/s) and the MIE decreases. It shows that the oxide shell, without water content mitigates the explosion ability of aluminium dust, but in presence of water in the oxide, which is almost always the case, this mitigation does not occur.

Figure 4 Figure 5

 45 Figure 4

  mass of oxygen, Al m the mass of aluminium powder injected and 2 O m the mass of oxygen.

  Figure 1: Hartmann tube and spark generator for MIE measurement

Figure 5 :Figure 6 :Figure 9 :

 569 Figure 5 : Voltage and current intensity time evolution of the spark

Table 2 :

 2 Figure 12 : Apparent flame velocity evolution with oxide content and for various water contents. Characteristics of tested dusts.

	F3915, H2Owt% < 0.7
	H2Owt% = 4.56
	H2Owt% < 0,47
	1.20<H2Owt% < 1.45
	1.59<H2Owt% < 1.70