I’m giving a public talk, the second of my Leverhulme Lectures at the International Centre for Mathematical Sciences:

• Life’s struggle to survive. Tuesday September 26, 6 pm UK time. Room G.03 on the ground floor of the Bayes Centre, 47 Potterrow, Edinburgh.

Abstract. When pondering our future amid global warming, it is worth remembering how we got here. Even after it got started, the success of life on Earth was not a foregone conclusion! In this talk I recount some thrilling, chilling episodes from the history of our planet. For example: our collision with the planet Theia, the “snowball Earth events” when most of the oceans froze over, and the asteroid impact that ended the age of dinosaurs. Some are well-documented, others only theorized, but pondering them may give us some optimism about the ability of life to survive crises.

To attend in person, you need to get a free ticket here. Refreshments will be served after the lecture. If you actually show up, say hi!

If you can’t join us, fear not: I should be able to put a recording of the talk on my YouTube channel eventually. And you can already see the slides here. If you find mistakes in them or just have questions, please let me know! I’m still polishing the slides—and the more questions I field now, the more prepared I’ll be when it comes time to give the actual talk.

This week is the 2023 DOE experimental condensed matter physics PI meeting - in the past I’ve written up highlights of these here (2021), here (2019), here (2017), here (2015), and here (2013).  This year, I am going to have to present remotely, however, because I am giving a talk at this interesting conference at the Kavli Institute for Theoretical Physics.  I will try to give some takeaways of the KITP meeting, and if any of the ECMP attendees want to give their perspective on news from the DOE meeting, I’d be grateful for updates in the comments.

The number of groups with $n$ elements goes like this, starting with $n = 0$:

0, 1, 1, 1, 2, 1, 2, 1, 5, …

The number of semigroups with $n$ elements goes like this:

1, 1, 5, 24, 188, 1915, 28634, 1627672, 3684030417, 105978177936292, …

Here I’m counting isomorphic guys as the same.

But how much do we know about such sequences in general? For example, is there any sort of algebraic gadget where the number of gadgets with $n$ elements goes like this:

1, 1, 2, 1, 1, 1, 1, 1, … ?

No! Not if by “algebraic gadget” we mean something described by a bunch of operations obeying equational laws — that is, an algebra of a Lawvere theory.

This follows from a result of László Lovász in 1967:

• László Lovász, Operations with structures, Acta Mathematica Academiae Scientiarum Hungarica 18, (1967) 321–328.

On Mastodon, Omar Antolín sketched a proof that greases the wheels with more category theory. It relies on a rather shocking lemma:

Super-Yoneda Lemma. Let $\mathsf{C}$ be the category of algebras of some Lawvere theory, and let $A, B \in \mathsf{C}$ be two algebras whose underlying sets are finite. If the functors $\mathrm{hom}(-,A)$ and $\mathrm{hom}(-,B)$ are unnaturally isomorphic, then $A \cong B$.

Here we say the functors $\mathrm{hom}(-,A)$ and $\mathrm{hom}(-,B)$ are unnaturally isomorphic if

$$\mathrm{hom}(X,A) \cong \mathrm{hom}(X,B)$$

for all $X \in \mathsf{C}$. We’re not imposing the usual commuting naturality square — indeed we can’t, since we’re not even giving any specific choice of isomorphism!

If $\mathrm{hom}(-,A)$ and $\mathrm{hom}(-,B)$ are naturally isomorphic, you can easily show $A \cong B$ using the Yoneda Lemma. But when they’re unnaturally isomorphic, you have to break the glass and pull out the Super-Yoneda Lemma.

Given this shocking lemma, it’s easy to show this:

Theorem. Let $A, B$ be two algebras of a Lawvere theory whose underlying sets are finite. If $A^k \cong B^k$ for some natural number $k$ then $A \cong B$.

Here’s how. Since $A^k \cong B^k$, we have natural isomorphisms

$$\mathrm{hom}(-,A)^k \cong \mathrm{hom}(-, A^k) \cong \mathrm{hom}(-, B^k) \cong \mathrm{hom}(-,B)^k$$

so for any $X \in \mathsf{C}$ the sets $\mathrm{hom}(X,A)^k$ and $\mathrm{hom}(X,B)^k$ have the same cardinality. This means we have an unnatural isomorphism

$$\mathrm{hom}(-,A) \cong \mathrm{hom}(-,B)$$

The lemma magically lets us conclude that

$$A \cong B$$

Now, how do we use this to solve our puzzle? Let $a(n)$ be the number of isomorphism classes of algebras whose underlying set has $n$ elements. We must have

$$a(n^k) \ge a(n)$$

since we’ve just seen that nonisomorphic algebras with $n$ elements give nonisomorphic algebras with $n^k$ elements. So, for example, we can never have $a(4) \lt a(2)$, since $4 = 2^2$. Thus, the sequence can’t look like the one I showed you, with

$$a(0) = 1, \; a(1) = 1, \; a(2) = 2, \; a(3) = 1,\; a(4) = 1, ...$$

Nice! So let’s turn to the lemma, which is the really interesting part.

I’ll just quote Omar Antolín’s proof, since I can’t improve on it. I believe the ideas go back to Lovász, but a bit of category theory really helps. Remember, $A$ and $B$ are algebras of some Lawvere theory whose underlying sets are finite:

Let $\mathrm{mon}(X, A)$ be the set of monomorphisms, which here are just homomorphisms that are injective functions. I claim you can compute the cardinality of $\mathrm{mon}(X, A)$ using the inclusion-exclusion principle in terms of the cardinalities of $\mathrm{hom}(Q, A)$ for various quotients of $X$.

Indeed, for any pair of elements $x, y \in X$, let $S(x, y)$ be the set for homomorphisms $f \colon X \to A$ such that $f(x) = f(y)$. The monomorphisms are just the homomorphisms that belong to none of the sets $S(x, y)$, so you can compute how many there are via the inclusion-exclusion formula: you’ll just need the cardinality of intersections of several $S(x_i, y_i)$.

Now, the intersection of some $S(x_i, y_i)$ is the set of homorphisms $f$ such that for all $i$, $f(x_i) = f(y_i)$. Those are in bijection with the homorphisms $Q \to A$ where $Q$ is the quotient of $X$ obtained by adding the relations $x_i=y_i$ for each $i$.

So far I hope I’ve convinced you that if $\mathrm{hom}(-, A)$ and $\mathrm{hom}(-, B)$ are unnaturally isomorphic, so are $\mathrm{mon}(-, A)$ and $\mathrm{mon}(-, B)$. Now it’s easy to finish: since $\mathrm{mon}(A, A)$ is non-empty, so is $\mathrm{mon}(A, B)$, so $A$ is isomorphic to a subobject of $B$. Similarly $B$ is isomorphic to a subobject of $A$, and since they are finite, they must be isomorphic.

Beautiful!

But if you look at this argument you’ll see we didn’t use the full force of the assumptions. We didn’t need $A$ and $B$ to be algebras of a Lawvere theory. They could have been topological spaces, or posets, or simple graphs (which you can think of as reflexive symmetric relations), or various other things. It seems all we really need is a category $\mathsf{C}$ of gadgets with a forgetful functor

$$U \colon \mathsf{C} \to \mathsf{FinSet}$$

that is faithful and has some extra property… roughly, that we can take an object in $\mathsf{C}$ and take a quotient of it where we impose a bunch of extra relations $x_i = y_i$, and maps out of this quotient will behave as you’d expect. More precisely, I think the extra property is this:

Given any $X \in \mathsf{C}$ and any surjection $p \colon U(X) \to S$, there is a morphism $j \colon X \to Q$ such that the morphisms $f \colon X \to Y$ that factor through $j$ are precisely those for which $U(f)$ factors through $p$.

Can anyone here shed some light on this property, and which faithful functors $U \colon \mathsf{C} \to \mathsf{FinSet}$ have it? These papers should help:

• Luca Reggio, Polyadic sets and homomorphism counting.

• Anuj Dawar, Tomás Jakl and Luca Reggio, Lovász-Type theorems and game comonads.

• Shoma Fujino and Makoto Matsumoto, Lovàsz’s hom-counting theorem by inclusion-exclusion principle.

but I haven’t had time to absorb them yet.

By the way, there’s a name for categories where the super-Yoneda Lemma holds: they’re called right combinatorial.

And there’s a name for the sequences I’m talking about. If $T$ is a Lawvere theory, the sequence whose $n$th term is the number of isomorphism classes of $T$-algebras with $n$ elements is called the fine spectrum of $T$. The idea was introduced here:

• Walter Taylor, The fine spectrum of a variety, Algebra Universalis 5 (1975), 263–303.

though Taylor used not Lawvere theories but an equivalent framework: ‘varieties’ in the sense of universal algebra. For a bit more on this, go here.

I’m interested in which sequences are the fine spectrum of some Lawvere theory. You could call this an ‘inverse problem’. The direct problem — computing the fine spectrum of a given Lawvere theory — is already extremely difficult in many cases. But the case where there aren’t any equational laws (except trivial ones) is manageable:

• Michael A. Harrison, The number of isomorphism types of finite algebras, Proceedings of the American Mathematical Society 17 (1966), 731–737.

Some errors in Harrison’s paper were corrected here:

• Philip Tureček, Counting finite magmas.

I suspect Harrison and Tureček’s formulas could be nicely derived using species, since they’re connected to the tree-like structures discussed here:

• François Bergeron, Gilbert Labelle and Pierre Leroux, Combinatorial Species and Tree-Like Structures, Cambridge U. Press, Cambridge, 1998.

For all I know these authors point this out! It’s been a while since I’ve read this book.

guest post by Keri D’Angelo, Johanna Maria Kirss and Matina Najafi and Wojtek Rozowski

Long ago, coalgebras of all kinds lived together: deterministic and nondeterministic automata, transition systems of the labelled and probabilistic varieties, finite and infinite streams, and any other arrows $\alpha: X\to F X$ for an arbitrary endofunctor $F:\mathcal{C}\to\mathcal{C}$.

These different systems were governed by a unifying theory of $F$-coalgebra which allowed them to understand each other in their differences and become stronger by a sense of sameness all at once.

However, the land of coalgebra was ruled by a rigid principle. Its name was Behavioural Equivalence, and many felt it was too harsh in its judgement.

Some more delicate transition systems like the probabilistic kinds, found being governed by behavioural equivalence to be unjust towards their nuanced and minute differences, and slowly, diversion began to brew among the peoples.

More and more did the coalgebra find within themselves small distinctions that did not quite outweigh their similarities, and more and more did they feel called to be able to express that in their measurements. The need for a notion of behavioural distance gained momentum, but various paths towards a behavioural distance emerged.

Transition systems as coalgebras

State transition systems are a pervasive object in theoretical computer science. Consider a deterministic finite automaton. The usual textbook definition (see, for example, “Automata and Computability” by Dexter Kozen) of a DFA is a 5-tuple $(Q, \Sigma, \delta : Q \times \Sigma \to Q, F \subseteq Q, q_0 )$ consisting of finite set of states $Q$, an alphabet $\Sigma$, a transition function $\delta : Q \times \Sigma \to Q$, that when given a state $q \in Q$ and a letter $a \in \Sigma$, $\delta(q,a) \in Q$ yields a state that can be obtained by reading a letter $a$ from the alphabet in some state $q$. The subset $F \subseteq Q$ describes a set of states which are accepting and $q_0$ denotes the initial state. The set of words over an alphabet $\Sigma$, which we denote by $\Sigma^{\ast}$ is the least set satisfying the following $$\epsilon \in \Sigma^{\ast} \quad \text{(Empty word } \epsilon \text{ is a word)}$$ $$\text{If }\; a \in \Sigma \;\text{and }\; w \in \Sigma^{\ast} \;\text{then}\; aw \in \Sigma^{\ast} \text{(Concatenating a letter to a word yields a word)}$$

We can now extend the transition function to operate on words. Define $\hat{\delta}: Q \times \Sigma^{\ast} \to Q$ by induction, using the construction of a word: $$\hat{\delta}(q,\epsilon) = q \quad\quad$$ $$\hat{\delta}(q, aw) = \hat\delta(\delta(q,a),w)$$

A word $w$ is accepted by the automaton if $\hat{\delta}(q_0, w) \in F$. The set of all accepted words $\{w \in \Sigma^\ast \mid \hat\delta(q_0,w) \in F\} \in 2^{\Sigma^\ast}$ is called the language of an automaton. The languages that can be accepted by a deterministic automaton with finitely many states are called regular or rational languages.

Now, let’s slightly relax and rearrange the definitions.

First, let’s drop the idea having an initial state. Instead of the language of the automaton, we will now speak of a language $q \in Q$ of a state of an automaton. Every automaton induces a function $\dagger : Q \to 2^{\Sigma^{\ast}}$ which is given by $q \mapsto \{ w \in \Sigma^\star \mid \hat\delta(q,w) \in F\}$, and the set $\dagger(q)$ is called the language of the state $q$.

We can view the set of accepting states, as a function $o : Q \to 2$ to the two-element set, such that $o(q)=1 \Leftrightarrow q \in F$. Currying the transition function yields $\delta : Q \to Q^\Sigma$. Now, we can use cartesian product and combine the functions $o$ and $\delta$ into a function $\langle o, \delta\rangle : Q \to 2 \times Q^\Sigma$. Intuitively, such function takes a state to its one-step observable behaviour. Finally, we will drop the requirement of the set of states to be finite. Automata with infinitely many states can denote more expressive langauges from the Chomsky hierarchy, such as Context-Free Languages.

Each deterministic automaton can be now viewed as a pair $(Q, \alpha : Q \to 2 \times Q^\Sigma)$. More interestingly, we can endow the set of all languages $2^{\Sigma^{\ast}}$ with the structure of a deterministic automaton. Define the acceptance function $\epsilon ? : 2^{\Sigma^{\ast}} \to 2$ to be given by $\epsilon ? (L) = 1 \Leftrightarrow \epsilon \in L$. In other words, a language will be an accepting state if and only if it contains the empty word. Now, define a transition function $(-)_a : 2^{\Sigma^{\ast}} \times \Sigma \to {2^{\Sigma^{\ast}}}$ to be given by $(L)_a=\{w \mid aw \in L\}$. Intuitively given a language $L$ and a letter $a$, we transition to a language obtained by cutting that letter from words that start with $a$ in the original language. The transition structure $\langle \epsilon ? , (-)_a \rangle$ is often called the semantic Brzozowski derivative, and the automaton $2^{\Sigma^{\ast}} \to 2\times (2^{\Sigma^{\ast}})^\Sigma$ is called the (semantic) Brzozowski automaton.

It can be observed that the Brzozowski automaton provides a form of a universal automaton in which every other deterministic automaton embeds in a well-behaved way. By well-behaved, we mean the following: - if a state $q\in Q$ in some automaton accepts, then its language $\dagger(q)$ contains an empty word, and so the language is an accepting state in the Brzozowski automaton, - if a state transitions to an another state on some letter $a\in \Sigma$, then in the Brzozowski automaton, the language of the first state transitions to the language of the second state on the same letter $a$.

Formally speaking, let $\langle o , \delta \rangle : Q \to 2 \times Q^\Sigma$ be a deterministic automaton with $Q$ being the set of states. The function $\dagger_{\langle o,\delta\rangle} : Q \to 2^{\Sigma^{\ast}}$ taking each state to its language satisfies the following for all $q \in Q$: - $o(q)=\epsilon?(\dagger_{\langle o,\delta\rangle}(q))$, - for all $a \in \Sigma$, $\left(\dagger_{\langle o,\delta\rangle}(q)\right)_a=\dagger_{\langle o,\delta\rangle}\left(\delta(a,q)\right)$.

In other words, the map $\dagger_{\langle o, \delta\rangle}$ to the Brzozowski automaton is structure-preserving. More generally, functions between any two deterministic automata satisfying the condition above are called homomorphisms. One can easily show that the Brzozowski automaton satisfies a certain universal property, namely that every other deterministic automaton admits a unique homomorphism to it (which is precisely the map which assigns to a state its language). We can use the Brzozowski automaton and language-assigining map to talk about the behaviour of states – we will say that two states are behaviourally equivalent if they are mapped to the same language in the Brzozowski automaton.

To sum up, the set of languages equipped with an automaton structure provides a universal and fully abstract treatment of the behaviours of states of deterministic automata.

Now, consider a different object of study within theoretical computer science and logic: Kripke frames. The usual way one gives the semantics of modal logic is through Kripke frames. A Kripke frame is a pair $(W, R \subseteq W \times W)$ consisting of a set of worlds $W$ and an accessibility relation $R \subseteq W \times W$. A valuation $v : W \to \mathcal{P}({AP})$ is a function, which assigns to each world a set of atomic propositions which are true in it. A Kripke frame along with a valuation forms a Kripke model. Given two Kripke models $((W_1, R_1 \subseteq W_1 \times W_1), v_1)$ and $((W_2, R_2 \subseteq W_2 \times W_2), v_2)$, we call a map $f : W_1 \to W_2$ a $p$-morphism if the following conditions hold: - if $u R_1 v$, then $f(u) R_2 f(v)$, - if $s R_2 t$ for some $s = f(u)$, then $u R_1 w$ and $t=f(w)$ for some $w \in W_1$, - $p \in v(w)$ if and only if $p \in v(f(w))$. domae $p$-morphisms are well-behaved morphisms preserving the structure of Kripke models (and hence the validity of modal formulae), and are thus somewhat similar in spirit to the homomorphisms between deterministic automata.

Observe that an accessibility relation $R \subseteq W \times W$ on a set of worlds can be viewed equivalently as a function $W \to \mathcal{P}(W)$. Similarly to deterministic automata, we can use the Cartesian product to combine seuthe accessibility relation and the valuation in a frame into a function $\langle R,v\rangle:W \to \mathcal{P}(W) \times \mathcal{P}({AP})$ which takes a world to its one-step observable behaviour. A Kripke model then becomes a pair $(W, \alpha : W \to \mathcal{P}(W) \times \mathcal{P}(AP))$.

Both deterministic automata and Kripke frames are pairs consisting of a set of states, and a one-step transition function which takes a state into some set-theoretic construction describing its bservable behaviour. These set-theoretic constructions are endofunctors $\mathsf{Set} \to \mathsf{Set}$, in our case $2 \times (-)^\Sigma$ and $\mathcal{P}(-) \times \mathcal{P}(AP)$. Deterministic automata and Kripke frames are concrete instances of coalgebras for an endofunctor.

Let’s spell out the concrete definitions.

Let $F : \mathcal{C} \to \mathcal{C}$ be an endofunctor on some category. An $F$-coalgebra is a pair $(X, \alpha : X \to F X)$ consisting of an object $X$ of category $\mathcal{C}$ and an arrow $\alpha : X \to F X$.

A homomorphism from $F$-coalgebra $(X, \beta)$ to $(Y, \gamma)$ is a map $f: X \to Y$ satisfying $\gamma \circ f = Ff \circ \beta$. Homomorphisms of deterministic automata and $p$-morphisms are the concrete instatiations of this definition.

Coalgebras and their homomorphisms form a category. Under an approriate size restrictions on the functor $F$, there exists a final coalgebra $(\nu F, t)$, which is a final object in the category of coalgebras. In other words, it satisfies the universal property that for every $F$-coalgebra $(X,\beta)$ there exists a unique homomorphism $\dagger \beta : X \to \nu F$. Final coalgebras provide a abstract domain providing denotation of the behaviour of $F$-coalgebras. We already saw that in the case of deterministic automata, Brzozowski automaton provided a final coalgebra, where formal langauges denoted the behaviour of states of automata. Finally, the concrete notion of behavioural equivalence was given by language equivalence.

Behavioural equivalence of quantitative systems

Having introduced the motivation for the study of coalgebras, we move on to a particular example, which will motivate looking at behavioural distance. Consider an endofunctor $\mathcal{D} : \mathsf{Set} \to \mathsf{Set}$, which takes each set $X$ to the set $\mathcal{D} X = \{\mu : X \to [0,1] \mid \sum_{x \in X} \mu(X) = 1\}$ of discrete probability distributions over $X$. On arrows $f : X \to Y$, we have that $\mathcal{D} f : \mathcal{D}X \to \mathcal{D}Y$ is given by $\mathcal{D} f (\mu)(y) = \sum_{f(x) = y} \mu(x)$, also known as the pushforward measure. Coalgebras for $\mathcal{D}$ are precisely Discrete Time Markov chains. Since all the states in such a case have no extra observable behaviour besides the transition probability, it turns out that all the states are behaviourally equivalent. Let’s consider a slightly more involved example, where each state can also be terminating with some probability.

Consider a composite functor $\mathcal{D}(1 + (-))$ that takes a set $X$ to $\mathcal{D}(\{\ast\}\cup X):=\mathcal{D}(1+X)$. Coalgebras for it can be thought of Markov Chains with potential deadlock behaviour. Now, let’s look at a concrete example of a four state automaton

State $z$ enters deadlock with probability $1$, while state $u$ has a self loop with probability $1$. The functor $\mathcal{D}(1 + (-))$ admits a final coalgebra and it is not too hard to observe that states $u$ and $z$ exhibit completely different behaviour and will be mapped into distinct elements of the carrier of final coalgebra. State $y$ has $\frac{1}{2}$ probability of ending in $u$ and $\frac{1}{2}$ probability of ending in $z$. It has two equiprobable options of tranisitioning to states, which behave in a different way from eachother. It is not too hard that $y$ is also not behaviourally equivalent to $u$ and $z$. Finally, consider the state $z$. Let $\epsilon \in [0, \frac{1}{2}]$. State $x$ can transition to $u$ with probability $\frac{1}{2} - \epsilon$ and transition to $z$ with probability $\frac{1}{2} + \epsilon$. Observe that only when $\epsilon=0$ state $x$ is behaviourally equivalent to $y$. Even for very small non-zero values of $\epsilon$, states $x$ and $y$ would be considered inequivalent.

For practical purposes, coalgebraic behavioural equivalence (for coalgebras on $\mathsf{Set}$) might be way too restrictive. In the case of systems exposing quantitative effects, it would be more desirable to consider a more robust notion of behavioural distance, which would quantify how similarly two states behave. The abstract idea of distance has been captured by mathematical notion of metric spaces and related objects.

Pseudometrics and $\mathsf{PMet}$

Underlying the behavioural distance between states of a coalgebra is the mathematical idea of distance. Most commonly, distance is treated in the form of a metric space. A metric space is a set $X$ with a distance function $d:X\times X\to [0,\infty)$ that satisfies the following axioms for each $x,y\in X$. - Separation: $d(x,y)=0\iff x=y$. - Symmetry: $d(x,y)=d(y,x)$, - Triangle inequality: $d(x,z)\leq d(x,y)+d(y,z)$.

In the context of coalgebras, however, we may wish to have a slightly altered notion of distance to capture behavioural similarity.

If two states behave identically, then even if they are not the same state, we expect their distance to be zero. Thus, we relax the separation axiom and only require that $d(x,x)=0$ for all $x\in X$. This yields a pseudometric. Note that a pseudometric is still symmetric and still fulfills the triangle inequality. It is also possible to have an asymmetric notion of distance, where both separation and symmetry are relaxed. The distance function obtained like that is a function $d:X\times X\to [0,\infty)$ that only fulfills the triangle inequality, but it is possible that $d(x,y)=0$ and $d(x,y)\neq d(y,x)$ for some $x\neq y$. This is called a hemimetric, and it occurs when formalising distance via fuzzy lax extensions.

Finally, we may wish to bound the distance, to have a way of expressing when two states are “maximally different”. For example, we use this to express that an accepting and a non-accepting state are maximally different. In order to accommodate that, we instead define the distance function as $d:X\times X\to [0,\top]$, where $\top \in (0,\infty]$. In the context of behavioural distances on coalgebra, it is common to take $\top = 1$ or $\top = \infty$. However, in the case of $\top = \infty$, this requires a way of calculating with infinity, and this is resolved by defining distance and addition with infinity as $$d(x,\infty) = \infty,\: x\neq \infty; \quad d(\infty,\infty)=0;\quad x+ \infty = \infty,\: x\in [0,\infty].$$

Once we fix the bound $\top$ and some set $X$, we can consider the set $\mathsf{PMet}(X)$ of all pseudometrics $d$ over $X$. It turns out that under the pointwise order and appropriate definitions of meet and join, $\mathsf{PMet}(X)$ becomes a lattice. In particular, the order is given by $$d_1 \leq d_2 \iff d_1(x,y)\leq d_2(x,y) \quad\forall x,y\in X,$$ and for a subset $D\subseteq \mathsf{PMet}(X)$, $$(\sup D)(x,y) := \sup \{d(x,y)\mid d\in D\},\quad\inf D := \sup \{d\mid d \in \mathsf{PMet}(X) \land \forall d'\in D. d\leq d'\}.$$

Moreover, it is a complete lattice, meaning each subset has a meet and a join. The lattice being complete implies that the category of all pseudometric spaces for a fixed $\top$ is complete and cocomplete, which in turn implies that the category has products and coproducts.

Here’s how we define this category of pseudometric spaces:

The category $\mathsf{PMet}$ for a fixed $\top\in (0,\infty]$ has - pseudometric spaces $(X,d_X)$ as objects, - nonexpansive maps $f:(X,d_X)\to (Y,d_Y)$ as morphisms.

The definition of nonexpansive maps is quite immediate: $$d(f(x),f(y))\leq d(x,y)\quad \forall x,y\in X,$$ i.e. the maps do not increase distances between elements. Clearly, the composition of nonexpansive maps is nonexpansive as well, and the identity map is nonexpansive.

Motivation from transportation theory

In the long run, we would like to be able to go from distances on the states of coalgebra to distances on observable behaviours. For now, let’s focus our attention on the discrete distributions functor. Let $X$ be a set equipped with a $\top$-pseudometric structure on it, given by $d_X : X \times X \to [0, \top]$ and let’s say we have two distributions $\nu, \mu \in \mathcal{D}X$. We would like define a pseudometric structure $d_{\mathcal{D} X} : \mathcal{D}X \times \mathcal{D}X \to [0,\top]$ which would allow us to calculate the distance between $\nu$ and $\mu$.

It turns out, there is well-known answer to this question, coming from the field of transportation theory. Let’s make the example slightly more concrete. Let $X = \{A,B,C\}$ and from now on we will omit the subscript on the map $d_X :X \times X \to [0,\top]$

Imagine that $A, B$ and $C$ are three bakeries with an adjacent shop where one can taste the pastries. We have that $d(A,A)=d(B,B)=d(C,C)=0$. Moreover, let’s say that distance between $A$ and $B$ is three ($d(A,B)=d(B,A)=3$), while $B$ and $C$ are in distance four ($d(B,C)=d(C,B)=4$) and $A$ and $C$ are in distance five ($d(A,C)=d(C,A)=5$). Hence, $d$ is a metric space.

Let $\nu \in \mathcal{D} X$ be the distribution of supply of the pastries in each of the bakeries. $\nu(A) = 0.7$, $\nu(B)=0.1$ and $\nu(C)=0.2$

Let $\mu \in \mathcal{D} X$ be the distribution of demand in pastry shops adjactent by the bakeries. We have that $\mu(A) = 0.2$, $\mu(B)=0.3$ and $\mu(C)=0.5$.

In bakery $A$, there are more pastries produced than being consumed, while in $B, C$ more people are having their pastry than $B, C$ can actually produce. The reasonable thing to do for an owner of these places, would be to redistribute the pastries so the needs of customers are satisfied. One way of solving this problem would be to come up with a transport plan, a map $t : X \times X \to [0,1]$, where $t(x,y) = k$ would intuitively mean move the ratio of $k$ pastries from bakery $x$ to $y$. Such a transport plan should satisfy

• For all $x \in X$, $\nu(x) = \sum_{x' \in X} t(x,x')$ - whole supply of pastries is used
• For all $x \in X$, $\mu(x) = \sum_{x ' \in X'} t(x',x)$ - all demand is satisfied

In other words, one can think of $t : X \times X \to [0,1]$ as a joint probability distribution $t \in \mathcal{D}(X \times X)$ which can be marginalised into $\nu$ and $\eta$. Such a joint distribution, which equivalently describes a transportation plan is called a coupling of $\eta$ and $\mu$. There can be multiple transportation plans, but some might involve unnecessary movement of pastries to the bakery which is too far away. Each transportation plan can be assigned a cost, proportional to the distance that each fraction of pastries needs to travel. The cost of plan $t$ is given by $c_t$ defined as $$c_t = \sum_{(x,y) \in X \times X} d(x,y)t(x,y)$$

Let $\Gamma(\nu, \mu)$ denote the set of all couplings of $\nu$ and $\mu$. The owner of the bakeries is aiming to minimise the total cost of transportation. The minimal cost of the tranportation from $\mu$ to $\nu$ is given by the following $$d^{\mathcal{D}\downarrow}(\mu, \nu) = \min\{\sum_{(x,y) \in X \times X} d(x,y)t(x,y) \mid t \in \Gamma(\nu, \mu)\}$$

It turns out that phrasing this minimisation problem as a linear program guarantees existence of the optimal coupling, which costs the least. The definition above actually defines takes a pseudometric $d : X \times X \to [0, \top]$ and transforms it into a pseudometric $d^{\mathcal{D}\downarrow} : \mathcal{D} X \times \mathcal{D} X \to [0, \top]$ on distributions over $X$. This (pseudo)metric is known as Wasserstein metric.

In our example, it turns out that the most cost optimal plan is to do the following: - Move $\frac{1}{5}$ of pastries from $A$ (where there is an overproduction) to $B$ - Move $\frac{3}{10}$ of pastries from $A$ (where there is an overproduction) to $C$

The optimal cost is given by the following $$d^{\mathcal{D}\downarrow}(\nu,\mu)= \frac{1}{5}\cdot 3 +\frac{3} {10} \cdot 5 = 2.1$$

Now, consider an alternative approach. Let’s say that instead of organising transport on their own, the owner of the bakery will hire an external company to do that. In such a setting the company will assign to each bakery a price for which it buy pastries (in case of overproduction) or sells (in the case of higher demand). Formally it will be modelled as functions $$f : X \to \mathbb{R}^{+}$$ satisfying that for all $x,y \in X$, we have that $$\mid f(x) - f(y)\mid \leq d(x,y)$$ One can think of the requirement above that intuitively owner of the bakeries won’t accept situation when they have to pay more for the transport than when performing the transport on their own. Formally speaking, it means that $f$ is a nonexpansive function from $(X,d)$ to nonnegative reals equipped with euclidean norm $d_e$. Given a price plan $f : X \to \mathbb{R}^+$ the income of the company will be given by $$\sum_{x \in X} f(x) (\mu(x) - \nu(x))$$

The external company would like to maximise their profits, so the optimal profit would be given by $$d^{\uparrow \mathcal{D}}(\mu, \nu)= \sup\left\{ \sum_{x \in X}f(x)(\mu(x)-\nu(x)) \mid f : (X, d) \to (\mathcal{R}^{+}, d_e) \text{ nonexpansive}\right\}$$

The optimal pricing plan exists (again by formulation of the problem as the linear programming problem), so the above is well-defined. $d^{\mathcal{D}\uparrow}$ happens to be a pseudometric, as long as $d$ is. This notation of distance between distributions is known as Kantorovich metric.

For the example above, the optimal price plan is given by the following: - Owner of the bakeries gives out the excess from $A$ for free ($f(A)=0$) - Bakery $B$ buys necessary pastries for three monetary units ($f(B)=3$) - Bakery $C$ does the same with the cost of five units ($f(C)=5$) In such a case, the distance is given by the following $$d^{\mathcal{D}\uparrow}(\mu, \nu) = 0 \cdot (0.2-0.7) + 3 \cdot (0.3 - 0.1) + 5 \cdot (0.5 - 0.2)= 2.1$$

In this particular case, we ended up with the same distance as before, when talking about transport plans. It is no coindidence and actually an instance of the quite famous result, know as Kantorovich-Rubinstein duality. We have that $$d^{\mathcal{D}\uparrow}=d^{\mathcal{D}\downarrow}$$ One can intuitively think that minimising the transportation cost is dual to the external company trying to maximise their profit.

Liftings to $\mathsf{PMet}$

The above distances can also be thought of as answers to the following lifting problem. If $F$ is a functor on $\mathsf{Set}$, then how can one construct a functor $\overline{F}$ on $\mathsf{PMet}$ such that

commutes? In other words, how can we construct a functor $\overline{F}:\mathsf{PMet}\to \mathsf{PMet}$ that acts as $F$ on the underlying sets and nonexpansive functions?

The first priority when defining a lift is that $\overline{F}$ should be a functor. That is, when given a pseudometric space $(X,d)$, we need to define a pseudometric on $FX$ in a sensible way. Since the definition of a lift implies that $\overline{F}f$ is just $Ff$ for all nonexpansive $f:(X,d_X)\to (Y,d_Y)$ and we need $Ff$ to be nonexpansive, then the pseudometrics on the objects $FX$ and $FY$ need to ensure that $Ff$ is nonexpansive. Then and only then does $\overline{F}$ become a functor.

Put precisely, in order to have a lift, we require that - for any pseudometric space $(X,d_X)$, we have a pseudometric space $(FX,d_X^F)$ such that - for any nonexpansive functions $f:(X,d_X)\to (Y,d_Y)$, the function $Ff:(FX,d_X^F)$ and $(FY,d_Y^F)$ is nonexpansive.

In the above case of the distance between two distributions, an initial distance $d_X$ between elements of $X$ was given, and the distance on $\mathcal{D}X$ was defined. The functoriality of such a construction was not checked, but it holds (and the proof in the abstract case can be found in the referential paper).

Inspired by the constructions in the case of $\mathcal{D}$, Kantorovich and Wasserstein liftings can be defined for arbitrary functors. This is also where the relevance to coalgebras becomes evident – the notion of a lift enables us to start with a pseudometric on the state space $X$, and induce from that a pseudometric on the space of possible behaviours $FX$.

In the mechanics of lifting a pseudometric, it is useful to consider an evaluation function: a function $ev_F:FX\to [0,\top]$ for all objects $X$. Then, we can consider the function $\widetilde{F}f:FX\to [0,\top]$ defined as $\widetilde{F}f = ev_F\circ Ff$ for morphisms $f:X\to[0,\top]$. Certain choices of evaluation functions may arise in the case of particular functors. For example, in the case of $\mathcal{D}$, the evaluation function $\mathcal{D}X\to [0,1]$ is taken to be the expected value $\mathbb{E}(-)$.

Kantorovich lifting

The Kantorovich lifting is defined as follows. Let $F$ be a functor on $\mathsf{Set}$ with an evaluation function $ev_F$. Then the Kantorovich lifting is the functor $\overline{F}$ that takes $(X,d)$ to the space $(FX,d^{\uparrow F})$, where $$d^{\uparrow F}(t_1,t_2) := \sup\{\: d_e\left( \widetilde{F}f(t_1),\widetilde{F}f(t_2)\right)\:\mid\: f:(X,d)\to ([0,\top],d_e) \:\}.$$

This is in fact the smallest possible pseudometric that makes all functions $\widetilde{F}f:FX\to [0,\top]$ nonexpansive. The Kantorovich lifting preserves isometries.

Wasserstein lifting

The Wasserstein distance $d^{\downarrow F}$ that is required to define the Wasserstein lifting, needs more work to set up. Altogether, it requires a generalised definition of couplings, some well-behavedness conditions from the evaluation function, and the preservation of weak pullbacks from the functor.

read more

guest post by Elena Dimitriadis, Richie Yeung, Tyler Hanks, and Zhixuan Yang

In the Part 1 of this post, we saw how logical equivalences of first-order logic (FOL) can be characterised by a combinatory game, but there are still a few unsatisfactory aspects of the formulation of EF games in Part 1:

1. The game was formulated in a slightly informal way, delegating the precise meaning of “turns”, “moves”, “wins” to our common sense.

2. There are variants of the EF game that characterise logical equivalences for other logics, but these closely related games are defined ad hoc rather than as instances of one mathematical framework.

3. We have confined ourselves entirely to the classical semantics of FOL in the category of sets, rather than general categorical semantics.

So you, a patron of the n-Category Café, must be thinking that category theory is perfect for addressing these problems! This is exactly what we are gonna talk about today—the framework of game comonads that was introduced by Abramsky, Dawar and Wang (2017) and Abramsky and Shah (2018).

(We will not address the third point above in this post though, but hopefully the reader will agree that what we talk about below is a useful first step towards model comparison games for general categorical logic.)

One-Way EF Games

Let’s warm up by recalling EF games and considering a simplified version of them.

Recall that a $k$-round EF game is parameterized by two $\sigma$-relational structures $\mathcal{A}$ and $\mathcal{B}$ for some relational vocabulary $\sigma$. The rule is that in every round $1 \leq i \leq k$, the spoiler picks either an element from $\mathcal{A}$ or an element from $\mathcal{B}$, and then the duplicator responds with an element from the other structure. The duplicator wins if after $k$-rounds, these elements form a partial isomorphism.

In the game the spoiler has the freedom in each round to pick the structure $\mathcal{A}$ or $\mathcal{B}$, so EF games are also sometimes called back-and-forth games. We can also consider the one-way variant of EF games from $\mathcal{A}$ to $\mathcal{B}$, where the spoiler can only pick elements $a_i$ from $\mathcal{A}$ (so the duplicator responds with elements $b_i$ from $\mathcal{B}$). Additionally, we weaken the winning condition for the duplicator to be $a_i \mapsto b_i$ forming a partial homomorphism from $\mathcal{A}$ to $\mathcal{B}$ (rather than a partial isomorphism).

It is not difficult to modify the Ehrenfeucht-Fraïssé theorem that we saw last time to show that such one-way EF games characterise the fragment of FOL that only uses $\exists$, $\wedge$, $\vee$, $\text{true}$, $\text{false}$. This fragment of FOL is known as existential-positive fragment of first-order logic or coherent logic.

Theorem (Existential Ehrenfeucht-Fraïssé). If the duplicator has a winning strategy for the $k$-round one-way EF game from $\mathcal{A}$ to $\mathcal{B}$, then $A \models \varphi$ implies $B \models \varphi$ for all closed formulas $\varphi$ of quantifier rank $k$ in the existential-positive fragment.

A consequence of the one-way EF games is that now a winning strategy for the duplicator can be thought of as a function from the half-board of $\mathcal{A}$-elements $\langle a_1, \cdots, a_i\rangle$ in each round $i$ to the duplicator’s response $b_i \in \mathcal{B}$, instead of a function from the whole board $\langle\langle a_1, \cdots, a_i\rangle, \langle b_1, \cdots, b_{i-1}\rangle\rangle$ to their response $b_i$. The reason is that the $\mathcal{B}$-elements $\langle b_1, \cdots, b_{i-1}\rangle$ were all picked by the duplicator themselves before, so the duplicator knows what they are, and they don’t have to be in the input to the duplicator’s winning strategy.

Write $A^{\leq k}$ for the set $\left\{\langle a_1, \cdots, a_i\rangle \in A^\ast \mid 1 \leq i \leq k\right\}$ of non-empty $A$-sequences of length at most $k$. Clearly, not every function $f : A^{\leq k} \to B$ is a valid winning strategy for the duplicator for the one-way EF game, since the duplicator has to make sure their responses $b_i$ maintain a partial homomorphism to the spoiler’s choices $a_i$.

More precisely, for all half-boards $\langle a_1, \cdots, a_i\rangle \in A^{\leq k}$, if some of its elements are related by a relation $P \in \sigma$ of arity $m$, i.e. $P^A(a_{j_1}, \dots, a_{j_m})$ holds for $1 \leq j_1, \dots, j_m \leq i$, the duplicator’s strategy $f : A^{\leq k} \to B$ must make $$P^B(f\;\langle a_1, \dots, a_{j_1}\rangle, \dots, f\;\langle a_1, \dots, a_{j_m}\rangle) \ \text{hold}.$$

The EF Game Comonad

Now we are ready to formulate EF games in a more categorical way using comonads. Recall that the Kleisli presentation a comonad $(G, \epsilon, (-)^\ast)$ on a category $\mathcal{C}$ is given by

• a map $G: \mathop{Obj}(\mathcal{C}) \to \mathop{Obj}(\mathcal{C})$,

• for all $A\in \mathcal{C}$, a counit $\epsilon_A: G A \to A$, and

• a co-extension operation $(-)^\ast$ that takes every morphism $f : G A \to B$ to a morphism $f^\ast: G A \to G B$

such that the following equations hold for all $f : G A \to B$ and $g : G B \to C$: $$\begin{array}{rcll} (g\circ {f^\ast})^\ast &=& g^\ast\circ f^\ast &: G A \to G C\\ \mathit{id}_{G A} &=& \epsilon_A^\ast &: G A \to G A\\ f &=& \epsilon_B\circ f^\ast &: G A \to B. \end{array}$$

Given any natural number $k$, the mapping from sets $A$ to sets $A^{\leq k}$ of non-empty $A$-sequences of length at most $k$ can be equipped with a comonad structure $E_k$ on $\mathbf{Set}$:

• $E_k A = A^{\leq k}$ for all sets $A$;

• $\epsilon_A \langle a_1, \dots, a_i\rangle = a_i$ extracts the last element of the sequence (which corresponds to the newest choice by the spoiler in the one-way EF game);

• for all $f: E_k A \to B$, the co-extension $f^\ast : E_k A \to E_k B$ is $$f^\ast\;\langle a_1, \ldots, a_i\rangle = \langle f \; \langle a_1\rangle,\ f \; \langle a_1,a_2\rangle,\ \dots, f \; \langle a_1, \ldots, a_i\rangle\rangle,$$ which intuitively means that the duplicator can recall their own historical moves on the half-board on $B$ given the spoiler’s half-board on $A$.

A co-Kleisli map $f : E_k A \to B$ for this comonad is then a function from half-boards of $A$-elements to responses in $B$, so $f$ encodes precisely a (not necessarily winning) strategy for the duplicator.

The way to formulate winning strategies is to lift the comonad $E_k$ on $\mathbf{Set}$ to a comonad $\mathbb{E}_k$ on the category $\mathcal{R}(\sigma)$ of $\sigma$-relational structures.

Definition (EF Comonad). The comonad $\mathbb{E}_k$ on $\mathcal{R}(\sigma)$ is defined as follows:

• The object mapping sends every $\sigma$-structure $\mathcal{A} = \langle{A, \{P^A\}_{P \in \sigma}}\rangle$ to the $\sigma$-structure $\mathbb{E}_k \mathcal{A} = \langle E_k A, \{P^{E_k A}\}_{P\in\sigma}\rangle$ whose underlying set is just $E_k A$, i.e. non-empty $A$-sequences of length at most $k$; for every relation symbol $P \in \sigma$ of arity $n$, its interpretation $P^{E_k A} \subseteq (E_k A)^n$ relates sequences $\langle s_1,\dots,s_n\rangle$ satisfying the following two conditions:

  1. for all $1 \leq i, j \leq n$, the sequence $s_i$ is a prefix of $s_j$ or $s_j$ is a prefix of $s_i$, and
  2. $\langle \epsilon_A(s_1), \dots, \epsilon_A(s_n)\rangle\in P^\mathcal{A}$.

• The counit $\epsilon_{\mathcal{A}} : \mathbb{E}_k \mathcal{A} \to \mathcal{A}$ and the co-extension $f^\ast : \mathbb{E}_k \mathcal{A} \to \mathbb{E}_k \mathcal{B}$ are the same as those of the comonad $E_k : \mathbf{Set} \to \mathbf{Set}$. It can be checked that they are valid morphisms in the category $\mathcal{R}(\sigma)$.

Co-Kleisli morphisms $\mathbb{E}_k \mathcal{A} \to \mathcal{B}$ are exactly winning strategies for the duplicator in the one-way EF game frome $\mathcal{A}$ to $\mathcal{B}$ (modulo one subtle problem that we will talk about later). Let’s gain some intuition by looking at a small example.

Let us have two $\sigma$-structures, $\mathcal{A}$ and $\mathcal{B}$, with underlying sets $A=\{a,b,c\}$ and $B=\{a',b',c',d'\}$ respectively, and let us play a 3-round one-way EF game. We will try to associate the objects of the comonad as we go: * The spoiler chooses $a\in A$. In response, the duplicator chooses $a' \in B$: $$\epsilon_A \langle a\rangle=a,\quad f \langle a\rangle=a',\quad f^\ast \langle a\rangle=\langle a'\rangle.$$

• The spoiler chooses $b\in A$. In response, the duplicator chooses $b'\in B$: $$\epsilon_A \langle a,b\rangle=b,\quad f \langle a,b\rangle=b',\quad f^\ast \langle a,b\rangle=\langle a',b'\rangle.$$

• The spoiler chooses $c\in A$. In response, the duplicator chooses $c'\in B$: $$\epsilon_A \langle a,b,c\rangle=c,\quad f \langle a,b,c\rangle=c',\quad f^\ast \langle a,b,c\rangle=\langle a',b',c'\rangle.$$

For intuition on how the EF comonad $\mathbb{E}_k$ acts on relations, let us look at the binary relation case. The general case has the same intuition, but with more terms.

Condition (1) of the above definition imposes that one sequence be a prefix of the other. In game terms, this amounts to that $s_1$ and $s_2$ can be stages of the same game play: either $s_1$ evolves to $s_2$ or $s_2$ evolves to $s_1$.

Condition (2) says that two sequences $s_1$ and $s_2$ are related iff their last elements are related. Since under Condition (1), $s_1$ and $s_2$ are two stages of the same play, so $s_1$ and $s_2$ being related mean precisely that two elements in a game are related.

Let us go back to our earlier example with our $\sigma$-structures $A=\{a,b,c\}$ and $B=\{a',b',c',d'\}$, and suppose there is binary relation symbol $\leq$ in $\sigma$ whose interpretation in $A$ and $B$ are the alphabetical order $\leq$. Then, we can say that $\langle a,b\rangle \leq^{E_k A} \langle a,b,c\rangle$, because on one hand both sequences start in the same way (this game has started with the spoiler playing $a$ and then $b$), and on the other hand $b\leq c$ in the alphabetical order.

Now the intuition behind the comonad $\mathbb{E}_k$ might be clearer: in the $\sigma$-relational structure $\mathbb{E}_k\mathcal{A}$, some sequences $s_1, \dots, s_n$ are related means precisely that there is a game play for which $s_1, \dots, s_n$ are the spoiler’s half-boards on $\mathcal{A}$ in certain rounds, and the spoiler’s choices $\epsilon(s_1), \dots, \epsilon(s_n)$ are related by some relation in $\mathcal{A}$. Therefore, a $\sigma$-structure homomorphism $\mathbb{E}_k \mathcal{A} \to \mathcal{B}$ is a winning strategy for the duplicator.