# Categories of Coalgebras with Monadic Homomorphisms

Wolfram Kahl

► To cite this version:

Wolfram Kahl. Categories of Coalgebras with Monadic Homomorphisms. 12th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2014, Grenoble, France. pp.151-167, 10.1007/978-3-662-44124-4_9. hal-01408758

HAL Id: hal-01408758

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

Submitted on 5 Dec 2016

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
# Categories of Coalgebras with Monadic Homomorphisms

Wolfram Kahl

McMaster University, Hamilton, Ontario, Canada, kahl@cas.mcmaster.ca

**Abstract.** Abstract graph transformation approaches traditionally consider graph structures as algebras over signatures where all function symbols are unary.

Attributed graphs, with attributes taken from (term) algebras over arbitrary signatures do not fit directly into this kind of transformation approach, since algebras containing function symbols taking two or more arguments do not allow component-wise construction of pushouts.

We show how shifting from the algebraic view to a coalgebraic view of graph structures opens up additional flexibility, and enables treating term algebras over arbitrary signatures in essentially the same way as unstructured label sets. We integrate substitution into our coalgebra homomorphisms by identifying a factoring over the term monad, and obtain a flexible framework for graphs with symbolic attributes. This allows us to prove that pushouts can be constructed for homomorphisms with unifiable substitution components.

We formalised the presented development in Agda, which crucially aided the exploration of the complex interaction of the different functors, and enables us to report all theorems as mechanically verified.

# 1 Introduction

In computer science, algebras are used in two different rôles:

- “Algebras providing datatype” are the concern in particular of the field of algebraic specifications [EM85, BKL+91, BM04]: The carrier sets of an algebra are datatypes, and the operations are available as some kind of executable function. Frequently, the carrier sets are so large that one would not consider to keep all their elements simultaneously available in some data structure.

- “Algebras as data” are most obviously the topic of the algebraic approach to graph transformation [CMR+97, EHK+97, EEPT06] which derives its name from the fact that it considers graphs as algebras.

In *attributed graphs*, the two views come together: An attributed graph is first of all a graph, that is an algebra that is considered in its whole as a piece of data, but (some of) its items may be assigned attributes which are elements of some datatypes provided by an attribute algebra, which is normally not considered in its whole as a piece of data. Although an attributed graph can be
considered as a single algebra, implementation considerations alone already dic-
tate a separation into a graph structure part and an attribution part. As far
as attributed graphs are to be transformed via the algebraic approach to graph
transformation, theoretical reasons contribute to this separation: for graph struc-
tures, considered as unary algebras, the pushouts of their homomorphisms can
be calculated component-wise and independent of the presence of operations be-
tween the different sorts, while in the presence of non-unary operations, this is
no longer the case. With more-than-unary operations, even a pushout of finite
algebras can become infinite, so that calculations of these pushouts is in gen-
eral not feasible. There is also typically little motivation to consider non-trivial
pushouts of attribute algebras, since most transformation concepts for attributed
graphs expect the transformation results to be attributed over the same attribute
datatypes. An exception to this consideration are symbolic attributes, which can
easily be drawn from term algebras over different variable sets during different
stages of transformation.

In the context of the algebraic approach to graph transformation, graph struc-
tures have traditionally been presented as unary algebras [Löw90, CMR+97].
However, as such they are the intersection between algebras and coalgebras, and
in this paper we show how more general coalgebras are useful in modelling graph
features, in particular symbolic attribution. Therefore, we define our graph struc-
tures not via algebraic signatures, but via coalgebraic signatures, and integrate
label types and term type constructors for attributes into the coalgebraic result
types.

For example, the following is a signature for directed hypergraphs where each
hyperedge has a sequence of source nodes and a sequence of target nodes, and
each node is labelled with an element of the constant set L :

sigDHG := < sorts: N, E

ops: src : E → List N

trg : E → List N

nlab : N → L

>

While constant sets like *L* are perfectly standard as results in coalgebras, modelling labelled graphs as algebras always has to employ the trick of declaring the label sets as additional sorts, and then consider the subcategory that has algebras with a fixed choice for these label sets, and morphisms that map them only with the identity. Similarly, list-valued source and target functions are frequently considered for algebraic graph transformation, but with ad-hoc definitions for morphisms and custom proofs of their properties.

In contrast, declaring these features via a coalgebra signature such as sigDHG
makes the generic theory of coalgebras available, which immediately produces
the standard homomorphism definition for directed hypergraphs considered as
sigDHG structures, without any necessity for ad-hoc treatment of the label type
or the list structure.
Even more interesting is the use of coalgebras for symbolically attributed
graphs, where morphisms are required to also contain substitutions for attribute
variables; the main contribution of this paper is to formulate the beginnings of
a coalgebraic approach to corresponding categories of symbolically attributed
graphs.

After discussing related work in the next section, we provide some more
detailed motivation for moving to coalgebras. We quickly fix our categorical no-
tation in Sect. 3 and explain basics of (co)algebras in Sect. 4. We show more
complex graphs structures in Sect. 5, and discuss the limitations of using stan-
dard coalgebra homomorphisms. In section Sect. 6 we show how a factoring of the
coalgebra functor over a monad allows us to replace the morphisms underlying
the coalgebra homomorphisms with Kleisli arrows, enabling typical applications
of symbolic attributes where instantiation of variables via substitution is required
and the variable set may be modified by transformations. We show that this gen-
eral factoring accommodates a natural formalisation of term graphs as monadic
coalgebras. Refining this factoring in Sect. 7 for a general class of structures
encompassing in particular common kinds of symbolically attributed graphs, we
show that pushouts in that setting can be constructed from unifications for the
substitution components of the homomorphisms.

The whole theoretical development has been formalised in the dependently
typed programming language and proof checker Agda2 [Nor07] on top of the
basic category formalisations provided by [Kah11, Kah14]. The Agda source
code for this development is available on-line<fnref n="1" />. For not disrupting the flow of
the presentation, we just add a check mark “ ✓ ” to statements for which a
formalised version has been mechanically checked by Agda.

## 2 Related Work

Löwe *et al.* [LKW93] started to consider attributed graphs in the context of the
algebraic approach to graph transformation; they propose working with a tri-
partitioned signature, with a unary graph structure part, an arbitrary attribute
signature, and a set of unary attribution operators connecting the two. Rewriting
uses the single pushout approach. Without discussing the issue in depth, they
propose to add sorts of attribute carriers that are deleted and re-created for
relabelling. König and Kozioura [KK08] follow the approach of [LKW93], but
impose a rigid organisation of unlabelled nodes, and labelled hyperedges with
label-conforming attribution.

In the double-pushout approach, Heckel *et al.* [HKT02] treat data algebra
carriers as graph nodes, with graph edges to them allowed, but data algebra
function symbols are not part of the graph. Their attribution edges from graph
nodes to data nodes are equivalent to the attribute carriers of [LKW93]. The
data part is kept constant during transformation. Rule graphs are attributed
over a term algebra with a fixed set of variables. The E-graphs of [EPT04] allows

<footnote n="1">¹ URL: http://relmics.mcmaster.ca/RATH-Agda/</footnote>
also attribute edges starting from edges. The algebra integration of [HKT02] is
strengthened from a commuting square to a pullback, which is used for showing
the equivalence of categories of typed attributed graphs over type graph ATG
with categories of algebras over a derived signature AGSIG(ATG), where each
type graph item is turned into a sort. For the symbolic graphs of [OL10], the
Σ-algebra is not integrated into the graph structure, but only connected to it via
constraints: A symbolic graph is an E-graph over a sorted variable set together
with a set of formulae that may refer to constants drawn from the Σ-algebra.

While all the approaches presented so far worked with total algebras through-
out, the relabelling DPO graph transformations of Habel and Plump [HP02,
Plu09] use partially labelled interface graphs. Rule side images of unlabelled
interface nodes are unlabelled as well, and natural pushouts (that are also pull-
backs) with injective matching are used for rewriting. In [PS04], rule schemas are
introduced to get around the fixed label sets of [HP02]; these rule schemas are
rules that are labelled over a term algebra. A different approach to relabelling is
that of Rebout [RFS08], which employs a special mechanism for relabelling via
"computations" in the left-hand side of the rule.

For general theory of coalgebra, we refer to Rutten’s overview article [Rut00].
The part of the coalgebra literature that deals with combining algebras and coal-
gebras is probably closest to our current endeavour; one approach considers sep-
arate algebraic and coalgebraic structures in the same carriers, for example Kurz
and Hennicker’s “Institutions for Modular Coalgebraic Specifications” [KH02].
A further generalisation are “dialgebras” [Hag87, PZ01], which have a single car-
rier X, and operations $f_i : F_i X \to G_i X$, where both $F_i$ and $G_i$ are polynomial
functors.

Pardo studies the combination of corecursion with monads [Par98], using as
an essential tool natural transformations for distribution of the monad over the
functor; his “monadic coalgebras” are defined by an operation of type
$A \to \mathcal{M}(\mathcal{F}A)$, which is the opposite functor composition to the one we use
in Sect. 6. Capretta’s survey [Cap11] covers coalgebras in functional program-
ming and type theory; like Pardo, also Capretta concentrates on coinduction
and infinite structures.

## 3 Category Notation

We assume familiarity with the basics of category theory; for notation, we write
“*f*: *A* → *B*” to declare that morphism *f* goes from object *A* to object *B*, and
use “;;” as the associative binary *forward composition* operator that maps two
morphisms *f*: *A* → *B* and *g*: *B* → *C* to (*f* ; *g*) : *A* → *C*. The identity morphism
for object *A* is written **I**<sub>*A*</sub>.

We assign “;” higher priority than other binary operators, and assign unary
operators higher priority than all binary operators.

The category of sets and functions is denoted by *Set*.

A functor $\mathcal{F}$ from one category to another maps objects to objects and morphisms to morphisms respecting the structure generated by $\to$, $\I$, and com-
position; we denote functor application by juxtaposition both for objects, $\mathcal{F} A$, and for morphisms, $\mathcal{F} f$. Although we use forward composition of morphisms, we use backward composition “$_{\circ}$$_{-}$” for functors, with $(\mathcal{G} \circ \mathcal{F}) A = \mathcal{G}(\mathcal{F} A)$, and may even omit parentheses and just write $\mathcal{G}\mathcal{F}A$.

A bifunctor is a functor where the source is a product category. An important example is the coproduct bifunctor $+ : \mathcal{C} \times \mathcal{C} \to \mathcal{C}$ for a category $\mathcal{C}$ with a choice of coproducts. Functors with more than two arguments are handled similarly.

The double-pushout (DPO) approach to high-level rewriting [CMR$^+$97] uses transformation rules that are spans $L \stackrel{l}{\leftarrow} G \stackrel{r}{\rightarrow} R$ in an appropriate category between the left-hand side $L$, gluing object $G$, and right-hand side $R$. A direct transformation step from object $A$ to object $B$ via such a rule is given by a double pushout diagram, where $m$ is called the match:

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

# 4 Algebras and Coalgebras

The category-theoretic definitions of algebras and coalgebras are simple: Given a (unary) functor $\mathcal{F}$,

- an $\mathcal{F}$-algebra $A = (C_A, f_A)$ is an object $C_A$ together with a morphism $f_A : \mathcal{F} C_A \to C_A$

- an $\mathcal{F}$-coalgebra $A = (C_A, f_A)$ is an object $C_A$ together with a morphism $f_A : C_A \to \mathcal{F} C_A$.

The algebraic approach to graph transformation was named for its understanding of graphs as algebras — unlabelled graphs are conventionally presented as algebras over the following signature:

$$ \mathit{sigGraph} := \langle \mathit{sorts}: N, E \\ \mathit{ops}: \mathit{src}: E \to N \\ \mathit{trg}: E \to N \rangle $$

(From now on, we assume the product bifunctor $\times$, the coproduct bifunctor $+$, the terminal object $\mathbb{1}$, and the initial object $\mathbb{0}$ to be given.) The functor giving rise to graphs as algebras is a functor on the product category $\mathit{Set} \times \mathit{Set}$ since there is more than one sort:

$$ \mathcal{F}_{\mathit{sigGraph-alg}}(N, E) = ((E + E), \mathbb{0}), $$
since there is an isomorphism mapping functions $E+E \to N$ to pairs of functions $(E \to N) \times (E \to N)$, and there is only one “empty” function in $\emptyset \to E$.

This functor can be constructed systematically from the signature above, and the signatures for which this systematic procedure works are called “algebraic”:

- An *algebraic signature* has only single sort symbols as *result types*.

Dually, a coalgebra functor can be constructed systematically for the following:

- An *coalgebraic signature* has only single sort symbols as *argument types*.

Obviously, **sigGraph** is also a coalgebraic signature, and the functor giving rise to graphs as coalgebras is the following:

$$ \mathcal{F}_{\text{sigGraph}} (N, E) = (\mathbf{1}, (N \times N)) $$

For algebras, one frequently considers only *polynomial functors*, that is, functors constructed from $+$, $\times$, and $\mathbf{1}$. For coalgebras, more varied functors are the norm, and many more complicated kinds of graphs can easily be characterised via coalgebraic signatures, for example:

- Node-labelled graphs are often presented with signature $\mathbf{sigNLG}_1$ for some node label set $L$ — note that $\mathbf{sigNLG}_1$ is not an algebraic signature, since $L$ is not a sort symbol:

$$ \begin{array}{l@{\qquad}l} \mathbf{sigNLG}_1 := \langle \mathbf{sorts}: N, E & \mathbf{sigNLG}_2 := \langle \mathbf{sorts}: N, E, L \\ \mathbf{ops}: \mathbf{src}: E \to N & \mathbf{ops}: \mathbf{src}: E \to N \\ \mathbf{trg}: E \to N & \mathbf{trg}: E \to N \\ \mathbf{nlab}: N \to L \rangle & \mathbf{nlab}: N \to L \rangle \end{array} $$

Although this is easily fixed, see $\mathbf{sigNLG}_2$ which introduces an additional sort $L$, this comes at the cost of considering the label set a *part of the graph*, while usually one may want to consider it as fixed. The category of $\mathbf{sigNLG}_2$-structures admits morphisms that change labels, and encompasses as subcategories images of the categories of $\mathbf{sigNLG}_1$-structures for different choices of the interpretation of $L$.

However, both $\mathbf{sigNLG}_1$ and $\mathbf{sigNLG}_2$ are coalgebraic signatures, which shows that the coalgebraic view has advantages even when dealing with very simple graph structures. For a fixed node set $L$, coalgebras over the functor for $\mathbf{sigNLG}_1$ form exactly the category of graphs with node labels drawn from $L$, without any complications:

$$ \mathcal{F}_{\mathbf{sigNLG}_1} (N, E) = (L, N \times N) $$

- $\mathbf{sigDHG}$, already mentioned in the introduction, is a signature for directed hypergraphs where each hyperedge has a sequence of source nodes and a sequence of target nodes, and each node is labelled with an element of the constant set $L$:

$$ \mathbf{sigDHG} := \langle \mathbf{sorts}: N, E \\ \mathbf{ops}: \mathbf{src}: E \to \text{List } N \\ \mathbf{trg}: E \to \text{List } N \\ \mathbf{nlab}: N \to L \rangle $$
Writing List for the list functor<fnref n="2" />, the functor corresponding to sigDHG is again a functor between product categories because of the two sorts:

$$F_{\text{sigDHG}}(N, E) = (L, ((\text{List } N) \times (\text{List } N)))$$

In general, we assume a language of functor symbols (with arity), and a signature introduces first, after “sorts:”, a list of sort symbols, and then, after “ops:”, a list of function symbols (or operation symbols), and for each operation symbol, an argument type expression and a result type expression (separated by “→”) each built from the functor symbols and the sort symbols.

In sigDHG, we used the unary functor symbol List and the zero-ary functor symbol L — we will not make any notational distinction between functor symbols and their interpretation as functors.

# 5 Limitations of Standard Coalgebra Homomorphisms

For a different situation consider edge-attributed graphs, with symbolic attributes taken from the term algebra $T_Σ V$ over some term signature $Σ$ and with variables from the variable carrier set for sort V:

$$\begin{array}{l} \text{sigAG}_{\Sigma} := \langle \text{sorts: } N, E, V \\ \quad \text{ops: } \text{src: } E \to N \\ \quad \text{trg: } E \to N \\ \quad \text{attr: } E \to T_{\Sigma} V \rangle \end{array}$$

The resulting homomorphism concept only allows renaming of variables:

**Fact 5.1** A sigAG<sub>Σ</sub>-coalgebra homomorphism $F : G_1 \to G_2$ consists of three mappings $F_N : N_1 \to N_2$ and $F_E : E_1 \to E_2$ and $F_V : V_1 \to V_2$ satisfying the following conditions:

$$\begin{array}{l} F_E : \text{src}_2 = \text{src}_1 ; F_N \\ F_E : \text{trg}_2 = \text{trg}_1 ; F_N \\ F_E : \text{attr}_2 = \text{attr}_1 ; T_\Sigma F_V \end{array} \qquad \square$$

DPO rewriting in this category therefore has to rely on deletion and re-creation of attribute carrying edges to implement relabelling, like the approaches of [LKW93, KK08]. In addition we also lack the ability to instantiate rules via variable substitution as part of the morphism concept, and might therefore be tempted to add such instantiation outside the DPO rewriting framework, as in [PS04].

<footnote n="2">² Note that List A can be defined as the initial algebra of the functor $L_A Y = 1+A \times Y$.</footnote>
Another example where the coalgebra category is unsatisfactory are term graphs, where each node is either a variable (of sort V), or an inner node (of sort N) that has a label (from set L) and a list of successors, which can be either variables or other nodes:

$$ \begin{array}{l} \texttt{sigTG} := \langle \texttt{sorts: V, N} \\ \texttt{ops: lab : N \to L} \\ \texttt{suc : N \to List (N + V)} \rangle \end{array} $$

The resulting standard homomorphism concept also has $F_V : V_1 \to V_2$ and therefore does not allow mapping of variables to inner nodes:

**Fact 5.2** A sigTG-coalgebra homomorphism $F : G_1 \to G_2$ consists of two mappings $F_N : N_1 \to N_2$ and $F_V : V_1 \to V_2$ satisfying the following conditions:

$$ \begin{array}{l} F_N : \texttt{lab}_2 = \texttt{lab}_1 \\ F_N : \texttt{suc}_2 = \texttt{suc}_1 : \texttt{List}(F_N + F_V) \end{array} \qquad \square $$

In the resulting category, pushout complements exist only in very special cases, and the resulting DPO rewriting concept does not correspond to any useful term graph rewriting concept.

# 6 Monadic Coalgebra Morphisms

We now introduce a more powerful morphism concept to remedy these shortcomings. We first show how the homomorphism concepts for sigAG<sub>Σ</sub>-coalgebras and for sigTG-coalgebras can be “fixed” to allow substitution, and then extract the general pattern behind this class of “fixes”.

## 6.1 Substituting Attributed Graph Homomorphisms

If we want to allow substitutions in morphisms between sigAG<sub>Σ</sub>-coalgebras, we also have to adapt the morphism conditions to take the substituted variables inside the image terms of the attribution function into account:

**Definition 6.1** We define the category AG<sub>Σ</sub> to have sigAG<sub>Σ</sub>-coalgebras as objects, and a morphism $F : G_1 \to G_2$ consists of three mappings typed as shown to the left, satisfying the conditions shown to the right:

$$ \begin{array}{l} F_N : N_1 \to N_2 \qquad F_E : \texttt{src}_2 = \texttt{src}_1 ; F_N \\ F_E : E_1 \to E_2 \qquad F_E : \texttt{trg}_2 = \texttt{trg}_1 ; F_N \\ F_V : V_1 \to \mathcal{T}_\Sigma V_2 \qquad F_E : \texttt{attr}_2 = \texttt{attr}_1 ; \mathcal{T}_\Sigma F_V ; \mu_{\mathcal{T}_\Sigma} \end{array} $$

where $\mu_{\mathcal{T}_\Sigma} : \forall X . \mathcal{T}_\Sigma(\mathcal{T}_\Sigma X) \to \mathcal{T}_\Sigma X$ is the canonical “term flattening” function that turns two-level nested terms into one-level terms. $\square$
It is not hard to verify that this category is well-defined— the key to the proof is to recognise that the $F_V$ components are substitutions and compose via Kleisli composition of the term monad.

The category $\mathbf{AG}_\Sigma$ of course does not have all pushouts, since pushout construction for the $F_V$ components involves term unification, which is not always defined.

## 6.2 “Substituting” Term Graph Homomorphisms

For term graphs, we just want to allow variables to be mapped also to inner nodes, and therefore adapt the type of $F_V$ accordingly. The resulting adaptation in the commutativity condition for $suc$ affects only the argument of the List functor:

**Definition 6.2** We define the category TG to have sigTG-coalgebras as objects, and a morphism $F: G_1 \to G_2$ consists of two mappings

$$ 
\begin{aligned}
F_N: N_1 &\to N_2 \\
F_V: V_1 &\to N_2 + V_2
\end{aligned}
 $$

satisfying the following conditions:

$$ 
\begin{aligned}
F_N: \mathit{lab}_2 &= \mathit{lab}_1 \\
F_N: \mathit{suc}_2 &= \mathit{suc}_1; \mathit{List}((F_N + F_V); \mu_{(N_2+)}
\end{aligned}
 $$

where $\mu_{(N+)}: \forall X. (N + (N + X)) \to (N + X)$ is the canonical flattening function for nested alternatives with $N$. $\square$

This time, we are dealing with a parameterised monad, namely $(N+)$, which maps any $X$ to $N+X$, where the parameter $N$ is instantiated with the respective carrier of that sort. Composition of the $V$ components of $F: T_1 \to T_2$ and $G: T_2 \to T_3$ is defined accordingly:

$$ (F; G)_V = F_V; (G_N + G_V); \mu_{(N_3+)} $$

Again, the resulting category is well-defined.✓

## 6.3 Generalised Coalgebra Morphisms

For obtaining the general shape of such “monadic coalgebra morphisms”, inspection of the signatures shows that each of the functors underlying these kinds of coalgebras not only contains a primitive monad (the term monad for attributed graphs, and an “alternative monad” for term graphs), but even can be factored over a monad on the relevant product category.

Since the signature $\mathbf{sigAG}_\Sigma$ has three sorts, the underlying category is the triple product $\mathit{Set} \times \mathit{Set} \times \mathit{Set}$, with triples of sets as objects.

The coalgebra functor for $\mathbf{sigAG}_\Sigma$ is then
$$ \mathcal{G}_{\text{sigAG}_{\Sigma}} (N, E, V) = (1, (N \times N \times \mathcal{T}_{\Sigma} V), 1), $$

mapping node and edge set to the terminal object $1$ since no operations take nodes or edges as arguments; since there are three operations taking edges as arguments, $\mathcal{G}_{\text{sigAG}_{\Sigma}}$ produces as “edge component” of its result type the Cartesian product $N \times N \times \mathcal{T}_{\Sigma} V$ consisting of the target sets of the three operations.

We can decompose this as $\mathcal{G}_{\text{sigAG}_{\Sigma}} = \mathcal{F}_{\text{sigAG}_{\Sigma}} \circ \mathcal{M}_{\text{sigAG}_{\Sigma}}$, where:

$$ \mathcal{M}_{\text{sigAG}_{\Sigma}} (N, E, V) = (N, E, \mathcal{T}_{\Sigma} V) $$

$$ \mathcal{F}_{\text{sigAG}_{\Sigma}} (N, E, T) = (1, (N \times N \times T), 1) $$

Since $\mathcal{M}_{\text{sigAG}_{\Sigma}}$ is the product of twice the identity monad with the term monad $\mathcal{T}_{\Sigma}$, it is obviously a monad.✓

Analogously, the coalgebra functor for sigTG is

$$ \mathcal{G}_{\text{sigTG}} (N, V) = (L \times \text{List}(N+V), 1), $$

mapping the variable set to the terminal object $1$ since no operations take variables as arguments. We can decompose this as $\mathcal{G}_{\text{sigTG}} = \mathcal{F}_{\text{sigTG}} \circ \mathcal{M}_{\text{sigTG}}$, where:

$$ \mathcal{M}_{\text{sigTG}} (N, V) = (N, (N + V)) $$

$$ \mathcal{F}_{\text{sigTG}} (N, S) = (L \times \text{List} S, 1) $$

It is straightforward to prove that $\mathcal{M}_{\text{sigTG}}$ is a monad constructed as a “dependent product monad”.✓

In general, we define:

**Definition 6.3** Given a monad $\mathcal{M}$ and an endofunctor $\mathcal{F}$ over a category $\mathcal{C}$, an $\mathcal{M}\text{-}\mathcal{F}$-coalgebra is a coalgebra over the functor $\mathcal{F} \circ \mathcal{M}$, that is, a pair $(A, \text{op}_A)$ consisting of

- an object $A$ of $\mathcal{C}$, and

- a morphism $\text{op}_A : A \to \mathcal{F}(\mathcal{M}A)$

A raw $\mathcal{M}\text{-}\mathcal{F}$-coalgebra homomorphism from $(A, \text{op}_A)$ to $(B, \text{op}_B)$ is a morphism from $A$ to $B$ in the Kleisli category of $\mathcal{M}$; raw morphism composition is Kleisli composition. $\square$

One might expect that we obtain just coalgebras over the Kleisli category of $\mathcal{M}$. However, the following complications hold:

- $\mathcal{F}$ does in general not give rise to a functor over the Kleisli category of $\mathcal{M}$.

- If a natural transformation from $\mathcal{F} \circ \mathcal{M}$ to $\mathcal{M} \circ \mathcal{F}$ exists, an endofunctor on the Kleisli category that coincides with $\mathcal{F}$ on objects can be constructed — however, no such a natural transformation exists for $\text{sigAG}_{\Sigma}$.✓

- Constructing an endofunctor on $\mathcal{C}$ from an endofunctor on the Kleisli category would require transformations to “extract from the monad $\mathcal{M}$” which can be natural neither on $\mathcal{C}$ nor on the Kleisli category.✓
In addition, not all raw $M_{\text{sigAG}_\Sigma}$-$\mathcal{F}_{\text{sigAG}_\Sigma}$-coalgebra homomorphisms satisfy the conditions we listed above for monadic $\text{sigAG}_\Sigma$ coalgebra homomorphisms — we need to identify an appropriate subcategory of the Kleisli category.

From the material we have, we can easily construct the following two mor-
phisms:

$$
f; \mathcal{M} \circ \mathcal{O}_B : A \to \mathcal{M} \mathcal{F} \mathcal{M} B
$$

$$
\mathrm{op}_A; \mathcal{F} \mathcal{M} f : A \to \mathcal{F} \mathcal{M} \mathcal{M} B
$$

"Obviously", we can complete this to a commutativity condition using a natural transformation constructed from the return $\eta$ and the join $\mu$ transformations of the monad $\mathcal{M}$, namely:

$$
\mathcal{F}\mu;\eta : \mathcal{F} \circ \mathcal{M} \circ \mathcal{M} \Rightarrow \mathcal{M} \circ \mathcal{F} \circ \mathcal{M}
$$

For the category $\mathbf{AG}_\Sigma$ of Def. 6.1, this condition is unfortunately only satisfied by morphisms where $F_V$ only renames variables✓, which defeats our intentions. This problem is actually not even due to the choice of $F\mu;\eta$, but to the choice of direction, since it arises for every natural transformation from $F \circ \mathcal{M} \circ \mathcal{M}$ to $\mathcal{M} \circ F \circ \mathcal{M}$. Therefore, using distribution transformations from $F \circ \mathcal{M}$ to $\mathcal{M} \circ F$ as used by Pardo [Par98] is not an option either.

We found that natural transformations from $\mathcal{M} \circ \mathcal{F} \circ \mathcal{M}$ to $\mathcal{F} \circ \mathcal{M}$ “work” when combined with a join on the other side:

**Definition 6.4** For an endofunctor $\mathcal{F}$ and a monad $(\mathcal{M}, \eta, \mu)$ on $\mathcal{C}$, an $\mathcal{M}\text{-}\mathcal{F}\text{-}$
$distrjoin$ transformation is a natural transformation $\xi : \mathcal{M} \circ \mathcal{F} \circ \mathcal{M} \Rightarrow \mathcal{F} \circ \mathcal{M}$
for which the following properties hold:

$$
- \eta; \xi = \mathbb{I}
$$

$$
- \mu ; \xi = \mathcal{M} \xi ; \xi
$$

$$
- \mathcal{M} \mathcal{F} \mu ; \xi = \xi ; \mathcal{F} \mu
$$

□

**Definition 6.5** Given an endofunctor $\mathcal{F}$ and a monad $(\mathcal{M}, \eta, \mu)$ on $\mathcal{C}$, and also an $\mathcal{M}\text{-}\mathcal{F}\text{-distrjoin}$ transformation $\xi$, an $\mathcal{M}\text{-}\mathcal{F}\text{-coalgebra homomorphism}$ from $(A, \text{op}_A)$ to $(B, \text{op}_B)$ is a morphism $f : A \to MB$ making the following diagram commute:

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

**Theorem 6.6** $\mathcal{M}\text{-}\mathcal{F}$-coalgebras with such $\mathcal{M}\text{-}\mathcal{F}$-coalgebra homomorphisms form a category. ✓
□

The instantiations of this for edge-attributed graphs (sigAG<sub>Σ</sub>) and for term
graphs (sigTG) are appropriate:
**Theorem 6.7** The $M_{\mathcal{sig}AG_{\Sigma}}$-$\mathcal{F}_{\mathcal{sig}AG_{\Sigma}}$-coalgebra category is equivalent to the category $AG_{\Sigma}$ of Def. 6.1.✓ □

**Theorem 6.8** The $M_{\mathcal{sigTG}}$-$\mathcal{F}_{\mathcal{sigTG}}$-coalgebra category is equivalent to the category TG of Def. 6.2.✓ □

## 6.4 Pushouts of Monadic Coalgebra Morphisms

It is well-known that the Kleisli category over the term monad $\mathcal{T}$ does not have all pushouts, and that existence of pushouts essentially corresponds to unifiability.

Therefore we cannot expect the category of monadic $\mathcal{sigAG}_{\Sigma}$ coalgebras to have all pushouts. Nevertheless, since pushouts are the key ingredient of the categoric approach to graph transformation, an interesting question is whether pushouts in the Kleisli category of $M$ give rise to pushouts in the $M$-$\mathcal{F}$-coalgebra category. It is easy to see that this is not the case for term graphs; however, it does hold for symbolically edge-attributed graphs, and in this section we explore the question how to prove this from the point of view of $M$-$\mathcal{F}$-coalgebra categories without considering decompositions of $M$ and $\mathcal{F}$.

A pushout for a span $B \underset{A}{\overset{F}{\rightleftharpoons}} C$ is a completion $B \underset{D}{\overset{H}{\rightleftharpoons}} C$ to a commuting square that is “minimal” in the sense that every other candidate completion factors uniquely over it (via $U$).

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

Assuming such a pushout in the Kleisli category of $M$, for constructing the operation $op_D$ of the target coalgebra we need to choose appropriate $H'$ and $K'$ such that the $U$ can be used to construct $op_D$ and prove its pushout property in the category of $M$-$\mathcal{F}$-coalgebras.

Without assuming additional (natural) transformations, we can only choose the following:

$$H' = op_B ; \mathcal{F}(MH ; \mu) ; \eta$$

$$K' = op_C ; \mathcal{F}(MK ; \mu) ; \eta$$

However, commutativity $F_\zeta H' = G_\zeta K'$ in the Kleisli category can only be shown assuming additional (natural) transformations and/or laws, which however are
not available for the setting of $\mathbf{sigAG}_\Sigma$ — there, this commutativity does not hold. ✓ The essential reason for this is that $\mathcal{F}$ maps $V$ to $1$, while $V$ is also the only component that has a non-trivial monad. Commutativity fails for the $V$ components due to the fact that $\mathbf{op}_B$ and $\mathbf{op}_C$ map these to $1$, while $\mathcal{M}$ for the $V$ components is the term monad $T_\Sigma$:

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

Due to this property of the operators in $\mathbf{sigAG}_\Sigma$, commutativity will actually fail for any definition of $H'$ of the shape "$H' = \mathbf{op}_B; \dots$". We solve this problem in the next section by restriction to more specialised versions of $\mathcal{M}$ and $\mathcal{F}$, which allows us to "patch" $H'$ and $K'$ so as to avoid this conflict.

# 7 Monadic Product Coalgebras

We now specialise the $\mathcal{M}-\mathcal{F}$-coalgebras of Sect. 6.3 in a way that still generalises the setup for symbolically edge-attributed graphs there, while also allowing a pushout construction.

The most general shape we have been able to identify for this are “monadic product coalgebras” over a product category $C_1 \times C_2$, defined in the following setting (which we will assume for the remainder of this section): Let $C_1$ and $C_2$ be two categories; let $\mathcal{M}$ be a monad on $C_2$, and $\mathcal{F}$ a functor from $C_1 \times C_2$ to $C_1$.

In terms of coalgebraic signatures this implements the restriction that sorts mentioned as monad arguments do not occur as source sorts of operators, and that the monad must not depend on sorts that do occur as source sorts of operators. This restriction is satisfied by all simple kinds of symbolically attributed graphs where the monad is typically a term monad, is applied only to sets of free variables, and these variables do not otherwise participate in the graph structure.

**Definition 7.1** An $\mathcal{M}-\mathcal{F}$-product-coalgebra $A$ is a triple $(A_1, A_2, \mathbf{op}_A)$ consisting of

- an object $A_1$ of $C_1$, and

- an object $A_2$ of $C_2$, and

- a morphism $\mathbf{op}_A : A_1 \to \mathcal{F}(A_1, \mathcal{M} A_2)$
A $\mathcal{M}-\mathcal{F}$-product-coalgebra homomorphism $f$ from $(A_1, A_2, \mathcal{op}_A)$ to $(B_1, B_2, \mathcal{op}_B)$ is a pair $(f_1, f_2)$ consisting of a $C_1$-morphism $f_1$ from $A_1$ to $B_1$ and a morphism $f_2$ from $A_2$ to $B_2$ in the Kleisli category of $\mathcal{M}$ such that

$$f_1; \mathcal{op}_B = \mathcal{op}_A; \mathcal{F} (f_1, \mathcal{M} f_2; \mu).$$

Morphism composition is composition of the corresponding product category. $\square$

This morphism composition is well-defined✓, and induces a category ✓.

Now let $\mathcal{M}_0$ be the product monad of the identity monad on $C_1$ and $\mathcal{M}$, and define $\mathcal{F}_0$ as endofunctor on $C_1 \times C_2$ by:

$$\mathcal{F}_0(X_1, X_2) = (\mathcal{F}(X_1, X_2), 1)$$

With these definitions, the $\mathcal{M}_0$-$\mathcal{F}_0$-distrjoin transformation (see Def. 6.4) has identities of $C_1$ and terminal morphisms of $C_2$ as its two components✓, which allows us to identify monadic product coalgebras as a special case of the monadic coalgebras of Sect. 6.3:

**Theorem 7.2** The category of $\mathcal{M}-\mathcal{F}$-product-coalgebra homomorphisms is equivalent to the category of $\mathcal{M}_0$-$\mathcal{F}_0$-coalgebra homomorphisms. ✓ $\square$

In addition, the more fine-grained structure of monadic product coalgebras allows us to circumvent the problems we encountered in Sect. 6.4.

Let $\mathbb{K}$ be the Kleisli category of $\mathcal{M}_0$. Since $\mathcal{M}_0$ is a product monad, pushouts in $\mathbb{K}$ are calculated component-wise, that is, they consist of a pushout in $C_1$ and a pushout in the Kleisli category of $\mathcal{M}$.

**Theorem 7.3** Let a span $B \xrightarrow{F} A \xrightarrow{G} C$ of $\mathcal{M}-\mathcal{F}$-product-coalgebra homomorphisms be given, and a cospan $(B_1, B_2) \xrightarrow{H} (D_1, D_2) \xleftarrow{K} (C_1, C_2)$ in $\mathbb{K}$ that is a pushout for the Kleisli morphisms underlying $F$ and $G$. Then $(D_1, D_2)$ can be extended to a $\mathcal{M}-\mathcal{F}$-product-coalgebra $D = (D_1, D_2, \mathcal{op}_D)$ such that $B \xrightarrow{H} D \xleftarrow{K} C$ is a pushout for $B \xrightarrow{F} A \xrightarrow{G} C$ in the $\mathcal{M}-\mathcal{F}$-product-coalgebra category. ✓

**Proof sketch:** The first step is the construction of a cospan

$$(B_1, B_2) \xrightarrow{H'} D' \xleftarrow{K'} (C_1, C_2)$$

in $\mathbb{K}$ such that the first component of the universal morphism $U : (D_1, D_2) \to D'$ from the $\mathbb{K}$ pushout can be used as $\mathcal{op}_D$.

The first constituent of $D'$ therefore must be the target of $\mathcal{op}_D$, so we define:

$$D' = ( \mathcal{F}(D_1, \mathcal{M} D_2) , D_2 )$$

$$H' = ( \mathcal{op}_B ; \mathcal{F}(H_1, \mathcal{M} H_2 ; \mu) , H_2 )$$

$$K' = ( \mathcal{op}_C ; \mathcal{F}(K_1, \mathcal{M} K_2 ; \mu) , K_2 )$$
The second constituent of $D'$ is inherited from ($D_1, D_2$), which allows us to
use the universality of the original $\mathbb{K}$ pushout when proving universality of the
resulting $M\text{-}\mathcal{F}$-product-coalgebra pushout. $\square$

Together with the two equivalences of categories of Theorems 7.2 and 6.7, pushouts for edge-attributed graphs essentially reduce to unification for their variable components (if we choose an underlying category that has pushouts, such as *Set*):

**Corollary 7.4** A span $B \stackrel{F}{\dashrightarrow} A \stackrel{G}{\dashrightarrow} C$ in the $M_{\text{sigAG}}\text{-}\mathcal{F}_{\text{sigAG}}$-coalgebra category over *Set* for edge-attributed graphs (as $\text{sigAG}_\Sigma$ structures) has a pushout if $F_V$ and $G_V$, as substitutions, have a pushout. ✓ $\square$

# 8 Conclusion and Outlook

We have shown how the additional flexibility of coalgebraic signatures enables us
to integrate label types and symbolic attribute types into graph structure signa-
tures, and then modified the coalgebraic homomorphism concept via integration
of Kleisli arrows to achieve the flexibility necessary to allow substitutions as part
of our morphisms. We showed that several seemingly plausible formalisations for
this do not model the intended applications, and arrived at a simple factoring
setup (Sect. 6.3) that additionally encompasses a natural formalisation of term
graphs. For symbolically attributed graphs fitting into the pattern of monadic
product coalgebras (Sect. 7), we showed that pushouts can be obtained where
the substitution components of their homomorphisms are unifiable.

Without the support of our mechanised formalisation in Agda, the mentioned
failures of inappropriate formalisations, and also the successful proofs reported
in the paper would have been extremely hard to arrive at with comparable
confidence.

Since pushouts do not necessarily exist in Kleisli categories, an important
question is whether general results for appropriate classes of restricted monomor-
phisms can be obtained. In this context, the “protected monads” of Ghani et al.
[GLDM05] might be useful, since a protected monad essentially can be represented
as $\mathrm{Id} + \mathcal{N}$ for some functor $\mathcal{N}$, and the identity component can be used to lift
monomorphisms from the base category into the Kleisli category.

The ultimate goal of this work is a fully verified implementation of monadic
coalgebra transformation that can be instantiated in particular for the transfor-
mation of symbolically attributed graph structures.

*Acknowledgements*. I am grateful to the anonymous referees for their construc-
tive comments.

References

[BKL<sup>+</sup>91] Bidoit, M., Kreowski, H.-J., Lescanne, P., Orejas, F., Sanella, D. (eds.) Algebraic System Specification and Development — A Survey and Annotated Bibliography, LNCS, vol. 501. Springer (1991)
[BM04] Bidoit, M., Mosses, P. D.: CASL User Manual, LNCS (IFIP Series), vol. 2900. Springer (2004). With chapters by T. Mossakowski, D. Sannella, and A. Tarlecki

[Cap11] Capretta, V.: Coalgebras in functional programming and type theory. Theoretical Computer Science 412, 5006–5024 (2011)

[CMR$^{+}$97] Corradini, A., Montanari, U., Rossi, F., Ehrig, H., Heckel, R., Löwe, M.: Algebraic Approaches to Graph Transformation, Part I: Basic Concepts and Double Pushout Approach. In [Roz97], Chapt. 3, pp. 163–245

[CEKR02] Corradini, A., Ehrig, H., Kreowski, H., Rozenberg, G. (eds.) ICGT 2002, LNCS, vol. 2505 (2002)

[EM85] Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification 1: Equations and Initial Semantics. Springer (1985)

[EHK$^{+}$97] Ehrig, H., Heckel, R., Korff, M., Löwe, M., Ribeiro, L., Wagner, A., Corradini, A.: Algebraic Approaches to Graph Transformation, Part II: Single Pushout Approach and Comparison with Double Pushout Approach. In [Roz97], Chapt. 4, pp. 247–312

[EPT04] Ehrig, H., Prange, U., Taentzer, G.: Fundamental Theory for Typed Attributed Graph Transformation. In [PPBE04], pp. 161–177

[EEPT06] Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Springer (2006)

[GLDM05] Ghani, N., Lüth, C., De Marchi, F.: Monads of Coalgebras: Rational Terms and Term Graphs. Mathematical Structures in Computer Science 15, 433–451 (2005)

[HP02] Habel, A., Plump, D.: Relabelling in Graph Transformation. In [CEKR02], pp. 135–147

[Hag87] Hagino, T.: A Categorical Programming Language. PhD thesis, Edinburgh University (1987)

[HKT02] Heckel, R., Küster, J. M., Taentzer, G.: Confluence of Typed Attributed Graph Transformation Systems. In [CEKR02], pp. 161–176

[Kah11] Kahl, W.: Dependently-Typed Formalisation of Relation-Algebraic Abstractions. In de Swart, H. (ed.) RAMiCS 2011, LNCS, vol. 6663, pp. 230–247. Springer (2011)

[Kah14] Kahl, W.: Relation-Algebraic Theories in Agda — RATH-Agda-2.0.1. Mechanically checked Agda theories available for download, with 456 pages literate document output. http://RelMiCS.McMaster.ca/RATH-Agda/. (2014)

[KK08] König, B., Kozioura, V.: Towards the Verification of Attributed Graph Transformation Systems. In Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT 2008, LNCS, vol. 5214, pp. 305–320 (2008)

[KH02] Kurz, A., Hennicker, R.: On Institutions for Modular Coalgebraic Specifications. Theoretical Computer Science 280, 69–103 (2002)

[Löw90] Löwe, M.: Algebraic Approach to Graph Transformation Based on Single Pushout Derivations. Technical Report 90/05, TU Berlin (1990)

[LKW93] Löwe, M., Korff, M., Wagner, A.: An Algebraic Framework for the Transformation of Attributed Graphs. In Sleep, M., Plasmeijer, M., van Eekelen, M. (eds.) Term Graph Rewriting: Theory and Practice, pp. 185–199. Wiley (1993)

[Nor07] Norell, U.: Towards a Practical Programming Language Based on Dependent Type Theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology (2007)
[OL10] Orejas, F., Lambers, L.: Delaying Constraint Solving in Symbolic Graph Transformation. In Ehrig, H., Rensink, A., Rozenberg, G., Schürr, A. (eds.) ICGT 2010, LNCS, vol. 6372, pp. 43–58 (2010)

[Par98] Pardo, A.: Monadic Corecursion — Definition, Fusion Laws and Applications. ENTCS 11, (1998)

[PPBE04] Parisi-Presicce, F., Bottoni, P., Engels, G. (eds.) ICGT 2004, LNCS, vol. 3256 (2004)

[PS04] Plump, D., Steinert, S.: Towards Graph Programs for Graph Algorithms. In [PPBE04], pp. 128–143

[Plu09] Plump, D.: The Graph Programming Language GP. In: CAI 2009, LNCS, vol. 5725, pp. 99–122 (2009)

[PZ01] Poll, E., Zwanenburg, J.: From Algebras and Coalgebras to Dialgebras. ENTCS 44, 289–307 (2001)

[RFS08] Rebout, M., Féraud, L., Soloviev, S.: A Unified Categorical Approach for Attributed Graph Rewriting In Hirsch, E., Razborov, A., Semenov, A., Slissenko, A. (eds.) CSR 2008, LNCS, vol. 5010, pp. 398–409. Springer (2008)

[Roz97] Rozenberg, G. (ed.) Handbook of Graph Grammars and Computing by Graph Transformation, Vol. 1: Foundations. World Scientific, Singapore (1997)

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