# Approximation theory for distant Bang calculus

Kostia Chardonnet, Jules Chouquet, Axel Kerinec

► To cite this version:

Kostia Chardonnet, Jules Chouquet, Axel Kerinec. Approximation theory for distant Bang calculus.
2026. hal-05518907

HAL Id: hal-05518907

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

Preprint submitted on 19 Feb 2026

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 CC BY 4.0 - Attribution - International License
# Approximation theory for distant Bang calculus

Kostia Chardonnet

Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France
https://kostiachardonnet.github.io/

Jules Chouquet

Université d'Orléans, INSA CVL, LIFO, UR 4022, Orléans, France
https://www.univ-orleans.fr/lifo/membres/chouquet/

Axel Kerinec

Université Paris Est Creteil, LACL, F-94010 Créteil, France https://axelkrnc.github.io/

## Abstract

Approximation semantics capture the observable behaviour of λ-terms; Böhm Trees and Taylor Expansion are its two central paradigms, related by the Commutation Theorem. While well understood in Call-by-Name (CbN), these notions were only recently developed for Call-by-Value (CbV), motivating the search for a unified approximation framework. The Bang-calculus provides such a framework, subsuming both CbN and CbV through linear-logic translations while providing robust rewriting properties. We develop the approximation semantics of dBang—the Bang-calculus with explicit substitutions and distant reductions—by defining Böhm trees and Taylor expansion and establishing their fundamental properties. Via translations, our results recover the CbN and CbV cases within a single unifying framework capturing infinitary and resource-sensitive semantics.

2012 ACM Subject Classification Theory of computation → Linear logic; Theory of computation → Lambda calculus; Theory of computation → Operational semantics

Keywords and phrases Lambda-calculus, Böhm Trees, Taylor expansion of lambda-terms

Funding This work is supported by the Plan France 2030 through the PEPR integrated project EPiQ ANR-22-PETQ-0007 and the HQI platform ANR-22-PNCQ-0002; and by the European project MSCA Staff Exchanges Qcomical HORIZON-MSCA-2023-SE-01. The project is also supported by the Maison du Quantique MaQuEst.

## 1 Introduction

A central approach to λ-calculus semantics is the program approximation theory, which captures program behaviour, finitarily or infinitarily, offering a characterization of “meaningful” terms.

In Call-by-Name (CbN), meaningful terms are the *solvable* ones, i.e. those reducing to the identity under some “testing context”. In Call-by-Value (CbV), meaningfulness is given by *scrutability*<fnref n="1" />, which only requires reduction to a value and is strictly finer. Among approximation techniques, Böhm Trees and Taylor Expansions are the most influential. Introduced by Barendregt [14], Böhm Trees associate to each λ-term a (possibly infinite) tree whose nodes describe successive approximations of the term’s *head normal form* or ⊥ when none exists, thus capturing its asymptotic CbN behaviour. Böhm trees were related to the notion of *solvability* of CbN terms by the fact that a term is solvable if and only if its Böhm tree is not ⊥.

Ehrhard and Regnier later introduced Taylor expansion [25], inspired by the differential λ-calculus [24] and relational semantics [31]. Taylor expansions unfold a λ-term into an (infinite) formal sum of resource terms underlying the linear-use of resources during computations, rather than progressively revealing their shape as Böhm Trees do.

The Commutation Theorem [25, Corollary 35] states that normalizing the Taylor expansion of a term yields exactly the Taylor expansion of its Böhm tree. Taylor expansions can then be

<footnote n="1">¹ Also called potential valuablility</footnote>
understood as a resource-sensitive version of Böhm trees. Originally proved for the CbN λ-calculus, this result provides a deep bridge between infinitary semantics and differential/resource semantics.

While Taylor expansions for the CbV calculus were already studied in [18, 21], the development of CbV Böhm Trees remained open until Kerinec's PhD work [29, 28]. Those Böhm trees have the same commutation theorem with Taylor expansion than in the CbN case. They also respect the same relation with scrutability than as CbN Böhm trees do to solvability. This emphasizes that scrutability is the appropriate notion of meaningfulness in CbV. However, this result is obtained in an alternative version of the original Plotkin CbV, which is known to have issues due to the β<sub>v</sub>-reduction being "too weak". Concretely, unlike in CbN, CbV reduction may get stuck: redexes can be blocked since their argument is in normal form but not a value. This phenomenon prevents a straightforward infinitary unfolding analogous to the CbN case.

The aforementioned CbV Böhm trees are defined in the $\lambda_v^\sigma$-calculus from [17], where the $\beta_v$-reduction is extended with permutation rules, the so-called $\sigma$-rules, originating from the translation of $\lambda$-terms to proof-nets [1]. Another way to solve the CbV issue, also coming from proof-nets, is using a distance-based CbV calculus *distant CbV (dCbV)*<fnref n="2" /> [3, 2, 4]. In this system, substitutions may be frozen thanks to *explicit substitutions*, written $M[N/x]$, which does *not* correspond to an (effective) substitution, but instead represents a substitution that is yet to be evaluated. The rewriting rules then act *at a distance* with respect to the explicit substitutions.

The divergence between CbN and CbV has historically required separate developments of most semantic notions. Such a duplication naturally called for a unifying perspective. *Call-by-Push-Value (CbPV)* [32] provides precisely this, reconciling typed call-by-name and call-by-value within a single calculus structured around a clear distinction between values and computations. CbPV later gave rise to its untyped analogue *Bang-calculus* (Bang) [23], by use of Linear Logic [22]. Both CbN and CbV arise within the *Bang-calculus* via Girard's translations of the intuitionistic arrow into linear logic [27], making it a natural setting in which to seek a uniform approximation theory. The *Bang-calculus* is then an extension of the $\lambda$-calculus with two new constructs: $!M$ (pronounced “bang $M$”) which *freezes* the computation of $M$, and *der*($M$) which unfreezes it. Both CbN and CbV can then be translated into the *Bang-calculus*, which simulates their rewriting strategies within a single rewriting system.

However, the *Bang-calculus* exhibits the same issue as CbV: ill-formed redexes may block evaluation. One might expect that adapting the $\sigma$-rules to the *Bang-calculus* would solve this issue; however, while the CbV calculus with $\sigma$-rules is confluent, this is not the case for the *Bang* calculus [23, Sec.2.3]. Confluence can be recovered modulo an equivalence relation contained in the $\sigma$-equivalence generated by the $\sigma$-rules, but this forces us to work modulo said equivalence. Another solution to this problem is to consider the distance variant (dBang) [16], similar to the distant variant of CbV. This allows us to work without the $\sigma$-rules and the aforementioned equivalences. This new system has been shown to be confluent [16]. It has also been used in unifying multiple results for dCbN and dCbV. For instance, in [9] the authors show that the rewriting results (confluence, factorization) of dBang carries over to the dCbN and dCbV setting using the translations into dBang<fnref n="3" />. Similarly, the notion of solvability in both dCbN and dCbV has been captured through the notion of meaningfulness in dBang [30, 11]. However, despite significant progress, the approximation theory of the dBang-calculus remains largely underdeveloped.

<footnote n="2">² Also called Value Substitution Calculus</footnote>

<footnote n="3">³ Note that while the translation of dCbN into dBang is the usual one mentioned before, the authors use a new translations for CbV which will be discussed in Section 3</footnote>
A recent work by Mazza & Dufour tried to close that gap [20]: they developed a generic notion of Böhm tree and Taylor expansion for a language called Proc, representing untyped proof structures. They showed how any language that can be embedded into Proc in a "nice way" inherits the notions of Böhm Trees and Taylor expansion from Proc, and their commutation Theorem. In particular, dBang admit such an embedding. However, no notion of meaningfulness exists in Proc and it is not clear how to relate the results from CbN and CbV with the notion developed in [20].

## 1.1 Contributions

We develop a theory of approximation of the distance Bang-calculus (dBang). To this end we recall the definitions and main results of dBang from [30, 10, 16] in Section 2. We start by developing the Taylor expansion of dBang (Section 2.2) where we introduce the resource calculus (Section 2.2.1) and define the approximation relation (Section 2.2.2) and establish a simulation result between dBang and its approximants in the Taylor expansion (Theorem 20). We next develop the Böhm approximants of dBang (Section 2.3) and prove a commutation theorem between the Taylor Expansion of Böhm Trees and the Taylor normal form (Theorem 45).

Finally, we establish the soundness of our definition with regard to the standard notion of Böhm Trees and Taylor Expansions in the CbN and CbV λ-calculus by translating these systems into dBang (Section 3), in particular, we show that the Böhm Trees of a term M in CbN (respectively CbV) are the same as its translation into dBang (Theorem 56). We show a similar result for Taylor expansion (Lemmas 51 and Corollaries 52).

Proofs are available in the Appendix.

## 1.2 Notations

For any reduction relation $\rightarrow$ we define, we use the standard notations: $\rightarrow^*$, $\rightarrow^k$ for, respectively, its reflexive transitive closure and its k-step iteration. We write $[m_1, ..., m_k]$ for a finite multiset containing k occurrences of terms. When necessary, we use a subscript as $[m]_k$ or $[m, ..., m]_k$ in order to make explicit the number of elements.

# 2 The (distance) Bang-calculus

We begin by recalling the theory of dBang, first with some results from previous studies [30, 10, 16], before developing its approximation theory via Taylor expansion and Böhm trees.

► **Definition 1.** (dBang: terms and contexts)

(Terms) $M, N := x | MN | \lambda x M | !M | \mathbf{der}(M) | M[N/x]$

(List contexts) $L := \square | L[M/x]$

(Surface contexts) $S := \square | SM | MS | \lambda x S | \mathbf{der}(S) | S[M/x] | M[S/x]$

(Full contexts) $F := \square | FM | MF | \lambda x F | \mathbf{der}(F) | F[M/x] | M[F/x] | !F$

Terms include the standard λ-calculus constructs: variable (ranging over a countably infinite set), application and abstraction. Two additional ones are used to define the Bang-calculus: the bang (or exponential) !M, representing delayed evaluation of the subterm M, and dereliction der(M), which reactivates it. Finally, explicit substitutions $M[N/x]$ comes from the "at distance" mecanism, and represents pending substitutions. The lambda-abstraction (as usual) and the explicit substitution bind the variable x in M. We use contexts, i.e. terms with a subterm hole (□) and we denote by $C\langle M \rangle$ the term obtained by filling the hole in C by M. We distinguish list, surface and full contexts. List contexts are sequences of explicit substitutions and will be used for the reduction at a
distance. Surface and full contexts determine whether reduction under a ! is allowed (in particular it is forbidden in weak calculi (CbN or CbV)).

The dBang calculus has three reduction rules:

$$L\langle\lambda xM\rangle N \mapsto_! L\langle M[N/x]\rangle \qquad M[L\langle!N\rangle/x] \mapsto_! L\langle M\{N/x\}\} \qquad \mathrm{der}(L\langle!M\rangle) \mapsto_! L\langle M\rangle$$

Notice that requiring subterms of the form !M assigns them *value* status in the CbV sense.

We write $\rightarrow_!$ and $\rightarrow_+$ for the coluseres under surface and full contexts, respectively; both are confluent [30, Theorem 1]. We also denote by $\rightarrow_i$ the internal reductions (i.e. $\rightarrow_i = \rightarrow_! \setminus \rightarrow_!$), these are the reductions occurring under a $!$-construct).

**Example 2.** $(\lambda xxy)[!z/y]!!((\lambda ww)!N) \rightarrow_! (xy)[!!((\lambda ww)!N)/x][!z/y] \rightarrow_! ((\lambda ww)!N)y[!z/y] \rightarrow_! ((\lambda ww)!N)z \rightarrow_! !!Nz$. The last step requires a full reduction.

**Example 3.**

- $\Delta = \lambda x(x!x), \Omega = \Delta!\Delta$. We have $\Omega \rightarrow_!^2 \Omega$.

- $Y_x^n = (\lambda yx!(y!y))!(\lambda yx!(y!y))$. We have $Y_x^n \rightarrow_!^+ x!Y_x^n$

- $Y_x^v = (\lambda yx(y!y))!(\lambda yx(y!y))$. We have $Y_x^v \rightarrow_!^+ xY_x^v$

The upper scripts in the two last items, as we shall see further, represent the fact that $Y_x^n$ and $Y_x^v$ correspond respectively to the CbN and CbV translations from a fixpoint combinator $Y$ of standard $\lambda$-calculus<fnref n="4" />.

## 2.1 Meaningfulness in dBang

This section focus on *meaningfulness*, later related to approximation theory in Section 4: intuitively, a term is meaningful if it reduces to a desired result under some *testing context*. It generalizes the notions of *solvability* CbN and *scrutability* CbV, and has been studied in detail for dBang in [30].

**Definition 4.** A term $M$ of dBang is said meaningful if there exists a testing context $T := \Box | TM | (\lambda xT)M$ and a term $P$ such that $T\langle M\rangle \rightarrow_!^* P$.

Notice that the surface reduction involved in meaningfulness is not restrictive: for any $N$, $N \rightarrow_!^* P$, then there is some $P'$ such that $N \rightarrow_!^* P'$ (this follows from a standardisation property, see Corollary 6 below). It has been shown in [30] that the smallest theory that identifies all meaningless terms is consistent; that meaningful terms and surface-normalizing terms can be characterized by an intersection type systems and finally that meaningless subterms do not affect the operational meaning of a given term [30, Proposition 8, Theorem 24 and Corollary 11].

A natural property of surface reduction is that it determines the external shape of a term. In other words, allowing full reduction does not unlock external redexes. This is expressed as the following factorization proposition:

**Proposition 5.** ([10, Corollary 21]) Let $M \rightarrow_!^* N$. There is some $P$ such that $M \rightarrow_!^* P \rightarrow_i^* N$.

Conversely, internal reductions preserve the *external shape*. We express this notion with multi-holes surface contexts, that let us reformulate the factorization property as follows:

<footnote n="4">⁴ Note that $Y_x^v$ lacks some good properties if one would want to use it for computations in CbV, and CbV fixpoints are usually defined differently. We nevertheless keep $Y_x^v$ as a running example, so as to illustrate an infinite computation, with a fixpoint behaviour, but with empty semantics.</footnote>
**Corollary 6 (Standardization).** Let $S^+$ denote multi-holes surface contexts and given by the syntax: $S^+ := \square | M | S^+S^+ | S^+[S^+/x] | \mathbf{der}(S^+) | \lambda x S^+$. For any reduction $M \to_i^* P$, there are some terms $N_i$ and a multi-hole surface context $S$ such that $P = S\langle!N_1, \dots, !N_k\rangle$ and $M \to_{i_s}^* S\langle!N'_1, \dots, !N'_k\rangle \to_i^* S\langle!N_1, \dots, !N_k\rangle$

If $k=0$, the context has no hole and the reduction occurs only at surface level.

## 2.2 Taylor expansion

We define the Taylor expansion of dBang, starting with the associated resource calculus $\delta$Bang. This calculus will also serve as the resource language for CbN and CbV in Section 3. There is no necessity to define specific resource calculi, as $\delta$Bang fits well as a target of usual Taylor expansion (Call-By-Name [26] and Call-By-Value [21]), with a straightforward adaptation to distant setting.

### 2.2.1 dBang: resources

**Definition 7 (Resource calculus $\delta$Bang).**

(terms) $m, n := x | mn | \lambda x m | \mathbf{der}(m) | m[n/x] | [m_1, \dots, m_k]$

(lists) $l := \square | l[m/x]$

(surface) $s := \square | sm | ms | \lambda xs | \mathbf{der}(s) | s[m/x] | m[s/x]$

(full) $f := \square | sm | mf | \lambda xf | \mathbf{der}(f) | f[m/x] | m[f/x] | [f, m_1, \dots, m_k]$

(tests) $t := \square | tm | (\lambda xt)m$

Terms $[m_1, \dots, m_k]$ for $k \in \mathbb{N}$, called bags denote finite multisets of resource terms, with $[]$ the empty bag. Contexts are exactly as in dBang (Definition 1), with bags replacing exponentials. We write $P_k$ for the sets of permutations of the set $\{1, \dots, k\}$, and we denote as $d_x(m)$ the number of free occurrences of the variable $x$ in $m$. Resource substitution is (multi-)linear: when we write $m\{n_1/x_1, \dots, n_k/x_k\}$, it is always intended (in the resource setting) that $x_i$ represents the $i$-th free occurrence of $x$ in $m$. In that way, each term $n_i$ is substituted exactly once in $m$.

We are now ready to define the reduction relation.

**Definition 8.**

The reduction relation $\Rightarrow_{\delta} \subseteq \delta$Bang $\times \wp(\delta$Bang) is then defined as follows:

- $l\langle\lambda x m\rangle n \Rightarrow_{\delta} \{l\langle m[n/x]\rangle\}$

- $m[l\langle[n_1, \dots, n_k]\rangle/x] \Rightarrow_{\delta} \left\{ \bigcup_{\sigma \in P_k} l\langle m\{n_{\sigma(1)}/x_1, \dots, n_{\sigma(k)}/x_k\}\rangle \quad \text{if } k = d_x(m) \\ \emptyset \quad \text{otherwise} \right.$

- $\mathbf{der}(l\langle[m_1, \dots, m_k]\rangle) \Rightarrow_{\delta} \{l\langle m_1\rangle\} \quad \text{if } k = 1 \text{ and } \emptyset \text{ otherwise}$

We write $m \to_{\delta} n$ as soon as $m \Rightarrow_{\delta} X$ and $n \in X$ for some $n$ (if $m \Rightarrow_{\delta} \emptyset$, we also abusively write $m \to_{\delta} \emptyset$, and we add the following equation: if $f\langle\emptyset\rangle = \emptyset$ for any full context $f$). We also define $\to_{\delta s}$ and $\to_{\delta}$ the contextual closures of $\to_{\delta}$ under surface and full contexts, respectively. Notice that none of these reductions is deterministic. Both $\to_{\delta s}$ and $\to_{\delta}$ are strongly normalizing, which is an immediate consequence of linearity: the size of bags of resource terms is decreasing. Confluence of $\to_{\delta s}$ and $\to_{\delta}$ follows from standard resource-calculus arguments and from the proofs for $\to_{i,s}$ and $\to_i$.

### 2.2.2 Approximation

In Figure 1, defines the relation $\triangleleft_i \subseteq \delta$Bang $\times$ dBang, where $m \triangleleft_i M$ means that $m$ is a multilinear resource approximation on $M$.
$$ \frac{m \triangleleft M}{x \triangleleft x} \qquad \frac{m \triangleleft M}{\lambda x m \triangleleft \lambda x M} \qquad \frac{m \triangleleft M}{\mathrm{der}(m) \triangleleft \mathrm{der}(M)} \qquad \frac{m \triangleleft M \quad n \triangleleft N}{mn \triangleleft MN} \\ \frac{m \triangleleft M \quad n \triangleleft N}{m[n/x] \triangleleft M[N/x]} \qquad \frac{m_1 \triangleleft M \quad \dots \quad m_k \triangleleft M}{[m_1, \dots, m_k] \triangleleft !M} \quad k \in \mathbb{N} $$

<caption>Figure 1 Resource approximation for dBang</caption>

We extend this definition to list contexts as follows: □ $\triangleleft$ □, $l[m/x] \triangleleft L[M/x]$ if $l \triangleleft L$ and $m \triangleleft M$. The extension to surface and full contexts follows analogously.

The expected behaviour of context approximation is given by the following lemma (proved by induction on contexts):

► Lemma 9.

- If $m \triangleleft L \langle N \rangle$, then there exist $l \triangleleft L$ and $n \triangleleft N$ such that $m = l \langle n \rangle$.

- If $m \triangleleft S \langle N \rangle$, then there exist $s \triangleleft S$ and $n \triangleleft N$ such that $m = s \langle n \rangle$.

Notice that this property fails for full contexts; consequently, our definitions do not provide a convenient notion of approximation between them. This is due to a need for parallel treatment of bags, which - as we shall see later - is incompatible with single-hole contexts.

► **Definition 10.** (Taylor expansion) For any $M \in \text{dBang}$, we define its Taylor expansion as the set of its resource approximants:

$$ \mathcal{T}(M) = \{m \in \delta\text{Bang} \mid m \triangleleft! M\} $$

By strong normalization of $\delta\text{Bang}$, we can define the normal form $\mathbf{nf}(m)$ of a resource term $m$ as the finite set made of its full reducts. We then define the *Taylor normal form* of dBang terms as $\text{TNF}(M) = \bigcup_{m \triangleleft! M} \mathbf{nf}(m)$. Notice that Taylor normal form is made of full normal terms, not only surface normal forms.

► **Example 11.** Consider the terms given in Example 3.

- An approximant of $m \triangleleft! \Omega$ must be of shape $(\lambda xx[x]_k)[\lambda xx[x]_{k_1}, \dots, \lambda xx[x]_{k_i}]$. Now, if $k = l-1$ (otherwise $m \mapsto! \emptyset$) then $m \to_{\delta s} (\lambda xx[x]_{k_1})[\lambda xx[x]_{k_2}, \dots, \lambda xx[x]_{k_i}]^5$, which is again an approximant of $\Omega$. But we can observe that the cardinality of the bag reduces during this reduction; hence if we iterate this reduction, we eventually reach a term like $(\lambda x[x]_k)[\to_{\delta s} \emptyset]$ (if an empty reduction has not occurred before). So, $\text{TNF}(\Omega) = \emptyset$.

- Similarly, if $m \triangleleft! Y_x^n$, we verify easily that $m \to_{\delta s} x[n_1, \dots, n_k]$, with $n_i \triangleleft! Y_x^n$. In particular, $x[\triangleleft! Y_x^n]$ and is in normal form. Actually, $\text{TNF}(Y_x^n)$ can be characterized inductively : $x[\triangleleft! Y_x^n]$, and if $n_1, \dots, n_k \in \text{TNF}(Y_x^n)$, then $x[n_1, \dots, n_k] \in \text{TNF}(Y_x^n)$, for any $k$.

- The other fixpoint term, $Y_x^v$, behaves slightly differently: if $m \triangleleft! Y_x^v$, then we verify $m \to_{\delta s}^* x n$, for some $n \triangleleft! Y_x^v$. But here, because of the argument not being in a bag, all approximants reduce (if not $\emptyset$) to some term $xxx\dots xn$, but are not in normal form; since such a reduction terminates, we observe that $\text{TNF}(Y_x^v) = \emptyset$.

<footnote n="5">⁵ We consider here one possible reduction, any element of the bag could be substituted to the inner head variable $x$, not necessarily $\lambda x[x]_{k_1}$, the argument is valid for all the reduction paths.</footnote>
► **Remark 12.** [Clashes and normal forms] Note that we have not excluded so-called clashes from our calculus, as they cause no issue in our setting. Thus, terms such der($\lambda xx$) are considered as regular normal forms. This approach is similar to the one of Dufour and Mazza [20]. However, giving an empty semantics to clashs could easily be done, for example, adding reductions such as der($\lambda x m$) → ∅ to resource calculus.

### 2.2.3 Simulation

We now formalize the simulation of dBang reduction in the approximants of $\delta$Bang, as sketched in the Example 11.

► **Lemma 13** (Substitution Lemma for Taylor expansion). For any $M, N$ of dBang, for any $m, n_1, \dots, n_{d_x(m)}$ of $\delta$Bang, we have $m\{n_1/x_1 \dots n_{d_x(m)}/x_{d_x(m)}\} \triangleleft! M\{N/x\}$ if and only if $m \triangleleft! M$, and $n_i \triangleleft! N_i$ for all $i \le d_x(m)$.

We can show, by a straightforward induction, with the help of the Substitution Lemma stated above, that the surface reduction acts exactly the same way in a dBang term and in its approximants:

► **Lemma 14.** Let $m \triangleleft! M$ and $m \to_{\delta_s} n$. Then there is $N \in \text{dBang}$ such that $M \to_{!s} N$ and $n \triangleleft! N$.

However, this result is false when considering reduction in full contexts: let $m = [(\lambda xx)y, (\lambda xx)y]$. We have $m \triangleleft! ((\lambda xx)y)$ and $m \to_{\delta} n = [x[y/x], (\lambda xx)y]$, but $n$ is not an approximant of any dBang term. We will need parallel reduction to achieve full simulation, this is done in Subsection 2.2.4.

► **Lemma 15.** *Considering the following configuration:*

$$ \begin{array}{ccc} M & \to_{!s} & N \\ \bigtriangledown & & \bigtriangledown \\ m & \to_{\delta_s} & n \end{array} $$

Given three of four terms, we can always obtain a convenient fourth that makes the square commute (for a proof, see lemmas 71, 72 and 73 in Appendix A).

► **Definition 16.** Let $X$ and $Y$ be sets, and $\mathcal{R} \subseteq X \times Y$ a relation. We write $X\overline{\mathcal{R}}Y$ whenever $\forall x \in X, \exists y \in Y$ such that $(x, y) \in \mathcal{R}$ and $\forall y \in Y, \exists x \in X$ such that $(x, y) \in \mathcal{R}$.

Then, using Lemma 15 we obtain a simulation theorem for surface reduction:

► **Theorem 17** (Simulation). Let $M, N$ in dBang such that $M \to_{!s} N$. We have $\mathcal{T}(M) \stackrel{\to_{\delta_s}}{\mathcal{T}}(N)$.

### 2.2.4 Parallel reduction and full contexts

Figure 2 defines a parallel resource reduction allowing us to handle full contexts. Intuitively, it needs to reduce at once every term occurring in a bag, in order to simulate internal reductions like $!M \to! !M'$. In particular, it needs to be reflexive because e.g. $[] \triangleleft! !M$ and $[]$ does not reduce to $\emptyset$, we have to consider that $[] \triangleleft! !M'$ is obtained from $[]$ by reduction. The resulting relation $\stackrel{\to_{\delta}}{\equiv}$, is a well-known non-deterministic extension of standard reduction which can be used to prove confluence property. In general, for a reduction $\to$, we have $\to \subsetneq \stackrel{\to}{\equiv} \subsetneq \to^*$, with $\equiv$ enjoying the diamond property. See e.g. Barendregt's proof of confluence for the $\lambda$-calculus [12], known as Tait-Martin-Löf technique. We abusively write $l \stackrel{\to_{\delta}}{\equiv} l'$ for contexts as soon as $l = \Box[m_1/x_1] \dots [m_k/x_k]$, $l' = \Box[m'_1/x_1] \dots [m'_k/x_k]$ and $m_i \stackrel{\to_{\delta}}{\equiv} m'_i$ for any $i \le k$.

Since $\stackrel{\to_{\delta}}{\equiv}$ is size-decreasing, it enjoys weak normalization, but obviously not strong, as it is reflexive. It also enjoys the (one-step) diamond property, as it can be proved by standard techniques. We can now state our simulation results for full contexts:
$$ \begin{array}{c} \overline{x \Leftrightarrow_{\delta} x} \\ \\ \frac{m_1 \Leftrightarrow_{\delta} m'_1 \quad \dots \quad m_k \Leftrightarrow_{\delta} m'_k}{[m_1, \dots, m_k] \Leftrightarrow_{\delta} [m'_1, \dots, m'_k]} k \in \mathbb{N} \\ \\ \frac{m \Leftrightarrow_{\delta} m'}{s \langle m \rangle \Leftrightarrow_{\delta} s \langle m' \rangle} * \\ \\ \frac{[m_1, \dots, m_k] \Leftrightarrow_{\delta} [m'_1, \dots, m'_k]}{n [l \langle [m_1, \dots, m_k] \rangle] \Leftrightarrow_{\delta} l' \langle n' \{m'_{\sigma(1)}/x_1, \dots, m'_{\sigma(k)}/x_k\} \rangle} ** \\ \\ \frac{m \Leftrightarrow_{\delta} m' \quad n \Leftrightarrow_{\delta} n' \quad l \Leftrightarrow_{\delta} l'}{l \langle \lambda x m \rangle n \Leftrightarrow_{\delta} l' \langle m' [n'/x] \rangle} \\ \\ \frac{m_1 \Leftrightarrow_{\delta} m'_1}{\mathrm{der}([m_1, \dots, m_k]) \Leftrightarrow_{\delta} m'_1} *** \end{array} $$

* s is any surface resource context

** $\sigma \in P_k$, and if $k = d_x(n')$ (otherwise the reduction gives $\emptyset$).

*** $k = 1$. Otherwise, the reduction gives $\emptyset$.

Figure 2 Parallel reduction for $\delta$Bang

**Lemma 18.** Let $M, N \in \text{dBang}$ with $M \to_! N$. For any $m \triangleleft_! M$, either $m \Leftrightarrow_{\delta} \emptyset$ or there is some $n \triangleleft_! N$ such that $m \Leftrightarrow_{\delta} n$

The symmetric counterpart of this result is obtained with a similar reasoning:

**Lemma 19.** Let $M, N \in \text{dBang}$ with $M \to_! N$. For any $n \triangleleft_! N$, there is some $m \triangleleft_! M$ such that $m \Leftrightarrow_{\delta} n$.

The two previous lemmas give us the desired simulation result for full reduction:

**Theorem 20.** Let $M, N \in \text{dBang}$ such that $M \to_! N$, then we have $\mathcal{T}(M) \overline{\Leftrightarrow_{\delta}} \mathcal{T}(M)$

We saw that surface reduction acts similarly in dBang and in $\delta$Bang, while parallel reduction is necessary to give a multilinear account to internal reductions (the definition of parallel reduction alone does not imply that they occur exclusively inside bags, but this is made mandatory through the use of invariant multi-hole surface contexts). The factorization properties established for dBang (Corollary 6) can easily be translated in the resource setting:

**Proposition 21 (Factorization).** Let $s^+$ denote multi-holes surface contexts and given by the syntax $s^+ := \square | m | s^+s^+ | s^+[s^+/x] | \text{der}(s^+) | \lambda x s^+$. For any reduction $m \to_{\delta}^* p$, there are some bags $\bar{n}_i$ and some multi-hole context $s$ such that $p = s\langle\bar{n}_1, \dots, \bar{n}_k\rangle$ and $m \to_{\delta s}^* s\langle\bar{n}'_1, \dots, \bar{n}'_k\rangle \Leftrightarrow_{\delta}^* s\langle\bar{n}_1, \dots, \bar{n}_k\rangle$

Following the reduction occurring on resource terms, we have defined previously Taylor normal form. We develop in this section some lemmas on those objects. They will be useful in order to prove the Commutation Theorem between Böhm trees and Taylor expansions.

**Lemma 22.** Given $M \to_!^* N$ then $\text{TNF}(M) = \text{TNF}(N)$.

**Lemma 23.** Given $m \in \text{TNF}(M)$ then there exists $M'$ such that $M \to_!^* M'$ and $m \triangleleft_! M'$.

## 2.3 Böhm trees

This section is devoted to Böhm approximants for dBang and their relation to the Taylor expansion via the Commutation Theorem (Theorem 45), which states that Taylor expansion of the Böhm tree of a term is equal to its Taylor normal form. This result is similar to the classical one in CbN [26] and a more recent one in CbV [29]).
**► Definition 24 (dBang$_{⊥}$).** Let dBang$_{⊥}$ be the set of dBang-terms extended with the symbol $⊥$. In the following we use subscripts as $⊥_i$ in order to distinguish occurrences of $⊥$ as a subterm. Similarly, we extend the different types of contexts; and we extend reductions in the obvious way.

**► Definition 25.** The set of approximants is a strict subset of dBang$_{⊥}$ generated by the grammar:

$$A := \perp | B | \lambda x A | !A | A[A_!/x] \qquad A_! := B | \lambda x A | A_![A_!/x]$$

$$B := x | A_\lambda A | \mathbf{der}(A_!) \qquad A_\lambda := B | !A | A_\lambda[A_!/x]$$

**► Lemma 26.** Approximants are the normal forms of dBang$_{⊥}$.

Substituting $⊥$ by any term preserves normal forms, as a consequence of the syntactic structure of approximants. First, approximants contain no redexes. Secondly, there are no approximants containing subterms of shape $\mathbf{der}(⊥)$, $⊥A$, $A[⊥/x]$ that could hide a potential redex. Formally:

**► Lemma 27.** Let $A$ be an approximant, $M$ any term of dBang$_{⊥}$, and $⊥_i$ some occurrence of $⊥$ in $A$. If $A[M/⊥_i] \to_! N$, then $N = A[M'/⊥_i]$ with $M \to_! M'$. i.e. we cannot create a redex when replacing a $⊥$ by a term $M$ in an approximant: the only redexes obtained this way are those already present in $M$.

**► Definition 28 (Order).** Let $\sqsubseteq \subseteq$ dBang$_{⊥}$ $\times$ dBang$_{⊥}$ be the least contextual closed preorder on dBang$_{⊥}$ generated by setting: $\forall M \in$ dBang$_{⊥}$ and for all full context $F$, $F[⊥] \subseteq F[M]$.

In other words, $M \sqsubseteq N$ if and only if $M = N\{\overrightarrow{P/⊥}\}$. In the Böhm trees literature, we sometimes find approximation orders where only terms of shape $!P$ are replaced by a $⊥$ (see e.g. Dufour and Mazza [20]). For technical reasons (Theorem 56 in particular) due to CbN and CbV embeddings into dBang, we need, for example, $\lambda x \perp \sqsubseteq \lambda x M$ to be a valid approximation.

The following lemma states that when a reduction occurs in a term, it cannot be seen by its approximations, that only represent a part of the skeleton of their normal form. In other words, when $A \sqsubseteq M$, then $A$ represents a subtree of $M$ which cannot be modified by some reduction.

**► Lemma 29.** $A \sqsubseteq M$ and $M \to_!^* N$ then $A \sqsubseteq N$.

**► Definition 30 (Set of approximants).** Given $M \in$ dBang, the set of approximants of $M$ is defined as follows: $\mathcal{A}(M) = \{A \mid M \to_!^* N, A \sqsubseteq N\}$.

Note that $\mathcal{A}(M)$ is never empty, since it contains at least $⊥$.

**► Example 31.** Consider the terms given in Example 3.

- The only reducts of $\Omega$ being $\Omega$ itself, and since the syntax $A$ of approximants contains no redex, we easily conclude that $\mathcal{A}(\Omega) = \{\perp\}$.

- The reducts of $Y_x^n$ are of shape $x!x!x...!Y_x^n$, we conclude that $\mathcal{A}(Y_x^n)$ contains precisely the terms $\perp, x\perp, x!\perp, x!x\perp, x!x!\perp, ...$

- The reducts of $Y_x^v$ follow the same observation, minus the exponentials, and $\mathcal{A}(Y_x^v)$ contains precisely $\perp, x\perp, xx\perp, xxx\perp, ...$

**► Lemma 32.** $M \to_!^* N$ then $\mathcal{A}(M) = \mathcal{A}(N)$.

**► Remark 33.** If $A = F[\vec{1}] \in \mathcal{A}(M)$ (where $F$ is a multi-hole context), then $M \to_*^* F[\vec{N}]$ for some $\vec{N}$. In particular, if $A$ contains no $⊥$ subterms, then $M$ has a normal form, which is exactly $A$.

**► Definition 34 (Ideal).** Let $X \subseteq$ dBang$_{⊥}$. We set $X$ is an ideal when $X$ is downwards closed for $\sqsubseteq$, and directed: for all $M, N \in X$ there exists some upper bound (with respect to $\sqsubseteq$) to $\{M, N\}$.
**► Lemma 35.** Let $M \in \text{dBang}$. $\mathcal{A}(M)$ is an ideal.

In order to define Böhm trees, we follow the long-established tradition for term rewriting systems, including CbN and CbV [6, 15, 13, 5, 7, 29], based on the ideal completion. This method constructs the set of ideals of approximants (ordered by a direct partial order). Böhm trees are then identified with such ideals. The finite and infinite ideals represent respectively the finite and infinite trees. For a $\lambda$-term $M$, its Böhm tree is the ideal generated by its set of approximants; equivalently, it can be seen as the supremum of these approximants in the associated directed-complete domain. This domain admits a concrete presentation as a coinductive grammar extending that of approximants, where constructors may be unfolded infinitely often. Given $M \in \text{dBang}$, $\mathcal{A}(M)$ has a supremum, noted $\cup \mathcal{A}(M)$, which is a potentially infinite tree.

**► Definition 36 (Böhm Tree).** *The Böhm tree of a term $M$ in dBang, is given by $\cup \mathcal{A}(M)$, and denoted $\text{BT}_!(M)$.*

Böhm trees satisfy the following immediate properties (we already used these facts on approximants for previous results, they lift immediately to Böhm trees).

**► Proposition 37 (Some properties of Böhm trees).**

- If $M$ is in normal form, $\text{BT}_!(M) = M$

- $\text{BT}_!(M) = \perp$ if and only if $\mathcal{A}(M) = \{\perp\}^6$, if and only if any reduct of $M$ is a redex.

- If $M \to^* N$, $\text{BT}_!(M) = \text{BT}_!(N)$, for example $\text{BT}_!(\text{der}(!M)) = \text{BT}_!(M)$.

- $\text{BT}_!(\lambda x M) = \lambda x \text{BT}_!(M)$ and $\text{BT}_!(!M) = ! (\text{BT}_!(M))$

- If $\text{BT}_!(M) \neq L\langle\lambda x - \rangle$, then $\text{BT}_!(MN) = \text{BT}_!(M)\text{BT}_!(N)$

- If $\text{BT}_!(M) \neq L\langle!-\rangle$, then $\text{BT}_!(\text{der}(M)) = \text{der}(\text{BT}_!(M))$ and $\text{BT}_!(N[M/x]) = \text{BT}_!(N)[\text{BT}_!(M)/x]$

In particular, we can infer from the facts above that if $\text{BT}_!(M)$ is an application, then it is equal to $(x)\text{BT}_!(N)$ for some $N$ (hence $M \to^* L\langle x \rangle N$).

**► Example 38.** From Example 31, we can infer that $\text{BT}_!(\Omega) = \perp$, $\text{BT}_!(Y_x^n)$ is the infinite application $x!x!x!x...$, and $\text{BT}_!(Y_x^v)$ is also an infinite application $xxxxx...$. This is the intended behaviour of Böhm trees, as in this category of terms they represent, at the limit, the amount of result produced by a computation, even if the term itself has no normal form.

## 2.4 The commutation between Böhm and Taylor approximation

Combining the previous results, we state the Commutation Theorem. We start by defining the Taylor expansion of Böhm trees.

**► Definition 39.** *We extend the Taylor expansion to dBang$_{\perp}$-terms by setting $\mathcal{T}(\perp) = \emptyset$ (recall that $f[\emptyset] = \emptyset$ for any full context $f$). In other words, there is no $\delta$Bang term $m$ such that $m \prec! \perp$.*

One immediate consequence of this definition is that, for $M$ in dBang$_{\perp}$, $\mathcal{T}(M) \neq \emptyset$ if $M$ contains no $\perp$ as a surface subterm. In other words, $M$ expands to a non-empty set if and only if the $\perp$ are under exponentials ! (in that case, these exponentials can be approximated by empty bags). Moreover, $M \subseteq N$ implies $\mathcal{T}(M) \subseteq \mathcal{T}(N)$.

<footnote n="6">⁶ This distinguishes our Böhm trees from those of Mazza and Dufour [20], in which $\text{BT}_!(M) = \perp$ as soon as $M$ has no surface normal form. Indeed, for technical reasons (relative to CbV embeddings), if $\text{BT}_!(M) = \perp$, we need to have $\text{BT}_!(\lambda x M) = \lambda x \perp$, and not $\perp$, because $\lambda x \perp$ embeds to $!(\lambda x \perp)$, while $\perp$ embeds to $\perp$, which loses the exponential and breaks commutation properties between Böhm trees and CbV embedding (Theorem 56). This distinction vanishes at the semantical level: as soon as we consider Taylor expansion of Böhm trees, the trees having no surface normal form are given an empty expansion (Definition 39).</footnote>
► **Definition 40** (Taylor expansion of Böhm trees). Given $M \in \text{dBang}$, $\mathcal{T}(\text{BT}_!(M)) = \cup_{a \in \mathcal{A}(M)} \mathcal{T}(a)$.

► **Example 41.** Following the terms of previous examples, we easily check that $\mathcal{T}(\text{BT}_!(\Omega)) = \emptyset$ (because $\mathcal{A}(\Omega) = \{\perp\}$). Recall that $\mathcal{A}(Y_x^n) = \{\perp, x\perp, x!\perp, \dots\}$. The first of these approximants having a non-empty expansion is $x!\perp$, approximated by $x[]$, $\mathcal{T}(\text{BT}_!(Y_x^n)) = \{x[], x[x[], \dots, x[\dots]\]}$. And $\mathcal{T}(\text{BT}_!(Y_x^v)) = \emptyset$. Indeed, all approximants of $Y_x^v$ are of shape $xxx...x\perp$, and have a surface $\perp$ that expands to $\emptyset$. With examples 31 and 11, we observe for these terms the identity of TNF($M$) and $\mathcal{T}(\text{BT}_!(M))$ which is proved globally in the remainder of this section.

Remark that, since $\mathcal{A}(M)$ is an ideal, $\mathcal{T}(\text{BT}_!(M))$ is a directed union. The purpose of Taylor expansion is to approach a term by finitary resource terms only, so we do not consider any infinite supremum of this union, and keep a set of terms, this approximation being inductive; while Böhm trees are coinductive and consist of infinite objects.

► **Lemma 42.** Let $A \subseteq M$, then $\mathcal{T}(A) \subseteq \mathcal{T}(M)$.

► **Lemma 43.** Let $A \in \mathcal{A}(M)$, then $\mathcal{T}(A) \subseteq \text{TNF}(M)$.

► **Lemma 44.** Let $m \triangleleft! M$ in normal form, then there exists an approximant $A$ such that $A \subseteq M$ and $m \triangleleft! A$ (remember that $m \triangleleft! M$ and $m \in \mathcal{T}(M)$ are the same thing).

From the previous lemmas we deduce the Commutation Theorem:

► **Theorem 45.** Let $M \in \text{dBang}$. $\mathcal{T}(\text{BT}_!(M)) = \text{TNF}(M)$.

## 3 Translations

This section is about the approximation theory of dCBN and dCBV, in particular about how the embeddings into dBang can profit from the result of previous Section. We briefly recall the relevant definitions and results of those embeddings, that have been already well studied [16, 30, 8, 9, 10, 11] dCBV and dCBN share the same syntax: $M, N ::= x \mid \lambda x M \mid MN \mid M[N/x]$. Furthermore, the values $V$ are defined as either a variable $x$ or a $\lambda$-abstraction $\lambda x M$. List contexts are defined as in dBang; reduction rules are:

- In dCBN: $L\langle\lambda x M\rangle N \rightarrow_n L\langle M[N/x]\rangle$ and $M[N/x] \rightarrow_n M\{N/x\}$

- In dCBV: $L\langle\lambda x M\rangle N \rightarrow_v L\langle M[N/x]\rangle$ and $M[L\langle V\rangle/x] \rightarrow_v L\langle M\{N/x\}\rangle$

We are now ready to define the translations of dCBN (noted $()^n$) and dCBV (noted $()^v$) into dBang. Several translations of dCBV into dBang exist (or the original Bang calculus without explicit substitutions). The first one [23], inspired by Girard second translation, does not preserve normal forms ($xy$ translates to $\text{der}(!x)!y$). Another translation was then proposed [16], which fixes this problem by simplifying the created redexes by the translations on the fly. This is the translation that we use here. It is worth noticing that this translation does not satisfy reverse simulation from dBang to dCBV [10, Figure 1] This issue has been addressed by a third translation [10]. However, reverse simulation is not necessary in our case, and we will keep with the translation proposed in [16], although we are convinced that the same developments could be carried out with the translation from [10]. This choice is motivated by the fact that the translation we consider fits better with the Linear Logic discipline from which stems Taylor expansion, and also because when considering the study of meaningfulness, we can rely on results that have been proved for this translation. Moreover, this translation enjoys a weaker property than strict reverse simulation, that we call embedding (see Lemma 55) and which is sufficient for our study (Böhm trees and Taylor expansion concern mostly iterated reductions $\rightarrow^*$, and one-step, thus reverse simulation is then not mandatory for our results).
$$
\begin{align*}
x^n &= x \\
(\lambda x M)^n &= \lambda x M^n \\
(M N)^n &= M^n! N^n \\
(M [N/x])^n &= M^n [!N^n/x]
\end{align*}
\[
x^v = !x \\
(\lambda x M)^v = !((\lambda x M)^v) \\
(M N)^v &= \begin{cases} L \langle P \rangle N^v & \text{if } M^v = L \langle !P \rangle \\ \mathbf{der}(M^v) N^v & \text{otherwise} \end{cases} \\
(M [N/x])^v &= M^v [N^v/x]
\]
$$

We abusively extend the translations to list contexts: let $\circ \in \{n, v\}$; if $L = \Box[M_1/x_1]\dots[M_k/x_k]$,
we write $L^\circ = \Box[M_1^\circ/x_1]\dots[M_k^\circ/x_k]$.

We are now ready to define meaningfulness in both systems:

**Definition 46** (dCBV and dCBN meaningfulness [30]). Given a testing context $T := \Box | T N | (\lambda x T) N$ we say that a term is $M \in \text{dCBV}$ is dCBV-meaningful (resp. $M \in \text{dCBN}$ and is dCBN-meaningful) if $T \langle M \rangle \to_v^* V$ for some value $V$ (resp. $T \langle M \rangle \to_n^* \lambda x x)^7$.

It has been shown that dCBN dCBV can be simulated through their encoding in dBang, and that
the meaningfulness of dCBV and dCBN coincides with the one of dBang (Definition 4):

**Theorem 47.** 1. If $M \to_n N$ (resp. $M \to_v N$) then $M^n \to_I N^n$ (resp. $M^v \to_I N^v$) [16, Lemma 4.6].

2. *M* is dCBN-*meaningful* iff *M*<sup>*n*</sup> is *meaningful* [30, Theorem 25].

3. *M* is dCBV-meaningful iff *M*<sup>*v*</sup> is meaningful [30, Theorem 30].

We study Böhm trees and Taylor expansion for dCBV and dCBN via their translations, in view of
meaningfulness.

**3.1 Taylor and Böhm approximation for dCBN and dCBV**

**3.1.1 Taylor expansion for dCBN and dCBV**

**Definition 48 (Resource approximations and Taylor expansion of dCBN).**

We define an approximation $\triangleleft_n$ relation between $\delta$Bang and dCBN. Notice that despite the approxi-
mants being defined in $\delta$Bang, there is no dereliction needed in the case of dCBN. The relation is given
by $x \triangleleft_n x$; if $m \triangleleft_n M$ then $\lambda x m \triangleleft_n \lambda x M$; and if $m \triangleleft_n M$ and $n_i \triangleleft_n N$ for any $i \le k$ then we have
$m[n_1, \dots, n_k] \triangleleft_n MN$ and $m[[n_1, \dots, n_k]/x] \triangleleft_n M[N/x]$.

Taylor expansion is again defined as sets of approximations: $T^n(M) = \{m \in \delta\text{Bang} \mid m \triangleleft_n M\}$.

We do not need to define a specific resource calculus for dCBN nor dCBV, since $\delta$Bang semantics
precisely subsumes both approximation theories.

► Remark 49. dCBN approximants are given by: $m, n := x \mid m[n_1, \dots, n_k] \mid \lambda x m \mid m[[n_1, \dots, n_k]/x]$

**Definition 50 (Resource approximation and Taylor expansion of dCBV).** We define the relation $m \triangleleft_v M$ for $m \in \delta\text{Bang}$ and $M \in \text{dCBV}$.

[x, ..., x]_k \triangleleft_v x for any k \in \mathbb{N}.

[\lambda x m_1, \dots, \lambda x m_k] \triangleleft_v \lambda x M \text{ if } m_i \triangleleft_v M \text{ for any } i \le k.

der(m)n \triangleleft_n MN if m \triangleleft_n M, n \triangleleft_n N and M \notin V

mn \triangleleft_v VN if [m] \triangleleft_v V and n \triangleleft_v N

<footnote n="7">⁷ Note that as for dBang, if such a reduction exists, then a weak reduction (analogous to surface reduction) is sufficient, i.e. it is not necessary to reduce under the $\lambda$s in dCBV or in the arguments of applications (or explicit substitutions) in dCBN.</footnote>
m[n/x] ⋄v M[N/x] if m ⋄v M and n ⋄v N.

Taylor expansion is defined as $T^v(M) = \{m \in \delta\text{Bang} \mid m \prec_v M\}$. Notice that, so as Taylor expansion commutes with this embedding, Taylor approximation also suppresses derelictions redexes, so as the expansion also preserves normal forms.

Both in dCBV and dCBN we also define TNF(M) as the set containing the normal forms of resource approximants of M. We get the following:

**Lemma 51.** Let $M \in \text{dCBN (resp. dCBV)}$ then $T^n(M) = T(M^n)$ (resp. $M^v$)

In the dCBV case, notice that the translation of application, as well as its Taylor expansion, is described by case on its first component such that the translation (resp. the expansion) of a term in normal form does not lead to any reducible pattern. From that we obtain the following properties:

**Corollary 52.** Let $M \in \text{dCBN (resp. dCBV)}$ then $\text{TNF}(M) = \emptyset \leftrightarrow \text{TNF}(M^n) = \emptyset$ (resp. $M^v$).

### 3.1.2 Böhm trees for dCBN and dCBV

**Definition 53.** The syntax of dCBN approximants is given by:

$$A_n ::= \perp \mid N_\lambda \mid \lambda x A_n \qquad N_\lambda ::= x \mid N_\lambda A_n$$

Notice that this syntax essentially contains inductive head normal forms, as it is standard in Böhm trees literature [12]; but also subterms such as $\lambda\vec{x}\perp$, which might correspond to non trivial approximants of non-solvable terms (e.g. $\lambda x\Omega$). We could endow the approximants with equations identifying $\lambda\vec{x}\perp$ to $\perp$, but this is not necessary<fnref n="8" /> since this trivialization is achieved by Taylor expansion. The same remarks holds for dCBV.

**Definition 54.** The syntax of dCBV approximants is given by:

$$\begin{align*} A_v &::= \perp \mid A_\lambda \mid \lambda x A_v \mid A_v [A_{x\lambda}/x] & A_{x\lambda} &::= A_\lambda A_v \mid A_{x\lambda} [A_{x\lambda}/x] \\ A_\lambda &::= x \mid A_\lambda A_v \mid A_\lambda [A_{x\lambda}/x] & & \end{align*}$$

We then define Böhm trees in the usual way, setting $\text{BT}_\circ(M) = \cup\{A_\circ \mid M \to_\circ^* N, A_\circ \sqsubseteq N\}$, for $\circ \in \{n, v\}$, (and where $M \sqsubseteq N$ means again that $M$ is obtained by replacing subterms of $N$ by $\perp$). We leave it to the reader to verify that the proof of Lemma 35 can be adapted to dCBV and dCBN, incorporating the distant setting into these standard results.

In the following, we extend translations ()$^n$ and ()$^v$ to approximants by setting $\perp^n = \perp^v = \perp$, and study the commutation between Böhm approximation and the embedding (Theorem 56), that will allow us to transport our Commutation Theorem (Theorem 45) into dCBV and dCBN. Notice that $M$ is a dCBN (resp. dCBV) approximant if and only if $M^n$ (resp. $M^v$) is a dBang approximant.

Now we can prove the weaker form of reverse simulation mentioned in the preamble of this section. Notice that this result corresponds to the embedding notion of Dufour and Mazza [20].

**Lemma 55 (Embedding).** 1. Let $M \in \text{dCBN}$. If $M^n \to_! N$, then there is some $P \in \text{dCBN}$ such that $M \to_n^* P$ and $N \to_!^* P^n$.

2. Let $M \in \text{dCBV}$. If $M^v \to_! N$, then there is some $P \in \text{dCBV}$ such that $M \to_v^* P$ and $N \to_!^* P^v$.

**Theorem 56.** 1. Let $M \in \text{dCBN}$. $(\text{BT}_n(M))^n = \text{BT}_!(M^n)$.

2. Let $M \in \text{dCBV}$. Then $(\text{BT}_v(M))^v = \text{BT}_!(M^v)$.

<footnote n="8">⁸ In fact, as for dBang, having $\text{BT}(\lambda x M) = \lambda x \text{BT}(M)$ holding globally is convenient for technical reasons.</footnote>
Thanks to the compatibility of Böhm trees and Taylor expansion with the translations of dCBN and dCBV into dBang we can apply our commutation result for dBang to both calculi. Although these results have been well established (to our knowledge, only for non-distant CbN and CbV), this application illustrates that the subsuming power of dBang has been brought in the approximation theory, which was our purpose.

► **Theorem 57.** 1. Let $M \in \text{dCBV. } \mathcal{T}^v(BT_v(M)) = \text{nf}(\mathcal{T}^v(M))$.

2. Let $M \in \text{dCBN. } \mathcal{T}^v(BT_n(M)) = \text{nf}(\mathcal{T}^n(M))$.

4 Meaningfulness and Taylor expansion

In CbN and CbV, solvability and scrutability are characterized by non-empty Taylor normal forms [26, 19]. We aim to establish an analogous link in dBang, for which a characterization of meaningfulness has been provided [30], but without an approximation theory related to this notion. The first part of this result is achieved by Theorem 58. The second part presents significant challenges, which this section aims to address.

► **Theorem 58.** Let $M \in \text{dBang. If } M \text{ is meaningful, then } \text{TNF}(M) \neq \emptyset$.

This result is encouraging for our study of Taylor expansion in dBang framework, as it applies to dCBN and dCBV through our previous results (Corollary 52): Theorem 58 applies to both settings.

The converse fails in general: some non-empty Taylor normal forms correspond to meaningless terms. As mentioned in [30], some elementary terms, such as $xx$, are meaningful, whereas $xy$ is not. Their intersection type system can distinguish between these terms, but it is unlikely that such a distinction can be captured at the syntactic level using Taylor expansion. Another approach would be to restrict ourselves to a (clash-free) fragment of dBang excluding patterns that do not make sense from a dCBV nor a dCBN discipline (such as $xx$), but again we can exhibit terms such as $(x!x)(x!x)$ (Recall that $(xM)^v = !x(M^v)$ and $(Mx)^n = M^n!x$.) that are meaningless but cannot reasonably be assigned an empty Taylor normal form.

We prove in the remaining of this section that the result holds independently for the two sub-
languages of dBang consisting of terms translated from ()^v and ()^n. Our proof employs techniques
adapted from CbN [26] and CbV [19], providing an initial characterization of the relationship
between meaningfulness and Taylor expression in a distant setting. Although it is frustrating that
we cannot prove the equivalence once for dBang and to apply it directly to its fragments; this
limitation also raises an open question which we find to be of interest: is there a significant, bigger
fragment of dBang for which the equivalence can be proven generically? Would this fragment cover
terms not coming from a dCBV or dCBN translations? This is, for now, an open question.

We consider two strict subsets of dBang: dBang<sub>V</sub> and dBang<sub>N</sub> corresponding to terms obtained by translating from dCBN and dCBV, respectively. These fragments also have the advantage of excluding clashes - problematic dBang terms such as der(λxM) - which are often omitted from the analysis [16, 23] (see Remark 12).

► **Definition 59.**

$$
\mathrm{dBang}_N: M_n := x \mid \lambda x M_n \mid M_n! M_n \mid M_n[!M_n/x]
$$

$$
\mathrm{dBang}_V: M_v := !x \mid !\left(\lambda x M_v\right) \mid L_v \langle \lambda x M_v \rangle M_v \mid L_v \langle x \rangle M_v \mid \mathrm{der}(M_v) M_v \mid M_v[M_v/x]
$$

$$
L_v := \square \mid L_v[M_v/x]
$$

A simple inspection of the definitions yields the following property:

► **Lemma 60.** For any $M \in \text{dCBV}$, $M^v \in \text{dBang}_V$, and for any $M \in \text{dCBN}$, $M^n \in \text{dBang}_N$.
Note that the converse holds for $\text{dBang}_N$, but not for $\text{dBang}_V$. For example $\text{der}(!x)M \in \text{dBang}_V$, but no term of $\text{dCBV}$ translates to this term due to the side condition of $(-)^v$ which ensures the preservation of normal forms. However, we cannot exclude these patterns from $\text{dBang}_V$ as they can be obtained from some reduction as shown in Section 3.

We aim to ensure that our fragments are closed under reduction. Otherwise, a term in $\text{dBang}_V$, for example, could reduce in a term in $\text{dBang}$ for which meaningfulness cannot be guaranteed (such as $xx$ or clashes like $\text{der}(\lambda xM)$). The following lemma can be proven by a standard induction.

**Lemma 61.** $\text{dBang}_V$ and $\text{dBang}_N$ are closed under $\rightarrow_!$.

## 4.1 Meaningfulness and Taylor Expansion for dCBN

The case of $\text{dCBN}$ is relatively easy to handle, as we can adapt to the distant case the following properties; which correspond to well-known features of $\lambda$ calculus: resource normal form corresponds to head normal forms and terms with head normal forms are meaningful.

**Lemma 62.** The normal forms of $\text{dBang}_N$ are of shape $\lambda x_1 \dots x_k(x)!N_1 \dots!N_l$, where $k, l \in \mathbb{N}$.

Naturally, full normal form requires the $N_l$ to be in normal form too, but as we shall see, this is not relevant for studying meaningfulness, as these terms will be erased by an appropriate testing context. Previous observations can be brought at a resource level.

**Lemma 63.** Let $m \prec_n M$ with $M \in \text{dBang}_N$. If $\text{nf}(m) \neq \emptyset$, it is of shape $\lambda x_1 \dots x_k(x) \bar{n}_1 \dots \bar{n}_l$.

We are now able to state the theorem establishing the classical link between Taylor expansion and meaningfulness in the case of $\text{dBang}_N$.

**Theorem 64.** Let $M \in \text{dBang}_N$. If $\text{TNF}(M) \neq \emptyset$, then $M$ is meaningful.

**Corollary 65.** For any $M$ in $\text{dCBN}$, $\text{TNF}(M) \neq \emptyset$ if and only if $M$ is meaningful.

## 4.2 Meaningfulness and Taylor expansion for dCBV

The dCBV case requires a finer analysis of normal forms. We first characterize normal forms of $\text{dBang}_V$ and their counterparts in resource calculus. The following definition and lemma are derived by a standard induction over the syntax of $\text{dBang}_V$.

**Definition 66.** The normal forms of $\text{dBang}_V$ are described by the following syntax:

$$ B := B_! | !\lambda x B | !x | L\langle B \rangle \qquad L := \Box | L[B_!|x] $$

$$ B_! := L\langle x \rangle B \mid \text{der}(B_!)B \mid L\langle B_! \rangle $$

**Lemma 67.** Let $m \prec_! M \in \text{dBang}_V$. If $\text{nf}(m) \neq \emptyset$ then it is of the following form:

$$ b := b_! | [\lambda x b, \dots, \lambda x b] | [x, \dots, x] | l\langle b \rangle \quad l := \Box | l[b_!|x] $$

$$ b_! := l\langle x \rangle b \mid \text{der}(b_!)b \mid l\langle b_! \rangle $$

We consider a family of terms which are suitable for providing an appropriate testing context for any term of $\text{dBang}_V$ with non-empty Taylor normal form, in which it eventually reduces to a value. We define $\circ_0 = \lambda x_0 x_0$ and $\circ_{k+1} = \lambda x_{k+1}!\circ_k$.

We establish the testing context with the following lemma. The proof (see Appendix C) follows Carraro and Guerrieri's technique of mutual induction [19] (Lemmas 26 and 27).

**Lemma 68.** Let $\{x_1, \dots, x_n\}$ be a set of variables and $M \in B$ (Definition 66) with $\text{fv}(M) \subseteq \{x_1, \dots, x_n\}$. There exists $c \in \mathbb{N}$ such that for any $k_1, \dots, k_n \ge c$ we have $M\{\circ_{k_1}/x_1 \dots \circ_{k_n}/x_n\} \rightarrow_!^* P$ for some $P$.
We can now state the central theorem of this section.

► **Theorem 69.** Let $M \in \text{dBang}_V$. If $\text{TNF}(M) \neq \emptyset$, then $M$ is meaningful.

► **Corollary 70.** Let $M \in \text{dCBV}$ then $M$ is meaningful if and only if $\text{TNF}(M) \neq \emptyset$.

# 5 Conclusion and Discussions

We developed an approximation theory for the distant Bang-calculus, defining Böhm trees and Taylor expansion and relating them to meaningfulness and to each other. These results are part of a wider effort to generalize the theory of the CbN and CbV λ-calculi. And indeed, we retrieve similar results in distant CbN and distant CbV, via translations in dBang.

Future work includes extending meaningfulness to proof structures, pursuing Dufour and Mazza's work [20] using non-inductive variants of classical approximation notions (in particular, their Böhm trees do not have an actual tree structure since approximations cannot be described through a tree-like inductive syntax). Also, we mentioned in Section 4 an open question about the possibility to characterize a significant fragment of dBang for which meaningful terms coincide with terms having a non-empty Taylor normal form; this line of work should be explored to develop the general understanding of dBang.

# References

1. *Advances in Linear Logic*. London Mathematical Society Lecture Note Series. Cambridge University Press, 1995.

2. Beniamino Accattoli. An Abstract Factorization Theorem for Explicit Substitutions. In Ashish Tiwari, editor, 23rd International Conference on Rewriting Techniques and Applications (RTA'12), volume 15 of Leibniz International Proceedings in Informatics (LIPIcs), pages 6-21, Dagstuhl, Germany, 2012. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.6, doi:10.4230/LIPIcs.RTA.2012.6.

3. Beniamino Accattoli and Delia Kesner. The structural λ-calculus. In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, pages 381-395, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg.

4. Beniamino Accattoli and Delia Kesner. Preservation of strong normalisation modulo permutations for the structural lambda-calculus. Logical Methods in Computer Science, Volume 8, Issue 1, March 2012. URL: http://dx.doi.org/10.2168/LMCS-8(1:28)2012, doi:10.2168/lmcs-8(1:28)2012.

5. Roberto Amadio and Pierre-Louis Curien. Domains and Lambda Calculi. 1998.

6. Zena Ariola. Relating graph and term rewriting via böhm models. Applicable Algebra in Engineering, Communication and Computing, 7, 02 1970. doi:10.1007/3-540-56868-9_15.

7. Zena M. Ariola and Stefan Blom. Skew confluence and the lambda calculus with letrec. Annals of Pure and Applied Logic, 117(1):95-168, 2002. URL: https://www.sciencedirect.com/science/article/pii/S016800720100104X, doi:10.1016/S0168-0072(01)00104-X.

8. Victor Arrial, Giulio Guerrieri, and Delia Kesner. Quantitative inhabitation for different lambda calculi in a unifying framework. Proc. ACM Program. Lang., 7 (POPL), January 2023. doi:10.1145/3571244.

9. Victor Arrial, Giulio Guerrieri, and Delia Kesner. The benefits of diligence. In Christoph Benzmüller, Marijn J.H. Heule, and Renate A. Schmidt, editors, Automated Reasoning, 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part II, volume 14740 of Lecture Notes in Computer Science, pages 338-359. Springer, 2024. doi:10.1007/978-3-031-63501-4_18.

10. Victor Arrial, Giulio Guerrieri, and Delia Kesner. The benefits of diligence. In Christoph Benzmüller, Marijn J. H. Heule, and Renate A. Schmidt, editors, Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part II, volume 14740 of Lecture Notes in Computer Science, pages 338-359. Springer, 2024. doi:10.1007/978-3-031-63501-4_18.

11. Victor Arrial, Giulio Guerrieri, and Delia Kesner. Genericity through stratification. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '24, New York, NY, USA, 2024. Association for Computing Machinery. doi:10.1145/3661814.3662113.
12 Henk Barendregt. *The Lambda Calculus: Its Syntax and Semantics*, volume 103 of *Studies in Logic and the Foundations of Mathematics*. North-Holland, Amsterdam, 1984.

13 Henk (Hendrik) Barendregt, Marko Eekelen, John Glauert, Richard Kennaway, Marinus Plasmeijer, and Michael Sleep. Term graph rewriting. pages 141–158, 01 1987.

14 Henk P. Barendregt. The type free lambda calculus. In Jon Barwise, editor, *HANDBOOK OF MATHEMATICAL LOGIC*, volume 90 of *Studies in Logic and the Foundations of Mathematics*, pages 1091–1132. Elsevier, 1977. URL: https://www.sciencedirect.com/science/article/pii/S0049237X08711297, doi:10.1016/S0049-237X(08)71129-7.

15 Gérard Boudol. Computational semantics of terms rewriting systems. Research Report RR-0192, INRIA, 1983. URL: https://inria.hal.science/inria-00076366.

16 Antonio Bucciarelli, Delia Kesner, Alejandro Ríos, and Andrés Viso. The bang calculus revisited. *Information and Computation*, 293:105047, 2023. URL: https://www.sciencedirect.com/science/article/pii/S0890540123000500, doi:10.1016/j.ic.2023.105047.

17 Albero Carraro and Giulio Guerrieri. A semantical and operational account of call-by-value solvability. In Anca Muscholl, editor, *Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings*, volume 8412 of *Lecture Notes in Computer Science*, pages 103–118. Springer, 2014. doi:10.1007/978-3-642-54830-7_7.

18 Alberto Carraro and Giulio Guerrieri. A semantical and operational account of call-by-value solvability. In Anca Muscholl, editor, *Foundations of Software Science and Computation Structures*, pages 103–118, Berlin, Heidelberg, 2014. Springer Berlin Heidelberg.

19 Alberto Carraro and Giulio Guerrieri. A semantical and operational account of call-by-value solvability. In Anca Muscholl, editor, *Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings*, volume 8412 of *Lecture Notes in Computer Science*, pages 103–118. Springer, 2014. doi:10.1007/978-3-642-54830-7_7.

20 Aloyüs Dufour and Damiano Mazza. Böhm and Taylor for All! In Jakob Rehof, editor, *9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)*, volume 299 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 29:1–29:20, Dagstuhl, Germany, 2024. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.29, doi:10.4230/LIPIcs.FSCD.2024.29.

21 Thomas Ehrhard. Collapsing non-idempotent intersection types. In Patrick Cégielski and Arnaud Durand, editors, *Computer Science Logic (CSL’12) - 26th International Workshop/21st Annual Conference of the EACSL*, volume 16 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 259–273, Dagstuhl, Germany, 2012. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.259, doi:10.4230/LIPIcs.CSL.2012.259.

22 Thomas Ehrhard. Call-by-push-value from a linear logic point of view. In Peter Thiemann, editor, *Programming Languages and Systems*, pages 202–228, Berlin, Heidelberg, 2016. Springer Berlin Heidelberg.

23 Thomas Ehrhard and Giulio Guerrieri. The bang calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value. In *Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming*, PPDP ’16, page 174–187, New York, NY, USA, 2016. Association for Computing Machinery. doi:10.1145/2967973.2968608.

24 Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. *Theoretical Computer Science*, 309(1):1–41, 2003. URL: https://www.sciencedirect.com/science/article/pii/S030439750300392X, doi:10.1016/S0304-3975(03)00392-X.

25 Thomas Ehrhard and Laurent Regnier. Uniformity and the taylor expansion of ordinary lambda-terms. *Theoretical Computer Science*, 403(2):347–372, 2008. URL: https://www.sciencedirect.com/science/article/pii/S0304397508004064, doi:10.1016/j.tcs.2008.06.001.

26 Thomas Ehrhard and Laurent Regnier. Uniformity and the taylor expansion of ordinary lambda-terms. *Theor. Comput. Sci.*, 403(2-3):347–372, 2008. URL: https://doi.org/10.1016/j.tcs.2008.06.001, doi:10.1016/J.TCS.2008.06.001.
18 Approximation theory for distant Bang calculus

27 Jean-Yves Girard. Linear logic. *Theoretical Computer Science*, 50(1):1–101, 1987. URL: https://www.sciencedirect.com/science/article/pii/0304397587900454, doi:10.1016/0304-3975(87)90045-4.

28 Axel Kerinec. *A story of lambda-calculus and approximation*. Theses, Université Paris-Nord - Paris XIII, June 2023. URL: https://theses.hal.science/tel-04624826.

29 Axel Kerinec, Giulio Manzonetto, and Michele Pagani. Revisiting call-by-value böhm trees in light of their taylor expansion. *Logical Methods in Computer Science*, Volume 16, Issue 3, Jul 2020. URL: https://lmcs.episciences.org/4817, doi:10.23638/LMCS-16(3:6)2020.

30 Delia Kesner, Victor Arrial, and Giulio Guerrieri. Meaningfulness and Genericity in a Subsuming Framework. In Jakob Rehof, editor, *9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)*, volume 299 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 1:1–1:24, Dagstuhl, Germany, 2024. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.1, doi:10.4230/LIPIcs.FSCD.2024.1.

31 Jim Laird, Giulio Manzonetto, Guy McCusker, and Michele Pagani. Weighted relational models of typed lambda-calculi. In *Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science*, LICS '13, page 301–310, USA, 2013. IEEE Computer Society. doi:10.1109/LICS.2013.36.

32 Paul Blain Levy. Call-by-push-value: A subsuming paradigm. In Jean-Yves Girard, editor, *Typed Lambda Calculi and Applications*, pages 228–243, Berlin, Heidelberg, 1999. Springer Berlin Heidelberg.
A Proofs of Section 2

► **Lemma 71.** If $M \mapsto_! N$, then for any $m \triangleleft_! M$, either $m \to_\delta \emptyset$, or there is some $n \triangleleft_! N$ such that $m \to_\delta n$.

*Proof of Lemma 71.* By induction on the definition $\mapsto_!$:

■ If $m \triangleleft_! \text{der}(L(\!N))$, then there exist $k \in \mathbb{N}, n_1, \dots, n_k \triangleleft_! N$, and $l \triangleleft_! L$ such that $m = \text{der}(l([n_1, \dots, n_k]))$, and then $m \mapsto_! \emptyset$ if $k \neq 1$, otherwise $m \mapsto_! l(n_1) \triangleleft_! L \langle N \rangle$.

■ If $m \triangleleft_! (L\langle\lambda xN\rangle P)$, then $m = l\langle\lambda xn\rangle p$ for some $l \triangleleft_! L, n \triangleleft_! N$ and $p \triangleleft_! P$. Then, $m \to_\delta l\langle n[p/x] \rangle \triangleleft_! L\langle N[P/x] \rangle$.

■ If $m \triangleleft_! N[L(\!P)/x]$ then there are $k \in \mathbb{N}, p_1, \dots, p_k \triangleleft_! P, n \triangleleft_! N, l \triangleleft_! N$ such that $m = n[l([p_1, \dots, p_k]/x]$. Then $m \to_\delta \emptyset$ if $d_x(m) \neq k$, and otherwise for any $\sigma \in P_k$, $m \to_\delta l\langle n\{p_{\sigma(1)}/x_1, \dots, p_{\sigma(k)}/x_k\} \rangle$. ◀

This simulation property can be extended to surface contexts:

► **Lemma 72.** If $M \to_! s N$, then for any $m \triangleleft_! M$, either $m \to_{\delta s} \emptyset$ or there is some $n \triangleleft_! N$ such that $m \to_{\delta s} n$.

*Proof of Lemma 72.* Let $M = S\langle M' \rangle$ and $N = S\langle N' \rangle$ with $M \mapsto_! N$; and then $m = s\langle m' \rangle$ for $s \triangleleft_! S$. By induction on surface contexts:

■ $S = \square$. Then $M \mapsto_! N$, we apply Lemma 71.

■ $S = \lambda xS'$. Then $M = \lambda xS'\langle M' \rangle$ and $N = \lambda xS'\langle N' \rangle$. By induction hypothesis, either $m' \to_{\delta s} \emptyset$, and then $\lambda xs'\langle m' \rangle \to_{\delta s} \emptyset$, either we have some $n' \triangleleft_! N'$ such that $m' \to_{\delta s} n'$, and then $\lambda xs\langle m' \rangle \to_\delta \lambda xs\langle n' \rangle$ by definition of resource surface reduction.

All remainder cases are similar, since for any resource surface context $s$ and term $n \triangleleft_! N$, there exist $S$ such that $s\langle n \rangle \triangleleft_! S\langle N \rangle$ which enables the induction hypothesis. Again, this fails for full contexts. ◀

We can obtain a symmetric property with the same arguments. We could qualify, following Dufour and Mazza [20], the previous lemma as *push forward*, and the next lemmas as *pull back*.

► **Lemma 73.** If $M \to_! s N$, then for any $n \triangleleft_! N$, there is some $m \triangleleft_! M$ such that $m \to_{\delta s} n$.

*Proof of Lemma 73.* Let $M = S\langle M' \rangle$, $N = S\langle N' \rangle$ with $M' \mapsto_! N'$ then we can reason by induction on $S$.

■ $S = \square$. Then $M \mapsto_! N$ and by a straightforward case analysis on $\mapsto_!$.

■ $S = \lambda xS'$. Then $M = \lambda xS'\langle M' \rangle$, $N = \lambda xS'\langle N' \rangle$ and $m = \lambda xs'\langle m' \rangle$ with $s' \triangleleft_! S'$. By induction hypothesis there exists $m' \triangleleft_! M'$ such that $m' \to_\delta n'$ then let $m = \lambda xs'\langle m' \rangle$ we have that $m \to_{\delta s} n$ by closure.

All the remainder cases are similar.

*Proof of Lemma 18.* We proceed by induction on the exponential depth where the reduction occurs. By lemma 72, and since $\to_{\delta s} \subseteq \to_\delta$, the only case we need to show is the full context closure, where $M = F\langle M' \rangle = !F'\langle M' \rangle$ and $N = F\langle N' \rangle$.

Then, $m = [p_1, \dots, p_k]$ for some $k \in \mathbb{N}$, where $p_i \triangleleft_! F'\langle M' \rangle$.

By induction hypothesis, either some $p_i$ reduces to $\emptyset$, and then also $m \mapsto_\delta \emptyset$, either for any $i \le k$, there is some $p'_i \triangleleft_! F'\langle N' \rangle$ such that $p_i \mapsto_\delta p'_i$. Then, $m \mapsto_\delta [p'_1, \dots, p'_k] \triangleleft_! !F'\langle N' \rangle = N$. ◀
## A.2 Proof of Section 2.4

**Proof of Lemma 42.** By induction on $A$. If $A = \perp$ then $\mathcal{T}(A) = \emptyset \subseteq \mathcal{T}(M)$. If $A = x$ then $M = x$ and $\mathcal{T}(A) = \mathcal{T}(M) = \{x\}$. If $A = \lambda x A'$, then $M = \lambda x M'$ with $A' \subseteq M'$. By induction hypothesis, $\mathcal{T}(A') \subseteq \mathcal{T}(M')$. Then, $\mathcal{T}(A) = \{\lambda x a' | a' \in \mathcal{T}(A')\} \subseteq \mathcal{T}(M) = \{\lambda x m' | m' \in \mathcal{T}(M')\}$. The other cases are treated similarly by routine induction. ◀

**Proof of Lemma 43.** We have some $M'$ such that $M \to_!^* M'$ and $A \subseteq M'$. We have that $\mathbf{nf}(\mathcal{T}(M)) = \mathbf{nf}(\mathcal{T}(M'))$ by Lemma 22. By Lemma 42 we have $\mathcal{T}(A) \subseteq \mathcal{T}(M')$. We conclude by observing that terms in $\mathcal{T}(A)$ are in normal form, and that normal terms in $\mathcal{T}(M')$ must also belong to $\mathbf{nf}(\mathcal{T}(M'))$ as they are not affected by any reduction. ◀

**Proof of Lemma 44.** By induction on $m$.

- If $m = x$, then $M = x$ and we set $A = x$.

- If $m = \lambda xn$, then $M = \lambda xN$ with $n \prec! N$. Since $n$ must be in normal form, we can apply the induction hypothesis to obtain some $A' \subseteq N$ such that $n \prec! A'$. We then set $A = \lambda x A'$.

- If $m = m_1 m_2$, then $M = M_1 M_2$ with $m_i \prec! M_i$. Again, by induction hypothesis, we have $A_1 \subseteq M_1$ and $A_2 \subseteq M_2$ with $m_i \prec! A_i$. It remains to show that $A_1 A_2$ belongs to the set of approximants described in Definition 25. Notice that $m_1$ cannot be of shape $l(\lambda x^-)$, then since $m_1 \prec! A_1$, $A_1$ cannot be a bottom or an abstraction. A simple examination of the syntax of approximants is enough to conclude that $A_1 A_2$ indeed belongs to it.

- If $m = \mathbf{der}(n)$, then we again obtain $n \prec! N$ and some $A' \subseteq N$ with $n \prec! A$. Since $n$ cannot be of shape $l([-])$. (since $m$ is normal), we can again check Definition 25 to conclude that $A = \mathbf{der}(A)'$ is an approximant, and that $m \prec! A$.

- If $m = n[p/x]$, we reason as for the application case, but using the case that $p$ cannot be of shape $l([-])$.

- If $m = [n_1, \dots, n_k]$, then $M = !N$ with $n_i \prec! N$ for all $i \in \{1, \dots, k\}$. Then by induction hypothesis, there is $A_i \subseteq N$ with $n_i \prec! A_i$. We then take $A = !A_i$, which works for any $i$. ◀

**Proof of Theorem 45.** We proceed by double inclusion.

- Take $m \in \mathcal{T}(\mathrm{BT}_!M)$, then there exists some $A_0 \in \mathcal{A}(M)$ such that $m \in \mathcal{T}(A_0)$, by Definition 40. There is $M_0$ such that $M \to_!^* M_0$ and $A_0 \subseteq M_0$. We can therefore apply Lemma 43 to conclude that $m \in \mathrm{TNF}(M_0)$, which is equal to $\mathrm{TNF}(M)$ by Lemma 22.

- Assume $m \in \mathrm{TNF}(M)$. By Lemma 23 there exists $M_0$ such that $M \to_!^* M_0$ and $m \in \mathcal{T}(M_0)$. By Lemma 44, there is $A \subseteq M_0$ such that $m \in \mathcal{T}(A)$. By definition, $A \in \mathcal{A}(M)$, so we conclude that $m \in \mathcal{T}(\mathrm{BT}_!M)$. ◀

# B Proofs of Section 3

**Proof of Lemma 51.** For the dCBN case: Considering a resource term $m \in \delta\mathrm{Bang}$, we can show that $m \prec_n M$ (see Definition 48) if and only if $m \prec! M^n$ (see Figure 1), by an immediate induction on $M$.

- $x$ is the only approximation of $x = x^n$.

- $m \prec_n \lambda x N \in \mathrm{dCBN}$ if and only if $m = \lambda xn$ with $n \prec_n N$, if and only if (induction hypothesis) $n \prec! N^n$, and then if and only if $m \prec! \lambda x N^n = (\lambda x N)^n$

- $m \prec_n NP \in \mathrm{dCBN}$ if and only if $m = n[p_1, \dots, p_k]$ with $n \prec_n N, p_i \prec! P$ for any $i \le k$ if and only if (induction hypothesis) $n \prec! N^n$ and $p_i \prec! P^n$, and then if and only if $m \prec! (NP)^n$.

- Case $M = N[P/x]$ is similar to the previous one. ◀
For the dCBV case: By induction on $M$:

■ For any $k \in \mathbb{N}$, $[x]_k \prec_v x$ and $[x]_k \prec! x^v = !x$.

■ For any $k \in \mathbb{N}$, $[\lambda x m_1, \dots, \lambda x m_k] \prec_v \lambda x M$ iff $m_i \prec_v M$ for all $i$ iff (induction hypothesis) $m_i \prec! M^v$ iff $[\lambda x m_1, \dots, \lambda x m_k] \prec! (\lambda x M)^v = ! (\lambda x M^v)$.

■ $m \prec_v NP$.

■ Either $N$ is an application. Then $m \prec_v NP$ iff $m = \text{der}(n)p$ with $n \prec_v N$ and $p \prec_v P$ iff (induction hypothesis) $n \prec! N^v$ and $p \prec! P^v$ iff $\text{der}(n)p \prec! (NP)^v$.

■ Either $N = !N'$, and then $m \prec_v NP$ iff $m = n'p$ with $n' \prec_v N'$ and $p \prec_v P$ iff $n' \prec! N'^v$, and $p \prec! P^v$ iff $n'p \prec! (NP)^v$.

► **Lemma 74** (Substitution).

1. Let $M, N \in \text{dCBN}$. $M^n\{N^n/x\} = M\{N/x\}^n$.

2. Let $M, N \in \text{dCBV}$. If $N^v = !P$, then $M\{N/x\}^v = M^v\{P/x\}$

*Proof.* Standard induction on $M$. This substitution lemma only holds for value in the case of dCBV, because substituting a term to (the traduction of) a variable necessarily puts it under an exponential. This is not an issue because in dCBV, these substitutions occur only if it is the case. ◀

**Theorem 55**

1. Let $M \in \text{dCBN}$. If $M^n \to! N$, then there is some $P \in \text{dCBN}$ such that $M \to_n^* P$ and $N \to_l^* P^n$.

2. Let $M \in \text{dCBV}$. If $M^v \to! N$, then there is some $P \in \text{dCBV}$ such that $M \to_v^* P$ and $N \to_l^* P^v$.

*Proof.* For $\circ \in \{v, n\}$, the statements of the lemma can be depicted as follows, where the dashed lines and the term $P$ are the ones to be established:

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

First, notice that the translations $()^v$ and $()^n$ generate only redexes of shape $L\langle\lambda x M\rangle N$ and $M\langle L\langle!N\rangle\rangle/x\rangle$<fnref n="9" />.

(1) By induction on the reduction $M^n \to! N$.

■ $M^n = L^n\langle\lambda x N_1^n\rangle!N_2^n$ and $N = L^n\langle N_1^n[!N_2^n/x]\rangle$. We have $N = (L\langle N_1[N_2/x]\rangle)^n$ by definition of $()^n$. Since $M = L\langle\lambda x N_1\rangle N_2$, we have $M \to! L\langle N_1[N_2/x]\rangle$, and we are done, setting $P = L\langle N_1[N_2/x]\rangle$.

■ $M^n = N_1^n[L^n\langle!N_2^n\rangle/x]$ and $N = L^n\langle N_1^n\{N_2^n/x\}\rangle$. By Lemma 74, $N = (L\langle N_1\{N_2/x\}\rangle)^n$, and again we are done, setting $P = L\langle N_1\{N_2/x\}\rangle$, since $M = N_1[L\langle N_2\rangle/x] \to! L\langle N_1\{N_2/x\}\rangle$.

■ The reduction is contextual:

■ $M^n = N_1^n!N_2^n$ and $N = N'_1!N'_2$ with $N_1 \to_n N'_1$. By induction hypothesis, there is some $P_1$ such that $N_1 \to_n^* P_1$ and $N'_1 \to_l^* P_1^n$. Then we set $P = P_1N_2$, and we have indeed $M = N_1N_1 \to_n^* P$ and $N = N'_1!N'_2 \to^* P_1^n!N_2^n = (P_1N_2)^n = P^n$.

■ $M^n = N_1^n!N_2^n$ and $N = N_1^n!N'_2$ with $N_2 \to_l N'_2$. By induction hypothesis, we have some $P_2$ such that $N_2 \to_n^* P_2$ and $N'_2 \to_l^* P_2^n$. We then set $P = N_1P_2$.

<footnote n="9">⁹ Redexes like $\text{der}(L(?!N))$ can however appear during reductions, from translations $()^v$, but not in the translation itself.</footnote>
- $M^n = N_1^n[!N_2^n/x], N = N_1^n[!N'_2/x]$ with $N_2 \to! N'_2$. We reason as in the previous case.

- $M^n = \lambda x N_0^n, N = \lambda x N'_0$ with $N_0^n \to! N'_0$. By induction hypothesis, there is $P_0$ such that $N_0 \to_n^* P_0$ and $N'_0 \to_!^* P_0^n$. We then set $P = \lambda x P_0$.

(2) By induction on the reduction $M^v \to! N$. The first two cases are similar to before except the position of the exponential.

- $M^v = L^v\langle\lambda x N_1^v\rangle N_2^v$ and $N = L^v\langle N_1^v[N_2^v/x]\rangle$. We have $N = (L\langle N_1[N_2/x]\rangle)^v$ by definition of $()^v$, and $M = L\langle\lambda x N_1\rangle N_2$. We set $P = L\langle N_1[N_2/x]\rangle$, satisfying $M \to_v P$ and $N \to_!^0 P^v$.

- $M^v = N_1^v[L^v\langle!N_2^v\rangle/x]$ and $N = L^v\langle N_1^v\{N_2^v/x\}\rangle$, then $M = N_1[L\langle N'_2\rangle/x]$ with $N'_2$ being a variable or an application. By Lemma 74 $N_1\{N'_2/x\}^v = N_1^v\{N_2^v/x\}$, so $N = (L\langle N_1\{N_2/x\}\rangle)^v$. We then set $P = L\langle N_1\{N_2/x\}\rangle$.

- The reduction is contextual. We only detail the case where the reduction occurs in the left member of an application and under a dereliction; the other cases follow from an application of the induction hypothesis as before. The second of these two cases is important, as it is the responsible for the only configuration where $P$ must be distinct from $N$.

- $M^v = \mathbf{der}(N_1^v)N_2^v$ (in that case $M = N_1N_2$ with $N_1$ not being of shape $L\langle V\rangle$ for any value $V$) and $N = \mathbf{der}(N'_1)N_2^v$. By induction hypothesis, there is some $P_1$ such that $N_1 \to_v^* P_1$ and $N'_1 \to_!^* P_1^v$. We then have two possibilities:

* $P_1^v \neq L\langle!-\rangle$ ($P_1$ is not a value). Then, $(P_1N_2)^v = \mathbf{der}(P_1^v)N_2^v$. We then set $P = P_1N_2$, and we have $M = N_1N_2 \to_v^* P_1N_2$ and $N \to_!^* \mathbf{der}(P_1^v)N_2^v = P^v$.

* $P_1^v = L^v\langle!Q^v\rangle$. Then, $(P_1N_2)^v = L^v\langle Q^v\rangle N_2^v$. We have $N \to_!^* \mathbf{der}(L^v\langle!Q^v\rangle)N_2^v \to_! L^v\langle Q^v\rangle N_2^v$ by a single reduction step$^{10}$. We then set $P = L\langle Q\rangle N_2$. It verifies $N \to_!^* P^v$ as we just saw. We also have $M \to_v^* P$, because $M = N_1N_2$ and $N_1 \to_v^* P_1$. Since $P_1^v = L^v\langle!Q^v\rangle$, it follows that $Q$ is a value (either a variable or an abstraction) and that $P_1 = L\langle Q\rangle$, by definition of $()^v$. ◀

**Theorem 56**

1. Let $M \in \text{dCBN}$. $(\text{BT}_n(M))^n = \text{BT}_!(M^n)$.

2. Let $M \in \text{dCBV}$. Then $(\text{BT}_v(M))^v = \text{BT}_!(M^v)$.

**Proof.** For this proof we will benefit from the properties of Böhm trees stated in Proposition 37.
(1) We proceed by coinduction on $\text{BT}_n(M)$.

- If $\text{BT}_n(M) = \bot$, then $\mathcal{A}(M) = \{\bot\}$. We need to show that $\mathcal{A}(M^n) = \{\bot\}$. Consider $A \in \mathcal{A}(M^n)$, we have $M^n \to_!^* N$ with $A \subseteq N$. By Lemma 55, we have some $P$ such that $M \to_!^* P$ and $N \to_!^* P^n$. By Lemma 29, $A \subseteq P^n$. Now, observe that $P$ must be some dCBN redex, otherwise $\mathcal{A}(M)$ would contain other approximations than $\bot$. Then, by simulation (Theorem 47), $P^n$ also is a redex, and since the syntax of approximants contains no redex, necessarily $A = \bot$. We conclude that $\text{BT}_!(M^n) = \bot$.

- If $\text{BT}_n(M) = x$, then $\text{BT}_n(M)^n = x = \text{BT}_!(x) = \text{BT}_!(x^n)$.

- If $\text{BT}_n(M) = \lambda x \text{BT}_n(N)$, then $(\text{BT}_n(M))^n = (\lambda x \text{BT}_n(N))^n = \lambda x (\text{BT}_n(N))^n$ (by definition of $()^n$). By coinduction hypothesis, $(\text{BT}_n(N))^n = \text{BT}_!(N^n)$. Then, $(\text{BT}_n(M))^n = \lambda x \text{BT}_!(N^n) = \text{BT}_!(\lambda x N^n) = \text{BT}_!((\lambda x N)^n) = \text{BT}_!(M^n)$.

- If $\text{BT}_n(M)$ is an application, then it is equal to some $(x)\text{BT}_n(N)$. Then, we have $(\text{BT}_n(M))^n = (x)!(\text{BT}_n(N))^n = (x)!\text{BT}_!(N^n)$, by coinduction hypothesis, which is equal to $\text{BT}_!((x)!N^n) = \text{BT}_!((x)N^n) = \text{BT}_!(M^n)$.

<footnote n="10">10 These steps are called administrative in Arrial, Guerrieri and Kessner's work [9].</footnote>
■ $\mathrm{BT}_n(M)$ cannot contain any explicit substitution, as they always correspond to redexes in dCBN.

(2) We proceed by coinduction on $\mathrm{BT}_v(M)$.

■ If $\mathrm{BT}_v(M) = \perp$, we reason as above, using this time the second item of Lemma 55.

■ If $\mathrm{BT}_v(M) = x$, then $(\mathrm{BT}_v(M))^v = x^v = !x = \mathrm{BT}_!(!x) = \mathrm{BT}_!(x^v)$.

■ If $\mathrm{BT}_v(M) = \lambda x \mathrm{BT}_v(N)$, then $(\mathrm{BT}_v(M))^v = ! (\lambda x (\mathrm{BT}_v(N))^v)$. By coinduction hypothesis, it is equal to $!(\lambda x \mathrm{BT}_!(N^v)) = \mathrm{BT}_!(!(\lambda x N^v)) = \mathrm{BT}_!((\lambda x N)^v) = \mathrm{BT}_!(M^v)$.

■ If $\mathrm{BT}_v(M)$ is an application, then it must be equal to some $x([\mathrm{BT}_v(N_i)/y_i])_{1\le i\le k} \mathrm{BT}_v(N_0^v)$ (because in this case $M$ reduces to some $L\langle x \rangle N_0$).

Then $(\mathrm{BT}_v(M))^v = x([((\mathrm{BT}_v(N_i))^v/y_i)])_{1\le i\le k} (\mathrm{BT}_v(N_0))^v$. By coinduction hypothesis, $(\mathrm{BT}_v(N_j))^v = \mathrm{BT}_!(N_j^v)$ for $j \in \{0, \dots, k\}$. Then $(\mathrm{BT}_v(M))^v = x([((\mathrm{BT}_!(N_i^v))/y_i)])_{1\le i\le k} \mathrm{BT}_!(N_0^v)$. Again, for $i \in \{1, \dots, k\}$, $\mathrm{BT}_!(N_i^v)$ cannot be an exponential, since those explicit substitutions must not be reducible. Then, $(\mathrm{BT}_v(M))^v = \mathrm{BT}_!\left(x([N_i^v/x])_{i \in \{1, \dots, k\}} N_0^v\right) = \mathrm{BT}_!(M^v)$.

■ If $\mathrm{BT}_v(M) = \mathrm{BT}_v(N_1)[\mathrm{BT}_v(N_2)/x]$, then again $\mathrm{BT}_v(N_2)$ cannot be a value, hence $(\mathrm{BT}_v(M))^v = \mathrm{BT}_!(N_1^v)[\mathrm{BT}_!(N_2^v)/x]$ (by coinduction hypothesis) $= \mathrm{BT}_!((N_1^v[N_2^v/x]) = \mathrm{BT}_!((N_1^v[N_2/x])^v)$.

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

**Proof of Theorem 57.** Let $\circ \in \{n, v\}$. We have the following equalities:

$$ \mathrm{nf}(\mathcal{T}^\circ(M)) = \mathrm{nf}(\mathcal{T}(M^\circ)) \qquad \text{By Lemma 51} $$

$$ = \mathcal{T}(\mathrm{BT}(M^\circ)) \qquad \text{By Theorem 45} $$

$$ = \mathcal{T}((\mathrm{BT}_\circ(M))^\circ) \qquad \text{By Theorem 56} $$

$$ = \mathcal{T}_\circ(\mathrm{BT}_\circ(M)) \qquad \text{By Lemma 51} $$

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

## C Proofs of Section 4

**Proof of Theorem 58.** We show the contrapositive of the statement: assume that $\mathrm{TNF}(M) = \emptyset$. By definition, for every $m \in \mathcal{T}(M)$, we have $m \to_{\delta}^* \emptyset$. Consider now any resource testing context $t$. We can easily establish that $t\langle m \rangle \to_{\delta}^* \emptyset$; since $\emptyset m = \emptyset$, $(\lambda x \emptyset)m = \emptyset$, and then by induction.

For $M$ to be meaningful, there must exist a testing context $T$ such that $T\langle M \rangle \to_{\delta}^k !P$ for some $P$ and $k \in \mathbb{N}$. We have $\lceil \lhd! P \rceil$. By iteratively applying Lemma 73, there is some term $s \lhd! T\langle M \rangle$ such that $s \to_{\delta s}^k \lceil \lhd! T, m \lhd! M \rceil$ such that $s = t\langle m \rangle$.

This leads to a contradiction: $t\langle m \rangle \to_{\delta s} \emptyset$, yet we have shown that $t\langle m \rangle \to_{\delta s} \emptyset$ for any $t$. ◀

**Proof of Lemma 62.** The following observations suffice:

■ terms in dBang$_N$ containing explicit substitutions are reducible.

■ If the leftmost subterm of an application is not a variable, the entire term is reducible. ◀

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

**Proof of Theorem 64.** Consider some $p \in \mathrm{TNF}(M)$, assumed non-empty. Then there is some $m \lhd! M$ such that $m \to_{\delta}^* p$.

By Lemma 63, $p = \lambda x_1 \dots x_k(x) \bar{n}_1 \dots \bar{n}_l$ for some $k, l \in \mathbb{N}$. Proposition 21 allows us to focus on surface reduction: there are some $m' = \lambda x_1 \dots x_k(x) \bar{n}'_1, \dots, \bar{n}'_l$ such that $m \to_{\delta s}^* m' \rightrightarrows_{\delta}^* p$ (the second part of the reduction acting inside the bags).

Then, by iteratively applying Lemma 14, we obtain $M' \in \mathrm{dBang}$ such that $m' \lhd! M'$ and $M \to_{\delta}^* M'$. By the definition of the approximation relation $\lhd!$, we have $M' = \lambda x_1 \dots x_k(x)!N'_1 \dots! N'_l$ where $\bar{n}'_i \lhd! N'_i$.
We now define the appropriate testing context $T = ((\lambda x \Box)!(\lambda y_1...y_l!z_0))!z_1...!z_k$ where the $z_i$ are chosen distinct from the $x_j$ and $y_j$.

We observe that $T\langle M' \rangle \to_{!s} (\lambda x_1...x_k(\lambda y_1...y_l!z_0)!z_1...!z_k)!N'_1...!N'_k \to_{!s}^2!z_0$. We conclude as follows: since $T\langle M' \rangle \to_{!s}^2!z_0$, $M \to_{!s}^* M'$ and $T$ is a surface context, we have $T\langle M \rangle \to_{!s}^*!z_0$ by the contextual closure of $\to_{!s}$. Therefore, $M$ is meaningful. ◀

**Proof of Corollary 65.** Recall that, by Corollary 52 and Theorem 47, TNF($M$) $\neq \emptyset$ if and only if TNF($M^n$) $\neq \emptyset$, and $M$ is meaningful if and only if $M^n$ is meaningful.

($\rightarrow$) Assume $M$ is meaningful, then $M^n$ is also meaningful, and by Theorem 58, TNF($M^n$) $\neq \emptyset$. It follows that TNF($M$) $\neq \emptyset$.

($\leftarrow$) If TNF($M$) $\neq \emptyset$, then TNF($M^n$) $\neq \emptyset$. By Lemma 60, $M^n \in \text{dBang}_N$, and Theorem 64 implies that $M^n$ must be meaningful. Therefore, $M$ is also meaningful. ◀

In what follows, the variables in $\circ_i$ are always taken fresh, so as they do not interfere with variables in the terms where the $\circ_i$ are substituted. In particular, we use the fact that for any $i > 1$ and any $M, \circ_k!M \to_l^2!\circ_{k-1}$.

**Proof of Lemma 68.** By induction on the syntax $B$:

- If $M$ is of the form $!x$ or $!\lambda x B$, then we are done since $M\sigma \to_l^0!P$ for some $P$ and any substitution $\sigma$.

- If $M \in B_!$, we apply Lemma 75, which guarantees the existence of a substitution $\sigma$ such that $M\sigma \to_l^*!\circ_j$ for some $j$.

- If $M = N[P_1/x_1]\dots[P_k/x_k]$, then $N \in B$ and $P_i \in B_!$ for all $i$. Let $\{y_1, \dots, y_l\} = \text{fv}(N) \cup \bigcup_{i \le k} \text{fv}(P_k)$. By induction hypothesis, we have $c$ such that for any $k_1, \dots, k_l \ge c$, $N\{\circ_{k_1}/y_1, \dots, \circ_{k_l}/y_l\} \to_l!P$ for some $P$. By Lemma 75, for $i \le k$, there exist $c_i$ and $n_i$ such that for any $k_{i,1}, \dots, k_{i,l} \ge c_i$, and for some $j_i \ge n_i$, $P_i\{\circ_{k_{i,1}}/y_1, \dots, \circ_{k_{i,l}}/y_l\} \to_l^*!P'[!\circ_{r_1}/y_1]\dots[!\circ_{r_l}/y_l] \to_l!P'\{!\circ_{r_1}/y_1}\dots\{!\circ_{r_l}/y_l\}$, which is again a value as required. ◀

**▶ Lemma 75.** Let $\{x_1, \dots, x_n\}$ be a set of variables and $M \in B_!$ (Definition 66) with $\text{fv}(M) \subseteq \{x_1, \dots, x_n\}$. There exist $k, c \in \mathbb{N}$ such that for any $k_1, \dots, k_n \ge c$, there is some $j \ge k$ with $M\{\circ_{k_1}/x_1 \dots \circ_{k_n}/x_n\} \to_l^*!\circ_j$.

**Proof.** By induction on $B_!$:

- $M = L\langle x \rangle N = (x[N_1/x_1]\dots[N_m/y_m])N$ with $N \in B$, $N_i \in B_!$ for all $x \le m$, and $\{x_1, \dots, x_n\} = \text{fv}(M)$. By Lemma 68, there exists $k$ such that $N\{\circ_{k_1}/x_1, \dots, \circ_{k_n}/x_n\} \to_l^*!P$ for any $k_i \ge k$ and some $P$.

By induction hypothesis, we have for each $i \le m$, some $l_i$ and $c_i$ such that for any $l_{i,1}, \dots, l_{i,n} \ge l_i$, $N_i\{\circ_{l_{i,1}}/y_1, \dots, \circ_{l_{i,n}}/y_n\} \to_l^*!\circ_{j_i}$ for some $j_i \ge c_i$.

Let $n_x$ be the index of $x$ in $\{x_1, \dots, x_n\}$ (of course, $x \in \text{fv}(M)$).

We then set $r_i = \max\{k_i, l_{i,1}, \dots, l_{i,n}\}$ for each $i \ne n_x$; and we consider $r_{n_x}$ an arbitrary integer greater or equal to $\max\{k_{n_x}, l_{n_x,1}, \dots, l_{n_x,n}\}$.

We find that $M\{\circ_{r_1}/x_1, \dots, \circ_{r_m}/x_m\} \to_l^* \circ_{n_x} [!\circ_{r'_1}/x_1]\dots[!\circ_{r'_m}/x_1]!P'$, with $r'_i \ge r_i$ for all $i \le m$. The reduction then yields $\circ_{n_x}!P'$, which reduces immediately to $!\circ_{r_{n_x}-1}$. This concludes the case, as the reduction holds for any $r_{n_x} \ge \max\{k_{n_x}, l_{n_x,1}, \dots, l_{n_x,n}\}$.

- $M = \text{der}(N)N'$ with $N \in B_!$, $N' \in B$, and $\{x_1, \dots, x_m\} = \text{fv}(M)$. By induction hypothesis, we have some $n, n', c$ such that for any $n_1, \dots, n_m \ge n$ and, $N\{\circ_{n_1}/x_1, \dots, \circ_{n_m}/x_m\} \to_l^*!\circ_j$ for all $j \ge c$, and for any $n'_1, \dots, n'_m \ge n'$, $N'\{\circ_{n'_1}/x_1, \dots, \circ_{n'_m}/x_m\} \to_l^*!P$ for some $P$.
Then, consider $k_i = \max\{n_i, n_i'\}$ for any $i \le m$, we have that $M\{\circ_{k_1}/x_1, \dots, \circ_{k_m}/x_m\} \to_i^* \text{der}(!_{\circ_j})!P' \to_i! \circ_j!P' \to_i^2! \circ_{j-1} (!_{\circ_j} \circ_{j-1}!)P' \to_i^* P'$ (notice that we need here to take $j > 1$, which is allowed by our hypothesis).

$M = N[P_1/x_1]\dots[P_k/x_k]$. This case is similar to the third case of Lemma 68: the explicit substitutions are removed after an application of the induction hypothesis. ◀

**Proof of Theorem 69.** Consider some $p \in \text{TNF}(M)$, assumed non-empty. There is some $m \triangleleft! M$ such that $m \to_{\delta}^* p$. By Lemma 67, $p$ belongs to the syntax $b$. Proposition 21 ensures that there is some $p' \in b$ such that $m \to_{\delta s} p'$ (as in Theorem 64, we focus on internal reduction).

By iteratively applying Lemma 73, we obtain $P'$ such that $M \to_i^* P'$ and $p' \triangleleft! P'$. By the definition of $\triangleleft!$, we also have that $P' \in B$.

Let $\{x_1, \dots, x_k\} = \text{fv}(P')$. Lemma 68 implies that there are some terms $N_1, \dots, N_k$ such that $P'\{N_1/x_1, \dots, N_k/x_k\} \to_i^* !Q$ for some term $Q$.

We define the testing context $C = (\lambda x_1 \dots \lambda x_k \Box)!N_1 \dots !N_k$, which satisfies $C\langle P' \rangle \to_i^* !Q$. We can conclude that $M$ is meaningful by the contextuality of reduction, since $C\langle M \rangle \to_i^* C\langle P' \rangle \to_i^* !Q$. ◀

**Proof of Corollary 70.** Recall that, by Corollary 52 and Theorem 47, $\text{TNF}(M) \neq \emptyset$ if and only if $\text{TNF}(M^v) \neq \emptyset$, and $M$ is meaningful if and only if $M^v$ is meaningful.

($\rightarrow$) Assume $M$ is meaningful, then $M^v$ is meaningful, and by Theorem 58, $\text{TNF}(M^v) \neq \emptyset$. It follows that $\text{TNF}(M) \neq \emptyset$.

($\leftarrow$) If $\text{TNF}(M) \neq \emptyset$, then $\text{TNF}(M^v) \neq \emptyset$. By Lemma 60, $M^v \in \text{dBang}_V$, and Theorem 69 implies that $M^v$ is meaningful. Therefore, $M$ is also meaningful. ◀