# Böhm's Theorem for Resource Lambda Calculus through Taylor Expansion

Giulio Manzonetto, Michele Pagani

► To cite this version:

Giulio Manzonetto, Michele Pagani. Böhm's Theorem for Resource Lambda Calculus through Taylor Expansion. 10th International Conference on Typed Lambda Calculi and Applications (TLCA 2011), 2011, Oxford, United Kingdom. pp.153-168, 10.1007/978-3-642-21691-6_14. http-04670290

HAL Id: hal-04670290

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

Submitted on 12 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>
# Böhm's Theorem for Resource Lambda Calculus through Taylor Expansion*

Giulio Manzonetto¹ and Michele Pagani²

¹ Intelligent Systems, Radboud University
g.manzonetto@cs.ru.nl

² Laboratoire LIPN, CNRS UMR7030 Université Paris 13
michele.pagani@lipn.univ-paris13.fr

**Abstract.** We study the resource calculus, an extension of the λ-calculus allowing to model resource consumption. We achieve an internal separation result, in analogy with Böhm's theorem of λ-calculus. We define an equivalence relation on the terms, which we prove to be the maximal non-trivial congruence on normalizable terms respecting β-reduction. It is significant that this equivalence extends the usual η-equivalence and is related to Ehrhard's Taylor expansion – a translation mapping terms into series of finite resources.

**Keywords:** differential linear logic, resource lambda-calculus, separation property, Böhm-out technique.

## Introduction

**Böhm's theorem in the λ-calculus.** Böhm's theorem [1] is a fundamental result in the untyped λ-calculus [2] stating that, given two closed distinct βη-normal λ-terms *M* and *N*, there exists a sequence of λ-terms *L*, such that *M* *L* β-reduces to the first projection λ*x*y.*x and *N* *L* β-reduces to the second projection λ*x*y.*y. The original issue motivating this result was the quest for solutions of systems of equations between λ-terms: given closed terms *M*₁, *N*₁, ..., *M*ₙ, *N*ₙ, is there a λ-term *S* such that *S*M*₁* ≡*β* *N*₁ ∧ ... ∧ *S*M*ₙ* ≡*β* *N*ₙ holds? The answer is trivial for *n* = 1 (just take *S* = λz.*N*₁ for a fresh variable *z*) and Böhm's theorem gives a positive answer for *n* = 2 and *M*₁, *M*₂ distinct βη-normal forms (apply the theorem to *M*₁, *M*₂ and set *S* = λf.f* *L* *N*₁ *N*₂). The result has been then generalized in [3] to treat every finite family *M*₁, ..., *M*ₙ of pairwise distinct βη-normal forms. This generalization is non-trivial since each *M*ᵢ may differ from the other ones at distinct addresses of its syntactic tree.

As an important consequence of Böhm's theorem we have that the βη-equivalence is the maximal non-trivial congruence on normalizable terms extending the β-equivalence. The case of non-normalizable terms has been addressed by Hyland in [4]. Indeed, the βη-equivalence is not maximal on such terms, and one must consider the congruence $\mathcal{H}^*$ equating two λ-terms whenever they have

<footnote>* This work is partly supported by NWO Project 612.000.936 CALMOC and the chaire CNRS "Logique linéaire et calcul".</footnote>
the same Böhm tree up to possibly infinite $\eta$-expansions [2, §16.2]. Then one
proves that for all closed $\lambda$-terms $M \not\equiv_{\mathcal{H}^*} N$ there is a sequence of $\lambda$-terms $\vec{L}$
such that $M\vec{L} \beta$-reduces to the identity $\lambda x.x$ while $N\vec{L}$ is unsolvable (i.e., it does
not interact with the environment [2, §8.3]) or *vice versa*. This property is called
*semi-separation* because of the asymmetry between the two values: the identity,
on the one hand, and any unsolvable term, on the other hand. In fact, non-
normalizable terms represent partial functions, and one cannot hope to separate
a term less defined than another one without sending the first to an unsolvable
term (corresponding to the empty function). Despite the fact that Hyland's semi-
separability is weaker than the full separability achieved by Böhm's theorem, it
is sufficient to entail that $\mathcal{H}^*$ is the maximal non-trivial congruence on $\lambda$-terms
extending $\beta$-equivalence and equating all unsolvable terms [2, Thm. 16.2.6].

**The resource $\lambda$-calculus.** We study Böhm's theorem in the resource $\lambda$-calculus ($\mathcal{A}^r$ for short), which is an extension of the $\lambda$-calculus along two directions. First, $\mathcal{A}^r$ is resource sensitive. Following Girard's linear logic [5], the $\lambda$-calculus application can be written as $M(N^1)$ emphasizing the fact that the argument $N$ is actually infinitely available for the function $M$, i.e. it can be erased or copied as many times as needed during the evaluation. $\mathcal{A}^r$ extends this setting by allowing also applications of the form $M(N^n)$ where $N^n$ denotes a finite resource that must be used exactly $n$-times during the evaluation. If the number $n$ does not match the needs of $M$ then the application evaluates to the empty sum 0, expressing the absence of a result. In fact, 0 is a $\beta$-normal form giving a notion of unsolvable different from the $\lambda$-calculus one represented by looping terms$^3$. The second feature of $\mathcal{A}^r$ is the non-determinism. Indeed, the argument of an application, instead of being a single term, is a bag of resources, each being either finite or infinitely available. In the evaluation several possible choices arise, corresponding to the different possibilities of distributing the resources among the occurrences of the formal parameter. The outcome is a finite formal sum of terms collecting all possible results.

Boudol has been the first to extend the $\lambda$-calculus with a resource sensitive
application [8]. His resource calculus was designed to study Milner's encoding of
the lazy $\lambda$-calculus into the $\pi$-calculus [9,10]. Some years later, Ehrhard and Reg-
nier introduced the differential $\lambda$-calculus [11], drawing on insights gained from
the quantitative semantics of linear logic, denoting proofs/terms as smooth (i.e.
infinitely differentiable) functions. As remarked by the authors, the differential
$\lambda$-calculus is quite similar to Boudol's calculus, the resource sensitive applica-
tion $M(N^n)$ corresponds to applying the $n$-th derivative of $M$ at 0 to $N$. This
intuition was formalized by Tranquilli, who defined the present syntax of $\mathcal{A}^r$ and
showed a Curry-Howard correspondence between this calculus and Ehrhard and
Regnier's differential nets [12]. The main differences between Boudol's calculus
and $\mathcal{A}^r$ are that the former is equipped with explicit substitution and lazy oper-
ational semantics, while the latter is a true extension of the regular $\lambda$-calculus.
Since we cannot separate $M$ from $M + M$ we will conveniently suppose that

<footnote n="3">³ Denotational models of $\mathcal{A}^r$ distinguishing between 0 and the usual unsolvable terms are built in [6]. For more details on the notion of solvability in $\mathcal{A}^r$ see [7].</footnote>
the sum on $\Lambda^r$ is idempotent as in [13]; this amounts to say that we only check
whether a term appears in a result, not how many times it appears.

**A resource conscious Böhm's theorem.** A notable outcome of Ehrhard and Regnier's work has been to develop the $\lambda$-calculus application as an infinite series of finite applications, $M(N^1) = \sum_{n=0}^{\infty} \frac{1}{n!} M(N^n)$, in analogy with the Taylor expansion of the entire functions. In [14], the authors relate the Böhm tree of a $\lambda$-term with its Taylor expansion, giving the intuition that the latter is a resource conscious improvement of the former. Following this intuition, we achieve the main result of this paper, namely a separation property in $\Lambda^r$ that can be seen as a resource sensitive Böhm's theorem (Theorem 2). Such a result states that for all closed $\beta$-normal $M, N$ having $\eta$-different Taylor expansion, there is a sequence $\vec{L}$, such that $M\vec{L} \beta$-reduces to $\lambda x.x$ and $N\vec{L} \beta$-reduces to 0, or vice versa.

This theorem reveals a first sharp difference between $\Lambda^r$ and the $\lambda$-calculus,
as our result is more similar to Hyland's semi-separation than Böhm's theorem,
even if we consider the $\beta$-normal forms. This is due to the empty sum 0, the
unsolvable $\beta$-normal form, outcome of the resource consciousness of $\Lambda^r$.

Taylor expansion is a semantical notion, in the sense that it is an infinite series
of finite terms. It is then notable that we give a syntactic characterization of the
Taylor equality introducing the $\tau$-equivalence in Definition 3 (Proposition 1). As
expected, our semi-separability is strong enough to entail that the $\eta\tau$-equivalence
induces the maximal non-trivial congruence on $\beta$-normalizable terms extending
the $\beta$-equivalence (Corollary 1).

A crucial ingredient in the classic proof of Böhm's theorem is the fact that
it is possible to erase subterms in order to pull out of the terms their structural
difference. This is not an easy task in $\Lambda^r$, since the finite resources must be con-
sumed and cannot be erased. In this respect, our technique has some similarities
with the one developed to achieve the separation for the $\lambda I$-calculus (i.e., the
$\lambda$-calculus without weakening, [2, §10.5]). Moreover, since the argument of an
application is a bag of resources, comparing a difference between two terms may
turn into comparing the differences between two multisets of terms, and this
problem presents analogies with that of separating a finite set of terms [3].

**Basic definitions and notations.** We let $\mathbf{N}$ denote the set of natural numbers. Given a set $\mathcal{X}$, $\mathcal{M}_f(\mathcal{X})$ is the set of all finite multisets over $\mathcal{X}$. Given a reduction $\rightarrow_f$ we let $\langle\cdot\rangle_f$, $\stackrel{r*}{\rightarrow}$ and $\equiv_r$ denote its transpose, its transitive-reflexive closure and its symmetric-transitive-reflexive closure, respectively.

An operator $F(-)$ (resp. $F(-, -)$) is extended by linearity (resp. bilinearity)
by setting $F(\Sigma_i A_i) = \Sigma_i F(A_i)$ (resp. $F(\Sigma_i A_i, \Sigma_j B_j) = \Sigma_{i,j} F(A_i, B_j)$).

# 1 Resource Calculus

**Syntax.** The resource calculus has three syntactic categories: terms that are in
functional position, bags that are in argument position and represent unordered
lists of resources, and finite formal sums that represent the possible results of
$\Lambda^r$: $M, N, L$ ::= $x \mid \lambda x.M \mid MP$ terms

$\Lambda^b$: $P, Q, R$ ::= $[M_1, \dots, M_n, M^1]$ bags

$\Lambda^e$: $A, B$ ::= $M \mid P$ expressions

$M, N \in 2\langle\Lambda^r\rangle \ P, Q \in 2\langle\Lambda^b\rangle \ A, B \in 2\langle\Lambda^e\rangle := 2\langle\Lambda^r\rangle \cup 2\langle\Lambda^b\rangle$ sums

(a) Grammar of terms, resources, bags, expressions, sums.

$\lambda x.(\sum_i M_i) := \sum_i \lambda x.M_i \qquad M(\sum_i P_i) := \sum_i MP_i$

$(\sum_i M_i)P := \sum_i M_i P \qquad [(\sum_i M_i)] \cdot P := \sum_i [M_i] \cdot P$

(b) Notation on $2\langle\Lambda^e\rangle$.

$y\langle N/x \rangle := \begin{cases} N & \text{if } y = x, \\ 0 & \text{otherwise,} \end{cases} \quad (\lambda y.M)\langle N/x \rangle := \lambda y.(M\langle N/x \rangle),$

$$ (MP)\langle N/x \rangle := M\langle N/x \rangle P + M\langle P\langle N/x \rangle \rangle, $$

$$ [M^1]\langle N/x \rangle := [M\langle N/x \rangle, M^1], \quad ([M] \cdot P)\langle N/x \rangle := [M\langle N/x \rangle] \cdot P + [M] \cdot P\langle N/x \rangle, $$

(c) Linear substitution, in the abstraction case we suppose $y \notin \text{FV}(N) \cup \{x\}$.

<caption>**Fig. 1:** Syntax, notations and linear substitution of resource calculus.</caption>

a computation. Figure 1(a) provides the grammar for generating the set $\Lambda^r$ of terms and the set $\Lambda^b$ of bags, together with their typical metavariables.

A bag $[\vec{M}, M^!]$ is a compound object, consisting of a multiset of linear resources $[\vec{M}]$ and a set of terms $M$ presented in additive notation (see the discussion on sets and sums below) representing the reusable resources. Roughly speaking, the linear resources in $\vec{M}$ must be used exactly once during a reduction, while the reusable ones in $M$ can be used ad libitum (hence, following the linear logic notation, $M$ is decorated with a $!$ superscript).

We shall deal with bags as if they were multisets presented in multiplicative notation, defining union by $[\vec{M}, M^!] \cdot [\vec{N}, N^!] := [\vec{M}, \vec{N}, (M+N)!]$. This operation is commutative, associative and has the empty bag $1 := [0!]$ as neutral element. To avoid confusion with application we will never omit the dot “.”. To lighten the notations we write $[L_1, \dots, L_k]$ for the bag $[L_1, \dots, L_k, 0!]$, and $[M^k]$ for the bag $[M, \dots, M]$ containing $k$ copies of $M$. Such a notation allows to decompose a bag in several ways, and this will be used throughout the paper.

As for example:

$$ [x, y, (x+y)!] = [x] \cdot [y, (x+y)!] = [x!] \cdot [x, y, y!] = [x, y] \cdot [(x+y)!] = [x, x!] \cdot [y, y!] $$

Expressions (whose set is denoted by $\Lambda^e$) are either terms or bags and will be used to state results holding for both categories.

Let **2** be the semiring $\{0, 1\}$ with $1 + 1 = 1$ and multiplication defined in the obvious way. For any set $\mathcal{X}$, we write $2\langle\mathcal{X}\rangle$ for the free 2-module generated by $\mathcal{X}$, so that $2\langle\mathcal{X}\rangle$ is isomorphic to the finite powerset of $\mathcal{X}$, with addition corresponding to union, and scalar multiplication defined in the obvious way.
However we prefer to keep the algebraic notations for elements of $\mathbf{2}\langle\mathcal{X}\rangle$, hence set union will be denoted by $+$ and the empty set by $0$. This amounts to say that $\mathbf{2}\langle\Lambda^r\rangle$ (resp. $\mathbf{2}\langle\Lambda^b\rangle$) denotes the set of finite formal sums of terms (resp. bags), with an idempotent sum. We also set $\mathbf{2}\langle\Lambda^e\rangle = \mathbf{2}\langle\Lambda^r\rangle \cup \mathbf{2}\langle\Lambda^b\rangle$. This is an abuse of notation, as $\mathbf{2}\langle\Lambda^e\rangle$ here does not denote the $\mathbf{2}$-module generated over $\Lambda^e = \Lambda^r \cup \Lambda^b$ but rather the union of the two $\mathbf{2}$-modules; this amounts to say that sums may be taken only in the same sort.

The size of $A \in \mathbf{2}\langle\Lambda^e\rangle$ is defined inductively by: $\text{size}(\Sigma_i A_i) = \Sigma_i \text{size}(A_i)$, $\text{size}(x) = 1$, $\text{size}(\lambda x.M) = \text{size}(M) + 1$, $\text{size}(MP) = \text{size}(M) + \text{size}(P) + 1$, $\text{size}([M_1, \dots, M_k, M^!]) = \sum_{i=1}^k \text{size}(M_i) + \text{size}(M) + 1$.

Notice that the grammar for terms and bags does not include any sums, but under the scope of a $(\cdot)^!$. However, as syntactic sugar – and not as actual syntax – we extend all the constructors to sums as shown in Figure 1(b). In fact all constructors except the $(\cdot)^!$ are (multi)linear, as expected. The intuition is that a reusable sum $(M+N)^!$ represents a resource that can be used several times and each time one can choose non-deterministically $M$ or $N$.

Observe that in the particular case of empty sums, we get $\lambda x.0 := 0$, $M0 := 0$, $0P := 0$, $[0] := 0$ and $0 \cdot P := 0$, but $[0^!] = 1$. Thus $0$ annihilates any term or bag, except when it lies under a $(\cdot)^!$. As an example of this extended (meta-)syntax, we may write $(x_1+x_2)[y_1+y_2, (z_1+z_2)^!]$ instead of $x_1[y_1, (z_1+z_2)^!]+x_1[y_2, (z_1+z_2)^!]+x_2[y_1, (z_1+z_2)^!]+x_2[y_2, (z_1+z_2)^!]$. This kind of meta-syntactic notation is discussed thoroughly in [14].

The $\alpha$-equivalence and the set $\text{FV}(A)$ of free variables are defined as in ordinary $\lambda$-calculus. From now on expressions are considered up to $\alpha$-equivalence. Concerning specific terms we set:

$$ \mathbf{I} := \lambda x.x, \qquad \mathbf{X}_n := \lambda x_1 \dots \lambda x_n \lambda x.x[x_1^! \dots [x_n^!]] \text{ for } n \in \mathbb{N}, $$

where $\mathbf{X}_n$ is called the $n$-th Böhm permutator.

Due to the presence of two kinds of resources, we need two different notions of substitutions: the usual $\lambda$-calculus substitution and a linear one, which is particular to differential and resource calculi (see [14,15]).

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

1. $A\{N/x\}$ is the usual capture-free substitution of $N$ for $x$ in $A$. It is extended to sums as in $A\{\mathbb{N}/x\}$ by linearity in $A$, and using the notations of Figure 1(b) for $\mathbb{N}$.

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

Intuitively, linear substitution replaces the resource to *exactly one* linear free occurrence of the variable. In presence of multiple occurrences, all possible choices are made and the result is the sum of them. E.g., $(x[x])\langle\mathbf{I}/x\rangle = \mathbf{I}[x] + x[\mathbf{I}]$.

*Example 1.* Notice the difference between $[x, x^!]\{M + N/x\} = [(M + N), (M + N)^!] = [M, (M + N)^!] + [N, (M + N)^!]$ and $[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^!]$.
Linear substitution bears resemblance to differentiation, as shown clearly in Ehrhard and Regnier's differential λ-calculus [11]. For instance, it enjoys the following Schwarz's Theorem, whose proof is rather classic and is omitted.

**Lemma 1 (Schwarz's Theorem [14,11]).** Given $A \in 2\langle\Lambda^e\rangle$, $M, N \in 2\langle\Lambda^r\rangle$ and $y \notin \text{FV}(M) \cup \text{FV}(N)$ we have $A\langle M/y \rangle \langle N/x \rangle = A\langle N/x \rangle \langle M/y \rangle + A\langle M\langle N/x \rangle \rangle/y$. In particular, if $x \notin \text{FV}(M)$ the two substitutions commute.

$$ \begin{array}{ccc} \frac{M R M}{\lambda x. M R \lambda x.M} & \text{lam} & \frac{M R M}{MP R MP} \text{app1} \\ \frac{M R M}{[M] \cdot P R [M] \cdot P} & \text{lin} & \frac{M R M}{[M'] \cdot P R [M'] \cdot P} \text{bng} \\ & & \frac{P R P}{A + B R A + B} \text{sum} \end{array} $$

(a) Rules defining the context closure of a relation $R \subseteq \Lambda^e \times 2\langle\Lambda^e\rangle$.

$$ \begin{array}{ccc} \frac{M R N}{\lambda x. M R \lambda x.N} & \text{lam} & \frac{M R N P R Q}{MP R NQ} \text{app} \\ \frac{M R N P R Q}{[M] \cdot P R [N] \cdot Q} & \text{lin} & \frac{M R N}{[M'] R [N']} \text{bng} \\ & & \frac{A R B A' R B'}{A + A' R B + B'} \text{sum} \end{array} $$

(b) Rules defining a compatible relation $R \subseteq 2\langle\Lambda^e\rangle \times 2\langle\Lambda^e\rangle$.

<caption>**Fig. 2:** Definition of context closure and compatible relation.</caption>

**Operational semantics.** Given a relation $R \subseteq \Lambda^e \times 2\langle\Lambda^e\rangle$ its context closure is the smallest relation in $2\langle\Lambda^e\rangle \times 2\langle\Lambda^e\rangle$ containing $R$ and respecting the rules of Figure 2(a). The main notion of reduction of resource calculus is $\beta$-reduction, which is defined as the context closure of the following rule:

$$ (\beta) \qquad (\lambda x.M)[L_1, \dots, L_k, N'] \stackrel{\beta}{\to} M\langle L_1/x \rangle \cdots \langle L_k/x \rangle \{N/x\}. $$

Notice that the $\beta$-rule is independent of the ordering of the linear substitutions, as shown by the Schwarz's Theorem above. We say that $A \in \Lambda^e$ is in $\beta$-normal form ($\beta$-nf, for short) if there is no $A$ such that $A \stackrel{\beta}{\to} A$. A sum $A$ is in $\beta$-nf if all its summands are. Notice that 0 is a $\beta$-nf. It is easy to check that a term $M$ is in $\beta$-nf iff $M = \lambda x_1 \dots x_n y P_1 \dots P_k$ for $n, k \ge 0$ and, for every $1 \le i \le k$, all resources in $P_i$ are in $\beta$-nf. The variable $y$ in $M$ is called head-variable.

The regular λ-calculus [2] can be embedded into the resource one by translating every application $MN$ into $M[N']$. In this fragment the $\beta$-reduction defined above coincides with the usual one. Hence the resource calculus has usual looping terms like $\Omega := (\lambda x.x[x'])[(\lambda x.x[x'])']$, but also terms like $\mathbf{I}1$ or $\mathbf{I}[y, y]$ reducing to 0 because there is a mismatch between the number of linear resources needed by the functional part of the application and the number it actually receives.
$$ (\sum_i A_i)^\circ := \bigcup_i A_i^\circ \qquad x^\circ := \{x\} \qquad (\lambda x.M)^\circ := \lambda x.M^\circ \qquad (MP)^\circ := M^\circ P^\circ $$

$$ ([M^\prime])^\circ := \mathcal{M}_f(M^\circ) \qquad ([M] \cdot P)^\circ := [M^\circ] \cdot P^\circ $$

<caption>Fig. 3: Taylor expansion $A^\circ$ of $A$.</caption>

**Theorem 1 (Confluence [15]).** The $\beta$-reduction is Church-Rosser on $\Lambda^r$.

The resource calculus is *intensional*, indeed just like in the $\lambda$-calculus there are different programs having the same extensional behaviour. In order to achieve an internal separation, we need to consider the $\eta$-reduction that is defined as the contextual closure of the following rule:

$$ (\eta) \qquad \lambda x.M[x^1] \xrightarrow{\eta} M, \text{ if } x \notin \mathrm{FV}(M). $$

**The Taylor expansion.** The finite resource calculus is the fragment of resource calculus having only linear resources (every bag has the set of reusable resources empty). The terms (resp. bags, expressions) of this sub-calculus are called *finite* and their set is denoted by $\Lambda_f^r$ (resp. $\Lambda_f^b, \Lambda_f^e$). Notice that the bags of $\Lambda_f^b$ are actually finite multisets. It is easy to check that the above sets are closed under $\beta$-reduction, while $\eta$-reduction cannot play any role here.

In Definition 2, we describe the Taylor expansion as a map $(\cdot)^\circ$ from $2\langle\Lambda^r\rangle$ (resp. $2\langle\Lambda^b\rangle$) to possibly infinite sets of finite terms (resp. finite bags). The Taylor expansion defined in [11,14], in the context of $\lambda$-calculus, is a translation developing every application as an infinite series of finite applications with rational coefficients. In our context, since the coefficients are in $2$, the Taylor expansion of an expression is a (possibly infinite) set of finite expressions. Indeed, for all sets $\mathcal{X}$, the set of the infinite formal sums $2\langle\mathcal{X}\rangle_\infty$ with coefficients in $2$ is isomorphic to the powerset of $\mathcal{X}$. Our Taylor expansion corresponds to the support$^4$ of the Taylor expansion taking rational coefficients given in [11,14].

To lighten the notations, we adopt for sets of expressions the same abbreviations as introduced for finite sums in Figure 1(b). For example, given $\mathcal{M} \subseteq \Lambda_f^r$ and $\mathcal{P}, \mathcal{Q} \subseteq \Lambda_f^b$ we have $\lambda x.\mathcal{M} = \{\lambda x.M \mid M \in \mathcal{M}\}$ and $\mathcal{P} \cdot \mathcal{Q} = \{P \cdot Q \mid P \in \mathcal{P}, Q \in \mathcal{Q}\}$.

**Definition 2.** Let $A \in 2\langle\Lambda^e\rangle$. The Taylor expansion of $A$ is the set $A^\circ \subseteq \Lambda_f^e$ which is defined (by structural induction on $A$) in Figure 3.

*Example 2.* As previously announced, the Taylor expansion of an expression $A$ can be infinite, e.g., $(\lambda x.x[x^1])^\circ = \{\lambda x.x[x^n] \mid n \in \mathbb{N}\}$. Different terms may share the same Taylor expansion: $(x[(z[y^1])^1])^\circ = (x[(z1 + z[y, y^1])^1])^\circ$. The presence of linear resources permits situations where $M^\circ \subsetneq N^\circ$, for example $M := x[x, x^1], N := x[x^1]$. The presence of non-determinism allows to build terms like

<footnote>$^4$ I.e., the set of those finite terms appearing in the series with a non-zero coefficient.</footnote>
$M_1 := x[(y+z)']$, $M_2 := x[(y+h)']$ such that $M_1^\circ \cap M_2^\circ = \{x[y^n] \mid n \in \mathbb{N}\}$ is infinite. However the intersection can also be finite as in $N_1 := x[y, z']$, $N_2 := x[z, y']$ where $N_1^\circ \cap N_2^\circ = \{x[y, z]\}$.

## 2 A Syntactic Characterization of Taylor Equality

In $\Lambda^r$, there are distinct $\beta\eta$-nf's which are inseparable, in contrast with what we have in the regular $\lambda$-calculus. In fact, all normal forms having equal Taylor expansions are inseparable, since the first author proved in [16] that there is a non-trivial denotational model of resource calculus equating all terms having the same Taylor expansion. For example, $x[(z[y']')']$ and $x[(z1+z[y, y'])']$ are distinct inseparable $\beta\eta$-nf's since they have the same Taylor expansion.

Because of its infinitary nature, the property of having the same Taylor expansion is more semantical than syntactical. In this section, we provide an alternative syntactic characterization (Definition 3, Proposition 1).

A relation $R \subseteq 2\langle\Lambda^e\rangle \times 2\langle\Lambda^e\rangle$ is compatible if it satisfies the rules in Figure 2(b). The congruence generated by a relation $R$, denoted $\equiv_R$, is the smallest compatible equivalence relation containing $R$. Given two relations $R, S \subseteq 2\langle\Lambda^e\rangle \times 2\langle\Lambda^e\rangle$, we write $\equiv_{RS}$ for the congruence generated by their union $R \cup S$.

**Definition 3.** The Taylor equivalence $\equiv_\tau$ is the congruence generated by:

$$ (\tau) \qquad [M'] \equiv_\tau 1 + [M, M'] $$

Moreover, we set $A \sqsubseteq_\tau B$ iff $A + B \equiv_\tau B$.

It is not difficult to check that $\sqsubseteq_\tau$ is a compatible preorder. We now prove that it captures exactly the inclusion between Taylor expansions (Proposition 1).

**Example 3.** We have $z[x, x'] + z1 \equiv_\tau z[x'] \sqsubseteq_\tau z[x, x'] + z[y']$, while $x[x'] \not\equiv_\tau x[y', y']$.

Note that all elements of $A^\circ$ share the same minimum structure, called here skeleton, obtained by taking 0 occurrences of every reusable resource.

**Definition 4.** Given $A \in \Lambda^e$, its skeleton $\mathfrak{s}(A) \in \Lambda_f^e$ is obtained by erasing all the reusable resources occurring in A. That is, inductively:

$$ \mathfrak{s}(x) := x, \quad \mathfrak{s}(\lambda x.M) := \lambda x.\mathfrak{s}(M), \quad \mathfrak{s}(MP) := \mathfrak{s}(M)\mathfrak{s}(P), $$

$$ \mathfrak{s}([M_1, \dots, M_n, \mathbb{M}']) := [\mathfrak{s}(M_1), \dots, \mathfrak{s}(M_n)]. $$

Obviously $\mathfrak{s}(A) \in A^\circ$. In general it is false that $\mathfrak{s}(A) \in B^\circ$ entails $A \sqsubseteq_\tau B$. Take for instance $A := x[x']$ and $B := x[y'];$ indeed $\mathfrak{s}(A) = x1 \in \{x[y^n] \mid n \in \mathbb{N}\} = B^\circ$. The above implication becomes however true when A is “expanded enough”.

**Definition 5.** Given $k \in \mathbb{N}$, we say that $A \in \Lambda^e$ is $k$-expanded if it is generated by the following grammar:

$$ M, N ::= x \mid \lambda x.M \mid MP \qquad P, Q ::= 1 \mid [M] \cdot P \mid [M^k, M'] \cdot P $$
*Example 4.* The terms $x, \lambda y.x[y]$ and $x1$ are $k$-expanded for all $k \in \mathbb{N}$. The bag $[y^4, x^3, (x+y)!]$ is 3-expanded since it can be decomposed as $[x^3, x'] \cdot [y^4, y!]$, while it is not 4-expanded.

**Lemma 2.** Let $A \in \Lambda^e$ be $k$-expanded for some $k \in \mathbb{N}$. Then for every $B \in \Lambda^e$ such that $\text{size}(B) \le k$, we have that $\mathfrak{s}(A) \in B^\circ$ entails $A \sqsubseteq_\tau B$.

*Proof.* By induction on $A$. The only significant case is when $A$ is a bag, which splits in three subcases, depending on how such a bag can be decomposed.

**CASE I (A = [M^k, M!].P, P k-EXPANDED).** By definition $\mathfrak{s}(A) = [\mathfrak{s}(M)^k] \cdot \mathfrak{s}(P)$. From $\mathfrak{s}(A) \in B^\circ$, we deduce that $B = Q_1 \cdot Q_2 \cdot Q_3$ where $Q_1 = [L_1, \dots, L_\ell]$, $Q_2 = [(N_1 + \dots + N_n)!]$ for some $\ell, n \ge 0$ and $Q_1, Q_2, Q_3$ are such that $[\mathfrak{s}(M)^\ell] \in Q_1^\circ$, $[\mathfrak{s}(M)^{k-\ell}] \in Q_2^\circ$ and $\mathfrak{s}(P) \in (Q_2 \cdot Q_3)^\circ$. From $\text{size}(B) \le k$ we get $\ell < k$ and this entails $n > 0$. We then have that $\mathfrak{s}(M) \in L_i^\circ$, for every $i \le \ell$, and there is a $j$ such that $\mathfrak{s}(M) \in N_j^\circ$. By induction hypothesis, we have $M \sqsubseteq_\tau L_i$ for every $i \le \ell$, $M \sqsubseteq_\tau N_j$ and $P \sqsubseteq_\tau Q_2 \cdot Q_3$. Hence, by compatibility of $\sqsubseteq_\tau$, we derive $[M^\ell] \sqsubseteq_\tau Q_1$ and $[M!] \sqsubseteq_\tau [N_j^!]$, that entails $[M^k, M!] \sqsubseteq_\tau [M^\ell, M!] \sqsubseteq_\tau Q_1 \cdot [N_j^!]$. From this, using $[N_j^!] \cdot Q_2 \equiv_\tau Q_2$ and $P \sqsubseteq_\tau Q_2 \cdot Q_3$, we conclude $A \sqsubseteq_\tau Q_1 \cdot [N_j^!] \cdot Q_2 \cdot Q_3 \equiv_\tau B$.

**CASE II (A = [M] · P, P WITHOUT REUSABLE RESOURCES).** By definition $\mathfrak{s}(A) = [\mathfrak{s}(M)] \cdot \mathfrak{s}(P)$. Suppose $\mathfrak{s}(A) \in B^\circ$, then two subcases are possible.

Case $B = [N] \cdot Q$ such that $\mathfrak{s}(M) \in N^\circ$ and $\mathfrak{s}(P) \in Q^\circ$. By induction hypothesis $M \sqsubseteq_\tau N$ and $P \sqsubseteq_\tau Q$. By compatibility, $A = [M] \cdot P \sqsubseteq_\tau [N] \cdot Q = B$.

Case $B = [N!] \cdot Q$ such that $\mathfrak{s}(M) \in N^\circ$ and $\mathfrak{s}(P) \in ([N!] \cdot Q)^\circ$. Then by induction hypothesis, $M \sqsubseteq_\tau N$ and $P \sqsubseteq_\tau [N!] \cdot Q$, and, always by compatibility of $\sqsubseteq_\tau$, we conclude that $A = [M] \cdot P \sqsubseteq_\tau [N, N!] \cdot Q \sqsubseteq_\tau B$.

**CASE III (A = 1).** From $\mathfrak{s}(A) = 1 \in B^\circ$, we deduce $B$ is a bag containing only reusable resources, hence trivially $A = 1 \sqsubseteq_\tau B$. $\square$

**Lemma 3.** For all $A \in \Lambda^e$ and $k \in \mathbb{N}$ there is a $k$-expanded $\mathbb{A}$ such that $A \equiv_\tau \mathbb{A}$.

*Proof.* By immediate structural induction on $A$. The crucial case is when $A = [M!] \cdot P$. Then by induction hypothesis $M \equiv_\tau \mathbb{M}$ and $P \equiv_\tau \mathbb{P}$ for some $k$-expanded $\mathbb{M}, \mathbb{P}$. Let us explicit the first sum into $\mathbb{M} = M_1 + \dots + M_m$. Then, we have:

$$[M!] \cdot P \equiv_\tau [M!] \cdot P \equiv_\tau [M_1^k, \dots, M_m^k, M!] \cdot P + \sum_{n_1=0}^{k-1} \dots \sum_{n_m=0}^{k-1} [M_1^{n_1}, \dots, M_m^{n_m}] \cdot P.$$

Note that all summands in the last sum are $k$-expanded, since so are $\mathbb{M}, \mathbb{P}$. $\square$

**Proposition 1.** For all $A, B \in 2\langle\Lambda^e\rangle$ we have that $A \sqsubseteq_\tau B$ iff $A^\circ \subseteq B^\circ$.

*Proof.* (⇒) By a trivial induction on a derivation of $A+B \equiv_\tau B$, remarking that all rules defining $\equiv_\tau$ preserve the property of having equal Taylor expansion.

(←) By induction on the number of terms in the sum $A$. If $A = 0$, then clearly $A \sqsubseteq_\tau B$ by the reflexivity of $\equiv_\tau$. If $A = A + A'$, then by induction hypothesis we have $A' \sqsubseteq_\tau B$. As for $A$, let $k \ge \max(\text{size}(A), \text{size}(B))$, by Lemma 3, we have a $k$-expanded sum $A'' = A_1 + \dots + A_a \equiv_\tau A$. From $A'' \equiv_\tau A$ and the already proved
left-to-right direction of the proposition we get $(A'')^\circ = A^\circ \subseteq \mathbb{B}^\circ$. This means that $A_i^\circ \subseteq \mathbb{B}^\circ$ for all $i \le a$. In particular $\mathfrak{s}(A_i) \in B_{ji}^\circ$, for a particular summand $B_{ji}$ of $\mathbb{B}$. Since we are supposing that $A_i$ is $k$-expanded and size($B_{ji}$) $\le k$, we can apply Lemma 2, so arguing $A_i \subseteq_{\tau} B_{ji} \subseteq_{\tau} \mathbb{B}$. Since this holds for every $i \le a$, we get $A'' \subseteq_{\tau} \mathbb{B}$. Then we can conclude $\mathfrak{A} \equiv_{\tau} \mathfrak{A}' + \mathfrak{A}'' \subseteq_{\tau} \mathbb{B} + \mathbb{B} \equiv_{\tau} \mathbb{B}$. $\square$

We conclude that $\equiv_{\tau}$ deserves the name of Taylor equivalence.

### 3 Separating a Finite Term from Infinitely Many Terms

We now know that two $\beta\eta$-nf's $\mathbb{M}, \mathbb{N}$ such that $\mathbb{M} \equiv_{\tau} \mathbb{N}$ are inseparable; hence, in order to achieve an internal separation, we need to consider the $\eta\tau$-difference. One may hope that $\mathbb{M} \not\equiv_{\eta\tau} \mathbb{N}$ is equivalent to first compute the $\eta$-nf of two $\beta$-normal $\mathbb{M}, \mathbb{N}$ and then check whether they are $\tau$-different. Unfortunately, this is false as shown in the following counterexample (which is a counterexample to the fact that $\eta$-reduction is confluent modulo $\equiv_{\tau}$ [17, §14.3]).

**Example 5.** For all variables $a, b$ we define the sums $\mathbb{M}_{a,b} := v[\lambda z.a1, \lambda z.b[z^1]] + v[\lambda z.a[z^1], \lambda z.b[z^1]]$ and $\mathbb{N}_{a,b} := v[\lambda z.a1, b] + v[a, b]$. Note that $\mathbb{M}_{a,b} \xrightarrow{\eta^*} \mathbb{N}_{a,b}$, hence:

$$ \mathbb{N}_{x,y} \xrightarrow{\eta^*} \mathbb{M}_{x,y} \equiv_{\tau} v[\lambda z.x[z^1], \lambda z.y[z^1]] \equiv_{\tau} \mathbb{M}_{y,x} \xrightarrow{\eta^*} \mathbb{N}_{y,x}. $$

Now, if $x \neq y$, then $\mathbb{N}_{x,y}$ and $\mathbb{N}_{y,x}$ are two inseparable but distinct $\beta\eta$-nf's such that $\mathbb{N}_{x,y} \not\equiv_{\tau} \mathbb{N}_{y,x}$.

The above example shows that, to study the $\eta\tau$-difference, we cannot simply analyze the structure of the $\eta$-nf's. Our solution will be to introduce a relation $\preceq_s$ such that $\mathbb{M} \not\equiv_{\eta\tau} \mathbb{N}$ entails either $\mathbb{M} \not\preceq_s \mathbb{N}$ or vice versa (Definition 7). Basically, this approach corresponds to first compute the Taylor expansion of $\mathbb{M}, \mathbb{N}$ and then compute their $\eta$-nf pointwise, using the following partial $\eta$-reduction on $\Lambda_f^r$.

**Definition 6.** The partial $\eta$-reduction $\xrightarrow{\varphi}$ is the contextual closure of the rule $\lambda x.M[x^n] \xrightarrow{\varphi} M$ if $x \notin \text{FV}(M)$.

We define the relation $\preceq_s$ corresponding to the *Smith extension* of $\xrightarrow{\varphi^*}$ and $\preceq_{\tau}$ corresponding to the relation "$\eta \sqsubseteq_{\tau}^{\eta}$" of [2, Def. 10.2.32] keeping in mind the analogy between Taylor expansions and Böhm trees discussed in [14].

**Definition 7.** Given $\mathbb{M}, \mathbb{N} \in \mathbb{2}\langle\Lambda^r\rangle$ we define:

$$ - \mathbb{M} \preceq_s \mathbb{N} \text{ iff } \forall M \in \mathbb{M}^\circ, \exists N \in \mathbb{N}^\circ \text{ such that } M \xrightarrow{\varphi^*} N. $$

$$ - \mathbb{M} \preceq_{\tau} \mathbb{N} \text{ iff } \exists \mathbb{M}' \xrightarrow{\eta^*} \mathbb{M}, \exists \mathbb{N}' \xrightarrow{\eta^*} \mathbb{N} \text{ such that } \mathbb{M}' \sqsubseteq_{\tau} \mathbb{N}'. $$

It is easy to check that $\preceq_s$ is a preorder, and we conjecture that also $\preceq_{\tau}$ is (we will not prove it because unnecessary for the present work).

**Remark 1.** It is clear that $\mathbb{M} \xrightarrow{\eta} \mathbb{N}$ implies $\mathbb{M} \preceq_s \mathbb{N}$. More generally, by transitivity of $\preceq_s$ we have that $\mathbb{M} \xrightarrow{\eta^*} \mathbb{N}$ entails $\mathbb{M} \preceq_s \mathbb{N}$.
**Lemma 4.** Let $M, N \in 2\langle A^r \rangle$. Then $M \preceq_{\tau} N$ and $N \preceq_{\tau} M$ entails $M \equiv_{\eta_{\tau}} N$

*Proof.* By hypothesis we have $M', M'' \xrightarrow{\eta^*} M$, $N', N'' \xrightarrow{\eta^*} N$, such that $M' \subseteq_{\tau} N'$ and $N'' \subseteq_{\tau} M''$. Then, $N' \equiv_{\tau} M' + N' \xrightarrow{\eta^*} M + N$, hence $N \equiv_{\eta_{\tau}} M + N$. Symmetrically, $M'' \equiv_{\tau} M'' + N'' \xrightarrow{\eta^*} M + N$, hence $M \equiv_{\eta_{\tau}} M + N$, and we conclude $M \equiv_{\eta_{\tau}} N$. $\square$

Notice that in the above proof it is crucial the idempotency of the sum.

**Lemma 5.** Let $M, N \in 2\langle A^r \rangle$. Then $M \preceq_s N$ entails $M \preceq_{\tau} N$.

*Proof.* (Outline) Define $\text{size}^{\text{sl}}(A)$ as the size of $A$, except for the bag case, where we set $\text{size}^{\text{sl}}([M_1, \dots, M_m, (\sum_{i=m+1}^{m+k} M_i)']) := 1 + \max_i(\text{size}^{\text{sl}}(M_i))$. Notice that $\sup_{A \in \mathcal{A}}(\text{size}^{\text{sl}}(A)) \le \text{size}(A)$ (in contrast, $\sup_{A \in \mathcal{A}}(\text{size}(A))$ can be unbounded). Extend the relation $\preceq_s$ on sets $\mathcal{A}, \mathcal{B}$ of finite terms in the obvious way: $\mathcal{A} \preceq_s \mathcal{B}$ iff $\forall M \in \mathcal{A}, \exists N \in \mathcal{B}$ such that $M \xrightarrow{\varphi^*} N$. Then, the lemma follows from the following claim (take $\mathcal{A} = \mathcal{M}^\circ$ and $\mathcal{B} = \mathbb{N}$).

*Claim 1.* For all $\mathcal{A} \subseteq \mathcal{A}_f^e$ and all $\mathbb{B} \in 2\langle \mathcal{A}^e \rangle$, if $\sup_{A \in \mathcal{A}}(\text{size}^{\text{sl}}(A))$ is finite and $\mathcal{A} \preceq_s \mathbb{B}^\circ$, then there exists $\mathbb{B}' \xrightarrow{\eta^*} \mathbb{B}$ such that $\mathcal{A} \subseteq \mathbb{B}'$.

The claim is proved by induction on the triplet made of $\sup_{A \in \mathcal{A}}(\text{size}^{\text{sl}}(A))$, $\sup_{A \in \mathcal{A}}(\text{size}^{\text{sl}}(A)) - \inf_{B \in \mathbb{B}^\circ}(\text{size}^{\text{sl}}(B))$ and $\text{size}(\mathbb{B})$ lexicographically ordered. $\square$

To sum up, $M \not\equiv_{\eta_{\tau}} N$ implies that, say, $M \not\subseteq_s N$, which means $\exists M \in \mathcal{M}^\circ$ such that $\forall N \in \mathcal{N}^\circ$ we have $M \xrightarrow{\varphi^*} N$. Hence, what *Lemma 7* below does, is basically to separate such finite term $M$ from all $N$'s satisfying the condition $\forall N \in \mathcal{N}^\circ$ $M \xrightarrow{\varphi^*} N$ (that are infinitely many). For technical reasons, we will need to suppose that $M$ has a number of $\lambda$-abstractions greater than (or equal to) the number of $\lambda$-abstractions of $N$, at any depth where its syntactic tree is defined.

**Definition 8.** Let $M, N \in \mathcal{A}^r$ be $\beta$-$nf$'s of the shape $M = \lambda x_1 \dots \lambda x_a \gamma P_1 \dots P_p$, $N = \lambda x_1 \dots \lambda x_b \gamma Q_1 \dots Q_q$. We say that $M$ is $\lambda$-wider than $N$ if $a \ge b$ and each (linear or reusable) resource $L$ in $P_i$ is $\lambda$-wider than every (linear or reusable) resource $L'$ in $Q_i$, for all $i \le q$. Given $M, N$ in $\beta$-$nf$ we say that $M$ is $\lambda$-wider than $N$ iff each summand of $M$ is $\lambda$-wider than all summands of $N$.

Notice that empty bags in $M$ make it $\lambda$-wider than $N$, independently from the corresponding bags in $N$.

*Example 6.* The term $y_1$ is $\lambda$-wider than $zQ$ for any bag $Q$. The term $x[\lambda y.\mathbf{I}, \mathbf{I}]1$ is $\lambda$-wider than $x[\mathbf{I}][\mathbf{I}]$ but not than himself.

*Remark 2.* If $M$ is $\lambda$-wider than $N$ then every $M \in \mathcal{M}^\circ$ is $\lambda$-wider than $N$.

**Lemma 6.** For all $M, N$ in $\beta$-$nf$ there is a $\beta$-normal $M'$ such that $M' \xrightarrow{\eta^*} M$ and $M'$ is $\lambda$-wider than both $M$ and $N$.
Proof. (Outline) For $m > \text{size}(\mathbb{M})$, define $\mathcal{E}_m^h(M)$ by induction as follows:

$$
\begin{align*}
\mathcal{E}_m^0(\mathbb{A}) &= \mathbb{A} & \mathcal{E}_m^{h+1}(A + \mathbb{A}) &= \mathcal{E}_m^{h+1}(A) + \mathcal{E}_m^{h+1}(\mathbb{A}) \\
\mathcal{E}_m^{h+1}(\lambda x_1 \dots \lambda x_n \cdot y \vec{P}) &= \lambda x_1 \dots \lambda x_m \cdot y \mathcal{E}_m^h(\vec{P}) \mathcal{E}_m^h([x_{n+1}^!]) \dots \mathcal{E}_m^h([x_m^!]) \\
\mathcal{E}_m^{h+1}([M_1, \dots, M_k, \mathbb{M}^!]) &= [\mathcal{E}_m^{h+1}(M_1), \dots, \mathcal{E}_m^{h+1}(M_k), (\mathcal{E}_m^{h+1}(\mathbb{M}))^!]
\end{align*}
$$

Consider then $\mathbb{M}' = \mathcal{E}_k^h(\mathbb{M})$ for some $k > \max(\text{size}(\mathbb{M}), \text{size}(\mathbb{N}))$. $\square$

The next lemma will be the key ingredient for proving the resource Böhm's theorem (Theorem 2, below).

**Lemma 7 (Main Lemma).** Let $M \in \Lambda_f^r$ be a finite $\beta$-nf and $\Gamma = \{x_1, \dots, x_d\} \supseteq \text{FV}(M)$. Then, there exist a substitution $\sigma$ and a sequence $\vec{R}$ of closed bags such that, for all $\beta$-normal $\mathbb{N} \in \mathbb{2}\langle\Lambda^r\rangle$ such that $M$ is $\lambda$-wider than $\mathbb{N}$ and $\text{FV}(\mathbb{N}) \subseteq \Gamma$, we have:

$$
(1) \qquad \mathbb{N}\sigma\vec{R} \xrightarrow{\beta*} \begin{cases} \mathbf{I} & \text{if } \exists N' \in \mathbb{N}^\circ, M \xrightarrow{\varphi*} N', \\ 0 & \text{otherwise.} \end{cases}
$$

Proof. The proof requires an induction loading, namely the fact that $\sigma = \{\mathbf{X}_{k_1}/x_1, \dots, \mathbf{X}_{k_d}/x_d\}$ such that for all distinct $i, j \le d$ we have $k_i, |k_i - k_j| > 2k$ for some fixed $k > \text{size}(M)$. Recall that $\mathbf{X}_p$ has been defined in section 1.

The proof is carried by induction on size($M$). Let

$$
M = \lambda x_{d+1} \dots \lambda x_{d+a} x_h P_1 \dots P_p
$$

where $a, p \ge 0$, $h \le d + a$ and, for every $i \le p$, $P_i = [M_{i,1}, \dots, M_{i,m_i}]$ with $m_i \ge 0$. Notice that, for every $j \le m_i$, $\text{FV}(M_{i,j}) \subseteq \Gamma \cup \{x_{d+1}, \dots, x_{d+a}\}$ and $k > \text{size}(M_{i,j})$. So, define $\sigma' = \sigma \cdot \{\mathbf{X}_{k_{d+1}}/x_{d+1}, \dots, \mathbf{X}_{k_{d+a}}/x_{d+a}\}$ such that $k_i, |k_i - k_j| > 2k$, for every different $i, j \le d + a$.

By induction hypothesis on $M_{i,j}$, we have a sequence $\vec{R}_{i,j}$ of closed bags
satisfying condition (1) for every $\mathbb{N}'$ such that $M_{i,j}$ is $\lambda$-wider than $\mathbb{N}'$ and
$\text{FV}(\mathbb{N}') \subseteq \Gamma \cup \{x_{d+1}, \dots, x_{d+a}\}$.

We now build the sequence of bags $\vec{R}$ starting from such $\vec{R}_{i,j}$'s. First, we
define a closed term $H$ as follows (setting $m = \max\{k_1, \dots, k_{d+a}\}$):

$$
H := \lambda z_1 \dots \lambda z_p \lambda w_1 \dots \lambda w_{m+k_h-p} \mathbf{I} [z_1 \vec{R}_{1,1}] \dots [z_1 \vec{R}_{1,m_1}] \dots [z_p \vec{R}_{p,1}] \dots [z_p \vec{R}_{p,m_p}].
$$

$$
\text{Then we set: } \vec{R} := [\mathbf{X}_{k_{d+1}}^1] \dots [\mathbf{X}_{k_{d+a}}^1] \underbrace{1 \dots 1}_{k_h-p \text{ times}} [\mathbf{H}^1] \underbrace{1 \dots 1}_{m \text{ times}}.
$$

Notice the base of induction is when $p=0$ or for every $i \le p$, $m_i = 0$. In these cases $H$ will be of the form $\lambda \bar{z} \lambda \bar{w} \cdot \mathbf{I}$.

We prove condition (1) for any $\mathbb{N}$ satisfying the hypothesis of the lemma.
Note that we can restrict to the case $\mathbb{N}$ is a single term $N$, the general case
follows by distributing the application $\mathbb{N}\sigma\vec{R}$ on every summand of $\mathbb{N}$. So, let

$$
N = \lambda x_{d+1} \dots \lambda x_{d+b} x_h' Q_1 \dots Q_q
$$
and let us prove that $N\sigma\vec{R} \xrightarrow{\beta*} I$ if there is $N' \in N^\circ$, $M \xrightarrow{\varphi*} N'$, otherwise $N\sigma\vec{R} \xrightarrow{\beta*} 0$. Since $M$ is $\lambda$-wider than $N$, we have $a \ge b$. We then get, setting $\sigma'' = \sigma \cdot \{\mathbf{X}_{k_{d+1}}/x_{d+1}, \dots, \mathbf{X}_{k_{d+b}}/x_{d+b}\}$:

$$ (2) \quad N\sigma\vec{R} \xrightarrow{\beta*} \mathbf{X}_{k_h'} Q_1 \dots Q_q \sigma'' [\mathbf{X}_{k_{d+b+1}}^! \dots [\mathbf{X}_{k_{d+a}}^! \underbrace{1\dots1}_{k_h-p} [H]^! \underbrace{1\dots1}_{m}]. $$

Indeed, since $a \ge b$, the variables $x_{d+b+1}, \dots, x_{d+a}$ can be considered not occurring in $Q_1, \dots, Q_q$, so that $\sigma'$ acts on $Q_1, \dots, Q_q$ exactly as $\sigma''$. Moreover, since $k > a$ and $k > q$, we have $k_{h'} \ge 2k > q + (a-b)$, so, setting $g = q + (a-b)$, we have (2) $\beta$-reduces to:

$$ (3) \quad (\lambda y_{g+1} \dots \lambda y_{k_h'} \lambda y.Q_1 \dots Q_q [\mathbf{X}_{k_{d+b+1}}^! \dots [\mathbf{X}_{k_{d+a}}^! [y_{g+1}^! \dots [y_{k_h'}^!]) \sigma' \underbrace{1\dots1}_{k_h-p} [H]^! \underbrace{1\dots1}_{m}]. $$

We consider now three cases.

**CASE I** ($h' \neq h$). This means $M$ and $N$ differ on their head-variable, in particular, for every $N' \in N^\circ$, $M \xrightarrow{\varphi*} N'$. We prove then (3) $\xrightarrow{\beta*} 0$. By the hypothesis on $k_h, k_{h'}$, we have either $k_h > k_{h'} + 2k$ or $k_{h'} > k_h + 2k$. In the first case, we get (by the hypothesis on $k$ and $N$) $k_h > k_{h'} + p + q + a + b > k_{h'} + p - g$, so that (3) $\xrightarrow{\beta*} 0$ since the head-variable $y$ will get 0 from an empty bag of the bunch of the $k_h - p$ empty bags. In the second case, we get $m \ge k_{h'} - g > k_h - p$, so that (3) $\xrightarrow{\beta*} 0$ since the head-variable $y$ will get 0 from an empty bag of the bunch of the $m$ empty bags.

**CASE II** ($h' = h$ AND $p - a \neq q - b$). This means that, for every $N' \in N^\circ$, $M \xrightarrow{\varphi*} N'$ (in fact, note that $(\cdot)^\circ$ preserve the length of the head prefix of abstractions and that of the head sequence of applications, while $\xrightarrow{\varphi}$ preserves the difference between the two). We prove then (3) $\xrightarrow{\beta*} 0$. As before, we have two subcases. If $p - a < q - b$, then $k_{h'} - g = k_h - g < k_h - p$ so (3) $\xrightarrow{\beta*} 0$, the head variable $y$ getting 0 from an empty bag of the bunch of the $k_h - p$ empty bags. Otherwise, $p - a > q - b$ implies $k_{h'} - g = k_h - g > k_h - p$ and so (3) $\xrightarrow{\beta*} 0$, the head variable $y$ getting 0 from an empty bag of the bunch of the $m$ empty bags.

**CASE III** ($h' = h$ AND $p - a = q - b$). In this case we have $k_{h'} - g = k_h - g = k_h - p$, so that (3) $\beta$-reduces to $HQ_1 \dots Q_q [\mathbf{X}_{k_{d+b+1}}^! \dots [\mathbf{X}_{k_{d+a}}^! \underbrace{1\dots1}_{k_h-p} \underbrace{1\dots1}_{m} \sigma']$. Notice that, by the definition of the substitution $\sigma'$, we can rewrite this term as

$$ (4) \quad HQ_1 \dots Q_q [x_{k_{d+b+1}}^! \dots [x_{k_{d+a}}^! \underbrace{1\dots1}_{k_h-p} \underbrace{1\dots1}_{m} \sigma'.] $$

Since $N$ can be in $\Lambda^r - \Lambda^r_\mathfrak{f}$, the bags $Q_i$'s may contain reusable resources. Hence, for every $i \le q$, let us explicit $Q_i = [N_{i,1}, \dots, N_{i,\ell_i}, (N_{i,\ell_i+1} + \dots + N_{i,n_i})^! ]$, where $n_i \ge \ell_i \ge 0$. We split into three subcases. Notice that $p \ge q$, indeed $a \ge b$ (as $M$ is $\lambda$-wider than $N$) and we are considering the case $p - a = q - b$. Also, recall that $m_i$ is the number of resources in $P_i$.
SUBCASE III.A ($\exists i \le q, m_i < \ell_i$). In this case, for every $N' \in N^\circ$, we have $M \xrightarrow{\varphi_i^*} N'$. In fact, any $N' \in N^\circ$ is of the form $\lambda x_{d+1} \dots \lambda x_{d+b} \cdot x_{h'} Q'_1 \dots Q'_q$, with $Q'_j \in Q_j^\circ$ for every $j \le q$. In particular, $Q'_i$ has at least $\ell_i > m_i$ linear resources, hence $P_i \xrightarrow{\varphi_i^*} Q'_i$, and hence $M \xrightarrow{\varphi_i^*} N'$.

We have $(4) \xrightarrow{\beta^*} 0$. Indeed, applying the $\beta$-reduction to (4) will eventually match the abstraction $\lambda z_i$ in $H$ with the bag $Q_i$. The variable $z_i$ has $m_i$ linear occurrences in $H$ and no reusable ones. This means there will be not enough occurrences of $z_i$ to accommodate all the $\ell_i$ linear resources of $Q_i$, so giving $(4) \xrightarrow{\beta^*} 0$.

SUBCASE III.B ($\exists i \le q, m_i \ne \ell_i$ AND $n_i = \ell_i$). This case means that $Q_i$ has no reusable resources and a number of linear resources different from $P_i$. Hence $M \xrightarrow{\varphi_i^*} N'$, for every $N' \in N^\circ$. Also, $(4) \xrightarrow{\beta^*} 0$ since the number of linear resources in $Q_i$ does not match the number of linear occurrences of the variable $z_i$ in $H$.

SUBCASE III.C ($\forall i \le q, m_i \ge \ell_i$, AND $m_i > \ell_i$ ENTAILS $n_i > \ell_i$). The hypothesis of the case says that $\ell_i < m_i$ entails that $Q_i$ has some reusable resources. Let $\mathcal{F}_i$ be the set of maps $s: \{1, \dots, m_i\} \to \{1, \dots, \ell_i, \ell_i+1, \dots, n_i\}$ such that

$\ell_i$-injectivity: for every $j, h \le m_i$, if $s(j) = s(h) \le \ell_i$, then $j = h$,

$\ell_i$-surjectivity: for every $h \le \ell_i$, there is $j \le m_i$, $s(j) = h$.

Intuitively, $\mathcal{F}_i$ describes the possible ways of replacing the $m_i$ occurrences of the variable $z_i$ in $H$ by the $n_i$ resources in $Q_i$: the two conditions say that each of the $\ell_i$ linear resources of $Q_i$ must replace exactly one occurrence of $z_i$. Notice that, being under the hypothesis that $p-a=q-b$, we have $p-q=a-b$, hence (4) $\beta$-reduces to the following sum

$$ (5) \quad \sum_{\substack{s_1 \in \mathcal{F}_1 \\ \vdots \\ s_q \in \mathcal{F}_q}} \mathbf{I}[N_{1,s_1(1)} \vec{R}_{1,1}]...[N_{1,s_1(m_1)} \vec{R}_{1,m_1}]...[N_{q,s_q(1)} \vec{R}_{q,1}]...[N_{q,s_q(m_q)} \vec{R}_{q,m_q}] \\ [x_{d+b+1} \vec{R}_{q+1,1}]...[x_{d+b+1} \vec{R}_{q+1,m_1}]...[x_{d+a} \vec{R}_{p,1}]...[x_{d+a} \vec{R}_{p,m_p}]\sigma' $$

Notice that for every $i \le q$, $s_i \in \mathcal{F}_i$, $j \le m_i$ the term $M_{i,j}$ is $\lambda$-wider than $N_{i,s_i(j)}$ and $\text{FV}(N_{i,s_i(j)}) \subseteq \Gamma \cup \{x_{d+1}, \dots, x_{d+a}\}$, so by the induction hypothesis

$$ (6) \quad N_{i,s_i(j)} \sigma' \vec{R}_{i,j} \xrightarrow{\beta_*} \begin{cases} \mathbf{I} & \text{if } \exists N' \in N_{i,s_i(j)}^\circ, M_{i,j} \xrightarrow{\varphi_*} N', \\ 0 & \text{otherwise.} \end{cases} $$

Also, for every $i, 1 \le i \le p-q=a-b$, $j \le m_{q+i}$, we have that $M_{q+i,j}$ is $\lambda$-wider than $x_{d+b+i} \in \Gamma \cup \{x_{d+1}, \dots, x_{d+a}\}$, so by induction hypothesis

$$ (7) \quad x_{d+b+i} \sigma' \vec{R}_{q+i,j} \xrightarrow{\beta_*} \begin{cases} \mathbf{I} & \text{if } M_{i,j} \xrightarrow{\varphi_*} x_{d+b+i}, \\ 0 & \text{otherwise.} \end{cases} $$

From (6) and (7) we deduce that $(5) \xrightarrow{\beta_*} \mathbf{I}$ if, and only if,
(i) for all $i \le q$, there exists $s_i \in \mathcal{F}_i$ such that, for all $j \le m_i$, $\exists N' \in N_{i,s_i(j)}^\circ$ satisfying $M_{i,j} \xrightarrow{\varphi_i^*} N'$, and

(ii) for all $i < p - q = a - b$ and for all $j \le m_{q+i}$, we have $M_{q+i,j} \xrightarrow{\varphi_i^*} x_{d+b+i}$.

Thanks to the conditions on the function $s_i$, item (i) is equivalent to say that for all $i \le q$, $\exists Q'_i \in Q_i^\circ$, $P_i \xrightarrow{\varphi_i^*} Q'_i$, while item (ii) is equivalent to say that for all $i < p - q = a - b$, $P_{q+i} \xrightarrow{\varphi_i^*} [x_{d+b+i}^{m_{q+i}}]$. This means that (5) $\xrightarrow{\beta^*} \mathbf{I}$ if, and only if,

$$ M = \lambda x_{d+1} \dots \lambda x_{d+a} \cdot x_h P_1 \dots P_p \\ \xrightarrow{\varphi_i^*} \lambda x_{d+1} \dots \lambda x_{d+b} \lambda x_{d+b+1} \dots \lambda x_{d+a} \cdot x_h Q'_1 \dots Q'_q [x_{d+b+1}^{m_{q+1}}] \dots [x_{d+a}^{m_p}] \\ \xrightarrow{\varphi_i^*} \lambda x_{d+1} \dots \lambda x_{d+b} \cdot x_h Q'_1 \dots Q'_q $$

where the last term is in $N^\circ$. To sum up, $N\sigma\bar{R}\beta$-reduces to $\mathbf{I}$ if $\exists N' \in N^\circ$ such that $M \xrightarrow{\varphi_i^*} N'$ and to 0, otherwise. We conclude that condition (1) holds. □

# 4 A Resource Conscious Böhm's Theorem

In this section we will prove the main result of our paper, namely Böhm's theorem for the resource calculus. We first need the following technical lemma.

**Lemma 8.** Let $M, N \in 2\langle\Lambda^r\rangle$. If $M \not\leq_{\tau} N$ then $M' \not\leq_{\tau} N$ for all $M' \xrightarrow{\eta^*} M$.

*Proof.* Suppose, by the way of contradiction, that there is an $M' \xrightarrow{\eta^*} M$ such that $M' \not\leq_{\tau} N$. Then, there are $M'' \xrightarrow{\eta^*} M'$ and $N' \xrightarrow{\eta^*} N$, such that $M'' \sqsubseteq_{\tau} N'$. By transitivity of $\xrightarrow{\eta^*}$, $M'' \xrightarrow{\eta^*} M$ holds, so we get $M \not\leq_{\tau} N$ which is impossible. □

We are now able to prove the main result of this paper.

**Theorem 2 (Resource Böhm's Theorem).** Let $M, N \in 2\langle\Lambda^r\rangle$ be closed sums in $\beta$-nf. If $M \not\equiv_{\eta\tau} N$ then there is a sequence $\vec{P}$ of closed bags such that either $M\vec{P} \xrightarrow{\beta^*} \mathbf{I}$ and $N\vec{P} \xrightarrow{\beta^*} 0$, or vice versa.

*Proof.* Let $M \not\equiv_{\eta\tau} N$, then $M \not\leq_{\tau} N$ or vice versa (Lemma 4): say $M \not\leq_{\tau} N$. Applying Lemma 8 we have $M' \not\leq_{\tau} N$ for all $M' \xleftarrow{\eta^*} M$; in particular, by Lemma 6, $M' \not\leq_{\tau} N$ holds for an $M' \lambda$-wider than both $M$ and $N$. By Lemma 5 there is $M' \in (M')^\circ$ such that for all $N \in N^\circ$ we have $M' \xrightarrow{\varphi_i^*} N$; such a term $M'$ is in $\beta$-nf since $M'$ is in $\beta$-nf and is $\lambda$-wider than both $M$ and $N$ by Remark 2.

From Lemma 7, recalling that $M', M, N$ are closed, there is a sequence $\vec{P}$ of closed bags such that: (i) $N\vec{P} \xrightarrow{\beta^*} 0$, since for all $N \in N^\circ$ we have $M' \xrightarrow{\varphi_i^*} N$, and (ii) $M\vec{P} \xrightarrow{\beta^*} \mathbf{I}$, since $M' \xrightarrow{\eta^*} M$ and hence by Remark 1 there is an $M \in M^\circ$ such that $M' \xrightarrow{\varphi_i^*} M$. This concludes the proof of our main result. □

**Corollary 1.** Let $\sim$ be a congruence on $2\langle\Lambda^e\rangle$ extending $\beta$-equivalence. If there are two closed $M, N \in 2\langle\Lambda^r\rangle$ in $\beta$-nf such that $M \not\equiv_{\eta\tau} N$ but $M \sim N$, then $\sim$ is trivial, i.e. for all sums $L \in 2\langle\Lambda^r\rangle$, $L \sim 0$.
*Proof.* Suppose $M \not\models_{\eta\tau} N$ but $M \sim N$. From **Theorem 2** there is $\vec{P}$ such that $M\vec{P} \xrightarrow{\beta*} I$ and $N\vec{P} \xrightarrow{\beta*} 0$, or vice versa. By the congruence of $\sim$, we have $M\vec{P} \sim N\vec{P}$. By the hypothesis that $\sim$ extends $\beta$-equivalence, we get $I \sim 0$. Now, take any term $L \in 2\langle A^r \rangle$, we have $L \equiv_{\beta} IL \sim 0L = 0$. $\square$

**Acknowledgements.** We thank Stefano Guerrini and Henk Barendregt for stimulating discussions and remarks.

**References**

1. Böhm, C.: Alcune proprietà delle forme $\beta$-$\eta$-normali nel $\lambda$-$K$-calcolo. Pubbl. INAC **696** (1968)

2. Barendregt, H.: The lambda-calculus, its syntax and semantics. Second edn. Number 103 in Stud. Logic Found. Math. North-Holland (1984)

3. Böhm, C., Dezani-Ciancaglini, M., Peretti, P., Ronchi Della Rocca, S.: A discrimination algorithm inside $\lambda\beta$-calculus. Theor. Comp. Sci **8**(3) (1979) 271–291

4. Hyland, J.M.E.: A syntactic characterization of the equality in some models of the lambda calculus. J. London Math. Soc. **2**(12) (1976) 361–370

5. Girard, J.Y.: Linear logic. Th. Comp. Sc. **50** (1987) 1–102

6. Carraro, A., Ehrhard, T., Salibra, A.: Exponentials with infinite multiplicities. In: Computer Science Logic. Volume 6247 of LNCS., Springer (2010) 170–184

7. Pagani, M., Ronchi Della Rocca, S.: Linearity, non-determinism and solvability. Fundamenta Informaticae **103**(1-4) (2010) 173–202

8. Boudol, G.: The lambda-calculus with multiplicities. INRIA Report 2025 (1993)

9. Boudol, G., Laneve, C.: The discriminating power of multiplicities in the lambda-calculus. Inf. Comput. **126**(1) (1996) 83–102

10. Boudol, G., Curien, P.L., Lavatelli, C.: A semantics for lambda calculi with resources. MSCS **9**(4) (1999) 437–482

11. Ehrhard, T., Regnier, L.: The differential lambda-calculus. Theor. Comput. Sci. **309**(1) (2003) 1–41

12. Tranquilli, P.: Intuitionistic differential nets and lambda-calculus. Theor. Comput. Sci., to appear (2008)

13. Bucciarelli, A., Carraro, A., Ehrhard, T., Manzonetto, G.: Full abstraction for resource calculus with tests. Submitted. http://www.dsi.unive.it/~gmanzone/papers/bcem11.pdf

14. Ehrhard, T., Regnier, L.: Uniformity and the Taylor expansion of ordinary lambda-terms. Theor. Comput. Sci. **403**(2-3) (2008) 347–372

15. Pagani, M., Tranquilli, P.: Parallel reduction in resource lambda-calculus. In: APLAS. Volume 5904 of LNCS. (2009) 226–242

16. Manzonetto, G.: What is a categorical model of the differential and the resource $\lambda$-calculi? Submitted. http://www.dsi.unive.it/~gmanzone/papers/man10.pdf.

17. Terese: Term Rewriting Systems. Volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press (2003)