(work in progress)

Guy McCusker, University of Bath

\[ \def\coh{\overset{\textstyle\frown}{\smile}} \] My visit to Marseille this month (November 2023) was funded by grants held by Pierre Clairambault and Lionel Vaux Auclair. And we talked about this material a little bit.

Thanks Pierre and Lionel – I’ve had a great time.

I’ve also chatted with Jim Laird (Bath) about some of this material.

With thanks to John Power…

“I understood that too”

Dana Scott, *Data Types as Lattices* (1976):

A continuous function \(f: \mathbf{P}\omega \rightarrow \mathbf{P}\omega\) is determined by the relation \[ \{ (S,n) \mid S \subset_f \omega, n \in f(S) \} \]

Since \(\mathbf{P}_f \omega \times \omega\) is *countable*, such relations can be encoded as sets of naturals.

This gives an embedding \[ (\mathbf{P}\omega \rightarrow \mathbf{P}\omega) \lhd \mathbf{P}\omega \] and hence a model of the \(\lambda\)-calculus.

But how should we understand the construction?

(Try to) define a category as follows:

- Objects: Sets
- Morphisms \(A \rightarrow B\): relations on \(\mathbf{P}_f A \times B\).
- Composition: \(f; g\) given by \[ \{ (\bigcup_i S_i, n) \mid (S_i, n_i) \in f, (\{n_1,\ldots, n_k\},n)\in g \} \]

The enumeration \(\{n_1,\ldots,n_k\}\) is not unique because set union is idempotent.

This means that there is no identity in the definition as given above.

There are lots of ways to fix this problem:

- up-close all the sets;
- more sophisticated closure based on preorders cf. Ehrhard (2012b);
- banish idempotence (coming next);
- something else (coming later).

We’ll explore a range of models of computation which have much in common with this construction.

We try to advocate a view of these categories as the *opposite* of categories of *algebras*.

(cf. Stone duality)

Most of this was presaged by Lamarche (1992)

Take Scott’s idea and replace sets with multisets:

- Objects: Sets
- Morphisms \(A \rightarrow B\): relations on \(\mathbf{M}_f A \times B\).
- Composition: \(f; g\) given by \[ \{ (\biguplus_i S_i, n) \mid (S_i, n_i) \in f, ([n_1,\ldots, n_k],n)\in g \} \]

This works just fine!

- \(\mathbf{Rel}\) is a *-autonomous category = model of MLL.
- finite multiset models the exponential !
- the category described above is the associated Cartesian closed category.

**Before**

**After**

- Models of Differential lambda calculus / LL Ehrhard and Regnier (2003)
- Generalised Species of Structures (Fiore et al., 2008)
- Non-idempotent intersection types (De Carvalho, 2009 explains the connection)

Recall that \(\mathbf{Rel}\) is the Kleisli category for the powerset monad on \(\mathbf{Set}\): relations are maps \(A \rightarrow \mathbf{P}B\).

The opposite category described above can be seen as consisting of functions \[ B \rightarrow \mathbf{P}\mathbf{M}_f A \]

The functor \(\mathbf{P}\mathbf{M}_f\) is a *monad* thanks to a *distributive law of monads*
\[
\mathbf{M}_f \mathbf{P} \rightarrow \mathbf{P}\mathbf{M}_f
\]
mapping
\[
[S_1,\ldots,S_k] \mapsto \{ [a_1,\ldots,a_k] \mid a_i \in S_i \}
\]

The Scott model — using \(\mathbf{P}_f\) rather than \(\mathbf{M}_f\) — cannot be constructed in this way.

There is no distributive law for \(\mathbf{P}_f\) over \(\mathbf{P}\) and in fact no monad structure on \(\mathbf{P}\mathbf{P}_f\) *at all* (Klin and Salamanca, 2018)

Related: Zwart and Marsden (2022) characterise the availability and non-availability of such distributive laws for a range of monads.

This category is:

- the opposite of the Kleisli category for \(\mathbf{P}\mathbf{M}_f\) — cf. Hyland et al., 2006
- the Kleisli category for the cofree cocommutative comonoid on \(\mathbf{Rel}\) — the linear logic view (hat tip: Yves Lafont)
- the opposite of the Kleisli category for \(\mathbf{P}\) on the category of free commutative monoids: morphisms in the underlying category are
*monoid homomorphisms*\[ \mathbf{M}_f B \rightarrow \mathbf{M}_f A \] - the opposite of the category of free commutative monoids on \(\mathbf{Rel}\).

We’ll expand on this last point of view.

Aside: the idea of using relations between monoids underpins Uday Reddy’s relational semantics of *imperative* computation (1996). We’ll see this later if there’s time.

Idea: replace \(\mathbf{P}X = 2^X\) with the monad \(R^X\) where \(R\) is an appropriate structure of *coefficients*:

- a ring
- a semiring
- a
*complete*semiring (allowing infinite sums) - a Σ-semiring (allowing partially-defined infinite sums)

Easy reading: each entry \((M, b)\) in a relation now comes with a coefficient. Coefficients could track:

- number of paths leading to this computation
- cost of computation
- probability of this computation
- etc…

When composing, the coefficient of an entry \((M,c)\) is computed by:

- taking the sum over all ways to produce \((M,c)\)…
- … of product of the coefficients of the \((M_1,b_1),\ldots, (M_n,b_n)\) and \(([b_1,\ldots,b_n],c)\)

(Laird et al., 2013; cf. Ehrhard & Regnier; cf. also Lamarche, obviously).

This is a simplification of Girard’s quantitative semantics, where the coefficients were taken to be sets, and of profunctor models, etc.

- \(\mathbf{B}, \vee, \wedge\): just relations
- \(\mathbf{N}^\infty, +, \times\): count paths
- \(\mathbf{N}^\infty, \min, +\): count shortest path length
- \(\mathbf{R}^\infty, +, \times\): probability

The monad \(\mathbf{M}_f\) distributes over \(R^X\) so we obtain a composite monad \(R^{\mathbf{M}_f X}\).

Yet another viewpoint is that the free commutative monoid construction extends to the Kleisli category for \(R^X\).

This all holds for general, abstract reasons: see e.g. Porst, 2008.

With our preferred view, the model looks like this:

- start with the Kleisli category for \(R^X\); this is the category of
*free \(R\)-modules* - move to the Kleisli category for \(\mathbf{M}_f\) over this: free commutative monoids over free \(R\)-modules.

Monoids in a category of modules are *algebras*.

The fact that relational semantics is based around algebras is not a new observation: it underpins Ehrhard’s development of finiteness spaces, and his work with Regnier on differential lambda-calculus, Taylor expansion etc.

And Lamarche’s paper was entirely based on algebras like the ones we’ll discuss.

But ** I understood that too**. Finally. Although there is lots for me still to understand.

Ehrhard’s line of work profitably uses the viewpoints of linear logic.

We’ll advocate that, sometimes, heading straight for the (opposite of the) Cartesian closed category – as Lamarche did – is helpful, because we can work directly with the algebras.

As we will see, the quantitative relational model may be described as follows:

- Objects: sets
- Maps \(A \rightarrow B\): algebra homomorphisms from the polynomial (or power-series) semiring \(R[B]\) to \(R[A]\).

This gives an alternative view, using arguably more standard mathematics.

A *monomial* over \(A\) is a formal product \(a_1\cdots a_n\) of elements of \(A\), identified up to commutativity.

That is, it is a finite multiset of elements of \(A\).

A *polynomial* is a linear combination
\[
p = \sum_{m \in \mathbf{M}_f A} p_m \cdot m
\]
with each \(p_m \in R\).

(We will typically work with semiring structures that admit *infinite* sums, so we don’t draw a distinction between polynomials and power series. Maybe we should.)

Polynomials form an *algebra*:

- scalar multiplication and addition
- multiplication

\[ (pq)_m = \sum_{m = m_1\cdot m_2} p_{m_1}q_{m_2} \]

The polynomial ring \(R[A]\) is the *symmetric algebra* over the *free module* with basis \(A\).

Perhaps more familiar: \(R[A]\) is the *free commutative monoid* over \(R^A\).

Algebra homomorphisms are module homomorphisms (linear maps) which also preserve multiplication.

So we get natural isomorphisms

\begin{eqnarray*}
\mathbf{Alg}(R[B],R[A]) & \cong & \mathbf{Mod}(R^B,R[A]) \\
& \cong & \mathbf{Set}(B,R^{\mathbf{M}_f A})\\
& \cong & \mathbf{Set}(\mathbf{M}_f A \times B, R)
\end{eqnarray*}

This was the perspective introduced by Lamarche (1992). (Note that when \(R = 2 = \{0,1\}\), \(R^A\) is \(\mathbf{P}A\) and we are in the traditional relational setting.)

Everything above is a *free* construction.

Thought: can we get something interesting by looking at other algebras i.e. by applying some quotients?

There are two equivalent ways to define algebras:

- an \(R\)-algebra \(A\) is a monoid in the category of \(R\)-modules
- an \(R\)-algebra \(A\) is a semiring together with a semiring homomorphism \[ R \longrightarrow A \]

The second view gives us easy access to a way of quotienting our structures: a semiring \(A\) can be quotiented by an *ideal* \(I\) via the *Bourne equivalence* (Bourne, 1951)
\[
x \equiv y \Leftrightarrow \exists i,j\in I. x + i = y+j .
\]

We obtain a new algebra \[ R \longrightarrow A \longrightarrow A/I \]

Another standard algebra construction will come in handy: we can use *any* monoid as the collection of monomials.

The polynomials (power series) \[ \sum_{m\in M} p_m \cdot m \] form an \(R\)-algebra.

Working over the Boolean semiring, Scott’s construction starts to look like the algebra (actually, free module) over the powerset monoid: the free commutative idempotent monoid on a set.

Step back and consider algebras formed from idempotent commutative monoids.

Let \(f:A \rightarrow B\) be an algebra homomorphism and \(a\) any monomial in \(A\).

Because of idempotence in the underlying monoid \[ f(a) = f(a^2) = f(a)^2 \]

Suppose \(f(a) = \sum_i b_i\).

Then we require

\begin{eqnarray*}
f(a) = f(a)^2 & = & (\sum_i b_i)\cdot(\sum_j b_j) \\
& = & \sum_i b_i^2 + \sum_{i\not=j} b_i b_j\\
& = & f(a) + \sum_{i\not=j} b_i b_j
\end{eqnarray*}

The secret to obtaining the *closed* structure in the relational model was freeness: *any* map from singleton-monomials to an algebra generates a well-defined algebra homomorphism.

That is no longer the case; how can we restore it?

Option 1: consider only those elements of our algebras which are *up-closed*: if monomial \(a\) has coefficient 1 then so does \(ab\) for every \(b\).

This leads to a category, but it is still tricky to obtain a closed structure.

Option 2: quotient our algebras so that each \(b_ib_j = 0\).

Consider instead idempotent commutative monoids *with a zero*, which we write as \(\bot\) to avoid clash with the semiring zero.

Form algebras which are sums \(\sum_i a_i\) such that
\[
i \not= j \Rightarrow a_i a_j = \bot
\]
(NB sums are now *partial*).

These algebras will be idempotent — \((\sum_i a_i)^2 = \sum_i a_i\) — if we can ignore \(\bot\).

We don’t want to care about coefficients of zero in our algebra: we want \(a = a + \bot\).

Easy! Quotient out by the ideal generated by \(\bot\).

We can see this algebra as containing sums of non-\(\bot\) elements. Multiplication discards any \(\bot\)s that are generated.

Let’s apply this idea to the Scott-like model and see what we get.

We have to decide which multiplications (unions) in \(\mathbf{P}_f A\) will yield \(\bot\).

To make life easy, just declare that certain pairs of elements \(a\), \(a'\) yield \(\bot\).

As above we generate an algebra whose monomials are the elements of \(\mathbf{P}_f A\) generated by this monoid operation.

What do algebra homomorphisms look like?

We’ll focus on the action of an algebra homomorphism on singletons \[ f(a) = \sum_i S_i \] where each \(S_i \subseteq_f B\).

Write \(a\mathbin f S_i\) when \(S_i\) is in the support of \(f(a)\).

Let’s see what properties this relation has.

Because of the definition of our algebras we have:

- \(a\mathbin f S\) and \(a \mathbin f T\) implies \(S\cdot T = \bot\) or \(S=T\).

If \(a \cdot a'= \bot\) then \(f(a\cdot a') = 0\). So if \(f(a) = \sum_i S_i\) and \(f(a') = \sum_j T_j\) we get \[ \sum_{i,j} S_i \cdot T_j = 0 \] which means each \(S_i \cdot T_j = \bot\).

So we have:

- \(a \cdot a' = \bot\), \(a \mathbin f S\), \(a' \mathbin f T\) implies \(S\cdot T = \bot\).

Write \(a\coh a'\) to mean \(a\cdot a'\not = \bot\).

Note that any set \(S\) appearing as a monomial in our algebra satisfies \[ x, y\in S \Rightarrow x \coh y \]

So the monomials are precisely *cliques*.

Reversing the arrows, to look at the opposite category, the conditions above become:

- \(S \mathbin f a\) and \(T \mathbin f a\) with \(S \coh T\) implies \(S = T\)
- \(S \mathbin f a\) and \(T \mathbin f a'\) with \(S \coh T\) implies \(a \coh a'\)

These are exactly the maps of coherence spaces!

I guess this is not Scott’s model any more.

**Theorem** The category of coherence spaces and stable maps is a full subcategory of the opposite of this category of partial algebras and algebra homomorphisms.

(Other than Lamarche, Ehrhard, Regnier…)

Tsukada and Asada (2022) have also shown how to reconstruct coherence spaces in categories of modules; they construct the linear maps, and find a free commutative comonoid. Their construction appears to be quite different to this one.

Reddy (*Global state considered unnecessary*, 1996) introduced another revolutionary idea.

Stateful computation can be modelled using traces of behaviour, rather than an explicit representation of state.

(This presaged the game semantics of imperative computation.)

In this interpretation, a term such as \[ x:\mathsf{Var}, y:\mathsf{Var} \vdash x:=0; x := !x + 1 ; y := !x :\mathsf{Comm} \] is modelled as a set of (tuples of) traces: \[ \mathsf{write}~0\cdot\mathsf{read}~n \cdot \mathsf{write}~(n+1) \cdot \mathsf{read}~m, \quad\mathsf{write}~m , \quad \checkmark \]

We model the allocation of (local) store to \(x\) by:

- considering only the “good variable” traces in \(x\)
- hiding the action in \(x\)

So the semantics of \[ y:\mathsf{Var} \vdash \mathsf{new}~x~\mathsf{in}~x:=0; x := !x + 1 ; y := !x :\mathsf{Comm} \] contains just \[ \mathsf{write}~1, \quad \checkmark. \]

Reddy defined a *multicategory*. In its simplest form:

- Objects: sets
- Morphisms \(A_1, \ldots, A_n \rightarrow B\): relations on \(A_1^* \times \cdots \times A_n^* \times B\).

(Reddy, 1996) The relational semantics is sound for inteference-controlled Idealised Algol (SCI).

(2002) The relational semantics is fully abstract for SCI with active expressions.

The non-multicategory variant of this construction can be achieved through our algebraic viewpoint:

- Objects: sets
- Morphisms \(A \rightarrow B\): homomorphisms between the
*free algebras*\(2\langle B\rangle\) and \(2\langle A\rangle\).

The free algebra is the noncommutative analogue of the symmetric algebra (polynomial ring): monomials are now finite *sequences* rather than finite multisets.

Active expressions are terms that return values but may affect the store, e.g. the preincrement operator
\[
x := !x + 1; \mathsf{return}~!x
\]
(also known as `++x`

).

Reddy refined the model with a notion of *passive type* where such side-effects cannot happen.

In the syntax, passivity is easy to achieve: simply do not provide access any state-changing operations at passive types.

A consequence is that, in a term such as \[ \Gamma, c : \mathsf{Comm} \vdash M: P \] where \(P\) is passive, we know (intuitively, or via an inductive proof) that the command \(c\) cannot be used.

In the semantics this property will appear as a notion of *passivity reflection*.

Idea: events in the traces are either *active* (state-changing) or *passive* (not state-changing).

Passive events *commute* with one another and are *idempotent*.

An A/P-monoid \(A\) is given by two sets, \(A_a\) and \(A_p\), and is the quotient of the free monoid over \(A_a + A_p\) by the relations

\begin{eqnarray*}
p \cdot p' & = & p' \cdot p \\
p \cdot p & = & p
p\end{eqnarray*}

for \(p,p' \in A_p\).

Concretely this can be described as the monoid of sequences \[ s_0 \cdot \alpha_0 \cdot s_1 \cdots s_n \cdot \alpha_n \] where:

- \(s_i \in A_a^*\) with \(s_i \not = \epsilon\) for \(i\gt0\)
- \(\alpha_i\) ∈ \(\mathbf{P}A_p\) with \(\alpha_i \not = \emptyset\) for \(i \lt n\).

As above, we can construct an algebra over this monoid, using linear combinations \[ \sum_{a\in A} k_a \cdot a \] with coefficients \(k_a\) drawn from some semiring.

Reddy’s description of the model is based on coherence spaces:

- each set \(A_p\), \(A_a\) comes with a coherence structure
- this is extended to traces: \(a_1\cdots a_n \coh b_1 \cdots b_m\) when the first non-equal elements in the sequences are coherent
- the sets \(\alpha_i\) are required to be pairwise coherent
- morphisms are those of coherence spaces
- morphisms are required to reflect passivity: if \((a,b) \in f\) and \(b \in B_p\) then \(a \subset A_p\)

**Observations**

- The algebraic character is lost (and wasn’t really noticed at the time)
- the “monoids” are now partial: incoherent passive elements cannot be multiplied
- an aspect that ought to emerge naturally — passivity reflection — is added by fiat.

- Objects: \((A_a,A_p, \coh)\) as in Reddy’s setup
- Each object generates a monoid of sequences as above, plus a single undefined element \(\bot\)
- From this we generate an algebra as above

- Morphisms: algebra homomorphisms.

WARNING!

There is now a distinction between

incoherenceandmultiplying to zero.

The coherence relation describes when events can appear in parallel while the monoid multiplication puts things together in sequence.

For the passive events, the two coincide.

This needs some study!

In our reverse direction, passivity reflection would mean: given \(b \in B_p\), the support of \(f(b)\) contains only elements made from \(A_p\).

Algebra homomorphisms are passivity reflecting.

For \(b\in B_p\) we have \(b\cdot b = b\). Hence \(f(b) = f(b\cdot b) = f(b)\cdot f(b)\).

Let \(s\) be a minimal sequence in the support of \(f(b)\) that contains an element of \(A_a\). The equation above means that \(s = s' \cdot s'\) for some \(s' \in f(b)\), which is impossible by minimality.

Nice! A desirable semantic property emerges from the homomorphism property in our algebraic view.

We can single out those objects \((\emptyset, A_p)\) where the set of active elements is empty, and immediately notice:

The full subcategory of objects with no active elements is the category of coherence spaces.

Then passivity-reflection may be expressed as:

The inclusion functor from coherence spaces to the opposite of our category of algebras has a left adjoint which maps an object \((A_a,A_p)\) to \((\emptyset, A_p)\).

- Lots of nice relational semantics can be expressed using categories of algebras and algebra homomorphisms
- François Lamarche knew this in the late 1980s
- But there is plenty of scope for working with algebras other than the free ones
- If you pretend hard enough you can convince yourself that coherence spaces are the algebraic fix of Scott’s model
- Much of Reddy’s work can be reproduced in this way, and homomorphisms yield attractive semantic properties; with more to be figured out.

Bourne, S., 1951. The Jacobson Radical of a Semiring. *Proceedings of the national academy of sciences* [Online], 37(3), pp.163–170. Available from: https://doi.org/10.1073/pnas.37.3.163 [Accessed 5 December 2023].

de Carvalho, D., 2009. *Execution Time of lambda-Terms via Denotational Semantics and Intersection Types* [Online]. arXiv. Comment: 36 pages. Available from: https://doi.org/10.48550/arXiv.0905.4251 [Accessed 5 December 2023].

Ehrhard, T., 2012a. Collapsing non-idempotent intersection types. *DROPS-IDN/v2/document/10.4230/LIPIcs.CSL.2012.259* [Online]. Schloss-Dagstuhl - Leibniz Zentrum für Informatik. Available from: https://doi.org/10.4230/LIPIcs.CSL.2012.259 [Accessed 5 December 2023].

Ehrhard, T., 2012b. The Scott model of linear logic is the extensional collapse of its relational model. *Theoretical computer science* [Online], 424, pp.20–45. Available from: https://doi.org/10.1016/j.tcs.2011.11.027 [Accessed 27 November 2023].

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.

Fiore, M., Gambino, N., Hyland, M. and Winskel, G., 2008. The cartesian closed bicategory of generalised species of structures. *Journal of the London Mathematical Society* [Online], 77(1), pp.203–220. Available from: https://doi.org/10.1112/jlms/jdm096 [Accessed 5 December 2023].

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

Hyland, M., Nagayama, M., Power, J. and Rosolini, G., 2006. A category-theoretic formulation of Engeler-style models of the untyped lambda-calculus. *Proc. MCFSIT 2004, electronic notes in theoretical computer science volume 161*. pp.43–57.

Klin, B. and Salamanca, J., 2018. Iterated Covariant Powerset is not a Monad. *Electronic notes in theoretical computer science* [Online], 341, pp.261–276. Available from: https://doi.org/10.1016/j.entcs.2018.11.013 [Accessed 5 December 2023].

Laird, J., Manzonetto, G., McCusker, G. and Pagani, M., 2013. Weighted relational models of typed lambda-calculi. *Proceedings of the 2013 28th annual acm/ieee symposium on logic in computer science* [Online]. LICS ’13. Washington, DC, USA: IEEE Computer Society, pp.301–310. Available from: https://doi.org/10.1109/LICS.2013.36.

Lamarche, F., 1992. Quantitative domains and infinitary algebras. *Theoretical computer science* [Online], 94(1), pp.37–62. Available from: https://doi.org/10.1016/0304-3975(92)90323-8 [Accessed 29 November 2023].

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.

Porst, H.-E., 2008. On Categories of Monoids, Comonoids, and Bimonoids. *Quaestiones mathematicae*, 31(2), pp.127–139.

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.

Tsukada, T. and Asada, K., 2022. Linear-Algebraic Models of Linear Logic as Categories of Modules over σ-Semirings. *Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science* [Online]. Haifa Israel: ACM, pp.1–13. Available from: https://doi.org/10.1145/3531130.3533373 [Accessed 26 November 2023].

Zwart, M. and Marsden, D., 2022. No-Go Theorems for Distributive Laws. *Logical methods in computer science* [Online], Volume 18, Issue 1. Available from: https://doi.org/10.46298/lmcs-18(1:13)2022 [Accessed 5 December 2023].