# Linearity, Non-determinism and Solvability

Michele Pagani, Simona Ronchi Della Rocca

► To cite this version:

Michele Pagani, Simona Ronchi Della Rocca. Linearity, Non-determinism and Solvability. Funda- menta Informaticae, 2010, From Mathematical Beauty to the Truth of Nature: to Jerzy Tiuryn on his 60th Birthday, 103 (1-4), pp.173-202. 10.3233/FI-2010-324. hal-04670080

HAL Id: hal-04670080

https://hal.science/hal-04670080v1

Submitted on 11 Aug 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Linearity, Non-determinism and Solvability*

Michele Pagani

Laboratoire d'Informatique de Paris-Nord – Université Paris 13

michele.pagani@lipn.univ-paris13.fr

Simona Ronchi Della Rocca

Dipartimento di Informatica – Università di Torino

ronchi@di.unito.it

Abstract

We study the notion of solvability in the resource calculus, an extension of the λ-calculus modelling resource consumption. Since this calculus is non-deterministic, two different notions of solvability arise, one optimistic (angelical, may) and one pessimistic (demoniac, must). We give a syntactical, operational and logical characterization for the may-solvability and only a partial characterization of the must-solvability. Finally, we discuss the open problem of a complete characterization of the must-solvability.

# 1 Introduction

We investigate the notion of solvability in the resource calculus ($\Lambda^r$), an extension of the λ-calculus, where both the features of linearity and non-determinism are present. $\Lambda^r$ is a calculus allowing to model resource consumption. Namely, the argument of a function comes as a finite multiset of resources, which in turn can be either linear or reusable. A linear resource needs to be used exactly once, while a reusable one can be called ad libitum, also zero times. Hence, the evaluation of a function applied to a multiset of resources gives rise to different possible choices, because of the different possibilities of distributing the resources among the occurrences of the formal parameter. So the calculus is not deterministic, but rather than having a purely non-deterministic notion of evaluation, the reduction introduces a formal sum of terms, representing all possible results of a non-deterministic computation. The presence of linear resources not only is a further source of non-determinism but it also introduces a notion of failure of the computation, the empty sum, distinct from non-termination: whenever the number of the available resources does not fit exactly the number of occurrences of the variable abstracted in a redex, then this latter evaluates to the empty sum. The resource calculus is a useful framework for studying the notions of linearity and non-determinism, and the relation between them.

$\Lambda^r$ is an evolution of the calculus of multiplicities, this last introduced by Boudol in order to study the semantics of the lazy λ-calculus [Bou93]. Ehrhard

<footnote>*Partially founded by the Italian MIUR project CONCERTO and the French ANR projet blanc CHOCO, ANR-07-BLAN-0324.</footnote>
and Regnier designed the differential λ-calculus [ER03], drawing on insights gained from an analysis of some denotational models of linear logic. As the authors remarked, the differential λ-calculus seemed quite similar to Boudol's calculus of multiplicities. Indeed, this was formalized by Tranquilli, who defined the Λ<sup>r</sup> syntax, and showed a Curry-Howard correspondence between this calculus and Ehrhard and Regnier's differential nets [Tra08]. The main differences between Boudol's calculus and Λ<sup>r</sup> are that the former is equipped with explicit substitution and lazy operational semantics, while the latter is a true extension of the classical λ-calculus.

One way to appreciate the resource calculus is by observing the various subcalculi it contains. Intuitively, usual λ-calculus can be embedded into Λ<sup>r</sup> translating the application MN into M[N<sup>1</sup>], where [N<sup>1</sup>] represents the multiset containing one copy of the resource N, which is reusable (see the grammar of Figure 1(a)). Forbidding linear terms but allowing non-empty finite multisets of reusable terms yields a purely non-deterministic extension of λ-calculus, which recalls de' Liguoro and Piperno's λ<sub>⊕</sub>-calculus [dP95] (studied also in [BEM09]). This fragment is also a variant of Vaux's algebraic λ-calculus [Vau09] without coefficients, where one moreover forbids the formation of the zero sum.

We will deal extensively with this fragment (noted here Λ<sup>||</sup> and called parallel calculus), in fact all the results we have obtained for Λ<sup>r</sup> hold also for Λ<sup>||</sup>. On the other side, allowing only multisets of linear terms yields the linear fragment of Λ<sup>r</sup>, used by Ehrhard and Regnier for giving a quantitative account to λ-calculus β-reduction through Taylor expansion [ER06, ER08].

As far as the operational behaviour of Λ<sup>r</sup> is concerned, the properties of confluence and a sort of standardization have been proved in [PT09]. In fact, confluence does not clash with non-determinism since, as written above, the outcome of a computation is a sum carrying all the possible results.

In this paper we will study the solvability property. Following the λ-calculus terminology, the word *solvable* denotes a term that can interact operationally with the environment, i.e., that can produce a given output when inserted into a context supplying it with suitable resources. According to this definition, in a computer science setting the solvable terms represent the meaningful programs.

In the λ-calculus, a closed term M is called solvable if and only if there is a sequence of arguments N such that MN reduces to the identity. λ-solvability has been completely characterized, by different points of view. Syntactically, a term is solvable if and only if it reduces to a head-normal form [Bar84], operationally, if and only if the head reduction strategy applied to it eventually stops [Bar84], logically, if and only if it can be typed in a suitable intersection type assignment system [CDCV81], denotationally, if and only if its denotation is not minimal in a suitable sensible model [Hyl76, RDRP04]. Our aim is to characterize the notion of solvability in Λ<sup>r</sup> and Λ<sup>||</sup>, following the same lines.

Actually, because of the non-deterministic behaviour of the calculus, two different notions of solvability arise, one optimistic (angelical, may) and one pessimistic (demoniac, must). A closed term *M* is may-solvable if there is a sequence of bags *P* such that *MP* reduces to a sum in which *at least one* term of the sum is the identity, while it is must-solvable when in the final sum *all* the terms are the identity. We stress the two notions collapse and coincide with the usual notion of solvability in the fragment of Λ<sup>r</sup> corresponding to the λ-calculus.

Our result is a characterization of the may-solvability in Λ<sup>r</sup> (Theorem 25),
and a characterization of the must-solvability in $\Lambda^{\|}$ (Theorem 36).

Theorem 25 characterizes the may-solvability from a syntactical, operational and logical point of view. An extended notion of head-normal form can be defined (called *may-outer-normal form*), such that a term is solvable if and only if it can reduce to a term of such form. From an operational point of view, we use the notion of outer-reduction strategy, defined in [PT09], where no reduction is made inside reusable resources, and we prove that in order to reach the outer-normal form we can restrict ourselves to use just reduction strategies of this kind. Also, we give a logical characterization of solvability, through a type system, assigning to terms suitable non-idempotent intersection types.

The characterization of must-solvability is a difficult problem, since it would imply to separate between the empty sum and the non-terminating terms (see discussion in Section 5). We achieve a complete characterization of must-solvability only for $\Lambda^{\|}$, the parallel fragment of $\Lambda^r$, where all resources are reusable and there is no empty sum. Inside this fragment, we characterize the must-solvability from a syntactical, operational and logical point of view, through a notion of *must-outer-normal form*.

All these characterizations are conservative with respect to the $\lambda$-calculus.

The type assignment system characterizing may-solvability is strongly related to the relational semantics of linear logic. It can be seen, basically, as an extension to $\Lambda^r$ of the type system introduced by de Carvalho in the restricted case of $\lambda$-calculus [dC09]. On the other side, the type assignment system characterizing must-solvability is based on a type theory supplying a logical description of the $D_{\infty}$ model of Scott [Sco76, PRDR04].

The characterization of the may-solvability in $\Lambda^r$ has been already presented, in a preliminary version, at FOSSACS 2010 [PRDR10].

The paper is organized as follows. Section 2 contains a syntactical description of the resource calculus. Section 3 is dedicated to the definition of may- and must-solvability and of outer-normal form. In Section 4, the complete characterization of may-solvability is given. In Section 5, the problem of the characterization of the must-solvability is discussed, and its characterization is given, inside the non-deterministic fragment $\Lambda^{\|}$.

## 2 Resource $\lambda$-calculus

**The syntax of $\Lambda^r$.** Basically, we have three syntactical sorts: terms, that are in functional position, bags, that are in argument position and represent multisets of resources, and finite formal sums, that represent the possible results of a computation. Precisely, Figure 1(a) gives the grammar for generating the set $\Lambda^r$ of **terms** and the set $\Lambda^b$ of **bags** (which are in fact finite multisets of **resources** $\Lambda^{(1)}$) together with their typical VARIABLES. A resource can be linear (it must be used exactly once) or not (it can be used ad libitum, also zero times), in the last case it is written with a ! apex. Bags are multisets presented in multiplicative notation, so that $P \cdot Q$ is the multiset union, and $1 = []$ is the empty bag: that means, $P \cdot 1 = P$ and $P \cdot Q = Q \cdot P$. It must be noted though that we will never omit the dot ., to avoid confusion with application.

**Sums** are multisets in additive notation, with 0 referring to the empty multiset, so that: $M+0 = M$ and $M+N = N+M$. We use two different notations for multisets in order to underline the different role of bags and sums. The former
<figure><img src="image_2.png" /><figcaption>**Figure 1:** Syntax of the resource calculus.</figcaption></figure>

are multisets in argument position, while the latter are in functional position: the two define notions of parallel composition behaving quite differently, as we will see in a while.

An **expression** (whose set is denoted by $\Lambda^{(b)}$) is either a term or a bag. Though in practice only sums of terms are needed, for the sake of the proofs we also introduce sums of bags and of expressions. The symbol **Nat** denotes the set of natural numbers, so that $\text{Nat}\langle\Lambda^r\rangle$ (resp. $\text{Nat}\langle\Lambda^b\rangle$) can be seen as the set of finite formal sums of terms (resp. bags). In particular, for $n \in \text{Nat}$ and $A$ an expression, the writing $nA$ denotes the sum $A + \dots + A$. In writing $\text{Nat}\langle\Lambda^{(b)}\rangle$ we are abusing the notation, as it does not denote the **Nat**-module generated over $\Lambda^{(b)} = \Lambda^r \cup \Lambda^b$ but rather the union of the two **Nat**-modules. This amounts to say that sums may be taken only in the same sort. $\text{Nat}$

ntimes

we are abusing the notation, as it does not denote the Nat-module generated over $\Lambda^{(b)} = \Lambda^r \cup \Lambda^b$ but rather the union of the two Nat-modules. This amounts to say that sums may be taken only in the same sort.

The grammar for terms and bags does not include sums in any point, so that in a sense they may arise only as a top level constructor. However, as an inductive notation (and *not* in the actual syntax) we extend all the constructors to sums as shown in Figure 1(b). In fact, all constructors but the $(\cdot)^!$ are, as expected, linear in the algebraic sense, i.e. they commute with sums.<fnref n="1" /> In particular, we have that 0 is always absorbing but for the $(\cdot)^!$ constructor, in which case we have $[0!] = 1$. Notice the similarity between the equations $[0!] = 1$ and $[(M+N)!] = [M!] \cdot [N!]$ and, respectively, $e^0 = 1$ and $e^{x+y} = e^x \cdot e^y$: this is far from a coincidence, as the relation between Taylor expansion and linear logic semantics shows [ER08]. We refer to [Tra08, Tra09] for the mathematical intuitions underlying the resource calculus.

We adopt the usual $\lambda$-calculus conventions as in [Bar84]. Also, we use the

<footnote n="1">¹However, the constructors do not commute with bag product, i.e. $M(P \cdot Q) \neq MP + MQ$. This is a first motivation for the different multiset notation between sums and bags.</footnote>
$$ y\langle N/x \rangle := \begin{cases} N & \text{if } y = x, \quad (\lambda y.M)\langle N/x \rangle := \lambda y.(M\langle N/x \rangle), \\ 0 & \text{otherwise,} \quad (MP)\langle N/x \rangle := M\langle N/x \rangle P + M(P\langle N/x \rangle), \end{cases} $$

$$ [M]\langle N/x \rangle := [M\langle N/x \rangle], \quad 1\langle N/x \rangle := 0, $$

$$ [M']\langle N/x \rangle := [M\langle N/x \rangle, M'], \quad (P \cdot R)\langle N/x \rangle := P\langle N/x \rangle \cdot R + P \cdot R\langle N/x \rangle. $$

<caption>**Figure 2:** Linear substitution. In the abstraction case we suppose $y \notin \text{FV}(N) \cup \{x\}$.</caption>

following notation for terms useful to build examples:

$$ \mathbf{I} := \lambda x.x, \quad \mathbf{F} := \lambda xy.y, \quad \mathbf{\Delta} := \lambda x.x[x'], \quad \mathbf{\Omega} := \mathbf{\Delta}[\mathbf{\Delta}'] $$

There is no technical difficulty in defining $\alpha$-equivalence and the set $\text{FV}(\mathbf{A})$ of free variables as in ordinary $\lambda$-calculus. The symbol $=$ will denote the $\alpha$-equivalence between expressions.

The pair reusable/linear has a counterpart in the following two different notions of substitutions: their definition, hence that of reduction, heavily uses the notation of Figure 1(b).

**Definition 1 (Substitutions).** We define the following substitution operations.

1. $A\{N/x\}$ is the usual $\lambda$-calculus (i.e. capture free) substitution of $N$ for $x$. It is extended to sums as in $\mathbf{A}\{\mathbb{N}/x\}$ by linearity in $\mathbf{A}^2$ and using the notations of Figure 1(b) for $\mathbb{N}$. The form $A\{x + N/x\}$ is called **partial substitution**.

2. $A\langle N/x \rangle$ is the **linear substitution** defined inductively in Figure 2. It is extended to $\mathbf{A}\langle \mathbb{N}/x \rangle$ by bilinearity in both $\mathbf{A}$ and $\mathbb{N}$.

Roughly speaking, the linear substitution corresponds to the replacement of the resource to exactly one linear occurrence of the variable. In the presence of multiple occurrences, all the possible choices are made, and the result is the sum of them. For example $(y[x][x])\langle N/x \rangle = y[N][x] + y[x][N]$. In the case there are no free linear occurrences, then linear substitution returns 0, morally an error message. For example $(\lambda y.y)\langle N/x \rangle = \lambda y.(y\langle N/x \rangle) = \lambda y.0 = 0$. Finally, in case of reusable occurrences of the variable, linear substitution acts on a linear copy of the variable, e.g. $[x']\langle N/x \rangle = [N, x']$. Indeed linear substitution bears resemblance to differentiation, as it is in Ehrhard and Regnier's differential $\lambda$-calculus [ER03], so deriving a constant function (as is $\lambda y.y$ with respect to the parameter $x$) returns 0 and deriving a product of functions (as is $y[x][x]$ with respect to $x$) gives a sum. Also the rule $[M']\langle N/x \rangle = [M\langle N/x \rangle, M']$ resembles the chain rule. The following are examples with sums

$$ \begin{aligned} (x[x'])\langle (M+N)/x \rangle &= (x[x'])\langle M/x \rangle + (x[x'])\langle N/x \rangle \\ &= M[x'] + x[M, x'] + N[x'] + x[N, x'], \\ (x[x'])\{(M+N)/x\} &= (M+N)[(M+N)'] = M[M', N'] + N[M', N'.] \end{aligned} $$

Substitutions commute as stated in the following.

<footnote n="2">²$F(A)$ (resp. $F(A, B)$) is extended by linearity (resp. bilinearity) by setting $F(\sum_i A_i) = \sum_i F(A_i)$ (resp. $F(\sum_i A_i, \sum_j B_j) = \sum_{i,j} F(A_i, B_j)$).</footnote>
**Lemma 2** ([ER03, Tra08, Tra09]). For A a sum of expressions, M, N sums of terms and x, y variables such that $y \notin \text{FV}(M) \cup \text{FV}(N)$, we have

$$ (A\langle N/y \rangle)\langle M/x \rangle = (A\langle M/x \rangle)\langle N/y \rangle + A\langle N\langle M/x \rangle/y \rangle \\ (A\{y + N/y\})\langle M/x \rangle = (A\langle M/x \rangle)\{y + N/y\} + A\langle N\langle M/x \rangle/y \rangle \{y + N/y\}. $$

In particular, if $x \notin \text{FV}(N)$ then the second term of both sums is 0 and the two substitutions commute. Furthermore if $x \notin \text{FV}(M) \cup \text{FV}(N)$,

$$ (A\{x + M/x\})\{x + N/x\} = A\{x + M + N/x\} = (A\{x + N/x\})\{x + M/x\}. $$

**The reductions of $\Lambda^r$.** A (monic) context $C(\cdot)$ is a term that uses a distinguished free variable called its **hole** exactly once. Formally, the set of **simple contexts** is given by the following grammar

$$ \Lambda_{(.)}: \quad C(\cdot), D(\cdot) ::= (\cdot) \mid \lambda x.C(\cdot) \mid C(\cdot)P \mid M[C(\cdot)] \cdot P \mid M[(C(\cdot))'] \cdot P $$

A **context** $C(\cdot)$ is a simple context in $\Lambda_{(.)}$ summed to any sum in $\text{Nat}\langle\Lambda^r\rangle$. The expression $C(M)$ denotes the result of blindly replacing $M$ to the hole (allowing variable capture) in $C(\cdot)$. We generalize to sums applying the notations of Figure 1(b). For example $C(\cdot) := \lambda x.y[(\cdot)']$ and $D(\cdot) := \lambda x.y[(\cdot)]$ are simple contexts. If $M = x + y$, then $C(M) = \lambda x.y[x', y']$ and $D(M) = \lambda x.y[x] + \lambda x.y[y]$.

A relation $\tilde{r}$ in $\Lambda^r \times \text{Nat}\langle\Lambda^r\rangle$ is extended to one in $\text{Nat}\langle\Lambda^r\rangle \times \text{Nat}\langle\Lambda^r\rangle$ by **context closure**$^3$ by setting: $M \tilde{r} N$ iff $\exists C(\cdot)$ and $M' \tilde{r} N'$ such that $M = C(M')$, $N = C(N')$.

A context is **linear** if its hole is not under the scope of a $(\cdot)'$ operator. Linear contexts can be defined inductively omitting the case $M[(C(\cdot))'] \cdot P$ in the $\Lambda_{(.)}$ definition. An **outer-context** is a context having the hole not in a bag. Outer-contexts can be defined inductively omitting the cases $M[C(\cdot)] \cdot P$ and $M[(C(\cdot))'] \cdot P$ in the $\Lambda_{(.)}$ definition. Notice that the composition $C(D(\cdot))$ of two outer- (resp. linear) contexts $C(\cdot)$, $D(\cdot)$ is an outer- (resp. linear) context.

We define two kinds of reduction rule, baby-step and giant-step reduction, the former being a decomposition of the latter. Both are meaningful: baby-step is more atomic, performing one substitution at a time, while the giant-step is closer to $\lambda$-calculus $\beta$-reduction, wholly consuming its redex in one shot.

**Definition 3** ([Tra08, Tra09]). The **baby-step reduction** $\xrightarrow{\text{b}}$ is defined by the context closure of the following relation (assuming $x$ not free in $N$):

$$ (\lambda x.M)1 \xrightarrow{\text{b}} M\{0/x\} \qquad (\lambda x.M)[N] \cdot P \xrightarrow{\text{b}} (\lambda x.M\langle N/x \rangle)P \\ (\lambda x.M)[N'] \cdot P \xrightarrow{\text{b}} (\lambda x.M\{N + x/x\})P $$

The **giant-step reduction** $\xrightarrow{\text{g}}$ is defined by the context closure of the following relation, for $\ell, n \ge 0$ (assuming $x$ not free in the $L_i$'s and $N_i$'s):

$$ (\lambda x.M)[L_1, \dots, L_\ell, N_1^!, \dots, N_n^!] \xrightarrow{\text{g}} M\langle L_1/x \rangle \dots \langle L_\ell/x \rangle \{N_1 + \dots + N_n/x\}. $$

In the case $n = 0$, the reduct is $M\langle L_1/x \rangle \dots \langle L_\ell/x \rangle \{0/x\}$. For any reduction $\xrightarrow{x}$, we denote by $\xrightarrow{x^+}$ and $\xrightarrow{x^*}$ its transitive and reflexive-transitive closure respectively.

<footnote>$^3$In [Tra08, Tra09] bag contexts are defined too, so that context closure extends a relation to $\text{Nat}\langle\Lambda^{(b)}\rangle \times \text{Nat}\langle\Lambda^{(b)}\rangle$. In fact we prefer to introduce the term contexts only, making clear that the set $\text{Nat}\langle\Lambda^r\rangle$ is the actual protagonist of the calculus. However, our choice is a matter of taste, affecting no main property of the calculus.</footnote>
<figure><img src="image_3.png" /><figcaption>**Figure 3:** An example of baby-step and giant-step reductions. We use the notation of Figure 1(b): after the first b-step the term $(\lambda x.(\Delta + x)[\Delta^!])[I]$ stands for $(\lambda x.\Delta[\Delta^!])[I] + (\lambda x.x[\Delta^!])[I]$, and the term after the following step is equal to $0 + (\lambda x.x[\Delta^!])[I]$. In fact 0 is the neutral element of the sum and $(\lambda x.\Delta[\Delta^!])[I] \xrightarrow{b} 0$.</figcaption></figure>

Notice that giant-step reduction is defined independently of the ordering of the linear substitutions, as shown by the substitution commutations stated in Lemma 2. Baby-step and giant-step reductions are clearly related to each other.

**Proposition 4** ([Tra08, Tra09]). We have $\xrightarrow{g} \subset \xrightarrow{b^*} \subset \xrightarrow{g^*g^*} \subset \xrightarrow{g^*}$, where the last denotes the relational composition between $\xrightarrow{g^*}$ and its inverse $\xrightarrow{g^*}$.

Figure 3 shows an example of baby-step and giant-step reduction sequences. The reader can check, in this example, that the two reductions are related to each other as stated in Proposition 4. By the way, let us mention that although giving the same normal forms, baby-step and giant-step reductions might have different properties: for example, the starting term in the Figure 3 is strongly normalizing for giant-step but only weakly normalizing for baby-step reduction (an infinite reduction sequence can be obtained by firing the $\Delta[\Delta^!]$ redex in the first term of the sum $(\lambda x.(\Delta + x)[\Delta^!])[I]$).

**The fragment $\Lambda^{\parallel}$**. We will consider a notable fragment of $\Lambda^r$, denoted by $\Lambda^{\parallel}$ and called the **parallel fragment**. It corresponds to a purely non-deterministic extension of $\lambda$-calculus which recalls de' Liguoro and Piperno's $\lambda_{\oplus}$-calculus [dP95]. Seeing the product of bags as a convolution product and taking into account that $[(M + N)^{!}] = [M^{!}] \cdot [N^{!}]$, the fragment $\Lambda^{\parallel}$ is also a fragment of Vaux's algebraic $\lambda$-calculus [Vau09], without coefficients nor zero sums.

$\Lambda^{\parallel}$ is defined permitting only non-empty bags with reusable resources and non-zero sums. Formally, this is obtained by replacing the grammar defining $\Lambda^b$ (Figure 1(a)) by the following:

$$ \Lambda^{b\parallel} : P, Q, R ::= [M^!] | P \cdot Q $$

and by considering only non-zero sums, i.e. the sets $\text{Nat}^+\langle\Lambda^{\parallel}\rangle$ and $\text{Nat}^+\langle\Lambda^{b\parallel}\rangle$ of formal sums with coefficients in the set $\text{Nat}^+$ of non-zero natural numbers.

Notice $\Lambda^{\parallel}$ is not closed under baby step reduction, since the latter can create empty bags. We therefore slightly adapt such a reduction as follows.

**Definition 5.** The middle-step reduction $\xrightarrow{m}$ is defined by the context closure of the following relation (assuming $x$ not free in $N$):

$$ (\lambda x.M)[N^!] \xrightarrow{m} M\{N/x\}, \quad (\lambda x.M)[N^!]\cdot[L^!] \cdot P \xrightarrow{m} (\lambda x.M\{N+x/x\})[L^!]\cdot P. $$
Clearly middle-step reduction does not alter $\Lambda^r$ operational semantics.

**Proposition 6.** We have $\mathbf{g} \stackrel{\mathbf{g}}{\subset} \mathbf{m}^* \stackrel{\mathbf{b}^*}{\subset} \mathbf{in} \Lambda^r$.

**The outer reduction.** The notion of head-reduction is extended to such a setting as follows.

**Definition 7 ([PT09]).** Let $\epsilon \in \{\mathbf{b}, \mathbf{g}, \mathbf{m}\}$. The outer $\epsilon$-reduction $\stackrel{\mathbf{g}}{\to}$ is the closure to linear contexts of the $\epsilon$ steps given in Definition 3 and 5.

Notice that an outer redex (i.e. a redex for $\stackrel{\mathbf{g}}{\to}$) is a redex not under the scope of a $(\cdot)^!$ constructor. For the terms in $\Lambda^\|$ (so in particular for the terms corresponding to the $\lambda$-terms) the outer redexes are exactly the head-redexes. However, in terms with linear resources it is possible to have outer redexes also in argument position, e.g. in $x[\mathbf{I}[y]]$.

# 3 May and Must Solvability

A $\lambda$-term is solvable whenever there is a outer-context reducing it to the identity [Bar84]. In the resource calculus, terms appear in formal sums, where repetitions do matter, so various notions of solvability arise, depending on the number of times one gets the identity. We deal extensively with the two different notions of solvability, related to a may and must operational semantics, respectively.

**Definition 8.** A simple term $M$ is **may-solvable** whenever there are a simple outer-context $C(\cdot)$ and a sum of terms $N$, possibly 0, such that $C(M) \stackrel{\mathbf{g}^*}{\to} \mathbf{I} + N$; $M$ is **must-solvable** whenever there are a simple outer-context $C(\cdot)$ and a number $n \neq 0$ such that $C(M) \stackrel{\mathbf{g}^*}{\to} n\mathbf{I}$. We will say $M$ is **may-solvable** (resp. **must-solvable**) in $\Lambda^\|$ in case the context $C(\cdot)$ is in $\Lambda^\|$.

The above definition considers the giant-step reduction, however, one can replace it with the baby-step or middle-step reductions, obtaining an equivalent notion of solvability, as easily argued from Proposition 4 and 6. The restriction to simple and outer-contexts is crucial: there are general contexts reducing constantly to $\mathbf{I}$, disregarding the term they are applied to. Let $\mathcal{C}(\cdot)$ be either the outer- but non-simple context $\mathbf{I}+(\cdot)[\mathbf{I}]$ or the simple but non-outer-context $(\lambda x.\mathbf{I})[(\cdot)^!]$; we have $\mathcal{C}(M) \stackrel{\mathbf{g}}{\to} \mathbf{I}$ for every term $M$.

Clearly, must-solvability implies the may-solvability but not vice versa. Consider, for example, the following reductions, where $\mathbf{I}$ and $\mathbf{\Omega}$ have been defined in the previous section:

$$ \mathbf{I}[\mathbf{I}, \mathbf{\Omega}] \stackrel{\mathbf{g}}{\to} 0 \qquad (1) $$

$$ \mathbf{I}[\mathbf{I}^1, \mathbf{\Omega}] \stackrel{\mathbf{g}}{\to} \mathbf{\Omega} \qquad (2) $$

$$ \mathbf{I}[\mathbf{I}, \mathbf{\Omega}^1] \stackrel{\mathbf{g}}{\to} \mathbf{I} \qquad (3) $$

$$ \mathbf{I}[\mathbf{I}^1, \mathbf{\Omega}^1] \stackrel{\mathbf{g}}{\to} \mathbf{I} + \mathbf{\Omega} \qquad (4) $$

We can reasonably guess that $\mathbf{\Omega}$ is neither may-solvable nor must-solvable (this will be proved in what follows), as well as any term reducing to 0. Hence, (1) and (2) give examples of unsolvable terms, (3) is both may- and must-solvable and
(4) is a may-solvable but not must-solvable term. One major outcome of this paper is the operational characterization of solvability by means of the following notions of outer normalizability.

**Definition 9.** An expression is an outer-normal form, onf for short, if it has no redex but under the scope of a ()'. The set onf can be defined inductively as follows.

$$ \frac{M \in \text{onf}}{\lambda x.M \in \text{onf}} \qquad \frac{P_i \in \text{onf}, \text{ for } i \le p}{xP_1 \dots P_p \in \text{onf}} \quad p \ge 0 \\ \frac{M \in \text{onf}}{1 \in \text{onf}} \qquad \frac{[M] \in \text{onf}}{[M^1] \in \text{onf}} \qquad \frac{P \in \text{onf}}{P \cdot Q \in \text{onf}} \qquad Q \in \text{onf} $$

A sum $M$ of terms is a **may-outer-normal form**, monf for short, whenever it contains a term in outer-normal form; $M$ is a **must-outer-normal form**, Monf for short, whenever it is a non-empty sum of outer-normal forms. A term $M$ is **may-/must-outer normalizable** iff it is reducible to a may-/must-outer-normal form.

Notice that the Monf are the normal forms with respect to the outer reductions defined in Definition 7. Let us restrict ourselves to consider resource terms which correspond to $\lambda$-terms, according to the standard correspondence recalled in the introduction. Then the two definitions of may and must solvability coincide, and they become the standard $\lambda$-solvability. Moreover the two notions of may and must-outer-normal form collapse, and they become the classical definition of head-normal form; indeed the only possible outer redex in such terms is the head-redex.

The term $\lambda x.y1[x^1, \Omega^1]$ is an onf, and it is must-solvable (hence may-solvable) via $(\lambda y.(\cdot))[\mathbf{F}^1][\mathbf{I}]$: indeed, $(\lambda y.(\lambda x.y1[x^1, \Omega^1]))[\mathbf{F}^1][\mathbf{I}] \xrightarrow{g} (\lambda x.\mathbf{F}1[x^1, \Omega^1])[\mathbf{I}] \xrightarrow{g} (\lambda x.\mathbf{I}[x^1, \Omega^1])[\mathbf{I}] \xrightarrow{g} \mathbf{I}[\mathbf{I}] + (\lambda x.\Omega)[\mathbf{I}] \xrightarrow{g^*} \mathbf{I} + 0 = \mathbf{I}$. The terms $\mathbf{F}[\mathbf{I}^1, \Omega^1]$, $\mathbf{I}[\mathbf{I}^1, \Omega^1]$ are not onf but the first is must-outer normalizable, the second is only may-outer normalizable (the former reducing to $\mathbf{I}$, the latter to $\mathbf{I} + \Omega$); indeed, the first is also must-solvable, the second only may-solvable. The terms $\mathbf{F}[x]$ or $\mathbf{I}[\Omega^1]$ are not may/must-outer normalizable: they reduce to 0 and $\Omega$, respectively.

The main result of this section is to prove that may-outer and must-outer normalizability entails may-solvability and must-solvability respectively (Theorem 13). Section 4 will prove the converse of this implication with respect to the may-solvability, while Section 5 discusses the case of the must-solvability, where the implication *must-solvable* $\Rightarrow$ *must-outer normalizable* does not hold in general but in $\Lambda^{\|}$.

In contrast to the $\lambda$-calculus, where having a head-normal form straightforwardly implies being solvable (see e.g. [Bar84]), Theorem 13 is not immediate, for two reasons. In the $\lambda$-calculus one can replace the head-variable of a onf with a term erasing all its arguments and returning the identity. In the resource calculus this is not possible, because of the linear resources, that cannot be erased but must be used. A further difficulty arises in the must case. In fact, given a term $M$ in must-outer normal form, one should define a simple outer-context $C(\cdot)$ such that $C(M) \xrightarrow{g^*} n_M \mathbf{I}$ for all terms $M$ in $M$. This is not at all obvious since the terms in $M$ can be quite different each other. Such a context is built in the proof of Lemma 12 and it is based on the notion of *resource* underlined
by this calculus. In Definition 10 we give a notion of query of resources of a onf,
then, roughly speaking, what Lemma 12 shows is that one can build for any
term M in the sum $\mathbb{M}$ a context $C_M(\cdot)$ such that $C_M(M') \xrightarrow{g^*} n_{M'} \mathbf{I}$ whenever
$M'$ is a term querying the same number of resources as M and $C_M(M') \xrightarrow{g^*} 0$
whenever $M'$ queries more resources than M. Then Theorem 13 is achieved
taking $C_M(\cdot)$ for M a term of the sum $\mathbb{M}$ querying the minimum amount of
resources among the simple terms in $\mathbb{M}$.

**Definition 10.** The query of resources of a onf $A$ is the number $r(A)$ of vari-
able occurrences (both bound and free) which are not under the scope of a ()'¹
constructor, i.e.:

$$
r(\lambda x.M) := r(M) \quad r(xP_1 \dots P_p) := 1 + \sum_{i=1}^{p} r(P_i)
$$

$$
r([M]) := r(M) \quad r([M^1]) := 0 \quad r(1) := 0 \quad r(P \cdot Q) := r(P) + r(Q)
$$

Clearly for any onf $y\vec{P}$ and term $N$, we have $r(y\vec{P}) = r(y\vec{P}[N^1])$.

**Lemma 11.** For every $n \in \text{Nat}$, let $\mathbf{X}_n := \lambda x_1 \dots x_{n+1} \cdot x_{n+1}[x_1^!, \dots, x_n^!].$ Let $A$ be a onf, $x$ be a variable free in $A$, and $n$ be any number greater than the size of $A$. Then $A \{\mathbf{X}_n/x\}$ g-reduces to a onf having the same query of resources as $A$ and no free occurrence of $x$.

*Proof.* By induction on the structure of $A$. The only interesting case is when $A = xP_1 \dots P_p$, where by hypothesis $p \le n$. By induction each $P_i \{\mathbf{X}_n/x\}$ g-reduces to a bag $\hat{P}_i$ in onf with query of resources equal to that of $P_i$, so

$$
M \{\mathbf{X}_n/x\} = \mathbf{X}_n(P_1 \{\mathbf{X}_n/x\}) \dots (P_p \{\mathbf{X}_n/x\}) \\
\xrightarrow{g^*} \lambda x_{n+1-p} \dots x_{n+1} \cdot x_{n+1} \hat{P}_1 \cdot \dots \cdot \hat{P}_p \cdot [x_{p+1}^!, \dots, x_n^!]
$$

The last term is a onf with query of resources equal to $1 + \sum_{i=1}^{p} r(\hat{P}_i) = 1 + \sum_{i=1}^{p} r(P_i) = r(M)$. $\square$

**Lemma 12.** Let $\mathbb{M}$ be a must-outer-normal form. There is a simple outer-context $C(\cdot)$ such that $C(\mathbb{M}) \xrightarrow{g^*} n\mathbf{I}$, for $n \in \text{Nat}^{>0}$. If moreover $\mathbb{M} \in \Lambda^{\|}$, then also $C(\cdot) \in \Lambda^{\|}$.

*Proof.* In fact we prove a stronger statement:

(*) let $\mathbb{M} = \sum_{i=1}^{m} M_i$ be a must-outer-normal form, s.t. $r(M_1) = \min_{i \le m} r(M_i)$, then there is a simple outer-context $C(\cdot)$ and numbers $\{n_i\}_{i \le m}$ such that for every $i \le m$,

1. $C(M_i) \xrightarrow{g^*} n_i \mathbf{I}$,

2. $r(M_i) \neq r(M_1) \Rightarrow n_i = 0$,

3. $n_1 \neq 0$.

We prove (*) by induction on $\sum_{i=1}^{m} r(M_i)$. The context $C(\cdot)$ is the composition
of the three contexts $D(\cdot)$, $E(\cdot)$, $F(\cdot)$ defined in the equations (5), (6), (7). The
contexts $D(\cdot)$ and $E(\cdot)$ are always in $\Lambda^{\|}$, while $F(\cdot)$ is in $\Lambda^{\|}$ if $\mathbb{M}$ is.
The first context reduces every $M_i$ to an applicative form. Let $\ell \ge 0$ be the maximal length of the prefixes of abstractions of the $M_i$'s and $x$ be a fresh variable, the context

$$D(\cdot) := (\cdot) \underbrace{[x^!][x^!]}_{\ell \text{ times}} \quad (5)$$

reduces each $M_i$ to a onf $\hat{M}_i$ of the form $y_i R_{i,1} \dots R_{i,r_i}$ having the same query of resources as $M_i$, indeed $r([x^!]) = 0$.

The second context mainly performs three tasks: it closes every bag $R_{i,1}, \dots, R_{i,r_i}$ (namely, it replaces all the free variables in the bags with closed terms), consequently, the head occurrence of $y_i$ will become the only free occurrence of a variable; the last task consists in gathering the contents of every bag $R_{i,1}, \dots, R_{i,r_i}$ into their product $R_{i,1} \dots R_{i,r_i}$. Let $J := \lambda x z . z [x^!]$ and notice that $JR[J^!]$ reduces to $JR$ for any bag $R$. Let $\{z_1, \dots, z_h\}$ be the free variables in $\sum_i \hat{M}_i$ (in particular every $y_i$ is in $\{z_1, \dots, z_h\}$), let $y$ be a fresh variable and $\ell$ be the size of $\sum_i \hat{M}_i$. Define the context

$$E(\cdot) := (\lambda z_1 \dots z_h(\cdot)) \underbrace{[\mathbf{X}_\ell^!][\mathbf{X}_\ell^!]}_{h \text{ times}} \underbrace{[J^!][J^!]}_{\ell+1 \text{ times}} [y^!]. \quad (6)$$

By Lemma 11 each $R_{i,j}\{\mathbf{X}_\ell/z_1\} \dots \{\mathbf{X}_\ell/z_h\}$ reduces to a closed onf $\hat{R}_{i,j}$ such that $r(\hat{R}_{i,j}) = r(R_{i,j})$. So we have, denoting the sequence $\{\mathbf{X}_\ell/y_1\} \dots \{\mathbf{X}_\ell/y_m\}$ simply as $\{\mathbf{X}_\ell/\vec{y}\}$:

$$ \begin{align*} E(y_i R_{i,1} \dots R_{i,r_i}) & \xrightarrow{g^*} \mathbf{X}_\ell (R_{i,1} \{\mathbf{X}_\ell/\vec{y}\}) \dots (R_{i,r_i} \{\mathbf{X}_\ell/\vec{y}\}) [J^!][J^!][y^!] \\ & \xrightarrow{g^*} \mathbf{X}_\ell \hat{R}_{i,1} \dots \hat{R}_{i,r_i} [J^!][J^!][y^!] \\ & \xrightarrow{g^*} (\lambda x_{r_i+1} \dots x_{\ell+1} x_{\ell+1} \hat{R}_{i,1} \dots \hat{R}_{i,r_i} \cdot [x_{r_i+1}^! , \dots , x_\ell^!]) [J^!][J^!][y^!] \\ & \xrightarrow{g^*} J \hat{R}_{i,1} \dots \cdot \hat{R}_{i,r_i} \cdot \underbrace{[J^! , \dots , J^!]}_{\ell-r_i} \underbrace{[J^!][J^!]}_{r_i} [y^!] \\ & \xrightarrow{g^*} y \hat{R}_{i,1} \dots \cdot \hat{R}_{i,r_i} \cdot [J^! , \dots , J^!]. \end{align*} $$

To sum up, the composition of $D(\cdot)$ and $E(\cdot)$ gives $E(D(\sum_{i=1}^m M_i)) \xrightarrow{g^*} \sum_{i=1}^m y Q_i$, where for every $i \le m$, $Q_i$ is a bag of closed terms and $r(y Q_i) = r(M_i)$. Notice also that both contexts $D(\cdot)$ and $E(\cdot)$ are in $\Lambda^\parallel$.

Every bag $Q_i$ can be decomposed into a bag $\hat{Q}_i = [L_{i,1}, \dots, L_{i,k_i}]$ of closed linear onf and a bag $\hat{\tilde{Q}}_i$ of closed exponentiated simple terms. Of course one or both between $\hat{Q}_i$ and $\hat{\tilde{Q}}_i$ can be equal to 1. For every $j \le k_1$ consider the following family $\mathcal{F}_j$, possibly empty, of pair of indexes:

$$\mathcal{F}_j := \{(i, h) \text{ s.t. } i \le m, h \le k_i \text{ and } r(L_{1,j}) \le r(L_{i,h})\}$$

Remark that $\sum_{(i,h) \in \mathcal{F}_j} r(L_{i,h}) < \sum_i r(M_i)$, hence in case $\mathcal{F}_j$ is non-empty we can apply the induction hypothesis on every $\mathbb{F}_j := \sum_{(i,h) \in \mathcal{F}_j} L_{i,h}$, choosing $L_{1,j}$ as the onf of minimal query of resources. This yields a family of simple outer contexts $\{C_j(\cdot)\}_{j \le k_1}$ such that for every $(i, h) \in \mathcal{F}_j$,
1. $C_j(L_{i,h}) \xrightarrow{g^*} n_{j,i,h} \mathbf{I}$,

2. $r(L_{i,h}) \neq r(L_{1,j}) \Rightarrow n_{j,i,h} = 0,$

3. $n_{j,1,j} \neq 0.$

Actually, since every $L_{i,h}$ is closed one can suppose each $C_j(\cdot)$ to be just ap-
plicative, i.e. of the form $(\cdot)P_{j,1} \dots P_{j,p_j}$. In the following, we will denote simply
by $\vec{P}_j$ the sequence of bags $P_{j,1} \dots P_{j,p_j}$. Let us define, with $z$ a fresh variable:

$$
H := \lambda z. \mathbf{I}[z \vec{P}_1] \dots [z \vec{P}_{k_1}].
$$

Notice that whenever $k_1 = 0$ (i.e. $Q_1$ contains no linear simple term), we do not
apply the induction hypothesis and we simply define $H := \lambda z.\mathbf{I}$, which is in $\Lambda^{\|}$.
Notice that $k_1$ is always equal to 0 in the case we started with a $\mathbb{M}$ in $\Lambda^{\|}$.

Let us consider $H Q_i$ for every $i \le m$. We claim that $H Q_i \xrightarrow{g^*} n_i \mathbf{I}$, with $n_1$ nonzero and whenever $r(Q_i) > r(Q_1)$, $n_i = 0$. Notice that $z$ occurs in $H$ linearly $k_1$ times and never exponentially. This means that whenever $k_i > k_1$ we have $H Q_i \xrightarrow{g^*} 0$, since $H$ does not succeed in using every linear term in $Q_i$.

Also in case $k_i < k_1$, we have $H Q_i \xrightarrow{g^*} 0$. Indeed, since $r(Q_i) \ge r(Q_1)$, if $k_i < k_1$ there should be a $L_{i,h} \in Q_i$ such that for every $L_{1,j} \in Q_1$, $r(L_{i,h}) > r(L_{1,j})$. This means for every $j \le k_1$, $(i,h) \in \mathcal{F}_j$ and hence $L_{i,h} \vec{P}_j \xrightarrow{g^*} 0$. Thus, denoting by $Q_i/L_{i,h}$ the bag obtained erasing $L_{i,h}$ in $Q_i$,

$$
\begin{align*}
H Q_i &\xrightarrow{\mathfrak{b}} \sum_{j=1}^{k_1} (\lambda z. \mathbf{I}[z \vec{P}_1] \dots [L_{i,h} \vec{P}_j] \dots [z \vec{P}_{k_1}]) Q_i / L_{i,h} \\
&\xrightarrow{\mathfrak{g}^*} \sum_{j=1}^{k_1} (\lambda z. \mathbf{I}[z \vec{P}_1] \dots 0 \dots [z \vec{P}_{k_1}]) Q_i / L_{i,h} = 0.
\end{align*}
$$

Finally, if $k_i = k_1$, we have $HQ_i \xrightarrow{g^*} \sum_{\sigma \in S_{k_1}} \mathbf{I}[L_{i,\sigma(1)}\vec{P}_1] \dots [L_{i,\sigma(k_1)}\vec{P}_{k_1}]$. For every permutation $\sigma \in S_{k_1}$, if for a $j \le k_1$ we have $r(L_{i,\sigma(j)}) \ne r(L_{1,j})$, then there should be $j' \le k_1$ (possibly $j' = j$) s.t. $r(L_{i,\sigma(j')}) > r(L_{1,j'})$, since by hypothesis $r(M_i) = \sum_{h=1}^{k_i} r(L_{i,h}) \ge \sum_{h=1}^{k_1} r(L_{1,h})$ and $k_i = k_1$. We deduce that $L_{i,\sigma(j')}\vec{P}_{j'}$ reduces to 0 and so $\mathbf{I}[L_{i,\sigma(1)}\vec{P}_1]\dots[L_{i,\sigma(k_1)}\vec{P}_{k_1}]$ does. Otherwise, for every $j \le k_1$, $r(L_{i,\sigma(j)}) = r(L_{1,j})$, and so $L_{i,\sigma(j)}\vec{P}_j \xrightarrow{g^*} n_{j,i,\sigma(j)}\mathbf{I}$, for a number $n_{j,i,\sigma(j)}$. We deduce $\mathbf{I}[L_{i,\sigma(1)}\vec{P}_1]\dots[L_{i,\sigma(k_1)}\vec{P}_{k_1}] \xrightarrow{g^*} (\prod_{j=1}^{k_1} n_{j,i,\sigma(j)})\mathbf{I}$. In particular, if $\sigma$ is the identity and $i=1$, then every $n_{j,i,\sigma(j)}$ is nonzero, and so it is $\prod_{j=1}^{k_1} n_{j,i,\sigma(j)}$. We conclude for an integer $n_i$:

$$
\sum_{\sigma \in S_{k_1}} \mathbf{I}[L_{i,\sigma(1)} \vec{P}_1] \dots [L_{i,\sigma(k_1)} \vec{P}_{k_1}] \xrightarrow{g^*} n_i \mathbf{I}.
$$

In particular, for $i=1$, $n_i$ is not zero. Moreover, if $n_i$ is nonzero, then there is
a permutation $\sigma \in S_{k_1}$ such that $\prod_{j=1}^{k_1} n_{j,i,\sigma(j)}$ is nonzero. This means that for
every $j \le k_1$ $r(L_{i,\sigma(j)}) = r(L_{1,j})$, and so $r(Q_i) = r(Q_1)$.

Finally, we define the third context, with $x$ a fresh variable:

$$
F(\cdot) := (\lambda y(\cdot))[\lambda x.H[x^1]], \quad (7)
$$
<figure><img src="image_4.png" /><figcaption>**Figure 4:** The type assignment system $\vdash_m$. The rules $\rightarrow \mathbf{I}_n$ and $!_n$ are parametrized by a natural number $n$, their 0-ary versions $\rightarrow \mathbf{I}_0$ and $!_0$ yield $\omega \rightarrow \tau$ and $\pi$ respectively.</figcaption></figure>

and we conclude: $F(yQ_i) \xrightarrow{g^*} HQ_i \xrightarrow{g^*} n_i \mathbf{I}$, where $n_i$ is nonzero in case $i=1$, and it is zero in case $r(Q_i) > r(Q_1)$. $\square$

Notice that linear resources play a crucial role in the above proof. For an example, consider the must-outer normal form $y[x] + y[x, \Omega^1]$. The resource context satisfying Lemma 12 is $C(\cdot) := (\lambda yx.\cdot)[\lambda k.\mathbf{I}[k]]$, indeed $C(y[x]) + C(y[x, \Omega^1])$ reduces to $2\mathbf{I}$. If you consider the $\lambda$-context $C^\lambda(\cdot) := (\lambda yx.\cdot)[(\lambda k.\mathbf{I}[k^1])^1]$, we have $C^\lambda(y[x]) + C^\lambda(y[x, \Omega^1]) \xrightarrow{g^*} 2\mathbf{I} + \lambda x.\Omega$.

**Theorem 13.** Let $M$ be a term with resources. If $M$ has a may-outer-normal form (resp. must-outer-normal form) then $M$ is may-solvable (resp. must-solvable); moreover, if $M \in \Lambda^\parallel$ then $M$ is may-solvable (resp. must-solvable) in $\Lambda^\parallel$.

*Proof.* By applying Lemma 12 to the outer-normal forms in a may/must-outer-normal form of $M$. $\square$

# 4 Characterization of May Solvability

In this section we study the converse of Theorem 13 for the "may" semantics: the properties of may-outer normalizability and may-solvability are equivalent in $\Lambda^r$ and in $\Lambda^\parallel$. The key ingredient we use is an intersection type system $\vdash_m$ assigning types to all and only the expressions having may-outer-normal form, so giving a complete characterization of may-solvability, from the syntactical, operational and logical point of view (Theorem 25).

The system $\vdash_m$ lacks idempotency $(\sigma \wedge \sigma \neq \sigma)$: in fact, we use the intersection as logical counterpart of the multiset union. The system has some similarities with that one in [BCL99], which supplies a logical semantics for the language in [Bou93]. The main logical difference between the two systems is that the one in [BCL99] is affine and describes a lazy operational semantics. In the restricted setting of $\lambda$-calculus similar non-idempotent systems have been considered starting from [CDCV80], e.g. [Kfo00, WDMT02, NM04, dC09].
**Definition 14.** The set of types is the union of the set of linear types and that of intersection types, given by the following grammars

$\sigma, \tau ::= a \mid \pi \rightarrow \sigma$ linear types

$\pi, \zeta ::= \sigma \mid \omega \mid \pi \wedge \zeta$ intersection types

where a ranges over a countable set of atoms and $\omega$ is a constant. We consider types modulo the equivalence $\sim$ generated by the following rules:

$$ \pi \wedge \zeta \sim \zeta \wedge \pi, \quad \pi \wedge \omega \sim \pi, \quad \pi_1 \wedge (\pi_2 \wedge \pi_3) \sim (\pi_1 \wedge \pi_2) \wedge \pi_3 $$

i.e., $\sim$ states that $\wedge$ defines a commutative monoid with $\omega$ as the neutral element. The last two rules allow us to consider n-ary intersections $\sigma_1 \wedge \dots \wedge \sigma_n$, for any $n \in \mathbf{Nat}$, $\omega$ being the 0-ary intersection.

A basis is a finite multiset of assignments of the shape $x : \sigma$, where $x$ is a variable and $\sigma$ is a linear type. Capital Greek letters $\Gamma$, $\Delta$ range over bases. We denote by $d(\Gamma)$ the set of variables occurring in $\Gamma$ and by $\Gamma$, $\Delta$ the multiset union between the bases $\Gamma$ and $\Delta$. A typing judgement is a sequent $\Gamma \vdash_m A : \pi$.

The $\vdash_m$ type assignment system derivates typing judgements for $\mathbf{Nat}\langle\Lambda^{(b)}\rangle$. Its rules are defined in Figure 4. Capital Greek letters $\Phi$, $\Psi$ range over derivations, $\Phi :: \Gamma \vdash_m A : \pi$ denoting a derivation $\Phi$ with conclusion $\Gamma \vdash_m A : \pi$.

Some comments are in order. The bases have a multiplicative behaviour, and there is no weakening nor contraction, in neither explicit nor implicit form. In the rule $!_n$ the parameter $n$ takes into account the number of times a reusable resource will be called, whereas the rule $\ell$ assigns just one type to the linear resource $M$. Duplication and erasure is handled at the level of types by the intersection. For example, in $(\lambda x.y)[M']$, $\lambda x.y$ is typed by $\omega \rightarrow \sigma$ (by the rules var and $\rightarrow I_0$), for some $\sigma$ and $[M']$ is typed by $\omega$ (by the rules 1 and $!_0$), and in $(\lambda x.y[x][x])[y']$, $\lambda x.y[x][x]$ is typed by $\sigma \wedge \sigma \rightarrow \tau$, using the rule $\rightarrow I_2$, and $[y']$ is typed by $\sigma \wedge \sigma$, using rule $!_2$, for any $\sigma$ and $\tau$.

All other rules are almost standard.

**Definition 15.** The measure of a derivation $\Phi$ is the number $m(\Phi)$ of axioms (i.e. var and 1 rules) in $\Phi$. The measure $m(A)$ of a sum of expressions $A$ is

$$ m(A) := \inf\{m(\Phi) ; \Phi :: \Gamma \vdash_m A : \pi, \text{ for } \Gamma \text{ a basis and } \pi \text{ a type}\}. $$

An easy inspection of the rules in Figure 4 will convince the reader that the shape of a type derivation is strictly related with that of the expression it types, as formally stated by the following lemma.

**Lemma 16 (Generation).** 1. $\Pi :: \Gamma \vdash_m x : \pi$ implies $\pi = \sigma$ and $\Gamma = x : \sigma$, and $\Pi$ is an instance of the axiom var.

2. $\Pi :: \Gamma \vdash_m 1 : \pi$ implies $\Pi$ is an instance of the axiom 1, hence $\Gamma = \emptyset$ and $\pi = \omega$.

3. $\Pi :: \Gamma \vdash_m \lambda x.M : \pi$ implies $\pi = (\sigma_1 \wedge \dots \wedge \sigma_n) \rightarrow \tau$ and $\Pi$ is an application of the rule $\rightarrow I_n$ with premise $\Pi' :: \Gamma, x : \sigma_1, \dots, x : \sigma_n \vdash_m M : \tau$; clearly, $m(\Pi) = m(\Pi')$.
4. $\Pi :: \Gamma \vdash_m MP : \pi$ implies $\pi = \sigma$, $\Gamma = \Gamma_1, \Gamma_2$ and $\Pi$ is an application of the rule $\rightarrow \mathbb{E}$ with premises $\Pi_1 :: \Gamma_1 \vdash_m M : \pi' \rightarrow \sigma$ and $\Pi_2 :: \Gamma_2 \vdash_m P : \pi'$ for an intersection type $\pi'$; also, $m(\Pi) = m(\Pi_1) + m(\Pi_2)$.

5. $\Pi :: \Gamma \vdash_m [M] \cdot P : \pi$ implies there are two derivations $\Pi_1 :: \Gamma_1 \vdash_m M : \sigma$ and $\Pi_2 :: \Gamma_2 \vdash_m P : \pi'$ such that $\pi = \sigma \wedge \pi'$, $\Gamma = \Gamma_1, \Gamma_2$ and $m(\Pi) = m(\Pi_1) + m(\Pi_2)$.

6. $\Pi :: \Gamma \vdash_m [M^1] \cdot P : \pi$ implies there are a number $n \ge 0$ of derivations $\Pi_i :: \Gamma_i \vdash_m M : \sigma_i$, and a derivation $\Pi_{n+1} :: \Gamma_{n+1} \vdash_m P : \pi'$ such that $\pi = \sigma_1 \wedge \dots \wedge \sigma_n \wedge \pi'$, $\Gamma = \Gamma_1, \dots, \Gamma_{n+1}$ and $m(\Pi) = \sum_{i=1}^{n+1} m(\Pi_i)$.

7. $\Pi :: \Gamma \vdash_m A : \pi$ implies there is an expression $A$ in the sum $A$ and a derivation $\Pi' :: \Gamma \vdash_m A : \pi$ such that $m(\Pi) = m(\Pi')$.

Notice in the above lemma that the cases of the bag decomposition (items 5, 6) refer to proofs that can be different from the subproofs of $\Pi$. This is due to the fact that bags can be broken up in various ways: different decompositions yield typing derivations having some swapped rules $\ell$ and $!_n$. Also, notice that terms and sums of terms are typed by linear types, bags and sums of bags by intersection types.

The following lemmata (Lemma 17-21) state basically that the typing system behaves well with respect to the substitutions of the resource calculus. They are needed to prove that typing judgements are invariant under baby, middle and giant-step reductions (Proposition 22).

**Lemma 17 (Linear Substitution).** Let $\Phi :: \Gamma, x : \tau \vdash_m A : \pi$ and $\Psi :: \Delta \vdash_m N : \tau$. There is a derivation $\mathcal{L}(\Phi, \Psi) :: \Gamma, \Delta \vdash_m A \langle N/x \rangle : \pi$ with $m(\mathcal{L}(\Phi, \Psi)) = m(\Phi) + m(\Psi) - 1$.

*Proof.* By induction on the structure of the derivation $\Phi$. We treat in detail only the case of a terminal $!_n$ rule. The base of induction is trivial: var is immediate, while 1 does not meet the condition of having $x : \tau$ in the basis. The cases $\rightarrow \mathbb{E}$, $\oplus$ are immediate consequences of the induction hypothesis, the cases $\rightarrow \mathbb{E}$, $\ell$ are easier variant of the $!_n$ case. So let us assume

$$ \Phi := \frac{\Gamma_i \vdash_m M : \sigma_i, \quad \text{for } 1 \le i \le n \quad \Gamma_P \vdash_m P : \zeta_{!_n}}{\Gamma_1, \dots, \Gamma_n, \Gamma_P \vdash_m [M^1] \cdot P : \sigma_1 \wedge \dots \wedge \sigma_n \wedge \zeta} $$

We suppose the underlined hypothesis $x : \tau$ is in $\Gamma_1$, i.e. $\Gamma_1 = \Gamma'_1, x : \tau$ (the case $x : \tau$ is in another $\Gamma_i$ or in $\Gamma_P$ being similar). Notice that supposing $x : \tau$ in $\Gamma_1$ entails $n \ge 1$. By induction there is $\mathcal{L}(\Phi_1, \Psi) :: \Gamma'_1, \Delta \vdash_m M \langle N/x \rangle : \sigma_1$ s.t. $m(\mathcal{L}(\Phi_1, \Psi)) = m(\Phi_1) + m(\Psi) - 1$. Let $M \langle N/x \rangle = \sum_{j=1}^k L_j$. By Generation (Lemma 16, item 7) $M \langle N/x \rangle$ must have a term (i.e. $k > 0$), say $L_1$, and a proof $\Phi'_1 :: \Gamma'_1, \Delta \vdash_m L_1 : \sigma_1$ s.t. $m(\Phi'_1) = m(\mathcal{L}(\Phi_1, \Psi))$. We define

$$ \mathcal{L}(\Phi, \Psi) := \frac{\Gamma'_1, \Delta \vdash_m L_1 : \sigma_1}{\Gamma_2, \dots, \Gamma_n, \Gamma_P \vdash_m [M^1] \cdot P : \sigma_2 \wedge \dots \wedge \sigma_n \wedge \zeta_{!_n}} \oplus \frac{\Gamma'_1, \Delta, \Gamma_2, \dots, \Gamma_n, \Gamma_P \vdash_m [L_1, M^1] \cdot P : \sigma_1 \wedge \dots \wedge \sigma_n \wedge \zeta}{\Gamma'_1, \Delta, \Gamma_2, \dots, \Gamma_n, \Gamma_P \vdash_m \sum_{j=1}^k [L_j, M^1] \cdot P : \sigma_1 \wedge \dots \wedge \sigma_n \wedge \zeta} $$
where by definition $[M\langle N/x\rangle, M^!\rangle \cdot P = \sum_{j=1}^k [L_j, M^!\rangle \cdot P$, and if $k=1$ the last $\oplus$ rule is omitted. Moreover, $m(\mathcal{L}(\Phi, \Psi)) = m(\Phi'_1) + m(\Phi_P) + \sum_{i=2}^n m(\Phi_i) = m(\mathcal{L}(\Phi_1, \Psi)) + m(\Phi_P) + \sum_{i=2}^n m(\Phi_i) = m(\Phi_1) + m(\Psi) - 1 + m(\Phi_P) + \sum_{i=2}^n m(\Phi_i) = m(\Phi) + m(\Psi) - 1$. $\square$

**Lemma 18 (Linear Expansion).** Let $\Phi :: \Gamma \vdash_m A \langle N/x \rangle : \pi$. There are a linear type $\tau$ and derivations $\Phi_1 :: \Gamma_1, x : \tau \vdash_m A : \pi$ and $\Phi_2 :: \Gamma_2 \vdash_m N : \tau$ with $\Gamma = \Gamma_1, \Gamma_2$.

*Proof.* By structural induction on the sum $A$. We detail the case $A = [M^!]\cdot P$, the other cases being easy variants. In this case, $A\langle N/x \rangle = [M\langle N/x \rangle, M^!\rangle \cdot P + [M^!]\cdot P\langle N/x \rangle$, so $\Phi$ types only one term of the sum $A\langle N/x \rangle$ through a $\oplus$ rule. Let us suppose this term is in $[M\langle N/x \rangle, M^!\rangle \cdot P$ (the case it is in $[M^!]\cdot P\langle N/x \rangle$ being easier), so being of the form $[M', M^!]\cdot P$, with $M\langle N/x \rangle = M' + M$. By Generation (Lemma 16, items 5 and 6) there is a derivation $\bar{\Phi}^1 :: \Gamma^1 \vdash_m M' : \sigma$ and a derivation $\bar{\Phi}^2 :: \Gamma^2 \vdash_m [M^!]\cdot P : \bar{\pi}$ s.t. $\Gamma = \Gamma^1, \Gamma^2, \pi = \sigma \wedge \bar{\pi}$ and $\bar{\Phi}^2$ ends in a $!_n$ rule with $n$ premises typing $M$ and one premise typing $P$. Possibly applying one $\oplus$ rule to $\bar{\Phi}^1$ we get a derivation of $\Gamma^1 \vdash_m M\langle N/x \rangle : \sigma$, hence by induction hypothesis we have $\bar{\Phi}_1^1 :: \Gamma_1^1, x : \tau \vdash_m M : \sigma$ and $\bar{\Phi}_2^1 :: \Gamma_2^1 \vdash_m N : \tau$. Then we define $\Phi_1 :: \Gamma_1, x : \tau \vdash_m [M^!]\cdot P : \pi$ as a $!_{n+1}$ rule with premise $\bar{\Phi}_1^1$ plus the premises of the $!_n$ rule ending $\bar{\Phi}^2$, and $\Phi_2$ as $\bar{\Phi}_2^1$. $\square$

**Lemma 19 (Partial Substitution).** Let $m \ge 0$, $\Phi :: \Gamma, x : \sigma_1, \dots, x : \sigma_m \vdash_m A : \pi$ and $\forall i \le m, \Psi_i :: \Delta_i \vdash_m N : \sigma_i$ with $\Delta = \Delta_1, \dots, \Delta_m$. There is $\mathcal{P}(\Phi, \Psi_{i \le m}) :: \Gamma, \Delta \vdash_m A \{(N+x)/x\} : \pi$ with $m(\mathcal{P}(\Phi, \Psi_{i \le m})) = m(\Phi) - m + \sum_{i=1}^m m(\Psi_i)$.

*Proof.* Like in the proof of Linear Substitution (Lemma 17), we do induction on the structure of $\Phi$. In the var case, we have $A = y$ and $m = 0$ or $1$. If $y \ne x$, then $m = 0$ and we set $\mathcal{P}(\Phi, \Psi_{i \le m}) = \Phi$. Otherwise, $y = x$, so $A\{N+x/x\} = N+x$. Hence we define $\mathcal{P}(\Phi, \Psi_{i \le m})$ by adding one $\oplus$ rule to $\Phi$ or to $\Psi_1$, depending whether $m=0$ or $m=1$. In both cases, we easily deduce $m(\mathcal{P}(\Phi, \Psi_{i \le m})) = m(\Phi) - m + \sum_{i=1}^m m(\Psi_i)$. The case 1 is the last rule is immediate.

As for the induction step we detail only the case of a terminal $!_n$ rule, the other cases being immediate or easier variants. So let

$$ \Phi := \frac{\frac{\vdots \quad \Phi_j}{\Gamma_j, \Gamma_j^x \vdash_m M : \tau_j, \text{ for } 1 \le j \le n} \quad \frac{\vdots \quad \Phi_{n+1}}{\Gamma_{n+1}, \Gamma_{n+1}^x \vdash_m P : \zeta}}{\Gamma, x : \sigma_1, \dots, x : \sigma_m \vdash_m [M^!]\cdot P : \tau_1 \wedge \dots \wedge \tau_n \wedge \zeta} !_n $$

where $\Gamma = \Gamma_1, \dots, \Gamma_{n+1}$ and $x : \sigma_1, \dots, x : \sigma_m = \Gamma_1^x, \dots, \Gamma_{n+1}^x$.<fnref n="4" /> Notice $m(\Phi) = \sum_{j=1}^{n+1} m(\Phi_j)$. For every $j \le n+1$, let $I^j$ be the set of $i \le m$ s.t. $x : \sigma_i$ is in $\Gamma_j^x, m^j$ being the cardinality of $I^j$, possibly 0. Notice $m = \sum_{j=1}^{n+1} m^j$. Let $\Delta_{I^j}$ be the multiset union of the $\Delta_i$ bases with $i \in I^j$. We apply the induction hypothesis to each pair $\Phi_j$ and $\Psi_{i \in I^j}$, getting a derivation $\mathcal{P}(\Phi_j, \Psi_{i \in I^j}) :: \Gamma_j, \Delta_{I^j} \vdash_m M\{N+x/x\} : \tau_j$ for every $j \le n$, and $\mathcal{P}(\Phi_{n+1}, \Psi_{I^{n+1}}) :: \Gamma_{n+1}, \Delta_{I^{n+1}} \vdash_m P\{N+x/x\} : \zeta$, such that $m(\mathcal{P}(\Phi_j, \Psi_{i \in I^j})) = m(\Phi_j) - m^j + \sum_{i \in I^j} m(\Psi_i)$ for

<footnote n="4">⁴Be careful not to confuse $m$ (the number of underlined occurrences of $x$) with $n$ (the number of premises typing $M$ in the $!_n$ rule).</footnote>
every $j \le n + 1$. Moreover, in case $m^j = 0$ we have $\mathrm{m}(\mathcal{P}(\Phi_j, \Psi_{i \in I^j})) = \mathrm{m}(\Phi_j)$. Let us shorten the notation, setting $\Delta_{I^j} = \bigsqcup_{i \in I^j} \Delta_i$.

As always, $M\{N+x/x\}$ (resp. $P\{N+x/x\}$) is generally a sum $\sum_{h=1}^k M_h$ (resp. $\mathbb{P}$). Let us suppose $k \ge 2$, the case $k=0$ not holding since $M\{N+x/x\}$ is typed and the case $k=1$ being immediate. Applying Generation (Lemma 16) to each $\mathrm{m}(\mathcal{P}(\Phi_j, \Psi_{i \in I^j}))$ we obtain a function $f: \{0, \dots, n-1\} \to \{0, \dots, k-1\}$, an term $P'$ in the sum $\mathbb{P}$, and a family of derivations $\Phi'_j :: \Gamma_j, \Delta_{I^j} \vdash_m M_{f(j)} : \tau_j$ for $j \le n$, and $\Phi'_{n+1} :: \Gamma_{n+1}, \Delta_{I^{n+1}} \Delta_i \vdash_m P' : \zeta$, s.t. $\mathrm{m}(\mathcal{P}(\Phi_j, \Psi_{i \in I^j})) = \mathrm{m}(\Phi'_j)$ for $j \le n+1$. For every $h \le k$, let $J_h = f^{-1}(h)$, and $l_h$ be the cardinality of $J_h$; for $h, 0 \le h < k$, let $\pi_0 = \zeta, \pi_{h+1} = \pi_h \wedge \bigwedge_{j \in f^{-1}(h+1)} \tau_j$, and $\bar{\Gamma}_0 = \Gamma_{n+1}, \bar{\Gamma}_{h+1} = \bar{\Gamma}_h, \Gamma_{f^{-1}(h)}$, and $\bar{\Delta}_0 = \Delta_{I^{n+1}}, \bar{\Delta}_{h+1} = \bar{\Delta}_h, \Delta_{j \in f^{-1}(h)}$, where, consistency as before, $\Gamma_{f^{-1}(h)}$ (resp. $\Delta_{j \in f^{-1}(h)}$) denotes the multiset union of the $\Gamma_j$ (resp. $\Delta_i$) bases with $j \in f^{-1}(h)$ (resp. $i \in \bigcup_{j \in f^{-1}(h)} I^j$). Recalling $\pi_k = \tau_1 \wedge \dots \wedge \tau_n \wedge \zeta = \pi$, we have $\mathcal{P}(\Phi, \Psi_{i \le m}) :=$

$$ \frac{\frac{\vdots \quad \Phi'_j \quad \vdots \quad \Phi'_{n+1}}{\Gamma_j, \Delta_{I^j} \vdash_m M_1 : \tau_j, \text{ for } j \in J_1 \quad \Gamma_{n+1}, \Delta_{I^{n+1}} \vdash_m P' : \zeta \quad \vdots \quad \bar{\Gamma}_1, \bar{\Delta}_1 \vdash_m [M_1^!]. P' : \pi_1}}{\Gamma_j, \Delta_{I^j} \vdash_m M_k : \tau_k, \text{ for } j \in J_k \quad \bar{\Gamma}_{k-1}, \bar{\Delta}_{k-1} \vdash_m [M_1^! , \dots , M_{k-1}^!]. P' : \pi_{k-1} \quad \vdots \quad \frac{\Gamma, \Delta \vdash_m [(M \{N+x/x\})^!]. P' : \tau_1 \wedge \dots \wedge \tau_n \wedge \zeta}{\Gamma, \Delta \vdash_m [(M \{N+x/x\})^!]. \mathbb{P} : \tau_1 \wedge \dots \wedge \tau_n \wedge \zeta} \oplus} \quad \Gamma_j \Delta_{I^j} \vdash_m \prod_{i \in I^j} m_i = m(\Phi) = m(\Psi) = m(\Psi_i) \quad \square $$

We have $\mathrm{m}(\mathcal{P}(\Phi, \Psi_{i \le m})) = \sum_{j=1}^{n+1} \mathrm{m}(\phi'_j) = \sum_{j=1}^{n+1} \mathrm{m}(\mathcal{P}(\Phi_j, \Psi_{i \in I^j})) = \sum_{j=1}^{n+1} (\mathrm{m}(\Phi_j) + \sum_{i \in I^j} \mathrm{m}(\Psi_i)) - \sum_{j=1}^{n+1} m^j = \mathrm{m}(\Phi) - m + \sum_{i=1}^m \mathrm{m}(\Psi_i). \quad \square$

The next lemmata have proofs similar to the previous Lemma 17-19 (by induction on the structure of $\mathbb{A}$ or $\Phi$). We omit their proofs.

**Lemma 20 (Partial Expansion).** Let $\Phi :: \Gamma \vdash_m \mathbb{A} \{N+x/x\} : \pi$, then there is a number $m \ge 0$, linear types $\tau_1, \dots, \tau_m$ and derivations $\Phi_1 :: \Gamma_1, x : \tau_1, \dots, x : \tau_m \vdash_m \mathbb{A} : \pi$ and $\Psi_i :: \Delta_i \vdash_m N : \tau_i$ for $i \le m$ and $\Gamma = \Gamma_1, \Delta_1, \dots, \Delta_m$.

**Lemma 21.** Let $x \notin d(\Gamma)$, then for every $\Phi :: \Gamma \vdash_m \mathbb{A} : \pi$ there is $\Psi :: \Gamma \vdash_m \mathbb{A} \{0/x\} : \pi$ with $\mathrm{m}(\Phi) = \mathrm{m}(\Psi)$, and vice versa.

The following proposition states that the type system $\vdash_m$ enjoys both subject reduction and subject expansion.

**Proposition 22 (Invariance of $\vdash_m$ typings).** Let $\epsilon \in \{\mathfrak{b}, \mathfrak{m}, \mathfrak{g}\}$ and $M \stackrel{\epsilon}{\to} \mathbb{M}$, then $M$ and $\mathbb{M}$ share the same judgements, i.e. $\Gamma \vdash_m M : \tau$ iff $\Gamma \vdash_m M : \tau$. Also, $M \stackrel{\mathrm{og}}{\to} \mathbb{M}$ entails $\mathrm{m}(M) > \mathrm{m}(\mathbb{M})$.

*Proof.* The proof is by induction on the context enclosing the redex reduced in $M \stackrel{\epsilon}{\to} \mathbb{M}$. All induction steps follow by induction, taking into account that, whenever the redex is inside a reusable resource $N^!$ (so the reduction is not outer) the measure $m$ may not decrease since (the bag containing) $N^!$ may be typed by $\omega$.

The base of induction is when $M$ is the redex fired by the reduction $M \stackrel{\epsilon}{\to} \mathbb{M}$. One can consider only the baby-step cases, the giant and the middle ones will
<figure><img src="image_5.png" /><figcaption>**Figure 5:** Definition of the derivations $\Psi$ and $\Phi$ used in the proof of Proposition 22 (case 2).</figcaption></figure>

follow since they correspond to a sequence of baby-steps. In particular, one
proves that the measure m is monotone strictly decreasing on every baby-step
but the one choosing a bang element from the bag, in which case m is monotone
decreasing (case 3 below). Then m strictly decreases on giant-steps since they
correspond to sequences of baby-steps ending always in an empty bag baby-step.

**Case 1 (empty bag).** Let $M = (\lambda x.L)1 \xrightarrow{\beta} L \{0/x\} = \mathbb{M}$, and suppose $\Psi :: \Gamma \vdash_m (\lambda x.L)1 : \sigma$. By Generation (Lemma 16) $\Psi$ ends in a $\rightarrow \mathbb{E}$ rule with premises $\Psi' :: \Gamma \vdash_m \lambda x.L : \omega \rightarrow \sigma$ and an instance of the 1 rule, and $m(\Psi) = m(\Psi') + 1$. Again by Generation $\Psi'$ ends in a $\rightarrow \mathbb{I}_0$ rule with premise $\Psi'' :: \Gamma \vdash_m L : \sigma$ and $x \notin d(\Gamma)$, $m(\Psi'') = m(\Psi')$. By Lemma 21 there is a derivation $\Phi :: \Gamma \vdash_m L \{0/x\} : \sigma$ with $m(\Phi) = m(\Psi'') = m(\Psi) - 1$. We conclude that the judgements of $(\lambda x.L)1$ are also of $L \{0/x\}$ and $m((\lambda x.L)1) \ge m(L \{0/x\}) + 1$.

Conversely, suppose $\Phi :: \Gamma \vdash_m L \{0/x\} : \sigma$. By definition of substitution, $L \{0/x\}$ is either 0 or a term with no free occurrence of $x$. The first hypothesis cannot hold, being $L \{0/x\}$ typable, hence $L \{0/x\}$ is a simple term having no free occurrence of $x$, so $x \notin d(\Gamma)$. Then we can apply Lemma 21, from which we deduce $\Psi :: \Gamma \vdash_m L : \sigma$. Adding to $\Psi$ one $\rightarrow \mathbb{I}_0$ rule, and then composing it with one 1 rule through a $\rightarrow \mathbb{E}$ yields a derivation $\Psi' :: \Gamma \vdash_m (\lambda x.L)1 : \sigma$. We thus conclude that $(\lambda x.L)1$ and $L \{0/x\}$ share the same types and $m((\lambda x.L)1) > m(L \{0/x\})$.

**Case 2 (bag with linear resource).** Let $M = (\lambda x.L)[N] \cdot P \xrightarrow{\beta} (\lambda x.L\langle N/x \rangle)P = \mathbb{M}$ and suppose $\Psi :: \Gamma \vdash_m (\lambda x.L)[N] \cdot P : \sigma$. By Generation (Lemma 16) we can assume $\Psi$ to be as in Figure 5(a), where by $\vec{x} : \vec{\tau}$ we are meaning $x : \tau_1, \dots, x : \tau_m$, and $\zeta$ is $\tau_1 \wedge \dots \wedge \tau_m$ (in case $m = 0, \zeta = \omega$). By Linear Substitution (Lemma 17) we get $\mathcal{L}(\Psi_1, \Psi_2) :: \Gamma_1, \vec{x} : \vec{\tau}, \Gamma_2 \vdash_m L\langle N/x \rangle : \sigma$, with $m(\mathcal{L}(\Psi_1, \Psi_2)) = m(\Psi_1) + m(\Psi_2) - 1$. As usual, we should notice that $L\langle N/x \rangle : \sigma$ might not be a simple term but a sum: in that case $\mathcal{L}(\Psi_1, \Psi_2)$ ends in a $\oplus$ rule with premise a derivation $\Phi_1 :: \Gamma_1, \vec{x} : \vec{\tau}, \Gamma_2 \vdash_m \bar{L} : \sigma$ with $\bar{L}$ a simple term in the sum $L\langle N/x \rangle$ and $m(\Phi_1) = m(\mathcal{L}(\Psi_1, \Psi_2))$. Then we define $\Phi$ as in Figure 5(b), with $\Phi_3 = \Psi_3$.

We remark that $m(\Phi) = m(\Phi_1) + m(\Phi_3) = m(\mathcal{L}(\Psi_1, \Psi_2)) + m(\Psi_3) = m(\Psi) - 1$. We conclude that every type of $(\lambda x.L)[N] \cdot P$ is also a type of $(\lambda x.L\langle N/x \rangle)P$ and $m((\lambda x.L)[N] \cdot P) \ge m((\lambda x.L\langle N/x \rangle)P) + 1$.

Conversely, assume $\Phi :: \Gamma \vdash_m (\lambda x.L\langle N/x \rangle)P : \sigma$. We can suppose $\Phi$ as in Figure 5(b), where as above $\vec{x} : \vec{\tau}$ denotes the basis $x : \tau_1, \dots, x : \tau_m$ with $\zeta = \tau_1 \wedge \dots \wedge \tau_m$, and in case $L\langle N/x \rangle$ is a simple term the terminal $\oplus$ rule is omitted. By possibly adding one $\oplus$ rule to $\Phi_1$ one gets $\bar{\Phi}_1 :: \Gamma_1, \Gamma_2, \vec{x} : \vec{\tau} \vdash_m L\langle N/x \rangle : \sigma$. Applying Linear Expansion (Lemma 18) we have $\Psi_1 :: \Gamma_1, \vec{x} : \vec{\tau}, x : \tau \vdash_m L : \sigma$
and $\Psi_2 :: \Gamma_2 \vdash_m N : \tau$ (where we recall $x \notin FV(N)$). Then we set $\Psi$ as in Figure 5(a). This proves that the types of $(\lambda x.L\langle N/x \rangle)P$ are also of $(\lambda x.L)[N]P$.

**Case 3 (bag with exponential resource).** Suppose $M = (\lambda x.L)[N^\dagger] \cdot P \xrightarrow{b} (\lambda x.L\{N+x/x\})P = \mathbb{M}$ and assume $\Psi :: \Gamma \vdash_m (\lambda x.L)[N^\dagger] \cdot P : \sigma$. As in the previous case, Generation (Lemma 16) allows us to suppose

$$ \Psi = \frac{\vdots \Psi_1 \qquad \vdots \Psi^i \qquad \vdots \Psi_3}{\frac{\Gamma_1, x : \tau_1, \dots, x : \tau_n, \vec{x} : \vec{\sigma} \vdash_m L : \sigma \qquad \Gamma_2 \vdash_m N : \tau_i \text{ for } i \le n \qquad \Gamma_3 \vdash_m P : \zeta}{\Gamma_1 \vdash_m \lambda x.L : (\bigwedge_{i=1}^n \tau_i) \wedge \zeta \to \sigma \qquad \Gamma_2, \Gamma_3 \vdash_m [N^\dagger] \cdot P : (\bigwedge_{i=1}^n \tau_i) \wedge \zeta \to \varepsilon}} \cdot P : \sigma $$

where $\Gamma_2 = \Gamma_2^1, \dots, \Gamma_2^n$, and as usual $\vec{x} : \zeta$ denotes the context $x : \sigma_1, \dots, x : \sigma_m$ for $\zeta = \sigma_1 \wedge \dots \wedge \sigma_m$. By Partial Substitution (Lemma 19) we get $\mathcal{P}(\Psi_1, \Psi^{i \le n}) :: \Gamma_1, \vec{x} : \vec{\sigma}, \Gamma_2 \vdash_m L\{N+x/x\} : \sigma$, with $m(\mathcal{P}(\Psi_1, \Psi^{i \le n})) = m(\Psi_1)-n+\sum_{i=1}^n m(\Psi^i)$. Let us suppose $L\{N+x/x\} : \sigma$ is a sum of terms (the case it is a single term being an easier variant): under this hypothesis Generation (Lemma 16) states that $\mathcal{P}(\Psi_1, \Psi^{i \le n})$ ends in a $\oplus$ rule with premise a derivation $\overline{\Psi} :: \Gamma_1, \vec{x} : \vec{\sigma}, \Gamma_2 \vdash_m \overline{L} : \sigma$ with $\overline{L}$ a simple term in the sum $L\{N+x/x\}$ and $m(\overline{\Psi}) = m(\mathcal{P}(\Psi_1, \Psi^{i \le n}))$. Then we define

$$ \Phi := \frac{\frac{\Gamma_1, \vec{x} : \vec{\sigma}, \Gamma_2 \vdash_m \overline{L} : \sigma}{\Gamma_1, \Gamma_2 \vdash_m \lambda x. \overline{L} : \zeta \to \sigma} \qquad \frac{\vdots \Psi_3}{\Gamma_3 \vdash_m P : \zeta} \qquad \vdots \Psi_3}{\frac{\Gamma \vdash_m (\lambda x. \overline{L}) P : \sigma}{\Gamma \vdash_m (\lambda x.L\{N+x/x\}) P : \sigma} \oplus} $$

We remark that $m(\Phi) = m(\overline{\Psi})+m(\Psi_3) = m(\mathcal{P}(\Psi_1, \Psi^{i \le n}))+m(\Psi_3) = m(\Psi)-n$. In particular, notice that whenever $n=0$ the measure is constant.

For the converse we use a similar variant of the above case 2, using Exponential Expansion (Lemma 20) instead of Linear Expansion. We conclude that $(\lambda x.L)[N] \cdot P$ and $(\lambda x.L\langle N/x \rangle)P$ share the same judgements and $m((\lambda x.L)[N^\dagger] \cdot P) \ge m((\lambda x.L\{N+x/x\})P)$.

□

We prove the equivalence among may-solvability, typability in $\vdash_m$ and may-outer normalizability (Theorem 25). As a byproduct we achieve also an operational characterization through the notion of outer reduction (Definition 7). In various $\lambda$-calculi the implication *typable* $\Rightarrow$ *head-normalizable* is often proven using suitable notions of computability or saturated sets (e.g. [Kri93], and our proof of the Theorem 42), whereas the implication *solvable* $\Rightarrow$ *head-normalizable* is argued through a standardization theorem (e.g. [Bar84]). Our proof is instead based on a different method, namely both implications are easy consequences of Lemma 23, which is argued by induction on the measure on the type derivations given in Definition 15. In the $\lambda$-calculus setting, a somewhat similar approach can be found in [Val01]. More generally, the idea of measuring quantitative properties of terms using non-idempotent intersection types can be found also in [dC09], springing out from the analysis of the $\beta$-reduction via the notion of Taylor expansion [ER06, ER08]. As an aside let us point out [dCPTdF08] also, where similar methods have been used to study (outer-)normalizability of linear logic proof-nets.
**Lemma 23.** Let $M$ be a resource term and $C(\cdot)$ be a simple outer-context. If $C(M)$ is typable, then $M$ is reducible to a monf by outer reduction.

*Proof.* By induction on $m(C(M))$, which is a finite number, $C(M)$ being typable. If $M$ is a monf we are done. Otherwise, it has an outer redex, so let $M \xrightarrow{\text{og}} \mathbb{M}$. Since $C(\cdot)$ is a outer-context, every outer redex of $M$ is outer in $C(M)$, hence we have $C(M) \xrightarrow{\text{og}} C(\mathbb{M})$. By Proposition 22 $m(C(M)) > m(C(\mathbb{M}))$. Let $\mathbb{M} = M' + \mathbb{M}''$ be such that $m(C(M')) = m(C(\mathbb{M}))$: the fact that $M'$ exists is due to $C(\cdot)$ being simple, as every term in the sum $C(\mathbb{M})$ is obtained by plugging a term of $\mathbb{M}$ in $C(\cdot)$. By induction hypothesis $M'$ is outer reducible to a monf $\mathbb{L}$. We conclude by context closure: $M \xrightarrow{\text{og}} M' + \mathbb{M}'' \xrightarrow{\text{og}*} \mathbb{L} + \mathbb{M}''$. $\square$

**Lemma 24.** Every may-outer-normal form is typable in $\vdash_m$.

*Proof.* By induction on the structure of a monf $\mathbb{M}$. The only interesting case is when $\mathbb{M}$ is of the form $xP_1 \dots P_p$ with each $P_i$ of the form $[M_{i,1}, \dots, M_{i,m_i}]$. $[N_{i,1}^!, \dots, N_{i,n_i}^!]$ with $m_i, n_i \ge 0$ and for each $j \le m_i, M_{j,m_i}$ onf. By induction hypothesis we have derivations $\Psi_{i,j} :: \Gamma_{i,j} \vdash_m M_{i,j} : \tau_{i,j}$ for each $i \le p, j \le m_i$ hence we can construct a derivation $\Phi_i :: \Gamma_{i,1}, \dots, \Gamma_{i,m_i} \vdash_m P_i : \tau_{i,1} \wedge \dots \wedge \tau_{i,m_i}$ by applying a tree of $m_i$ rules $\ell$ having as premises the $\Psi_{i,1}, \dots, \Psi_{i,m_i}$ respectively and, as the rightmost leaf, a derivation of $\vdash_m [N_{i,1}^!, \dots, N_{i,n_i}^!]$ : $\omega$ made of $n_i$ rules $!_0$ and one rule 1. Similarly we get a derivation typing $xP_1 \dots P_p$ by applying a tree of $p$ rules $\to_E$ having as premises the $\Phi_i$'s derivations and, as the leftmost leaf, a var rule typing $x$ with $(\bigwedge_{j \le m_1} \tau_{1,j}) \wedge \dots \wedge (\bigwedge_{j \le m_p} \tau_{p,j}) \to \sigma$, for a linear type $\sigma$. $\square$

**Theorem 25.** Given a resource term $M \in \Lambda^r$, the following are equivalent:

1. *M is may-outer normalizable*,

2. *M is typable by $\vdash_m$*,

3. *M is reducible to a monf by outer reduction*,

4. *M is may-solvable*.

Moreover, if $M \in \Lambda^\| \text{ then } 4$ can be replaced by

4'. *M is may-solvable in $\Lambda^\|$.*

*Proof.* $1 \Rightarrow 2$: by Proposition 22 and Lemma 24. $2 \Rightarrow 3$: by Lemma 23, merely taking the hole as the simple head-context. $3 \Rightarrow 4$ (resp. $3 \Rightarrow 4'$): by Theorem 13 and context closure. $4 \Rightarrow 1$: if there is a simple head-context $C(\cdot)$ s.t. $C(M)$ has a monf, by the already proven implication $1 \Rightarrow 2$, $C(M)$ is typable, we conclude by Lemma 23. $\square$

The implication $1 \Rightarrow 3$ can also be argued as a corollary of the standardization proven in [PT09]. However, our proof uses the type assignment system, namely Lemma 23, so it adopts a different approach with respect to the techniques in [PT09].

We can now trust in the examples 1-4 of Section 3. In fact $\Omega$, having no monf, is may (hence must) unsolvable.
# 5 The problem of Must Solvability

The characterization of the must solvability in $\Lambda^r$ is a tough problem. In $\Lambda^r$ we have the empty sum (i.e. 0) and diverging terms (like $\Omega$). They are both considered unsolvable since they do not communicate with the environment, but they have a crucial difference: 0 is the neutral element of the sum, hence it disappears when added to a solvable term, $\Omega$ does not. This difference is harmless when considering may-solvability but becomes relevant for the must-solvability. Consider the terms:

$$M_1 = \lambda x. \mathbf{I}[\Omega^1, x^1] \xrightarrow{g} \lambda x. \Omega + \lambda x. x$$

$$M_2 = \lambda x. \mathbf{I}[(\Omega[x])^1, x^1] \xrightarrow{g} \lambda x. \Omega[x] + \lambda x. x$$

We claim that $M_1$ is must-solvable whilst $M_2$ is not. In fact, both $\lambda x. \Omega$ and $\lambda x. \Omega[x]$ have no monf, so they are not may solvable (Theorem 25). Hence the only possibility for having a sum of identities from $M_1$ (resp. $M_2$) is to find a context reducing $\lambda x. \Omega$ (resp. $\lambda x. \Omega[x]$) to 0 and keeping $\lambda x. x$ different from 0. Such a context exists for $M_1$, e.g. $(\cdot)[\mathbf{I}]$, but not for $M_2$, both $\lambda x. \Omega[x]$ and $\lambda x. x$ using $x$ linearly.

This example shows: first, that the implication *must-solvable* $\Rightarrow$ *must-outer normalizable*, i.e. the converse of Theorem 13 for the must case, does not hold in $\Lambda^r$, $M_1$ being a contra-example; second, that in order to characterize whether a sum is must-solvable, one should know if there are contexts reducing the diverging terms of a sum to 0 and keeping at least one among the others different from 0. With respect to this point the situation can be even worse, consider:

$$M_3 = \lambda x. \mathbf{I}[(\Omega[x])^1, y^1] \xrightarrow{g} \lambda x. \Omega[x] + \lambda x. y$$

The term $M_3$ is must-solvable via the context $\lambda y.(\cdot)1$. This means that the term $\lambda x. \Omega[x]$, occurring in the sums that are reduct of both $M_2$ and $M_3$, has a different behaviour depending on the shape of the other terms of the sum. In particular, the property of being must-solvable does not commute with the sum.

Such kinds of problems are too difficult for us at the present, so we study the must-solvability in the simpler setting of $\Lambda^\parallel$, the purely non-deterministic fragment of $\Lambda^r$. In this fragment we have only non-empty bags of reusable resources and non-empty sums, so no term reduces to 0, and the problem of must-solvability becomes smoother than in $\Lambda^r$.

## 5.1 Characterization of Must Solvability in $\Lambda^\parallel$

From now on we consider $\Lambda^\parallel$, the purely non-deterministic fragment of $\Lambda^r$ that has been defined at the end of Section 2.

A type assignment system characterizing logically the must-solvability must assign types to all the elements of a sum, so to type the sum itself (by definition of must-solvability), and, in order to type an application $(\lambda x.M)P$ the types of all elements of $P$ need to match the types of all the free occurrences of $x$ in $M$. Namely, the type assignment needs to have a correct behaviour with respect to the $\lambda$-calculus, which is a proper fragment of $\Lambda^\parallel$, i.e., a term of $\Lambda$ needs to be typed in it if and only if it has head-normal form, in the standard sense.

Therefore, we use a well-known $\lambda$-model, namely the $D_\infty$ of Scott [Sco76], described in logical form in [PRDR04]. In fact, the underlined structure is a
$$ \pi \preceq \omega \qquad \pi \preceq \pi \wedge \pi \qquad \pi_1 \wedge \pi_2 \preceq \pi_i \quad (i = 1, 2) \qquad \omega \to \phi \preceq \phi \preceq \omega \to \phi $$

$$ \omega \preceq \omega \to \omega \qquad \pi \to \omega \preceq \omega \to \omega \qquad (\pi \to \rho) \wedge (\pi \to \zeta) \preceq \pi \to (\rho \wedge \zeta) $$

$$ \frac{\pi \preceq \pi' \quad \rho \preceq \rho'}{\pi \wedge \rho \preceq \pi' \wedge \rho'} \qquad \frac{\pi' \preceq \pi \quad \rho \preceq \rho'}{\pi \to \rho \preceq \pi' \to \rho'} $$

(a) rules defining the preorder $\preceq$ over types

$$ \overline{\Gamma, x : \pi \vdash_M x : \pi}^{\text{var}} \qquad \overline{\Gamma \vdash_M M : \omega}^{\omega} \qquad \frac{\Gamma \vdash_M M : \pi \quad \Gamma \vdash_M \mathbb{N} : \pi}{\Gamma \vdash_M M + \mathbb{N} : \pi}^{\text{mix}+} $$

$$ \frac{\Gamma, x : \pi \vdash_M M : \rho}{\Gamma \vdash_M \lambda x.M : \pi \to \rho} \to_I \frac{\Gamma \vdash_M M : \pi \to \tau \quad \Gamma \vdash_M P : \pi}{\Gamma \vdash_M MP : \tau} \to_E $$

$$ \frac{\Gamma \vdash_M M : \pi}{\Gamma \vdash_M [M^!]' : \pi}! \qquad \frac{\Gamma \vdash_M M : \pi \quad \Gamma \vdash_M P : \pi}{\Gamma \vdash_M [M^!]' \cdot P : \pi}^{\text{mix}} $$

$$ \frac{\Gamma \vdash_M M : \pi \quad \Gamma \vdash_M M : \rho}{\Gamma \vdash_M M : \pi \wedge \rho} \wedge_I \frac{\Gamma \vdash_M M : \rho \quad \rho \preceq \pi}{\Gamma \vdash_M M : \pi} \preceq $$

(b) deductive rules of $\vdash_M$

<caption>**Figure 6:** The type assignment system $\vdash_M$.</caption>

complete lattice with infinite descending chains, so every pair of compact points has a least upper bound (lub) greater than $\perp$ and a greatest lower bound (glb) less than $\top$. From a logical point of view, since types are names for compact elements, this means that every two typable terms have a non-trivial type in common. Since $D_\infty$ is a sensible model, giving non-trivial interpretation to all and only the solvable terms, this implies that every pair of solvable terms have at least one type in common.

The type assignment system $\vdash_M$ characterizing must-solvability is exactly the logical description of $D_\infty$, plus two new rules for typing bags and sums. Note that, thanks to the previously described property, these rules are very easy, since they ask that all the elements of a bag or a sum have the same type.

**Definition 26.** The set of types for $\vdash_M$ is given by the following grammar:

$$ \pi, \rho, \zeta ::= \phi \mid \omega \mid \pi \to \rho \mid \pi \wedge \rho $$

where $\phi$ and $\omega$ are two different constants. We consider the smallest pre-order relation $\preceq$ over types satisfying the rules in Figure 6(a). The relation $\approx$ is the equivalence generated by $\preceq$. The symbol $=$ denote the identity relation on types.

A basis is a function from variables to types, with finite domain. A typing judgement is a sequent $\Gamma \vdash_M \mathbb{A} : \pi$, where $\Gamma$ is a basis. The rules of the type assignment system $\vdash_M$ are defined in Figure 6(b).

We extend to $\vdash_M$ the notations used in the previous section for $\vdash_m$.
The system $\vdash_M$ is very different from $\vdash_m$. Essentially, $\vdash_m$ has a quantitative aspect missing in $\vdash_M$. This is reflected in the fact that the intersection is idempotent in the latter and not in the former. Indeed, in $\vdash_m$ the non-idempotency of the intersection is crucial to account for the consumption of linear resources, while in $\vdash_M$ we do not need to count the number of resources in a bag since $\Lambda^{\|}$ allows only reusable resources. Moreover, in order to type a sum, all elements of the sum need to be typed by the same type. The constant type $\omega$ represents the empty bag in $\vdash_m$, while in $\vdash_M$ it is a trivial type, which can be assigned to all terms. Indeed, the empty bag does not belong to $\Lambda^{\|}$. Another difference is that in $\vdash_M$ we allow intersection in the right side of an arrow, but this is made for making the type matching exactly the compact elements of $D_{\infty}$. Since $\pi_1 \wedge \pi_2 \preceq \pi_i$, the rule $\preceq$ entails the $\wedge$-elimination rule, which we have therefore omitted in the definition of $\vdash_M$:

$$ \frac{\Gamma \vdash_M M : \pi_1 \wedge \pi_2}{\Gamma \vdash_M M : \pi_i} \wedge E $$

Also the following rules are admissible:

$$ \frac{\Gamma \vdash_M M : \rho \quad x \notin d(\Gamma)}{\Gamma, x : \pi \vdash_M M : \rho} \quad \text{weak} $$

$$ \frac{\Gamma, x : \zeta \vdash_M M : \rho \quad \pi \preceq \zeta}{\Gamma, x : \pi \vdash_M M : \rho} \preceq_L $$

The following lemma states well-known properties of $\approx$ that we will use in the sequel. We refer to [RDRP04] (chapter 11.1.1, p. 132) for its proof.

**Lemma 27 (Properties of $\preceq$, [RDRP04]).** The constants $\omega$ and $\phi$ belong to the $\approx$-classes that are, respectively, the $\preceq$-maximum and the $\preceq$-minimum. Indeed such classes can be characterized as follows:

$$ \begin{array}{l} \phi \not\approx \omega \\ \pi \wedge \rho \approx \omega \quad \text{iff} \quad \pi \approx \omega \text{ and } \rho \approx \omega, \\ \pi \rightarrow \rho \approx \omega \quad \text{iff} \quad \rho \approx \omega, \end{array} \quad \begin{array}{l} \pi \wedge \rho \approx \phi \quad \text{iff} \quad \pi \approx \phi \text{ or } \rho \approx \phi, \\ \pi \rightarrow \rho \approx \phi \quad \text{iff} \quad \pi \approx \omega \text{ and } \rho \approx \phi. \end{array} $$

For every type $\pi$ there is a minimum $n \in \text{Nat}$, and types $\pi_1^1, \dots, \pi_1^n, \pi_2^1, \dots, \pi_2^n$ such that $\pi \approx \bigwedge_{i \le n} \pi_1^i \rightarrow \pi_2^i$. Moreover, we have

$$ \rho_2^j \not\approx \omega \text{ implies } \exists J \subseteq \{1, \dots, n\}, \bigwedge_{i \in J} \pi_1^i \preceq \rho_1^j, \bigwedge_{i \in J} \pi_2^i \preceq \rho_2^j \quad (1 \le j \le m) \quad (8) $$

Definition 28 extends to our setting the aggregation operation $\odot$ of [BEM09]. That operation has been introduced to interpret a parallel constructor corresponding to the $+$ of $\Lambda^{\|}$. Indeed, our setting allows to prove that the $\odot$ of [BEM09] is the sup of the preorder $\preceq$ (Proposition 29).

**Definition 28.** We define the following operation over types by induction on their lengths:

$$ \begin{array}{l@{\qquad}l} \phi \odot \pi &:= \pi & (\pi_1 \rightarrow \pi_2) \odot (\rho_1 \rightarrow \rho_2) := (\pi_1 \wedge \rho_2) \rightarrow (\pi_2 \odot \rho_2) \\ \omega \odot \pi &:= \omega & (\pi_1 \wedge \pi_2) \odot \rho := (\pi_1 \odot \rho) \wedge (\pi_2 \odot \rho) \\ (\pi_1 \rightarrow \pi_2) \odot \rho &:= \rho \odot (\pi_1 \rightarrow \pi_2) & \text{if } \rho \text{ is not an arrow} \end{array} $$
Notice that $\odot$ is associative and commutative modulo the associativity and commutativity of $\wedge$, in fact, (assuming $\pi_i, \rho_i$ arrows)

$$ (\pi_1 \wedge \pi_2) \odot (\rho_1 \wedge \rho_2) = ((\rho_1 \odot \pi_1) \wedge (\rho_2 \odot \pi_1)) \wedge ((\rho_1 \odot \pi_2) \wedge (\rho_2 \odot \pi_2)) \\ \approx ((\pi_1 \odot \rho_1) \wedge (\pi_2 \odot \rho_2)) \wedge ((\pi_1 \odot \rho_2) \wedge (\pi_2 \odot \rho_2)) = (\rho_1 \wedge \rho_2) \odot (\pi_1 \wedge \pi_2) $$

Besides, $\odot$ is compatible with $\approx$, i.e. $\pi \approx \pi'$ and $\rho \approx \rho'$ entails $\pi \odot \rho \approx \pi' \odot \rho'$.

**Proposition 29.** For any two types $\pi, \rho$, we have:

$$ \pi \wedge \rho \approx \inf(\pi, \rho) $$

$$ \pi \odot \rho \approx \sup(\pi, \rho) $$

Also, if $\pi, \rho$ are not $\approx$-equivalent to $\omega$ (resp. $\phi$) then so is $\pi \odot \rho$ (resp. $\pi \wedge \rho$).

*Proof.* By the characterization of the $\approx$-class of $\omega$ (resp. $\phi$) given in Proposition 27 one can easily deduce that $\pi, \rho \not\approx \omega$ (resp. $\not\approx \phi$) entails $\pi \odot \rho \not\approx \omega$ (resp. $\pi \wedge \rho \not\approx \phi$).

That intersection is the inf is an immediate consequence of the rules of Figure 6(a). As for $\odot$ we proceed by structural induction on $\pi$ and $\rho$.

The cases where one between $\pi, \rho$ is equal to $\phi$ or $\omega$ are immediate consequences of the fact that the two constants are respectively the minimum and the maximum of $\leq$ (Proposition 27).

If $\pi = \bigwedge_{i \leq n} (\pi_i^1 \to \pi_i^2)$ for an $n > 0$, then we have $\pi \odot \rho \approx \bigwedge_{i \leq n} ((\pi_i^1 \to \pi_i^2) \odot \rho)$. Hence by induction hypothesis $\pi \odot \rho \succeq \pi, \rho$. Let now $\zeta \succeq \pi, \rho$, we claim $\zeta \succeq \pi \odot \rho$. By Proposition 27, there is a minimum $m$ such that $\zeta \approx \bigwedge_{i \leq m} (\zeta_j^1 \to \zeta_j^2)$. Note that the minimality condition implies either $\zeta \approx \omega$ or $\zeta_j^2 \not\approx \omega$, for all $j \leq m$. Since $\pi \leq \zeta$, for every $j \leq m$, there is $J \subseteq \{1, \dots, n\}$ s.t. $\bigwedge_{i \in J} (\pi_i^1 \to \pi_i^2) \leq \zeta_j^1 \to \zeta_j^2$. Since also $\rho \leq \zeta$, we have:

$$ \bigwedge_{i \leq n} (\sup(\pi_i^1 \to \pi_i^2, \rho)) \leq \bigwedge_{i \in J} (\sup(\pi_i^1 \to \pi_i^2, \rho)) \leq \sup \bigwedge_{i \in J} (\pi_i^1 \to \pi_i^2, \rho) \leq \zeta_j^1 \to \zeta_j^2 $$

The above inequality holds for every $j \leq m$, hence $\pi \odot \rho \leq \zeta$.

If $\pi = \pi^1 \to \pi^2$, then the definition of $\pi \odot \rho$ depends on $\rho$. The cases $\rho = \phi, \omega$ have been already considered and $\rho = \rho^1 \wedge \rho^2$ turns to the previous one. So, let $\rho = \rho^1 \to \rho^2$ and $\pi \odot \rho = (\pi^1 \wedge \rho^1) \to (\pi^2 \odot \rho^2)$. By induction hypothesis this gives, $\pi \odot \rho = \inf(\pi^1, \rho^1) \to \sup(\pi^2, \rho^2)$, which immediately implies $\pi, \rho \leq \pi \odot \rho$. The proof that for every $\zeta \succeq \pi, \rho$, we have $\zeta \succeq \pi \odot \rho$ is an easy variant of the case $\pi$ is a proper intersection. $\square$

The next lemma is an easy variant in the setting of $\Lambda^{\parallel}$ of the Generation Lemma in [RDRP04] (Lemma 10.1.7).

**Lemma 30 (Generation).** 1. $\Gamma \vdash_M x : \pi$ implies $\Gamma(x) \leq \pi$.

2. $\Gamma \vdash_M \lambda x.M : \pi$ implies either $\pi \approx \omega$ or there are $\pi_1, \dots, \pi_n$ such that $\pi_1 \wedge \dots \wedge \pi_n \leq \pi$, $\pi_i = \zeta_i \to \rho_i$ and $\Gamma, x : \zeta_i \vdash_M M : \rho_i$ for every $i \in \{1, \dots, n\}, n > 1$.

3. $\Gamma \vdash_M \lambda x.M : \pi \to \rho$ implies $\Gamma, x : \pi \vdash_M M : \rho$.
4. $\Gamma \vdash_M MP : \pi$ implies there are $\pi_1, \dots, \pi_n$, for $n \ge 1$, s.t. $\pi_1 \wedge \dots \wedge \pi_n \preceq \pi$ and for all $1 \le i \le n$, $\Gamma \vdash_M M : \rho_i \rightarrow \pi_i$ and $\Gamma \vdash_M P : \rho_i$.

5. $\Gamma \vdash_M [M^!].P : \pi$ implies $\Gamma \vdash_M M : \pi$ and, if $P$ is non-empty, also $\Gamma \vdash_M P : \pi$.

6. $\Gamma \vdash_M \mathbb{M} : \pi$ implies that, for every term $M$ of the sum $\mathbb{M}$, $\Gamma \vdash_M M : \pi$.

7. $\Gamma, x : \pi \vdash_M A : \rho$ and $x \notin \mathrm{FV}(A)$ imply $\Gamma \vdash_M A : \rho$.

In what follows we prove that the set of types assigned by $\vdash_M$ is invariant under middle (hence giant) reduction (Proposition 34).

**Lemma 31 (Substitution).** If $\Gamma, x : \pi \vdash_M A : \rho$ and $\Gamma \vdash_M N : \pi$, then there are $\Gamma, x : \pi \vdash_M A \{(N+x)/x\} : \rho$ and $\Gamma \vdash_M A \{N/x\} : \rho$.

*Proof.* By structural induction on $\mathbb{A}$. If $\mathbb{A} = x$, Lemma 30.1 states $\pi \preceq \rho$. Then a derivation of $\Gamma, x : \pi \vdash_M A \{(N+x)/x\} : \rho$ can be obtained by applying rule $\preceq$ to the derivation of $\Gamma \vdash_M N : \pi$. Moreover, we can build the derivation:

$$ \frac{\frac{\Gamma, x : \pi \vdash_M x : \pi \qquad \frac{\Gamma \vdash_M N : \pi}{\Gamma, x : \pi \vdash_M N : \pi} \text{ weak}}{\Gamma, x : \pi \vdash_M x : \rho \preceq \Gamma, x : \pi \vdash_M N : \rho \preceq \Gamma, x : \pi \vdash_M N : \rho \preceq \Gamma, x : \pi \vdash_M N + x : \rho \preceq \Gamma, x : \pi \vdash_M N + x : \rho}}{\Gamma, x : \pi \vdash_M N + x : \rho} $$

If $\mathbb{A} = [M^!] \cdot P$, we consider $P$ non-empty, and we build only $\Gamma, x : \pi \vdash_M [M^!]$. $P \{(N+x)/x\} : \rho$: the case $P$ empty and the definition of $\Gamma \vdash_M A \{N/x\} : \rho$ are easy variants. So, let $\mathbb{A} \{N+x/x\} = [M_1^!, \dots, M_k^!]. P \{N+x/x\}$, where $M \{N+x/x\} = \sum_{i=0}^k M_i$ and $P \{N+x/x\}$ is always a simple bag, $P$ not containing linear resources. By Lemma 30.5, we have two derivations of $\Gamma, x : \pi \vdash_M [M^!] : \rho$ and $\Gamma, x : \pi \vdash_M P : \rho$. The induction hypothesis yields $\Gamma, x : \pi \vdash_M [M_1^!, \dots, M_k^!], \rho$ and $\Gamma, x : \pi \vdash_M P \{N+x/x\} : \rho$. By Lemma 30, $\Gamma \vdash_M M_i : \rho$, and the result follows by applying $n$ times the rule *mix*.

The other cases are straightforward or easy variants of the previous one. $\square$

Similarly to above, the following lemmas are proven by easy structural in-
ductions on $\mathbb{A}$.

**Lemma 32 (Partial expansion).** Let $\Gamma, x : \pi \vdash_M \mathbb{A} \{N+x/x\} : \rho$, then there are a type $\zeta \succeq \pi$ such that $\Gamma, x : \zeta \vdash_M \mathbb{A} : \rho$ and $\Gamma \vdash_M N : \zeta$.

**Lemma 33 (Total expansion).** Let $x \notin d(\Gamma)$, if $\Gamma \vdash_M \mathbb{A} \{N/x\} : \rho$ then there is a type $\pi$ such that $\Gamma, x : \pi \vdash_M \mathbb{A} : \rho$ and $\Gamma \vdash_M N : \pi$.

**Proposition 34 (Invariance of $\vdash_M$ typings).** Let $\epsilon \in \{\mathfrak{m}, \mathfrak{g}\}$ and $M \stackrel{\epsilon}{\to} \mathbb{M}$, then $M$ and $\mathbb{M}$ share the same judgements, i.e. $\Gamma \vdash_M M : \pi$ iff $\Gamma \vdash_M \mathbb{M} : \pi$.

*Proof.* The proof is by induction on the context enclosing the redex reduced in $M \stackrel{\epsilon}{\to} \mathbb{M}$. The induction steps are immediate, while the base of induction is when $M$ is the redex fired by the reduction $M \stackrel{\epsilon}{\to} \mathbb{M}$. One can consider only the middle-step cases, the giant one will follow since it corresponds to a sequence of middle-steps.

Suppose $M = (\lambda x.L)[N^!].P$, we suppose also $P$ non-empty, the case $P$ is empty being simpler (using Lemma 33 instead of Lemma 32). So, let $M \stackrel{\epsilon}{\to} (\lambda x.L \{N+x/x\})P = \mathbb{M}$ and assume $\Gamma \vdash_M (\lambda x.L)[N^!].P : \pi$. Generation (Lemma 30) allows us to say that $\pi \approx \pi_1 \wedge \dots \wedge \pi_n$, and, for all $i$, there is $\rho_i$ such
that $\Gamma, x : \rho_i \vdash_M L : \pi_i$ and $\Gamma \vdash_M N : \rho_i$, and $\Gamma \vdash_M P : \rho_i$. By Lemma 31 and the first two judgements, we get a derivation $\Phi_i :: \Gamma, x : \rho_i \vdash_M L \{N+x/x\} : \pi_i$. For each $i \le n$, we get a derivation of $\Psi_i :: \Gamma \vdash_M (\lambda x.L \{N+x/x\})P : \pi_i$ by applying to $\Phi_i$ one $\to_I$ rule and one $\to_E$ rule with right premise $\Gamma \vdash_M P : \rho_i$. Then, gathering all $\Psi_i$'s with $n-1$ rules $\wedge I$ and applying one $\preceq$ yields a derivation with conclusion $\Gamma \vdash_M (\lambda x.L \{N+x/x\})P : \pi$.

For the converse, let $\Gamma \vdash_M (\lambda x.L \{N+x/x\})P = \mathbb{M} : \pi$. Having all bags just reusable resources, the variable $x$ can have at most one linear occurrence in $L$ (and an arbitrary number of reusable ones). $\mathbb{M}$ is either a simple term or a sum having two terms. Let us consider the last case, the former being an easier variant. So, we have $L \{N+x/x\} = L^1 + L^2$ and $\mathbb{M} = (\lambda x.L^1)P + (\lambda x.L^2)P$. By applying Generation, we get, for $i = 1, 2$, $\Gamma \vdash_M (\lambda x.L^i)P : \pi$ and then $\pi_1^i \wedge \dots \wedge \pi_{n_i}^i \preceq \pi$ and $\rho_1^i, \dots, \rho_{n_i}^i$ such that for every $j \le n_i$, $\Gamma \vdash_M \lambda x.L^i : \rho_j^i \to \pi_j^i$ and $\Gamma \vdash_M P : \rho_j^i$. Notice that for every $i, j$, $\bigwedge_{i,j} \rho_j^i \preceq \rho_j^i$, so $\rho_j^i \to \pi_j^i \preceq (\bigwedge_{i,j} \rho_j^i) \to \pi_j^i$, and so by a $\preceq$-rule we have $\Gamma \vdash_M \lambda x.L^i : (\bigwedge_{i,j} \rho_j^i) \to \pi_j^i$. Thus, a number of $\wedge I$-rules gives us $\Gamma \vdash_M \lambda x.L^i : \bigwedge_{i,j} ((\bigwedge_{i,j} \rho_j^i) \to \pi_j^i)$ and, since $\bigwedge_{i,j} ((\bigwedge_{i,j} \rho_j^i) \to \pi_j^i) \preceq (\bigwedge_{i,j} \rho_j^i) \to (\bigwedge_{i,j} \pi_j^i) \preceq (\bigwedge_{i,j} \rho_j^i) \to \pi$, we have $\Gamma \vdash_M \lambda x.L^i : (\bigwedge_{i,j} \rho_j^i) \to \pi$. By Generation (Lemma 30), $\Gamma, x : \bigwedge_{i,j} \rho_j^i \vdash_M L^i : \pi$ and by a mix+-rule $\Gamma, x : \bigwedge_{i,j} \rho_j^i \vdash_M L \{N+x/x\} : \pi$. We can now apply Lemma 32, getting a type $\zeta \succeq \bigwedge_{i,j} \rho_j^i$ and derivations $\Phi :: \Gamma, x : \zeta \vdash_M L : \pi$ and $\Psi :: \Gamma \vdash_M N : \zeta$. Since $\Gamma \vdash_M P : \bigwedge_{i,j} \rho_j^i$, by one $\preceq$-rule we have $\Gamma \vdash_M P : \zeta$, hence, by a mix+-rule $\Gamma \vdash_M P \cdot [N!] : \zeta$. We conclude by one rule $\to_I n$ and one $\to_E$. $\square$

**Lemma 35.** Every must-outer-normal form of $\Lambda^\|$ is typable in $\vdash_M$ with a non-trivial type, i.e. a type $\not\approx \omega$.

*Proof.* We do induction on the number $n \ge 1$ of terms in a Monf $\mathbb{M}$. Let $n=1$, then $\mathbb{M}$ has the following shape: $M = \lambda x_1 \dots x_s \cdot y P_1 \dots P_p$. Let $y = x_j$ (the case $y$ is free being an easy variant), for some $j \le s$. Let $\Gamma(x_k) = \omega$, for every $k \ne j$ and let $\Gamma(x_j) = \underbrace{\omega \to \dots \to \omega}_{p \text{ times}} \to \phi$. Recall that, for all $i \le p$, $\Gamma \vdash_M P_i : \omega$, hence

by $p-1$ rules $\to_E$ we obtain a derivation of $\Gamma \vdash_M x_j P_1 \dots P_p : \phi$, and then by $s$ rules $\to_I$ we get $\vdash_M \lambda x_1 \dots x_s \cdot x_j P_1 \dots P_p : \pi$, where

$$ \pi = \underbrace{\omega \to \dots \to \omega}_{j-1} \to (\underbrace{\omega \to \dots \to \omega}_{p} \to \phi) \to \underbrace{\omega \to \dots \to \omega}_{s-j} \to \phi, $$

which is a type $\not\approx \omega$ by Lemma 27.

As for the induction case, let $\mathbb{M} = \mathbb{M}' + \mathbb{M}''$, with both $\mathbb{M}', \mathbb{M}''$ different from 0. By the definition of Monf, both $\mathbb{M}', \mathbb{M}''$ are Monf and hence by the induction hypothesis $\Gamma' \vdash_M \mathbb{M}' : \sigma'$ and $\Gamma'' \vdash_M \mathbb{M}'' : \sigma''$, with $\sigma', \sigma'' \not\approx \omega$.

Define the following context having domain equal to $d(\Gamma') \cup d(\Gamma'')$:

$$ \Gamma(x) = \begin{cases} \pi & \text{if } x \notin d(\Gamma') \cap d(\Gamma'') \text{ and } \Gamma'(x) \text{ or } \Gamma''(x) \text{ is } \pi, \\ \pi' \wedge \pi' & \text{if } \Gamma'(x) = \pi' \text{ and } \Gamma''(x) = \pi'' \end{cases} $$

Since the rules weak and $\preceq$ are admissible, we get $\Gamma \vdash_M \mathbb{M}' : \sigma'$ and $\Gamma \vdash_M \mathbb{M}'' : \sigma''$. Then, since $\sigma' \odot \sigma'' \succeq \sigma'$, $\sigma''$ (Proposition 29), we have $\Gamma \vdash_M \mathbb{M}' : \sigma' \odot \sigma''$ and $\Gamma \vdash_M \mathbb{M}'' : \sigma' \odot \sigma''$, and so $\Gamma \vdash_M \mathbb{M} : \sigma' \odot \sigma''$ by one mix+-rule. We have $\sigma' \odot \sigma'' \not\approx \omega$ still by Proposition 29. $\square$
In order to prove that having a non-trivial type in the system $\vdash_M$ implies to be must-outer normalizable by means of an outer reduction sequence, we will use a computability argument. The proof is an adaptation of the proof of approximation in the model $D_\infty$, given in [PRDR04], and it is given in the next subsection.

**Theorem 36.** Given a term $M \in \Lambda^{\|\|}$, the following are equivalent:

1. M is must-outer normalizable,

2. M is non-trivially typable by $\vdash_M$,

3. M is reducible to a Monf by outer $\epsilon$ reduction, $\epsilon \in \{\mathfrak{m}, \mathfrak{g}\}$,

4. M is must-solvable in $\Lambda^{\|\|}$.

*Proof.* 1 $\Rightarrow$ 2: by Lemma 35 and Proposition 34. 2 $\Rightarrow$ 3: by Theorem 42. 3 $\Rightarrow$ 4: by Theorem 13. 4 $\Rightarrow$ 1: if M is must-solvable then there is a outer-context $C(\cdot)$ such that $C(M) \xrightarrow{g^*} n\mathbf{I}$. Since the latter is a Monf, we have for the already proven 1 $\Rightarrow$ 2 that $C(M)$ is typable with a type $\rho \not\approx \omega$. Since $C(\cdot)$ is a outer-context, then M is typable with a type $\pi \not\approx \omega$ (this can be easily deduced by inspecting the rules of Figure 6(b) and the characterization of the $\omega$ $\approx$-class in Lemma 27). Then, by Theorem 42 M has a Monf. $\square$

## 5.2 Non-trivial typability entails the finiteness of $\mathcal{O}$.

We adapt to our setting a variant of the saturated sets technique due to [Kri93]. In this section, outer reduction is short for both middle and giant outer reduction, and $\mathcal{O}$ denotes $\mathcal{O}^\epsilon$, with $\epsilon \in \{\mathfrak{m}, \mathfrak{g}\}$.

**Definition 37.** We interpret types as sets of resource terms as follows:

$$[[\phi]] := \{M \mid M \overset{\mathcal{O}^*}{\to} \sum_i x_i P_{i,1} \dots P_{i,p_i} \mid i \le n > 0, p_i \ge 0, P_{i,j} \in \Lambda^{b^j}\};$$

$$[[\omega]] := \text{Nat}^+\langle\Lambda^{\|\|}\rangle; \quad [[\pi \to \rho]] := \{M \mid \forall N \in [[\pi]], M[N^1] \in [[\rho]]\}; \quad [[\pi \wedge \rho]] := [[\pi]] \cap [[\rho]].$$

The following three lemmas show that this interpretation respects the pre-order on types, assures the outer normalization for non-trivial types and is closed under outer expansion.

**Lemma 38 (Preorder).** For any types $\pi$ and $\rho$, $\pi \le \rho$ entails $[[\pi]] \subseteq [[\rho]]$. In particular, $[[\phi]] \subseteq [[\pi]]$ and for any variable $x$, $x \in [[\pi]]$.

*Proof.* By induction on $\pi$, considering all cases defining $\leq$ (Figure 6(a)). Then, Lemma 27 allows to deduce $[[\phi]] \subseteq [[\pi]]$ and $x \in [[\pi]]$, since $x \in [[\phi]]$ by definition.

The only delicate case is $\phi \leq \omega \to \phi$. Let $M \in [[\phi]]$, i.e. $M \overset{\mathcal{O}^*}{\to} \sum_i x^i P_1^i \dots P_{n_i}^i$. We prove that for any $N \in \text{Nat}^+\langle\Lambda^{\|\|}\rangle$, $M[N^1] \in [[\phi]]$. Indeed, any term of a sum that is an outer reduct of $M$ cannot be a $\lambda$ abstraction, since otherwise $M \overset{\mathcal{O}^*}{\to} \sum_i x^i P_1^i \dots P_{n_i}^i$. Hence, $M[N^1] \overset{\mathcal{O}^*}{\to} \sum_i x^i P_1^i \dots P_{n_i}^i$, i.e. $M[N^1] \in [[\phi]]$. $\square$

**Lemma 39 (Outer normalization).** For every type $\pi \not\approx \omega$, for every $M \in [[\pi]]$, M is reducible to a must-outer-normal form by the outer reduction.
*Proof.* By induction on $\pi$. The case $\pi = \phi$ is by definition of $\llbracket \phi \rrbracket$. If $\pi = \pi_1 \wedge \pi_2$ then by Lemma 27 there is $\pi_i \not\approx \omega$. By induction hypothesis the terms in $\llbracket \pi_i \rrbracket$ are outer normalizable and we conclude by $\llbracket \pi \rrbracket \subseteq \llbracket \pi_i \rrbracket$. If $\pi = \pi_1 \to \pi_2$, then let $\mathbb{M} \in \llbracket \pi_1 \to \pi_2 \rrbracket$. By Lemma 38 any variable $x \in \llbracket \pi_1 \rrbracket$, so $\mathbb{M}[x'] \in \llbracket \pi_2 \rrbracket$. By Lemma 27, $\pi_2 \not\approx \omega$, so by induction $\mathbb{M}[x']$ is outer normalizable. We conclude by the simple remark that if $\mathbb{M}[x']$ is outer normalizable then so is $\mathbb{M}$. $\square$

**Lemma 40 (Saturation).** For every type $\pi$, if $\mathbb{M}\{\mathbb{N}/x\} P_1 \dots P_n \in \llbracket \pi \rrbracket$, we have $(\lambda x.\mathbb{M})[\mathbb{N}^1]P_1 \dots P_n \in \llbracket \pi \rrbracket$.

*Proof.* By induction on $\pi$. The case $\pi = \omega, \phi$ are straightforward. If $\pi = \pi_1 \to \pi_2$, suppose $\mathbb{M}\{\mathbb{N}/x\} P_1 \dots P_n \in \llbracket \pi_1 \to \pi_2 \rrbracket$, and let $\mathbb{L} \in \llbracket \pi_1 \rrbracket$. We have $\mathbb{M}\{\mathbb{N}/x\} P_1 \dots P_n[\mathbb{L}^1] \in \llbracket \pi_2 \rrbracket$ and, by induction on $\pi_2$, $(\lambda x.\mathbb{M})[\mathbb{N}^1]P_1 \dots P_n[\mathbb{L}^1] \in \llbracket \pi_2 \rrbracket$. We conclude $(\lambda x.\mathbb{M})[\mathbb{N}^1]P_1 \dots P_n \in \llbracket \pi_1 \to \pi_2 \rrbracket$. The case $\pi = \pi_1 \wedge \pi_2$ is an immediate consequence of the induction hypothesis applied $\pi_1$ and $\pi_2$. $\square$

The adequacy lemma relates the interpretation on types with the derivations.

**Lemma 41 (Adequacy).** Let $x_1 : \pi_1, \dots, x_n : \pi_n \vdash_M \mathbb{M} : \rho$ and for every $i \le n$, $N_i \in \llbracket \pi_i \rrbracket$, we have $\mathbb{M}\{N_1/x_1\} \dots \{N_n/x_n\} \in \llbracket \rho \rrbracket$.

*Proof.* By structural induction on a derivation $\Phi$ of $x_1 : \pi_1, \dots, x_n : \pi_n \vdash_M \mathbb{M} : \rho$. The case **var** and $\omega$ are immediate. If $\Phi$ ends in a $\to_I$ rule with premise $x_1 : \pi_1, \dots, x_n : \pi_n, y : \zeta \vdash_M M' : \rho$ (where $\mathbb{M} = \lambda y.M'$), then by induction we have, for any $i \le n$, $N_i \in \llbracket \pi_i \rrbracket$ and $\mathbb{L} \in \llbracket \zeta \rrbracket$, $M'\{N_1/x_1\} \dots \{N_n/x_n\} \{\mathbb{L}/y\} \in \llbracket \rho \rrbracket$. By Lemma 40, we have $(\lambda y.M'\{N_1/x_1\} \dots \{N_n/x_n\})[\mathbb{L}^1] \in \llbracket \rho \rrbracket$, hence $(\lambda y.M')\{N_1/x_1\} \dots \{N_n/x_n\} \in \llbracket \zeta \to \rho \rrbracket$.

If $\Phi$ ends in a $\to_E$ rule with premises $x_1 : \pi_1, \dots, x_n : \pi_n \vdash_M M' : \zeta \to \rho$ and $x_1 : \pi_1, \dots, x_n : \pi_n \vdash_M P : \zeta$ (where $\mathbb{M} = M'P$), then one concludes easily by induction hypothesis once remarked that $\Phi$ must have a subproof of $x_1 : \pi_1, \dots, x_n : \pi_n \vdash_M N : \zeta$ for every term $N$ in the bag $P$.

The case $\wedge I$ is an immediate consequence of the induction hypothesis and the case of a $\leq$ rule is a consequence of the induction and of Lemma 38. $\square$

**Theorem 42.** For any term $M \in \Lambda^\|$ and for any type $\pi \not\approx \omega$, if $\Gamma \vdash_M M : \pi$, then $M$ is reducible to a must-outer-normal form by outer reduction.

*Proof.* Let $x_1 : \pi_1, \dots, x_n : \pi_n \vdash_M M : \pi$, by Lemma 38, $x_i \in \llbracket \pi_i \rrbracket$, then by Lemma 41, $M = M\{x_1/x_1\} \dots \{x_n/x_n\} \in \llbracket \pi \rrbracket$. We conclude by Lemma 39. $\square$

# 6 Conclusion and future work

We did study the notions of may and must-solvability in the resource calculus. We succeeded in characterizing completely the may-solvability, from the syntactical, operational and logical point of view. The notion of must solvability has been completely characterized only for the purely non deterministic fragment. In fact, the problem of characterizing the must-solvability in the whole calculus seems to coincide with the problem of semantically separating the two notions of failure and non termination, which is an open problem, for the moment.

The two type assignment systems we used for the logical characterization of may-solvability in $\Lambda^r$ and of must-solvability in $\Lambda^\|$ can be the starting point for providing a denotational semantics in logical forms of the two calculi. In
particular $\vdash_m$ can be presented as a logical description of a denotational model for the resource calculus, where all the may-unsolvable terms are equated. Indeed such a goal seems to us non immediate, since a quantitative account of resources does not fit well with the contextual closure of the interpretation function. For a discussion about this point see [dC09]. A possible solution might be achieved following the ideas in [BEM07].

## References

[Bar84] Henk Barendregt. *The Lambda-Calculus, its Syntax and Semantics*. Stud. Logic Found. Math., vol. 103. North-Holland, 1984.

[BCL99] Gerard Boudol, Pierre-Louis Curien, and Carolina Lavatelli. A Semantics for Lambda Calculi with Resources. *MSCS*, 9(5):437–482, 1999.

[BEM07] Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. Not Enough Points Is Enough. In *CSL*, volume 4646 of *Lecture Notes in Comp. Sci.*, pages 298–312, 2007.

[BEM09] Antonio Bucciarelli, Thomas Ehrhard, and Giulio Mazonetto. A relational semantics for parallelism and non-determinism in a functional setting. Preprint, 2009.

[Bou93] Gérard Boudol. The Lambda-Calculus with Multiplicities. *INRIA Report 2025*, 1993.

[CDCV80] Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. Principal Type Schemes and Lambda-Calculus Semantics. In *To H. B. Curry. Essays on Combinatory Logic, Lambda-calculus and Formalism*, pages 480–490. Accademic Press, 1980.

[CDCV81] Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. Functional Characters of Solvable Terms. *Zeitschrift für Mathematische Logik*, 27:45–58, 1981.

[dC09] Daniel de Carvalho. Execution Time of λ-Terms via Denotational Semantics and Intersection Types. Preprint, 2009.

[dCPTdF08] Daniel de Carvalho, Michele Pagani, and Lorenzo Tortora de Falco. A Semantic Measure of the Execution Time in Linear Logic. *Th. Comp. Sci.*, 2008. to appear.

[dP95] Ugo de'Liguoro and Adolfo Piperno. Non Deterministic Extensions of Untyped Lambda-Calculus. *Inf. Comput.*, 122(2):149–177, 1995.

[ER03] Thomas Ehrhard and Laurent Regnier. The Differential Lambda-Calculus. *Theor. Comput. Sci.*, 309(1):1–41, 2003.

[ER06] Thomas Ehrhard and Laurent Regnier. Böhm trees, Krivine's Machine and the Taylor Expansion of Lambda-Terms. In *CiE*, volume 3988 of LNCS, pages 186–197, 2006.
[ER08] Thomas Ehrhard and Laurent Regnier. Uniformity and the Taylor Expansion of Ordinary Lambda-Terms. *Theor. Comput. Sci.*, 403(2-3):347-372, 2008.

[Hyl76] J. Martin E. Hyland. A Syntactic Characterization of the Equality in Some Models of the Lambda Calculus. *J. London Math. Soc.*, 2(12):361-370, 1976.

[Kfo00] Assaf J. Kfoury. A Linearization of the Lambda-Calculus and Consequences. *J. Logic Comp.*, 10(3):411-436, 2000.

[Kri93] Jean-Louis Krivine. *Lambda-calculus, types and models*. Ellis Horwood, 1993.

[NM04] Peter M. Neergaard and Harry G. Mairson. Types, Potency, and Idempotency: why Nonlinearity and Amnesia Make a Type System Work. In Okasaki and Fisher, editors, *9th ACM SIGPLAN ICFP 2004*, pages 138-149. ACM, 2004.

[PRDR04] Luca Paolini and Simona Ronchi Della Rocca. The parametric parameter passing λ-calculus. *Information and Computation*, 189(1):87-106, February 2004.

[PRDR10] Michele Pagani and Simona Ronchi Della Rocca. Solvability in Resource Lambda-Calculus. In Luke Ong, editor, *FOSSACS*, volume 6014 of *Lecture Notes in Comp. Sci.*, pages 358-373, 2010.

[PT09] Michele Pagani and Paolo Tranquilli. Parallel Reduction in Resource Lambda-Calculus. In *APLAS*, volume 5904 of *LNCS*, pages 226-242, 2009.

[RDRP04] Simona Ronchi Della Rocca and Luca Paolini. *The Parametric λ-Calculus: a Metamodel for Computation*. EATCS Series. Springer, Berlin, 2004.

[Sco76] Dana S. Scott. Data types as lattices. *SIAM J. Comput.*, 5(3):522-587, 1976.

[Tra08] Paolo Tranquilli. Intuitionistic Differential Nets and Lambda-Calculus. *Theor. Comput. Sci.*, 2008. to appear.

[Tra09] Paolo Tranquilli. *Nets between Determinism and Nondeterminism*. Ph.D. thesis, Università Roma Tre/Université Paris Diderot (Paris 7), April 2009.

[Val01] Silvio Valentini. An elementary proof of strong normalization for intersection types. *Archive for Mathematical Logic*, 40(7):475-488, October 2001.

[Vau09] Lionel Vaux. The algebraic lambda calculus. *Math. Struct. Comp. Sci.*, 19(5):1029-1059, 2009.

[WDMT02] J. B. Wells, Allyn Dimock, Robert Muller, and Franklyn Turbak. A Calculus with Polymorphic and Polyvariant Flow Types. *J. Funct. Program.*, 12(3):183-227, 2002.