Work performed as part of the DFG-funded project
COAX (MI 717/5-1 and SCHR 1118/12-1)

T. Wißmann]Thorsten Wißmann
U. Dorsch]Ulrich Dorsch
S. Milius]Stefan Milius
L. Schröder]Lutz Schröder
Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

We present a generic partition refinement algorithm that quotients
coalgebraic systems by behavioural equivalence, an important task in
system analysis and verification.  Coalgebraic generality allows us
to cover not only classical relational systems but also, e.g.  various forms of weighted systems and furthermore to flexibly
combine existing system types. Under assumptions on the type functor
that allow representing its finite coalgebras in terms of nodes and
edges, our algorithm runs in time $\mathcal{O}(m\cdot \log n)$ where
$n$ and $m$ are the numbers of nodes and edges, respectively. The
generic complexity result and the possibility of combining system
types yields a toolbox for efficient partition refinement
algorithms. Instances of our generic algorithm match the
run-time of the best known algorithms for unlabelled transition
systems, Markov chains, deterministic automata (with fixed
alphabets), Segala systems, and for color refinement.

§ INTRODUCTION

The minimization of a state based system typically consists of two steps:

* Removal of unreachable states.

* Identification of states exhibiting the same behaviour, w.r.t. a
suitable notion of `sameness'; here we are interested in
minimization under bisimilarity.
The computation of reachable states is usually
accomplished by a straightforward search through the transition graph
of a system. Minimization under
bisimilarity however is more complex because of its corecursive
nature: whether two states are bisimilar depends on which of their
successors are bisimilar. In the present work, we present a generic
algorithm to perform bisimilarity minimization efficiently for a broad
class of systems.

The task of minimization appears as a subtask in state space reduction
(e.g. [12]) or non-interference
checking [55]. The notion of bisimulation was first
defined for relational systems [54, 43, 46]; it
was later extended to other system types including probabilistic
systems [42, 18], weighted
automata [14], and (weighted) tree
automata [30, 29]. More generally,
universal coalgebra (see e.g. Rutten [49]) provides
a framework capturing all these types of systems uniformly, and their
notions of bisimulation appear as special instances of Aczel and
Mendler's notion of bisimulation for
coalgebras [4].

The importance of minimization under bisimilarity appears to increase with
the complexity of the underlying system type. E.g. while in LTL model
checking, minimization drastically reduces the state space but,
depending on the application, does not necessarily lead to a speedup
in the overall balance [23], in probabilistic model
checking, minimization under strong bisimilarity does lead to
substantial efficiency gains [37]. This is the reason why
model checkers implement bisimilarity minimization, e.g. the mCRL2
toolset [11] provides explicit routines for comparing and
minimizing systems w.r.t. strong bisimilarity and also other types of

The algorithmics of minimization, often referred to as partition
refinement or lumping, has received a fair amount of
attention. Since bisimilarity is a greatest fixpoint, it is more or
less immediate that it can be calculated in polynomial time by
approximating this fixpoint from above following Kleene's fixpoint
theorem. For transition systems, Kanellakis and
Smolka [40, 41] introduced an algorithm that in fact runs
in time $\mathcal{O}(nm)$ where $n$ is the number of nodes and $m$ is
the number of transitions. An even more efficient algorithm running in
time $\mathcal{O}(m\log n)$ was later described by Paige and
Tarjan [47]; this bound holds even if the number of
action labels is not fixed [53]. Current algorithms
typically apply further optimizations to the Paige-Tarjan algorithm,
achieving better average-case behaviour but the same worst-case
behaviour [22]. Probabilistic minimization has undergone
a similarly dynamic
development [10, 17, 59, 27], and the
best algorithms for minimization of Markov chains now have the same
$\CO(m\log n)$ run-time as the relational Paige-Tarjan
algorithm [32, 19, 56].  Using ideas
from abstract interpretation, Ranzato and Tapparo [48]
have developed a relational partition refinement algorithm that is
generic over notions of process equivalence. As instances, they
recover the classical Paige-Tarjan algorithm for strong bisimilarity
and an algorithm for stuttering equivalence, and obtain new algorithms
for simulation equivalence and for a new process equivalence; the
generic run-time analysis, however, is coarser for this algorithm, and
in particular does not recover the $\CO(m\log n)$ bound for the
classical Paige-Tarjan algorithm. Recently, Groote et
al. [24] have presented an improved algorithm for
relational partition refinement that covers stuttering, branching and
strong bisimilarity.

In this paper we follow an orthogonal approach and provide a generic
partition refinement algorithm that can be instantiated for many
different types of systems (e.g. nondeterministic,
probabilistic, weighted). The key to genericity is to use the methods of
universal coalgebra. That is, we encapsulate
transition types of systems as endofunctors on sets (or a more general
category), and model systems as coalgebras for a given type

§.§ Overview of the paper

In <ref>, the categorical generalizations of the standard set
operations on partitions and equivalence relations are introduced. A short
introduction to coalgebras as a framework for state-based systems is given.

In order to explain the generic pattern that existing partition
refinement algorithms in the literature follow, we exhibit in
<ref> an informal partition refinement algorithm in
natural language that operates on a high level of generality.

In <ref>, the generic pattern is made precise by a
categorical construction, in which we work with coalgebras for a
monomorphism-preserving endofunctor on a category with image
factorizations. Here we present a quite general category-theoretic
partition refinement algorithm, and we prove its correctness. The
algorithm is parametrized over a select routine that determines
which observations are used to split blocks of states. We present two
select routines; one yields a known coalgebraic final-chain
algorithm (e.g. [1, 36]),
the other routine is select the smaller half, a trick that
goes back to Hopcroft [31] and lies at the heart of most
modern partition refinement algorithms including Paige and
Tarjan's [47], being responsible for the logarithmic
(rather than linear) dependence of the run-time on the number of

While the categorical construction recomputes the involved partitions from
scratch in each iteration, we present an optimized version of our algorithm
(<ref>) that computes the partitions incrementally. For the
correctness of the optimization, we need to restrict to sets and assume that the
type endofunctor satisfies a condition we call zippability. This property
holds, e.g. for all polynomial endofunctors on sets and for the type functors
of labelled and weighted transition systems, but is not closed under composition
of functors.

In order to be able to provide a concrete presentation of our
algorithm and perform a complexity analysis we make the algorithm
parametric in an abstract refinement interface of the type
functor, which encapsulates simple functor specific computations
needed to implement the select the smaller half
routine. In <ref> we introduce
refinement interfaces, and we provide several examples for various zippable
type functors of interest and show that they can be implemented with a
linear run-time.

Then in <ref> we provide pseudocode for the
algorithm using the incremental computation of the partitions from
<ref> and with the select the smaller half
routine hard-wired. We show that if the
refinement interface operations can be implemented to run in linear time, then the
algorithm runs in time $\CO((m+n) \cdot \log n)$, where $n$ is the number of
states and $m$ the number of `edges' in a syntactic encoding of the input
coalgebra. We thus recover the complexity of the most efficient known algorithms
for transition systems (Paige and Tarjan [47]), for weighted
systems (Valmari and Franceschinis [56]), for the task of color
refinement (Berkholz, Bonsma, and Grohe [9]), as well as
Hopcroft's classical automata minimization algorithm [31] for a
fixed alphabet $A$ and $m= n\cdot |A|$.

<ref> is devoted to modularity and explains how to
handle combinations of system types, in particular functor
composition. We will see that this can be achieved with just a bit of
extra preprocessing, so that our main algorithm need not be adjusted
at all. In fact, given a functor $T$ built as a term from finitary
functors $\Set^k\to \Set$, we first recall from
[51] how this induces a functor
$\bar T\colon \Set^n\to\Set^n$ on multisorted sets, and we present a
transformation from finite $T$-coalgebras to finite
$\bar T$-coalgebras (with possibly more states) that reflects
bisimilarity minimization. We then present a new construction that
provides for every functor on the category $\C^n$, where $\C$ is any
extensive category (e.g. ), a functor on $\C$ and a transformation
from coalgebras of the former to coalgebras of the latter that
preserves the size of carriers (i.e. the number of states) and
preserves and reflects bisimilarity minimization. This yields a
reduction from bisimilarity minimization of $T$-coalgebras to
minimization of $\coprodfunctor \bar T\Delta$-coalgebras, where
$\Delta\colon \Set \to \Set^n$ is the diagonal functor and
$\coprodfunctor\colon \Set^n \to \Set$ takes coproducts. The latter
problem is solved by the algorithm from <ref>,
because we prove that if $T$ is built from functors fulfilling our
assumptions, then $\coprodfunctor \bar T \Delta$ fulfils the
assumptions too – even if $T$ itself does not.

As instances of this result, we obtain an efficient modular
algorithm for systems whose type is built from basic system types
fulfilling our assumptions, e.g. probability, non-determinism,
weighted branching (with weights in an arbitrary abelian group), by
composition, finite products and finite coproducts

One of these instances is an $\CO((m+n) \log (m+n))$ algorithm for
Segala systems, to our knowledge a new result (more precisely, we
improve an earlier bound established by Baier, Engelen, and
Majster-Cederbaum [10], roughly speaking by letting only
non-zero probabilistic edges enter into the time bound). Note that Groote et
al.'s recent algorithm [27] for Segala systems, which was
discovered independently and almost at the same time, has a similar
complexity as ours.

We also obtain efficient minimization algorithms for general Segala
systems and alternating systems [28]. In
further work [21] we extend our algorithm to cover weighted
branching (with weights in an arbitrary monoids) and tree automata,
for which we obtain an algorithm improving the previous best
complexity for minimization w.r.t. backwards bisimulation. In addition
op. cit. presents a generic implementation in the form of the
partition refinement tool .

This paper is an extended and completely reworked version of a
previous conference paper [20]. Besides providing detailed
proofs of all our results, we have included the new
<ref> showing that modularity is achieved without
any adjustment of our algorithm.

Acknowledgement. We would like to thank the anonymous
referees for their comments, which helped to improve the presentation
of our paper.

§ PRELIMINARIES

It is advisable for readers to be familiar with basic category
theory [3].  However, our results can be understood by
reading the notation in the usual set-theoretic way, which corresponds
to their meaning in $\Set$, the category of sets and functions. For the
convenience of the reader we recall some concepts that are central for
the categorical version of our algorithm.

§.§ Equivalence Relations and Partitions, Categorically

Our most general setting is a category $\C$ in which we have a well-behaved
notion of equivalence relation corresponding to quotient
objects. We will assume that $\C$ has finite products and

The terminal object of $\C$
is denoted by $1$, with unique morphisms $!\colon A\to 1$. In ,
$1 = \{0\}$ as usual. We denote the product of objects $A$, $B$ by
$A \xleftarrow{\out_1} A×B \xrightarrow{\out_2} B$. Given
$f\colon D\to A$ and $g\colon D\to B$, the morphism induced by the
universal property of the product $A \times B$ is denoted by
$\fpair{f,g}\colon D\to A\times B$.

For morphisms $f\colon A\to D$, $g\colon B\to D$, we denote by

\[
\begin{mytikzcd}
P \arrow{r}{\pi_1}
\arrow{d}[swap]{\pi_2}
\pullbackangle{-45}
& A
\arrow{d}{f}
\\
\arrow{r}{g}
& D
\end{mytikzcd}
\]

that $P$ (together with the projections $\pi_1, \pi_2$) is the pullback of $f$
along $g$. In , we have

\[
P = \{ (a,b) \in A\times B \mid f(a) = g(b) \}.
\]

The kernel $\ker f$ of a morphism $f\colon A\to B$ is
the pullback of $f$ along itself.

We write $\rightarrowtail$ for monomorphisms (in $\Set$, the
monomorphisms are the  injections), and $\epito$ for regular
epimorphisms; by definition, $q\colon A\to B$ is a regular epimorphism
($q\colon A \epito B$) if there exists a parallel pair of morphisms
$f,g\colon R\rightrightarrows A$ such that $q$ is the coequalizer of
$f$ and $g$. In , the coequalizer of
$f,g\colon R\rightrightarrows A$ is the quotient of $A$ modulo the
smallest equivalence relation on $A$ relating $f(r)$ and $g(r)$ for
all $r\in R$. Here, one can think of $R$ as a set of witnesses $r$ of
the pairs $(f(r), g(r))$ generating that equivalence (note that there
may be several witnesses for the same pair). Hence, we will often
denote the coequalizer of $f,g\colon R\rightrightarrows A$ by
$\kappa_R\colon A\twoheadrightarrow A/R$, and such a map represents a
quotient. When $f$ and $g$ are clear from the context, we will
just write $R\rightrightarrows A$.

Kernels and coequalizers allow us to talk about equivalence relations
and partitions in a category, and when we speak of an
equivalence relation on the object $X$ of $\C$ we mean the
kernel of some morphism with domain $X$. Indeed, recall that for
every set $A$, every equivalence relation $\sim$ is the kernel of the
canonical quotient map $\kappa_\sim\colon A \epito A/\mathord{\sim}$, and there is a
bijection between equivalence relations and partitions on
$A$. In order to obtain a similar bijection for more general
categories than $\Set$ we make the following global assumption.

We assume throughout that $\C$ is a finitely complete category that
has coequalizers and in which regular epimorphisms are closed under composition.

Examples of categories satisfying <ref> abound. In
particular, every regular category with coequalizers
satisfies our assumptions. The category $\Set$ of sets and functions is
regular. Every topos is regular, and so is every
finitary variety, i.e. a category of algebras for a finitary
signature satisfying given equational axioms (e.g. monoids, groups,
vector spaces etc.). If $\C$ is regular, so is the functor category
$\C^\E$ for any category $\E$. For our main applications, we will be
interested in the special case $\C^n$ where $n$ is a natural number,
i.e. the case where $\E$ is the discrete category with the set of
objects $\{1,\ldots, n\}$.

The category of posets and the category of topological spaces both
fail to be regular but still satisfy our assumptions.

In , a function $f\colon A\to B$ factorizes through the
partition $\unnicefrac{A}{\ker f}$ induced by its kernel, via the
function $[-]_f\colon A\twoheadrightarrow \unnicefrac{A}{\ker f}$ taking
equivalence classes

\begin{equation}
[x]_f := \{ x'\in A\mid f(x) = f(x')\} = \{ x' \in D\mid (x,x') \in \ker f\}.
\label{eq:funEquivClass}
\end{equation}

Well-definedness of functions on $\unnicefrac{A}{\ker f}$ is determined
precisely by the universal property of $[-]_f$ as a coequalizer of $\ker
f\rightrightarrows A$. In particular, $f$ induces an injection
$\unnicefrac{A}{\ker f}\rightarrowtail B$; together with $[-]_f$, this is the
factorization of $f$ into a regular epimorphism and a monomorphism.

More generally, our category $\C$ from <ref> has a
(RegEpi,Mono)-factorization system <cit.>, that
is, every morphism $f\colon A\to B$ has a factorization

\[
\begin{mytikzcd}
\arrow[shiftarr={yshift=6mm}]{rr}{f}
\arrow[->>]{r}{e}
& \Im(f)
\arrow[>->]{r}{m}
& B,
\end{mytikzcd}
\]

where $m$ is a monomorphism and $e$ is a regular epimorphism,
specifically the coequalizer of the kernel
$\pi_1,\pi_2\colon \ker f\rightrightarrows A$. The subobject
$m\colon \Im(f) \monoto B$ is called the image and the
factorization $f = m \cdot e$ the image factorization of
$f$. In every category, we have the diagonal fill-in property
for monomorphisms $m$ and regular epimorphisms $e$: Whenever
$f\cdot e=m\cdot g$ then there exists a unique diagonal $d$ such that
$d\cdot e=g$ and $m\cdot d=f$, implying that
(RegEpi,Mono)-factorizations are unique.

Using image factorizations it is easy to show that in our category $\C$, there is a
bijection between kernels $K\rightrightarrows A$ and quotients of $A$
– the two directions of this bijection are given by taking the kernel
of a coequalizer and by taking the coequalizer of a kernel.
In particular, every regular epimorphism is the
coequalizer of its kernel.

Furthermore, the above bijection is in fact an order isomorphism
between the natural partial orderings on kernels and quotients,
respectively. In detail, relations from $A$ to $B$ in $\C$,
i.e. jointly monic spans $A \leftarrow R \to B$, and in particular
kernels, represent subobjects of $A\times B$, which are ordered by
inclusion in the usual way: We say that a relation
$\fpair{p_1,p_2}\colon R \monoto A \times B$ (or a kernel) is
finer than a relation
$\fpair{p_1',p_2'}\colon R' \monoto A\times B$ if there exists
$m\colon R \monoto R'$ (necessarily unique and monic) such that
$p_i' \cdot m = p_i$, for $i = 1,2$.  We write $\cap$
(intersection) and $\cup$ (union) for meets and joins of
kernels in the inclusion ordering on relations (not equivalence
relations or kernels) on $A$. In this notation,

\begin{equation}\label{eq:kercap}
\ker \fpair{f,g} =\ker f\cap\ker g;
\end{equation}

in particular, kernels are stable under intersection of relations.

Similarly, a quotient represented by
$q_1\colon A\twoheadrightarrow B_1$ is finer than a quotient
represented by $q_2\colon A\twoheadrightarrow B_2$ if there exists
$b\colon B_1\epito B_2$ (necessarily unique and regular epic) with
$q_2=b\cdot q_1$.

We need a few simple observations on kernels that are familiar when
instantiated to $\Set$:

*  For every $f\colon X \to Y$ and $g\colon Y \to Z$,
$\ker(f)$ is finer than $\ker(g\cdot f)$.

*  For every $f\colon X \to Y$ and every mono $m\colon Y
\monoto Z$, $\ker(m\cdot f) = \ker f$.

*  For every $f\colon X \to Y$ and regular epi $q\colon X
\epito Z$, $\ker(f) = \ker (q)$ iff there exists a mono $m\colon
Z \monoto Y$ with $f = m\cdot q$. One implication follows from the
previous point, and conversely, take the image factorization $f =
n \cdot e$. Then $\ker(e) = \ker(f)$ by point <ref>, and
therefore $e$ and $q$ represent the same quotient, which means
there exists some isomorphism $i\colon Z \to \Im(f)$ with $i \cdot q =
e$. It follows that $m = n \cdot i$ is the desired mono.

*  For every $f\colon X \to Z$ and regular epi $e\colon X \epito Y$,
$\ker(e)$ is finer than $\ker(f)$ iff
there exists some morphism $g\colon Y \to Z$ such that $g \cdot e = f$.

To see this let $p,q\colon \ker(e) \rightrightarrows X$ be the kernel
pair of $e$. If $\ker(e)$ is finer than
$\ker(f)$, then we have $f\cdot p = f\cdot q$. Hence, since $e$
is the coequalizer of its kernel pair we obtain $g$ as desired
from the universal property of $e$. For the other direction apply <ref>.

Whenever $\ker (a\colon D\to A) = \ker (b\colon D\to B)$ then
$\ker (a\cdot g) = \ker (b\cdot g)$, for every $g\colon W\to D$.

Indeed, the kernel $\ker(a \cdot g)$ can be obtained from $\ker a$
by pasting pullback squares as shown below (and similarly for $b\colon
D \to B$):

\[
\begin{mytikzcd}
\ker\big( a \cdot g\big)
\arrow{r}
\arrow{d}
\pullbackangle{-45}
& \bullet
\pullbackangle{-45}
\arrow{r}
\arrow{d}
& W
\arrow{d}{g}
\\
\bullet
\arrow{d}
\arrow{r}
\pullbackangle{-45}
& \ker a
\arrow{d}
\arrow{r}
\pullbackangle{-45}
& D
\arrow{d}{a}
\\
\arrow{r}{g}
& D
\arrow{r}{a}
& A
\end{mytikzcd}
\]

So if $\ker a = \ker b$, then $\ker(a\cdot g) = \ker(b\cdot g)$.

Even though only existence of coequalizers is assumed, $\C$
has more colimits:

$\C$ has pushouts of regular epimorphisms (i.e. pushouts of spans containing
at least one regular epimorphism).sollten wir die nicht lieber
pushouts along reg epis nennen? Inverse images sind ja auch pullbacks
along monos und nicht pullbacks of monos

Let $X\xleftarrow{e}Y\xrightarrow{h}W$ be a span, with $e$ a
regular epi. Let $(\pi_1,\pi_2)$ be the kernel pair of $e$, and
let $q\colon W\epito Z$ be the coequalizer of $h\cdot \pi_1$ and $h\cdot \pi_2$.

Since $e$ is the
coequalizer of $\pi_1,\pi_2$ there exists $r\colon X\to Z$ such
that $r\cdot e=q\cdot h$. We claim that the square in

\begin{equation*}
\begin{mytikzcd}
\ker e
\arrow[shift left=1]{r}{\pi_1}
\arrow[shift right=1]{r}[swap]{\pi_2}
& Y \arrow[->>]{r}[above]{e} \arrow{d}[left]{h} &
X\arrow{d}[right]{r} \\
& W\arrow[->>]{r}[below]{q} & Z
\end{mytikzcd}
\end{equation*}

is a pushout. Uniqueness of mediating morphisms is clear since $q$
is epic; it remains to show existence. So let
$W\xrightarrow{g} U \xleftarrow{f} X$ be such that
$g\cdot h = f\cdot e$. Then
$g\cdot h\cdot \pi_1=f\cdot e\cdot\pi_1=f\cdot e\cdot \pi_2=g\cdot
so by the universal property of $q$ we obtain $k\colon Z\to U$ such
that $k\cdot q=g$. It remains to check that $k\cdot r=f$. Indeed, we
have $k\cdot r\cdot e=k\cdot q\cdot h=g\cdot h=f\cdot e$, which
implies the claim because $e$ is epic.

§.§ Coalgebra

We now briefly recall basic notions from universal coalgebra, seen as
a unified framework for state-based reactive systems. For introductory
texts, see [49, 35, 2, 34].  Given an
endofunctor $H\colon \C \to \C$, a coalgebra is a pair
where $X$ is an object of $\C$ called the carrier and thought
of as an object of states, and $\xi\colon X \to HX$ is a morphism
called the structure of the coalgebra. Our leading examples are
the following.

* Labelled transition systems with labels from a set $A$ are
coalgebras for the functor $HX = \Pot(A \times X)$ (and unlabelled
transition systems are simply coalgebras for $\Pot$) on $\Set$. Explicitly,
a coalgebra $\xi\colon X\to HX$ assigns to each state $x$ a set
$\xi(x)\in\Pot(A\times X)$, and this represents the transition
structure at $x$: $x$ has an $a$-transition to $y$ iff
$(a,y)\in \xi(x)$.
In concrete examples, we restrict to the finite powerset functor $\Potf X =
\{S\in \Pot X \mid S\text{ finite}\}$, and coalgebras for $HX =
\Potf(A\times X)$ are finitely branching LTSs.

*  Weighted transition systems with weights from a
commutative monoid $(M,+,0)$ are modelled as coalgebras as
follows. We consider the monoid-valued functor $M^{(-)}$
defined on sets $X$ by

\[
M^{(X)} = \{ f\colon X \to M \mid f(x) \neq 0\text{ for only finitely many
\]

and on maps $h\colon X \to Y$ by

\[
M^{(h)}(f)(y) = \textstyle\sum_{h(x) = y} f(x).
\]

$M$-weighted transition systems are in bijective correspondence
with coalgebras for $M^{(-)}$, and for $M$-weighted
labelled transition systems one takes $(M^{(-)})^A$, where $A$ is
the label alphabet (see [26]).

*  The finite powerset functor $\Potf$ is the
monoid-valued functor $\B^{(-)}$ for the Boolean monoid
$\B = (2, \vee, 0)$.  The bag functor $\Bagf$, which
assigns to a set $X$ the set of bags (i.e. finite multisets)
on $X$, is the monoid-valued functor for the additive monoid of
natural numbers $(\N, + , 0)$.

* Probabilistic transition systems are modelled coalgebraically
using the distribution functor $\Dist$. This is the subfunctor
$\Dist X\subseteq \R_{\ge 0}^{(X)}$, where $\R_{\ge 0}$ is the
monoid of addition on the non-negative reals, given by
$\Dist X=\{f\in\R_{\ge 0}^{(X)}\mid \sum_{x \in X} f(x) = 1\}$.

*  Simple (resp. general) Segala
systems [50] strictly alternate between
non-deterministic and probabilistic transitions.

Simple Segala systems can
be modelled as coalgebras for the set functor $\Potf(A×\Dist(-))$,
which means that for every label $a \in A$, a state
non-deterministically proceeds to one of a finite number of
possible probability distributions over states. General Segala
systems are coalgebras for $\Potf\Dist(A \times -)$, which means
that a state $s$ non-deterministically proceeds to one of a finite
number of distributions over the set of $A$-labelled transitions
from $s$.

*  Let $\Sigma$ be a signature (a.k.a ranked alphabet), i.e. a
set of (operation) symbols, each with a prescibed natural number, its
arity. The corresponding polynomial
functor $H_\Sigma\colon \Set \to \Set$ maps a set $X$ to the set

\[
H_\Sigma X = \coprod_{n \in \N} \Sigma_n \times X^n,
\]

where $\Sigma_n$ is the set of symbols of arity $n$, and
$H_\Sigma$ acts similarly on maps. Note that the elements of $H_\Sigma X$
may be identified with shallow terms over $X$, i.e. formal
expressions $\sigma(x_1, \ldots, x_n)$, where $\sigma \in \Sigma$ is an
$n$-ary symbol and $x_1, \ldots, x_n \in X$.

A coalgebra $\xi\colon X \to H_\Sigma X$ is a deterministic system,
where the coalgebra structure assigns to each state $x \in X$ a
tuple $\xi(x) = (\sigma, x_1, \ldots, x_n)$ in which $\sigma \in
\Sigma$ is an $n$-ary output symbol and $x_1, \ldots, x_n$
are successor states, one for every input in $\{1, \ldots, n\}$.
Coalgebras for $H_\Sigma$ can also be thought of as top-down
deterministic tree automata.

* For a fixed finite set $A$, the coalgebras of the functor
$HX=2\times X^A$ are deterministic automata for the input alphabet
$A$ (neglecting the initial state). Concretely, a coalgebra
structure $\fpair{o,\delta}\colon X\to 2\times X^A$ consists of
the characteristic function $o\colon X \to 2$ of the set of final
states of the automaton and the next state function $\delta$. Note
that the functor $H$ is (naturally isomorphic to) a polynomial
functor, where the signature $\Sigma$ consists of two $A$-ary
operation symbols.

A coalgebra morphism from a coalgebra $(X,\xi)$ to a coalgebra
$(Y,\zeta)$ is a morphism $h\colon X \to Y$ such that
$\zeta \cdot h = Hh \cdot \xi$; intuitively, coalgebra morphisms preserve
observable behaviour.  Coalgebras and their morphisms form a
category $\Coalg(H)$. The forgetful functor $\Coalg(H)\to \C$
creates all colimits, so $\Coalg(H)$ has all colimits that $\C$ has;
in particular, our running assumptions imply the following:

Y rζ

$\Coalg(H)$ has all coequalizers and pushouts of regular

A subcoalgebra of a coalgebra $(X,\xi)$ is represented
by a coalgebra morphism $m\colon (Y,\zeta) \monoto (X,\xi)$ such that $m$ is
a monomorphism in $\C$. Likewise, a quotient of a coalgebra
$(X,\xi)$ is represented by a coalgebra morphism
$q\colon (X,\xi) \epito (Y,\zeta)$ carried by a regular epimorphism $q$ of
$\C$. If $H$ preserves monomorphisms, then the image factorization
structure on $\C$ lifts to coalgebras in the sense that every
coalgebra morphism $f$ has a factorization $f = m \cdot e$ into
coalgebra morphisms $m$ and $e$ such that $m$ is a monomorphism and
$e$ a regular epimorphism in $\C$ (see e.g. <cit.>).

Recall that a coalgebra is called simple if it
does not have any non-trivial quotients [33]. We will use the following
equivalent characterization:

If $H$ preserves monomorphisms,
then a coalgebra $(X,\xi)$ is simple iff every coalgebra
morphism with domain $(X,\xi)$ is carried by a monomorphism.

For necessity, consider a coalgebra morphism
$h\colon (X,\xi) \to (Y,\zeta)$ and take its image factorization to obtain
$q\colon (X,\xi) \twoheadrightarrow (\Im(h),i)$ and
$m\colon (\Im(h),i) \monoto (Y,\zeta)$ in $\Coalg(H)$. Since $(X,\xi)$ is
simple, $q$ is an isomorphism, and so $h = m\cdot q$ is a
monomorphism. For sufficiency, consider $q\colon (X,\xi)\epito(Y,\zeta)$
with $q$ a regular epimorphism in $\C$. By assumption, $q$ is also
monic, whence an isomorphism.

Intuitively, in a simple coalgebra all states exhibiting the
same observable behaviour are already identified. This paper is
concerned with the design of algorithms for computing the
simple quotient of a given coalgebra:

A simple quotient of a coalgebra is unique (up to
isomorphism). Concretely, let $(X,\xi)$ be a coalgebra, and let
$e_i\colon (X,\xi)\epito(Y_i,\zeta_i)$, $i=1,2$, be quotients with
$(D_i,d_i)$ simple. Then $(D_1,d_1)$ and $(D_2,d_2)$ are isomorphic;
more precisely, $e_1$ and $e_2$ represent the same quotient.

By <ref>, there is a pushout
$Y_1\xrightarrow{f_1}Z\xleftarrow{f_2}Y_2$ of
$Y_1\xleftarrow{e_1}X\xrightarrow{e_2}Y_2$ in $\Coalg(H)$. Since
regular epimorphisms are generally stable under pushouts,

$f_1$ and $f_2$ are regular
epimorphisms, hence isomorphisms because $Y_1$ and $Y_2$ are simple;
this proves the claim.

Existence of the simple quotient can be shown under additional
assumptions on $\C$ (cf. <ref> below):

Assume that $\C$ is cocomplete and cowellpowered. Then every
coalgebra $(X,\xi)$ has a simple quotient given by the cointersection
(i.e. the wide pushout) of all quotient coalgebras

\[
q\colon (X,\xi) \epito (X', \xi').
\]

For $\C = \Set$, two elements $x\in X$ and $y\in Y$ of
coalgebras $(X,\xi)$ and $(Y, \zeta)$ are behaviourally
equivalent if they can be merged by coalgebra
morphisms, that is, if there exist a coalgebra $(Z,\omega)$ and
coalgebra morphisms $f\colon (X,\xi)\to (Z,\omega)$,
$g\colon (Y,\zeta) \to (Z,\omega)$ such that $f(x)=g(y)$.
Intuitively, the simple quotient of a coalgebra in is its quotient modulo
behavioural equivalence. In our main examples, this means that we minimize
w.r.t. standard bisimilarity-type equivalences:

Behavioural equivalence instantiates to various notions of

* Park-Milner bisimilarity on labelled transition systems [4];

* weighted bisimilarity on weighted transition systems <cit.>;

* stochastic bisimilarity on probabilistic transition systems [38];

* Segala bisimilarity on simple and general Segala systems <cit.>.

A final coalgebra is a terminal object in the category of
coalgebras, i.e. a coalgebra $(T,\tau)$ such that every coalgebra
$(X,\xi)$ has a unique coalgebra morphism into $(T,\tau)$.  There
are reasonable conditions under which a final coalgebra is
guaranteed to exist, e.g. when $\C$ is a locally presentable
category (in particular, when $\C=\Set$) and $H$ is
accessible [5]. If $H$ preserves monomorphisms and has a final
coalgebra $(T,\tau)$, then the simple quotient of a coalgebra
$(X,\xi)$ is the image of $(X,\xi)$ under the unique morphism into
$(T,\tau)$; in particular, in this case every coalgebra has a simple

Finally, we note a useful result that implies that computing the
simple quotient of a coalgebra for $H$ can be reduced to computing the simple
quotient of its induced coalgebra for a superfunctor of $H$:
This is a beautiful and general reduction result,
that I'd put up front and not hide in some technical development
on many-sorted sets! Besides it is needed for the correctness of
automata minimization with $\Potf$ in Section 8.

Suppose that $m\colon H \monoto G$ is a natural transformation with
monomorphic components. Then every $H$-coalgebra $\xi\colon X \to HX$
and its induced $G$-coalgebra

\[
X \xrightarrow{\xi} HX \xrightarrow{m_X} GX
\]

have the same quotients and, hence, the same simple ones (if they exists).

We prove only the first claim. Let $q\colon X\epito Y$ be a regular
epimorphism. It suffices to show that $q$ carries an $H$-coalgebra
morphism with domain $(X,\xi)$ iff it carries a
$G$-coalgebra morphism with domain
$(X,m_X \cdot \xi)$. Note that $m\colon H \monoto G$ induces an
embedding $\Coalg(H)\to\Coalg(G)$. Hence, `only
if' is clear, and we prove `if'. Suppose that $q$ is a coalgebra
morphism $(X, m_X\cdot \xi) \to (Y,\zeta)$. Then the outside of
the following diagram commutes:

\[
\begin{mytikzcd}
\arrow{r}{\xi}
\arrow[->>]{d}[swap]{q}
& HX
\arrow{r}{m_X}
\arrow{d}[swap]{Hq}
& GX
\arrow{d}{G q}
\\
\arrow[dashed]{r}[near end]{\exists! \zeta'}
\arrow{rr}[swap]{\zeta}
& |[yshift=5mm]| HY
\arrow[>->]{r}{m_Y}
& GY
\end{mytikzcd}
\]

By the naturality of $m$ the right-hand part commutes. Hence, since
$m_Y$ is monic we obtain $\zeta'$ as in the diagram by the diagonal
fill-in property (Section <ref>), making $q$ an
$H$-coalgebra morphism $(X,\xi)\epito(Y,\zeta')$.

§ PARTITION REFINEMENT FROM AN ABSTRACT POINT OF VIEW

In the next section we will provide an abstract partition refinement
algorithm and formally prove its correctness.  Our main contribution
is genericity: we are able to state and prove our results at a
level of abstraction that uniformly captures various kinds of state
based systems. This allows us to instantiate our efficient generic
algorithm to many different (combinations of) transition structures.
Before describing the abstract algorithm (<ref>) formally,
we now give an informal description of a partition refinement
algorithm, which will make it clear which parts of partition
refinement algorithms are generic and which parts are specific to a
particular transition type. Although <ref> works in
categorical generality, we use set-theoretic parlance in the present
informal discussion.

Given a system with a set $X$ of states, one of the core ideas of the
known partition refinement algorithms mentioned so far, in particular
the algorithms by Hopcroft [31] and
Paige-Tarjan [47], is to maintain two equivalence
relations $P$ and $Q$ on $X$, represented by the corresponding
partitions $X/P$ and $X/Q$, where $X/P$ will be one transition
step ahead of $X/Q$, so the relation $P$ is a refinement of
$Q$. Therefore, the elements of $X/P$ are called subblocks and
the elements of $X/Q$ are called compound blocks.

Initially, we put $X/Q = \{X\}$ and let $X/P$ be the initial partition
with respect to the output behaviour of the states in
$X$. For example, in the case of deterministic automata, the output
behaviour of a state is its finality, i.e. the initial partition
separates final from non-final states; in the case of
transition systems, the initial partition separates deadlock states
from states with successors; and for weighted systems, the initial
partition groups the states by the sum of weights of outgoing edges.

Initial Partitions
After the first iteration
After the second iteration

false(x0) (x1) (x2) (x3) (x4)(x0) (x1) (x2),(x3) (x4)
false(x0) (x1) (x2),(x3) (x4)(x0) (x1),(x2),(x3) (x4)
false(x0) (x1),(x2),(x3) (x4)(x0) (x1),(x2),(x3) (x4)

true(x0) (x1) (x2) (x3) (x4)(x0) (x1),(x2) (x3) (x4)
true(x0) (x1),(x2) (x3) (x4)(x0),(x1),(x2) (x3) (x4)
true(x0),(x1),(x2) (x3) (x4)(x0),(x1),(x2) (x3) (x4)

Example of the partition refinement in (a)
transition systems ($H=\Potf$) and  (b) $\R$-weighted systems ($H=\R^{(-)}$). The partition
$X/Q_i$ is indicated by dashed lines, and $X/P_i$ by solid lines.

[Informal Partition Refinement]
Given a system on $X$ and initial partitions $X/Q=\{X\}$ and $X/P$
as above, iterate the following while $P$ is different from $Q$:

a subblock $S$ in $X/P$ that
is properly contained in a compound block $C \in X/Q$, i.e. $S\subsetneqq C$.

Note that this choice represents a quotient $q\colon X\epito \{S, C\setminus
S, X\setminus C\}$.

*  Refine $X/Q$ with respect to this
quotient by splitting $C$ into two blocks $S$ and $C\setminus S$;
that is, replace $X/Q$ with the intersection (greatest common
refinement) of the partitions $X/Q$ and
$\{S,C\setminus S, X\setminus C\}$ according to the terminology
introduced in <ref>.

*  Update $X/P$ to the coarsest refinement
of $X/P$ in which any two states are distinguished if the
transition structure distinguishes them up to $Q$, equivalently:
If two states are identified, then the transition structure
identifies them up to $Q$.

* Since $X/Q$ is refined using only information from $X/P$ in
each iteration, the algorithm maintains the invariant that the
partition $X/P$ is finer than $X/Q$.

* The informal property of the refinement
of $X/P$ in step (3) is referred to as stability of $P$
w.r.t. $Q$. The formal definition of this notion takes into account
the transition type of the given system. In fact,  Paige and
Tarjan [47] have defined stability for transition
systems, and we generalize their definition to the level of
coalgebras in <ref>.

Note that Steps (1) and (2) are independent of the given
transition type, as they perform only basic operations on
quotients. In contrast, the initialization procedure and Step (3)
depend on the transition type of the specific system, encoded by the
type functor.

<ref> illustrates
runs of partition refinement algorithms and how the transition type
specific steps are handled for two different types of systems: in
Paige and Tarjan's algorithm for transition
systems [47] and in Valmari and Franceschinis'
Markov chain lumping algorithm, which in fact works for
$\R$-weighted systems [56]:

* In transition systems, the initial partition only
distinguishes between deadlocks and live states; in our example
$X/P_0 = \{\{x_0,x_1,x_2\},\{x_3,x_4\}\}$, and $X/Q_0 = \{X\}$
identifies all states.

* In the first iteration of the loop of <ref>, there are
two choices for $S$ in Step <ref>, $\{x_0,x_1,x_2\}$ and
$\{x_3,x_4\}$, both leading to the same refinement step: In
Step <ref> the only block of $X/Q_0$ is split into two
blocks, and so $X/Q_1 = X/P_0$. In Step <ref>, $X/P_1$ is
the coarsest refinement of $X/P_0$ that is stable w.r.t. $X/Q_1$. In
transition systems, $X/P$ is stable w.r.t. $X/Q$ if for all elements in
the same block $x,x'\in B\in X/P$ and any other block $B'\in X/Q$, $x$ has
an edge to $B'$ iff $x'$ has an edge to $B'$ [47]. In
detail, the state $x_2$ becomes a separate block because $x_2$ has a
transition to $\{x_3,x_4\}\in X/Q_1$ whereas $x_0$ and $x_1$ do not. The
states $x_0$ and $x_1$ remain in the same block in $X/P_1$, because both
have a transition to $\{x_0,x_1,x_2\}\in X/Q_1$, and have no transition to
$\{x_3,x_4\} \in X/Q_1$. So $X/P_1 = \{\{x_0,x_1\},\{x_2\},\{x_3,x_4\}\}$.

* In the second iteration, we have symmetric choices
$\{x_0,x_1\}$ and $\{x_2\}$ for $S$, and both split the compound
block $\{x_0,x_1,x_2\}$ so that $X/Q_2 = X/P_1$. The partition
$X/Q_2$ is stable w.r.t. itself because both $x_0$ and $x_1$
have transitions to $\{x_0,x_1\}$ and $\{x_2\}$, and because
$x_3$ and $x_4$ both are deadlock states (for the singleton
block $\{x_2\}$ there is nothing to check). Hence,
$X/P_2 = X/Q_2$ and the algorithm terminates.

* In weighted systems, the initial partition groups the states
by the sum of the weights of their outgoing
transitions.[For actual Markov chains or probabilistic
transition systems, where weights sum up to $1$, the initial
partition would thus be trivial, causing immediate termination;
this corresponds to the fact that all states of a Markov chain
are behaviourally equivalent unless we introduce additional
observable features such as propositional atoms or deadlock. In
standard treatments of Markov chain lumping, such additional
features are abstracted in the choice of a non-trivial initial
partition.] For $x_0$ and $x_1$, the sum is 2, and for $x_2$,
$x_3$, $x_4$ the sum is 0. Hence
$X/P_0 =\{\{x_0,x_1\},\{x_2,x_3,x_4\}\}$, and as always,
$X/Q_0 = \{X\}$ identifies all states.

* In the first iteration of <ref>, we can choose
$\{x_0,x_1\}$ or $\{x_2,x_3,x_4\}$ for $S$, both leading to $X/Q_1 =
X/P_0$. In weighted systems, stability of $X/P$ w.r.t. $X/Q$ means that
all elements of the same block $x,x'\in B\in X/P$ have the same
accumulated transition weight to any other block $B'\in X/Q$, for $f\colon
X\to \R^{(X)}$ this means $\sum_{y\in B'} f(x)(y) = \sum_{y\in
B'}f(x')(y)$ (called `compatibility' in [56]). When
refining $X/P_1$ to be as coarse as possible and stable w.r.t. $X/Q_1$, we
have the following accumulated sums. The transition from $x_2$ to
$\{x_2,x_3,x_4\} \in X/Q_1$ has weight $0$, just like the (non-existent)
transition from $x_3$ (resp. $x_4$) to $\{x_2,x_3,x_4\} \in X/Q_1$, and
hence $x_2, x_3, x_4$ are identified in $X/P_1$. The transition from $x_0$
to $\{x_2,x_3,x_4\}\in X/Q_1$ has weight $\frac{3}{2}$, but the transition
from $x_1$ to $\{x_2,x_3,x_4\}$ has weight $1$. Thus, $x_0$ and $x_1$ are
split in $X/P_1$, and therefore we have $X/P_1 =
\{\{x_0\},\{x_1\},\{x_2,x_3,x_4\}\}$.

* In the second iteration, we can choose $S$ to be $\{x_0\}$ or
$\{x_1\}$. In either case, $X/Q_2 = X/P_1$, and we have that $X/Q_2$ is
stable w.r.t. $X/Q_2$ because the transition from $x_2$ to
$\{x_2,x_3,x_4\}$ in $X/Q_2$ has weight 0. Thus, $X/P_2 = X/Q_2$ and the
algorithm terminates.

In the remainder of the paper we shall see that one can
unify the similarities between <ref>(a) and
<ref>(b) into a generic algorithm on a
coalgebraic level, where the specifics of the transition type are
hidden within the coalgebraic type functor.

§ A CATEGORICAL ALGORITHM FOR BEHAVIOURAL EQUIVALENCE

We proceed to give a formal description of a categorical partition
refinement algorithm that computes the simple quotient of a given
coalgebra under fairly general assumptions.

In addition to <ref>, we fix an endofunctor $H\colon \C\to \C$ that
preserves monomorphisms.

For $\C = \Set$, the assumption that $H$ preserves monomorphisms is
w.l.o.g. First note that every endofunctor on preserves
nonempty monomorphisms. Moreover, for every set functor $H$ there exists a
mono-preserving set functor $H'$ that is identical to $H$ on the
full subcategory of all nonempty
sets <cit.>. Hence, $H'$ has essentially
the same coalgebras as $H$ since there is only one coalgebra
structure on $\emptyset$.

For a given coalgebra $\xi\colon X\to HX$ in $\Set$, any
partition refinement algorithm should maintain a quotient
$q\colon X\twoheadrightarrow \unnicefrac{X}{Q}$ that distinguishes
some (but possibly not all) states with different behaviour, and in
fact, initially $q$ typically identifies everything. Using the
language of universal coalgebras, one can express the transition
type specific steps from <ref> generically. Informally,
our algorithm repeats the following steps until it stabilizes:

Analyse $X\xrightarrow{\xi} HX \xrightarrow{Hq} H(\unnicefrac{X}{Q})$
to identify equivalence classes w.r.t. $q$ (i.e. compound blocks) containing
states that exhibit distinguishable behaviour when considering one more step of
the transition structure $\xi$.

* Use parts of this information to refine $q$.

Here, the composite $Hq\cdot\xi$ (more precisely its kernel) defines
the finer partition $\unnicefrac X P$ in <ref> (our
algorithm will guarantee that this does refine the previous value
of $P$). More precisely, $P$ will be defined to be the kernel of
$Hq\cdot \xi$, and so $P$ is as coarse as possible to be stable
w.r.t. $q\colon X\twoheadrightarrow X/Q$, in the following sense:

Given a coalgebra $\xi \colon X\to HX$, a kernel
$P \rightrightarrows X$ is said to be stable
w.r.t. a morphism $q\colon X\to Y$ provided that there exists a morphism
$\xi/q\colon X/P \to HY$ such that the following square

\[
\begin{tikzcd}
\arrow{r}{\xi}
\arrow[->>]{d}[swap]{\kappa_{P}}
\arrow{d}{Hq}
\\
\arrow{r}{\xi/q}
\end{tikzcd}
\]

Equivalently, the kernel $\pi_1,\pi_2\colon P\rightrightarrows X$ is
stable w.r.t. $q$ if $Hq\cdot \xi \cdot \pi_1 = Hq\cdot \xi \cdot
\pi_2$.

Note that $P \rightrightarrows X$ is stable
w.r.t. $\kappa_P\colon X \epito X/P$ iff $\kappa_P$ is a coalgebra
morphism and thus represents a quotient of $(X, \xi)$.

This definition of stability for a coalgebra $\xi\colon X\to HX$ matches the
concrete instances we have seen in <ref>:

* In a transition system $\xi\colon X\to \Potf X$, $P\rightrightarrows X$ is stable
w.r.t. $\kappa_Q\colon X\twoheadrightarrow X/Q$ if for all elements in the
same block $x,x'\in B\in X/P$ and any other block $B'\in X/Q$, $x$ has an
edge to $B'$ iff $x'$ has an edge to $B'$ [47].

* In a weighted system $\xi\colon X\to \R^{(X)}$, stability of $P
\rightrightarrows X$ w.r.t. $X/Q$ means that all elements of the same block
$x,x'\in B\in X/P$ have the same accumulated transition weight to any other
block $B'\in X/Q$, i.e. $\sum_{y\in B'} \xi(x)(y) = \sum_{y\in B'}\xi(x')(y)$.
This is called `compatibility' in [56].

* For LTSs, Blom and Orzan [12] define the signature of
state $x\in X$ with respect to $q$ as $Hq\cdot \xi(x)$ (with
$HX=\Pot(A\times X)$) and then define a partition $X/P$ to be stable if
every two members $(x,x')\in P$ have the same signature w.r.t. $q:=\kappa_P$.

The refinement step (2) above corresponds to
the subblock selection in <ref>. This selection will be
encapsulated at the present level of generality in a routine
$\op{select}$, assumed as a parameter of our algorithm:

A select routine is an operation that receives a chain of two
regular epis
\(
\begin{mytikzcd}
|[inner sep=0mm]|
X\  \arrow[->>]{r}{y}
& Y \arrow[->>]{r}{z}
& Z
\end{mytikzcd}
\)
and returns some morphism $\op{select}(y,z)\colon Y \to K$. We
refer to $Y$ and $Z$ as the objects of subblocks and
compound blocks, respectively.

In our algorithm, $y$ will represent the canonical quotient
$X\twoheadrightarrow X/P$ and $z$ the canonical map
$X/P\twoheadrightarrow X/Q$ given by the invariant that $P$ is finer
than $Q$.  Intuitively, the morphism $\op{select}(y,z)\colon Y\to K$
selects some of the information contained in $Y$ and discards all the
remaining information by identifying the remaining elements. For
example, in the Paige-Tarjan algorithm with $Y=X/P$ and $Z=X/Q$,
$\op{select}$ models the selection of only a single block $S \in X/P$
leading to a split of the surrounding block $C\in X/Q, S\subseteq C$
into two blocks $S$ and $C\setminus S$. In this case,
$\op{select}(y,z)$ is thus essentially a characteristic function of
the following shape:

For sets $S\subseteq C\subseteq X$, define the map

\[
\chi_S^C\colon X\to 3
\qquad
3 = \{0,1,2\}
\qquad
\chi_S^C(x) =
\begin{cases}
2 &\text{if }x \in S \\
1 & \text{if }x \in C\setminus S \\
0 & \text{if }x \in X\setminus C.
\end{cases}
\]

This is a three-valued version of the characteristic function
$\chi_{M}\colon X\to 2$ for a subset $M\subseteq X$. Put
differently, $\chi_S^C$ is the codomain restriction of
$\fpair{\chi_S,\chi_C}\colon X\to 2\times 2$ obtained by leaving out
the impossible case of $x\in S\setminus C$.

We present some examples of select routines. Throughout, we fix
a chain
\(
\begin{mytikzcd}[inlinecd]
|[inner sep=0mm]|
X\  \arrow[->>]{r}{y}
& Y \arrow[->>]{r}{z}
& Z
\end{mytikzcd}
\)
of quotients.

*  In Hopcroft's
algorithm [31], and in all the known efficient
partition refinement algorithms mentioned so far, the goal is to
find a proper subblock that is at most half the size of the compound
block it is contained in. The optimized version of our algorithm
over $\C = \Set$ (<ref>) will use the same
strategy, embodied in the following $\op{select}$ routine. First, we
identify the elements of $Y$ with the corresponding equivalence
classes in $\unnicefrac{X}{\ker y}$ and those of $Z$ with
equivalence classes in $X/\ker(z \cdot y)$. Now let $S$ be a
subblock, i.e. $S \in \unnicefrac{X}{\ker y} \cong Y$, such that its
compound block,
i.e. $C = z(S) \in \unnicefrac{X}{\ker(z \cdot y)} \cong Z$
satisfies $2\cdot |S| \le |C|$. Then we put (using our
notation (<ref>) for equivalence classes induced by
the map $z$):

\begin{equation}\label{eq:select}
\op{select}(y,z) = \chi_{\{S\}}^{[S]_z}\colon Y\to 3.
\end{equation}

Note that we then have

\[
\op{select}(y,z)\cdot y = \chi_S^C\colon X\to 3.
\]

If there is no such $S \in Y$, then $X$ is infinite or $z$ is an isomorphism,
and in either case we simply put $\op{select}(y,z) = \id_Y$.

*  One obvious choice for
$\op{select}(y,z)\colon Y\to K$ is the identity on $Y$, so that
all of the information present in $Y$ is used for further
refinement. We will explain in <ref> how under this
choice, our algorithm instantiates to König and Küpper's final chain
algorithm [36].

* Two other, trivial, choices are
$\op{select}(y,z)\colon Y\overset{!}\to 1$ and
$\op{select}(y,z)=z$. Since both of these choices discard all the
information in $Y$, this will leave the partitions computed by the
algorithm unchanged, see the proof of <ref>.

Given a select routine, the most general form of our
partition refinement algorithm works as follows. Given a coalgebra
$\xi\colon X\to HX$, we successively refine equivalence relations
(i.e. kernel pairs) $Q \rightrightarrows X$ and
$P \rightrightarrows X$, maintaining the invariant that $P$ is finer
than $Q$ (cf. <ref>), which is witnessed by a
(necessarily unique) morphism $f\colon X/P \epito X/Q$ such that
$f \cdot \kappa_P = \kappa_Q$, where $\kappa_P$ and $\kappa_Q$ denote
the canonical quotients (i.e. coequalizers) of the above two kernel
pairs (<ref>).

Before each iteration of the main loop, we take into account new
information on the behaviour of states, represented by a morphism
$q\colon X\to K$, and accumulate this information in a morphism
$\bar q\colon X\to \bar K$ where $\bar K$ is the Cartesian product of
the instances of $K$ encountered up to the present iteration. In order
to facilitate the analysis later, we index the variables
$P,Q,f,q,\bar q$ over loop iterations $i$ in the description. For
brevity, we will just write the objects $Q_i$ and $P_i$ in lieu of the
respective kernel pairs $P_i \rightrightarrows X$ and
$Q_i \rightrightarrows X$.

Given a coalgebra $\xi\colon X\to HX$ and a $\op{select}$ routine,
initially put

\begin{equation*}
Q_0  = X \times X,\qquad
\bar q_0  = \mathbin{!}\colon X \to 1 = K_0,\qquad
P_0 =  \ker(
X \xrightarrow{\xi}
HX \xrightarrow{H!} H1).
\end{equation*}

Then iterate the following steps, with $i$ counting iterations starting
at $0$, while $P_i$ is properly finer than $Q_i$:

$q_{i+1} := {\!\!\begin{mytikzcd}[inlinecd,sep=2.5em]
X \arrow[->>]{r}{\kappa_{P_i}}
& \unnicefrac{X}{P_i} \arrow{r}{\op{select}(\kappa_{P_i},f_i)}
&[10mm] K_{i+1}
\end{mytikzcd}\!\!}$,
$\bar q_{i+1} := \fpair{\bar q_i,q_{i+1}}\colon
\begin{mytikzcd}[inlinecd]
X \arrow{r}
& \prod_{j \le i} K_i × K_{i+1}
\end{mytikzcd}$

where $f_i\colon X/P_i\twoheadrightarrow X/Q_i$ witnesses that
$P_i$ is finer than $Q_i$.

*  $Q_{i+1} := \ker\bar q_{i+1} = Q_i\cap \ker q_{i+1}$

$P_{i+1} := \ker\big(\!\begin{mytikzcd}[inlinecd] X \arrow{r}{\xi}
& HX \arrow{rr}{H\bar q_{i+1}} && H\prod_{j\le i+1} K_j
\end{mytikzcd}\!\big)$

Upon termination of the above loop return

Note that <ref> is precisely the informal <ref>

* the partitions and equivalence relations are replaced by
coequalizers and kernel pairs;

* $P_i$ being properly finer than $Q_i$ means that the canonical
morphism $f_i\colon X/P_i \epito X/Q_i$ is not an isomorphism;

* in Step <ref>, we have
$\ker \bar q_{i+1} = \ker \fpair{\bar q_i,q_{i+1}}= \ker \bar q_i
\cap \ker q_{i+1} = Q_i\cap \ker q_{i+1}$, see (<ref>);

* transition type specific steps involve how the type functor
$H$ acts on morphisms;

* Step <ref> makes $P_{i+1}$ stable w.r.t. $\bar q_{i+1}$;

* the choice of a subblock $S$ and a compound block $C$ is
performed by the $\op{select}$ routine.

In general, <ref> need not terminate, but we
present sufficient conditions for termination in
<ref>. We now proceed to show that when
<ref> terminates, then it returns the (carrier object of
the) simple quotient of $(X,\xi)$, i.e. we prove correctness. We
continue to use the notation established in
Algorithm <ref>. Since $\bar q$ accumulates more information in
every step, it is clear that $P$ and $Q$ are being successively

For every $i$, we have monomorphisms
$P_{i+1} \monoto P_i \monoto Q_{i+1} \monoto Q_{i}$ witnessing
inclusions of relations.

(The above inclusions state that the kernel $P_{i+1}
\rightrightarrows X$ is finer than the kernel $P_i \rightrightarrows X$ etc., see <ref>.)

We have that $Q_{i+1}$ is finer than $Q_i$ by definition
and use <ref><ref> for the remaining inclusions:

*  $P_{i+1}\monoto P_i$: Let $p\colon \prod_{j\le i+1} K_j \to \prod_{j\le i} K_j$ be the product projection.
We have
\(
H\bar q_i \cdot \xi = H p \cdot H\bar q_{i+1} \cdot
\xi
\),
so $P_{i+1} = \ker (H\bar q_{i+1}\cdot \xi)$ is finer than $P_i = \ker(H\bar q_i\cdot
\xi)$.

* $P_i\monoto Q_{i+1}$: First observe that for every $i$, $P_i$ is
finer than $\ker q_{i+1}$ because $q_{i+1}$ factors through
$\kappa_{P_i}\colon X\epito\unnicefrac{X}{P_i}$ by step <ref>
in <ref>. We now obtain the desired result by induction on
$i$. In the base case we have that $P_0$ is finer than
$Q_1 = \ker \fpair{\bar q_0, q_1} = \ker \fpair{!, q_1} = \ker q_1$.
For the induction step ($i> 0$), since
$Q_{i+1}=Q_i\cap \ker q_{i+1}$, it suffices to show that $P_i$ is
finer than $Q_i $ and $\ker q_{i+1}$. The latter is just our lead-in
observation, and for the former use the inductive hypothesis
($P_{i-1}\monoto Q_i$) and the fact that,
by <ref>, $P_i$ is finer than $P_{i-1}$.

One of the key ingredients in the correctness proof is that the
partition $X/P_i$ is one “transition step” ahead of $X/Q_i$,
i.e. the kernel $P_i$ is stable w.r.t. the quotient $\kappa_{Q_i}$:
The extra property that $\xi/Q_i$ is monic is used
later! So please do not reformulate as `$P_i$ is stable
w.r.t. $Q_i$' because more is proved here and needed later.

There exist monomorphisms
$\unnicefrac{\xi}{Q_i}\colon \unnicefrac{X}{P_i} \monoto H(\unnicefrac{X}{Q_i})$
for $i\ge 0$ (necessarily unique) such that (<ref>)

\begin{equation}
\begin{mytikzcd}[
row sep=4mm,
column sep=12mm,
\arrow[->>]{d}[swap]{\kappa_{P_i}}
\arrow{r}{\xi\ }
&  HX
\arrow[->]{d}[yshift=1pt]{H\kappa_{Q_i}}
\\
\unnicefrac{X}{P_i}
\arrow[dash pattern=on 2pt off 1pt,>->]{r}{\ \unnicefrac{\xi}{Q_i}}
& H (\unnicefrac{X}{Q_i})
\end{mytikzcd}
\label{eq:xiQuotient}
\end{equation}

Since $Q_i=\ker\bar q_i$, the image factorization of $\bar q_i$ has
the form

\[
\bar q_i=
\big(\!\!
\begin{mytikzcd}
X \arrow[->>]{r}{\kappa_{Q_i}}
& X/Q_i
\arrow[>->]{r}{m}
& \prod_{j\le i} K_j
\end{mytikzcd}\!\!
\big).
\]

By definition of $P_i$ and
because $H$ preserves monos, we thus have
$P_i = \ker(H\bar q_i\cdot \xi)=\ker(H\kappa_{Q_i}\cdot\xi)$, and
hence we obtain $\unnicefrac{\xi}{Q_i}$ as in (<ref>) by
the universal property of the coequalizer $\kappa_{P_i}$:

\[
\begin{tikzcd}
\arrow[xshift=-1mm]{d}\arrow[xshift=1mm]{d}
\\
\arrow[->>]{d}[swap]{\kappa_{P_i}}
\arrow{r}{\xi\ }
\arrow[->]{d}[yshift=1pt]{H\kappa_{Q_i}}
\arrow{rd}{H\bar q_i}
\\
\unnicefrac{X}{P_i}
\arrow[dash pattern=on 2pt off 1pt,>->]{r}{\ \unnicefrac{\xi}{Q_i}}
H (\unnicefrac{X}{Q_i})
\arrow[>->]{r}{Hm}
H\big(\prod_{j\le i} K_j\big)
\end{tikzcd}
\]

In fact, $\kappa_{P_i}$ is the regular-epi part of the factorization of $H\bar
q_i\cdot \xi$, and so $Hm\cdot \xi/Q_i$ is the mono part, and thus $\xi/Q_i$
is also a monomorphism.

If $P_i = Q_i$ for some $i$, then $\unnicefrac{X}{Q_i}$ carries a unique coalgebra
structure making $\kappa_{P_i}$ a coalgebra morphism.

For $\C = \Set$, this means that all states of $X$ that are
merged by the algorithm are actually behaviourally equivalent. We
still need to prove the converse, namely that all behaviourally equivalent
states are indeed identified in $X/Q_i$:

Let $h\colon (X,\xi)\to (D,d)$ represent a quotient of $(X,\xi)$. Then
$\ker h$ is finer than both $P_i$ and $Q_i$, for all $i\ge 0$.

We claim that

\begin{equation}\label{eq:hq-to-hp}
\text{if $\ker h$ is finer than $Q_i$, then $\ker h$ is finer than $P_i$}.
\end{equation}

This is seen as follows: If $\ker h$ is finer than $Q_i$, then
$\kappa_{Q_i}\colon X\to\unnicefrac{X}{Q_i}$ factorizes through $h\colon X\epito D$, so
that $H\kappa_{Q_i}\cdot\xi$ factorizes through $Hh\cdot\xi$ and hence
through $h$, since $Hh\cdot\xi=d\cdot h$:

\[
\begin{mytikzcd}
\arrow{r}{\xi}
\arrow{d}{h}
\arrow{d}{Hh}
\arrow{r}{H\kappa_{Q_i}}
\\
\arrow{r}{d}
\arrow[swap]{ru}{Hq}
\end{mytikzcd}
\]

Since $P_i=\ker(H\kappa_{Q_i}\cdot\xi)$, this implies that $\ker h$
is finer than $P_i$.  The claim of the lemma is then proved by
induction: for $i=0$, the claim for $Q_0=X\times X$ is trivial, and
the one for $P_0$ follows by (<ref>). The inductive step
follows from <ref>: $\ker(h) \monoto P_i \monoto
Q_{i+1}$, whence we are done by (<ref>).

If $P_i = Q_i$ for some $i$, then $\unnicefrac{\xi}{Q_i}\colon \unnicefrac{X}{Q_i}\to
H(\unnicefrac{X}{Q_i})$ is a simple coalgebra.

Let $h\colon (X,\xi) \epito (D,d)$ represent a quotient.

* We first prove that for all $i\ge 0$,

\begin{equation}\label{eq:hq-to-hp}
\text{if $\ker h$ is finer than $Q_i$, then $\ker h$ is finer than $P_i$}.
\end{equation}

This is seen as follows: If $\ker h$ is finer than $Q_i$, then
$\kappa_{Q_i}\colon X\epito\unnicefrac{X}{Q_i}$ factorizes through
$h\colon X\epito D$, i.e. we have some
$q\colon D \epito \unnicefrac{X}{Q_i}$ such that
$q \cdot h = \kappa_{Q_i}$ (see
<ref><ref>). So $H\kappa_{Q_i}\cdot\xi$
factorizes through $Hh\cdot\xi$ and hence through $h$, since
$Hh\cdot\xi=d\cdot h$:

\[
\begin{mytikzcd}
\arrow{r}{\xi}
\arrow[->>]{d}[swap]{h}
\arrow{d}{Hh}
\arrow{r}{H\kappa_{Q_i}}
\\
\arrow{r}{d}
\arrow[swap]{ru}{Hq}
\end{mytikzcd}
\]

Since $P_i=\ker(H\kappa_{Q_i}\cdot\xi)$, this implies that $\ker h$
is finer than $P_i$, again by <ref><ref>.

* Next we prove by induction on $i$ that $\ker h$ is finer than
both $P_i$ and $Q_i$, for all $i\ge 0$. For $i=0$, the claim for
$Q_0=X\times X$ is trivial, and the one for $P_0$ follows
by (<ref>). In the induction step, we have by the
inductive hypothesis that $\ker(h)$ is finer than $P_i$, thus by
<ref> also finer than $Q_{i+1}$ and consequently
by (<ref>) finer than $P_{i+1}$.

* Now we are ready to prove the claim of the theorem. Let
$q\colon (\unnicefrac{X}{Q_i},\unnicefrac{\xi}{Q_i}) \epito (D,d)$
represent a quotient. Then
$q\cdot \kappa_{Q_i}\colon (X,\xi) \to (D,d)$ represents a quotient
of $(X,\xi)$, so by point (2) above, $\ker( q\cdot\kappa_{Q_i})$ is
finer than $Q_i$. By <ref><ref>,
$Q_i = \ker(\kappa_{Q_i})$ is also finer than
$\ker( q\cdot\kappa_{Q_i})$, so
$\ker(q\cdot \kappa_{Q_i}) = \ker(\kappa_{Q_i}) =Q_i$.  This implies
that $\kappa_{Q_i}\colon X\epito X/Q_i$ is the regular epi part of
the image factorization of $q\cdot \kappa_{Q_i}$, i.e. we have
$m \cdot \kappa_{Q_i} = q \cdot \kappa_{Q_i}$ for some monomorphism
$m$. Since $\kappa_{Q_i}$ is an epimorphism, we obtain $m = q$,
i.e. $q$ is a monomorphism, and hence an isomorphism.

Most classical partition refinement algorithms are parametrized by an initial
partition $\kappa_{\mathcal{I}}\colon X\twoheadrightarrow
\unnicefrac{X}{\mathcal{I}}$. We start with the trivial partition $!\colon X \to 1$
because a non-trivial initial partition might split equivalent behaviours and
then would invalidate <ref>. To accommodate an initial partition
$\unnicefrac{X}{\mathcal{I}}$ coalgebraically, replace $(X,\xi)$ with the
coalgebra $\fpair{\xi,\kappa_\mathcal{I}}$ for the functor
$H(-)×\unnicefrac{X}{\mathcal{I}}$ – indeed, already $P_0$ will then be finer
than $\mathcal{I}$.

We look in more detail at two corner cases of the algorithm
where the select routine retains all available information,
respectively none.

If $\op{select}(
\begin{mytikzcd}
|[inner sep=0mm]|
X\  \arrow[->>]{r}{y}
& Y \arrow[->>]{r}{z}
& Z
\end{mytikzcd}
) = \id_Y$ (cf. <ref><ref>),
then <ref> becomes König and Küppers' final chain
algorithm [36], as we will now explain.

* Recall that $H$ induces the final chain:

\[
1 \xleftarrow{!} H1 \xleftarrow{H!} H^21 \xleftarrow{H^2!} \cdots
\xleftarrow{H^{i-1}!} H^i 1 \xleftarrow{H^i !} H^{i+1} 1
\xleftarrow{H^{i+1} !} \cdots
\]

(The chain is transfinite but we consider only the first $\omega$
stages.)  Every coalgebra $\xi\colon X\to HX$ then induces a
canonical cone $\xi^{(i)}\colon X\to H^i 1$ on the final
chain, defined inductively by

\[
\xi^{(0)}=\mathbin{!}\colon X \to H^0 1 = 1
\quad\text{and}\quad
\xi^{(i+1)} = (X \xrightarrow{\xi} HX \xrightarrow{H\xi^{(i)}}
HH^i 1 = H^{i+1} 1).
\]

The objects $H^n 1$ may be thought of as domains of $n$-step
behaviour for $H$-coalgebras. If $\C=\Set$ and $X$ is finite, then
states $x$ and $y$ are behaviourally equivalent iff
$\xi^{(i)}(x) = \xi^{(i)}(y)$ for all $i < \omega$
[58].  In fact, Worrell showed this for
unrestricted $X$ and for finitary set functors $H$,
i.e. set functors preserving filtered colimits; equivalently, $H$
is finitary if for every $x \in HX$ there exists a finite subset
$m\colon Y \subto X$ and $y \in HY$ such that $x = Hm(y)$. Note
that for a finite coalgebra for an arbitrary set functor $H$,
behavioural equivalence remains the same when we pass to the
finitary part of $H$, i.e. the functor given by

\[
H_f X = \bigcup\{Hm[Y] \mid \text{$m\colon Y \subto X$ and $Y$
\]

To see this note that if two states in a finite
coalgebra can be identified by a coalgebra morphism into some $H$-coalgebra,
then they can be identified by a coalgebra morphism into a finite
$H$-coalgebra. This is just by image factorization of coalgebras
(see <ref>).

* The inclusions $P_i \monoto Q_{i+1}$ in <ref>
reflect that only some and not necessarily all of the information
present in the relation $P_i$ (resp. the quotient
$\unnicefrac{X}{P_i}$) is used for further refinement. If indeed
everything is used, then $Q_{i+1}= P_i$, and our algorithm simply computes the
kernels of the morphisms $\xi^{(i)}\colon X \to H^i 1$ forming the
canonical cone:

If $\op{select}(
\begin{mytikzcd}[inlinecd]
|[inner sep=0mm]|
X\  \arrow[->>]{r}{y}
& Y \arrow[->>]{r}{z}
& Z
\end{mytikzcd}\!\!) = \id_Y$, then for all $i\in
\N$, $Q_i=\ker \xi^{(i)}$.

With $\op{select}(y,z) = \id_Y$, we have
$q_{i+1} = \kappa_{P_i}\colon X\to \unnicefrac{X}{P_i}$, and so
$\ker q_{i+1} = P_i$ for all $i\in \N$. Thus, $\ker q_{i+1}$ is
finer than $Q_i$ by <ref>. It follows that
$Q_{i+1} = Q_i\cap \ker q_{i+1} = \ker q_{i+1} = P_i$.

In order to prove that $Q_i=\ker \xi^{(i)}$, for all $i\in \N$, we
construct monomorphisms $m_i\colon X/Q_i\rightarrowtail H^{i}1$ with
$m_i\cdot \kappa_{Q_i} = \xi^{(i)}$ inductively (which implies
$Q_i = \ker \xi^{(i)}$ by <ref>.<ref>). For
$i=0$, we trivially have $m_0\colon X/Q_0 \xrightarrow{\cong} 1$. In the inductive
step, we put $m_{i+1} := Hm_i\cdot \xi/Q_i$:

\[
\begin{mytikzcd}[baseline=(bot.base)]
X \arrow{r}{\xi}
\descto{dr}{\eqref{eq:xiQuotient}}
\arrow[->>]{d}[swap]{\kappa_{Q_{i+1}}}
\arrow[shiftarr={yshift=7mm}]{rr}{\xi^{(i+1)}}
& HX
\arrow{d}[swap]{H\kappa_{Q_i}}
\descto[pos=0.2]{dr}{IH}
\arrow{r}{H\xi^{(i)}}
& H^{i+1} 1
\\
\arrow[>->]{r}{\xi/Q_i}
& H(X/Q_i)
\arrow[>->]{ur}[swap]{Hm_i}
& {}
\end{mytikzcd}
\tag*{\qedhere}
\]

Intuitively, the select routine in <ref> retains all
available information. The other extreme is the following:

We say that select is discarding at $X \overset{y}{\epito} Y
\overset{z}{\epito} Z$ if $\op{select}(y,z)\colon Y\to K$ factorizes through $z$.
Further, we call $\op{select}$ progressing if $\op{select}(y,z)$ is
discarding at $y, z$ only if $z$ is an isomorphism.

* The $\op{select}$ picking the smaller half in
<ref><ref> is progressing. We
prove the contraposition: if $z$ in
$X \overset{y}{\epito} Y \overset{z}{\epito} Z$ is not an
isomorphism, let $S \in \unnicefrac{X}{\ker y} \cong Y$ be the
subblock used in the definition (<ref>) of
$\op{select}(y,z)$, and note that then there also exists a subblock
$B \in \unnicefrac{X}{\ker y} \cong Y$ with $z(B) = z(S)$ and
$|S| \leq |B|$. By the definition of $k=\op{select}(y,z)$, we have
$k(B) = 1 \neq 2 = k(S)$, and so $k$ cannot factor through $z$.

* The $\op{select}$ routine that always returns $\id_Y$ for
$X \overset{y}{\epito} Y \overset{z}{\epito} Z$ in
<ref><ref> is trivially
progressing: if $\id_Y$ factorizes through $z$, then $z$ is a
(split) mono, and hence an isomorphism.

* The $\op{select}$ routine that returns the morphism
$!\colon Y\to 1$ or $z\colon Y\to Z$ is always discarding, and thus
fails to be progressing (unless all regular epis in $\C$ are

If select is progressing, then <ref> terminates and
computes the simple quotient of the input coalgebra $(X,\xi)$,
provided that $(X,\xi)$ has only finitely many quotients.

E.g. for $\C=\Set$, every finite coalgebra has only finitely many quotients.

* We first show that our algorithm fails to progress in
the $(i+1)^{\text{st}}$ iteration, i.e. $Q_{i+1}=Q_i$, iff select
is discarding at $X/P_i,X/Q_i$, i.e. iff
X \overset{\kappa_{P_i}}\twoheadrightarrow
\unnicefrac{X}{P_i} \overset{f_i}\twoheadrightarrow
\unnicefrac{X}{Q_i}
\!\big)$ factorizes through $f_i$.

To see this, first note that select is discarding at
$X/P_i,X/Q_i$ iff $q_{i+1}$ factorizes through $\kappa_{Q_i}$:

\[
\begin{mytikzcd}
\arrow[->>]{r}{\kappa_{P_i}}
\arrow[->>,shiftarr={yshift=6mm}]{rr}{q_{i+1}}
\arrow[->>,swap]{rd}{\kappa_{Q_i}}
\unnicefrac{X}{P_i}
\arrow{r}{k_{i+1}}
\arrow[->>]{d}{f_i}
\\
\unnicefrac{X}{Q_i}
\ar[ru,dashed]
\end{mytikzcd}
\]

We thus have the desired equivalence: $q_{i+1}$ factorizes through
$\kappa_{Q_i}$ iff (by <ref><ref>) $Q_i$ is
finer than $\ker q_{i+1}$ iff
$Q_{i}=Q_i\cap \ker q_{i+1} = Q_{i+1}$.

* We proceed to prove the claim. <ref> shows that
we obtain a chain of successively finer quotients
$\unnicefrac{X}{Q_i}$. Since $X$ has only finitely many quotients,
there must be an $i$ such that $Q_i = Q_{i+1}$, and this implies,
using point (1), that $\op{select}$ is discarding at $X/P_i,
Since the $\op{select}$ routine is progressing, we obtain
$P_i = Q_i$ as desired.

§ INCREMENTAL PARTITION REFINEMENT

In the most generic version of the partition refinement algorithm
(Algorithm <ref>), the partitions are recomputed from scratch in every
step: In Step <ref> of the algorithm, $P_{i+1}=\ker(H\fpair{\bar
q_i,q_{i+1}}\cdot\xi)$ is computed from the information $\bar q_i$ accumulated
so far and the new information $q_{i+1}$, but in general one cannot exploit that
the kernel of $\bar q_i$ has already been computed. We now present a refinement
of the algorithm in which the partitions are computed incrementally, i.e.$P_{i+1}$ is computed from $P_i$ and $q_{i+1}$. This requires the type functor
$H$ to be zippable (<ref>) and the select routine to
respect compound blocks (<ref>).

Note that in Step <ref>, <ref> computes a kernel
$Q_{i+1} = \ker \bar q_{i+1} = \ker \fpair{\bar q_i, q_{i+1}}$ as the
intersection of $\ker(\bar q_i)$ and $\ker(q_i)$ (cf. (<ref>)).

Hence, the partition $X/\ker \bar q_{i+1}$ for such a kernel can be computed in
two steps:

* Compute $\unnicefrac{X}{\ker \bar q_i}$.

* Refine every block in $\unnicefrac{X}{\ker \bar q_{i}}$ with respect to
$q_{i+1}\colon X\to K_{i+1}$.

<ref> can thus be implemented to keep track of the partition
$\unnicefrac{X}{Q_i}$ and then refine this partition by $q_{i+1}$ in
each iteration.

However, the same trick cannot be applied immediately to the
computation of $\unnicefrac{X}{P_i}$, because of the functor $H$
inside the computation of the kernel:
\( P_{i+1} = \ker (H\fpair{\bar q_i, q_{i+1}}\cdot \xi) \).
In <ref>, we will provide sufficient conditions for $H$,
$a\colon D\to A$, $b\colon D\to B$ to satisfy

\[
\ker H\fpair{a,b}
= \ker \fpair{Ha,Hb}.
\]

As soon as this holds for $a=\bar q_i, b=q_{i+1}$, we can optimize the
algorithm by changing Step <ref> to

\begin{equation}
P_{i+1}' := \ker \fpair{H\bar q_i\cdot \xi, Hq_{i+1}\cdot \xi}
\quad(= P_i \cap \ker
(Hq_{i+1}\cdot \xi)).
\label{kernelOptimization}
\end{equation}

The conditions on $a$ and $b$ will be ensured by a condition on select, and
the condition on the functor $H$ is as follows:

A functor $H\colon C\to \D$ is zippable
if the following morphisms are monomorphisms for every objects $A$
and $B$:

\[
\op{unzip}_{H,A,B}\colon
H(A+B) \xrightarrow{\fpair{H(A+!),H(!+B)}} H(A+1) × H (1+B)
\]

Intuitively, if $H$ is a functor on $\Set$, we may think of
elements $t$ of $H(A+B)$ as shallow terms with variables from
$A+B$. Then zippability means that each $t$ is uniquely determined by
the two terms obtained by replacing $A$- and $B$-variables,
respectively, by some placeholder $\gap$, viz. the element of $1$, as
illustrated in the examples in <ref>.

\(
\begin{mytikzcd}[row sep = 0mm]
\arrow[shiftarr={xshift=18mm},mapsto]{d}[xshift=-4mm,pos=0.0,above]{\op{unzip}}
\\
\begin{array}{c}
(a_1a_2\gap a_3 \gap, \\
\phantom{(}\,\gap \gap\,b_1\!\gap b_2)
\end{array}
\end{mytikzcd}
\)
$(-)^*$ is zippable

\(
\begin{mytikzcd}[row sep = 0mm, ampersand replacement = \&]
\{a_1,a_2,b_1\}
\arrow[shiftarr={xshift=18mm},mapsto]{d}[xshift=-4mm,pos=0.0,above]{\op{unzip}}
\\
\begin{array}{r@{\,}l}
(\{a_1,a_2,&\gap\}, \\
\{\gap,&b_1\})
\end{array}
\end{mytikzcd}
\)
$\Potf$ is zippable

\(
\begin{mytikzcd}[row sep = 0mm,
column sep = -13mm,
|[inner xsep=0mm]|
\begin{array}{@{}l@{}}
\big\{\{a_1,b_1\},
\{a_2,b_2\}\big\}
\end{array}
\arrow[start anchor={[xshift=-4mm]},
rounded corners,
to path={ |- (\tikztotarget) \tikztonodes },
|[inner xsep=0mm]|
\begin{array}{@{}l@{}}
\big\{\{a_1,b_2\},
\{a_2,b_1\}\big\}
\end{array}
\arrow[start anchor={[xshift=4mm]},
rounded corners,
to path={ |- (\tikztotarget) \tikztonodes },
\\
|[inner xsep = 1mm]|
\begin{array}{@{}l@{}}
(\big\{\{a_1,\gap\},\{a_2,\gap\}\big\}, \\
\phantom{(}\big\{\{\gap, b_1\},\{\gap,b_2\}\big\}) \\
\end{array}
\end{mytikzcd}
\)

$\Potf\Potf$ is not zippable

Zippability of -Functors for sets
$A=\{a_1,a_2,a_3\}$, $B=\{b_1,b_2\}$.

Let $H$ be zippable and $f\colon A\to C$, $g\colon B\to D$. Then the following
is a mono:

\[
H(A+B) \xrightarrow{\fpair{H(A+g),H(f+B)}} H(A+D) × H (C+B)
\]

By finality of $1$, the diagram

\[
\begin{mytikzcd}[column sep = 3cm]
\arrow{d}[left]{\fpair{H(A+g),H(f+B)}}
\arrow[>->]{dr}[sloped,above]{
\op{unzip}_{H,A,B}
= \fpair{H(A+!),H(!+B)}
\\
H(A+D) × H (C+B)
\arrow{r}{H(A+!) × H (!+B)}
H(A+1) × H (1+B)
\end{mytikzcd}
\]

commutes. Since the diagonal arrow is monic, so is

For the remainder of
<ref>, we assume that $\C = \Set$.

However, most proofs are category-theoretic to clarify where working
in $\Set$ is really needed and where the arguments are more general.

* Constant functors $X\mapsto A$ are zippable: $\op{unzip}$
is the diagonal $A \to A \times A$.

* The identity functor is zippable since
\(
\fpair{A+!, !+B}\colon A+B \to (A+1) × (1+B)
\)
is monic in $\Set$.

* From Lemma <ref> it follows that every
polynomial endofunctor is zippable. Indeed, a polynomial functor
is precisely one that is build from constant and the identity
functors using (finite) products and coproducts (cf. <ref><ref>).

Zippable endofunctors are closed under (possibly infinite) products, coproducts and

(Recall that products and coproducts of functors are formed
pointwise, e.g. $(F+G)(X)=FX+GX$.)

For the closure under products and coproducts, we only provide the proof for the
binary case; the proof for arbitrary products and coproducts is
completely analogous. Let $F,
G$ be endofunctors.

* Suppose that both $F$ and $G$ are zippable. That $F \times
G$ is zippable follows from monos being closed under products:

\[
\begin{mytikzcd}[column sep=15mm,row sep=5mm]
F(A+B) × G(A+B)
\ar[r,>->,"\op{unzip}_{F,A,B} × \op{unzip}_{G,A,B}"{yshift=2mm}]
\ar[to path={
|- (\tikztotarget) \tikztonodes
rounded corners,
]{dr}[below,near end]{\op{unzip}_{F×G,A,B}}
F(A+1) × F(1+B)
×G(A+1) × G(1+B)
\ar[phantom,d,"\cong" {sloped}]
\\
\big(F(A+1)
× \big(F(1+B)
× G(1+B)\big).
\end{mytikzcd}
\]

* Suppose again that $F$ and $G$ are zippable. To see that $F+G$ is zippable consider the diagram

\[
\begin{mytikzcd}[column sep=15mm,row sep=5mm]
F(A+B) + G(A+B)
\ar[r,>->,"\op{unzip}_{F,A,B} + \op{unzip}_{G,A,B}"{yshift=2mm}]
\ar[to path={
|- (\tikztotarget) \tikztonodes
rounded corners,
]{dr}[below,near end]{\op{unzip}_{F×G,A,B}}
\big(F(A+1) × F(1+B)\big)
+ \big(G(A+1) × G(1+B)\big)
\ar[>->,d,"\fpair{(\pi_1+\pi_1), (\pi_2+\pi_2)}" {right}]
\\
\big(F(A+1)
× \big(F(1+B)
+ G(1+B)\big).
\end{mytikzcd}
\]

The horizontal morphism is monic since monos are closed under
coproducts in $\Set$.

The vertical morphism is monic since for any sets
$A_i$ and $B_i$, $i = 1, 2$, the following morphism clearly is a

\[
(A_1×B_1) + (A_2×B_2)
\xrightarrow{\fpair{(\pi_1+\pi_1), (\pi_2+\pi_2)}}
(A_1+A_2) × (B_1+B_2).
\]

* Suppose now that $F$ is a subfunctor of $G$ via $s\colon F
\rightarrowtail G$, where $G$ is zippable. Then the following diagram
shows that $F$ is zippable, too:

\[
\begin{mytikzcd}[column sep = 2cm,baseline=(bot.base)]
\arrow{r}{\op{unzip}_{F,A,B}}
\arrow[>->]{d}[left]{s_{A×B}}
\arrow[>->,
to path={
-- ([xshift=-4mm]\tikztostart.west)
|- ([yshift=-4mm]\tikztotarget.south)
-- (\tikztotarget)
rounded corners,
& F(A+1) × F(1+B)
\arrow[>->]{d}{s_{A+1} × s_{1+B}}
\\
\arrow[>->]{r}{\op{unzip}_{G,A,B}}
& G(A+1) × G(1+B).
\end{mytikzcd}
%    \tag*{\qedhere}
\]

Indeed, since the composition of the lower and left-hand morphisms
is monomorphic, so is the upper morphism.

If $H$ has a componentwise monic natural transformation
$H(X+Y) \rightarrowtail HX × HY$, then $H$ is zippable.

Let $\alpha_{X,Y}\colon H(X+Y) \rightarrowtail HX × HY$ be monic and
natural in $X$ and $Y$. Then the square

\[
\begin{mytikzcd}[column sep = 4cm]
H(A+B) \ar[d,>->,"\alpha_{A,B}"'] \ar[r,"\op{unzip} = \fpair{H(A+!),H(!+B)}"]
& H(A+1)×H(1+B)
\ar[d,"\alpha_{A,1}×\alpha_{1,B}"]
\\
\ar[r,>->,"\fpair{HA×H!,H!×HB}"]
& (HA×H1)×(H1×HB)
\end{mytikzcd}
\]

commutes by naturality of $\alpha$. The
bottom morphism is monic because it has a left inverse,
$\pi_1×\pi_2$. Therefore, $\op{unzip}$ is monic as well.

* For every commutative monoid, the monoid-valued functor
$M^{(-)}$ (see <ref><ref>) admits a natural
isomorphism $M^{(X+Y)} \cong M^{(X)} \times M^{(Y)}$, and hence is
zippable by Lemma <ref>.

* As special cases of monoid-valued functors we obtain
that the finite powerset functor $\Potf$ and the bag functor $\Bagf$
are zippable.

* By <ref>, the full powerset functor $\Pot$ is zippable.

* The distribution functor $\Dist$ (see Example <ref>) is
a subfunctor of the monoid-valued functor $\R_{\ge 0}^{(-)}$ for the
additive monoid $\R_{\ge 0}$ of real numbers, and hence is zippable by
Item <ref> and Lemma <ref>.

* The previous examples together with the closure properties in
Lemma <ref> show that a number of functors of interest
are zippable, e.g. $2×(-)^\Inputs$,
$2×\Potf(-)^\Inputs$, $\Potf(\Inputs×(-))$, $2×\big((-)+1\big)^\Inputs$,
and variants where $\Potf$ is replaced by $\Bagf$, $M^{(-)}$, or

Out of the above results, only zippability of the identity and
coproducts of zippable functors make use of properties of $\Set$
(<ref>). Indeed, zippable functors on a
category $\C$ are closed under coproducts as soon as monomorphisms
are closed under coproducts in $\C$, which is satisfied in most
categories of interest. Zippability of the identity holds whenever
$\C$ is extensive, i.e. it has well-behaved set-like coproducts (see
e.g. [16] or <ref> later). Examples of
extensive categories are the categories of sets, posets and graphs
as well as any presheaf category. We will take a closer look at
extensive categories when we discuss multisorted coalgebras

The monotone neighbourhood functor, which maps a set $X$ to the set

\[
\mathcal{M}(X) =
\{
N \subseteq \Pot X
\mid
A \in N \wedge B\supseteq A
\implies B\in N
\},
\]

of monotone neighbourhood systems over $X$, is not zippable, that
is, there are distinct monotone neighbourhood systems that are
identified by $\op{unzip}$. Indeed, denoting the upwards closure
of a set system by $(-)\upa$, we have

\begin{align*}
\op{unzip}\left(\left\{
\{a_1,b_1\},
\{a_2,b_2\}
\right\}\!\upa\right)
\big(
\big\{\{a_1,\gap\},
\{a_2,\gap\}\big\}\upa
\big\{\{\gap,b_1\},
\{\gap,b_2\}\big\}\upa
\big)
\\&=
\op{unzip}\left(\left\{
\{a_1,b_2\},
\{a_2,b_1\}
\right\}\!\upa\right).
\end{align*}

The functor $\Potf\Potf$ fails to be zippable, as shown in
<ref>. First, this shows that zippable functors are
not closed under quotients, since $\Potf\Potf$ is a quotient of the
polynomial, hence zippable, functor $HH$ where
$HX = \coprod_{n <\omega} X^n$.  Secondly, this shows that zippable
functors are not closed under composition.

The following example shows that the optimized algorithm,
i.e. <ref> run with (<ref>) in lieu of
Step <ref>, is not correct for the non-zippable functor
$\Potf\Potf$, even though the $\op{select}$ routine used here (see
<ref><ref>) behaves sufficiently
well (specified later in <ref> and
cf. <ref>).

Consider the following coalgebra $\xi\colon X\to HX$ for $HX = 2×\Potf\Potf X$:

n/.style =
execute at begin node=\(,%
execute at end node=\),
inner sep = 1mm,
grow'                   = right,
sibling distance        = 7mm,
level distance          = 12mm,
edge from parent/.style =

shorten <= 1pt,
shorten >= 1pt,
level 1/.append style =
sibling distance = 12mm,
level 2/.append style =
sibling distance = 7mm,
every node/.style       = n,font=,
dummy/.style    = circle,
inner sep=1pt,
outer sep=1pt,
minimum width=0,
minimum height=0,
final/.style    =
line width=1pt,
inner sep =1pt,
(a1) a_1
child  node[dummy]
child  node[final] (a2) a_2
child  node (a3) a_3
child  node[dummy]
child  node (a6) a_6

child  node[dummy]
child  node (a4) a_4
child  node (a5) a_5
child  node[dummy]
child  node[final] (a7) a_7

(b1) at ([xshift=6cm]a1)b_1
child  node[dummy]
child  node[final] (b2) b_2
child  node (b3) b_3
child  node[dummy]
child  node[final] (b6) b_6

child  node[dummy]
child  node (b4) b_4
child  node (b5) b_5
child  node[dummy]
child  node (b7) b_7

Final states, i.e. states $x$ with $\pi_1(\xi(x)) = 1$, are indicated by a circle. Let us replace
step <ref> of <ref> by equation (<ref>),
i.e. we compute

\begin{equation*}
P_{i+1} = P_{i+1}' \overset{\eqref{kernelOptimization}}{=}
\ker \fpair{H\bar q_i\cdot \xi,Hq_{i+1}\cdot\xi}
= \ker P_i' \cap \ker (Hq_{i+1}\cdot\xi).
% \tag*{\eqref{kernelOptimization}}
\end{equation*}

We will show that the states $a_1$ and $b_1$ are identified by all $P_i'$ and $Q_i$, i.e. they are not distinguished by the algorithm, although they are
clearly behaviourally inequivalent.

We simplify the partitions by defining abbreviations for the final and
non-final states without successors as well as the rest,

\[
F:= \{a_2,a_7, b_2,b_6\},
\quad
N:=\{a_4,a_6, b_4,b_7\}
\quad
\text{and}
\quad
R:=\{a_1,a_3,a_5, b_1,b_3,b_5\}.
\]

Then we run the optimized algorithm with the $\op{select}$ routine in <ref><ref>, computing $Q_i$ and $P_{i}'$ (see
(<ref>)), and we obtain the following sequence of

i     q_i     XQ_i     XP_i'

F, N,

F,N, R
F,N, {a_1,b_1}, {a_3,b_5}, {a_5,b_3}

F,N, {a_1,b_1}, {a_3,b_5, a_5,b_3}
F,N, {a_1,b_1}, {a_3,b_5}, {a_5,b_3}

F,N, {a_1,b_1}, {a_3,b_5}, {a_5,b_3}
F,N, {a_1,b_1}, {a_3,b_5}, {a_5,b_3}

For the subblock $S=\{a_3,b_5\}$ selected in the third
iteration we see that $\{a_1, b_1\}$ is not split in $\unnicefrac{X}{P_3'}$

\begin{align*}
H\chi_{\{a_3,b_5\}}^{\{a_3,b_5,a_5,b_3\}} \cdot \xi(a_1)
&= H\chi_{\{a_3,b_5\}}^{\{a_3,b_5,a_5,b_3\}} \myblocklist{\{a_2,a_3\}, \{a_4,a_5\}} \\
&= \phantom{H\chi_{\{a_3,b_5\}}^{\{a_3,b_5,a_5,b_3\}}}\myblocklist{\{0,2\}, \{0,1\}}
\\ &
= \phantom{H\chi_{\{a_3,b_5\}}^{\{a_3,b_5,a_5,b_3\}}}\myblocklist{\{0,1\}, \{0,2\}} \\
&= H\chi_{\{a_3,b_5\}}^{\{a_3,b_5,a_5,b_3\}} \myblocklist{\{b_2,b_3\}, \{b_4,b_5\}}
= H\chi_{\{a_3,b_5\}}^{\{a_3,b_5,a_5,b_3\}} \cdot \xi(b_1)
\end{align*}

At this point the algorithm terminates because $\unnicefrac{X}{Q_2} =
\unnicefrac{X}{P_2}$, while incorrectly not distinguishing $a_1$ and

Note that this result remains the same if we chose the subblock
$\{a_5,b_3\}$ in the third iteration or if we chose
$\{a_3,b_5\}$ in the second iteration and $\{a_1,b_1\}$ in the third one.

Observe that, in general,
$\ker H\fpair{a,b}$ differs from $\ker\fpair{Ha,Hb}$ even if $H$ is

For $H=\Potf$ and product projections
$\pi_1\colon A \times B \to A$ and $\pi_2\colon A \times B \to B$,
$\fpair{\Potf\pi_1,\Potf\pi_2}$ in general fails to be injective
although $\Potf\fpair{\pi_1,\pi_2}=\Potf\id_{A \times B}=\id_{\Potf(A
\times B)}$. Thus

\[
\ker \Potf\fpair{\pi_1,\pi_2} \cong \Potf(A \times B) \not\cong
\ker \fpair{\Potf\pi_1,\Potf\pi_2}.
\]

Hence, in addition to zippability of $H$, we will need to enforce constraints on the
select routine to achieve the desired
optimization (<ref>).

The next example illustrates this issue, and a related one: One might
be tempted to implement splitting by a subblock $S$ by using the usual
characteristic function $q_i = \chi_S\colon X \to K_i$.
While this approach is sufficient for systems with real-valued
weights [56], it may in general let
$\ker (H\fpair{\bar q_i, q_{i+1}}\cdot \xi)$ and
$\ker \fpair{H\bar q_i\cdot \xi, Hq_{i+1}\cdot \xi}$ differ even if
$H$ is zippable, thus rendering the algorithm incorrect:

every node/.style=
inner sep = 1pt,
label distance=0mm,
every label/.append style=
execute at begin node=\(,
execute at end node=\),
inner sep=2pt,
x = 14mm,
y = 14mm,
on background layer,
every node/.style=
every node/.append style=
inner sep = 3mm,
line width=2pt,

[partitionQi ]
[fit = (square1) (circle1) (circle2) (circle3)
(triangle2) (triangle1)] ;

[partitionPi ]
[fit = (square1)] ;
[fit = (circle1) (circle2)] ;
[fit = (circle3)] ;
[fit = (triangle2) (triangle1)] ;

$Q_0, P_0$ for $\bar q_0 = \mathbin{!}$

[ partitionQi ]
[fit = (square1)] ;
[fit = (circle1) (circle2)] ;
[fit = (circle3)] ;
[fit = (triangle2) (triangle1)] ;

[ partitionPi ]
[fit = (square1)] ;
[fit = (circle2)] ;
[fit = (circle1)] ;
[fit = (circle3)] ;
[fit = (triangle2) (triangle1)] ;

$Q_1, P_1$ for $\bar q_1 =
\kappa_{P_0}$

Partitions of a coalgebra $\xi$ for $H=\{\blacktriangle,
\mdblksquare, \smblkcircle\} × \Potf(-)$. $\unnicefrac{X}{Q_i}$ is
indicated by dashed, $\unnicefrac{X}{P_i}$ by solid lines.

execute at begin node=\(,
execute at end node=\),
/in top/2,middle/1,bottom/0
[elementX] (circle1) at (0,) c_1;
[elementX] (circle2) at (1,) c_2;
[elementX] (circle3) at (2,) c_3;
[elementX] (square1) at (3,) s_1;
[elementX] (triangle1) at (4,) t_1;
[elementX] (triangle2) at (5,) t_2;

every node/.append style=partitionBlock,inner sep=0mm,
[fit = (topsquare1)] ;
[fit = (topcircle1) (topcircle2)] ;
[fit = (topcircle3)] ;
[fit = (toptriangle2) (toptriangle1)] (XQ1) ;

every node/.append style=partitionBlock,inner sep=0mm,
[fit =  (middlecircle1)] ;
[fit = (middlesquare1)
(middlecircle2) (middlecircle3) (middletriangle2)
(middletriangle1)] (chiS) ;

every node/.append style=partitionBlock,inner sep=0mm,
[fit =  (bottomcircle1)] ;
[fit = (bottomcircle2) ] ;
[fit = (bottomcircle3) (bottomsquare1) (bottomtriangle2)
(bottomtriangle1)]  (chiSC);

[every node/.style=

inner xsep=0cm,
at (chiS.east) $\unnicefrac{X}{\ker \chi_S}$;
at (chiSC.east) $\unnicefrac{X}{\ker \chi_S^C}$;
at (XQ1.east) $\unnicefrac{X}{Q_1} = \unnicefrac{X}{P_0}$;

Grouping of elements when $S:=\{c_1\}$ is chosen as the
next subblock and $C := \{c_1,c_2\}$ as the compound block.

Consider the coalgebra $\xi\colon X\to HX$ for the zippable functor
$H=\{\blacktriangle, \mdblksquare, \smblkcircle\} × \Potf(-)$
illustrated in <ref> (essentially a Kripke
model). The initial partition $\unnicefrac{X}{P_0}$ splits the set
of all states by shape and by $\Potf!$, i.e. states with successors
are distinguished from the ones without
successors (<ref>). Now, suppose that
$\op{select}$ returns $k_1 := \id_{\unnicefrac{X}{P_0}}$, i.e.  retains all information (cf. <ref>), so that
$Q_1 = P_0$ and $P_1$ puts $c_1$ and $c_2$ into different blocks
(<ref>). Since $q_0 = \mathord{!}$, we have $\ker \bar q_1 = \ker
q_1$ and thus simplify notation by directly defining
$\bar q_1 := \kappa_{P_0}$. We now analyse the next partition that
arises when we split w.r.t. the subblock $S=\{c_1\}$ but not
w.r.t. the rest $C\setminus S$ of the compound block
$C=\{c_1,c_2\}$; in other words, we take
$k_2 := \chi_{\{\{c_1\}\}}\colon \unnicefrac{X}{P_1}\to 2$, making
$q_2 = \chi_{\{c_1\}}\colon X\to 2$.  Then,
$H\fpair{\bar q_1,q_2}\cdot \xi$ splits $t_1$ from $t_2$, because
$t_1$ has a successor $c_2$ with $\bar q_1(c_2) = \{c_1,c_2\}$ and
$q_2(c_2) = 0$ whereas $t_2$ has no such successor. However,
$t_1,t_2$ fail to be split by $\fpair{H\bar q_1, Hq_2}\cdot \xi$
because their successors do not differ when we look at successor
blocks in $\unnicefrac{X}{Q_1}$ and $\unnicefrac{X}{\ker \chi_S}$
separately: both have $\{c_1,c_2\}$ and $\{c_3\}$ as successor
blocks in $\unnicefrac{X}{Q_1}$ and $\{c_1\}$ and
$X\setminus\{c_1\}$ as successors in
$\unnicefrac{X}{\ker\chi_S}$ (cf. <ref>). Formally:

\begin{align*}
H\bar q_1\cdot \xi (t_1) &=
(\id×\Potf\kappa_{P_0})\cdot \xi (t_1) =
\{c_1,c_2\},
\{c_3\}
\big\})
= H\bar q_1\cdot \xi (t_2),
\\
H q_2\cdot \xi (t_1) &=
(\id× \Potf\chi_{\{c_1\}})\cdot \xi (t_1) =
0, 1
\big\})
= H q_2\cdot \xi (t_2).
\end{align*}

So if we computed $P_2$ iteratively as in
(<ref>) for $q_2=\chi_S$, then $t_1$ and $t_2$
would not be split, and we would reach the termination condition
$P_2 = Q_2$ before all behaviourally inequivalent states have been

Already Paige and Tarjan <cit.> note that one additionally needs to
split by $C\setminus S=\{c_3\}$, which is accomplished by
splitting by $q_i=\chi_S^C$ (see
<ref><ref>). This is
formally captured by the condition we introduce next and explain
further in <ref>.

A select routine respects compound blocks if whenever
$k= \op{select}(X\overset{y}{\twoheadrightarrow} Y
\overset{z}{\twoheadrightarrow} Z)$
then the union $\ker z\cup \ker k$ is a kernel.

Since in $\Set$, reflexive and symmetric relations are
closed under unions, the definition boils down to $\ker z\cup\ker k$
being transitive. In $\Set$, we have an intuitive characterization:

For maps $a\colon Y\to A$, $b\colon Y\to B$, the following are

* $\ker a\cup \ker b\rightrightarrows Y$ is a kernel (i.e. an
equivalence relation).

* $\ker a\cup \ker b\rightrightarrows Y$ is the kernel of
the pushout of $a$ and $b$.

* For all $x,y,z \in Y$, $a(x) =a(y)$ and $b(y)=b(z)$ implies
$a(x) = a(y) = a(z)$ or $b(x)=b(y)=b(z)$.

* For all $x\in Y$, $[x]_a \subseteq [x]_b$ or  $[x]_b
\subseteq [x]_a$.

The last item states that when we move from $a$-equivalence classes to
$b$-equivalence classes, the classes either merge or split, but do not merge
with other classes and split at the same time. In <ref>, $\ker
a\cup\ker b$ is transitive, and thus also a kernel. For $x\in \{y_1,y_2,y_3\}$,
we have $[x]_b\subseteq [x]_a$ and for $x\in \{y_4,y_5\}$ we have
$[x]_a\subseteq [x]_b$. On the other hand in <ref>, $\ker
a\cup \ker b$ is not transitive because $(y_1,y_3)\in \ker b$ and $(y_3,y_5) \in
\ker a$, but $(y_1,y_5)\not \in \ker a\cup\ker b$, and indeed condition
<ref> of <ref> fails because
$[y_3]_a\not\subseteq [y_3]_b$ and $[y_3]_b\not\subseteq [y_3]_a$ (because $[y_3]_a =
\{y_3,y_4,y_5\}$, $[y_3]_b=\{y_1,y_2,y_3\}$).

.49 [5]
(A1), (A2) (A3), (A4), (A5),
(B1), (B2), (B3), (B4) (B5),
(I1), (I2), (I3), (I4), (I5)

$\ker a\cup \ker b$ is transitive.

.49 [5]
(A1) (A2), (A3) (A4) (A5),
(B1) (B2) (B3), (B4) (B5),
(I1) (I2), (I3), (I4) (I5)

$\ker a\cup \ker b$ is not transitive.

Maps $a\colon Y\to A$ and $b\colon Y\to B$, where the elements of $A$
and $B$ are considered as equivalence classes of elements of $Y$, defining
$a$ and $b$ implicitly. $Y/\ker\fpair{a,b}$ is the block-wise intersection
of the partitions defined by $a$ and $b$.

In <ref> of a concrete run of our algorithm, one sees in
<ref> that $Q_1\cup \ker \chi_S$ fails to be transitive,
while $Q_1\cup \ker \chi_S^C$ is transitive.

(4) $\Rightarrow$ (1) In , kernels are equivalence relations. Obviously, $\ker
a\cup \ker b$ is both reflexive and symmetric. For transitivity,
take $(x,y),(y,z) \in \ker a\cup \ker b$. Then $x, z \in [y]_a\cup
[y]_b$. If $[y]_a\subseteq [y]_b$, then $x,z \in [y]_b$ and $(x,z)
\in \ker b$; otherwise $(x,z) \in \ker a$.

(1) $\Rightarrow$ (2) In , monomorphisms are stable under pushouts, so it is
sufficient to show that $\ker a \cup \ker b$ is the kernel of the
pushout of the regular epis from the image factorization of $a$
and $b$, respectively. In other words, w.l.o.g. we may
assume that $a$ and $b$ are surjective maps, and we need to check that $\ker
a\cup \ker b$ is the kernel of $p:= p_A\cdot a = p_B\cdot b$,
where $p_A$ and $p_B$ are the two injections of the pushout below:

\[
\begin{mytikzcd}[baseline=(bot.base), ampersand replacement=\&]
Y \ar[->>,d,swap,"b"] \ar[->>,r,"a"]
\& A
\ar[d,"p_A"]
\\
\ar[r,"p_B"]
\& P.
\pullbackangle{135}
\end{mytikzcd}
\]

Let $\ker a\cup \ker b$ be the kernel of some $f\colon Y\to Y'$. Then,
$f$ makes the projections of $\ker a$ (resp. $\ker b$) equal and hence
the coequalizer $a$ (resp. $b$) induces a unique $f_A$
(resp. $f_B$) such that the triangles in the diagrams below commute:

\[
\begin{mytikzcd}
\ker a
\ar[r,hook]
\ar[rr,shiftarr={yshift=5mm},"\pi_1"]
\ar[rr,shiftarr={yshift=-5mm},"\pi_2"']
\ker a \cup \ker b
\ar[r,shift left = 1,"{\pi_1}"]
\ar[r,shift left = -1,"{\pi_2}"']
& Y
\ar[r,"f"]
\ar[dr,->>,"a"']
& Y'
\\
&&& A
\ar[u,dashed,"\exists! f_A"']
\end{mytikzcd}
\quad
\begin{mytikzcd}
\ker b
\ar[r,shift left = 1,"\pi_1"]
\ar[r,shift left = -1,"\pi_2"']
& Y
\ar[r,"f"]
\ar[dr,->>,"b"']
& Y'
\\
&& B
\ar[u,dashed,"\exists! f_B"']
\end{mytikzcd}
\]

Since $f_B \cdot b = f = f_A \cdot a$,  $(f_A,f_B)$ is a competing
cocone for the above pushout. This induces a cocone morphism $m\colon (P,p_A,p_B)\to
(Y,f_A,f_B)$, and we have

\begin{equation}\label{eq:ypp-y}
m\cdot p = m\cdot p_A\cdot a = f_A\cdot a = f.
\end{equation}

We are ready to show that $\ker a\cup \ker b$ is a kernel of $p$. By the
definition of $p$, the projections of $\ker a \cup\ker b$ are made equal by
$p$. For the universal property, let $d_1\colon D'\to D$, $d_2\colon D'\to
D$ such that $p\cdot d_1 = p\cdot d_2$. Then we have

\[
f\cdot d_1 \stackrel{\text{\eqref{eq:ypp-y}}}{=} m\cdot p \cdot d_1 =
m\cdot p \cdot d_2 \stackrel{\text{\eqref{eq:ypp-y}}}{=} f\cdot d_2.
\]

This means that $d_1,d_2\colon D'\rightrightarrows D$ is a competing cone
w.r.t. the kernel of $f$.
We thus obtain a unique cone morphism $u\colon D'\to \ker a \cup \ker b$ as

(2) $\Rightarrow$ (3) Take $x,y,z \in Y$ with $a(x)=a(y)$ and
$b(y) = b(z)$. Then $a(x)$ and $b(z)$ are identified in the
pushout $P$:

\[
p(x) = p_A \cdot a(x) = p_A \cdot a(y) = p_B\cdot b(y) = p_B
\cdot b(z) = p(z).
\]

This shows that $(x,z)$ lies in $\ker a\cup \ker b$, hence we have
that $a(x) = a(z)$ or $b(x) = b(z)$.

(3) $\Rightarrow$ (4) For a given $y\in Y$, there is nothing to show
in the case where $[y]_a \subseteq [y]_b$. Otherwise if
$[y]_a \not\subseteq [y]_b$, then there is some $x\in [y]_a$ that does
not lie in $[y]_b$, i.e. such that $a(x) = a(y)$ and $b(x) \neq
b(y)$. Now let $z \in [y]_b$, i.e. $b(y) = b(z)$. Then, by assumption,
$a(x) = a(y) = a(z)$ or $b(x) = b(y) = b(z)$. Since the latter does
not hold, we have $a(y) = a(z)$, i.e. $z\in [y]_a$.

All $\op{select}$ routines in <ref> respect compound blocks.
To see this, let $k = \op{select}\big(
\overset{z}{\twoheadrightarrow}\!Z
\big)

* For $S\in Y$ and $[S]_z\subseteq Y$, $k :=
\chi_{\{S\}}^{[S]_z}\colon Y \to 3$ respects
compound blocks using
Lemma <ref><ref>. Indeed,
one proceeds by case distinction on $B \in Y$:

* If $B = S$, then $[B]_k = \{S\} \subseteq [S]_z = [B]_z$.

* If $B \in [S]_z$ and $B \neq S$, then $k(B) = 1$ so that

\[
[B]_k = [S]_z \setminus \{S\} \subseteq [S]_z = [B]_z.
\]

* Finally, if $B \in Y \setminus [S]_z$, then we have
$z(B) \neq z(S)$ and therefore
$[B]_z \subseteq Y \setminus [S]_z = [B]_k$, where the latter
equation follows from $k(B) = 0$.

For $B \
\begin{itemize}
\item For $p \in Y\setminus C$, $z(p) \neq z(S)$ and so $[p]_z
\subseteq Y\setminus C = [p]_k$.

\item For $p \in C$, $z(p) = z(S)$ and so $[p]_k \subseteq C =
\end{itemize}
}% end takeout

\item The \op{select} routine returning the identity $𝕀_Y$ respects compound
blocks, because for any morphism $zY→Z$, $𝕀_Y ∪z =
z$ is a kernel.

\item The constant $k=!$ respects compound blocks, because for all
$B∈Y$: $[B]_z ⊆Y = [B]_!$.
\qedhere
\end{enumerate}
\end{example}
\noindent For every pair $aY→A$, $bY→B$ of maps,
the kernel of $a,bY→A×B$ is the intersection
$a∩b$. If the union $a ∪b$ is an
equivalence relation, then every block in the partition
$Y/a,b$ is either is an equivalence class from $Y/a$
or from $X/b$. That this happens can be visually illustrated as
follows (see \autoref{subfig:trans}): Every equivalence class of
$a∩b$ already appears in $a$ or in $b$ (or
both), i.e.~for all $x∈Y$, we have $[x]_a = [x]_a,b$ or
$[x]_b = [x]_a,b$. However for \autoref{subfig:nontrans},
${y_1,y_2,y_3} = [y_3]_b≠[y_3]_a,b ≠[y_3]_a =
In the following we prove formally that whenever $a∪b$
is an equivalence relation, then every equivalence class of
$a,b$ comes from one of $a$ (i.e.~is in the set $A'$)
or of $b$ (i.e.~is in the set $B'$).
\begin{lemma}
\label{ABpartition}
Let $a\colon Y\to A$,  $b\colon Y\to B$ such that
$\ker a\cup \ker b$ is a kernel. Then there exist sets $A'$, $B'$,
and maps $m$, $q$, $f_A$, and $f_B$ such that the following diagrams commute:
\[
\begin{mytikzcd}
\arrow[shiftarr={yshift=6mm}]{rr}{\fpair{a,b}}
\arrow{r}{q}
& A'+B'
\arrow{r}{m}
& A\times B
\end{mytikzcd}
\quad
\begin{mytikzcd}
A' + \bar A'
\arrow[equals]{d}
& A' + B'
\arrow{d}{m}
\arrow{l}[swap]{A'+f_A}
\arrow{r}{f_B+B'}
& \bar B' + B'
\arrow[equals]{d}
\\
& A\times B
\arrow{l}[swap]{\pi_1}
\arrow{r}{\pi_2}
& B
\end{mytikzcd}
\]
\end{lemma}
\begin{proof}
Define the sets
\begin{align*}
Y_A &= \{ x \in Y\mid [x]_a\subseteq [x]_b \},
Y_B &= \{ x \in Y\mid [x]_a\supsetneqq [x]_b \},
\\
A' &= \{a(x)\mid x \in Y_A\},
B' &= \{b(x)\mid x \in Y_B\}.
\end{align*}
By \autoref{compoundBlockEquivalences}, $Y = Y_A + Y_B$. Next define
$q = a' + b'\colon Y \cong Y_A+Y_B \to A' + B'$, where~$a'$ and~$b'$
are the obvious restrictions of $a$ and $b$, respectively. Now
put $\bar A' := A\setminus A'$, $\bar B' := B\setminus B'$, and
define $f_A\colon B'\to \bar A'$
and $f_B\colon A'\to \bar B'$ by
\[
f_A (b(x)) = a(x)
\qquad
f_B (a(x)) = b(x).
\]
These functions are well-defined by the definition of $Y_A$ and
$Y_B$. Moreover, the
codomain of $f_A$ restricts to~$\bar A'$, because $a(x) \in A'$
implies that $[x]_a \subseteq [x]_b$, contradicting $x\in Y_B$.
Analogously, the codomain of~$f_B$ restricts to $\bar B'$. Let $m$
be the unique map such that the right-hand diagram above commutes,
i.e.~$m$ is induced by the universal property of the product $A
\times B$. Since  $(\id_{A'}+f_A)\cdot q = a$ and $(f_B +
\id_{B'})\cdot q = b$, we see that the left-hand diagram above
\end{proof}
\noindent This factorization is the main ingredient making~$H$
essentially commute with $-,-$:
\begin{proposition} \label{propZippable}
Let $a\colon Y\to A$, $b\colon Y\to B$
such that $\ker a\cup \ker b$ is a kernel, and let
$H\colon \Set \to \Set$ be a zippable functor. Then we have
\begin{equation}
\ker \fpair{Ha,Hb} = \ker H\fpair{a,b}.
% \label{eqKerFpair}
\end{equation}
\end{proposition}
\begin{proof}
Using the additional data provided by \autoref{ABpartition}, we note that
the following diagram commutes:
\[
\begin{mytikzcd}
\arrow{d}[swap]{Hq}
\arrow{rr}{H\fpair{a,b}}
&[26mm] & H(A\times B)
\arrow{d}{\fpair{H\pi_1,H\pi_2}}
\\
\arrow[>->]{r}[swap]{\fpair{H (A'+f_A), H(f_B+B')}}
\arrow[>->]{urr}[sloped,above]{Hm}
& H(A'+\bar A')
\times H(\bar B'+ B')
\arrow[equals]{r}
& HA \times HB
\end{mytikzcd}
\]
By \autoref{zippableExtended}, the composition at the bottom is a
mono, because $H$ is zippable. Hence, $Hm$ is a mono as well.
We conclude
\[
\ker \fpair{Ha, Hb} =
\ker \big(\fpair{H\pi_1,H\pi_2}
\cdot H\fpair{a,b}\big)%\,
% \overset{\text{Rem.~\ref{rem:kernel}(\ref{i:mono})}}{=}
\ker (H q)
% \overset{\text{Rem.~\ref{rem:kernel}(\ref{i:mono})}}{=}
\ker H\fpair{a,b},
\]
using \autoref{rem:kernel}\ref{i:mono} in the last two equalities.
\end{proof}
\begin{remark}
Note that \autoref{propZippable} holds more generally for every
functor $H\colon \Set \to \D$, where $\D$ is a finitely
complete category.
\end{remark}
\noindent For a $select$ routine respecting compound blocks, we
can now apply \autoref{propZippable} to prove the equivalence of
\eqref{kernelOptimization} and Step~\ref{step:P} of \autoref{catPT}:
\begin{theorem}\label{optimizationCorrectness}
If $H\colon \Set\to\Set$ is zippable and $\op{select}$ respects
compound blocks, then the optimization \eqref{kernelOptimization} is
\end{theorem}
\begin{proof}
Correctness of \eqref{kernelOptimization} means that
\[
P_{i+1} = P_{i+1}' = \ker(H\fpair{\bar q_i,q_{i+1}}\cdot \xi) = P_i \cap \ker (Hq_{i+1}\cdot \xi).
\]
Indeed, suppose that $H$ is zippable, and let $k =
\op{select}(\kappa_{P_i}, f_i)$, where $f_i\colon
X/P_i\twoheadrightarrow X/Q_i$ witnesses that $P_i$ is finer than
$Q_i$ (see \autoref{catPT}). Then we have
\begin{equation}\label{eq:aux}
q_{i+1} = k \cdot \kappa_{P_i}
\qquad
\text{and}
\qquad
\bar q_i = m \cdot \kappa_{Q_i} = m \cdot f_i \cdot \kappa_{P_i},
\end{equation}
where $m$ is obtained by the image factorization of $\bar q_i$. By
\autoref{rem:kernel}\ref{i:mono} we have $\ker f_i = \ker (m \cdot
f_i)$. Since $\op{select}$ respects compound blocks we know that
$\ker f_i \cup \ker k$ is a kernel, thus so is $\ker(m \cdot f_i)
\cup \ker k$. By \autoref{propZippable}, we obtain
\[
\ker \fpair{H(m \cdot f_i), Hk} = \ker H \fpair{m \cdot f_i, k},
\]
which, using \autoref{rem:kernel}\ref{i:squares}, implies
\begin{equation}\label{eq:aux2}
\ker (\fpair{H(m \cdot f_i), Hk} \cdot H\kappa_{P_i} \cdot \xi)
\ker (H\fpair{m \cdot f_i, k} \cdot H\kappa_{P_i} \cdot \xi).
\end{equation}
Thus we obtain the desired result:
\begin{align*}
P_i \cap \ker(Hq_{i+1} \cdot \xi)
&= \ker\big(\fpair{H\bar q_i \cdot \xi, Hq_{i+1} \cdot \xi}\big) &
\text{def.~of $P_i$}
\\
&= \ker\big(\fpair{H(m \cdot f_i), Hk} \cdot H\kappa_{P_i} \cdot
\xi\big)
& \text{by~\eqref{eq:aux}}
\\
&= \ker (H\fpair{m \cdot f_i, k} \cdot H\kappa_{P_i} \cdot \xi)
& \text{by~\eqref{eq:aux2}}
\\
&= \ker\big(H \fpair{\bar q_i, q_{i+1}} \cdot \xi\big)
& \text{by~\eqref{eq:aux}}
\\
&= \ker\big(H\bar q_{i+1} \cdot \xi\big)
& \text{def.~of $\bar q_{i+1}$}
\\
&= P_{i+1} & \text{def.~of $P_{i+1}$}.
\tag*{\qedhere}
\end{align*}
\takeout{% taken out: I think text explanation of the argument is better.
\[
\begin{array}[b]{cl}
&\op{select}\text{ respects compound blocks}
\\
\overset{\text{Def.}}{\Leftrightarrow} &
\text{$\ker f_i\cup \ker k$ is a kernel}
\\
\overset{\ref{propZippable}}{\Rightarrow}
& \ker\fpair{Hf_i, Hk} = \ker H\fpair{f_i, k_{i+1}}
\\
\overset{\text{\ref{rem:kernel}\ref{i:squares}}}{\Rightarrow}
\ker(\fpair{Hf_i, Hk_{i+1}}\cdot H\kappa_{P_i}\cdot\xi) = \ker (H\fpair{f_i,
k_{i+1}}\cdot H\kappa_{P_i}\cdot\mathrlap{\xi )}
\\
\overset{\phantom{\ref{propZippable}}}{\Rightarrow}
P_i \cap \ker(Hq_{i+1}\cdot \xi)
= \ker \big(\fpair{H\bar q_i\cdot \xi, H q_{i+1}\cdot \xi}\big)
= \ker \big(H\fpair{\bar q_i, q_{i+1}} \cdot \xi\big) \\
& \phantom{P_i \cap \ker(Hq_{i+1}\cdot \xi) }= \ker \big(H\bar q_{i+1} \cdot \xi\big)
= P_{i+1}
\end{array}
\tag*{\qedhere}
\]
}% end takeout
\end{proof}
\noindent
Combining \autoref{optimizationCorrectness} and \autoref{thm:correct}
we obtain:
\begin{corollary}\label{optimizationSummary}
Suppose that $H$ is a zippable endofunctor and that
$\op{select}$ respects compound blocks and is progressing. Then \autoref{catPT} with
optimization~\eqref{kernelOptimization} terminates and computes the
simple quotient of a given finite $H$-coalgebra.
\end{corollary}
% \begin{proposition}
%   \label{C:sorted}
%     For an $\Sorts$-indexed family of zippable \Set-functors $H_s$ and a permutation
%     $\pi\colon \Sorts\to \Sorts$, define a functor on $\Set^{\Sorts}$ by $(H^\pi X)_s =
%     H_{s} X_{\pi(s)}$. Then for any span $a\colon D\to A$, $b\colon D\to B$,
%     where $\ker a\cup \ker b$ is a kernel, we have
%     \(
%         \ker \fpair{H^\pi a,H^\pi b} = \ker H^\pi \fpair{a,b}.
%     \)
% \end{proposition}

\begin{remark}
Note that all results in this section can be formulated and proved
in a Boolean topos $\C$ in lieu of $\Set$, e.g.~the category of
nominal sets and equivariant maps. In particular, the set-theoretic
statements in \autoref{compoundBlockEquivalences} and
\autoref{ABpartition} can be formulated in the internal language of
a Boolean topos, i.e.~the ordinary set theory ZF (with bounded
quantifiers only) without the axiom of choice, but with the law of
excluded middle. A detailed definition and discussion of this
language can be found, e.g.\ in Mac Lane and
\end{remark}

\section{Refinement Interfaces}
\label{sec:interface}
\tikzsetfigurename{partref-efficient-} In \autoref{catPT}, we left
unspecified how the kernels and partitions can be computed
efficiently. In this section we introduce the notion of a
\emph{refinement interface} for the given type functor. This interface
is aimed at efficient computation of the partition $X/P$ in
\autoref{catPT}, both in the initialization and in the
\emph{refinement step}, i.e.~in the optimization
\eqref{kernelOptimization} of Step~\ref{step:P} in \autoref{catPT}. In
\autoref{sec:efficient} we will assume that the type functor $H$ comes
equipped with a refinement interface which is used as a parameter for
a generic initialization procedure and an implementation
of~\eqref{kernelOptimization} such that partition refinement on a
coalgebra $ξX→HX$ with $n= |X|$ states and $m$ edges runs
in $((m+n)·logn)$. In order to phrase and actually achieve
this complexity bound, we need a notion of edges in coalgebras. This
notion will also provide a representation of coalgebras, for purposes
of using them as inputs to the partition refinement algorithm:
\begin{definition}\label{D:enc}
An \emph{encoding} of a functor $H$ consists of a set $A$ of
\emph{labels} and a family of maps
$\flat\colon HX\to \Bag(A\times X)$, one for every set~$X$. The
\emph{encoding} of an $H$-coalgebra $\xi\colon X\to HX$ is given by
the map
$\fpair{H!,\flat}\cdot \xi\colon X\to H1\times \Bag(A\times X)$ and we
say that the coalgebra has $n = |X|$ states and
$m = \sum_{x\in X}|\flat(\xi(x))|$ edges.
\end{definition}
\noindent The purpose of these functions is to enable a representation
of an input coalgebra $ξX→HX$ as a labelled graph. In
concrete examples, an encoding expresses how one intuitively
visualizes coalgebras (see e.g.~\autoref{fig:exPartRef},
\autoref{exWrongRunForPP}, and \autoref{figSplitStep}). The reader
should note here that standard partition refinement for graphs on the
encoding does \emph{not} correctly minimize the input coalgebra, that
is, an encoding does by no means provide a reduction of the
minimization problem from coalgebras to graphs
(\autoref{fig:exPartRef} illustrates how Markov chain lumping and
bisimilarity in transition systems lead to different
partitions). Technically speaking, behavioural equivalence in
$H$-coalgebras is not the same as behavioural equivalence in
$H1×(A×(-))$-coalgebras. Moreover, it is not even
assumed that the map~$♭:HX→(A×X)$ in an encoding is
natural in~$X$.
\begin{example} \label{exFunctorEncoding}
\begin{enumerate}
\item For $H=\Potf$, the labels are a singleton set $A=1$ and we define
$\flat\colon \Potf X\to \Bag(1\times X)\cong \Bag(X)$ to be the obvious
inclusion $\flat(t)(x) = 1$ if $x\in t$ and $\flat(t)(x) = 0$ if $x\not\in t$.
\item For $HX=\R^{(X)}$, the labels are non-zero real numbers $A= \R_{\neq 0}$, and $\flat\colon
\R^{(X)} \to \Bag(\R_{\neq 0}\times X)$ is defined as $\flat(t)(r,x) = 1$ if $t(x) =
r \neq 0$ and $\flat(t)(r,x) = 0$ if $t(x)\neq r$ or $t(x) = 0$. An example
of this encoding is visualized in \autoref{fig:exPartRef:Markov}.
\item For a polynomial functor $H_\Sigma$ (see
\autoref{ex:coalg}\ref{i:poly}), we have an encoding where the
label set $A= \N$ describes the ordering of the components:
$\flat\colon H_\Sigma X\to \Bag(\N\times X)$ is defined by
$\flat(\sigma(x_1,\ldots,x_n)) = \{(1,x_1),\ldots,(n,x_n)\}$ for
an $n$-ary symbol $\sigma \in \Sigma$. Note that the set $H_\Sigma1$ may
be identified with the signature $\Sigma$ so
$H!\cdot \xi$ assigns to each state $x$ of a $H_\Sigma$-coalgebra its
output symbol, and the bag $\flat\cdot \xi(x)$ contains
the successor states of $x$ together with their corresponding input $i \in \{1,
\ldots, n \}$.
\end{enumerate}
\end{example}
\noindent Having a coalgebra encoded in terms of labelled edges, the following
computational task is solved in the refinement step: Given a coalgebra $ξX→HX$ as its encoding $X→H1×(A×X)$ and partitions
$X/P$ and $X/Q$ such that $P$ is stable w.r.t.~$Q$ (see \autoref{D:stable}), how
does splitting a block $C∈X/Q$ into $S⊆C$ and $C∖S$ affect
the partition $X/P$? The explicit case for $H = $ is visualized in
\autoref{fig:RefineStep} and is computed as follows:

\begin{example}\label{exPaigeTarjanSplit}
For the finite powerset functor, fix a coalgebra $\xi\colon X \to \Potf X$. We say
that there is an edge from $x$ to a subset $S \subseteq X$ if $x$ has a
successor node in $S$.

In the Paige-Tarjan algorithm~[47], when a block
$C\in X/Q$ is split into smaller blocks $S\subseteq C$ and
$C\setminus S$, every block of $B\in X/P$ is split into (at most)
three blocks as visualized in \autoref{fig:RefineStep}:
\begin{enumerate}
\item States $x\in B$ with edges to $S$ but not to $C\setminus S$.
\item States $x\in B$ with edges to both $S$ and $C\setminus S$.
\item States $x\in B$ with edges to $C\setminus S$ but not to $S$.
\end{enumerate}
It is one of the key points in the analysis of the overall time
complexity that this split is performed in linear time in the number
of ingoing edges into~$S$, regardless of the sizes of $C\setminus S$
and~$B$. Roughly, this works as follows. All edges from a state
$x\in X$ to the same block $C\in X/Q$ share an integer counter
variable that stores how many such edges exist. Sharing a variable
means that every edge is equipped with a pointer to a memory cell
holding the actual counter. For example, in
\autoref{fig:RefineStep}, $x_2\to y_2$, $x_2\to y_4$, and
$x_2\to y_3$ share a variable with the value 3. When splitting $C$
into $S$ and $C\setminus S$, we count the edges ending in $S$ and
then compare the result with the counter variable of each of those
edges, which allows us to implement the above three-way split by
iterating over the source nodes $x \in B$ with edges to~$S$:
\begin{figure}
\begin{tikzpicture}
\begin{scope}[
every node/.append style={
inner sep=0pt,
outer sep=2pt,
minimum width=1pt,
minimum height=4pt,
\begin{scope}[yshift=1.5cm]
\node (x1) at (-1.2,0) {$x_1$};
\node (x2) at (0,0) {$x_2$};
\node (x3) at (1.2,0) {$x_3$};
\end{scope}
\node (y1) at (-1.6,0) {$y_1$};
\node (y2) at (-0.5,0) {$y_2$};
\node (y3) at (0.5,0) {$y_3$};
\node (y4) at (1.2,0) {$y_4$};
\end{scope}
\node[anchor=west,xshift=2mm] (y5) at (y4.east) {$\ldots$};
\draw (y1) edge[draw=none] node {$\ldots$} (y2);
\begin{scope}[
every node/.append style={
inner sep=2pt,
every label/.append style={
outer sep=1pt,
inner sep=1pt,
minimum height=2mm,
\node[fit=(x1) (x2) (x3)] (x123){};
\node[fit=(y1) (y5)] (C) {};
\node[every label] at ([xshift=-1mm]x123.north east) {\normalsize $B$};
\node[every label] at ([xshift=-1mm]C.north east) {\normalsize $C$};
% blocks that are displayed half
\begin{scope}[every node/.append style={minimum width=10mm}, % width of a block
\newcommand{\nextblockdistance}{8mm} % distance to the next block
\foreach \name/\nodesource/\anchor/\direction in
Qwest/C/west/-} {
\begin{scope}
\clip ([yshift=1mm]\nodesource.north \anchor)
rectangle ([yshift=-1mm,xshift=\direction\nextblockdistance]
\nodesource.south \anchor);
\node at ([xshift=\direction\nextblockdistance]\nodesource.\anchor) (\name) {};
\end{scope}
\end{scope}
\end{scope}
\draw[thick, decoration={brace,mirror},decorate]
([yshift=-2mm]y1.south west) -- node[anchor=north,yshift=-2pt]{$S$} ([yshift=-2mm]y2.south east) ;
\draw[thick, decoration={brace,mirror},decorate]
([yshift=-2mm]y3.south west) -- node[anchor=north,yshift=-2pt]{$C\setminus S$} ([yshift=-2mm]y3.south west -| y5.south east) ;
\foreach \name in {Peast,Pwest,Qeast,Qwest} {
\node[draw=none,minimum width=1pt,minimum height=1pt,text height=1pt,inner xsep=1pt]
at (\name.center) {$\ldots$};
\begin{scope}[text depth=2pt]
\node[outer sep=5mm,anchor=east] at (Pwest.center -| Qwest.center) (P) {$X/P:$};
\node[outer sep=5mm,anchor=east] at (Qwest.center) (Q) {$X/Q:$};
% the x-cooridnate of the map X -> PY
\coordinate (mapXCoordinate) at ([xshift=10mm]Qeast.center);
\node[outer sep=1pt,anchor=center] at (Peast.center -| mapXCoordinate) (X) {$X$};
\node[outer sep=1pt,anchor=center] at (Qeast.center -| mapXCoordinate) (PY) {$\Potf X$};
\end{scope}
\draw[commutative diagrams/.cd, every arrow, every label] (X) edge node {$\xi$} (PY);
\begin{scope}[
bend angle=10,
line width=4pt,
preaction={draw,-,line width=1mm,white},
every node/.append style={
inner sep=1pt,
\draw[edge,bend right] (x1) to (y1);
\draw[edge,bend left] (x1) to (y2);
\draw[edge,bend right] (x2) to (y2);
\draw[edge,bend left] (x2) to (y3);
\draw[edge,bend left] (x2) to (y4);
\draw[edge,bend right] (x3) to (y3);
\draw[edge] (x3) to (y4);
\draw[edge,bend left] (x3) to (y5);
\end{scope}
\begin{scope}[% scissor lines
inner sep=0pt,
line width=1mm,
\foreach \leftnode/\rightnode/\northlen/\southlen in
{x1/x2/4mm/4mm,x2/x3/4mm/4mm,y2/y3/4mm/4mm} {
\coordinate (northend) at ($ (\leftnode) !.5! (\rightnode) + (0,\northlen)$);
\coordinate (southend) at ($ (\leftnode) !.5! (\rightnode) - (0,\southlen)$);
\node[anchor=east,rotate=-90,scissors] at (northend) {\scissors};
\draw[gapstyle] (northend) -- (southend);
\draw[linestyle] (northend) -- (southend);
\end{scope}
\end{tikzpicture}
%%% Local Variables:
%%% TeX-PDF-mode:t
%%% ispell-local-dictionary: "british-ize"
%%% TeX-master: "coalgpartref-lmcs"
%%% End:

\caption{The refinement step for $\xi\colon X \to \Potf X$, for $S\subseteq
C\in X/Q$.}
\label{fig:RefineStep}
\end{figure}
\begin{enumerate}
\item If the counters match, then all edges from $x$ to $C$ go indeed to $S$,
and we move all these~$x$ to a new block.
\item If the values mismatch, then some edges from $x$ to $C$ go to
$S$ and some to $C\setminus S$. Hence, we move all these $x$ to a
new block and then update the counter variables. To this end, we
count the number~$n$ of edges from $x$ to $S$. We re-use the
existing counter variable for edges $x\to C$ and make it the
variable for $x\to C\setminus S$ by decrementing it by $n$. For
example, in \autoref{fig:RefineStep} the counter for the edge
$x_2\to y_2$ is decremented from $3$ to $2$, and this counter
variable is shared with $x_2\to y_3$ and $x_2\to y_4$, so the
count for these edges is correctly decremented as well. We then
allocate a new counter with value $n$ and change the pointer of
all edges $x\to S$ to this new counter. In the example in
\autoref{fig:RefineStep}, the pointer of the edge $x_2\to y_2$ now
points to this new counter, which holds the value $1$.

\item All the remaining $x \in B$ have no edge to $S$, and
nothing needs to be done for them, because the counters for edges
from $x$ need not change.
\end{enumerate}
We thus have refined the partition $X/P$ such that it becomes
(again) stable w.r.t.~the new partition $X/Q$ where $C$ is split
into~$S$ and $C\setminus S$.
\end{example}

\noindent Note that in \autoref{exPaigeTarjanSplit}, the block $B$ is
split into smaller blocks in such a way that elements $x,x'$ end up in
the same block iff $χ_S^C(ξ(x)) = χ_S^C(ξ(x))$.
This split is done efficiently by maintaining an integer variable for
counting edges.  The present section generalizes this procedure from
$$ to a \Set-functor~$H$ that implements a so-called
\emph{refinement interface}, in which the integer counter generalizes
to a set $W$ \textqt{weights} and the comparison of counters
generalizes to an $update$ function:

\begin{definition}\label{refinementInterface}
A \emph{refinement interface} for a $\Set$-functor~$H$ equipped with
a functor encoding is formed by a set $W$ of \emph{weights} and
\begin{align*}
\begin{array}{l@{\qquad}c@{\quad}l}
\op{init}\colon H1×\Bagf A\to W,&\op{update}\colon \Bagf A × W \to W× H3× W
\end{array}
\end{align*}
such that there exists a family of \emph{weight maps} $w\colon \Potf X \to (HX \to W)$
such that for all
$S\subseteq C\subseteq X$, the diagrams
\vspace{-2mm}
\begin{equation}
\label{eqSplitterLabels}
\hspace{-4mm}
\begin{mytikzcd}
H1 × \Bagf A
\arrow{r}{\op{init}}
& W
\\
\arrow{u}[left, pos=0.4]{
\fpair{
\op{fil}_X\cdot \flat}}
\arrow{ur}[swap]{w(X)}
\end{mytikzcd}
\hspace{1mm}
\begin{mytikzcd}[column sep=1.4cm]
\Bagf A × W
\arrow{r}{\op{update}}
& W × H3 × W
\\
\arrow[
]{ur}[swap]{\fpair{w(S),H\chi_S^C, w(C\setminus S)}}
\arrow{u}[left]{\fpair{\op{fil}_S\cdot \flat,w(C)}}
\end{mytikzcd}
\hspace{-3mm}
\end{equation}
commute, where \( \op{fil}_S\colon \Bagf(A×X) \to \Bagf(A)\)
is the filter function
\(\op{fil}_S (f)(a) = \textstyle\sum_{y \in S} f(a,y)\)
for $S\subseteq X$ (e.g.~$\op{fil}_X = \Bagf \pi_1$).
\end{definition}
\begin{remark} \label{R:filS}
\begin{enumerate}
\item Note that for a coalgebra $\xi\colon X \to HX$, $\op{fil}_S \cdot
\flat \cdot \xi(x)$ is the bag of labels of all edges from $x$ to $S
\subseteq X$ in the encoding of $\xi$.
\item Observe that $\op{fil}_S$ is natural in $A$, i.e.~for every
map $h\colon A \to A'$ the following square commutes:
\[
\begin{tikzcd}
\Bagf(A \times X)
\arrow{r}{\op{fil}_S}
\arrow{d}[swap]{\Bagf(h \times X)}
\Bagf A \arrow{d}{\Bagf h}
\\
\Bagf(A' \times X)
\arrow{r}{\op{fil}_S}
\Bagf A'.
\end{tikzcd}
\]
Indeed, we have for all $f\in \Bagf(A\times X)$
\begin{align*}
\op{fil}_S \cdot \Bagf(h \times X) (f)
&= \op{fil}_S \big( (a',x) \mapsto \sum_{(h \times X)(a,y) =
(a',x)} f(a,y) \big)
\\
&= \op{fil}_S \big((a',x) \mapsto \sum_{h(a) =
a'} f(a,x) \big)
\\
&= a'\mapsto \sum_{y\in S} \sum_{h(a) = a'} f(a,y)
\\
&= a'\mapsto \sum_{h(a) = a'} \sum_{y\in S} f(a,y)
\\
&= \Bagf h \big( a \mapsto \sum_{y \in S} f(a,y)\big)
\\
&= \Bagf h \cdot \op{fil}_S(f).
\end{align*}
\end{enumerate}
\end{remark}
\noindent
Informally, for a given coalgebra $ξX→HX$, the above
axioms for \op{init} and \op{update} can be understood as a kind of
contract that their implementation for a given functor needs to
fulfil: \op{init} receives in its first argument the information which
states of $X$ are (non-)terminating, in its second argument the bag of
labels of all outgoing edges of a state $x ∈X$ in the graph
representation of $ξ$, and it returns the total weight of those
edges. The operation \op{update} receives a pair consisting of the bag
of labels of all edges from some state $x ∈X$ into the set
$S ⊆X$ and the weight of all edges from $x$ to
$C⊆X$, and from only this information (in particular
$update$ does not know $S$ and $C$ explicitly) it computes the
triple consisting of the weight of edges from $x$ to $S$, the result
of $Hχ_S^C ·ξ(x)$ and the weight of edges from $x$ to
$C∖S$ (in \autoref{exPaigeTarjanSplit}, the number of edges
from $x$ to $S$, the value for the three way split, and the number of
edges from $x$ to $C∖S$). The significance of the set $H3$ is that when using a
set $S⊆C⊆X$ as a splitter, we want to split every
block $B$ in such a way that it becomes \emph{compatible} with $S$ and
$C∖S$, i.e.~we group the elements $x∈B$ by the value of
$Hχ_S^C·ξ(x) ∈H3$. The set~$W$ depends on the
functor. But in most cases $W=H2$ and
$w(C) = H χ_CHX →H2$ are sufficient.

In implementations, the refinement interface does not need to
provide~$w$ explicitly, because the algorithm will compute the values
of $w$ incrementally using \eqref{eqSplitterLabels}, and $♭$ need
not be implemented because we assume the input coalgebra to be already
\emph{encoded} via $♭$.
\begin{example} \label{examplePowerset} The refinement interface for
the powerset functor $H=\Potf$ needs to count the edges into blocks
$C$, so that we know in the refinement with $S\subseteq C$ whether
there are edges to $C\setminus S$, as in
\autoref{exPaigeTarjanSplit}. For a natural number $n$, we define
the auxiliary function
\[
(-) \geZero 0\colon \N \to 2\qquad\text{by }(n\geZero 0) =
\min(n,1) =
\begin{cases}
1 &  \text{if $n > 0$} \\
0 &  \text{else.}
\end{cases}
\]
For the refinement interface we use
the following weights and labels:
\[
A = 1,
\quad
W = 2\times \N,
\quad
\text{$w\colon \Potf X \to (\Potf X \to 2\times \N)$ with
$w(C)(t) = (|t\setminus C| \geZero 0, |t\cap C|)$.}
\]
For a map $\xi\colon X\to \Potf X$, a state $x\in X$, and a block
$C\subseteq X$, the weight $w(C)(\xi(x))$ is a tuple whose first
component tells us whether there is any edge from $x$ to
$X\setminus C$ and whose second component is the number of edges from
$x$ to $C$. Since we have a singleton label alphabet $A=1$, every
bag of labels is just a natural number, because
$\Bagf A = \Bagf 1 \cong \N$. The functions
\[
\op{init}\colon \Potf 1\times \N \to 2\times \N
\qquad\text{and}\qquad
\op{update}\colon \N \times (2\times \N) \to (2\times \N)\times \Potf 3 \times (2\times \N)
\]
in the refinement interface for $\Potf$ are implemented as follows:
\[
\op{init}(z,n) = (0,n) \qquad\text{and}\qquad
\begin{array}[t]{r@{\,}l@{}l}
\op{update}(n_S,(r,n_C)) &=
\big(&(r\vee (n_{C\setminus S}\geZero 0), n_S), \\[5pt]
&& (r, n_{C\setminus S}\geZero 0, n_S\geZero 0), \\[5pt]
&& (r\vee (n_{S}\geZero 0), n_{C\setminus S})\big),
\end{array}
\]
where $n_{C\setminus S} := \max(n_C - n_S, 0)$,
$\vee\colon 2\times 2\to 2$ is disjunction, and the middle return
value in $\Potf 3$ is written as a bit vector of length three. The
axioms in~\eqref{eqSplitterLabels} ensure that
$n_S, n_C, n_{C\setminus S}$ can be understood as the numbers of
edges to $S$, $C$, and $C\setminus S$, respectively.

For the verification of \eqref{eqSplitterLabels}, note that for all $S\subseteq X$,
the map $\op{fil}_S\cdot \flat\colon \Potf X\to \N$ is given by
$\op{fil}_S(\flat(t)) = |t\cap S|$. Hence, we see that for all $t\in
\Potf X$ we have
\[
\op{init}(\Potf!(t), \op{fil}_X(\flat(t)))
= (0, \op{fil}_X(\flat(t)))
= (|t\setminus X|\geZero 0, |t\cap X|)
= w(X)(t).
\]
In the verification of the axiom of \op{update}, the parameters expand as
\[
\op{update}(\op{fil}_S(\flat(t)), w(C)(t))
= \op{update}(|t\cap S|, (|t\setminus C|\geZero 0, |t\cap C|))
\Rightarrow
\left\{
\begin{array}{l@{\,}l}
n_S &= |t\cap S| \\
r &= |t\setminus C|\geZero 0 \\
n_C &= |t\cap C| \\
\end{array}\right.
\]
So $n_{C\setminus S} = \max(n_C-n_S, 0)= \max(|t\cap C| - |t\cap S|, 0) =
|t\cap (C\setminus S)|$, since $S\subseteq C$. The remaining steps of the
verification are performed component-wise: for $x =
\op{update}(\op{fil}_S(\flat(t)), w(C)(t))$ we have
\begin{align*}
\qquad
\pi_1(x)
&= \big((|t\setminus C|\geZero 0) \vee (|t\cap (C\setminus S)|\geZero 0), |t\cap S|\big)
\\ &
= \big(|t\setminus S|\geZero 0, |t\cap S|\big)
= w(S)(t),
\\[5pt]
\pi_2(x) &= (|t\setminus C|\geZero 0,
|t\cap (C\setminus S)| \geZero 0,
|t\cap S|\geZero 0)
\\
&= (\bigvee_{\substack{y\in t\\ \chi_S^C(y) = 0}}\!\!1,
\bigvee_{\substack{y\in t\\ \chi_S^C(y) = 1}}\!\!1,
\bigvee_{\substack{y\in t\\ \chi_S^C(y) = 2}}\!\!1)
%= (k \in 3 \mapsto \bigvee_{\substack{y\in t\\ \mathclap{\chi_S^C(y) = k}}}1)
%\quad\in (2,\vee,0)^{(3)}
\qquad\qquad \text{as an element of $\Potf 3$}
\\ &
= \{\chi_S^C(y)\mid y\in t\}
= \Potf\chi_S^C(t),
\\[5pt]
\pi_3(x) &=
\big((|t\setminus C|\geZero 0) \vee (|t\cap S|\geZero 0), |t\cap (C\setminus S)|\big)
\\ &
= \big(|t\setminus (C\setminus S)|\geZero 0, |t\cap (C\setminus S)|\big)
= w(C\!\setminus\! S)(t).
\end{align*}
%  Hence, \eqref{eqSplitterLabels} is fulfilled.
\end{example}
\begin{example} \label{exampleH2} In the following examples, we always
\[
W = H2
\qquad\text{and}\qquad
w(C) = H\chi_C\colon HX\to H2.
\]
We also use the helper function
\[
\op{val} := \fpair{H(=2), \id_{H3}, H(=1)}\colon H3\to H2×H3×H2,
\]
where $(=x)\colon 3\to 2$ is the equality check for $x\in \{1,2\}$, and in
each case define
\[
\op{update} = (
\Bagf A \times H2 \xrightarrow{\op{up}} H3
\xrightarrow{\op{val}} H2 \times H3 \times H2),
\]
for a function $\op{up}\colon \Bagf A× H2\to H3$ that is defined
individually for every functor.

For the verification of \eqref{eqSplitterLabels} note that, in
general, for $S\subseteq C\subseteq X$, we have
\[
\op{val}\cdot H\chi_S^C = \fpair{H\chi_{S}, H\chi_S^C,
H\chi_{C\setminus S}}.
\]
Hence, to verify the axiom for
$\op{update} = \op{val}\cdot \op{up}$ it suffices to verify that
\begin{equation}\label{eq:toveri}
\op{up}\cdot\fpair{\op{fil}_S\cdot \flat, H\chi_C } = H\chi_S^C;
\end{equation}
in fact, using $w(C) = H \chi_C$ we have:
\begin{align*}
\op{update}\cdot \fpair{\op{fil}_S \cdot\flat, w(C)}
&= \op{val} \cdot \op{up} \cdot \fpair{\op{fil}_S \cdot\flat, H\chi_C}
\\
&= \op{val} \cdot H \chi^C_S \\
&= \fpair{H\chi_S, H\chi^C_S, H\chi_{C\setminus S}} \\
&= \fpair{w(S), H\chi^C_S, w(C\setminus S)}.
\end{align*}

\begin{enumerate}%[wide]
\item\label{exampleH2.1} For the monoid-valued functor $H= G^{(-)}\!$
over an Abelian group $(G,+,0)$, we take labels $A = G$ and define
$\flat(f) = \{ (f(y),y) \mid y\in X, f(y) \neq 0\}$ (which is
finite because $f$ is finitely supported). With $W= H2= G×G$, the
weight $w(C) = H\chi_C\colon HX\to G×G$ assigns to $f \in HX = G^{(X)}$
the pair of accumulated weights of $X\setminus C$ and $C$ under
\[
w(C)(f) = \Big(\sum_{y \in X \setminus C} f(y), \sum_{y \in C} f(y)\Big).
\]
The remaining functions are
\begin{align*}
\op{init}(h_1, e) = (0, \groupsum e)
\quad
\text{and}
\quad
\op{up}(e, (r,c)) =
(r, c - \groupsum e,  \groupsum e),
\end{align*}
where $\groupsum\colon \Bagf G \to G$ is the obvious summation map
assigning to a bag of elements of $G$ their sum in $G$.

Then for all $f\in HX = G^{(X)}$ and $S\subseteq C\subseteq X$, we have:
\begin{align*}
\op{init}(H!(f), \op{fil}_X\cdot\flat(f)) &=
\big(0, {\textstyle\sum}\Bagf\pi_1\cdot\flat(f)\big)
\\ & =
%\big(0, \sum_{\mathclap{\substack{y\in X,\\ f(y)\neq 0}}}
%f(y)\big) =
\big(0, \sum_{\mathclap{\substack{y\in X}}} f(y)\big) =
G^{(\chi_X)}(f) = w(X)(f),
\\
\op{up}(\op{fil}_S(\flat(f)), H\chi_C(f))
\op{up}\big(
\{f(y)\mid y\in S\},
\big(\sum_{\mathclap{y\in X\setminus C}} f(y),
\sum_{\mathclap{y\in C}} f(y)\big)
\big)
\\ &
= \big(\sum_{\mathclap{y\in X\setminus C}} f(y),
\sum_{\mathclap{y\in C}} f(y)- \sum_{\mathclap{y\in S}} f(y),
\sum_{\mathclap{y\in S}} f(y)
\big)
\\ &
\overset{\mathclap{S\subseteq C}}{=} ~~\big(\sum_{\mathclap{y\in X\setminus C}} f(y),
\sum_{\mathclap{y\in C\setminus S}} f(y),
\sum_{\mathclap{y\in S}} f(y)
\big)
= H\chi_S^C(f),
\end{align*}
which verifies~\eqref{eq:toveri} and therefore~\eqref{eqSplitterLabels}.

\item\label{item:R} As a special case, we obtain a refinement
interface for the functor $\R^{(-)}$, and from this we can derive one
for the distribution functor $\Dist$, a subfunctor of $\R_{\geq 0}^{(-)}$, the following
$\op{init}$ and $\op{up}$ functions:
\[
\op{init}(h_1, e) = (0,1) \in \Dist 2 \subset [0,1]^2
\qquad\text{and}\qquad
\op{up}(e, (r,c)) = (r, c - \groupsum e, \groupsum e),
\]
if the latter lies in $\Dist 3$, and $\op{up}(e,(r,c)) = (0,0,1)$ otherwise.

The axiom for $\op{init}$ clearly holds since for every
$f \in \Dist X$, we have
$\groupsum \Bag\pi_1 \cdot \flat(f) = \sum_{y \in X} f(y) =

The axiom~\eqref{eq:toveri} for $\op{up}$ is proved as in the
previous example; in fact, note that for an $f \in \Dist X$ all
components of the triple
\big(\sum_{y\in X\setminus C} f(y),
\sum_{y\in C\setminus S} f(y),
\sum_{y\in S} f(y)
\big)
are in $[0,1]$ and their sum is $\sum_{y \in X} f(y) = 1$. Thus,
this triple lies in $\Dist 3$ and is equal to $\Dist \chi^C_S(f)$.

\item Similarly, one obtains a refinement interface for $\Bagf =
\N^{(-)}$, adjusting the one for $\Z^{(-)}\!$; in fact,
$\op{init}$ remains unchanged and $\op{up}(e, (r,c)) = (r,
c-\groupsum e, \groupsum e)$ if the middle component is a natural
number and $(0,0,0)$ otherwise.

To verify~\eqref{eqSplitterLabels} for the refinement interface for
$\N^{(-)}$ we argue similarly as in point~\ref{item:R} above: If
$f$ lies in $\N^{(X)}\subseteq \Z^{(X)}$, i.e.~has only non-negative components,
then only non-negative components appear in the data returned by $\op{up}$ and
$\op{update}$, so $\op{up}$ and $\op{update}$ restrict from $\Z^{(-)}$ to
$\N^{(-)}$ as desired.

\item Given a polynomial functor $H_\Sigma$
for the signature $\Sigma$,
recall from \autoref{exFunctorEncoding} that the labels $A = \N$
records the generators contained in a shallow term together with their indices:
\[
\flat(\sigma(y_1,\ldots,y_n)) = \{ (1,y_1),\ldots,(n,y_n)\}.
\]
Then the functor interface is given by $w(C) = H\chi_C$ and
\begin{align*}
\op{init}(\sigma(0,\ldots,0), f) &= \sigma(1,\ldots,1)
\\
\op{up}(I, \sigma(b_1,\ldots,b_n))
&= \sigma(b_1 + (1\in I),\ldots,b_i + (i\in I),\ldots,b_n + (n\in I)).
\end{align*}
Here $b_i + (i\in I)$ means $b_i + 1$ if $i\in I$ and $b_i$ otherwise.

To verify~\eqref{eqSplitterLabels}, let $S \subseteq C \subseteq X$,
$t=\sigma(y_1,\ldots,y_n) \in H_\Sigma X$ with $\sigma$ of arity
$n$, let $b_i = \chi_C(y_i)$, and
$I= \{ 1 \le i \le n \mid y_i \in S\}$. Then we have:
\begin{align*}
\op{init}(H_\Sigma!(t), \Bagf\pi_1\cdot \flat(t))
&= \op{init}(\sigma(0,\ldots,0), \Bagf\pi_1(\{(1,y_1),\ldots,(n,y_n) \}))
\\ &
= \op{init}(\sigma(0,\ldots,0), \{1,\ldots,n \})
= \sigma(1,\ldots,1)
\\ &
= \sigma(\chi_X(y_1),\ldots,\chi_X(y_n))
= H_\Sigma \chi_X (t).
\\
\op{up}(\op{fil}_S\cdot \flat(t), H_\Sigma\chi_C(t)) &=
\op{up}(\op{fil}_S(\{(1,y_1),\ldots,(n,y_n)\}),
\sigma(b_1,\ldots,b_n))
\\ &
= \op{up}(I, \sigma(b_1,\ldots,b_n))
\\ &
= \sigma(b_1 + (1\in I),\ldots,b_i + (i\in I),\ldots, b_n + (n\in I))
\\ &
= \sigma(\chi_S^C(y_1),\ldots,\chi_S^C(y_i),\ldots, \chi_S^C(y_n))
\\ &
\end{align*}
In the second last step we use that:
\[
\begin{array}[b]{lcl}
y_i \in X\setminus C
&\Rightarrow& b_i + (i\in I) =
0 + 0 = 0 = \chi_S^C(y_i),
\\
y_i \in C\setminus S
&\Rightarrow& b_i + (i\in I) =
1 + 0 = 1 = \chi_S^C(y_i),
\\
y_i \in S
&\Rightarrow& b_i + (i\in I) =
1 + 1 = 2 = \chi_S^C(y_i).
\end{array}
\tag*{\qedhere}
\]
\end{enumerate}
\end{example}
\noindent
By~\autoref{P:reduction}, the interface for Abeliean-group-valued
functors can also be used for monoid-valued functors~$M^(-)$ for
cancellative monoids~$M$ (as these embed into Abelian groups). In
further work~[21], we provide a refinement interface for
monoid-valued functors~$M^(-)$ over unrestricted monoids~$M$; this
also yields a refinement interface for $$ as the monoid-valued
functor $(2,∨,0)^(-)$. However, the more general refinement
interface is less efficient than the specific interface for $$
described in \autoref{examplePowerset}; in particular it does not
yield the linear run-time complexity we seek here and require next in
\autoref{interface-linear}.

The next result shows that for every refinement interface the weight
function $w(C)$ provides at least as much information as $Hχ_C$.
\begin{proposition}\label{prop:atleast}
For every refinement interface, $H\chi_C = H (=1) \cdot \pi_2\cdot
\op{update}(\emptyset)\cdot w(C)$.
\end{proposition}

\begin{proof}
The axiom for $\op{update}$ and definition of $\op{fil}_\emptyset$ makes
the following diagram commute:
\[
\begin{mytikzcd}[sep=1.4cm,baseline=(bot.base)]
\arrow[
rounded corners,
to path={
-- ([yshift=-5mm]\tikztostart -| \tikztotarget) \tikztonodes
-- (\tikztotarget)
w(C\setminus \emptyset)}}
\arrow[
rounded corners,
to path={
-- ([yshift=-4.5mm]\tikztostart -| \tikztotarget) \tikztonodes
-- (\tikztotarget)
\arrow[
rounded corners,
to path={
-- (\tikztostart -| \tikztotarget) \tikztonodes
-- (\tikztotarget)
\arrow[shiftarr={xshift=-20mm}]{d}[left]{\fpair{\emptyset!, w(C)}}
\arrow{d}[left]{\fpair{\flat\cdot \op{fil}_\emptyset,w(C)}}
\\
\Bagf A × W
\arrow{r}{\op{update}}
& W × H3 × W
\arrow{r}{\pi_2}
& H3
\arrow{r}{H(=1)}
& H2
\end{mytikzcd}
\tag*{\qedhere}
\]
\end{proof}

\begin{assumption}\label{interface-linear}