has to occur

Long Title]Exponentials as Substitutions, and the Cost of Cut Elimination in Linear Logic
B. Accattoli]Beniamino Accattoli

Inria & LIX, École Polytechnique, France

This paper introduces the exponential substitution calculus (ESC), a new presentation of cut elimination for IMELL, based on proof terms and building on the idea that exponentials can be seen as explicit substitutions. The idea in itself is not new, but here it is pushed to a new level, inspired by Accattoli and Kesner's linear substitution calculus (LSC).

One of the key properties of the LSC is that it naturally models the sub-term property of abstract machines, which is the key ingredient for the study of reasonable time cost models for the $\lambda$-calculus. The new ESC is then used to design a cut elimination strategy with the sub-term property, providing the first polynomial  cost model for cut elimination with unconstrained exponentials.

For the ESC, we also prove untyped confluence and typed strong normalization, showing that it is an alternative to proof nets for an advanced study of cut elimination.

§ INTRODUCTION

Two key aspects of linear logic are  its  resource-awareness and that it  models the evaluation of $\l$-terms via cut elimination, even of untyped $\l$-terms, if recursive formulas are allowed. One would then expect that, given a $\l$-term $\tm$ represented as a linear proof $\pi_{\tm}$, the length of cut elimination in $\pi_{\tm}$ could provide estimates about the time complexity of $\tm$. Surprisingly, this is not (yet) the case.

Linear Logic and Complexity Classes Linear logic is often used in implicit computational complexity, a field that aims at characterizing complexity classes with no explicit references to machine models. In this line of work, classes are characterized by seeing program execution as cut elimination in fragments of, and variations on, linear logic, usually obtained by constraining the exponential connectives in some way. Some representative papers are <cit.>.

A first limitation of these results is that the bound is given on whole fragments of linear logic, without saying how to compute the cost of a fixed proof, which might be much lower than the bound for the fragment. A second limitation is that, as soon as one steps out of the fragment that characterizes the class, nothing is known.

The Cut Elimination Clock The underlying problem is that there are no known complexity measures for cut elimination in linear logic. The use of linear logic for implicit complexity is so implicit that, not only it avoids machine models, it also never states what is the underlying logical unit for time, that is, what are the ticks of the cut elimination clock.

Formally, what is missing is a polynomial time cost model for cut elimination. That is, a cut elimination strategy of which the number of steps is a bound, up to a polynomial overhead, to the time complexity of implementing cut elimination according to that strategy. But be careful, it is not the number of steps that has to be polynomial: it would not be possible, linear logic cut elimination can take way more than polynomially many steps (in the size of the initial proof). It is the cost of implementing the sequence of steps (on a random access machine, or on another reasonable framework) that must be polynomial—ideally linear—in their number (which can be whatever) and in the size of the proof.
In this way, the number of steps taken by the strategy on a proof $\pi$ provides a reliable measure for the time cost of $\pi$. Roughly, the steps of such a strategy become the ticks of a cut elimination clock.

One might wonder why not any strategy would do. The point is that cut elimination strategies often suffer of size explosion: one can build families of proofs $\{\pi_n\}_{n\in\nat}$ on which the strategy iterates duplications in malicious ways, leading to a growth of the proof size which is exponential in the number $k$ of cut elimination steps. Therefore, $k$ cannot be taken as the time cost for implementing the cut elimination sequence (not even up to a polynomial), if the sequence has to be implemented as it is. Intuitively, taking such strategies as clocks would correspond to having irregular ticks of non-uniform length, some of which take a very long time. In sub-term-size-explosion, we shall show that cut elimination by levels,  the  strategy of reference in linear logic (especially for implicit computational complexity), suffers from size explosion.

The aim of this paper is to provide a clock of which the ticks are regular enough to serve as a reliable time measure for unconstrained exponentials. That is, we shall provide a new strategy of which the number of steps is a polynomial time cost model. In our pursuit, we are inspired by developments in the study of cost models for the $\l$-calculus and in the modern theory of $\l$-calculi with explicit substitutions.

The Linear Substitution Calculus In the last decade, the study of reasonable time cost models, that is, of polynomial cost models that additionally are equivalent to the time cost model of Turing machines, has advanced considerably in the sister field of $\l$-calculus, starting with Accattoli and Dal Lago's result about the number of steps of the leftmost strategy <cit.>. The advances have been enabled and developed over Accattoli and Kesner's linear substitution calculus (shortened to LSC)  <cit.>, which is a neat and compact refinement of the $\l$-calculus that  probably can be considered the answer to the quest for the canonical $\l$-calculus with explicit substitutions (shortened to ES). The LSC refines ES with ideas from both proof nets, namely using contextual rewriting rules on terms—also called  at a distance—to avoid commuting constructors (taken from Accattoli and Kesner  <cit.>), and the $\pi$-calculus/bigraphs, in modeling duplication as replication in $\pi$ (following Milner <cit.>).

The Sub-Term Property The relevance of the LSC for cost models is due to its natural modeling of strategies having the sub-term property often found in abstract machines:

All sub-terms duplicated  or erased along an evaluation sequence from $\tm$ are sub-terms of $\tm$.

When a strategy $\Rew{\symfont{st}}$ has the sub-term property, the cost of implementing a sequence $\tm \Rew{\symfont{st}}^{k} \tmtwo$  is polynomial, and in general linear, in $k$ and in the size $\size\tm$ of $\tm$. Therefore, the sub-term property implies that the number of steps is a polynomial cost model for time. Intuitively, it states that the steps of the strategy are the regular ticks of a reliable clock. It represents, for the study of cost models, what the sub-formula property is for proof-search, or the cut-elimination theorem for sequent calculi.

Typically, important strategies of the $\l$-calculus such as weak head, head, or leftmost-outermost reduction do not have the sub-term property (actually, we show in sub-term-size-explosion that no strategy in the $\l$-calculus has the property), while their analogous in the LSC does.  One of the key points is that the sub-term property requires micro-steps evaluation, that is, performing one variable replacement at a time (as in the LSC), rather than small-step evaluation, that is, using rules resting on meta-level substitution such as $\beta$. The sub-term property and the related degeneracy of size explosion are discussed in detail in sub-term-size-explosion.

Linear Logic and the Sub-Term Property In linear logic, the problem is not just that there are no known cut elimination strategies providing polynomial cost models. What is worse, is that there are no known micro-step strategies with the sub-term property (as we discuss below), despite the clear linear logical flavor of the property. Therefore, the study of cost models is, at present, simply out of reach.

How can one recover the sub-term property in linear logic? This is the challenge addressed by this paper. There are two natural possible routes. One is working inside linear logic as it is usually presented, and try to recover the sub-term property. This would inevitably mean working with proof nets, as cut elimination in the sequent calculus requires to deal with too many commutative cases.
Another one is to develop an alternative, commutation-free presentation of linear logic akin to the LSC, and use it to design a strategy with the sub-term property. We choose the second option, for three reasons.

* Terms are more easily manageable: graphical syntaxes are too hard to manage for the long and delicate proofs typical of the study of cost models.

* Better rewriting: the rewriting theory of the LSC is better behaved than the one of proof nets.

* Novelty: we aim at a fresh look at linear logic, importing ideas from a sister field.

This Paper We provide three main contributions:

* Design: we introduce the exponential substitution calculus (ESC), which is a new presentation of linear logic cut elimination based over the theory of ES and the LSC and free from commutative cases. It is a design study, done in a principled way. It is also a stress test, as linear logic has many more constructors and rewriting rules than the LSC. We shall see that, in order to guarantee some expected properties of ES, one is forced to turn to intuitionistic linear logic.

* Sub-term strategy: we define a new cut elimination strategy for the ESC and prove that it has the sub-term property. Therefore, we solve the issue mentioned at the beginning of the paper, providing the first polynomial time cost model for unconstrained exponentials.

* Foundations: we prove various key properties of the ESC, among which untyped confluence and typed strong normalization, thus providing solid foundations for our presentation. The non-trivial proofs of these properties are developed from scratch, using elegant proof techniques developed for the LSC.

The next section provides overviews of these contributions.

Related Work To our knowledge, there are no works in the literature studying cost models for linear logic. Many term and process calculi for or related to linear logic have been proposed, for instance <cit.>. There are also proposals for $\l$-calculi with ES with linear features such as  <cit.>. None of these calculi employs rewriting rules at a distance as we do here. Mazza uses a natural deduction linear calculus at a distance <cit.>, and Kesner develops a $\l$-calculus with ES reflecting proof nets cut elimination <cit.> but only for the fragment representing the $\l$-calculus. Various authors consider terms for proof structures <cit.> which then need correctness criteria, not required here.

The sub-term property is a folklore property first called as such by Accattoli and Dal Lago  <cit.>, who also show a surprising link with the standardization theorem in <cit.>.

Journal Version and Proofs This journal version extends the conference one adding  explanations, in particular sub-term-size-explosion is new, and most proofs together with the intermediary lemmas that were omitted from the conference version. A few proofs are particularly long and tedious so they are still omitted or partially omitted, but can be found on Arvix in the technical report <cit.> associated to the conference paper, which is accessible as version one ("v1", see the bibliography entry for the link) of the present paper on Arxiv (which is instead "v2").

§ OVERVIEW OF THE CONTRIBUTIONS

§.§ Contribution 1: The Exponential Substitution Calculus

By allowing duplication and erasure of
sub-proofs, the exponentials can be seen as a substitution device: it is the core of the simulation of the $\l$-calculus into linear logic due to Girard <cit.>.
Historically, ES became popular with a calculus by Abadi et al. <cit.>, later shown defective at the rewriting level by <cit.>. Linear logic and the exponentials were thus considered as a more solid formalism to borrow from. Di Cosmo and Kesner were the first ones to do so <cit.>, seeing ES as exponential cuts.

Along the years, however, the theory of ES made progresses of its own, and here   we reverse the transfer. The idea is enforcing and pushing to the extreme the slogan:

Exponentials = Explicit Substitutions

To continue, we need to recall the very basics of ES.

Basics of Explicit Substitutions The idea is to extend the $\l$-calculus with a new term constructor $\tm\esub\var\tmtwo$
(which is just a compact notation for $\letin\var\tmtwo\tm$, but with no fixed order of evaluation between $\tmtwo$ and $\tm$) denoting a delayed or explicit substitution, and decomposing the $\beta$-rule:

$(\la\var\tm)\tmtwo \tob \tm\isub\var\tmtwo$

where $\tm\isub\var\tmtwo$ is meta-level substitution, into two rules:

$(\la\var\tm)\tmtwo \Rew{\symfont{B}} \tm\esub\var\tmtwo \tos \tm\isub\var\tmtwo$

Now,  rule $\tos$ is further decomposed into various micro-step rules. There are many possible sets of such substitution rules. What they all have in common, even the defective ones mentioned above, is that, when considered separately from rule $\Rew{\symfont{B}}$, they are strongly normalizing even without types.

Design Principles Our exponentials as substitutions design of the ESC is based on the following principles.

Principle 1: proofs as typing derivations. Calculi with ES are studied as untyped calculi. Then we want the ESC to be an untyped calculus with good properties by itself, and see proofs of linear logic as typing derivations for it.

Principle 2: ES terminates/intuitionism. As we recalled above, the rules that manage ES are always strongly normalizing without types. It is possible to define also untyped linear logic proofs, as done in de Carvalho et al. <cit.>, obtaining a notion of untyped proof net. In the case of classical linear logic à la Girard (with involutive negation), the exponentials of such proof nets can diverge by themselves, as in classical-diverging (left). In such a setting, then, exponentials are not as ES. We then switch to intuitionistic linear logic, and prove that therein untyped exponentials are strongly normalizing (local-termination, p. thm:local-termination). To our knowledge, this is a new result and the first time that such a discrepancy between the classical and intuitionistic case is pointed out. The proof of the theorem requires long calculuations but it is otherwise simple. Termination is obtained via a measure defined by induction over terms. Essentially, the result states that in the intuitionistic setting exponentials are as ES. It is one of the main contributions of the paper.

Principle 3: micro and small steps together. The sub-term property requires a micro-step operational semantics. But studying micro-step ES constantly requires to refer to meta-level substitution, which is small-step. For linear logic, Girard originally considered micro-step cut elimination <cit.>, but soon afterwards Regnier introduced a small-step variant, to study the $\l$-calculus <cit.>, and both are frequently used in the literature. In the ESC, we want small and micro steps to co-exist, so as to provide a comprehensive framework.

Left Splitting The design of the ESC systematically exploits a simple fact about IMELL proofs: they can be seen as ending on a sequence of left rules following a right rule or an axiom. Representing a proof as a term $\tm$, one can thus uniquely split it as $\tm = \lctxp\val$, that is, a sub-proof ending on a right rule or an axiom, what we shall call a value $\val$, and a possibly empty sequence of left rules $\lctx$ from the last sequent of $\val$ to the last sequent of $\tm$. Such a left splitting is a basic property of sequent proofs that is not related to polarity or focussing—it is in fact simpler—and yet plays a crucial role in our rewriting rules at a distance for IMELL.

Additives We do not consider the additive connectives, and so we deal with IMELL. The reason is that they are both trivial and challenging, depending on the approach. If one adopts slices <cit.>, then our results lift smoothly. Without slices, instead, it is unclear how to combine additives and LSC-style micro steps while retaining all the properties.

Syntactical Variants A number of alternative syntaxes could have been adopted, typically Curien & Herbelin $\lambdamutcalc$ calculi <cit.>, Benton's linear-non-linear approach <cit.>, Pfenning & Caires' processes <cit.>, and, of course, proof nets or natural deduction. We prefer avoiding them to show that their additional ingredients (the distinguished conclusion on the left of sequents <cit.>, the linear-non-linear separation <cit.>, and the graphical syntax) are not required for studying cost models for linear logic, while we avoided processes because their evaluation does not compute cut-free proofs, since they do not evaluate under prefixes. Finally, we prefer the sequent calculus to natural deduction because it is more commonly used for presenting linear logic, and because in this way we provide a novel use of the LSC technology, given that the LSC is based on natural deduction. Our study can however be adapted to any of these settings.

§.§ Contribution 2: the Sub-Term Strategy

The proof nets strategy of reference is the notion of least level (or by levels) strategy $\Rew{ll}$ (introduced—we believe—by Girard <cit.> and studied for instance by de Carvalho et al. <cit.>), which reduces cuts of minimal level, defined as the number of $\bang$-boxes surrounding a cut. Unfortunately, $\Rew{ll}$ is not a good candidate for a linear logic clock. Consider the following diagram made out of micro steps at level $0$, which is an important sub-strategy $\Rew{l_0}$ of $\Rew{ll}$:

The right-down path shows that $\Rew{l_0}$, and thus $\Rew{ll}$, lacks the sub-term property, as the duplicated box  is not a sub-proof of the initial one. Moreover, iterating such a pattern gives size explosion for $\Rew{l_0}$, as shall we show in sub-term-size-explosion. The down-left path has the sub-term property but it shows that different $\Rew{l_0}$ paths can have different lengths—that is, $\Rew{l_0}$ is not diamond—forbidding to take its number of steps as a measure, because the number of its steps to normal form is an ambiguously defined quantity.

The Linear Head Strategy There actually is a micro-step strategy in the linear logic literature which is both diamond and with the sub-term property. It is Mascari & Pedicini's and Danos & Regnier's linear head strategy $\tolh$ <cit.> (which is a sub-strategy of level 0 cut elimination) but it is defined only on the fragment representing the $\l$-calculus and it does not compute cut-free proofs.

The linear head strategy is naturally modeled by the LSC, used by Accattoli and co-authors for proving properties of $\tolh$, design variants and extensions <cit.>, as well as to prove that it provides a reasonable time cost model <cit.>.

The Good Strategy The ESC strategy introduced here is simply called the good strategy $\tog$, because it avoids bad steps breaking the sub-term property. It is the generalization of the linear head strategy to the whole of IMELL and extended as to compute cut-free proofs.
The good strategy is micro-step, diamond, and it has the sub-term property, and thus provides the first polynomial cost model for IMELL[Is it a reasonable cost model? Roughly, yes. For time reasonability, the subtle part is polynomiality of the cost model, that is, the polynomial simulation of the ESC on Turing machines/RAM. The complementary part—here missing—is simulating Turing machines in the untyped ESC within polynomial overhead. It is true, but for very minor reasons it does not follow from results in the literature and it has to be (tediously) reproved from scratch. Moreover, the missing part is not relevant/cannot hold for the typed ESC, as IMELL is not Turing-complete (IMELL cut-elimination being strongly normalizing, it cannot model diverging computations).]. Its design is based on the creation of cuts, a notion due to the intuitionistic arrow $\lolli$ and invisible in classical linear logic.

§.§ Overview of Contribution 3: Foundations

We provide a foundational study of the ESC, ensuring that the new cut elimination rules are well behaved, but also to promote it as an alternative to the use of proof nets for IMELL. We prove three important properties:

* Untyped confluence: the untyped case is possibly divergent and thus more difficult than the typed case, as one cannot exploit termination in the proof technique. We prove confluence using the Hindley-Rosen method, and exploit termination nonetheless by building on the strong normalization of the exponentials, following an approach pushed forward by Accattoli in the study of the LSC <cit.>.

* Untyped PSN: preservation of untyped strong normalization (shortened to PSN) is a property typical of calculi with ES, stating that if a term is SN for the small-step rules (in the untyped setting where terms can also be divergent) then it is SN for the micro-step rules. Essentially, it states that the decomposition of  small steps in micro steps does not introduce degeneracies. The proof is based on a technique due to Kesner <cit.>. This theorem is notoriously technical for $\l$-calculi with ES. We adapt a simple proof by Accattoli and Kesner <cit.>, where the simplicity is enabled by adopting rules at a distance. Our adaptation is even simpler than the proof in <cit.>.

* Typed SN: we prove strong normalization (SN) of the small-step rules in the typed case, using the reducibility method. This theorem too is notoriously technical to prove for fragments of linear logic including the exponentials. We here provide what is probably the simplest and cleanest proof of SN in the literature, improving the already simplified approach of Accattoli <cit.> based on rules at a distance. We then use PSN to transport SN to micro steps.

Confluence and strong normalization are not usually studied for sequent calculi with traditional  cut elimination, that is, with both principal and commutative cases, because of the following two facts:

* No SN: cut elimination is not SN, because cut commutes with itself, leading to non-termination:

* No confluence: cut elimination is not confluent, not even in IMLL (!), because commutations affect the result, as shown by this counter-example, courtesy of Olivier Laurent:

Retrieving confluence and SN requires cut elimination modulo commutations, or via proof nets, or adding some rigidity to proofs such as focalization. In stark contrast, the cut elimination at a distance of the ESC, being free from commutations, achieves them without rewriting modulo nor modifying the deductive system.

Our study thus lies a new foundation for the study of cut elimination. It also sums up ten years of research on the rewriting of the LSC, at the same time generalizing the developed techniques to the considerably more general setting of IMELL.

§ SUB-TERM PROPERTY AND SIZE EXPLOSION

The sub-term property is used in many works on abstract machines, or the LSC, or reasonable cost models for the $\l$-calculus. Here we aim at providing evidence of its relevance. We first discuss it in the $\l$-calculus and then see an example of size explosion in proof nets.

We give  a new and more accurate definition of the property than the one in the introduction. We actually define two properties, a structural one and a quantitative one.

[Sub-term property]
A rewriting system $(S,\to)$ has the sub-term property if, for every $\tm_0\in S$ and every sequence $\tm_0 \to^n \tm_n$, every step of the sequence either only involves a constant number of constructors or it duplicates or erases a term:

* Structural sub-term property: which is a sub-term of $\tm_0$ up to variables renaming;

* Quantitative sub-term property: of size bound by $\size{\tm_0}$.

In the case of duplications, the number of copies is also bound by $\size{\tm_0}$ (for both notions).

The structural property provides the intuition and gives the name to the property. For cost analyses, however, one only needs the quantitative version. The two formulations are two sides of the same concept and most of the time we simply refer to the sub-term property, without further specification.

$\l$-Calculus $vs$ the Sub-Term Property In the $\l$-calculus, no evaluation strategy has the structural sub-term property—as we now show—because its operational semantics is somewhat too coarse. Let $\tau_{\tm} \defeq \la\vartwo\vartwo\tm\tm$ and $\Id \defeq \la\var\var$. Then:

\begin{equation}
\begin{array}{lllllllll}
\tmtwo \defeq &(\la\var\var(\la\varthree\tau_{\varthree})\tau_{\var}) \Id
\Id(\la\varthree\tau_{\varthree})\tau_{\Id}

\label{eq:no-subterm}
\end{array}\end{equation}

Note that the term $\tau_{\Id}$ duplicated by the third step is not a sub-term of $\tmtwo$. Moreover, $\tmtwo$ is closed and each term in the sequence as at most one $\beta$-redex, which is out of abstractions and the argument of which is a value. Therefore, the example affects also closed weak evaluation, and even its call-by-value variant.

What actually happens is that in the $\l$-calculus duplicated sub-terms are combinations of sub-terms of the initial term, as it is the case for $\tau_\Id$ in the example above. The size of such combinations can grow exponentially with the number of $\beta$-steps, a degeneracy called size explosion and affecting all strategies in the $\l$-calculus, as we shall now recall, suggesting that the number of $\beta$-steps might not be a polynomial cost model for any strategy.

Inevitable Size Exploding Family In the $\l$-calculus, there is a size exploding family that explodes no matter the evaluation strategy. Its definition is in two steps. Firstly, define the following pre-family $\{\tm_n\}_{1\leq n\in\nat}$, where, again, $\tau_{\tm} \defeq \la\vartwo\vartwo\tm\tm$:

\tm_1 & \defeq & \la{\var}\tau_\var
\tm_{n+1}  &\defeq &\la{\var}\tm_n \tau_\var
\end{array}$

The size exploding family is
actually given by $\{\tm_n \Id\}_{1\leq n\in\nat}$ , that is, it is obtained by applying the term $\tm_n$
of the pre-family to the identity.  Note that it is a family of closed terms.
We also define the family of results $\{\tmfour_n\}_{n\in\nat}$ as follows:

\tmfour_0  \defeq  \Id &
\tmfour_{n+1}  \defeq  \tau_{\tmfour_{n}}
\end{array}$$

Last, let $\towh$ be the weak head strategy, which reduces only head redexes out of abstractions and is the simplest meaningful reduction strategy in the $\l$-calculus.

$n \!>\! 0$. Then

* Size explosion for the weak head strategy: $\tm_n \Id \towh^n  \tmfour_n$ and then $i$-th step of the sequence makes two copies of $\tmfour_{i-1}$.

* Strategy independent: any other reduction sequence $\tm_n \Id \towh^*  \tmfour_n$ has length $n$, and all redexes in these sequences are $\betav$ redexes.

Moreover, $\size{\tm_n \Id} = \bigo(n)$, $\size{\tmfour_n} = \Omega(2^n)$,
$\tm_n \Id$ is closed, and $\tmfour_n$ is a $\beta$ normal form.

The bounds on the sizes are straightforward inductions.

* We prove a more general statement: $\tm_n \tmfour_m \towh^n  \tmfour_{n+m}$ (note that $\tmfour_1 = \Id$). By induction on $n$. If $n=1$ then $(\la\var\tau_\var) \tmfour_m \towh \tau_{\tmfour_m} = \tmfour_{m+1}$. For $n+1$, $\tm_{n+1} \tmfour_m = (\la\var\tm_n \tau_\var) \tmfour_m \towh \tm_n \tau_{\tmfour_m} = \tm_n \tmfour_{m+1}$. By ,  $\tm_n \tmfour_{m+1} \towh^n  \tmfour_{n+m+1}$.

* It is easily seen that the $n$ redexes in $\tm_n \Id$ are all hereditarily independent and by-value: they cannot duplicate/erase each other, their arguments are abstractions, and they all produce terms with the same property. Then all local confluence diagrams from $\tm_n \Id$, as well as from the terms reachable from it, are diamonds and all reductions to normal form have the same length.

Size explosion is the fact that the linear size term $\tm_n \Id$ reduces in $n$ steps to the exponential size result $\tmfour_n$, thus doing an exponential amount of work in a linear number of steps. The first point specifies that $\tm_n \Id$ explodes while using the weak head strategy, and that in this case each step of the sequence (but the first one) breaks the structural sub-term property, as it duplicates $\tmfour_n$ which is not a sub-term of the initial term $\tm_n \Id$. Thus, breaking the sub-term property leads to size explosion for the weak head strategy, which breaks the quantitative sub-term property, as, for $n$ big enough, the last duplication of the sequence involves a term bigger than the initial one.

The second point says that the family evaluates to the same result and in the same number of steps according to any other evaluation strategy, no matter whether strong or weak, call-by-name or call-by-value. It is easily seen that the family is also typable with simple types, although of types that grow in size exponentially in $n$. Since the family is also closed, size explosion affects all the main variants and dialects of the $\l$-calculus.

Let us show a final observation about size explosion. Consider the third element $\tm_3 \Id$ of the given family, and let us reduce it in a innermost way:

\begin{equation}
\tm_3 \Id \  = \ (\la{\var}(\la{\var}(\la{\var}\tau_{\var}) \tau_{\var}) \tau_{\var}) \Id
\
\tob \ (\la{\var}(\la{\var}\tau_{\tau_{\var}}) ) \tau_{\var}) \Id
\ \tob \ (\la{\var}\tau_{\tau_{\tau_{\var}}}) \Id
\ \tob \ \tau_{\tau_{\tau_{ \Id}}}
\label{eq:innerm-size-exp}
\end{equation}

The first two steps duplicate $\tau_\var$ and that the last step duplicates $\Id$: it looks like the structural sub-term property is not broken. Here it plays a role the final clause in the definition of the property:
in the case of duplications, the number of copies is also bound by $\size{\tm_0}$.
Indeed in innerm-size-exp it is the number of copies of the duplicated sub-term that grows exponentially (note that $\tau_{\tau_{\tau_{\var_3}}}$ has eight occurrences of $\var_3$), thus still breaking the sub-term property.

Small-Steps $vs$ Micro-Steps
The reader might be aware of the fact that, despite what just explained, the number of steps of some strategies of the $\l$-calculus do provide polynomial cost models. How is that possible?

There is a way out, but it requires deviating from the $\l$-calculus. The lack of the sub-term property in the $\l$-calculus stems from its small-step operational semantics, $\beta$-reduction, which is based on meta-level substitution. To retrieve the property, one has to add ES (or some other form of sharing) to the $\l$-calculus  and decompose $\beta$-reduction in micro-steps performing one variable replacement at a time. Then, there are strategies for the refined setting that have the sub-term property, of which the number of steps thus is a  polynomial cost model. The micro-step refinement can be formulated in various ways,  the LSC being an elegant one. Without going into too much detail, the result is then transferred to the $\l$-calculus, by showing that there is a polynomial simulation (up to some form of sharing) of a small-step strategy by a micro-step one with the sub-term property. Therefore, small-step polynomiality is inherited from the micro-step formalism (as in Blelloch and Greiner <cit.>, Sands et al. <cit.>, Dal Lago and Martini <cit.>, Accattoli and Dal Lago <cit.>, Accattoli et al. <cit.>, Biernacka et al. <cit.>).

Summing up, the sub-term property seems to be mandatory for the study of cost models, because even when the cost model strategy does not have the property, the proof of its polynomiality rests on an auxiliary strategy that does indeed have it. Moreover, the micro-step aspect seems unavoidable for unlocking polynomial time cost models.

Size Explosion in Linear Logic
We now explain how to obtain a size exploding family for linear logic proof nets, taking as notion of evaluation cut elimination at level 0 (the level of a link is the number of $!$ boxes in which it is contained), noted $\Rew{l_0}$, which is, roughly, the analogous of head reduction for proof nets (all head reduction redexes are redexes at level 0, when $\l$-terms are translated to proof nets). We shall need only the following two reduction rules for proof nets:

Promotion / contraction     Promotion / auxiliary port

We shall use $\Rew{\contr 0}$ and $\Rew{\boxbox 0}$ for when these rules are applied to cuts at level $0$.

Size Exploding Family. For the time being, let's consider untyped proof nets. We now define various families of proof nets. The $n$-th net $\tau_{n}$ has the following shape:

at (0,0) [nospace](bang);
at (bang.center) [etic, above left = 6pt and 11pt](name)$\tau_{n}$;
at (bang.center) [etic, left = ](auxr);
at (auxr.center) [etic, left = 1.4*](auxl);
at (auxr.center) [etic, below = 0.7*](auxrghost);
at (auxl.center) [etic, below = 0.7*](auxlghost);
at auxlauxr [etic, below = 0.4*](dots)$...$;
at auxlghostauxrghost[below=, rotate=90, nospace, anchor = center](bracket){;
at (bracket.center)[ below=, nospace](bracket2)$2^{n}$;

at (bang.center)[etic] (bangsym)$!$;

at (bang.center) [etic, below = 0.7*](bangghost);

And it is defined as follows:

Then we define the family $\pi_{n}$, which is obtained from $\tau_{n}$ by contracting all its $2^{n}$ auxiliary conclusions via a tree of contractions:

$\pi_{n} \ \defeq\ \ $
at (0,0) [nospace](bang);
at (bang.center) [etic, above left = 6pt and 11pt](name)$\tau_{n}$;
at (bang.center) [etic, left = ](auxr);
at (auxr.center) [etic, left = 1.4*](auxl);
at (auxr.center) [etic, below = 0.7*](auxrghost);
at (auxl.center) [etic, below = 0.7*](auxlghost);
at auxlauxr [etic, below = 0.4*](dots)$...$;
at (contr.pal) [etic, below = 0.7*](contrghost);

at (bang.center)[etic] (bangsym)$!$;

at (bang.center) [etic, below = 0.7*](bangghost);

also noted
at (0,0) [nospace](bang);
at (bang.center) [etic, above left = 6pt and 5pt](name)$\pi_{n}$;
at (bang.center) [nospace, left = ](auxr);
at (auxr.center) [etic, below = 0.7*](auxrghost);

at (bang.center)[etic] (bangsym)$!$;

at (bang.center) [etic, below = 0.7*](bangghost);

, for instance:

Finally, define the following family of nets:

\rho_1 & \defeq & \pi_{1}
\rho_{n+1} & \defeq & \input{figure-size-exploding-family}
\end{array}$

$\rho_{n} \Rew{0}^{3(n-1)} \pi_{n}$, $\size{\rho_{n}}= \bigo(n)$, and $\size{\pi_{n}}= \Omega(2^{n})$.

By induction on $n$. The bounds on the sizes follow immediately from the definition and the For $n=1$, we have $\rho_{1} = \pi_{1}$, so the statement holds. For $n+1$, we have that by $\rho_{n} \Rew{0}^{3(n-1)} \pi_{n}$. Therefore, we obtain:

The size exploding family of size-exp is a chain of what Roversi and Vercelli in <cit.> call spindles, which they identify as the problematic configurations for representing polynomial time.

Typing the Size Exploding Family The proof net $\rho_{1} = \pi_{1}$ used to build the family can be typed by assigning type $\form$, for an arbitrary type $\form$, to the right conclusion of the axioms (thus having $\form^{\bot}$ on the left conclusion of the axioms), and $\form_{1} \defeq !(\form \tens\form)$ for the right conclusions of $\rho_{1}$ (and $?\form^\bot$ on the left conclusion of $\rho_{1}$). To type the second term of the family $\rho_{2}$, and assuming that the left occurrence of $\pi_{1}$ in $\rho_{2}$ is typed as just described, the right one needs to be typed using $\form_1$ as type of the axioms, thus obtaining as type of the right conclusion, $\form_{2} \defeq !(\form_1\tens \form_1) =  !(!(\form \tens\form)\tens !(\form \tens\form))$. It is then easily seen that the type $\form_{n+1}$ of the right conclusion of $\rho_{n+1}$ is given by $\form_{n+1} = !(\form_{n}\tens \form_{n})$, that is, the type size grows exponentially with $n$.

Size Explosion and Elementary Linear Logic The proofs $\rho_{n}$ of the size exploding family actually belong to elementary linear logic (ELL): they use derelictions—which are forbidden in ELL—but those derelictions can be seen as the auxiliary ports of functorial promotions associated to the $!$s, which are allowed in ELL. Therefore, size explosion affects ELL as well. We mention this fact because ELL has some interesting properties with respect to 's optimal reduction. On the one hand, ELL provides a much simpler implementation of optimal reduction, because the technical oracle part of the implementation is not needed in ELL, as  pointed out by Asperti <cit.>. On the other hand, the complex behavior of duplication responsible for the unreasonability of optimal reduction is already fully present in ELL, and it is thus independent of the oracle, as shown by Asperti et al.  <cit.>. For the study of time cost models, restricting to E(ME)LL does not seem to simplify the problem, as size explosion affects both MELL and EMELL with respect to reduction at level 0. This is rather  in line with the results of <cit.>.

§ THE LINEAR SUBSTITUTION CALCULUS

Here we recall the basics of the linear substitution calculus, which is the footprint of the exponential substitution calculus.

There are various ingredients. First, the syntax of the $\l$-calculus is extended with explicit substitutions $\tm\esub\var\tmtwo$ (shortened to ES), which is a constructor binding $\var$ in $\tm$ (meant to be substituted by $\tmtwo$)—and a compact notation for $\letin\var\tmtwo\tm$—while we use $\tm\isub\var\tmtwo$ for  meta-level substitution.

\textsc{LSC Terms} & \tm,\tmtwo, \tmthree & \grameq \var \mid \la\var\tm \mid \tm\tmtwo
\mid \tm \esub\var\tmtwo
\end{array}$

The LSC is based on the rejection of commuting rules for ES. In traditional $\l$-calculi with ES, a term such as $(\tm\tmtwo)\esub\var\tmthree$ would rewrite to $\tm\esub\var\tmthree\tmtwo\esub\var\tmthree$ by commuting the ES and the application. In the LSC it does not: ES interact directly with variable occurrences, using contexts to specify a commutation-free rewriting system.
Contexts, used pervasively in the study of the LSC, are terms with a hole $\ctxhole$ intuitively standing for a removed sub-term. Here, we need (general) contexts $\ctx$ and the special case of substitution contexts $\lctx$ (standing for List of substitutions).

\textsc{Contexts} & \ctx & \grameq \ctxhole \mid \ctx \tm \mid \tm \ctx \mid \la{\var}{\ctx} \mid %
\ctx \esub\var\tm \mid \tm \esub \var \ctx \\
\textsc{Sub. Ctxs } &\lctx & \grameq \ctxhole \mid \lctx
\esub\var\tm
\end{array}$

Replacing the hole of a context $\ctx$ with a term $\tm$ (or another context $\ctxtwo$) is called plugging and noted $\ctxp\tm$ (resp. $\ctxp\ctxtwo$).
In general, plugging does capture free variables, that is, $(\la\var\ctxhole\var)\ctxholep{\var} = \la\var\var\var$. We use $\ctxfp\tm$ for a plugging with on-the-fly renaming of bound variables of $\ctx$ to avoid capture in $\tm$. For instance, $(\la\var\ctxhole\var)\ctxholefp{\var} = \la\vartwo\var\vartwo$.

The LSC has three rewriting rules. As usual, the root rules are extended to be applied everywhere in a term via a context closure. An unusual aspect is that two of the rules also use contexts in the definition of the root rules.

\multicolumn{4}{c}{\textsc{LSC Root rewriting rules}}\\
\textsc{Beta at a distance} & \lctxp{\la\var\tm}\tmtwo &  \rtodb  & \lctxp{\tm\esub{\var}{\tmtwo}}
\\
\textsc{Linear Substitution}  & \ctxfp\var\esub\var{\tmtwo} &  \rtols  & \ctxfp\tmtwo\esub\var\tmtwo
\\
\textsc{Garbage Collection}  & \tm\esub\var\tmtwo &  \rtogc  & \tm \ \ \ \mbox{if }\var\notin\fv\tm

\end{array}$
Contextual closure:

$\tm \rootRew{a} \tm'$
$  \ctxp{\tm} \Rew{a} \ctxp{\tm'}$

($a \in \set{\db,\ls,\gc}$)

For $\tols$, the notation means that given $\tm\esub\var\tmtwo$ with $\var\in\fv\tm$ we consider a decomposition $\tm=\ctxfp\var$ isolating a free occurrence of $\var$ (one among possibly many). The rule is inspired by replication in the $\pi$-calculus. Examples of steps:

(\la\var\var\vartwo)\esub\vartwo\tm \tmtwo \tmthree
& \todb & (\var\vartwo)\esub\var\tmtwo \esub\vartwo\tm \tmthree
\\
\la\var((\la\vartwo\var\var)\esub\varthree\tm)
\la\var\la\vartwo\var\var
\\
(\la\vartwo\var\var)\esub\var\tm \esub\varthree\tmtwo
(\la\vartwo\var\tm)\esub\var\tm \esub\varthree\tmtwo
\\
(\la\vartwo\var\var)\esub\var\tm \esub\varthree\tmtwo
&\tols& (\la\vartwo\tm\var)\esub\var\tm \esub\varthree\tmtwo
\end{array}$

The LSC is a very well behaved rewriting system (see <cit.>), conservatively extending the $\l$-calculus, and improving it in various respects.

Micro-Step Simulates Small-Step Let $\sizep\tm\var$ the number of free occurrences of $\var$ in $\tm$. The LSC simulates meta-level substitution with

$\tm\esub\var\tmtwo \tols^{\sizep\tm\var} \tm\isub\var\tmtwo\esub\var\tmtwo \togc \tm\isub\var\tmtwo$

that is, by first replacing one by one the occurrences of $\var$ using $\tols$, and then collecting $\esub\var\tmtwo$ when none are left. Therefore, the LSC simulates $\beta$ reduction, as $(\la\var\tm)\tmtwo \todb \tm\esub\var\tmtwo \tols^{*}\togc \tm\isub\var\tmtwo$.

Strong Normalization We define strong normalization as it is relevant for the next property, and shall be used also later on. Given a reduction relation $\to$, the predicate $\tm$ is $\snsubst$, also noted $\tm \in \snsubst$, is defined inductively as follows:

* $\tm$ is $\snsubst$ if $\tm$ is $\to$-normal, , has no $\to$ redexes.

* $\tm$ is $\snsubst$ if $\tmtwo$ is $\snsubst$ for all $\tmtwo$ such that $\tm \to \tmtwo$.

We use $\snsubst$ for the set of terms that are $\sn{\to}$, and say that $\to$ is strongly normalizing (or $\sn{}$) if $\tm\in\sn\to$ for all terms $\tm$.

Local Termination While terms in the LSC can be divergent, because the LSC simulates the $\l$-calculus, an important property is that the rewriting rules of the LSC are strongly normalizing when considered separately.

Let $\to \in \set{\todb, \tols, \togc}$. Then $\to$ is strongly normalizing.

The only non-trivial point is the strong normalization of $\tols$, which requires a measure. It easily extends to the one of $\tols\cup\togc$, that is, of the sub-system rewriting ES. The ESC shall preserve this key property, as we shall prove in local-termination.

Structural Equivalence The LSC is often enriched with the following equivalence.

[Structural equivalence] Define head contexts as follows:

\textsc{Head ctxs} & \hctx & \grameq \ctxhole \mid \hctx \tm  \mid \la{\var}{\hctx} \mid \hctx \esub\var\tmtwo
\end{array}$

If $\var\notin\fv\hctx$ and $\hctx$ does not capture variables in $\fv\tmtwo$, set:

\hctxp\tm\esub\var\tmtwo\ \ \sim \ \ \hctxp{\tm\esub\var\tmtwo}

Structural equivalence $\eqstruct$ is the closure of $\sim$ by reflexivity, symmetry, transitivity, and contexts $\ctx$.

Its key property is that it commutes with evaluation in the following strong sense.

Let $a\in\set{\db,\ls,\gc}$. If $\tm \eqstruct\tmtwo \Rew{a} \tmthree$ then exists $\tmfour$ such that $\tm \Rew{a}\tmfour \eqstruct\tmthree$.

Essentially, $\equiv$ never creates redexes, it can be postponed, and vanishes on normal forms (that have no ES). Accattoli shows that $\equiv$ is exactly the quotient induced by the (call-by-name) translation of $\l$-terms with ES to proof nets <cit.>.

Linear Head Reduction One of the key properties of the LSC is that it admits a neat definition of Danos & Regnier's and Mascari & Pedicini's linear head reduction <cit.>. Before the introduction of the LSC, the presentations of linear head reduction were instead hard to manage. To define it, we need the notion of head context:

\textsc{Head contexts} & \hctx & \grameq \ctxhole \mid \hctx \tm \mid \la{\var}\hctx \mid %
\hctx \esub\var\tm
\end{array}$

Then head contexts are first used to define the root linear head substitution rule:

\textsc{Linear Head Substitution}  & \hctx\ctxholefp\var\esub\var{\tmtwo} &  \rtolhs  & \hctx\ctxholefp\tmtwo\esub\var\tmtwo
\end{array}$

Finally, the root rules $\rtodb$, $\rtolhs$, and $\rtogc$ are closed by head contexts:

3cContextual closures

$\tm \rootRew{\db} \tm'$
$  \hctxp{\tm} \Rew{\symfont{lh}\db} \hctxp{\tm'}$

$\tm \rootRew{\lhs} \tm'$
$  \hctxp{\tm} \tolhs \hctxp{\tm'}$

$\tm \rootRew{\gc} \tm'$
$  \hctxp{\tm} \Rew{\symfont{lh}\gc} \hctxp{\tm'}$

\textsc{Linear head reduction} & \tolh & \defeq \Rew{\symfont{lh}\db} \cup \tolhs \cup \Rew{\symfont{lh}\gc}
\end{array}$

Linear head reduction has many interesting property. For the present paper, the most relevant one is the sub-term property, which, for the given presentation, is proved by Accattoli and Dal Lago in <cit.> (it was already used by Danos & Regnier's and Mascari & Pedicini, but not exploited for complexity analyses).

All the sub-terms duplicated by $\tolhs$ along a linear head evaluation sequence $\tm \tolh^* \tmtwo$ are sub-term of $\tm$ (up to variables renaming).

The good strategy for IMELL that we shall define in strategy generalizes linear head reduction to the whole of IMELL and preserves its sub-term property. For that, note that $\tolh$ never evaluates inside ES. Similarly, the good strategy shall not evaluate inside cuts. Note also that $\tolh$ does not compute normal forms, as it never evaluates arguments. Since we want the good strategy to compute cut-free proofs, we shall have to evaluate the analogous of arguments in our framework (namely, the left premises of subtractions). This shall be obtained by entering into arguments only under some conditions, similarly to how $\tolh$ is generalized to enter inside arguments by Accattoli and co-authors <cit.>, obtaining linear leftmost-outermost reduction.

§ TOWARDS EXPONENTIALS AS SUBSTITUTIONS

This section is an informal and hopefully intuitive introduction to our cut elimination for IMELL. The logical rules we refer to are standard (but decorated with terms), see typing.

Splitting Terms For the moment, we prefer to avoid giving grammars, but we want nonetheless to fix some terminologies and intuitions. We distinguish variables into multiplicatives, noted $\mvar, \mvartwo, \mvarthree$, and exponentials, noted $\evar, \evartwo, \evarthree$, and use $\var,\vartwo,\varthree$ for variables of unspecified kind. Proof terms for axioms and right introduction rules shall be called values, and noted $\val$. We borrow from the LSC the notation $\lctx$ (here standing for Left context) and generalize it to a context corresponding to (the term annotations induced by) a sequence of left rules of the sequent calculus. Exactly as IMELL proofs can be seen as ending on a sequence of left rules following a right rule or an axiom, every proof term $\tm$ shall uniquely (on-the-fly) decompose as $\lctxp\val$, called its splitting.

Meta-Level Substitution For the design of our system, the first step is understanding the subtle interplay between linearity and substitution. Consider a cut on an exponential formula, and a first attempt at decorating it with terms:

$\multiForm   \vdash \tmtwo \hastype \bang\form$
$\multiFormtwo, \evar\hastype \bang\form \vdash \tm\hastype\formtwo$
$  \multiForm, \multiFormtwo\vdash \cuta\tmtwo\evar\tm\hastype\formtwo$

Note that the notation $\cuta\tmtwo\evar\tm$ for cuts is similar but opposite to the one for ES in the LSC, as the arrow goes from left to right and it binds on the right (in $\tm$), to better reflect the structure of sequent proofs. We seek a notion of meta-level substitution $\cutsub\tmtwo\evar\tm$ and a small-step rule such as:

\begin{equation}
\label{eq:naive-sub}
\cuta\tmtwo\evar\tm \ \to\ \cutsub\tmtwo\evar\tm
\end{equation}

Perhaps surprisingly, linear logic does not validate this rule. Despite the $\bang\form$ type, not all of $\tmtwo$, indeed, might be allowed to be duplicated. Let's refine the example and consider the case in which the last rule contributing to $\tmtwo$ is, say, the left rule for $\tens$, what we shall call a par and annotate with $\para\mvar\var\vartwo$:

$\multiForm, \var\hastype\formtwo, \vartwo\hastype\formthree   \vdash \tmtwo' \hastype \bang\form$
$ \tensLeftRule $
$\multiForm, \mvar\hastype\formtwo\tens\formthree   \vdash \para\mvar\var\vartwo\tmtwo' \hastype \bang\form$
$\multiFormtwo, \evar\hastype \bang\form \vdash \tm\hastype\formtwo$
$  \multiForm, \mvar\hastype\formtwo\tens\formthree,\multiFormtwo\vdash \cuta{\para\mvar\var\vartwo\tmtwo'}\evar\tm\hastype\formtwo$

Now we can see why naive-sub is not valid: the annotation $\para\mvar\var\vartwo$ being linear, it should not be duplicated. The proof nets approach to this issue is marking with a box the sub-term/proof net of $\tmtwo'$ that can be duplicated. The usual sequent calculus approach, instead, is commuting the cut with $ \tensLeftRule $, which on proof terms corresponds to have a rule such as:

$\cuta{\para\mvar\var\vartwo\tmtwo'}\evar\tm \to \para\mvar\var\vartwo\cuta{\tmtwo'}\evar\tm$

and then keep commuting the cut with left rules until an introduction of a $\bang$ connective on the right—what we call an exponential value, noted $\exval$—is reached, which can then trigger the substitution. But these commutative rules are a burden, and exactly what the LSC philosophy rejects.

The idea is to exploit the splitting of terms into values and left contexts, so as to import on terms the proof nets approach. A term $\tmtwo$ of exponential type, in fact, shall always be splittable as $\lctxp\exval$, that is, as a left context and an exponential value. We then refine naive-sub as follows:

$\cuta\tmtwo\evar\tm = \cuta{\lctxp\exval}\evar\tm \to \lctxp{\cutsub\exval\evar\tm}

Meta-level substitution thus concerns only exponential values $\exval$—playing the role of proof nets boxes—and not  the surrounding left context $\lctx$. This same mechanism is used in Accattoli and Paolini's value substitution calculus <cit.>.

Split Cuts In fact, we adopt a further refinement. We restrict cuts to have only values as left sub-terms, that is, of being of shape $\cuta\val\var\tm$. Since we want to stick to the standard sequent calculus for IMELL, we do not restrict the typing rule, we do instead modify its decoration:

$\multiForm   \vdash \tmtwo =\lctxp\val \hastype \bang\form$
$\multiFormtwo, \evar\hastype \bang\form \vdash \tm\hastype\formtwo$
$  \multiForm, \multiFormtwo\vdash \lctxp{\cuta\val\evar\tm} \hastype\formtwo$

And we shall do the same for the left rule $\lolliLeftRule$ for $\lolli$ (see typing). This refinement simplifies various technical points, in particular it enables a simple definition of the good strategy.

Micro-Step Substitution For micro-step substitution we simply borrow the LSC approach, adopting rules such as:

$\cuta\exval\evar\ctxfp\evar \to \cuta\exval\evar\ctxfp\exval$

While in line with the LSC, this is not how cut elimination is usually performed in both proof nets and the sequent calculus. There are three main differences:

* LSC-style duplications: in our case duplication happens also when there are no contractions involved, for instance we shall have $\cuta\exval\evar\evar \to \cuta\exval\evar\exval$, and there shall be a rule ($\tobder$) duplicating and interacting with derelictions at the same time (see the next section). Not only this approach is perfectly sound, it actually has better rewriting properties than the traditional one.

* No commutations: there are no commutations with $\bang$. Even in proof nets, where most commutative cuts vanish, micro-step cut elimination usually relies on a commutative rule for  $\bang$-boxes (namely $\Rew{\boxbox}$ in classical-diverging), that on proof terms would look as follows (when $\evar$ occurs in $\tm$):

$\cuta\exval\evar\bang\tm \to \bang\cuta\exval\evar\tm$

The LSC philosophy rejects such a commutative rule.

* Axioms: in the proof nets literature, cut elimination of exponential axioms is identical to the one for multiplicative axioms (there is in fact no distinction between the two kinds of axioms) and simply amounts to the removal of the cut and the axiom, in both the small-step (à la Regnier) and the micro-step (à la Girard) approaches. In (asymmetric) intuitionistic settings, axioms have two rules, depending on whether they are substituted, or substituted upon. In our syntax, the traditional approach to cut elimination for exponential axioms would take the following form:

$ \cuta\evartwo\evar\tm \ \  \to \ \ \cutsub\evartwo\evar\tm$

When written with terms, one immediately notices that such a rule is small-step. In confluence, we shall show that such a small-step rule generates a closable but unpleasant local confluence diagram with the other micro-step exponential rules, which is avoided by adopting a LSC-duplication style also for exponential axioms/variables.

§ THE EXPONENTIAL SUBSTITUTION CALCULUS

Grammars of the exponential substitution calculus.

Values and Terms The grammars of the ESC are in grammars. First of all, a disclaimer. The constructors of the calculus are  an untyped minimalist encoding of the sequent calculus rules, and not an intuitively readable calculus. For that aim, one would rather use $\symfont{let\mbox{-}in}$ notations. Variables are of two disjoint kinds, multiplicative and exponential, and we often refer to variables of unspecified kind using the notations $\var,\vartwo,\varthree$. Values are the proof terms associated to axioms or to the right rules and, beyond variables, are abstractions $\la\var\tm$, tensor pairs $\pair\tm\tmtwo$, and promotions $\bang\tm$. The proof terms decorating left rules are pars $\para\mvar\var\vartwo\tm$, subtractions $\suba\mvar\val\var\tm$, derelictions $\dera\evar\var\tm$,  and cuts $\cuta\val\var\tm$, which is in red because of its special role.  Note that cuts and subtractions are split, that is, have values (rather than terms) as left sub-terms. Back to readability, subtraction might also be decorated with $\letin \var {\mvar\val}\tm$, but note that this notation is less faithful to the logical rule because the two premises are represented asymmetrically, and that it uses an application constructor that rather belongs to natural deduction.

In $\la\var\tm$, $\suba\mvar\val\var\tm$, $\dera\evar\var\tm$, and $\cuta\val\var\tm$ we have that $\var$ is bound in $\tm$, and in $\para\mvar\var\vartwo\tm$ both $\var$ and $\vartwo$ are bound in $\tm$. We identify terms up to $\alpha$-renaming. Free variables (resp.  multiplicative/exponential variables) are defined as expected, and noted $\fv\tm$ (resp. $\mfv\tm$ and $\efv\tm$). We use $\sizep\tm\var$ for the number of free occurrences of $\var$ in $\tm$.
There is a notion of proper term ensuring the linearity of multiplicative variables. The only relevant case is: $\bang\tm$ is if $\tm$ is and $\mfv\tm = \emptyset$.

[Proper terms]

Proper terms are defined by induction on $\tm$ as follows:

* Variables: $\mvar$ and $\evar$ are .

* Tensor: $\pair\tm\tmtwo$ is if $\tm$ is , $\tmtwo$ is , and $\mfv\tm \cap \mfv\tmtwo = \emptyset$

* Par: $\para\mvar\var\vartwo \tm$ is if $\tm$ is and $\mvar \notin(\mfv\tm\setminus{\var,\vartwo})$

* Implication: $\la\var\tm$ is if $\tm$ is and if $\var$ is a multiplicative variable then $\var \in\mfv\tm$.

* Subtraction: $\suba\mvar\val\var \tm$ is if $\tm$ is , $\val$ is , $\mfv\val \cap (\mfv\tm\setminus\set{\var}) = \emptyset$, $\mvar \notin\mfv\tm$, and if $\var$ is a multiplicative variable then $\var \in\mfv\tm$.

* Bang: $\bang\tm$ is if $\tm$ is and $\mfv\tm = \emptyset$.

* Dereliction: $\dera\evar\var \tm$ is if $\tm$ is and if $\var$ is a multiplicative variable then $\var \in\mfv\tm$.

* Cut: $\cuta\val\var\tm$ is if $\tm$ is , $\val$ is , $\mfv\val \cap (\mfv\tm\setminus\set\var) = \emptyset$, and if $\var$ is a multiplicative variable then $\var \in\mfv\tm$.

IMELL typing rules for the ESC, where $\multiForm\#\multiFormtwo$ is a shortcut for $\dom\multiForm\cap\dom\multiFormtwo = \emptyset$.

Typing System The typing rules are in typing. The formulas of IMELL and the deductive rules of the sequent calculus are standard, but for the decoration with proof terms and the side conditions about variable names. Linear implication $\lolli$ is also referred to as lolli. The only atomic formula that we consider, $\aform$, is multiplicative. There is no multiplicative unit because in presence of the exponentials $1$ can be simulated by $!(\aform \lolli\aform)$. We distinguish between multiplicative and exponential axioms, in order to decorate them with the corresponding kind of variable.
Note that the weakening and contraction rules do not add constructors to terms. This is crucial in order to keep the calculus manageable. Note also that the decorations of the cut and $\lolliLeftRule$ rules are split, as explained in the previous section. Clearly, typed terms are proper.  We use $\tderiv \pof \multiForm \vdash \tm\hastype \form$ for a proof/typing derivation $\tderiv$ ending in that sequent.

Contexts and Plugging The broadest notion of context that we consider is general contexts $\ctx$, which simply allow the hole $\ctxhole$ to replace any sub-term in a term. Because of split cuts and subtractions, the definition relies on the auxiliary notion of value context $\vctx$. The definition also uses left contexts $\lctx$, which are contexts under left constructors (or, for binary left constructors, under the right sub-term) that play a key role in the system—their use in defining $\ctx$ is just to keep the grammar compact (to fit it in the figure).

A fact used pervasively is that every term $\tm$ writes, or splits uniquely as $\tm = \lctxp\val$. For instance $\dera\evar\mvar\cuta\val\mvartwo\pair\mvar\mvartwo$ splits as $\lctx = \dera\evar\mvar\cuta\val\mvartwo\ctxhole$ and $\val =\pair\mvar\mvartwo$. We also have multiplicative contexts $\mctx$, that the proof nets literature would call level 0 contexts, that is, contexts with the hole out of all $\bang$, and which also rely on their own value contexts $\vmctx$.

Because of split cuts and subtractions, plugging is slightly tricky, as it has to preserve the split shape.  For instance, we have $(\cuta\ctxhole\mvarthree\tm)\ctxholep{\dera\evar\mvar\pair\mvar\mvartwo} = \dera\evar\mvar\cuta{\pair\mvar\mvartwo}\mvarthree\tm$.
A similar approach to plugging is also used by Accattoli et al. in <cit.>. The full definition follows. It is mostly as expected, the only two subtle cases are for $\cuta\ctxhole\var\tm$ and $\suba\mvar\ctxhole\var$.

Plugging $\ctxp\tm$ is defined as follows:

\ctxhole\ctxholep\tm & \defeq & \tm
(\la\var\ctx)\ctxholep\tm& \defeq & \la\var\ctxp\tm
\\
\pair\ctx\tmtwo\ctxholep\tm & \defeq & \pair{\ctxp\tm}\tmtwo
\pair\tmtwo\ctx\ctxholep\tm & \defeq & \pair\tmtwo{\ctxp\tm}
\\
(\bang\ctx)\ctxholep\tm& \defeq & \bang\ctxp\tm
(\dera\evar\var\ctx)\ctxholep\tm & \defeq & \dera\evar\var\ctxp\tm
\\
(\para\mvar\var\vartwo \ctx)\ctxholep\tm& \defeq & \para\mvar\var\vartwo \ctxp\tm
(\suba\mvar\val\var\ctx)\ctxholep\tm& \defeq & \suba\mvar\val\var\ctxp\tm
\\
(\cuta\val\var\ctx)\ctxholep\tm & \defeq &  \cuta\val\var\ctxp\tm
\end{array}$

(\suba\mvar\vctx\var\tmtwo)\ctxholep\tm& \defeq &
\begin{cases}
\lctxp{\suba\mvar\val\var\tmtwo}
& \mbox{if }\vctx = \ctxhole\mbox{ and }\tm = \lctxp\val
\\
\suba\mvar{\vctxp\tm}\var\tmtwo  & \mbox{otherwise}
\end{cases}
\\
(\cuta\vctx\var \tmtwo)\ctxholep\tm& \defeq &
\begin{cases}
\lctxp{\cuta\val\var \tmtwo} & \mbox{if }\vctx = \ctxhole\mbox{ and }\tm = \lctxp\val
\\
\cuta{\vctxp\tm}\var \tmtwo & \mbox{otherwise}
\end{cases}
\end{array}$

Plugging $\ctxp\ctxtwo$ of contexts is defined similarly, and plugging is extended to all forms of contexts by seeing them as general contexts. As for the LSC, plugging can capture variables and we use $\ctxfp\tm$ when we want to prevent it.

With our notion of plugging, a left constructor in a term might be identified via plugging of a term in a context in various ways, for $\tm \defeq \pair{\dera\evar\mvar\cuta\mvar\mvartwo\mvartwo}{\evartwo}$ we have $\tm = \ctxp{\dera\evar\mvar\mvar}$ with $\ctx \defeq \pair{\cuta\ctxhole\mvartwo\mvartwo}{\evartwo}$, and $\tm = \ctxtwop{\dera\evar\mvar\cuta\mvar\mvartwo\mvartwo}$ with $\ctxtwo \defeq\pair{\ctxhole}{\evartwo}$. For most uses, in particular for defining the rewriting rules, this is harmless. It shall play a role, however, for defining the good strategy, because it shall be important whether the hole of the context is inside or outside a cut. Then note that in the first decomposition the term $\dera\evar\mvar\mvar$ is not a sub-term of $\tm$. This suggest the following notion. A position in a term $\tm$ is a decomposition $\tm=\ctxp\tmtwo$ such that $\tmtwo$ is a sub-term of $\tm$ (as for $\ctxtwop{\dera\evar\mvar\cuta\mvar\mvartwo\mvartwo}$ above).

We can now state the property ensured by properness.

Let $\tm$ be a term and $\mvar\in\mfv\tm$. Then $\varmeas\tm\mvar = 1$ and $\tm = \mctxfp\mvar$ for some $\mctx$.

By induction on $\tm$.

Rewriting rules of the ESC.

Meta-Level Substitution and the Small-Step Exponential Rule The rewriting rules are in rewriting-rules. For defining the small-step exponential cut elimination we need meta-level substitution $\cutsub\exval\evar\tm$, which is defined only for exponential values (that is, exponential variables $\evartwo$ and promotions $\bang\tm$). The long definition is mostly as expected, but for one case, explained after the definition.
[Meta-level exponential substitution]

The meta-level (exponential) substitution $\cutsub\exval\evar\tm$ of the exponential value $\exval$ for the free occurrences of $\evar$ in $\tm$ is defined by induction on $\tm$ as follows (assuming on-the-fly $\alpha$-renaming to avoid capture of free variables, omitted for ease of reading and manipulation):

2cMeta-level substitution

\cutsub{\exval}\evar \mvar & \defeq & \mvar
\\
\cutsub\exval\evar \evartwo & \defeq & \evartwo
\\
\cutsub{\exval}\evar \evar & \defeq & \exval
\\
\cutsub{\exval}\evar \pair\tm\tmthree & \defeq & \pair{\cutsub{\exval}\evar\tm}{\cutsub{\exval}\evar\tmthree}
\\
\cutsub{\exval}\evar \la\var\tm & \defeq & \la\var \cutsub{\exval}\evar \tm
\\
\cutsub{\exval}\evar \bang\tm& \defeq & \bang\cutsub{\exval}\evar\tm
\end{array}$

\cutsub{\exval}\evar\para\mvar\var\vartwo \tm & \defeq & \para\mvar\var\vartwo  \cutsub{\exval}\evar \tm
\\
\cutsub{\exval}\evar \suba\mvar\val\var \tm & \defeq & \suba\mvar {\cutsub{\exval}\evar\val}\var \cutsub{\exval}\evar\tm
\\
\cutsub{\exval}\evar \dera\evartwo\var \tm & \defeq & \dera\evartwo\var \cutsub{\exval}\evar \tm
\\
\cutsub{\evartwo}\evar \dera\evar\var \tm & \defeq & \dera\evartwo\var \cutsub{\exval}\evar\tm
\\
\cutsub{\bang\lctxp\val}\evar \dera\evar\var \tm & \defeq & \lctxp{\cuta\val\var \cutsub{\exval}\evar\tm}
\\
\cutsub{\exval}\evar \cuta\val\var\tm & \defeq & \cuta{\cutsub{\exval}\evar\val}\var \cutsub{\exval}\evar\tm
\end{array}$

The key case is the substitution of a promotion for a dereliction (the second to last in the right column), that removes the dereliction, copies the promotion body, and puts it in a cut—in proof nets jargon, it opens the box. To preserve the split shape, the body of the promotion is split and only the value is cut. An example:

$\cutsub{\bang\cuta\evartwo\evarthree \evarthree}\evar \dera\evar{\evar'} \pair{\evar'}\evar = \cuta\evartwo\evarthree \cuta{\evarthree}{\evar'} \pair{\evar'}{\bang\cuta\evartwo\evarthree \evarthree}$

Our definition verifies the expected properties of meta-level substitution. Some are given by the next two lemmas.

* If $\exval$ and $\tm$ are proper then $\cutsub\exval\evar\tm$ is proper.

*  $\cutsub\exval\evar\exvaltwo$ is an exponential value and $\cutsub\exval\evar\mval$ is a multiplicatie value.

*  If $\ctx$ does not capture free variables of $\exval$ then $\cutsub\exval\evar \ctxp\tm = (\cutsub\exval\evar \ctx)\ctxholep{\cutsub\exval\evar \tm}$.

*  $\cutsub\exval\evar \tmtwo = \tmtwo$ if $\evar\notin\fv\tmtwo$.

*  $\cutsub{\exval}\evartwo \cutsub{\exvaltwo}\evar \tm =  \cutsub{\cutsub{\exval}\evartwo\exvaltwo}\evar \cutsub{\exval}\evartwo\tm$.

*  $\cutsub\exval\evar \cutsub\exvaltwo\evartwo \tmthree = \cutsub\exvaltwo\evartwo \cutsub\exval\evar \tmthree$ if $\evar\notin\fv\tmtwo$ and $\evar\notin\fv\tmthree$.

*  $\cutsub\exval\evar \cutsub\mvartwo\mvar \tmthree = \cutsub\mvartwo\mvar \cutsub\exval\evar \tmthree$.

*  $\cutsub{\bang\tmthree}\evar \cutsub{\bang\tmthree}\evartwo \tm = \cutsub{\bang\tmthree}\evar\cutsub\evar\evartwo\tm$.

If $\tm \Rew{a} \tmtwo$ then $\cutsub{\exval}\evar\tm \Rew{a} \cutsub{\exval}\evar\tmtwo$ for $a\in\set{\axmone,\axmtwo,\tens,\lolli,\ess, \ems}$.

If $\exval \Rew{a} \exvaltwo$ then $\cutsub{\exval}\evar\tm \Rewn{a}\cutsub{\exvaltwo}\evar\tm$ for $a\in\set{\axmone,\axmtwo,\tens,\lolli,\ess, \axeone,\axetwo,\bdersym,\wsym}$.

The small-step exponential rule $\toess$ then simply turns a cut $\cuta\exval\evar\tm$ into the corresponding meta-level substitution.

Multiplicative Cut Elimination Rules The ESC has four multiplicative rules, in particular two for axioms, depending on whether they are acted upon ($\toaxmone$) or used to rename another multiplicative (thus linear) variable ($\toaxmtwo$). For $\toaxmtwo$, we abuse notations and use a form of meta-level substitution $\cutsub\mvartwo\mvar\tm$ for the renaming operation. There is also a slight superposition between $\toaxmone$ and $\toaxmtwo$, for instance in $\cuta\mvar\mvartwo \la\evar\mvartwo \to \la\evar\mvar$, which can be both kinds of steps. To disambiguate, one should refine $\toaxmtwo$ into two rules:

\cuta{\mvartwo}\mvar \mctxp{\para\mvar\var\vartwo \tm}
& \Rew{\axmtwo'} &
\mctxp{\para\mvartwo\var\vartwo \tm}
\\[3pt]
\cuta{\mvartwo}\mvar \mctxp{\suba\mvar\val\var  \tm}
& \Rew{\axmtwo''} &
\mctxp{\suba\mvartwo\val\var \tm}
\end{array}$

But the ambiguity is harmless and the notation is convenient. Note that in $\toaxmone$, $\totens$, and $\tololli$ (and $\Rew{\axmtwo'/\axmtwo''}$), the cut acts on a sub-term inside a multiplicative context $\mctx$, that is, out of $!$. Moreover, it is silently assumed that $\mctx$ does not capture $\mvar$ in $\totens$ and $\tololli$ (and $\Rew{\axmtwo'/\axmtwo''}$), but it might capture other variables in $\tm$ and $\val$.

In both $\totens$ and $\tololli$ the rule has to respect split cuts, which is why, for writing the reduct, the sub-terms $\tmtwo$ and $\tmthree$ are split. We suggest to have a look at the proof of subject reduction on page thm:sub-red, which shows how some of the rewriting steps act on the decorated proof.
An example of $\tololli$ step follows:

$\cuta{\la\evar\dera\evar\mvar\mvar}\mvartwo\suba\mvartwo{\bang\evartwo}\mvarthree\mvarthree \ \tololli \
\cuta{\bang\evartwo}\evar\dera\evar\mvar\cuta\mvar\mvarthree \mvarthree.$

Micro-Step Exponential Rules There are also four micro-step exponential rules, with again two rules for axioms. Replacement of variables ($\toaxeone$) and erasure ($\tobw$) are expressed generically for exponential values $\exval$, interaction with derelictions (in $\toaxetwo$ and $\tobder$) instead requires inspecting $\exval$. Rule $\tobder$ simply turns into a rewriting rule the relevant case in the definition of meta-level substitution. Note that it entangles interaction with a dereliction and duplication, which is not what proof nets usually do, as mentioned in towards.  It is silently assumed that $\ctx$ does not capture $\evar$ in $\toaxetwo$ and $\tobder$ but it might capture other variables in $\tm$.

Linear Implication and Cuts Creations Rule $\tololli$ is special in that it is the only rule of the ESC that creates cuts. Note indeed that in the root $\rtololli$ rule:

\cuta{\la\vartwo\lctxp\val}\mvar \mctxp{\suba\mvar\valtwo\var \tm}
& \rtololli &
\mctxp{ \cuta\valtwo\vartwo \lctxp{\cuta\val\var \tm }}
\end{array}$

the cut $\cuta\valtwo\vartwo$ in the reduct is not a cut of the reducing term. One might argue that also $\rtotens$ and $\rtobang$ do create cuts, because in their root rules, recalled here:

\cuta{\pair{\lctxp\val}{\lctxtwop\valtwo}}\mvar \mctxp{\para\mvar\var\vartwo \tm}
\mctxp{\lctxp{\cuta\val\var \lctxtwop{\cuta\valtwo\vartwo \tm}}}
\\[6pt]
\cuta{\bang\lctxp\val}\evar\ctxp{\dera\evar\var \tm}
& \rtobang &
\cuta{\bang\lctxp\val}\evar\ctxp{\lctxp{\cuta\val\var \tm}}
\end{array}$

the cuts $\cuta\val\var$ and $\cuta\valtwo\vartwo$ of the reducts are not in the reducing terms. The difference is that $\val$ and $\valtwo$ do occur as sub-terms of cuts in the reducing terms of $\rtotens$ and $\rtobang$, while in $\rtololli$ the value $\valtwo$ does not. We then say that $\cuta\valtwo\vartwo$ is created in $\rtololli$.
This fact shall play a key role for local termination (local-termination below) and for the good strategy. Being specific to $\tololli$, it is a feature of the intuitionistic setting, that is, it is invisible in classical linear logic.

Positions and Redexes For later defining the good strategy, we identify a redex with its position, which is a context, as it is done for the LSC by Accattoli and Dal Lago  <cit.>. Every step $\tm \tomsnw \tmtwo$ reduces a redex of shape $\tm=\ctxp{\cuta\val\var\ctxtwop{\tm_{\var}}}$ where $\tm_{\var}$ is an occurrence of $\var$, a sub-term of $\tm$ of shape $\var$, $\para\var\vartwo\varthree\tmtwo$, $\suba\var\val\vartwo\tmtwo$, or $\dera\var\vartwo\tmtwo$. The position of the $\tomsnw$ redex is the context $\ctxp{\cuta\exval\var\ctxtwo}$. For $\tobw$ and $\toess$ redexes, the position is the context closing the root step (as a sub-term). We write $\ctx:\tm\Rew{\mssym/\sssym}\tmtwo$ for a redex of position $\ctx$.

We conclude the section with the fact that proper terms are stable by reduction.

Let $\ctxp\tm$ be a term. Then:

* $\tm$ is .

* If $\tmtwo$ is and such that $\mfv\tmtwo = \mfv\tm$ then $\ctxp\tmtwo$ is .

By induction on $\ctx$.

Let $\tm$ be a term and $\tm \toms \tmtwo$. Then $\tmtwo$ is .

Let $\tm = \ctxp\tmthree \toms \ctxp\tmfour = \tmtwo$. By proper-replacement, $\tmthree$ is , and to prove the statement it is enough to prove that if $\tmthree \toms \tmfour$ is a root step then $\tmfour$ is proper and  $\mfv\tmfour = \mfv\tmthree$. Note that all the  root  rules preserve the set of multiplicative variables, that is, $\mfv\tmfour = \mfv\tmthree$ holds. Proving that the root rules preserve being is a straightforward induction.

Preservation of properness by $\toess$ follows from full composition (ms-simulates-ss),  just below.

§ BASIC PROPERTIES

We now prove various basic properties of the ESC. An expected property that we do not prove is the simulation of the LSC by the ESC. It can be obtained via Girard's (call-by-name) encoding of intuitionistic logic into linear logic. It is not surprising and yet it is technical, for reasons (the encoding of applications via subtractions) that are intrinsic to the translation and orthogonal to the features of the ESC, which is why it is omitted.

Full Composition. First of all, micro-step exponential rules simulate the small-step one. The ES literature calls this fact full composition.

If $\tm\toess \tmtwo$ then $\tm\toems^{+}\tmtwo$.

$\tm = \ctxp{\cuta\exval\evar\tmthree} \toess \ctxp{\cutsub\exval\evar\tmthree} = \tmtwo$. We treat the case $\exval = \bang\tmfour$, the case $\exval = \evartwo$ is analogous. The proof is by induction on $k \defeq \varmeas{\tmthree}\evar$. If $k = 0$ then $\ctxp{\cuta\exval\evar\tmthree} \tobw \ctxp{\tmthree} = \ctxp{\cutsub\exval\evar\tmthree}$. Otherwise, $\tmthree$ writes has $\ctxtwop{\evar}$ or $\ctxtwop{\dera\evar\var \tmthree'}$. Consider the first case. Then:

$\ctxp{\cuta{\bang\tmthree'}\evar\ctxtwop{\evar}} \toaxeone
\ctxp{\cuta{\bang\tmthree'}\evar\ctxtwop{\bang\tmthree'}} =: \tmtwo'

Now note that $\tmtwo' \toess \tmtwo$ and that in $\tmtwo'$ we have $\varmeas{\ctxp{\bang\tmthree'}}\evar < k$. Then we can apply the , obtaining $\tmtwo' \toems^{+}\tmtwo$, that is, $\tm \toems^{+}\tmtwo$. The case $\tmthree=\ctxtwop{\dera\evar\var \tmthree'}$ is analogous, simply using $\tobder$ instead of $\toaxeone$.

Let $\tm$ be a term and $\tm \toss \tmtwo$. Then $\tmtwo$ is .

Subject Reduction. The next property is that the defined untyped cut elimination respects the typing system, that is, subject reduction holds. We first need a lemma.

Let $\tderiv \pof \multiform \vdash \tm \hastype \form$.  We have $\form = \bang\formtwo$ if and only if $\tm = \lctxp\exval$.

If $\form =  \bang\formtwo$, then consider $\tm = \lctxp\val$. The proof is by induction on $\lctx$. Clearly, if $\lctx=\ctxhole$ then the last rule of $\tderiv$ is necessarily an exponential axiom or a right introduction of $\bang$, that is, $\val = \evar$ or $\val = \bang\tmtwo$, that is, $\val$ is an exponential value. If $\lctx \neq \ctxhole$ then it follows from the

The reasoning is analogous if $\form \neq \bang\formtwo$.

Let $\multiform\vdash \tm\hastype \form$ and $\tm \toms \tmtwo$. Then $\multiform\vdash \tmtwo\hastype \form$.

Full composition extends subject reduction to $\toess$.

Clashes. The presence of many constructors in an untyped setting gives rise to clashes, that is, irreducible cuts.
[Clash, clash-free terms]
A clash is a term of the form $\cuta\mval\evar\tm$, $\cuta\exval\mvar\tm$, $\cuta{\pair\tm\tmtwo}\mvar \mctxp{\suba\mvar\val\vartwo\tmthree}$, or $\cuta{\la\var\tm}\mvar \mctxp{\para\mvar\vartwo\varthree \tmthree}$ and in these cases we also say that the root cut is clashing. A term $\tm$ is clash-free if, co-inductively,

* No sub-terms of $\tm$ are clashes, and

* If $\tm \toms \tmtwo$ then $\tmtwo$ is clash-free.

Note that there are no purely exponential clashes. The second point of the next lemma uses subject reduction.

Let $\tm$ be a proper term.

* If $\tm$ has no clashes and $\tm \not\toms$ then $\tm$ is cut-free.

* If $\tm$ is typable then it is clash-free.

* Suppose by contradiction that $\tm$ has a cut. Then $\tm = \ctxp{\cuta\val\var\tmtwo}$. If $\var$ is exponential then, since there are no clashes, $\val$ is also exponential. Then there is a $\toess$ redex, and, by full composition, a $\toems$ redex, absurd. If $\var=\mvar$ is multiplicative then so is $\val$. By structural linearity (proper-linearity), $\tmtwo$ has one of the following shapes:

* $\mctxp\mvar$. Then there is a $\toaxmone$ redex, absurd.

* $\mctxp{\para\mvar\vartwo\varthree\tmtwo}$. Since $\tm$ has no clashes, $\val$ is either a multiplicative variable, and then there is a $\toaxmtwo$ redex, or a tensor pair, and then there is a $\totens$ redex, absurd.

* $\mctxp{\suba\mvar\val\vartwo\tmtwo}$. Since $\tm$ has no clashes, $\val$ is either a multiplicative variable, and then there is a $\toaxmtwo$ redex, or an abstraction, and then there is a $\tololli$ redex, absurd.

* By co-induction on the definition of being clash-free. It is easily seen that clashes are not typable. So if $\tm$ is typable then it has no clashes. Now, if $\tm \toms \tmtwo$ then by subject reduction (sub-red) $\tmtwo$ is typable. By the co-inductive hypothesis, $\tmtwo$ is clash-free. Therefore, $\tm$ is clash-free.

Postponement of Garbage Collection The micro-step rule $\tobw$, that models garbage collection, can be postponed. The same happens in the LSC,
but not in the $\l$-calculus: for instance, the first step in the sequence $(\la\var\la\vartwo\vartwo)\tmtwo\tmthree \tob (\la\vartwo\vartwo)\tmthree \tob \tmthree$ is erasing but cannot be postponed.

If $\tm \tobw \tomsnw \tmtwo$ then $\tm\tomsnw \tobw^{+}\tmtwo$.

if $\tm \toms^{*} \tmtwo$ then $\tm \tomsnw^{*} \tobw^{*} \tmtwo$.

It is an instance of a well-known rewriting property: the local swap in local-post-gc is an instance of Hindley's strong postponement property, which implies postponement.

Cut Equivalence Similarly to the structural equivalence of the LSC, we consider a notion of cut equivalence, which is a strong bisimulation and it is postponable.

[Cut equivalence]
If $\var\notin\fv\mctx$ and $\mctx$ does not capture variables in $\fv\val$, define:

\cuta\val\var \mctxp\tm\ \ \rcuteq \ \ \mctxp{\cuta\val\var \tm}

Cut equivalence $\cuteq$ is the closure of $\rcuteq$ by reflexivity, symmetry, transitivity, and general contexts.

To prove that cut equivalence is a strong bisimulation in the small-step case, we need the following substitutivity property.

If $\tm \cuteq \tmtwo$ then $\cutsub\exval\evar\tm \cuteq \cutsub\exval\evar\tmtwo$ for all $\exval$.

If $\exval \cuteq \exvaltwo$ then $\cutsub\exval\evar\tm \cuteq \cutsub\exvaltwo\evar\tm$.

Let $\to\in\set{\toss,\toms}$.

* Strong bisimulation:
$\cuteq$ is a strong bisimulation with respect to $\to$, preserving also the kind of step.

Preservation of SN: if $\tm \cuteq \tmtwo$ and $\tm\in\snsubst$ then $\tmtwo\in\snsubst$.

* Postponement of $\cuteq$: if $\tm (\cuteq\to\cuteq)^k \tmtwo$ then $\tm \to^k \cuteq \tmtwo$.

Cut equivalence shall play a role in the following sections. Note that its postponement property means that it is never needed for cut elimination to progress. And on cut-free terms, obviously, it vanishes.

There is also a larger left equivalence $\streq_{\symfont{left}}$ defined as $\cuteq$ but including every left constructor (cut, par, subtraction, and dereliction), which is also a strong bisimulation. As mentioned in lsc, $\equiv$ is the quotient induced by proof nets on the LSC. Intuitively, $\streq_{\symfont{left}}$ is the quotient induced by proof nets on the ESC. There are, however, no proof nets realizing such a quotient, as weakenings require non-canonical jumps for IMELL, that can instead be avoided for the LSC, as shown by Accattoli <cit.>.

A possibly interesting point is that we shall need cut equivalence, in particular for the proof of strong normalization, while there is no need of left equivalence for any of the properties studied in this paper.

Stability Under Renaming The last basic property that we prove is the stability of the rules and of their strong normalization under renaming.

Let $\to\in\set{\toss,\toms}$ and $\var$ and $\vartwo$ be two variables of the same
multiplicative/exponential kind such that  $\cutsub\var\vartwo\tm$ is proper.

*  Stability of steps under renaming:
if $\ctx:\tm \Rew{a} \tmtwo$ then $\cutsub\vartwo\var\ctx:\cutsub\vartwo\var\tm \Rew{a} \cutsub\vartwo\var\tmtwo$.

*  Stability of SN under renaming:
if $\tm \in \sn\toss$  then $\cutsub\var\vartwo\tm \in \sn\toss$.

* Straightforward induction on the rewriting step.

* By induction on $\elctxfp\tm\in\sn\toss$. Since renaming cannot create, erase, duplicate, or change the kind of redexes,
if $\cutsub\var\vartwo\tm \toss \tmtwo$ then there exists $\tmthree$ such that $\tm \toss \tmthree$ and
$\cutsub\var\vartwo\tmthree = \tmtwo$. Then by on $\tmthree$ we obtain $\cutsub\var\vartwo\tmthree=\tmtwo\in\sn\toss$.

§ LOCAL TERMINATION

Here we are going to prove that the ESC has the same local termination property of the LSC, thus showing that one can claim that it realizes the slogan exponentials as substitutions.

Divergence Let us first show that evaluation in the untyped ESC can diverge. We adapt the usual looping combinator $\Omega$ of the $\l$-calculus. Let $\delta \defeq \la\evar\dera\evar\mvar\suba\mvar\evar\mvartwo\mvartwo$ and consider:

\begin{array}{lllllll}
\Omega &\defeq &\cuta\delta\mvarthree \suba\mvarthree{\bang\delta}{\mvarthree'}\mvarthree'
& \tololli &
\cuta{\bang\delta}\evar \dera\evar\mvar\suba\mvar\evar\mvartwo\cuta\mvartwo{\mvarthree'}\mvarthree'
\\
&&& \toaxeone &
\cuta{\bang\delta}\evar \dera\evar\mvar\suba\mvar{\bang\delta}\mvartwo\cuta\mvartwo{\mvarthree'}\mvarthree'
\\
&&& \tobder &
\cuta{\bang\delta}\evar \cuta\delta\mvar \suba\mvar{\bang\delta}\mvartwo\cuta\mvartwo{\mvarthree'}\mvarthree'
\\
&&& \tow &
\cuta\delta\mvar \suba\mvar{\bang\delta}\mvartwo\cuta\mvartwo{\mvarthree'}\mvarthree'
\\
&&& \toaxmone &
\cuta\delta\mvar \suba\mvar{\bang\delta}\mvartwo\mvartwo
&=_\alpha & \Omega
\end{array}

Local Termination A key feature of the untyped ESC (inherited from the LSC) is local termination, that is, every rewriting rule is strongly normalizing (SN) when considered separately (not valid in the $\l$-calculus which has only one rule). Additionally, the groups of multiplicative rules $\tom$ and of micro-step exponential rules $\toems$ are also SN separately, which is instead not valid in untyped classical proof nets (classical-diverging left).

Even the union of all the micro-step rules except $\tololli$, noted $\tomsnlolli$, is SN. This is due to the fact that $\tololli$ is the only rule that creates cuts, as explained in calculus. Strong normalization of $\tomsnlolli$ is a deep property, pointed out here for the first time. It shows that, for expressivity, rule $\tololli$ is as important as duplication, and thus, non-linearity. It also shows that $\lolli$ and $\tens$ have completely different computational properties. This is remarkable because in classical linear logic à la Girard, the two are collapsed and managed by a single cut elimination rule, the one for $\parr/\tens$, and creations are not visible. Together with (non-)termination of untyped exponentials, it is a sign that the intuitionistic setting is sharper than the classical one for studying cut elimination.

Proving Local Termination. The proofs of local termination and of the termination of $\tomsnlolli$ require various definitions. First, we need a notion of variable potential, which is used to define a measure, that it is then showed to decrease with every micro-step rewriting rule but $\tololli$. A number of auxiliary lemmas are also required.

The intuition behind the potential $\potmul\tm\var$ of a variable $\var$ in $\tm$ is that it is the maximum number of occurrences of $\var$ that can appear during the cut elimination of $\tm$, plus the same number for all the variables that are recursively 'nested' under $\var$, where for instance $\var$ nests under $\evar$ in $\dera\evar\var\tm$. The key clause is the one for cuts $\cuta\val\var\tm$, which multiplies the potential in $\val$ for the one of $\var$ in $\tm$.
[Variable potential]
The potential $\potmul\tm\var$ of a variable $\var$ in $\tm$ is given by:

\potmul \vartwo \var & \defeq & 0
\\
\potmul \var \var & \defeq & 1
\\\potmul{ \pair\tm\tmtwo}\var & \defeq & \potmul\tm\var + \potmul\tmtwo\var
\\
\potmul{ \bang \tm}\var& \defeq & \potmul{  \tm}\var
\\
\potmul{ \la\vartwo\tm}\var & \defeq &  \potmul\tm\var

\end{array}$

\potmul{\para\mvar\vartwo\varthree \tm}\var & \defeq &
\begin{cases}
1+ \potmul\tm\vartwo + \potmul\tm\varthree & \mbox{if }\var=\mvar\\
\potmul{  \tm}\var & \mbox{otherwise.}
\end{cases}
\\
\potmul{\suba\mvar\val\vartwo  \tm}\var & \defeq & \
\begin{cases}
1 & \mbox{if }\var=\mvar\\
\potmul\val\var + \potmul\tm\var & \mbox{otherwise.}
\end{cases}
\\
\potmul{\dera\evar\vartwo \tm}\var & \defeq &
\begin{cases}
1 + \potmul\tm\var + \potmul\tm\vartwo & \mbox{if }\var=\evar\\
\potmul\tm\var & \mbox{otherwise.}
\end{cases}
\end{array}$

\potmul{\cuta\val\vartwo\tm}\var & \defeq & \potmul\tm\var + \potmul\val\var\cdot(\potmul\tm\vartwo +1)
\end{array}$

The potential is extended to contexts by considering $\ctxhole$ as a (fresh) exponential variable, that is, having $\potmul\ctxhole\var \defeq 0$, $\potmul\var\ctxhole \defeq 0$, and $\potmul\ctxhole\ctxhole \defeq 1$, plus all the expected inductive cases for contexts.

In the definition of the potential, the clause for cut multiplies $\potmul\val\var$ for $\potmul\tm\vartwo +1$ where, for exponential variables, the $+1$ accounts for the garbage copy of $\val$ that survives the replacement of all the occurrences of $\var$ with $\val$. The clause does not distinguish between cuts on multiplicative or exponential variables, treating all variables as if they were exponential. Such an over-estimate is harmless and provides a more compact definition of the potential.

Note also the clause for subtractions: when $\var=\mvar$, one could define it as $0$, because anyway cuts on subtractions are ignored. But it simpler to set it to $1$, as to obtain the useful property of potmul-proponebis below.

[Termination measure]

The termination measure $\ltmeas\tm$ of a term $\tm$ is defined as follows (and extended to contexts by defining it also for $\ctxhole$):

$\begin{array}{rll\colspace \colspace rll}
\ltmeas\var & \defeq & 1
\ltmeas\ctxhole & \defeq & 0
\\
\ltmeas{\para\mvar\var\vartwo \tm} & \defeq & \ltmeas{  \tm} +1
\ltmeas{ \pair\tm\tmtwo} & \defeq & \ltmeas\tm + \ltmeas\tmtwo
\\
\ltmeas{\suba\mvar\val\var \tm} & \defeq & \ltmeas\val + \ltmeas\tm +1
\ltmeas{ \la\var\tm} & \defeq &  \ltmeas\tm
\\
\ltmeas{\dera\evar\var \tm} & \defeq & \ltmeas\tm+1
\ltmeas{ \bang \tm}& \defeq & \ltmeas{  \tm}
\\
\ltmeas{\cuta{\val}\var\tm} & \defeq & \ltmeas\val\cdot(\potmul\tm\var +1) + \ltmeas\tm
\end{array}$

The idea behind the measure is that it counts all variable occurrences (that is, variables, pars, derelictions, and subtractions), multiplying for the potential of $\var$ the occurrences appearing in a value cut on $\var$, as for the potential. Each rewriting step removes a variable occurrence, which makes the measure decrease. An exponential rewriting step can also duplicate a sub-term and increase the number of occurrences, but this increment is anticipated by the measure by means of the potential.

For proving that the measure decreases, we need some basic properties of the potential and of the measure plus some lemmas about their decomposition with respect to contexts.

*  if $\var\notin\fv\tm$ then $\potmul\tm\var =0 $.

*  if $\var\in\fv\tm$ then $\potmul\tm\var \geq 1$.

*  $\potmul\ctx\ctxhole \geq 1$.

*  $\ltmeas{\tm}\geq 1$.

$\ltmeas{\tm} = \ltmeas{\cutsub\mvartwo\mvar\tm}$.

Points 1, 2, 4, and 5 are easy inductions on $\tm$. Point 3 follows from Point 2, since, when looking at the hole $\ctxhole$ as a variable, one has $\ctxhole\in \fv\ctx$ for every context $\ctx$.

*  $\potmul{\ctxfp\tm}\var = \potmul\ctx\var + \potmul\ctx{\ctxhole}\cdot\potmul\tm\var$.

*  $\ltmeas{\ctxfp\tm} = \ltmeas\ctx + \potmul\ctx{\ctxhole}\cdot\ltmeas\tm$.

*  If $\ctx$ does not capture variables in $\fv\lctx$ and $\var\notin\fv\lctx$ then $\potmul{\ctxp{\lctxp\tm}}\var = \potmul{\ctxp{ \tm}}\var$.

If $\ctx$ does not capture $\evar$ and $\evartwo$ then:

*  Potential:
$\potmul{\ctxp{\dera\evar\var \tm}}\evar = \potmul{\ctxp{ \tm}}\evar + (1+\potmul\tm\var)\cdot\potmul\ctx\ctxhole$ and $\potmul{\ctxp{\dera\evartwo\var \tm}}\evar < \potmul{\ctxp{\dera\evar\var \tm}}\evar$.

*  Measure:
$\ltmeas{\ctxp{\dera\evar\var \tm}}>\ltmeas{\ctxp{\tm}}$ and $\ltmeas{\ctxp{\dera\evar\var \tm}} = \ltmeas{\ctxp{\dera\evartwo\var \tm}}$.

If $\mctx$ does not capture $\mvar$ then:

*  Potential:
$\potmul{\mctxp{\para\mvar\var\vartwo \tm}}\mvar = (1+ \potmul\tm\var + \potmul\tm\vartwo)\cdot\potmul\mctx\ctxhole$.

*  Measure:
$\ltmeas{\mctxp{\para\mvar\var\vartwo \tm}}> \ltmeas{\mctxp{\tm}}$.

The fourth point of the next lemma shall be used in the proof that the measure decreases for the the $\totens$ and $\tobder$ cases. The first three point are intermediate properties to obtain the fourth one.

Let $\ctx$ be a context that does not capture free variables in $\lctx$ nor $\val$, and $\lctx$ does not capture variables of $\tm$.

*  $\potmul{\lctxp{\cuta\val\var\tm}}\vartwo \leq \potmul{\tm}\vartwo +\potmul{\lctxp\val}\vartwo \cdot(1+\potmul\tm\var)$.

*  $\ltmeas{\lctxp{\cuta\val\var\tm}} \leq \ltmeas{\tm} +\ltmeas{\lctxp\val} \cdot(1+\potmul\tm\var)$.

*  $\potmul{\ctxp{\lctxp{\cuta\val\var\tm}}}\vartwo \leq \potmul{\ctxp{\tm}}\vartwo +\potmul{\lctxp\val}\vartwo \cdot(1+\potmul\tm\var)\cdot\potmul\ctx\ctxhole$.

*  $\ltmeas{\ctxp{\lctxp{\cuta\val\var\tm}}} \leq \ltmeas{\ctxp{\tm}} +\ltmeas{\lctxp\val} \cdot(1+\potmul\tm\var)\cdot\potmul\ctx\ctxhole$.

If $\tm \Rew{a} \tmtwo$ with $a\in\set{\axmone,\axmtwo,\tens,\axeone,\axetwo,\bdersym,\wsym}$ then $\ltmeas\tm > \ltmeas\tmtwo$.

Let $a \in \set{
\msym, \ems,\ess,\msnlolli, \ssnlolli}$. Then $\Rew{a}$ is strongly normalizing.

For $\toems$ and $\tomsnlolli$ it is an immediate consequence of the fact that the measure decreases (meas-decreases) and that it is always positive (potmul-propfour). The result is extended to $\toess$ and $\tossnlolli$ by full composition (ms-simulates-ss). For $\tom$, the statement is obvious, as at each step $\tom$ decreases the number of constructors.

The literature contains other partitions of linear logic cut elimination in strongly normalizing reductions: Danos <cit.> and Joinet <cit.> split it into axiom and non-axiom rewriting rules, Pagani and Tortora de Falco <cit.> into structural (a subset of exponential) and logical (non-structural). We are interested in the lolli/non-lolli partition because it mimics what happens in $\l$-calculi with ES, and also because of the future work described in the next step paragraph of the conclusions, for which the mentioned alternative partitions in the literature would not work.

Next Three independent topics follow: confluence (confluence), the good strategy (strategy), and strong normalization  (Sections <ref> and <ref>). They can be read in any order. First, however, we need to develop some technical tools for dealing with contexts in proofs.

§ SOME TECHNICALITIES

This section develops definitions and technical tools that are used in the proofs of the following sections to manage contexts, namely the outside-in order on contexts,
contexts with two holes (called double contexts), and a technical but important deformation lemma. At a first (or even second) reading, the reader can skip this section.

[Outside-in context order, disjoint contexts]
We define the partial outside-in order $\outer$ over contexts as follows:

$\ctxhole \outer \ctx$

$\ctx \outer\ctxtwo$
$\ctxthreep\ctx \outer \ctxthreep\ctxtwo$

And say that $\ctx$ is outer than $\ctxtwo$ if $\ctx\outer \ctxtwo$. If $\ctx\not\outer \ctxtwo$ and
$\ctxtwo\not\outer \ctx$ we say that $\ctx$ and $\ctxtwo$ are disjoint, and write $\ctx\parallel \ctxtwo$.

Double Contexts. Double contexts shall be used to compare two contexts on the same term. They have as base
cases binary constructors (that is, tensor pairs, cuts, and subtractions) having contexts replacing their subterms, and
as inductive cases they are simply closed by an ordinary context.
[Double contexts]
Double contexts $\cctx$ are defined by the following grammar.

\[\begin{array}{l@{\sep}llll}
\textsc{Double contexts} & \cctx& \defeq & \pair\ctx\ctxtwo \mid \suba\mvar\ctx\var\ctxtwo \mid \cuta\ctx\var\ctxtwo
\mid \ctxp\cctx
\end{array}\]

Some easy facts about double contexts.

* Plugging: the plugging $\cctxp{\tm,\tmtwo}$ of two terms $\tm$ and $\tmtwo$ into a double context $\cctx$
is defined as expected and gives a term. The two ways of plugging one term $\cctxp{\tm,\ctxhole}$ and
$\cctxp{\ctxhole,\tmtwo}$ into a double context give instead a context. We often use $\cctxp{\tm,\cdot}$ and
$\cctxp{\cdot,\tmtwo}$ as compact notations for $\cctxp{\tm,\ctxhole}$ and $\cctxp{\ctxhole,\tmtwo}$.

* Pairs of disjoint positions and double contexts: every pair of positions $\ctxp\tm=\ctxtwop\tmtwo$ which
are disjoint, that is, such that $\ctx \parallel\ctxtwo$, gives rise to a double context $\cctx_{\ctx,\ctxtwo}$ such
that $\cctx_{\ctx,\ctxtwo}\ctxholep{\cdot,\tmtwo} = \ctx$ and $\cctx_{\ctx,\ctxtwo}\ctxholep{\tm,\cdot} = \ctxtwo$.
Conversely, every double context $\cctx$ and every pair of terms $\tm$ and $\tmtwo$ gives rise to two context
$\cctx_{l}^{\tm,\tmtwo} \defeq \cctxp{\cdot, \tmtwo}$ and $\ctx_{r}^{\tm,\tmtwo} \defeq \cctxp{\tm,\cdot}$. Note that
the two constructions are inverse of each other, that is, given $\cctx$, we have
$\cctx_{\cctx_{l}^{\tm,\tmtwo},\ctx_{r}^{\tm,\tmtwo} } = \cctx$, and, conversely, given $\ctxp\tm=\ctxtwop\tmtwo$ we
have $(\cctx_{\ctx,\ctxtwo})_{l}^{\tm,\tmtwo} = \ctx$ and $(\cctx_{\ctx,\ctxtwo})_{r}^{\tm,\tmtwo} = \ctxtwo$.

$\ctxp{\cctxp{\tm,\cdot}} = \ctxp{\cctx}\ctxholep{\tm,\cdot}$ and $\ctxp{\cctxp{\cdot,\tm}} =
\ctxp{\cctx}\ctxholep{\cdot,\tm}$.

By induction on $\ctx$.

Deformation Lemma We need a set of deformation lemmas, collected together in
aux-props-loc-confl-strong-comm, that say what happens to a variable occurrence under the action
of a rewriting step: for instance, given a step $\mctxfp\mvar \toms \tmtwo$, one lemma states that $\tmtwo$ has shape $\mctxtwofp\mvar$ unless the step reduces a cut containing $\mvar$. The idea is that then $\mctxtwo$ is the residual of $\mctx$, but the statement(s) avoid using any form of residuals of steps, sub-terms, or constructors. The residual aspect is captured by specifying the preservation modulo a parameter—in
the case mentioned above, this is obtained stating that there is a step $\mctxfp\mval \Rew{a}
\mctxtwofp\mval$ for every $\mval$.

The deformation lemmas shall  be used in the following sections, namely in the proofs of local confluence (where preservation modulo a parameter is exploited), for the diamond property of the good strategy (for which the deformation lemmas shall have to be strengthened), and for the root cut expansion property (root-sn-expansion) at work in both the preservation of untyped strong normalization and typed normalization.

Let $\to\in\set{\toss,\toms}$.

Let $\ctx: \tm = \mctxfp\mvar \Rew{a} \tmtwo$ and $\Rew{a}$ be a $\to$ step. Then:

either $\tmtwo = \mctxtwofp{\mvar}$ for some
$\mctxtwo$ such that $\mvar\notin\fv\mctxtwo$ and there is a step $\ctxtwo_{\mval}: \mctxfp\mval \Rew{a}
\mctxtwofp\mval$ for every $\mval$,

* or $\mctx = \mctxtwop{\cuta\ctxhole\mvartwo\tmthree}$ for some
$\mctxtwo$ and $\ctx$ reduces the cut on $\mvartwo$.

Let $\ctx: \tm = \mctxfp{\tm_\mvar} \Rew{a} \tmtwo$ where $\tm_\mvar$ is a par or a subtraction of conclusion $\mvar$,
$\mctxtwo$ does not capture $\mvartwo$, and $\Rew{a}$ be a $\to$ step. Then  $\tmtwo = \mctxtwofp{\tmtwo_\mvar}$ where
$\tmtwo_\mvar$ is an occurrence of $\mvar$ of the same kind of $\tm_\mvar$,
$\mctxtwo$ does not capture $\mvar$ and $\mvar\notin\fv\mctxtwo$, and there is a step $\ctxtwo_{\mvartwo}:
\mctxfp{\cutsub\mvartwo\mvar \tm_\mvar} \Rew{a} \mctxtwofp{\cutsub\mvartwo\mvar \tmtwo_\mvar}$ for every fresh
multiplicative variable $\mvartwo$.

*  If $\ctx: \mctxp{\para\mvar\var\vartwo \tm} \Rew{a} \tmtwo$ is a
$\to$-step and $\mctx$ does not
capture $\mvar$ then
$\tmtwo = \mctxtwop{\para\mvar\var\vartwo \tm'}$ with $\mctxtwo$ not capturing $\mvar$ and
such that there is a step $\ctxtwo_{\ctxthree}: \mctxp{\ctxthreep\tm} \Rew{a} \mctxtwop{\ctxthreep{\tm'}}$ for every
context $\ctxthree$ capturing no more than $\var$ and $\vartwo$ in $\tm$ and such that $\mctx$ does not capture
variables of $\ctxthree$.

*  If $\ctx: \mctxp{\suba\mvar\val\var \tmfour} \Rew{a} \tmtwo$ is a
$\to$-step and $\mctx$ does not
capture $\mvar$ then either

* $\tmtwo = \mctxtwop{\suba\mvar\val\var \tmfour'}$ with
$\ctxtwo_{\ctxthree}:\mctxp{\ctxthreep\tmfour} \Rew{a}
\mctxtwop{\ctxthreep{\tmfour'}}$ for every context $\ctxthree$ capturing no more than $\var$ in $\tmfour$  and such
$\mctx$ does not capture in $\ctxthree$ more variables than those in $\fv\val$, or

* $\tmtwo = \mctxtwop{\suba\mvar\valtwo\var \tmfour}$ with $\ctxtwo_{\ctxthree}:\mctxp{\ctxthreep\val} \Rew{a}
\mctxtwop{\ctxthreep{\valtwo}}$ for every context $\ctxthree$ not capturing variables of $\val$ and such that $\mctx$
does not capture in $\ctxthree$ more variables than those in $\fv\tmfour \setminus\set{\var}$.

In both cases $\mctxtwo$ does not capture $\mvar$.

Let $\ctx: \tm = \ctxtwofp\evar \Rew{a} \tmtwo$ and $\Rew{a}$  be a $\toms$ step.  Then:

either $\tmtwo = \ctxtwo'\ctxholefp{\evar}$ for some
$\ctxthree$ such that there is a step $\ctx^\bullet_{\exval}:\ctxtwofp\exval \Rew{a} \ctxtwo'\ctxholefp\exval$ for

* or $\ctxtwo = \ctxthreep{\cuta\ctxfour\evartwo\tmthree}$ for some
$\ctxthree$ and $\ctxfour$, and $\ctx$ reduces a redex where the  active cut is the one on $\evartwo$.

Let $\ctx: \tm = \ctxtwop{\dera\evar\var\tmthree} \Rew{a} \tmtwo$ with $\ctxtwo$ not capturing $\evar$ and $\Rew{a}$
a $\toms$ step.  Then:

either $\tmtwo = \ctxtwo'\ctxholep{\dera\evar\var\tmthree'}$ for some
$\ctxtwo'$ such that there is a step $\ctx^\bullet_{\ctxthree}:\ctxtwop{\ctxthreep{\tmthree}} \Rew{a}
\ctxtwo'\ctxholep{\ctxthreep{\tmthree'}}$ for every $\ctxthree$ capturing no more than $\var$ in $\tmthree$ and

* or $\ctxtwo = \ctxthreep{\cuta\ctxfour\evartwo\tmthree}$ for some $\ctxthree$ and
$\ctxfour$, and $\ctx$ reduces a redex given by the cut on $\evartwo$.

The proof is by induction on the rewriting step in each point, and is a tedious check. In <cit.>, we give all the (many!) details for the first deformation property. The proofs of the others are minor variations.

§ UNTYPED CONFLUENCE

Here we prove confluence for the untyped ESC, using an elegant technique based on local diagrams and local termination. The technique is the Hindley-Rosen method. In our case, it amounts to prove that the multiplicative and exponential rules $\tom$ and $\toems$ are confluent separately, proved by local termination and Newman lemma, and commute, proved by local termination and Hindley's strong commutation. Confluence then follows by Hindley-Rosen lemma, for which the union of confluent and commuting reductions is confluent.

The Hindley-Rosen method is a modular technique often used for confluence of extensions of the $\l$-calculus, for instance in <cit.>. It is also used for untyped proof nets by Pagani and Tortora de Falco <cit.>.
Confluence for untyped proof nets is also proved by Danos <cit.> and Tranquilli <cit.> via finite developments. Essentially, local termination internalizes finite developments.

The Glitch For the untyped ESC there is a slight flaw due to clashes. The following local diagram, indeed, can be closed only if $\cuta\val\mvar$ is not a clashing cut (precisely, when $\val$ is not an exponential value nor an abstraction), or with cut equivalence $\cuteq$:

\cuta\val\mvar\mctxtwop{\cuta\mvar\mvartwo\mctxp{\para\mvartwo\var\vartwo\tm}}
\toaxmone
\mctxtwop{\cuta\val\mvartwo\mctxp{\para\mvartwo\var\vartwo\tm}}
\\
\downarrow_{\axmtwo}
\\
\cuta\val\mvar\mctxtwop{\mctxp{\para\mvar\var\vartwo\tm}}
\end{array}$

A second similarly problematic diagram is obtained by replacing the par with a subtraction.

Now, if there is a clash, the fact that confluence holds only up
to $\cuteq$ is irrelevant: the clash is a bigger issue. Moreover:

* (Recursive) types remove clashes: clashes are ruled out by our typing (clashfree-implies-cutfree), but also by recursive types such as those used for typing the untyped $\l$-calculus, or even the more general weak recursive typing considered by Ehrhard and Regnier in <cit.>.

* Proof nets are not better: because of weakenings, IMELL proof nets need jumps and jump rewiring rules. Confluence should then be proved up to jump rewiring, which is analogous to confluence up to $\cuteq$.

* Good steps are glitch-free: anticipating from the next section, the glitch does not affect good steps, as the $\axmone$ steps in the diagram above is bad.

The Proof We first prove the local properties.

* Multiplicative clash-free diamond:
$\tom$ is diamond on clash-free terms.

* Exponential local confluence: $\toess$ and $\toems$ are both
locally confluent.

In contrast to confluence, commutation of two reductions $\Rew{1}$ and $\Rew{2}$ does not follow from their local commutation and strong normalization. In our case however the rules verify Hindley's strong (local) commutation <cit.>, for which $\tmtwo_{1} \lRew{1} \tm \Rew{2} \tmtwo_{2}$ implies that there exists $\tmthree$ such that $\tmtwo_{1} \Rewn{2} \tmthree$ and either $\tmthree \lRew{1} \tmtwo_{2}$ or $\tmthree = \tmtwo_{2}$, that is, on one side of the commutation there are no duplications of steps. Strong commutation and strong normalization do imply commutation.

$\toess$ and $\toems$ both strongly commute over $\tom$.

Then we lift the local properties using local termination and conclude using Hindley-Rosen lemma.

The relations $\toss$ and $\toms$ are confluent on clash-free terms.

We deal with $\toms$, the reasoning for $\toess$ is identical. By Newman lemma, local confluence (loc-confluence) and local termination (local-termination) imply that $\tom$ and $\toess$ are confluent separately. By a result of Hindley <cit.>, strong commutation  (strong-commutation) and local termination imply that $\tom$ and $\toess$ commute. By Hindley-Rosen lemma, $\toms = \tom \cup \toems$ is confluent.

As it was mentioned at the end of towards, our micro-step rules for exponential axioms are different from the one at work in proof nets. The proof net micro-step rule, when formulated on terms, looks as a small-step rule:

$ \cuta\evartwo\evar\tm \ \  \to \ \ \cutsub\evartwo\evar\tm$

If considered with our other micro-step rules, in particular our $\tobder$, it generates a closable but unpleasant local confluence diagram:

\cuta{\bang\val}\evartwo \ctxp{\cuta\evartwo\evar \tm}
& \rtobder &
\cuta{\bang\val}\evartwo \ctxp{\cuta{\bang\val}\evar \tm}
\dasharrow_{\ems}^+
\cuta{\bang\val}\evartwo \ctxp{\cutsub{\bang\val}\evar \tm}

\\
\downarrow & &&&\dashdownarrow_{\ems+}

\\
\cuta{\bang\val}\evartwo \ctxp{\cutsub\evartwo\evar \tm}
& \dasharrow_{\ems}^+ &
\cutsub{\bang\val}\evartwo \ctxp{\cutsub\evartwo\evar \tm}
& = &
\cutsub{\bang\val}\evartwo \ctxp{\cutsub{\bang\val}\evar \tm}
\end{array}$

In order to close the local diagram one needs to fully develop some exponential cuts (note $\dasharrow_{\ems}^+$), which is a small-step concept and not a micro-step one. This is why we adopt different axiom rules, for which local confluence diagrams never need small-step developments.

§ THE GOOD STRATEGY

In this section, we define the good cut elimination strategy $\tog$ for the untyped ESC, show various of its properties, including the sub-term property, and prove that it provides a polynomial cost model.

Breaking the Sub-Term Property When does the sub-term property not hold? One has to duplicate an exponential value $\exval$ touched by previous steps. In our setting, touched can mean two things. Either a redex fully contained in $\exval$ is reduced, obtaining $\exvaltwo$, and then $\exvaltwo$ is duplicated (or erased), as in the step marked with $\bigstar$ in the following diagram (the other, dashed path of which has the sub-term property):

\cuta{\exval} \evar \ctxfp{\evar}
&& \toms &&
\cuta{\exvaltwo} \evar \ctxfp{\evar}
\\
\dashdownarrow_{\axeone}&& & &\downarrow_{\axeone} \bigstar
\\
\cuta{\exval}\evar\ctxfp{\exval}
& \dashrightarrow_{\mssym} &
\cuta{\exvaltwo} \evar \ctxfp{\exval}
& \dashrightarrow_{\mssym} &
\cuta{\exvaltwo}\evar\ctxfp{\exvaltwo}
\end{array}$

The other way of touching $\exval$ is when a cut $\cuta{\exvaltwo} \evar$ external to $\exval$ acts on some exponential variable $\evar$ in $\exval=\vctxfp\evar$:

\[\arraycolsep=1pt\footnotesize\begin{array}{cccccccc}
\cuta{\exvaltwo} \evar \ctxp{\cuta{\vctxfp\evar} \evartwo \ctxtwofp{\evartwo}}
&& \rtoaxeone &&
\cuta{\exvaltwo} \evar \ctxp{\cuta{\vctxfp\exvaltwo} \evartwo \ctxtwofp{\evartwo}}
\\
\dashdownarrow_{\axeone} & &&&\downarrow_{\axeone} \bigstar
\\
\cuta{\exvaltwo} \evar \ctxp{\cuta{\vctxfp\evar} \evartwo \ctxtwofp{\vctxfp\evar}}
& \dashrightarrow_{\axeone} &
\cuta{\exvaltwo} \evar \ctxp{\cuta{\vctxfp\exvaltwo} \evartwo \ctxtwofp{\vctxfp\evar}}
& \dashrightarrow_{\axeone} &
\cuta{\exvaltwo} \evar \ctxp{\cuta{\vctxfp\exvaltwo} \evartwo \ctxtwofp{\vctxfp\exvaltwo}}
\end{array}\]

Similar diagrams can be obtained using $\tobder$ rather than $\toaxeone$, and these are all the local confluence diagrams for $\toms$ that are not squares nor triangles (see loc-confluence and strong-commutation).

Preventing these situations from happening, thus forcing evaluation to follow the other side of the diagram, is easy. It is enough to forbid the position of the redex to be inside the left sub-term of a cut—we say inside a cut value for short. It is however not enough, because cuts are also created. Consider:

\begin{array}{clllllcl}
\cuta{\la\evar\pair\evar\evar}\mvar\suba\mvar\exval\var\tm &\toms&
\cuta{\la\evar\pair\evar\evar}\mvar\suba\mvar\exvaltwo\var\tm &\tololli
\\
&&\cuta\exvaltwo\evar\cuta{\pair\evar\evar}\var\tm &\overset\bigstar\rightarrow_{\axeone} &
\cuta\exvaltwo\evar\cuta{\pair\exvaltwo\evar}\var\tm
\end{array}

Reducing inside the subtraction value $\exval$ leads to a later breaking of the sub-term property by the $\axeone$ step, because the $\tololli$ step creates a cut with $\exvaltwo$ inside.
Preventing these cases is tricky, because forbidding reducing subtraction values leads to cut elimination stopping too soon, without producing a cut-free term. In the $\l$-calculus, it corresponds to forbidding reducing inside arguments, which leads to head reduction, that does not compute normal $\l$-terms. We shall then forbid reducing only subtraction values which are at risk of becoming cuts. It might look like the dangerous positions are those in $\val$ in $\cuta\mval\mvar\mctxp{\suba\mvar\val\var\tm}$, i.e. those where the surrounding subtraction is involved in a cut. They are in fact more general. Consider the positions inside $\val$ in $\tm$ here:

$\tm\ =\ \cuta{\bang\mval}\evar\dera\evar\mvar\suba\mvar\val\var\tmtwo\ \tobder\ \cuta{\bang\mval}\evar\cuta\mval\mvar\suba\mvar\val\var\tmtwo$

they are also dangerous, because they reduce to those of the previous kind. Therefore, we need to ensure that the conclusion $\mvar$ of the subtraction is not hereditarely involved  in a cut. The key notion is the one of dominating (free) variables $\dfv\ctx$ of a context (where $\ctx$ is meant to be the position of a redex), in strategy, the base case of which is for $\suba\mvar\vctx\var\tm$. If $\ctx$ is a position and $\var\in\dfv\ctx$ then $\cuta\val\var\ctx$ turns $\ctx$ into a dangerous position, that is, a redex of position $\cuta\val\var\ctx:\tm\toms\tmtwo$ might lead to a breaking of the sub-term property later on during cut elimination. In the last example, $\evar$ dominates the context $\dera\evar\mvar\suba\mvar\vctx\var\tmtwo$ of $\dera\evar\mvar\suba\mvar\val\var\tmtwo$ for every $\vctx$.

Good and Bad Contexts and Steps The previous considerations  lead to the notions of good and bad contexts in strategy. A good context forbids the two ways of breaking the sub-term property: its hole cannot be in a cut value (note the absence of the production $\cuta{\vgctx}\var\tm$) nor in a subtraction value such that one of its dominating variables is cut (because of the production $\cuta\val\var\gctx$ if $\var\notin\dfv\gctx
$). Every other step is allowed. The next lemma ensures that bad and good contexts are indeed complementary concepts.

Let $\ctx$ be a context. Then $\ctx$ is either good or bad.

By induction on $\ctx$. The empty context $\ctxhole$ is good and not bad. For all inductive cases but cut, it follows from the The cut cases:

* $\ctx = \cuta\vctx\var\tm$. Then $\ctx$ is bad and not good.

* $\ctx = \cuta\val\var\ctxtwo$. By , $\ctxtwo$ is either good or bad. If $\ctxtwo$ is bad then $\ctx$ is bad, and $\ctx$ is not good because $\ctxtwo$ is not good. If $\ctxtwo$ is good, consider whether $\var\in \dfv\ctxtwo$. If it does, then $\ctx$ is bad and not good. If instead  $\var\notin \dfv\ctxtwo$ then $\ctx$ is good and not bad.

[Good/bad step, good strategy]
A micro step $\ctx : \tm \toms \tmtwo$ is good if its position $\ctx$ is good. In such a case, we write $\tm \tog \tmtwo$. The good cut elimination strategy is simply $\tog$. A step $\tm \toms \tmtwo$ is bad if it is not good, and we then write $\tm\tobad \tmtwo$. We also use $\togp a$ and $\tobadp a$ to stress that the good/bad step is of kind $a\in\set{\axmone,\axmtwo,\tens,\lolli, \axeone,\axetwo,\bdersym,\wsym}$.

A Technical Remark About Goodness The notions of good and bad steps are inherently micro-step, as the next example shows. Consider the following term:

\[\tm \defeq \cuta{\evartwo}\evar \dera\evar\evarthree \cuta\mvarthree\mvar \suba\mvar\evar\mvartwo \mvartwo\]

In $\tm$, the cut $\cuta{\evartwo}\evar$ gives rise to two redexes, one for each occurrence of $\evar$. The redex concerning $\dera\evar\evarthree$ is good while the one concerning $\suba\mvar\evar\mvartwo $ is bad, because its position $\cuta{\evartwo}\evar \dera\evar\evarthree \cuta\mvarthree\mvar  \suba\mvar\ctxhole\mvartwo \mvartwo$ is a bad context ($\mvar$ dominates the hole, and there is a cut on $\mvar$). Thus, being good/bad is not a property of the cut $\cuta{\evartwo}\evar$, that is, it is not a small-step property, because not all the micro-step redexes in which a cut is involved share the same character. Consider now:

\[\tm \defeq \cuta{\evartwo}\evar \dera\evar\mvar \suba\mvar\evar\mvartwo \mvartwo\]

In $\tm$, again, there are two redexes on $\evar$, a good one and a bad one. The difference is that now it is the good occurrence of $\evar$ that turns the other occurrence into a bad one (by dominating $\mvar$, which dominates the second occurrence).

Basic Properties of Good Contexts. The next three lemmas collect basic facts about good contexts that are used in the proof of the rest of the section.

Let $\ctxp\ctxtwo$ be a good context. Then $\ctx$ and $\ctxtwo$ are good contexts.

Let $\gctxp\tm= \bctxp\tmtwo$. Then $\bctx\not\outer\gctx$, that is, either $\gctx\outer\bctx$ or $\gctx \parallel \bctx$.

By induction on $\gctx$. Note that $\bctx$ cannot be empty, otherwise it would be good. Cases:

* $\gctx = \ctxhole$. Then $\tm = \bctxp\tmtwo$ and so $\bctx\not\outer \gctx$.

* The abstraction, bang, par, and dereliction cases follow from the
* $\gctx = \pair\gctxthree\tmthree$. If $\bctx = \pair\bctxtwo\tmthree$ then it follows from the If $\bctx = \pair\tmfour\bctxtwo$ then $\bctx \not\outer \gctx$.

* The subtraction case is as the tensor case.

* $\gctx = \cuta\val\var\gctxtwo$. If $\bctx = \cuta\val\var\bctxtwo$ it follows from the If $\bctx = \cuta\bctxtwo\var\tmthree$ then $\bctx \not\outer \gctx$.

Let $\cctx$ be a double context and $\tm$ and $\tmtwo$ be two terms. Then:

* $\cctxp{\cdot,\tm}$ is as capturing as $\cctxp{\cdot,\tmtwo}$;

* $\dfv{\cctxp{\cdot,\tm}} = \dfv{\cctxp{\cdot,\tmtwo}}$;

* $\cctxp{\cdot,\tm}$ is good if and only if $\cctxp{\cdot,\tmtwo}$ is good.

Note that the last point of double-ctx-repl could have be equivalently stated with respect to being bad.

By induction on $\cctx$. The base cases are straightforward, and the inductive cases follow from the In the inductive case $\cctx = \cuta\val\var\cctxtwo$, the third point uses the second one.

Sub-Term Property. We are ready for the key point of the paper, the sub-term property of the good strategy. The proof is based on a natural local invariant about bad values, which are the sub-terms at risk of being duplicated or erased.
[Bad values]
Given $\tm = \ctxp\val$, $\val$ is a bad value of $\tm$ if $\ctx$ is a bad context.

The local invariant shows that one good step cannot create bad values. Since strict equality of sub-terms is not preserved by reduction (because of on-the-fly $\alpha$-renaming), the invariant concerns the size of bad values, which is what is important for cost analyses. The sub-term property follows by induction on the length of cut elimination sequences.

*  If $\ctxp{\cuta\val\var\ctxtwo}$ is good then $\ctxp{\ctxtwo}$ is good.

* If $\ctxp{\ctxtwo}$ is bad then $\ctxp{\cuta\val\var\ctxtwo}$ is bad.

Point 1 is by induction on $\ctx$. Since a context is either good or bad (good-bad-partition), Point 2 is simply the contrapositive of Point 1.

Let $\tm \tog \tmtwo = \bctxp\val$. Then $\tm = \bctxtwop\valtwo$ for some $\bctxtwo$ and $\valtwo$ such that $\size\val = \size\valtwo$.

Let $\tm \tog^{*} \tmtwo$ and $\val$ be a bad value of $\tmtwo$. Then $\size\val\leq \size\tm$.

By induction on the length $k$ of the reduction $\tm \tog^{k} \tmtwo$. If $k=0$ then the statement trivially holds. If $k>0$ then  consider the last step $\tmthree \tog \tmtwo$ of the sequence. By the local sub-term property (local-sub-tm), the size of every bad value $\val$ of $\tmtwo$ is bound by the size of a bad value $\valtwo$ of $\tmthree$, which by satisfy the statement.

Good Diamond The good strategy is not deterministic, as for instance if $\tm \tog \tmtwo$ then:

\pair\tmtwo\tm\ \ \lRew{\Gsym}\ \ \pair\tm\tm \ \ \tog \ \ \pair\tm\tmtwo$.

Note also, however, that the local diagrams that are not squares nor triangles are forbidden by design for good steps (see above). Triangles are also forbidden: it is easily seen that they all involve touching the cut value of a $\tobw$ step, which is bad. Then all local diagrams for good steps are squares.

$ \tmtwo_{1} \lRew{\Gsym}\tm \tog \tmtwo_{2}$ and $\tmtwo_{1} \neq \tmtwo_{2}$ then $ \tmtwo_{1} \tog \tmthree \lRew{\Gsym}  \tmtwo_{2}$ for some $\tmthree$.

Two well known consequences of being diamond are uniform normalization, that is, if there is a normalizing reduction
sequence then there are no diverging sequences, and random
descent, that is, when a term is normalizable, all sequences to
normal form have the same length. Being diamond
is then a relaxed form of determinism. These properties are essential for the study of cost models, as otherwise the number of steps of the strategy is an ambiguously defined measure.

Fullness. The sub-term property expresses the correctness of our design. We need to prove a simple form of completeness, ensuring that the good strategy does not stop when there is still work left to do. This is given by fullness, that is, the fact that as long as $\tm$ is not normal then $\tm$ has a good redex. We need to assume that $\tm$ has no clashes, because terms with clashes such as $\cuta{(\cuta\evar\evartwo\evartwo,\evar)}\mvar \suba\mvar\evar\mvartwo\mvartwo$, where the tensor pair and the subtraction clash, are not normal (note that $\cuta\evar\evartwo\evartwo$ is a redex) but have no good redexes, as all their redexes are inside cut values of clashing cuts.

We recall that an occurrence of $\var$ in $\tm$ is given by a position $\tm = \ctxp{\tm_{\var}}$  where $\tm_{\var}$ is a sub-term of $\tm$ of shape $\var$, $\para\var\vartwo\varthree\tmtwo$, $\suba\var\val\vartwo\tmtwo$, or $\dera\var\vartwo\tmtwo$. Note that the shapes of $\tm_{\var}$ are the kind of terms with which a cut on $\var$ can interact at a distance to form a redex.

[Outermost variable occurrence]
An occurrence $\tm = \ctxp{\tm_{\var}}$ of $\var$ in $\tm$ is outermost if $\ctxtwo \not\outer\ctx$ for all other occurrences $\tm = \ctxtwop{\tm'_{\var}}$ of $\var$.

Let $\tm = \ctxp{\tm_{\var}}$ be an outermost occurrence of $\var$ in $\tm$ with $\ctx$ not capturing $\var$. Then $\var \notin\dfv\ctx$.

By induction on the number $\sizep\ctx\var$ of free occurrences of $\var$ in $\ctx$. If $\sizep\ctx\var = 0$ then $\var\notin \fv\ctx \supset \dfv\ctx$. If $\sizep\ctx\var > 0$ consider another occurrence $\ctxtwop{\tm_{\var}'}$ of $\var$ in $\tm$ such that $\ctx\not\outer\ctxtwo$, which exists because $\sizep\ctx\var > 0$ (indeed if $\ctx\outer\ctxtwo$ then $\tm_{\var}'$ is a sub-term of $\tm_{\var}$ and does not contribute to $\sizep\ctx\var$). Since $\tm_{\var}$ is outermost, we have $\ctxtwo \parallel \ctx$. Now, consider the double context $\cctx_{\ctx,\ctxtwo}$ such that $\cctx_{\ctx,\ctxtwo}\ctxholep{\cdot, \tm_{\var}'}=\ctx$ and $\cctx_{\ctx,\ctxtwo}\ctxholep{\tm_{\var},\cdot}=\ctxtwo$. By double-ctx-repl, the context $\ctxthree \defeq \cctx_{\ctx,\ctxtwo}\ctxholep{\cdot, \la\mvar\mvar}$ verifies $\dfv\ctxthree = \dfv\ctx$ and $\sizep\ctxthree\var \leq \sizep\ctx\var -1$. Then by we have $\var\notin\dfv\ctxthree = \dfv\ctx$.

Let $\var\in\dfv\ctx$.  Then one of the following cases hold:

* $\ctx = \mctxp{\para\mvar\vartwo\varthree\ctxtwo}$ and $\var = \mvar$;

* $\ctx = \mctxp{\suba\mvar\val\vartwo\ctxtwo}$ and $\var = \mvar$;

* $\ctx = \mctxp{\suba\mvar\vctx\vartwo\tm}$ and $\var = \mvar$;

* $\ctx = \ctxtwop{\dera\evar\vartwo\ctxthree}$, $\var = \evar$, and $\evar \notin\dfv\ctxtwo$.

The first three points are simply the observation that if $\var=\mvar$ is multiplicative and $\mvar\in\dfv\ctx$ then

* $\mvar\in\fv\ctx$ and so the position of $\mvar$ has to be a multiplicative context $\mctx$;

* the occurrence has to be a par or subtraction occurrence by definition of $\dfv\ctx$ (that is, it cannot be a variable occurrence).

The fourth point is similar but it says something more so we need a bit more. It is by induction on $\ctx$. If $\var=\evar$  is exponential and $\evar\in\dfv\ctx$ then $\ctx = \ctxtwo'\ctxholep{\dera\evar\vartwo\ctxthree'}$. Now, if $\evar\notin\dfv{\ctxtwo'}$ the statement holds with $\ctxtwo \defeq \ctxtwo'$. Otherwise, by , $\ctxtwo' = \ctxtwo''\ctxholep{\dera\evar\varthree\ctxthree''}$ with $\evar\notin\dfv{\ctxtwo''}$. Then $\ctx =  \ctxtwo''\ctxholep{\dera\evar\varthree\ctxthree''\ctxholep{\dera\evar\vartwo\ctxthree'}}$, which satisfies the statement with respect to $\ctxtwo \defeq \ctxtwo''$.

Let $\tm$ be clash-free. If $\tm$ is not $\toms$-normal then $\tm \tog\tmtwo$ for some $\tmtwo$.

Summing Up. Together with typed strong normalization (from SN), the properties of the good strategy imply our main result.

Let $\multiform\vdash \tm\hastype \form$ be a typed term. Then there exist  $k$ and a cut-free term $\tmtwo$ such that $\tm \tog^{k} \tmtwo$. Moreover, such a reduction sequence is implementable on a random access machine in time polynomial in $k$ and $\size\tm$.

By typed strong normalization (sn), $\tog$ terminates on $\tm$, let $\tmtwo$ be its $\tog$ normal form. Since typable implies clash-freeness (clashfree-implies-cutfree), $\tm$ is clash-free, and thus so is $\tmtwo$. By fullness (good-fullness) and $\tog$ normality, $\tmtwo$ is $\toms$-normal, which with clash-freeness implies that it is cut-free (clashfree-implies-cutfree).

Now, about the cost. Let $\tm = \tm_{0} \tog \tm_{1} \tog\ldots \tog \tm_{k} = \tmtwo$. All steps $\tm_{i} \tog \tm_{i+1}$ of the sequence that are multiplicative, as well as all $\toaxetwo$ step, do only manipulation of a constant number of constructors of the term. Therefore, they can clearly be implemented in time polynomial in $\size{\tm_{i}}$, as searching for a redex and checking that its position is good are clearly polynomial problems, and there is at most a linear number of redexes in a term. By a straightforward induction using the sub-term property (sub-term-prop), one obtains that $\size{\tm_{i}} \leq i\cdot\size{\tm_{0}}$, and so all those steps have  cost polynomial in $k$ and $\size{\tm_{0}}$. Again by the sub-term property, the cost of duplication/erasure of values in non-linear steps (namely, $\toaxeone$, $\tobder$, and $\tobw$ steps) is bound by $\tm_{0}$, so they have polynomial cost in $k$ and $\size{\tm_{0}}$ as well.

About the degree of the polynomial, Accattoli et al. <cit.> show that strategies with the sub-term property are usually implementable via abstract machines in time linear in both $k$ and $\size\tm$. We expect the linear bound to hold here as well, but we leave the design of an abstract machine to future work.

§ UNTYPED PRESERVATION OF STRONG NORMALIZATION

In the ES literature, the crucial property for a calculus with ES is preservation of $\beta$ strong normalization (shortened to PSN) on untyped terms, that is, that if a $\l$-term is $\sn\beta$ then it is SN when evaluated with ES. In our setting, it is rephrased as $\tm\in\sn\toss$ implies $\tm\in\sn\toms$. The property ensures that switching to micro-steps does not introduces unexpected divergence, as it was surprisingly the case, historically, for the first $\l$-calculus with ES by Abadi et al. <cit.>, as shown by <cit.>.

Proofs of PSN are often demanding, see Kesner's survey <cit.>. Contextual rewriting rules enable instead short proofs, as first showed by Accattoli and Kesner <cit.>. We adapt and further simplify that proof, that here rests on just two natural properties of micro steps, here referred to as extension and root cut expansion (Kesner calls the latter IE property), the latter making use of structural stability, that is, the fact that cut equivalence preserves SN (cuteq-bisimsn). The properties are actually also used for strong normalization in the next section, where they are used for $\toss$, which is why the statements concern both $\toms$ and $\toss$.

Extension. The extension property is the easy fact that, for all root constructs but (non clashing) cuts, SN follows from SN of the root sub-terms.

Let $\to\in\set{\toss,\toms}$ and $\tm, \tmtwo, \val \in \snsubst$.

* Neutral:
$\pair\tm\tmtwo$, $\la\var\tm$, $\bang\tm$, $\para\mvar\var\vartwo \tm$,  $\suba\mvar\val\var  \tm$, and $\dera\evar\var \tm$ are in $\snsubst$;

* Clash: if the root cut of $\cuta\val\var\tm$ is clashing then $\cuta\val\var\tm\in\snsubst$.

Root Cut Expansion. The root cut expansion property is the less obvious fact that if the reduct of a root small-step cut is $\sn\toms$ then the reducing term also is. Kesner isolated the importance of this property for PSN <cit.>, calling it IE property. Accattoli and Kesner <cit.> show that, with rules at a distance, it is proved via simple inductions (here even simpler than in <cit.> thanks to LSC-style duplication and structural stability), while commutative rules (such as Girard's box commutation $\Rew{\boxbox}$ for proof nets) break those inductions and require more complex techniques.

Let $\to\in\set{\toss,\toms}$

* Multiplicative: if $\tm \rtom \tmtwo$ and $\tmtwo\in \sn\to$ then $\tm\in\sn\to$.

* Exponential:
if $\exval\in\sn\to$ and $\cutsub\exval\evar\tm\in\sn\to$ then
$\cuta{\exval}\evar \tm \in\sn\to$.

PSN Now, PSN is proved via a very easy induction over $\tm\in\sn\toss$ and the size $ \size\tm$ of $\tm$, using the two properties.

If $\tm\in\sn{\toss}$ then $\tm\in\sn{\toms}$.

The next section proves typed SN for $\toss$, which then transfers to $\toms$ by PSN. The relevance of PSN, however, is that it holds in the untyped setting, thus it transfers SN also if proved with respect to other type systems, such as intersection types, polymorphic types, and so on.

§ TYPED STRONG NORMALIZATION

Here we prove strong normalization of the IMELL-typed small-step ESC (then transferred to the micro-step ESC by PSN)
using the reducibility method. We do it following the bi-orthogonal schema for proof nets  by Girard
<cit.>, see also Pagani and Tortora de Falco <cit.>. We actually
adopt here the variant by Accattoli <cit.>, the main point of which is that without
commutative exponential rules (as it is also the case here) there is a simpler proof of adequacy (the key step of
the method) based on the root cut expansion property of the previous section. There are 3 differences between the
present proof and <cit.> (beyond a neater technical development here):

* Formal: the study in <cit.> uses proof nets and an informal term notation
with explicit and meta-level substitutions. That informal notation is here replaced by a formal one, the ESC;

* Exponential rules: both studies use rules without commutative cases, but here we use LSC-style
duplications, obtaining a simpler proof of root cut expansion.

* Quotient $vs$ cut equivalence: the quotient on proofs given by proof nets plays a subtle role in the proof
of adequacy. The argument is here  replaced by the stability by cut equivalence $\cuteq$ of strong normalization.

We are also inspired by Riba's dissection of reducibility <cit.>, and refer to
<cit.> for extensive discussions and references about strong normalization in linear logic.
To our knowledge, the literature contains only two studies of strong normalization for a linear term calculus:

* Benton <cit.>, who, as he points out, does not deal with commutative cases—that are
nonetheless crucial in his presentation—thus not really proving strong normalization;

* Pérez et al. <cit.>, where cut elimination is seriously restricted because they
use it to model process communication, which does not take place under prefixes. Logically, it means that their notion
of cut elimination does not compute cut-free proofs.

Key Properties. The reducibility method requires a number of definitions. From a high-level perspective,
however, our proof is based on three key properties of $\toss$:

* Structural stability: if $\tm\in\sn\toss$ and $\tm\cuteq\tmtwo$ then $\tmtwo\in\sn\toss$

* Extension (extension), and

* Root cut expansion (root-sn-expansion).

Since they hold also for micro-step cut elimination $\toms$, our proof works with only minor changes also for
micro-steps, without really needing PSN.

Elimination Contexts and Duality.
Elimination contexts are multiplicative contexts of the form $\lctxp{\cuta{\ctxhole}\var\tm}$, noted $\elctx$. They can
be typed
by considering $\ctxhole$ as a free variable and typing it via an axiom, as follows:

$  \ctxhole\hastype\form \vdash \ctxhole\hastype \form$

Let us set some notations:

* $\lltermsform$ for the set of terms $\tm$ of type $\form$, that is, such that $\multiForm\vdash \tm\hastype\form$,
and also  $\vars_{\form} \defeq  \lltermsform \cap \vars$.

* $\elctxsform \defeq \set{\elctx \
|\ \multiForm, \ctxhole\hastype \form \vdash \elctx\hastype \formtwo}$ the set of typed elimination contexts with hole
of type $\form$, and say that $\elctx$ has co-type $\form$.

* $\elvars_{\form} \defeq \set{\elctx\in\elctxsform \ |\  \elctx = \cuta\ctxhole\var\var}$.

* $\elctx \in \sn\toss$ if $\elctx = \lctxp{\cuta\ctxhole\var\tm}$ and $\lctxp{\cutsub\vartwo\var\tm}\in\sn\toss$
for every variable $\vartwo$ of the same kind as $\var$ which is not captured by $\lctx$.

Checking that $\elctx=\lctxp{\cuta\ctxhole\var\tm}$ is in $\sn\toss$ amounts to prove that

$\lctxp{\cutsub\vartwo\var\tm} = \cutsub\vartwo\var\lctxp{\tm}\in\sn\toss$ for every appropriate $\vartwo$. By the stability of SN by renamings (deformationssn), it is enough to prove that $\lctxp{\tm}\in\sn\toss$.

Given a set $\settone \subseteq \lltermsform$ of terms of type $\form$, the dual set
$\settone^\bot\subseteq\elctxsform$ contains the elimination contexts $\elctx$ of co-type
$\form$ such that  $\elctxfp{\tm}$ is and in $\sn\toss$ for every
$\tm\in\settone$. The dual of a set of elimination contexts $\setecone \subseteq\elctxsform$ of co-type $\form$ is
defined analogously.

Note the
use of $\ctxholef$ in the definition of duality: the plugging in contexts at work in duality does not capture the variables of the plugged
term, this is crucial, and standard in the reducibility method.

The following properties of duality are standard.

If $\settone \subseteq \lltermsform$ or $\settone\subseteq\elctxsform$ then:

* Closure: $\settone\subseteq\settone^{\bot\bot}$;

* Bi-orthogonal: $\settone^{\bot\bot\bot}=\settone^{\bot}$.

Generators, Candidates, and Formulas. The definition of reducibility candidates comes together with a notion
of generator, justified by the proposition that follows (which requires an auxiliary lemma).

[Generators and candidates]
A generator of type $\form$ (resp. co-type $\form$) is a sub-set $\settone\subseteq\lltermsform$ (resp.
$\settone\subseteq\elctxsform$) such that:

* Non-emptyness: $\settone \neq \emptyset$, and

* Strong normalization: $\settone\subseteq \sn\toss$.

A generator $\settone$ of type $\form$ (resp. co-type $\form$) is a candidate if

* Variables: $\vars_{\form}\subseteq \settone$ (resp. $\elvars_{\form}\subseteq \settone$), and

* Bi-orthogonal: $\settone=\settone^{\bot\bot}$.

Let $\tm \in \lltermsform$ and $\elctx \in \elctxsform$.

If $\elctxfp\tm\in\sn\toss$ then $\tm \in \sn\toss$ and $\elctx\in\sn\toss$.

If $\tm \in \sn\toss$ and $\elctx \in \elvars_{\form}$ then $\elctxfp\tm\in \sn\toss$.

If $\elctx \in \sn\toss$ and $\vartwo \in \vars_{\form}$ then $\elctxfp\vartwo\in \sn\toss$.

* By induction on $\elctxfp\tm\in\sn\toss$. Let $\tm = \lctxp\val$ and $\elctx =
\lctxtwop{\cuta\ctxhole\var\tmtwo}$, so that $\elctxfp\tm = \lctxtwop{\lctxp{\cuta\val\var\tmtwo}}$. The proof of the
statement is based on the obvious fact that every step from $\tm$ or $\lctxtwop\tmtwo$ (we rely on sn-renaming)
can be mimicked on $\lctxtwop{\lctxp{\cuta\val\var\tmtwo}}$, so that one can then apply the

* If $\elctx \in \elvars_{\form}$ then $\elctx = \cuta\ctxhole\var\var$. Let $\tm = \lctxp\val$. We  have to