# A characterization of the Taylor expansion of lambda-terms

Pierre Boudes, Fanny He, Michele Pagani

► To cite this version:

Pierre Boudes, Fanny He, Michele Pagani. A characterization of the Taylor expansion of lambda-terms. 22nd EACSL Annual Conference Computer Science Logic (CSL 2013), EACSL, Sep 2013, Turin, Italy. pp.101-115, 10.4230/LIPIcs.CSL.2013.101 . hal-04670289

HAL Id: hal-04670289

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

Submitted on 12 Aug 2024

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

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

<figure><img src="image_1.png" /></figure>
# A characterization of the Taylor expansion of λ-terms*

Pierre Boudes, Fanny He, and Michele Pagani

LIPN – University Paris 13

Villetaneuse, France

{boudes, he, pagani}@lipn.univ-paris13.fr

## Abstract

The Taylor expansion of λ-terms, as introduced by Ehrhard and Regnier, expresses a λ-term as a series of multi-linear terms, called simple terms, which capture bounded computations. Normal forms of Taylor expansions give a notion of infinitary normal forms, refining the notion of Böhm trees in a quantitative setting.

We give the algebraic conditions over a set of normal simple terms which characterize the property of being the normal form of the Taylor expansion of a λ-term. From this full completeness result, we give further conditions which semantically describe normalizable and total λ-terms.

**1998 ACM Subject Classification** F.4.1 Lambda calculus and related systems, F.3.2 Denotational semantics

**Keywords and phrases** Lambda-Calculus, Böhm trees, Differential Lambda-Calculus, Linear Logic

Digital Object Identifier 10.4230/LIPIcs.CSL.2013.101

## 1 Introduction

Recently various semantics of linear logic and λ-calculus have been proposed (e.g. [5, 6]), where morphisms are infinitely differentiable functions between vector spaces (or more generally, modules). In fact, one can define the Taylor expansion of a function as an infinite sum of terms that are calculated from the values of the function's *n*-th derivatives at a given point. These models subsequently provide an intriguing way to describe the regularity of the behavior of a λ-term — the functions interpreting λ-terms are analytic, i.e. they are equal to their Taylor expansion at any point of their domain.

The main interest of Taylor expansion for the λ-calculus lies in the analogy that can be drawn between the usual notion of differentiation and its computational meaning. In fact, applying the derivative at 0 of the λ-term *M* on the argument *N* corresponds to passing the input *N* to *M* *exactly once*. This can be formalized in the setting of the *differential λ-calculus* [7] — an extension of the λ-calculus with a syntactic derivative operator, allowing to compute the optimal approximation of a program when applied to depletable arguments. The Taylor formula yields a natural notion of linear approximation of the ordinary application of λ-calculus. Let *M* and *N* be two λ-terms and assume `(D^n M · N^n)0` denotes the *n*-th derivative of *M* at 0 applied to *N* (as in the usual notation `f(n)(0) · x^n` with *M* as function *f*, *N* as argument *x*, and 0 as non-linear argument). Then the application of the term *M* to

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

© Pierre Boudes, Fanny He, and Michele Pagani;
licensed under Creative Commons License CC-BY

Computer Science Logic 2013 (CSL’13).

Editor: Simona Ronchi Della Rocca; pp. 101–115

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

LIPICS

Leibniz International Proceedings in Informatics

Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

<footnote>* This work was supported by the ANR 12 JS02 006 01 project COQUAS: Computing with quantitative semantics.</footnote>
the term N becomes:

$$ (M)N = \sum_{n=0}^{\infty} \frac{1}{n!} (\mathbb{D}^n M \cdot N^n) 0. \qquad (1) $$

Basically, $(\mathbb{D}^n M \cdot N^n)0$ expresses an evaluation of the application $(M)N$ using exactly $n$ linear copies of $N$. The coefficient $\frac{1}{n!}$ is there to take care of the number of permutations on the argument of $\mathbb{D}^n M$.

More generally, if one fully develops each application occurring in a $\lambda$-term $M$ into its corresponding Taylor expansion, one expresses the term as an infinite sum $M^*$ of purely “differential programs”, all of which containing only multi-linear applications and applications to 0. Ehrhard and Regnier develop a convenient notation for expressing such “differential programs”, calling them *simple terms* [8, 9]. Also, the authors define a rewriting system inspired by the standard rules for computing derivatives of polynomials which allow to give a normal form $NF(M^*)$ to a Taylor series $M^*$.

We denote by $\Delta^{\text{NF}}$ the set of normal simple terms (Equation (10)) and by $\mathbb{Q}^+[[\Delta^{\text{NF}}]]$ the formal linear combinations of terms in $\Delta^{\text{NF}}$ taking coefficients in the semi-ring of positive rational numbers. The combinations of $\mathbb{Q}^+[[\Delta^{\text{NF}}]]$ allow to express the normal forms of the Taylor expansion of $\lambda$-terms, however not all formal combinations can be associated with a $\lambda$-term. We propose here a characterization of the image of the $\lambda$-calculus into $\mathbb{Q}^+[[\Delta^{\text{NF}}]]$.

Let us underline that the space $\mathbb{Q}^+[[\Delta^{\text{NF}}]]$ is an example of syntax-based semantics of the untyped $\lambda$-calculus (as well as of its differential extension) — the interpretation being given by the function $M \mapsto \text{NF}(M^*)$, and the composition being assured by a notion of linear substitution (see Equation (5)). Roughly speaking, such a model is a quantitative refinement of the model provided by Böhm trees [1, §10] and it is crucial to the study of vectors based semantics, exactly as Böhm trees are at the core of domain-based denotational semantics. Our result basically amounts to defining a sub-model of $\mathbb{Q}^+[[\Delta^{\text{NF}}]]$ which is fully complete for the untyped $\lambda$-calculus.

Fortunately, the problem is significantly simplified by Ehrhard and Regnier's result. In particular, they prove [9, Corollary 35] that the normal form of the Taylor expansion of a $\lambda$-term $M$ can be defined as:

$$ \text{NF}(M^*) = \sum_{t \in \text{NF}(\tau(M))} \frac{1}{m(t)} t \qquad (2) $$

where: $m(t)$ is a natural number (called *multiplicity coefficient*) univocally defined by $t$, and $\text{NF}(\tau(M))$ is the *support* of the normal form of the Taylor expansion of $M$, i.e. the set of the simple terms appearing with a non-zero coefficient in $\text{NF}(M^*)$. The open issue is then to characterize the sets of simple terms which are of the form $\text{NF}(\tau(M))$, for some $\lambda$-term $M$.

We give three conditions which are necessary and sufficient for a subset $\mathcal{T}$ of $\Delta^{\text{NF}}$ to be equal to $\text{NF}(\tau(M))$, for some $\lambda$-term $M$ (Theorem 25): (i) the set of free variables occurring in $\mathcal{T}$ must be finite; (ii) $\mathcal{T}$ must be recursively enumerable; (iii) $\mathcal{T}$ must be an ideal with respect to a definedness relation (Definition 9).

Our characterization is based on two previous results: a theorem by Ehrhard and Regnier stating that Taylor expansion and normalization ($\lambda$-terms via Böhm trees; and sets of simple terms via the NF operator) commute (here Theorem 8), and Barendregt's characterization of the Böhm-like trees which are Böhm trees of $\lambda$-terms (here Theorem 5). Conditions (i) and (ii) are in fact an adaptation of Barendregt's characterization, but they are not sufficient to characterize Taylor expansions since the Taylor expansion gives a more atomic decomposition of $\lambda$-terms than that obtained from Böhm trees. Condition (iii) is a completeness condition,
assuring that there is no hole in the description of the support of a Taylor expansion. This condition looks like the usual one characterizing the set of finite approximants of a tree as an ideal with respect to the subtree order relation. However, the fine grained notion of approximant given by the simple terms makes our definedness relation a bit subtler than a subtree relation, in fact it is not even a preorder relation.

Our result concerns only the supports of the formal combinations in $Q^+[[\Delta^{\text{NF}}]]$, i.e. the subsets of $\Delta^{\text{NF}}$, the issue about coefficients being completely accomplished by Equation 2. Actually, the powerset of $\Delta^{\text{NF}}$ has an interest by its own. In fact, the powerset of $\Delta^{\text{NF}}$ can be formally seen as the space $\mathbf{Bool}[[\Delta^{\text{NF}}]]$ of the formal combinations with coefficients in the boolean ring $\mathbf{Bool} = (\{0, 1\}, \max, \min, 0, 1)$. The Taylor expansion of a $\lambda$-term $M$ into the space $\mathbf{Bool}[[\Delta^{\text{NF}}]]$ is the support $\tau(M)$ of the Taylor expansion of $M$ into $Q^+[[\Delta^{\text{NF}}]]$. Let us remark that $\mathbf{Bool}[[\Delta^{\text{NF}}]]$ gives another syntax-based quantitative semantics of the $\lambda$-calculus, and our result characterizes the image of the $\lambda$-calculus into $\mathbf{Bool}[[\Delta^{\text{NF}}]]$.

**Related works.** The question of characterizing the support of Ehrhard and Regnier's Taylor expansion has already been addressed by Pagani and Tasson in the setting of the simply typed linear logic proof-nets [12]. In that paper, the authors define a rewriting algorithm taking as input a finite set of cut-free differential nets (corresponding here to the normal simple terms) and either returning a cut-free proof-net or falling in a deadlock. Although related, our approach is different from that of [12] in various points. First, we are considering the untyped $\lambda$-calculus, while [12] deals with a simply typed (hence strongly normalizing) framework. Second, the criterion proposed by [12] is the termination of a rewriting relation in a proof-net. In the present setting, this will amount to refer to the termination of an algorithm which starts with a set $\mathcal{T}$ of simple terms and tries to compute a $\lambda$-term $M$ such that $\mathcal{T} \subseteq \text{NF}(\tau(M))$. We are giving more abstract conditions without referring to the termination of a computation. Finally, [12] characterizes the property of being a *finite subset* of the support of the Taylor expansion, while we are capturing here the property of being the whole support ($\mathcal{T} = \text{NF}(\tau(M))$).

**Structure of the paper.** Section 2 recalls the standard notions on $\lambda$-calculus and Böhm trees needed in the sequel. In particular, Definition 2 introduces Böhm-like trees and Theorem 5 states Barendregt's characterization of the set of Böhm-like trees corresponding to $\lambda$-terms. Section 3 defines Ehrhard and Regnier's resource $\lambda$-calculus, the normal form operator NF and the support $\tau(M)$ of the Taylor expansion of a $\lambda$-term $M$ (Equation 8). Theorem 8 recalls the commutation of the Taylor expansion with Böhm trees. Finally, Section 4 contains the original results of the paper. Our characterization of the normal forms of the Taylor expansions of $\lambda$-terms is given in Theorem 25. Corollary 28 gives an answer to what the maximal cliques of simple terms correspond to, a question addressed in [9]. Finally, Corollary 29 states the conditions characterizing the property of being a normalizable $\lambda$-term.

## 2 $\Lambda$-Calculus and Böhm trees

We denote by $\Lambda$ the set of $\lambda$-terms, written using Krivine's convention [11]:

$$ \Lambda : M, N ::= x \mid (M)N \mid \lambda x.M, $$

where $x$ ranges over a countable set $\text{Var}$ of variables. As usual, we suppose that application associates to the left and $\lambda$-abstraction to the right. The $\alpha$-conversion and the set $\text{FV}(M)$ of free variables of $M$ are defined following [11]. A term $M$ is closed whenever $\text{FV}(M) = \emptyset$.
Given two terms $M, N$, we denote by $M\{N/x\}$ the term obtained by simultaneously substituting $N$ to all free occurrences of $x$ in $M$, subject to the usual proviso about renaming bound variables in $M$ to avoid capture of free variables in $N$.

Hereafter terms are considered up to $\alpha$-conversion. We define the following terms:

$$
\begin{align*}
\mathbf{I} &:= \lambda x.x, & \mathbf{S} &:= \lambda xyz.((x)z)(y)z, & \mathbf{\Omega} &:= (\lambda x.(x)x)\lambda x.(x)x, \\
\mathbf{\Theta}_f &:= \lambda x.(f)(x)x, & \mathbf{\Theta} &:= \lambda f.(\mathbf{\Theta}_f)\mathbf{\Theta}_f.
\end{align*}
$$

The $\beta$-reduction $\beta \to$ is the smallest relation over $\Lambda$ containing the $\beta$-step $(\lambda x.M)N \stackrel{\beta}{\to} M\{N/x\}$ and closed under the following context rules (supposing $M \stackrel{\beta}{\to} M'$):

$$
(\text{abs}) : \lambda x.M \xrightarrow{\beta} \lambda x.M', \quad (\text{fun}) : (M)N \xrightarrow{\beta} (M')N, \quad (\text{arg}) : (N)M \xrightarrow{\beta} (N)M'. \quad (3)
$$

We denote by $\beta^* \to$ the reflexive and transitive closure of $\beta \to$. A $\beta$-normal form is a normal form for $\beta \to$. The reduction $\beta \to$ is confluent which implies that the $\beta$-normal form of a $\lambda$-term is unique, whenever it exists. However, $\beta \to$ is not normalizing, i.e. there are $\lambda$-terms $M$ without a $\beta$-normal form, e.g. $\Omega$ and $\Theta$. Indeed, $\Omega$ reduces only to itself, i.e. $\Omega \stackrel{\beta}{\to} \Omega$, while $\Theta$ yields the infinite reduction sequence $\Theta \stackrel{\beta}{\to} \lambda f.(f)(\Theta_f)\Theta_f \stackrel{\beta}{\to} \lambda f.(f)(f)(\Theta_f)\Theta_f \stackrel{\beta}{\to} \dots$.

Notice however that $\Omega$ and $\Theta$ are quite different. Any application $(\Omega)M_0 \dots M_{n-1}$ gives a non-normalizing $\lambda$-term, independently from $M_0, \dots, M_{n-1}$. In that sense $\Omega$ represents the everywhere undefined function. On the contrary, $\Theta$ is a fundamental term producing a potentially infinite iteration of its first argument, i.e. $(\Theta)M_0 \dots M_{n-1} \xrightarrow{\beta^*} (M_0)(\Theta)M_0 M_1 \dots M_{n-1} \xrightarrow{\beta^*} (M_0)(M_0)(\Theta)M_0 M_1 \dots M_{n-1} \xrightarrow{\beta^*} \dots$, and so it converges for certain $M_0, \dots, M_{n-1}$ for appropriate reduction strategies. Böhm trees are introduced in [1, §10] and provide a notion of infinitary normal form allowing to distinguish between totally undefined terms, like $\Omega$, and terms like $\Theta$, which are not normalizing but can interact with their arguments giving convergent computations.

The Böhm tree of a term is defined by using the *head reduction* $h \to$, a deterministic restriction of $\beta \to$ obtained by forbidding (arg) in the set of rules (3) and by restricting the (fun) rule to the case where $M$ is not an abstraction. A *head normal form* is a normal form for the reduction $h \to$, and it always has the shape: $\lambda x_0 \dots x_{m-1}.(y)M_0 \dots M_{n-1}$, for $n, m \ge 0$, $x_0, \dots, x_{m-1}$, $y$ variables, and $M_0, \dots, M_{n-1}$ $\lambda$-terms. The variable $y$ is called the *head variable*, and $M_0, \dots, M_{n-1}$ its arguments.

Notice that $\Omega$ has no head normal form, while $\lambda f.(f)(\Theta_f)\Theta_f$ is a head normal form of $\Theta$. Basically, the Böhm tree $\text{BT}(M)$ of a $\lambda$-term $M$ is a (possibly infinite) nesting of head normal forms: if $M$ is $\beta$-normalizable, then $\text{BT}(M)$ is just the applicative tree of its $\beta$-normal form (e.g. Figure 1a, 1c), otherwise it can be either infinite in depth (e.g. Figure 1d) or with “holes” denoting totally undefined sub-terms (e.g. Figure 1b) or both (e.g. Figure 1e).

We recall some definitions of [1, §10]. We introduce the set of Böhm-like trees (Definition 2), which is the codomain of the function $\text{BT}()$. In general, a labelled tree can be represented as a partial function from the set $\mathbb{N}^*$ of finite sequences of integers to the set of possible labels. In the case of Böhm-like trees, a label is a pair $(\lambda x_0 \dots x_{m-1}.y, n)$, where $\lambda x_0 \dots x_{m-1}.y$ represents the $\lambda$-prefix and the head variable of a head normal form, and $n$ the number of its arguments, which is also a bound to the number of children of the node labelled by $(\lambda x_0 \dots x_{m-1}.y, n)$. Definition 4 associates with any $\lambda$-term $M$ a Böhm-like tree $\text{BT}(M)$. Not every Böhm-like tree is the Böhm tree of a $\lambda$-term, and we recall in Theorem 5 Barendregt's characterization of the image set of $\text{BT}()$.
**► Notation 1.** Greek letters $\alpha, \beta, \gamma$ will vary over $\mathbb{N}^*$, the set of finite sequences of natural numbers. We denote by $@$ the concatenation operator, by $<$ the strict prefix order, by length($\alpha$) the length of a sequence $\alpha \in \mathbb{N}^*$, and by $\langle n_1, \dots, n_k \rangle$ the sequence of $n_1, \dots, n_k$. In particular, $\langle \rangle$ is the empty sequence. For example $\langle 1, 2 \rangle < \langle 1, 2, 3 \rangle = \langle 1 \rangle @ \langle 2, 3 \rangle$.
We recall that, when $f$ is a partial function, $f(x) \downarrow$ means that $f(x)$ is defined and that $f(x) \uparrow$ means that $f(x)$ is undefined.

**► Definition 2.** Let $\Sigma \stackrel{\Delta}{=} \{\lambda x_0 \dots x_{m-1}. y \; ; \; m \in \mathbb{N}, x_i, y \in \text{Var}\}$. A Böhm-like tree<fnref n="1" /> is a partial function $\mathcal{B}$ from $\mathbb{N}^*$ to $\Sigma \times \mathbb{N}$ such that:

- if $\mathcal{B}(\alpha) \downarrow$ and $\beta < \alpha$, then $\mathcal{B}(\beta) \downarrow$,

- if $\mathcal{B}(\alpha) = (a, n)$, then $\forall k \ge n$, $\mathcal{B}(\alpha @ \langle k \rangle) \uparrow$.

Actually, a sequence $\alpha$ in the domain of $\mathcal{B}$ describes a path from the root to a node labelled by $\mathcal{B}(\alpha)$. Notice that the enumeration of the children of a node allows some holes, representing the presence of totally undefined arguments in the head normal form associated with such a node. Figure 1 gives examples of a convenient graphical representation of Böhm-like trees, where the number $n$ of a label $(a, n)$ is encoded by using pending edges. More precisely,

Figure 1a is the function $\langle \rangle \mapsto (\lambda x.x, 0)$,

Figure 1b is the function $\langle \rangle \mapsto (\lambda x.x, 1)$,

Figure 1c is the function $\langle \rangle \mapsto (\lambda xyz.x, 2)$, $\langle 0 \rangle \mapsto (z, 0)$, $\langle 1 \rangle \mapsto (y, 1)$, $\langle 10 \rangle \mapsto (z, 0)$,

Figure 1d is the function $\langle \rangle \mapsto (\lambda f.f, 1)$, $\langle 0 \rangle \mapsto (f, 1)$, $\langle 00 \rangle \mapsto (f, 1)$, $\langle 000 \rangle \mapsto (f, 1)$...

Figure 1e is the function $\langle \rangle \mapsto (f, 2)$, $\langle 1 \rangle \mapsto (f, 2)$, $\langle 11 \rangle \mapsto (f, 2)$, $\langle 111 \rangle \mapsto (f, 2)$...

The height of a Böhm-like tree $\mathcal{B}$ is defined by: $\text{height}(\mathcal{B}) \stackrel{\Delta}{=} \sup\{1 + \text{length}(\alpha) \mid \mathcal{B}(\alpha) \downarrow\}$. Remark that the domain of $\mathcal{B}$ can be empty and in that case it has a zero height, otherwise the height is positive or infinite. Given $h \in \mathbb{N}$, the restriction of $\mathcal{B}$ to $h$ is the Böhm-like tree $\mathcal{B}|_h$ defined by cutting off subtrees at height $h$: $\mathcal{B}|_h(\alpha) = \mathcal{B}(\alpha)$ if length($\alpha$) < $h$, otherwise $\mathcal{B}|_h(\alpha) \uparrow$. Moreover, if $\mathcal{B}(\langle \rangle) = (a, n)$ and $i < n$, we define the $i$-th subtree $\mathcal{B}_i$ of $\mathcal{B}$ as: $\mathcal{B}_i(\alpha) = \mathcal{B}(\langle i \rangle @ \alpha)$.

Trees can be seen as ordered by the set-theoretical inclusion on the graph of their functions. With respect to this order $\{\mathcal{B}|_h\}_{h \in \mathbb{N}}$ is a chain whose limit is $\mathcal{B}$, i.e. $\mathcal{B} = \bigcup_{h \in \mathbb{N}} \mathcal{B}|_h$. Such a remark is useful for proofs and definitions on infinite Böhm-like trees. For example, the set $\text{FV}(\mathcal{B})$ of free variables of a Böhm-like tree is defined as follows: if $\text{height}(\mathcal{B}) = 0$, then $\text{FV}(\mathcal{B}) \stackrel{\Delta}{=} \emptyset$; if $\text{height}(\mathcal{B}) = h + 1$, let $\mathcal{B}(\langle \rangle) = (\lambda x_0 \dots x_{m-1}.y, n)$, then $\text{FV}(\mathcal{B}) \stackrel{\Delta}{=} (\{y\} \cup \bigcup_{i=0}^{n-1} \text{FV}(\mathcal{B}_i)) \setminus \{x_0, \dots, x_{m-1}\}$; finally, if $\text{height}(\mathcal{B}) = \infty$, then $\text{FV}(\mathcal{B}) \stackrel{\Delta}{=} \bigcup_{h \in \mathbb{N}} \text{FV}(\mathcal{B}|_h)$.

**► Definition 3.** A Böhm-like tree $\mathcal{B}$ is recursively enumerable, r.e. for short, if $\mathcal{B}$ is a partial recursive function (after some coding of $\Sigma$).

**► Definition 4.** The Böhm tree $\text{BT}(M)$ of a $\lambda$-term $M$ is defined as follows:

- if $M \stackrel{h^*}{\to} \lambda x_0 \dots x_{m-1}.(y) M_0 \dots M_{n-1}$, then,

$$ \text{BT}(M)(\langle \rangle) \stackrel{\Delta}{=} (\lambda x_0 \dots x_{m-1}.y, n) $$

$$ \text{BT}(M)(\langle i \rangle @ \alpha) \stackrel{\Delta}{=} \text{BT}(M_i)(\alpha) \qquad \text{if } i < n, $$

$$ \text{BT}(M)(\langle i \rangle @ \alpha) \uparrow \qquad \text{otherwise.} $$

- Otherwise, $\text{BT}(M)$ is the totally undefined function.

<footnote n="1">¹ This is called an *effective Böhm-like tree* in [1, Def. 10.1.9].</footnote>
<figure><img src="image_4.png" /><figcaption>Figure 1 Some examples of Böhm trees.</figcaption></figure>

Figure 1 gives examples of BT() values. A Böhm-like tree which is not in the image of a λ-term is the infinite branch

$$ \epsilon \mapsto (x_0, 1), \quad \langle 0 \rangle \mapsto (x_1, 1), \quad \langle 00 \rangle \mapsto (x_2, 1), \quad \langle 000 \rangle \mapsto (x_3, 1) \dots $$

for $x_0, x_1, x_2, x_3, \dots$ pairwise distinct variables.

**Theorem 5** ([1, Theorem 10.1.23]). Let $\mathcal{B}$ be a Böhm-like tree. There is a λ-term $M$ such that $\text{BT}(M) = \mathcal{B}$ if, and only if, $\text{FV}(\mathcal{B})$ is finite and $\mathcal{B}$ is r.e..

The left-to-right direction is a straight consequence of the remark that $\text{FV}(\text{BT}(M)) \subseteq \text{FV}(M)$ and of the fact that the definition of $\text{BT}(M)$ is effective (hence by Church's Thesis it is r.e.). The proof of the right-to-left direction is more involved. Essentially, it uses a theorem stating that the set $\Lambda^0$ of closed λ-terms can be enumerated in such a way that there are two λ-terms **E** and **F** such that $\forall M \in \Lambda^0$, denoting by $\underline{M}$ the Church numeral associated with $M$ by the enumeration, we have $(\underline{\text{E}})M =_{\beta} \underline{M}$ and, vice versa, $(\underline{\text{F}})\underline{M} =_{\beta} M$. We refer to [1, 10] for more details.

## 3 Taylor expansion

We recall the resource calculus as presented in [8, 9]. Let us warn the reader that the name “resource calculus” also refers in the literature to slightly different calculi. In particular, we have the calculus by Boudol et al.’s in [3], which is a resource-sensitive extension of the lazy call-by-value λ-calculus, and Tranquilli’s resource λ-calculus [13] which is basically a different notation for Ehrhard and Regnier’s differential λ-calculus. The resource calculus of [8, 9], which we briefly recall here, is a fragment of Tranquilli’s calculus.

We define the set $\Delta$ of the simple terms (Grammar (4)), a rewriting relation $\xrightarrow{r}$ over the finite powerset of $\Delta$ (rules (5) and (6)), and a normal form operator NF over the (finite and infinite) powerset of $\Delta$ (Equation 7). Concerning the discussion in the Introduction, the simple terms in $\Delta$ are a notation that express the terms in a Taylor series (Equation 2) and the subsets of $\Delta$ are the supports of such series.

Equation (8) defines the Taylor expansion of the λ-calculus and Equation (9) extends it to Böhm-like trees. Theorem 8 states Ehrhard and Regnier’s correspondence between the resource reduction on the Taylor expansion of λ-terms and their Böhm trees.

**Resource calculus.** The set $\Delta$ of simple terms is defined by:

$$ \Delta : t ::= x \mid \lambda x.t \mid \langle t \rangle \mu, \qquad (4) $$

where $x$ ranges over the set Var of variables, and $\mu$ is a finite multiset of simple terms, called *bag*. Small Latin letters like $s, t, u$ will vary on simple terms, and small Greek letters $\mu, \nu, \rho$
on bags. We recall that we adopt Krivine's notation [11], so, in particular, $\langle t \rangle \mu_1 \dots \mu_n$ is a shortcut for $\langle \dots \rangle \langle t \rangle \mu_1 \dots \mu_n$.

**► Notation 6.** We recall that for any set $E$, a multiset on $E$ is a function $\mu: E \to \mathbb{N}$. The support $|\mu|$ of $\mu$ is the set of all elements $e$ of $E$ such that $\mu(e) \neq 0$, and $\mu$ is called a finite multiset when $|\mu|$ is a finite set. We denote by $\mathcal{M}(E)$ the set of multisets on $E$ and by $\mathcal{M}_f(E)$ the set of finite multisets on $E$. A multiplicative notation is used for bags, 1 is the empty bag and $\mu \cdot \nu$ is the disjoint union of $\mu$ and $\nu$. The bag $[t]$ is the singleton containing exactly one occurrence of the simple term $t$. More occurrences of $t$ can be written as a power: $[t^3] = [t, t, t] = [t] \cdot [t] \cdot [t]$.

Free and bound variables and the $\alpha$-equivalence $\equiv_\alpha$ are defined as in the $\lambda$-calculus.

The symbols $S, T, U$ will vary over the powerset $\mathcal{P}(\Delta^{\text{NF}})$. By notational convention, we extend all the constructs of the grammar of $\Delta$ as point-wise operations on (possibly infinite) sets of simple terms, like for example

$$ \lambda x.T \triangleq \{\lambda x.t \mid t \in T\}, \quad \langle S \rangle [T^2, U] \triangleq \{\langle s \rangle [t_1, t_2, u] \mid s \in S, t_1, t_2 \in T, u \in U\}. $$

The number of free occurrences of $x$ in $t$, called degree of $x$ in $t$, is written $\deg_x(t)$. A redex is a simple term of the shape $\langle \lambda x.t \rangle [s_1, \dots, s_n]$. Its reduction gives a finite set of simple terms, which is empty whenever $\deg_x(t) \neq n$, otherwise it is the set of all possible simple terms obtained by linearly replacing each free occurrence of $x$ with exactly one $s_i$, for $i = 1, \dots, n$. Formally,

$$ \langle \lambda x.t \rangle [s_1, \dots, s_n] \xrightarrow{r} \begin{cases} \{t\{s_{\sigma(1)}/x_1, \dots, s_{\sigma(n)}/x_n\} \mid \sigma \in S_n\} & \text{if } \deg_x(t) = n, \\ \emptyset & \text{otherwise.} \end{cases} \quad (5) $$

where $S_n$ is the group of permutations over $n = \{1, \dots, n\}$ and $x_1, \dots, x_n$ is any enumeration of the free occurrences of $x$ in $t$, so that $t\{s_{\sigma(i)}/x_i\}$ denotes the term obtained from $t$ by replacing the $i$-th free occurrence of $x$ with the term $s_{\sigma(i)}$.

The relation $\xrightarrow{r} \subseteq \Delta \times \mathcal{P}_f(\Delta)$ is extended to $\mathcal{P}_f(\Delta) \times \mathcal{P}_f(\Delta)$ by context closure, i.e. $\xrightarrow{r}$ is the smallest relation on $\mathcal{P}_f(\Delta) \times \mathcal{P}_f(\Delta)$ satisfying Equation 5 and such that, whenever $t \xrightarrow{r} \mathcal{T}$ and $S \in \mathcal{P}_f(\Delta)$, we have:

$$ \lambda x.t \xrightarrow{r} \lambda x.T, \quad \langle t \rangle \mu \xrightarrow{r} \langle T \rangle \mu, \quad \langle s \rangle [t] \cdot \mu \xrightarrow{r} \langle s \rangle [T] \cdot \mu, \quad \{t\} \cup S \xrightarrow{r} \mathcal{T} \cup S. \quad (6) $$

Notice that the size (i.e. the number of symbols) of each simple term in $\mathcal{T}$ is strictly less than the size of $t$, whenever $t \xrightarrow{r} \mathcal{T}$. Therefore, $\xrightarrow{r}$ is strongly normalizing on $\mathcal{P}_f(\Delta)$. Moreover, one can easily check that $\xrightarrow{r}$ is weakly confluent, thus confluent by Newman's lemma.

**► Proposition 7.** The relation $\xrightarrow{r}$ is strongly normalizing and confluent on $\mathcal{P}_f(\Delta)$.

In particular, given any simple term $t$, its unique normal form $\text{NF}(t)$ is always well-defined. Such an operator is extended over $\mathcal{P}(\Delta^{\text{NF}})$ by:

$$ \text{NF}(\mathcal{T}) \triangleq \bigcup_{t \in \mathcal{T}} \text{NF}(t). \quad (7) $$

We also extend over the notation for free variables by setting $\text{FV}(\mathcal{T}) \triangleq \bigcup_{t \in \mathcal{T}} \{\text{FV}(t)\}$.
**Taylor expansion.** We define the map $\tau$ from $\Lambda$ to $\mathcal{P}_f(\Delta)$ by structural induction on the $\lambda$-terms. As said in the Introduction, $\tau$ is the support of the Taylor expansion described in [7, 9], from the $\lambda$-calculus to the infinite formal linear combinations in $\mathbb{Q}^+[[\Delta]]$, as well as the Taylor expansion into $\mathbf{Bool}[[\Delta]]$.

$$ \tau(x) \stackrel{\Delta}{=} x, \quad \tau(\lambda x.M) \stackrel{\Delta}{=} \lambda x.\tau(M), \quad \tau((M)N) \stackrel{\Delta}{=} \bigcup_{n=0}^{\infty} \langle\tau(M)\rangle[\tau(N)^n]. \quad (8) $$

For example, we have

$$ \begin{align*} \tau(\mathbf{I}) &\stackrel{\Delta}{=} \{\lambda x.x\}, \\ \tau(\mathbf{S}) &\stackrel{\Delta}{=} \{\lambda xyz.\langle x \rangle[z^{n_0}][\langle y \rangle[z^{n_1}], \dots, \langle y \rangle[z^{n_k}]] ; k, n_0, \dots, n_k \in \mathbb{N}\}, \\ \tau(\mathbf{\Omega}) &\stackrel{\Delta}{=} \{\langle \lambda x.\langle x \rangle[x^{n_0}] \rangle[\lambda x.\langle x \rangle[x^{n_1}], \dots, \lambda x.\langle x \rangle[x^{n_k}] \rangle ; k, n_0, \dots, n_k \in \mathbb{N}\}, \\ \tau(\mathbf{\Theta}) &\stackrel{\Delta}{=} \{\lambda f.\langle \lambda x.\langle f \rangle[\langle x \rangle[x^{n_1}], \dots, \langle x \rangle[x^{n_k}]] \rangle[\lambda x.\langle f \rangle[\langle x \rangle[x^{n_{1,1}}], \dots, \langle x \rangle[x^{n_{1,k_1}}]] , \dots, \\ & \phantom{\stackrel{\Delta}{=} \{\lambda f.\langle \lambda x.\langle f \rangle[\langle x \rangle[x^{n_1}, \dots, \langle x \rangle[x^{n_{h_1,k_1}}]] \rangle[\lambda x.\langle f \rangle[\langle x \rangle[x^{n_{1,1}}], \dots, \langle x \rangle[x^{n_{1,k_1}}]] , \dots,} \lambda x.\langle f \rangle[\langle x \rangle[x^{n_{h_1}}, \dots, \langle x \rangle[x^{n_{h,k_h}}]] \rangle ; k, n_i, h, n_{i,j} \in \mathbb{N}\} \end{align*} $$

The Taylor expansion of a $\beta$-redex contains resource redexes. If one looks for an invariant under $\beta$-reduction, one should consider the normal forms of the Taylor expansions. By induction on the size of the simple terms, one can for example prove that $\mathrm{NF}(\tau(\mathbf{\Omega})) = \emptyset$, while

$$ \mathrm{NF}(\tau(\mathbf{\Theta})) = \{\lambda f.\langle f \rangle 1, \lambda f.\langle f \rangle [(\langle f \rangle 1)^n], \lambda f.\langle f \rangle [(\langle f \rangle [(\langle f \rangle 1)^{n_1}], \dots, \langle f \rangle [(\langle f \rangle 1)^{n_k}]]], \dots \}. $$

Indeed, notice that these examples can be seen as a thick version [2] of the finite approximants of the Böhm tree of the corresponding $\lambda$-terms, where each sub-tree has been recursively replaced by a finite multiset of copies of it. We recall the following Theorem 8, stating a commutation between the resource reduction and the Taylor expansion through the Böhm tree operator. To do this, we need to extend the notion of Taylor expansion to Böhm-like trees:

$$ \tau(\mathcal{B}) \stackrel{\Delta}{=} \left\{ \begin{array}{ll} \emptyset & \text{if } \mathrm{height}(\mathcal{B}) = 0, \\ \{\lambda x_0 \dots x_{m-1}.\langle y \rangle \mu_0 \dots \mu_{n-1} ; \mu_i \in \mathcal{M}_F(\tau(\mathcal{B}_i))\} & \text{if } \mathrm{height}(\mathcal{B}) = h + 1 \text{ and } \mathcal{B}(\langle \rangle) = (\lambda x_0 \dots x_{m-1}.y, n), \\ \bigcup_h \tau(\mathcal{B}|_h) & \text{if } \mathrm{height}(\mathcal{B}) = \infty. \end{array} \right. \quad (9) $$

**► Theorem 8** ([8, Theorem 2]). For every $\lambda$-term $M$, $\mathrm{NF}(\tau(M)) = \tau(\mathrm{BT}(M))$.

# 4 Characterizing the Taylor expansion

In this section, we prove our main result (Theorem 25), an algebraic characterization of the normal forms of the Taylor expansion of $\Lambda$. Definitions 9 and 10 give the two crucial notions (a notion of ideal and a notion of effective element) for such a characterization.

Let $\Delta^{\mathrm{NF}}$ be the set of the simple terms which are normal forms with respect to $\xrightarrow{r}$. They have the following shape:

$$ \Delta^{\mathrm{NF}} : t ::= \lambda x_0 \dots x_{m-1}. \langle y \rangle \mu_0 \dots \mu_{n-1} \quad (10) $$

where $m, n \ge 0$ and each $\mu_i$ is a bag of simple terms in normal form.
**► Definition 9 (Definedness).** The definedness relation $\leq$ on $\Delta^{\text{NF}}$ is given as follows:

$$ \lambda x_0 \dots x_{m-1} \cdot \langle y \rangle \mu_0 \dots \mu_{n-1} \leq t \text{ iff } \left\{ \begin{array}{l} t = \lambda x_0 \dots x_{m-1} \cdot \langle y \rangle \nu_0 \dots \nu_{n-1} \text{ and} \\ \forall i < n, |\mu_i| \neq \emptyset \implies \exists v \in |\nu_i|, \forall u \in |\mu_i|, u \leq v. \end{array} \right. $$

Given $\mathcal{T} \in \mathcal{P}(\Delta^{\text{NF}})$ we say that:

- $\mathcal{T}$ is downward closed whenever $\forall t \text{ s.t. } \exists t' \in \mathcal{T}, t \leq t'$, we have $t \in \mathcal{T}$;

- $\mathcal{T}$ is directed, whenever $\forall t, t' \in \mathcal{T}$, we have $\exists t'' \in \mathcal{T}$, s.t. $t, t' \leq t''$;

- $\mathcal{T}$ is an ideal whenever it is downward closed and directed.

Notice that the relation $\leq$ is transitive but not reflexive (i.e. it is not a preorder). For instance, $\langle y \rangle[\langle y \rangle 1[y], \langle y \rangle[y]1] \not\leq \langle y \rangle[\langle y \rangle 1[y], \langle y \rangle[y]1]$, as $\langle y \rangle 1[y] \not\leq \langle y \rangle[y]1$ as well as $\langle y \rangle[y]1 \not\leq \langle y \rangle 1[y]$. It is not antireflexive either, for example $\langle y \rangle[x] \leq \langle y \rangle[x]$. Moreover, it is neither symmetric nor antisymmetric. We have $\langle y \rangle[x]1 \leq \langle y \rangle[x][x]$, but $\langle y \rangle[x][x] \not\leq \langle y \rangle[x]1$, and $\langle y \rangle[t] \leq \langle y \rangle[t, t]$, $\langle y \rangle[t, t] \leq \langle y \rangle[t]$ but $\langle y \rangle[t] \neq \langle y \rangle[t, t]$. However, on the simple terms having bags of at most one element, $\leq$ is an order relation.

We need to formalize what is an “effective element” of $\mathcal{P}(\Delta^{\text{NF}})$. In order to do that, we use the notion of a recursively enumerable subset of $\mathbb{N}$ and an encoding of $\Delta^{\text{NF}}$ into $\mathbb{N}$. Let $G$ be any effective bijection between $\Delta^{\text{NF}}/\equiv_\alpha$ and $\mathbb{N}$. One way of defining $G$ is by using the De Brujin notation [4], which gives a system of canonical representatives for the $\alpha$-equivalence. We will omit such details, so we fix once and for all a recursive Gödel numbering $G : \Delta^{\text{NF}} \mapsto \mathbb{N}$.

**► Definition 10 (Effectiveness).** An element $\mathcal{T}$ of $\mathcal{P}(\Delta^{\text{NF}})$ is recursively enumerable, r.e. for short, whenever the set $G(\mathcal{T}) \stackrel{\Delta}{=} \{G(t) ; t \in \mathcal{T}\} \subseteq \mathbb{N}$ is recursively enumerable, i.e. either $\mathcal{T} = \emptyset$, or there exists a total recursive function $\phi : \mathbb{N} \mapsto \mathbb{N}$ such that $G(\mathcal{T}) = \{\phi(n) ; n \in \mathbb{N}\}$.

Notice that the notion of a r.e. element of $\mathcal{P}(\Delta^{\text{NF}})$ does not depend on the chosen Gödel enumeration of $\Delta^{\text{NF}}$.

**► Definition 11.** We say that a set $\mathcal{T} \in \mathcal{P}(\Delta^{\text{NF}})$ is single-headed with width $n$, whenever there exist $m \in \mathbb{N}$, $x_0, \dots, x_{m-1}, y \in \text{Var}$, $J \subseteq \mathbb{N}$ and, for each $i < n$, a family $(\mu_i^j)_{j \in J}$ of bags such that:

$$ \mathcal{T} = \{ \lambda x_0 \dots x_{m-1} \cdot \langle y \rangle \mu_0^j \dots \mu_{n-1}^j \mid j \in J \}. \qquad (11) $$

For each $i$, we denote by $\hat{T}_i$ the set $\{\mu_i^j \mid j \in J\}$ and simply by $\mathcal{T}_i$ the set $\bigcup_{j \in J} |\mu_i^j|$. Notice that $\hat{T}_i \subseteq \mathcal{M}_F(\mathcal{T}_i)$.

**► Lemma 12.** If $\mathcal{T}$ is directed then $\mathcal{T}$ is single-headed and $\mathcal{T}_i$ is directed (for every $i$ less than the width of $\mathcal{T}$). Let $\mathcal{T} \in \mathcal{P}(\Delta^{\text{NF}})$ be non-empty. If $\mathcal{T}$ is single-headed with width $n \in \mathbb{N}$ and downward closed then $\mathcal{T}_i$ is downward closed (for every $i < n$).

**Proof.** It is straightforward to check that $\mathcal{T}$ directed implies $\mathcal{T}$ single-headed.

From now on assume $\mathcal{T}$ is single-headed of width $n$ and let us prove that $\mathcal{T}_i$ is downward closed (resp. directed) whenever $\mathcal{T}$ is downward closed (resp. directed).

Let $u' \leq u \in \mathcal{T}_i$. This means that there is $t = \lambda x_0 \dots x_{m-1} \cdot \langle y \rangle \mu_0 \dots \mu_{n-1} \in \mathcal{T}$, such that $u \in |\mu_i|$. Define $t' \stackrel{\Delta}{=} \lambda x_0 \dots x_{m-1} \cdot \langle y \rangle 1 \dots 1[u']1 \dots 1$ and notice that $t' \leq t$. By the downward closedness of $\mathcal{T}$ we conclude $t' \in \mathcal{T}$, so $u' \in \mathcal{T}_i$ and hence $\mathcal{T}_i$ is downward closed.

Let $u_1, u_2 \in \mathcal{T}_i$. We have in $\mathcal{T}$ two elements $t_1 = \lambda x_0 \dots x_{m-1} \cdot \langle y \rangle \mu_0^1 \dots \mu_{n-1}^1$ and $t_2 = \lambda x_0 \dots x_{m-1} \cdot \langle y \rangle \mu_0^2 \dots \mu_{n-1}^2$, such that $u_1 \in |\mu_i^1|$ and $u_2 \in |\mu_i^2|$. By directedness of $\mathcal{T}$,
there is an element $t_3 = \lambda x_0 \dots x_{m-1} \cdot \langle y \rangle \mu_0^3 \dots \mu_{n-1}^3 \in \mathcal{T}$ such that $t_1, t_2 \preceq t_3$. So, there is $v_1, v_2 \in |\mu_i^3|$, such that $u_1 \preceq v_1$ and $u_2 \preceq v_2$. Again by directedness of $\mathcal{T}$, there exists $t_4 = \lambda x_0 \dots x_{m-1} \cdot \langle y \rangle \mu_0^4 \dots \mu_{n-1}^4 \in \mathcal{T}$ such that $t_3 \preceq t_4$, so there exists $w \in |\mu_i^4|$, such that $v_1, v_2 \preceq w$. We have $w \in \mathcal{T}_i$ and by transitivity, $u_1, u_2 \preceq w$. Hence $\mathcal{T}_i$ is directed. ◀

We now define a coherence relation on normal simple terms, originally introduced in [9], which will mainly be used to approximate the notion of ideal. Indeed, we will show that every ideal is a clique (Proposition 16) and every clique is included in an ideal (Proposition 20).

**Definition 13 (Coherence, [9, §3]).** The coherence relation $\preceq$ on $\Delta^{\text{NF}}$ is defined by:

$$ \lambda x_0 \dots x_{m-1} \cdot \langle y \rangle \mu_0 \dots \mu_{n-1} \preceq t \quad \text{iff} \quad \left\{ \begin{array}{l} t = \lambda x_0 \dots x_{m-1} \cdot \langle y \rangle \nu_0 \dots \nu_{n-1} \text{ and} \\ \forall i < n, \forall u, u' \in |\mu_i \cdot \nu_i|, u \preceq u'. \end{array} \right. $$

We call $\mathcal{T} \in \mathcal{P}(\Delta^{\text{NF}})$ a clique whenever $\forall t, t' \in \mathcal{T}, t \preceq t'$.

Notice that $\preceq$ is symmetric, but not reflexive. For example, $\langle y \rangle[x, z] \not\preceq \langle y \rangle[x, z]$. Let us stress, however, that the previous example $\langle y \rangle[\langle y \rangle 1[y], \langle y \rangle[y]1]$ showing the non-reflexivity of $\preceq$, is indeed coherent with itself. Furthermore, $\preceq$ is not transitive. We have $\langle y \rangle[x][z] \preceq \langle y \rangle[x]1$ and $\langle y \rangle[x][y] \preceq \langle y \rangle[x]1$ but $\langle y \rangle[x][z] \not\preceq \langle y \rangle[x][y]$.

As a direct consequence of the definition of coherence we get the following lemma.

**Lemma 14 (Hereditary characterization of cliques).** Let $\mathcal{C} \in \mathcal{P}(\Delta^{\text{NF}})$, $\mathcal{C}$ is a clique iff $\mathcal{C}$ is single-headed of a certain width $n$ and for each $i < n$, $\mathcal{C}_i$ is a clique.

Hereafter, we will often use the induction of the following notion of height, analogous to the definition of height of a Böhm-like tree.

**Definition 15 (Height).** Given a simple normal form $t = \lambda x_0 \dots x_{m-1} \cdot \langle y \rangle \mu_0 \dots \mu_{n-1}$, we define height($t$) = $1 + \max_i(\max_{t_i \in |\mu_i|} \text{height}(t_i))$. The height of a set $\mathcal{T} \in \mathcal{P}(\Delta^{\text{NF}})$ is height($\mathcal{T}$) = $\sup_{t \in \mathcal{T}}$ (height($t$)). We define $\mathcal{T}|_h = \{t \in \mathcal{T} \mid \text{height}(t) < h\}$.

Notice that height($t$) = 1 if and only if $t$ has only empty bags. Of course, the height of a set of simple normal forms $\mathcal{T}$ can be infinite. For example, height(NF($\tau(\Theta)$)) = $\infty$, while height(NF($\tau(S)$)) = 3.

**Proposition 16 (Ideals are cliques).** If $\mathcal{D} \in \mathcal{P}(\Delta^{\text{NF}})$ is an ideal then $\mathcal{D}$ is a clique.

**Proof.** It is enough to check that, for every two terms $t_1, t_2 \in \Delta^{\text{NF}}$, if there exists an ideal $\mathcal{D}'$ such that $t_1, t_2 \in \mathcal{D}'$ then $t_1 \preceq t_2$. Let us prove this claim by induction on the maximal height among $t_1$ and $t_2$. Since $\mathcal{D}'$ is an ideal there exists $t_3 \in \mathcal{D}'$ such that $t_1, t_2 \preceq t_3$ and, by Lemma 12, $\mathcal{D}'$ is single-headed of a certain width $n$, so there exist bags $\mu_i^j$ such that

$$ t_j = \lambda x_0 \dots x_{m-1} \cdot \langle y \rangle \mu_0^j \dots \mu_{n-1}^j \text{ (for each } j = 1, 2, 3), $$

moreover each $\mathcal{D}'_i$ is directed.

If $\max(\text{height}(t_1), \text{height}(t_2)) = 1$ then $t_1 = t_2 = \lambda x_0 \dots x_{m-1} \cdot \langle y \rangle 1 \dots 1$ and this term is coherent with itself. Now let $h = \max(\text{height}(t_1), \text{height}(t_2))$. In order to prove $t_1 \preceq t_2$ we have to prove that for each $i < n$, for every $u_1, u_2 \in |\mu_i^1 \cdot \mu_i^2|$, we have $u_1 \preceq u_2$. But $\max(\text{height}(u_1), \text{height}(u_2)) \le h - 1$ and $u_1, u_2$ belong to $\mathcal{D}'_i$ which is directed. We conclude by induction hypothesis. ◀

In fact, every subset of an ideal is a clique (just check that the proof above does not use the downward closure).
**► Definition 17 (Linearization).** Let $\mathcal{C}$ be a non-empty clique of finite height. The linearization of $\mathcal{C}$, defined by induction on height($\mathcal{C}$), is the simple term $\mathcal{L}(\mathcal{C}) \triangleq \lambda x_0 \dots x_{m-1} \langle y \rangle \xi_0 \dots \xi_{n-1}$ where, for every $i < n$, $\xi_i = [\mathcal{L}(C_i)]$ if $C_i$ non-empty, otherwise $\xi_i = 1$.

**Lemma 18.** Let $\mathcal{C} \subseteq \mathcal{D}$ be two non-empty cliques of finite height. We have: $\text{height}(\mathcal{L}(\mathcal{C})) = \text{height}(\mathcal{C})$, $\mathcal{L}(\mathcal{C}) \preceq \mathcal{L}(\mathcal{D})$ and, finally, $\forall t \in \mathcal{C}, t \preceq \mathcal{L}(\mathcal{C})$.

**Proof.** Let $\mathcal{C}$ and $\mathcal{D}$ satisfying the hypothesis. By Lemma 14, $\mathcal{C}$ and $\mathcal{D}$ are single headed with same width $n$. For any $i < n$, notice that $C_i \subseteq D_i$. We proceed by induction on height($\mathcal{C}$). If height($\mathcal{C}$) = 1, then $\mathcal{C} = \{\mathcal{L}(\mathcal{C}) = \lambda x_0 \dots x_{m-1} \langle y \rangle 1 \dots 1\}$. Clearly, one gets the statement. Otherwise, let height($\mathcal{C}$) > 1. Then $\mathcal{L}(\mathcal{C})$ is defined as in the equation of Definition 17. By Lemma 14, $D_i$ and $C_i$ are cliques. Hence, whenever $C_i$ is non-empty, we have by induction hypothesis that $\mathcal{L}(C_i)$ satisfies the statement of the lemma for $C_i$ and $D_i$. One can then easily conclude that height($\mathcal{L}(\mathcal{C})$) = height($\mathcal{C}$), and $\mathcal{L}(\mathcal{C}) \preceq \mathcal{L}(\mathcal{D})$ and, finally, $\forall t \in \mathcal{C}, t \preceq \mathcal{L}(\mathcal{C})$. ◀

**Lemma 19.** Let $\mathcal{D}$ be an ideal and let $\mathcal{C} \subseteq \mathcal{D}$ be a non-empty clique of finite height. Then, $\mathcal{L}(\mathcal{C}) \in \mathcal{D}$.

**Proof.** Let $\mathcal{D}$ and $\mathcal{C}$ satisfying the hypothesis. By Lemma 12, $\mathcal{D}$ (and hence $\mathcal{C}$) are single headed and of same width $n$. The proof of $\mathcal{L}(\mathcal{C}) \in \mathcal{D}$ is by induction on height($\mathcal{C}$).

Let $I$ be the set of indices $i < n$ such that $C_i$ is non-empty. If $I$ is empty, then $\mathcal{L}(\mathcal{C}) = \lambda x_0 \dots x_{m-1} \langle y \rangle 1 \dots 1$, and one can deduce that $\mathcal{L}(\mathcal{C}) \in \mathcal{D}$ since $\mathcal{D}$ is downward closed and $\mathcal{L}(\mathcal{C})$ is $\preceq$ to any element of $\mathcal{D}$. If otherwise $I$ is non-empty, then for every $i \in I$, we have that $C_i \subseteq D_i$, as well as that $C_i$ is a clique (Lemma 14). By induction hypothesis we can suppose $\mathcal{L}(C_i) \in D_i$. This means that there is $w_i \in \mathcal{D}$, $w_i = \lambda x_0 \dots x_{m-1} \langle y \rangle \rho_0 \dots \rho_{n-1}$, and $\mathcal{L}(C_i) \in \{\rho_i\}$. As $\mathcal{D}$ is directed and $\preceq$ is transitive, we can construct $w \in \mathcal{D}$ such that $w_i \preceq w$, for every $i \in I$. We remark that $\mathcal{L}(\mathcal{C}) \preceq w \in \mathcal{D}$, therefore $\mathcal{L}(\mathcal{C}) \in \mathcal{D}$. ◀

**Proposition 20 (Cliques can be ideals).** Let $\mathcal{C}$ be a clique. Then:

1. the set $\mathcal{I}(\mathcal{C}) \triangleq \{t \mid \exists h > 0, t \preceq \mathcal{L}(C|h)\}$ is an ideal;

2. This set $\mathcal{I}(\mathcal{C})$ is the smallest ideal containing $\mathcal{C}$.

**Proof.** Obviously $\mathcal{I}(\mathcal{C})$ is downward closed. Moreover, by Lemma 18, $\{\mathcal{L}(C|h)\}_{h \in \mathbb{N}}$ is a chain (in fact $C|h \subseteq C|_{h+1}$), hence directed. We conclude that $\mathcal{I}(\mathcal{C})$ is directed because the downward closure of a directed set is directed ($\preceq$ being a transitive relation).

As for item 2, first, we prove that $\mathcal{C} \subseteq \mathcal{I}(\mathcal{C})$. By Lemma 18, $C|h \subseteq \mathcal{I}(\mathcal{C})$, for every $h$. We conclude because $\mathcal{C} = \bigcup_h C|h$. Second, let $\mathcal{D}$ be an ideal containing $\mathcal{C}$, it is enough to prove $\mathcal{L}(C|h) \in \mathcal{D}$ for every $h$ for concluding $\mathcal{C} \subseteq \mathcal{D}$. This is a consequence of Lemma 19. ◀

**Corollary 21.** Let $\mathcal{C}$ be a maximal clique. Then, $\mathcal{C}$ is an ideal.

**Proof.** Let $\mathcal{C}$ be a maximal clique. By Proposition 20, $\mathcal{I}(\mathcal{C})$ is an ideal and $\mathcal{C} \subseteq \mathcal{I}(\mathcal{C})$. And by Proposition 16, $\mathcal{I}(\mathcal{C})$ is a clique. So we conclude by maximality of $\mathcal{C}$, that $\mathcal{C}$ is equal to the ideal $\mathcal{I}(\mathcal{C})$. ◀

Recall from Section 2 that we consider Böhm-like trees ordered by the set-theoretical inclusion on the graph of their functions. Indeed, such an order is reflected in their Taylor expansion.

**Lemma 22.** If $\mathcal{B}, \mathcal{B}'$ are Böhm-like trees, $\tau(\mathcal{B}) \subseteq \tau(\mathcal{B}')$ iff $\mathcal{B} \subseteq \mathcal{B}'$. Moreover, height($\mathcal{B}$) = height($\tau(\mathcal{B})$).
**Proof.** ⇒ We suppose that $\tau(\mathcal{B}) \subseteq \tau(\mathcal{B}')$. By induction on length($\alpha$), for any $\alpha \in \mathbb{N}^*$, we show that $\mathcal{B}(\alpha) = \mathcal{B}'(\alpha)$, whenever $\mathcal{B}(\alpha)$ is defined.

If $\mathcal{B}(\langle\rangle) = (\lambda x_0 \dots x_{m-1}. y, n)$, then $\lambda x_0 \dots x_{m-1}. \langle y \rangle 1 \dots 1 \in \tau(\mathcal{B}) \subseteq \tau(\mathcal{B}')$, therefore by definition $\mathcal{B}'(\langle\rangle) = (\lambda x_0 \dots x_{m-1}. y, n)$. The induction case follows because $\tau(\mathcal{B}) \subseteq \tau(\mathcal{B}')$ implies $\tau(\mathcal{B}_i) \subseteq \tau(\mathcal{B}'_i)$ for every $i < n$. Then, $\mathcal{B}(\langle i \rangle @\alpha) = \mathcal{B}_i(\alpha)$ which, by induction hypothesis, is equal to $\mathcal{B}'_i(\alpha) = \mathcal{B}'(\langle i \rangle @\alpha)$.

⇔ We suppose that $\mathcal{B} \subseteq \mathcal{B}'$. Let $t \in \tau(\mathcal{B})$, by induction on height($t$), one shows that $t \in \tau(\mathcal{B}')$. The reasoning is similar to the left-to-right implication.

The last statement regarding the height is trivial.

◀

**▶ Lemma 23.** Let $\mathcal{T} \in \mathcal{P}(\Delta^{\mathbf{NF}})$. There is a Böhm-like tree $\mathcal{B}$ such that $\tau(\mathcal{B}) = \mathcal{T}$ iff $\mathcal{T}$ is an ideal.

**Proof.** ⇒ The proof depends whether height($\mathcal{B}$) is finite or infinite.

If height($\mathcal{B}$) is finite, we proceed by induction on height($\mathcal{B}$). If $\mathcal{B}(\langle\rangle) = (\lambda x_0 \dots x_{m-1}. y, n)$, then $\tau(\mathcal{B}) = \{\lambda x_0 \dots x_{m-1}. \langle y \rangle \mu_0 \dots \mu_{n-1} \mid i < n, \mu_i \in \mathcal{M}_F(\tau(\mathcal{B}_i))\}$.

**Downward closure.** Let $t \preceq t' \in \tau(\mathcal{B})$. Since $t' \in \tau(\mathcal{B})$ we have $t'$ of the shape

$$t' = \lambda x_0 \dots x_{m-1} \langle y \rangle \mu_0' \dots \mu_{n-1}', \qquad (12)$$

Then, since $t \preceq t'$, $t$ is of the form

$$t = \lambda x_0 \dots x_{m-1} \langle y \rangle \mu_0 \dots \mu_{n-1}, \qquad (13)$$

such that, for every $i < n$, either $\mu_i = 1 \in \mathcal{M}_F(\tau(\mathcal{B}_i))$, or there exists $u' \in \mu_i'$ such that for any $u \in \mu_i$, $u \preceq u'$. Notice that $u' \in \tau(\mathcal{B}_i)$, so by induction hypothesis $u \in \tau(\mathcal{B}_i)$. Since this is the case for every $u \in \mu_i$, we get $\mu_i \in \mathcal{M}_F(\tau(\mathcal{B}_i))$. We conclude $t \in \tau(\mathcal{B})$.

**Directedness.** Let $t, t' \in \tau(\mathcal{B})$, and let us find $t''$ such that $t, t' \preceq t''$. The terms $t$ and $t'$ are as in Equation (13) and (12), respectively.

For $i < n$, $\mu_i \cdot \mu_i' \in \mathcal{M}_F(\tau(\mathcal{B}_i))$. By induction hypothesis, $\tau(\mathcal{B}_i)$ is directed. Since $\mu_i \cdot \mu_i'$ is finite (and $\preceq$ is transitive), if $\mu_i \cdot \mu_i'$ is non-empty, then there exists $t_i \in \tau(\mathcal{B}_i)$, such that for any $u \in \mu_i \cdot \mu_i'$, $u \preceq t_i$. Then, define $\xi_i = [t_i]$ if $\mu_i \cdot \mu_i'$ non-empty, otherwise $\xi_i = 1$. We set $t'' = \lambda x_0 \dots x_{m-1} \langle y \rangle \xi_0 \dots \xi_{n-1}$. Notice that $t'' \in \tau(\mathcal{B})$, since $\xi_i \in \mathcal{M}_F(\tau(\mathcal{B}_i))$, and $t, t' \preceq t''$.

Now let us consider the case height($\mathcal{B}$) = $\infty$. By definition $\tau(\mathcal{B}) = \bigcup_{h \in \mathbb{N}} \tau(\mathcal{B}|_h)$. Notice that $\tau(\mathcal{B}|_h)$ is a Böhm-like tree of finite height, so, by the previous reasoning, we can conclude that $\tau(\mathcal{B}|_h)$ is an ideal. Since $\{\mathcal{B}|_h\}_{h \in \mathbb{N}}$ is a chain, we can easily conclude that the whole $\tau(\mathcal{B})$ is an ideal.

⇔ In this case, we also split in two subcases, depending whether height($\mathcal{T}$) is finite or infinite. In the first case our induction is on height($\mathcal{T}$).

If height($\mathcal{T}$) = 0, then $\mathcal{T} = \emptyset$ and we choose the Böhm-like tree undefined everywhere. Otherwise, $\mathcal{T}$ is non-empty and we can write it as in Equation (11), by Lemma 12. Moreover, for any $i < n$, $\mathcal{T}_i$ is an ideal. By induction hypothesis, we can assume that there exists a Böhm-like tree $\mathcal{B}^i$ such that $\tau(\mathcal{B}^i) = \mathcal{T}_i$ (notice that $\mathcal{B}^i$ is the everywhere undefined function whenever $\mathcal{T}_i = \emptyset$). Define then $\mathcal{B}(\langle\rangle) \triangleq (\lambda x_0 \dots x_{m-1}. y, n)$ and $\mathcal{B}(\langle i \rangle @\alpha) = \mathcal{B}^i(\alpha)$. Note that in particular $\mathcal{B}_i = \mathcal{B}^i$.

In order to prove $\tau(\mathcal{B}) = \mathcal{T}$, we must show that $\hat{\mathcal{T}}_i = \mathcal{M}_F(\tau(\mathcal{B}_i))$, for every $i < n$. By Lemma 12, we only know that $\hat{\mathcal{T}}_i \subseteq \mathcal{M}_F(\mathcal{T}_i) = \mathcal{M}_F(\tau(\mathcal{B}^i)) = \mathcal{M}_F(\tau(\mathcal{B}_i))$. Let $\mu_i \in \mathcal{M}_F(\mathcal{T}_i)$, we prove that $\mu_i \in \hat{\mathcal{T}}_i$. Actually, we prove that the term $t_{\mu_i} \triangleq \lambda x_0 \dots x_{m-1} \langle y \rangle 1 \dots 1 \mu_i 1 \dots 1 \in \mathcal{T}$, which is enough to conclude.
If $\mu_i = 1$ then the bags in $t_{\mu_i}$ are all empty and so one concludes by the downward closure of $\mathcal{T}$, remarking that $t_{\mu_i}$ is $\leq$ to any element in $\mathcal{T}$. Otherwise, we have that $|\mu_i|$ is a non-empty sub-set of $\mathcal{T}_i$ of finite height (since it has finite cardinality). Moreover, since $\mathcal{T}_i$ is an ideal, $\mathcal{T}_i$, and hence $|\mu_i|$, are cliques (Proposition 16). We first apply Lemma 19 to $C = |\mu_i| \subseteq \mathcal{T}_i$. We then obtain $\mathcal{L}(|\mu_i|) \in \mathcal{T}_i$, so there exists $t \in \mathcal{T}$ whose $i$-th bag contains $\mathcal{L}(|\mu_i|)$. We further apply Lemma 18, arguing that $\forall u \in |\mu_i|$, $u \leq \mathcal{L}(|\mu_i|)$. This induces that $t_{\mu_i} \leq t$, so finally, $t_{\mu_i} \in \mathcal{T}$.

We now suppose that height($\mathcal{T}$) = $\infty$. Recall Definition 15, and notice that $\mathcal{T}|_h \subseteq \mathcal{T}$ is downward closed because $t \leq t'$ implies height($t$) $\leq$ height($t'$). We now show that $\mathcal{T}|_h$ is directed. In fact, take any two $t_1, t_2 \in \mathcal{T}|_h$. Set $C = \{t_1, t_2\} \subseteq \mathcal{T}$. By Proposition 16, $\mathcal{T}$ and $C$ are cliques, so by Lemma 18 and 19, $\mathcal{L}(\{t_1, t_2\}) \in \mathcal{T}$, $t_1, t_2 \leq \mathcal{L}(\{t_1, t_2\})$ and height($\mathcal{L}(\{t_1, t_2\})$) $\leq h$. We conclude $\mathcal{L}(\{t_1, t_2\}) \in \mathcal{T}|_h$.

We can then apply the reasoning for sets of finite heights and conclude that there exists $\mathcal{B}^h$ such that $\tau(\mathcal{B}^h) = \mathcal{T}|_h$. As $\{\mathcal{T}|_h\}_{h \in \mathbb{N}}$ is by definition a chain, we conclude with Lemma 22 that $\{\mathcal{B}^h\}_{h \in \mathbb{N}}$ is a chain. Let $\mathcal{B} = \bigcup_{h \in \mathbb{N}} \mathcal{B}^h$, we have that $\mathcal{B}$ is a Böhm-like tree. Remark that $\mathcal{B}|_h = \mathcal{B}^h$, as for any $h \in \mathbb{N}$, the difference between $\mathcal{B}^h$ and $\mathcal{B}^{h+1}$ lies only on the sequences of length $h$, which are undefined for $\mathcal{B}^h$. Finally $\tau(\mathcal{B}) \stackrel{\Delta}{=} \bigcup_{h \in \mathbb{N}} \tau(\mathcal{B}|_h) = \bigcup_{h \in \mathbb{N}} \tau(\mathcal{B}^h) = \bigcup_{h \in \mathbb{N}} \mathcal{T}|_h = \mathcal{T}$. $\quad$

**► Lemma 24.** Let $\mathcal{B}$ be a Böhm-like tree, then

■ FV($\mathcal{B}$) = FV($\tau(\mathcal{B})$),

■ $\mathcal{B}$ is r.e. iff $\tau(\mathcal{B})$ is r.e.

**Proof.** The only difficulty is to prove that $\tau(\mathcal{B})$ r.e. implies $\mathcal{B}$ r.e. Observe that an element $t$ of $\tau(\mathcal{B})$ defines a kind of subtree of $\mathcal{B}$ (in fact, a rooted thick subtree [2]) which can be used to define a partial function $f_t : \mathbb{N}^* \to \Sigma \times \mathbb{N}$ such that, whenever $f_t(\alpha)$ is defined, $f_t(\alpha)$ equals $\mathcal{B}(\alpha)$. Moreover for every $\alpha \in \mathbb{N}^*$, such that $\mathcal{B}(\alpha)$ is defined, there exists $t \in \tau(\mathcal{B})$ such that $f_t(\alpha)$ is defined. Hence, given an effective enumeration of $\tau(\mathcal{B})$, one can compute $\mathcal{B}(\alpha)$ by iterating over $\tau(\mathcal{B})$ with $t$ until $f_t(\alpha)$ is defined (if $\mathcal{B}(\alpha)$ is undefined this will never end). $\quad$

**► Theorem 25.** Let $\mathcal{T} \in \mathcal{P}(\Delta^{\mathbf{NF}})$. There is a $\lambda$-term $M$ such that $\mathrm{NF}(\tau(M)) = \mathcal{T}$ iff the following conditions hold:

1. FV($\mathcal{T}$) is finite,

2. $\mathcal{T}$ is r.e.,

3. $\mathcal{T}$ is an ideal wrt $\leq$.

**Proof.** By Theorem 8, the equality $\mathrm{NF}(\tau(M)) = \mathcal{T}$ can be replaced by $\tau(\mathrm{BT}(M)) = \mathcal{T}$. Then, by Theorem 5 the condition at the left-hand side of the iff can be replaced by “there is a Böhm-like tree $\mathcal{B}$ such that (i) FV($\mathcal{B}$) is finite, (ii) $\mathcal{B}$ is r.e., (iii) $\tau(\mathcal{B}) = \mathcal{T}$”. The equivalence is then achieved by Lemma 23 and 24. $\quad$

In [9], Ehrhard and Regnier noticed that the Taylor expansion of normal forms are maximal cliques with respect to the set-theoretical inclusion. However, not every maximal clique $\mathcal{T}$ represents a normalizable $\lambda$-term, even if $\mathcal{T}$ enjoys the conditions of Theorem 25. For example, $\mathrm{NF}(\tau(\boldsymbol{\Theta}))$ is a maximal clique. We define the total $\lambda$-terms (called $\perp$-free in [1, Definition 10.1.12]) and prove that they correspond to the property of being a maximal clique in $\mathcal{P}(\Delta^{\mathbf{NF}})$.
**Definition 26 (Totality).** A Böhm-like tree $\mathcal{B}$ is total whenever $\mathcal{B}(\langle\rangle) \downarrow$ and $\mathcal{B}(\alpha) = (a,n)$ implies that for all $i < n$, $\mathcal{B}(\alpha@\langle i \rangle) \downarrow$. A $\lambda$-term $M$ is total whenever $M \xrightarrow{h_*} \lambda x_0 \dots x_{m-1}.(y)M_0 \dots M_{n-1}$ and $M_0, \dots M_{n-1}$ are total, i.e. $\text{BT}(M)$ is total.

**Lemma 27.** Let $\mathcal{B}$ be a Böhm-like tree. The set $\tau(\mathcal{B})$ is a maximal clique (with respect to the set-theoretical inclusion) iff $\mathcal{B}$ is total.

**Proof.** One proves the equivalent statement: there exists $t \in \Delta^{\text{NF}}$, $t \not\in \tau(\mathcal{B})$, coherent with any element of $\tau(\mathcal{B})$, iff $\mathcal{B}$ is not total. The left-to-right direction is by induction on height($t$), noticing that if a subtree $\mathcal{B}_i$ is not total, then $\mathcal{B}$ is not total. The converse direction is by induction on length($\alpha$) for a sequence $\alpha$ such that $\mathcal{B}(\alpha) = (a,n)$ but there is $i < n$, $\mathcal{B}(\alpha@\langle i \rangle) \uparrow$. ◀

**Corollary 28.** Let $\mathcal{T} \in \mathcal{P}(\Delta^{\text{NF}})$. There is a total $\lambda$-term $M$ such that $\text{NF}(\tau(M)) = \mathcal{T}$ iff

1. $\text{FV}(\mathcal{T})$ is finite,

2. $\mathcal{T}$ is r.e.,

3. $\mathcal{T}$ is a maximal clique.

**Proof.** $\implies$ By Theorem 25, we get **1** and **2**. Condition **3** is a consequence of Theorem 8 and Lemma 27.

$\Leftarrow$ By Lemma 21 and Theorem 25 we get a $\lambda$-term $M$ such that $\text{NF}(\tau(M)) = \mathcal{T}$. By Theorem 8 and Lemma 27 we conclude that $M$ is total. ◀

Of course, one would like to characterize the property of having a $\beta$-normal form.

**Corollary 29.** Let $\mathcal{T} \in \mathcal{P}(\Delta^{\text{NF}})$. There is a normalizable $\lambda$-term $M$ such that $\text{NF}(\tau(M)) = \mathcal{T}$ iff

1. $\text{height}(\mathcal{T})$ is finite,

2. $\mathcal{T}$ is a maximal clique.

**Proof.** $\implies$ Remark that if $M$ is normalizable, then $\text{BT}(M)$ is total and of finite height. In fact, $\text{BT}(M)$ is the applicative tree of the normal form of $M$. By Corollary 28, $\text{NF}(\tau(M))$ is a maximal clique. By Theorem 8 and Lemma 22 we get that $\text{height}(\text{NF}(\tau(M)))$ is finite.

$\Leftarrow$ Consider the simple term $\mathcal{L}(\mathcal{T})$. One can easily prove that $\mathcal{L}(\mathcal{T})$ does not contain empty bags, otherwise $\mathcal{T}$ would not be maximal. Moreover, by induction of height($\mathcal{L}(\mathcal{T})$), one also proves that the $\lambda$-term $M$ obtained from $\mathcal{L}(\mathcal{T})$ by replacing any resource application $\langle t \rangle [u]$ with a $\lambda$-calculus application $(t)u$ is such that $\mathcal{L}(\mathcal{T}) \in \tau(M)$. Let us prove that $\mathcal{T} = \tau(M)$. By Proposition 20, $\mathcal{I}(\{\mathcal{L}(\mathcal{T})\})$ is the smallest ideal containing $\mathcal{L}(\mathcal{T})$, so $\mathcal{I}(\{\mathcal{L}(\mathcal{T})\}) \subseteq \tau(M)$. By Lemma 18, for every $t \in \mathcal{T}$, $t \preceq \mathcal{L}(\mathcal{T})$, hence $\mathcal{T} \subseteq \mathcal{I}(\{\mathcal{L}(\mathcal{T})\}) \subseteq \tau(M)$. By the maximality of $\mathcal{T}$ we conclude $\mathcal{T} = \tau(M)$. ◀

Let us notice that the simple term $\mathcal{L}(\mathcal{T})$ used in the proof of Corollary 29 for proving the existence of a $\beta$-normal form $M$ s.t. $\tau(M) = \mathcal{T}$ is called the *linearization* of $M$ in [9].

**5 Conclusion**

The main Theorem 25, combined with Ehrhard and Regnier's Equation 2, gives a characterization of the support $\text{NF}(\tau(M))$ of $\text{NF}(M^*)$ that can be extended to a characterization of $\text{NF}(M^*)$ itself (with positive rational coefficients instead of booleans). This refinement can be done by requiring in addition that the coefficient of each non-zero element $t$ of the formal combination should exactly be the so-called *multiplicity coefficient* $m(t)$ of $t$, a number defined by induction on $t$ through the use of a generalization of binomial coefficients to
multisets (see [9]). Roughly speaking the multiplicity coefficient of a simple term *t* expresses the various ways *t* can be recombined into itself by varying enumeration of multisets.

Such a strict correspondence between supports and coefficients is lost in a non-deterministic setting. Ehrhard and Regnier's Equation 2 is due to the fact that the supports of the Taylor expansions of the λ-terms are cliques, and this is false as soon as one allows to superpose programs (e.g. by adding an or constructor, or a random operator). An open issue is then to capture the convergence of formal combinations of simple terms to non-deterministic, or probabilistic λ-terms.

**Acknowledgement.** We thank the reviewers for their useful and detailed comments on improving the quality of this publication.

References

1. Henk Barendregt. *The lambda calculus: its syntax and semantics*. North-Holland, Amsterdam, 1984.

2. Pierre Boudes. Thick subtrees, games and experiments. In Pierre-Louis Curien, editor, *Proceedings of TLCA 2009*, number 5608 in Lecture Notes in Computer Sciences, pages 65–79. Springer Verlag, 2009.

3. Gérard Boudol, Pierre-Louis Curien, and Carolina Lavatelli. A semantics for lambda calculi with resources. *Mathematical Structures in Computer Science*, 9(4):437–482, 1999.

4. N.G. de Bruijn. A survey of the project automath. In J.H. Geuvers R.P. Nederpelt and R.C. de Vrijer, editors, *Selected Papers on Automath*, volume 133 of *Studies in Logic and the Foundations of Mathematics*, pages 141 – 161. Elsevier, 1994.

5. Thomas Ehrhard. On Köthe sequence spaces and linear logic. *Mathematical Structures in Computer Science*, 12(5):579–623, 2003.

6. Thomas Ehrhard. Finiteness spaces. *Mathematical Structures in Computer Science*, 15(4):615–646, 2005.

7. Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. *Theoretical Computer Science*, 309(1):1–41, 2003.

8. Thomas Ehrhard and Laurent Regnier. Böhm trees, Krivine's machine and the Taylor expansion of lambda-terms. In Arnold Beckmann, Ulrich Berger, Benedikt Löwe, and John V. Tucker, editors, *CiE*, volume 3988 of *Lecture Notes in Computer Science*, pages 186–197. Springer, 2006.

9. Thomas Ehrhard and Laurent Regnier. Uniformity and the Taylor Expansion of Ordinary Lambda-Terms. *Theor. Comput. Sci.*, 403(2-3):347–372, 2008.

10. Fanny He. On the Characterization of the Taylor Expansion of λ-terms. Master's thesis, LMFI – Paris VII, France, October 2012.

11. Jean-Louis Krivine. *Lambda-calcul: types et modèles*. Études et recherches en informatique. Masson, 1990.

12. Michele Pagani and Christine Tasson. The Taylor Expansion Inverse Problem in Linear Logic. In Andrew Pitts, editor, *Proceedings of the Twenty-Fourth Annual IEEE Symposium on Logic in Computer Science (LICS 2009)*, pages 222–231. IEEE Computer Society Press, 2009.

13. Paolo Tranquilli. Intuitionistic differential nets and lambda-calculus. *Theoretical Computer Science*, 412(20):1979–1997, 2011.