# Finitary Simulation of Infinitary $\beta$-Reduction via Taylor Expansion, and Applications

Rémy Cerda, Lionel Vaux Auclair

► To cite this version:

Rémy Cerda, Lionel Vaux Auclair. Finitary Simulation of Infinitary $\beta$-Reduction via Taylor Expansion, and Applications. Logical Methods in Computer Science, 2023, 19 (4), pp.34. 10.46298/lmcs-19(4:34)2023 . hal-04357092

HAL Id: hal-04357092

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

Submitted on 13 Sep 2024

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
# FINITARY SIMULATION OF INFINITARY β-REDUCTION
VIA TAYLOR EXPANSION, AND APPLICATIONS

RÉMY CERDA ◦ª AND LIONEL VAUX AUCLAIR ◦ª

Aix-Marseille Université, CNRS, I2M

e-mail address: remy.cerda@univ-amu.fr, lionel.vaux@univ-amu.fr

**ABSTRACT.** Originating in Girard's Linear logic, Ehrhard and Regnier's Taylor expansion of λ-terms has been broadly used as a tool to approximate the terms of several variants of the λ-calculus. Many results arise from a Commutation theorem relating the normal form of the Taylor expansion of a term to its Böhm tree. This led us to consider extending this formalism to the infinitary λ-calculus, since the Λ<sub>∞</sub><sup>001</sup> version of this calculus has Böhm trees as normal forms and seems to be the ideal framework to reformulate the Commutation theorem.

We give a (co-)inductive presentation of Λ<sub>∞</sub><sup>001</sup>. We define a Taylor expansion on this calculus, and state that the infinitary β-reduction can be simulated through this Taylor expansion. The target language is the usual resource calculus, and in particular the resource reduction remains finite, confluent and terminating. Finally, we state the generalised Commutation theorem and use our results to provide simple proofs of some normalisation and confluence properties in the infinitary λ-calculus.

## CONTENTS

<table><tr><td>1. Introduction</td><td>2</td></tr><tr><td>2. The infinitary λ-calculus</td><td>4</td></tr><tr><td>2.1. The set Λ<sub>∞</sub><sup>001</sup> of 001-infinitary λ-terms</td><td>4</td></tr><tr><td>2.2. What about α-equivalence?</td><td>7</td></tr><tr><td>2.3. Finitary β-reduction</td><td>7</td></tr><tr><td>2.4. Infinitary β-reduction</td><td>9</td></tr><tr><td>3. The Taylor expansion of λ-terms</td><td>12</td></tr><tr><td>3.1. The resource λ-calculus</td><td>12</td></tr><tr><td>3.2. The Taylor expansion</td><td>15</td></tr><tr><td>3.3. Reducing (possibly infinite) sets of resource terms</td><td>16</td></tr><tr><td>4. Simulating the infinitary reduction</td><td>17</td></tr><tr><td>4.1. Simulation of the finite reductions</td><td>18</td></tr><tr><td>4.2. A “step-by-step” decomposition of the reduction</td><td>19</td></tr><tr><td>4.3. Decomposing the decomposition</td><td>22</td></tr><tr><td>4.4. Height of a resource term</td><td>23</td></tr></table>

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

<footnote>Key words and phrases: lambda-calculus, infinitary rewriting, taylor expansion, program approximation, semantics of program languages.</footnote>
<table><tr><td>4.5. The diagonal argument</td><td>23</td></tr><tr><td>5. Head reduction and normalisation properties</td><td>25</td></tr><tr><td>5.1. Solvability in Λ<sup>001</sup></td><td>25</td></tr><tr><td>5.2. Normalisation, confluence and the Commutation Theorem</td><td>27</td></tr><tr><td>5.3. Infinitary contexts and the Genericity Lemma</td><td>31</td></tr><tr><td>6. Conclusion</td><td>33</td></tr><tr><td>References</td><td>35</td></tr></table>

# 1. INTRODUCTION

The seminal idea of *quantitative semantics*, introduced in the early 1980s by Girard as an alternative to traditional denotational semantics based on Scott domains, is to interpret the terms of the λ-calculus by power series [Gir88; for a bief survey see Pag14]. In this model, each monomial of the interpretation captures a finite approximation of the execution of the interpreted term, and its degree corresponds to the number of times it uses its argument. The parallelism between the decomposition of such a power series into linear maps and the behaviour of the cut-elimination of proofs led Girard to introduce *linear logic* [Gir87; Gir95], which has been a major and fruitful refinement of the Curry-Howard correspondence.

In the early 2000s, Ehrhard reformulated Girard’s quantitative semantics in a more standard algebraic framework, where terms are interpreted as analytic maps between certain vector spaces [Ehr05]. The notion of differentiation, that is available in this framework, was then brought back to the syntax by Ehrhard and Regnier in their *differential λ-calculus* [ER03]. Eventually, they defined the operation of *Taylor expansion* which maps λ-terms to infinite sums of resource terms — the latter are the terms of the resource λ-calculus, which is the finitary, purely linear fragment of the differential λ-calculus. Each term of the sum thus gives a finite approximation of the operational behaviour of the original term [ER08; BM20, for a lightened presentation].

The strength of this tool is the strong normalisation property of resource terms, and the fact that Taylor expansion commutes with normalisation: the normal form of the Taylor expansion of a term is the Taylor expansion of the Böhm tree of this term [ER06]. This Commutation theorem enables one to deduce properties of some λ-terms from the properties of their Taylor expansion; typically, properties of the (possibly) non-terminating execution of a λ-term, previously characterized by coinductive objects like its Böhm tree, are proved *via* the Taylor expansion by mere induction. This approach has been successfully applied not only to the ordinary λ-calculus [ER06; Oli18; Oli20; BM20], but also to nondeterministic [BEM12; VA19], probabilistic [DZ12; DL19], call-by-value [KMP20], and call-by-push-value [CT20] calculi, as well as Parigot’s λµ-calculus [Bar22].

In this paper, we aim to extend this formalism to the *infinitary λ-calculus*. Böhm trees [Böh68; Bar77] were already a kind of infinitary λ-terms, but an infinitary calculus (having infinite terms and infinite reductions) was first introduced in the 1990s by Kennaway, Klop, Sleep and de Vries [Ken+95; Ken+97] and by Berarducci [Ber96]. Initially presented as the metric completion of the set of λ-terms (considered as finite syntactic trees), the set of infinite λ-terms has been reformulated as an ideal completion [Bah18], and maybe more crucially as the “coinductive version” of the λ-calculus [Joa04; EP13; Cza14].
Even if the “plain” infinitary $\lambda$-calculus does not enjoy confluence, several results of confluence and of normalisation modulo “meaningless” terms have been established [Ken+97; Cza14; Cza20], as well as a standardisation theorem using coinductive techniques [EP13]. Some normalisation properties have also been characterised using non-idempotent intersection types [Via17; Via21].

These results are often only established in one of the different variants of the infinitary $\lambda$-calculus. Indeed, Kennaway et al. identify eight variants depending on the metric one chooses on syntactic trees (each of the three constructors of $\lambda$-terms can “add depth” to the term), among which only three enjoy reasonable properties (in addition to the finitary variant). Following the authors, they are called $\Lambda_{\infty}^{001}$, $\Lambda_{\infty}^{101}$ and $\Lambda_{\infty}^{111}$. In the following, we will concentrate on the $\Lambda_{\infty}^{001}$ variant, that is the one where a term can have an infinite branch only if its right applicative depth tends to infinity.

The motivation for choosing $\Lambda_{\infty}^{001}$ is that the normal forms of this calculus are the Böhm trees which are, as we recalled above, strongly related to the Taylor expansion. In some sense, $\Lambda_{\infty}^{001}$ is the “natural” setting to define and manipulate the Taylor expansion of ordinary $\lambda$-terms, as we hope to advocate for. Indeed, it enables us to state Ehrhard and Regnier’s Commutation theorem without any particular definition of the Taylor expansion of Böhm trees, and then to prove some classical results that are preserved in $\Lambda_{\infty}^{001}$, like characterisations of head- and $\beta$-normalisation or the Genericity lemma.

Since we want to take advantage of the modern, coinductive approach of [EP13], we will provide a definition of $\Lambda_{\infty}^{001}$ using coinduction. However, some technicalities arise from the fact that this is not the “fully coinductive version” of $\lambda$-calculus and that one has to mix induction and coinduction to manipulate terms and reductions in $\Lambda_{\infty}^{001}$.

Such mixings are not new and have been appearing in various areas for several decades. In particular, type systems featuring inductive and coinductive types have been presented in the late 1980s by Hagino and Mendler [Hag87; Men91], and even Eratosthenes’ sieve can be seen as an inductive-coinductive structure [Ber05]. A wide range of examples is provided by Basold’s PhD thesis, which builds a whole type-theoretic framework for inductive-coinductive reasoning [Bas18]. Several previous formalisations of mixed induction and coinduction had been proposed, in particular in [DA09; Cza19; Dal16]. We will provide a mixed formal system inspired by the latter.

**Contributions and structure of the paper.** In Section 2, we recall the definition of the infinitary $\lambda$-calculus $\Lambda_{\infty}^{001}$ and discuss the setting we choose for this mixed inductive-coinductive construction.

In Section 3, we extend the Taylor expansion of $\lambda$-terms to this calculus, and we show our main result in Section 4: the reduction of the Taylor expansion provides a simulation of the infinitary $\beta$-reduction (Theorem 4.21) by a (possibly infinite) superposition of finite reductions. This adapts the results of the second author for the ordinary $\beta$-reduction [VA17; VA19], with three important differences, induced by the infinitary nature of our setting:

(1) In [VA19], one step of $\beta$-reduction is simulated by a superposition of single steps of *parallel* reduction on resource terms (reducing all the copies of the fired redex simultaneously in each component). Here, since one step of infinitary $\beta$-reduction amounts to a possibly infinite sequence of single $\beta$-reductions, we can no longer bound the number of reductions to be performed on resource terms in the simulation. This forces us to consider the reflexive and transitive closure of reduction, rather than parallel reduction, as the underlying dynamics on resource terms.
(2) Due to the previous point, establishing the simulation is more demanding. We first obtain the simulation of finite sequences of reductions exactly as in [VA19]. Then we exploit the fact that the depth of fired redexes in an infinite $\beta$-reduction must tend to infinity, together with the strictly finitary nature of the reduction of resource terms (in particular, the fact that the size of resource terms is nonincreasing under reduction): we deduce the general simulation result by a kind of diagonal argument (see Section 4.5).

(3) Also due to the first point, we can no longer consider arbitrary infinite weighted sums of resource terms as the target of Taylor expansion: reducing arbitrarily the components of such a sum might yield infinite sums of coefficients (an example is given in Remark 3.17). We thus choose to keep to a qualitative setting only, i.e. use boolean coefficients: equivalently, we consider sets of resource terms, rather than sums.

Finally, in Section 5, we use this framework to prove the Commutation theorem (Theorem 5.20). We show that this provides new proofs of the classical results of normalisation (Lemma 5.16) and confluence (Corollary 5.23), as well as characterisations of solvability and normalisation in $\Lambda_{\infty}^{001}$ similar to the ones known for the ordinary $\lambda$-calculus. We also show an infinitary Genericity lemma (Theorem 5.30), adapting the technique introduced by [BM20].

## 2. THE INFINITARY $\lambda$-CALCULUS

### 2.1. The set $\Lambda_{\infty}^{001}$ of 001-infinitary $\lambda$-terms.
The original definition of the infinitary $\lambda$-calculus by Kennaway et al. [Ken+97] was topological. Finite terms were represented by their syntactic tree, and the usual distance $d$ on trees was defined on them by:

$$d(M, N) = 2^{-(\text{the smallest depth at which } M \text{ and } N \text{ differ})}.$$

The space of infinitary $\lambda$-terms was obtained by taking the metric completion.

One can notice that this definition is dependent on the notion of depth. Indeed, the authors defined eight variants of $\Lambda_{\infty}$, each one of them using a different notion of depth of (an occurrence of) a subterm $N$ in a term $M$:

$$ \begin{align*} \text{depth}_{N}^{abc}(N) &= 0, \\ \text{depth}_{\lambda x.M}^{abc}(N) &= a + \text{depth}_{M}^{abc}(N), \\ \text{depth}_{(M)M'}^{abc}(N) &= b + \text{depth}_{M}^{abc}(N) & \text{if the occurrence is in } M, \\ \text{depth}_{(M)M'}^{abc}(N) &= c + \text{depth}_{M'}^{abc}(N) & \text{otherwise,} \end{align*} $$

where $a, b, c \in \{0, 1\}$. This gives rise to eight spaces $\Lambda_{\infty}^{abc}$, where $\Lambda_{\infty}^{000}$ is the set of finite $\lambda$-terms $\Lambda$ and $\Lambda_{\infty}^{111}$ contains all infinitary $\lambda$-terms (notice that infinitary terms are not necessarily infinite, since all finite terms also belong to the spaces defined). The depth of all infinite branches in a term of $\Lambda_{\infty}^{abc}$ must go to infinity, that is to say such a branch must cross infinitely often a node increasing the depth. In particular, for the $\Lambda_{\infty}^{001}$ version we are interested in, the only infinite branches allowed are those crossing infinitely often the right side of an application. In Fig. 1, the left term is in $\Lambda_{\infty}^{001}$ whereas the right one is not (notice that in the former term, the infinite branch also crosses infinitely many lambdas; this is not forbidden, provided this infinite branch crosses infinitely many right sides of applications).

All versions enjoy weak normalisation, provided one identifies all “0-active” terms (i.e. those terms such that every reduct contains a redex at depth 0) with a single constant $\perp$. For instance, in $\Lambda_{\infty}^{000}$, this means identifying all non normalising terms; and in $\Lambda_{\infty}^{001}$ this
<figure><img src="image_3.png" /><figcaption>FIGURE 1. Two infinitary terms, only the left one of which is 001-infinitary.</figcaption></figure>

means identifying all non head-normalising terms. With this extended reduction, only three versions enjoy confluence, and thus unicity of normal forms: $\Lambda_{\infty}^{001}$, $\Lambda_{\infty}^{101}$ and $\Lambda_{\infty}^{111}$. Their respective normal forms are three already known notions of infinite expansions of a term, namely Böhm trees [Bar77; Bar84, § 2.1.13], Lévy-Longo trees [Lév75; Lon83; Ong88] and Berarducci trees [Ber96]. The two latter equate less terms than the unsolvable ones, and thus provide a more fine-grained description of the computational behaviour of λ-terms.

As an alternative, the infinitary λ-calculus can be seen as the “coinductive version” of the λ-calculus. If the set $\Lambda$ of the λ-terms is built inductively on the signature:

$$M, N, \dots := x \in \mathcal{V} \mid \lambda x.M \mid (M)N, \qquad (\sigma)$$

given a fixed set $\mathcal{V}$ of variables (that is, it is the initial algebra of the corresponding monotonous functor $\mathcal{V} + \lambda\mathcal{V}. - + (-) - : \mathbf{Set}^3 \to \mathbf{Set}$), then the set $\Lambda_{\infty}$ of all infinitary λ-terms is built coinductively on the same signature, as the terminal coalgebra of the same functor [for a detailed reminder of these constructions, see for instance AMM18]. This construction is summarised in the following notation, using fix-points:

$$\Lambda = \mu X.(\mathcal{V} + \lambda\mathcal{V}.X + (X)X) \qquad \Lambda_{\infty} = \nu X.(\mathcal{V} + \lambda\mathcal{V}.X + (X)X).$$

This coinductive approach has been fruitfully exploited by Endrullis and Polonsky [EP13] and Czajka [Cza14; Cza20] in the case of $\Lambda_{\infty}^{111}$. We would like to use it in the case of $\Lambda_{\infty}^{001}$, but this implies mixing induction and coinduction in order to distinguish between the “allowed” and “forbidden” infinite branches. Thus, using the same notation as above, we provide the following definition.

**Definition 2.1** (001-infinitary terms). Given a fixed set of variables $\mathcal{V}$, the set $\Lambda_{\infty}^{001}$ of 001-infinitary λ-terms is defined by:

$$\Lambda_{\infty}^{001} = \nu Y.\mu X.(\mathcal{V} + \lambda\mathcal{V}.X + (X)Y).$$
<figure><img src="image_4.png" /><figcaption>FIGURE 2. Some derivations corresponding to terms in $\Lambda_{\infty}^{001}$. Notice that the loops are correct because they cross a coinductive rule.</figcaption></figure>

It is beyond the scope of this paper to describe a general framework for defining and manipulating such a mixed inductive-coinductive set. One may consider the type-theoretic system built by Basold in his extensive study of this question [Bas18]. As a somehow less technological alternative, we interpret the binders $\mu$ and $\nu$ as the usual least and greatest fix-point constructions in the lattice $(\mathcal{P}(\Lambda_{\infty}), \subseteq)$, or the initial algebra and terminal coalgebra of the functors $\mathcal{V} + \lambda\mathcal{V}. - + (-)-$ and $\mu X.(\mathcal{V} + \lambda\mathcal{V}.X + (X)-)$ respectively.

Definition 2.1 can be unfolded using a mixed formal system (in such a system, simple bars denote inductive rules and double bars denote coinductive rules). This reformulation, inspired by [Dal16], provides a graphical description of terms in $\Lambda_{\infty}^{001}$.

**Definition 2.2** (001-infinitary terms, using a mixed formal system). $\Lambda_{\infty}^{001}$ is the set of all coinductive terms $T$ on the signature $\sigma^1$ such that $\vdash T$ can be derived in the following system:

$$ \frac{\vdash x \quad (\mathcal{V}) \quad \vdash M \quad (\lambda) \quad \vdash M \quad \vdash N \quad (@) \quad \vdash M \quad \vdash M}{\vdash x.M} \quad (\text{coI}) $$

**Remark 2.3.** To make the coinductive step explicit, we use the *later* modality $\vdash$ due to [Nak00] and named after [App+07]. This formalism could be condensed in the following “mixed rule” (@'), in a rather unusual fashion:

$$ \frac{\vdash M \quad \vdash N}{\vdash (M)N} \quad (@') $$

**Example 2.4.** Have $Y^* := \lambda f.(f)(f)(f)\dots$, which can be defined coinductively as $Y^* := \lambda f.f^{\infty}$ where $f^{\infty}$ is the largest solution of the equation $f^{\infty} = (f)f^{\infty}$. This corresponds to the derivation in Fig. 2b. Similarly, one can show that $(f^{\infty})f^{\infty} \in \Lambda_{\infty}^{001}$ and $(f^{\infty})^{\infty} \in \Lambda_{\infty}^{001}$, as derived in Figs. 2c and 2d.

**Notation 2.5.** Given $M, N \in \Lambda_{\infty}^{001}$ two terms and $k \in \mathbb{N}$ an integer, we define:

$$ (M)N^{(k)} := (\dots ((M)\underbrace{N\dots N}_{k \text{ terms}})\dots)N \qquad N^k := \underbrace{(N)\dots(N)}_{k-1 \text{ terms}} N $$

The corresponding trees are described in Fig. 3. Notice that the term $N^{\infty}$ introduced in the previous example is coherent with this notation, whereas there is no possible $(M)N^{(\infty)}$ in $\Lambda_{\infty}^{001}$.

<footnote n="1">¹Notice that for any $M, \vdash M$ cannot be a term in $\Lambda_{\infty}^{001}$, the only valid derivations being those producing terms on the signature $\sigma$, i.e. ending with one of the first three rules.</footnote>
<figure><img src="image_5.png" /><figcaption>FIGURE 3. The terms $(M)N^{(k)}$ and $N^k$.</figcaption></figure>

## 2.2. What about α-equivalence?
As one usually does when working with λ-terms, we consider the terms up to α-equivalence (renaming of bound variables) in the following. In particular, we will define substitution using Barendregt's variable convention, that is considering that any term has disjoint bound and free variables, which is usually achieved by renaming conflictual bound variables with fresh ones [Bar84, § 2.1.13].

However, this requires some precautions in an infinitary setting since we could consider an infinite term $M$ such that $FV(M) = V$, which would prevent us from taking a fresh variable. This obstacle can be overcome using some tricks, like taking a non-countable variable set $V$, or ordering it to be able to implement Hilbert's hotel — which is usually done when the proofs are formalised using De Bruijn indices [Bru72; EP13; Cza20].

One can also use nominal sets [GP02; Pit13] to directly define the quotient of the infinitary λ-calculus modulo α-equivalence as the terminal coalgebra for some functor. This construction yields a corecursion principle allowing to define substitution and normal forms for $\Lambda_{\infty}^{111}$ [Kur+12]. There is hope that the same tools could be applied to the specific case of $\Lambda_{\infty}^{001}$.

One more solution, which seems radical but which we believe is appropriate in practice, is to restrict ourselves to infinitary terms whose subterms all contain a finite number of free variables. This makes it easy to get fresh variables to implement Barendregt's convention, while preserving the strength of $\Lambda_{\infty}^{001}$ as a tool to study the infinite behaviour of finite λ-terms. Indeed, all infinitary terms generated by reductions of finitary ones enjoy this property of having finitely many free variables [Bar84, Thm. 10.1.23].<fnref n="2" />

For the sake of simplicity, we stick to the presentation using a single class of variables (instead of relying on De Bruijn indices or nominal techniques), and assume without justification that it is always possible to obtain fresh variables. We believe this question is completely orthogonal to the main matter of the paper anyway, and that our developments could be adapted straightforwardly to any other formalisation of bound variables.

## 2.3. Finitary β-reduction.
The finitary β-reduction is defined exactly as in the usual λ-calculus. We just have to check that our definitions are consistent with the restrictions we put on infinitary terms.

<footnote n="2">²Note that, writing $\Lambda(\Gamma)$ for the set of λ-terms whose free variables are in the set $\Gamma$, it is clear that $\Lambda$ is the union of the sets $\Lambda(\Gamma)$ where $\Gamma$ ranges over finite sets of variables. By contrast, the union of the sets $\Lambda_{\infty}^{abc}(\Gamma)$ — again, for $\Gamma$ finite — is a strict subset of $\Lambda_{\infty}^{abc}$, as introduced before.</footnote>
construct some possibly infinite tree (a term or a derivation), following the structure of some input which is itself a possibly infinite tree. We then reason by cases on the root of the input tree, assuming the result of the construction is known for immediate subtrees: to ensure that this defines an object in the output type, it is sufficient to check that, each time we reach a coinductive step in the input, we proceed with the construction under the guard of at least one coinductive step in the output.

**Definition 2.8** (finitary reduction $\to_\beta$). The relation $\beta_0$ is defined on $\Lambda_\infty^{001}$ by:

$$ \beta_0 := \{((\lambda x.M)N, M[N/x]), M, N \in \Lambda_\infty^{001}, x \in \mathcal{V}\}. $$

The relation $\to_\beta$ is then defined on $\Lambda_\infty^{001}$ by induction as the *contextual closure* of $\beta_0$, namely:

$$ \frac{M \beta_0 N}{M \underset{\beta}{\longrightarrow} N} (\mathrm{ax}_\beta) \qquad \frac{M \to_\beta N}{\lambda x.M \underset{\beta}{\longrightarrow} \lambda x.N} (\lambda_\beta) \\ \frac{M \to_\beta N}{(M)P \underset{\beta}{\longrightarrow} (N)P} (@l_\beta) \qquad \frac{M \to_\beta N}{(P)M \underset{\beta}{\longrightarrow} (P)N} (@r_\beta) $$

2.4. **Infinitary β-reduction.** We extend our calculus with an infinitary β-reduction. As already mentioned, an infinite reduction must “go to infinity”, that is to say that the depth of fired redexes tends to infinity.

**Notation 2.9.** Given a relation $\to$, we denote $\to^? \beta$ its reflexive closure and $\to^* \beta$ its reflexive and transitive closure.

**Definition 2.10** (001-infinitary reduction $\to_\beta^\infty$). The infinitary reduction $\to_\beta^\infty$ is defined on $\Lambda_\infty^{001}$ as the *001-strongly convergent closure* of $\to_\beta$, that is to say by the following mixed formal system:

$$ \frac{M \to_\beta^* x}{M \underset{\beta}{\longrightarrow} x} (\mathrm{ax}_\beta^\infty) \qquad \frac{M \to_\beta^* \lambda x.P \quad P \to_\beta^\infty P'}{M \underset{\beta}{\longrightarrow} \lambda x.P'} (\lambda_\beta^\infty) \\ \frac{M \to_\beta^* (P)Q \quad P \to_\beta^\infty P' \quad \triangleright Q \to_\beta^\infty Q'}{M \underset{\beta}{\longrightarrow} (P')Q'} (@_\beta^\infty) \qquad \frac{M \to_\beta^\infty M' \quad \triangleright M \to_\beta^\infty M'}{\mathrm{coI}_\beta^\infty} (\mathrm{coI}_\beta^\infty) $$

Definition 2.10 provides an inductive-coinductive presentation of the notion of strongly convergent reduction sequences defined by [Ken+97], in the specific setting of $\Lambda_\infty^{001}$: the only coinductive step occurs in argument position in the application rule, which is the position where depth$^{001}$ is incremented. In that we follow Dal Lago [Dal16], whereas the fully coinductive approach of Endrullis and Polonsky [EP13] is limited to $\Lambda_\infty^{111}$.

**Example 2.11.** The well-known $Y = \lambda f.(\Delta_f)\Delta_f$, with $\Delta_f = \lambda x.(f)(x)x$, satisfies $Y \to_\beta^\infty Y^*$. Indeed:
$$ 
\begin{aligned}
& Y \underset{\beta}{\to}^* \lambda f.(\Delta_f)\Delta_f \\
& \qquad \frac{\underset{\beta}{\overline{(\Delta_f)\Delta_f \to^* \beta (f)(\Delta_f)\Delta_f}}} {\underset{\beta}{\overline{(\Delta_f)\Delta_f \to^* \beta f}}} \\
& \qquad \frac{\underset{\beta}{\overline{\lambda(\Delta_f)\Delta_f \to^* \beta f^\infty}}} {\underset{\beta}{\overline{\lambda(\Delta_f)\Delta_f \to^* \beta f^\infty}}} \\
& \underset{\beta}{\to}^\infty Y^* = \lambda f.f^\infty
\end{aligned}
$$

**Remark 2.12.** Definitions 2.8 and 2.10 could, again, be formulated in terms of fix-points:

$$ 
\begin{aligned}
\to_{\beta} &:= \nu Y \cdot \mu X \cdot (\beta_0 + \lambda \mathcal{V} \cdot X + (X) \Lambda_{\infty}^{001} + (\Lambda_{\infty}^{001}) Y) \\
\to_{\beta}^{\infty} &:= \nu Y \cdot \mu X \cdot (\to_{\beta}^{*} + \to_{\beta}^{*}; (\lambda \mathcal{V} \cdot X) + \to_{\beta}^{*}; (X) Y)
\end{aligned}
$$

where the functors act on relations, for instance $\lambda \mathcal{V} \cdot X = \{(\lambda v \cdot x_1, \lambda v \cdot x_2) \mid v \in \mathcal{V}, (x_1, x_2) \in X\}$, and the symbol $;$ denotes the composition of relations.

**Lemma 2.13.**

(1) $\to_{\beta}^{\infty}$ is reflexive.

(2) $\to_{\beta}^{*} \subseteq \to_{\beta}^{\infty}$.

(3) $\to_{\beta}^{\infty}$ is transitive.

*Proof.* (1) For any $M \in \Lambda_{\infty}^{001}$, a derivation of $M \to_{\beta}^{\infty} M$ is built straightforwardly by nested coinduction and induction,<fnref n="3" /> following the structure of the derivation of $\vdash M$.

(2) Immediate from the rules of Definition 2.10 and from the reflexivity of $\to_{\beta}^{*}$, by cases on the reduct of $\to_{\beta}^{*}$. For instance, in the case of an abstraction:

$$ 
\begin{array}{c} 
\frac{M \to_{\beta}^{*} \lambda x.P}{M \to_{\beta}^{\infty} \lambda x.P} \\ 
\qquad (1) 
\end{array}
$$

(3) To prove transitivity, we have to show a series of sublemmas:

$$ \text{if } M \to_{\beta}^{*} M', \text{ then } M[N/x] \to_{\beta}^{*} M'[N/x] \qquad (i) $$

$$ \text{if } M \to_{\beta}^{*} M' \to_{\beta}^{\infty} M'', \text{ then } M \to_{\beta}^{\infty} M'' \qquad (ii) $$

$$ \text{if } M \to_{\beta}^{\infty} M' \text{ and } N \to_{\beta}^{\infty} N', \text{ then } M[N/x] \to_{\beta}^{\infty} M'[N'/x] \qquad (iii) $$

$$ \text{if } M \to_{\beta}^{\infty} M' \to_{\beta}^{\infty} M'', \text{ then } M \to_{\beta}^{\infty} M'' \qquad (iv) $$

$$ \text{if } M \to_{\beta}^{\infty} M' \to_{\beta}^{*} M'', \text{ then } M \to_{\beta}^{\infty} M'' \qquad (v) $$

$$ \text{if } M \to_{\beta}^{\infty} M' \to_{\beta}^{\infty} M'', \text{ then } M \to_{\beta}^{\infty} M'' \qquad (vi) $$

(i) and (ii) are immediate, respectively by nested coinduction and induction on M and by case analysis on $M' \to_{\beta}^{\infty} M''$.

To prove (iii), proceed by nested coinduction and induction on $M \to_{\beta}^{\infty} M'$.

* If $M' = x$ and $M \to_{\beta}^{*} x$, use (i) to get $M[N/x] \to_{\beta}^{*} x[N/x] = N \to_{\beta}^{\infty} N'$, and conclude with (ii).

* If $M' = y$ and $M \to_{\beta}^{*} y$, use (i) to get $M[N/x] \to_{\beta}^{*} y[N/x] = y = y[N'/x]$ and conclude with (2).

<footnote n="3">³We recall that this proof scheme is discussed in Remark 2.7 — especially in its last paragraph.</footnote>
that cannot be reduced through $\to_{\beta}$. Then, a $\beta$-normal form of a term $M$ (for the infinitary $\lambda$-calculus) is a term $N$ in $\beta$-normal form such that $M \to_{\beta}^{\infty} N$.

### 3. THE TAYLOR EXPANSION OF $\lambda$-TERMS

Introduced by Ehrhard and Regnier as a particular case of the differential $\lambda$-calculus [ER03], the resource $\lambda$-calculus [ER08] is the target language of the Taylor expansion of finite $\lambda$-terms: a $\lambda$-term is translated as a set of resource terms — or, in a quantitative setting, as a (possibly infinite) weighted sum of resource terms.

In this section, we extend the definition of Taylor expansion to infinite $\lambda$-terms. Note that this generalisation is very straightforward, and it does not require to extend the target of the translation. Indeed, Ehrhard and Regnier have defined Taylor expansion not only on finite $\lambda$-terms but also on Böhm trees, and our generalisation boils down to observe that there is already enough “room” to accommodate all terms in $\Lambda_{\infty}^{001}$.

**3.1. The resource $\lambda$-calculus.** First, let us recall the definition of the resource $\lambda$-calculus. A more detailed presentation can be found in [VA19; BM20].

**Definition 3.1 (resource $\lambda$-terms).** The set $\Lambda_r$ of resource terms on a set of variables $V$ is defined inductively by:

$$ \Lambda_r := V \mid \lambda V \Lambda_r \mid \langle \Lambda_r \rangle \Lambda_r^! $$

$$ \Lambda_r^! := \mathcal{M}_{\text{fin}}(\Lambda_r) $$

where $\mathcal{M}_{\text{fin}}(X)$ is the set of finite multisets on $X$.

We call resource monomials the elements of $\Lambda_r^!$.

To denote indistinctly $\Lambda_r$ or $\Lambda_r^!$, we write $\Lambda_r^{(1)}$. The multisets are denoted $\bar{t} = [t_1, \dots, t_n]$, in an arbitrary order. Union of multisets is denoted multiplicatively, and terms are identified to the corresponding singleton: for example, $s \cdot [t, u] = [u, s, t]$. In particular, the empty multiset is denoted 1. The cardinality of a multiset $\bar{t}$ is denoted $\#\bar{t}$.

Let $(2, \vee, \wedge)$ be the semi-ring of boolean values, and $2\langle\Lambda_r^{(1)}\rangle$ the free 2-module generated by $\Lambda_r^{(1)}$. We denote by capital $S, T$ (resp. $\bar{S}, \bar{T}$) the elements of $2\langle\Lambda_r\rangle$ (resp. $2\langle\Lambda_r^!\rangle$). By construction, an element of $2\langle\Lambda_r^{(1)}\rangle$ is nothing but a finite set of resource terms (resp. monomials), so that we find it more practical to stick to the additive notation: e.g., we will write $s + S$ instead of $\{s\} \cup S$, and we write 0 for the empty set of terms or monomials. In addition, we extend the constructors of $\Lambda_r^{(1)}$ to $2\langle\Lambda_r^{(1)}\rangle$ by linearity:

$$ \lambda x. \sum_i s_i := \sum_i (\lambda x. s_i) \left\langle \sum_i s_i \right\rangle \sum_j \bar{t}_j := \sum_{i,j} \langle s_i \rangle \bar{t}_j \left( \sum_i s_i \right) \cdot \bar{T} := \sum_i s_i \cdot \bar{T}. $$

**Remark 3.2.** We work in a qualitative setting, where $s + s = s$, in opposition with the original quantitative setting where the semi-ring $(\mathbb{N}, +, \times)$ allows to count occurrences of a resource term (for instance, $s + s = 2s$). This is similar to what is done by, e.g., Barbarossa and Manzonetto [BM20]. Our choice is motivated by the fact that, as discussed in the introduction, the treatment of infinitary reduction forbids us to consider Taylor expansion with coefficients in an arbitrary semi-ring (see Remark 3.17 for further details): we thus restrict to the qualitative version of Taylor expansion, which sends a $\lambda$-term to a (possibly
infinite) set of resource terms. We then find natural to consider a qualitative variant of the
resource calculus itself as well.

**Definition 3.3** (substitution of resource terms). If $s \in \Lambda_r$, $x \in \mathcal{V}$ and $\bar{t} = [t_1, \dots, t_n] \in \Lambda_r^!$, we define:

$$
s\langle\bar{t}/x\rangle := \left\{ \begin{array}{ll} \displaystyle \sum_{\sigma \in \mathfrak{S}_n} s[t_{\sigma(i)}/x_i] & \text{if } \deg_x(s) = n \\ 0 & \text{otherwise} \end{array} \right.
$$

where $\deg_x(s)$ is the number of free occurrences of $x$ in $s$, $x_1, \dots, x_n$ is an arbitrary enumer-
ation of these occurrences, and $s[t_{\sigma(i)}/x_i]$ is the term obtained by formally substituting $t_{\sigma(i)}$
to each corresponding occurrence $x_i$.

A more fine-grained definition can be found in [ER03; ER08], where substitution is built
as the result of a *differentiation* operation: $s\langle\bar{t}/x\rangle := (\frac{\partial^n s}{\partial x^n} \cdot \bar{t})[0/x]$.

**Definition 3.4 (resource reduction).** The simple resource reduction $\dashv_r \subset \Lambda_r^{(1)} \times 2\langle\Lambda_r^{(1)}\rangle$ is the smallest relation such that for every $s, x$ and $\bar{t}, \langle\lambda x.s\rangle \bar{t} \dashv_r s\langle\bar{t}/x\rangle$ holds, and closed under:

$$
\frac{s \mapsto_r S}{\lambda x.s \mapsto_r \lambda x.S} (\lambda_r)
\qquad
\frac{s \mapsto_r S}{\langle s \rangle \bar{t} \mapsto_r \langle S \rangle \bar{t}} (@l_r)
\\[2ex]
\frac{\bar{t} \mapsto_r \bar{T}}{\langle s \rangle \bar{t} \mapsto_r \langle s \rangle \bar{T}} (@r_r)
\qquad
\frac{s \mapsto_r S}{s \cdot \bar{t} \mapsto_r S \cdot \bar{t}} (!_r)
$$

This relation is extended to $\dashv_r \subset 2\langle\Lambda_r\rangle \times 2\langle\Lambda_r\rangle$ by the rule:

$$
\frac{s_0 \mapsto_r T_0 \quad (s_i \mapsto_r^? T_i)_{i=1}^n}{\sum_{i=0}^n s_i \dashrightarrow_r \sum_{i=0}^n T_i} (\Sigma_r)
$$

**Remark 3.5.** Some authors, like [BM20], prefer the following alternative:

$$
\frac{s \mapsto_r S \quad s \notin T}{s + T \dashrightarrow_r S + T} (\Sigma'_r)
$$

Both versions define the same normal forms, but do not induce the same dynamics. In
particular, $(\Sigma'_r)$ preserves the termination of $\dashv_r^*$ even in the qualitative setting, whereas
$(\Sigma_r)$ allows to reduce $s$ to $s+S$ whenever $s \dashrightarrow_r S$, which obviously prevents termination.

However, the assumption $s \notin T$ in $(\Sigma'_r)$ forbids to reduce *contextually* in a sum, meaning
that with this rule, $S \dashrightarrow_r^* S'$ and $T \dashrightarrow_r^* T'$ do not straightforwardly imply $S+T \dashrightarrow_r^* S' + T'$.<fnref n="4" /> Hence our choice to use $(\Sigma_r)$ instead: ensuring the contextuality of $\dashrightarrow_r$ gives rise
to a strong confluence result, as recalled in Lemma 3.9 — whereas the reduction defined by
$(\Sigma'_r)$ is “only” confluent.<fnref n="5" /> This technical choice will play a crucial role in the following: see in
particular Remark 3.15 and Lemma 3.18.

<footnote n="4">⁴We could find no counterexample to this implication, but no proof either. Our best effort allowed us to prove that $S \dashrightarrow_r^* S'$ and $S \cap T = \emptyset$ imply $S + T \dashrightarrow_r^* S' + T$.</footnote>

<footnote n="5">⁵Using the fact that $(\Sigma'_r)$ is a particular case of $(\Sigma_r)$, and the fact that the reduction using $(\Sigma_r)$ is confluent and normalising, we do know that each $S \in 2\langle\Lambda_r\rangle$ reduces to a unique normal form $nf_r(S)$, and that $nf_r(S+T) = nf_r(S) + nf_r(T)$, whatever rule we choose. This is sufficient to obtain confluence, but the proof is thus indirect for the version using rule $(\Sigma'_r)$. By contrast, the proof sketch in [BM20] claims to rely on a direct proof of local confluence, but it is not given in full: in particular the case of sums is not discussed. It can be worked out, but it is not straightforward, again because of the lack of contextuality.</footnote>
**Definition 3.6.** The size $|\cdot|$ of resource terms is defined inductively by:

$$ 
\begin{align*}
|x| &:= 1 \\
|\lambda x.s| &:= 1 + |s| \\
|\langle s \rangle \bar{t}| &:= |s| + |\bar{t}| \\
|[t_1, \dots, t_n]| &:= 1 + \sum_{i=1}^{n} |t_i|.
\end{align*}
$$

The size of a finite sum $S \in 2\langle\Lambda_r\rangle$ is given by $|S| := \max_{s \in S} |s|$. By convention, $|0| := 0$.

**Lemma 3.7.** Given $s \in \Lambda_r$ and $S \in 2\langle\Lambda_r\rangle$, if $s \mapsto_r S$ then $|S| < |s|$.

*Proof.* We first show that for $s \in \Lambda_r$, $x \in \mathcal{V}$ and $\bar{t} = [t_1, \dots, t_n] \in \Lambda_r^!$, $|s \langle \bar{t}/x \rangle| < |\langle \lambda x.s \rangle \bar{t}|$.

* If $\deg_x(s) \neq n$, $|s \langle \bar{t}/x \rangle| = |0| = 0$ and $|\langle \lambda x.s \rangle \bar{t}| \geq 3$.

* Otherwise, $|s \langle \bar{t}/x \rangle| = |s| - n + \sum_{i=1}^n |t_i|$ and $|\langle \lambda x.s \rangle \bar{t}| = |s| + 2 + \sum_{i=1}^n |t_i|$, which leads to the expected inequality.

We obtain the desired result on $\mapsto_r$ by induction. $\square$

**Remark 3.8.** Observe that, as a corollary, we obtain $|S'| \leq |S|$ whenever $S \to_r S'$ in $2\langle\Lambda_r\rangle$, but this inequality is not strict in general; indeed, if $S \to_r S'$ and $|T| \geq |S|$ then $S+T \to_r S' + T$ but $|S'+T| = |S+T| = |T|$.

Nonetheless, the previous Lemma ensures the normalisation of $\to_r$, using the multiset order on the sizes of elements in a finite sum, as we now show.

**Lemma 3.9 (normalisation and confluence of $\to_r$).**

(1) The resource reduction $\to_r \subset 2\langle\Lambda_r\rangle \times 2\langle\Lambda_r\rangle$ is weakly normalising.

(2) This reduction is strongly confluent in the following sense: whenever there are $S, T_1, T_2 \in 2\langle\Lambda_r\rangle$ as below, there is a $U \in 2\langle\Lambda_r\rangle$ such that:

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

In particular, it is confluent.

*Proof.* We prove (1). For (2), the proof is exactly the same as that of [VA19, Lem. 3.11].

To each $S = \sum_{i=1}^n s_i$ (assuming the $s_i$'s are pairwise distinct), we can associate the multiset $\|S\| := [|s_1|, \dots, |s_n|]$. Lemma 3.7 entails $\|S' + T\| \prec \|s + T\|$ whenever $s \mapsto_r S'$ and $s \notin T$ — where $\prec$ denotes the Dershowitz–Manna ordering [DM79] induced on $M_{\text{fin}}(\mathbf{N})$ by $<$, which is well-founded. This entails the strong normalisation property for the version of $\to_r$ restricted to rule $(\Sigma'_r)$, hence the weak normalisation of the more general version we use. $\square$

**Notation 3.10.** For $s \in \Lambda_r^{(l)}$, we write $nf_r(s)$ for its normal form.
**3.2. The Taylor expansion.** Just like the Taylor expansion of a function in calculus, the Taylor expansion of a term is a weighted, possibly infinite sum of finite approximants. In our qualitative setting, the weights vanish and the Taylor expansion can be seen as a mere set of approximants (usually called the *support* of the full quantitative Taylor expansion). However, we describe these sets using an additive formalism, to be consistent with the finite sums as defined above.

**Notation 3.11.** A possibly infinite set $\{s_i, i \in I\} \subset \Lambda_r$ will be denoted as $\sum_{i \in I} s_i$. In particular, finite sets will be assimilated to the corresponding finite sums in $2\langle\Lambda_r\rangle$. Accordingly:

* $s \in \sum_{i \in I} s_i$ means that $s$ belongs to the given set (and equivalently, in the finite case, has coefficient 1 in the given sum),

* unions of sets are also denoted with the symbols $+$ and $\sum$,

* the singleton $\{s\}$ is assimilated to the 1-term sum $s$.

In the finitary setting, the definition of the Taylor expansion relies on the following induction:

$$ \begin{aligned} \mathcal{T}(x) &:= x, & \mathcal{T}(\lambda x.M) &:= \sum_{s \in \mathcal{T}(M)} \lambda x.s, \\ \mathcal{T}((M)N) &:= \sum_{s \in \mathcal{T}(M)} \sum_{\bar{t} \in \mathcal{T}(N)!} \langle s \rangle \bar{t}, & \mathcal{T}(M)! &:= \mathcal{M}_{\text{fin}}(\mathcal{T}(M)). \end{aligned} $$

In our setting, the principle of the definition is exactly the same: to collect the finite approximants of an infinitary term, one just has to *inductively* scan the term. However, there is no possible “structural induction” on coinductive objects, so that we need to define explicitly an approximation relation.

**Definition 3.12 (Taylor expansion).** The relation $\ltimes$ of *Taylor approximation* is inductively defined on $\Lambda_r \times \Lambda_\infty^{001}$ by:<fnref n="6" />

$$ \overline{x \ltimes x} (\lambda x) \quad \frac{s \ltimes M}{\lambda x.s \ltimes \lambda x.M} (\lambda_\ltimes) \quad \frac{s \ltimes M \quad \bar{t} \ltimes! N}{\langle s \rangle \bar{t} \ltimes (M)N} (@_\ltimes) \quad \frac{(t_i \ltimes M)^n_{i=1}}{[t_1, \dots, t_n] \ltimes! M} (!_\ltimes) $$

The *Taylor expansion* of a term $M \in \Lambda_\infty^{001}$ is the set $\mathcal{T}(M) := \sum_{s \ltimes M} s$.

Again, it is practical to extend $\ltimes$ to sums of resource terms: we write $\sum_i s_i \ltimes M$ whenever $\forall i, s_i \ltimes M$, so that $\mathcal{T}(M) \ltimes M$ and $\mathcal{T}(M)$ is the greatest set of resource terms with that property. Note that, due to the shape of rule $(!_\ltimes)$, $\mathcal{T}(M)$ is infinite as soon as $M$ contains an application.

**Remark 3.13.** We could very well consider a quantitative version of Taylor expansion: it poses no particular problem to define the coefficient of $s$ in $\mathcal{T}(M)$ by induction on $s$, following the original definition for ordinary $\lambda$-calculus [ER06]. Establishing a quantitative version of our simulation result, taking coefficients into account, is another matter, because the reduction of infinite weighted sums of resource terms is not always well defined: see Remark 3.17 below.

<footnote n="6">⁶The relation $\ltimes$ could be equivalently defined by induction on resource terms, rather than by a system of derivations: derivations are actually directed by the syntax of resource terms.</footnote>
**3.3. Reducing (possibly infinite) sets of resource terms.** So far, we are only able to reduce finite sums of resource terms (using $\rightarrow_r$), but the Taylor expansion of a term is an infinite sum in general. The following definition enables us to lift $\rightarrow_r^*$ from $\Lambda_r \times 2\langle\Lambda_r\rangle$ to $\mathcal{P}(\Lambda_r) \times \mathcal{P}(\Lambda_r)$.

**Definition 3.14.** Let $X$ be a set, and $\rightarrow \subset X \times 2\langle X\rangle$ a relation. We define a reduction $\rightsquigarrow \subset \mathcal{P}(X) \times \mathcal{P}(X)$ by stating that $A \rightsquigarrow B$ if we can write:

$$A = \sum_{i \in I} a_i, \quad B = \sum_{i \in I} B_i \quad \text{and} \quad \forall i \in I, a_i \rightarrow B_i,$$

where $I$ is a (possibly infinite) set of indices and, for each $i \in I$, $a_i \in X$ and $B_i \in 2\langle X\rangle$.

In the following, we consider the relation $\rightsquigarrow_r^*$ on sets of resource terms.

**Remark 3.15.** As a direct consequence of the definition, given two sets $S, S' \in \mathcal{P}(\Lambda_r)$, we have $S \rightsquigarrow_r^* S'$ whenever we can write:

$$S' = \sum_{s \in S} S'_s \quad \text{and} \quad \forall s \in S, s \rightarrow_r^* S'_s. \qquad (i)$$

Note in particular that the length of each reduction $s \rightarrow_r^* S'_s$ might depend on $s$, and is not bounded in general, which will be crucial in the following.

It turns out that condition (i) is in fact equivalent to the definition of $S \rightsquigarrow_r^* S'$.

**Lemma 3.16.** We have $S \rightsquigarrow_r^* S'$ iff condition (i) holds.

*Proof.* Due to the way we defined $\rightarrow_r$ from $\mapsto_r$, we have $S \rightarrow_r^* S'$ iff we can write $S = \sum_{i=1}^n s_i$ and $S' = \sum_{i=1}^n S'_i$ with $s_i \rightarrow_r^* S'_i$ for $1 \le i \le n$. In particular $s \rightarrow_r^* S'$ iff we can write $S' = \sum_{i=1}^n S'_i$ with $n > 0$ and $s \rightarrow_r^* S'_i$ for $1 \le i \le n$ — note that this latter equivalence holds only because we consider finite sets of terms rather than formal sums, so that $s = \sum_{i=1}^n s$.

Hence condition (i) holds iff we can write $S = \sum_{i \in I} s_i$ and $S' = \sum_{i \in I} S'_i$ so that for each $i \in I$, $s_i \rightarrow_r^* S'_i$, and furthermore for each $s \in \Lambda_r$, $\{i \in I, s_i = s\}$ is finite. But this finiteness condition is always fulfilled: Lemma 3.7 entails that $|S'| \le |s|$ whenever $s \rightarrow_r^* S'$, and since moreover the free variables of $S'$ are also free in $s$, we obtain that $\{S', s \rightarrow_r^* S'\}$ is finite. $\square$

Observe that several steps in the previous proof rely implicitly on the contextuality of $\rightarrow_r^*$, obtained thanks to rule $(\Sigma_r)$, as stressed in Remark 3.5.

**Remark 3.17.** The proof of Lemma 3.16 also shows that $\rightsquigarrow_r^*$ is in fact a variant of the relation on (possibly infinite) linear combinations of resource terms introduced by the second author in a quantitative setting, in order to simulate the $\beta$-reduction of ordinary $\lambda$-terms [VA17; VA19, Def. 5.4].

The only difference is that the underlying reduction on resource terms is the iterated reduction $\rightarrow_r^*$ rather than a parallel variant of $\rightarrow_r$. Indeed, we want to simulate $\rightarrow_{\beta}^\infty$, which amounts to a possibly infinite sequence of $\beta$-reductions: as discussed in the introduction, we cannot bound the number of reductions to be performed on resource terms in the simulation of one step of $\rightarrow_{\beta}^\infty$, and we are forced to consider the reflexive and transitive closure of resource reduction instead — the only point of parallel resource reduction was precisely to avoid the need to consider $\rightarrow_r^*$ in the simulation of a single $\beta$-reduction step.
In particular, we do face obstacles to considering a quantitative version of reduction, as studied in [VA19]. For instance, observe that the Taylor expansion of the 001-infinitary term $(\lambda x.x)^{\infty}$ contains each resource term of the shape

$$ \langle \lambda x.x \rangle^k [s] := \underbrace{\langle \lambda x.x \rangle [\cdots [ \langle \lambda x.x \rangle [s] \cdots ]]}_{k \text{ nested linear applications}} $$

where $s$ is itself any fixed approximant of $(\lambda x.x)^{\infty}$. Each $\langle \lambda x.x \rangle^k [s]$ reduces to $s$ (in $k$ steps): in particular, $\sum_{k \in \mathbb{N}} \langle \lambda x.x \rangle^k [s] \xrightarrow{\beta^*} \sum_{k \in \mathbb{N}} s$. If we were to take coefficients into account we would have to deal with infinite sums of coefficients. This is precisely why we stick to the qualitative setting.

**Lemma 3.18.**

(1) $\xrightarrow{\beta^*}$ is reflexive and transitive.

(2) $(\xrightarrow{\beta^*})^* \subseteq \xrightarrow{\beta^*}$.

*Proof.* (1) Reflexivity is immediate: $A = \sum_{a \in A} \{a\}$ with $a \to_{\beta}^* a$. For transitivity, consider $A \xrightarrow{\beta^*} B \xrightarrow{\beta^*} C$, that is $B = \sum_{a \in A} B_a$ with $a \to_{\beta}^* B_a$, and $C = \sum_{b \in B} C_b$ with $b \to_{\beta}^* C_b$. From the latter, we have $B_a \to_{\beta}^* \sum_{b \in B_a} C_b$ for each $a$. Finally:

$$ C = \sum_{a \in A} \sum_{b \in B_a} C_b \quad \text{and} \quad \forall a \in A, a \xrightarrow{\beta}^* B_a \xrightarrow{\beta}^* \sum_{b \in B_a} C_b, $$

that is $A \xrightarrow{\beta}^* C$.

(2) We have $\xrightarrow{\beta}^* \subset \xrightarrow{\beta}^*$, from which we deduce $\xrightarrow{\beta}^* \subset \xrightarrow{\beta}^*$, and finally $(\xrightarrow{\beta}^*)^* \subseteq (\xrightarrow{\beta}^*)^* = \xrightarrow{\beta}^*$ from (1). $\square$

**Notation 3.19.** For every $S \in \mathcal{P}(\Lambda_r^{(1)})$, we write its normal form $\tilde{nf}_r(S) = \sum_{s \in S} \tilde{nf}_r(s)$. Observe that $S \xrightarrow{\beta}^* \tilde{nf}_r(S)$, because $s \to_{\beta}^* \tilde{nf}_r(s)$ for each $s \in S$.

## 4. SIMULATING THE INFINITARY REDUCTION

The goal of this part is to simulate the infinitary reduction through the Taylor expansion, that is to obtain the following result:

$$ \text{if } M \xrightarrow{\beta}^\infty N, \text{ then } \mathcal{T}(M) \xrightarrow{\beta}^* \mathcal{T}(N). $$

We first show that the result holds if $M \xrightarrow{\beta}^* N$ (Lemma 4.2). Then we decompose $\xrightarrow{\beta}^\infty$ into finite “min-depth” steps $\xrightarrow{\beta}^* \xrightarrow{\beta \ge d}$ followed by an infinite $\xrightarrow{\beta \ge d}$ (Lemma 4.11), and we refine this decomposition into a tree of (min-depth resource) reductions using the Taylor expansion (Corollary 4.14). Finally, after having related the *size* and *height* of resource terms, we conclude with a diagonal argument that enables us to “skip” the part related to $\xrightarrow{\beta \ge d}$ in each branch of the aforementioned tree (Theorem 4.21).
**4.1. Simulation of the finite reductions.** As a first step, we want to simulate substitution and finite $\beta$-reduction through the Taylor expansion. This follows a well-known path, similar to the finitary calculus [VA17].

**Lemma 4.1 (simulation of the substitution).** Let $M, N \in \Lambda^0_{\infty}$ be terms, and $x \in \mathcal{V}$ be a variable. Then:

$$ \mathcal{T}(M[N/x]) = \sum_{s \in \mathcal{T}(M)} \sum_{\bar{t} \in \mathcal{T}(N)!} s\langle \bar{t}/x \rangle. $$

*Proof.* We proceed by double inclusion. First, we show that for all derivation $u \times M[N/x]$, there exist derivations $s \times M$ and $\bar{t} \times! N$ such that $u \in s\langle \bar{t}/x \rangle$. We do so by induction on $u \times M[N/x]$, considering the possible cases for $M$:

* If $M = x$ then $M[N/x] = N$, hence $u \times N$. Then we can set $s := x$ and $\bar{t} := [u]$.

* If $M = y \neq x$ then $M[N/x] = y$, hence $u = y$. Then we can set $s := y$ and $\bar{t} := 1$.

* If $M = \lambda y.M'$ then $M[N/x] = \lambda y.M'[N/x]$, hence we must have $u = \lambda y.u'$ with $u' \times M'[N/x]$. The induction hypothesis yields $s' \times M'$ and $\bar{t} \times! N$ such that $u' \in s'\langle \bar{t}/x \rangle$. Then we can set $s := \lambda y.s'$.

* If $M = (M')N'$ then $M[N/x] = (M'[N/x])M''[N/x]$, hence we must have $u = \langle u' \rangle \bar{u}''$ with $u' \times M'[N/x]$ and $\bar{u}'' \times! M''[N/x]$. Writing $\bar{u}'' = [u''_1, \dots, u''_n]$, this means $u''_i \times M''[N/x]$ for $1 \le i \le n$. The induction hypothesis applied to $u' \times M'[N/x]$ yields $s' \times M'$ and $\bar{t}_0 \times! N$ such that $u' \in s'\langle \bar{t}_0/x \rangle$. The induction hypothesis applied to each $u''_i \times M''[N/x]$ yields $s''_i \times M''$ and $\bar{t}_i \times! N$ such that $u''_i \in s''_i\langle \bar{t}_i/x \rangle$. Then we can set $s := \langle s' \rangle [s''_1, \dots, s''_n]$ and $\bar{t} := \bar{t}_0 \dots \bar{t}_n$.

This concludes the first inclusion. Conversely, let us show that for all derivations $s \times M$ and $\bar{t} \times! N$, $s\langle \bar{t}/x \rangle \times M[N/x]$. We proceed by induction on the derivation $s \times M$:

* If $s = x \times x = M$ and $\bar{t} = [t] \times! N$, then $s\langle \bar{t}/x \rangle = t \times N = M[N/x]$.

* If $s = y \times y = M$ and $\bar{t} = 1 \times! N$, then $s\langle \bar{t}/x \rangle = y \times y = M[N/x]$.

* If $s$ is a variable, but none of the previous two cases apply, then we have $s\langle \bar{t}/x \rangle = 0 \times M[N/x]$ for free.

* If $s = \lambda y.s' = \lambda y.P = M$ with $s' \times P$, then by induction for any derivation $\bar{t} \times! N$, we have $s'\langle \bar{t}/x \rangle \times P[N/x]$. Applying the rule $\lambda_{\times}$ to each summand of $s'\langle \bar{t}/x \rangle$ gives $s\langle \bar{t}/x \rangle = \lambda y.s'\langle \bar{t}/x \rangle \times \lambda y.P[N/x] = M[N/x]$.

* If $s = \langle s' \rangle \bar{s}'' \times (P)Q = M$ with $s' \times P$ and $\bar{s}'' = [s''_1, \dots, s''_m] \times! Q$. Fix $\bar{t} \times! N$. For each $v \in s\langle \bar{t}/x \rangle$, there are monomials $\bar{t}_0, \dots, \bar{t}_m$ such that $\bar{t} = \bar{t}_0 \dots \bar{t}_m$ and $v \in \langle s'\langle \bar{t}_0/x \rangle \rangle [s''_1\langle \bar{t}_1/x \rangle, \dots, s''_m\langle \bar{t}_m/x \rangle]$. Observing that $\bar{t}_i \times! N$ for $0 \le i \le m$, the induction hypothesis yields:

- $s'\langle \bar{t}_0/x \rangle \times P[N/x]$,

- and, for $1 \le i \le m$, $s''_i\langle \bar{t}_i/x \rangle \times Q[N/x]$.

We obtain $v \times (P[N/x])Q[N/x] = M[N/x]$ by applying the rules ($@_{\times}$) and ($!_{\times}$). Hence $s\langle \bar{t}/x \rangle \times M[N/x]$. $\square$

**Lemma 4.2 (simulation of the finitary reduction).** If $M \xrightarrow{\beta}^* N$, then $\mathcal{T}(M) \xrightarrow{\sim}^* \mathcal{T}(N)$.

*Proof.* We first show the result for $M \xrightarrow{\beta} N$, by induction on the corresponding derivation.

* Case ($\alpha x_{\beta}$). Take $M = (\lambda x.P)Q \beta_0 P[Q/x] = N$, then:

$$ \mathcal{T}(M) = \mathcal{T}((\lambda x.P)Q) = \sum_{s \in \mathcal{T}(\lambda x.P)} \sum_{\bar{t} \in \mathcal{T}(Q)!} \langle s \rangle \bar{t} = \sum_{s \in \mathcal{T}(P)} \sum_{\bar{t} \in \mathcal{T}(Q)!} \langle \lambda x.s \rangle \bar{t}. $$
Since $\langle \lambda x.s \rangle \bar{t} \to_r s \langle \bar{t}/x \rangle$, we obtain from Lemma 4.1:

$$ \mathcal{T}(M) \underset{\sim}{\to}_r \sum_{s \in \mathcal{T}(P)} \sum_{\bar{t} \in \mathcal{T}(Q)!} s \langle \bar{t}/x \rangle = \mathcal{T}(P[Q/x]) = \mathcal{T}(N). $$

* Case $(\lambda_\beta)$. Take $M = \lambda x.P \to_\beta \lambda x.P' = N$, with $P \to_\beta P'$. By induction, we have $\mathcal{T}(P) \underset{\sim}{\to}_r^* \mathcal{T}(P')$, that is $\mathcal{T}(P') = \sum_{s \in \mathcal{T}(P)} S'_s$ with $s \to_r^* S'_s$. Then:

$$ \mathcal{T}(M) = \sum_{s \in \mathcal{T}(P)} \lambda x.s \quad \text{and} \quad \mathcal{T}(N) = \sum_{s' \in \mathcal{T}(P')} \lambda x.s' = \sum_{s \in \mathcal{T}(P)} \lambda x.S'_s, $$

with $\lambda x.s \to_r^* \lambda x.S'_s$, so $\mathcal{T}(M) \underset{\sim}{\to}_r^* \mathcal{T}(N)$.

* Case $(@l_\beta)$: similar to the previous one.

* Case $(@r_\beta)$. Take $M = (P)Q \to_\beta (P)Q' = N$, with $Q \to_\beta Q'$. By induction, we have $\mathcal{T}(Q) \underset{\sim}{\to}_r^* \mathcal{T}(Q')$, that is $\mathcal{T}(Q') = \sum_{t \in \mathcal{T}(Q)} T'_t$ with $t \to_r^* T'_t$. Then:

$$ \mathcal{T}(M) = \sum_{s \in \mathcal{T}(P)} \sum_{\bar{t} \in \mathcal{T}(Q)!} \langle s \rangle \bar{t} $$

and:

$$ \begin{aligned} \mathcal{T}(N) &= \sum_{s \in \mathcal{T}(P)} \sum_{\bar{t}' \in \mathcal{T}(Q)!} \langle s \rangle \bar{t}' \\ &= \sum_{s \in \mathcal{T}(P)} \sum_{k \in \mathbf{N}} \sum_{t'_1 \in \mathcal{T}(Q')} \cdots \sum_{t'_k \in \mathcal{T}(Q')} \langle s \rangle [t'_1, \dots, t'_k] \\ &= \sum_{s \in \mathcal{T}(P)} \sum_{k \in \mathbf{N}} \sum_{t_1 \in \mathcal{T}(Q)} \cdots \sum_{t_k \in \mathcal{T}(Q)} \langle s \rangle [T'_{t_1}, \dots, T'_{t_k}] \\ &= \sum_{s \in \mathcal{T}(P)} \sum_{\bar{t} \in \mathcal{T}(Q)!} \langle s \rangle [T'_{t_1}, \dots, T'_{t_{\#\bar{t}}}] \end{aligned} $$

Yet for any $\bar{t} \in \mathcal{T}(Q)$ and for all $t_i \in \bar{t}$, $t_i \to_r^* T'_{t_i}$, so $\langle s \rangle \bar{t} \to_r^* \langle s \rangle [T'_{t_1}, \dots, T'_{t_{\#\bar{t}}}]$. This leads to $\mathcal{T}(M) \underset{\sim}{\to}_r^* \mathcal{T}(N)$.

We conclude in the general case $M \to_\beta^* N$ using Lemma 3.18. $\square$

4.2. A “step-by-step” decomposition of the reduction. Since an infinitary reduction must reduce redexes whose depth tends to infinity, we want to decompose reductions into an infinite succession of finite reductions occuring at lower-bounded depth (in the following, we name these *min-depth* reductions, for reductions occuring “at a minimal depth”). As a side consequence, we obtain a result of (weak) standardisation for $\Lambda_\infty^{001}$.

**Definition 4.3** (min-depth finitary $\beta$-reduction). The reduction $\to_{\beta \ge d} \subset \Lambda_\infty^{001} \times \Lambda_\infty^{001}$ is defined for all $d \in \mathbf{N}$ by the rules:

$$ \begin{aligned} \frac{M \to_\beta N}{M \to_{\beta \ge 0} N} & (\alpha_{\beta \ge 0}) & \frac{M \to_{\beta \ge d+1} N}{\lambda x.M \to_{\beta \ge d+1} \lambda x.N} & (\lambda_{\beta \ge d+1}) \\ \frac{M \to_{\beta \ge d+1} N}{(M)P \to_{\beta \ge d+1} (N)P} & (@l_{\beta \ge d+1}) & \frac{M \to_{\beta \ge d} N}{(P)M \to_{\beta \ge d+1} (P)N} & (@r_{\beta \ge d+1}) \end{aligned} $$
**Remark 4.4.** It is easy to check that if $M \to_{\beta \ge d} N$ then $M \to_{\beta} N$, and $M \to_{\beta \ge d'} N$ whenever $d \ge d'$. Moreover, one can show by induction on $d$ that $\to_{\beta \ge d}^*$ can be defined directly by the following rules:

$$ \begin{gathered} \frac{M \to_{\beta}^* M'}{M \to_{\beta \ge 0}^* M'} (\mathrm{ax}_{\beta \ge 0}^*) \qquad \xrightarrow{x \to_{\beta \ge d+1}^* x} (\mathcal{V}_{\beta \ge d+1}^*) \\ \frac{M \to_{\beta \ge d+1}^* M'}{\lambda x.M' \to_{\beta \ge d+1}^* \lambda x.M'} (\lambda_{\beta \ge d+1}^*) \qquad \frac{M \to_{\beta \ge d+1}^* M' \quad N \to_{\beta \ge d}^* N'}{(M)N \to_{\beta \ge d+1}^* (M')N'} (\mathrm{ax}_{\beta \ge d+1}^*) \end{gathered} $$

and the infinitary version to be defined below will follow the same pattern.

**Definition 4.5 (min-depth resource reduction).** The reduction $\mapsto_{r \ge d} \subset \Lambda_r^{(l)} \times 2\langle\Lambda_r^{(l)}\rangle$ is defined for all $d \in \mathbb{N}$ by the rules:

$$ \begin{gathered} \frac{s \mapsto_r S}{s \mapsto_{r \ge 0} S} (\mathrm{ax}_{r \ge 0}) \qquad \frac{s \mapsto_{r \ge d+1} S}{\lambda x.s \mapsto_{r \ge d+1} \lambda x.S} (\lambda_{r \ge d+1}) \qquad \frac{s \mapsto_{r \ge d+1} S}{\langle s \rangle \bar{t} \mapsto_{r \ge d+1} \langle S \rangle \bar{t}} (@_{l \ge d+1}) \\ \frac{\bar{t} \mapsto_{r \ge d+1} \bar{T}}{\langle s \rangle \bar{t} \mapsto_{r \ge d+1} \langle s \rangle \bar{T}} (@_{r \ge d+1}) \qquad \frac{s \mapsto_{r \ge d} S}{s \cdot \bar{t} \mapsto_{r \ge d+1} S \cdot \bar{t}} (!_{r \ge d+1}) \end{gathered} $$

where $d \in \mathbb{N}$. We also extend $\mapsto_{r \ge d}$ to $\to_{r \ge d} \subset 2\langle\Lambda_r\rangle \times 2\langle\Lambda_r\rangle$ in the same way as in Definition 3.4 by adding a rule $(\Sigma_{r \ge d})$.

**Lemma 4.6 (simulation of min-depth finitary reduction).** Let $M, N \in \Lambda_{\infty}^{001}$ be terms, and $d \in \mathbb{N}$. If $M \to_{\beta \ge d}^* N$, then $T(M) \xrightarrow{\sim} T(N)$.

*Proof.* By induction on $\to_{\beta \ge d}^*$. In the case $(\mathrm{ax}_{\beta \ge 0})$, just apply Lemma 4.2. In the other cases, the proof is analogous to the corresponding cases in Lemma 4.2. $\square$

**Definition 4.7 (min-depth infinitary $\beta$-reduction).** The reduction $\to_{\beta \ge d}^{\infty}$ is defined for all $d \in \mathbb{N}$ by the rules:

$$ \begin{gathered} \frac{M \to_{\beta}^{\infty} M'}{M \to_{\beta \ge 0}^{\infty} M'} (\mathrm{ax}_{\beta \ge 0}^{\infty}) \qquad \xrightarrow{x \to_{\beta \ge d+1}^{\infty} x} (\mathcal{V}_{\beta \ge d+1}^{\infty}) \\ \frac{M \to_{\beta \ge d+1}^{\infty} M'}{\lambda x.M' \to_{\beta \ge d+1}^{\infty} \lambda x.M'} (\lambda_{\beta \ge d+1}^{\infty}) \qquad \frac{M \to_{\beta \ge d+1}^{\infty} M' \quad N \to_{\beta \ge d}^{\infty} N'}{(M)N \to_{\beta \ge d+1}^{\infty} (M')N'} (\mathrm{ax}_{\beta \ge d+1}^{\infty}) \end{gathered} $$

where $d \in \mathbb{N}^*$.

**Lemma 4.8.** Each relation $\to_{\beta \ge d}^{\infty}$ is reflexive and transitive, and moreover such that $\to_{\beta \ge d+1}^{\infty} \subseteq \to_{\beta \ge d}^{\infty} \subseteq \to_{\beta}^{\infty}$.

*Proof.* Reflexivity and transitivity of $\to_{\beta \ge 0}^{\infty}$ are derived from that of $\to_{\beta}^{\infty}$. Reflexivity of each $\to_{\beta \ge d}^{\infty}$ follows by induction on $d$: in the inductive step, we reason by induction on the top-level (inductive only) structure of terms. Transitivity of each $\to_{\beta \ge d}^{\infty}$ follows, again by
a straightforward induction on $d$, and by induction on derivations of $\to_{\beta \ge d}^{\infty}$. The identity $\to_{\beta \ge 0}^{\infty} = \to_{\beta}^{\infty}$ is straightforward. The inclusion $\to_{\beta \ge 1}^{\infty} \subseteq \to_{\beta}^{\infty}$ is proved by induction on the derivations of $\to_{\beta \ge 1}^{\infty}$, using the reflexivity and transitivity of $\to_{\beta}^{\infty}$. The inclusion $\to_{\beta \ge d+1}^{\infty} \subseteq \to_{\beta \ge d}^{\infty}$ follows by induction on $d$, and then by induction on the derivations of $\to_{\beta \ge d+1}^{\infty}$. $\square$

**Lemma 4.9.** If $M \to_{\beta}^{\infty} M'$, then there exists a term $M_0 \in \Lambda_{\infty}^{001}$ such that $M \to_{\beta}^{*} M_0 \to_{\beta \ge 1}^{\infty} M'$.

*Proof.* We define $M_0$ and the reduction $M_0 \to_{\beta \ge 1}^{\infty} M'$ by reasoning on the inductive layer of the reduction $M \to_{\beta}^{\infty} M'$.

* Case $(\mathrm{ax}_{\beta}^{\infty})$, $M \to_{\beta}^{*} x = M'$. We can set $M_0 := x \to_{\beta \ge 1}^{\infty} M'$, using the reflexivity of $\to_{\beta \ge 1}^{\infty}$.

* Case $(\lambda_{\beta}^{\infty})$, $M \to_{\beta}^{*} \lambda x.P$ and $M' = \lambda x.P'$ with $P \to_{\beta}^{\infty} P'$. The induction hypothesis yields $P_0$ such that $P \to_{\beta}^{*} P_0 \to_{\beta \ge 1}^{\infty} P'$, and we can set $M_0 := \lambda x.P_0$ and obtain $M_0 \to_{\beta \ge 1}^{\infty} M'$ by rule $(\lambda_{\beta \ge 1}^{\infty})$.

* Case $(\mathrm{@}_{\beta}^{\infty})$, $M \to_{\beta}^{*} (P)Q$ and $M' = P'Q'$ with $P \to_{\beta}^{\infty} P'$ and $Q \to_{\beta}^{\infty} Q'$. The induction hypothesis applies to the first reduction, which yields $P_0$ such that $P \to_{\beta}^{*} P_0 \to_{\beta \ge 1}^{\infty} P'$. Rule $(\mathrm{ax}_{\beta \ge 0}^{\infty})$ entails $Q \to_{\beta \ge 0}^{\infty} Q'$. We can set $M_0 := (P_0)Q$, and obtain $M_0 \to_{\beta \ge 1}^{\infty} M'$ by rule $(\mathrm{@}_{\beta \ge 1}^{\infty})$. $\square$

**Lemma 4.10.** If $M \to_{\beta \ge d}^{\infty} M'$, then there exists a term $M_d \in \Lambda_{\infty}^{001}$ such that $M \to_{\beta \ge d}^{*} M_d \to_{\beta \ge d+1}^{\infty} M'$.

*Proof.* We define $M_d$ and the reductions $M \to_{\beta \ge d}^{*} M_d \to_{\beta \ge d+1}^{\infty} M'$ by induction on the reduction $M \to_{\beta \ge d}^{\infty} M'$. The case of rule $(\mathrm{ax}_{\beta \ge 0}^{\infty})$ is given by the previous Lemma. All the other cases are straightforward using the induction hypothesis. $\square$

**Lemma 4.11.** For all $M, N \in \Lambda_{\infty}^{001}$ such that $M \to_{\beta}^{\infty} N$, there is a sequence of terms $(M_d)_{d \in \mathbb{N}}$ such that for all $d \in \mathbb{N}$:

$$M = M_0 \to_{\beta \ge 0}^{*} M_1 \to_{\beta \ge 1}^{*} M_2 \to_{\beta \ge 2}^{*} \dots \to_{\beta \ge d-1}^{*} M_d \to_{\beta \ge d}^{\infty} N.$$

*Proof.* We construct the sequence $(M_d)_{d \in \mathbb{N}}$ inductively, by applying the previous Lemma. $\square$

**Remark 4.12** (standardisation for $\to_{\beta}^{\infty}$). The decomposition of Lemma 4.11 can be slightly improved: if $M \to_{\beta}^{\infty} N$, there exist $M_0, M_1, M_2, \dots \in \Lambda_{\infty}^{001}$ such that, for all $d \in \mathbb{N}$:

$$M = M_0 \to_{\beta=0}^{*} M_1 \to_{\beta=1}^{*} M_2 \to_{\beta=2}^{*} \dots \to_{\beta=d-1}^{*} M_d \to_{\beta \ge d}^{\infty} N$$

where $\to_{\beta=d}$ is defined as expected. This consequence is a weak counterpart to Curry and Feys' standardisation theorem for the $\lambda$-calculus [CF58]. Another, similar, standardisation theorem has been proved for $\Lambda_{\infty}^{111}$ by Endrullis and Polonsky, using coinductive techniques [EP13].

*Sketch of proof.* Using a classical result [Bar84, lemma 11.4.6] which can be easily adapted to $\Lambda_{\infty}^{001}$, $M \to_{\beta}^{*} N$ can be decomposed into head and internal reductions: $M \to_{h}^{*} M' \to_{i}^{*} N$. Using this, one can prove by induction on $N$ that $M \to_{\beta=0}^{*} M_1 \to_{\beta \ge 1}^{*} N$. Indeed, we can write either

$$N = \lambda x_1 \dots x_m (\dots ((y)Q_1) \dots) Q_n$$
in case it is a head normal form, or

$$N = \lambda x_1 \dots x_m (\dots ((\lambda z.P)Q_0) \dots) Q_n$$

if it has a head redex; and then by the definition of internal reduction we must have respectively

$$M' = \lambda x_1 \dots x_m (\dots ((y)Q'_1) \dots) Q'_n$$

or

$$M' = \lambda x_1 \dots x_m (\dots ((\lambda z.P')Q'_0) \dots) Q'_n$$

with $Q'_i \to_{\beta}^* Q_i$ for each $i$, and also $P' \to_{\beta}^* P$ in the second case. In the case of a head normal form, we obtain $M' \to_{\beta \ge 1}^* N$ so we can set $M_1 := M'$ directly. In the other case, we use the induction hypothesis on $P'$, to obtain $P_1$ such that $P' \to_{\beta=0}^* P_1 \to_{\beta \ge 1}^* N$, and then set

$$M_1 := \lambda x_1 \dots x_m (\dots ((\lambda z.P_1)Q'_0) \dots) Q'_n$$

so that $M \to_{\beta=0}^* M' \to_{\beta=0}^* M_1 \to_{\beta \ge 1}^* N$.

Then one deduces that $M \to_{\beta \ge d}^* N$ implies $M \to_{\beta=d}^* M_d \to_{\beta \ge d+1}^* N$, by induction on the derivation of $M \to_{\beta \ge d}^* N$. Standardisation follows by applying this result to the sequence of reductions obtained by Lemma 4.11. $\square$

We do not detail the proof (nor the definition of $\to_{\beta=d}^*$) further, because this standardisation result is not used in the following: at this point of the paper, the interested reader already has all the tools to complete the construction.

**4.3. Decomposing the decomposition.** Each finite, min-depth reduction occuring in the decomposition of Lemma 4.11 can be simulated by the Taylor expansion. Using this fact, we can track the successive reducts of each approximant in the Taylor expansion of the original term $M$, providing a decomposition of each $\mathcal{T}(M_d)$ into finite sums of approximants.

**Lemma 4.13 (additive splitting).** Let $S, T \subset \Lambda_r$ be sets, and $d \in \mathbb{N}$. If $S \xrightarrow{\sim} T$ then, whenever we write $S = \sum_{i \in I} S_i$ where each $S_i$ is a finite sum, there exist finite sums $T_i$ for $i \in I$, such that $T = \sum_{i \in I} T_i$ and $\forall i \in I$, $S_i \to_{r \ge d}^* T_i$.

*Proof.* For each $i \in I$, write $S_i = \sum_{j \in J_i} s_{i,j}$ with $s_{i,j} \in \Lambda_r$, so that $S = \sum_{i \in I} \sum_{j \in J_i} s_{i,j}$. Since $S \xrightarrow{\sim} T$ and using Remark 3.15, there are finite sums $T_s$ for $s \in S$ such that $T = \sum_{s \in S} T_s$ and $\forall s \in S$, $s \to_{r \ge d}^* T_s$. Define, for each $i \in I$, $T_i := \sum_{j \in J_i} T_{s_{i,j}}$. It is straightforward to prove that for all $i \in I$, $S_i \to_{r \ge d}^* T_i$ (by induction on the sum of the lengths of reductions $s_{i,j} \to_{r \ge d}^* T_{s_{i,j}}$ for $j \in J_i$). $\square$

**Corollary 4.14.** Let $M, N \in \Lambda_{\infty}^{001}$ be terms such that $M \to_{\beta}^{\infty} N$, and $(M_d)_{d \in \mathbb{N}}$ given by Lemma 4.11. If $\mathcal{T}(M) = \sum_{i \in I} s_i$, then for each $d \in \mathbb{N}$ there exist finite sums $(T_{d,i})_{i \in I}$ such that:

(1) $\forall i \in I, T_{0,i} = s_i,$

(2) $\forall d \in \mathbb{N}, \mathcal{T}(M_d) = \sum_{i \in I} T_{d,i},$

(3) $\forall d \in \mathbb{N}, \forall i \in I, T_{d,i} \to_{r \ge d}^* T_{d+1,i}.$

*Proof.* For each $i \in I$, set $T_{0,i} := s_i$ and define $T_{d,i}$ by induction on $d$ using the previous lemma and the fact that $\mathcal{T}(M_d) \xrightarrow{\sim} T(M_{d+1})$, which is a consequence of Lemma 4.6. $\square$
4.4. **Height of a resource term.** We show a few properties of the interplay between the size and the height (wrt. the 001-depth) of a term, that will play a crucial role in the main proof.

**Definition 4.15 (height of resource terms).** The height $h^{001}(\cdot)$ of resource terms is defined inductively by:

$$ 
\begin{align*}
h^{001}(x) &:= 0 \\
h^{001}(\lambda x.s) &:= h^{001}(s) \\
h^{001}(\langle s \rangle \bar{t}) &:= \max(h^{001}(s), h^{001}(\bar{t})) \\
h^{001}([t_1, \dots, t_n]) &:= 1 + \max_{1 \le i \le n} h^{001}(t_i)
\end{align*}
$$

The height of a finite sum $S \in 2\langle\Lambda_r\rangle$ is given by $h^{001}(S) := \max_{s \in S} h^{001}(s)$ — by convention, $h^{001}(0) = 0$.

**Lemma 4.16.** For all $S \in 2\langle\Lambda_r\rangle$, $h^{001}(S) \le |S|$.

*Proof.* Show the result for $s \in \Lambda_r$ by an immediate induction on $s$. Conclude by taking the maximum over $s \in S$. $\square$

**Lemma 4.17.** Let $S \in 2\langle\Lambda_r\rangle$ be a finite sum of resource terms and $d \in \mathbb{N}$ such that $d > h^{001}(S)$. Then there is no reduction $S \to_{r \ge d} S'$.

*Proof.* The result immediately follows from the fact that given $d$, $s$ and $S'$, if $s \mapsto_{r \ge d} S'$ then $d \le h^{001}(s)$. We prove this by induction on the derivation $s \mapsto_{r \ge d} S'$.

* Case $(\max_{r \ge 0}), d = 0$ and the result is trivial.

* Case $(\lambda_{r \ge d+1}), s = \lambda x.u$ and $S' = \lambda x.U'$ with $u \to_{r \ge d+1} U'$. We conclude directly by the induction hypothesis since $h^{001}(u) = h^{001}(u)$.

* Cases $(@l_{r \ge d+1})$ and $(@r_{r \ge d+1})$ are similar to the previous one.

* Cases $(!_{r \ge d+1}), \bar{s} = [t] \cdot \bar{u}$ and $\bar{S}' = [T'] \cdot \bar{u}$ with $t \to_{r \ge d} T'$. By induction hypothesis, we have $d \le h^{001}(t)$, hence $d+1 \le 1 + h^{001}(t) \le \max(1+h^{001}(t), h^{001}(\bar{u})) = h^{001}(\bar{s})$. $\square$

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

4.5. **The diagonal argument.** Finally, we conclude by a sort of diagonal argument: $\mathcal{T}(N)$ is shown to be the union of the $T_{i,d_i}$, each of these finite sums being finitely reached from some $s_i \in \mathcal{T}(M)$. In that sense, we obtain a pointwise finitary simulation of the infinitary reduction.

The key definition is somehow complementary to the min-depth reduction: it is the Taylor expansion at (upper-)bounded depth, defined hereunder. Concretely, $\mathcal{T}_{<d}(M)$ is the sum of all approximants $s \in \mathcal{T}(M)$ such that $h^{001}(s) < d$.

**Definition 4.18 (bounded-depth Taylor expansion).** For all $d \in \mathbb{N}$, the relation $\llcorner_d$ of Taylor approximation at depth bounded by $d$ is inductively defined on $\Lambda_r \times \Lambda_\infty^{001}$ by $\llcorner_d := \emptyset$ and by the following rules:
$$ \overline{x \prec_{<d+1} x} (\mathrm{ax}_{\prec_{<d+1} x}) \qquad \frac{s \prec_{<d+1} M}{\lambda x.s \prec_{<d+1} \lambda x.M} (\lambda_{\prec_{<d+1}}) $$

$$ \frac{s \prec_{<d+1} M \quad \bar{t} \prec_{<d+1} N}{\langle s \rangle \bar{t} \prec_{<d+1} (M)N} (@_{\prec_{<d+1}}) \qquad \frac{(t_i \prec_{<d} M)_{i=1}^n}{[t_1, \dots, t_n] \prec_{<d+1} M} (!_{\prec_{<d+1}}) $$

The Taylor expansion of a term $M \in \Lambda_{\infty}^{001}$ at depth bounded by $d$ is the set $\mathcal{T}_{<d}(M) := \sum_{s \prec_{<d} M} s$. We also write $\mathcal{T}_{<d}^{!}(M) := \sum_{\bar{s} \prec_{<d} M} \bar{s}$.

It should be clear that we have $s \prec_{<d} M$ iff $s \prec M$ and $h^{001}(s) < d$, so that we obtain the following Lemma.

**Lemma 4.19.** Let $M \in \Lambda_{\infty}^{001}$ be a term, $S \in 2\langle\Lambda_r\rangle$ a finite sum of resource terms, and $d \in \mathbb{N}$. If $S \subset \mathcal{T}(M)$ and $h^{001}(S) < d$, then $S \subset \mathcal{T}_{<d}(M)$.

**Lemma 4.20.** Let $M, N \in \Lambda_{\infty}^{001}$ be terms. If $M \to_{\beta \ge d} N$ then $\mathcal{T}_{<d}(M) = \mathcal{T}_{<d}(N)$.

*Proof.* We prove the result by induction on $M \to_{\beta \ge d} N$.

* Case $(\mathrm{ax}_{\beta \ge 0})$, $\mathcal{T}_{<0}(M) = 0 = \mathcal{T}_{<0}(N)$.

* Case $(\mathcal{V}_{\beta \ge d+1})$, $N = x = M$ so $\mathcal{T}_{<d+1}(M) = x = \mathcal{T}_{<d+1}(N)$.

* Case $(\lambda_{\beta \ge d+1})$, $M = \lambda x.P \to_{\beta \ge d+1} \lambda x.P' = N$, with $P \to_{\beta \ge d+1} P'$. By induction, $\mathcal{T}_{<d+1}(P) = \mathcal{T}_{<d+1}(P')$ so $\mathcal{T}_{<d+1}(M) = \mathcal{T}_{<d+1}(N)$ using the rule $(\lambda_{\prec_{<d+1}})$.

* Case $(@_{\beta \ge d+1})$, $M = (P)Q \to_{\beta \ge d+1} (P')Q' = N$, with $P \to_{\beta \ge d+1} P$ and $Q \to_{\beta \ge d} Q'$. By induction, $\mathcal{T}_{<d+1}(P) = \mathcal{T}_{<d+1}(P')$ and $\mathcal{T}_{<d}(Q) = \mathcal{T}_{<d}(Q')$, so $\mathcal{T}_{<d+1}^{!}(Q) = \mathcal{T}_{<d+1}^{!}(Q')$ by the rule $(!_{\prec_{<d+1}})$, and finally $\mathcal{T}_{<d+1}(M) = \mathcal{T}_{<d+1}(N)$ by the rule $(@_{\prec_{<d+1}})$).

□

**Theorem 4.21** (simulation of the infinitary reduction). Let $M, N \in \Lambda_{\infty}^{001}$ be terms. If $M \to_{\beta}^{\infty} N$, then $\mathcal{T}(M) \xrightarrow{\sim_r^*} \mathcal{T}(N)$.

*Proof.* Suppose $M \to_{\beta}^{\infty} N$. By Lemma 4.11, we obtain terms $M_0, M_1, M_2, \dots \in \Lambda_{\infty}^{001}$ such that, for all $d \in \mathbb{N}$:

$$ M = M_0 \to_{\beta \ge 0}^* M_1 \to_{\beta \ge 1}^* M_2 \to_{\beta \ge 2}^* \dots \to_{\beta \ge d-1}^* M_d \to_{\beta \ge d}^* N. $$

Writing $\mathcal{T}(M) = \sum_{i \in I} s_i$, Corollary 4.14 yields finite sums $T_{d,i}$ such that:

(1) $\forall i \in I, T_{0,i} = s_i$,

(2) $\forall d \in \mathbb{N}, \mathcal{T}(M_d) = \sum_{i \in I} T_{d,i}$,

(3) $\forall d \in \mathbb{N}, \forall i \in I, T_{d,i} \xrightarrow{r \ge d} T_{d+1,i}$.

For $i \in I$, define $d_i := |s_i| + 1$ and $T_i := T_{d_i,i}$. Using Lemma 4.16, for all $d \in \mathbb{N}$, $h^{001}(T_{d,i}) \le |T_{d,i}| \le |s_i|$. Thus, $h^{001}(T_i) < d_i$.

* From Lemma 4.19 and Lemma 4.20, we have $T_i \subset \mathcal{T}_{<d_i}(M_{d_i}) = \mathcal{T}_{<d_i}(N) \subset \mathcal{T}(N)$. Hence, $\sum_{i \in I} T_i \subseteq \mathcal{T}(N)$.

* Take $t \in \mathcal{T}(N)$. From Lemma 4.19, $t \in \mathcal{T}_{<h}(N)$ where $h := h^{001}(t) + 1$. With Lemma 4.20, $t \in \mathcal{T}_{<h}(M_h) \subset \mathcal{T}(M_h)$, so $\exists i \in I, t \in T_{h,i}$. For all $d \ge h$, $T_{h,i} \xrightarrow{r \ge h} T_{d,i}$ so, by Lemma 4.17, $t \in T_{d,i}$.

Notice that for all $d \ge d_i$, $T_i \xrightarrow{r \ge d_i} T_{d,i}$ so using again Lemma 4.17, $T_{d,i} = T_i$.

Thus, if we take $d \ge \max(h, d_i)$, we obtain $t \in T_i$. This leads us to $\mathcal{T}(N) \subseteq \sum_{i \in I} T_i$.
Finally, $\mathcal{T}(M) = \sum_{i \in I} s_i$, $\mathcal{T}(N) = \sum_{i \in I} T_i$, and $\forall i \in I$, $s_i \to_r^* T_i$. This implies the theorem. □

**Remark 4.22** (models of $\Lambda_\infty^{001}$). An important consequence of this simulation result is that any model $\mathcal{M}$ of $\Lambda_r$ is also a model of $\Lambda_\infty^{001}$, as soon as it makes sense to consider infinite sets of resource terms: it suffices to interpret any term $M \in \Lambda_\infty^{001}$ by $[[M]]_\mathcal{M} := \bigoplus_{s \in \mathcal{T}(M)} [[s]]_\mathcal{M}$. This is in particular the case of the well-known construction of a reflexive object $\mathcal{D}$ in the category **MRel** [BEM07].

## 5. HEAD REDUCTION AND NORMALISATION PROPERTIES

In this final part, we show several consequences of Theorem 4.21. Most of them are unsurprising, which is good news: we want $\Lambda_\infty^{001}$ to be a convenient framework to consider reductions and normal forms of the usual $\lambda$-terms. In particular, head- and $\beta$-normalisation can be characterised in a similar fashion as in the finitary $\lambda$-calculus, and we prove infinitary counterparts to well-known results such as the Commutation theorem and the Genericity lemma.

**5.1. Solvability in $\Lambda_\infty^{001}$**. The definition of $\Lambda_\infty^{001}$ is tightly related to head reduction: the inductive/coinductive structure of 001-infinitary terms follows the head structure of terms; and since $\to_{\beta \ge 0}$ contains head reduction, Lemma 4.11 entails that any $\to_{\beta}$-reduction involves only finitely many head reduction steps.

The good properties of head reduction should thus be preserved when moving from $\Lambda$ to $\Lambda_\infty^{001}$. This is indeed the case, as expressed by Theorem 5.6: a 001-infinitary term is head-normalising if and only if the head reduction strategy terminates. As a consequence, we will show that the notion of solvability is completely preserved in $\Lambda_\infty^{001}$.

**Lemma 5.1** (head forms). Let $M \in \Lambda_\infty^{001}$ be a term, then either

$$M = \lambda x_1 \dots \lambda x_m (\dots ((\lambda z.N)P) Q_1) \dots) Q_n$$

or:

$$M = \lambda x_1 \dots \lambda x_m (\dots ((y)Q_1) \dots) Q_n$$

where $m, n \in \mathbb{N}$, $x_1, \dots, x_m, y, z \in \mathcal{V}$ and $N, P, Q_1, \dots, Q_n \in \Lambda_\infty^{001}$. In the first case, $(\lambda y.N)P$ is the head redex of $M$. In the second case, $M$ is in head normal form (HNF).

Similarly, a resource term $s \in \Lambda_r$ can always be written $s = \lambda x_1 \dots \lambda x_m \langle \dots \langle \langle u \rangle \bar{t}_1 \rangle \dots \rangle \bar{t}_n$ where $u$ is either a (head) redex or a variable.

*Proof.* By induction, following the inductive structure of $M$ (we do not need to cross any coinductive rule here, and remain within the first “coinductive level” of $M$; thus, the proof is exactly the same as in the finitary case). □

**Definition 5.2** (head reductions). The *head reduction* is the relation $\to_h$ defined on $\Lambda_\infty^{001}$ so that $M \to_h N$ if $N$ is obtained by reducing the head redex of $M$.

Similarly, the *resource head reduction* is the relation $\to_{rh}$ defined on $\Lambda_r$ such that $s \to_{rh} T$ if $T$ is obtained by reducing the head redex of $s$. It is extended to $\to_{rh}$ on $2\langle\Lambda_r\rangle$ in the same way as $\to_r$.
**Notation 5.3** (head reduction operators). If $M \in \Lambda_{\infty}^{001}$ we set: $H(M) := N$ if $M \to_h N$; and $H(M) := M$ if $M$ is in HNF.

Similarly, if $s \in \Lambda_r$ we set: $H_r(s) := T$ if $s \mapsto_{rh} T$; and $H(s) := s$ if $s$ is in HNF. This operator is extended to $2\langle\Lambda_r\rangle$ by $H_r(\sum_i s_i) := \sum_i H_r(s_i)$.

**Lemma 5.4** (simulation of the head reduction operator). Let $M \in \Lambda_{\infty}^{001}$ be a term, then $H_r(\mathcal{T}(M)) = \mathcal{T}(H(M))$.

*Proof.* Direct consequence of Lemma 4.1. □

**Lemma 5.5** (termination of the resource head reduction operator). Let $S \in 2\langle\Lambda_r\rangle$ be a sum of resource terms, then there exists $k \in \mathbb{N}$ such that $H_r^k(S)$ is in HNF.

*Proof.* Given $S \in 2\langle\Lambda_r\rangle$, write $S = S' + S_{\text{HNF}}$ where $S_{\text{HNF}}$ contains the terms of $S$ in HNF. By definition of $H_r$, we have $H_r(S) = H_r(S') + S_{\text{HNF}}$ with $|H_r(S')| < |S'|$ from Lemma 3.7 whenever $S' \neq 0$, so that $\|H_r(S)\| < \|S\|$ in this case — with the notation of Lemma 3.9. We conclude by the well-foundedness of $\prec$.

Now we provide a characterisation of head-normalising infinitary terms based on their Taylor expansion. In a finitary setting, this result has been folklore for some time [Oli18; Oli20].

**Theorem 5.6** (characterisation of head-normalising terms). Let $M \in \Lambda_{\infty}^{001}$ be a term, then the following propositions are equivalent:

(1) there exists $N \in \Lambda_{\infty}^{001}$ in HNF such that $M \to_{\beta}^{\infty} N$,

(2) there exists $s \in \mathcal{T}(M)$ such that $nf_r(s) \neq 0$,

(3) there exists $N \in \Lambda_{\infty}^{001}$ in HNF such that $M \to_h^* N$.

*Proof.* Suppose (1), that is $M \to_{\beta}^{\infty} N = \lambda x_1 \dots \lambda x_m \dots ((y)N_1) \dots) N_n$. In particular, $\mathcal{T}(N)$ contains $t_0 = \lambda x_1 \dots \lambda x_m \dots \langle\langle y \rangle\rangle 1 \dots \rangle 1$, which is normal. Using Theorem 4.21, there exists $s \in \mathcal{T}(M)$ and $T \in \mathcal{T}(N)$ such that $s \to_r^* t_0 + T$ which proves (2).

Now, suppose that (2) holds, that is $s \to_r^* t_0 + T$ with $t_0$ in normal form. According to Lemma 5.5, there is a $k \in \mathbb{N}$ such that $H_r^k(s)$ is in HNF. Thus, using confluence, there exists a $U \in 2\langle\Lambda_r\rangle$ such that: $t_0 + T \to_r^* U$ and $H_r^k(s) \to_r^* U$. Since $t_0$ is in normal form, $t_0 \in U$. Thus, $H_r^k(s) \neq 0$, so there exists a term

$$ \lambda x_1 \dots \lambda x_m \langle\dots\langle\langle y \rangle\rangle \bar{t}_1 \dots\rangle \bar{t}_n \in H_r^k(s) \in H_r^k(\mathcal{T}(M)) = \mathcal{T}(H^k(M)), $$

by Lemma 5.4. As a consequence, $H^k(M)$ has shape $\lambda x_1 \dots \lambda x_m \dots ((y)M_1) \dots) M_n$, which shows (3).

Finally, (1) is as immediate consequence of (3). □

A first notable consequence of the previous result is the equivalence of head-normalisation and solvability. In the finitary $\lambda$-calculus, this is a well-known theorem [Wad76]. The following proof, based on the Taylor expansion and inspired by [Oli20], is much simpler than the original one.

**Definition 5.7** (solvability). A term $M \in \Lambda_{\infty}^{001}$ is said to be *solvable* in $\Lambda$ (resp. in $\Lambda_{\infty}^{001}$) if there exist $x_1, \dots, x_m \in \mathcal{V}$ and $N_1, \dots, N_n \in \Lambda$ (resp. $\Lambda_{\infty}^{001}$) such that

$$ ((\lambda x_1 \dots \lambda x_m M) N_1) \dots) N_n \to_{\beta}^* \lambda x.x \quad (\text{resp. } \to_{\beta}^{\infty}). $$

Otherwise, $M$ is unsolvable.
**Corollary 5.8 (characterisation of solvable terms).** Let $M \in \Lambda_{\infty}^{001}$ be a term, then the following propositions are equivalent:

(1) M is solvable in $\Lambda_{\infty}^{001}$,

(2) M is head-normalising,

(3) M is solvable in $\Lambda$.

*Proof.* Suppose (1), i.e. there exists $x_1, \dots, x_m \in \mathcal{V}$ and $N_1, \dots, N_n \in \Lambda_{\infty}^{001}$ such that

$$ (\dots ((\lambda x_1 \dots \lambda x_m.M)N_1)\dots)N_n \xrightarrow{\beta} \lambda x.x, $$

which is in HNF. Then, according to Theorem 5.6, there is an

$$ s \in \mathcal{T}((\dots ((\lambda x_1 \dots \lambda x_m.M)N_1)\dots)N_n) $$

such that $nf_r(s) \neq 0$. This resource term has shape

$$ s = \langle \dots \langle \langle \lambda x_1 \dots \lambda x_m.u \rangle \bar{t}_1 \rangle \dots \rangle \bar{t}_n $$

with $u \in \mathcal{T}(M)$ and $\bar{t}_i \in \mathcal{T}(N_i)$. We must have $nf_r(u) \neq 0$, which leads to (2), again with Theorem 5.6.

Now, suppose (2). Theorem 5.6 gives $M \xrightarrow{h}^* \lambda x_1 \dots \lambda x_m. (\dots ((y)M_1)\dots) M_n$. Then:

* if $y = x_i$, then $(M)(K^n I)^{(m)} \xrightarrow{\beta} I$,

* otherwise, $((\lambda y.M)K^n I) I^{(m)} \xrightarrow{\beta} I$,

using Notation 2.5 and the usual terms $I := \lambda x.x$ and $K := \lambda x.\lambda y.x$. This shows (3).

The implication from (3) to (1) is direct, by Lemma 2.13. $\square$

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

**5.2. Normalisation, confluence and the Commutation Theorem.** We shall now address the key properties of normalisation and confluence in $\Lambda_{\infty}^{001}$. It is known since Kennaway et al.'s seminal paper [Ken+97] that, even though the infinitary $\lambda$-calculi are not strongly normalising (in any version $\Lambda_{\infty}^{abc}$, there is no strongly convergent reduction from the term $\Omega$ to a normal form), the so-called $\beta$-$\perp$-reduction is normalising and confluent in $\Lambda_{\infty}^{001}$, $\Lambda_{\infty}^{101}$ and $\Lambda_{\infty}^{111}$. This is a confluence “up to a set of meaningless terms”, which are forced to reduce to a constant $\perp$ (this technique was introduced by [Ber96] and [Ken+97; KOV96]; for a summary, see [BM22, § 6.3]). In the case of $\Lambda_{\infty}^{001}$, the meaningless terms are the unsolvable ones.

In this part, we use the Taylor expansion and a new version of Ehrhard and Regnier's Commutation theorem to give a simple presentation of normalisation, confluence, and a few other noteworthy corollaries.

First, we have to add the constant $\perp$ to our language, and to update the definition of the reductions and of the Taylor expansion correspondingly.

**Definition 5.9 ($\lambda$-$\perp$-terms).** Given a set of variables $\mathcal{V}$, the set $\Lambda_{\infty\perp}^{001}$ of 001-infinitary $\lambda$-$\perp$-terms is defined by:

$$ \Lambda_{\infty\perp}^{001} := \nu Y.\mu X. (\mathcal{V} + \lambda\mathcal{V}.X + (X)Y + \perp). $$

**Definition 5.10 ($\beta$-$\perp$-reduction).** The binary relation $\perp_0$ is defined on $\Lambda_{\infty\perp}^{001}$ by:

$$ \perp_0 := \{(M, \perp), M \text{ is unsolvable}\} \cup \{(\lambda x.\perp, \perp), x \in \mathcal{V}\} \cup \{((\perp)M, \perp), M \in \Lambda_{\infty\perp}^{001}\}. $$

The $\beta$-$\perp$-reduction $\xrightarrow{\beta\perp}$ is the contextual closure of $\beta_0 \cup \perp_0$. The infinitary $\beta$-$\perp$-reduction $\xrightarrow{\beta\perp}$ is the 001-strongly convergent closure of $\xrightarrow{\beta\perp}$.
Recall that, as underlined in Remark 2.14, a $\beta$-$\perp$-normal form is a term that cannot be reduced through $\to_{\beta\perp}$ (and not through $\to_{\beta\perp}^{\infty}$, which is reflexive), and that the $\beta$-$\perp$-normal forms of $M$ are the $\beta$-$\perp$-normal terms $N$ such that $M \to_{\beta\perp}^{\infty} N$.

**Definition 5.11** (Taylor expansion for $\perp$). The Taylor expansion is extended to $\Lambda_{\infty\perp}^{001}$ by defining $\boxtimes$ exactly as in Definition 3.12. This means that there is no approximant of $\perp$, and thereby $\mathcal{T}(\perp) = 0$.

**Remark 5.12.** Observe that $\mathcal{T}(M) = 0$ iff $M = \perp$ or $M = \lambda x.M'$ or $M = (M')N$ with $\mathcal{T}(M') = 0$. In particular, if $\mathcal{T}(M) = 0$ and $M \neq \perp$ then $M$ contains a subterm of the form $\lambda x.\perp$ or $(\perp)N$.

The following result is an extension of Theorem 4.21, ensuring that adding the constant $\perp$ does not break all our previous work.

**Corollary 5.13** (simulation of $\to_{\beta\perp}^{\infty}$). Let $M, N \in \Lambda_{\infty\perp}^{001}$ be $\lambda\perp$-terms. If $M \to_{\beta\perp}^{\infty} N$, then $\mathcal{T}(M) \xrightarrow{\sim_r^*} \mathcal{T}(N)$.

*Proof.* If $M$ is unsolvable then $M \perp_0 \perp$, and there is no $N$ in HNF such that $M \to_{\beta}^* N$. From Theorem 5.6, it follows that $\forall s \in \mathcal{T}(M)$, $nf_r(s) = 0$, that is to say $\mathcal{T}(M) \xrightarrow{\sim_r^*} \mathcal{T}(\perp)$. If $M = \lambda x.\perp$ or $M = (\perp)M'$, then $\mathcal{T}(M) = \mathcal{T}(\perp) = 0$. This extends Lemma 4.2 to the $\beta\perp$-reduction: if $M \to_{\beta\perp}^* N$, then $\mathcal{T}(M) \xrightarrow{\sim_r^*} \mathcal{T}(N)$. The rest of the proof is analogous to Section 4. $\square$

The next definition concerns Böhm trees. Based on an idea by Böhm [Böh68] and formally defined by Barendregt [Bar77], Böhm trees were introduced as a notion of infinite normal form for the usual $\lambda$-calculus, giving account of the (potentially) infinite behaviour of $\lambda$-terms. They rely on a coinductive definition (probably the first one in the study of the $\lambda$-calculus), and are the normal forms of $\Lambda_{\infty}^{001}$.

**Definition 5.14** (Böhm tree). The Böhm tree of a term $M \in \Lambda_{\infty}^{001}$ is the $\lambda\perp$-term BT$(M)$ defined coinductively as follows:

* if $M$ is solvable and $M \to_h^* \lambda x_1 \dots \lambda x_m. (\dots ((y)M_1)\dots) M_n$, then:

$$ \mathrm{BT}(M) := \lambda x_1 \dots \lambda x_m. (\dots ((y)\mathrm{BT}(M_1))\dots) \mathrm{BT}(M_n), $$

* if $M$ is unsolvable, then $\mathrm{BT}(M) := \perp$.

This definition is extended to $\Lambda_{\infty\perp}^{001}$ by setting $\mathrm{BT}(\perp) := \perp$.

Notice again that every coinductive call to BT(-) occurs in the right side of an application, that is to say under a rule (coI) carrying the $\triangleright$ modality.

**Lemma 5.15.** Let $M \in \Lambda_{\infty\perp}^{001}$ be a term

(1) BT$(M)$ is in $\beta$-$\perp$-normal form.

(2) If $M$ is in $\beta$-$\perp$-normal form then $\mathrm{BT}(M) = M$.

*Proof.* (1) By induction on the definition of $\to_{\beta\perp}$, we show that for any $\lambda\perp$-terms $M$ and $N$, if $M \to_{\beta\perp} N$ then $M$ is not a Böhm tree: in the base case, it is sufficient to observe that a Böhm tree is never a $\beta$-redex nor a $\perp$-redex; the contextuality cases are straightforward.

(2) By coinduction on the definition of BT$(M)$, using the fact that a $\beta$-$\perp$-normal term is either solvable or equal to $\perp$. $\square$
**Lemma 5.16** (weak $\beta \perp$-normalisation). Let $M \in \Lambda_{\infty \perp}^{001}$ be a term, then $M \to_{\beta \perp}^{\infty} \text{BT}(M)$. Furthermore, if $M \in \Lambda_{\infty}^{001}$ and $\text{BT}(M) \in \Lambda_{\infty}^{001}$, then $M \to_{\beta}^{\infty} \text{BT}(M)$.

*Proof.* We build a derivation of $M \to_{\beta \perp}^{\infty} \text{BT}(M)$ coinductively. If $M$ is either unsolvable or $\perp$, we have $M \to_{\beta \perp}^{\beta} \perp = \text{BT}(M)$ by definition. Otherwise, we have

$$M \to_h^* \lambda x_1 \dots \lambda x_m . (\dots ((y)M_1)\dots) M_n .$$

In this case, we apply $m$ times rule $(\lambda_{\beta}^{\infty})$, then $n$ times rule $(\beta^{\infty})$, and proceed coinductively to build derivations of $M_i \to_{\beta}^{\infty} \text{BT}(M_i)$ for $1 \le i \le m$.

If $\text{BT}(M) \in \Lambda_{\infty}^{001}$, then the first case of the construction never occurs, and we obtain $M \to_{\beta}^{\infty} \text{BT}(M)$ instead. $\square$

The following two technical lemmas, already well-known in a finitary setting [VA19, Facts 4.17 and 4.15], will be useful to show the unicity of $\beta \perp$-normal forms.

**Lemma 5.17.** Let $M \in \Lambda_{\infty \perp}^{001}$ be a term in $\beta \perp$-normal form, then $\mathcal{T}(M)$ is in normal form.

*Proof.* By contraposition, if some $s \in \mathcal{T}(M)$ contains a redex then so does $M$. $\square$

**Lemma 5.18** (injectivity, almost). Let $M, N \in \Lambda_{\infty \perp}^{001}$ be terms. If $\mathcal{T}(M) = \mathcal{T}(N)$, and if neither $M$ nor $N$ contain a subterm of the form $\lambda x. \perp$ or $(\perp)M'$, then $M = N$.

*Proof.* By nested induction and coinduction on the structure of $M$:

* If $M = \perp$, then $\mathcal{T}(N) = \mathcal{T}(M) = 0$, hence $N = \perp$ by Remark 5.12.

* Likewise, if $M = x$, then $\mathcal{T}(N) = \mathcal{T}(M) = \{x\}$ so $x \not\perp N$, and thus $N = x$.

* If $M = \lambda x.M'$, then $\mathcal{T}(N) = \mathcal{T}(M) = \lambda x.\mathcal{T}(M')$. By assumption, $M' \neq \perp$ so, by Remark 5.12, there exists $s \in \mathcal{T}(M')$ and then $\lambda x.s \not\perp N$. Thus, $\exists N' \in \Lambda_{\infty \perp}^{001}, N = \lambda x.N'$. Furthermore, we must have $\mathcal{T}(M') = \mathcal{T}(N')$ so, by induction hypothesis, $M' = N'$ and finally $M = N$.

* If $M = (M')M'',$ then $\mathcal{T}(N) = \mathcal{T}(M) = \langle \mathcal{T}(M') \rangle \mathcal{T}(M'')!$. By assumption, $M' \neq \perp$ so, by Remark 5.12, there exist $s \in \mathcal{T}(M')$ and $\bar{t} \in \mathcal{T}(M'')!$, and then $\langle s \rangle \bar{t} \not\perp N$. Thus, there exist $N', N'' \in \Lambda_{\infty \perp}^{001}$ such that $N = (N')N'$. The fact that $\mathcal{T}(M) \neq 0$ together with the injectivity of $(s, \bar{t}) \mapsto \langle s \rangle \bar{t}$ ensure that $\mathcal{T}(M') = \mathcal{T}(N')$ and $\mathcal{T}(M'')! = \mathcal{T}(N'')!$, hence $\mathcal{T}(M'') = \mathcal{T}(N'')$. We deduce $M' = N'$ by induction and proceed coinductively to prove $M'' = N''$. $\square$

**Remark 5.19.** The previous lemma does establish the injectivity of $\mathcal{T}(-)$ when restricted to $\Lambda_{\infty}^{001}$.

Now we have all the necessary material available, we can state the Commutation theorem, as well as some corollaries. Contrary to its original formulation [see ER06, p. 193], no specific definition of $\mathcal{T}(\text{BT}(M))$ is needed here thanks to the extension of the Taylor expansion to infinitary $\lambda \perp$-terms.

**Theorem 5.20** (Commutation theorem). For all term $M \in \Lambda_{\infty \perp}^{001}$, $\tilde{\text{n}}f_r(\mathcal{T}(M)) = \mathcal{T}(\text{BT}(M))$.

*Proof.* From Lemma 5.16, we know that $M \to_{\beta \perp}^{\infty} \text{BT}(M)$. Using the simulation theorem (Corollary 5.13), we deduce that $\mathcal{T}(M) \underset{r}{\to}^* \mathcal{T}(\text{BT}((M)))$, which itself is in normal form because $\text{BT}(M)$ is, using Lemmas 5.15 and 5.17. This is the desired result (via Notation 3.19). $\square$
From the Commutation theorem we can deduce the following two results, originally proved in [Ken+97] and later reformulated as a particular case of confluence modulo any set of strongly meaningless terms [Cza20; BM22].

**Corollary 5.21** (unicity of $\beta\perp$-normal forms). Let $M \in \Lambda_{\infty\perp}^{001}$ be a term, then $\mathrm{BT}(M)$ is its unique $\beta\perp$-normal form. Furthermore, if $M \in \Lambda_{\infty}^{001}$ and $\mathrm{BT}(M) \in \Lambda_{\infty}^{001}$, then the latter is the unique $\beta$-normal form of $M$.

*Proof.* Suppose there is an $N \in \Lambda_{\infty\perp}^{001}$ in $\beta\perp$-normal form such that $M \xrightarrow{\sim_{\beta\perp}} N$. Then by Lemma 5.15 and Theorem 5.20, $\mathcal{T}(N) = \mathcal{T}(\mathrm{BT}(N)) = \tilde{\mathrm{n}}_{\mathrm{r}}(\mathcal{T}(N)) = \mathrm{n}_{\mathrm{r}}(\mathcal{T}(M)) = \mathcal{T}(\mathrm{BT}(M))$. Since neither $\mathrm{BT}(M)$ nor $N$ (that are in $\beta\perp$-normal form) can contain a subterm of the form $\lambda x.\beta$ or $(\beta)P$, we can apply Lemma 5.18 and obtain $N = \mathrm{BT}(M)$. $\square$

**Remark 5.22.** For terms $M, N \in \Lambda_{\infty}^{001}$, write $M =_{\tau} N$ whenever $\tilde{\mathrm{n}}_{\mathrm{r}}(\mathcal{T}(M)) = \tilde{\mathrm{n}}_{\mathrm{r}}(\mathcal{T}(N))$, and $M =_{\beta} N$ whenever $\mathrm{BT}(M) = \mathrm{BT}(N)$. Theorem 5.20 entails that $M =_{\beta} N$ implies $M =_{\tau} N$. The proof of the previous corollary can be adapted to obtain the reverse implication: if $M =_{\tau} N$ then $\mathcal{T}(\mathrm{BT}(M)) = \mathcal{T}(\mathrm{BT}(N))$ by Theorem 5.20, and then Lemma 5.18 entails $\mathrm{BT}(M) = \mathrm{BT}(N)$.

This means in particular that all the models mentioned in Remark 4.22 are *sensible*, i.e. they equate all unsolvable terms.

**Corollary 5.23** (confluence of the $\beta\perp$-reduction). The reduction $\xrightarrow{\sim_{\beta\perp}}$ is confluent.

*Proof.* Given $M, N, N' \in \Lambda_{\infty\perp}^{001}$:

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

Another consequence is the following characterisation of normalising terms, which again is an infinitary counterpart to some folklore finitary result. Whereas the finitary case relies on *positive* resource terms (terms with no occurrence of the empty multiset 1), we have to refine this concept by considering *d-positive* terms, that is terms with no occurrence of 1 at depth smaller than *d*.

**Definition 5.24** (*d*-positive resource terms). Given an integer $d \in \mathbb{N}$, the set $\Lambda_r^{+d}$ of *d*-positive resource terms is defined inductively as follows:

* $\Lambda_r^{+0} := \Lambda_r,$

* if $d \ge 1$, $\Lambda_r^{+d} := \mathcal{V} \mid \lambda\mathcal{V}.\Lambda_r^{+d} \mid \langle\Lambda_r^{+d}\rangle \Lambda_r^{!+d-1}$ with $\Lambda_r^{!+d} := \mathcal{M}_{\mathrm{fin}}(\Lambda_r^{+d}) \setminus \{1\}$.

**Corollary 5.25** (characterisation of normalising terms). Let $M \in \Lambda_{\infty}^{001}$ be a term, then the following propositions are equivalent:

(1) there exists $N \in \Lambda_{\infty}^{001}$ in $\beta$-normal form such that $M \xrightarrow{\sim_{\beta}} N$,

(2) for any $d \in \mathbb{N}$, there exists $s \in \mathcal{T}(M)$ such that $\mathrm{n}_{\mathrm{r}}(s)$ contains a *d*-positive term.

*Proof.* Suppose (1), that is to say $\mathrm{BT}(M) \in \Lambda_{\infty}^{001}$ by Corollary 5.21. In particular, $M$ is solvable. By induction on $d \in \mathbb{N}$:
• Case $d = 0$. By solvability of $M$ and Theorem 5.6 there is an $s \in \mathcal{T}(M)$ such that $nf_r(s) \neq 0$, i.e. it contains a (0-positive) term.

• Case $d \ge 1$. Since $M$ is solvable, $M \to_{\beta}^{*} \lambda x_1 \dots \lambda x_m \dots ((y)M_1) \dots M_n$ and $\text{BT}(M) = \lambda x_1 \dots \lambda x_m \dots ((y)\text{BT}(M_1)) \dots \text{BT}(M_n)$, with $M_i \to_{\beta}^{\infty} \text{BT}(M_i)$ and $\text{BT}(M_i) \in \Lambda_{\infty}^{001}$. By induction, for every $i$ there is an $s_i \in \mathcal{T}(M_i)$ such that $nf_r(s_i)$ contains a $(d-1)$-positive $t_i$. Then by Theorem 4.21 there are $s \in \mathcal{T}(M)$ and $S, T \in 2\langle\Lambda_r\rangle$ such that:

$$s \to_r^* \lambda x_1 \dots \lambda x_m \langle \dots \langle \langle y \rangle [s_1] \rangle \dots \rangle [s_n] + S \\ \to_r^* \lambda x_1 \dots \lambda x_m \langle \dots \langle \langle y \rangle [t_1] \rangle \dots \rangle [t_n] + T$$

where $\lambda x_1 \dots \lambda x_m \langle \dots \langle \langle y \rangle [t_1] \rangle \dots \rangle [t_n] \in \text{normal form}$ and $d$-positive.

Conversely, we suppose (2) and establish $\text{BT}(M) \in \Lambda_{\infty}^{001}$ by nested induction and coinduction on $\text{BT}(M) \in \Lambda_{\infty}^{001}$. First note that (2) ensures that $nf_r(\mathcal{T}(M)) \neq 0$. Then Theorem 5.6 entails that $M$ is solvable, so

$$M \to_h^* \lambda x_1 \dots \lambda x_m \dots ((y)M_1) \dots M_n.$$

Now fix $d \in \mathbf{N}$: (2) ensures that we can find $s \in \mathcal{T}(M)$ and $t \in nf_r(s)$ so that $t$ is $(d+1)$-positive. By Theorem 4.21, $t \in \mathcal{T}(\text{BT}(M))$ so it has the shape

$$t = \lambda x_1 \dots \lambda x_m \langle \dots \langle \langle y \rangle \bar{t}_1 \rangle \dots \rangle \bar{t}_n$$

where $\bar{t}_i \in \Lambda_r^{!+d}$, i.e. each $\bar{t}_i$ contains a normal and $d$-positive $t_{i,1}$. By Theorem 4.21 again, there are $s_i \in \mathcal{T}(M_i)$ such that $t_{i,1} \in nf_r(s_i)$. We have thus proved that (2) is valid for each $M_i$. We proceed coinductively to establish $\text{BT}(M_i) \in \Lambda_{\infty}^{001}$. $\square$

If the finitary case, normalisation is also equivalent to the termination of the left-parallel reduction strategy, which plays the same role as the head strategy in Theorem 5.6 [Oli20, Thm. 4.10]. In our setting, there is of course no finite reduction strategy reaching the normal form of a term. A characterisation of the 001-normalising terms, called hereditarily head-normalising (HHN) in the literature, has been shown by Vial by means of infinitary non-idempotent intersection types [Via17; Via21], thus answering to the so-called “Klop’s problem”. However, there is no hope for an effective characterisation, since HHN terms are not recursively enumerable [Tat08].

### 5.3. Infinitary contexts and the Genericity Lemma.
To conclude this paper, we use the previous results to extend to $\Lambda_{\infty}^{001}$ a classical result in $\lambda$-calculus, the Genericity lemma [Bar84, Prop. 14.3.24]. A similar extension has been proved using completely different techniques [KOV96, § 5.3; Sal00, Thm. 20]. The intuition behind this lemma is that an unsolvable subterm of a normalising term cannot contribute to its normal form (it is generic). This justifies that unsolvables are taken as a class of meaningless terms — in fact, the unsolvables are the largest non-trivial set of (formally defined) meaningless terms [SV11; BM22].

**Definition 5.26 (context).** The set $\Lambda_{\infty}^{001}(\cdot|\cdot)$ of 001-infinitary contexts is defined by:

$$\Lambda_{\infty}^{001}(\cdot|\cdot) = \nu Y.\mu X. (\mathcal{V} + \lambda\mathcal{V}.X + (X)Y + \cdot)$$

where $\cdot$ is a constant called the “hole” (contexts are not quotiented by $\alpha$-equivalence).

Given a context $C \in \Lambda_{\infty}^{001}(\cdot|\cdot)$ and a term $M \in \Lambda_{\infty}^{001}$, we denote as $C(M)$ the term obtained by substituting $M$ for each occurrence of $\cdot$ in $C$ — like $C[M/\cdot]$, but possibly capturing the free variables of $M$.
**Definition 5.27** (resource context). The set $\Lambda_r[\cdot|\cdot]$ of resource contexts is defined, as in Definition 5.26, by adding the constant $*$ to $\Lambda_r$ (again, without quotienting by $\alpha$-equivalence).

Given a resource context $c \in \Lambda_r[\cdot|\cdot]$ and a resource monomial $\bar{t} \in \Lambda_r^!$, we denote as $c[\bar{t}]$ the sum of resource terms obtained by substituting each occurrence of $*$ in $c$ with exactly one element of $\bar{t}$, or 0 if the cardinality of $\bar{t}$ does not match the number of occurrences of $*$ — again, like $c\langle\bar{t}/*\rangle$, but possibly capturing the free variables of $\bar{t}$.

The Taylor expansion is extended to $\mathcal{T}: \Lambda_\infty^{001}(\cdot|\cdot) \to \mathcal{P}(\Lambda_r[\cdot|\cdot])$ by setting $\mathcal{T}(\cdot) := \{*\}$.

**Lemma 5.28.** Let $C \in \Lambda_\infty^{001}(\cdot|\cdot)$ be a context and $M \in \Lambda_\infty^{001}$ be a term. Then:

$$ \mathcal{T}(C(\mathcal{M})) = \{c[\bar{t}], c \in \mathcal{T}(C), \bar{t} \in \mathcal{T}(M)^!\}. $$

*Proof.* Direct consequence of Lemma 4.1. □

**Lemma 5.29** (characterisation of $\mathcal{T}$ by the $d$-positive elements). Let $M, N \in \Lambda_\infty^{001}$ be terms. If for any $d \in \mathbf{N}$ there exists a $d$-positive $s_d \in \mathcal{T}(M) \cap \mathcal{T}(N)$, then $M = N$.

*Proof.* Under the hypothesis, we establish $M = N$ by nested induction and coinduction on the structure of $M$.

* Case $M = x$. For $d = 0$, $\exists s_0 \in \mathcal{T}(M) \cap \mathcal{T}(N)$. Since $s_0 \in \mathcal{T}(M)$, $s_0 = x$ so $N = x$ too.

* Case $M = \lambda x.M'$. Suppose $\forall d \in \mathbf{N}$, $\exists s_d \in \mathcal{T}(M) \cap \mathcal{T}(N)$. Since $s_d \in \mathcal{T}(M)$, $s_d = \lambda x.s'_d$ for some $d$-positive $s'_d$. $s_d \in \mathcal{T}(N)$, whence $N = \lambda x.N'$ for some $N'$, and $s'_d \in \mathcal{T}(N')$. By induction, $M' = N'$, so $M = N$.

* Case $M = (M')M''$. Suppose $\forall d \in \mathbf{N}$, $\exists s_d \in \mathcal{T}(M) \cap \mathcal{T}(N)$. Since $s_d \in \mathcal{T}(M)$, $s_d = \langle t_d \rangle \bar{u}_d$ for some $t_d \in \Lambda_r^{+d}$ and $\bar{u}_d \in \Lambda_r^{!(d-1)}$. Furthermore $s_d \in \mathcal{T}(N)$, whence $N = (N')N''$ for some $N'$ and $N''$ such that $t_d \in \mathcal{T}(N')$ and $\bar{u}_d \in \mathcal{T}(N'')^!$. Since $\forall d \in \mathbf{N}$, $t_d \in \mathcal{T}(M') \cap \mathcal{T}(N')$ the induction hypothesis gives $M' = N'$. Moreover, $\forall d \in \mathbf{N}$, by $(d+1)$-positivity of $s_{d+1}$, $\bar{u}_{d+1}$ must contain at least one element $u_{d+1,1}$, which is $d$-positive and such that $u_{d+1,1} \in \mathcal{T}(M'') \cap \mathcal{T}(N'')$. Thus we can proceed to establish $M'' = N''$ coinductively. □

Using the previous work, we can state and show the infinitary Genericity lemma — without any further hypotheses than in the finitary setting. Our proof is a refinement of the (finitary) proof by Barbarossa and Manzonetto [BM20, Thm. 5.3]. As stressed by the authors, the key feature of the Taylor expansion here is that a resource term cannot erase any of its subterms (without being itself reduced to zero). However, in the infinitary setting, a term is in general not characterised by a single element of its Taylor expansion, which motivates the above characterisation by $d$-positive elements.

**Theorem 5.30** (Genericity lemma). Let $M \in \Lambda_\infty^{001}$ be an unsolvable term and $C(\cdot|\cdot)$ be a context in $\Lambda_\infty^{001}$. If $C(\mathcal{M})$ has a $\beta$-normal form $C^*$, then for any term $N \in \Lambda_\infty^{001}$, $C(\mathcal{N}) \to_\beta^\infty C^*$.

*Proof.* Suppose $C(\mathcal{M}) \to_\beta^\infty C^*$ in $\beta$-normal form. Then:

$$ \forall d \in \mathbf{N}, \exists s \in \mathcal{T}(C(\mathcal{M})), \exists t_d \in \Lambda_r^{+d}, t_d \in \mathrm{nf}_r(s) \quad \text{by Corollary 5.25} $$

hence

$$ \forall d \in \mathbf{N}, \exists c \in \mathcal{T}(C), \exists \bar{m} \in \mathcal{T}(M)^!, \exists t_d \in \Lambda_r^{+d}, t_d \in \mathrm{nf}_r(c[\bar{m}]) \quad \text{by Lemma 5.28.} $$

Write $\bar{m} = [m_1, \dots, m_n]$ with $n := \deg_*(c)$. By unsolvability of $M$ and Theorem 5.6, for each $1 \le i \le n$, $m_i \to_r^* 0$, so by confluence (Lemma 3.9) there is a $T_d \in 2\langle\Lambda_r\rangle$ for each $d \in \mathbf{N}$ such that:
<figure><img src="image_10.png" /></figure>

If $*$ appeared in $c$, then $n = \deg_*(c) \ge 1$ and $c[[0, \dots, 0]] = 0$, which is impossible. Thus, there is no occurrence of $*$ in $c$, and $c[[1]]$ is (the $\alpha$-equivalence class of) $c$.

Now, take any $N \in \Lambda_{\infty}^{001}$. By Lemma 5.28, $c[[1]] \ltimes C(|N|)$. Since $c[[1]] \to_r^* t_d + T_d$ we have $t_d \in \widetilde{\mathrm{nf}}_r(\mathcal{T}(C(|N|))) = \mathcal{T}(\mathrm{BT}(C(|N|)))$ by Theorem 5.20. Similarly, since we had taken $t_d \in \mathrm{nf}_r(s)$ for some $s \ltimes C(|M|)$, $t_d \in \mathcal{T}(\mathrm{BT}(C(|M|))) = \mathcal{T}(C^*)$, recalling that $\mathrm{BT}(C(|M|)) = C^*$ by Corollary 5.21.

There is a $d$-positive $t_d \in \mathcal{T}(\mathrm{BT}(C(|N|)))$ for any $d \in \mathbb{N}$, so we can apply Corollary 5.25 and deduce that $\mathrm{BT}(C(|N|)) \in \Lambda_{\infty}^{001}$. Since in addition we have $t_d \in \mathcal{T}(C^*)$, we obtain $\mathrm{BT}(C(|N|)) = C^*$ by Lemma 5.29 and $C(|N|) \xrightarrow{\beta} C^*$ by Lemma 5.16. $\square$

## 6. CONCLUSION

**Summary.** As the main result of this paper, we showed that the resource reduction of Taylor expansions simulates the infinitary $\beta$-reduction of $\Lambda_{\infty}^{001}$ terms (Theorem 4.21). This could be expected from Ehrhard and Regnier's Commutation Theorem, which tightly relates normalisation of the Taylor expansion and normal forms of $\Lambda_{\infty\perp}^{001}$ (aka. Böhm trees), but remains remarkable in that it enables to simulate an infinitary dynamics with a finitary one.

Using this fact, we were able to give simple proofs of well-known properties of $\Lambda_{\infty\perp}^{001}$ like confluence (Corollary 5.23), weak normalisation (Lemma 5.16), unicity of normal forms (Corollary 5.21). We also extended to infinitary terms several $\lambda$-calculus results like the Commutation Theorem (Theorem 5.20), the characterisations of head- and $\beta$-normalisation through Taylor expansion (Theorem 5.6 and Corollary 5.25), and we provided a new proof of the infinitary Genericity Lemma (Theorem 5.30).

As we already underlined, we believe that these results suggest that $\Lambda_{\infty\perp}^{001}$ is a reasonable extension of $\Lambda$ to consider when addressing head-normalisation and Taylor expansion issues. In particular, we were able to express the Commutation Theorem without any technical patch for the treatment of Böhm trees and reduction towards them.

**Further work.** The question naturally arises whether the converse of Theorem 4.21 is also true, that is whether $M \to_{\beta}^{\infty} N$ whenever $\mathcal{T}(M) \xrightarrow{\beta}^{*} \mathcal{T}(N)$. Similar issues have been successfully addressed in the setting of the algebraic $\lambda$-calculus [Ker19; KV23], which suggests such a conservativity result is within reach.

It is in fact possible to show that for ordinary $\lambda$-terms $M, N \in \Lambda$, $\mathcal{T}(M) \xrightarrow{\beta}^{*} \mathcal{T}(N)$ implies $M \to_{\beta}^{*} N$. In the infinitary setting, however, the conjecture fails: we were able to design terms $A, \bar{A} \in \Lambda_{\infty}^{001}$ such that $\mathcal{T}(A) \xrightarrow{\beta}^{*} \mathcal{T}(\bar{A})$, and such that there exists no reduction $A \to_{\beta}^{\infty} \bar{A}$. These results are the subject of a separate paper [CV23].
One could also ask whether the Taylor expansion can be further extended to the $\Lambda_{\infty}^{101}$ and $\Lambda_{\infty}^{111}$ infinitary calculi, looking for a counterpart to the Commutation Theorem involving Lévy-Longo and Berarducci trees. We believe this can be done with only minor adaptions in the case of Lévy-Longo trees, but not in the case of Berarducci trees.

Indeed, recall that Böhm trees can be seen as maximal directed sets of finite $\lambda \perp$-terms in $\beta \perp$-normal form, i.e. in HNF [Bar84, Sec. 14.3]. The crucial observation by [ER08] is that such terms are isomorphic to affine resource terms in normal form, the isomorphism mapping the elements of BT($M$) to the affine elements of $\mathcal{T}(BT(M))$.

* It is easy to design a resource calculus extending this property to Lévy-Longo trees (and the corresponding $\beta \perp$-normal forms, namely weak head normal forms): one should add a constructor approximating an abstraction with unknown body as follows

$$ \Lambda_r := \mathcal{V} \mid \lambda\mathcal{V} \cdot \mid \lambda\mathcal{V}\Lambda_r \mid \langle\Lambda_r\rangle \Lambda_r' $$

$$ \Lambda_r' := \mathcal{M}_{\text{fin}}(\Lambda_r) $$

so that we could set $\mathcal{T}(\lambda x.M) := \lambda x.\mathcal{T}(M) + \lambda x.\bullet$ in order to take into account the possibility to encounter an infinite chain of abstractions.

* On the other hand, the notion of $\beta \perp$-normal form corresponding to Berarducci trees (top normal forms) does not immediately enjoy such a property because there is no “top-level” syntactic characterisation of top normal forms: $(M)N$ is in TNF if $M$ does not reduce to an abstraction, which can only be checked by reducing $M$ at an unknown depth.

Thus, designing a Taylor approximation for the $\Lambda_{\infty}^{111}$ calculus, if possible, seems to require more advanced techniques.

Finally, we have limited our study to a qualitative setting only: as explained in Remark 3.13, it is not difficult to extend the definition of Taylor expansion with appropriate coefficients; but as explained in Remark 3.17, a quantitative version of our simulation result seems out of reach, if only because the reduction of infinite weighted sums of resource terms is not well defined in general. Nonetheless, we conjecture that the Commutation theorem also holds in a quantitative setting.

Indeed, in their seminal results [ER06; ER08], Ehrhard and Regnier exploited a uniformity property to show that the normalization (rather than an arbitrary reduction) of a sum of resource terms obtained by Taylor expansion does not generate sums of coefficients: each term occurring in the normal form is generated by a single term of the original sum. It is then possible to deduce the quantitative Commutation theorem from the qualitative one: this was essentially the path followed by Ehrhard and Regnier, and revisited by Olimpieri and the second author [OV22]. In the latter work, the qualitative Commutation theorem was established quite straightforwardly, by proving that Taylor expansion commutes with a variant of hereditary head reduction (the reduction strategy underlying the definition of Böhm trees). Moreover, by contrast with arbitrary reduction of resource terms, the latter reduction strategy does enjoy the uniformity property. We do believe that this alternative approach can be adapted to the infinitary setting, in order to deal with quantitative Taylor expansion: we leave this for future work.
REFERENCES

[AMM18] Jiří Adámek, Stefan Milius, and Lawrence S. Moss. "Fixed points of functors". In: *Journal of Logical and Algebraic Methods in Programming* 95 (2018), pp. 41–81. doi: 10.1016/j.jlamp.2017.11.003.

[App+07] Andrew W. Appel et al. "A very modal model of a modern, major, general type system". In: *ACM SIGPLAN Notices* 42.1 (2007), pp. 109–122. doi: 10.1145/1190215.1190235.

[Bah18] Patrick Bahr. "Strict Ideal Completions of the Lambda Calculus". In: *3rd International Conference on Formal Structures for Computation and Deduction*. Ed. by Hélène Kirchner. 2018. doi: 10.4230/LIPICS.FSCD.2018.8.

[Bar22] Davide Barbarossa. "Resource approximation for the λµ-calculus". In: *Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science*. 2022. doi: 10.1145/3531130.3532469.

[BM20] Davide Barbarossa and Giulio Manzonetto. "Taylor Subsumes Scott, Berry, Kahn and Plotkin". In: *47th Symp. on Princ. of Prog. Lang*. 1. Proc. ACM Prog. Lang., 2020. doi: 10.1145/3371069.

[BM22] Henk Barendregt and Giulio Manzonetto. *A Lambda Calculus Satellite*. Mathematical logic and foundations 94. College publications, 2022.

[Bar77] Henk P. Barendregt. "The Type Free Lambda Calculus". In: *Handbook of Mathematical Logic*. Ed. by Jon Barwise. Studies in Logic and the Foundations of Mathematics 90. Elsevier, 1977, pp. 1091–1132. doi: 10.1016/s0049-237x(08)71129-7.

[Bar84] Henk P. Barendregt. *The Lambda Calculus. Its Syntax and Semantics*. 2nd ed. Studies in Logic and the Foundations of Mathematics 103. Amsterdam: Elsevier Science, 1984.

[Bas18] Henning Basold. "Mixed Inductive-Coinductive Reasoning. Types, Programs and Logic". PhD thesis. Radboud University Nijmegen, 2018. URL: https://repository.ubn.ru.nl/handle/2066/190323.

[Ber96] Alessandro Berarducci. "Infinite λ-calculus and non-sensible models". In: *Logic and Algebra*. Routledge, 1996, pp. 339–377. doi: 10.1201/9780203748671-17.

[Ber05] Yves Bertot. "Filters on CoInductive Streams, an Application to Eratosthenes' Sieve". In: *Typed Lambda Calculi and Applications*. Ed. by Paweł Urzyczyn. LNCS. Springer, 2005, pp. 102–115. doi: 10.1007/11417170_9.

[Böh68] Corrado Böhm. "Alcune proprietà delle forme β-η-normali nel λ-K-calcolo". In: *Pubblicazioni dell'Instituto per le Applicazioni del Calcolo* 696 (1968). URL: http://www.ens-lyon.fr/LIP/REWRITING/TYPES_AND_L_CALCULUS/bohm696.pdf.

[Bru72] Nicolaas Govert de Bruijn. "Lambda Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with applications to the Church-Rosser Theorem". In: *Indagationes Mathematicæ* 34 (1972). doi: 10.1016/1385-7258(72)90034-0.

[BEM07] Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. "Not Enough Points Is Enough". In: *Computer Science Logic 2007*. 2007, pp. 298–312. doi: 10.1007/978-3-540-74915-8_24.

[BEM12] Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. "A relational semantics for parallelism and non-determinism in a functional setting". In: *Annals of Pure and Applied Logic* 163.7 (2012), pp. 918–934. doi: 10.1016/j.apal.2011.09.008.

[CV23] Rémy Cerda and Lionel Vaux Auclair. *How To Play The Accordion. On the (Non-)Conservativity of the Reduction Induced by the Taylor Approximation of λ-Terms*. 2023. arXiv: 2305.02785 [cs.LO].

[CT20] Jules Chouquet and Christine Tasson. "Taylor expansion for Call-By-Push-Value". en. In: *28th EACSL Annual Conference on Computer Science Logic*. 2020. doi: 10.4230/LIPICS.CSL.2020.16.

[CF58] Haskell B. Curry and Robert Feys. *Combinatory Logic*. Amsterdam: North Holland, 1958.

[Cza14] Łukasz Czajka. "A Coinductive Confluence Proof for Infinitary Lambda-Calculus". In: *Rewriting and Typed Lambda Calculi*. Ed. by Gilles Dowek. LNCS 8560. Cham: Springer International Publishing, 2014, pp. 164–178. doi: 10.1007/978-3-319-08918-8_12.

[Cza19] Łukasz Czajka. *Coinduction: an elementary approach*. 2019. arXiv: 1501.04354v8 [cs.LO].

[Cza20] Łukasz Czajka. "A new coinductive confluence proof for infinitary lambda calculus". In: *Logical Methods in Computer Science* 16.1 (2020). URL: https://lmcs.episciences.org/6194.

[Dal16] Ugo Dal Lago. *Infinitary λ-Calculi from a Linear Perspective*. Long version of a LICS paper. 2016. arXiv: 1604.08248.
[DL19] Ugo Dal Lago and Thomas Leventis. "On the Taylor Expansion of Probabilistic Lambda Terms". In: *4th International Conference on Formal Structures for Computation and Deduction*. Ed. by Herman Geuvers. LIPIcs 131. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2019. DOI: 10.4230/LIPIcs.FSCD.2019.13.

[DZ12] Ugo Dal Lago and Margherita Zorzi. "Probabilistic operational semantics for the lambda calculus". In: *Theoretical Informatics and Applications* 46.3 (2012), pp. 413–450. DOI: 10.1051/ita/2012012.

[DA09] Nils A. Danielsson and Thorsten Altenkirch. "Mixing Induction and Coinduction". 2009. URL: http://www.cse.chalmers.se/~nad//publications/danielsson-altenkirch-mixing.html.

[DM79] Nachum Dershowitz and Zohar Manna. "Proving termination with multiset orderings". In: *Communications of the ACM* 22.8 (1979), pp. 465–476. DOI: 10.1145/359138.359142.

[Ehr05] Thomas Ehrhard. "Finiteness Spaces". In: *Mathematical Structures in Computer Science* 15.4 (2005), pp. 615–646. DOI: 10.1017/S0960129504004645.

[ER03] Thomas Ehrhard and Laurent Regnier. "The differential lambda-calculus". In: *Theoretical Computer Science* 309.1 (2003), pp. 1–41. DOI: 10.1016/S0304-3975(03)00392-X.

[ER06] Thomas Ehrhard and Laurent Regnier. "Böhm Trees, Krivine's Machine and the Taylor Expansion of Lambda-Terms". In: *Logical Approaches to Computational Barriers*. Ed. by Arnold Beckmann et al. Berlin, Heidelberg: Springer, 2006, pp. 186–197. DOI: 10.1007/11780342_20.

[ER08] Thomas Ehrhard and Laurent Regnier. "Uniformity and the Taylor expansion of ordinary lambda-terms". In: *Theoretical Computer Science* 403.2 (2008), pp. 347–372. DOI: 10.1016/j.tcs.2008.06.001.

[EP13] Jörg Endrullis and Andrew Polonsky. "Infinitary Rewriting Coinductively". In: *TYPES 2011*. 2013, pp. 16–27. DOI: 10.4230/LIPIcs.TYPES.2011.16.

[GP02] Murdoch J. Gabbay and Andrew M. Pitts. "A New Approach to Abstract Syntax with Variable Binding". In: *Formal Aspects of Computing* 13 (2002), pp. 341–363. DOI: 10.1007/s001650200016.

[Gir87] Jean-Yves Girard. "Linear Logic". In: *Theoretical Computer Science* 50 (1987), pp. 1–102. DOI: 10.1016/0304-3975(87)90045-4.

[Gir88] Jean-Yves Girard. "Normal functors, power series and λ-calculus". In: *Annals of Pure and Applied Logic* 37.2 (1988), pp. 129–177. DOI: 10.1016/0168-0072(88)90025-5.

[Gir95] Jean-Yves Girard. "Linear Logic: Its syntax and semantics". In: *Advances in Linear Logic*. Ed. by Jean-Yves Girard, Yves Lafont, and Laurent Regnier. Cambridge: Cambridge University Press, 1995, pp. 1–42. DOI: 10.1017/CBO9780511629150.002.

[Hag87] Tatsuya Hagino. "A typed lambda calculus with categorical type constructors". In: *Category Theory and Computer Science*. 1987, pp. 140–157. DOI: 10.1007/3-540-18508-9_24.

[Joa04] Felix Joachimski. "Confluence of the coinductive λ-calculus". In: *Theoretical Computer Science* 311.1-3 (2004), pp. 105–119. DOI: 10.1016/s0304-3975(03)00324-4.

[KOV96] Richard Kennaway, Vincent van Oostrom, and Fer-Jan de Vries. "Meaningless terms in rewriting". In: *Algebraic and Logic Programming*. 1996, pp. 254–268. DOI: 10.1007/3-540-61735-3_17.

[Ken+95] Richard Kennaway et al. "Infinitary lambda calculi and böhm models". In: *Rewriting Techniques and Applications*. LNCS 914. Springer, 1995, pp. 257–270. DOI: 10.1007/3-540-59200-8_62.

[Ken+97] Richard Kennaway et al. "Infinitary lambda calculus". In: *Theoretical Computer Science* 175.1 (1997), pp. 93–125. DOI: 10.1016/S0304-3975(96)00171-5.

[Ker19] Axel Kerinec. Internship notes about the conservativity of β-reduction in the algebraic λ-calculus. Personal communication. 2019.

[KMP20] Axel Kerinec, Giulio Manzonetto, and Michele Pagani. "Revisiting Call-by-value Böhm trees in light of their Taylor expansion". In: *Logical Methods in Computer Science* 16 (3 2020), pp. 1860–5974. DOI: 10.23638/LMCS-16(3:6)2020.

[KV23] Axel Kerinec and Lionel Vaux Auclair. *The algebraic λ-calculus is a conservative extension of the ordinary λ-calculus*. 2023. arXiv: 2305.01067 [cs.LO].

[KS17] Dexter Kozen and Alexandra Silva. "Practical coinduction". In: *Math. Struct. in Comp. Sci.* 27.7 (2017), pp. 1132–1152. DOI: 10.1017/S0960129515000493.

[Kur+12] Alexander Kurz et al. "An Alpha-Corecursion Principle for the Infinitary Lambda Calculus". In: *CMCS 2012*. Springer, 2012, pp. 130–149. DOI: 10.1007/978-3-642-32784-1_8.
[Lév75] Jean-Jacques Lévy. "An algebraic interpretation of the λβK-calculus and a labelled λ-calculus". In: *λ-Calculus and Computer Science Theory*. Ed. by Corrado Böhm. LNCS 37. Springer, 1975, pp. 147-165. DOI: 10.1007/bfb0029523.

[Lon83] Giuseppe Longo. "Set-theoretical models of λ-calculus: theories, expansions, isomorphisms". In: *Annals of Pure and Applied Logic* 24.2 (1983), pp. 153-188. DOI: 10.1016/0168-0072(83)90030-1.

[Men91] Nax Paul Mendler. "Inductive types and type constraints in the second-order lambda calculus". In: *Annals of Pure and Applied Logic* 51.1-2 (1991), pp. 159-172. DOI: 10.1016/0168-0072(91)90069-x.

[Nak00] Hiroshi Nakano. "A modality for recursion". In: *Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science*. 2000. DOI: 10.1109/lics.2000.855774.

[Oli18] Federico Olimpieri. *Normalization and Taylor expansion of lambda-terms*. EasyChair Preprint no. 165. 2018. DOI: 10.29007/pqv5.

[Oli20] Federico Olimpieri. *Normalization, Taylor expansion and rigid approximation of λ-terms*. 2020. arXiv: 2001.01619.

[OV22] Federico Olimpieri and Lionel Vaux Auclair. "On the Taylor expansion of λ-terms and the groupoid structure of their rigid approximants". In: *Logical Methods in Computer Science* 18 (1 2022). DOI: 10.46298/lmcs-18(1:1)2022.

[Ong88] C.-H. Luke Ong. "The Lazy Lambda Calculus: An investigation into the foundations of functional programming". PhD thesis. London: Imperial College, 1988. URL: http://hdl.handle.net/10044/1/47211.

[Pag14] Michele Pagani. "A Bird's Eye View on the Quantitative Semantics of Linear Logic". QAPL'13-14. Grenoble, 2014. URL: http://qapl14.inria.fr/QAPLAbstract_Pagani Quantitative Semantics of Linear Logic.pdf.

[Pit13] Andrew M. Pitts. *Nominal Sets. Names and Symmetry in Computer Science*. Cambridge University Press, 2013. DOI: 10.1017/CBO9781139084673.

[Sal00] Antonino Salibra. "On the algebraic models of lambda calculus". In: *Theoretical Computer Science* 249.1 (2000), pp. 197-240. DOI: 10.1016/S0304-3975(00)00059-1.

[SV11] Paula Severi and Fer-Jan de Vries. "Decomposing the Lattice of Meaningless Sets in the Infinitary Lambda Calculus". In: *WoLLIC 2011*. 2011, pp. 210-227. DOI: 10.1007/978-3-642-20920-8_22.

[Tat08] Makoto Tatsuta. "Types for Hereditary Head Normalizing Terms". In: *Functional and Logic Programming. FLOPS 2008*. Ed. by Jacques Garrigue and Manuel V. Hermenegildo. 2008, pp. 195-209. DOI: 10.1007/978-3-540-78969-7_15.

[VA17] Lionel Vaux. "Taylor Expansion, β-Reduction and Normalization". In: *26th EACSL Annual Conference on Computer Science Logic (CSL 2017)*. 2017, 39:1-39:16. DOI: 10.4230/LIPICS.CS.L.2017.39.

[VA19] Lionel Vaux. "Normalizing the Taylor expansion of non-deterministic λ-terms, via parallel reduction of resource vectors". In: *Logical Methods in Computer Science* 15.3 (2019), 9:1-9:57. DOI: 10.23638/LMCS-15(3:9)2019.

[Via17] Pierre Vial. "Infinitary intersection types as sequences: A new answer to Klop's problem". In: *32nd Annual ACM/IEEE Symposium on Logic in Computer Science*. IEEE, 2017. DOI: 10.1109/lics.2017.8005103.

[Via21] Pierre Vial. *Sequence Types and Infinitary Semantics*. preprint. 2021. arXiv: 2102.07515.

[Wad76] Christopher P. Wadsworth. "The Relation between Computational and Denotational Properties for Scott's D_∞-Models of the Lambda-Calculus". In: *SIAM Journal on Computing* 5.3 (1976), pp. 488-521. DOI: 10.1137/0205036.