Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

July 29, 2022

Relational Universal Algebra with String Diagrams

Posted by Emily Riehl

guest post by Phoebe Klett and Ralph Sarkis

This post continues the series from the Adjoint School of Applied Category Theory 2022. It is a summary of the main ideas introduced in this paper:

Just as category theory gives us a bird’s-eye view of all mathematical structures, universal algebra gives a bird’s-eye view of all algebraic structures (groups, rings, modules, etc.) While universal algebra leads to a beautiful theory with many general statements — it also enjoys a categorical formulation introduced in F.W. Lawvere’s thesis which inspired the aforementioned paper’s title — it does not deal with several common structures in mathematics like graphs, orders, categories and metric spaces. Relational universal algebra allows to cover these examples and more. In this post, we present this field of study using a diagrammatic syntax based on cartesian bicategories of relations.

Relational Algebras

We start by describing the classical (or non-categorical) view of relational theories because it should look more familiar to most people. The classical story starts with universal algebra, a field of mathematics that studies algebraic structures — like groups, rings, modules or lattices — from above. Instead of doing group theory, ring theory, etc., universal algebra formalizes what all these theories have in common to study algebraic theories all at once. An algebraic theory is the basic object of study in universal algebra, and it syntactically describes a kind of structure by asserting what types of operations can be done and the properties they satisfy. For instance, the theory of monoids contains

  • a symbol \cdot that takes two inputs and a symbol 11 that takes no inputs, and
  • axioms that stipulate how these symbols can be manipulated.

While theories embody the syntax wielded by an algebra professor on the blackboard, students understand the meaning of these obscure symbols using models. A model for a theory is an interpretation of the symbols that instantiates the structure described, e.g., models of the theory of monoids are monoids.

The limit of universal algebra is that the structures have to be sets XX equipped with functions of type X nXX^n\to X. This does not cover things that are not intuitively algebraic, e.g., graphs, orders, metric spaces. Relational algebraic theories can cover all these examples as well as all algebraic theories.

Let us go quickly through the definitions before giving more insight with examples.

Definition: A relational signature Ξ\Xi is a set of symbols, each with an arity and coarity in \mathbb{N}. We write m:R:nΞm:\mathsf{R}:n \in \Xi for a symbol of arity mm and coarity nn belonging to Ξ\Xi.

Definition: A model of Ξ\Xi is a set AA, called the carrier, equipped with a relation R AA m×A n\llbracket\mathsf{R}\rrbracket_{A} \subseteq A^m \times A^n for every m:R:nΞm:\mathsf{R}:n \in \Xi. A morphism of models is a function between the carriers that preserves all relations in the signature, i.e., f:ABf: A \rightarrow B satisfying

m:R:nΞ,(x,y)R A(f(x),f(y))R B.\forall m:\mathsf{R}:n \in \Xi, (\vec{x},\vec{y}) \in \llbracket\mathsf{R}\rrbracket_{A} \implies (f(\vec{x}),f(\vec{y})) \in \llbracket\mathsf{R}\rrbracket_{B}. Examples:

  • Models of the empty signature Ξ=\Xi = \emptyset are simply sets, and their morphisms are functions with no constraints.
  • Models of Ξ={1:P:0}\Xi = \{1:\mathsf{P}:0\} are sets AA equipped with a predicate, i.e., a subset of A 1×A 0=AA^1 \times A^0 = A. For two predicates P AAP_{A} \subseteq A and P BBP_{B} \subseteq B, a function f:ABf: A \to B preserves the predicate iff f(P A)P Bf(P_{A}) \subseteq P_{B}, or, written differently, aP Af(a)P Ba \in P_{A} \implies f(a) \in P_{B}.
  • Models of Ξ={1:E:1}\Xi = \{1:\mathsf{E}:1\} are sets AA equipped with a binary relation, i.e., a subset of A 1×A 1=A 2A^1 \times A^1 = A^2. Given binary relations E AE_{A} and E BE_{B} on AA and BB respectively, a function f:ABf:A \to B is a morphism iff (a,a)E A(f(a),f(a))E B(a,a') \in E_{A} \implies (f(a), f(a')) \in E_{B}.

To obtain more interesting objects, we need to impose axioms on the relations in the signature, e.g.,

  • a poset is a set with a binary relation that is reflexive, transitive and antisymmetric
  • an undirected graph (with loops) is a set with a binary relation that is symmetric
  • a magma is a set with a relation between A 2A^2 and AA that is a function, namely, each element of A 2A^2 is related to exactly one element in AA.

In universal algebra, axioms are imposed by equations between terms constructed using the symbols of the theory. The theory of monoids, for instance, contains the following three equations

x(yz)=(xy)zx1=x1x=x x\cdot (y\cdot z) = (x\cdot y) \cdot z \qquad x \cdot 1 = x \qquad 1 \cdot x = x which imply that, in every model, the monoid operation is associative and has 11 as its neutral element (on the left and right). It is not hard to design something similar for posets. The structure consists of a binary relation A×A{\sqsubseteq} \subseteq A \times A, and the axioms are (where 1 AA×A1_A \subseteq A\times A is the identity or diagonal relation and ;; denotes composition of relations)

1 A;1 A.1_{A} \subseteq {\sqsubseteq} \qquad {\sqsubseteq; \sqsubseteq} \subseteq {\sqsubseteq} \qquad {\sqsubseteq} \cap {\sqsupseteq} \subseteq 1_{A}. For now, you can believe us that these assert reflexivity, transitivity, and antisymmetry respectively.

The terms x(yz)x\cdot (y\cdot z), (xy)z(x\cdot y)\cdot z, x1x\cdot 1, and 1x1 \cdot x, were constructed using only the syntax that is part of the theory of monoids, while the axioms in the theory of posets rely on the identity relation and the composition and intersection of relations in addition to the symbols in the signature. Moreover, the axioms are stated as inequations rather than equations.

Cartesian Bicategory of Relations

In this section, we describe a diagrammatic syntax that will be used to specify axioms of a theory, and in particular, to construct complex relations out of symbols in the signature. This syntax comes from the structure of a cartesian bicategory of relation. We will introduce this notion by looking at one particular instance of it: the category Rel\mathbf{Rel} of sets and relations.

The objects of Rel\mathbf{Rel} are sets, and a morphism XYX \to Y in Rel\mathbf{Rel} is a subset of X×YX\times Y that we call a relation from XX to YY. The composition of two relations R:XYR:X \to Y and S:YZS: Y \to Z is defined by R;S={(x,z)yY,(x,y)Rand(y,z)S}X×Z,R\mathop{;}S = \{(x,z) \mid \exists y \in Y, (x,y) \in R\ \text{and}\ (y,z) \in S\} \subseteq X\times Z, and the identity relation is id X={(x,x)xX}X×X\mathrm{id}_X = \{(x,x) \mid x \in X\} \subseteq X\times X.

The categorical product in Rel\mathbf{Rel} is the disjoint union of sets (it is also the coproduct), so the Cartesian product of sets does not satisfy the usual universal property. (For those who already know about functorial semantics of algebraic theories, this explains why the naive attempt to describe relational algebras as Rel\mathbf{Rel}-valued cartesian functors fails.) However, Rel\mathbf{Rel} equipped with the Cartesian product is a cartesian bicategory of relations, namely, it is poset-enriched, symmetric monoidal, and it is a hypergraph category where convolution is idempotent. Let us unroll this.

Rel\mathbf{Rel} is enriched in the category of posets and order-preserving maps. Explicitly, we can see the Hom-set Rel(X,Y)\mathbf{Rel}(X,Y) as the powerset 𝒫(X×Y)\mathcal{P}(X\times Y), then \subseteq (set inclusion) is a partial order, and one can check for any R 1R 2Rel(X,Y)R_{1} \subseteq R_{2} \in \Rel(X,Y) and S 1S 2Rel(Y,Z)S_{1} \subseteq S_{2} \in \Rel(Y,Z), R 1;S 1R 2;S 2R_{1} \mathop{;} S_{1} \subseteq R_{2} \mathop{;} S_{2}.

Rel\mathbf{Rel} equipped with the Cartesian product of sets is a symmetric monoidal category. Indeed, the Cartesian product of sets is associative (up to isomorphisms), and the singleton 1={}\mathbf{1} = \{\bullet\} is the unit, i.e., for any set XX, X×1X1×XX\times \mathbf{1} \cong X \cong \mathbf{1}\times X. For any two relations RRel(X,Y)R \in \mathbf{Rel}(X,Y) and RRel(X,Y)R' \in \mathbf{Rel}(X',Y'), we define R×R:={((x,x),(y,y))(x,y)Rand(x,y)R}(X×X)×(Y×Y).R\times R' := \{((x,x'),(y,y')) \mid (x,y) \in R\ \text{and}\ (x',y') \in R'\} \subseteq (X\times X') \times (Y \times Y'). One can check that the interchange identity holds (R;S)×(R;S)=(R×R);(S×S),(R\mathop{;} S) \times (R'\mathop{;}S') = (R\times R') \mathop{;} (S\times S'), and the Cartesian product preserves the order, i.e., for any R 1R 2Rel(X,Y)R_{1} \subseteq R_{2} \in \mathbf{Rel}(X,Y) and S 1S 2Rel(X,Y)S_{1} \subseteq S_{2} \in \mathbf{Rel}(X',Y'), R 1×S 1R 2×S 2.R_{1} \times S_{1} \subseteq R_{2} \times S_{2}. For any sets XX and YY, the braiding is the relation σ X,Y={((x,y),(y,x))xX,yY}(X×Y)×(Y×X).\sigma_{X,Y} = \{((x,y), (y,x)) \mid x \in X, y \in Y\} \subseteq (X\times Y) \times (Y \times X).

We can summarize the last paragraph by saying how we can manipulate relations with string diagrams. For any set XX, we draw the identity relation on XX as a single wire

we draw a relation R:XYR: X \to Y as a box

we draw the composition of two relations R:XYR:X \to Y and S:YZS: Y \to Z as the sequential composition of boxes

we draw the product of relations R:XYR:X \to Y and R:XYR': X' \to Y' as parallel composition of boxes

and, finally we draw the braidings as wires crossing

This two dimensional syntax is that it is topologically sound. This means you can manipulate a diagram as you if you were moving actual wires connected to boxes on a table, and if you do not break/cut any connection and leave the boundary (the input and output wires) untouched, then the diagram you started with and the diagram you end up with represent the same relation. Here is an example of two diagrammatic representations of the same relation.

In addition, with a bit of visual imagination, one can figure out the relation represented by a diagram without translating to the classical syntax. We abstain from explaining this process here, but we can recommend these wonderful videos that introduce a syntax very similar to ours.

Rel\mathbf{Rel} equipped with ×\times is a hypergraph category because every set can be coherently equipped with a special commutative Frobenius algebra structure. Explicitly, given a set XX, there are four relations Δ X\Delta_{X}, X\nabla_{X}, ! X!_{X} and ? X?_{X} depicted below that satisfy a bunch of equations listed below.

f ={(x,(y,z))x=y=z}X×X 2\begin{matrix}\phantom{f}\\ = \{(x,(y,z)) \mid x = y = z\} \subseteq X \times X^2\end{matrix}
f ={((x,y),z)x=y=z}=Δ X op\begin{matrix}\phantom{f}\\ = \{((x,y),z) \mid x = y = z\} = \Delta_X^{\mathrm{op}}\end{matrix}
f ={(x,)xX}X×1\begin{matrix}\phantom{f}\\ = \{(x,\bullet) \mid x\in X\} \subseteq X \times \mathbf{1}\end{matrix}
f ={(,x)xX}=! X op\begin{matrix}\phantom{f}\\ = \{(\bullet,x) \mid x\in X\} = {!}_X^{\mathrm{op}}\end{matrix}

For our purposes, all of this is simply additional syntax that we can use to construct relations. These equations mean that whenever you see the left hand side of an equation within a bigger diagram, you can replace it with the right hand side without altering the meaning of the bigger diagram.

Finally, convolution in Rel\mathbf{Rel} is idempotent. Given two relations R,S:XYR,S: X \to Y, the convolution of RR and SS is the relation Δ X;(R×S); Y\Delta_{X}\mathop{;} (R\times S) \mathop{;} \nabla_{Y} drawn as

Puzzle: What is the convolution of RR and SS?

The solution is given later in the post, but for now, it is important to note that for any relation RR, the convolution of RR with itself is equal to RR, that is, convolution is idempotent.

Recall that we introduced the diagrammatic syntax of cartesian bicategories of relations because we wanted a language to express axioms of a theory of relational algebras. The following section is devoted to such theories.

Frobenius Theories

Now that we’ve been introduced to the ideas of universal algebra and the syntax of cartesian bicategories of relations, we can start to talk about theories of a categorical flavor, theories in functorial semantics, and specifically Frobenius theories as introduced by the authors of the paper. The definition of a theory in this case looks very similar to that of universal algebra.

Given a relational signature Ξ\Xi, a Frobenius Ξ\Xi-term is a string diagram constructed with the generators in Ξ\Xi and the syntax of cartesian bicategories of relations. This construction of terms will allow us to express and impose axioms on more complex terms, as we lacked in the previously discussed theories.

A Frobenius theory is a pair T=(Ξ,I)T = (\Xi, I) consisting of a relational signature Ξ\Xi and a set of inequations II, i.e., pairs sts\leq t where ss and tt are Frobenius Ξ\Xi-terms. Note that inequationas are at least as powerful as equations since, in the interpretation outlined below, having s=ts = t would be equivalent to having sts\leq t and tst\leq s. We often call theories with inequations lax theories, as we’ve relaxed the equality into an inequality.

Let’s see an example. The Frobenius theory of posets can be described with one generating relation 1::11:{\sqsubseteq}: 1 and 3 inequations.

Translating between the string diagrams and axioms (in blue) is achieved using models of the theory, which will be discussed shortly.

Given a theory T=(Ξ,I)T = (\Xi, I), we can generate a Frobenius prop T\mathcal{F}_T or “frop” for short. A prop is a strict symmetric monoidal category, where the objects are the natural numbers and the monoidal product is addition. Arrows nmn \rightarrow m are string diagrams with nn input wires and mm output wires.

Just as we can generate a vector space from a set of basis vectors, we can generate a prop from a theory. Given the (co)monoid structure of cartesian bicategories of relations, along with any generating relations of the theory, we can freely construct terms or arrows in our frop using sequential and parallel composition.

Arrows in T\mathcal{F}_T are Frobenius Ξ\Xi-terms modulo laws of cartesian bicategories of relations, modulo smallest congruence with respect to (;,×)({;}, \times) containing equations sts \leq t s,tI\forall s,t \in I. This means for a pair (s,t)I(s,t) \in I we can swap out these terms in our arrows as shown below.

Models of a Frobenius Theory

Earlier we discussed models of a theory as instances of the thing we care about. (I.e. if we’re studying the theory of groups, a model in that case is a choice of group.) Functorial semantics is a categorical perspective of what it means to be a model. Namely, models of Frobenius theories are functors of a specific type.

Explicitly, a model for a Frobenius theory TT is a functor M: TCM:\mathcal{F}_T \to \mathbf{C} from T\mathcal{F}_{T}, the frop generated by TT, to a cartesian bicategory of relations C\mathbf{C} such that MM preserves the structure of cartesian bicategories of relations. For intuition, we’ll use C=Rel\mathbf{C} = \mathbf{Rel} in this post.

To continue with the analogy of vector spaces, to understand how a linear transformation behaves we only need to consider how it acts on the basis vectors. In our case, in order to understand how our model behaves we only need to consider how it acts on the generating relations. And in order to interpret our inequations in the new setting of Rel\mathbf{Rel} we simply apply our model. We illustrate the example of posets below.

Note that we used the solution of the puzzle above: the convolution of M()M(\sqsubseteq) and M()M(\sqsupseteq) is their intersection.

What about morphisms of models? To understand the category of models, we need to know what arrows in that space look like. Morphisms of models are natural transformations, and in the Frobenius case, a morphism of models MKM \to K is a monoidal lax natural transformation.

In particular, given M: TRelM: \mathcal{F}_{T} \rightarrow \mathbf{Rel},

K: TRelK: \mathcal{F}_{T} \rightarrow \mathbf{Rel}

ϕ:MK\phi: M\rightarrow K is the data ϕ n:M(n)K(n)n\phi_{n}: M(n) \rightarrow K(n) \qquad n \in \mathbb{N}

But since we know (in the Frobenius case) that this natural transformation is monoidal, we can conclude that it’s determined by ϕ 1\phi_1.

We also know that for all f:no Tf:n \rightarrow o \in \mathcal{F}_{T} the diagram below laxly commutes.

We consider the interesting cases when ff is the (co)monoidal terms and any generating terms in the signature.

Inequations for \nabla and ?? hold for any relation ϕ\phi, but inequations for Δ\Delta and !! hold if and only if the relation ϕ\phi is a function\mathbf{function}.

f=f = \sqsubseteq

ϕ 1(M()(M(1))K()(ϕ 1(M(1)))\phi_{1}(M(\sqsubseteq)(M(1))\leq K(\sqsubseteq)(\phi_{1}(M(1)))

When ff is the generating relation in signature of posets, we arrive at the function being order preserving.

In general for any theory, a morphism in the category of models is a function preserving the relations. And this is the same as we had in the classical view. In cases where the classical models of universal algebra are equally expressive as the models of functorial semantics, their models are isomorphic. This is true for example in the case of Monoids.

Mod( CM,Set)Monoid\mathbf{Mod}(\mathcal{F}_{CM},Set) \cong Monoid

Examples

Let’s see a few more examples.

What is the category of models for the empty Frobenius theory

(,)(\emptyset, \emptyset)?

This is just Set\mathbf{Set} the category of sets and functions. models F:F ,RelF : F_{\emptyset, \emptyset} \rightarrow \mathbf{Rel} are uniquely determined by the object F1F1, which is just a set, and as we saw before, morphisms of models are functions.

What about if we add the following inequation to II?

How do we even interpret this inequation? The right hand side can be decomposed into the composition of the unit and the counit, and relationally can be interpreted as “there exists an object aa such that it’s related to the (co)unit”. This is true for any object aa, so this inequation is just asking us to have an element in our set, or for our set to be nonempty.

Models are sets that contain at least one element.

Let’s take semigroups, roughly groups where we forget about identities and inverses. We define the signature and equations as below.

How should we interpret these equations?

Consider the inequation called “total”. Intuitively, total asks that all inputs map to at least one output. We can see this in the diagram by noting that both the right hand side and the right most term on the left hand side are always true, leaving only the first term on the left side, which simply quantifies the output of any input x,yx,y. or “there exists some zz such that R(x,y)=zR(x,y) = z”.

If we add the following equation, we get regular semigroups, or semigroups where for any aa, there exists xx such that axa=aa x a=a.

If you picture aa and xx coming in along the strings here, being copied/multiplied at the nodes, you can follow along to this conclusion.

The category of models and model morphisms is the category of regular semigroups and semigroup homomorphisms.

Posted at July 29, 2022 2:57 PM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/3413

0 Comments & 0 Trackbacks

Post a New Comment