Normalizing the Taylor expansion of non-deterministic {\lambda}-terms, via parallel reduction of resource vectors

TL;DR

This paper extends the known commutation of Taylor expansion and normalization from pure lambda calculus to algebraic lambda calculus with non-determinism, introducing resource vectors and a generalized notion of B"ohm trees.

Contribution

It introduces a reduction on resource vectors and generalizes B"ohm trees to handle non-deterministic algebraic lambda calculus, ensuring normalization commutes with Taylor expansion.

Findings

Taylor expansion and normalization commute for a broad class of algebraic lambda terms.

Resource vectors effectively model the dynamics of beta-reduction in non-deterministic settings.

A new generalized notion of B"ohm trees is proposed for algebraic lambda calculus.

Abstract

It has been known since Ehrhard and Regnier's seminal work on the Taylor expansion of $\lambda$-terms that this operation commutes with normalization: the expansion of a $\lambda$-term is always normalizable and its normal form is the expansion of the B\"ohm tree of the term. We generalize this result to the non-uniform setting of the algebraic $\lambda$-calculus, i.e. $\lambda$-calculus extended with linear combinations of terms. This requires us to tackle two difficulties: foremost is the fact that Ehrhard and Regnier's techniques rely heavily on the uniform, deterministic nature of the ordinary $\lambda$-calculus, and thus cannot be adapted; second is the absence of any satisfactory generic extension of the notion of B\"ohm tree in presence of quantitative non-determinism, which is reflected by the fact that the Taylor expansion of an algebraic $\lambda$-term is not always normalizable. Our solution is to provide a fine grained study of the dynamics of $\beta$-reduction under Taylor expansion, by introducing a notion of reduction on resource vectors, i.e. infinite linear combinations of resource $\lambda$-terms. The latter form the multilinear fragment of the differential $\lambda$-calculus, and resource vectors are the target of the Taylor expansion of $\lambda$-terms. We show the reduction of resource vectors contains the image of any $\beta$-reduction step, from which we deduce that Taylor expansion and normalization commute on the nose. We moreover identify a class of algebraic $\lambda$-terms, encompassing both normalizable algebraic $\lambda$-terms and arbitrary ordinary $\lambda$-terms: the expansion of these is always normalizable, which guides the definition of a generalization of B\"ohm trees to this setting.

Equations

$$0{.}_{\mathcal{M}}m$$

$$(a+b){.}_{\mathcal{M}}m$$

$$a{.}_{\mathcal{M}}{0}_{\mathcal{M}}$$

$$\varphi \left(\sum _{i=1}^n{a}_i.m_i\right)=\sum _{i=1}^n{a}_i.\varphi \left(m_i\right)$$

$$\left|\xi \right|:=\left\{x\in X;{\xi }_x\ne 0\right\}.$$

$$\mathbf{S}\left[X\right]:=\left\{\xi \in {\mathbf{S}}^X;\left|\xi \right|\text{ is finite}\right\}.$$

$${\mathfrak{S}}^{\perp }:=\{{\mathcal{X}}^{\prime }\subseteq X;\text{ for all X∈S, X∩X′ is finite}\}.$$

$$\left\{(i,x)\in I\times X;{\xi }_{i,x}\ne 0\right\}$$

$${\left(\sum \overrightarrow{\xi }\right)}_x:=\sum _{i\in I}{\xi }_{i,x}.$$

$$⟨f⟩({\xi }_1,\dots ,{\xi }_n):=\sum _{\left(x_1,\dots ,x_n\right)\in X_1\times \cdots \times X_n}{\xi }_{1,x_1}\cdots {\xi }_{n,x_n}.f(x_1,\dots ,x_n).$$

$$\phi \left(\sum _{i_1\in I_1}{a}_{1,i_1}.{\xi }_{1,i_1},\dots ,\sum _{i_n\in I_n}{a}_{n,i_n}.{\xi }_{n,i_n}\right)=\sum _{(i_1,\dots ,i_n)\in I_1\times \cdots \times I_n}{a}_{1,i_1}\cdots a_{n,i_n}.\phi ({\xi }_{1,i_1},\dots ,{\xi }_{n,i_n}).$$

$${\left({\xi }_{1,i_1,x_1}\cdots {\xi }_{n,i_n,x_n}.f(x_1,\dots ,x_n)\right)}_{(i_1,\dots ,i_n)\in I_1\times \cdots \times I_n,(x_1,\dots ,x_n)\in X_1\times \cdots \times X_n}$$

$$\text{oc}\Delta \ni \overline{s},\overline{t},\overline{u},\overline{v},\overline{w}::=\left[\right]\mid \left[s\right]\cdot \overline{t}$$

$$\begin{array}[]{rclcl}\Delta&\ni&s,t,u,v,w&\mathrel{\mathord{:}\mathord{:}\mathord{=}}&x\mid\lambda x\,{s}\mid{\left\langle s\right\rangle}\,{\overline{t}}\\ \oc\Delta&\ni&\overline{s},\overline{t},\overline{u},\overline{v},\overline{w}&\mathrel{\mathord{:}\mathord{:}\mathord{=}}&{\left[\right]}\mid{\left[s\right]}\cdot\overline{t}.\end{array}$$

$$\mathbf{s}\left(x\right)$$

$$\mathbf{s}\left(\lambda xs\right)$$

$$\mathbf{s}\left(⟨s⟩\overline{t}\right)$$

$$\mathbf{s}\left(\left[s_1,\dots ,s_n\right]\right)$$

$${\mathbf{n}}_x\left(y\right)$$

$${\mathbf{n}}_x\left(\lambda ys\right)$$

$${\mathbf{n}}_x\left(⟨s⟩\overline{t}\right)$$

$${\mathbf{n}}_x\left(\left[s_1,\dots ,s_n\right]\right)$$

$$\begin{array}[]{rlr}\mathbf{d}_{x}{\left(y\right)}&\mathrel{\mathord{:}\mathord{=}}\begin{cases}{\left\{1\right\}}&\text{if $x=y$}\\ \emptyset&\text{otherwise}\end{cases}\\ \mathbf{d}_{x}{\left(\lambda y\,{s}\right)}&\mathrel{\mathord{:}\mathord{=}}{\left\{d+1\mathrel{;}d\in\mathbf{d}_{x}{\left(s\right)}\right\}}&(\text{choosing }y\not=x)\\ \mathbf{d}_{x}{\left({\left[s_{1},\dotsc,s_{n}\right]}\right)}&\mathrel{\mathord{:}\mathord{=}}\bigcup_{i=1}^{n}\mathbf{d}_{x}{\left(s_{i}\right)}\\ \mathbf{d}_{x}{\left({\left\langle s\right\rangle}\,{\overline{t}}\right)}&\mathrel{\mathord{:}\mathord{=}}\mathbf{d}_{x}{\left(s\right)}\mathbin{\cup}{\left\{d+1\mathrel{;}d\in\mathbf{d}_{x}{\left(\overline{t}\right)}\right\}}.\end{array}$$

$$\frac{\partial y}{\partial x}\cdot u$$

$$\frac{\partial \lambda ys}{\partial x}\cdot u$$

$$\frac{\partial ⟨s⟩\overline{t}}{\partial x}\cdot u$$

$$\frac{\partial \left[s_1,\dots ,s_n\right]}{\partial x}\cdot u$$

$$\frac{\partial ϵ}{\partial x}\cdot \sigma =\sum _{i=1}^n\sum _{j=1}^p\frac{\partial e_i}{\partial x}\cdot s_j.$$

$$\frac{\partial }{\partial y}\left(\frac{\partial e}{\partial x}\cdot t\right)\cdot u=\frac{\partial }{\partial x}\left(\frac{\partial e}{\partial y}\cdot u\right)\cdot t+\frac{\partial e}{\partial x}\cdot \left(\frac{\partial t}{\partial y}\cdot u\right).$$

$$\frac{\partial }{\partial y}\left(\frac{\partial e}{\partial x}\cdot t\right)\cdot u=\frac{\partial }{\partial x}\left(\frac{\partial e}{\partial y}\cdot u\right)\cdot t.$$

$$\frac{{\partial }^{n}e}{\partial x^n}\cdot \left(s_1,\dots ,s_n\right):=\frac{\partial }{\partial x}\left(\cdots \frac{\partial e}{\partial x}\cdot s_1\cdots \right)\cdot s_n.$$

$$\frac{{\partial }^{n}e}{\partial x^n}\cdot \left(s_1,\dots ,s_n\right):=\left(\frac{{\partial }^{n}e\left[y/x\right]}{\partial y^n}\cdot \left(s_1,\dots ,s_n\right)\right)\left[x/y\right]$$

$$\frac{{\partial }^{n}e}{\partial x^n}\cdot \left(s_1,\dots ,s_n\right)=\frac{{\partial }^{n}e}{\partial x^n}\cdot \left(s_{f(1)},\dots ,s_{f(n)}\right)$$

$$\frac{{\partial }^{n}e}{\partial x^n}\cdot \overline{s}:=\frac{{\partial }^{n}e}{\partial x^n}\cdot \left(s_1,\dots ,s_n\right)$$

$$\frac{{\partial }^{n}e}{\partial x^n}\cdot \left[s_1,\dots ,s_n\right]=\sum _{\begin{array}{c}f:\left\{1,\dots ,n\right\}\to \left\{1,\dots ,m\right\}\\ \text{f injective}\end{array}}e\left[s_1,\dots ,s_n/x_{f(1)},\dots ,x_{f(n)}\right]$$

$$\frac{{\partial }^{n}y}{\partial x^n}\cdot \overline{u}$$

Full text

We generalize this result to the non-uniform setting of the algebraic $\lambda$-calculus, i.e., $\lambda$-calculus extended with linear combinations of terms. This requires us to tackle two difficulties: foremost is the fact that Ehrhard and Regnier’s techniques rely heavily on the uniform, deterministic nature of the ordinary $\lambda$-calculus, and thus cannot be adapted; second is the absence of any satisfactory generic extension of the notion of Böhm tree in presence of quantitative non-determinism, which is reflected by the fact that the Taylor expansion of an algebraic $\lambda$-term is not always normalizable.

Our solution is to provide a fine grained study of the dynamics of $\beta$-reduction under Taylor expansion, by introducing a notion of reduction on resource vectors, i.e. infinite linear combinations of resource $\lambda$-terms. The latter form the multilinear fragment of the differential $\lambda$-calculus, and resource vectors are the target of the Taylor expansion of $\lambda$-terms. We show the reduction of resource vectors contains the image of any $\beta$-reduction step, from which we deduce that Taylor expansion and normalization commute on the nose.

We moreover identify a class of algebraic $\lambda$-terms, encompassing both normalizable algebraic $\lambda$-terms and arbitrary ordinary $\lambda$-terms: the expansion of these is always normalizable, which guides the definition of a generalization of Böhm trees to this setting.

This work was supported by French ANR projects Coquas (number ANR-12-JS02-0006) and Récré (number ANR-11-BS02-0010), as well as the French-Italian Groupement de Recherche International on Linear Logic.

1. Introduction

Quantitative semantics was first proposed by Girard [Gir88] as an alternative to domains and continuous functionals, for defining denotational models of $\lambda$-calculi with a natural interpretation of non-determinism: a type is given by a collection of “atomic states”; a term of type $A$ is then represented by a vector (i.e. a possibly infinite formal linear combination) of states. The main matter is the treatment of the function space: the construction requires the interpretation of function terms to be analytic, i.e. defined by power series.

This interpretation of $\lambda$-terms was at the origin of linear logic: the application of an analytic map to its argument boils down to the linear application of its power series (seen as a matrix) to the vector of powers of the argument; similarly, linear logic decomposes the application of $\lambda$-calculus into the linear cut rule and the promotion operator. Indeed, the seminal model of linear logic, namely coherence spaces and stable/linear functions, was introduced as a qualitative version of quantitative semantics [Gir86, especially Appendix C].

Dealing with power series, quantitative semantics must account for infinite sums. The interpretations of terms in Girard’s original model can be seen as a special case of Joyal’s analytic functors [Joy86]: in particular, coefficients are sets and infinite sums are given by coproducts. This allows to give a semantics to fixed point operators and to the pure, untyped $\lambda$-calculus. On the other hand, it does not provide a natural way to deal with weighted (e.g., probabilistic) non-determinism, where coefficients are taken in an external semiring of scalars.

In the early 2000’s, Ehrhard introduced an alternative presentation of quantitative semantics [Ehr05], limited to a typed setting, but where types can be interpreted as particular vector spaces, or more generally semimodules over an arbitrary fixed semiring; called finiteness spaces, these are moreover equipped with a linear topology, allowing to interpret linear logic proofs as linear and continuous maps, in a standard sense. In this setting, the formal operation of differentiation of power series recovers its usual meaning of linear approximation of a function, and morphisms in the induced model of $\lambda$-calculus are subject to Taylor expansion: the application $\varphi(\alpha)$ of the analytic function $\varphi$ to the vector $\alpha$ boils down to the sum $\sum_{n\in\mathbf{N}}\frac{1}{n\,\mathord{!}}{\left(\frac{\partial^{n}\varphi}{\partial x^{n}}\right)}_{x=0}\cdot{\alpha^{n}}$ where ${\left(\frac{\partial^{n}\varphi}{\partial x^{n}}\right)}_{x=0}$ is the $n$-th derivative of $\varphi$ computed at [math], which is an $n$-linear map, and $\alpha^{n}$ is the $n$-th tensor power of $\alpha$.

Ehrhard and Regnier gave a computational meaning to such derivatives by introducing linearized variants of application and substitution in the $\lambda$-calculus, which led to the differential $\lambda$-calculus [ER03], and then the resource $\lambda$-calculus [ER08] — the latter retains iterated derivatives at zero as the only form of application. They were then able to recast the above Taylor expansion formula in a syntactic, untyped setting: to every $\lambda$-term $M$, they associate a vector $\mathord{\tau}{\left(M\right)}$ of resource $\lambda$-terms, i.e. terms of the resource $\lambda$-calculus.

The Taylor expansion of a $\lambda$-term can be seen as an intermediate, infinite object, between the term and its denotation in quantitative semantics. Indeed, resource terms still retain a dynamics, if a very simple, finitary one: the size of terms is strictly decreasing under reduction. Furthermore, normal resource terms are in close relationship with the atomic states of quantitative semantics of the pure $\lambda$-calculus (or equivalently with the elements of a reflexive object in the relational model [BEM07]; or with normal type derivations in a non-idempotent intersection type system [dC08]), so that the normal form of $\mathord{\tau}{\left(M\right)}$ can be considered as the denotation of $M$, which allows for a very generic description of quantitative semantics.

Other approaches to quantitative semantics generally impose a constraint on the computational model a priori. For instance, the model of finiteness spaces [Ehr05] is, by design, limited to strongly normalizing computation. Another example is that of probabilistic coherence spaces [DE11], a model of untyped $\lambda$-calculi extended with probabilistic choice, rather than arbitrary weighted superpositions. Alternatively, one can interpret non-deterministic extensions of PCF [LMMP13, Lai16], provided the semiring of scalars has all infinite sums. By contrast, the “normalization of Taylor expansion” approach is more canonical, as it does not rely on a restriction on the scalars, nor on the terms to be interpreted.

Of course, there is a price attached to such canonicity: in general, the normal form of a vector of resource $\lambda$-terms is not well defined, because we may have to consider infinite sums of scalars. Ehrhard and Regnier were nonetheless able to prove that the Taylor expansion $\mathord{\tau}{\left(M\right)}$ of a pure $\lambda$-term is always normalizable [ER08]. This can be seen as a new proof of the fact that Girard’s quantitative semantics of pure $\lambda$-terms uses finite cardinals only [Has96]. They moreover established that this normal form is exactly the Taylor expansion of the Böhm tree $\mathord{\mathsf{BT}}{\left(M\right)}$ of $M$ [ER06] ($\mathord{\mathsf{BT}}{\left(M\right)}$ is the possibly infinite tree obtained by hereditarily applying the head reduction strategy in $M$). Both results rely heavily on the uniformity property of the pure $\lambda$-calculus: all the resource terms in $\mathord{\tau}{\left(M\right)}$ follow a single syntactic tree pattern. This is a bit disappointing since quantitative semantics was introduced as a model of non-determinism, which is ruled out by uniformity.

Actually, the Taylor expansion operator extends naturally to the algebraic $\lambda$-calculus [Vau09]: a generic, non-uniform extension of $\lambda$-calculus, augmenting the syntax with formal finite linear combinations of terms. Then it is not difficult to find terms whose Taylor expansion is not normalizable. Nonetheless, interpreting types as finiteness spaces of resource terms, Ehrhard [Ehr10] proved by a reducibility technique that the Taylor expansion of algebraic $\lambda$-terms typed in a variant of system $F$ is always normalizable.

1.1. Main results

In the present paper, we generalize Ehrhard’s result and show that all weakly normalizable algebraic $\lambda$-terms have a normalizable Taylor expansion (Theorem 7, p.7).111 We had already obtained such a result for strongly normalizable $\lambda$-terms in a previous work with Pagani and Tasson [PTV16]: there, we further proved that the finiteness structure on resource $\lambda$-terms could be refined to characterize exactly the strong normalizability property in a $\lambda$-calculus with finite formal sums of terms. Here we rely on a much coarser notion of finiteness: see subsection 8.1.

We moreover relate the normal form of the expansion of a term with the normal form of the term itself, both in a computational sense (i.e. the irreducible form obtained after a sequence of reductions) and in a more denotational sense, via an analogue of the notion of Böhm tree: Taylor expansion does commute with normalization, in both those senses (Theorem 8, p.8; Theorem 9, p.9).

When restricted to pure $\lambda$-terms, Theorem 9 provides a new proof, not relying on uniformity, that the normal form of $\mathord{\tau}{\left(M\right)}$ is isomorphic to $\mathord{\mathsf{BT}}{\left(M\right)}$. In their full extent, our results provide a generalization of the notion of non-deterministic Böhm tree [dLP95] in a weighted, quantitative setting.

Let us stress that neither Ehrhard’s work [Ehr10] nor our own previous work with Pagani and Tasson [PTV16] addressed the commutation of normalization and Taylor expansion. Indeed, in the absence of uniformity, the techniques used by Ehrhard and Regnier [ER08, ER06] are no longer available, and we had to design another approach.222 It is in fact possible to refine Ehrhard and Regnier’s approach, via the introduction of a rigid variant of Taylor expansion [TAO17], which can then be adapted to the non-deterministic setting. This allows to describe the coefficients in the normal form of Taylor expansion, like in the uniform case, and then prove that Taylor expansion commutes with the computation of Böhm trees. It does not solve the problem of possible divergence, though, and one has to assume the semiring of coefficients is complete, i.e. that all sums converge. See Subsection 1.3 on related work for more details. Our solution is to introduce a notion of reduction on resource vectors, so that: (i) this reduction contains the translation of any $\beta$-reduction step (Lemma 7.10, p.7.10); (ii) normalizability (and the value of the normal form) of resource vectors is preserved under reduction (Lemma 8.4, p.8.4). This approach turns out to be quite delicate, and its development led us to two technical contributions that we deem important enough to be noted here:

• •

the notion of reduction structure (subsection 5.3) that allows to control the families of resource terms simultaneously involved in the reduction of a resource vector: in particular this provides a novel, modular mean to circumvent the inconsistency of $\beta$-reduction in presence of negative coefficients (a typical deficiency of the algebraic $\lambda$-calculus [Vau09]);

• •

our analysis of the effect of parallel reduction on the size of resource $\lambda$-terms (Section 6): this constitutes the technical core of our approach, and it plays a crucial rôle in establishing key additional properties such as confluence (Lemma 6.26, p.6.26, and Corollary 6.46, p.6.46) and conservativity (Lemma 7.24, p.7.24, and Lemma 8.33, p.8.33).

1.2. Structure of the paper

The paper begins with a few mathematical preliminaries, in section 2: we recall some definitions about semirings and semimodules (Subsection 2.1), if only to fix notations and vocabulary; we also provide a very brief review of finiteness spaces (Subsection 2.2), then detail the particular case of linear-continuous maps defined by summable families of vectors (subsection 2.3), the latter notion pervading the paper.

In Section 3 we review the syntax and the reduction relation of the resource $\lambda$-calculus, as introduced by Ehrhard and Regnier [ER08]. The subject is quite standard now, and the only new material we provide is about minor and unsurprising combinatorial properties of multilinear substitution.

Section 4 contains our first notable contribution: after recalling the Taylor expansion construction, we prove that it is compatible with substitution. This result is related with the functoriality of promotion in quantitative denotational models and the proof technique is quite similar. In the passing, we recall the syntax of the algebraic $\lambda$-calculus and briefly discuss the issues raised by the contextual extension of $\beta$-reduction in presence of linear combinations of terms, as evidenced by previous work [Vau07, AD08, Vau09, etc.].

In Section 5, we discuss the possible extensions of the reduction of the resource $\lambda$-calculus to resource vectors, i.e. infinite linear combinations of resource terms, and identify two main issues. First, in order to simulate $\beta$-reduction, we are led to consider the parallel reduction of resource terms in resource vectors, which is not always well defined. Indeed, a single resource term might have unboundedly many antecedents by parallel reduction, hence this process might generate infinite sums of coefficients: we refer to this phenomenon as the size collapse of parallel resource reduction (Subsection 5.2). Second, similarly to the case of the algebraic $\lambda$-calculus, the induced equational theory might become trivial, due the interplay between coefficients in vectors and the reduction relation. To address the latter problem we introduce the notion of reduction structure (Subsection 5.3) which allows us to modularly restrict the set of resource terms involved in a reduction: later in the paper, we will identify reduction structures ensuring the consistency of the reduction of resource vectors (Subsection 8.4).

In Section 6, we introduce successive restrictions of the parallel reduction of resource vectors, in order to avoid the abovementioned size collapse. We first observe that, to bound the size of a term as a function of the size of any of its reducts, it is sufficient to bound the length of chains of immediately nested fired redexes in a single parallel reduction step (Subsection 6.1). This condition does not allow us to close a pair of reductions to a common reduct, because it is not stable under unions of fired redexes. We thus tighten it to bounding the length of all chains of (not necessarily immediately) nested fired redexes (Subsection 6.2): this enables us to obtain a strong confluence result, under a mild hypothesis on the semiring. An even more demanding condition is to require the fired redexes as well as the substituted variables to occur at a bounded depth (subsection 6.3): then we can define a maximal parallel reduction step for each bound, which entails strong confluence without any additional hypothesis. Finally, we consider reduction structures involving resource terms of bounded height (Subsection 6.4): when restricting to such a bounded reduction structure, the strongest of the above three conditions is automatically verified.

We then show, in Section 7, that the translation of $\beta$-reduction through Taylor expansion fits into this setting: the height of the resource terms involved in a Taylor expansion is bounded by that of the original algebraic $\lambda$-term, and every $\beta$-reduction step is an instance of the previously introduced parallel reduction of resource vectors. As a consequence of our strongest confluence result, we moreover obtain that any reduction step from the Taylor expansion of a $\lambda$-term can be extended into the translation of a parallel $\beta$-reduction step.

We turn our attention to normalization in Section 8. We first show that normalizable resource vectors are stable under reduction. We moreover establish that their normal form is obtained as the limit of the parallel left reduction strategy (Subsection 8.1). Then we introduce Taylor normalizable algebraic $\lambda$-terms as those having a normalizable Taylor expansion, and deduce from the previous results that they are stable under $\beta$-reduction (Subsection 8.2): in particular, the normal form of Taylor expansion does define a denotational semantics for that class of terms. Then we establish that normalizable terms are Taylor normalizable (subsection 8.3): it follows that normalization and Taylor expansion commute on the nose.

We conclude with Section 9, showing how our techniques can be applied to the class of hereditarily determinable terms, that we introduce ad-hoc: those include pure $\lambda$-terms as well as normalizable algebraic $\lambda$-terms as a particular case, and we show that all hereditarily determinable terms are Taylor normalizable and the coefficients of the normal form are given by a sequence of approximants, close to the Böhm tree construction.

1.3. Related and future work

Besides the seminal work by Ehrhard and Regnier [ER08, ER06] in the pure case, we have already cited previous approaches to the normalizability of Taylor expansion based on finiteness conditions [Ehr10, PTV16].

A natural question to ask is how our generic notion of normal form of Taylor expansion compares with previously introduced notions of denotation in non-deterministic settings: non-deterministic Böhm trees [dLP95], probabilistic Böhm trees [Lev16], weighted relational models [DE11, LMMP13, Lai16], etc. The very statement of such a question raises several difficulties, prompting further lines of research.

One first obstacle is the fact that, by contrast with the uniform case of the ordinary $\lambda$-calculus, the Taylor expansion operator is not injective on algebraic $\lambda$-terms (see Subsection 4.5), not even on the partial normal forms that we use to introduce the approximants in section 9. This is to be related with the quotient that the non-deterministic Böhm trees of de’Liguoro and Piperno [dLP95] must undergo in order to capture observational equivalence. On the other hand, to our knowledge, finding sufficient conditions on the semiring of scalars ensuring that the Taylor expansion becomes injective is still an open question.

Also, we define normalizable vectors based on the notion of summability: a sum of vectors converges when it is componentwise finite i.e., for each component, only finitely many vectors have a non-zero coefficient (see subsection 2.3). If more information is available on scalars, namely if the semiring of scalars is complete in some topological or order-theoretic sense, it becomes possible to normalize the Taylor expansion of all terms.

Indeed, Tsukada, Asada and Ong have recently established [TAO17] the commutation between computing Böhm trees and Taylor expansion with coefficients taken in the complete semiring of positive reals $[0,+\infty]$ where all sums converge. Let us precise that they do not consider weighted non-determinism, only formal binary sums of terms, and that the notion of Böhm tree they consider is a very syntactic one, similar to the partial normal forms we introduce in section 9. Their approach is based on a precise description of the relationship between the coefficients of resource terms in the expansion of a term and those in the expansion of its Böhm-tree, using a rigid Taylor expansion as an intermediate step: this avoids the ambiguity between the sums of coefficients generated by redundancies in the expansion and those representing non-deterministic superpositions.

Tsukada, Asada and Ong’s work can thus be considered as a refinement of Ehrhard and Regnier’s method, that they are moreover able to generalize to the non-deterministic case provided the semiring of scalars is complete. By contrast, our approach is focused on $\beta$-reduction and identifies a class of algebraic $\lambda$-terms for which the normalization of Taylor expansion converges independently from the topology on scalars. It seems only natural to investigate the connections between both approaches, in particular to tackle the case of weighted non-determinism in a complete semiring, as a first step towards the treatment of probabilistic or quantum superposition, as also suggested by the conclusion of their paper.

In the probabilistic setting, though, the Böhm tree construction [Lev16] relies on both the topological properties of real numbers and the restriction to discrete probability subdistributions. Relying on this, Dal Lago and Leventis have recently shown [DLL19] that the sum defining the normal form of Taylor expansion of an arbitrary probabilistic $\lambda$-term always converges with finite coefficients, and that this normal form is the Taylor expansion of its probabilistic Böhm tree, in the non-extensional sense [Lev16, section 4.2.1]. To get a better understanding of the shape of Taylor expansions of probabilistic $\lambda$-terms and their stability under reduction, a possible first step is to investigate probabilistic coherence spaces [DE11] on resource $\lambda$-terms: these would be the analogue, in the probabilistic setting, of the finiteness structures ensuring the summability of normal forms in the non-deterministic setting (see Subsection 8.3).

Apart from relating our version of quantitative semantics with pre-existing notions of denotation for non-deterministic $\lambda$-calculi, we plan to investigate possible applications to other proof theoretic or computational frameworks: namely, linear logic proof nets [Gir87] and infinitary $\lambda$-calculus [KKSdV97].

The Taylor expansion of $\lambda$-terms can be generalized to linear logic proof nets: the case of linear logic can even be considered as being more primitive, as it is directly related with the structure of those denotational models that validate the Taylor expansion formula [Ehr16]. Proof nets, however, do not enjoy the uniformity property of $\lambda$-terms: no general coherence relation is satisfied by the elements of the Taylor expansion of a proof net [Tas09, section V.4.1]. This can be related with the non-injectivity of coherence semantics [TdF03]. In particular, it is really unclear how Ehrhard and Regnier’s methods, or even Tsukada, Asada and Ong’s could be transposed to this setting. By contrast, our recent work with Chouquet [CA18] shows that our study of reduction under Taylor expansion can be adapted to proof nets.

It is also quite easy to extend the Taylor expansion operator to infinite $\lambda$-terms, at least for those of $\Lambda^{001}$, where only the argument position of applications is treated coinductively. For infinite $\lambda$-terms, it is no longer the case that the support of Taylor expansion involves resource $\lambda$-terms of bounded height only. Fortunately, we can still rely on the results of subsection 6.2, where we only require a bound on the nesting of fired redexes: this should allow us to give a counterpart, through Taylor expansion, of the strongly converging reduction sequences of infinite $\lambda$-terms. More speculatively, another possible outcome is a characterization of hereditarily head normalizable terms via their Taylor expansion, adapting our previous work on normalizability with Pagani and Tasson [PTV16].

2. Technical preliminaries

We write:

• •

$\mathbf{N}$ for the semiring of natural numbers;

• •

$\mathord{\mathfrak{P}}{\left(X\right)}$ for the powerset of a set $X$: $\mathcal{X}\in\mathord{\mathfrak{P}}{\left(X\right)}$ iff $\mathcal{X}\subseteq X$;

• •

$\mathord{\#}{X}$ for the cardinal of a finite set $X$;

• •

$\oc X$ for the set of finite multisets of elements of $X$;

• •

${\left[x_{1},\dotsc,x_{n}\right]}\in\oc X$ for the multiset with elements $x_{1},\dotsc,x_{n}\in X$ (taking repetitions into account), and then $\mathord{\#}{{\left[x_{1},\dotsc,x_{n}\right]}}=n$ for its cardinality;

• •

$\prod_{i\in I}X_{i}$ and $\sum_{i\in I}X_{i}$ respectively for the product and sum of a family ${\left(X_{i}\right)}_{i\in I}$ of sets: in particular $\sum_{i\in I}X_{i}=\bigcup_{i\in I}{\left\{i\right\}}\times X_{i}$;

• •

$X^{I}=\prod_{i\in I}X$ for the set of applications from $I$ to $X$ or, equivalently, for the set of $I$ indexed families of elements of $X$.

Throughout the paper we will be led to consider various categories of sets and elements associated with a single base set $X$: elements of $X$, subsets of $X$, finite multisets of elements of $X$, etc. In order to help keeping track of those categories, we generally adopt the following typographic conventions:

• •

we use small latin letters for the elements of $X$, say $a,b,c\in X$;

• •

for subsets of $X$, we use cursive capitals, say $\mathcal{A},\mathcal{B},\mathcal{C}\in\mathord{\mathfrak{P}}{\left(X\right)}$;

• •

for sets of subsets of $X$, we use Fraktur capitals, say $\mathfrak{A},\mathfrak{B},\mathfrak{C}\subseteq\mathord{\mathfrak{P}}{\left(X\right)}$;

• •

for (possibly infinite) linear combinations of elements of $X$, we use small greek letters, say $\alpha,\beta,\gamma\in\mathbf{S}^{X}$, where $\mathbf{S}$ denotes some set of scalar coefficients;

• •

we transpose all of the above conventions to the set $\oc X$ of finite multisets by overlining: e.g., we write $\overline{a}={\left[a_{1},\dotsc,a_{n}\right]}\in\oc X$, $\overline{\mathcal{A}}\subseteq\oc X$ or $\overline{\alpha}\in\mathbf{S}^{\oc X}$.

In the remaining of this section, we introduce basic mathematical content that will be used throughout the paper.

2.1. Semirings and semimodules

A semiring333 The terminology of semirings is much less well established than that of rings, and one can find various non equivalent definitions depending on the presence of units or on commutativity requirements. Following Golan’s terminology [Gol13], our semirings are commutative semirings, which is required here because we consider multilinear applications between modules. $\mathbf{S}$ is the data of a carrier set $\underline{\mathbf{S}}$, together with commutative monoids $(\underline{\mathbf{S}},+_{\mathbf{S}},0_{\mathbf{S}})$ and $(\underline{\mathbf{S}},\cdot_{\mathbf{S}},1_{\mathbf{S}})$ such that the multiplicative structure distributes over the additive one, i.e. for all $a,b,c\in\underline{\mathbf{S}}$, $a\mathbin{\cdot_{\mathbf{S}}}0_{\mathbf{S}}=0_{\mathbf{S}}$ and $a\cdot_{\mathbf{S}}(b+_{\mathbf{S}}c)=a\cdot_{\mathbf{S}}b+_{\mathbf{S}}a\cdot_{\mathbf{S}}c$.

We will in general abuse notation and identify $\mathbf{S}$ with its carrier set $\underline{\mathbf{S}}$. We will moreover omit the subscripts on symbols $+$, $\cdot$, [math] and $1$, and denote multiplication by concatenation: $ab=a\cdot b$. We also use standard notations for finite sums and products in $\mathbf{S}$, e.g. $\sum_{i=1}^{n}a_{i}=a_{1}+\cdots+a_{n}$. For any semiring $\mathbf{S}$, there is a unique semiring morphism (in the obvious sense) from $\mathbf{N}$ to $\mathbf{S}$: to $n\in\mathbf{N}$ we associate the sum $\sum_{i=1}^{n}1\in\mathbf{S}$ that we also write $n\in\mathbf{S}$, although this morphism is not necessarily injective. Consider for instance the semiring $\mathbf{B}$ of booleans, with $\underline{\mathbf{B}}={\left\{0,1\right\}}$, $\mathord{+}_{\mathbf{B}}=\mathord{\max}$ and $\mathord{\cdot}_{\mathbf{B}}=\mathord{\times}$.

We finish this subsection by recalling the definitions of semimodules and their morphisms. A (left) $\mathbf{S}$-semimodule $\mathcal{M}$ is the data of a commutative monoid $(\underline{\mathcal{M}},0_{\mathcal{M}},+_{\mathcal{M}})$ together with an external product $._{\mathcal{M}}:\mathbf{S}\times\underline{\mathcal{M}}\to\underline{\mathcal{M}}$ subject to the following identities:

[TABLE]

for all $a,b\in\mathbf{S}$ and $m,n\in\underline{\mathcal{M}}$. Again, we will in general abuse notation and identify $\mathcal{M}$ with its carrier set $\underline{\mathcal{M}}$, and omit the subscripts on symbols $+$, . and [math].

Let $\mathcal{M}$ and $\mathcal{N}$ be $\mathbf{S}$-semimodules. We say $\phi:\mathcal{M}\to\mathcal{N}$ is linear if

[TABLE]

for all $m_{1},\dotsc,m_{n}\in\mathcal{M}$ and all $a_{1},\dotsc,a_{n}\in\mathbf{S}$. If moreover $\mathcal{M}_{1},\dotsc,\mathcal{M}_{n}$ are $\mathbf{S}$-semimodules, we say $\psi:\mathcal{M}_{1}\times\cdots\times\mathcal{M}_{n}\to\mathcal{N}$ is $n$-linear if it is linear in each component.

Given a set $X$, $\mathbf{S}^{X}$ is the semimodule of formal linear combinations of elements of $X$: a vector $\xi\in\mathbf{S}^{X}$ is nothing but an $X$-indexed family of scalars ${\left(\xi_{x}\right)}_{x\in X}$, that we may also denote by $\sum_{x\in X}\xi_{x}.x$. The support ${\left|\xi\right|}$ of a vector $\xi\in\mathbf{S}^{X}$ is the set of elements of $X$ having a non-zero coefficient in $\xi$:

[TABLE]

We write $\mathbf{S}{\left[X\right]}$ for the set of vectors with finite support:

[TABLE]

In particular $\mathbf{S}{\left[X\right]}$ is the semimodule freely generated by $X$, and is a subsemimodule of $\mathbf{S}^{X}$.

2.2. Finiteness spaces

A finiteness space [Ehr05] is a subsemimodule of $\mathbf{S}^{X}$ obtained by imposing a restriction on the support of vectors, as follows.

If $X$ is a set, we call structure on $X$ any set $\mathfrak{S}\subseteq\mathord{\mathfrak{P}}{\left(X\right)}$, and then the dual structure is

[TABLE]

A relational finiteness space is a pair $(X,\mathfrak{F})$, where $X$ is a set (the web of the finiteness space) and $\mathfrak{F}\subseteq\mathord{\mathfrak{P}}{\left(X\right)}$ is a structure on $X$ such that $\mathfrak{F}=\mathfrak{F}^{\perp\perp}$: $\mathfrak{F}$ is then called a finiteness structure, and we say $\mathcal{X}\subseteq X$ is finitary in $(X,\mathfrak{F})$ iff $\mathcal{X}\in\mathfrak{F}$. The finiteness space generated by $(X,\mathfrak{F})$, denoted by $\mathbf{S}{\left\langle X,\mathfrak{F}\right\rangle}$, or simply $\mathbf{S}{\left\langle\mathfrak{F}\right\rangle}$, is then the set of vectors on $X$ with finitary support: $\xi\in\mathbf{S}{\left\langle\mathfrak{F}\right\rangle}$ iff ${\left|\xi\right|}\in\mathfrak{F}$. By this definition, if $\xi\in\mathbf{S}{\left\langle\mathfrak{F}\right\rangle}$ and $\xi^{\prime}\in\mathbf{S}{\left\langle\mathfrak{F}^{\perp}\right\rangle}$ then the sum $\sum_{x\in X}\xi_{x}\xi^{\prime}_{x}$ involves finitely many nonzero summands.

Finitary subsets are downwards closed for inclusion, and finite unions of finitary subsets are finitary, hence $\mathbf{S}{\left\langle X,\mathfrak{F}\right\rangle}$ is a subsemimodule of $\mathbf{S}^{X}$. Moreover, the least (resp. greatest) finiteness structure on $X$ is the set $\mathord{\mathfrak{P}_{f}}{\left(X\right)}$ of finite subsets of $X$ (resp. the powerset $\mathord{\mathfrak{P}}{\left(X\right)}$), generating the finiteness space $\mathbf{S}{\left[X\right]}$ (resp. $\mathbf{S}^{X}$).

We do not describe the whole category of finiteness spaces and linear-continuous maps here. In particular we do not recall the details of the linear topology induced on $\mathbf{S}{\left\langle X,\mathfrak{F}\right\rangle}$ by $\mathfrak{F}$: the reader may refer to Ehrhard’s original paper [Ehr05] or his survey presentation of differential linear logic [Ehr16].

In the following, we focus on a very particular case, where the finiteness structure on base types is trivial (i.e. there is no restriction on the support of vectors): linear-continuous maps are then univocally generated by summable functions.

We started with the general notion of finiteness space nonetheless, because it provides a good background for the general spirit of our contributions: we are interested in infinite objects restricted so that, componentwise, all our constructions involve finite sums only. Also, the semimodule of normalizable resource vectors introduced in section 8 is easier to work with once its finiteness space structure is exposed.

2.3. Summable functions

Let $\overrightarrow{\xi}={\left(\xi_{i}\right)}_{i\in I}\in{\left(\mathbf{S}^{X}\right)}^{I}$ be a family of vectors: write $\xi_{i}=\sum_{x\in X}\xi_{i,x}.x$. We say $\overrightarrow{\xi}$ is summable if, for all $x\in X$, ${\left\{i\in I\mathrel{;}x\in{\left|\xi_{i}\right|}\right\}}$ is finite. In this case, we define the sum $\sum\overrightarrow{\xi}=\sum_{i\in I}\xi_{i}\in\mathbf{S}^{X}$ in the obvious, pointwise way:444 The reader can check that the family $\overrightarrow{\xi}$ is summable iff the support set

${\left\{(i,x)\in I\times X\mathrel{;}\xi_{i,x}\not=0\right\}}$

is finitary in the relational arrow finiteness space $(I\times X,\mathord{\mathfrak{P}}{\left(I\right)}\multimap\mathord{\mathfrak{P}}{\left(X\right)})$ as defined by Ehrhard [Ehr05, see in particular Lemma 3]. Then $\sum\overrightarrow{\xi}$ is the result of applying the matrix ${\left(\xi_{i,x}\right)}_{i\in I,x\in X}$ to the vector ${\left(1\right)}_{i\in I}\in\mathbf{S}{\left\langle\mathord{\mathfrak{P}}{\left(I\right)}\right\rangle}=\mathbf{S}^{I}$.

[TABLE]

Of course, any finite family of vectors is summable and, fixing an index set $I$ and a base set $X$, summable families in ${\left(\mathbf{S}^{X}\right)}^{I}$ form an $\mathbf{S}$-semimodule, with operations defined pointwise.

Moreover, if ${\left(\xi_{i}\right)}_{i\in I}\in{\left(\mathbf{S}^{X}\right)}^{I}$ is summable, then it follows from the inclusion ${\left|a_{i}.\xi_{i}\right|}\subseteq{\left|\xi_{i}\right|}$ that ${\left(a_{i}.\xi_{i}\right)}_{i\in I}$ is also summable for any family of scalars ${\left(a_{i}\right)}_{i\in I}\in\mathbf{S}^{I}$. Whenever the $n$-ary function $f:X_{1}\times\cdots\times X_{n}\to\mathbf{S}^{Y}$ (i.e. the family ${\left(f(x_{1},\dotsc,x_{n})\right)}_{{\left(x_{1},\dotsc,x_{n}\right)}\in X_{1}\times\cdots\times X_{n}}$) is summable, we can thus define its extension ${\left\langle f\right\rangle}:\mathbf{S}^{X_{1}}\times\cdots\times\mathbf{S}^{X_{n}}\to\mathbf{S}^{Y}$ by

[TABLE]

Note that we can consider $f:X\to\mathbf{S}^{Y}$ as a $Y\times X$ matrix: $f_{y,x}=f(x)_{y}$. Then if $f$ is summable and $\xi\in\mathbf{S}^{X}$, ${\left\langle f\right\rangle}({\xi})$ is nothing but the application of the matrix $f$ to the column $\xi$: the summability hypothesis ensures that this is well defined.

It turns out that the linear extensions of summable functions are exactly the linear-continuous maps, defined as follows:

Definition \thethm.

Let $\varphi:\mathbf{S}^{X_{1}}\times\cdots\times\mathbf{S}^{X_{n}}\to\mathbf{S}^{Y}$. We say ${\varphi}$ is $n$-linear-continuous if, for all summable families $\overrightarrow{\xi_{1}}={\left(\xi_{1,i}\right)}_{i\in I_{1}}\in{\left(\mathbf{S}^{X_{1}}\right)}^{I_{1}},\dotsc,\overrightarrow{\xi_{n}}={\left(\xi_{n,i}\right)}_{i\in I_{n}}\in{\left(\mathbf{S}^{X_{n}}\right)}^{I_{n}}$, the family ${\left(\varphi(\xi_{1,i_{1}},\dotsc,\xi_{n,i_{n}})\right)}_{(i_{1},\dotsc,i_{n})\in I_{1}\times\cdots\times I_{n}}$ is summable and, for all families of scalars, $\overrightarrow{a_{1}}={\left(a_{1,i}\right)}_{i\in I_{1}}\in{\mathbf{S}}^{I_{1}},\dotsc,\overrightarrow{a_{n}}={\left(a_{n,i}\right)}_{i\in I_{n}}\in{\mathbf{S}}^{I_{n}}$, we have

[TABLE]

Lemma \thethm.

If $\varphi:\mathbf{S}^{X_{1}}\times\cdots\times\mathbf{S}^{X_{n}}\to\mathbf{S}^{Y}$ is $n$-linear-continuous then its restriction $\varphi\mathord{\upharpoonright}_{X_{1}\times\cdots\times X_{n}}$ is a summable $n$-ary function and $\varphi={\left\langle\varphi\mathord{\upharpoonright}_{X_{1}\times\cdots\times X_{n}}\right\rangle}$. Conversely, if $f:X_{1}\times\cdots\times X_{n}\to\mathbf{S}^{Y}$ is a summable $n$-ary function then ${\left\langle f\right\rangle}$ is $n$-linear-continuous.

Proof.

It is possible to derive both implications from general results on finiteness spaces.555 One might check that a map $\varphi:\mathbf{S}^{X_{1}}\times\cdots\times\mathbf{S}^{X_{n}}\to\mathbf{S}^{Y}$ is $n$-linear-continuous in the sense of Definition 2.3 iff it is $n$-linear and continuous in the sense of the linear topology of finiteness spaces, observing that the topology on $\mathbf{S}^{X}=\mathbf{S}{\left\langle\mathord{\mathfrak{P}}{\left(X\right)}\right\rangle}$ is the product topology ($\mathbf{S}$ being endowed with the discrete topology) [Ehr05, Section 3]. Moreover, $n$-ary summable functions $f:X_{1}\times\cdots\times X_{n}\to\mathbf{S}^{Y}$ are the elements of the finiteness space $\mathbf{S}{\left\langle\mathord{\mathfrak{P}}{\left(X_{1}\right)}\otimes\cdots\otimes\mathord{\mathfrak{P}}{\left(X_{n}\right)}\multimap\mathord{\mathfrak{P}}{\left(Y\right)}\right\rangle}$. As a general fact, the linear-continuous maps $\mathbf{S}{\left\langle\mathfrak{F}\right\rangle}\to\mathbf{S}{\left\langle\mathfrak{G}\right\rangle}$ are exactly the linear extensions of vectors in $\mathbf{S}{\left\langle\mathfrak{F}\multimap\mathfrak{G}\right\rangle}$. But linear-continuous maps from a tensor product of finiteness spaces correspond with multilinear-hypocontinuous maps [Ehr05, Section 3] rather than the more restrictive multilinear-continuous maps. In the very simple setting of summable functions, though, both notions coincide, since $\mathbf{S}^{X}$ is always locally linearly compact [Ehr05, Proposition 15].

We also sketch a direct proof.

The first implication follows directly from the definitions, observing that each diagonal family of vectors $(x)_{x\in X_{i}}$ is obviously summable.

For the converse: let $\overrightarrow{\xi_{1}}={\left(\xi_{1,i}\right)}_{i\in I_{1}}\in{\left(\mathbf{S}^{X_{1}}\right)}^{I_{1}},\dotsc,\overrightarrow{\xi_{n}}={\left(\xi_{n,i}\right)}_{i\in I_{n}}\in{\left(\mathbf{S}^{X_{n}}\right)}^{I_{n}}$ be summable families. We first prove that the family

[TABLE]

is summable. Fix $y\in Y$. If $y\in{\left|\xi_{1,i_{1},x_{1}}\cdots\xi_{n,i_{n},x_{n}}.f(x_{1},\dotsc,x_{n})\right|}$ then in particular $y\in{\left|f(x_{1},\dotsc,x_{n})\right|}$: since $f$ is summable, there are finitely many such tuples $(x_{1},\dotsc,x_{n})\in X_{1}\times\cdots\times X_{n}$. For each such tuple $(x_{1},\dotsc,x_{n})$ and each $k\in{\left\{1,\dotsc,n\right\}}$, since $\overrightarrow{\xi}_{k}$ is summable, there are finitely many $i_{k}$’s such that $\xi_{k,i_{k},x_{k}}\not=0$. The necessary equation then follows from the associativity of sums. ∎

From now on, we will identify summable functions with their multilinear-continuous extensions. Moreover, it should be clear that multilinear-continuous maps compose.

3. The resource $\lambda$-calculus

In this section, we recall the syntax and reduction of the resource $\lambda$-calculus, that was introduced by Ehrhard and Regnier [ER08] as the multilinear fragment of the differential $\lambda$-calculus [ER03]. The syntax is very similar to that of Boudol’s resource $\lambda$-calculus [Bou93] but the intended meaning (multilinear approximations of $\lambda$-terms) as well as the dynamics is fundamentally different.

We also recall the definitions of the multilinear counterparts of term substitution: partial differentiation and multilinear substitution.

In the passing, we introduce various quantities on resource $\lambda$-terms (size, height, and number and maximum depth of occurrences of a variable) and we state basic results that will be used throughout the paper.

Finally, we present the dynamics of the calculus: resource reduction and normalization.

3.1. Resource expressions

In the remaining of the paper, we suppose an infinite, countable set $\mathcal{V}$ of variables is fixed: we use small letters $x,y,z$ to denote variables.

We define the sets $\Delta$ of resource terms and $\oc\Delta$ of resource monomials by mutual induction as follows:666 We use a self explanatory if not standard variant of BNF notation for introducing syntactic objects:

$\oc\Delta\ni\overline{s},\overline{t},\overline{u},\overline{v},\overline{w}\mathrel{\mathord{:}\mathord{:}\mathord{=}}{\left[\right]}\mid{\left[s\right]}\cdot\overline{t}$

means that we define the set $\oc\Delta$ of resource monomials as that inductively generated by the empty monomial, and addition of a term to a monomial, and that we will denote resource monomials using overlined letters among $\overline{s},\overline{t},\overline{u},\overline{v},\overline{w}$, possibly with sub- and superscripts.

[TABLE]

Terms are considered up to $\alpha$-equivalence and monomials up to permutativity: we write ${\left[t_{1},\dotsc,t_{n}\right]}$ for ${\left[t_{1}\right]}\cdot{\left(\cdots\cdot{\left({\left[t_{n}\right]}\cdot{\left[\right]}\right)}\right)}$ and equate ${\left[t_{1},\dotsc,t_{n}\right]}$ with ${\left[t_{f(1)},\dotsc,t_{f(n)}\right]}$ for all permutation $f$ of ${\left\{1,\dotsc,n\right\}}$, so that resource monomials coincide with finite multisets of resource terms.777 Resource monomials are often called bags, bunches or poly-terms in the literature, but we prefer to strengthen the analogy with power series here.

We will then write $\overline{s}\cdot\overline{t}$ for the multiset union of $\overline{s}$ and $\overline{t}$, and $\mathord{\#}{{\left[s_{1},\dotsc,s_{n}\right]}}\mathrel{\mathord{:}\mathord{=}}n$.

We call resource expression any resource term or resource monomial and write $(\oc)\Delta$ for either $\Delta$ or $\oc\Delta$: whenever we use this notation several times in the same context, all occurrences consistently denote the same set. When we make a definition or a proof by induction on resource expressions, we actually use a mutual induction on resource terms and monomials.

Definition \thethm.

We define by induction over a resource expression $e\in(\oc)\Delta$, its size $\mathord{\mathbf{s}}{\left(e\right)}\in\mathbf{N}$ and its height $\mathord{\mathbf{h}}{\left(e\right)}\in\mathbf{N}$:

[TABLE]

It should be clear that, for all $e\in(\oc)\Delta$, $\mathord{\mathbf{h}}{\left(e\right)}\leq\mathord{\mathbf{s}}{\left(e\right)}$. Also observe that $\mathord{\mathbf{s}}{\left(s\right)}>0$ and $\mathord{\mathbf{h}}{\left(s\right)}>0$ for all $s\in\Delta$, and $\mathord{\mathbf{s}}{\left(\overline{s}\right)}\geq\mathord{\#}{\overline{s}}$ for all $\overline{s}\in\oc\Delta$. In the application case, we chose not to increment the height of the function: this is not crucial but it will allow to simplify some of our computations in Section 6. In particular, in the case of a redex we have $\mathord{\mathbf{h}}{\left({\left\langle\lambda x\,{s}\right\rangle}\,{\overline{t}}\right)}=1+\max{\left\{\mathord{\mathbf{h}}{\left(s\right)},\mathord{\mathbf{h}}{\left(\overline{t}\right)}\right\}}$.

For all resource expression $e$, we write $\mathord{\mathbf{fv}}{\left(e\right)}$ for the set of its free variables. In the remaining of the paper, we will often have to prove that some set $\mathcal{E}\subseteq(\oc)\Delta$ is finite: we will generally use the fact that $\mathcal{E}$ is finite iff both ${\left\{\mathord{\mathbf{s}}{\left(e\right)}\mathrel{;}e\in\mathcal{E}\right\}}$ and $\mathord{\mathbf{fv}}{\left(\mathcal{E}\right)}\mathrel{\mathord{:}\mathord{=}}\bigcup_{e\in\mathcal{E}}\mathord{\mathbf{fv}}{\left(e\right)}$ are finite.

Besides the size and height of an expression, we will also need finer grained information on occurrences of variables, providing a quantitative counterpart to the set of free variables:

Definition \thethm.

We define by induction over resource expressions the number $\mathbf{n}_{x}{\left(e\right)}\in\mathbf{N}$ of occurrences and the set $\mathbf{d}_{x}{\left(e\right)}\in\mathbf{N}$ of occurrence depths of a variable $x$ in $e\in(\oc)\Delta$:

[TABLE]

and

[TABLE]

We then write $\mathbf{md}_{x}{\left(e\right)}\mathrel{\mathord{:}\mathord{=}}\max\mathbf{d}_{x}{\left(e\right)}$ for the maximal depth of occurrences of $x$ in $e$.

Again, it should be clear that $\mathbf{n}_{x}{\left(e\right)}\leq\mathord{\mathbf{s}}{\left(e\right)}$ and $\mathbf{md}_{x}{\left(e\right)}\leq\mathord{\mathbf{h}}{\left(e\right)}$. Moreover, $x\in\mathord{\mathbf{fv}}{\left(e\right)}$ iff $\mathbf{n}_{x}{\left(e\right)}\not=0$ iff $\mathbf{d}_{x}{\left(e\right)}\not=\emptyset$ iff $\mathbf{md}_{x}{\left(e\right)}\not=0$.

3.2. Partial derivatives

In the resource $\lambda$-calculus, the substitution $e{\left[s/x\right]}$ of a term $s$ for a variable $x$ in $e$ admits a linear counterpart: this operator was initially introduced in the differential $\lambda$-calculus [ER03] in the form of a partial differentiation operation, reflecting the interpretation of $\lambda$-terms as analytic maps in quantitative semantics.

Partial differentiation enforces the introduction of formal finite sums of resource expressions: these are the actual objects of the resource $\lambda$-calculus, and in particular the dynamics will act on finite sums of terms rather than on simple resource terms (see Subsection 3.4). We extend all syntactic constructs to finite sums of resource expressions by linearity: if $\sigma=\sum_{i=1}^{n}s_{i}\in\mathbf{N}{\left[\Delta\right]}$ and $\overline{\tau}=\sum_{j=1}^{p}\overline{t}_{j}\in\mathbf{N}{\left[\oc\Delta\right]}$, we set $\lambda x\,{\sigma}\mathrel{\mathord{:}\mathord{=}}\sum_{i=1}^{n}\lambda x\,{s_{i}}$, ${\left\langle\sigma\right\rangle}\,{\overline{\tau}}\mathrel{\mathord{:}\mathord{=}}\sum_{i=1}^{n}\sum_{j=1}^{p}{\left\langle s_{i}\right\rangle}\,{\overline{t}_{j}}$ and ${\left[\sigma\right]}\cdot{\overline{\tau}}\mathrel{\mathord{:}\mathord{=}}\sum_{i=1}^{n}\sum_{j=1}^{p}{\left[s_{i}\right]}\cdot{\overline{t}_{j}}$.

This linearity of syntactic constructs will be generalized to vectors of resource expressions in the next section. For now, up to linearity, it is already possible to consider the substitution $e{\left[\sigma/x\right]}$ of a finite sum of terms $\sigma$ for a variable term $x$ in an expression $e$: in particular $e{\left[0/x\right]}=0$ whenever $x\in\mathord{\mathbf{fv}}{\left(e\right)}$. This is in turn extended to sums by linearity: $\epsilon{\left[\sigma/x\right]}=\sum_{i=1}^{n}e_{i}{\left[\sigma/x\right]}$ when $\epsilon=\sum_{i=1}^{n}e_{i}$. Observe that this is not linear in $\sigma$, because $x$ may occur several times in $e$: for instance, with a monomial of degree 2, ${\left[x,x\right]}{\left[t+u/x\right]}={\left[t,t\right]}+{\left[t,u\right]}+{\left[u,t\right]}+{\left[u,u\right]}$.

Partial differentiation is then defined as follows:

Definition \thethm.

For all $u\in\Delta$ and $x\in\mathcal{V}$, we define the partial derivative $\frac{\partial e}{\partial x}\cdot u\in\mathbf{N}{\left[(\oc)\Delta\right]}$ of $e\in(\oc)\Delta$, by induction on $e$:

[TABLE]

Partial differentiation is extended to finite sums of expressions by bilinearity: if $\epsilon=\sum_{i=1}^{n}e_{i}\in\mathbf{N}{\left[(\oc)\Delta\right]}$ and $\sigma=\sum_{j=1}^{p}s_{j}\in\mathbf{N}{\left[\Delta\right]}$, we set

[TABLE]

{lemC}

[[ER08, Lemma 2]]

If $x\not\in\mathord{\mathbf{fv}}{\left(u\right)}$ then

[TABLE]

If moreover $y\not\in\mathord{\mathbf{fv}}{\left(t\right)}$, we obtain a version of Schwarz’s theorem on the symmetry of second derivatives:

[TABLE]

If $x\not\in\mathord{\mathbf{fv}}{\left(s_{i}\right)}$ for all $i\in{\left\{1,\dotsc,n\right\}}$, we write

[TABLE]

More generally, we write

[TABLE]

for any $y\not\in\bigcup_{i=1}^{n}\mathord{\mathbf{fv}}{\left(s_{i}\right)}\mathbin{\cup}(\mathord{\mathbf{fv}}{\left(e\right)}\setminus{\left\{x\right\}})$: it should be clear that this definition does not depend on the choice of such a variable $y$. By the previous lemma,

[TABLE]

for any permutation $f$ of ${\left\{1,\dotsc,n\right\}}$ and we will thus write

[TABLE]

whenever $\overline{s}={\left[s_{1},\dotsc,s_{n}\right]}$.

An alternative, more direct presentation of iterated partial derivatives is as follows. Suppose $\mathbf{n}_{x}{\left(e\right)}=m$, and write $x_{1},\dotsc,x_{m}$ for the occurrences of $x$ in $e$. Then:

[TABLE]

More formally, we obtain:

Lemma \thethm.

*For all monomial $\overline{u}={\left[u_{1},\dotsc,u_{n}\right]}\in\oc\Delta$ and all variable $x\in\mathcal{V}$:888 In this definition and in the remaining of the paper, we say a tuple $(I_{1},\dotsc,I_{n})\in\mathord{\mathfrak{P}}{\left(I\right)}^{n}$ is a partition of $I$ if $I=\bigcup_{i=1}^{n}I_{k}$, and the $I_{k}$’s are pairwise disjoint. We do not require the $I_{k}$’s to be nonempty. Hence a partition of $I$ into a $n$-tuple is uniquely defined by a function from $I$ to ${\left\{1,\dotsc,n\right\}}$. *

[TABLE]

where $\overline{u}_{I}$ denotes ${{\left[u_{i_{1}},\dotsc,u_{i_{p}}\right]}}$ whenever $I={\left\{i_{1},\dotsc,i_{p}\right\}}$ with $p=\mathord{\#}{I}$.

Proof.

Easy, by induction on $n$. ∎

Lemma \thethm.

For all $e\in(\oc)\Delta$, $\overline{s}\in\oc\Delta$, $x\not=y\in\mathcal{V}$ and ${e^{\prime}}\in{\left|\frac{\partial^{n}e}{\partial x^{n}}\cdot\overline{s}\right|}$ with $n=\mathord{\#}{\overline{s}}$, moreover assuming that $x\not\in\mathord{\mathbf{fv}}{\left(\overline{s}\right)}$:

• •

$\mathbf{n}_{x}{\left(e\right)}\geq n$* and $\mathbf{n}_{x}{\left(e^{\prime}\right)}=\mathbf{n}_{x}{\left(e\right)}-n$;*

• •

$\mathbf{n}_{y}{\left(e^{\prime}\right)}=\mathbf{n}_{y}{\left(e\right)}+\mathbf{n}_{y}{\left(\overline{s}\right)}$;

• •

$\mathbf{d}_{x}{\left(e^{\prime}\right)}\subseteq\mathbf{d}_{x}{\left(e\right)}$;

• •

$\mathbf{d}_{y}{\left(e\right)}\subseteq\mathbf{d}_{y}{\left(e^{\prime}\right)}\subseteq\mathbf{d}_{y}{\left(e\right)}\mathbin{\cup}{\left\{d+d^{\prime}-1\mathrel{;}d\in\mathbf{d}_{x}{\left(e\right)},d^{\prime}\in\mathbf{d}_{y}{\left(\overline{s}\right)}\right\}}$;

• •

$\mathord{\mathbf{s}}{\left(e^{\prime}\right)}=\mathord{\mathbf{s}}{\left(e\right)}+\mathord{\mathbf{s}}{\left(\overline{s}\right)}-n$;

• •

$\mathord{\mathbf{h}}{\left(e\right)}\leq\mathord{\mathbf{h}}{\left(e^{\prime}\right)}\leq\max{\left\{\mathord{\mathbf{h}}{\left(e\right)},\mathbf{md}_{x}{\left(e\right)}+\mathord{\mathbf{h}}{\left(\overline{s}\right)}-1\right\}}$.

Proof.

Each result is easily established by induction on $e$, using the previous lemma to enable the induction. ∎

3.3. Multilinear substitution

Recall that Taylor expansion involves iterated derivatives at [math]. If $n=\mathord{\#}{\overline{s}}$ and $x\not\in\mathord{\mathbf{fv}}{\left(\overline{s}\right)}$ we write

[TABLE]

Observe that by Lemma 3.2: if $n>\mathbf{n}_{x}{\left(e\right)}$ then $\frac{\partial^{n}e}{\partial x^{n}}\cdot\overline{s}=0$; and if $n<\mathbf{n}_{x}{\left(e\right)}$ then $x\in\mathord{\mathbf{fv}}{\left(e^{\prime}\right)}$ for all $e^{\prime}\in{\left|\frac{\partial^{n}e}{\partial x^{n}}\cdot\overline{s}\right|}$, and then $e^{\prime}{\left[0/x\right]}=0$. In other words,

[TABLE]

We say $\partial_{x}e\cdot\overline{s}$ is the $n$-linear substitution of $\overline{s}$ for $x$ in $e$. More generally, we write

[TABLE]

for any $y\not\in\mathord{\mathbf{fv}}{\left(\overline{s}\right)}\mathbin{\cup}(\mathord{\mathbf{fv}}{\left(e\right)}\setminus x)$ and it should again be clear that this definition does not depend of the choice of such a $y$. By a straightforward application of Lemma 3.2, we obtain:

Lemma \thethm.

For all $e\in(\oc)\Delta$, $\overline{s}\in\oc\Delta$, $x\not=y\in\mathcal{V}$ and ${e^{\prime}}\in{\left|\partial_{x}e\cdot\overline{s}\right|}$, assuming $x\not\in\mathord{\mathbf{fv}}{\left(\overline{s}\right)}$:

• •

$\mathbf{n}_{x}{\left(e\right)}=\mathord{\#}{\overline{s}}$* and $\mathbf{n}_{x}{\left(e^{\prime}\right)}=0$;*

• •

$\mathbf{n}_{y}{\left(e^{\prime}\right)}=\mathbf{n}_{y}{\left(e\right)}+\mathbf{n}_{y}{\left(\overline{s}\right)}$;

• •

$\mathbf{d}_{x}{\left(e^{\prime}\right)}=\emptyset$;

• •

$\mathbf{d}_{y}{\left(e\right)}\subseteq\mathbf{d}_{y}{\left(e^{\prime}\right)}\subseteq\mathbf{d}_{y}{\left(e\right)}\mathbin{\cup}{\left\{d+d^{\prime}-1\mathrel{;}d\in\mathbf{d}_{x}{\left(e\right)},d^{\prime}\in\mathbf{d}_{y}{\left(\overline{s}\right)}\right\}}$;

• •

$\mathord{\mathbf{s}}{\left(e^{\prime}\right)}=\mathord{\mathbf{s}}{\left(e\right)}+\mathord{\mathbf{s}}{\left(\overline{s}\right)}-\mathord{\#}{\overline{s}}$;

• •

$\mathord{\mathbf{h}}{\left(e\right)}\leq\mathord{\mathbf{h}}{\left(e^{\prime}\right)}\leq\max{\left\{\mathord{\mathbf{h}}{\left(e\right)},\mathbf{md}_{x}{\left(e\right)}+\mathord{\mathbf{h}}{\left(\overline{s}\right)}-1\right\}}$.

In particular, $\mathord{\mathbf{fv}}{\left(e^{\prime}\right)}=(\mathord{\mathbf{fv}}{\left(e\right)}\setminus{\left\{x\right\}})\mathbin{\cup}\mathord{\mathbf{fv}}{\left(\overline{s}\right)}$, and $\max{\left\{\mathord{\mathbf{s}}{\left(e\right)},\mathord{\mathbf{s}}{\left(\overline{s}\right)}\right\}}\leq\mathord{\mathbf{s}}{\left(e^{\prime}\right)}\leq\mathord{\mathbf{s}}{\left(e\right)}+\mathord{\mathbf{s}}{\left(\overline{s}\right)}$.

Again, we can give a direct presentation of multilinear substitution. Suppose $\mathbf{n}_{x}{\left(e\right)}=m$, and write $x_{1},\dotsc,x_{m}$ for the occurrences of $x$ in $e$. Then:

[TABLE]

More formally, as a consequence of Lemma 3.2:

Lemma \thethm.

For all monomial $\overline{u}={\left[u_{1},\dotsc,u_{n}\right]}\in\oc\Delta$ and all variable $x\in\mathcal{V}$:

[TABLE]

where the conditions on cardinalities of subsets of ${\left\{1,\dotsc,n\right\}}$ in the application and monomial cases may be omitted.

A similar result is the commutation of multilinear substitutions:

Lemma \thethm.

If $x\not\in\mathord{\mathbf{fv}}{\left(\overline{u}\right)}$ then:

[TABLE]

Proof.

Write $n=\mathord{\#}{\overline{t}}$ and $p=\mathord{\#}{\overline{u}}$. It is sufficient to prove

[TABLE]

by induction on $n$ and $p$, using Lemma 3.2. ∎

3.4. Resource reduction

If $\mathrel{{\rightarrow}}$ is a reduction relation, we will write $\mathrel{{\rightarrow^{?}}}$ (resp. $\mathrel{{\rightarrow^{+}}}$; $\mathrel{{\rightarrow^{*}}}$) for its reflexive (resp. transitive; reflexive and transitive) closure.

In the resource $\lambda$-calculus, a redex is a term of the form ${\left\langle\lambda x\,{t}\right\rangle}\,{\overline{u}}\in\Delta$ and its reduct is $\partial_{x}t\cdot\overline{u}\in\mathbf{N}{\left[\Delta\right]}$. The resource reduction $\mathrel{{\rightarrow_{\partial}}}$ is then the contextual closure of this reduction step on finite sums of resource expressions. More precisely:

Definition \thethm.

We define the resource reduction relation $\mathord{\mathrel{{\rightarrow_{\partial}}}}\subseteq(\oc)\Delta\times\mathbf{N}{\left[(\oc)\Delta\right]}$ inductively as follows:

• •

${\left\langle\lambda x\,{s}\right\rangle}\,{\overline{t}}\mathrel{{\rightarrow_{\partial}}}\partial_{x}s\cdot\overline{t}$ for all $s\in\Delta$ and $\overline{t}\in\oc\Delta$;

• •

$\lambda x\,{s}\mathrel{{\rightarrow_{\partial}}}\lambda x\,{\sigma^{\prime}}$ as soon as $s\mathrel{{\rightarrow_{\partial}}}\sigma^{\prime}$;

• •

${\left\langle s\right\rangle}\,{\overline{t}}\mathrel{{\rightarrow_{\partial}}}{\left\langle\sigma^{\prime}\right\rangle}\,{\overline{t}}$ as soon as $s\mathrel{{\rightarrow_{\partial}}}\sigma^{\prime}$;

• •

${\left\langle s\right\rangle}\,{\overline{t}}\mathrel{{\rightarrow_{\partial}}}{\left\langle s\right\rangle}\,{\overline{\tau}^{\prime}}$ as soon as $\overline{t}\mathrel{{\rightarrow_{\partial}}}\overline{\tau}^{\prime}$;

• •

${\left[s\right]}\cdot\overline{t}\mathrel{{\rightarrow_{\partial}}}{\left[\sigma^{\prime}\right]}\cdot\overline{t}$ as soon as $s\mathrel{{\rightarrow_{\partial}}}\sigma^{\prime}$.

We extend this reduction to finite sums of resource expressions: write $\epsilon\mathrel{{\rightarrow_{\partial}}}\epsilon^{\prime}$ if $\epsilon=\sum_{i=0}^{n}e_{i}$ and $\epsilon^{\prime}=\sum_{i=0}^{n}\epsilon^{\prime}_{i}$ with $e_{0}\mathrel{{\rightarrow_{\partial}}}\epsilon^{\prime}_{0}$ and, for all $i\in{\left\{1,\dotsc,n\right\}}$, $e_{i}\mathrel{{\rightarrow_{\partial}^{?}}}\epsilon^{\prime}_{i}$.

Observe that we allow for parallel reduction of any nonzero number of summands in a finite sum. This reduction is particularly well behaved. In particular, it is confluent in a strong sense:

Lemma \thethm.

For all $\epsilon,\epsilon_{0},\epsilon_{1}\in\mathbf{N}{\left[(\oc)\Delta\right]}$, if $\epsilon\mathrel{{\rightarrow_{\partial}}}\epsilon_{0}$ and $\epsilon\mathrel{{\rightarrow_{\partial}}}\epsilon_{1}$ then there is $\epsilon^{\prime}\in\mathbf{N}{\left[(\oc)\Delta\right]}$ such that $\epsilon_{0}\mathrel{{\rightarrow_{\partial}^{?}}}\epsilon^{\prime}$ and $\epsilon_{1}\mathrel{{\rightarrow_{\partial}^{?}}}\epsilon^{\prime}$.

Proof.

The proof follows a well-trodden path for proving confluence.

One first proves by induction on $s$ that if $s\mathrel{{\rightarrow_{\partial}}}\sigma^{\prime}$ then $\partial_{x}s\cdot\overline{t}\mathrel{{\rightarrow_{\partial}^{?}}}\partial_{x}\sigma^{\prime}\cdot\overline{t}$, and if $\overline{t}\mathrel{{\rightarrow_{\partial}}}\overline{\tau}^{\prime}$ then $\partial_{x}s\cdot\overline{t}\mathrel{{\rightarrow_{\partial}^{?}}}\partial_{x}s\cdot\overline{\tau}^{\prime}$. Note that the reflexive closure is made necessary by the possibility that $\partial_{x}s\cdot\overline{t}=0$, and the transitive closure is not needed because there is no duplication of the redexes of $\overline{t}$ in the summands of the multilinear substitution $\partial_{x}s\cdot\overline{t}$.

One then proves that if $e\mathrel{{\rightarrow_{\partial}}}\epsilon_{0}$ and $e\mathrel{{\rightarrow_{\partial}}}\epsilon_{1}$ then there is $\epsilon^{\prime}\in\mathbf{N}{\left[(\oc)\Delta\right]}$ such that $\epsilon_{0}\mathrel{{\rightarrow_{\partial}^{?}}}\epsilon^{\prime}$ and $\epsilon_{1}\mathrel{{\rightarrow_{\partial}^{?}}}\epsilon^{\prime}$. The proof is straightforward, by induction on the pair of reductions $e\mathrel{{\rightarrow_{\partial}}}\epsilon_{0}$ and $e\mathrel{{\rightarrow_{\partial}}}\epsilon_{1}$, using the previous result in case $e$ is a redex which is reduced in $\epsilon_{0}$ but not in $\epsilon_{1}$ (or vice versa). ∎

In other words, $\mathrel{{\rightarrow_{\partial}^{?}}}$ enjoys the diamond property.999 This strong confluence result was not mentioned in Ehrhard and Regnier’s papers about resource $\lambda$-calculus [ER08, ER06] but they established a very similar result for differential nets [ER05, Section 4]: Lemma 3.4 can be understood as a reformulation of the latter in the setting of resource calculus.

Moreover, the effect of reduction on the size of terms is very regular. First introduce some useful notation: write $e\succ_{\partial}e^{\prime}$ if $e\mathrel{{\rightarrow_{\partial}}}\epsilon^{\prime}$ with $e^{\prime}\in{\left|\epsilon^{\prime}\right|}$.

Lemma \thethm.

Let $e\succ_{\partial}e^{\prime}$. Then $\mathord{\mathbf{fv}}{\left(e^{\prime}\right)}=\mathord{\mathbf{fv}}{\left(e\right)}$, and $\mathord{\mathbf{s}}{\left(e^{\prime}\right)}+2\leq\mathord{\mathbf{s}}{\left(e\right)}\leq 2\mathord{\mathbf{s}}{\left(e^{\prime}\right)}+2$.

Proof.

By induction on the reduction $e\mathrel{{\rightarrow_{\partial}}}\epsilon^{\prime}$ with $e^{\prime}\in{\left|\epsilon^{\prime}\right|}$. The inductive contextuality cases are easy, and we only detail the base case, i.e. $e={\left\langle\lambda x\,{t}\right\rangle}\,{\overline{u}}$ and $\epsilon^{\prime}=\partial_{x}t\cdot\overline{u}$.

Write $n=\mathbf{n}_{x}{\left(t\right)}$. The result then follows from Lemma 3.3, observing that $\mathord{\mathbf{s}}{\left(e^{\prime}\right)}=\mathord{\mathbf{s}}{\left(t\right)}+\mathord{\mathbf{s}}{\left(\overline{u}\right)}-n=\mathord{\mathbf{s}}{\left(e\right)}-2-n$ and $n\leq\mathord{\mathbf{s}}{\left(\overline{u}\right)}\leq\mathord{\mathbf{s}}{\left(e^{\prime}\right)}$. ∎

We will write $\geq_{\partial}$ (resp. $>_{\partial}$) for $\succ_{\partial}^{*}$ (resp. $\succ_{\partial}^{+}$). Observe that $e\geq_{\partial}e^{\prime}$ (resp. $e>_{\partial}e^{\prime}$) iff there is $\epsilon^{\prime}\in\mathbf{N}{\left[(\oc)\Delta\right]}$ such that $e^{\prime}\in{\left|\epsilon^{\prime}\right|}$ and $e\mathrel{{\rightarrow_{\partial}^{*}}}\epsilon^{\prime}$ (resp. $e\mathrel{{\rightarrow_{\partial}^{+}}}\epsilon^{\prime}$). Moreover, ${\left\{e^{\prime}\mathrel{;}e\geq_{\partial}e^{\prime}\right\}}$ is always finite and $>_{\partial}$ defines a well-founded strict partial order. A direct consequence is that $\mathrel{{\rightarrow_{\partial}}}$ always converges to a unique normal form:

Lemma \thethm.

The reduction $\mathrel{{\rightarrow_{\partial}}}$ is confluent and strongly normalizing. Moreover, for all $\epsilon\in\mathbf{N}{\left[(\oc)\Delta\right]}$, the set ${\left\{\epsilon^{\prime}\mathrel{;}\epsilon\mathrel{{\rightarrow_{\partial}^{*}}}\epsilon^{\prime}\right\}}$ is finite.

Proof.

Confluence is a consequence of Lemma 3.4. By Lemma 3.4, the transitive closure $\succ_{\partial}^{+}$ is a well-founded strict partial order. Observe that the elements of $\mathbf{N}{\left[(\oc)\Delta\right]}$ can be considered as finite multisets of resource expressions: then $\mathrel{{\rightarrow_{\partial}^{+}}}$ is included in the multiset ordering induced by $\succ_{\partial}^{+}$, and it follows that $\mathrel{{\rightarrow_{\partial}^{+}}}$ defines a well-founded strict partial order on $\mathbf{N}{\left[(\oc)\Delta\right]}$, i.e. $\mathrel{{\rightarrow_{\partial}}}$ is strongly normalizing.

The final property follows from strong normalizability applying König’s lemma to the tree of possible reductions, observing that each $\epsilon$ has finitely many $\mathrel{{\rightarrow_{\partial}}}$-reducts. ∎

If $\epsilon\in\mathbf{N}{\left[(\oc)\Delta\right]}$, we then write $\mathord{\mathsf{NF}}{\left(\epsilon\right)}$ for the unique sum of normal resource expressions such that $\epsilon\mathrel{{\rightarrow_{\partial}^{*}}}\mathord{\mathsf{NF}}{\left(\epsilon\right)}$. A consequence of the previous lemma is that any reduction discipline reaches this normal form:

Corollary \thethm.

Let $\mathord{\to}\subseteq\mathbf{N}{\left[(\oc)\Delta\right]}\times\mathbf{N}{\left[(\oc)\Delta\right]}$ be such that $\mathord{\to}\subseteq\mathord{\mathrel{{\rightarrow_{\partial}^{*}}}}$. Moreover assume that, for all non normal $\epsilon\in\mathbf{N}{\left[(\oc)\Delta\right]}$ there is $\epsilon^{\prime}\not=\epsilon$ such that $\epsilon\to\epsilon^{\prime}$. Then $\epsilon\to^{*}\mathord{\mathsf{NF}}{\left(\epsilon\right)}$ for all $\epsilon\in\mathbf{N}{\left[(\oc)\Delta\right]}$.

4. Vectors of resource expressions and Taylor expansion of algebraic $\lambda$-terms

4.1. Resource vectors

A vector $\sigma=\sum_{s\in\Delta}\sigma_{s}.s$ of resource terms will be called a term vector whenever its set of free variables $\mathord{\mathbf{fv}}{\left(\sigma\right)}\mathrel{\mathord{:}\mathord{=}}\bigcup_{s\in{\left|\sigma\right|}}\mathord{\mathbf{fv}}{\left(s\right)}$ is finite. Similarly, we will call monomial vector any vector of resource monomials whose set of free variables is finite. We will abuse notation and write $\mathbf{S}^{\Delta}$ for the set of term vectors and $\mathbf{S}^{\oc\Delta}$ for the set of monomial vectors.101010 The restriction to vectors with finitely many free variables is purely technical. For instance, it allows us to assume that a sum of abstractions $\sigma=\sum_{i\in I}\lambda x_{i}\,{s_{i}}$ can always use a common abstracted variable: $\sigma=\sum_{i\in I}\lambda x\,{\left(s_{i}{\left[x/x_{i}\right]}\right)}$, with $x\not\in\mathbin{\cup}_{i\in I}\mathord{\mathbf{fv}}{\left(\lambda x_{i}\,{s_{i}}\right)}$. Working without this restriction would only lead to more contorted statements and tedious bookkeeping: consider, e.g., what would happen to the definition of the substitution of a term vector for a variable (Definition 4.3), especially the abstraction case.

A resource vector will be any of a term vector or a monomial vector, and we will write $\mathbf{S}^{(\oc)\Delta}$ for either $\mathbf{S}^{\Delta}$ or $\mathbf{S}^{\oc\Delta}$: as for resource expressions, whenever we use this notation several times in the same context, all occurrences consistently denote the same set.

The syntactic constructs are extended to resource vectors by linearity: for all $\sigma\in\mathbf{S}^{\Delta}$ and $\overline{\sigma},\overline{\tau}\in\mathbf{S}^{\oc\Delta}$, we set

[TABLE]

This poses no problem for finite vectors: e.g., if ${\left|\sigma\right|}$ is finite then finitely many of the vectors $\sigma_{s}.\lambda x\,{s}$ are non-zero, hence the sum is finite. In the general case, however, we actually need to prove that the above sums are well defined: the constructors of the calculus define summable functions, which thus extend to multilinear-continuous maps.111111 The one-to-one correspondence between summable $n$-ary functions and multilinear-continuous maps was established for semimodules of the form $\mathbf{S}^{X}$, i.e. the semimodules of all vectors on a fixed set. Due to the restriction we put on free variables, $\mathbf{S}^{(\oc)\Delta}$ is not of this form: it should rather be written $\bigcup_{V\in\mathord{\mathfrak{P}_{f}}{\left(\mathcal{V}\right)}}\mathbf{S}^{(\oc)\Delta_{V}}$ where $(\oc)\Delta_{V}\mathrel{\mathord{:}\mathord{=}}{\left\{e\in(\oc)\Delta\mathrel{;}\mathord{\mathbf{fv}}{\left(e\right)}\subseteq V\right\}}$. So when we say a function is multilinear-continuous on $\mathbf{S}^{(\oc)\Delta}$, we actually mean that its restriction to each $\mathbf{S}^{(\oc)\Delta_{V}}$ with $V\in\mathord{\mathfrak{P}_{f}}{\left(\mathcal{V}\right)}$ is multilinear-continuous. In the present case, keeping this precision implicit is quite innocuous, but we will be more careful when considering the restriction to bounded vectors in Subsection 6.4, and to normalizable vectors in Section 8.

Lemma \thethm.

The following families of vectors are summable:

[TABLE]

Proof.

The proof is direct, but we detail it if only to make the requirements explicit.

For all $u\in\Delta$ there is at most one $s$ such that $u\in{\left|\lambda x\,{s}\right|}$ (in which case $u=\lambda x\,{s}$) and at most one pair $(s,\overline{t})$ such that $u\in{\left|{\left\langle s\right\rangle}\,{\overline{t}}\right|}$ (in which case $u={\left\langle s\right\rangle}\,{\overline{t}}$).

For all $\overline{u}\in\oc\Delta$ there is at most one $s$ such that $\overline{u}\in{\left|{\left[s\right]}\right|}$ (in which case $\overline{u}={\left[s\right]}$), and there are finitely many $\overline{s}$ and $\overline{t}$ such that $\overline{u}\in{\left|{\overline{s}\cdot{\overline{t}}}\right|}$ (those such that $\overline{u}=\overline{s}\cdot\overline{t}$). ∎

For each term vector $\sigma$, we then write $\sigma^{n}$ for the monomial vector

[TABLE]

4.2. Partial differentiation of resource vectors.

We can extend partial derivatives to vectors by linear-continuity (recall that, via the unique semiring morphism from $\mathbf{N}$ to $\mathbf{S}$, we can consider that $\mathbf{N}{\left[(\oc)\Delta\right]}\subseteq\mathbf{S}^{(\oc)\Delta}$).

Lemma \thethm.

The function

[TABLE]

is summable.

Proof.

Let $e^{\prime}\in(\oc)\Delta$ and assume that $e^{\prime}\in{\left|\frac{\partial^{n}e}{\partial x^{n}}\cdot\overline{s}\right|}$ with $\mathord{\#}{\overline{s}}=n$. By Lemma 3.2, $\mathord{\mathbf{fv}}{\left(e\right)}\subseteq\mathord{\mathbf{fv}}{\left(e^{\prime}\right)}\mathbin{\cup}{\left\{x\right\}}$, $\mathord{\mathbf{fv}}{\left(\overline{s}\right)}\subseteq\mathord{\mathbf{fv}}{\left(e^{\prime}\right)}$, $\mathord{\mathbf{s}}{\left(e\right)}\leq\mathord{\mathbf{s}}{\left(e^{\prime}\right)}$ and $\mathord{\mathbf{s}}{\left(\overline{s}\right)}\leq\mathord{\mathbf{s}}{\left(e^{\prime}\right)}$: $e^{\prime}$ being fixed, there are finitely many $(e,\overline{s})$ satisfying these constraints. ∎

The characterization of iterated partial derivatives given in Lemma 3.2 extends directly to resource vectors, by the linear-continuity of syntactic constructs and partial derivatives. For instance, given term vectors $\sigma,\rho_{1},\dotsc,\rho_{n}\in\mathbf{S}^{\Delta}$ and a monomial vector $\overline{\tau}\in\mathbf{S}^{\oc\Delta}$, we obtain:

[TABLE]

Now we can consider iterated differentiation along a fixed term vector $\rho$: $\frac{\partial^{n}\epsilon}{\partial x^{n}}\cdot\rho^{n}$. We obtain:

Lemma \thethm.

For all $\sigma,\tau_{1},\dotsc,\tau_{n},\rho\in\mathbf{S}^{\Delta}$ and all $\overline{\tau}\in\mathbf{S}^{\oc\Delta}$,

[TABLE]

Proof.

First recall that, if $k=\sum_{i=1}^{n}k_{i}$, the multinomial coefficient ${\left[\genfrac{}{}{0.0pt}{}{k}{k_{1},\dotsc,k_{n}}\right]}\mathrel{\mathord{:}\mathord{=}}\frac{k!}{\prod_{i=1}^{n}k_{i}!}$ is nothing but the number of partitions of ${\left\{1,\dotsc,k\right\}}$ into $n$ sets $I_{1},\dotsc,I_{n}$ such that $\mathord{\#}{I}_{j}=k_{j}$ for $1\leq j\leq n$ [DLMF, §26.4]. Then both results derive directly from Lemma 3.2. ∎

4.3. Substitutions

Since ${\left|\partial_{x}e\cdot\overline{s}\right|}\subseteq{\left|\frac{\partial^{n}e}{\partial x^{n}}\cdot\overline{s}\right|}$, multilinear substitution also defines a summable binary function and we will write

[TABLE]

By contrast with partial derivatives, the usual substitution is not linear, so the substitution of resource vectors must be defined directly.

Definition \thethm.

We define by induction over resource expressions the substitution $e{\left[\sigma/x\right]}\in\mathbf{S}^{(\oc)\Delta}$ of $\sigma\in\mathbf{S}^{\Delta}$ for a variable $x$ in $e\in(\oc)\Delta$:

[TABLE]

Lemma \thethm.

For all $e\in(\oc)\Delta$, $x\in\mathcal{V}$ and $\sigma\in\mathbf{S}^{\Delta}$:

• •

if $\sigma\in\Delta$ then $e{\left[\sigma/x\right]}\in\Delta$;

• •

if $\sigma\in\mathbf{S}{\left[\Delta\right]}$ then $e{\left[\sigma/x\right]}\in\mathbf{S}{\left[(\oc)\Delta\right]}$;

• •

if $x\not\in\mathord{\mathbf{fv}}{\left(e\right)}$ then $e{\left[\sigma/x\right]}=e$;

• •

if $x\in\mathord{\mathbf{fv}}{\left(e\right)}$ then $e{\left[0/x\right]}=0$;

• •

for all $e^{\prime}\in{\left|e{\left[\sigma/x\right]}\right|}$, $\mathord{\mathbf{fv}}{\left(e\right)}\setminus{\left\{x\right\}}\subseteq\mathord{\mathbf{fv}}{\left(e^{\prime}\right)}\subseteq{\left(\mathord{\mathbf{fv}}{\left(e\right)}\setminus{\left\{x\right\}}\right)}\mathbin{\cup}\mathord{\mathbf{fv}}{\left(\sigma\right)}$ and $\mathord{\mathbf{s}}{\left(e^{\prime}\right)}\geq\mathord{\mathbf{s}}{\left(e\right)}$.

Proof.

Each statement follows easily by induction on $e$. ∎

A consequence of the last item is that the function

[TABLE]

is summable: we thus write

[TABLE]

4.4. Promotion

Observe that the family ${\left(\sigma^{n}\right)}_{n\in\mathbf{N}}$ is summable because the supports ${\left|\sigma^{n}\right|}$ for $n\in\mathbf{N}$ are pairwise disjoint. We then define the promotion of $\sigma$ as ${\sigma}^{\oc}\mathrel{\mathord{:}\mathord{=}}\sum_{n\in\mathbf{N}}\frac{1}{n!}.\sigma^{n}$.

For this definition to make sense, we need inverses of natural numbers to be available: we say $\mathbf{S}$ has fractions if every $n\in\mathbf{N}\setminus{\left\{0\right\}}$ admits a multiplicative inverse in $\mathbf{S}$. This inverse is necessarily unique and we write it $\frac{1}{n}$. Observe that $\mathbf{S}$ has fractions iff there is a semiring morphism from the semiring $\mathbf{Q}^{+}$ of non-negative rational numbers to $\mathbf{S}$, and then this morphism is unique, but not necessarily injective: consider the semiring $\mathbf{B}$ of booleans. Semifields, i.e. commutative semirings in which every non-zero element admits an inverse, obviously have fractions: $\mathbf{Q}^{+}$ and $\mathbf{B}$ are actually semifields. In the following, we will keep this requirement implicit: whenever we use quotients by natural numbers, it means we assume $\mathbf{S}$ has fractions.

Lemma \thethm.

For all $\sigma$ and $\tau\in\mathbf{S}^{\Delta}$, ${\sigma}^{\oc}{\left[\tau/x\right]}={\left(\sigma{\left[\tau/x\right]}\right)}^{\oc}$.

Proof.

By the linear-continuity of $\epsilon\mapsto\epsilon{\left[\sigma/x\right]}$, it is sufficient to prove that

[TABLE]

which follows from the $n$-linear-continuity of $(\sigma_{1},\dotsc,\sigma_{n})\mapsto{\left[\sigma_{1},\dotsc,\sigma_{n}\right]}$ and the definition of substitution. ∎

Lemma \thethm.

The following identities hold:

[TABLE]

Proof.

Since each syntactic constructor is multilinear-continuous, it is sufficient to consider the case of $\partial_{x}e\cdot{\rho}^{\oc}$ for a resource expression $e\in(\oc)\Delta$. First observe that, if $k=\mathbf{n}_{x}{\left(e\right)}$ then $\partial_{x}e\cdot{\rho}^{\oc}=\frac{1}{k!}.{\frac{\partial^{k}e}{\partial x^{k}}\cdot\rho^{k}}$. In particular the case of variables is straightforward.

The case of abstractions follows directly, since $\frac{\partial^{k}\lambda x\,{s}}{\partial x^{k}}\cdot\rho^{k}=\lambda x\,{\left(\frac{\partial^{k}s}{\partial x^{k}}\cdot\rho^{k}\right)}$.

If $e={\left\langle s\right\rangle}\,{\overline{t}}$, write $l=\mathbf{n}_{x}{\left(s\right)}$ and $m=\mathbf{n}_{x}{\left(\overline{t}\right)}$. It follows from Lemma 4.2 that $\partial_{x}e\cdot\rho^{k}={\left[\genfrac{}{}{0.0pt}{}{k}{l,m}\right]}.{\left\langle\partial_{x}s\cdot\rho^{l}\right\rangle}\,{\partial_{x}\overline{t}\cdot\rho^{m}}$ and then $\frac{1}{k!}.\partial_{x}e\cdot\rho^{k}={\left\langle\frac{1}{l!}.\partial_{x}s\cdot\rho^{l}\right\rangle}\,{\frac{1}{m!}.\partial_{x}\overline{t}\cdot\rho^{m}}$.

Similarly, if $e={\left[t_{1},\dotsc,t_{n}\right]}$, write $k_{i}=\mathbf{n}_{x}{\left(t_{i}\right)}$ for all $i\in{\left\{1,\dotsc,n\right\}}$. It follows from Lemma 4.2 that $\partial_{x}e\cdot\rho^{k}={\left[\genfrac{}{}{0.0pt}{}{k}{k_{1},\dotsc,k_{n}}\right]}.{\left[\partial_{x}t_{1}\cdot\rho^{k_{1}},\dotsc,\partial_{x}t_{n}\cdot\rho^{k_{n}}\right]}$ and then $\frac{1}{k!}.\partial_{x}e\cdot\rho^{k}={\left[\frac{1}{k_{1}!}\partial_{x}t_{1}\cdot\rho^{k_{1}},\dotsc,\frac{1}{k_{n}!}\partial_{x}t_{n}\cdot\rho^{k_{n}}\right]}$. ∎

Lemma \thethm.

For all $\epsilon\in\mathbf{S}^{(\oc)\Delta}$ an $\sigma\in\mathbf{S}^{\Delta}$,

[TABLE]

Proof.

By the linear-continuity of $\epsilon\mapsto\partial_{x}\epsilon\cdot{\sigma}^{\oc}$ and $\epsilon\mapsto\epsilon{\left[\sigma/x\right]}$, it is sufficient to show that

[TABLE]

for all resource expression $e$. The proof is then by induction on $e$, using the previous Lemma in each case. ∎

By Lemma 4.4, we thus obtain

[TABLE]

which can be seen as a counterpart of the functoriality of promotion in linear logic. To our knowledge it is the first published proof of such a result for resource vectors. This will enable us to prove the commutation of Taylor expansion and substitution (Lemma 4.5), another unsurprising yet non-trivial result.

4.5. Taylor expansion of algebraic $\lambda$-terms

Since resource vectors form a module, there is no reason to restrict the source language of Taylor expansion to the pure $\lambda$-calculus: we can consider formal finite linear combinations of $\lambda$-terms.

We will thus consider the terms given by the following grammar:

[TABLE]

where $a$ ranges in $\mathbf{S}$.121212We follow Krivine’s convention [Kri90], by writing ${\left(M\right)}\,{N}$ for the application of term $M$ to term $N$. We more generally write ${\left(M\right)}\,{N_{1}\cdots N_{k}}$ for ${\left(\cdots{\left(M\right)}\,{N_{1}}\cdots\right)}\,{N_{k}}$. Moreover, among term constructors, we give sums the lowest priority so that ${\left(M\right)}\,{N}+P$ should be read as ${\left({\left(M\right)}\,{N}\right)}+P$ rather than ${\left(M\right)}\,{{\left(N+P\right)}}$.

For now, terms are considered up to the usual $\alpha$-equivalence only: the null term [math], scalar multiplication $a.M$ and sum of terms $M+N$ are purely syntactic constructs.

Definition \thethm.

We define the Taylor expansion $\mathord{\tau}{\left(M\right)}\in\mathbf{S}^{(\oc)\Delta}$ of a term $M\in\Sigma_{\mathbf{S}}$ inductively as follows:

[TABLE]

Lemma \thethm.

For all $M,N\in\Sigma_{\mathbf{S}}$, and all variable $x$,

[TABLE]

Proof.

By induction on $M$, using Lemmas 4.4 and 4.4. ∎

Let us insist on the fact that, despite its very simple and unsurprising statement, the previous lemma relies on the entire technical development of the previous subsections. Again, to our knowledge, it is the first proof that Taylor expansion commutes with substitution, in an untyped and non-uniform setting, without any additional assumption.

By contrast, one can forget everything about the semiring of coefficients and consider only the support of Taylor expansion. Recall that $\mathbf{B}$ denotes the semiring of booleans. Then we can consider that $\mathbf{B}^{(\oc)\Delta}=\mathord{\mathfrak{P}}{\left((\oc)\Delta\right)}$ and write, e.g., $\lambda x\,{\mathcal{S}}={\left\{\lambda x\,{s}\mathrel{;}s\in\mathcal{S}\right\}}$ for all set $\mathcal{S}$ of resource terms.

Definition \thethm.

The Taylor support $\mathord{\mathcal{T}}{\left(M\right)}\subseteq\Delta$ of $M\in\Sigma_{\mathbf{S}}$ is defined inductively as follows:131313 One might be tempted to make an exception in case $a=0$ and set $\mathord{\mathcal{T}}{\left(0.M\right)}=\emptyset$ but this would only complicate the definition and further developments for little benefit: what about $\mathord{\mathcal{T}}{\left(a.M+b.M\right)}$ (resp. $\mathord{\mathcal{T}}{\left(a.b.M\right)}$) in a semiring where $a\not=0$, $b\not=0$ and $a+b=0$ (resp. $ab=0$)? If we try and cope with those too, we are led to make $\mathord{\mathcal{T}}$ invariant under the equations of $\mathbf{S}$-module, which is precisely what we want to avoid here: see the case of $\mathord{\tau}$ in the remaining of the present section.

[TABLE]

It should be clear that ${\left|\mathord{\tau}{\left(M\right)}\right|}\subseteq\mathord{\mathcal{T}}{\left(M\right)}$, but the inclusion might be strict, if only because $\mathord{\mathcal{T}}{\left(0.M\right)}=\mathord{\mathcal{T}}{\left(M\right)}$. By contrast with the technicality of the previous subsection, the following qualitative analogue of Lemma 4.5 is easily established:

Lemma \thethm.

For all $M,N\in\Sigma_{\mathbf{S}}$, and all variable $x$,

[TABLE]

Proof.

The qualitative version of Lemma 4.4 is straightforward. The result follows by induction on $M$. ∎

The restriction of $\mathord{\mathcal{T}}$ to the set $\Lambda$ of pure $\lambda$-terms was used by Ehrhard and Regnier [ER08] in their study of Taylor expansion. They showed that if $M\in\Lambda$ then $\mathord{\mathcal{T}}{\left(M\right)}$ is uniform: all the resource terms in $\mathord{\mathcal{T}}{\left(M\right)}$ have the same outermost syntactic construct and this property is preserved inductively on subterms. They moreover proved that $\mathord{\tau}{\left(M\right)}$, and in fact $M$ itself, is entirely characterized by $\mathord{\mathcal{T}}{\left(M\right)}$: in this case, $\mathord{\tau}{\left(M\right)}=\sum_{s\in\mathord{\mathcal{T}}{\left(M\right)}}\frac{1}{m(s)}s$ where $m(s)$ is an integer coefficient depending only on $s$. Of course this property fails in the non uniform setting of $\Sigma_{\mathbf{S}}$.

Now, let us consider the equivalence induced on terms by Taylor expansion: write $M\simeq_{\mathord{\tau}}N$ if $\mathord{\tau}{\left(M\right)}=\mathord{\tau}{\left(N\right)}$.

Lemma \thethm.

The following equations hold:

[TABLE]

Moreover, $\simeq_{\mathord{\tau}}$ is compatible with syntactic constructs: if $M\simeq_{\mathord{\tau}}M^{\prime}$ then $\lambda x\,{M}\simeq_{\mathord{\tau}}\lambda x\,{M}^{\prime}$, ${\left(M\right)}\,{N}\simeq_{\mathord{\tau}}{\left(M^{\prime}\right)}\,{N}$, ${\left(N\right)}\,{M}\simeq_{\mathord{\tau}}{\left(N\right)}\,{M^{\prime}}$, $a.M\simeq_{\mathord{\tau}}a.M^{\prime}$, $M+N\simeq_{\mathord{\tau}}M^{\prime}+N$ and $N+M\simeq_{\mathord{\tau}}N+M^{\prime}$.

Proof.

Up to Taylor expansion, these equations reflect the fact that $\mathbf{S}^{(\oc)\Delta}$ forms a semimodule (first three lines), and that all the constructions used in the definition of $\mathord{\tau}$ are multilinear-continuous, except for promotion (last two lines). Compatibility follows from the inductive definition of $\mathord{\tau}$. ∎

Let us write $\simeq_{\mathrm{v}}$ for the least compatible equivalence relation containing the equations of the previous lemma, and call vector $\lambda$-terms the elements of the quotient $\mathord{\mathord{\Sigma_{\mathbf{S}}}/\mathord{\simeq_{\mathrm{v}}}}$: these are the terms of the previously studied algebraic $\lambda$-calculus [Vau09, Alb14].141414 In those previous works, the elements of $\mathord{\mathord{\Sigma_{\mathbf{S}}}/\mathord{\simeq_{\mathrm{v}}}}$ were called algebraic $\lambda$-terms, but here we reserve this name for another, simpler, notion.

It is clear that $\mathord{\mathord{\Sigma_{\mathbf{S}}}/\mathord{\simeq_{\mathrm{v}}}}$ forms a $\mathbf{S}$-semimodule. In fact, one can show [Vau09] that $\mathord{\mathord{\Sigma_{\mathbf{S}}}/\mathord{\simeq_{\mathrm{v}}}}$ is freely generated by the $\simeq_{\mathrm{v}}$-equivalence classes of base terms, i.e. those described by the following grammar:

[TABLE]

Hence we could write $\mathord{\mathord{\Sigma_{\mathbf{S}}}/\mathord{\simeq_{\mathrm{v}}}}=\mathbf{S}{\left[\mathord{\mathord{\Sigma_{\mathbf{S}}^{\mathrm{b}}}/\mathord{\simeq_{\mathrm{v}}}}\right]}$.

Notice however that Taylor expansion is not injective on vector $\lambda$-terms in general.

Example \thethm.

We can consider that $\mathord{\mathord{\Sigma_{\mathbf{B}}}/\mathord{\simeq_{\mathrm{v}}}}=\mathord{\mathfrak{P}_{f}}{\left(\mathord{\mathord{\Sigma_{\mathbf{B}}^{\mathrm{b}}}/\mathord{\simeq_{\mathrm{v}}}}\right)}$ and $\mathord{\tau}{\left(M\right)}\subseteq\Delta$ for all $M\in\Sigma_{\mathbf{B}}$. It is then easy to check that, e.g., $\mathord{\tau}{\left({\left(x\right)}\,{\emptyset}\right)}\subseteq\mathord{\tau}{\left({\left(x\right)}\,{x}\right)}$, hence ${\left(x\right)}\,{\emptyset}+_{\mathbf{B}}{\left(x\right)}\,{x}\simeq_{\mathord{\tau}}{\left(x\right)}\,{x}$.151515 This discrepancy is also present in the non-deterministic Böhm trees of de’Liguoro and Piperno [dLP95]: in that qualitative setting, they can solve it by introducing a preorder on trees based on set inclusion. They moreover show that this preorder coincides with that induced by a well chosen domain theoretic model, as well as with the observational preorder associated with must-solvability. This preorder should be related with that induced by the inclusion of normal forms of Taylor expansions (which are always defined since we then work with support sets rather than general vectors).

This contrasts with the case of pure $\lambda$-terms, for which $\mathord{\tau}$ is always injective: in this case, it is in fact sufficient to look at the linear resource terms in supports of Taylor expansions.

Fact 1**.**

For all $M,N\in\Lambda$, $\mathord{\ell}{\left(M\right)}\in{\left|\mathord{\tau}{\left(N\right)}\right|}$ iff $M=N$, where $\mathord{\ell}$ is defined inductively as follows:

[TABLE]

To our knowledge, finding sufficient conditions on $\mathbf{S}$ ensuring that $\mathord{\tau}$ becomes injective on $\mathord{\mathord{\Sigma_{\mathbf{S}}}/\mathord{\simeq_{\mathrm{v}}}}$ is still an open question.

Observe moreover that the $\mathbf{S}$-semimodule structure of $\mathord{\mathord{\Sigma_{\mathbf{S}}}/\mathord{\simeq_{\mathrm{v}}}}$ gets in the way when we want to study $\beta$-reduction and normalization: it is well known [Vau07, AD08, Vau09] that $\beta$-reduction in a semimodule of terms is inconsistent in presence of negative coefficients.

Example 4.1**.**

Consider $\delta_{M}\mathrel{\mathord{:}\mathord{=}}\lambda x\,{\left(M+{\left(x\right)}\,{x}\right)}$ and $\infty_{M}\mathrel{\mathord{:}\mathord{=}}{\left(\delta_{M}\right)}\,{\delta_{M}}$. Observe that $\infty_{M}$ $\beta$-reduces to $M+\infty_{M}$. Suppose $\mathbf{S}$ is a ring. Then any congruence $\simeq$ on $\Sigma_{\mathbf{S}}$ containing $\beta$-reduction and the equations of $\mathbf{S}$-module is inconsistent: $0\simeq\infty_{M}+(-1).\infty_{M}\simeq(M+\infty_{M})+(-1).\infty_{M}\simeq M$.

The problem is of course the identity $0\simeq\infty_{M}+(-1).\infty_{M}$. Another difficulty is that, if $\mathbf{S}$ has fractions then, up to $\mathbf{S}$-semimodule equations, one can split a single $\beta$-reduction step into infinitely many fractional steps: if $M\mathrel{{\rightarrow_{\beta}}}M^{\prime}$ then

[TABLE]

It is not our purpose here to explore the various possible fixes to the rewriting theory of $\beta$-reduction on vector $\lambda$-terms. We rather refer the reader to the literature on algebraic $\lambda$-calculi [Vau09, AD08, Alb14, DC11] for various proposals. Our focus being on Taylor expansion, we propose to consider vector $\lambda$-terms as intermediate objects: the reduction relation induced on resource vectors by $\beta$-reduction through Taylor expansion contains $\beta$-reduction on vector terms — which is mainly useful to understand what may go wrong.

We still need to introduce some form of quotient in the syntax, though, if only to allow formal sums to retain a computational meaning: otherwise, for instance, no $\beta$-redex can be fired in ${\left(\lambda x\,{M}+\lambda x\,{N}\right)}\,{P}$; and more generally there are $\beta$-normal terms whose Taylor expansion is not normal, and conversely (consider, e.g., ${\left(\lambda x\,{0}\right)}\,{P}$).

Write $\Lambda_{\mathbf{S}}$ for the quotient of $\Sigma_{\mathbf{S}}$ by the least compatible equivalence $\simeq_{+}$ containing the following six equations:

[TABLE]

We call algebraic $\lambda$-terms the elements of $\Lambda_{\mathbf{S}}$. We will abuse notation and denote an algebraic $\lambda$-term by any of its representatives.

Observe that $\mathord{\mathcal{T}}{\left(M\right)}$ is preserved under $\simeq_{+}$ so it is well defined on algebraic terms, although not on vector terms.

Fact 2**.**

An algebraic $\lambda$-term $M$ is $\beta$-normal (i.e. each of its representatives is $\beta$-normal) iff $\mathord{\mathcal{T}}{\left(M\right)}$ contains only normal resource terms.

We do not claim that $\simeq_{+}$ is minimal with the above property (for this, the bottom three equations are sufficient) but it is quite natural for anyone familiar with the decomposition of $\lambda$-calculus in linear logic, as it reflects the linearity of $\lambda$-abstraction and the function position in an application. Moreover it retains the two-level structure of vector $\lambda$-terms, seen as sums of base terms.

It is indeed a routine exercise to show that orienting the defining equations of $\simeq_{+}$ from left to right defines a confluent and terminating rewriting system. We call canonical terms the normal forms of this system, which we can describe as follows. The sets $\Sigma_{\mathbf{S}}^{\mathrm{c}}$ of canonical terms and $\Sigma^{\mathrm{s}}_{\mathbf{S}}$ of simple canonical terms are mutually generated by the following grammars:

[TABLE]

so that each algebraic term $M$ admits a unique canonical $\simeq_{+}$-representative.

In the remaining of this paper we will systematically identify algebraic terms with their canonical representatives and keep $\simeq_{+}$ implicit. Moreover, we write $\Lambda^{\mathrm{s}}_{\mathbf{S}}$ for the set of simple algebraic $\lambda$-terms, i.e. those that admit a simple canonical representative.

Fact 3**.**

Every simple term $S\in\Lambda^{\mathrm{s}}_{\mathbf{S}}$ is of one of the following two forms:

• •

$S=\lambda x_{1}\,{\cdots\lambda x_{n}\,{{\left(x\right)}\,{M_{1}\cdots M_{k}}}}$: $S$ is a head normal form;

• •

$S=\lambda x_{1}\,{\cdots\lambda x_{n}\,{{\left(\lambda x\,{T}\right)}\,{M_{0}\cdots M_{k}}}}$: ${\left(\lambda x\,{T}\right)}\,{M_{0}}$ is the head redex of $S$.

So each algebraic $\lambda$-term can be considered as a formal linear combination of head normal forms and head reducible simple terms, which will structure the notions of weak solvability and hereditarily determinable terms in section 9.

5. On the reduction of resource vectors

Observe that

[TABLE]

and

[TABLE]

In order to simulate $\beta$-reduction through Taylor expansion we might be tempted to consider the reduction given by $\epsilon\to\epsilon^{\prime}$ as soon as $\epsilon=\sum_{i\in I}a_{i}.e_{i}$ and $\epsilon^{\prime}=\sum_{i\in I}a_{i}.\epsilon^{\prime}_{i}$ with $e_{i}\mathrel{{\rightarrow_{\partial}}}\epsilon^{\prime}_{i}$ for all $i\in I$.161616 We must of course require that $\bigcup_{i\in I}\mathord{\mathbf{fv}}{\left(e_{i}\right)}$ is finite but, again, we will keep such requirements implicit in the following.

Observe indeed that, as soon as ${\left(a_{i}.e_{i}\right)}_{i\in I}\in(\oc)\Delta$ is summable (i.e. for all $e\in(\oc)\Delta$, there are finitely many $i\in I$ such that $a_{i}\not=0$ and $e_{i}=e$), the family ${\left(a_{i}.\epsilon^{\prime}_{i}\right)}_{i\in I}$ is summable too: if $e^{\prime}\in{\left|a_{i}.\epsilon^{\prime}_{i}\right|}$ then $a_{i}\not=0$ and $e^{\prime}\in{\left|\epsilon^{\prime}_{i}\right|}$ hence by Lemma 3.4, $\mathord{\mathbf{fv}}{\left(e_{i}\right)}=\mathord{\mathbf{fv}}{\left(e^{\prime}\right)}$ and $\mathord{\mathbf{s}}{\left(e_{i}\right)}\leq 2\mathord{\mathbf{s}}{\left(e^{\prime}\right)}+2$; $e^{\prime}$ being fixed, there are thus finitely many possible values for $e_{i}$ hence for $i$. So we do not need any additional condition for this reduction step to be well defined.

This reduction, however, is not suitable for simulating $\beta$-reduction because whenever the reduced $\beta$-redex is not in linear position, we need to reduce arbitrarily many resource redexes.

Example 5.1**.**

Observe that

[TABLE]

and

[TABLE]

Then the reduction from ${\left[{\left\langle\lambda x\,{x}\right\rangle}\,{z^{k_{1}}},\dotsc,{\left\langle\lambda x\,{x}\right\rangle}\,{z^{k_{n}}}\right]}$ to $z^{n}$ if each $k_{i}=1$ (resp. to [math] if one $k_{i}\not=1$) requires firing $n$ independent redexes (resp. one of those $n$ redexes).

5.1. Parallel resource reduction

One possible fix would be to replace $\mathrel{{\rightarrow_{\partial}}}$ with $\mathrel{{\rightarrow_{\partial}^{*}}}$ in the above definition, i.e. set $\epsilon\to\epsilon^{\prime}$ as soon as $\epsilon=\sum_{i\in I}a_{i}.e_{i}$ and $\epsilon^{\prime}=\sum_{i\in I}a_{i}.\epsilon^{\prime}_{i}$ with $e_{i}\mathrel{{\rightarrow_{\partial}^{*}}}\epsilon^{\prime}_{i}$ for all $i\in I$, but then the study of the reduction subsumes that of normalization, which we treat in Section 8, and this relies on the possibility to simulate $\beta$-reduction steps.

A reasonable middle ground is to consider a parallel variant $\mathrel{{\Rightarrow_{\partial}}}$ of $\mathrel{{\rightarrow_{\partial}}}$, where any number of redexes can be reduced simultaneously in one step. The parallelism involved in the translation of a $\beta$-reduction step is actually quite constrained: like in the previous example, the redexes that need to be reduced in the Taylor expansion are always pairwise independent and no nesting is involved. However, in order to prove the confluence of the reduction on resource vectors, or its conservativity w.r.t. $\beta$-reduction, it is much more convenient to work with a fully parallel reduction relation, both on algebraic $\lambda$-terms and on resource vectors. Indeed, parallel reduction relations generally allow, e.g., to close confluence diagrams in one step or to define a maximal parallel reduction step: the relevance of this technical choice will be made clear all through Section 6.

Definition 5.2**.**

We define parallel resource reduction $\mathord{\mathrel{{\Rightarrow_{\partial}}}}\subseteq(\oc)\Delta\times\mathbf{N}{\left[(\oc)\Delta\right]}$ inductively as follows:

• •

$x\mathrel{{\Rightarrow_{\partial}}}x$;

• •

${\left\langle\lambda x\,{s}\right\rangle}\,{\overline{t}}\mathrel{{\Rightarrow_{\partial}}}\partial_{x}\sigma^{\prime}\cdot\overline{\tau^{\prime}}$ as soon as $s\mathrel{{\Rightarrow_{\partial}}}\sigma^{\prime}$ and $\overline{t}\mathrel{{\Rightarrow_{\partial}}}\overline{\tau^{\prime}}$;

• •

$\lambda x\,{s}\mathrel{{\Rightarrow_{\partial}}}\lambda x\,{\sigma^{\prime}}$ as soon as $s\mathrel{{\Rightarrow_{\partial}}}\sigma^{\prime}$;

• •

${\left\langle s\right\rangle}\,{\overline{t}}\mathrel{{\Rightarrow_{\partial}}}{\left\langle\sigma^{\prime}\right\rangle}\,{\overline{\tau^{\prime}}}$ as soon as $s\mathrel{{\Rightarrow_{\partial}}}\sigma^{\prime}$ and $\overline{t}\mathrel{{\Rightarrow_{\partial}}}\overline{\tau}^{\prime}$;

• •

${\left[s_{1},\dotsc,s_{n}\right]}\mathrel{{\Rightarrow_{\partial}}}{\left[\sigma^{\prime}_{1},\dotsc,\sigma^{\prime}_{n}\right]}$ as soon as $s_{i}\mathrel{{\Rightarrow_{\partial}}}\sigma^{\prime}_{i}$ for each $i\in{\left\{1,\dotsc,n\right\}}$.

We extend this reduction to sums of resource expressions by linearity: $\epsilon\mathrel{{\Rightarrow_{\partial}}}\epsilon^{\prime}$ if $\epsilon=\sum_{i=1}^{n}e_{i}$ and $\epsilon^{\prime}=\sum_{i=1}^{n}\epsilon^{\prime}_{i}$ with $e_{i}\mathrel{{\Rightarrow_{\partial}}}\epsilon^{\prime}_{i}$ for all $i\in{\left\{1,\dotsc,n\right\}}$.

It should be clear that $\mathord{\mathrel{{\rightarrow_{\partial}}}}\subseteq\mathord{\mathrel{{\Rightarrow_{\partial}}}}\subset\mathord{\mathrel{{\rightarrow_{\partial}^{*}}}}$, Moreover observe that, because all term constructors are linear, the reduction rules extend naturally to finite sums of resource expressions: for instance, $\lambda x\,{\sigma}\mathrel{{\Rightarrow_{\partial}}}\lambda x\,{\sigma^{\prime}}$ as soon as $\sigma\mathrel{{\Rightarrow_{\partial}}}\sigma^{\prime}$.

We will prove in Sections 6 and 7 that this solution is indeed a good one: parallel resource reduction is strongly confluent, and there is a way to extend it to resource vectors so that not only the resulting reduction is strongly confluent and allows to simulate $\beta$-reduction, but any reduction step from the Taylor expansion of an algebraic term can be completed into a parallel $\beta$-reduction step. There are two pitfalls with this approach, though.

5.2. Size collapse

First, parallel reduction $\mathrel{{\Rightarrow_{\partial}}}$ (like iterated reduction $\mathrel{{\rightarrow_{\partial}^{*}}}$) lacks the combinatorial regularity properties of $\mathrel{{\rightarrow_{\partial}}}$ given by Lemma 3.4: write $e{}_{\partial}e^{\prime}$ if $e\mathrel{{\Rightarrow_{\partial}}}\epsilon^{\prime}$ with $e^{\prime}\in{\left|\epsilon^{\prime}\right|}$; $e^{\prime}\in(\oc)\Delta$ being fixed, there is no bound on the size of the $\mathrel{{\Rightarrow_{\partial}}}$-antecedents of $e^{\prime}$, i.e. those $e\in(\oc)\Delta$ such that $e{}_{\partial}e^{\prime}$.

Example 5.3**.**

Fix $s\in\Delta$. Consider the sequences $\overrightarrow{u}(s)$ and $\overrightarrow{v}(s)$ of resource terms given by:

[TABLE]

Observe that for all $n\in\mathbf{N}$, $u_{n+1}(s)\mathrel{{\rightarrow_{\partial}}}u_{n}(s)$ and $v_{n+1}(s)\mathrel{{\rightarrow_{\partial}}}v_{n}(s)$, and more generally, for all $n^{\prime}\leq n$, $u_{n}(s)\mathrel{{\Rightarrow_{\partial}}}u_{n^{\prime}}(s)$ and $v_{n}(s)\mathrel{{\Rightarrow_{\partial}}}v_{n^{\prime}}(s)$. In particular $u_{n}(s)\mathrel{{\Rightarrow_{\partial}}}s$ and $v_{n}(s)\mathrel{{\Rightarrow_{\partial}}}s$ for all $n\in\mathbf{N}$.

Reducing all resource expressions in a resource vector simultaneously is thus no longer possible in general: consider, e.g., $\sum_{n\in\mathbf{N}}u_{n}(x)$. As a consequence, when we introduce a reduction relation on resource vectors by extending a reduction relation on resource expressions as above, we must in general impose the summability of the family of reducts as a side condition:

Definition 5.4**.**

Fix an arbitrary relation $\mathord{\mathrel{{\rightarrow}}}\subseteq(\oc)\Delta\times\mathbf{N}{\left[(\oc)\Delta\right]}$. For all $\epsilon,\epsilon^{\prime}\in\mathbf{S}^{(\oc)\Delta}$, we write $\epsilon\mathrel{{\widetilde{\rightarrow}}}\epsilon^{\prime}$ whenever there exist families $(a_{i})_{i\in I}\in\mathbf{S}^{I}$, ${\left(e_{i}\right)}_{i\in I}\in(\oc)\Delta^{I}$ and ${\left(\epsilon^{\prime}_{i}\right)}_{i\in I}\in\mathbf{N}{\left[(\oc)\Delta\right]}^{I}$ such that:

• •

${\left(e_{i}\right)}_{i\in I}$ is summable and $\epsilon=\sum_{i\in I}a_{i}.e_{i}$;

• •

${\left(\epsilon^{\prime}_{i}\right)}_{i\in I}$ is summable and $\epsilon^{\prime}=\sum_{i\in I}a_{i}.\epsilon^{\prime}_{i}$;

• •

for all $i\in I$, $e_{i}\mathrel{{\rightarrow^{?}}}\epsilon^{\prime}_{i}$.

The necessity of such a side condition forbids confluence. Indeed:

Example 5.5**.**

Let $\sigma=\sum_{n}u_{n}(v_{n}(x))$. Then $\sigma\mathrel{{\widetilde{\Rightarrow_{\partial}}}}\sum u_{n}(x)$ and $\sigma\mathrel{{\widetilde{\Rightarrow_{\partial}}}}\sum v_{n}(x)$, but since the only common reduct of $u_{p}(x)$ and $v_{q}(x)$ is $x$, there is no way171717 In fact, this argument is only valid if $\mathbf{S}$ is zerosumfree (i.e. if $a+b=0\in\mathbf{S}$ entails $a=b=0$; see below, in particular Lemma 5.7), for instance if $\mathbf{S}=\mathbf{N}$: we rely on the fact that if $\sum_{i\in I}a_{i}.s_{i}=\sum_{n\in\mathbf{N}}u_{n}(x)$ then for all $i\in I$ such that $a_{i}\not=0$, there is $n\in\mathbf{N}$ such that $s_{i}=u_{n}(x)$.

to close this pair of reductions: ${\left(x\right)}_{n\in\mathbf{N}}$ is not summable.

These considerations lead us to study the combinatorics of parallel resource reduction more closely: in Section 6, we introduce successive variants of parallel reduction, based on restrictions on the nesting of fired redexes, and provide bounds for the size of antecedents of a resource expression. We moreover consider sufficient conditions for these restrictions to be preserved under reduction.

We then observe in Section 7 that, when applied to Taylor expansions, parallel reduction is automatically of the most restricted form, which allows us to provide uniform bounds and obtain the desired confluence and simulation properties.

5.3. Reduction structures

The other, a priori unrelated pitfall is the fact that the reduction can interact badly with the semimodule structure of $\mathbf{S}^{(\oc)\Delta}$: we can reproduce Example 4.1 in $\mathbf{S}^{(\oc)\Delta}$ through Taylor expansion (see the discussion in Section 7.1, p.7.1). Even more simply, we can use the terms of Example 5.3:

Example 5.6**.**

Let $s\in\Delta$ and $\sigma=\sum_{n\in\mathbf{N}}u_{n+1}(s)\in\mathbf{S}^{\Delta}$. Assuming $\mathbf{S}$ is a ring: $0=\sigma+(-1).\sigma\mathrel{{\widetilde{\Rightarrow_{\partial}}}}\sum_{n\in\mathbf{N}}u_{n}(s)+(-1).\sigma=s$.

Of course, this kind of issue does not arise when the semiring of coefficients is zerosumfree: recall that $\mathbf{S}$ is zerosumfree if $a+b=0$ implies $a=b=0$, which holds for all semirings of non-negative numbers, as well as for booleans. This prevents interferences between reductions and the semimodule structure:

Lemma 5.7**.**

Assume $\mathbf{S}$ is zerosumfree and fix a relation $\mathord{\mathrel{{\rightarrow}}}\subseteq(\oc)\Delta\times\mathbf{N}{\left[(\oc)\Delta\right]}$. If $\epsilon\mathrel{{\widetilde{\rightarrow}}}\epsilon^{\prime}$ then, for all $e^{\prime}\in{\left|\epsilon^{\prime}\right|}$ there exists $e\in{\left|\epsilon\right|}$ and $\epsilon_{0}\in\mathbf{N}{\left[(\oc)\Delta\right]}$ such that $e\mathrel{{\rightarrow^{?}}}\epsilon_{0}$ and $e^{\prime}\in{\left|\epsilon_{0}\right|}$.

Proof 5.8**.**

Assume $\epsilon=\sum_{i\in I}a_{i}.e_{i}$ and $\epsilon^{\prime}=\sum_{i\in I}a_{i}.\epsilon^{\prime}_{i}$ with $e_{i}\mathrel{{\rightarrow^{?}}}\epsilon^{\prime}_{i}$ for all $i\in I$. If $e^{\prime}\in{\left|\epsilon^{\prime}\right|}$ then there is $i\in I$ such that $e^{\prime}\in{\left|a_{i}.\epsilon^{\prime}_{i}\right|}$ hence $a_{i}\not=0$ and $e^{\prime}\in{\left|\epsilon^{\prime}_{i}\right|}$. Then, since $\mathbf{S}$ is zerosumfree, $e_{i}\in{\left|\epsilon\right|}$.

Various alternative approaches to get rid of this restriction in the setting of the algebraic $\lambda$-calculus can be adapted to the reduction of resource vectors: we refer the reader to the literature on algebraic $\lambda$-calculi [Vau09, AD08, Alb14, DC11] for several proposals. The linear-continuity of the resource $\lambda$-calculus allows us to propose a novel approach: consider possible restrictions on the families of resource expressions simultaneously reduced in a $\mathrel{{\widetilde{\rightarrow}}}$-step.

Definition 5.9**.**

We call resource support any set $\mathcal{E}\subseteq(\oc)\Delta$ of resource expressions such that $\mathord{\mathbf{fv}}{\left(\mathcal{E}\right)}=\bigcup_{e\in\mathcal{E}}\mathord{\mathbf{fv}}{\left(e\right)}$ is finite. Then a resource structure is any set $\mathfrak{E}\subseteq\mathord{\mathfrak{P}}{\left((\oc)\Delta\right)}$ of resource supports such that:

• •

$\mathfrak{E}$ contains all finite resource supports;

• •

$\mathfrak{E}$ is closed under finite unions;

• •

$\mathfrak{E}$ is downwards closed for inclusion.

The maximal resource structure is $(\oc)\mathfrak{F}_{\mathord{\mathbf{fv}}}\mathrel{\mathord{:}\mathord{=}}{\left\{\mathcal{E}\subseteq(\oc)\Delta\mathrel{;}\mathord{\mathbf{fv}}{\left(\mathcal{E}\right)}\text{ is finite}\right\}}$, which is also a finiteness structure [Ehr10]. Observe that any finiteness structure $\mathfrak{F}\subseteq(\oc)\mathfrak{F}_{\mathord{\mathbf{fv}}}$ is a resource structure: all three additional conditions are automatically satisfied.

Definition 5.10**.**

Fix a relation $\mathord{\mathrel{{\rightarrow}}}\subseteq(\oc)\Delta\times\mathbf{N}{\left[(\oc)\Delta\right]}$. For all resource support $\mathcal{E}$, we write $\mathrel{{\widetilde{\rightarrow}_{\mathcal{E}}}}$ for $\mathrel{{\widetilde{\rightharpoonup_{\mathcal{E}}}}}$ where $\rightharpoonup_{\mathcal{E}}$ denotes ${\mathord{\to}\mathbin{\cap}(\mathcal{E}\times\mathbf{N}{\left[(\oc)\Delta\right]})}$. For all resource structure $\mathfrak{E}$, we then write $\mathrel{{\widetilde{\rightarrow}_{\mathfrak{E}}}}$ for $\bigcup_{\mathcal{E}\in\mathfrak{E}}\mathord{\mathrel{{\widetilde{\rightarrow}_{\mathcal{E}}}}}$.

We have $\mathord{\mathrel{{\widetilde{\rightarrow}_{\mathcal{E}}}}}\subseteq\mathord{\mathrel{{\widetilde{\rightarrow}}}}\mathbin{\cap}(\mathbf{S}^{\mathcal{E}}\times\mathbf{S}^{(\oc)\Delta})$, but in general the reverse inclusion holds only if $\mathbf{S}$ is zerosumfree: in this latter case $\epsilon\mathrel{{\widetilde{\Rightarrow_{\partial}}}}\epsilon^{\prime}$ iff $\epsilon\mathrel{{\widetilde{\Rightarrow_{\partial}}_{{\left|\epsilon\right|}}}}\epsilon^{\prime}$.

Definition 5.11**.**

We call $\mathrel{{\rightarrow}}$-reduction structure any resource structure $\mathfrak{E}$ such that if $\mathcal{E}\in\mathfrak{E}$ then $\bigcup{\left\{{\left|\epsilon^{\prime}\right|}\mathrel{;}e\in\mathcal{E}\text{ and }e\mathrel{{\rightarrow^{?}}}\epsilon^{\prime}\right\}}\in\mathfrak{E}$.

We will consider some particular choices of reduction structure in the following, but the point is that our approach is completely generic. The results of Section 7 will imply that if $\mathfrak{S}\subseteq\mathord{\mathfrak{P}}{\left(\mathbf{S}^{\Delta}\right)}$ is a $\mathrel{{\Rightarrow_{\partial}}}$-reduction structure containing ${\left|\mathord{\tau}{\left(M\right)}\right|}$ then one can translate any $\mathrel{{\Rightarrow_{\beta}}}$-reduction sequence from $M$ into a $\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathfrak{S}}}}$-reduction sequence from $\mathord{\tau}{\left(M\right)}$. Additional properties such as the confluence of $\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathfrak{S}}}}$, its conservativity over $\mathrel{{\Rightarrow_{\beta}}}$, or its compatibility with normalization will depend on additional conditions on $\mathfrak{S}$.

6. Taming the size collapse of parallel resource reduction

In this section, we study successive families of restrictions of the parallel resource reduction $\mathrel{{\Rightarrow_{\partial}}}$. Our purpose is to enforce some control on the size collapse induced by $\mathrel{{\Rightarrow_{\partial}}}$, so as to obtain a confluent restriction of $\mathrel{{\widetilde{\Rightarrow_{\partial}}}}$, all the while retaining enough parallelism to simulate parallel $\beta$-reduction on algebraic $\lambda$-terms, ideally in a conservative way.

First observe that parallel resource reduction itself is strongly confluent as expected: following a classic argument, we define $\mathord{\mathsf{F}}{\left(e\right)}$ as the result of firing all redexes in $e$ and then, whenever $e\mathrel{{\Rightarrow_{\partial}}}\epsilon^{\prime}$, we have $\epsilon^{\prime}\mathrel{{\Rightarrow_{\partial}}}\mathord{\mathsf{F}}{\left(e\right)}$. Formally:

Definition 6.1**.**

For all $e\in(\oc)\Delta$ we define the full parallel reduct $\mathord{\mathsf{F}}{\left(e\right)}$ of $e$ by induction on $e$ as follows:

[TABLE]

Then if $\epsilon=\sum_{i=1}^{n}e_{i}\in\mathbf{N}{\left[(\oc)\Delta\right]}$, we set $\mathord{\mathsf{F}}{\left(\epsilon\right)}=\sum_{i=1}^{n}\mathord{\mathsf{F}}{\left(e_{i}\right)}$.

Lemma 6.2**.**

For all $\epsilon,\epsilon^{\prime}\in\mathbf{N}{\left[(\oc)\Delta\right]}$, if $\epsilon\mathrel{{\Rightarrow_{\partial}}}\epsilon^{\prime}$ then $\epsilon^{\prime}\mathrel{{\Rightarrow_{\partial}}}\mathord{\mathsf{F}}{\left(\epsilon\right)}$.

Proof 6.3**.**

Follows directly from the definitions.

In general, however, if we fix $e^{\prime}\in(\oc)\Delta$ then there is no bound on those $e\in(\oc)\Delta$ such that $e^{\prime}\in{\left|\mathord{\mathsf{F}}{\left(e\right)}\right|}$, so we cannot extend $\mathord{\mathsf{F}}$ on $\mathbf{S}^{(\oc)\Delta}$, nor generalize Lemma 6.2 to $\mathrel{{\widetilde{\Rightarrow_{\partial}}}}$. Indeed, we have shown that $\mathrel{{\widetilde{\Rightarrow_{\partial}}}}$ is not even confluent.

In order to understand what restrictions are necessary to recover confluence, we first provide a close inspection of the combinatorial effect of $\mathrel{{\Rightarrow_{\partial}}}$ on the size of resource expressions: we show in subsection 6.1 that bounding the length of chains of immediately nested fired redexes is enough to bound the size of $\mathrel{{\Rightarrow_{\partial}}}$-antecedents of a fixed resource expression.

In order to close a pair of reductions $e\mathrel{{\Rightarrow_{\partial}}}\epsilon^{\prime}$ and $e\mathrel{{\Rightarrow_{\partial}}}\epsilon^{\prime\prime}$, we have to reduce at least the residuals in $\epsilon^{\prime}$ of the redexes fired in the reduction $e\mathrel{{\Rightarrow_{\partial}}}\epsilon^{\prime\prime}$ (and vice versa). So we want the above bounds to be stable under taking the unions of sets of redexes in a term: it is not the case if we consider chains of immediately nested redexes. In Subsection 6.2, we extend the boundedness condition to all chains of nested fired redexes and introduce the family ${\left(\mathrel{{\Rightarrow_{{(b)}}}}\right)}_{b\in\mathbf{N}}$ of boundedly nested parallel reductions. We then show that this family enjoys a kind of diamond property (Lemma 6.21), which can then be extended to $\mathord{\mathrel{{\widetilde{\Rightarrow_{{(\partial)}}}}}}=\bigcup_{b\in\mathbf{N}}\mathord{\mathrel{{\widetilde{\Rightarrow_{{(b)}}}}}}$. We must require that $\mathbf{S}$ enjoys an additional additive splitting property (see Definition 6.23), in order to “align” the $\mathrel{{\Rightarrow_{{(b)}}}}$-reductions involved in both sides of a pair of $\mathrel{{\widetilde{\Rightarrow_{{(b)}}}}}$-reductions from the same resource vector (see the proof of Lemma 6.26).

To get rid of the additive splitting hypothesis we must further restrict resource reduction so as to recover a notion of full reduct at bounded depth. It is not sufficient to bound the depth of fired redexes because this is not stable under reduction. In Subsection 6.3, we rather introduce the parallel reduction $\mathrel{{\Rightarrow_{{\lfloor d\rfloor}}}}$ where substituted variables occur at depth at most $d$. We then show that $\mathord{\mathrel{{\widetilde{\Rightarrow_{{\lfloor\partial\rfloor}}}}}}=\bigcup_{d\in\mathbf{N}}\mathord{\mathrel{{\widetilde{\Rightarrow_{{\lfloor d\rfloor}}}}}}$ is strongly confluent by proving that any $\mathrel{{\Rightarrow_{{\lfloor d\rfloor}}}}$-step from $\epsilon$ can be followed by a $\mathrel{{\Rightarrow_{{\lfloor d^{\prime}\rfloor}}}}$-reduction to $\mathord{\mathsf{F}}_{{\lfloor d\rfloor}}{\left(\epsilon\right)}$, where $\mathord{\mathsf{F}}_{{\lfloor d\rfloor}}{\left(\epsilon\right)}$ is obtained by firing all redexes in $\epsilon$ for which the bound variables occur at depth at most $d$, and $d^{\prime}$ depends only on $d$.

Finally, we consider resource vectors of bounded height: these contain the Taylor expansions of algebraic $\lambda$-terms. We show that all the above restrictions actually coincide with $\mathrel{{\widetilde{\Rightarrow_{\partial}}}}$ on bounded resource vectors. In this particular case, we can actually extend $\mathord{\mathsf{F}}$ by linear-continuity and obtain a proof of the diamond property for $\mathrel{{\widetilde{\Rightarrow_{\partial}}}}$.181818 Note that, although they involve increasing constraints on parallel reduction, Subsections 6.1 to 6.3 are essentially pairwise independent. Moreover, we obtain the diamond property for $\mathrel{{\widetilde{\Rightarrow_{\partial}}}}$ on bounded resource vectors as a consequence of the results of Subsection 6.3, but it could as well be proved directly, using similar techniques (see Footnote 21, p.21). So, the reader who only wants the proofs necessary for the main results of the paper can skip Subsections 6.1 and 6.2; the reader who is not interested in checking proofs can also skip subsection 6.3. We chose to present the successive families of restrictions anyway, because their construction provides a precise understanding of the combinatorics of parallel resource reduction, and of the various ingredients involved in designing a strongly confluent version of $\mathrel{{\widetilde{\Rightarrow_{\partial}}}}$: we start by avoiding the size collapse by putting a restriction on families of redexes that can be fired in parallel; then we ensure that this restriction is stable under reduction. This understanding plays a key rôle in enabling the generalization of our approach to linear logic proof nets or infinitary $\lambda$-calculus: with Chouquet, we have recently established that our restrictions on the nesting of redexes, as well as their preservation under reduction, can be adapted to the setting of proof nets [CA18]; and preliminary work on infinitary $\lambda$-calculus indicates that it could be amenable to the technique of Subsection 6.2, whereas it does not make sense to restrict the depth of substituted variables in this setting.

At this point of the discussion, it is worth noting that, if we extend a relation $\mathord{\mathrel{{\rightarrow}}}\subseteq{(\oc)\Delta\times\mathbf{N}{\left[(\oc)\Delta\right]}}$ to a binary relation on finite sums of resource expressions so that $\epsilon\mathrel{{\rightarrow}}\epsilon^{\prime}$ iff $\epsilon=\sum_{i=1}^{n}e_{i}$ and $\epsilon^{\prime}=\sum_{i=1}^{n}\epsilon^{\prime}_{i}$ with $e_{i}\mathrel{{\rightarrow}}\epsilon^{\prime}_{i}$ for all $i\in{\left\{1,\dotsc,n\right\}}$, then for all $\mathrel{{\rightarrow}}$-reduction structure $\mathfrak{E}$ and all resource vectors $\epsilon,\epsilon^{\prime}\in\mathbf{S}^{(\oc)\Delta}$, we have $\epsilon\mathrel{{\widetilde{\rightarrow}_{\mathfrak{E}}}}\epsilon^{\prime}$ iff there exist a set $I$ of indices, a resource support $\mathcal{E}\in\mathfrak{E}$, a family $(a_{i})_{i\in I}\in\mathbf{S}^{I}$ of scalars and families ${\left(\epsilon_{i}\right)}_{i\in I}\in\mathbf{N}{\left[\mathcal{E}\right]}^{I}$ and ${\left(\epsilon^{\prime}_{i}\right)}_{i\in I}\in\mathbf{N}{\left[(\oc)\Delta\right]}^{I}$ such that:

• •

${\left(\epsilon_{i}\right)}_{i\in I}$ is summable and $\epsilon=\sum_{i\in I}a_{i}.\epsilon_{i}$;

• •

${\left(\epsilon^{\prime}_{i}\right)}_{i\in I}$ is summable and $\epsilon^{\prime}=\sum_{i\in I}a_{i}.\epsilon^{\prime}_{i}$;

• •

for all $i\in I$, $\epsilon_{i}\mathrel{{\rightarrow}}\epsilon^{\prime}_{i}$.

We will use this fact for confluence proofs: $\mathrel{{\Rightarrow_{\partial}}}$ and its variants are all of this form.

6.1. Bounded chains of redexes

Definition 6.4**.**

We define a family of relations $\mathord{\mathrel{{\Rightarrow_{{\left(m|k\right)}}}}}\subseteq(\oc)\Delta\times\mathbf{N}{\left[(\oc)\Delta\right]}$ for $m\leq k\in\mathbf{N}$ inductively as follows:

• •

$x\mathrel{{\Rightarrow_{{\left(m|k\right)}}}}x$ for all $m\leq k\in\mathbf{N}$;

• •

$\lambda x\,{s}\mathrel{{\Rightarrow_{{\left(m|k\right)}}}}\lambda x\,{\sigma^{\prime}}$ if $m\leq k$ and $s\mathrel{{\Rightarrow_{{\left(m_{1}|k\right)}}}}\sigma^{\prime}$ for some $m_{1}\leq k$;

• •

${\left\langle s\right\rangle}\,{\overline{t}}\mathrel{{\Rightarrow_{{\left(m|k\right)}}}}{\left\langle\sigma^{\prime}\right\rangle}\,{\overline{\tau^{\prime}}}$ if $m\leq k$, $s\mathrel{{\Rightarrow_{{\left(m_{1}|k\right)}}}}\sigma^{\prime}$ and $\overline{t}\mathrel{{\Rightarrow_{{\left(m_{2}|k\right)}}}}\overline{\tau^{\prime}}$ for some $m_{1}\leq k$ and $m_{2}\leq k$;

• •

${\left[s_{1},\dotsc,s_{r}\right]}\mathrel{{\Rightarrow_{{\left(m|k\right)}}}}{\left[\sigma^{\prime}_{1},\dotsc,\sigma^{\prime}_{r}\right]}$ if $s_{i}\mathrel{{\Rightarrow_{{\left(m|k\right)}}}}\sigma^{\prime}_{i}$ for all $i\in{\left\{1,\dotsc,r\right\}}$;

• •

${\left\langle\lambda x\,{s}\right\rangle}\,{\overline{t}}\mathrel{{\Rightarrow_{{\left(m|k\right)}}}}\partial_{x}\sigma^{\prime}\cdot\overline{\tau^{\prime}}$ if $0<m\leq k$, $s\mathrel{{\Rightarrow_{{\left(m-1|k\right)}}}}\sigma^{\prime}$ and $\overline{t}\mathrel{{\Rightarrow_{{\left(m-1|k\right)}}}}\overline{\tau^{\prime}}$.

Intuitively, we have $e\mathrel{{\Rightarrow_{{\left(m|k\right)}}}}\epsilon^{\prime}$ iff $e\mathrel{{\Rightarrow_{\partial}}}\epsilon^{\prime}$ and that reduction fires chains of redexes of length at most $k$, those starting at top level being of length at most $m$. In particular, it should be clear that if $e\mathrel{{\Rightarrow_{{\left(m|k\right)}}}}\epsilon^{\prime}$ then $e\mathrel{{\Rightarrow_{\partial}}}\epsilon^{\prime}$, and $e\mathrel{{\Rightarrow_{{\left(m^{\prime}|k^{\prime}\right)}}}}\epsilon^{\prime}$ as soon as $m\leq m^{\prime}\leq k^{\prime}$ and $k\leq k^{\prime}$. Moreover, $e\mathrel{{\Rightarrow_{\partial}}}\epsilon^{\prime}$ iff $e\mathrel{{\Rightarrow_{{\left(\mathord{\mathbf{h}}{\left(e\right)}|\mathord{\mathbf{h}}{\left(e\right)}\right)}}}}\epsilon^{\prime}$.

Definition 6.5**.**

We define $\mathbf{gb}_{k}{\left(l,m\right)}\in\mathbf{N}$ for all $k,l,m\in\mathbf{N}$, by induction on the lexicographically ordered pair $(l,m)$:

[TABLE]

We then write $\mathbf{gb}_{k}{\left(l\right)}\mathrel{\mathord{:}\mathord{=}}\mathbf{gb}_{k}{\left(l,k\right)}$.

For all $k,l,m\in\mathbf{N}$, the following identities follow straightforwardly from the definition and will be used throughout this subsection:

[TABLE]

Lemma 6.6**.**

For all $k,l,l^{\prime},m\in\mathbf{N}$, $\mathbf{gb}_{k}{\left(l+l^{\prime},m\right)}\geq\mathbf{gb}_{k}{\left(l,m\right)}+\mathbf{gb}_{k}{\left(l^{\prime},m\right)}$.

Proof 6.7**.**

By induction on $l^{\prime}$. The case $l^{\prime}=0$ is direct. Assume the result holds for $l^{\prime}$, we prove it for $l^{\prime}+1$:

[TABLE]

The following generalization follows directly:

Corollary 6.8**.**

For all $l_{1}\dotsc,l_{n}\in\mathbf{N}$

[TABLE]

Lemma 6.9**.**

For all $k,l,m\in\mathbf{N}$, $\mathbf{gb}_{k}{\left(l,m\right)}\geq l$.

Proof 6.10**.**

By Corollary 6.8, $\mathbf{gb}_{k}{\left(l,m\right)}\geq l\times\mathbf{gb}_{k}{\left(1,m\right)}=l\times 4^{m}$.

Lemma 6.11**.**

For all $k,k^{\prime},l,l^{\prime},m,m^{\prime}\in\mathbf{N}$ if $k\leq k^{\prime}$, $l\leq l^{\prime}$ and $m\leq m^{\prime}$, then:

[TABLE]

Proof 6.12**.**

We prove the monotonicity of $\mathbf{gb}_{k}{\left(l,m\right)}$ in $m$, $l$ and then $k$, separately.

First, if $m\leq m^{\prime}$ then $\mathbf{gb}_{k}{\left(l,m\right)}=4^{m}\mathbf{gb}_{k}{\left(l,0\right)}\leq 4^{m^{\prime}}\mathbf{gb}_{k}{\left(l,0\right)}=\mathbf{gb}_{k}{\left(l,m^{\prime}\right)}$.

By Lemma 6.6, if $l\leq l^{\prime}$, $\mathbf{gb}_{k}{\left(l^{\prime},m\right)}\geq\mathbf{gb}_{k}{\left(l,m\right)}+\mathbf{gb}_{k}{\left(l^{\prime}-l,m\right)}\geq\mathbf{gb}_{k}{\left(l,m\right)}$.

Finally, we prove that if $k\leq k^{\prime}$ then $\mathbf{gb}_{k}{\left(l,m\right)}\leq\mathbf{gb}_{k^{\prime}}{\left(l,m\right)}$ by induction on the lexicographically ordered pair $(l,m)$:

[TABLE]

Write $e{}_{{\left(m|k\right)}}e^{\prime}$ if $e\mathrel{{\Rightarrow_{{\left(m|k\right)}}}}\epsilon^{\prime}$ with $e^{\prime}\in{\left|\epsilon^{\prime}\right|}$.

Lemma 6.13**.**

If $e{}_{{\left(m|k\right)}}e^{\prime}$ then $\mathord{\mathbf{s}}{\left(e\right)}\leq\mathbf{gb}_{k}{\left(\mathord{\mathbf{s}}{\left(e^{\prime}\right)},m\right)}$.

Proof 6.14**.**

By induction on the reduction $e\mathrel{{\Rightarrow_{{\left(m|k\right)}}}}\epsilon^{\prime}$ such that $e^{\prime}\in\epsilon^{\prime}$.

If $e=x=\epsilon^{\prime}$ then $e^{\prime}=x$ and $\mathord{\mathbf{s}}{\left(e\right)}=1=\mathbf{gb}_{0}{\left(1,0\right)}\leq\mathbf{gb}_{k}{\left(\mathord{\mathbf{s}}{\left(e^{\prime}\right)},m\right)}$.

If $e=\lambda x\,{s}$, $\epsilon^{\prime}=\lambda x\,{\sigma^{\prime}}$, $m\leq k$ and $s\mathrel{{\Rightarrow_{{\left(m_{1}|k\right)}}}}\sigma^{\prime}$ with $m_{1}\leq k$, then $e^{\prime}=\lambda x\,{s^{\prime}}$ with $s{}_{{\left(m_{1}|k\right)}}s^{\prime}$. We obtain:

[TABLE]

If $e={\left\langle s\right\rangle}\,{\overline{t}}$, $\epsilon^{\prime}={\left\langle\sigma^{\prime}\right\rangle}\,{\overline{\tau^{\prime}}}$, $m\leq k$, $s\mathrel{{\Rightarrow_{{\left(m_{1}|k\right)}}}}\sigma^{\prime}$ and $\overline{t}\mathrel{{\Rightarrow_{{\left(m_{2}|k\right)}}}}\overline{\tau^{\prime}}$ with $m_{i}\leq k$ for all $i\in{\left\{1,2\right\}}$, then $e^{\prime}={\left\langle s^{\prime}\right\rangle}\,{\overline{t^{\prime}}}$ with $s{}_{{\left(m_{1}|k\right)}}s^{\prime}$ and $\overline{t}{}_{{\left(m_{2}|k\right)}}\overline{t^{\prime}}$. We obtain:

[TABLE]

If $e={\left[s_{1},\dotsc,s_{r}\right]}$, $\epsilon^{\prime}={\left[\sigma^{\prime}_{1},\dotsc,\sigma^{\prime}_{r}\right]}$ and $s_{i}\mathrel{{\Rightarrow_{{\left(m|k\right)}}}}\sigma^{\prime}_{i}$ for all $i\in{\left\{1,\dotsc,r\right\}}$, then $e^{\prime}={\left[s^{\prime}_{1},\dotsc,s^{\prime}_{r}\right]}$ with $s_{i}{}_{{\left(m|k\right)}}s^{\prime}_{i}$ for all $i\in{\left\{1,\dotsc,r\right\}}$. We obtain:

[TABLE]

If $e={\left\langle\lambda x\,{s}\right\rangle}\,{\overline{t}}$, $\epsilon^{\prime}=\partial_{x}\sigma^{\prime}\cdot\overline{\tau^{\prime}}$, $0<m\leq k$, $s\mathrel{{\Rightarrow_{{\left(m-1|k\right)}}}}\sigma^{\prime}$ and $\overline{t}\mathrel{{\Rightarrow_{{\left(m-1|k\right)}}}}\overline{\tau^{\prime}}$, then there are $s^{\prime}\in{\left|\sigma^{\prime}\right|}$ and $\overline{t^{\prime}}\in{\left|\overline{\tau^{\prime}}\right|}$ such that $e^{\prime}\in{\left|\partial_{x}s^{\prime}\cdot\overline{t}^{\prime}\right|}$. In particular, $s{}_{{\left(m-1|k\right)}}s^{\prime}$ and $\overline{t}{}_{{\left(m-1|k\right)}}\overline{t^{\prime}}$ and we obtain:

[TABLE]

As a direct consequence, for all $m\leq k\in\mathbf{N}$, for all summable family ${\left(e_{i}\right)}_{i\in I}$ and all family ${\left(\epsilon^{\prime}_{i}\right)}_{i\in I}$ such that $e_{i}\mathrel{{\Rightarrow_{{\left(m|k\right)}}}}\epsilon^{\prime}_{i}$ for all $i\in I$, ${\left(\epsilon^{\prime}_{i}\right)}_{i\in I}$ is also summable: we can thus drop the side condition in the definition of $\mathrel{{\widetilde{\Rightarrow_{{\left(m|k\right)}}}}}$.

Observe however that those reduction relations are not stable under taking the unions of fired redexes in families of reduction steps: using, e.g., the terms $u_{n}(s)$ from Example 5.3, for all $n\in\mathbf{N}$, we have $u_{2n}(s)\mathrel{{\Rightarrow_{{\left(1|1\right)}}}}u_{n}(s)$ by firing all redexes at even depth, $u_{2n}(s)\mathrel{{\Rightarrow_{{\left(0|1\right)}}}}u_{n}(s)$ by firing all redexes at odd depth, and $u_{2n}(s)\mathrel{{\Rightarrow_{{\left(2n|2n\right)}}}}s$ by firing both families, but there is obviously no $k\in\mathbf{N}$ such that $u_{2n}(s)\mathrel{{\Rightarrow_{{\left(k|k\right)}}}}s$ uniformly for all $n\in\mathbf{N}$. Although we can close the induced critical pair

$\sum_{n\in\mathbf{N}}u_{2n}(s)\mathrel{{\widetilde{\Rightarrow_{{\left(0|1\right)}}}}}\sum_{n\in\mathbf{N}}u_{n}(s)$ and $\sum_{n\in\mathbf{N}}u_{2n}(s)\mathrel{{\widetilde{\Rightarrow_{{\left(1|1\right)}}}}}\sum_{n\in\mathbf{N}}u_{n}(s)$

trivially in this case, this phenomenon is an obstacle to confluence:

Example 6.15**.**

Fix $s\in\Delta$ and consider the sequence $\overrightarrow{w}(s)$ of resource terms given by $w_{0}(s)=s$ and:

[TABLE]

Then for all $n\in\mathbf{N}$, $w_{2n}(s)\mathrel{{\Rightarrow_{{\left(1|1\right)}}}}u_{n}(s)$, $w_{2n+1}(s)\mathrel{{\Rightarrow_{{\left(0|1\right)}}}}u_{n}(s)$, $w_{2n}(s)\mathrel{{\Rightarrow_{{\left(0|1\right)}}}}v_{n}(s)$, and $w_{2n+1}(s)\mathrel{{\Rightarrow_{{\left(1|1\right)}}}}v_{n}(s)$. Then for instance

[TABLE]

but we know from Example 5.5 that this pair of reductions cannot be closed in general.

6.2. Boundedly nested redexes

From the previous subsection, it follows that bounding the length of chains of immediately nested redexes allows to tame the size collapse of resource expressions under reduction, but we need to further restrict this notion in order to keep it stable under unions of fired redex sets. A natural answer is to require a bound on the depth of the nesting of fired redexes, regardless of the distance between them:

Definition 6.16**.**

We define a family of relations ${\left(\mathrel{{\Rightarrow_{{(b)}}}}\right)}_{b\in{\mathbf{N}}}$ inductively as follows:

• •

$x\mathrel{{\Rightarrow_{{(b)}}}}x$ for all $b\in\mathbf{N}$;

• •

$\lambda x\,{s}\mathrel{{\Rightarrow_{{(b)}}}}\lambda x\,{\sigma^{\prime}}$ if $s\mathrel{{\Rightarrow_{{(b)}}}}\sigma^{\prime}$;

• •

${\left\langle s\right\rangle}\,{\overline{t}}\mathrel{{\Rightarrow_{{(b)}}}}{\left\langle\sigma^{\prime}\right\rangle}\,{\overline{\tau^{\prime}}}$ if $s\mathrel{{\Rightarrow_{{(b)}}}}\sigma^{\prime}$ and $\overline{t}\mathrel{{\Rightarrow_{{(b)}}}}\overline{\tau^{\prime}}$;

• •

${\left[s_{1},\dotsc,s_{r}\right]}\mathrel{{\Rightarrow_{{(b)}}}}{\left[\sigma^{\prime}_{1},\dotsc,\sigma^{\prime}_{r}\right]}$ if $s_{i}\mathrel{{\Rightarrow_{{(b)}}}}\sigma^{\prime}_{i}$ for all $i\in{\left\{1,\dotsc,r\right\}}$;

• •

${\left\langle\lambda x\,{s}\right\rangle}\,{\overline{t}}\mathrel{{\Rightarrow_{{(b)}}}}\partial_{x}\sigma^{\prime}\cdot\overline{\tau^{\prime}}$ if $b\geq 1$, $s\mathrel{{\Rightarrow_{{(b-1)}}}}\sigma^{\prime}$ and $\overline{t}\mathrel{{\Rightarrow_{{(b-1)}}}}\overline{\tau^{\prime}}$.

Intuitively, we have $e\mathrel{{\Rightarrow_{{(b)}}}}\epsilon^{\prime}$ iff $e\mathrel{{\Rightarrow_{\partial}}}\epsilon^{\prime}$ and every branch of $e$ (seen as a rooted tree) crosses at most $b$ fired redexes. In particular it should be clear that if $e\mathrel{{\Rightarrow_{{(b)}}}}\epsilon^{\prime}$ then $e\mathrel{{\Rightarrow_{{\left(b|b\right)}}}}\epsilon^{\prime}$, and moreover $e\mathrel{{\Rightarrow_{{(b^{\prime})}}}}\epsilon^{\prime}$ for all $b^{\prime}\geq b$. Moreover observe that $e\mathrel{{\Rightarrow_{{(\mathord{\mathbf{h}}{\left(e\right)})}}}}\epsilon^{\prime}$ whenever $e\mathrel{{\Rightarrow_{\partial}}}\epsilon^{\prime}$, hence $\mathord{\mathrel{{\Rightarrow_{\partial}}}}=\bigcup_{b\in\mathbf{N}}\mathord{\mathrel{{\Rightarrow_{{(b)}}}}}$.

Write $e{}_{{(b)}}e^{\prime}$ if $e\mathrel{{\Rightarrow_{{(b)}}}}\epsilon^{\prime}$ with $e^{\prime}\in{\left|\epsilon^{\prime}\right|}$. If $e{}_{{(b)}}e^{\prime}$, then $e{}_{{\left(b|b\right)}}e^{\prime}$ and we thus know that $\mathord{\mathbf{s}}{\left(e\right)}\leq\mathbf{gb}_{b}{\left(\mathord{\mathbf{s}}{\left(e^{\prime}\right)}\right)}$. In this special case, we can in fact provide a much better bound:

Lemma 6.17**.**

If $e{}_{{(b)}}e^{\prime}$ then $\mathord{\mathbf{s}}{\left(e\right)}\leq 4^{b}\mathord{\mathbf{s}}{\left(e^{\prime}\right)}$.

Proof 6.18**.**

By induction on the reduction $e\mathrel{{\Rightarrow_{{(b)}}}}{\epsilon^{\prime}}$ such that $e^{\prime}\in{\left|\epsilon^{\prime}\right|}$.

If $e=x=\epsilon^{\prime}$ then $e^{\prime}=x$ and $\mathord{\mathbf{s}}{\left(e\right)}=1\leq 4^{b}=4^{b}\mathord{\mathbf{s}}{\left(e^{\prime}\right)}$.

If $e=\lambda x\,{s}$ and $\epsilon^{\prime}=\lambda x\,{\sigma^{\prime}}$ with $s\mathrel{{\Rightarrow_{{(b)}}}}\sigma^{\prime}$, then $e^{\prime}=\lambda x\,{s^{\prime}}$ with $s{}_{{(b)}}s^{\prime}$. By induction hypothesis, $\mathord{\mathbf{s}}{\left(s\right)}\leq 4^{b}\mathord{\mathbf{s}}{\left(s^{\prime}\right)}$. Then $\mathord{\mathbf{s}}{\left(e\right)}=\mathord{\mathbf{s}}{\left(s\right)}+1\leq 4^{b}\mathord{\mathbf{s}}{\left(s^{\prime}\right)}+1\leq 4^{b}{\left(\mathord{\mathbf{s}}{\left(s^{\prime}\right)}+1\right)}=4^{b}\mathord{\mathbf{s}}{\left(e^{\prime}\right)}$.

If $e={\left\langle s\right\rangle}\,{\overline{t}}$, $\epsilon^{\prime}={\left\langle\sigma^{\prime}\right\rangle}\,{\overline{\tau^{\prime}}}$, $s\mathrel{{\Rightarrow_{{(b)}}}}\sigma^{\prime}$ and $\overline{t}\mathrel{{\Rightarrow_{{(b)}}}}\overline{\tau^{\prime}}$, then $e^{\prime}={\left\langle s^{\prime}\right\rangle}\,{\overline{t^{\prime}}}$ with $s{}_{{(b)}}s^{\prime}$ and $\overline{t}{}_{{(b)}}\overline{t^{\prime}}$. By induction hypothesis, $\mathord{\mathbf{s}}{\left(s\right)}\leq 4^{b}\mathord{\mathbf{s}}{\left(s^{\prime}\right)}$ and $\mathord{\mathbf{s}}{\left(\overline{t}\right)}\leq 4^{b}\mathord{\mathbf{s}}{\left(\overline{t^{\prime}}\right)}$. Then $\mathord{\mathbf{s}}{\left(e\right)}=\mathord{\mathbf{s}}{\left(s\right)}+\mathord{\mathbf{s}}{\left(\overline{t}\right)}+1\leq 4^{b}\mathord{\mathbf{s}}{\left(s^{\prime}\right)}+4^{b}\mathord{\mathbf{s}}{\left(\overline{t^{\prime}}\right)}+1\leq 4^{b}{\left(\mathord{\mathbf{s}}{\left(s^{\prime}\right)}+\mathord{\mathbf{s}}{\left(\overline{t^{\prime}}\right)}+1\right)}=4^{b}\mathord{\mathbf{s}}{\left(e^{\prime}\right)}$.

If $e={\left[s_{1},\dotsc,s_{r}\right]}$, $\epsilon^{\prime}={\left[\sigma^{\prime}_{1},\dotsc,\sigma^{\prime}_{r}\right]}$ and $s_{i}\mathrel{{\Rightarrow_{{(b)}}}}\sigma^{\prime}_{i}$ for all $i\in{\left\{1,\dotsc,r\right\}}$, then $e^{\prime}={\left[s^{\prime}_{1},\dotsc,s^{\prime}_{r}\right]}$ with $s_{i}{}_{{(b)}}s^{\prime}_{i}$ for all $i\in{\left\{1,\dotsc,r\right\}}$. By induction hypothesis, $\mathord{\mathbf{s}}{\left(s_{i}\right)}\leq 4^{b}\mathord{\mathbf{s}}{\left(s^{\prime}_{i}\right)}$ for all $i\in{\left\{1,\dotsc,r\right\}}$ and then $\mathord{\mathbf{s}}{\left(e\right)}=\sum_{i=1}^{r}\mathord{\mathbf{s}}{\left(s_{i}\right)}\leq\sum_{i=1}^{r}4^{b}{\mathord{\mathbf{s}}{\left(s^{\prime}_{i}\right)}}=4^{b}{\mathord{\mathbf{s}}{\left(e^{\prime}\right)}}$.

If $e={\left\langle\lambda x\,{s}\right\rangle}\,{\overline{t}}$, $\epsilon^{\prime}=\partial_{x}\sigma^{\prime}\cdot\overline{\tau^{\prime}}$, $b>0$, $s\mathrel{{\Rightarrow_{{(b-1)}}}}\sigma^{\prime}$ and $\overline{t}\mathrel{{\Rightarrow_{{(b-1)}}}}\overline{\tau^{\prime}}$, then there are $s^{\prime}\in{\left|\sigma^{\prime}\right|}$ and $\overline{t^{\prime}}\in{\left|\overline{\tau^{\prime}}\right|}$ such that $e^{\prime}\in{\left|\partial_{x}s^{\prime}\cdot\overline{t^{\prime}}\right|}$. In particular, $s{}_{{(b-1)}}s^{\prime}$ and $\overline{t}{}_{{(b-1)}}\overline{t^{\prime}}$ and, by induction hypothesis, $\mathord{\mathbf{s}}{\left(s\right)}\leq 4^{b-1}\mathord{\mathbf{s}}{\left(s^{\prime}\right)}$ and $\mathord{\mathbf{s}}{\left(\overline{t}\right)}\leq 4^{b-1}\mathord{\mathbf{s}}{\left(\overline{t^{\prime}}\right)}$. Writing $n=\mathbf{n}_{x}{\left(s^{\prime}\right)}=\mathord{\#}{\overline{t^{\prime}}}$, we have:

[TABLE]

Like for parallel reduction (Definition 5.2), we extend each $\mathrel{{\Rightarrow_{{(b)}}}}$ to sums of resource expressions by linearity: $\epsilon\mathrel{{\Rightarrow_{{(b)}}}}\epsilon^{\prime}$ if $\epsilon=\sum_{i=1}^{n}e_{i}$ and $\epsilon^{\prime}=\sum_{i=1}^{n}\epsilon^{\prime}_{i}$ with $e_{i}\mathrel{{\Rightarrow_{{(b)}}}}\epsilon^{\prime}_{i}$ for all $i\in{\left\{1,\dotsc,n\right\}}$. Again, because all term constructors are linear, the reduction rules extend naturally to finite sums of resource expressions: for instance,${\left\langle\lambda x\,{\sigma}\right\rangle}\,{\overline{\tau}}\mathrel{{\Rightarrow_{{(b)}}}}\partial_{x}\sigma^{\prime}\cdot\overline{\tau^{\prime}}$ as soon as $b\geq 1$, $\sigma\mathrel{{\Rightarrow_{{(b-1)}}}}\sigma^{\prime}$ and $\overline{\tau}\mathrel{{\Rightarrow_{{(b-1)}}}}\overline{\tau^{\prime}}$.

The relations $\mathrel{{\Rightarrow_{{(b)}}}}$ are then stable under unions of families of fired redexes, avoiding pitfalls such as that of Example 6.15.

Lemma 6.19**.**

If $e\mathrel{{\Rightarrow_{{(b_{0})}}}}\epsilon^{\prime}$ and $\overline{u}\mathrel{{\Rightarrow_{{(b_{1})}}}}\overline{\upsilon^{\prime}}$ then $\partial_{x}e\cdot\overline{u}\mathrel{{\Rightarrow_{{(b_{0}+b_{1})}}}}\partial_{x}\epsilon^{\prime}\cdot\overline{\upsilon^{\prime}}$.

Proof 6.20**.**

Write $\overline{u}={\left[u_{1},\dotsc,u_{n}\right]}$. Then we can write $\overline{\upsilon^{\prime}}={\left[\upsilon^{\prime}_{1},\dotsc,\upsilon^{\prime}_{n}\right]}$ with $u_{i}\mathrel{{\Rightarrow_{{(b_{1})}}}}{\upsilon^{\prime}}_{i}$ for all $i\in{\left\{1,\dotsc,n\right\}}$. Recall that whenever $I={\left\{i_{1},\dotsc,i_{k}\right\}}\subseteq{\left\{1,\dotsc,n\right\}}$ with $\mathord{\#}{I}=k$, we write $\overline{u}_{I}={\left[u_{i_{1}},\dotsc,u_{i_{k}}\right]}$ and $\overline{\upsilon^{\prime}}_{I}={\left[\upsilon^{\prime}_{i_{1}},\dotsc,\upsilon^{\prime}_{i_{k}}\right]}$.

The proof is by induction on the reduction $e\mathrel{{\Rightarrow_{{(b_{0})}}}}\epsilon^{\prime}$. If $e=y=\epsilon^{\prime}$ then:

• •

if $y=x$ and $n=1$ then $\partial_{x}e\cdot\overline{u}=u_{1}\mathrel{{\Rightarrow_{{(b_{1})}}}}\upsilon^{\prime}_{1}=\partial_{x}\epsilon^{\prime}\cdot\overline{\upsilon^{\prime}}^{\prime}$;

• •

if $y\not=x$ and $\overline{u}={\left[\right]}$ then $\partial_{x}e\cdot\overline{u}=y\mathrel{{\Rightarrow_{{(0)}}}}y=\partial_{x}\epsilon^{\prime}\cdot\overline{\upsilon^{\prime}}$;

• •

otherwise, $\partial_{x}e\cdot\overline{u}=0\mathrel{{\Rightarrow_{{(0)}}}}0=\partial_{x}\epsilon^{\prime}\cdot\overline{\upsilon^{\prime}}$.

If $e=\lambda y\,{s}$ (choosing $y\not=x$ and $y\not\in\mathord{\mathbf{fv}}{\left(\overline{u}\right)}$), $\epsilon^{\prime}=\lambda y\,{\sigma^{\prime}}$ and $s\mathrel{{\Rightarrow_{{(b_{0})}}}}\sigma^{\prime}$ then, by induction hypothesis, $\partial_{x}s\cdot\overline{u}\mathrel{{\Rightarrow_{{(b_{0}+b_{1})}}}}\partial_{x}\sigma^{\prime}\cdot\overline{\upsilon^{\prime}}$. We obtain: $\partial_{x}e\cdot\overline{u}=\lambda y\,{\left(\partial_{x}s\cdot\overline{u}\right)}\mathrel{{\Rightarrow_{{(b_{0}+b_{1})}}}}\lambda y\,{\left(\partial_{x}\sigma^{\prime}\cdot\overline{\upsilon^{\prime}}\right)}=\partial_{x}\epsilon^{\prime}\cdot\overline{\upsilon^{\prime}}$.

If $e={\left\langle s\right\rangle}\,{\overline{t}}$, $\epsilon^{\prime}={\left\langle\sigma^{\prime}\right\rangle}\,{\overline{\tau^{\prime}}}$, $s\mathrel{{\Rightarrow_{{(b_{0})}}}}\sigma^{\prime}$ and $\overline{t}\mathrel{{\Rightarrow_{{(b_{0})}}}}\overline{\tau^{\prime}}$ then, by induction hypothesis, $\partial_{x}s\cdot\overline{u}_{I}\mathrel{{\Rightarrow_{{(b_{0}+b_{1})}}}}\partial_{x}\sigma^{\prime}\cdot\overline{\upsilon^{\prime}}_{I}$ and $\partial_{x}\overline{t}\cdot\overline{u}_{I}\mathrel{{\Rightarrow_{{(b_{0}+b_{1})}}}}\partial_{x}\overline{\tau^{\prime}}\cdot\overline{\upsilon^{\prime}}_{I}$, for all $I\subseteq{\left\{1,\dotsc,n\right\}}$. We obtain:

[TABLE]

If $e={\left[s_{1},\dotsc,s_{r}\right]}$, $\epsilon^{\prime}={\left[\sigma^{\prime}_{1},\dotsc,\sigma^{\prime}_{r}\right]}$ and $s_{i}\mathrel{{\Rightarrow_{{(b_{0})}}}}\sigma^{\prime}_{i}$ for all $i\in{\left\{1,\dotsc,r\right\}}$ then, by induction hypothesis, $\partial_{x}s_{i}\cdot\overline{u}_{I}\mathrel{{\Rightarrow_{{(b_{0}+b_{1})}}}}\partial_{x}\sigma^{\prime}_{i}\cdot\overline{\upsilon^{\prime}}_{I}$ for all $i\in{\left\{1,\dotsc,r\right\}}$ and all $I\subseteq{\left\{1,\dotsc,n\right\}}$. We obtain:

[TABLE]

If $e={\left\langle\lambda y\,{s}\right\rangle}\,{\overline{t}}$ (choosing $y\not=x$ and $y\not\in\mathord{\mathbf{fv}}{\left(\overline{t}\right)}\mathbin{\cup}\mathord{\mathbf{fv}}{\left(\overline{u}\right)}$), $\epsilon^{\prime}=\partial_{y}\sigma^{\prime}\cdot\overline{\tau^{\prime}}$, $b_{0}\geq 1$, $s\mathrel{{\Rightarrow_{{(b_{0}-1)}}}}\sigma^{\prime}$ and $\overline{t}\mathrel{{\Rightarrow_{{(b_{0}-1)}}}}\overline{\tau^{\prime}}$ then, by induction hypothesis, $\partial_{x}s\cdot\overline{u}_{I}\mathrel{{\Rightarrow_{{(b_{0}+b_{1}-1)}}}}\partial_{x}\sigma^{\prime}\cdot\overline{\upsilon^{\prime}}_{I}$ and $\partial_{x}\overline{t}\cdot\overline{u}_{I}\mathrel{{\Rightarrow_{{(b_{0}+b_{1}-1)}}}}\partial_{x}\overline{\tau^{\prime}}\cdot\overline{\upsilon^{\prime}}_{I}$, for all $I\subseteq{\left\{1,\dotsc,n\right\}}$. We obtain:

[TABLE]

using Lemma 3.3.

Lemma 6.21**.**

Let $K$ be a finite set, and assume $\epsilon\mathrel{{\Rightarrow_{{(b_{k})}}}}\epsilon^{\prime}_{k}$ for all $k\in K$. Then, setting $b=\sum_{k\in K}b_{k}$, there is $\epsilon^{\prime\prime}$ such that $\epsilon^{\prime}_{k}\mathrel{{\Rightarrow_{{(2^{\scriptstyle b_{k}}b)}}}}\epsilon^{\prime\prime}$ for all $k\in K$.

Proof 6.22**.**

By the linearity of the definition of reduction on finite sums, it is sufficient to address the case of $\epsilon=e\in(\oc)\Delta$. The proof is then by induction on the family of reductions $e\mathrel{{\Rightarrow_{{(b_{k})}}}}\epsilon^{\prime}_{k}$.

If $e=x=\epsilon^{\prime}_{k}$ for all $k\in K$, then we set $\epsilon^{\prime\prime}=x$.

If $e=\lambda x\,{s}$, and $\epsilon^{\prime}_{k}=\lambda x\,{\sigma^{\prime}_{k}}$ with $s\mathrel{{\Rightarrow_{{(b_{k})}}}}\sigma^{\prime}_{k}$ for all $k\in K$ then, by induction hypothesis, we have $\sigma^{\prime\prime}$ such that $\sigma^{\prime}_{k}\mathrel{{\Rightarrow_{{(2^{\scriptstyle b_{k}}b)}}}}\sigma^{\prime\prime}$ for all $k\in K$, and then we set $\epsilon^{\prime\prime}=\lambda x\,{\sigma^{\prime\prime}}$.

If $e={\left[s_{1},\dotsc,s_{r}\right]}$ and $\epsilon^{\prime}_{k}={\left[\sigma^{\prime}_{1,k},\dotsc,\sigma^{\prime}_{r,k}\right]}$ with $s_{j}\mathrel{{\Rightarrow_{{(b_{k})}}}}\sigma^{\prime}_{j,k}$ for all $j\in{\left\{1,\dotsc,r\right\}}$ and $k\in K$ then, by induction hypothesis, we have $\sigma^{\prime\prime}_{j}$ such that $\sigma^{\prime}_{j,k}\mathrel{{\Rightarrow_{{(2^{\scriptstyle b_{k}}b)}}}}\sigma^{\prime\prime}_{j}$ for all $j\in{\left\{1,\dotsc,r\right\}}$ and $k\in K$, and then we set $\epsilon^{\prime\prime}={\left[\sigma^{\prime\prime}_{1},\dotsc,\sigma^{\prime\prime}_{r}\right]}$.

Finally, assume $K=K_{0}+K_{1}$, $e={\left\langle\lambda x\,{s}\right\rangle}\,{\overline{t}}$ and:

• •

for all $k\in K_{0}$, $\epsilon^{\prime}_{k}={\left\langle\lambda x\,{\sigma^{\prime}_{k}}\right\rangle}\,{\overline{\tau^{\prime}}_{k}}$ with $s\mathrel{{\Rightarrow_{{(b_{k})}}}}\sigma^{\prime}_{k}$ and $\overline{t}\mathrel{{\Rightarrow_{{(b_{k})}}}}\overline{\tau^{\prime}}_{k}$;

• •

for all $k\in K_{1}$, $b_{k}\geq 1$ and $\epsilon^{\prime}_{k}=\partial_{x}\sigma^{\prime}_{k}\cdot\overline{\tau^{\prime}}_{k}$ with $s\mathrel{{\Rightarrow_{{(b_{k}-1)}}}}\sigma^{\prime}_{k}$ and $\overline{t}\mathrel{{\Rightarrow_{{(b_{k}-1)}}}}\overline{\tau^{\prime}}_{k}$.

Write $b^{\prime}=b-\mathord{\#}{K_{1}}$. By induction hypothesis, there are $\sigma^{\prime\prime}$ and $\overline{\tau^{\prime\prime}}$ such that, for all $k\in K_{0}$, $\sigma^{\prime}_{k}\mathrel{{\Rightarrow_{{(2^{\scriptstyle b_{k}}b^{\prime})}}}}\sigma^{\prime\prime}$ and $\overline{\tau^{\prime}}_{k}\mathrel{{\Rightarrow_{{(2^{\scriptstyle b_{k}}b^{\prime})}}}}\overline{\tau^{\prime\prime}}$, and for all $k\in K_{1}$, \sigma^{\prime}_{k}\mathrel{{\Rightarrow_{{\bigl{(}2^{\scriptstyle(b_{k}-1)}b^{\prime}\bigr{)}}}}}\sigma^{\prime\prime} and \overline{\tau^{\prime}}_{k}\mathrel{{\Rightarrow_{{\bigl{(}2^{\scriptstyle(b_{k}-1)}b^{\prime}\bigr{)}}}}}\overline{\tau^{\prime\prime}}.

If $K_{1}=\emptyset$ then $b=b^{\prime}$ and we set $\epsilon^{\prime\prime}={\left\langle\lambda x\,{\sigma^{\prime\prime}}\right\rangle}\,{\overline{\tau^{\prime\prime}}}$: we obtain $\epsilon^{\prime}_{k}\mathrel{{\Rightarrow_{{(2^{\scriptstyle b_{k}}b)}}}}\epsilon^{\prime\prime}$, for all $k\in K=K_{0}$.

Otherwise, $b>b^{\prime}$ and we set $\epsilon^{\prime\prime}=\partial_{x}\sigma^{\prime\prime}\cdot\overline{\tau^{\prime\prime}}$ so that:

• •

for all $k\in K_{0}$, $\epsilon^{\prime}_{k}={\left\langle\lambda x\,{\sigma^{\prime}_{k}}\right\rangle}\,{\overline{\tau^{\prime}}_{k}}\mathrel{{\Rightarrow_{{(2^{\scriptstyle b_{k}}b^{\prime}+1)}}}}\sigma^{\prime}_{k}$ with $2^{b_{k}}b^{\prime}+1\leq 2^{b_{k}}b$;

• •

for all $k\in K_{1}$, by the previous lemma, $\epsilon^{\prime}_{k}=\partial_{x}\sigma^{\prime}_{k}\cdot\overline{\tau^{\prime}}_{k}\mathrel{{\Rightarrow_{{(2^{\scriptstyle b_{k}}b^{\prime})}}}}\sigma^{\prime}_{k}$ and $2^{b_{k}}b^{\prime}<2^{b_{k}}b$.

We already know $\mathrel{{\widetilde{\Rightarrow_{\partial}}}}$ is not confluent, and the counter examples we provided actually show that no single $\mathrel{{\widetilde{\Rightarrow_{{(b)}}}}}$ is confluent either. Setting191919 Our notation is somehow abusive as $\mathrel{{\widetilde{\Rightarrow_{{(\partial)}}}}}$ is not of the form described in Definition 5.10: there should not be any ambiguity as we have not defined any relation $\mathrel{{\Rightarrow_{{(\partial)}}}}$. Similarly, we may also write $\mathrel{{\widetilde{\Rightarrow_{{(\partial)}}}_{\mathfrak{E}}}}$ for $\bigcup_{b\in\mathbf{N}}\mathord{\mathrel{{\widetilde{\Rightarrow_{{(b)}}}_{\mathfrak{E}}}}}$ in the following.

[TABLE]

however, we will obtain a strongly confluent reduction relation, under the assumption that $\mathbf{S}$ has the following additive splitting property:202020 The additive splitting property was previously used by Carraro, Ehrhard and Salibra [CES10, Car11] in their study of linear logic exponentials with infinite multiplicities. There is no clear connection between that work and our present contributions, though.

Definition 6.23**.**

We say $\mathbf{S}$ has the additive splitting property if: whenever $a_{1}+a_{2}=b_{1}+b_{2}\in\mathbf{S}$, there exists $c_{1,1},c_{1,2},c_{2,1},c_{2,2}\in\mathbf{S}$ such that $a_{i}=c_{i,1}+c_{i,2}$ and $b_{j}=c_{1,j}+c_{2,j}$ for $i,j\in{\left\{1,2\right\}}$.

This property is satisfied by any ring, but also by the usual semirings of non-negative numbers ($\mathbf{N}$, $\mathbf{Q}^{+}$, etc.) as well as booleans. We will in fact rely on the following generalization of the property to finite families of finite sums of any size:

Lemma 6.24**.**

Assume $\mathbf{S}$ has the additive splitting property. Let $a\in\mathbf{S}$, $J_{1},\dotsc,J_{n}$ be finite sets and, for all $i\in{\left\{1,\dotsc,n\right\}}$, let ${\left(b_{i,j}\right)}_{j\in J_{i}}\in\mathbf{S}^{J_{i}}$ be a family such that $a=\sum_{j\in J_{i}}b_{i,j}$. Write $J=J_{1}\times\cdots\times J_{n}$ and, for all $i\in{\left\{1,\dotsc,n\right\}}$, write $J^{\prime}_{i}=J_{1}\times\cdots\times J_{i-1}\times J_{i+1}\times\cdots\times J_{n}$. Whenever $\overrightarrow{\jmath}^{\prime}=(j_{1},\dotsc,j_{i-1},j_{i+1},\dotsc,j_{n})\in J^{\prime}_{i}$ and $j_{i}\in J_{i}$, write $\overrightarrow{\jmath}^{\prime}\cdot_{i}j_{i}=(j_{1},\dotsc,j_{n})\in J$. Then there exists a family ${\left(c_{\overrightarrow{\jmath}}\right)}\in\mathbf{S}^{J}$ such that, for all $i\in{\left\{1,\dotsc,n\right\}}$ and all $j\in J_{i}$, $b_{i,j}=\sum_{\overrightarrow{\jmath}^{\prime}\in J^{\prime}_{i}}c_{\overrightarrow{\jmath}^{\prime}\cdot_{i}j}$.

Proof 6.25**.**

By induction on $n$, and then on $\mathord{\#}{J_{n}}$ for $n>0$, using the binary additive splitting property to enable the induction.

Lemma 6.26**.**

Assume $\mathbf{S}$ has the additive splitting property and fix a $\mathrel{{\Rightarrow_{\partial}}}$-reduction structure $\mathfrak{E}$. For all finite set $K$ and all reductions $\epsilon\mathrel{{\widetilde{\Rightarrow_{{(\partial)}}}_{\mathfrak{E}}}}\epsilon^{\prime}_{k}$ for $k\in K$, there is $\epsilon^{\prime\prime}$ such that $\epsilon^{\prime}_{k}\mathrel{{\widetilde{\Rightarrow_{{(\partial)}}}_{\mathfrak{E}}}}\epsilon^{\prime\prime}$ for all $k\in K$.

Proof 6.27**.**

For all $k\in K$, there are $b_{k}\in\mathbf{N}$, a resource support $\mathcal{E}_{k}\in\mathfrak{E}$, a set $I_{k}$ of indices, a family ${\left(a_{k,i}\right)}_{i\in I_{k}}$ of scalars, and summable families ${\left(e_{k,i}\right)}_{i\in I_{k}}\in\mathcal{E}_{k}^{I_{k}}$ and ${\left(\epsilon^{\prime}_{k,i}\right)}_{i\in I_{k}}\in\mathbf{N}{\left[(\oc)\Delta\right]}^{I_{k}}$ such that $\epsilon=\sum_{i\in I_{k}}a_{k,i}.e_{k,i}$, $\epsilon^{\prime}_{k}=\sum_{i\in I_{k}}a_{k,i}.\epsilon^{\prime}_{k,i}$ and $e_{k,i}\mathrel{{\Rightarrow_{{(b_{k})}}}}\epsilon^{\prime}_{k,i}$ for all $i\in I_{k}$.

Write $\mathcal{E}={\left\{e_{k,i}\mathrel{;}k\in K,\ i\in I_{k}\right\}}$: since $\mathcal{E}\subseteq\bigcup_{k\in K}\mathcal{E}_{k}$ and $\mathfrak{E}$ is a resource structure, we have $\mathcal{E}\in\mathfrak{E}$. Write $\mathcal{E}^{\prime}=\bigcup{\left\{{\left|\epsilon^{\prime}_{k,i}\right|}\mathrel{;}k\in K,\ i\in I_{k}\right\}}$: since $\mathfrak{E}$ is a reduction structure, we also have $\mathcal{E}^{\prime}\in\mathfrak{E}$.

Now fix $e\in(\oc)\Delta$ and write $a=\epsilon_{e}$. For all $k\in K$, the set $I_{e,k}={\left\{i_{k}\in I_{k}\mathrel{;}e_{k,i_{k}}=e\right\}}$ is finite, and then $\sum_{i_{k}\in I_{e,k}}a_{k,i_{k}}=a$. Write $I_{e}=\prod_{k\in K}I_{e,k}$ and, for all $k\in K$, $K^{\prime}_{k}=K\setminus{\left\{k\right\}}$ and $I^{\prime}_{e,k}=\prod_{l\in K^{\prime}_{k}}I_{e,l}$. If $\overrightarrow{\imath}={\left(i_{l}\right)}_{l\in K^{\prime}_{k}}\in I^{\prime}_{e,k}$ and $i_{k}\in I_{e,k}$, write $\overrightarrow{\imath}\cdot_{k}i_{k}={\left(i_{k}\right)}_{k\in K}\in I_{e}$. By Lemma 6.24, we obtain a family of scalars ${\left(a^{\prime}_{e,\overrightarrow{\imath}}\right)}_{\overrightarrow{\imath}\in I_{e}}$ such that, for all $k\in K$ and all $i_{k}\in I_{e,k}$, $a_{k,i_{k}}=\sum_{\overrightarrow{\imath}\in I^{\prime}_{e,k}}a^{\prime}_{e,\overrightarrow{\imath}\cdot_{k}i_{k}}$. Moreover, $a=\sum_{\overrightarrow{\imath}\in I_{e}}a^{\prime}_{e,\overrightarrow{\imath}}$.

Since each $I_{e}$ is finite, the family ${\left(e\right)}_{e\in(\oc)\Delta,\overrightarrow{\imath}\in I_{e}}$ is summable. Moreover, if we fix $k\in K$ and $i_{k}\in I_{k}$, there are finitely many $e\in(\oc)\Delta$ and $\overrightarrow{\imath}\in I^{\prime}_{e,k}$ such that $\overrightarrow{\imath}\cdot_{k}i_{k}\in I_{e}$: indeed in this case $e=e_{k,i_{k}}$. Since ${\left(\epsilon^{\prime}_{k,i_{k}}\right)}_{i_{k}\in I_{k}}$ is summable too, it follows that ${\left(\epsilon^{\prime}_{k,i_{k}}\right)}_{e\in(\oc)\Delta,\overrightarrow{\imath}\in I_{e}}$ is summable. By associativity, we obtain

[TABLE]

and

[TABLE]

for all $k\in K$.

Write $b=\sum_{k\in K}b_{k}$. For all $e\in(\oc)\Delta$ and all $\overrightarrow{\imath}={\left(i_{k}\right)}_{k\in K}\in I_{e}$, we have $e\mathrel{{\Rightarrow_{{(b_{k})}}}}\epsilon^{\prime}_{k,i_{k}}$ for all $k\in K$ hence Lemma 6.21 gives $\epsilon^{\prime\prime}_{e,\overrightarrow{\imath}}\in\mathbf{N}{\left[(\oc)\Delta\right]}$ such that $\epsilon^{\prime}_{k,i_{k}}\mathrel{{\Rightarrow_{{(2^{\scriptstyle b_{k}}b)}}}}\epsilon^{\prime\prime}_{e,\overrightarrow{\imath}}$ for all $k\in K$. Moreover, for all $k\in K$ and $e^{\prime\prime}\in(\oc)\Delta$, if $e^{\prime\prime}\in{\left|\epsilon^{\prime\prime}_{e,\overrightarrow{\imath}}\right|}$ then there is $e^{\prime}\in{\left|\epsilon^{\prime}_{k,i_{k}}\right|}$ such that $e^{\prime}{}_{{(2^{\scriptstyle b_{k}}b)}}e^{\prime\prime}$, and then $e{}_{{(b_{k})}}e^{\prime}$: it follows that $\mathord{\mathbf{s}}{\left(e\right)}\leq 4^{b_{k}+2^{b_{k}}b}\mathord{\mathbf{s}}{\left(e^{\prime\prime}\right)}$ and $\mathord{\mathbf{fv}}{\left(e\right)}=\mathord{\mathbf{fv}}{\left(e^{\prime\prime}\right)}$. Since each $I_{e}$ is finite, there are finitely many pairs ${\left(e,\overrightarrow{\imath}\right)}\in\sum_{e\in(\oc)\Delta}I_{e}$ such that $e^{\prime\prime}\in{\left|\epsilon^{\prime\prime}_{e,\overrightarrow{\imath}}\right|}$. Hence the family ${\left(\epsilon^{\prime\prime}_{e,\overrightarrow{\imath}}\right)}_{e\in(\oc)\Delta,\overrightarrow{\imath}\in I_{e}}$ is summable. Recall moreover that $\epsilon^{\prime}_{k,i_{k}}\in\mathbf{N}{\left[\mathcal{E}^{\prime}\right]}$ for all $k\in K$ and $i_{k}\in I_{k}$: we obtain

[TABLE]

for all $k\in K$, which concludes the proof.

6.3. Bounded depth of substitution

In the previous subsection, we relied on the additive splitting property to establish the confluence of $\mathrel{{\widetilde{\Rightarrow_{{(\partial)}}}}}$: this is because there is no maximal way to $\mathrel{{\widetilde{\Rightarrow_{{(b)}}}}}$-reduce a resource vector, hence we must track precisely the different redexes that are fired in each reduction of a critical pair.

We can get rid of this hypothesis by considering a more uniform bound on reductions. A first intuition would be to bound the depth at which redexes are fired, but as with $\mathrel{{\Rightarrow_{{\left(m|k\right)}}}}$ this boundedness condition is not preserved in residuals: rather, we have to bound the depth at which variables are substituted. First recall from Definition 3.1 that $\mathbf{md}_{x}{\left(s\right)}=\max\mathbf{d}_{x}{\left(s\right)}$ is the maximum depth of an occurrence of $x$ in $s$. Then:

Definition 6.28**.**

We define a family of relations ${\left(\mathrel{{\Rightarrow_{{\lfloor d\rfloor}}}}\right)}_{d\in{\mathbf{N}}}$ inductively as follows:

• •

$e\mathrel{{\Rightarrow_{{\lfloor 0\rfloor}}}}e$ for all $e\in(\oc)\Delta$;

• •

$x\mathrel{{\Rightarrow_{{\lfloor d+1\rfloor}}}}x$ for all $x\in\mathcal{V}$;

• •

$\lambda x\,{s}\mathrel{{\Rightarrow_{{\lfloor d+1\rfloor}}}}\lambda x\,{\sigma^{\prime}}$ if $s\mathrel{{\Rightarrow_{{\lfloor d\rfloor}}}}\sigma^{\prime}$;

• •

${\left\langle s\right\rangle}\,{\overline{t}}\mathrel{{\Rightarrow_{{\lfloor d+1\rfloor}}}}{\left\langle\sigma^{\prime}\right\rangle}\,{\overline{\tau^{\prime}}}$ if $s\mathrel{{\Rightarrow_{{\lfloor d+1\rfloor}}}}\sigma^{\prime}$ and $\overline{t}\mathrel{{\Rightarrow_{{\lfloor d\rfloor}}}}\overline{\tau^{\prime}}$;

• •

${\left[s_{1},\dotsc,s_{r}\right]}\mathrel{{\Rightarrow_{{\lfloor d+1\rfloor}}}}{\left[\sigma^{\prime}_{1},\dotsc,\sigma^{\prime}_{r}\right]}$ if $s_{i}\mathrel{{\Rightarrow_{{\lfloor d+1\rfloor}}}}\sigma^{\prime}_{i}$ for all $i\in{\left\{1,\dotsc,r\right\}}$;

• •

${\left\langle\lambda x\,{s}\right\rangle}\,{\overline{t}}\mathrel{{\Rightarrow_{{\lfloor d+1\rfloor}}}}\partial_{x}\sigma^{\prime}\cdot\overline{\tau^{\prime}}$ if $\mathbf{md}_{x}{\left(s\right)}\leq d$, $s\mathrel{{\Rightarrow_{{\lfloor d\rfloor}}}}\sigma^{\prime}$ and $\overline{t}\mathrel{{\Rightarrow_{{\lfloor d\rfloor}}}}\overline{\tau^{\prime}}$.

It should be clear that if $e\mathrel{{\Rightarrow_{{\lfloor d\rfloor}}}}\epsilon^{\prime}$ then $e\mathrel{{\Rightarrow_{{(d)}}}}\epsilon^{\prime}$, and moreover $e\mathrel{{\Rightarrow_{{\lfloor d^{\prime}\rfloor}}}}\epsilon^{\prime}$ for all $d^{\prime}\geq d$. We also have $e\mathrel{{\Rightarrow_{{\lfloor\mathord{\mathbf{h}}{\left(e\right)}\rfloor}}}}\epsilon^{\prime}$ as soon as $e\mathrel{{\Rightarrow_{\partial}}}\epsilon^{\prime}$.

Definition 6.29**.**

For all $e\in(\oc)\Delta$ we define the full parallel reduct $\mathord{\mathsf{F}}_{{\lfloor d\rfloor}}{\left(e\right)}$ at substitution depth $d$ of $e$ by induction on the pair $(d,e)$ as follows:

[TABLE]

Then if $\epsilon=\sum_{i=1}^{n}e_{i}\in\mathbf{N}{\left[(\oc)\Delta\right]}$, we set $\mathord{\mathsf{F}}_{{\lfloor d\rfloor}}{\left(\epsilon\right)}\mathrel{\mathord{:}\mathord{=}}\sum_{i=1}^{n}\mathord{\mathsf{F}}_{{\lfloor d\rfloor}}{\left(e_{i}\right)}$.

Lemma 6.30**.**

For all $e\in(\oc)\Delta$, $e\mathrel{{\Rightarrow_{{\lfloor d\rfloor}}}}\mathord{\mathsf{F}}_{{\lfloor d\rfloor}}{\left(e\right)}$.

Proof 6.31**.**

By a straightforward induction on $d$ then on $e$.

It follows that $e\mathrel{{\Rightarrow_{{(d)}}}}\mathord{\mathsf{F}}_{{\lfloor d\rfloor}}{\left(e\right)}$, hence if $e^{\prime}\in{\left|\mathord{\mathsf{F}}_{{\lfloor d\rfloor}}{\left(e\right)}\right|}$ then $\mathord{\mathbf{s}}{\left(e\right)}\leq 4^{d}\mathord{\mathbf{s}}{\left(e^{\prime}\right)}$. In particular $\mathord{\mathsf{F}}_{{\lfloor d\rfloor}}$ defines a linear-continuous function on $\mathbf{S}^{(\oc)\Delta}$.

Lemma 6.32**.**

If $e\mathrel{{\Rightarrow_{{\lfloor d_{0}\rfloor}}}}\epsilon^{\prime}$, $\overline{u}\mathrel{{\Rightarrow_{{\lfloor d_{1}\rfloor}}}}{\overline{\upsilon}^{\prime}}$ and $d\geq\max{\left({\left\{d_{0}\right\}}\mathbin{\cup}{\left\{d_{x}+d_{1}-1\mathrel{;}d_{x}\in\mathbf{d}_{x}{\left(e\right)}\right\}}\right)}$ then $\partial_{x}e\cdot\overline{u}\mathrel{{\Rightarrow_{{\lfloor d\rfloor}}}}\partial_{x}\epsilon^{\prime}\cdot\overline{\upsilon}^{\prime}$.

Proof 6.33**.**

Write $n=\mathord{\#}{\overline{u}}$, $\overline{u}={\left[u_{1},\dotsc,u_{n}\right]}$ and $\overline{\upsilon}^{\prime}={\left[\upsilon^{\prime}_{1},\dotsc,\upsilon^{\prime}_{n}\right]}$ so that $u_{i}\mathrel{{\Rightarrow_{{\lfloor d_{1}\rfloor}}}}\upsilon^{\prime}_{i}$ for $i\in{\left\{1,\dotsc,n\right\}}$.

The proof is by induction on the reduction $e\mathrel{{\Rightarrow_{{\lfloor d_{0}\rfloor}}}}{\epsilon^{\prime}}$. We treat the cases $d_{0}=0$ and $d_{0}>0$ uniformly by a further induction on $e$, setting $d^{\prime}_{0}=\max{\left\{0,d_{0}-1\right\}}$.

If $d_{0}=d^{\prime}_{0}+1$, $e={\left\langle\lambda y\,{s}\right\rangle}\,{\overline{t}}$ and $\epsilon^{\prime}=\partial_{y}\sigma^{\prime}\cdot\overline{\tau}^{\prime}$ with $y\not\in{\left\{x\right\}}\mathbin{\cup}\mathord{\mathbf{fv}}{\left(\overline{t}\right)}\mathbin{\cup}\mathord{\mathbf{fv}}{\left(\overline{u}\right)}$, $\mathbf{md}_{y}{\left(s\right)}\leq{d^{\prime}_{0}}$, $s\mathrel{{\Rightarrow_{{\lfloor d^{\prime}_{0}\rfloor}}}}\sigma^{\prime}$ and $\overline{t}\mathrel{{\Rightarrow_{{\lfloor d^{\prime}_{0}\rfloor}}}}\overline{\tau}^{\prime}$, then we have

[TABLE]

and

[TABLE]

Observe that $d>0$ and $d-1\geq\max{\left\{d^{\prime}_{0}\right\}}\mathbin{\cup}{\left\{d^{\prime}_{x}+d_{1}-1\mathrel{;}d^{\prime}_{x}\in\mathbf{d}_{x}{\left(s\right)}\mathbin{\cup}\mathbf{d}_{x}{\left(\overline{t}\right)}\right\}}$. By induction hypothesis, we obtain $\partial_{x}s\cdot\overline{u}_{I}\mathrel{{\Rightarrow_{{\lfloor d-1\rfloor}}}}\partial_{x}\sigma^{\prime}\cdot\overline{\upsilon}^{\prime}_{I}$ and $\partial_{x}\overline{t}\cdot\overline{u}_{J}\mathrel{{\Rightarrow_{{\lfloor d-1\rfloor}}}}\partial_{x}\overline{\tau}^{\prime}\cdot\overline{\upsilon}^{\prime}_{J}$, and we conclude since $\mathbf{md}_{y}{\left(\partial_{x}s\cdot\overline{u}_{I}\right)}=\mathbf{md}_{y}{\left(s\right)}\leq d^{\prime}_{0}\leq d-1$.

If $e=y=\epsilon^{\prime}$, with $y\not=x$, then $\partial_{x}e\cdot\overline{u}=\partial_{x}\epsilon^{\prime}\cdot\overline{\upsilon}^{\prime}=y$ and we conclude directly by the definition of $\mathrel{{\Rightarrow_{{\lfloor d\rfloor}}}}$.

If $e=x=\epsilon^{\prime}$, then $\mathbf{d}_{x}{\left(e\right)}={\left\{1\right\}}$ hence $d\geq d_{1}$ and we conclude since $\partial_{x}e\cdot\overline{u}=\overline{u}$, $\partial_{x}\epsilon^{\prime}\cdot\overline{\upsilon}^{\prime}=\overline{\upsilon}^{\prime}$ and $\overline{u}\mathrel{{\Rightarrow_{{\lfloor d_{1}\rfloor}}}}{\overline{\upsilon}^{\prime}}$.

If $e=\lambda y\,{s}$ and $\epsilon^{\prime}=\lambda y\,{\sigma^{\prime}}$ with $y\not\in{\left\{x\right\}}\mathbin{\cup}\mathord{\mathbf{fv}}{\left(\overline{u}\right)}$ and $s\mathrel{{\Rightarrow_{{\lfloor d^{\prime}_{0}\rfloor}}}}\sigma^{\prime}$, then write $d^{\prime}=\max{\left\{d^{\prime}_{0}\right\}}\mathbin{\cup}{\left\{d^{\prime}_{x}+d_{1}-1\mathrel{;}d^{\prime}_{x}\in\mathbf{d}_{x}{\left(s\right)}\right\}}$. By induction hypothesis, we obtain $\partial_{x}s\cdot\overline{u}\mathrel{{\Rightarrow_{{\lfloor d^{\prime}\rfloor}}}}\partial_{x}\sigma^{\prime}\cdot\overline{\upsilon}^{\prime}$. Observe that either $d=d^{\prime}+1$ or $d=d^{\prime}=0$ (in that latter case, $\partial_{x}s\cdot\overline{u}=\partial_{x}\sigma^{\prime}\cdot\overline{\upsilon}^{\prime}$), and then we conclude since $\partial_{x}e\cdot\overline{u}=\lambda y\,{\left(\partial_{x}s\cdot\overline{u}\right)}$ and $\partial_{x}\epsilon^{\prime}\cdot\overline{\upsilon}^{\prime}=\lambda y\,{\left(\partial_{x}\sigma^{\prime}\cdot\overline{\upsilon}^{\prime}\right)}$.

If $e={\left\langle s\right\rangle}\,{\overline{t}}$ and $\epsilon^{\prime}={\left\langle\sigma^{\prime}\right\rangle}\,{\overline{\tau}^{\prime}}$, with $s\mathrel{{\Rightarrow_{{\lfloor d_{0}\rfloor}}}}\sigma^{\prime}$ and $\overline{t}\mathrel{{\Rightarrow_{{\lfloor d^{\prime}_{0}\rfloor}}}}\overline{\tau}^{\prime}$, then we have

[TABLE]

and

[TABLE]

Write $d^{\prime}=\max{\left\{d^{\prime}_{0}\right\}}\mathbin{\cup}{\left\{d^{\prime}_{x}+d_{1}-1\mathrel{;}d^{\prime}_{x}\in\mathbf{d}_{x}{\left(\overline{t}\right)}\right\}}$. By induction hypothesis, we obtain $\partial_{x}s\cdot\overline{u}_{I}\mathrel{{\Rightarrow_{{\lfloor d\rfloor}}}}\partial_{x}\sigma^{\prime}\cdot\overline{\upsilon}^{\prime}_{I}$ and $\partial_{x}\overline{t}\cdot\overline{u}_{J}\mathrel{{\Rightarrow_{{\lfloor d^{\prime}\rfloor}}}}\partial_{x}\overline{\tau}^{\prime}\cdot\overline{\upsilon}^{\prime}_{J}$. Then we conclude observing that $d=d^{\prime}+1$ or $d=d^{\prime}=0$ (in that latter case, $\partial_{x}s\cdot\overline{u}_{I}=\partial_{x}\sigma^{\prime}\cdot\overline{\upsilon}^{\prime}_{I}$ and $\partial_{x}\overline{t}\cdot\overline{u}_{J}=\partial_{x}\overline{\tau}^{\prime}\cdot\overline{u}^{\prime}_{J}$).

If $e={\left[s_{1},\dotsc,s_{k}\right]}$ and $\epsilon^{\prime}={\left[\sigma^{\prime}_{1},\dotsc,\sigma^{\prime}_{k}\right]}$, with $s_{i}\mathrel{{\Rightarrow_{{\lfloor d_{0}\rfloor}}}}\sigma^{\prime}_{i}$ for $i\in{\left\{1,\dotsc,k\right\}}$, then we have

[TABLE]

and

[TABLE]

By induction hypothesis, we obtain

[TABLE]

for all partition $(I_{1},\dotsc,I_{k})$ of ${\left\{1,\dotsc,n\right\}}$ and we conclude.

Lemma 6.34**.**

If $e\mathrel{{\Rightarrow_{{\lfloor d\rfloor}}}}\epsilon^{\prime}$ and $e^{\prime}\in{\left|\epsilon^{\prime}\right|}$ then $\mathbf{md}_{x}{\left(e^{\prime}\right)}\leq 2^{d}\max{\left\{d,\mathbf{md}_{x}{\left(e\right)}\right\}}$.

Proof 6.35**.**

By induction on the reduction $e\mathrel{{\Rightarrow_{{\lfloor d\rfloor}}}}\epsilon^{\prime}$.

If $d=0$, then $e^{\prime}=\epsilon^{\prime}=e$ and the result is trivial. For the other inductive cases, write $d=d^{\prime}+1$.

If $e={\left\langle\lambda y\,{s}\right\rangle}\,{\overline{t}}$ and $\epsilon^{\prime}=\partial_{y}\sigma^{\prime}\cdot\overline{\tau}^{\prime}$ with $\mathbf{md}_{y}{\left(s\right)}\leq d^{\prime}$, $s\mathrel{{\Rightarrow_{{\lfloor d^{\prime}\rfloor}}}}\sigma^{\prime}$ and $\overline{t}\mathrel{{\Rightarrow_{{\lfloor d^{\prime}\rfloor}}}}\overline{\tau}^{\prime}$, choosing $y\not\in{\left\{x\right\}}\mathbin{\cup}\mathord{\mathbf{fv}}{\left(\overline{t}\right)}$, then e^{\prime}\in{\bigl{|}\partial_{y}s^{\prime}\cdot\overline{t}^{\prime}\bigr{|}} with $s^{\prime}\in{\left|\sigma^{\prime}\right|}$ and $\overline{t}^{\prime}\in{\left|\overline{\tau}^{\prime}\right|}$. By induction hypothesis, $\mathbf{md}_{z}{\left(s^{\prime}\right)}\leq 2^{d^{\prime}}\max{\left\{d^{\prime},\mathbf{md}_{z}{\left(s\right)}\right\}}$ and $\mathbf{md}_{z}{(\overline{t}^{\prime})}\leq 2^{d^{\prime}}\max{\left\{d^{\prime},\mathbf{md}_{z}{\left(\overline{t}\right)}\right\}}$ for any $z\in\mathcal{V}$. By Lemma 3.3,

[TABLE]

If $e=\lambda y\,{s}$ and $\epsilon^{\prime}=\lambda y\,{\sigma^{\prime}}$ with $s\mathrel{{\Rightarrow_{{\lfloor d^{\prime}\rfloor}}}}\sigma^{\prime}$, choosing $y\not=x$, then $e^{\prime}=\lambda x\,{s^{\prime}}$ with $s^{\prime}\in{\left|\sigma^{\prime}\right|}$. By induction hypothesis, $\mathbf{md}_{x}{\left(s^{\prime}\right)}\leq 2^{d^{\prime}}\max{\left\{d^{\prime},\mathbf{md}_{x}{\left(s\right)}\right\}}$. Then $\mathbf{md}_{x}{\left(e^{\prime}\right)}\leq\mathbf{md}_{x}{\left(s^{\prime}\right)}+1\leq 2^{d^{\prime}}\max{\left\{d^{\prime},\mathbf{md}_{x}{\left(s\right)}\right\}}+1\leq 2^{d}\max{\left\{d,\mathbf{md}_{x}{\left(s\right)}\right\}}\leq 2^{d}\max{\left\{d,\mathbf{md}_{x}{\left(e\right)}\right\}}$.

If $e={\left\langle s\right\rangle}\,{\overline{t}}$ and $\epsilon^{\prime}={\left\langle\sigma^{\prime}\right\rangle}\,{\overline{\tau}^{\prime}}$ with $s\mathrel{{\Rightarrow_{{\lfloor d\rfloor}}}}\sigma^{\prime}$ and $\overline{t}\mathrel{{\Rightarrow_{{\lfloor d^{\prime}\rfloor}}}}\overline{\tau}^{\prime}$, then $e^{\prime}={\left\langle s^{\prime}\right\rangle}\,{\overline{t}^{\prime}}$ with $s^{\prime}\in{\left|\sigma^{\prime}\right|}$ and $\overline{t}^{\prime}\in{\left|\overline{\tau}^{\prime}\right|}$. By induction hypothesis, $\mathbf{md}_{x}{\left(s^{\prime}\right)}\leq 2^{d}\max{\left\{d,\mathbf{md}_{x}{\left(s\right)}\right\}}$ and $\mathbf{md}_{x}{(\overline{t}^{\prime})}\leq 2^{d^{\prime}}\max{\left\{d^{\prime},\mathbf{md}_{x}{\left(\overline{t}\right)}\right\}}$. Then:

[TABLE]

If $e={\left[s_{1},\dotsc,s_{k}\right]}$ and $\epsilon^{\prime}={\left[\sigma^{\prime}_{1},\dotsc,\sigma^{\prime}_{k}\right]}$, with $s_{i}\mathrel{{\Rightarrow_{{\lfloor d\rfloor}}}}\sigma^{\prime}_{i}$ for all $i\in{\left\{1,\dotsc,k\right\}}$, then $e^{\prime}={\left[s^{\prime}_{1},\dotsc,s^{\prime}_{k}\right]}$ with $s^{\prime}_{i}\in{\left|\sigma^{\prime}_{i}\right|}$ for all $i\in{\left\{1,\dotsc,k\right\}}$. By induction hypothesis, for all $i\in{\left\{1,\dotsc,k\right\}}$, $\mathbf{md}_{x}{\left(s^{\prime}_{i}\right)}\leq 2^{d}\max{\left\{d,\mathbf{md}_{x}{\left(s_{i}\right)}\right\}}$, hence

[TABLE]

Lemma 6.36**.**

If $e\mathrel{{\Rightarrow_{{\lfloor d\rfloor}}}}\epsilon^{\prime}$ then $\epsilon^{\prime}\mathrel{{\Rightarrow_{{\lfloor 2^{d}d\rfloor}}}}\mathord{\mathsf{F}}_{{\lfloor d\rfloor}}{\left(e\right)}$.

Proof 6.37**.**

By induction on the reduction $e\mathrel{{\Rightarrow_{{\lfloor d\rfloor}}}}\epsilon^{\prime}$.

If $d=0$, then $\epsilon^{\prime}=e$ and the result follows from Lemma 6.30. For the other inductive cases, set $d=d^{\prime}+1$.

If $e={\left\langle\lambda x\,{s}\right\rangle}\,{\overline{t}}$ and $\epsilon^{\prime}=\partial_{x}\sigma^{\prime}\cdot\overline{\tau}^{\prime}$ with $\mathbf{md}_{x}{\left(s\right)}\leq{d^{\prime}}$, $s\mathrel{{\Rightarrow_{{\lfloor d^{\prime}\rfloor}}}}\sigma^{\prime}$ and $\overline{t}\mathrel{{\Rightarrow_{{\lfloor d^{\prime}\rfloor}}}}\overline{\tau}^{\prime}$ then by induction hypothesis, we have $\sigma^{\prime}\mathrel{{\Rightarrow_{{\lfloor 2^{d^{\prime}}d^{\prime}\rfloor}}}}\mathord{\mathsf{F}}_{{\lfloor d^{\prime}\rfloor}}{\left(s\right)}$ and $\overline{\tau}^{\prime}\mathrel{{\Rightarrow_{{\lfloor 2^{d^{\prime}}d^{\prime}\rfloor}}}}\mathord{\mathsf{F}}_{{\lfloor d^{\prime}\rfloor}}{\left(\overline{t}\right)}$. By the previous lemma, we moreover have $\mathbf{md}_{x}{\left(\sigma^{\prime}\right)}\leq 2^{d^{\prime}}\max{\left\{d^{\prime},\mathbf{md}_{x}{\left(s\right)}\right\}}=2^{d^{\prime}}d^{\prime}$. It follows that $2^{d}d\geq 2^{d^{\prime}}d^{\prime}$ and $2^{d}d\geq\mathbf{md}_{x}{\left(\sigma^{\prime}\right)}+2^{d^{\prime}}d^{\prime}-1$ hence we can apply Lemma 6.32 to obtain $\epsilon^{\prime}\mathrel{{\Rightarrow_{{\lfloor 2^{d}{d}\rfloor}}}}\partial_{x}\mathord{\mathsf{F}}_{{\lfloor d^{\prime}\rfloor}}{\left(s\right)}\cdot\mathord{\mathsf{F}}_{{\lfloor d^{\prime}\rfloor}}{\left(\overline{t}\right)}=\mathord{\mathsf{F}}_{{\lfloor d\rfloor}}{\left(e\right)}$.

If $e=\lambda y\,{s}$ and $\epsilon^{\prime}=\lambda y\,{\sigma^{\prime}}$ with $s\mathrel{{\Rightarrow_{{\lfloor d^{\prime}\rfloor}}}}\sigma^{\prime}$, then by induction hypothesis, $\sigma^{\prime}\mathrel{{\Rightarrow_{{\lfloor 2^{d^{\prime}}d^{\prime}\rfloor}}}}\mathord{\mathsf{F}}_{{\lfloor d^{\prime}\rfloor}}{\left(s\right)}$, hence $\epsilon^{\prime}\mathrel{{\Rightarrow_{{\lfloor 2^{d^{\prime}}d^{\prime}+1\rfloor}}}}\lambda x\,{\mathord{\mathsf{F}}_{{\lfloor d^{\prime}\rfloor}}{\left(s\right)}}=\mathord{\mathsf{F}}_{{\lfloor d\rfloor}}{\left(e\right)}$ and we conclude since $2^{d^{\prime}}d^{\prime}+1\leq 2^{d}d$.

If $e={\left\langle s\right\rangle}\,{\overline{t}}$ and $\epsilon^{\prime}={\left\langle\sigma^{\prime}\right\rangle}\,{\overline{\tau}^{\prime}}$ with $s\mathrel{{\Rightarrow_{{\lfloor d\rfloor}}}}\sigma^{\prime}$ and $\overline{t}\mathrel{{\Rightarrow_{{\lfloor d^{\prime}\rfloor}}}}\overline{\tau}^{\prime}$, there are two subcases:

• •

If moreover $s=\lambda x\,{u}$ and $\mathbf{md}_{x}{\left(u\right)}\leq d^{\prime}$ then $\sigma^{\prime}=\lambda x\,{\upsilon^{\prime}}$ with $u\mathrel{{\Rightarrow_{{\lfloor d^{\prime}\rfloor}}}}\upsilon^{\prime}$. Then by induction hypothesis, $\upsilon^{\prime}\mathrel{{\Rightarrow_{{\lfloor 2^{d^{\prime}}d^{\prime}\rfloor}}}}\mathord{\mathsf{F}}_{{\lfloor d^{\prime}\rfloor}}{\left(u\right)}$, and $\overline{\tau}^{\prime}\mathrel{{\Rightarrow_{{\lfloor 2^{d^{\prime}}d^{\prime}\rfloor}}}}\mathord{\mathsf{F}}_{{\lfloor d^{\prime}\rfloor}}{\left(\overline{t}\right)}$. By the previous lemma, we moreover have $\mathbf{md}_{x}{\left(\upsilon^{\prime}\right)}\leq 2^{d^{\prime}}\max{\left\{d^{\prime},\mathbf{md}_{x}{\left(u\right)}\right\}}=2^{d^{\prime}}d^{\prime}$, hence $\epsilon^{\prime}={\left\langle\lambda x\,{\upsilon^{\prime}}\right\rangle}\,{\overline{\tau}^{\prime}}\mathrel{{\Rightarrow_{{\lfloor 2^{d^{\prime}}d^{\prime}+1\rfloor}}}}\partial_{x}\mathord{\mathsf{F}}_{{\lfloor d^{\prime}\rfloor}}{\left(u\right)}\cdot\mathord{\mathsf{F}}_{{\lfloor d^{\prime}\rfloor}}{\left(\overline{t}\right)}=\mathord{\mathsf{F}}_{{\lfloor d\rfloor}}{\left(e\right)}$, and we conclude since $2^{d^{\prime}}d^{\prime}+1\leq 2^{d}d$.

• •

Otherwise $s$ is not an abstraction or $s=\lambda x\,{u}$ with $\mathbf{md}_{x}{\left(u\right)}>d^{\prime}$. By induction hypothesis, $\sigma^{\prime}\mathrel{{\Rightarrow_{{\lfloor 2^{d}d\rfloor}}}}\mathord{\mathsf{F}}_{{\lfloor d\rfloor}}{\left(\sigma^{\prime}\right)}$, and $\overline{\tau}^{\prime}\mathrel{{\Rightarrow_{{\lfloor 2^{d^{\prime}}d^{\prime}\rfloor}}}}\mathord{\mathsf{F}}_{{\lfloor d^{\prime}\rfloor}}{\left(\overline{t}\right)}$. Since $2^{d^{\prime}}d^{\prime}<2^{d}d$, we obtain $\overline{\tau}^{\prime}\mathrel{{\Rightarrow_{{\lfloor 2^{d}d-1\rfloor}}}}\mathord{\mathsf{F}}_{{\lfloor d^{\prime}\rfloor}}{\left(\overline{t}\right)}$ and then $\epsilon^{\prime}\mathrel{{\Rightarrow_{{\lfloor 2^{d}d\rfloor}}}}{\left\langle\mathord{\mathsf{F}}_{{\lfloor d\rfloor}}{\left(s\right)}\right\rangle}\,{\mathord{\mathsf{F}}_{{\lfloor d^{\prime}\rfloor}}{\left(\overline{t}\right)}}=\mathord{\mathsf{F}}_{{\lfloor d\rfloor}}{\left(e\right)}$.

If $e={\left[s_{1},\dotsc,s_{k}\right]}$ and $\epsilon^{\prime}={\left[\sigma^{\prime}_{1},\dotsc,\sigma^{\prime}_{k}\right]}$, with $s_{i}\mathrel{{\Rightarrow_{{\lfloor d\rfloor}}}}\sigma^{\prime}_{i}$ for all $i\in{\left\{1,\dotsc,k\right\}}$, then by induction hypothesis, for all $i\in{\left\{1,\dotsc,k\right\}}$, $\sigma^{\prime}_{i}\mathrel{{\Rightarrow_{{\lfloor 2^{d}d\rfloor}}}}\mathord{\mathsf{F}}_{{\lfloor d\rfloor}}{\left(s_{i}\right)}$ and we conclude directly.

Lemma 6.38**.**

For all $\mathrel{{\Rightarrow_{\partial}}}$-reduction structure $\mathfrak{E}$, if $\epsilon\mathrel{{\widetilde{\Rightarrow_{{\lfloor d\rfloor}}}_{\mathfrak{E}}}}\epsilon^{\prime}$ then $\epsilon^{\prime}\mathrel{{\widetilde{\Rightarrow_{{\lfloor 2^{d}d\rfloor}}}_{\mathfrak{E}}}}\mathord{\mathsf{F}}_{{\lfloor d\rfloor}}{\left(\epsilon^{\prime}\right)}$.

Proof 6.39**.**

Assume there is $\mathcal{E}\in\mathfrak{E}$, summable families ${\left(e_{i}\right)}_{i\in I}\in\mathcal{E}^{I}$ and ${\left(\epsilon^{\prime}_{i}\right)}_{i\in I}\mathbf{N}{\left[(\oc)\Delta\right]}^{I}$, and a family of scalars ${\left(a_{i}\right)}_{i\in I}$ such that $\epsilon=\sum_{i\in I}a_{i}.e_{i}$, $\epsilon^{\prime}=\sum_{i\in I}a_{i}.\epsilon^{\prime}_{i}$ and $e_{i}\mathrel{{\Rightarrow_{{\lfloor d\rfloor}}}}\epsilon^{\prime}_{i}$ for all $i\in I$. Write $\mathcal{E}^{\prime}=\bigcup_{i\in I}{\left|\epsilon^{\prime}_{i}\right|}$: since $\mathfrak{E}$ is a reduction structure, we obtain $\mathcal{E}^{\prime}\in\mathfrak{E}$. The family ${\left(\mathord{\mathsf{F}}_{{\lfloor d\rfloor}}{\left(e_{i}\right)}\right)}_{i\in I}$ is summable, and by the previous lemma, $\epsilon^{\prime}_{i}\mathrel{{\Rightarrow_{{\lfloor 2^{d}d\rfloor}}}}\mathord{\mathsf{F}}_{{\lfloor d\rfloor}}{\left(e_{i}\right)}$ for all $i\in I$. We conclude that $\epsilon^{\prime}\mathrel{{\widetilde{\Rightarrow_{{\lfloor 2^{d}d\rfloor}}}}}\sum_{i\in I}a_{i}.\mathord{\mathsf{F}}_{{\lfloor d\rfloor}}{\left(e_{i}\right)}=\mathord{\mathsf{F}}_{{\lfloor d\rfloor}}{\left(\epsilon\right)}$.

Similarly to $\mathrel{{\widetilde{\Rightarrow_{{(\partial)}}}}}$, we set

[TABLE]

and we obtain:

Corollary 6.40**.**

For all $\mathrel{{\Rightarrow_{\partial}}}$-reduction structure $\mathfrak{E}$ and all $\epsilon,\epsilon^{\prime}_{1},\dotsc,\epsilon^{\prime}_{n}\in\mathbf{S}^{(\oc)\Delta}$ such that $\epsilon\mathrel{{\widetilde{\Rightarrow_{{\lfloor\partial\rfloor}}}_{\mathfrak{E}}}}\epsilon^{\prime}_{i}$ for $i\in{\left\{1,\dotsc,n\right\}}$, there exists $d\in\mathbf{N}$ such that $\epsilon^{\prime}_{i}\mathrel{{\widetilde{\Rightarrow_{{\lfloor\partial\rfloor}}}_{\mathfrak{E}}}}\mathord{\mathsf{F}}_{{\lfloor d\rfloor}}{\left(\epsilon\right)}$ for $i\in{\left\{1,\dotsc,n\right\}}$.

6.4. Parallel reduction of resource vectors of bounded height

Recall that we have $e\mathrel{{\Rightarrow_{\partial}}}\epsilon^{\prime}$ iff $e\mathrel{{\Rightarrow_{{\left(\mathord{\mathbf{h}}{\left(e\right)}|\mathord{\mathbf{h}}{\left(e\right)}\right)}}}}\epsilon^{\prime}$ iff $e\mathrel{{\Rightarrow_{{(\mathord{\mathbf{h}}{\left(e\right)})}}}}\epsilon^{\prime}$ iff $e\mathrel{{\Rightarrow_{{\lfloor\mathord{\mathbf{h}}{\left(e\right)}\rfloor}}}}\epsilon^{\prime}$.

Definition 6.41**.**

We say a resource vector $\epsilon\in\mathbf{S}^{(\oc)\Delta}$ is bounded if ${\left\{\mathord{\mathbf{h}}{\left(e\right)}\mathrel{;}e\in{\left|\epsilon\right|}\right\}}$ is finite. We then write $\mathord{\mathbf{h}}{\left(\epsilon\right)}=\max{\left\{\mathord{\mathbf{h}}{\left(e\right)}\mathrel{;}e\in{\left|\epsilon\right|}\right\}}$.

If $\mathcal{E}\subseteq(\oc)\Delta$, we also write $\mathord{\mathbf{h}}{\left(\mathcal{E}\right)}\mathrel{\mathord{:}\mathord{=}}{\left\{\mathord{\mathbf{h}}{\left(e\right)}\mathrel{;}e\in\mathcal{E}\right\}}$ and then

[TABLE]

which is a resource structure (see Definition 5.9). Indeed, $(\oc)\mathfrak{B}\subseteq(\oc)\mathfrak{F}_{\mathord{\mathbf{fv}}}$, and if we write

[TABLE]

for all $h\in\mathbf{N}$ and all $V\subseteq\mathcal{V}$, we have $(\oc)\mathfrak{B}={\left\{(\oc)\Delta_{h,V}\mathrel{;}h\in\mathbf{N}\text{ and }V\in\mathord{\mathfrak{P}_{f}}{\left(\mathcal{V}\right)}\right\}}^{\perp\perp}$: this is a consequence of a generic transport lemma [TV16]. The semimodule of bounded resource vectors is then $\mathbf{S}{\left\langle(\oc)\mathfrak{B}\right\rangle}$.

Lemma 6.42**.**

For all $h\in\mathbf{N}$ and $V\in\mathord{\mathfrak{P}_{f}}{\left(\mathcal{V}\right)}$, ${\left(\mathord{\mathsf{F}}{\left(e\right)}\right)}_{e\in(\oc)\Delta_{h,V}}$ is summable. Moreover, for all $\epsilon\in\mathbf{S}{\left\langle(\oc)\mathfrak{B}\right\rangle}$, we have ${\left|\epsilon\right|}\subseteq(\oc)\Delta_{\mathord{\mathbf{h}}{\left(\epsilon\right)},\mathord{\mathbf{fv}}{\left(\epsilon\right)}}$ and then, setting $\mathord{\mathsf{F}}{\left(\epsilon\right)}\mathrel{\mathord{:}\mathord{=}}\sum_{e\in{\left|\epsilon\right|}}\epsilon_{e}.\mathord{\mathsf{F}}{\left(e\right)}$, we obtain $\epsilon\mathrel{{\widetilde{\Rightarrow_{\partial}}_{{\left|\epsilon\right|}}}}\mathord{\mathsf{F}}{\left(\epsilon\right)}$.

Proof 6.43**.**

Follows from Lemmas 6.30 and 6.17 using the fact that, if $\mathord{\mathbf{h}}{\left(e\right)}\leq h$ then $\mathord{\mathsf{F}}{\left(e\right)}=\mathord{\mathsf{F}}_{{\lfloor h\rfloor}}{\left(e\right)}$.

If $\mathbf{S}$ is zerosumfree, we have: $\epsilon\mathrel{{\widetilde{\Rightarrow_{\partial}}}}\epsilon^{\prime}$ iff $\epsilon\mathrel{{\widetilde{\Rightarrow_{{\lfloor\mathord{\mathbf{h}}{\left(\epsilon\right)}\rfloor}}}}}\epsilon^{\prime}$ as soon as $\epsilon$ is bounded. More generally, without any assumption on $\mathbf{S}$, we have $\epsilon\mathrel{{\widetilde{\Rightarrow_{\partial}}_{(\oc)\Delta_{h,V}}}}\epsilon^{\prime}$ iff $\epsilon\mathrel{{\widetilde{\Rightarrow_{{\lfloor h\rfloor}}}_{(\oc)\Delta_{h,V}}}}\epsilon^{\prime}$. We can moreover show that bounded vectors are stable under $\mathrel{{\widetilde{\Rightarrow_{\partial}}_{(\oc)\mathfrak{B}}}}$:

Lemma 6.44**.**

If $e{}_{\partial}e^{\prime}$ then $\mathord{\mathbf{h}}{\left(e^{\prime}\right)}\leq 2^{\mathord{\mathbf{h}}{\left(e\right)}}{\mathord{\mathbf{h}}{\left(e\right)}}$.

Proof 6.45**.**

The proof is by induction on the reduction $e\mathrel{{\Rightarrow_{\partial}}}\epsilon^{\prime}$ such that $e^{\prime}\in{\left|\epsilon^{\prime}\right|}$, and is very similar to that of Lemma 6.34. We detail only the base case.

If $e={\left\langle\lambda x\,{s}\right\rangle}\,{\overline{t}}$ and $\epsilon^{\prime}=\partial_{x}\sigma^{\prime}\cdot\overline{\tau}^{\prime}$ with $s\mathrel{{\Rightarrow_{\partial}}}\sigma^{\prime}$ and $\overline{t}\mathrel{{\Rightarrow_{\partial}}}\overline{\tau}^{\prime}$. Then $e^{\prime}\in{\left|\partial_{x}s^{\prime}\cdot\overline{t^{\prime}}\right|}$ with $s^{\prime}\in{\left|\sigma^{\prime}\right|}$ and $\overline{t^{\prime}}\in{\left|\overline{\tau}^{\prime}\right|}$. By induction, $\mathord{\mathbf{h}}{\left(s^{\prime}\right)}\leq 2^{\mathord{\mathbf{h}}{\left(s\right)}}\mathord{\mathbf{h}}{\left(s\right)}$ and $\mathord{\mathbf{h}}{\left(\overline{t^{\prime}}\right)}\leq 2^{\mathord{\mathbf{h}}{\left(\overline{t}\right)}}\mathord{\mathbf{h}}{\left(\overline{t}\right)}$. By Lemma 3.2,

[TABLE]

It follows that $(\oc)\mathfrak{B}$ is a $\mathrel{{\Rightarrow_{\partial}}}$-reduction structure: since $\mathrel{{\widetilde{\Rightarrow_{\partial}}_{(\oc)\mathfrak{B}}}}$ coincides with $\mathrel{{\widetilde{\Rightarrow_{{\lfloor\partial\rfloor}}}_{(\oc)\mathfrak{B}}}}$, Corollary 6.40 entails that $\mathrel{{\widetilde{\Rightarrow_{\partial}}_{(\oc)\mathfrak{B}}}}$ is strongly confluent. We can even refine this result following Lemma 6.42. First, let us call bounded reduction structure any $\mathrel{{\Rightarrow_{\partial}}}$-reduction structure $\mathfrak{E}$ such that $\mathfrak{E}\subseteq(\oc)\mathfrak{B}$. Then Lemma 6.38 entails:

Corollary 6.46**.**

For all bounded reduction structure $\mathfrak{E}$, and all reduction $\epsilon\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathfrak{E}}}}\epsilon^{\prime}$, $\epsilon^{\prime}\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathfrak{E}}}}\mathord{\mathsf{F}}{\left(\epsilon\right)}$.

It should moreover be clear that $\mathord{\tau}{\left(M\right)}$ is bounded for all $M\in\Lambda_{\mathbf{S}}$. In the next section, we show that $\mathrel{{\widetilde{\Rightarrow_{\partial}}_{(\oc)\mathfrak{B}}}}$ allows to simulate parallel $\beta$-reduction via Taylor expansion.212121

Observe that it is possible to establish Corollary 6.46 quite directly, following the proof of Lemma 6.38, and using only Lemma 6.44 and a variant of Lemma 6.17 (replacing $b$ with $\mathord{\mathbf{h}}{\left(e\right)}$). This is the path adopted in the extended abstract [Vau17] presented at CSL 2017.

7. Simulating $\beta$-reduction under Taylor expansion

From now on, for all $M,N\in\Lambda_{\mathbf{S}}$, we write $M\mathrel{{\widetilde{\Rightarrow_{\partial}}}}N$ if $\mathord{\tau}{\left(M\right)}\mathrel{{\widetilde{\Rightarrow_{\partial}}}}\mathord{\tau}{\left(N\right)}$. More generally, for all $M\in\Lambda_{\mathbf{S}}$ and all $\sigma\in\mathbf{S}^{(\oc)\Delta}$, we write $M\mathrel{{\widetilde{\Rightarrow_{\partial}}}}\sigma$ (resp. $\sigma\mathrel{{\widetilde{\Rightarrow_{\partial}}}}M$) if $\mathord{\tau}{\left(M\right)}\mathrel{{\widetilde{\Rightarrow_{\partial}}}}\sigma$ (resp. $\sigma\mathrel{{\widetilde{\Rightarrow_{\partial}}}}\mathord{\tau}{\left(M\right)}$). We will show in Subsection 7.1 that $M\mathrel{{\widetilde{\Rightarrow_{\partial}}}}N$ as soon as $M\mathrel{{\Rightarrow_{\beta}}}N$ where $\mathrel{{\Rightarrow_{\beta}}}$ is the parallel $\beta$-reduction defined as follows:

Definition 7.1**.**

We define parallel $\beta$-reduction on algebraic terms $\mathord{\mathrel{{\Rightarrow_{\beta}}}}\subseteq\Lambda_{\mathbf{S}}\times\Lambda_{\mathbf{S}}$ by the following inductive rules:

• •

$x\mathrel{{\Rightarrow_{\beta}}}x$;

• •

if $S\mathrel{{\Rightarrow_{\beta}}}M^{\prime}$ then $\lambda x\,{S}\mathrel{{\Rightarrow_{\beta}}}\lambda x\,{M^{\prime}}$;

• •

if $S\mathrel{{\Rightarrow_{\beta}}}M^{\prime}$ and $N\mathrel{{\Rightarrow_{\beta}}}N^{\prime}$ then ${\left(S\right)}\,{N}\mathrel{{\Rightarrow_{\beta}}}{\left(M^{\prime}\right)}\,{N^{\prime}}$;

• •

if $S\mathrel{{\Rightarrow_{\beta}}}M^{\prime}$ and $N\mathrel{{\Rightarrow_{\beta}}}N^{\prime}$ then ${\left(\lambda x\,{S}\right)}\,{N}\mathrel{{\Rightarrow_{\beta}}}M^{\prime}{\left[N^{\prime}/x\right]}$;

• •

$0\mathrel{{\Rightarrow_{\beta}}}0$;

• •

if $M\mathrel{{\Rightarrow_{\beta}}}M^{\prime}$ then $a.M\mathrel{{\Rightarrow_{\beta}}}a.M^{\prime}$;

• •

if $M\mathrel{{\Rightarrow_{\beta}}}M^{\prime}$ and $N\mathrel{{\Rightarrow_{\beta}}}N^{\prime}$ then $M+N\mathrel{{\Rightarrow_{\beta}}}M^{\prime}+N^{\prime}$.

In particular, if $1\in\mathbf{S}$ admits an opposite element $-1\in\mathbf{S}$ then $\mathrel{{\widetilde{\Rightarrow_{\partial}}_{(\oc)\mathfrak{B}}}}$ is degenerate. Indeed, we can consider $\mathrel{{\Rightarrow_{\beta}}}$ up to the equality of vector $\lambda$-terms by setting $M\mathrel{{\Rightarrow_{\widetilde{\beta}}}}N$ if there are $M^{\prime}\simeq_{\mathrm{v}}M$ and $N^{\prime}\simeq_{\mathrm{v}}N$ such that $M^{\prime}\mathrel{{\Rightarrow_{\beta}}}N^{\prime}$. Since $\simeq_{\mathord{\tau}}$ subsumes $\simeq_{\mathrm{v}}$, the results of Subsection 7.1 will imply that $M\mathrel{{\widetilde{\Rightarrow_{\partial}}_{(\oc)\mathfrak{B}}}}N$ as soon as $M\mathrel{{\Rightarrow_{\widetilde{\beta}}}}N$. If $-1\in\mathbf{S}$, we have $M\mathrel{{\Rightarrow_{\widetilde{\beta}}^{*}}}N$ for all $M,N\in\Lambda_{\mathbf{S}}$ by Example 4.1, hence $M\mathrel{{\widetilde{\Rightarrow_{\partial}}_{(\oc)\mathfrak{B}}^{*}}}N$.

Using reduction structures, we will nonetheless be able to define a consistent reduction relation containing $\beta$-reduction, but restricted to those algebraic $\lambda$-terms that have a normalizable Taylor expansion, in the sense to be defined in Section 8.

On the other hand, even assuming $\mathbf{S}$ is zerosumfree, Taylor expansions are not stable under $\mathrel{{\widetilde{\Rightarrow_{\partial}}}}$: if $M\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathfrak{B}}}}\sigma^{\prime}$, we know from the previous section that $\sigma^{\prime}$ is bounded and $M\mathrel{{\widetilde{\Rightarrow_{{\lfloor\partial\rfloor}}}}}\sigma^{\prime}$, but there is no reason why $\sigma^{\prime}$ would be the Taylor expansion of an algebraic $\lambda$-term.

We do know, however, that $\sigma^{\prime}\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathfrak{B}}}}\mathord{\mathsf{F}}{\left(\mathord{\tau}{\left(M\right)}\right)}$, which will allow us to obtain a weak conservativity result w.r.t. parallel $\beta$-reduction: for all reduction $M\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathfrak{B}}^{*}}}\sigma^{\prime}$ there is a reduction $M\mathrel{{\Rightarrow_{\beta}^{*}}}M^{\prime}$ such that $\sigma^{\prime}\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathfrak{B}}^{*}}}M^{\prime}$, i.e. any $\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathfrak{B}}}}$-reduction sequence from a Taylor expansion can be completed into a parallel $\beta$-reduction sequence (Subsection 7.2). Restricted to normalizable pure $\lambda$-terms, this will enable us to obtain an actual conservativity result.

7.1. Simulation of parallel $\beta$-reduction

We show that $\mathrel{{\widetilde{\Rightarrow_{\partial}}_{(\oc)\mathfrak{B}}}}$ allows to simulate $\mathrel{{\Rightarrow_{\beta}}}$ on $\mathbf{S}^{(\oc)\Delta}$, without any particular assumption on $\mathbf{S}$.

Lemma 7.2**.**

If $\sigma\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathcal{S}}}}\sigma^{\prime}$ and $\overline{\tau}\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\overline{\mathcal{T}}}}}\overline{\tau^{\prime}}$ then ${\left\langle\lambda x\,{\sigma}\right\rangle}\,{\overline{\tau}}\mathrel{{\widetilde{\Rightarrow_{\partial}}_{{\left\langle\lambda x\,{\mathcal{S}}\right\rangle}\,{\overline{\mathcal{T}}}}}}\partial_{x}\sigma^{\prime}\cdot\overline{\tau^{\prime}}$.

Proof 7.3**.**

Assume there are summable families ${\left(s_{i}\right)}_{i\in I}$, ${\left(\sigma^{\prime}_{i}\right)}_{i\in I}$, ${\left(\overline{t}_{j}\right)}_{j\in J}$ and ${\left(\overline{\tau}^{\prime}_{j}\right)}_{j\in J}$, and families of scalars ${\left(a_{i}\right)}_{i\in I}\in\mathcal{S}^{I}$ and ${\left(b_{j}\right)}_{j\in J}\in\overline{\mathcal{T}}^{J}$ such that:

• •

$\sigma=\sum_{i\in I}a_{i}.s_{i}$, $\sigma^{\prime}=\sum_{i\in I}a_{i}.\sigma^{\prime}_{i}$ and $s_{i}\mathrel{{\Rightarrow_{\partial}}}\sigma^{\prime}_{i}$ for all $i\in I$;

• •

$\overline{\tau}=\sum_{j\in J}b_{j}.\overline{t}_{j}$, $\overline{\tau}^{\prime}=\sum_{j\in J}b_{j}.\overline{\tau}^{\prime}_{j}$, and $\overline{t}_{j}\in\overline{\mathcal{T}}$ and $\overline{t}_{j}\mathrel{{\Rightarrow_{\partial}}}\overline{\tau}^{\prime}_{j}$ for all $j\in J$.

By multilinear-continuity, the families ${\left({\left\langle\lambda x\,{s_{i}}\right\rangle}\,{\overline{t}_{j}}\right)}_{i\in I,j\in J}$ and ${\left(\partial_{x}\sigma^{\prime}_{i}\cdot\overline{\tau}^{\prime}_{j}\right)}_{i\in I,j\in J}$ are summable, ${\left\langle\lambda x\,{\sigma}\right\rangle}\,{\overline{\tau}}=\sum_{i\in I,j\in J}a_{i}b_{j}.{\left\langle\lambda x\,{s_{i}}\right\rangle}\,{\overline{t}_{j}}$ and $\partial_{x}\sigma^{\prime}\cdot\overline{\tau}^{\prime}=\sum_{i\in I,j\in J}a_{i}b_{j}.\partial_{x}\sigma^{\prime}_{i}\cdot\overline{\tau}^{\prime}_{j}$. It is then sufficient to observe that ${\left\langle\lambda x\,{s_{i}}\right\rangle}\,{\overline{t}_{j}}\mathrel{{\Rightarrow_{\partial}}}\partial_{x}\sigma^{\prime}_{i}\cdot\overline{\tau}^{\prime}_{j}$ for all $(i,j)\in I\times J$.

The additional requirement on resource supports is straightforwardly satisfied, since ${\left\langle\lambda x\,{s_{i}}\right\rangle}\,{\overline{t}_{j}}\in{\left\langle\lambda x\,{\mathcal{S}}\right\rangle}\,{\overline{\mathcal{T}}}$ for all $(i,j)\in I\times J$.

Lemma 7.4**.**

If $\sigma\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathcal{S}}}}\sigma^{\prime}$ then $\lambda x\,{\sigma}\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\lambda x\,{\mathcal{S}}}}}\lambda x\,{\sigma^{\prime}}$. If moreover $\overline{\tau}\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\overline{\mathcal{T}}}}}\overline{\tau^{\prime}}$ then ${\left\langle\sigma\right\rangle}\,{\overline{\tau}}\mathrel{{\widetilde{\Rightarrow_{\partial}}_{{\left\langle\mathcal{S}\right\rangle}\,{\overline{\mathcal{T}}}}}}{\left\langle\sigma^{\prime}\right\rangle}\,{\overline{\tau^{\prime}}}$.

Proof 7.5**.**

Similarly to the previous lemma, each result follows from the multilinear-continuity of syntactic operators, and the contextuality of $\mathrel{{\Rightarrow_{\partial}}}$.

Lemma 7.6**.**

If $\sigma\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathcal{S}}}}\sigma^{\prime}$ then ${\sigma}^{\oc}\mathrel{{\widetilde{\Rightarrow_{\partial}}_{{\mathcal{S}}^{\oc}}}}{{\sigma^{\prime}}}^{\oc}$.

Proof 7.7**.**

Assume there are summable families ${\left(s_{i}\right)}_{i\in I}$ and ${\left(\sigma^{\prime}_{i}\right)}_{i\in I}$, and a family of scalars ${\left(a_{i}\right)}_{i\in I}$ such that $\sigma=\sum_{i\in I}a_{i}.s_{i}$, $\sigma^{\prime}=\sum_{i\in I}a_{i}.\sigma^{\prime}_{i}$ and $s_{i}\mathrel{{\Rightarrow_{\partial}}}\sigma^{\prime}_{i}$ for all $i\in I$.

Then by multilinear-continuity of the monomial construction, for all $n\in\mathbf{N}$, the families ${\left({\left[s_{i_{1}},\dotsc,s_{i_{n}}\right]}\right)}_{i_{1},\dotsc,i_{n}\in I}$ and ${\left({\left[\sigma^{\prime}_{i_{1}},\dotsc,\sigma^{\prime}_{i_{n}}\right]}\right)}_{i_{1},\dotsc,i_{n}\in I}$ are summable, and

[TABLE]

and

[TABLE]

Since the supports of the monomial vectors $\sigma^{n}$ (resp. ${\sigma^{\prime}}^{n}$) for $n\in\mathbf{N}$ are pairwise disjoint, we obtain that the families ${\left({\left[s_{i_{1}},\dotsc,s_{i_{n}}\right]}\right)}_{\begin{subarray}{c}n\in\mathbf{N}\\ i_{1},\dotsc,i_{n}\in I\end{subarray}}$ and ${\left({\left[\sigma^{\prime}_{i_{1}},\dotsc,\sigma^{\prime}_{i_{n}}\right]}\right)}_{\begin{subarray}{c}n\in\mathbf{N}\\ i_{1},\dotsc,i_{n}\in I\end{subarray}}$ are summable, and

[TABLE]

and

[TABLE]

which concludes the proof since each ${\left[s_{i_{1}},\dotsc,s_{i_{n}}\right]}\mathrel{{\Rightarrow_{\partial}}}{\left[\sigma^{\prime}_{i_{1}},\dotsc,\sigma^{\prime}_{i_{n}}\right]}$.

Lemma 7.8**.**

If $\epsilon\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathcal{E}}}}\epsilon^{\prime}$ and $\varphi\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathcal{F}}}}\varphi^{\prime}$ then $a.\epsilon\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathcal{E}}}}a.\epsilon^{\prime}$ and $\epsilon+\varphi\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathcal{E}\mathbin{\cup}\mathcal{F}}}}\epsilon^{\prime}+\varphi^{\prime}$.

Proof 7.9**.**

Follows directly from the definitions, using the fact that summable families form a $\mathbf{S}$-semimodule.

Lemma 7.10**.**

If $M\mathrel{{\Rightarrow_{\beta}}}M^{\prime}$ then $M\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathord{\mathcal{T}}{\left(M\right)}}}}M^{\prime}$.

Proof 7.11**.**

By induction on the reduction $M\mathrel{{\Rightarrow_{\beta}}}M^{\prime}$ using Lemmas 7.2 to 7.6 in the cases of reduction from a simple term, and Lemma 7.8 in the case of reduction from an algebraic term.

Recalling that $\mathord{\mathcal{T}}{\left(M\right)}\in\mathfrak{B}$ we obtain:

Corollary 7.12**.**

If $M\mathrel{{\Rightarrow_{\beta}}}M^{\prime}$ then $M\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathfrak{B}}}}M^{\prime}$.

Observe that these results hold on Taylor supports as well, which will be useful in the treatment of Taylor normalizable terms in Section 8:

Lemma 7.13**.**

If $M\mathrel{{\Rightarrow_{\beta}}}M^{\prime}$ then $\mathord{\mathcal{T}}{\left(M\right)}\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathord{\mathcal{T}}{\left(M\right)}}}}\mathord{\mathcal{T}}{\left(M^{\prime}\right)}$ in $\mathbf{B}^{\Delta}$.

Proof 7.14**.**

The proof is again by induction on the reduction $M\mathrel{{\Rightarrow_{\beta}}}M^{\prime}$ using Lemmas 7.2 to Lemma 7.8 in $\mathbf{B}^{\Delta}$.

7.2. Conservativity

Definition 7.15**.**

We define the full parallel reduct of simple terms and algebraic terms inductively as follows:

[TABLE]

As can be expected, we have $M^{\prime}\mathrel{{\Rightarrow_{\beta}}}\mathord{\mathsf{F}}{\left(M\right)}$ as soon as $M\mathrel{{\Rightarrow_{\beta}}}M^{\prime}$. In this subsection, we will show that a similar property holds for $\mathrel{{\widetilde{\Rightarrow_{\partial}}_{(\oc)\mathfrak{B}}}}$.

Recall that, by Lemma 6.42, the full reduction operator $\mathord{\mathsf{F}}$ on resource expressions extends to bounded resource vectors. We obtain:

Lemma 7.16**.**

For all bounded $\sigma_{0}\in\mathbf{S}^{\Delta}$, $\overline{\tau}\in\mathbf{S}^{\oc\Delta}$, $\epsilon,\varphi\in\mathbf{S}^{(\oc)\Delta}$,

[TABLE]

Proof 7.17**.**

The proofs of those identities are basically the same as those of Lemmas 7.2 to 7.8, the necessary summability conditions following from Lemma 6.42.

Lemma 7.18**.**

For all $M\in\Lambda_{\mathbf{S}}$, $\mathord{\mathsf{F}}{\left(\mathord{\tau}{\left(M\right)}\right)}=\mathord{\tau}{\left(\mathord{\mathsf{F}}{\left(M\right)}\right)}$.

Proof 7.19**.**

We know that $\mathord{\tau}{\left(M\right)}$ is bounded. The identity is then proved by induction on simple terms and algebraic terms, using the previous lemma in each case.

Lemma 7.20**.**

For all bounded term reduction structure $\mathfrak{S}$ and all $M\in\Lambda_{\mathbf{S}}$, if $M\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathfrak{S}}}}\sigma^{\prime}$ then $\sigma^{\prime}\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathfrak{S}}}}\mathord{\mathsf{F}}{\left(M\right)}$.

Proof 7.21**.**

By Corollary 6.46, $\sigma^{\prime}\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathfrak{S}}}}\mathord{\mathsf{F}}{\left(\mathord{\tau}{\left(M\right)}\right)}$ and we conclude by the previous lemma.

This result can then be generalized to sequences of $\mathrel{{\widetilde{\Rightarrow_{\partial}}}}$-reductions.

Lemma 7.22**.**

For all bounded term reduction structure $\mathfrak{S}$ and all $M\in\Lambda_{\mathbf{S}}$, if $M\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathfrak{S}}^{n}}}\sigma^{\prime}$ then $\sigma^{\prime}\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathfrak{S}}^{n}}}\mathord{\mathsf{F}}^{n}{\left(M\right)}$.

Proof 7.23**.**

By induction on $n$. The case $n=0$ is trivial, and the inductive case follows from the previous lemma and strong confluence of $\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathfrak{S}}}}$: if $M\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathfrak{S}}^{n}}}\sigma^{\prime}\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathfrak{S}}}}\tau$ then by induction hypothesis $\sigma^{\prime}\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathfrak{S}}^{n}}}\mathord{\mathsf{F}}^{n}{\left(M\right)}$, hence by strong confluence, there exists $\tau^{\prime}$ such that $\tau\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathfrak{S}}^{n}}}\tau^{\prime}$ and $\mathord{\mathsf{F}}^{n}{\left(M\right)}\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathfrak{S}}}}\tau^{\prime}$; by the previous lemma, $\tau^{\prime}\mathrel{{\widetilde{\Rightarrow_{\partial}}}}\mathord{\mathsf{F}}^{n+1}{\left(M\right)}$.

We have thus obtained some weak kind of conservativity of $\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathfrak{B}}}}$ w.r.t. $\beta$-reduction, but it is not very satisfactory: the same result would hold for the tautological relation $\mathbf{S}{\left\langle\mathfrak{B}\right\rangle}\times\mathbf{S}{\left\langle\mathfrak{B}\right\rangle}$, which is indeed the same as $\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathfrak{B}}}}$ if $1$ has an opposite element in $\mathbf{S}$. Even when $\mathbf{S}$ is zerosumfree, the converse to Lemma 7.10 cannot hold in general if only because there can be distinct $\beta$-normal forms $M\not\simeq_{\mathrm{v}}N$ such that $M\simeq_{\mathord{\tau}}N$ (see Example 4.5). Under this hypothesis, we can nonetheless obtain an actual conservativity result on normalizable pure $\lambda$-terms as follows.

We write $\simeq_{\beta}$ for the symmetric, reflexive and transitive closure of $\mathrel{{\Rightarrow_{\beta}}}$. Similarly, if $\mathfrak{E}$ is a reduction structure, we write $\simeq_{\partial\,\mathfrak{E}}$ for the equivalence on $\mathbf{S}{\left\langle\mathfrak{E}\right\rangle}$ induced by $\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathfrak{E}}}}$.

Lemma 7.24**.**

Assume $\mathbf{S}$ is zerosumfree. Let $M,N\in\Lambda$ be such that $M$ is normalizable. Then $M\simeq_{\partial\,\mathfrak{B}}N$ iff $M\simeq_{\beta}N$.

Proof 7.25**.**

Corollary 6.46 entails that, if $\mathfrak{E}$ is a bounded reduction structure, then $\epsilon\simeq_{\partial\,\mathfrak{E}}\epsilon^{\prime}$ iff $\epsilon\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathfrak{E}}^{*}}}\mathord{\mathsf{F}}^{n}{\left(\epsilon^{\prime}\right)}$ for some $n\in\mathbf{N}$. Now assume $M\in\Lambda_{\mathbf{S}}$ is normalizable and write $\mathord{\mathsf{NF}}{\left(M\right)}$ for its normal form: in particular $M\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathfrak{B}}^{*}}}\mathord{\mathsf{NF}}{\left(M\right)}$, by Corollary 7.12. If $M\simeq_{\partial\,\mathfrak{B}}N$, we thus have $\mathord{\mathsf{NF}}{\left(M\right)}\simeq_{\partial\,\mathfrak{B}}N$, hence $\mathord{\mathsf{NF}}{\left(M\right)}\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathfrak{B}}^{*}}}\mathord{\mathsf{F}}^{n}{\left(N\right)}$ for some $n\in\mathbf{N}$. In particular, if $\mathbf{S}$ is zerosumfree, we obtain $\mathord{\mathsf{NF}}{\left(M\right)}\simeq_{\mathord{\tau}}\mathord{\mathsf{F}}^{n}{\left(N\right)}$. If moreover $M,N\in\Lambda$, we deduce $M\simeq_{\beta}N$ by the injectivity of $\mathord{\tau}$ on $\Lambda$.

The next section will allow us to establish a similar conservativity result, without any assumption on $\mathbf{S}$, at the cost of restricting the reduction relation to normalizable resource vectors.

8. Normalizing Taylor expansions

Previous works on the normalization of Taylor expansions were restricted a priori, to a strict subsystem of the algebraic $\lambda$-calculus:

• •

the uniform setting of pure $\lambda$-terms [ER08, ER06];

• •

the typed setting of an extension of system $F$ to the algebraic $\lambda$-calculus [Ehr10];

• •

a $\lambda$-calculus extended with formal finite sums, rather than linear combinations [PTV16, TAO17].

In all these, pathological terms were avoided, e.g. those involved in the inconsistency Example 4.1. Moreover observe that the very notion of normalizability is not compatible with $\simeq_{\mathrm{v}}$, and in particular the identity $0\simeq_{\mathrm{v}}0.M$: those previous works circumvented this incompatibility, either by imposing normalizability via typing, or by excluding the formation of the term $0.M$.

Our approach is substantially different. We introduce a notion of normalizability on resource vectors such that:

• •

both pure $\lambda$-terms and normalizable algebraic $\lambda$-terms (in particular typed algebraic $\lambda$-terms and normalizable $\lambda$-terms with sums) have a normalizable Taylor expansion;

• •

the restriction of $\mathrel{{\widetilde{\Rightarrow_{\partial}}}}$ to normalizable resource vectors is a consistent extension of both $\beta$-reduction on pure $\lambda$-terms and normalization on algebraic $\lambda$-terms, without any assumption on the underlying semiring of scalars.

8.1. Normalizable resource vectors

We say $\epsilon\in\mathbf{S}^{(\oc)\Delta}$ is normalizable whenever the family ${\left(\mathord{\mathsf{NF}}{\left(e\right)}\right)}_{e\in{\left|\epsilon\right|}}$ is summable. In this case, we write $\mathord{\mathsf{NF}}{\left(\epsilon\right)}\mathrel{\mathord{:}\mathord{=}}\sum_{e\in(\oc)\Delta}\epsilon_{e}.\mathord{\mathsf{NF}}{\left(e\right)}$.

Normalizable vectors form a finiteness space. Recall indeed from Subsection 3.1 that $e\geq_{\partial}e^{\prime}$ iff $e\mathrel{{\rightarrow_{\partial}^{*}}}\epsilon^{\prime}$ with $e^{\prime}\in{\left|\epsilon^{\prime}\right|}$. If $e\in(\oc)\Delta$, we write $\mathord{\uparrow}{e}\mathrel{\mathord{:}\mathord{=}}{\left\{e^{\prime}\in(\oc)\Delta\mathrel{;}e^{\prime}\geq_{\partial}e\right\}}$. Then $\epsilon$ is normalizable iff for each normal resource expression $e$, ${\left|\epsilon\right|}\mathbin{\cap}\mathord{\uparrow}{e}$ is finite: writing (\oc)\mathcal{N}={\left\{e\in(\oc)\Delta\mathrel{;}\text{e is normal}\right\}} and $(\oc)\mathfrak{N}={\left\{\mathord{\uparrow}{e}\mathrel{;}e\in(\oc)\mathcal{N}\right\}}^{\perp}\mathbin{\cap}(\oc)\mathfrak{F}_{\mathord{\mathbf{fv}}}$, we obtain that $\mathbf{S}{\left\langle(\oc)\mathfrak{N}\right\rangle}$ is the set of normalizable resource vectors. Observe that $\mathord{\mathsf{NF}}$ is defined on all $\mathbf{S}{\left\langle(\oc)\mathfrak{N}\right\rangle}$ but is guaranteed to be linear-continuous only when restricted to subsemimodules of the form $\mathbf{S}^{\mathcal{E}}$ with $\mathcal{E}\in(\oc)\mathfrak{N}$.

For our study of hereditarily determinable terms in Section 9, it will be useful to decompose $(\oc)\mathfrak{N}$ into a decreasing sequence of finiteness structures.

Definition 8.1**.**

We define the monomial depth $\mathord{\mathbf{d}}{\left(e\right)}\in\mathbf{N}$ of a resource expression $e\in(\oc)\Delta$ as follows:

[TABLE]

We write $(\oc)\mathcal{N}_{d}={\left\{e\in(\oc)\mathcal{N}\mathrel{;}\mathord{\mathbf{d}}{\left(e\right)}\leq d\right\}}$ so that $(\oc)\mathcal{N}=\bigcup_{d\in\mathbf{N}}(\oc)\mathcal{N}_{d}$. We then write $(\oc)\mathfrak{N}_{d}={\left\{\mathord{\uparrow}{e}\mathrel{;}e\in(\oc)\mathcal{N}_{d}\right\}}^{\perp}\mathbin{\cap}(\oc)\mathfrak{F}_{\mathord{\mathbf{fv}}}$ so that $(\oc)\mathfrak{N}=\bigcap_{d\in\mathbf{N}}(\oc)\mathfrak{N}_{d}$. Each finiteness structure $(\oc)\mathfrak{N}_{d}$ is moreover a reduction structure for any reduction relation contained in $\mathrel{{\rightarrow_{\partial}^{*}}}$ (and so is $(\oc)\mathfrak{N}$). Indeed, writing $\mathord{\downarrow}{e}={\left\{e^{\prime}\in(\oc)\Delta\mathrel{;}e\geq_{\partial}e^{\prime}\right\}}$ and $\mathord{\downarrow}{\mathcal{E}}=\bigcup_{e\in\mathcal{E}}\mathord{\downarrow}{e}$, we obtain:

Lemma 8.2**.**

If $\mathcal{E}\in(\oc)\mathfrak{N}_{d}$ then $\mathord{\downarrow}{\mathcal{E}}\in(\oc)\mathfrak{N}_{d}$.

Proof 8.3**.**

Let $e^{\prime\prime}\in(\oc)\mathcal{N}_{d}$ and $e^{\prime}\in\mathord{\downarrow}{\mathcal{E}}\mathbin{\cap}\mathord{\uparrow}{e^{\prime\prime}}$. Necessarily, there is $e\in\mathcal{E}$ such that $e\geq_{\partial}e^{\prime}$. Then $e\in\mathcal{E}\mathbin{\cap}\mathord{\uparrow}{e^{\prime\prime}}$: since $\mathcal{E}\in(\oc)\mathfrak{N}_{d}$, there are finitely many values for $e$ hence for $e^{\prime}$ by Lemma 3.4.

It follows that normalizable vectors are stable under reduction:

Lemma 8.4**.**

If $\epsilon\mathrel{{\widetilde{\Rightarrow_{\partial}}_{(\oc)\mathfrak{N}}}}\epsilon^{\prime}$ then $\epsilon^{\prime}\in\mathbf{S}{\left\langle(\oc)\mathfrak{N}\right\rangle}$ and $\mathord{\mathsf{NF}}{\left(\epsilon\right)}=\mathord{\mathsf{NF}}{\left(\epsilon^{\prime}\right)}$.

Proof 8.5**.**

Assume there exists $\mathcal{E}\in(\oc)\mathfrak{N}$ and families $(a_{i})_{i\in I}\in\mathbf{S}^{I}$, ${\left(e_{i}\right)}_{i\in I}\in(\oc)\Delta^{I}$ and ${\left(\epsilon^{\prime}_{i}\right)}_{i\in I}\in\mathbf{N}{\left[(\oc)\Delta\right]}^{I}$ such that:

• •

${\left(e_{i}\right)}_{i\in I}$ is summable and $\epsilon=\sum_{i\in I}a_{i}.e_{i}$;

• •

${\left(\epsilon^{\prime}_{i}\right)}_{i\in I}$ is summable and $\epsilon^{\prime}=\sum_{i\in I}a_{i}.\epsilon^{\prime}_{i}$;

• •

for all $i\in I$, $e_{i}\in\mathcal{E}$ and $e_{i}\mathrel{{\widetilde{\Rightarrow_{\partial}}}}\epsilon^{\prime}_{i}$.

We obtain that $\mathcal{E}^{\prime}\mathrel{\mathord{:}\mathord{=}}\bigcup_{i\in I}{\left|\epsilon^{\prime}_{i}\right|}\in(\oc)\mathfrak{N}$ by Lemma 8.2, hence $\epsilon^{\prime}\in\mathbf{S}{\left\langle(\oc)\mathfrak{N}\right\rangle}$ since ${\left|\epsilon^{\prime}\right|}\subseteq\mathcal{E}^{\prime}$. Then, by the linear-continuity of $\mathord{\mathsf{NF}}$ on $\mathbf{S}^{\mathcal{E}^{\prime}}$,

[TABLE]

As a direct consequence, we obtain that $\simeq_{\partial\,(\oc)\mathfrak{N}}$ is consistent, without any additional condition on the semiring $\mathbf{S}$:

Corollary 8.6**.**

If $\epsilon\simeq_{\partial\,(\oc)\mathfrak{N}}\epsilon^{\prime}$ (in particular $\epsilon,\epsilon^{\prime}\in\mathbf{S}{\left\langle(\oc)\mathfrak{N}\right\rangle}$) then $\mathord{\mathsf{NF}}{\left(\epsilon\right)}=\mathord{\mathsf{NF}}{\left(\epsilon^{\prime}\right)}$.

We can moreover show that the normal form of a Taylor normalizable term is obtained as the limit of the parallel left reduction strategy. Let us first precise the kind of convergence we consider. With the notations of Subsection 2.3, we say a sequence $\overrightarrow{\xi}={\left(\xi_{n}\right)}_{n\in\mathbf{N}}\in{\left(\mathbf{S}^{X}\right)}^{\mathbf{N}}$ of vectors converges to $\xi^{\prime}$ if, for all $x\in X$ there exists $n_{x}\in\mathbf{N}$ such that, for all $n\geq n_{x}$, $\xi_{n,x}=\xi^{\prime}_{x}$. In other words we consider the product topology on $\mathbf{S}^{X}$, $\mathbf{S}$ being endowed with the discrete topology. Similarly to the notion of summability, this notion of convergence coincides with that induced by the linear topology on $\mathbf{S}^{X}$ associated with the maximal finiteness structure $\mathord{\mathfrak{P}}{\left(X\right)}$ on $X$: in this particular case, a base of neighbourhoods of [math] is given by the sets ${\left\{\xi\in\mathbf{S}^{X}\mathrel{;}{\left|\xi\right|}\mathbin{\cap}\mathcal{X}^{\prime}=\emptyset\right\}}$ for $\mathcal{X}^{\prime}\in\mathord{\mathfrak{P}}{\left(X\right)}^{\perp}=\mathord{\mathfrak{P}_{f}}{\left(X\right)}$, or equivalently by the the sets ${\left\{\xi\in\mathbf{S}^{X}\mathrel{;}x\not\in{\left|\xi\right|}\right\}}$ for $x\in X$.

The parallel left reduction strategy on resource vectors is defined as follows.

Definition 8.7**.**

We define the left reduct of a resource expression inductively as follows:

[TABLE]

This is extended to finite sums of resource expressions by linearity: $\mathord{\mathsf{L}}{\left(\sum_{i=1}^{n}e_{i}\right)}=\sum_{i=1}^{n}\mathord{\mathsf{L}}{\left(e_{i}\right)}$.

Lemma 8.8**.**

For all resource expression $e\in(\oc)\Delta$, $e\mathrel{{\Rightarrow_{{(1)}}}}\mathord{\mathsf{L}}{\left(e\right)}$.

Proof 8.9**.**

Easy by induction on $e$.

In particular $\mathord{\mathsf{NF}}{\left(e\right)}=\mathord{\mathsf{NF}}{\left(\mathord{\mathsf{L}}{\left(e\right)}\right)}$ for all $e\in(\oc)\Delta$. By Lemma 6.17, we moreover obtain that if $e^{\prime}\in{\left|\mathord{\mathsf{L}}{\left(e\right)}\right|}$ then $\mathord{\mathbf{s}}{\left(e\right)}\leq 4\mathord{\mathbf{s}}{\left(e^{\prime}\right)}$ and $\mathord{\mathbf{fv}}{\left(e\right)}=\mathord{\mathbf{fv}}{\left(e^{\prime}\right)}$. As a consequence ${\left(\mathord{\mathsf{L}}{\left(e\right)}\right)}_{e\in(\oc)\Delta}$ is summable. For all $\epsilon\in\mathbf{S}^{(\oc)\Delta}$, we set

[TABLE]

and obtain a linear-continuous map on resource vectors.

For all $\epsilon\in\mathbf{S}^{(\oc)\Delta}$, we write $\epsilon\mathord{\upharpoonright}_{(\oc)\mathcal{N}}$ for the projection of $\epsilon$ on normal resource expressions: $\epsilon\mathord{\upharpoonright}_{(\oc)\mathcal{N}}\mathrel{\mathord{:}\mathord{=}}\sum_{e\in(\oc)\mathcal{N}}\epsilon_{e}.e\in\mathbf{S}^{(\oc)\mathcal{N}}$. We obtain:

Theorem 8.9**.**

For all normalizable resource vector $\epsilon\in\mathbf{S}{\left\langle(\oc)\mathfrak{N}\right\rangle}$, ${\left(\mathord{\mathsf{L}}^{k}{\left(\epsilon\right)}\mathord{\upharpoonright}_{(\oc)\mathcal{N}}\right)}_{k\in\mathbf{N}}$ converges to $\mathord{\mathsf{NF}}{\left(\epsilon\right)}$ in $\mathbf{S}^{(\oc)\mathcal{N}}$.

Proof 8.10**.**

Fix ${e^{\prime}}\in\mathcal{N}$. Since ${\left|\epsilon\right|}\in(\oc)\mathfrak{N}$, $\mathcal{E}\mathrel{\mathord{:}\mathord{=}}{\left|\epsilon\right|}\mathbin{\cap}\mathord{\uparrow}{e^{\prime}}$ is finite. Let ${k^{\prime}}$ be such that $\mathord{\mathsf{L}}^{k^{\prime}}{\left(e\right)}$ is normal for all $e\in\mathcal{E}$. Then $\mathord{\mathsf{NF}}{\left(\epsilon\right)}_{e^{\prime}}=\sum_{e\in{\left|\epsilon\right|}}\epsilon_{e}.{\mathord{\mathsf{NF}}{\left(e\right)}}_{e^{\prime}}=\sum_{e\in\mathcal{E}}\epsilon_{e}.{\mathord{\mathsf{NF}}{\left(e\right)}}_{e^{\prime}}=\sum_{e\in\mathcal{E}}\epsilon_{e}.{\mathord{\mathsf{L}}^{k^{\prime}}{\left(e\right)}}_{e^{\prime}}$. Moreover, by the linear-continuity of $\mathord{\mathsf{L}}^{k}$ on resource vectors, ${\left(\mathord{\mathsf{L}}^{k}{\left(\epsilon\right)}\mathord{\upharpoonright}_{(\oc)\mathcal{N}}\right)}_{e^{\prime}}=\mathord{\mathsf{L}}^{k}{\left(\epsilon\right)}_{e^{\prime}}=\sum_{e\in\Delta}\epsilon_{e}.{\mathord{\mathsf{L}}^{k}{\left(e\right)}}_{e^{\prime}}=\sum_{e\in\mathcal{E}}\epsilon_{e}.{\mathord{\mathsf{L}}^{k}{\left(e\right)}}_{e^{\prime}}=\sum_{e\in\mathcal{E}}\epsilon_{e}.{\mathord{\mathsf{L}}^{k^{\prime}}{\left(e\right)}}_{e^{\prime}}$.

Observe that the projection on normal expressions is essential:

Example 8.11**.**

Consider the looping term $\Omega\mathrel{\mathord{:}\mathord{=}}{\left(\lambda x\,{{\left(x\right)}\,{x}}\right)}\,{\lambda x\,{{\left(x\right)}\,{x}}}$: one can check that $\mathord{\mathsf{NF}}{\left(\mathord{\tau}{\left(\Omega\right)}\right)}=\mathord{\tau}{\left(\Omega\right)}\mathord{\upharpoonright}_{\mathcal{N}}=0$, but it will follow from the results of subsection 8.2 that $\mathord{\mathsf{L}}^{k}{\left(\mathord{\tau}{\left(\Omega\right)}\right)}=\mathord{\tau}{\left(\Omega\right)}\not=0$ for all $k\in\mathbf{N}$.

Analyzing this phenomenon was fundamental in the characterization of strongly normalizable $\lambda$-terms by a finiteness structure on resource terms, obtained by Pagani, Tasson and the author [PTV16].

8.2. Taylor normalizable terms

It is possible to transfer some of the good properties of reduction on normalizable vectors to those algebraic $\lambda$-terms that have a normalizable Taylor expansion. More precisely, we say $M\in\Lambda_{\mathbf{S}}$ is Taylor normalizable if $\mathord{\mathcal{T}}{\left(M\right)}\in(\oc)\mathfrak{N}$. Then:

Lemma 8.12**.**

Assume $M,M^{\prime}\in\Lambda_{\mathbf{S}}$ are such that $M\mathrel{{\Rightarrow_{\beta}}}M^{\prime}$. Then $M$ is Taylor normalizable iff $M^{\prime}$ is Taylor normalizable.

Proof 8.13**.**

First observe that by Lemma 7.13, we have $\mathord{\mathcal{T}}{\left(M\right)}\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathord{\mathcal{T}}{\left(M\right)}}}}\mathord{\mathcal{T}}{\left(M^{\prime}\right)}$ in $\mathbf{B}^{\Delta}$. Moreover observe that $\mathbf{B}{\left\langle\mathfrak{N}\right\rangle}$ is nothing but $\mathfrak{N}$.

Assume $M$ is Taylor normalizable, i.e. $\mathord{\mathcal{T}}{\left(M\right)}\in\mathfrak{N}$: by Lemma 8.4, $\mathord{\mathcal{T}}{\left(M^{\prime}\right)}\in\mathbf{B}{\left\langle\mathfrak{N}\right\rangle}$, i.e. $M^{\prime}$ is Taylor normalizable.

Conversely, assume $M^{\prime}$ is Taylor normalizable and let $s^{\prime\prime}\in\mathcal{N}$ and $\mathcal{S}\mathrel{\mathord{:}\mathord{=}}\mathord{\mathcal{T}}{\left(M\right)}\mathbin{\cap}\mathord{\uparrow}{s^{\prime\prime}}$: we prove $\mathcal{S}$ is finite. Fix an enumeration ${\left(s_{k}\right)}_{k\in K}\in\mathcal{S}^{K}$ of $\mathcal{S}$: $\mathcal{S}={\left\{s_{k}\mathrel{;}k\in K\right\}}$. Since $\mathord{\mathcal{T}}{\left(M\right)}\mathrel{{\widetilde{\Rightarrow_{\partial}}_{\mathord{\mathcal{T}}{\left(M\right)}}}}\mathord{\mathcal{T}}{\left(M^{\prime}\right)}$, we have $\mathord{\mathcal{T}}{\left(M\right)}={\left\{t_{i}\mathrel{;}i\in I\right\}}$ and $\mathord{\mathcal{T}}{\left(M^{\prime}\right)}=\bigcup_{i\in I}{\left|\tau^{\prime}_{i}\right|}$ with $t_{i}\mathrel{{\Rightarrow_{\partial}}}\tau^{\prime}_{i}$ for all $i\in I$. Now for all $k\in K$, there exists $i\in I$ such that $s_{k}=t_{i}$. Since $s_{k}\geq_{\partial}s^{\prime\prime}$, $\tau^{\prime}_{i}\not=0$ and we can fix $s^{\prime}_{k}\in{\left|\tau^{\prime}_{i}\right|}\subseteq\mathord{\mathcal{T}}{\left(M^{\prime}\right)}$ such that $s_{k}{}_{\partial}s^{\prime}_{k}\geq_{\partial}s^{\prime\prime}$. Since $\mathord{\mathcal{T}}{\left(M^{\prime}\right)}\in\mathfrak{N}$, the set ${\left\{s^{\prime}_{k}\mathrel{;}k\in K\right\}}$ is finite. Then $\mathcal{S}\subseteq{\left\{s\in\Delta\mathrel{;}k\in K\text{, }s{}_{{(\mathord{\mathbf{h}}{\left(M\right)})}}s^{\prime}_{k}\right\}}$ which is finite by Lemma 6.17.

The consistency of $\beta$-reduction on Taylor normalizable terms follows.

Theorem 8.13**.**

Assume $M,M^{\prime}\in\Lambda_{\mathbf{S}}$ are such that $M\simeq_{\beta}M^{\prime}$. Then $M$ is Taylor normalizable iff $M^{\prime}$ is Taylor normalizable, and in this case $\mathord{\mathsf{NF}}{\left(\mathord{\tau}{\left(M\right)}\right)}=\mathord{\mathsf{NF}}{\left(\mathord{\tau}{\left(M^{\prime}\right)}\right)}$.222222 In the standard terminology of denotational semantics, Theorem 5 expresses the soundness of $\mathord{\mathsf{NF}}{\left(\mathord{\tau}{\left(\cdot\right)}\right)}$ on Taylor normalizable terms.

Proof 8.14**.**

The first part is a direct corollary of Lemma 8.12. By Lemma 7.10, it follows that $M\simeq_{\partial\,(\oc)\mathfrak{N}}M^{\prime}$, and then we conclude by Corollary 8.6.

In other words, when restricted to Taylor normalizable terms, the normal form of Taylor expansion is a valid notion of denotation. Remark that, in general, it is not possible to generalize this result to those terms $M$ such that $\mathord{\tau}{\left(M\right)}$ is normalizable because of the interaction with coefficients: consider, e.g., $0\simeq_{\mathord{\tau}}{\left(I\right)}\,{\infty_{x}}+(-1).{\left(I\right)}\,{\infty_{x}}\mathrel{{\Rightarrow_{\beta}}}\infty_{x}+(-1).{\left(I\right)}\,{\infty_{x}}$, and observe that $\mathord{\tau}{\left(\infty_{x}+(-1).{\left(I\right)}\,{\infty_{x}}\right)}\not\in\mathbf{S}{\left\langle\mathfrak{N}\right\rangle}$.

Definition 8.15**.**

We define the left reduct of an algebraic $\lambda$-term inductively as follows:

[TABLE]

Observe that this definition is exhaustive by Fact 3. It should be clear that $M\mathrel{{\Rightarrow_{\beta}}}\mathord{\mathsf{L}}{\left(M\right)}$ for all term $M$, and that $\mathord{\mathsf{L}}{\left(M\right)}=M$ when $M$ is in normal form (although the converse may not hold). Now we can establish that $\mathord{\mathsf{L}}$ commutes with Taylor expansion.

Lemma 8.16**.**

For all $\sigma\in\mathbf{S}^{\Delta}$, $\mathord{\mathsf{L}}{\left({\sigma}^{\oc}\right)}={\mathord{\mathsf{L}}{\left(\sigma\right)}}^{\oc}$.

Proof 8.17**.**

First observe that by the definition of $\mathord{\mathsf{L}}$ and the linear-continuity of both $\mathord{\mathsf{L}}$ and the monomial construction, for all $\sigma_{1},\dotsc,\sigma_{n}\in\mathbf{S}^{\Delta}$, we have $\mathord{\mathsf{L}}{\left({\left[\sigma_{1},\dotsc,\sigma_{k}\right]}\right)}={\left[\mathord{\mathsf{L}}{\left(\sigma_{1}\right)},\dotsc,\mathord{\mathsf{L}}{\left(\sigma_{k}\right)}\right]}$. In particular, $\mathord{\mathsf{L}}{\left(\sigma^{k}\right)}=\mathord{\mathsf{L}}{\left(\sigma\right)}^{k}$. We deduce that $\mathord{\mathsf{L}}{\left({\sigma}^{\oc}\right)}=\mathord{\mathsf{L}}{\left(\sum_{k\in\mathbf{N}}\frac{1}{k\,\mathord{!}}.{\sigma^{k}}\right)}=\sum_{k\in\mathbf{N}}\frac{1}{k\,\mathord{!}}.\mathord{\mathsf{L}}{\left(\sigma\right)}^{k}={\mathord{\mathsf{L}}{\left(\sigma\right)}}^{\oc}$, by the linear-continuity of $\mathord{\mathsf{L}}$.

Lemma 8.18**.**

For all $M\in\Lambda_{\mathbf{S}}$, $\mathord{\mathsf{L}}{\left(\mathord{\tau}{\left(M\right)}\right)}=\mathord{\tau}{\left(\mathord{\mathsf{L}}{\left(M\right)}\right)}$.

Proof 8.19**.**

By induction on the definition of $\mathord{\mathsf{L}}{\left(M\right)}$: in addition to the inductive hypothesis and the linear-continuity of $\mathord{\mathsf{L}}$, we use Lemma 8.16 in the case of a head variable, and Lemmas 4.4, 4.5 and 8.16 in the case of a head $\beta$-redex.

As a direct corollary of Theorem 4, we obtain:

Theorem 8.19**.**

For all Taylor normalizable term $M$, the sequence of normal resource vectors ${\left(\mathord{\tau}{\left(\mathord{\mathsf{L}}^{k}{\left(M\right)}\right)}\mathord{\upharpoonright}_{\mathcal{N}}\right)}_{k\in\mathbf{N}}$ converges to $\mathord{\mathsf{NF}}{\left(\mathord{\tau}{\left(M\right)}\right)}$ in $\mathbf{S}^{\mathcal{N}}$.

This property is very much akin to the fact that the Böhm tree $\mathord{\mathsf{BT}}{\left(M\right)}$ of a pure $\lambda$-term $M$ is obtained as the limit (in an order theoretic sense) of normal form approximants of the left reducts of $M$. This analogy will be made explicit in Section 9. Before that, we apply our results to normalizable algebraic $\lambda$-terms.

8.3. Taylor expansion and normalization commute on the nose

By a general standardization argument, we can show that parallel reduction is a normalization strategy:

Lemma 8.20**.**

An algebraic $\lambda$-term $M$ is normalizable iff there exists $k\in\mathbf{N}$, such that $\mathord{\mathsf{L}}^{k}{\left(M\right)}=\mathord{\mathsf{NF}}{\left(M\right)}$.

Proof 8.21**.**

Recall that we consider algebraic $\lambda$-terms up to $\simeq_{+}$ only. Then one can for instance use the general standardization technique developed by Leventis for a slightly different presentation of the calculus [Lev16].

A direct consequence is that $M$ normalizes iff the judgement ${M}\,\mathord{\Downarrow}$ can be derived inductively by the following rules:232323 Moreover, it seems natural to conjecture that if ${M}\,\mathord{\Downarrow}$ then $M$ (or, rather, its $\simeq_{\mathrm{v}}$-class) is normalizable in the sense of Alberti [Alb14], and then the obtained normal forms are the same (up to $\simeq_{\mathrm{v}}$).

{S}\,\mathord{\Downarrow}$${\lambda x\,{S}}\,\mathord{\Downarrow}

{M_{1}}\,\mathord{\Downarrow}$$\cdots$${M_{n}}\,\mathord{\Downarrow}$${{\left(x\right)}\,{M_{1}\cdots M_{n}}}\,\mathord{\Downarrow}

{{\left(S{\left[M_{0}/x\right]}\right)}\,{M_{1}\cdots M_{n}}}\,\mathord{\Downarrow}$${{\left(\lambda x\,{S}\right)}\,{M_{0}\,M_{1}\cdots M_{n}}}\,\mathord{\Downarrow}

${0}\,\mathord{\Downarrow}$

{M}\,\mathord{\Downarrow}$${a.M}\,\mathord{\Downarrow}

{M}\,\mathord{\Downarrow}$${N}\,\mathord{\Downarrow}$${\left(M+N\right)}\,\mathord{\Downarrow}

In the remaining of this subsection, we prove that normalizable algebraic $\lambda$-terms are Taylor normalizable, using a reducibility technique: like in Ehrhard’s work for the typed case [Ehr10], or our previous work for the strongly normalizable case [PTV16], $(\oc)\mathfrak{N}$ is the analogue of a reducibility candidate. We prove each key property (Lemmas 8.22 to 8.29) using the family of structures $(\oc)\mathfrak{N}_{d}$ rather than $(\oc)\mathfrak{N}$ directly: this will be useful in section 9, while the corresponding results for $(\oc)\mathfrak{N}$ are immediately derived from those.

Lemma 8.22**.**

If $\mathcal{S}\in\mathfrak{N}_{d}$ then $\lambda x\,{\mathcal{S}}\in\mathfrak{N}_{d}$.

Proof 8.23**.**

Let $t^{\prime}\in\mathcal{N}_{d}$ and $t\in{\left(\lambda x\,{\mathcal{S}}\right)}\mathbin{\cap}\mathord{\uparrow}{t^{\prime}}$. Necessarily, $t=\lambda x\,{s}$ and $t^{\prime}=\lambda x\,{s^{\prime}}$ with $s\in{\mathcal{S}}\mathbin{\cap}\mathord{\uparrow}{s^{\prime}}$ which is finite by assumption.

Lemma 8.24**.**

If $\mathcal{S}\in\mathfrak{N}_{d}$ then ${\mathcal{S}}^{\oc}\in\oc\mathfrak{N}_{d+1}$.

Proof 8.25**.**

Let $\overline{t}^{\prime}\in\oc\mathcal{N}_{d+1}$ and $\overline{t}\in{{\mathcal{S}}^{\oc}}\mathbin{\cap}\mathord{\uparrow}{\overline{t}^{\prime}}$. Write $n=\mathord{\#}{\overline{t}^{\prime}}$. Without loss of generality, we can write $\overline{t}={\left[t_{1},\dotsc,t_{n}\right]}$ and $\overline{t}^{\prime}={\left[t^{\prime}_{1},\dotsc,t^{\prime}_{n}\right]}$ so that $t_{i}\geq_{\partial}t^{\prime}_{i}$ and $t^{\prime}_{i}\in\mathcal{N}_{d}$, for all $i\in{\left\{1,\dotsc,n\right\}}$. Since $\overline{t}\in{{\mathcal{S}}^{\oc}}$, each $t_{i}\in{\mathcal{S}}$. Since $\mathcal{S}\in\mathfrak{N}_{d}$, $t^{\prime}_{i}$ being fixed, there are finitely many possible values for each $t_{i}$.

Lemma 8.26**.**

If $\overline{\mathcal{T}}_{1},\dotsc,\overline{\mathcal{T}}_{n}\in\oc\mathfrak{N}_{d}$ then ${\left\langle x\right\rangle}\,{\overline{\mathcal{T}}_{1}\cdots\overline{\mathcal{T}}_{n}}\in\mathfrak{N}_{d}$.

Proof 8.27**.**

Let $t^{\prime}\in\mathcal{N}_{d}$ and $t\in{\left({\left\langle x\right\rangle}\,{\overline{\mathcal{T}}_{1}\cdots\overline{\mathcal{T}}_{n}}\right)}\mathbin{\cap}\mathord{\uparrow}{t^{\prime}}$. Necessarily, $t={\left\langle x\right\rangle}\,{\overline{t}_{1}\cdots\overline{t}_{n}}$ and $t^{\prime}={\left\langle x\right\rangle}\,{\overline{t}^{\prime}_{1}\cdots\overline{t}^{\prime}_{n}}$ and, for each $i\in{\left\{1,\dotsc,n\right\}}$, $\overline{t}_{i}\in\overline{\mathcal{T}}_{i}$, $\overline{t}_{i}\geq_{\partial}\overline{t}^{\prime}_{i}$ and $\overline{t}^{\prime}_{i}\in\oc\mathcal{N}_{d}$: since $\overline{\mathcal{T}}_{i}\in\oc\mathfrak{N}_{d}$, there are finitely many possible values for each $\overline{t}_{i}$.

Corollary 8.28**.**

If $\mathcal{T}_{1},\dotsc,\mathcal{T}_{n}\in\mathfrak{N}_{d}$ then ${\left\langle x\right\rangle}\,{{\mathcal{T}_{1}}^{\oc}\cdots{{\mathcal{T}_{n}}^{\oc}}}\in\mathfrak{N}_{d+1}$.

Lemma 8.29**.**

If ${\left\langle\partial_{x}\mathcal{S}\cdot\overline{\mathcal{T}}_{0}\right\rangle}\,{{\overline{\mathcal{T}}_{1}}\cdots{\overline{\mathcal{T}}_{n}}}\in\mathfrak{N}_{d}$ then ${\left\langle\lambda x\,{\mathcal{S}}\right\rangle}\,{{\overline{\mathcal{T}}_{0}}\,{\overline{\mathcal{T}}_{1}}\cdots{\overline{\mathcal{T}}_{n}}}\in\mathfrak{N}_{d}$.

Proof 8.30**.**

Let $u^{\prime}\in\mathcal{N}_{d}$, and let $u\in{\left({\left\langle\lambda x\,{\mathcal{S}}\right\rangle}\,{{\overline{\mathcal{T}}_{0}}\,{\overline{\mathcal{T}}_{1}}\cdots{\overline{\mathcal{T}}_{n}}}\right)}\mathbin{\cap}\mathord{\uparrow}{u^{\prime}}$. In other words, $u^{\prime}\in{\left|\mathord{\mathsf{NF}}{\left(u\right)}\right|}$ and we can write $u={\left\langle\lambda x\,{s}\right\rangle}\,{{\overline{t}_{0}}\,{\overline{t}_{1}}\cdots{\overline{t}_{n}}}$ with $s\in{\left|\mathcal{S}\right|}$ and $\overline{t}_{i}\in{\left|\overline{\mathcal{T}}_{i}\right|}$ for $i\in{\left\{0,\dotsc,n\right\}}$. Write $v={\left\langle\partial_{x}s\cdot\overline{t}_{0}\right\rangle}\,{{\overline{t}_{1}}\cdots{\overline{t}_{n}}}$: Corollary 3.4 entails $v\geq_{\partial}u^{\prime}$, hence we have $v\in{\left({\left\langle\partial_{x}\mathcal{S}\cdot\overline{\mathcal{T}}_{0}\right\rangle}\,{{\overline{\mathcal{T}}_{1}}\cdots{\overline{\mathcal{T}}_{n}}}\right)}\mathbin{\cap}\mathord{\uparrow}{u^{\prime}}$. By assumption, there are finitely many possible values for $v$. Then, $v$ being fixed, by Lemma 3.4, we have $\mathord{\mathbf{fv}}{\left(u\right)}=\mathord{\mathbf{fv}}{\left(v\right)}$ and $\mathord{\mathbf{s}}{\left(u\right)}\leq 2\mathord{\mathbf{s}}{\left(v\right)}+2$, hence there are finitely many possible values for $u$.

Theorem 8.30**.**

If $M$ is normalizable, then $\mathord{\mathcal{T}}{\left(M\right)}\in\mathfrak{N}$, and $\mathord{\tau}{\left(M\right)}\in\mathbf{S}{\left\langle\mathfrak{N}\right\rangle}$.

Proof 8.31**.**

By induction on the derivation of ${M}\,\mathord{\Downarrow}$: Lemma 8.22, Corollary 8.28 and Lemma 8.29 respectively entail the translation of the first three inductive rules through Taylor expansion. The other three follow from the fact that $\mathfrak{N}$ is a resource structure (because it is a finiteness structure).

It remains to prove that in this case, $\mathord{\tau}{\left(\mathord{\mathsf{NF}}{\left(M\right)}\right)}$ is indeed the normal form of $\mathord{\tau}{\left(M\right)}$.

Theorem 8.31**.**

If $M$ is normalizable, then $\mathord{\mathsf{NF}}{\left(\mathord{\tau}{\left(M\right)}\right)}=\mathord{\tau}{\left(\mathord{\mathsf{NF}}{\left(M\right)}\right)}$.

Proof 8.32**.**

By Theorem 7, $M$ is Taylor normalizable. Then Theorem 5 entails $\mathord{\mathsf{NF}}{\left(\mathord{\tau}{\left(M\right)}\right)}=\mathord{\mathsf{NF}}{\left(\mathord{\tau}{\left(\mathord{\mathsf{NF}}{\left(M\right)}\right)}\right)}=\mathord{\tau}{\left(\mathord{\mathsf{NF}}{\left(M\right)}\right)}$.

8.4. Conservativity

The restriction to normalizable vectors allows us to prove an analogue of Lemma 7.24, without any assumption on the semiring of scalars.

Lemma 8.33**.**

Let $M,N\in\Lambda$ be normalizable. Then $M\simeq_{\partial\,\mathfrak{N}}N$ iff $M\simeq_{\beta}N$.

Proof 8.34**.**

Assume $M\simeq_{\partial\,\mathfrak{N}}N$. By Corollary 8.6, we have $\mathord{\mathsf{NF}}{\left(\mathord{\tau}{\left(M\right)}\right)}=\mathord{\mathsf{NF}}{\left(\mathord{\tau}{\left(M^{\prime}\right)}\right)}$. By Theorem 8, we obtain $\mathord{\mathsf{NF}}{\left(M\right)}\simeq_{\mathord{\tau}}\mathord{\mathsf{NF}}{\left(M^{\prime}\right)}$. Since $M$ and $N$ are pure $\lambda$-terms, we deduce $\mathord{\mathsf{NF}}{\left(M\right)}=\mathord{\mathsf{NF}}{\left(N\right)}$ from the injectivity of $\mathord{\tau}$ on $\Lambda$.

The reverse direction is similar to Theorem 5 and does not depend on $M$ and $N$ being pure $\lambda$-terms: apply Lemmas 7.10, 8.4 and 8.12 to the reduction path from $M$ to $N$

We can adapt this result to non-normalizing pure $\lambda$-terms thanks to previous work by Ehrhard and Regnier:242424 We could as well rely on Theorem 9, to be proved in the next section.

{thmC}

[[ER08, ER06]]

For all pure $\lambda$-term $M\in\Lambda$, $\mathord{\mathcal{T}}{\left(M\right)}\in\mathfrak{N}$ and $\mathord{\mathsf{NF}}{\left(\mathord{\tau}{\left(M\right)}\right)}=\mathord{\tau}{\left(\mathord{\mathsf{BT}}{\left(M\right)}\right)}$ where $\mathord{\mathsf{BT}}{\left(M\right)}$ denotes the Böhm tree of $M$.

Here Böhm tree is to be understood as generalized normal form for left $\beta$-reduction. In particular it does not involve $\eta$-expansion. More formally, the Böhm tree of a $\lambda$-term is the possibly infinite tree obtained coinductively as follows:

• •

if $M$ is head normalizable and its head normal form is $\lambda x_{1}\,{\cdots\lambda x_{n}\,{{\left(x\right)}\,{N_{1}\cdots N_{k}}}}$ then $\mathord{\mathsf{BT}}{\left(M\right)}\mathrel{\mathord{:}\mathord{=}}\lambda x_{1}\,{\cdots\lambda x_{n}\,{{\left(x\right)}\,{\mathord{\mathsf{BT}}{\left(N_{1}\right)}\cdots\mathord{\mathsf{BT}}{\left(N_{k}\right)}}}}$

• •

otherwise $\mathord{\mathsf{BT}}{\left(M\right)}\mathrel{\mathord{:}\mathord{=}}\bot$, where $\bot$ is a constant representing unsolvability.

Taylor expansion can be generalized to Böhm trees [ER06], setting in particular $\mathord{\tau}{\left(\bot\right)}=0$: this is still injective.

Lemma 8.35**.**

If $M,N\in\Lambda$ and $M\simeq_{\partial\,\mathfrak{N}}N$ then $\mathord{\mathsf{BT}}{\left(M\right)}=\mathord{\mathsf{BT}}{\left(N\right)}$.

Proof 8.36**.**

By Corollary 8.6, we have $\mathord{\mathsf{NF}}{\left(\mathord{\tau}{\left(M\right)}\right)}=\mathord{\mathsf{NF}}{\left(\mathord{\tau}{\left(M^{\prime}\right)}\right)}$. By Theorem 8.34, we obtain $\mathord{\tau}{\left(\mathord{\mathsf{BT}}{\left(M\right)}\right)}=\mathord{\tau}{\left(\mathord{\mathsf{BT}}{\left(N\right)}\right)}$. We conclude since $\mathord{\tau}$ is injective on Böhm trees.

In the next and final section, we prove a generalization of Theorem 8.34 to the non-uniform setting which is made possible by the results we have achieved so far.

9. Normal form of Taylor expansion, façon Böhm trees

The Böhm tree construction is often introduced as the limit of an increasing sequence $(\mathord{\mathsf{BT}}_{d}{\left(M\right)})_{d\in\mathbf{N}}$ of finite normal form approximants, aka finite Böhm trees, where $\mathord{\mathsf{BT}}_{d}{\left(M\right)}$ is defined inductively as follows:

• •

$\mathord{\mathsf{BT}}_{0}{\left(M\right)}=\bot$;

• •

if $M$ is head normalizable and its head normal form is $\lambda x_{1}\,{\cdots\lambda x_{n}\,{{\left(x\right)}\,{N_{1}\cdots N_{k}}}}$ then $\mathord{\mathsf{BT}}_{d+1}{\left(M\right)}\mathrel{\mathord{:}\mathord{=}}\lambda x_{1}\,{\cdots\lambda x_{n}\,{{\left(x\right)}\,{\mathord{\mathsf{BT}}_{d}{\left(N_{1}\right)}\cdots\mathord{\mathsf{BT}}_{d}{\left(N_{k}\right)}}}}$

• •

otherwise $\mathord{\mathsf{BT}}_{d+1}{\left(M\right)}\mathrel{\mathord{:}\mathord{=}}\bot$;

and the order on Böhm trees is the contextual closure of the inequality $\bot\leq M$ for all $M$.

In this final section of our paper, we show that the normal form of Taylor expansion operator generalizes this construction to the class of hereditarily determinable terms: these encompass both all pure $\lambda$-terms and all normalizable algebraic $\lambda$-terms, but exclude terms such as $\infty_{x}$, that produce unbounded sums of head normal forms. More precisely, we show that any hereditarily determinable term $M$ is Taylor normalizable, and moreover admits a sequence of approximants ${\left(\mathsf{NA}_{d}{\left(M\right)}\right)}_{d\in\mathbf{N}}$, such that each $\mathsf{NA}_{d}{\left(M\right)}$ is an algebraic $\lambda$-term in normal form, and the sequence of normal term vectors ${\left(\mathord{\tau}{\left(\mathsf{NA}_{d}{\left(M\right)}\right)}\right)}_{d\in\mathbf{N}}$ converges to $\mathord{\mathsf{NF}}{\left(\mathord{\tau}{\left(M\right)}\right)}$.

The results in this section should not hide the fact that the more fundamental notion is that of Taylor normalizable term, which arises naturally by combining Taylor expansion with the normalization of resource terms, subject to a summability condition. We believe this approach is quite robust, and may be adapted modularly following both parameters: to other systems admitting Taylor expansion; and to variants of summability, possibly associated with topological conditions of the semiring of scalars.

By contrast, the definition of hereditarily determinable terms is essentially ad-hoc. Its only purpose is to allow us to generalize Theorem 8.34 and support our claim that: the normal form of Taylor expansion extends the notion of Böhm tree to the non-uniform setting.

9.1. Taylor unsolvability

In the ordinary $\lambda$-calculus, head normalizable terms are exactly those with a non trivial Böhm tree. This is reflected via Taylor expansion: it is easy to check that $\mathord{\mathsf{NF}}{\left(\mathord{\tau}{\left(M\right)}\right)}=0$ iff $M$ has no head normal form. In the non uniform setting, a similar result holds, although we need to be more careful about the interplay between reduction and coefficients.

Definition 9.1**.**

We say an algebraic $\lambda$-term $M$ (resp. simple term $S$) is weakly solvable if the judgement ${M}\,\mathord{\Downarrow}_{\mathrm{w}}$ can be derived inductively by the following rules:

${{\left(x\right)}\,{M_{1}\cdots M_{n}}}\,\mathord{\Downarrow}_{\mathrm{w}}$

{S}\,\mathord{\Downarrow}_{\mathrm{w}}$${\lambda x\,{S}}\,\mathord{\Downarrow}_{\mathrm{w}}

{{\left(S{\left[M_{0}/x\right]}\right)}\,{M_{1}\cdots M_{n}}}\,\mathord{\Downarrow}_{\mathrm{w}}$${{\left(\lambda x\,{S}\right)}\,{M_{0}\,M_{1}\cdots M_{n}}}\,\mathord{\Downarrow}_{\mathrm{w}}

{M}\,\mathord{\Downarrow}_{\mathrm{w}}$${a.M}\,\mathord{\Downarrow}_{\mathrm{w}}

{M}\,\mathord{\Downarrow}_{\mathrm{w}}$${M+N}\,\mathord{\Downarrow}_{\mathrm{w}}

{N}\,\mathord{\Downarrow}_{\mathrm{w}}$${M+N}\,\mathord{\Downarrow}_{\mathrm{w}}

It should be clear that, if $M$ is a pure $\lambda$-term, ${M}\,\mathord{\Downarrow}_{\mathrm{w}}$ iff $M$ is head normalizable. In the general case, we show that ${M}\,\mathord{\Downarrow}_{\mathrm{w}}$ iff normalizing the Taylor expansion of $M$ yields a non trivial result. More formally:

Definition 9.2**.**

We say an algebraic $\lambda$-term $M\in\Lambda_{\mathbf{S}}$ is Taylor unsolvable and write ${M}\,\mathord{\Uparrow}$ if $\mathord{\mathsf{NF}}{\left(s\right)}=0$ for all $s\in\mathord{\mathcal{T}}{\left(M\right)}$.

In particular, if ${M}\,\mathord{\Uparrow}$ then $\mathord{\tau}{\left(M\right)}\in\mathbf{S}{\left\langle\mathfrak{N}\right\rangle}$ and $\mathord{\mathsf{NF}}{\left(\mathord{\tau}{\left(M\right)}\right)}=0$: indeed, ${\left|\mathord{\tau}{\left(M\right)}\right|}\subseteq\mathord{\mathcal{T}}{\left(M\right)}$. Beware that the reverse implication does not hold in general. We can then show that ${M}\,\mathord{\Downarrow}_{\mathrm{w}}$ iff $M$ is Taylor solvable (Lemmas 9.3 and 9.5).

Lemma 9.3**.**

If there exists $s\in\mathord{\mathcal{T}}{\left(M\right)}$ such that $\mathord{\mathsf{NF}}{\left(s\right)}\not=0$ then ${M}\,\mathord{\Downarrow}_{\mathrm{w}}$.

Proof 9.4**.**

We prove by induction on $k\in\mathbf{N}$ then on $M\in\Lambda_{\mathbf{S}}$ that if ${\left|\mathord{\mathsf{L}}^{k}{\left(s\right)}\right|}$ contains a normal resource term and $s\in\mathord{\mathcal{T}}{\left(M\right)}$ then ${M}\,\mathord{\Downarrow}_{\mathrm{w}}$.

If $M={\left(x\right)}\,{M_{1}\cdots M_{n}}$ we conclude directly.

If $M=\lambda x\,{T}$ then $s=\lambda x\,{t}$ with $t\in\mathord{\mathcal{T}}{\left(T\right)}$: necessarily ${\left|\mathord{\mathsf{L}}^{k}{\left(t\right)}\right|}$ contains a normal resource term and by induction hypothesis we obtain ${T}\,\mathord{\Downarrow}_{\mathrm{w}}$ hence ${M}\,\mathord{\Downarrow}_{\mathrm{w}}$.

If $M={\left(\lambda x\,{T}\right)}\,{M_{0}\,M_{1}\cdots M_{n}}$ then $s={\left\langle\lambda x\,{t}\right\rangle}\,{\overline{s}_{0}\,\overline{s}_{1}\cdots\overline{s}_{n}}$ with $t\in\mathord{\mathcal{T}}{\left(T\right)}$ and $\overline{s}_{i}\in{\mathord{\mathcal{T}}{\left(M_{i}\right)}}^{\oc}$ for $i\in{\left\{0,\dotsc,n\right\}}$. Necessarily $k>0$ and there is $s^{\prime}\in{\left|\mathord{\mathsf{L}}{\left(s\right)}\right|}={\left|{\left\langle\partial_{x}t\cdot\overline{s}_{0}\right\rangle}\,{\overline{s}_{1}\cdots\overline{s}_{n}}\right|}$ such that ${\left|\mathord{\mathsf{L}}^{k-1}{\left(s^{\prime}\right)}\right|}$ contains a normal resource term. By Lemma 4.5, $s^{\prime}\in\mathord{\mathcal{T}}{\left({\left(T{\left[M_{0}/x\right]}\right)}\,{M_{1}\cdots M_{n}}\right)}$: we obtain ${{\left(T{\left[M_{0}/x\right]}\right)}\,{M_{1}\cdots M_{n}}}\,\mathord{\Downarrow}_{\mathrm{w}}$ by induction hypothesis, and then ${M}\,\mathord{\Downarrow}_{\mathrm{w}}$.

If $M=a.N$, $M=N+P$ or $M=P+N$ with $s\in\mathord{\mathcal{T}}{\left(N\right)}$ then we obtain ${N}\,\mathord{\Downarrow}_{\mathrm{w}}$ by induction hypothesis, and then ${M}\,\mathord{\Downarrow}_{\mathrm{w}}$.

Lemma 9.5**.**

If ${M}\,\mathord{\Downarrow}_{\mathrm{w}}$, then there exists $s\in\mathord{\mathcal{T}}{\left(M\right)}$ such that $\mathord{\mathsf{NF}}{\left(s\right)}\not=0$.

Proof 9.6**.**

By induction on the derivation of ${M}\,\mathord{\Downarrow}_{\mathrm{w}}$.

If $M={\left(x\right)}\,{M_{1}\cdots M_{n}}$, set $s={\left\langle x\right\rangle}\,{{\left[\right]}\cdots{\left[\right]}}$ ($x$ applied $n$ times to the empty monomial): $s\in\mathord{\mathcal{T}}{\left(M\right)}$ and $s$ is normal.

If $M=\lambda x\,{T}$ with ${T}\,\mathord{\Downarrow}_{\mathrm{w}}$: by induction hypothesis, we obtain $t\in\mathord{\mathcal{T}}{\left(T\right)}$ with $\mathord{\mathsf{NF}}{\left(t\right)}\not=0$ and set $s=\lambda x\,{t}$.

If $M=\lambda x\,{T}{M_{0}\,M_{1}\cdots M_{n}}$ and $M^{\prime}={\left(T{\left[M_{0}/x\right]}\right)}\,{M_{1}\cdots M_{n}}$ with ${M^{\prime}}\,\mathord{\Downarrow}_{\mathrm{w}}$, the induction hypothesis gives $s^{\prime}\in\mathord{\mathcal{T}}{\left(M^{\prime}\right)}$ such that $\mathord{\mathsf{NF}}{\left(s^{\prime}\right)}\not=0$. By Lemma 4.5, there exist $t\in\mathord{\mathcal{T}}{\left(T\right)}$ and $\overline{u}_{i}\in{\mathord{\mathcal{T}}{\left(M_{i}\right)}}^{\oc}$ for $i\in{\left\{0,\dotsc,n\right\}}$ such that $s^{\prime}\in{\left|{\left\langle\partial_{x}t\cdot\overline{u}_{0}\right\rangle}\,{\overline{u}_{1}\cdots\overline{u}_{n}}\right|}$. We then set $s={\left\langle\lambda x\,{t}\right\rangle}\,{\overline{u}_{0}\cdots\overline{u}_{n}}$.

If $M=a.N$, $M=N+P$ or $M=P+N$ with ${N}\,\mathord{\Downarrow}_{\mathrm{w}}$: the induction hypothesis gives $s\in\mathord{\mathcal{T}}{\left(N\right)}\subseteq\mathord{\mathcal{T}}{\left(M\right)}$ with $\mathord{\mathsf{NF}}{\left(s\right)}\not=0$ directly.

Taylor unsolvable terms are thus exactly those that are not weakly solvable.252525 If we restrict to non-deterministic $\lambda$-terms (i.e. only add a sum operator to the usual $\lambda$-term constructs) then we obtain ${M}\,\mathord{\Uparrow}$ iff $\mathord{\mathsf{NF}}{\left(\mathord{\mathcal{T}}{\left(M\right)}\right)}=\emptyset$, which states the adequacy of $\mathord{\mathsf{NF}}{\left(\mathord{\mathcal{T}}{\left(\cdot\right)}\right)}$ for the observational equivalence associated with may-style head normalization.

They are moreover stable under $\simeq_{\beta}$:

Lemma 9.7**.**

If $M\mathrel{{\Rightarrow_{\beta}}}M^{\prime}$ then ${M}\,\mathord{\Uparrow}$ iff ${M^{\prime}}\,\mathord{\Uparrow}$.

Proof 9.8**.**

If $\mathcal{E}\subseteq(\oc)\Delta$, we write $\mathord{\mathsf{NF}}{\left(\mathcal{E}\right)}\mathrel{\mathord{:}\mathord{=}}\bigcup{{\left\{{\left|\mathord{\mathsf{NF}}{\left(e\right)}\right|}\mathrel{;}e\in\mathcal{E}\right\}}}$. We leave as an exercise to the reader the proof that $\mathord{\mathsf{NF}}{\left(\mathord{\mathcal{T}}{\left(M\right)}\right)}=\mathord{\mathsf{NF}}{\left(\mathord{\mathcal{T}}{\left(M^{\prime}\right)}\right)}$ as soon as $M\mathrel{{\Rightarrow_{\beta}}}M^{\prime}$: this is the analogue of Lemma 8.4 on Taylor supports (in particular there is no summability condition, and scalars play absolutely no rôle).

9.2. Hereditarily determinable terms

The Böhm tree construction is based on the fact that, for a pure $\lambda$-term $M$, either $M$ is unsolvable, or it reduces to a head normal form; and then the same holds for the arguments of the head variable. We will be able to follow a similar construction for the class of hereditarily determinable terms: intuitively, a simple term is in determinate form if it is either unsolvable or a head normal form; and a term is hereditarily determinable if it reduces to a sum of determinate forms, and this holds hereditarily in the arguments of head variables. Formally:

Definition 9.9**.**

Let $M\in\Lambda_{\mathbf{S}}$ be an algebraic $\lambda$-term. We say $M$ is $d$-determinable if the judgement ${M}\,\mathord{\Downarrow}_{d}$ can be derived inductively from the following rules:

${M}\,\mathord{\Downarrow}_{0}$

{M}\,\mathord{\Uparrow}$${M}\,\mathord{\Downarrow}_{d}

{S}\,\mathord{\Downarrow}_{d}$${\lambda x\,{S}}\,\mathord{\Downarrow}_{d}

{M_{1}}\,\mathord{\Downarrow}_{d}$$\cdots$${M_{n}}\,\mathord{\Downarrow}_{d}$${{\left(x\right)}\,{M_{1}\cdots M_{n}}}\,\mathord{\Downarrow}_{d+1}

{M}\,\mathord{\Downarrow}_{d}$${a.M}\,\mathord{\Downarrow}_{d}

{M}\,\mathord{\Downarrow}_{d}$${N}\,\mathord{\Downarrow}_{d}$${M+N}\,\mathord{\Downarrow}_{d}

{{\left(S{\left[M_{0}/x\right]}\right)}\,{M_{1}\cdots M_{n}}}\,\mathord{\Downarrow}_{d}$${{\left(\lambda x\,{S}\right)}\,{M_{0}\,M_{1}\cdots M_{n}}}\,\mathord{\Downarrow}_{d}

We say $M$ is hereditarily determinable and write ${M}\,\mathord{\Downarrow}_{\omega}$ if ${M}\,\mathord{\Downarrow}_{d}$ for all $d\in\mathbf{N}$. We say $M$ is in $d$-determinate form and write ${M}\,\mathsf{df}_{d}$ if ${M}\,\mathord{\Downarrow}_{d}$ is derivable from the above rules excluding the last one.

It should be clear that ${M}\,\mathord{\Downarrow}$ implies ${M}\,\mathord{\Downarrow}_{\omega}$. Observing that ${M}\,\mathord{\Uparrow}$ for all unsolvable pure $\lambda$-terms (i.e. those pure $\lambda$-terms having no head normal form), we moreover obtain ${M}\,\mathord{\Downarrow}_{\omega}$ for all $M\in\Lambda$.

We can already prove that hereditarily determinable terms are Taylor normalizable:262626 Observe that this fails if we replace $\mathord{\mathcal{T}}{\left(M\right)}$ with ${\left|\mathord{\tau}{\left(M\right)}\right|}$ in the definition of ${M}\,\mathord{\Uparrow}$: write $I\mathrel{\mathord{:}\mathord{=}}\lambda x\,{x}$ and consider, e.g., $M={\left(\lambda x\,{{\left(I\right)}\,{{\left(x+(-1).\infty_{y}\right)}}}\right)}\,{\infty_{y}}$ which head-reduces to ${\left(I\right)}\,{{\left(\infty_{y}+(-1).\infty_{y}\right)}}\simeq_{\mathord{\tau}}{\left(I\right)}\,{0}$, with ${{\left(I\right)}\,{0}}\,\mathord{\Uparrow}$ but of course $\mathord{\tau}{\left(M\right)}\not\in\mathfrak{N}_{0}$. The very same problem would occur if we were to consider terms up to $\simeq_{\mathrm{v}}$.

Lemma 9.10**.**

If ${M}\,\mathord{\Downarrow}_{d}$ then $\mathord{\mathcal{T}}{\left(M\right)}\in\mathfrak{N}_{d}$. If moreover ${M}\,\mathord{\Downarrow}_{\omega}$ then $\mathord{\mathcal{T}}{\left(M\right)}\in\mathfrak{N}$.

Proof 9.11**.**

The second fact follows directly from the first one, which we prove by induction on the derivation of ${M}\,\mathord{\Downarrow}_{d}$: we use the definition of ${M}\,\mathord{\Uparrow}$ for the base case, and rely on Lemma 8.22, Corollary 8.28, Lemma 8.29, or the fact that $\mathfrak{N}_{d}$ is a resource structure to establish the induction in the other cases.

On the other hand, there are Taylor normalizable terms that do not follow this pattern: intuitively, hereditarily determinable terms rule out any representation of an infinite sum of head normal forms, whereas Taylor normalizability allows to represent an infinite sum of normal forms as long as their Taylor expansions are pairwise disjoint. More formally:

Example 9.12**.**

Write $s_{0}\mathrel{\mathord{:}\mathord{=}}\lambda x\,{x}$, and $s_{n+1}\mathrel{\mathord{:}\mathord{=}}\lambda x\,{s_{n}}$. Let $M_{step}=\lambda y\,{\lambda z\,{z}}+\lambda y\,{\lambda z\,{\lambda x\,{{\left(y\right)}\,{y\,z}}}}$ and then $M_{loop}={\left(M_{step}\right)}\,{M_{step}\,\lambda x\,{x}}$. Write $u=\lambda y\,{\lambda z\,{z}}$ and $v_{n,k}=\lambda y\,{\lambda z\,{\lambda x\,{{\left\langle y\right\rangle}\,{y^{n}\,z^{k}}}}}$ so that $\mathord{\mathcal{T}}{\left(M_{step}\right)}={\left\{u\right\}}\mathbin{\cup}{\left\{v_{n,k}\mathrel{;}n,k\in\mathbf{N}\right\}}$. Let $s\in\mathord{\mathcal{T}}{\left(M_{loop}\right)}$ be such that $\mathord{\mathsf{NF}}{\left(s\right)}\not=0$: a simple inspection shows that either $s={\left\langle u\right\rangle}\,{{\left[\right]}\,{\left[s_{0}\right]}}$ and then $\mathord{\mathsf{NF}}{\left(s\right)}=s_{0}$, or $s={\left\langle v_{n,1}\right\rangle}\,{{\left[v_{0,1},\dotsc,v_{n-1,1},u\right]}\,{\left[s_{0}\right]}}$ and then $\mathord{\mathsf{NF}}{\left(s\right)}=s_{n+1}$. It follows that $M_{loop}$ is Taylor normalizable. On the other hand, observe that $\mathord{\mathsf{L}}^{2}{\left(M_{loop}\right)}=\lambda x\,{x}+\lambda x\,{M_{loop}}$, which is not $1$-determinate: hence no $\mathord{\mathsf{L}}^{2k}{\left(M_{loop}\right)}$ is $1$-determinate and it will follow from Lemma 9.15 that $M_{loop}$ is not $1$-determinable.

Hence hereditarily determinable terms form a strict subclass of Taylor normalizable terms, containing both pure $\lambda$-terms and normalizable algebraic $\lambda$-terms. For each level $d\in\mathbf{N}$, the class of $d$-determinable terms (resp. of $d$-determinate terms) is moreover stable under left reduction:

Lemma 9.13**.**

If ${M}\,\mathord{\Downarrow}_{d}$ (resp. ${M}\,\mathsf{df}_{d}$) then ${\mathord{\mathsf{L}}{\left(M\right)}}\,\mathord{\Downarrow}_{d}$ (resp. ${\mathord{\mathsf{L}}{\left(M\right)}}\,\mathsf{df}_{d}$).

Proof 9.14**.**

We give the proof for $d$-determinable terms, by induction on the derivation of ${M}\,\mathord{\Downarrow}_{d}$: the case of $d$-determinate terms is similar, except that we do not consider head redexes.

If $d=0$ the result is direct. Otherwise, write $d=d^{\prime}+1$.

If ${M}\,\mathord{\Uparrow}$ then ${\mathord{\mathsf{L}}{\left(M\right)}}\,\mathord{\Uparrow}$ by Lemma 9.7, and we conclude directly.

If $M=\lambda x\,{S}$ with ${S}\,\mathord{\Downarrow}_{d}$: by induction hypothesis ${\mathord{\mathsf{L}}{\left(S\right)}}\,\mathord{\Downarrow}_{d}$, and then ${\lambda x\,{\mathord{\mathsf{L}}{\left(S\right)}}}\,\mathord{\Downarrow}_{d}$.

If $M={\left(x\right)}\,{M_{1}\cdots M_{n}}$ with ${M_{i}}\,\mathord{\Downarrow}_{d^{\prime}}$ for $i\in{\left\{1,\dotsc,n\right\}}$: by induction hypothesis ${\mathord{\mathsf{L}}{\left(M_{i}\right)}}\,\mathord{\Downarrow}_{d^{\prime}}$ for $i\in{\left\{1,\dotsc,n\right\}}$, and then ${{\left(x\right)}\,{{\mathord{\mathsf{L}}{\left(M_{1}\right)}}\cdots{\mathord{\mathsf{L}}{\left(M_{n}\right)}}}}\,\mathord{\Downarrow}_{d}$.

If $M={\left(\lambda x\,{S}\right)}\,{M_{0}\,M_{1}\cdots M_{n}}$ with ${{\left(S{\left[M_{0}/x\right]}\right)}\,{M_{1}\cdots M_{n}}}\,\mathord{\Downarrow}_{d}$ then we conclude directly since $\mathord{\mathsf{L}}{\left(M\right)}={\left(S{\left[M_{0}/x\right]}\right)}\,{M_{1}\cdots M_{n}}$.

If $M=a.N$ with ${N}\,\mathord{\Downarrow}_{d}$: by induction hypothesis ${\mathord{\mathsf{L}}{\left(N\right)}}\,\mathord{\Downarrow}_{d}$, and then ${a.\mathord{\mathsf{L}}{\left(N\right)}}\,\mathord{\Downarrow}_{d}$.

If $M=N+P$ with ${N}\,\mathord{\Downarrow}_{d}$ and ${P}\,\mathord{\Downarrow}_{d}$: by induction hypothesis ${\mathord{\mathsf{L}}{\left(N\right)}}\,\mathord{\Downarrow}_{d}$ and ${\mathord{\mathsf{L}}{\left(P\right)}}\,\mathord{\Downarrow}_{d}$, and then ${\mathord{\mathsf{L}}{\left(N\right)}+\mathord{\mathsf{L}}{\left(P\right)}}\,\mathord{\Downarrow}_{d}$.

Now we can formally prove that applying the parallel left reduction strategy to $d$-determinable terms does reach $d$-determinate forms.

Lemma 9.15**.**

If ${M}\,\mathord{\Downarrow}_{d}$ then there exists $k\in\mathbf{N}$ such that ${\mathord{\mathsf{L}}^{k}{\left(M\right)}}\,\mathsf{df}_{d}$.

Proof 9.16**.**

By induction on the derivation of ${M}\,\mathord{\Downarrow}_{d}$.

If $d=0$ or ${M}\,\mathord{\Uparrow}$, then ${M}\,\mathsf{df}_{d}$.

If $M=\lambda x\,{S}$ with ${S}\,\mathord{\Downarrow}_{d}$: by induction hypothesis, we have $k\in\mathbf{N}$ such that ${\mathord{\mathsf{L}}^{k}{\left(S\right)}}\,\mathsf{df}_{d}$ and then $\mathord{\mathsf{L}}^{k}{\left(M\right)}=\lambda x\,{\mathord{\mathsf{L}}^{k}{\left(S\right)}}$ hence ${\mathord{\mathsf{L}}^{k}{\left(M\right)}}\,\mathsf{df}_{d}$.

If $M={\left(x\right)}\,{M_{1}\cdots M_{n}}$ with $d>0$ and ${M_{i}}\,\mathord{\Downarrow}_{d-1}$ for each $i\in{\left\{1,\dotsc,n\right\}}$: by induction hypothesis, we obtain $k_{i}\in\mathbf{N}$ such that ${\mathord{\mathsf{L}}^{k_{i}}{\left(M_{i}\right)}}\,\mathsf{df}_{d-1}$ for each $i\in{\left\{1,\dotsc,n\right\}}$. Let $k=\max{\left\{k_{i}\mathrel{;}1\leq i\leq n\right\}}$: by Lemma 9.13, we also have ${\mathord{\mathsf{L}}^{k}{\left(M_{i}\right)}}\,\mathsf{df}_{d-1}$ for all $i\in{\left\{1,\dotsc,n\right\}}$. Since $\mathord{\mathsf{L}}^{k}{\left(M\right)}=\mathord{\mathsf{L}}^{k}{\left({\left(x\right)}\,{M_{1}\cdots M_{n}}\right)}={\left(x\right)}\,{\mathord{\mathsf{L}}^{k}{\left(M_{1}\right)}\cdots\mathord{\mathsf{L}}^{k}{\left(M_{n}\right)}}$ we conclude that ${\mathord{\mathsf{L}}^{k}{\left(M\right)}}\,\mathsf{df}_{d}$.

If $M={\left(\lambda x\,{S}\right)}\,{M_{0}\,M_{1}\cdots M_{n}}$ with ${{\left(S{\left[M_{0}/x\right]}\right)}\,{M_{1}\cdots M_{n}}}\,\mathord{\Downarrow}_{d}$: by induction hypothesis, we have $k_{0}\in\mathbf{N}$ such that ${\mathord{\mathsf{L}}^{k_{0}}{\left({\left(S{\left[M_{0}/x\right]}\right)}\,{M_{1}\cdots M_{n}}\right)}}\,\mathsf{df}_{d}$. It is then sufficient to observe that $\mathord{\mathsf{L}}{\left(M\right)}={\left(S{\left[M_{0}/x\right]}\right)}\,{M_{1}\cdots M_{n}}$ and set $k=k_{0}+1$.

If $M=a.N$ with ${N}\,\mathord{\Downarrow}_{d}$: by induction hypothesis, we have $k\in\mathbf{N}$ such that ${\mathord{\mathsf{L}}^{k}{\left(S\right)}}\,\mathsf{df}_{d}$ and then $\mathord{\mathsf{L}}^{k}{\left(M\right)}=a.{\mathord{\mathsf{L}}^{k}{\left(S\right)}}$ hence ${\mathord{\mathsf{L}}^{k}{\left(M\right)}}\,\mathsf{df}_{d}$.

If $M=N+P$ with ${N}\,\mathord{\Downarrow}_{d}$ and ${P}\,\mathord{\Downarrow}_{d}$: by induction hypothesis, we have $k_{0},k_{1}\in\mathbf{N}$ such that ${\mathord{\mathsf{L}}^{k_{0}}{\left(N\right)}}\,\mathsf{df}_{d}$ and ${\mathord{\mathsf{L}}^{k_{1}}{\left(P\right)}}\,\mathsf{df}_{d}$ and then, setting $k=\max(k_{0},k_{1})$, $\mathord{\mathsf{L}}^{k}{\left(M\right)}=\mathord{\mathsf{L}}^{k}{\left(N\right)}+\mathord{\mathsf{L}}^{k}{\left(P\right)}$ hence ${\mathord{\mathsf{L}}^{k}{\left(M\right)}}\,\mathsf{df}_{d}$ by the previous lemma.

9.3. Approximants of the normal form of Taylor expansion

Now we introduce the analogue of finite Böhm trees for hereditarily determinable terms:

Definition 9.17**.**

If ${M}\,\mathord{\Downarrow}_{d}$ then we define the normal $d$-approximant $\mathsf{NA}_{d}{\left(M\right)}$ of $M$ inductively as follows: $\mathsf{NA}_{d}{\left(M\right)}\mathrel{\mathord{:}\mathord{=}}0$ if $d=0$ or ${M}\,\mathord{\Uparrow}$, and

[TABLE]

otherwise.

First observe that $d$ approximants are stable under parallel left reduction:

Lemma 9.18**.**

If ${M}\,\mathord{\Downarrow}_{d}$ then $\mathsf{NA}_{d}{\left(M\right)}=\mathsf{NA}_{d}{\left(\mathord{\mathsf{L}}{\left(M\right)}\right)}$.

Proof 9.19**.**

Recall indeed that, by Lemma 9.13, ${\mathord{\mathsf{L}}{\left(M\right)}}\,\mathord{\Downarrow}_{d}$ so that $\mathsf{NA}_{d}{\left(\mathord{\mathsf{L}}{\left(M\right)}\right)}$ is well defined. The proof is then straightforward, by induction on ${M}\,\mathord{\Downarrow}_{d}$.

We do not prove here that $d$-determinable terms and the associated $d$-approximants are stable under arbitrary reduction: if ${M}\,\mathord{\Downarrow}_{d}$ and $M\mathrel{{\Rightarrow_{\beta}}}M^{\prime}$ then ${M^{\prime}}\,\mathord{\Downarrow}_{d}$ and then $\mathsf{NA}_{d}{\left(M\right)}=\mathsf{NA}_{d}{\left(M^{\prime}\right)}$. We believe it is a very solid conjecture, but it would require us to develop a full standardization argument: in our non-deterministic setting, this is known to be tedious at best [Alb14, Lev16]. Since we introduced hereditarily determinable terms ad-hoc, only to be able to define normal $d$-approximants, we feel that the general study of their computational behaviour is not worth the effort.

Our next step is to show that if $M$ is in $d+1$ determinate form, then $\mathord{\tau}{\left(M\right)}\mathord{\upharpoonright}_{\mathcal{N}_{d}}$ depends only on $\mathsf{NA}_{d+1}{\left(M\right)}$.

Lemma 9.20**.**

If ${M}\,\mathsf{df}_{d+1}$ then, for all $s\in\mathcal{N}_{d}$, $\mathord{\tau}{\left(M\right)}_{s}=\mathord{\tau}{\left(\mathsf{NA}_{d+1}{\left(M\right)}\right)}_{s}$.

Proof 9.21**.**

By induction on the derivation of ${M}\,\mathsf{df}_{d+1}$, writing $M^{\prime}=\mathsf{NA}_{d+1}{\left(M\right)}$.

If ${M}\,\mathord{\Uparrow}$ then $M^{\prime}=0$ and $\mathord{\tau}{\left(M\right)}_{s}=0$ for all $s\in\mathcal{N}$, hence the result holds.

If $M=\lambda x\,{T}$ with ${T}\,\mathsf{df}_{d+1}$ then $M^{\prime}=\lambda x\,{\mathsf{NA}_{d+1}{\left(T\right)}}$ and we can assume $s=\lambda x\,{t}$: otherwise $\mathord{\tau}{\left(M\right)}_{s}=0=\mathord{\tau}{\left(M^{\prime}\right)}_{s}$. Then $t\in\mathcal{N}_{d}$ and by induction hypothesis $\mathord{\tau}{\left(M\right)}_{s}=\mathord{\tau}{\left(T\right)}_{t}=\mathord{\tau}{\left(\mathsf{NA}_{d+1}{\left(T\right)}\right)}_{t}=\mathord{\tau}{\left(M^{\prime}\right)}_{s}$.

If $M={\left(x\right)}\,{N_{1}\cdots N_{n}}$ with ${N_{i}}\,\mathsf{df}_{d}$ for all $i\in{\left\{1,\dotsc,n\right\}}$ then $M^{\prime}={\left(x\right)}\,{N^{\prime}_{1}\cdots N^{\prime}_{n}}$ with $N^{\prime}_{i}=\mathsf{NA}_{d}{\left(N_{i}\right)}$ and we can assume $s={\left\langle x\right\rangle}\,{\overline{t}_{1}\cdots\overline{t}_{n}}$: otherwise $\mathord{\tau}{\left(M\right)}_{s}=0=\mathord{\tau}{\left(M^{\prime}\right)}_{s}$. If $d=0$, $s\in\mathcal{N}_{0}$, hence $n=0$ and then $M=x=M^{\prime}$. Otherwise write $d=d^{\prime}+1$. For each $i\in{\left\{1,\dotsc,n\right\}}$, ${\left|\overline{t}_{i}\right|}\subseteq\mathcal{N}_{d^{\prime}}$. By induction hypothesis we obtain $\mathord{\tau}{\left(N_{i}\right)}_{u}=\mathord{\tau}{\left(N^{\prime}_{i}\right)}_{u}$ for all $u\in{\left|\overline{t}_{i}\right|}$: it follows that ${\mathord{\tau}{\left(N_{i}\right)}}^{\oc}_{\overline{t}_{i}}={\mathord{\tau}{\left(N^{\prime}_{i}\right)}}^{\oc}_{\overline{t}_{i}}$ by the definition of promotion. Then $\mathord{\tau}{\left(M\right)}_{s}=\prod_{i=1}^{n}\mathord{\tau}{\left(N_{i}\right)}_{\overline{t}_{i}}=\prod_{i=1}^{n}\mathord{\tau}{\left(N^{\prime}_{i}\right)}_{\overline{t}_{i}}=\mathord{\tau}{\left(M^{\prime}\right)}_{s}$.

If $M=a.N$ with ${N}\,\mathsf{df}_{d+1}$ then $\mathord{\tau}{\left(M\right)}_{s}=a.\mathord{\tau}{\left(N\right)}_{s}=a.\mathord{\tau}{\left(\mathsf{NA}_{d+1}{\left(N\right)}\right)}_{s}=\mathord{\tau}{\left(M^{\prime}\right)}_{s}$ by induction hypothesis.

Similarly, if $M=N+P$ with ${N}\,\mathsf{df}_{d+1}$ and ${P}\,\mathsf{df}_{d+1}$ then $\mathord{\tau}{\left(M\right)}_{s}=\mathord{\tau}{\left(N\right)}_{s}+\mathord{\tau}{\left(P\right)}_{s}=\mathord{\tau}{\left(\mathsf{NA}_{d+1}{\left(N\right)}\right)}_{s}+\mathord{\tau}{\left(\mathsf{NA}_{d+1}{\left(P\right)}\right)}_{s}=\mathord{\tau}{\left(M^{\prime}\right)}_{s}$ by induction hypothesis.

We obtain our final theorem:

Theorem 9.21**.**

For all hereditarily determinable term $M$, the sequence ${\left(\mathord{\tau}{\left(\mathsf{NA}_{d}{\left(M\right)}\right)}\right)}_{d\in\mathbf{N}}$ of normal vectors converges to $\mathord{\mathsf{NF}}{\left(\mathord{\tau}{\left(M\right)}\right)}$ in $\mathbf{S}^{\mathcal{N}}$.

Proof 9.22**.**

First observe that each $\mathord{\tau}{\left(\mathsf{NA}_{d}{\left(M\right)}\right)}\in\mathbf{S}^{\mathcal{N}}$, because $\mathsf{NA}_{d}{\left(M\right)}$ is in normal form. Let $s\in\mathcal{N}$ and fix $d\geq\mathord{\mathbf{d}}{\left(s\right)}+1$: by Lemmas 9.13, 9.15 and 9.18, there exists $k_{0}\in\mathbf{N}$ such that ${\mathord{\mathsf{L}}^{k}{\left(M\right)}}\,\mathsf{df}_{d}$ and $\mathsf{NA}_{d}{\left(\mathord{\mathsf{L}}^{k}{\left(M\right)}\right)}=\mathsf{NA}_{d}{\left(M\right)}$ whenever $k\geq k_{0}$. By Lemma 9.20, we moreover have $\mathord{\tau}{\left(\mathsf{NA}_{d}{\left(M\right)}\right)}_{s}=\mathord{\tau}{\left(\mathsf{NA}_{d}{\left(\mathord{\mathsf{L}}^{k}{\left(M\right)}\right)}\right)}_{s}=\mathord{\tau}{\left(\mathord{\mathsf{L}}^{k}{\left(M\right)}\right)}_{s}$. It follows that $\mathord{\tau}{\left(\mathsf{NA}_{d}{\left(M\right)}\right)}_{s}=\mathord{\mathsf{NF}}{\left(\mathord{\tau}{\left(M\right)}\right)}_{s}$, by Theorem 6. Since this holds for any $d\geq\mathord{\mathbf{d}}{\left(s\right)}+1$, we have just proved that ${\left(\mathord{\tau}{\left(\mathsf{NA}_{d}{\left(M\right)}\right)}_{s}\right)}_{d\in\mathbf{N}}$ converges to $\mathord{\mathsf{NF}}{\left(\mathord{\tau}{\left(M\right)}\right)}_{s}$, for the discrete topology.

In the case of pure $\lambda$-terms, by identifying [math] with the unsolvable Böhm tree $\bot$, it should be clear that the sequence ${\left(\mathsf{NA}_{d}{\left(M\right)}\right)}_{d\in\mathbf{N}}$ is nothing but the increasing sequence of finite approximants of $\mathord{\mathsf{BT}}{\left(M\right)}$: Theorem 9 is thus a proper generalization of Theorem 8.34 of which it provides a new proof.