Part of a presentation on Coalgebras over Lawvere Metric Spaces

Generalizing to Quantales

How far can we push the observation that the notions of behavioural equivalence can be generalised using enriched category theory?

As suggested by Rutten (1998) and Worrell (2000) a fruitful level of generality is coalgebras over the category of categories enriched over a quantale

$\mathrm{\Omega }$.

Lawvere metric spaces are one of the most interesting examples of categories enriched over a quantale.

Lawvere Metric Spaces

Metric Spaces, Generalized Logic, and Closed Categories:

Lawvere focusses in his paper on the quantale

$[0,\mathrm{\infty }]$ where

$0$ is top and the quantale-multiplication is addition, but his ideas can be applied to any quantale.

For the remainder of this presentation we follow our article Extending set functors to generalised metric spaces., where all details and references can be found.

A quantale

$\mathrm{\Omega }$ is a complete lattice with an order-preserving 'multiplication'

$\otimes$ and neutral element

$e$ such that

$v\otimes -$ and

$-\otimes v$ have right adjoints for all

$v\in \mathrm{\Omega }$.

Intuitively, we may think of the order

$v\le w$ as representing (i) logical impliciation,

$w$ being closer to truth than

$v$ or (ii)

$v$ being a greater distance than

$w$. In the latter case

$\otimes$ is addition of distances and the internal hom

$[v,w]$ is

$e$ if

$v\le w$ and, otherwise, how much further from truth

$w$ is than

$v$.

The paradigmatic example for the distance interpretation is the subset of real numbers

$\mathrm{\Omega }=[0,\mathrm{\infty }]$ with addition as multiplication and truncated minus as internal hom.

The categories enriched over

$[0,\mathrm{\infty }]$ are known as Lawvere metric spaces. If one uses minimum instead of addition as tensor one obtains Lawvere ultrametric spaces.

The following shows an example with a non symmetric distance.

Example: Let

$X$ be the set of finite and infinite words (strings) over the alphabet

$A$. We define a distance on

$X$ via

$X(s,t)=0$ if

$s$ is a prefix of

$t$ and, otherwise,

$X(s,t)=2^{-n}$ where

$n$ is the position of the first letter where

$s$ is different from

$t$.

In this section we emphasised quantales as lattices of distances. On the other hand, not every quantale lends itself naturally to this interpretation. The next section offers a different interpretation.

Relational Presheaves

Another way to look at categories enriched over a quantale is as relational presheaves. This point of view is equivalent to the metric point of view, but supports a rather different intutition.

Given a category

$X$ enriched over quantale

$\mathrm{\Omega }$ we build a relational structure on the set

$X$ by choosing one binary relation

$R_v\subseteq X\times X$ for all

$v\in \mathrm{\Omega }$,

$v\ne \mathrm{\perp }$, satisfying

$$\begin{array}{rl}(x,y)\in R_v& ⟺X(x,y)\le v\end{array}$$

One can axiomatize those relational structures that arise in this way to obtain an equivalent, independent characterization of categories enriched over

$\mathrm{\Omega }$.

Example: Here are two quantales on the 3-element set:

$$\begin{array}{|cccc|}\hline \otimes & 0& 1& 2\\ 0& 0& 0& 0\\ 1& 0& 1& 2\\ 2& 0& 2& 2\\ \hline\end{array}\begin{array}{|cccc|}\hline [-,-]& 0& 1& 2\\ 0& 2& 2& 2\\ 1& 0& 1& 2\\ 2& 0& 0& 2\\ \hline\end{array}\begin{array}{|cccc|}\hline \otimes & 0& 1& 2\\ 0& 0& 0& 0\\ 1& 0& 1& 1\\ 2& 0& 1& 2\\ \hline\end{array}\begin{array}{|cccc|}\hline [-,-]& 0& 1& 2\\ 0& 2& 2& 2\\ 1& 0& 2& 2\\ 2& 0& 1& 2\\ \hline\end{array}$$

On the left hand side (

$e=1$): The objects of an

$\mathrm{\Omega }$-category are events subject to a schedule, endowed with a preorder

$x\le y$ given by

$R_1$ (with the interpretation that "

$x$ happens no later than

$y$") and a binary relation

$x\prec y$ given by

$R_2$ (which is intended to mean "

$x$ happens strictly earlier than

$y$").

$R_2\subseteq R_1$ says that strict precedence implies weak precedence, while the multiplication law

$1\otimes 2=2$ accounts for the prosset-law that

$x\le y\prec z\le w$ implies

$x\prec w$.

On the right hand side (

$e=2$): The relation

$x{<}^{t}y$ given by

$X_1$ is interpreted as "

$x$ precedes

$y$ in time" and the relation

$x{<}^{c}y$ given by

$R_2$ is interpreted as "

$x$ causally precedes

$y$".

$R_2\subseteq X_1$ captures that causal precedence implies temporal precedence and the multiplication law

$1\otimes 2=1$ reflects that

$x{<}^{t}y{<}^{c}z{<}^{t}w$ implies

$x{<}^{t}w$.

Example: Of course, one can also see Lawvere metric spaces in this way. This is closely related to uniformities.

Thousands of more examples are available in Jipsen and Galatos RESIDUATED LATTICES OF SIZE UP TO 6.

Summary

My longterm aim is to expand general coalgebraic methods to the quantale enriched setting. In the next section, we will look at one successful generalisation in more detail and the last section will look at one area in which many challenges still remain.

Here are some articles generalising set and order based coalgebra to the enriched setting.

• A Kurz, J Velebil: Relation lifting. J. Log. Algebr. Meth. Program. 85(4): 475-499 (2016). Postfinal version with a typo corrected thanks to Uli Fahrenberg.
• M. Bilkova, A. Kurz, D. Petrisan, J. Velebil: Relation lifting, with an application to the many-valued cover modality. Logical Methods in Computer Science, 2013.
• A. Kurz, J. Velebil: Enriched logical connections. Appl. Categ. Structures, online first, 23 September 2011. pdf
• J. Velebil, A. Kurz: Equational presentations of functors and monads . Mathematical Structures in Computer Science (2011) 21(2):363-381. pdf

Further References

The example of relational presheaves are due to:

• R. Casley, On the specification of concurrent systems. PhD thesis, Stanford University (1991)
• H. Gaifman and V. Pratt, Partial order models of concurrency and the computation of functions. In: LICS 1987, IEEE Computer Society Press, Ithaca, NY (1987), 72–85