Sophie Pinchinat
email: sophie.pinchinat@irisa.fr

Olivier Serre
email: olivier.serre@liafa.univ-paris-diderot.fr

Emptiness Of Alternating Parity Tree Automata Using Games With Imperfect Information

Keywords: Alternating Tree Automata, Emptiness, Imperfect Information Games, Positional Determinacy Automates d'arbres alternants, test du vide, jeux à information imparfaite, déterminaison positionnelle

We focus on the emptiness problem for alternating parity tree automata. The usual technique to tackle this problem first removes alternation, going to non-determinism, and then checks emptiness by reduction to a two-player perfect-information parity game. In this note, we give an alternative roadmap to this problem by providing a direct reduction to the emptiness problem to solving an imperfect-information two-player parity game.

Introduction

Tree automata [START_REF] Thomas | Languages, automata, and logic[END_REF][START_REF] Flum | Logic and Automata: History and Perspectives[END_REF] are a powerful tool to handle sets of infinite trees which are widely needed in verification, since they provide a natural representation of branching-time system executions. It is well known that by equipping tree automata with the parity condition, one captures all ω-regular tree languages [START_REF] Grädel | Automata, Logics, and Infinite Games: A Guide to Current Research[END_REF]. Additionally, tree automata may employ alternation [START_REF] Chandra | [END_REF], which makes their complementation an extremely simple task. In particular, combining alternation with the parity condition yields the automata-theoretic counterpart of the propositional µ-calculus, where the translation from one to the other can be done in linear time [START_REF] Arnold | Rudiments of µ-calculus[END_REF][START_REF] Grädel | Automata, Logics, and Infinite Games: A Guide to Current Research[END_REF]. Hence, the model-checking and the satisfiability/validity of logical formulas amount to respectively verify membership and non-emptyness/universality on their corresponding tree automata.

The membership problem for alternating tree automata has a fairly simple algorithm: one compiles the input tree and the automaton into a polyomial size perfect information parity game and solves it. On the contrary, the usual roadmap to check emptiness of an alternating tree automaton is more involved. First one builds an equivalent non-deterministic automaton thanks to the Simulation Theorem [START_REF] Muller | Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra[END_REF], and then one checks emptiness of this latter automaton by solving an associated two-player perfect information game.

The contribution of this note is to propose a decision procedure for emptiness of alternating parity tree automata that goes directly to solve a two-player game, but with imperfect information. The proposed construction extends the notion of blindfold games given by Reif in his seminal paper [START_REF] Reif | Universal games of incomplete information[END_REF] used to check universality of non-deterministic automata on finite words (a similar idea was later considered in [START_REF] Wulf | Antichains: A new algorithm for checking universality of finite automata[END_REF]).

This reduction of the non-emptiness of alternating parity automata to imperfect information games does not lead to a gain in complexity, due to intrinsic hardness. Nevertheless, we believe that its simplicity is of interest, and we also think that this approach generalizes to other classes of automata on infinite objects, as recently demonstrated for probabilistic qualitative tree languages [START_REF] Carayol | Qualitative tree languages[END_REF].

Definitions

Let X be a (possibly infinite) alphabet. Then we denote by X * (resp. X ω ) the set of finite (resp. infinite) words over X. We let ε be the empty word.

Let Σ be a finite alphabet. An infinite Σ-labelled binary tree (or simply a tree when Σ is clear from the context) is a map t : {0, 1} * → Σ. In this setting, we shall refer to an element n ∈ {0, 1} * as a node and to ε as the root. For a node n, we call t(n) the label of n in t. A language of infinite Σ-labelled binary trees is a set of infinite Σ-labelled binary trees.

Two-Player Perfect Information Games

A graph is a pair G = (V, E) where V is a set of vertices and E ⊆ V × V is a set of edges. The size of a graph is defined to be |V | + |E|. A dead-end is a vertex v such that there is no vertex v with (v, v ) ∈ E; in the rest of the paper, we only consider graphs that have no dead-end, hence this is implicit from now on.

An arena is a triple G = (G, V E , V A ) where G = (V, E) is a graph and V = V E V A is a partition of the vertices among two players, Éloïse and Abelard. A colouring function ρ is a mapping ρ : V → Col ⊂ N where Col is a finite set of colours. An infinite two-player parity game on an arena G is a triple G = (G, ρ, v 0 ) where v 0 ∈ V is some initial vertex.

Éloïse and Abelard play in G by moving a pebble along edges. A play starts from the initial vertex v 0 and proceeds as follows: the player owning v 0 (i.e. Éloïse if v 0 ∈ V E , Abelard otherwise) moves the pebble to a vertex v 1 such that (v 0 , v 1 ) ∈ E. Then the player owning v 1 chooses a successor v 2 and so on. As we assumed that there is no dead-end, a play is an infinite word

v 0 v 1 v 2 • • • ∈ V ω
and it is won by Éloïse just in case lim inf(ρ(v i )) i≥0 is even. A partial play is a prefix of a play.

A strategy for Éloïse is a function assigning, to every partial play ending in some vertex

v ∈ V E , a vertex v such that (v, v ) ∈ E. Éloïse respects a strategy ϕ during a play v 0 v 1 v 2 • • • if v i+1 = ϕ(v 0 • • • v i ), for all i ≥ 0 such that v i ∈ V E .
A strategy ϕ for Éloïse is winning if Éloïse wins every play where she respects ϕ.

Of special interest are strategies that do not require memory. A positional strategy is a strategy ϕ such that for any two partial plays of the form λ.v and λ .v, one has ϕ(λ • v) = ϕ(λ • v), i.e. ϕ only depends on the current vertex. It is a well known result that positional strategies suffice to win in parity games [START_REF] Zielonka | Infinite games on finitely coloured graphs with applications to automata on infinite trees[END_REF].

Theorem 1 (Positional determinacy). Let G be a parity game. Then for any vertex, either Éloïse or Abelard has a positional winning strategy.

Hence, we now only consider positional strategies and we represent such a strategy as functions from V E (or V A depending on the player) into V .

Collection des Publications Internes de l'Irisa c IRISA

Alternating Parity Tree Automata

An alternating parity tree automaton is a tuple

A = Q ∃ , Q ∀ , Σ, ∆, q in , ρ , where Q ∃ is a set of existential states and Q ∀ is a set of universal states such that Q ∃ and Q ∀ are disjoint (we let Q = Q ∃ Q ∀ ), q in ∈ Q is an initial state, Σ is a labelling alphabet, ∆ ⊆ Q × Σ × Q × Q is a transition relation and ρ : Q → N is a colouring function.
In the following, we use alternating parity tree automata as acceptors for tree languages, and we define acceptance by means of a parity game. Let A = Q ∃ , Q ∀ , Σ, ∆, q in , ρ be an alternating parity tree automaton, and let t be a Σ-labelled tree. From A and t, we define a two-player perfect information parity game G A,t .

Intuitively, a play in G A,t consists in moving a pebble along a branch of t in a top-down manner: the pebble is attached to a state and in some node n with state q Éloïse (if q ∈ Q ∃ ) or Abelard (if q ∈ Q ∀ ) picks a transition (q, t(n), q 0 , q 1 ) ∈ ∆, and then Abelard chooses to move down the pebble either to n • 0 (and update the state to q 0 ) or to n • 1 (and update the state to q 1 ).

More formally, G A,t = (G A,t , ρ A,t , (ε, q in )) where:

• The arena G A,t is (G = (V E ∪ V A , E), V E , V A
) is defined by:

-

V E = {(n, q) | n ∈ {0, 1} * and q ∈ Q ∃ }.
Vertices controlled by Éloïse are pairs made of a node together with a control state in Q ∃ .

-

V A = {(n, q) | n ∈ {0, 1} * and q ∈ Q ∀ } ∪ {(n, q, q 0 , q 1 ) | n ∈ {0, 1}
* and (q, t(n), q 0 , q 1 ) ∈ ∆}. Vertices controlled by Abelard are pairs made of a node together with a control state in Q ∃ as well as tuples consisting of a node and three states consistent with the transition relation of A.

-The set of edges E is equal to {((n, q), (n, q, q 0 , q 1 )) | (n, q, q 0 , q 1 ) ∈ V )} ∪ {((n, q, q 0 , q 1 ), (n • x, q x )) | x ∈ {0, 1} and (n, q, q 0 , q 1 ) ∈ V )}.

• The colouring function mimics the one of the automaton A: ρ A,t ((n, q)) = ρ A,t ((n, q, q 0 , q 1 )) = ρ(q).

Note that this game is not symmetric as it is always Abelard who is in charge of choosing the direction.

A tree t is accepted by A if and only if Éloïse has a winning strategy in the game G A,t ; if not the tree is rejected. Finally, we define the set L(A) as those trees accepted by A.

The emptiness problem for A consists in deciding whether L(A) = ∅.

Remark 1. There are several definitions of alternating tree automata, and another popular one is by not distinguishing between existential and universal states but replacing the transition relation by a map δ :

Q × Σ → B + (Q × {0, 1}
) where B + (X) denotes the positive Boolean formulas over X (see e.g. [START_REF] Kupferman | An automata-theoretic approach to branching-time model checking[END_REF]). Our model is easily seen to be equi-expressive with that one.

Remark 2. A positional strategy for Éloïse in G A,t can be described as a function ϕ : {0, 1} * × Q ∃ → Q × Q that satisfies the following property: ∀n ∈ {0, 1} * , if ϕ(n, q) = (q 0 , q 1 ) then (q, t(n), q 0 , q 1 ) ∈ ∆. Equivalently, if one let T be the set of functions from Q ∃ into Q × Q, a positional strategy can be described as a T -labelled binary tree.

A non-deterministic parity tree automaton is an alternating automaton in which all states are existential. In this setting it is well-known how to define a two-player perfect information parity game in which Éloïse wins iff the language of the automaton is non-empty (see e.g. [START_REF] Grädel | Automata, Logics, and Infinite Games: A Guide to Current Research[END_REF][START_REF] Apt | Lectures in Game Theory for Computer Scientists[END_REF]). Note that this game is of polynomial size in the number of states of the automaton and uses the same set of colours.

It is a well-known (but technically involved) result that alternating and non-deterministic automata are equi-expressive [START_REF] Muller | Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra[END_REF].

Theorem 2 (Simulation Theorem). Let A be an alternating parity tree automaton with n states and using k colours. Then one can effectively construct a non-deterministic parity tree automaton B such that L(A) = L(B). The automaton B has 2 O(nk log(nk)) and it uses O(nk) colours.

Hence, the usual roadmap to check emptiness of an alternating tree automaton is as follows. First one builds an equivalent non-deterministic automaton thanks to Theorem 2, and then one checks emptiness of this latter automaton by solving the associated emptiness game.

Imperfect Information Games

In the following we introduce a quite restrictive class of games with imperfect information [START_REF] Chatterjee | Algorithms for omega-regular games with imperfect information[END_REF][START_REF] Apt | Lectures in Game Theory for Computer Scientists[END_REF].

A game structure (of imperfect information) is a tuple G = S, s in , A, T, ∼ where S is a finite set of states, s in ∈ S is an initial state, A is a finite alphabet of actions, T ⊆ S × A × S is a transition relation and ∼ is an equivalence relation over S. We additionally require that for all (s, a) ∈ S × A there is at least one s ∈ S such that (s, a, s ) ∈ T . An imperfect information game is a pair G = G, ρ where G is a game structure with set of states S and ρ : S → N is a colouring function.

A play starts from the initial state s 0 = s in and proceeds as follows: Éloïse plays an action a ∈ A and then Abelard resolves the nondeterminism by choosing a state s 1 such that (s 0 , a, s 1 ) ∈ T . Then Éloïse plays a new action, Abelard resolves the nondeterminism and so on forever. Hence a play is an infinite word s 0 a 0 s 1 a 1 s 2 a 2 • • • ∈ (S × A) ω and it is won by Éloïse just in case lim inf(ρ(s i )) i≥0 is even. A partial play is a prefix of a play.

Imperfect information is important when defining strategies for Éloïse. Intuitively, she should not play differently in two indistinguishable plays, where the indistinguishability of Éloïse is based on perfect recall [START_REF] Fagin | Reasoning about Knowledge[END_REF], that is: Éloïse cannot distinguish two plays s 0 a 0 s 1 a 1 • • • s and s 0 a 0 s 1 a 1 • • • s with s i ∼ s i for all 0 ≤ i ≤ and a i = a i for all 0 ≤ i < . Hence, a strategy for Éloïse is a function ϕ : (S /∼ × A) * • (S /∼ ) → A assigning an action to every set of indistinguishable plays (here S /∼ denotes the set of equivalence classes of ∼ in S, and for every s ∈ S, we shall write [s] ∼ for its ∼-equivalence class). Éloïse respects a strategy ϕ during a play λ = s 0 a 0 s

1 a 1 s 2 a 2 • • • if a i+1 = ϕ([s 0 ] ∼ a 0 • • • [s i ] ∼ )
, for all i ≥ 0. A strategy ϕ for Éloïse is winning if Éloïse wins every play where she respects ϕ.

Remark 3. Our model of imperfect information games belongs to a restrictive class compared to general ones as developed in [START_REF] Gripon | Qualitative concurrent stochastic games with imperfect information[END_REF][START_REF] Bertrand | Qualitative determinacy and decidability of stochastic games with signals[END_REF]. Indeed, Abelard is perfectly informed, and there is no stochastic transitions; moreover we only consider sure winning and non-randomized strategies (which is actually not a restriction for sure winning). However, our model turns out to be expressive enough for our purpose.

Remark 4. It is important to note that Éloïse may not observe the colour of the current state in general, as we do not require that s ∼ s ⇒ ρ(s) = ρ(s ). In particular, this has to be taken into account when eventually solving the game.

An Emptiness Game For Alternating Parity Tree Automata

For the rest of this section, we fix an alternating parity tree automaton A = Q ∃ , Q ∀ , Σ, ∆, q in , ρ . We define a game structure of imperfect information G A that intuitively works as follows. Éloïse describes both a tree t and a positional strategy ϕ for her in the game G A,t ; the strategy ϕ is described as a T -labeled tree (where T is the set of functions from

Q ∃ into Q × Q, see Remark 2).
As the plays are of ω-length, she actually does not fully describe t and ϕ but only a branch: this branch is chosen by Abelard, who also takes care of computing the sequence of states along it (either by updating an existential state accordingly to ϕ or, when the state is universal, by choosing an arbitrary valid transition of the automaton). In this game, Éloïse observes the directions, but not the actual control state of the automaton.

Formally, we let G A = S, s in , A, T, ∼ where S = (Q × {0, 1}) ∪ {(q in , ε)} and s in = (q in , ε); A ⊆ Σ × T is the set of pairs (a, τ ) such that for all q ∈ Q ∃ we have that (q, a, q 0 , q 1 ) ∈ ∆ where τ (q) = (q 0 , q 1 ) (recall that T is the set of functions from Q ∃ into Q × Q); T = {((q, i), (a, τ ), (q 0 , 0)), ((q, i), (a, τ ), (q 1 , 1)) | q ∈ Q ∃ and τ (q) = (q 0 , q 1 )} ∪ {((q, i), (a, τ ), (q 0 , 0)), ((q, i), (a, τ ), (q 1 , 1)) | q ∈ Q ∀ and (q, a, q 0 , q 1 ) ∈ ∆} and (q, i) ∼ (q , i) for all q, q ∈ Q and i ∈ {0, 1}.

Finally we let G A = G A , ρ A be the parity game obtained by letting ρ A (q, i) = ρ(q) for any (q, i) ∈ S.

We then have the following result.

Theorem 3. Éloïse has a winning strategy in G

A iff L(A) = ∅.
Proof. Due to how ∼ is defined, a strategy for Éloïse in G A can also be viewed as a map ϕ : {0, 1} * → A. As A ⊆ Σ × T , one can see ϕ as a pair (t, ϕ t ) where t is an infinite Σ-labelled binary tree, and ϕ t is a strategy for Éloïse in the acceptance game G A,t of t by A. Now, once such a strategy ϕ is fixed, the set of plays in G A where Éloïse respects ϕ is in one-to-one correspondence with the set of plays in G A,t where she respects ϕ t , and this correspondence preserves the property of being winning. Therefore, ϕ = (t, ϕ t ) is winning iff ϕ t is a winning strategy in G A,t iff t ∈ L(A). Therefore, Éloïse has a winning strategy iff there exists some tree t ∈ L(A).

Remark 5. From the proof of Theorem 3, one can also conclude that if L(A) = ∅ then L(A) contains a regular tree (i.e. the unfolding of a finite graph). Indeed, this is a direct consequence of the fact that if Éloïse has a winning strategy in G A , then she has one that uses finite memory [START_REF] Chatterjee | Algorithms for omega-regular games with imperfect information[END_REF].

Collection des Publications Internes de l'Irisa c IRISA Theorem 3 provides a reduction of the emptiness problem to deciding the existence of a winning strategy in a game with imperfect information. We prove a converse result. Theorem 4. Let G be an imperfect information game. Then one can construct an alternating parity tree automaton A G such that Éloïse has a winning strategy in G iff L(A G ) = ∅. Moreover in A G all states are universal.

Proof. Let G = S, s in , A, T, ∼ be the underlying game structure of G = G, ρ and let C 1 , • • • , C k be the equivalence classes of ∼. We design an alternating automaton A G = Q ∃ = ∅, Q ∀ = S ∪ { }, A, ∆, s in , ρ , working on infinite A-labelled trees of arity k, that are maps t : {1, . . . , k} * → A. The only difference with the definition of Section 2.2 when considering automata handling such trees is that the transition relation ∆ is a subset of Q × A × Q k . We let ρ ( ) = 0 and ρ (s) = ρ(s) for all s ∈ S and ∆ = {(s, a, s 1 , . . . , s k ) | ∀1 ≤ i ≤ k, (s i ∈ C i and (s, a, s i ) ∈ T ) or s i = }} ∪ {( , a, , . . . , ) | a ∈ A} Note that A-labelled trees of arity k are trivially in bijection with strategies of Éloïse in G. Indeed with a tree t of arity k we associate a strategy ϕ t by letting ϕ

t (C j0 a 0 • • • C ji ) = t(j 0 • • • j i ).
Then it is rather immediate to check that the set of plays where Éloïse respects ϕ t in G is isomorphic to the set of plays in the acceptance game G A G ,t (note that in this game all vertices are controlled by Abelard as all states in A G are universal); moreover winning plays are preserved. By noting that one can always encode trees of arity k into binary trees (and modify A accordingly) one concludes the proof.

Conclusion

In this note we presented a method for checking emptiness of alternating parity tree automata that does not rely on the Simulation Theorem [START_REF] Muller | Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra[END_REF]. It is however important to stress that the two ingredients in the proof of the Simulation Theorem did not vanish: we make crucial use of positional determinacy of games in our reduction, and determinization of automata on infinite word is implicitly needed when solving the imperfect information games. Indeed, since Éloïse does not observe the colour, one has to use a standard trick that consists in embedding in the subset construction of [START_REF] Chatterjee | Algorithms for omega-regular games with imperfect information[END_REF] a deterministic parity word automaton that checks that all plays consistent with the observations fit the parity condition; this requires to determinize a non-deterministic Büchi word automaton. Somehow, our construction helps separating the two techniques.

We also think that going to imperfect information games may lead to efficient implementation for emptiness checking, as many proper techniques (e.g. antichains) have recently been developed to deal with those games [START_REF] Berwanger | Alpaga: A tool for solving parity games with imperfect information[END_REF][START_REF] Berwanger | Strategy construction for parity games with imperfect information[END_REF].

Collection des Publications Internes de l'Irisa c IRISA


On the discriminating power of tests in resource λ-calculus

Since its discovery, differential linear logic (DLL) inspired numerous domains. In denotational semantics, categorical models of DLL are now commune, and the simplest one is Rel, the category of sets and relations. In proof theory this naturally gave birth to differential proof nets that are full and complete for DLL. In turn, these tools can naturally be translated to their intuitionistic counterpart. By taking the co-Kleisly category associated to the ! comonad, Rel becomes MRel, a model of the λ-calculus that contains a notion of differentiation. Proof nets can be used naturally to extend the λ-calculus into the lambda calculus with resources, a calculus that contains notions of linearity and differentiations. Of course MRel is a model of the λ-calculus with resources, and it has been proved adequate, but is it fully abstract?

 for which M∞ is fully abstract, the tests.

Introduction

The first extension of the λ-calculus with resources, by Boudol in 1993 [START_REF] Boudol | The lambda-calculus with multiplicities[END_REF], was introducing a special resource sensitive application that may involve multisets of affine arguments (each one has to be used at most one time). This was a natural way to export resource sensitiveness to the functional setting. However, gathering no known and interesting properties (confluence, linearity...), it was not fully explored.

Later on, Ehrhard and Regnier, working on functional interpretation of differential proof nets, discovered a calculus similar to Boudol's one, named differential λ-calculus [START_REF] Ehrhard | The differential lambdacalculus[END_REF]. By adding to the λ-calculus a derivative operation ∂M x (N ), which syntactically corresponds to a linear substitution of x by N in M , it recovers the resource-sensitiveness. This is done through the translation (λx.M ) [N 1 , ..., N n ; N ! ] ≃ (λx. ∂ (n) M

x (N 1 ,..., N n )) N where N i are the linear arguments and N is the non linear one. This more semantical view even allow for the generalisation of the operation and recover excellent semantical properties (confluence, Taylor expansion...). We will adopt the syntax of [START_REF] Pagani | Parallel reduction in resource lambdacalculus[END_REF] that re-implements improvements from differential λ-calculus into Boudol's calculus, and we will call it ∂λ-calculus.

The category Rel of set and relations is known to model the linear logic, and, despite its high degree of degeneration (Rel op = Rel), it is a very natural construction. Indeed, what appeared to be a degeneration is in reality a natural choice that preserves all proofs, i.e. the interpretation function from proof to MRel is injective up to isomorphism ( [START_REF] De | The relational model is injective for Multiplicative Exponential Linear Logic (without weakenings)[END_REF]). But our principal interest for this category is that it models the differential linear logic, and of known such category it is the simplest and more natural.

As for every categorical model of linear logic, the interpretation of the ! induced a comonad. From that comonad we can construct the co-kleisly category. In the case of Rel, this new category, MRel, corresponds to the category of sets with, as morphisms from A to B, the relations from M f (A) (the finite multisets over A) to B. It is then a model of the λ-calculus and of the ∂λ-calculus. This construction being the most natural we can do, MRel is, a priori, one of the most natural models of the ∂λ-calculus (even if non well pointed [START_REF] Bucciarelli | Not Enough Points Is Enough[END_REF]).

It is only natural, then, to question on the depth of the link among the reflexive elements of MRel and the ∂λ-calculus. And more precisely among MRel's canonical reflexive element M ∞ and the ∂λ-calculus. Until now we knew that M ∞ ( [START_REF] Bucciarelli | Not Enough Points Is Enough[END_REF]) was adequate for the λ-calculus, i.e. that two terms carrying the same interpretations in MRel behave the same way in all contexts. But we did not know anything about the counterpart, named full abstraction.

This question has been thoroughly studied, however, since M ∞ has been proved (resp. in [START_REF] Manzonetto | A general class of models of H ⋆[END_REF], [START_REF] Bucciarelli | Full Abstraction for Resource Lambda Calculus with Tests, throught Taylor expansion[END_REF] and [START_REF] Bucciarelli | Full Abstraction for Resource Calculus with Tests[END_REF]) fully abstract not only for both of the principal sub-calculi of ∂λ-calculus, namely the usual λ-calculus and Kfoury's linear calculus of [START_REF] Kfoury | A linearization of the Lambda-calculus and consequences[END_REF], but also for the extension with tests of [START_REF] Bucciarelli | Full Abstraction for Resource Calculus with Tests[END_REF] (denoted τ ∂λ-calculus). Therefore Bucciarelli et al emit in [START_REF] Bucciarelli | Full Abstraction for Resource Calculus with Tests[END_REF] a strong conjecture of full abstraction for the ∂λ-calculus.

However, and it is our purpose here, a counter example can be found. In order to exhibit this counter example, we will take an unusual shortcut using full abstraction result for τ ∂λ-calculus. Indeed, we will prove a slightly more general theorem: the failure of full abstraction for ∂λ-calculus of any model that is fully abstract for τ ∂λ-calculus. Due to this generalization we will not have to introduce the full description of M ∞ in the core of the article (it is available in annexes).

Additionally to be considerably easier and more intuitive than the direct and usual method, this way of proceeding is part of a larger study of full abstraction. Indeed, we are looking for a mechanical way to tackle full abstraction problems in two steps. First we extend the calculus with well chosen semantical objects in order to reach the definability of compact elements. Then we study the full abstraction question indirectly via the link between the operational equivalence of the original calculus and of its artificial extension. This reduces our mix of semantic and syntactic question to a purely syntactic one, allowing us to use powerful syntactic constructions.

Tests where introduced in [START_REF] Boudol | A semantics for lambda calculi with resources[END_REF] to have a full abstraction theorem for Boudol λ-calculus with resources. Later on, the principle was improved in [START_REF] Bucciarelli | Full Abstraction for Resource Calculus with Tests[END_REF], implementing semantic objects in the syntax in order to get full abstraction of M ∞ , following an idea of [START_REF] Ehrhard | Interpreting a finitary pi-calculus in differential interaction nets[END_REF]. This extension can, in our context, be compared to a basic exception mechanism. The term τ (Q) is raising the exception (or test) Q, absorbing all its non resources-limited applications and the exception τ (M ) is catching any exception in M by annihilating all the head-λ-abstraction. The most important here being the scope of the τ (M ) that act as an infinite application over M . Notations: λx n will be used for λx 1 , ..., x n (n is not specified when it can be any integer) and I will denotes the identity λx.x.

Background

∂λ-calculus

As explained, this article is directly following [START_REF] Bucciarelli | Full Abstraction for Resource Calculus with Tests[END_REF]. For this reason we need to introduce the ∂λ-calculus and then the tests. In the ∂λ-calculus , the notion of linearity is capital. Any term in linear position will never suffer any duplication or erasing regardless the reduction strategy. Linear subterms are subterms that are either the first subterm of a lambda abstraction in linear position, the left side of an application that is in linear position, or in the linear part of its right side. The last case is the real improvement and asks for arguments to be separated in linear and non linear arguments. Therefore, the right side of the applications will be replaced by a new kind of expression different from terms, the "bags". Bags are multisets containing some linear (non banged) arguments and exactly one non linear (banged) argument:

(terms)

M, N ∶ λx.M M B M +N 0 (bags) B, C ∶ [M 1 , ..., M n ; M ! ] B + C 0 This is the syntax of [4] modulo the macro M +N = (λx.x) [{M +N } ! ].
For convenience, the finite sums will be denoted Σ i Q i and the different 0's are just the neutral elements of the different sums. This demonic sum had to be implemented since we want the calculus to be resource sensitive and confluent, thus there is no other choice than to considere the sum of all the possible outcomes. Sums distribute with any linear context:

λx.(Σ i M i ) = Σ i (λ x .M i ) (Σ i M i ) (Σ j N j ) = Σ i,j (M i N j ) ([(Σ i1≤k1 M 1 i1 ), ..., (Σ in≤kn M n in ); M ! ]) = Σ (ij )j ≤(kj )j [M i i1 , ..., M n in ; M ! ]
In the application, each linear argument will replace one and only one occurrence of the variable, thus the need of two kinds of substitutions, the usual one, denoted {.}, and the linear one, denoted ⟨.⟩. This last will act like a derivation M ⟨N x⟩ ∼ ∂M ∂x (N ):

x⟨N x⟩ = N x⟨N y⟩ = 0 (λy.M )⟨N x⟩ = λy.(M ⟨N x⟩) ([M 1 , ..., M n ; M ! ])⟨N x⟩ = (Σ n i=1 [M 1 , .., M i ⟨N x⟩, ...M n ; M ! ]) + [M 1 , ..., M n , M ⟨N x⟩; M ! ] (M P )⟨N x⟩ = (M ⟨N x⟩ P ) + (M P ⟨N x⟩)
This enables us to describe the β-reduction:

(β) (λx.M )[N 1 , ..., N n ; N ! ] → M ⟨N 1 x⟩⋯⟨N n x⟩{N ! x}
In other words

(λx.M )[N 1 , ..., N n ; N ! ] → ∂ n M ∂ n x (N 1 , ..., N n )(N )

τ∂λ-calculus

In differential proof nets the 0-ary tensor and the 0-ary par can be added freely in the sense that we still have a natural interpretation in MRel and M ∞ . These operations can be translated in our calculus as an exception mechanism. With on one side a τ (Q) that "raises" the exception (or test) Q by burning its applicative context (whenever these applications do not have any linear component, otherwise it diverges). And with on the other side a τ (M ) that "catch" the exceptions in M by burning the abstraction context of M (whenever this abstraction is dummy). The main difference with a usual exception system is the divergence of the catch if no exception are raised. We introduce a new operators and a new kind of expression that will play the role of exception, the tests:

(terms) M, N ∶ τ (Q) (test) Q, R ∶ ǫ Q R τ (M ) Q+R 0
New operator immediately imply new distribution rules for the sum and the linear substitution:

τ (Σ i M i ) = Σ i τ (M i ) τ (Σ i Q i ) = Σ i τ (Q i ) j Σ i Q i(j) = Σ i j Q i(j) τ (M )⟨N x⟩ = τ (M ⟨N x⟩) τ (Q)⟨N x⟩ = τ (Q⟨N x⟩) (Q+R)⟨N x⟩ = Q⟨N x⟩+R⟨N x⟩ (Q R)⟨N x⟩ = Q⟨N x⟩ R⟨N x⟩
Here is the corresponding operational semantics:

(γ) τ [τ (Q)] → Q (τ ) τ (λx.M ) → τ (M {0 x}) (τ 1 ) (τ (Q)) [M ! ] → τ (Q) (τ 2 ) (τ (Q)) [M 1 , ..., M n≥1 ; M ! ] → 0 (ǫ) ǫ ǫ → ǫ
The intuition of τ (Q) is an operator that take a test (a Boolean value), compute it and returns an infinite λ-abstraction with no occurrence of the abstracted variables. The test τ (M ) is taking a term and returns a successful test if the term is converging in a context that consists of an infinite empty application.

Observational order and full abstraction

In order to ask for full abstraction, one has to specify a reduction strategy. A natural choice would be the head reduction, but this would make (λx.x [0, 0]) a normal form while no applicative instantiation of x allow the convergence of this term. Therefore, the reduction strategy we are considering will not be headreduction, but the outer-head-reduction. This reduction will reduce subterms in linear position after the subterms in head positions ( [START_REF] Pagani | Linearity, Nondeterminism and Solvability[END_REF]). The corresponding normal forms are terms and tests of the form:

M + λx.y [N 1,1 , ..., N 1,k1 ; L ! 1 ] ⋯ [N n,1 , ..., N n,kn ; L ! n ] M + λx.τ (Q) Q + ( τ (N i ))
Where every N and Q must be in outer-head normal forms and can't be a sum (but the L i are of any kind).

Definition 1 M is observationally below N , if for all context C . , we have C N which is outer-head-converging whenever C M is outer-head-converging. They are observationally equivalent if moreover N is observationally below M In the particular case of the τ∂λ-calculus , we can easily restrict contexts to test-contexts, which is contexts whose output is a tests. This will be applied systematically for simplification. We will denote ≤ τ ∂ and ≡ τ ∂ the observational order and equivalence of the τ∂λcalculus and ≤ ∂ and ≡ ∂ those of the ∂λ-calculus .

Bucciarelli, Carraro, Ehrhard and Manzonetto were then able to prove a strong theorem relating the model to the calculus: Theorem 1 M ∞ is fully abstract for the Λ-calculus with resources and tests: for all closed terms M, N with resources ans tests,

M = N ⇔ M ≡ τ ∂ N

The counter-example

In order to exhibit our counter-example we will use the following property: Fact 1 Let B a calculus and A a super-calculus. Let M a model that is fully abstract for A. M is fully abstract for B iff the operational equivalences of B and A are equal on their domain intersection.

In our context it means that, in order to prove the non full abstraction for the ∂λ-calculus , it is sufficient to find two terms of the ∂λ-calculus that cannot be separated by any context of the ∂λ-calculus but that are separated by a context of the τ∂λ-calculus . This makes the research and the proof quite easier when the terms of the ∂λ-calculus involved are complex but not the context of the τ∂λ-calculus .

We are firstly exhibiting a term A of the ∂λ-calculus that is observationally above the identity in the ∂λ-calculus ', but not in the τ∂λ-calculus 's observational order:

A = Θ [λuvw.w [I [v ! ]] , (λuvw.u [(v [w ! ]) ! ]) ! ]
(1) where Θ is the Turing fix point combinator:

(λgu.u[(g [(g [u ! ]) ! ]) ! ]) [(λgu.u[(g [(g [u ! ]) ! ]) ! ]
) ! ] This term seems quite complex, but, modulo η-equivalence, A reduces exactly to any of the elements of the following sum, and thus can be think as an equivalent:

Σ n≥1 B n = Σ n≥1 λū n w.w [I [u ! 1 ] [u ! 2 ] ⋯ [u ! n ]]
(2) This is due to the following property:

Lemma 1 If A i = λx i+1 .A (x 1 [x ! 2 ] ⋯ [x ! i+1 ]) then A 0 → η A and for all i, A i → A i+1 + B i+1
Proof. Simple reduction unfolding the Θ once. ◻

In absence of tests, this term has a comportment similar to ǫ 0 in the sense that it will converges in any applicative context provided that these applications do not carry linear components. In particular it converges more often than the identity: ◻

But in presence of real tests, its comportment appeared to be different that ǫ 0 in the sense that it diverges under a τ . In particular it is not observationally above the identity in τ∂λ-calculus :

Lemma 3 In the τ∂λ-calculus , τ (A [ǫ ! 0 ]) diverges, while τ (I [ǫ ! 0 ]) converges, i.e. I ≤ τ ∂ A Proof. For all i, τ (A i [ǫ ! 0 ]) diverges since, by co-induction: τ (A i [ǫ 0 ]) → τ ((A i+1 + (λx i+1 y.y [I [x ! 1 ] ⋯ [x ! i+1 ]])) [ǫ 0 ]) = τ (A i+1 [ǫ 0 ]) + τ ((λx i+1 y.y [I [x ! 1 ] ⋯ [x ! i+1 ]]) [ǫ 0 ]) → τ (A i+1 [ǫ 0 ]) + τ (λx i y.y [ǫ 0 [x ! 1 ] ⋯ [x ! i+1 ]]) → * τ (A i+1 [ǫ 0 ]) + τ (0 [ǫ 0 [0 ! ] ⋯ [0 ! ]])
The non outer-head convergence comes with the co-induction hypothesis for the first term, and is trivial for the second.

◻ Hence, we have broken the conjecture concerning the equality between the observational and denotational orders. Let's break the whole conjecture:

Theorem 2 M ∞ is not fully abstract for the λ-calculus with resources 4 Further works First a diligent reader will remark that we have a critical use of the demonic sum which is very powerful in this calculus. And an even more diligent one will remark that an arbitrary choice have been made concerning this sum: we could differentiate terms and reduced of terms and remove sums from the original syntax (they just have to appear in reductions of terms). The choice we made here corresponds to the one of [START_REF] Bucciarelli | Full Abstraction for Resource Calculus with Tests[END_REF] and carries an understandable counter-example. But we claim that another equivalent counter-example arises for the case with limited sum. This counter-example is, however, a little more complicated and make it necessary to rework the material of [START_REF] Bucciarelli | Full Abstraction for Resource Calculus with Tests[END_REF] (even if everything works exactly the same way).

Our counter-example can be translated to some related cases. In particular, to prove non full abstraction of Scott's D ∞ for the λ-calculus with angelic and demonic sums (conjectured in [START_REF] Bucciarelli | A relational model of a parallel and non-deterministic lambda-calculus[END_REF]). For this calculus the extension with tests exists and is fully abstract for D ∞ , this is a trivial modification of the tests of [START_REF] Breuvart | A new proof of the Hyland/Wadsworth full abstraction theorem[END_REF] (using general demonic and angelic sums). In this framework the term θ(λxy.x + y) plays exactly the role of A in our example with the same output.

In the end, from a unique object that is DLL, we exhibit two natural constructions, one in the semantical world, the other in the syntactical one, but they appeared do not respect full abstraction. One would say that they are not that natural and that more natural one may be found. But this would be to easy, from the state of art we don't known more natural construction. The misunderstanding comes with the concept of naturality, it seems that the syntactic idea of "convergence" does not really correspond to the equivalent in semantical word. One being a lowest fix point and the second a largest one. This difference appears when working with the demonic sum that allow to check the convergence in unbounded applicative context.

Finally we presented tests as a general tool whose importance is above the role we gave them here. This result is interesting and important as it presents tests as useful tools to verify that full abstraction fails. But it remains a negative result that does not justify alone any real interest for them. Further works will then focus on presenting positive proofs of full abstractions that are using tests. Following this way we already submitted a revisited proof of full abstraction of the Scott's D ∞ for the usual λ-calculus [START_REF] Breuvart | A new proof of the Hyland/Wadsworth full abstraction theorem[END_REF].

A The model M ∞

A.1 Categorical model

The category Rel of sets and relations is known to be a model of linear logic as it is a Seely category (we are giving the interpretation, but we will let the comutative diagrams to the reader since their comutations are trivial or like):

It is monoidal with tensor functor given by A

⊗ B = A × B, f ⊗ g = {((u, x), (v, y)) (u, v) ∈ f, (x, y) ∈ g} and with the arbitrary unit 1 = { * }. It is symetric monoidal close with (A ⊸ B) = A × B if we take the evaluation ev = {(((a, b), a), b) a ∈ A, b ∈ B} ∈ Rel((A ⊸ B) ⊗ A, B
). So it is star autonomus with 1 as dualising object (for a trvial duality). This give us the interpretation of multiplicatives:

A⊗B = A`B = A ⊸ B = A×B
The category is cartesian, with catesian product ˘Ai = {(i, x) i ∈ I, x ∈ s i }, projections π i = {((i, a), a) a ∈ A i } and product of morphisms ˘i f i = {(b, (i, a)) (b, a) ∈ f i }. The terminal object is ⊺ = ∅. This give us the interpretation of additives:

⊕ i∈I A i = ˘i∈I A i = {(i, a) i ∈ I, a ∈ A i }
We can add a comonade (!, d, p) where the functor is define by ! But it can even be seen as a categorical model of differential linear logic. By defining the co-dereliction natural transforamtion dA = {(a, [a]) a ∈ A} ∈ A → !A, we are fixing the contraction c A = {(l+r, (l, r)) l, r ∈!A} the co-contraction cA = {((l, r), l+r) l, r ∈!A}, the weakening w A = {([], * )} and the co-weakening wA = {( * , [])}. So that we can define the derivative ∂ X = (id !X ⊗ d X ) ○ c X ∶!X → !X ⊗X and the co-derivative ∂X = cX ○(id !X ⊗ dD ) ∶!X ⊗X →!X. This derivatives are Taylor, i.e. if two morphisms f 1 , f 2 ∶!A → B are such that f 1 ○ ∂A = f 2 ○ ∂A then f 1 + (f 2 ○ wX ○ w X ) = (f 1 ○ wX ○ w X ) + f 2 . Finally the exponential acept anti-derivatives, since it is bi-comutative and J A = Id A + ∂A ∂ A = Id A is an isomorphism. For more detail about models of DLL see ??.

A = M f (A), !f = {([a 1 , ..., a k ], [b 1 , ..., b k ) ∀i ≤ k, (a i , b i ) ∈ f }, the deriliction by d A = {([a], a) a ∈ A} and the digging by p A = {(m 1 +⋯+m k , [m 1 , ..., m k ]) m 1 , ..., m k ∈ M F (a)
As for every categorical model of linear logic, the exponential is a comonade and induced a coKleisly M Rel = Rel ! whose objects are the set and whose morphisms from P to Q are the relations between !P and Q. The identities are the relations dig P = {({x}, x) x ∈ P } and the composition f ○g = {(X, z) ∃(Y, z) ∈ f, ∀y ∈ Y, (X, y) ∈ g}.

A.2 Algebraic model

In order to have an algebraic model of ∂λ-calculus we only need a reflexive object, i.e. a triplet (M, app, abs) where M is an object of MRel, app ∶ (M →

Lemma 2

 2 For all context C . of the ∂λ-calculus , if C I converges then C A converges, i.e. I ≤ ∂ A Proof. Let C . a context that converge on I With the context lemma ([14]), and since neither I nor A has free variables, we can assume that C . = . P 1 ⋯ P k , thus by lemma 1, we have A → * U + B k and C A → * U ′ + λw.w [I P 1 ⋯ P k ] = U ′ + λw.w [C M ] converges.

  }. This give us the interpretation of exponentials: !P =?P = M f (P ) This is a Seely category and a model of linear logic since the isomorphismes 1 ≃ [] is trivial and !A⊗!B ≃!(A & B) is defined by ([a 1 , ..., a l ], [b 1 , ..., b r ]) ≃ [(1, a 1 ), ..., (1, a l ), (2, b 1 ), ..., (2, b r )].

The type system is the following:Γ ⊢ ∆ x ∶ [], Γ ⊢ ∆ x ∶ [α] ⊢ x ∶ α Γ ⊢ M ∶ α Γ ⊢ M +N ∶ α Γ ⊢ N ∶ α Γ ⊢ M +N ∶ α Γ, x ∶ v ⊢ M ∶ α Γ ⊢ λx.M ∶ v∶∶α Γ ⊢ M ∶ w∶∶α Γ ′ ⊢ B ∶ w Γ + Γ ′ ⊢ M B ∶ α ⋀ j≤n Γ j ⊢ L j ∶ β j ⋀ i≥n Γ i ⊢ L ∶ β i (Σ n+m r=1 Γ r ) ⊢ [L 1 , ..., L n ; L ! ] ∶ [β 1 , ..., β n+m ] Γ ⊢ Q Γ ⊢ τ (Q) ∶ *

(!M ⊸ M ) = (M f (M ) × M )) and aps ∶ ((M f (M ) × M ) → M ) such that app ○ abs = Id. Such an object can a priory found by taking the lower fix point of M ↦ M ⇒ M =?M ⊸ M = M f (M ) × M . But this will just leads to the trivial empty model. We will then resolve the more complicated fix point M ↦ (?M ) &N = N × M f (M ) where the exponent represent an infinit tensor product. The lower fix point will be called M ∞ .

An other way to see the fixpoint is to say that M have to be equal to the set of quazi everywhere empty lists of finite substets of itself. Its element are the recursively defined as being either * , the list of empty elements, or a∶∶α with a ∈ M f (M ∞ ) and α ∈ M ∞ . The coresponding app and abs arise imediatly from the functoriality:

In order to be understandable, we are presenting the interpretation of terms via a type system with types living in M ∞ . The usual presentation of the interpretation can be recoverd from the type system: