Krivine Machine and Taylor Expansion in a Non-uniform Setting

TL;DR

This paper extends the Krivine machine to the algebraic lambda-calculus, enabling resource annotations and probabilistic interpretations, with coefficients derived from Taylor expansions.

Contribution

It generalizes the resource-sensitive Krivine machine to algebraic lambda-calculus, linking resource annotations to Taylor expansion coefficients and probabilistic semantics.

Findings

Coefficients in the machine correspond to resource usage probabilities.

Taylor expansion coefficients can recover resource annotations.

The approach applies to probabilistic lambda-calculus models.

Abstract

The Krivine machine is an abstract machine implementing the linear head reduction of lambda-calculus. Ehrhard and Regnier gave a resource sensitive version returning the annotated form of a lambda-term accounting for the resources used by the linear head reduction. These annotations take the form of terms in the resource lambda-calculus. We generalize this resource-driven Krivine machine to the case of the algebraic lambda-calculus. The latter is an extension of the pure lambda-calculus allowing for the linear combination of lambda-terms with coefficients taken from a semiring. Our machine associates a lambda-term M and a resource annotation t with a scalar k in the semiring describing some quantitative properties of the linear head reduction of M. In the particular case of non-negative real numbers and of algebraic terms M representing probability distributions, the coefficient k gives the probability that the linear head reduction actually uses exactly the resources annotated by t. In the general case, we prove that the coefficient k can be recovered from the coefficient of t in the Taylor expansion of M and from the normal form of t.

Tables

Table 1. Table 1: Algebraic equalities of the algebraic λ 𝜆 \lambda -calculus

Algebraic equalities of the $𝕊$-module
$M+\mathrm{𝟎}{\equiv }_{\text{alg}}M$ $\left(M+N\right)+P{\equiv }_{\text{alg}}M+\left(N+P\right)$ $M+N{\equiv }_{\text{alg}}N+M$
$\alpha \left(M+N\right){\equiv }_{\text{alg}}\alpha M+\alpha N$ $\alpha M+\beta M{\equiv }_{\text{alg}}\left(\alpha +\beta \right)M$ $\alpha \left(\beta M\right){\equiv }_{\text{alg}}\left(\alpha \beta \right)M$
$1M{\equiv }_{\text{alg}}M$ $\mathrm{𝟎}M{\equiv }_{\text{alg}}\mathrm{𝟎}$ $\alpha \mathrm{𝟎}{\equiv }_{\text{alg}}\mathrm{𝟎}$
Linear properties
$\lambda x.\left(M+N\right){\equiv }_{\text{alg}}\lambda x.M+\lambda x.N$ $\lambda x.\left(\alpha M\right){\equiv }_{\text{alg}}\alpha (\lambda x.M)$ $\lambda x.0{\equiv }_{\text{alg}}\mathrm{𝟎}$
$\left(\mathrm{𝟎}\right)M{\equiv }_{\text{alg}}\mathrm{𝟎}$ $\left(\alpha M\right)N{\equiv }_{\text{alg}}\alpha \left(M\right)N$ $\left(M+N\right)P{\equiv }_{\text{alg}}\left(M\right)P+\left(N\right)P$

Table 2. Table 2: Breakdown of the execution of the Krivine machine

Algebraic state			Resource state
Term	Env.	Stack	Term	Env.	Stack
$((\lambda x.\left(x\right)x)\lambda x.x)c_0$	$\varnothing$	$\left[\right]$	$⟨⟨\lambda x.⟨x⟩x⟩{(\lambda x.x)}^2⟩c_0$	$e_0$	$\left[\right]$
$(\lambda x.\left(x\right)x)\lambda x.x$	$\varnothing$	$\left[(c_0,\varnothing )\right]$	$⟨\lambda x.⟨x⟩x⟩{(\lambda x.x)}^2$	$e_0$	$\left[(c_0,e_0)\right]$
$\lambda x.\left(x\right)x$	$\varnothing$	$[(\lambda x.x,\varnothing );(c_0,\varnothing )]$	$\lambda x.⟨x⟩x$	$e_0$	$[({(\lambda x.x)}^2,e_0);(c_0,e_0)]$
$\left(x\right)x$	$\{x\mapsto (\lambda x.x,\varnothing )\}$	$\left[(c_0,\varnothing )\right]$	$⟨x⟩x$	$\{x\mapsto ({(\lambda x.x)}^2,e_0)\}$	$\left[(c_0,e_0)\right]$
$x$	$\{x\mapsto (\lambda x.x,\varnothing )\}$	$[(x,\{x\mapsto (\lambda x.x,\varnothing )\});(c_0,\varnothing )]$	$x$	$\{x\mapsto (\lambda x.x,e_0)\}$	$[(x,\{x\mapsto (\lambda x.x,e_0)\});(c_0,e_0)]$
$\lambda x.x$	$\varnothing$	$[(x,\{x\mapsto (\lambda x.x,\varnothing )\});(c_0,\varnothing )]$	$\lambda x.x$	$e_0$	$[(x,\{x\mapsto (\lambda x.x,e_0)\});(c_0,e_0)]$
$x$	$\{x\mapsto (x,\{x\mapsto (\lambda x.x,\varnothing )\})\}$	$\left[(c_0,\varnothing )\right]$	$x$	$\{x\mapsto (x,\{x\mapsto (\lambda x.x,e_0)\})\}$	$\left[(c_0,e_0)\right]$
$x$	$\{x\mapsto (\lambda x.x,\varnothing )\}$	$\left[(c_0,\varnothing )\right]$	$x$	$\{x\mapsto (\lambda x.x,e_0)\}$	$\left[(c_0,e_0)\right]$
$\lambda x.x$	$\varnothing$	$\left[(c_0,\varnothing )\right]$	$\lambda x.x$	$e_0$	$\left[(c_0,e_0)\right]$
$x$	$\left\{x\mapsto (c_0,\varnothing )\right\}$	$\left[\right]$	$x$	$\left\{x\mapsto (c_0,e_0)\right\}$	$\left[\right]$
$c_0$	$\varnothing$	$\left[\right]$	$c_0$	$e_0$	$\left[\right]$

Equations

$${\Lambda }_{\mathbb{S}}:M,N::=x|\lambda x.M|(M)N|\alpha M|M+N|0$$

$$\text{T}(M,E)$$

$$\text{T}(M,E,({\Gamma }_1,\dots ,{\Gamma }_n))$$

$$\Delta :s,t,u::=x|\lambda x.t|⟨t⟩S$$

$${\partial }_x(s,t_1\dots t_n)=\{\begin{array}{ll}\sum _{f\in {\mathfrak{S}}^n}\hat{s}[t_{f(1)}/x_1,\dots ,t_{f(n)}/x_n]& {\text{ if deg}}_x(s)=n\\ 0\in \mathbb{S}⟨\Delta ⟩& {\text{ if deg}}_x(s)\ne n\end{array}$$

$${\partial }_{x_1,\dots ,x_n}(s,T_1,\dots ,T_n)={\partial }_{x_n}(\dots {\partial }_{x_1}(s,T_1),\dots ,T_n)$$

$$\hat{K}(M{)}_t=K(M,\varnothing ,\varnothing {)}_{(t,e_0,\varnothing )}$$

$$\hat{K}((\Delta )I{c}_0)=\{\begin{array}{l}⟨⟨\lambda x.⟨x⟩x⟩(\lambda x.x{)}^2⟩c_0\mapsto 1\\ \_\mapsto 0\end{array}$$

$$\begin{array}{rl}K({\mathbf{S}}_1{)}_{(⟨x⟩x,\{x\mapsto ((\lambda x.x{)}^2,e_0)\},[(c_0,e_0)])}& =K({\mathbf{S}}_2{)}_{(x,\{x\mapsto (\lambda x.x,e_0)\},[(x,\{x\mapsto (\lambda x.x,e_0)\});(c_0,e_0)])}\\ & +K({\mathbf{S}}_2{)}_{(x,\{x\mapsto 1\},[(x,\{x\mapsto ((\lambda x.x{)}^2,e_0)\});(c_0,e_0)])}\\ & +K({\mathbf{S}}_2{)}_{(x,\{x\mapsto ((\lambda x.x{)}^2,e_0)\},[(x,\{x\mapsto 1\});(c_0,e_0)])}\end{array}$$

$$\hat{K}((\Delta )(pI+qF)c_0)=\{\begin{array}{l}⟨\lambda x.⟨x⟩x⟩I^2⟩c_0\mapsto p^2\\ ⟨\lambda x.⟨x⟩1⟩F⟩c_0\mapsto q\\ \_\mapsto 0\end{array}$$

$$((P)Q{)}^{\ast }=\sum _{n=0}^{\infty }\frac{1}{n!}⟨P^{\ast }⟩Q^{\ast n}$$

$$m(x)$$

$$m(\lambda x.t)$$

$$m(⟨t⟩T)$$

$$w(t,\alpha M)$$

$$w(t,M+N)$$

$$m(⟨\lambda x.x⟩(⟨y⟩z^3{)}^2)$$

$$=m(x)2(m(y)3!m(z{)}^3{)}^2$$

$$=2\ast (3!{)}^2$$

$$=2\ast 36=72$$

$$w(⟨x⟩x^3,(x)(2x+y)+(x)(x+z))$$

$$=w(x,x)w(x,2x+y{)}^3+w(x,x)w(x,x+z{)}^3$$

$$=w(x,x)(2w(x,x)+w(x,y){)}^3+w(x,x)(w(x,x)+w(x,z){)}^3$$

$$=2^3+1=9$$

$$M^{\ast }=\sum _{t\in \Delta }\frac{w(t,M)}{m(t)}t$$

$$\hat{K}(M{)}_t=M_t^{\ast }\mathrm{NF}(t{)}_{c_0}$$

Full text

We generalize this resource-driven Krivine machine to the case of the algebraic $\lambda$-calculus. The latter is an extension of the pure $\lambda$-calculus allowing for the linear combination of $\lambda$-terms with coefficients taken from a semiring. Our machine associates a $\lambda$-term $M$ and a resource annotation $t$ with a scalar $\alpha$ in the semiring describing some quantitative properties of the linear head reduction of $M$.

In the particular case of non-negative real numbers and of algebraic terms $M$ representing probability distributions, the coefficient $\alpha$ gives the probability that the linear head reduction actually uses exactly the resources annotated by $t$. In the general case, we prove that the coefficient $\alpha$ can be recovered from the coefficient of $t$ in the Taylor expansion of $M$ and from the normal form of $t$.

1 Introduction

The Krivine machine is an abstract machine implementing the linear head reduction [2] on the pure $\lambda$-calculus. Ehrhard and Regnier gave a resource sensitive version [4] returning the annotated form of a $\lambda$-term accounting for the resources used by the linear head reduction. These annotations take the form of terms in the resource $\lambda$-calculus. As an example, the ordinary term $((\lambda x.(x)x)\lambda x.x)c_{0}$ which reduces to the constant $c_{0}$ is annotated by the following resource term $\langle\langle\lambda x.\langle x\rangle x^{1}\rangle(\lambda x.x)^{2}\rangle c_{0}^{1}$. This resource term informs us that $\lambda x.x$ is used twice during the reduction and $x$ and $c_{0}$ are used once.

We generalize this resource-driven Krivine machine to the case of the algebraic $\lambda$-calculus111This machine has been implemented and is available online at http://allioux.iiens.net/taylor/.. The latter is an extension of the pure $\lambda$-calculus allowing for the linear combination of $\lambda$-terms with coefficients taken from a semiring. Some properties enjoyed by the ordinary $\lambda$-calculus do not hold anymore in the case of the algebraic $\lambda$-calculus and some results become nontrivial. Our machine associates a $\lambda$-term $M$ and a resource annotation $t$ with a scalar $\alpha$ in the semiring describing some quantitative properties of the linear head reduction of $M$. We will only consider terms reducing to a multiple of a constant for the sake of convenience.

In the particular case of non-negative real numbers and of terms $M$ representing probability distributions, the coefficient $\alpha$ gives the probability that the linear head reduction actually uses exactly the resources annotated by $t$. In the general case, we prove that the coefficient $\alpha$ can be recovered from the coefficient of $t$ in the Taylor expansion of $M$ and from the normal form of $t$. A more detailed report concerning this work can be found at http://allioux.iiens.net/taylor/report.pdf.

2 Algebraic lambda calculus

The algebraic $\lambda$-calculus is an extension of the pure $\lambda$-calculus allowing for the linear combination of $\lambda$-terms. More precisely, we endow it with a structure of left $\mathbb{S}$-module where $\mathbb{S}$ is a semiring. We shall follow the presentation of the algebraic $\lambda$-calculus given in [6].

2.1 Grammar

Let $x$ be a variable in $\mathcal{V}$, the set of variables, and let $\alpha$ be a scalar in $\mathbb{S}$. The grammar of the algebraic $\lambda$-calculus is the following:

[TABLE]

We denote $\equiv_{\text{alg}}$ the equivalence relation described in Table 1 making $\Lambda_{\mathbb{S}}$ into a left $\mathbb{S}$-module and providing linear properties to terms. We consider the terms of the quotient set $\Lambda_{\mathbb{S}}/\equiv_{\text{alg}}$ up to $\alpha$-conversion and we call them algebraic terms. We define free variables and $\alpha$-conversion as in [6].

2.2 Algebraic states

The behaviour of the Krivine machine is defined on some structures we call states with which we can associate a unique algebraic term rather than on algebraic terms directly. A state is a snapshot of the abstract machine at a given time and represents the dissection of a unique $\lambda$-term.

Algebraic environment

An algebraic environment is a finite partial function $E$ mapping variables to closures. We introduce the notation $E_{x\mapsto\Gamma}$ to refer to the environment which behaves like $E$ for variables other than $x$ and which maps $x$ to $\Gamma$.

Algebraic closure

An algebraic closure $\Gamma$ is a pair $(M,E)$ composed of an algebraic term $M\in\Lambda_{\mathbb{S}}$ and of an environment $E$ such that $\mathrm{FV}(M)\subseteq\mathrm{Dom}(E)$ where $\text{FV}(M)$ denotes the free variables of $M$ and $\mathrm{Dom}(E)$ denotes the domain of $E$.

Algebraic state

An algebraic state is a nonempty stack of closures. We choose to denote states as triples $(M,E,\Pi)$ where $(M,E)$ is the first closure of the stack and $\Pi$ is the stack of the remaining closures. Indeed, our Krivine machine implementing the linear head reduction, we reduce according to the structure of the first closure and we give it a special status. We refer to the set of the algebraic states by $\mathcal{S}(\Lambda_{\mathbb{S}})$.

The intuition behind algebraic states can be made explicit by defining the function $\text{T}:\mathcal{S}(\Lambda_{\mathbb{S}})\rightarrow\Lambda_{\mathbb{S}}$ which given an algebraic state returns its unique associated algebraic term.

Given any algebraic closure $(M,E)$ and any stack of algebraic closures $\Gamma_{1},\dots,\Gamma_{n}$ with $n\geq 0$, we first define T on closures and then extend it to states as follows:

[TABLE]

2.3 Krivine machine

In this particular section the semiring $\mathbb{S}$ is complete — its sum is infinitary.

We give a description of the Krivine machine as the limit $K$ of the sequence $(K_{n})_{n\in\mathbb{N}}$ defined by induction on $(n,M)$ lexicographically ordered where $n$ is a non-negative integer and $M$ is an algebraic term. The induction on $n$ turns the reduction of $M$ into a finite process even for non-normalizing terms. We also enrich the grammar of the algebraic $\lambda$-calculus with the constant $c_{0}$ as we restrict our study to closed terms reducing to this constant.

• •

$K_{0}(M,E,\Pi)=\mathbf{0}$,

• •

$K_{n+1}(c_{0},E,\emptyset)=c_{0}$,

• •

$K_{n+1}(x,E,\Pi)=K_{n}(E(x),\Pi)$ if $x\in\mathrm{Dom}(E)$,

• •

$K_{n+1}(\lambda x.M,E,\Gamma::\Pi)=K_{n}(M,E_{x\mapsto\Gamma},\Pi)$ assuming $x\notin\mathrm{Dom}(E)$,

• •

$K_{n+1}((M)N,E,\Pi)=K_{n}(M,E,(N,E)::\Pi)$.

These rules, excluding the first two ones, are the ones of the original Krivine machine. As the algebraic $\lambda$-calculus is just an extension of the ordinary $\lambda$-calculus, it suffices to add the two following rules to the description of the Krivine machine to handle it:

• •

$K_{n+1}(\alpha M,E,\Pi)=\alpha K_{n+1}(M,E,\Pi)$,

• •

$K_{n+1}(M+N,E,\Pi)=K_{n+1}(M,E,\Pi)+K_{n+1}(N,E,\Pi)$.

Finally we set $K=\lim_{n\to\infty}K_{n}$.

3 Resource lambda calculus

We recall the syntax and the reduction of the resource $\lambda$-calculus which has been defined in [5]. Indeed, we will define the Taylor expansion of an algebraic term in terms of a sum of resource terms.

3.1 Grammar

The resource $\lambda$-calculus shares its syntax with the ordinary $\lambda$-calculus with the exception that the application takes multisets of terms as argument. We use the multiplicative notation to denote multisets so the multiplicative unit $1$ is the empty multiset. For example $s^{2}t$ is the multiset formed of two occurrences of $s$ and one occurrence of $t$. Multisets are commutative. The multiset union of $S$ and $T$ is denoted $ST$. The multiplicity of an element $t$ in a multiset $T$ is given by $T(t)$. The support of $T$, denoted $\text{supp}(T)$, is the set of elements of $T$ whose multiplicity is nonzero.

The grammar of simple terms in the resource $\lambda$-calculus is:

[TABLE]

where $x,y,\dots\in\mathcal{V}$, the set of variables and where $S$ is a finite multiset of simple terms. We denote the set of simple terms $\Delta$ and we refer to its elements using lower case letters $s,t,\dots$. The set of finite multisets of simple terms is denoted $\Delta^{!}$. We call its elements simple poly-terms and we refer to them using upper case letters $S,T,\dots$. When a term $t$ can either be a simple term or a simple poly-term we say it is in $\Delta^{(!)}=\Delta\cup\Delta^{!}$.

When denoting an application, we use the Krivine notation which we recall: for any simple term $t$ and any simple poly-terms $S_{1},\dots,S_{n}$, we denote the application $\langle\dots\langle t\rangle S_{1}\dots\rangle S_{n}$ by the simplified form $\langle t\rangle S_{1}\dots S_{n}$.

The module $\mathbb{S}\langle\Delta^{(!)}\rangle$ is the set of linear combinations of simple (poly-)terms with coefficients in $\mathbb{S}$. We call its elements (poly-)terms in opposition to simple (poly-)terms which are not part of a linear combination. These combinations can not be expressed in the syntax of the resource $\lambda$-calculus contrarily to the algebraic $\lambda$-calculus. We refer to (poly-)terms using the letters $\mathcal{S},\mathcal{T},\dots$. We denote $\mathcal{S}_{s}$ the coefficient of the (poly-)term $s$ in $\mathcal{S}$. Finally we extend the grammar of the resource $\lambda$-calculus to all (poly-)terms by multilinearity so that: $\lambda x.(t+u)=\lambda x.t+\lambda x.u$, $\langle s+t\rangle T=\langle s\rangle T+\langle t\rangle T$ and $(s+t)T=sT+tT$.

3.2 Linear substitution and reduction

The reduction of the resource $\lambda$-calculus is based on a particular notion of linear substitution. What distinguishes linear substitutions from classical substitutions is that, in the former case, substituted terms have to be used once and only once whereas this restriction does not apply in the latter case.

For a variable $x$ and a term $s$, we define deg${}_{x}(s)$ to be the number of occurrences of $x$ in $s$ and we call it the degree in $x$ of $s$.

Let $\hat{s}$ be the resource term obtained from a resource term $s$ by renaming its different occurrences of $x$ to $x_{1},\dots,x_{n}$ with $n=\mathrm{deg}_{x}(s)$. $\hat{s}$ is such that for all $i\in\llbracket 1,n\rrbracket$, deg${}_{x_{i}}(\hat{s})=1$ and $s=\hat{s}[x/x_{1},\dots,x_{n}]$.

Let $s$ be a simple term and let $t_{1}\dots t_{n}$ be any poly-term with $n$ being a non-negative integer, the linear substitution of $s$ by $t_{1}\dots t_{n}$ is defined as follows:

[TABLE]

with $\mathfrak{S}^{n}$ being the group of permutations on the set $\{1,\dots,n\}$. This construction can be extended to simple (poly-)terms.

We extend this notation to the linear substitution of several variables. For all poly-terms $T_{1},\dots,T_{n}$ with $n$ being a non-negative integer,

[TABLE]

This substitution does not depend on the order of the iterated substitutions as the variables $x_{1},\dots,x_{2}$ are pairwise distincts.

We derive the $\beta$-reduction relation for the resource $\lambda$-calculus from this linear substitution. A redex in the resource $\lambda$-calculus is of the form $\displaystyle\langle\lambda x.s\rangle T$ and reduces as follows: $\langle\lambda x.s\rangle T\rightarrow_{\beta}\partial_{x}(s,T)$.

We extend this relation to $\mathbb{S}\langle\Delta^{(!)}\rangle\times\mathbb{S}\langle\Delta^{(!)}\rangle$ by defining it as being the least relation closed under the following rules, assuming $s\rightarrow_{\beta}\mathcal{S}$ with $s\in\Delta$ and $\mathcal{S}\in\mathbb{S}\langle\Delta\rangle$:

$\hfill\langle s\rangle T\rightarrow_{\beta}\langle\mathcal{S}\rangle T\hfill\langle u\rangle sT\rightarrow_{\beta}\langle u\rangle\mathcal{S}T\hfill\lambda x.s\rightarrow_{\beta}\lambda x.\mathcal{S}\hfill s+u\rightarrow_{\beta}\mathcal{S}+u\hfill\hbox{}$

This relation is confluent and strongly normalizing for $\mathbb{S}=\mathbb{N}$ as proved in [3] and we derive NF, the unique normalization map $\mathbb{N}\langle\Delta^{(!)}\rangle\rightarrow\mathbb{N}\langle\Delta_{0}^{(!)}\rangle$, where $\Delta_{0}$ stands for the set of normal simple terms.

3.3 Resource states

Similarly to the case of the algebraic $\lambda$-calculus, we define resource closures, resource environments and resource states in a mutually recursive fashion.

Resource environment

A resource environment is a total function from the set of variables $\mathcal{V}$ to resource closures. $e_{0}$ is the empty environment mapping any variable in $\mathcal{V}$ to the empty closure $1$. We use the notation $[x\mapsto c]$ to refer to the environment which maps the variable $x$ to the closure $c$ and all the other variables to the closure $1$. Given two environments $e^{\prime}$ and $e^{\prime\prime}$, we define their pointwise concatenation $e^{\prime}e^{\prime\prime}$ such that for all variables $x$, $e^{\prime}e^{\prime\prime}(x)=e^{\prime}(x)e^{\prime\prime}(x)$.

Resource closure

A resource closure is defined as a pair $c=(T,e)$ where $T$ is a simple poly-term and $e$ is a resource environment. A resource closure is said to be elementary when its multiset $T$ is a singleton. The empty closure is $1=(1,e_{0})$. We use letters $c,c_{1},\dots$ for general resource closures and $\gamma,\gamma_{1},\dots$ for elementary resource closures.

Resource state

A resource state is a triple $(t,e,\pi)$ where $(t,e)$ is an elementary resource closure and where $\pi$ is a stack of resource closures. We denote the set of resource states $\mathcal{S}(\Delta)$.

4 Quantitative Krivine machine and Taylor expansion

4.1 Quantitative Krivine machine

In turn we define our quantitative Krivine machine (qKAM) $K$222This machine has been implemented and is available online at http://allioux.iiens.net/taylor/. which draws its inspiration from the one described in [4]. This definition is the main contribution of this paper. It is important to note that for the sake of convenience we will only consider closed algebraic terms which reduce to the constant $c_{0}$. From now on, we therefore enrich the syntax of the resource $\lambda$-calculus with this same constant $c_{0}$.

The following machine computes a coefficient associated with an algebraic state and a resource state. We remind that an algebraic state corresponds to a unique $\lambda$-term and a resource state corresponds to a unique sum of resource terms. Therefore, in the case of algebraic terms whose sums correspond to probability distributions, this coefficient will be the sum of the probabilities that each resource term in the sum describe a resource usage of the reduction of the algebraic term to $c_{0}$.

Definition 4.1**.**

(Quantitative Krivine machine)

The quantitative Krivine machine is defined as a matrix $K\in\mathbb{S}^{\mathcal{S}(\Lambda_{\mathbb{S}})\times\mathcal{S}(\Delta)}$. It is defined by induction on the pair $(\mathrm{size}(t,e,\pi),\mathrm{size}(M,E,\Pi))$333The size of a term is its number of symbols. lexicographically ordered. $K(M,E,\Pi)_{(t,e,\pi)}$ denotes the coefficient in $K$ associated with the pair $((M,E,\Pi),(t,e,\pi))$.

• •

$K(c_{0},E,\emptyset)_{(c_{0},e_{0},\emptyset)}=1$,

• •

$K(x,E,\Pi)_{(x,e,\pi)}=K(E(x),\Pi)_{(e(x),\pi)}$ if $x\in\mathrm{Dom}(E)$ and $e$ is such that $\forall y\neq x,e(y)=1$,

• •

$K(\lambda x.M,E,\Gamma::\Pi)_{(\lambda x.u,e,c::\pi)}=K(M,E_{x\mapsto\Gamma},\Pi)_{(u,e_{x\mapsto c},\pi)}$ if $e(x)=1$ and where w.l.o.g $x\notin Dom(E)$,

• •

$K((M)N,E,\Pi)_{(\langle t\rangle T,e,\pi)}=\sum_{\begin{subarray}{c}(e^{\prime},e^{\prime\prime})\\ e^{\prime}e^{\prime\prime}=e\end{subarray}}K(M,E,(N,E)::\Pi)_{(t,e^{\prime},(T,e^{\prime\prime})::\pi)}$,

The major difference with the case of the ordinary $\lambda$-calculus appears in the following two cases:

• •

$K(\alpha M,E,\Pi)_{(t,e,\pi)}=\alpha K(M,E,\Pi)_{(t,e,\pi)}$,

• •

$K(M+N,E,\Pi)_{(t,e,\pi)}=K(M,E,\Pi)_{(t,e,\pi)}+K(N,E,\Pi)_{(t,e,\pi)}$,

• •

Otherwise $K(M,E,\Pi)_{(t,e,\pi)}=0$.

As we do not want to deal with states directly, we hide them by defining $\hat{K}$ which takes terms instead of states.

Definition 4.2**.**

For any algebraic term $M$ and any resource term $t$,

[TABLE]

This machine is defined for all semirings and in the particular case of $\mathbb{Q}^{+}$ computes a coefficient we shall characterize in Theorem 4.5.

We shall give some examples of execution. Let $\Delta=\lambda x.(x)x,I=\lambda x.x,T=\lambda xy.x$ and $F=\lambda xy.y$. Consider the two examples $(\Delta)Ic_{0}$ and $(\Delta)(pI+qF)c_{0}$, where $p,q\in\mathbb{S}$.

[TABLE]

Table 2 exposes the succession of states taken by the machine which are associated with a nonzero coefficient during the execution of this example. In fact, in this very case all the states have the coefficient 1 in $K$. We shall detail the transition from the $4^{th}$ to the $5^{th}$ state as this is the only one which involves a sum with several summands even though only one of these summands is nonzero.

Let $\mathbf{S}_{1}$ be the algebraic state $((x)x,\{x\mapsto(\lambda x.x,\emptyset)\},[(c_{0},\emptyset)])$ and let $\mathbf{S}_{2}$ be the algebraic state $(x,\{x\mapsto(\lambda x.x,\emptyset)\},[(x,\{x\mapsto(\lambda x.x,\emptyset)\});(c_{0},\emptyset)])$.

Then the transition from the $4^{th}$ to the $5^{th}$ state in Table 2 given by Definition 4.1 is:

[TABLE]

But both $K(\mathbf{S}_{2})_{(x,\{x\mapsto 1\},[(x,\{x\mapsto((\lambda x.x)^{2},e_{0})\});(c_{0},e_{0})])}$ and $K(\mathbf{S}_{2})_{(x,\{x\mapsto((\lambda x.x)^{2},e_{0})\},[(x,\{x\mapsto 1\});(c_{0},e_{0})])}$ are equal to 0 according to Definition 4.1.

That is why we only show the pair of states $(\mathbf{S}_{2},(x,\{x\mapsto(\lambda x.x,e_{0})\},[(x,\{x\mapsto(\lambda x.x,e_{0})\});(c_{0},e_{0})]))$ in Table 2.

We will not give the full breakdown of the execution of the machine for the next example.

[TABLE]

There are two non-deterministic reductions of $(\Delta)(pI+qF)c_{0}$ which lead to $c_{0}$. The first one with multiplicity $p^{2}$ and the second one with multiplicity $q$ which correspond to the two non-deterministic choices induced by the sum $pI+qF$.

4.2 Taylor expansion

In this setting we choose to restrict $\mathbb{S}$, the semiring over which is defined our algebraic $\lambda$-calculus, to any semiring having a multiplicative inverse such as $\mathbb{Q}^{+}$. Taylor expanding an algebraic term then comes down to expanding its applications according to the following formula:

[TABLE]

where $M^{*}$ denotes the Taylor expansion of the algebraic term $M$ and where $Q^{*n}$ is the sum of multisets of cardinality $n$ whose elements are in the support of $Q^{*}$ associated with a coefficient we will not detail here but which can be found in the report.

We justify the terminology “Taylor expansion” by pointing out that in analysis the Taylor series of an infinitely differentiable function $f$ at [math] is $\sum_{n=0}^{\infty}\frac{1}{n!}f^{(n)}(0)x^{n}$. This is, indeed, quite similar to the form of the Taylor expansion of the application in the $\lambda$-calculus. See [3] for more details.

This operation can alternatively be defined by means of coefficients defined inductively on algebraic and resource terms. To this effect, we recall the coefficient $m$ described in [5] accounting for the intrinsic contribution of a resource term $t$ to its coefficient in the Taylor expansion of an algebraic term $M$ and we introduce the weights $w$ which account for the dependance in $M$ of this coefficient.

Definition 4.3**.**

The multiplicity $m$ of a resource term $t$ and the weight $w$ of a resource term $t$ in an algebraic term $M$ are inductively defined as follows:

[TABLE]

The coefficient $m(t)$ corresponds to the number of permutations of variable occurrences of $t$ preserving the name of the variables and letting the term $t$ unchanged. Finally, contrary to the case of the ordinary $\lambda$-calculus, the multiplicity of $t$ in the Taylor expansion of $M$ does not only depend on $t$ but also depends on $M$. The weights $w$ account for this phenomenon and represent one of the contributions of this paper.

We shall give some examples to enlighten the reader about these coefficients.

[TABLE]

As for the weights, their use is motivated by terms of the form $M+N$ and $\alpha M$. Otherwise, if a term $M$ is a pure $\lambda$-term and not an algebraic term then for any $t\in\Delta$, $w(t,M)$ is equal to $1$ if $t\in M^{*}$ and [math] otherwise.

Consider the following example:

[TABLE]

Therefore, there are 9 ways to derive $\langle x\rangle x^{3}$ from $(x)(2x+y)+(x)(x+z)$.

Finally, the expression of the Taylor expansion can alternatively be given by the following definition:

Definition 4.4**.**

(Taylor expansion) Given an algebraic term $M$, its Taylor expansion is:

[TABLE]

It is easy to show this definition leads to an inductive definition of the Taylor expansion on the shape of algebraic terms which is compatible with Equation 6. This motivates our terminology.

4.3 Connection between the qKAM and the Taylor expansion

The following theorem, which is one of the main contributions of this paper, along with the definition of the qKAM, links the behaviour of the qKAM with the Taylor expansion of algebraic terms.

Theorem 4.5**.**

For all algebraic terms $M\in\Lambda_{\mathbb{S}}$, for all resource terms $t\in\Delta$ and provided that $\mathbb{S}$ has a multiplicative inverse,

[TABLE]

where $M_{t}^{*}$ is the coefficient of $t$ in $M^{*}$ and $\mathrm{NF}(t)_{c_{0}}$ is the coefficient of $c_{0}$ in $\mathrm{NF}(t)$.

This theorem is a particular case of a more general result applying to any algebraic state and any resource state. It can be found in the report.

4.4 Computational complexity

At first, it seemed that Theorem 4.5 informed us of an efficient way to compute $K(M,\emptyset,\emptyset)$. Indeed, the Krivine machine reduces $M$ to compute a subset of its Taylor expansion whereas the equation (8) gave hope we could obtain the same result more efficiently as the right-hand side does not involve the reduction of $M$. Although $M^{*}_{t}$ can be computed statically by means of the coefficients $m$ and $w$, it is folklore that determining $\mathrm{NF}(t)_{c_{0}}$ is NP-complete.