# Coalgebraic Determinization of Alternating Automata
Report on a M1 Internship

Meven Bertrand, under the supervision of Jurriaan Rot

(September 25 2017)

###### Abstract

Coalgebra is a currently quite active field, which aims to look at generic
state-based systems (most prominently automata) from a very abstract point of
view, mainly using tools from category theory. One of its achievements is to
give a completely generic approach of determinization, unifying in an elegant
manner non-deterministic automata, probabilistic automata or non-deterministic
pushdown automata in one and the same model.

However, the case of alternating automata fails to easily fit in this model.
The aim of this internship was therefore to tackle this problem: can
alternating automata also be determinized in the coalgebraic way? Does this
give semantics that coincides with the concretely defined one?

In this report, we give a positive answer to both questions. The main element
of our construction is a distributive law, the definition of which has been
for some time an open question.

###### Contents

  1. 1 Introduction
  2. 2 Category Theory
    1. 2.1 Basic Definitions
    2. 2.2 More Advanced Constructions
  3. 3 Coalgebras And Determinization
    1. 3.1 State-Based Systems as Coalgebras
    2. 3.2 The Problem Of Determinization
    3. 3.3 Bialgebraic Semantics
    4. 3.4 Semantics Via Determinization
  4. 4 The Case Of Alternating Automata
    1. 4.1 Alternating Automata
    2. 4.2 A Monadic Structure For Alternating Automata
    3. 4.3 Induced Semantics
  5. 5 Conclusion
  6. A Proofs
    1. A.1 Preliminary Order Lemmas
    2. A.2 Monad Structure of Up and Dn
    3. A.3 Naturality Of The Distributive Law
    4. A.4 Monad Structure of Alt
  7. B Thanks

##  1 Introduction

A big part of computer science is about studying models of computation, for
various purposes. A lot of these models (automata, Turing machines, stream
systems, Mealy machines, etc.) share a common structure: they consist of a set
of states, together with some kind of transition structure. The “user” does
not have access to the states, but only to some output: the system behaves
like a black box.

Coalgebra is a field that uses tools coming from category theory to describe
systems of this kind in a generic way. Its biggest achievement is the notion
of bisimulation, a sound reasoning principle for behavioural equivalence that
exists for any of these state-based systems as soon as they are described in
the coalgebraic setting.

However, this notion of bisimulation will not be our main concern here.
Rather, we will look at another quite interesting construction:
determinization. A lot of state based systems include some kind of branching
structure: it can be choice between multiple transitions (non-deterministic
automata, non-deterministic Turing machines, and so forth), but also
probabilistic transitions (probabilistic automata), and even more exotic
models (weighted automata, alternating automata, etc.). In most of these
cases, one can construct a deterministic version of the system, by making the
state space bigger. Thanks to the coalgebraic setting, this determinization is
now understood at an abstract level, and can be performed on generic non-
deterministic systems, as surveyed in [6].

However, there are a few cases that somehow do not easily fit in this setting.
The case of alternating automata is one, and it has resisted attempts to
describe it coalgebraically for some time. In this report we give a
coalgebraic description of alternating automata in the setting of
determinization. This finally solves the aforementioned difficulty, and makes
alternating automata another example of the power of the coalgebraic theory.
Moreover, this definition gives a semantics that is similar to the concrete
one, which makes it very satisfactory.

The crucial point of this determinization is a categorical construction called
distributive law. The law itself was already known, but it was used in a
completely different setting. Thus, our work was mostly to acknowledge that
this law could be used in our setting, and construct the frame around it to
make it fit into the general picture of determinization. After this, we still
had to verify that the semantics corresponding to this construction is indeed
the usual, concrete one.

#### Literature review

The search for this distributive law has caused a lot of mistakes and
unsatisfactory trials: in [5] and [6], the problem of alternating automata is
tackled, but each time the model is less interesting than the original one;
concerning the law itself, a construction that is erroneously claimed to be a
distributive law appears in different papers, for instance [8] (corrected in
[9]), or [11]. The case of [9] is rather interesting, as they use an imperfect
law, and are still able to draw some results out of it, but this is not enough
to really solve the problem. A precise description of the errors can be found
in [7] (which is, to my knowledge, unpublished and unavailable online). The
use of our the distributive law was suggested by Luigi Santocanale. It seems
to be somewhat a folklore result, so it is hard to trace back, but it can for
example be found in [12, p. 220-221], where it is just a simple example of a
much more complex construction.

#### Outline

The report is divided in three parts: the first one (section 2) gives some
generic categorical notions, the second one (section 3) introduces the needed
notions of coalgebra, including the generic determinization procedure, and the
last one (section 4) exposes the special case of alternating automata. This
last section is the one containing the original work, the two others are
mostly there to give context.

##  2 Category Theory

In this section, we give a small overview of category theory, with the aim of
introducing the main subjects the internship was dealing with. Since we mean
it to be an overview, and not a proper course of any kind, we will not give
proofs, but just state the interesting properties, and try to give intuition
on the reason they are true. Complete definitions and proofs can be found in
[1].

###  2.1 Basic Definitions

In almost every field of mathematics, one is concerned with a certain type of
objects, and with mappings that preserve these objects: sets and functions,
vectors spaces and linear maps, groups and group homomorphisms, ordered sets
and monotone maps, topological spaces and continuous functions, and so on.
This is what category theory tries to define, on a very abstract level.

######  Definition 2.1 (Category).

A category consists of

  * •

a collection of objects ($A$, $B$, $C$ …),

  * •

a collection of arrows ($f$, $g$, $h$ …),

and the following are also given

  * •

for each arrow, two objects are given, its domain and codomain, written
respectively as $\operatorname{dom}(f)$ and $\operatorname{codom}(f)$, and we
usually write $f:A\to B$ to indicate that $\operatorname{dom}(f)=A$ and
$\operatorname{codom}(f)=B$,

  * •

given any three objects $A$, $B$ and $C$ and arrows $f:A\to B$ and $g:B\to C$,
an arrow $g\circ f:A\to C$ is given, called the composite of $f$ and $g$,

  * •

for each object, an arrow $\operatorname{id}_{A}$ is given, called the
identity of $A$,

and these must satisfy

  * •

associativity: $h\circ(g\circ f)=(h\circ g)\circ f$ whenever the composition
is defined,

  * •

unit: for any arrow $f:A\to B$, we have $\operatorname{id}_{B}\circ
f=f=f\circ\operatorname{id}_{A}$.

All the examples mentioned above are categories according to this definition.
Some much weirder constructions are also categories, but we will not present
these, as they are of little interest for this report.

####

We will mostly work in the following category:

######  Definition 2.2 (Category of sets).

The sets (as objects) and functions (as arrows), with the usual compositions
and identities, form a category, that we will denote by
$\operatorname{\mathbf{Set}}$.

Another category we will make use of is the following:

######  Definition 2.3 (Category of posets).

A poset (partially ordered set) is a set together with an order relation
(transitive, reflexive and antisymmetric relation).
A monotone map $f$ between two posets $(X,\leq)$ and $(Y,\preceq)$ is a
function $f:X\to Y$ such that

$\forall\>x,x^{\prime}\in X,\ x\leq x^{\prime}\Rightarrow f(x)\preceq
f(x^{\prime})$

The posets and monotone maps (with the usual composition and identity) form a
category, that we will denote as $\operatorname{\mathbf{Poset}}$.

Of course, we want maps between categories. This is possible using the next
definition.

######  Definition 2.4 (Functor).

Given two categories $\mathbb{C}$ and $\mathbb{D}$, a functor $\mathcal{F}:
\mathbb{C}\to\mathbb{D}$ is a mapping from objects of $\mathbb{C}$ to objects
of $\mathbb{D}$ and from arrows of $\mathbb{C}$ to arrows of $\mathbb{D}$ that
preserves domains, codomains, composition and identities, that is:

  * •

for any arrow $f:A\to B$ in $\mathbb{C}$, $\mathcal{F}(f):
\mathcal{F}(A)\to\mathcal{F}(B)$,

  * •

for any two arrows $f:A\to B$ and $g:B\to C$, $\mathcal{F}(g\circ
f)=\mathcal{F}(g)\circ\mathcal{F}(f)$,

  * •

for any object $A$,
$\mathcal{F}(\operatorname{id}_{A})=\operatorname{id}_{\mathcal{F}(A)}$.

This definition can apply to an extremely large amount of contexts and usual
constructions, and this is the main reason why category theory is so handy in
formulating coalgebra, as we will see in section 3.1.

####

Here are some examples that we will use later in this report.

######  Example 2.1 (Product as a functor).

Given a set $X$, one can define the Cartesian product with $X$ as a functor
$\mathcal{F}$ in the category $\operatorname{\mathbf{Set}}$:

  * •

on objects, we define $\mathcal{F}(Y)=X\times Y$,

  * •

on arrows, we define $\mathcal{F}(f)(x,y)=(x,f(y))$, that is, $\mathcal{F}(f)$
is the identity on the $X$ component, and $f$ on the other component.

One can easily check that this fits into the definition above. This functor
will be denoted as $X\times(-)$ later in this report.

######  Example 2.2 (Exponential as a functor).

Given a set $X$, one can define the exponential with respect to $X$ as a
functor $\mathcal{F}$ in the category $\operatorname{\mathbf{Set}}$:

  * •

on objects, we define $\mathcal{F}(Y)=Y^{X}$, the set of functions from $X$ to
$Y$,

  * •

on arrows, we define $\mathcal{F}(f)(g)=f\circ g$, that is $\mathcal{F}(f)$ is
the post-composition with $f$.

Again, it is easy to check that this fits into the definition above. This
functor will be denoted as $(-)^{X}$ later in this report.

######  Example 2.3 (Identity functor).

Given a category $\mathbb{C}$, there is a so-called identity functor on
$\mathbb{C}$, written as $\operatorname{id}_{\mathbb{C}}$, defined as the
identity both on objects and arrows.

######  Example 2.4 (Powerset functor).

The usual powerset construction can be seen as a functor
$\mathcal{P}:\operatorname{\mathbf{Set}}\to\operatorname{\mathbf{Poset}}$,
defined as follows:

  * •

on objects, we define $\mathcal{P}(X)$ as the set of all subsets of $X$, with
the order given by inclusion,

  * •

on arrows, we define $\mathcal{P}(f)(P)=\\{f(x),x\in P\\}$, that is
$\mathcal{F}(f)$ takes the direct image of a subset by $f$.

If one forgets about the order structure, one can also see the same
$\mathcal{P}$ as a functor
$\mathcal{P}:\operatorname{\mathbf{Set}}\to\operatorname{\mathbf{Set}}$. In
the rest of the report, we will abuse notation and make no distinction between
both functors, as the correct type can be inferred from the context.

######  Example 2.5 (Forgetful functor).

A large and very useful class of functors is the class of forgetful functors,
that is functors between categories that “forget” some of the structure. For
instance, we can look at the category $\operatorname{\mathbf{Poset}}$. Its
objects are ordered sets, but one can “forget” that these objects have some
order structure, and rather look at them purely as sets. That is what the
following forgetful functor $\mathcal{U}$ does:

  * •

on objects, we define $\mathcal{U}((X,\leq))=X$,

  * •

on arrows, we define $\mathcal{U}(f)=f$ (but $f$ which was a monotone function
is now considered as a mere function between sets).

A last definition, which characterize to objects that are in a certain sense
“universal”.

######  Definition 2.5 (Final object).

A final object of a category $\mathbb{C}$ is an object $\mathbf{1}$ of
$\mathbb{C}$ such that for any other object $A$ of $\mathbb{C}$, there exists
a unique arrow $!_{A}:A\to\mathbf{1}$.

###  2.2 More Advanced Constructions

Until here, the constructions we defined were rather simple, and though they
may be useful as such, the real interest in category theory comes from more
complex constructions. These constructions are also the ones that are at the
core of the coalgebraic setting we will work in, mostly the notion of monad,
that we will use to encapsulate non-determinism.

The definitions will be given fully and illustrated with examples, in order to
give some grasp on them, but the details of the definitions are not needed to
understand the rest of the report past this section.

######  Definition 2.6 (Natural transformation).

Given two functors $\mathcal{F}:\mathbb{C}\to\mathbb{D}$ and
$\mathcal{G}:\mathbb{C}\to\mathbb{D}$, a natural transformation
$\lambda:\mathcal{F}\operatorname{\Rightarrow}\mathcal{G}$ is a family of
arrows (in $\mathbb{D}$) $\lambda_{X}:\mathcal{F}(X)\to\mathcal{G}(X)$ (one
for each object $X$ of $\mathbb{C}$) such that for any arrow $f: X\to Y$ in
$\mathbb{C}$, the following diagram commutes:
${\mathcal{F}(X)}$${\mathcal{G}(X)}$${\mathcal{F}(Y)}$${\mathcal{G}(Y)}$$\scriptstyle{\mathcal{F}(f)}$$\scriptstyle{\lambda_{X}}$$\scriptstyle{\mathcal{G}(f)}$$\scriptstyle{\lambda_{Y}}$
that is, such that
$\lambda_{Y}\circ\mathcal{F}(f)=\mathcal{G}(f)\circ\lambda_{X}$.

The idea of a natural transformation is that it is a transformation between
two functors that can be indifferently applied before of after a function
application. In a sense, it transforms $\mathcal{F}(X)$ into $\mathcal{G}(X)$
without looking at the content of $X$, but only at the structure given by
$\mathcal{F}$ and $\mathcal{G}$.

######  Example 2.6 (Cartesian Product).

Recall the functor $X\times(-)$ that we already defined on
$\operatorname{\mathbf{Set}}$. We could also define in a very similar way the
functor $(-)\times X$. Then there is a natural transformation
$\lambda:X\times(-)\operatorname{\Rightarrow}(-)\times X$ between these two
functors, defined by the components:

$\begin{array}[]{rccl}\lambda_{Y}:&X\times Y&\to&Y\times X\\\
&(x,y)&\mapsto&(y,x)\end{array}$

This notion of natural transformation is already useful as such, but it is
also a building element in a lot of other categorical notions, such as the one
of monad.

######  Definition 2.7 (Monad).

A monad is a functor $\mathcal{T}$ from a category $\mathbb{C}$ to itself,
together with two natural transformations
$\eta:\operatorname{id}\operatorname{\Rightarrow}\mathcal{T}$ and
$\mu:\mathcal{T}\circ\mathcal{T}\to\mathcal{T}$ such that the following
diagrams commute for any object $X$:
${\mathcal{T}(X)}$${\mathcal{T}(\mathcal{T}(X))}$${\mathcal{T}(\mathcal{T}(X))}$${\mathcal{T}(X)}$$\scriptstyle{\eta_{\mathcal{T}(X)}}$$\scriptstyle{\operatorname{id}_{X}}$$\scriptstyle{\mathcal{T}(\eta_{X})}$$\scriptstyle{\mu_{X}}$$\scriptstyle{\mu_{X}}$
${\mathcal{T}(\mathcal{T}(\mathcal{T}(X)))}$${\mathcal{T}(\mathcal{T}(X))}$${\mathcal{T}(\mathcal{T}(X))}$${\mathcal{T}(X)}$$\scriptstyle{\mu_{\mathcal{T}(X)}}$$\scriptstyle{\mathcal{T}(\mu_{X})}$$\scriptstyle{\mu_{X}}$$\scriptstyle{\mu_{X}}$
that is we have
$\mu_{X}\circ\eta_{\mathcal{T}(X)}=id_{X}=\mu_{X}\circ\mathcal{T}(\eta_{X})$
and $\mu_{X}\circ F(\mu_{X})=\mu_{X}\circ\mu_{F(X)}$.
The transformation $\eta$ is called the unit of the monad, and the
transformation $\mu$ is called its multiplication.

The idea is that a monad is some kind of structure, along with a way to put an
object into this structure (the unit), and a way to collapse two levels of the
structure together. These must respect some easy rules: if you use the unit to
put a second level, and collapse this level, then you get the thing you
started with, and if you collapse three levels into one, you can collapse the
outer most or inner most two first, with the same result.

######  Example 2.7 (Powerset as a monad).

We already described the powerset as a functor $\mathcal{P}$ from the category
$\operatorname{\mathbf{Set}}$ to itself. This functor can be made into a
monad, by taking:

  * •

the unit $\begin{array}[]{rccl}\eta_{X}:&X&\to&\mathcal{P}(X)\\\
&x&\mapsto&\\{x\\}\end{array}$,

  * •

the multiplication
$\begin{array}[]{rccl}\mu_{X}:&\mathcal{P}(\mathcal{P}(X))&\to&\mathcal{P}(X)\\\
&S&\mapsto&\cup S=\cup_{s\in S}s\end{array}$ (that is, take a set of sets to
their union).

The last important definition is the one of adjoints. This is a quite
difficult notion to grasp, although it is very powerful by itself. However, in
this report we will mostly be interested in their link with monads, as
adjunctions are a usual way to construct monads.

######  Definition 2.8 (Adjoints).

Two functors $\mathcal{F}:\mathbb{C}\to\mathbb{D}$ and
$\mathcal{G}:\mathbb{D}\to\mathbb{C}$ are said to be adjoints (this is written
as $\mathcal{F}\dashv\mathcal{G}$, $\mathcal{F}$ is called the left adjoint
and $\mathcal{G}$ is called the right adjoint) if there are two natural
transformation
$\eta:\operatorname{id}_{\mathbb{C}}\operatorname{\Rightarrow}\mathcal{G}\circ\mathcal{F}$
and
$\varepsilon:\mathcal{F}\circ\mathcal{G}\operatorname{\Rightarrow}\operatorname{id}_{\mathbb{D}}$
such that for any objects $C$ of $\mathbb{C}$ and $D$ of $\mathbb{D}$, we have

$\mathcal{G}(\varepsilon_{D})\circ\eta_{\mathcal{G}(D)}=\operatorname{id}_{\mathcal{G}(D)}$

and

$\varepsilon_{\mathcal{F}(C)}\circ\mathcal{F}(\eta_{C})=\operatorname{id}_{\mathcal{F}(C)}$

that is, such that the two following diagrams commute:
${\mathcal{G}(D)}$${\mathcal{G}(\mathcal{F}(\mathcal{G}(D)))}$${\mathcal{G}(D)}$$\scriptstyle{\eta_{\mathcal{G}(D)}}$$\scriptstyle{\operatorname{id}_{\mathcal{G}(D)}}$$\scriptstyle{\mathcal{G}(\varepsilon_{D})}$
${\mathcal{F}(C)}$${\mathcal{F}(\mathcal{G}(\mathcal{F}(C)))}$${\mathcal{F}(C)}$$\scriptstyle{\mathcal{F}(\eta_{C})}$$\scriptstyle{\operatorname{id}_{\mathcal{F}(C)}}$$\scriptstyle{\varepsilon_{\mathcal{F}(C)}}$

There are many equivalent ways to define adjunctions. This one is good for our
purposes, as it emphasizes the role of the unit and counit, which we will use
in section 4.1 to define a monad. Although this definition might not seem of
importance, adjoints, together with monads, form two of the most interesting
objects of category theory: a lot of mathematical interesting propositions and
definitions can be seen as instances of adjunctions, be it formal polynomials,
quantifiers, interior and closure operators in topology, free objects over a
set…

####

Here is an example of adjunction, of which we will make use later to construct
a monad.

######  Definition 2.9 (Discrete order functor).

The functor $\operatorname{\mathcal{O}}$ is the functor from the category
$\operatorname{\mathbf{Set}}$ to the category $\operatorname{\mathbf{Poset}}$
that maps

  * •

a set $X$ to the discrete order on $X$, that is
$\operatorname{\mathcal{O}}(X)=(X,=)$ (in the discrete order, the only
comparable elements are the ones that are equal),

  * •

an arrow $f$ to itself.

Note that if $f:X\to Y$ is a function in $\operatorname{\mathbf{Set}}$, then
$f$ is also a monotone function between $\operatorname{\mathcal{O}}(X)$ and
$\operatorname{\mathcal{O}}(Y)$, so that this definition makes sense.

######  Proposition 2.1 (Adjunction for $\operatorname{\mathcal{O}}$).

There is an adjunction $\operatorname{\mathcal{O}}\dashv\mathcal{U}$ between
the discrete order functor we just defined and the forgetful functor
$\mathcal{U}:\operatorname{\mathbf{Poset}}\to\operatorname{\mathbf{Set}}$ as
defined in section 2.1.

Its unit is just the identity, and its counit is defined on a preorder
$X=(S,\leq)$ by

$\begin{array}[]{rccl}\varepsilon_{X}:&\operatorname{\mathcal{O}}(\mathcal{U}(X))&\to&X\\\
&x&\mapsto&x\end{array}$

so it is the identity of $S$, but it goes from the preorder $(S,=)$ to the
preorder $(S,\leq)$.

##  3 Coalgebras And Determinization

In this section, we present the main subject of the internship, namely
coalgebra and the view it gives on determinization. Once again, we do not
provide the proofs of the facts we state, but these can be found in the papers
we refer to.

###  3.1 State-Based Systems as Coalgebras

In this subsection we define our core construction: coalgebras. We also show
how final objects can be used to give some sort of semantics. A more complete
approach (with proofs!) can be found in [4].

######  Definition 3.1 (Coalgebra).

Given a category $\mathbb{C}$, a coalgebra for a functor
$\mathcal{F}:\mathbb{C}\to\mathbb{C}$ consists of an object $X$ together with
an arrow $f:X\to\mathcal{F}X$.

Coalgebras are meant to represent state-based system, where $X$ represents the
states of the system, and $f$ is the transition function. Then the functor
$\mathcal{F}$ characterizes the type of system we are looking at.

######  Example 3.1 (Stream system).

A stream system over an alphabet (set of letters) $A$ is a set of states $X$
together with two functions $o:X\to A$ (output) and $t:X\to X$ (transition).
It is a coalgebra for the functor $A\times(-)$, the transition function being
$\langle o,t\rangle:X\to A\times X$, where $\langle o,t\rangle$ is defined by:
$\begin{array}[]{rccl}\langle o,t\rangle:&X&\to&A\times X\\\
&x&\mapsto&(o(x),t(x))\end{array}$

######  Example 3.2 (Deterministic automaton).

A deterministic automaton over an alphabet $A$ is a set of states $Q$,
together with a function $o:X\to\mathbf{2}$ (where $\mathbf{2}$ is the two-
element set $\\{\mathbf{0},\mathbf{1}\\}$, returning $\mathbf{1}$ if the state
is accepting and $\mathbf{0}$ otherwise) and a transition function
$\delta:Q\to Q^{A}$. It is a coalgebra for the functor
$\mathbf{2}\times(-)^{A}$, the transition function being $\langle
o,\delta\rangle$ where $\chi_{F}$.

This way of looking at things is a bit unusual, but this is really the same as
the usual definition of non-deterministic automata: the function $o$
corresponds to the characteristic function of the set of final states, and the
function $\delta$ can be seen as a function of the type $X\times A\to X$, as
for any $(x,a)\in X\times A$, $\delta(x)(a)$ is an element of $X$ (the
$\delta$ of the coalgebraic definition is the curried version of the usual
one).

Since we will reuse this $\mathbf{2}\times(-)^{A}$ functor, we will denote it
as $\mathcal{D}$.

Note that in the above examples we are not taking into account any starting
state. This is because the aim is really to describe a state-based system, not
just one “computation” into it (for instance, the computation of a stream for
a stream system, or of the acceptance or rejection of a word in an automaton).

######  Definition 3.2 (Homomorphism of coalgebras).

Given two coalgebras $(X,f)$ and $(Y,g)$ for a functor $\mathcal{F}$, a
coalgebra homomorphism is an arrow $h:X\to Y$ such that the following diagram
commutes:
${X}$${Y}$${\mathcal{F}X}$${\mathcal{F}Y}$$\scriptstyle{f}$$\scriptstyle{h}$$\scriptstyle{g}$$\scriptstyle{\mathcal{F}h}$

That is, we can either make a transition, and then use the arrow, or use the
arrow first, and then make a transition.

####

With this we can construct a new category.

######  Proposition 3.1.

Given a (fixed) functor, the coalgebras and homomorphism of coalgebras for
this functor form a category.

######  Definition 3.3 (Final coalgebra).

Given a functor $\mathcal{F}$, a coalgebra $(Z,\xi)$ is called a final
coalgebra if it is a final object in the category of coalgebras. This means
that given a coalgebra $(X,f)$ for $\mathcal{F}$, there is a unique arrow
$\operatorname{beh}_{f}$ (we might call it simply $\operatorname{beh}$ if
there is no possible confusion) such that the following diagram commutes:
${X}$${Z}$${\mathcal{F}X}$${\mathcal{F}Z}$$\scriptstyle{f}$$\scriptstyle{\operatorname{beh}}$$\scriptstyle{\xi}$$\scriptstyle{\mathcal{F}\operatorname{beh}}$

This definition is crucial, as it gives semantics for states: if we work in
the category of sets, and $x$ is an element of $X$, then
$\operatorname{beh}_{f}(x)$ is the semantics of the state $x$, as the
following examples illustrate.

######  Example 3.3 (Final stream system).

Given an alphabet $A$, the coalgebra $(A^{\omega},\langle
o_{z},t_{z}\rangle)$, where $o_{z}(s)=s(0)$ (the output is the first element
of the stream) and $t_{z}(s)(i)=s(i+1)$ (the transition is a shift of the
stream), is a final coalgebra for the functor $A\times(-)$ of stream systems.
Moreover, if $(X,\langle o,t\rangle)$ is a stream system, then
$\operatorname{beh}(x)=(o(x),o(t(x)),o(t^{2}(x)),o(t^{3}(x)),\dots)$.

This corresponds to the stream one would naturally associate with $x$ in the
stream system $(X,\langle o,t\rangle)$.

######  Example 3.4 (Final deterministic automaton).

Given an alphabet $A$, the coalgebra $(\mathbf{2}^{A^{*}},\langle O,D\rangle)$
where $\mathbf{2}^{A^{*}}$ is the set of languages over $A$,

$O(L)=\left\\{\begin{array}[]{l}\mathbf{0}\text{ if
}\operatorname{\varepsilon}\notin L\\\ \mathbf{1}\text{ if
}\operatorname{\varepsilon}\in L\end{array}\right.$

with $\operatorname{\varepsilon}$ denoting the empty word, and

$D(L)(a)=\\{w\in A^{*}\mid a\cdot w\in L\\}$

is a final coalgebra for $\mathbf{2}\times(-)^{A}$.

As expected, if $(Q,\langle o,\delta\rangle)$ is an automaton and $q$ is a
state of $Q$, then $\operatorname{beh}(q)$ is the language accepted by the
automaton with starting state $q$, as defined usually:

  * •

$\operatorname{\varepsilon}\in\operatorname{beh}(q)$ if and only if $o(q)=1$,

  * •

for any word $w$ and letter $a$, $a\cdot w\in\operatorname{beh}(q)$ if and
only if $w\in\operatorname{beh}(\delta(q)(a))$.

###  3.2 The Problem Of Determinization

The main subject of this internship is the determinization procedure for an
automaton. There is a well-known example, namely the one of non-deterministic
automata. In that case, a new (deterministic) automaton is created, whose
states are sets of states of the original automaton, and the semantics (in
this case, the language denoted by the automaton) is preserved by the
construction.

######  Definition 3.4 (Non-deterministic automaton).

Given an alphabet $A$, a non-deterministic automaton consists of a set of
states $Q$ together with a function $o:Q\to\mathbf{2}$ and a transition
function $\delta:Q\to\mathcal{P}(Q)^{A}$. It is a coalgebra for the functor
$\mathbf{2}\times(\mathcal{P}(-))^{A}$.
A word $w$ is accepted by a state $q\in Q$ if

  * •

$w=\operatorname{\varepsilon}$ and $o(q)=1$,

  * •

$w=a\cdot w^{\prime}$ and $w^{\prime}$ is accepted by one of the states in
$\delta(q)(a)$.

######  Definition 3.5 (Determinization of an automaton).

Given a non-deterministic automaton $(Q,o,\delta)$ over an alphabet $A$, its
determinization is a deterministic automaton, with

  * •

state set $\mathcal{P}(Q)$,

  * •

accepting function $o^{\\#}$ defined by
$o^{\\#}(S)=1\Leftrightarrow\exists\>s\in S,\ o(s)=1$, a subset of $Q$ is
accepting if it contains an accepting state,

  * •

transition function $\delta^{\\#}: \mathcal{P}(Q)\to\mathcal{P}(Q)^{A}$,
defined by $\delta^{\\#}(S)(a)=\cup_{q\in P}\delta(q)(a)$.

######  Theorem 3.2 (Preservation of the semantics).

A state $q$ of a non-deterministic automaton accepts a word if and only if the
state $\\{q\\}$ of the determinization of the automaton accepts the word.

Following this motivating example, we wand to find a general way to perform
the same kind of determinization. But first, we need to define what we wish to
determinize.

######  Definition 3.6 ($\mathcal{T}$-automaton).

Given a monad $(\mathcal{T},\eta,\mu)$ on the category of sets, a
$\mathcal{T}$-automaton for an alphabet $A$ is a coalgebra for the functor
$\mathbf{2}\times(\mathcal{T}(-))^{A}$.

Here the monad represents the “non-determinisic” component of the automaton,
as the example of non-deterministic automata illustrates. The
$\mathbf{2}\times(-)^{A}$, as we already saw, corresponds to the automaton
structure.

######  Example 3.5 (Non-deterministic automaton as a
$\mathcal{P}$-automaton).

A non-deterministic automaton is a $\mathcal{P}$-automaton, that is, a
coalgebra for the functor $\mathbf{2}\times(\mathcal{P}(-))^{A}$.

But for instance the case of probabilistic automata also fits into this
definition, with a proper monad (whose functorial component involves
probability distributions).

####

The aim is then, given a monad $\mathcal{T}$ and a $\mathcal{T}$-automaton
$(X,f)$, to find a semantics for $(X,f)$, that is a function from $X$ to the
final coalgebra $\mathbf{2}^{A^{*}}$, that should arise “naturally” in some
sense, and correspond with the concrete semantics that one already has on the
motivating examples like the non-deterministic automata.

The next two sections provide two different ways to do this. The first one
gives some semantics directly, without really resorting to determinization as
such. The second one is the direct abstraction of the determinization of non-
deterministic automata, in the sense that from a $\mathcal{T}$-automaton with
state space $X$ it constructs a deterministic automaton with state space
$\mathcal{T}(X)$.

###  3.3 Bialgebraic Semantics

The construction presented here can be found in all details in [5]. Its main
ingredient is a so called Eilenberg-Moore algebra, that is an arrow
$\beta:\mathcal{T}(\mathbf{2})\to\mathbf{2}$ satisfying some axioms.

######  Definition 3.7 (Eilenberg-Moore algebra).

Given a monad $(\mathcal{T},\eta,\mu)$, an Eilenberg-Moore algebra is an
object $X$ together with an arrow $\beta:\mathcal{T}(X)\to X$ such that the
following diagrams commute:
${X}$${\mathcal{T}(X)}$${X}$$\scriptstyle{\eta_{X}}$$\scriptstyle{\operatorname{id}_{X}}$$\scriptstyle{\beta}$
${\mathcal{T}(\mathcal{T}(X)))}$${\mathcal{T}(X)}$${\mathcal{T}(X)}$${X}$$\scriptstyle{\mathcal{T}(\beta)}$$\scriptstyle{\mu_{X}}$$\scriptstyle{\beta}$$\scriptstyle{\beta}$

Given such an Eilenberg-Moore algebra, one can construct a new algebra on
functions, using the so-called strength of the monad.

######  Definition 3.8 (Strength).

Given a monad $\mathcal{T}$, the strength
$\operatorname{st}:\mathcal{T}(X^{Y})\to\mathcal{T}(X)^{Y}$ is defined by
$\operatorname{st}(f)(y)=\mathcal{T}(\lambda h\in X^{Y}\cdot h(y))(f)$.

Note that this construction only works because in the category
$\operatorname{\mathbf{Set}}$, the function $\lambda h\in X^{Y}\cdot h(y)$
always exists, no matter what $y$ is chosen, which is not the case in all
categories.

We will use this strength operator (which actually is a natural transformation
$\operatorname{st}:\mathcal{T}(X^{Y})\operatorname{\Rightarrow}\mathcal{T}(X)^{Y}$)
again later, as it is a very useful construction: it allows to put a monad
“inside” a set of functions.

####

Now we can construct our algebra on functions.

######  Proposition 3.3 (Pointwise Eilenberg-Moore algebra).

Given a Eilenberg-Moore algebra $(X,\beta)$ for a monad $\mathcal{T}$ in the
category of sets and a set $Y$, one can define a new Eilenberg-Moore algebra
$(X^{Y},\hat{\beta})$, defined, given $f\in\mathcal{T}(X^{Y})$, by

$\begin{array}[]{rccl}\hat{\beta}(f):&Y&\to&X\\\
&y&\mapsto&\beta(\operatorname{st}(f)(y))\end{array}$

####

With this algebra, we can state the main theorem of this section, found in
[5].

######  Theorem 3.4 (Bialgebraic semantics).

Given some monad $(\mathcal{T},\eta,\mu)$, an Eilenberg-Moore algebra
$\beta:\mathcal{T}(\mathbf{2})\to\mathbf{2}$, and a $\mathcal{T}$-automaton
$(X,f)$, there exists a unique map
$\operatorname{beh}_{1}:X\to\mathbf{2}^{A^{*}}$ that makes the following
diagram commute:
${X}$${\mathbf{2}^{A^{*}}}$${\mathcal{D}(\mathbf{2}^{A^{*}})}$${\mathbf{2}\times(\mathcal{T}(X))^{A}=\mathcal{D}(\mathcal{T}(X))}$${\mathcal{D}(\mathcal{T}(\mathbf{2}^{A^{*}}))}$$\scriptstyle{\operatorname{beh}_{1}}$$\scriptstyle{f}$$\scriptstyle{\langle
O{,}D\rangle}$$\scriptstyle{\mathcal{D}(\mathcal{T}(\operatorname{beh}_{1}))}$$\scriptstyle{\mathcal{D}(\hat{\beta})}$
(recall that $\mathcal{D}$ is the functor for deterministic automata, that is
$\mathcal{D}=\mathbf{2}\times(-)^{A}$).

This means that given only an Eilenberg-Moore algebra on $\mathbf{2}$, we can
get a semantics for any $\mathcal{T}$-automaton, and moreover this semantics
is the only one “compatible” with the algebra. When one considers in detail
the above diagram for $\operatorname{beh}_{1}$, this “compatibility” says that
one can either make a transition in the automaton, then go to the semantics
world and use $\beta$ to aggregate the states together, or go to the semantics
world and make the transition there, and that these two yield the same result.

When looking at examples, spelling out this diagram in concrete terms usually
corresponds to an inductive definition of acceptance of a word, similar to the
one we gave for non-deterministic automata in section 3.2: there is a rule for
acceptance of the empty word, and a rule for acceptance of a word $a\cdot w$,
based on the transitions made from the current state using $a$. We will have
another example of this with alternating automata once we have a suitable
$\mathcal{T}$-automaton structure for it.

####

In this theorem, the algebra $\beta$ should be seen as the formal translation
of the accept condition after one step. The following example, that uses the
same monad but different algebras, illustrates that.

######  Example 3.6 (Universal and existential non-deterministic automata).

Given a $\mathcal{P}$-automaton, one has two “natural” ways to define
$\beta:\mathcal{P}(\mathbf{2})\to\mathbf{2}$: one can take $\beta(P)=\max(P)$
or $\beta(P)=\min(P)$.

The map $\operatorname{beh}_{\max}$ obtained by the first one is the usual
semantics, where we require that there exists a transition
$q\stackrel{{\scriptstyle a}}{{\to}}q^{\prime}$ where $q^{\prime}$ accepts $w$
for $q$ to accept $a\cdot w$. This is the usual definition of a non-
deterministic automaton (as appearing in section 3.2), but we could also call
it an existential non-deterministic automaton.

On the contrary, the map $\operatorname{beh}_{\min}$ obtained by the second
one corresponds to the semantics where we require that all transitions
$q\stackrel{{\scriptstyle a}}{{\to}}q^{\prime}$ lead to a state $q^{\prime}$
accepting $w$ for $q$ to accept $a\cdot w$. This is also called a universal
non-deterministic automaton.

###  3.4 Semantics Via Determinization

The content of this section is drawn out of [6]. Its main ingredient is a so
called distributive law.

######  Definition 3.9 (Distributive law).

Given a monad $(\mathcal{T},\eta,\mu)$ and a functor $\mathcal{G}$, a
distributive law is a natural transformation
$\lambda:\mathcal{T}\mathcal{G}\operatorname{\Rightarrow}\mathcal{G}\mathcal{T}$,
that is compatible with the monad structure, that is such that the following
diagrams commute for any object $X$:
${\mathcal{G}(X)}$${\mathcal{T}(\mathcal{G}(X))}$${\mathcal{G}(\mathcal{T}(X))}$$\scriptstyle{\eta_{\mathcal{G}(X)}}$$\scriptstyle{\mathcal{G}(\eta_{X})}$$\scriptstyle{\lambda_{X}}$
${\mathcal{T}^{2}(\mathcal{G}(X))}$${\mathcal{T}(\mathcal{G}(\mathcal{T}(X)))}$${\mathcal{G}(\mathcal{T}^{2}(X))}$${\mathcal{T}(\mathcal{G}(X))}$${\mathcal{G}(\mathcal{T}(X))}$$\scriptstyle{\mathcal{T}(\lambda_{X})}$$\scriptstyle{\mu_{\mathcal{G}(X)}}$$\scriptstyle{\lambda_{\mathcal{T}(X)}}$$\scriptstyle{\mathcal{G}(\mu_{X})}$$\scriptstyle{\lambda_{X}}$

######  Theorem 3.5 (Determinization via a distributive law).

Given a monad $(\mathcal{T},\eta,\mu)$, a functor $\mathcal{G}$, a
distributive law $\lambda$ and a $\mathcal{G}\mathcal{T}$-coalgebra $(X,f)$,
one can construct a determinization of $(X,f)$, namely the
$\mathcal{G}$-coalgebra
$(\mathcal{T}(X),\mathcal{F}_{\mathcal{E}\mathcal{M}}(f))$, where

$\mathcal{F}_{\mathcal{E}\mathcal{M}}(f):\mathcal{T}(X)\to\mathcal{G}(\mathcal{T}(X))=\left(\mathcal{T}(X)\stackrel{{\scriptstyle\mathcal{T}(f)}}{{\to}}\mathcal{T}(\mathcal{G}(\mathcal{T}(X)))\stackrel{{\scriptstyle\lambda_{\mathcal{T}(X)}}}{{\to}}\mathcal{G}(\mathcal{T}^{2}(X))\stackrel{{\scriptstyle\mathcal{G}(\mu_{X})}}{{\to}}\mathcal{G}(\mathcal{T}(X))\right)$

Moreover, this determinized coalgebra makes the following diagram commute:
${X}$${\mathcal{T}(X)}$${\mathcal{G}(\mathcal{T}(X))}$$\scriptstyle{\eta_{X}}$$\scriptstyle{f}$$\scriptstyle{\mathcal{F}_{\mathcal{E}\mathcal{M}}(f)}$

This commutative triangle is also called the generalized powerset
construction, and has appeared for the first time is [14].

######  Corollary 3.6.

In the context of the theorem above, if the functor $\mathcal{G}$ has a final
coalgebra $(Z,\xi)$, one gets a semantics for $f$ via the unique arrow
$\operatorname{beh}_{2}:\mathcal{T}(X)\to Z$, that is the unique arrow making
the following diagram commute:
${X}$${\mathcal{T}(X)}$${Z}$${\mathcal{G}(\mathcal{T}(X))}$${\mathcal{G}(Z)}$$\scriptstyle{\eta_{X}}$$\scriptstyle{f}$$\scriptstyle{\mathcal{F}_{\mathcal{E}\mathcal{M}}(f)}$$\scriptstyle{\operatorname{beh}_{2}}$$\scriptstyle{\xi}$$\scriptstyle{\mathcal{G}(\operatorname{beh}_{2})}$

In the case where $\mathcal{G}$ is the functor for automata, the situation is
even better, as the distributive law can be constructed from a
$\mathcal{T}$-algebra, similar to the one used in section 3.3, as shown in
[6].

######  Proposition 3.7 (Distributive law arising from an algebra).

Given a monad $(\mathcal{T},\eta,\mu)$ and a $\mathcal{T}$-algebra
$\beta:\mathcal{T}(\mathbf{2})\to\mathbf{2}$, there is a distributive law
$\lambda$ between $\mathcal{T}$ and $\mathcal{D}$, constructed as follows:

$\lambda_{X}:\mathcal{T}(\mathbf{2}\times
X^{A})\to\mathbf{2}\times\mathcal{T}(X)^{A}=\left(\mathcal{T}(\mathbf{2}\times
X^{A})\stackrel{{\scriptstyle\langle\mathcal{T}(\pi_{1}),\mathcal{T}(\pi_{2})\rangle}}{{\longrightarrow}}\mathcal{T}(\mathbf{2})\times\mathcal{T}(X^{A})\stackrel{{\scriptstyle\beta\times
st}}{{\longrightarrow}}\mathbf{2}\times\mathcal{T}(X)^{A}\right)$

where $\pi_{1}$ and $\pi_{2}$ are the two projection from the product
$\mathbf{2}\times X^{A}$.

So as before, given only a $\mathcal{T}$-algebra on $\mathbf{2}$ we are able
to fully define a semantics.

######  Example 3.7 (Correspondance with concrete determinization).

In the case where the monad is $\mathcal{P}$, the functor is $\mathcal{D}$ and
$\beta$ is $\max$, the obtained determinized coalgebra is exactly the same as
in the usual determinization: if $(Q,\langle o,\delta\rangle)$ is a non-
deterministic automaton, then $\mathcal{F}_{\mathcal{E}\mathcal{M}}(\langle
o,\delta\rangle)=\langle o^{\\#},\delta^{\\#}\rangle$, with $o^{\\#}$ and
$\delta^{\\#}$ defined as in 3.2.

Then the theorem of preservation of semantics (theorem 3.2) just states that
the semantics defined by $\operatorname{beh}_{2}\circ\eta_{Q}$ is the same as
the one defined concretely, because for $\mathcal{P}$, the unit $\eta$ is
defined by $\eta_{Q}(q)=\\{q\\}$.

The most interesting fact, however, is the following, which appears in [5],
but relies on more high-level results from [2].

######  Theorem 3.8 (Correspondance of the two semantics).

Given a monad $(\mathcal{T},\eta,\mu)$ and a $\mathcal{T}$-algebra
$\beta:\mathcal{T}(\mathbf{2})\to\mathbf{2}$, the two semantics
$\operatorname{beh}_{1}$ of section 3.3 and $\operatorname{beh}_{2}$ are such
that $\operatorname{beh}_{2}\circ\eta_{X}=\operatorname{beh}_{1}$.

In other words, the bialgebraic semantics and the semantics via
determinization are essentially the same, even if the way they are presented
is quite different. This can be interpreted in two different ways: one could
argue the fact that those two constructs yield in the end the same result, is
an argument in favor of thinking that they represent the “natural” way to
associate a semantics to a $\mathcal{T}$-automaton.

The second way, and maybe more interesting way, is to view the previous
theorem as stating that the determinization procedure yields the only
semantics that is compatible with $\beta$ (in the sense we developed at the
end of section 3.3), so that it is in a way the only correct way to
determinize with respect to $\beta$.

The two different constructions also have different interests:
$\operatorname{beh}_{1}$ is useful in getting a semantics, and obtaining in
concrete terms the definition of this semantics, while
$\operatorname{beh}_{2}$ is a way to construct a new automaton, that
recognizes the same language as the $\mathcal{T}$-automaton we were
considering.

##  4 The Case Of Alternating Automata

###  4.1 Alternating Automata

In this section, we present the state-based system we are interested in, the
alternating automaton. This model is a kind of extension of the non-
deterministic automaton: in a non-deterministic automaton, a word $a\cdot w$
is accepted from a state $q$ if there is a transition
$q\stackrel{{\scriptstyle a}}{{\to}}q^{\prime}$ to a state $q^{\prime}$ that
accepts the word $w$. However, one could choose a different rule, for instance
say that every transition labeled with $a$ should lead to a state accepting
$w$. These are the simplest examples, but one could wish to use other logical
rule to relate acceptation by a state to acceptation by other states. This is
the idea that lead to the model of alternating automata.

Alternating automata were first introduced in [3] with slightly more general
features than the ones we consider, and in a quite different presentation. Our
model has been chosen over the original one because of the ease to translate
it in a categorical fashion.

######  Definition 4.1 (Alternating automata (preliminary)).

An alternating automaton with respect to an alphabet $A$ is a coalgebra for
the functor $\mathcal{D}\circ\mathcal{P}\circ\mathcal{P}$, that is a set $Q$
together with a function $\langle
o,\delta\rangle:Q\to\mathbf{2}\times\mathcal{P}(\mathcal{P}(Q))^{A}$. As for a
deterministic automaton, the function $o:Q\to\mathbf{2}$ represents the
accepting states. Concerning the transition function,
$\mathcal{P}(\mathcal{P}(Q))$ is seen as a set of “forks”.
Acceptation of a word is then defined by induction, as follows:

  * •

a state $q$ accepts the empty word if and only if $o(q)=\mathbf{1}$,

  * •

a state $q$ accepts the word $a\cdot w$ if and only if there is a fork in
$\delta(q)(a)$ such that every state of the fork accepts $w$, that is
$accepts(q,a\cdot w)\Leftrightarrow\exists\>F\in\delta(q)(a),\
\forall\>q^{\prime}\in F,\ accepts(q,w)$.

Note how we decomposed our functor in two parts: one corresponding to the
automaton structure, and the other one to the non-deterministic part. This is
the same decomposition we already studied in section 3. Our hope is to give a
monadic structure to $\mathcal{P}\circ\mathcal{P}$, so that our definition of
alternating automaton fits in the generic picture of determinization of a
$\mathcal{T}$-automaton in section 3.

######  Example 4.1 (Example of alternating automata).

The following automaton, with start state $q_{0}$, recognizes words with an
even number of $a$ and $b$, or an odd number of $a$ and $b$.
$q_{0}$$q_{1}$$q_{2}$$q_{3}$$q_{4}$$a,b$$a,b$babaabab

###  4.2 A Monadic Structure For Alternating Automata

This section contains most of the original work of the report. For reasons of
clarity, we did not include the proofs of the original theorems we state in
the section. However we added them in appendix A, so that the interested
reader can still have a look at them.

####

As we want to give a monadic structure to $\mathcal{P}\mathcal{P}$, and we
already know $\mathcal{P}$ has a monadic structure, we are looking for a way
to compose monads. The following proposition is the usual way it is done. It
involves a distributive law between monads, which is defined in a similar way
to a distributive law as defined in section 3.4, with two more properties for
the compatibility of the law with the second monad.

######  Proposition 4.1 (Composition of monads).

Given two monads $(\mathcal{T}_{1},\eta^{1},\mu^{1})$ and
$(\mathcal{T}_{2},\eta^{2},\mu^{2})$ and a distributive law between monads
$\lambda:\mathcal{T}_{1}\mathcal{T}_{2}\operatorname{\Rightarrow}\mathcal{T}_{2}\mathcal{T}_{1}$,
one can create a new composite monad, with the components:

  * •

functorial part $\mathcal{T}=\mathcal{T}_{2}\circ\mathcal{T}_{1}$,

  * •

unit $\eta$ defined by the components

$\eta_{X}:X\to\mathcal{T}(X)=\left(X\stackrel{{\scriptstyle\eta^{1}_{X}}}{{\longrightarrow}}\mathcal{T}_{1}(X)\stackrel{{\scriptstyle\eta^{2}_{\mathcal{T}_{1}(X)}}}{{\longrightarrow}}\mathcal{T}_{2}(\mathcal{T}_{1}(X))\right)$

  * •

multiplication $\mu$ defined by the components

$\mu_{X}:\mathcal{T}^{2}(X)\to\mathcal{T}(X)=\left(\mathcal{T}_{2}(\mathcal{T}_{1}(\mathcal{T}_{2}(\mathcal{T}_{1}(X))))\stackrel{{\scriptstyle\mathcal{T}_{2}(\lambda_{\mathcal{T}_{1}(X)})}}{{\longrightarrow}}\mathcal{T}_{2}^{2}(\mathcal{T}_{1}^{2}(X))\stackrel{{\scriptstyle\mu^{2}_{\mathcal{T}_{1}^{2}(X)}}}{{\longrightarrow}}\mathcal{T}_{2}(\mathcal{T}_{1}^{2}(X))\stackrel{{\scriptstyle\mathcal{T}_{2}(\mu^{1}_{X})}}{{\longrightarrow}}\mathcal{T}_{2}(\mathcal{T}_{1}(X))\right)$

Note that naturality of the components of both monads ensure that the order in
which the units and multiplications are performed are irrelevant, for instance
one could apply $\eta^{2}$ first and the $\eta^{1}$, the resulting $\eta$
would be the same.

####

One could then try to construct a suitable distributive law for powerset over
powerset, that should somehow reflect the fact that the outside powerset is
considered disjunctively and the inside one is considered conjunctively. The
natural candidate is the following law:

$\begin{array}[]{rccl}\lambda_{X}:&\mathcal{P}(\mathcal{P}(X))&\to&\mathcal{P}(\mathcal{P}((X))\\\
&S&\mapsto&\\{V\subseteq\cup S\mid\forall\>U\in S,\ \operatorname{Card}(V\cap
U)=1\\}\end{array}$

that corresponds to the conversion of a disjunctive normal form into a
conjunctive normal form.

However this is sadly not even a natural transformation. Patching it to

$\begin{array}[]{rccl}\lambda_{X}:&\mathcal{P}(\mathcal{P}(X))&\to&\mathcal{P}(\mathcal{P}((X))\\\
&S&\mapsto&\\{V\subseteq\cup S\mid\forall\>U\in S,\ \operatorname{Card}(V\cap
U)\geq 1\\}\end{array}$

(instead of taking exactly one element in every set, we take at least one)
yields a natural transformation, however this natural transformation is not a
distributive law (of monads over monads), and actually there are examples in
[13] showing the natural transformation does not lead to a monad structure on
$\mathcal{P}\mathcal{P}$.

A way to explain it is to observe that in the functor $\mathcal{P}\mathcal{P}$
we wish to turn into a monad, the outside $\mathcal{P}$ is in some way too
relaxed. Indeed, if we have two forks $f\subseteq f^{\prime}\subseteq X$, then
the fork $f^{\prime}$ accepts a word only if the fork $f$ accepts that word as
well, so $\\{f,f^{\prime}\\}$ accepts the exact same words as $\\{f\\}$. This
is not very annoying for our concrete definition of acceptance, but as we just
saw, when we move to category theory, the outside $\mathcal{P}$ causes
troubles.

There are at least two different ways to patch this and get a unique set of
fork to represent an acceptance condition:

  * •

require that no two forks are comparable; this replaces
$\mathcal{P}(\mathcal{P}(X))$ by $\mathcal{A}(\mathcal{P}(X))$, the set of
antichains (set of pairwise incomparable elements) of $\mathcal{P}(X)$,

  * •

close the set of forks with respect to inclusion; this replaces
$\mathcal{P}(\mathcal{P}(X))$ by
$\tilde{\operatorname{\mathcal{U\mkern-3.0mup}}}(\mathcal{P}(X))$, the set of
upward closed sets of $\mathcal{P}(X)$.

These two solutions are actually really close, as for any ordered set, there
is a bijection between antichains over the set and upsets over the set (taking
the minimal elements of an upset, and the upwards closure of an antichain).
This is why we only explore one of the two idea — the one using upsets. It
will enable us to give a correct distributive law, and following, also a
correct monadic structure. This is why we alter the coalgebraic definition of
alternating automata to the following:

######  Definition 4.2 (Alternating automata).

An alternating automaton with respect to an alphabet $A$ is a coalgebra for
the functor
$\mathcal{D}\circ\operatorname{\widetilde{\operatorname{\mathcal{U\mkern-3.0mup}}}}\circ\mathcal{P}$,
where $\mathcal{P}$ is the powerset monad (with codomain the category
$\operatorname{\mathbf{Poset}}$), and
$\operatorname{\widetilde{\operatorname{\mathcal{U\mkern-3.0mup}}}}$ is a
functor from the category $\operatorname{\mathbf{Poset}}$ to the category
$\operatorname{\mathbf{Set}}$ that takes a poset to the set of its upwards
closed sets.
We will denote the functor
$\operatorname{\widetilde{\operatorname{\mathcal{U\mkern-3.0mup}}}}\circ\mathcal{P}$
by $\operatorname{\mathcal{A\mkern-3.0mult}}$.

Now, if we want to make this definition work with the results from section 3,
we need to give $\operatorname{\mathcal{A\mkern-3.0mult}}$ a monadic
structure. This is where category theory proves useful, because it will enable
us to combine simple constructions in a reasonably easy way.

######  Definition 4.3 (Upwards closure, downwards closure).

Given a poset $X$ and a subset $P$ of $X$, the upwards closure of $P$, denoted
as $\operatorname{\uparrow}P$ is the set defined by

$\operatorname{\uparrow}P=\\{x\in X\mid\exists\>y\in P,\ y\leq x\\}$

The downwards closure of $P$, denoted as $\operatorname{\downarrow}P$, is
defined similarly as

$\operatorname{\downarrow}P=\\{x\in X\mid\exists\>y\in P,\ y\geq x\\}$

Note that the upwards (resp. downwards) closure of a set is always upwards
(resp. downwards) closed.

Using this, we can define two monads on $\operatorname{\mathbf{Poset}}$.

######  Definition 4.4 (Upset monad).

We define the monad
$(\operatorname{\mathcal{U\mkern-3.0mup}},\eta^{\operatorname{\mathcal{U\mkern-3.0mup}}},\mu^{\operatorname{\mathcal{U\mkern-3.0mup}}})$
on the category of posets as follows:

  * •

on objects, $\operatorname{\mathcal{U\mkern-3.0mup}}((X,\preceq))$ is the set
of upwards closed sets of $X$, ordered by reversed inclusion order, that is
$\operatorname{\mathcal{U\mkern-3.0mup}}(X)=(\\{P\subseteq
X\mid\forall\>x,y\in X,\ x\preceq y\wedge x\in P\Rightarrow y\in
P\\},\supseteq)$,

  * •

on arrows,
$\operatorname{\mathcal{U\mkern-3.0mup}}(f)(P)=\operatorname{\uparrow}f(P)=\\{y\in
X\mid\exists\>x\in P,\ f(x)\leq y\\}$,

  * •

the unit is
$\eta^{\operatorname{\mathcal{U\mkern-3.0mup}}}(x)=\operatorname{\uparrow}\\{x\\}$,

  * •

the multiplication is $\mu^{\operatorname{\mathcal{U\mkern-3.0mup}}}(S)=\cup
S$, as for the powerset monad.

######  Definition 4.5 (Downset monad).

We define the monad
$(\operatorname{\mathcal{D\mkern-3.0mun}},\eta^{\operatorname{\mathcal{D\mkern-3.0mun}}},\mu^{\operatorname{\mathcal{D\mkern-3.0mun}}})$
on the category of posets as follows:

  * •

on objects, $\operatorname{\mathcal{D\mkern-3.0mun}}(X)$ is the set of
downwards closed sets of $X$, ordered by inclusion order, that is
$\operatorname{\mathcal{D\mkern-3.0mun}}(X)=(\\{P\subseteq
X\mid\forall\>x,y\in X,\ x\geq y\wedge x\in P\Rightarrow y\in
P\\},\subseteq)$,

  * •

on arrows,
$\operatorname{\mathcal{D\mkern-3.0mun}}(f)(P)=\operatorname{\downarrow}f(P)$,

  * •

the unit is
$\eta^{\operatorname{\mathcal{D\mkern-3.0mun}}}(x)=\operatorname{\downarrow}\\{x\\}$,

  * •

the multiplication is $\mu^{\operatorname{\mathcal{D\mkern-3.0mun}}}(S)=\cup
S$.

The reason of the reversion of the order for the inclusion can be understood
with the two following diagrams:
$x$$y$ $y$$x$
On the leftmost, $x\leq y$ but $\uparrow x\supseteq\uparrow y$, whereas on the
rightmost $x\leq y$ and $\uparrow x\subseteq\uparrow y$.

####

Note that the $\operatorname{\mathcal{U\mkern-3.0mup}}$ functor is of type
$\operatorname{\mathcal{U\mkern-3.0mup}}:
\operatorname{\mathbf{Poset}}\to\operatorname{\mathbf{Poset}}$, so the functor
$\tilde{\operatorname{\mathcal{U\mkern-3.0mup}}}$ that we use in the
definition of alternating automata is really just
$\mathcal{U}\circ\operatorname{\mathcal{U\mkern-3.0mup}}$.

We also have a relation between $\operatorname{\mathcal{D\mkern-3.0mun}}$,
$\operatorname{\mathcal{O}}$ and $\mathcal{P}$:

######  Proposition 4.2 (Downwards closed sets of a discrete order).

We have the equality

$\operatorname{\mathcal{D\mkern-3.0mun}}\circ\operatorname{\mathcal{O}}=\mathcal{P}$

######  Proof.

Take a set $X$. By definition of $\operatorname{\mathcal{D\mkern-3.0mun}}$, it
holds that
$\operatorname{\mathcal{D\mkern-3.0mun}}\circ\operatorname{\mathcal{O}}(X)$ is
a subset of $\mathcal{P}(X)$, ordered by inclusion. So we only need to show
that any subset of $X$ is a downwards closed set of
$\operatorname{\mathcal{O}}(X)$. Now, take $P$ a subset of $X$, $x$ and $y$
elements of $X$ and suppose $x\in P$. Because of the definition of the
discrete order, if $x\geq y$ then $x=y$, and so $y\in P$. So $P$ is indeed
downwards closed on $\operatorname{\mathcal{O}}(X)$.

Thus, we can now rewrite the functor
$\operatorname{\mathcal{A\mkern-3.0mult}}$ as
$\mathcal{U}\circ\operatorname{\mathcal{U\mkern-3.0mup}}\circ\operatorname{\mathcal{D\mkern-3.0mun}}\circ\operatorname{\mathcal{O}}$.
This does not seem much of an improvement, but we can now use the adjunction
$\operatorname{\mathcal{O}}\dashv\mathcal{U}$ mentioned in section 2.2 and the
monadic composition of $\operatorname{\mathcal{U\mkern-3.0mup}}$ and
$\operatorname{\mathcal{D\mkern-3.0mun}}$ to turn
$\operatorname{\mathcal{A\mkern-3.0mult}}$ into a monad. But first, we need a
last ingredient. This is the distributive law we have been advertising
throughout the paper. It has not been created for this paper, although tracing
it back is hard to do. In our case, we found its description in [12, p.
220-221].

######  Theorem 4.3 (Distributive law).

The following
$\lambda:\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\Rightarrow}\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{D\mkern-3.0mun}}$
is a distributive law between monads:

$\begin{array}[]{rccl}\lambda_{X}:&\operatorname{\mathcal{D\mkern-3.0mun}}(\operatorname{\mathcal{U\mkern-3.0mup}}(X))&\to&\operatorname{\mathcal{U\mkern-3.0mup}}(\operatorname{\mathcal{D\mkern-3.0mun}}(X))\\\
&S&\mapsto&\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}(X)\mid\forall\>s\in
S,\ s\cap T\neq\emptyset\\}\end{array}$

This transformation is similar to the way one transforms a disjunctive normal
form into a conjunctive normal form in logic: to form a disjunction of
conjunction from a conjunction of disjunction, one makes a big disjunction of
all the different ways to pick one literal in each disjunction of the
disjunctive normal form. Here, because of the upwards and downwards closure,
at least one literal is taken rather than exactly one, but the idea is the
same. Also, the functors $\operatorname{\mathcal{U\mkern-3.0mup}}$ and
$\operatorname{\mathcal{D\mkern-3.0mun}}$ encode this logical view on the
powerset directly in the type, by making a clear difference between the monad
interpreted disjunctively and the one interpreted conjunctively.

####

Using the first proposition of this section about the composition of monads,
this distributive law yields a monad structure.

######  Corollary 4.4 (Monad structure for
$\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{D\mkern-3.0mun}}$).

The functor
$\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{D\mkern-3.0mun}}$
can be given a monad structure
$(\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{D\mkern-3.0mun}},\eta^{1},\mu^{1})$.

This distributive law is the most important element of this report: giving a
categorical semantics to alternating automata amounts to give a monad
structure to some functor (either $\mathcal{P}\mathcal{P}$ or a modified
version of it), which in turn amounts to finding a correct distributive law.
Quite a lot of errors have been made trying to define this distributive law: a
list appears in [7], itself being a correction of an error in [8], tracing
back the error to reference books such as [11]. A lot of patches have been
found, but ours is the first completely satisfactory one: it preserves the
properties of powerset (idempotency, commutativity, associativity), which was
not the case in certain attempts (for instance, the lists/languages used in
[5]), while keeping the full power of alternating automata (contrary to the
simpler version covered in [6]), and it is an actual distributive law between
monads (unlike the one proposed in [9], a corrected version of [8]).

The main idea that had not been used before is to define the distributive law
on $\operatorname{\mathbf{Poset}}$ instead of $\operatorname{\mathbf{Set}}$,
and to use the adjunction $\operatorname{\mathcal{O}}\dashv\mathcal{U}$ to
turn the obtained monad into a monad on $\operatorname{\mathbf{Set}}$.

Using another category and adjunctions to construct a correct monad structure
for alternating automata is not a new idea: an idea of how to do this (using
semi-lattices and distributive lattices) is given in [13]. We tried this
before devising our current solution, but the attempt was not successful.

####

The exact definition of the complete monad is then as follows:

######  Theorem 4.5 (Monad structure for
$\operatorname{\mathcal{A\mkern-3.0mult}}$).

Let $\eta^{2}$ (resp. $\varepsilon^{2}$) be the unit (resp. counit) of the
adjunction $\operatorname{\mathcal{O}}\dashv\mathcal{U}$. Then the functor
$\operatorname{\mathcal{A\mkern-3.0mult}}$ (equal to
$\operatorname{\widetilde{\operatorname{\mathcal{U\mkern-3.0mup}}}}\mathcal{P}$
or
$\mathcal{U}\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{O}}$)
is a monad, which unit $\eta$ has components
${\eta_{X}:\operatorname{id}_{X}}$${\mathcal{U}(\operatorname{\mathcal{O}}(X))}$${\operatorname{\mathcal{A\mkern-3.0mult}}(X)}$$\scriptstyle{\eta^{2}_{X}}$$\scriptstyle{\mathcal{U}(\eta^{1}_{\operatorname{\mathcal{O}}(X)})}$
and multiplication $\mu$ has components
${\mu_{X}:\operatorname{\mathcal{A\mkern-3.0mult}}(\operatorname{\mathcal{A\mkern-3.0mult}}(X))}$${\mathcal{U}\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{O}}(X)}$${\operatorname{\mathcal{A\mkern-3.0mult}}(X)}$$\scriptstyle{\mathcal{U}\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{D\mkern-3.0mun}}\varepsilon^{2}_{\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{O}}(X)}}$$\scriptstyle{\mathcal{U}(\mu^{1}_{\operatorname{\mathcal{O}}(X)})}$

This construction is not ad-hoc, but it comes from the link between monads and
adjunctions. See appendix A.4 for details.

One can easily compute the unit of this monad, and get

$\eta_{X}(x)=\operatorname{\uparrow}\\{x\\}=\\{T\in\mathcal{P}X\mid x\in T\\}$

For the multiplication, the computation gives the following:

$\mu_{X}(S)=\\{T\in\mathcal{P}(X)\mid\exists\>s\in S,\ \forall\>t\in s,\
\exists\>u\in t,\ \forall\>v\in u,\ v\in T\\}$

Because we constructed this multiplication stepwise, we can also give an
intuition of how it works:

  1. 1.

use $\varepsilon^{2}$ to get rid of the
$\operatorname{\mathcal{O}}\mathcal{U}$ in the middle without really modifying
the object (recall from section 2.2 that $\varepsilon^{2}$ is merely just the
identity),

  2. 2.

use the distributive law to exchange the position of
$\operatorname{\mathcal{U\mkern-3.0mup}}$ and
$\operatorname{\mathcal{D\mkern-3.0mun}}$, similarly as the transformation of
a disjunctive normal form into a conjunctive normal form,

  3. 3.

flatten two levels of $\operatorname{\mathcal{U\mkern-3.0mup}}$ into one and
two levels of $\operatorname{\mathcal{D\mkern-3.0mun}}$ into one using the
union.

###  4.3 Induced Semantics

Now that we have a monad, we need an algebra for this monad to be able to
define a semantics as in section 3.

######  Proposition 4.6 (Algebra for
$\operatorname{\mathcal{A\mkern-3.0mult}}$).

The pair $(\mathbf{2},\beta)$ where

$\begin{array}[]{rccl}\beta:&\operatorname{\mathcal{A\mkern-3.0mult}}(\mathbf{2})&\to&\mathbf{2}\\\
&S&\mapsto&\left\\{\begin{array}[]{l}\mathbf{1}\text{ if }\\{\mathbf{1}\\}\in
S\\\ \mathbf{0}\text{ otherwise}\end{array}\right.\end{array}$

is an algebra for $\operatorname{\mathcal{A\mkern-3.0mult}}$.

On a side note, one has
$\operatorname{\mathcal{A\mkern-3.0mult}}(\emptyset)=\operatorname{\widetilde{\operatorname{\mathcal{U\mkern-3.0mup}}}}(\mathcal{P}(\emptyset))=\operatorname{\widetilde{\operatorname{\mathcal{U\mkern-3.0mup}}}}(\\{\emptyset\\})=\\{\emptyset,\\{\emptyset\\}\\}=\mathbf{2}$,
and the algebra $(\mathbf{2},\beta)$ we just gave is actually
$(\operatorname{\mathcal{A\mkern-3.0mult}}(\emptyset),\mu_{\emptyset})$, which
is usually called the free algebra on $\emptyset$.

####

Given this $\beta$ and a alternating automaton $(X,\langle o,\delta\rangle)$,
there is a unique map $beh_{1}:X\to\mathbf{2}^{A^{*}}$ that makes the
following diagram commute:
${X}$${\mathbf{2}^{A^{*}}}$${\mathcal{D}(\mathbf{2}^{A^{*}})}$${\mathbf{2}\times(\operatorname{\mathcal{A\mkern-3.0mult}}(X))^{A}=\mathcal{D}(\operatorname{\mathcal{A\mkern-3.0mult}}(X))}$${\mathcal{D}(\operatorname{\mathcal{A\mkern-3.0mult}}(\mathbf{2}^{A^{*}}))}$$\scriptstyle{\operatorname{beh}_{1}}$$\scriptstyle{\langle
o{,}\delta\rangle}$$\scriptstyle{\langle
O{,}D\rangle}$$\scriptstyle{\mathcal{D}(\operatorname{\mathcal{A\mkern-3.0mult}}(\operatorname{beh}_{1}))}$$\scriptstyle{\mathcal{D}(\hat{\beta})}$

If we spell out $\hat{\beta}$, we get
$\hat{\beta}(S)(w)=\mathbf{1}\Leftrightarrow\exists\>s\in S,\ \forall\>L\in
S,\ L(w)=\mathbf{1}$, and we can translate the above diagram into two
conditions, corresponding to the first and second components of the products:

  * •

for $q\in X$, $\operatorname{beh}_{1}(q)(\operatorname{\varepsilon})=o(q)$, so
$\operatorname{beh}_{1}(q)$ accepts the empty word if and only if $o(q)$ is
$\mathbf{1}$,

  * •

for $q\in X$, $a\in A$ and $w\in A^{*}$, $\operatorname{beh}_{1}(q)(a\cdot
w)=\mathbf{1}\Leftrightarrow\exists\>F\in\delta(q)(a),\ \forall\>q^{\prime}\in
F,\ \operatorname{beh}_{1}(q^{\prime})(w)=\mathbf{1}$.

This corresponds exactly to the concrete definition of acceptance that we gave
for an alternating automaton in section 4.1! So our whole construction is
sound, as the categorical approach to alternating automata is equivalent to
the usual one.

##  5 Conclusion

Using the construction described in this report, we are finally able to fully
fit alternating automata in the large picture of determinization, and show
that the problem there was not a failure of the theory, but rather a lack of a
proper monad. A problem that we solved by finding a happy detour through order
structures.

A nice thing about this construction is that it really shows the power of
category theory: without it, formulating just the right monad would have been
really hard. But using categorical tools like distributive law and
adjunctions, breaking the problem in small, handleable pieces, and then
putting these pieces together, makes the problem reasonable.

## References

  * [1] S. Awodey  “Category Theory”  Oxford: Clarendon Press, 2006
  * [2] Falk Bartels  “On Generalised Coinduction and Probabilistic Specification Formats: Distributive Laws in Coalgebraic Modelling”, 2004
  * [3] Ashok K. Chandra, Dexter C. Kozen and Larry J. Stockmeyer  “Alternation”  In J. ACM 28.1 New York, NY, USA: ACM, 1981, pp. 114–133  DOI: 10.1145/322234.322243
  * [4] B. Jacob  “Introduction to Coalgebra”  Cambridge University Press, 2016
  * [5] Bart Jacobs  “A Bialgebraic Review of Deterministic Automata, Regular Expressions and Languages”  In Algebra, Meaning, and Computation: Essays dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday Springer Berlin Heidelberg, 2006, pp. 375–404  DOI: 10.1007/11780274_20
  * [6] Bart Jacobs, Alexandra Silva and Ana Sokolova  “Trace semantics via determinization”  In Journal of Computer and System Sciences 81.5, 2015, pp. 859–879  DOI: 10.1016/j.jcss.2014.12.005
  * [7] Bartek Klin  “An Erroneous Monad Structure On Double Covariant Powerset”, 2016
  * [8] Bartek Klin and Jurriaan Rot  “Coalgebraic Trace Semantics via Forgetful Logics”  In FOSSACS 2015, Proceedings Springer Berlin Heidelberg, 2015, pp. 151–166  DOI: 10.1007/978-3-662-46678-0_10
  * [9] Bartek Klin and Jurriaan Rot  “Coalgebraic trace semantics via forgetful logics”  In Logical Methods in Computer Science 12.4, 2016  DOI: 10.2168/LMCS-12(4:10)2016
  * [10] Sauders MacLane  “Categories For The Working Mathematician”  Springer New York, 1978
  * [11] Ernie Manes  “Monads of sets”  In Handbook of Algebra 3, 2003, pp. 67–153  DOI: 10.1016/S1570-7954(03)80059-1
  * [12] F. Marmolejo, R.D. Rosebrugh and R.J. Wood  “A basic distributive law”  In Journal of Pure and Applied Algebra 168.2, 2002, pp. 209–226  DOI: 10.1016/S0022-4049(01)00097-4
  * [13] J. Moerman  “$\mathcal{PP}$ is not a monad?!”, 2017  URL: http://joshuamoerman.nl/notes/17pp-is-not-a-monad.pdf
  * [14] Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue and Jan J… Rutten  “Generalizing determinization from automata to coalgebras”  In Logical Methods in Computer Science 9.1, 2013  DOI: 10.2168/LMCS-9(1:9)2013

##  Appendix A Proofs

Because of the reversed inclusion order used in the monad
$\operatorname{\mathcal{U\mkern-3.0mup}}(P)$, given a set of states $X$
ordered with some order $\leq$ and a subset $P$ of $X$, we need to make a
difference between the upwards (resp. downwards) closure of $P$ with respect
to $\leq$, and the upwards (resp. downwards) closure of $P$ with respect to
the usual inclusion order. We will use the arrows $\operatorname{\uparrow}$
(resp. $\operatorname{\downarrow}$) for the first one, and
$\operatorname{\upharpoonleft}$ (resp. $\operatorname{\downharpoonleft}$) for
the second.

Also, we will write $\left\\{x\in S\mid P(x)\right\\}$ for the set of elements
of $S$ having the property $P$ and $\left\\{f(s),s\in S\right\\}$ for the set
$\left\\{x\in T\mid\exists\>s\in S,\ t=f(s)\right\\}$ if $T$ is the codomain
of $f$.

Finally, to avoid confusion due to the many levels of intricate sets, we will
write $f_{*}$ for the direct image, that is $f_{*}(S)=\left\\{f(s),s\in
S\right\\}$.

###  A.1 Preliminary Order Lemmas

######  Lemma A.1 (Downwards closure and union).

Given a set of sets $S$, we have $\cup\operatorname{\downharpoonleft}S=\cup
S$.

######  Lemma A.2 (Order closure and direct image).

Given two posets $(X,\leq)$ and $(Y,\preceq)$, a monotone map $f: X\to Y$ and
a set $P\subseteq X$, we have
$\operatorname{\uparrow}f_{*}(\operatorname{\uparrow}P)=\operatorname{\uparrow}f_{*}(P)$,
and similarly
$\operatorname{\downarrow}f_{*}(\operatorname{\downarrow}P)=\operatorname{\downarrow}f_{*}(P)$.

######  Lemma A.3 (Upwards closure and intersection).

If $S$ is a set of sets and $t$ is a set, then
$\forall\>s\in\operatorname{\upharpoonleft}S,\ t\cap s\neq\emptyset$ is
equivalent to $\forall\>s\in S,\ t\cap s\neq\emptyset$.

###  A.2 Monad Structure of $\operatorname{\mathcal{U\mkern-3.0mup}}$ and
$\operatorname{\mathcal{D\mkern-3.0mun}}$

######  Proposition A.4 (Upset monad).

The triple
$(\operatorname{\mathcal{U\mkern-3.0mup}},\eta^{\operatorname{\mathcal{U\mkern-3.0mup}}},\mu^{\operatorname{\mathcal{U\mkern-3.0mup}}})$,
defined as follows:

  * •

on objects, $\operatorname{\mathcal{U\mkern-3.0mup}}((X\leq))$ is the set of
upwards closed sets of $X$, ordered by reversed inclusion order, that is
$\operatorname{\mathcal{U\mkern-3.0mup}}((X,\leq))=(\left\\{P\subseteq
X\mid\forall\>x,y\in X,\ x\leq y\wedge x\in P\Rightarrow y\in
P\right\\},\supseteq)$,

  * •

on arrows,
$\operatorname{\mathcal{U\mkern-3.0mup}}(f)(P)=\operatorname{\uparrow}f_{*}(P)$,

  * •

the unit is
$\eta^{\operatorname{\mathcal{U\mkern-3.0mup}}}(x)=\operatorname{\uparrow}\left\\{x\right\\}$,

  * •

the multiplication is $\mu^{\operatorname{\mathcal{U\mkern-3.0mup}}}(S)=\cup
S$,

is a monad.

######  Proof.

In this proof we write $\eta$ for
$\eta^{\operatorname{\mathcal{U\mkern-3.0mup}}}$ and $\mu$ for
$\mu^{\operatorname{\mathcal{U\mkern-3.0mup}}}$.

First, we need to prove that $\operatorname{\mathcal{U\mkern-3.0mup}}$ is a
functor. Since direct image and upwards closure preserve inclusion, if $f:X\to
Y$ is an arrow in $\operatorname{\mathbf{Poset}}$, then
$\operatorname{\mathcal{U\mkern-3.0mup}}(f)$ is monotone, and so it is an
arrow
$\operatorname{\mathcal{U\mkern-3.0mup}}(X)\to\operatorname{\mathcal{U\mkern-3.0mup}}(Y)$.
Checking that $\operatorname{\mathcal{U\mkern-3.0mup}}$ preserves identity is
easy. Finally, if $f$ and $g$ are two arrows with the correct types,
$\operatorname{\uparrow}g_{*}(\operatorname{\uparrow}f_{*}(S))=\operatorname{\uparrow}g_{*}(f_{*}(S))=\operatorname{\uparrow}(g\circ
f)_{*}(S)$, using lemma A.2.

Next, the unit. The upwards closure of the image by $\eta$ is obvious. Next,
suppose $(X,\leq)$ is a poset, and $x,y\in X$ are such that $x\leq y$. Then
$y\in\operatorname{\uparrow}\left\\{x\right\\}$, so
$\operatorname{\uparrow}\left\\{y\right\\}\subseteq\operatorname{\uparrow}\left\\{x\right\\}$,
and so $\eta_{(X,\leq)}(x)\supseteq\eta_{(X,\leq)}(y)$. But because
$\operatorname{\mathcal{U\mkern-3.0mup}}(X)$ is ordered with respect to the
reversed inclusion order, $\eta_{(X,\leq)}$ is monotone, and it is an arrow
$\eta_{P}:P\to\operatorname{\mathcal{U\mkern-3.0mup}}(P)$. To prove the
naturality, we need to show
$\operatorname{\uparrow}f_{*}(\operatorname{\uparrow}\left\\{x\right\\})=\operatorname{\uparrow}\left\\{f(x)\right\\}$.
But using lemma A.2, we have
$\operatorname{\uparrow}f_{*}(\operatorname{\uparrow}\left\\{x\right\\})=\operatorname{\uparrow}f_{*}(\left\\{x\right\\})$
and since $f_{*}(\left\\{x\right\\})=\left\\{f(x)\right\\}$, we have
naturality of $\eta$.

Now, the multiplication. Any union of upwards closed sets is upwards closed,
and if $S\subseteq S^{\prime}$ then $\cup S\subseteq(\cup
S)\cup(\cup(S^{\prime}\backslash S))=\cup S^{\prime}$ so $\mu_{P}$ is an arrow
$\mu_{P}:\operatorname{\mathcal{U\mkern-3.0mup}}(\operatorname{\mathcal{U\mkern-3.0mup}}(P))\to\operatorname{\mathcal{U\mkern-3.0mup}}(P)$.
For naturality, we need to prove
$\cup(\operatorname{\uparrow}\left\\{\operatorname{\uparrow}f_{*}(s),s\in
S\right\\})=\operatorname{\uparrow}f_{*}(\cup S)$. Now because of the reversed
order on $\operatorname{\mathcal{U\mkern-3.0mup}}(P)$, we have
$\cup(\operatorname{\uparrow}\left\\{\operatorname{\uparrow}f_{*}(s),s\in
S\right\\})=\cup(\operatorname{\downharpoonleft}\left\\{\operatorname{\uparrow}f_{*}(s),s\in
S\right\\})$, and using lemma A.1, we deduce

$\displaystyle\cup(\operatorname{\uparrow}\left\\{\operatorname{\uparrow}f_{*}(s),s\in
S\right\\})$ $\displaystyle=\cup\left\\{\operatorname{\uparrow}f_{*}(s),s\in
S\right\\}$
$\displaystyle=\cup\left\\{\operatorname{\uparrow}\left\\{f(x),x\in
s\right\\},s\in S\right\\}$
$\displaystyle=\left\\{\operatorname{\uparrow}f(x),x\in\cup S\right\\}\text{
because $x\in s\in S\Leftrightarrow x\in\cup S$}$

and so $\mu$ is natural.

Next, the multiplication and unit are compatible, because
$\mu_{X}\circ\eta_{\operatorname{\mathcal{U\mkern-3.0mup}}(X)}(S)=\cup\operatorname{\uparrow}\left\\{S\right\\}=\cup\operatorname{\downharpoonleft}\left\\{S\right\\}=S$
and
$\mu_{X}\circ\operatorname{\mathcal{U\mkern-3.0mup}}(\eta_{X})(S)=\cup_{s\in
S}(\operatorname{\uparrow}\left\\{s\right\\})$, so
$x\in\mu\circ\operatorname{\mathcal{U\mkern-3.0mup}}(\eta_{X})(S)$ if and only
if $\exists\>s\in S,\ x\geq s$, that is if and only if
$x\in\operatorname{\uparrow}S$. But since $S$ is an upset,
$\operatorname{\uparrow}S=S$. So we indeed have

${\operatorname{\mathcal{U\mkern-3.0mup}}X}$${\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{U\mkern-3.0mup}}X}$${\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{U\mkern-3.0mup}}X}$${\operatorname{\mathcal{U\mkern-3.0mup}}(X)}$$\scriptstyle{\eta_{\operatorname{\mathcal{U\mkern-3.0mup}}X}}$$\scriptstyle{\operatorname{\mathcal{U\mkern-3.0mup}}(\eta_{X})}$$\scriptstyle{\mu_{X}}$$\scriptstyle{\mu_{X}}$

Finally the diagram
${\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{U\mkern-3.0mup}}X}$${\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{U\mkern-3.0mup}}X}$${\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{U\mkern-3.0mup}}X}$${\operatorname{\mathcal{U\mkern-3.0mup}}X}$$\scriptstyle{\operatorname{\mathcal{U\mkern-3.0mup}}(\mu_{X})}$$\scriptstyle{\mu_{\operatorname{\mathcal{U\mkern-3.0mup}}X}}$$\scriptstyle{\mu_{X}}$$\scriptstyle{\mu_{X}}$
is easy to deduce, as

$\displaystyle\cup\operatorname{\uparrow}\left\\{\cup s,s\in S\right\\}$
$\displaystyle=\cup\operatorname{\downharpoonleft}\left\\{\cup s,s\in
S\right\\}$ $\displaystyle=\cup\left\\{\cup s,s\in S\right\\}$
$\displaystyle=\left\\{x\in X\mid\exists\>s\in S,\ \exists\>t\in s,\ x\in
t\right\\}$ $\displaystyle=\cup\cup S$

######  Proposition A.5 (Downset monad).

The triple
$(\operatorname{\mathcal{D\mkern-3.0mun}},\eta^{\operatorname{\mathcal{D\mkern-3.0mun}}},\mu^{\operatorname{\mathcal{D\mkern-3.0mun}}})$,
defined as follows:

  * •

on objects, $\operatorname{\mathcal{D\mkern-3.0mun}}(X)$ is the set of
downwards closed sets of $X$, ordered by inclusion order, that is
$\operatorname{\mathcal{D\mkern-3.0mun}}(X)=(\left\\{P\subseteq
X\mid\forall\>x,y\in X,\ x\geq y\wedge x\in P\Rightarrow y\in
P\right\\},\subseteq)$,

  * •

on arrows,
$\operatorname{\mathcal{D\mkern-3.0mun}}(f)(P)=\operatorname{\downarrow}f_{*}(P)$,

  * •

the unit is
$\eta^{\operatorname{\mathcal{D\mkern-3.0mun}}}(x)=\operatorname{\downarrow}\left\\{x\right\\}$,

  * •

the multiplication is $\mu^{\operatorname{\mathcal{D\mkern-3.0mun}}}(S)=\cup
S$,

is a monad.

######  Proof.

The proof is extremely similar to the one for
$\operatorname{\mathcal{U\mkern-3.0mup}}$, so we will not repeat it. The only
thing to note is that every time we transformed a $\operatorname{\uparrow}$
into a $\operatorname{\downharpoonleft}$ in the previous proof, in the case of
$\operatorname{\mathcal{D\mkern-3.0mun}}$ we would get a
$\operatorname{\downarrow}$ on a set ordered by regular inclusion, so it would
also translate into $\operatorname{\downharpoonleft}$.

###  A.3 Naturality Of The Distributive Law

######  Theorem A.6 (Distributive law).

The following
$\lambda:\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\Rightarrow}\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{D\mkern-3.0mun}}$
is a distributive law between monads:

$\begin{array}[]{rccl}\lambda_{X}:&\operatorname{\mathcal{D\mkern-3.0mun}}(\operatorname{\mathcal{U\mkern-3.0mup}}(X))&\to&\operatorname{\mathcal{U\mkern-3.0mup}}(\operatorname{\mathcal{D\mkern-3.0mun}}(X))\\\
&S&\mapsto&\left\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}(X)\mid\forall\>s\in
S,\ s\cap T\neq\emptyset\right\\}\end{array}$

######  Proof.

First, $\lambda$ is well defined because
$\left\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}(X)\mid\forall\>s\in S,\
s\cap T\neq\emptyset\right\\}$ is an upset of downsets.

Next, we prove naturality. Take $X,Y$ posets and $f:X\to Y$ and arrow in
$\operatorname{\mathbf{Poset}}$. We need to prove the following diagram:
${\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{U\mkern-3.0mup}}X}$${\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{D\mkern-3.0mun}}X}$${\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{U\mkern-3.0mup}}Y}$${\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{D\mkern-3.0mun}}Y}$$\scriptstyle{\lambda_{X}}$$\scriptstyle{\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{U\mkern-3.0mup}}f}$$\scriptstyle{\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{D\mkern-3.0mun}}f}$$\scriptstyle{\lambda_{Y}}$
Take
$S\in\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{U\mkern-3.0mup}}X$
and $d\in\operatorname{\mathcal{D\mkern-3.0mun}}Y$. First, we rewrite the
lower triangle:

$\displaystyle
d\in\lambda_{Y}\circ\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{U\mkern-3.0mup}}(f)(S)$
$\displaystyle\Leftrightarrow\forall\>u\in\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{U\mkern-3.0mup}}f(S),\
u\cap d=\emptyset$
$\displaystyle\Leftrightarrow\forall\>u\in\operatorname{\downarrow}\left\\{\operatorname{\uparrow}f_{*}(s),s\in
S\right\\},\ u\cap d\neq\emptyset$
$\displaystyle\Leftrightarrow\forall\>u\in\operatorname{\upharpoonleft}\left\\{\operatorname{\uparrow}f_{*}(s),s\in
S\right\\},\ u\cap d\neq\emptyset$
$\displaystyle\Leftrightarrow\forall\>u\in\left\\{\operatorname{\uparrow}f_{*}(s),s\in
S\right\\},\ u\cap d\neq\emptyset\text{ by lemma~{}\ref{closint}}$
$\displaystyle\Leftrightarrow\forall\>s\in S,\
d\cap\operatorname{\uparrow}f_{*}(s)\neq\emptyset$
$\displaystyle\Leftrightarrow\forall\>s\in S,\ d\cap
f_{*}(s)\neq\emptyset\text{ because $d$ is a downwards closed set}$
$\displaystyle\Leftrightarrow\forall\>s\in S,\ \exists\>x\in s,\ f(x)\in d$

Now the upper triangle, we obtain:

$\displaystyle
d\in\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{D\mkern-3.0mun}}(f)\circ\lambda_{X}(S)$
$\displaystyle\Leftrightarrow
d\in\operatorname{\uparrow}\left\\{\operatorname{\downarrow}f_{*}(t),t\in\lambda_{X}(S)\right\\}$
$\displaystyle\Leftrightarrow\exists\>d^{\prime}\in\operatorname{\mathcal{D\mkern-3.0mun}}Y,\
d\geq d^{\prime}\wedge\exists\>t\in\lambda_{X}(S),\
d^{\prime}=\operatorname{\downarrow}f_{*}(t)$
$\displaystyle\Leftrightarrow\exists\>t\in\operatorname{\mathcal{D\mkern-3.0mun}}X,\
(\forall\>s\in S,\ t\cap
s\neq\emptyset)\wedge(d\geq\operatorname{\downarrow}f_{*}(t))$
$\displaystyle\Leftrightarrow\exists\>t\in\operatorname{\mathcal{D\mkern-3.0mun}}X,\
(\forall\>s\in S,\ t\cap
s\neq\emptyset)\wedge(d\supseteq\operatorname{\downarrow}f_{*}(t))$
$\displaystyle\Leftrightarrow\exists\>t\in\operatorname{\mathcal{D\mkern-3.0mun}}X,\
(\forall\>s\in S,\ t\cap s\neq\emptyset)\wedge(f_{*}(t)\subseteq d)\text{
because $d$ is a downset}$
$\displaystyle\Leftrightarrow\exists\>t\in\operatorname{\mathcal{D\mkern-3.0mun}}X,\
(\forall\>s\in S,\ t\cap s\neq\emptyset)\wedge(\forall\>x\in t,\ f(x)\in d)$

Now suppose $\exists\>t\in\operatorname{\mathcal{D\mkern-3.0mun}}X,\
(\forall\>s\in S,\ t\cap s\neq\emptyset)\wedge(\forall\>x\in t,\ f(x)\in d)$.
Then given $s\in S$, there is some $x_{s}\in t\cap s$, but then $f(x_{s})\in
d$, and so $\forall\>s\in S,\ \exists\>x\in s,\ f(x)\in d$. Conversely,
suppose $\forall\>s\in S,\ \exists\>x\in s,\ f(x)\in d$. For each $s\in S$ fix
some $x_{s}\in s$ such that $f(x_{s})\in d$, and define
$t=\operatorname{\downarrow}\left\\{x_{s},s\in S\right\\}$. Then by
construction $t\in\operatorname{\mathcal{D\mkern-3.0mun}}X$, and moreover
$\forall\>s\in S,\ t\cap s\supseteq\left\\{x_{s}\right\\}\supsetneq\emptyset$.
Also, if $x\in t$, then take some $s\in S$ such that $x\leq x_{s}$. Then
$f(x)\leq f(x_{s})\in d$, and because $d$ is a downwards closed set, $f(x)\in
d$. Thus, $\exists\>t\in\operatorname{\mathcal{D\mkern-3.0mun}}X,\
(\forall\>s\in S,\ t\cap s\neq\emptyset)\wedge(\forall\>x\in t,\ f(x)\in d)$.
In the end
$d\in\lambda_{Y}\circ\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{U\mkern-3.0mup}}(f)(S)\Leftrightarrow
d\in\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{D\mkern-3.0mun}}(f)\circ\lambda_{X}(S)$
and so the diagram commutes.

####

Next, the first triangle diagram, namely
${\operatorname{\mathcal{U\mkern-3.0mup}}X}$${\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{U\mkern-3.0mup}}X}$${\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{D\mkern-3.0mun}}X}$$\scriptstyle{\eta^{\operatorname{\mathcal{D\mkern-3.0mun}}}_{\operatorname{\mathcal{U\mkern-3.0mup}}X}}$$\scriptstyle{\operatorname{\mathcal{U\mkern-3.0mup}}(\eta^{\operatorname{\mathcal{D\mkern-3.0mun}}}_{X})}$$\scriptstyle{\lambda_{X}}$
Take $S\in\operatorname{\mathcal{U\mkern-3.0mup}}X$, we have one one hand

$\displaystyle\operatorname{\mathcal{U\mkern-3.0mup}}(\eta^{\operatorname{\mathcal{D\mkern-3.0mun}}}_{X})(S)$
$\displaystyle=\operatorname{\uparrow}\left\\{\operatorname{\downarrow}s,s\in
S\right\\}$
$\displaystyle=\left\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}X\mid\exists\>s\in
S,\ \operatorname{\downarrow}s\subseteq T\right\\}$
$\displaystyle=\left\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}X\mid\exists\>s\in
S,\ s\in T\right\\}\text{ because $T$ is a downwards closed set}$
$\displaystyle=\left\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}X\mid T\cap
S\neq\emptyset\right\\}$

On the other hand,

$\displaystyle\lambda_{X}\circ\eta^{\operatorname{\mathcal{D\mkern-3.0mun}}}_{\operatorname{\mathcal{U\mkern-3.0mup}}X}(S)$
$\displaystyle=\left\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}X\mid\forall\>s\in\eta^{\operatorname{\mathcal{D\mkern-3.0mun}}}_{\operatorname{\mathcal{U\mkern-3.0mup}}X}(S),\
s\cap T\neq\emptyset\right\\}$
$\displaystyle=\left\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}X\mid\forall\>s\in\operatorname{\downarrow}\left\\{S\right\\},\
s\cap T\neq\emptyset\right\\}$
$\displaystyle=\left\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}X\mid\forall\>s\in\operatorname{\upharpoonleft}\left\\{S\right\\},\
s\cap T\neq\emptyset\right\\}$
$\displaystyle=\left\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}X\mid\forall\>s\in\left\\{S\right\\},\
s\cap T\neq\emptyset\right\\}\text{ by lemma~{}\ref{closint}}$
$\displaystyle=\left\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}X\mid S\cap
T\neq\emptyset\right\\}$

and so the diagram commutes.

####

The second triangle diagram is:
${\operatorname{\mathcal{D\mkern-3.0mun}}X}$${\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{U\mkern-3.0mup}}X}$${\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{D\mkern-3.0mun}}X}$$\scriptstyle{\eta^{\operatorname{\mathcal{U\mkern-3.0mup}}}_{\operatorname{\mathcal{D\mkern-3.0mun}}X}}$$\scriptstyle{\operatorname{\mathcal{D\mkern-3.0mun}}(\eta^{\operatorname{\mathcal{U\mkern-3.0mup}}}_{X})}$$\scriptstyle{\lambda_{X}}$
Take $S\in\operatorname{\mathcal{D\mkern-3.0mun}}X$, we have on one hand

$\displaystyle\eta^{\operatorname{\mathcal{U\mkern-3.0mup}}}_{\operatorname{\mathcal{D\mkern-3.0mun}}X}(S)$
$\displaystyle=\operatorname{\uparrow}\left\\{S\right\\}$

On the other hand, we have

$\displaystyle\lambda_{X}\circ\operatorname{\mathcal{D\mkern-3.0mun}}(\eta^{\operatorname{\mathcal{U\mkern-3.0mup}}}_{X})(S)$
$\displaystyle=\left\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}(X)\mid\forall\>t\in\operatorname{\downarrow}\left\\{\operatorname{\uparrow}\left\\{s\right\\},s\in
S\right\\},\ T\cap t\neq\emptyset\right\\}$
$\displaystyle=\left\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}(X)\mid\forall\>t\in\operatorname{\upharpoonleft}\left\\{\operatorname{\uparrow}\left\\{s\right\\},s\in
S\right\\},\ T\cap t\neq\emptyset\right\\}$
$\displaystyle=\left\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}(X)\mid\forall\>t\in\left\\{\operatorname{\uparrow}\left\\{s\right\\},s\in
S\right\\},\ T\cap t\neq\emptyset\right\\}\text{ by lemma~{}\ref{closint}}$
$\displaystyle=\left\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}(X)\mid\forall\>s\in
S,\ T\cap\operatorname{\uparrow}\left\\{s\right\\}\neq\emptyset\right\\}$
$\displaystyle=\left\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}(X)\mid\forall\>s\in
S,\ s\in T\right\\}\text{ because $T$ is a downset}$
$\displaystyle=\left\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}(X)\mid
S\subseteq T\right\\}$ $\displaystyle=\operatorname{\uparrow}\\{S\\}$

And so this triangle diagram commutes as well.

####

Now, the first rectangle diagram, that is
${\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{U\mkern-3.0mup}}X}$${\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{D\mkern-3.0mun}}X}$${\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{D\mkern-3.0mun}}X}$${\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{U\mkern-3.0mup}}X}$${\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{D\mkern-3.0mun}}X}$$\scriptstyle{\operatorname{\mathcal{D\mkern-3.0mun}}(\lambda_{X})}$$\scriptstyle{\mu^{\operatorname{\mathcal{D\mkern-3.0mun}}}_{\operatorname{\mathcal{U\mkern-3.0mup}}X}}$$\scriptstyle{\lambda_{\operatorname{\mathcal{D\mkern-3.0mun}}X}}$$\scriptstyle{\operatorname{\mathcal{U\mkern-3.0mup}}(\mu^{\operatorname{\mathcal{D\mkern-3.0mun}}}_{X})}$$\scriptstyle{\lambda_{X}}$
Take
$S\in\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{U\mkern-3.0mup}}X$,
on one hand we have

$\displaystyle\lambda_{X}\circ\mu^{\operatorname{\mathcal{D\mkern-3.0mun}}}_{\operatorname{\mathcal{U\mkern-3.0mup}}X}(S)$
$\displaystyle=\left\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}X\mid\forall\>s\in\cup
S,\ ,s\cap T\neq\emptyset\right\\}$
$\displaystyle=\left\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}X\mid\forall\>s\in
S,\ \forall\>t\in s,\ t\cap T\neq\emptyset\right\\}$

On the other hand, we have

$\displaystyle\operatorname{\mathcal{U\mkern-3.0mup}}(\mu^{\operatorname{\mathcal{D\mkern-3.0mun}}}_{X})\circ\lambda_{\operatorname{\mathcal{D\mkern-3.0mun}}X}\circ\operatorname{\mathcal{D\mkern-3.0mun}}(\lambda_{X})(S)$
$\displaystyle=\operatorname{\uparrow}\left\\{\cup
T,T\in\lambda_{\operatorname{\mathcal{D\mkern-3.0mun}}X}(\operatorname{\mathcal{D\mkern-3.0mun}}(\lambda_{X})(S))\right\\}$
$\displaystyle=\operatorname{\uparrow}\left\\{\cup
T,T\in\left\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{D\mkern-3.0mun}}X\mid\forall\>s\in\operatorname{\mathcal{D\mkern-3.0mun}}(\lambda_{X})(S),\
s\cap T\neq\emptyset\right\\}\right\\}$
$\displaystyle=\operatorname{\uparrow}\left\\{\cup
T,T\in\left\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{D\mkern-3.0mun}}X\mid\forall\>s\in\operatorname{\downarrow}(\lambda_{X})_{*}(S),\
s\cap T\neq\emptyset\right\\}\right\\}$
$\displaystyle=\operatorname{\uparrow}\left\\{\cup
T,T\in\left\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{D\mkern-3.0mun}}X\mid\forall\>s\in\operatorname{\upharpoonleft}(\lambda_{X})_{*}(S),\
s\cap T\neq\emptyset\right\\}\right\\}$
$\displaystyle=\operatorname{\uparrow}\left\\{\cup
T,T\in\left\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{D\mkern-3.0mun}}X\mid\forall\>s\in(\lambda_{X})_{*}(S),\
s\cap T\neq\emptyset\right\\}\right\\}\text{ by lemma~{}\ref{closint}}$
$\displaystyle=\operatorname{\uparrow}\left\\{\cup
T,T\in\left\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{D\mkern-3.0mun}}X\mid\forall\>s\in
S,\ \lambda_{X}(s)\cap T\neq\emptyset\right\\}\right\\}$
$\displaystyle=\operatorname{\uparrow}\left\\{\cup
T,T\in\left\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{D\mkern-3.0mun}}X\mid\forall\>s\in
S,\ T\cap\left\\{u\in\operatorname{\mathcal{D\mkern-3.0mun}}X\mid\forall\>t\in
s,\ t\cap u\neq\emptyset\right\\}\neq\emptyset\right\\}\right\\}$
$\displaystyle=\operatorname{\uparrow}\left\\{\cup
T,T\in\left\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{D\mkern-3.0mun}}X\mid\forall\>s\in
S,\ \exists\>u\in T,\ \forall\>t\in s,\ t\cap
u\neq\emptyset\right\\}\right\\}$

Take $T\in\operatorname{\mathcal{D\mkern-3.0mun}}X$ and suppose
$T\in\lambda_{X}\circ\mu^{\operatorname{\mathcal{D\mkern-3.0mun}}}_{\operatorname{\mathcal{U\mkern-3.0mup}}X}(S)$,
that is

$\forall\>s\in S,\ \forall\>t\in s,\ t\cap T\neq\emptyset$

Then we have

$\forall\>s\in S,\
\exists\>u\in(\operatorname{\downharpoonleft}\left\\{T\right\\}),\
\forall\>t\in s,\ t\cap u\neq\emptyset$

with $u$ taken each time to be $T$. But
$\operatorname{\downharpoonleft}\left\\{T\right\\}$ is a downset, thus,
$\operatorname{\downharpoonleft}\left\\{T\right\\}\in\left\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{D\mkern-3.0mun}}X\mid\forall\>s\in
S,\ \exists\>u\in T,\ \forall\>t\in s,\ t\cap u\neq\emptyset\right\\}$. Since
$T=\cup\operatorname{\downharpoonleft}\left\\{T\right\\}$, we deduce that
$T\in\operatorname{\mathcal{U\mkern-3.0mup}}(\mu^{\operatorname{\mathcal{D\mkern-3.0mun}}}_{X})\circ\lambda_{\operatorname{\mathcal{D\mkern-3.0mun}}X}\circ\operatorname{\mathcal{D\mkern-3.0mun}}(\lambda_{X})(S)$.

Conversely, take
$T\in\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{D\mkern-3.0mun}}X$
such that $\forall\>s\in S,\ \exists\>u\in T,\ \forall\>t\in s,\ t\cap
u\neq\emptyset$, and take $s\in S$. By hypothesis, take $u_{s}\in T$ such that
$\forall\>t\in s,\ t\cap u_{s}\neq\emptyset$. Take some $t\in s$, we have
$t\cap\cup T\supseteq t\cap u_{s}\supsetneq\emptyset$, and so $t\cap\cup
T\neq\emptyset$. This proves $\cup
T\in\lambda_{X}\circ\mu^{\operatorname{\mathcal{D\mkern-3.0mun}}}_{\operatorname{\mathcal{U\mkern-3.0mup}}X}(S)$.
Because the set
$\lambda_{X}\circ\mu^{\operatorname{\mathcal{D\mkern-3.0mun}}}_{\operatorname{\mathcal{U\mkern-3.0mup}}X}(S)$
is an upwards closed set, for any $T^{\prime}\geq T$ we still have
$T^{\prime}\in\lambda_{X}\circ\mu^{\operatorname{\mathcal{D\mkern-3.0mun}}}_{\operatorname{\mathcal{U\mkern-3.0mup}}X}(S)$.
Thus, we have
$\operatorname{\mathcal{U\mkern-3.0mup}}(\mu^{\operatorname{\mathcal{D\mkern-3.0mun}}}_{X})\circ\lambda_{\operatorname{\mathcal{D\mkern-3.0mun}}X}\circ\operatorname{\mathcal{D\mkern-3.0mun}}(\lambda_{X})(S)\subseteq\lambda_{X}\circ\mu^{\operatorname{\mathcal{D\mkern-3.0mun}}}_{\operatorname{\mathcal{U\mkern-3.0mup}}X}(S)$.

The double inclusion proves the equality, and so the diagram commutes.

####

Finally, the last diagram to prove is
${\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{U\mkern-3.0mup}}X}$${\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{U\mkern-3.0mup}}X}$${\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{D\mkern-3.0mun}}X}$${\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{U\mkern-3.0mup}}X}$${\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{D\mkern-3.0mun}}X}$$\scriptstyle{\lambda_{\operatorname{\mathcal{U\mkern-3.0mup}}X}}$$\scriptstyle{\operatorname{\mathcal{D\mkern-3.0mun}}(\mu^{\operatorname{\mathcal{U\mkern-3.0mup}}}_{X})}$$\scriptstyle{\operatorname{\mathcal{U\mkern-3.0mup}}(\lambda_{X})}$$\scriptstyle{\mu^{\operatorname{\mathcal{U\mkern-3.0mup}}}_{\operatorname{\mathcal{D\mkern-3.0mun}}X}}$$\scriptstyle{\lambda_{X}}$
Take
$S\in\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{U\mkern-3.0mup}}X$,
the lower part gives

$\displaystyle\lambda_{X}\circ\operatorname{\mathcal{D\mkern-3.0mun}}(\mu^{\operatorname{\mathcal{U\mkern-3.0mup}}}_{X})(S)$
$\displaystyle=\\{t\in\operatorname{\mathcal{D\mkern-3.0mun}}X\mid\forall\>u\in\operatorname{\mathcal{D\mkern-3.0mun}}(\mu^{\operatorname{\mathcal{U\mkern-3.0mup}}}_{X})(S),\
u\cap t\neq\emptyset\\}$
$\displaystyle=\\{t\in\operatorname{\mathcal{D\mkern-3.0mun}}X\mid\forall\>u\in\operatorname{\downarrow}\\{\cup
s,s\in S\\},\ u\cap t\neq\emptyset\\}$
$\displaystyle=\\{t\in\operatorname{\mathcal{D\mkern-3.0mun}}X\mid\forall\>u\in\operatorname{\upharpoonleft}\\{\cup
s,s\in S\\},\ u\cap t\neq\emptyset\\}$
$\displaystyle=\\{t\in\operatorname{\mathcal{D\mkern-3.0mun}}X\mid\forall\>u\in\\{\cup
s,s\in S\\},\ u\cap t\neq\emptyset\\}\text{ by lemma~{}\ref{closint}}$
$\displaystyle=\\{t\in\operatorname{\mathcal{D\mkern-3.0mun}}X\mid\forall\>s\in
S,\ t\cap\cup s\neq\emptyset\\}$

The upper part gives

$\displaystyle\mu^{\operatorname{\mathcal{U\mkern-3.0mup}}}_{\operatorname{\mathcal{D\mkern-3.0mun}}X}\circ\operatorname{\mathcal{U\mkern-3.0mup}}(\lambda_{X})\circ\lambda_{\operatorname{\mathcal{U\mkern-3.0mup}}X}(S)$
$\displaystyle=\cup\operatorname{\uparrow}\\{\lambda_{X}(T),T\in\lambda_{\operatorname{\mathcal{U\mkern-3.0mup}}X}(S)\\}$
$\displaystyle=\cup\operatorname{\downharpoonleft}\\{\lambda_{X}(T),T\in\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{U\mkern-3.0mup}}X\mid\forall\>s\in
S,\ T\cap s\neq\emptyset\\}$
$\displaystyle=\cup\\{\lambda_{X}(T),T\in\\{T\in\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{U\mkern-3.0mup}}X\mid\forall\>s\in
S,\ T\cap s\neq\emptyset\\}\text{ by lemma~{}\ref{closun}}$
$\displaystyle=\\{t\in\operatorname{\mathcal{D\mkern-3.0mun}}X\mid\exists\>T\in\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{U\mkern-3.0mup}}X,\
(\forall\>s\in S,\ T\cap s\neq\emptyset)\wedge(\forall\>x\in T,\ x\cap
t\neq\emptyset)\\}$

Now take $t\in\operatorname{\mathcal{D\mkern-3.0mun}}X$, and suppose
$\forall\>s\in S,\ t\cap\cup s\neq\emptyset$. For each $s\in S$, fix $y_{s}\in
s$ and $x_{s}\in y_{s}$ such that $x_{s}\in t$. Define
$T=\operatorname{\upharpoonleft}\\{y_{s},s\in
S\\}=\operatorname{\downarrow}\\{y_{s},s\in S\\}$, by definition we have
$T\in\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{U\mkern-3.0mup}}X$.
Moreover, for any $s\in S$, we have $y_{s}\in s\cap T$ and so $\forall\>s\in
S,\ T\cap s\neq\emptyset$. Also, for a given $y\in T$, there is some $s\in S$
such that $y\supseteq y_{s}$. But then $t\cap y\supseteq t\cap
y_{s}\supsetneq\emptyset$. Therefore,
$t\in\mu^{\operatorname{\mathcal{U\mkern-3.0mup}}}_{\operatorname{\mathcal{D\mkern-3.0mun}}X}\circ\operatorname{\mathcal{U\mkern-3.0mup}}(\lambda_{X})\circ\lambda_{\operatorname{\mathcal{U\mkern-3.0mup}}X}(S)$.

Conversely, take $t\in\operatorname{\mathcal{D\mkern-3.0mun}}X$ and suppose
$\exists\>T\in\operatorname{\mathcal{D\mkern-3.0mun}}\operatorname{\mathcal{D\mkern-3.0mun}}X,\
(\forall\>s\in S,\ T\cap s\neq\emptyset)\wedge(\forall\>x\in T,\ x\cap
t\neq\emptyset)$. Take such a $T$, and some $s\in S$. By hypothesis, there is
a $y_{s}\in T\cap s$, and because $y_{s}\in T$, there is some $x_{s}\in
y_{s}\cap t$. But then $x_{s}\in\cup s$, and so $t\cap\cup s\neq\emptyset$.
Thus,
$t\in\lambda_{X}\circ\operatorname{\mathcal{D\mkern-3.0mun}}(\mu^{\operatorname{\mathcal{U\mkern-3.0mup}}}_{X})(S)$.
By double inclusion, the diagram commutes.

###  A.4 Monad Structure of $\operatorname{\mathcal{A\mkern-3.0mult}}$

The construction we used to construct the monad
$\operatorname{\mathcal{A\mkern-3.0mult}}$ from a monad and an adjunction is
not ad-hoc. Instead it is a consequence of the three following facts, which
are classical results on monads and adjoints (see for instance [10, chapter 4,
6]):

######  Theorem A.7 (Monad arising from an adjunction).

Given an adjunction $\mathcal{F}\vdash\mathcal{G}$ with unit $\eta$, the
functor $\mathcal{G}\circ\mathcal{F}$ can be equipped with a monad structure,
whose unit is the unit of the adjunction.

The multiplication of the monad can also be described in term of the
adjunction, but not in a simple way, so we leave this out.

######  Proposition A.8 (Adjoints arising from a monad).

Given a monad $(\mathcal{T},\eta,\mu)$ on a category $\mathbb{C}$, the monad
arises from the following adjunction:
${\mathbb{C}}$${\bot}$${\operatorname{\mathcal{EM}}(\mathcal{T})}$$\scriptstyle{\mathcal{F}}$$\scriptstyle{\mathcal{U}}$
Where $\operatorname{\mathcal{EM}}(T)$ is the category of algebras for
$\mathcal{T}$, $\mathcal{F}(X)=(\mathcal{T}X,\mu_{X})$, $\mathcal{F}(f)=T(f)$,
$\mathcal{U}^{\prime}(X,f)=X$ and $\mathcal{U}^{\prime}(\alpha)=\alpha$.

The exact details of the two adjoint functors is not very relevant, the
important part is that the monad arising from the adjunction is $\mathcal{T}$.

######  Proposition A.9 (Composition of adjoints).

If $\mathcal{F}\dashv\mathcal{G}$ is an adjunction between $\mathbb{C}$ and
$\mathbb{D}$, with unit $\eta$ and counit $\varepsilon$ and
$\mathcal{F}^{\prime}\dashv\mathcal{G}^{\prime}$ is an adjunction between
$\mathbb{D}$ and $\mathbb{E}$ with unit $\eta^{\prime}$ and counit
$\varepsilon^{\prime}$, that is we are in the following situtation:
${\mathbb{C}}$${\bot}$${\mathbb{D}}$${\bot}$${\mathbb{E}}$$\scriptstyle{\mathcal{F}}$$\scriptstyle{\mathcal{G}}$$\scriptstyle{\mathcal{F}^{\prime}}$$\scriptstyle{\mathcal{G}^{\prime}}$
then
$\mathcal{F}^{\prime}\circ\mathcal{F}\dashv\mathcal{G}\circ\mathcal{G}^{\prime}$
is an adjunction between $\mathbb{C}$ and $\mathbb{E}$, with unit

$\eta^{\prime\prime}:\operatorname{id}_{\mathbb{C}}\stackrel{{\scriptstyle\eta}}{{\operatorname{\Rightarrow}}}\mathcal{G}\circ\mathcal{F}\stackrel{{\scriptstyle\mathcal{G}\eta^{\prime}\mathcal{F}}}{{\operatorname{\Rightarrow}}}\mathcal{G}\mathcal{G}^{\prime}\mathcal{F}^{\prime}\mathcal{F}$

and counit

$\mu^{\prime\prime}:\mathcal{F}^{\prime}\mathcal{F}\mathcal{G}\mathcal{G}^{\prime}\stackrel{{\scriptstyle\mathcal{F}^{\prime}\varepsilon\mathcal{G}^{\prime}}}{{\operatorname{\Rightarrow}}}\mathcal{F}^{\prime}\mathcal{G}^{\prime}\stackrel{{\scriptstyle\varepsilon^{\prime}}}{{\operatorname{\Rightarrow}}}\operatorname{id}_{\mathbb{E}}$

Now the monadic structure for $\operatorname{\mathcal{A\mkern-3.0mult}}$ can
be constructed in three steps:

  1. 1.

from
$\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{D\mkern-3.0mun}}$
get an adjunction
${\operatorname{\mathbf{Poset}}}$${\bot}$${\operatorname{\mathcal{EM}}(\operatorname{\mathcal{U\mkern-3.0mup}}\operatorname{\mathcal{D\mkern-3.0mun}})}$$\scriptstyle{\mathcal{F}}$$\scriptstyle{\mathcal{U}^{\prime}}$
using proposition A.8

  2. 2.

compose this adjunction with
${\operatorname{\mathbf{Set}}}$${\bot}$${\operatorname{\mathbf{Poset}}}$$\scriptstyle{\operatorname{\mathcal{O}}}$$\scriptstyle{\mathcal{U}}$
using proposition A.9

  3. 3.

from this composite adjunction, get a monad on $\operatorname{\mathbf{Set}}$
using propoition A.7

And this monad on $\operatorname{\mathbf{Set}}$ is exactly the monad on
$\operatorname{\mathcal{A\mkern-3.0mult}}$ described at the end of section
4.2.

##  Appendix B Thanks

I would like to thank Jurriaan Rot for being my guide in the world of
coalgebras and pointing me again and again in the right direction, Luigi
Santocanale whom I never met in person but who still gave me the right thing
to look at for the distributive law, Joshua Moerman for his paper summing up
all the troubles people have had on the same problem as me before, and
Alexandre Goy, for keeping the mood up in the office.