Pierre Hyvernat
email: pierre.hyvernat@univ-savoie.fr

Interaction Systems and Linear Logic ¿A Different Games Semantics?

Keywords: Denotational Semantics, Linear Logic, Differential λ-calculus, Interaction Systems, Simulations, Games Semantics, Containers

We define a model for linear logic based on two well-known ingredients: games and simulations. This model is interesting in the following respect: while it is obvious that the objects interpreting formulas are games and that everything is developed with the intuition of interaction in mind, the notion of morphism is very different from traditional morphisms in games semantics. In particular, we make no use of the notion of strategy! The resulting structure is very different from what is usually found in categories of games.

. Once this is done, we go a little further by constructing a reflexive object in this category, thus getting a concrete non-trivial model for the untyped differential λ-calculus.

We then show, using a highly non-constructive principle, that this category is in fact a model for full classical linear logic ; and we finally have a brief look at the related notions of predicate transformers ([2]) and containers ([3]).

Introduction

Transition systems and simulation relations are well known tools in computer science. More recent is the use of games to give models for different programming languages [START_REF] Abramsky | Full abstraction for PCF[END_REF][START_REF] Hyland | On full abstraction for PCF: I, II and III[END_REF], or as an interesting tool for the study of other programming notions [START_REF] Abramsky | Applying game semantics to compositional software modelling and verification[END_REF]. We devise a denotational model of linear logic based on those two ideas. Basically, a formula will be interpreted by an "alternating transition system" (called an interaction system) and a proof will be interpreted by a safety property for this interaction system. Those concepts which were primarily developed to model imperative programming and interfaces turned out to give a rather interesting games model: a formula is interpreted by a game (the interaction systems), and a proof by a witness that a non-loosing strategy exists (the safety property). The notion of morphism corresponds to the notion of simulation relation, a particular case of safety properties.

Part of the interest is that the notion of safety property is very simple. They are only subsets of states in which the first player can remain, whatever the second player does. In other words, from any state in the safety property, the first player has an infinite strategy which never leaves the safety property. This is to be contrasted with traditional notions where morphisms are functions (usually depending on some subset of the history) giving the strategy.

The structure of safety properties is much richer than the structure of proofs. In particular, safety properties are closed under arbitrary unions. Since there is no notion of "sum" of proofs, this doesn't reflect a logical property. However, this is a feature rather than a bug: the differential λ-calculus of Ehrhard and Regnier ( [START_REF] Ehrhard | The differential lambda calculus[END_REF]) is an extension of λ-calculus with a notion of differentiation and non-deterministic sum. As we will show, interaction systems can interpret this extra structure quite naturally.

Even better, this category enjoys such properties that we can, without much difficulty, construct a reflexive object allowing an interpretation of untyped differential λ-calculus. This reflexive object is constructed using a fixpoint construction which is already available in the category Rel of sets and relations between them.

The last thing we look at in this category is the object "⊥". As far as interaction is concerned, this is one of the most boring objects. However, it satisfies a very strong algebraic property: it is dualizing and we can thus interpret the whole of classical linear logic. This was rather unexpected and has a few surprising consequences (see corollary 34). The main reason for this is that the principle used to prove this fact (the contraposition of the axiom of choice) is relatively counter-intuitive. It is also the only part of this work where highly non-constructive principles are used, which explains why we separate this from the rest.

We conclude this paper by relating interaction systems with other notions, namely the notion of predicate transformers ( [START_REF] Hyvernat | Predicate transformers and linear logic: yet another denotational model[END_REF]) and the notion of containers ( [START_REF] Abott | Containers -constructing strictly positive types[END_REF]) and "dependent containers".

Interaction Systems

The definition of interaction system we are using was developed primarily by Peter Hancock and Anton Setzer. Their aim was to describe programming interfaces in dependent type theory ( [START_REF] Hancock | Interactive programs in dependent type theory[END_REF][START_REF] Hancock | Workshop on subtyping and dependent types in programming[END_REF]). The ability to use dependent types makes it possible to add logical specifications to usual specification. The result is a notion of formal interface describing:

• the way the programmer is allowed to use commands;

• and the logical properties he can expect from those commands.

In practice, it is usually the case that the logical specification is ensured a posteriori : a command might be legally used in a situation, even though the logical specification prevents it Because of their definition however, interaction systems can be interpreted in many different ways. In order to develop some intuitions, we prefer using a "games" interpretation: an interaction system describes the modalities of a two persons game.

The Category of Interaction Systems

Let's start with the raw definition: Definition 1 Let S be a set (of states); an interaction system on S is given by the following data:

• for each s ∈ S, a set A(s) of possible actions;

• for each a ∈ A(s), a set D(s, a) of possible reactions to a; • for each d ∈ D(s, a), a new state n(s, a, d) ∈ S. We usually write s[a/d] instead of n(s, a, d).

We use the letter w for an arbitrary interaction system, and implicitly name its components A, D and n. To resolve ambiguity, we sometimes use the notation w.A, w.D and w.n to denote the components of interaction system w. The set of states is usually implicit, and we write it w.S.

Following standard practice within computer science, we distinguish the two "characters" by calling them the Angel (choosing actions, hence the A) and the Demon (choosing reactions, hence the D). Depending on the authors' background, other names could be Player and Opponent, Eloise and Abelard, Alice and Bob, Master and Slave, Client and Server, System and Environment, alpha and beta, Arthur and Bertha, Left and Right etc.

As stated above, one of the original goals for interaction systems was to represent programming interfaces. Here is for example the interface of a stack of booleans:

• S = List(B); •      A([]) = {Push(b) | b ∈ B} A( ) = {Push(b) | b ∈ B} ∪ {Pop} • D( , ) = {Akn} •      n(s, Push(b)) = b :: s n(b :: s, Pop) = s
The set of states S represents the "virtual" internal states of an implementation of stacks: lists (stacks) of booleans.

In a non-empty state, we can issue a "pop" or a "push(b)" command, but if the state is empty, we can only issue a push command.

The responses are (in this case) trivial: we can only get an "Aknowledgment".

The next state is defined by either adding a boolean in front of the list (push) or removing the first element of the list (pop).

What is still missing from this description is the "side-effects" part: it doesn't say anywhere that a "pop" command will return the first element of the state. 1This is however much more precise than traditional interfaces which are usually given by a collection of types. Compare with this poor description of stacks:

• Pop : B • Push : B → ()
For any given stack, there are two commands: "Pop" and "push": the first one returns a boolean and the second one takes a single boolean argument and "does something".

Since we are aiming at a games semantics, we will rather use the following interpretation:

• S is a set of states describing the possible states of a game;

• for a state s ∈ S, the set A(s) is the set of legal moves in state s;

• for such a move a ∈ A(s), the set D(s, a) is the set of countermoves to a; • finally, s[a/d] is just the new state of the game after a/d has been played.

Departing from the well established tradition of "morphisms as strategies", we use the following notion of "simulation relation":

Definition 2 If w 1 and w 2 are two interaction systems on S 1 and S 2 respectively; a relation r ⊆ S 1 × S 2 is called a simulation if:

(s 1 , s 2 ) ∈ r ⇒ (∀a 1 ∈ A 1 (s 1 )) (∃a 2 ∈ A 2 (s 2 )) (∀d 2 ∈ D 2 (s 2 , a 2 )) (∃d 1 ∈ D 1 (s 1 , a 1 )) (s 1 [a 1 /d 1 ], s 2 [a 2 /d 2 ]) ∈ r .
This definition is very similar to the usual definition of simulation relations between labeled transition systems, but adds one layer of quantifiers to deal with reactions. That (s 1 , s 2 ) ∈ r means that "s 2 simulates s 1 ". By extension, if a 2 is a witness to the first existential quantifier, we say that "a 2 simulates a 1 ". Note that because the left hand side would be vacuous, the empty relation is always a simulation.

It is illuminating to look at the usual "copycat strategy" with this in mind: a simulation is just a generalization of what happens there. Intuitively, a simulation from w to w ′ means that if the Angel knows how to play in w, she can simulate, move after move, a play in w ′ . (And vice and versa for the Demon.)

To continue on the previous example, programming a stack interface amounts to implementing the stack commands using a lower level interface (arrays and pointer for examples). If we interpret the quantifiers constructively, this amounts to providing a (constructive) proof that a non-empty relation is a simulation from this lower level interaction system to stacks: for each of the stacks commands, we need to provide a witness command in the low level world in such a way as to guarantee simulation. (See [START_REF] Hancock | Programming interfaces and basic topology[END_REF] and [START_REF] Hyvernat | A logical investigation of interaction systems[END_REF] for a more detailed description of programming in terms of interaction systems.)

Recall that the composition of two relations is given by:

(s 1 , s 3 ) ∈ r 2 • r 1 ⇔ (∃s 2 ) (s 1 , s 2 ) ∈ r 1 and (s 2 , s 3 ) ∈ r 2
It should be obvious that the composition of two simulations is a simulation and that the equality relation is a simulation from any w to itself. Thus, we can put: Definition 3 We call Int the category of interaction systems with simula-tions.

Note that this category is locally small but that, for any given set of states S, the collection of interaction systems on S forms a proper class. It is possible to restrict to "finitary" interaction systems: those for which the sets of actions and the sets of reactions are always finite. For our purposes, it is impossible to restrict to finite sets of states (see the definition of !w) or to countable actions/reactions sets (see the definition of w 1 ⊸ w 2 ). Subtler considerations show that it is however possible to restrict to sets of states of cardinalities ℵ 0 and sets of actions of cardinalities 2 ℵ 0 and sets of reactions of cardinalities ℵ 0 . (See the proof of proposition 38 for a hint.)

We have the following "forgetful" functor from Int to Rel, the category of sets and relations between them: In terms of games, magic means "the Demon resigns" (he cannot answer any move) while abort means "the Angel resigns" (she cannot play).

This category enjoys a very strong algebraic property:

Proposition 5 The category Int is enriched over complete sup-lattices.

Note that enrichment over sup-lattice is stronger than enrichment over commutative monoids.

PROOF. Proving that an arbitrary unions of simulations in Int(w 1 , w 2 ) is still a simulation in Int(w 1 , w 2 ) is trivial; as well as showing that the empty relation is always a simulation.

It thus only remains to show that composition commutes with unions, on the right and on the left. Since this is true in Rel, it is also true in Int! 2

Notation

Let's recall some traditional notation.

• An element of the indexed cartesian product a∈A D(a) is given by a function f taking any a ∈ A to an f (a) in D(a). When the set D(a) doesn't depend on a, it amounts to a function f : A → D. • An element of the indexed disjoint sum a∈A D(a) is given by a pair (a, d)

where a ∈ A and d ∈ D(a). When the set D(a) doesn't depend on a, this is simply the cartesian product A × D. • We write List(S) for the set of "lists" over set S. A list is a tuple (s 1 , s 2 , . . . s n ) of elements of S. The empty list is written ().

• The collection M f (S) of finite multisets over S is the quotient of List(S) by permutations. We write [s 1 , . . . s n ] for the equivalence class containing (s 1 , . . . s n ). We use "+" for the sum of multisets; it simply corresponds to concatenation on lists.

Constructions

We now define, at the level of interaction systems, the connectives of linear logic. With those, making Int into a denotational model of intuitionistic linear logic more or less amounts to showing that it is symmetric monoidal closed, has finite products and coproducts and has a well behaved comonad.

Constants.

A very simple, yet important interaction system is "I", the interaction system without interaction.

Definition 6 Define I to be the interaction system on the singleton set { * }:

A I ( * ) = { * } D I ( * , * ) = { * } n I ( * , * , * ) = { * } .
This interaction systems is also called " skip". This is the perfect example of "stable" or "constant" game: no knowledge is ever gained by any of the players. Since the interaction traces are ultimately constant, this is sometimes considered a terminating system: both sides have reached an agreement.

One last interaction system of (theoretical) interest is given by the interaction system on the empty set of states:

Definition 7 Define 0 to be the unique interaction system on ∅.

This interaction system is even more boring than I: there are no states! From a practical point of view, this system doesn't even exist. The following is trivial:

Lemma 8
In Int, the object 0 is a zero object: it is both initial and terminal.

Product and Coproduct

Since the forgetful functor w → |w| has a right adjoint, we know it commutes with colimits. As a result, we know that if the coproduct of w 1 and w 2 exists in Int, its set of states is isomorphic to the coproduct of S 1 and S 2 in Rel.

We thus define:

Definition 9 Suppose w 1 and w 2 are interaction systems on S 1 and S 2 . Define the interaction system w 1 ⊕ w 2 on S 1 + S 2 as follows:2

A w 1 ⊕w 2 ((i, s i )) = A i (s i ) D w 1 ⊕w 2 ((i, s i ), a) = D i (s i , a) n w 1 ⊕w 2 ((i, s i ), a, d) = (i, s i [a/d])
In other words, the game w 1 ⊕ w 2 is simply a disjoint sum of w 1 and w 2 , and interaction takes place in only one of the games. Because we have no initial state, there is no need to specify who, among the Angel or the Demon, is making the choice of the game to use. With this in mind, lemma 11 isn't very surprising.

We have:

Lemma 10 The operation ⊕ is the coproduct in Int.

PROOF. We just "lift" the constructions from the category Rel:

• injections: we put

i 1 : Int(w 1 , w 1 ⊕ w 2 ) = {(s 1 , (1, s 1 )) | s 1 ∈ S 1 }
and similarly for i 2 ∈ Int(w 2 , w 1 ⊕ w 2 ). • copairing: suppose r 1 ∈ Int(w 1 , w) and r 2 ∈ Int(w 2 , w), define:

[r 1 , r 2 ] :

Int(w 1 ⊕ w 2 , w) = {((1, s 1 ), s)) | (s 1 , s) ∈ r 1 } ∪ {((2, s 2 ), s)) | (s 2 , s) ∈ r 2 }
Checking that those constructions yield simulations is direct.

Commutativity of the appropriate diagrams as well as universality can be lifted from Rel...

2

The next result is only surprising at first sight: the situation is similar in Rel.

It will however to be quite important in the sequel since we cannot interpret the differential λ-calculus without it.

Lemma 11

In Int, ⊕ is also the product.

PROOF. This is a direct consequence of commutative monoid enrichment (proposition 5). 32

When dealing with linear logic, we use the usual symbol & when it denotes a conjunction...

Synchronous Product.

There is an obvious tensor construction reminiscent of the synchronous product found in SCCS (synchronous calculus of communicating systems, [START_REF] Milner | Calculi for synchrony and asynchrony[END_REF]):

Definition 12 Suppose w 1 and w 2 are interaction systems on S 1 and S 2 . Define the interaction system w 1 ⊗ w 2 on S 1 × S 2 as follows:

A w 1 ⊗w 2 ((s 1 , s 2 )) = A 1 (s 1 ) × A 2 (s 2 ) D w 1 ⊗w 2 ((s 1 , s 2 ), (a 1 , a 2 )) = D 1 (s 1 , a 1 ) × D 2 (s 2 , a 2 )
n w 1 ⊗w 2 ((s 1 , s 2 ), (a 1 , a 2 ), (d 1 , d 2 )) = (s 1 [a 1 /d 1 ], s 2 [a 2 /d 2 ]) .
This is a kind of lock-step synchronous parallel composition of w 1 and w 2 : the Angel and the Demon exchange pairs of actions/reactions. In terms of games, the players simply play two games in parallel at the same pace.

For any sensible notion of morphism, I should be a neutral element for this product. It is indeed the case, for the following reason: the components of w⊗I and w are isomorphic by dropping the second (trivial) coordinate:

w ⊗ I w S × { * } ≃ S A((s, * )) = A(s) × { * } ≃ A(s) D((s, * ), (a, * )) = D(s, a) × { * } ≃ D(s, a) n((s, * ), (a, * ), (d, * )) = (s[a/d], * ) ≃ s[a/d]
This implies trivially that {((s, * ), s) | s ∈ S} is an isomorphism. For similar reasons, this product is transitive and commutative.

Lemma 13 ⊗ is a commutative tensor product in the category Int. Its action on morphisms is given by:

((s 1 , s ′ 1 ), (s 2 , s ′ 2 )) ∈ r ⊗ r ′ ⇔      (s 1 , s 2 ) ∈ r and (s ′ 1 , s ′ 2 ) ∈ r ′
Checking that r ⊗ r ′ is a simulation is easy.

The notion of "componentwise" isomorphism is too fine for most purposes and the notion of isomorphism inherited from simulations is coarser. In particular, it is easy to find examples of isomorphic interaction systems in Int where the actions/reactions sets are not isomorphic. For example, if w is an interaction system, let ε s be a choice function from P * (A(s)), the collection of non-empty subsets of A(s) to A(s); and define w with

• A(s) = P * (A(s)); • D(s, U) = D(s, ε s (U)); • n(s, U, d) = n(s, ε s (U), d).
The systems w and w are isomorphic, but the sets A(s) and A(s) have different cardinalities.

Linear Arrow.

Any category with a zero object cannot be cartesian closed. We thus cannot hope to model the simply typed λ-calculus inside Int. One of the points of linear logic is precisely to give logical status to a simpler kind of structure: linear implication. We do not require our denotational model to be cartesian closed but only symmetric monoidal closed w.r.t. to a tensor which is generally not the cartesian product. This is the case for Int, but the definition of the functor ⊸ is a little more involved:

Definition 14 If w 1 and w 2 are interaction systems on S 1 and S 2 , define the interaction system w 1 ⊸ w 2 on S 1 × S 2 as follows:

A ⊸ ((s 1 , s 2 )) = f ∈A 1 (s 1 )→A 2 (S 2 ) a 1 ∈A 1 (s 1 ) D 2 (s 2 , f (a 1 )) → D 1 (s 1 , a 1 ) D ⊸ ((s 1 , s 2 ), (f, G)) = a 1 ∈A 1 (s 1 ) D 2 (s 2 , f (a 1 )) n ⊸ ((s 1 , s 2 ), (f, G), (a 1 , d 2 )) = (s 1 [a 1 /G a 1 (d 2 )] , s 2 [f (a 1 )/d 2 ]) .
It may seem difficult to get some intuition about this interaction system; but it is a posteriori quite natural. Let's unfold this definition with simulations in mind:

• An action in state (s 1 , s 2 ) is given by a pair consisting of:

(1) a function f (the index for the element of the disjoint sum) translating actions from s 1 into actions from s 2 ;

(2) for any action a 1 , a function G a 1 translating reactions to f (a 1 ) into reactions to a 1 . • A reaction to such a "one step translating mechanism" is given by:

(2) an action a 1 in A 1 (s 1 ) (which we want to simulate);

(1) and a reaction d 2 in D 2 (s 2 , f (a 1 )) (which we want to translate back).

• Given such a reaction, we can simulate a 1 by a 2 = f (a 1 ) ∈ A 2 (s 2 ); and translate back

d 2 into d 1 = G a 1 (d 2 ) ∈ D 1 (s 1 , a 1 ). The next state is just the pair of states s 1 [a 1 /d 1 ] and s 2 [a 2 /d 2 ].
In essence, the Angel translates what the Demon gives her.

This connective is indeed a "linear arrow":

Proposition 15
In Int, ⊗ is left adjoint to ⊸ : there is an isomorphism

Int(w 1 ⊗ w 2 , w 3 ) ≃ Int(w 1 , w 2 ⊸ w 3 ) , natural in w 1 , w 2 and w 3
PROOF. The proof is not really difficult. First notice that the axiom of choice can be written as

AC : (∀a ∈ A)(∃d ∈ D(a)) ϕ(a, d) ⇔ (∃f ∈ a∈A D(a))(∀a ∈ A) ϕ(a, f (a)) .
When the domain D(a) for the existential quantifier doesn't depend on a ∈ A, we can simplify it into:

AC : (∀a ∈ A)(∃d ∈ D) ϕ(a, d) ⇔ (∃f ∈ A → D)(∀a ∈ A) ϕ(a, f (a)) .
We will use AC to shuffle quantifiers and complexify the domains of quantification. This will transform the condition defining a simulation from w 1 ⊗ w 2 to w 3 into the condition defining a simulation from w 1 to w 2 ⊸ w 3 .

In the sequel, the part of the formula being manipulated will be written in bold. That r is a simulation from w 1 ⊗ w 2 to w 3 takes the form 4

(s 1 , s 2 , s 3 ) ∈ r ⇒ (∀a 1 ∈ A 1 (s 1 ))(∀a 2 ∈ A 2 (s 2 )) (∃a 3 ∈ A 3 (s 3 )) (∀d 3 ∈ D 3 (s 3 , a 3 )) (∃d 1 ∈ D 1 (s 1 , a 1 ))(∃d 2 ∈ D 2 (s 2 , a 2 )) (s 1 [a 1 /d 1 ], s 2 [a 2 /d 2 ], s 3 [a 3 /d 3 ]) ∈ r .
Using AC on ∀a 2 ∃a 3 , we obtain:

(s 1 , s 2 , s 3 ) ∈ r ⇒ (∀a 1 ∈ A 1 (s 1 )) (∃f ∈ A 2 (s 2 ) → A 3 (s 3 )) (∀a 2 ∈ A 2 (s 2 ))(∀d 3 ∈ D 3 (s 3 , f (a 2 ))) (∃d 1 ∈ D 1 (s 1 , a 1 ))(∃d 2 ∈ D 2 (s 2 , a 2 )) (s 1 [a 1 /d 1 ], s 2 [a 2 /d 2 ], s 3 [f (a 2 )/d 3 ]) ∈ r .
We can now apply AC on ∀d 3 ∃d 2 :

(s 1 , s 2 , s 3 ) ∈ r ⇒ (∀a 1 ∈ A 1 (s 1 )) (∃f ∈ A 2 (s 2 ) → A 3 (s 3 )) (∀a 2 ∈ A 2 (s 2 )) (∃g ∈ D 3 (s 3 , f (a 2 )) → D 2 (s 2 , a 2 )) (∀d 3 ∈ D 3 (s 3 , f (a 2 ))) (∃d 1 ∈ D 1 (s 1 , d 1 )) (s 1 [a 1 /d 1 ], s 2 [a 2 /g(d 3 )], s 3 [f (a 2 )/d 3 ]) ∈ r 4 modulo associativity (S 1 × S 2 ) × S 3 ≃ S 1 × (S 2 × S 3 ) ≃ S 1 × S 2 × S 3 .
and apply AC one more time on ∀a 2 ∃g to obtain:

(s 1 , s 2 , s 3 ) ∈ r ⇒ (∀a 1 ∈ A 1 (s 1 )) (∃f ∈ A 2 (s 2 ) → A 3 (s 3 )) (∃G ∈ a 2 ∈A 2 (s 2 ) D 3 (s 3 , f (a 2 )) → D 2 (s 2 , a 2 )) (∀a 2 ∈ A 2 (s 2 ))(∀d 3 ∈ D 3 (s 3 , f (a 2 ))) (∃d 1 ∈ D 1 (s 1 , d 1 )) (s 1 [a 1 /d 1 ], s 2 [a 2 /G a 2 (d 3 )], s 3 [f (a 2 )/d 3 ]) ∈ r which is equivalent to (s 1 , s 2 , s 3 ) ∈ r ⇒ (∀a 1 ∈ A 1 (s 1 ))   ∃(f, G) ∈ f ∈A 2 (s 2 )→A 3 (s 3 ) a 2 ∈A 2 (s 2 ) D 3 (s 3 , f (a 2 )) → D 2 (s 2 , a 2 )    (∀(a 2 , d 3 ) ∈ A 2 (s 2 ) D 3 (s 3 , f (a 2 ))) (∃d 1 ∈ D 1 (s 1 , d 1 )) (s 1 [a 1 /d 1 ], s 2 [a 2 /G a 2 (d 3 )], s 3 [f (a 2 )/d 3 ]) ∈ r .
By definition, this means that r is a simulation from w 1 to w 2 ⊸ w 3 .

Naturality is trivial: it corresponds to naturality of associativity in Rel. 2

In particular, proposition 15 implies that

Int(w 1 , w 2 ) ≃ Int(I, w 1 ⊸ w 2 ) .
We call a simulation from I to w a safety property for w.

Lemma 16 (with Def.) A subset x ⊆ S is a simulation from

I to w iff 5 s ∈ x ⇒ (∃a ∈ A(s))(∀d ∈ D(s, a)) s[a/d] ∈ x .
We write S(w) for the collection of such subsets, and we call such an x a safety property for w.

Finally, we have

Int(w 1 , w 2 ) = S(w 1 ⊸ w 2 ) .
The analogy with traditional notions of morphisms as strategies is rather subtle. A safety property x satisfies the property if interaction is started from a state in x, then the Angel has a move that guarantees that the next state will also be in x (provided the Demon does answer).

This is a safety property in the sense that it guarantees that "nothing bad happens". (As opposed to liveness properties, which ensure that "something good happens"...) In particular, this means that the Angel has an infinite strategy from any state in x: she can always find a move to play. The choice of those moves is irrelevant to the notion of safety property: we only know they exist. In particular, such a move needs not be unique.

As special case, let's look at the definition of linear negation. The orthogonal w ⊥ of w is defined as usual as the interaction system w ⊸ ⊥. For intuitionistic linear logic, any object can formally be used as ⊥, but anticipating on proposition 33, we use ⊥ = I. We have:

A ⊥ ((s, * )) = f ∈A(s)→{ * } a∈A(s) { * } → D(s, a) D ⊥ ((s, * ), (f, G)) = a∈A(s) { * } n ⊥ ((s, * ), (f, G), (a, * )) = (s[a/G a 1 ( * )], * )
which, after simplification, is equivalent to

A ⊥ (s) = a∈A(s) D(s, a) D ⊥ (s, f ) = A(s) n ⊥ (s, f, a) = s[a/f (a)] .
One important point to notice is that with this definition, the set of states of w ⊥ is the same as the set of states of w. In particular, the canonical morphism in Int(w, w ⊥⊥ ) will be given by the equality relation.

The definition looks complex but can be interpreted in a very traditional way: negation interchanges the two players. In our context, it is not possible to simply interchange actions and reactions since reactions depend on a particular action. We have to do the following:

• an action in A ⊥ (s) is a conditional reaction; or a one move strategy to react to any action; • a reaction in D ⊥ (s, f ) is just an action in w;

• the new state after "action" f and "reaction" a is just the state obtained after playing a followed by f (a).

The "polarities" of moves and coutermoves is interchanged, and it does swap the players in the sense that it transforms Angel strategies into Demon strategies and vice and versa. (See [START_REF] Hyvernat | A logical investigation of interaction systems[END_REF] for more details.)

The dual w ⊥ enjoys a surprising property: the set of possible reactions to a particular action doesn't depend on the particular action! 1.3.5 Multithreading.

We now come to the last connective needed to interpret intuitionistic linear logic. Its computational interpretation is related to the notion of multithreading, i.e. the possibility to run several instances of a program in parallel. In our case, it corresponds to the ability to play several synchronous instances of the same game in parallel. Let's start by defining synchronous multithreading in the most obvious way:

Definition 17 If w is an interaction system on S, define L(w), the multithreaded version of w to be the interaction system on List(S) with:

L.A((s 1 , . . . , s n )) = A(s 1 ) × . . . × A(s n ) L.D((s 1 , . . . , s n ), (a 1 , . . . , a n )) = D(s 1 , a 1 ) × . . . × D(s n , d n ) L.n((s 1 , . . . , s n ), (a 1 , . . . , a n ), (d 1 , . . . , d n )) = (s 1 [a 1 /d 1 ], . . . , s n [a n /d n ]) .
This interaction system is just the sum of all "n-ary" versions of the synchronous product.

Lemma 18

The operator w → L(w) can be extended to a functor from Int to Int.

To get the abstract properties we want, we need to quotient multithreading by permutations. Just like multisets are lists modulo permutations, so is !w the multithreaded L(w) modulo permutations. This definition is possible be-cause L(w) is "compatible" with permutations: if σ is a permutation, we have

σ • ((s 1 , . . . s n )[(a 1 , . . . a n )/(d 1 , . . . d n )]) = (σ • (s 1 , . . . s n ))[σ • (a 1 , . . . a n )/σ • (d 1 , . . . d n )] .
The final definition is:

Definition 19 If w is an interaction system on S, define !w to be the following interaction system on M f (S):

!A(µ) = s∈µ L.A(s) !D(µ, (s, a)) = L.D(s, a) !n(µ, (s, a), d) = [ L.n(s, a, d)] .
(Note that as an element of µ, s is just a specific order for the element of µ.)

Unfolded, it gives:

• an action in state µ is given by an element s (a list) of µ (a multiset, i.e. an equivalence class) together with an element a in L.A(s) (a list of actions); Lemma 20 This operation w → !w can be extended to a functor from Int to Int. Moreover, we have the following bisimulation (which is not an isomorphism)

•
L(w) σ → ← p !w ( 1
)
where σ is just membership of a list in a multiset (equivalence class of lists) and p its converse.

This operation enjoys a very strong algebraic property:

Proposition 21 !w is the free ⊗-comonoid generated by w.

Note that because !w "is" n≥0 w ⊗n /S n , this is not very surprising.

PROOF. Quite a lot can be deduced from the same property of Rel, but we will look at some details.

Let's start by looking at the ⊗-comonoid structure of !w: the counit and comultiplication are given by e ∈ Int(!w, I) and m ∈ Int(!w, !w ⊗ !w)

= {([], * )} = {(µ + ν, (µ, ν)) | µ, ν ∈ M f (S)}
We need to show that for any interaction system w and ⊗-comonoid w c , there is a natural isomorphism

CoMon(Int, ⊗)(w c , !w) ≃ Int(w c , w) .
Going from left to right is easy:

CoMon(Int, ⊗)(w c , !w) → Int(w c , w) r → {(s c , s) | (s c , [s]) ∈ r} .
Checking that this operation is well-defined (it sends a comonoid morphism to a simulation) is direct.

The other direction is more interesting. Let w c be a commutative comonoid. This means we are given e c ∈ Int(w c , I) and m c ∈ Int(w c , w c ⊗ w c ), satisfying additional commutativity and associativity conditions.

Suppose r is a simulation from w c to w. This is a relation with no condition about the comonoid structure of w c . We construct a relation from w c to !w in the following way:

• we start by extending comultiplication m c to m c : Int(w c , L(w c ));

• we then compose that with L(r) : Int( L(w c ), L(w));

• and finally compose that with σ : Int( L(w), !w), see (1) in lemma 20.

We then check that this simulation respects the comonoid structures of w c and !w.

Define m c ⊆ S c × List(S c ) by the following clauses: (inductive definition)

(s, ()) ∈ m c iff s ∈ e c (s, s ′ ) ∈ m c iff s = s ′ (s, (s 1 , . . . , s n )) ∈ m c iff (s, (s 1 , s ′ )) ∈ m c ∧ (s ′ , (s 2 , . . . , s n )) ∈ m c
for some s ′ ∈ S c .

Using the fact that e c and m c are simulations, we can easily show (by induction) that m c is a simulation from w c to L(w c ).

Moreover, we have:

(s c , (s c,1 , . . . , s c,n+m )) ∈ m c ⇔ (∃s 1 c , s 2 c ∈ S c ) (s c , (s 1 c , s 2 c )) ∈ m c ∧ (s 1 c , (s c,1 , . . . , s c,n )) ∈ m c ∧ (s 2 c , (s c,n+1 , . . . , s c,n+m )) ∈ m c (2)
by transitivity and We know that r = σ • L(r) • m c is a simulation from w c to !w. We need to check that this simulation respects the comonoid structures of w c and !w, i.e. that both

w c r -!w w c c -w c ⊗ w c
• (s c , (s 1 c , s 2 c )) ∈ m c • (s 1 c , (s c,1 , . . . , s c,n )) ∈ m c • (s 2 c , (s c,n+1 , . . . , s c,n+m )) ∈ m c • and (s i , s c,i ) ∈ r for all i = 1, . . . , n + m.
By using ( 2) and ( 3), it is trivial to show that the two conditions are equivalent. This proves that the second diagram is commutative.

It only remains to show that the two operations defined are inverse of each other. This is not difficult. 2

Interpreting Linear Logic

We now have all the necessary ingredients to construct a denotational model for intuitionistic linear logic. The details of categorical models for linear logic are quite intricate, and there are several notions, not all of which are equivalent. We refer to the survey [START_REF] Melliès | Categorical models of linear logic revisited[END_REF] and the references given there.

In the case of Int, the situation is however quite simple: proposition 21 makes Int into a "Lafont category" (see [START_REF] Lafont | Logiques, catégories et machines[END_REF]).

Corollary 22

With the construction defined in the previous sections, Int is a Lafont category. In particular, " ! " is a comonad; and we have for any w 1 and w 2 , we have the following natural isomorphism:

!(w 1 & w 2 ) ≃ !w 1 ⊗ !w 2 .
Recall that since the product and coproduct coincide, & is the same as ⊕.

A direct proof of the fundamental isomorphism is easy: there is a "componentwise" isomorphism between the interaction systems !(w 1 & w 2 ) and !w 1 ⊗ !w 2 .

Lafont categories were used to give a semantics to linear logic and were latter subsumed by Seely categories and linear categories.

It is thus possible to give a semantics to formulas and proofs in the usual way. We write F for the interpretation of a formula F (no confusion arises) and [[π]] for the interpretation of a proof π.

Proposition 23 For all proof π 1 and π 2 of the same sequent, if π 1 and π 2 have the same cut-free normal form, then

[[π 1 ]] = [[π 2 ]].
Moreover, since the interpretation is done using canonical morphisms, which are just lifting of the same morphisms in Rel, the interpretation of a proof is the same as its relational interpretation: 6Proposition 24 For any proof π of a sequent Γ ⊢ F , the relational interpretation [[π]] of π is a simulation from Γ to F . (This holds for any valuation of the propositional variables.)

The presence of propositional variables is crucial because without them, the model becomes trivial:

Proposition 25 Suppose F is a formula without propositional variables; then its interpretation is trivial : any subset of its set of states is a safety property.

More precisely, we have

• A F (s) = { * } (singleton set) ; • D F (s, * ) = { * } (singleton set) ; • n F (s, * , * ) = s.
The proof is a trivial induction on the formula. This model is thus only appropriate when interpreting Π 1 1 logic, i.e. propositional linear logic. There, it has a real discriminating power. The model can even be extended to deal with full second order, with the usual proviso: the interpretation may decrease (in some very special cases) during elimination of a second order cut. For more details, see [10, chap. 8]. 73 Interpreting the Differential λ-calculus So far, proposition 5 hasn't been used, except to deduce the existence of a product. The problem is that this proposition doesn't reflect a property of proofs. The reason is that

• not every formula has a proof; • we do not see a priori how to sum proofs of a single formula.

Ehrhard and Regnier's differential λ-calculus ( [START_REF] Ehrhard | The differential lambda calculus[END_REF]) extends the λ-calculus by adding a notion of differentiation of λ-terms. One consequence is that we need a notion of sum of terms, interpreted as a non-deterministic choice. It is also possible to only add sums (and coefficients) to the usual λ-calculus as in [START_REF] Vaux | λ-calculus in an algebraic setting[END_REF].

It is not the right place to go into the details of the differential λ-calculus and we refer to [START_REF] Ehrhard | The differential lambda calculus[END_REF] for motivations and a complete description. A complete definition can also be found in the Appendix on page 36.

In the typed case, we have the following typing rules:

(1) Γ ⊢ 0 : τ and Γ ⊢ t : τ Γ ⊢ u : τ Γ ⊢ t + u : τ ; (2) Γ ⊢ t : τ → σ Γ ⊢ u : τ Γ ⊢ D t • u : τ → σ .
The intuitive meaning is that "D t • u" is the result of (non-deterministically) replacing exactly one occurrence of the first variable of t by u. We thus obtain a sum of terms, depending on which occurrence was replaced. This gives a notion of differential substitution (or linear substitution) which yields a differentialreduction. The rules governing this reduction are more complex than usual β-reduction rules; we refer to [START_REF] Ehrhard | The differential lambda calculus[END_REF] or the Appendix.

Besides the natural commutativity and associativity of addition, differential λ-terms are also quotiented modulo the following equivalence relations:

• 0 = (0)u = λx.0 = D 0 • t = D t • 0; • (t 1 + t 2 ) u = (t 1 )u + (t 2 )u; • λx.(t 1 + t 2 ) = λx.t 1 + λx.t 2 ; • D(t 1 + t 2 ) • u = D t 1 • u + D t 2 • u; • D t • (u 1 + u 2 ) = D t • u 1 + D t • u 2 ; • D(D t • u) • v = D(D t • v) • u.
The last one is probably the most important one as it allows to link the notion of differentiation to the traditional, analytic notion of differentiation. Note that even if the first five rules can be oriented from left to right, a quotient is inevitable because of the sixth rule and the commutativity of addition. This quotient is natural because none of those rules carries any computational content.

Interpreting usual (without "D", "+" nor "0") λ-terms can be done using the well-known translation of the simply typed λ-calculus into intuitionistic linear logic with propositional variables. Just replace an atomic type by a propositional variable and the type τ → σ by !τ ⊸ σ inductively. That the resulting interpretation is sound follows directly from the fact that Int is a Lafont category. (In any model for linear logic, the co-Kleisli category of ! is cartesian closed.)

The general notion of categorical model for the differential λ-calculus (or differential proof nets, or "differential linear logic") is only beginning to emerge.

The main paper on the subject is [START_REF] Blute | Differential categories[END_REF], where the categorical notion of "differentiation combinator" is studied in details. No real soundness theorem is however proved there because the authors work in a more general setting: the base category is not necessarily monoidal closed, i.e. the co-Kleisli category is not necessarily cartesian closed.

The notion of differential category is well-suited for our purposes, and we will show that the category Int is indeed a differential category. Together with the fact that Int is a Lafont category, it allows to deduce that we do get a categorical model for the differential λ-calculus.

Definition 26 If C is a symmetric monoidal category with a coalgebra modality ! , we call a natural transformation d X : X ⊗ !X → !X a deriving transformation in case the following hold:

d X e X = 0 d X ∆ = (1 ⊗ ∆) (d X ⊗ 1) + (1 ⊗ ∆) (c ⊗ 1) (1 ⊗ d X ) d X ǫ X = (1 ⊗ e) u X d X δ = (1 ⊗ ∆) (d X ⊗ δ)d !X
where e X : !X → I and ∆ X : !X → !X ⊗ !X are the operations of the coalgebra !X;

c : A ⊗ B → B ⊗ A is the symmetry and u X : X ⊗ I → X is the unit; -δ X : !X → !!X and ǫ X : !X → X come from the usual comonad laws. 8In our case, we can lift d X from the relational model:

Lemma 27 (and definition) For any interaction system w on S, the relation d w defined by

d w = (s 0 , [s 1 , . . . , s n ]), [s 0 , s 1 , . . . , s n ] | s 0 , . . . , s n ∈ S is a deriving transformation.
PROOF. Because it is already shown in [START_REF] Blute | Differential categories[END_REF] that this relation is indeed a deriving transformation in Rel, is suffices to show that d w is a simulation from w ⊗ !w to !w. This is immediate.

2

We can now extend the interpretation to differential λ-terms:

• the additive structure (0 and +) is directly interpreted by the monoid structure (∅ and ∪); • the differential structure is interpreted in the only sensible way: suppose we have Γ ⊢ t : τ → σ and Γ ⊢ u : τ ; by induction, we have

[[t]] ∈ Int(!Γ, !τ ⊸σ) and [[u]] ∈ Int(!Γ, τ ).
We can define a morphism in Int(!τ ⊸σ, (τ ⊗!τ )⊸σ):

1 ∈ Int(!τ ⊸ σ , !τ ⊸ σ) ⇔ 1 ∈ Int((!τ ⊸ σ) ⊗ !τ , σ) ⇒ 1 (1 ⊗ d τ ) ∈ Int((!τ ⊸ σ) ⊗ τ ⊗ !τ , σ) ⇔ 1 (1 ⊗ d τ ) ∈ Int(!τ ⊸ σ , (τ ⊗ !τ ) ⊸ σ)
We write D for this morphism. This is an internal version of the differential combinator from [17, def. 2.3]. From this, we get

D [[t]] ∈ Int(!Γ , (τ ⊗ !τ ) ⊸ σ) ⇔ D[[t]] ∈ Int(!Γ ⊗ τ , !τ ⊸ σ) which we'll call [[D t]].
We can now compose interpretations as in:

!Γ ∆ -→ !Γ ⊗ !Γ 1⊗[[u]] -→ !Γ ⊗ τ [[D t]] -→ !τ ⊸ σ This morphism in Int(!Γ , !τ ⊸ σ) is the interpretation of D t • u.
Spelled out concretely in the case of Rel or Int, the inductive definition looks like:

(γ, µ, s ′ ) ∈ [[D t • u]] ⇔ (γ 1 , µ + [s], s ′ ) ∈ [[t]] for some (γ 2 , s) ∈ [[u]] s.t. γ = γ 1 + γ 2
That the interpretation is sound follows rather directly from the properties of a deriving transformation, see [START_REF] Blute | Differential categories[END_REF] for some of the missing details:

Lemma 28 For all differential λ-terms and valuations γ, we have

• [[0]] = [[(0)u]] = [[λx.0]] = [[D 0 • t]] = [[D t • 0]]; • [[(t 1 + t 2 ) u]] = [[(t 1 )u + (t 2 )u]]; • [[λx.(t 1 + t 2 )]] = [[λx.t 1 + λx.t 2 ]]; • [[D(t 1 + t 2 ) • u]] = [[D t 1 • u + D t 2 • u]]; • [[D t • (u 1 + u 2 )]] = [[D t • u 1 + D t • u 2 ]]; • [[D(D t • u) • v]] = [[D(D t • v) • u]].
We finally obtain the desired result:

Proposition 29 Suppose that Γ ⊢ t : σ where Γ is a context and t a differential λ-term. The relation [[t]] is a simulation relation from !Γ to σ. Moreover, for all t and u we have:

[[(λx.t)u]] = [[t[u/x]]] [[D(λx.t) • u]] = [[λx . (∂t/∂x) • u]]
PROOF. That we obtain a simulation is true by construction.

Invariance under β-reduction follows from the correctness of the interpretation of λ-calculus in a cartesian-closed category.

Invariance under linear substitution seems to follow from general considerations about deriving transformation in linear categories, even if this is not treated in [START_REF] Blute | Differential categories[END_REF]. (In our case, a direct verification is possible, but long and tedious...)

4 Untyped Calculus

Interpreting untyped λ-calculus remained an open question for quite a long time: since the cardinality of a function space is strictly bigger than the cardinality of the original set, it seemed difficult to get a model where any λ-term can be either an argument or a function. Dana Scott finally found a model by constructing a special object in the category of domains.

The solution is quite elegant: to interpret untyped λ-terms in a cartesian closed category, one "just" needs to find a reflexive object in a cartesian closed category, i.e. an object X with a retraction / projection pair [X → X] ⊳ X.

We have at our disposal a cartesian closed category: the Kleisli category over the comonad ! . Were we to find a reflexive object W in this category, we could model the untyped differential λ-calculus in the λ-model S(W ). We now show how to construct such a reflexive object, in a fairly straightforward way.

We start with a non-trivial interaction system w on a set of states S (natural numbers for example) and then define an interaction system W , satisfying the equation W ≃ w ⊕ (!W ⊸ W ) as follows:

(1) the set of states S W is defined as the least fixpoint of X → S+M f (X)×X; in a more "programming" fashion"

S W = data Leaf(s ∈ S) | Node µ ∈ M f (S W ) , u ∈ S W
(2) the possible actions in a given state are defined by induction on the state: using "pattern matching", we have

A W (Leaf(s)) = A(s) A W (Node(µ, u)) = (!A W ⊸ A W )((µ, u))
(3) reactions are defined similarly as

D W (Leaf(s), a) = D(s, a) D W (Node(µ, u), b) = (!D W ⊸ D W )((µ, u), b) (4
) and finally, the next state function is defined as

n W (Leaf(s), a, d) = Leaf(s[a/d]) n W (Node(µ, u), b, p) = (!n W ⊸ n W )((µ, u), b, p)
Due to the presence of multisets, an actual implementation of W in a dependently typed functional programming language would be a little more complex: we would need to work with lists rather than multisets, and reason modulo shuffling concretely.

Lemma 30 The relation r between S + (M f (S W ) × S W ) and S W defined by

((1, s) , Leaf(s)) ∈ r ((2, (µ, u)) , Node(µ, u)) ∈ r is an isomorphism (in Int) from w ⊕ (!W ⊸ W ) to W .
The proof is direct. (This is an instance of a strong, "componentwise" isomorphism.)

Corollary 31 In the ! -Kleisli category of Int, which is cartesian closed, there is a retract W W ⊳ W .

PROOF. First, notice that it is sufficient to find a retract in the category Int: any morphism in a category can also be seen as a morphism in a Kleisli category (in a way which is compatible with composition in the Kleisli category).

There is the canonical injection i 2 from !W ⊸ W to w ⊕ (!W ⊸W ). Now, in the category Int, we have that product and coproduct coincide; in particular, we have the projection

π 2 from w & (!W ⊸W ) = w ⊕ (!W ⊸W ) to !W ⊸ W .
Moreover, by definition, we have

π 2 • i 2 = Id !W ⊸W .
We can now prove that r • i 2 / π 2 • r ∼ is a retraction / projection from !W ⊸ W to W :9 it follows from the previous remark that π 2 • i 2 = Id and that r ∼ is the inverse of r. (Recall that r is an isomorphism.) 2

From there, constructing a model for the untyped λ-calculus is standard. We refer to [START_REF] Amadio | Domains and lambda-calculi[END_REF]. We obtain in this way a model where each term is interpreted by a safety property for W .

Since S(W ) is a complete sup-lattice, we can also model sums, and by the very same construction defined in section 3, model differentiation. (Remark that the interpretation of a term is not really by induction on the type inference, but directly by induction on the term: we can thus apply it to untyped terms as well.)

The interpretation becomes: if t is a differential λ-term with its free variables among x 1 , . . . , x n , we interpret t by a subset of

M f (S W )ו • •×M f (S W )×S W . In the sequel, γ is a tuple in M f (S W ) × • • • × M f (S W
) and we use γ(x) for the projection on the appropriate coordinate.

•

[[x]] = {(γ, s)} where γ(x) = [s] and γ(y) = [] otherwise • [[λx.t]] = {(γ, (µ, s)) | (γ x:=µ , s) ∈ [[t]]} • (γ, s) ∈ [[(t)u]] iff        (γ 0 , Node(µ, s)) ∈ [[t]] for some µ = [s 1 , . . . , s n ] s.t. (γ i , s i ) ∈ [[u]] for i = 1, . . . , n and γ = γ 0 + γ 1 + . . . + γ n ; • [[0]] = ∅; • [[t 1 + t 2 ]] = [[t 1 ]] ∪ [[t 2 ]]; • (γ, µ, s ′ ) ∈ [[D t • u]] iff    (γ 1 , Node(µ + [s], s ′ )) ∈ [[t]] for some (γ 2 , s) ∈ [[u]] s.t. γ = γ 1 + γ 2 .
Proposition 32 For any closed differential λ-term t, we have that [[t]] is a safety property for W .

We have thus, in effect, constructed a non-trivial (in the sense that not all subsets of S W are safety properties) denotational model for the untyped differential λ-calculus. This is particularly interesting because the original model for differential λ-calculus (finiteness spaces) did not have a reflexive object: they could not interpret fixpoint combinators (see [START_REF] Ehrhard | Finiteness spaces[END_REF]).

Classical Linear Logic

If one has in mind the definition of negation (see page 15), the next result can look quite surprising: interaction systems can interpret classical linear logic.

In other words, for any interaction system w, we have w ≃ w ⊥⊥ . The reason behind that is that our notion of morphism is not the notion of "componentwise" morphism. Even though the actions/reactions in w ⊥⊥ are very complex sets, the way they interact with states remains relatively simple.

The reason we haven't shown this result in section 2 is that the principle at work is highly non-constructive and that natural generalizations of interaction systems are unlikely to satisfy it.

Recall that any object can be used to represent ⊥ in the intuitionistic case. However, in or case, the object I plays a very special role. For ⊥ = I, we have:

Proposition 33 In Int, for any interaction system w, the identity relation is an isomorphism between w and w ⊥⊥ .

Equivalently, the object ⊥ is dualizing in Int.

PROOF. The principle at stake in the proof is the contrapositive of the axiom of choice:

CtrAC : (∃a ∈ A)(∀d ∈ D(a)) ϕ(a, d) ⇔ (∀f ∈ a∈A D(a))(∃a ∈ A) ϕ(a, f (a))
When the domain D(a) for the universal quantifier doesn't depend on a ∈ A, we can simplify it into:

CtrAC : (∃a ∈ A)(∀d ∈ D) ϕ(a, d) ⇔ (∀f ∈ A → D)(∃a ∈ A) ϕ(a, f (a))
Here are the components of w ⊥⊥ :

A ⊥⊥ (s) =   a∈A(s) D(s, a)   → A(s) D ⊥⊥ (s, F ) = a∈A(s) D(s, a) n ⊥⊥ (s, F, g) = s[F (g)/g(F (g))] .
That equality is a simulation from w ⊥⊥ to w takes the form:

(∀s ∈ S) (∀F ∈ A ⊥⊥ (s))(∃a ∈ A(s)) (∀d ∈ D(s, a))(∃g ∈ D ⊥⊥ (s, F )) s[a/d] = S s[F (g)/g(F (g))]
.

By applying the contraposition of the axiom of choice on ∃a∀d, this is equivalent to

(∀s ∈ S) (∀F ∈ A ⊥⊥ (s)) ∀f ∈ a∈A(s) D(s, a) (∃a ∈ A(s))(∃g ∈ D ⊥⊥ (s, F )) s[a/d] = S s[F (g)/g(F (g))] .
We can swap quantifiers and obtain, by the definitions of A ⊥ , D ⊥ and A ⊥⊥ ,

(∀s ∈ S) (∀f ∈ A ⊥ (s))(∀F ∈ A ⊥ (s) → D ⊥ (s, )) (∃g ∈ D ⊥⊥ (s, F ))(∃a ∈ D ⊥ (s, f )) s[a/f (a)] = S s[F (g)/g(F (g))]
.

We can now apply the contraposition of the axiom of choice on ∀F ∃g to get the equivalent formulation

(∀s ∈ S) (∀f ∈ A ⊥ (s))(∃g ∈ D ⊥⊥ (s, F )) (∀b ∈ D ⊥ (s, g))(∃a ∈ D ⊥ (s, f )) s[a/f (a)] = S s[b/g(b)] .
Since D ⊥⊥ is equal to A ⊥ , this is obviously true.

Thus, we can conclude that equality is a simulation from w ⊥⊥ to w. 2

We obtain a surprising corollary:

Corollary 34 Any interaction system is isomorphic to an interaction where the sets of reactions do not depend on a particular action. (More precisely, for any state s, the function a → D(s, a) is constant.)

PROOF. Just notice that w ⊥⊥ satisfies this property. 2

Finally, we have

Corollary 35 The category Int is ⋆-autonomous (see [START_REF] Barr | * -autonomous categories and linear logic, Mathematical Structures in Computer Science[END_REF]), we can thus interpret classical linear logic.

PROOF. Once we know that ⊥ is dualizing, the remaining condition are fairly easy to check: the following diagram should be commutative

w 1 ⊸ w 2 ⊥ -w ⊥ 2 ⊸ w ⊥ 1 w ⊥⊥ 1 ⊸ w ⊥⊥ 2 ⊥ ? d -1 w 1 • • d w 2 -
where d w is the natural isomorphism from w to w ⊥⊥ . This is immediate since d w is the identity on S and ⊥ is the "converse" operation of a relation. (See footnote 9 on page 27.)

We can then unfold all the usual technology to give a denotational model for classical linear logic.

2

It is interesting to highlight some aspects of this model

• Int is a "games" model for full classical linear logic. The isomorphism between w and w ⊥⊥ is given by the identity relation. • The constructions are quite different from usual games constructions; in particular, they have a strong synchronous feeling. • The notion of strategy is not used to define morphisms; rather, we use the notion of simulation. • The fact that w ≃ w ⊥⊥ seems rather accidental as it is not expected to hold in any generalized version of interaction systems. (See the discussion about containers in section 6.2). This fact is also highly non-constructive and almost counter-intuitive.

Putting the model of the differential λ-calculus with the dualizing object ⊥, it is expected that we get a model for Lionel Vaux's "differential λµ-calculus" (see [START_REF] Vaux | Differential λµ-calculus[END_REF]), either in Vaux's setting (typed) or in an untyped setting.

6 Related Notions

Predicate Transformers

The category Int has a very concrete feeling. In [START_REF] Hyvernat | Predicate transformers and linear logic: yet another denotational model[END_REF], we have developed a model for full linear logic with a different intuition: the category of predicate transformers with forward data-refinements:

Definition 36 If S is a set, a predicate transformer on S is a monotonic (w.r.t. inclusion of subsets) function from P(S) to P(S).

If F 1 and F 2 are predicate transformers respectively on S 1 and S 2 , a forward data-refinement from

P 1 to P 2 is a relation r ⊆ S 1 ×S 2 s.t. r •F 1 ⊆ F 2 • r . 10 (Extensional ordering.)
Such predicate transformers with forward data-refinements form a category called PT.

An interaction system can be seen as a concrete representation for a predicate transformer. More precisely:

Proposition 37 The operation w → w • from Int to PT defined as The intuition in s ∈ w • (x) is that the Angel has a foolproof way to reach x in exactly one interaction.

PROOF. The action on morphisms is just the identity: we thus need to show that r is a simulation from w 1 to w 2 iff r is a forward data-refinement from w

• 1 to w • 2 .
The proof is not very difficult and can be found in [START_REF] Hyvernat | A logical investigation of interaction systems[END_REF]. 2

The interesting point is that all the constructions presented above are the concrete versions of the constructions presented in [START_REF] Hyvernat | Predicate transformers and linear logic: yet another denotational model[END_REF]. For example, we have

(w 1 ⊗ w 2 ) • = w • 1 ⊗ w • 2 10
Where r is the direct image of r:

s 2 ∈ r (x) iff (∃s 1 ) (s 1 , s 2 ) ∈ r ∧ s 1 ∈ x.
where ⊗ on the left is the synchronous tensor on interaction systems and the tensor on the right is the tensor on predicate transformers. 11Another interesting example is the fact that (w ⊥ ) • = (w • ) ⊥ . This is interesting because the definition of duality in the case of predicate transformers is very simple, and involutivity is trivial:

F ⊥ (x) = F (x)
where x represents the S-complement of x (i.e. x = S \ x).

Surprisingly, proposition 37 can be strengthened in an ad-hoc way to read:

Proposition 38 The categories Int and PT are equivalent. Moreover, this equivalence is a "retract".

PROOF.

By "retract", we mean the following: there is a functor F from PT to Int which satisfies F (F ) • = F and F (w • ) ≃ w. In other words, we obtain equal object in one direction but only isomorphic objects in the other direction.

This functor F is defined as follows: let F be a predicate transformer on S, define F to be the interaction system on S with components

F (F ).A(s) = {x ⊆ S | s ∈ F (x)} F (F ).D(s, x) = x F (F ).n(s, x, s ′ ) = s ′
Checking that this operation does define a functor is left as an exercise.

(See [START_REF] Hyvernat | A logical investigation of interaction systems[END_REF].) 2

Once more, we separate propositions 37 and 38 because while we expect proposition 37 to hold for different generalizations of interaction systems / predicate transformers (see theorem 3.4 in [START_REF] Abott | Containers -constructing strictly positive types[END_REF]), proposition 38 seems very specific to this particular case.

Containers

In [START_REF] Abott | Containers -constructing strictly positive types[END_REF], the authors study the notion of container, a structure bearing several similarities with the notion of interaction system. They work in a variant of Martin-Löf type theory ( [START_REF] Martin-Löf | Intuitionistic type theory[END_REF][START_REF] Nordström | Programming in Martin-Löf's type theory. An introduction[END_REF]), a dependent predicative type theory.

Mild knowledge about this type theory is assumed in this section.

Simply, a container is given by the following:

• a set A of shapes;

• and for any a ∈ A, a set D(a) of positions.

A morphisms from (A 1 , D 1 ) to (A 2 , D 2 ) is given by a pair (f, u) where f is a function f : A 1 → A 2 and u is a family of functions indexed by A 1 and we have u a 1 : D 2 (f (a 1 )) → D 1 (a 1 ). This is reminiscent of interaction systems in the following way: any interaction system on the set of states { * } (singleton set) can be seen as a container, and any container can be seen as an interaction system on { * }.

The links between container morphisms and simulations is subtler: a simulation from w 1 to w 2 (two interaction systems on { * }) is given by a relation r ⊆ { * } × { * } ≃ { * }. In Martin-Löf type theory, a subset is seen as a propositional function r : { * } → Set, i.e. a set. The condition required to make this "relation" a simulation is the following:

r ⇒ (∀a 1 ∈ A 1 )(∃a 2 ∈ A 2 )
(∀d 2 ∈ D 2 (a 2 ))(∃d 1 ∈ D 1 (a 1 )) r .

We can apply the (constructive) axiom of choice to skolemize this and we obtain r ⇒ (∃f : Thus, a constructive (in the sense of Martin-Löf type theory) simulations between two interaction systems on { * } is given by:

A 1 → A 2 ) ∃u : a 1 ∈A 1 D 2 (f (a 1 )) → D 1 (a 1 ) (∀a 1 ∈ A 1 )(∀d 2 ∈ D 2 (f (a 1 ))) r
• a set r;

• and a function r → (Σf : A 1 → A 2 ) a 1 ∈A 1 D 2 (f (a 1 )) → D 1 (a 1 ).

Equivalently, a simulation between two interaction systems on { * } is nothing but a family of container morphisms between the corresponding containers! However, the difference is that while container morphisms are identified when the functions acting on actions / reactions are extensionally equal, simulations are identified when the relations between states are extensionally equal. In other words, two simulations (r 1 , (f 1 , u 1 )) and (r 2 , (f 2 , u 2 )) between interaction systems on { * } are equal when there are "translating functions" r 1 → ← r 2 . 12If we adopt a classical point of view, then everything is rather boring: there is at most one non-empty simulation between two interaction systems on { * }: the relation {( * , * )}. The links with container morphisms is then the following:

if there is at least one container morphisms from w 1 to w 2 , then there will be exactly one non-empty simulation from w 2 to w 2 ; if there are no container morphism from w 1 to w 2 , then the only simulation from w 1 to w 2 will be the empty simulation.

This whole theory of containers can be extended to work in a large class of locally cartesian closed categories. (See [START_REF] Abott | Containers -constructing strictly positive types[END_REF].) In such a setting, one needs to take care of additional coherence diagrams, but the idea is similar.

There is currently some work being done on generalizing containers to a notion of dependent containers, i.e. interaction systems. The idea, following the original intuition of [START_REF] Seely | Locally Cartesian closed categories and type theory[END_REF] and [START_REF] Hofmann | On the interpretation of type theory in locally cartesian closed categories[END_REF] is to define a dependent container in a locally cartesian closed category C as:

• an object S in C;

• an object A in C/S; • an object D in C/(Σ S A); 13• a morphism n in C(Σ Σ S A D , S).

The appropriate notion(s) of morphism is not entirely clear and still under heavy discussion...

Conclusion

We have developed a new category where objects are games to model linear logic or λ-calculus. What is rather new is the use of a notion of simulation for morphisms: the notion of strategy is not used in this model! Strategies do however appear implicitly in the notion of safety property which are the "points" of our model: a safety property is set of states for which there is an infinite strategy which restrict interaction to stay in the safety property. This strategy is only guaranteed to exists, but there is in general no way to obtain it.

Some of the interesting points about this model are that is allows to model full linear logic (it can even be extended to second order). Moreover, and this is relatively new, it can interpret the untyped differential λ-calculus.

An interesting project is to see whether one can apply the technology developed here in order to give denotational models for more interesting programming languages. PCF-like languages ought to be rather easy, but interaction systems (or predicate transformers) are rooted in "real" programming 14 so that we might expect to have access to many programming features...

A The Simply Typed Differential λ-calculus

The syntax of the simply typed differential λ-calculus is given by the following grammar:

t, u, t 14 Predicate transformers were used to give a semantics to sequential programs by Dijkstra (wp or wlp calculus) and have been extended to deal with specifications as well (whole field of refinement calculus); interaction systems, as hinted in the first section seem appropriate to describe interfaces.

Lemma 4

 4 The operation w → |w| = w.S is a faithful functor from Int to Rel. Its action on morphisms is just the identity. This functor has a right adjoint S → magic(S) and a left adjoint S → abort(S) defined by (where { * } denotes a singleton set) magic(S).A(s) = { * } abort(S).A(s) = ∅ magic(S).D(s, * ) = ∅ abort(S).D(s, ) = magic(S).n(s, * , ) = abort(S).n(s, , ) =

  a reaction is given by a list of reactions d in L.D(s, a); • the next state is the equivalence class containing the list s[a/d] (the orbit of s[a/d] under the action of the group of permutations).

(

  s c , (s c,1 , . . . , s c,i , s c,i+1 , . . . , s c,n )) ∈ m c ⇔ (s c , (s c,1 , . . . , s c,i+1 , s c,i , . . . , s c,n )) ∈ m c

?

  are commutative. The first diagram is easily shown to be commutative. For the second one: suppose (s c , [s 1 , .

s

  ∈ w • (x) ⇔ (∃a ∈ w.a(s))(∀d ∈ w.D(s, a)) s[a/d] ∈ x can be extended to a full and faithful functor from Int to PT.

which is logically equivalent to r ⇒ (∃f : A 1 → A 2 )

 12 ∃u : a 1 ∈A 1 D 2 (f (a 1 )) → D 1 (a 1 ) ⊤where ⊤ denotes the true proposition (or the singleton set in Martin Löf type theory).

  . . , s n ], [s n+1 , . . . , s n+m ]) ∈ m• r. This is equivalent to saying that there are s c,1 , . . . , s c,n+m in S c s.t. • and (s c , (s c,1 , . . . , s c,n+m )) ∈ m c . That (s c , [s 1 , . . . , s n ], [s n+1 , . . . , s n+m ]) is in r ⊗ r • c means that there are s 1 , . . . , s n ]) ∈ r and (s 2 c , [s n+1 , . . . , s n+m ]) ∈ r, i.e. there are s 1 c and s 2 c in S c , and s c,1 , . . . , s c,n , s c,n+1 , . . . , s c,n+m in S c s.t.

	c
	and s 2 c in S c s.t.
	• (s c , (s 1 c , s 2 c )) ∈ m c
	• and (s 1 c , [s 1

• (s c,i , s i ) ∈ r for all i = 1, . . . , n + m

It is possible to devise interaction systems with such side-effects, but the theory of those is still to be developed.

Recall that A + B = {1}×A ∪ {2}×B.

This is well known for abelian categories (see[11, chap. 8]), but the existence of inverses is irrelevant.

This is well defined since P({ * }×S) ≃ P(S).

the relational interpretation is folklore, at least in Marseille and Paris, but it is surprisingly difficult to find an early reference to it. For those who want to see the concrete definition of the interpretation, we refer to of[15, app. 4].

There, the equivalent notion of predicate transformers rather than interaction systems is used, but as we will show in section 6.1, the two categories are equivalent.

The applications of the isomorphism σ : (A ⊗ B) ⊗ C → A ⊗ (B ⊗ C) are omitted for readability.

The converse r ∼ of a relation is defined as (s 2 , s 1 ) ∈ R ∼ iff (s 1 , s 2 ) ∈ r.

(s 1 , s 2 ) ∈ F 1 ⊗F 2 (r) iff (∃x⊆S 1 )(∃y⊆S 2 ) x×y ⊆ r ∧ s 1 ∈ F 1 (x) ∧ s 2 ∈ F 2 (y)

Note that since r 1 and r 2 are "propositions", we do not require that those translating functions are inverse of each other.

[START_REF] Melliès | Categorical models of linear logic revisited[END_REF] Recall that in a locally cartesian closed category, if B is a slice in C/A, we write Σ A B for the codomain of B.

where substitution is extended in the following "obvious" way:

Differential reduction is defined as:

where ∂t/∂x • u, the linear substitution of x by u in t is defined as:

Terms are quotiented by the (contextual closure of the) following equations:

The typing rules are

(1) Γ ⊢ x : τ if "x : τ " appears in Γ;

(2) Γ, x : τ ⊢ t : σ Γ ⊢ λx.t : σ → τ ;

(3)

Typed terms enjoy the Church-Rosser property and strong normalization (w.r.t. β/differential reduction).


Bruno Schapira

RANDOM WALK ON A BUILDING OF TYPE Ãr AND BROWNIAN MOTION OF THE WEYL CHAMBER

Keywords: Random walk, affine building, root systems, GUE process A.M.S. classification: 05C25, 60B10, 60B15, 60C05, 60J10, 60J25, 60J35, 60J60

. The main ingredients of the proof are a combinatorial formula on the building and the estimate of the transition density proved in [AST].

Introduction

The Brownian Motion of the Weyl chamber, or intrinsic BM, considered by Biane in [START_REF] Ph | Quelques propriétés du mouvement Brownien dans un cône[END_REF], has bring recently a growing attention, due to his apparition in many branches of the probability theory. In dimension 1 for instance it is the Bessel 3 process, whose importance is well known. More generally it appears in particular in the theory of random matrices, of particles systems, in queuing theory, in oriented percolation (see [O] for an overview), but also in the theory of stochastic processes on Riemannian symmetric spaces [ABJ], and more recently in the theory of Dunkl and Heckman-Opdam processes [GY] [S]. It takes values in a Weyl chamber, denoted here by a + , which is a cone of the Euclidean space R r delimited by hyperplanes satisfying some conditions. More precisely it may be defined as the Brownian motion killed on the boundary of a + and conditioned (in the sense of Doob) never to escape the cone.

A basic question is to find a natural discrete version of this process, i.e. some random walk on some lattice of R r which after renormalization converges toward this process. An example of such random walk has been introduced and first studied by Biane [Bi2] [Bi3] [Bi4] and then by Biane, Bougerol and O'Connell [BiBO]. It is defined on the so-called weight lattice, actually its positive part P + , which is a natural choice, well known in the theory of root systems, since it has roughly the same geometric structure than a + (see the next section for details). So this random walk is defined analogously, as the simple random walk on P + , killed on the boundary of P + , and conditioned never to touch it. One can compute explicitly its transition kernel, with the help of the reflexion principle, and then prove its convergence, after the usual renormalization, toward the intrinsic BM [BiBO]. In fact [Bi2] [Bi4] this random walk appears naturally in the context of quantum random walks on the dual of a compact Lie group.

In this paper we study another discrete version of the intrinsic BM, when the cone a + is associated to a root system of type A r (see the next section). In this case the intrinsic BM identifies with the process of eigenvalues of hermitian matrices with zero trace, whose coefficients are Brownian motions (also called GUE process). Our random walk is also defined on the weight lattice but indirectly. It is the socalled radial part of some nearest neighbor random walk (X n , n ≥ 0) on an affine building of type Ãr . To be short, let say simply that a building is some graph containing copies, called apartments, of the weight lattice. Once a vertex O, an apartment containing O, and its positive part P + , have been fixed, then the radial part of a vertex x is its projection x, in some sense, onto P + . This notion of radial part generalizes the usual notion of distance between two vertices in regular trees, which are buildings of type Ã1 . Call A the transition operator of the random walk (X n , n ≥ 0). Let F 0 be some eigenfunction of A at the bottom of its spectrum. Let (Y n , n ≥ 0) be the relativized F 0 -random walk in the sense of Doob. For N ≥ 0, let (Y N t , t ≥ 0) be the continuous time normalized F 0 -random walk defined by

Y N t = Y [N t] /
√ N for all t ≥ 0. Then the main result of this paper is that the sequence (Y N t , t ≥ 0) converges in law in the path space toward the intrinsic BM, when N → +∞.

The idea of this result goes back to the work of Bougerol and Jeulin [START_REF] Ph | Brownian bridge on hyperbolic spaces and on homogeneous trees[END_REF]. They proved it in the tree case, which as we already mentioned are particular examples of buildings (they are affine buildings of rank one). In the same time they proved an analogue version on Riemannian symmetric spaces of the noncompact type of rank one (in particular on complex and real hyperbolic spaces), which are continuous versions of regular trees. Then they managed to extend their result with Anker [ABJ] [BJ1] on Riemannian symmetric spaces of higher rank. The author also proved it in the general context of Heckman-Opdam's theory [S]. So the present paper investigates the higher rank case on the discrete space level. However this story may not be finished yet, since here we consider essentially only one particular random walk and only on a particular type of affine buildings (those associated to root systems of type A). The main reason for this is that we need good estimates of the transition densities of the random walk, which for the moment are known only in few cases [AST]. Random walks on buildings have already been studied so far. In particular [CaW] and [START_REF] Parkinson | Isotropic random walks on affine buildings[END_REF] prove a law of large numbers, central and local limit theorems. This paper is organized as follows. In the next section we recall some definitions and basic properties of the main objects of study. In section 3 we define precisely the F 0 -random walks and show that they appear naturally as limits of random bridges when the length of the bridge tends to infinity. Then in section 4, we compute explicitly the transition densities of the radial part of nearest neighbor random walks. This, in our opinion, is actually the main part of the proof (once the results of [AST] are known). It allows to derive directly the result for all nearest neighbor random walks when the starting point of the intrinsic BM lies inside the Weyl chamber. For this we have to renormalize also the starting point of the random walks and use a general criteria of Ethier and Kurtz [EK] on the convergence of generators. We explain all this in section 5. In the last section we consider the case where the intrinsic BM starts from the origin. This case is more difficult, since the criteria of Ethier and Kurtz is not sufficient. We need in addition estimates of the transition densities of the random walk to control its norm in small times. These estimates, as we already mentioned were proved recently in [AST].

Preliminaries

The root system. We denote by a the Euclidean space of dimension r, endowed with its scalar product < •, • >. We denote by a C := a + ia its complexification. Let R ⊂ a be a root system of type A r . One can define it (see [Bou]) as the set of vectors e ie j , for 1 ≤ i = j ≤ r + 1, where (e 1 , . . . , e r+1 ) is the canonical basis of R r+1 and a is the hyperplane {< x, e 1 + • • • + e r+1 >= 0}, endowed with the restriction of the canonical scalar product on R r+1 . We denote by | • | the associated norm. A subset of positive roots R + is defined as follows: one first choose arbitrarily u ∈ a such that < u, α > = 0 for all α ∈ R. Then one set

R + = {α ∈ R |< α, u > > 0}.
For instance one can take the set of vectors e ie j , where i < j. The positive Weyl chamber associated to a + is defined by

a + = {x ∈ a |< α, x > > 0 ∀α ∈ R + }.
We denote by a + its closure and by ∂a + its boundary. If α ∈ R, we denote by r α the orthogonal reflexion with respect to the hyperplane orthogonal to α. The Weyl group W 0 is the finite subset of the orthogonal group generated by the r α 's with α ∈ R. In fact R is generated by the set Π := {α 1 , . . . , α r }, where α i = e ie i+1 (these elements are called the simple roots). Furthermore W 0 is generated by the r i := r αi , i = 1, . . . , r. Any w ∈ W 0 can be written under the form r i1 . . . r i l . The smallest possible l in such writing is called the length of w, and is denoted by l(w). The dual basis of Π is denoted by {λ 1 , . . . , λ r }. More precisely we assume that < α i , λ j >= δ i,j for all i, j. The elements of the dual basis are called the fundamental weights. The weight lattice P is by definition the Z-lattice generated by the fundamental weights. We denote by P + the subset of positive weights, i.e. P ∩ a + , and by P ++ the subset of regular positive weights, i.e. P ∩ a + . The lattice P generates a simplicial complex, called the Coxeter complex (see [START_REF] Parkinson | Spherical harmonic analysis on affine buildings[END_REF] for a more precise definition), which is denoted by P. We attribute labels lying in the set {0, . . . , r} to the elements of P as follows: we attribute the label i to λ i , and for any simplex of maximal dimension we assume that the set of labels of its extremal vertices is exactly {0, . . . , r}. We denote by W the affine Weyl group, which is generated by W 0 and the translations by elements of P . We denote by W the extended affine Weyl group, which is generated by W and the group Ω which acts by circular permutation on the fundamental weights and 0 (see [Bou]). The group W is in fact generated by Π and the orthogonal reflexion r 0 with respect to the hyperplane {< x, α 1 + • • • + α r >} = 1. This allows to define the length of w ∈ W analogously as in W 0 . Then we set q w = q l(w) . This definition extends to W : if w = wg, with w ∈ W and g ∈ Ω, then we set q w = q w . One can prove (see [START_REF] Parkinson | Spherical harmonic analysis on affine buildings[END_REF]) that if t λ is the translation by λ ∈ P + , then q t λ = q P α∈R + <α,λ> . It will be convenient to extend this formula to any λ ∈ P . So we set:

qt λ := q P α∈R + <α,λ> ∀λ ∈ P.
The affine building. An affine building (see [START_REF] Parkinson | Spherical harmonic analysis on affine buildings[END_REF] or [Ron]) of type Ãr is a nonempty simplicial complex containing sub-complexes, called apartments, such that:

• Any apartment is isomorphic (see [START_REF] Parkinson | Spherical harmonic analysis on affine buildings[END_REF]) to the Coxeter complex P.

• Given two chambers (simplex of maximal dimension) there exists an apartment containing both. • Given two apartments having at least one common chamber there exists a unique isomorphism between them fixing pointwise their intersection. We denote by X the set of vertices (simplexes of dimension 0) of the building and we fix one, called O. The preceding definition allows to attribute labels to elements of X such that O has label 0 and isomorphisms in the definition preserve labels.

Let us mention, to avoid any ambiguity, that chambers of the building, also called alcoves, which are compact simplexes, must not be confused with the positive Weyl chamber, which is a chamber of the root system and in particular an unbounded open cone of a.

Two chambers of the building are called adjacent if they are distinct and have a common face (simplex of co-dimension 1). A gallery is a sequence of chambers (C 0 , . . . , C n ), where for all i ≤ n -1, C i and C i+1 are adjacent. The integer n is called the length of the gallery. We define the distance between two chambers C and C ′ as the minimal length of a gallery starting from C and ending in C ′ , and we denote it by d(C, C ′ ). If F a face of a chamber C, we will assume that the number q of chambers adjacent to C and containing F is independent of F and C (we say that the building is regular). For r = 1 for instance, X is a tree where each vertex has q + 1 neighbors.

If x ∈ X there exists by definition an apartment containing x and O, and an isomorphism between this apartment and P sending O on 0 and x on an element of P + . The image of x by this isomorphism, let say x, is uniquely defined and called the radial part or coordinate of x. When r = 1 for instance P + identifies with N and x is the distance (in the usual sense) between x and O. For λ ∈ P + , we denote by V λ (O) the set of vertices of coordinate λ and we call it the sphere of radius λ centered in O. Given a vertex x we define also the sphere V λ (x) of radius λ centered in x, as the set of vertices y ∈ X such that there exists an apartment A containing x and y and an isomorphism between A and P, preserving labels up to translation, and sending x on 0 and y on λ. For all λ ∈ P + , V λ (x) is a finite subset of X , whose cardinality N λ is independent of x. If λ ∈ P , let W 0λ be the stabilizer of λ under the action of W 0 . Then we have the formula (see [START_REF] Parkinson | Spherical harmonic analysis on affine buildings[END_REF] Formula (1.5)):

N λ = W 0 (q -1 ) W 0λ (q -1 ) q t λ ,
where V (q -1 ) = w∈V q -1 w for any subgroup V of W 0 . We define also the function

π on P by π(λ) = α∈R + < α, λ > .
The Macdonald polynomials. The functions c and h are defined for z ∈ a C by

c(z) = α∈R + 1 -q -1 e -<α,z>
1e -<α,z> , and

h(z) = r i=1 λ∈W0λi
e <λ,z> .

We set also h := h/h(0). Macdonald's polynomials are defined (see for instance [Ca] [M1] [M2] or [START_REF] Parkinson | Spherical harmonic analysis on affine buildings[END_REF]) for λ ∈ P + and z ∈ a C by

P λ (z) = q -1 2 t λ W 0 (q -1 ) w∈W0 c(w -1 z)e <wλ,z> . (1)
The function F 0 is defined on P + by F 0 (λ) = P λ (0). We recall the estimate in P + (see [AST]):

F 0 (λ) ≍ q -1 2 t λ α∈R + (1+ < α, λ >). (2)
Moreover when < α, λ >→ +∞ for all α ∈ R + , then

F 0 (λ) ∼ const • q -1 2 t λ π(λ).
(3) Symmetric nearest neighbor random walk. By definition it is a Markov chain (X n , n ≥ 0) on X whose transition densities are equal to

p(x, y) = p i if y ∈ V λi (x), 0 otherwise,
where the p i 's satisfy the condition

r i=1 p i N λi = 1. Let ρ = r i=1 p i q 1 2 t λ i |W 0 λ i |,
be the spectral gap (the fact that ρ is well the spectral gap results from Formula (2) in [AST]). The radial random walk is by definition the Markov chain (X n , n ≥ 0) on P + . We denote by p its transition kernel. A particular example is the so-called simple random walk. Its transition probabilities are determined by

p i = q -1 2 t λ i r i=1 q -1 2 t λ i N λi , (4)
for all i ≤ r. For this random walk we have a relatively simple integral formula for the transition kernel (see for instance [START_REF] Parkinson | Isotropic random walks on affine buildings[END_REF] Formula (1.10) and [AST]

Formula (2)): if U = {θ ∈ a |< α, θ > ≤ 2π ∀α ∈ R},
and if p n (O, x) denotes the probability, starting from O, to arrive in x ∈ V λ (O) in n steps, then p n (O, x) = const • ρn U hn (iθ)P λ (iθ) dθ |c(iθ)| 2 . (5)
The Brownian motion of the Weyl chamber. This process is also called the intrinsic Brownian motion. There are many ways to define it. We will only recall some of them here. Before this, to avoid some (linear) time change in Theorem 6.1, we define another norm on a:

||x|| 2 := 1 h(0) r i=1 λ∈W0λi < λ, x > 2 .
Since any homogeneous W 0 -invariant polynomial of degree 2 is proportional to | • | 2 (see [Hel]), one knows that

||•|| is proportional to |•|. An elementary calculus shows that in fact || • || 2 = 2 r-2 (2 r -1) -1 | • | 2 .
We will denote by << •, • >> the scalar product associated to || • ||, and we set c := 2 r-2 (2 r -1) -1 . Now one can define the intrinsic BM (see Biane [START_REF] Ph | Quelques propriétés du mouvement Brownien dans un cône[END_REF] or Anker-Bougerol-Jeulin [ABJ]) as the π-process, in the sense of Doob, of the standard Brownian motion in (a, || • ||) killed on the boundary of a + . In fact, as Biane noticed, π is the unique positive harmonic function which vanishes on ∂a + . So one can also interpret this process as the Brownian motion killed on ∂a + and conditioned to never touch ∂a + (or to escape a + at infinity). From this point of view it is a natural generalization of the Bessel-3 in higher dimension. In fact Biane, Bougerol and O'Connell [BiBO] proved a deeper result which reinforces this. They proved that this process can be obtained by some transformation of the Brownian motion on a, which generalizes the Pitman transform 2S -B in dimension 1. But one can also define it as the Dunkl process with parameter k = 1 (see [GY]). In particular it is a Feller process with generator D (see [S]) defined for a regular and W 0 -invariant function f by

Df (x) = 1 2 ∆f (x)+ << ∇ log π, ∇f >> (x) ∀x ∈ a + ,
where ∆ is the usual Laplacian on (a, || • ||). Finally, since our definition coincides with the definition in [ABJ] up to a linear time change, one can deduce from Formula (3.5) in [ABJ] that the law of this process starting from 0 has density

p t (0, x) = const • 1 t |R + |+ r 2 π(x) 2 e -|x| 2 2ct ,
for all t ≥ 0 and all x ∈ a + .

3. The F 0 -random walk Let (X n , n ≥ 0) be a symmetric nearest neighbor random walk, with transition kernel p. The function F 0 is an eigenfunction of its transition operator (see [START_REF] Parkinson | Spherical harmonic analysis on affine buildings[END_REF] Theorem 3.22): y∈X p(x, y)F 0 (y) = ρF 0 (x), for all x ∈ X . Then the F 0 -random walk (Y n , n ≥ 0) is the Markov chain on X with transition kernel q q(x, y) = p(x, y) F 0 (y) F 0 (x) ρ-1 .

We denote by (X N,0 n , n ≥ 0) the bridge of length N around O, i.e. the random walk starting from O and conditioned to come back in O at time N . The next proposition shows that the F 0 -random walk can be seen as a loop of infinite length around O.

There is an analogue result on Riemannian symmetric spaces G/K [ABJ] and in Heckman-Opdam's theory [S].

Proposition 3.1. When N → +∞, (X N,0 n , n ≥ 0) converges in law, in the path space, toward (Y n , n ≥ 0).

Proof. Let P be the law of (X n , n ≥ 0) and let F n := σ(X k , k ≤ n) be its natural filtration. Let P N,0 be the law of (X N,0 n , n ≥ 0). The following absolute continuity relation holds:

P N,0 |Fn = p N -n (O, X n ) p N (O, O) P |Fn , (6)
for all n ≥ 0. To simplify, assume first that (X n , n ≥ 0) is the simple random walk. Then from (5), we deduce that for all λ ∈ P + and all x ∈ V λ (O),

p N -n (O, x) p N (O, O) = ρ-n U hN-n (iθ)P λ (iθ)|c(iθ)| -2 dθ U hN (iθ)P 0 (iθ)|c(iθ)| -2 dθ .
Next in the above integrals we make the following change of variables:

θ → θ/ √ N -n, respectively θ → θ/ √ N . Then one can observe that hN (i θ √ N ) → e -1 2h(0) P λ <λ,θ> 2 = e -1 2 ||θ|| 2 ,
when N → +∞. Moreover c -1 (iθ) is equivalent (up to some constant) to π(iθ) near 0. Thus we get the following convergence result:

p N -n (O, x) p N (O, O) → ρ-n P λ (0) P 0 (0) ,
when N → +∞. Together with the relation ( 6) this proves the proposition for the simple random walk. In general h has to be replaced by some sum of exponentials but whose coefficients are not necessarily equal (see [START_REF] Parkinson | Isotropic random walks on affine buildings[END_REF] Formula (1.10) and [AST] Formula (2)). However the same proof applies as well.

Transition probabilities of the radial random walk

In this section we give explicit formula for the transition probabilities of radial part of nearest neighbor random walks. We will use them in the next section to prove Theorem 5.1. These formula are derived from a combinatorial calculus (Proposition 4.1 below) which could be of independent interest. One can find a similar result in [CaW] Lemma 2.1, and at the end of Parkinson's thesis [START_REF] Parkinson | Buildings and Hecke Algebras[END_REF] for all affine buildings of rank 2.

Proposition 4.1. For all λ ∈ P ++ , x λ ∈ V λ (O), w ∈ W 0 and i ∈ {1, . . . , r},

|V λ+wλi (O) ∩ V λi (x λ )| = q 1 2 t λ i q 1 2 t wλ i .
Proof. Let us fix λ ∈ P ++ and x λ ∈ V λ (O). Let w ′ ∈ W 0 be of maximal length such that w ′ λ i = wλ i . Since the desired formula does not change when we replace w by w ′ , one can always assume that w = w ′ . Now by definition of q, we know that if we fix a face F containing x λ , then there are exactly q + 1 chambers containing F . Equivalently, if we fix a chamber C and one of its faces F , there are exactly q vertices x ∈ X , such that (F, x) defines a chamber adjacent to C. Denote by C + and C -the chambers (in P) containing λ and all weights λ + λ i , respectively λλ i , for i = 1, . . . , r. We set also C w := t λ wt -λ C + . We know (see [START_REF] Parkinson | Spherical harmonic analysis on affine buildings[END_REF] Lemma B.2) that for all i,

V λ-λi (O) ∩ V λj (x λ ) = 1, (7) if -λ i ∈ W 0 λ j .
In other words there exists a unique chamber in the building, also denoted by C -, containing x λ and whose vertices have coordinate λ, λλ 1 , . . . , λλ r . The same argument shows that for any vertex x ∈ X , there exists a unique chamber of the building, let say C x , containing x and at minimal distance from C -. Now we claim that

|V λ+wλi (O) ∩ V λi (x λ )| = q lw , (8)
where l w = d(C -, C w ). If l w = 0 then the claim follows from (7). So assume that l w > 0. Let G be a gallery in P of length l w starting from C -and finishing in C w . From the preceding discussion we see that there exists q lw galleries in the building, starting from C -and whose radial part coincides with G. Let (C -= C 0 , C 1 , . . . , C lw ) be one of them. Let x be the unique vertex of C lw which does not belong to C lw-1 . Let us show that x ∈ V λ+wλi (O) ∩ V λi (x λ ). First observe that the sequence of vertices x 1 , . . . , x lw = x defined by x k ∈ C k and x k / ∈ C k-1 has for radial part the analogue sequence for G. In particular x λ does not belong to this sequence (so x λ ∈ C x ) and x ∈ V λ+wλi (O). Thus there exists an apartment containing x λ and x, and an isomorphism between this apartment and P sending x λ and x respectively on λ and λ + wλ i . If one composes this isomorphism with the transformation w -1 t -λ , we obtain an isomorphism sending x λ on 0 and x on λ i , which proves that x ∈ V λi (x λ ). Therefore x ∈ V λ+wλi (O) ∩ V λi (x λ ). Next observe that two different galleries with the same radial part starting from the same chamber cannot have the same last chamber. So they necessarily finish by two different vertices x and x ′ , which proves already one inequality in (8). To show the other one, it suffices to observe that for x in V λ+wλi (O) ∩ V λi (x λ ), the associated chamber C x is well the last chamber of a gallery starting from C -with radial part G. To see this, notice that (7) implies that any apartment containing x λ and O contains C -. In particular from the definition of the building we conclude that there exists an apartment containing C x , C -and O. Any copy of G in this apartment is well a gallery starting from C -finishing in C x and with radial part G. This concludes the proof of (8). Remember that l(w) denotes the length of w. It is well known (see [Bou] Ch.6 § 1.6) that it is also equal to d(C + , C w ), and that

l(w) = R + ∩ w -1 R -.
Moreover, from Theorem 2.15(iv) in [Ron] we get,

d(C -, C w ) + d(C w , C + ) = d(C -, C + ) = R + . Thus l w = |R + | -l(w) = R + ∩ w -1 R + .
Furthermore, by our choice of w,

R + ∩ w -1 R + = α∈R + ∩w -1 R + < α, λ i > .
Indeed, for all α ∈ R + , < α, λ i > is equal to 0 or 1. If there exists α ∈ R + ∩w -1 R + such that < α, λ i >= 0, then by decomposing α in the basis Π, we see that we can always assume α ∈ Π. But r α λ i = λ i . Thus wr α λ i = wλ i . Since α ∈ Π, r α establishes a bijection from R + ∩ w -1 R + {α} onto R + ∩ (wr α ) -1 R + . Therefore l(wr α ) = l(w) + 1 and we get an absurdity. We conclude that < α,

λ i >= 1 for all α ∈ R + ∩ w -1 R + . Since α → -α is a bijection from R + R + ∩ w -1 R + onto w -1 R + R + ∩ w -1 R + , we get α∈R + ∩w -1 R + < α, λ i >= 1 2 α∈R + < α, λ i > + α∈R + < α, wλ i > .
This concludes the proof of the proposition.

We can deduce from this proposition the transition probabilities of a radial random walk:

p(λ, λ + wλ i ) = q 1 2 t λ i q 1 2 t wλ i p i ,
for all λ ∈ P ++ . In particular for the simple random walk, Formula (4) gives

p(λ, λ + wλ i ) = q 1 2 t wλ i r i=1 q -1 2 t λ i N λi . (9)
5. Convergence toward the intrinsic BM starting from the interior of the Weyl chamber Let x ∈ X and let (X x n , n ≥ 0) be a nearest neighbor symmetric random walk starting from x. Denote by (Y x n , n ≥ 0) the F 0 -random walk starting from x. If a ∈ a + , we denote by [a] one of the weight (it does not matter which one) in P + at minimal distance from a. For N ∈ N and t ∈ R + , we set

Y N,a t = Y [ √ N a] [N t] √ N .
We have Theorem 5.1. When N → +∞, the sequence of processes (Y N,a t , t ≥ 0) converges in law in D(R + , a + ) toward the intrinsic Brownian motion starting from a, up to some linear time change.

Proof. We first recall that the intrinsic Brownian motion starting from a ∈ a + takes values a.s. in a + . Moreover it is a Feller process with generator D and core C ∞ c (a + ), the space of C ∞ functions with compact support inside a + (see [S] for instance). Let (N t , t ≥ 0) be a Poisson process with parameter 1, independent of (Y t , t ≥ 0). Let (Z N,a t , t ≥ 0) be the homogeneous Markov process defined by

Z N,a t = Y [ √ N a] NNt √ N ∀t ≥ 0.
¿From the calculus of the preceding section, we see that the generator A N of this process is defined for f ∈ C ∞ c (a + ) by

A N f (λ) = ρ-1 N r i=1 q 1 2 t λ i p i λ∈W0λi q 1 2 t wλ i F 0 ( √ N λ + wλ i ) F 0 ( √ N λ) f (λ + wλ i √ N ) -N f (λ), for all λ ∈ P + / √ N . Thus (3), implies that for any function f ∈ C ∞ c (a + ), A N f converges uniformly on a + toward π -1 p(∂)(πf ), where p is the polynomial p(x) = 1 2 ρ-1 r i=1 q 1 2 t λ i p i λ∈W0λi < λ, x > 2 .
In particular p is homogeneous W 0 -invariant and of degree 2. Thus it is proportional to || • || 2 . Since ∆π = 0, ∆(πf )/π = 2Df . The claim of the theorem follows from Corollary 8.7 p.232 in [EK].

Convergence toward the intrinsic BM starting from the origin

Now we want to obtain a result of convergence toward the intrinsic Brownian motion starting from 0. It happens to be more difficult to prove than Theorem 5.1, since in this case the criteria of Ethier and Kurtz does not apply directly. Indeed a core of the intrinsic BM starting from 0 may contain functions which do not vanish in 0. But for such function f it is not so clear if A N f converges uniformly toward Df on a + . However, since the intrinsic BM takes values in a + for t > 0 (see [ABJ]), the criteria applies for t ≥ η for any η > 0. Then it only remains to obtain a control of what happens in small time. One way for this is to get good estimates of the transition kernel. But, except when r = 2, the only known convenient estimates [AST] concern the simple random walk on buildings of type Ãr . This explains why in the next result we restrict us to this particular case.

We set Y N t := Y N,0 t for all t ≥ 0, and we denote by (I t , t ≥ 0) the intrinsic BM starting from 0.

Theorem 6.1. The sequence (Y N t , t ≥ 0) converges in law in D(R + , a + ) toward (I t , t ≥ 0), when N → +∞.
Proof. The proof is divided into two parts. We first prove the convergence in law at a fixed time (Lemma 6.1 below). With the criteria of Ethier and Kurtz this allows to deduce the convergence in law on [η, +∞) for any η > 0. Then we prove a tightness result, which allows to conclude by general theorems. Lemma 6.1. For all t ≥ 0, Y N t converges in law toward I t , when N → ∞.

Proof. Let f = 1 K be the indicator function of a compact K ⊂ a + , and let q n (O, •) be the transition kernel of (Y n , n ≥ 0). Then

E[f (Y N t )] = λ∈P + q [N t] (O, λ)N λ f ( λ √ N ) = 1 N r 2 u∈ P + √ N ∩K N r 2 q [N t] (O, √ N u)N √ Nu .
We will show that for all u

∈ P ++ √ N , N r 2 q [N t] (O, √ Nu)N √ N u → const • π(u) 2 t |R + |+ r 2 e -|u| 2 2ct , (10)
when N → ∞. The limit being precisely the density of I t , we will deduce the lemma by a usual argument of integral approximation by series, and Sheffé's lemma. First remember that

q n (O, λ) = p n (O, λ) F 0 (λ) F 0 (0) ρ-n ,
for all λ ∈ P + and all n ≥ 0. Moreover by ( 5) and W 0 -invariance of h, we get

p n (O, λ) = const • ρn q -1 2 t λ U
hn (iθ)e i<λ,θ> dθ c(-iθ) .

Next we make the change of variables θ → θ/ [N t] in the integral. Then as in Lemma 3.1 we use the convergence of h[Nt] (iθ/ [N t]) toward e -1 2 ||θ|| 2 , which is moreover dominated by e -ǫ|θ| 2 for ǫ small enough and |θ| ≤ const • [N t]. Thus we can apply the dominated convergence theorem, and using (3), we get

N r 2 q [N t] (O, √ N u)N √ N u → const • π(u) t |R + | 2 + r 2 e -1 2 ||θ|| 2 +i<θ, u √ t > π(-iθ) dθ,
Then we make the change of variables θ → θ + iu/(c √ t) and we get the limit const • π(u)

t |R + | 2 + r 2 e -|u| 2 2ct e -1 2 ||θ|| 2 π(-iθ + u c √ t ) dθ.
We conclude as follows: observe that the polynomial defined for x ∈ a by r(x) := e -1 2 ||θ|| 2 π(-iθ + x) dθ.

is skew W 0 -invariant, and of degree exactly |R + |. Thus it is equal (up to a constant) to π (see Corollary 3.8 p.362 in [Hel]). This proves (10) and finishes the proof of the Lemma.

The next step is the following tightness result.

Proposition 6.1. Let α > 0 and ǫ > 0. There exists η > 0 such that lim sup

N →∞ P sup t≤η |Y N t | ≥ α ≤ ǫ.
Proof. The set

A := sup k≤[N η] |Y k | > α √ N ,
is equal to the disjoint union:

A = [N η] k=1 A k ,
where

A k = |Y 1 | ≤ α √ N, . . . , |Y k-1 | ≤ α √ N , |Y k | > α √ N .
For ǫ ∈ (0, 1), k ≤ [N η], K > 0 and η ∈ (0, 1) such that α/ √ η > K, set

B k = |Y [N η]-k | ≤ ( α √ η -K) N η , and
D ǫ,k = ∀i ∈ {([N 1-ǫ ] -k) + , ([2N 1-ǫ ] -k) + , . . . , (N -k) + }, Π(Y i ) ≥ N (|R + |-ǫ)/2 ,
where u + = u ∨ 0 for any u ∈ R, and

Π(λ) := α∈R + (1+ < α, λ >) ∀λ ∈ P + . Set also N ǫ := [N 1-ǫ/2|R + | ],
and

D ǫ = ∀i ∈ {[N 1-ǫ ], [2N 1-ǫ ], . . . , N } ∩ [N ǫ , +∞), Π(Y i ) ≥ N (|R + |-ǫ)/2 .
Note first that for any ǫ ∈ (0, 1),

P[A] ≤ P[B c 0 ∪ D c ǫ ] + Nǫ k=1 P[A k ] + [N η] k=Nǫ+1 P[A k ∩ B 0 ∩ D ǫ ].
Then Markov property implies that for all k ≥ N ǫ

P[A k ∩ B 0 ∩ D ǫ ] ≤ E {1 A k P Y k [B k ∩ D ǫ,k ]} ,
where for any x, P x denotes the law of Y starting from x. So

P[A] ≤ P[B c 0 ∪ D c ǫ ] + Nǫ k=1 P[A k ] + P[A] × sup k,x P x [B k ∩ D ǫ,k ] , (11)
where the sup is over integers k ∈ (N ǫ , [N η]) and vertices x such that |x| = [α √ N ]+ 1. Now we need the following lemma: Lemma 6.2. For ǫ small enough, lim sup

N →+∞ sup k,x P x [B k ∩ D ǫ,k ] < 1, where the sup is over integers k ≤ [N η] and x's such that |x| = [α √ N ] + 1.
Proof. Let x be such that |x| = [α √ N ] + 1. We first claim that the probability of the event {Y travel a distance larger than α √ N /2 in less than N 1-ǫ steps} decays exponentially fast to 0 when N → +∞.

(12) This is due to the Gaussian factor in the transition kernel of Y . More precisely estimates from [AST] show that for any λ ∈ P + , any y ∈ V λ (x) and any l ≥ 1,

q l (x, y) ≤ C F 0 (y)F 0 (λ) F 0 (x)l |R + |+r/2 e -c|λ| 2 /l . (13)
On the other hand for any µ ∈ P + , we have

|V λ (x) ∩ V µ (0)| ≤ CF 0 (x)q 1/2 t λ q 1/2 tµ . (14)
This follows from [START_REF] Parkinson | Spherical harmonic analysis on affine buildings[END_REF] Formula (1.7) and Lemma 6.1. Then the estimate (2) of F 0 , (13) and ( 14) prove our claim (12). Now on D ǫ,k we know that Y (starting from x) will enter the set

E ǫ,N := {Π(λ) ≥ N (|R + |-ǫ)/2 } before time N 1-ǫ
. So if we denote by x ′ the position of Y at his first entrance in this set, we can assume by ( 12) that |x ′ | ≥ α √ N /2. By using next the Markov property, it is enough to prove the lemma with x ′ in place of x. Actually in the following, for notation convenience, we will assume that x already lies in the set E ǫ,N .

Then let T ∂a+ be the first time the (radial part of) the random walk reaches ∂a + . We claim that for ǫ small enough and N large enough,

P x B k ∩ D ǫ,k ∩ {T ∂a+ ≤ [N η] -k} ≤ 1 4 ∀k ≤ [N η]. (15)
To see this we need to describe the behavior of Y on P ++ . Denote by q(•, •) its one-step transition kernel, and remember that p(•, •) denotes the one of the radial part of the simple random walk on X . First by definition

q(λ, µ) = F 0 (µ) F 0 (λ) ρ-1 p(λ, µ),
for all λ ∈ P ++ and µ ∈ P + such that |λ -µ| = 1. Denote by c 0 the inverse of the number of neighbors (in P + ) of any weight λ ∈ P ++ . By using the explicit formula (9) of p(λ, µ), we see that

q(λ, µ) = c 0 F 0 (µ)q 1/2 tµ F 0 (λ)q 1/2 t λ . (16)
Let now y ∈ X be such that y ∈ E ǫ,N and |y| ≤ N (1+ǫ/|R + |)/2 . If λ = y, then by ( 16) we get

P y T ∂a+ ≤ N 1-ǫ = F 0 (µ)q 1/2 tµ F 0 (λ)q 1/2 t λ c l 0 , (17)
where the sum is over all l ≤ N 1-ǫ and all paths (λ = λ 1 , . . . , λ l = µ) in P + of length l, going from λ to some µ ∈ ∂a + ∩ P + . But if µ ∈ ∂a + ∩ P + , then at least one positive root vanishes in µ. If moreover µ is at distance at N 1-ǫ from λ = y, then |µ| ≤ C|λ| and thus Π(µ) ≤ CN (|R + |+ǫ-1)/2 . So in (17) the ration F 0 (µ)q 1/2 tµ /F 0 (λ)q 1/2 t λ is always bounded by CN ǫ-1/2 . This shows that

P y T ∂a+ ≤ N 1-ǫ ≤ CN ǫ-1/2 P (T ∂a+ ≤ N 1-ǫ ) ≤ CN ǫ-1/2 , ( 18
)
where P denotes the law of the simple random walk on P + (say reflected on ∂a + ). On the other hand, thanks again to the Gaussian factor in (13), we know that (except on an event of probability decaying exponentially fast to 0 when N → +∞) for all i ∈ {([N 1-ǫ ]-k) + , ([2N 1-ǫ ]-k) + , . . . , (N -k) + }, |Y i | ≤ N (1+ǫ/|R + |)/2 . Thus (18), applied (at most) [ηN ǫ ] times, proves our claim (15), if ǫ is small enough (e.g. ǫ < 1/4).

Consider now |µ| ≤ |x|, and some path f = (x = λ 1 , . . . , λ l = µ) going from x to µ and not intersecting ∂a + . Set α 0 := α 1 + • • • + α r , and let H x be the affine hyperplane containing x and orthogonal to α 0 . Call f ′ the path obtained by reflecting orthogonally the last excursion of f out of H x on the other side of H x . Then f ′ does not intersect ∂a + and the map f → f ′ is one to one. Moreover under P , f and f ′ have the same probability. Thus by using again ( 16) and (3), we see that the probability (for Y ) to arrive at some time t below level |x|/2 without touching ∂a + is at most 1/2 + o(1), where o(1) tends to 0 when N → +∞. Thus for N large enough,

P x B k ∩ D ǫ,k ∩ {T ∂a+ ≥ [N η] -k} ≤ 2 3 ∀k ≤ [N η].
This concludes the proof of the lemma.

We can finish now the proof of Proposition 6.1. Coming back to (11) and applying the previous lemma, we see that for ǫ small enough and N large enough, But the cardinality of a sphere of radius λ is of order q t λ . So estimate (13) with x = O (and y = λ) shows that the right hand term in the above inequality tends to 0 when K and N tend to +∞. This finishes the proof of the proposition.

Theorem 6.1 is now a consequence of standard theorems (see for instance [Bil] or Theorem 7.2 p.128 in [EK]).

Remark 6.1. As mentioned previously, when r = 2 the estimates in [AST] hold for all symmetric nearest neighbor random walks. So slight modifications of the previous proof show that Theorem 6.1 extend to all these random walks when r = 2.

This paper is part of my Ph.D. thesis. I warmly thank my advisors Jean-Philippe Anker and Philippe Bougerol for their suggestion of studying this problem, and Philippe Bougerol for having drawn my attention to a mistake in the proof of Proposition 6.1 in a previous version of this paper.