Taylor expansion for Imperative Programs

Guy McCusker (University of Bath)

joint work with
Pierre Clairambault and Lionel Vaux-Auclair
(Aix-Marseille Université)

1. Taylor Expansion of Lambda Terms

Ehrhard and Regnier (2003) introduced the Differential Lambda Calculus and with it the Taylor expansion of lambda-terms.

\[ P x = \sum_{n=0}^\infty \frac{1}{n!} (\mathsf{D}^n P \cdot x^n) 0 \]

$\mathsf{D}^n P \cdot x^n$ represents a version of $P$ linearly applied to $n$ occurrences of its argument.

The fully developed Taylor expansion — in which subterms are recursively expanded — can be seen as an infinite sum of linear terms drawn from a resource calculus.

1.1. Differential lambda-calculus

This has led to a great deal of further developments, including:

abstract categorical theory of differential and tangent categories e.g. (Blute, Cockett and Seely)
comparisons with Gödel’s Dialectica interpretation (Kerjean and Pédrot)
redevelopment of the classical theory of lambda-calculus using Taylor expansion (Barbarossa and Manzonetto)
the 2024 Alonzo Church Award.

1.2. In this talk:

Some curiosity-driven exploration of resource calculus and Taylor expansion
A new view on imperative programs

2. Resource Calculus

The resource calculus replaces regular application of lambda-terms $MN$ with a resource-sensitive application:

\begin{eqnarray*} m, n & ::= & x \mid \lambda x.m \mid m \bar{n} \\ \bar{n} & ::= & [n_1, \ldots, n_k] \quad\quad \mbox{a finite multiset of terms} \end{eqnarray*}

Intuition: execution of $MN$ is like execution of $M[N,\ldots,N]$ for some number of copies of $N$.

2.1. Resource calculus reduction

\[ (\lambda x.m)\bar{n} \rightarrow_\beta m[\bar{n}/x] \]

Linear substitution generates a finite sum of terms:

\begin{eqnarray*} x[\bar{n}/x] & = & \left\{\begin{array}{rl} n & \text{if }\bar{n} = [n]\\ \rZero& \text{otherwise} \end{array}\right. \\ y[\bar{n}/x] & = & \left\{\begin{array}{rl} y & \text{if }\bar{n} = []\\ \rZero& \text{otherwise} \end{array}\right. \\ (\lambda y.m)[\bar{n}/x] & = & \lambda y.m[\bar{n}/x]\\ (m\bar{p})[\bar{n}/x] & = & \sum_{\bar n = \bar{n_1} \uplus \bar{n_2}} m[\bar{n_1}/x]\bar{p}[\bar{n_2}/x]\\ ([p_1,\ldots,p_k])[\bar{n}/x] & = & \sum_{\bar n = \bar{n_1} \uplus \ldots \uplus \bar{n_k}} [p_1[\bar{n_1}/x], \ldots, p_k[\bar{n_k}/x]] \end{eqnarray*}

All syntactic operations can be extended to sums via linearity. This includes preservation of $\rZero$, so any zero that appears destroys the whole term.

(Technically we’re working in the free module over the terms, with coefficients drawn from a suitable semiring.)

2.2. Resource calculus behaviour

Reduction is strongly normalizing and (locally) confluent.

Terms can experience starvation e.g. \[ (\lambda x. x[x]) ([\lambda x.x[x], \lambda x.x [x]]) \rightarrow (\lambda x.x[x])[\lambda x.x[x]] \rightarrow \rZero \]

Surfeit also destroys a term: \[ (\lambda x. x[x]) ([\lambda x.x[x], \lambda x.x [x], \lambda x.x [x]]) \rightarrow \rZero \]

2.3. Taylor Expansion

The Taylor expansion of a lambda-term is now readily defined:

\begin{eqnarray*} \mathbf{T}(x) & = & x \\ \mathbf{T}(\lambda x. M) & = & \lambda x. \mathbf{T}(M)\\ \mathbf{T}(MN) & = & \sum_k \frac{1}{k!}\mathbf{T}(M)[\mathbf{T}(N)^k] \end{eqnarray*}

(If using an idempotent semiring — which suffices for our purposes — the rational coefficient can be ignored.)

2.4. Key result: Böhm commutation

Ehrhard and Regnier (2008) demonstrated that normalised Taylor expansions coincide with Taylor-expanded Böhm trees: \[ NF(\mathbf{T}(M)) = \mathbf{T}(\mathbf{BT}(M)). \]

So equivalence of Taylor expansions is the same as equivalence of Böhm trees.

Barbarossa and Manzonetto (2019) used this to redevelop several classical lambda-calculus results using Taylor expansions.

Taylor expansion provides a powerful new approximation theory for the lambda-calculus.

2.5. A semantic view: Relational Semantics

These ideas grew from quantitative semantics of lambda-calculus and linear logic (Girard, 1988).

The simplest variant of quantitative semantics is the relational model:

types = sets
$\sem{A\rightarrow B} = \mathbf{M}_f \sem{A} \times \sem{B}$
terms $x:A \vdash M: B$ = relations between $\mathbf{M}_f A$ and $B$

(Reddy, 1996) described a relational model of imperative programs based on lists rather than multisets.

3. From multisets to lists

A (natural?) question: can we adapt the resource calculus and associated theory to a noncommutative setting, replacing multisets with lists?

(We remark that Tsukada, Asada and Ong (2017) introduced a “rigid” resource calculus, using lists, but subject to permutations; we abandon the permutations and embrace the fixed ordering.)

3.1. First attempt

The syntax looks the same as before, thanks to the magic of overloading.

\begin{eqnarray*} m, n & ::= & x \mid \lambda x.m \mid m \vec{n} \\ \vec{n} & ::= & [n_1, \ldots, n_k] \quad\quad \mbox{a finite list of terms} \end{eqnarray*}

\[ (\lambda x.m)\vec{n} \rightarrow_\beta m[\vec{n}/x] \]

What is the substitution?

3.2. Noncommutative substitution

\begin{eqnarray*} x[\vec{n}/x] & = & \left\{\begin{array}{rl} n & \text{if }\vec{n} = [n]\\ \rZero& \text{otherwise} \end{array}\right. \\ y[\vec{n}/x] & = & \left\{\begin{array}{rl} y & \text{if }\vec{n} = []\\ \rZero& \text{otherwise} \end{array}\right. \\ (\lambda y.m)[\vec{n}/x] & = & \lambda y.m[\vec{n}/x]\\ (m\vec{p})[\vec{n}/x] & = & \sum_{\vec n = \vec{n_1} \cdot \vec{n_2}} m[\vec{n_1}/x]\vec{p}[\vec{n_2}/x]\\ ([p_1,\ldots,p_k])[\vec{n}/x] & = & \sum_{\vec n = \vec{n_1} \cdot \ldots \cdot \vec{n_k}} [p_1[\vec{n_1}/x], \ldots, p_k[\vec{n_k}/x]] \end{eqnarray*}

In contrast to the original resource calculus, the “sums” here are either $\rZero$ or singletons.

3.3. Problem: confluence fails

Confluence is immediately problematic:

3.4. A heavy-handed solution

We can avoid this situation by restricting our syntax.

A linear application rule

\[ \frac{\Gamma \vdash m \quad \Delta \vdash n_i \quad \quad (i = 1, \ldots, k)}{\Gamma, \Delta \vdash m[n_1, \ldots, n_k]} \] prevents variables from occurring in both function and argument.

The resulting calculus is very boring: just linear lambda-calculus. But it is confluent!

3.5. Solution (more interesting)

Perhaps we can restore some interesting computations to the calculus by adding a sequencing construct \[ m \rSeq n \] with an additive style rule \[ \frac{\Gamma \vdash m \quad \Gamma \vdash n}{\Gamma \vdash m \rSeq n} \]

3.6. A noncommutative resource calculus

We can add constants and assertions to obtain a noncommutative resource calculus.

\[ \rM, \rN \inddef \vX \mid \cC \mid \rAbs{\vX}{\rM} \mid \rApp{\rM}{\bN} \mid \rM \rSeq \rN \mid \rAssert{\cC}{\rM} \]

Assertions will allow us to encode conditionals using formal sums: \[ \rAssert{\rTrue}{B} \rSeq M + \rAssert{\rFalse}{B}\rSeq N \] behaves like if-then-else.

3.7. Linear substitution

Linear substitution now works as expected.

Multiple occurrences of a variable are always separated by $\rSeq$ or occur in separate parts of a list: there is a well-defined order.

Linear substitution respects this order.

3.8. Resource calculus reductions

\[ (\lambda x.m)\vec{n} \rightarrow_\beta m[\vec{n}/x] \quad\quad \rSkip \rSeq m \rightarrow m \]

\[ \rAssert{\cC}{\cC} \rightarrow \rSkip \quad\quad \rAssert{\cC}{\cD} \rightarrow \rZero \]

\[ \rAssert{\cC}{(m \rSeq n)} \rightarrow m \rSeq \rAssert{\cC}{n} \]

\[ \frac{m \rightarrow m'}{m \rSeq n \rightarrow m' \rSeq n} \quad\quad \frac{n \rightarrow n'}{m \rSeq n \rightarrow m \rSeq n'} \quad\quad \]

What could this be good for?

3.9. A clue: relational semantics of imperative programs

(Reddy, 1996) pioneered a relational semantics of imperative programs.

His model replaces the multisets of the familiar relational model of linear logic with lists: a non-commutative relational semantics.

It was later shown [M 2002] that this model is fully abstract for a programming language called Basic SCI.

Reddy’s work was an important precursor to the game semantics of local variables [Abramsky & M, 1996].

4. SCI: Syntactic Control of Interference

Reynolds (1978) introduced syntactic control of interference (SCI) as an approach to control of aliasing in imperative programming.

Key idea: functions and their arguments should not share identifiers.

Reynolds used this property to ensure that distinct identifiers never interfere; this enables cleaner reasoning about programs.

Nowadays we see this as a linear (or affine) type system.

SCI is a restricted Idealized Algol. It has an important place in the development of programming language theory.

O’Hearn’s early work on SCI led him to notice the phenomenon doubly-closed categories
… which led to Bunched Implications (O’Hearn and Pym, 1999)
… and hence to Separation Logic (Reynolds, 2002)

4.1. Basic SCI

Basic SCI is a higher-order imperative programming language with local variables and an affine type system.

Types:

\begin{eqnarray*} \sGround & \inddef & \sUnit \mid\sBool \mid \sNat \quad\quad \text{unit, Booleans, natural numbers}\\ \sType{A} & \inddef &\sGround \mid \sType{A} \sFun \sType{B} \end{eqnarray*}

Constants: \[ \sConst{k} \inddef \sSkip \mid \sTrue \mid \sFalse \mid \sConst{i} \]

Syntax:

\begin{eqnarray*} M, N, P & \inddef & x \mid \sAbs{x^A}{M} \mid \sApp{M}{N} \\ & \mid & \sAssign{l}{M} \mid \sDeref{l} \mid \sSeq{M}{N} \mid \sWhile{M}{N} \mid \sNew{l}{M} \\ & \mid & \sConst{k} \mid \sIsZero{M} \mid \sPred{M} \mid \sSucc{M} \mid \sIf{M}{N}{P} \\ \end{eqnarray*}

$l$ ranges over an infinite set of locations.

Note that there is no recursion: a function cannot call itself because \[ f(f(\ldots)) \] violates the linearity constraint.

Type judgements $ \sTypes{\Gamma}{L}{M}{A} $:

\[ \frac{\sTypes{\Gamma}{L}{M}{A \sFun B} \quad\quad \sTypes{\Delta}{L'}{N}{A}} {\sTypes{\Gamma,\Delta}{L,L'}{\sApp{M}{N}}{B}} \]

\[ \frac{\sTypes{\Gamma}{L}{M}{\sUnit} \quad\quad \sTypes{\Gamma}{L}{N}{\sGround}}{\sTypes{\Gamma}{L}{\sSeq{M}{N}}{\sGround}} \]

\[ \frac{\sTypes{\Gamma}{L,l}{M}{\sGround}} {\sTypes{\Gamma}{L}{\sNew{l}{M}}{\sGround}} \]

4.2. Operational semantics

This language can be given a small-step operational semantics: \[ M, \sigma \rightarrow M', \sigma' \] where $\sigma, \sigma'$ are states: functions from locations to integers.

Key reductions: \[ (\lambda x.M)N, \sigma \rightarrow M[N/x], \sigma \]

\[ \sAssign{l}{i}, \sigma \rightarrow \sSkip,\sUpd{\sigma}{l}{i} \]

\[ \sDeref{l},\sigma \rightarrow \sigma(i), \sigma \]

\[ \sNew{l}{M}, \sigma \rightarrow M, \sUpd{\sigma}{l}{0} \]

In the last case the set of available locations grows to include $l$.

4.3. From SCI to resource calculus

We’ll now see how to extend our noncommutative resource calculus to incorporate the ideas from Reddy’s model.

The corresponding Taylor expansion will map SCI terms to sums of resource terms, following the ideas of Reddy’s interpretation.

5. Imperative resource terms

Resource calculus (reminder): \[ \rM, \rN \inddef \vX \mid \cC \mid \rAbs{\vX}{\rM} \mid \rApp{\rM}{\bN} \mid \rM \rSeq \rN \mid \rAssert{\cC}{\rM} \]

To this we add assignment and lookup operations: \[ \rM, \rN \inddef \ldots \mid \rGet{\lL} \mid \rAssign{\lL}{i} \]

Note that the more general $\rAssign{\lL}{\rM}$ can be encoded via sums and asserts as \[ \sum_i \rAssert{i}{\rM}\rSeq \rAssign{\lL}{i} \]

5.1. Imperative resource reductions

We add no more reductions to the calculus!

The calculus is strongly normalizing and (locally) confluent.

So how does it model state? Via the Taylor expansion of local variables.

6. Imperative Taylor Expansion

We can begin to give the Taylor expansion of SCI terms.

A term $M$ will be taken to a formal sum $\mathbf{T}(M)$ of resource terms.

For the lambda-calculus part, the definition appears identical to Ehrhard and Regnier’s:

\begin{eqnarray*} \mathbf{T}(x) & = & x \\ \mathbf{T}(\lambda x. M) & = & \lambda x. \mathbf{T}(M)\\ \mathbf{T}(MN) & = & \sum_k \mathbf{T}(M)[\mathbf{T}(N)^k] \end{eqnarray*}

It is not the same — it is much dumber!

we work with lists rather than multisets
in the application $MN$ there are no identifiers in common between $M$ and $N$
the deterministic nature of our substitution means that no rational coefficients are required, even if we use a non-idempotent semiring

Arithmetic and conditionals are handled using sequencing, assert, and sums:

\begin{eqnarray*} \mathbf{T}(\sPred{M}) & = & \rAssert{0}{\mathbf{T}(M)}\rSeq 0 \\ & + & \sum_{i\in\N}\rAssert{i+1}{\mathbf{T}(M)}\rSeq i\\ \mathbf{T}(\sSucc{M})& = & \sum_{i\in\N}\rAssert{i}{\mathbf{T}(M)}\rSeq i+1 \\ \mathbf{T}(\sIf{M}{N}{P}) & = & \rAssert{\rTrue}{\mathbf{T}(M)}\rSeq\mathbf{T}(N) \\ & + & \rAssert{\rFalse}{\mathbf{T}(M)}\rSeq\mathbf{T}(P) \end{eqnarray*}

Basic imperative constructs:

\begin{eqnarray*} \mathbf{T}(\sSeq{M}{N}) & = & \mathbf{T}(M)\rSeq\mathbf{T}(N)\\ \mathbf{T}(\rGet{l}) & = & \rGet{l}\\ \mathbf{T}(\sAssign{l}{M}) & = & \sum_{i\in\N}\rAssert{i}{\mathbf{T}(M)}\rSeq\rAssign{l}{i} \end{eqnarray*}

We just need to figure out variable allocation…

6.1. Motivating example

Consider the term \[ f: \sUnit \rightarrow \sUnit \vdash^l \sSeq{f(\sAssign{l}{\sDeref{l}+1})}{\sDeref{l}}:\sNat \]

The first terms of its Taylor expansion are

\begin{array}{cl} & & f([])\rSeq \rGet{l} \\ & + & \sum_i f[\rAssert{i}{\rGet{l}}\rSeq \rAssign{l}{i+1}] \rSeq \rGet{l}\\ & + & \sum_{i,j} f[\rAssert{i}{\rGet{l}}\rSeq \rAssign{l}{i+1}, \rAssert{j}{\rGet{l}}\rSeq \rAssign{l}{j+1}] \rSeq \rGet{l}\\ & + & \ldots \end{array}

(after simplifying some assertions.)

Each term contains a single trace of reads and writes to location $l$.

The behaviour of such a term after $l$ is allocated to a cell will be given by:

replacing each $\rGet{l}$ with an appropriate constant, reflecting the last value written
replacing each $\rAssign{l}{i}$ with $\rSkip$

We can perform this replacement using a variant of linear substitution.

6.2. Semantics of local variables

We define an operation of linear substitution of state traces into resource terms.

State traces are sequences of operations: \[ \oOp \inddef \oWI \mid \oRI \]

Given a trace $\trT$ and a location $l$, we define the substitution \[ \rFeed{m}{\lL}{\trT} \] on resource terms.

This substitution represents the result of term $m$, executed in an environment where location $l$ insists on performing the trace $\trT$.

(Compare this to a linear application to a fixed list of inputs.)

The key cases: \[ \rFeed{(\rGet{\lL'})}{\lL}{\trT}\eqdef\left\{\begin{array}{rl} i&\text{if $\trT=\oRI$ and $\lL=\lL'$} \\ \rGet{\lL'}&\text{if $\trT=\emptyword$ and $\lL\not=\lL'$} \\ \rZero&\text{otherwise} \end{array}\right. \]

\[ \rFeed{(\rAssign{\lL'}{i})}{\lL}{\trT}\eqdef\left\{\begin{array}{rl} \rSkip&\text{if $\trT=\oWI$ and $\lL=\lL'$} \\ \rAssign{\lL'}{i}&\text{if $\trT=\emptyword$ and $\lL\not=\lL'$} \\ \rZero&\text{otherwise} \end{array}\right. \]

\[ \rFeed{\cC}{\lL}{\trT}\eqdef\left\{\begin{array}{rl} \cC&\text{if $\trT=\emptyword$} \\ \rZero&\text{otherwise} \end{array}\right. \] \[ \rFeed{x}{\lL}{\trT}\eqdef\left\{\begin{array}{rl} x&\text{if $\trT=\emptyword$} \\ \rZero&\text{otherwise} \end{array}\right. \] \[ \rFeed{(\rAbs{\vX}{\rM})}{\lL}{\trT}\eqdef \rAbs{\vX}{\rFeed{\rM}{\lL}{\trT}} \] \[ \rFeed{(\rApp{\rM}{\bN})}{\lL}{\trT}\eqdef\left\{\begin{array}{rl} \rApp{\rFeed{\rM}{\lL}{\trT}}{\bN}&\text{if $\lL$ is a location of $\rM$} \\ \rApp{\rM}{\rFeed{\bN}{\lL}{\trT}}&\text{if $\lL$ is a location of $\rN$} \end{array}\right. \] \[ \rFeed{\bag{\rM_1,\ldots,\rM_k}}{\lL}{\trT}\eqdef \sum_{\trT=t_1\cdots t_k}\bag{\rFeed{\rM_1}{\lL}{t_1},\dotsc,\rFeed{\rM_k}{\lL}{t_k}} \] \[ \rFeed{(\rM\rSeq \rN)}{\lL}{\trT}\eqdef \sum_{\trT=t_1\cdot t_2}\rFeed{\rM}{\lL}{t_1}\rSeq \rFeed{\rN}{\lL}{t_2} \] \[ \rFeed{(\rAssert{\cC}{\rM})}{\lL}{\trT}\eqdef \rAssert{\cC}{\rFeed{\rM}{\lL}{\trT}} \]

6.3. Taylor expansion of variable allocation

Variable allocation is expanded via substitution of all possible valid traces: those where the reads and writes match up as you would expect. \[ \mathbf{T}(\sNew{\lL}{M}) = \sum_{\trT\in\allValidTr} \rFeed{\mathbf{T}(M)}{\lL}{\trT}. \]

6.4. Back to our example

Recall the term \[ f: \sUnit \rightarrow \sUnit \vdash^l \sSeq{f(\sAssign{l}{\sDeref{l}+1})}{\sDeref{l}}:\sNat \]

with its Taylor expansion

To compute the expansion of \[ f: \sUnit \rightarrow \sUnit \vdash^{\emptyset} \sNew{l}{\sSeq{f(\sAssign{l}{\sDeref{l}+1})}{\sDeref{l}}}:\sNat \] we perform all possible substitutions with valid state-traces, and discard any $\rZero$s that arise.

When $f$ does not invoke its argument, the location is left unchanged: \[ \sum_{\trT\in\allValidTr} \rFeed{(f([])\rSeq \rGet{l})}{l}{\trT} = \sum_{t = \opRead{0}} \rFeed{(f([])\rSeq \rGet{l})}{l}{\trT} = f[]; 0 \]

When $f$ invokes its argument once, the location is incremented once: \[ \sum_{\trT\in\allValidTr} \rFeed{(\sum_i f[\rAssert{i}{\rGet{l}}\rSeq \rAssign{l}{i+1}] \rSeq \rGet{l})}{l}{\trT} = \sum_i f[\rAssert{i}{0}\rSeq\rSkip]\rSeq i+1 \] because the only traces yielding a non-zero substitution are of the form \[ \opRead{0}\opWrite{i+1}\opRead{i+1}. \]

Discarding failed asserts, this is \[ f[\rAssert{0}{0}\rSeq\rSkip]\rSeq 1 \] which reduces to \[ f[\rSkip]\rSeq 1 \]

When $f$ invokes its argument twice, the location is incremented twice:

\begin{eqnarray*} & & \sum_{\trT\in\allValidTr} \rFeed{(\sum_{i,j} f[\rAssert{i}{\rGet{l}}\rSeq \rAssign{l}{i+1}, \rAssert{j}{\rGet{l}}\rSeq \rAssign{l}{j+1}] \rSeq \rGet{l})}{l}{\trT} \\ & = & \sum_{\trT\in\allValidTr} \sum_{i,j} f[\rAssert{i}{0}\rSeq \rSkip, \rAssert{j}{i+1}\rSeq \rSkip] \rSeq j+1 \\ \end{eqnarray*}

This reduces to \[ f[\rAssert{0}{0}\rSeq \rSkip, \rAssert{1}{1} \rSeq\rSkip] \rSeq 2 \] and then to \[ f[\rSkip,\rSkip]\rSeq 2 \]

7. Soundness

The Taylor expansion accurately reflects the operational semantics of SCI:

If $M, \sigma \rightarrow M', \sigma'$ then for every $t' \in \validTr{\sigma'}{-}$ and every $m' \in \mathbf{T}(M')$, there is $m \in \mathbf{T}(M)$ and $t \in \validTr{\sigma}{-}$ such that \[ NF(\rFeed{m}{L}{t}) = NF(\rFeed{m'}{L'}{t'}). \]

This is proved by straightforward induction.

7.1. Adequacy

We can prove an adequacy result: if the Taylor expansion of a closed program is non-zero, the program terminates.

For a program $\vdash^{\emptyset}M:\sUnit$, if $NF(\mathbf{T}(M)) \not = \rZero$ then $M, \sigma \rightarrow^* \sSkip, \sigma'$, where $\sigma$ is the unique state on no locations and $\sigma'$ is some state.

The proof is a typical logical relations argument.

Combining soundness and adequacy with the compositionality of the Taylor expansion we obtain:

For terms $\Gamma \vdash^L M,N:A$ of SCI, if $NF(\mathbf{T}(M)) = NF(\mathbf{T}(N))$ then $M$ and $N$ are observably equivalent.

However, the Taylor expansion is not a fully abstract semantics. For example, in SCI \[ \lambda x.\lambda y. \sSeq{x}{y} \cong \lambda x.\lambda y. \sSeq{y}{x}: \sUnit\rightarrow\sUnit\rightarrow\sUnit \] but their Taylor expansions are clearly different.

8. Summary

We introduced a noncommutative resource calculus which serves as a target of a Taylor expansion of imperative programs.

The calculus is confluent, strongly normalizing, and has no reduction rules for handling imperative behaviour!

Normal forms of the calculus can be seen as basic bricks of approximants to SCI programs.

not discussed: eta-long normal forms denote single elements of Reddy’s relational model

9. Directions

Can we characterise Taylor equivalence? What does it mean for $NF(\mathbf{T}(M)) = NF(\mathbf{T}(N))$?
Passive types: Reynolds’s SCI allowed sharing of identifiers bound to phrases which do not write to the store. Can we develop a hybrid list/multiset resource calculus to incorporate these?
Beyond SCI: can we handle full Idealized Algol similarly? Game semantics provides models of Algol, and the models are differential categories.
Would like to understand the relationship between this account of state and others e.g. algebraic effects

10. Bibliography

Abramsky, S. and McCusker, G., 1996. Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions (extended abstract). Proceedings of 1996 workshop on linear logic, 3. Electronic notes in theoretical computer science. Elsevier, pp.2–14.

Barbarossa, D. and Manzonetto, G., 2019. Taylor subsumes Scott, Berry, Kahn and Plotkin. Proc. acm program. lang. [Online], 4(POPL). Available from: https://doi.org/10.1145/3371069.

Blute, R.F., Cockett, J.R.B. and Seely, R.A.G., 2006. Differential categories. Mathematical. structures in comp. sci. [Online], 16(6), pp.1049–1083. Available from: https://doi.org/10.1017/S0960129506005676.

Ehrhard, T. and Regnier, L., 2003. The differential lambda-calculus. Theoretical computer science [Online], 309(1), pp.1–41. Available from: https://doi.org/https://doi.org/10.1016/S0304-3975(03)00392-X.

Ehrhard, T. and Regnier, L., 2008. Uniformity and the Taylor expansion of ordinary lambda-terms. Theoretical computer science [Online], 403(2-3), pp.347–372. Available from: https://doi.org/10.1016/j.tcs.2008.06.001 [Accessed 29 November 2023].

Girard, J.-Y., 1988. Normal functors, power series and lambda-calculus. Ann. pure appl. logic, 37, pp.129–177.

Kerjean, M.M. and Pédrot, P.-M., 2024. Δ is for Dialectica. Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science [Online]. LICS ’24. New York, NY, USA: Association for Computing Machinery, pp.1–13. Available from: https://doi.org/10.1145/3661814.3662106 [Accessed 12 March 2025].

McCusker, G., 2002. A fully abstract relational model of syntactic control of interference. Proceedings, computer science logic (CSL) 2002, 2471. Lecture notes in computer science. Springer-Verlag, pp.247–261.

O’Hearn, P.W., 1993. A model for syntactic control of interference. Mathematical structures in computer science, 3(4), pp.435–465.

O’Hearn, P.W. and Pym, D.J., 1999. The logic of bunched implications. Bulletin of symbolic logic, 5(2), pp.215–244.

Reddy, U.S., 1996. Global state considered unnecessary: Object-based semantics for interference-free imperative programs. Lisp and symbolic computation, 9(1), pp.7–76.

Reynolds, J.C., 1978. Syntactic control of interference. Conf. record 5th acm symposium on principles of programming languages. pp.39–46.

Reynolds, J.C., 2002. Separation logic: a logic for shared mutable data structures. Seventeenth annual IEEE symposium on logic in computer science (lics 2002). IEEE Computer Society Press, pp.55–74.

Tsukada, T., Asada, K. and Ong, C.-H.L., 2017. Generalised species of rigid resource terms. 2017 32Nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) [Online]. pp.1–12. Available from: https://doi.org/10.1109/LICS.2017.8005093 [Accessed 28 November 2023].

11. Coda: Reddy’s model

The ideas of differential lambda calculus and Taylor expansion grew from quantitative semantics of lambda-calculus and linear logic [Girard 1988].

The simplest variant of quantitative semantics is the relational model:

types = sets
$\sem{A\rightarrow B} = \mathbf{M}_f \sem{A} \times \sem{B}$
terms $x:A \vdash M: B$ = relations between $\mathbf{M}_f A$ and $B$

E.g. \[ \sem{x:\mathbf{Z} \vdash x - x:\mathbf{Z}} = \{ ([n,m], n-m) \mid n,m \in \mathbf{Z}\}. \]

In function application, the argument can provide multiple inputs to the function.

For closed terms: \[ \sem{MN} = \{ b \mid ([a_1, \ldots, a_k], b) \in \sem{M}, a_1, \ldots, a_k \in \sem{N} \}. \] Note that all inputs are drawn from $\sem{N}$ and the order does not matter.

cf. $\mathbf{T}(M)[\mathbf{T}(N)^k]. $

Resource terms provide finer control over the contents of the input bags.

Interpretation of resource calculus terms:

closed term of type $A$ = subset of $A$
bag of closed terms of type $A$ = subset of $\mathbf{M}_f A$.

\[ \sem{[M_1, \ldots, M_n]} = \{ [m_1, \ldots, m_n] \mid m_i \in \sem{M_i} \} \]

Resource terms describe building blocks of the relational semantics.

In some situations, a normal-form resource term denotes a single element of the relational model.

11.1. Reddy’s model of imperative programming

We outline the basic definitions of Reddy’s model of SCI, for comparison.

Types = sets
$\sem{A \rightarrow B} = \sem{A}^* \times \sem{B}$
Terms $x:A \vdash M:B$ = relations between $A^*$ and $B$

The unit type $\sUnit$ is modelled as a singleton set $\{*\}$.

Locations are treated as variables of a special type $\sVars$, modelled as the set of possible read and write actions. \[ \{ \oRI \mid i \in \sNat \} \cup \{ \oWI \mid i \in \sNat \} \]

The term

\[f:\sUnit \rightarrow \sUnit \vdash^{l} \sSeq{f(\sAssign{l}{\sDeref{l}+1})}{\sDeref{l}}: \sNat \] is interpreted as a relation with entries such as

\begin{array}{ccccc} \sUnit & \rightarrow & \sUnit, & \sVars & \vdash & \sNat \\ f: [([*,*], & & *)], & l: [\opRead{i},\opWrite{i+1},\opRead{j},\opWrite{j+1},\opRead{k}], & & k \end{array}

11.2. Semantics of application

As in the relational model of lambda-calculus, the semantics of application of closed terms is easy to describe: \[ \sem{MN} = \{ b \mid ([a_1, \ldots, a_k], b) \in \sem{M}, a_1, \ldots, a_k \in \sem{N} \}. \]

11.3. Semantics of local variables

Semantics of local variable application is similar!

Given \[ \Gamma \vdash^{l} M:\sGround \] we have \[ \sem{\Gamma \vdash^{\emptyset}\sNew{l}{M}} = \{ (s,b) \mid (s,t,b) \in \sem{M}, t\text{ is a valid state trace}\} \]

Recalling our example:

\begin{array}{ccccc} \sUnit & \rightarrow & \sUnit, & \sVars & \vdash & \sNat \\ f: [([**], & & *)], & l: [\opRead{i},\opWrite{i+1},\opRead{j},\opWrite{j+1},\opRead{k}], & & k \end{array}

After allocation of $l$ as a local variable, the only elements in play are those with valid state traces

\begin{array}{ccccc} \sUnit & \rightarrow & \sUnit, & \sVars & \vdash & \sNat \\ f: [([**], & & *)], & l: [\opRead{0},\opWrite{1},\opRead{1},\opWrite{2},\opRead{2}], & & 2 \end{array}

and the final semantics is

\begin{array}{ccccc} \sUnit & \rightarrow & \sUnit & \vdash & \sNat \\ f: [([**], & & *)] & & 2 \end{array}