§ INTRODUCTION

The role of category theory, algebra, and logic in deepening our understanding of semantics and algorithms in Computer Science has long been one of Samson's flagships. His seminal paper Domain Theory in Logical Form [1]  studies the connection between program logic and domain theory via Stone duality. This is an example of a fundamental duality in Computer Science between semantics, operational or denotational, and syntax, provided as a logic or specification language.

Building on Stone's celebrated representation theorems for Boolean algebras [68] and distributive lattices [69], categorical dualities linking algebra and topology [43] have been widely used in logic and theoretical computer science
[27, 19, 35]. With algebras corresponding to the syntactic, deductive side of logical systems, and topological spaces to their semantics, Stone-type dualities  provide a powerful mathematical framework for studying various properties of logical systems. More recently,  it has also been fruitfully explored in more algorithmic applications, notably in understanding minimisation of various types of automata [2, 16, 21, 20, 48, 58, 31]. Among these, [16] and [20] had striking similarities in the approach yet it was not clear whether the differences could be harmonised in a uniform way. The main aim of this paper is to find a unifying perspective on the minimisation constructions in [16] and [20]. Duality will play a central role in achieving our aim of unification of approaches, which puts us on the path forged by Samson.

In [16], the authors adopt the coalgebraic perspective on automata and use a dual equivalence between the category of coalgebras and a category of algebras to explain minimisation. The key observation is that the algebras considered provide semantics of a modal logic. This algebraic semantics is dual to coalgebraic semantics in which
logical equivalence coincides with trace equivalence.
From this coalgebra-algebra duality it follows that maximal quotients of coalgebras correspond to minimal subobjects of algebras. In order to explain the minimisation algorithm, the authors exploit duality to prove that the maximal quotient of a coalgebra can be constructed by computing
the subalgebra of definable predicates in the dual modal algebra.
The examples in [16] include partially observable DFAs, linear weighted automata viewed as
coalgebras over finite-dimensional vector spaces, and belief automata which are coalgebras on compact Hausdorff spaces.

In [20],
Brzozowski's double-reversal minimisation algorithm for deterministic finite automata
(with both initial and final states) was described categorically and its correctness  explained
via the duality between reachability and observability, whose origins trace back to seminal work of Kalman in control theory [45]. Kalman's work was extended to automata theory in a collection of papers by Arbib and Manes [9, 6, 10, 8, 7, 11, 12]. The work of [20] is closely related to these and includes generalisations of Brzozowski's algorithm to Moore
and weighted automata over commutative semirings.

The contributions of the present paper are as follows.

* A categorical framework within which minimisation algorithms can be understood and different  approaches unified (Section <ref>). We start with a comparison between the approaches in [16] and [20] (Section <ref>) and then proceed to
a general setup for different automata types based on algebra and coalgebra (Section <ref>).
Section <ref>
includes the categorical picture that unifies the work in [16] and [20]: in a nutshell, it is a stack of three interconnected adjunctions. It starts with a base dual adjunction that is subsequently lifted to a dual adjunction between coalgebras and algebras, and finally to a dual adjunction between automata.
Section <ref> extends this categorical picture place to include trace logic.
Section <ref>,
presents an abstract understanding of reachability and observability,
and finally everything is summarised and abstract minimisation algorithms are stated in Section <ref>.

* A thorough illustration of the general framework instantiated to concrete examples. In Section <ref>), we revisit a range of examples stemming from previous approaches: deterministic Kripke frames, weighted automata, and topological automata (belief automata). In Section <ref>, we include an extensive new example on alternating automata, which uses the duality of complete atomic Boolean algebras and sets.
For weighted automata, we use our framework to extend a well-known result for weighted automata over a field [65] to weighted automata over a principal ideal domain: the minimal weighted automaton over a principal ideal domain always exists, and, as expected, it has a state space smaller or equal than that of the original automaton.

We conclude the paper with a review of related work (Section <ref>).

§ PRELIMINARIES

In this section, we fix notation and recall basic definitions of coalgebras and algebras.
For a more detailed introduction to coalgebra, we refer to [60].
For general categorical notions, see e.g. [3].
We assume familiarity with classic automata such as (non)deterministic finite automata,
and Moore automata.

Categories are denoted by $\catC, \catD, \ldots$,
objects of categories by $X,Y,Z,\ldots$,
and arrows/morphisms of categories by $f,g,h,\dots$.
We denote by $\Set$ the category of sets and functions.
Let $X_1, X_2$ be in $\catC$.
The product of $X_1$ and $X_2$ (if it exists) is denoted by $X_1 \times X_2$
with projection maps $\pi_i\colon X_1 \times X_2 \to X_i$, $i=1,2$.
Similarly, their coproduct (if it exists) is written $X+Y$
with coprojection maps $\inc_i \colon X_i \to X_1 + X+2$.
In $\Set$, $X \times Y$ and $X+Y$ are the usual constructions of cartesian product and disjoint union.
Let $X$ be an object in $\catC$ and $A$ be a set.
Assuming $\catC$ has products,
then $X^A := \prod_A X$ denotes the $A$-fold product of $X$ with itself.
Similarly, if $\catC$ has coproducts, then $A \cdot X := \coprod_A X$ denotes the $A$-fold coproduct of $X$ with itself.

The covariant powerset functor $\Pow\colon \Set\to\Set$ sends a set $X$ to its powerset $\Pow(X)$ and a function $f\colon X \to Y$ to the direct-image map $\Pow(f)\colon \Pow(X) \to \Pow(Y)$.
The contravariant powerset functor $\cPo\colon \Set\to\SetOp$ also sends a set $X$ to its powerset, now denoted $\cPo(X)$, and a function $f \colon X \to Y$ to its inverse-image map
$\cPo(f)\colon \Pow(Y) \to \Pow(X)$.

For a set $A$ of letters,
$A^*$ denotes the set of all words (i.e., finite sequences) over $A$, and $\epsilon$ the empty word; and $w_1\cdot w_2$ (and $w_1w_2$) the concatenation of words $w_1,w_2 \in A^*$.

§.§ Coalgebras, Algebras and Monads

Given an endofunctor $F \colon \catC \to\catC$,
an $F$-coalgebra is a pair $(X, \gamma\colon X\to FX)$,
where $X$ is a $\catC$-object and $\gamma\colon X\to FX$ is a $\catC$-arrow.
The functor $F$ specifies the type of the coalgebra (which may be thought of as the type of observations and transitions), and the structure map $\gamma$ specifies the dynamics.
An $F$-coalgebra morphism from an $F$-coalgebra $(X,\gamma)$ to an
$F$-coalgebra $(Y,\delta)$ is a $\catC$-arrow $h\colon X \to Y$ that preserves
the coalgebra structure, i.e., $\delta\circ h = Fh \circ \gamma$.
$F$-coalgebras and $F$-coalgebra morphisms form a category denoted by $\Coalg_\catC(F)$. A final $F$-coalgebra is a final object in $\Coalg_\catC(F)$, i.e., an $F$-coalgebra $(\Omega,\omega)$ is final if for all $T$-coalgebras $(X,\gamma)$ there is a unique $F$-coalgebra morphism $h \colon (X,c) \to (\Omega,\omega)$.

An $F$-algebra is the dual concept of an $F$-coalgebra.
An $F$-algebra is a pair $(X, \alpha)$,
where $X$ is a $\catC$-object and $\alpha\colon FX \to X$ is a $\catC$-arrow.
Now, the functor $F$ can be seen to specify the type of operations of the algebra. An $F$-algebra morphism from an $F$-algebra $(X,\alpha)$ to an
$F$-algebra $(Y,\beta)$ is a $\catC$-arrow $h\colon X \to Y$ that preserves the
algebra structure, i.e., $h\circ \alpha = \beta \circ Fh$.
$F$-algebras and $F$-algebra morphisms form a category denoted by $\Alg_\catC(F)$. An initial $F$-algebra is an initial object $(A,\alpha)$ in $\Alg_\catC(F)$, i.e., for all $F$-algebras $(X,\beta)$ there is a unique $F$-algebra morphism $h\colon (A,\alpha) \to (X,\beta)$.

A monad (on $\catC$) is a triple $(T, \eta, \mu)$ consisting of a functor
$T\colon \catC\to\catC$ and two natural transformations
$\eta\colon \Id \to T$ (the unit) and $\mu\colon TT \to T$ (the multiplication) satisfying $\mu \o \eta T = \id_T = \mu \o T\eta$ and $\mu \o T\mu = \mu \o \mu T$.
For brevity, we will sometimes refer to a monad simply by its functor part, leaving the unit and multiplication implicit.
An Eilenberg-Moore $T$-algebra for a monad $(T,\eta,\mu)$
is a $T$-algebra $(A, \alpha)$ such that $\alpha \o \eta_A = \id_A$ and
$\alpha \o \mu_A = \alpha \o T\alpha$.
Eilenberg-Moore $T$-algebras and $T$-algebra morphisms form a category denoted by $\EM{T}$.
In particular, for every $X$ in $\catC$, $(TX, \mu_X)$ is the free
Eilenberg-Moore $T$-algebra on $X$,
i. e., for every
$(A,\alpha)$ in $\EM{T}$ and
every $\catC$-arrow $f\colon X \to A$ there is a unique $T$-algebra morphism
(called the free extension of $f$) $\ext f\colon (TX,\mu_X) \to (A,\alpha)$ such that $\ext f \o \eta_X = f$.

\begin{equation}
\label{not:ext}
\vcenter{
\xymatrix{
\ar[r]^-{\mu_X}
\ar[d]_{T\ext f}
\ar[d]^{\ext f}
\ar[l]_-{\eta_X}
\ar[ld]^-f
\\
\ar[r]_-\alpha
\end{equation}

Notice also that we have $\ext f = \alpha \o Tf$.

§.§ Determinisation

Let $(T,\eta,\mu)$ be a monad on $\Set$ and
$F\colon \Set \to\Set$ a functor given by
$FX = B \times X^A$ where $A$ is a set and $B$ is the carrier of an Eilenberg-Moore $T$-algebra $(B,\beta)$.
Then $FT$-coalgebras can be seen as automata with input alphabet $A$, output in $B$ and branching structure given by $T$. For example, nondeterministic automata are $F\Pow$-coalgebras where $FX = 2 \times X^A$
and $\beta = \lor \colon \Pow{2} \to 2$ is the join (or max).
Such $FT$-coalgebras can be “determinised” using a generalisation of the classic powerset construction [67], and the result can be seen as an $F$-coalgebra in the category $\EM{T}$.
We follow [15, 41] in explaining this general construction. As shown in [41], there is a so-called distributive law $\lambda\colon TF \To FT$ of the monad $(T,\eta,\mu)$ over the functor $F$ given by

\begin{equation}
\xymatrix@C=5em{
\lambda_X \colon T (B \times X^A) \ar[r]^-{\tup{T{\pi_1},T{\pi_2}}}
& TB\times T(X^A) \ar[r]^-{\beta\times \st}
& B\times (TX)^A
\label{eq:lambda}
\end{equation}

where $\st\colon T \o (-)^A \To (-)^A \o T$ is the strength natural transformation that exists for all monads on $\Set$.
Such a distributive law $\lambda$ corresponds to a lifting of $F\colon \Set\to\Set$ to a functor $\Flam\colon \EM{T} \to \EM{T}$ [44],
and it induces a functor
$\det{(-)} \colon \Coalg_\Set(FT) \to \Coalg_{\EM{T}}(\Flam)$
which sends an $FT$-coalgebra $\gamma = \tup{o,t}\colon X \to B \times (TX)^A$
to its determinisation
$\det{\gamma} = F\mu_X \circ\lambda_{TX} \circ T\gamma$,

that is,

\begin{equation}
%\det{\gamma} = F\mu_X \circ\lambda_{TX} \circ T\gamma
\det{\gamma} =
\xymatrix{
TX \ar[r]^-{T\gamma}
& T(B \times (TX)^A) \ar[r]^-{\lambda_{TX}}
& B \times (TTX)^A \ar[r]^-{B \times (\mu_X)^A}
& B \times (TX)^A
\label{eq:det}
\end{equation}

Another perspective is that $\lambda$ induces an Eilenberg-Moore $T$-algebra structure $\alpha$ on $FTX$, and $\det{\gamma}\colon (TX,\mu_S) \to (FTX,\alpha)$ is the free extension of $\gamma$ induced by $\alpha$. This also justifies our use of the notation $\det{(-)}$.

The determinisation $\det{\gamma}$ can be seen as a Moore automaton in $\EM{T}$.
We will use the determinisation construction in order to place alternating automata and weighted automata in our general minimisation framework.

§ MINIMISATION VIA DUAL ADJUNCTIONS

§.§ Unifying Previous Approaches

One aim of this paper is to find a unifying perspective on the automata minimisation constructions in
[16] and [20].
We therefore start by summarising the two papers, and discuss the differences and similarities.

First we establish some terminology regarding key notions.
A classic DFA is reachable if all states are reachable by reading some word from the initial state,
it is observable if no two states accept the same language, and
it is minimal if it is both reachable and observable.
These notions can be generalised to other types of automata using that
automata are in a sense both algebras and coalgebras as we will explain in
Section <ref>.
We will call an algebra reachable if it has no proper subalgebras,
and a coalgebra is observable if it has no proper quotients.
A (generalised) automaton is then minimal if its algebra part is reachable and
its coalgebra part is observable.
Note that in the literature, observable coalgebras are usually called minimal coalgebras.

In [16], (generalised) Moore automata (without initial state) are modelled as coalgebras
for a functor $F = B \times (-)^\Alph$ on base categories of algebras or topological spaces.

The main observation used in [16] is that for many types of such coalgebras,
one can define a category of algebras that is dually equivalent to the category of coalgebras.
This dual equivalence can be seen as a generalisation of the Jonsson-Tarski duality known from modal logic,
which in turn arises from Stone duality.
The algebras in [16] are therefore understood as modal algebras, i.e.,
they consist of an algebra (that describes a propositional logic, e.g., Boolean logic)
expanded with the modal operators.

From this coalgebra-algebra duality it follows that maximal quotients of coalgebras
correspond to minimal subobjects of algebras.

The main contribution of [16] can then be formulated as follows:
Letting $\gamma$ be a coalgebra,
the minimal subalgebra of its dual modal algebra $\alpha$
consists of the predicates over $\gamma$ that are definable in the modal logic.
Hence to make $\gamma$ observable, compute the subalgebra of definable subsets
(which is reachable by construction), and dualise to obtain an observable coalgebra.

Although, this is not stated in [16], for classic automata
the computation of definable subsets corresponds to the partition refinement algorithm.

The minimisation-via-duality approach of [16] was shown to apply to
partially observable DFAs
(using duality of finite sets and finite Boolean algebras),
linear weighted automata
(using the self-duality of vector spaces),
and belief automata viewed as coalgebras on compact Hausdorff spaces
(using Gelfand duality).
Moreover, for each of these examples it is shown that the definable subsets are determined by the
subsets definable in the trace logic fragment consisting of formulas of the shape
$\boxmod{a_0} \cdots \boxmod{a_n}p$

In [20],
Brzozowski's double-reversal minimisation algorithm [26] for classic automata

was described categorically.
The Brzozowski algorithm works as follows.
Starting with a classic, finite (possibly nondeterministic) automaton accepting a language $\Lang$,
reverse the transitions,
swap initial and final states, and make the result deterministic using the subset construction.
This reversed automaton accepts the reversed language $\rev(\Lang)$.
Take the reachable part of the reversed automaton.
Now, do all of this again.
The result will be a reachable and observable (i.e., minimal) classic deterministic automaton accepting $\Lang$.

(In practice, one would do the subset construction and reachability on-the-fly such that only the reachable part is actually constructed,
rather than constructing the full powerset and only afterwards take the reachable part.)

The correctness of the algorithm was explained in [20]
via the duality between reachability and observability known from control theory
(cf. [45, 9, 6].
This duality arises from a dual adjunction between algebras and coalgebras,
and therefore only works in one direction,
so to speak, namely, a reachable algebra dualises to an observable coalgebra, but not vice versa.
This, however, is sufficient to formalise Brzozowski's algorithm in terms of a
dual adjunction between categories of automata (with both initial and final states).

Generalisations of the Brzozowski algorithm were then formulated in [20]
for Moore automata (over $\Set$)
and weighted automata, which include nondeterministic and linear weighted automata as instances.
More precisely, weighted automata were first determinised into
Moore automata over semimodules, and after the reverse-determinise step,
the semimodule structure is forgotten in order to take the reachable part.
Example 8.3 in [20] illustrates that one generally wants to take a
subsemimodule that spans the reachable part, but this was not fully formalised.
One aim of the present paper is to make this part precise.

We summarise the main differences and similarities.
In [16], the minimisation-via-duality approach
produces from a coalgebra (with structured state space),
an observable coalgebra of the same type.
In [20], the Brzozowski-based approach
starts with a $\Set$-based automaton
that possibly has branching structure specified by a monad $T$.
This automaton is determinised to yield a Moore automaton
over the category $\EM{T}$ of Eilenberg-Moore algebras for $T$,
and the result is a reachable and observable (i.e., minimal) Moore automaton
over $\EM{T}$.
If the automaton has no branching, we just proceed with Brzozowki over $\Set$.
In Appendix <ref>, we give a small example illustrating the difference between
the two minimisation constructs on a concrete DFA.

In [16], the perspective is based on modal logic.
Language semantics and reachability of automata is not an explicit part of the story,
although it is implicitly present via trace logic, however the connection to reachability
(in the usual set-theoretic sense) is not made.
In [20], the perspective is language-based. No link is made to modal logic.

Towards the aim of finding a unified categorical of both algorithms,
a few observations can be made already.
A dual equivalence is a special case of a dual adjunction.

In the remainder of this section, we present a categorical picture
that unifies both approaches.
In particular,

our picture formalises the role of trace logic in the minimisation algorithms. Some of the technical details of this part are known from  [58, 46, 39, 20] – precise connections are detailed throughout the sections and in Section <ref>.

§.§ Automata, Algebras and Coalgebras

Throughout this paper, we let $\Alph$ be a finite set. We will consider different types of automata, but they will all have input alphabet $\Alph$.

A classic deterministic automaton (on alphabet $\Alph$) consists of
a set $X$ (the state space),
a transition map $t \colon X \to X^\Alph$ (or equivalently $t \colon \Alph \times X \to X$),
an acceptance map $f \colon X \to 2$, and
an initial state $i \colon 1 \to X$.
We generalise this basic definition to arbitrary categories as follows.

Let $\catC$ be a category, and let $\I$ and $\B$ be objects in $\catC$.
A $\catC$-automaton
(with initialisation in $\I$ and output in $\B$)
is a quadruple $\str{X} = (X,t,i,f)$
consisting of
a state space object (or carrier) $X$ in $\catC$,
a $\Alph$-indexed set of transition morphisms $\{t_a \colon X \to X \mid a \in \Alph\}$,
an initialisation morphism $i \colon \I \to X$, and
an output morphism $f \colon X \to \B$.

A $\catC$-automaton morphism from $\str{X}_1 = (X_1,t_1,i_1,f_1)$ to $\str{X}_2 = (X_2,t_2,i_2,f_2)$

is a $\catC$-morphism $h \colon X_1 \to X_2$
such that for all $a \in \Alph$, $h \o t_{1,a} = t_{2,a} \o h$,
$f_1 = f_2 \o h$, and
$h \o  i_1 = i_2$.

Together, $\catC$-automata with initialisation in $\I$ and output in $\B$,
and their morphisms form a category which we denote by $\Aut^{I,B}_\catC$.

A classic deterministic automaton is then easily seen to be a $\Set$-automaton with output in $2$
and initialisation in $1$.

A central observation in [20] is that
automata can be seen as coalgebras with initialisation, or dually, as algebras with output,
as we briefly recall now.
Assuming that $\catC$ has products and coproducts,
the transition morphisms  $\{t_a \colon X \to X \mid a \in \Alph\}$
correspond uniquely to morphisms of the following type:

\begin{equation}
\begin{array}{c}
\tup{t_a}_{a \in \Alph}\colon X \to X^\Alph\\
\hline\hline
[t_a]_{a \in \Alph}\colon \Alph \cdot X \to X
\end{array}
\end{equation}

Letting $F$ and $G$ be endofunctors on $\catC$ given by
$FX = \B \times X^\Alph$
$GX = \I + \Alph \cdot X$, we see that
a $\catC$-automaton is an $F$-coalgebra $\tup{f,\tup{t_a}_{a \in \Alph}}\colon X \to B \times X^\Alph$
with intialisation $i\colon I \to X$.

Or equivalently, a $G$-algebra $[i,[t_a]_{a \in \Alph}]\colon GX \to X$ with output $f\colon X \to B$.

§.§ Dual Adjunctions of Coalgebras, Algebras and Automata

The categorical picture that unifies the work in [16] and [20]
is sketched in the diagram (<ref>) below.
This picture starts with a base dual adjunction that is lifted
to a dual adjunction between coalgebras and algebras.
This adjunction captures the construction in [16]
for obtaining observable coalgebras via duality.
The coalgebra-algebra adjunction is then lifted to a dual adjunction between automata
which captures the formalisation of the Brzozowski algorithm from [20],
which uses automata with initial states.

As shown above, automata have an algebra-part and a coalgebra part.
In order to generalise the notion of reachability on both sides
of the adjunction, we need an algebraic view on both sides.
Similarly, in order to generalise the notion of language semantics
on both sides, we need a coalgebraic view on both sides. [HH: I am thinking about how to present this with the minimal means...maybe we don't need the dual adj below on the right.]

In the remainder of the section, we will explain the details
of how this picture comes about.

\begin{equation}\label{eq:unify-pic}
\ba{ccc}
\xymatrix@C=0.8em@R=4em{
\left(\Aut_\catC^{I,R(O)}\right)^\op \ar@/^1pc/[rrrr]^-{\ol{\Pred}'} \ar@{}|{\top}[rrrr] \ar[d] &&&&
\Aut_\catD^{O,L(I)} \ar@/^1pc/[llll]^-{\ol{\Spc}'} \ar[d]
%\left(\text{\begin{tabular}{l}$G$-alg with\\output in $L(I)$\end{tabular}}\right)^\op
%\ar@{=}[r] & \Alg_\catD(G)^\op
\\
\Coalg_\catC(F_\catC)^\op \ar@/^1pc/[rrrr]^-{\ol{\Pred}} \ar@{}|{\top}[rrrr] \ar[d]
&&&& \Alg_\catD(G_\catD) \ar@/^1pc/[llll]^-{\ol{\Spc}} \ar[d]
\\
\ar@(dl,ul)^-{F_\catC^\op} \catC^\op \ar@/^1pc/[rrrr]^-{\Pred} \ar@{}|{\top}[rrrr] &&&&
\ar@(dr,ur)_-{G_\catD} \catD \ar@/^1pc/[llll]^-{\Spc}
%  &
%  \quad
%  &
\rem{
\xymatrix@C=0.8em@R=4em{
\Aut_\catC^{I       ,R(O)} \ar@/^1pc/[rrrr]^-{\wt{L}'} \ar@{}|{\bot}[rrrr] \ar[d] &&&&
\left(\Aut_\catD^{O,L(I)}\right)^\op \ar@/^1pc/[llll]^-{\wt{R}'} \ar[d]
%\left(\text{\begin{tabular}{l}$G$-alg with\\output in $L(I)$\end{tabular}}\right)^\op
%\ar@{=}[r] & \Alg_\catD(G)^\op
\\
\Alg_\catC(G_\catC) \ar@/^1pc/[rrrr]^-{\wt{L}} \ar@{}|{\bot}[rrrr] \ar[d]
&&&& \Coalg_\catD(F_\catD)^\op \ar@/^1pc/[llll]^-{\wt{R}} \ar[d]
\\
\ar@(dl,ul)^-{G_\catC} \catC \ar@/^1pc/[rrrr]^-{L} \ar@{}|{\bot}[rrrr] &&&&
\ar@(dr,ur)_-{F_\catD^\op} \catD^\op \ar@/^1pc/[llll]^-{R}
\\\\
F_\catC = \Spc (O) \times (-)^\Alph, \qquad
G_\catD = O + \Alph \cdot (-)
\rem{
\ba{rcl}
F_\catC &=& \Spc (O) \times (-)^\Alph\\
G_\catD &=& O + \Alph \cdot (-)
\ea}

\rem{
%  \qquad\qquad\qquad\qquad
\ba{rcl}
F_\catD &=& \L (I) \times (-)^\Alph\\
G_\catC &=& I + \Alph \cdot (-)
\ea
\\
\rem{
\ba{l}
\xi \colon  F_\catC \Spc \natIso \Spc G_\catD\\
\rho\colon G_\catD \Pred \To \Pred F_\catC
\ea
\rem{
\ba{l}
\chi \colon \L G_\catC \natIso F_\catD \L\\
\delta\colon G_\catC \Spc \To \Spc F_\catD
\ea
\ea
\end{equation}

§.§.§ Base dual adjunction

Our starting point is a dual adjunction $\Spc \dashv \Pred$ between categories $\catC$ and $\catD$
as in the above picture.
We will generally try to avoid the use of superscript $\op$,
and treat $\Pred$ and $\Spc$ as contravariant functors.
The units of the dual adjunction will be denoted
$\eta \colon \Id \To \Pred\Spc$
$\coun \colon \Id \To \Spc\Pred$.
The natural isomorphism of Hom-sets $\theta_{X,Y} \colon \catC(X,\Spc Y) \to \catD(Y, \Pred X)$,

will sometimes be written in both directions simply
as $f \mapsto \transp{f}$.
For $f \colon X \to \Spc{Y}$, its adjoint is $\transp{f} = \Pred{f} \o \eta_Y$,
and for $g \colon Y \to \Pred{X}$, its adjoint is $\transp{g} = \Spc{g} \o \coun_X$.

In all our examples, $\catC$ and $\catD$ are concrete categories, and
the dual adjunction arises from homming into a dualising object $\dua$ (cf. [57]),

i.e., $\Pred = \catC(-,\dua)$ and $\Spc = \catD(-,\dua)$,
and we will often denote both of them by $\dua^{(-)}$.
This means that adjoints are obtained simply by swapping arguments.
E.g., for $f\colon Y \to \dua^X$ we have
$\transp{f}(x)(y) = f(y)(x)$.
Moreover, the units are given by evaluation. E.g. $\eta_X \colon X \to \dua^{\dua^X}$
is defined by $\eta_X(x)(f) = f(x)$.

A central example is the self-dual adjunction of $\Set$
given by the contravariant powerset functor $\cPo = \Set(-,2)$
which maps a set $X$ to its powerset $2^X$ and a function $f:X\to Y$
to its inverse image map $f^{-1}\colon 2^Y \to 2^X$.
The functor $\cPo$ is dually self-adjoint with $\cPo^\op\dashv\cPo$,
and the isomorphism of Hom-sets is given by taking exponential transposes,
i.e., for $f\colon X \to 2^Y$ we have $\transp{f}\colon Y \to 2^X$.

Dual adjunctions are also called logical connections as they form the basis of semantics
for coalgebraic modal logics [22, 47, 42].
In this logic perspective,
$\catC$ is a category of state spaces,
$\catD$ is a category of algebras (e.g. Boolean algebras) encoding a propositional logic,
and the functor $G_\catD$ encodes a modal logic.
Intuitively, the adjoint $\Pred$ maps a state space $C$ to the predicates over $C$,
and $\Spc$ maps a predicate $A$ to the theories of $A$.
The logic given by $G_\catD$ can be interpreted over
$F_\catC$-coalgebra by providing a so-called one-step modal semantics in the form of a
natural transformation
$\rho\colon G_\catD \Pred \To \Pred F_\catC$,
or equivalently via its mate
$\xi \colon  F_\catC \Spc \To \Spc G_\catD$.
The pair $(G_\catD,\rho)$ is referred to as a logic.
By assuming that the initial $G_\catD$-algebra $(A_0,\alpha_0)$ exists, and viewing its elements as formulas,
the semantics of formulas in a $F_\catC$-coalgebra is $(C,\gamma)$ is obtained by initiality:
$\sm{G_\catD} \colon (A_0,\alpha_0) \to \Pred(\gamma) \o \rho_C$,
i.e., as an underlying $\catD$-map, it has type
$\sm{G_\catD} \colon A_0 \to \Pred(C)$.
Alternatively, the semantics can be specified by the theory map
$\th{G_\catD} \colon C \to \Spc(A_0)$ which is defined as
the adjoint of $\sm{G_\catD}$.
We refer to [22, 47, 42] for a more detailed introduction
to coalgebraic modal logic via dual ajdunctions.

§.§.§ Dual adjunction between coalgebras and algebras

We lift the base dual adjunction to coalgebras and algebras using some
some basic results from [39, 46].
We assume that
$\catC$ has products, $\catD$ has coproducts,
and that we have functors $F_\catC$ and $G_\catD$
as given above, i.e.,

\[
F_\catC(C) = \Spc(O) \times C^\Sigma \quad\text{ and }\quad
G_\catD(D) =  O + \Sigma \cdot D
\]

We know from
<cit.> (see also <cit.>),
the dual base adjunction $\Spc \dashv \Pred$ lifts to a dual adjunction
$\ol{\Spc} \dashv \ol{\Pred}$  between $\Coalg_\catC(F_\catC) = \Alg_{\catC^\op}(F_\catC^\op)$ and $\Alg_{\catD}(G_\catD)$
if there is a natural isomorphism $\xi\colon F_\catC \Spc \natIso \Spc G_\catD$.
We have for all $D \in \catD$,

\begin{equation}\label{eq:xi}
\Spc G_\catD(D) = \Spc(O + \Alph \cdot D) \cong \Spc(O)\times \Spc(D)^\Alph = F_\catC\Spc(D)
\end{equation}

since $\Spc$ (as a dual adjoint functor) turns colimits into limits.
Hence there is a natural isomorphism $\xi\colon F_\catC \Spc \natIso \Spc G_\catD$.
Let $\rho\colon G_\catD \Pred \To \Pred F_\catC$ be the mate of $\xi$,
i.e., the adjoint of $\xi_\Pred \circ F_\catC \coun$:

\begin{equation}\label{eq:mate}
\rho = \Pred F_\catC \coun \o \Pred \xi\Pred \o \eta G_\catD \Pred
\end{equation}

The lifted adjoint functors are defined for
all $F_\catC$-coalgebras $\gamma\colon C \to F_\catC(C)$,
all  $F_\catC$-coalgebra morphisms $f$,
all $G_\catD$-algebras $\alpha \colon G_\catD(D) \to D$,
and all $G_\catD$-algebra morphisms $g$ by:

\begin{equation}\label{eq:ol-LR}
\begin{array}{rclc}
\ol{\Pred}(\gamma) &=&  \Pred\gamma \o \rho_C \colon G_\catD \Pred C \to \Pred C, & \ol{\Pred}(f) = \Pred(f) \\
\ol{\Spc}(\alpha) &=& \xi_D \o \Spc\alpha \colon \Spc D \to F_\catC \Spc D, & \ol{\Spc}(g) = \Spc(g)
\end{array}
\end{equation}

The following lemma states the precise result.

Assume a dual adjunction $\Spc \dashv \Pred$ between $\catC$ and $\catD$
as described above, and that
the functors $F_\catC\colon\catC\to\catC$ and $G_\catD\colon\catD\to\catD$ are
as above, i.e.,

\[
F_\catC(C) = \Spc(O) \times C^\Sigma \quad\text{ and }\quad
G_\catD(D) =  O + \Sigma \cdot D
\]

where $\Alph$ is a finite set.
Then the dual adjunction $\Spc \dashv \Pred$
lifts to a dual adjunction $\ol{\Spc} \dashv \ol{\Pred}$
between $\Coalg_\catC(F_\catC)$ and $\Alg_{\catD}(G_\catD)$.
The lifted adjoint functors are defined for
all $F_\catC$-coalgebras $\gamma\colon C \to F_\catC(C)$,
all  $F_\catC$-coalgebra morphisms $f$,
all $G_\catD$-algebras $\alpha \colon G_\catD(D) \to D$,
and all $G_\catD$-algebra morphisms $g$ by:

\begin{equation}\label{eq:ol-LR}
\begin{array}{rclc}
\ol{\Pred}(\gamma) &=&  \Pred\gamma \o \rho_C \colon G_\catD \Pred C \to \Pred C, & \ol{\Pred}(f) = \Pred(f) \\
\ol{\Spc}(\alpha) &=& \xi_D \o \Spc\alpha \colon \Spc D \to F_\catC \Spc D, & \ol{\Spc}(g) = \Spc(g)
\end{array}
\end{equation}

The lemma follows from <cit.> (or <cit.>),
and the fact that $\Coalg_{\catD^\op}(G_\catD^\op) = \Alg_\catD(G_\catD)$.

The lifting to algebras and coalgebras in the above diagram on the right comes about similarly.
For all $C \in \catC$, we have

\begin{equation}\label{eq:chi}
\Pred G_\catC (C) = \Pred(I + \Alph\cdot C) = \Pred(I) \times (\Pred C)^\Alph = F_\catD L(C)
\end{equation}

Hence there is a natural isomorphism $\chi \colon \Pred G_\catC \natIso F_\catD \Pred$.
Let $\delta\colon G_\catC \Spc \To \Spc F_\catD$ be the mate of $\chi^{-1}$,
i.e., the adjoint of $\chi_\Spc^{-1}\circ F_\catD \coun$:

\begin{equation}\label{eq:mate-delta}
\delta = \Spc F_\catD\coun \o \Spc \xi^{-1}\Spc \o \coun G_\catC\Spc
\end{equation}

[HH: Need to check whether we really need this lemma.]

Assume a dual adjunction $\Spc \dashv \Pred$ between $\catC$ and $\catD$
as described above, and that the functors
$G_\catC\colon\catC\to\catC$ and $F_\catD\colon\catD\to\catD$ are
as above, i.e.,

\[
F_\catD(D) = \Pred(I) \times C^\Sigma \quad\text{ and }\quad
G_\catC(C) =  I + \Sigma \cdot D
\]

where $\Alph$ is a finite set.
Then the dual adjunction $\Spc \dashv \Pred$
lifts to a dual adjunction $\wt{\Spc} \dashv \wt{\Pred}$
between $\Alg_\catC(G_\catC)$ and $\Coalg_{\catD}(F_\catD)$.
The lifted adjoint functors are defined for
all $F_\catD$-coalgebras $\gamma\colon D \to F_\catD(D)$,
all  $F_\catD$-coalgebra morphisms $f$,
all $G_\catC$-algebras $\alpha \colon G_\catC(C) \to C$,
and all $G_\catC$-algebra morphisms $g$ by:

\begin{equation}\label{eq:wt-LR}
\begin{array}{rclc}
\wt{\Spc}(\gamma) &=&  \Spc\gamma \o \delta_D \colon G_\catC \Spc D \to \Spc D, & \wt{\Spc}(f) = \Spc(f) \\
\wt{\Pred}(\alpha) &=& \chi_C \o \Pred\alpha \colon \Pred C \to F_\catD \Pred C, & \wt{\Pred}(g) = \Pred(g)
\end{array}
\end{equation}

The lemma follows from <cit.>
and the fact that $\Alg_{\catD^\op}(F_\catD^\op) = \Coalg_\catD(F_\catD)$.

If $F'_\catC\colon\catC\to\catC$ is $F'_\catC(C) = B \times C^\Alph$ with $B \cong \Spc(O)$,
then $F'_\catC \natIso F_\catC$, and hence $\Coalg_\catC(F'_\catC) \cong \Coalg_\catC(F_\catC)$,
so we can think of $F'_\catC$-coalgebras as $F_\catC$-coalgebras.

The isomorphism $\ol{\theta}$ of Hom-sets for $\ol{\Spc} \dashv \ol{\Pred}$
is simply the restriction of the isomorphism $\theta$ of Hom-sets
for $\Spc \dashv \Pred$ to the relevant morphisms.

\[
\ba{c}
\gamma \sgoes{\transp{h}} \ol{\Spc}(\alpha)\\
\hline\hline
\alpha \sgoes{h} \ol{\Pred}(\gamma)
\ea
\]

The natural transformation $\rho \colon G_\catD\Pred \To \Pred F_\catC$
provides the one-step semantics for a modal logic for $F_\catC$-coalgebras
as described at the end of Section <ref>.

This makes most sense when the dual adjunction arises from a dualising object $\dua$
in which case $\dua$ is a domain of truth-values, i.e., the logic is $\dua$-valued,
and when $\catD$ is category of algebras with operations given by a signature $Sgn$.
The algebra functor $G_\catD = O + \Alph\cdot(-)$ then corresponds to a modal language
$\LLang{G_\catD}$ that has atomic propositions from $O$, labelled modalities $\boxmod{a}$, $a \in \Alph$,
and the propositional connectives are the operations from $Sgn$.
That is, formulas in $\LLang{G_\catD}$ are generated by the following grammar:

\[
\phi ::= q \in O \mid \boxmod{a}\phi, a \in \Alph \mid \sigma(\Psi), \sigma \in Sgn
\]

where $\Psi$ is a set of formulas of cardinality matching the arity of the operation $\sigma$.

For our specific choice of functors $F_\catC$ and $G_\catD$,
we compute the concrete definition of $\rho$ from (<ref>)
when the adjunction arises from a dualising object.

\[\ba{lcccccl}
\rho_X\colon\\
O + \Alph\cdot\Pred{X} & \sgoes{\eta_{G\Pred{X}}}
& \Pred\Spc(O+\Alph\cdot\Pred{X}) & \sgoes{\sim}
& \Pred(\Spc{O}\times(\Spc\Pred{X})^\Alph) & \sgoes{\Pred F_\catC\coun_X}
& \Pred(\Spc{O} \times X^\Alph)
\\
O + \Alph\cdot\dua^{X} & \sgoes{\eta_{G(\dua^{X})}}
& \dua^{\dua^{(O+\Alph\cdot\dua^{X})}} & \sgoes{\sim}
& \dua^{(\dua^{O}\times(\dua^{\dua^{X}})^\Alph)} & \sgoes{\dua^{F_\catC\coun_X}}
& \dua^{\dua^{O} \times X^\Alph}
\\
q & \mapsto & \eta(q) & \mapsto &  \eta(q) & \mapsto &
\lambda (j,d) . j(q)
\\
\qquad (a,p) & \mapsto & \eta(a,p) & \mapsto &  \eta(a,p) & \mapsto &
\lambda (j,d) . p(d(a))
\ea\]

Here we used that the units evaluate, and that

\[\ba{lccc}
\dua^{F_\catC\coun_X} \colon
& \dua^{(\dua^{O}\times(\dua^{\dua^{X}})^\Alph)} & \sgoes{}
& \dua^{\dua^{O} \times X^\Alph}
\\
& h & \mapsto &
\lambda(j,d) . h (j, \lambda a. \lambda g. g(d(a)))
\ea\]

In short,

\begin{equation}\label{eq:rho-concrete}
\ba{rc}
\rho_X\colon\colon
& O + \Alph\cdot\dua^{X}
\sgoes{}
\dua^{\dua^{O} \times X^\Alph}
\\
\ba{rcl}
\rho(q)(j,d) &=& j(q)\\
\rho(a,p)(j,d) &=& p(d(a))
\ea
\ea
\end{equation}

For our specific choice of functors $F_\catC$ and $G_\catD$,
and when the adjunction arises from a dualising object $\dua$,
we can compute the concrete definition of $\rho$ from (<ref>)
(see Appendix <ref>) and we get the following $\dua$-valued modal semantics
of the language $\LLang{G_\catD}$:

\[
\ba{rcll}
\sem{q}(x) &=& j(q), & \text{where } \gamma(x) = \tup{j\colon \dua^O,d\colon X^\Alph}
\\
\sem{\boxmod{a}\phi}(x) &=& \sem{\phi}(d(a)), &  \text{where } \gamma(x) = \tup{j\colon \dua^O,d\colon X^\Alph}
\\
\sem{\sigma(\Psi)}(x) &=& \sigma(\{\sem{\psi}(x) \mid \psi \in \Psi\})
\ea\]

This shows that $\rho$ gives the expected modal semantics for
$F_\catC$-coalgebras viewed as deterministic $\Alph$-labelled Kripke frames with observations from $O$.
In particular, the modalities are “deterministic” Kripke box/diamond-modalities.

We consider the case of classic deterministic automata.
Here $\catC =\catD=\Set$,
$F_\Set = 2 \times (-)^\Alph$ and $G_\Set = 1 + \Alph\cdot(-)$,
and the self-dual adjunction of $\Set$ is
by the contravariant powerset functor $\cPo = \Set(-,2)$ (Example <ref>).
The logic we obtain is trace logic [47],
but here interpreted over DFAs rather than labelled transition systems as in [47].
The initial $G_\Set$-algebra is $\Alph^*$, the set of finite words over $\Alph$,
and these are the formulas $\LLang{G_\catD}$,
since $\catD = \Set$ means that there are no propositional connectives.

The natural transformation $\rho$ has type
$\rho_X \colon 1 + \Alph\cdot 2^X \to 2^{2 \times X^\Alph}$,
and is given concretely here together with the induced semantics, where we write $x \Vdash \phi$ iff $\sem{\phi}(x) = 1$:

\[
\ba{rcl}
\rho_X(*) &=&  \{ (b,d) \in 2 \times X^\Alph \mid b = 1\}\\
\rho_X(a,U) &=&  \{ (b,d) \in 2 \times X^\Alph \mid d(a) \in U \}
\ea
\ba{||lcl}
x \Vdash *  & \iff & \text{$x$ is accepting}\\
x \Vdash \boxmod{a}\phi  & \iff & x \sgoes{a} y \text{ and } y \Vdash \phi
\ea
\]

§.§.§ Dual adjunction between automata

In order to obtain the upper adjunction in (<ref>) (which formalises Brzozowski),
we will use algebra and coalgebra structure on both sides,
hence we assume that $\catC$ and $\catD$ both have products and coproducts.
The lifting is a small extension of $\ol{\Spc} \dashv \ol{\Pred}$
obtained by defining how an initialisation map $I \to C$ for an $F_\catC$-coalgebra $\gamma$
is turned into an observation map $\Pred{C} \to \Pred{I}$ for the $G_\catD$-algebra $\ol{\Pred}(\gamma)$,
and vice versa for $\ol{\Spc}$.

by defining $\ol{\Pred}'\colon \Aut_\catC^{I,\Spc O} \to \Aut_\catD^{O, \Pred I}$
and $\ol{R}' \colon \Aut_\catD^{O, \Pred I} \to \Aut_\catC^{I,\Spc O}$ as follows
for all $\gamma\colon C \to F_\catC C$ and $\alpha \colon G_\catD D \to D$:

\begin{equation}\label{eq:def-Aut-LR}
\begin{array}{rclc}
\ol{\Pred}'(\gamma, i\colon I \to C) &=&  (\ol{\Pred}(\gamma) \colon G_\catD\Pred C \to \Pred C, \Pred(i)\colon \Pred C \to \Pred I), & \ol{\Pred}'(f) = \Pred(f) \\
\ol{\Spc}'(\alpha, j\colon D \to \Pred I) &=& (\ol{R}(\alpha)\colon \Spc D \to F_\catC\Spc D,\transp{j}\colon I \to \Spc D) , & \ol{\Spc}'(g) = \Spc(g)
\end{array}
\end{equation}

Under the assumptions of section <ref>,
the dual adjunction
$\ol{\Spc} \dashv \ol{\Pred}$ between $\Coalg_\catC(F_\catC)$ and $\Alg_{\catD}(G_\catD)$
lifts to a dual adjunction $\ol{\Spc}' \dashv \ol{\Pred}'$
between $\Aut_\catC^{I,\Spc O}$ and $\Aut_\catD^{O, \Pred I}$ by
defining $\ol{\Pred}'$
and $\ol{R}'$
as follows for all $\gamma\colon C \to F_\catC C$ and $\alpha \colon G_\catD D \to D$:

\[\begin{array}{rclc}
\ol{\Pred}'(\gamma, i\colon I \to C) &=&  (\ol{\Pred}(\gamma) \colon G_\catD\Pred C \to \Pred C, \Pred(i)\colon \Pred C \to \Pred I), & \ol{\Pred}'(f) = \Pred(f) \\
\ol{\Spc}(\alpha, j\colon D \to \Pred I) &=& (\ol{R}(\alpha)\colon \Spc D \to F_\catC\Spc D,\transp{j}\colon I \to \Spc D) , & \ol{\Spc}'(g) = \Spc(g)
\end{array}
\]

This is a minor generalisation of Prop. 9.1 in [20].
It suffices to show that
for all $\catC$-arrows $i \colon I \to C$, and
all $\catD$-arrows $g \colon D \to \Pred{I}$ and $h\colon D \to \Pred{X}$:
g = \Pred{i} \o h \text{ iff } \transp{g} = \transp{h} \o i.
First, if $g = \Pred{i} \o h$, then
$\transp{g} = \Spc{g} \o \coun_I = \Spc{h} \o \Spc\Pred{i} \o \coun_I = \Spc{h} \o \coun_X \o i = \transp{h} \o i$,
where the third equality follows from naturality of $\coun$.
Conversely, if $\transp{g} = \transp{h} \o i$, then
$g = \Pred{\transp{g}} \o \eta_D = \Pred{i} \o \Pred{\transp{h}} \o \eta_D = \Pred{i} \o h$.

Define $\wt{L}'$ and $\wt{R}'$ similarly, and show that
$\wt{L}' = \ol{L}'$ and $\wt{R}' = \ol{R}'$.

It is straightforward to verify that for our choice of $F_\catC$,
the final $F_\catC$-coalgebra exists,

and we usually view it as having carrier
$\Spc(O)^{\Alph^*}$, hence for $\gamma \colon C \to F_\catC(C)$,
the final morphism $!_\gamma \colon C \to \Spc(O)^{\Alph^*}$
assigns to each state in $C$ what can be seen as an $\Spc(O)$-weighted language.
For $\str{X} = \tup{\gamma,i} \in \Aut_\catC^{I,\Spc(O)}$,
we define its language semantics as the composition
$\I \stackrel{i}{\to} C \stackrel{!_\gamma}{\to} \Spc(O)^{\Alph^*}$.

This $\catC$-morphism can be seen as an $\Alph^*$-indexed family of
$\catC$-morphisms $\langsem{\str{X}}_w \colon I \to \Spc{O}$
defined for all $w = a_1 \cdots a_k \in \Alph^*$ by

\[
\langsem{\str{X}}_w \;\;=\;\; I \sgoes{i} X \sgoes{t_{a_1}} \cdots  \sgoes{t_{a_k}} X \sgoes{f} \Spc(O)
\]

Computing the adjoint transpose $\transp{\langsem{\str{X}}_w} = \Pred{\langsem{\str{X}}} \o \eta_O$,
we get the $\catD$-morphism:

\[
\transp{\langsem{\str{X}}_w} \;\;=\;\; \Pred(I) \sfrom{i} \Pred(X) \sfrom{\Pred t_{a_1}} \cdots \sfrom{\Pred t_{a_k}} \Pred(X) \sfrom{\transp{f}} O
\]

Hence $\transp{\langsem{\str{X}}_w} = \langsem{\ol{\Pred}'(\str{X})}_{w^R}$
where $w^R = a_k \cdots a_1$ is the reversal of $w$.
Similarly, we find that
for all $\str{Y} \in \Aut_\catD^{O,\Pred(I)}$,
$\transp{\langsem{\str{Y}}_w} = \langsem{\ol{\Spc}'(\str{Y})}_{w^R}$.
In the case of classic DFAs from Example <ref>
where $I=O=1$ and $\Spc(O) = \Pred(I) \cong 2$,
the above says that the adjoint functors reverse the language accepted by the automaton.

In the case of PODFAs and BAOs
where $O = \FBA(\Obs) = 2^{2^\Obs}$ for a finite set $\Obs$ of observations,
$\Pred(X) = 2^X$, $\Spc(A) = \Uf(A)$,
and we choose an initial state with $i \colon 1 \to X$,

\[\ba{rll}
\langsem{\str{X}}_w: & 1 \to 2^\Obs = \Uf(\FBA(\Obs)) & \text{ in } \Set\\
\hline\hline
\langsem{\ol{\Pred}'(\str{X})}_{w^R}: & \FBA(\Obs) \to 2^1 & \text{ in } \BA\\
\hline\hline
\langsem{\ol{\Pred}'(\str{X})}_{w^R}: & \Obs \to 2^1 & \text{ in } \Set\\
\ea\]

§.§ Language Semantics and Trace Logic

In this section, we give a general condition on the output sets that ensures
that we can link trace logic with the full modal logic via an adjunction.
This places trace logic in the general picture.

In [16], it was shown in each of the concrete examples that trace logic
is equally expressive as the full modal logic.
The results of this section give a general explanation of this fact.

Assume that the category $\catD$ is monadic over $\Set$
with adjunction
\begin{tikzcd}[sep=1.5em, cramped]
\FreeD : \catD
\arrow[r, shift left=1.7pt]
& \Set : \ForgD
\arrow[l, shift left=1.7pt]
\end{tikzcd}
This adjoint situation allows us to relate the $\Set$-based language semantics to
the final $F_\catC$-coalgebra semantics as we will show now.

Consider the functor $G \colon\Set\to\Set$ defined as
$G(X) = \Obs + \Alph \cdot X = \Obs + \Alph \times X$ where $\Obs$ is a finite
set of observations.
Then the set $\Alph^*\Obs$ is an initial $G$-algebra with algebra structure
$\Obs + \Alph \times (\Alph^*\Obs) \to \Alph^*\Obs$
given by prefixing $\obs\in\Obs$ with the empty word
$\obs \mapsto \emptyword \obs$

and concatenation $(a,w) \mapsto aw$.

Let $\Phi_\catD \dashv U_\catD$ be an adjunction between $\Set$ and $\catD$.
Then we can compose with the dual adjunction $\Spc \dashv \Pred$
to obtain a dual adjunction between $\catC$ and $\Set$ as follows:

\begin{equation}\label{eq:comp-adj}
\xymatrix@C=0.8em@R=4em{
\ar@(dl,ul)^-{F_\catC^\op} \catC^\op \ar@/^1pc/[rrrr]^-{\Pred} \ar@{}|{\top}[rrrr] &&&&
\ar@(dl,dr)_-{G_\catD} \catD \ar@/^1pc/[llll]^-{\Spc}   \ar@/^1pc/[rrrr]^-{\ForgD} \ar@{}|{\top}[rrrr] &&&&
\ar@(dr,ur)_-{G} \Set \ar@/^1pc/[llll]^-{\FreeD}
\end{equation}

Assume we have the situation in (<ref>), and that $F_\catC$, $G_\catD$, $G$ are defined by:

\[
F_\catC(C) = \Spc\FreeD(\Omega) \times C^\Alph, \qquad
G_\catD(D) = \FreeD(\Omega) + \Alph \cdot D, \qquad
G(X) = \Obs + \Alph \cdot X.
\]

\[\ba{llcr}
G \colon \Set \to \Set, & G(X) &=& \Obs + \Alph \cdot X
\\
G_\catD \colon \catD \to \catD, & G_\catD(D) &=& \FreeD(\Omega) + \Alph \cdot D
\\
F_\catC \colon \catC \to \catC, & F_\catC(C) &=& \Spc\FreeD(\Omega) \times C^\Alph
\ea
\]

Then (<ref>) lifts to

\begin{equation}\label{eq:comp-adj-lifted}
\xymatrix@C=0.8em@R=4em{
\Coalg_\catC(F_\catC)^\op \ar@/^1pc/[rrrr]^-{\ol{\Pred}} \ar@{}|{\top}[rrrr] %\ar[d]
&&&& \Alg_\catD(G_\catD) \ar@/^1pc/[llll]^-{\ol{\Spc}}   \ar@/^1pc/[rrrr]^-{\ol{\ForgD}}  \ar@{}|{\top}[rrrr] %\ar[d]
&&&& \Alg_\Set(G) \ar@/^1pc/[llll]^-{\ol{\FreeD}} %\ar[d]
\rem{
\\
\ar@(dl,ul)^-{F_\catC^\op} \catC^\op \ar@/^1pc/[rrrr]^-{\Pred} \ar@{}|{\top}[rrrr] &&&&
\ar@(dl,dr)_-{G_\catD} \catD \ar@/^1pc/[llll]^-{\Spc}   \ar@/^1pc/[rrrr]^-{\ForgD} \ar@{}|{\top}[rrrr] &&&&
\ar@(dr,ur)_-{G} \Set \ar@/^1pc/[llll]^-{\FreeD}
\end{equation}

The dual adjunction on the left lifts because of a special case of (<ref>).
For similar reasons, the adjunction on the right lifts, because
there is a natural isomorphism $\kappa: \FreeD G \natIso G_\catD \FreeD$ that can
be obtained as follows

\begin{equation}\label{eq:kappa}
\kappa \colon \FreeD G X = \FreeD (\Obs + \Alph\cdot X) \cong \FreeD (\Obs) + \Alph\cdot \FreeD(X)
= G_\catD \FreeD(X),
\end{equation}

since $\FreeD$ (being a left adjoint) preserves colimits.
By <cit.>, $\FreeD \dashv \ForgD$ lifts to an adjunction between
$\ol{\FreeD} \dashv \ol{\ForgD}$  between $\Alg_\catD(G_\catD)$ and $\Alg_\Set(G)$ where the
functor $\ol{\FreeD}$ maps a $G$-algebra $(X,\alpha)$ to the $G_\catD$-algebra
$(\FreeD(X),\FreeD \alpha \circ \kappa^{-1})$.

By composition of adjunctions, also $\Spc\FreeD \dashv \ForgD\Pred$ lifts.
This could also be verified by noticing that for all sets $X$, there is natural isomorphism

\begin{equation}\label{eq:xi-trace}
\xitrc \coloneqq  \Spc \kappa \circ \xi\FreeD : F_\catC\Spc\FreeD \natIso  \Spc\FreeD G
%F_\catC\Spc\FreeD X = \Spc\FreeD(\Obs) \times (\Spc\FreeD X)^\Alph \cong  \Spc(\FreeD(\Obs + \Alph\cdot X)) = \Spc\FreeD G(X)
\end{equation}

where $\xi\colon F_\catC \Spc \natIso \Spc G_\catD$ from (<ref>)
is the mate of the modal logic $(G_\catD,\rho)$.

Hence by <cit.> (see also <cit.>),
the adjunction $\Spc\FreeD \dashv \ForgD\Pred$ lifts to one between $\Coalg_\catC(F_\catC)^\op$ and $\Alg_\Set(G)$.

Letting $\rhotrc\colon G \ForgD\Pred \To \ForgD\Pred F_\catC$ be the mate of
$\xitrc$ from (<ref>), then $(G,\rhotrc)$ is a modal logic for $F_\catC$-coalgebras.
Since its formulas are the elements of the intial $G$-algebra of traces,
we refer to $(G,\rhotrc)$ as a trace logic.

The theory maps $\th{G}$ and $\th{G_\catD}$ of the logics  $(G,\rhotrc)$ and  $(G_\catD,\rho)$ coincide.

Due to the adjunctions in (<ref>),
the intial $G$-algebra $\Trc$ of traces is mapped by $\ol{\FreeD}$ to an initial $G_\catD$ algebra,
which in turn is mapped by $\ol{\Spc}$ to a final $F_\catD$-coalgebra.
The coincidence of the theory maps follows from them being adjoints of the initial maps.
A more detailed argument is given in Appendix <ref>.

In the case where $\catD = \BA$, the fact that $\FreeD(\Trc)$ is an initial $G_\catD$-algebra implies that elements of the
Lindenbaum-Tarski algebra of $\LLang{G_\catD}$ are equivalent to a Boolean combination of trace formulas.
The elements of ${\FreeD}(\Trc)$ can therefore be seen as normal forms.

Since the mates $\xi$ and $\xitrc$ are both natural isomorphisms,

it follows from [47, 42] (and $\catC$ having a suitable factorisation system, cf. Theorem <ref>)
that the full modal logic $(G_\catD,\rho)$ and trace logic $(G,\rhotrc)$ are both
expressive for $F_\catC$-coalgebras.
In other words, the propositional connectives from $\catD$-structure in the logic language $\LLang{G_\catD}$
do not add any epxressive power to $\LLang{G}=\Trc$.

In summary, we arrive at the following proposition.

With the above assumptions, the trace logic $(G,\rhotrc)$
and the full logic $(G_\catD,\rho)$ are equally expressive over $F_\catC$-coalgebras,
meaning that for all $F_\catC$-coalgebras $\gamma\colon C \to F_\catC(C)$,
and all states $c_1, c_2$ in $C$ (recall that $\catC$ is a concrete category),
$c_1$ and $c_2$ are logically equivalent for $(G,\rhotrc)$
iff they are logically equivalent for $(G_\catD,\rho)$.

By the uniqueness of final coalgebras up to isomorphism,
it follows that there is an isomorphism
$\sigma\colon \Spc\FreeD(\Obs)^{\Alph^*} \stackrel{\sim}{\to} \Spc\,\FreeD(\Trc)$
which links the language semantics in the automata/coalgebraic sense
with trace logic semantics given by initiality.

For all $F_\catC$ coalgebras $\gamma$, its language semantics defined
as the unique morphism into the final $F_\catC$-coalgebra
corresponds to the trace theory map $\th{G}$ into the final $F_\catC$-coalgebra
(and with the theory map $\th{G_\catD}$)
via the isomorphism $\sigma$.

We remark that it is straightforward to extend $\ol{\FreeD} \dashv \ol{\ForgD}$
to an adjunction of automata by taking adjoints of additional output maps to the algebras.
We omit the details.

Finally, we show that trace logic expressiveness can be extended to coalgebras for
what we can think of as subfunctors of $F_\catC$. This will be needed for the
topological automata in section <ref>.

Let $F'_\catC$ be a functor on $\catC$ which preserves monos and
such that there is a natural transformation
$\tau \colon F'_\catC \To F_\catC$ which is abstract mono,
i.e., all components are mono.
Assume that $\catC$ has factorisation system $(E,M)$ with $E \subseteq Epi$
and $M \subseteq Mono$.

Defining  $\xi' = \xitrc \o \tau_\Spc$,
then $\xi'\colon F'_\catC \Spc\FreeD \To \Spc\FreeD G$ defines semantics of trace formulas
over $F'_\catC$-coalgebras which is essentially the same as the semantics over
Since $\tau$ is abstract mono and $\xitrc$ is a natural iso,
it follows that $\xi'$ is abstract mono, and hence the asscoiated logic
is expressive [47, 42].

§.§ Reachability and Observability

A main point emphasised in [20] is that reachability is an algebraic concept, and
observability is a coalgebraic concept, and both concepts apply to automata
as they are both coalgebras and algebras.
We will call an algebra reachable if it has no proper subalgebras,
and a coalgebra is observable if it has no proper quotients.

Both [16] and [20] use that a reachable algebra dualises to an
observable coalgebra, only the perspectives differ.
Note that in [16], observable coalgebras are referred to as minimal automata.

In [16], the reachable part of a $G_\catD$-algebra is defined as its least subalgebra,
and its existence was ensured by assuming that $\catC$ is wellpowered.
In [20], automata were generally considered as automata over $\Set$,
and the reachable part of an automaton was  defined as the image of the
initial $G$-algebra inside the automaton (using its $G$-algebra structure, after possibly forgetting $\catD$-structure).

In Appendix <ref>, we show that the two reachability notions in
[16] and [20] coincide when conditions for both are satisfied.

In [16],
the least $G_\catD$-algebra of the dual $G_\catD$-algebra $\ol{\Pred}(\gamma)$
was characterised as the subalgebra $\alpha_\mathrm{Def}$ of
$\LLang{G_\catD}$-definable subsets of $C$
(or more abstractly $\dua$-valued predicates on $C$).
It was observed that $\alpha_\mathrm{Def}$ is generated by subsets
definable by trace formulas on $(C,\gamma)$.
The general statement of this fact is Proposition <ref>.
Hence to compute $\alpha_\mathrm{Def}$, it suffices to compute trace logic definable subsets.
In the case of classic DFA, these subsets are precisely the reachable states
(in the usual transition-sense) of $\ol{\Pred}(\gamma)$.

As mentioned, observability is a coalgebraic concept.
A coalgebra is observable if it has no proper quotients,
hence a coalgebra can be made observable by taking a largest quotient.

In [16], largest quotients of $F_\catC$-coalgebras were ensured to exist by assuming that
$\catC$ is co-wellpowered which entails that $\Coalg_\catC(F_\catC)$ is co-wellpowered.
As with initial $G_\catD$-algebras, the final $F_\catC$-coalgebra generally did not exist.
In [20], the final $F_\catC$-coalgebra always existed, and
observability was defined as the final morphism being injective.
It is straightforward to formulate and prove a dual version of Lemma <ref>.
We omit the details due to lack of space.

The general setup described in Lemma <ref> is most closely related to
that of [20],
as we have an initial $G$-algebra and an initial $G_\catD$-algebra. The latter is mapped by $\ol{\Spc}$ to a final $F_\catC$-coalgebra
since the dual adjoint functors turn colimits into limits.
For this reason, $\ol{\Spc}$ maps epis to monos, but monos are not necessarily mapped to epis.
In particular,
we cannot argue that a least subalgebra of $\ol{\Pred}(\gamma)$
is mapped by $\ol{\Spc}$ to a largest quotient of $\gamma$.
But using factorisation and existence of an initial $G_\catD$-algebra,
we obtain that the reachable part of $\ol{\Pred}(\gamma)$ is mapped by $\ol{\Spc}$
to an observable coalgebra.

Under the assumptions of Lemma <ref>,
and assuming further that
$\catD$ has a factorisation system $(E,M)$
such that $E \subseteq Epi$ and $M \subseteq Mono$,

we then have:

For all $(D,\delta) \in \Alg_\catD(G_\catD)$, let $\reach{D,\delta}$ be
the reachable part of $(D,\delta)$ obtained
by $(E,M)$-factorisation of the initial morphism:

\ol{\FreeD}(\Trc,\alpha) \stackrel{e}{\surj} \reach{D,\delta} \stackrel{m}{\subto} (D,\delta).

Then  $\ol{\Spc}(\reach{D,\delta})$ is an observable $F_\catC$-coalgebra.

The epimorphism $e\colon \ol{\FreeD}(\Trc,\alpha) \surj \reach{D,\delta}$
is mapped by $\ol{\Spc}$ to a monomorphism

$$\ol{\Spc}(e) \colon \ol{\Spc}(\reach{D,\delta}) \subto \ol{\Spc}\ol{\FreeD}(\Trc,\alpha).$$

Since $\ol{\Spc}\ol{\FreeD}(\Trc,\alpha)$ is a final $F_\catC$-coalgebra, we can conclude that
$\ol{\Spc}(\reach{D,\delta})$ is an observable $F_\catC$-coalgebra.

The above proposition thus tells us how to obtain an observable $F_\catC$-coalgebra, and hence also
an observable $\catC$-automaton, by taking the reachable part on the dual side.

Extending the notion of reachable part to $\catD$-automata is done simply by taking the reachable part of their $G_\catD$-algebraic part and restricting the output map.
Brzozowski's algorithm produces a minimal $\catC$-automaton by taking the reachable part
of the resulting observable $\catC$-automaton, that is, with respect to the
algebraic structure of $\catC$-automata given by $G_\catC = \I + \Alph\cdot(-)$.
In order to do so, we need that also $\catC$ has an suitable factorisation system.

§.§ Abstract minimisation algorithms

We now put everything together into one diagram with which we can describe both approaches from
[16] and [20] including the role of trace logic.

\begin{equation}\label{eq:comp-adj-all}
\ba{c}
\xymatrix@C=0.7em@R=4em{
\left(\Aut_\catC^{\I,\Spc\FreeD(\Obs)}\right)^\op \ar@/^1pc/[rrrr]^-{\ol{\Pred}'} \ar@{}|{\top}[rrrr] \ar[d] &&&&
\Aut_\catD^{\FreeD(\Obs),\Pred(I)} \ar@/^1pc/[llll]^-{\ol{\Spc}'} \ar@/^1pc/[rrrr]^-{\ol{\ForgD}'} \ar@{}|{\top}[rrrr] \ar[d] &&&&
\Aut_\Set^{\Obs,\ForgD\Pred(I)} \ar@/^1pc/[llll]^-{\ol{\FreeD}'} \ar[d]
\\
\Coalg_\catC(F_\catC)^\op \ar@/^1pc/[rrrr]^-{\ol{\Pred}} \ar@{}|{\top}[rrrr] \ar[d]
&&&& \Alg_\catD(G_\catD) \ar@/^1pc/[llll]^-{\ol{\Spc}}   \ar@/^1pc/[rrrr]^-{\ol{\ForgD}}  \ar@{}|{\top}[rrrr] \ar[d]
&&&& \Alg_\Set(G) \ar@/^1pc/[llll]^-{\ol{\FreeD}} \ar[d]
\\
\ar@(dl,ul)^-{F_\catC^\op} \catC^\op \ar@/^1pc/[rrrr]^-{\Pred} \ar@{}|{\top}[rrrr] &&&&
\ar@(dl,dr)_-{G_\catD} \catD \ar@/^1pc/[llll]^-{\Spc}   \ar@/^1pc/[rrrr]^-{\ForgD} \ar@{}|{\top}[rrrr] &&&&
\ar@(dr,ur)_-{G} \Set \ar@/^1pc/[llll]^-{\FreeD}
\\
F_\catC(C) = \Spc\FreeD(\Omega) \times C^\Alph, \quad
G_\catD(D) = \FreeD(\Omega) + \Alph \cdot D, \quad
G(X) = \Obs + \Alph \cdot X.
\ea
\end{equation}

Let $\catC, \catD$ be concrete categories, both having products and coproducts, and
both having factorisation systems $(E,M)$  such that $E \subseteq Epi$ and $M \subseteq Mono$.
Let $\Obs$ be a finite set (of observations), and $\I$  an (initialisation) object in $\catC$, and
assume that we have the adjoint situation between $\catC$, $\catD$, $\Set$ and functors
as described at the bottom level of (<ref>).
Then the lower adjunctions lift to the upper two levels in (<ref>)
as shown in sections <ref>, <ref> and <ref>,
and we have the following abstract algorithms:

Given an $F_\catC$-coalgebra $\gamma$, compute $\ol{\Spc}(\reach{\ol{\Pred}(\gamma)})$ which will be an observable $F_\catC$-coalgebra.

Given an $F_\catC$-coalgebra $\gamma$, compute $\ol{\Spc}\ol{\FreeD}(\reach{\ForgD\ol{\Pred}(\gamma)})$ which will be an observable $F_\catC$-coalgebra.

Given a $\catC$-automaton $(\gamma,i)$, compute $\reach{\ol{\Spc}'(\reach{\ol{\Pred}'(\gamma,i)})}$, which will be a reachable and observable (i.e., minimal)  $\catC$-automaton.

Given a $\catC$-automaton $(\gamma,i)$, compute $\reach{\ol{\Spc}'\,\ol{\FreeD}'(\reach{\ol{\ForgD}'\,\ol{\Pred}'(\gamma,i)})}$, which will be a reachable and observable (i.e., minimal)  $\catC$-automaton.

and assume there are contravariant adjoint functors
\begin{tikzcd}[sep=1.5em, cramped]
\Pred : \catC
\arrow[r, shift left=1.7pt]
& \catD : \Spc
\arrow[l, shift left=1.7pt]
\end{tikzcd}
and covariant adjoint functors
\begin{tikzcd}[sep=1.5em, cramped]
\ForgD : \catD
\arrow[r, shift left=1.7pt]
& \Set : \FreeD
\arrow[l, shift left=1.7pt]
\end{tikzcd}
Let $\Obs$ is a finite set of observations, and let $\I$ be an (initialisation) object in $\catC$,
and assume the following functor definitions:
$F_\catC(C) = \Spc\FreeD(\Omega) \times C^\Alph$,
$G_\catD(D) = \FreeD(\Omega) + \Alph \cdot D$,
$G(X) = \Obs + \Alph \cdot X$.

Of course, the abstract algorithms only become actual algorithms, when all structures involved have
finite representations.

Furthermore, we note that the one could consider an algorithm that uses the horizontally composed adjunction in (<ref>), i.e.,
compute  $\ol{\Spc}\ol{\FreeD}(\reach{\ForgD\ol{\Pred}(\gamma)})$.
Although, the result will be an observable coalgebra, this is, however, not a good choice in general, because the reachable part is now computed over $\Set$, and this may yield an infinite coalgebra/automaton whereas it might have been finitely generated as a coalgebra/automaton over $\catD$. An example where this happens is found in Example 8.3 of  [20].

Although [16] does not describe a concrete algorithm,
the implicit abstract algorithm is essentially Algo1,
since the conceptual emphasis is placed on computing the least $G_\catD$-subalgebra of $\ol{\Pred}(\gamma)$
as the subalgebra of $(G_D,\rho)$-definable subsets/predicates.
The characterisation of this $G_\catD$-subalgebra as being freely generated by the least $G$-subalgebra of
(i.e. the reachable part in the usual set-theoretic sense) can be viewed as an optimisation: to determine
the reachable part of a given $G_\catD$-algebra it suffices to compute the part that can be “reached”/defined via trace formulas.
This is the information contained in the right-hand side of the diagram.

In comparison,
Brzozowski's algorithm and its generalisation to weighted automata in Section <ref>
are instances of Algo2 as they use initial states.
Classic Brzozowski is the case $\catC = \catD = \Set$, $G_\catD = G$, and $\Obs = \I = 1$.
The set-based algorithm for weighted automata in [20] is neither of the above algorithms, but it can be described as constructing  $\reach{\ol{\ForgD}'\,\ol{\Pred}'(\gamma,i)}$, and then dualise back (without going through $\SMod$) to get a $\Set$-based Moore automaton. As mentioned above, this may result in the reachable part of the reversed automaton being infinite.

In the case where the dual adjunction is a full duality, the initial state is easily found back in the observable coalgebra resulting from Algo1 as its language equivalence class, so the extension to Algo2 seems almost trivial. In case the dual adjunction is not a full duality, the transformation of the initial state goes via the adjunction, and factorisation on the dual side, and this is what Theorem <ref> formalises.

We end this section by observing that the requirements regarding products, coproducts and
factorisation systems hold in all our examples, since $\catC$ and $\catD$ are monadic over $\Set$
meaning that they are equivalent to an
Eilenberg-Moore category $\EM{T}$ for a $\Set$-monad $T$.
For such a category $\EM{T}$, we know that it is
complete, cocomplete and exact <cit.>.
W.r.t factorisation systems, $(Epi,Mono)$ is generally not a factorisation system for $\EM{T}$, rather $(RegEpi,Mono)$ is. Using that regular epis are the surjective morphisms, and monos are the injective morphisms, one can prove that in $\Coalg_\catC(F_\catC)$ and $\Alg_\catD(G_\catD)$ the surjective and injective morphisms form a factorisation system. We refer to Lemma <ref>.

In particular, $\KHaus$ is the Eilenberg-Moore category of the ultrafilter monad [54].

The monadicity of complex-valued commutative, unital $C^*$-algebras was proved in [56],
see also <cit.>.
This specialises to the real-valued case.
In order to view  $\KHaus \cong\CCStar^\op$ as a concrete duality it seems necessary to enlarge
$\catC$ to e.g. locally compact Hausdorff spaces and $\CCStar$,
since $\bbR$ with the standard topology is not compact, but it is locally compact.
[Need to look closer at <cit.>.]

* $\catC, \catD$ are concrete categories.

* (dual) adjunctions and functors as indicated above.

* $\Obs$ is a finite set of observations.

* $F_\catC(C) = \Spc\FreeD(\Obs)) \times C^\Alph$ ($\catC$ has products).

* $G_\catD(D) = \FreeD(\Omega) + \Alph \cdot D$ ($\catD$ has coproducts).

* $G(X) = \Omega + \Alph \cdot X \cong \Omega + \Alph\times X$.

* $\catC, \catD$ have (Epi,Mono)-factorisation systems.

* For Brzozowski (to get a minimal automaton, not only observable coalgebra): Object of initialisation $\I$ in $\catC$.

automata     $\catC$, $\catD$     $\dua$     $\Obs$

Brzozowski DFA     $\catC=\catD=\Set$     2     1

Brzozowski Moore aut     $\catC=\catD=\Set$     $B$     1

PODFA/DKM     $\catC=\Set$, $\catD=\BA$     2     $\Obs$

Nondeterm. aut ($\Powf$-aut)     $\catC=\catD=\EM{\Powf} = \cat{JSL}$      $\Two$     1

Weighted aut ($\V$-aut)     $\catC=\catD=\SMod = \EM{\V}$     $\S$     1

Linear Weighted aut ($\mathcal{V}_\k$-aut) & $=== 𝒱_$ & $$̨     1

Probabilistic aut ($\D$-aut)     $\catC=\KHaus$, $\catD=\CCStar$     $\Real$     1

Alternating aut ($\N$-aut)     $\CABA = \EM{\N}$, $\Set$     $2$     1

\[\xymatrix{
\cat{Aut}_\catC(\Lang) \ar[r]^-{\ol{\L}'}  &
\cat{Aut}_{\catD^\op}(\rev(\Lang))^\op \ar[d]^-{\blue{reach^\op}}
\\
\cat{Aut}_\catC(\Lang) \ar[d]_-{\blue{reach}}&
\cat{Aut}_{\catD^\op}(\rev(\Lang))^\op \ar[l]_-{\ol{\Spc}'}
\\
\blue{\cat{Aut}_\catC(\Lang)} &

\[\xymatrix{
\Coalg(FT)(\Lang) \text{ over }\Set \ar[d]^-{\det{(-)}} %\ar@/^1pc/[dr]
\\
\Aut_{\EM{T}}^{I,R(O)}(\Lang) \ar[r]^-{\ol{\L}'}  &
\cat{Aut}_{\catD^\op}^{L(I),O}(\rev(\Lang))^\op \ar[d]^-{\blue{reach^\op}}
\\
\cat{Aut}_{\EM{T}}^{I,R(O)}(\Lang) \ar[d]_-{\blue{reach}}&
\cat{Aut}_{\catD^\op}^{L(I),O}(\rev(\Lang))^\op \ar[l]_-{\ol{\Spc}'}
\\
\blue{\cat{Aut}_{\EM{T}}^{I,R(O)}(\Lang)} &

Running Example: Brzozowski for Moore automata (includes classic DFA):

\[\ba{lc}
& \xymatrix@C=1em@R=4em{
\ar@(ul,ur)^-{F} \Set \ar@/^1pc/[rrrr]^-{\cPo} \ar@{}|{\bot}[rrrr] &&&&
\ar@(ul,ur)^-{G^\op} \Set^\op \ar@/^1pc/[llll]^-{\cPo^\op}
\\
\ba{lcl}
F(X) = B \times X^\Alph & \qquad & G(X) = 1 + \Alph\cdot X
\\
I = 1  & \qquad &  \cPo^\op(1) = B^1 \cong B
\ea
%& F\colon \Set \to \Set & F(X) = 2 \times X^\Alph & \\
%& G\colon \Set \to \Set & G(X) = 1 + \Alph\cdot X &
\ea\]

What is the modal logic? The logic of tests of the form: $\Alph^*p$ where $p$ is $B$-valued predicate?

Overview of examples:

automata     $\catC$     $\catD$     dua.obj     restricts to duality?

DFA     $\Set$     $\Set$     2     No

Moore aut     $\Set$     $\Set$     $B$     No

PODFA/DKM     $\Set$     $\BA$     2     $\cat{FSet} \cong \cat{FBA}^\op$

Nondeterm. aut ($\Powf$-aut)     $\EM{\Powf} = \cat{JSL}$     $\EM{\Powf} = \cat{JSL}$      $\Two$
$\cat{JSL} \cong\cat{JSL}^\op$

Weighted aut ($\V$-aut)     $\SMod = \EM{\V}$     $\SMod= \EM{\V}$     $\S$     ? (maybe fin.dim)

Linear Weighted aut ($\mathcal{V}_\k$-aut) & $= 𝒱_$ & $= 𝒱_$  & $$ & $≅^$ (fin.dim.)\\
\hline
Probabilistic aut ($$-aut) & $$  & $$ & $$ & Gelfand: $≅^$\\
\hline
Alternating aut ($$-aut) & $= $ & $$ & $2$ & $≅^$\\
\hline
\end{tabular}
\end{center}
\begin{center}
\begin{tabular}{|l|c|c|c|}
\hline
automata & $\catC$, $\catD$ & dua.obj & restricts to duality?\\
\hline\hline
DFA & $\catC=\catD=\Set$ & 2 & No \\
\hline
Moore aut & $\catC=\catD=\Set$ & $B$ & No\\
\hline
PODFA/DKM & $\catC=\Set$, $\catD=\BA$ & 2 & $\cat{FSet} \cong \cat{FBA}^\op$\\
\hline
Nondeterm. aut ($\Powf$-aut) & $\catC=\catD=\EM{\Powf} = \cat{JSL}$  & $\Two$ &
$\cat{JSL} \cong\cat{JSL}^\op$\\
\hline
Weighted aut ($\V$-aut) & $\catC=\catD=\SMod = \EM{\V}$ & $\S$ & ? (maybe fin.dim) \\
\hline
Linear Weighted aut ($\mathcal{V}_\k$-aut) & $\catC=\catD=\Veck = \EM{\mathcal{V}_\k}$ & $\S$ & $\FVec \cong \FVec^\op$ (fin.dim.)\\
\hline
Probabilistic aut ($\D$-aut) & $\catC=\KHaus$, $\catD=\CCStar$ & $\Real$ & Gelfand: $\KHaus \cong\CCStar^\op$\\
\hline
Alternating aut ($\N$-aut) & $\CABA = \EM{\N}$, $\Set$ & $2$ & $\CABA \cong \Set^\op$\\
\hline
\end{tabular}
\end{center}

% Revisiting existing examples

\section{Revisiting Examples}
\label{sec:old-ex}

%\blue{Show that examples from WoLLIC paper and ACM TOCL paper
%are instances of general framework.}

\subsection{Deterministic Kripke Models}
\label{sec:deterministic}

A central example from~[16]
are deterministic Kripke models (in {\em loc.cit} referred
to as PODFAs, i.e., partially observable DFAs).
%The main difference to the earlier mentioned Moore machines is that
%a state now carries a set of observations and the corresponding
%logic containing Boolean connectives.
We will first recall the definitions of deterministic Kripke models and
their dual Boolean algebras with operators corresponding to a
modal logic of tests.
After that we will see how this duality can be seen
as a special case of our general duality picture, which has as
immediate corollary a minimisation algorithm for the case of finite models.
%discuss the basic setup that builds on the
%dual adjunction between $\Set$ and $\BA$. After that
%We will use this c3onnection to establish  a link to the Moore machine case
In addition, results from Section~\ref{sec:trace-logic} entail that
%our general framework provides a concise argument for why already
the modal test language without propositional  operators
is sufficiently expressive to specify deterministic Kripke models up to bisimulation
and to compute their observable quotient.

%The following definition introduces the main notion of this section.
\begin{definition}
We define \emph{deterministic Kripke models}
to be quintuples $\cS = (S,\Alph,\Obs,\gamma:S\to
2^{\Obs},\delta:S \to S^\Alph)$ where $S$ is a finite set of \emph{states}, $\Alph$ is a finite set
of \emph{actions}, $\Obs$ is a finite set of \emph{observations}, $\delta$
is a \emph{transition function} and $\gamma$ is an \emph{observation function}.
A function $f:S_1 \to S_2$ is a morphism between Kripke models
and $(S_2,\Alph,\Obs,\gamma_2,\delta_2)$
if for all $s \in S_1$ and all $a \in \Alph$ we have
$\gamma_1(s) =\gamma_2(s)$ and $f(\delta_1(s)(a)) = \delta_2(f(s))(a)$.
We let $\cat{DKM}$ denote the category of deterministic Kripke models.
\end{definition}
In other words, deterministic Kripke models are Kripke models where for
each action $a \in \Alph$ the corresponding relation is the graph of a (total) function.
It is well-known that there is a duality between $\mathbf{DKM}$ and a suitable category $\cat{BAO}$ of
Boolean algebras. We will now recall the definition of $\cat{BAO}$ and some known facts
concerning this duality.

\begin{definition}
The category $\cat{BAO}$ of (deterministic) \emph{Boolean algebras with
operators} (BAOs) has as objects Boolean algebras $B$ with the
usual operators $\land$ and $\neg$ with a greatest element $\top$ and
least element $\bot$ together with unary operators $(a):B \to B$, for
each action $a \in \Alph$, such that $(a)$ is a Boolean homomorphism.  For each
observation $\omega \in \Obs$, we also have constants
$\underline{\omega}$.  We denote an object of $\cat{BAO}$ by
$$\cB =
\land,\neg).$$
The $\cat{BAO}$ morphisms  are the usual Boolean homomorphisms
preserving, in addition, the constants and commuting with the unary operators.
Finally we denote by $\cat{FBAO}$ the category of {\em finite} Boolean algebras with
\end{definition}

The following fact is well-known (cf.~e.g.~[19, 36]).

\begin{fact}
There is a dual adjunction between $\cat{Set}$ and $\cat{BA}$ as depicted in Figure~\ref{fig:DKM}
%     \[
%    \xymatrix@C=1em@R=4em{
%   \cat{Set} \ar@/^1pc/[rrrr]^-{\bbP} \ar@{}|{\bot}[rrrr] &&&&
%    \cat{BA}^\op \ar@/^1pc/[llll]^-{\Uf}
%   }
%  \]
given by the contravariant functor $\bbP$
that maps a set to its Boolean algebra of subsets
and the functor  $\Uf\mathrel{:=}\Hom(-,\bf{2})$, ie., the contravariant functor the maps a
Boolean algebra to its collection of ultrafilters.%\marginpar{CK: should we introduce ultrafilters?}
This adjunction restricts to a dual equivalence between the category  $\cat{FSet}$ of finite
sets and the category $\cat{FBA}$ of finite Boolean algebras.
\end{fact}
% \begin{fact}
%    The dual adjunction between $\Set$ to $\BA$ extends to a dual adjunction between
%    $\cat{DKM}$ and $\cat{BAO}$. \marginpar{CK: should we describe how exactly?}
%    In the finite case we obtain a full dual equivalence between the category of
%    finite deterministic Kripke models and the category $\cat{FBAO}$.
% \end{fact}
We are now going to show how this example fits into our general
framework. As a corollary we obtain a minimisation procedure for finite
deterministic Kripke models.

\begin{proposition}\label{prop:DKM(co)alg}
We have the following equivalences:
\begin{enumerate}
\item $  \cat{DKM} \cong \Coalg_\Set(F) $ for $F = 2^\Obs \times X^\Alph$
\item $\cat{BAO} \cong \Alg_\BA(G_\cat{BA})$ for $G_\cat{BA} =  \Phi_{\cat{BA}}(\Obs) + \Alph\cdot X$
\end{enumerate}
\end{proposition}

\begin{figure}
\[\ba{lc}
&   \xymatrix@C=1em@R=4em{
\ar@(ul,ur)^-{F^\op} \cat{Set}^\op \ar@/^1pc/[rrrr]^-{\bbP} \ar@{}|{\top}[rrrr] &&&&
\ar@(ul,ur)^-{G_\cat{BA}} \cat{BA} \ar@/^1pc/[llll]^-{\Uf}
\\
\ba{lcl}
F(X) = 2^\Obs \times X^\Alph & \qquad &
G_\cat{BA}(X) = \Phi_{\cat{BA}}(\Obs) + \Alph\cdot X
\\
I = 1 & \qquad &\Uf(\Phi_{\cat{BA}}(\Obs)) \cong 2^\Obs
\ea
\ea\]
\caption{Functors and base adjunction for deterministic Kripke frames}
\label{fig:DKM}
\end{figure}

Both equivalences are an immediate consequence of the definitions. In the sequel,
we will make no distinction between $F$-coalgebras and deterministic Kripke models and, likewise,
between $G_{\cat{BA}}$-algebras and BAOs.
As a consequence of the proposition we obtain the following duality results by  applying our general framework.
\begin{proposition}
The dual adjunction $\Uf \dashv \bbP$ lifts to a dual adjunction
between $\cat{DKM}$ and $\cat{BAO}$ and to an adjunction between
$\Aut_{\Set}^{1,2^\Obs}$ and $\Aut_{\cat{\BA}}^{2,F\Phi_{\cat{BA}}(\Obs)}$.
If we start with the dual equivalence $\cat{FSet} \cong \cat{FBA}$, both liftings are dual equivalences as well.
\end{proposition}
\begin{proof}
For the dual adjunction between $\cat{DKM}$ and $\cat{BAO}$ recall from Proposition~\ref{prop:DKM(co)alg}
that both categories are equivalent to categories of $F$-coalgebras and $G_\cat{BA}$-algebras for certain functors $F$ and $G_\cat{BA}$, respectively.
Furthermore, we have $\Uf(\Phi_{\cat{BA}}(\Obs)) \cong 2^\Obs$, which follows
from the well-known fact that the set of homomorphisms of type $\Phi_{\cat{BA}}(\Obs) \to \bf{2}$
(i.e., ultrafilters)
is in one-one correspondence with the set of functions of type $\Obs \to 2$.
Therefore the functors $F$ and $G_\cat{BA}$ have the shape required by our general
lifting result from Section~\ref{sec:liftcoalg} and
we obtain functors $\ol{\bbP}: \Coalg(F)^\op \to \Alg(G_\cat{BA})$ and $\ol{Uf}:\Alg(G_\cat{BA}) \to \Coalg(F)^\op$
with $\ol{Uf} \dashv \ol{\bbP}$.

To extend the adjunction $\ol{Uf} \dashv \ol{\bbP}$ between $\Coalg(F)$ and $\Alg(G_\cat{BA})$ further to a dual adjunction $\ol{Uf}' \dashv \ol{\bbP}'$ between
$\Aut_{\Set}^{1,2^\Obs}$ and $\Aut_{\cat{\BA}^\op}^{2,\Phi_{\cat{BA}}(\Obs)}$
- the latter is a slight extension of the former by adding a initial state
to deterministic Kripke models and by viewing BAOs as some kind of automata with acceptance predicate - it suffices to note that
$\bbP 1 \cong 2$ such that the result follows from the general theorem in Section~\ref{sec:liftaut}.

The fact that the obtained adjunctions restrict to equivalences when we replace the base categories
$\cat{Set}$ and $\cat{BA}$ with $\cat{FSet}$ and $\cat{FBA}$, respectively, is a matter of routine checking.
\end{proof}

%  As a corollary from our general picture we obtain a well-known dual adjunction between
%  deterministic Kripke models and BAOs.  Furthermore, this dual adjunction becomes an equivalence when
%  we confine ourselves to the finite case.
% \begin{proposition}\label{prop:dual_podfa}
% 	$\Coalg(F)$ and $\cat{BAO}^\op$ are related via a dual adjunction that is given by two contravariant functors
% 	$\ol{\bbP}: \Coalg(F) \to \cat{BAO}^\op$ and $\ol{\Uf}:  \cat{BAO}^\op \to \Coalg(F)$. For finite
% 	models and algebras we obtain a duality, i.e.,  $\Coalg(F_\mathrm{fin}) \cong \cat{FBAO}^\op$
% 	where $F_\mathrm{fin}:\cat{FSet} \to \cat{FSet}$ is the restriction of $F$ to finite sets.
% \end{proposition}

This shows, in particular, that we get a duality between finite deterministic Kripke models
%automata with observations
and \cat{FBAO}s.  This is the key for obtaining a minimal
realization via logical theories.

\begin{definition}
%To make the above more precise,
Consider the language $\LLang{G_\cat{BA}}$:
\[ \varphi ::=  \top \mid \hat{\omega}, \omega \in \Obs \mid \boxmod{a} \varphi, a \in \Alph \mid \varphi_1\wedge \varphi_2
\mid \neg \varphi. \]
with semantics defined as below \eqref{eq:rho-concrete} on page~\pageref{eq:rho-concrete}.
% Now, for a given automaton $\cS = (S,\gamma,\delta)$ we can define a
% satisfaction relation for the formulas as follows:
% \[
% \begin{array}{lclclcl}
% s\models \top & & \mbox{ always } & \qquad &
% s\models\hat{\omega} & \mbox{ iff }  & \omega\in \gamma(s) \\
% s\models \varphi_1\wedge \varphi_2 &  \mbox{ iff } &  s\models \varphi_1 \mbox{ and } s\models \varphi_2 & &
% s\models\neg \varphi & \mbox{ iff } & s\not\models \varphi \\
% s\models (a) \varphi &  \mbox{ iff }   & \delta(s)(a)\models \varphi.
% \end{array}
% \]
%We say that a formula $\phi$ \textbf{distinguishes} $s_1$ and $s_2$ if
%$s_1\models\phi$ and $s_2\not\models\phi_2$ or \emph{vice versa}.
For a given automaton $\cS = (S,\gamma,\delta)$  we say that a subset $U$ of $S$ is \emph{definable by} $\LLang{G_\cat{BA}}$ if  $U=\sem{\varphi}$% \coloneqq \{s \in S \mid \varphi\}$
for some $\varphi \in\LLang{G_\cat{BA}}$ where we identify the predicate $\sem{\varphi}: S \to 2$ with the set $\{ s \in S \mid \sem{\varphi}(s) =1\}$ .
We let $\mathrm{Def}(\cS) = (\mathrm{Def}(S),\{(a)_\cS \}_{a \in \Alph}, \{\sem{\hat{\omega}}\}_{\omega \in \Obs})$ be the BAO
based on the definable subsets of $\cS$, where $(a)_\cS(\lsem \varphi \rsem) = \lsem \boxmod{a} \varphi \rsem$.

\end{definition}
In other words, the modal logic is the modal logic with (deterministic)
$\Alph$-indexed modalities and atomic propositions from $\Obs$.
For a given deterministic Kripke model, the algebra of definable subsets yields the reachable part (=zero generated subalgebra) of the dual automaton (=algebra).

\begin{proposition}
%  Let $(A,p:A \to 2, \alpha: GA \to A) \in  \Aut_{\cat{BA}^\op}^{2,F_{\cat{BA}}(\Obs)}$, ie.,
%   let $(A,\alpha) \in \Alg(G)$ together with a predicate $p:A \to 2$. Then $(B,p',\beta)$
%   with $p' = \restr{p}{B}$ and $(B,\beta)$ the algebra based
%   of $(A,\alpha)$ is isomorphic to the reachable part of $(A,p,\beta)$.
Let $\cS=(S,\gamma,\delta) \in \cat{DKM}$ be a deterministic Kripke model, $s_I \in S$ an initial state and let $\mathrm{Def}(\cS)  \in \cat{BAO}$ the dual algebra
of definable subset. %s with predicate $p_{s_I}: \mathrm{Def}(\cS) \to 2$ given by $p_{s_I}(U) = 1$ iff $s_I \in U$.
Then $\mathrm{Def}(\cS) \in \cat{BAO}$ is isomorphic to the reachable part  $\reach{\ol{\bbP} (\cS)}$ of %\todo{CK: talk about algebras or automata here?}
$\ol{\bbP} (\cS) \in \cat{BAO}$.
\end{proposition}
\begin{proof}
The result follows from the fact that  the unique morphism  $i_\mathrm{Def}(\cS)$ from the initial $G_{\cat{BA}}$-algebra $\cI$ to $\mathrm{Def}(\cS)$
together with the embedding $m: \mathrm{Def}(\cS) \to \ol{\bbP} (\cS)$ is the
image-factorisation of
$i_{\ol{\bbP} (\cS)}:\cI \to \ol{\bbP} (\cS)$,
which is the $(E,M)$-factorisation obtained from the factorisation system of
surjective and injective Boolean homomorphisms
%\blue{[HH: You have not said what  $\cE$ and $\cM$ are, but I assume they are as in Lemma~\ref{lem:factor-sys}]}
\end{proof}

% The following proposition will show that a definable subset is definable with trace-like tests that
% essentially consist of a sequence of inputs followed by one output.
% \begin{proposition}\label{prop:definable}
%     Let $\cS=(S,\gamma,\delta) \in \cat{DKM}$. Any definable subset $U$ is definable
%     by  Boolean combinations
% of tests of the form
% \[ (a_1)\dots (a_n) \omega \qquad \mbox{ for } \omega \in \Obs.\]
% \end{proposition}
% \begin{proof}
%     %Connect initial algebras + simple argument using that modalities are homomorphisms.
%     To prove the claim we consider the adjunction between $\Set$ and $\cat{BA}$ given
%     by the functors $U \dashv  F_{\cat{BA}}$. Let $G': \Set \to \Set$ be the functor mapping
%     a set $X$ to $\Obs + \Alph \cdot X$. Then by~\ref{} \todo{Helle's fact} we have that there
%     exists an ismorphism of Boolean algebras
%     \[ \kappa: F_{\cat{BA}}(\cI_{G'}) \to \cI_G \]
%     where $\cI_G$ and $\cI_{G'}$ denote the  initial algebras of $G$ and of $G'$, respectively.
%     Moreover, a closer inspection of the definition of $\kappa$ reveals that
%     $$\kappa((a_1)\dots (a_n) \omega) = (a_1)\dots (a_n) \omega$$
%     for $a_1,\dots,a_n \in \Alph$ and $\omega \in \Obs$.
%     As $\kappa$ is a Boolean isomorphism this shows that each element
%     of $\cI_{G}$ is equivalent to a Boolean combination of equivalence classese of elements
%     of the form $(a_1)\dots (a_n) \omega$.
% \end{proof}

% As a consequence we obtain that for the overall minimisation procedure we
% do not have to consider the full reachable part of the dual algebra, but only the part
% that corresponds to the sets definable by tests of the form $ (a_1)\dots (a_n) \omega$.

\begin{definition}
We call a formula $\varphi$ of the form $ \boxmod{a_1}\dots \boxmod{a_n} \omega$ for some $n \in \bbN$
and $a_i \in \Alph$ for $i \in \{1,\dots,n\}$ a trace formula. For a DKM $\cS$ we denote
by $\mathrm{Def}^*(\cS)$ the collection of trace-definable subsets of $\cS$, i.e, the collection
of subsets definable by a trace formula.
\end{definition}

\begin{proposition}
For all DKMs $\cS$ we have
$$\ol{\Uf}(\mathrm{reach}(\ol{\bbP}(\cS))) \cong (\ol{\Uf}(\mathrm{Def}(\cS)) \cong (\ol{\Uf}(\ol{\Phi}_\cat{BA}(\mathrm{Def}^*(\cS))).$$
\end{proposition}
\begin{proof}
%Clearly the collection of trace formulas is isomorphic to $\Trc$. Therefore,
By the results in Section~\ref{sec:trace-logic}, we have
$\Phi_\cat{BA} \Trc$ is isomorphic to the Lindenbaum algebra of  $\LLang{G_\cat{BA}}$.
Therefore the reachable part of $\ol{\bbP}(\cS)$ is obtained as
the image of $\Phi_\cat{BA} \Trc$  under the initial morphism
from $\Phi_\cat{BA} \Trc$ to $\ol{\bbP}(\cS)$ which can be easily checked to be $\Phi_\cat{BA}(\mathrm{Def}^*(\cS))$.
%is generated by closing  $\mathrm{Def}^*(\cS)$ under the Boolean operations.
\end{proof}

We finish with a key observation from~[16] that allows to compute quotients of finite DKMs
via duality.

\begin{corollary}
Given a finite DKM $\cS$, the quotient of $\cS$ modulo bisimulation is isomorphic to   $(\ol{\Uf}(\ol{\Phi}_\cat{BA}(\mathrm{Def}^*(\cS)))$.
\end{corollary}
\begin{proof}
By Prop~\ref{prop:reach-D} we have that $(\ol{\Uf}(\mathrm{Def}(\cS))$ and thus $(\ol{\Uf}(\ol{\Phi}_\cat{BA}(\mathrm{Def}^*(\cS)))$ is observable.
As $\cat{FSet}$ and $\cat{FBA}$ are dually {\em equivalent}, we get
that $(\ol{\Uf}(\mathrm{Def}(\cS))$ and thus $(\ol{\Uf}(\ol{\Phi}_\cat{BA}(\mathrm{Def}^*(\cS)))$ are the maximal quotient of $\cS$.
\end{proof}

% \begin{remark}
%    What I would like to argue now is that for the set of ultrafilters it does not really matter whether we
%    are considering Boolean combinations of $ (a_1)\dots (a_n) \omega$, i.e., all definable subsets, or
%    simply the sets definable by $ (a_1)\dots (a_n) \omega$.
% \end{remark}

% \[\ba{lc}
% &   \xymatrix@C=1em@R=4em{
%     \ar@(ul,ur)^-{F} \cat{FSet} \ar@/^1pc/[rrrr]^-{\bbP} \ar@{}|{\bot}[rrrr] &&&&
%   \ar@(ul,ur)^-{G^\op} \cat{FBA}^\op \ar@/^1pc/[llll]^-{\At}
%   }
%  \\
%  &
%  \ba{lcl}
%  F(X) = 2^\Obs \times X^\Alph & \qquad &
%  G(X) = F_{\cat{BA}}(\Obs) + \Alph\cdot X
%  \\
%  I = 1 & \qquad &\At(F_{\cat{BA}}(\Obs)) \cong 2^\Obs
%  \ea
%  \ea\]

% \begin{remark}
% {\bf TODO} Explain why Boolean connectives are not needed. Issue: We would like to do this by relating the initial $G$-algebra in $\cat{BA}$ to the
% initial $O + \Alph\cdot(-)$-algebra in $\Set$, but there is no initial $G$-algebra over finite Boolean algebras.
% Can this example be placed in the general framwework by taking dual adjunction between $\Set$ and $\cat{BA}$? \blue{Yes we can}
% % \blue{Answer to the latter question is yes, but it's not clear how to relate initial algebras in  meaningful way.
% % A concrete argument seems to be required - abstract nonsense not sufficient. A more general question is what the point is
% % of having both  the $\Set^\op$ and the $\BA$ example. Possible answer: allow for non-determinism and accept that notion of minimality
% % is not the ``right'' one?}
% \end{remark}

\subsection{Weighted Automata}
\label{sec:weighted}

%\blue{[By: Marcello and Alexandra.]}

\subsubsection{Semirings and semimodules} We need some basic definitions on semirings and semimodules to present the example of weighted automata.

Recall that a \emph{semiring} is a tuple $(\S, +, \cdot, 0,1)$ where $(\S, + , 0)$ and $(\S,\cdot, 1)$ are monoids, the former of which is commutative, and multiplication  distributes over finite sums:
\[
\begin{array}{cccccc}
r \cdot 0 = 0 = 0 \cdot r
& \qquad &
r\cdot(s + t) = r \cdot s + r \cdot t
& \qquad &
(r + s)\cdot t = r \cdot t + s \cdot t
\end{array}
\]
We just write $\S$ to denote a semiring. Examples of semirings are:  every field, the Boolean semiring $2$, the semiring $(\Nat,+, \cdot, 0, 1)$ of natural numbers, and the tropical semiring $(\Nat \cup \{\infty\}, \min, +, \infty, 0)$.  All these semirings are examples of {\em commutative} semirings, as the $\cdot$ operation is also commutative.

For a semiring $\S$, an \emph{$\S$-semimodule} is a commutative monoid $(M, +, 0)$ with a left-action $\S \times M \to M$ denoted by juxtaposition $rm$ for $r \in \S$ and $m \in M$, such that for every $r,s \in \S$ and every $m, n \in M$ the following laws hold:
\[
\begin{array}{rcl@{\qquad}rcl}
(r+s)m & = & rm + sm & r(m+n) & = & rm + rn \\
0m &  = & 0 & r0 & = & 0 \\
1m &  = & m & r(sm) & = & (r \cdot s) m
\end{array}
\]
Every semiring $\S$ is an $\S$-semimodule, where the action is taken to be just the semiring multiplication.  Semilattices are another example of semimodules (for the Boolean semiring $\S$).

An $\S$-semimodule homomorphism is a monoid homomorphism $h\colon M_1 \to M_2$ such that
$h(rm) = rh(m)$ for each $r \in \S$ and $m \in M_1$.  $\S$-semimodule homomorphisms are also
called $\S$-\emph{linear maps} or simply \emph{linear maps}.  The set of all linear maps from a $\S$-semimodule $M_1$ to $M_2$
is denoted by $\SMod(M_1,M_2)$.

\emph{Free $\S$-semimodules} over a set $X$ exist and can be built using
the functor $\V \colon \Set \to \Set$ defined on sets $X$ and maps $h\colon X \to Y$
as follows:
\[
\begin{array}{lcl}
\label{eq:V}
\V (X) & = &  \{\, \varphi\colon X \to \S \mid \text{$\varphi$ has finite support}\,\},
\\[1em]
\V (h(\varphi)) & = & \big(y \mapsto \sum_{x \in h^{-1}(y)} \varphi(x)\big),
\end{array}
\]
where a function $\varphi\colon X \to \S$ is said to have finite support if $\varphi(x) \neq 0$ holds
only for finitely many elements $x \in X$. $\V(X)$ is the free $\S$-semimodule on $X$ when equipped with the following pointwise
$\S$-semimodule structure:
\[
(\varphi_1 + \varphi_1 )(x) = \varphi_1(x) + \varphi_2(x)
\;\;\;\;
(s\varphi_1)(x) = s \cdot \varphi_1(x) \,.
\]
We sometimes  write the elements of $\V(X)$ as formal sums $s_1x_1 + \ldots + s_nx_n$ with $s_i \in \bbS$ and $x_i \in X$.
%\V(X) = \{ s_1x_1 + \ldots + s_nx_n \mid s_i \in \bbS, x_i \in X\}.$$
$\V(X)$ is a monad and the category of Eilenberg-Moore algebras is $\SMod$,
the category of $\bbS$-semimodules and $\bbS$-linear maps. As usual, free $\bbS$-semimodules enjoy the following universal property: for every function $h\colon X \to M$ from a set $X$ to a semimodule $M$, there exists a unique linear map $h^{\sharp}\colon \V(X) \to M$ that is called the \emph{linear extension} of $h$.

We can define for an $\S$-semimodule $M$ its \emph{dual space} $M^\star$ to be the set $\SMod(M,\S)$ of all linear maps
between $M$ and $\S$, endowed with the $\S$-semimodule structure obtained
by taking pointwise addition and monoidal action: $(g + h)(m) = g(m) + h(m)$, and
$(sh)(m) = s \cdot h(m)$.  Note that $\S \cong V(1)$ and that $\S^\star = \SMod(\S,\S) \cong \S$.

\subsubsection{Weighted automata and weighted languages}

A \emph{weighted automaton} with finite input alphabet $\Sigma$ and weights over a semiring
$\S$ is given by a set of states $X$, a function $t\colon X \to \V(X)^\Sigma$ (encoding
the transition relation in the following way: the state $x \in X$ can make a transition to $y \in X$
with input $a \in \Sigma$ and weight $s \in \S$ if and only if $t(x)(a)(y) = s$), a final state
function $f\colon X \to \S$ associating an output weight with every state, and an initial
state function $i\colon 1 \to \V(X)$. Diagrammatically:

\[
<EMAIL_ADDRESS>1\ar[rd]^{i}  & & {\bbS}&  && %& \blue{\bbS}
\\
& X \ar[ru]^f \ar[d]^t & &&%s&\bbS^{\Alph^*} \ar[ru]^{o} \ar[d]^{d}
\\
&  \V(X)^\Alph &&&%& (\bbS^{\Alph^*})^\Alph
\]

The function $t\colon X \to \V(X)^\Sigma$ can be inductively extended to words $w\in \Sigma^*$:
\begin{align*}
t(x)(\varepsilon) &= 1.x \\
t(x)(aw) &= v_1 t (x_1)(w) + \cdots +v_n t (x_n)(w) \text{, where }  t(x)(a)=v_1x_1+ \cdots +v_nx_n
\end{align*}

Weighted automata recognise functions in $\S^{\Sigma^*}$, or \emph{formal power series over $\S$}.
More precisely, the formal power series recognised by a weighted automaton $\str{X} = (X,t,i,f)$
is the function $L(\str{X})\colon \Sigma^* \to \S$ that maps $w \in \Sigma^*$ to $f(t(i)(w)) \in \S$. More concretely, the value $L(\str{X})(w)$, for $w=a_1a_2\cdots a_n$, is the  sum of all $v_1 \cdot \ldots \cdot v_{n} \cdot f(x_{n+1})$ over all paths $p_w = x_1\xrightarrow{a_1,v_1} \ldots \xrightarrow{a_{n},v_{n}} x_{n+1}$ labelled by $w$. The value of $L(\str{X})(w)$ can be easily computed using the usual matrix representation of linear maps: the initial state function $i$ is then a column vector, the final state function $f$ is a row vector, and the transition relation $t$ can be represented as a $\Sigma$-indexed collection of $X\times X$-matrices $t_a$ where $t_a(y,x) = t(x)(a)(y)$ for all $x,y \in X$. $L(\str{X})(w)$ is then obtained by the following matrix multiplication $f \times t_{a_n} \times \ldots \times t_{a_0} \times i$.

Observe that $\bbS$ is (isomorphic to) the carrier of the free Eilenberg-Moore $\V$-algebra
on one generator $\V(1)$.
Hence, as described in Section~\ref{sec:det}, we can determinise a weighted automaton $\left <f,t\right >\colon X \to \bbS \times (\V X)^\Alph$ into a Moore automaton over $\SMod$.

1\ar[rd]^{i}  & & {\bbS}\ar@{-->}[rrrr]&  && & {\bbS}
\\
& X \ar[ru]^f \ar[d]^t \ar[r]^\eta&V(X)\ar[ld]^{t^\sharp}\ar[u]^{f^\sharp}\ar@{-->}[rrr]
& &&\bbS^{\Alph^*} \ar[ru]^{o} \ar[d]^{d}
\\
&  V(X)^\Alph \ar@{-->}[rrrr]&&&& (\bbS^{\Alph^*})^\Alph

%Brzozowski for weighted languages: given a weighted automaton we want a {\bf canonical} representative of the image in the final coalgebra -- Moore automaton.
The unique map into final Moore automaton of weighted languages gives precisely the language semantics concretely given above.

\subsubsection{Brozowski for Weighted Automata}

There is self-dual adjunction of $\SMod$ obtained by taking dual space: ${(-)^* = \SMod(-,\bbS)}$.
A special case is the self-dual adjunction of vector spaces in case $\S$ is a field,
which restricts to a duality between finite-dimensional vector spaces.
This duality was used in [16] to obtain observable Moore automata over vector spaces.

We lift the base adjunction to one between Moore automata in $\SMod$ using Theorem~\ref{thm:liftaut}.
Let $\catC=\catD=\SMod=\EM{\V}$  and
$F_\SMod(X) = \bbS \times X^\Alph$ and $G_\SMod(X) = \bbS + \Alph\cdot X$.
Since $\S^* \cong \S$,
the conditions for Theorem~\ref{thm:liftaut} hold, and the adjunction lifts,
as illustrated here:
\[\xymatrix@C=1em@R=4em{
\left(\Aut_{\SMod}^{\S,\S}\right)^\op \ar@/^1pc/[rrrr]^-{\ol{(-)^*}'} \ar@{}|{\top}[rrrr] \ar[d] &&&&
\Aut_{\SMod}^{\S,\S} \ar@/^1pc/[llll]^-{\ol{(-)^*}'} \ar[d]
\\
\ar@(dl,dr)_-{F_\SMod} \SMod^\op \ar@/^1pc/[rrrr]^-{{(-)}^*} \ar@{}|{\top}[rrrr] &&&&
\ar@(dl,dr)_-{G_\SMod^\op} \SMod \ar@/^1pc/[llll]^-{{(-)}^*}
\]
We can now give the Brzozowski algorithm for weighted automata
by instantiating \textbf{Algo2} of Theorem~\ref{thm:min-algo} for the determinised automaton.
Start with a weighted automaton in $\Set$, determinise it into a Moore automaton in $\Aut_\SMod^{\S,\S}$ (to have a canonical representative of the accepted language), reverse and determinise, take the reachable part (w.r.t $G_\SMod$-structure over $\SMod$), reverse and determinise, take the reachable part again. Diagramatically, \textbf{Algo2} is (putting $^\op$ on the right-hand side to start and end in $\Aut_{\SMod}^{\S,\S}$):
\[\xymatrix{
{\cat{WAut} \text{ over }\Set} \ar[d]^-{(-)^\sharp} \ar@/^1pc/[dr]
\\
\Aut_{\SMod}^{\S,\S} \ar[r]^-{\ol{(-)^*}'}  &
\left(\Aut_{\SMod}^{\S,\S}\right)^\op\ar[d]^-{{reach^\op}}
\\
\cat{Aut}_\SMod^{\S,\S} \ar[d]_-{{reach}}&
\left(\Aut_{\SMod}^{\S,\S}\right)^\op \ar[l]_-{\ol{(-)^*}'}
\\
\Aut_{\SMod}^{\S,\S}
\rem{
\[\xymatrix{
%{\cat{WAut} \text{ over }\Set} \ar[d]^-{(-)^\sharp} \ar@/^1pc/[dr]
\left(\Aut_{\SMod}^{\S,\S}\right)^\op \ar[r]^-{\ol{(-)^*}'}  &
\cat{Aut}_\SMod^{\S,\S} \ar[d]^-{{reach}}
\\
\left(\Aut_{\SMod}^{\S,\S}\right)^\op \ar[d]_-{{reach^\op}}&
\cat{Aut}_\SMod^{\S,\S}\ar[l]_-{\ol{(-)^*}'}
\\
\left(\Aut_{\SMod}^{\S,\S}\right)^\op
At this point we have built a minimal Moore automaton accepting the same language as the weighted automaton we started with and, moreover, the state space is a subsemimodule of the semimodule generated by the original state space.

The last step missing is to recover a weighted automaton in $\Set$, with as state space the generators of the state space of the  minimal Moore automaton resulting after applying our Brzozowski algorithm.
Unfortunately, subsemimodules of free, finitely generated semimodules are not necessarily free and finitely generated. Therefore our construction does not guarantee, in general, that the resulting automaton is actually a weighted automaton in $\Set$. Fortunately, we know from a result of Tan~[71] that for a commutative semiring $\S$, every nonzero subsemimodule $N$ of a finitely generated free $\S$-semimodule $M$ is free if and only if $\S$ is a principal ideal domain (\cite[Theorem 4.3]{tan16}). Furthermore, because $N$ is free, it follows that it is also finitely generated and of rank smaller than that of $M$ [(\cite[Theorem 4.3]{tan16}). In other words, the minimal weighted automaton over a principal ideal domain exists and has a state space smaller or equal than that of the original automaton if the latter is finite.

Recall that a principal ideal domain is an integral domain in which every ideal is principal, i.e., can be generated by a single element. Examples include any Euclidean domain, thus any field, the ring of integers, the ring of polynomials in one variable with coefficients in a field, and the ring of formal power series over a field and one variable. The ring of polynomials in two or more variables and the ring of polynomials with integer coefficients are not principal ideal domains.

\subsection{Topological Automata via Gelfand Duality}
\label{sec:top-gelfand}

%\blue{[By: Prakash.]}

A very popular model heavily used in reforcement learning is the
\emph{partially observable Markov decision process} (POMDP).  The idea is
that one can only see the observations and not exactly which state the
system is in.  Many algorithms in machine learning deal with this situation
by constructing a new automaton called the \emph{belief automaton}.  The
state space of this automaton is the set of probability distributions on
$S$.  When seeking to minimize this using duality~[16],
the original idea was to exploit the fact that the state space of the
belief automaton is a compact Hausdorff space and use Gelfand duality.
However, we have since felt that convex duality is a better match for this
situation.  Nevertheless, the notion of a topological automaton is
interesting in its own right and may be the basis for later extensions and
examples.  This section, therefore develops Gelfand duality and its
application to topological automata.

Given a finite set $X$ we write \(\SubD{X}\) for the set of discrete
\emph{sub}distributions on $X$ endowed with the relative topology when
viewed as a subset of \([0,1]^X\).  This is a compact Hausdorff space.
\begin{definition}
A \textbf{compact Hausdorff automaton} is a $5$-tuple
\[ \mathcal{H} = (S,t:S\x\Sigma\to S, f:S\to\SubD{\Obs}) \]
where $S$ is a compact Hausdorff space, $\Alph$ is a finite set of actions
or inputs, $\Obs$ is a finite set of observations, $t$ is a
\emph{continuous} transition function and $f$ is a continuous
observation function.
\end{definition}

We recall a few basic facts about $C^*$-algebras, and refer to
[13, 18, 43, 61] for further information.
Usually $C^*$-algebras are considered as algebras over the complex field.
Here, we are concerned with probabilistic computation, and therefore we
consider $C^*$-algebras over the field $\bbR$ of real numbers.

A \emph{(real-valued) Banach algebra} $A$ is Banach space (complete normed
real vector space) equipped with an associative multiplication such that
\( \norm{xy} \leq \norm{x}\norm{y}\)
for all $x,y$.  This requirement makes multiplication continuous in the
norm topology.  A \emph{(real) $C^*$-algebra} is a Banach algebra together
with an \emph{involution} $(-)^*$ which is a linear, norm-preserving map on
$A$ such that $(xy)^* = y^*x^*$ and $(x^*)^*$, and which in addition
satisfies the $C^*$-axiom: $\|x^*x\| = \|x\|^2$ for all $x \in A$.  A
$C^*$-algebra $A$ is \emph{unital} if it has a multiplicative unit $1$
whose norm is $1 \in \bbR$, and $A$ is \emph{commutative} if the
multiplication is commutative.

A \emph{homomorphism of $C^*$-algebras} is a bounded, linear map that
preserves the multiplication and the involution.  A homomorphism of unital
$C^*$-algebras is additionally required to preserve the unit.  We denote by
$\CCStar$ the category of unital, commutative, real-valued $C^*$-algebras
and their homomorphisms.

In [56] it was shown~\footnote{Strictly speaking, she
showed it for complex-valued $C^*$-algebras, but the result also holds
for real-valued ones.}
that $U$ has a left adjoint
$M \colon \Set \to \CCStar$ given by
\begin{eqnarray}\label{eq:free-cstar}
M(X) & = & C([0,1]^X) = \{ f\colon [0,1]^X \to \bbR \mid f \text{ continuous}\}\\
M(g\colon X \to Y) & = & f (v \circ g) \quad \text{ where } f\in C([0,1]^X), v \in [0,1]^Y.
\end{eqnarray}
where $[0,1]^X$ is equipped with the product topology.

We denote by $\KHaus$ the category of compact Hausdorff spaces and
continuous maps.  Given a compact Hausdorff space $X$, the hom-set
$\Cont(X)= \Hom_\KHaus(X,\bbR)$ becomes a commutative, unital, real-valued
$C^*$-algebra by defining operations pointwise. In particular, the unit is
the constantly 1 map, and for $f \in \Cont(X)$, and the norm is
$\|f\| = \sup\{|f(x)| \mid x \in X\}$; recall that for a compact space and
a continuous function the supremum is attained.  For a morphism
$g \colon X \to Y$ in $\KHaus$, defining $\Cont(g)(h) = h \circ g$ makes
$\Cont(-)$ a functor from $\KHaus$ to $\CCStar^\op$.

Conversely, for $A \in \CCStar$, the set $\hat{A} = \Hom_\CCStar(A,\bbR)$
becomes a compact Hausdorff space (called the \emph{spectrum of $A$}) by
equipping it with the weak $^*$-topology $\tau$ which is generated by the
sets $O_x = \{ \Phi \in \hat{A} \mid \Phi(x) \neq 0 \}$ for all $x \in A$.
We define $\Spec(A) = (\hat{A},\tau)$.  For a morphism $h\colon A \to B$ in
$\CCStar$, defining $\Spec(h)(\Phi) = \Phi \circ h$ makes $\Spec$ a functor
from $\CCStar^\op$ to $\KHaus$.

The functors $\Cont$ and $\Spec$ establish a dual equivalence between
$\KHaus$ and $\CCStar$ known as Gelfand duality
\begin{equation}\label{eq:gelfand-dua}
\xymatrix@R=4em{
\KHaus \ar@/^1pc/[r]^-{\Cont} \ar@{}|{\cong}[r] &
\CCStar^\op \ar@/^1pc/[l]^-{\Spec}
\end{equation}

For the purposes of this paper, we only need a dual adjunction.  We will
take $\Cont$ to be the right adjoint.  As this dual adjunction is in fact a
dual equivalence, the unit and the counit of this adjunction are natural
isomomorphisms.  The unit $\eta_A\colon A \to \Cont(\Spec(A))$ is
known as the \emph{Gelfand transform}, and is given by
$\eta_A(x)(\Phi) = \Phi(x)$.  For all $A \in \CCStar$, $\epsilon_A$ is
an isometric isomorphism in $\CCStar$.

We will lift the base dual adjunction between $\KHaus$ and $\CCStar$ to an
adjunction between the category $\cat{CHA}$ of compact Hausdorff automata
and $\cat{CAO}$ of $\CCStar$-automata. These are obtained from
$F$-coalgebras and $G$-algebras, respectively, where
\begin{equation}\label{eq:gelfand-fctrs}
\ba{lll}
F \colon \KHaus \to \KHaus,   & F(X) = \SubD(\Obs) \times X^\Sigma \\
G \colon \CCStar \to \CCStar, & G(A) = M(\Obs)/J + \Sigma\cdot A
\ea\end{equation}
where $\SubD(\Obs)$ is the set of discrete, subdistributions on the set
$\Obs$ of observations equipped with the relative topology viewed as a
subset $\SubD(\Obs) \subseteq [0,1]^\Obs$. This makes $\SubD(\Obs)$ a
compact Hausdorff space.
Recall from \eqref{eq:free-cstar} that $M$ is the
left adjoint of the unit interval functor $U$.  Finally, $J \subseteq M(\Obs)$ is an
ideal of the $\CCStar$-algebra $M(\Obs)$ which we describe in a moment.
Note that $\CCStar$ has coproducts.  This can readily be seen from the fact
that $\KHaus$ has products and using Gelfand duality.

In order to lift the base dual adjunction $\Spec \dashv \Cont$
to a dual adjunction between $\Coalg(F)$ and $\Alg(G)$ as
in section~\ref{sec:liftcoalg},
we need to show that $\Spec(M(\Obs)/J) \cong \SubD(\Obs)$.
First, we define the ideal $J$.
Fix a finite set $Y$ and consider the $C^*$-algebra $M(Y) \in \CCStar$
defined by \([0,1]^Y\).
For each $y \in Y$, we have a projection map $\pi_y \in M(Y)\to \Real$
given by $\pi_y(v) = v(y)$.  Let $\pi = \sum_{y \in Y}\pi_y$.
Then $\pi\colon [0,1]^Y \to \Real$ is linear and $\pi \in  M(Y)$.
We will take $J$ to be the ideal corresponding to the congruence generated
by the equality obtained by rewriting $\pi \pleq 1$ as an equality as
\[\begin{array}{rcl}
\pi \pleq 1 & \iff & \pi \lor 1 = 1 \\
& \iff & \tfrac{1}{2}(\pi+1) + \tfrac{1}{2}|\pi+1| = 1\\
& \iff & |1 - \pi| = 1 - \pi
\end{array}\]

\begin{definition}\label{def:cong-J}
We define the ideal $J$ of $M(Y)$ as the principal ideal generated by the
element $(|\pi^-| - \pi^-)$ where  $\pi^- := 1-\pi$. That is,
\[
J = \{ m \in M(Y) \mid \exists k \in M(Y): m = k(|\pi^-| - \pi^-)\}.
\]
The congruence relation  $\icong{J}$ on $M(Y)$ arising from the ideal $J$
is then defined standardly as follows:
For $m, n \in M(Y)$, $m \icong{J} n \quad\text{ if }\quad  m-n \in J.$
We write $M(Y)/J$ for the quotient of $M(Y)$ with respect to $\icong{J}$.
\end{definition}

The rather technical proof of the following isomorphism lemma is in Appendix~\ref{app:topo-aut-iso}.

\begin{lemma}\label{lem:topo-aut-iso}
For any set $Y$,  $\SubD(Y) \cong \Spec(M(Y)/J)$ in $\KHaus$.
\end{lemma}
\rem{
\begin{proof}
Let $\alpha\colon \SubD(Y) \to \Spec(M(Y)/J)$ be defined by
$\alpha(\phi)(m) = m(\phi)$ where $\phi \in \SubD(Y)$ and $m \in M(Y)$.
Note that this is well defined.  If $m \icong{J} m'$ then their
difference lies in $J$ which means that
\(m(\phi) - m'(\phi) =k(\phi)(|\pi^-|-\pi^-)(\phi)\).
This condition is equivalent to \(1-\pi\)
is positive and hence $|\pi^-|$ and $\pi^-$ are equal and hence the
second term is $0$, whence \(m(\phi) = m'(\phi)\).
Note that the topology of \(\Spec(M(Y)/J)\)
is generated by the taking as the closed sets, sets of maximal ideals
that contain a fixed element $\phi$ of $M(Y)$.  Any maximal ideal
consists of the functions that vanish at a point $y$, call this $m_y$.
So if we fix such an $\phi$ for it to be in a maximal ideal $m_y$, we
have $\phi(y) =0$.  This means that $\alpha^{-1}$ of a closed set is the
set of subdistributions that assign $0$ to a particular element $y$; this
is a closed set so $\alpha$ is continuous.

Let $\beta\colon \Spec(M(Y)/J) \to \SubD(Y)$ be defined by
$\beta(\Phi)(y) = \Phi(\pi_y)$ where $\pi_y \in M(Y)/J$ projects onto $y$.
We check that $\beta(\Phi)$ is a subdistribution:
\[\sum_{y\in Y}\beta(\Phi)(y)
= \sum_{y\in Y}\Phi(\pi_y)
= \Phi\left(\sum_{y\in Y} \pi_y \right)
\pleq \Phi(1) = 1
\]
The second and last identity hold because $\Phi$ is a
$\CCStar$-homomorphism (hence linear and unital);
the inequality holds since we are in $M(Y)/J$ (which says that $\pi\pleq
1$) and $\Phi$ is monotone.

We now show that for $\phi \in \SubD(Y)$,
$\beta(\alpha(\phi)) = \phi$. Let $y \in Y$, we then have:
\beta(\alpha(\phi))(y) = \alpha(\phi)(\pi_y) = \pi_y(\phi) = \phi(y)
We show that for $\Phi \in \Spec(M(Y)/J)$, $\alpha(\beta(\Phi)) = \Phi$.
Let $m\in M(Y)$, we then have
\alpha(\beta(\Phi))(m) = m(\beta(\Phi)).
By the Stone-Weierstrass theorem, the polynomials on the compact Hausdorff
space $[0,1]^Y$ are dense in $\Cont([0,1]^Y)$.
Since $m \colon [0,1]^Y \to \bbR$ is continuous,
it therefore suffices to show that for all polynomials $p$ on $[0,1]^Y$ we
have that $p(\beta(\Phi)) = \Phi(p)$.

\emph{Case $p = 1$:} $p(\beta(\Phi)) = 1 = \Phi(1) = \Phi(p)$.
\emph{Case $p = r \in \bbR$:} $p(\beta(\Phi)) = r = \Phi(r) = \Phi(p)$.
\emph{Case $p = \sum_{y\in Y} r_y \pi_y$:}
$\Phi(p) = \Phi(\sum_{y\in Y} r_y \pi_y) = \sum_{y \in Y}r_y\Phi(\pi_y) = \sum_{y \in Y} r_y\beta(\Phi)(y) = p(\beta(\Phi))$.
Finally, let $p = \sum_{y\in Y} r_y \pi_y$ and $q = \sum_{y\in Y} s_y \pi_y$.
\Phi(pq) = \Phi(p)\Phi(q) = p(\beta(\Phi))q(\beta(\Phi)) = (pq)(\Phi).
It follows that $p(\beta(\Phi)) = \Phi(p)$ holds for all polynomials
$p$\footnote{Clearly all polynomials can be expressed as sums of products
of lower degree polynomials.}
and we have now shown that $\alpha \colon \SubD(Y) \to \Spec(M(Y)/J) $ is a
bijection with inverse $\beta$.
\end{proof}

From Lemma~\ref{lem:topo-aut-iso} and section~\ref{sec:liftcoalg},
it follows that the base dual adjunction
lifts to one between $F$-coalgebras and $G$-algebras.
\[\xymatrix@R=4em{
\cat{CHA}^\op \ar@/^1pc/[r]^-{\ol{\Cont}} \ar@{}|{\top}[r] \ar[d] &
\quad \cat{CAO} \ar@/^1pc/[l]^-{\ol{\Spec}} \ar[d] \\
\KHaus^\op \ar@/^1pc/[r]^-{\Cont} \ar@{}|{\top}[r] &
\CCStar \ar@/^1pc/[l]^-{\Spec}
\]

The abstract algorithm \textbf{Algo1} applies
since $\KHaus$ and $\CCStar$ are monadic over $\Set$
In particular, $\KHaus$ is the Eilenberg-Moore category of
the ultrafilter monad [54].
In order to show that the associated trace logic is expressive
we need an extra argument, since the functor $F$
defined in \eqref{eq:gelfand-fctrs} does not have the shape required
by Lemma~\ref{lem:comp-adj} and Theorem~\ref{thm:min-algo}.
However, we can apply Remark~\ref{rem:subF} after observing
the following.
Let $F' := \Spec(M(\Omega)) \times (-)^\Alph$.
Then % we know from Proposition~\ref{prop:trc-expressive}
the associated natural isomorphism
${\xitrc}' \colon F' \Spec M \To \Spec M G$
specifies semantics of trace logic over $F'$-coalgebras.
To obtain a suitable $\tau \colon F \To F'$ note that
quotienting with $J$ in $\CCStar$ yields an epi
$e: M(O) \surj M(O)/J$
from which we get a mono in $\KHaus$
$\Spec(e): \Spec(M(O)/J) \inj \Spec(M(O))$.
Pre-composing $\Spec(e)$ with the isomorphism
$h: SubD(O) \stackrel{\sim}{\to} Spec(M(O)/J)$ given
by Lemma~\ref{lem:topo-aut-iso}
and defining
$\tau := (Spec(e) \circ h) \times id$,
it follows that
$\tau \colon F \To F'$ has all components mono in $\KHaus$.
It now follows that trace logic is also expressive for
$F$-coalgebras, i.e., for compact Hausdorff automata.

\begin{remark}
In order to view Gelfand duality \eqref{eq:gelfand-dua}
as a concrete dualty obtained from a dualising object,
we need to expand the setting a bit,
since $\bbR$ is not a compact Hausdorff space. %but it is locally compact.
This can be done by considering the dual adjunction
between locally compact Hausdorff spaces and
not-necessarily unital commutative $C^*$-algebras.
Gelfand duality is a restriction of this dual adjunction.
\end{remark}

% New Examples
%\section{New Examples}

\section{Alternating Automata}
\label{sec:alternating}

%\blue{[By: Dexter.]}

% commented out since in main file
%\section{Alternating Automata}

\emph{Alternating finite automata} (aka \emph{Boolean automata} or \emph{parallel automata}) were first studied in [49, 29, 28, 53, 25] as a finite-state analog of alternating Turing machines. Let $\Sigma$ be a fixed finite
\emph{input alphabet}. An \emph{alternating finite automaton} (AFA) over $\Sigma$ is a tuple $\A = (X,\iota,\delta,F)$, where
\begin{itemize}
\item
$X$ is a finite set of \emph{states},
\item
$F\subs X$ are the \emph{final states},
\item
$\delta : \Sigma \to X \to 2^X \to 2$ is the \emph{transition function}, and
\item
$\iota : 2^X \to 2$ is the \emph{acceptance condition}.
\end{itemize}
Intuitively, the machine $\A$ operates as follows. Let $k=\len X$.
Initially $k$ processes are started, each assigned to a different state, reading the first symbol
of the input word $w\in\Sigma^*$.
In each step, a process at state $s$ reads the next input symbol $a$ and
spawns $k$ child processes, each of which moves to a different state and continues in the same fashion,
while the parent process at $s$ waits for the child processes to report back a Boolean value. In this way
a $k$-branching computation tree is generated. When the end of the input word is reached,
a process at state $s$ reports 1 back to its parent if $s\in F$, 0 otherwise.
A non-leaf process waiting at state $s$, having read input symbol $a$, collects the $k$-tuple
$b\in 2^X$ of Boolean values reported by its children, computes $\delta asb$, and
reports that Boolean value back to its parent. When the initial processes have all received
values, say $c\in 2^X$, the machine accepts if $\iota c=1$, otherwise it rejects.

Alternating automata accept all and only regular sets. It was shown in [50] by
combinatorial means that a language $L\subs\Sigma^*$ is accepted by a $k$-state AFA iff its reverse
$\set{w^R}{w\in L}$ is accepted by a $2^k$ state deterministic finite automaton (DFA).

Our purpose in this section is to recast this result in the framework of our general duality principle.
The duality involves \emph{complete atomic Boolean algebras} (\CABA) and \emph{discrete spaces} (\Set), which underlie \emph{powerset Boolean algebras}.

\subsection{\CABA, \EMN, and \Setop}
\label{sec:CABA-EMN}

\subsubsection{\CABA}

A \emph{complete Boolean algebra} (\CBA) is a structure $(B,\neg,\bigvee,\bigwedge,0,1,{\le})$, where $B$ is a set, $\neg$ is a unary operation on $B$, $\bigvee$ and $\bigwedge$ are infinitary operations on the powerset of $B$, $0$ and $1$ are constants, and $\le$ is a partial order on $B$, such that
\begin{itemize}
\item
$(B,\neg,\vee,\wedge,0,1,{\le})$ is an ordinary Boolean algebra (\BA), where $\vee$ and $\wedge$ are the restrictions of $\bigvee$ and $\bigwedge$, respectively, to two-element sets; and
\item
$\bigvee A$ and $\bigwedge A$ give the supremum and infimum of $A$, respectively, with respect to $\le$.
\end{itemize}
The morphisms of \CBA are \BA homomorphisms that preserve $\bigvee$ and $\bigwedge$.

An \emph{atom} of a \BA is a $\le$-minimal nonzero element. A \BA is \emph{atomic} if every nonzero element has an atom $\le$-below it. A \emph{complete atomic Boolean algebra} (\CABA) is an atomic \CBA. The morphisms of \CABA are just the morphisms of \CBA.

%The axiomatization of {\CBA}s and {\CABA}s is an infinitary universal equational Horn axiomatization. Specifically, the axiomatization of \CBA consists of
%equational axioms of Boolean algebra with respect to $\neg,\vee,\wedge,0,1$;
%for $a\subs B$ and $x\in a$, $x \le \bigvee a$;
%$(\forall x\in a\ \ x \le y) \Imp \bigvee a \le y$;
%for $a\subs B$ and $x\in a$, $\bigwedge a \le x$;
%$(\forall a\in A\ \ x \le a) \Imp x \le \bigwedge A$.

It is known that every \CABA is isomorphic to the powerset Boolean algebra on its atoms,
thus every element is the supremum of the atoms below it.
{\CBA}s and {\CABA}s satisfy infinitary de Morgan and distributive laws:
\begin{align*}
\neg\bigvee a &= \bigwedge\set{\neg x}{x\in a}
& (\bigvee a) \wedge x &= \bigvee \set{y\wedge x}{y\in a}\\
\neg\bigwedge a &= \bigvee\set{\neg x}{x\in a}
& (\bigwedge a) \vee x &= \bigwedge \set{y\vee b}{y\in a}
\end{align*}
as well as other useful infinitary properties such as commutativity, associativity, and idempotence of $\bigvee$ and $\bigwedge$. The free \CABA on generators $X$ is the powerset \CABA $(\TTwo X,\bigcup,\bigcap,\setcompl,\emptyset,2^X)$.
See [38, 37, 55, 66] for further information on the theory of {\CBA}s and {\CABA}s.

%For \CABA, we include the axiom
%for $a\subs B$, $\bigvee_{b\subs a} (\bigwedge_{x\in b} x \wedge \bigwedge_{x\in a-b} \neg x) = 1$.
%This axiom is sound. For an atom $z$, let $\up z=\set{x\in B}{z\le x}$, the principal ultrafilter of $B$ on $z$. For any $a\subs B$,
%z &= \bigwedge\up z
%\le \bigwedge_{x\in a\cap\up z} x \wedge \bigwedge_{x\in a-\up z} \neg x
%\le \bigjoin_{b\subs a} (\bigwedge_{x\in b} x \wedge \bigwedge_{x\in a-b} \neg x).
%Thus if $B$ is atomic, then $1\wedge\neg(\bigjoin_{b\subs a} (\bigwedge_{x\in b} x \wedge \bigwedge_{x\in a-b} \neg x))=0$, because otherwise it must have an atom below it, which we have just shown cannot happen.
%Conversely, any \CBA\ that satisfies the atomicity axiom is atomic. Taking $a=B$ in the atomicity axiom, for any $y\ne 0$ we have
%y &= y\wedge 1 = y \wedge (\bigvee_{b\subs B} (\bigwedge_{x\in b} x \wedge \bigwedge_{x\not\in b} \neg x))
%= \bigvee_{b\subs B} (y \wedge \bigwedge_{x\in b} x \wedge \bigwedge_{x\not\in b} \neg x) \ne 0,
%so for some $b\subs B$ we must have
%\bigwedge_{x\in b} x \wedge \bigwedge_{x\not\in b} \neg x \ge y \wedge \bigwedge_{x\in b} x \wedge \bigwedge_{x\not\in b} \neg x &\ne 0.
%Taking $z = \bigwedge_{x\in b} x \wedge \bigwedge_{x\not\in b} \neg x$, we have that $z \ge z\wedge y \ne 0$, and $z$ is below $x$ or below $\neg x$ for every $x$, thus $z$ generates a principal ultrafilter. Moreover, we must have $y\in b$, so $z$ is an atom below $y$.

\rem{
\subsubsection{$\cPo$ and $\Qop$}
\label{sec:Q-and-Qop}

The \emph{contravariant powerset functor} $\cPo :\Set\to\Setop$ maps objects $X$ to their powerset $2^X$ and morphisms $f:X\to Y$ to
\begin{align}
& \cPo f = f^{-1}:2^Y\to 2^X & \cPo f(b) = f^{-1}(b) &= \set{x\in X}{f(x)\in b}.\label{eq:Qdef}
\end{align}
The functor $\cPo $ is dually self-adjoint with $\cPo \dashv\Qop$.
The natural bijection between $\Set(X,2^Y)$ and $\Setop(2^X,Y)$ in both directions is given by the \emph{exponential transpose} $f\mapsto \transp f = \lam{yx}{fxy}$, an involution that simply switches the order of the arguments.
\begin{align}
\begin{array}c
\begin{tikzpicture}[->, >=stealth', node distance=28mm, auto]
\small
\node (NW) {$2^X$};
\node (NE) [right of=NW] {$Y$};
\node (SW) [below of=NW, node distance=12mm] {$X$};
\node (SE) [below of=NE, node distance=12mm] {$2^Y$};
\path (NW) edge[<-] node {$\transp f=\lam{yx}{fxy}$} (NE);
\path (NE) edge node {$\Qop$} (SE);
\path (SW) edge node {$\cPo $} (NW)
edge node[swap] {$f = \trtr f$} (SE);
\node (NL) [left of=NW, node distance=8mm, anchor=east] {$\Setop$:};
\node (SL) [left of=SW, node distance=8mm, anchor=east] {$\Set$:};
\end{tikzpicture}
\end{array}
\label{eq:adjoint}
\end{align}
In terms of sets, $\transp f = \lambda y.\set{x\in X}{y\in f(x)}$.
The unit $\eta_X : X \to \TTwo X$ and counit $\eps_X = \eta_X^\op$ are opposites but represent the same set function $\eta_X(x)=\set{a}{x\in a}$.

%Note that we are using $\eta$ and $\eps$ here locally to denote the unit and counit of $\cPo \dashv\Qop$. This should not be confused with $\eta$ and $\eps$ as used in Section~\ref{sec:base}. HH: Actually, I realised they are the same!

\subsubsection{\EMN}

The self-dual adjunction $\cPo^\op\dashv\cPo$ of the contravariant powerset functor (Example~\ref{exm:self-dual-powerset}) gives rise to a $\Set$-monad $N = \cPo \o \cPo^\op$, where for $X$ a set and $f:X\to Y$ a set function,
\begin{align*}
N X &= \cPo \cPo^\op X = 2^{2^X} & Nf &= (f^{-1})^{-1}:\TTwo X\to\TTwo Y
\end{align*}
The unit and multiplication are
\begin{align*}
\eta_X(x) = \set a{x\in a},\quad\quad
\mu_X(H) = \set a{\eta_{\cPo{X}}(a)\in H} = \eta_{\cPo X}^{-1}(H).
%\mu_X(H) &= \\cPo op\eps_{\cPo X}(H) = \set a{\eps_{\cPo X}^\op(a)\in H} = \set a{\eta_{\cPo X}(a)\in H} = \eta_{\cPo X}^{-1}(H).
\end{align*}
This is called the \emph{double powerset} or \emph{neighborhood monad}. The category of Eilenberg-Moore algebras of $N$ is denoted \EMN.

\subsubsection{Equivalence of \CABA, \Setop, and \EMN}
\label{sec:Setop=to-EM}

It is known that the Eilenberg-Moore algebras of the double powerset monad $N$ are exactly the {\CABA}s. These two categories are also dually equivalent to \Set, that is, equivalent to \Setop, as observed in [72].

The equivalence of the three categories can be shown via the composition of three faithful functors that are injective on objects:
\begin{align}
\begin{array}c %to get label in the right place
\begin{tikzpicture}[->, >=stealth', node distance=20mm, auto]
\small
\node (A) {\Setop};
\node (B) [right of=A] {\EMN};
\node (C) [right of=B] {\CABA};
\node (D) [right of=C] {\Setop.};
\path (A) edge node {$J$} (B);
\path (B) edge node {$\EMNtoCABA$} (C);
\path (C) edge node {$\At$} (D);
\end{tikzpicture}
\end{array}
\label{eq:threefunctors}
\end{align}
%\hhh{Say what $J$ does concretely, since it is needed to check the conditions for Thm.~\ref{thm:min-algo}.}
Here $J$ is the Eilenberg-Moore comparison functor [3, 52]. Concretely, $J$ sends a set $X$ to the \CABA $2^X$ and a function $f: X \to Y$ to its inverse image map. That is, $J = \Set(-,2)$ with Boolean structure.
The functor $\At$ takes a \CABA to its set of atoms and a \CABA morphism $f:A\to B$ to $\At f:\At B\to\At A$, where $\At\!f\,(b)$ is the unique atom $a$ of $A$ such that $\up a = f^{-1}(\up b)$ and $\up a$ and $\up b$ are the principal ultrafilters on atoms $a$ and $b$, respectively.
In a \CABA, there is a bijection between principal ultrafilters and atoms, and we have that $\At \cong \CABA(-,2)$. In other words, the equivalence given by $J$ and $\At$ is a concrete duality with dualising object $2$.

Although the equivalence between \EMN and \CABA is fairly well known, the details are rarely provided. We therefore describe the functor $\EMNtoCABA$ that produces a \CABA from an \EMN-algebra $(X,\alpha)$. Let $TX$ be the term monad for \CABA terms over indeterminates $X$.\footnote{$TX$ consists of \CBA terms with the arity of the infinitary operations bounded by $2^{2^{\len X}}$. There can be no such bound for \CBA in general, as there are {\CBA}s of arbitrarily large cardinality generated by $X$; thus there is no term monad for \CBA. However, {\CABA}s generated by $X$ are of cardinality at most double exponential in $\len X$, and we can bound arities accordingly.} Let $\EMNtoCABA(X,\alpha) = (X,\EMNtoCABA\alpha)$, where
\begin{align}
& \EMNtoCABA\alpha:TX\to X & \EMNtoCABA\alpha &= \alpha\circ(\tau N\circ T\eta)_X,\label{def:alphap}
\end{align}
where $T\eta_X:TX\to TNX$ substitutes $\eta_X(x)$ for $x\in X$ in a term and $\tau_{NX}:TNX\to NX$ is the evaluation map of the powerset \CABA $(\TTwo X,\bigcup,\bigcap,\setcompl,\emptyset,2^X)$.
In particular (and in more conventional notation), this gives the following definitions of the Boolean operations:
\begin{gather}
\begin{array}c
\bigvee_n x_n = \alpha(\bigcup_n \eta_X(x_n)) \qquad\quad
\bigwedge_n x_n = \alpha(\bigcap_n \eta_X(x_n))\\[8pt]
\neg x = \alpha(\setcompl{\eta_X(x)}) \qquad\quad 0 = \alpha(\emptyset) \qquad\quad 1 = \alpha(2^X).
\end{array}
\label{eq:BAdefs}
\end{gather}
The action of $\EMNtoCABA$ on morphisms is the identity.

The natural transformation $\tau N\circ T\eta:T\to N$ in \eqref{def:alphap} relating \CABA terms and double powerset is invertible up to \CABA equivalence. Consider the natural transformation
\begin{align*}
& \upsilon : N\to T & \upsilon_X(A) &= \bigvee_{a\in A} (\bigwedge_{x\in a} x \wedge \bigwedge_{x\not\in a} \neg x),\ \ A\in \TTwo X.
\end{align*}
It can be shown that
\begin{align*}
\tau N\circ T\eta\circ\upsilon &= \id_{N} & \upsilon\circ\tau N\circ T\eta &\equiv \id_{T}.
\end{align*}
By the latter we mean that for any term $t\in TX$,
$\upsilon_X(\tau_{NX}(T\eta_X(t))) \equiv t$ modulo the axioms of \CABA.
This essentially says that there is a disjunctive normal form for \CABA terms.

%\subsubsection{Equivalence of \CABA, \Setop, and \EMN}

%\subsection{Characterization of Principal Ultrafilters}
%If $x\in a$ then $\alpha(\{a\})\le x$.
%%If $A\subs B$ then $\alpha(A)\le\alpha(B)$.
%It follows from Lemma \ref{lem:BA} that $A\subs B \Imp \alpha(A)\le\alpha(B)$. Then
%x\in a &\Imp a\in\eta_X(x) \Imp \{a\}\subs\eta_X(x) \Imp \alpha(\{a\})\le\alpha(\eta_X(x))=x.
%The following are equivalent:
%$\alpha(A)\in a$ iff $a\in A$; \dck{That is, $a$ is relevant in the sense of Helle and Clemens}
%$\alpha(\{a\})\neq 0$;
%{\upshape(}$x\in a$ iff $\alpha(\{a\})\le x${\upshape)} and $0\not\in a$;
%$a$ is a principal ultrafilter of $X$.
%(i) $\Imp$ (ii):
%\dck{This argument is given in Helle's writeup.}
%Since $a\in\{a\}$, we have $\alpha(\{a\})\in a$, but since $a\not\in\emptyset$, we have $\alpha(\emptyset)\not\in a$. Thus $\alpha(\{a\})\neq\alpha(\emptyset)=0$.
%(ii) $\Imp$ (iii):
%The forward implication of the biconditional holds without the assumption (i) by Lemma \ref{lem:relevant}. For the other direction, if $\alpha(\{a\})\neq 0$ and $\alpha(\{a\})\le x$, then
%\alpha(\{a\}\cap\eta_X(x)) &= \alpha(\{a\})\wedge\alpha(\eta_X(x)) = \alpha(\{a\}) \neq 0,
%so $\{a\}\cap\eta_X(x)\neq\emptyset$, so $a\in\eta_X(x)$, so $x\in a$. Also, $0\not\in a$ by Lemma \ref{lem:relevant}.
%(iii) $\Imp$ (iv):
%We know that $\alpha(\{a\})$ is either an atom or 0. Assuming (iii), the latter implies $0\in a$, a contradicting (iii). In the former case, $a = \set x{x\in a} = \set x{\alpha(\{a\})\le x}$ is the principal ultrafilter generated by the atom $\alpha(\{a\})$.
%(iv) $\Imp$ (i):
%Suppose $a$ is a principal ultrafilter generated by an atom $\alpha(\{b\})\neq 0$ (as argued in the proof of Theorem \ref{thm:CABA}, all atoms are of this form). Then $y\in a$ iff $\alpha(\{b\})\le y$. Also by Lemma \ref{lem:relevant}, if $y\in b$ then $\alpha(\{b\})\le y$. It follows that $b\subs a$. Since $b$ and $a$ are both maximal consistent sets, we must have $b=a$, therefore $\alpha(\{a\})\neq 0$.
%Now for all $A$,
%\reasoning{\alpha(\{a\}\cap A) = \alpha(\{a\})\neq 0}
%\alpha(A)\in a &\Imp \reason{\alpha(\{a\})\le\alpha(A)}{by Lemma \ref{lem:relevant}}\nonumber\\
%&\Imp \alpha(\{a\}\cap A) = \alpha(\{a\})\neq 0\nonumber\\
%&\Imp \{a\}\cap A\neq\emptyset\nonumber\\
%&\Imp a\in A.\label{eq:ch}
%For the converse, since $a$ is an ultrafilter,
%\alpha(A)\not\in a &\Imp \neg\alpha(A)\in a \Imp \alpha(\setcompl A)\in a \Imp a\in\setcompl A,
%the last step by \eqref{eq:ch}.
%\dck{\emph{Relevant} is not the same as \emph{consistent}. There are three possibilities for $a$. Let us call $a$
%\emph{relevant} if $a$ is a principal ultrafilter, that is, $a$ satisfies the conditions of Theorem \ref{thm:relevant};
%\emph{consistent} if $a$ is an ultrafilter (not necessarily principal); and
%\emph{garbage} if neither.
%Garbage and nonprincipal ultrafilters go to 0 under $\alpha$, and the principal ultrafilters correspond to atoms. Thus $X$ is isomorphic to the full powerset algebra on its atoms.}
%\subsection{From $\CABA$ to $\EMN$}
%In \S\ref{sec:EM-to-CABA}, we showed how to go from \EMN to \CABA. In this section we go in the opposite direction.
%Suppose we are given an arbitrary \CABA. By the representation theorem, we can assume without loss of generality that it is a powerset Boolean algebra $(2^X,\bigcup,\bigcap,\setcompl,\emptyset,X)$ on some set $X$.
%For $x\in X$, let $\up{x} = \set{a\in 2^X}{x\in a}$, the principal ultrafilter on $x$.
%Let $A=2^X$. Define $\alpha:\TTwo{A}\to A$ by
%\alpha(U) &= \set{x\in X}{\up x\in U},\ U\in\TTwo A.
%$(A,\alpha)$ is an \EMN.
%We need to verify the Eilenberg-Moore laws \eqref{eq:alpha}. For the $\eta$-law, for $a\in A$,
%&= \set{x}{\up{x}\in\eta_A(a)}
%= \set{x}{a\in\up{x}}
%= \set{x}{x\in a}
%= a.
%For the $\mu$-law, for $\FF\in N^2{A}$,
%\alpha( N\alpha(\FF))
%&= \set x{\up{x}\in N\alpha(\FF)}
%= \set x{\alpha^{-1}(\up{x})\in\FF}\\
%&= \set x{\set U{\alpha(U)\in\up{x}} \in \FF}
%= \set x{\set U{x\in\alpha(U)} \in \FF}\\
%&= \set x{\set U{\up{x}\in U} \in \FF}
%= \set x{\eta_{\cPo A}(\up{x})\in \FF}\\
%&= \set x{\up{x} \in \mu_A(\FF)}
%= \alpha(\mu_A(\FF)).
%It remains to argue that this construction is respects morphisms of the two categories.
%Every \CABA morphism $f:A\to B$ is an \EMN morphism.
%Again, without loss of generality we may assume that $A$ and $B$ are powerset {\BA}s $A=2^X$ and $B=2^Y$. Because $f$ is a \CBA homomorphism on powerset {\CBA}s, $f^{-1}$ maps principal ultrafilters of $B$ to principal ultrafilters of $A$. Let $F(y)\in X$ be the generator of the principal ultrafilter $f^{-1}(\up y)$; that is, $\up{F(y)}=f^{-1}(\up y)$. Then $F^{-1} = f$, since for all $y\in Y$ and $a\in A$,
%y\in F^{-1}(a)
%&\Iff F(y) \in a
%\Iff a\in \up{F(y)}\\
%&\Iff a\in f^{-1}(\up y)
%\Iff f(a)\in \up y
%\Iff y\in f(a).
%The desired condition on $f$ now follows. If $(A,\alpha)$ and $(B,\beta)$ are the \EMN-algebras constructed from $A$ and $B$, then for any $U\in\TTwo A$,
%&= F^{-1}(\alpha(U))
%= \set y{F(y)\in\alpha(U)}\\
%&= \set y{\up{F(y)}\in U}
%= \set y{f^{-1}(\up y)\in U}\\
%&= \set y{\up y\in (f^{-1})^{-1}(U)}
%= \set y{\up y\in Nf(U)}
%= \beta(Nf(U)).
%We have shown
%The construction given above constitutes a functor $\CABA\to\EMN$.
%An alternative approach leading to the same result would have been to show that the set $\TTwo X$ with the set-theoretic \CBA operations is the free \CABA on generators $X$, and that the monad arising from the free construction is $(N,\mu,\eta)$. The functor of Theorem \ref{thm:CABA-to-EM} is then the comparison functor to \EMN \cite{}. However, the present approach gives a concrete construction and avoids some foundational issues associated with the fact that there is no term monad for the signature of \CBA, as the class of terms is not a set.
%\section{Some Equivalences and Adjunctions}
%The relevant categories and functors and their relationships are given in the following diagram:
%\CABA \ar@/^1pc/[r]^-{\At} \ar@{}[r]|{\cong}
%& \Setop \ar@/^1pc/[r]^-{J} \ar@/^1pc/[l]^-{\Qop} \ar@/^1pc/[d]^-{\Qop}  \ar@{}[r]|{\cong}
%& \EMN \ar@/^1pc/[l]^-{R}
%& \Set \ar@/^1pc/[u]^-{\cPo } \ar@{}[u]|{\dashv} \ar@(dl,dr)_{ N=\Qop\circ \cPo }
%We explain each of the three parts of this picture separately.
%The concrete definition of $\alpha$ in \eqref{eq:alpha-concrete} indeed agrees with the definition obtained via $J \circ \At$.
%For $A$ a \CABA with atoms $X$ and $U \in \TTwo{2^X}$:
%\eta_X^{-1}(U) &= \set{x\in X}{\eta_X(x)\in U} = \set{x\in X}{\up{x}\in U} = \alpha(U).
%Since $J$ is known to be a functor, we do not need to check the $\eta$-law and $\mu$-law explicitly.
%It follows from Par\'e's theorem (see \cite[Part IV.5, Theorem 3, p.~181]{MM:Sheaves}) that the comparison functor $J : \Setop \to \EMN$ yields an equivalence, but we would like an explicit description of the inverse functor $R:\EMN\to\Setop$. It should be the case that for all sets $X$, $X\cong R(J(X))$, and for all \EMN-algebras $(A,\alpha)$, $J(R(A,\alpha)) \cong (A,\alpha)$. The functor $R$ should thus map an arbitrary \EMN-algebra $(A,\alpha)$ to the set of atoms of its corresponding \CABA.
%Let $(A,\alpha)$ be in $\EMN$. Define the set $R(A,\alpha) \subs A$ by
%R(A,\alpha) &= \set{\alpha(\{U\})}{U\subs A} \setminus \{\alpha(\emptyset)\}.
%Since $R = \At\circ \EMNtoCABA$ where $\EMNtoCABA(A,\alpha)$ is the \CABA associated with $(A,\alpha)$, and $\At: \CABA \to \Setop$ takes atoms,\hhh{(Dexter, please add reference to your description of $\EMNtoCABA$ and $\At$)}
%we have that for any $\EMN$-morphism $f: (A,\alpha) \to (B,\beta)$ and $y \in R(B,\beta) = \At(\EMNtoCABA(B,\beta))$,
%\bar{R}f(y) &= \bigwedge \set{a\in A}{y\le f(a)}
%= \alpha(\bigcap\set{\eta_A(a)}{y\le f(a)})
%For every set $X$, we have that $X\cong R(J(X))$.
%Recall that $J(X) = (2^X,\eta_X^{-1})$.
%In particular, $\eta_X^{-1}(\emptyset) = \emptyset$.
%By definition, for all $U \subs 2^X$,
%\eta_X^{-1}(\{U\}) = \{ x \in X \mid \eta_X(x) \in \{U\} \}
%\{x\} & \text{ if } U = \eta_X(x)\\[.3em]
%\emptyset & \text{ otherwise}
%since $\eta_X$ is injective.
%Hence $R(2^X,\eta_X^{-1}) = \set{\{x\}}{x \in X} \cong X$.
%The other isomorphism is a bit more work to show.
%For every $(A,\alpha)$ in $\EMN$, we have that $(A,\alpha) \cong J(R(A,\alpha))$.
%Let $X = R(A,\alpha) \subs A$ such that $J(R(A,\alpha)) = (2^X,\eta_X^{-1})$.
%We wish to define an $\EMN$-isomorphism $f$:
%NA \ar[r]^-{N f} \ar[d]_-{\alpha}
%&  N2^X \ar[d]^-{\eta_X^{-1}}
%A \ar[r]^-{f} & 2^X
%We define
%\begin{align*} f(a) = \{ x \in X \mid x \le a\}
%where $\le$ is defined on $A$ by
%a \le b \quad\Iff\quad \alpha(\eta_A(a) \cup \eta_A(b)) = \alpha(\eta_A(b)).
%We then have to show:
%\item $\le$ is a partial order.
%\item $f$ is bijective.
%\item $f$ is an algebra homomorphism.
%Items 1 and 2 follow from resuls in Dexter's notes.
%This is essentially the same as showing that $(A,\alpha)$ can be turned into
%a CABA with set of atoms $X$.
%It remains to prove 3, i.e., that $f$ is an algebra homomorphism,
%i.e., that for all $N \in  N(A)$ and all atoms $x \in X$:
%\begin{align*} x \in f(\alpha(N)) \Iff x \in \eta_X^{-1}( N{f}(N)).
%We have,
%x \in  f(\alpha(N)) & \Iff
%  & x \le \alpha(N) = \alpha(\bigcup_{U \in N} \{ U \}) = \bigvee_{U \in N}\alpha(\{U\}) & \text{(Dexter's lemma 0.2)}
% & \Iff & \exists U \in N : x = \alpha(\{U\})
% & \text{($x$ is atom)}
% & \stackrel{(*)}{\Iff} & \{ a \in A \mid x \le a\} \in N
% & \Iff & \{ a\in A \mid \{x \in X \mid x \le a\} \in \eta_X(x)\}\in N
% & \Iff & f^{-1}(\eta_X(x)) \in N
% & \Iff & \eta_X(x) \in N f (N)
% & \Iff & x \in  \eta_X^{-1}( N{f}(N))
%To see that $(*)$ holds, for $\Rightarrow$:
%$\alpha(\{U\}) = x$ implies that $\alpha(\{U\}) \neq 0$, and hence
%by Dexter's Theorem 0.4 that $U$ is relevant, and
%hence $x \in U$. Since $U$ is also principal ultrafilter, it must be
%generated by the atom $x$, i.e., $U = \{a \in A \mid x \le a\}$.
%For $\Leftarrow$, take $U = \{ a \in A \mid x \le a\}$, so $U$ is a principal
%ultrafilter, and hence by Dexter's Theorem 0.4
%$\alpha(\{U\}) \neq 0$ and $\alpha(\{U\}) \in U$, so $x \le \alpha(\{U\})$.
%Since $x$ and $\alpha(\{U\})$ are both atoms, they must be equal.
%\subsection{Relevant sets}
%Def. Let $(A,\alpha)$ be in $\EMN$. A subset $U \subs A$ is \emph{relevant} if
%\begin{align*} \forall N \in \TTwo{A}\ \ \alpha(N) \in U \Iff U \in N.
%Let $\RS = \set{U\subs A}{\text{$U$ is relevant}}$.
%Some facts about relevant sets: