Michele Pagani
email: michele.pagani@lipn.univ-paris13.fr

Visible acyclic differential nets Part I: semantics ✩

Keywords: Linear Logic, Differential Interaction Nets, Finiteness Spaces

We give a geometric condition that characterizes the differential nets having a finitary interpretation in finiteness spaces: visible acyclicity. This is based on visible paths, an extension to differential nets of a class of paths we introduced in the framework of linear logic nets. The characterization is then carried out as follows: the differential nets having no visible cycles are exactly those whose interpretation is a finitary relation. Visible acyclicity discloses a new kind of correctness for the promotion rule of linear logic, which goes beyond sequent calculus correctness.

Introduction

Nets in proof theory. The first protagonists of this paper are proof nets [START_REF] Girard | Linear logic[END_REF] -a graph-theoretical representation of linear logic proofs, made of cells and wires. Basically, cells correspond to the logical and structural rules, and wires correspond to the formulas 1 .

This proof system differs from sequent calculus, namely it represents the sequent rules disregarding the context formulas in most cases. Hence, proof nets yield canonical representatives with respect to several commutation equivalences over sequent proofs.

Having context-free rules, proof nets are similar to natural deductions. Indeed they have been called classical natural deductions by their inventor, Jean-Yves Girard [START_REF] Girard | Linear logic[END_REF]. Why classical? Traditional natural deduction (as defined by Gerhard Gentzen for intuitionistic and classical logic) represents a proof as a rooted tree, of which the leaves are the hypotheses and the root is the thesis of the proof. Such a "proof-as-tree" paradigm thinks of a proof as a function from its hypotheses (the leaves of the tree) to its thesis (the root). In this setting the renowned Curry-Howard correspondence was settled between traditional natural deduction (at first restricted to intuitionistic logic, then enlarged to wider systems) and functional programming (at first λ-calculus, later extended). Basically, this correspondence expresses that: (i) a logical formula can be seen as a data type (and conversely), (ii) a proof can be seen as a program (and conversely), (iii) the cut-elimination in a proof can be seen as the evaluation of the corresponding program (and conversely). This correspondence emphasizes the functional paradigm of computation underlying natural deductions.

However proof nets do not fit in such a paradigm. Considering cells as nodes and wires as edges, a proof net yields a graph more complicated than a treeit can contain cycles and has no specific conclusion as root. Instead of functions from inputs to outputs, proof nets seem rather to express communication channels between their conclusions. Since the inception of the proof net theory, a wealth of works appeared trying to link proof nets to process calculi (just for an example, see [START_REF] Abramsky | Computational interpretations of linear logic[END_REF]).

When speaking of a proof net as a classical deduction, we think we should not refer to classical logic in contrast with intuitionistic logic, but rather to a new geometrical shape of proofs emerging from proof nets, in contrast with the proof-as-tree paradigm adopted by traditional natural deduction (which actually yields a satisfactory proof system only for intuitionistic logic). What has driven to represent proofs as nets? The answer to this question should be addressed to our second protagonist -denotational semantics.

The semantics of proofs. Denotational semantics interprets programs as functions between given mathematical structures, like sets, topological spaces, vector spaces, etc. The idea is to model concrete and operational properties of programs with abstract and algebraic ones. Thanks to the Curry-Howard correspondence, denotational semantics provides an abstract interpretation also for natural deductions, thus fulfilling an old dream dating back to Arend Heyting, who figured a semantics for intuitionistic logic proofs.

Dana Scott constructed in 1969 the first of such semantics, defining a class of topological spaces called Scott domains [START_REF] Scott | Continuous lattices[END_REF]. His fruitful idea was to model the finitary aspect of computation by using the mathematical notion of continuity, by intepreting data types by topological spaces and programs by continuous functions. However, topological spaces in general behave badly with functional spaces, which are fundamental to model higher order types. Hence Scott domains are required to meet several constraints, and consequently they are better presented as partial ordered sets, enjoying some properties. Scott's topology is linked so much to this order, that continuous functions can be equivalently defined as the increasing functions which preserve the suprema of directed sets.

A notable class of models living in Scott's semantics is that of graph models, which was isolated in the seventies by Erwin Engeler, Gordon Plotkin and Scott himself. These models are called webbed since they define states as subsets of a set of more atomic elements, called web, and replace the order over states with set-theoretical inclusion. In this manner abstract notions take intuitive meanings (for example, compact elements become finite subsets, prime elements singletons). Any Scott continuous function f is completely determined by its trace, which is an encoding of its graph restricted to the pairs of compact and prime elements, e.g. in the setting of graph models: trace(f ) := { u, y ; y ∈ f (u), u finite state, y web element} .

(

) 1
Stable functions are a refinement of Scott continuous functions, introduced by Gérard Berry [START_REF] Berry | Stable models of typed lambda-calculi[END_REF] in order to catch the operational notion of sequential program. In webbed stable semantics, functional spaces encode stable functions by their traces, the web being then the Cartesian product between the set of the finite states of the domain and the web of the codomain. Of course not every subset of the web of a functional space is a stable trace, which opens the quest for criteria marking out those sets which are traces of stable functions. Girard's coherence spaces [START_REF] Girard | The system F of variable types, fifteen years later[END_REF] achieved one among the finest characterizations of stable traces.

A coherence space is a webbed model endowed with a symmetric and reflexive graph having as vertices the elements of the web -two vertices which are incident are said coherent. The cliques (i.e. complete subgraphs) of this graph are the states of the model; it turns out that the cliques of a functional space are exactly the stable traces. Moreover, Girard noticed that the space A → B associated with the stable functions from A to B is indeed asymmetrical, its web being made of pairs with finite cliques and web elements as left and right components, respectively (recall Equation (1)). Girard then detected a subclass of stable functions, that of linear functions, whose traces are symmetrical in the sense that the minimal cliques occurring in them are singletons: for f linear, trace(f ) := { {x}, y ; y ∈ f ({x}), x, y web elements} . [START_REF] Lafont | From proof nets to interaction nets[END_REF] Intuitively, linear functions correspond to programs evaluating outputs using exactly once their inputs. The space A ⊸ B of linear functions can be defined directly from the Cartesian product between the webs of A and B. Then the space of stable functions A → B decomposes into a space !A, whose web is the set of finite cliques of A, and the space of linear functions from !A to B:

A → B = !A ⊸ B . (3)
This decomposition led Girard to a new logic, based on linear functions -linear logic [START_REF] Girard | Linear logic[END_REF], LL for short. Linear logic is a refinement of classical and intuitionistic logic characterized by an involutive negation (-) ⊥ , the splitting of standard connectives ("and", "or") in two classes (the multiplicatives ⊗ and `, and the additives & and ⊕), and by the introduction of a new pair of dual connectives, the exponentials ! and ?. Exponentials give a logical status to the structural rules of classical and intuitionistic logic, and by Curry-Howard to the actions of erasing and duplicating data during the evaluation of a program. Proof nets arose precisely from this setting. LL proofs are interpreted as traces in A ⊸ B, and these, thanks to their symmetry, can be equivalently seen as traces in B ⊥ ⊸ A ⊥ . At a logical level, this means that an LL proof from hypothesis A to thesis B is also a proof from B ⊥ to A ⊥ (and viceversa). Proof nets provide a graphical representation of this equivalence, they are the syntactic counterpart of linear traces, expressing their crucial symmetry between domain and codomain, and moving from the proof-as-tree paradigm.

Our question: errors and correctness. This change of perspective (from proofas-tree to proof-as-net) introduces new objects in proof theory: wrong proofs. In fact, proof nets belong to a wider class of graphs, that of nets (or proof structures in Girard's terminology). Not every net is a proof net (i.e. it corresponds to a proof in the usual sequent calculus), some nets represent proofs with errors (intuitively they are argumentations using part of the thesis as hypothesis). Correctness criteria have been designed in order to characterize the set of proof nets, independently from the sequent calculus. In this paper we will mention one of these criteria -switching acyclicity (see Definition 2.3 and Theorem 2.4), introduced by Vincent Danos and Laurent Regnier [START_REF] Danos | The structure of multiplicatives[END_REF] at first in the multiplicative fragment of linear logic (MLL for short).

The dichotomy between "correct" and "incorrect" net has a semantic counterpart. As we wrote above, proof nets correspond to traces of linear functions. What about nets in general? By means of the key notion of experiment ([1], Definition 2.14) one can interpret any net as a subset of the web associated with the conclusions of the net. In case the net is a proof net, then this subset is a trace of a linear function (i.e. a clique in coherence spaces): Theorem 1.1 ( [START_REF] Girard | Linear logic[END_REF]). If a LL net is switching acyclic (i.e. it is a proof net), then its interpretation is a clique in any coherence space associated with its conclusions.

However, in case the net contains "errors", its interpretation might not be a clique. Indeed, Christian Retoré proved in [START_REF] Retoré | A semantic characterisation of the correctness of a proof net[END_REF] that in the multiplicative fragment of linear logic Girard's theorem can be reversed as follows: Theorem 1.2 ( [START_REF] Retoré | A semantic characterisation of the correctness of a proof net[END_REF]). If a MLL net is cut-free and it is interpreted as a clique in any coherence space associated with its conclusions, then it is switching acyclic.

Girard's and Retoré's Theorems prove together that switching acyclicity expresses in MLL nets the semantic property of being a trace of a linear function between coherence spaces. There is an intriguing relation between the logical correctness, dealing with the switching paths on nets by Danos and Regnier's criterion, and the semantic definition of linear trace, characterized by the notion of clique in the coherence spaces.

Girard's theorem 1.1 is proved by a technique consisting in drawing a switching path 2 in a net following the coherence/incoherence relations between the values of two experiments of that net. Then from switching acyclicity one easily deduces the pairwise coherence of the elements of the web associated with these experiments. Retoré's theorem 1.2 is proved by reversing this technique: experiments can be built following switching paths.

Retoré's theorem adds the hypothesis of being cut-free: in case of cuts one might have switching cycles invisible to coherence spaces. One should expect such constraint -the denotational interpretation of a net with cuts usually (and so it is for coherence spaces) does not describe the net itself, but its normal form. We also want to emphasize the requirement of being a clique in any coherence space associated with the conclusions of a net. The interpretation of the conclusions is in fact not unique, but parameterized by the coherence space associated with the atomic variables occurring in them, and proving switching acyclicity needs to interpret such variables as a space having at least three points in its web, two of them strictly coherent and two strictly incoherent 3 .

Multiplicative linear logic is an ideal world where syntax and semantics happily marry, but things become harder as one starts to extend the framework. In presence of additives, for example, we mention Paolo Tranquilli's hypercorrectness [START_REF] Tranquilli | A characterization of hypercoherent semantic correctness in multiplicative additive linear logic[END_REF], a fine criterion on nets corresponding to the semantic correctness of hypecoherence spaces (a refinement of coherence spaces able to catch the strongly stable functions) -it remains an open question whether hypercorrectness is equivalent to the correctness induced by sequent calculus. As for the present work, we are interested in what happens when exponentials come into the picture.

Exponentials introduce weakening and contraction in LL. In sequent calculus a proof of the premise of a promotion rule -the sole logical rule of LL introducing !-formulas (see Figure 1(a)) -may be duplicated or erased under the elimination of a cut between that promotion and resp. a contraction or a weakening. In this cut-elimination the context of that promotion plays an active role, since it changes its formulas into conclusions of contractions (if the above proof is duplicated) or weakenings (if the above proof is erased). In the setting of nets, this means that the context of promotion must be left explicit, thus adding a bit of sequentialization. Sequent calculus promotion is in fact translated in nets with the so-called exponential box -a special cell having the feature of being parameterized by a net, this last one standing for the proof of the premise of the corresponding promotion rule (see Definition 2.1 and Figure 3). The net associated with a box is often referred to as the contents of that box.

How do boxes alter the correctness criterion on nets? How do paths inside a box interact with those outside? A rough answer is the so-called black-box principle [START_REF] Girard | Linear logic[END_REF]: no interaction is possible, a box is an insuperable wall dividing the inside from the outside. Danos and Regnier's criterion extends to the multiplicative exponential fragment of linear logic (MELL) following this principle: a MELL net is switching acyclic whenever its boxed subnets are switching acyclic, and the net itself is switching acyclic if one sees boxes as simple nodes (see Definition 2.3). This criterion characterizes MELL proof nets, that is those nets which correspond to MELL sequent calculus proofs.

Here is the problem: the semantic correctness is different from switching acyclicity on exponential boxes. There are switching cycles "invisible" to coherence spaces, and consequently there are non-logically correct nets interpreted as cliques. Such invisible cycles always cross exponential boxes and their invisibility depends on the contents of these boxes (the reader will find examples in Figures 4(b)/5(a) and in Figure 6). This means that semantic correctness does not respect the black-box principle.

In [START_REF] Pagani | Acyclicity and Coherence in Multiplicative and Exponential Linear Logic[END_REF] we analyzed this phenomenon and we designed a new notion of paths, called visible paths (Definition 2.5), yielding an acyclicity criterion weaker than switching acyclicity. We then proved that visible acyclicity characterizes the nets interpreted as cliques in non-uniform coherence spaces: 4Theorem 1.3 ([11]). If a MELL net is visible-acyclic, then its interpretation is a clique in any (non-uniform) coherence space associated with its conclusions. Theorem 1.4 ([11]). If a MELL net is a value and it is interpreted as a clique in any non-uniform coherence space associated with its conclusions, then it is visible-acyclic.

Let us spend a word about the notion of value appearing in Theorem 1.4. Values (Definition 2.8) stand for cut-free nets in Retoré's Theorem -besides cuts, the presence of exponentials require to rule out upward cycles and weak wires also. Value means then cut-free, upward acyclic, and weak wire-free net. These are technical details explained in Definition 2.8 and in the discussion of Figure 13. 5The goal of this paper is to generalize Theorems 1.3 and 1.4 to a wider setting, that of differential linear logic and finiteness spaces.

Differential linear logic. The differential extension of linear logic has risen from a recasting by Ehrhard of an intuition dating back to Girard's quantitative semantics [START_REF] Girard | Normal functors, power series and λ-calculus[END_REF] -stable functions (i.e. non-linear proofs) can be seen as analytic functions.

In the stable webbed semantics, states are subsets of webs and linear functions over states are represented by their traces, i.e. relations between webs (recall (2)). Indeed, the powerset of a set X can be seen as a module {0, 1} X , addition is componentwise and corresponds to set union. In this setting traces are matrices indexed by the Cartesian product of the webs of the domain and codomain, and the functions they represent are linear in a standard mathematical sense, i.e. they preserve addition and multiplication by a scalar. Quantitative semantics takes this idea forward, and considers modules (usually vector spaces) taking scalars from rigs (usually fields) richer than {0, 1}. The clear improvement on "usual" denotational semantics being that vectors allow to model quantitative properties of programs.

Let K be a field, A and B be two finite sets. Linear functions between the vector spaces K A and K B form a space K A ⊸ K B having as a basis the Cartesian product A × B, in the sense that any linear function can be seen as a matrix in K A×B (and conversely). Composition u • v between v ∈ K A ⊸ K B and u ∈ K B ⊸ K C corresponds then to the matrix product:

(u • v) a,c := b∈B v a,b • u b,c , (4)
where • is the product between scalars. Equation ( 4) expresses in the quantitative setting the superimposition of various possible results of eliminating non-deterministically a cut between a proof of A ⊸ B and a proof of B ⊸ C. Equation ( 4) is well-defined since we are supposing B finite. Interpreting exponentials complicates things, since they require vector spaces with infinite dimension. In that case, there is no reason why the sum in Equation (4) should converge, and the quest for subspaces guaranteeing such a convergence begins.

Noteworthily, coherence spaces have something to say on this matter. Indeed considering bases as webs of coherence spaces A, B, C, one can take the set of vectors having cliques as supports 6 . Restricted to this set the sum in (4) always converges, for the simple reason that, fixed a ∈ |A| and c ∈ |C|, there is a unique b ∈ |B| for which both v a,b and u b,c differ from 0.7 However the set of vectors having cliques as support unfits this setting, since it does not define a vector space (nor a module), not being closed under the sum (the union of two cliques is not in general a clique).

The search for better solutions led Thomas Ehrhard to new webbed semantics -Köthe spaces [START_REF] Ehrhard | On köthe sequence spaces and linear logic[END_REF] and finiteness spaces [START_REF] Ehrhard | Finiteness spaces[END_REF]. Let us focus on these latter. The idea is to relax the notion of clique, requiring that the number of b ∈ |B| s.t. both v a,b and u b,c differ from 0 (fixed a ∈ |A| and c ∈ |C|) is finite, instead of being at most one. This condition suffices for having the convergence of (4), and yields a vector space, being closed under finite sums of vectors (and of course scalar multiplication).

Concretely, we define an operation over subsets of a powerset P(X): for

F ⊆ P(X), we set F ⊥ = {v ⊆ X ; ∀u ∈ F, v ∩ u is finite} ⊆ P(X).
Then a finiteness space is a pair X = |X |, F (X ) , where |X | is a set, the web, and F (X ) is a collection of subsets of |X | such that F (X ) = F (X ) ⊥⊥ . The elements in F (X ) are called finitary subsets of X . The vector space associated with X will be the collection K X of all vectors in K |X | whose support is in F (X ). Intuitively, finitary sets play the role of cliques in coherence spaces. However this analogy fails for two key points: (i) finitary sets are closed under finite unions, cliques are not; and (ii) cliques are closed under infinite unions of compatible cliques 8 , finitary sets are not (unless F (X ) = P(|X |)). Point (i) explains why finiteness spaces give rise to vector spaces, while coherence spaces do not, and point (ii) why finiteness spaces do not admit Scott's topology, where continuity is seen as preservation of directed unions. Indeed, finiteness spaces yield a different topology 9 (studied at first by Lefschetz in 1942), and interpret linear logic proofs as linear (in the algebraic sense) and continuous (in Lefschetz topology) functions.

This setting yields also a mathematically very appealing interpretation of non-linear (i.e. intuitionistic) proofs. Linear continuous functions from K !A to K B can be seen as entire functions from K A to K B , that is power series converging on the whole space K A . This fulfils in a standard algebraic setting Girard's intuition [START_REF] Girard | Normal functors, power series and λ-calculus[END_REF] of interpreting intuitionistic proofs (i.e. λ-terms) as analytic functions.

Analytic functions are smooth, i.e. infinitely differentiable, and we can wonder whether differentiation is a meaningful syntactic operation. A positive answer is given by Ehrhard and Regnier's differential λ-calculus [START_REF] Ehrhard | The differential lambda-calculus[END_REF] and differential linear logic [18] 10 , DiLL for short. Differential linear logic is an extension of LL characterized by a sum rule, expressing addition between vectors, and three new rules dealing with the ! modality -coweakening, cocontraction and codereliction (see Figure 1(c)). These rules are dual of the corresponding ? rules and give a logical status to differentiation, codereliction expressing in particular the derivative of a function at 0 (see [START_REF] Ehrhard | Differential interaction nets[END_REF] for more details).

Differential linear logic has its own nets, differential nets -formal sums of simple nets made of cells (those of LL plus the ones associated with the new ! rules) and wires. As LL nets correspond to relations between webs, some of them being traces of linear functions, differential nets can be seen as syntactical counterparts of web-indexed matrices, some of them representing linear continuous functions (with respect to a given basis). It is then natural to look for geometrical criteria characterizing the nets associated with the matrices of linear continuous functions. The main results of this paper (Theorem 3.3 and 8 Two cliques are compatible if their union is a clique. 9 A sharp contrast between the topology endowed by finiteness spaces and that by Scott domains is that the former is Hausdorff, the latter is not.

10 Actually [START_REF] Ehrhard | Differential interaction nets[END_REF] presents the promotion-free fragment of differential linear logic. As for references to the whole differential linear logic (i.e. with promotion) we mention Lionel Vaux's PhD thesis [START_REF] Vaux | λ-calcul différentiel et logique classique : interactions calculatoires[END_REF], mainly dedicated to a polarized version of differential linear logic, Tranquilli's paper [START_REF] Tranquilli | Intuitionistic differential nets and lambda-calculus[END_REF], focused on differential λ-calculus, and Pagani and Tranquilli's paper [START_REF] Pagani | The conservation theorem for differential nets[END_REF].

Theorem 4.5) prove that the extension of visible acyclicity to differential nets yields such a criterion.

More in detail, consider two finiteness spaces A and B. A net π with conclusions A ⊥ , B is interpreted as a matrix π in K |A|×|B| . This matrix describes a partial function π from the vector space K A to the space K B , but in general this function can be non-total (i.e. Equation 4 does not always converge) and non-continuous (with respect to the Lefschetz linear topology associated with K A and K B ). As mentioned above, Ehrhard proves in [START_REF] Ehrhard | Finiteness spaces[END_REF] that π is linear (hence total) and continuous if and only if the support of π is a finitary set of the finiteness space A ⊸ B (i.e. iff π belongs to K A ⊸ B ). Our Theorems 3.3 and 4.5 then prove that the support of π is a finitary relation if and only if π is visible-acyclic. Of course Theorem 4.5 holds (and so the characterization of linear continuous functions by means of visible acyclicity) supposing π enjoys hypotheses analogous to the ones discussed previously for Retoré's Theorem (here Th. 1.2) and Theorem 1.4 -π should be a value and the variables occurring in A ⊥ and B should be interpreted with a finiteness space having two infinite sets, one finitary and the other one anti-finitary (i.e. finitary in the dual space).

Waiting for cut-elimination. As written above, finiteness spaces have been designed to have a notion of linear functions which compose, i.e. for which the sum in (4) converges. Composition expresses cut-elimination in semantics, and the convergence of (4) corresponds to the termination of cut-elimination. Having these observations in mind, it becomes natural to expect strict links between finiteness spaces and normalization properties of differential nets.

This feeling is strengthened by Ehrhard's remark that (usual) fixed point operators are not finitary [START_REF] Ehrhard | Finiteness spaces[END_REF]. We recast the remark in the framework of differential nets, by considering a net (Figure 10) introduced by Raphaël Montelatici [START_REF] Montelatici | Polarized proof nets with cycles and fixpoints semantics[END_REF]: this net yields a fixed point operator in (a polarized fragment of) LL. Here we show that the net is visibly cyclic and that its interpretation is not finitary.

We will present a strict correspondence between normalization and finiteness spaces in a forthcoming paper [START_REF] Pagani | Visible acyclic differential nets -Part II: interaction[END_REF], the present one being already quite long. . . We say that a set of differential nets has a safe interaction, when any cut between two nets in this set can be eliminated in a finite number of steps. We will prove in [START_REF] Pagani | Visible acyclic differential nets -Part II: interaction[END_REF] that the set of visible-acyclic nets is exactly the maximum set of differential nets containing the image of the desequentialization of DiLL and having a safe interaction. Then, using the correspondence between visible acyclicity and finitary sets proved here, we conclude that finiteness spaces characterize the "closure" of DiLL with respect to safe interaction.

Preliminaries

In this section we introduce all notions and properties we use in this work; since we want a self-contained paper, the definitions abounded; since we want also, as far as we can, a readable paper, most of the definitions are left in normal text, emphasized with boldface. We reserve a regular definition environment only for the key notions of differential net (Def. 2.1), switching acyclicity (Def. 2.3), visible acyclicity (Def. 2.5), value (Def. 2.8), finiteness space (Def. 2.9), experiment (Def. 2.14), and finitary net (Def. 2.15).

Notation. We denote sets with braces { }, multisets with square brackets [ ] and sequences by angles . The left projection (resp. right) of a pair is written as p 1 (resp. p 2 ): p 1 ( a, b ) = a, p 2 ( a, b ) = b. We denote sets with capital Latin letters X, Y, . . . , and multisets with Greek letters µ, ν, . . . . Given two sets X and Y , we write X ⊆ ∞ Y whenever X is an infinite subset of Y ; we denote by P(X) the power set of X, and by M f in (X) the set of finite multisets over X, equivalently seen as functions µ : X → N with finite support (which is denoted by supp(µ)). We will use the multiset additive notation: [x, y] + [x] = [x, x, y], as well as for any natural number n, n[x, y] = [x, y, . . . , x, y n times ]. We denote by 0 the empty multiset. If X is a set or a multiset, we denote by card(X) the cardinality of X.

In the sequel, we will speak of an element x of a multiset µ meaning an occurrence of the element x in µ. As a consequence, when we write x ∈ µ, we are considering an occurrence of x in the multiset µ, and when that expression bounds an operator, as for example in x∈µ , we mean that x ∈ µ varies on the set of occurrences of µ's elements. At least, to make easier notations, we will often denote a singleton [x] ∈ M f in (X) with its unique element x. So we have for example µ = x∈µ x.

Let I be a set, an I-indexed family (x i ) i∈I is a function with domain in I: we denote by {x i } i∈I its set of values. Notice that the cardinality of {x i } i∈I can be less than that of I in the case there are i, j ∈ I with x i = x j . The family (x i ) i∈I is injective if for any i, j ∈ I, i = j entails x i = x j .

As usual, we can drop brackets for arguments of unary operators: for example, given a multiset µ, supp µ means supp(µ).

Differential nets

Differential linear logic. The formulas of propositional multiplicative exponential unit-free linear logic, MELL for short, are generated by the following grammar, where X is a fixed propositional variable:

A, B ::= X | X ⊥ | A ⊗ B | A `B | !A | ?A.
In order to avoid useless bureaucracy, we deal with formulas generated by a unique variable X. However every result in this paper can be easily extended to the general case of more variables. A real restriction is instead the absence of the multiplicative units 1, ⊥: this constraint is required by Theorem 4.5, as we will discuss at the beginning of Section 4.

Linear negation is defined through De Morgan laws:

(X) ⊥ := X ⊥ (X ⊥ ) ⊥ := X (A ⊗ B) ⊥ := A ⊥ `B⊥ (A `B) ⊥ := A ⊥ ⊗ B ⊥ (!A) ⊥ := ?A ⊥ (?A) ⊥ := !A ⊥
The variable X and its negation are atomic, connectives ⊗, `are called multiplicative, while !, ? are exponential. Also X, ⊗, ! are called positive, while X ⊥ , `, ? are negative. A sequent Γ is a finite sequence (possibly empty) of formulas A 1 , . . . , A n . We denote sequents by capital Greek letters Γ, ∆, . . . . The degree of a formula A, denoted deg A, is the number of connectives occurring in A. Linear logic sequent calculus for MELL is defined in Fig. 1(a).11 Indeed we will deal with an extension of MELL, defined by adding the rules empty and mix of Fig. 1(b). This extension is standard in the framework of proof-nets, allowing simple correctness criteria (see for example [START_REF] Tortora De Falco | Obsessional experiments for linear logic proof-nets[END_REF], see also Theorem 2.4). Notice that empty and zeroary ? rules allow to prove ⊢ ?A for every formula A.

Starting from their work on differential λ-calculus [START_REF] Ehrhard | The differential lambda-calculus[END_REF], Ehrhard and Regnier introduced the differential extension of linear logic, defined by the rules of Figure 1(c); in [START_REF] Ehrhard | The differential lambda-calculus[END_REF][START_REF] Ehrhard | Differential interaction nets[END_REF] it is discussed a very appealing mathematical interpretation of these rules, associating them with differential operators over the proofs of LL, so motivating the adjective differential.

We call differential linear logic, DiLL for short, the logic defined by the rules of the whole Figure 1. Notice that every formula A is provable in DiLL by using a zeroary sum rule; moreover, if every occurrence of the atoms X and X ⊥ in A is under the scope of an exponential, then we can prove A even without the sum rule. These peculiar facts show that a theory of DiLL provability should be quite problematic. On the contrary, a theory of proofs seems really fruitful, indeed DiLL cut-elimination modifies the viewpoint on linear logic exponentials: not only these connectives allow to give a logical status to the structural rules of weakening and contraction, but also they model, thanks to the differential rules,

ax ⊢ A, A ⊥ ⊢ Γ, A ⊢ A ⊥ , ∆ cut ⊢ Γ, ∆ ⊢ Γ, A, B, ∆ ex ⊢ Γ, B, A, ∆ ⊢ Γ, A, B ⊢ Γ, A `B ⊢ Γ, A ⊢ B, ∆ ⊗ ⊢ Γ, A ⊗ B, ∆ ⊢ Γ, ?A, . . . , ?A ? ⊢ Γ, ?A ⊢ Γ, A ?d ⊢ Γ, ?A ⊢ ?Γ, A p ⊢ ?Γ, !A (a) unit-free MELL [1] empty ⊢ ⊢ Γ ⊢ ∆ mix ⊢ Γ, ∆ (b)
empty and mix rules

⊢ Γ • • • ⊢ Γ sum ⊢ Γ ⊢ Γ, A !d ⊢ Γ, !A ⊢ !A, Γ 1 • • • ⊢ !A, Γ n ! ⊢ !A, Γ 1 , . . . , Γ n (c) differential rules [17]
Figure 1: sequent calculus rules for differential linear logic; in the ?-rule we allow to contract a number n ≥ 0 (n = 1) of ?A formulas; the !-rule and the sum-rule have n ≥ 0 (n = 1) premises, in case n = 0 they are initial rules.

a kind of communication between proofs which is similar to the one described in process calculi (see [START_REF] Ehrhard | Interpreting a finitary pi-calculus in differential interaction nets[END_REF]).

Interaction nets. The proofs of DiLL sequent calculus can be translated into graphs called differential nets: in Figure 3 we give such a translation. Differential nets are introduced in Definition 2.1. They are defined on top of Lafont's interaction nets [START_REF] Lafont | Interaction nets[END_REF], so we start by briefly recalling these last ones (for more details, we refer to [START_REF] Mazza | Interaction nets: Semantics and concurrent extensions[END_REF]).

An interaction net α is the union of two structures: a directed hypergraph and an undirected graph on a given set of nodes.

• The nodes of α are called ports. Every port is crossed exactly by one edge and at most by one hyperedge. Ports will be denoted by final Latin letters p, q, r . . .

• The directed hyperedges are called cells or links. Every link l is labelled by a symbol taken from a given alphabet. Such a label determines the arity of l, that is the number of ports crossed by l, and the types of the wires incident with l. Every link crosses at least one port, the first one being called principal, the other ones (if any) being called auxiliary.

Cells are typically graphically depicted as triangles with the principal port on a vertex, the auxiliary ones on the opposed side, and the label inside the triangle: *

• • • principal port cell label auxiliary ports

Cells will be denoted by middle-position Latin letters l, m, o . . .

• The undirected edges of α are called wires, and they are denoted by initial position Latin letters a, b, c . . . . We allow wires with only one incident node, called loops, and we impose that no loop crosses cell ports. A wire a incident to two different ports p and q has two orientations: from p to q and from q to p. We denote one of such orientations by ↑a and the other one by ↓a; we write a meaning indifferently ↑a or ↓a. If a is an oriented wire from p to q, then we call p (resp. q) its source (resp. target). We require that to every orientation is assigned a MELL formula in such a way that if A is associated with ↑a, then A ⊥ is associated with ↓a:

A q p ↑a iff A ⊥ q p ↓a
We refer to the label A of an oriented wire a as its type, and we write a : A. By an extension of language we speak also of the type of an unoriented wire, meaning the type of one of its orientations (so for example a has type A, as well as A ⊥ ). Also, with every loop we associate a pair of dual types A, A ⊥ . The ports of an interaction net α which are not crossed by hyperedges nor by loops are called free. We require that α is given together with an enumeration p 1 , . . . , p n of its free ports. An oriented wire a is a premise (resp. conclusion) of a cell l whenever its target (resp. source) is an auxiliary (resp. the principal) port of l; a is a conclusion of α whenever its target is a free port of α. Usually premises/conclusions will be presented together with their respective types. Notice that for every free port p of α there is exactly one conclusion having p as extremity; notice also that it might well be the case that both the orientations ↑ a, ↓ a of a wire a are conclusions of α. The interface of α is the sequence of its conclusions a 1 : A 1 , . . . , a n : A n , where p 1 , . . . , p n is the enumeration of α's free ports, and for every i ≤ n, p i is the target of a i . 12 We call the sequent Γ = A 1 , . . . , A n the sequent conclusion of α. Let c 1 : C 1 , . . . , c m : C m be the interface of another interaction net β, we say that α and β have the same interface, if n = m and for every i ≤ n, A i = C i . Notice that two interaction nets with the same sequent conclusion have the same interface.

Our manner of typing oriented wires is taken from [START_REF] Lafont | From proof nets to interaction nets[END_REF] and it follows Girard's basic idea (see [START_REF] Girard | Linear logic[END_REF]) of handling linear negation apart from logical connectives, meaning a switch between two dual configurations such as true/false, input/output, question/answer. In the framework of nets, negation is the change of wire orientation.

The degree of a wire a, denoted deg a, is the degree of one of its types. Notice deg a is well-defined, since deg A = deg A ⊥ .

Differential nets. In the specific case of differential nets, cells will be labelled by the logical (⊗, `) and structural (?, ?d, !, !d, p) rules of the sequent calculus in Figure 1. Apart from promotion (which we discuss separately below), the principal port (resp. auxiliary ports) of a cell stands for the active formula in the conclusion (resp. in the premises) of the corresponding sequent calculus rule. Wires set connections between cells, they correspond to sequent calculus identities (axiom and cut) and, more in general, to formula occurrences in a proof.

Differential nets actually go out of the interaction net paradigm for two reasons: they have boxes, and they are linear combinations of simple nets. Boxes are necessary to represent linear logic promotion: they are a special kind of cells parameterized by a net, this last one standing for a proof of the premise of the corresponding promotion rule. In sequent calculus, the context of promotion plays an active role in cut-elimination: this requires to add a bit of sequentialization in our nets, by "boxing" the subgraph corresponding to the proof of the premise of a promotion rule. The introduction of boxes makes fundamental results like confluence or normalization far harder than in usual interaction net paradigm, since it introduces commutative cuts.

The differential extension of linear logic requires a second step forward: for- mal sums have to be introduced in order to represent the sum rule in Figure 1(c). The way we manage these sums is very similar to the handling of linear logic additives in sliced proof-nets (see [START_REF] Pagani | Strong Normalization Property for Second Order Linear Logic[END_REF]). In a general setting, differential nets are finite linear combinations of simple nets with coefficients in a commutative semiring with units. More precisely, taken a commutative semiring R with unit, and denoted by S the set of simple nets, the set of differential nets with coefficients in R is the R-module R S generated by S. That is, a generic element of R S is written as α∈S c α α, with c α ∈ R and for all but a finite number of α ∈ S, c α = 0. In this paper however we will consider only the case R = N, and in such a case N S is in fact M f in (S), and each sum can be written without coefficients, as for π ∈ N S = M f in (S) we can write π = α∈π α, as explained in the paragraph on notations.

A `B A B par or `-cell A ⊗ B A B ⊗ tensor or ⊗-cell !A ?C 1 • • • ?Cn !π promotion or box ?A ?d A dereliction or ?d-cell ?A ?A ? • • • ?A contraction or ?- cell !A !d A codereliction or !d-cell !A !A ! • • • !A cocontraction or !-cell
Simple nets and differential nets are defined simultaneously, by induction on their exponential depth: Definition 2.1 (From [START_REF] Ehrhard | Differential interaction nets[END_REF]). A simple net of depth 0 is an interaction net defined from the links of Figure 2, without the box. A simple net of depth d + 1 is an interaction net α defined from the links of Figure 2, such that every box o of α is labelled by a symbol !π, where π is a differential net of depth at most d, called the contents of o. Moreover, together with o it is given a fixed correspondence between the conclusions of every simple net β ∈ π and the premises and conclusions of o: for every premise/conclusion a of o we denote by a β the corresponding free port of β. This correspondence enjoys the following typing conditions:

• if a : !A is the conclusion of o, then the conclusion a β of β must have type A; • if a : !A is a premise of o, then the conclusion a β of β must have type ?A ⊥ .
Finally, α has at least one box with contents a differential net of depth d.

A differential net π of depth d and sequent conclusion Γ is a finite multiset of simple nets of depth at most d, with sequent conclusion Γ, and such that at least one of these simple nets has depth d. We denote by depth π the depth of π. We define DN as the set of differential nets. We denote simple nets by initial Greek letters α, β . . . , differential nets by final Greek letters π, σ, ρ . . . . Notice that, following the terminology of interaction nets, we call premise (resp. conclusion) of a cell l an oriented wire a having the target auxiliary port (resp. the source principal port) of l. In particular, remark the difference with respect to the standard terminology on proof-nets in case l is a box.

With the sake of simplifying figures, we often omit to write types, if unimportant; we also avoid to denote ports with explicit dots, as they correspond to wire extremities. Sometimes we present a box with its contents pictured inside, as for example:

β • • • β∈π ?C n ?C 1 A !A • • • ?C n ?C 1 := • • • !π ?C n ?C n !A
We also adopt the convention of barring wires, meaning bunches of multiple wires, as for example:

? := • • • ?
We refer to a port/cell/wire of a differential net π as to a port/cell/wire of a simple net in π; we refer to a port/cell/wire of a simple net α as to a port/cell/wire of α viewed as an interaction net: this means in particular that the ports/cells/wires of ρ are not ports/cells/wires of a simple net containing !ρ as a box.

A cut is a wire connecting two principal ports or a principal port and an auxiliary port of a box. An axiom is a wire which does not connect any principal or box auxiliary port. We will call n-contraction (resp. n-cocontractions) one which has n + 1 ports; 0-contractions (resp. 0-cocontractions) are also called weakenings (resp. coweakenings). We denote by Box(α) the set of boxes of α. We extend this notation to differential nets: Box π := ∪ α∈π Box α.

The size of a simple net α, as well as of a differential net π, is defined by induction on their depths:

size α := number of ports in α + !π∈Box α size π, size π := α∈π size α.
Many definitions of this paper are done by induction on the depth of differential nets, as we did for the size: let us skip to say it explicitly, when evident. So, we define a differential net π cut-free whenever every π's simple net is cut-free; and we define a simple net α cut-free whenever α has no cut and for every !π ∈ Box α, π is cut-free.

As mentioned at the beginning of the paragraph, the proofs of DiLL sequent calculus can be translated in differential nets. This translation is named desequentialization: given a sequent proof P with conclusion ⊢ Γ, the desequentialization of P , denoted Des P , is the differential net with sequent conclusion Γ defined inductively by the rules of Figure 3. Notice that promotion is the only non linear rule -sums remain within the boxes. Desequentialization enjoys several properties: it simulates cut-elimination, it offers canonical representatives for several commutative equivalences, it preserves denotational semantics interpretation, etc. . . . What we are interested in here is that switching acyclicity (which will be introduced in the next paragraph) geometrically characterizes exactly those differential nets which are the translation of DiLL sequent proofs.

Paths and acyclicity. One of the main tools in our investigation is the notion of path. Paths allow us to walk in a simple net, and they provide a geometric account of syntactic and semantic behaviors of nets.

A path φ in a simple net α is a sequence a 1 , . . . , a n of oriented wires of α such that for every different i, j ≤ n, a i = a j , and for every i < n, the target of a i and the source of a i+1 are ports of the same cell. We say that φ starts from a 1 , or from a 1 , and ends in a n , or in a n . The length of φ is n, that is the number of wires composing φ. A differential net π contains φ if π = α + π ′ , and φ is a path of α.

We say that φ crosses a wire a (resp. an oriented wire a), and we write a ∈ φ (resp. a ∈ φ), whenever there is an i ≤ n such that a = a i (resp. a = a i ). Notice that a ∈ φ entails a ∈ φ; conversely a ∈ φ entails ↑a ∈ φ or ↓a ∈ φ. We say that φ crosses a cell l, if φ crosses at least two wires incident to that cell.

The path φ is a cycle whenever the target of a n and the source of a 1 are the same port (i.e. φ is a loop) or are ports of the same cell. Of course if φ is a cycle, any cyclic permutation a k , . . . , a n , a 1 , . . . , a k-1 of φ's wires (k ≤ n) is a cycle.

We define the composition φ • ψ of two paths φ = a 1 , . . . , a n and ψ = c 1 , . . . , c m whenever a n = c 1 , and for every i < n, and j, 1 < j ≤ m, a i = c j . The composition is then:

φ • ψ := a 1 , . . . , a n = c 1 , . . . , c m .
Notice that the wires and cells crossed by φ • ψ are exactly the ones crossed by φ plus the ones crossed by ψ.

!X ⊥ ? !X ⊥ ? ?X ?X ↑b ↑a
An oriented wire a is upward whenever the source of a is either auxiliary or free, and the target of a is principal. Notice that neither axioms nor cuts can have upward orientations. A path is upward, if it is a sequence of upward oriented wires. A wire a is above another wire b in α, a > α b for short, if there is an upward path of length at least 2 from a to b. Notice that in general > α is not an order on wires, due to the possible presence of upward cycles in α. For example, in the simple net at left we have an upward cycle ↑a, ↑b , so that a > α b > α a.

Des ax ⊢ A, A ⊥ := A A ⊥ Des empty ⊢ := empty graph Des   P 1 ⊢ Γ, A P 2 ⊢ A ⊥ , ∆ cut ⊢ Γ, ∆   := α∈Des P1 β∈Des P2 α ∆ Γ β A Des   P ⊢ Γ, A, B, ∆ ex ⊢ Γ, B, A, ∆   := α∈Des P Γ ∆ α B A Des   P ⊢ Γ, A, B ⊢ Γ, A `B   := α∈Des P α Γ A `B Des   P 1 ⊢ Γ, A P 2 ⊢ B, ∆ ⊗ ⊢ Γ, A ⊗ B, ∆   := α∈Des P1 β∈Des P2 α ⊗ Γ ∆ β A ⊗ B Des   P ⊢ Γ, A ?d ⊢ Γ, ?A   := α∈Des P ?A ?d Γ α Des   P ⊢ Γ, ?A, . . . , ?A ? ⊢ Γ, ?A   := α∈Des P α Γ ?A ? • • • Des   P ⊢ ?Γ, A p ⊢ ?Γ, !A   := α !d !A ?Γ α∈Des P Des   P ⊢ Γ, A !d ⊢ Γ, !A   := α∈Des P Γ α !A !d Des   P 1 ⊢ !A, Γ 1 • • • P n ⊢ !A, Γ n ! ⊢ !A, Γ 1 , . . . , Γ n   := α1∈Des P1 . . . αn∈Des Pn ! !A α 1 Γ 1 Γn αn • • • Des   P 1 ⊢ Γ P 2 ⊢ ∆ mix ⊢ Γ, ∆   := α∈Des P1 β∈Des P2 α Γ ∆ β Des P 1 ⊢ Γ • • • P n ⊢ Γ sum ⊢ Γ := n i=1 Des P i
d `?!X !X ?X ⊥ `?!X !X ?X ⊥ ↓e ↑a ↑a ′ ↓b ′ ↓b ?!X ?X ⊥ !!X
Proposition 2.2. Let α be a simple net with no upward cycles, then > α is a well-founded order over the wires of α.

Proof. First, we prove the transitivity of > α . Assume a > α b, and b > α c. We will prove that there is an upward path from a to c. Clearly if a = c, then this path has length ≥ 2, hence proving a > α c. The assumptions a > α b and b > α c entail that there are two upward paths φ and ψ, both of length ≥ 2 and φ from a to b, ψ from b to c. Let b ′ be the first wire crossed by φ which is also in ψ. Notice that such a b ′ should exist, since φ and ψ share at least b. Notice also that both φ and ψ must cross b ′ with the same orientation, in fact: ↑b ′ ∈ φ iff (φ ′ being upward) the source of ↑b ′ is free or auxiliary, and the target of ↑b ′ is principal, iff (ψ being upward) ↑b ′ ∈ ψ. Then define φ ′ (resp. ψ ′ ) as the subpath of φ (resp. ψ) from a (resp. from b ′ ) to b ′ (resp. to c). Remark that φ ′ and ψ ′ share the only wire b ′ , hence they can be composed. Their composition defines an upward path from a to c.

Second, we prove that > α is antisymmetric on upward acyclic α's. Indeed from a > α b and b > α a, one deduces similarly as above an upward cycle crossing a and b. Hence > α is a strict order whenever α has no upward cycles.

At last, > α is well-founded, since α has a finite number of wires.

We now introduce Danos and Regnier's correctness criterion, called switching acyclicity. Actually, the original Danos and Regnier's criterion speaks of switching acyclicity and connectedness, where the sole role of switching connectedness is to invalidate the mix rule (Figure 1(b)) in MLL. However as one extends MLL with multiplicative units or with exponentials, mix-free proofs are not characterized by switching connectedness (see [START_REF] Regnier | Lambda-calcul et réseaux[END_REF]) -indeed, as far as we know, at the time of writing there is no satisfactory correctness criterion corresponding to the mix-free sequent calculus of MLL with units or with exponentials. Moreover mix is accepted by all the denotational semantics we consider, hence we decide to accept it in sequent calculus and to drop switching connectedness from Danos and Regnier's criterion. Definition 2.3 ([7,[START_REF] Ehrhard | Differential interaction nets[END_REF]). A path is switching if it never crosses both premises of a `nor more than one premise of a contraction.

A differential net is switching acyclic whenever each of its simple nets is switching acyclic. A simple net α is switching acyclic if α has no switching cycle and for every box !ρ ∈ Box α, ρ is switching acyclic.

We denote as AC the set of differential nets which are switching acyclic.

A first example of switching cycle is ↑a, ↓b in Figure 4(b). By the way notice that ↑a, ↓b is not upward. An example of a switching acyclic simple net is in Figure 4(a), in particular the cycle ↑a, ↓b is not switching.

As mentioned, switching acyclicity geometrically characterizes those differential nets which correspond to DiLL sequential proofs: this is stated in Theorem 2.4. The proof of Theorem 2.4 consists in a simple generalization of the proof of the corresponding theorem in linear logic (see [START_REF] Girard | Linear logic[END_REF][START_REF] Danos | The structure of multiplicatives[END_REF]). For this reason and since also we do not use Theorem 2.4 to achieve our main results (Theorems 3.3, 4.5), we omit its proof.

Theorem 2.4. For every differential net π, there is a sequent proof P such that Des P = π iff π is switching acyclic.

As an example the reader can check that the switching acyclic simple net in Figure 4(a) is an image of Des, while the switching cyclic simple net in Figure 4(b) is not.

A passage of a path φ through a box !ρ is a pair a, b of wires incident to !ρ such that there is an orientation a of a and an orientation b of b such that a, b is a subsequence of φ. Recall the simple net α in Figure 4(b): the pair a, b is a passage of the path ↑a, ↓b through the box in α. Notice that switching paths can pass through boxes by means of any pair of their incident wires. This means that switching paths enjoy the black-box principle: changing the contents of the boxes in a simple net does not change the switching paths in it. We now set a subclass of switching paths which will be sensitive to the boxes's contents.

Definition 2.5 ([11]

). We define simultaneously the visible passages through a box !ρ with conclusion ↓c and the visible paths in a simple net α. The definition is by induction on the depth of resp. !ρ and α.

A passage a, b through !ρ is visible iff at least one of the followings holds:

1. there is a simple net β ∈ ρ, and a visible path in β from a β to b β , 2. there is a simple net β ∈ ρ, and a visible path in

β from c β to b β , 3. b = c,
where recall that a β (resp. b β , c β ) is the wire of β corresponding to the wire a (resp. b, c) incident to !ρ. A path in α is visible whenever it is switching and every its passage through boxes of α is visible. A differential net is visible-acyclic whenever each of its simple nets is visible-acyclic. A simple net α is visible-acyclic if α has no visible cycle and for every box !ρ ∈ Box α, ρ is visible-acyclic.

? !X ?d ??X ⊥ ⊗ ?!X ⊗ !!X ?d ↑a ?!X !?X ⊥ ↓c ↓b (a) a, b visible, cond 1; ?d ??X ⊥ ⊗ ?!X ⊗ !!X ? ?d ?X ⊥ !X ↑a ↓b !?X ⊥ ?!X ↓c (b) a, b visible, cond. 2; ? ! ?d !X ? ?d ??X ⊥ ?X ⊥ !?X ⊥ ?!X ⊗ !?X ⊥ ⊗ !?X ⊥ ↓a ↑b ↓c (c) b, c visible, cond. 3.
We denote as VAC the set of differential nets which are visible-acyclic.

Clearly switching acyclicity entails visible acyclicity, and visible acyclicity entails upward acyclicity, but the vice versa of each implication does not hold, in general. For example, the simple net in Figure 4 Visible paths introduce two noteworthy novelties with respect to switching paths. First, as above mentioned, visible paths partly break the black-box principle: the visibility of a passage through a box depends on what is inside the box. Changing the contents of a box may alter the visible paths outside it: for example the cycle ↑a, ↓b is visible in Figures 5(a)-(b), but it is not in Figure 4(b), where only the contents of the box change. Second, visibility is sensitive to direction: the passage a, b (resp. b, c ) in Figure 5(b) (resp. Figure 5(c)) is visible, even if its reverse b, a (resp. c, b ) is not. More in general, a path from a wire a to a wire b may be visible, even if the "reverse" path from b to a is not. In Figure 6 we have an example of the role played by directedness in visible acyclicity: the simple net in Figure 6(a) is visiblecyclic, since the cycle ↑b, ↓c, ↑d, ↓a is visible, so being the passages b, c and d, a ; instead the simple net in Figure 6(b) is visible-acyclic, since the cycle ↑b, ↓c, ↑d, ↓a and its reverse ↑a, ↓d, ↑c, ↓b are not visible, each having a nonvisible passage (resp. d, a and c, b ).

Remark that switching and visible acyclicities are totally independent from types. A digression: correctness and visible graphs. It is well known that the notion of correctness graph [START_REF] Danos | The structure of multiplicatives[END_REF] allows to define switching acyclicity in an alternative but equivalent way with respect to Definition 2.3. In this paragraph we present an analogous notion of graphs corresponding to visible acyclicity. In the sake of brevity, the presentation is kept informal and the proofs of Propositions 2.6, 2.7 are omitted; indeed the following results will not be used in the sequel.

⊗ ⊗ ?d !?X ⊗ !!X ⊥ ?!X ⊥ ⊗ ??X ??X ??X ! ?d ? !X ⊥ ?X o u !?X ↓c ↑b ↓a !?X ↑d (a) visible-cyclic; ⊗ ⊗ ?d ! ! !?X ⊗ !!X ⊥ ?!X ⊥ ⊗ ??X ??X ??X ! ?d ? !X ⊥ o u !?X ↓c ↑b ↓a !?X ↑d ?X (b) visible-acyclic.
We start recalling Danos and Regnier's definition of correctness graph. A switching of a cell l is an undirected graph σ l defined following Figure 7: the nodes of σ l are the ports of l and the edges are defined depending on the label of l. In particular, notice that pars (resp. n-contractions, for n ≥ 2) have two (resp. n) possible switchings. Observe also that the switchings of boxes are independent from their contents: once again the black-box principle.

A correctness graph of a differential net π is a correctness graph of one of its simple nets; a correctness graph of a simple net α is an undirected graph σ α having as nodes the ports of α and as edges the wires of α plus the edges obtained substituting every cell with one among its switchings. Clearly if α has p pars and k contractions not weakening of arity resp. n 1 + 1, . . . , n k + 1, then α has 2 p k i=1 n i correctness graphs -a number exponential in the size of α. The reader can easily check that the switching cycles in a simple net α exactly correspond to the cycles in a correctness graph of α, and vice versa. Hence: Proposition 2.6. Let π be a differential net, π is switching acyclic with respect to Definition 2.3 iff every correctness graph of π is an acyclic graph and for every !ρ ∈ Box π, ρ is switching acyclic.

It should be mentioned that an easy extension of a result by Guerrini [START_REF] Guerrini | Correctness of multiplicative proof nets is linear[END_REF] shows that the switching acyclicity of a differential net can be decided in linear time with respect to its size, even if the number of its correctness graphs is exponential.

What about visible acyclicity? We define visible graphs, and we state they are the graphs covered by visible paths (Proposition 2.7). Visible graphs are obtained like the correctness ones, by substituting every cell with one among its switchings. What changes is the switching associated with boxes, which we call visible switching to differ it from that of Figure 7. The visible switchings associated with a box !ρ are defined recursively, supposing we already know the visible graphs of the contents ρ; these switchings introduce some edges which are directed.

` → or ?w → ? 1 n • • • → i 1 n • • • • • • for an i ≤ n ⊗ → !w → ! 1 n • • • → • • • 1 n ?d → !d → !ρ 1 n • • • → • • • 1 n
A visible graph of a differential net is a visible graph of one of its simple nets; a visible graph of a simple net α of depth 0 is a switching graph of α; a visible graph of a simple net α of depth d + 1 is a directed graph σ α having among its nodes the ports of α and among its edges the wires of α, intended as non-oriented edges (i.e. edges that can be crossed in whatever direction), in addition σ α has the nodes and edges obtained substituting every cell except boxes with one among its switchings, and every box with one among its visible switchings; at last, the visible switchings of a box !ρ are defined as follows. Let p 0 , p 1 , . . . , p n be the ports of !ρ, p 0 being the principal one. If ρ = 0 then !ρ has one visible switching, which is a directed version of the usual switching for boxes:

!0 p 1 p n • • • p 0 → p 1 p n • • • p 0
If ρ = 0, then choose β 1 , . . . , β n visible graphs (with possible repetitions) associated with ρ, where n is the number of auxiliary ports of !ρ. For each i, j ≤ n, call q j i the node of β j corresponding to p i . Choose also i 1 , . . . , i n ∈ {0, . . . , n}.

These choices define the following visible switching:

!ρ p 1 p n • • • p 0 → p 1 p n • • • • • • p 0 • • • • • • • • • q n n q n 1 • • • q 1 n q 1 1 q 1 0 q n 0 q 0 0 i n 1 n 0 1 n 0 i 1 • • • β 1 β n
where p j , for j ∈ {1, . . . , n}, is connected with q 0 0 if i j = 0, else it is connected with q i ij . Notice that the edges between the p j 's and q 0 0 are downward directed, hence a visible switching of !ρ is a directed graph.

Counting the number of visible graphs of a simple net is more complicated than for switching graphs, since this number depends on the contents of the boxes in the simple net. In fact, consider a box !ρ with n auxiliary ports and such that ρ = 0. Suppose we know that ρ has a number v of visible graphs, then the number of possible visible switchings of !ρ is (n + 1) n v+n-1 n , where the binomial coefficient v+n-1 n denotes the number of multisets of cardinality n, with elements taken from a finite set of cardinality v [START_REF] Stanley | Enumerative Combinatorics[END_REF]. In our case v+n-1 n denotes the number of different choices of the multiset [β 1 , . . . , β n ], while (n+1) n is the number of different choices of the sequence i 1 , . . . , i n . This means that the number of visible graphs of a simple net α is a tower of exponentials whose height depends on the depth of α -much more than the number of its correctness graphs! Proposition 2.7. Let π be a differential net, π is visible-acyclic with respect to Definition 2.5 iff every visible graph of π is a directed acyclic graph.

It might be interesting knowing whether there is a linear algorithm deciding the visible acyclicity of differential nets, as it is for switching acyclicity, in spite of the huge difference between the numbers of correctness and visible graphs.

Values. We now introduce our notion of value (Definition 2.8), which will be used to state Theorem 4.5. One would like to define a value simply as a cut-free differential net, but this is not enough to achieve Theorem 4.5 (see the discussion on the simple nets in Figure 13). Indeed we need to rule out also upward cycles and weak wires, these last ones defined down here.

A weak wire is a wire a having one orientation a such that one of the followings holds:

• a is conclusion of a weakening and premise of a contraction, or

• a is premise of a box !ρ and for every β ∈ ρ, a β is conclusion of a weakening.

?

• • • • • • ? → • • • ? α∈π • • • α ? • • • → α∈π ? • • • • • • α Figure 8
: elementary steps of the elimination of weak wires: in the step pictured at left, the contraction in the reduct which comes out to have 2 ports is a convention to denote a single connecting wire.

The differential nets having no weak wire and recursively having no box with weak wires in its contents, are exactly the normal forms of the reduction defined by the elementary steps depicted in Figure 8. Such a reduction has been considered also in [START_REF] Pagani | The conservation theorem for differential nets[END_REF]. None of the simple nets depicted up to now have weak wires. Figure 13 shows examples where they are present. Definition 2.8. A differential net is a value if each of its simple nets is a value. A simple net α is a value, if the following holds:

1. α has no cut and no weak wire, 2. α has no upward cycle, 3. for every box !ρ ∈ Box α, ρ is a value.

Finiteness spaces

Finiteness spaces. In the purely relational model of linear logic, formulas are interpreted as sets and nets as relations between these sets. Multiplicative connectives are interpreted as cartesian products and exponentials as the operation which maps a set X to the set M f in (X) of finite multisets with support in X. Finiteness spaces are obtained adding to the relational model a notion of "finitary" relation satisfying a closure condition. This condition is based on an algebraic duality, modelling linear negation.

Let X be a set and F ⊆ P(X), we define the dual of F , denoted F ⊥ , as the set

F ⊥ := {u ′ ⊆ X ; ∀u ∈ F, u ∩ u ′ is finite} ⊆ P(X).
Notice that F ⊥ contains every finite subset of X, and it is closed downward (that is, if v ⊆ u ′ ∈ F ⊥ , then v ∈ F ⊥ ) and under finite unions. Moreover, we have the usual properties of duality:

• if F ⊆ G, then G ⊥ ⊆ F ⊥ , • F ⊆ F ⊥⊥ , • F ⊥⊥⊥ = F ⊥ .
Definition 2.9 ([16]). A finiteness space X is given by a pair |X |, F (X ) , where |X | is a set called the web of X , and F (X ) is a subset of P(|X |) satisfying F (X ) ⊥⊥ = F (X ). The elements of F (X ) are called the finitary sets of X . We denote by F ∞ (X ) the set of infinite finitary sets of X . We write finiteness spaces by calligraphic capitals X , Y . . .

Notice that u ∈ F (X ) ∩ F (X ) ⊥ iff u is finite; in particular u ∈ F ∞ (X ) entails u / ∈ F (X ) ⊥ ; we have also that u ∈ F (X ) ⊥ iff ∀v ⊆ u, v / ∈ F ∞ (X )
. We associate with linear negation and with positive connectives (⊗, !) a corresponding operation on finiteness spaces.

Negation: |X ⊥ | := |X |, F (X ⊥ ) := F (X ) ⊥ . Tensor: |X ⊗ Y| := |X | × |Y|, F (X ⊗ Y) := {u × v ; u ∈ F (X ), v ∈ F (Y)} ⊥⊥ . Of course: |!X | := M f in (|X |), F (!X ) := {M f in (u) ; u ∈ F (X )} ⊥⊥ .
Let X be a set and suppose w ∈ P(M f in (X)), we define the global support of w, denoted supp(w), as the set µ∈w supp(µ), which is an element of P(X).

Through De Morgan laws we derive also the operations associated with negative connectives: X `Y := (X ⊥ ⊗ Y ⊥ ) ⊥ , and ?X := (!X ⊥ ) ⊥ .

By means of these operations we can associate a finiteness space A X with any MELL formula A and any finiteness space X , called the X interpretation of A. The definition is by induction on deg A:

X X := X , X ⊥ X := X ⊥ , A ⊗ B X := A X ⊗ B X , A `B X := A X ` B X , !A X := ! A X , ?A X := ? A X .
Remark that by definition A ⊥ X = A ⊥ X . We set the interpretation of a sequent Γ = A 1 , . . . , A n as Γ X := ˙n i=1 A i X , we disregard any problem of bracketing, and consider the web of Γ X as made up of n-tuples. Notice that Γ

⊥ X = n i=1 A ⊥ i X .
Properties of finiteness spaces. We present some results on finiteness spaces useful in the sequel. Except for Lemma 2.13, these results come from [START_REF] Ehrhard | Finiteness spaces[END_REF], so we omit their proofs.

Lemma 2.10 ([16]

). Let w ⊆ |X ⊗Y|. One has w ∈ F (X ⊗Y) iff p 1 (w) ∈ F (X ) and p 2 (w) ∈ F (Y).

The next lemma is expressed in [START_REF] Ehrhard | Finiteness spaces[END_REF] by using the linear implication ⊸ instead of `. One gets the original statement by setting X ⊸ Y := X ⊥ `Y. Lemma 2.11 (From [START_REF] Ehrhard | Finiteness spaces[END_REF]). Let w ⊆ |X `Y|. One has w ∈ F (X `Y) iff the two following conditions hold: For the following lemma we recall that supp(w) denotes the global support of w. Lemma 2.12 ( [START_REF] Ehrhard | Finiteness spaces[END_REF]). Let w ⊆ |!X |. One has w ∈ F (!X ) iff supp(w) ∈ F (X ). Lemma 2.13. Consider a finiteness space !X , n ≥ 1 indexed sets

u 1 := {µ 1 i } i∈I , . . . , u n := {µ n i } i∈I ⊆ |!X |,
and the set

w := n j=1 µ j i i∈I
.

The following properties hold:

∀j ≤ n, u j ∈ F (!X ) ⇐⇒ w ∈ F (!X ) (5) ∃j ≤ n, ∃u ′ ⊆ u j , u ′ ∈ F ∞ (?X ) ⇐⇒ ∃w ′ ⊆ w, w ′ ∈ F ∞ (?X ) (6) ∃j ≤ n, u j infinite ⇐⇒ w infinite (7) ∀j ≤ n, u j ∈ F (?X ) =⇒ w ∈ F (?X ) (8)
Proof. [START_REF] Berry | Stable models of typed lambda-calculi[END_REF]. ∀j ≤ n, u j ∈ F (!X ) iff (by Lemma 2.12) ∀j ≤ n, supp(u j ) ∈ F (X ) iff (by finite union closure) n j=1 supp(u j ) = supp(w) ∈ F (X ) iff (again by Lemma 2.12) w ∈ F (!X ). [START_REF] Girard | The system F of variable types, fifteen years later[END_REF]. It is equivalent to property [START_REF] Berry | Stable models of typed lambda-calculi[END_REF], since by definition of finitary relation w ∈ F (!X ) iff ∀w ′ ⊆ w, w ′ / ∈ F ∞ (?X ⊥ ). [START_REF] Danos | The structure of multiplicatives[END_REF]. Define an equivalence relation on n-tuples of finite multisets:

η 1 , . . . , η n ∼ ǫ 1 , . . . , ǫ n iff n j=1 η j = n j=1 ǫ j
Now, consider the set u of all n-tuples µ 1 i , . . . , µ n i with i ∈ I. Since the multisets are finite, all equivalence classes of u are finite, thus we obtain: there are finitely many classes in u (i.e. w is finite) iff u is finite iff all projections u j = {µ j i } i∈I are finite (none of them is empty). ( 8). Suppose w / ∈ F (?X ), then there is

I ′ ⊆ I s.t. { n j=1 µ j i } i∈I ′ ∈ F ∞ (!X ⊥ )
. By [START_REF] Berry | Stable models of typed lambda-calculi[END_REF] we have ∀j ≤ n, {µ j i } i∈I ′ ∈ F (!X ⊥ ), and by [START_REF] Danos | The structure of multiplicatives[END_REF] there is j ≤ n such that {µ j i } i∈I ′ is infinite. We conclude that there is j ≤ n such that u j / ∈ F (?X ).

Notice that the converse of property (8) does not hold. For an example, consider a finiteness space X with {x i } i∈N ∈ F ∞ (X ) and {y i } i∈N ∈ F ∞ (X ) ⊥ : define u := {[x i ]} i∈N and v := {[y i ]} i∈N , and w := {[x i , y i ]} i∈N . Clearly v / ∈ F (?X ), since it is an infinite set of F ∞ (!X ⊥ ) (by Lemma 2.12), nevertheless we have w ∈ F (?X ), since there is no infinite w ′ ⊆ w belonging to F ∞ (!X ⊥ ) (in fact if w ′ is infinite, then supp(w ′ ) / ∈ F (X ⊥ ) because of its x i 's elements, and this prevents w ′ to be in F (!X ⊥ ) (Lemma 2.12)). Experiments. We define the interpretation of nets using the notion of experiment. Experiments were developed by Girard in [START_REF] Girard | Linear logic[END_REF] to give a way to directly interpret multiplicative linear logic proof nets in coherent semantics, without passing through sequent calculus. The following definition extends experiments to differential nets: Definition 2.14 (From [START_REF] Girard | Linear logic[END_REF]). Suppose an interpretation X of the variable X. An experiment e on a differential net π, denoted e : π, is an experiment on one of π's simple nets. An experiment e on a simple net α is a function which associates with every box !ρ ∈ Box α a multiset [e 1 , ..., e k ], for k ≤ 0, of experiments on ρ, and with every wire a of α an element of | A X | = | A ⊥ X |, where A, A ⊥ are the pair of dual types associated with a. We require moreover that e satisfies the following conditions (see Fig. • if a is the conclusion of a !/?-cell with auxiliary ports b 1 , . . . , b n (n ≥ 0), then e(a) = i≤n e(b i ); in particular if a is the conclusion of a (co)weakening, then e(a) = 0;

ρ ′ j + ?d x [x] i≤n µ i µ 1 ? • • • µn !d x [x] i≤n µ i µ 1 ! • • • µn
• if a is incident to a box !ρ, let e(!ρ) = [e ρ
1 , . . . , e ρ k ] (k ≥ 0), and for every j ≤ k let α j be the simple net of ρ on which e ρ j is defined. We denote by a αj the wire of α j associated with a. If a is the conclusion of !ρ, then e(a) = j≤k e ρ j (a αj ) ; if a is a premise of !ρ, then e(a) = j≤k e ρ j (a αj ). If a 1 : A 1 , . . . , a n : A n is the interface of α, then the result of e, denoted by e(α), is the element e(a 1 ), . . . , e(a n ) of | ˙n i=1 A i X |.

The interpretation of a differential net is the union of the interpretations of its simple nets; the interpretation of a simple net is the set of the results

? ?d X ?d X !X !X ↓a ↑b
(a) Montelatici's fixed point operator applied to identity [START_REF] Montelatici | Polarized proof nets with cycles and fixpoints semantics[END_REF]. Obviously the interpretation of the empty sum is the empty set. Notice that the empty sum is actually the only value interpreted by the empty set. Defining an experiment e on a value π is in fact easy: one has to declare the values of e on axioms and, inductively, on boxes, then e is univocally extended to all wires of π by using the conditions of Definition 2.14. In presence of cuts or upward cycles, the existence of experiments on π might be a tough problem: indeed this problem is strictly related to the cut-elimination of π, as showed in [START_REF] Carvalho | A semantic measure of the execution time in linear logic[END_REF] in the framework of pure nets.

? ⊗ !X ?X ⊥ `!X ?d X !X !X ⊗ ?X ⊥
For an example of a net with cuts and with empty interpretation, consider the simple net γ depicted in Figure 10(a). This example is taken from Montelatici's [START_REF] Montelatici | Polarized proof nets with cycles and fixpoints semantics[END_REF], where the author shows how one can use switching -we would say visible -cycles to define a fixed point operator. In particular, the simple net γ corresponds to such an operator applied to the identity, and indeed γ reduces to itself. We will discuss the cut-elimination of γ in [START_REF] Pagani | Visible acyclic differential nets -Part II: interaction[END_REF], here let us argue that the interpretation γ X is empty, for any X . Suppose by absurdum that there is x ∈ γ X , then there is an experiment e : γ with result x; by Def. 2.14 we should have that e(a) = e(b) + [x], and by the contents of the box of γ that e(a) = e(b), i.e. a contradiction. We conclude that γ X is empty. Consider now the simple values α and β in Figure 10(b). Notice that a cut between α and β reduces to γ. However, α and β have non-empty interpretations, being values. Indeed:

α X = { µ, µ ; µ ∈ |!X |}, β X = { µ, µ + [x] , x ; µ ∈ |!X |, x ∈ |X |}.
As a simple consequence of Lemma 2.11, α X is a finitary set of ?X ⊥ `!X ; we now prove that β X is not finitary in (!X ⊗ ?X ⊥ ) `X whenever there is

x ∈ |X |. Indeed we claim u = { µ, µ + [x] , x ; µ ∈ M f in ({x})} ∈ F ∞ ((?X ⊥ `!X ) ⊗ X ⊥ ), from which we conclude β X / ∈ F ((!X ⊗ ?X ⊥ ) `X ), since u ⊆ β X .
The claim follows from Lemma 2.10 and the facts that

p 1 (u) = { µ, µ + [x] ; µ ∈ M f in ({x})} ∈ F ∞ (?X ⊥ `!X ) and p 2 (u) = {x} ∈ F (X ⊥ ).
While the latter is trivial, the first fact is due to the infinity of M f in ({x}) and Lemmas 2.11, 2.12: suppose v ∈ F (!X ), then

p 1 (u)(v) = {µ + [x] ; µ ∈ M f in ({x}) ∩ v} ∈ F (!X ) by the downward closure of F (!X ) (notice that {µ + [x] ; µ ∈ M f in ({x})} ⊂ M f in ({x}) ∈ F (!X ) by Lemma 2.12); dually, suppose v ∈ F (?X ⊥ ), then p 1 (u) ⊥ (v) = {µ ∈ M f in ({x}) ; µ + [x] ∈ v} is finite (in fact M f in ({x}) ∩ v is finite), so it belongs to F (?X ⊥ ).
We will see in [START_REF] Pagani | Visible acyclic differential nets -Part II: interaction[END_REF] that Figure 10 yields a particular example of a very general property of finiteness spaces: whenever a cut between two values (here α and β of Figure 10(b)) is not normalizing, at least one of the two values has not a finitary interpretation.

Let us change example: consider the simple net α in Figure 4(b), and let Γ be its sequent conclusion ?!X ⊥ ⊗ ??X, !?X ⊥ . As previously discussed, α is visible-acyclic but not switching acyclic. Let us prove that α X is a finitary set of Γ X . We have:

α X = { n [0] , n [0] , n [0] ; n ∈ N}.
Notice supp({n [0]} n∈N ) = {0}, hence by Lemma 2.12 we have {n [0]} n∈N finitary in !?X ⊥ X . We use Lemma 2.11 to deduce α X ∈ Γ X . For every set of indexes I ⊆ N, we clearly have α

X ({ n [0] , n [0] } n∈I ) = {n [0]} n∈I ∈ F ( !?X ⊥ X ); conversely, if one has {n [0]} n∈I ∈ F ( !?X ⊥ X ) ⊥ , then I is finite, so is α ⊥ X ({n [0]} n∈I ) = { n [0] , n [0] } n∈I , hence α ⊥ X ({n [0]} n∈I ) ∈ F ( ?!X ⊥ ⊗ ??X X ). We conclude α X ∈ Γ X .
Let us compare the previous example with the simple value β of Figure 5(c): α and β look similar, however they behave quite differently. We noticed that β is visible-cyclic, let us prove β X is not finitary in Γ ′ X , where Γ ′ is the sequent conclusion ??X ⊥ , ?!X ⊗ !?X ⊥ of β. We have:

β X = { n [0] , n [0] , n [0] ; n ∈ N}.
Similarly to how we argued in the previous case, Lemma 2.12 entails that the set {n [0]} n∈N is finitary in !!X X as well as in !?X ⊥ X , in particular we have

{n [0]} n∈N / ∈ F ( ?!X X ). Then by Lemma 2.10, { n [0] , n [0] } n∈N / ∈ F ( ?!X ⊗ !?X ⊥ X ). So we have β X ({n [0]} n∈N ) = { n [0] , n [0] } n∈N / ∈ F ( ?!X X ), even if {n [0]} n∈N ∈ F ( ??X ⊥ ⊥ X ). We conclude β X / ∈ F ( Γ ′ X
) by Lemma 2.11. Notice the difference with respect to the previous case: the tensor between ?!X and !?X ⊥ "neutralizes" the finiteness of {n[0]} n∈N in !?X ⊥ , which is at the base of the finiteness of α X .

The simple net in Figure 4(a) requires a subtler discussion which will be done in the next Section 3. Consider instead the other examples of visible cyclicity in Figure 5. Call γ and δ the simple values respectively in the subfigures 5(a), 5(b), and let Γ be their sequent conclusion ??X ⊥ ⊗ ?!X, !?X ⊥ . We prove that the interpretations of γ and δ are not finitary in Γ X , for a suitable X . We have:

γ X = { µ, µ , n [0] ; µ ∈ M f in (M f in (|X |)) and n = card µ}, δ X = { n [0] , µ , µ ; µ ∈ M f in (M f in (|X |)) and n = card µ}.
Let us start with γ: suppose {η i } i∈I is an infinite set finitary in !X X , for example choose η i = i [0], I infinite set of integers. By Lemma 2.12,

{[η i ]} i∈I ∈ F ∞ (!!X ) and thus {[η i ]} i∈I / ∈ F (??X ⊥ ). By Lemma 2.10, { [η i ] , [η i ] } i∈I / ∈ F (??X ⊥ ⊗ ?!X ), and by downward closure, { [η] , [η] ; η ∈ M f in (|X |)} / ∈ F (??X ⊥ ⊗ ?!X ). This means γ ⊥ X ({[0]}) = { [η] , [η] ; η ∈ M f in (|X |)} / ∈ F (??X ⊥ ⊗ ?!X ), even if clearly {[0]} ∈ F (!?X ⊥ ) ⊥ ,
being a singleton. We conclude γ X is not finitary in Γ X by Lemma 2.11.

In case of the simple value δ of Fig. 5(b) the choice of the infinite set finitary in !X X must be subtler: we start from (x i ) i∈I an infinite injective family such that the set {x i } i∈I of its values is finitary in X . We then consider {[x i ]} i∈I , which is in F ∞ ( !X X ) by Lemma 2.12. Notice there are finiteness spaces for which such a family (x i ) i∈I does not exist, as every space having finite web, however what we want to prove is that γ X is not finitary for a well-chosen X , and not for every finiteness space. This is in accordance with Theorem 4.5, and it explains why we have omitted the multiplicative units, which would have introduced formulas whose interpretation has finite web.

Suppose I to be a set of integers, and define u as

{ i [0] , i [[x i ]] , i [[x i ]] } i∈I . Notice that u ⊆ γ X . We prove that u / ∈ F ( Γ X ), hence also β X / ∈ F ( Γ X ) by downward closure.
First, we claim that {i [[x i ]]} i∈I ∈ F (?!X ) = F (!?X ⊥ ) ⊥ . In fact, for any subset v ⊆ {i [[x i ]]} i∈I , we prove v / ∈ F ∞ (!?X ⊥ ). By contradiction, suppose v ∈ F ∞ (!?X ⊥ ), then supp v ∈ F ∞ (?X ⊥ ) by Lemma 2.12 and by the fact that the injectivity of the family (x i ) i∈I and the supposed infinity of v imply the infinity of supp v. Then we have a contradiction, since supp v is an infinite

subset of {[x i ]} i∈I ∈ F (!X ).
Second, notice that {i [0]} i∈I ∈ F ∞ (!!X ) by Lemma 2.12, hence it does not belong to F (??X ⊥ ), so

{ i [0] , i [[x i ]] } i∈I /
∈ F (??X ⊥ ⊗ ?!X ) by Lemma 2.10. We conclude u / ∈ F ( Γ X ) by Lemma 2.11, since

u ⊥ ({i [[x i ]]} i∈I ) = { i [0] , i [[x i ]] } i∈I / ∈ F (??X ⊥ ⊗ ?!X )
Definition 2.15. A differential net π with sequent conclusion Γ is finitary, if for every finiteness space X , π X is a finitary set of Γ X . We denote as FIN the set of differential nets which are finitary.

It seems from Definition 2.15 that to decide whether a differential net π is finitary we need to check π X for every X . Actually, a notable corollary of our results will be that whenever π is a value, π is finitary iff π X ∈ F (X ), for any finiteness space X with both F ∞ (X ) and F ∞ (X ⊥ ) not empty (Corollary 4.6).

Visible acyclicity ⇒ finiteness

In this section we prove the soundness theorem: every visible-acyclic differential net is finitary (Theorem 3.3). This result extends Girard's soundness theorem for linear logic: every proof-net (i.e. switching acyclic proof-structure) is a clique in coherence spaces [START_REF] Girard | Linear logic[END_REF]. As the reader will notice, such an extension is very close, in the sense that our proof of Theorem 3.3 generalizes the technique developed by Girard in the so-called Compatibility Lemma [START_REF] Girard | Linear logic[END_REF]. Precisely, Theorem 3.3 is based on Lemma 3.2, this last one taking origin in Girard's Compatibility Lemma (see also [START_REF] Pagani | Acyclicity and Coherence in Multiplicative and Exponential Linear Logic[END_REF]). Let us see an example showing the main ideas behind the proof of Theorem 3.3. Consider the simple net α in Figure 4(a). We have:

α X = n j=1 µ j , n j=1 [µ j ] , n j=1 ν j , n j=1 [ν j ] ; n ∈ N, µ j , ν j ∈ M f in (|X |) .
Since α is visible-acyclic, α X should be a finitary set of Γ X , where Γ = ?X ⊥ `?!X, ?X ⊥ , !!X is the sequent conclusion of α. Let us prove it by showing that for every u ⊆ α X , u ∈ F ( Γ ⊥ X ) implies that u is finite. Assume there is a family (e i ) i∈N of experiments over α such that {e i (α)} i∈N ∈ F ( Γ ⊥ X ), we argue that {e i (α)} i∈N is finite. By {e i (α)} i∈N ∈ F ( Γ ⊥ X ) and Lemma 2.10, we have

{e i (a)} i∈N := ni j=1 µ j i i∈N ∈ F (!X ), (9)
{e i (b)} i∈N := ni j=1 [µ j i ] i∈N ∈ F (!?X ⊥ ), ( 10
)
{e i (d)} i∈N := ni j=1 ν j i i∈N ∈ F (!X ), ( 11
)
{e i (c)} i∈N := ni j=1 [ν j i ] i∈N ∈ F (??X ⊥ ). ( 12
)
We prove that all the above four sets are finite, so concluding {e i (α)} i∈N finite. Suppose {e i (c)} i∈N is infinite, then {e i (c)} i∈N / ∈ F (!!X ), hence by Lemma 2.12, i∈N supp(supp(e i (c))) = i∈N supp(e i (d)) / ∈ F (X ), and so {e i (d)} i∈N / ∈ F (!X ), which contradicts claim [START_REF] Pagani | Acyclicity and Coherence in Multiplicative and Exponential Linear Logic[END_REF]. We conclude that {e i (c)} i∈N is finite. Notice that this argumentation "draws" in α the visible path ↑c, ↓d , in the precise sense that it deals with the values of (e i ) i∈N first on c and then on d. As for the wire d: if {e i (d)} i∈N were infinite, then {e i (c)} i∈N would be infinite too, contrary to what we have proven. This argumentation draws the visible path ↑d, ↓c .

Suppose {e i (a)} i∈N is infinite, then we split in two cases, depending whether the sequence of n i 's increases arbitrarily. In case for every i there is a j such that n i < n j , then {e i (c)} i∈N is infinite: this clashes either with claim [START_REF] Pagani | Acyclicity and Coherence in Multiplicative and Exponential Linear Logic[END_REF] or with claim (12), as we argued before. This reasoning follows the path ↑a, ↓c or the path ↑a, ↓d , in both cases visible. In case the sequence of n i 's has a max m, then by Lemma 2.13.( 7) and the supposed infinity of {e i (a)} i∈N , there is a j ≤ m such that the set {µ j i } i∈N is infinite, where we consider µ j i = 0 whenever j > n i . We then deduce {µ j i } i∈N ∈ F ∞ (!X ) (Lemma 2.13.( 5)), and thereafter i∈N supp(e i (b)) / ∈ F (?X ⊥ ), since it contains the infinite subset {µ j i } i∈N . By Lemma 2.12, we infer a contradiction with claim [START_REF] Tranquilli | A characterization of hypercoherent semantic correctness in multiplicative additive linear logic[END_REF]. Notice this argumentation follows the path ↑a, ↓b . In a symmetric way, one argues that {e i (b)} i∈N is finite.

We conclude that every family (e i ) i∈N of α's experiments whose set of results is finitary in Γ ⊥ X should be finite. So α X is a finitary set of Γ X . We have underlined that every case in the above argumentation draws a path in α which is visible. This is the key which makes the proof of Theorem 3.3 work: following the values of a family of α's experiments draws a visible path in α and this always succeed in proving that the set of the results of such experiments is finitary, since this this path cannot be a cycle, α being visible-acyclic by hypothesis. This technique is developed in Lemma 3.2.

We recall that a family (x i ) i∈I is injective whenever for every i, i ′ ∈ I, i = i ′ implies x i = x i ′ . As an immediate application of the axiom of choice we have: Fact 3.1. For every indexed family (x i ) i∈I :

1. there is I ′ ⊆ I s.t. (x i ) i∈I ′ is injective and {x i } i∈I ′ = {x i } i∈I ; 2. if (x i ) i∈I is injective, then for every subset I ′ ⊆ I, (x i ) i∈I ′ is injective; 3. if (x i ) i∈I is injective and I is infinite, then {x i } i∈I is infinite.
Lemma 3.2 (Key lemma). Consider a visible-acyclic simple net α, a finiteness space X , a family (e i ) i∈I of experiments on α, and a conclusion ↓a : A of α.

If {e i (a)} i∈I ∈ F ∞ ( A ⊥ X ), then there is a subset I ′ ⊆ I and a visible path φ in α starting from ↑a : A ⊥ and ending in a conclusion of α such that:

1. for every oriented wire c :

C crossed by φ, {e i (c)} i∈I ′ ∈ F ∞ ( C X ).
Proof. The proof is by induction on the depth of α.

We define a procedure giving a sequence of visible paths φ 0 ⊂ φ 1 ⊂ . . . and a sequence of infinite subsets I ⊇ I 0 ⊇ I 1 ⊇ . . . , s.t. φ 0 =↑a, and for each φ j , I j (j ≥ 0), for every oriented wire c : C crossed by φ j , the following holds:

1. {e i (c)} i∈Ij ∈ F ∞ ( C X ); 2. (e i (c)) i∈Ij is injective.
Since α is finite and visible-acyclic, this sequence eventually stops with a visible path φ k ending in a conclusion of α: the pair φ k , I k then satisfies condition 1 of the lemma.

Before showing this procedure, let us note that:

( * ) both properties 1 and 2 hold for every infinite subset I ′ ⊆ I j This is due to the injectivity of (e i (c)) i∈Ij : if (e i (c)) i∈Ij is injective, then so (e i (c)) i∈I ′ is (Fact 3.1); as for property 1, if

{e i (c)} i∈Ij ∈ F ∞ ( C X ), then by downward closure {e i (c)} i∈I ′ ∈ F ( C X ) and by Fact 3.1, {e i (c)} i∈I ′ is infinite.
As written above, we define φ 0 =↑a; as for I 0 : since by hypothesis {e i (a)} i∈I ∈ F ∞ ( A ⊥ X ), we deduce that there is an infinite subset (e i (a)) i∈I ′ is injective and {e i (a)} i∈I = {e i (a)} i∈I ′ (Fact 3.1): we then set

I ′ ⊆ I, such that D • • • C φ j l ↓c ↓d (a) cases 1 and 2 !E ?F ?F β !B • • • !B • • • β ∈ ρ φ j ↓c ↑b ↑b ′ ↓c ′ ↓d ′ ↓d E (b) subcase 2.3 • • • D l C φ j ↑d ↓c (c) case 3
I 0 = I ′ .
Let us now define φ j+1 , I j+1 from φ j , I j , where φ j is supposed visible and φ j , I j are supposed satisfying the above conditions 1 and 2. Let ↓c : C be the last oriented wire crossed by φ j (we denote by ↓c the last oriented wire crossed by φ j , but we could have denoted it indifferently by ↑c), and let p be the port target of ↓ c. If ↓ c is a conclusion of α (i.e. p is a free port of α), then the procedure stops: we set φ = φ j and I ′ = I j . Otherwise, p is a port of a cell l, we then split in three cases: case 1, ↓c is premise of l (i.e. p is auxiliary), and, set ↓d : D the conclusion of l, {e i (d)} i∈Ij ∈ F ∞ ( D X ); case 2, ↓c is premise of l, and {e i (d)} i∈Ij / ∈ F ∞ ( D X ); case 3, ↑c is conclusion of l (i.e. p is principal).

Case 1 (↓c premise of l, conclusion of l in F ∞ ). Suppose ↓c is premise of a cell l, having ↓d : D as conclusion (see Fig. 11(a)), and suppose

{e i (d)} i∈Ij ∈ F ∞ ( D X ).
First, we show that d / ∈ φ j . By condition 1 on φ j , I j , we know that ↑d / ∈ φ j . As for ↓d, we argue using α's visible acyclicity: if ↓d ∈ φ j , then φ j = φ ′ j • φ ′′ j , with φ ′ j (resp. φ ′′ j ) ending in ↓d (resp. ↓c) and φ ′′ j starting in ↓d; then φ ′′ j would be a visible cycle, violating the hypothesis of α visible-acyclic.

Second, since I j is infinite, then there is an infinite subset

I ′ ⊆ I j , such that (e i (d)) i∈I ′ is injective and {e i (d)} i∈I ′ = {e i (d)} i∈Ij (Fact 3.1).
Then, we set φ j+1 := φ j • ↓d and I j+1 := I ′ . Clearly φ j+1 , I j+1 meet both conditions 1 and 2 (recall the remark ( * )).

The proof of this case is not yet finished, since we need to check the visibility of φ j+1 . If l is a box, then clearly the passage c, d added to φ j+1 is visible, ↓d being the conclusion of l13 . It remains to check that φ j+1 is switching. Indeed, the only case in which φ j+1 might miss to be switching is because ↓d is a premise of a `/?-cell r already crossed by φ j : we prove that this case violates either the hypothesis {e i (d)} i∈Ij ∈ F ∞ ( D X ) or α's visible acyclicity.

? ?B l φ j ?B • • • φ j ? ?B φ j l φ j ?B • • • ↓ c ↓b • • • • • • ↓a i ↓ c ↓a i • • • ↓b • • • ↓d ↓d ?B ?B
Figure 12: proof that φ j+1 does not violate switching acyclicity.

We suppose r is a ?-cell (the `-cell case is an easy variant): this means D = ?B for a suitable formula B. Let ↓ b :?B be the conclusion of r and ↓a 1 : ?B, . . . , ↓a m : ?B, for m ≥ 1, be the premises of r different from ↓d. The path φ j can cross r either from ↑b to ↑a i (see at left of Fig. 12), or from ↓a i to ↓ b (at right of Figure 12), for an i ≤ m. In case ↑ b ∈ φ j , then by condition 1, we know that {e i (b)} i∈Ij ∈ F ∞ ( !B ⊥ X ), hence by Lemma 2.13.( 5) we have {e

i (d)} i∈Ij ∈ F ∞ ( !B ⊥ X ), which contradicts the hypothesis {e i (d)} i∈Ij ∈ F ∞ ( D X ) = F ∞ ( ?B X ). In case ↓b ∈ φ j , then φ j = φ ′ j • φ ′′ j , with φ ′ j (resp. φ ′′ j )
ending in ↓b (resp. ↓c) and φ ′′ j starting in ↓b; then ↓d, ↓b • φ ′′ j is a visible cycle, violating the hypothesis of α visible-acyclic.

Case 2 (↓c premise of l, conclusion of l not in F ∞ ). As before, suppose ↓c is premise of a cell l, having ↓ d : D as conclusion (see Fig. 11(a)), but now let {e i (d)} i∈Ij / ∈ F ∞ ( D X ). This case is subtle and it deserves more attention. We start by proving that under these assumptions l is either a ⊗-cell or a !-cell or a box. Indeed, l cannot be a (co)weakening, because it has at least one premise, ↓c; l cannot be a (co)dereliction, otherwise the hypothesis {e

i (c)} i∈Ij ∈ F ∞ ( C X ) would entail {e i (d)} i∈Ij = {[e i (c)]} i∈Ij ∈ F ∞ ( D X ).
As for `/?-cells: suppose l is a ?-cell and let us prove a contradiction (the `case is an easy variant). In this case we have C, D = ?B for a suitable formula B. At first notice that {e i (d)} i∈Ij is infinite, since {e i (c)} i∈Ij is infinite (use Lemma 2.13.( 7)). This means that {e

i (d)} i∈Ij / ∈ F ∞ ( D X ) implies {e i (d)} i∈Ij / ∈ F ( D X ): i.e. there is a subset I ′ ⊆ I j , such that {e i (d)} i∈I ′ ∈ F ∞ ( !B ⊥ X )
, in particular notice that I ′ must be infinite. We deduce by Lemma 2.13.(5) (use Lemma 2.10 in the `case) that {e i (c)} i∈I ′ ∈ F ( !B ⊥ X ). Last step: the injectivity of (e i (c)) i∈I ′ (condition 2 and Fact 3.1) and the hypothesis that

I ′ is infinite imply that {e i (c)} i∈I ′ is infinite, so violating the hypothesis {e i (c)} i∈Ij ∈ F ∞ ( ?B ).
We conclude that l is either a ⊗-cell or a !-cell or a box. Let us split in the three subcases.

i (c)} i∈Ij ∈ F ∞ ( !B X ) and {e i (d)} i∈Ij / ∈ F ∞ ( !B X )
. By the infinity of {e i (c)} i∈Ij , we deduce that of {e i (d)} i∈Ij (Lemma 2.13.(7)), hence {e i (d)} i∈Ij / ∈ F ( !B X ). Then by Lemma 2.13.( 5), there is a premise of l ↓b : !B different from ↓c such that {e i (b)} i∈Ij / ∈ F ( !B X ). This means that there is an infinite subset I ′ ⊆ I j such that {e i (b)} i∈I ′ ∈ F ∞ ( ?B ⊥ X ). By Fact 3.1, there exists an infinite subset

I ′′ ⊆ I ′ s.t. (e i (b)) i∈I ′′ is injective and {e i (b)} i∈I ′′ = {e i (b)} i∈I ′ .
We thus define φ j+1 := φ j • ↑b and I j+1 := I ′′ . By construction and by remark ( * ), φ j+1 , I j+1 meet conditions 1 and 2. As for φ j+1 's visibility, one argues similarly to the preceding case 1.

Subcase 2.2 (⊗-cell). The case l is a ⊗-cell is a simpler variant of the former subcase 2.1 and it is left to the reader (one has to use Lemma 2.11 instead of Lemma 2.13.( 5)).

Subcase 2.3 (box)

. If l is a box !ρ, then for every i ∈ I j , let e i (l) = [e k i ] k≤mi , with m i ∈ N, and let C = !B, D = !E for suitable formulas B and E (see Figure 11(b)). Moreover, for every i ∈ I j and every β ∈ ρ, let K β i be the set (possibly empty) of the superscripts of the experiments in e i (l) which are defined on β. We set:

µ β i := k∈K β i e k i (c ′ ), ν β i := k∈K β i [e k i (d ′ )],
where ↑c ′ (resp. ↓d ′ ) is the conclusion of β with c ′ (resp. d ′ ) associated with c (resp. d), as in Figure 11(b). Notice that:

e i (c) := β∈ρ µ β i , e i (d) := β∈ρ ν β i . (13)
We further split in two subcases, depending if {e i (d)} i∈Ij is finite or not.

1. If {e i (d)} i∈I j is finite, then max i∈I m i is defined, where recall that m i is the cardinality of e i (l), hence also of e i (d).

By the left equation ( 13) we deduce that { β∈ρ µ β i } i∈Ij = {e i (c)} i∈Ij . So by {e i (c)} i∈Ij ∈ F ∞ ( !B X ) and Lemma 2.13.(5), we have that {µ β i } i∈Ij ∈ F ( !B X ), for every β ∈ ρ. Furthermore, the infinity of {e i (c)} i∈Ij entails that there is a simple net β ∈ ρ s.t. {µ β i } i∈Ij is infinite (use Lemma 2.13. [START_REF] Danos | The structure of multiplicatives[END_REF]. Observe that it is crucial in this passage that the differential net ρ contains a finite number of simple nets). In particular we have

{µ β i } i∈Ij ∈ F ∞ ( !B X ): let us fix such a β. Now for every i ∈ I j and k ≤ max i∈I m i , we define µ k,β i := e k i (c ′ ) if k ∈ K β i , otherwise µ k,β i := 0. Notice that: µ β i = k≤maxi∈I mi µ k,β i . (14)
Since

{µ β i } i∈Ij ∈ F ∞ ( !B X )
, we use Lemma 2.13.( 5) and Lemma 2.13.(7) as above, and we deduce that there is a k ≤ max i∈I m i s.t. {µ k,β i } i∈Ij ∈ F ∞ ( !B X ): let us fix such a k (notice it is crucial in this passage that max i∈I m i is defined). i in e i (l). Since {λ i } i∈I ′ ∈ F ∞ ( ?F X ), then by Lemma 2.13.( 6) there is I ′′ ⊆ I ′ s.t. {e i (b)} i∈I ′′ ∈ F ∞ ( ?F X ). We apply Fact 3.1 and get I ′′′ ⊆ I ′′ s.t (e i (b)) i∈I ′′′ is injective and {e i (b)} i∈I ′′′ = {e i (b)} i∈I ′′ . We thus set φ j+1 := φ j • ↓c, ↑b and I j+1 := I ′′′ . As before φ j+1 and I j+1 meet conditions 1 and 2 (recall remark ( * )). As for visibility, we check the switching property exactly as in case 1, and we moreover notice that the passage c, b added to φ j+1 is visible 14 , thanks to φ β . 2. If {e i (d)} i∈I j is infinite, then the assumption {e

k i (c ′ )} i∈I k,β j ⊆ {µ k,β i } i∈Ij ⊆ {e k i (c ′ )} i∈I k,β j ∪ {0}, so {e k i (c ′ )} i∈I k,β j ∈ F ∞ ( !B X ).
i (d)} i∈Ij / ∈ F ∞ ( !E X ), implies {e i (d)} i∈Ij / ∈ F ( !E X ). Recall the above definition ν β i := k∈K β i [e k i (d ′ )],
for every simple net β ∈ ρ and index i ∈ I j . Since { β∈ρ ν β i } i∈Ij = {e i (d)} i∈Ij and {e i (d)} i∈Ij / ∈ F ( !E X ), we deduce that there is a simple net β ∈ ρ such that {ν β i } i∈Ij / ∈ F ( !E X ) (use Lemma 2.13.( 5)): let us fix such a β. By Lemma 2.12,

{ν β i } i∈Ij / ∈ F ( !E X ) implies that {e k i (d ′ )} i∈Ij k∈K β i / ∈ F ( E X ).
This means there is an infinite set I ′ ⊆ I j and a family of non-empty finite subsets

K ′ i ⊆ K β i (for i ∈ I ′ ), s.t. {e k i (d ′ )} i∈I ′ k∈K ′ i ∈ F ∞ ( E ⊥ X ). From the infinity of {e k i (d ′ )} i∈I ′ k∈K ′ i
and from the fact that each K ′ i is finite and non-empty, we deduce there is a function15 s β which associates with every

i ∈ I ′ an index s β (i) ∈ K ′ i such that {e s β (i) i (d ′ )} i∈I ′ is infinite. Of course
by downward closure we have also {e

s β (i) i (d ′ )} i∈I ′ ∈ F ∞ ( E ⊥ X
). Since β is visible-acyclic and size β < size α, we can apply the induction hypothesis to β and (e s β (i) i (d ′ )) i∈I ′ and get a subset I ′′ ⊆ I ′ , and a path φ β in β starting from ↑d ′ and ending in a conclusion ↑b ′ : ?F of β, and enjoying the condition 1 of the lemma. In particular {e

s β (i) i (b ′ )} i∈I ′′ ∈ F ∞ ( ?F X ).
Now for every i ∈ I ′′ , we set:

e i (b) = λ i + ν i ,
where λ i = e s β (i) i (b ′ ) and ν i is the sum of the values on b ′ of the experiments in e i (l) with superscript different from s β (i). We then argue exactly as in the above subcase and find I ′′′ ⊆ I ′′ s.t. (e i (b)) i∈I ′′′ is injective and its set of values is in F ∞ ( ?F X ). We thus define the path φ j+1 := φ j • ↓c, ↑b and I j+1 := I ′′′ . As before one notices that φ j+1 , I j+1 enjoys conditions 1 and 2. As for visibility, we check the switching property exactly as in case 1, and we moreover notice that the passage c, b added to φ j+1 is visible since there is a visible path, i.e. φ β , from ↑d ′ to ↑b. 16Case 3 (↑c conclusion of l). The last case is when ↑c is the conclusion a cell l (see Figure 11(c)). If l is a box, then we argue exactly as in the former case 2.3. Indeed the hypothesis of case 2.3 is that l is a box, and the set of (e i ) i∈Ij values on the conclusion of l is not finitary: here in fact condition 1 applied to ↓c ∈ φ j gives {e i (c)} i∈Ij / ∈ F ( !B X ), with ↑c : !B. The other cases (l a `/ ⊗ /!/?-cell) are very similar each other, all of them are easy variant of case 2.1. For example, suppose l is a !-cell, and let ↑c : !B, for a suitable formula B. As written above we have {e i } i∈Ij (c) / ∈ F ( !B X ). This means, by Lemma 2.13. [START_REF] Berry | Stable models of typed lambda-calculi[END_REF], that there should be a premise ↑ d : !B of l such that {e i (d)} i∈Ij / ∈ F ( !B X ). Hence there is I ′ ⊆ I j such that {e i (d)} i∈I ′ ∈ F ∞ ( ?B ⊥ X ). By Fact 3.1, we find I ′′ ⊆ I ′ such that (e i (d)) i∈I ′′ is injective and {e i (d)} i∈I ′′ = {e i (d)} i∈I ′ . We thus define φ j+1 := φ j • ↓c, ↓d and I j+1 := I ′′ . Theorem 3.3 (Soundness theorem). Let π be a differential net with conclusion the sequent Γ.

If π is visible-acyclic, then π is finitary, i.e. ∀X finiteness space, π X is a finitary relation of Γ X .

Proof. Let π be visible-acyclic and with conclusion Γ = C 1 , . . . , C n . We have to prove π X ∈ F (Γ) X = F ( ˙n j=1 C j X ). Suppose this is false, that is, suppose there is a subset u ⊆ π X s.t. u ∈ F ∞ ( Γ ⊥ X ). We prove a contradiction.

For every simple net α ∈ π, let u α be equal to u ∩ α X . Since by definition u = α∈π u α and since π contains a finite number of simple nets, then the infinity of u implies that there is an α ∈ π, s.t. u α is infinite. Let us fix such an α. By downward closure, we have also u α ∈ F ∞ ( Γ ⊥ X ). This means there is a family of experiments on α s.t. {e i (α)} i∈I ∈ F ∞ ( Γ ⊥ X ). By the infinity of {e i (α)} i∈I we deduce that there is a conclusion ↓ c k : C k of α s.t. {e i (c k )} i∈I is infinite: let us fix such a conclusion ↓ c k : C k . By Lemma 2.10 we deduce that {e

i (c k )} i∈I ∈ F ∞ ( C ⊥ k X ).
We can thus apply Lemma 3.2 to α, (e i ) i∈I and obtain a set I ′ ⊆ I and a conclusion ↓c

h : C h , s.t. {e i (c h )} i∈I ′ ∈ F ∞ ( C h X ). But this means {e i (c h )} i∈I / ∈ F ∞ ( C ⊥ h X ), thus (Lemma 2.10) u α / ∈ F ∞ ( Γ ⊥ X
), which contradicts the assumption.

We conclude that π X is a finitary relation of Γ X .

Finiteness ⇒ visible acyclicity

In this section we prove Theorem 4.5, which is the inverse of Theorem 3.3 for values. Corollary 4.7 uses these results to show the equivalence on values between visible acyclicity and finiteness.

Theorem 4.5 states the visible acyclicity of a value π from the finiteness of its interpretation π X , for a suitable X . The proof uses a general method based on Lemma 4.4 -morally the inverse of Lemma 3.2. Consider a simple value α with sequent conclusion Γ. Lemma 3.2 associates with a family of experiments (e i ) i∈N a visible path proving {e i (α)} i∈N ∈ F ( Γ X ); Lemma 4.4 instead is used in Theorem 4.5 to associate with a visible cycle a family of experiments (e i ) i∈N such that {e i (α)} i∈N / ∈ F ( Γ X ), or equivalently such that there is a set of indexes I ⊆ N such that {e i (α)} i∈I ∈ F ∞ ( Γ ⊥ X ). Let us give the idea of how the family (e i ) i∈N is defined by considering an example. Let α be the simple value in Figure 6(a), which contains the visible cycle φ = ↑b, ↓c, ↑d, ↓a . Let Γ be the sequent !?X ⊗ !!X ⊥ , ?!X ⊥ ⊗ ??X, conclusion of α. We define (e i ) i∈N by assigning the values of each e i on the boxes in α (and also on the conclusions of the axioms, in the general case): such an assignment gives always an experiment on α, since α is a value. The values of e i are given depending whether and how φ crosses a box, what we want in general is that for every oriented wire e : A crossed by φ, {e i (e)} i∈N / ∈ F ( A X ) ⊥ , or equivalently there is a set of indexes I ⊆ N, such that {e i (e)} i∈I ∈ F ∞ ( A X ). So in our example we need:

{e i (c)} i∈N , {e i (b)} i∈N / ∈ F (!?X ) ⊥ , ( 15
)
{e i (a)} i∈N , {e i (d)} i∈N / ∈ F (??X ) ⊥ . (16)
Claim ( 15) can be achieved by defining for every i ∈ N, e i (o

) = i[e o ]
, where e o is the unique experiment over the contents of o. In this way we have in fact {e i (c)} i∈N = {e i (b)} i∈N = {i[0]} i∈N , which is an infinite set in F ∞ (!?X ) by Lemma 2.12, and consequently it is not in F (!?X ) ⊥ . As for claim [START_REF] Ehrhard | Finiteness spaces[END_REF], we should suppose a set {x i } i∈N ∈ F ∞ (X ), so to define e i (u) = [e u i ], where e u i is the The following definition is morally an extension to differential nets of the definition of exhaustive experiments for proof-nets in [START_REF] Carvalho | A semantic measure of the execution time in linear logic[END_REF].17 So defined e, we prove it is exhaustive: consider a wire a of α which is not incident to a (co)weakening, we prove e(a) = 0 by induction on the number of wires above a. Notice this induction makes sense, since α is a value, hence it is upward acyclic, hence > α is a well-founded order on the wires (Proposition 2.2). The only delicate case is when ↓a is the premise of a box !ρ. In this case notice that a is not a weak wire, since α is a value. This means that there is at least one simple net γ ∈ ρ such that the conclusion ↓a γ of γ associated with a is not incident to a weakening. By definition we have e γ (a γ ) = 0, hence e(a) = 0 since e γ (a γ ) ⊆ e(a).

The hypothesis of α weak wire free plays a crucial role in the above Proposition 4.3, and consequently in Lemma 4.4 and Theorem 4.5. Indeed these results do not hold for upward acyclic cut-free simple nets which are not values. For an example, consider the simple nets α ′ and β ′ respectively in Figures 13(a), 13(b), which are non-value variants of resp. Figures 5(c), 5(b). The interpretations of α ′ and β ′ are:

α ′ X = { n [0] , 0, n [0] ; n ∈ N}, β ′ X = { 0, µ , µ ; µ ∈ M f in (M f in (|X |))}.
The two simple nets are visible-cyclic, but one can check that both α ′ X and β ′ X are finitary for every X . These examples motivate the definition of value (Definition 2.8) and explain why the following lemma cannot suppose α to be only cut-free and upward acyclic. 18Lemma 4.4 (Key lemma). Let α be a simple value, let X be a finiteness space having F ∞ (X ) and F ∞ (X ⊥ ) non-empty, and let φ be a path between two conclusions of α.

If φ is visible, then there is a family (e i ) i∈N of experiments on α such that for every oriented wire ↓c : C, we have:

1. for every I ⊆ ∞ N, if c ∈ φ then {e i (c)} i∈I is infinite; 2. if ↓c /
∈ φ, ↑c is not a conclusion of a cell and ↓c is not premise of a box, then {e i (c)} i∈N ∈ F ( C ⊥ X ). Proof. Given the simple value α, the finiteness space X , and the path φ as in the hypotheses, we define a family (e i ) i∈N of exhaustive experiments on α satisfying conditions 1 and 2 for every wire c. As usual, (e i ) i∈N is defined by induction on the depth of α.

For every formula A we have ∃u A ∈ F ∞ ( A X ) and ∃v A ∈ F ∞ ( A ⊥ X ) (Proposition 4.1). Let us fix once and for all for every positive formula 19 A, a pair of such u A , v A and two enumerations (x A i ) i∈N , (y A i ) i∈N of the elements in u A and v A (i.e. {x A i } i∈N = u A , {y A i } i∈N = v A ). Each experiment e i (i ∈ N) is defined by assigning its values on the axioms and boxes at depth 0 of α. Such an assignment gives always an experiment on α, since α is a simple value.

• Let a be an axiom of α, and let ↑a : A be its orientation with A positive, we set • Let !ρ be a box in Box α. Before giving the value of e i on !ρ, we need to define some preliminary experiments. First, we fix, independently from the index i, an arbitrary exhaustive experiment e !ρ on !ρ, which always exists since α, hence !ρ, is a value (Proposition 4.3). Second, let a 1 , b 1 ,. . . , a h , b h , for h ≥ 0, be the passages of φ through !ρ, if any: we associate with each j ≤ h a family of exhaustive experiments (e j i ) i∈N on !ρ, as follows (see Figure 14). (a). If b j is incident to the principal port of !ρ, then we set, for every i ∈ N, e j i (!ρ) := ie !ρ (!ρ). (b). If b j is incident to an auxiliary port of !ρ, and if there is a simple net β j ∈ ρ and a visible path φ j in β j starting from the conclusion of β j corresponding to the conclusion of !ρ and ending in the conclusion of β j corresponding to b j , then we apply the induction hypothesis to β j and φ j . So we get a family (e β j i ) i∈N of exhaustive experiments on β j satisfying conditions 1, 2. We set, for every i ∈ N, e j i (!ρ) := i e β j i .

e i (a) :=      x A i if ↑a ∈ φ, y A i if ↓a ∈ φ, x A 1 otherwise (i.e. a / ∈ φ). ρ a j b j • • • • • • (a) case ρ ′ + b ′ j β j φ j b j (b) case ρ ′ + b ′ j b j a ′ j a j β j φ j (c) case
(c). If b j is incident to an auxiliary port of !ρ, and the former case (b) does not hold, then from the visibility of a j , b j follows that there is a simple net β j ∈ ρ and a visible path φ j in β j starting from the conclusion of β j corresponding to a j and ending in the conclusion of β j corresponding to b j . We apply the induction hypothesis to β j and φ j , obtaining a family (e β j i ) i∈N of exhaustive experiments on β j satisfying conditions 1, 2. We set, for every i ∈ N, e j i (!ρ) := e β j i .

Once we have defined the families (e 1 i ) i∈N , . . . , (e h i ) i∈N associated with the h passages of φ though !ρ, we eventually set, for every i ∈ N:

? ?D ↓ c • • • • • • ?D ↓ b (a) case 2.1 ! !D ↓ c • • • !D !D ↓ a ↓ b (b) case 2.2 D β j ρ ′ + !D ↓ c ′ ↓ c (c) case 2.4 β j ρ ′ + !D ⊥ ?D ↓ c ′ ↑ c (d) case 3
e i (!ρ) := j≤h e j i (!ρ) if h > 0, e !ρ if h = 0.
We have so settled the definition of (e i ) i∈N . Notice the way we define e i on the boxes of α assures the exhaustivity of every e i (to formally prove this one should argue as in the proof of Prop. 4.3). The rest of the proof is devoted to show that (e i ) i∈N enjoys conditions 1 and 2. Let ↓c : C be an oriented wire of α, we prove conditions 1, 2 by induction on the number of wires above c. As for Proposition 4.3, notice that this induction makes sense, since α is upward acyclic (Proposition 2.2). The proof splits in three cases, depending on c: case 1, c is an axiom; case 2, one orientation of c is conclusion of a cell; case 3, one orientation of c is premise of a box. Notice that these cases are disjoint and complete since α is a value, in particular since α is cut-free.

Case 1 (c axiom). If c is an axiom, then both conditions 1 and 2 follow straightforwardly by the definition of {e i } i∈N .

Case 2 (↓c or ↑c conclusion of a cell). Assume ↓c : C is the conclusion of a cell l (the case ↑c is the conclusion of l is an easier variant, in particular condition 2 is trivial). We split in further subcases, depending on the type of l. Subcase 2.1 (l is a ?-cell). If l is a ?-cell, then ↓ c : C = ?D, for a suitable formula D (see Figure 15(a)).

Let us prove condition 1: let I ⊆ ∞ N and assume c ∈ φ, we show that {e i (c)} i∈I is infinite. If c ∈ φ, then there is a premise ↓b : ?D of l such that b ∈ φ (recall φ is a path between two conclusions of α). By induction hypothesis (condition 1) {e i (b)} i∈I is infinite. We conclude that {e i (c)} i∈I is infinite by Lemma 2.13. [START_REF] Danos | The structure of multiplicatives[END_REF].

As for condition 2: suppose ↓c / ∈ φ, we prove {e i (c)} i∈N ∈ F ( !D ⊥ X ). From ↓ c / ∈ φ and the visibility of φ, we deduce for every premise ↓ b : ?D of l that ↓b / ∈ φ. Also, remark that nor ↑b is conclusion of a cell, nor ↓b is premise of a box, so by the induction hypothesis (condition 2) we have {e i (b)} i∈N ∈ F ( !D ⊥ X ). Since for every i ∈ N, e i (c) is equal to the sum of the e i values on l's premises, we conclude {e i (c)} i∈N ∈ F ( !D ⊥ X ) by Lemma 2.13.(5). Subcase 2.2 (l is a !-cell). If l is a !-cell, then ↓ c : C = !D, for a suitable formula D (see Figure 15(b)). Condition 1 is proven exactly as in subcase 2.1. Let us show condition 2: suppose ↓c / ∈ φ, we prove {e i (c)} i∈N ∈ F ( ?D ⊥ X ). This case is more delicate than the former subcase 2.1, since φ can cross some premises of l. We thus split in two subcases.

1. If no premise of l is in φ, then we deduce {e i (c)} i∈N ∈ F ( ?D ⊥ X ) exactly as in subcase 2.1, but using point (8) of Lemma 2.13 instead of point (5). 2. If φ crosses some premise of l, then it must cross one premise upwardly.

In fact if ↓b : !D is a premise of l such that ↓b ∈ φ, then there is another premise ↓a : !D such that ↑a ∈ φ, φ being a path ending in a conclusion of α and ↓c / ∈ φ (recall Figure 15(b)). So assume ↑a ∈ φ, this implies ↓a / ∈ φ. As in the subcase 2.1, we can apply the induction hypothesis and obtain (condition 2) {e i (a)} i∈N ∈ F ( ?D ⊥ X ). Moreover, by condition 1 we infer for every I ⊆ ∞ N that {e i (a)} i∈I is infinite. The downward closure allows then to deduce for every

I ⊆ ∞ N, {e i (a)} i∈I ∈ F ∞ ( ?D ⊥ X ). Now, suppose by contradiction {e i (c)} i∈N / ∈ F ( ?D ⊥ X ). This means there is I ⊆ ∞ N, s.t. {e i (c)} i∈I ∈ F ∞ (! D X ). By Lemma 2.13.(5), we have {e i (a)} i∈I ∈ F (! D X ), so contradicting {e i (a)} i∈I ∈ F ∞ ( ?D ⊥ X ). We conclude {e i (c)} i∈N ∈ F ( ?D ⊥ X ).
The reader should notice that the above reasoning uses the fact that condition 1 holds for every infinite subset I of N and not simply for N. Subcase 2.3 (l is a ⊗/`/!d/?d-cell). The case l is a `-cell (resp. a ⊗-cell) is an easier variant of subcase 2.1 (resp. subcase 2.2). If l is a (co)dereliction cell then the conditions 1, 2 are immediate consequences of the induction hypothesis. Subcase 2.4 (l is a box). If l is a box !ρ, then we have C = !D, for a suitable formula D (see Figure 15(c)). The reader will notice a strict similarity between this case and the cocontraction case (subcase 2.2).

We start by proving condition 1. Suppose φ crosses c, then there is a passage a j , b j of φ through !ρ such that c = a j or c = b j . Since ↓c is the conclusion of !ρ, then the family (e j i ) i∈N of experiments on !ρ associated with the passage a j , b j is defined in accordance with the above case (a) or case (b): that is for every i ∈ N,

e j i (c) = ie !ρ (c) if c = b j , i[e β j i (c ′ )] if c = a j ,
where, in case c = a j , ↓c ′ is the conclusion corresponding to ↓c of the simple net β j of ρ on which e β j i is defined (see Fig. 15(c)). Notice for every I ⊆ ∞ N, {e j i (c)} i∈I is infinite, since it contains multisets of arbitrary large cardinality. Lemma 2.13.(7) allows then to conclude that {e i (c)} i∈I is infinite (in fact {e i (c)} i∈N = { j≤h e j i (c)} i∈N ). We conclude that condition 1 holds for c.

As for condition 2: suppose ↓c / ∈ φ, we prove {e i (c)} i∈N ∈ F ( ?D ⊥ X ).

If φ does not cross !ρ, then {e i (c)} i∈N = {e !ρ (c)}, which is clearly in F ( ?D ⊥ X ), being a singleton. Otherwise, let a 1 , b 1 , . . . , a h , b h , for h > 0, be the passages of φ through !ρ: by definition {e i (c)} i∈N = { j≤h e j i (c)} i∈N . We prove that for every j ≤ h, {e j i (c)} i∈N ∈ F ( ?D ⊥ X ). From this follows {e i (c)} i∈N ∈ F ( ?D ⊥ X ), by applying Lemma 2.13. [START_REF] Retoré | A semantic characterisation of the correctness of a proof net[END_REF].

So consider a j , b j for a j ≤ h: notice that c = b j , since ↓ c / ∈ φ. Hence the family (e j i ) i∈N has been defined as in case (b) or in case (c). Let β j (resp. φ j ) denote the simple net of ρ (resp. the visible path in β j ) associated with the passage a j , b j , and let ↓c ′ : D denote the conclusion of β j corresponding to c (recall Fig. 15(c)). We split in two subcases.

1. If the family (e j i ) i∈N has been defined following case (b), then we have e j i (c) = i e β j i (c ′ ) , and also that φ j starts from ↑ c ′ . This means that, from condition 1 applied to (e β j i ) i∈N , we have for every I ⊆ ∞ N that {e β j i (c ′ )} i∈I is infinite; and from ↓ c ′ / ∈ φ j , condition 2 and the downward closure we have {e β j i (c ′ )} i∈I ∈ F ( D ⊥ X ). We conclude that for every I ⊆ ∞ N, {e β j i (c ′ )} i∈I ∈ F ∞ ( D ⊥ X ). Now suppose by contradiction {e j i (c)} i∈N / ∈ F ( ?D ⊥ X ). This means there is I ⊆ ∞ N such that {e j i (c)} i∈I ∈ F ∞ (! D X ). By Lemma 2.10 we deduce {e β j i (c ′ )} i∈I = supp {e j i (c)} i∈I ∈ F ( D X ). But we have already remarked that {e β j i (c ′ )} i∈I ∈ F ∞ ( D ⊥ X ) (I being infinite 20 ), so we get a contradiction. We conclude {e j i (c)} i∈N ∈ F ( ?D ⊥ X ). 2. If the family (e j i ) i∈N has been defined following case (c), then we have e j i (c) = e β j i (c ′ ) .

Since ↓c ′ / ∈ φ j , we can apply condition 2 to (e β j i ) i∈N and φ j and obtain {e β j i (c ′ )} i∈N ∈ F ( D ⊥ X ). We easily conclude {e j i (c)} i∈N = {[e β j i (c ′ )]} i∈N ∈ F ( ?D ⊥ X ).

Case 3 (↓c or ↑c is premise of a box). Assume ↑c is premise of a box !ρ ∈ Box α (as for the case 2, the subcase ↓c is premise of !ρ is an easier variant, in particular condition 2 is trivial). Then we have C = ?D, for a suitable formula D (see Figure 15(d)).

We first prove condition 1: suppose c ∈ φ, let us show that for every I ⊆ ∞ N, the set {e i (c)} i∈I is infinite.

Since c ∈ φ, there is a passage a j , b j of φ through !ρ such that c = a j or c = b j . Let (e j i ) i∈N be the family of experiments on !ρ associated with the passage a j , b j . We prove that for every I ⊆ ∞ N, the set {e j i (c)} i∈I is infinite. This entails that also {e i (c)} i∈I is infinite (Lemma 2.13.( 7)). The proof splits in two cases.

1. If (e j i ) i∈N has been defined in accordance with case (a) or case (b), then we have:

e j i (c) = ie !ρ (c) if case (a), ie β j i (c ′ ) if case (b),
where, in case (b), β j is the simple net on which is defined e β j i , and c ′ is the wire of β j corresponding to c (recall Fig. 15(d)). By the exhaustivity of e !ρ (resp. e β j i ) we deduce that e !ρ (c) (resp. e β j i (c ′ )) is non-empty. Hence {e j i (c)} i∈I is infinite for every I ⊆ ∞ N, having multisets of arbitrary large cardinality. 212. If (e j i ) i∈N has been defined in accordance with case (c): let β j (resp. φ j ) denote the simple net of ρ (resp. the visible path in β j ) associated with the passage a j , b j , and let ↓c ′ : ?D be the conclusion of β j corresponding to c (recall Fig. 15(d)). We have:

e j i (c) = e β j i (c ′ )
Notice that c ′ ∈ φ j , so by definition (condition 1) of (e β j i ) i∈N , for every I ⊆ ∞ N, {e β j i (c ′ )} i∈I = {e j i (c)} i∈I is infinite. Let us prove condition 2. Suppose ↓c / ∈ φ. We prove {e i (c)} i∈N ∈ F (! D ⊥ X ). If φ does not cross !ρ, then {e i (c)} i∈N = {e !ρ (c)}, which is clearly in F (! D ⊥ X ), being a singleton. Otherwise, let a 1 , b 1 , . . . , a h , b h , for h > 0, be the passages of φ through !ρ: we have {e i (c)} i∈N = { j≤h e j i (c)} i∈N , by definition. We prove {e j i (c)} i∈N ∈ F (! D ⊥ X ), for every j ≤ h. From this we have {e i (c)} i∈N ∈ F (! D ⊥ X ), by applying Lemma 2.13. [START_REF] Berry | Stable models of typed lambda-calculi[END_REF].

So consider a j , b j for a j ≤ h, we have for any i ∈ N:

e j i (c) =     
ie !ρ (c) if e j i is defined following case (a), ie β j i (c ′ ) if e j i is defined following case (b), e β j i (c ′ ) if e j i is defined following case (c),

where in cases (b) and (c), β j (resp. φ j ) denotes the simple net of ρ (resp. the visible path of β j ) associated with the passage a j , b j , and ↓c ′ : ?D denotes the conclusion of β j corresponding to c. Since ↓c / ∈ φ, then ↓c ′ / ∈ φ j . In case (a), notice i∈N supp(e j i (c)) = supp(e !ρ (c)) is finite, hence it is in F ( D ⊥ X ). By Lemma 2.10 this entails {e j i (c)} i∈N ∈ F ( !D ⊥ X ). In the cases (b) and (c), we have ↓c ′ / ∈ φ j , hence by induction hypothesis (condition 2) we have {e β j i (c ′ )} i∈N ∈ F (! D ⊥ X ). So Lemma 2.12 entails supp {e β j i (c ′ )} i∈N ∈ F (! D ⊥ X ); moreover, being supp {e β j i (c ′ )} i∈N = supp {e j i (c)} i∈N , we conclude (again by Lemma 2.12) {e j i (c)} i∈N ∈ F (! D ⊥ X ).

Theorem 4.5. Let π be a value with conclusion the sequent Γ, and let X be a finiteness space such that both F ∞ (X ) and F ∞ (X ⊥ ) are non-empty. If π X is a finitary relation of Γ X , then π is visible-acyclic.

Proof. Let us fix once and for all a finiteness space X with F ∞ (X ) and F ∞ (X ⊥ ) non-empty. Let π be a value which is not visible-acyclic: we prove that π X / ∈ F ( Γ X ). The proof is by induction on the size of π.

Case 1 (linear combination). If π is a linear combination of more than one simple net, then we can consider π = π 1 + π 2 s.t. size π i < size π (i = 1, 2) and at least π 1 is not visible-acyclic. By induction hypothesis π 1 X / ∈ F ( Γ X ). Since π 1 X ⊂ π X , we conclude π X / ∈ F ( Γ X ) by the downward closure.

The other cases deal with a value π which is simple: let us call it α, let also Γ = C 1 , . . . , C n . We prove that there is a family (e i ) i∈N of experiments on α, such that {e i (α)} i∈N ∈ F ∞ ( Γ ⊥ X ). This is of course equivalent to prove α X / ∈ F ( Γ X ).

Case 2 (mix-rule). If π is a simple net α with more than one component, let α 1 , α 2 be any non-trivial partition of α's components in two simple subnets. We can assume w.l.o.g. that α's conclusions are enumerated in such a way that the first h < n conclusions are the conclusions of α 1 . That is C 1 , . . . , C h (resp. C h+1 , . . . , C n ) is the sequent conclusion of α 1 (resp. α 2 ). Of course size α i < size α, for i = 1, 2, and we can suppose that at least one of the two simple subnets, say α 1 , is not visible-acyclic. By induction hypothesis there is a family of experiments (e α1 i ) i∈N s.t.:

{e α1 i (α 1 )} i∈N ∈ F ∞ ( h i=1 C ⊥ i X ) (17)
Fix now an arbitrary experiment e α2 on α 2 (which always exists, α 2 being a value), and define for every i ∈ N, the experiment e i on α as the union of e α1 i and e α2 . We have {e i (α)} i∈N = { e α1 i (α 1 ), e α2 (α 2 ) } i∈N . By the above claim [START_REF] Ehrhard | The differential lambda-calculus[END_REF] and Lemma 2.10, we immediately have {e

i (α)} i∈N ∈ F ∞ ( n i=1 C ⊥ i X ) = F ∞ ( Γ ⊥ X
). Now we can suppose α being a connected simple value. In this case we have only two possibilities: either α has at depth 0 a cell l which is not a box, and whose conclusion is a conclusion of α, or α is made of only one box !ρ at depth 0. We thus split in these two cases.

Case 3 (terminal cell, no box). Assume α has a cell l which is not a box and whose conclusion ↓ c is also a conclusion of α. Suppose w.l.o.g. the type of ↓c is C 1 . Then the proof splits in several subcases, depending on the type of l. We consider only the case l is a !-cell, the other cases (⊗/ `/?/!d/?d-cell) are similar or easier. If l is a !-cell, then C 1 = !D, for a suitable formula D. Let α ′ be the simple net obtained from α by removing l and the wire c, and let !D, . . . , !D, C 1 , . . . , C n be the sequent conclusion of α ′ , where !D occurs as many times as the number of premises of l.

Since l is a !-cell, we can have visible cycles in α which are not in α ′ (these are specifically the cycles crossing l), in particular α ′ could be visible-acyclic. Thus we split in two subcases. 22Subcase 3.1. If α ′ is not visible-acyclic, we apply the induction hypothesis to α ′ , obtaining a family (e i ) i∈N of experiments s.t.:

{e i (α ′ )} i∈N ∈ F ∞ ( ?D ⊥ ⊗ . . . ⊗ ?D ⊥ ⊗ n i=2 C ⊥ i X ).
For every i ∈ N we extend e i to α in the obvious way, i.e.

By Lemma 2.10 and Lemma 2.13.( 7)-(8), we have {e i (α)} i∈N ∈ F ∞ ( Γ ⊥ X ). Subcase 3.2. If α ′ is visible-acyclic, then every visible cycle of α crosses l. This means that there is a visible path φ between two premises ↓a 1 , ↓a 2 of l, which are conclusions of α ′ . Suppose w.l.o.g. φ starts from ↑a 1 and ends in ↓a 2 . We then apply Lemma 4.4 to α ′ and φ, obtaining a family of experiments (e i ) i∈N enjoying conditions 1 and 2 of the lemma. In particular, for every I ⊆ ∞ N, {e i (a 1 )} i∈I ∈ F ∞ ( ?D ⊥ X ) and for every conclusion ↓g : G of α ′ different from ↓a 2 , we have {e i (g)} i∈N ∈ F ( G ⊥ X ). 23We extend every e i (i ∈ N) to α as in the above equation [START_REF] Ehrhard | Differential interaction nets[END_REF]. One can show (as we did in the proof of Lemma 4.4, subcase 2.2) that {e i (c)} i∈N ∈ F ∞ ( ?C ⊥ X ), since for every I ⊆ ∞ N, {e i (a 1 )} i∈I ∈ F ∞ ( ?C ⊥ X ). We conclude, using Lemma 2.10, {e i (α)} i∈N ∈ F ∞ ( Γ ⊥ X ). Case 4 (only a box). If α is a box !ρ, then let ↓c 1 : !D 1 , ↓c 2 : ?D 2 , . . . , ↓c n : ?D n be the interface of α, where ↓c 1 (resp. ↑c 2 , . . . , ↑c n ) is the conclusion (resp. are the premises) of !ρ.

Clearly, the hypothesis α not visible-acyclic, implies that neither ρ is visibleacyclic (recall α is made of the only box !ρ). We thus apply the induction hypothesis, obtaining a family (e ρ i ) i∈N of experiments on ρ s.t. {e ρ i (ρ)} i∈N ∈ F ∞ ( D ⊥ Corollary 4.6. Let X be any finiteness spaces with F ∞ (X ) and F ∞ (X ⊥ ) nonempty. For every value π with sequent conclusion Γ, we have: π X ∈ F ( Γ X ) iff π is finitary, i.e. ∀Y finiteness space, π Y ∈ F ( Γ Y ).

Proof. The right-to-left implication is obvious. As for the left-to-right one: if π X ∈ F ( Γ X ), then by Theorem 4.5, π is visible-acyclic, then by Theorem 3.3, π is finitary.

1 25 3 31 4

 12531 Differential nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.2 Finiteness spaces . . . . . . . . . . . . . . . . . . . . . . . . . . . Visible acyclicity ⇒ finiteness Finiteness ⇒ visible acyclicity 39

Figure 2 :

 2 Figure 2: cells for differential nets, together with their typing rules. Contractions and cocontractions are commutative (their auxiliary ports are indistinguishable and interchangeable) and cannot have two ports.

Figure 3 :

 3 Figure3: desequentialization of the proofs of the DiLL sequent calculus; as for the 0-cocontraction, we mean that its desequentialization is the simple net consisting of a unique !-cell.

?

Figure 4 :

 4 Figure 4: example of switching acyclicity and switching cyclicity (Def. 2.3).

Figure 5 :

 5 Figure 5: examples of visible cycles (Definition 2.5).

  (b) is switching cyclic but visible-acyclic, in fact both passages a, b and b, a are not visible; in Figures 5(a)-(c) we have three examples of visible-cyclic simple nets, which are however upward acyclic. In particular the passage a, b of the cycle ↑a, ↓b in Figure 5(a) (resp. Figure 5(b)) is visible by Condition 1 (resp. Condition 2) of Definition 2.5, while the passage b, c of ↑b, ↓c in Figure 5(c) is visible by Condition 3.

Figure 6 :

 6 Figure 6: example of the importance of directedness in the notion of visibility.

Figure 7 :

 7 Figure 7: switchings associated with the cells for differential nets. In case of n-(co)contractions, we suppose n ≥ 2.

1 .

 1 for any u ∈ F (X ) ⊥ , one has w(u) = {b ∈ |Y| ; ∃a ∈ u, (a, b) ∈ w} ∈ F (Y), and 2. for any v ∈ F (Y) ⊥ , one has w ⊥ (v) ∈ F (X ), where w ⊥ = {(b, a) ; (a, b) ∈ w} ⊆ |X | × |Y| = |X ⊥ `Y⊥ | is the transpose of w.

Figure 9 :

 9 Figure 9: conditions required on experiments. Experiments are pictured as wire/box's labelling. In case of a box !ρ, we set ρ ′ j := ρα j , for every α j ∈ ρ.

  9): for every wires a, b 1 , . . . , b n , • if a is the conclusion of a ⊗/`-cell with premises b 1 , b 2 , then e(a) = e(b 1 ), e(b 2 ) ; • if a is the conclusion of a !d/?d-cell with premise b 1 , then e(a) = [e(b 1 )];

  Simple values with interaction reducing to Figure 10(a).

Figure 10 :

 10 Figure 10: Montelatici's fixed point operator applied to identity and two simple values giving it as an interaction.

Figure 11 :

 11 Figure 11: main cases of the proof of Lemma 3.2.

Subcase 2 . 1

 21 (!-cell). If l is a !-cell, then C, D = !B for a suitable formula B. By hypotheses we have {e

  Let now I k,β j ⊆ I j be the set of indexes s.t. (e k i ) i∈I k,β j is the family of experiments on β with superscript k in i∈Ij [e 1 i , . . . , e mi i ]. In particular, we have {e

  Since β is a visible-acyclic simple net and depth β < depth α, we can apply the induction hypothesis to β and (e k i ) i∈I k,β j and obtain an infinite set I ′ ⊆ I k,β j and a visible path φ β in β starting from ↓c ′ , ending in a conclusion ↑b ′ : H of β, and enjoying the condition 1 of the lemma. In particular {e k i (b ′ )} i∈I ′ ∈ F ∞ ( H X ). Let b be the wire incident to l corresponding to b ′ . Notice that b should be different from d, since by hypothesis {e i (d)} i∈Ij is finite, so i∈Ij supp e i (d) is finite, while b = d would imply that {e k i (b ′ )} i∈I ′ ⊆ i∈Ij supp e i (d), which violates the infinity of {e k i (b ′ )} i∈I ′ . We conclude b = d, hence one orientation of b, say ↓b, is a premise of l. Let then ↑b : ?F , as well as H = ?F (recall always Figure 11(b)). Notice that for every i ∈ I ′ , e i (b) = λ i + ν i , where λ i = e k i (b ′ ) and ν i is the sum of the values on b ′ of the experiments different from e k

  variant of Fig. 5(b).

Figure 13 :

 13 Figure 13: examples of visible-cyclic nets which are not values.

Definition 4 . 2 .Proposition 4 . 3 .

 4243 An exhaustive experiment of a differential net is an exhaustive experiment of one of its simple nets; an exhaustive experiment of a simple net α is an experiment e : α such that:• for every wire a, e(a) = 0 iff a is incident to a (co)weakening,• for every box !ρ, e(!ρ) contains only exhaustive experiments of ρ.Exhaustive experiments always exist over values: Given a simple value α, there exist exhaustive experiments over α.Proof. By induction on the depth of α. Define e : α by assigning a web element different from the empty multiset to the axioms and by setting for every box !ρ ∈ Box α, e(!ρ) = β∈ρ e β , where e β is an exhaustive experiment on β (which exists by induction hypothesis).

Figure 14 :

 14 Figure 14: the three cases of the definition of {e j i } i∈N , proof of Lemma 4.4.

Figure 15 :

 15 Figure 15: main cases in the proof of Lemma 4.4.

e

  i (c) := ↓a premise of l e i (a).

1 n

 1 i=2 !D ⊥ i X ). For every i ∈ N, we define an experiment of α simply by setting e i (!ρ) := [e ρ i ]. Clearly we have {e i (α)} i∈N ∈ F ∞ ( Γ ⊥ X ).Theorem 3.3 and Theorem 4.5 have two notable consequences with respect to the notion of finitary value (Definition 2.15).

Corollary 4 . 7 .

 47 For every value π, π ∈ FIN iff π ∈ VAC.Proof. Immediate consequence of Theorem 3.3 and Theorem 4.5.

To be precise, Girard's original proof does not deal with switching paths, introduced later by Danos and Regnier, but with a variant of them, called trips.

Indeed Retoré's proof of Theorem 1.2 needs slightly stronger assumptions on the interpretation of variables. Paolo Di Giamberardino has later reduced the hypotheses to the only existence of three points, two strictly coherent and two strictly incoherent[START_REF] Di Giamberardino | Proof Nets and Semantics: Coherence and Acyclicity, Mémoire de D.E.A. de Mathématiques Discrétes et[END_REF].

Non-uniform coherence spaces are a variant of Girard's coherence spaces introduced by Antonio Bucciarelli and Thomas Ehrhard in[START_REF] Bucciarelli | On phase semantics and denotational semantics: the exponentials[END_REF]. The main difference being that in Girard's semantics the webs associated with the exponentials depend on the coherence relation, in Bucciarelli and Ehrhard's one it does not. We adopt moreover a further variant of Bucciarelli and Ehrhard's definition of non-uniform coherence, given by Pierre Boudes in[START_REF] Boudes | Non uniform hypercoherences[END_REF].

We must mention here that the original statement of Theorem 1.4 in[START_REF] Pagani | Acyclicity and Coherence in Multiplicative and Exponential Linear Logic[END_REF] has a mistake, since the weak wire-free hypothesis is missing.

The support of a vector v ∈ K X is the set {a ; va = 0} ⊆ X.

In fact, for any a ∈ |A| (resp. c ∈ |C|), the set of b ∈ |B| s.t. v a,b = 0 should be a clique of B (resp. of B ⊥ ), and cliques and anti-cliques (i.e. cliques of the complement graph) intersect at most in one point.

Actually, Figure1(a) defines a slight variant of usual MELL sequent calculus gathering in a unique n-ary ?-rule a tree of binary contractions and zeroary weakenings.

Remark one can have i, j ≤ n such that ↑a i =↓a j .

Remark that the passage c, d is visible thanks to condition 3 of Definition 2.5.

Remark that the passage c, b is visible thanks to condition 1 of Definition 2.5.

Here we are using the axiom of choice.

Remark that the passage c, b is visible thanks to condition 2 of Definition 2.5.

Actually there are minor differences between our definition and that of[START_REF] Carvalho | A semantic measure of the execution time in linear logic[END_REF], but we do not want to bore the reader with such technicalities.

The definition of value corrects a mistake in[START_REF] Pagani | Acyclicity and Coherence in Multiplicative and Exponential Linear Logic[END_REF]: in that extended abstract only the cut-free hypothesis was supposed.

We recall that a formula is positive if it is X or its topmost connective is a ! or a ⊗; notice A is positive iff A ⊥ isn't.

Again, remark that it is crucial in this reasoning that condition 1 holds for every infinite subset I of N and not simply for N.

This argumentation uses the hypothesis that e !ρ /e β j i are exhaustive. Exactly for this passage we have introduced Definition 4.2.

Notice that if l is a cell of type ?, `, !d, ?d, then every visible cycle of α is a visible cycle of α ′ , hence the proof of those cases follows directly subcase 3.1.

Indeed, remark that if ↓g is a conclusion of α ′ , then ↑g cannot be a conclusion of a cell in α ′ nor ↓g can be premise of a box, so condition 2 of Lemma 4.4 entails {e i (g)} i∈N ∈ F ( G ⊥ X ).

Acknowledgements

I am especially grateful to Thomas Ehrhard for his several hints which let me understand finiteness spaces and differential linear logic. I also warmly thank Giulio Manzonetto, Damiano Mazza, Christine Tasson and Paolo Tranquilli for their insightful comments and suggestions that helped me to improve the paper.

✩ Supported by a postdoc fellowship of Région Île-de-France and by the French ANR project "Curry Howard for the Concurrency" ANR-07-BLAN-0324.

experiment over the contents of u, taking value [x i ] on the axiom inside the box u. So defining, we have {e i (a)} i∈N = {e i (d)} i∈N = {[[x i ]]} i∈N , which is a set not in F (??X ) ⊥ , by Lemma 2.12 and the fact that supp(supp({[[x i ]]} i∈N )) / ∈ F (X ⊥ ). We then have the following set of experiment results:

which is a set not in Γ X , by Lemmas 2.10, 2.11 and claims [START_REF] Ehrhard | On köthe sequence spaces and linear logic[END_REF], [START_REF] Ehrhard | Finiteness spaces[END_REF]. Let us conclude the example stressing once more the key role played by the visibility of the passages b, c , d, a of φ through o and u. If one considers the simple net β in Fig. 6(b), in which the passage d, a is not visible, one has:

which is a finitary set of Γ X , for every X .

The above example uses a set {[x i ]} i∈N ∈ F ∞ (?X ) as the set of values of a family of experiments (e u i ) i∈N on an axiom ↑d : ?X. In the general case we have to assure that for every formula A there is such a set u ∈ F ∞ ( A X ), and this is true if one suppose F ∞ (X ) and F ∞ (X ⊥ ) non-empty, as proven in the next Proposition 4.1.

Proposition 4.1. Let X be a finiteness space such that both F ∞ (X ) and F ∞ (X ⊥ ) are non-empty. Then the same holds for the interpretation of every formula A, i.e. ∃u A ∈ F ∞ ( A X ) and ∃v A ∈ F ∞ ( A ⊥ X ). Proof. By induction on deg A. Apart from the immediate base of induction (A atomic), we have two cases, depending if the topmost connective of A is multiplicative or exponential. We treat only the latter case, the former one being an easier variant.

Suppose A = !B (the case A = ?B is symmetric), by induction hypothesis we have

, and this would prevent v ′ to be in F ∞ (! B X ) (Lemma 2.12).

Notice that there are finiteness spaces X such that both F ∞ (X ) and F ∞ (X ⊥ ) are non-empty. For example, let 1 be the finiteness space with the singleton { * } as web, and consider !1 `?1. Clearly (!1 `?1) ⊥ = ?1 ⊗ !1, since 1 ⊥ = 1. One can easily check that the set

Another trick used in the example of Figure 6(a) is the set {e i (b)} i∈N associated with the premise ↑ b : !?X of the box o, which is infinite even if it has a finite global support (in the example supp({e i (b)} i∈N ) = {0}), so that {e i (b)} i∈N ∈ F ∞ ( ?X ⊥ X ) by Lemma 2.12. To assure that this trick is always possible we need the next notion of exhaustive experiment and Proposition 4.3.