# Product Rules and Distributive Laws

Joost Winter

► To cite this version:

Joost Winter. Product Rules and Distributive Laws. 13th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2016, Eindhoven, Netherlands. pp.114-135, 10.1007/978-3-319-40370-0_8. hal-01446036

HAL Id: hal-01446036

https://inria.hal.science/hal-01446036

Submitted on 25 Jan 2017

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Product Rules and Distributive Laws

Joost Winter¹*

University of Warsaw, Faculty of Mathematics, Informatics, and Mechanics
jwinter@mimuw.edu.pl

**Abstract.** We give a categorical perspective on various product rules, including Brzozowski's product rule $((st)_a = s_at + o(s)t_a)$ and the familiar rule of calculus $((st)_a = s_at + st_a)$. It is already known that these product rules can be represented using distributive laws, e.g. via a suitable quotient of a GSOS law. In this paper, we cast these product rules into a general setting where we have two monads $S$ and $T$, a (possibly copointed) behavioural functor $F$, a distributive law of $T$ over $S$, a distributive law of $S$ over $F$, and a suitably defined distributive law $TF \Rightarrow FST$. We introduce a coherence axiom giving a sufficient and necessary condition for such triples of distributive laws to yield a new distributive law of the composite monad $ST$ over $F$, allowing us to determine $FST$-coalgebras into lifted $F$ coalgebras via a two step process whenever this axiom holds.

## 1 Introduction

In [Brz64], Brzozowski introduced a calculus of derivatives for regular expressions, including amongst other rules the *product rule*

$$ (xy)_a = x_a y + o(x)y_a $$

which can be contrasted with the familiar (Leibniz) product rule from calculus (here rephrased with a somewhat uncommon nomenclature, to highlight the correspondences and differences with Brzozowski's rule)

$$ (xy)_a = x_a y + xy_a. $$

In the work of Rutten, starting with [Rut98], a picture started to emerge in which Brzozowski's calculus of derivatives was absorbed into the framework of universal coalgebra. Notably, in [Rut03] and [Rut05] both product rules were considered as behavioural differential equations, or coinductive definitions, possessing unique solutions, and *defining* respectively the convolution product (Brzozowski's rule) and the shuffle product (Leibniz' rule) on the final coalgebra.

In the work of Bonsangue and Rutten together with the present author, starting with [WBR11], a coalgebraic presentation of the context-free languages

<footnote>* This work was supported by the Polish National Science Centre (NCN) grant 2012/07/E/ST6/03026.</footnote>
was given, in which Brzozowski's derivative rules (excluding the star rule) again play a crucial role. This work was based on a concretely presented extension of $2 \times \mathcal{P}_{\omega}(-^*)^A$-coalgebras into $2 \times -^A$-coalgebras, as in the following diagram:

<figure><img src="image_2.png" /></figure>

In [BHKR13], it was shown that the above diagram could be understood in terms of a distributive law of the monad $\mathcal{P}_{\omega}(-^*)$ over the cofree copointed functor on $2 \times -^A$, that is, over $(- \times (2 \times -^A), \pi_1)$ by means of a suitable quotient of distributive laws. This firmly established the connection between the work of [WBR11] and the general categorical framework of bialgebras and distributive laws, considered in e.g. [LPW00], [Bar04], [Jac06a], [Jac06b], [Kli11], and [JSS12], as well as to the (closely related) generalized powerset construction presented in [SBBR10] and [SBBR13].

Moreover, in [BRW12], the approach was generalized from formal languages to formal power series, thus giving a coalgebraic characterization of the constructively algebraic power series.

In [Win14], the author's PhD thesis, this extension was broken up into a two step process, as in the diagram,

<figure><img src="image_3.png" /></figure>

and it was noted that the first extension corresponded directly to the product rule (combined with the unit rule), whereas the second extension was simply an instance of ordinary determinization, applied to a coalgebra which is by itself infinite. This two-step process again easily generalizes from the setting of languages to the setting of noncommuting power series over commutative semirings; however, no general categorical presentation of this two-step process was given in the thesis.

The main aim of this paper is to give such a categorical presentation of this two-step process. This involves a setting including both distributive laws between monads $\lambda^0 : TS \Rightarrow ST$, distributive laws of a monad over a functor (or copointed functor) $\lambda^2 : SF \Rightarrow FS$, as well as a, suitably defined, distributive law of type $\lambda^1 : TF \Rightarrow FST$ (this definition will be given in Section 3).

In Section 4, we will present our main result, which states that the three laws as suggested above can be combined to form a new distributive law $\tilde{\lambda}$ of the composite monad $ST$ over $F$, if and only if a certain coherence axiom involving the three laws is satisfied. This construction works regardless whether $F$ is an ordinary or copointed functor. The proof that satisfaction of the coherence axiom
implies the multiplicative law of the distributive law of the composite monad ST over F was automatically derived using a Prolog program written for this purpose.

We then show that both the Brzozowski and Leibniz product rules, as well as the (simpler) pointwise rule defining the Hadamard product, can be cast into this setting, and that the coherence axiom is satisfied in these cases, and additionally present a counterexample where the coherence axiom is not satisfied. We conclude with a presentation of an extension of the generalized powerset construction to incorporate these two-step extensions.

*Related work.* All of the aforementioned references can be regarded as related work. In particular, [Che07] gives a similar coherence condition, for the existence of composite distributive laws in the context of distributive laws between monads. The relationships between [Che07] and the present paper involve some subtleties, and in Section 6, we will present a more detailed investigation of the relationship.

Additionally, [MMS13] and [Sch14] also give a compositional approach to distributive laws, however, in a setting different from our approach, not including the combination of distributive laws between monads and distributive laws of monads over functors into new distributive laws. In [Jac06b], a coinductive presentation of the shuffle product using a two-step process is also given, however, the coinductive definition of the multiplication there is not given using a distributive law.

*Acknowledgements.* For various discussions, comments, and criticism (hopefully in all cases taken as constructively as possible), I would like to thank Henning Basold, Marcello Bonsangue, Helle Hvid Hansen, Bart Jacobs, Bartek Klin, Jurriaan Rot, Jan Rutten, and Alexandra Silva, as well as to Charles Paperman for suggesting automation of the proofs (which in the end was carried out for only a part of just one of the propositions). Additionally I would like to thank the anonymous referees (as well as the anonymous referees of the earlier, rejected, submission) for a large amount of corrections and constructive comments.

# 2 Preliminaries

## 2.1 General preliminaries

We assume familiar the basic notions of category theory (functors, natural transformations, monads, (Eilenberg-Moore) algebras), of (commutative) monoids and semirings, and of coalgebras for a functor. These can be found in e.g. [Awo10] or [Mac71] for general categorical notions, and in [Rut00] for the basics of coalgebra.

An important endofunctor we will use is the functor $K \times -^A$ on **Set**, representing automata with output in $K$ over the input alphabet $A$, often called *Moore automata* but in this paper simply *K-automata*. The transition of coalgebras for this functor is represented as a pair $(o, \delta)$, called an *output-derivative pair*, with $\delta(x)(a)$ denoted by $x_a$. A final coalgebra for this functor exists, and
can be given by $(K\langle\langle A\rangle\rangle, O, \Delta)$, where $K\langle\langle A\rangle\rangle$ is the function space $A^* \to K$, $O(\sigma) = \sigma(1)$ and $\sigma_a(w) = \sigma(aw)$ for all $\sigma \in K\langle\langle A\rangle\rangle$, $a \in A$, and $w \in A^*$. Here, and elsewhere in this paper, 1 denotes the empty word.

A copointed endofunctor is a pair $(F, \epsilon)$, where $F$ is a C-endofunctor, and $\epsilon$ is a natural transformation $\epsilon: F \Rightarrow 1_C$. A coalgebra for a copointed endofunctor $(F, \epsilon)$ consists of a coalgebra $(X, \delta)$ for the endofunctor $F$, satisfying the condition that $\epsilon_X \circ \delta = 1_X$.

Of special interest to us are cofree copointed endofunctors, which can be constructed in any category that has binary products. Given an ordinary endofunctor $F$, the cofree copointed endofunctor on $F$ is the pair $(\mathrm{Id} \times F, \pi_1)$. For any functor $F$ such that a cofree copointed endofunctor on $F$ exists, there is an isomorphism between coalgebras for the ordinary endofunctor $F$, and coalgebras for the copointed endofunctor $(\mathrm{Id} \times F, \pi_1)$.

Given a monad $T$ (we will frequently refer to a monad simply using the name of its functorial part) and an endofunctor $F$, a $(T, F)$-bialgebra is a triple $(X, \alpha, \delta)$ such that $(X, \alpha)$ is an algebra for the monad $T$ and $(X, \delta)$ is a $F$-coalgebra. If $F$ is a copointed functor (here again, we often refer to the copointed functor simply using the name of the functor), we additionally require the coalgebraic part of a $(T, F)$-bialgebra to be a coalgebra for the copointed functor. (We will turn to $\lambda$-bialgebras involving a distributive law soon!)

Given a commutative semiring $K$ (in this paper, we will essentially only be concerned with commutative semirings), a $K$-semimodule $(M, 0, +, \times)$ consists of a commutative monoid $(M, 0, +)$ and an operation $\times: K \times M \to M$ (called scalar product) such that, for all $k, l \in k$ and $m, n \in M$:

$$ 
\begin{align*}
k \times (m + n) &= (k \times m) + (k \times n) \quad 1_K \times m = m \\
(k + l) \times m &= (k \times m) + (l \times m) \quad 0_K \times m = 0 \\
(kl) \times m &= k \times (l \times m) \quad k \times 0 = 0
\end{align*}
$$

For any commutative semiring $K^1$, the $K$-semimodules are exactly the algebras for the monad $(\mathrm{Lin}_K(-), \eta, \mu)$, where $\mathrm{Lin}_K(X)$ is the set of finitely supported functions on $X$, and, given a function $f: X \to Y$,

$$ \mathrm{Lin}_K(f) = y \mapsto \sum_{x \in f^{-1}(y)} f(x). $$

The multiplication of the monad, for any $X$ and any $f \in \mathrm{Lin}_K(\mathrm{Lin}_K(X))$, can be given by

$$ \mu_X(f) = x \mapsto \sum_{g \in \mathrm{supp}(f)} f(g) \cdot g(x) $$

and the unit of the monad, for any $x \in X$, by:

$$ \eta_X(x) = y \mapsto \text{if } x = y \text{ then } 1 \text{ else } 0 $$

<footnote n="1">¹ For a semiring $K$ that is not commutative, one can define two distinct monad structures on $\mathrm{Lin}_K(-)$, with a different multiplication, one corresponding to left-K-semimodules, and one corresponding to right K-semimodules. When $K$ is commutative, these two monads are identical.</footnote>
Given some $\sigma \in \text{Lin}_K(X)$ and some $x \in X$, we furthermore write $[\sigma \downarrow x]$ for the application of $\sigma$ at $x$.

Given a commutative semiring $K$, a $K$-algebra<fnref n="2" /> (see e.g. [Eil76]) is a tuple $(X, 0, 1, +, \cdot, \times)$ such that $(X, 0, 1, +, \cdot)$ is a semiring, $(X, 0, +, \times)$ is a $K$-semimodule, such that for all $k \in K$ and $x \in X$:

$$ (k \times 1) \cdot x = k \times x = x \cdot (k \times 1) $$

An equivalent, and as it turns out for us more convenient, characterization is the following: a $K$-algebra is a tuple $(X, 0, 1, +, \cdot, \times)$ such that $(X, 1, \cdot)$ is a monoid, $(X, 0, +, \times)$ is a $K$-semimodule, furthermore satisfying the following axioms:

$$ x \cdot (y + z) = x \cdot y + x \cdot z $$

$$ (x + y) \cdot z = x \cdot z + y \cdot z $$

$$ (k \times 1) \cdot x = k \times x = x \cdot (k \times 1) $$

(Note that the pair of semiring axioms $0 \cdot x = 0 = x \cdot 0$ can be derived from the pair of axioms on the third line.)

For some semirings $K$, the categories of $K$-semimodules and $K$-algebras correspond to familiar categories. We summarize some of these in the following table:

<table><thead><tr><th>K</th><th>K-semimodules</th><th>K-algebras</th></tr></thead><tbody><tr><td>B</td><td>join-semilattices</td><td>idempotent semirings</td></tr><tr><td>N</td><td>commutative monoids</td><td>semirings</td></tr><tr><td>Z</td><td>abelian groups</td><td>rings</td></tr></tbody></table>

Moreover, it is easily verified that the monad $\text{Lin}_B(-)$ is naturally isomorphic to the finite powerset monad $\mathcal{P}_\omega$.

## 2.2 Distributive laws between monads

We now summarize the definitions and some important facts about distributive laws between monads, which can be found in e.g. [Bec69] and [BW85].

Given monads $(S, \mu^S, \eta^S)$ and $(T, \mu^T, \eta^T)$, a distributive law of the monad $T$ over the monad $S$ is a natural transformation $\lambda : TS \Rightarrow ST$ such that the four diagrams of natural transformations

<figure><img src="image_4.png" /></figure>

<footnote n="2">² In the literature often called a unital associative algebra</footnote>
<figure><img src="image_5.png" /></figure>

commute.

In the presence of a distributive law of a monad T over another monad S, we obtain, amongst other things, the following:

1. A monad structure on the composite functor ST, given by:

$$ \eta^{ST} = \eta^S T \circ \eta^T \quad \text{and} \quad \mu^{ST} = S\mu^T \circ \mu^S TT \circ S\lambda T $$

2. A lifting of the monad S to a monad $\hat{S}$ in the category $C^T$ of T-algebras, with the functorial part of $\hat{S}$ given by:

$$ \hat{S}(X, \alpha) = (SX, S\alpha \circ \lambda_X) $$

3. An isomorphism of categories between the categories of algebras for the monad ST and algebras for the monad $\hat{S}$. Given an $\hat{S}$-algebra $(X, \alpha^T, \alpha^S)$, the corresponding ST-algebra can be given by $(X, \alpha^S \circ S\alpha^T)$, and given a ST-algebra $(X, \alpha)$, the corresponding $\hat{S}$-algebra can be given by $(X, \alpha \circ \eta^S_{TX}, \alpha \circ S\eta^T_X)$. These constructions are mutually inverse, as shown in [Bec69, Section 2].

In the case where $T = -^*$ and $S = \text{Lin}_K(-)$ (where K is a commutative semiring), there is a distributive law $\lambda : (\text{Lin}_K(-))^* \Rightarrow \text{Lin}_K(-^*)$ of T over S, given by:

$$ \lambda_X \left( \prod_{i=1}^{n} \sum_{j=1}^{m_i} k_{ij} \times x_{ij} \right) = \sum_{j_1=1}^{m_1} \cdots \sum_{j_n=1}^{m_n} \left( \prod_{i=1}^{n} k_{ij_i} \times \prod_{i=1}^{n} x_{ij_i} \right) $$

(recall that $\times$ is the scalar product, and thus, the $k_{ij}$ here are scalars of $K$!) Here the product symbol $\prod$ denotes the operation on the monoid structure, and the summation symbol $\sum$ and times $\times$ denote the (sum and scalar product) on the semimodule structure, respectively.

It is well-known, at least<fnref n="3" /> in the cases of the semirings $\mathbb{B}$, $\mathbb{N}$, and $\mathbb{Z}$ (and probably in the remaining cases as well—nevertheless we give a full proof in the appendix), that this is a distributive law of $-^*$ over $\text{Lin}_K(-)$:

**Proposition 1.** The natural transformation $\lambda$ as given above is a distributive law of the monad $\text{Lin}_K(-)$ over the monad $-^*$.

We let $K\langle - \rangle = \text{Lin}_K(-^*)$ denote the resulting composite monad. Elements of $K\langle X \rangle$ can be identified with noncommuting polynomials in variables from X.

<footnote n="3">³ See e.g. [Bec69] for $\mathbb{Z}$ and [Jac06a] for $\mathbb{N}$ and $\mathbb{B}$</footnote>
Moreover, the algebras for this monad are precisely the K-algebras: by definition, a K-algebra is both a monoid and a semimodule additionally satisfying

$$
\begin{align*}
x \cdot (y + z) &= x \cdot y + x \cdot z \\
(x + y) \cdot z &= x \cdot z + y \cdot z \\
(k \times 1) \cdot x &= k \times x = x \cdot (k \times 1)
\end{align*}
$$

for elements $x, y, z$ and scalars $k$ and an algebra for the monad $K\langle - \rangle$ is both a monoid and a semimodule additionally satisfying

$$
\prod_{i=1}^{n} \sum_{j=1}^{m_i} k_{ij} \times x_{ij} = \sum_{j_1=1}^{m_1} \cdots \sum_{j_n=1}^{m_n} \left( \prod_{i=1}^{n} k_{ij_i} \times \prod_{i=1}^{n} x_{ij_i} \right)
$$

It is easily verified that these two conditions are equivalent.

2.3 Distributive laws of a monad over a (copointed) endofunctor

We now turn to a brief summary of distributive laws of monads over endofunc-
tors and copointed endofunctors. The material which now follows can all be
found in either [Bar04] or [JSS12]; supplementary presentations can be found in
e.g. [Jac06a], [Jac06b], [Kli11], and [LPW00] (in which the notions of distribu-
tive laws of monads over endofunctors and copointed endofunctors were first
considered).

Given a monad (T, μ, η) and an endofunctor F on any category C, a distribu-
tive law of the monad T over F is a natural transformation λ : TF ⇒ FT such
that the two diagrams of natural transformations

<figure><img src="image_6.png" /></figure>

commute.

Given a distributive law $\lambda$ of $T$ over $F$, a $\lambda$-bialgebra is a $(T, F)$-bialgebra for which the following diagram commutes:

<figure><img src="image_7.png" /></figure>

A distributive law of a monad (T, η, μ) over a copointed endofunctor (F, ϵ)
is a distributive law of the monad over the (ordinary) endofunctor F, such that
additionally the diagram

<figure><img src="image_8.png" /></figure>
commutes.

For distributive laws of a monad over a copointed endofunctor, bialgebras can again be defined: the only modification needed here is that we additionally require $(X, \delta)$ to be a coalgebra for the copointed endofunctor $F$. Note that any distributive law $\lambda$ of a monad $T$ over an ordinary functor $F$ extends to a distributive law $\lambda'$ of $T$ over the cofree copointed functor $(\mathrm{Id} \times F)$, such that the $\lambda$-bialgebras and $\lambda'$-bialgebras are isomorphic as categories.

In the presence of a distributive law $\lambda$ of $T$ over $F$, we obtain, amongst other things, the following (both for ordinary and copointed endofunctors, see e.g. [Bar04] for proofs):

1. A lifting of $F$ to a functor $\hat{F}$ in the category of algebras for the monad $T$, and of $T$ to a functor $\hat{T}$ the category of $F$-coalgebras, together with an isomorphic correspondence between the categories of $\lambda$-bialgebras, $\hat{F}$-coalgebras, and algebras for the monad $\hat{T}$.

2. If $F$ has a final coalgebra $(\Omega, \omega)$, there is a unique algebra $\xi$ for the monad $T$ on $\Omega$ such that $(\Omega, \xi, \omega)$ is a $\lambda$-bialgebra, which moreover is a final $\lambda$-bialgebra.

An important instance of a distributive law, considered in e.g. [JSS12], is the law of the functor $K \times -^A$ over the monad $\mathrm{Lin}_K(-)$ where $K$ is any semiring$^4$, given by:

$$ \lambda_X \left( \sum_{i=1}^{n} k_i \times (o_i, a \mapsto d_{ia}) \right) = \left( \sum_{i=1}^{n} k_i o_i, a \mapsto \sum_{i=1}^{n} k_i \times d_{ia} \right) $$

This distributive law can be obtained canonically by means of the strength operation (see e.g. [JSS12]), using the obvious $K$-semimodule structure on $K$ itself. The bialgebras for this distributive law are precisely the structures that are both $K$-automata and $K$-semimodules, such that the output and derivative (with respect to an arbitrary alphabet symbol) are both linear mappings. A concrete formulation is the following: a $K$-linear automaton$^5$ is a tuple $(X, 0, +, \times, o, \delta)$ such that $(X, 0, +, \times)$ is a $K$-semimodule, $(X, o, \delta)$ is a $K$-automaton, and $o$ and $\delta(-)(a)$ (for each $a \in A$) are linear mappings.

## 2.4 The generalized powerset construction

We now turn to a summary of some of the main observations from [SBBR10] and [SBBR13] pertaining to the generalized powerset construction (many instances of which can be found in these two papers as examples). Beyond that, we also sketch how the 'generalized powerset construction' framework can be extended to distributive laws over (cofree) copointed functors, and highlight some of the (additional) subtleties that arise in this case.

<footnote>$^4$ If $K$ is not commutative, we can consider left $K$-semimodules, but for this paper, this is not relevant.</footnote>

<footnote>$^5$ called linear weighted automata in e.g. [BBB$^{+}$12]</footnote>
Given a (possibly copointed) endofunctor $F$ such that a final $F$-coalgebra exists, a monad $T$ (on the same category), and a distributive law of $T$ over $F$, any $FT$-coalgebra $(X, \delta)$ (if $F$ is copointed, we additionally require that $\epsilon_{TX} \circ \delta = \eta_X$) can be extended canonically to an $F$-coalgebra $(TX, \hat{\delta})$, where $\hat{\delta}$ can be specified as:

$$ \hat{\delta} = F\mu_X \circ \lambda_{TX} \circ T\delta $$

In fact, it follows that $(TX, \mu_X, \hat{\delta})$ is a $\lambda$-bialgebra (and, hence, that $FTX$ has the structure of an algebra for the monad $T$). If $F$ has a final coalgebra $(\Omega, \omega)$, we thus obtain

<figure><img src="image_9.png" /></figure>

where $\llbracket - \rrbracket$ is a morphism of $\lambda$-bialgebras to the unique $\lambda$-bialgebra on the final $F$-coalgebra. If $F$ is copointed, note that

$$ \begin{aligned} \epsilon_{TX} \circ \hat{\delta} &= \epsilon_{TX} \circ F\mu_X \circ \lambda_{TX} \circ T\delta = \mu_X \circ \epsilon_{TTX} \circ \lambda_{TX} \circ T\delta \\ &= \mu_X \circ T\epsilon_X \circ T\delta = \mu_X \circ T\eta_X = 1_{TX} \end{aligned} $$

so that $\hat{\delta}$ is indeed a coalgebra for the copointed functor.

When the functor $F$ is a cofree copointed functor of the form $(\mathrm{Id} \times G, \pi_1)$, note that $\delta$ has to be of the form $(\eta_X, \zeta)$, where $\zeta$ is an (ordinary) $GT$-coalgebra, and because $\hat{\delta}$ is a coalgebra for the cofree copointed functor, it has to be of the form $(1_{TX}, \zeta^b)$ for some $\zeta^b$. Similarly, $\omega$ has to be of the form $(1_\Omega, \psi)$, where $(\Omega, \psi)$ is the final $G$-coalgebra. Now note that there is a correspondence of commuting diagrams of the form

<figure><img src="image_10.png" /></figure>

and:

<figure><img src="image_11.png" /></figure>

However, in general we are *not* guaranteed that the second diagram occurs as the result of an ordinary distributive law of $T$ over $G$. Hence, in general, although we are guaranteed that $TX \times GTX$ has the structure of an algebra for the monad $T$, we do not have this guarantee of GTX itself (this may in fact fail, e.g. for GSOS rules that cannot be presented using the simple SOS format). On the other hand, we are still guaranteed that $\llbracket - \rrbracket$ is a $T$-algebra morphism, because this follows from the upper diagram.
### 3 Distributive laws of a monad over a (copointed) endofunctor into a composite monad

In this section, we present a definition of a new (as far as the author is aware) type of distributive law, which allows us to formulate the ‘two-step’ generalized powerset construction. We start by giving the general formulation, before turning to the main examples.

Given two monads $(S, \mu^S, \eta^S)$, $(T, \mu^T, \eta^T)$ such that a distributive law $\lambda^0: TS \Rightarrow ST$ exists, and an endofunctor $F$, on any category $\mathcal{C}$, a distributive law of the monad $T$ over $F$ into the composite monad $ST$ is a natural transformation $\lambda: TF \Rightarrow FST$ such that the two diagrams of natural transformations

<figure><img src="image_12.png" /></figure>

commute.

We can again define a suitable notion of a $\lambda$-bialgebra for a distributive law of $T$ over $F$ into the composite monad $ST$. For such a $\lambda$, a $\lambda$-bialgebra $(X, \alpha, \delta)$ is a $(ST, F)$-bialgebra such that the diagram

<figure><img src="image_13.png" /></figure>

commutes (note that we can here replace $\alpha \circ \eta_{TX}^S$ with $\alpha^T$).

A distributive law $\lambda$ of a monad $(T, \eta, \mu)$ over a copointed endofunctor $(F, \epsilon)$ into a composite monad is a distributive law of the monad over the (ordinary) endofunctor $F$ into the same composite monad, such that additionally the diagram

<figure><img src="image_14.png" /></figure>

commutes. Again, the corresponding notion of a $\lambda$-bialgebra is obtained by adding the additional requirement that $(X, \delta)$ is a coalgebra for the copointed functor $F$.

The following result is unspectacular, but will be useful for us later on:

**Lemma 2.** Given monads $(S, \eta^S, \mu^S)$ and $(T, \eta^T, \mu^T)$, and a (possibly copointed) endofunctor $F$, and a distributive law $\lambda^0: TS \Rightarrow ST$, if a natural transformation $\lambda: TF \Rightarrow FT$ is a distributive law of $T$ over $F$, then $\lambda = F\eta^S T \circ \lambda$ is a distributive law of $T$ over $F$ into the composite monad $ST$. If $\eta$ is pointwise monic and $F$ preserves monos, the converse also holds.
## 3.1 Product rules as distributive laws

Instantiating $S = \text{Lin}_K(-)$, $T = -^*$, and $F = K \times -^A$, we can model each of the three product rules as distributive laws of the monad $(T, \eta^T, \mu^T)$ over the copointed functor $(\text{Id} \times F, \pi_1)$ into the composite monad $(ST, \eta^{ST}, \mu^{ST})$ as follows:

1. The Brzozowski product rule can be specified as

$$ \lambda_X \left( \prod_{i=1}^{n} (x_i, o_i, a \mapsto d_{ia}) \right) = \left( \prod_{i=1}^{n} x_i, \prod_{i=1}^{n} o_i, a \mapsto \sum_{i=1}^{n} \left( \prod_{k=1}^{i-1} o_i \right) \times \left( d_{ia} \cdot \prod_{k=i+1}^{n} x_i \right) \right) $$

or equivalently inductively as:

$$ \begin{gathered} \lambda_X(1) = (1, 1, a \mapsto 0) \\ \lambda_X(x, o, a \mapsto d_a)w = (x\pi_0(\lambda_X(w)), o\pi_1(\lambda_X(w)), a \mapsto d_a\pi_0(\lambda_X(w)) + o\pi_2(\lambda_X(w))(a)) \end{gathered} $$

The latter pair of equations can be more conveniently represented using the output-derivative notation as:

$$ \begin{gathered} o(1) = 1 \qquad 1_a = 0 \\ o(xw) = o(x)o(w) \quad (xw)_a = x_a w + o(x)w_a \end{gathered} $$

2. The Leibniz product rule can be given as

$$ \lambda_X \left( \prod_{i=1}^{n} (x_i, o_i, a \mapsto d_{ia}) \right) = \left( \prod_{i=1}^{n} x_i, \prod_{i=1}^{n} o_i, a \mapsto \sum_{i=1}^{n} \left( \left( \prod_{k=1}^{i-1} x_i \right) \cdot d_{ia} \cdot \prod_{k=i+1}^{n} x_i \right) \right) $$

or inductively and using the output-derivative notation as:

$$ \begin{gathered} o(1) = 1 \qquad 1_a = 0 \\ o(xw) = o(x)o(w) \quad (xw)_a = x_a w + xw_a \end{gathered} $$

3. Finally, the pointwise (Hadamard) product rule is given as

$$ \lambda_X \left( \prod_{i=1}^{n} (o_i, a \mapsto d_{ia}) \right) = \left( \prod_{i=1}^{n} o_i, a \mapsto \prod_{k=1}^{n} d_{ia} \right) $$

or inductively and using the output-derivative notation as:

$$ \begin{gathered} o(1) = 1 \qquad 1_a = 1 \\ o(xw) = o(x)o(w) \quad (xw)_a = x_a w \end{gathered} $$
In the case of the Brzozowski and Leibniz product rules, it can be verified that they yield distributive laws using a lengthy verification.

**Proposition 3.** *The Brzozowski and Leibniz product rule both are distributive laws of $-^*$ over the copointed endofunctor $(\mathrm{Id} \times F, \pi_1)$ into the composite monad $K(-)$.*

In the case of the Hadamard product, everything is a bit easier.

**Proposition 4.** *The pointwise product rule is a distributive law of $-^*$ over the endofunctor $F$ into the composite monad $K(-)$.*

*Proof.* This follows from the fact that the Hadamard product can be given as a pointwise distributive law of $-^*$ over $K \times -^A$ obtained using the strength operation and multiplication over $K$ giving its monoid structure (see e.g. [Jac06b] for a detailed discussion of distributive laws obtained using strength). By Lemma 2, this distributive law yields another distributive law into the composite monad.

□

We will henceforth refer to the three above distributive laws as $\lambda^{\mathrm{brz}}$, $\lambda^{\mathrm{lei}}$, and $\lambda^{\mathrm{had}}$, respectively.

From the above propositions and the definition of $\lambda$-bialgebras for distributive laws of a monad over a functor into another monad, it follows directly that any $\lambda$-bialgebra for any of the above distributive laws satisfies the corresponding product rule for arbitrary elements. For example, it is easy to see from the definitions that the $\lambda$-bialgebras for the Brzozowski product rule are precisely the $(T, F)$-bialgebras that satisfy the unit and product rule

$$ \begin{array}{l} o(1) = 1 \\ 1_a = 0 \end{array} \qquad \begin{array}{l} o(xy) = o(x)o(y) \\ (xy)_a = x_a y + o(x)y_a \end{array} $$

for arbitrary elements $x$ and $y$ of the bialgebra and alphabet symbols $a$. *Mutatis mutandis*, the same holds for the two other product rules.

# 4 Composite distributive laws

In this section we will introduce a *coherence axiom*, comparable to but different from the Yang-Baxter condition presented in [Che07]. The relation with the work in [Che07] will be discussed in Section 6. We consider a setting, where we are given monads $S$ and $T$, a (possibly copointed) endofunctor $F$, on an arbitrary category $\mathcal{C}$, together with three distributive laws, as follows:

- $\lambda^0 : TS \Rightarrow ST$, a distributive law of $T$ over $S$.

- $\lambda^1 : TF \Rightarrow FST$, a distributive law of $T$ over $F$ into the composite monad $ST$.

- $\lambda^2 : SF \Rightarrow FS$, a distributive law of $S$ over $F$.
For such triples<fnref n="6" />, we can compose the distributive laws as follows, yielding a new natural transformation $\hat{\lambda} : (ST)F \Rightarrow F(ST)$ given by:

$$STF \underset{\sim}{\overset{S\lambda^1}{\longrightarrow}} SFST \underset{\sim}{\overset{\lambda^2ST}{\longrightarrow}} FSST \underset{\sim}{\overset{F\mu^{ST}}{\longrightarrow}} FST$$

A triple of distributive laws $(\lambda^0, \lambda^1, \lambda^2)$ as above is said to satisfy the coherence axiom whenever the following diagram commutes:

$$\begin{tikzcd}[column sep=2.8em, row sep=2.8em]
TSF \arrow[r, "T\lambda^2"] \arrow[d, "\lambda^0F"] & TFS \arrow[r, "\lambda^1S"] \arrow[d, "\lambda^0F"'] & FSST \arrow[r, "FS\lambda^0"] \arrow[d, "F\mu^{ST}"] & FSST \\
STF \arrow[r, "S\lambda^1"] \arrow[d, "\lambda^1F"] & SFST \arrow[r, "\lambda^2ST"] \arrow[d, "\lambda^1F"'] & FSST \arrow[r, "F\mu^{ST}"] \arrow[d, "F\mu^{ST}"] & FST
\end{tikzcd} \quad (2)$$

As it turns out, the coherence axiom is a sufficient and necessary condition for $\hat{\lambda}$ to be a distributive law:

**Theorem 5.** Given three distributive laws as above for monads $S$ and $T$ and a functor (or copointed functor) $F$, the natural transformation $\hat{\lambda}$ is a distributive law of the composite monad $ST$ over the functor (or copointed functor) $F$ if and only if the coherence axiom is satisfied.

Perhaps interesting to note, after initially finding myself unable to prove one of the directions of the above theorem by hand (the initial aim was to prove that a triple of distributive laws always yields a composite distributive law), I wrote a Prolog program generating all the possible ways to go from $STSTF$ to $STF$, together with equivalences determined by naturality squares, the multiplicative laws for the monad, and the various distributive laws (however excluding the unit laws), as well as all of these equivalences with any functor applied to it. Using this program, the source of which can be found at

http://www.mimuw.edu.pl/~jwinter/distlaws.prolog

the following facts were found:

1. There are 784 different ways of going from $STSTF$ to $STF$, using compositions of arbitrary natural transformations satisfying the regular expression:

$$(S|T|F)^*(\mu^S|\mu^T|\lambda^0|\lambda^1|\lambda^2)(S|T|F)^*$$

2. Without the coherence axiom, and using the equivalence relation named above, these divide up into two different equivalence classes (of sizes 218 and 566, respectively).

3. With the coherence axiom added, the two equivalence classes collapse into one.

<footnote n="6">⁶ In some of the literature, monads are called triples, but in this paper it simply means a list of three elements.</footnote>
After the proof was *found* automatically, it was, however, easily *verified* by hand, and transformed into a (rather large) commuting diagram.

Later, it was found (by hand) that the coherence axiom can also be derived from the existence of a composite distributive law, turning the theorem into one giving a sufficient and necessary condition, and indeed a counterexample (soon to be presented) to the coherence axiom was found. (Note that neither the theorem, nor the falling apart of the paths into two equivalence classes is *by itself* a proof that there are counterexamples to the coherence axiom, but only a proof that the coherence axiom cannot be derived using one particular method.)

Furthermore, it turns out that each of the distributive laws from Section 3.1 satisfies the coherence axiom, when combined with the distributive laws presented in Sections 2.2 and 2.3:

**Proposition 6.** The three distributive laws for the Brzozowski, Leibniz, and Hadamard product rules satisfy the coherence axiom, when instantiating $\lambda^0$ with the distributive law between monads presented in Section 2.2, and instantiating $\lambda^2$ with the distributive law of S over F from Section 2.3.

We will henceforth refer to the extensions of the three distributive laws earlier named as $\lambda^{brz}$, $\lambda^{lei}$, and $\lambda^{had}$, respectively.

We now turn to the counterexample, consisting of a distributive law of T over F into the composite monad ST, which, together with the same $\lambda^2$ and $\lambda^0$ as before, does not satisfy the coherence axiom.

**Counterexample 1.** Consider the natural transformation given by $\lambda^1 : (\mathbb{N} \times -^A)^* \Rightarrow \mathbb{N} \times \mathbb{N}(-)^A$ given by

$$ \lambda_X^1 \left( \prod_{i=1}^n (x_i, o_i, a \mapsto d_{ia}) \right) = \left( \prod_{i=1}^n x_i, \sum_{i=1}^n o_i, a \mapsto \prod_{i=1}^n d_{ia} \right) $$

This distributive law can again be given by means of a (pointwise) distributive law from $-^*$ over $\mathbb{N} \times -^A$ using the strength operator, this time by considering the additive monoid structure on $\mathbb{N}$ (as opposed to the multiplicative monoid structure, which yields the Hadamard product).

Now consider

$$ ((x, 1, a \mapsto x) + (x, 1, a \mapsto x)) \cdot (x, 1, a \mapsto x) $$

which is an element of $TSF\{x\}$. It now follows that by applying

$$ F\mu^{ST} \circ FS\lambda^0 \circ \lambda^1 S \circ T\lambda^2 $$

we obtain an element $(y, o, d) \in FST\{x\}$ such that $o = 3$, whereas by applying

$$ F\mu^{ST} \circ \lambda^2 ST \circ S\lambda^1 \circ \lambda^0 F $$

we obtain an element $(y', o', d') \in FST\{x\}$ such that $o' = 4$. This proves that the coherence axiom is not satisfied, and hence, by Theorem 5, also that $\lambda$, although a natural transformation, is not a distributive law of the composite monad ST over F.
**Proposition 7.** Given three distributive laws $\lambda^0, \lambda^1, \lambda^2$ as above, such that $\hat{\lambda}$ is a distributive law over ST over F, a (ST, F)-bialgebra $(X, \alpha, \delta)$ is a $\hat{\lambda}$-bialgebra if and only if $(X, \alpha^S, \delta)$ is a $\lambda^2$-bialgebra and $(X, \alpha^T, \delta)$ is a $\lambda^1$-bialgebra.

*Proof.* We will establish the result by establishing the following implications (in the diagrams, each of the (internal) faces commutes by either one of the assumed algebras or bialgebras, one of the axioms for monads or distributive laws, a naturality square, or a functor applied to any of these types of diagrams):

- If $(X, \alpha, \delta)$ is a $\hat{\lambda}$-bialgebra, then $(X, \alpha^T, \delta)$ is a $\lambda^1$-bialgebra. This is established by the following diagram:

<figure><img src="image_15.png" /></figure>

- If $(X, \alpha, \delta)$ is a $\hat{\lambda}$-bialgebra, then $(X, \alpha^S, \delta)$ is a $\lambda^2$-bialgebra. This is established by the following diagram:

<figure><img src="image_16.png" /></figure>
- If $(X, \alpha^T, \delta)$ is a $\lambda^1$-bialgebra and $(X, \alpha^S, \delta)$ is a $\lambda^2$-bialgebra, then $(X, \alpha, \delta)$ is a $\hat{\lambda}$-bialgebra. This is established by the following diagram:

<figure><img src="image_17.png" /></figure>

From the preceding proposition, we can now directly conclude that, given a commutative semiring $K$, the corresponding $\hat{\lambda}^{\text{brz}}$-bialgebras are precisely the structures $(X, 0, 1, +, \cdot, \times, o, \delta)$ such that $(X, 0, 1, +, \cdot, \times)$ is a $K$-algebra, that $(X, 0, +, \times, o, \delta)$ is a $K$-linear automaton, and such that additionally the unit and product rule are satisfied for arbitrary elements. Again, *mutatis mutandis*, the same holds for the Leibniz and pointwise product rules. It may be worthwhile to note that (in the context of a singleton alphabet $A$ and a field as underlying semiring) the bialgebras for $\hat{\lambda}^{\text{lei}}$, are precisely *differential algebras* (as defined in e.g. [RR08]) together with output functions that are $K$-algebra morphisms.

Another corollary of this proposition is that the final $\hat{\lambda}$-bialgebra has a structure compatible with the final $\lambda^2$-bialgebra, because the final $\hat{\lambda}$-bialgebra is a $\lambda^2$-bialgebra (by the preceding proposition) compatible with the final $F$-coalgebra (as a consequence of [Bar04, Corollary 3.4.19]), and again by [Bar04, Corollary 3.4.19], there is a *unique* $\lambda^2$-bialgebra compatible with the final $F$-coalgebra. By similar reasoning, the final $\hat{\lambda}$-bialgebra also has a structure with the final $\lambda^1$-bialgebra. So, the final $\hat{\lambda}$-bialgebra can now be seen to naturally extend both the final $\lambda^1$-bialgebra and the final $\lambda^2$-bialgebra, inheriting the coalgebraic structure from the final $F$-coalgebra, and with algebraic structure compatible to that of the final bialgebras for $\lambda^1$ and $\lambda^2$.

# 5 The generalized powerset construction for composite distributive laws

We can now formulate a two-step version of the generalized powerset construction, in the setting where we are given three distributive laws $\lambda^0, \lambda^1, \lambda^2$ as in the previous section. Here the extensions can be specified as

$$ \delta^{\sharp} = F \mu_X^{ST} \circ \lambda_{STX}^1 \circ T \delta \quad \text{and} \quad \hat{\delta} = F \mu_{TX}^S \circ \lambda_{STX}^2 \circ S \delta^{\sharp}. $$
# 6 Comparison to the coherence condition from [Che07]

In [Che07], a similar coherence condition to the one from this paper is presented, providing a way of iterating distributive laws between which a coherence condition similar to (but simpler than) the one presented in this paper is used. We will concentrate on the specific case of just three monads with interacting distributive laws, as the more general iterated cases are less directly relevant to the present paper. In this case, the main result from [Che07] instantiates as:

**Proposition 10.** Given monads $(S, \eta^S, \mu^S)$, $(T, \eta^T, \mu^T)$, and $(U, \eta^U, \mu^U)$, together with distributive laws $\lambda^0 : UT \Rightarrow TU$, $\lambda^1 : US \Rightarrow SU$, and $\lambda^2 : TS \Rightarrow ST$, if the diagram

<figure><img src="image_18.png" /></figure>

(called the coherence condition or Yang-Baxter condition) commutes, the natural transformations

$$ \lambda^2 U \circ T \lambda^1 : (TU)S \Rightarrow S(TU) $$

and

$$ S\lambda^0 \circ \lambda^1 T : U(ST) \Rightarrow (ST)U $$

are distributive laws between monads (of the composite monad TU over S, and of U over the composite monad ST), respectively). Moreover both of these laws yield the same composite monad on STU.

A difference between this result and the corresponding result from our paper is that the result in [Che07] is only presented in one direction, instead of as an equivalence. Thus, one can wonder if in this case, too, the result can be turned into an equivalence. In fact, it can be stated in the form of the following three-way equivalence:

**Proposition 11.** Given monads S, T, and U and distributive laws $\lambda^0$, $\lambda^1$, and $\lambda^2$ as in the previous proposition, the following are equivalent:

1. The Yang-Baxter condition holds.

2. $\lambda^2 U \circ T \lambda^1$ is a distributive law of the composite monad TU over S.

3. $S\lambda^0 \circ \lambda^1 T$ is a distributive law of U over the composite monad ST.

As a variant on this result, bridging the gap between it and our result, we will move to a setting where, rather than three monads, we have two monads, $(S, \eta^S, \mu^S)$ and $(T, \eta^T, \mu^T)$ and an endofunctor $F$, together with a distributive law between monads $\lambda^0 : TS \Rightarrow ST$, and two distributive laws of the monad-over-endofunctor type, $\lambda^1 : TF \Rightarrow FT$, and $\lambda^2 : SF \Rightarrow FS$. We now obtain the following result, in much the same manner as before:
**Proposition 12.** Given monads $(S, \eta^S, \mu^S)$, $(T, \eta^T, \mu^T)$, and an endofunctor $F$, together with distributive laws $\lambda^0 : TS \Rightarrow ST$, $\lambda^1 : TF \Rightarrow FT$, and $\lambda^2 : SF \Rightarrow FS$, the following are equivalent:

1. The Yang-Baxter condition holds, as follows:

$$ \begin{array}{ccc} TSF & \underset{\lambda^0 F}{\overset{T\lambda^2}{\rightleftharpoons}} & TFS \underset{F\lambda^0}{\overset{\lambda^1 S}{\rightleftharpoons}} FTS \\ \Big\downarrow & & \Big\downarrow \\ STF & \underset{S\lambda^1}{\overset{S\lambda^1}{\rightleftharpoons}} & SFT \underset{FST}{\overset{\lambda^2 T}{\rightleftharpoons}} \end{array} \qquad (3) $$

2. $\lambda^2 T \circ S\lambda^1$ is a distributive law of the composite monad $ST$ over $F$.

(Note that this result is very similar to, but different from, one direction of [BMSZ15, Proposition 7.1], which is concerned with two monads, an endofunctor, and one distributive law between these monads, and two Kleisli-type laws, i.e. laws of the endofunctor over both of the monads.)

In fact, the result can be related to the results from Section 4 by means of Lemma 2 and the following proposition:

**Proposition 13.** Given monads $(S, \eta^S, \mu^S)$ and $(T, \eta^T, \mu^T)$, an endofunctor $F$, and distributive laws $\lambda^0 : TS \Rightarrow ST$, $\lambda^1 : TF \Rightarrow FT$, and $\lambda^2 : SF \Rightarrow FS$, the Yang-Baxter condition (3) holds if and only if the law $\lambda^1 = F\eta^S T \circ \lambda^1 : TF \Rightarrow FST$ makes diagram (2) (Section 4) commute.

Connecting this result to the three product rules mentioned in this paper, we recall that the Hadamard product rule can also be given directly as a distributive law of type $TF \Rightarrow FT$ (with $T = -^*$, $F = K \times -^A$) using the strength operator. This law can be given concretely by

$$ \lambda_X \left( \prod_{i=1}^{n} (o_i, a \mapsto d_{ia}) \right) = \left( \prod_{i=1}^{n} o_i, a \mapsto \prod_{k=1}^{n} d_{ia} \right) $$

with the difference that the right hand side is now regarded as an element of $FT$, instead of an element of $FST$ (with $S = \text{Lin}_K(-)$). The Leibniz and Brzozowski product rules, however, do not fit into this simpler scheme, as a direct result of the occurrence of a summation on the right hand side.

It thus turns out that, while the results from [Che07] are easily modified to a coalgebraic setting with laws $\lambda^0 : TS \Rightarrow ST$, $\lambda^1 : TF \Rightarrow FT$, and $\lambda^2 : SF \Rightarrow FS$, the usage of distributive laws into a composite monad (where $\lambda^1$ is of the form $TF \Rightarrow FST$) allows us to specify product rules of the type $(xy)_a = x_y a + o(x)y_a$, where a summation occurs in the right hand side, that are not possible to specify in a two-step mechanism using the simple variant of the result in [Che07].

Additionally, in the case of distributive laws into composite monads, we require an octagonal coherence condition, rather than the hexagonal condition from [Che07].
# 7 Further directions

One interesting direction for future work consists of making a further generalization from copointed functors to comonads. Another possible direction, owing inspiration to [Wor09] (where it is shown that K-algebras are precisely the monoids in the monoidal category of K-semimodules), consists of investigating whether we can reverse the order of the two-step process in the concrete setting of product rules, going from $X$ via $\text{Lin}_K(X)$ to $K\langle X\rangle$ instead of via $X^*$. Finally, it may be very worthwhile to further develop the Prolog-program, developed here in an *ad hoc* manner to prove a part of Theorem 5, into a more general tool able to (at least in certain contexts) prove commutativity of diagrams.

# References

[Awo10] Steve Awodey. *Category Theory*. Oxford University Press, 2010.

[Bar04] Falk Bartels. *On Generalized Coinduction and Probabilistic Specification Formats*. PhD thesis, Vrije Universiteit Amsterdam, 2004.

[BBB$^+$12] Filippo Bonchi, Marcello M. Bonsangue, Michele Boreale, Jan Rutten, and Alexandra Silva. A coalgebraic perspective on linear weighted automata. *Information and Computation*, 211:77–105, 2012.

[Bec69] Jon Beck. Distributive laws. In *Seminar on triples and categorical homology theory*, pages 119–140. Springer, 1969.

[BHKR13] Marcello M. Bonsangue, Helle H. Hansen, Alexander Kurz, and Jurriaan Rot. Presenting distributive laws. In Reiko Heckel and Stefan Milius, editors, *CALCO*, volume 8089 of *Lecture Notes in Computer Science*, pages 95–109. Springer, 2013.

[BMSZ15] Filippo Bonchi, Stefan Milius, Alexandra Silva, and Fabio Zanasi. Killing epsilons with a dagger: A coalgebraic study of systems with algebraic label structure. *Theoret. Comput. Sci.*, 604:102–126, 2015. http://dx.doi.org/10.1016/j.tcs.2015.03.024.

[BRW12] Marcello M. Bonsangue, Jan Rutten, and Joost Winter. Defining context-free power series coalgebraically. In Pattinson and Schröder [PS12], pages 20–39.

[Brz64] Janusz A. Brzozowski. Derivatives of regular expressions. *Journal of the ACM*, 11:481–494, 1964.

[BW85] Michael Barr and Charles Wells. *Toposes, triples, and theories*. Grundlehren der mathematischen Wissenschaften. Springer-Verlag, New York, 1985.

[Che07] Eugenia Cheng. Iterated distributive laws. http://arxiv.org/pdf/0710.1120v1.pdf, 2007.

[Eil76] Samuel Eilenberg. *Automata, Languages, and Machines*. Academic Press, Inc., 1976.

[Jac06a] Bart Jacobs. A bialgebraic review of deterministic automata, regular expressions and languages. In *Essays Dedicated to Joseph A. Goguen*, pages 375–404, 2006.

[Jac06b] Bart Jacobs. Distributive laws for the coinductive solution of recursive equations. *Inf. Comput.*, 204(4):561–587, 2006.

[JSS12] Bart Jacobs, Alexandra Silva, and Ana Sokolova. Trace semantics via determinization. In Pattinson and Schröder [PS12], pages 109–129.
[Kli11] Bartek Klin. Bialgebras for structural operational semantics: An introduction. *Theoretical Computer Science*, 412(38):5043–5069, 2011.

[LPW00] Marina Lenisa, John Power, and Hiroshi Watanabe. Distributivity for endofunctors, pointed and co-pointed endofunctors, monads and comonads. *Electr. Notes Theor. Comput. Sci.*, 33:230–260, 2000.

[Mac71] Saunders MacLane. *Categories for the Working Mathematician*. Springer-Verlag, 1971.

[MMS13] Stefan Milius, Lawrence S. Moss, and Daniel Schwencke. Abstract GSOS rules and a modular treatment of recursive definitions. *Logical Methods in Computer Science*, 9(3), 2013.

[MPW16] Stefan Milius, Dirk Pattinson, and Thorsten Wißmann. A new foundation for finitary corecursion. *CoRR*, abs/1601.01532, 2016.

[PS12] Dirk Pattinson and Lutz Schröder, editors. *Coalgebraic Methods in Computer Science - 11th International Workshop, CMCS 2012, Colocated with ETAPS 2012, Tallinn, Estonia, March/April 2012, Revised Selected Papers*, volume 7399 of *Lecture Notes in Computer Science*. Springer, 2012.

[RR08] Markus Rosenkranz and Georg Regensburger. Integro-differential polynomials and operators. In *Proceedings of the Twenty-first International Symposium on Symbolic and Algebraic Computation*, ISSAC '08, pages 261–268, New York, NY, USA, 2008. ACM.

[Rut98] Jan Rutten. Automata and coinduction (an exercise in coalgebra). In Davide Sangiorgi and Robert de Simone, editors, *CONCUR*, volume 1466 of *Lecture Notes in Computer Science*, pages 194–218. Springer, 1998.

[Rut00] Jan Rutten. Universal coalgebra: a theory of systems. *Theoretical Computer Science*, 249(1):3–80, 2000.

[Rut03] Jan Rutten. Behavioural differential equations: a coinductive calculus of streams, automata, and power series. *Theoretical Computer Science*, 308(1-3):1–53, 2003.

[Rut05] Jan Rutten. A coinductive calculus of streams. *Mathematical Structures in Computer Science*, 15(1):93–147, 2005.

[SBBR10] Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan Rutten. Generalizing the powerset construction, coalgebraically. In Kamal Lodaya and Meena Mahajan, editors, *FSTTCS*, volume 8 of *LIPIcs*, pages 272–283. Schloss Dagstuhl—Leibniz-Zentrum für Informatik, 2010.

[SBBR13] Alexandra Silva, Filippo Bonchi, Marcello Bonsangue, and Jan Rutten. Generalizing determinization from automata to coalgebras. *Logical Methods in Computer Science*, 9(1), 2013.

[Sch14] Daniel Schwencke. *Compositional and Effectful Recursive Specification Formats*. PhD thesis, Technische Universität Braunschweig, 2014.

[WBR11] Joost Winter, Marcello M. Bonsangue, and Jan Rutten. Context-free languages, coalgebraically. In Andrea Corradini, Bartek Klin, and Corina Cîrstea, editors, *CALCO*, volume 6859 of *Lecture Notes in Computer Science*, pages 359–376. Springer, 2011.

[WBR13] Joost Winter, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Coalgebraic characterizations of context-free languages. *Logical Methods in Computer Science*, 9 (3:14), 2013.

[Win14] Joost Winter. *Coalgebraic Characterizations of Automata-Theoretic Classes*. PhD thesis, Radboud Universiteit Nijmegen, 2014.

[Wor09] James Worthington. *Automata, Representations, and Proofs*. PhD thesis, Cornell University, 2009.