Differential Lambda Calculus and Resource Taylor Expansion

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

In the term $(\lambda x(x)x)N$ the argument $N$ is used twice, and $\beta$-reduction shows this by copying $N$. The copy destroys the information: after one step the term is $(N)N$, and nothing in it records that the two occurrences came from one argument. A calculus that keeps that record must resolve a prior question — how many copies of $N$ are supplied? — and must do something definite when the supply does not match the demand.

Neither of the two obvious answers works. Forbidding copies altogether, as in the linear discipline of chapter 18, rejects $\lambda x(x)x$ outright, so nothing is learned about it. Allowing copies silently returns us to $\beta$-reduction. The answer developed here supplies a multiset of copies at each application, lets each reduction step consume exactly one copy and place it at exactly one occurrence of the variable, and sums over the possible placements. When the supply and the demand disagree the sum is empty, and the term reduces to $0$.

Two things then have to be proved and one has to be constructed. The placement-and-sum operation is a derivative, and reduction using it must be confluent and terminating, or the calculus computes nothing. That is theorem 181.15. The construction is the passage back: an ordinary $\lambda$-term must be recovered as an infinite linear combination of resource terms, one for each way of fixing the supply, with coefficients that make normalization commute with the decomposition. Those coefficients are factorials, the decomposition is a Taylor expansion, and the exact sense in which it commutes with normalization is stated in theorem 181.23, theorem 181.27.

Differentiating a term

Fix a commutative semiring $R$ of coefficients; for this chapter $R$ is either $\mathbb{N}$ or $\mathbb{Q}$, and the difference matters exactly once, in theorem 181.15. For a set $I$, write $R⟨I⟩$ for the $R$-module of finite formal linear combinations of elements of $I$, and $\mathrm{supp}(\sigma )\subseteq I$ for the set of elements with nonzero coefficient in $\sigma$.

The constructor $\mathsf{D}s\cdot u$ is read: apply $s$ to $u$ once, linearly, leaving the ordinary argument still to come. The next definition is what gives that reading its content.

Three clauses are the product rule and one is not. Abstraction and the function position of an application are linear, so the derivative passes through them. The argument position of an ordinary application is not linear: the argument may be used any number of times. The last clause therefore does not differentiate $v$ in place; it first creates one linear copy of the argument, by replacing $(s)v$ with $(\mathsf{D}s\cdot v)v$, and differentiates that copy. This is the chain rule, and it is the reason $\mathsf{D}$ belongs to the syntax: without a linear application there is no place to put the differentiated copy.

This is Theorem 18 of Ehrhard and Regnier, The Differential Lambda-Calculus, Theoretical Computer Science, volume 309, pages 1–41, 2003, proved there for an arbitrary commutative semiring of coefficients by a parallel-reduction argument. It is imported for exactly the statement displayed: confluence of the untyped calculus. Nothing about normalization, about typed terms, or about the analytic meaning of $\mathsf{D}$ is imported with it, and the chapter’s own normalization result is proved below for the resource fragment, where the argument is short and self-contained.

Resource terms

The differential calculus still contains ordinary application, hence still copies. Deleting ordinary application and keeping only a supply of linear copies gives the fragment in which the counting is exact.

Proof of Lemma 181.8 — Differential substitution is placement

Proof. Induction on $s$. For $s=x$ there is one occurrence and the sum is $u$; for $s=y\ne x$ there is none and the sum is $0$. For $s=\lambda y{s}^{\prime }$ the free occurrences of $x$ in $s$ are those in $s^{\prime }$, and the clause applies $\lambda y$ to each summand given by the induction hypothesis. For $s=⟨s^{\prime }⟩[t_1,\dots ,t_k]$ the occurrences of $x$ are those in $s^{\prime }$ together with those in each $t_i$, and the two clauses of definition 181.7 produce exactly the replacements in $s^{\prime }$ and the replacements in each $t_i$, the latter keeping the other members of the multiset fixed. ◻

Termination and confluence

Proof of Lemma 181.12 — Size strictly decreases

Proof. By induction on the position of the contracted redex, the contextual cases being immediate because size is a sum over the immediate subterms and one summand strictly decreases. Two root cases remain.

For $⟨\lambda xs⟩[]{⇝}_{0}s[0/x]$: the support of the right side is empty or $\{s\}$, and $|⟨\lambda xs⟩[]|=|s|+2$.

For $⟨\lambda xs⟩(u\cdot T){⇝}_0⟨\lambda x(\frac{\partial s}{\partial x}\cdot u)⟩T$: by lemma 181.8 every element of $\mathrm{supp}(\frac{\partial s}{\partial x}\cdot u)$ is $s$ with one occurrence of $x$, of size $1$, replaced by $u$, so it has size $|s|-1+|u|$. Hence every element of the support of the right side has size $$(|s|-1+|u|)+1+\sum _{t\in T}|t|+1=|s|+|u|+\sum _{t\in T}|t|+1,$$ while the left side has size $(|s|+1)+|u|+\sum _{t\in T}|t|+1$, larger by exactly one. ◻

Proof of Lemma 181.13 — Symmetry of the second derivative

Proof. By lemma 181.8, both sides are sums over ordered pairs $(p,q)$ of distinct occurrences of $x$ in $s$, the left side placing $u$ at $p$ and $v$ at $q$, the right side placing $v$ at $p$ and $u$ at $q$. The pairs $(p,q)$ and $(q,p)$ contribute the same simple term to the two sides, since placement at distinct occurrences is independent of order, so the two sums have the same summands. The occurrences are distinct because $x$ is not free in $u$ or in $v$: the first placement removes the occurrence it fills and creates no new one. ◻

Proof of Lemma 181.14 — Reduction commutes with placement

Proof. (ii) is immediate from lemma 181.8: each summand contains one copy of $u$ in some position, and reduction is contextual, so reducing that copy in each summand takes $\frac{\partial s}{\partial x}\cdot u$ to $\frac{\partial s}{\partial x}\cdot \upsilon$ in as many steps as there are summands.

(i) Induction on the position of the redex contracted in $s$. If the redex is inside a subterm not containing the occurrence of $x$ being filled, the two operations act on disjoint positions and commute. The remaining case is the root redex $s=⟨\lambda yr⟩(w\cdot T)$ with $x$ free in $r$, $w$, or $T$. Placing $u$ at an occurrence of $x$ inside $r$ commutes with the reduction because $\frac{\partial }{\partial x}(\frac{\partial r}{\partial y}\cdot w)\cdot u=\frac{\partial }{\partial y}(\frac{\partial r}{\partial x}\cdot u)\cdot w$ when $x\ne y$ and neither variable is free in the other’s argument, which holds by lemma 181.8 for the same reason as lemma 181.13: both sides sum over pairs consisting of an occurrence of $x$ and an occurrence of $y$. Placing $u$ inside $w$ or inside $T$ commutes because those positions are untouched by the reduction, up to the linearity already used in (ii). ◻

Proof of Theorem 181.15 — Church–Rosser and strong normalization

Proof. Strong normalization. Assign to $\sigma \in \mathbb{N}⟨\mathrm{\Delta }⟩$ the finite multiset $\mathrm{sz}(\sigma ):=\{|t|:t\in \mathrm{supp}(\sigma )\}$ of natural numbers. A step $\sigma ⟶{\sigma }^{\prime }$ replaces one element $t$ of the support by the elements of the support of its reduct, each of strictly smaller size by lemma 181.12, and leaves the other elements unchanged. So $\mathrm{sz}({\sigma }^{\prime })$ is strictly smaller than $\mathrm{sz}(\sigma )$ in the multiset order on finite multisets of natural numbers, which is well founded. Hence there is no infinite reduction sequence.

Local confluence. Let $\sigma ⟶{\sigma }_1$ and $\sigma ⟶{\sigma }_2$. By linearity it suffices to treat a simple $s$ in the support with two redex occurrences. If the two occurrences are disjoint, contracting either leaves the other unchanged, and contracting both in either order gives the same term, since reduction is contextual and the contexts do not overlap.

If one occurrence is inside the other, the outer redex is $r=⟨\lambda xp⟩S$ and the inner one lies in $p$ or in a member of $S$. Both cases are lemma 181.14: reducing the inner redex first and then the outer one, or the other way round, reaches the same term, by (i) when the inner redex is in $p$ and by (ii) when it is in a member of $S$.

The remaining overlap is at one redex with two admissible choices of the consumed element: $⟨\lambda xp⟩(u\cdot v\cdot T)$ contracts to $⟨\lambda x(\frac{\partial p}{\partial x}\cdot u)⟩(v\cdot T)$ or to $⟨\lambda x(\frac{\partial p}{\partial x}\cdot v)⟩(u\cdot T)$. One further step from each, consuming the other element, gives $$⟨\lambda x\frac{\partial }{\partial x}(\frac{\partial p}{\partial x}\cdot u)\cdot v⟩T\text{and}⟨\lambda x\frac{\partial }{\partial x}(\frac{\partial p}{\partial x}\cdot v)\cdot u⟩T,$$ which are equal by lemma 181.13. If $S$ is empty there is no choice, and if $S$ is a singleton the two contractions coincide.

Conclusion. For $R=\mathbb{N}$, strong normalization and local confluence give confluence by Newman’s lemma (lemma 40.27), and a confluent terminating relation has unique normal forms. For a general commutative semiring the same local confluence holds, and confluence is then the specialization to this fragment of theorem 181.5. ◻

Taylor expansion

An ordinary $\lambda$-term is now decomposed into resource terms. The decomposition has to choose, at every application, how large a supply to provide; so it is a sum over all choices, and the coefficients must be fixed so that repeated patterns are not counted twice.

Uniformity

Example 181.20 used one fact that is not obvious: distinct elements of $T(M)$ contributed to distinct normal simple terms, so no coefficient was ever formed by adding two contributions. That is the content of the uniformity theorem.

Proof of Lemma 181.22 — Members of an expansion are uniform and pairwise coherent

Proof. Induction on $M$. For $M=x$ both terms are $x$. For $M=\lambda xN$ both are abstractions whose bodies lie in $T(N)$, and the induction hypothesis applies. For $M=(N)P$ we have $t=⟨r⟩S$ and $t^{\prime }=⟨r^{\prime }⟩S^{\prime }$ with $r,r^{\prime }\in T(N)$ and $S,S^{\prime }$ multisets over $T(P)$; the induction hypothesis gives $r⌢r^{\prime }$ and gives coherence of every member of $S$ with every member of $S^{\prime }$, since all of them lie in $T(P)$. ◻

This is Theorem 21 of the authors’ long version of Uniformity and the Taylor Expansion of Ordinary Lambda-Terms by Ehrhard and Regnier, the manuscript retained in this book’s reference library; the published article is [ER08], whose numbering is not assumed to agree with the long version. Its proof rests on the coherence analysis of definition 181.21 together with a quantitative study of normal forms that is not reproduced here. What is imported is exactly the displayed statement: uniqueness of the contributing expansion term, and the value of its coefficient. Nothing is imported about which normal terms arise this way; that is the subject of section 181.6.

Böhm trees and the resource-driven machine

Theorem 181.23 says that a normal resource term is reached from at most one expansion term. It does not say which normal resource terms are reached, nor how to find the expansion term that reaches a given one. Both are answered by the Böhm tree of $M$.

These are Theorems 10 and 11 of [ER06]. The proof of the first constructs a modified Krivine abstract machine that takes an ordinary term $M$, an environment, and a normal resource term $u$, and computes the unique $s\in T(M)$ whose normal form contains $u$; the partial function so obtained is the content of the theorem’s uniqueness clause. The second theorem is a consequence of the first together with the quantitative statement imported as theorem 181.23. Both are imported for exactly the displayed statements; in particular nothing is imported about the complexity of the machine, and the observation in that paper that the number of machine steps measures reduction cost is not used here.

Two bounded comparisons

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 181.5, then exercise 181.6; the implementation project exercise 181.8 may be attempted at any time.

Exercise 181.5¶

★★☆ Prove lemma 181.13 again, this time by induction on $s$ rather than by the occurrence count of lemma 181.8, and identify the case in which the hypothesis $x\notin \mathrm{FV}(u)\cup \mathrm{FV}(v)$ is used. Then give a term $s$ and terms $u,v$ violating that hypothesis for which the two iterated derivatives differ.

Referenced from 3 locations

• Differential Lambda Calculus and Resource Taylor Expansion

Exercise 181.6¶

★★☆ Let $M=(\lambda x(x)(x)x)y$. Compute $T(M)$, determine for which supplies the normal form is nonzero, compute $\mathrm{NF}(M^{\ast })$, and check the coefficient identity of theorem 181.23 for $u=⟨y⟩[⟨y⟩[y^n]]$ by computing $m(t)$ and $m(u)$ separately.

Referenced from 3 locations

• Differential Lambda Calculus and Resource Taylor Expansion

Exercise 181.7¶

★★☆ Exhibit a simple resource term that is not uniform in the sense of definition 181.21, and prove that it belongs to no $T(M)$. Then explain why theorem 181.23 would be false without the restriction to terms of the form $T(M)$, by exhibiting two coherent-but-distinct terms whose normal forms share a summand.

Referenced from 2 locations

• Differential Lambda Calculus and Resource Taylor Expansion

Exercise 181.8¶

★★★ Practical project.resource-taylor-normalizer Implement in Agda or Kappa the resource calculus of definition 181.6, definition 181.9 and its Taylor expansion. Represent simple terms with de Bruijn indices or with names and explicit renaming, poly-terms as sorted multisets, and resource terms as finite maps from simple terms to natural coefficients. Implement: differential substitution $\frac{\partial s}{\partial x}\cdot u$; one reduction step; normalization; the multiplicity $m(t)$ of definition 181.17; and the enumeration of $T(M)$ for an ordinary $\lambda$-term $M$ up to a bound on the size of every supply.

The invariant to maintain is the one proved in lemma 181.8, lemma 181.12: differential substitution produces exactly one summand per free occurrence of the variable, and every summand produced by one reduction step is strictly smaller in the size of definition 181.11, so normalization terminates. The concrete result is a function from an ordinary term and a supply bound to the list of pairs $(t,\mathrm{NF}(t))$ for $t\in T(M)$ within the bound, together with $m(t)$.

Acceptance test. With the terms of this chapter: $⟨\lambda x⟨x⟩[x]⟩[u,v]$ normalizes to $⟨u⟩[v]+⟨v⟩[u]$; the same term with supply $[u]$ or $[u,v,w]$ normalizes to $0$; for $M=(\lambda x(x)x)y$ and supply bound $4$ the tool reports $\mathrm{NF}(t_{n,n+1})=(n+1)!⟨y⟩[y^n]$ and $m(t_{n,n+1})=n!(n+1)!$ for $n\le 3$, and $0$ for every other $t_{n,k}$ within the bound; and the ratio $m(t)/m(u)$ equals the reported coefficient in each nonzero case, which is the instance of theorem 181.23 checked in example 181.24. A mutation of differential substitution that places the argument at every occurrence simultaneously, rather than summing over single placements, must fail the first test by returning $⟨u⟩[u]+\dots$ instead of the displayed sum.

The program computes with finitely many resource terms within a supply bound. It illustrates theorem 181.15, theorem 181.23 and proves neither; in particular it never inspects the infinite sum $M^{\ast }$.

Referenced from 4 locations

• Differential Lambda Calculus and Resource Taylor Expansion

Bibliographic notes