1. Acknowledgements

\[ \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.

1.1. Alternative title

With thanks to John Power…

“I understood that too”

2. Scott’s P-omega model

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?

2.1. A categorical view (failed)

(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 \} \]

2.2. This doesn’t work!

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.

2.3. Fixing this

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).

2.4. Idea of this talk

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)

3. The relational model of linear logic

1

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!

3.1. Linear logic roots

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

3.2. References

Before

• Ehrhard (2012a) writes that this was “introduced implicitly” by Girard (1988)
• … and that it was folklore in the LL community in the early 1990s.
• It is explicit in Lamarche (1992) Quantitative domains and infinitary algebras [written in 1990]

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)

4. Categorical analysis of the construction

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 \} \]

4.1. Aside: Scott’s model is not like this

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.

4.2. Multiple points of view

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.

4.3. Monoids and relations

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.

5. Weighted relations, quantitative models

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.

5.1. Complete semirings

• \(\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

5.2. Model construction, categorically

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.

5.3. So what are we looking at?

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.

6. Algebraic perspective: polynomials

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.

6.1. Polynomial (semi-)ring

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} \]

6.2. Symmetric algebra

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

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.)

6.3. Beyond free constructions?

Everything above is a free construction.

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

6.4. Algebras are semirings

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 \]

6.5. Constructing algebras

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 \]

6.6. Monoid rings

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.

7. Scott’s model using 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.

7.1. The trouble with idempotence

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

7.2. Characterising algebra homomorphisms

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\).

7.3. Zeros

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\).

7.4. Quotient out the zeros

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.

7.5. Back to powersets

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\).

7.6. Dénouement

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.

7.7. Punchline

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.

7.8. Related

(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.

8. Imperative computation

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\).

8.1. Algebraic viewpoint

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.

8.2. Active expressions

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.

8.3. Passive types

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.

8.4. A/P monoids

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

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\).

8.5. A/P algebras

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.

8.6. Reddy’s refinements

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.

9. Algebraic version of Reddy’s model

• 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 incoherence and multiplying 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!

9.1. Passivity reflection

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\).

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

9.2. Passive subcategory

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

Then passivity-reflection may be expressed as:

10. Conclusions

• 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.

11. Bibliography