Algebra, Order and Monads

In the previous post, we introduced preorders, posets and monotone maps between them. We then investigated a small number of monads on these categories of ordered structures. The additional order relations enable interesting new structure on $\mathsf{Pos}$ -monads that we hadn’t encountered before with our main example of $\mathsf{Set}$ -monads.

In this post, we will sketch how the algebraic perspective that is so instructive with $\mathsf{Set}$ monads can be generalised to monads on $\mathsf{Pos}$ . Our discussions will be relatively informal, aiming to highlight the additional aspects of algebra in the land of ordered structures that are of interest. The details involve some fairly technical ideas, which are beyond the scope of what we have covered so far. Interested readers will find some pointers at the end of the post.

Relatives of the Maybe Monad

In the previous post, we introduced the “obvious” generalisation of the maybe monad from sets to posets, with functor component:

$X \mapsto X + 1$

To do so, we mimicked the construction used in $\mathsf{Set}$ in terms of binary coproducts and terminal objects. Our current aim to try and understand such constructions from an algebraic perspective, whatever that means now we’ve moved from sets to posets.

To try and get an algebraic handle on $\mathsf{Pos}$ -monads, we are going to assume we need a collection of operations $\Sigma$ , and a collection of equations $E$ , as was the case for ordinary algebra.

In fact, for the maybe monad, this is already sufficient, so we don’t need anything new. We assume $\Sigma$ consists of a single new constant element $\star$ , and we require no equations. As we only have a constant element, the only terms we can form over $X$ are either:

Variables from $X$ .
The constant symbol $\star$ .

As there are no equations, we don’t need to worry about forming equivalence classes. If we assume variables inherit an ordering from $X$ , and no other non-trivial order relations hold, the resulting poset is isomorphic to

$X + 1$

which is exactly what we hoped for. So far, so easy. A small additional step will take us into less familiar territory. Rather than generalising the maybe monad, instead we can consider the exception monad induced by some poset $E$ . This will have functor action:

$X \mapsto X + E$

Recall that the coproduct of posets inherits the order from the two components, and no other non-trivial order relations hold.

Algebraically, the $\mathsf{Set}$ exception monad corresponded to adding a set $E$ of new constant symbols. If we do this is $\mathsf{Pos}$ , and form terms over $X$ as we did above for the maybe monad, we will get a poset with an underlying set consisting of:

Variables from $X$ .
Constant symbols $e \in E$ .

The only non-trivial order relations will be those between the variables inherited from $X$ . This isn’t quite general enough for what we want, as we want to allow $E$ to be a poset, not just a mere set. It is reasonably clear we cannot achieve the desired effect, even if we add in some equations. So we shall need the first new feature of algebra on posets:

Operation symbols of the same arity form a poset.

If we were to provide some formal syntax, in our example, we are allowing ourselves to introduce relations

$e_1 \leq e_2$

between the constant symbols representing exceptions. More generally, if we have two operation symbols $o_1, o_2$ of the same arity, and $o_1 \leq o_2$ , then we have the following axiom between terms:

$o_1(x_1,\ldots,x_n) \leq o_2(x_1,\ldots,x_n)$

Last time, we introduced another relative of the maybe monad, the lift monad. Here, we map a poset $X$ to a poset with a new element $\star$ added below all of the elements of $X$ . It doesn’t seem we can achieve the desired effect by ordering our operation symbols, as we need to add an inequation of the form:

$\star \leq x$

between an operation symbol and a bare variable. It is tempting to conclude that for algebra between posets, we need to permit inequations rather than mere equations between terms. In fact, this seems mathematically very natural, but lets not be too hasty.

We can’t achieve the desired effect directly by ordering our operation symbols, as we currently only have the constant symbol $\star$ . Nobody said we can’t add additional operation symbols, so lets be a bit more creative, and add two unary symbols $l$ (for left hand side) and $r$ (for right hand side), and require that $l \leq r$ . Finally, we require the equations:

$l(x) = \star$ and $r(x) = x$

Then we can conclude that:

$\star = l(x) \leq r(x) = x$

If we form equivalence classes of terms, ordering them according to these axioms, the resulting construction yields the lift monad. The upshot of this procedure is that

We can use inequations between terms in poset algebra, but this is achieved using ordering between operation symbols, and equations between terms.

So from this perspective, poset algebra is still fundamentally about equations, not inequations, which is possibly a bit of a surprise.

Relatives of the List Monad

Previously, in the case of $\mathsf{Set}$ -monads, we have seen that the list monad is the free monoid monad. That is, we have a constant symbol $1$ , and a binary operation symbol $\times$ , such that the following three equations hold:

$1 \times x = x = x \times 1$ and $(x \times y) \times z = x \times (y \times z)$ .

We don’t need to consider ordering between our operation symbols, as they are of different arities. We can form equivalence classes of terms, as we would for the set theoretic construction, which correspond to the lists of variables symbols that appear in the terms. The key question is what non-trivial order relations should we add between terms. As we’ve seen before, for terms over poset $X$ , we should always inherit the order relations between variables. Now we have a non-constant operation symbol $\times$ , we have two obvious choices about how this operation interacts with the order structure of its arguments:

Consider the multiplication operation $\times$ to be monotone.
Consider the multiplication operation $\times$ to be an arbitrary function.

If we take the first option, the resulting monad is the list monad, with lists of the same length ordered pointwise. This is the monad $\mathbb{L}_2$ of the previous post. If on the other hand we take the less restrictive route of the second option, we get a different list monad, in which only the singleton lists are ordered with respect to each other if their contained elements are. This is the monad we called $\mathbb{L}_1$ in the previous post. These observations apply in full generality, and lead us to our second observation about poset algebra:

We have the right, but the not obligation, to require that every operation is monotone.

So in fact, there are two different notions of poset algebra we can consider, depending on this choice. It is perhaps slightly surprising at first glance that allowing non-monotone operations is a viable option. One choice corresponds to $\mathsf{Pos}$ -enriched monad theory, and the other to $\mathsf{Set}$ -enriched monad theory, but that will take us further into technically challenging material than is appropriate with what we know so far.

Obviously, we can impose other relations such as:

$x \leq x \times y$ and $x \times y \leq y$

using the ability to encode inequations as axioms discussed above. These additional inequations yield two more of the list monad variants from the previous post. We also note that in general, our ability to encode inequations lets us require that some, but not all of our operations are monotone.

Finally, we need to consider the ordered list monads that we discussed last time. Recall, these were monads in which we only allow rising lists of the form:

$[x_1,\ldots,x_n]$

where each consecutive pair of elements are ordered, that is $x_i \leq x_{i + 1}$ .

These monads seem to involve some sort of phenomenon that we’ve not encountered so far. It doesn’t seem possible to encode such a monad using the features we’ve introduced previously. We need something new. This leads us to possibly the most exotic feature of poset algebra.

Intuitively, the problem we have is that if we consider a binary operation $\times$ , there’s no restriction on the arguments we can apply it to, for example we can form

$x \times y$

where $x$ is strictly greater than $y$ . This is because for ordinary set algebra, an operation is a map:

$\overbrace{X \times \ldots \times X}^{n\rm\ times} \rightarrow X$

and we have so far continued with this approach to operation arities in the order theoretic context. To generalise things, we observe that if we write $[n]$ for the set $\{ 1, \ldots, n \}$ , this is equivalent to a function:

$X^{[n]} \rightarrow X$

where $X^{[n]}$ is the exponential, the set of all functions from $[n]$ to $X$ . In fact, such an operation is equivalent to one of the form:

$X^A \rightarrow X$

where $A$ is any $n$ -element set. So operations in set can be seen as having arities finite sets. If we generalise this point of view to posets, an operation should be a map:

$X^A \rightarrow X$

where $A$ is a finite poset. This gives us more freedom than before, as finite posets can specify non-trivial ordering between arguments, as the exponential $X^A$ contains only monotone maps. For our list based construction, we can require a $\times$ operation with arity the two element poset $\{ x \leq y \}$ . This is an operation that maps ordered pairs to a new element.

In terms of syntax, this means we should only be able to form the term $x \times y$ if we have established that $x \leq y$ .

Combining these general arities with some of the previous tricks allows us to specify monads that deal with ordered lists. This leads us to our third and final observation about poset algebra:

Operations have arities which are finite posets.

This is a feature we might not have anticipated in advance, but in fact is does fall out of some (rather technical) general categorical arguments, involving locally finite presentable categories.

Conclusion

We have sketched some features we might encounter when dealing with monads and algebra in the context of posets. We encountered three new features beyond what we see in the setting of ordinary universal algebra.

Operation symbols of the same arity can be ordered with respect to each other.
We have the option to require that all our operations are monotone, but this is not compulsary.
The arities of operations that we can consider are not mere numbers. Instead they are specified by finite posets imposing constraints on how the arguments are ordered.

We also discovered we didn’t need to impose inequations between terms as a new feature, as these can be simulated using the features above.

These generalisations follow a pattern that continues for appropriate notions of algebra in other categorical settings. A good starting point for further background is Robinsons “Variations on Algebra”, which is written in an enjoyable expository style, whilst being much more precise on the details than this post. Important technical background can be found in Kelly and Power’s “Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads”. A lot more detail about the right notion of algebra in these generalised settings can be found in the many papers on Lawvere theories of Power and co-authors. The papers “Presentations and algebraic colimits of enriched monads for a subcategory of arities” and “Diagrammatic presentations of enriched monads and varieties for a subcategory of arities” by Lucyshyn-Wright and Parker may also be of interest.

Although there is a great deal of literature about generalised algebra, particularly at the level of Lawvere theories, there is a bit of a gap in the literature. Developing precise syntax and proof systems for these generalised equational logics in specific cases of interest is rarely worked out in detail, particularly when generalised arities are involved. This is a shame, as the concrete tools of equational presentations and equational logic are tremendously useful tools in the set theoretic setting. Detailed meta-theoretic results for such systems, at a high level of abstraction, can be found in the work of Fiore and co-authors, but applying these methods to a specific setting is still challenging.

Acknowledgements: Thanks to Jason Parker for pointing out the two Lucyshyn-Wright and Parker papers as interesting references.

Relatives of the Maybe Monad

Relatives of the List Monad

Conclusion

Share this:

Like this:

Related

Leave a Reply Cancel reply