Strong Normalizability as a Finiteness Structure via the Taylor Expansion of $\lambda$-terms

Abstract

In the folklore of linear logic, a common intuition is that the structure of finiteness spaces, introduced by Ehrhard, semantically reflects the strong normalization property of cut-elimination.

We make this intuition formal in the context of the non-deterministic $\lambda$-calculus by introducing a finiteness structure on resource terms, which is such that a $\lambda$-term is strongly normalizing iff the support of its Taylor expansion is finitary.

An application of our result is the existence of a normal form for the Taylor expansion of any strongly normalizable non-deterministic $\lambda$-term.

Supported by French ANR Project Coquas (number ANR 12 JS02 006 01).

1 Introduction

It is well-known that sets and relations can be presented as a category of modules and linear functions over the boolean semi-ring, giving one of the simplest semantics of linear logic. In [10] (see also [9]), it is shown how to generalize this construction to any complete¹ semi-ring $\mathcal R$ and yet obtain a model of linear logic. In particular, the composition of two matrices $\phi \in \mathcal R^{A\times B}$ and $\psi \in \mathcal R^{B\times C}$ is given by the usual matrix multiplication:

$$\begin{aligned} (\phi ; \psi )_{a,c} \mathrel {\mathop :\!=}\sum _{b\in B} \phi _{a,b}\cdot \psi _{b,c} \end{aligned}$$

(1)

The semi-ring $\mathcal R$ must be complete because the above sum might be infinite. This is an issue, because it prevents us from considering standard vector spaces, which are usually constructed over “non-complete” fields like reals or complexes.

In order to overcome this problem, Ehrhard introduced the notion of finiteness space [3]. A finiteness space is a pair of a set A and a set $\mathfrak {A}$ (called finiteness structure in Definition 7) of subsets of A which is closed under a notion of duality. The point is that, for any field $\mathcal K$ (resp. any semi-ring), the set of vectors in $\mathcal K^{A}$ whose support² is in $\mathfrak {A}$ constitutes a vector space (resp. a module) over $\mathcal K$. Moreover, any two matrices $\phi \in \mathcal K^{A\times B}$ and $\psi \in \mathcal K^{B\times C}$ whose supports are in resp. $\mathfrak {A}\multimap \mathfrak {B}$ and $\mathfrak {B}\multimap \mathfrak {C}$ (the finiteness structures associated with the linear arrow) compose, because the duality condition on the supports makes the terms in the sum of Eq. (1) be zero almost everywhere. This gives rise to a category which is a model of linear logic and its differential extension.

The notion of finiteness space seems strictly related to the property of normalization. Already in [3], it is remarked that the coKleisli category of the exponential comonad is a model of simply typed $\lambda$-calculus, but it is not cpo-enriched and thus cannot interpret (at least in a standard way) fixed-point combinators, so neither PCF nor untyped $\lambda$-calculus. Moreover, in the setting of differential nets, Pagani showed that the property of having a finitary interpretation corresponds to an acyclicity criterion (called visible acyclicity [12]) which entails the normalization property of the cut-elimination procedure [11], while there are examples of visibly cyclic differential nets which do not normalize.

The goal of this paper is to shed further light on the link between finiteness spaces and normalization, this time considering the non-deterministic untyped $\lambda$-calculus. Since we deal with $\lambda$-terms and not with linear logic proofs (or differential nets), we will speak about formal power series rather than matrices at the semantical level. This corresponds to move from the morphisms of a linear category to those of its coKleisli construction. Moreover, following [7], we describe the monomials of these power series as resource terms in normal form. The benefit of this setting is that the interpretation of a $\lambda$-term M as a power series [|M|] can be decomposed in two distinct steps: first, the term M is associated with a formal series ${M}^*$ of resource terms possibly with redexes, called the Taylor expansion of M (see Table 1a); second, one reduces each resource term t appearing in the support $\mathcal {T}\left( M\right)$ of ${M}^*$ into a normal form $\mathrm {NF}(t)$ and sum up all the results, that is (${M}^*_t$ denotes the coefficient of t in ${M}^*$):

$$\begin{aligned}{}[|M|] = \sum _{t\in \mathcal {T}\left( M\right) } {M}^*_t\cdot \mathrm {NF}(t) \end{aligned}$$

(2)

The issue about the convergence of infinite sums appears in Eq. (2) because there might be an infinite number of resource terms in $\mathcal {T}\left( M\right)$ reducing to the same normal form and thus possibly giving infinite coefficients to the formal series [|M|]. Ehrhard and Regnier proved in [7] that this is not the case for deterministic $\lambda$-terms, however the situation gets worse in presence of non-deterministic primitives. If we allow sums $M+N$ representing potential reduction to M or N, then one can construct terms evaluating to a variable y an infinite number of times, like (where $\mathbf \Theta$ denotes Turing’s fixed-point combinator):

$$\begin{aligned} \left( \mathbf \Theta \right) \lambda x.(x+y)\rightarrow _\beta ^*\left( \mathbf \Theta \right) \lambda x.(x+y)+y\rightarrow _\beta ^*\left( \mathbf \Theta \right) \lambda x.(x+y)+y+y\rightarrow _\beta ^*\dots \end{aligned}$$

(3)

We postpone to Examples 1 and 4 a more detailed discussion of $\left( \mathbf \Theta \right) \lambda x.(x+y)$, however we can already guess that this interplay between infinite reductions and non-determinism may produce infinite coefficients.

One can then wonder whether there are interesting classes of terms where the coefficients of the associated power series can be kept finite. Ehrhard proved in [4] that the terms typable by a non-deterministic variant of Girard’s System $\mathcal F$ have always finite coefficients. A by-product of our results is Corollary 39, which is a generalization of Ehrhard’s result: every strongly normalizable non-deterministic $\lambda$-term can be interpreted by a power series with finite coefficients.

The main focus of our paper is however in the means used for obtaining this result rather than on the result itself. The proof in [4] is based on a finiteness structure $\mathfrak {S}$ over the set of resource terms $\varDelta ^{}$, such that any term M typable in System $\mathcal F$ has the support $\mathcal {T}\left( M\right)$ of its Taylor expansion in $\mathfrak {S}$. We show that this method can be both generalized and strengthened in order to characterize strong normalization via finiteness structures. Namely, we give sufficient conditions on a finiteness structure $\mathfrak {S}$ over $\varDelta ^{}$ such that for every non-deterministic $\lambda$-term M: (i) if M is strongly normalizable, then $\mathcal {T}\left( M\right) \in \mathfrak {S}$ (Corollary 30); (ii) if $\mathcal {T}\left( M\right) \in \mathfrak {S}$, then M is strongly normalizable (Theorem 36).

Fig. 1.

Main results of the paper

Contents. Section 2 gives the preliminary definitions: the non-deterministic $\lambda$-calculus, its Taylor expansion into formal series of resource terms and the notion of finiteness structure. The proof of Item (i) splits into Sects. 3 and 4, using an intersection type system (Table 2) for characterizing strong normalization. Section 5 gives the proof of Item (ii) and Sect. 6 concludes with Corollary 39 about the finiteness of the coefficients of the power series of strongly normalizable terms. Figure 1 sums up the main results of the paper.

2 Preliminaries

2.1 Non-deterministic $\lambda$-calculus $\varLambda _+^{}$

The non-deterministic $\lambda$-calculus is defined by the following grammar³:

$$\begin{aligned} \lambda \text {-terms }&\varLambda _+^{}:&M \mathrel {\mathop :\!=}x \mid \mathord {\lambda x.M} \mid \left( M\right) M \mid M + M \end{aligned}$$

subject to $\alpha$-equivalence and to the following identities:

$$\begin{aligned} M+N = N+M, \qquad (M+N)+P = M+(N+P), \end{aligned}$$

$$\begin{aligned} \mathord {\lambda x.(M+N)} = \mathord {\lambda x.M} + \mathord {\lambda x.N}, \left( M+N\right) P = \left( M\right) P + \left( N\right) P. \end{aligned}$$

The last two equalities state that abstraction is a linear operation (i.e. commutes with sums) while application is linear only in the function but not in the argument (i.e. $\left( P\right) (M+N)\ne \left( P\right) M + \left( P\right) N$). Notice also that the sum is not idempotent: $M+M\ne M$. This is a crucial feature for making a difference between terms reducing to a value once, twice, more times or an infinite number of times (see the discussion about Eq. (3) in the Introduction).

Although this follows an old intuition from linear logic, the first extension of the $\lambda$-calculus with (a priori non idempotent) sums subject to these identities was, as far as we know, the differential $\lambda$-calculus of Ehrhard and Regnier [5]. This feature is now quite standard in the literature following this revival of quantitative semantics.

The (capture avoiding) substitution of a term for a variable is defined as usual and $\beta$-reduction $\rightarrow _\beta$ is defined as the context closure of:

$$\begin{aligned} \left( \mathord {\lambda x.M}\right) N \rightarrow _\beta {M}\left[ {N}/{x}\right] . \end{aligned}$$

We denote as $\rightarrow _\beta ^*$ the reflexive-transitive closure of $\rightarrow _\beta$.

Example 1

Some $\lambda$-terms which will be used in the following are:

$$\begin{aligned} \mathbf \varDelta \mathrel {\mathop :\!=}\lambda x.\left( x\right) x,\qquad \mathbf \Omega \mathrel {\mathop :\!=}\left( \mathbf \varDelta \right) \mathbf \varDelta ,\qquad \mathbf {\varDelta _3}\mathrel {\mathop :\!=}\lambda x.\left( x\right) xx, \qquad \mathbf {\Omega _3}\mathrel {\mathop :\!=}\left( \mathbf {\varDelta _3}\right) \mathbf {\varDelta _3}, \end{aligned}$$

$$\begin{aligned} \mathbf \Theta \mathrel {\mathop :\!=}\left( \lambda xy. \left( y\right) \left( x\right) xy\right) \lambda xy. \left( y\right) \left( x\right) xy. \end{aligned}$$

The term $\mathbf \Omega$ is the prototypical diverging term, reducing to itself in one single $\beta$-step. $\mathbf {\Omega _3}$ is another example of diverging term, producing terms of greater and greater size: $\mathbf {\Omega _3}\rightarrow _\beta \left( \mathbf {\Omega _3}\right) \mathbf {\varDelta _3}\rightarrow _\beta \left( \mathbf {\Omega _3}\right) \mathbf {\varDelta _3}\mathbf {\varDelta _3}\rightarrow _\beta \dots$ It will be used in Remark 37 to prove the subtlety of characterizing strong normalization with finiteness spaces. The Turing fixed-point combinator $\mathbf \Theta$ has been used in the Introduction to construct $\left( \mathbf \Theta \right) \lambda x.(x+y)$ as an example of non-deterministic $\lambda$-term morally reducing to normal forms with infinite coefficients (Eq. (3)). Notice that, by abstraction linearity, $\left( \mathbf \Theta \right) \lambda x.(x+y)=\left( \mathbf \Theta \right) (\lambda x.x+\lambda x.y)$, however $\left( \mathbf \Theta \right) (\lambda x.x+\lambda x.y)\ne \left( \mathbf \Theta \right) \lambda x.x+\left( \mathbf \Theta \right) \lambda x.y$, because application is not linear in the argument. This distinction is crucial: the latter term reduces to $(\left( \mathbf \Theta \right) \lambda x.x) + y$, with $\left( \mathbf \Theta \right) \lambda x.x$ reducing to itself without producing any further occurence of y.

2.2 Resource Calculus $\varDelta ^{}$ and Taylor Expansion

The syntax. Resource terms and bags are given by mutual induction:

$$\begin{aligned} \text {resource terms }&\varDelta ^{}:&s&\mathrel {\mathop :\!=}x \mid \lambda x.s \mid \left\langle s \right\rangle \,\overline{s}&\text {bags }&{{\varDelta ^{}}}^!:&\overline{s}&\mathrel {\mathop :\!=}1 \mid s\cdot \overline{s} \end{aligned}$$

subject to both $\alpha$-equivalence and permutativity of $(\cdot )$: we most often write $[s_1,\cdots ,s_n]$ for $s_1\cdot (\cdots \cdot (s_n \cdot 1)\cdots )$ and then $[s_1,\cdots ,s_n]= [s_{\sigma (1)},\cdots ,s_{\sigma (n)}]$ for any permutation $\sigma$. In other words, bags are finite multisets of terms.

Linear Extension. Let $\mathcal R$ be a rig (a.k.a. semi-ring). Of particular interest are the rigs $\mathbb {B}\mathrel {\mathop :\!=}(\left\{ 0,1\right\} , \max , \min )$ of booleans, $\mathbb N\mathrel {\mathop :\!=}(\mathbf N, +, \times )$ of non-negative integers and $\mathbb Q\mathrel {\mathop :\!=}(\mathbf Q, +, \times )$ of rational numbers. We denote as $\mathcal R[\![\varDelta ^{}]\!]$ (resp. $\mathcal R[\![{{\varDelta ^{}}}^!]\!]$) the set of all formal (finite or infinite) linear combinations of resource terms (resp. bags) with coefficients in $\mathcal R$. If $a\in \mathcal R[\![\varDelta ^{}]\!]$ (resp. $\overline{a}\in \mathcal R[\![{{\varDelta ^{}}}^!]\!]$) and $s\in \varDelta ^{}$ (resp. $\overline{s}\in {{\varDelta ^{}}}^!$), then $a_s\in \mathcal R$ (resp. $\overline{a}_{\overline{s}}\in \mathcal R$) denotes the coefficient of s in a (resp. $\overline{s}$ in $\overline{a}$). As is well-known, $\mathcal R[\![\varDelta ^{}]\!]$ is endowed with a structure of $\mathcal R$-module, where addition and scalar multiplication are defined component-wise, i.e. for $a,b\in \mathcal R[\![\varDelta ^{}]\!]$ and $\alpha \in \mathcal R$: $(a+b)_s\mathrel {\mathop :\!=}a_s+b_s$, and $(\alpha a)_s\mathrel {\mathop :\!=}\alpha a_s$. We will write $\left| a\right| \subseteq \varDelta ^{}$ for the support of a: $\left| a\right| =\left\{ s\in \varDelta ^{};\;a_s\not =0\right\}$.

Moreover, each resource calculus constructor extends to $\mathcal R[\![\varDelta ^{}]\!]$ component-wise, i.e. for any $a,a_1,\dots , a_n\in \mathcal R[\![\varDelta ^{}]\!]$ and $\overline{a}\in \mathcal R[\![{{\varDelta ^{}}}^!]\!]$, we set:

$$\begin{aligned} \textstyle \mathord {\lambda x.a} \mathrel {\mathop :\!=}\sum _{s\in \varDelta ^{}}a_s\mathord {\lambda x.s},\qquad \left\langle a \right\rangle \,\overline{a} \mathrel {\mathop :\!=}\sum _{s\in \varDelta ^{},\,\overline{s}\in {{\varDelta ^{}}}^!} a_s\overline{a}_{\overline{s}}\left\langle s \right\rangle \,\overline{s}, \end{aligned}$$

$$\begin{aligned} \textstyle \left[ a_1,\dots , a_n\right] \mathrel {\mathop :\!=}\sum _{s_1,\dots ,s_n\in \varDelta ^{}}\left( a_1\right) _{s_1}\cdots \left( a_n\right) _{s_n}\left[ s_1,\dots ,s_n\right] . \end{aligned}$$

Notice that the last formula is coherent with the notation of the concatenation of bags as a product since it expresses a distributivity law. In particular, we denote $a^n\mathrel {\mathop :\!=}\underbrace{\left[ a,\dots , a\right] }_n$ and if $\mathbb Q\subseteq \mathcal R$, $\displaystyle a^!\mathrel {\mathop :\!=}\sum _{n\in \mathbf N}\tfrac{1}{n!}a^n$.

In the case $\mathcal R=\mathbb {B}$, notice that $\mathbb {B}[\![\varDelta ^{}]\!]$ is the power-set lattice $\mathfrak {P}\left( \varDelta ^{}\right)$, so that we can use the set-theoretical notation: e.g. writing $s\in a$ instead of $a_s\ne 0$, or $a\cup b$ for $a+b$. Also, in that case the preceding formulas lead to: for $a,b\subseteq \varDelta ^{}$, $t\in \varDelta ^{}$, $\overline{a}\subseteq {{\varDelta ^{}}}^!$: $\mathord {\lambda x.a}\mathrel {\mathop :\!=}\left\{ \mathord {\lambda x.s};\;s\in a\right\}$, ${a}^!\mathrel {\mathop :\!=}\left\{ \left[ s_1,\cdots ,s_n\right] ;\;s_1,\cdots ,s_n\in a\right\}$, $\left\langle t \right\rangle \,\overline{a}\mathrel {\mathop :\!=}\left\{ \left\langle t \right\rangle \,\overline{s};\;\overline{s}\in \overline{a}\right\}$ and $\left\langle a \right\rangle \,\overline{a}\mathrel {\mathop :\!=}\bigcup \left\{ \left\langle s \right\rangle \,\overline{a};\;s\in a\right\}$.

Taylor expansion. Ehrhard and Regnier have used in [7] the rig of rational numbers to express the $\lambda$-terms as formal combinations in $\mathbb Q[\![\varDelta ^{}]\!]$. We refer to this translation ${(\;)}^*: \varLambda _+\mapsto \mathbb Q[\![\varDelta ^{}]\!]$ as the Taylor expansion and we recall it in Table 1a by structural induction. The supports of these expansions can be seen as a map $\mathcal {T}\left( \;\right) : \varLambda _+\mapsto \mathbb {B}[\![\varDelta ^{}]\!]$ and directly defined by induction as in Table 1b.

Table 1. Definition of the Taylor expansion ${(\;)}^*$ and of its support $\mathcal {T}\left( \;\right)$

Example 2

From the above definitions we have:

$$\begin{aligned} {\mathbf \varDelta }^*=\sum _{n}\frac{1}{n!}\lambda x.\left\langle x \right\rangle \,x^n,\qquad {\mathbf {\varDelta _3}}^*=\sum _{n,m}\frac{1}{n!m!}\lambda x.\left\langle \left\langle x \right\rangle \,x^n \right\rangle \,x^m. \end{aligned}$$

Let us denote as $\delta _n$ (resp. $\delta _{n,m}$) the term $\lambda x.\left\langle x \right\rangle \,x^n$ (resp. $\lambda x.\left\langle \left\langle x \right\rangle \,x^n \right\rangle \,x^m$). We can then write:

$$\begin{aligned} {\mathbf \Omega }^*= & {} \sum _{k}\frac{1}{k!}\sum _{n_0,\dots ,n_k}\frac{1}{n_0!\cdots n_k!}\left\langle \delta _{n_0} \right\rangle \,\left[ \delta _{n_1},\dots ,\delta _{n_k}\right] , \end{aligned}$$

(4)

$$\begin{aligned} {\mathbf {\Omega _3}}^*= & {} \sum _{k}\frac{1}{k!}\sum _{\begin{array}{c} n_0,\dots ,n_k\\ m_0,\dots ,m_k \end{array}} \frac{1}{n_0!m_0!\cdots n_k!m_k!}\left\langle \delta _{n_0,m_0} \right\rangle \,\left[ \delta _{n_1,m_1},\dots ,\delta _{n_k,m_k}\right] . \end{aligned}$$

(5)

It is clear that the resource terms appearing with non-zero coefficients in ${M}^*$ describe the structure of M taking an explicit number of times the argument of each application, and this recursively. The rôle of the rational coefficients will be clearer once defined the reduction rules over $\varDelta ^{}$ (see Example 5).

Operational Semantics. Let us write $\mathrm {deg}_{x}(t)$ for the number of free occurrences of a variable x in a resource term t. We define the differential substitution of a variable x with a bag $\left[ s_1,\cdots ,s_n\right]$ in a resource term t, denoted $\partial _{x}{t\cdot \left[ s_1,\cdots ,s_n\right] }$: it is a finite formal sum of resource terms, which is zero whenever $\mathrm {deg}_{x}(t)\ne n$; otherwise it is the sum of all possible terms obtained by linearly replacing each free occurrence of x with exactly one $s_i$, for $i=1,\dots , n$. Formally,

$$\begin{aligned} \partial _{x}{t\cdot \left[ s_1,\cdots ,s_n\right] }\mathrel {\mathop :\!=}{\left\{ \begin{array}{ll} \displaystyle \sum _{f\in \mathfrak S_{n}}t\left[ {s_{f(1)}}/{x_1},\dots ,{s_{f(n)}}/{x_n}\right] &{}\text {if}\; \mathrm {deg}_{x}(t)=n,\\ 0&{}\text {otherwise,} \end{array}\right. } \end{aligned}$$

(6)

where $\mathfrak 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}\left[ {s_{f(i)}}/{x_i}\right]$ denotes the term obtained from t by replacing the i-th free occurrence of x with $s_{f(i)}$. Then, we give a linear extension of the differential substitution: if $a\in \mathcal R[\![\varDelta ^{}]\!]$ and $\overline{a}\in \mathcal R[\![{{\varDelta ^{}}}^!]\!]$, we set: $\partial _{x}{a\cdot \overline{a}}= \sum _{t\in \varDelta ^{}, \overline{s}\in {{\varDelta ^{}}}^!}a_t\, \overline{a}_{\overline{s}}\partial _{x}{t\cdot \overline{s}}$.

The resource reduction $\rightarrow _{r}$ is then the smallest relation satisfying:

$$\begin{aligned} \left\langle \lambda x.t \right\rangle \,\left[ s_1,\cdots ,s_n\right] \rightarrow _{r}\partial _{x}{t\cdot \left[ s_1,\cdots ,s_n\right] } \end{aligned}$$

and moreover linear and compatible with the resource calculus constructors. Spelling out these two last conditions: for any $t,u\in \varDelta ^{}$, $\overline{s}\in {{\varDelta ^{}}}^!$, $a,b\in \mathcal R[\![\varDelta ^{}]\!]$, $\alpha \in \mathcal R\setminus \left\{ 0\right\}$, whenever $t\rightarrow _{r}a$, we have: (compatibility) $\lambda x.t\rightarrow _{r}\lambda x.a$, $\left\langle t \right\rangle \,\overline{s}\rightarrow _{r}\left\langle a \right\rangle \,\overline{s}$, $\left\langle u \right\rangle \,t\cdot \overline{s}\rightarrow _{r}\left\langle u \right\rangle \,a\cdot \overline{s}$, and (linearity) $\alpha t+b\rightarrow _{r}\alpha a+b$.

Proposition 3

([7]). Resource reduction $\rightarrow _{r}$ is confluent over the whole $\mathcal R[\![\varDelta ^{}]\!]$ and it is normalizing on the sums in $\mathcal R[\![\varDelta ^{}]\!]$ having a finite support.

Proposition 3 shows that any single resource term $t\in \varDelta ^{}$ has a unique normal form that we can denote as $\mathrm {NF}(t)$. What about possibly infinite linear combinations in $\mathcal R[\![\varDelta ^{}]\!]$? We would like to extend the normal form operator component-wise, as follows:

$$\begin{aligned} \mathrm {NF}(a)\mathrel {\mathop :\!=}\sum _{t\in \varDelta ^{}} a_t\cdot \mathrm {NF}(t) \end{aligned}$$

(7)

Example 4

The sum in Eq. (7) can be undefined for general $a\in \mathcal R[\![\varDelta ^{}]\!]$. Take $a=\lambda x.x + \left\langle \lambda x.x \right\rangle \,\left[ \lambda x.x\right] +\left\langle \lambda x.x \right\rangle \,\left[ \left\langle \lambda x.x \right\rangle \,\left[ \lambda x.x\right] \right] +\dots$: any single term of this sum reduces to $\lambda x.x$, hence $\mathrm {NF}(a)_{\lambda x.x}$ is infinite.

Another example is given by the Taylor expansion of the term in Eq. (3): one can check that the sum defining $\mathrm {NF}\bigl ({\left( \left( \mathbf \Theta \right) \lambda x.(x+y)\right) }^*\bigr )_{y}$ following Eq. (7) is infinite because, for all $n\in \mathbb N$, there is a resource term of the form $\left\langle t_n \right\rangle \,\left[ (\lambda x.x)^n,\lambda x.y\right] \in \mathcal {T}\left( \left( \mathbf \Theta \right) \lambda x.(x+y)\right)$, reducing to y. A closer inspection of the resulting coefficients (that we do not develop here) moreover shows that this infinite sum has unbounded partial sums in $\mathbb Q$, hence it diverges in general.

In fact, Corollary 39 ensures that if a is the Taylor expansion of a strongly normalizing non-deterministic $\lambda$-term then Eq. (7) is well-defined.

Example 5

Recall the expansions of Example 2 and consider ${(\left( \mathbf \varDelta \right) \lambda x.x)}^*=\sum _{n,k}\frac{1}{n!k!}\left\langle \lambda x.\left\langle x \right\rangle \,\left[ x^n\right] \right\rangle \,\left[ (\lambda x.x)^k\right]$. The resource reduction applied to a term of this sum gives zero except for $k=n+1$; in this latter case we get $(n+1)!\left\langle \lambda x.x \right\rangle \,\left[ (\lambda x.x)^n\right]$. Hence we have: ${(\left( \mathbf \varDelta \right) \lambda x.x)}^*\rightarrow _{r}\sum _{n}\frac{1}{n!}\left\langle \lambda x.x \right\rangle \,\left[ (\lambda x.x)^n\right]$, because the coefficient $(n+1)!$ generated by the reduction step is erased by the fraction $\frac{1}{k!}$ in the definition of Taylor expansion. Then, the term $\left\langle \lambda x.x \right\rangle \,\left[ (\lambda x.x)^n\right]$ reduces to zero but for $n=1$, in the latter case giving $\lambda x.x$. So we have: $\mathrm {NF}({(\left( \mathbf \varDelta \right) \lambda x.x)}^*)=\lambda x.x={(\mathrm {NF}(\left( \mathbf \varDelta \right) \lambda x.x))}^*$.

The commutation between computing normal forms and Taylor expansions has been proven in general for deterministic $\lambda$-terms [6]⁴ and witnesses the solidity of the definitions. The general case for $\varLambda _+^{}$ is still an open issue.

Example 6

Recall the notation of Eq. (4) from Example 2 expressing the sum ${\mathbf \Omega }^*$. All terms with $n_0\ne k+1$ reduce to zero in one step. For $n_0=k+1$, we have that a single term rewrites to $\sum _{f\in \mathfrak S_{k}}\left\langle \delta _{n_{f(1)}} \right\rangle \,\left[ \delta _{n_{f(2)}},\dots ,\delta _{n_{f(k)}}\right]$, which is a sum of terms still in $\mathcal {T}\left( \mathbf \Omega \right)$, but with smaller size w.r.t. the redex. Therefore, every term of ${\mathbf \Omega }^*$ eventually reduces to zero, after a reduction sequence whose length depends on the initial size of the term, and whose elements are sums with supports in $\mathcal {T}\left( \mathbf \Omega \right)$. This is in some sense the way Taylor expansion models the unbounded resource consumption of the loop $\mathbf \Omega \rightarrow _\beta \mathbf \Omega$ in $\lambda$-calculus.

We postpone the discussion of the reduction of ${\mathbf \Omega _3}^*$ until Remark 37.

2.3 Finiteness Structures Induced by Antireduction

Let us get back to Eq. (7), and consider it pointwise: for all $s\in \varDelta ^{}$ in normal form, we want to set $\mathrm {NF}(a)_s = \sum _{t\in \varDelta ^{}} a_t\cdot \mathrm {NF}(t)_s$. Notice that this series can be obtained as the inner product between a and the vector with : one can think of s as a test, that a passes whenever the sum converges.

There is one very simple condition that one can impose on a formal series to ensure its convergence: just assume there are finitely many non-zero terms. This seemingly dull remark is in fact the starting point of the definition of finiteness spaces, introduced by Ehrhard [3] and discussed in the Introduction. The basic construction is that of a finiteness structure:

Definition 7

([3]). Let A be a fixed set. A structure on A is any set of subsets $\mathfrak {A}\subseteq \mathfrak {P}\left( A\right)$. For all subsets a and $a'\subseteq A$, we write $a\perp a'$ whenever $a\cap a'$ is finite. For all structure $\mathfrak {A}\subseteq \mathfrak {P}\left( A\right)$, we define its dual ${\mathfrak {A}}^{\bot _{}}=\left\{ a\subseteq A;\;\forall a'\in \mathfrak {A},\ a\perp a'\right\}$. A finiteness structure on A is any such ${\mathfrak {A}}^{\bot _{}}$.

Notice that: $\mathfrak {A}\subseteq \mathfrak {A}^{\perp \perp }$, also $\mathfrak {A}\subseteq \mathfrak {A}'$ entails ${\mathfrak {A}'}^{\bot _{}}\subseteq {\mathfrak {A}}^{\bot _{}}$, hence ${\mathfrak {A}}^{\bot _{}}=\mathfrak {A}^{\perp \perp \perp }$.

Let , we obtain that $\left| a\right| \in {\mathfrak {C}_0}^{\bot _{}}$ iff Eq. (7) involves only pointwise finite sums. So, one is led to focus on support sets only, leaving out coefficients entirely. Henceforth, unless specified otherwise, we will thus stick to the case of $\mathcal R=\mathbb {B}$, and use set-theoretical notations only. This approach of ensuring the normalization of Taylor expansion via a finiteness structure was first used by Ehrhard [4] for a non-deterministic variant of System $\mathcal {F}$. Our paper strengthens Ehrhard’s result in several directions. In order to state them, we introduce a construction of finiteness structures on $\varDelta ^{}$ induced by anticones for the reduction order defined as follows:

Definition 8

For all $s,t\in \varDelta ^{}$, we write $t\ge s$ whenever there exists a reduction $t\rightarrow _{r}^* a$ with $s\in a$.

It should be clear that this defines a partial order relation (in particular we have antisymmetry because $\rightarrow _{r}$ terminates).

Definition 9

If $a\subseteq \varDelta ^{}$, is the cone of antireduction over a.⁵ For any structure $\mathfrak {T}\subseteq \mathfrak {P}\left( \varDelta ^{}\right)$, we write .

We can consider the elements of $\mathfrak {T}$ as tests, and say a set $a\subseteq \varDelta ^{}$ passes a test $a'\in \mathfrak {T}$ iff . The structure of sets that pass all tests is exactly ${\triangledown \left( \mathfrak {T}\right) }^{\bot _{}}$. Then Ehrhard’s result can be rephrased as follows:

Theorem 10

([4]). If $M\in \varLambda _+^{}$ is typable in System $\mathcal {F}$ then $\mathcal {T}\left( M\right) \in {\triangledown \left( \mathfrak {S}_{\text {sgl}}\right) }^{\bot _{}}$ where $\mathfrak {S}_{\text {sgl}}\mathrel {\mathop :\!=}\left\{ \left\{ s\right\} ;\;s\in \varDelta ^{}\right\}$.

Notice that, in contrast with the definition of $\mathfrak {C}_0$, $\mathfrak {S}_{\text {sgl}}$ is in fact not restricted to normal forms. Our paper extends this theorem in three directions: first, one can relax the condition that M is typed in System $\mathcal F$ and require only that M is strongly normalizable; second, the same result can be established for sets of “tests” larger (hence more demanding) than $\mathfrak {S}_{\text {sgl}}$; third, the implication can be reversed for a suitable set of tests $\mathfrak {T}$, i.e. M is strongly normalizable iff $\mathcal {T}\left( M\right) \in {\triangledown \left( \mathfrak {T}\right) }^{\bot _{}}$ (and we do need $\mathfrak {T}$ to provide more tests than just singletons: see Remark 37). In order to state our results precisely, we need to introduce a few more notions.

Definition 11

We say that a resource term s is linear whenever each bag appearing in s has cardinality 1. A set a of resource terms is said linear whenever all its elements are linear. We say a is bounded whenever there exists a number $n\in \mathbf N$ bounding the cardinality of all bags in all terms in a. We then write

$$\begin{aligned} \mathfrak {L}\mathrel {\mathop :\!=}\left\{ a\subseteq \varDelta ^{};\;a \;\text {linear}\right\} \quad \text {and}\quad \mathfrak {B}\mathrel {\mathop :\!=}\left\{ a\subseteq \varDelta ^{};\;a\; \text {bounded}\right\} . \end{aligned}$$

We also denote as $\ell \left( M\right)$ the subset of the linear resource terms in $\mathcal {T}\left( M\right)$. Notice that $\ell \left( M\right)$ is always non-empty and can be directly defined by replacing the definition of $\mathcal {T}\left( \left( M\right) N\right)$ in Table 1b with: $\ell \left( \left( M\right) N\right) \mathrel {\mathop :\!=}\left\{ \left\langle s \right\rangle \,\left[ t\right] ;\;s\in \ell \left( M\right) , t\in \ell \left( N\right) \right\}$.

Observe that $\mathfrak {S}_{\text {sgl}},\mathfrak {L}\subseteq \mathfrak {B}$.

Table 2. The intersection type assignment system $\mathcal D_+$ for $\varLambda _+^{}$

We can sum up our results Corollary 30 and Theorem 36 as follows:

Theorem 12

Let $M\in \varLambda _+^{}$:

• If M is strongly normalizing, then $\mathcal {T}\left( M\right) \in {\triangledown \left( \mathfrak {T}\right) }^{\bot _{}}$ as soon as $\mathfrak {T}\subseteq \mathfrak {B}$.

• If $\mathcal {T}\left( M\right) \in {\triangledown \left( \mathfrak {T}\right) }^{\bot _{}}$ with $\mathfrak {L}\subseteq \mathfrak {T}$, then M is strongly normalizing.

3 Strongly Normalizing Terms Are $\mathcal D_+$ Typable

Intersection types are well known, as well as their relation with normalizability. We refer to [2] for the original system with subtyping characterizing the set of strongly normalizing $\lambda$-terms, and [1, 8] for simpler systems. However, as far as we know, the literature about intersection types for non-deterministic $\lambda$-calculi is less well established and in fact we could find no previous characterization of strong normalization in a non-deterministic setting. Hence, we give in Table 2 a variant of Krivine’s system $\mathcal D$ [8], characterizing the set of strongly normalizing terms in $\varLambda _+^{}$. In this section, we only prove that strongly normalizing terms are typable (Theorem 14): the reverse implication follows from the rest of the paper (see Fig. 1). These techniques are standard.

Remark 13

Krivine’s original System $\mathcal D$ does not have $\left( \preceq \right)$ and $\left( +\right)$, but it has the two usual elimination rules for intersection (here derivable). The rule $\left( +\right)$ is necessary to account for non-determinism, however adding just $\left( +\right)$ to System $\mathcal D$ is misbehaving. We can find terms M and N, and a context $\varGamma$ such that $\left( M\right) N$ is typable in System $\mathcal D$ with $\left( +\right)$ under the context $\varGamma$ but M is not: take $\varGamma =x:A\rightarrow B\cap B',y:A\rightarrow B\cap B'',z:A$, observe that $\left( x+y\right) z=\left( x\right) z+\left( y\right) z$, and thus $\varGamma \vdash \left( x+y\right) z:B$ but $x+y$ is not typable in $\varGamma$. This is the reason why we introduce subtyping.

Theorem 14

For all $M\in \varLambda _+^{}$, if M is strongly normalizable, then there exists a derivable judgement $\varGamma \vdash M:A$ in system ${\mathcal D_+}$.

Proof

(Sketch). For M a strongly normalizable term, let $\mathbf l\left( M\right)$ be the maximum length of a reduction from M, and $\mathbf s\left( M\right)$ the number of symbols occurring in M. By well-founded induction on the pair $(\mathbf l\left( M\right) ,\mathbf s\left( M\right) )$ we prove that there exists $n_M\in \mathbf N$ such that for all type B and all $n\ge n_M$, there is a context $\varGamma$ and a sequence $(A_1,\cdots ,A_n)$ of types such that $\varGamma \vdash M:A_1\rightarrow \cdots \rightarrow A_n\rightarrow B$.

The proof splits depending on the structure of M. In case $M=M_1+M_2$, we apply the induction hypothesis on both $M_1$ and $M_2$ and conclude by rule $\left( \preceq \right)$ and a contravariance property: $\varGamma \vdash M:A$ whenever $\varGamma '\vdash M:A$ and $\varGamma \preceq \varGamma '$.

In case of head-redexes, i.e. $M=\left( \left( \mathord {\lambda x.N}\right) P\right) M_1\cdots M_q$, we apply the induction hypothesis on $M'=\left( {N}\left[ {P}/{x}\right] \right) M_1\cdots M_q$ and on P. Then, we conclude via a subject expansion lemma stating that: $\varGamma \vdash \left( \mathord {\lambda x.N}\right) P\,M_1\cdots M_n:A$, whenever $\varGamma \vdash \left( {N}\left[ {P}/{x}\right] \right) M_1\cdots M_n:A$ and there exists B such that $\varGamma \vdash P:B$.

The other cases are similar to the first one.    $\square$

4 $\mathcal D_+$ Typable Terms Are Finitary

This section proves Corollary 30, giving sufficient conditions (to be dispersed, hereditary and expandable, see resp. Definitions 23, 26 and 27) over a structure $\mathfrak {T}$ in order to have all cones for $a\in \mathfrak {T}$ dual to the Taylor expansion of any strongly normalizing non-deterministic $\lambda$-term.

It is easy to check that these conditions are satisfied by the structures $\mathfrak {B}$ of bounded sets and $\mathfrak {L}$ of sets of linear terms (Definition 11). Moreover, as an immediate corollary one gets also that any subset $\mathfrak {T}\subseteq \mathfrak {B}$ is also such that $\mathcal {T}\left( M\right) \in {\triangledown \left( \mathfrak {T}\right) }^{\bot _{}}$ for any strongly normalizable term $M\in \varLambda _+^{}$, so getting the first Item of Theorem 12.

Thanks to previous Theorem 14 we can prove Corollary 30 by a realizability technique on the intersection type system $\mathcal D_+$. For a fixed structure $\mathfrak {S}$, we associate with any type A a realizer $\left\| A\right\| _{\mathfrak {S}}$ (Definition 18). In the case $\mathfrak {S}$ is adapted (Definition 17), we can prove that $\left\| A\right\| _{\mathfrak {S}}$ contains the Taylor expansion of any term of type A and that it is contained in $\mathfrak {S}$ (Theorem 21). These definitions and theorem are adapted from Krivine’s proof for System $\mathcal D$ [8].

The crucial point is then to find structures $\mathfrak {S}$ which are adapted: here is our contribution. The structures that we study have the shape ${\triangledown \left( \mathfrak {T}\right) }^{\bot _{}}$, so that we are speaking of the interaction with cones of anti-reducts of tests in a structure $\mathfrak {T}$. Intuitively, $\mathfrak {T}$ is a set of tests that can be passed by any term typable in System $\mathcal D_+$ (hence by any strongly normalizing term). We prove (Lemma 29) that for a structure $\mathfrak {T}$, being dispersed, hereditary and expandable is sufficient to guarantee that the dual structure ${\triangledown \left( \mathfrak {T}\right) }^{\bot _{}}$ is adapted, then achieving Corollary 30.

Definition 15

(Functional). Given two structures $\mathfrak {S},\mathfrak {S}'\subseteq \mathfrak {P}\left( \varDelta ^{}\right)$, we define the structure $\mathfrak {S}\rightarrow \mathfrak {S}'\mathrel {\mathop :\!=}\left\{ f\subseteq \varDelta ^{};\;\forall a\in \mathfrak {S}, \left\langle f \right\rangle \,{a}^!\in \mathfrak {S}'\right\}$.

Definition 16

(Saturation). Let $\mathfrak {S}, \mathfrak {S}'\subseteq \mathfrak {P}\left( \varDelta ^{}\right)$. We say $\mathfrak {S}'$ is $\mathfrak {S}$ -saturated if $\forall e,f_0,\dots ,f_n\in \mathfrak {S}$, $\left\langle \partial _{x}{e\cdot {f_0}^!} \right\rangle \,{f_1}^!\dots {f_n}^!\in \mathfrak {S}'$ implies $\left\langle \lambda x.e \right\rangle \,{f_0}^!\,{f_1}^!\dots {f_n}^!\in \mathfrak {S}'$.

Definition 17

(Adaptedness). For all $\mathfrak {S}\subseteq \mathfrak {P}\left( \varDelta ^{}\right)$ we set ${\mathfrak {S}}_h \mathrel {\mathop :\!=}\left\{ \left\{ x\right\} ;\;x\in \mathcal {V}\right\} \mathbin \cup \left\{ \left\langle x \right\rangle \,{a_1}^!\cdots {a_n}^!;\;x\in \mathcal {V},\ n>0 \text { and } \forall i,\ a_i\in \mathfrak {S}\right\}$ and say $\mathfrak {S}$ is adapted if:

• 1. $\mathfrak {S}$ is $\mathfrak {S}$-saturated;

• 2. ${\mathfrak {S}}_h\subset (\mathfrak {S}\rightarrow {\mathfrak {S}}_h)\subset ({\mathfrak {S}}_h\rightarrow \mathfrak {S})\subset \mathfrak {S}$;

• 3. $\mathfrak {S}$ is closed under finite unions: $\forall b,b'\in \mathfrak {S}$, $b\cup b'\in \mathfrak {S}$.

Definition 18

(Realizers). Let $\mathfrak {S}\subseteq \mathfrak {P}\left( \varDelta ^{}\right)$. To each type A of System $\mathcal D_+$, we associate a structure $\left\| A\right\| _{\mathfrak {S}}$ defined inductively (X being a propositional variable):

$$\begin{aligned} \left\| X\right\| _{\mathfrak {S}}&\mathrel {\mathop :\!=}\mathfrak {S},&\left\| A\rightarrow B\right\| _{\mathfrak {S}}&\mathrel {\mathop :\!=}\left\| A\right\| _{\mathfrak {S}}\rightarrow \left\| B\right\| _{\mathfrak {S}},&\left\| A\cap B\right\| _{\mathfrak {S}}&\mathrel {\mathop :\!=}\left\| A\right\| _{\mathfrak {S}}\cap \left\| B\right\| _{\mathfrak {S}}. \end{aligned}$$

Lemma 19

Let $\mathfrak {S}$ be an adapted structure, then for every type A, $\left\| A\right\| _{\mathfrak {S}}$ is $\mathfrak {S}$-saturated, closed under finite unions and ${\mathfrak {S}}_h\subseteq \left\| A\right\| _{\mathfrak {S}}\subseteq \mathfrak {S}$.

Lemma 20

(Adequacy). If $\mathfrak {S}\subseteq \mathfrak {P}\left( \varDelta ^{}\right)$ is adapted, $x_1:A_1,\cdots ,x_n:A_n\vdash M:B$ and for all $1\le i\le n$, $a_i\in \left\| A_i\right\| _{\mathfrak {S}}$, then $\partial _{x_1,\cdots ,x_n}{\mathcal {T}\left( M\right) \cdot {a_1}^!,\cdots ,{a_n}^!}\in \left\| B\right\| _{\mathfrak {S}}$.

Proof

(Sketch). By structural induction on the derivation of $x_1:A_1,\cdots ,x_n:A_n\vdash M:B$. The cases where the last rule is $\left( \rightarrow _i\right)$ or $\left( +\right)$ use respectively the facts that the realizers are saturated and closed by finite unions. The case where the last rule is $\left( \preceq \right)$ is an immediate consequence of the induction hypothesis and of a lemma stating that $A\preceq B$ implies $\left\| A\right\| _{\mathfrak {S}}\subseteq \left\| B\right\| _{\mathfrak {S}}$.    $\square$

Theorem 21

If $\mathfrak {S}\subseteq \mathfrak {P}\left( \varDelta ^{}\right)$ is adapted and M is typable in System $\mathcal D_+$, then $\mathcal {T}\left( M\right) \in \mathfrak {S}$.

Proof

Let $\varGamma \vdash M:B$. For any x : A in $\varGamma$, $\{x\}\in {\mathfrak {S}}_h\subset \left\| A\right\| _{\mathfrak {S}}$ by Lemma 19 and Definition 17. Hence, $\mathcal {T}\left( M\right) =\partial _{x_1,\cdots ,x_n}{\mathcal {T}\left( M\right) \cdot {\left\{ x_1\right\} }^!,\cdots ,{\left\{ x_n\right\} }^!}\in \left\| B\right\| _{\mathfrak {S}}$ by Lemma 20. Again by Lemma 19, $\left\| B\right\| _{\mathfrak {S}}\subseteq \mathfrak {S}$, so $\mathcal {T}\left( M\right) \in \mathfrak {S}$.    $\square$

Now we look for conditions to ensure that a structure $\mathfrak {S}$ is adapted. These conditions (Definitions 23, 26 and 27) are quite technical but they are easy to check, in particular the structures $\mathfrak {B}$ and $\mathfrak {L}$ enjoy them (Remark 28).

Definition 22

The height $\mathbf h\left( s\right)$ of a resource term s is defined inductively: $\mathbf h\left( x\right) \mathrel {\mathop :\!=}1$, $\mathbf h\left( \lambda x.s\right) \mathrel {\mathop :\!=}1+\mathbf h\left( s\right)$ and $\mathbf h\left( \left\langle s_0 \right\rangle \,\left[ s_1,\cdots ,s_n\right] \right) \mathrel {\mathop :\!=}1+\max _i(\mathbf h\left( s_i\right) )$.

Definition 23

(Dispersed). A set $a\subseteq \varDelta ^{}$ is dispersed whenever for all $n\in \mathbf N$, and all finite set V of variables, the set $\left\{ s\in a;\;\mathbf h\left( s\right) \le n\text { and }\mathsf {fv}\left( s\right) \subseteq V\right\}$ is finite. A structure $\mathfrak {S}$ is dispersed whenever $\forall a\in \mathfrak {S}$, a is dispersed.

Definition 24

Let $s\in \varDelta ^{}$ and $x\not \in \mathsf {fv}\left( s\right)$. We define immediate subterm projections $\pi ^{}_{x}s\in \mathfrak {P}\left( \varDelta ^{}\right)$, $\pi ^{}_{0}s\in \mathfrak {P}\left( \varDelta ^{}\right)$, $\overline{\pi }^{}_{1}s\in \mathfrak {P}\left( {\varDelta ^{}}^!\right)$ and $\pi ^{}_{1}s\in \mathfrak {P}\left( \varDelta ^{}\right)$ as follows:

• if $s=\lambda x.t$ then $\pi ^{}_{x}s=\left\{ t\right\}$; otherwise $\pi ^{}_{x}s=\emptyset$;

• if $s=\left\langle t \right\rangle \,\overline{u}$ then $\pi ^{}_{0}s=\left\{ t\right\}$, $\overline{\pi }^{}_{1}s=\left\{ \overline{u}\right\}$, $\pi ^{}_{1}s=\left| \overline{u}\right|$; otherwise $\pi ^{}_{0}s=\overline{\pi }^{}_{1}s=\pi ^{}_{1}s=\emptyset$.

Observe that up to $\alpha$-conversion and the hypothesis $x\not \in \mathsf {fv}\left( s\right)$, the abstraction case is exhaustive. These functions obviously extend to sets of terms, up to some care about free variables. If $V\subseteq \mathcal {V}$ is a set of variables, we write $\varDelta ^{V}$ for the set of resource $\lambda$-terms with free variables in V.

Definition 25

For all $V\subseteq \mathcal {V}$ and $a\subseteq \varDelta ^{V}$, let

$$\begin{aligned} \pi ^{}_{0}a&\mathrel {\mathop :\!=}\bigcup _{s\in a}\pi ^{}_{0}s\subseteq \varDelta ^{V},&\overline{\pi }^{}_{1}a&\mathrel {\mathop :\!=}\bigcup _{s\in a}\overline{\pi }^{}_{1}s\subseteq {\varDelta ^{V}}^!,&\pi ^{}_{1}a&\mathrel {\mathop :\!=}\bigcup _{s\in a}\pi ^{}_{1}s\subseteq \varDelta ^{V}, \end{aligned}$$

and if moreover $x\not \in V$, then let $\pi ^{}_{x}a \mathrel {\mathop :\!=}\bigcup _{s\in a}\pi ^{}_{x}s\subseteq \varDelta ^{V\cup \left\{ x\right\} }$.

Definition 26

(Hereditary). A structure $\mathfrak {S}\subseteq \mathfrak {P}\left( \varDelta ^{}\right)$ is said to be hereditary if, $\mathfrak {S}$ is downwards closed, and for all $a\in \mathfrak {S}$, $\pi ^{}_{0}a\in \mathfrak {S}$, $\pi ^{}_{1}a\in \mathfrak {S}$ and for all $x\in \mathcal {V}\setminus \mathsf {fv}\left( a\right)$, $\pi ^{}_{x}a\in \mathfrak {S}$.

Definition 27

(Expandable). A structure $\mathfrak {S}\subseteq \mathfrak {P}\left( \varDelta ^{}\right)$ is said to be expandable if, for all $x\in \mathcal {V}$ and all $a\in \mathfrak {S}$, we have $\left\{ \left\langle s \right\rangle \,\left[ x\right] ;\;s\in a\right\} \in \mathfrak {S}$.

Remark 28

The structures $\mathfrak {S}_{\text {sgl}}$ (Theorem 10) and $\mathfrak {L}$, $\mathfrak {B}$ (Definition 11) are dispersed and expandable. The last two are also hereditary, while $\mathfrak {S}_{\text {sgl}}$ is not.

Lemma 29

For any structure $\mathfrak {T}$ which is dispersed, hereditary and expandable, we have that ${\triangledown \left( \mathfrak {T}\right) }^{\bot _{}}$ is adapted.

Proof

(Sketch). One has to prove the three conditions of Definition 17. Heredity and dispersion are used to obtain saturation (Condition 1). The inclusions of Condition 2 need all hypotheses and an auxiliary lemma proving that ${{\triangledown \left( \mathfrak {T}\right) }^{\bot _{}}}_h\subseteq {\triangledown \left( \mathfrak {T}\right) }^{\bot _{}}$, for which dispersion is crucial. Finally, the closure under finite unions (Condition 3) is satisfied by all finiteness structures.    $\square$

Corollary 30

Let $\mathfrak {T}\subseteq \mathfrak {P}\left( \varDelta ^{}\right)$ be dispersed, hereditary and expandable. For every strongly normalizable term M, we have $\mathcal {T}\left( M\right) \in {\triangledown \left( \mathfrak {T}\right) }^{\bot _{}}$. Hence, this holds for $\mathfrak {T}\in \left\{ \mathfrak {L}, \mathfrak {B}\right\}$ and for any of their subsets, such as $\mathfrak {S}_{\text {sgl}}\subset \mathfrak {B}$.

Proof

The general statement follows from Theorems 14  and 21 and Lemma 29. Remark 28 implies $\mathcal {T}\left( M\right) \in {\triangledown \left( \mathfrak {T}\right) }^{\bot _{}}$ for $\mathfrak {T}\in \left\{ \mathfrak {B}, \mathfrak {L}\right\}$. The rest of the statement follows because, for any structures $\mathfrak {S},\mathfrak {S}'$, $\mathfrak {S}\subseteq \mathfrak {S}'$ implies ${\mathfrak {S}'}^{\bot _{}}\subseteq {\mathfrak {S}}^{\bot _{}}$.   $\square$

5 Finitary Terms Are Strongly Normalizing

In this section we prove Theorem 36, giving a sufficient condition for a structure $\mathfrak {T}$ to be able to test strong normalization. The condition is that $\mathfrak {T}$ includes at least $\mathfrak {L}$, i.e. the set of all sets of linear terms⁶.

The proof is by contraposition, suppose that M is divergent, then $\mathcal {T}\left( M\right)$ is not dual to some cone , with $a\in \mathfrak {L}$. The proof enlightens two kinds of divergence in $\lambda$-calculus: the one generated by looping terms: $\mathbf \Omega \rightarrow _\beta \mathbf \Omega \rightarrow _\beta \dots$ and the other generated by infinite reduction sequences $(M_i)_{i\in \mathbf N}$ with an infinite number of different terms: $\mathbf {\Omega _3}\rightarrow _\beta \left( \mathbf {\Omega _3}\right) \mathbf {\varDelta _3}\rightarrow _\beta \left( \left( \mathbf {\Omega _3}\right) \mathbf {\varDelta _3}\right) \mathbf {\varDelta _3}\rightarrow _\beta \dots$ (see Example 1).

In the first case, the cone of the linear expansion (Definition 11) of the looping term $\mathbf \Omega$ suffices to show up the divergence, since is infinite. Indeed the Taylor expansion of a looping term, say $\mathcal {T}\left( \mathbf \Omega \right)$, is a kind of “contractible space”, where any resource term reduces to a smaller term within the same Taylor expansion or vanishes (see Example 6). In particular, there are unboundedly large resource terms reducing to the linear expansion $\ell (\mathbf \Omega )$.

In the case of an infinite reduction sequence of different terms, one should take, basically, the cone of all linear expansions of the terms occurring in the sequence: the linear expansion of a single term (or of a finite set of terms) might not suffice to test this kind of divergence. For example, is finite, while is infinite, so $\mathcal {T}\left( \mathbf {\Omega _3}\right) \!\notin \!{\triangledown \left( \mathfrak {L}\right) }^{\bot _{}}$.

In the presence of the non-deterministic sum $+$, we have a third kind of divergence, which is given by infinite reduction sequences of terms $(M_i)_{i\in \mathbf N}$ which are pairwise different but whose Taylor expansion support repeats infinitely many times: consider, e.g., the reducts of $\left( \mathbf \Theta \right) (\lambda x.x+y)$. We prove that this kind of divergence is much more similar to a loop rather than to a sequence of different $\lambda$-terms. In particular, there is a single linear resource term (depending on the reduction sequence) whose cone is able to show up the divergence. Indeed, most of the effort in the proof of Theorem 36 is devoted to deal with this kind of “looping Taylor expansion”. Namely, Definition 31 gives a notion of non-deterministic reduction $\rightharpoonup _{}$ allowing Lemma 35, which is the key statement used in the proof of Theorem 36 for dealing with both the divergence of looping terms (like $\mathbf \Omega$) and that of looping Taylor expansions (like $\left( \mathbf \Theta \right) (\mathord {\lambda x.x+y})$).

We introduce a reduction rule $\rightharpoonup _{}$ on $\varLambda _+^{}$ which corresponds to one step of $\beta$-reduction and a potential loss of some addenda in a term. For that, we need an order $\trianglerighteq$ on $\varLambda _+^{}$ expressing this loss. For instance, $\left( \mathbf \Theta \right) (\mathord {\lambda x.x+y})+y\trianglerighteq \left( \mathbf \Theta \right) \mathord {\lambda x.x}$, thus $\left( \mathbf \Theta \right) (\mathord {\lambda x.x+y})\rightharpoonup _{}^*\left( \mathbf \Theta \right) \mathord {\lambda x.x}$, and similarly, $\left( \mathbf \Theta \right) (\mathord {\lambda x.x+y})\rightharpoonup _{}^*y$.

Definition 31

(Partial reduction). We write $M\rightharpoonup _{}N$ if there exists P such that $M\rightarrow _\beta P$ and $P\trianglerighteq N$, where the partial order $\trianglelefteq$ over $\varLambda _+$ is defined as the least order such that $M\trianglelefteq M+N$; $N\trianglelefteq M+N$ and if $M\trianglelefteq N$ then: $M+P\trianglelefteq N+P$, $\mathord {\lambda x.M}\trianglelefteq \mathord {\lambda x.N}$, $\left( M\right) P\trianglelefteq \left( N\right) P$, and $\left( P\right) M\trianglelefteq \left( P\right) N$.

A reduction $M\rightharpoonup _{}N$ is at top level if $M=\left( \mathord {\lambda x.M'}\right) M''\rightarrow M'[M''/x]\trianglerighteq N$.

Write $s>t$ whenever $s\ge t$ (Definition 8) and $s\not =t$: this is a strict partial order relation.

Lemma 32

If $M\rightharpoonup _{}N$ and $t\in \mathcal {T}\left( N\right)$, then there exists $s\in \mathcal {T}\left( M\right)$ such that $s\ge t$. If moreover, $M\rightharpoonup _{}N$ is at top level, then $s>t$.

Lemma 33

Let $M\rightharpoonup _{}N$ and $u\in \varDelta ^{}$. If is infinite, then is also infinite.

Definition 34

The height $\mathbf h\left( M\right)$ of a term $M\in \varLambda _+^{}$ is defined inductively as follows: $\mathbf h\left( x\right) \mathrel {\mathop :\!=}1$, $\mathbf h\left( \mathord {\lambda x.M}\right) \mathrel {\mathop :\!=}1+\mathbf h\left( M\right)$, $\mathbf h\left( \left( M\right) N\right) \mathrel {\mathop :\!=}1+\max (\mathbf h\left( M\right) ,\mathbf h\left( N\right) )$ and $\mathbf h\left( {M}+{N}\right) \mathrel {\mathop :\!=}\max (\mathbf h\left( M\right) ,\mathbf h\left( N\right) )$.

Lemma 35

Let $(M_i)_{i\in \mathbf N}$ be a sequence. If $\forall i\in \mathbf N$, $M_i\rightharpoonup _{}M_{i+1}$ and $(\mathbf h\left( M_i\right) )_{i\in \mathbf N}$ is bounded, then there exists a linear term t such that is infinite.

Proof

(Sketch). First, it is sufficient to address the case of a sequence $(S_i)_{i\in \mathbf N}$ of simple terms (i.e. without $+$ as the top-level constructor) such that $S_i\rightharpoonup _{}S_{i+1}$ for all $i\in \mathbf N$ and $(\mathbf h\left( S_i\right) )_{i\in \mathbf N}$ is bounded. Besides, by Lemma 33, it is sufficient to have infinite for some $i_0\in \mathbf N$.

Then, by induction on $h=\max \left\{ \mathbf h\left( S_i\right) ;\;i\in \mathbf N\right\}$, we show that there exists $i_0\in \mathbf N$ and a sequence $(s_j)_{j\in \mathbf N}\in \mathcal {T}\left( S_{i_0}\right) ^\mathbf N$ such that $s_0$ is linear and, for all $j\in \mathbf N$, $s_{j+1}>s_j$. Since $>$ is a strict order relation, this implies that the set is infinite.

First assume that there are infinitely many top level reductions. Observe that, since $\mathbf h\left( S_i\right) \le h$ and $\mathsf {fv}\left( S_i\right) \subseteq \mathsf {fv}\left( S_0\right)$ for all i, the set $\left\{ \mathcal {T}\left( S_i\right) ;\;i\in \mathbf N\right\}$ is finite. Hence there exists an index $i_0\in \mathbf N$ such that $\left\{ i\in \mathbf N;\;\mathcal {T}\left( S_i\right) =\mathcal {T}\left( S_{i_0}\right) \right\}$ is infinite. As there are infinitely many top level reductions, there are $i_1$ and $i_2$ such that $i_0<i_1<i_2$, the reduction $i_1$ is at top level and $\mathcal {T}\left( S_{i_2}\right) =\mathcal {T}\left( S_{i_0}\right)$. We inductively define the required sequence by choosing arbitrary $s_0\in \ell \left( S_{i_0}\right) \subseteq \mathcal {T}\left( S_{i_0}\right)$, and by iterating Lemma 32: for $s_j\in \mathcal {T}\left( S_{i_0}\right) =\mathcal {T}\left( S_{i_2}\right)$, we obtain $s_{j+1}\in \mathcal {T}\left( S_{i_0}\right)$ with $s_{j+1} >s_j$ since the reduction $i_1$ is at top level.

Now assume that there are only finitely many top level reductions. Let $i_1$ be such that no reduction $S_i\rightharpoonup _{}S_{i+1}$ with $i\ge i_1$ is at top level. Either for all $i\ge i_1$, $S_i=\mathord {\lambda x.M'_i}$ with $M'_i\rightharpoonup _{}M'_{i+1}$, and we conclude by applying the induction hypothesis to the sequence $(M'_{i+i_1})_{i\in \mathbf N}$; or for all $i\ge i_1$, $S_i=\left( M'_i\right) N'_i$ so that $(M'_i)_{i\ge i_1}$ and $(N'_i)_{i\ge i_1}$ are sequences of terms, at least one of them involving infinitely many partial reductions. In this case, assume for instance that we can extract from $(M'_i)_{i\ge i_1}$ an infinite subsequence $(M'_{\phi (i)})_{i\in \mathbf N}$ of partial reductions. It provides $i'_0$ and a sequence $(s'_j)\in \mathcal T(M'_{\phi (i'_0)})^N$ with $s'_0$ linear and, $s'_{j+1}>s'_j$. Fix $t\in \ell (N'_{\phi (i'_0)})$ arbitrarily. So we set $i_0=\phi (i'_0)$ and $s_j=\left\langle s'_j \right\rangle \,\left[ t\right]$ for all $j\in \mathbf N$.   $\square$

Theorem 36

Let $\mathfrak {T}$ be a structure such that $\mathfrak {L}\subseteq \mathfrak {T}$. If $\mathcal {T}\left( M\right) \in {\triangledown \left( \mathfrak {T}\right) }^{\bot _{}}$ then M is strongly normalizable. In particular, this holds for $\mathfrak {T}\in \left\{ \mathfrak {L}, \mathfrak {B}\right\}$.

Proof

Assume that $(M_i)_{i\in \mathbf N}$ is such that $M=M_0$ and for all i, $M_i\rightarrow _\beta M_{i+1}$. We prove that $\mathcal {T}\left( M\right) \not \in {\triangledown \left( \mathfrak {T}\right) }^{\bot _{}}$ by exhibiting $a\in \mathfrak {T}$ such that .

If $(\mathbf h\left( M_i\right) )_{i\in \mathbf N}$ is bounded, then fix $a=\left\{ t\right\}$ with t given by Lemma 35.

Otherwise, $\forall i\in \mathbf N$, fix $t_i\in \ell \left( M_i\right)$ such that $\mathbf h\left( t_i\right) =\mathbf h\left( M_i\right)$. Lemma 32 implies that there is $s_i\in \mathcal {T}\left( M\right)$ such that $s_i\ge t_i$. Denote by $\mathbf s\left( s\right)$ the number of symbols occurring in s. Since there is no duplication in reduction $\rightarrow _{r}$ it should be clear that if $s\ge t$ then $\mathbf s\left( s\right) \ge \mathbf s\left( t\right)$. Besides, $\mathbf s\left( s\right) \ge \mathbf h\left( s\right)$. Therefore, since $\left\{ \mathbf h\left( M_i\right) ;\;i\in \mathbf N\right\}$ is unbounded, $\left\{ \mathbf h\left( t_i\right) ;\;i\in \mathbf N\right\}$, $\left\{ \mathbf s\left( t_i\right) ;\;i\in \mathbf N\right\}$ and $\left\{ \mathbf s\left( s_i\right) ;\;i\in \mathbf N\right\}$ are unbounded. Fix $a=\bigcup _{i\in \mathbf N}\ell \left( M_i\right) \in \mathfrak {T}$, we have proved that is infinite.    $\square$

Notice that the structure $\mathfrak {S}_{\text {sgl}}$ of singletons used in [4] does not enjoy the hypothesis of Theorem 36 ($\mathfrak {L}\not \subset \mathfrak {S}_{\text {sgl}}$). In fact:

Remark 37

We prove that $\mathcal {T}\left( \mathbf {\Omega _3}\right) \in {\triangledown \left( \mathfrak {S}_{\text {sgl}}\right) }^{\bot _{}}$, although $\mathbf {\Omega _3}$ is not normalizing. Recall from Example 2, that the support of the Taylor expansion of $\mathbf {\Omega _3}$ is made of terms of the form $\left\langle \delta _{n_0,m_0} \right\rangle \,\left[ \delta _{n_1,m_1},\dots ,\delta _{n_k,m_k}\right]$ (for $k,n_i,m_i\in \mathbf N$). Write $\varDelta _h=\left\{ \left\langle \delta _{-,-} \right\rangle \,\left[ \dots \delta _{-,-}\dots \right] \cdots \left[ \dots \delta _{-,-}\dots \right] \;\text { with } \; h \; \text {bags}\right\}$: in particular $\mathcal {T}\left( \mathbf {\Omega _3}\right) =\varDelta _1$. One can easily check that if $s\in \varDelta _h$ and $s\ge s'$, then $s'\in \varDelta _{h'}$ with $h\le h'$. A careful inspection of such reductions shows that they are moreover reversible: for all $s'\in \varDelta _{h'}$ and all $h\le h'$ there is exactly one $s\in \varDelta _h$ such that $s\ge s'$. It follows that $\varDelta _1\cap \uparrow s$ is either empty or a singleton. Therefore $\mathcal {T}\left( \mathbf {\Omega _3}\right) \in {\triangledown \left( \mathfrak {S}_{\text {sgl}}\right) }^{\bot _{}}$.

6 Conclusion

We achieved all implications of Fig. 1, but the rightmost one, concerning the finiteness of the coefficients in the normal form of the Taylor expansion of a strongly normalizing $\lambda$-term (recall Eq. (2) in the Introduction).

Thanks to the definition of cones (Definition 9) we immediately have the following lemma, which is the last step to Corollary 39.

Lemma 38

Let $\mathfrak {T}$ be a structure. If $\mathcal {T}\left( M\right) \in {\triangledown \left( \mathfrak {T}\right) }^{\bot _{}}$, then $\forall t\in \bigcup \mathfrak {T}$, $\mathrm {NF}(\mathcal {T}\left( M\right) )_t$ is finite.

Applying Corollary 30 and Lemma 38 to a structure like $\mathfrak {B}$ or $\mathfrak {S}_{\text {sgl}}$, we get:

Corollary 39

Given a non-deterministic $\lambda$-term M, if M is strongly normalizable, then $\mathrm {NF}(\mathcal {T}\left( M\right) )_t$ is finite for all $t\in \varDelta ^{}$.