M A R C O S O L I E R I
email: ms@xt3.it

Under consideration for publication in Math. Struct. in Comp. Science Geometry of Resource Interaction and Taylor-Ehrhard-Regnier Expansion A Minimalist Approach

Geometry of resource interaction and

Taylor-Ehrhard-Regnier expansion: a minimalist approach

Introduction

Geometry of Interaction. The dynamics of β-reduction or cut elimination can be described in a purely geometric way -studying paths in some graph representations of terms or proofs, and looking at those which are persistent, i.e. that have a residual path in any reduct. The quest for an effective semantic characterisation of persistence separately produced three notions of paths: regularity, defined by a dynamic algebra [START_REF] Girard | Geometry of interaction I: Interpretation of System F[END_REF][START_REF] Danos | Proof-nets and the Hilbert space[END_REF], legality, formulated by topological conditions cycles [START_REF] Asperti | Paths, computations and labels in the lambda-calculus[END_REF]; consistency, expressed as traces of a token-machine execution [START_REF] Gonthier | The geometry of optimal lambda reduction[END_REF] and developed to study the implementation [START_REF] Lamping | An algorithm for optimal lambda calculus reduction[END_REF][START_REF] Kathail | Optimal Interpreters for lambda-calculus based functional languages[END_REF] of Lévy-optimal reduction [START_REF] Lévy | Réductions Correctes et Optimales dans le Lambda Calcul[END_REF]. These notions are equivalent [START_REF] Asperti | Paths in the lambda-calculus[END_REF], and their common core idea -describing computation by local and asynchronous conditions on routing of paths -inspired the design of efficient parallel abstract machines [START_REF] Mackie | The geometry of interaction machine[END_REF][START_REF] Danos | Directed virtual reductions[END_REF][START_REF] Laurent | A Token Machine for Full Geometry of Interaction (Extended Abstract)[END_REF][START_REF] Pinto | Parallel Implementation Models for the Lambda-Calculus Using the Geometry of Interaction[END_REF][START_REF] Pedicini | PELCR: Parallel environment for optimal lambda-calculus reduction[END_REF][START_REF] Dal Lago | The Geometry of Synchronization[END_REF][START_REF] Pedicini | Sequential and parallel abstract machines for optimal reduction[END_REF]Dal Lago et al., 2015, among others). More recently, the geometry of interaction (GoI) approach has been fruitfully employed for semantic investigations which characterised quantitative properties of programs, with respect to both time [START_REF] Dal Lago | Context semantics, linear logic, and computational complexity[END_REF][START_REF] Perrinel | On Context Semantics and Interaction Nets[END_REF][START_REF] Aubert | Unary Resolution: Characterizing Ptime[END_REF] and space complexity [START_REF] Löding | Characterizing co-NL by a group action[END_REF][START_REF] Seiller | Logarithmic Space and Permutations[END_REF]Mazza, 2015b;[START_REF] Mazza | Parsimonious Types and Non-uniform Computation[END_REF].

Taylor-Ehrhard-Regnier expansion and resource calculus. Linear logic's [START_REF] Girard | Linear logic[END_REF] decomposition of the intuitionistic implication unveiled the relation between the algebraic concept of linearity and the computational property of a function argument to be used exactly once. Such a decomposition enabled a differential constructor and linear combinations to extend: the λ-calculus into the differential λ-calculus [START_REF] Ehrhard | The differential lambda-calculus[END_REF]; and, more generally, linear logic into the differential linear logic (DiLL) [START_REF] Ehrhard | Differential interaction nets[END_REF][START_REF] Tranquilli | Intuitionistic differential nets and lambda-calculus[END_REF]. These constructions allow considering the Taylor expansion of a term [START_REF] Ehrhard | Uniformity and the Taylor expansion of ordinary lambdaterms[END_REF], which rewrites it as an infinite series of terms of the resource λ-calculus (RC). It is a completely linear restriction of the differential λ-calculus, similar to the λ-calculus with multiplicities [START_REF] Boudol | The lambda-calculus with multiplicities[END_REF], where the argument of an application is a superposition of terms and must be linearly used. Taylor-Ehrhard-Regnier expansion contains any finite approximation of the headnormalisation of a term, as evoked by its commutativity with Böhm trees: the expansion of the Böhm tree of a term is equal to the normal form of its expansion (Ehrhard and Regnier, 2006a). Approximation of λ-terms have been studied within affine calculi as well (Mazza, 2015a), and also using paths to guide the very process of linearisation [START_REF] Alves | Weak linearization of the lambda calculus[END_REF]. Taylor-Ehrhard-Regnier expansion originated various investigations on quantitative semantics, using the concept of power series for describing program evaluation, and has been applied in various non-standard models of computation [START_REF] Danos | Probabilistic coherence spaces as a model of higher-order probabilistic computation[END_REF]Pagani et al., 2014, for example).

Aim and contributions. How can geometry of interaction and Taylor-Ehrhard-Regnier expansion interact? What is the GoI for resource calculus? How are paths dynamics related before and after the expansion? Can we expand β-reduction into an infinite parallel step of resource reductions? Is there a linear and non-deterministic GoI for the resource calculus? Can we use it to characterise persistent paths in λ-terms, via expansion? This paper addresses these questions and recounts the interplay between the two aforementioned semantic approaches, exploring both directions of their mutual influence. After having introduced RC (Section 1), we consider the resource interaction nets (RINs), that are the type-restricted translation of resource terms into differential interaction nets (Section 2). We then study the appropriate notion of paths (Section 3) in RINs and their property of persistence, which intuitively is the ability to survive to the graph rewriting until the normal form. We extend the usual definition to deal with the fact that the reduct of a term t is a sum of terms t 1 + . . . + t n . Also, we observe that every path in the net-representation of t i has to be a residual of some path in the net of t, and that the reduction strongly normalises. Thus, we say that a path of t is persistent whenever it has a residual in at least one of the addends of the reduct of (the net of) t. Restricting to the constant type, whose only inhabitant is the value , we have t → + . . . + . Now there is only one persistent path of , the trivial one, therefore we prove that persistent paths of t are as many as persistent paths of its normal form (Theorem 1). Furthermore, we define a suitable GoI for RC, in order to characterise persistence (Section 4). We define the notion of regularity by rL * , a monoidal structure simplifying the dynamic algebra, where exponential modalities (! and ?) become an n-ary variant of the multiplicatives connectives (resp. ⊗ and `), whose premises are not ordered. Morally, they are the sum of those generalised multiplicatives we obtain by considering all the n! permutations of their premises. We weigh paths with objects of rL * , and then consider the sum of the weights of all paths in a RIN. What we obtain is the execution formula for resource nets, which is shown to be invariant under reduction (Theorem 3). Therefore, the construction provides denotational semantics for RC and of the corresponding logic, that is a minimal, propositional and promotion-free fragment of DiLL. From invariance theorem not only we subsume the equivalence of persistence and regularity (Corollary 1), that is the usual result of GoI constructions, but we also show that the number of addends in a normal form is equal to the number of regular paths (Corollary 2). In the last part of the paper, we present proof-nets of the minimal propositional restriction of the multiplicative exponential fragment of linear logic (mMELL), where the typed λ-calculus is encoded. Then we introduce a qualitative variant of Taylor-Ehrhard-Regnier expansion (Section 5), which maps a proof-net, or a path within it, in an infinite sum of simple RINs, or of set of paths within them. Since here this sum is idempotent, the expansion is essentially the infinite set. Also, we define a notion of expanded cut-elimination, a kind of infinite parallel reduction for RINs which reduces together all redexes that are copied by the expansion (Section 6). The commutativity of the expansion of the reducts and the reduction of the expansion over paths is proved in Theorem 4. Therefore, the property of being persistent can be transferred along expansion: a path persists to MELL reduction if and only if there is a path in its expansion which persists to RIN reduction (Theorem 5). Lastly, we exploit these last results to define a variant of the execution formula for the λ-calculus based on the GoRI -if we assign to every path π in a proof-net the infinite sets of rL * -weights belonging to expansions of π, we obtain an expanded formula enjoying the properties of our interest: invariance (Theorem 6) hence characterisation of persistence (Corollary 3). Related works. A GoI construction for differential interaction nets (DINs) [START_REF] Ehrhard | Differential interaction nets[END_REF] has already been formulated [START_REF] De Falco | The geometry of interaction of differential interaction nets[END_REF]. Besides the similarities in the technical setting of DINs, the geometry of resource interaction turns out to be simpler and more effective, mainly thanks to: (1) the restriction to closed and groundtyped resource nets, (2) the associative syntax we adopted for exponential links, and (3) the stronger notion of path we use. The first simplifies the shape of persistent paths, because it implies that they are palindromes -they first start from the root of the net, then travel until to a link representing the constant term , and finally return to the root -and unique in every normal net/term. The second simplifies the management of the exponential links, because it ensures associativity and delimits their dynamics in only one pair of links, while in De Falco's work this property was completely lost and the system more verbose. In the latter paper, the author uses binary exponential links and introduces a syntactical embedding of the sum in nets by mean of binary links of named sums, and then recover associativity with an equivalence on nets. Compared to ours, De Falco's choice results in a drastically more complex GoI construction, even though he suggests possible extensions of his approach with promotion (corresponding to the full differential λ-calculus) or even additives. The third ingredient allows us to consider full reduction, i.e. including the annihilating rule, while De Falco studied a "weak" variant, where that kind of redexes are frozen, and the GoI only characterises the corresponding notion of "weak-persistence". Indeed, we restrict to paths that cross every exponential in the net and prove this assumption not being a limitation, since it is always true, in case of persistence. Thus whenever t → 0 a path necessarily crosses the annihilating redex, and the dynamic algebra is able to detect it. In an inspiring paper (Ehrhard and Regnier, 2006a) Taylor expansion was already shown to commute with head-reduction normalisation. In particular, the authors proved that for any ordinary term t, the set of resource terms obtained by expanding the Böhm tree of t is equal to the set of any non-zero normal form of the expansion of t. Their proof is based on a operational view on the correspondence with a modified Krivine's machine [START_REF] Krivine | A call-by-name lambda-calculus machine[END_REF]. For simply typed terms, the aforementioned Theorem 4 of this paper generalises such commutation property to any reduction sequence and to any choice of strategy, and is more directly formulated and proved on paths. This paper extends with Section 5-7 a previous work [START_REF] Solieri | Geometry of resource interaction -a minimalist approach[END_REF] by the author, who is grateful to Michele Pagani and Stefano Guerrini for their advice, to Lionel Vaux and Laurent Regnier for interesting discussions, and to anonymous reviewers of this paper for numerous comments and suggestions.

Resource calculus

The resource calculus (RC) is, on one hand, a linear and thus finitary restriction of the λcalculus: in the application t S the function t must use exactly once each s belonging to the multiset of arguments S, i.e. s cannot be duplicated nor erased, so every reduction enjoys strong normalisation. On the other hand, RC adds non-determinism to such restriction of the λ-calculus, since arguments are now finite multisets of ordinary terms. Therefore, the reduct of t S is defined as the superposition, i.e. a sum, of all the possible ways of substituting each s ∈ S. In particular, the number of arguments provided to a function can be insufficient or excess the function's request, i.e. the number of occurrences of the variable bounded by the abstraction under consideration. In this case, computation is deadlocked and the application reduces to 0.

In this section until in Subsection 5.1, where we present proof-nets of the minimal propositional fragment of MELL (mMELL), we shall avoid to repeat the "resource" naming of terms, interaction nets, reduction, paths and and other notions that are identically named in the two systems.

Definition 1 (Syntax). Let V be a denumerable set of variable symbols x, y, z, . . .. Then, the set ∆ of simple terms and the set ∆ ! of simple polyterms are inductively and mutually generated by the following grammars.

∆ : M

::= | V | λV.M | M B ∆ ! : B ::= 1 | [M] | B • B (1)
Where is the constant dummy value, 1 is the empty multiset, brackets delimit multisets, and • is the multiset union (associative and commutative, has 1 as neutral element). So that ( Definition 2 (Reduction). A redex is a simple term of the form (λx.s)T . Let the i-th free occurrence of x appearing in s to be uniquely indexed with a natural number as x @i , with 1 ≤ i ≤ for m being the number of occurrences. The reduction is the relation → between polyterms obtained by the context closure and the linear extension to sums of the following elementary reduction rule.

[x]•1)•[y] = [x,
(λx.s) [t 1 , . . . , t n ] →      σn∈Sn s {t 1 /x @σn(1) , . . . , t n /x @σn(n) } if n = m 0 if n = m (2)
Where S n denotes the set of permutations over the set {1, . . . , n}, and {t/x} is the usual capture-avoiding substitution.

Notation 1 (Rewriting). We fix some quite usual notational conventions employed for rewriting notions. Given a rewriting relation → on a set A, the symbols → + and → * respectively denote the transitive and the transitive-reflexive closures of →. Given a, a ∈ A, if a → a (resp. a → * a ) we say that there is a rewriting step (resp. sequence) from a to a . Also, if a sequence is made of k steps, we write → k . We write a → and say that a is a normal form, when there exists no a such that a → a . If a → * a →, then we say that a is a normal form of a; if a is unique † we also write NF(a) = a . Reduction steps are named with Greek letters ρ, σ, τ, . . ., and sequences with barred letters, so that we can denote the reduct of a with respect to a step ρ (resp. a sequence ρ) as ρ(a) (resp. ρ(a)).

Example 1. Let I = I = λx.x @1 and also let t

= λf.f @1 [f @2 [ ]]
, where occurrences of † It is the case for all reductions we consider here. See Proposition 1 and 2.

f have been subscripted in order to distinguish them. Then we have:

t[I, I ] → f 1 [f @2 [ ]]{I/f @2 , I /f @2 } + f 1 [f @2 [ ]]{I/f @2 , I /f @1 } = I[I [ ]] + I [I[ ]] → 2 I [ ] + I[ ] → 2 2 = NF(t[I, I ])
Note also a case of annihilation in t[I] → 0. Finally, observe that if s = (λx. )T → then T must be 1 (otherwise s → 0).

Proposition 1. Resource reduction is confluent and strong normalising [START_REF] Pagani | Parallel Reduction in Resource Lambda-Calculus[END_REF][START_REF] Ehrhard | The differential lambda-calculus[END_REF].

Resource nets

From an operational point of view, a net can be seen as a graphical, finer representation of typed terms by means of a syntax extending linear logic proof-nets, where negative exponential links have a symmetrical dual. From a proof-theoretic point of view, a net is a proof of a minimal, propositional, promotion-free fragment of differential linear logic [START_REF] Ehrhard | Differential interaction nets[END_REF]. Our presentation of resource nets employs a concise syntax [START_REF] Mazza | The Separation Theorem for Differential Interaction Nets[END_REF] which belongs to the tradition of the so-called nouvelle syntaxe for linear logic proof-nets, and many technical solutions are inspired by Tranquilli's careful work (2001) on the more general setting of differential nets, that includes also promotion rule and boxes.

Pre-nets

Definition 3 (Links). Given a denumerable set of symbols called vertices, a link l is a triple (P, K, C), where: P is a sequence of vertices, called premisses; K is a kind, i.e. an element in the set { , , ¯ , !, ?}; C is a singleton with a vertex, called conclusion, disjoint from P . A link l = ((u 1 , . . . , u n ), κ, {v}) will be denoted as u 1 , . . . , u n (κ) v , or depicted as in Figure 1. We shall also write P (l), K(l) and C(l) to denote the three components of l. When v ∈ P (l) ∪ C(l) for some vertex v and link l, we write that v is connected by l, or simply that v ∈ l. The arity of a link l is the length of its premisses' sequence, and as shown in Figure 1, it is determined by K(l) when it is different from ! and ?, which instead have arbitrary finite arity. Links of these last kinds are exponential links, and are respectively called co-contraction and contraction or, when their arity is 0, co-weakening and weakening. In the same figure it is shown that l assigns to its connected vertices a polarity, that is one of the two elements in {in, out}, where each one is said to be the opposite of the other. By extension, the polarity of a link is that of its conclusion. In graphical representations, vertices of a link shall be placed following the usual convention for λ-calculus graphs (outs on the top, and ins on the bottom); exiting arrows mark conclusions vertices, while premisses have entering ones. is the only ground type. A typing function T is a map from vertices of a link to types. If l = u 1 , . . . , u n (K(l)) v is a link, and A, B are types, then T respects the following constraints.

v out ( ) v out v out u in 2 u out 1 u out 1 , u in 2 ( ) v out ¯ u out 2 u in 1 v in u in 1 , u out 2 ( ¯ ) v in ! v out u in 1 u in n . . . u in 1 , . . . , u in n (! ) v out ? u out 1 u out n v in . . . u out 1 , . . . , u out n (?) v in
-If K(l) = , then T (v) = . -If K(l) = or ¯ , then T (v) = A B with A = T (u 1 ) and B = T (u 2 ). -If K(l) = ? or !, then T (v) = !A, where A = T (u i ) for all 1 ≤ i ≤ n.
Definition 5 (Pre-nets). A simple pre-net P is a triple (V, L, T ), where V is a set of vertices, L is a set of links and T a typing function on V , such that for every vertex v ∈ V the followings holds:

1 there are at least one and at most two links l, l such that l v ∈ l , and when there is only one, then v is called a conclusion of P; 2 the set C(P) of conclusions contains exactly one vertex u with out polarity, and if u is the unique element of C(P) then P is called closed ; 3 if l v ∈ l , then l, l associate opposite polarities to v; in particular, v is called a cut when C(l) = v = C(l ), and an axiom when P (l) v ∈ P (l ).

We shall also write V (P) and L(P) to denote the first and second component of P, respectively. The type of a pre-net P is the type T = T (v), where v ∈ C(P) of out polarity, written P : T . The interface I(P) of a simple pre-net P is the set, for all v ∈ C(P), of the ordered pair (T (v), p) where p is the polarity of v. A pre-net P of interface I is a linear combination c 1 P 1 + . . . + c n P n of simple pre-nets on the semiring N where for any 1 ≤ i = j ≤ n, we have: V (P i ) ∩ V (P j ) = ∅ and I(P i ) = I. We shall simply use 0 to denote each of the empty sums of pre-nets having the same interface I, for every interface I. Two simple pre-nets P, Q are equal when there exists a type-preserving isomorphism such that P Q. Let P = c 1 P 1 +. . .+c n P n and Q = d 1 Q 1 +. . .+c m Q m be two pre-nets. We say P = Q when there is a bijection ∼ between the non-zero addends of P and those of Q such that if c i P i ∼ d j P j , then c i = d j and P i Q j .

Term translation and net reduction

As in the usual translation of the simply typed λ-calculus into MELL proof-nets [START_REF] Girard | Linear logic[END_REF], the -link is used to translate λ-abstraction, the ¯ -link for application, and the ?-link for contracting together all the occurrences of the same variable. In addition, we use !-link for polyterm and formal sum of nets for. . . formal sum of terms.

Γ = v x@i Γ = Γ(x@i) λx.t Γ = t Γ v ? u1 u2
Definition 6 (Term translation). Let t be a simple term, and Γ an injection between the variable occurrences in t and a set of vertices V . The translation t Γ is a pre-net whose vertices is a superset of V and that is defined in Figure 2. The actual work is performed by the pre-translation of t, denoted as t Γ , which goes by induction on the syntax of t; while the final step only adds a ?-link linking all occurrences of a given free variable x, for all free variables of t. Since the choice of Γ produce no change in the translation, we shall omit to specify it. Moreover, a linear combination of simple terms is translated as the same linear combination of their translation, i.e.: c 1 t 1 + . . . + c n t n = c 1 t 1 + . . . + c n t n .

Remark 1. A pre-net translation is always defined for simple terms while it is not for general terms, because of possible incompatibilities in the interfaces of translated addends.

Definition 7 (Resource permutations). Given a simple pre-net P, a resource permutation σ P is a function from the set of !-links in P, to n∈N S n , where S n is the group of permutations over the set {1, . . . , n}, such that: if a !-link l has arity m, then σ(l) is an element σ m of S m . We shall write σ l for σ P (l) and denote the set of resource permutation of P as S P .

Definition 8 (Contexts, redexes and reduction). Recall that a vertex w in a simple pre-net is a cut if it the conclusion of two links l, l . The redex of w is the pair l, l . The reduction → is the graph-rewriting relation on pre-nets defined by closing with respect to contexts the relation given by the two rules in Figure 3, which maps simple pre-nets into pre-nets. Namely, if according to that figure P → P (where P may be a simple net), then C[P] → C[P], for any context C[ ]. In Figure 3, [v ≡ u] denotes the fact that the two vertices v, u have been equated. Other notational conventions have been previously fixed in Notation 1.

¯ u u v v w → • v ≡ u • v ≡ u ? ! v1 . . . vn u1 . . . um w n=m --→ σn∈Sn • v1 ≡ v σn(1) . . . • vn ≡ v σn(n) 0 n =m ← --
Definition 9 (Resource interaction nets). Let t ∈ N ∆ and t → * N , for a pre-net

N = c 1 N 1 + . . . + c n N n . Then each N i is called a simple net and N a net.
Proposition 2. Net reduction simulates term reduction and strongly normalises. [START_REF] Tranquilli | Intuitionistic differential nets and lambda-calculus[END_REF], on the promotion-enabled generalisation of RINs and RC).

Example 2. Consider δ = λx.x @1 [x @2 ] and notice δ is not defined, because of the lack of adequate typing function. Recall the terms I = λx.x @1 and t = λf.f @1 [f @2 [ ]] from Example 1; we now explain Figure 4, which shows the translations of these terms as nets, and provides an example of net reduction. On the left extremity: I is closed and I : ! . On the middle left: N : is not a translation of a term, but it is a net, because t[x, y] → N by eliminating a linear implication cut. Also, N is not a closed net, because it has three conclusions: v 1 , z 1 , z 2 . On the right side: an exponential reduction step involving index permutation, that rewrites N as a sum of two normal simple nets. In order to stress the fact that addends do not share vertices, those of the rightmost addend have been labelled differently from the leftmost one. Observe the reduct is equal to

x[y[ ]] + y[x[ ]] . Consider λf.f @1 [f @2 [ ]][I, I]
, that is a closed net of type , and observe the reduct M of the only linear implication cut that is depicted in Figure 5 (with the same vertex notation as before). The normalisation requires: one exponential step (on the left), two linear implication steps per addend (on the right), and finally two other exponential steps per addend (omitted) to reach the net ( )

v 1 ≡ v 8 + ( ) v 1 ≡ v 8 = 2 .

Paths

Path statics

We introduce some basic definitions about paths, where the most notable characterise those where the computation is visible (straightness) in its entirety (maximality and ?

N = I = w1 ? w2 w3 v1 ¯ ! ¯ ? ! ! z2 z1 v2 v4 v5 v6 v7 v3 v8 → v1 ¯ ! ¯ ! v2 ≡ z2 v6 ≡ z1 v4 v5 v7 v8 + v 1 ¯ ! ¯ ! v 6 ≡ z 2 v 2 ≡ z 1 v 4 v 5 v 7 v 8
z 2 z 3 v 1 ¯ ! ¯ ! v 2 ≡ z 1 v 4 v 5 v 6 ≡ w 1 v 7 v 8 → 4 v1 ≡ w2 ? ! ? ! w3 ≡ v4 v5 ≡ z2 z3 ≡ v7 v8 + v 1 ≡ z 2 ? ! ? ! z 3 ≡ v 4 v 5 ≡ w 2 w 3 ≡ v 7 v 8
Fig. 5: Example: nets reduction. Rightmost reduction is made of four steps, two on each addend.

comprehensiveness). This last notion is the only substantial difference with respect to the classic restrictions for paths in proof-nets [START_REF] Danos | Proof-nets and the Hilbert space[END_REF]. A superficial technical difference is the choice of using concatenation instead of composition as the basic relation on paths.

Definition 10 (Path). Given a simple net N , two vertices u, w

∈ N are connected, if there is a link l ∈ N s.t. u, w ∈ l. A path π = (v 1 , . . . , v n ) with n > 0 in N is a sequence of vertices s.t. for all i < n, the vertices v i , v i+1 are connected. We call π trivial if its length is 1, atomic if it is 2
, and remark that in the latter case π crosses exactly one link. If π crosses consecutively the same link l, then π is called bouncing. If l is not a -link and

π crosses l through v i , v i+1 such that v i , v i+1 ∈ C(l) or v i , v i+1 ∈ P (l), then π is twisting. When π is not bouncing nor twisting, π is straight. Moreover, π is maximal if there is no other path π ∈ N s.t. π ⊆ π ,
where ⊆ is the inclusion ordering on sequences. Also, π is comprehensive when it crosses all the premisses of all the exponential links. Finally if π is both straight and maximal, then π is an execution path. In a net N , we denote with P(N ) the set of straight paths in any simple N addend of N , while P E (N ) is the set of execution paths, and P EC (N ) is the set of comprehensive execution paths.

Given π = (v 1 , . . . , v n ) and φ = (u 1 , . . . , u m ) in P(N ), we denote the reversal of π by

π † = (v n , . . . , v 1 ). If v n = u 1 then the concatenation of φ to π is defined as π :: π = (v 1 , . . . , v n = u 1 , . . . u m ). If π ∈ P(N ) and φ ∈ P(M), we say π = φ when N = M and, if is the isomorphism such that N M, then v i u i , for any 1 ≤ i ≤ n = m.
Example 3. Recall the nets discussed in Example 2 and observe again Figure 4. Consider the net I and the path φ = (w 1 , w 2 , w 3 ), which is straight and also maximal. Moreover, P E ( I ) = {φ, φ † }. Notice that in N the paths (v 1 , v 4 ) and (v 1 , v 2 , v 1 ) are not straight -the former is twisting, while the latter is bouncing. What about P E (N )? If we start from v 1 we find two paths seeking for the head variable:

π 1 = (v 1 , v 2 , v 3 , z 1 ) and π 2 = (v 1 , v 2 , v 3 , z 2 ).
Both π 1 , π 2 are straight and maximal, thus execution, but they are not comprehensive, since they do not cross v 4 nor v 7 .

Path dynamics

With the notions just introduced we now define the property of path persistence, that intuitively means "surviving cut-elimination". We first inspect the action of reduction on paths, and isolate the notion of residual of a given path with respect to a given reduction. We shall go by induction on its subpaths that pass through a given redex, called crossings, and say that the residual(s) of a path are obtained by the substitution of the crossing with its residual(s), that are the images of reduction as naturally induced by the graphrewriting. The case of linear implication is straightforward, because the rewriting is local and we only have to ensure that a path does not partially belong to the redex. The case of exponentials is instead more delicate, because the rewriting is global: a simple net is rewritten as a sum of simple nets, hence a path may be duplicated in several addends or destroyed. Which addends contain the residual(s) of a given crossing of the redex? If the reduction of an exponential redex R rewrites the simple net to which it belongs as the empty sum, then also the residual of the crossing is 0. Otherwise, the reduction rewrites the net as a sum of simple nets where any crossing always has a residual (cf. Definition 8). But two crossings of R within a path may have residuals in different simple nets created by the reduction, each one obtained from a fixed permutation of premisses to substitute R. Therefore, the residual of a path is a sum of paths, morally varying on the set of permutations they are allowed to follow.

Definition 11 (Crossing). Given a net N and a reduction ρ on a redex R, we say a path π ∈ P(N ) is long enough for R when neither its first nor its last vertex is the cut vertex in R. A crossing of R is a maximal sub-sequence of π entirely contained in R. If π is long enough for R, we can express π in the redex crossing form of π for R, i.e. RCF R (π) = π 0 :: χ 1 :: π 1 :: . . . :: χ k :: π k , where for any 1 ≤ l ≤ k, the sub-path χ l is a crossing of R.

Definition 12 (Linear implication residual). Let N be a net where χ ∈ P(N ) is a crossing of a linear implication redex R. Suppose R as in the leftmost redex of Figure 3, and let ρ be the reduction step on R. Then the residual of χ with respect to ρ, is defined as follows and by the rule ρ(χ

† ) = (ρ(χ)) † . ρ((v, w, u)) = (v) (3) ρ((v , w, u )) = (v ) (4) ρ((v, w, u )) = 0 (5) ρ((v , w, u)) = 0 (6)
Let π ∈ P(N ) such that RCF R (π) = π 0 :: χ 1 :: π 1 :: . . . :: χ k :: π k . Then:

ρ(π) = π 0 :: ρ(χ 1 ) :: π 1 :: . . . :: ρ(χ k ) :: π k if for any i, ρ(χ i ) = 0 0 otherwise (7)

Fix definition

Definition 13 (Exponential residual). Let N be a net where χ ∈ P(N ) is a crossing of an exponential redex R. Suppose R as in the rightmost redex of Figure 3, and let ρ be the reduction step on R and σ n ∈ S n . The residual of χ with respect to ρ and σ n is defined as follows and by rule ρ(χ † ) = (ρ(χ)) † . For any 1 ≤ i ≤ n, and 1 ≤ j ≤ m:

ρ σn ((v i , w, u j )) = (v i ) if n = m, and σ n (i) = j, 0 if n = m, or σ n (i) = j; (8)
where in V (ρ(R)) we have that v i ≡ u σn(i) . Now, similarly to the last definition, given π ∈ P(N ) such that RCF R (π) = π 0 :: χ 1 :: π 1 :: . . . :: χ k :: π k , we define the residual of π with respect to σ n :

ρ σn (π) =     
π 0 :: ρ σn (χ 1 ) :: π 1 :: . . . :: ρ σn (χ k ) :: π k if n = m, and for all 1 ≤ l ≤ k, ρ σn (χ l ) = 0; 0 otherwise.

(9)

Notice that ρ σn (π) may be 0 even if k = 0, i.e. when π does not cross R. Finally, we can define the residual of π as the sum of all the residuals, for any σ n :

ρ(π) = σn∈Sn ρ σn (π). ( 10
)
Definition 14 (Reduction and persistence). For a given reduction step ρ, the path reduction function w.r.t. ρ is the function, written ρ, that maps a path π in N to the residual of π, i.e. a sum of paths in ρ(N ). If ρ(π) = 0, then π is persistent w.r.t. ρ. If, for every reduction sequence ρ = (ρ 1 , . . . , ρ m ), and for every 1 ≤ i ≤ m, the path π is persistent w.r.t. ρ i , then π is persistent.

Example 4. Recall the nets discussed in Example 2 and let ρ be the reduction illustrated in Figure 4, where we will denote by N l and N r the left and right addend of the reduct, respectively. Observe the execution paths

π 1 = (v 1 , v 2 , v 3 , z 1 ) and π 2 = (v 1 , v 2 , v 3 , z 2 ), mentioned in Example 3. Both are persistent, since: NF(π 1 ) = π 1r = (v 1 , v 2 ≡ z 1 ) and NF(π 2 ) = π 2 l = (v 1 , v 2 ≡ z 2 ).
Remark also that π 1 , π 2 cross the exponential redex differently, and they do not belong to the same addend of the reduct, for π 1r ∈ N r , while π 2 l ∈ N l . Also, if we begin with the in conclusion z 1 , which morally represents a free variable, we find straight paths that search for the argument to be substituted there, eventually reaching the out conclusion. Consider π 3 = (z 1 , v 3 , v 2 , v 4 , v 5 , v 6 , v 3 , z 1 ). It crosses the same exponential redex with two crossings, namely (z 1 , v 3 , v 2 ) and (v 6 , v 3 , z 1 ), that are incompatible since they belong to different permutations. Therefore π 3 not persistent, as it morally uses the same variable twice, for both the applications in N .

Fact 1. Straightness, maximality and comprehensiveness are preserved by reduction.

Comprehensiveness and bijectivity

The persistence property of a path naturally implies that it travels only through vertices whose links morally contributes to the normalisation -a persistent path cannot cross (co-)weakenings ‡ . Therefore, if we restrict ourselves to closed nets of constant type, we obtain a stronger property: a persistent execution path travel through all vertices of the net that are not conclusions of a 0-ary exponential links. Despite what the creation of sums may suggest at a first glance, RINs do not allow for duplication of paths: the set of persistent ones are intuively splitted from the simple net containing the redex into the addends created by the reduction. We shall show indeed that path reduction for any step ρ induces a bijection between the persistent paths of a net N and those of ρ(N ).

To prove these two facts, we first explicit in the next lemma an expected property: the alternation between multiplicative and exponential operators that lies in the grammar of types has a natural and graphical counterpart in links of nets.

Lemma 1. In a closed net, a non-cut vertex v is the conclusion of an exponential link if and only if v is the first premiss of multiplicative link.

Proof. Given Definition 9 of nets, we proceed by induction on the length of the reduction sequence ρ : t → * N , for some term t.

1 Base. Suppose |ρ| = 0. Observe first, that the syntax of terms (Definition 1) and the typing constraints (Definition 4) of their translation into nets (Definition 6), forces t to have the out conclusion r typed either with or with , otherwise t would be a polyterm, contradicting the hypothesis. Therefore, a vertex that is the conclusion of an exponential link or the first premiss of a multiplicative one, cannot be r, nor any another in conclusion of t , because, since t is closed, there are not. Secondly, an immediate verification of the definition of translation shows that the statement holds for t , since: a -link and a ?-link are introduced when pre-translating an abstraction; a ¯ -link and a !-link are introduced when pre-translating an application and the polyterm; and in both cases the statement holds. 2 Step. Suppose |ρ| > 0 and let ρ = ρ ρ , for some reduction sequence ρ , and for some step ρ of our interest acting on a redex R. For any z / ∈ R the inductive hypothesis ‡ The remark can be generalised also to GoI constructions for non-linear calculi, such as the ordinary λ-calculus or MELL proof-nets, where an abstraction with no occurrences of the bound variable may erase its argument, or a weakening may erase the box that is cut with.

(IH) is trivially preserved. So let us focus on R and distinguish two cases depending its type.

(a) T (R) = / ¯ . Let R = u, v ( ) w , u , v ( ¯ ) w . By IH, since v and v are the first premisses of two multiplicative links, they must be conclusions of a ?and a !-link, respectively. Now, in ρ (R) we have the vertex v ≡ v , where the claim trivially holds since it is a cut.

(b) T (R) = !/?. Let R = v 1 . . . v n (?) w , u 1 . . . u m (! ) w . If n = m then ρ (R) = 0
and there is nothing to prove, so let us assume otherwise. We show that no vertex z in R can satisfy any of the two statements whose co-implication is claimed.

i If z = w, then it is a cut. Moreover, z cannot be the premiss of any link, since in R there are already two links connected to z, (cf. Definition 5, item 1).

ii If z = v i (or z = u i ) for some 1 ≤ i ≤ n, then we observe that it cannot be the conclusion of an exponential link l, nor the first premiss of a multiplicative link l , since it would violate the typing constraints. Indeed, it must be the case that T (z) = !A, where either A = T (x) and x is any premiss of l, or !A B = T (y) and y is the conclusion of l . This would require that T (w) = !!A, which does not belong to the grammar of types (cf. Definition 4).

Lemma 2. In a closed net N : any persistent execution path is comprehensive.

Proof. We shall prove a stronger statement: given a persistent path π ∈ P E (N ), a vertex v / ∈ π if and only if there exists a (co-)weakening l such that v ∈ C(l).

-The "if" direction of the claim follows from a mere observation of the Definition 10 of execution paths. If π includes a conclusion of a (co-)weakening, then π is necessarily bouncing or non-maximal, in both cases contradicting the hypothesis that π is an execution path. -In order to prove the "only if" part of the claim, let us first recall that, by Definition 9, for any simple net N there exists a term such that N either appears in its translation, or in some of its reducts. We now go by induction on a sequence (ρ) -1 of expansions (or an anti-sequence of reductions) from NF(N ) back to N = t , for some term t. If NF(N ) = 0 there is nothing to prove, so we shall assume it to be non-zero.

1 Base. Suppose |ρ| = 0. Then NF(N ) = N = t . Therefore t = , because the only closed term whose translation is normal with respect to net reduction is .

Then N = ( ) v , and

P E (N ) = {(v, v)}, hence the claim.
2

Step. Suppose |ρ| > 0. Let ρ : N → N and N → * NF(N ). Also, let R be the redex eliminated by ρ, and C[ ] its context. We then distinguish two sub-cases depending on the type of R.

(a) T (R) = / ¯ . Suppose N to be an addend of N containing the vertices v ≡ v 1 ≡ v 2 and u ≡ u 1 ≡ u 2 , and assume N to be the addend of N containing u, v. Let the expansion step be the following, which introduces the distinct vertices v 1 , v 2 , u 1 , u 2 , w.

N = C[u 1 ≡ u 2 , v 1 ≡ v 2 ] ← C[ u 1 , v 1 ( ) w , u 2 , v 2 ( ¯ ) w ] (11)
We firstly assume that π ∈ N , because otherwise π is unaffected and the IH would be trivially preserved. Now v 1 , v 2 are second premisses of the cut links, therefore, as established by Lemma 1, they cannot be the conclusion of a (co-)weakening, and consequently neither v can. Hence, by IH, v ∈ π and it is enough to observe, by Definition 12, that also v 1 , v 2 ∈ ρ -1 (π). Let's now discuss u. Observe first that, since u 1 and u 2 are first premisses of multiplicative links, we know from Lemma 1 that they both must be conclusion of exponential links. Therefore, and by definition of reduction, u has to be an exponential cut. We distinguish two sub-cases.

i If u / ∈ π, then by definition of path reduction, u 1 , u 2 / ∈ ρ -1 (π). Moreover, by IH we have that u the conclusion of a weakening or a co-weakening link.

A If u is the conclusion of a weakening, then observe that the co-contraction whose conclusion is u must have arity 0. Otherwise, the reduction of u would rewrite N as 0, contradicting the persistence hypothesis for π.

B If instead u the conclusion of a co-weakening, then, dually with respect to the previous case, and for the same reductio ad absurdum, the contraction that has conclusion in u must have arity 0.

Hence, in both cases u is a cut between 0-ary exponentials, which by definition of reduction implies that u 1 , u 2 are respectively conclusions of a weakening and a co-weakening link.

ii Otherwise, u ∈ π. Then again by inspection of Definition 12, we verify that u 1 , u 2 ∈ ρ -1 (π).

(b) T (R) = !/?. If the expansion affects no addends, i.e. if the reduction rewrites as 0 a simple net in N , then π is unaffected, since we assumed it to be persistent, and IH is trivially preserved. Otherwise, the arity of the two exponential links are equal, so let ρ be as follows.

C σn∈Sn v 1 ≡ u σn(1) , . . . , v n ≡ u σn(n) ← C [ v 1 , . . . , v n (! ) w , u 1 , . . . , u n (?) w ] (12)
i If n = 0, and the reduct of the redex is empty, then trivially π cannot not cross it. Nor can cross the redex, since the redex is made by a wakening and a co-weakening link, and we supposed π maximal and persistent.

ii If n > 0, then let σ n ∈ S n and consider the vertex v i ≡ u σn(i) . Notice that it cannot be the conclusion of a 0-ary exponential link. By contraposition, suppose otherwise and notice that, by definition of typing, in the reducendum we would have T (v i ≡ v σn(i) ) = !A for some type A. This would absurdly imply T (w) = !!A, that is not a valid type. Not being a (co-)weakening conclusion, by IH we have that v i ≡ u σn(i) ∈ π. To conclude it is then sufficient to observe that by definition of reduction, either (v i , w, v σn(i) ) or its reversal belong to ρ -1 (π).

Theorem 1. For any closed net N : , every reduction step ρ induces a bijection between execution paths in N that are persistent to ρ and those in ρ(N ).

Proof. Let π ∈ P E (N ) be persistent to ρ, let R the redex of ρ, and suppose RCF R (π) = π 0 :: χ 1 :: π 1 :: . . . :: χ k :: π k . There are two reduction rules possibly used by ρ.

1 T (R) = / ¯ . Because of the persistence of π to ρ, and by the definition given by Equation 7, we have χ l = 0, for all 0 ≤ l ≤ k, and ρ(π) = π 0 :: ρ(χ 1 ) :: π 1 :: . . . :: ρ(χ k ) :: π k . Then, if ρ is as in Figure 3, the bijection is given as follows:

(a)

χ l = (v, w, u) if and only if ρ(χ l ) = (v); (b) χ l = (v , w, u ) if and only if ρ(χ l ) = (v ).
Such a bijection holds between χ l and ρ(χ l ), so we also have a bijection between π and ρ(π). 2 T (R) = !/?. Suppose the redex R being as in Figure 3. Because of the persistence of π to ρ, and by the definition given by Equation 9and 10, it must be the case that n = m and that there exists a permutation σ n ∈ S n such that for all 0 ≤ l ≤ k, we have ρ σn (χ l ) = 0. Moreover, by Lemma 2, π is comprehensive, which in particular means that v i , u j ∈ π for any 1 ≤ i, j ≤ n. Hence, for any 1 ≤ i ≤ n there exist 0 ≤ l ≤ k and 0 ≤ j ≤ n such that χ l is either (v 1 , w, u j ) or its reversal. In both cases, by Equation 8, it must be the case that σ n (i) = j so that ρ σn (χ l ) = (v σn(i) ≡ u j ). This means that σ n is unique, and for any other σ n we have ρ σ n (π) = 0. We then obtained a one-to-one correspondence between π and ρ(π).

Confluence and persistence

Since reductions on both RC and on RINs enjoy local confluence, the property is easily verified also on path reduction. This implies that persistence of a path with respect to a normalisation sequence is a sufficient condition for its general persistence.

Lemma 3. Let N be a resource net and let π ∈ P E (N ). For any two reduction steps ρ, σ on N , there exist two sequences ρ, σ such that ρ(σ(π)) = σ(ρ(π)).

Proof. Let R, S be the respective redexes of ρ and σ, and let N , M be the simple nets to which R, S respectively belong.

1 If N = M, then let N = M + N + M. By Definition 8 of reduction, ρ(N ) = M + ρ(N ) + M and σ(N ) = M + N + σ(M). Therefore R ⊂ σ(N ) and S ⊂ ρ(N ).
Let ρ be the reduction step acting on R within σ(N ) and let σ be that on S within ρ(N ). We immediately obtain that ρ(σ(N )) = M + ρ(N ) + σ(M), and σ(ρ(N )) = M + ρ(N ) + σ(M), which are equal as claimed. 2 If N = M, then consider the partitioning of π obtained by iteratively isolating: first the longest prefix π which does not cross S, then the longest prefix π which does not cross R. π = π 1 :: π 1 :: . . . ::

π h :: π h (13) By definition of reduction, R, S are disjoint, i.e. if R v ∈ S then I(R) v ∈ I(S).
This means that π i , π i , for any 1 ≤ i ≤ h, are long enough respectively for R, S. Therefore, we can highlight RCF R (π i ) and RCF S (π i ) within Equation 13and obtain a combined redex crossing form of π for R, S:

RCF R,S (π) = π 0,0 :: χ 1,1 :: π 1,1 :: . . . :: χ 1,r1 :: π 1,r1 ::

ψ 1,1 :: π 1,r1+1 :: . . . :: ψ 1,s1 :: π 1,r1+s1 :: . . . χ h,1 :: π h,1 :: . . . :: χ h,r h :: π h,r h ::

ψ h,1 :: π h,r h +1 :: . . . :: ψ h,s h :: π h,r h +s h ( 14
)
where χ i,j (resp. ψ i,j ) is the j-th crossing of R (resp. of S) within π i (resp. π i ). We distinguish three cases, depending on the kind of redexes.

(a) T (R) = T (S) = / ¯ . Recall that R, S are disjoint, and observe that by Definition 8 of net reduction, both ρ and σ rewrite N as a simple net. Thus, S ⊂ ρ(N ) and R ⊂ σ(N ). This means that we can simply take ρ = ρ reducing R and σ = σ reducing S. We immediately verify the claim by applying Definition 12 of multiplicative residual to Equation 14.

σ(ρ(π)) = ρ(σ(π)) = π 0,0 :: ρ(χ 1,1 ) :: π 1,1 :: . . . :: ρ(χ 1,r1 ) :: π 1,r1 ::

σ(ψ 1,1 ) :: π 1,r1+1 :: . . . :: σ(ψ 1,s1 ) :: π 1,r1+s1 :: . . . ρ(χ h,1 ) :: π h,1 :: . . . :: ρ(χ h,r h ) :: π h,r h ::

σ(ψ h,1 ) :: π h,r h +1 :: . . . :: σ(ψ h,s h ) ::

π h,r h +s h (15)
(b) T (R) = / ¯ and T (S) = !/?, or T (R) = !/? and T (S) = / ¯ . We assume the former, since the proof is identical once the roles of R and S are swapped. Let n be the arity of the ?-link in R. This time ρ rewrites N as a simple net, while σ rewrites it as a sum of n simple nets (cf. Definition 8). Observe again that S ⊂ ρ(N ), so take σ = σ to be the reduction step for such S.

i If n = 0, R is not present in σ(N ) = 0. So, let ρ be the empty reduction sequence. We immediately verify the claim.

ii Otherwise n > 0, which means that R is copied in the n addends of σ(N ) = σn∈Sn σ σn N . To close the reduction diagram, we then have to reduce all the duplicates of R. So, let us denote the sum of reducts of R as σn∈Sn R σn , and consider the set, for any σ n ∈ S n , of the reduction step ρ σn which reduces R σn . Let ρ be the sequence obtained by any ordering on that set. We can now unfold Definition 12 and Definition 13 of exponential residual onto Equation 14. σ(ρ(π)) = σn∈Sn π 0,0 :: ρ(χ 1,1 ) :: π 1,1 :: . . . :: ρ(χ 1,r1 ) :: π 1,r1 :: σ σn (ψ 1,1 ) :: π 1,r1+1 :: . . . :: σ σn (ψ 1,s1 ) :: π 1,r1+s1 :: . . . ρ(χ h,1 ) :: π h,1 :: . . . :: ρ(χ h,r h ) :: π h,r h ::

σ σn (ψ h,1 ) :: π h,r h +1 :: . . . :: σ σn (ψ h,s h ) :: π h,r h +s h (16)
ρ(σ(π)) = σn∈Sn π 0,0 :: ρ σn (χ 1,1 ) :: π 1,1 :: . . . :: ρ σn (χ 1,r1 ) :: π 1,r1 ::

σ σn (ψ 1,1 ) :: π 1,r1+1 :: . . . :: σ σn (ψ 1,s1 ) :: π 1,r1+s1 :: . . . ρ σn (χ h,1 ) :: π h,1 :: . . . :: ρ σn (χ h,r h ) :: π h,r h ::

σ σn (ψ h,1 ) :: π h,r h +1 :: . . . ::

σ σn (ψ h,s h ) :: π h,r h +s h (17)
Comparing the last two equations, we verify immediately that ρ σm (χ i,j ) = ρ(χ i,j ), for any σ n ∈ S n . Ergo ρ(σ(π)) = σ(ρ(π)).

(c) T (R) = T (S) = !/?. Let n, m respectively be the arities of the ?-links in R, S, and let n , m be the numbers of simple nets respectively generated by ρ, σ on N .

We separate three cases depending on the condition of nullity of n , m .

i n = m = 0, which means that n (resp. m) is not equal to the arity of the !-link in R (resp. S). Then clearly ρ(π) = σ(π) = 0, so let ρ and σ both be the empty reduction sequence, and immediately obtain the claim: ρ(σ(π)) = σ(ρ(π)) = 0.

ii Either n or m is null. Suppose the former (the other case is dual), i.e. n = 0 and m > 0. This last fact implies that ρ(π) = 0, so on the one hand, let σ be the empty reduction sequence. On the other hand notice that, as in case 2(b)ii, R is copied by σ into σn∈Sn R σn . So, let ρ be an enumeration of the set including the reduction step ρ σn reducing on R Sn , for all σ n ∈ S n . We then obtain: ρ(σ(π)) = σm∈Sm σn∈Sn π 0,0 :: ρ σm σn (χ 1,1 ) :: π 1,1 :: . . . :: ρ σm σn (χ 1,r1 ) :: π 1,r1 :: σ σn (ψ 1,1 ) :: π 1,r1+1 :: . . . :: σ σn (ψ 1,s1 ) :: π 1,r1+s1 :: . . . ρ σm σn (χ h,1 ) :: π h,1 :: . . . :: ρ σm σn (χ h,r h ) :: π h,r h :: σ σn (ψ h,1 ) :: π h,r h +1 :: . . . :: σ σn (ψ h,s h ) :: π h,r h +s h (18)

where for any σ n ∈ S n , and any σ m ∈ S m , we have ρ σm σn (χ i,j ) = 0. Thus, ρ(σ(π)) = 0.

iii n , m > 0. Let ρ be defined as in sub-sub-case 2(c)ii. Dually, since S is copied by ρ into σm∈Sm S σm , define σ as an enumeration of the set of any reduction step σ σn reducing on S Sm , for all σ m ∈ S m . We obtain: ρ(σ(π)) = σn∈Sn σm∈Sm π 0,0 :: ρ σm (χ 1,1 ) :: π 1,1 :: . . . :: ρ σm (χ 1,r1 ) :: π 1,r1 ::

σ σn σm (ψ 1,1 ) :: π 1,r1+1 :: . . . :: σ σn σm (ψ 1,s1 ) :: π 1,r1+s1 :: . . . ρ σm (χ h,1 ) :: π h,1 :: . . . :: ρ σm (χ h,r h ) :: π h,r h :: σ σn σm (ψ h,1 ) :: π h,r h +1 :: . . . ::

σ σn σm (ψ h,s h ) :: π h,r h +s h (19)
Comparing it with Equation 18, we observe that for any σ n ∈ S n and any σ m ∈ S m , we clearly have ρ σm (χ i,j ) = ρ σm σn (χ i,j ), and σ σn (ψ i ,j ) = ρ σn σm (ψ i ,j ). Hence ρ(σ(π)) = σ(ρ(π)).

Lemma 4. Let N be a resource net and let π ∈ P E (N ). If π is persistent w.r.t. a reduction sequence ρ such that ρ(N ) = NF(N ), then π is persistent.

Proof. Let the rank rk(N ) of a resource net N be the length of the longest reduction sequence on N . Observe that the rank is always finite, since the reduction on RINs is strongly normalising and thanks to Kőnig lemma. So we can go by induction on rk(N ) and show that π is persistent to any normalisation sequence σ.

1 Base: rk(N ) = 0. This implies that |ρ| = 0, which means that NF(N ) = N . Therefore, ρ is the only possible reduction sequence on N . Hence, π is trivially persistent. 2 Step: rk(N ) > 0. Since this implies that |ρ|, |σ| > 0, let ρ = ρ 1 ρ2 and σ = σ 1 σ2 for some reduction steps ρ 1 , σ 1 and reduction sequences ρ2 , σ2 . We can then apply the local confluence property (Lemma 3) on ρ 1 , σ 1 and obtain that there exist two sequences θ, φ such that θ(ρ 1 (π)) = φ(σ 1 (π)). Now, since rk(ρ 1 (N )) < rk(N ) and ρ 1 (π) is persistent w.r.t. the normalisation ρ2 , per IH we have that ρ 1 (π) is persistent. This in particular implies that ρ 1 (π) persists to θ. Moreover, if μ is a normalisation sequence on θ(ρ 1 (π)), then ρ 1 (π) persists to θ μ as well. Therefore, we can apply IH again, because rk( θ(ρ 1 (N ))) < rk(ρ 1 (N )) < rk(N ), and obtain that θ(ρ 1 (π)) is persistent. But φ(σ 1 (π)) = θ(ρ 1 (π)) = 0, therefore this means that σ 1 (π) persists to φ and to φμ. Now rk(σ 1 (N )) < rk(N ), so we can apply the IH one last time and conclude that σ 1 (π) is persistent. Hence, σ 1 (π) persists in particular to σ2 , which means that π is persistent w.r.t. σ 1 σ2 , i.e. w.r.t. σ.

Execution

Dynamic algebra and execution

We are ready to formulate the GoI construction for RINs. We adapt the formulation for the case of MELL as most classically formulated [START_REF] Danos | Proof-nets and the Hilbert space[END_REF], but we characterise our resource exponentials, which have no promotion, as a sort of superposition of n-ary multiplicatives. We define a weight assignment for paths, so that the execution of a net is the sum of the weights of any execution path within it, and we formulate a monoidal structure rL * of weights representing the computation. A crossing of an exponential link is morally weighed with a sum of indexed symbols, where the index varies in the set of permutations of the link's premisses, and exponential weights interacts exactly as multiplicatives ones, i.e. by nullification or neutralisation.

Definition 15 (Dynamic algebra). The rL * monoid is defined over terminal symbols in {0, 1, p, q, l, r, }. A word of its alphabet, called weight, is generated by a binary concatenation operator with infix implicit notation and a unary adjoint operator (•) * . The concatenation operator and the set of symbols has the structure of a monoid, whose identity element is 1, equipped with an additional absorbing element 0 (cf. Figure 6a). Moreover, the inversion operator is involutive and distributes over concatenation by reversing left and right operands (cf. Figure 6b), and satisfies the neutralisation and two annihilation equations in Figure 6c. We denote l r . . . r n as e n , so that for any n = m ∈ N we have e n e * n = 1 and e n e * m = 0.

Definition 16 (Weighting and execution). The permuted base weighting is a map w that associate a weight of rL * to an atomic straight path π = (u, v) ∈ P(N ) and a resource permutation σ. Straightness of π implies that it goes either: (i) from a conclusion to a conclusion of a -link; (ii) from a premiss to a conclusion of a binary link; (iii) vice versa, from a conclusion vertex to a premiss of a binary link. The permuted base weighting is defined as follows, where the first clause covers (i), the clauses from the second to the fifth cover (ii), and the last clause covers (iii).

w σ ((u, v)) =                      if there is ( ) u and u = v p if there is u, w ( ) v or u, w ( ¯ ) v q if there is w, u ( ) v or w, u ( ¯ ) v e i if there is u 1 , . . . , u i , . . . , u n (?) v and u i = u e σr(i) if there is r = u 1 , . . . , u i , . . . , u n (! ) v and u i = u w σ ((v, u)) * otherwise. ( 27
)
The permuted weighting, denoted again as w σ (π), is the lifting of the permuted base weighting to generic straight paths, and the path weighting, written w (π), is the sum of all the permuted weights of a path, for any resource permutation:

w σ ((v)) = 1 (28) w σ ((u, v) :: π) = w σ ((u, v)) w σ (π) (29)
w (0) = 0 (30) w (π) = σ∈S N w σ (π) (31)
The sum forms a free commutative monoid on the rL * structure, and its identity is 0. Formally, we have that for any a, b, c ∈ (rL * , +):

(a + b) + c = a + (b + c) (32) a + b = b + a (33) a + 0 = a (34)
A path π is regular if w (π) = 0. The execution of a net N , is defined as:

Ex(N ) = π∈P EC (N ) w (π) . ( 35
)
Example 5. Consider again the closed simple net M, whose reduction has been discussed in Example 2, and that is depicted in the leftmost extremity of Figure 5. To have an idea of the execution of M and of the behaviour of the algebraic structure, let us consider an execution comprehensive path, one of the persistent two, and compute its weight. Given that the path is palindromic, i.e. has the form π :: π † , we will consider only its first half, that goes from the root of the term to the constant. Moreover, we will break lines when a path inverts its polarity direction, i.e. if it walks from in to out or vice versa.

(v 1 , v 2 , v 3 , w 1 , w 2 , w 3 , σ∈S2 q e 1 e * σ(2) q * e 1 • w 1 , v 3 , v 2 , p e σ(2) e * 1 • v 4 , v 5 , v 6 , v 3 , z 1 , z 2 , z 3 , p * e * 1 q e 2 e * σ(1) q * e 1 • z 1 , v 3 , v 6 , p e σ(1) e * 2 • v 7 , v 8 ) p * e * 1
On the path: reduce it using the exponential rule. On the weight: apply Equation 26and then 22 on the addend s.t. σ = (2, 1), apply Equation 25and then 21 on the one s.t. σ = (1, 2).

→ (v 1 , v 2 ≡ w 1 , w 2 , w 3 , = rL * q q * e 1 • w 1 ≡ v 2 , p • v 4 , v 5 , v 6 ≡ z 1 , z 2 , z 3 , p * e * 1 q q * e 1 • z 1 ≡ v 6 , p • v 7 , v 8 ) + p * e * 1 + 0 0
Forget zeros on both side. On the path: reduce it using the leftmost linear implication rule. On the weight: apply Equation 25 and then 21.

→ (v 1 ≡ w 2 , w 3 ≡ v 4 , v 5 , v 6 ≡ z 1 , z 2 , z 3 , = rL * e 1 e * 1 q q * e 1 • z 1 ≡ v 6 , p • v 7 , v 8 ) p * e * 1
On the path: reduce it using the linear implication rule. On the weight: apply Equation 25and then 21.

→ (v 1 ≡ w 2 , w 3 ≡ v 4 , v 5 ≡ z 2 , z 3 ≡ v 7 , v 8 ) = rL * e 1 e * 1 e 1 e * 1
On the path: reduce it twice using exponential rules. On the weight: apply Equation 25and then 21, and repeat.

→ (v 1 ≡ w 2 ≡ v 5 ≡ z 2 , z 3 ≡ v 7 , v 8 ) = rL * e 1 e * 1 → (v 1 ≡ w 2 ≡ v 5 ≡ z 2 ≡ v 8 ) = rL *
Therefore the persistent path turns out to be regular. Even more, along the reduction we managed to apply, for each step, some rL * equations so that the weight of every reduct is equal to the manipulated weight. The next two theorems shall generalise these two facts.

Invariance and regularity

We now show that the rL * monoid introduced above accurately computes path reduction. We prove the equivalence between regularity and persistence, and show that execution is invariant by reduction. Not only the construction is a suitable semantic for ground typed RINs, but also possesses quantitative awareness, since, for any term, the number of execution paths that are regular is equal to the number of addends in its normal form.

Lemma 5. For any closed net N : , any reduction step ρ, and any path π ∈ P EC (N ):

w (π) = rL * w (ρ(π)) . ( 36
)
Proof. Let π ∈ P E (N ) with N addend of N containing the redex R. Recall that π has to be long enough for ρ, for it is maximal. Suppose the RCF of π w.r.t. R is π 0 :: χ 1 :: π 1 :: . . . :: χ k :: π k . We proceed by a case analysis of the kind of reduction rule.

T (R) =

/ ¯ . Let R be as in the leftmost redex of Figure 3. We distinguish two sub-cases, depending on the nullity of ρ(π).

(a) Suppose ρ(π) = 0. By definition of weighting (Equation 30) we have w (ρ(π)) = 0.

Moreover, by Definition 12 and in particular Equation 7, there must exists 0 ≤ l ≤ k, such that ρ(χ l ) = 0. Hence, it must be the case that χ l is either as in Equation 5, or as in Equation 6.

i Suppose χ l = (v, w, u ). Then ρ(χ l ) = 0, and w (χ l ) = pq * = rL * 0.

ii Suppose χ l = (v , w, u). Then ρ(χ l ) = 0, and w (χ l ) = qp * = rL * 0.

Again by definition of weighting (Equation 29, 31), and applying Equation 22, we conclude w (π) = rL * 0 = w (ρ(π)).

(b) Suppose ρ(π) = 0. Then, again by definition of multiplicative residual, and in particular by Equation 7, we know ρ(χ l ) = 0 for any 0 ≤ l ≤ k. Hence, it must be the case that χ l is either as in Equation 3, or as in 4.

i Suppose χ l = (v, w, u). Then ρ(χ l ) = (v ≡ u ), and w (χ l ) = pp * = rL * 1.

ii Suppose χ l = (v , w, u ). Then ρ(χ l ) = (v ≡ u ), and w (χ l ) = qq * = rL * 1.

Now, applying this fact on the definition given by Equation 7, and using Equation 21 we conclude.

w (π) = σ∈S N w σ (π 0 ) w σ (χ 1 ) w σ (π 1 ) . . . w σ (χ k ) w σ (π k ) = σ∈S N w σ (π 0 ) w σ (π 1 ) . . . w σ (π k ) = w (ρ(π))
2 T (R) = !/?. Let R be as in the rightmost redex of Figure 3, and let r be the !-link involved in it. We distinguish again two sub-cases, depending on the nullity of ρ(π).

(a) Suppose ρ(π) = 0. Then by Definition 13, in particular Equation 9, there are only two possible causes.

i Arity mismatch, i.e. when n = m, where n, m are the arities of the two links.

Because of the hypothesis of comprehensiveness of π, it must be the case that k ≥ max(n, m). Then, whatever permutation σ n ∈ S n we choose for the premisses of the !-link in R, there always exists a crossing χ l , for some 0 ≤ l ≤ k, such that χ l = (u σn(i) , w, v j ) and σ n (i) = j.

ii Permutation incoherence, i.e. when n = m, but for any σ n ∈ S n there exists a crossing χ l ⊆ π such that σ n (i) = j. This morally happens when π tries to use more than once a resource, travelling from the same premiss of the ?-link to two different premisses of the corresponding !-link.

Thus, in both cases there is a "wrong" crossing χ l ⊂ π such that, for any resource permutation σ ∈ S N (recall Definition 7), we have w σ (χ l ) = e σ(r)(i) e * j where σ(r)(i) = j. Hence, by Equation 26, w σ (χ l ) = 0. By definition of weighting (Equation 29, 31) and applying Equation 22, we have w (π) = rL * 0. But by the same definition we also have w (ρ(π)) = 0, so we conclude.

(b) Suppose ρ(π) = 0. Again by definition of path reduction, it must be the case that n = m, and that there exists σ n ∈ S n such that for all 0 ≤ l ≤ k we have ρ σ n (χ l ) = 0. In particular, let χ l be as in Equation 8, and observe it must be also the case that σ n (i) = j, which allows ρ σ n (v i , w, u j ) = (v σn(i) ≡ u j ). Moreover, by the comprehensiveness hypothesis for π, σ n has to be unique, so that for any other σ n , we have ρ σ n (π) = 0. So, according to this, we split resource permutations S N into S N ∪ S N , where the former is the set of any σ such that σ (r) = σ n , while, symmetrically, the latter contains any σ for which σ (r) = σ n . Hence, by Definition 16 we obtain:

w (π) = σ ∈S N w σ (π) + σ ∈S N w σ (π) = σ ∈S N w σ (π 0 ) w σ (χ 1 ) w σ (π 1 ) . . . w σ (χ k ) w σ (π k ) + σ ∈S N w σ (π 0 ) w σ (χ 1 ) w σ (π 1 ) . . . w σ (χ k ) w σ (π k ).
In the leftmost series, by Equation 25, w σ (χ l ) = e σ (r)(i) e * j = 1. While in the rightmost, by Equation 26, w σ (χ l ) = e σ (r)(i) e * j = 0, so it neutralises to 0. Therefore we concluded:

= rL * σ ∈S N w σ (π 0 ) w σ (π 1 ) . . . w σ (π k ) = w (ρ(π)) .
Theorem 2. For any closed net N : , any reduction sequence ρ, and any path π ∈ P EC (N ):

w (π) = rL * w (ρ(π)) . ( 37
)
Proof. A straightforward induction on the length n of ρ.

1 Base. Suppose n = 0. Trivially, ρ(π) = π, so w (ρ(π)) = w (π). 2

Step. Suppose n > 0. Let ρ = ρ ρ , with ρ a single step, ρ a sequence of reductions. By Definition 14 of path reduction, ρ (ρ (π)) = ρ(π). By previous Lemma 5, w (ρ (π)) = rL * w (ρ (ρ (π))). But, by inductive hypothesis we have that w (π) = rL * w (ρ (π)) so we conclude.

Corollary 1. For any closed net N : , a path π ∈ P EC (N ) is persistent if and only if π is regular.

Proof. Immediate from Theorem 2.

Theorem 3. For any closed net N : and any reduction sequence ρ,

Ex(N ) = rL * Ex(ρ(N )). ( 38
)
Proof. Consider first the execution of N (Definition 16 and Equation 35), and notice that we can separate the weights of paths that are persistent to ρ from those of paths that are not.

Ex(N ) = π∈P EC (N ) w (π) = π ∈P EC (N ) persistent to ρ w (π ) + π ∈P EC (N ) not persistent to ρ w (π ) (39)
But, by hypothesis of non-persistence w.r.t. ρ we have ρ(π) = 0, which implies by Theorem 2 that w (π ) = 0. Hence, the rightmost series is 0, and we obtain that:

= π ∈P EC (N ) persistent to ρ w (π ) . ( 40
)
Consider now the execution of ρ(N ), which by definition is:

Ex(ρ(N )) = π ∈P EC ( ρ(N )) w (π ) . ( 41
)
Observe that, by a straightforward induction on the length of ρ, we can generalise Theorem 1 to obtain the bijection induced by ρ between the paths in P EC (N ) persist to ρ and those in P EC (ρ(N )). So let π ∈ P EC (N ) persistent to ρ, and π ∈ P EC (ρ(N )), such that ρ(π ) = π . But by Theorem 2 we have w (π ) = w (ρ(π ))), hence we conclude.

= π ∈P EC (N ) persistent to ρ w (π ) = Ex(N ) (42)
Corollary 2. For any term t : , regular paths in t are as many as (non-zero) addends in NF(t).

Proof. By definition of the calculus and of its nets syntax, NF(t) = n , for some natural number n. Clearly, P EC ( ) contains a unique path, made by the unique vertex of . Then |P EC ( NF(t) )| = n. But from last Theorem 3, Ex( t ) = Ex( NF(t) ), therefore the claim.

mMELL nets, Taylor-Ehrhard expansion and paths

mMELL proof-nets, paths and reduction

We now introduce proof-nets for the mimimal propositional fragment of multiplicative exponential linear logic (mMELL for short) as a translation of λ-calculus. We follow Girard's translation of intuitionistic logic (1987) which represents a formula/type A → B as !A B and implements a call-by-name calculus [START_REF] Maraist | Call-by-name, Call-by-value, Call-by-need, and the Linear Lambda Calculus[END_REF]. There we can recall how paths are deformed under cut-elimination. With respect to the heterogeneous panorama of proof-net definitions, we opted, among the most common traits, for those that resulted of the highest convenience for our interest, similarly to how RINs have been formalised. We adopt a hypergraph formulation of the so-called nouvelle syntaxe tradition, where in particular: (i) hyperlinks represent logical connectors or syntactic constructs, while vertices represent formulae or types; (ii) there is only one in exponential link instead of three (dereliction, contraction and weakening); (iii) auxiliary doors, cut and axioms are not represented by explicit links, but as vertices with some distinctive properties. For the sake of clarity, in the present and next section we shall explicit "mMELL" and "resource" to distinguish nets, reduction, paths and other notions that are identically named in the two systems.

Definition 17 (mMELL links, boxes and structures). The set of mMELL links is similar to that of resource links introduced in Definition 3 and Figure 1. The only difference is that the !-link has fixed unary arity, instead of arbitrary, is called promotion, instead of co-contraction (see Figure 7). A mMELL pre-net is a pre-net made of mMELL links. Given a pre-net P = (V, L, T ), a sub-pre-net P of P is a pre-net (V , L , T ) such that V ⊆ V (P), L ⊆ L(P ), and T is the restriction of T to V . A boxing b is a function that maps a promotion link l to a sub-pre-net B ⊆ P and satisfies the followings.

1 The vertex v = P (l) belongs to V (B). 2 Any v ∈ I(B) different from v is either the premiss of a ?-link or a conclusion of P. 3 There is no v ∈ V (B) such that P (l ) v ∈ C(l ) while l ∈ L(B) and l / ∈ L(B). 4 For any !-link l such that B = b(l ), if L(B) ∩ L(B ) = ∅ then B ⊆ B or B ⊇ B .
A mMELL structure N is a pair (P, b) where P is a mMELL pre-net and b is a boxing for !-links of P. A sub-structure N of N , written N ⊆ N , is a structure (P , b ) such that: P ⊆ P, and b is the restriction of b to L(P ) such that for any !-link l ∈ L(P ), b(l) ⊆ P . If b(l) = P for some !-link l in L(N ), then: B = N is a box of N ; the sub-structure made by B and l is a bordered box and written B; the vertex v ∈ I(B) is called the principal door of B if v ∈ C(l), otherwise an auxiliary door. The set of boxes of N is written Bxs (N ). The box B is depicted drawing a dashed square enclosing all the vertices in B and connecting its doors. In textual notation, B will be denoted as its collapse to a link, e.g. as x 1 , . . . , x n [B] w , where w is the principal door and x i is an auxiliary one. The box depth level, or simply the depth, of a vertex v, written d(v), is the number of boxes it belongs to. By extension, the depth of a link l is d(C(l)), while the depth of a box V [B] w is d(w). Two structures are equal when there exists a box-and type-preserving isomorphism between them.

Definition 18 (Term translation). A λ-term t, is an element of the language Λ induced by the grammar T ::= | V | λV.T | (T T). Given t ∈ Λ and Γ injection between the variable occurrences in t and a set of vertices V , the translation t Γ is a mMELL structure having one out conclusion and a possibly empty set of in conclusions. The translation is defined almost identically to that of simple resource terms we introduced in Definition 6 and Figure 2. The only different case is the pre-translation of application, that is depicted in Figure 7, where the pre-translation of the argument is put into a box and connected by a promotion (instead of a co-contraction).

Definition 19 (mMELL reduction and proof-nets). The mMELL reduction is the In this case, the redex sub-structure R includes not only the two exponential links u 1 , . . . , u k (?) c and p = v (! ) c , but also the box W [B] v that is connected to the cut !-link, together with the set of every link X i (?) y i such that there exists w ∈ W that also belongs to X i . (The boxes C, D are drawn in Figure 8 for the sake of clarity, but are not part of the redex.) The reduction removes the cut exponential links, and duplicates B into k copies (erasing it when k = 0):

W 1 [B 1 ] u 1 , . . . , W k [B k ] u k .
Also, the boxing b of the reduct is obtained by the boxing b of R so that the box copy B h is included in any box that in R contains v h . More precisely:

1 if p is the !-link of a box B containing u h for some 0 ≤ h ≤ k, then b (p ) = b(p ) ∪ B h ; 2 if p = p is the !-link of a box B B then b (p h ) = b(p ), for any 0 ≤ h ≤ k; 3 otherwise b (p ) = b(p ).
Notice that for any 0 ≤ j ≤ s, the set of premisses of the j-th ?-link containing auxiliary doors for B is modified by the reduction: the sequence of premisses X j of its reduct is obtained by replacing any occurrence of a vertex w ∈ W with the sequence (w 1 , . . . , w k ) such that its elements respectively belongs to W 1 , . . . , W k .

A mMELL structure N is a mMELL proof-net if there exists t ∈ Λ such that t → * N .

Static notions and notations for paths defined in Section 3 in RINs are seamlessly extended to mMELL proof-nets: recall from Definition 10 straight, maximal and execution paths, and reversal and concatenation; adapt from Definition 11 the notions of crossing to the mMELL exponential reduction rule.

Definition 20 (mMELL path reduction). The mMELL path reduction is a function mapping a straight path π that is in a proof-net N and long enough for a reduction ρ to a set ρ(π) of paths in ρ(N ). The reduct of a redex crossing χ is defined depending on its kind. The linear implication case is obtained by the corresponding case in Definition 12, by taking the set of the (unique) image there defined. For the exponential case, let R be as in Figure 8, and let β be a maximal sub-path of χ whose vertices are in the box B. Also, let β j be the copy of β in B j , that is the j-th copy of B. We isolate three kinds of crossings, depending on the polarities (in or out) of the two extrema of β.

1 out-out. Let 1 ≤ j, j ≤ k, where j = j . Then ρ (u j , c, v) :: β :: (v, c, u j ) = {(u j ) ::

β j :: (u j ) [u j ≡ v j ]} ; (43) ρ (u j , c, v) :: β :: (v, c, u j ) = ∅. (44)
2 out-in. Let 1 ≤ j ≤ k and 1 ≤ l ≤ s. Then ρ (u j , c, v) :: β :: (w l , y l ) = (u j ) ::

β j :: (w lj , y l ) [u j ≡ v j ] . (45)
3 in-in. Let 1 ≤ l, m ≤ s. Then ρ (y l , w l ) :: β :: (w m , y m ) = (y l , w lj ) ::

β j :: (w mj , y m ) 1 ≤ j ≤ k . ( 46
)
If R is the redex of ρ, and RCF R (π) = π 0 :: χ 1 :: π 1 :: . . . :: χ k :: π k , then ρ(π) = π 0 :: χ 1 :: π 1 :: . . . :: χ k ::

π k χ 1 ∈ ρ(χ 1 ), . . . , χ k ∈ ρ(χ k ) . ( 47
)
Lemma 6. The reduction of a path induces a partition on paths of the reduct. Given N mMELL proof-net and ρ reduction step, for any π ∈ P E (ρ(N )) there exists a unique φ ∈ P E (N ) such that π ∈ ρ(φ).

Proof. Let N = C[R],
for some redex R and some context C[ ]. Suppose also that π = π 0 :: χ 1 :: π 1 :: . . . χ n :: π n , where, for any 1 ≤ i ≤ k, the subpath χ i is a maximal sequence of vertices belonging to ρ(R). Observe that the extrema of χ i necessarily belong to the interface of ρ(R), because π is an execution path. Now, by definition of reduction, and in particular as per Equation 47, if n = 0 (i.e. π does not cross ρ(R)), then there is nothing to prove, since by definition of reduction we have that π ∈ P E (N ) and ρ(π) = {π}. So, suppose otherwise that n > 0 and let us discuss χ i distinguishing two cases depending on the kind of the redex.

1 T (R) = / ¯ . The claim is proven by case item 1 of the proof of Theorem 1. 2 T (R) = !/?. Let ρ be as in Figure 8 and recall that ρ(R) is made by the subnets B j , for any 1 ≤ j ≤ k, that are copies of the box W [B] c in R. We distinguish three sub-cases depending on the polarity of the extrema of π. (a) out-out. Let χ i = (u j ) :: β j :: (u j ) for some 1 ≤ j ≤ k. Then take χ i = (u j , c, v) :: β :: (v, c, u j ), and observe that by definition of reduction (cf. Equation 43) χ i is the only crossing of R such that ρ(χ i ) = {χ i }.

(b) out-in. Let χ i = (u j ) :: β j :: (w lj , y l ). Then take χ = (u j , c, v) :: β :: (w l , y l ), and verify again (cf. Equation 45) that χ i is the only crossing of R such that ρ(χ i ) = {χ i }.

(c) Let χ i = (y l , w lj ) :: β j :: (w mj , y m ) for some 1 ≤ l, m ≤ s (recall that s is the number of ?-links having a premiss in W j for some 1 ≤ j ≤ k). Then take χ = (y l , w l ) :: β :: (w m , y m ) and inspect Equation 46to verify that χ i is the only crossing of R such that χ i ∈ ρ(χ i ).

Net expansion

We now recall Taylor-Ehrhard-Regnier expansion of mMELL proof-nets into RINs, using almost standard definitions. Although the challenging study of multiplicity coefficients is postponed to future investigations, we preserve coherence and employ sums to put together simple nets, even though the sum is idempotent so they essentially represent the support of the infinite series used in the original definition.

Definition 21 (Proof-net expansion). Given a mMELL pre-net N , and B ∈ Bxs (N ), the i-ary box expansion of B, written B i , is depicted in Figure 9. Contractions' premisses are duplicated together with B enforcing stability with respect to their ordering: given a contraction X j (?) y j such that there exists x h ∈ X j secondary door of B, in the expansion such a contraction becomes X j (?) y j , where the sequence X j is obtained from X j by replacing any such x h with the sequence x h.1 , . . . , x h.i . A simple mixed net is pre-net built with resource or mMELL links, i.e. possibly containing co-contractions and promotions with boxes, and a mixed net is a possibly infinite sum of simple mixed nets. The sum + is not only associative, commutative, and having an identity element, i.e. the empty sum 0, but it is also idempotent: M + M = M. The outermost expansion, is a function from simple to generic mixed nets, written as M • when applied to M, and defined by induction on d(M). If d(M) = 0, then simply M • = M. Otherwise, if B 1 , . . . , B n are the outermost bordered boxes of M, and N n is the set of functions from {1, . . . , n} to N, then:

N • = a∈N n N a , ( 48
) N a = N B a(1) 1 B 1 , . . . , B a(n) n B n . ( 49
)
We define the complete expansion of a simple mixed net M as the fixed point of the outermost expansion, whose domain is extended to generic mixed nets.

0 • = 0 (50) (M + M) • = M • + M • (51) M • = (M • ) • (52)
The support of a mixed net M is the set supp (M) of all addends in M. And any element in supp (M • ) is called an expansion of N .

Fact 2. The complete expansion of a mMELL proof-net is a possibly infinite sum of simple resource interaction nets.

Path expansion

We now proceed to define the expansion of a path π in a proof-net N from the natural observation of the action of expansion on paths -it is the sum of all paths belonging to any simple resource nets in the complete expansion of N .

Definition 22 (Box crossing). Given a proof-net N and π ∈ P(N ), its outermost-box crossing form is: OBCF (π) = 0 :: β 1 :: 1 :: . . . :: β n :: n , where, for every 1 ≤ i ≤ n, β i is a box crossing, that is a maximal subpath belonging to an outermost box B, i.e. d(B) = 0. Notice that n may be null and that a crossing is not necessarily a maximal path in B.

Definition 23 (Path expansion). Given N a mixed net and π ∈ P(N ), let B 1 , . . . , B m be the outermost bordered boxes of N and a ∈ N m . Then the a-ary outermost expansion of π in N is the sets of paths obtained by the action of the outermost expansion of N according to a.

π

N a =    {π} if m = 0, 0 :: β 1 k 1 :: 1 :: . . . :: β n kn :: n 1 ≤ k i ≤ a(i) otherwise. ( 53
)
Notice that the rightmost side of Equation 53 is empty whenever there exists 1 ≤ i ≤ m such that a(i) = 0; while it is the singleton { 0 } if n = 0. The outermost expansion of a set of paths Π is the sum of sets of paths generated by the sum of all a-ary outermost expansions, extending its domain to sets of path. The sum of paths satisfies the same properties of the sum of simple resource nets.

Π N a = π∈Π π N a (54) Π N • =      Π if m = 0, a∈N m Π N a otherwise. ( 55
)
the equivalence between persistence of π and the existence of a persistent path π within π N • . Before that, we need to detail what is such an infinitary parallel reduction, which represents the expansion of mMELL proof-nets' dynamics. Fact 3 implies that a mMELL vertex c is a cut if and only if every set in every addend of its expansion contains only resource cuts; moreover, their redexes never overlap. We therefore define first a tailored § notion of parallel reduction and then precisely restrict it to reduce all and only resource cuts which belong to the complete expansion of the same mMELL cut.

C N = c∈Nn Nm C[P c(1) /h 1 , . . . , P c(n) /h n ] s.t. I(P c(i) ) = I(h i ) (60)
In particular, note that if m = 0 and consequently N = 0, then C N = 0. Given C a non-simple resource context, and N a resource pre-net, C N is the substitution of the latter in each addend of the former; i.e.: 0 N = 0 and (C + C) N = C N + C N .

Definition 25 (Parallel and expanded reduction). The closure of the simple reduction relation with respect to multi-hole resource contexts is called parallel resource reduction and written . Formally, given a resource net N = C P 1 + . . . + P n where C is a multi-hole context and P 1 , . . . , P n are pre-nets, if P 1 → P 1 , . . . , P n → P n then N C P 1 + . . . + P n . Given a mMELL proof-net N and a reduction step ρ on a cut c ∈ V (N ), the expanded reduction of ρ, written ρ • , is the parallel reduction of the set of any resource redex in supp (N • ) for any cut in supp (c • ).

Notation. We extend the domain of resource reduction for paths to sets of paths. For any reduction ρ, and any set of paths Π, we write ρ(Π) to denote π∈Π ρ(π).

Commutativity of reduction and expansion

Lemma 8. Let R be a mMELL redex, ρ be its reduction step, and χ ∈ P(R). Then:

supp (ρ(χ)) (ρ(R)) • = supp ρ • χ R • . ( 61
)
Proof. We distinguish two cases according to the type of redex. § The classic and general notion has been formalised in a similar setting [START_REF] Mazza | The Separation Theorem for Differential Interaction Nets[END_REF].

1 T (R) = / ¯ . Let R = v , v ( ) w , u , u ( ¯ ) w as in Figure 3. We immediately notice that, by Definition 21, R • = R while, as per Definition 23, we have χ R • = {χ}.

We consider two sub-cases depending on the persistence of χ to ρ.

(a) ρ(χ) = ∅. This implies that, by Definition 12 and in particular Equation 3, 4, that χ is either (v , w, u ), (v, w, u), or the reversal of these. Given that from the analysis of one case the other three can be straightforwardly obtained, let us assume χ = (v , w, u ). By definition of reduction, we have ρ

(χ) = {(v )[v ≡ u ]}.
Moreover, by definition of path expansion, we have that

(ρ(χ)) (ρ(R)) • = {(v )[v ≡ u ]} (ρ(R)) • = {(v )[v ≡ u ]} .
Let us now look at χ R • = {χ}, and consider its expanded reduction:

ρ • χ R • = ρ • (χ).
Notice that ρ • contains only one reduction step, which is identical to ρ, because R • = R. Hence we conclude:

ρ • χ N • = ρ(χ) = {(v )[v ≡ u ]} . (b) ρ(χ) = ∅.
Then we immediately notice that by definition of path expansion:

(ρ(χ)) (ρ(R)) • = ∅ (ρ(R)) • = ∅.
Moreover, given that, as we remarked in previous case, we have χ R • = {χ}, and ρ • = {ρ}, we immediately conclude:

ρ • (χ R • ) = ρ • (χ) = ρ(χ) = ∅.
2 T (R) = !/?. Let R be as in Figure 8:

R = u 1 , . . . , u k (?) c , v (! ) c , W [B] v , X 1 (?) y 1 , . . . , X s (?) y s . ( 62
)
We distinguish three sub-cases depending on the polarities of the extrema vertices of the crossing of B.

(a) out-out. Let χ = (u j , c, v) :: β :: (v, c, u j ). Being the most interesting one, we shall discuss in full details this sub-case, further distinguishing two sub-sub-cases according to the persistence of χ.

i χ persistent to ρ. Then, by definition of mMELL path reduction (in particular Equation 43), j = j and:

ρ (χ) = {(u j ) :: β j :: (u j ) [u j ≡ v j ]} ,
where we kept trivial paths as extrema for the sake of clarity. By Definition 23:

(ρ(χ)) (ρ(R)) • = (u j ) :: β B • j j :: (u j )
Now let us look at the rightmost side of Equation 61, and apply the definition of path expansion. If B is the h-th of the m outermost boxes of R,

(χ) R • = a∈N m (u j , c, v n ) :: β B • n n :: (v n , c, u j ) 1 ≤ n ≤ a(h) ,
so we can consider its expanded reduction w.r.t. ρ,

ρ • χ R • = a∈N m ρ • (u j , c, v n ) :: β B • n n :: (v n , c, u j ) 1 ≤ n ≤ a(h) .
Notice that in any element of any addend of the sum, the two outermost paths are crossings of a resource redex of exponential type. The reduction step ρ • performs by definition the reduction of any cut c ∈ C ∈ supp (c • ), including c. Therefore, we can apply Definition 13 of path reduction and in particular Equation 10.

ρ • χ R • = a∈N m σ∈S a(h) ρ σ (u j , c, v n ) :: β B • n n :: (v n , c, u j ) 1 ≤ n ≤ a(h) = a∈N m σ∈S a(h) ρ σ ((u j , c, v n )) :: β B • n n :: ρ σ ((v n , c, u j )) 1 ≤ n ≤ a(h) .
By definition (cf. Equation 8), ρ σ maps to 0 whenever the arities mismatch, or when the permutation is not respected by all crossing; otherwise it reduces to a trivial path. Hence, recalling that k is the arity of the cut ?-link in R,

ρ • χ R • = a∈N m σ∈S a(h) (u j ) :: β B • n n :: (u j ) u j ≡ v σ(j) 1 ≤ n ≤ a(h), k = a(h), σ(j) = n .
Because of the condition on a(h), we can immediately simplify as:

ρ • χ R • = σ∈S k (u j ) :: β B • n n :: (u j ) u j ≡ v σ(j) 1 ≤ n ≤ k, σ(j) = n .
Observe that for any σ ∈ S k there exists a unique 1 ≤ n ≤ k such that σ(j) = n. Therefore, every addend is a singleton of a path:

ρ • χ R • = σ∈S k (u j ) :: β B • σ(j) σ(j) :: (u j ) u j ≡ v σ(j) .
Now observe that, for any {χ }, {χ } ∈ supp ρ • χ R • , we have χ = χ , since they are copies of the same path, within copies of the same sub-substructure.

In particular, we have |S k | = k! equal addends, which can be simplified in a single one, since the sum is idempotent, and conclude:

supp ρ • χ R • = (u j ) :: β B • j j :: (u j ) [u j ≡ v j ] = supp (ρ(χ)) (ρ(R)) • .
ii χ not persistent to ρ. Then, as per Equation 44, j = j and ρ(χ) = ∅. Then, immediately by Equation 55: (ρ(χ))

(ρ(R)) • = 0. The analysis of ρ • χ R • goes θ) with any expansion of ρ(χ i ). (ρ(π)) (ρ(N )) • = Γ∈supp γ C • X i ∈supp ρ(χi) (ρ(R)) •
γ 0 :: χ 1 :: γ 1 :: . . . :: χ k :: γ k γ 0 :: θ 1 :: γ 1 :: . . . :: θ k ::

γ k ∈ Γ, χ i ∈ X i (66)
Now let us consider the action of expanded reduction on Equation 65. For any set of resource redexes R in the support of the expansion of R, let ρ R ⊆ ρ • denote the set of ordinary resource reduction steps acting on every redex in R . We distinguish two cases according to the type of redex.

1 T (R) = / ¯ . We can directly apply Definition 12.

ρ • π N • = Γ∈supp γ C • R ∈supp(R • ) X i ∈supp ρ R χ R • i
γ 0 :: χ 1 :: γ 1 :: . . . :: χ k :: γ k γ 0 :: θ 1 :: γ 1 :: . . . ::

θ k :: γ k ∈ Γ, χ i ∈ X i (67)
Therefore, from Equation 66 and 67, we deduce that it is enough to prove that

supp ρ(χ i ) (ρ(R)) • ? = supp   R ∈supp(R • ) ρ R χ R • i   ,
which is equivalent to the very statement of Lemma 8:

supp ρ(χ i ) (ρ(R)) • = supp ρ • χ R • i .
2 T (R) = !/?. Similarly to the previous case, we now apply Definition 13 of path reduction. This time the sum we obtain spans also over the resource permutation:

ρ • π N • = Γ∈supp γ C • R ∈supp(R • ) σ∈S R X i ∈supp ρ R σ χ R • i
γ 0 :: χ 1 :: γ 1 :: . . . :: χ k :: γ k γ 0 :: θ 1 :: γ 1 :: . . . ::

θ k :: γ k ∈ Γ, χ i ∈ X i (68)
Comparing Equation 66and 68, we reduce the statement to:

supp ρ(χ i ) (ρ(R)) • ? = supp     R ∈supp(R • ) σ∈S R ρ R σ χ R • i     ,
which is ensured again by Lemma 8:

supp ρ(χ i ) (ρ(R)) • = supp ρ • χ R • i .
Theorem 4. Let N be a mMELL proof-net, let ρ be a reduction sequence on N , and π ∈ P E (N ). Then:

supp (ρ(π)) ( ρ(N )) • = supp ρ• (π N • ) . (69)
Proof. Using Lemma 9, the proof reduces to a simple induction on the number of reduction steps in ρ.

Theorem 5. For any proof-net N , and π ∈ P E (N ), π is persistent if and only if there exists π ∈ Π ∈ supp π N • which is persistent.

Proof. We separately prove necessity and sufficiency. 1 (⇐). By contraposition, suppose π non persistent. This means that there exists a mMELL reduction sequence σ such that σ(π) = ∅. Hence, (σ(π)) (σ(N )) • = ∅. Therefore, by commutativity of Theorem 4, also σ• (π N • ) = ∅. This allows us to conclude -for any Π ∈ supp π N • and for every π ∈ Π, there exists some resource reduction sequence σ ⊆ σ• such that σ (π ) = ∅. 2 (⇒). Let σ be a reduction sequence N → * NF(N ). By hypothesis σ(π) = ∅, therefore (σ(π))

NF(N ) • = ∅. By commutativity of expansion with reduction (Theorem 4), supp (σ(π))

NF(N ) • = supp σ• π N • , which implies that σ• π N • = ∅. Hence,
there exist Π ∈ supp π N • and π ∈ Π such that σ• (π ) = ∅. Now, since σ(N ) is cut-free, by Fact 3 it must be the case that also σ• (N • ) is cut-free, i.e. it is in normal form with respect to resource reduction. Therefore, we conclude by Lemma 4 that π is persistent.

Expansion and execution

Theorem 5 showed that persistence of a mMELL execution path π can be characterised by the existence of persistent resource paths in its expansion. But this, in turn, can be characterised by regularity, as established in Corollary 1. So we can formulate an expanded variant of the notion of regularity, which characterise persistence of π using weights of its expansion. Moreover, we can formulate a qualitative and expanded variant of the execution formula for a -typed mMELL proof-net N . We weigh, within the rL * monoid, any path in any set of the sum obtained by expanding any path in N . Such expansion-execution is invariant with respect to mMELL reduction.

Definition 26 (Expansion-regularity and execution). The expanded weight of a mMELL path π in a mMELL proof-net N is the sum of the rL * weights any of its comprehensive expansions:

w • (π) = π ∈Π∈supp π N • π compr.
w (π ) .

(70)

We call π expansion-regular if w • (π) = 0. The expansion-execution of N , written Ex • (N ), is the sum of the expanded weights of any execution path in N :

Ex • (N ) = π∈P E (N ) w • (π). ( 71
)
Corollary 3. A path π is persistent if and only if π is expansion-regular.

Proof. We separately prove necessity and sufficiency. Let N be the proof-net of π.

1 (⇐). By contraposition, suppose π not persistent. Then, by Theorem 5, we have that any π ∈ Π ∈ supp π N • is not persistent. In particular, it is the case when π is comprehensive, but Corollary 1 established that any such π is not regular, which means by definition that w (π ) = 0. Ergo, π is not expansion-regular. 2 (⇒). By contraposition, suppose π not expansion-regular, which by definition means that π compr.∈Π∈supp(π N • ) w (π ) = 0. Now, since in (rL * , +) the only invertible element is the identity (for any a, b ∈ rL * , if a + b = 0 then a = b = 0), it must be the case that w (π ) = 0 for any π . Ergo, by Corollary 1, any comprehensive π ∈ π N • is not persistent. Now, recall that, by Lemma 2, every execution path that is not comprehensive cannot be persistent. Therefore, there exists no π ∈ π N • being persistent. Hence, by Theorem 5, we conclude that π is not persistent as well.

Theorem 6. For any mMELL proof-net N and reduction step ρ, Ex • (N ) = rL * Ex • (ρ(N )).

Proof. By definition, we need to show that π∈P E (N ) w • (π) = φ∈P E (ρ(N )) w • (φ). Since by Lemma 6, the step ρ induces a partition on P E (ρ(N )), we may express the claim as the equality between w (φ ) .

Exploiting again Lemma 6, we can highlight the expansion of ρ(π) within the rightmost summation, and obtain:

π ∈Π ∈supp π N • π compr.
w (π ) and π ∈Π ∈supp (ρ(π)) (ρ(N )) • π compr.

w (π ) .

On the leftmost summation, by invariance theorem of rL * (Theorem 3), for any reduction step ρ , we have that w (π ) = rL * w (ρ (π )). Consequently, iterating this argument on any step of ρ • , we conclude that w (π ) = rL * w (ρ • (π )). Hence, we can equivalently compare:

π ∈Π∈supp π N • π compr.
w (ρ • (π )) and π ∈Π∈supp (ρ(π)) (ρ(N )) • π compr.

w (π ) .

On the rightmost summation, we know from commutativity Lemma 9 that (ρ(π)) (ρ(N )) • and ρ • π N • have the same support. Thus, we obtain:

π ∈Π ∈supp π N • π compr.
w (ρ • (π )) and

π ∈Π ∈supp ρ • (π N • ) π compr.
w (π ) .

Recall that ρ • is equivalent to a reduction sequence σ which includes a step ρ redex of ρ • . Now for any such ρ , we know from Theorem 1 that ρ • induces a bijection between execution paths in a RIN and its reduct, provided they persist to ρ . Moreover, as stated in Fact 1, comprehensiveness is preserved by reduction. Thus, ρ, hence ρ • , induces a bijection between execution comprehensive paths π N • and those of ρ • π N • . Therefore we can write the rightmost summation identically to the leftmost one.

Future work

The results presented here not only open various interesting questions, but also evoke some possible directions towards their answers.

(i) Can we strengthen the expressivity of the calculi considered here, beyond the minimalist formulation to get closer to real programming-language class? An obvious direction is the inclusion of fixed-point combinators, to define a PCF-like variant of the resource calculus (RC), where the restriction to ground types remains innocuous.

(ii) Is there a nicely-expressible and general notion of infinite paths allowing representing infinite normal-forms? The inspiration may come from Böhm trees and its notion of meaningful infinite head normal form, and such a reduction strategy is already known to be closely related both to dynamics of expansion (Ehrhard and Regnier, 2006a) and of paths [START_REF] Laurent | A Token Machine for Full Geometry of Interaction (Extended Abstract)[END_REF].

(iii) Can we design a non-deterministic linear abstract machine inspired by the construction presented here? In order to do so, we need to represent locally the notion expansion, which has a twofold global nature: one in the argument superposition of RC, the other in the superposition of differently expanded terms. Removing the latter, indeed subsumed by the former, the challenge becomes that of formalising a notion of expanded execution which does not explicitly consider the expansion of the proof-net, but which instead first assigns algebraic weights locally, and then computes them in a distributed way. Starting from the approach presented here, the question may be addressed by formalising expansion as a local graph-rewriting system. (iv) Is it possible to define a more general GoI-based model for the full differential λ-calculus, and for the full differential linear logic, where both superposition and nonlinearity are present? In that case, the shape of persistent crossings in an exponential redex does not necessarily respect the definition we gave here by means of fixed permutations, because different copies of a box containing a redex may need different resource assignments. Moreover, in order to obtain a degree of compositionality higher than our GoRI, one should most probably sacrifice the beauty of the invariance under reduction, and make do with a result of equivalence between regularity and persistence. Nonetheless, the presented results on the dynamics of Taylor-Ehrhard-Regnier expansion of paths seems to provides a promising starting point for these investigations.

(v) What are the multiplicity coefficients for path expansion? A study of the non-trivial combinatorial properties would complete our results, providing a tool to study the combinatorics of ordinary paths in λ-terms. We believe it to be connected to the normalisation complexity and the expansion-related part of the framework to be fruitfully extendible at a quantitative level.

Fig. 1 :

 1 Fig. 1: Links: kind, arity and polarity associated to vertices, in both graphical and textual notations

  A simple context C[ ] is a simple pre-net containing exactly one hole-link, i.e. a link with arbitrary arity, polarity and types. A context C[ ] is the sum of a simple context C and a pre-net P. The interface of the hole link is called the internal interface of C[ ]. Given P a simple pre-net and C[ ] a simple context with hole link h, the substitution of the former in the latter, written C[P], is defined whenever the interface of P is the same as the internal interface of C[ ] by replacing P for h. The substitution of non-simple nets is the extension to linear combinations: C[0] = 0, and C[c P + P] = c C[P] + C[P]. Finally, given a non-simple context C[ ] = C[ ] + P, we define C[P] = C[P] + P.

Fig. 3 :

 3 Fig. 3: Cut elimination rules: linear implication and exponential.

Fig. 4 :

 4 Fig. 4: Example: nets and reduction.

Fig. 6 :

 6 Fig. 6: The rL * monoid.

Fig. 7 :Fig. 8 :

 78 Fig. 7: mMELL statics: promotion link, and pre-translation of application.

Fig. 9 :

 9 Fig. 9: i-ary box expansion.

  any π ∈ P E (N ), we shall prove that the followings are equal:w • (π)andφ∈ρ(π) w • (φ).By definition, they are the sum of their comprehensive expansions:

  y] is a simple polyterm. Simple terms are denoted by lowercase Latin letters s, t, u, . . ., polyterms by uppercase S, T, U, . . .. The set N ∆ of terms (resp. the set N ∆ ! of polyterms) is the set of linear combinations of simple terms (resp. polyterms) having coefficients in the semiring of natural numbers N . We also assume all syntactic constructors of simple terms and polyterms to be extended to sums by (bi-) linearity, i.e. to commute with sums. E.g., a non-simple term could be written as (λx.

(2x + y))[z + 4u] to mean: 2(λx.x)[z] + 8(λx.x)[u] + (λx.y)[z] + 4(λx.y)[u].

  6.1. Expanded reductionDefinition 24 (Multi-hole contexts and substitution). A simple multi-hole context C , (resp. a multi-hole context C ) is a simple context (resp. a linear combination of simple contexts over the semiring of N) having a finite, possibly null, number of hole links (see Definition 8). If C has holes h 1 , . . . , h n and N is a sum of simple resource pre-nets P 1 , . . . , P m , then C N consists of the (possibly empty) sum of any possible substitution of the m (non-zero) addends of N into the n holes of C . Formally, if N k denotes {1, . . . , k} (where N 0 = {}), and A B the set of injections from a set A to a set B:

The complete expansion of a sum of sets of paths Π is the fixpoint of the outermost expansion, where we neatly extend its domain to sums of sets of nets.

When it does not lead to confusion, we shall ease the notation of {π} N • writing π N • .

The complete expansion of a vertex v is the sum of sets of vertices that is naturally obtained by the complete expansion of the atomic path (v):

We similarly define the complete expansion of a link l in N as the sum of sets of links defined as follows.

Fact 3. Expansion preserves types and polarities of links. For any mMELL proof-net

Remark 2 (Length and cardinality). Path expansion does not expand a path in the sense of increasing its length. Indeed, for any π ∈ P(N ), and any π ∈ Π ∈ supp π N • , we have |π| = |π |. On the other hand, path expansion introduces a degree of nondeterminism quite higher than net expansion. In fact, for any single N ∈ supp (N • ), the set Π ∈ supp π N • containing expansions of π in N has a cardinality that is a function of the number of box crossing and their respective expanded arities. For example, in the case of just one box expanded in n copies and k crossings, |Π| ∼ n k .

Lemma 7. The inverse relation of path expansion is a function. For any mMELL proofnet N , any simple resource net N ∈ supp (N • ), and any path π ∈ P(N ):

Proof. By immediate verification against definition of path expansion.

Expansion and reduction

We are now able to see how the Taylor-Ehrhard expansion commutes with reduction, proving that, for any reduction sequence, the series obtained by expansion of the set of reducts of a mMELL path π is qualitatively equal to what one gets by reducing in parallel any addend of the expansion of π. Thanks to such result, we will obtain as a corollary as we previously did, until we reach

where we notice that there exists no σ ∈ S a(h) such that σ(j) = n = σ(j ). Therefore, by Equation 8, in every element of any set of the summation that we are now considering, we have that

(b) out-in. We follow the same reasoning used in previous sub-case. Let 1 ≤ j ≤ k and 1 ≤ l ≤ s, and then let χ = (u j , c, v) :: β i :: (w l , y l ). Then:

Hence,

On the other side of Equation 61,

In this case, expanded reduction trivially deals with one cut per crossing of the expansion. Therefore simply applying the definition of reduction, and then simplifying by sum's idempotence the k! equal singletons in the summation, we obtain:

σ(j) :: (w lj , y l ) u j ≡ v σ(j)

= (u j ) ::

whose support is equal to supp (ρ(χ)) (ρ(R)) • , as required.

(c) in-in. Again, along the same line of reasoning, let 1 ≤ l, m ≤ s, and let χ = (y l , w l ) :: β :: (w m , y m ). This time, differently from previous cases 2a and 2b, the set that is the reduct of χ may contain more than one path (cf. Equation 46).

ρ χ = (y l , w lj ) ::

Hence, its expansion is:

On the right side of Equation 61, if B is the h-th of the b outermost boxes of R, we find that

Now, consider its expanded reduction as we previously did:

ρ σ (y l , w ln ) ::

Let us consider the persistence w.r.t. ρ • of a path χ ∈ X , for some addend X of the sum. By definition, given a redex R of some cut

where k is the arity of the ?-link cut in R and is equal to k, the arity of the ?-link cut in R; every crossing of R in χ preserves σ ∈ S a(h) . Now, χ contains no such crossing, so the second condition is always (vacuously) satisfied. Hence, we can simplify by imposing a(h) = k and applying the definition of exponential reduction.

= and we observe that its support is equal to supp (ρ(χ)) (ρ(R)) • .

Lemma 9. Let N be a mMELL proof-net, let ρ be a reduction step on N , and π ∈ P E (N ). Then

Proof. Let R be the redex of ρ, so that N = C[R]. Being an execution path, π is necessarily long enough for R, so let RCF R (π) = γ 0 :: χ 1 :: γ 1 :: . . . :: χ k :: γ k , and let γ = γ 0 :: θ 1 :: γ 1 :: . . . :: θ k :: γ k be the corresponding path in C, where θ i for any 1 ≤ i ≤ k is an atomic path crossing its hole-link. Now let us analyse path expansion. By definition, we can express π N • as the appropriate substitution of any χ i appearing in χ R • i of the corresponding θ i appearing in γ C • :

γ 0 :: χ 1 :: γ 1 :: . . . :: χ k :: γ k γ 0 :: θ 1 :: γ 1 :: . . . :: θ k :: 65, we can write the expansion of ρ(π) as the expansion of γ where we substitute any sub-path θ i (that is an expansion of