# Linear Additives

Gianluca Curzi University of Turin
Torino, Italy<EMAIL_ADDRESS>
###### Abstract

We introduce $\mathsf{LAM}$, a subsystem of $\mathsf{IMALL}_{\\_}2$ with
restricted additive rules able to manage duplication linearly, called linear
additive rules. $\mathsf{LAM}$ is presented as the type assignment system for
a calculus endowed with copy constructors, which deal with substitution in a
linear fashion. As opposed to the standard additive rules, the linear additive
rules do not affect the complexity of term reduction: typable terms of
$\mathsf{LAM}$ enjoy linear strong normalization. Moreover, a mildly weakened
version of cut-elimination for this system is proven which takes a cubic
number of steps. Finally, we define a sound translation from $\mathsf{LAM}$’s
proofs into $\mathsf{IMLL}_{\\_}2$’s linear lambda terms, and we study its
complexity.

##  1 Introduction

Linear Logic ($\mathsf{LL}$) is a refinement of both classical and
intuitionistic logic introduced by Girard in [14]. A central role in
$\mathsf{LL}$ is played by the exponential modalities $\oc$ and $\wn$, which
give a logical status to the structural rules of weakening and contraction.
The exponentials allow us to discriminate between linear resources, consumed
exactly once, and non-linear resources, reusable at will. Moreover, since the
uncontrolled use of the structural rules is forbidden, conjunction and
disjunction come with two distinct presentations: the multiplicative version
(resp. $\otimes$ and $\parr$) and the additive one (resp. $\with$ and
$\oplus$).

The presence of multiple formulations of the same connective has prompted the
analysis of specific _fragments_ of Linear Logic, i.e. subsystems of
$\mathsf{LL}$ that illustrate the behavior of a specific group of connectives.
The simplest fragment of $\mathsf{LL}$ is $\mathsf{MLL}$ (Multiplicative
Linear Logic), i.e. the modal-free subsystem of $\mathsf{LL}$ with inference
rules for $\otimes$, $\parr$. Another one is $\mathsf{MALL}$ (Multiplicative
Additive Linear Logic), obtained by extending $\mathsf{MLL}$ with additive
rules, i.e. the inference rules for $\with$, $\oplus$.

As pointed out in [20], according to the “computation-as-normalization”
paradigm, the additive rules of $\mathsf{LL}$ can be used to express non-
deterministic program executions. This intuition has been further investigated
in the field of ICC (Implicit Computational Complexity), a branch of
computational complexity devising calculi that abstract from machine models
and characterize complexity classes without imposing “external” resource
bounds. In this setting, several variants of the additive rules able to
express non-deterministic computation more explicitly have been proposed to
capture the class $\mathsf{NP}$. Examples are [20, 12, 21], all based on
_light logics_ , i.e. subsystems of (second-order) $\mathsf{LL}$ with weaker
exponential rules that induce a complexity bound on proof normalization.

Using variants of the additive rules to characterize the non-deterministic
polytime problems raises some issues, because these inference rules affect the
complexity of cut-elimination/normalization, which may require an exponential
cost. A standard approach to circumvent this fact is to focus on a specific
cut-elimination strategy called lazy [13], which “freezes” those commuting
cut-elimination steps that involve duplication of (sub)proofs. A similar
technique can be found in [12], where the type system $\mathsf{STA}_{\\_}+$ is
introduced to capture the complexity class $\mathsf{NP}$ in the style of ICC.
$\mathsf{STA}_{\\_}+$ extends Soft Type Assignment [11] with the sum rule
below

$\Gamma\vdash M:A$ $\Gamma\vdash N:A$ $sum$ $\Gamma\vdash M+N:A$ (1)

and the non-deterministic reductions $M\leftarrow M+N\rightarrow N$ for the
choice operator $+$. The sum rule is close to the additive rules, and suffers
the same drawbacks. Consequently, to prove that $\mathsf{STA}_{\\_}+$ is sound
for $\mathsf{NP}$, a particular reduction strategy is needed to avoid
exponential computations.

In this paper we present a different solution to the complexity-theoretical
issues caused by the additive rules. We start focusing on the second-order
intuitionistic formulation of $\mathsf{MALL}$, i.e. $\mathsf{IMALL}_{\\_}2$.
We shall look at the latter as a type system, essentially by considering
formulas as types and by decorating logical derivations with $\lambda$-terms
endowed with pairs and projections. The analysis of the non-linear features of
the additive rules leads to the new type system $\mathsf{LAM}$ (Linearly
Additive Multiplicative Type Assignment). This is a subsystem of
$\mathsf{IMALL}_{\\_}2$ obtained by imposing some conditions on types and by
replacing the standard additive rules with weaker versions, called linear
additive rules. To some extent, $\mathsf{LAM}$ is more expressive than the
“lazy” restriction of $\mathsf{IMALL}_{\\_}2$. Indeed, the linear additive
rules allow some forms of duplication that lazy evaluation forbids.
Nonetheless, these special additive rules are able to maintain control on the
complexity of normalization, preventing exponential explosions and recovering
linear strong normalization.

The cut-elimination rules for $\mathsf{LAM}$ are constrained to copy-cat the
reduction rules on terms, making the cut rule no longer admissible. We then
identify a class of types, called $\forall$-lazy, whose derivations can always
be turned into cut-free ones in cubic time. This result is analogous to
Girard’s restricted (lazy) cut-elimination theorem for $\mathsf{MALL}$ in
[13], but somehow more permissive.

Last, following essentially [8], we introduce a computationally sound
translation mapping a derivation of $\mathsf{LAM}$ into a linear
$\lambda$-term of $\mathsf{IMLL}_{\\_}2$ whose size can be exponentially
bigger than the source derivation. The translation exploits the mechanisms of
linear duplication and erasure studied by Mairson and Terui in [18, 19], and
shows how $\mathsf{LAM}$ is able to express such mechanisms in a very compact
and elegant way.

##  2 From Standard Additives to Linear Additives

In this section we briefly recall the $(\multimap,\with,\forall)$ fragment of
$\mathsf{IMALL}_{\\_}2$ as a type system, and we show how nesting instances of
the additive rules in a derivation produces an exponential blow up in
normalization. To circumvent this issue we introduce _linear additives_ ,
weaker versions of the standard additives permitting restricted forms of
duplication without affecting the complexity of normalization.

###  2.1 The System $\mathsf{IMALL}_{\\_}2$

We present $\mathsf{IMALL}_{\\_}2$ as a type assignment system for the
calculus $\Lambda_{\\_}{\pi,\langle\rangle}$, whose terms are defined by the
following grammar:

$M:=x\ |\ \lambda x.M\ |\ MM\ |\ \langle M,M\rangle\ |\ \pi_{\\_}1(M)\ |\
\pi_{\\_}2(M)$ (2)

where $x$ is taken from a denumerable set of variables. The set of free
variables of a term $M$ is written $FV(M)$, and the meta-level substitution
for terms is denoted $M[N/x]$. The size $|M|$ of a term $M$ is inductively
defined as follows:

$\displaystyle|x|$ $\displaystyle\triangleq 1$ (3) $\displaystyle|\lambda
x.M|$ $\displaystyle\triangleq|\pi_{\\_}i(M)|\triangleq|M|+1$ $\displaystyle
i\in\\{1,2\\}$ $\displaystyle|MN|$ $\displaystyle\triangleq|\langle
M,N\rangle|\triangleq|M|+|N|+1.$

The _one-step relation $\rightarrow_{\\_}{\beta}$_ is the binary relation over
$\Lambda_{\\_}{\pi,\langle\rangle}$ defined by:

$\displaystyle(\lambda x.M)N$
$\displaystyle\rightarrow_{\\_}{\beta}M[N/x]\qquad\qquad\pi_{\\_}i\langle
M_{\\_}1,M_{\\_}2\rangle$ $\displaystyle\rightarrow_{\\_}{\beta}M_{\\_}i\qquad
i\in\\{1,2\\}$ (4)

Its reflexive and transitive closure is $\rightarrow^{*}_{\\_}\beta$. If $M$
$\beta$-reduces to $N$ in exactly $n$ steps we write
$M\rightarrow^{n}_{\\_}{\beta}N$. As usual, a $\lambda$-term is in (or is a)
_normal form_ whenever no reduction rule applies to it.

The set $\Theta_{\\_}\with$ of types of $\mathsf{IMALL}_{\\_}2$ is generated
by the following grammar:

$A:=\ \alpha\ |\ A\multimap A\ |\ A\with A\ |\ \forall\alpha.A$ (5)

where $\alpha$ belongs to a denumerable set of type variables. The set of free
type variables of a type $A$ is written $FV(A)$, and the standard meta-level
substitution for types is denoted $A\langle B/\alpha\rangle$. A type $A$ is
_closed_ if $FV(A)=\emptyset$. The size $|A|$ of a type $A$ is inductively
defined as follows:

$\displaystyle|\alpha|$ $\displaystyle\triangleq 1$ (6)
$\displaystyle|A\multimap B|$ $\displaystyle\triangleq|A\with
B|\triangleq|A|+|B|+1$ $\displaystyle|\forall\alpha.A|$
$\displaystyle\triangleq|A|+1.$

We define the notions of _positive subtype_ and of _negative subtype_ of a
type $A$ by simultaneous induction on the structure of $A$:

  * •

$A$ is a positive subtype of itself;

  * •

if $B\multimap C$ is a positive (resp. negative) subtype of $A$, then $B$ is a
negative (resp. positive) subtype of $A$, and $C$ is a positive (resp.
negative) subtype of $A$;

  * •

if $B\with C$ is a positive (resp. negative) subtype of $A$, then so are $B$
and $C$;

  * •

if $\forall\alpha.B$ is a positive (resp. negative) subtype of $A$, then so is
$B$.

We say that a type $A$ has _positive (resp. negative) occurrences of
$\forall$_ if there exists a positive (resp. negative) subtype of $A$ with
shape $\forall\alpha.B$. We define in a similar way positive and negative
occurrences of $\multimap$ and $\with$.

The system $\mathsf{IMALL}_{\\_}2$ (Intuitionistic Second-Order Multiplicative
Additive Linear Logic) is displayed in Figure 1, where $\with$R and
$\with$L$i$ are the additives rules. It derives judgements with form
$\Gamma\vdash M:A$, where $M\in\Lambda_{\\_}{\pi,\langle\rangle}$,
$A\in\Theta_{\\_}\with$ and $\Gamma$ is a context, i.e. a finite multiset of
assumptions $x:A$. The system requires the linear constraint $FV(\Gamma)\cap
FV(\Delta)=\emptyset$ in both $cut$ and $\multimap$L, where $FV(\Gamma)$
denotes the set of all free type variables in $\Gamma$. With
$\mathcal{D}\triangleleft\Gamma\vdash M:A$ we denote a derivation
$\mathcal{D}$ of $\Gamma\vdash M:A$, and in this case we say that $M$ is an
inhabitant of $A$ (or that $A$ is inhabited by $M$). The size $|\Gamma|$ of a
context $\Gamma=x_{\\_}1:A_{\\_}1,\ldots,x_{\\_}n:A_{\\_}n$ is
$\sum^{n}_{\\_}{i=1}|A_{\\_}i|$, and the size $|\mathcal{D}|$ of a derivation
$\mathcal{D}$ is the number of its rules applications.

We recall that $\mathsf{IMLL}_{\\_}2$ (Intuitionistic Second-Order
Multiplicative Linear Logic) is obtained from $\mathsf{IMALL}_{\\_}2$ by
excluding the additive rules from Figure 1. It gives a type exactly to the
class of linear $\lambda$-terms (see [15, 19]), i.e. those terms $M$ from the
standard $\lambda$-calculus such that:

  1. (i)

each free variable of $M$ occurs in it exactly once, and

  2. (ii)

for each subterm $\lambda x.N$ of $M$, $x$ occurs in $N$ exactly once.

Tensors ($\otimes$) and units ($\mathbf{1}$) can be introduced in
$\mathsf{IMLL}_{\\_}2$ (and hence in $\mathsf{IMALL}_{\\_}2$) by means of
second-order definitions:

$\displaystyle\textbf{1}\triangleq\forall\alpha.(\alpha\multimap\alpha)$
$\displaystyle A\otimes B\triangleq\forall\alpha.(A\multimap
B\multimap\alpha)\multimap\alpha$ (7)
$\displaystyle\mathbf{I}\triangleq\lambda x.x$ $\displaystyle M\otimes
N\triangleq\lambda z.z\,M\,N$ $\displaystyle\mathtt{let}\ M\mathtt{\ be\
}\mathbf{I}\mathtt{\ in\ }N\triangleq MN$ $\displaystyle\mathtt{let}\
M\mathtt{\ be\ }x\otimes y\mathtt{\ in\ }N\triangleq M(\lambda x.\lambda
y.N).$

Hence, the inference rules for $\otimes$ and $\mathbf{1}$, and the reduction
rules

$\displaystyle\mathtt{let}\ \mathbf{I}\mathtt{\ be\ }\mathbf{I}\mathtt{\ in\
}N$ $\displaystyle\rightarrow_{\\_}\beta N$ (8) $\displaystyle\mathtt{let}\
M_{\\_}1\otimes M_{\\_}2\mathtt{\ be\ }x_{\\_}1\otimes x_{\\_}2\mathtt{\ in\
}N$ $\displaystyle\rightarrow_{\\_}\beta
N[M_{\\_}1/x_{\\_}1,M_{\\_}2/x_{\\_}2]$

are derivable in $\mathsf{IMLL}_{\\_}2$.

*[Right=$ax$]

x: A ⊢x: A *[Right=$cut$]Γ⊢N: A

Δ, x: A ⊢M: CΓ, Δ⊢M[N/x]: C

*[Right=$\multimap$R]Γ, x: A ⊢M: BΓ⊢λx. M : A ⊸B*[Right=$\multimap$L]Γ⊢N:A

Δ, x:B ⊢M:CΓ, y: A ⊸B, Δ⊢M[yN/x]: C

*[Right=$\with$R]Γ⊢M1: A1

Γ⊢M2: A2Γ⊢⟨M1, M2⟩: A1 A2 *[Right=$\with$L$i$]Γ, xi: Ai ⊢M:C i ∈{1,2 }Γ, y :A1
A2 ⊢M[πi(y)/xi] :C

*[Right=$\forall$R]Γ⊢M: A⟨γ/α⟩ γ／∈FV(Γ)Γ⊢M: ∀α. A*[Right=$\forall$L]Γ, x: A ⟨B/α⟩⊢M: CΓ, x: ∀α. A ⊢M: C

Figure 1: The system $\mathsf{IMALL}_{\\_}2$.

###  2.2 Exponential Blowup and Lazy Cut-Elimination for
$\mathsf{IMALL}_{\\_}2$

The additive rule $\with$R in Figure 1 affects the complexity of normalization
in $\mathsf{IMALL}_{\\_}2$, letting the size of typable terms and the number
of their redexes grow exponentially during reduction. Definition 1 and
Proposition 1 show an example.

######  Definition 1 (Nesting $\mathsf{IMALL}_{\\_}2$ terms).

Let $A\in\Theta_{\\_}\with$ and $M\in\Lambda_{\\_}{\pi,\langle\rangle}$. For
all $n\in\mathbb{N}$, we define $A_{\\_}{[n]}$ and $M_{\\_}{[n]}$ as follows:

$A_{\\_}{[n]}\triangleq\begin{cases}A&n=0\\\ A_{\\_}{[n-1]}\with
A_{\\_}{[n-1]}&n>0\end{cases}\qquad\qquad
M_{\\_}{[n]}\triangleq\begin{cases}M&n=0\\\ \langle
M_{\\_}{[n-1]},M_{\\_}{[n-1]}\rangle&n>0\end{cases}$ (9)

Notice that $\langle M,M\rangle_{\\_}{[n]}=M_{\\_}{[n+1]}$. Moreover, for all
$n\in\mathbb{N}$ we define $\mathtt{add}^{x}_{\\_}{n}$ as follows:

$\mathtt{add}^{x}_{\\_}{n}\triangleq\begin{cases}x&n=0\\\ (\lambda
y.\mathtt{add}^{y}_{\\_}{n-1})\langle x,x\rangle&n>0\end{cases}$ (10)

######  Proposition 1 (Exponential blow up).

Let $A\in\Theta_{\\_}\with$, and let $M\in\Lambda_{\\_}{\pi,\langle\rangle}$
be of type $A$. For all $n\in\mathbb{N}$:

  1. 1.

$\vdash\lambda x.\mathtt{add}^{x}_{\\_}{n}:A\multimap A_{\\_}{[n]}$ is
derivable in $\mathsf{IMALL}_{\\_}2$;

  2. 2.

$(\lambda x.\mathtt{add}^{x}_{\\_}n)M\rightarrow^{n+1}_{\\_}\beta
M_{\\_}{[n]}$, where $|(\lambda
x.\mathtt{add}^{x}_{\\_}n)M|=\mathcal{O}(n\cdot|M|)$ and
$|M_{\\_}{[n]}|=\mathcal{O}(2^{n\cdot|M|})$.

###### Proof.

Concerning point 1, we prove by induction on $n$ that $\lambda
x.\mathtt{add}^{x}_{\\_}{n}$ has type $A_{\\_}{[k]}\multimap A_{\\_}{[k+n]}$,
for all $k\in\mathbb{N}$. If $n=0$ then $\mathtt{add}^{x}_{\\_}0=x$, so that
$\lambda x.x$ has type $A_{\\_}{[k]}\multimap A_{\\_}{[k]}$. Let us consider
the case $n>0$. By induction hypothesis, $\lambda
y.\mathtt{add}^{y}_{\\_}{n-1}$ has type $A_{\\_}{[k+1]}\multimap
A_{\\_}{[k+n]}$. If $x$ has type $A_{\\_}{[k]}$ then $\langle x,x\rangle$ has
type $A_{\\_}{[k+1]}$ and $(\lambda y.\mathtt{add}^{y}_{\\_}{n-1})\langle
x,x\rangle$ has type $A_{\\_}{[k+n]}$. Therefore, $\lambda
x.\mathtt{add}^{x}_{\\_}{n}=\lambda x.((\lambda
y.\mathtt{add}^{y}_{\\_}{n-1})\langle x,x\rangle)$ has type
$A_{\\_}{[k]}\multimap A_{\\_}{[k+n]}$. Concerning point 2, it suffices to
prove by induction on $n$ that
$\mathtt{add}^{x}_{\\_}n\rightarrow^{n}_{\\_}{\beta}x_{\\_}{[n]}$. The base
case is trivial. If $n>0$ then $\mathtt{add}^{x}_{\\_}{n}=(\lambda
y.\mathtt{add}^{y}_{\\_}{n-1})\langle
x,x\rangle\rightarrow_{\\_}\beta\mathtt{add}^{y}_{\\_}{n-1}[\langle
x,x\rangle/y]$. Since by induction hypothesis
$\mathtt{add}^{y}_{\\_}{n-1}\rightarrow^{n-1}_{\\_}\beta y_{\\_}{[n-1]}$ then
$\mathtt{add}^{y}_{\\_}{n-1}[\langle x,x\rangle/x]\rightarrow^{n-1}_{\\_}\beta
y_{\\_}{[n-1]}[\langle x,x\rangle/y]=\langle
x,x\rangle_{\\_}{[n-1]}=x_{\\_}{[n]}$. Finally, we notice that, for all
$n\in\mathbb{N}$, it holds that $|\mathtt{add}^{x}_{\\_}n|=(5\cdot n)+1$ and
$|M_{\\_}{[n]}|=2^{n\cdot|M|}+\sum^{n-1}_{\\_}{i=0}2^{i}$. ∎

Proposition 1 is about the complexity of normalization for
$\mathsf{IMALL}_{\\_}2$’s typable terms, but it can be easily restated for
cut-elimination. To prevent the problem of exponential computation, Girard
introduced in [13] the so-called _lazy cut-elimination_ , a rewriting
procedure for both $\mathsf{MALL}$’s proof nets and their second-order
versions that requires only a linear number of steps. Intuitively, in the
sequent calculus presentation of $\mathsf{IMALL}_{\\_}2$, lazy cut-elimination
“freezes” the commuting cut-elimination steps applied to those instances of
$cut$ whose right premise is the conclusion of $\with$R, as they involve
duplication of (sub)proofs (see Figure 2).

$\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
72.44444pt\hbox{\vbox{\hbox{\vbox{\hbox{\hskip 18.45126pt\hbox{\hskip
4.0pt\hbox{$\mathcal{D}$}\hskip 4.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip
1.0pt}}\lower-0.5pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hbox{\hskip
4.0pt\hbox{$\Gamma\vdash M:A$}\hskip 4.0pt}}}\hbox{\hskip
14.45377pt}\vbox{\hbox{\vbox{\hbox{\hskip 32.01889pt\hbox{\hskip
4.0pt\hbox{\vdots}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip 1.0pt}}\lower-0.5pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\Delta,x:A\vdash
N:B$}\hskip 4.0pt}}}\hbox{\hskip 14.45377pt}\vbox{\hbox{\hskip
31.24876pt\hbox{\hskip 4.0pt\hbox{\vdots}\hskip 4.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip
1.0pt}}\lower-0.5pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hbox{\hskip
4.0pt\hbox{$\Delta,x:A\vdash P:C$}\hskip
4.0pt}}}}\vskip-1.21666pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox to171.98907pt{\xleaders\hrule\hfill}\lower
3.21666pt\hbox{\hskip
3.0pt$\with$R}}\vskip-1.21666pt\nointerlineskip\hbox{\hskip
30.79956pt\hbox{\hbox{\hskip 4.0pt\hbox{$\Delta,x:A\vdash\langle
N,P\rangle:B\with C$}\hskip
4.0pt}}}}}\vskip-0.8754pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox to208.18472pt{\xleaders\hrule\hfill}\lower
2.8754pt\hbox{\hskip 3.0pt$cut$}}\vskip-0.8754pt\nointerlineskip\hbox{\hskip
25.87311pt\hbox{\hbox{\hskip 4.0pt\hbox{$\Gamma,\Delta\vdash\langle
N[M/x],P[M/x]\rangle:B\with C$}\hskip 4.0pt}}}}}\ignorespaces\\\
\rightsquigarrow\\\
\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
72.44444pt\hbox{\vbox{\hbox{\vbox{\hbox{\vbox{\hbox{\hskip
18.45126pt\hbox{\hskip 4.0pt\hbox{$\mathcal{D}$}\hskip 4.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip
1.0pt}}\lower-0.5pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hbox{\hskip
4.0pt\hbox{$\Gamma\vdash M:A$}\hskip 4.0pt}}}\hbox{\hskip
14.45377pt}\vbox{\hbox{\hskip 32.01889pt\hbox{\hskip 4.0pt\hbox{\vdots}\hskip
4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip 1.0pt}}\lower-0.5pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\Delta,x:A\vdash
N:B$}\hskip 4.0pt}}}}\vskip-0.8754pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox to146.53297pt{\xleaders\hrule\hfill}\lower
2.8754pt\hbox{\hskip 3.0pt$cut$}}\vskip-0.8754pt\nointerlineskip\hbox{\hskip
26.22675pt\hbox{\hbox{\hskip 4.0pt\hbox{$\Gamma,\Delta\vdash N[M/x]:B$}\hskip
4.0pt}}}}\hbox{\hskip 14.45377pt}\vbox{\hbox{\vbox{\hbox{\hskip
18.45126pt\hbox{\hskip 4.0pt\hbox{$\mathcal{D}$}\hskip 4.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip
1.0pt}}\lower-0.5pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hbox{\hskip
4.0pt\hbox{$\Gamma\vdash M:A$}\hskip 4.0pt}}}\hbox{\hskip
14.45377pt}\vbox{\hbox{\hskip 31.24876pt\hbox{\hskip 4.0pt\hbox{\vdots}\hskip
4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip 1.0pt}}\lower-0.5pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\Delta,x:A\vdash
P:C$}\hskip 4.0pt}}}}\vskip-0.8754pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox to144.99272pt{\xleaders\hrule\hfill}\lower
2.8754pt\hbox{\hskip 3.0pt$cut$}}\vskip-0.8754pt\nointerlineskip\hbox{\hskip
26.22675pt\hbox{\hbox{\hskip 4.0pt\hbox{$\Gamma,\Delta\vdash P[M/x]:C$}\hskip
4.0pt}}}}}\vskip-1.21666pt\nointerlineskip\hbox{\hskip
26.22675pt\lower-0.2pt\hbox{}\hbox to270.18922pt{\xleaders\hrule\hfill}\lower
3.21666pt\hbox{\hskip
3.0pt$\with$R}}\vskip-1.21666pt\nointerlineskip\hbox{\hskip
83.1021pt\hbox{\hbox{\hskip 4.0pt\hbox{$\Gamma,\Delta\vdash\langle
N[M/x],P[M/x]\rangle:B\with C$}\hskip 4.0pt}}}}}\ignorespaces$ Figure 2:
Commuting cut-elimination step (with term annotation) involving duplication of
$\mathcal{D}$.

Since lazy cut-elimination cannot perform certain cut-elimination steps, it
may fail to produce a cut-free proof. Nonetheless, Girard showed that a cut-
elimination theorem for $\mathsf{MALL}_{\\_}2$’s proof nets holds if we stick
to those receiving ($\with,\exists$)-free types (see [13]). Following [19], we
call these special types “lazy”, and we define their intuitionistic
counterparts as follows:

######  Definition 2 (Lazy types).

A type $A\in\Theta_{\\_}\with$ is _lazy_ if it contains no negative
occurrences of $\forall$ and no positive occurrences of $\with$.

Note that the restriction on negative occurrences of $\forall$ in the above
definition is just to forbid the hiding of $\with$ connectives by $\forall$L
in $\mathsf{IMALL}_{\\_}2$.

Lazy cut-elimination for $\mathsf{IMALL}_{\\_}2$ can be reformulated as a
reduction on terms by introducing some form of sharing, e.g. explicit
substitution (see [2]). The idea is to replace the meta-notation $M[N/x]$ with
a term constructor of the following shape:

$M\langle\\!\langle{x:=N}\rangle\\!\rangle$ (11)

and to add reduction rules able to introduce and perform substitution
stepwise, such as:

$\displaystyle(\lambda x.M)N$ $\displaystyle\rightarrow
M\langle\\!\langle{x:=N}\rangle\\!\rangle$ (12) $\displaystyle
x\langle\\!\langle{x:=N}\rangle\\!\rangle$ $\displaystyle\rightarrow N$
$\displaystyle y\langle\\!\langle{x:=N}\rangle\\!\rangle$
$\displaystyle\rightarrow y$ $\displaystyle y\neq x$ $\displaystyle(\lambda
y.M)\langle\\!\langle{x:=N}\rangle\\!\rangle$ $\displaystyle\rightarrow\lambda
y.(M\langle\\!\langle{x:=N}\rangle\\!\rangle)$ $\displaystyle y\neq x\text{
and }y\not\in FV(N)$
$\displaystyle(MP)\langle\\!\langle{x:=N}\rangle\\!\rangle$
$\displaystyle\rightarrow M\langle\\!\langle{x:=N}\rangle\\!\rangle
P\langle\\!\langle{x:=N}\rangle\\!\rangle$
$\displaystyle\pi_{\\_}i(M)\langle\\!\langle{x:=N}\rangle\\!\rangle$
$\displaystyle\rightarrow\pi_{\\_}i(M\langle\\!\langle{x:=N}\rangle\\!\rangle)$
$\displaystyle i\in\\{1,2\\}$ $\displaystyle\langle
M,P\rangle\langle\\!\langle{x:=N}\rangle\\!\rangle$
$\displaystyle\rightarrow\langle
M\langle\\!\langle{x:=N}\rangle\\!\rangle,P\langle\\!\langle{x:=N}\rangle\\!\rangle\rangle.$

_Lazy reduction_ is then obtained by forbidding substitutions of terms in a
pair, i.e. by ruling out the last rewriting rule of (12), since it mimics the
cut-elimination step in Figure 2. As an example, consider the following
typable terms of $\mathsf{IMALL}_{\\_}2$:

$\displaystyle M$ $\displaystyle\triangleq(\lambda x.\pi_{\\_}1\langle
x,x\rangle)N$ (13) $\displaystyle M^{\prime}$ $\displaystyle\triangleq(\lambda
x.\langle x,x\rangle)N.$

If we applied standard $\beta$-reduction to $M$ we would obtain
$\pi_{\\_}1\langle N,N\rangle$, thus creating a (useless) copy of $N$. By
contrast, thanks to explicit substitution, lazy reduction enables a better
control on the parameter-passing mechanism and reduces $M$ without making new
copies of $N$:

$(\lambda x.\pi_{\\_}1\langle x,x\rangle)N\rightarrow\pi_{\\_}1\langle
x,x\rangle\langle\\!\langle{x:=N}\rangle\\!\rangle\rightarrow
x\langle\\!\langle{x:=N}\rangle\\!\rangle\rightarrow N.$

The above reasoning does not apply to $M^{\prime}$, as the substitution
$\langle x,x\rangle\langle\\!\langle{x:=N}\rangle\\!\rangle$ would remain
unperformed, so that lazy reduction may fail to produce a substitution-free
term, in general. Again, as in the case of cut-elimination, when a term has
lazy type in $\mathsf{IMALL}_{\\_}2$ each pair $\langle P,Q\rangle$ occurring
in it eventually turns into a redex $\pi_{\\_}i\langle P,Q\rangle$, so that
all suspended substitutions are sooner or later carried out. Going back to the
terms in (13), notice that $M$ has lazy type in $\mathsf{IMALL}_{\\_}2$
whenever $N$ has, while only (non-lazy) types with shape $A\with A$ can be
assigned to $M^{\prime}$.

Explicit substitution and other forms of sharing play a fundamental role in
the study of reasonable cost models of the untyped $\lambda$-calculus, where
$\beta$-reduction and meta-level substitution cause size explosions similar to
Proposition 1 (see e.g. [3, 4, 17]). As an example, in [4] Accattoli and Dal
Lago have shown that $\lambda$-terms with explicit substitutions can be
managed in reasonable (i.e. polynomial) time, without having to unfold the
sharing (that would re-introduce an exponential size blow up). Explicit
substitutions have been introduced to cover the gap between the
$\lambda$-calculus and concrete implementations, but they can also produce
pathological behaviors in a typed setting, as shown by Melliès in [22].

###  2.3 Linear Additives

To prevent the exponential blow up discussed in the previous section we
introduce weaker versions of the standard additive rules called _linear
additive rules_ , which give types to $\mathtt{copy}$ constructs. The linear
additive rules are displayed in Figure 3,

*[Right=$\with$R$0$]⊢M1: A1

⊢M2: A2 ⊢⟨M1, M2 ⟩: A1 A2 *[Right=$\with$L$i$]Γ, xi: Ai ⊢M:C i ∈{1,2 }Γ, y :A1
A2 ⊢M[πi(y)/xi] :C

*[Right=$\with$R$1$]x1: A ⊢M1:A1

x2: A ⊢M2:A2

⊢V:Ax: A ⊢copy^V x  as x1, x2  in  ⟨M1,M2 ⟩: A1 A2

Figure 3: Linear additive rules, where $V\in\mathcal{V}$ and
$A,A_{\\_}1,A_{\\_}2$ are closed and $\forall$-lazy types.

where $V$ is a _value_ , i.e. a closed and normal term free from instances of
$\mathtt{copy}$ and projections, and the types $A,A_{\\_}1,A_{\\_}2$ are
closed and _$\forall$ -lazy_, according to the following definition:

######  Definition 3 ($\forall$-lazy types).

A type $A\in\Theta_{\\_}\with$ is _$\forall$ -lazy_ if it contains no negative
occurrences of $\forall$. We say that
$x_{\\_}1:A_{\\_}1,\ldots,x_{\\_}n:A_{\\_}n\vdash M:B$ is a $\forall$-lazy
judgement if $A_{\\_}1\multimap\ldots\multimap A_{\\_}n\multimap B$ is a
$\forall$-lazy type. Finally, we say that
$\mathcal{D}\triangleleft\Gamma\vdash M:A$ is a $\forall$-lazy derivation if
$\Gamma\vdash M:A$ is a $\forall$-lazy judgement.

The reduction rule corresponding to $\mathsf{copy}$ will be of the following
form:

$\mathtt{copy}^{V}U\mathtt{\ as\ }x_{\\_}1,x_{\\_}2\mathtt{\ in\ }\langle
M_{\\_}1,M_{\\_}2\rangle\rightarrow\langle
M_{\\_}1[U/x_{\\_}1],M_{\\_}2[U/x_{\\_}2]\rangle\qquad U,V\in\mathcal{V}$ (14)

where $\mathcal{V}$ is the set of all values. Notice that the inference rule
$\with$R$0$ in Figure 3 is introduced to let the above reduction rule preserve
types, i.e. to assure Subject reduction. Intuitively, the operator
$\mathtt{copy}$ behaves as a suspended substitution, quite like in lazy
reduction discussed in Section 2.2: the crucial difference is that lazy
reduction forbids _any_ substitution of a term $N$ in a pair $\langle
M_{\\_}1,M_{\\_}2\rangle$, while $\mathtt{copy}$ allows it when $N$ is turned
into a value $U$.

Hence, some limited forms of duplication are permitted by the linear additive
rules. Nonetheless, they do not affect the complexity of normalization. On the
one hand, indeed, the reduction rule in (14) can only copy values, i.e. normal
terms, so that no redex is duplicated. This allows linear time normalization.
On the other hand, since any _$\forall$ -lazy_ type $A$ is inhabited by
finitely many values (see Proposition 3.2), by taking $V$ in Figure 3 as the
largest one of that type, we enable the size of $\mathtt{copy}^{V}$ to bound
the size of the new copy of $U$ produced by applying (14) (since $U$ has type
$A$). This lets reduction strictly decrease the size of terms, recovering
linear space normalization.

As a final remark, let us observe that the linear additive rule $\with$R$1$
introduces a seemingly severe restriction: context-sharing is permitted for
premises having _exactly_ one assumption. This constraint has no real impact
on the algorithmic expressiveness of linear additives, since a general
inference rule with premises sharing multiple assumptions can be easily
derived by exploiting the definitions in (7). Indeed, tensors are able to turn
a context with $n$ assumptions $x_{\\_}1:A_{\\_}1,\ldots,x_{\\_}n:A_{\\_}n$
into one with single assumption $x:A_{\\_}1\otimes\ldots\otimes A_{\\_}n$.
Narrowing context-sharing has its benefits: it avoids heavy notation produced
by several occurrences of the construct $\mathtt{copy}$, each one expressing
the sharing of a single assumption.

##  3 A Type Assignment With Linear Additives

In this section we introduce Linearly Additive Multiplicative Type Assignment,
$\mathsf{LAM}$ for short. It is a subsystem of $\mathsf{IMALL}_{\\_}2$ endowed
with the linear additive rules in Figure 3. Thanks to the controlled use of
substitution, these rules can be freely nested in $\mathsf{LAM}$ without
incurring exponential normalization.

###  3.1 The System $\mathsf{LAM}$

The following grammar generates raw terms:

$\displaystyle M,N$ $\displaystyle:=\,x\ |\ \lambda x.M\ |\ MM\ |\ \langle
M,M\rangle\ |\ \pi_{\\_}i(M)\ |\ \mathtt{copy}^{U}M\mathtt{\ as\ }x,y\mathtt{\
in\ }\langle M,M\rangle$ (15) $\displaystyle U,V$ $\displaystyle:=\,x\ |\
\lambda x.U\ |\ UU\ |\ \langle U,U\rangle$ (16)

where $\mathtt{copy}^{U}M\mathtt{\ as\ }x,y\mathtt{\ in\ }\langle P,Q\rangle$
binds both $x$ in $P$ and $y$ in $Q$. A _value_ is any closed raw term
generated by the grammar (16) that is _normal_ with respect to the reduction
step $(\lambda x.U)V\rightarrow U[V/x]$. The set of all values is denoted
$\mathcal{V}$. A raw term is a _term_ if any occurrence of the
$\mathtt{copy}^{U}$ operator in it is such that $U\in\mathcal{V}$. The set of
terms is denoted $\Lambda_{\\_}{\mathtt{copy}}$. We extend the definition of
$|M|$ in (3) to the new clause:

$\displaystyle|{\mathtt{copy}^{U}M\mathtt{\ as\ }x,y\mathtt{\ in\ }\langle
P,Q\rangle}|$ $\displaystyle=|U|+|M|+|\langle P,Q\rangle|+1$

The one-step reduction $\rightarrow$ on $\Lambda_{\\_}{\mathtt{copy}}$ extends
$\rightarrow_{\\_}{\beta}$ in (4) with the reduction rule in (14), and applies
in any context. Its reflexive and transitive closure is $\rightarrow^{*}$. If
$M$ reduces to $N$ in exactly $n$ steps we write $M\rightarrow^{n}N$. A term
is in (or is a) normal form if no reduction applies to it.

The system $\mathsf{LAM}$ is essentially obtained by replacing the standard
additive rules of $\mathsf{IMALL}_{\\_}2$ with the linear additive rules in
Figure 3, and by imposing a mild requirement on the inference rules
$\multimap$L and $\forall$R that plays an crucial role to assure a weak form
of cut-elimination.

######  Definition 4 (The system $\mathsf{LAM}$).

The system $\mathsf{LAM}$ (Linearly Additive Multiplicative Type Assignment)
is the type assignment for $\Lambda_{\\_}{\mathtt{copy}}$ obtained by
extending $\mathsf{IMLL}_{\\_}2$ with the linear additive rules in Figure 3,
and by imposing the following _closure conditions_ :

  1. (i)

no instance of $\multimap$L has conclusion $\Delta,y:A\multimap B,\Gamma\vdash
M:C$ with $FV(B)=\emptyset$ and $FV(A)\neq\emptyset$;

  2. (ii)

no instance of $\forall$R has conclusion $\Gamma\vdash M:\forall\alpha.A$ with
$FV(\forall\alpha.A)=\emptyset$ and $FV(\Gamma)\neq\emptyset$.

As it stands, $\mathsf{LAM}$ is able to linearly bound the number of steps
required to normalize typable terms, essentially because we can only duplicate
values, which are redex-free. However, the system has no control over the size
of terms, which may grow exponentially during normalization. What we need is
to bound the size of the new copies of values that are produced by applying
the reduction rule (14). This is the goal of Proposition 3 and Remark 1.

######  Definition 5 ($\eta$-expansion).

Given $\mathcal{D}\triangleleft\Gamma\vdash M:A$ a $\forall$-lazy and _cut-
free_ derivation, we say that $\mathcal{D}$ is $\eta$-expanded if all its
axioms are atomic, i.e. of the form $x:\alpha\vdash x:\alpha$ for some type
variable $\alpha$. In this case, $M$ is called a $\eta$-long normal form (note
that $M$ must be a normal form).

We now state some basic properties about $\forall$-lazy and $\eta$-expanded
derivations.

######  Proposition 2 ($\forall$-lazy derivations).

  1. 1.

If a premise of one among the rules $\multimap$R, $\multimap$L and $\forall$R
is not $\forall$-lazy, then neither is its conclusion. Moreover, the
conclusions of $\with$R$1$, $\with$L$i$ and $\forall$L are not $\forall$-lazy,
while the conclusion of $\with$R$0$ is.

  2. 2.

Let $\mathcal{D}\triangleleft\Gamma\vdash M:A$ be $\forall$-lazy and cut-free,
then:

     * •

$\mathcal{D}$ contains no instances of $\with$R$1$, $\with$L$i$ and
$\forall$L;

     * •

$M$ is normal and contains no occurrences of $\mathtt{copy}$ and $\pi_{\\_}i$;

     * •

if $\Gamma=\emptyset$ then $M\in\mathcal{V}$.

######  Proposition 3 ($\eta$-expanded derivations).

Let $\mathcal{D}\triangleleft\Gamma\vdash M:A$ be $\forall$-lazy and
$\eta$-expanded. Then:

  1. 1.

$|M|\leq|\Gamma|+|A|\leq 2\cdot|\mathcal{D}|$;

  2. 2.

if $\mathcal{D}^{\prime}\triangleleft\Gamma\vdash N:A$ is cut-free for some
$N\in\Lambda_{\\_}{\mathtt{copy}}$, then both $|N|\leq|{M}|$ and
$|{\mathcal{D}^{\prime}}|\leq|{\mathcal{D}}|$.

###### Proof.

By Definition 5 and Proposition 2.2, $\mathcal{D}$ is cut-free and without
instances of $\with$R$1$, $\with$L$i$, $\forall$L, with $M$ normal and free
from $\mathtt{copy}$ constructs. Point 1 is a straightforward induction on
$\mathcal{D}$. Concerning point 2, we have
$|\mathcal{D}^{\prime}|\leq|{\mathcal{D}}|$, because $\mathcal{D}$ is
$\eta$-expanded. Now, notice that
$|{N}|+\forall(\Gamma,A)=|{\mathcal{D}^{\prime}}|+\forall_{\\_}{ax}(\mathcal{D}^{\prime})$,
where $\forall(\Gamma,A)$ denotes the number of occurrences of $\forall$ in
$\Gamma,A$, and $\forall_{\\_}{ax}(\mathcal{D}^{\prime})$ denotes the number
of occurrences of $\forall$ in the conclusions of the instances of $ax$ in
$\mathcal{D}^{\prime}$. We have,
$|{N}|+\forall(\Gamma,A)=|{\mathcal{D}^{\prime}}|+\forall_{\\_}{ax}(\mathcal{D}^{\prime})\leq|{\mathcal{D}}|+\forall_{\\_}{ax}(\mathcal{D})=|{M}|+\forall(\Gamma,A)$,
which implies $|N|\leq|M|$. ∎

######  Remark 1.

Given $\mathcal{D}\triangleleft\Gamma\vdash M:A$ a $\forall$-lazy and cut-free
derivation, we can always construct a $\eta$-expanded derivation
$\mathcal{D}^{*}\triangleleft\Gamma\vdash M^{*}:A$. Moreover, Proposition 3.2
implies both $|N|\leq|M^{*}|$ and
$|\mathcal{D}^{\prime}|\leq|\mathcal{D}^{*}|$, for any cut-free derivation
$\mathcal{D}^{\prime}\triangleleft\Gamma\vdash N:A$. Henceforth, w.l.o.g. we
shall assume that the derivation of the premise $\vdash V:A$ of $\with$R$1$ is
$\eta$-expanded.

Remark 1 prevents the increase of size during normalization, since the size of
$V$ in $\with$R$1$ is always bigger than then size of any value $U$ of type
$A$, and so the construct $\mathtt{copy}^{V}$ bounds the size of the new copy
of $U$ produced by applying the reduction rule in (14).

###  3.2 Linear Additives Prevent the Exponential Blowup

We can observe the benefits of moving from the standard additive rules to the
linear additive rules as soon as we adapt the constructions in Definition 1 to
$\mathsf{LAM}$.

######  Definition 6 (Nesting $\mathsf{LAM}$ terms).

Let $V\in\mathcal{V}$ and $k\in\mathbb{N}$. For all $n\in\mathbb{N}$ we define
$\mathtt{ladd}^{x,V_{\\_}{[k]}}_{\\_}{n}$ as follows:

$\mathtt{ladd}^{x,V_{\\_}{[k]}}_{\\_}{n}\triangleq\begin{cases}x&n=0\\\
(\lambda
y.\mathtt{ladd}^{y,V_{\\_}{[k+1]}}_{\\_}{n-1})(\mathtt{copy}^{V_{\\_}{[k]}}x\
\mathtt{as}\ x_{\\_}1,x_{\\_}2\mathtt{\ in\ }\langle
x_{\\_}1,x_{\\_}2\rangle)&n>0\end{cases}$

where $V_{\\_}{[k]}$ is as in (9).

The following proposition states that nesting instances of $\with$R$1$ in a
derivation of $\mathsf{LAM}$ produces no exponential blow up.

######  Proposition 4 (Linearity of $\mathsf{LAM}$).

Let $A$ be a closed and $\forall$-lazy type, and let $U,V\in\mathcal{V}$ be
inhabitants of $A$, with $V$ a $\eta$-long normal form. For all
$n\in\mathbb{N}$:

  1. 1.

$\vdash\lambda x.\mathtt{ladd}^{x,V}_{\\_}{n}:A\multimap A_{\\_}{[n]}$ is
derivable in $\mathsf{LAM}$;

  2. 2.

$(\lambda x.\mathtt{ladd}^{x,V}_{\\_}n)U\rightarrow^{2n+1}U_{\\_}{[n]}$, where
$|(\lambda x.\mathtt{ladd}^{x,V}_{\\_}n)U|>|U_{\\_}{[n]}|>2n+1$.

###### Proof.

Concerning point 1, we prove by induction on $n$ that $\lambda
x.\mathtt{ladd}^{x,V_{\\_}{[k]}}_{\\_}{n}$ has type $A_{\\_}{[k]}\multimap
A_{\\_}{[k+n]}$, for all $k\in\mathbb{N}$. If $n=0$ then
$\mathtt{ladd}^{x,V_{\\_}{[k]}}_{\\_}{n}=x$, so that $\lambda x.x$ has type
$A_{\\_}{[k]}\multimap A_{\\_}{[k]}$. Let us consider the case $n>0$. By
induction hypothesis, $\lambda y.\mathtt{ladd}^{y,V_{\\_}{[k+1]}}_{\\_}{n-1}$
has type $A_{\\_}{[k+1]}\multimap A_{\\_}{[k+n]}$. If $x,x_{\\_}1,x_{\\_}2$
have type $A_{\\_}{[k]}$ then $\mathtt{copy}^{V_{\\_}{[k]}}x\ \mathtt{as}\
x_{\\_}1,x_{\\_}2\mathtt{\ in\ }\langle x_{\\_}1,x_{\\_}2\rangle$ has type
$A_{\\_}{[k+1]}$ and $(\lambda
y.\mathtt{ladd}^{y,V_{\\_}{[k+1]}}_{\\_}{n-1})(\mathtt{copy}^{V_{\\_}{[k]}}x\
\mathtt{as}\ x_{\\_}1,x_{\\_}2\mathtt{\ in\ }\langle
x_{\\_}1,x_{\\_}2\rangle)$ has type $A_{\\_}{[k+n]}$. Therefore, $\lambda
x.\mathtt{ladd}^{x,V_{\\_}{[k]}}_{\\_}{n}$ has type $A_{\\_}{[k]}\multimap
A_{\\_}{[k+n]}$. Concerning point 2, we show by induction on $n$ that
$(\mathtt{ladd}^{x,V_{\\_}{[k]}}_{\\_}{n})[U_{\\_}{[k]}/x]\rightarrow^{2n}U_{\\_}{[n+k]}$,
for all $k\in\mathbb{N}$. The base case is trivial. If $n>0$ then, since
$U_{\\_}{[k]}\in\mathcal{V}$, we have:

$\displaystyle(\mathtt{ladd}^{x,V_{\\_}{[k]}}_{\\_}{n})[U_{\\_}{[k]}/x]$
$\displaystyle=(\lambda
y.\mathtt{ladd}^{y,V_{\\_}{[k+1]}}_{\\_}{n-1})(\mathtt{copy}^{V_{\\_}{[k]}}U_{\\_}{[k]}\mathtt{as}\
x_{\\_}1,x_{\\_}2\mathtt{\ in\ }\langle x_{\\_}1,x_{\\_}2\rangle)$
$\displaystyle\rightarrow(\lambda
y.\mathtt{ladd}^{y,V_{\\_}{[k+1]}}_{\\_}{n-1})\langle
U_{\\_}{[k]},U_{\\_}{[k]}\rangle$
$\displaystyle\rightarrow\mathtt{ladd}^{y,V_{\\_}{[k+1]}}_{\\_}{n-1}[\langle
U_{\\_}{[k]},U_{\\_}{[k]}\rangle/y]=\mathtt{ladd}^{y,V_{\\_}{[k+1]}}_{\\_}{n-1}[U_{\\_}{[k+1]}/y]$

which reduces in $2(n-1)$ steps to $U_{\\_}{[k+n]}$ by induction hypothesis.
Finally, we notice that
$|\mathtt{ladd}^{x,V_{\\_}{[k]}}_{\\_}n|=7n+\sum^{n-1}_{\\_}{i=0}|V_{\\_}{[k+i]}|+1$
and $|U_{\\_}{[n]}|=2^{n\cdot|U|}+\sum^{n-1}_{\\_}{i=0}2^{i}$, for all
$n\in\mathbb{N}$. Since $V$ is a $\eta$-long normal form of $A$, we have
$|V|\geq|U|$ by Proposition 3.2, and the conclusion follows. ∎

##  4 Computational and Proof-Theoretical Properties of $\mathsf{LAM}$

In Section 3.2 we have shown with the help of a key example how linear
additives prevent exponential explosions in normalization. We now investigate
further this point by proving that $\mathsf{LAM}$ enjoys both linear strong
normalization (Theorem 8) and a mildly weakened cubic cut-elimination property
(Theorem 13).

###  4.1 Subject Reduction and Linear Strong Normalization

Linear strong normalization for $\mathsf{LAM}$ is achieved by proving that
reduction preserves types and shrinks the size of typable terms, i.e. a
slightly stronger version of Subject reduction. First, we need some
straightforward preliminary lemmas:

######  Lemma 5 (Linearity).

If $\mathcal{D}\triangleleft\Gamma,x:A\vdash M:C$ then $x$ occurs exactly once
in $M$.

######  Lemma 6 (Generation).

  1. 1.

If $\mathcal{D}\triangleleft\Gamma\vdash\lambda x.M:A$ then
$A=\forall\alpha_{\\_}1\ldots\forall\alpha_{\\_}n.(B\multimap C)$ and, by
permuting some rules of $\mathcal{D}$, we obtain a derivation
$\mathcal{D}^{\prime}$ of $\Gamma,x:B\vdash M:C$, followed by an instance of
$\multimap$R and a sequence of $\forall$R.

  2. 2.

If $\mathcal{D}\triangleleft\Gamma,x:\forall\alpha.A\vdash M[xN/y]:B$ then
$\mathcal{D}$ contains an instance of $\forall$L that introduces
$x:\forall\alpha.A$.

  3. 3.

If $\mathcal{D}\triangleleft\Gamma,x:A\multimap B\vdash M[xN/y]:C$ then
$\mathcal{D}$ contains an instance of $\multimap$L that introduces
$x:A\multimap B$.

  4. 4.

If $\mathcal{D}\triangleleft\Gamma\vdash\langle M_{\\_}1,M_{\\_}2\rangle:A$
then $\Gamma=\emptyset$, $A=B_{\\_}1\with B_{\\_}2$, and the last rule of
$\mathcal{D}$ is $\with$R$0$.

  5. 5.

If $\mathcal{D}\triangleleft\Gamma,x:A_{\\_}1\with A_{\\_}2\vdash
M[\pi_{\\_}{i}(x)/x_{\\_}i]:A$ then $\mathcal{D}$ contains an instance of
$\with$L$i$ that introduces $x:A_{\\_}1\with A_{\\_}2$.

  6. 6.

If $\mathcal{D}\triangleleft\Gamma,x:B\vdash M[\mathtt{copy}^{V}x\mathtt{\ as\
}x_{\\_}1,x_{\\_}2\mathtt{\ in\ }\langle N_{\\_}1,N_{\\_}2\rangle/y]:A$, then
$\mathcal{D}$ contains an instance of $\with$R$1$ that introduces $x:B$.

######  Theorem 7 (Subject reduction).

If $\mathcal{D}\triangleleft\Gamma\vdash M_{\\_}1:A$ and $M_{\\_}1\rightarrow
M_{\\_}2$ then:

  * •

$|{M_{\\_}2}|<|{M_{\\_}1}|$, and

  * •

$\mathcal{D}^{*}\triangleleft\Gamma\vdash M_{\\_}2:A$, for some
$\mathcal{D}^{*}$.

###### Proof.

We proceed by structural induction on $\mathcal{D}$. The crucial case is when
the last rule of $\mathcal{D}$ is an instance of $cut$ introducing the redex
in $M_{\\_}1$ that has been fired by the reduction step $M_{\\_}1\rightarrow
M_{\\_}2$. We just consider the case where
$M_{\\_}1=P[\mathtt{copy}^{U}V\mathtt{\ as\ }x_{\\_}1,x_{\\_}2\mathtt{\ in\
}\langle N_{\\_}1,N_{\\_}2\rangle/y]$ and $M_{\\_}2=P[\langle
N_{\\_}1[V/x_{\\_}1],N_{\\_}2[V/x_{\\_}2]\rangle/y]$. We have:

$\mathcal{D}_{\\_}1\triangleleft\vdash V:B$
$\mathcal{D}_{\\_}2\triangleleft\Delta,x:B\vdash P[\mathtt{copy}^{U}x\mathtt{\
as\ }x_{\\_}1,x_{\\_}2\mathtt{\ in\ }\langle N_{\\_}1,N_{\\_}2\rangle/y]:A$
$cut$ $\mathcal{D}\triangleleft\Delta\vdash P[\mathtt{copy}^{U}V\mathtt{\ as\
}x_{\\_}1,x_{\\_}2\mathtt{\ in\ }\langle N_{\\_}1,N_{\\_}2\rangle/y]:A$

By applying Lemma 6.6, $\mathcal{D}_{\\_}2$ must be of the following form:

$\mathcal{D}^{\prime}\triangleleft x_{\\_}1:B\vdash N_{\\_}1:B_{\\_}1$
$\mathcal{D}^{\prime\prime}\triangleleft x_{\\_}2:B\vdash N_{\\_}2:B_{\\_}2$
$\mathcal{D}^{\prime\prime\prime}\triangleleft\vdash U:B$ $\with$R$1$
$x:B\vdash\mathtt{copy}^{U}x\mathtt{\ as\ }x_{\\_}1,x_{\\_}2\mathtt{\ in\
}\langle N_{\\_}1,N_{\\_}2\rangle:B_{\\_}1\with B_{\\_}2$ $\vdots\ \gamma$
$\mathcal{D}_{\\_}2\triangleleft\Delta,x:B\vdash P[\mathtt{copy}^{U}x\mathtt{\
as\ }x_{\\_}1,x_{\\_}2\mathtt{\ in\ }\langle N_{\\_}1,N_{\\_}2\rangle/y]:A$

where $\gamma$ is a sequence of rules. We construct $\mathcal{D}^{*}$ as the
following derivation:

$\mathcal{D}_{\\_}1\triangleleft\vdash V:B$ $\mathcal{D}^{\prime}\triangleleft
x_{\\_}1:B\vdash N_{\\_}1:B_{\\_}1$ $cut$ $\vdash
N_{\\_}1[V/x_{\\_}1]:B_{\\_}1$ $\mathcal{D}_{\\_}1\triangleleft\vdash V:B$
$\mathcal{D}^{\prime\prime}\triangleleft x_{\\_}2:B\vdash N_{\\_}2:B_{\\_}2$
$cut$ $\vdash N_{\\_}2[V/x_{\\_}2]:B_{\\_}2$ $\with$R$0$ $\vdash\langle
N_{\\_}1[V/x_{\\_}1],N_{\\_}2[V/x_{\\_}2]\rangle:B_{\\_}1\with B_{\\_}2$
$\vdots\ \gamma$ $\Delta\vdash P[\langle
N_{\\_}1[V/x_{\\_}1],N_{\\_}2[V/x_{\\_}2]\rangle/y]:A$

By Remark 1, $U$ is a $\eta$-long normal form, so that $|{V}|\leq|{U}|$ by
Proposition 3.2. By Lemma 5, $x_{\\_}1$ and $x_{\\_}2$ occur exactly once in
$N_{\\_}1$ and $N_{\\_}2$, respectively. Hence,
$|{N_{\\_}i[V/x_{\\_}i]}|=|{N_{\\_}i}|+|{V}|-1$, for $i=1,2$. We have:

$\begin{split}|{\langle
N_{\\_}1[V/x_{\\_}1],N_{\\_}2[V/x_{\\_}2]\rangle}|&=|{N_{\\_}1[V/x_{\\_}1]}|+|{N_{\\_}2[V/x_{\\_}2]}|+1=2\cdot|{V}|+|{N_{\\_}1}|+|{N_{\\_}2}|-1\\\
&\leq|{U}|+|{V}|+|{N_{\\_}1}|+|{N_{\\_}2}|-1<|{\mathtt{copy}^{U}V\mathtt{\ as\
}x_{\\_}1,x_{\\_}2\mathtt{\ in\ }\langle
N_{\\_}1,N_{\\_}2\rangle}|\end{split}$

and this implies $|{M_{\\_}2}|<|{M_{\\_}1}|$. ∎

Subject reduction entails linear strong normalization.

######  Theorem 8 (Linear strong normalization).

If $\mathcal{D}\triangleleft\Gamma\vdash M:A$ then $M$ reduces to a normal
form in at most $|{M}|$ reduction steps.

######  Remark 2.

By Newman’s Lemma (see [5]), confluence of $\rightarrow$ for typable terms
holds as a consequence of Theorem 8 and weak confluence, the latter being easy
to establish. Therefore, each typable term reduces to a _unique_ normal form.

###  4.2 Cubic $\forall$-Lazy Cut-Elimination

$\mathsf{LAM}$ is a subsystem of $\mathsf{IMALL}_{\\_}2$. Hence, from a purely
proof-theoretical viewpoint, the former inherits the cut-elimination rules of
the latter (see for example [7]). However, these proof rewriting rules for
$\mathsf{LAM}$ would be more permissive than the reduction rules for
$\Lambda_{\\_}{\mathtt{copy}}$, essentially because the $\mathtt{copy}$
construct can only duplicate values. The next examples illustrate this point.

######  Example 1.

Let us consider the following derivation of $\mathsf{LAM}$:

$y:\mathbf{1}\vdash y\mathbf{I}:\mathbf{1}$ $x_{\\_}1:\mathbf{1}\vdash
x_{\\_}1:\mathbf{1}$ $x_{\\_}2:\mathbf{1}\vdash x_{\\_}2:\mathbf{1}$
$\vdash\mathbf{I}:\mathbf{1}$ $\with$R$1$
$x:\mathbf{1}\vdash\mathtt{copy}^{\mathbf{I}}\,x\mathtt{\ as\
}x_{\\_}1,x_{\\_}2\mathtt{\ in\ }\langle
x_{\\_}1,x_{\\_}2\rangle:\mathbf{1}\with\mathbf{1}$ $cut$
$y:\mathbf{1}\vdash\mathtt{copy}^{\mathbf{I}}\,y\mathbf{I}\mathtt{\ as\
}x_{\\_}1,x_{\\_}2\mathtt{\ in\ }\langle
x_{\\_}1,x_{\\_}2\rangle:\mathbf{1}\with\mathbf{1}$ (17)

and let us apply the cut-elimination rule of $\mathsf{IMALL}_{\\_}2$ moving
the $cut$ upward. We get a derivation of $y:\mathbf{1}\vdash
M:\mathbf{1}\with\mathbf{1}$, where $M$ is
$\mathtt{copy}^{\mathbf{I}}\,y\mathtt{\ as\ }y_{\\_}1,y_{\\_}2\mathtt{\ in\
}\langle y_{\\_}1\mathbf{I},y_{\\_}2\mathbf{I}\rangle$. But
$\mathtt{copy}^{\mathbf{I}}\,y\mathbf{I}\mathtt{\ as\
}x_{\\_}1,x_{\\_}2\mathtt{\ in\ }\langle
x_{\\_}1,x_{\\_}2\rangle\not\rightarrow^{*}M$.

######  Example 2.

Let us consider the following derivation of $\mathsf{LAM}$:

$x_{\\_}1:\mathbf{1}\vdash x_{\\_}1:\mathbf{1}$ $x_{\\_}2:\mathbf{1}\vdash
x_{\\_}2:\mathbf{1}$ $\vdash\mathbf{I}:\mathbf{1}$ $\with$R$1$
$x:\mathbf{1}\vdash\mathtt{copy}^{\mathbf{I}}\,x\mathtt{\ as\
}x_{\\_}1,x_{\\_}2\mathtt{\ in\ }\langle
x_{\\_}1,x_{\\_}2\rangle:\mathbf{1}\with\mathbf{1}$ $z:\mathbf{1}\vdash
z:\mathbf{1}$ $\with$L$i$
$y:\mathbf{1}\with\mathbf{1}\vdash\pi_{\\_}1(y):\mathbf{1}$ $cut$
$x:\mathbf{1}\vdash\pi_{\\_}1(\mathtt{copy}^{\mathbf{I}}\,x\mathtt{\ as\
}x_{\\_}1,x_{\\_}2\mathtt{\ in\ }\langle x_{\\_}1,x_{\\_}2\rangle):\mathbf{1}$
(18)

and let us apply the principal cut-elimination rule for $\with$ in
$\mathsf{IMALL}_{\\_}2$. We get a cut with premises $x_{\\_}1:\mathbf{1}\vdash
x_{\\_}1:\mathbf{1}$ and $z:\mathbf{1}\vdash z:\mathbf{1}$. However, no
reduction rule rewrites $\pi_{\\_}1(\mathtt{copy}^{\mathbf{I}}\,x\mathtt{\ as\
}x_{\\_}1,x_{\\_}2\mathtt{\ in\ }\langle x_{\\_}1,x_{\\_}2\rangle)$ into
$x_{\\_}1$.

To circumvent the above mismatch between proof rewriting and term reduction,
we introduce the _$\forall$ -lazy cut-elimination rules_. They never eliminate
instances of $cut$ like (17) and (18), so that cut-elimination fails in
general. We then show that, by defining a special $\forall$-lazy cut-
elimination strategy with cubic cost, cut-elimination can be recovered in the
restricted case of derivations of $\forall$-lazy types (Theorem 13). This
result is analogous to the restricted (lazy) cut-elimination property for
derivations of lazy types discussed in Section 2.2. The crucial difference is
that, while Girard’s lazy types rule out both negative occurrences of
$\forall$ and positive occurrences of $\with$, the $\forall$-lazy types only
require the absence of negative $\forall$, as illustrated in Figure 4. This
allows us to nest instances of $\with$R$1$ in a derivation of $\mathsf{LAM}$
without incurring exponential proof normalization, as shown in Section 3.2 in
the case of term reduction.

|  negative $\forall$ |  positive $\with$
---|---|---
lazy types | $X$ | $X$
$\forall$-lazy types | $X$ | $\checkmark$
Figure 4: Lazy types vs $\forall$-lazy types.

######  Definition 7 ($\forall$-lazy cut-elimination rules).

  * •

With $(X,Y)$ we denote a $cut$ whose left (resp. right) premise is the
conclusion of an instance of the inference rule $X$ (resp. $Y$). Cuts are
divided into four classes: the _symmetric cuts_ are
$(\multimap\text{R},\multimap\text{L})$, $(\with\text{R}0,\with\text{L}i)$,
$(\forall\text{R},\forall\text{L})$ and those of the form $(X,ax)$ or
$(ax,Y)$, for some $X$ and $Y$; the _copy-first cuts_ have form
$(\with{R}1,\with\text{L}i)$; the critical cuts have form
$(X,\with\text{R}1)$, for some rule $X$; finally, the _commuting cuts_ are all
the remaining instances of $cut$.

  * •

Let the following be a critical cut:

$\mathcal{D}$ $\Gamma\vdash M:A$ $x_{\\_}1:A\vdash N_{\\_}1:B$
$x_{\\_}2:A\vdash N_{\\_}2:C$ $\vdash V:A$ $\with$R$1$
$x:A\vdash\mathtt{copy}^{V}\,x\mathtt{\ as\ }x_{\\_}1,x_{\\_}2\mathtt{\ in\
}\langle N_{\\_}1,N_{\\_}2\rangle:B\with C$ $cut$
$\Gamma\vdash\mathtt{copy}^{V}\,M\mathtt{\ as\ }x_{\\_}1,x_{\\_}2\mathtt{\ in\
}\langle N_{\\_}1,N_{\\_}2\rangle:B\with C$

It is called safe if $\Gamma=\emptyset$, and deadlock otherwise. Also, it is
called ready if it is safe and $\mathcal{D}$ is cut-free. In this case, since
$A$ is $\forall$-lazy, Proposition 2.2 implies $M\in\mathcal{V}$.

  * •

The _$\forall$ -lazy cut-elimination rules_ are defined as follows:

    * –

they correspond to the standard cut-elimination rules of $\mathsf{LL}$ for
commuting cuts and for the symmetric cuts
$(\multimap\text{R},\multimap\text{L})$, $(\forall\text{R},\forall\text{L})$,
$(X,ax)$ and $(ax,Y)$ (see e.g. [7]);

    * –

they are displayed in Figure 5 for the symmetric cut
$(\with\text{R}0,\with\text{L}i)$ and for those critical cuts
$(X,\with\text{R}1)$ which are ready;

    * –

there is no $\forall$-lazy cut-elimination rule for copy-first cuts and the
remaining critical cuts.

If $\mathcal{D}$ rewrites to $\mathcal{D}^{\prime}$ by a $\forall$-lazy cut-
elimination rule, we write $\mathcal{D}\rightsquigarrow\mathcal{D}^{\prime}$.
The reflexive and transitive closure of $\rightsquigarrow$ is
$\rightsquigarrow^{*}$.

The $\forall$-lazy cut-elimination rules prevent duplication of terms that are
not values, restoring a match between proof rewriting and term reduction. What
we are going to show is that any $\forall$-lazy derivation $\mathcal{D}$ can
be rewritten into a cut-free one by a specific strategy of $\forall$-lazy cut-
elimination steps. This implies that any instance of critical cut in
$\mathcal{D}$ (e.g. the deadlock in (17)) is eventually turned into a ready
cut, and that all instances of copy-first cuts like (18) are eventually turned
into $(\with\text{R}0,\with\text{L}i)$ cuts. The latter is due to the
replacement of $\with$R$1$ with $\with$R$0$ given by the $\forall$-lazy cut
elimination of ready cuts in Figure 5.

$\begin{aligned}
&(\with\text{R}0,\with\text{L}i)&&\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
50.07999pt\hbox{\vbox{\hbox{\vbox{\hbox{\hbox{\hskip 1.0pt\hbox{$\vdash
N_{\\_}1:A_{\\_}1$}\hskip 1.0pt}\hbox{\hskip 14.45377pt}\hbox{\hskip
1.0pt\hbox{$\vdash N_{\\_}2:A_{\\_}2$}\hskip 1.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to122.94785pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 8.96979pt\hbox{\hbox{\hskip
1.0pt\hbox{$\vdash\langle N_{\\_}1,N_{\\_}2\rangle:A_{\\_}1\with
A_{\\_}2$}\hskip 1.0pt}}}}\hbox{\hskip 14.45377pt}\vbox{\hbox{\hskip
10.54512pt\hbox{\hbox{\hskip 1.0pt\hbox{$\Gamma,x_{\\_}i:A_{\\_}i\vdash
M:B$}\hskip 1.0pt}\hbox{\hskip 14.45377pt}\hbox{\hskip
1.0pt\hbox{$i\in\\{1,2\\}$}\hskip 1.0pt}}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to162.17827pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip 1.0pt\hbox{$\Gamma,x:A_{\\_}1\with
A_{\\_}2\vdash M[\pi_{\\_}i(x)/x_{\\_}i]:B$}\hskip
1.0pt}}}}\vskip-0.8754pt\nointerlineskip\hbox{\hskip
8.96979pt\lower-0.2pt\hbox{}\hbox to290.61009pt{\xleaders\hrule\hfill}\lower
2.8754pt\hbox{\hskip 3.0pt$cut$}}\vskip-0.8754pt\nointerlineskip\hbox{\hskip
86.53285pt\hbox{\hbox{\hskip 1.0pt\hbox{$\Gamma\vdash M[\pi_{\\_}i\langle
N_{\\_}1,N_{\\_}2\rangle/x_{\\_}i]:B$}\hskip
1.0pt}}}}}\ignorespaces\rightsquigarrow\
\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
26.29pt\hbox{\vbox{\hbox{\hbox{\hskip 1.0pt\hbox{$\vdash
N_{\\_}i:A_{\\_}i$}\hskip 1.0pt}\hbox{\hskip 14.45377pt}\hbox{\hskip
1.0pt\hbox{$\Gamma,x_{\\_}i:A_{\\_}i\vdash M:B$}\hskip
1.0pt}}\vskip-0.8754pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox to152.8913pt{\xleaders\hrule\hfill}\lower
2.8754pt\hbox{\hskip 3.0pt$cut$}}\vskip-0.8754pt\nointerlineskip\hbox{\hskip
30.31633pt\hbox{\hbox{\hskip 1.0pt\hbox{$\Gamma\vdash
M[N_{\\_}i/x_{\\_}i]:B$}\hskip 1.0pt}}}}}\ignorespaces\\\ \\\
&(X,\with\text{R}1)&&\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
50.07999pt\hbox{\vbox{\hbox{\vbox{\hbox{\hskip 11.3249pt\hbox{\hskip
1.0pt\hbox{$\mathcal{D}^{\dagger}$}\hskip 1.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip
1.0pt}}\lower-0.5pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hbox{\hskip
1.0pt\hbox{$\vdash V:A$}\hskip 1.0pt}}}\hbox{\hskip
14.45377pt}\vbox{\hbox{\hbox{\hskip 1.0pt\hbox{$x_{\\_}1:A\vdash
N_{\\_}1:B_{\\_}1$}\hskip 1.0pt}\hbox{\hskip 14.45377pt}\hbox{\hskip
1.0pt\hbox{$x_{\\_}2:A\vdash N_{\\_}2:B_{\\_}2$}\hskip 1.0pt}\hbox{\hskip
14.45377pt}\hbox{\hskip 1.0pt\hbox{$\vdash U:A$}\hskip 1.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to240.2677pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 4.02872pt\hbox{\hbox{\hskip
1.0pt\hbox{$x:A\vdash\mathtt{copy}^{U}x\mathtt{\ as\
}x_{\\_}1,x_{\\_}2\mathtt{\ in\ }\langle
N_{\\_}1,N_{\\_}2\rangle:B_{\\_}1\with B_{\\_}2$}\hskip
1.0pt}}}}}\vskip-0.8754pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox to285.47035pt{\xleaders\hrule\hfill}\lower
2.8754pt\hbox{\hskip 3.0pt$cut$}}\vskip-0.8754pt\nointerlineskip\hbox{\hskip
37.623pt\hbox{\hbox{\hskip 1.0pt\hbox{$\vdash\mathtt{copy}^{U}V\mathtt{\ as\
}x_{\\_}1,x_{\\_}2\mathtt{\ in\ }\langle
N_{\\_}1,N_{\\_}2\rangle:B_{\\_}1\with B_{\\_}2$}\hskip
1.0pt}}}}}\ignorespaces\rightsquigarrow\
\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
73.5922pt\hbox{\vbox{\hbox{\vbox{\hbox{\vbox{\hbox{\hskip
11.3249pt\hbox{\hskip 1.0pt\hbox{$\mathcal{D}^{\dagger}$}\hskip 1.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip
1.0pt}}\lower-0.5pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hbox{\hskip
1.0pt\hbox{$\vdash V:A$}\hskip 1.0pt}}}\hbox{\hskip 14.45377pt}\hbox{\hskip
1.0pt\hbox{$x_{\\_}1:A\vdash N_{\\_}1:B_{\\_}1$}\hskip
1.0pt}}\vskip-0.8754pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox to137.59142pt{\xleaders\hrule\hfill}\lower
2.8754pt\hbox{\hskip 3.0pt$cut$}}\vskip-0.8754pt\nointerlineskip\hbox{\hskip
22.94896pt\hbox{\hbox{\hskip 1.0pt\hbox{$\vdash
N_{\\_}1[V/x_{\\_}1]:B_{\\_}1$}\hskip 1.0pt}}}}\hbox{\hskip
14.45377pt}\vbox{\hbox{\vbox{\hbox{\hskip 11.3249pt\hbox{\hskip
1.0pt\hbox{$\mathcal{D}^{\dagger}$}\hskip 1.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip
1.0pt}}\lower-0.5pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hbox{\hskip
1.0pt\hbox{$\vdash V:A$}\hskip 1.0pt}}}\hbox{\hskip 14.45377pt}\hbox{\hskip
1.0pt\hbox{$x_{\\_}2:A\vdash N_{\\_}2:B_{\\_}1$}\hskip
1.0pt}}\vskip-0.8754pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox to137.59142pt{\xleaders\hrule\hfill}\lower
2.8754pt\hbox{\hskip 3.0pt$cut$}}\vskip-0.8754pt\nointerlineskip\hbox{\hskip
22.94896pt\hbox{\hbox{\hskip 1.0pt\hbox{$\vdash
N_{\\_}2[V/x_{\\_}2]:B_{\\_}2$}\hskip
1.0pt}}}}}\vskip-1.21666pt\nointerlineskip\hbox{\hskip
22.94896pt\lower-0.2pt\hbox{}\hbox to260.40192pt{\xleaders\hrule\hfill}\lower
3.21666pt\hbox{\hskip
3.0pt$\with$R$0$}}\vskip-1.21666pt\nointerlineskip\hbox{\hskip
63.19934pt\hbox{\hbox{\hskip 1.0pt\hbox{$\vdash\langle
N_{\\_}1[V/x_{\\_}1],N_{\\_}2[V/x_{\\_}2]\rangle:B_{\\_}1\with
B_{\\_}2$}\hskip 1.0pt}}}}}\ignorespaces\end{aligned}$

Figure 5: $\forall$-lazy cut-elimination rules for
$(\with\text{R}0,\with\text{L}i)$ and for ready cuts, where
$\mathcal{D^{\dagger}}$ is cut-free.

The proposition below exploits the closure conditions introduced in Definition
4.

######  Proposition 9.

If $\mathcal{D}\triangleleft\Gamma\vdash M:A$ and $FV(A)=\emptyset$ then
$FV(\Gamma)=\emptyset$.

###### Proof.

By induction on $\mathcal{D}$ using the closure conditions (i)-(ii) in
Definition 4 and the conditions on linear additives. We only consider some
interesting cases. Suppose $\mathcal{D}$ ends with an instance of $\multimap$L
with premises $\Gamma^{\prime}\vdash N:B$ and $\Delta,x:C\vdash M^{\prime}:A$.
If $FV(A)=\emptyset$ then, by induction hypothesis,
$FV(\Delta)=FV(C)=\emptyset$. By applying the closure condition (i), we have
$FV(B)=\emptyset$. By applying, again, the induction hypothesis we have
$FV(\Gamma^{\prime})=\emptyset$, and hence $FV(\Gamma^{\prime},y:B\multimap
C,\Delta)=\emptyset$. Let us now consider the case where $\mathcal{D}$ ends
with an instance of $\with$L$i$ with premise
$\Gamma^{\prime},x_{\\_}i:B_{\\_}i\vdash M^{\prime}:A$ and conclusion
$\Gamma^{\prime},y:B_{\\_}1\with B_{\\_}2\vdash
M^{\prime}[\pi_{\\_}i(y)/x_{\\_}i]:A$. If $FV(A)=\emptyset$ then
$FV(\Gamma^{\prime})=\emptyset$ by induction hypothesis. Moreover, since
$B_{\\_}1\with B_{\\_}2$ is a closed $\forall$-lazy type, we conclude
$FV(\Gamma^{\prime},y:B_{\\_}1\with B_{\\_}2)=\emptyset$. ∎

The next lemmas are essential to ensure the restricted cut-elimination result
for $\forall$-lazy types.

######  Lemma 10.

Let $\mathcal{D}\triangleleft\Gamma\vdash M:A$ be a derivation whose only cuts
are either deadlocks or copy-first. If one of those cuts exists in
$\mathcal{D}$, then $\mathcal{D}$ is not $\forall$-lazy.

###### Proof.

First, we show that both the conclusion of a deadlock and the conclusion of a
copy-first cut cannot be $\forall$-lazy. It suffices to find a closed type in
the context of these judgments, since closed types must contain at least a
$\forall$ in positive position. Let

$\Delta\vdash N:B$ $x:B\vdash\mathtt{copy}^{V}x\mathtt{\ as\
}x_{\\_}1,x_{\\_}2\mathtt{\ in\ }\langle P,Q\rangle:C\with D$ $cut$
$\Delta\vdash\mathtt{copy}^{V}N\mathtt{\ as\ }x_{\\_}1,x_{\\_}2\mathtt{\ in\
}\langle P,Q\rangle:C\with D$

be a deadlock. By definition, we have $\Delta\neq\emptyset$. Since
$x:B\vdash\mathtt{copy}^{V}x\mathtt{\ as\ }x_{\\_}1,x_{\\_}2\mathtt{\ in\
}\langle N_{\\_}1,N_{\\_}2\rangle:C\with D$ is the conclusion of $\with$R$1$,
we have $FV(B)=\emptyset$. Hence $FV(\Delta)=\emptyset$, by Proposition 9.
Moreover, let

$x:B\vdash\mathtt{copy}^{V}x\mathtt{\ as\ }x_{\\_}1,x_{\\_}2\mathtt{\ in\
}\langle N_{\\_}1,N_{\\_}2\rangle:B_{\\_}1\with B_{\\_}2$
$\Delta,x:B_{\\_}1\with B_{\\_}2\vdash M[\pi_{\\_}i(x)/x_{\\_}i]:C$ $cut$
$\Delta,x:B\vdash M[\pi_{\\_}i(\mathtt{copy}^{V}x\mathtt{\ as\
}x_{\\_}1,x_{\\_}2\mathtt{\ in\ }\langle
N_{\\_}1,N_{\\_}2\rangle)/x_{\\_}i]:C$

be a copy-first cut. Its leftmost premise is the conclusion of $\with$R$1$, so
$B$ must be closed by definition.

Suppose now that $\mathcal{D}$ contains some cuts. Then it contains at least a
deadlock or a copy-first cut. In both cases, $\mathcal{D}$ contains a judgment
that is not $\forall$-lazy. Let $R_{\\_}1,\ldots R_{\\_}n$ be the sequence of
rule instances from $\Gamma\vdash M:A$ up to this judgment. We prove by
induction on $n$ that $\Gamma\vdash M:A$ cannot be $\forall$-lazy. The case
$n=0$ is trivial. If $n>0$, then we have two cases depending on $R_{\\_}n$. If
$R_{\\_}n$ is a cut, then it is either a deadlock or a copy-first cut, and its
conclusion cannot be $\forall$-lazy, so we apply the induction hypothesis. If
$R_{\\_}n$ is not a cut, we apply Proposition 2.1 and the induction
hypothesis. ∎

######  Lemma 11 (Existence of a safe cut).

Let $\mathcal{D}\triangleleft\Gamma\vdash M:A$ be a $\forall$-lazy derivation
whose only cuts are either critical or copy-first. Then:

  1. 1.

if $\mathcal{D}$ has critical cuts, then it has safe cuts;

  2. 2.

if $\mathcal{D}$ is free from critical cuts, then it is free from copy-first
cuts.

###### Proof.

Both points follow from Lemma 10. ∎

######  Definition 8 (Height and weight).

Let $\mathcal{D}\triangleleft\Gamma\vdash M:A$ be a derivation of
$\mathsf{LAM}$:

  * •

The weight of $\mathcal{D}$, written $\with(\mathcal{D})$, is the number of
instances of the rule $\with$R$1$ in $\mathcal{D}$.

  * •

Given a rule instance $R$ in $\mathcal{D}$, the _height of $R$_, written
$h(R)$, is the number of rule instances from the conclusion $\Gamma\vdash M:A$
of $\mathcal{D}$ upward to the conclusion of $R$. The height of $\mathcal{D}$,
written $h(\mathcal{D})$, is the largest $h(R)$ among its rule instances.

######  Lemma 12 (Eliminating a ready cut).

Let $\mathcal{D}\triangleleft\Gamma\vdash M:A$ be a $\forall$-lazy derivation
whose only cuts are either critical or copy-first. The following statements
hold:

  1. 1.

if $\mathcal{D}$ has critical cuts, then it has ready cuts;

  2. 2.

if $\mathcal{D}^{*}$ is obtained by eliminating a ready cut in $\mathcal{D}$,
then
$|\mathcal{D}^{*}|+2\cdot\with(\mathcal{D}^{*})<|\mathcal{D}|+2\cdot\with(\mathcal{D})$.

###### Proof.

Concerning point 1, by Lemma 11.1 $\mathcal{D}$ contains at least one safe
cut. Let $R$ be the one with maximal height, we display as follows:

$\mathcal{D}^{\prime}$ $\vdash N:B$ $\mathcal{D}_{\\_}1$ $x_{\\_}1:B\vdash
M_{\\_}1:B_{\\_}1$ $\mathcal{D}_{\\_}2$ $x_{\\_}2:B\vdash M_{\\_}2:B_{\\_}2$
$\mathcal{D}^{\prime\prime}$ $\vdash U:B$ $\with$R$1$
$x:B\vdash\mathtt{copy}^{U}x\mathtt{\ as\ }x_{\\_}1,x_{\\_}2\mathtt{\ in\
}\langle M_{\\_}1,M_{\\_}2\rangle:B_{\\_}1\with B_{\\_}2$ $cut$
$\vdash\mathtt{copy}^{U}N\mathtt{\ as\ }x_{\\_}1,x_{\\_}2\mathtt{\ in\
}\langle M_{\\_}1,M_{\\_}2\rangle:B_{\\_}1\with B_{\\_}2$ (19)

Since $B$ is a $\forall$-lazy type, $\mathcal{D}^{\prime}$ is a $\forall$-lazy
derivation. By Lemma 11.1 and maximality of $h(R)$, $\mathcal{D}^{\prime}$ has
no critical cut, hence $\mathcal{D}^{\prime}$ is cut-free by Lemma 11.2.
Therefore, $R$ is a ready cut.

As for point 2, let $\mathcal{D}^{*}$ be the derivation obtained by
eliminating a ready cut like (19) in $\mathcal{D}$ (see Figure 5). By Remark
1, $\mathcal{D}^{\prime\prime}$ is $\eta$-expanded, hence cut-free by
definition. Since both $\mathcal{D}^{\prime}$ and $\mathcal{D}^{\prime\prime}$
are $\forall$-lazy and cut-free, they have no instances of $\with$R$1$ by
Proposition 2.2, so that $\with(\mathcal{D^{*}})=\with(\mathcal{D})-1$.
Moreover, $|\mathcal{D}^{\prime}|\leq|\mathcal{D}^{\prime\prime}|$ by
Proposition 3.2. We have:
$2\cdot|\mathcal{D}^{\prime}|+|\mathcal{D}_{\\_}1|+|\mathcal{D}_{\\_}2|+3+2\cdot\with(\mathcal{D^{*}})<|\mathcal{D}|+2\cdot\with(\mathcal{D^{*}})+2=|\mathcal{D}|+2\cdot(\with(\mathcal{D}^{*})+1)$.
Therefore,
$|\mathcal{D}^{*}|+2\cdot\with(\mathcal{D^{*}})<|\mathcal{D}|+2\cdot\with(\mathcal{D})$.
∎

######  Theorem 13 (Cubic $\forall$-lazy cut-elimination).

Let $\mathcal{D}\triangleleft\Gamma\vdash M:A$ be a $\forall$-lazy derivation.
Then, the $\forall$-lazy cut-elimination reduces $\mathcal{D}$ to a cut-free
$\mathcal{D}^{\dagger}\triangleleft\Gamma\vdash M^{\dagger}:A$ in
$\mathcal{O}(|\mathcal{D}|^{3})$ steps.

###### Proof.

Let us define a $\forall$-lazy cut-elimination strategy divided into rounds.
At each round:

  1. {1}

we eliminate all the commuting instances of $cut$;

  2. {2}

if a symmetric instance of $cut$ exists, we eliminate it; otherwise, all
instances of $cut$ are either critical or copy-first, and we eliminate a ready
one, if any.

We now show that the above $\forall$-lazy cut-elimination strategy terminates
with a cut-free derivation. We proceed by induction on the lexicographical
order of the pairs
$\langle|\mathcal{D}|+2\cdot\with(\mathcal{D}),H(\mathcal{D})\rangle$, where
$H(\mathcal{D})$ is the sum of the heights $h(\mathcal{D}^{\prime})$ of all
subderivations $\mathcal{D}^{\prime}$ of $\mathcal{D}$ whose conclusion is an
instance of $cut$. During 1, every commuting $\forall$-lazy cut-elimination
step moves an instance of $cut$ upward, strictly decreasing $H(\mathcal{D})$
and leaving $|\mathcal{D}|+2\cdot\with(\mathcal{D})$ unaltered. During 2,
every symmetric $\forall$-lazy cut-elimination step shrinks $|\mathcal{D}|$.
If only critical and copy-first cuts are in $\mathcal{D}$ then, by Lemma 11.2,
either $\mathcal{D}$ has critical cuts or it is cut-free. In the former case,
by Lemma 12.1 a ready cut exists. By Lemma 12.2, if we apply the corresponding
$\forall$-lazy cut-elimination step
$\mathcal{D}\rightsquigarrow\mathcal{D}^{*}$, we have
$|\mathcal{D}^{*}|+2\cdot\with(\mathcal{D}^{*})<|\mathcal{D}|+2\cdot\with(\mathcal{D})$.

We now exhibit a bound on the number of $\forall$-lazy cut-elimination steps
from $\mathcal{D}$ to $\mathcal{D}^{\dagger}$. Generally speaking, we can
represent a $\forall$-lazy cut-elimination strategy as:

$\displaystyle\mathcal{D}=\mathcal{D}_{\\_}0\underset{cc_{\\_}0}{\rightsquigarrow^{*}}\mathcal{D}^{\prime}_{\\_}0\underset{src_{\\_}0}{\rightsquigarrow}\mathcal{D}_{\\_}1\,\cdots\underset{cc_{\\_}i}{\rightsquigarrow^{*}}\mathcal{D}^{\prime}_{\\_}{i}\underset{src_{\\_}i}{\rightsquigarrow}\mathcal{D}_{\\_}{i+1}\underset{cc_{\\_}{i+1}}{\rightsquigarrow^{*}}\cdots\,\mathcal{D}^{\prime}_{\\_}{n-1}\underset{src_{\\_}{n-1}}{\rightsquigarrow}\mathcal{D}_{\\_}n\underset{cc_{\\_}n}{\rightsquigarrow^{*}}\mathcal{D}^{\prime}_{\\_}{n}=\mathcal{D}^{*}$
(20)

where, for $0\leq i\leq n$ and $0\leq j\leq n-1$, $cc_{\\_}i$ denotes a
sequence of $\forall$-cut elimination steps applied to commuting cuts, while
$src_{\\_}j$ denotes a $\forall$-cut elimination step applied to either a
symmetric or a ready cut. A bound on the length of the sequence $cc_{\\_}i$ is
$|\mathcal{D}_{\\_}{i}|^{2}$ because every instance of rule in
$\mathcal{D}_{\\_}{i}$ can, in principle, be commuted with every other.
Moreover,
$|\mathcal{D}_{\\_}{j+1}|+2\cdot\with(\mathcal{D}_{\\_}{j+1})<|\mathcal{D}^{\prime}_{\\_}{j}|+2\cdot\with(\mathcal{D}^{\prime}_{\\_}j)$,
for every $0\leq j\leq n-1$. Finally, since
$|\mathcal{D}_{\\_}{i}|=|\mathcal{D}^{\prime}_{\\_}{i}|$ for all $0\leq i\leq
n$, we have $n\leq|\mathcal{D}|+2\cdot\with(\mathcal{D})\leq
3\cdot|\mathcal{D}|$. Therefore, the total number of $\forall$-lazy cut-
elimination steps in (20) is $O(|\mathcal{D}|\cdot|\mathcal{D}|^{2})$. ∎

Recalling that the normal form of a typable term in $\mathsf{LAM}$ exists by
Theorem 8 and is unique by Remark 2, we have the following straightforward
corollary.

######  Corollary 14.

Let $\mathcal{D}\triangleleft\Gamma\vdash M:A$ be a $\forall$-lazy derivation,
and let $M^{\dagger}$ be the normal form of $M$. Then:

  * •

$M^{\dagger}$ is free from instances of $\mathtt{copy}$ and $\pi_{\\_}i$;

  * •

if $\Gamma=\emptyset$ then $M^{\dagger}\in\mathcal{V}$.

###### Proof.

It suffices to observe that, if a $\forall$-lazy derivation
$\mathcal{D}\triangleleft\Gamma\vdash M:A$ rewrites to
$\mathcal{D}^{\prime}\triangleleft\Gamma\vdash M^{\prime}:A$ by a
$\forall$-lazy cut-elimination step, then $M\rightarrow^{*}M^{\prime}$ (we
consider terms up to $\alpha$-equivalence). By Theorem 13 a cut-free
$\mathcal{D}^{\dagger}$ exists such that
$\mathcal{D}^{\dagger}\triangleleft\Gamma\vdash M^{\dagger}:A$, for some
$M^{\dagger}$. We conclude by Proposition 2.2. ∎

As we already observed in Section 2.3, a $\mathtt{copy}$ construct behaves
quite like a suspended substitution. So, a normal form with shape
$\mathtt{copy}^{V}\,N\mathtt{\ as\ }x_{\\_}1,x_{\\_}2\mathtt{\ in\ }\langle
P,Q\rangle$ represents a substitution that cannot be performed. Corollary 14
states that, whenever a term has $\forall$-lazy type, its normal form is
always free from these “unevaluated” expressions. This result is analogous to
Girard’s linear normalization by lazy evaluation for terms having lazy type in
$\mathsf{IMALL}_{\\_}2$ (see Section 2.2). However, the above corollary allows
us to gain something more. On the one hand, indeed, $\mathsf{LAM}$’s typable
terms enjoy linear strong normalization (Theorem 8). Therefore, as opposed to
$\mathsf{IMALL}_{\\_}2$, the system $\mathsf{LAM}$ does not require specific
evaluation strategies to avoid exponential reductions. On the other hand, as
already remarked, the $\forall$-lazy types are more expressive than the lazy
ones (see Figure 4).

##  5 Comparing $\mathsf{LAM}$ and $\mathsf{IMLL}_{\\_}2$

Following [8], we exploit the mechanisms of linear erasure and duplication
studied by Mairson and Terui [18, 19] to define a sound translation of
$\mathsf{LAM}$ into $\mathsf{IMLL}_{\\_}2$ (Theorem 17). A fundamental result
of this section is Theorem 18, stating that derivations of $\mathsf{LAM}$ may
exponentially compress linear $\lambda$-terms of $\mathsf{IMLL}_{\\_}2$. On
the one hand, these results witness that the former system is not
algorithmically more expressive than the latter. On the other hand, in a way
similar to [8], they show that $\mathsf{LAM}$ is able to compactly represent
Mairson and Terui’s linear erasure and duplication.

###  5.1 Linear Erasure and Duplication in $\mathsf{IMLL}_{\\_}2$

Mairson has shown in [18] that $\mathsf{IMLL}$ is expressive enough to encode
boolean circuits. This result was later reformulated by Mairson and Terui in
$\mathsf{IMLL}_{\\_}2$ to prove results about the complexity of cut-
elimination [19], where the advantage of working with $\mathsf{IMLL}_{\\_}2$
is to assign uniform types to structurally related linear $\lambda$-terms. In
the latter encoding, the boolean values “true” and “false” are represented by
$\mathtt{tt}\triangleq\lambda x.\lambda y.x\otimes y$ and
$\mathtt{ff}\triangleq\lambda x.\lambda y.y\otimes x$ respectively, with type
$\mathbf{B}\triangleq\forall\alpha.\alpha\multimap\alpha\multimap\alpha\otimes\alpha$.
The key step of the encoding is the existence of an “eraser”
$\mathtt{E}_{\\_}{\mathbf{B}}$ and a “duplicator”
$\mathtt{D}_{\\_}{\mathbf{B}}$ for the Boolean data type $\mathbf{B}$:

$\displaystyle\mathtt{E}_{\\_}{\mathbf{B}}$ $\displaystyle\triangleq\lambda
z.\mathtt{let\ }z\mathbf{I}\mathbf{I}\mathtt{\ be\ }x\otimes y\mathtt{\ in\
}(\mathtt{let\ }y\mathtt{\ be\ }\mathbf{I}\mathtt{\ in\
}x):\mathbf{B}\multimap\mathbf{1}$ (21)
$\displaystyle\mathtt{D}_{\\_}{\mathbf{B}}$ $\displaystyle\triangleq\lambda
z.\mathtt{proj}_{\\_}1(z(\mathtt{tt}\otimes\mathtt{tt})(\mathtt{ff}\otimes\mathtt{ff})):\mathbf{B}\multimap\mathbf{B}\otimes\mathbf{B}$
(22) $\displaystyle\mathtt{proj}_{\\_}1$ $\displaystyle\triangleq\lambda
z.\mathtt{let\ }z\mathtt{\ be\ }x\otimes y\mathtt{\ in\ }(\mathtt{let\
}\mathtt{E}_{\\_}{\mathbf{B}}\,y\mathtt{\ be\ }\mathbf{I}\mathtt{\ in\
}x):(\mathbf{B}\otimes\mathbf{B})\multimap\mathbf{B}$ (23)

where $\mathtt{proj}_{\\_}1$ is the linear $\lambda$-term projecting the first
element of a pair. For $M\in\\{\mathtt{tt},\mathtt{ff}\\}$, we have
$\mathtt{E}_{\\_}{\mathbf{B}}\,M\rightarrow_{\\_}{\beta}^{*}\mathbf{I}$ and
$\mathtt{D}_{\\_}{\mathbf{B}}\,M\rightarrow^{*}_{\\_}\beta M\otimes M$. In
other words, linear erasure involves a stepwise “data consumption” process,
while linear duplication works “by selection and erasure”: it contains both
possible outcomes of duplication $\mathtt{tt}\otimes\mathtt{tt}$ and
$\mathtt{ff}\otimes\mathtt{ff}$, and it selects the desired pair by linearly
erasing the other one.

In [19], Mairson and Terui generalize the above mechanism of linear erasure
and duplication to the class of closed $\Pi_{\\_}1$ types:

######  Definition 9 ($\Pi_{\\_}1$ types [19]).

A type of $\mathsf{IMLL}_{\\_}2$ is a $\Pi_{\\_}1$ type if it contains no
negative occurrences of $\forall$.

Closed $\Pi_{\\_}1$ types represent _finite_ data types, because they admit
only finitely many closed and normal inhabitants. An example is $\mathbf{B}$,
representing the Boolean data type.

The fundamental result about closed $\Pi_{\\_}1$ types is the following:

######  Theorem 15 (Erasure and duplication [19]).

  1. 1.

For any closed $\Pi_{\\_}1$ type $A$ there is a linear $\lambda$-term
$\mathtt{E}_{\\_}{A}$ of type $A\multimap\mathbf{1}$ such that, for all closed
and normal inhabitant $M$ of $A$,
$\mathtt{E}_{\\_}{A}\,M\rightarrow_{\\_}{\beta}^{*}\mathbf{I}$.

  2. 2.

For any closed and _inhabited_ $\Pi_{\\_}1$ type $A$ there is a linear
$\lambda$-term $\mathtt{D}_{\\_}{A}$ of type $A\multimap A\otimes A$ such
that, for all closed and normal inhabitant $M$ of $A$,
$\mathtt{D}_{\\_}{A}\,M\rightarrow_{\\_}{\beta\eta}^{*}M\otimes M$.

We call $\mathtt{E}_{\\_}A$ eraser and $\mathtt{D}_{\\_}A$ duplicator of $A$.
Intuitively, by taking as input a closed and normal inhabitant $M$ of closed
$\Pi_{\\_}1$ type $A$, $\mathtt{D}_{\\_}A$ implements the following three main
operations:

  1. (1)

“expand” $M$ to an $\eta$-long normal form of $A$, let us say $M^{\prime}$;

  2. (2)

compile $M^{\prime}$ to a linear $\lambda$-term $\lceil M^{\prime}\rceil$
which encodes $M^{\prime}$ as a boolean tuple;

  3. (3)

copy and decode $\lceil M^{\prime}\rceil$ obtaining $M^{\prime}\otimes
M^{\prime}$, which $\eta$-reduces to $M\otimes M$.

Point 3 implements Mairson and Terui’s “duplication by selection and erasure”
discussed for the type $\mathbf{B}$, and requires a nested series of if-then-
else playing the role of a look-up table that stores all pairs of closed and
normal inhabitants of $A$ (which are always finite, as already observed). Each
pair represents a possible outcome of duplication. Given a boolean tuple
$\lceil M^{\prime}\rceil$ as input, the nested if-then-else select the
corresponding pair $M^{\prime}\otimes M^{\prime}$, erasing all the remaining
“candidates”. The inhabitation condition for $A$ stated in Theorem 15.2
assures the existence of a default pair $N\otimes N$, a sort of “exception”
that we “throw” if the boolean tuple in input encodes no closed normal
inhabitant of $A$.

Point 2 of Theorem 15 was only sketched in [19]. A detailed proof of the
construction of $\mathtt{D}_{\\_}A$ is in [8], which also estimates the
complexity of duplicators and erasers:

######  Proposition 16 (Size of $\mathtt{E}_{\\_}A$ and $\mathtt{D}_{\\_}{A}$
[8]).

If $A$ is a closed $\Pi_{\\_}1$ type, then
$|\mathtt{E}_{\\_}{A}|\in\mathcal{O}(|A|)$. Moreover, if $A$ is inhabited,
then $|\mathtt{D}_{\\_}{A}|\in\mathcal{O}(2^{|A|^{2}})$.

###  5.2 A Translation of $\mathsf{LAM}$ Into $\mathsf{IMLL}_{\\_}2$ and
Exponential Compression

Following [8], we define a translation $(\\_)^{\bullet}$ from derivations of
$\mathsf{LAM}$ into linear $\lambda$-terms with type in
$\mathsf{IMLL}_{\\_}2$. It maps closed $\forall$-lazy types into closed
$\Pi_{\\_}1$ types, and instances of the inference rules $\with$R$1$ and
$\with$L$i$ into, respectively, duplicators and erasers of closed $\Pi_{\\_}1$
types. We prove that the translation is sound and the linear $\lambda$-term
$\mathcal{D}^{\bullet}$ associated with a derivation $\mathcal{D}$ of
$\mathsf{LAM}$ has size that can be exponential with respect to the size of
$\mathcal{D}$.

######  Definition 10 (From $\mathsf{LAM}$ to $\mathsf{IMLL}_{\\_}2$).

We define a map $(\\_)^{\bullet}$ translating a derivation
$\mathcal{D}\triangleleft\Gamma\vdash M:A$ of $\mathsf{LAM}$ into a linear
$\lambda$-term $\mathcal{D}^{\bullet}$ such that
$\Gamma^{\bullet}\vdash\mathcal{D}^{\bullet}:A^{\bullet}$ is derivable in
$\mathsf{IMLL}_{\\_}2$.

  1. 1.

The map $(\\_)^{\bullet}$ is defined on types of $\Theta_{\\_}\with$ by
induction on their structure:

$\displaystyle\alpha^{\bullet}$ $\displaystyle\triangleq\alpha\ $
$\displaystyle(A\with B)^{\bullet}$ $\displaystyle\triangleq
A^{\bullet}\otimes B^{\bullet}$ $\displaystyle(A\multimap B)^{\bullet}$
$\displaystyle\triangleq A^{\bullet}\multimap B^{\bullet}$
$\displaystyle(\forall\alpha.A)^{\bullet}$
$\displaystyle\triangleq\forall\alpha.A^{\bullet}\enspace.$

Notice that $(A\langle B/\alpha\rangle)^{\bullet}=A^{\bullet}\langle
B^{\bullet}/\alpha\rangle$. If
$\Gamma=x_{\\_}1:A_{\\_}1,\ldots,x_{\\_}n:A_{\\_}n$, we set
$\Gamma^{\bullet}\triangleq
x_{\\_}1:A_{\\_}1^{\bullet},\ldots,x_{\\_}n:A_{\\_}n^{\bullet}$.

  2. 2.

The map $(\\_)^{\bullet}$ is defined on derivations
$\mathcal{D}\triangleleft\Gamma\vdash M:A$ of $\mathsf{LAM}$ by induction on
the last rule:

    1. (a)

if $\mathcal{D}$ is $ax$ with conclusion $x:A\vdash x:A$, then
$\mathcal{D}^{\bullet}\triangleq x$;

    2. (b)

if $\mathcal{D}$ has last rule $cut$ with premises
$\mathcal{D}_{\\_}1\triangleleft\Delta\vdash N:B$ and
$\mathcal{D}_{\\_}2\triangleleft\Sigma,x:B\vdash P:A$, where $M=P[N/x]$, then
$\mathcal{D}^{\bullet}\triangleq\mathcal{D}_{\\_}2^{\bullet}[\mathcal{D}_{\\_}1^{\bullet}/x]$;

    3. (c)

if $\mathcal{D}$ has last rule $\multimap$R with premise
$\mathcal{D}_{\\_}1\triangleleft\Gamma,x:B\vdash N:C$ and $M=\lambda x.N$,
then $\mathcal{D}^{\bullet}\triangleq\lambda x.\mathcal{D}_{\\_}1^{\bullet}$;

    4. (d)

if $\mathcal{D}$ has last rule $\multimap$L with premises
$\mathcal{D}_{\\_}1\triangleleft\Delta\vdash N:B$ and
$\mathcal{D}_{\\_}2\triangleleft\Sigma,x:C\vdash P:A$, where
$\Gamma=\Delta,\Sigma,y:B\multimap C$, then
$\mathcal{D}^{\bullet}\triangleq\mathcal{D}_{\\_}2^{\bullet}[y\mathcal{D}^{\bullet}_{\\_}1/x]$;

    5. (e)

if $\mathcal{D}$ has last rule $\with$R$0$ with premises
$\mathcal{D}_{\\_}1\triangleleft\vdash N_{\\_}1:B_{\\_}1$ and
$\mathcal{D}_{\\_}2\triangleleft\vdash N_{\\_}2:B_{\\_}2$ then
$\mathcal{D}^{\bullet}\triangleq\mathcal{D}_{\\_}1^{\bullet}\otimes\mathcal{D}_{\\_}2^{\bullet}$;

    6. (f)

if $\mathcal{D}$ has last rule $\with$L$i$ with premise
$\mathcal{D}_{\\_}1\triangleleft\Delta,x_{\\_}i:B_{\\_}{i}\vdash N:A$, where
$\Gamma=\Delta,x:B_{\\_}1\with B_{\\_}2$, then
$\mathcal{D}^{\bullet}\triangleq\mathtt{let\ }x\mathtt{\ be\ }x_{\\_}1\otimes
x_{\\_}2\mathtt{\ in\ }(\mathtt{let\
}\mathtt{E}_{\\_}{B^{\bullet}_{\\_}{3-i}}x_{\\_}{3-i}\mathtt{\ be\
}\mathbf{I}\mathtt{\ in\ }\mathcal{D}^{\bullet}_{\\_}1)$, where
$\mathtt{E}_{\\_}{B^{\bullet}_{\\_}{3-i}}$ is the eraser of
$B^{\bullet}_{\\_}{3-i}$;

    7. (g)

if $\mathcal{D}$ ends with $\with$R$1$ with premises
$\mathcal{D}_{\\_}1\triangleleft x_{\\_}1:B\vdash N_{\\_}1:B_{\\_}1$,
$\mathcal{D}_{\\_}2\triangleleft x_{\\_}2:B\vdash N_{\\_}2:B_{\\_}2$, and
$\mathcal{D}_{\\_}3\triangleleft\vdash V^{\bullet}:B^{\bullet}$ then
$\mathcal{D}^{\bullet}\triangleq\mathtt{\ let\
}\mathtt{D}_{\\_}{B^{\bullet}}x\mathtt{\ be\ }x_{\\_}1\otimes
x_{\\_}2\mathtt{\ in\
}\mathcal{D}_{\\_}1^{\bullet}\otimes\mathcal{D}_{\\_}2^{\bullet}$, where
$\mathtt{D}_{\\_}{B^{\bullet}}$ is the duplicator of $B^{\bullet}$;

    8. (h)

if $\mathcal{D}$ has last rule $\forall$R with premise
$\mathcal{D}_{\\_}1\triangleleft\Gamma\vdash M:B\langle\gamma/\alpha\rangle$
then $\mathcal{D}^{\bullet}\triangleq\mathcal{D}_{\\_}1^{\bullet}$;

    9. (i)

if $\mathcal{D}$ has last rule $\forall$L with premise
$\mathcal{D}_{\\_}1\triangleleft\Delta,x:B\langle C/\alpha\rangle\vdash M:A$,
where $\Gamma=\Delta,x:\forall\alpha.B$, then
$\mathcal{D}^{\bullet}\triangleq\mathcal{D}^{\bullet}_{\\_}1$.

######  Remark 3.

Points 22f-2g are well-defined. Indeed, since $B,B_{\\_}1,B_{\\_}2$ in both
points are closed and $\forall$-lazy, the types
$B^{\bullet},B_{\\_}1^{\bullet},B_{\\_}2^{\bullet}$ are closed $\Pi_{\\_}1$,
so that Theorem 15.1 assures the existence of
$\mathtt{E}_{\\_}{B_{\\_}{3-i}^{\bullet}}$. Moreover, the closed $\Pi_{\\_}1$
type $B^{\bullet}$ in point 22g is inhabited by the closed linear
$\lambda$-term $\mathcal{D}_{\\_}3^{\bullet}$. The latter is also normal,
since by Remark 1 $\mathcal{D}_{\\_}3$ is $\eta$-expanded (hence cut-free).
Therefore, Theorem 15.2 assures that $\mathtt{D}_{\\_}{B^{\bullet}}$ exists.

We now show that every $\forall$-lazy cut-elimination step applied to a
derivation $\mathcal{D}\triangleleft\Gamma\vdash M:A$ of $\mathsf{LAM}$ can be
simulated by a sequence of $\beta\eta$-reduction steps applied to
$\mathcal{D}^{\bullet}$.

######  Theorem 17 (Soundness of $(\\_)^{\bullet}$).

Let $\mathcal{D}$ be a derivation of $\mathsf{LAM}$. If
$\mathcal{D}\rightsquigarrow\mathcal{D}^{\prime}$ then
$\mathcal{D}^{\bullet}\rightarrow^{*}_{\\_}{\beta\eta}\mathcal{D}^{\prime\bullet}$.

###### Proof.

W.l.o.g. it suffices to consider the case where the last rule of $\mathcal{D}$
is the instance of $cut$ the $\forall$-lazy cut-elimination rule
$\mathcal{D}\rightsquigarrow\mathcal{D}^{\prime}$ is applied to. The only
interesting cases are the $\forall$-lazy cut-elimination rules in Figure 5.
So, suppose that $\mathcal{D}$ ends with a cut
$(\with\text{R}0,\with\text{L}i)$, where the premises of $\with\text{R}0$ are
$\mathcal{D}_{\\_}1\triangleleft\vdash N_{\\_}1:A_{\\_}1$ and
$\mathcal{D}_{\\_}2\triangleleft\vdash N_{\\_}2:A_{\\_}2$, and the premise of
$\with$L$i$ is $\mathcal{D}_{\\_}3\triangleleft\Gamma,x_{\\_}i:A_{\\_}i\vdash
M:B$. Since $\mathcal{D}_{\\_}{3-i}^{\bullet}$ is a closed linear
$\lambda$-term of closed $\Pi_{\\_}1$ type $A^{\bullet}_{\\_}{3-i}$, by
applying Theorem 15.1 and the reduction rules in (8) we have:

$\displaystyle\mathcal{D}^{\bullet}$ $\displaystyle=\mathtt{\ let\
}\mathcal{D}_{\\_}1^{\bullet}\otimes\mathcal{D}_{\\_}2^{\bullet}\mathtt{\ be\
}x_{\\_}1\otimes x_{\\_}2\mathtt{\ in\ }(\mathtt{let\
}\mathtt{E}_{\\_}{A^{\bullet}_{\\_}{3-i}}x_{\\_}{3-i}\mathtt{\ be\
}\mathbf{I}\mathtt{\ in\ }\mathcal{D}_{\\_}3^{\bullet})$
$\displaystyle\rightarrow_{\\_}\beta\mathtt{let\
}\mathtt{E}_{\\_}{A_{\\_}{3-i}}\mathcal{D}^{\bullet}_{\\_}{3-i}\mathtt{\ be\
}\mathbf{I}\mathtt{\ in\
}\mathcal{D}_{\\_}3^{\bullet}[\mathcal{D}_{\\_}i^{\bullet}/x_{\\_}i]$
$\displaystyle\rightarrow^{*}_{\\_}{\beta}\mathtt{let\ }\mathbf{I}\mathtt{\
be\ }\mathbf{I}\mathtt{\ in\
}\mathcal{D}_{\\_}3^{\bullet}[\mathcal{D}_{\\_}i^{\bullet}/x_{\\_}i]$
$\displaystyle\rightarrow_{\\_}{\beta}\mathcal{D}_{\\_}3^{\bullet}[\mathcal{D}_{\\_}i^{\bullet}/x_{\\_}i]=\mathcal{D}^{\prime\bullet}.$

Finally, suppose that $\mathcal{D}$ ends with a ready cut
$(X,\with\text{R}1)$, for some $X$, where the left premises of the $cut$ is
$\mathcal{D}_{\\_}1\triangleleft\vdash V:A$ and the premises of
$\with\text{R}1$ are $\mathcal{D}_{\\_}2\triangleleft x_{\\_}1:A\vdash
N_{\\_}1:B_{\\_}1$, $\mathcal{D}_{\\_}3\triangleleft x_{\\_}2:A\vdash
N_{\\_}2:B_{\\_}2$ and $\mathcal{D}_{\\_}4\triangleleft\vdash U:A$. Since the
cut is ready, $\mathcal{D}_{\\_}1$ must be cut-free, and hence
$\mathcal{D}_{\\_}1^{\bullet}$ is a closed and normal linear $\lambda$-term of
closed $\Pi_{\\_}1$ type $A^{\bullet}$. Therefore, by applying Theorem 15.2
and the reduction rules in (8), we have:

$\displaystyle\mathcal{D}^{\bullet}$ $\displaystyle=\mathtt{\ let\
}\mathtt{D}_{\\_}{A^{\bullet}}\mathcal{D}_{\\_}1^{\bullet}\mathtt{\ be\
}x_{\\_}1\otimes x_{\\_}2\mathtt{\ in\
}\mathcal{D}_{\\_}2^{\bullet}\otimes\mathcal{D}_{\\_}3^{\bullet}$
$\displaystyle\rightarrow^{*}_{\\_}{\beta\eta}\mathtt{\ let\
}\mathcal{D}_{\\_}1^{\bullet}\otimes\mathcal{D}_{\\_}1^{\bullet}\mathtt{\ be\
}x_{\\_}1\otimes x_{\\_}2\mathtt{\ in\
}\mathcal{D}_{\\_}2^{\bullet}\otimes\mathcal{D}_{\\_}3^{\bullet}$
$\displaystyle\rightarrow_{\\_}\beta\mathcal{D}_{\\_}2^{\bullet}[\mathcal{D}_{\\_}1^{\bullet}/x_{\\_}1]\otimes\mathcal{D}_{\\_}3^{\bullet}[\mathcal{D}_{\\_}1^{\bullet}/x_{\\_}2]=\mathcal{D}^{\prime\bullet}$

this concludes the proof. ∎

The above result stresses a fundamental advantage of $\mathsf{LAM}$ over
$\mathsf{IMLL}_{\\_}2$: as shown in both [19] and [8], the latter type system
requires an extremely complex linear $\lambda$-term to encode linear
duplication (see Theorem 16), while the former can compactly represent it by
means of typed terms with shape:

$\lambda x.\mathtt{copy}^{V}x\mathtt{\ as\ }x_{\\_}1,x_{\\_}2\mathtt{\ in\
}\langle x_{\\_}1,x_{\\_}2\rangle:A\multimap A\with A$ (24)

Moreover, linear erasure is expressed by the following simple typed term:

$\lambda x.\pi_{\\_}2(\langle x,\mathbf{I}\rangle):A\multimap\mathbf{1}$ (25)

This crucial aspect of $\mathsf{LAM}$ can be made apparent by estimating the
impact of the translation $(\\_)^{\bullet}$ on the size of derivations, and
hence the cost of “unpacking” the inference rules $\with$R$1$ and $\with$L$i$.

######  Theorem 18 (Exponential compression for $\mathsf{LAM}$).

Let $\mathcal{D}$ be a derivation in $\mathsf{LAM}$. Then,
$|\mathcal{D}^{\bullet}|=\mathcal{O}(2^{|\mathcal{D}|^{k}})$, for some $k\geq
1$.

###### Proof.

By structural induction on $\mathcal{D}$. The only interesting case is when
$\mathcal{D}$ ends with $\with$R$1$ with premises
$\mathcal{D}_{\\_}1\triangleleft x_{\\_}1:A\vdash N_{\\_}1:B_{\\_}1$,
$\mathcal{D}_{\\_}2\triangleleft x_{\\_}2:A\vdash N_{\\_}2:B_{\\_}2$ and
$\mathcal{D}_{\\_}3\triangleleft\vdash U:A$. By Definition 10,
$\mathcal{D}^{\bullet}=\mathtt{\ let\ }\mathtt{D}_{\\_}{A^{\bullet}}x\mathtt{\
be\ }x_{\\_}1\otimes x_{\\_}2\mathtt{\ in\
}\mathcal{D}_{\\_}1^{\bullet}\otimes\mathcal{D}_{\\_}2^{\bullet}$. By Remark
1, $\mathcal{D}_{\\_}3$ is $\eta$-expanded, so that $|A|\leq
2\cdot|\mathcal{D}_{\\_}3|$ by Proposition 3.1. Hence,
$|\mathtt{D}_{\\_}{A}|\in\mathcal{O}(2^{(2\cdot|{\mathcal{D}_{\\_}3}|)^{2}})$
by Proposition 16. We apply the induction hypothesis on $\mathcal{D}_{\\_}1$
and $\mathcal{D}_{\\_}2$ and conclude. ∎

##  6 Conclusions

We introduce $\mathsf{LAM}$, a type assignment system endowed with a weaker
version of the Linear Logic additive rules $\with$R and $\with$L, called
_linear additive rules_. We prove both linear strong normalization and a
restricted cut-elimination theorem. Also, we present a sound translation of
$\mathsf{LAM}$ into $\mathsf{IMLL}_{\\_}2$, and we study its complexity.

A future direction is to find linear additive rules based on the additive
connective $\oplus$, and to prove results similar to Theorem 8 and Theorem 13.
This goal turns out to be harder, due to the “classical flavor” of the
inference rule $\oplus$L, displayed below:

$\Gamma,x:A\vdash M:C$ $\Gamma,y:B\vdash N:C$ $\Gamma,z:A\oplus
B\vdash\mathtt{case}\ z\mathtt{\ of\ }[\mathtt{inj}_{\\_}1(z)\to M\ |\
\mathtt{inj}_{\\_}2(z)\to N]:C$

Let us discuss this point. The linear additive rule $\with$R$1$ prevents
exponential normalization by carefully controlling context-sharing, which
involves hidden contractions and is responsible for unrestricted duplication.
Finding a linear additive rule corresponding to $\oplus$L means controlling
the sharing of types in the right-hand side of the turnstile. But this sharing
hides a co-contraction, i.e. $C\otimes C\multimap C$, which requires fairly
different techniques to be tamed.

Interesting applications of linear additives are in the field of ICC, and
indeed they motivate the tools developed in the present paper. As already
discussed in the Introduction, variants of the additive rules expressing non-
determinism explicitly have been used to capture $\mathsf{NP}$ [20, 12, 21].
To the best of our knowledge, all these characterizations of $\mathsf{NP}$
crucially depend on the choice of a special evaluation strategy able to avoid
the exponential blow up described in Section 2.2. Linear additives can refine
[20, 12, 21], because they do not affect the complexity of normalization, and
so they allow for natural cost models that can be implemented with a
negligible overhead. A possible future work could be then to extend Soft Type
Assignment ($\mathsf{STA}$), a type system capturing $\mathsf{PTIME}$ [11],
with a non-deterministic variant of linear additives, and to show that Strong
Non-deterministic Polytime Soundness holds for the resulting system. This
would allow us to characterize $\mathsf{NP}$ in a “wider” sense, i.e.
independently of the reduction strategy considered.

In a probabilistic setting, similar goals have already been achieved. In [9]
Curzi and Roversi studied the type system $\mathsf{PSTA}$, an extension of
$\mathsf{STA}$ with a non-deterministic variant of the linear additive rules
obtained by replacing $\with$L$i$ with the following:

$\Gamma,x:A\vdash M:C$ $\Gamma,y:A\with A\vdash M[\pi(y)/x]:C$

and by considering the non-deterministic reduction rule
$M\leftarrow\pi(\langle M,N\rangle)\rightarrow N$ in place of
$\pi_{\\_}i(\langle M_{\\_}1,M_{\\_}2\rangle)\rightarrow M_{\\_}i$. It is
shown that, when $\mathsf{PSTA}$ is endowed with a probabilistic big-step
reduction relation, it is able to capture the probabilistic polytime functions
and problems independently of the reduction strategy.

## Acknowledgments

I would like to thank L. Roversi for the precious discussions about the topic,
and the anonymous reviewers for useful comments and suggestions. This work was
supported by a UKRI Future Leaders Fellowship, ‘Structure vs Invariants in
Proofs’, project reference MR/S035540/1.

## References

  * [1]
  * [2] Martín Abadi, Luca Cardelli, Pierre-Louis Curien & Jean-Jacques Lévy (1990): _Explicit Substitutions_.  In Frances E. Allen, editor: Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, USA, January 1990, ACM Press, pp. 31–46, 10.1145/96709.96712.
  * [3] Beniamino Accattoli (2017): _(In)Efficiency and Reasonable Cost Models_.  In Sandra Alves & Renata Wasserman, editors: 12th Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2017, Brasília, Brazil, September 23-24, 2017, Electronic Notes in Theoretical Computer Science 338, Elsevier, pp. 23–43, 10.1016/j.entcs.2018.10.003.
  * [4] Beniamino Accattoli & Ugo Dal Lago (2012): _On the Invariance of the Unitary Cost Model for Head Reduction_.  In Ashish Tiwari, editor: 23rd International Conference on Rewriting Techniques and Applications (RTA’12) , RTA 2012, May 28 - June 2, 2012, Nagoya, Japan, LIPIcs 15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 22–37, 10.4230/LIPIcs.RTA.2012.22.
  * [5] Henk Barendregt, Wil Dekkers & Richard Statman (2013): _Lambda calculus with types_.  Cambridge University Press, 10.1017/CBO9781139032636.
  * [6] Roel Bloo & Kristoffer H. Rose (1995): _Preservation of Strong Normalisation in Named Lambda Calculi with Explicit Substitution and Garbage Collection_.  In: IN CSN-95: COMPUTER SCIENCE IN THE NETHERLANDS, pp. 62–72.
  * [7] Torben Braüner & Valeria De Paiva (1996): _Cut-elimination for full intuitionistic linear logic_.  10, University of Cambridge, Computer Laboratory, 10.7146/brics.v3i10.19973.
  * [8] Gianluca Curzi & Luca Roversi (2020): _A type-assignment of linear erasure and duplication_.  Theoretical Computer Science 837, pp. 26–53, 10.1016/j.tcs.2020.05.001.
  * [9] Gianluca Curzi & Luca Roversi (2020): _Probabilistic Soft Type Assignment_.  arXiv preprint arXiv:2007.01733.
  * [10] Alejandro Díaz-Caro & Gilles Dowek (2013): _Non determinism through type isomorphism_.  arXiv preprint arXiv:1303.7334.
  * [11] Marco Gaboardi & Simona Ronchi Della Rocca (2009): _From light logics to type assignments: a case study_.  Logic Journal of the IGPL 17(5), pp. 499–530, 10.1093/jigpal/jzp019.
  * [12] Marco Gaboardi, Jean-Yves Marion & Simona Ronchi Della Rocca (2008): _Soft linear logic and polynomial complexity classes_.  Electronic Notes in Theoretical Computer Science 205, pp. 67–87, 10.1016/j.entcs.2008.03.066.
  * [13] Jean-Yves Girard (2017): _Proof-nets: the parallel syntax for proof-theory_.  In: Logic and Algebra, Routledge, pp. 97–124, 10.1201/9780203748671-4.
  * [14] Jean-Yves Girard & Yves Lafont (1987): _Linear logic and lazy computation_.  In: International Joint Conference on Theory and Practice of Software Development, Springer, pp. 52–66, 10.1007/BFb0014972.
  * [15] J Roger Hindley (1989): _BCK-combinators and linear $\lambda$-terms have types_.  Theoretical Computer Science 64(1), pp. 97–105, 10.1016/0304-3975(89)90100-X.
  * [16] Ross Horne (2019): _The sub-additives: A proof theory for probabilistic choice extending linear logic_.  In: 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 10.4230/LIPIcs.FSCD.2019.23.
  * [17] Ugo Dal Lago & Simone Martini (2006): _An Invariant Cost Model for the Lambda Calculus_.  In Arnold Beckmann, Ulrich Berger, Benedikt Löwe & John V. Tucker, editors: Logical Approaches to Computational Barriers, Second Conference on Computability in Europe, CiE 2006, Swansea, UK, June 30-July 5, 2006, Proceedings, Lecture Notes in Computer Science 3988, Springer, pp. 105–114, 10.1007/11780342_11.
  * [18] Harry G. Mairson (2004): _Linear Lambda Calculus and PTIME-completeness_.  J. Funct. Program. 14(6), pp. 623–633, 10.1017/S0956796804005131.
  * [19] Harry G. Mairson & Kazushige Terui (2003): _On the Computational Complexity of Cut-Elimination in Linear Logic_.  In Carlo Blundo & Cosimo Laneve, editors: Theoretical Computer Science, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 23–36, 10.1007/978-3-540-45208-9_4.
  * [20] Satoshi Matsuoka (2004): _Nondeterministic Linear Logic_.  arXiv preprint cs/0410029.
  * [21] François Maurel (2003): _Nondeterministic light logics and NP-time_.  In: International Conference on Typed Lambda Calculi and Applications, Springer, pp. 241–255, 10.1007/3-540-44904-3_17.
  * [22] Paul-André Melliès (1995): _Typed Lambda-Calculi with Explicit Substitutions May Not Terminate_.  In: Proceedings of the Second International Conference on Typed Lambda Calculi and Applications, TLCA ’95, Springer-Verlag, Berlin, Heidelberg, p. 328–334, 10.1007/BFb0014062.