Emmanuel Hebrard

Christian Artigues

Pierre Lopez

Arnaud Lusson
email: lusson@laas.fr

Steve Chien

Adrien Maillard

Gregg Rabideau
email: gregg.r.rabideau@jpl.nasa.gov

An Efficient Approach to Data Transfer Scheduling for Long Range Space Exploration

Long range space missions, such as Rosetta, require robust plans of data-acquisition activities and of the resulting data transfers. In this paper we revisit the problem of assigning priorities to data transfers in order to maximize safety margin of onboard memory. We propose a fast sweep algorithm to verify the feasibility of a given priority assignment and we introduce an efficient exact algorithm to assign priorities on a single downlink window. We prove that the problem is NP-hard for several windows, and we propose several randomized heuristics to tackle the general case. Our experimental results show that the proposed approaches are able to improve the plans computed for the real mission by the previously existing method, while the sweep algorithm yields drastic accelerations.

Introduction

Scientific instruments for deep space exploration spacecrafts become more and more sophisticated and consequently produce more and more data that must be sent to Earth. Data management is highly critical as the onboard memory is limited and communication with Earth is often a bottleneck [Vallat et al., 2017;[START_REF] Pérez-Ayúcar | [END_REF]. The Rosetta case is representative of most high profile missions supported by the Deep Space Network where concurrent uploads and downloads make the optimization of data transfers a critical component. ESA and JPL designed an efficient algorithm for solving the memory dumping problem of the Rosetta spacecraft [Chien et al., 2021] in the case where a data production plan is already designed and the decision process concerns transfer priorities. Conversely, for the Philae probe (Rosetta's lander), the transfer priorities were decided a priori, and the experiments were scheduled in consequence [Simonin et al., 2015]. In both cases, data is produced into several memory buffers and the goal is to avoid data loss, which occurs when data is produced into a full buffer. More precisely, we want to maximize the minimum margin, where the margin is the percentage of a buffer's capacity left free, in order to design robust plans where unexpected changes of the dump or fill rates can be absorbed by the margins.

In this paper we consider the same case as Rabideau et al. where the data production plan is known and the problem consists in planning memory dumps [Rabideau et al., 2017]. This problem is recurrent in space missions, see e.g. [Oddi et al., 2002a;Oddi et al., 2002b;Righini and Tresoldi, 2010]. Under this assumption, the fill rate of each memory buffer over the planning horizon is part of the input. Data can only be dumped when the spacecraft is visible from Earth. This is materialized by consecutive disjoint downlink windows. Data dumping is a semi-automatized process. For each downlink window a priority has to be assigned to each buffer, then, the transfers follow this priority ordering.

Note that another way to control the dumping process is to deactivate a buffer at a given time-point. This can only be done once per buffer per downlink window, and no reactivation is possible in that window. The buffer then stops data dumping independently of the buffer priority. However, it must be underlined that assigning precise times to events is incompatible with the robustness objective. Indeed, because fill and dump rates may not be known with precision, a buffer might be deactivated when its usage differs from what motivated that decision. Such uncertainties might lead to waste of the bandwidth. Hence, as Rabideau et al., we consider only decisions on buffer priority because such plans better cope with uncertainties. We thus tackle the problem of computing a priority assignment that maximizes the minimum margin.

In Section 2, we define the problem, establish that it is NPcomplete in general, and we give an efficient algorithm to simulate data transfers given a priority assignment. Then in Section 3 we provide a polynomial algorithm for a single downlink window. From this algorithm, we derive a heuristic for the case with multiple windows in Section 4. Finally, in Section 5 we report the results of a set of experiments on data instances from the Rosetta mission and we compare the proposed heuristic with the one actually used during the mission.

Overlapping Memory Dumping

In the overlapping Memory Dumping Problem (oMDP), we are given m downlink windows, where [s j , e j [ stands for the time interval in which the downlink j is available, and δ j for the dump rate for transfers of downlink j. Moreover, there are n memory buffers, where C i stands for the capacity of buffer i; r i (j) for the maximum handover usage of buffer i at the end of downlink window j; and f i : R → R + for the piecewise constant fill rate function of buffer i over time. Let ν be the number of inflection points over all fill rate functions.

The transfers can be controlled by setting a priority function over the buffers defining a ranking. Data is transferred in standard-sized packets. At every step, one of the buffers of highest priority among those who have at least one packet of data in memory is selected via round-robin to transfer it.

Let U i : R → R be the quantity of data on buffer i over time and g i : R → R be the transfer rate out of buffer i over time.

In between downlink window, all transfer rates are null and the memory usage growth is the fill function, for every buffer i. In particular, for any time t preceding the start of the first downlink s 1 , we have

g i (t) = 0 and U i (t) = t 0 f i (x) dx.
During a downlink window with dump rate δ, however, the effective transfer rate at time t depends on the priority function P, and on the usages and fill rates at time t.

We consider the decision problem of finding a priority ranking for every downlink, such that the peak usage of any buffer (given its fill rate functions, and the data transfer system described above) is less than its capacity, i.e., without data loss. The objective function is actually to maximize the minimum margin, min{M (i) | i ∈ B}, where M (i) is defined as one minus the ratio between the peak usage and the capacity of buffer i. However, it can be achieved by binary search using an algorithm for the decision problem above.

Example 1. Figure 1 shows a plan with two downlinks, both with dump rate 1, and 3 buffers all of capacity 1. Fill rates are figured by colored rectangles, e.g., f 1 (t) = 1 2 for t ∈ [0, 1]. In the first downlink, all buffers have equal priority P 1 (1) = P 1 (2) = P 1 (3) = 1, in the second, buffer priorities are given by their index (P 1 (i) = i, i.e., buffer 3 has the highest priority then 2 then 1). The resulting buffer usage functions U i (t) are displayed in black line. The minimum margin is 1 6 .

Simulation of a Dumping Plan

As shown by Simonin et al., it is possible to compute the data transfers efficiently, that is, with a complexity polynomial in the number of changes in the fill rate functions, as opposed to the number of packets of data [Simonin et al., 2015]. Here we use a similar method, and crucially, we show that one does not need to know the exact priority function to compute the usage of a given memory buffer over time and that a polynomial number of time points have to be considered. This algorithm is denoted Simulation in the remainder of the paper.

Lemma 1. Given the set of buffers of strictly higher priorities and the set of buffers of equal priority, the usage at any time of a given buffer can be computed in polynomial time.

Proof. Consider first the problem of computing the instant transfer rate g i (t) at time t of a buffer i when the usages U(t) are known. Given a set of buffers Ω, let f Ω (t) = i∈Ω f i (t) be the sum of the instant fill rates for buffers in Ω. Let Γ be a set of buffers with priority over buffer i. If at least one buffer in Γ contains some data at time t, no buffer outside Γ may dump any data. Otherwise, buffers in Γ globally dump in downlink window j at rate g Γ (t) = min(δ j , f Γ (t)) where δ j is the dump rate of the downlink j, which leaves a residual dump rate of δ j -g Γ (t). In example 1, at time t = 5.5, buffer 2 thus dumps at the full residual rate δ 2 -f 3 (t) = 1/3 since it is not empty, and buffer 1 cannot dump data.

B3 B2 B1 t = 0 t = 1 t = 3 t = 4 t = 6 1 -1 6 -2 5 1 2 1 3 1 2 1 2 2 5 1 3 1 6 3 4 1 2 2 3 margin = 1 6
In other words, the set of high-priority buffers takes all the available bandwidth (up to its total fill rate if they are all empty) and the exact priority function within Γ is irrelevant to lower priority buffers. Now, let g i (t, Ω, ∆ j (t)) denote the transfer rate from buffer i if the effective dump rate available to buffers in Ω at time t is ∆ j (t) and all buffers in Ω have the same priority as i. It can be computed recursively as follow:

• ∆ j (t) is initialized with the residual rate δ j -g Γ (t). If Ω contains empty buffers, let ℓ be one with minimum fill rate. If f ℓ (t) < ∆ j (t)/|Ω|, then g i (t, Ω, ∆ j (t)) = f ℓ (t). This value can be subtracted to the effective dump rate and ℓ be ignored in order to compute, for all i ̸ = ℓ, g i (t, Ω, δ j ) = g i (t, Ω \ {ℓ}, δ j -g ℓ (t, Ω, δ j )).

• Otherwise, every buffer in Ω could transfer at a rate greater than or equal to ∆ j (t)/|Ω|, and therefore they transfer at that rate through the round-robin policy.

In Example 1, at time t = 1 and Ω = {1, 2, 3} we initially have ∆ j (t) = 1. Buffer 3 is empty and f 3 (t) = 1/6 < 1/3, so we set ∆ j (t) = 1 -1/6 = 5/6 and Ω = {1, 2}. Buffer 2 is empty and f 2 (t) = 2/5 < 5/12, so we set ∆ j (t) = 5/6 -2/5 = 13/30, which is the transfer rate of buffer 1.

Therefore, if we know the usage U i (t) of each buffer i at time t, their fill rates f i (t) and the current dump rate δ j , we can compute all the transfer rates at time t by applying the method above, starting with the batch Ω of buffers of highest priority, until either all buffers have been explored or the residual bandwidth at time t is null. This takes O(n log n) time.

Moreover, notice that fill and dump rates are piece-wise constant and hence the transfer rates are also piece-wise constant, and the usage rates are piece-wise linear. Therefore, we only need to compute those rates at the inflection points, i.e., when one of the following events happens: the dump rate changes or the fill rate of a buffer changes or a buffer becomes empty.

Changes in dump rates occur when downlink windows starts and ends, and are thus known in advance as are changes in fill rates. Moreover, given the fill and dump rates at time t, the transfer rate of each buffer can be computed as shown above, and hence it is easy to know when a buffer would become empty at the current rate. Such "empty buffer" events need to be inserted only when they are relevant, i.e., when they come earlier than the next rate-change event. Moreover, at most n such events can occur before the next rate-change event.

Therefore, there are O(n(ν + m)) events to explore in total.

For each event, the memory usages are updated w.r.t. the previous event, and dump and fill rates are updated in O(n) time.

The complexity of an iteration is dominated by the computation of the round-robin dump rate g i for every buffer i. As explained above, this can be done in O(n log n) by sorting the buffers and applying the proposed recursion. Moreover, the Θ(ν + m) events known "a priori" must be sorted, which costs Θ((ν + m) log(ν + m)) and the worst case time com-

plexity is in O((ν + m)(log(ν + m) + n 2 log n)).

Problem Complexity

We consider here the decision problem PRIORITYALLOC: "Is there a priority assignment for each downlink window such that there is no data loss?". Theorem 1. The problem PRIORITYALLOC is NP-complete.

Proof. It is in NP by Lemma 1, since verifying that a priority allocation entails no data loss is polynomial. To show hardness, we use a reduction from PARTITION, which, given a set A = {a 1 , . . . , a m } of positive reals with m j=1 a j = 1, asks if there is a set S ⊆ A such that aj ∈S a j = 1 2 . We build an instance π(A) of PRIORITYALLOC with m downlink windows, such that window j has duration a j and dump rate 2, and m + 2 buffers 1, . . . , m + 2. Buffers m + 1 and m + 2 have capacities 3 2 , while buffer j has capacity a j for j ∈ [1, m]. The fill rates f m+1 and f m+2 are equal to 1 for a duration 1 before the first downlink window, then they are equal to 1 during every downlink and null otherwise. Moreover, f j is equal to 2 during window j and is null otherwise.

Any solution of π(A) satisfies the four following properties:

1. Every buffer must be full at the end of the last window.

Indeed, the cumulative amount of data produced is 6 while a most 2 can be dumped. Moreover, the capacities of buffers m + 1 and m + 2 add up to 3 and the capacities of all other buffers add up to 1.

2. Buffer j cannot have priority strictly higher than both m + 1 and m + 2 in window j. Indeed, if j had strict priority over m + 1 and m + 2, then all data produced on this buffer would be dumped and it would be empty at t = e m , which contradicts Property (1).

3. In window j, for any k < j, the priority of k must be low enough so that no data is dumped from this buffer. This is a direct consequence of Property (1) since no more data will be produced on buffer k.

4. Either m + 1 or m + 2 must have a strictly lower priority than j, and none can be of strictly higher priority in window j. Indeed, if neither m + 1 or m + 2 is ranked lower than j, then it cannot get more than 1/3 of the bandwidth. Therefore, it cannot dump more than 2a j /3 in window j and the residual data (4a j /3) exceeds its capacity. Moreover, if either m + 1 or m + 2 has strict priority over j, it will take the whole bandwidth since they both contain data at all times. Therefore, buffer j would not dump any data and hence exceeds its capacity.

Therefore, on window j, there are only two feasible ranking:

1. P(m + 1) = P(j) > P(m + 2) ≥ P(k) ∀k ∈ [1, j -1] 2. P(m + 2) = P(j) > P(m + 1) ≥ P(k) ∀k ∈ [1, j -1]
In the first case, buffers m + 1 and j share the bandwidth equally (i.e., the dump rate is 1 for each) and at the end of window j, the data on buffers j and m + 2 has increased by a j . The usage of all other buffers remains the same.

The second case is symmetric, and at the end of window j, the data on buffers j and m + 1 has increased by a j .

In other words, there is an equivalence between the choice among these two rankings and the choice of a partition for element a j . Therefore, given a solution S of an instance A of PARTITION, we can build a solution of the instance π(A) of PRIORITYALLOC where, on window j, the priority is

P(m + 1) = P(j) > P(m + 2) > P(k) ∀k ∈ [1, j -1] if a j ∈ S and P(m + 2) = P(j) > P(m + 1) > P(k) ∀k ∈ [1, j -1] if a j ∈ S otherwise.
It can be verified that this solution does not exceed any buffer's capacity.

Consider now a solution of the instance π(A). On each window j, the usage of exactly one of buffers m + 1 and m + 2 grows by a j . Since the final usage of both buffers is 1 2 , they form an equi-partition of A and we can conclude that the instance A of PARTITION is satisfiable.

This reduction requires m buffers and m downlink windows, and hence does not preclude that an efficient algorithm exists if either parameter is fixed. In the next section we show that the problem is polynomial for a single window.

Polynomial Algorithm for a Single Window

Let M Γ≺Ω (i, j) = C i -max t∈[ej-1,ej [ (U i (t)) /C i
be the usage margin of i in the interval [e j-1 , e j [, with Γ the set of buffers with priority over i and Ω the set of buffers with same priority as i. The usage U i (t) of buffer i at all times t can be computed efficiently using the algorithm Simulation with a priority assignment compatible with the definition of Γ and Ω, since the exact priority within Γ is irrelevant. It follows that M Γ≺Ω (i, j) can also be computed efficiently.

The four following lemmas lead to a method (Algorithm 1) to decide if there exists a priority assignment of the buffers such that given their usage at time e j-1 , every buffer has a margin of at least obj in [e j-1 , e j [, with e 0 = 0 and s m+1 = ∞. Lemma 2. i = k or k ̸ ∈ Ω or M ∅≺Ω (i, j) ≥ M {k}≺Ω\{k} (i, j).

Algorithm 1: An Algorithm for a Single Window Algorithm: SINGLEWINDOW Data: A downlink window j, a target margin obj Result: Returns ∅ and sets the priority ranking Pj on B for downlink window j, if there is one that achieves the target margin. Otherwise, returns a minimal set of buffers that would exceed the target margin even if all other buffers were given less priority.

p ← 0 B ← {1, . . . , n} while B ̸ = ∅ do Ω ← B 1 repeat Ω ′ ← Ω 2 Ω ← {i | i ∈ Ω & M B\Ω≺Ω (i, j) ≥ obj} until Ω ′ = Ω 3 if Ω = ∅ then return B 4 foreach i ∈ Ω do Pj(i) ← p 5 B ← B \ Ω p ← p + 1
Proof. If given a strictly higher priority k can only take more bandwidth, and hence the margin of i can only decrease.

Lemma 3. If M ∅≺Ω (i, j) < M , then the priority of i cannot be the lowest of all buffers in Ω, if the minimum margin is M .

Proof. By lemma 2, the margin can only decrease if any buffer except i is given more priority.

Lemma 4. If for every i ∈ Ω, we have M ∅≺Ω (i, j) < M , then there is no solution with margin M or larger.

Proof. By lemma 3, no buffer in Ω can be of lowest priority among all buffers in Ω, which is a contradiction.

Lemma 5. If i ∈ Ω =⇒ M Γ≺Ω (i, j) ≥ M , then there is a solution with margin at least M if and only if there is a solution with margin at least M for the set of buffers Γ.

Proof. "If": Suppose that there is a solution for Γ with margin ≥ M . Give the same priority (strictly lower than that of any buffer in Γ) to all buffers in Ω. Since M Γ≺Ω (i, j) ≥ M for all i ∈ Ω, this solution extends to a solution of Γ ∪ Ω with margin ≥ M . "Only if": Trivial.

Algorithm 1 first tries to determine which buffers can be of lowest priority. In Loop 1 the margin of all remaining buffers are computed conditional to all having the lowest priority. By lemma 3, the buffers whose margin is below obj cannot be of lowest priority. Therefore, we remove those buffers with margin less than M from the candidate set for lowest priority Ω and iterate. If eventually no buffer can have a margin equal to or larger than M , we can conclude that there is no solution by lemma 4. Otherwise, in Line 4, we set the priority of the buffers in Ω, and we can ignore these buffers by lemma 5.

In the worst case, i.e., when the priority has to be a total order and a single buffer is removed from Ω at each iteration of Loop 1, Algorithm 1 requires O(n 2 ) calls to Simulation. . . ,Cn,[s1,e1[,. . . ,[sm,em[,f), initial memory usage U, a step parameter ϵ ub ← RelaxBandwidth(X) lb ← 0 while lb < ub do clear handover constraints

1 P, lb ← DownlinkCount(X, lb) M ← Repair(X, P, U, lb + ϵ) if M > lb then lb ← M else ub ← lb return lb
Notice that, besides the margin, we can check handover constraints (specific bound on the usage of a buffer at the end of a downlink) with the same method. Moreover, we also only need to know the sets of buffers of higher and equal priority. In other words, on the downlink window [s j , e j [, we can change the test at Line 2 to: M B\Ω≺Ω (i, j) ≥ obj & U i (e j ) ≤ r i (j) and Algorithm 1 remains correct.

A Heuristic for Priority Assignment

Here we consider the general (NP-complete) problem, with buffer usage carrying over multiple downlink windows.

We propose a heuristic (Algorithm 2) which implements a greedy "descent": a seed priority assignment is computed using the heuristic DownlinkCount [Rabideau et al., 2017] in Line 1, and iteratively "repaired" via Algorithm 3 to achieve a strictly higher target margin (by a step ϵ = 10 -5 ).

It simulates the current priority assignment until reaching downlinks j at which the target margin is exceeded. Then, at line 2 it calls Algorithm 1 to check whether there exists a priority assignment P j that achieves the expected margin.

If there is such an assignment, it is run by Simulation at Line 1 and we advance to downlink window j + 1. If the last window is reached, an improving solution has been found. Otherwise, if downlink j does not have a priority assignment without data loss, Algorithm 1 returns a set B of buffers guaranteed to exceed their target margin given the current usage at the end of downlink j -1, even if they are given (globally) the highest priority. Therefore, the only way to avoid data loss in this downlink is to reduce the residual load for at least one of these buffers at the end the previous downlink.

In order to avoid branching on the possible ways of reducing this load, we instead add one randomly chosen handover constraint at Line 4. We pick a random buffer i in the set B and we set its maximum handover value r i (j -1) to the current usage U i (j -1) to which we subtract the gap we need to achieve the expected margin: the margin we obtain when buffer i is given highest priority with all other buffers in B (that is, M ∅≺B (i, j)) minus the expected margin obj. Then the previous window is solved again with this new constraint: it "backtracks" by decreasing the current downlink window j Algorithm 3: A heuristic to repair a assignment

Algorithm: Repair Data: An oMDP instance X = (C1, . . . , Cn,[s1,e1[,. . . ,[sm,em[,f), priority assignment P, current usage U, target margin obj Result: Update the priority assignment P and return the corresponding margin obj ′ > obj, or ∅ if no improving priority assignment was found

obj ′ ← 1 j ← 1 while j ≤ m + 1 do 1 Simulation([ej-1, ej], X) M ← min{ C i -U i (t) C i | i ∈ {1, . . . , n}, t ∈ [ej-1, ej]} if M ≥ obj then obj ′ ← min(M, obj ′ ) j ← j + 1 else repeat 2 B ← SINGLEWINDOW({1, . . . , n}, [sj, ej[) if B ̸ = ∅ then if j = 1 then return ∅ 3 j ← j -1 pick a random buffer i ∈ B 4 ri(j) ← Ui(ej) -(M ∅≺B (i, j) -obj)Ci until B = ∅ return obj ′
at Line 3. If the current downlink window is the first (j = 1), then no such constraint can be posted and we fail.

Observe that Algorithm 2 converges since at Line 4, one maximum handover value strictly decreases. Therefore, eventually, either the last window will be solved with the expected margin, or the first window will be proven unsatisfiable (given the choice of handover constraints).

Experimental Evaluation

The software used for the real mission (DALLOC) is a proprietary software. Therefore, we could not directly compare our method to it and instead we re-implemented the best heuristic described by Rabideau et al.. This approach relies on a heuristic called DOWNLINKCOUNT (DC for short). This methods greedily assigns priorities based on when each buffer would exceed a given target margin. More precisely, it counts in how many downlinks would occur before exceeding the target if no data is dumped. At each downlink window j ∈ [1, m], the transfers are computed starting from the current usage, and with a dump rate equal to 0. Then a priority assignment is extracted as defined above, and window j is simulated using the same procedure but with dump rate δ j . It is important to notice that the choice of target margin can change the priority assignment. Therefore, in DALLOC, this heuristic is used within a binary search. The resulting algorithm is denoted ITERATEDLEVELING (IL for short). We do not compare with two other methods introduced by Rabideau et al. that were found to be less effective, in particular because they are not suited to the binary search method (IL).

In this section we first give some evidence that our implementation using a faster data transfer simulation algorithm is more efficient than DALLOC's. Then, we compare REPAIRDES-CENTwith our implementation of ITERATEDLEVELING, using the same hardware and common routines. We used the same data set as Rabideau et al., constituted of four scenarios (MTP1, MTP2, MTP3 and MTP4), corresponding to the whole activity sequence of Rosetta divided in four quarters. The whole sequence has over 40,000 data production events for 16 memory buffers and 324 downlink windows.

Its duration is about three months and a half with a precision of one second. It turns out that the first three can be solved to optimality as a simple lower bound matches the results of our method or DALLOC's ITERATEDLEVELING.

The last instance (MTP4) is not trivial. However, in order to get significant results, we generated a synthetic data set. We first added 48 new buffers, for a total of 64, as follows: For each memory buffer in the original data set, we created three "clones" whose capacities and fill rates were multiplied by a factor drawn uniformly randomly in [0.8, 1.2] and whose activities were shifted in time drawn uniformly randomly in [0s, 3600s]. Then, for each value of n in {8, 12, . . . , 36} we randomly chose n memory buffers, and generated one instance for a set of time intervals defined by the ends of two downlink windows x and y. We generated 14160 instances: each one is parameterized by the number of buffers n and the first and last considered downlinks are multiple of 5 x, y ∈ {0, . . . , 325} such that x + 10 ≤ y.

Re-implementation of DOWNLINKCOUNT

Table 1 shows the results published in [Rabideau et al., 2017] for DOWNLINKCOUNT and the results of our implementation. We believe that the main difference is the algorithm used to play the downlinks given a priority assignment. We used Algorithm Simulation, and we can clearly see a speedup: even though the hardware may not be equivalent, it cannot account for the speedup of several orders of magnitude. We also observe that our version finds downlink plans with higher margin for MTP1 and MTP2. This is because the results of Rabideau et al. include pre-assigned (high) priorities for some buffers due to some specific constraints of the actual mission. We are confident, however, that this implementation is truthful, and at least as effective as the one in DALLOC.

Comparison with the State of the Art

Now that we have established that our implementation is at least as efficient as the one in DALLOC, we can compare the algorithm proposed in this paper (REPAIRDESCENT) with the approach introduced by Rabideau et al. (ITERATEDLEVELING). Table 2 shows the results of both approaches (denoted respectively RD and IL) on the original instances. We report the minimum margin (in percent of the capacity) and the average CPU time. The three first instances are solved to optimality, witnessed by the simple upper bound (UB) consisting in allocating the full bandwidth to every buffer. Observe, moreover, that our implementation of DOWNLINKCOUNT also solves MTP1 optimally, but not MTP2 nor MTP3. This indicates that on MTP1 in particular, the bottleneck on each downlink window is mainly due to a single memory buffer. Yet, finding this critical buffer might not be straightforward (such as in MTP2 and MTP3), since priority decisions can have an impact far downstream. On MTP4, however, the bottleneck is likely due to a much more complex interaction between buffers, and no approach can reach the upper bound. Our method improve the minimum margin by 4.3 points over the solution found by ITERATEDLEVELING. CPU times are comparable and very low (under a second for all instances).

The real scenarios do not give us enough datapoints for a statistically significant comparison. Therefore we ran these approaches on the large dataset described above. Table 3 gives an overview of the results. We ignored the instances for which both REPAIRDESCENT and ITERATEDLEVELING find the same margin (32% of the data set). For the other scenarios we give the average minimum margin and the average CPU time for these two algorithms (denoted respectively RD and IL) as well as for the heuristic DOWNLINKCOUNT (DC), for four classes of instances: those with 12 buffers or fewer, with less 20 buffers, with 24 to 28 and with 32 buffers or more. We can see that our algorithm finds more robust transfer plans, by about 2.5 points for the first class, 4.5 points for the second class, 6.6 for the third and 8 points for last. It requires, however, much more CPU time on large instances.

These average results on CPU times might be deceiving, however. Figure 2 shows the average best margin X after Y seconds for the instances with at most 20 buffers and for more than 20 buffers. We can see that REPAIRDESCENT is actually faster than ITERATEDLEVELING to find solutions of similar quality. In other words, it takes more time to converge because it continues to optimize the plan for longer. We ran randomized versions of the algorithms. In the case of DOWN-LINKCOUNT, each of the m priority decisions randomly uses a total ordering based on the two versions discussed earlier, based time or the window of the first data loss. The heuristic is then called 10000 times. For ITERATEDLEVELING, we simply use the randomized version of DOWNLINKCOUNT whereas REPAIRDESCENT is naturally randomized because handover constraints are chosen randomly. In both cases, the number of runs per iteration is shown besides the method name. From these graphs, it is clear that investing more time via randomization can pay off, however, REPAIRDESCENT is almost always the best choice.

Conclusion

We proposed an efficient algorithm to simulate data transfers under priorities, and overlapping data production and dumping. Then, we showed that deciding if there is a priority assignment without data loss is polynomial for a single downlink, but NP-complete for multiple downlinks. Finally, we proposed a heuristic for allocating priorities over multiple windows based on the exact algorithm for a single window. This approach significantly outperforms the state of the art for the overlapping Memory Dumping problem.

Figure 1 :

 1 Figure 1: Illustration of Example 1. White areas indicate visibility.

Algorithm 2 :

 2 A heuristic for multiple downlinksAlgorithm: Descent Data: An oMDP instance X = (C1, .

Figure 2 :

 2 Figure 2: Comparison with the state of the art on synthetic scenarios.

Table 1 :

 1 New and old implementations of DOWNLINKCOUNT.

		MTP1	Margin MTP2 MTP3	MTP4	Avg. CPU
	DALLOC's	40.4	46.5	17.8	29.8	14.6
	Ours	46.4	68.1	17.8	30.8	0.018

Table 2 :

 2 Comparison with the state of the art on real scenarios.

		MTP1	Margin MTP2 MTP3	MTP4	Avg. CPU
	UB	46.4	72.5	54.8	53.4
	IL	46.4	72.5	54.8	48.5	0.116
	RD	46.4	72.5	54.8		0.088
	≤ 12	16-20		24-28	≥ 32
	M. CPU M. CPU	M.	CPU	M.	CPU
	DC 28.7	0.0 -41.5	0.1 -249.3	0.1 -460.7	0.1
	IL 47.1	0.3 22.9	0.8 -22.4	1.4 -68.7	2.2
	RD 49.6	0.1 27.4	1.1 -15.8	7.5 -60.7 31.3

Table 3 :

 3 Comparison with the state of the art on synthetic scenarios.

Acknowledgements

Part of this research was carried out at the Jet Propulsion Laboratory, California Institute of Technology, under a contract with the National Aeronautics and Space Administration (80NM0018D0004). Part of this work was supported by the AI Interdisciplinary Institute ANITI, funded by the French program "Investing for the Future -PIA3" under grant agreement no. ANR-19-PI3A-0004. We would like to thank the European Space Agency and in particular Miguel Perez Ayucar and Federico Nespoli for providing data.


Emmanuel Hebrard
email: hebrard@laas.fr.

Christian Artigues
email: artigues@laas.fr.

Pierre Lopez
email: lopez@laas.fr.

Arnaud Lusson

Steve Chien
email: steve.a.chien@jpl.nasa.gov.

Adrien Maillard
email: adrien.maillard@jpl.nasa.gov.

Gregg Rabideau
email: gregg.r.rabideau@jpl.nasa.gov.

Data transfer scheduling for deep space exploration

1 The overlapping memory dumping problem Scientific instruments for deep space exploration spacecrafts become more and more sophisticated and consequently produce more and more data that must be sent to Earth. Data management is highly critical as the onboard memory is limited and communication with Earth is often a bottleneck. In this paper we consider the same case as in [START_REF] Rabideau | Managing Spacecraft Memory Buffers with Concurrent Data Collection and Downlink[END_REF] in the context of the Rosetta/Philae mission, where the data production plan is known and the problem consists in planning memory dumps. Data is produced into several memory buffers and the goal is to avoid data loss, which occurs when data are produced into a full buffer. More precisely, we want to maximize the minimum margin of buffer, where the margin is the percentage of its capacity left free. This objective aims at designing robust plans where unexpected changes of the dump or fill rates can be absorbed by the margins. Under this assumption, the fill rate of each memory buffer over the planning horizon is part of the input. Data can only be dumped when the spacecraft is visible from Earth. This is materialized by consecutive disjoint downlink windows. Data dumping is a semi-automatized process. For each downlink window a priority has to be assigned to each buffer, then, the transfers follow this priority ordering. We therefore consider the problem of computing a priority assignment that maximizes the minimum margin.

In the overlapping Memory Dumping Problem (oMDP), we are given m downlink windows, where [s j , e j [ stands for the time interval in which the downlink j is available, and δ j for the dump rate for transfers of downlink j. Moreover, there are n memory buffers, where C i stands for the capacity of buffer i; r i (j) for the maximum handover (residual) usage of buffer i at the end of downlink window j; and f i : R → R + for the piece-wise constant fill rate function of buffer i over time. Let ν be the number of inflection points over all fill rate functions.

The transfers can be controlled by setting a priority function over the buffers defining a ranking. At every step, one of the buffers of highest priority among those who have a packet in memory is selected via round-robin to transfer a packet. Let U i R → R be the quantity of data on buffer i over time and g i : R → R be the transfer rate out of buffer i over time.

B3 B2 B1 t = 0 t = 1 t = 3 t = 4 t = 6 1 -1 6 -2 5 1 2 1 3 1 2 1 2 2 5 1 3 1 6 3 4 1 2 2 3 margin = 1 6
In between downlink window, all transfer rates are null and the memory usage growth is the fill function, for every buffer i. In particular, for any time t preceding the start of the first downlink s 1 , we have g i (t) = 0 and U i (t) = t 0 f i (x) dx. During a downlink window with dump rate δ, however, the effective transfer rate at time t depends on the priority function P, and on the usages and fill rates at time t. We consider the decision problem of finding a priority ranking for every downlink, such that the peak usage of any buffer (given its fill rate functions, and the data transfer system described above) is less than its capacity, i.e., without data loss. The objective function is actually to maximize the minimum margin, min{M (i) | i ∈ B}, where M (i) is defined as one minus the ratio between the peak usage and the capacity of buffer i. However, it can be achieved by dichotomic search using an algorithm for the decision problem above.

Example 1. Figure 1 shows a plan with two downlinks, both with dump rate 1, and 3 buffers all of capacity 1. Fill rates are figured by colored rectangles, e.g., f 1 (t) = 1 2 for t ∈ [0, 1]. In the first downlink, all buffers have equal priority P 1 (1) = P 1 (2) = P 1 (3) = 1, in the second, buffer 3 has the highest priority then buffer 2 then buffer 1. The black curves stand for the resulting buffer usage over time U i (t). The minimum margin is 1 6 .

Complexity and algorithms

The software used for the real mission (DALLOC) is described in [START_REF] Rabideau | Managing Spacecraft Memory Buffers with Concurrent Data Collection and Downlink[END_REF] and relies on a heuristic called DOWNLINKCOUNT. In a nutshell, this method assigns priorities based on when each buffer would exceed a given target margin. More precisely, it counts how many downlink windows would occur before exceeding the target if no data could be dumped. At each downlink window j ∈ [1, m], the transfers are computed starting from the current usage, and with a dump rate equal to 0. Then a priority assignment is extracted as defined above, and window j is simulated using the same procedure but with dump rate δ j . It is important to notice that the choice of target margin can change the priority assignment. Therefore, in DALLOC, this heuristic is used within a binary search. The resulting algorithm is denoted ITERATEDLEVELING.

As the complexity of the problem was not established, we first consider the decision problem PRIORITYALLOC: "Is there a priority assignment for each downlink window such that there is no data loss?".

First, we show that the problem is in NP because, given a priority assignment, simulating the transfers and therefore verifying a certificate, can be done in polynomial time, using similar arguments as in [START_REF] Simonin | Scheduling scientific experiments for comet exploration[END_REF]. This is not trivial to see that not every packet of data need to be tracked individually, and the number of packets can be exponential in the size of the instance. Moreover, to compute the usage over time of a given buffer, we only need to know the set of buffers of strictly higher priority and the set of buffers of equal priority (Property 1). In other words, the exact priority assignment within the set with higher priority is irrelevant. We define a procedure (denoted Algorithm 1 from now on) to compute the memory usages (and so the minimum margin

) in O((ν + m)(log(ν + m) + n 2 log n))
time, given a priority assignment P on each downlink window. Then we use a reduction from partition to show that PRIORITYALLOC is NP-complete.

Next we consider the single-window problem (m = 1). Thanks to Property 1 and Algorithm 1, it is possible to compute the margin M Γ≺Ω (i, j) of buffer i in window j when the buffers in the set Γ have a strictly higher priority than i, and the buffers in the set Ω have the same priority as i. We propose a method (Algorithm 2) to solve PRIORITYALLOC on a single downlink window with O(n 2 ) calls to Algorithm 1.

Finally, for the general case, we propose a heuristic (REPAIRDESCENT) which implements a greedy "descent": a seed priority assignment is computed using the heuristic DOWNLINKCOUNT and iteratively "repaired" to achieve a strictly higher target margin.

The repair procedure runs the current priority assignment using Algorithm 1 until reaching downlink j at which the target margin is exceeded. Then, it calls Algorithm 2 to check whether there exists a priority assignment P j that achieves the expected margin. If there is such an assignment, it is run by Algorithm 1 and we advance to downlink window j + 1. If the last window is reached, an improving solution has been found. Otherwise, if downlink j does not have a priority assignment without data loss, Algorithm 2 returns a set B of buffers guaranteed to exceed their target margin given the current usage at the end of downlink j -1, even if they are given (globally) the highest priority. Therefore, the only way to avoid data loss in this downlink is to reduce the residual load for at least one of these buffers at the end the previous downlink. In order to avoid branching on the possible ways of reducing this load, we instead add one randomly chosen handover constraint. We pick a random buffer i in the set B, and we set its maximum handover value r i (j -1) to the current usage U i (j -1) to which we subtract the gap we need to achieve the expected margin: the margin we obtain when buffer i is given highest priority with all other buffers in B (that is, M ∅≺B (i, j)) minus the expected margin obj. Then the previous window is solved again with this new constraint: it "backtracks" by decreasing the current downlink window j. If the current downlink window is the first (j = 1), then no such constraint can be posted and we fail.

Experimental Evaluation

We used the same data set as in [START_REF] Rabideau | Managing Spacecraft Memory Buffers with Concurrent Data Collection and Downlink[END_REF], constituted of four scenarios (MTP1, MTP2, MTP3 and MTP4), corresponding to the whole activity sequence of Rosetta divided in four quarters.

The whole sequence has over 40,000 data production events for 16 memory buffers and 324 downlink windows. Its duration is about three months and a half with a precision of one second. Table 1 give the margin value DOWNLINKCOUNT incorporating Algorithm 1 and DALLOC's published results [START_REF] Rabideau | Managing Spacecraft Memory Buffers with Concurrent Data Collection and Downlink[END_REF], as well as average CPU times for both algorithms. We observe that our reimplementation is much faster than the original one. Finally, on a much larger randomly generated data set, REPAIRDESCENT is consistently faster than ITERATEDLEVELING to find solutions of similar quality and is able to significantly improve the minimum margin when given more CPU time.

Figure 1 :

 1 Figure 1: Example with 3 buffers. White areas indicate visibility.

Table 1 :

 1 New and old implementations of DOWNLINKCOUNT.Moreover, REPAIRDESCENT finds a more robust download plan for the hardest real scenario (MTP4). Both methods match an upper bound on MTP1, MTP2, and MTP3.

	1

Table 2 :

 2 Comparison with the state of the art on real scenarios.

The slight difference in margin values is because DALLOC's results include pre-assigned priorities. We did not have the data to reproduce it.


Paolo Tranquilli
email: ptranqui@pps.jussieu.fr

Confluence of Pure Differential Nets with Promotion

come

Confluence of Pure Differential Nets with Promotion

Introduction

The inception of Linear Logic (LL, [START_REF] Girard | Linear logic[END_REF]) in the 80's has reinforced the bridge between logic and computer science already established by the Curry-Howard correspondence years before. LL is in fact a refinement of intuitionistic and classical logic brought forth by a fine semantical analysis. One of its main features is the introduction of two dual modalities, the exponentials ! and ?, regulating the use of structural rules (weakening and contraction), which on the program side correspond to erasure and duplication of resources. This endeavour, among other things, led the way to a new, parallel syntax of proofs, proof nets. These are the syntax of choice for LL, especially when considering cut elimination. In fact one of the main advances of LL over classical logic is that, though preserving an involutive negation (and therefore twosided sequents), it also preserves properties of intuitionistic logic lacking in the classical framework. One of these, central to our work, is confluence of cut elimination, i.e. the independence of the result of the cut elimination procedure with respect to the actual cuts one decides to reduce.

A further semantical analysis led by Ehrhard [START_REF] Ehrhard | Finiteness spaces[END_REF] has recently provided LL with new models based on topological vector spaces where we can take the derivative of an object. The efforts of the same author and Regnier have permitted to lift such operations to syntax, giving rise to Differential Linear Logic (DiLL, [START_REF] Ehrhard | Differential interaction nets[END_REF]), and their syntax, differential nets. Three new rules are introduced to handle the !-modality (coweakening, cocontraction and codereliction) which are duals to the LL rules handling ?. In the proofs as programs paradigm, codereliction allows to introduce depletable resources, which may be asked for many times but may be used just one time, nondeterministically choosing which query they satisfy. This feature configures differential nets as a promising logical framework to extend the Curry-Howard correspondence to nondeterminism and concurrency (see [START_REF] Ehrhard | Interpreting a finitary pi-calculus in differential interaction nets[END_REF]).

Actually, [START_REF] Ehrhard | Differential interaction nets[END_REF] gives the syntax for the promotion free fragment of DiLL only, giving rise to differential interaction nets, a nondeterministic example of Lafont's interaction nets [START_REF] Lafont | Interaction nets[END_REF]. By modelling nondeterminism by formal sums confluence remains an important property, which is however straightforward in an interaction net paradigm, where no reduction can change the other ones. Here we will extend such property to the whole of differential nets. Promotion in proof nets is handled by boxes, synchronized areas of proofs enabling to mark what is to be erased or duplicated. Boxes break the interaction net paradigm: there are cuts (the commutative ones) which can be changed by other reductions, so confluence is definitely more delicate.

Part of a previous work of ours [START_REF] Tranquilli | Intuitionistic differential nets and lambda calculus[END_REF] was focused on proving confluence for the intuitionistic fragment, which used the recursive types needed to translate λcalculus. There we observed that confluence fails without keeping into account some semantically grounded equivalences, namely associativity of contractions and cocontractions. A fully quotienting syntax as the one used in [START_REF] Regnier | Lambda-Calcul et Réseaux[END_REF] for LL is seemingly out of reach in DiLL. Our solution in [START_REF] Tranquilli | Intuitionistic differential nets and lambda calculus[END_REF] was employing generalized (co)contraction cells in the style of [START_REF] Di Cosmo | Strong normalization of proof nets modulo structural congruences[END_REF], and some additional reductions.

Here we generalize the result in three ways. By concentrating on the computational contents rather than the logical one, we consider pure nets, where types (i.e. formulae) play no role whatsoever, not even recursive ones. Furtherly, the needed equivalences are settled to the maximum extent by means of. . . equivalences on nets. We thus generalize the equivalences and reductions of [START_REF] Di Cosmo | Proof nets and explicit substitutions[END_REF], providing as a byproduct the first proof of confluence 1 for such LL proof nets with equivalences in the completely pure case, as previous works concentrated on normalization in the typed one. Finally, we are able to introduce one more equivalence potentially giving the right to always consider boxes without sums inside (the bang sum equivalence). This result has several ramifications. As is evident in [START_REF] Pagani | Strong normalization property for second order linear logic[END_REF], this is the first step in proving strong normalization in the typed case 2 . Furtherly, as can be deducted from [START_REF] Di Cosmo | Proof nets and explicit substitutions[END_REF], this can be the ground for new work on calculi with explicit substitutions: whether by extending some results to untyped calculi; or by considering explicit substitutions for nondeterministic calculi akin to Boudol's λ-calculus with resources (see [START_REF] Tranquilli | Intuitionistic differential nets and lambda calculus[END_REF]).

Our technique, reminiscent of the work done on LL in [START_REF] Pagani | Strong normalization property for second order linear logic[END_REF], uses a finite development theorem used to prove a strong confluence property of a suitable notion of parallel reduction.

Rewriting Theory Modulo Equivalence

The aim of this section is making the reader acquainted with the notion of rewriting modulo equivalence, to the extent needed for our purposes. We refer to [START_REF]Term Rewriting Systems[END_REF]Section 14.3] for more indepth details and proofs.

Let (S, →) be an abstract reduction system and let ∼ be an equivalence relation on S. As usual, = → and * → denote the reflexive and reflexive-transitive closures of → respectively. Take also a symmetric relationsuch that - * = ∼, possibly ∼ itself. Let s ⊻ t (t and s are joinable modulo ∼) if s * →∼ * ← t. We say then that → is

-locally confluent modulo ∼ if ←→ ⊆ ⊻; -confluent modulo ∼ if * ←∼ * → ⊆ ⊻; -locally coherent with -if -→ ⊆ ⊻; -Church-Rosser modulo ∼ (or CR∼) if ≈ ⊆ ⊻, where ≈ := (→ ∪ ← ∪ ∼) * ; -strongly normalizing modulo ∼ (or SN∼) if → ∼ is SN, where 3 → ∼ := ∼→∼; -strongly Church-Rosser modulo ∼ if ∼ = ← = →∼ ⊆ = →∼ = ←;
The last definition is our terminology, while the rest follows [START_REF]Term Rewriting Systems[END_REF]. Being Church-Rosser modulo ∼ is the most important property of all those concerning confluence. In particular it implies the unique normal form modulo ∼ property, (≈ = ∼ on normal forms), which again implies that in order to compute the normal form one can use just regular reductions, without ever be forced to ∼-convert in order to get the result 4 . Contrary to what happens in regular reduction, CR∼ is strictly stronger than plain confluence in absence of WN [START_REF]Term Rewriting Systems[END_REF]Remarks 14.3.6,Exercise 14.3.7]. Following are some important lemmas: the first is a generalization of Newman's Lemma, the last is a trivial result we did not find in the literature which we will need in our proof.

Lemma 1 (Huet).

If → is SN∼, locally confluent modulo ∼ and locally coherent with -, then it is CR∼.

Lemma 2 (van Oostrom

). → is CR∼ iff * → is strongly CR∼. Lemma 3. If → is strongly CR∼, then it is CR∼.
Proof. Straightforward induction: to show that ∼ -A set p(π) of ports.

-A set c(π) of cells; to each cell c is assigned a symbol σ(c) in a given alphabet, a port in p(π) called principal, and a number of other, auxiliary ones. How the latter are treated distinguishes between two kinds of cells: in non commutative ones, auxiliary ports are a finite sequence, in commutative ones they form a finite set. Every port in p(π) can be associated with at most one cell; a port associated with a cell is called connected, otherwise it is free.

Free ports (also called conclusions) are denoted by fp(π). The number of auxiliary ports is determined by the symbol σ(c). -A set w(π) of wires, which can be either unordered pairs {p, q} of ports, or deadlocks, i.e. wires not connecting any port (intuitively short circuited wires). Each port is in exactly one wire. A directed wire is an ordered pair (p, q) such that {p, q} is a wire. Terminal wires are the directed ones going to the free ports.

An elementary path in π is one in the graph trivially obtained by taking cells and free ports as nodes and directed wires as edges, which moreover does not intersect itself 5 . A polynet is a formal sum of nets, or equivalently a multiset of nets, all sharing the same free ports. At times we distinguish nets (thus singletons) from polynets by calling them simple.

Statics

DiLL 0 nets and polynets are built from all the symbols in Figure 1 but the box one. These are exactly the differential interaction nets presented in [START_REF] Ehrhard | Differential interaction nets[END_REF]. For the moment let us ignore the labels we assign to the ports in the figure, which will be needed only later (see page 9). As usual, the apex of the cell represents the principal port, while the auxiliary ones are depicted on the opposite side.

In order to add boxes, one proceeds by induction, by considering them as cells having a whole polynet as symbol. Let DiLL k+1 nets and polynets be the ones built from all the cells of Figure 1 where for each box its symbol is a polynet π in DiLL k and there is a bijection between its ports and fp(π). The symbol σ(B) of a box B is also called its contents. We will denote by !π a generic box having π as contents. A DiLL polynet π is one of DiLL k for any k; if such k is minimal, we say that k is the depth of π (in fact, the maximal number of nested boxes). A port is active if it is either a principal one, or an auxiliary one of a box. A wire linking two active ports is a cut.

Figures 4 and5 will show examples of differential nets. The explicit marking of ports is dropped as they can always be identified with the extremities of wires.

Let p ! (π), fp ! (π) c ! (π) and w ! (π) be the set of all occurrences of ports, free ports, cells and wires respectively occurring in π, including in all the contents of the boxes in π. We can slice those sets by depth, so we will denote by p i (π), Fig. 1: The cells of differential nets. The labels in { !, ?, * } assigned to ports will be needed only later (see page 9).

fp i (π) c i (π) and w i (π) the corresponding elements of the nets contained in i nested boxes, where i is called the depth of the element in π6 .

Correctness criterion.

As usual, the nets blindly built with the cells available are not in general "correct", where the word can take the meaning of unsequentializable in sequent calculus, or having deranged computational behaviour.

Since [START_REF] Danos | The structure of multiplicatives[END_REF] one of the most used correctness criteria for proof nets is that of switching acyclicity. Given a DiLL net, a switching path is an elementary one which does not traverse two auxiliary ports of any `or contraction cell (does not bounce "above" it). A DiLL polynet is called a DiLL proof net (or differential proof net) if it is switching acyclic, i.e. it has no deadlocks nor switching cycles, and inductively all box contents are also switching acyclic. In particular from now on we can suppose all our polynets to be deadlock-free.

Dynamics

As with various calculi, the reduction of differential nets can be defined as the context closure of a set of reduction rules, presented as pairs of redexes and contracta. A linear context δ[ ] is a simple net δ together with a subset H δ of its free ports (the hole of δ[ ]). It is linear as it is not a sum and the hole is not inside a box. Given a simple net λ and a bijection σ between H δ and fp(λ), the plugging δ[λ] of a simple net λ in the hole of δ[ ] amounts to identifying the Fig. 2: The multiplicative and exponential reduction rules of DiLL. ε and ε denote either ? and ! or vice versa. α denotes any symbol among ! 2 , ! 0 or a box symbol π. In particular weakening against coweakening reduces to the empty net. We make implicit use of the rule for context plugging of sums: the π inside boxes is a polynet. For example the dereliction on box rule may introduce sums.

ports according to σ and welding the wires that come together in this way 7 .

δ p k p 1 H δ λ σ(p 1 ) σ(p k ) := δ λ
This definition is then extended by linearity when we plug a polynet, by setting

δ i λ i := i δ[λ i ].
Finally, contexts generalize the concept in the following way. A linear context δ[ ] is a context; furthermore if ω[ ] is a context then:

-δ[ω[ ]] for δ[ ] linear is a context 8 ; -ω[ ] + π for π polynet is a context; -!ω[ ] (i.e. a box containing a context) is a context.
Plugging is easily extended to all contexts. The context closure R of a relation R is then defined by π R σ iff π = ω[λ], σ = ω[µ] and λ R µ.

We are now able to define multiplicative reduction m → and the exponential one e → by context closure of the rules of Figure 2, which are pairs consisting of a simple net (the redex) and a polynet (the contractum). Each redex here is identified by a unique cut. The union me → of the two reduction is the cut elimination of DiLL.

Equivalences and Canonical Reductions

As we will show with Remark 5, the reductions just presented fail to give a confluent system: we cannot ignore associativity of (co)contractions and neutrality of (co)weakening over (co)contraction. This prompts us to introduce the former as an equivalence and the latter as a reduction. As we need anyway to consider reduction modulo an equivalence, we also study other equivalences (backed by semantical and observational equivalence) which are optional though must be taken together. Each equivalence is accompanied by a reduction which in a sense settles a zeroary case of the equivalence. Reversing each of these gives unwanted looping reductions. The associative, push and bang sum equivalences, together with the neutral, pull and bang zero reductions (which do not reduce cuts), are shown in Figure 3. The π, σ 0 condition is needed: without one would be able to spawn arbitrarily large trees of contractions, easily giving again unwanted looping reductions. From now on ∼ and c → (canonical reduction) will denote either a ∼ and n → or the union of the a, p and s conversions and the npz-reduction respectively.

Proposition 4 (stability of correctness). If π is switching acyclic and π

mec -→ π ′ or π ∼ π ′ then π ′ is switching acyclic also.
Proof. Many cases belong to the literature of LL and to [START_REF] Ehrhard | Differential interaction nets[END_REF]. The new ones are straightforward checks.

Let us spend some more words on ∼ and c →. The push equivalence 9 has already been studied in the literature on proof nets and explicit substitutions [START_REF] Di Cosmo | Strong normalization of proof nets modulo structural congruences[END_REF][START_REF] Di Cosmo | Proof nets and explicit substitutions[END_REF]. The pull reduction may seem somewhat complicated, however it is a generalization of the reduction pulling out weakenings from boxes [START_REF] Di Cosmo | Proof nets and explicit substitutions[END_REF]. The usual reduction can be reobtained when having ̺ = 0, which by means of a z-reduction and some n ones gives the expected result. Such form (which in fact contains a sort of on-the-fly s-conversion) is required in order to get local coherence. (b) Non-termination of exponential reduction with switching acyclicity. The part about sums inside boxes was already known to be valid semantically and observationally: we give here some sintactic ground to using it. From the point of view of semantics it is interesting to note that it implements the well known exponential isomorphism !A ⊗ !B !(A & B) from linear logic (see [START_REF] Ehrhard | Finiteness spaces[END_REF]).

Paolo Tranquilli

! π ! ! b a e → ! 2 ! π ! 0 ! π ! ? 2 ? 2 ! e * → ! 2 ! π ! 0 ! 0 ! π ! ! ? 2 + ! 2 ! 2 ! π ! 0 ! 0 ! π ! ! 0 ! π ! 0 ! ? 2 ? 2
⊥ me * ←- ! ? 1 1 ! ? ⊥ ⊥ me * -→ ! ? ⊥ 1 (a) Non-confluence
Examples and remarks. Figure 4 gives the reason to employ associative equivalence, showing the reduction of the coderelictions on box critical peak. One reduction only is shown, as the other is symmetric. One can already see two big differences with respect to LL and the work done with it in [START_REF] Pagani | Strong normalization property for second order linear logic[END_REF]: firstly, sums may arise even without the "logical" step of dereliction on box; moreover, the codereliction on box rule, which reduces a commutative cut, changes the possible cuts on all other cuts of the box. These problems prevent an immediate adaptation of the measures used in [START_REF] Pagani | Strong normalization property for second order linear logic[END_REF]. The nets in Figure 5 are examples already known in LL showing issues about correctness and types.

Remark 5. The net shown in Figure 4 is a counterexample to DiLL being confluent without a ∼. Other similar diagrams show we cannot also omit the n reduction.

The Finite Development Theorem

In [START_REF] Danos | La Logique Linéaire appliquée à l'étude de divers processus de normalisation (principalement du λ-calcul)[END_REF], Danos proved the counterpart of the finite development theorem for MELL, and Pagani and Tortora de Falco did the same for the whole of second order LL in [START_REF] Pagani | Strong normalization property for second order linear logic[END_REF]. In this setting the actual definition of what a "new" redex is gets more technical.

Marking New Cuts

We define a notion of new and old cuts, by leaving a mark on the new ones.

Marks are cells of a new symbol with two ports and no reduction rule, graphically depicted by little circles. Its main purpose is to block reductions and equivalences (for example a mark between two contractions blocks the a-conversion).

Ideally, these marks are placed during reduction to block "new" wires. By new we mean two kinds of wires: those that in a typed setting would decrease the logical complexity of the cut formula, and those that before the reduction were exponential clashes. The latter are peculiar to a truly untyped setting, and are brought by the opening box and neutral reductions, which erase an exponential port. For example, if we erase marks from the net shown in Figure 6, and we fire the dereliction against box redex we end up with a valid multiplicative cut which was a clash before. Rather than lock this special kind of "new" wires during reduction, we can lock all potentially dangerous clashes since the start, as markings will prevent new clashes from arising. We thus need to define what an exponential clash is.

Let τ be the partial function from p ! (π) to the labels { !, ?, * } thus defined. On ports of cells it gives the values already shown in Figure 1; on the ports of marks it is undefined; for p ∈ fp ! (π) we set τ(p) = ? if p is over an auxiliary port of a box, we leave it undefined otherwise. τ provides for a sort of pre-typing. A directed wire (p, q) is called a !-wire (resp. ?-wire) if τ(p) = ? and τ(q) = ! (resp. vice versa), where however we let at most one of the two be undefined. In any case ! and ?-wires are called exponential (which applies to undirected wires also). An exponential clash (simply clash from now on) is a wire {p, q} such that one of τ(p), τ(q) is ! (resp. ?) and the other is defined but not ? (resp. !) 10 .

DiLL • is the system given by polynets with marks and without clashes, and by changing some rules to introduce the mark as depicted in Figure 7. It is immediate to see that the absence of clashes is preserved by reduction, as the new wires which could bring close unmatched ports are interrupted by marks. From the point of view of DiLL, clash-freeness imposes just that some marks be added: given any DiLL polynet π, we define the injection π • in DiLL • by placing a mark interrupting each clash. Conversely, DiLL • can be clearly surjected on DiLL by erasing all marks. We call this surjection π • . The net π in Figure 6(a

Measuring Exponential Reduction

Ideally, we may regard exponential reduction as a procedure that "slides" cells along exponential paths in the net, with ! and ? cells sliding in opposite direction. We thus assign to each cut a natural number, indicating how far the two cells around it are from the end of the path they are sliding on. After a reduction however many cuts may have arisen. So we will employ the multiset of the weights of the cuts and the multiset order 11 . Global additive duplication poses another problem. In [START_REF] Tranquilli | Intuitionistic differential nets and lambda calculus[END_REF] we settled it by employing multisets of multisets. Here however we estimate how many addends can sprout during reduction, so we can use this value and count each cut as many times as there can be addends containing it. We will also need to get an estimate of the number of copies (both regular and linear) of a box.

Exponential paths.

An !-path (resp. ?-path) is an elementary path made only of !-wires (resp. ?-wires), not traversing any mark, dereliction or codereliction (though it may end on them). In either case, the path is called exponential. All cells internal to an exponential path must necessarily be contractions, cocontractions or boxes. The main technical advantage of DiLL • over DiLL is that in it no reduction can open new exponential paths.

Next we define by mutual induction three basic measures on which we will base the measure of the whole net. Two of them, the ?-weight ?(e) and the !-weight !(e), are on wires. The third, the spread sp(λ), is defined on simple nets.

Weighting wires and estimating addends. First, ?(e) = !(e) = 1 if e is not exponential; otherwise, let e be oriented so that it is an !-wire (resp. ?-wire), and let c be the node (either a free port or a cell) to which e thus points. Table 1 provides the laws for ?(e) (resp. !(e)), giving them depending on c. By e λ we denote the wire : ? :

(e i ) =        ?( f )(1 + j !(e j )) if π = 0, ?( f )(1 + j !(e j ))
!(e) = !( f ); e ! π f k f 1 : !(e) =        1 + j !( f j ) if π = 0, ( 1
+ i !( f i )) λ∈π sp(λ) otherwise. otherwise: !(e) = 1. sp(λ) = c∈c 0 (λ) σ(c)=? !(c) • c∈c 0 (λ) σ(c)=! ?(c)
Table 1. Rules for the ?-weight (top), the ! one (middle) and the spread sp (bottom). We remind that the subscripts of the products for the spread make them range over the derelictions and coderelictions at depth 0.

corresponding to e inside a box, in the net λ of the box contents. At the bottom we also show the law for the spread. Notice that there is a circular dependency between the three measures, so the next lemma is not trivial. Lemma 6. Given a DiLL • proof net π, ?(e), !(e) and sp(λ) are defined and unique for all e ∈ w ! (π) and all λ simple subnets of π at any depth.

→tech.app.

Proof (sketch). Substituting the free port cases by assigning variables, we get all the measures as polynomials in those variables (see the section on modularity). One then proceeds by a primary induction on the depth: supposing all the (polynomial) measures have been defined on strictly less depth, one can define !(e) by induction on the maximal length of ?-paths starting from e (instantiating the variables of the ?-conclusions inside boxes in the process);

only then, define ?(e) by induction on the maximal length of !-paths (relying also on measures at greater depth just instantiated); -finally define the spread from the two.

⊓ ⊔

Weighting nets and polynets. The weight |e| of a wire is ?(e) + !(e). Let !cw 0 (λ) (resp. b 0 (λ)) be the set of exponential cuts (resp. boxes) at depth 0 of a simple net λ. Let us fix a polynet π. Then for each sum (i.e. multiset) of subnets of π we define by induction on their depth the following multiset (λ will denote a generic simple subnet):

σ := λ∈σ sp(λ) λ , λ := [ |e| | e ∈ !cw 0 (λ) ] + B∈b 0 (λ) #(B) σ(B) ,
where #(B), the count of the box, is ?(e)(1 + j !( f j )) with e and f j the wires on the principal and the auxiliary ports respectively. In particular we just defined the measure for the whole net.

Notice that this measure depends monotonously from the weight of each part of the net. This intuition will be given a solid ground by the modularity Lemma 8.

Intuitive ideas of the measures. Morally !(e) measures the size of the tree of cocontractions above e (which is invariant under associativity). The most important feature is that it counts all the coderelictions linked to e. On boxes we count the !-weight on the auxiliary ports because the codereliction against box rule creates a contraction and a codereliction; plus one to count the box itself, especially if it has no auxiliary ports; -multiplied by the spread of the contents in order to be invariant by sconversion, and keep such invariants even if the sum inside. . . spreads.

Dually ?(e) measures the size of the tree of contractions above e. The rule when e is on an auxiliary port of a box B contains:

-?( f ) because the contractions on the principal port of B may shift to auxiliary ports during reduction; -the sum of !-weights of the auxiliary wires because codereliction against box creates contractions; plus 1 to provide something to decrease when a cut enters a box (box against box and those similar); -the ?-measures inside because either by opening the box or by p-conversion the contraction trees inside can pour outside; summed to respect both pconversion and s-conversion; however the sum is weighted with the internal spread to avoid that a reduction generating a sum inside could raise such weight.

As already hinted, sp(λ) estimates how many addends may have a reduct of λ. This is achieved by morally multiplying all the possible number of choices potentially to be done in λ. Now sums arise -on (co)dereliction against co(co)ntraction reductions, so the size of the tree of co(co)ntractions on the principal port of a (co)dereliction should estimate what choices that (co)dereliction may do; -on (co)dereliction against box rules, when the box contains an actual sum; however the spread of a box contents are already accounted for in both "moral" contraction and cocontraction trees.

Finally the cuts inside a box B count #(B) times as this number estimates how many regular and linear copies of its contents may be done, and all cuts count sp(λ) times to account for additive duplication.

Replacement and modularity lemmas. For the purpose of working modularly with the measure, we introduce variables on the terminal wires over fp 0 (π). So for each terminal ?-wire d (resp. !-wire), we consider variables !(d) (resp. ?(d)). All measures become then polynomials with natural coefficients; in the following, we will consider the extensional (i.e. pointwise) order ≤ on non-zero values for such variables.

For different simple nets λ, µ, we distinguish the weights calculated on one or the other by putting them as superscripts, as in ? λ (e). Suppose λ and µ are two nets with identified terminal wires C. We say that λ can replace µ if for each terminal wire d we have that ! λ (d) ≤ ! µ (d) and ? λ (d) ≤ ? µ (d) (one of the comparisons may be a trivial one among the same variables).

Lemma 7 (replacement). Suppose λ can replace µ, ω[ ] is a linear context with ω[λ]

and ω[µ] proof nets. Then for each e wire in the context ω, ? ω[µ] (e) ≤ ? ω[λ] (e) and ! ω[µ] (e) ≤ ! ω[λ] (e).

→tech.app.

Proof (sketch). By easy induction on ω[ ].

One gradually moves cells from ω to λ and µ, and then all the wires which loop on the hole of ω (where the acyclicity condition saves us from circular dependencies).

In the following the weight |D| of a set of wires D is the multiset of the weights of its wires. A terminal wire is dormant if it connects an active port or two free ones. Dormant wires are those that can become cuts when glued in a context.

Lemma 8 (modularity)

. Take λ and µ 1 , . . . , µ n with simple modules and ω[ ] a context such that ω[λ] and ω[µ i ] are all DiLL • pure proof nets. Suppose the following points are satisfied:

for every i we have that µ i can replace λ;

-i sp(µ i ) ≤ sp(λ); -if n = 0, then λ > [ ];
otherwise, for every i we have µ i + D i µ i < λ , (resp. ≤) where D i is the set of active wires in µ i that are not dormant in λ.

Then we have the pointwise inequality ω

i µ i < ω[λ] (resp. ≤).
→tech.app.

Proof (sketch). By induction on the depth of the hole in ω[

]. The base step is little more than the replacement lemma. The inductive step shows that the deepest box where the substitution happens satisfies all the hypotheses. Lemma 9. . has the following properties.

-if π e → π ′ then π ′ < π ; -if π mc → π ′ then π ′ ≤ π ; -if π ∼ π ′ then π ′ = π .
→tech.app.

Proof (sketch). Thanks to the modularity lemma, it suffices to consider each pair of redex and contractum, assign variables to their terminal wires as explained, and mechanically check the hypotheses of the lemma. For equivalences it is enough to check the same hypotheses replacing inequalities by equalities.

Theorem 10 (finite developments). Reduction on DiLL

• is SN. →tech.app.

Proof (sketch).

Only m and c remain to be settled. For all reductions, the pair given by π , # m (π)+# c (π) strictly decreases for lexicographic ordering, where # m just counts the multiplicative cells in π, and # c weights coweakenings, weakenings and boxes contining 0 in the following inductive way:

# c (π) := 1 + # ! 0 (π) + # ? 0 (π) + B∈b 0 (π) (1 + deg(B)) # c (σ(B))
where # ! 0 and # ? 0 count coweakenings and weakenings at depth 0, and the degree deg(B) is the number of ports of B. This accounts both for 0-boxes becoming (co)weakenings, and for weakenings pulls splitting boxes. # c by the way can be used to prove that c-reduction is strongly normalizing.

Proving Confluence

Recall that ∼ and c may be a-equivalence and n-reduction, or full asp-equivalence and nzp-reduction. Some of the diagrams show we cannot separate s-equivalence from the p one (and their associated reductions).

Proposition 11. Reduction on DiLL • is CR∼. →tech.app.

Proof (sketch). The proof relies on Lemma 1 and the strong normalization of DiLL • we proved in the previous section. One has therefore to prove local confluence modulo ∼ and local coherence with the generating relation -, by going through all the (numerous) critical pairs. As for multiplicative reductions, we can even be more specific, as m is strongly confluent and commutes with e (in particular

. Let π → σ iff π • mec * -→ ̺ in DiLL • and σ = ̺ • . Then - mec → ⊆ → ⊆ mec * -→, so that → * = mec * -→ (notice π • cannot block any reduction); -→ is strongly CR∼ because mec * -→ is so in DiLL • .
Then we conclude, as → is CR∼ by Lemma 3 (→ is reflexive), which means that → * = mec * -→ is strongly CR∼, which in turn by Lemma 2 gives Church-Rosser modulo ∼ for the ordinary reduction 12 . It is not hard to give parallel reductions for the ec and m ones and do the same.

Technical Appendix

Let us denote by λ µ the relation "λ can replace µ". In the following we will use measures on free ports: these must be intended as the measures (possibly variables) of the terminal wires above such ports. Also, just for the technical appendix, we here use the notation

ε := ε 2 ε := ε 0 .
Lemma 6. Given a DiLL • proof net π, ?(e), !(e) and sp(λ) are defined and unique for all e ∈ w ! (π) and all λ simple subnets of π at any depth. ←back

Proof. Uniqueness is clear. We prove that we can define all of the measures by a nested induction. Suppose we have defined them for all DiLL • proof nets of depth strictly less than d(π). Acyclicity ensures no looping dependencies can be established.

First we show that !(e) is defined for all w ! (π), and at the same time that ?(e) and sp(λ) are for e ∈ w k (π) and λ ∈ ℘ k (π) (simple subnets at depth k) with k ≥ 1. This is done by induction on the length of maximal ?-paths: starting with e for e ∈ w 0 (π), or with the wire f on the principal port of the box B ∈ b 0 (π) containing e or λ otherwise. In fact all measures inside boxes are already defined by induction hypothesis, but they depend on variables ?(p) and !(p) with p ∈ fp 1 (π). However by clash-freeness:

all the variables ?(p) upon which the measures depend must be on the ports over a principal port of a box, and we can instantiate them with 1; -all the variables !(p) are over auxiliary ports, and we can instantiate them with !( f ) with f ∈ w 0 (π), defined by secondary induction hypothesis, as these are wires further down ?-paths than the wire on the principal port.

In the other case, e ∈ w 0 (π), !(e) is defined from the !-weight on wires further down ?-paths, and possibly the spread of nets inside a box which have just been seen to be defined, all by secondary induction hypothesis. Next, ?(e) for e ∈ w 0 (π) can now be defined by induction on the maximal length of !-paths starting with e, as they depend: on !-weights; on weights ?( f ) with either f ∈ w 1 (π) or further down !-paths; and on sp(λ) with λ ∈ ℘ 1 (π).

Finally, taken any λ ∈ ℘ 0 (π), its spread depends on ! and ?-weights. ⊓ ⊔

Lemma 7 (replacement). Suppose λ can replace µ, ω[ ] is a linear context with ω[λ]

and ω[µ] proof nets. Then for each e wire in the context ω, ? ω[µ] (e) ≤ ? ω[λ] (e) and

! ω[µ] (e) ≤ ! ω[λ] (e). ←back
Proof. We reason by induction on the size of ω: if there is a cell c with a wire on the internal interface, detach it from ω obtaining a smaller context ω ′ . One must then check that glueing c to both simple nets obtaining λ ′ and µ ′ yields still µ ′ λ ′ . This really poses no problem because we are adding cells with a single wire attached to the hole for now, and all the measures are defined with monotonous operations. For example in

f ! σ f e
when we check the replacement condition on e we get (if

e i is a terminal !-wire) that ! µ ′ (e i ) = ! µ (e i ) (1 + !( f )) ν∈σ sp(ν) ?( f )
(where [x/y] denotes substitution as usual) and similarly for ?, which by the hypothesis µ λ is less than ! λ ′ . Then checking the ?-weight for f , we have

? µ ′ ( f i ) = (1 + !( f )) ν∈σ sp(ν)?( f ν ) ? µ ′ ( f ) which again is right as ? µ ′ ( f ) = ? µ ( f ) ≤ ? λ ( f ) = ? λ ′ .
The slightly harder part comes if ω has no cells on H ω , and we suppose that there is a wire e which connects H ω to itself. Supposing that glueing e to λ/µ yields an exponential wire (otherwise it is trivial), the situation can be depicted by the following picture.

d e f g
As e is not a clash, e and f cannot be terminal wires of the same kind (in the sense of !-wires and ?-wires). Wlog we can suppose e a ?-wire and f an !-one (if one of the two is not exponential it is trivial). There cannot be then any exponential path linking e and f in neither λ nor µ, as it would form an exponential loop with e. Therefore the variable !(e) (resp. ?( f )) does not appear in ! λ ( f ) and ! µ ( f ) (resp. ? λ (e) and ? µ (e)). We can therefore safely write

! µ ′ ( d ) = ! µ ( d ) ! µ (p)/!(q) ≤ ! λ ( d ) ! λ (p)/!(q) = ! λ ′ ( d ), ? µ ′ ( d ) = ? µ ( d ) ! µ (p)/!(q), ? µ (q)/?(p) ≤ ? λ ( d ) ! λ (p)/!(q), ? λ (q)/?(p) = ? λ ′ ( d ).
If in ω there are no cells nor wires on the hole, it means that ω[λ] is just a juxtaposition of λ and the net ω without the wiring on the hole. In any case it is done.

⊓ ⊔ Lemma 8 (modularity). Take λ and µ 1 , . . . , µ n with simple modules and ω[ ] a context such that ω[λ] and ω[µ i ] are all DiLL • pure proof nets. Suppose the following points are satisfied: ←back -for every i we have that µ i can replace λ;

-i sp(µ i ) ≤ sp(λ); -if n = 0, then λ > [ ];
otherwise, for every i we have µ i + D i µ i < λ , where D i is the set of active wires in µ i that are not dormant in λ.

Then we have the pointwise inequality

ω i µ i < ω[λ] .

Proof. Let us reason by induction on the depth of the hole in

ω[ ]. Let µ = i µ i . Base step. If ω[ ] = δ[ ] + π with δ[ ] linear, then it suffices to show the thesis for δ[ ]. If n = 0 then trivially δ[λ] ≥ λ > [ ] = 0 = δ[0] .
Suppose therefore n ≥ 1. By the replacement lemma we have that for every i, all the weights of wires in δ are less in δ

[µ i ] than in δ[λ], so δ δ[µ i ] ≤ δ δ[λ] .
If moreover C denotes the set of cuts of δ[λ] that are on the interface, and

C i the same for δ[µ i ], then clearly C i ⊆ C ∪ D i , and |C i \ D i | δ[µ i ] ≤ |C| δ[λ]
, as such wires are in δ and the replacement lemma applies. For the same reason when we instantiate the variables we get

µ i δ[µ i ] + |D i | δ[µ i ] < λ δ[λ]
. We thus have

ω[µ i ] = ω δ[µ i ] + |C i | δ[µ i ] + µ i ≤ ω δ[λ] + |C i \ D i | δ[µ i ] + |D i | δ[µ i ] + µ i < ω δ[λ] + |C| δ[λ] + λ δ[λ] = δ[λ] .
As for the spread, we have

i sp(δ[µ i ]) = sp δ[µ i ] (δ) i sp δ[µ i ] (µ i ) ≤ sp δ[λ] (δ) • sp δ[λ] (λ) = sp(δ[λ]).
So we conclude this step by

δ i µ i ] = i sp(δ[µ i ]) δ[µ i ] < i sp(δ[µ i ]) • δ[λ] ≤ sp(δ[λ]) λ = λ .
Clearly replacing ≤ for < is still valid.

Inductive step. Suppose now that ω has the hole at non-zero depth. Let B[ ] ∈ b ! (ω) be the box containing the hole at maximal depth, so that its contents is δ[ ] + π with δ[ ] linear, and let ψ[ ] be the context in

ω such that ω[ ] = ψ[B[ ]].
If n = 0 by inspecting the laws of the measures one easily sees that

B[π] B[δ[λ] + π], sp(B[π]) = 1 = sp(B[δ[λ] + π]) and
B[π] = #(B) π < #(B)( δ[λ] + π ) = B[δ[λ] + π] ,
so we can apply inductive hypothesis and get the result.

If n ≥ 1, applying the replacement lemma we get that the measures in δ[µ i ] are pointwise lower than the ones in δ[λ], and we can instantiate them with the variables of B[ ] (and 1 for the one above the principal port). The measures in π are clearly oblivious of the changes.

Let ̺ = B[ i δ[µ i ] + π], σ = B[δ[λ] + π],
and

B[ ] = ! p r k r 1 q k q 1
We have

! ̺ (p) = (1 + j !(q j )) i sp ̺ (δ[µ i ]) + ν∈π sp(ν) = (1 + j !(q j )) sp ̺ (δ) i sp ̺ (µ i ) + ν∈π sp(ν) ≤ (1 + j !(q j )) sp σ (δ) i sp σ (λ) + ν∈π sp(ν) = ! σ (p), ? ̺ (q h ) = ?(p)(1 + j !(q j )) i sp ̺ (δ[µ i ])? ̺ (r h ) + ν∈π sp(ν) ≤ ?(p)(1 + j !(q j )) sp σ (δ) i sp ̺ (µ i ) ? σ (r h ) + ν∈π sp(ν) ≤ (1 + j !(q j )) sp σ (δ) sp σ (λ)? σ (r h ) + ν∈π sp(ν) = ? σ (q h ),
so that ̺ σ. We can see here how the sum weighted with the spread value makes sure that the measures do not grow if the number of addends inside the box grows. As for the rest of the hypotheses, sp(̺) = 1 = sp(σ), there are no new dormant wires and in fact

̺ = #(B) i δ[µ i ] + π < #(B) δ[λ] + π = σ ,
using the base step. The box count depends solely on the variables outside the box. We can now apply inductive hypothesis, and get that

ω i µ i = ψ[̺] < ψ[σ] = ω[λ] .
Again replacing < with ≤ poses no problems.

⊓ ⊔ Lemma 9. . has the following properties.

-if π e → π ′ then π ′ < π ; -if π mc → π ′ then π ′ ≤ π ; -if π ∼ π ′ then π ′ = π . ←back
Proof. We here report some of the cases. The full list can be consulted in http: //www.pps.jussieu.fr/~ptranqui/content/docs/phd.pdf.

Codereliction against box.

λ := d ! i ν i ! p q r e → i d d ν j ! ! ν i ! ! j ν j ! ? ? p q r =: i µ i
No new dormant wires. We may suppose i ν i 0, as otherwise it is trivial. In µ i both the ν i outside the box and the ν j s inside get the same measures. If B is the box, then

# λ (B) = ?(p)(2 + h !(q h )) = ?(p) + # µ (B) ≥ 1 + # µ (B).
Replacement hypothesis:

! µ i (p) = 1 + (1 + h !(q h )) j sp(ν j ) ≤ (2 + h !(q h )) j sp(ν j ) = ! λ (p), ? µ i (q h ) = ? µ i (q ν i h ) + # µ i (B) j sp(ν j )? µ (q ν j h ) ≤ j sp(ν j )? λ (q ν j h ) + # µ i (B) j sp(ν j )? λ (q ν j h ) ≤ # λ (B) j sp(ν j )? λ (q ν j h ) = ? λ (q h ), ? µ (r) = 1 = ? λ (r). Spread hypothesis: i sp(µ i ) = i ?(p) sp(ν i )? µ i (d) = ?(p) i sp(ν i )? λ (d ν i ) ≤ ?(p)(1 + h !(q h )) i sp(ν i )? λ (d ν i ) = ? λ (d) = sp(λ). Weight hypothesis: |d| µ i = ? µ i (d) + 1 = ? λ (d ν i ) + 1 < ? λ (d) + 1 = |d| , |d ν j | µ i = ? µ i (d ν j ) + 1 = ? λ (d ν j ) + 1 < |d| , µ i ≤ ν i + [ |d| µ ] + # µ (B) j sp(ν j )([ |d ν j | ] + |ν j |) ≤ [ |d| µ ] + # µ (B) j sp(ν j )[ |d ν j | ] + (1 + # µ (B)) j sp(ν j )|ν j | < [ |d| λ ] + # λ (B) j ν j = λ .
Box against box.

λ := d ! i ν i ! σ p q r e → d ν i ! ν i ! σ i ν ′ i p q r =: µ
No new dormant wires. All measures inside both boxes are constant during this reduction. We suppose i ν i 0, or else the step is trivial. Let ν ′ i be the addend inside the second box in µ, corresponding to ν i . If B is the box with the ν i s inside in both nets then

# λ (B) = ?(p)(1 + ! λ (d) + k (r k )) = ?(p)(1 + (1 + h !( f h )) sp(σ) + k !(r k )) > ?(p)(1 + h !( f h ) + k !(r k )) = # µ (B),
where sp(σ) = 1 if σ = 0, and the sum of its spreads otherwise. Replacement:

? µ (q j ) = # µ (B) i sp(ν ′ i )? µ (q ν ′ i ) = # µ (B) i sp(ν i )? µ (d ν i )(1 + h !(q h )) κ∈σ ? µ (q κ ) < # λ (B) i sp(ν i )? λ (d ν i ) (1 + h !(q h )) κ∈σ ? λ (q κ ) = ? λ (d)(1 + h !(q h )) κ∈σ ? λ (q κ ) = ? λ (q j ), ? µ (r j ) = # µ (B) i sp(ν ′ i )? µ (r ν ′ i ) < # λ (B) i sp(ν i )? λ (r ν i ) = ? λ (r j ). Spread: sp(µ) = 1 = sp(λ). Weight: |d ν i | µ = ? µ (d ν i ) + ! µ (d ν i ) < # λ (B) i sp(µ i )? λ (d ν i ) + ! λ (d) = |d| λ , µ ≤ # µ (B) i sp(ν ′ i ) ν i + |d ν i | µ + ? µ (d ν i )(1 + h !(q h )) σ < # λ (B) i sp(ν i ) [ ν i ] + # λ (B) i sp(ν i ) ν i + # λ (B) i sp(ν i )? λ (d ν i ) (1 + h !(q h )) σ < |d| λ + # λ (B) i ν i + ? λ (d)(1 + h !(q h )) σ = λ .

Contraction against cocontraction

λ := d ? ! p 2 p 1 q 1 q 2 e → e 1 f 1 e 2 f 2 ! ? ! ? p 1 p 2 q 1 q 2 =: µ
The new dormant wires are all e 1 , e 2 , f 1 and f 2 . Replacement: ! µ (p i ) = !(q 1 ) + !(q 2 ) = ! λ (p i ), ? µ (q i ) = ?(p 1 ) + ?(p 2 ) = ? λ (q i ). Spread: sp(µ) = 1 = sp(λ). Weight: |e i | µ = !(p i )(?(q 1 ) + ?(q 2 )) < (!(p 1 ) + !(p 2 ))(?(q 1 ) + ?(q 2 )) = |d| λ , f i µ = ?(q i )(!(p 1 ) + !(p 2 )) < (?(q 1 ) + ?(q 2 ))(!(p 1 )

+ !(p 2 )) = |d| λ , µ + |e 1 | , |e 2 | , f 1 , f 2 < [ ] + |d| λ = λ .
Push conversion.

λ := ! i ν i ? d e p q r p ∼ ! i ν i ? d ν i e ν i p q r =: µ
Here we have only to check for ?(r), as the rest is trivial.

? µ (r) = # µ (B) i sp(ν i )(? µ (d ν i ) + ? µ (e ν i )) = # λ (B) i sp(ν i )? λ (d ν i ) + # λ (B) i sp(ν i )? λ (e ν i ) = ? λ (r).
Bang sum conversion.

λ := ! i ν i + j κ j p q s ∼ ! ! i ν i ! j κ j ? ? p q =: µ
The conversion does not create new dormant wires. Moreover if B is the box on the left, then # λ (B) is the count also of both boxes on the right. Also the contents of the boxes, which we denote by B ′ and B ′′ , get the same measures. Recall that such contents are required to be non zero. Replacement: ? µ (q h ) = # µ (B) i sp(ν i )?(e µ (q ν i h ) + j sp(κ j )?(e µ (q

κ j h ) = ? λ (q h ), ! µ (p) = (1 + h !(q h )) i sp(ν i ) + j sp(κ j ) = ! λ (p), Spread: sp(µ) = 1 = sp(λ); Weight: µ = # µ (B ′ ) i ν i + # µ (B ′′ ) j κ j = # λ (B)( i ν i + j κ j ) = λ ⊓ ⊔
Theorem 10 (finite developments). Reduction on DiLL • is SN. ←back

Proof. Only m and c remain to be settled. For all reductions, the pair given by π , # m (π) + # c (π) strictly decreases, where # m just counts the multiplicative cells in π, and # c weights coweakenings, weakenings and boxes contining 0 in the following inductive way:

# c (π) := 1 + # ! (π) + # ? 0 (π) + B∈b 0 (π) (1 + deg(B)) # c (σ(B))
where # ! 0 and # ? 0 count coweakenings and weakenings at depth 0, deg(B) is the number of ports of B.

-if π e → π ′ the first component strictly decreases; -if π m → π ′ then π ′ = π , # m (π ′ ) < # m (π) and # c (π) = # c (π ′ ); -if π n → π ′ then a (co)weakening disappears, so # c (π ′ ) < # c (π)
, and the rest is unchanged; -if π p → π ′ let B the box for which is happening, and B ′ and B ′′ the two corresponding boxes in π ′ . First note that apart the weakenings, all other cells are preserved, possibly splitted between the boxes. Let k ≥ 1 be the number of addends in B ′ (i.e. the number of pulled weakenings). Then

deg(B) # c (σ(B)) = (1 + deg(B)) k -1 + # c (σ(B ′ )) + # c (σ(B ′′ )) ≥ (1 + deg(B)) # c (σ(B ′ )) + (1 + deg(B)) # c (σ(B ′′ )) > (1 + deg(B ′ )) # c (σ(B ′ )) + (1 + deg(B ′′ )) # c (σ(B ′′ )),
where the -1 at the beginning is due to counting two times the as the other addend reduces to 0. Notice that we must use the neutral reduction of weakening. Codereliction on box on contraction: Figure 9 shows this confluence diagram.

Here we need both the neutral rule of coweakening and associativity of contraction.

⊓ ⊔

Following is a less formal description of the remaining cases (which are all accounted for).

-Box on box on dereliction, weakening or contraction, or two boxes on a third: these are in LL and therefore are known. The one with dereliction just needs to take into account the sums that may have arisen. One just takes uses the Σe → version of the steps taken in LL. As for the coherence diagram, Figure 10 shows an example of a typical coherence diagram, serving both sides of a conversion against a certain reduction. Another list of sketched descriptions follows. The last point shows the necessity of the particular shape of neutral reduction.

-All critical pairs with associativity: trees of contractions and cocontractions are known to behave like generalized n-ary (co)contractions. In particular when dealing with a tree of two nested (co)contraction, it suffices to complete the reduction on both to join the peak. Neutrality on associativity is trivial. -Box, coweakening or cocontraction on a s conversion: on one side they enter the box getting additively duplicated inside, while on the other they are duplicated by a contraction before entering. In any case another s conversion closes -Dereliction on a s conversion: on one side the net is additively split by opening the box, on the other the net is split first by the dereliction on cocontraction rule, then depending on the box chosen the other gets deleted, and finally closing with n-reductions we obtain the same net. -Contraction or weakening on a s conversion: both traverse the two sides doing the same operations, on one side by being duplicated by the leading cocontraction. s-convertible box on another box: both sides may enter the box, safe for the trailing contractions, which must be settled by a push conversion. -Codereliction on a s conversion: on one side, the net splits additively on the box contents on the box, with the linear copy being a single net taken from inside. On the other one, the choice of which addend of the box to extract is done at the contraction, while the other gets a coweakening exactly as with codereliction on box reduction. In any case we join in the end by s-converting the remaining boxes. -Reduction to zero taking an addend of the conversion: on the side where the box is split, we z-reduce the box and by n-reductions we get exactly to the other side. -Pull reduction on s-conversion: the pull is designed to integrate a sort of s-conversion step, so that it may be always performed on two sides of a conversion. n-conversion does the rest. -Box, coweakening or cocontraction on a p conversion: the cell gets duplicated and enters the box on both sides, but in opposite order. -Dereliction on a p conversion: the reductions on the two sides are equal.

-Contraction or weakening on a p conversion: the way in which contractions are stacked may change, but a-conversion (and n-reduction) ensures joinability. p-convertible box on another box: apart from having to exit/enter two boxes on one side, the two are the same. -Codereliction on a p conversion: additive splitting and box opening happen on both sides, but in different order. -Reduction to zero of the p-converted box: by c-normalization we get just weakenings and coweakenings on both sides. -Pull reduction on p-conversion, on different auxiliary ports: we can pconvert all boxes involved, we just have to reorganize the stack of contractions by a-conversion.

-Pull reduction on p-conversion, with the weakening on an auxiliary port interested by the conversion: pull and neutral reductions join the two sides. -Neutral reduction on p-conversion: n-reduction can block the conversion on one side by destroying the contraction of an addend. This is joined by a p-reduction and then by a full asp conversion. This is exaclty the point where the particular shape of the p-reduction is needed. ⊓ ⊔

Fig. 3 :

 3 Fig. 3: Top: the rules for associative equivalence a ∼, the push one p ∼ and the bang sum one s ∼; -denotes a one-step conversion. Bottom: the rules for neutral reduction n →, the pull one p → and the bang zero one z →. The condition π, σ 0 applies to all rules.

Fig. 4 :

 4 Fig. 4: Reduction of a box with two coderelictions on it. Starting with codereliction b swaps the two linear copies of !π and therefore both the cocontraction and contraction trees in the last addend.

Fig. 5 :

 5 Fig.5: Issues with confluence. Figure5(a) shows the need for correctness. The example shown is even simply typed. Figure5(b) shows how in the pure case even the exponential reduction alone is not terminating.

  ) is an example of DiLL • net enjoying (π • ) • = π. On the other hand, if σ is the net in Figure5(b), then σ • = σ and it is strongly normalizing to the net in Figure6(b).

  A DiLL • net π where marks are compulsory, such that (π • ) • = π.

  The normal form in DiLL • of the non-terminating net of Figure 5(b).

Fig. 6 :Fig. 7 :

 67 Fig. 6: Examples for DiLL • .

  λ∈π sp(λ)?(e λ ) otherwise; otherwise: ?(e) = 1.e p f : !(e) = !( f ) if p ∈ fp 0 (σ(B)) for a box B, p is above an auxiliary port, and f is the wire corresponding to p outside the box, e) = !(e 1 ) + !(e 2 );

Figure 4

 4 has already shown one of the most interesting cases for local confluence, two coderelictions on a box. The other critical pairs for both confluence and coherence can be joined by a long exercise in reductions.We can finally arrive to the main theorem of the work.Main Theorem. Reduction on DiLL pure proof nets is CR∼, and so are m and ec taken alone.Proof. Using DiLL • we define a parallel reduction →

Fig. 8 :Fig. 9 :

 89 Fig. 8: Confluence diagram of codereliction on box on dereliction.

Fig. 10 :

 10 Fig. 10: Coherence diagram between the bang sum equivalence and a codereliction.

  DiLL k+1 ( i λ i polynet of DiLL k )

	⊗ *	` *			? ?	! !	? 2 ?	? 0 ?
	tensor	par			dereliction	contraction	weakening
						(commutative)
	1 *	⊥ *			! !	? ?	! 2 !	! 0 !
	one	bottom		codereliction	cocontraction	coweakening
						(commutative)
	? ?	i λ i	!	!	box of

  in absence of switching acyclicity.

	?	? 2	!	? 2	?	?	? 2	!	? ! ? 2	?	?	? 2	! ? 2	?

e → e →

  1 added by default to # c . The rest is unchanged. ′ then let B be the reduced box: and deg(B) (co)weakenings are created, but the deleted box weighted 1 + deg(B).if π ∼ π ′ then all multiplicative, weakening and coweakening cells are in both polynets, in boxes with the same degree, so also that also the second component is invariant.

	-if π
	Codereliction on box on dereliction: the confluence diagram is shown in Fig-
	ure 8. We use the fact that
	!	!	?	e * → ?

z → π ⊓ ⊔ Proposition 11. Reduction on DiLL • is CR∼. ←back Proof.

We here a couple of more cases for local confluence.

To be precise, the stronger result of being Church-Rosser modulo (see Section 1.1).

Actually the subject of a future submission by the author and Pagani.

Here like in the rest of the paper, := means "defined as".

This also mean there is never the need to perform conversion steps in order to ready some cuts, i.e. make them visible.

Technically, one prohibits the repetition of unoriented wires and that three ports of the same cell be crossed by the path.

All of this can be defined more formally by an inductive definition. Nevertheless we leave it to the reader as an easy exercise.

For the quite delicate technical details the reader is referred to[START_REF] Vaux | λ-calcul différentiel et logique classique : interactions calculatoires[END_REF].

Composition of contexts should be defined, but it is trivial once plain plugging is defined.

The name may be misleading, as an equivalence is not directed. It comes from[START_REF] Di Cosmo | Strong normalization of explicit substitutions via cut elimination in proof nets[END_REF] and[START_REF] Tranquilli | Intuitionistic differential nets and lambda calculus[END_REF] where it was treated as a reduction, and we felt like keeping it because of the good name pairing with the pull reduction.

More intuitively: !-wires and ?-wires are those that in a typing attempt would get an outermost ! or ? respectively, while clashes would give a failure to unify an outermost exponential modality.

Multisets over a well founded set, presented as [a 1 , . . . , a k ] and additive notation, have the well founded order given by the transitive closure of A + [a] > A + B with ∀b ∈ B : b < a.

Notice that we cannot infer CR∼ of → directly from the same property in DiLL • , as chained parallel reductions are not necessarily in DiLL •