On the Taylor Expansion of Probabilistic $\lambda$-Terms (Long Version)

TL;DR

This paper extends the Taylor expansion framework to probabilistic lambda calculus, establishing its adequacy as a semantic tool and linking it to probabilistic B"ohm trees, thus advancing the understanding of probabilistic computation semantics.

Contribution

It generalizes the Taylor expansion to probabilistic lambda-terms and proves its adequacy and correspondence with probabilistic B"ohm trees, providing a new semantic perspective.

Findings

Taylor expansion is adequate for probabilistic lambda-terms

Established a correspondence with probabilistic B"ohm trees

Extended resource calculus to probabilistic settings

Abstract

We generalise Ehrhard and Regnier's Taylor expansion from pure to probabilistic $\lambda$-terms through notions of probabilistic resource terms and explicit Taylor expansion. We prove that the Taylor expansion is adequate when seen as a way to give semantics to probabilistic $\lambda$-terms, and that there is a precise correspondence with probabilistic B\"ohm trees, as introduced by the second author.

Equations

$$s,t\in {\Delta }^{\oplus }:=x\mid \lambda x.s\mid ⟨s⟩\overline{t}\mid s{\oplus }_p\cdot \mid \cdot {\oplus }_{p}s\overline{s},\overline{t}\in !{\Delta }^{\oplus }:=[s_1,\dots ,s_n]$$

$${\delta }_x\sigma \cdot [t_1,\dots ,t_n]=\{\begin{array}{l}0\text{if σ does not have exactly n free occurences of x}\\ {\sum }_{\rho \in {\mathfrak{S}}_n}\sigma [t_{\rho (1)}/x_1,\dots ,t_{\rho (n)}/x_n]\in {\mathbb{R}}_{\ge 0}^{((!){\Delta }^{\oplus })}\text{otherwise}\end{array}$$

$$\begin{array}{rlrlrl}{\delta }_{x}x\cdot [t]& =t& & & {\delta }_x(\lambda y.s)\cdot \overline{t}& =\lambda y.{\delta }_{x}s\cdot \overline{t}\text{if}y\ne x\\ {\delta }_{x}y\cdot []& =y\text{if}y\ne x& & & {\delta }_x(s{\oplus }_p\cdot )\cdot \overline{t}& ={\delta }_{x}s\cdot \overline{t}{\oplus }_p\cdot \\ {\delta }_{x}z\cdot \overline{t}& =0\text{in any other case}& & & {\delta }_x(\cdot {\oplus }_{p}s)\cdot \overline{t}& =\cdot {\oplus }_p{\delta }_{x}s\cdot \overline{t}\end{array}$$

$$\begin{array}{rl}{\delta }_x(⟨s⟩\overline{u})\cdot [t_1,\dots ,t_n]& =\sum _{I\uplus J=\{1,\dots ,n\}}⟨{\delta }_{x}s\cdot [t_i{]}_{i\in I}⟩{\delta }_x\overline{u}\cdot [t_j{]}_{j\in J}\\ {\delta }_x[u_1,\dots ,u_m]\cdot [t_1,\dots ,t_n]& =\sum _{{⨄}_{k=1}^m{I}_k=\{1,\dots ,n\}}[{\delta }_x{u}_1\cdot [t_i{]}_{i\in I_1},\dots ,{\delta }_x{u}_m\cdot [t_i{]}_{i\in I_m}]\end{array}$$

$$⟨\lambda x.s⟩\overline{t}$$

$$\lambda x.(s{\oplus }_p\cdot )$$

$$⟨s{\oplus }_p\cdot ⟩\overline{t}$$

$$\mathrm{L}(s{\oplus }_p\cdot )$$

$$\mathrm{L}(\cdot {\oplus }_{p}s)$$

$$\mathrm{L}(\lambda \vec{x}.⟨y⟩{\overline{u}}_1\dots {\overline{u}}_m)$$

$$\mathrm{L}(\lambda \vec{x}.⟨\lambda y.s⟩\overline{t}{\overline{u}}_1\dots {\overline{u}}_m)$$

$$\mathrm{L}(\lambda \vec{x}.⟨s{\oplus }_p\cdot ⟩{\overline{u}}_1\dots {\overline{u}}_m)$$

$$\mathrm{L}(\lambda \vec{x}.⟨\cdot {\oplus }_{p}s⟩{\overline{u}}_1\dots {\overline{u}}_m)$$

$$\mathrm{L}([s_1,\dots ,s_n])$$

$$x\text{coh}x$$

$$s\text{coh}{s}^{\prime }$$

$$\mathrm{m}(x)$$

$$\mathrm{m}(\lambda x.s)$$

$${\Sigma }_p$$

$$\mathrm{Iso}(\phi ,p)$$

$$\mathrm{Iso}(p,\Phi ,q)$$

$$\mathrm{Iso}(\phi ,p,\Phi ,q)$$

$$M,N\in {\Lambda }^{+}:=x\mid \lambda x.M\mid MN\mid M{\oplus }_{p}N$$

$$x^{\ast \oplus }$$

$$(\lambda x.M{)}^{\ast \oplus }$$

$${\mathcal{T}}^r(x)$$

$${\mathcal{T}}^r(\lambda x.M)$$

$${\mathcal{T}}^r(MN)$$

$${\mathcal{T}}^r(M{+}_{p}N)$$

$$M^{\ast \oplus }=\sum _{s\in {\mathcal{T}}^r(M)}\frac{1}{\mathrm{m}(s)}s\in {\mathbb{R}}_{\ge 0}^{{\Delta }^{+}}.$$

$$x^{\ast \oplus }=\sum _{s\in {\mathcal{T}}^r(x)}\frac{1}{\mathrm{m}(s)}s=\frac{1}{\mathrm{m}(x)}x=x.$$

$$(\lambda x.N{)}^{\ast \oplus }=\sum _{s\in {\mathcal{T}}^r(N)}\frac{1}{\mathrm{m}(\lambda x.s)}(\lambda x.s)=\lambda x.\left(\sum _{s\in {\mathcal{T}}^r(N)}\frac{1}{\mathrm{m}(s)}s\right)=\lambda x.N^{\ast \oplus }$$

$$|\{(t_1,\dots ,t_n)|[t_1,\dots ,t_n]=\overline{t}\}|=\frac{n!}{{\prod }_u\overline{t}(u)!}$$

$$(NL{)}^{\ast \oplus }$$

$$=\sum _{s\in {\mathcal{T}}^r(N)}\sum _{n\in \mathbb{N}}\sum _{\overline{t}\in {\mathrm{M}}_{\mathrm{fin}}^n({\mathcal{T}}^r(L))}\frac{1}{\mathrm{m}(⟨s⟩\overline{t})}⟨s⟩\overline{t}$$

$$=\sum _{s\in {\mathcal{T}}^r(N)}\sum _{n\in \mathbb{N}}\sum _{\overline{t}\in {\mathrm{M}}_{\mathrm{fin}}^n({\mathcal{T}}^r(L))}\frac{1}{\mathrm{m}(s)\mathrm{m}(\overline{t})}⟨s⟩\overline{t}$$

$$=\sum _{s\in {\mathcal{T}}^r(N)}\sum _{n\in \mathbb{N}}\sum _{t_1,\dots ,t_n\in {\mathcal{T}}^r(L)}\frac{{\prod }_u[t_1,\dots ,t_n](u)}{\mathrm{m}(s)\cdot \mathrm{m}([t_1,\dots ,t_n])\cdot n!}⟨s⟩[t_1,\dots ,t_n]$$

$$=\sum _{s\in {\mathcal{T}}^r(N)}\sum _{n\in \mathbb{N}}\sum _{t_1,\dots ,t_n\in {\mathcal{T}}^r(L)}\frac{1}{\mathrm{m}(s)\cdot (\prod \mathrm{m}(t_i))\cdot n!}⟨s⟩[t_1,\dots ,t_n]$$

$$=\sum _{n\in \mathbb{N}}\frac{1}{n!}\sum _{s\in {\mathcal{T}}^r(N)}\sum _{t_1,\dots ,t_n\in {\mathcal{T}}^r(L)}\frac{1}{\mathrm{m}(s)\cdot (\prod \mathrm{m}(t_i))}⟨s⟩[t_1,\dots ,t_n]$$

$$=\sum _{n\in \mathbb{N}}\frac{1}{n!}⟨\sum _{s\in {\mathcal{T}}^r(N)}\frac{1}{\mathrm{m}(s)}s⟩{\left(\sum _{t\in {\mathcal{T}}^r(L)}\frac{1}{\mathrm{m}(t)}t\right)}^n$$

$$(N{+}_{p}L{)}^{\ast \oplus }$$

$$=\sum _{s\in {\mathcal{T}}^r(N)}\frac{1}{\mathrm{m}(s)}(s{\oplus }_p\cdot )+\sum _{s\in {\mathcal{T}}^r(L)}\frac{1}{\mathrm{m}(s)}(\cdot {\oplus }_{p}s)$$

Full text

1 Introduction

Linear logic is a proof-theoretical framework which, since its inception [10], has been built around an analogy between on the one hand linearity in the sense of linear algebra, and on the other hand the absence of copying and erasing in cut elimination and higher-order rewriting. This analogy has been pushed forward by Ehrhard and Regnier, who introduced a series of logical and computational frameworks accounting, along the same analogy, for concepts like that of a differential, or the very related one of an approximation. We are implicitly referring to differential $\lambda$-calculus [6], to differential linear logic [8], and to the Taylor expansion of ordinary $\lambda$-terms [9]. The latter has given rise to an extremely interesting research line, with many deep contributions in the last ten years. Not only the Taylor expansion of pure $\lambda$-terms has been shown to be endowed with a well-behaved notion of reduction, but the Böhm tree and Taylor expansion operators are now known to commute [7]. This easily implies that the equational theory (on pure $\lambda$-terms) induced by the Taylor expansion coincides with the one induced by Böhm trees.

The Taylor expansion operator is essentially quantitative, in that its codomain is not merely the set of resource $\lambda$-terms [3, 6], a term syntax for promotion-free differential proofs, but the set of linear combinations of those terms, with positive real number coefficients. When enlarging the domain of the operator to account for a more quantitative language, one is naturally lead to consider algebraic $\lambda$-calculi, to which giving a clean computational meaning has been proved hard so far [18].

But what about probabilistic $\lambda$-calculi [11], which have received quite some attention recently (see, e.g. [5, 2, 16]) due to their applicability to randomised computation and bayesian programming? Can the Taylor expansion naturally be generalised to those calculi? This is an interesting question, to which we give the first definite positive answer in this paper. In particular, we show that the Taylor expansion of probabilistic $\lambda$-terms is a conservative extension of the well-known one on ordinary $\lambda$-terms. In particular, the target can be taken, as usual, as a linear combination of ordinary resource $\lambda$-terms, i.e., the same kind of structure which Ehrhard and Regnier considered in their work on the Taylor expansion of pure $\lambda$-terms. We moreover show that the Taylor expansion, as extended to probabilistic $\lambda$-terms, continues to enjoy the nice properties it has in the deterministic realm. In particular, it is adequate as a way to give semantics to probabilistic $\lambda$-terms, and the equational theory on probabilistic $\lambda$-terms induced by Taylor expansion coincides with the one induced by a probabilistic variation on Böhm trees [1]. The latter, noticeably, has been proved to capture observational equivalence, one quotiented modulo $\eta$-equivalence [1].

Are we the first ones to embark on the challenge of generalising Taylor’s expansion to probabilistic $\lambda$-calculi, and in general to effectful calculi? Actually, some steps in this direction have recently been taken. First of all, we need to mention the line of works originated by Tsukada and Ong’s paper on rigid resource terms [14]. This has been claimed from the very beginning to be a way to model effects in the resource $\lambda$-calculus, but it has also been applied to, among others, probabilistic effects, giving rise to quantitative denotational models [15]. The obtained models are based on species, and are proved to be adequate. The construction being generic, there is no aim at providing a precise comparison between the discriminating power of the obtained theory and, say, observational equivalence: the choice of the underlying effect can in principle have a huge impact on it.

One should also mention Vaux’s work on the algebraic $\lambda$-calculus [18], where one can build arbitrary linear combinations of terms. He showed a correspondence between Taylor expansion and Böhm trees, but only for terms whose Böhm trees approximants at finite depths are computable in a finite number of steps. This includes all ordinary $\lambda$-terms but not all probabilistic ones. More recently Olimpieri and Vaux have studied a Taylor expansion for a non-deterministic $\lambda$-calculus [19] corresponding to our notion of explicit Taylor expansion (Section 3).

In the rest of this section, probabilistic Taylor expansion will be informally introduced by way of an example, so as to make the main concepts comprehensible to the non-specialist. In sections 2 and 3, we introduce a new form of resource term, and a notion of explicit Taylor expansion from probabilistic $\lambda$-terms. These constructions have an interest in themselves (again, see [19]) but in this paper they are just an intermediate step towards proving our main results. Definitionally, the crux of the paper is Section 4, in which the Taylor expansion of a probabilistic $\lambda$-term is made to produce ordinary resource terms. The relationship between the introduced theory and the one induced by Probabilistic Böhm trees [13] is investigated in Section 5 and Section 7.

The Probabilistic Taylor Expansion, Informally

In this section, we introduce the main ingredients of the probabilistic Taylor expansion by way of an extremely simple, although instructive, example. Let us consider the probabilistic $\lambda$-term $M=\delta(I\oplus\Omega)$, where $\oplus$ is an operator for binary, fair, probabilistic choice, $\delta=\lambda x.xx$, $I=\lambda.x.x$ and $\Omega=\delta\delta$ is a purely diverging, term. As such, $M$ is a term of a minimal, untyped, probabilistic $\lambda$-calculus. Evaluation of $M$, if performed leftmost-outermost is as in Figure 1. In particular, the probability of convergence for $M$ is $\frac{1}{4}$.

Please observe that two copies of the argument $I\oplus\Omega$ are produced, and that the “rightmost” one is evaluated only when the “leftmost” one converges, i.e. when the probabilistic choice $I\oplus\Omega$ produces $I$ as a result.

The main idea behind building the Taylor expansion of any $\lambda$-term $M$ is to describe the dynamics of $M$ by way of linear approximations of $M$. In the realm of the $\lambda$-calculus, a linear approximation has traditionally been taken as a resource $\lambda$-term, which can be seen as a pure $\lambda$-term in which applications have the form $\langle s\rangle\ \overline{t}$, where $s$ is a term and $\overline{t}$ is a multiset of terms, and in which the result of firing the redex $\langle\lambda x.s\rangle\ \overline{t}$ is the linear combination of all the terms obtained by allocating the resources in $\overline{t}$ to the occurrences of $x$ in $s$. For instance, one such element in the Taylor expansion of $\Delta$ is $\lambda x.(\langle x\rangle\ [x])$, where the occurrence of $x$ in head position is provided with only one copy of its argument. If applied to the multiset $[y,z]$, this term would reduce into $\langle y\rangle\ [z]+\langle z\rangle\ [y]$. Similarly, an element in the Taylor expansion of $\Delta\ I$ would be $\langle\lambda x.\langle x\rangle\ [x]\rangle\ [I^{2}]$, which reduces into $2.\langle I\rangle\ [I]$. Another element of the same Taylor expansion is $\langle\lambda x.\langle x\rangle\ [x]\rangle\ [I^{3}]$, but this one reduces into [math]: there is no way to use its resources linearly, i.e., using them without copying and erasing. The actual Taylor expansion of a term is built by translating any application $M\ N$ into an infinite sum $(M\ N)^{*}=\sum_{n\in\mathbb{N}}\frac{1}{n!}.\langle M^{*}\rangle\ [(N^{*})^{n}]$. For instance, the Taylor expansion of $\Delta\ I$ is $\sum_{m,n\in\mathbb{N}}\frac{1}{m!n!}.\langle\lambda x.\langle x\rangle\ [x^{m}]\rangle\ [I^{n}]$. Remark that any summand properly reduces only when $n=m+1$, in which case it reduces to $n!.\langle I\rangle\ [I^{m}]$. In turn $\langle I\rangle\ [I^{m}]$ reduces properly only when $m=1$, and the result is $I$. All the other terms reduce to [math]. In the end the Taylor expansion of $\Delta\ I$ normalises to $\frac{2!}{1!2!}.I=I$.

Extending the Taylor expansion to probabilistic terms seems straightforward, a natural candidate for the Taylor expansion of $M\oplus N$ being just $\frac{1}{2}.M^{*}+\frac{1}{2}.N^{*}$. When computing the Taylor expansion of $M$ we will find expressions such as $\langle\lambda x.\langle x\rangle\ [x]\rangle\ [(\frac{1}{2}.I+\frac{1}{2}.\Omega^{*})^{2}]$, i.e. $\frac{1}{4}.\langle\lambda x.\langle x\rangle\ [x]\rangle\ [I^{2}]+\frac{1}{4}.\langle\lambda x.\langle x\rangle\ [x]\rangle\ [\Omega^{2}]+\frac{1}{2}.\langle\lambda x.\langle x\rangle\ [x]\rangle\ [I,\Omega]$. For non-trivial reasons, the Taylor expansion of any diverging term normalises to [math], so just like in our previous example, the only element in $M^{*}$ which does not reduce to [math] is $\langle\lambda x.\langle x\rangle\ [x]\rangle\ [I^{2}]$. The difference is that this time it appears with a coefficient $\frac{1}{1!2!}\frac{1}{4}$, so $M^{*}$ normalises to $\frac{1}{4}.I$. Please notice how this is precisely the “normal form” of the original term $M$. This is a general phenomenon, whose deep consequences will be investigated in the rest of this paper, and in particular in Section 5.

Notations

We write $\mathbb{N}$ for the set of natural numbers and $\mathbb{R}_{\geq 0}$ for the set of nonnegative real numbers. Given a set $A$, we write $\mathbb{R}_{\geq 0}^{A}$ for the set of families of positive real numbers indexed by elements in $A$. We write such families as linear combinations: an element $S\in\mathbb{R}_{\geq 0}^{A}$ is a sum $S=\sum_{a\in A}S_{a}.a$, with $S_{a}\in\mathbb{R}_{\geq 0}$. The support of a family $S\in\mathbb{R}_{\geq 0}^{A}$ is $\mathrm{supp}(S)=\{a\in A\mid S_{a}>0\}$. We write $\mathbb{R}_{\geq 0}^{(A)}$ for those families $S\in\mathbb{R}_{\geq 0}^{A}$ such that $\mathrm{supp}(S)$ is finite. Given $a\in A$ we often write $a$ for $1.a\in\mathbb{R}_{\geq 0}^{A}$ unless we want to emphasise the difference between the two expressions. We also define finite multisets over $A$ as functions $m:A\rightarrow\mathbb{N}$ such that $m(a)\neq 0$ for finitely many $a\in A$. We use the notation $[a_{1},\dots,a_{n}]$ to describe the multiset $m$ such that $m(a)$ is the number of indices $i\leq n$ such that $a_{i}=a$.

2 Probabilistic Resource $\lambda$-Calculus

In this section, we describe the theory of resource terms with explicit choices, for the purpose of extending many of the properties of resource terms to the probabilistic case. All this has an interest in itself, but here this is mainly useful as a way to render certain proofs about the Taylor Expansion easier (see Section 3 for more details). For this reason we try to give the reader a clear understanding of this calculus and of why these definitions and properties are useful, without focusing on the actual proofs. These are straightforward generalisations of those for deterministic resource terms [9] and can be found in an extended version of this paper [4]. The same results have recently been given for a non-deterministic calculus [19] by Olimpieri and Vaux.

2.1 The Basics

Definition 2.1**.**

The sets of probabilistic simple resource terms $\Delta^{\oplus}$ and of probabilistic simple resource poly-terms $!\Delta^{\oplus}$ over a set of variables $\mathcal{V}$ are defined by mutual induction as follows:

[TABLE]

where $p$ ranges over $[0,1]$. We call finite probabilistic resource terms the finite linear combinations of resource terms in $\mathbb{R}_{\geq 0}^{(\Delta^{\oplus})}$, and finite probabilistic resource poly-terms the finite linear combinations of resource poly-terms in $\mathbb{R}_{\geq 0}^{(!\Delta^{\oplus})}$. We extend the constructors of simple (poly-)terms to (poly-)terms by linearity, e.g., if $S\in\mathbb{R}_{\geq 0}^{(\Delta^{\oplus})}$ then $\lambda x.S$ is defined as the poly-term such that $(\lambda x.S)_{\lambda x.s}=S_{s}$ and $(\lambda x.S)_{t}=0$ if $t$ is not an abstraction.

Some consecutive abstractions $\lambda x_{1}.\dots\lambda x_{n}.s$ will be indicated as $\lambda x_{1}\dots x_{n}.s$, or even as $\lambda\vec{x}.s$. Similarly, to describe many successive applications $\langle\langle\langle M\rangle\ N_{1}\rangle\ \dots\rangle\ N_{k}$, we use a single pair of brackets and we write $\langle M\rangle\ N_{1}\ \dots\ N_{k}$. We write $(!)\Delta^{\oplus}$ for $\Delta^{\oplus}\cup!\Delta^{\oplus}$, which is ranged over by metavariables like $\sigma,\tau$. Note that intuitively $(!)\Delta^{\oplus}$ should stand for either $\Delta^{\oplus}$ or $!\Delta^{\oplus}$, not their union. For instance we will prove some properties for finite linear combinations in $\mathbb{R}_{\geq 0}^{((!)\Delta^{\oplus})}$, but the only relevant linear combinations are the actual (poly-)terms in $\mathbb{R}_{\geq 0}^{(\Delta^{\oplus})}$ or $\mathbb{R}_{\geq 0}^{(!\Delta^{\oplus})}$. Yet this distinction is technically irrelevant, and all our results hold if we define $(!)\Delta^{\oplus}$ as a union.

The reason why linear combinations over such elements are dubbed terms will be clear once we describe the operational semantics of the resource calculus. The main point of the resource $\lambda$-calculus is to allow functions to use their argument arbitrarily many times and yet remain entirely linear, which is achieved by taking multisets as arguments: if a function uses its argument $n$ times then it needs to receive $n$ resources as argument and use each of them linearly. This idea has two consequences. First, an application can fail if a function is not given exactly as many arguments as it needs, as it would need either to duplicate or to discard some of them. Second, the result of a valid application is often not unique: a function can choose how to allocate the different resources to the different calls to its argument, and different choices may lead to different results. Both these features are treated using linear combinations: a failed application results in [math] (i.e. the trivial linear combination) and a successful one yields the sum of all its possible outcomes.

Definition 2.2**.**

We define the substitution of $\overline{t}\in!\Delta^{\oplus}$ for $x\in\mathcal{V}$ in $\sigma\in(!)\Delta^{\oplus}$ by:

[TABLE]

where $x_{1},\dots,x_{n}$ are the free occurrences of $x$ in $\sigma$ and $\mathfrak{S}_{n}$ is the set of permutations over $\{1,\dots,n\}$. Alternatively, we could define $\delta_{x}s\cdot\overline{t}$ by induction on $s$, as follows

[TABLE]

where $\uplus$ is the disjoint union of sets.

Example 2.1*.*

A basic example is $\delta_{x}(\langle x\rangle\ [x])\cdot[y,z]=\langle y\rangle\ [z]+\langle z\rangle\ [y]$: there are two occurrences of $x$ in $\langle x\rangle\ [x]$, so there are two ways to substitute $[y,z]$ for them. Remark that we also have $\delta_{x}[x,x]\cdot[y,z]=[y,z]+[z,y]=2.[y,z]$: the two occurrences of $x$ are not as clearly distinguished as in the first example but they still count as different occurrences. Similarly $\delta_{x}(\langle x\rangle\ [x])\cdot[y,y]=2.\langle y\rangle\ [y]$ and $\delta_{x}[x,x]\cdot[y,y]=2.[y,y]$: there are two distinct occurrences of $y$, so there are two ways to allocate them. As another example, please consider $\delta_{x}(\lambda x.x)\cdot[y]=\delta_{x}(\langle x\rangle\ [x])\cdot[y]=0$: the substitution fails if the number of resources does not match the number of free occurrences of the substituted variable.

The operational semantics of the deterministic resource $\lambda$-calculus [9] is usually given as a single rule of $\beta$-reduction. In the probabilistic setting, we also need rules to make choices commute with head contexts.

Definition 2.3**.**

The reductions $\rightarrow_{\beta}$ and $\rightarrow_{\oplus}$ are defined from $(!)\Delta^{\oplus}$ to $\mathbb{R}_{\geq 0}^{((!)\Delta^{\oplus})}$ by:

[TABLE]

extended under arbitrary contexts. We simply write $\rightarrow$ for $\rightarrow_{\beta}\cup\rightarrow_{\oplus}$. Reduction can be extended to finite terms in the following way: if $S\in\mathbb{R}_{\geq 0}^{((!)\Delta^{\oplus})}$, $S_{\sigma}>0$ and $\sigma\rightarrow T$ then $S\rightarrow S-S_{\sigma}.\sigma+S_{\sigma}T$.

As the resource $\lambda$-calculus does not allow any duplication, and $\beta$-reduction erases some constructors, it naturally decreases the size of the involved simple terms. Consequently, $\beta$-reduction is strongly normalising. This result can be extended to the whole reduction $\rightarrow$, which is also confluent.

More specifically we define the size $||\sigma||$ of a simple (poly-)term in a natural way. To any $S\in\mathbb{R}_{\geq 0}^{((!)\Delta^{\oplus})}$ we associate two sizes: $||S||=1+\max_{\sigma\in\mathrm{supp}(S)}||\sigma||$ and $||S||^{\dagger}=[||\sigma||]_{\sigma\in\mathrm{supp}(S)}\in\mathrm{M}_{\mathrm{fin}}(\mathbb{N})$. We order $\mathrm{M}_{\mathrm{fin}}(\mathbb{N})$ with a reverse lexicographical order: $m\prec n$ iff there exists $a\in\mathbb{N}$ such that $m(a)<n(a)$ and $m(b)=n(b)$ for all $b>a$.

Proposition 2.1**.**

The reduction $\rightarrow$ is confluent and strongly normalising on $\mathbb{R}_{\geq 0}^{((!)\Delta^{\oplus})}$. Given $S\in\mathbb{R}_{\geq 0}^{((!)\Delta^{\oplus})}$ we write $\mathrm{nf}(S)$ for its unique normal form for $\rightarrow$, and given $\sigma\in(!)\Delta^{\oplus}$ we write $\mathrm{nf}(\sigma)$ for $\mathrm{nf}(1.\sigma)$.

Proof.

Proving weak confluence is straightforward. Strong normalisation is proven in two steps. First using an appropriate weight on terms describing how deep choices are we can prove that $\rightarrow_{\oplus}$ is strongly normalising. Second one can observe that $\rightarrow_{\oplus}$ preserves size, and that if $\sigma\rightarrow_{\beta}T$ and $\tau\in\mathrm{supp}(T)$ then $||\tau||<||\sigma||$, hence if $S\rightarrow_{\beta}T$ then $||T||^{\dagger}\prec||S||^{\dagger}$. The confluence is given by Newman’s Lemma. ∎

2.2 Complete Left Reduction

This reduction is not convenient to study (poly-)terms with particular properties such as uniformity or regularity, which we will define later. For instance given a simple poly-term $\overline{s}=[s,\dots,s]$ we can reduce independently the different occurrences of $s$, so not every reduct of $\overline{s}$ is of the form $[T,\dots,T]$ with $s\twoheadrightarrow T$. Similarly given a term $S$ we can reduce independently the elements of its support, possibly losing some common properties shared by these elements. For that reason (as well as the issue of infinite terms discussed in the rest of this section) we are mostly interested in normalisation rather than reduction. To study this normalisation we still need some small-step operational semantics, but it will be more convenient to consider the complete left reduction defined as follows.

Definition 2.4**.**

We define the complete left reduct $\mathrm{L}(\sigma)\in\mathbb{R}_{\geq 0}^{((!)\Delta^{\oplus})}$ of a simple (poly-)term $\sigma$ by induction:

[TABLE]

We extend this definition to terms: $\mathrm{L}(S)=\sum_{\sigma\in(!)\Delta^{\oplus}}S_{\sigma}\mathrm{L}(\sigma)$.

Proposition 2.2**.**

For all $S\in\mathbb{R}_{\geq 0}^{((!)\Delta^{\oplus})}$, $S\twoheadrightarrow\mathrm{L}(S)$.

Proposition 2.3**.**

For all $S\in\mathbb{R}_{\geq 0}^{((!)\Delta^{\oplus})}$ there is $k\in\mathbb{N}$ such that $\mathrm{nf}(S)=\mathrm{L}^{k}(S)$.

Proof.

The reduction $\rightarrow$ being strongly normalising we reason by induction on the bound on the length of the reductions of $S$. We have either $\mathrm{L}(S)=S$ and $S$ is already in normal form or $S$ reduces into $\mathrm{L}(S)$ in a least one step and we conclude by induction hypothesis. ∎

2.3 Infinite Terms

So far we only worked with finite terms but to fully express the operational behaviour of a $\lambda$-term in the resource $\lambda$-calculus, which is the purpose of the Taylor expansion, we need infinite ones. We can extend the constructors of the calculus to $\mathbb{R}_{\geq 0}^{(!)\Delta^{\oplus}}$ by linearity and generalise the reduction relation $\rightarrow$, but Proposition 2.1 fails. Indeed let $I_{0}=I=\lambda x.x$ and $I_{n+1}=\langle I_{n}\rangle\ [I]$. For $n\in\mathbb{N}$, let $S=\sum_{n\in\mathbb{N}}I_{n}$. Then, for all $n\in\mathbb{N}$ the term $I_{n}$ normalises in $n$ steps and $S$ does not normalise in a finite number of reduction steps. A simple solution to this problem is to define the “normal form” of an infinite term by normalising each of its components: we can set $\mathrm{nf}(S)=\sum_{\sigma\in(!)\Delta^{\oplus}}S_{\sigma}\mathrm{nf}(\sigma)$. But then another problem arises. In our previous example, we have $\mathrm{nf}(I_{n})=I$ for all $n\in\mathbb{N}$, thus we would have $\mathrm{nf}(S)=\sum_{n\in\mathbb{N}}I$, which is not an element of $\mathbb{R}_{\geq 0}^{(!)\Delta^{\oplus}}$ as the coefficient of $I$ is infinite. Still we can use this pointwise normalisation if we consider terms with a particular property, called uniformity.

Definition 2.5**.**

The coherence relation $\coh$ on $(!)\Delta^{\oplus}$ is defined by:

[TABLE]

[TABLE]

For $S,S^{\prime}\in(!)\Delta^{\oplus}$ we write $S\coh S^{\prime}$ when for all $\sigma,\sigma^{\prime}\in\mathrm{supp}(S)\cup\mathrm{supp}(S^{\prime})$, $\sigma\coh\sigma^{\prime}$. A simple (poly-)term $\sigma\in(!)\Delta^{\oplus}$ is called uniform if $\sigma\coh\sigma$, and a term $S\in\mathbb{R}_{\geq 0}^{(!)\Delta^{\oplus}}$ is called uniform if $S\coh S$.

Remark 2.1*.*

In the rule for $s\oplus_{p}\cdot\coh\cdot\oplus_{p}t$ we require $s\coh s$ and $t\coh t$ to ensure that whenever $\sigma\coh\tau$, the simple (poly-)terms $\sigma$ and $\tau$ are necessarily uniform. This is not crucial, as we will only consider uniform (poly-)terms, whose support contains only uniform simple (poly-)terms by definition, but this simplifies inductive reasoning.

What makes coherence and uniformity interesting is that if two coherent terms $S$ and $S^{\prime}$ have disjoint supports, then all of their reducts, and in particular their normal forms, have disjoint supports. Then any element in the support of $\mathrm{nf}(S+S^{\prime})$ comes either from $\mathrm{nf}(S)$ or from $\mathrm{nf}(S^{\prime})$, but it cannot come from both.

Lemma 2.4**.**

If $\sigma\coh\sigma^{\prime}$ and $\overline{u}\coh\overline{u^{\prime}}$ then $\delta_{x}\sigma\cdot\overline{u}\coh\delta_{x}\sigma^{\prime}\cdot\overline{u^{\prime}}$. Besides if $\mathrm{supp}(\delta_{x}\sigma\cdot\overline{u})\cap\mathrm{supp}(\delta_{x}\sigma^{\prime}\cdot\overline{u^{\prime}})\neq\emptyset$ then $\sigma=\sigma^{\prime}$ and $\overline{u}=\overline{u^{\prime}}$.

Proof.

By induction on $\sigma\coh\sigma^{\prime}$:

• •

If $x\coh x$ then for $\mathrm{supp}(\delta_{x}x\cdot\overline{u})$ and $\mathrm{supp}(\delta_{x}x\cdot\overline{u^{\prime}})$ to be both nonempty we need to have $\overline{u}=[v]$ and $\overline{u^{\prime}}=[v^{\prime}]$ for some $v,v^{\prime}\in\Delta^{+}$, and in this case $\delta_{x}x\cdot\overline{u}=v$ and $\delta_{x}x\cdot\overline{u^{\prime}}=v^{\prime}$. The hypothesis $\overline{u}\coh\overline{u^{\prime}}$ implies $v\coh v^{\prime}$, and if $v=v^{\prime}$ then $\overline{u}=\overline{u^{\prime}}$.

• •

If $y\coh y$ with $y\neq x$ then either one of the substitutions is [math] or we have $u=u^{\prime}=[\ ]$.

• •

If $\lambda x.s\coh\lambda x.s^{\prime}$, $s\oplus_{p}\cdot\coh s^{\prime}\oplus_{p}\cdot$ or $\cdot\oplus_{p}s\coh\cdot\oplus_{p}s^{\prime}$, with in each case $s\coh s^{\prime}$, then the result is immediate by induction hypothesis.

• •

If $s\oplus_{p}\cdot\coh\cdot\oplus_{p}t$ then we use the induction hypothesis on $s\coh s$ and $u\coh u$ (given by Proposition LABEL:prop:coh_ref) to prove that for $v\in\mathrm{supp}(\delta_{x}s\cdot\overline{u})$ we have $v\coh v$, and similarly for $w\in\mathrm{supp}(\delta_{x}\overline{t}\cdot\overline{u^{\prime}})$, and the result follows. Notice that we will never have $v\oplus_{p}\cdot=\cdot\oplus_{p}w$.

• •

If $\langle s\rangle\ \overline{t}\coh\langle s^{\prime}\rangle\ \overline{t^{\prime}}$ then $\mathrm{supp}(\delta_{x}\langle s\rangle\ \overline{t}\cdot\overline{u})=\bigcup_{I\uplus J=[1,\#\overline{u}]}\{\langle v\rangle\ \overline{w}\;v\in\mathrm{supp}(\delta_{x}s\cdot\overline{u}_{I}),\overline{w}\in\mathrm{supp}(\delta_{x}\overline{t}\cdot\overline{u})\}$, and similarly for $\langle s^{\prime}\rangle\ \overline{t^{\prime}}$. Observe that for $I\uplus J=[1,\#\overline{u}]$ and $I^{\prime}\uplus J^{\prime}=[1,\#\overline{u^{\prime}}]$ we have $u_{I}\coh u^{\prime}_{I^{\prime}}$ and $u_{J}\coh u^{\prime}_{J^{\prime}}$ so we can apply the induction hypothesis to $s\coh s^{\prime}$ and $u_{I}\coh u^{\prime}_{I^{\prime}}$ and to $\overline{t}\coh\overline{t^{\prime}}$ and $u^{\prime}_{J}\coh u_{J^{\prime}}$ to get the result.

• •

Finally if $\overline{s}=[s_{1},\dots,s_{m}]\coh[s_{m+1},\dots,s_{m+n}]=\overline{s^{\prime}}$ we use a similar reasoning: for any $I,I^{\prime}\subset[1,\#\overline{u}]$ and $J,J^{\prime}\subset[1,\#\overline{u^{\prime}}]$ we have $u_{I}\coh u_{I^{\prime}}$, $u^{\prime}_{J}\coh u^{\prime}_{J^{\prime}}$ and $u_{I}\coh u^{\prime}_{J}$, hence by induction hypothesis for any $v,v^{\prime}\in\bigcup_{i\leq m}\bigcup_{I\subset[1,\#\overline{u}]}\mathrm{supp}(\delta_{x}s_{i}\cdot\overline{u}_{I})$ and $w,w^{\prime}\in\bigcup_{j\leq n}\bigcup_{J\subset[1,\#\overline{u^{\prime}}]}\mathrm{supp}(\delta_{x}s_{m+j}\cdot\overline{u^{\prime}}_{J})$ we have $v\coh v^{\prime}$, $w\coh w^{\prime}$ and $v\coh w$. This gives the first part of the result. Now if $\overline{v}=[v_{1},\dots,v_{k}]\in\mathrm{supp}(\delta_{x}\overline{s}\cdot\overline{u})\cap\mathrm{supp}(\delta_{x}\overline{s^{\prime}}\cdot\overline{u^{\prime}})$ then necessarily $n=m=k$, and we can find sets $I_{i}$ and $J_{i}$ such that $\biguplus_{i\leq k}I_{i}=[1,\#\overline{u}]$, $\biguplus_{i\leq k}J_{i}=[1,\#\overline{u^{\prime}}]$ and $v_{i}\in\mathrm{supp}(\delta_{x}s_{i}\cdot\overline{u}_{I_{i}})\cap\mathrm{supp}(\delta_{x}s_{k+i}\cdot\overline{u^{\prime}}_{J_{i}})$ (up to permutation of the indices in $\overline{s}$ and $\overline{s^{\prime}}$). By induction hypothesis we get $s_{i}=s_{k+i}$ and $\overline{u}_{I_{i}}=\overline{u^{\prime}}_{J_{i}}$, hence $\overline{s}=\overline{s^{\prime}}$ and $\overline{u}=\overline{u^{\prime}}$.

∎

Proposition 2.5**.**

Given $S,S^{\prime}\in\mathbb{R}_{\geq 0}^{((!)\Delta^{\oplus})}$, if $S\coh S^{\prime}$ then $\mathrm{L}(S)\coh\mathrm{L}(S^{\prime})$. If moreover $\mathrm{supp}(S)\cap\mathrm{supp}(S^{\prime})=\emptyset$ then $\mathrm{supp}(\mathrm{L}(S))\cap\mathrm{supp}(\mathrm{L}(S^{\prime}))=\emptyset$.

Proof.

It is sufficient to prove the result for simple terms $\sigma,\sigma^{\prime}$ as the generalisation to finite terms is straightforward. We reason by induction on $\sigma$ and the proof of $\sigma\coh\sigma^{\prime}$.

• •

If $s\oplus_{p}\cdot\coh s^{\prime}\oplus_{p}\cdot$ or $\cdot\oplus_{p}s\coh\cdot\oplus_{p}s^{\prime}$ the result is immediate by induction hypothesis.

• •

If $s\oplus_{p}\cdot\coh\cdot\oplus_{p}s^{\prime}$ then $s$ and $s^{\prime}$ are uniform and by induction hypothesis so are $\mathrm{L}(s)$ and $\mathrm{L}(s^{\prime})$, hence $\mathrm{L}(s)\oplus_{p}\cdot\coh\cdot\oplus_{p}\mathrm{L}(s^{\prime})$.

• •

The case of head normal forms is immediate by induction hypothesis.

• •

If $\lambda\vec{x}.\langle\lambda y.s\rangle\ \overline{t}\,\overline{u}_{1}\,\dots\,\overline{u}_{m}\coh\lambda\vec{x}.\langle\lambda y.s^{\prime}\rangle\ \overline{t}^{\prime}\,\overline{u}^{\prime}_{1}\,\dots\,\overline{u}^{\prime}_{m}$ then we apply Lemma 2.4.

• •

The cases of head choices are immediate.

• •

The case of poly-terms is immediate by induction hypothesis.

∎

Corollary 2.6**.**

Given $S,S^{\prime}\in\mathbb{R}_{\geq 0}^{((!)\Delta^{\oplus})}$, if $S\coh S^{\prime}$ then $\mathrm{nf}(S)\coh\mathrm{nf}(S^{\prime})$. If moreover $\mathrm{supp}(S)\cap\mathrm{supp}(S^{\prime})=\emptyset$ then $\mathrm{supp}(\mathrm{nf}(S))\cap\mathrm{supp}(\mathrm{nf}(S^{\prime}))=\emptyset$.

Proof.

Using Proposition 2.3, by induction on $k$. ∎

This immediately implies that pointwise reduction of infinite uniform terms is well defined, as both complete left reducts and normal forms of distinct but coherent simple (poly-)terms have disjoint supports.

Corollary 2.7**.**

If $S\in\mathbb{R}_{\geq 0}^{(!)\Delta^{\oplus}}$ is uniform then $\sum_{\sigma\in(!)\Delta^{\oplus}}S_{s}\mathrm{L}(\sigma)$ and $\sum_{\sigma\in(!)\Delta^{\oplus}}S_{\sigma}\mathrm{nf}(\sigma)$ are in $\mathbb{R}_{\geq 0}^{(!)\Delta^{\oplus}}$. We write $\mathrm{L}(S)$ and $\mathrm{nf}(S)$ respectively for these sums.

Proof.

For all $\sigma\neq\sigma^{\prime}\in\mathrm{supp}(S)$ we have by hypothesis $\sigma\coh\sigma^{\prime}$ so the previous proposition gives $\mathrm{supp}(\mathrm{L}(\sigma))\cap\mathrm{supp}(\mathrm{L}(\sigma^{\prime}))=\emptyset$. Therefore given any $\tau\in(!)\Delta^{\oplus}$ there is at most one $\sigma\in\mathrm{supp}(S)$ such that $\tau\in\mathrm{supp}(\mathrm{L}(\sigma))$. The same goes for normalisation. ∎

Remark 2.2*.*

Although both complete left reduction and normal forms are well defined for infinite terms, Proposition 2.3 doesn’t hold: consider $\overline{s}_{0}=[\ ]$, $\overline{s}_{n+1}=[\langle\lambda x.x\rangle\ \overline{s}_{n}]$ and $\overline{S}=\sum_{n\in\mathbb{N}}\overline{s}_{n}$, then $\overline{S}$ is uniform and $\mathrm{nf}(\overline{S})=0$ but for all $k\in\mathbb{N}$, $\mathrm{L}^{k}(\overline{S})=\overline{S}\neq 0$. Besides $\mathrm{nf}(\overline{S})$ is not even the limit of the $\mathrm{L}^{k}(\overline{S})$ as $k$ approaches $\infty$. However normal forms are indeed limits of complete left reducts restricted to normal simple terms.

Proposition 2.8**.**

Given a uniform (poly-)term $S\in\mathbb{R}_{\geq 0}^{(!)\Delta^{\oplus}}$ and given $\tau(!)\Delta^{\oplus}$ in normal form, we have $\mathrm{nf}(S)_{\tau}=\mathrm{L}^{k}(S)_{\tau}$ for all $k\in\mathbb{N}$ large enough.

Proof.

If $\tau\in\mathrm{supp}(\mathrm{nf}(S))$ then by Corollary 2.6 there is a unique $\sigma\in\mathrm{supp}(S)$ such that $\tau\in\mathrm{supp}(\mathrm{nf}(\sigma))$, and by Proposition 2.3 for all $k\in\mathbb{N}$ large enough we have $\mathrm{nf}(\sigma)_{\tau}=\mathrm{L}^{k}(\sigma)_{\tau}$. ∎

2.4 Regular Terms

The deterministic Taylor expansion associates to any $\lambda$-term a uniform term, and explicit choices are adopted precisely for the sake of preserving this property in the probabilistic case. Taylor expansions have another important property: they are entirely defined by their support. If a simple term $s$ is in the support of the Taylor expansion of a $\lambda$-term $M$, then its coefficient is the inverse of its multinomial coefficient, which does not depend on $M$. Moreover this property is preserved by normalisation. Using explicit choices enforces this result in the probabilistic case, as well.

Definition 2.6**.**

For any $\sigma\in(!)\Delta^{\oplus}$ we define the multinomial coefficient $\mathrm{m}(\sigma)\in\mathbb{N}$ by:

[TABLE]

where $\overline{s}(u)$ is the multiplicity of $u$ in $\overline{s}$.

Definition 2.7**.**

A uniform term $S\in\mathbb{R}_{\geq 0}^{(!)\Delta^{\oplus}}$ is called regular if for all $\sigma\in\mathrm{supp}(S)$, $S_{\sigma}=\frac{1}{\mathrm{m}(\sigma)}$.

Multinomial coefficients correspond to the number of permutations of multisets which preserve the description of simple (poly-)terms. For instance, given variables $x_{1},\dots,x_{n}\in\mathcal{V}$, the coefficient $\mathrm{m}([x_{1},\dots,x_{n}])$ is exactly the number of permutations $\rho\in\mathfrak{S}_{n}$ such that $(x_{\rho(1)},\dots,x_{\rho(n)})=(x_{1},\dots,x_{n})$. For a more precise interpretation of multinomial coefficients see [9] or [14]. Due to their relation with permutations in multisets, these coefficients appear naturally when we perform substitutions.

Theorem 2.9**.**

For any $\sigma\in(!)\Delta^{\oplus}$ uniform, for $x\in\mathcal{V}$, $\overline{t}\in!\Delta^{\oplus}$ and $u\in\mathrm{supp}(\delta_{x}\sigma\cdot\overline{t})$, we have: $(\delta_{x}\sigma\cdot\overline{t})_{u}=\frac{\mathrm{m}(\overline{t})\mathrm{m}(\sigma)}{\mathrm{m}(u)}$.

There exist two methods to prove similar theorems in the literature, and both can be used to prove Theorem 2.9. The first one is the original proof by Ehrhard and Regnier for the pure deterministic case [9], and its generalisation is straightforward and only requires to extend the notion of uniformity (to take into account that $[s\oplus_{p}\cdot,\cdot\oplus_{p}t]$ is uniform). The second one is by Asada, Tsukada and Ong for a simply typed calculus with choices [14], and it has been extended to the untyped case by Olimpieri and Vaux in an unpublished paper [19]. We present here a direct generalisation of the proof in [9].

Definition 2.8**.**

A multilinear-free (poly)-term is a (poly)-term $\varphi\in(!)\Delta^{+}$ such that all of its variables are free and each one occurs exactly once. A multilinear-free substitution is a partial function $\Phi$ from $\mathcal{V}$ to multilinear-free terms such that $\mathcal{V}(\Phi(x))\cap\mathcal{V}(\Phi(x^{\prime}))=\emptyset$ for all $x\neq x^{\prime}$ in $\mathrm{Dom}(\Phi)$. We say that $(\varphi,\Phi)$ is adapted if $\mathcal{V}(\varphi)\subset\mathrm{Dom}(\Phi)$ and no element of $\mathcal{V}(\Phi)$ is bound in $\varphi$. Then $\Phi\varphi$ is the multilinear-free (poly)-term obtained by applying $\Phi$ on the variables of $\varphi$. Similarly for any multilinear-free (poly)-term $\varphi$ and $p:\mathcal{V}(\varphi)\rightarrow\mathcal{V}$ we write $p\varphi$ for the term obtained by applying $p$ to the variables of $\varphi$ without renaming captured variables. A pair $(\varphi,p)$ is said to represent $\sigma\in\Delta^{+}$ if $p\varphi=\sigma$.

Definition 2.9**.**

We define the following sets of bijections over variables:

[TABLE]

Lemma 2.10**.**

$|\mathrm{Iso}(\varphi,p)|=\mathrm{m}(p\varphi)$.

Lemma 2.11**.**

For any $g\in\mathrm{Iso}(p,\Phi,q)$ there exists a unique $\pi(g)\in\Sigma_{q}$ such that $g\Phi=\Phi\pi(g)$, and $\pi:\mathrm{Iso}(p,\Phi,q)\rightarrow\Sigma_{p}$ is a group homomorphism.

Lemma 2.12**.**

$\pi(\mathrm{Iso}(p,\Phi,q))\mathrm{Iso}(\varphi,p)\subset\mathrm{Iso}(\varphi,p,\Phi,q)$.

Definition 2.10**.**

We define by induction a notion of uniformity for pairs $(F,p)$ where $F$ is a multilinear-free polyterm and $p:\mathcal{V}(F)\rightarrow\mathcal{V}$:

• •

$([x_{1},\dots,x_{n}],p)$ is uniform if $p(x_{i})=p(x_{j})$ for all $i,j$;

• •

$([\lambda x.\varphi_{1},\dots,\lambda x.\varphi_{n}],p)$ is uniform if $([\varphi_{1},\dots,\varphi_{n}],p)$ is uniform;

• •

$([\langle\varphi_{1}\rangle\ G_{1},\dots,\langle\varphi_{n}\rangle\ G_{n}],p)$ is uniform if $([\varphi_{1},\dots,\varphi_{n}],q)$ and $(G_{1}+\dots+G_{n},r)$ are uniform, with $q$ and $r$ the obvious restrictions of $p$;

• •

$([\varphi_{1}\oplus_{p}\cdot,\dots,\varphi_{n}\oplus_{p}\cdot,\cdot\oplus_{p}\varphi^{\prime}_{1},\dots,\cdot\oplus_{p}\varphi^{\prime}_{n^{\prime}}],p)$ is uniform if $([\varphi_{1},\dots,\varphi_{n}],q)$ and $([\varphi^{\prime}_{1},\dots,\varphi^{\prime}_{n^{\prime}}],q^{\prime})$ are uniform, where $q$ and $q^{\prime}$ are the obvious restrictions of $p$.

If $\varphi$ is a multilinear-free simple term we say that $(\varphi,p)$ is uniform if $([\varphi],p)$ is uniform.

Lemma 2.13**.**

A pair $(\varphi,p)$ is uniform iff $p\varphi$ is uniform (i.e. $p\varphi\coh p\varphi$).

Lemma 2.14**.**

For $(\varphi,p)$ a uniform pair and $\Phi,\Phi^{\prime}$ two multilinear-free substitutions over $\mathcal{V}(\varphi)$, if $\Phi\varphi=\Phi^{\prime}\varphi$ then there exists $f\in\mathrm{Iso}(\varphi,p)$ such that $\Phi^{\prime}=\Phi f$.

Lemma 2.15**.**

If $(\varphi,p)$ is uniform then $\mathrm{Iso}(\varphi,p,\Phi,q)\subset\pi(\mathrm{Iso}(p,\Phi,q))\mathrm{Iso}(\varphi,p)$.

Proposition 2.16**.**

If $(\varphi,p)$ is uniform then $|\mathrm{Iso}(\varphi,p,\Phi,q)|=\frac{|\mathrm{Iso}(p,\Phi,q)||\mathrm{Iso}(\varphi,p)|}{|\mathrm{Iso}(\Phi\varphi,q)|}$

Proof.

We have $|\pi(\mathrm{Iso}(p,\Phi,q))\mathrm{Iso}(\varphi,p)|=\frac{|\pi(\mathrm{Iso}(p,\Phi,q))||\mathrm{Iso}(\varphi,p)|}{|\pi(\mathrm{Iso}(p,\Phi,q))\cap\mathrm{Iso}(\varphi,p)|}$.

Observe that $|\pi(\mathrm{Iso}(p,\Phi,q))|=\frac{|\mathrm{Iso}(p,\Phi,q)|}{\ker\pi}$ and $|\pi(\mathrm{Iso}(p,\Phi,q))\cap\mathrm{Iso}(\varphi,p)|=|\ker\pi||\mathrm{Iso}(\Phi\varphi,q)|$. ∎

This is enough to conclude the proof of Theorem 2.9.

This theorem ensures that a regular $\beta$-redex $\frac{1}{\mathrm{m}(\langle\lambda x.s\rangle\ \overline{t})}.\langle\lambda x.s\rangle\ \overline{t}$ reduces into a regular term. More generally, the theorem is the key step towards proving that regular (poly-)terms always normalise to regular (poly-)terms.

Proposition 2.17**.**

If $\sigma$ is uniform then for any $\tau\in\mathrm{supp}(\mathrm{L}(\sigma))$, $\mathrm{L}(\sigma)_{\tau}=\frac{\mathrm{m}(\sigma)}{\mathrm{m}(\tau)}$.

Proof.

We reason by induction on $\sigma$, using Theorem 2.9 when dealing with $\beta$-reduction. Observe that in the case of a poly-term $\overline{s}=[s_{1},\dots,s_{n}]$, according to Proposition 2.5 for all $i,j\leq n$ we have either $s_{i}=s_{j}$ or $\mathrm{supp}(\mathrm{L}(s_{i}))\cap\mathrm{supp}(\mathrm{L}(s_{j}))=\emptyset$. This means that for a poly-term $\overline{t}=[t_{1},\dots,t_{n}]\in\mathrm{supp}(\mathrm{L}(\overline{s}))$ the number of pairwise distinct sequences $(t_{\rho(1)},\dots,t_{\rho(n)})$ with $\rho\in\mathfrak{S}_{n}$ such that $t_{\rho(i)}\in\mathrm{supp}(\mathrm{L}(s_{i}))$ for all $i\leq n$ is exactly $\frac{\prod_{u\in\Delta^{\oplus}}\overline{s}(u)!}{\prod_{v\in\Delta^{\oplus}}\mathrm{L}(\overline{s})(v)!}$. ∎

Corollary 2.18**.**

For all finite regular term $S$, $\mathrm{L}(S)$ and $\mathrm{nf}(S)$ are regular.

Theorem 2.19**.**

If $S\in\mathbb{R}_{\geq 0}^{(!)\Delta^{\oplus}}$ is regular then $\mathrm{nf}(S)$ is regular.

Proof.

This follows directly from the previous result and Corollary 2.6. ∎

2.5 Regularity and the Exponential

The regularity of terms is preserved by the constructors of simple resource terms.

Proposition 2.20**.**

For all $x\in\mathcal{V}$, $S\in\mathbb{R}_{\geq 0}^{\Delta^{\oplus}}$ regular and $\overline{T}\in\mathbb{R}_{\geq 0}^{!\Delta^{\oplus}}$ regular, the terms $1.x$, $\lambda x.S$, $S\oplus_{p}\cdot$, $\cdot\oplus_{p}S$ and $\langle S\rangle\ \overline{T}$ are regular.

One may expect a similar result for poly-terms: if $S_{1}$,…,$S_{n}$ in $\mathbb{R}_{\geq 0}^{\Delta^{\oplus}}$ are regular then $[S_{1},\dots,S_{n}]$ is regular. However, this is not the case: $1.x$ is regular and yet $1.[x,x]$ is not. Indeed nontrivial coefficients appear in $\mathrm{m}(\sigma)$ precisely when $\sigma$ contains simple poly-terms with multiplicities greater than $1$, so the regular sum with the same support as $[S_{1},\dots,S_{n}]$ has no simple description. A natural way to build regular poly-terms from regular terms is to use the following construction.

Definition 2.11**.**

The exponential of $S\in\mathbb{R}_{\geq 0}^{\Delta^{\oplus}}$ is $!S=\sum_{n\in\mathbb{N}}\frac{1}{n!}[S^{n}]\in\mathbb{R}_{\geq 0}^{!\Delta^{\oplus}}$, where $[S^{n}]$ stands for the poly-term $[S,\dots,S]$ with $n$ copies of $S$.

Proposition 2.21**.**

If $S\in\mathbb{R}_{\geq 0}^{\Delta^{\oplus}}$ is regular then $!S$ is regular.

Proof.

The key point is that the number of sequences $(s_{1},\dots,s_{n})$ which describe a given simple poly-term $\overline{s}=[s_{1},\dots,s_{n}]$ is exactly $\frac{n!}{\prod_{u\in\Delta^{\oplus}}\overline{s}(u)!}$. ∎

With these results, we have all the ingredients we need to translate (probabilistic) $\lambda$-terms into regular terms: variables and abstractions of regular terms are regular, and we can define an application between regular terms following Girard’s call-by-name translation of intuitionistic logic into linear logic [10]: $S$ applied to $T$ is $\langle S\rangle\ !T$.

3 Explicit Probabilistic Taylor Expansion

This section is devoted to defining and studying the Taylor expansion with explicit choices, or explicit Taylor expansion, of probabilistic $\lambda$-terms. It is named as such because its target is the set of probabilistic resource terms, as defined in the previous section, rather than the usual ones. This is not the main contribution of this paper, but an intermediate step in the study of Taylor expansion as defined in Section 4.

3.1 The Definition

Probabilistic $\lambda$-terms are $\lambda$-terms enriched with a probabilistic choice operator.

Definition 3.1**.**

The set of probabilistic $\lambda$-terms $\Lambda^{+}$ is:

[TABLE]

Example 3.1*.*

Let us consider the probabilistic $\lambda$-term $Q=\Delta(I+_{\frac{1}{2}}\Omega)$, where $\Delta=\lambda x.xx$, $I=\lambda x.x$, and $\Omega$ is any diverging term, e.g. $\Delta\Delta$. The term converges (to $I$) with probability $\frac{1}{4}$, and will be used as a running example throughout this section.

Definition 3.2**.**

The explicit Taylor expansion $M^{*\oplus}$ is defined inductively as follows:

[TABLE]

Definition 3.3**.**

The support $\mathcal{T}^{r}(M)\subset\Delta^{+}$ of the Taylor expansion of $M\in\Lambda^{+}$ is defined by:

[TABLE]

Proposition 3.1**.**

For every $M\in\Lambda^{+}$, it holds that

[TABLE]

Proof.

By induction on the structure of $M$:

• •

If $M$ is a variable $x$, then

[TABLE]

• •

If $M$ is an abstraction $\lambda x.N$, then:

[TABLE]

• •

If $M$ is an application $NL$, then we can first of all give the following lemma. For every $\overline{t}\in\mathrm{M}^{n}_{\mathrm{fin}}(X)$, it holds that

[TABLE]

As a consequence,

[TABLE]

• •

If $M$ is a sum $N+_{p}L$, then

[TABLE]

∎

The results from the previous section immediately imply that Taylor expansions are regular resource terms and that they are normalisable.

Proposition 3.2**.**

For all $M\in\Lambda^{+}$, the explicit Taylor expansion $M^{*\oplus}$ is uniform and regular.

Proof.

This is a direct consequence of Proposition 2.20 and Proposition 2.21. ∎

Corollary 3.3**.**

Every explicit Taylor expansion $M^{*\oplus}$ has a normal form $\mathrm{nf}(M^{*\oplus})$, which we call the explicit Taylor normal form of $M$, and which is regular.

Proof.

This is given by Theorem 2.19. ∎

3.2 Probabilistic Reduction

In the literature, the probabilistic $\lambda$-calculus is usually endowed with a labelled transition relation $\xrightarrow{p}$ describing a probabilistic reduction process, where a choice $M\oplus_{p}N$ reduces to $M$ with probability $p$ and to $N$ with probability $1-p$. Another kind of operational semantics, more common for other quantitative calculi such as the algebraic $\lambda$-calculus, is to have a non-labelled reduction where choices simply commute with some contexts, as we did in our probabilistic resource calculus. In this paper we use both kinds of semantics. On one hand a deterministic operational semantics will simplify the comparison between the operational semantics of $\lambda$-terms and that of their Taylor expansion, but on the other hand explicit Taylor expansion precisely splits choices into two different branches, just like labelled transition systems do.

Definition 3.4**.**

Head contexts are contexts of the form $\lambda\vec{x}.[\ ]\ \vec{P}$, and are indicated with the metavariable $H$. Head normal forms are terms of the form $H[y]$. We write $\mathrm{hnf}$ for the set of all head normal forms. We now define a formal system deriving judgements in the form $\rho\vdash M\rightarrow\mathrel{\mkern-14.0mu}\rightarrow h$ where $M\in\Lambda^{+}$, $h\in\mathrm{hnf}$ and $\rho$ is a finite sequence of elements in $\{\mathrm{l},\mathrm{r}\}\times[0,1]$:

[TABLE]

where $\epsilon$ is the empty sequence and $(\ell,p)\cdot(\rho_{1},\dots,\rho_{n})=((\ell,p),\rho_{1},\dots,\rho_{n})$ for $\ell\in\{\mathrm{l},\mathrm{r}\}$.

Proposition 3.4**.**

For all $M\in\Lambda^{+}$ and $\rho$ there is at most one $h\in\mathrm{hnf}$ such that $\rho\vdash M\rightarrow\mathrel{\mkern-14.0mu}\rightarrow h$.

Definition 3.5**.**

For all $M\in\Lambda^{+}$ we define the complete left reduct of $M$ by:

[TABLE]

Proposition 3.5**.**

For all $M\in\Lambda^{+}$, $\mathrm{L}(M^{*\oplus})=\mathrm{L}(M)^{*\oplus}$.

Proof.

By a simple induction on $M$. ∎

Proposition 3.6**.**

If $\rho\vdash M\rightarrow\mathrel{\mkern-14.0mu}\rightarrow h$ then either $\rho\vdash\mathrm{L}(M)\rightarrow\mathrel{\mkern-14.0mu}\rightarrow h$ or $\rho\vdash\mathrm{L}(M)\rightarrow\mathrel{\mkern-14.0mu}\rightarrow\mathrm{L}(h)$. Conversely if $\rho\vdash\mathrm{L}(M)\rightarrow\mathrel{\mkern-14.0mu}\rightarrow h$ then there is $h^{\prime}\in\mathrm{hnf}$ such that $\rho\vdash M\rightarrow\mathrel{\mkern-14.0mu}\rightarrow h^{\prime}$ and either $h=h^{\prime}$ or $h=\mathrm{L}(h^{\prime})$.

Proof.

By induction on $M$.

• •

For $M+_{p}N$ for both results the sequence of choices cannot be empty. Let us assume wlog we reduce to the left-hand side. If $(\mathrm{l},p)\cdot\rho\vdash M+_{p}N\rightarrow\mathrel{\mkern-14.0mu}\rightarrow h$ then $\rho\vdash M\rightarrow\mathrel{\mkern-14.0mu}\rightarrow h$ and by induction hypothesis either $\rho\vdash\mathrm{L}(M)\rightarrow\mathrel{\mkern-14.0mu}\rightarrow h$ or $\rho\vdash\mathrm{L}(M)\rightarrow\mathrel{\mkern-14.0mu}\rightarrow\mathrm{L}(h)$, hence either $(\mathrm{l},p)\cdot\rho\vdash\mathrm{L}(M)+_{p}\mathrm{L}(N)\rightarrow\mathrel{\mkern-14.0mu}\rightarrow h$ or $(\mathrm{l},p)\cdot\rho\vdash\mathrm{L}(M)+_{p}\mathrm{L}(N)\rightarrow\mathrel{\mkern-14.0mu}\rightarrow\mathrm{L}(h)$. Similarly if $(\mathrm{l},p)\cdot\rho\vdash\mathrm{L}(M)+_{p}\mathrm{L}(N)\rightarrow\mathrel{\mkern-14.0mu}\rightarrow h$ we conclude by induction hypothesis.

• •

For head normal forms if $\epsilon\vdash h\rightarrow\mathrel{\mkern-14.0mu}\rightarrow h$ then $\epsilon\vdash\mathrm{L}(h)\rightarrow\mathrel{\mkern-14.0mu}\rightarrow\mathrm{L}(h)$, and conversely if $\epsilon\vdash\mathrm{L}(h)\rightarrow\mathrel{\mkern-14.0mu}\rightarrow\mathrm{L}(h)$ then $\epsilon\vdash h\rightarrow\mathrel{\mkern-14.0mu}\rightarrow h$.

• •

If there is a head $\beta$-redex then $\lambda\vec{x}.(\lambda y.M)\,N\,P_{1}\,\dots\,P_{m}$ and \lambda\vec{x}.M\left[\raisebox{1.99997pt}{N}/\raisebox{-1.99997pt}{y}\right]\,P_{1}\,\dots\,P_{m} have the same reductions. The same goes for head choices.

∎

An interesting property of explicit Taylor expansion is that the explicit Taylor normal form of a term $M$ is precisely given by the explicit Taylor normal forms of the head normal forms $h$ of $M$, as well as the sequences of choices $\rho$ such that $\rho\vdash M\rightarrow\mathrel{\mkern-14.0mu}\rightarrow h$.

Definition 3.6**.**

Given a sequence of choices $\rho$ and $s\in\Delta^{\oplus}$ we define $\rho\cdot s\in\Delta^{\oplus}$ by induction on the length of $\rho$ by:

[TABLE]

We extend this definition to $\mathbb{R}_{\geq 0}^{\Delta^{\oplus}}$ by linearity.

Theorem 3.7**.**

Given any $M\in\Lambda^{+}$,

[TABLE]

Proof.

First observe that these resource terms are regular: Corollary 3.3 states that $\mathrm{nf}(M^{*\oplus})$ and the $\mathrm{nf}(h^{*\oplus})$ are regular (so the $\rho\cdot\mathrm{nf}(h^{*\oplus})$ are regular too), and if $\rho\vdash M\rightarrow\mathrel{\mkern-14.0mu}\rightarrow h$ and $\rho^{\prime}\vdash M\rightarrow\mathrel{\mkern-14.0mu}\rightarrow h^{\prime}$ then either $\rho=\rho^{\prime}$ and by Proposition 3.4 $h=h^{\prime}$, or $\rho\neq\rho^{\prime}$ and then $\rho\cdot\mathrm{nf}(h^{*\oplus})$ and $\rho^{\prime}\cdot\mathrm{nf}((h^{\prime})^{*\oplus})$ are coherent and have disjoint supports. Thus we only need to prove that these terms have the same supports.

Now if $\rho\vdash M\rightarrow\mathrel{\mkern-14.0mu}\rightarrow h$ then we prove by induction on the proof this relation that if $s\in\mathrm{supp}(\mathrm{nf}(h^{*\oplus}))$ then $\rho\cdot s\in\mathrm{supp}(\mathrm{nf}(M^{*\oplus}))$. More precisely we prove that for some $k\in\mathbb{N}$, $\rho\cdot s\in\mathrm{supp}(\mathrm{L}^{k}(M^{*\oplus}))$.

• •

If $\epsilon\vdash h\rightarrow\mathrel{\mkern-14.0mu}\rightarrow h$ the result is immediate.

• •

If $\rho\vdash H[(\lambda x.M)N]\rightarrow\mathrel{\mkern-14.0mu}\rightarrow h$ and $s\in\mathrm{supp}(\mathrm{nf}(h^{*\oplus}))$ then by induction hypothesis there is $k\in\mathbb{N}$ such that \rho\cdot s\in\mathrm{supp}(\mathrm{L}^{k}(H[(M\left[\raisebox{1.99997pt}{N}/\raisebox{-1.99997pt}{x}\right]]^{*\oplus})), ie $\rho\cdot s\in\mathrm{supp}(\mathrm{L}^{k+1}(H[(\lambda x.M)N]^{*\oplus}))$.

• •

The same goes for head choices.

Conversely according to Proposition 2.8 for all $\tau$ in normal form there is $k\in\mathbb{N}$ such that $\mathrm{nf}(M^{*\oplus})_{\tau}=\mathrm{L}^{k}(M^{*\oplus})_{\tau}$, and according to Proposition 3.5 we have $\mathrm{L}^{k}(M^{*\oplus})=\mathrm{L}^{k}(M)^{*\oplus}$. Hence if $\tau\in\mathrm{supp}(\mathrm{nf}(M^{*\oplus}))$ we have $\tau\in\mathrm{supp}(\mathrm{L}^{k}(M)^{*\oplus})$. It is then easy to prove by induction on $\tau$ that there are $\rho$ and $h$ such that $\rho\vdash\mathrm{L}^{k}(M)\rightarrow\mathrel{\mkern-14.0mu}\rightarrow h$ and $\tau\in\rho\cdot\mathrm{supp}(h^{*\oplus})$. Then according to the previous proposition there is $h^{\prime}$ such that $\rho\vdash M\rightarrow\mathrel{\mkern-14.0mu}\rightarrow h^{\prime}$ and $h=\mathrm{L}^{k^{\prime}}(h^{\prime})$ (with $k^{\prime}\leq k$), hence $\tau\in\rho\cdot\mathrm{supp}(\mathrm{nf}(h^{*\oplus}))$. ∎

Lemma 3.8**.**

For all $M,N\in\Lambda^{+}$, if $s\in\mathrm{supp}(M^{*\oplus})$ and $\overline{t}\in\mathrm{supp}(!N^{*\oplus})$ then \delta_{x}s\cdot\overline{t}\in\mathrm{supp}(M\left[\raisebox{1.99997pt}{N}/\raisebox{-1.99997pt}{x}\right]^{*\oplus}).

Proof.

By induction on $M$. ∎

Lemma 3.9**.**

For any $M,N\in\Lambda^{+}$ and any head context $H$ we have:

[TABLE]

4 Generic Taylor Expansion of Probabilistic $\lambda$-terms

4.1 Barycentric Semantics of Choices

The explicit probabilistic Taylor expansion is satisfactory in that it is an extension of deterministic Taylor expansion which preserves its most important properties: it is regular and so are its normal forms. But while deterministic Taylor normal forms are well known to correspond to Böhm trees [7], explicit Taylor normal forms are not such a good denotational semantics for probabilistic $\lambda$-calculus, as they take the exact choices made during the reduction into account. For instance the terms $x\oplus_{\frac{1}{2}}y$ and $y\oplus_{\frac{1}{2}}x$ have distinct explicit Taylor normal forms while one could expect them to have the same semantics. More precisely we expect any model of the probabilistic $\lambda$-calculus to interpret probabilistic choices as a barycentric sum respecting the following equivalence.

Definition 4.1**.**

The barycentric equivalence $\mathrel{\equiv_{\mathrm{bar}}}$ is the least congruence on $\Lambda^{+}$ such that for all $M,N,P\in\Lambda^{+}$ and $p,q\in[0,1]$:

[TABLE]

Saying it another way, We want a notion of Taylor expansion $M^{*}$ such that if $M\mathrel{\equiv_{\mathrm{bar}}}N$ then $M^{*}=N^{*}$. This is easy to achieve, as the resource $\lambda$-calculus stemmed precisely from quantitative models of the $\lambda$-calculus, and resource terms are linear combinations.

Definition 4.2**.**

The sets of simple resource terms $\Delta$ and of simple resource poly-terms $!\Delta$ are:

[TABLE]

The set of resource terms is $\mathbb{R}_{\geq 0}^{\Delta}$ and the set of resource poly-terms is $\mathbb{R}_{\geq 0}^{!\Delta^{\oplus}}$.

Definition 4.3**.**

The Taylor expansion $M^{*}\in\mathbb{R}_{\geq 0}^{\Delta}$ of a term $M\in\Lambda^{+}$ is defined inductively as follows:

[TABLE]

The definition of the Taylor expansion of a probabilistic choice immediately gives the expected property.

Proposition 4.1**.**

If $M\mathrel{\equiv_{\mathrm{bar}}}N$ then $M^{*}=N^{*}$.

4.2 Normalisation

Unfortunately, these Taylor expansions lack all the good properties of explicit expansions: they are not entirely defined by their support, and those supports are not uniform, so we do not even know if such Taylor expansions admit normal forms. But there is actually a close relationship between explicit and non explicit Taylor expansions which can be used to recover our most important results. Indeed, switching from the explicit Taylor expansion to the Taylor expansion simply amounts to using coefficients instead of explicit choices.

Definition 4.4**.**

Given any $\sigma\in(!)\Delta^{\oplus}$ we define $|\sigma|\in(!)\Delta$ and a probability $\mathcal{P}(\sigma)$ as follows:

[TABLE]

To any probabilistic resource (poly-)term $S\in\mathbb{R}_{\geq 0}^{(!)\Delta^{\oplus}}$ one could associate the resource term $\sum_{\sigma\in(!)\Delta^{\oplus}}S_{\sigma}\mathcal{P}(\sigma).|\sigma|$. But just like with normalisation, infinite coefficients may appear. For instance, removing the choices from $S=\sum((x\oplus_{1}\cdot)\dots)\oplus_{1}\cdot$ could give $x$ an infinite coefficient. Fortunately, we do not get any infinite coefficient if we work with regular terms.

Proposition 4.2**.**

For any $\mathcal{S}\subset(!)\Delta^{\oplus}$ such that for all $\sigma,\sigma^{\prime}\in\mathcal{S}$, $\sigma\coh\sigma^{\prime}$ and $|\sigma|=|\sigma^{\prime}|$ we have $\sum_{\sigma\in\mathcal{S}}\mathcal{P}(\sigma)\leq 1$.

Corollary 4.3**.**

For all $S\in\mathbb{R}_{\geq 0}^{(!)\Delta^{\oplus}}$ regular, $\sum_{\sigma\in(!)\Delta^{\oplus}}S_{\sigma}\mathcal{P}(\sigma).|\sigma|$ is in $\mathbb{R}_{\geq 0}^{(!)\Delta}$.

In particular, we can apply this process to explicit Taylor expansions and to their normal forms. It is easy to see that we associate to every explicit Taylor expansion the corresponding Taylor expansion, but more interestingly erasing choices commutes with normalisation.

Proposition 4.4**.**

For any $M\in\Lambda^{+}$:

[TABLE]

hence $\sum_{s\in\Delta}M^{*}_{s}.\mathrm{nf}(s)$ is well defined. We denote it by $\mathrm{nf}(M^{*})$ and we call it the Taylor normal form of $M$.

Proof.

The key point is that $\mathrm{nf}(|\sigma|)=|\mathrm{nf}(\sigma)|$ and for any $\tau\in\mathrm{supp}(\mathrm{nf}(\sigma))$, $\mathcal{P}(\tau)=\mathcal{P}(\sigma)$. ∎

4.3 Adequacy

The behaviour of a probabilistic $\lambda$-term is usually described as a (sub-)probability distribution over the possible results of its evaluation. In particular, the observable behaviour of a term is its convergence probability, i.e. the probability for its computation to terminate [11, 5]. To show that the Taylor expansion gives a meaningful semantics we will prove it is adequate, i.e. it does not equate terms which are not observationally equivalent. We can actually show a more refined result, given as a Corollary of Theorem 3.7: the Taylor normal form of a term is given by the Taylor normal forms of its head normal forms.

Definition 4.5**.**

The any sequence of choices $\rho$ we associate a probability $\mathcal{P}(\rho)$ by:

[TABLE]

The probability $\mathcal{P}\left(M\rightarrow\mathrel{\mkern-14.0mu}\rightarrow h\right)$ for $M\in\Lambda^{+}$ to reduce into a head normal form $h$ and its convergence probability $\mathcal{P}_{\Downarrow}(M)$ are defined as follows:

[TABLE]

Proposition 4.5**.**

For $M\in\Lambda^{+}$ we have:

[TABLE]

Proof.

This is given by Proposition 4.4 and Theorem 3.7. Observe that for any $\rho$ and $s\in\mathrm{nf}(h^{*\oplus})$ we have $\mathcal{P}(\rho\cdot s)=\mathcal{P}(\rho)\mathcal{P}(s)$ and $|\rho\cdot s|=|s|$. ∎

The adequacy follows immediately.

Proposition 4.6**.**

If $\mathrm{nf}(M^{*})=\mathrm{nf}(N^{*})$ then for all context $C$, $\mathcal{P}_{\Downarrow}(C[M])=\mathcal{P}_{\Downarrow}(C[N])$, i.e. $M$ and $N$ are contextually equivalent.

Proof.

First the convergence probability of a term $M$ is exactly the sum of the coefficients $\mathrm{nf}(M^{*})_{\lambda\vec{x}.y\,[\ ]\,\dots\,[\ ]}$. Second if $\mathrm{nf}(M^{*})=\mathrm{nf}(N^{*})$ then $\mathrm{nf}(C[M]^{*})=\mathrm{nf}(C[N]^{*})$ for all $C$. ∎

5 On the Taylor Expansion and Böhm Trees

5.1 A Commutation Theorem

Deterministic Taylor normal forms are an adequate semantics for the probabilistic $\lambda$-calculus, but more precisely they are known to correspond to Böhm trees [7]. We are now able to show that this result extends to the probabilistic case.

Definition 5.1**.**

The sets of probabilistic Böhm trees $\mathcal{PT}_{d}$ and of probabilistic value trees $\mathcal{VT}_{d}$ for $d\in\mathbb{N}$ are defined inductively by induction on the depth $d$:

[TABLE]

where $\mathbf{D}(X)$ is the set of countable-support subprobability distributions on any set $X$, $\bot$ is the only subprobability distribution over the empty set, i.e. over $\mathcal{VT}_{0}$.

Definition 5.2**.**

We define $\mathit{PT}_{d}(M)$ for $M\in\Lambda^{+}$ and $d\geq 0$, and $\mathit{VT}_{d}(h)$ for $h\in\mathrm{hnf}$ and $d\geq 1$ by induction on the depth $d$ as follows:

[TABLE]

Intuitively the Böhm tree of a term $M$ is the limit of its finite Böhm approximants $\mathit{PT}_{d}(M)$. To avoid making the structure of Böhm trees of infinite depth explicit, we simply write $\mathit{PT}(M)$ for the sequence $(\mathit{PT}_{d}(M))_{d\in\mathbb{N}}$. In particular we say that $M$ and $N$ have the same Böhm tree iff $\mathit{PT}_{d}(M)=\mathit{PT}_{d}(N)$ for every $d\in\mathbb{N}$.

The definition of the Taylor expansion can easily be generalised to finite-depth Böhm trees. We simply define $\mathbf{T}^{*}$ for $\mathbf{T}\in\mathcal{PT}_{d}$ and $\mathbf{t}^{*}$ for $\mathbf{t}\in\mathcal{VT}_{d+1}$ by:

[TABLE]

We extend this definition to infinite Böhm trees as follows: if $s\in\Delta$ contains at most $d_{s}$ layers of nested multisets then for any $M\in\Lambda^{+}$, $\mathit{PT}_{d}(M)^{*}_{s}=\mathit{PT}_{d_{s}}(M)^{*}_{s}$ for all $d\geq d_{s}$, so $\mathit{PT}(M)^{*}_{s}$ can be taken as $\mathit{PT}_{d_{s}}(M)^{*}_{s}$. Then the Taylor normal form of a term is exactly the Taylor expansion of its Böhm tree.

Theorem 5.1**.**

For all $M\in\Lambda^{+}$, $\mathrm{nf}(M^{*})=(\mathit{PT}(M))^{*}$.

Proof.

We prove $\mathrm{nf}(M^{*})_{s}=(\mathit{PT}(M))^{*}_{s}$ by induction on $d_{s}$, using to Proposition 4.5. ∎

This theorem is important but it does not actually prove the correspondence between Böhm trees and Taylor expansions: we still do not know if Taylor expansion is injective on Böhm trees. In the deterministic case this is simple to prove: to every deterministic Böhm tree $\mathbf{T}$ of depth $d$ we can associate a simple resource term $s_{\mathbf{T}}$ such that for all $M\in\Lambda$, $\mathit{BT}_{d}(M)=\mathbf{T}$ iff $s_{\mathbf{T}}\in\mathrm{supp}(\mathrm{nf}(M^{*}))$ (by associating $\lambda\vec{x}.\langle y\rangle\ [s_{\mathbf{T}_{1}}]\,\dots\,[s_{\mathbf{T}_{m}}]$ to $\lambda\vec{x}.y\,\mathbf{T}_{1}\,\dots\,\mathbf{T}_{m}$). The situation is more complicated in the probabilistic case, as Taylor expansions are no longer defined solely by their supports. The rest of this article is devoted to proving injectivity for the probabilistic Taylor expansion.

5.2 Böhm Tests

In order to better understand coefficients in probabilistic Taylor expansions and to get our injectivity property, we use a notion of testing coming from the literature on labelled Markov decision processes [17].

Definition 5.3** (Böhm Tests).**

The classes of Böhm term tests (BTTs) and Böhm hnf tests (BHTs) are given as follows, by mutual induction:

[TABLE]

The probability of success of a BTT $T$ on a term $M$ and the probability of success of a BHT $t$ on an head-normal-form $h$, indicated as $\mathsf{Pr}(T,M)$ and $\mathsf{Pr}(t,h)$ respectively, are defined as follows:

[TABLE]

[TABLE]

The following is the first step towards proving the main result of this paper, as it characterises Böhm tree equality as equality of families of real numbers.

Theorem 5.2**.**

Two terms $M$ and $N$ have the same Böhm trees iff for every BTT $T$ it holds that $\mathsf{Pr}(M,T)=\mathsf{Pr}(N,T)$.

Theorem 5.2 is quite nontrivial to prove. Section 6 is dedicated to a proof of this result.

6 Probabilistic Tree Transition Systems and Testing Equivalence

A tree transition system is a tuple $\mathbf{T}=(Q,S,\mathcal{L},\mathcal{I},\delta,\gamma)$ such that

• •

$Q$ and $S$ are sets of linear states and of branching states, respectively.

• •

$\mathcal{L}$ and $\mathcal{I}$ are disjoint sets of labels.

• •

The linear transition map $\delta$ is a partial function from $Q\times\mathcal{L}$ to distributions over $S$;

• •

The branching transition map $\gamma$ is a partial function from $S\times\mathcal{I}$ to $Q^{*}$.

An example of a tree transition system is the one coming out of Böhm trees as defined in the last section. In particular:

• •

$Q$ is the set of terms, while $S$ is the set of head normal forms.

• •

$\mathcal{L}=\{\mathsf{ev}\}$, while $\mathcal{I}=\{(\lambda x_{1}.\cdots\lambda x_{n}.y)\}$.

• •

$\delta$ and $\gamma$ can be defined in the natural way.

Let us call the resulting tree transition system $\mathbf{BT}$.

A tree bisimulation relation for a tree transition system $\mathbf{T}=(Q,S,\mathcal{L},\mathcal{I},\delta,\gamma)$ is given by two relations $R^{Q}$ and $R^{S}$ such that the following two contstraints both hold:

• •

If $qR^{Q}r$, then for every label $\ell\in\mathcal{L}$ it holds that $\delta(q,\ell)$ is defined iff $\delta(r,\ell)$ is defined, and in the latter case there is $I$ such that

[TABLE]

where for every $i\in I$ it holds that $q_{i}T^{S}r_{i}$.

• •

If $sR^{S}t$, then for every label $\iota\in\mathcal{I}$ it holds that $\gamma(s,\iota)$ is defined iff $\gamma(r,\iota)$ is defined, and in the latter case there is $n$ such that

[TABLE]

where for every $1\leq i\leq n$ it holds that $s_{i}R^{Q}t_{i}$.

The (pointwise) largest bisimulation relation is called tree-bisimilarity, and is indicated as $\sim_{\mathbf{T}}=(\sim_{\mathbf{T}}^{Q},\sim_{\mathbf{T}}^{S})$.

Lemma 6.1**.**

Two terms $M$ and $N$ have the same Böhm Tree iff $M\sim_{\mathbf{BT}}N$.

Proof.

One the one hand, we can prove that equality of Böhm trees is a tree bisimulation relation for $\mathbf{BT}$. On the other hand, we can prove that if $M\sim_{\mathbf{BT}}N$, then their Böhm trees are equal up to any level $n$, by induction on $n$. ∎

The rest of this section is devoted to proving that tree-bisimilarity can be characterised by a notion of testing, which generalises the one we saw for $\mathbf{BT}$ in the previous section. The set of linear and branching tests are defined as follows

[TABLE]

The probability of success of a linear test $T_{L}$ on a linear state $q$ and the one of a branching test $T_{B}$ on a branching state $s$, indicated as $\mathsf{Pr}(T_{L},q)$ and $\mathsf{Pr}(T_{B},s)$ respectively, are defined as follows:

[TABLE]

Two linear states $q,r$ are said to be testing equivalent iff for every linear test $T_{L}$ we have that

[TABLE]

Similarly for branching states. Testing equivalence is indicated with $\eqsim_{\mathbf{T}}$, where $\mathbf{T}$ is the underlying tree transition system. It consists of a pair of equivalence relations $(\eqsim_{\mathbf{T}}^{Q},\eqsim_{\mathbf{T}}^{S})$

Theorem 6.2**.**

$\eqsim_{\mathbf{T}}$* and $\sim_{\mathbf{T}}$ coincide.*

Proof.

The idea is to make heavy use of the results from [17], which relate bisimilarity and testing equivalence. We are however a little detour which needs to be taken, due to the fact that the results from [17] are formulated for Labelled Markov Chains (LMCs), while we need the same result we need here is for tree transition system. The way we will proceed consists in defining, for every tree transition system $\mathbf{T}$ an equivalent LMC $\mathbf{T}^{*}$, then proving that both bisimilarity and testing equivalent in $\mathbf{T}$ and $\mathbf{T}^{*}$ coincide. Given a tree transition system $\mathbf{T}=(Q,S,\mathcal{L},\mathcal{I},\delta,\gamma)$, we define the LMC $\mathbf{T}^{*}$ as the triple $(Q\uplus S,\eta,\mathcal{L}\uplus\mathcal{I}^{*})$ where $\mathcal{I}^{*}=\mathcal{I}\times\mathbb{N}\times\mathbb{N}\cup\mathcal{I}\times\mathbb{N}$ and:

• •

On the states from $Q$, $\eta$ behaves like $\delta$;

• •

For every state $s$ in $S$, we have that

[TABLE]

• •

In all the other cases, $\eta$ returns the empty distribution.

The results from [17] tell us that testing equivalence and bisimilarity coincide in $\mathbf{T}^{*}$, where tests now have the following form:

[TABLE]

and $a\in\mathcal{L}\uplus\mathcal{I}^{*}$. The rest of the proof is thus organised as follows:

• •

We can first of all prove that $\eqsim_{\mathbf{T}}$ and $\eqsim_{\mathbf{T}^{*}}$ coincide. This can be proved by showing that any $\mathbf{T}$-test can be turned into a $\mathbf{T}^{*}$-test having the same probability of success, and vice versa. The two mappings we need can be given as follows, by induction on the structure of tests:

• •

We can then prove that $\sim_{\mathbf{T}}$ and $\sim_{\mathbf{T}^{*}}$ coincide, by proving that each of the two relations is a bisimulation in the sense of the other.

∎

Proposition 6.3**.**

For all BTT context $T[\ ]$ with a hole in BHT, for all $M\in\Lambda^{+}$ there exists a probability distribution $(p_{h})_{h\in\mathrm{hnf}}$ such that for all BHT $U$, $\mathsf{Pr}(T[U],M)=\mathsf{Pr}(T[\omega],M)\sum_{h\in\mathrm{hnf}}p_{h}\mathsf{Pr}(U,h)$.

Proof.

We prove this result, as well as its equivalent for head normal forms and BHT contexts, by induction on test contexts.

For BHT contexts, let $h_{0}\in\mathrm{hnf}$. For the empty context we have $\mathsf{Pr}(U,h_{0})=\mathsf{Pr}(\omega,h_{0})\mathsf{Pr}(U,h_{0})$. For a product $T[\ ]\wedge T^{\prime}$ we apply the induction hypothesis to $T[\ ]$ to get $(p_{h})$ and we have

[TABLE]

The same goes if the hole is on the right side of a conjunction. Finally for a test context of the form $(\lambda\vec{x}.y)(T^{1},\dots,T^{i}[\ ],\dots,T^{m})$, either $\mathsf{Pr}((\lambda\vec{x}.y)(T^{1},\dots,T^{i}[U],\dots,T^{m}),h_{0})=\mathsf{Pr}((\lambda\vec{x}.y)(T^{1},\dots,T^{i}[\omega],\dots,T^{m}),h_{0})=0$ if $h_{0}$ does not have the right shape, or $h_{0}=\lambda\vec{x}.y\ M_{1}\ \dots\ M_{m}$, the induction hypothesis applied to $T^{i}[\ ]$ and $M_{i}$ gives some $(p_{h})$, and we have

[TABLE]

For BTT contexts the cases of $\omega$ and conjunction are similar. The interesting case is that of the evaluation. Given a BTT context $\mathsf{ev}(T[\ ])$ and $M\in\Lambda^{+}$ we apply the induction hypothesis to $T[\ ]$ and every head normal form $h$, or at least any $h$ such that $\mathcal{P}\left(M\rightarrow\mathrel{\mkern-14.0mu}\rightarrow h\right)\neq 0$, to get distributions $(p_{h^{\prime}}^{h})_{h^{\prime}\in\mathrm{hnf}}$. Then we have

[TABLE]

∎

7 Implementing Tests as Resource Terms

There is a very tight correspondence between simple resource terms and Böhm tests, but this correspondence does not hold for all Böhm tests. Simple resource terms can be seen as a particular class of Böhm tests.

Definition 7.1**.**

The classes of resource Böhm term tests (rBTTs) and resource Böhm hnf tests (rBHTs) are given as follows, by mutual induction:

[TABLE]

Definition 7.2**.**

For every rBTT $T$ we define a simple poly-term $\overline{s}_{T}$ and for every rBHT $t$ we define a simple term $s_{t}$ in the following way:

[TABLE]

The similarity between simple resource terms and resource Böhm tests is more than structural: the probability of success of a resource Böhm test is actually given by a coefficient in the Taylor normal form.

Proposition 7.1**.**

For every rBTT $T$ and $M\in\Lambda^{+}$, $!\mathrm{nf}(M^{*})_{\overline{s}_{T}}=\frac{\mathsf{Pr}(T,M)}{\mathrm{m}(\overline{s}_{T_{t}})}$. 2. 2.

For every rBHT $t$ and $h\in\mathrm{hnf}$, $\mathrm{nf}(h^{*})_{s_{t}}=\frac{\mathsf{Pr}(t,h)}{\mathrm{m}(s_{T_{h}})}$.

Proof.

We reason by induction on tests. Observe that these can be considered modulo commutativity and associativity of the conjunction and modulo $\omega\wedge T\simeq T$: these equivalences preserve both the results of testing and the associated simple resource (poly-)terms. Then every rBTT is equivalent either to $\omega$ or to a conjunction $T=\mathsf{ev}(t_{1})\wedge\dots\wedge\mathsf{ev}(t_{k})$. In the first case we always have $!\mathrm{nf}(M^{*})_{[\ ]}=1$. In the second case just like in the proof of regularity of the exponential (Proposition 2.21) for any $M\in\Lambda^{+}$ we have $!\mathrm{nf}(M^{*})_{\overline{s}_{T}}=\frac{1}{\prod_{u\in\Delta}\overline{s}_{T}(u)!}\prod_{i=1}^{k}\mathrm{nf}(M^{*})_{s_{t_{i}}}$. To conclude we want to show that $\mathrm{nf}(M^{*})_{s_{t_{i}}}=\frac{\mathsf{Pr}(\mathsf{ev}(t_{i}),M)}{\mathrm{m}(s_{t_{i}})}$ for all $i\leq k$. We have by definition $\mathsf{Pr}(\mathsf{ev}(t_{i}),M)=\sum_{h\in\mathrm{hnf}}\mathcal{P}\left(M\rightarrow\mathrel{\mkern-14.0mu}\rightarrow h\right)\cdot\mathsf{Pr}(t_{i},h)$, and Proposition 4.5 gives $\mathrm{nf}(M^{*})_{s_{t_{i}}}=\sum_{h\in\mathrm{hnf}}\mathcal{P}\left(M\rightarrow\mathrel{\mkern-14.0mu}\rightarrow h\right)\cdot\mathrm{nf}(h^{*})_{s_{t_{i}}}$, so we conclude by induction hypothesis on $t_{i}$. Now given a rBHT $t=(\lambda\vec{x}.y)(T^{1},\dots,T^{m})$ and $h\in\mathrm{hnf}$ we have either $\mathrm{nf}(h^{*})_{s_{t}}=\prod_{i=1}^{m}!\mathrm{nf}(M^{*}_{i})_{\overline{s}_{T^{i}}}$ and $\mathsf{Pr}(t,h)=\prod_{i=1}^{m}\mathsf{Pr}(T^{i},M_{i})$ if $h$ is of the form $\lambda\vec{x}.y\ M_{1}\ \dots\ M_{m}$, in which case we conclude by induction hypothesis, or $\mathrm{nf}(h^{*})_{s_{t}}=\mathsf{Pr}(t,h)=0$ otherwise. ∎

With this result, we completely characterise Taylor normal forms by resource Böhm tests.

Corollary 7.2**.**

Two terms $M$ and $N$ have the same Taylor normal form iff for every rBTT $T$ it holds that $\mathsf{Pr}(M,T)=\mathsf{Pr}(N,T)$.

Proof.

Simply observe that every simple resource term in normal form is equal to $s_{T}$ for some resource Böhm test $T$. ∎

Thanks to Theorem 5.2 and Corollary 7.2 both Böhm tree equality and Taylor normal form equality are characterised by tests. They still leave a gap in our reasoning, as not all Böhm tests are resource Böhm tests. This difference is not just cosmetic: $\mathsf{ev}(\omega)$ is a valid Böhm test which computes the convergence probability of any $\lambda$-term, which cannot be done using only resource Böhm tests. More precisely this cannot be done using a single Böhm test. To fill the gap between Böhm tests and resource Böhm tests we observe that any of the former can be simulated by a family of resource Böhm tests.

Proposition 7.3**.**

For every BTT $T$ there is a family $(T_{i})_{i\in I}$ of rBTTs of arbitrary size (possibly empty, possibly infinite) such that for all $\lambda$-term $M$ we have $\mathsf{Pr}(T,M)=\sum_{i\in I}\mathsf{Pr}(T_{i},M)$.

Proof.

We prove this, as well as the corresponding result for BHTs, by induction on the size of tests. In the case of BTTs, the result is simply given by induction hypothesis. To the BTT $\omega$ we associate the single-element family $(w)$, to $T\wedge U$ we associate $(T_{i}\wedge U_{j})_{i\in I,j\in J}$ where $(T_{i})_{i\in I}$ and $(U_{j})_{j\in J}$ are given by induction hypothesis on $T$ and $U$, and to $\mathsf{ev}(t)$ we associate $(\mathsf{ev}(t_{i}))_{i\in I}$. The interesting part of the proof is on BHTs, where we want to remove two constructors. Modulo commutativity and associativity of the conjunction and the equivalence $\omega\wedge T\simeq T$, every BHT is either $\omega$ or of the form $(\lambda x_{1}...x_{n_{1}}.y_{1})(T_{1}^{1},\dots,T_{1}^{m_{1}})\wedge\dots\wedge(\lambda x_{1}...x_{n_{k}}.y_{k})(T_{k}^{1},\dots,T_{k}^{m_{k}})$ with $k\geq 1$. In the first case to $\omega$ we associate the family $((\lambda x_{1}\dots x_{n}.y)(\omega^{m}))_{m,n\in\mathbb{N},y\in\mathcal{V}}$ where $\omega^{m}$ denotes the sequence $\omega,\dots,\omega$ of length $m$. In the second case if $m_{i}\neq m_{j}$, $n_{i}\neq n_{j}$ or $y_{i}\neq y_{j}$ for some $i,j\leq k$ then the result of the test is always [math], which is simulated by the empty family of rBHTs. Otherwise let $m=m_{1}$, $n=n_{1}$ and $y=y_{1}$, the test is equivalent to $(\lambda x_{1}\dots x_{n}.y)(T_{1}^{1}\wedge\dots\wedge T_{k}^{1},\dots,T_{1}^{m}\wedge\dots\wedge T_{k}^{m})$. We apply the induction hypothesis to the BTTs $T_{1}^{i}\wedge\dots\wedge T_{k}^{i}$ to get families $(U_{j}^{i})_{j\in J_{i}}$ and we associate the family $((\lambda x_{1}\dots x_{n}.y)(U_{j_{1}}^{1},\dots,U_{j_{m}}^{m}))_{j_{1}\in J_{1},\dots,j_{m}\in J_{m}}$ to the original BHT. ∎

Corollary 7.4**.**

Given two terms $M$ and $N$, for every BTT $T$ it holds that $\mathsf{Pr}(M,T)=\mathsf{Pr}(N,T)$ iff for every rBTT $T$ it holds that $\mathsf{Pr}(M,T)=\mathsf{Pr}(N,T)$.

We can now state the main result of this paper.

Theorem 7.5**.**

Two terms have the same Böhm trees iff their Taylor expansions have the same normal forms.

Proof.

The result follows from Theorem 5.2, Corollary 7.4 and Corollary 7.2. ∎

8 Conclusion

In this paper, we attack the problem of extending the Taylor Expansion construction to the probabilistic $\lambda$-calculus, at the same time preserving its nice properties. What we find remarkable about the defined notion of Taylor expansion is that its codomain is the set of ordinary resource terms, and that the equivalence induced by the Taylor expansion is precisely the one induced by Böhm trees [13]. The latter, not admitting $\eta$, is strictly included in contextual equivalence.

Among the many questions this work leaves open, we could cite the extension of the proposed definition to call-by-value reduction, along the lines of [12], and a formal comparison between the notion of equivalence introduced here and the the one from [15] in which, however, the target language is not the one of ordinary resource terms, but one specifically designed around probabilistic effects.