Paul-André Melliès
email: mel-lies@pps.jussieu.fr

Asynchronous Games 4 A Fully Complete Model of Propositional Linear Logic

We construct a denotational model of propositional linear logic based on asynchronous games and winning uniform innocent strategies. Every formula A is interpreted as an asynchronous game [A] and every proof π of A is interpreted as a winning uniform innocent strategy [π] of the game [A]. We show that the resulting model is fully complete: every winning uniform innocent strategy σ of the asynchronous game [A] is the denotation [π] of a proof π of the formula A.

Introduction

By promoting a dynamic and interactive view on proofs and programs, game semantics has modified our basic understanding of both logical systems and programming languages. The semantic analysis has revealed that formulas and types describe games, and that proofs and programs describe strategies. Hence, cut-eliminating a proof against its refutation, or evaluating a program against its environment, amounts to playing a strategy σ against a counter-strategy τ . The play σ|τ resulting from the evaluation of σ against τ defines a "symbolic trajectory" which captures the essence as well as the syntactic details of the usual cut-elimination and evaluation procedures. Besides, the game paradigm was shown to apply to a large variety of programming languages, starting from PCF [START_REF] Abramsky | Full abstraction for PCF[END_REF][START_REF] Hyland | On full abstraction for PCF: I, II and III[END_REF][START_REF] Nickau | Hereditarily sequential functionals[END_REF] and Idealized AL-GOL [START_REF] Abramsky | Linearity, sharing and state: a fully abstract game semantics for idealized algol with active expressions[END_REF].

The remarkable success of game semantics in the analysis of proofs and programs should not hide the fact that, after less than fifteen years of active research, game semantics remains a young and experimental subject, full of promises but still a long way from maturity. Most notably, game semantics bumps since its origins against three extremely puzzling facts, without offering a proper solution to any of them. Taken separately, each fact is generally accepted as a minor defect in a beautiful and fruitful theory. Taken to-gether, they indicate that something fundamental remains to be understood about games. This is the starting point of this work. After reviewing the three facts, we explain how we managed to resolve them together in [START_REF] Melliès | Asynchronous games 3: an innocent model of linear logic[END_REF] with the notion of asynchronous game developed in [START_REF] Melliès | Asynchronous games 1: a grouptheoretic formulation of uniformity[END_REF][START_REF] Melliès | Asynchronous games 2: the true concurrency of innocence[END_REF][START_REF] Melliès | Asynchronous games 2: the true concurrency of innocence[END_REF]. This discussion conveys us to the main contribution of the paper: the formulation of a fully complete model of propositional linear logic, in the sense of [START_REF] Abramsky | Games and full completeness for multiplicative linear logic[END_REF].

Game semantics describes fragments of linear logicnot linear logic itself. Game semantics really emerged in the early 1990s when people realized after Blass [START_REF] Blass | A games semantics for linear logic[END_REF] that the formulas of linear logic describe sequential games. Abramsky and Jagadeesan notice in [START_REF] Abramsky | Games and full completeness for multiplicative linear logic[END_REF] that Blass model does not provide a satisfactory interpretation of proofs as deterministic strategies, because the model does not quite define a category: strategies may be composed as in a category, but composition is not associative. Much work has been devoted subsequently to construct proper categories of sequential games and deterministic strategies. Despite these efforts, only fragments of linear logic could be interpreted in this way, most notably:

• multiplicative linear logic (MLL) has the tensor product and the duality of linear logic, but no additives and no exponentials. The first game models of MLL are given by Abramsky, Jagadeesan, Hyland and Ong [START_REF] Abramsky | Games and full completeness for multiplicative linear logic[END_REF][START_REF] Hyland | Fair games and full completeness for multiplicative linear logic without the mix rule[END_REF] who refine the category of Conway games constructed by Joyal [START_REF]Remarques sur la théorie des jeux à deux personnes[END_REF] in order to obtain precise (that is, fully complete) models.

• intuitionistic linear logic (ILL) has the tensor product, the linear implication, the cartesian product, and the exponential modality of linear logic -but no duality. The first game models of ILL are given by Lamarche [START_REF] Lamarche | Sequentiality, games and linear logic[END_REF][START_REF] Curien | On the symmetry of sequentiality[END_REF] who linearizes in this way the sequential algorithm model of Berry and Curien [START_REF] Berry | Sequential algorithms on concrete data structures[END_REF]; and by McCusker [START_REF] Mccusker | Games and full abstraction for a functional metalanguage with recursive types[END_REF] who combines the work by Hyland and Ong on arena games [START_REF] Hyland | On full abstraction for PCF: I, II and III[END_REF] and by Abramsky, Jagadeesan, Malacaria on token games [START_REF] Abramsky | Full abstraction for PCF[END_REF]. Another interesting model of ILL appears in Hyland's survey on game semantics [START_REF] Hyland | Game semantics[END_REF].

• polarized linear logic (LLP) has all the connectives of linear logic -but formulas are restricted to Continuation Passing Style formulas (CPS formulas) by a polarity constraint. Girard introduces the idea of polarity in his work on LC and classical logic [START_REF] Girard | A new constructive logic: Classical logic[END_REF]. Laurent defines LLP and adapts to the logic the arena game model of Intuitionistic Logic [START_REF] Laurent | Polarized games (extended abstract)[END_REF].

Other less conventional game models have been designed, most notably a concurrent model of the multiplicative additive fragment [START_REF] Abramsky | Concurrent games and full completeness[END_REF], a non deterministic model of the multiplicative exponential fragment [START_REF] Baillot | Believe it or not, ajm's games model is a model of classical linear logic[END_REF], and two slightly mysterious game models of propositional linear logic [START_REF] Hyland | Games on graphs and sequentially realizable functionals[END_REF][START_REF] Hyvernat | Synchronous games, deadlocks and linear logic[END_REF]. However, it seemed hardly possible to formulate a sequential game model of propositional linear logic in the style of Blass games -until the asynchronous game model of propositional linear logic came out in [START_REF] Melliès | Asynchronous games 3: an innocent model of linear logic[END_REF]. The task of the present paper is precisely to refine this particular model in order to obtain a full completeness result.

Game semantics is affine -not linear. Another puzzling fact about game semantics is that the unit 1 of the tensor product and the unit ⊤ of the cartesian product are generally identified in game models of ILL. Typically, the two units are interpreted as the empty game, see [START_REF] Lamarche | Sequentiality, games and linear logic[END_REF][START_REF] Curien | On the symmetry of sequentiality[END_REF][START_REF] Mccusker | Games and full abstraction for a functional metalanguage with recursive types[END_REF][START_REF] Hyland | Game semantics[END_REF]. From a logical point of view, the equality 1 = ⊤ implies that the weakening rule may be applied on any formula A.

From a categorical point of view, the unit ⊤ is the terminal object of the underlying category of sequential games. Every strategy σ of a game B may be seen alternatively as a morphism 1 -→ B of the category. The equality 1 = ⊤ enables to compose this morphism to the canonical morphism A -→ ⊤ associated to any object A. The resulting strategy

A -→ 1 -→ B
is affine in the sense that it does not need to interact on the game A in order to complete the interaction on the game B. This departs severely from linear logic, in which every proof of the linear implication

A ⊸ B
uses its hypothesis exactly once. So, linearity in the precise sense of linear logic is not captured by usual game semantics, or only marginally by the notion of strict morphism [START_REF] Abramsky | Axioms for Definability and Full Completeness[END_REF]. Interestingly, linearity (identified to strictness) is the key ingredient of the asynchronous game model of linear logic formulated in [START_REF] Melliès | Asynchronous games 3: an innocent model of linear logic[END_REF] and will be one of the many elements of the present work.

Game semantics is sequential -not positional. The most puzzling fact about mainstream game semantics (eg. arena games [START_REF] Hyland | On full abstraction for PCF: I, II and III[END_REF][START_REF] Abramsky | Game semantics[END_REF] or token games [START_REF] Abramsky | Full abstraction for PCF[END_REF]) is certainly that the whole theory is developed without ever mentioning the notion of position of a game. A game is understood simply as a set of plays, where a play is defined as a (possibly justified) sequence of moves. Consequently, mainstream game semantics is purely "sequential" (that is, based on sequences) instead of being also positional. This lack of positionality conceals a fundamental aspect of games: different plays may reach the same position (or state) of the game; this position is what the plays compute, each play describing one particular trajectory to reach it. By way of illustration, the boolean game B implements a rudimentary computing device consisting of exactly one memory cell. The memory cell contains a boolean value, which may be either V (for "Vrai", the French word for "True") or F (for "False"). The game B is played in two steps. The user (Opponent) asks the value of the cell by playing the move q (for "question"). Then, the device (Player) answers by playing either the move true when the value is V or the move false when the value is F . The game is summarized in the decision tree below.

• • • true âa a a a false @ @ Ñ Ñ Ñ Ñ Ñ • q O O
The tensor product of linear logic enables to combine two boolean games B 1 and B 2 in order to implement the computing device consisting of two memory cells (we use the superscripts 1 and 2 only to distinguish the two boolean games). The resulting game B 1 ⊗ B 2 is played as follows.

Suppose that the first cell has value V and the second cell has value F in the current state of the device. The user (Opponent) may start by asking the value of the first cell. In that case, she plays the move q 1 and the device (Player) reacts by playing the move true 1 . The user may then ask the value of the second cell by playing the move q 2 , and the device will react by playing the move false 2 . The sequence of interactions constructs the left branch of the (fragment of) decision tree representing the game B 1 ⊗ B 2 :

• • • false2 W W H H H • true1 G G • q2 W W H H H • q1 G G • true1 W W H H H • false2 G G • q1 âa a a q2 @ @ Ò Ò Ò Ò (1)
Now, the user may permute his order of inquiry, and start by asking the value of the second cell, then the value of the first cell. The resulting sequence of four moves constructs the right branch of the decision tree. Since the order of inquiry is somewhat irrelevant, it is natural to think that the two branches should reach the same position of the game. This is represented in diagrams by bending the two branches of picture [START_REF] Abramsky | Axioms for Definability and Full Completeness[END_REF] and by drawing the decision tree as a graph:

• • false2 9 9 r r r r r r • true1 e e v v v v v v • q2 @ @ Ò Ò Ò • q1 ^`• true1 ^``• false2 @ @ Ò Ò Ò • q1 e e v v v v v v q2 9 9 r r r r r r (2)
This new picture is more informative than the previous one because it does not only indicate how Player and Opponent interact, but also what they compute: in that case, the state of the computing device, telling that the first cell has value V and the second cell has value F . Surprisingly, the positional intuition is never really exploited in mainstream game semantics. Nonetheless, the author discovered a few years ago that positionality is just there, hidden in the core of the theory, in the notions of arena game and innocent strategy. This unexpected discovery was the starting point of asynchronous games.

Asynchronous games. Asynchronous games are games played on asynchronous transition systems generated by event structures [START_REF] Panangaden | Stability and sequentiality in data flow networks[END_REF][START_REF] Winskel | Models for concurrency[END_REF]. An asynchronous transition system is a directed graph equipped with 2-dimensional tiles of the shape of a 1 × 1 square: From this follows an homotopy relation ∼ on plays, relating plays equal modulo permutation of moves. The term homotopy should be understood mathematically as (directed) homotopy in the topological presentation of asynchronous transition systems as a n-dimensional cubical sets [START_REF] Goubault | Geometry and concurrency: A user's guide[END_REF].

x ′
By way of illustration, this enables to refine picture (2) as the asynchronous game represented below:

V ⊗ F V ⊗ q false2 8 8 r r r r r ∼ q ⊗ F true1 f f v v v v v V ⊗ * q2 9 9 r r r r r ∼ q ⊗ q true1 v v f f v v false2 r r 8 8 r r ∼ * ⊗ F q1 e e u u u u u q ⊗ * true1 e e v v v v v q2 r r 8 8 r r ∼ * ⊗ q q1 v v f f v v false2 9 9 r r r r r * ⊗ * q1 f f w w w w w q2 8 8 q q q q q
In this 2-dimensional picture, the two plays of pictures ( 1) and ( 2) appear to be homotopic after a series of four permutations. Note also that every position is given a name (like q ⊗ * or V ⊗ F ) which reflects the current state of the computation.

Positionality. We explain in [START_REF] Melliès | Asynchronous games 1: a grouptheoretic formulation of uniformity[END_REF][START_REF] Melliès | Asynchronous games 2: the true concurrency of innocence[END_REF] how to formulate arena games and innocent strategies in the language of asynchronous games. This shift from arena games to asynchronous games is prerequisite if one takes positionality seriously. For instance, the naive idea that the current position x of a justified sequence s in an arena game may be simply defined as the set of moves (and pointers) which have been played... does not really work, for subtle reasons related to the interpretation of the exponential modality, and further discussed in [START_REF] Melliès | Asynchronous games 1: a grouptheoretic formulation of uniformity[END_REF].

A strategy of asynchronous game is defined in the usual "sequential" way, as a set of plays satisfying the usual properties of alternacy, determinism, etc. A strategy is innocent when it satisfies moreover two local consistency diagrams recalled in the Appendix (Figures 2 and3). The two diagrams replace the condition originally formulated in arena games that an innocent strategy plays according to the current Player view, see [START_REF] Hyland | On full abstraction for PCF: I, II and III[END_REF][START_REF] Nickau | Hereditarily sequential functionals[END_REF][START_REF] Abramsky | Game semantics[END_REF] for details.

By definition, a strategy σ plays a position x when there exists a play s ∈ σ with target x in the asynchronous game. The set of positions played by a strategy σ is denoted σ • . The main result of [START_REF] Melliès | Asynchronous games 2: the true concurrency of innocence[END_REF] is that every innocent strategy σ may be reconstructed from the set of positions σ • . In that sense, an innocent strategy is positional as well as sequential.

Moreover, once understood as positional strategies, innocent strategies compose just as relations: given two innocent strategies σ : A ⊸ B and τ : B ⊸ C, their composite σ; τ : A ⊸ C is the innocent strategy characterized by the equation:

(σ; τ ) • = {x ⊸ z | ∃y, x ⊸ y ∈ σ • ∧ y ⊸ z ∈ τ • }. (4)
Here, we write x ⊸ z for the position of A ⊸ C projecting on the position x in A and on the position z in C, and similarly for x ⊸ y and y ⊸ z.

Linearity. Shifting from a sequential to a positional point of view enables to resolve the points raised earlier in a very natural way. To every position x, one assigns an integer κ(x) ∈ Z called its payoff. Every strategy σ is then required to be a winning strategy, playing only on positions of positive payoff. Now, a typical arena game (without bracketing policy) is translated as an asynchronous game B in which all the positions are of null payoff, except for the initial position * B which is of payoff +1. The game starts by a move m by Opponent, followed by a move n by Player:

* B m → x n → y.
Suppose given another asynchronous game A of the same kind. In the definition of A ⊸ B appearing in [START_REF] Melliès | Asynchronous games 3: an innocent model of linear logic[END_REF] as well as in the present paper, Opponent starts the game by playing simultaneously a hidden move reaching the initial position * A of component A, and one initial move m reaching a position x in component B:

* A⊸B m → ( * A ⊸ x). (5)
A winning strategy of A ⊸ B cannot react to Opponent's move ( 5) by playing a move n in B. The resulting play

* A⊸B m → ( * A ⊸ x) n → ( * A ⊸ y) (6)
would indeed reach the position * A ⊸ y, whose payoff happens to be -1. We will not explain here how this payoff is calculated from the payoff +1 of * A in component A, and the null payoff of y in component B. This calculation is elementary, and will be explained at a later stage of the paper. What matters here is that the negative payoff of position * A ⊸ y compels every winning strategy of A ⊸ B to be strict: if the strategy reacts to Opponent's first move, it has to react by playing a move in component A.

Propositional linear logic. Hence, assigning payoffs to positions treats the second puzzling fact: linearity. But what about the first one? Unexpectedly, the positional point of view happens to be also the key to full propositional linear logic. We explain how after describing briefly the problem. The existing sequential game models of intuitionistic linear logic (ILL) define symmetric monoidal closed categories. In every symmetric monoidal closed category, there exists for every two objects A and ⊥ a canonical morphism:

∂ A : A -→ (A ⊸ ⊥) ⊸ ⊥.
An object ⊥ is called dualizing when this morphism is an isomorphism for every object A. A symmetric monoidal closed category with a dualizing object ⊥ is called a *autonomous category. Besides, a model of propositional linear logic is simply a model of ILL in which the underlying category happens to be * -autonomous, see [START_REF] Seely | Linear logic, * -autonomous categories and cofree coalgebras[END_REF][START_REF] Melliès | Categorical models of linear logic revisited[END_REF].

From that point of view, it should be noted that the existing symmetric monoidal closed categories of sequential games are nearly * -autonomous. There exists indeed a tentative dualizing object in these categories: the sequential game ⊥ with a unique move played by Opponent. Of course, the game ⊥ is not exactly dualizing. In fact, the game (A ⊸ ⊥) ⊸ ⊥ is obtained by lifting the game A twice: once by a Player move, then by an Opponent move. The resulting game is not isomorphic to the original game A... but not far from it! There exists indeed a strategy

ρ A : (A ⊸ ⊥) ⊸ ⊥ -→ A.
which defines with ∂ A a retraction between the two games. Of course, the composite ρ A ; ∂ A does not coincide with the identity of (A ⊸ ⊥) ⊸ ⊥: [START_REF] Abramsky | Concurrent games and full completeness[END_REF] and this is all the problem! If the two strategies were coinciding, the strategy ∂ A would be an isomorphism, and the category would be * -autonomous. This situation is interesting, but not particular to categories of games. Selinger [START_REF] Selinger | Control categories and duality: on the categorical semantics of the lambda-mu calculus[END_REF] notices that it occurs in fact in any control category. Again, the positional point of view leads to a very natural and elegant solution. Because the two strategies ∂ A and ρ A are innocent, equation ( 7) may be rewritten in the positional fashion:

ρ A ; ∂ A = id (A⊸⊥)⊸⊥
(ρ A ; ∂ A ) • = (id (A⊸⊥)⊸⊥ ) • . ( 8
)
It appears after inspection that the two sets of positions in (8) differ only on the very "early" positions of the game -which all have positive payoffs +1 or more. In particular, the two sets of positions coincide exactly on the positions with null payoff. This motivates to focus on the set of positions with null payoff of a strategy σ:

σ • = σ • ∩ {x | κ A (x) = 0}.
The equality follows:

(ρ A ; ∂ A ) • = (id (A⊸⊥)⊸⊥ ) • . (9)
This equality prompts us to call external any position of null payoff, and to identify any two innocent strategies σ and τ which play the same external positions -what we write σ ≃ τ . The intuition is that every innocent strategy σ realizes the set of external positions σ • . A position is called internal when it is not external. This distinction between external and internal position revisits traditional realizability, by integrating the realizer and the object it realizes in the same computational space, instead of treating them as separate and heteregeneous entities.

Remarkably, the fact expressed by equation ( 4) that composition is relational remains valid when one considers only the external positions of two winning innocent strategies:

(σ; τ ) • = {x ⊸ z | ∃y, x ⊸ y ∈ σ • ∧ y ⊸ z ∈ τ • }.
Consequently, the equivalence relation ≃ is preserved by composition: given two pairs of winning innocent strategies σ, σ ′ : A ⊸ B and τ, τ

′ : B ⊸ C, σ ≃ σ ′ and τ ≃ τ ′ ⇒ σ; τ ≃ σ ′ ; τ ′ .
We obtain in this way what we were looking for: Proposition 1 The category of asynchronous games and winning innocent strategies (modulo ≃) defines a *autonomous category.

Not only that: the category is cartesian, and leads to a model of propositional linear logic. The only difficulty is to interpret the exponential modality. As explained in [START_REF] Melliès | Asynchronous games 1: a grouptheoretic formulation of uniformity[END_REF], this is done by indexing copies in a way inspired by Geometry of Interaction [START_REF] Girard | Geometry of interaction I: interpretation of system F[END_REF] and token games [START_REF] Abramsky | Full abstraction for PCF[END_REF]. Every asynchronous game is then equipped with a left and right group action on the indices of these copies. A group-theoretic notion of uniform strategy replaces the notion of self-equivalent strategy designed by Abramsky, Jagadeesan and Malacaria in token games [START_REF] Abramsky | Full abstraction for PCF[END_REF]. This point is detailed in [START_REF] Melliès | Asynchronous games 1: a grouptheoretic formulation of uniformity[END_REF]. One obtains:

Proposition 2 The category of asynchronous games and winning uniform innocent strategies (modulo ≃) defines a model of propositional linear logic.

Full completeness. In the model, every formula A of propositional linear logic is interpreted as an asynchronous game [A] and every proof π of the formula A is interpreted as a winning uniform innocent strategy [π] of the game [A]. The model is fully complete when the converse property holds: every winning uniform innocent strategy σ of the game [A] is the denotation σ ≃ [π] of a proof π of the formula A. The model formulated in [START_REF] Melliès | Asynchronous games 3: an innocent model of linear logic[END_REF] is not fully complete, because it identifies the two formulas

(A&B) ⊗ ⊤ and (A ⊗ ⊤) & (B ⊗ ⊤) (10)
for any given formulas A and B. Note that the same problem occurs in the usual game models of intuitionistic linear logic, because the unit ⊤ coincides with the unit 1.

From the proof search point of view, the introduction rule of the additive unit ⊤: ⊢ Γ, ⊤ plays the role of a garbage collector: once the rule has collected the context Γ, the proof search succeeds. Proving one of the two formulas [START_REF] Blass | A games semantics for linear logic[END_REF] in a context Γ consists in applying the garbage collector on a piece ∆ of the context before proving the formulas A and B. The collected piece is the same for the two formulas A and B in the case of the formula (A&B) ⊗ ⊤, whereas it is selected independently for each formula A and B in the case of the formula (A ⊗ ⊤)&(B ⊗ ⊤). Consequently, the linear implication

(A&B) ⊗ ⊤ ⊸ (A ⊗ ⊤) & (B ⊗ ⊤).
holds in (intuitionistic) linear logic, but not its converse.

Bracketing revisited. In order to obtain a fully complete model of propositional linear logic, we thus need to refine the notion of winning strategy given in [START_REF] Melliès | Asynchronous games 3: an innocent model of linear logic[END_REF]. We achieve this by revisiting the well-bracketing condition of arena games [START_REF] Hyland | On full abstraction for PCF: I, II and III[END_REF][START_REF] Nickau | Hereditarily sequential functionals[END_REF][START_REF] Abramsky | Game semantics[END_REF]. We observe first that usual wellbracketing may be reformulated by assigning a payoff to every path of the game, indicating roughly the number of pending questions appearing in the path; then by requiring that every paths x -→ -→ y between two positions x, y ∈ σ • has positive payoff. However, the resulting condition is still not sufficient to obtain full completeness. We thus go further and require that every walk x ←→ ←→ y followed by the strategy σ between two positions x, y ∈ σ • , is of positive payoff, see Section 2 for a definition of walk. This generalized form of well-bracketing happens to be sufficient to establish full completeness. The reader may check for instance that it separates the two formulas [START_REF] Blass | A games semantics for linear logic[END_REF].

Contributions of this work. We solve in this paper a famous and longstanding problem of linear logic. The solution is far from straightforward. It results from the stubborn and meticulous analysis of asynchronous games reported in [START_REF] Melliès | Asynchronous games 1: a grouptheoretic formulation of uniformity[END_REF][START_REF] Melliès | Asynchronous games 2: the true concurrency of innocence[END_REF][START_REF] Melliès | Asynchronous games 3: an innocent model of linear logic[END_REF]. Many ideas and techniques are imported from these three papers. But the key to the full completeness theorem is formulated here for the first time: the extension of the payoff function from finite positions to finite walks. The proof of full completeness is also new, and extremely instructive on the very nature of linear logic.

Related works. Much of the related work has been already mentioned. The interested reader will also find sequential games played on graphs in the reformulation by Hyland and Schalk of the sequential algorithm model [START_REF] Hyland | Games on graphs and sequentially realizable functionals[END_REF].

Synopsis. The rest of the paper is structured in the following way. After the necessary preliminaries on event structures (Section 2) we define formally the notions of asynchronous arena and winning uniform innocent strategy (Section 3). We then construct the model of propositional linear logic (Section 4) and give an outline of the proof of full completeness (Section 5) before concluding (Section 6). We can only give an outline of the proof in this extended abstract; a detailed account is given in a draft full paper [START_REF] Melliès | Asynchronous games 4: a fully complete model of propositional linear logic[END_REF].

Event structures

Event structures. An event structure (M, ≤, #) is a partial order (M, ≤) whose elements are called events, equipped with a binary symmetric irreflexive relation #, satisfying:

• the set m ↓ = {n ∈ M | n ≤ m} is finite for every event m,
• m#n ≤ p implies m#p for every events m, n, p.

Two events m, n ∈ M are called incompatible when m#n, and compatible otherwise. Two events m and n are called independent when they are compatible: ¬(m#n), and incomparable: ¬(m ≤ n) and ¬(n ≤ m). In that case, we write:

m I n.
An event m is initial when m ↓ = {m} and second when m ↓ contains only initial events besides the event m itself.

Positions. A position is a downward closed subset of (M, ≤) consisting of pairwise compatible events. The set of (possibly infinite) positions defines a domain (complete pointed partial order) denoted D. The set of finite (resp. infinite) positions of this domain is denoted D fin (resp D ∞ .)

The positional graph. Every event structure A induces a graph G whose nodes are the finite positions x, y ∈ D fin , and whose edges m : x → y are the events verifying y = x ⊎ {m}. Here, we write ⊎ to mean that y = x ∪ {m} and that the move m is not element of x. Note that the graph G is rooted, with root the empty position noted * .

Tiles. The positional graph is also equipped with 2dimensional tiles expressing that two independent events m and n starting from the same position x may be permuted.

We use the notation ∼ to indicate a tile in our diagrams.

Walks. A walk w is a sequence

w = (x 0 , m ǫ1 1 , x 1 , ..., x k-1 , m ǫ k k , x k ) (11)
in which every x i is a finite position, every m i is a move, every ǫ i is a signature in {+1, -1}, and

m i : x i-1 → x i when ǫ i = +1, m i : x i → x i-1 when ǫ i = -1.
In that case, we write w : 0 ←→ ←→ x k and say that w crosses the positions x 0 , ..., x k . So, a walk is just a path in the non oriented graph associated to the graph G. The concatenation of two walks w 1 : x ←→ ←→ y and w 2 : y ←→ ←→ z defines a walk noted w 1 • w 2 : x ←→ ←→ z. We write W for the set of walks of the event structure.

3 Asynchronous games and strategies

The arenas Asynchronous arenas. An asynchronous arena

A = (M A , ≤ A , # A , λ A , κ A , κ ∞ A )
is an event structure whose events m ∈ M A are called the moves of the arena, equipped with:

• a polarity function λ A : M A → {-1, +1} on moves,
• a payoff function κ A : D fin A + W A → Z on finite positions and walks,

• a payoff function κ ∞ A : D ∞ A → {-∞, +∞} on infinite positions.
A move m with polarity λ A (m) = +1 (resp. λ A (m) = -1) is called a Player (resp. Opponent) move. Every asynchronous arena is required to satisfy the additional properties:

• every two initial moves m and n are incompatible: m # A n.

• the payoff of the initial position * A is either -1 or +1,

• the polarity of every initial move m is the opposite of the payoff of the initial position:

λ A (m) = -κ A ( * A ),
• the polarity of every second move n is the payoff of the initial position:

λ A (n) = κ A ( * A ),
• the payoff of an empty walk w : x ←→ ←→ A x is null,

• the payoff of a non-empty walk w : x ←→ ←→ A y which crosses the initial position * A is equal to the payoff κ A (y) of its target y.

The opposite of the payoff κ A ( * A ) is called the polarity of the arena, denoted π A . Thus, every initial move is Opponent in a negative game and Player in a positive game. A finite position x or a walk w is declared winning when its payoff is positive or null. An infinite position x is declared winning when its payoff is +∞. A finite position x is external when its payoff κ A (x) is null, and internal otherwise.

The strategies

Path. A walk w : x 0 ←→ ←→ x k as formulated in ( 11) is called a path from x 0 to x k when ǫ i = +1 for every index i. We write w :

x 0 -→ -→ x k in that case. A path is alternating when λ(m i+1 ) = -λ(m i ) for every index i ∈ [1, ..., k -1].
Play. A play is a path starting from the empty position * A .

Strategy. A strategy σ is a set of alternating plays such that, for every positions x, y, z, z 1 , z 2 :

1. the empty play ( * ) is element of σ, 2. every play s ∈ σ starts by an Opponent move, and ends by a Player move, 3. for every play s : * -→ -→ x, for every Opponent move m : x → y and Player move n :

y → z, s • m • n ∈ σ ⇒ s ∈ σ.
4. for every play s : * -→ -→ x, for every Opponent move m : x → y and Player moves n 1 : y → z 1 and n 2 :

y → z 2 , s • m • n 1 ∈ σ and s • m • n 2 ∈ σ ⇒ n 1 = n 2 .
Thus, a strategy is a non empty set (Clause 1) of even-length plays (Clause 2) closed under even-length prefix (Clause 3) and deterministic (Clause 4).

The innocent strategies

The notion of innocent strategy is introduced in [START_REF] Melliès | Asynchronous games 2: the true concurrency of innocence[END_REF] in order to reformulate the notion of innocence formulated originally in the language of arena games. A strategy σ is called innocent when it is backward consistent and forward consistent in the following sense.

Backward consistency. A strategy σ is backward consistent (see Figure 2 in Appendix) when for every play s 1 , for every path s 2 , for every moves

m 1 , n 1 , m 2 , n 2 ∈ M A , it follows from s 1 • m 1 • n 1 • m 2 • n 2 • s 2 ∈ σ and n 1 I m 2 and m 1 I m 2 that n 1 I n 2 and m 1 I n 2 and s 1 • m 2 • n 2 • m 1 • n 1 • s 2 ∈ σ.
Forward consistency. A strategy σ is forward consistent (see Figure 3 in Appendix) when for every play s 1 and for every moves

m 1 , n 1 , m 2 , n 2 ∈ M A , it follows from s 1 •m 1 • n 1 ∈ σ and s 1 • m 2 • n 2 ∈ σ and m 1 I m 2 and m 2 I n 1 that m 1 I n 2 and n 1 I n 2 and s 1 • m 1 • n 1 • m 2 • n 2 ∈ σ.

Positions and walks on a strategy

Finite position of a strategy. The set of finite positions played by a strategy σ is defined as

σ • = {x ∈ D A | ∃s ∈ σ, s : * A -→ -→ x}.
Infinite position of a strategy. An infinite play s is defined as a sequence of moves:

* A m1 → x 1 m2 → x 2 • • • x k-1 m k → x k m k+1 → x k+1 • • • (12)
The target position x of such an infinite play s is defined as:

x = i∈N x i = {m i | i ∈ N}.
In that case, we write s : * A ∞ -→ -→ x. Given a strategy σ, the set σ ∞ denotes the set of infinite plays [START_REF] Girard | Geometry of interaction I: interpretation of system F[END_REF]

such that * A m1 → x 1 m2 → • • • m 2k → x 2k
is element of the strategy σ, for every index k ∈ N. Then,

σ •• = {x ∈ D A | ∃s ∈ σ ∞ , s : * A ∞ -→ -→ x}.
Alternating walks. A walk is alternating when

λ A (m i+1 ) × ǫ i+1 = -λ A (m i ) × ǫ i for every index i ∈ [1, ..., k -1].
Here, (-× -) denotes the usual product of two signatures in the ring Z. So, at each step of an alternating walk w, either the direction ǫ i or the polarity λ(m i ) of the move changes. This generalizes the previous notion of alternating play. A typical alternating walk w : x 0 ←→ ←→ x k looks like this:

y x k x 0 s1 > > > > ~z s2 _ _ _ _ b b b b b b b s3 > > > > } } } } } } } }
where s 1 , s 2 and s 3 are alternating plays, the last moves of s 1 and s 2 are of the same polarity, and the first moves of s 2 and s 3 are of the same polarity.

Walk on a strategy. A walk w on a strategy σ is defined as an alternating walk (11) satisfying:

• λ A (m 1 ) × ǫ 1 = -1 and λ A (m k ) × ǫ k = +1,
• every position x 2i is a position of the strategy σ,

for i ∈ [0, ..., k 2 ].
Note that the length k of the walk is an even number by the first clause, and by the definition of an alternating walk. This justifies the use of the fraction k 2 as a natural number in the last clause.

The winning strategies

A strategy is winning when the four conditions below are satisfied: This definition extends the definition of winning strategy in [START_REF] Melliès | Asynchronous games 3: an innocent model of linear logic[END_REF] which required only totality and positive payoff on finite positions. The payoff condition 3. on infinite positions reformulates the usual winning condition on strategies [START_REF] Hyland | Game semantics[END_REF]. The payoff condition 4. on walks strengthens the usual wellbracketing condition of arena games -in order to achieve full completeness.

Asynchronous games and uniform strategies

Asynchronous games. An asynchronous game A is an asynchronous arena equipped with a left and right group actions on moves:

G A × M A × H A -→ M A
satisfying four coherence axioms given in [START_REF] Melliès | Asynchronous games 1: a grouptheoretic formulation of uniformity[END_REF]. These axioms ensure that the actions on moves extend to actions on plays, in a pointwise manner. The action of two elements g ∈ G A and h ∈ H A on a play s = m 1 • • • m k is thus defined as follows:

g s h = (g m 1 h) • • • (g m k h).
Uniformity. The definition appears in [START_REF] Melliès | Asynchronous games 1: a grouptheoretic formulation of uniformity[END_REF]. A strategy σ is uniform when for every play s ∈ σ and every h ∈ H A , there exists g ∈ G A such that g s h ∈ σ. Uniformity reformulates the notion of self-equivalent strategy in [START_REF] Abramsky | Full abstraction for PCF[END_REF].

The model of propositional linear logic

We explicate below our asynchronous game model of propositional linear logic. For lack of space, we will not describe here the group actions associated to each game; we refer the reader to [START_REF] Melliès | Asynchronous games 1: a grouptheoretic formulation of uniformity[END_REF] for a detailed account.

Dual. The dual A ⊥ of an asynchronous game A is obtained by reversing the polarity of moves and the payoffs of positions and walks. Note that the operation is involutive: A ⊥⊥ = A; and that the dual of a positive game is a negative game, and conversely.

Lifting. The positive lifting (with payoff p) of a negative asynchronous game A is the positive game ↓ p A (often written ↓ A when no confusion is possible) defined below:

• M ↓A = M A + {new} with m # ↓A n ⇐⇒ m # A n, and
m ≤ ↓A n ⇐⇒ m = new, or m ≤ A n,
• κ ( * ↓A ) = -1; and κ ↓ p A ({new}) = p; κ ↓A (y) = κ A (x) when y = x ⊎ {new},

• κ ↓A (w) = κ A (w) when the walk w does not contain the initial position * ↓A ; κ ↓A (w) = 0 when w is the empty walk on the initial position * ↓A ; κ ↓A (w) = κ ↓A (y) when the walk w : x ←→ ←→ ↓A y is non empty and contains the initial position * ↓A ;

• κ ∞ ↓A = κ ∞ A .
This defines by duality a negative lifting ↑ p A on positive games.

Affine vs. linear lifting. Two lifted games ↓ p A and ↓ q A differ only on the payoff of the position {new}. This enables to distinguish the linear lifting and the affine lifting of a negative game A, defined respectively as ↓ +1 A and ↓ 0 A.

Sum. The sum of two positive games A and B is the positive game A ⊕ B defined below:

• M A⊕B = M A + M B , ≤ A⊕B =≤ A + ≤ B , and
m # A⊕B n ⇐⇒        m # A n, or m # B n, or m ∈ M A and n ∈ M B , or m ∈ M B and n ∈ M A ,
• κ A⊕B (y) = κ A (x) when y = inl(x) and κ A⊕B (y) = κ B (x) when y = inr(x), where inl and inr are the left and right injections

D A → D A⊕B ← D B ,
• κ A⊕B (w) = κ A (w) when w is a walk in the component A; κ A⊕B (w) = κ B (w) when w is a walk in the component B; κ A⊕B (w) = κ A⊕B (y) when w : x ←→ ←→ A⊕B y is a walk on the two components A and B,

• κ ∞ A⊕B = κ ∞ A + κ ∞ B .
This definition extends easily to the sum i∈I A i of a family (A i ) i∈I of positive games.

Tensor product. Every positive game P may be seen as a sum i∈I ↓ pi L i of a family of lifted negative games L i . The tensor product of two positive games

P = i∈I ↓ pi K i and Q = j∈J ↓ qj L j
is defined as the positive game

P ⊗ Q = (i,j)∈I×J ↓ pi K i ⊗ ↓ qj L j
where ↓ pi K i ⊗ ↓ qj L j is defined as the lifting

↓ pi K i ⊗ ↓ qj L j =↓ pi⊗qj N (i,j)
of the negative game N (i,j) defined in the following way:

M N (i,j) = M Ki + M Lj ≤ N (i,j) =≤ Ki + ≤ Lj and m # N (i,j) n ⇐⇒ m # Ki n, or m # Lj n.
The payoffs κ x and κ w and κ ∞

x are computed by projecting the position x, and the walk w on each component K i and L j , and then by applying the calculation table of Figure 1 -in which the payoffs in K i and L j appear in the first row and first column. Note that the table is symmetric in K i and L j because the tensor product is commutative.

Units. The unit 0 is the positive game with no move. The unit 1 is the affine lifting ↓ 0 ⊤ of the dual ⊤ of the unit 0.

⊗

-∞ -p 0 +p +∞ -∞ -∞ -∞ -∞ -∞ -∞ -q -∞ -p -q -q -q +∞ 0 -∞ -p 0 p +∞ +q -∞ -p q p + q +∞ +∞ -∞ +∞ +∞ +∞ +∞ Figure 1.
The table for calculating the payoff p ⊗ q from the payoffs p and q.

Linear logic. The tensor product and the sum are called positive connectives because they are naturally defined on positive games, see [START_REF] Girard | A new constructive logic: Classical logic[END_REF][START_REF] Laurent | Polarized games (extended abstract)[END_REF]. We use the linear lifting ↓ +1 and ↑ -1 in order to extend the definition to any (positive or negative) asynchronous game. Typically, the sum A ⊕ B and the tensor product A⊗B of two asynchronous games A and B is defined by lifting first the negative games (if any), then applying the earlier construction on positive games. The tensor product A ⊗ B is thus defined as:

A ⊗ ↓ +1 B when A is positive and B negative,

↓ +1 A ⊗ B
when A is negative and B is positive, ↓ +1 A ⊗ ↓ +1 B when A and B are negative, and similarly for the sum construction. Identically, the positive lifting ↓ k of a positive game A is defined as:

↓ k A = ↓ k ↑ -1 A .
B = (A ⊥ ⊗ B ⊥ ) ⊥ .
Exponentials. The exponential modality ! is defined by decomposing it as the affine lifting ↓ 0 followed by an infinite tensor product:

!A = i∈N ↓ 0 A (13)
This decomposition is one of the two decompositions studied by Jacobs in [START_REF] Jacobs | Semantics of weakening and contraction[END_REF].

As already explained in the introduction, we identify any two strategies σ and τ playing the same positions of null payoff, what we write σ ≃ τ . We then construct a category with asynchronous games A, B as objects, and uniform winning innocent strategies of A ⊸ B = A ⊥ . . . . . . . . . . . . . . . . . . . . . . . . . Note that the three asynchronous games A, ↓ p A and ↑ p A are isomorphic in this category, when p = 0.

Full completeness

Our proof of full completeness is based on a directed proof search. We start from a uniform winning innocent strategy σ of the asynchronous game [A], and we search a proof π of the formula A, such that [π] = σ. This search is driven by the strategy σ. The distinctive difficulty compared to other similar proofs of full abstraction for PCF [START_REF] Abramsky | Full abstraction for PCF[END_REF][START_REF] Hyland | On full abstraction for PCF: I, II and III[END_REF][START_REF] Nickau | Hereditarily sequential functionals[END_REF] or of full completeness for LLP [START_REF] Laurent | Polarized games (extended abstract)[END_REF] is that the contexts involved are not affine anymore. This requires to deal explicitly with the context. The proof is done in three stages.

Stage 1. We establish full completeness for the multiplicative additive fragment enriched with the lifting modalities ↓ p and ↑ p . A good part of the difficulties are already there! When it is Player's turn to play, the MALL sequent may be written as

⊢ Γ , ↑ p ( ↓ q1 M ⊗ ↓ q2 N )
where Γ =↑ p1 P 1 , • • • , ↑ p k P k is a sequence of lifted positive formulas (we use the language of LLP here). Suppose that the strategy σ plays the move m which "plays" the tensor ↓ q1 M ⊗ ↓ q2 N . Then, one may deduce from the diagrammatic properties of innocence that the strategy σ splits the context in three parts: Γ 1 is the part "connected" to the formula M , Γ 2 is the part "connected" to the formula N , and Γ 3 is the part not connected to anything. The payoff condition on walks then ensures that the strategy σ itself "splits" in two winning innocent strategies σ 1 and σ 2 of the sequents:

⊢ Γ 1 , M ⊢ Γ 2 , N
The proof is then concluded by induction on the size of σ.

Stage 2. The full completeness result established at stage 1 is extended to a non uniform variant of linear logic, in which a proof π of the formula !A is defined as a family of proofs (π k ) k∈N of the formula A. Every winning innocent strategy σ is shown to be the interpretation of a proof π.

Stage 3. Every uniform winning innocent strategy σ is shown to be the interpretation of a proof π of usual linear logic. This completes the proof:

Theorem 4 (Full Completeness) Asynchronous games and uniform winning innocent strategies define a fully complete model of propositional linear logic.

Conclusion and future works

We formulate a fully complete model of propositional linear logic for the first time. The construction requires to introduce a rich body of techniques: asynchronous games, internal vs. external positions, payoffs on walks, non uniform linear logic, etc. These techniques generalize and clarify the usual notions of mainstream game semantics: arena games, well-bracketing, uniform strategies, etc. The next step will be to see how these new ideas clarify the current game models of references in programming languages [START_REF] Abramsky | Linearity, sharing and state: a fully abstract game semantics for idealized algol with active expressions[END_REF][START_REF] Abramsky | Fully abstract game semantics for general reference[END_REF]. By this line of research, we expect to see an asynchronous geometry of programming languages and interactive behaviours emerge slowly -at the crossing point of the Curry-Howard isomorphism, the object-based semantics of states advocated by Reddy in [START_REF] Reddy | Global state considered unnecessary: Introduction to object-based semantics[END_REF] and the geometry of concurrency described in [START_REF] Goubault | Geometry and concurrency: A user's guide[END_REF]. The full completeness theorem established in the present paper is certainly an important and encouraging step in that direction.

  with edges m • n and n • m indicates that the two moves m and n may be permuted in a play, what one writes m • n ∼ n • m.

1 .

 1 totality: given any play s • m in which s ∈ σ and m is an Opponent move, there exists a Player move n such that s • m • n ∈ σ, 2. finite positions: the payoff of every finite position x ∈ σ • is positive or null, 3. infinite positions: the payoff of every infinite position x ∈ σ •• is positive or null, 4. walks: the payoff of every alternating walk on the strategy σ is positive or null.

  De Morgan duality. The two negative connectives of linear logic are then deduced by De Morgan duality:A&B = (A ⊥ ⊕ B ⊥ ) ⊥ A

	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

  . . . .

	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . B as
	morphisms A -→ B. We obtain:
	Proposition 3 The resulting category defines a model of
	propositional linear logic.

This work has been supported by the FNS ACI Géométrie du Calcul (GEOCAL).

Appendix: the two figures of innocence


S F Matar
email: s.matar@u-bordeaux1.fr

A Houari

M A Belkhir

Ab initio studies of magnetic properties of cobalt and tetracobalt nitride Co 4 N

Keywords: numbers: 71.15.Mb, 71.15.Nc, 71.20-b, 75.10.Lp, 74.25.Ha, 73.43.Cd

Magnetic properties and bonding analyses of perovskite structure Co 4 N nitride have been investigated within density functional theory using both pseudo potential and all electron methods.

In the same time, the structural and magnetic stability of pure cobalt in hexagonal close packed (HCP), face centered cubic (FCC) and body centered cubic (BCC) structures are reviewed. At equilibrium, non-spin polarized (NSP) and spin polarized (SP) calculations of the energy versus volume show that the ground state is ferromagnetic in both materials. HCP-Co is found to be more stable than the cubic ones. Magnetic moments of Co atoms in Co 4 N nitride respectively belonging to two different crystallographic sites are studied over a wide range of the cubic lattice constant, and a comparison with the FCC-cobalt one is given. The volume expansion in the nitride indicates that the corner Co I atoms show localized magnetism while face center Co II atoms exhibit an itinerant behavior. Like in FCC-Fe/Fe 4 N, a "low volume-low moment" and "large volume-high moment" behavior is observed for FCC-Co/Co 4 N. The density of states of the Co 4 N ferromagnetic ground state is interpreted within the rigid band model. The different bonding characters of Co I -N versus Co II -N are shown with help of electron localization fucntion ELF plots and spin resolved chemical bonding criteria.

I. INTRODUCTION

With respect to their thermal, mechanical and magnetic properties, the transition metal nitrides are known to be very interesting in many technological areas. For example, in the field of high density magnetic recording, iron nitrides are applied [1][2][3][4][5]. Unlike iron nitrides, the cobalt nitrides seem to be less explored and there are only few studies which treat their magnetic properties. The cobalt-nitrogen system was reported to contain many phases ranging from Co 4 N to CoN [6][7][8][9][10][11]. In the cobalt-rich side, a cubic Co 4 N was synthesised with a lattice constant of 6.7788 bohr (1 bohr=0.529 Å), but no magnetic data were given [7]. On the other side bulk Co 2 N was prepared with an orthorhombic Fe 2 C-type structure [10], whereas no structure was indexed in Co 2 N thin films [11]. However, the case of CoN mononitride seems somewhat conflicting. Like what happens in the iron mononitride [12], it was early reported in cubic rocksalt structure [9], but recently it was found in a paramagnetic zinc-blende type one [13]. On the theoretical side a lack of data about the cobalt nitrides is noted. Except some density functional calculations on CoN [14,15], no calculations are carried out for Co 2 N and Co 4 N. Nevertheless, for the latter some studies on antiperovskite cobalt-substituted Fe 4 N, i.e. CoFe 3 N, have been undertaken [16,17].

From the structural point of view, Co 4 N can be assimilated as an insertion of N atom in FCC-cobalt. In this context, a reinvestigation of cobalt metal, at the same time as Co 4 N could be useful for a better understanding of the nitride magnetic properties; especially the Co-N interaction.

Many experimental and theoretical reports have been carried out in order to study the three known structural types of cobalt, namely body centered cubic (BCC), face centered cubic (FCC) and hexagonal close packed (HCP), see [18][19][20][21][22][23][START_REF] Donahue | The structures of the elements[END_REF][START_REF] Modak | [END_REF][26] and references therein. Under ambient conditions of temperature and pressure, Co is well known to crystallize in hexagonal close packed (HCP) structure. Experimentally a lattice constant in the vicinity of a=4.739 bohr, a c/a parameters ratio between 1.615-1.623 and an atomic magnetic moment of ∼1.6μ B were found [18][19][20][21]. These results were confirmed later by density functional based calculations [22][23]. Further the stabilization of cobalt in BCC-structure [20], a structural transformation between the two close packed structures: FCC and HCP are also known to occur in cobalt [21]. Recently, the stability of the two latter structures was investigated theoretically but BCC-Co was not included [START_REF] Modak | [END_REF]. To our knowledge, the only work which includes the three types of structures is the one of Min et al [23] but within the framework of local spin density approximation (LSDA) to the density functional theory [28]. In this context, it is important to remind the well known drawback of this energy functional in predicting the ferromagnetic BCC-ground state of iron [29] which was of a major impetus in the development of generalized gradient approximation (GGA) [30].

The lack of theoretical as well as experimental data concerning Co 4 N (and in general on the Co-N system), has motivated us to carry out a first principles study. The aim of this present work is to assess the chemical role of nitrogen within Co 4 N and to check whether the variation for the magnetic moments at different lattice sites follows the trends of cobalt metal in the same FCC-like structure through magnetovolume effects.

The present paper is organized as follows. In section II the computational framework of calculations and the methods are briefly presented. It is followed by a section, divided in two parts. The first part describes and discusses the phase stability and magnetic moments in cobalt; the second one is devoted to the Co 4 N electronic structure and magnetic properties, where these are treated in details by means of partial density of states and chemical bonding assessments. Finally, section IV presents the conclusions.

II. COMPUTATIONAL FRAMEWORK AND METHODS

Two computational methods were used in the framework of density functional theory.

For a description of the electronic and magnetic structures, the all electrons augmented spherical wave (ASW) method [START_REF] Eyert | The Augmented Spherical Wave Method -A Comprehensive Treatment[END_REF] was used. The exchange-correlation effects were accounted for within the generalized gradient approximation (GGA) using the parameterization of Perdew, Burke and Ernzerhof [32]. This scheme was preferred over the LDA (local density approximation) in view of the recent results on iron mono nitrides [12]. In the ASW method, the wave function is expanded in atom-centered augmented spherical waves, which are Hankel functions and numerical solutions of Schrödinger's equation, respectively, outside and inside the so-called augmentation spheres. In order to optimize the basis set, additional augmented spherical waves were placed at interstitial sites corresponding to middle of cube edges of the open (in the sense of non close packed) perovskite structure of Co 4 N. The cobalt 4s, 3d and nitrogen 2s, 2p states were treated as valence states. The basis set was complemented by wave functions of s-, p-, and possibly, d-symmetry centered at the interstitial sites which ensure for the covalence effects within the lattice. A sufficiently large number of k points was used to sample the irreducible wedge of the Brillouin zone, and the energy and charge differences between successive iterations were converged below ΔE=10 -8 Ryd. and ΔQ=10 -8 , respectively, in order to obtain accurate values of the magnetic moments and total energy differences between various ordered magnetic states.

To extract more information about the nature of the interactions between the atomic constituents from electronic structure calculations, the crystal orbital overlap population (COOP) [33] or the crystal orbital Hamiltonian population (COHP) [34] may be employed.

Both approaches provide a qualitative description of the bonding, nonbonding and antibonding interactions between two atoms. A slight refinement of the COHP was recently proposed in form of the 'energy of covalent bond' (ECOV), which combines COHP and COOP to calculate quantities independent of the choice of the zero of potential [35]. Both COOP and ECOV give similar general trends, but COOP, when defined within plane-wave basis sets, exaggerates the magnitude of antibonding states. In the present work the ECOV description was used for the chemical bonding analysis. In the plots, negative, positive and zero ECOV magnitudes are relevant to bonding, antibonding and nonbonding interactions respectively.

In as far as no structural determination is available for Co 4 N trends in cell volumes and ground state crystal structure were desirable in the first place. The equilibrium structures were obtained from a full geometry relaxation of nitride systems starting from Fe 4 N structural setup and using a pseudo potential approach within the VASP code [36]. Ultra soft Vanderbilt pseudo potentials (US-PP) [37] built within GGA scheme [32] were used. The calculations were converged at an energy cut-off of 435.12 eV for the plane-wave basis set with respect to the k -point integration with a starting mesh of 6*6*6 up to 12*12*12 for best convergence and relaxation to zero strains. The tetrahedron method with Blöchl corrections [38] was applied leading from 141 to 1569 inequivalent tetrahedra. The Brillouin-zone integrals were approximated using a special k-point sampling.

III. RESULTS AND DISCUSSIONS.

A. Cobalt metal.

The volume dependence of the total energy for spin polarized (SP) ferromagnetic and non-spin polarized (NSP -meaning a non magnetic spin degenerate system) configuration for the three cobalt phases: BCC, FCC and HCP are displayed in figure 1-a, 1-b and1-c, respectively. The ferromagnetic state is largely preferred over the non-magnetic one in all 3 different structures. The lowest energy in the spin polarized configuration is obtained for HCP-Co which is the ambient form of cobalt. This structural stability in the spin-polarized case is better illustrated in figure 1-d, where the E(V) plots for the three structures are shown together in the SP ferromagnetic state. Between HCP and FCC cobalt, a small energy difference ΔE(SP-NSP)∼0.2 eV/atom is obtained; this agrees well with the low magnitudes reported experimentally and points to the possible coexistence of the two phases at some high pressure range [21]. Furthermore, considering the non magnetic state where FCC cobalt is more stable than HCP-Co, one should conclude that the spin polarization is in favour of the latter. Our calculations at low volume show that the HCP-phase remains (ferro)magnetic whereas FCC one begins to lose the magnetic character (becomes non magnetic) while being more stable than the former. This finding is in agreement with the recent experimental observations of a non magnetic FCC-phase preferred to the HCP one in cobalt under high pressure [21]. From figure 1-d, the theoretical equilibrium volumes are nearly equal for HCP and FCC phases (∼78.27 bohr 3 .atom -1 ), whereas the BCC one is slightly larger (∼79.51 bohr 3 .atom -1 ). In terms of total energy, and as confirmed by recent theoretical study [26], a BCC-cobalt phase as bulk material should not be stable at ambient pressure. Nevertheless, the experimentally stabilized BCC cobalt thin films [20] were explained to originate from such imperfections or substrate lattice constant mismatch at an early stage of growth. Furthermore a critical thickness above which the BCC phase begins to transform to HCP one was identified [27]. In HCP-cobalt, our c/a ratio (1.603) and magnetic moment (1.634 μ B ) are in good agreement with experiments [18][19][20][21] and in better agreement than recent full potential calculations [START_REF] Modak | [END_REF]. For FCC cobalt no experimental report is available for the cobalt magnetic moment; on the other hand our computed value of ∼1.67 μ B is in good agreement of theoretical results both in LSDA [23] and GGA [START_REF] Modak | [END_REF] exchange-correlation functionals. As for BCC-Co, it needs to be stressed that our 1.757 μ B moment magnitude which agrees with computed LSDA [23] one, is larger than the only reported experimental value of 1.53 μ B [20].

B. Tetracobalt nitride Co 4 N.

Geometry optimization and electron localization from pseudo potential calculations.

We started the geometry optimization by using Fe 4 N structural setup with a lattice parameter from experiment: a=7.165 bohr. We recall that this structure can be viewed from a cubic perovskite lattice: ABX 3 where A is a large cation at corner, B is a smaller cation at cube center and X is an anion at face centers. From this Co I Co II 3 N is an anti-perovskite because Co II replace X anion sites at face centers. Then the lattice geometry was fully relaxed for the cell volume, shape and atomic positions. The calculations were carried out for both non magnetic and spin polarized configurations. The resulting structure was found to be cubic with lattice constants: a NSP (Co 4 N)=6.975 bohr, a SP (Co 4 N)=7.062 bohr, with an energy difference of ΔE(SP-NSP)= -0.982 eV favoring the spin polarized configuration.

The experimental value of a exp. (Co 4 N)= 6.779 bohr [7] is significantly smaller and this calls for an interpretation.

One explanation can be found in the possibility of existence of N vacancies within the lattice. A geometry optimization with a nitrogen deficient system was carried out calling for a new cell set up. Starting from a supercell with 8 formula units leading to 32 Co and 8 N, the above calculated lattice constant of Co 4 N was checked firstly. Then vacancies were created at nitrogen sites. With 2 N vacancies, a small change of lattice constant is obtained with a= 6.925 bohr; with 4 nitrogen vacancies the calculated lattice constant becomes smaller with a = 6.762 bohr. This magnitude comes close to the experimental value. When all 8 nitrogen sites are vacant, a lattice constant of a= 6.539 bohr is reached.

These results support the potentiality of a partly nitrogen deficient lattice in the sense of the existence of some nitrogen lacking domains with stoichiometries such as Co 4 N 1-x , beside fully stoichiometric Co 4 N. While such a result is not reported experimentally [7], we suggest that nitriding conditions calling for high nitrogen pressures can be useful to obtain the stoichiometric compound [39]. Although the supercell calculation results allowed to clarify the hypothesis of nitrogen vacancies with the tetracobalt nitride lattice, it should be kept in mind that they assumed an ideal bulk lattice with an ordered distribution of nitrogen atoms and vacancies, while in experimental reality those should be randomly distributed with possible surface effects.

A quantity that can be extracted from calculations is the electron localization function ELF which allows determining the amount of localization of electrons with respect to the free electron gas distribution as described by Becke and Edgecomb [40]. Figure 2 shows a < 101 > diagonal plane crossing all atomic sites of Co 4 N. This illustration stresses the isolated character of the corner sites Co I at a √ 3/2 from N with respect to face center cobalt

Co II which are at a/2 from N. Further there is a non negligible localization along Co II -N-Co II direction. Nitrogen exhibits the largest localization (large white area around it) in agreement with the description of the system as a "nitride" from the chemical view point.

On the contrary, the metal sites show no localization (dark areas) due to their electropositive character so that electrons are smeared out in between the lattice sites (light grey areas) like in a metal, which is the characteristics of the system under study.

C. Analysis of the electronic and magnetic structure

In this section, we investigate in detail the magnetic and electronic properties of pure our magnetic moments agree with reference [16] for cobalt Co I (situated in the corners) and for nitrogen; whereas a large difference exists for Co II . This fact is expected because the previous authors have substituted only one of the three face centers irons, and thus their Co II moments (0.842μ B , see [16]), are largely affected by the neighbouring irons. Nevertheless, our Co I moment is smaller than 2.26μ B computed in ref. [17] for CoFe 3 N.

Comparison of FCC-Co versus Co 4 N

The magnetovolume effect of nitrogen insertion within Co 4 N is illustrated in figure 3. is subjected to the chemical presence of neighboring N atoms at a/2 and the strong p-d hybridization makes its moment vary slowly with the volume until a sufficient value (beyond the FCC-Co equilibrium) where its variation begins to be more pronounced. From this, it can be concluded that the two kinds of moment variation in FCC-Co are simultaneously present in Co 4 N and this is due to the insertion of N atom. We note finally that this behavior is observed, with almost the same manner as in Fe 4 N versus FCC-Fe [41,42].

Moreover, since Co

Analyses of the density of states and bonding properties

Using equilibrium values of lattice constants determined above, we examine the spin (↑ and ↓) and site projected density of states (PDOS) accounting for site multiplicity in the formula unit: 1Co I , 3Co II and 1N. This is shown in figure 4. Further, for sake of comparison we present the DOS of three studied varieties of Co in figure 5 at equilibrium lattice volumes (cf. fig. 1). From the very low spin ↑ DOS at the Fermi level due to the filling of the Co(3d ↑ ) sub band up to 5 electrons, the major feature of the latter is its strong ferromagnetic behavior in all three varieties; we note the resemblence of BCC-Co DOS with BCC-Fe DOS [START_REF] Mohn | Magnetism in the solid State, An Introduction[END_REF]. Thus from the point of view of strength of magnetic behavior cobalt is like FCC-Ni whose pressure for the disappearance of magnetic moment is ∼4000 kbar, contrary to BCC-Fe which is a weak ferromagnet [START_REF] Mohn | Magnetism in the solid State, An Introduction[END_REF].

In IV. CONCLUSIONS.

In this work, we have studied the electronic and magnetic properties of Co 4 N compound with respect to pure cobalt in three different structures: HCP, FCC and BCC. For the latter, the obtained results were found in good agreement with experimental and theoretical ones. Such a reinvestigation, especially for FCC-cobalt was very useful to understand the magnetovolume effects in Co 4 N. We showed that the magnetic moment variation in the

4 N

 4 can be seen as FCC-Co with N atom at the body center, we have included the variation of the moment in FCC-Co in order to allow a better check of this effect. One can distinguish two different parts in figure3. At low volume (below FCC-Co equilibrium), the Co I moment rises rapidly to high value reaching 1.909μ B at the FCC-Co theoretical equilibrium volume (just below the Co 4 N one); while Co II moment increases somewhat slowly and a value of 1.486μ B is reached at equilibrium. Beyond the Co 4 N equilibrium volume, the Co II moment still increases while Co I one seems to stabilize at high volume. This variation can be assimilated to the moment variation of FCC-Co. At low volume the latter resembles Co I and increases rapidly to a high value with increasing volume. However, beyond its theoretical equilibrium the FCC-Co moment varies like Co II . As a consequence it can be concluded that the face centers Co atoms (Co II ) show itinerant magnetism while the corners ones (Co I ) exhibit a localized behavior. The observed behavior can be explained in terms of Co-N bond p-d hybridization in the two different cobalt sites Co I and Co II . While Co I is far from the cube center, it seems almost not affected by the nitrogen atom and shows a great sensibility to the onset of volume variation by acquiring a large moment value and it begins to stabilize only at high volume. On the contrary, Co II

  Co 4 N nitride, the energy shift between spin ↑ and ↓ populations, due to the exchange splitting is larger for Co I than for Co II . From Hankel spherical wave function energies E Hankel which, in the ASW formalism, are relative to the middle of the band, we compute the following exchange splitting magnitudes: ΔE Hankel (Co I )=2.74 eV and ΔE Hankel (Co II )=1.42 eV while an intermediate value of ΔE Hankel (Co)= 1.66 eV is obtained for FCC Co. The magnitudes of spin splitting are proportional to the magnetic moments. They can be interpreted by the more localized PDOS of Co I as with respect to Co II atoms which undergo the chemical pressure from nitrogen with a subsequent lower magnetic moment. Due to the electronegative character of nitrogen its PDOS are found at lowest energy within the VB, between -10 and -6 eV. One common feature between tetracobalt nitride and FCC-Co is the very low DOS at the Fermi level for majority spin which means that both Co sites in the nitride contribute to make the system behave as a strong ferromagnet just like FCC-Co.Particularly one can notice the low intensity peak at ∼0.5 eV below the Fermi level in the spin ↑ panel which arises from the Co II -N π* bonding. This is a major difference with Fe 4 N[41,42] where the corresponding peak due to Fe II -N π* lies exactly at the Fermi level and contributes to assign a weak ferromagnetic behavior for the iron based nitride.For further explanations of the quantum mixing between the valence states, the two atom chemical interactions are examined within the covalent bond energy ECOV plotted for the spin polarized ferromagnetic state in figure6. Negative and positive ECOV magnitudes designate bonding and antibonding interactions respectively. Looking firstly at the bonding within the Co metal sublattices, due to the large filling of Co d states the Co I -Co II interaction is found half bonding/half antibonding. The exchange splitting causes this interaction to stabilize for majority (↑) spin at lower energy so that it is found within the VB (panel 5-a) while its destabilization to higher energy for minority ↓ spin (panel 5-b) places the antibonding states on the Fermi level. This means that ↓ Co I -Co II interaction is more bonding than ↑ one. The bonding with nitrogen is clearly dominant for face center cobalt and is found mainly in the lower part of the VB with σ like bonding sharp peaks at ∼-9 eV and more extended π-like bonding in the [-9, -6 eV] range. They are followed by antibonding counterparts π* around E F as suggested in the DOS discussion and σ* above E F within the conduction band at ∼ 4 eV. From the relative energy position between the two panels of fig.6, Co I -N and Co II -N are little affected by the exchange splitting and they are both dominantly bonding within the VB so that nitrogen plays a role in stabilizing Co 4 N nitride.

  latter could be assimilated to FCC-Co. The low volume (low moment) and large volume (high moment) states of FCC-cobalt are found to be present, at the same time, in the two cobalt sites Co II and Co I of Co 4 N. The Co I moment appears very sensitive to the onset of volume variation, like cobalt at low volume, and reaches saturation rapidly, whereas the Co II one begins to increase significantly only beyond equilibrium and without fully saturating. This behavior (low volume-low moment and large volume-high moment) is explained, via the density of states and chemical bonding analyses, in terms of Co-N relative distances and the corresponding d-p hybridization. The Co I atom at a √ 3/2 from N atom is not affected and is found rather localized while the Co II one which is at only a/2 from N is submitted to a chemical pressure due to nitrogen and has itinerant behavior. Although similarities with Fe 4 N can be traced out, the overall DOS features point to a strong ferromagnetic nitride for both Co sites.

FIG. 1 :FIG. 3 :

 13 FIG. 1: Energy versus volume curves for non spin polarized (NSP ) and spin polarized (SP) cobalt in three allotropic varieties a) HCP, b) FCC, c) BCC and d) comparison of the three structures of Co in ferromagnetic ground state.

FIG. 5 :FIG. 6 :

 56 FIG. 5: DOS of spin polarized (SP) cobalt in three allotropic varieties (a) HCP, (b) FCC, (c) BCC .

  Co =2.193 bohr[16]), one can conclude that Fe 4 N and Co 4 N must have nearly the same magnitude of lattice constant. As commented in the previous section and demonstrated by geometry optimization for N deficient system, this may be due to the presence of N vacancies in the elaborated samples. The theoretical lattice parameter of the system in the magnetically ordered state, which is very close to the Fe 4 N one[22], agrees well with the experimental study of Co-substituted Fe 4 N[16]. However it is larger than the value reported for Co 4 N[7].The values of total energy at equilibrium show that the ferromagnetic state is preferred over the non magnetic one with ΔE(SP-NSP)= -1.4 eV per fu. This value is somehow close to the energy stabilization of SP ground state from US-PP calculations because the latter method accounts for valence electrons only. A magnetic volume expansion is visible whereby the theoretical lattice constant increases from 7.010 bohr in the non magnetic state at equilibrium to 7.098 bohr in the ferromagnetic state so that one expects the system to be more compressible in the spin polarized configuration. In the latter, we have obtained magnetic moment values of 1.967μ B , 1.486μ B and 0.069μ B for Co I , Co II and N respectively.With respect to the average value of 1.6 μ B of Co, the enhancement of the magnetic moment of corner Co I underlines its isolated character on one hand and the reduction of Co II moment points to the chemical role of neighboring nitrogen on the other hand. Experimentally no reports about Co 4 N magnetic moments are available. Compared to the data on CoFe 3 N,

	Furthermore, considering the iron and cobalt atomic radii (Co is slightly smaller than Fe:
	r F e =2.212 bohr and r

Co 4 N. The chemical effects of nitrogen are studied by means of partial density of states (PDOS) and chemical bonding properties (covalence energy ECOV). Within FCC cobalt the result of nitrogen insertion is to redistribute the FCC lattice into two different sublattices: Co I (cube corners) and Co II (face centers). The same atomic arrangement is found within Fe 4 N but intriguingly the lattice parameter of the pure Co 4 N found experimentally (a= 6.7788 bohr)

[7]

is much smaller than the Fe 4 N one (a= 7.1777 bohr)

[22]

. Moreover, Matar et al

[16]

have carried out an experimental study, reinforced by theoretical calculations, on cobalt-substituted Fe 4 N and have shown that Co can substitute Fe in both corners (CoFe 3 N) and face centers sites (FeCoFe 2 N) with no change in Fe 4 N lattice constant value.

V. ACKNOWLEDGEMENTS

Computations were partly carried out on main frame computers of the M3PEC-Mésocentre -University Bordeaux 1 Science and Technology (http://wwww.m3pec.u-bordeaux1.fr), financed by the "Conseil Régional d'Aquitaine" and the French Ministry of Research and Tecnology.