# How to Play the Accordion: Uniformity and the (Non-)Conservativity of the Linear Approximation of the λ-Calculus

Rémy Cerda, Lionel Vaux Auclair

► To cite this version:

Rémy Cerda, Lionel Vaux Auclair. How to Play the Accordion: Uniformity and the (Non-Conservativity of the Linear Approximation of the λ-Calculus. 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025), Mar 2025, Jena, Germany. pp.23, 10.4230/LIPIcs.STACS.2025.23 . hal-04964448

HAL Id: hal-04964448

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

Submitted on 23 Jan 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
# How to Play the Accordion:
Uniformity and the (Non-)Conservativity of the
Linear Approximation of the λ-Calculus

Rémy Cerda

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

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

Aix-Marseille Université, CNRS, I2M, France
Université Paris Cité, CNRS, IRIF, F-75013, Paris, France

Lionel Vaux Auclair

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

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

Aix-Marseille Université, CNRS, I2M, France

## Abstract

Twenty years after its introduction by Ehrhard and Regnier, differentiation in λ-calculus and in linear logic is now a celebrated tool. In particular, it allows to write the Taylor formula in various λ-calculi, hence providing a theory of linear approximations for these calculi. In the standard λ-calculus, this linear approximation is expressed by results stating that the (possibly) infinitary β-reduction of λ-terms is simulated by the reduction of their Taylor expansion: in terms of rewriting systems, the resource reduction (operating on Taylor approximants) is an extension of the β-reduction.

In this paper, we address the converse property, conservativity: are there reductions of the Taylor approximants that do not arise from an actual β-reduction of the approximated term? We show that if we restrict the setting to finite terms and β-reduction sequences, then the linear approximation is conservative. However, as soon as one allows infinitary reduction sequences this property is broken. We design a counter-example, the Accordion. Then we show how restricting the reduction of the Taylor approximants allows to build a conservative extension of the β-reduction preserving good simulation properties. This restriction relies on uniformity, a property that was already at the core of Ehrhard and Regnier's pioneering work.

**2012 ACM Subject Classification** Theory of computation → Rewrite systems; Theory of computation → Lambda calculus; Theory of computation → Proof theory; Theory of computation → Linear logic

**Keywords and phrases** program approximation, quantitative semantics, lambda-calculus, linear approximation, Taylor expansion, conservativity

**Digital Object Identifier** 10.4230/LIPIcs.STACS.2025.23

**Related Version** A short abstract of a preliminary version of this work has been presented at the 7th International Workshop on Trends in Linear Logic and its Applications (TLLA'23). Most of this work has also appeared in the first author's PhD thesis, with the noticeable difference that Theorem 27 was only proved in a qualitative setting.

*Previous Version (Short abstract presented at TLLA'23): https://lipn.univ-paris13.fr/TLLA/2023/abstracts/05-Final.pdf*

*Previous Version (PhD thesis version, see Chapter 5): https://hal.science/tel-04664728 [7]*

**Funding** Rémy Cerda: Partially supported by the French ANR project RECIPROG (ANR-21-CE48-019).

Lionel Vaux Auclair: Partially supported by the French ANR projects LambdaComb (ANR-21-CE48-0017), RECIPROG (ANR-21-CE48-019), and PPS (ANR-19-CE48-0014).

# 1 Introduction

The traditional approach to program approximation in a functional setting consists in describing the total information that a (potentially non-terminating) program can produce by the supremum of the finite pieces of information it can produce in finite time. This

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

© Rémy Cerda and Lionel Vaux Auclair;
licensed under Creative Commons License CC-BY 4.0

42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025).

Editors: Olaf Beyersdorff, Michał Pilipczuk, Elaine Pimentel, and Nguyễn Kim Thắng;
Article No. 23; pp. 23:1–23:21

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

Leibniz International Proceedings in Informatics
LIPICS Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

<figure><img src="image_8.png" /></figure>
## 23:2 How to Play the Accordion

continuous approximation is tightly related to the Scott semantics of λ-calculi [29]: the Böhm tree of a term (or equivalently its semantics) is the limit of the approximants produced by hereditary head reduction [21, 32, 3].

More recently, Ehrhard and Regnier introduced the differential λ-calculus and differential linear logic [16, 17], following ideas rooted in the semantics of linear logic [20, 13, 14]. This suggested the renewed approach of linear approximation of functional programs. In this setting, a program (i.e. a λ-term) is approximated by multilinear (or “polynomial”) programs, obtained by iterated differentiation at zero. Using this differential formalism, the Taylor formula yields a weighted sum $T(M)$ of all multilinear approximants of a λ-term $M$, producing the same total information as $M$, via normalization. More precisely, Ehrhard and Regnier’s “commutation” theorem [19, 18] ensure that the normal form of the Taylor expansion of $M$ is the Taylor expansion of the Böhm tree of $M$:

$$nf(T(M)) = T(BT(M)) \qquad (1)$$

(and a Böhm tree is uniquely determined by its Taylor expansion). This approach subsumes the previous one [2]. In addition, it allows for characterising quantitative properties of programs (e.g. complexity [11]), which is a key benefit of linearity. This approximation technique has been fruitfully applied to many languages, richer than the plain λ-calculus: nondeterministic [31], probabilistic [10], extensional [5], call-by-value [23], and call-by-push-value [15, 9] calculi, as well as for Parigot’s λμ-calculus [1]. The interplay of the operational and Taylor approximations also suggests a broader notion of a approximation of a computation process [26, 12].

Another benefit of linear approximation is that it can approximate not only β-normalisation (the information ultimately produced by a program) but β-reduction (the “information flow” along program execution). In particular, Equation (1) can be refined into

$$M \to_{\beta}^* N \Rightarrow T(M) \to_{\to_r} T(N), \qquad (2)$$

where $\to_{\to_r}$ denotes the so-called “resource” reduction acting linearly on approximants. As highlighted by our previous work [8, 7], this can even be extended to

$$M \to_{\beta}^{\infty} N \Rightarrow T(M) \to_{\to_r} T(N) \qquad (3)$$

if one extends the λ-calculus with infinite λ-terms and an infinitary closure of the β-reduction, which is a way to encompass infinite computations and their limits [22].

This paper is interested in the converse of Equations (2) and (3): is the linear approximation of the λ-calculus conservative? In other terms, we ask whether every resource reduction from $T(M)$ to $T(N)$ corresponds to a β-reduction sequence from $M$ to $N$.

We show that the finite β-reduction of finite λ-terms is conservatively approximated (Section 3), but we are able to design a counter-example to conservativity (the Accordion A) as soon as we want to approximate infinitary β-reductions (Section 4). However, we introduce a uniform linear approximation allowing for the same good properties as the standard one, while enjoying conservativity (Section 5).

# 2 Preliminaries

In this section, we briefly recall the linear approximation of the λ-calculus, following its refined presentation in [7]. We first recall the definition of the λ-calculus, as well as its “001” infinitary extension: this is the version of the infinitary λ-calculus that fits the formalism
of both continuous and linear approximations as they are usually presented (Section 2.1). Then we present the resource $\lambda$-calculus, i.e. a linear variant of the $\lambda$-calculus (there are no duplications or erasures of subterms during the reduction) enjoying strong confluence and normalisation properties (Section 2.2). Finally, the linear approximation relies on the Taylor expansion, that maps a $\lambda$-term to a sum of resource terms, in a way such that the reduction of $\lambda$-terms is simulated by the reduction of the resource approximants (Section 2.3).

## 2.1 Finite and infinitary $\lambda$-calculi

We give a brief presentation of the 001-infinitary $\lambda$-calculus. A more detailed exposition and a general account of infinitary $\lambda$-calculi can be found in [7, 4]. From now on, we fix a countable set $V$ of variables.

**► Definition 1.** The set $\Lambda$ of (finite) $\lambda$-terms is the set $\mathcal{X}$ defined by the inductive rules:

$$ \frac{x \in \mathcal{V} \quad (\mathcal{V})}{x \in \mathcal{X}} \qquad \frac{x \in \mathcal{V} \quad M \in \mathcal{X} \quad (\lambda)}{\lambda x.M \in \mathcal{X}} \qquad \frac{M \in \mathcal{X} \quad N \in \mathcal{X} \quad (@)}{(M)N \in \mathcal{X}} $$

The set $\Lambda^{001}$ of 001-infinitary $\lambda$-terms is the set $\mathcal{X}$ defined by the rules $(\mathcal{V})$, $(\lambda)$, and:

$$ \frac{M \in \mathcal{X} \quad \triangleright N \in \mathcal{X} \quad (@^{001})}{(M)N \in \mathcal{X}} \qquad \frac{N \in \mathcal{X} \quad \triangleright N \in \mathcal{X} \quad (\triangleright)}{\triangleright} $$

where the rule $(\triangleright)$ is treated coinductively: infinite derivations are allowed provided each infinite branch crosses infinitely often this coinductive rule.

This means that $\Lambda^{001}$ contains the infinitary $\lambda$-terms whose syntax tree contains only infinite branches entering infinitely often the argument side of an application.

Notice that we use Krivine's notation for applications [25], i.e. we parenthesise functions instead of arguments. We abbreviate the application of a term to successive arguments $(\cdots((M)N_1)\cdots)N_k$ as $(M)N_1\cdots N_k$, which is obtained by nesting applications on the left: this allows to use parentheses more sparingly, which will be a great relief later on. By contrast, $(M_1)(M_2)\cdots(M_k)N$ is obtained by nesting applications on the right. A typical example of a term in $\Lambda^{001}$ is $(x)^\omega := (x)(x)(x)\cdots$. Observe also that there is an immediate inclusion $\Lambda \subseteq \Lambda^{001}$. On the contrary, neither $\lambda x_0.\lambda x_1.\lambda x_2\cdots$ nor $((\cdots)x_2)x_1)x_0$ are allowed in $\Lambda^{001}$.

In practice we only consider infinitary terms having finitely many free variables, which allows us to consider them up to $\alpha$-equivalence (i.e. renaming of bound variables) – as one usually does when dealing with $\lambda$-terms, and as we will do implicitly in all this paper. This enables us to define capture-avoiding substitution in the usual way, and we denote by $M[N/x]$ the term obtained by substituting $N$ to $x$ in $M$. We refer to [6] for a more careful and detailed presentation. These sets come equipped with the following dynamics.

**► Definition 2.** The relation $\to_{\beta} \subset \Lambda^{001} \times \Lambda^{001}$ of $\beta$-reduction is defined by the rules:

$$ \frac{\lambda x.M)N \to_{\beta} M[N/x] \quad (\beta)}{P \to_{\beta} P'} \qquad \frac{\lambda x.P \to_{\beta} \lambda x.P'}{\lambda x.P \to_{\beta} \lambda x.P'} \quad (\lambda_{\beta}) $$

$$ \frac{P \to_{\beta} P'}{(P)Q \to_{\beta} (P')Q} \quad (@l_{\beta}) \qquad \frac{Q \to_{\beta} Q'}{(P)Q \to_{\beta} (P)Q'} \quad (@r_{\beta}) $$
**► Definition 3.** The relation $\xrightarrow{\beta}^{001} \subset \Lambda^{001} \times \Lambda^{001}$ of **001-infinitary $\beta$-reduction** is defined by the rules:

$$ \frac{M \xrightarrow{\beta}^* x}{M \xrightarrow{\beta}^{001} x} (\nu_{\beta}^{001}) \qquad \frac{M \xrightarrow{\beta}^* \lambda x.P \quad P \xrightarrow{\beta}^{001} P'}{M \xrightarrow{\beta}^{001} \lambda x.P'} (\lambda_{\beta}^{001}) \\ \frac{M \xrightarrow{\beta}^* (P)Q \quad P \xrightarrow{\beta}^{001} P' \quad \triangleright Q \xrightarrow{\beta}^{001} Q'}{M \xrightarrow{\beta}^{001} (P')Q'} (@_{\beta}^{001}) \qquad \frac{Q \xrightarrow{\beta}^{001} Q'}{\triangleright Q \xrightarrow{\beta}^{001} Q'} (\triangleright) $$

where $\xrightarrow{\beta}^*$ denotes the reflexive-transitive closure of $\xrightarrow{\beta}$.

Infinitary $\beta$-reduction can be understood as allowing an infinite number of $\beta$-reduction steps, as long as the $\beta$-redexes are fired inside increasingly nested arguments of applications. This is formalised in the following result:

**► Theorem 4 (stratification).** Given $M, N \in \Lambda^{001}$, there is a reduction $M \xrightarrow{\beta}^{001} N$ iff there exists a sequence of terms $(M_d) \in (\Lambda^{001})^N$ such that for all $d \in \mathbb{N}$,

$$ M = M_0 \xrightarrow{\beta \geq 0} M_1 \xrightarrow{\beta \geq 1} M_2 \xrightarrow{\beta \geq 2} \dots \xrightarrow{\beta \geq d-1} M_d \xrightarrow{\beta \geq d} N, $$

where $\xrightarrow{\beta}^*$ and $\xrightarrow{\beta}^{001}$ denote $\beta$-reductions occurring inside (at least) $d$ nested arguments of applications. Formally, **$\beta$-reduction at minimum depth $d$ is defined by:**

$$ \frac{M \xrightarrow{\beta} M' \qquad (\nu_{\beta \geq 0})}{M \xrightarrow{\beta \geq 0} M'} \qquad \frac{P \xrightarrow{\beta \geq d+1} P' \qquad (\lambda_{\beta \geq d+1})}{\lambda x.P \xrightarrow{\beta \geq d+1} \lambda x.P'} \\ \frac{P \xrightarrow{\beta \geq d+1} P' \qquad (@_{\beta \geq d+1})}{(P)Q \xrightarrow{\beta \geq d+1} (P')Q} \qquad \frac{Q \xrightarrow{\beta \geq d} Q' \qquad (@_{\beta \geq d+1})}{(P)Q \xrightarrow{\beta \geq d+1} (P)Q'} $$

and **001-infinitary $\beta$-reduction at minimum depth $d$ is defined by:**

$$ \frac{M \xrightarrow{\beta}^{001} M' \qquad (\nu_{\beta \geq 0})}{M \xrightarrow{\beta}^{001} M'} \qquad \frac{x \xrightarrow{\beta}^{001} x \qquad (\nu_{\beta \geq d+1}^{001})}{\lambda x.P \xrightarrow{\beta}^{001} \lambda x.P'} \\ \frac{P \xrightarrow{\beta \geq d+1} P' \qquad (@_{\beta \geq d+1}^{001})}{\lambda x.P \xrightarrow{\beta \geq d+1} \lambda x.P'} \qquad \frac{P \xrightarrow{\beta \geq d+1} P' \quad Q \xrightarrow{\beta \geq d} Q' \qquad (@_{\beta \geq d+1}^{001})}{(P)Q \xrightarrow{\beta \geq d+1} (P')Q} $$

A typical (and even motivating) example of an infinitary $\beta$-reduction involves the fix-point combinator $\mathcal{Y} := \lambda f.(\lambda x.(f)(x)x)\lambda x.(f)(x)x$. It consists in the reduction $(\mathcal{Y})M \xrightarrow{\beta}^{001} (M)^\omega$ corresponding to the sequence $(\mathcal{Y})M \xrightarrow{\beta}^{*}_{0} (M)(\mathcal{Y})M \xrightarrow{\beta}^{*}_{1} (M)(M)(\mathcal{Y})M \xrightarrow{\beta}^{*}_{2} \dots$. On the contrary, the infinite reduction sequence $\Omega \xrightarrow{\beta} \Omega \xrightarrow{\beta} \Omega \xrightarrow{\beta} \dots$, where $\Omega := (\lambda x.(x)x)\lambda x.(x)x$, does not give rise to a 001-infinitary reduction because the redexes are fired at top-level all the way. On the other hand, each finite reduction sequence $\Omega \xrightarrow{\beta}^* \Omega$ induces a reduction $\Omega \xrightarrow{\beta}^{001} \Omega$, but only because $\xrightarrow{\beta}^{001}$ contains $\xrightarrow{\beta}^*$ (see [8], Lemma 2.13).

## 2.2 The resource $\lambda$-calculus

The resource $\lambda$-calculus is the target language of the linear approximation of the $\lambda$-calculus. We recall its construction, and we refer to [31, 7] for more details. The main intuition behind this calculus is that arguments become *finite multisets*, and that $(\lambda x.s)[t_1, \dots, t_n]$ will reduce to a term obtained by substituting *linearly* one $t_i$ for each occurrence of $x$ in $s$. The different matchings of the $t_i$'s and the occurrences of $x$ are superposed by a sum operator; if a wrong number of $t_i$'s is provided, the term collapses to the empty sum.
Given a set $\mathcal{X}$, we denote by $!\mathcal{X}$ the set of finite multisets of elements of $\mathcal{X}$. A multiset is denoted by $\bar{x} = [x_1, \dots, x_n]$, with its elements in an arbitrary order. Multiset union is denoted multiplicatively, by $\bar{x} \cdot \bar{y}$. Accordingly, the empty multiset is denoted by 1. We may also write $[x_1^{k_1}, \dots, x_m^{k_m}]$ to indicate multiplicities: this is the same as $[x_1]^{k_1} \cdots [x_m]^{k_m}$.

**Definition 5.** The set $\Lambda_r$ of resource terms is defined by the rules:

$$ \frac{x \in \mathcal{V}}{x \in \Lambda_r} (\mathcal{V}) \qquad \frac{x \in \mathcal{V} \quad s \in \Lambda_r}{\lambda x.s \in \Lambda_r} (\lambda) \qquad \frac{s \in \Lambda_r \quad \bar{t} \in !\Lambda_r}{(s)\bar{t} \in \Lambda_r} (@!) $$

and is implicitly quotiented by $\alpha$-equivalence. Multisets in $!\Lambda_r$ are called resource monomials. To denote indistinctly $\Lambda_r$ or $!\Lambda_r$, we write $(!)\Lambda_r$.

Given a semiring $\mathbb{S}$ and a set $\mathcal{X}$, we denote by $\mathbb{S}^{\mathcal{X}}$ the set of possibly infinite linear combinations of elements of $\mathcal{X}$ with coefficients in $\mathbb{S}$, considered as formal weighted sums. Given a sum $\mathbf{S} \in \mathbb{S}^{\mathcal{X}}$, its support $|\mathbf{S}|$ is the set of all elements of $\mathcal{X}$ bearing a non-null coefficient. We also denote by $\mathbb{S}^{(\mathcal{X})}$ the sub-semimodule of $\mathbb{S}^{\mathcal{X}}$ of all sums having a finite support.

We use the following syntactic sugar. The empty sum $\sum_{x \in \mathcal{X}} 0 \cdot x$ is denoted by 0. The one-element sum $\sum_{x \in \mathcal{X}} \delta_{x,y} \cdot x$ is assimilated to $y$, yielding an inclusion $\mathcal{X} \subseteq \mathbb{S}^{\mathcal{X}}$. Sums can be summed, i.e. $\sum_{x \in \mathcal{X}} a_x \cdot x + \sum_{x \in \mathcal{X}} b_x \cdot x = \sum_{x \in \mathcal{X}} (a_x + b_x) \cdot x$. It is also convenient to extend by linearity all the constructors of the calculus to sums of resource terms, i.e.

$$ \lambda x. \left( \sum_{i \in I} a_i \cdot s_i \right) := \sum_{i \in I} a_i \cdot \lambda x.s_i, \\ \left( \sum_{i \in I} a_i \cdot s_i \right) \sum_{j \in J} b_j \cdot \bar{t}_j := \sum_{i \in I} \sum_{j \in J} a_i b_j \cdot (s_i) \bar{t}_j, \qquad (4) \\ \left[ \sum_{i \in I} a_i \cdot s_i \right] \cdot \sum_{j \in J} b_j \cdot \bar{t} := \sum_{i \in I} \sum_{j \in J} a_i b_j \cdot [s_i] \cdot \bar{t}_j. $$

**Definition 6.** For all $u \in (!)\Lambda_r$, $\bar{t} = [t_1, \dots, t_n] \in !\Lambda_r$ and $x \in \mathcal{V}$, the multilinear substitution of $x$ by $\bar{t}$ in $u$ is the finite sum $s(\bar{t}/x) \in \mathbb{N}^{((!)\Lambda_r)}$ defined by

$$ s(\bar{t}/x) := \begin{cases} \sum_{\sigma \in \mathcal{S}(n)} u[t_{\sigma(1)}/x_1, \dots, t_{\sigma(n)}/x_n] & \text{if } x \text{ occurs } n \text{ times in } u \\ 0 & \text{otherwise} \end{cases} $$

where $x_1, \dots, x_n$ is an arbitrary enumeration of the occurrences of $x$ in $u$, and $u[t_{\sigma(1)}/x_1, \dots]$ denotes the result of the (capture-avoiding) substitution of each $x_i$ by the corresponding $t_{\sigma(i)}$.

**Definition 7.** The relation $\rightarrow_r \subset \mathbb{N}^{((!)\Lambda_r)} \times \mathbb{N}^{((!)\Lambda_r)}$ of resource $\beta$-reduction is defined using the auxiliary relation $\rightarrow_r \subset (!)\Lambda_r \times \mathbb{N}^{((!)\Lambda_r)}$ generated by the rules

$$ \frac{\lambda x.s \quad \bar{t} \longrightarrow_r s \langle \bar{t}/x \rangle}{(\lambda x.s) \bar{t} \longrightarrow_r s(\bar{t}/x)} \quad (\beta_r) \qquad \frac{s \longrightarrow_r S' \quad \lambda x.s \longrightarrow_r \lambda x.S'}{\lambda x.s \longrightarrow_r \lambda x.S'} \quad (\lambda_r) \qquad \frac{s \longrightarrow_r S' \quad (s) \bar{t} \longrightarrow_r (S') \bar{t}}{(s) \bar{t} \longrightarrow_r (S') \bar{t}} \quad (@l_r) $$

$$ \frac{\bar{t} \longrightarrow_r \bar{T}'}{(s) \bar{t} \longrightarrow_r (s) \bar{T}'} \quad (@r_r) \qquad \frac{s \longrightarrow_r S' \quad [s] \cdot \bar{t} \longrightarrow_r [S'] \cdot \bar{t}}{[s] \cdot \bar{t} \longrightarrow_r [S'] \cdot \bar{t}} \quad (!_r) $$

as well as the lifting rule

$$ \frac{u_1 \longrightarrow_r U'_1 \quad \forall i \ge 2, \quad u_i \longrightarrow_r^? U'_i}{\sum_{i=1}^n u_i \longrightarrow_r \sum_{i=1}^n U'_i} \quad (\Sigma_r) $$

where $\longrightarrow_r^?$ is the reflexive closure of $\longrightarrow_r$.
## 23:6 How to Play the Accordion

From now on, we fix a semiring $\mathbb{S}$. We consider $\mathbb{N}$ as a subset of $\mathbb{S}$ through the map $n \mapsto 1 + \dots + 1$ (notice however that it might not be an injection), and we suppose that $\mathbb{S}$ “has fractions”, i.e. for all non-null $n \in \mathbb{N}$ there is some $\frac{1}{n} \in \mathbb{S}$ such that $n \times \frac{1}{n} = 1$. This is the case of the semirings $\mathbb{Q}_+$ and $\mathbb{R}_+$ of non-negative rational (resp. real) numbers, but also of the semiring $\mathbb{B}$ of boolean values (equipped with the logical “or” and “and” operations).

**Definition 8.** Given a set $\mathcal{X}$ and a semiring $\mathbb{S}$, a family of sums $(\mathbf{S}_i)_{i \in I} \in (\mathbb{S}^{\mathcal{X}})^I$ is **summable** when each $x \in \mathcal{X}$ bears a non-null coefficient in finitely many of the $\mathbf{S}_i$. If this is the case then $\sum_{i \in I} \mathbf{S}_i$ is a well-defined sum.

**Definition 9.** The relation $\dashrightarrow_r \subset \mathbb{S}^{(1)\Lambda_r} \times \mathbb{S}^{(1)\Lambda_r}$ of **pointwise resource reduction** is defined by saying that there is a reduction $\mathbf{U} \dashrightarrow_r \mathbf{V}$ whenever there are summable families $(u_i)_{i \in I} \in ((!)\Lambda_r)^I$ and $(V_i)_{i \in I} \in (\mathbb{N}^{((1)\Lambda_r)})^I$ such that

$$ \mathbf{U} = \sum_{i \in I} a_i \cdot u_i, \quad \mathbf{V} = \sum_{i \in I} a_i \cdot V_i \quad \text{and} \quad \forall i \in I, u_i \dashrightarrow_r^* V_i. $$

Notice that whereas $\dashrightarrow_r$ reduces finite sums with integer coefficients, $\dashrightarrow_r$ reduces arbitrary sums with arbitrary coefficients.

## 2.3 Linear approximation and the conservativity problems

We recall the definition of the Taylor expansion of $\lambda$-terms, and the approximation theorems it enjoys. Again, a detailed presentation can be found in [31], and in [7] for the adaption to infinitary $\lambda$-calculi. In the latter setting, we shall start with the following unusual definition.

**Definition 10.** The Taylor expansion is the map $\mathcal{T} : \Lambda^{001} \to \mathbb{S}^{\Lambda_r}$ defined by

$$ \mathcal{T}(M) := \sum_{s \in \Lambda_r} \mathcal{T}(M, s) \cdot s, $$

where the coefficient $\mathcal{T}(M, s)$ is defined by induction on $s \in \Lambda_r$ as follows:

$$ \mathcal{T}(x, x) := 1 $$

$$ \mathcal{T}(\lambda x.P, \lambda x.s) := \mathcal{T}(P, s) $$

$$ \mathcal{T}((P)Q, (s)[t_1^{k_1}, \dots, t_m^{k_m}]) := \mathcal{T}(P, s) \times \prod_{i=1}^{m} \frac{\mathcal{T}(Q, t_i)^{k_i}}{k_i!}, \quad \text{the } t_i \text{'s being pairwise distinct} $$

$$ \mathcal{T}(M, s) := 0 \qquad \text{in all other cases.} $$

Let us stress a crucial observation: whenever $s \in |\mathcal{T}(M)|$, the value of $\mathcal{T}(M, s)$ does not depend on $M$, hence $\mathcal{T}(M)$ is uniquely determined by its support [19].

Using the notation from Equation (4), we obtain the following description of the Taylor expansion. This is usually how the definition is presented for finite $\lambda$-terms, but since it is not a valid coinductive definition we had to provide Definition 10 in the infinitary setting.

**Lemma 11** ([7], Corollary 4.7). For all variables $x \in \mathcal{V}$ and terms $P, Q \in \Lambda^{001}$,

$$ \mathcal{T}(x) = x \qquad \mathcal{T}(\lambda x.P) = \lambda x.\mathcal{T}(P) \qquad \mathcal{T}((P)Q) = (\mathcal{T}(P))\mathcal{T}(Q)^{!}, $$

where the operation of **promotion** is defined for all $\mathbf{S} \in \mathbb{S}^{\Lambda_r}$ by $\mathbf{S}^{!} := \sum_{n \in \mathbb{N}} \frac{1}{n!} \cdot [\mathbf{S}]^n$.

We defined a map $\mathcal{T}$ taking $\lambda$-terms to weighted sums of approximants. This induces an approximation of the $\lambda$-calculus, thanks to the following theorems expressing the fact that the reduction of the approximants can simulate the reduction of the approximated term.

**Theorem 12** ([31], Lemma 7.6). For $M, N \in \Lambda$, if $M \dashrightarrow_{\beta}^* N$ then $\mathcal{T}(M) \dashrightarrow_r \mathcal{T}(N)$.

**Theorem 13** ([7], Theorem 4.56). For $M, N \in \Lambda^{001}$, if $M \dashrightarrow_{\beta}^{001} N$ then $\mathcal{T}(M) \dashrightarrow_r \mathcal{T}(N)$.
In particular, the latter theorem encompasses the “Commutation theorem” [19, 18], which is usually presented as the cornerstone of the linear approximation of the λ-calculus: the normal form of $\mathcal{T}(M)$ is equal to the Taylor expansion of the Böhm tree of $M$ (which is a notion of infinitary β-normal form of $M$), i.e. normalisation commutes with approximation<fnref n="1" />.

**► Definition 14.** Let $(A, \to_A)$ and $(B, \to_B)$ be two reduction systems. The latter is an extension of the former if:

1. there is an injection $i: A \hookrightarrow B$,

2. $\to_A$ simulates $\to_B$ through $i$, i.e. $\forall a, a' \in A$, if $a \to_A a'$ then $i(a) \to_B i(a')$. This extension is said to be conservative<fnref n="2" /> if $\forall a, a' \in A$, if $i(a) \to_B i(a')$ then $a \to_A a'$.

Theorems 12 and 13 can be reformulated using this definition, thanks to the fact that $\mathcal{T}: \Lambda^{001} \to \mathbb{S}^{\Lambda_r}$ is injective [8, Lemma 5.18]:

- Theorem 12 tells that $(\mathbb{S}^{\Lambda_r}, \dashv_r)$ simulates $(\Lambda, \dashv_\beta^*)$,

- Theorem 13 tells that $(\mathbb{S}^{\Lambda_r}, \dashv_r)$ simulates $(\Lambda^{001}, \dashv_\beta^{001})$, which leads us to the problems we tackle in this paper.

**▷ Problem 15.** Is $(\mathbb{S}^{\Lambda_r}, \dashv_r)$ conservative wrt. $(\Lambda, \dashv_\beta^*)$?

**▷ Problem 16.** Is $(\mathbb{S}^{\Lambda_r}, \dashv_r)$ conservative wrt. $(\Lambda^{001}, \dashv_\beta^{001})$?

# 3 Conservativity wrt. the finite λ-calculus

In this first section, we give a positive answer to Problem 15:

**► Theorem 17 (conservativity).** For all $M, N \in \Lambda$, if $\mathcal{T}(M) \dashv_r \mathcal{T}(N)$ then $M \dashv_\beta^* N$.

We adapt a proof technique by Kerinec and the second author [24], who used it to prove that the algebraic λ-calculus is a conservative extension of the usual λ-calculus. Their proof relies on a relation $\vdash$, called “mashup” of β-reductions, relating λ-terms (from the “small world”) to their algebraic reducts (in the “big world”). In our setting, $M \vdash s$ when $s$ is an approximant of a reduct of $M$.

**► Definition 18.** The mashup relation $\vdash \subset \Lambda \times \Lambda_r$ is defined by the following rules:

$$ \frac{M \dashv_{\beta}^{*} x}{M \vdash x} \qquad \frac{M \dashv_{\beta}^{*} \lambda x.P \qquad P \vdash s}{M \vdash \lambda x.s} $$

$$ \frac{M \dashv_{\beta}^{*} (P)Q \qquad P \vdash s \qquad Q \vdash \bar{t}}{M \vdash (s) \bar{t}} \qquad \frac{M \vdash t_1 \dots M \vdash t_n}{M \vdash [t_1, \dots, t_n]} $$

It is extended to $\Lambda \times \mathbb{S}^{\Lambda_r}$ by the following rule:

$$ \frac{\forall i \in I, M \vdash s_i}{M \vdash \sum_{i \in I} a_i \cdot s_i} $$

for any index set $I$ and coefficients $a_i \in \mathbb{S}$ such that the sum exists.

<footnote n="1">¹ To be rigorous, Theorem 13 must first be extended to a variant of the β-reduction called β⊥-reduction. We remain allusive here, and refer to [8, 7] for more details.</footnote>

<footnote n="2">² Notice that our definition varies from the one chosen by the *Teresé* [30, § 1.3.21], where the conservativity of $\to_B$ wrt. $\to_A$ is defined as a property of the conversions $=A$ and $=B$ they generate. We prefer to distinguish between a conservative extension of a reduction (“in the small world, the big reduction reduces the same people to the same people”) and a conservative extension of the corresponding conversion.</footnote>
23:8 How to Play the Accordion

**Lemma 19.** For all $M \in \Lambda$, $M \vdash \mathcal{T}(M)$.

**Proof.** Take any $s \in |\mathcal{T}(M)|$. By an immediate induction on $s$, $M \vdash s$ follows from the rules of Definition 18 (where all the assumptions $\to_{\beta}^*$ are just taken to be equalities). ◀

**Lemma 20.** For all $M, N \in \Lambda$ and $S \in \mathbb{S}^{\Lambda_r}$, if $M \to_{\beta}^* N$ and $N \vdash S$ then $M \vdash S$.

**Proof.** Take any $s \in |S|$, then $N \vdash s$. By an immediate induction on $s$, $M \vdash s$ follows from the rules of Definition 18 (where the assumptions $M \to_{\beta}^* \dots$ follow from the corresponding $M \to_{\beta}^* N \to_{\beta}^* \dots$). ◀

**Lemma 21.** For all $M, N \in \Lambda$, $x \in \mathcal{V}$, $s \in \Lambda_r$ and $\bar{t} \in !\Lambda_r$, if $M \vdash s$ and $N \vdash \bar{t}$ then $\forall s' \in |s\langle\bar{t}/x\rangle|$, $M[N/x] \vdash s'$.

**Proof.** Assume $M$ and $N$ are given and show the following equivalent result by induction on $s$: if $M \vdash s$ then for all $\bar{t}$ such that $N \vdash \bar{t}$ and for all $s' \in |s\langle\bar{t}/x\rangle|$, $M[N/x] \vdash s'$. ◀

**Lemma 22.** For all $M \in \Lambda$ and $S, T \in \mathbb{S}^{\Lambda_r}$, if $M \vdash S$ and $S \dashv_r T$ then $M \vdash T$.

**Proof.** Let us first show that for all $M \in \Lambda$ and $s \in \Lambda_r$ and $T \in \mathbb{N}^{(\Lambda_r)}$, if $M \vdash s \dashv_r T$ then $\forall t \in |T|$, $M \vdash t$. We do so by induction on $s \dashv_r T$. When $s = (\lambda x.u) \bar{v}$ is a redex, there exists a derivation:

$$ M \dashv_{\beta}^* (P)Q \quad \frac{\begin{array}{c} P \dashv_{\beta}^* \lambda x.P' \quad P' \vdash u \\ P \vdash \lambda x.u \end{array}}{M \vdash (\lambda x.u) \bar{v}} \quad Q \vdash \bar{v} $$

By Lemma 21 with $P' \vdash u$, $Q \vdash \bar{v}$, for all $t \in |u\langle\bar{v}/x\rangle|$, we obtain $P'[Q/x] \vdash t$. Finally, since $M \to_{\beta}^* (\lambda x.P')Q \to_{\beta} P'[Q/x]$, we conclude by Lemma 20. The other cases of the induction follow immediately by lifting to the context.

As a consequence, we can easily deduce the following steps:

- if $M \vdash s \dashv_r T$ then $M \vdash T$, for all $M \in \Lambda$, $s \in \Lambda_r$ and $T \in \mathbb{N}^{(\Lambda_r)}$,

- if $M \vdash S \dashv_r T$ then $M \vdash T$, for all $M \in \Lambda$ and $S, T \in \mathbb{N}^{(\Lambda_r)}$,

- if $M \vdash S \dashv_r^* T$ then $M \vdash T$, for all $M \in \Lambda$ and $S, T \in \mathbb{N}^{(\Lambda_r)}$, which leads to the result. ◀

Before we state the last lemma of the proof, recall that there is a canonical injection $\lfloor - \rfloor_r : \Lambda \to \Lambda_r$ defined by:

$$ \lfloor x \rfloor_r := x \quad \lfloor \lambda x.P \rfloor_r := \lambda x. \lfloor P \rfloor_r \quad \lfloor (P)Q \rfloor_r := (\lfloor P \rfloor_r) \lfloor \lfloor Q \rfloor \rfloor_r $$

and such that for all $N \in \Lambda$, $\lfloor N \rfloor_r \in |\mathcal{T}(N)|$.

**Lemma 23.** For all $M, N \in \Lambda$, if $M \vdash \mathcal{T}(N)$ then $M \to_{\beta}^* N$.

**Proof.** If $M \vdash \mathcal{T}(N)$, then in particular $M \vdash \lfloor N \rfloor_r$. We proceed by induction on $N$:

- If $N = x$, then $M \vdash x$ so $M \to_{\beta}^* x$ by definition.

- If $N = \lambda x.P'$, then $M \vdash \lambda x. \lfloor P' \rfloor_r$, i.e. there is a $P \in \Lambda$ such that $M \to_{\beta}^* \lambda x.P$ and $P \vdash \lfloor P' \rfloor_r$. By induction, $P \to_{\beta}^* P'$, thus $M \to_{\beta}^* \lambda x.P' = N$.

- If $N = (P')Q'$, then $M \vdash (\lfloor P' \rfloor_r) \lfloor \lfloor Q' \rfloor \rfloor_r$ i.e. there are $P, Q \in \Lambda$ such that $M \to_{\beta}^* (P)Q$, $P \vdash \lfloor P' \rfloor_r$ and $Q \vdash \lfloor \lfloor Q' \rfloor \rfloor_r$. By induction, $P \to_{\beta}^* P'$ and $Q \to_{\beta}^* Q'$, thus $M \to_{\beta}^* (P')Q' = N$. ◀

**Proof of Theorem 17.** Suppose that $\mathcal{T}(M) \dashv_r \mathcal{T}(N)$. By Lemma 19 we obtain $M \vdash \mathcal{T}(M)$, hence by Lemma 22 $M \vdash \mathcal{T}(N)$. We can conclude with Lemma 23. ◀
# 4 Non-conservativity wrt. the infinitary λ-calculus

The previous theorem relied on the excellent properties of the Taylor expansion of finite λ-terms: a single (well-chosen) term $|M|_r \in |T(M)|$ is enough to characterise $M$, and a single (again, well-chosen) sequence of resource reducts of some $s \in |T(M)|$ suffices to characterise any sequence $M \to_*^\beta N$. These properties are not true any more when considering more complicated settings, like the 001-infinitary λ-calculus. This does not only make the “mashup” proof technique fail, but also enables us to give a negative answer to Problem 16.

## 4.1 Failure of the “mashup” technique

Let us first describe where we hit an obstacle if we try to reproduce the proof we have given in the finite setting, which will make clearer the way we later build a counterexample.

First, it is not obvious what the mashup relation should be: we could just use the relation $\vdash$ defined on $\Lambda^{001} \times \Lambda_r$ by the same set of rules as in Definition 18, or define an infinitary mashup $\vdash_{001}$ by the rules

$$ \frac{M \to_{\beta}^{001} x}{M \vdash_{001} x} \qquad \frac{M \to_{\beta}^{001} \lambda x.P \qquad P \vdash_{001} s}{M \vdash_{001} \lambda x.s} $$

$$ \frac{M \to_{\beta}^{001} (P)Q \qquad P \vdash_{001} s \qquad Q \vdash_{001} \bar{t}}{M \vdash_{001} (s) \bar{t}} \qquad \frac{M \vdash_{001} t_1 \dots M \vdash_{001} t_n}{M \vdash_{001} [t_1, \dots, t_n]} $$

and extend it to $S^{\Lambda_r}$ accordingly. In fact, this happens to define the same relation.

**Lemma 24.** For all $M \in \Lambda^{001}$ and $s \in \Lambda_r$, $M \vdash_{001} s$ iff $M \vdash s$.

**Proof.** The inclusion $\vdash \subseteq \vdash_{001}$ is immediate. Let us show the converse. First, observe that the proof of Lemma 20 can be easily extended in order to show that for all $M, N \in \Lambda^{001}$ and $s \in \Lambda_r$, if $M \to_{\beta}^{001} N \vdash_{001} s$ then $M \vdash_{001} s$. Then we proceed by induction on $s$.

- If $M \vdash_{001} x$, then $M \to_{\beta}^{001} x$, i.e. $M \to_*^\beta x$, and finally $M \vdash x$.

- If $M \vdash_{001} \lambda x.u$, then there is a derivation:

$$ \frac{M \to_{\beta}^{*} \lambda x.P \qquad P \to_{\beta}^{001} P' \qquad M \to_{\beta}^{001} \lambda x.P' \qquad P' \vdash_{001} u}{M \vdash_{001} \lambda x.u} $$

Since $P \to_{\beta}^{001} P' \vdash_{001} u$, we have $P \vdash_{001} u$, and by induction on $u$ we obtain $P \vdash u$.

With $M \to_*^\beta \lambda x.P$, this yields $M \vdash \lambda x.u$.

- The case of $M \vdash_{001} (u) \bar{v}$ is similar. ◀

As a consequence, Lemmas 19–22 can be easily extended to $\to_{\beta}^{001}$ and $\vdash_{001}$. We have already explained how the proof of this can be done for Lemma 20; for the other ones, one just needs to observe that the proofs are all by induction on resource terms or on some inductively defined relation, hence replacing $\to_*^\beta$ with $\to_{\beta}^{001}$ does not change anything (and neither does replacing $\vdash$ with $\vdash_{001}$, thanks to Lemma 24).

The failure of the infinitary “mashup” proof occurs in the extension of Lemma 23. Indeed, this proof crucially relies on the existence of an injection $]-\cdot]_r : \Lambda \to \Lambda_r$, whereas for $\Lambda^{001}$ there is only the counterpart $]-\cdot]_{r,-} : \Lambda^{001} \times \mathbb{N} \to \Lambda_r$ defined by
23:10 How to Play the Accordion

$$
\begin{align*}
\lfloor x \rfloor_{r,d} &:= x & \lfloor (P)Q \rfloor_{r,0} &:= (\lfloor P \rfloor_{r,0}) 1 \\
\lfloor \lambda x.P \rfloor_{r,d} &:= \lambda x.\lfloor P \rfloor_{r,d} & \lfloor (P)Q \rfloor_{r,d+1} &:= (\lfloor P \rfloor_{r,d+1}) [\lfloor Q \rfloor_{r,d}].
\end{align*}
$$

Now, if we suppose that $M \vdash \mathcal{T}(N)$ and we want to show that $M \xrightarrow{\beta}^{001} N$, we cannot rely
any more on the fact that $M \vdash [N]_r$, but only on the fact that $\forall d \in \mathbb{N}, M \vdash [N]_{r,d}$. This
makes the induction fail. For instance, for the case where $N$ is an abstraction $\lambda x.P'$, we
obtain a $d$-indexed sequence of derivations

$$
\frac{M \to_{\beta}^{*} \lambda x.P_d \qquad P_d \vdash [P']_{r,d}}{M \vdash [N]_{r,d} = [\lambda x.P']_{r,d}}
$$

but nothing tells us that the terms $P_d$ and reductions $M \to_{\beta}^{*} \lambda x.P_d$ are coherent! This
failure is what enables us to design a counterexample.

4.2 The Accordion

In this section, we define 001-infinitary λ-terms A and Ā and show that they form a counterex-
ample not only to the 001-infinitary counterpart of Lemma 23, but also to the conservativity
property in the infinitary setting.

► **Notation 25.** We denote as follows the usual representation of booleans, an “applicator”
$\langle - \rangle$, and the Church encodings of integers and of the successor function:

$$
T := \lambda x.\lambda y.x \qquad F := \lambda x.\lambda y.y \qquad \langle M \rangle := \lambda b.(b)M
$$

$$
n := \lambda f.\lambda x.(f)^n x \qquad \text{Succ} := \lambda n.\lambda f.\lambda x.(n) f(f)x
$$

► **Definition 26.** The Accordion λ-term is defined as $A := (P)0$, where:

$$
P := (\mathbf{Y}) \lambda\phi.\lambda n. (\langle\mathbf{T}\rangle) ((n)\langle\mathbf{F}\rangle) \mathbf{Q}_{\phi,n} \qquad \mathbf{Q}_{\phi,n} := (\mathbf{Y}) \lambda\psi.\lambda b. ((b)(\phi)(\mathbf{Succ})n) \psi.
$$

$$
\text{We also define } \bar{A} := (\langle T \rangle)(\langle F \rangle)^{\omega}.
$$

Let us show how this term behaves (and why we named it the Accordion). There exist
terms P'' (which is nothing but the first head reduct of P) and Qn (for all n ∈ N) such that
the following reductions hold:

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

This means that:

1. for any $d \in \mathbb{N}$, $A$ reduces to terms $A_d$ that are similar to $\bar{A}$ up to depth $d$ (and, as a consequence, any finite approximant of $\bar{A}$ is a reduct of approximants of $A$);

2. but this is not a valid infinitary reduction because we *need* to reduce a redex at depth 0 to obtain $A_d \xrightarrow{\beta} A_{d+1}$, thus the stratification property (Theorem 4) is violated: the depth of the reduced redexes does not tend to the infinity.
Our definition of A and $\bar{A}$ was entirely guided by this specification. More concretely:

- when fed with a Church integer argument $n$, the term $P''$ produces a term mimicking $\bar{A}$ up to the $n$-th copy of $\langle \mathbf{F} \rangle$, the latter being applied to $\mathbb{Q}_n = \mathbb{Q}_{P'',n}$;

- the applicator $\langle - \rangle$ enforces a kind of call-by-value discipline, giving control to the argument (observe that $(\langle M \rangle)N \to_{\beta} (N)M$);

- $\mathbb{Q}_{P'',n}$ eats up boolean arguments $\mathbf{F}$, until it is fed with a boolean $\mathbf{T}$ (marking the root of the tree), at which point it restores $P''$, applied to the next Church integer.

In particular, this dynamics (A is “stretched” and “compressed” over and over) justifies the name “Accordion”.

To be a counterexample to conservativity, A actually has to satisfy a stronger property: all reduction paths starting from A should have this “accordion” behaviour. A thorough analysis of the dynamics will allow us to establish this, and obtain:

**Theorem 27.** (i) $\mathcal{T}(A) \dashv_r \mathcal{T}(\bar{A})$, but (ii) there is no reduction $A \to_{\beta}^{001} \bar{A}$.

This theorem improves on the results from the first author's PhD thesis [7, Theorem 5.12], where only the qualitative setting was treated (i.e. when $S = \mathbb{B}$). Non-conservativity in the general case was presented as Conjecture 5.15, which is thereby solved.

## 4.3 Proof of the counterexample

In this (highly technical) section, we prove Theorem 27: a reader already satisfied with the above intuitions might prefer to skip it, and jump to Section 5. The key ingredient in the proof are the following well-known notions as well as the associated factorization property, due to Mitschke [28, cor. 5].

**Definition 28.** A $\lambda$-term $M \in \Lambda^{001}$ has two possible head forms:

- either the form $\lambda x_1 \dots \lambda x_m.(y)M_1 \dots M_n$, called head normal form (HNF),

- or the form $\lambda x_1 \dots \lambda x_m.(\lambda x.P)QM_1 \dots M_n$, where $(\lambda x.P)Q$ is called the head redex.

As a consequence, a $\beta$-reduction $M \to_{\beta} N$ reduces:

- either a head redex: it is a head reduction, denoted by $M \to_h N$,

- or any other redex: it is an internal reduction, denoted by $M \to_i N$.

**Lemma 29 (head-internal decomposition).** For all $M, N \in \Lambda$ such that $M \to_{\beta}^* N$, there exists an $M' \in \Lambda$ such that $M \to_h^* M' \to_i^* N$.

Let us also introduce some abbreviations<fnref n="3" />:

$$P' := \lambda\phi.\lambda n. (\langle T \rangle) ((n)\langle F \rangle) \mathbb{Q}_{\phi,n} \qquad P'' := (\lambda x. (P')(x)x) \lambda x. (P')(x)x \qquad \mathbb{Q}_n := \mathbb{Q}_{P'',(\text{Succ})^n 0}$$

$$\mathbb{Q}'_n := \lambda\psi.\lambda b. ((b)(P'')(\text{Succ})^{n+1} 0) \psi \qquad \mathbb{Q}''_n := (\lambda x.(\mathbb{Q}'_n)(x)x) \lambda x.(\mathbb{Q}'_n)(x)x.$$

Using these definitions, Figure 1 describes the head reduction path starting from A.

**Proof of Theorem 27, item (i).** For all $d \in \mathbb{N}$, we define:

- $\bar{A}_d := (\langle T \rangle)(\langle F \rangle)^d \mathbb{Q}_n$. As a consequence of the reduction described in Figure 1, in particular its step 7, there are reductions $A \to_{\beta}^* \bar{A}_0 \to_{\beta}^* \bar{A}_1 \to_{\beta}^* \bar{A}_2 \to_{\beta}^* \dots$ By Theorem 12, we obtain

$$\mathcal{T}(A) \dashv_r \mathcal{T}(\bar{A}_0) \dashv_r \mathcal{T}(\bar{A}_1) \dashv_r \mathcal{T}(\bar{A}_2) \dashv_r \dots \qquad (29)$$

<footnote n="3">³ Notice that the $\mathbb{Q}_n$ we define here are slightly different from those in the example reduction described above, but they play the same role.</footnote>
23:12 How to Play the Accordion

The first step is:

$$
\mathbf{A} = ((\mathbf{Y})\mathbf{P}')_0 \to_h (\mathbf{P}'')_0
$$

Then, for each $n \in \mathbb{N}$, we do the following head reduction steps:

$$
(\mathbf{P}')(\mathbf{S}\mathbf{u})^{n}{}_{0}
$$

$$
\to_h ( (\mathbf{P}')\mathbf{P}'')^{n}{}_{0} \quad (5)
$$

$$
\to_h (\lambda n. (\langle \mathbf{T} \rangle) ((n)\langle \mathbf{F} \rangle) \mathbf{Q}_{\mathbf{p}''}, n) (\mathbf{S}\mathbf{u})^{n}{}_{0} \quad (6)
$$

$$
\to_h ((\langle \mathbf{T} \rangle) (((\mathbf{S}\mathbf{u})^{n}{}_{0}) \langle \mathbf{F} \rangle) \mathbf{Q}_{n}) \quad (7)
$$

$$
\to_h (\mathbf{S}\mathbf{u})^{n}{}_{0} \langle \mathbf{F} \rangle \mathbf{Q}_{n} \mathbf{T} \quad (8)
$$

$$
\to_h (\lambda f. \lambda x. ((((\mathbf{S}\mathbf{u})^{n-1}{}_{0})f)(f)x) \langle \mathbf{F} \rangle) \mathbf{Q}_{n} \mathbf{T} \quad (9)
$$

$$
\to_h (\lambda x. ((((\mathbf{S}\mathbf{u})^{n-1}{}_{0})\langle \mathbf{F} \rangle)((\langle \mathbf{F} \rangle)x) \mathbf{Q}_{n}) \mathbf{T} \quad (10)
$$

$$
\to_h ((\mathbf{S}\mathbf{u})^{n-1}{}_{0} \langle \mathbf{F} \rangle (\langle \mathbf{F} \rangle) \mathbf{Q}_{n}) \mathbf{T} \quad (11)
$$

and by repeating steps (9) to (11):

$$
\to_h^* ((0)\langle \mathbf{F} \rangle ((\mathbf{F})^n \mathbf{Q}_n) \mathbf{T}) \quad (12)
$$

$$
\to_h ((\lambda x.x)((\langle \mathbf{F} \rangle)^n \mathbf{Q}_n) \mathbf{T}) \quad (13)
$$

$$
\to_h ((\lambda b.(b)\mathbf{F})((\langle \mathbf{F} \rangle)^{n-1} \mathbf{Q}_n) \mathbf{T}) \quad (14)
$$

$$
\to_h ((\langle \mathbf{F} \rangle)^{n-1} \mathbf{Q}_n) \mathbf{F} \mathbf{T} \quad (15)
$$

and by repeating step (15):

$$
\to_h^* (\underbrace{(\mathbf{Y})\mathbf{Q}'_n}_{\text{n times}} \mathbf{F} \dots \mathbf{F} \mathbf{T}) \quad (16)
$$

$$
\to_h (\mathbf{Q}''_{n}) \mathbf{F} \dots \mathbf{F} \mathbf{T} \quad (17)
$$

$$
\to_h (\mathbf{Q}'_n \mathbf{Q}''_n) \mathbf{F} \dots \mathbf{F} \mathbf{T} \quad (18)
$$

$$
\to_h (\lambda b. ((b)(\mathbf{P}'') (\mathbf{S}\mathbf{u})^{n+1}{}_{0}) \mathbf{Q}''_{n}) \mathbf{F} \dots \mathbf{F} \mathbf{T} \quad (19)
$$

$$
\to_h \left( \left( \left( \lambda x. \lambda y. y \right) (\mathbf{P}'') (\mathbf{S}\mathbf{u})^{n+1}{}_{0} \right) \mathbf{Q}''_{n} \right) \underbrace{\mathbf{F} \dots \mathbf{F} \mathbf{T}}_{\text{n-1 times}} \quad (20)
$$

$$
\to_h (\langle \lambda y. y \rangle \mathbf{Q}''_{n}) \mathbf{F} \dots \mathbf{F} \mathbf{T} \quad (21)
$$

$$
\to_h (\mathbf{Q}''_{n}) \mathbf{F} \dots \mathbf{F} \mathbf{T} \quad (22)
$$

and by repeating steps (18) to (22):

$$
\to_h^* (\mathbf{Q}''_{n}) \mathbf{T} \quad (23)
$$

$$
\to_h (\mathbf{Q}'_n \mathbf{Q}''_n) \mathbf{T} \quad (24)
$$

$$
\to_h (\lambda b. ((b)(\mathbf{P}'') (\mathbf{S}\mathbf{u})^{n+1}{}_{0}) \mathbf{Q}''_{n}) \mathbf{T} \quad (25)
$$

$$
\to_h ((\lambda x. \lambda y. x)(\mathbf{P}'') (\mathbf{S}\mathbf{u})^{n+1}{}_{0}) \mathbf{Q}''_{n} \quad (26)
$$

$$
\to_h (\lambda y. (\mathbf{P}'') (\mathbf{S}\mathbf{u})^{n+1}{}_{0}) \mathbf{Q}''_{n} \quad (27)
$$

$$
\to_h (\mathbf{P}'') (\mathbf{S}\mathbf{u})^{n+1}{}_{0} \quad (28)
$$

which brings us back to step (5).

Figure 1 Exhaustive head reduction of the Accordion. We highlight the fired head redexes.

■ $\mathcal{T}'_d(\bar{\mathbf{A}}) := \mathcal{T}((\langle \mathbf{T} \rangle)(\langle \mathbf{F} \rangle)^d \perp)$, where $\perp$ is a constant such that $\mathcal{T}(\perp) := 0$ (this is just a trick to “cut” the Taylor expansion at some point), as well as

$$
\left\{
\begin{aligned}
\mathcal{T}_0(\bar{\mathbf{A}}) &:= \mathcal{T}'_0(\bar{\mathbf{A}}) \\
\mathcal{T}_{d+1}(\bar{\mathbf{A}}) &:= \mathcal{T}'_{d+1}(\bar{\mathbf{A}}) - \mathcal{T}'_d(\bar{\mathbf{A}}) = \sum_{s \in |\mathcal{T}'_{d+1}(\bar{\mathbf{A}})| \setminus |\mathcal{T}'_d(\bar{\mathbf{A}})|} \mathcal{T}(s, \bar{\mathbf{A}}) \cdot s.
\end{aligned}
\right.
$$

By construction (using the observation that the coefficient of $s \in |\mathcal{T}(M)|$ does not depend on $M$), we obtain:

$$
\mathcal{T}(\bar{\mathbf{A}}) = \mathcal{T}_d(\bar{\mathbf{A}}) + \mathbf{S}_d, \text{ for some } \mathbf{S}_d \text{ such that } |\mathcal{T}_d(\bar{\mathbf{A}})| \cap |\mathbf{S}_d| = \emptyset \quad (30)
$$

$$
\mathcal{T}(\bar{\mathbf{A}}) = \sum_{n \in \mathbb{N}} \mathcal{T}_d(\bar{\mathbf{A}}) \qquad (31)
$$

Before we use this material to prove the theorem, we need to make the following crucial observation:

$$
\forall s \in \mathcal{T}_d(\bar{\mathbf{A}}), \forall k > 0, \exists t \in \mathcal{T}_{d+k}(\bar{\mathbf{A}}), s \xrightarrow{r} t + T \quad (32)
$$

for some $T \in \mathbb{N}^{(\Lambda_r)}$. This is due to the fact that terms in $\mathcal{T}(\bar{\mathbf{A}})$ cannot see their (applicative) depth increase through resource reduction.

Now we start with Equation (29), having $\mathcal{T}(\mathbf{A}) \xrightarrow{\to_r} \mathcal{T}(\bar{\mathbf{A}}_0) \xrightarrow{\to_r} \mathcal{T}(\bar{\mathbf{A}}_1)$. Thanks to Equation (30), this can be rewritten as $\mathcal{T}(\mathbf{A}) \xrightarrow{\to_r} \mathcal{T}_0(\bar{\mathbf{A}}) + \mathbf{S}_0 \xrightarrow{\to_r} \mathcal{T}_1(\bar{\mathbf{A}}) + \mathbf{S}_1$. Equation (32) allows to say that only $\mathbf{S}_0$ contributes to $\mathcal{T}_1(\bar{\mathbf{A}})$ in the second reduction. If we leave $\mathcal{T}_0(\bar{\mathbf{A}})$ untouched and only reduce $\mathbf{S}_0$, we obtain $\mathcal{T}_0(\bar{\mathbf{A}}) + \mathbf{S}_0 \xrightarrow{\to_r} \mathcal{T}_0(\bar{\mathbf{A}}) + \mathcal{T}_1(\bar{\mathbf{A}}) + \mathbf{S}'_1$ for some $\mathbf{S}'_1$ that is part of $\mathbf{S}_1$. If we keep applying Equations (30) and (32) and we iterate the process, we obtain:
$$ \mathcal{T}(\mathbf{A}) \dashrightarrow_{\mathbf{r}} \mathcal{T}_0(\bar{\mathbf{A}}) + \mathbf{S}_0 \dashrightarrow_{\mathbf{r}} \mathcal{T}_0(\bar{\mathbf{A}}) + \mathcal{T}_1(\bar{\mathbf{A}}) + \mathbf{S}'_1 \dashrightarrow_{\mathbf{r}} \dots \dashrightarrow_{\mathbf{r}} \sum_{d=0}^{N} \mathcal{T}_d(\bar{\mathbf{A}}) + \mathbf{S}'_N \quad (33) $$

for all $N \in \mathbb{N}$. For each $s \in |\mathcal{T}(\mathbf{A})|$, this can be turned into$^4$:

$$ s \dashrightarrow_{\mathbf{r}}^{*} T_{s,0} + S_{s,0} \dashrightarrow_{\mathbf{r}}^{*} T_{s,0} + T_{s,1} + S_{s,1} \dashrightarrow_{\mathbf{r}}^{*} \dots \dashrightarrow_{\mathbf{r}}^{*} \sum_{d=0}^{N} T_{s,d} + S_{s,N} \quad (34) $$

for some $T_{s,d}, S_{s,d} \in \mathbb{N}^{(\Lambda_r)}$ satisfying $\mathcal{T}_d(\bar{\mathbf{A}}) = \sum_{s \in \Lambda_r} \mathcal{T}(s, \mathbf{A}) \cdot T_{s,d}$. In fact:

- There are only finitely many $d$'s such that $T_{s,d} \neq 0$ (this is due to the fact that a resource terms has only finitely many reducts [31, Lemma 3.13]).

- A has no head normal form as demonstrated in Figure 1, which entails that $\mathcal{T}(\mathbf{A}) \dashrightarrow_{\mathbf{r}} 0$ [8, Theorem 5.6]. Since $\mathbf{S}'_d$ only contains reducts of terms in $\mathcal{T}(\mathbf{A})$, this means that we can reduce $\mathbf{S}'_N \dashrightarrow_{\mathbf{r}}^*$ 0.

As a consequence, $s \dashrightarrow_{\mathbf{r}}^* \sum_{d \in \mathbb{N}} T_{s,d}$ and we can conclude:

$$ \mathcal{T}(\mathbf{A}) = \sum_{s \in \Lambda_r} \mathcal{T}(s, \mathbf{A}) \cdot s \dashrightarrow_{\mathbf{r}} \sum_{s \in \Lambda_r} \mathcal{T}(s, \mathbf{A}) \cdot \sum_{d \in \mathbb{N}} T_{s,d} = \sum_{d \in \mathbb{N}} \mathcal{T}_d(\bar{\mathbf{A}}) = \mathcal{T}(\bar{\mathbf{A}}) $$

by Equation (31).

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

**Proof of Theorem 27, item (ii).** We suppose that there is a reduction $\mathbf{A} \dashrightarrow_{\beta}^{001} \bar{\mathbf{A}}$ and we show that this leads to a contradiction. By Theorem 4 and Lemma 29, there exists respectively a sequence of terms $\mathbf{A}_d \in \Lambda$ and a term $\mathbf{A}'_0 \in \Lambda$ such that there are reductions

$$ \mathbf{A} \dashrightarrow_{h}^{*} \mathbf{A}'_{0} \dashrightarrow_{i}^{*} \mathbf{A}_{1} \dashrightarrow_{\beta \geq 1}^{*} \mathbf{A}_{d} \dashrightarrow_{\beta \geq d}^{001} \bar{\mathbf{A}}. $$

$\mathbf{A}'_0$ and $\bar{\mathbf{A}}$ must have the same head form, i.e. there must be $M, N \in \Lambda$ such that $\mathbf{A}'_0 = (\lambda b.M)N$. The exhaustive description of the head reducts of $\mathbf{A}$ detailed in Figure 1 allows to observe that this only happens in four cases (corresponding to steps 6, 7, 25 and 27 in Figure 1):

$$ \begin{array}{c} (s_{s,d,i})_{\substack{s \in \Lambda_r \\ 1 \leq i \leq n_{s,d}}} \underset{1 \leq i \leq n_{s,d}}{\overset{\mathbf{S}'_d}{\rightleftharpoons}}^{*} (T'_{s,d,i} + S'_{s,d,i})_{\substack{s \in \Lambda_r \\ 1 \leq i \leq n_{s,d}}} \\ \sum_{s \in \Lambda_r} \mathcal{T}(s, \mathbf{A}) \cdot \underbrace{\sum_{i=1}^{n_{s,d}} s_{s,d,i}}_{\mathbf{S}'_d} \underset{\mathbf{S}'_d}{\overset{\mathbf{S}'_d}{\rightleftharpoons}}^{*} \sum_{s \in \Lambda_r} \mathcal{T}(s, \mathbf{A}) \cdot \underbrace{\left( \sum_{i=1}^{n_{s,d}} T_{s,d+1,i} + \sum_{i=1}^{n_{s,d}} S_{s,d+1,i} \right)}_{\mathcal{T}_{d+1}(\bar{\mathbf{A}}) + \mathbf{S}'_{d+1}} \\ \sum_{s \in \Lambda_r} \mathcal{T}(s, \mathbf{A}) \cdot \underbrace{\sum_{i=1}^{n_{s,d}} s_{s,d,i}}_{\mathbf{S}'_d} \underset{\mathbf{S}'_d}{\overset{\mathbf{S}'_d}{\rightleftharpoons}}^{*} \sum_{s \in \Lambda_r} \mathcal{T}(s, \mathbf{A}) \cdot \underbrace{\left( \sum_{i=1}^{n_{s,d}} T_{s,d+1,i} + \sum_{i=1}^{n_{s,d}} S_{s,d+1,i} \right)}_{\mathcal{T}_{d+1}(\bar{\mathbf{A}}) + \mathbf{S}'_{d+1}} \end{array} $$

<footnote>$^4$ This inference might not be possible for an arbitrary reduction sequence, because the obtained reductions (34) occur in $\mathbb{N}^{(\Lambda_r)}$ (with integer coefficients only) while the original reductions (33) occur in $\mathbb{S}^{\Lambda_r}$ (possibly with rational coefficients): if for some $s \in \mathbf{S}'_d$ the original reduction $\mathbf{S}'_d \dashrightarrow_{\mathbf{r}} \mathcal{T}_{d+1}(\bar{\mathbf{A}}) + \mathbf{S}'_{d+1}$ consists in doing $s = \frac{1}{3}s + \frac{2}{3}s \dashrightarrow_{\mathbf{r}} \frac{1}{3}S' + \frac{2}{3}S''$, we will not be able to retrieve a reduction $s \dashrightarrow_{\mathbf{r}}^* \dots$ of the desired shape.</footnote>

<footnote>But the reductions in $\mathbb{S}^{\Lambda_r}$ we consider are not arbitrary: Equation (29) was obtained by simulating a sequence of $\beta$-reductions via Theorem 12, so that we can apply uniformity. With the notations to be introduced in Section 5, using Corollary 34 we obtain reductions $\mathbf{S}'_d \dashrightarrow_{\mathbf{r}}^* \mathcal{T}_{d+1}(\bar{\mathbf{A}}) + \mathbf{S}'_{d+1}$ instead of $\mathbf{S}'_d \dashrightarrow_{\mathbf{r}} \mathcal{T}_{d+1}(\bar{\mathbf{A}}) + \mathbf{S}'_{d+1}$. These reductions can only be derived as follows:</footnote>

<footnote>the premise of which allows to build a reduction $S_{s,d} \dashrightarrow_{\mathbf{r}}^* T_{s,d+1} + S_{s,d+1}$.</footnote>
23:14 How to Play the Accordion

$$
1. A'_{0} = (\lambda n. (\langle T \rangle) ((n)\langle F \rangle) Q_{p'',n}) (\mathrm{Succ})^{n0},
$$

$$
2. A'_{0} = (\langle T \rangle) (((\mathrm{Succ})^{n0} \langle F \rangle) Q_{n},
$$

$$
3. A'_{0} = (\lambda b. ((b)(P'')(\mathrm{Succ})^{n+1}0) Q''_{n}) T,
$$

$$
4. A'_{0} = (\lambda y. (P'') (\mathrm{Succ})^{n+1} 0) Q''_{n},
$$

for some $n \in \mathbb{N}$ (in the following, $n$ denotes this specific integer appearing in $A'_0$). In particular,
for one of these possible values of $A'_0$ there must be a reduction

$$
A'_{0} \xrightarrow{i}^{*} A_{n+4} \xrightarrow{\beta \ge n+4}^{001} \bar{A}.
$$

Since $A_{n+4}$ and $\bar{A}$ are identical up to applicative depth $n+3$, we can write $A_{n+4} =$
$(\langle T \rangle)(\langle F \rangle)^{n+1}M$ for some $M \in \Lambda$ such that $M \xrightarrow{001} \beta (\langle F \rangle)^\omega$ (we need to go up to depth $n+3$
since $\langle T \rangle$ and $\langle F \rangle$ are themselves of applicative depth 2). Finally, there must be a reduction

$$
A'_{0} \xrightarrow{i}^{*} (\langle T \rangle)(\langle F \rangle)^{n+1} M.
$$

For each of the possible cases for $A'_0$, let us show that this is impossible. The easy cases are:

Case 1, step (6) Such a reduction would imply that (Succ)$^{n0} \xrightarrow{\beta} (\langle F \rangle)^{n+1} M$. However (Succ)$^{n0} \xrightarrow{\beta} n$, which is in $\beta$-normal form, while $(\langle F \rangle)^{n+1} M$ has no normal form. We conclude by confluence of the finite $\lambda$-calculus.

Case 3, step (25) Immediate because T is in normal form.

Case 4, step (27) Such a reduction would imply that $\lambda y.(P'')(\mathrm{Succ})^{n+1}0 \xrightarrow{\beta} \langle T \rangle = \lambda y.(y)T$, and therefore that $(P'')(\mathrm{Succ})^{n+1}0$ has a HNF $(y)T$. This is impossible, as detailed in the exhaustive head reduction of $\mathbf{A}$ in Figure 1.

The remaining case concerns the reduct ((⟨T⟩) (((Succ)ⁿ₀ ⟨F⟩) Qₙ. It is the only “non-
degenerate” one, in the sense that it is where the accordion-like behaviour of A is illustrated:
the sub-term ⟨T⟩ here is really “the same” as the one appearing at the root of A but we need
to reduce this sub-term at some point (i.e. to “compress” the Accordion). Thus there can be
no 001-infinitary reduction towards A. The formal proof of this case, i.e. of the impossibility
of (Succ)ⁿ₀⟨F⟩Qₙ →
\*_{β} ⟨F⟩)ⁿ+¹M, is given by Lemma 31 below.

◀

► Lemma 30. For all $k \in \mathbb{N}$, $n \in \mathbb{N}$ and $M \in \Lambda$, there is no reduction

$$
(\langle \mathbf{F} \rangle)^k Q_n \xrightarrow{\beta} (\langle \mathbf{F} \rangle)^{k+1} M.
$$

Proof. We proceed by induction on $k$. First, take $k=0$ and suppose there is a reduction
$Q_n \xrightarrow{\beta} (\langle F \rangle)M$. By Lemma 29, there are $R, R' \in \Lambda$ such that

$$
Q_n \xrightarrow{R'} (\lambda b.R)R' \xrightarrow{i}^* (\langle F \rangle)M = (\lambda b.(b)F)M.
$$

An exhaustive head reduction of $Q_n$ gives the possible values of $R$ and $R'$:

$$
\begin{align*}
Q_n &= (Y)Q'_n \\
    &\rightarrow_h (\lambda x. (Q'_n)(x)x) \quad \lambda x. (Q'_n)(x)x \\
    &\rightarrow_h (\lambda \psi. \lambda b. ((b)(P'')(\mathrm{Succ})^{n+1}0) \psi) \quad Q''_n \\
    &\rightarrow_h \lambda b. ((b)(P'')(\mathrm{Succ})^{n+1}0) \quad Q''_n,
\end{align*}
$$

the last reduct being in HNF, which leaves only the first three possibilities. In any of those
three cases, $R \xrightarrow{\beta} (b)F$ (modulo renaming of $b$ by $\alpha$-conversion) is impossible by immediate
arguments, so that $(\lambda b.R)R' \xrightarrow{i} ((\langle F \rangle)M$ cannot hold.
If $k \ge 1$, let us again suppose that there is a reduction $(\langle \mathbf{F} \rangle)^k \mathbf{Q}_n \xrightarrow{\beta} (\langle \mathbf{F} \rangle)^{k+1} M$. Lemma 29 states that there are $R, R' \in \Lambda$ such that

$$ (\langle \mathbf{F} \rangle)^k \mathbf{Q}_n \xrightarrow{h} (\lambda b.R) R' \xrightarrow{i} (\lambda b.(b)\mathbf{F}) (\langle \mathbf{F} \rangle)^k M. $$

An exhaustive head reduction of $(\langle \mathbf{F} \rangle)^k \mathbf{Q}_n$ gives the possible values of $R$ and $R'$ (we write only the reduction steps corresponding to the well-formed reducts – see the details in the detailed head reduction of $\mathbf{A}$, steps (15) and following):

$$ \begin{align*} (\langle \mathbf{F} \rangle)^k \mathbf{Q}_n &= (\lambda b.(b)\mathbf{F}) (\langle \mathbf{F} \rangle)^{k-1} \mathbf{Q}_n \\ &\xrightarrow{h} (\lambda b.((b)(\mathbf{P}'')(\mathbf{Succ}))^{n+1} 0) \mathbf{Q}_n'' \mathbf{F} \\ &\xrightarrow{h} (\lambda y.y) \mathbf{Q}_n'' \\ &\xrightarrow{h} \mathbf{Q}_n'' \end{align*} $$

In the first case, a reduction $(\lambda b.(b)\mathbf{F}) (\langle \mathbf{F} \rangle)^{k-1} \mathbf{Q}_n \xrightarrow{i} (\lambda b.(b)\mathbf{F}) (\langle \mathbf{F} \rangle)^k M$ is impossible because it would imply that $(\langle \mathbf{F} \rangle)^{k-1} \mathbf{Q}_n \xrightarrow{\beta} (\langle \mathbf{F} \rangle)^k M$, which is impossible by induction. The second and third cases are impossible by immediate arguments; the fourth case has already been explored $(\mathbf{Q}_n''$ is exactly the term from the second line of the reduction of $\mathbf{Q}_n$ above). $\quad$

**Lemma 31.** For all $n \in \mathbb{N}$, $k \in [0, n]$ and $M \in \Lambda$, there is no reduction:

$$ (\mathbf{Succ})^{n-k} 0 \langle \mathbf{F} \rangle (\langle \mathbf{F} \rangle)^k \mathbf{Q}_n \xrightarrow{\beta} (\langle \mathbf{F} \rangle)^{n+1} M. $$

**Proof.** We proceed by induction on $n-k$. The base case is $k=n$: if there is a reduction $(0) \langle \mathbf{F} \rangle (\langle \mathbf{F} \rangle)^n \mathbf{Q}_n \xrightarrow{\beta} (\langle \mathbf{F} \rangle)^{n+1} M$, then by Lemma 29 there are terms $R, R' \in \Lambda$ such that

$$ (0) \langle \mathbf{F} \rangle (\langle \mathbf{F} \rangle)^n \mathbf{Q}_n \xrightarrow{h} (\lambda b.R) R' \xrightarrow{i} (\lambda b.(b)\mathbf{F}) (\langle \mathbf{F} \rangle)^n M. $$

Observe that

$$ (0) \langle \mathbf{F} \rangle (\langle \mathbf{F} \rangle)^n \mathbf{Q}_n \xrightarrow{h} (\lambda x.x) (\langle \mathbf{F} \rangle)^n \mathbf{Q}_n \xrightarrow{h} (\langle \mathbf{F} \rangle)^n \mathbf{Q}_n $$

hence, because $\lambda x.x$ is in $\beta$-normal form and by Lemma 30, we reach a contradiction.

If $k < n$ and there is a reduction $(\mathbf{Succ})^{n-k} 0 \langle \mathbf{F} \rangle (\langle \mathbf{F} \rangle)^k \mathbf{Q}_n \xrightarrow{\beta} (\langle \mathbf{F} \rangle)^{n+1} M$, then again by Lemma 29 there are terms $R, R' \in \Lambda$ such that

$$ (\mathbf{Succ})^{n-k} 0 \langle \mathbf{F} \rangle (\langle \mathbf{F} \rangle)^k \mathbf{Q}_n \xrightarrow{h} (\lambda b.R) R' \xrightarrow{i} (\lambda b.(b)\mathbf{F}) (\langle \mathbf{F} \rangle)^n M. $$

Observe that

$$ \begin{align*} (\mathbf{Succ})^{n-k} 0 \langle \mathbf{F} \rangle (\langle \mathbf{F} \rangle)^k \mathbf{Q}_n &\xrightarrow{h} (\lambda f.\lambda x.(\mathbf{Succ})^{n-k-1} 0 f(f)x) \langle \mathbf{F} \rangle (\langle \mathbf{F} \rangle)^k \mathbf{Q}_n \\ &\xrightarrow{h} (\lambda x.(\mathbf{Succ})^{n-k-1} 0 \langle \mathbf{F} \rangle (\langle \mathbf{F} \rangle)x) (\langle \mathbf{F} \rangle)^k \mathbf{Q}_n \\ &\xrightarrow{h} (\mathbf{Succ})^{n-k-1} 0 \langle \mathbf{F} \rangle (\langle \mathbf{F} \rangle)^{k+1} \mathbf{Q}_n \end{align*} $$

The first reduct does not have the expected head form. In the second case, $(\lambda b.R)R' \xrightarrow{i} (\lambda b.(b)\mathbf{F}) (\langle \mathbf{F} \rangle)^n M$ would imply that $(\langle \mathbf{F} \rangle)^k \mathbf{Q}_n \xrightarrow{\beta} (\langle \mathbf{F} \rangle)^n M$, which is impossible by Lemma 30 because $k < n$. In the third case, apply the induction hypothesis. $\quad$
## 5 The missing ingredient: Uniformity

The fact that the simulation of $\xrightarrow{\beta}^{001}$ by $\xrightarrow{\r}$ via the Taylor expansion is not conservative confirms that the pointwise reduction $\xrightarrow{\r}$, even if needed in order to express the pointwise normal form of a sum through the resource reduction, weakens the dynamics of the $\beta$-reduction by allowing to reduce resource approximants along reductions paths that do not correspond to an actual reduction of the approximated term. As already underlined by Ehrhard and Regnier in their seminal work [19], uniformity is what gives the linear approximation all its robustness; this will also be the case for our study.

**► Definition 32.** The relation $\sqsubseteq \subset (!)\Lambda_r \times (!)\Lambda_r$ of coherence is defined by the rules:

$$ \frac{x \sqsubseteq x}{\lambda x.s \sqsubseteq \lambda x.s'} \qquad \frac{s \sqsubseteq s' \quad \bar{s} \sqsubseteq \bar{s'}}{(s) \bar{t} \sqsubseteq (s) \bar{t}'} $$

$$ \frac{\forall i \in \{1, \dots, m\}, \forall j \in \{1, \dots, n\}, t_i \sqsubseteq t'_j}{[t_1, \dots, t_m] \sqsubseteq [t'_1, \dots, t'_n]} (m, n \in \mathbb{N}) $$

For $\mathbf{S}, \mathbf{T} \in \mathbb{S}^{(!)\Lambda_r}$, we write $\mathbf{S} \sqsubseteq \mathbf{T}$ whenever $\forall s \in |\mathbf{S}|, \forall t \in |\mathbf{T}|, s \sqsubseteq t$.

**► Definition 33.** Given an index set $I$ and a depth $d \in \mathbb{N}$, we define a relation $\overset{\r}{\sqsubseteq}_d \subset ((!)\Lambda_r)^I \times (\mathbb{N}^{((!)\Lambda_r)})^I$ by the following rules:

$$ \frac{\forall i, j, s_i \sqsubseteq s_j \quad \forall i, j, \bar{t}_i \sqsubseteq \bar{t}_j}{((\lambda x.s_i) \bar{t}_i)_{i \in I} \overset{\r}{\sqsubseteq} \bar{t}_i} \qquad \frac{(s_i)_{i \in I} \overset{\r}{\sqsubseteq} \bar{t}_i}{(\lambda x.s_i)_{i \in I} \overset{\r}{\sqsubseteq} \bar{t}_i} $$

$$ \frac{(s_i)_{i \in I} \overset{\r}{\sqsubseteq} \bar{t}_i \ge d (S'_i)_{i \in I} \quad \forall i, j, \bar{t}_i \sqsubseteq \bar{t}_j}{((s_i) \bar{t}_i)_{i \in I} \overset{\r}{\sqsubseteq} \bar{t}_i \ge d ((S'_i) \bar{t}_i)_{i \in I}} \qquad \frac{(t_{i,j})_{i \in I} \overset{\r}{\sqsubseteq} \bar{t}_i \ge d (T'_{i,j})_{i \in I} \quad \forall 1 \le j \le k_i}{([t_{i,1}, \dots, t_{i,k_i}])_{i \in I} \overset{\r}{\sqsubseteq} \bar{t}_i \ge d ([T'_{i,1}, \dots, T'_{i,k_i}])_{i \in I}} $$

$$ \frac{\forall i, j, s_i \sqsubseteq s_j \quad (\bar{t}_i)_{i \in I} \overset{\r}{\sqsubseteq} \bar{t}_i \ge 0 (\bar{T}'_i)_{i \in I}}{((s_i) \bar{t}_i)_{i \in I} \overset{\r}{\sqsubseteq} \bar{t}_i \ge 0 ((s_i) \bar{T}'_i)_{i \in I}} \qquad \frac{\forall i, j, s_i \sqsubseteq s_j \quad (\bar{t}_i)_{i \in I} \overset{\r}{\sqsubseteq} \bar{t}_i \ge d (\bar{T}'_i)_{i \in I}}{((s_i) \bar{t}_i)_{i \in I} \overset{\r}{\sqsubseteq} \bar{t}_i \ge d+1 ((s_i) \bar{T}'_i)_{i \in I}} $$

The relation $\overset{\r}{\sqsubseteq}_d \subset \mathbb{S}^{(!)\Lambda_r} \times \mathbb{S}^{(!)\Lambda_r}$ of uniform resource reduction at minimum depth $d$ is defined by

$$ \frac{(u_i)_{i \in I} \overset{\r}{\sqsubseteq} \bar{t}_i \ge d (U'_i)_{i \in I}}{\sum_{i \in I} a_i u_i \overset{\r}{\sqsubseteq} \bar{t}_i \ge d \sum_{i \in I} a_i U'_i} $$

We denote $\overset{\r}{\sqsubseteq}_{\ge 0}$ and $\overset{\r}{\sqsubseteq}_{\ge 0}$ simply by $\overset{\r}{\sqsubseteq}$ and $\overset{\r}{\sqsupseteq}$, and call the latter uniform resource reduction.

The intuition behind $\overset{\r}{\sqsubseteq}$ is that:

- it can only reduce “uniform” sums, i.e. sums containing resource terms that all have the same shape (formally, sums $\mathbf{S}$ such that $\mathbf{S} \sqsubseteq \mathbf{S}$),

- each reduction step of a sum is a “bundle” of resource reduction steps occurring at the same address in the elements of the sum ($\overset{\r}{\sqsubseteq}$ is an inductive reformulation of Midez' $\Gamma$-reduction [27]).
This allows to capture only the reductions of some $\mathcal{T}(M)$ that correspond to a $\beta$-reduction of $M$, as we will formally show. In fact, all the pointwise reductions $\to_r$ occurring in the proof of Theorem 12 are already instances of the particular case $\to_r^*$, hence the following reformulation.

**Corollary 34 (of Theorem 12; [7], Lemma 4.50).** For all $M, N \in \Lambda$, if $M \to_{\beta \ge d} N$ then $\mathcal{T}(M) \to_{r \ge d} \mathcal{T}(N)$.

Let us show how this property can be used to build a conservative simulation of $\to_{\beta}^{001}$. The simulating reduction needs to be:

- a restriction of $\to_r$, because we want to eliminate the non-uniform reductions that cannot be turned into actual $\beta$-reductions,

- an extension of $\to_r^*$, because we want to be able to simulate not only finite, but also infinitary reductions.

The way we proceed is guided by the stratification property (Theorem 4).

**Notation 35.** The (applicative) depth of a resource term is the integer defined by

$$ \mathrm{depth}(x) := 0 $$

$$ \mathrm{depth}((s) \bar{t}) := \max (\mathrm{depth}(s), 1 + \mathrm{depth}(\bar{t})) $$

$$ \mathrm{depth}(\lambda x.s) := \mathrm{depth}(s) $$

$$ \mathrm{depth}([t_1, \dots, t_n]) := \max_{1 \le i \le n} \mathrm{depth}(t_i). $$

For all $\sum_{i \in I} a_i \cdot s_i \in \mathbb{S}^{\Lambda_r}$ and integer $d \in \mathbb{N}$, we write $\left(\sum_{i \in I} a_i \cdot s_i\right)_{<d} := \sum_{\substack{i \in I \\ \mathrm{depth}(s_i) < d}} a_i \cdot s_i$.

**Definition 36.** The relation $\to_r^\infty \subset \mathbb{S}^{(1)\Lambda_r} \times \mathbb{S}^{(1)\Lambda_r}$ of infinitary uniform resource reduction is defined by writing $\mathbf{U} \to_r^\infty \mathbf{V}$ whenever there is a sequence $(\mathbf{U}_d)_{d \in \mathbb{N}}$ such that

$$ \mathbf{U}_0 = \mathbf{U} \quad \forall d \in \mathbb{N}, \quad \mathbf{U}_d \to_{r \ge d}^* \mathbf{U}_{d+1} \quad \forall d \in \mathbb{N}, \quad (\mathbf{U}_d)_{<d} = (\mathbf{V})_{<d}. $$

By design, $\to_r^\infty$ simulates the stratification of an infinitary $\beta$-reduction, hence the following property.

**Corollary 37 (of Theorem 4 and Corollary 34).** For all $M, N \in \Lambda^{001}$, if $M \to_{\beta}^{001} N$ then $\mathcal{T}(M) \to_r^\infty \mathcal{T}(N)$.

**Proof.** We need to define a sequence $(\mathbf{U}_d)_{d \in \mathbb{N}}$ as in Definition 36. By stratification (Theorem 4), we obtain a sequence $(M_d)_{d \in \mathbb{N}}$ and we can define $\mathbf{U}_d := \mathcal{T}(M_d)$. The conclusion follows by Corollary 34 and by the fact that whenever $M \to_{\beta \ge d}^0 N$, then $(\mathcal{T}(M))_{<d} = (\mathcal{T}(N))_{<d}$. $\quad$

As announced, this simulation enjoys a converse conservativity property.

**Theorem 38 (conservativity).** For $M, N \in \Lambda^{001}$, if $\mathcal{T}(M) \to_r^\infty \mathcal{T}(N)$ then $M \to_{\beta}^{001} N$.

The proof of the theorem goes as follows.

**Lemma 39.** For all $M, N \in \Lambda^{001}$ and $d \in \mathbb{N}$, if $\mathcal{T}(M) \to_{r \ge d} \mathcal{T}(N)$ then $M \to_{\beta \ge d} N$.

**Proof.** By an immediate induction on the reduction $(s)_{s \in |\mathcal{T}(M)|} \to_{r \ge d} (T_s)_{s \in |\mathcal{T}(M)|}$ induced by $\mathcal{T}(M) \to_{r \ge d} \mathcal{T}(N)$. $\quad$

**Lemma 40.** For all $M \in \Lambda^{001}$ and $S \in \mathbb{S}^{\Lambda_r}$, if $\mathcal{T}(M) \to_r S$ then there exists an $M' \in \Lambda^{001}$ such that $S = \mathcal{T}(M')$.
**Proof.** By an immediate induction on the reduction $(s)_{s \in |\mathcal{T}(M)|} \stackrel{\leftarrow}{\rightarrow}_{r \ge d} (T_s)_{s \in |\mathcal{T}(M)|}$ induced by $\mathcal{T}(M) \stackrel{\leftarrow}{\rightarrow}_{r \ge d} S$. The base case relies on the same substitution lemma (Lemma 4.8 of [31]) as the proof of Theorem 12.

◀

**Lemma 41.** Consider families $(u_i)_{i \in I} \in ((!)\Lambda_r)^I$ and $(V_i)_{i \in I} \in (\mathbb{N}^{((!)\Lambda_r)})^I$ such that $(u_i)_{i \in I} \stackrel{\leftarrow}{\rightarrow_r} (V_i)_{i \in I}$. For all $i, j \in I$, if $u_i = u_j$ then $V_i = V_j$.

**Proof.** By induction on $(u_i)_{i \in I} \stackrel{\leftarrow}{\rightarrow_r} (V_i)_{i \in I}$.

In particular, this lemma allows to change the index set $I$ when writing a reduction $(u_i)_{i \in I} \stackrel{\leftarrow}{\rightarrow_r} (V_i)_{i \in I}$, as soon as no $u_i$ (and corresponding $V_i$) is erased or created – but duplications and erasures of duplicates are allowed.

**Lemma 42.** For all $S, T \in \mathbb{S}^{\Lambda_r}$, if $S' \stackrel{\leftarrow}{\rightarrow_r} T'$ then $S \stackrel{\leftarrow}{\rightarrow_r} T$.

**Proof.** Suppose that $S' \stackrel{\leftarrow}{\rightarrow_r} T'$. Thanks to Lemma 41, there is a derivation

$$ \begin{array}{c} \begin{array}{c} \begin{array}{c} (s_i) \qquad \begin{array}{c} n \in \mathbb{N} \\ s_1, \dots, s_n \in |S| \\ 1 \le i \le n \end{array} \end{array} \stackrel{\leftarrow}{\rightarrow}_r (T_{s_i}) \qquad \begin{array}{c} n \in \mathbb{N} \\ s_1, \dots, s_n \in |S| \\ 1 \le i \le n \end{array} \end{array} \\ \begin{array}{c} \begin{array}{c} ([s_1, \dots, s_n]) \qquad \begin{array}{c} n \in \mathbb{N} \\ s_1, \dots, s_n \in |S| \end{array} \end{array} \stackrel{\leftarrow}{\rightarrow}_r ([T_{s_1}, \dots, T_{s_n}) \qquad \begin{array}{c} n \in \mathbb{N} \\ s_1, \dots, s_n \in |S| \end{array} \end{array} \\ \sum_{n \in \mathbb{N}} \sum_{s_1, \dots, s_n \in |S|} \underbrace{\frac{\prod_{i=1}^n a_{s_i}}{n!} \cdot [s_1, \dots, s_n]}_{S'} \stackrel{\rightarrow}{\rightarrow}_r \sum_{n \in \mathbb{N}} \sum_{s_1, \dots, s_n \in |S|} \underbrace{\frac{\prod_{i=1}^n a_{s_i}}{n!} \cdot [T_{s_1}, \dots, T_{s_n}]}_{T'} \end{array} \end{array} $$

with $S = \sum_{s \in |S|} a_s \cdot s$. By Lemma 41 again, the hypothesis of the derivation is equivalent to $(s)_{s \in |S|} \stackrel{\leftarrow}{\rightarrow_r} (T_s)_{s \in |S|}$, hence we can derive:

$$ \frac{(s)_{s \in |S|} \stackrel{\leftarrow}{\rightarrow_r} (T_s)_{s \in |S|}}{S \stackrel{\rightarrow}{\rightarrow_r} \sum_{s \in |S|} a_s \cdot T_s} $$

To see that $T = \sum_{s \in |S|} a_s \cdot T_s$, observe that

the coefficient of $t$ in $T$

= the coefficient of $[t]$ in $T'$

= the coefficient of $[t]$ in $\sum_{n \in \mathbb{N}} \sum_{s_1, \dots, s_n \in |S|} \frac{\prod_{i=1}^n a_{s_i}}{n!} \cdot [T_{s_1}, \dots, T_{s_n}]$

= $\sum_{s \in |S|} a_s$ × the coefficient of $t$ in $T_s$

= the coefficient of $t$ in $\sum_{s \in |S|} a_s \cdot T_s$,

which concludes the proof.

**Proof of theorem 38.** Suppose that there is a sequence $(S_d)_{d \in \mathbb{N}}$ such that

$$ S_0 = \mathcal{T}(M) \quad \forall d \in \mathbb{N}, \quad S_d \stackrel{*}{\rightarrow}_{r \ge d} S_{d+1} \quad \forall d \in \mathbb{N}, \quad (S_d)_{<d} = (\mathcal{T}(N))_{<d}. $$

By Lemma 40 there is a sequence of terms $(M_d)_{d \in \mathbb{N}}$ such that $\forall d \in \mathbb{N}$, $S_d = \mathcal{T}(M_d)$. We can take $M_0 = M$, and our hypotheses yield

$$ \forall d \in \mathbb{N}, \mathcal{T}(M_d) \stackrel{*}{\rightarrow}_{r \ge d} \mathcal{T}(M_{d+1}) \quad (35) $$

$$ \forall d \in \mathbb{N}, (\mathcal{T}(M_d))_{<d} = (\mathcal{T}(N))_{<d}. \quad (36) $$
For any sequence $(M_d)_{d \in \mathbb{N}}$ such that Equations (35) and (36) hold, we build a reduction $M_0 \to_{\beta}^{001} N$ by nested induction and coinduction on $N$.

- Case $N = x$. $(\mathcal{T}(M_1))_{<1} = (\mathcal{T}(N))_{<1} = x$ hence also $\mathcal{T}(M_1) = x$. As a consequence, $\mathcal{T}(M_0) \to_{\mathbb{r}} x$ so by Lemma 39 $M_0 \to_{\beta}^{*} x$, which leads to the conclusion.

- Case $N = \lambda x.P'$. For all $d \ge 1$, $(\mathcal{T}(M_d))_{<d} = (\mathcal{T}(N))_{<d} = \lambda x.(\mathcal{T}(P'))_{<d}$ hence there is a term $P_d \in \Lambda^{001}$ such that $M_d = \lambda x.P_d$. We also define $P_0 := P_1$, so that $M_0 \to_{\beta}^{*} \lambda x.P_0$ by Equation (35) and Lemma 39.

The sequence $(P_d)_{d \in \mathbb{N}}$ satisfies Equations (35) and (36) wrt. $P'$, hence by induction we can build a reduction $P_0 \to_{\beta}^{001} P'$. We conclude with the rule $(\lambda_{\beta}^{001})$ from Definition 3.

- Case $N = (P')Q'$. For all $d \ge 1$, $(\mathcal{T}(M_d))_{<d} = (\mathcal{T}(N))_{<d} = ((\mathcal{T}(P'))_{<d}) (\mathcal{T}(Q'))_{<d-1}$ hence there are terms $P_d, Q_d \in \Lambda^{001}$ such that $M_d = (P_d)Q_d$. We also define $P_0 := P_1$, so that $M_0 \to_{\beta}^{*} (P_0)Q_1$ by Equation (35) and Lemma 39.

By Equation (35), for all $d \ge 1$ there are reductions

$$ \mathcal{T}(P_d) \underset{\mathbb{r} \ge d}{\to} \mathcal{T}(P_{d+1}) \quad \text{and} \quad \mathcal{T}(Q_d)' \underset{\mathbb{r} \ge d-1}{\to} \mathcal{T}(Q_{d+1})' $$

From the first reduction we deduce that the sequence $(P_d)_{d \in \mathbb{N}}$ satisfies Equations (35) and (36) wrt. $P'$, hence by induction we can build a reduction $P_0 \to_{\beta}^{001} P'$. From the second reduction, by Lemma 42 we deduce that the sequence $(Q_{d+1})_{d \in \mathbb{N}}$ satisfies Equations (35) and (36) wrt. $Q'$: we apply rule $(\beta^{001})$ and proceed coinductively, through the guard (▶), to establish $Q_1 \to_{\beta}^{001} Q'$.

In particular, observe that there is no reduction $A \to_{\mathbb{r}}^{\infty} \bar{A}$: in the sequence of reductions given in Equation (29) in the proof of Theorem 27, item 1, all steps $\mathcal{T}(A_d) \to_{\mathbb{r}} \mathcal{T}(A_{d+1})$ can be turned into $\mathcal{T}(A_d) \to_{\mathbb{r}}^{*} \mathcal{T}(A_{d+1})$ (as explained in Footnote 4), but not into $\mathcal{T}(A_d) \to_{\mathbb{r} \ge d} \mathcal{T}(A_{d+1})$ because there is always a reduction step occurring at depth 0.

We finally obtained a conservative approximation of the 001-infinitary $\lambda$-calculus. As a conclusive remark, let us mention that we did not take any $\perp$-reductions into account, though they are needed if one wants to simulate the reductions $M \to_{\beta \perp}^{001} BT(M)$ corresponding to Ehrhard and Regnier's commutation theorem. These reductions could be taken into account by adding the following rule:

$$ \frac{\forall i, j, u_i \subset u_j \quad \forall i, u_i \to_{\mathbb{r}}^{*} 0}{(u_i)_{i \in I} \underset{\mathbb{r} \perp}{\to} (0)_{i \in I}} $$

to Definition 33. One would then be able to provide a conservative simulation of $\to_{\beta \perp}^{001}$ by $\to_{\mathbb{r} \perp}^{\infty}$.

The question naturally arises whether this approach is transferrable to the richer $\lambda$-calculi already endowed with a linear approximation (as listed in the introduction). This remains unclear, since most of these settings are non-uniform, i.e. it is not true any more that $\mathcal{T}(M) \subset \mathcal{T}(M)$ in general. Investigating how existing techniques used to tame non-uniformity, e.g. in [31], can be exploited to address the conservativity problem in richer settings, remains an open line of research.

References

1. Davide Barbarossa. Resource approximation for the $\lambda\mu$-calculus. In *Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science*, 2022. doi:10.1145/3531130.3532469.
2 Davide Barbarossa and Giulio Manzonetto. Taylor Subsumes Scott, Berry, Kahn and Plotkin. In *47th Symposium on Principles of Programming Languages*, 2020. doi:10.1145/3371069.

3 Henk P. Barendregt. *The Lambda Calculus*. Elsevier, Amsterdam, 2 edition, 1984.

4 Henk P. Barendregt and Giulio Manzonetto. *A Lambda Calculus Satellite*. Number 94 in Mathematical logic and foundations. College publications, 2022.

5 Lison Blondeau-Patissier, Pierre Clairambault, and Lionel Vaux Auclair. Extensional Taylor Expansion, 2024. arXiv:2305.08489v2.

6 Rémy Cerda. Nominal algebra-coalgebraic data types, with applications to infinitary λ-calculi. To appear in the proceedings of the 12th International Workshop on Fixed Points in Computer Science (FICS'24).

7 Rémy Cerda. *Taylor Approximation and Infinitary λ-Calculi*. PhD thesis, Aix-Marseille Université, 2024. URL: https://hal.science/tel-04664728.

8 Rémy Cerda and Lionel Vaux Auclair. Finitary Simulation of Infinitary β-Reduction via Taylor Expansion, and Applications. *Logical Methods in Computer Science*, 19, 2023. doi: 10.46298/LMCS-19(4:34)2023.

9 Jules Chouquet and Christine Tasson. Taylor expansion for call-by-push-value. In *28th EACSL Annual Conference on Computer Science Logic*, 2020. doi:10.4230/LIPICS.CSL.2020.16.

10 Ugo Dal Lago and Thomas Leventis. On the Taylor Expansion of Probabilistic Lambda Terms. In Herman Geuvers, editor, *4th International Conference on Formal Structures for Computation and Deduction*, 2019. doi:10.4230/LIPIcs.FSCD.2019.13.

11 Daniel de Carvalho. Execution time of λ-terms via denotational semantics and intersection types. *Mathematical Structures in Computer Science*, 28(7):1169–1203, 2017. doi:10.1017/s0960129516000396.

12 Aloöš Dufour and Damiano Mazza. Böhm and Taylor for All! In *9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)*, 2024. doi:10.4230/LIPICS.FSCD.2024.29.

13 Thomas Ehrhard. On Köthe sequence spaces and linear logic. *Mathematical Structures in Computer Science*, 12(5):579–623, 2002. doi:10.1017/s0960129502003729.

14 Thomas Ehrhard. Finiteness spaces. *Mathematical Structures in Computer Science*, 15(4):615–646, 2005. doi:10.1017/S0960129504004645.

15 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*, 2016. doi:10.1145/2967973.2968608.

16 Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. *Theoretical Computer Science*, 309(1):1–41, 2003. doi:10.1016/S0304-3975(03)00392-X.

17 Thomas Ehrhard and Laurent Regnier. Differential interaction nets. *Electronic Notes in Theoretical Computer Science*, 123:35–74, 2005. doi:10.1016/j.entcs.2004.06.060.

18 Thomas Ehrhard and Laurent Regnier. Böhm Trees, Krivine's Machine and the Taylor Expansion of Lambda-Terms. In Arnold Beckmann, Ulrich Berger, Benedikt Löwe, and John V. Tucker, editors, *Logical Approaches to Computational Barriers*, pages 186–197. Springer, 2006. doi:10.1007/11780342_20.

19 Thomas Ehrhard and Laurent Regnier. Uniformity and the Taylor expansion of ordinary lambda-terms. *Theoretical Computer Science*, 403(2):347–372, 2008. doi:10.1016/j.tcs. 2008.06.001.

20 Jean-Yves Girard. Linear logic. *Theoretical Computer Science*, 50:1–102, 1987. doi:10.1016/ 0304-3975(87)90045-4.

21 Martin Hyland. A syntactic characterization of the equality in some models for the lambda calculus. *Journal of the London Mathematical Society*, s2-12:361–370, 1976. doi:10.1112/ jlms/s2-12.3.361.

22 Richard Kennaway, Jan Willem Klop, Ronan Sleep, and Fer-Jan de Vries. Infinitary lambda calculus. *Theoretical Computer Science*, 175(1):93–125, 1997. doi:10.1016/S0304-3975(96) 00171-5.
23 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*, 16:1860–5974, 2020. URL: https://lmcs.episciences.org/6638, doi:10.23638/LMCS-16(3:6)2020.

24 Axel Kerinec and Lionel Vaux Auclair. The algebraic λ-calculus is a conservative extension of the ordinary λ-calculus, 2023. arXiv:2305.01067, doi:10.48550/arXiv.2305.01067.

25 Jean-Louis Krivine. Lambda-calcul, types et modèles. Masson, 1990.

26 Damiano Mazza. An axiomatic notion of approximation for programming languages and machines, 2021. Unpublished. URL: https://www.lipn.fr/~mazza/papers/ApxAxiom.pdf.

27 Jean-Baptiste Midez. *Une étude combinatoire du lambda-calcul avec ressources uniforme*. PhD thesis, Aix-Marseille Université, 2014. URL: http://www.theses.fr/2014AIXM4093.

28 Gerd Mitschke. The standardization theorem for λ-calculus. *Zeitschrift für mathematische Logik und Grundlagen der Mathematik*, 25:29–31, 1979. doi:10.1002/malq.19790250104.

29 Dana Scott. A type-theoretical alternative to ISWIM, CUCH, OWHY. *Theoretical Computer Science*, 121(1-2):411–440, 1993. doi:10.1016/0304-3975(93)90095-b.

30 Terese. *Term Rewriting Systems*. Cambridge University Press, 2003.

31 Lionel Vaux. Normalizing the Taylor expansion of non-deterministic λ-terms, via parallel reduction of resource vectors. *Logical Methods in Computer Science*, 15:9:1–9:57, 2019. doi:10.23638/LMCS-15(3:9)2019.

32 Christopher P. Wadsworth. Approximate reduction and lambda calculus models. *SIAM Journal on Computing*, 7(3):337–356, 1978. doi:10.1137/0207028.