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
10, to be proved in the next section.

######  Theorem 8.34 ([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 9, 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 9 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 9 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

$\displaystyle\mathsf{NA}_{d}{\left(\lambda x\,{S}\right)}$
$\displaystyle\mathrel{\mathord{:}\mathord{=}}\lambda
x\,{\mathsf{NA}_{d}{\left(S\right)}}$
$\displaystyle\mathsf{NA}_{d}{\left({\left(x\right)}\,{M_{1}\cdots
M_{n}}\right)}$
$\displaystyle\mathrel{\mathord{:}\mathord{=}}{\left(x\right)}\,{\mathsf{NA}_{d-1}{\left(M_{1}\right)}\cdots\mathsf{NA}_{d-1}{\left(M_{n}\right)}}$
$\displaystyle\mathsf{NA}_{d}{\left({\left(\lambda
x\,{S}\right)}\,{M_{0}\,M_{1}\cdots M_{n}}\right)}$
$\displaystyle\mathrel{\mathord{:}\mathord{=}}\mathsf{NA}_{d}{\left({\left(S{\left[M_{0}/x\right]}\right)}\,{M_{1}\cdots
M_{n}}\right)}$ $\displaystyle\mathsf{NA}_{d}{\left(a.M\right)}$
$\displaystyle\mathrel{\mathord{:}\mathord{=}}a.\mathsf{NA}_{d}{\left(M\right)}$
$\displaystyle\mathsf{NA}_{d}{\left(M+N\right)}$
$\displaystyle\mathrel{\mathord{:}\mathord{=}}\mathsf{NA}_{d}{\left(M\right)}+\mathsf{NA}_{d}{\left(N\right)}$

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 $0$ 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 10 is thus a proper
generalization of Theorem 9 of which it provides a new proof.

## References

  * [AD08] Pablo Arrighi and Gilles Dowek.  Linear-algebraic lambda-calculus: higher-order, encodings, and confluence.  In Andrei Voronkov, editor, Rewriting Techniques and Applications, 19th International Conference, RTA 2008, Hagenberg, Austria, July 15-17, 2008, Proceedings, volume 5117 of Lecture Notes in Computer Science, pages 17–31. Springer, 2008.
  * [Alb14] Michele Alberti.  On operational properties of quantitative extensions of $\lambda$-calculus.  PhD thesis, Aix Marseille Université ; Università di Bologna, December 2014.
  * [BEM07] Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto.  Not enough points is enough.  In Computer Science Logic, volume 4646 of Lecture Notes in Computer Science, pages 298–312. Springer Berlin, 2007.
  * [Bou93] Gérard Boudol.  The lambda-calculus with multiplicities (abstract).  In CONCUR ’93: Proceedings of the 4th International Conference on Concurrency Theory, pages 1–6, London, UK, 1993. Springer-Verlag.
  * [CA18] Jules Chouquet and Lionel Vaux Auclair.  An application of parallel cut elimination in unit-free multiplicative linear logic to the taylor expansion of proof nets.  In Dan R. Ghica and Achim Jung, editors, 27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4-7, 2018, Birmingham, UK, volume 119 of LIPIcs, pages 15:1–15:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018.
  * [Car11] Alberto Carraro.  Models and theories of pure and resource lambda calculas.  PhD thesis, 2011.  Thèse de doctorat dirigée par Salibra, Antonino et Bucciarelli, Antonio Informatique Paris 7 2011.
  * [CES10] Alberto Carraro, Thomas Ehrhard, and Antonino Salibra.  Exponentials with infinite multiplicities.  In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6247 of Lecture Notes in Computer Science, pages 170–184. Springer, 2010.
  * [dC08] Daniel de Carvalho.  Execution time of lambda-terms via denotational semantics and intersection types.  Technical report, 2008.  Rapport de recherche INRIA n° 6638.
  * [DC11] Alejandro Díaz-Caro.  Du typage vectoriel.  PhD thesis, Université de Grenoble, France, September 23, 2011.
  * [DE11] Vincent Danos and Thomas Ehrhard.  Probabilistic coherence spaces as a model of higher-order probabilistic computation.  Information and Computation, 2011.
  * [DLL19] Ugo Dal Lago and Thomas Leventis.  On the Taylor expansion of probabilistic $\lambda$-terms.  Submitted, 2019.
  * [DLMF] NIST Digital Library of Mathematical Functions.  http://dlmf.nist.gov/, Release 1.0.11 of 2016-06-08.  Online companion to [OLBC10].
  * [dLP95] Ugo de’ Liguoro and Adolfo Piperno.  Nondeterministic extensions of untyped $\lambda$-calculus.  Information and Computation, 149-177(122), 1995.
  * [Ehr05] Thomas Ehrhard.  Finiteness spaces.  Mathematical Structures in Computer Science, 15(4):615–646, 2005\.
  * [Ehr10] Thomas Ehrhard.  A finiteness structure on resource terms.  In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, United Kingdom, pages 402–410. IEEE Computer Society, 2010.
  * [Ehr16] Thomas Ehrhard.  An introduction to differential linear logic: proof-nets, models and antiderivatives.  CoRR, abs/1606.01642, 2016.
  * [ER03] Thomas Ehrhard and Laurent Regnier.  The differential lambda-calculus.  Theoretical Computer Science, 309:1–41, 2003.
  * [ER05] Thomas Ehrhard and Laurent Regnier.  Differential interaction nets.  Electr. Notes Theor. Comput. Sci., 123:35–74, 2005.
  * [ER06] Thomas Ehrhard and Laurent Regnier.  Böhm trees, Krivine’s machine and the Taylor expansion of $\lambda$-terms.  In Arnold Beckmann, Ulrich Berger, Benedikt Löwe, and John V. Tucker, editors, CiE, volume 3988 of Lecture Notes in Computer Science, pages 186–197. Springer, 2006.
  * [ER08] Thomas Ehrhard and Laurent Regnier.  Uniformity and the taylor expansion of ordinary lambda-terms.  Theor. Comput. Sci., 403(2-3):347–372, 2008.
  * [Gir86] Jean-Yves Girard.  The system F of variable types, fifteen years later.  Theor. Comput. Sci., 45(2):159–192, 1986.
  * [Gir87] Jean-Yves Girard.  Linear logic.  Theoretical Computer Science, 50:1–102, 1987.
  * [Gir88] Jean-Yves Girard.  Normal functors, power series and lambda-calculus.  Annals of Pure and Applied Logic, 37(2):129–177, 1988.
  * [Gol13] J.S. Golan.  Semirings and their Applications.  SpringerLink : Bücher. Springer Netherlands, 2013.
  * [Has96] Ryu Hasegawa.  The generating functions of lambda terms.  In Douglas S. Bridges, Cristian S. Calude, Jeremy Gibbons, Steve Reeves, and Ian H. Witten, editors, First Conference of the Centre for Discrete Mathematics and Theoretical Computer Science, DMTCS 1996, Auckland, New Zealand, December, 9-13, 1996, pages 253–263. Springer-Verlag, Singapore, 1996.
  * [Joy86] André Joyal.  Foncteurs analytiques et espèces de structures, pages 126–159.  Springer Berlin Heidelberg, Berlin, Heidelberg, 1986.
  * [KKSdV97] J.R. Kennaway, J.W. Klop, M.R. Sleep, and F.J. de Vries.  Infinitary lambda calculus.  Theoretical Computer Science, 175(1):93 – 125, 1997.
  * [Kri90] Jean-Louis Krivine.  Lambda-calcul, types et modèles.  Masson, Paris, 1990.
  * [Lai16] J. Laird.  Fixed points in quantitative semantics.  In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, LICS ’16, New York, NY, USA, July 5-8, 2016, pages 347–356. ACM, 2016.
  * [Lev16] Thomas Leventis.  Probabilistic $\lambda$-theories.  PhD thesis, Aix-Marseille Université, December 2016.
  * [LMMP13] Jim Laird, Giulio Manzonetto, Guy McCusker, and Michele Pagani.  Weighted relational models of typed lambda-calculi.  In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages 301–310. IEEE Computer Society, 2013.
  * [OLBC10] F. W. J. Olver, D. W. Lozier, R. F. Boisvert, and C. W. Clark, editors.  NIST Handbook of Mathematical Functions.  Cambridge University Press, New York, NY, 2010.  Print companion to [DLMF].
  * [PTV16] Michele Pagani, Christine Tasson, and Lionel Vaux.  Strong normalizability as a finiteness structure via the taylor expansion of $\lambda$-terms.  In Bart Jacobs and Christof Löding, editors, Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9634 of Lecture Notes in Computer Science, pages 408–423. Springer, 2016.
  * [TAO17] Takeshi Tsukada, Kazuyuki Asada, and C.-H. Luke Ong.  Generalised species of rigid resource terms.  In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1–12. IEEE Computer Society, 2017.
  * [Tas09] Christine Tasson.  Sémantiques et syntaxes vectorielles de la logique linéaire.  PhD thesis, Université Paris Diderot – Paris 7, December 2009.
  * [TdF03] Lorenzo Tortora de Falco.  Obsessional experiments for linear logic proof-nets.  Mathematical Structures in Computer Science, 13(6):799–855, 2003\.
  * [TV16] Christine Tasson and Lionel Vaux.  Transport of finiteness structures and applications.  Mathematical Structures in Computer Science, page 1–36, 2016.
  * [Vau07] Lionel Vaux.  On linear combinations of $\lambda$-terms.  In Franz Baader, editor, RTA, volume 4533 of Lecture Notes in Computer Science, pages 374–388. Springer, 2007.
  * [Vau09] Lionel Vaux.  The algebraic lambda calculus.  Mathematical Structures in Computer Science, 19(5):1029–1059, 2009\.
  * [Vau17] Lionel Vaux.  Taylor expansion, lambda-reduction and normalization.  In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic, CSL 2017, August 20-24, 2017, Stockholm, Sweden, volume 82 of LIPIcs, pages 39:1–39:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017.