Two modes of recognition: algebra, coalgebra, and languages

TL;DR

This paper connects algebraic and coalgebraic approaches in categorical language theory, defining regular maps that generalize classical automata languages and establishing a Kleene-like theorem for their characterization.

Contribution

It introduces a unified framework linking algebraic and coalgebraic language theories for monads, generalizing regular languages and automata behaviors.

Findings

Regular maps form a subcategory of the Kleisli category.

A Kleene-like theorem characterizes regular morphisms.

Framework applies to various automata types like non-deterministic, tree, fuzzy, and weighted automata.

Abstract

The aim of the paper is to build a connection between two approaches towards categorical language theory: the coalgebraic and algebraic language theory for monads. For a pair of monads modelling the branching and the linear type we defined regular maps that generalize regular languages known in classical non-deterministic automata theory. These maps are behaviours of certain automata (i.e. they possess a coalgebraic nature), yet they arise from Eilenberg-Moore algebras and their homomorphisms (by exploiting duality between the category of Eilenberg-Moore algebras and saturated coalgebras). Given some additional assumptions, we show that regular maps form a certain subcategory of the Kleisli category for the monad which is the composition of the branching and linear type. Moreover, we state a Kleene-like theorem characterising the regular morphisms category in terms of the smallest subcategory closed under certain operations. Additionally, whenever the branching type monad is taken to be the powerset monad, we show that regular maps are described as maps recognized by certain functors whose codomains are categories with all finite hom-sets. We instantiate our framework on classical non-deterministic automata, tree automata, fuzzy automata and weighted automata.

Tables

Table 1. Table 1 : Languages of ( α , ℱ ) 𝛼 ℱ (\alpha,\mathcal{F}) expressed in 𝒦 ​ l ​ ( 𝒫 ) 𝒦 𝑙 𝒫 \mathcal{K}\mspace{-1.0mu}l(\mathcal{P})

$L(\alpha ,ℱ,i)=$	where
$1\stackrel{i_n}{⟶\bullet \circ }n\stackrel{{\alpha }^{\ast }}{⟶\bullet \circ }\overline{{\Sigma }^{\ast }}n\stackrel{\overline{{\Sigma }^{\ast }}{\chi }_{ℱ}}{⟶\bullet \circ }\overline{{\Sigma }^{\ast }}1$
	$i_n:1⟶\bullet \circ n=1\to 𝒫n;1\mapsto \left\{i\right\}$.

Equations

$$\displaystyle f_{-}\colon Y\makebox[1.1pt][l]{$\longrightarrow\makebox{$\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu$}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}$}X=Y\to\mathcal{P}X;y\mapsto\{x\in X\mid y\in f(x)\}.$$

$$\mathcal{E}\mathcal{M}(S{)}^{op}\cong \mathcal{S}\mathcal{A}\mathcal{T}(S)$$

$$L(\mathcal{A},i)=1\stackrel{{\scriptstyle i_{n}}}{{\makebox[1.1pt][l]{$\longrightarrow\makebox{$\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu$}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}$}}}n\stackrel{{\scriptstyle\alpha}}{{\makebox[1.1pt][l]{$\longrightarrow\makebox{$\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu$}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}$}}}\overline{S}n\stackrel{{\scriptstyle\overline{S}\chi}}{{\makebox[1.1pt][l]{$\longrightarrow\makebox{$\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu$}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}$}}}\overline{S}1$$

$$1\stackrel{{\scriptstyle i_{n}}}{{\makebox[1.1pt][l]{$\longrightarrow\makebox{$\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu$}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}$}}}n\stackrel{{\scriptstyle\alpha}}{{\makebox[1.1pt][l]{$\longrightarrow\makebox{$\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu$}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}$}}}\overline{S}n\stackrel{{\scriptstyle\overline{S}\chi}}{{\makebox[1.1pt][l]{$\longrightarrow\makebox{$\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu$}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}$}}}\overline{S}p.$$

$$\vspace{-.4ex}L(\mathcal{A},i)=1\makebox[1.1pt][l]{$\longrightarrow\makebox{$\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu$}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}$}n\stackrel{{\scriptstyle a}}{{\makebox[1.1pt][l]{$\longrightarrow\makebox{$\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu$}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}$}}}\overline{\Sigma^{\ast}}n\stackrel{{\scriptstyle\overline{\Sigma^{\ast}}\chi}}{{\makebox[1.1pt][l]{$\longrightarrow\makebox{$\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu$}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}$}}}\overline{\Sigma^{\ast}}1$$

$$T^2$$

$$FX\stackrel{F\mathsf{inr}}{\to }F(F{F}^{\ast }X+X)\stackrel{F{i}_X}{\to }F{F}^{\ast }X\stackrel{\mathsf{inl}}{\to }F{F}^{\ast }X+X\stackrel{i_X}{\to }{F}^{\ast }X.$$

$$X$$

$$|a|=STX\stackrel{\lambda }{\to }TSX\stackrel{Ta}{\to }TTX\stackrel{\mu }{\to }TX$$

$$h_{-}=S\left((e_X{)}_{-})\circ S(h_{-}\right)\circ b_{-}=S\left((e_X{)}_{-})\circ h_{-}\right)\circ b_{-}=S\left((h\circ e_X{)}_{-}\right)\circ b_{-}.$$

$$(\nu \circ a_{-}{)}^{\ast }\le (a_{-}{)}^{\ast }=a_{-}.$$

$$m=n_{1}+\ldots+n_{p}\stackrel{{\scriptstyle\alpha_{1}+\ldots+\alpha_{p}}}{{\makebox[1.1pt][l]{$\longrightarrow\makebox{$\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu$}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}$}}}\overline{S}n_{1}+\ldots+\overline{S}n_{p}\stackrel{{\scriptstyle[\overline{S}\mathsf{in}^{n_{i}}_{m}]_{i}}}{{\makebox[1.1pt][l]{$\longrightarrow\makebox{$\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu$}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}$}}}\overline{S}(n_{1}+\ldots+n_{p})=\overline{S}m$$

$$n\stackrel{{\scriptstyle r_{1}}}{{\makebox[1.1pt][l]{$\longrightarrow\makebox{$\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu$}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}$}}}\overline{S}k\stackrel{{\scriptstyle\overline{S}r_{2}}}{{\makebox[1.1pt][l]{$\longrightarrow\makebox{$\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu$}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}$}}}\overline{S}^{2}q\stackrel{{\scriptstyle\overline{m}}}{{\makebox[1.1pt][l]{$\longrightarrow\makebox{$\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu$}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}$}}}\overline{S}q$$

$${\alpha:n\makebox[1.1pt][l]{$\longrightarrow\makebox{$\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu$}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}$}\overline{S}n\quad\in\mathcal{SAT}(\overline{S})}$$

$$|\mathsf{Alg}(\alpha )|:S\mathcal{P}n\to \mathcal{P}n\in \mathcal{E}\mathcal{M}(S)$$

$$(h_2\diamond h_1{)}_A\stackrel{†}{=}(h_1{)}_A\circ (h_2{)}_A\in {\mathbb{T}}_{F_A}(k,m).$$

$$(h_2\diamond h_1{)}_A=(h_1{)}_A\circ (h_2{)}_A.$$

$$(h_2\diamond h_1{)}_A(x)=k\stackrel{h_1}{\to }Sl\stackrel{S{h}_2}{\to }{S}^{2}m\stackrel{m}{\to }Sm\stackrel{Sx}{\to }S\mathcal{P}n\stackrel{|\mathsf{Alg}(\alpha )|}{\to }\mathcal{P}n.$$

$$f:k\to Sl\in {\mathbb{T}}_S(k,l)\text{ to }h(f)=f_A\in {\mathbb{T}}_{F_A}(k,l).$$

$$T_{\chi }\subseteq {\mathbb{T}}_{F_A}(1,p)=\{g_A:(p\to \mathcal{P}n)\to (1\to \mathcal{P}n)\mid g:1\to Sp\in {\mathbb{T}}_S(1,p)\}$$

$$|\mathsf{Alg}(\alpha )|\circ S{\chi }_{-}\circ f=i_n\in \text{Set}$$

$$\overline{h}:M_{{\mathbb{T}}_S}⟹M_{{\mathbb{T}}^{\prime }}.$$

$$a:M_{{\mathbb{T}}_S}{M}_{{\mathbb{T}}^{\prime }}(p)\stackrel{{\overline{h}}_{M_{{\mathbb{T}}^{\prime }}p}}{\to }{M}_{{\mathbb{T}}^{\prime }}{M}_{{\mathbb{T}}^{\prime }}(p)\stackrel{m_p^{\prime }}{\to }{M}_{{\mathbb{T}}^{\prime }}p={\mathbb{T}}^{\prime }(1,p).$$

$$a^{♯}\bullet \overline{M_{{\mathbb{T}}_S}}{h}^{♯}=h^{♯}\bullet m^{♯}.$$

$$h^{-1}(t)=h_{-}^{♯}(t)=h_{-}^{♯}\bullet t_{{\mathbb{T}}^{\prime }}^{♯}(1)=\overline{M_{{\mathbb{T}}_S}}(e_{-}^{♯}\bullet h_{-})\bullet \mathsf{CoAlg}(a^{♯})\bullet t_{{\mathbb{T}}^{\prime }}^{♯}(1),$$

$$\alpha :n\to \mathcal{P}(n\times \Sigma \times n);i\mapsto \{(j,a,k)\mid (j,k)\in \delta (a,i)\}.$$

$$t\in L(\alpha ,\mathcal{F},i)(1)⟺t\text{ is accepted by the state i}\text{ in the tree automaton }(\alpha ,\mathcal{F}).$$

$$({\mathcal{M}}_{\mathcal{S}}X,\psi )\mapsto \left(X,\sum (\varphi (x)\cdot \psi (\varphi ))\bullet x\right)x\mapsto (X,x\bullet 1)\text{.}$$

$$L(\mathcal{A},i)({\sigma }_1\dots {\sigma }_k)=\sum \left\{\chi (j_k)\cdot \prod _{p<k}\hat{\alpha }(j_p)({\sigma }_{p+1},j_{p+1})|j_0=i,j_1,\dots ,j_k\in n\right\}\text{.}$$

$$f_{-}(y)(x)\triangleq f(x)(y)\text{.}$$

Full text

Given some additional assumptions, we show that regular maps form a certain subcategory of the Kleisli category for the monad which is the composition of the branching and linear type. Moreover, we state a Kleene-like theorem characterising the regular morphisms category in terms of the smallest subcategory closed under certain operations. Additionally, whenever the branching type monad is taken to be the powerset monad, we show that regular maps are described as maps recognized by certain functors whose codomains are categories with all finite hom-sets.

We instantiate our framework on classical non-deterministic automata, tree automata, fuzzy automata and weighted automata.

1 Introduction

Automata theory is one of the core branches of theoretical computer science and formal language theory. One of the most fundamental state-based structures considered in the literature is a non-deterministic automaton and its relation with languages. Non-deterministic automata with a finite state-space are known to accept regular languages, characterized as subsets of words over a fixed finite alphabet that can be obtained from the languages consisting of words of length less than or equal to one via a finite number of applications of three types of operations: union, concatenation and the Kleene star operation [23]. This result is known under the name of Kleene theorem for regular languages. It readily generalizes to automata accepting other types of input with more general versions of this theorem stated in the category-theoretic setting in the context of coalgebras and Lawvere theories [18, 19, 17, 9, 34]. Coalgebraic language theory is based on a unifying theory of different types of automata and has been part of the focus of the coalgebraic community in recent years (\eg[35, 25, 26, 6]). Our paper puts the main emphasis on a part of this research which describes a general theory of systems with internal transitions [39, 7, 8, 6, 11, 10, 29]. Intuitively, these systems have a special computation branch that is silent. This special branch, usually denoted by the letter $\tau$ or $\varepsilon$, is allowed to take several steps and in some sense remain neutral to the structure of a process. These systems arise in a natural manner in many branches of theoretical computer science, among which are process calculi [30] (labelled transition systems with $\tau$-moves and their weak bisimulation) or automata theory (automata with $\varepsilon$-moves), to name only two. The approach from [8, 10] suggests that these systems should be defined as coalgebras whose type is a monad. This treatment allows for an elegant modelling of weak behavioural equivalences [10, 11, 12] among which we find Milner’s weak bisimulation [30]. Each coalgebra $\alpha\colon X\to TX$ becomes an endomorphism \alpha\colon X\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}X in the Kleisli category for the monad $T$ and Milner’s weak bisimulation on a labelled transition system $\alpha$ can be defined to be a strong bisimulation on its saturation $\alpha^{\ast}$ which is the smallest LTS over the same state space satisfying $\alpha\leq\alpha^{\ast}$, $\mathsf{id}\leq\alpha^{\ast}\text{ and }\alpha^{\ast}\cdot\alpha^{\ast}\leq\alpha^{\ast}$ (where the composition and the order are given in the Kleisli category for the LTS monad) [8]. Hence, intuitively, $\alpha^{\ast}$ is the reflexive and transitive closure of $\alpha$.

Saturation $\alpha\mapsto\alpha^{\ast}$ can also be used as one of the main components of the coalgebraic language theory. Indeed, the language accepted by an automaton whose transition map is modelled by $\alpha$ can be defined in terms of a simple expression involving its saturation $\alpha^{\ast}\colon X\to TX$ calculated in the Kleisli category for the monad $T$ (see [3, 19, 9]). Regular languages, \ielanguages accepted by automata with finite carriers for carefully chosen transition $\alpha$ form a subclass of the class of all languages accepted by automata of type $T$.

Languages have also been studied from the algebraic perspective (\eg[42, 33, 16, 21, 43, 34]) with a general approach presented on the categorical level in the context of Eilenberg-Moore algebras for a monad in [4]. For set-based algebras, a language (\iea subset of the carrier of a given algebra) is said to be recognizable if it is a preimage of a subset of a finite algebra under an algebra homomorphism. Using this approach one may \egcharacterize regular languages for non-deterministic automata as recognizable languages for the monoid of words $(\Sigma^{\ast},\cdot,\varepsilon)$. An algebraic characterization of classical regular languages is one of several examples of a similar phenomenon, where regular and recognizable languages meet (see \loccit).

Contributions

We show existence of a general coincidence between an algebraic and coalgebraic approach towards defining languages stated on a categorical level by building on the duality between Eilenberg-Moore algebras and saturated coalgebras. In this setting, we define regular languages as a class of morphisms (herein, regular morphisms) arising from automata whose coalgebra structure is saturated and is dual to an Eilenberg-Moore algebra. As we put our emphasis on automata with finite carriers, it is natural to consider Lawvere theories since a Lawvere theory for a monad is, roughly speaking, the part of its Kleisli category which is suitable to model morphisms with finite domains and codomains only [27, 24]. Lawvere theories become our natural habitat where we provide Kleene-like theorem at the level of regular morphisms. Additionally, in the case of generalized non-deterministic automata we show that regular languages (with variables) which are modelled by arrows in one Lawvere theory are essentially subsets of arrows of another Lawvere theory recognized by Lawvere theory morphisms whose targets are finitary theories. Hence, we obtain a general algebraic characterisation of such languages.

2 Basic notions

We assume the reader is familiar with basic category theory concepts like a functor, a monad $(T,\mu,\eta)$, an adjunction, a Lawvere theory, a Kleisli category $\mathcal{K}\mspace{-1.0mu}l(T)$ and an Eilenberg-Moore category $\mathcal{EM}(T)$ for a monad $T$, a distributive law $\lambda\colon ST\implies TS$ of a monad $(S,m,e)$ over a monad $(T,\mu,\eta)$, a lifting of a monad $(S,m,e)$ to a monad $(\overline{S},\overline{m},\overline{e})$ on $\mathcal{K}\mspace{-1.0mu}l(T)$ and the fact that if $(S,m,e)$ lifts to $(\overline{S},\overline{m},\overline{e})$ on $\mathcal{K}\mspace{-1.0mu}l(T)$ then it yields a monadic structure on $TS$ whose Kleisli category satisfies $\mathcal{K}\mspace{-1.0mu}l(TS)=\mathcal{K}\mspace{-1.0mu}l(\overline{S})$ (see \eg[28, 2, 32] for details).

The most important example of a monad used throughout the paper is the powerset monad $(\mathcal{P}\colon\textnormal{{Set}}\to\textnormal{{Set}},\bigcup,\{-\})$. Moreover, we also consider the following running example.

Example 2.1**.**

Let $M=(M,\cdot,1)$ be any monoid. The functor $M\times\mathcal{I}d\colon\textnormal{{Set}}\to\textnormal{{Set}}$ carries a monadic $(M\times\mathcal{I}d,m,e)$ with $m_{X}\colon M\times M\times X\to M\times X;(m,n,x)\mapsto(m\cdot n,x)$ and $e_{X}\colon X\to M\times X;x\mapsto(1,x)$. The most often used example in our paper is the monad $\Sigma^{\ast}\times\mathcal{I}d$, where $\Sigma^{\ast}$ is the free monoid over a set $\Sigma$. Eilenberg-Moore algebras for the monad $M\times\mathcal{I}d\colon\textnormal{{Set}}\to\textnormal{{Set}}$ consist of algebras $a\colon M\times X\to X$ satisfying $a(1,x)=x$ and $a(m\cdot n,x)=a(m,a(n,x))$ for any $x\in X$. The monad $M\times\mathcal{I}d$ lifts to a monad $\overline{M}\colon\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})\to\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$ via the distributive law $\theta\colon M\times\mathcal{P}\to\mathcal{P}(M\times\mathcal{I}d)$ given $\theta_{X}\colon M\times\mathcal{P}X\to\mathcal{P}(M\times X);(m,Y)\mapsto\{(m,y)\mid x\in Y\}$ [8, 12]. The monad $\overline{M}$ maps any object $X$ in $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$ onto $\overline{M}X=M\times X$ and any map $f\colon X\to\mathcal{P}Y$ between $X$ and $Y$ in $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$ onto $\overline{M}f=M\times X\stackrel{{\scriptstyle M\times f}}{{\to}}M\times\mathcal{P}Y\stackrel{{\scriptstyle\theta_{Y}}}{{\to}}\mathcal{P}(M\times Y)$. Its multiplication and unit are $\overline{m}=\{-\}\circ m$ and $\overline{e}=\{-\}\circ e$ respectively. The Kleisli category $\mathcal{K}\mspace{-1.0mu}l(\overline{M})$ has sets as objects and maps $X\to\mathcal{P}(M\times Y)$ as morphisms from $X$ to $Y$. The composition in the Kleisli category $\mathcal{K}\mspace{-1.0mu}l(\overline{M})$ is given for any $f\colon X\to\mathcal{P}(M\times Y)$ and $g\colon Y\to\mathcal{P}(M\times Z)$ as $(g\cdot f)(x)=\{(m_{1}\cdot m_{2},z)\mid(m_{2},z)\in g(y)\text{ and }(m_{1},y)\in g(x)\}$. Identity morphisms are the maps $x\mapsto\{(1,x)\}$. The lifting $\overline{M}$ of the monad $M\times\mathcal{I}d$ yields a monadic structure on the functor $\mathcal{P}(M\times\mathcal{I}d)$. For $M=\Sigma^{\ast}$, this monad $\mathcal{P}(\Sigma^{\ast}\times\mathcal{I}d)$ is called LTS monad [8]. Eilenberg-Moore algebras for the lifting $\overline{M}\colon\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})\to\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$ of $M\times\mathcal{I}d$ to $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$ are algebras whose underlying morphism is a\colon\overline{M}X\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}X=M\times X\to\mathcal{P}X,111In order to distinguish morphisms from the Kleisli category $\mathcal{K}\mspace{-1.0mu}l(T)$ and the base category $\mathsf{C}$ we often denote the former by \longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{\mkern-21.0mu\circ\mkern 10.0mu} and the latter by $\to$. Hence, X\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}Y=X\to TY for any two objects. where $a(1,x)=\{x\}$ and $a(m\cdot n,x)=\bigcup\{a(n,y)\mid y\in a(m,x)\}$.

Lawvere theories

The primary interest of the theory of automata and formal languages focuses on automata over a finite state space. Hence, since, as stated in the introduction, we are interested in systems with internal moves (\iecoalgebras $X\to TX$ for a monad $T$), without any loss of generality we may focus our attention on coalgebras of the form $n\to Tn$, where $n\triangleq\{1,\ldots,n\}$ with $n=0,1,\ldots$ for a Set-monad $T$. These morphisms are endomorphisms in a full subcategory of the Kleisli category for $T$ whose objects are $n$ for $n=0,1\ldots$ which is known under the name of (Lawvere) theory and is denoted by $\mathbb{T}_{T}$. That is why we will often restrict the setting of this paper to Lawvere theories. Because we are interested in the coalgebraic essence of a Lawvere theory, we adopt the definition which is dual to the classical notion [27].

Coalgebras and saturation

Saturated coalgebras were introduced in [7, 8] in the context of coalgebraic weak bisimulation. As noticed in loc. cit. the concept of a saturated map can be given in any order enriched category222A category is order enriched if each hom-set is a poset with the order being preserved by the composition. $\mathsf{K}$: we say that an endomorphism $\alpha\colon X\to X$ in $\mathsf{K}$ is saturated if $\mathsf{id}\leq\alpha\text{ and }\alpha\circ\alpha\leq\alpha$. Whenever $S=(S,m,e)$ is a monad then $\alpha\colon X\to SX$ is saturated if the endomorphism \alpha\colon X\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}X is saturated in the order enriched category $\mathcal{K}\mspace{-1.0mu}l(S)$. If we assume $(S,m,e)$ is a monad on an order enriched category $\mathsf{K}$ and $S$ is monotonic333 $f\leq g\implies Sf\leq Sg$ for any pair of morphisms in $\mathsf{K}$ with a common domain and codomain. then we can introduce an order on the category $\mathcal{K}\mspace{-1.0mu}l(S)$ which arises from the order enrichment of the base category $\mathsf{K}$ in an obvious way. In this case, the inequalities that define a saturated endomorphism can be translated into the language of $\mathsf{K}$ by: $e\leq\alpha\text{ and }m\circ S\alpha\circ\alpha\leq\alpha$. These two axioms bear resemblance to the axioms that define Eilenberg-Moore algebras for $S$. The purpose of Section 4 is to elaborate more on this connection.

Let $\mathcal{K}\mspace{-1.0mu}l(S)$ be order enriched. By $\mathsf{Sat}(S)$ we denote the category whose objects are saturated $S$-coalgebras and morphisms are maps $f\colon X\to Y\in\mathsf{K}$ between the carriers of $\alpha\colon X\to SX$ and $\beta\colon Y\to SY$ which satisfy $Sf\circ\alpha\leq\beta\circ f$. Following [8, 10] we say that the monad $S$ admits saturation if for any $S$-coalgebra $\alpha\colon X\to SX$ there is $\alpha^{\ast}\colon X\to SX\in\mathsf{Sat}(S)$ such that $\alpha^{\ast}$ is the smallest saturated coalgebra which satisfies $\alpha\leq\alpha^{\ast}$ and $f\circ\alpha\Box\beta\circ Sf\implies f\circ\alpha^{\ast}\Box\beta^{\ast}\circ Sf$ for $\Box\in\{\leq,\geq\}$ and any $f\colon X\to Y\in\mathsf{K}$.

Example 2.2**.**

The monad $\overline{M}\colon\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})\to\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$ from Ex. 2.1 admits saturation [8]. Given any \alpha\colon X\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{M}X=X\to\mathcal{P}(M\times X) the saturated map $\alpha^{\ast}\colon X\to\mathcal{P}(M\times X)$ satisfies: $x\stackrel{{\scriptstyle 1}}{{\to}}_{\alpha^{\ast}}x$ for any $x\in X$ and $x\stackrel{{\scriptstyle m_{1}\cdot\ldots\cdot m_{k}}}{{\longrightarrow}}_{\alpha^{\ast}}x^{\prime}\iff x\stackrel{{\scriptstyle m_{1}}}{{\to}}_{\alpha}x_{1}\stackrel{{\scriptstyle m_{1}}}{{\to}}_{\alpha}\ldots\stackrel{{\scriptstyle m_{k}}}{{\to}}_{\alpha}x_{k}=x^{\prime}$.

3 Classical automata and regular languages, revisited

The main purpose of the section is to restate the basic properties and definitions from non-deterministic automata theory in the language of category theory. We will elaborate more on the (co)algebraic characterisation of classical regular languages from this perspective. This section should serve as a more detailed introduction to the remaining part of the paper.

A (finite non-deterministic) automaton [23] is a tuple $\mathcal{A}=(X,\delta\subseteq X\times\Sigma\times X,\mathcal{F}\subseteq X)$, where $X$ is a finite set called the set of states, $\delta$ is the transition and $\mathcal{F}$ is the set of final states. The language $L(\mathcal{A},x)$ of a state $x\in X$ in the automaton $\mathcal{A}$ is defined to be the set of words $\{w\in\Sigma^{\ast}\mid x\stackrel{{\scriptstyle w}}{{\to}}x^{\prime}\in\mathcal{F}\}$, where $x\stackrel{{\scriptstyle\varepsilon}}{{\to}}x^{\prime}$ iff $x=x^{\prime}$ and $x\stackrel{{\scriptstyle w}}{{\to}}x^{\prime}\stackrel{{\scriptstyle\Delta}}{{\iff}}x\stackrel{{\scriptstyle a_{1}}}{{\to}}x_{1}\stackrel{{\scriptstyle a_{2}}}{{\to}}x_{2}\ldots\stackrel{{\scriptstyle a_{n}}}{{\to}}x_{n}=x^{\prime}$ for $w=a_{1}\ldots a_{n}$ and $y\stackrel{{\scriptstyle a}}{{\to}}y^{\prime}\stackrel{{\scriptstyle\Delta}}{{\iff}}(y,a,y^{\prime})\in\delta$ for $y,y^{\prime}\in X$ and $a\in\Sigma$ 444Note that the textbook definition of an automaton usually includes the specification of the so-called initial state (see \eg[23]). Then the language of an automaton is defined to be the language of its initial state.. Note that since $X$ is finite we can assume without any loss of generality that $X=n$ for some positive integer $n$. We can see that $\delta$ can be encoded by a map $\alpha\colon n\to\mathcal{P}(\Sigma\times n);i\mapsto\{(a,j)\mid i\stackrel{{\scriptstyle a}}{{\to}}j\text{ in }\mathcal{A}\}$. Hence, the automaton $\mathcal{A}$ can be viewed as a pair $(\alpha\colon n\to\mathcal{P}(\Sigma\times n),\mathcal{F}\subseteq n).$

Automata in categories

We will now focus on the categorical perspective on non-deterministic automata and their languages. First, we introduce basic players of this paragraph and establish the notation. Here we work with two main categories, namely: $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$ and Set. These two categories share the class of objects: all sets. What is different is the morphisms and the compositions: we denote the morphisms from $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$ by \longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{\mkern-21.0mu\circ\mkern 10.0mu} and the maps from Set by $\to$.

Hence, X\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}Y=X\to\mathcal{P}Y. Considering the fact that the monad $(\Sigma^{\ast}\times\mathcal{I}d,m,e)$ lifts to the monad $(\overline{\Sigma^{\ast}},\overline{m},\overline{e})=(\overline{\Sigma^{\ast}},\{-\}\circ m,\{-\}\circ e)$ on $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$ (as in Ex. 2.1) the codomain of the transition map $\alpha$ of $\mathcal{A}$ changes depending on which category it is considered in—as summarised aside. Since the monad $\overline{\Sigma^{\ast}}$ admits saturation we also have the map \alpha^{\ast}\colon n\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{\Sigma^{\ast}}n=n\to\mathcal{P}(\Sigma^{\ast}\times n) given by (\cfExample 2.2): $\alpha^{\ast}(i)=\{(\varepsilon,i)\}\cup\{(a_{1}\ldots a_{k},j)\mid i\stackrel{{\scriptstyle a_{1}}}{{\to}}_{\alpha}\ldots\stackrel{{\scriptstyle a_{k}}}{{\to}}_{\alpha}i_{k}=j\}.$ Note that there is an obvious bijection between the set of all languages $L\subseteq\Sigma^{\ast}$ and maps $1\to\mathcal{P}(\Sigma^{\ast}\times 1)$. This allows us to represent the language $L(\mathcal{A},i)$ of a state $i$ in the automaton $\mathcal{A}$ in terms of a morphism L(\alpha,\mathcal{F},i)\colon 1\to\mathcal{P}(\Sigma^{\ast}\times 1)=1\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{\Sigma^{\ast}}1, which maps the unique element of $1$ onto $\{(w,1)\mid w\in L(\mathcal{A},i)\}$. It is easy to see that this language morphism can be expressed in terms of a composition of maps calculated in $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$ (conf. Table 1).

Algebra-coalgebra language coincidence

The entry in the first column of Table 1 may be viewed as a coalgebraic (automata) definition of regular languages stated in the category $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$. Interestingly, it immediately allows us to see the dual, algebraic, characterisation of these languages. Indeed, the category $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$ comes with $(-)_{-}\colon\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})\to\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})^{op}$ mapping any object onto itself and any map f\colon X\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}Y=X\to\mathcal{P}Y onto

[TABLE]

Additionally, it can be shown that the functor $\overline{\Sigma^{\ast}}$ on $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$ commutes with $(-)_{-}$, \ie$(\overline{\Sigma^{\ast}}f)_{-}=\overline{\Sigma^{\ast}}f_{-}$ for any f\colon X\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}Y\in\mathcal{K}\mspace{-1.0mu}l(\mathcal{P}). It turns out that (\alpha^{\ast})_{-}\colon\overline{\Sigma^{\ast}}n\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}n in $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$ is an Eilenberg-Moore algebra for the monad $(\overline{\Sigma^{\ast}},\overline{m},\overline{e})$ from Example 2.1. Moreover, the $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$-morphism L(\alpha,\mathcal{F})=n\stackrel{{\scriptstyle\alpha^{\ast}}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}\overline{\Sigma^{\ast}}n\stackrel{{\scriptstyle\overline{\Sigma^{\ast}}\chi_{\mathcal{F}}}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}\overline{\Sigma^{\ast}}1=n\to\mathcal{P}(\Sigma^{\ast}\times 1) which maps $i$ to its language $L(\alpha,\mathcal{F},i)(1)=\{(w,1)\mid w\in L(\mathcal{A},i)\}$ satisfies the following statement.

Fact 1**.**

The map L(\alpha,\mathcal{F})_{-}\colon\overline{\Sigma^{\ast}}1\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}n=\Sigma^{\ast}\times 1\to\mathcal{P}n, which maps a pair $(w,1)$ to the set of states of $(\alpha,\mathcal{F})$ that accept $w$, is an algebra homomorphism from the free Eilenberg-Moore algebra \overline{m}_{1}\colon\overline{\Sigma^{\ast}}\overline{\Sigma^{\ast}}1\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{\Sigma^{\ast}}1 to the algebra (\alpha^{\ast})_{-}\colon\overline{\Sigma^{\ast}}n\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}n. Additionally, any homomorphism from $\overline{m}_{1}$ to $(\alpha^{\ast})_{-}$ in $\mathcal{EM}(\overline{\Sigma^{\ast}})$ is of the form $L(\alpha,\mathcal{F})_{-}$ for some $\mathcal{F}\subseteq n$.

The above statement is a consequence of a more general Theorem 4.3 stated in the next section. Since, as we will show in the remaining part of the paper, any Eilenberg-Moore algebra in $\mathcal{EM}(\overline{\Sigma^{\ast}})$ is of the form $(\alpha^{\ast})_{-}$ for some morphism $\alpha\colon X\to\mathcal{P}(\Sigma\times X)$, the above fact can be read as follows: a language map L\colon n\to\mathcal{P}(\Sigma^{\ast}\times 1)=n\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{\Sigma^{\ast}}1 is regular (\ie$L=L(\alpha,\mathcal{F})$ for some automaton $(\alpha,\mathcal{F})$) if and only if its dual L_{-}\colon\overline{\Sigma^{\ast}}1\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}n=\Sigma^{\ast}\times 1\to\mathcal{P}n is an algebra homomorphism from \overline{m_{1}}\colon\overline{\Sigma^{\ast}}\overline{\Sigma^{\ast}}1\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{\Sigma^{\ast}}1 to an Eilenberg-Moore algebra over a finite carrier. Interestingly, this characterization leads us to the following result (see Theorem 4.11 for a more general version).

Fact 2**.**

For $L\subseteq\mathbb{T}_{\Sigma^{\ast}\times\mathcal{I}d}(1,1)$ the map \widehat{L}\colon 1\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{\Sigma^{\ast}}1=1\to\mathcal{P}(\Sigma^{\ast}\times 1);1\mapsto\{l(1)\mid l\in L\} is regular if and only if there is a Lawvere theory morphism $h\colon\mathbb{T}_{\Sigma^{\ast}\times\mathcal{I}d}\to\mathbb{T}^{\prime}$ into a finitary555A theory morphism $h\colon\mathbb{T}\to\mathbb{T}^{\prime}$ is a functor which maps $n$ onto itself. A theory $\mathbb{T}^{\prime}$ is finitary if all hom-sets $\mathbb{T}^{\prime}(m,n)$ are finite. Lawvere theory $\mathbb{T}^{\prime}$ such that $L=h^{-1}(T^{\prime})$ for some $T^{\prime}\subseteq\mathbb{T}^{\prime}(1,1)$.

Since the restriction of $h$ to hom-sets: $\mathbb{T}_{\Sigma^{\ast}\times\mathcal{I}d}(1,1)$ and $\mathbb{T}^{\prime}(1,1)$, is a monoid homomorphism from the monoid $(\mathbb{T}_{\Sigma^{\ast}\times\mathcal{I}d}(1,1),\circ,\mathsf{id})$ to the monoid $(\mathbb{T}^{\prime}(1,1),\circ,\mathsf{id})$, the above statement may be viewed as a Lawvere theory generalization of the classical characterisation of regular languages as languages recognized by monoid homomorphisms.

The aim of the remaining part of the paper is to generalize these observations to arbitrary Set-based monads (modulo some extra assumptions).

Final remarks

Predominantly, in the coalgebraic literature finite behaviour (language) of systems is introduced in terms of the finite trace [39, 6, 26]. In the order enriched setting for which the type monad encodes terminal states, the finite trace is given by $\alpha^{\dagger}=\mu x.x\cdot\alpha$ [7]. However, in our setting the final states are not part of the transition and the language is defined via saturation. Although, as noted in [9, 17] these two approaches are equivalent we choose our approach since it shows a more evident connection between the algebraic and coalgebraic frameworks for defining languages emphasizing the duality between Eilenberg-Moore algebras and (a subcategory of) saturated coalgebras. At this point the reader may also wonder why we choose Lawvere theories as the setting for our algebraic characterisation of languages (akin to Fact 2). Indeed, such a treatment seems to be a redundant overcomplication in the light of a simple, monoid homomorphism characterisation. However, non-deterministic automata and regular languages in the classical sense revolve around sequential data. If we move away from sequential data and deal with \egtrees then we need to be able to simultaneously consider terms with more (but a finite number of) variables. We refer the reader to \eg[9] where a simple example to understand this phenomenon has been described in the context of regular tree languages and an analogue of the Kleene theorem for trees.

4 On algebra-coalgebra duality

The purpose of this section is to build a framework to reason about an algebra-coalgebra duality akin to Fact 1 which will allow us, in some cases, to state a general version of Fact 2. Given a monad $(S,m,e)$ on an order enriched category $\mathsf{K}$, we first elaborate more on a functor from the dual of the category $\mathcal{EM}(S)$ to the category $\mathsf{Sat}(S)$.

In what follows, we assume that for the order enriched category $\mathsf{K}$ we have:

1. (A)

a subcategory $\mathsf{J}$ of $\mathsf{K}$ with all objects from $\mathsf{K}$, 2. (B)

an identity on objects functor $(-)_{-}\colon\mathsf{K}\to\mathsf{K}^{op}$ which preserves the order, \ie$f\leq g\implies f_{-}\leq g_{-}$, 3. (C)

for any $f\colon X\to Y\in\mathsf{J}$ the map $f_{-}\colon Y\to X\in\mathsf{K}$ is its right adjoint in the poset $\mathsf{K}(X,Y)$.

The last item reworded, means that for any $f\colon X\to Y\in\mathsf{J}$ the map $f_{-}\colon Y\to X$ satisfies $f_{-}\circ f\geq\mathsf{id}$ and $f\circ f_{-}\leq\mathsf{id}$. Moreover, we assume that $(S,m,e)$ is a monad on $\mathsf{K}$ such that:

1. (D)

$S$ is monotonic, $m_{X}\colon S^{2}X\to SX,e_{X}\colon X\to SX\in\mathsf{J}$ for any object $X$ and $S(f_{-})=(Sf)_{-}$ for any morphism $f\colon X\to Y\in\mathsf{K}$.

Example 4.1**.**

Our prototypical example of $\mathsf{J}$ and $\mathsf{K}$ are Set and $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$ respectively, with the inclusion functor given by $\textnormal{{Set}}\to\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$ taking any set to itself and any map $f\colon X\to Y$ to $\{-\}\circ f\colon X\to\mathcal{P}Y;x\mapsto\{f(x)\}$. The order on $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$ is defined in a natural manner by $f\colon X\to\mathcal{P}Y\leq g\colon X\to\mathcal{P}Y\iff f(x)\subseteq g(x)$ for any $x\in X$. The category $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$ is equipped with a functor $(-)_{-}\colon\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})\to\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})^{op}$ which assigns to any object itself and to any morphism $f\colon X\to\mathcal{P}Y$ the map $f_{-}$ given in (OP). It is easy to verify that (A)-(C) hold for this choice of categories. Now if we take $S$ to be the lifting $(\overline{\Sigma^{\ast}},\{-\}\circ m,\{-\}\circ e)$ of the monad $(\Sigma^{\ast}\times\mathcal{I}d,m,e)$ to $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$ then it satisfies (D). In Section 5 we will see other examples of $\mathsf{J}$, $\mathsf{K}$ and $S$ that meet the above requirements.

Let us now recall that an Eilenberg-Moore algebra $a\colon SX\to\leavevmode\nobreak\ X$ makes the standard EM-diagrams commute for $(S,m,e)$. By applying $(-)_{-}$ to these diagrams and by (D) we get commutativity of the diagrams on the right. Hence $Sa_{-}\cdot a_{-}=m_{-}\circ a_{-}$ and $e_{-}\circ a_{-}=\mathsf{id}$. This means that $m\circ Sa_{-}\circ a_{-}=m\circ m_{-}\circ a_{-}$ together with $e\circ e_{-}\circ a_{-}=e.$ By (C) and (D), this finally means that: $m\circ Sa_{-}\circ a_{-}\leq a_{-}\text{ and }e\leq a_{-}$. These are the inequalities that define a saturated $S$-coalgebra. Moreover, if $h\colon X\to Y$ is a homomorphism in $\mathcal{EM}(S)$ between algebras $a\colon SX\to X$ and $b\colon SY\to Y$ then $a_{-}\circ h_{-}=Sh_{-}\circ b_{-}$. Hence, $h_{-}\colon Y\to X$ is a morphism from $b_{-}$ to $a_{-}$ in $\mathsf{Sat}(S)$. The above remark allows us to define a functor $\mathsf{CoAlg}\colon\mathcal{EM}(S)^{op}\to\mathsf{Sat}(S),$ which assigns to any algebra $a\colon SX\to X$ the coalgebra $a_{-}\colon X\to SX$ and to an algebra homomorphism $h\colon X\to Y$ from $a\colon SX\to X$ to $b\colon SY\to Y$ the $S$-coalgebra map $h_{-}\colon Y\to X$.

Remark 4.2**.**

The functor $\mathsf{CoAlg}$ maps a homomorphism $h$ between algebras $a$ and $b$ onto a strict homomorphism $h_{-}$ between coalgebras $b_{-}$ and $a_{-}$.

Theorem 4.3**.**

Let $b\colon SY\to Y$ be an Eilenberg-Moore. The morphism $h_{-}\colon Y\to SX$ is the opposite of a homomorphism $h\colon SX\to Y$ from the Eilenberg-Moore algebra $m_{X}\colon S^{2}X\to SX$ to $b\colon SY\to Y$ iff $h_{-}=Sf\circ b_{-}$ for some $f\colon Y\to X$.

Theorem 4.3 is a generalisation of Fact 1 and provides us with the foundation for generalising the notion of regular maps for non-deterministic automata.

4.1 Duality

Let us now denote by $\mathcal{SAT}(S)$ a subcategory of $\mathsf{Sat}(S)$ consisting of saturated $S$-coalgebras whose duals are Eilenberg-Moore algebras and strict homomorphisms between them. By Remark 4.2 we have a category isomorphism

[TABLE]

Note that in the above duality we do not have to assume that the monad $S$ admits saturation. However, if it does then sometimes it is possible to describe members of $\mathcal{SAT}(S)$ (and hence also of $\mathcal{EM}(S)$) in terms of $\alpha^{\ast}\colon X\to SX$ for a certain choice of maps $\alpha\colon X\to SX$. One example of this phenomenon is described below, where for a free monad $F^{\ast}$ over a functor $F$ the class of objects of $\mathcal{SAT}(F^{\ast})$ is (modulo some additional requirements) is given by saturating $F$-coalgebras only.

Duality for free monads

Let $F\colon\mathsf{K}\to\mathsf{K}$ be a functor and let $(F^{\ast},m,e)$ be the free monad over $F$ together with the transformation $\nu\colon F\implies F^{\ast}$. Assume that (A)-(D) hold for $(F^{\ast},m,e)$ on $\mathsf{K}$ with $F^{\ast}$ admitting saturation. If $\mathsf{K}$ has binary coproducts then the object $F^{\ast}X$ is the carrier of the initial $F(-)+X$-algebra $i_{X}\colon FF^{\ast}X+X\to F^{\ast}X$ [2]. Any Eilenberg-Moore algebra $a\colon F^{\ast}X\to X$ for the monad $F^{\ast}$ is uniquely determined by $\underline{a}\triangleq FX\stackrel{{\scriptstyle\nu_{X}}}{{\to}}F^{\ast}X\stackrel{{\scriptstyle a}}{{\to}}X$ as $a\colon F^{\ast}X\to X$ can be recovered from $\underline{a}$ in terms of a unique homomorphism between the $F(-)+X$-algebras $i_{X}\colon FF^{\ast}X+X\to F^{\ast}X$ and $[\underline{a},id_{X}]\colon FX+X\to X$. In this case, if we assume the dual of the saturated map $(X\stackrel{{\scriptstyle\alpha}}{{\to}}FX\stackrel{{\scriptstyle\nu_{X}}}{{\to}}F^{\ast}X)^{\ast}$ is an Eilenberg-Moore algebra for the monad $F^{\ast}$ for any $\alpha\colon X\to FX$ and that for any Eilenberg-Moore algebra $a\colon F^{\ast}X\to X$, the map $a$ is the least EM-algebra satisfying $F^{\ast}X\stackrel{{\scriptstyle\nu_{-}}}{{\to}}FX\stackrel{{\scriptstyle\underline{a}}}{{\to}}X\leq F^{\ast}X\stackrel{{\scriptstyle a}}{{\to}}X$ then we have the following statement.

Proposition 4.4**.**

Any Eilenberg-Moore algebra for $F^{\ast}$ is of the form $\left\{(X\stackrel{{\scriptstyle\alpha}}{{\to}}FX\stackrel{{\scriptstyle\nu_{X}}}{{\to}}F^{\ast}X)^{\ast}\right\}_{-}$ for an $F$-coalgebra $\alpha\colon X\to FX$.

Hence, we immediately get the isomorphism between $\mathcal{EM}(F^{\ast})^{op}$ and the subcategory of $\mathsf{Sat}(F^{\ast})$ consisting of $\alpha^{\ast}\colon X\to F^{\ast}X$ for $\alpha\colon X\to FX\stackrel{{\scriptstyle\nu_{X}}}{{\to}}F^{\ast}X$ as objects and strict (coalgebra) homomorphisms as morphisms.

Example 4.5**.**

The Set-endofunctor $\Sigma^{\ast}\times\mathcal{I}d$ is a free monad over $\Sigma\times\mathcal{I}d\colon\textnormal{{Set}}\to\textnormal{{Set}}$ with the canonical embedding transformation $\Sigma\times\mathcal{I}d\implies\Sigma^{\ast}\times\mathcal{I}d$. As shown in \eg[8] this means that the lifting $\overline{\Sigma^{\ast}}$ to $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$ from Example 2.1 is a free monad over the lifting of the functor $\Sigma\times\mathcal{I}d$ to $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$. Moreover, it is not hard to verify that $\overline{\Sigma^{\ast}}$ satisfies the requirements of this subsection. Hence, Proposition 4.4 holds. This precisely means that every Eilenberg-Moore algebra for the monad $\overline{\Sigma^{\ast}}$ is obtained by taking the duals of saturations of maps of the form $X\to\mathcal{P}(\Sigma\times X)\hookrightarrow\mathcal{P}(\Sigma^{\ast}\times X)$.

4.2 Regular behaviours and two modes of recognition

The purpose of this subsection is to generalize the notion of regular language for classical non-deterministic automata from Section 3 to our more general setting. Taking into account Theorem 4.3 (generalizing Fact 1) and Table 1 we obtain what follows.

Assume $(T,\mu,\eta)$ and $(S,m,e)$ are monads on Set and that $(S,m,e)$ lifts to a monad $(\overline{S},\overline{m},\overline{e})$ on $\mathcal{K}\mspace{-1.0mu}l(T)$ via a distributive law $\lambda\colon ST\implies TS$. This yields a monadic structure on the composition $TS$ such that $\mathcal{K}\mspace{-1.0mu}l(TS)=\mathcal{K}\mspace{-1.0mu}l(\overline{S})$. Moreover, assume that (A)-(D) are met for $\mathsf{J}=\textnormal{{Set}}$, $\mathsf{K}=\mathcal{K}\mspace{-1.0mu}l(T)$ and the monad $(\overline{S},\overline{m},\overline{e})$. Arrows between two objects $X,Y$ in $\mathcal{K}\mspace{-1.0mu}l(T)$ will be denoted as before by X\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}Y, \ieX\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}Y=X\to TY. Akin to [14, 41, 9], we model automata (with branching type $T$ and linear type $S$) as follows:

Definition 4.6**.**

A $(T,S)$-automaton is a pair $(\alpha,\chi)$, where \alpha\colon n\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{S}n=n\to TSn is in $\mathcal{SAT}(\overline{S})$ and \chi\colon n\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}1=n\to T1 is an arbitrary map in $\mathcal{K}\mspace{-1.0mu}l(T)$. By behaviour (or language) of a state $i\in n$ in $\mathcal{A}$ we mean map 1\to TS1=1\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{S}1 given by:

[TABLE]

where the assignment i_{n}\colon 1\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}n=1\to Tn maps $1$ onto $\eta(i)$ for the unit $\eta_{n}\colon n\to Tn$.

Example 4.7**.**

If $T=\mathcal{P}$ and $S=\Sigma^{\ast}\times\mathcal{I}d$ then a $(\mathcal{P},\Sigma^{\ast}\times\mathcal{I}d)$-automaton is a pair $(\alpha\colon n\to\mathcal{P}(\Sigma^{\ast}\times n),\chi\colon n\to\mathcal{P}1)$ where $\alpha$ is a saturated morphism of a map $n\to\mathcal{P}(\Sigma\times n)$ (conf. Example 4.5) and $\chi$ is uniquely determined by the set $\mathcal{F}=\{i\in n\mid\chi(i)\neq\varnothing\}$. Hence, (up to the fact that we replace the original transition of a classical non-deterministic automaton with its saturated version and we replace the set of terminal states with its characteristic function) we obtain the known non-deterministic automaton. Additionally, by Table 1 the above definition of the language coincides with the classical one.

We are now ready to introduce the notion of regular behaviour: a map 1\to TS1=1\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{S}1 in $\mathcal{K}\mspace{-1.0mu}l(TS)=\mathcal{K}\mspace{-1.0mu}l(\overline{S})$ is regular if it is a behaviour of a state in a $(T,S)$-automaton. However, as mentioned in the final remarks of Section 3, in the case of non-sequential data we need to be able to cover regular morphisms with more than one variable (see also [9]). Hence, we introduce the following concept. A morphism 1\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{S}p=1\to TSp in $\mathcal{K}\mspace{-1.0mu}l(\overline{S})=\mathcal{K}\mspace{-1.0mu}l(TS)$ is called regular if it is of the form

[TABLE]

for a $\mathcal{SAT}(\overline{S})$-coalgebra $\alpha$ and \chi\colon n\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}p=n\to Tp. By Th. 4.3 the map n\stackrel{{\scriptstyle\alpha}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}\overline{S}n\stackrel{{\scriptstyle\overline{S}\chi}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}\overline{S}p is the dual to an Eilenberg-Moore algebra homomorphism from (the free $\overline{S}$-algebra at $p$) \overline{m}_{p}\colon\overline{S}^{2}p\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{S}p to (the dual of the saturated coalgebra $\alpha$) \alpha_{-}\colon\overline{S}n\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}n.

The above definition of regular maps (REG) easily extends to morphisms $p\to TSq$ coordinate-wise.

Theory of regular behaviours

As it turns out below (given some extra assumptions) the family of regular maps $p\to TSq$ contains the unit of the monad $TS$, is closed under cotupling and $\mathcal{K}\mspace{-1.0mu}l(TS)$-composition (and hence forms a subtheory of the theory $\mathbb{T}_{TS}$). We assume that

1. (I)

For any $n<\omega$ the map \overline{e}_{n}\colon n\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{S}n is $\mathcal{SAT}(\overline{S})$, 2. (II)

for any two \alpha\colon m\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{S}m and \beta\colon n\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{S}n which are members of $\mathcal{SAT}(\overline{S})$ the map m+n\stackrel{{\scriptstyle\alpha+\beta}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}\overline{S}m+\overline{S}n\stackrel{{\scriptstyle[\overline{S}\mathsf{inl},\overline{S}\mathsf{inr}]}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}\overline{S}(m+n) is in $\mathcal{SAT}(\overline{S})$, 3. (III)

if f\colon\overline{S}k\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}n and g\colon\overline{S}q\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}k are EM-homomorphisms from \overline{m}_{k}\colon\overline{S}^{2}k\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{S}k to a\colon\overline{S}n\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}n and from \overline{m}_{q}\colon\overline{S}^{2}q\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{S}q to b\colon\overline{S}k\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}k respectively then there is an Eilenberg-Moore algebra c\colon\overline{S}l\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}l for the monad $\overline{S}$, a homomorphism h\colon\overline{S}q\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}l from \overline{m}_{q}\colon\overline{S}^{2}q\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{S}q to c\colon\overline{S}l\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}l and $j\in l$ s.t.: \overline{S}q\stackrel{{\scriptstyle h}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}l\stackrel{{\scriptstyle(j_{l})_{-}}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}1=\overline{S}q\stackrel{{\scriptstyle(\overline{m}_{q})_{-}}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}\overline{S}^{2}q\stackrel{{\scriptstyle\overline{S}g}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}\overline{S}k\stackrel{{\scriptstyle f}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}n\stackrel{{\scriptstyle(i_{n})_{-}}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}1.

Theorem 4.8**.**

The collection of objects $p$ for $p<\omega$ and regular maps $p\to TSq$ as morphisms form $p$ to $q$ forms a subtheory of the theory $\mathbb{T}_{TS}$.

As a direct corollary of the above theorem we get a Kleene-like theorem characterisation of the regular map theory. Indeed, the subtheory of $\mathbb{T}_{TS}$ consisting of regular maps as morphisms is the smallest subtheory which contains all maps of the form p\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}q\stackrel{{\scriptstyle\overline{e}_{q}}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}\overline{S}q ($\dagger$) and all duals to Eilenberg-Moore algebras \overline{S}n\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}n. So, if there is a class $\mathcal{B}$ of regular morphisms in $\mathbb{T}_{TS}$ with a common domain and codomain for which $\bigcup_{r\in\mathcal{B}}r^{\mathsf{sat}}$ contains all members of $\mathcal{SAT}(\overline{S})$ over a finite state space, where $r^{\mathsf{sat}}=\{\alpha\mid r\leq\alpha\text{ and }\alpha\in\mathcal{SAT}(\overline{S})\}$, then the theory of regular morphisms is the smallest subtheory containing all maps from $\mathcal{B}$, all maps ($\dagger$) and being closed under $(-)^{\mathsf{sat}}$.

Example 4.9**.**

The above statement is true for our running example of regular maps for $\mathcal{P}(\Sigma^{\ast}\times\mathcal{I}d)$. In this case the theory of regular maps is given as the smallest theory containing all maps $m\to\mathcal{P}(\Sigma\times n)$ and being closed under finite unions and Kleene star closure (i.e. saturation) [9, 18, 19].

Lawvere theory morphism recognition

Finally, we point out that in the case when $T=\mathcal{P}$ a natural algebraic characterisation of regular maps holds. Indeed, if the monad $S$ is finitary666A Set-based monad is called finitary if for any $X$ and $x\in SX$ there is a finite subset $X_{0}\subseteq X$ such that $x\in SX_{0}$. This assumption about $S$ is technical and related to the fact that in this case the theory $\mathbb{T}_{S}$ associated with $S$ uniquely determines the monad $S$ [24]. then we can characterize regular morphisms 1\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{S}p=1\to\mathcal{P}Sp in terms of preimages of Lawvere theory morphisms as follows.

Definition 4.10**.**

A subset $L\subseteq\mathbb{T}_{S}(1,p)$ is recognizable if there is a Lawvere theory morphism $h\colon\mathbb{T}_{S}\to\mathbb{T}^{\prime}$ whose target is finitary, and a subset $T^{\prime}\subseteq\mathbb{T}^{\prime}(1,p)$ s.t. $L=h^{-1}(T^{\prime})$.

Theorem 4.11**.**

The map L\colon 1\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{S}p=1\to\mathcal{P}Sp\in\mathbb{T}_{\mathcal{P}S}(1,p) is regular if and only if the set $\{f\colon 1\to Sp\in\mathbb{T}_{S}(1,p)\mid f(1)\subseteq L(1)\}$ is recognizable.

5 Beyond non-deterministic automata

In this section we illustrate the generality of our results by listing some representative examples of models fitting our framework besides our running example of classical non-deterministic automata and their languages (details are in Appendix C).

Tree automata

For a non-empty set $\Sigma$, let $T_{\Sigma}$ be the free monad for the endofunctor $\mathcal{I}d\times\Sigma\times\mathcal{I}d$ over Set: $T_{\Sigma}X$ is the set of binary trees with $\Sigma$-labelled nodes and leaves in the set $X$, $T_{\Sigma}f$ is the function that replaces leaves according to the function $f$. Monadic multiplication is tree grafting, and monadic unit is the embedding into trees with one leaf (and no internal nodes). The monad $T_{\Sigma}$ lifts to a monad $\overline{T_{\Sigma}}$ on $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$ by the unique extension of the distributive law of the functor $\mathcal{I}d\times\Sigma\times\mathcal{I}d$ over the monad $\mathcal{P}$ given by the assignment $(L\times\sigma\times R)\mapsto\{(l,\sigma,r)\mid l\in L,r\in R\}$ [8]. The monad $\overline{T_{\Sigma}}$ coincides with the free monad for the (canonical) lifting of $\mathcal{I}d\times\Sigma\times\mathcal{I}d$ to $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$ [8]. Additionally, the monad $\overline{T_{\Sigma}}$ admits saturation [9]. Indeed, if \alpha\colon X\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{T_{\Sigma}}X=X\to\mathcal{P}T_{\Sigma}X then $\alpha^{\ast}(x)=\bigcup_{n<\omega}(\mathsf{id}\cup\alpha)^{n}(x)$, where $(\mathsf{id}\cup\alpha)^{0}(x)=\{x\}$, $(\mathsf{id}\cup\alpha)^{1}(x)=\{x\}\cup\alpha(x)$ and if $t\in(\mathsf{id}\cup\alpha)(x)$ is with leaves in $\{x_{1},\ldots,x_{k}\}$ then a tree which is obtained from $t$ by replacing any occurrence of $x_{i}$ by some tree from $(\mathsf{id}\cup\alpha)^{n}(x_{i})$ is in $(\mathsf{id}\cup\alpha)^{n+1}(x)$. It can be checked that $\overline{T_{\Sigma}}$ satisfies the requirements of Section 4.1 and hence that Proposition 4.4 holds. As a consequence, Eilenberg-Moore algebras for $\overline{T_{\Sigma}}$ are dual to the saturations of morphism of form $X\to\mathcal{P}(X\times\Sigma\times X)\hookrightarrow\mathcal{P}T_{\Sigma}X$.

Let $\mathcal{A}=(\alpha\colon n\to\mathcal{P}T_{\Sigma}n,\chi\colon n\to\mathcal{P}1)$ be a $(\mathcal{P},T_{\Sigma})$-automaton. It follows from the above remark and Section 4.1 that the transition map $\alpha\in\mathcal{SAT}(\overline{T_{\Sigma}})$ of $\mathcal{A}$ is equivalent a map $\hat{\alpha}\colon n\to\mathcal{P}(n\times\Sigma\times n)$ (\ie$\alpha=(\nu_{n}\circ\hat{\alpha})^{\ast}$) and that the language accepted by a state $i\in n$ is characterised as: L(\mathcal{A},i)=1\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}n\stackrel{{\scriptstyle(\nu_{X}\circ\hat{\alpha})^{\ast}}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}\overline{T_{\Sigma}}n\stackrel{{\scriptstyle\overline{T_{\Sigma}}\chi}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}\overline{T_{\Sigma}}1, where $\nu$ is the canonical embedding of $\mathcal{P}(\mathcal{I}d\times\Sigma\times\mathcal{I}d)$ into $\mathcal{P}T_{\Sigma}$. By comparing this observation with the classical definition of a tree automaton and its language777A tree automaton is a pair $(\hat{\alpha}\colon n\to\mathcal{P}(n\times\Sigma\times n),\mathcal{F}\subseteq n)$. Intuitively, the language of a state $i$ in a tree automaton is given by the set of finite tree traces whose leaves are all in $\mathcal{F}$. More formally, this concept can be put into our setting by translating the classical definition of the behaviour accepted by the state $i\in n$ into the language of the Kleisli category for the monad $\mathcal{P}$ and is the following: 1\stackrel{{\scriptstyle i_{n}}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}n\stackrel{{\scriptstyle\hat{\alpha}^{\ast}}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}\overline{T_{\Sigma}}n\stackrel{{\scriptstyle\overline{T_{\Sigma}}\chi_{\mathcal{F}}}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}\overline{T_{\Sigma}}1, where \chi_{\mathcal{F}}\colon n\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}1=n\to\mathcal{P}1 is as in Section 3. At this point it is also worth noting that originally non-deterministic tree automata did not have an evident coalgebraic transition map. However, our approach to defining these objects is equivalent to the original. See \eg[34, 9] for details. (see \eg[34]) we immediately get the following correspondence.

Theorem 5.1**.**

Regular maps $1\to\mathcal{P}T_{\Sigma}1$ for $\mathcal{P}T_{\Sigma}$ coincide with languages recognised by tree automata in the classical sense.

Theorem 4.11 instantly provides us with an algebraic characterisation of regular languages for tree automata we will now instantiate on a simple example. Let $\Sigma=\{a,b\}$ and consider a two state tree automaton whose transition morphism $\alpha\colon 2\to\mathcal{P}(2\times\Sigma\times 2)$ is defined by $1\mapsto\varnothing,2\mapsto\{(2,a,2),(1,b,1)\}$ and $\mathcal{F}=\{1\}$. The language accepted by the state $2$ consists of binary trees of height $>0$ whose nodes preceding the leaf nodes are all $b$ and the remaining non-leaf nodes are $a$. By following the guidelines of the proof of Theorem 4.11 we build a theory morphism $h\colon\mathbb{T}_{T_{\Sigma}}\to\mathbb{T}^{\prime}$ which recognizes the language of the state $2$ in the above automaton. The finitary theory $\mathbb{T}^{\prime}$ and the theory morphism $h$ are determined by the automaton $(\alpha,\mathcal{F})$ with the hom-set $\mathbb{T}^{\prime}(1,1)$ of $\mathbb{T}^{\prime}$ consisting of $4$ elements which are assignments $\mathcal{P}2\to\mathcal{P}2$ given in the table below. The composition in $\mathbb{T}^{\prime}$ of morphisms $\mathbb{T}^{\prime}(1,1)$ is the ordinary assignment composition of maps $\mathcal{P}2\to\mathcal{P}2$ given in the reversed order.

The morphism $h\colon\mathbb{T}_{T_{\Sigma}}\to\mathbb{T}^{\prime}$, if restricted to $\mathbb{T}_{T_{\Sigma}}(1,1)$, maps the tree $1$ to $\mathsf{id}$, any tree $t$ such that after the composition with the tree $(1,b,1)$ in $\mathbb{T}_{T_{\Sigma}}$ the result is in the language of the state $2$ to $a_{A}$, any tree from the language accepted by the state $2$ onto $b_{A}$ and any other to $b^{2}_{A}$. We see that our language of the state $2$ is given in terms of $h^{-1}(\{b_{A}\})$.

Weighted automata

For $(\mathcal{S},+,0,\cdot,1,\leq)$ a positive $\omega$-semiring888 A positive $\omega$-semiring is relational structure $(\mathcal{S},+,0,\cdot,1,\leq)$ with the property that $(\mathcal{S},+,0,\cdot,1)$ is a semiring with countable sums, $(\mathcal{S},\leq,0)$ is an $\omega$-complete partial order, $+$ and $\cdot$ are $\omega$-continuous in both arguments.

(\egthe set of non-negative reals extended with positive infinity $[0,+\infty]$), an $\mathcal{S}$-multiset is a pair $(X,\phi)$ where $X$ is a set and $\phi\colon X\to\mathcal{S}$ is a function such that the set $\operatorname*{\rm{supp}}(\phi)=\{x\mid\phi(x)>0\}$ (called support) is countable. We write $\mathcal{S}$-multiset as formal sums. The $\mathcal{S}$-multiset functor $\mathcal{M_{S}}\colon\textnormal{{Set}}\to\textnormal{{Set}}$ assigns to every set $X$ the set $\mathcal{M_{S}}X$ of $\mathcal{S}$-multisets with universe $X$, and to every function $f\colon X\to Y$ the function mapping each $(X,\phi)$ to $(X,\sum_{x\in\operatorname*{\rm{supp}}(\phi)}\phi(x)\bullet f(x))$. This functor carries a monad structure $(\mathcal{M_{S}},\mu,\eta)$ whose multiplication $\mu$ and unit $\eta$ are given on each set $X$ by the mappings: $(\mathcal{M_{S}}X,\psi)\mapsto\left(X,\sum(\phi(x)\cdot\psi(\phi))\bullet x\right)$ and $x\mapsto(X,x\bullet 1)$. The probability distribution monad $\mathcal{D}$ is a submonad of $\mathcal{M}_{[0,\infty]}$ [10].

The free monad $\Sigma^{\ast}$ lifts to a monad $\overline{\Sigma^{\ast}}$ on $\mathcal{K}\mspace{-1.0mu}l(\mathcal{M_{S}})$ by the unique extension of the distributive law of the functor $\Sigma\times\mathcal{I}d$ over the monad $\mathcal{M_{S}}$ given by the assignment $\Sigma\times(X,\phi)\mapsto(\Sigma\times X,\sum\phi(x)\bullet(\sigma,x))$ [10]. The main problem with this choice of monads is that they do not fit our setting from Section 4 directly. Indeed, $\mathcal{K}\mspace{-1.0mu}l(\mathcal{M_{S}})$ is not self-dual (due to the limited size of the cardinality of the support of functions in $\mathcal{M_{S}}$). There are two workarounds to this problem: one is to extend the definition of $\mathcal{M_{S}}$ to cover functions of arbitrary supports, the other is to realize that when dealing with regular behaviours as in (REG) we actually focus on systems over a finite state space. Hence, we restrict w.l.o.g. to the subcategory identified by finite sets. In this case, if $\Sigma^{\ast}$ is countable then any Eilenberg-Moore algebra a\colon\overline{\Sigma^{\ast}}n\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}n=\Sigma^{\ast}\times n\to\mathcal{M_{S}}n on $\mathcal{K}\mspace{-1.0mu}l(\mathcal{M_{S}})$ yields a saturated system a_{-}\colon n\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{\Sigma^{\ast}}n=n\to\mathcal{M_{S}}({\Sigma^{\ast}\times n}) by simple currying and uncurrying. Since $\overline{\Sigma^{\ast}}$ is the free monad over $\overline{\Sigma}$ on $\mathcal{K}\mspace{-1.0mu}l(\mathcal{M_{S}})$ [8], the Eilenberg-Moore algebra $a$ is uniquely determined by $\underline{a}\colon\Sigma\times n\to\mathcal{M_{S}}n$ (conf Subsec. 4.1). Hence, so is its dual $a_{-}$.

Let $\mathcal{A}=(\alpha\colon n\to\mathcal{M_{S}}(\Sigma^{\ast}\times n),\chi\colon n\to\mathcal{M_{S}}1)$ be a $(\mathcal{M_{S}},\Sigma^{\ast})$-automaton with the behaviour of a state $i\in n$ given by

[TABLE]

where $\nu$ is the canonical embedding of $\mathcal{M_{S}}(\Sigma\times\mathcal{I}d)$ into $\mathcal{M_{S}}(\Sigma^{\ast}\times\mathcal{I}d)$. This is essentially the classical presentation of an automaton weighted over $\mathcal{S}$999A weighted automaton is a pair $(\hat{\alpha}\colon n\to\mathcal{M_{S}}(\Sigma\times n),\chi\colon n\to\mathcal{S})$ and the language of a state $i\in n$ is the $\mathcal{S}$-multisetset $\left(\Sigma^{\ast},\lambda\sigma_{1}\dots\sigma_{k}.\sum\left\{\chi(j_{k})\cdot\prod_{p<k}\hat{\alpha}(j_{p})(\sigma_{p+1},j_{p+1})\,\middle|\,j_{0}=i,j_{1},\dots,j_{k}\in n\right\}\right)$. [37, 5].

Theorem 5.2**.**

Regular maps 1\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{\Sigma^{\ast}}1=1\to\mathcal{M}_{\mathcal{S}}(\Sigma^{\ast}\times 1) for $\mathcal{M}_{\mathcal{S}}({\Sigma^{\ast}}\times\mathcal{I}d)$ coincide with languages recognised by weighted automata in the classical sense.

Regular morphisms form a subtheory of $\mathbb{T}_{\mathcal{M}_{\mathcal{S}}({\Sigma^{\ast}}\times\mathcal{I}d)}$, as weighted languages enjoy Kleene Theorem [38].

Weighted tree automata and their languages are captured by our framework as well since the monad $T_{\Sigma}$ lifts to $\mathcal{K}\mspace{-1.0mu}l(\mathcal{M_{S}})$.

Fuzzy automata

For $(\mathcal{Q},\cdot,1,\leq)$ a unital quantale (\egthe real unit interval $([0,1],\cdot,1,\leq)$), let $(\mathcal{P_{Q}},\bigcup_{\mathcal{Q}},\{-\}_{\mathcal{Q}})$ be the $\mathcal{Q}$-fuzzy powerset monad and observe that the free monad $\Sigma^{\ast}$ lifts to $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P_{Q}})$ via the unique extension of the distributive law $\lambda\colon\Sigma\times\mathcal{I}d\to\mathcal{P_{Q}}$ given by $(\Sigma\times(X,\phi))\mapsto(\Sigma\times X,\lambda(\sigma,x).\phi(x))$, Proposition 4.4 holds for $\overline{\Sigma^{\ast}}$ since $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P_{Q}})$ admits saturation [12] and meets the requirements of Section 4.1. As a consequence, Eilenberg-Moore algebras for $\overline{\Sigma^{\ast}}$ are dual to the saturations of morphism of the form $X\to\mathcal{P_{Q}}(\Sigma\times X)\hookrightarrow\mathcal{P_{Q}}(\Sigma^{\ast}\times X)$.

Let $\mathcal{A}=(\alpha\colon n\to\mathcal{P_{Q}}(\Sigma^{\ast}\times n),\chi\colon n\to\mathcal{P_{Q}}1)$ be a $(\mathcal{P_{Q}},\Sigma^{\ast})$-automaton. The transition map $\alpha\in\mathcal{SAT}(\overline{\Sigma^{\ast}})$ of $\mathcal{A}$ is equivalently defined (by saturation and construction of $\Sigma^{\ast}$) as a map $\hat{\alpha}\colon n\to\mathcal{P_{Q}}(\Sigma\times n)$ and the language accepted by a state $i\in n$ as L(\mathcal{A},i)=1\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}n\stackrel{{\scriptstyle(\nu_{X}\circ\hat{\alpha})^{\ast}}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}\overline{\Sigma^{\ast}}n\stackrel{{\scriptstyle\overline{\Sigma^{\ast}}\chi}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}\overline{\Sigma^{\ast}}1. If we now recall the classical definition of a fuzzy automaton and its language101010A fuzzy automaton is a pair $(\hat{\alpha}\colon n\to\mathcal{P_{Q}}(\Sigma\times n),(n,\chi))$ and the language of a state $i\in n$ is the fuzzy set $\left(\Sigma^{\ast},\lambda\sigma_{1}\dots\sigma_{k}.\bigvee\left\{\chi(j_{k})\cdot\prod_{p<k}\hat{\alpha}(j_{p})(\sigma_{p+1},j_{p+1})\,\middle|\,j_{0}=i,j_{1},\dots,j_{k}\in n\right\}\right)$. (\egfrom [31, 15]) we immediately get the following coincidence.

Theorem 5.3**.**

Regular maps 1\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{\Sigma^{\ast}}1=1\to\mathcal{P_{Q}}(\Sigma^{\ast}\times 1) for $\mathcal{P_{Q}}({\Sigma^{\ast}}\times\mathcal{I}d)$ coincide with languages recognised by fuzzy automata in the classical sense.

Regular maps form a subtheory of $\mathbb{T}_{\mathcal{P_{Q}}({\Sigma^{\ast}}\times\mathcal{I}d)}$, as fuzzy languages enjoy Kleene Theorem as they are closed under composition, sums, and saturation [31, 40].

Fuzzy tree automata and their languages are similarly captured by our framework since $T_{\Sigma}$ lifts to $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P_{Q}})$ and the resulting monad meets the hypotheses of Proposition 4.4.

6 Conclusion

The paper’s goal was to build a connection between two approaches towards categorical language theory: the coalgebraic and algebraic language theory for monads. For a pair of $\mathsf{Set}$-based monads $T$ and $S$ (with $T$ modelling the branching type and $S$ the linear type) which admit a monadic structure on their composition $TS$ we defined regular maps $p\to TSq$ that generalize regular languages known in classical non-deterministic automata theory. Although these maps are of coalgebraic nature (as they are, roughly speaking, behaviours of finite $(T,S)$-automata), they arise as duals of certain Eilenberg-Moore algebra homomorphisms. The key ingredient to all our results was the Eilenberg-Moore algebra-saturated coalgebra duality based on the self-duality of (a certain subcategory of) $\mathcal{K}\mspace{-1.0mu}l(T)$.

We showed that, given some extra assumptions, regular maps form a subtheory of the Lawvere theory associated with the monad $TS$. Moreover, we stated a Kleene-like theorem saying that the Lawvere theory of regular morphisms is the smallest subtheory containing all branching type maps and duals of Eilenberg-Moore algebras of a lifting of $S$ to $\mathcal{K}\mspace{-1.0mu}l(T)$.

Additionally, whenever $T=\mathcal{P}$ we showed that regular maps of type $\mathcal{P}S$ are characterised as maps recognized by Lawvere theory morphisms whose codomains are finitary theories.

Although, our running example were classical non-deterministic automata and regular languages we instantiated the theory presented in this paper to tree automata, fuzzy automata and weighted automata.

Related work

We build on the coalgebraic language theory from [3, 41, 18, 19, 9], the algebraic language theory stated in the context of Eilenberg-Moore algebras in [4] and some classical results from [34, 43, 16]. We are unaware of any research which exploits the Eilenberg-Moore algebra-saturated coalgebra duality on the categorical level to show an equivalence between regular and recognizable languages akin to our approach. The closest are [1] and [36], both study Eilenberg-type dualities: The first work characterises deterministic word-automata in a locally finite variety whereas our work applies also \egto tree automata. The second work provides a duality result between algebras for a monad and coalgebras for a comonad whereas we investigate dualities between algebras and saturated coalgebras for the same type. Moreover, we present a Kleene-like theorem for regular maps which (up to our knowledge) has not been stated at this level of generality.

Future work

This paper provides evidence that Lawvere theory morphism recognition is a natural context to investigate whether concepts and properties known in the algebraic language theory (syntactic algebra, star-free language characterization, and more \cf[42]) can be stated at this level of generality. A key result in this direction would be the extension of the notion of morphism recognition and our results beyond non-determinism ($T=\mathcal{P}$). We see the recent enriched view on the extended finitary monad-Lawvere theory correspondence [20] as a helpful stepping stone towards this goal.

Appendix A Basic notions (extended)

A.1 Algebras and coalgebras

Let $F:\mathsf{C}\to\mathsf{C}$ be a functor. An $F$-coalgebra ($F$-algebra) is a morphism $\alpha:A\to FA$ (resp. $a:FA\to A$). The object $A$ is called a carrier of the underlying $F$-(co)algebra. Given two coalgebras $\alpha:A\to FA$ and $\beta:B\to FB$ a morphism $h:A\to B$ is homomorphism from $\alpha$ to $\beta$ provided that $\beta\circ h=F(h)\circ\alpha$. For two algebras $a:FA\to A$ and $b:FB\to B$ a morphism $h:A\to B$ is called homomorphism from $a$ to $b$ if $b\circ F(h)=h\circ a$. The category of all $F$-coalgebras ($F$-algebras) and homomorphisms between them is denoted by $\mathsf{CoAlg}(F)$ (resp. $\mathsf{Alg}(F)$). Let $\Sigma$ be a set of labels.

A.2 Monads

A monad on $\mathsf{C}$ is a triple $(T,\mu,\eta)$, where $T:\mathsf{C}\to\mathsf{C}$ is an endofunctor and $\mu:T^{2}\implies T$, $\eta:\mathcal{I}d\implies T$ are two natural transformations for which the following diagrams commute:

[TABLE]

The transformation $\mu$ is called multiplication and $\eta$ unit.

A.3 Kleisli category

We start this section by recalling the notion of Kleisli category for a monad and listing basic examples of monads and their Kleisli categories we will work with throughout this paper.

Any monad $(T:\mathsf{C}\to\mathsf{C},\mu,\eta)$ gives rise to the Klesli category $\mathcal{K}\mspace{-1.0mu}l(T)$ for $T$: it has the class of objects equal to the class of objects of $\mathsf{C}$ and for two objects $X,Y$ in $\mathcal{K}\mspace{-1.0mu}l(T)$ we have ${\mathcal{K}\mspace{-1.0mu}l(T)}(X,Y)={\mathsf{C}}(X,TY)$ with the composition $\bullet$ in $\mathcal{K}\mspace{-1.0mu}l(T)$ defined between two morphisms $f:X\to TY$ and $g:Y\to TZ$ by $g\bullet f:=\mu_{Z}\circ T(g)\circ f$. In order to emphasize the distinction between morphisms in $\mathsf{C}$ and in $\mathcal{K}\mspace{-1.0mu}l(T)$ any morphism between two objects $X,Y$ will be denoted by $X\to Y$ if it is a morphism in $\mathsf{C}$ and X\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}Y if it is a morphism in $\mathcal{K}\mspace{-1.0mu}l(T)$. Hence, X\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}Y=X\to TY and X\stackrel{{\scriptstyle f}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}Y\stackrel{{\scriptstyle g}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}Z=X\stackrel{{\scriptstyle f}}{{\to}}TY\stackrel{{\scriptstyle Tg}}{{\to}}T^{2}Z\stackrel{{\scriptstyle\mu_{Z}}}{{\to}}TZ. The category $\mathsf{C}$ is a subcategory of $\mathcal{K}\mspace{-1.0mu}l(T)$ where the inclusion functor $(-)^{\sharp}$ sends each object $X\in\mathsf{C}$ to itself and each map $f:X\to Y$ in $\mathsf{C}$ to the morphism $f^{\sharp}:X\to TY;f^{\sharp}\triangleq\eta_{Y}\circ f.$

Example A.1**.**

The powerset endofunctor $\mathcal{P}:\textnormal{{Set}}\to\textnormal{{Set}}$ is a monad whose multiplication $\bigcup:\mathcal{P}^{2}\implies\mathcal{P}$ and unit $\{-\}:\mathcal{I}d\implies\mathcal{P}$ are given by $\bigcup:\mathcal{P}\mathcal{P}X\to\mathcal{P}X;S\mapsto\bigcup S$ and $\{-\}_{X}:X\to\mathcal{P}X;x\mapsto\{x\}$. The Kleisli category $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$ consists of sets as objects and maps $f:X\to\mathcal{P}Y$ and $g:Y\to\mathcal{P}Z$ with the composition $g\bullet f:X\to\mathcal{P}Z$ defined as follows: $g\bullet f(x)=\{z\in Z\mid z\in\bigcup g(f(x))\}.$ It is a simple exercise to prove that this category is isomorphic to the category $\mathsf{Rel}$ of sets as objects and binary relations with standard relation composition as morphisms and their composition.

A.3.1 Distributive laws and liftings

Let $(T,\mu,\eta)$ be a monad on $\mathsf{C}$ and $S$ a $\mathsf{C}$-endofunctor. A distributive law $\lambda:ST\implies TS$ of the functor $S$ over the monad $T$, \ienatural transformation which satisfies extra conditions (see \eg[32] for details):

STX$$TSX$$SX$$S\eta$$\eta$$\lambda$$STX$$TSX$$ST^{2}X$$TSTX$$T^{2}SX$$S\mu$$\lambda$$\mu$$\lambda$$T\lambda

A distributive law of the monad $(S,m,e)$ on $\mathsf{C}$ over the monad $(T,\mu,\eta)$ [2] is a distributive law $\lambda:ST\implies TS$ of the underlying functor $S$ over the monad $T$ which additionally satisfies:

STX$$TSX$$TX$$e$$Te$$\lambda$$STX$$TSX$$SSTX$$STSX$$TSSX$$m$$\lambda$$Tm$$S\lambda$$\lambda

Let $\lambda:ST\implies TS$ be a distributive law of a functor $S:\mathsf{C}\to\mathsf{C}$ over a monad $(T,\mu,\eta)$ on $\mathsf{C}$. This allows us to define a functor $\overline{S}:\mathcal{K}\mspace{-1.0mu}l(T)\to\mathcal{K}\mspace{-1.0mu}l(T)$ as follows. Any object $X\in\mathcal{K}\mspace{-1.0mu}l(T)$ is mapped onto $SX\in\mathcal{K}\mspace{-1.0mu}l(T)$. Any morphism f:X\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}Y=X\to TY is mapped onto \overline{S}f:\overline{S}X\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{S}Y=SX\to TSY given by: $\overline{S}f\triangleq SX\stackrel{{\scriptstyle Sf}}{{\to}}STY\stackrel{{\scriptstyle\lambda_{Y}}}{{\to}}TSY.$ We then say that $S:\mathsf{C}\to\mathsf{C}$ lifts to $\overline{S}:\mathcal{K}\mspace{-1.0mu}l(T)\to\mathcal{K}\mspace{-1.0mu}l(T)$ via $\lambda$.

If $\lambda:ST\implies TS$ is a distributive law of a monad $(S,m,e)$ over the monad $(T,\mu,\eta)$ then this allows to introduce a monadic structure $(\overline{S},\overline{m},\overline{e})$ on the lifting $\overline{S}$ of the functor $S$ to $\mathcal{K}\mspace{-1.0mu}l(T)$ by putting $\overline{e}_{X}\triangleq\eta_{X}\circ e_{X}$ and $\overline{m}_{X}\triangleq\eta_{SX}\circ m_{X}$. We then say that the monad $(S,m,e)$ on $\mathsf{C}$ lifts to the monad $(\overline{S},\overline{m},\overline{e})$ on $\mathcal{K}\mspace{-1.0mu}l(T)$ via $\lambda$.

This also yields a monadic structure on $TS:\mathsf{C}\to\mathsf{C}$ with $\mathcal{K}\mspace{-1.0mu}l(TS)=\mathcal{K}\mspace{-1.0mu}l(\overline{S})$, where the composition $g\cdot f$ is given in $\mathsf{C}$ for $f\colon X\to TSY$ and $g\colon Y\to TSZ$ by:

X$$TSY$$(TS)^{2}Z$$T^{2}S^{2}Z$$T^{2}SZ$$TSZ$$g\cdot f$$f$$TSg$$T\lambda_{SZ}$$T^{2}m_{Z}$$\mu_{SZ}

A.3.2 Free monads and their liftings

A free monad [2] over a functor $F:\mathsf{C}\to\mathsf{C}$ is a monad $(F^{\ast},m,e)$ together with a natural transformation $\nu:F\implies F^{\ast}$ such that for any monad $S=(S,m^{\prime},e^{\prime})$ on $\mathsf{C}$ and a natural transformation $s:F\to S$ there is a unique monad morphism $\overline{s}:F^{\ast}\to S$ such that $\overline{s}\circ\nu=s$. The free monad $F^{\ast}$ over $F$ has an explicit construction in terms of free $F$-algebras as follows. Let $\mathsf{C}$ admit binary coproducts $+$ with the cotupling denoted by $[-,-]$ and the coprojections into the first and second component of $X+Y$ by $\mathsf{inl}:X\to X+Y$ and $\mathsf{inr}:Y\to X+Y$ respectively. Assume $F$ has an initial $F(-)+X$ algebra (=free $F$-algebra over $X$) for any $X$. This allows us to define a functor $F^{\ast}:\mathsf{K}\to\mathsf{K}$ which maps any object $X$ onto the carrier of the initial $F(-)+X$ algebra $i_{X}:FF^{\ast}X+X\to F^{\ast}X$. Moreover, this functor carries a monadic structure $(F^{\ast},m,e)$ which arises from universal properties of the initial algebras $i_{X}$ and turns $(F^{\ast},m,e)$ into a free monad over $F$ with a natural transformation $\nu:F\implies F^{\ast}$ on its $X$-component given by:

[TABLE]

Additionally, if $F:\mathsf{C}\to\mathsf{C}$ is a funtor that lifts to $\mathcal{K}\mspace{-1.0mu}l(T)$ and admits a free monad $F^{\ast}:\mathsf{C}\to\mathsf{C}$ then the monad $F^{\ast}$ lifts to a monad $\overline{F^{\ast}}:\mathcal{K}\mspace{-1.0mu}l(T)\to\mathcal{K}\mspace{-1.0mu}l(T)$ which is a free monad over the lifting $\overline{F}$ [8].

Example A.2**.**

Our two running examples of monads, namely $\Sigma^{\ast}\times\mathcal{I}d$ and $T_{\Sigma}$, are both free monad over the functors $\Sigma\times\mathcal{I}d$ and $\mathcal{I}d\times\Sigma\times\mathcal{I}d$ respectively. Hence, since the functors $\Sigma\times\mathcal{I}d$ and $\mathcal{I}d\times\Sigma\times\mathcal{I}d$ lift to $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$ [22], the monads $\Sigma^{\ast}\times\mathcal{I}d$ and $T_{\Sigma}$ also do. Their distributive laws over $\mathcal{P}$ are given in Example 2.1 and Section 5. The statement remains true if we change $\mathcal{P}$ into $\mathcal{P_{Q}}$ or $\mathcal{M_{S}}$.

A.4 Eilenberg-Moore algebras

Given a monad $(T,\mu,\eta)$ on a category $\mathsf{C}$ we say that a $T$-algebra $a:TX\to X$ is an Eilenberg-Moore algebra if $a\circ Ta=a\circ\mu_{X}$ and $id_{X}=a\circ\eta_{X}$:

[TABLE]

The collection of all Eilenberg-Moore algebras for the monad $T$ as objects with $T$-algebra homomorphisms as morphisms forms the category of Eilenberg-Moore algebras denoted by $\mathcal{EM}(T)$. For any object $X$ the map $\mu_{X}:TTX\to TX$ is an Eilenberg-Moore algebra over $X$. Moreover, given an Eilenberg-Moore algebra $a:TA\to A$ and a morphism $h:X\to A$ there is a unique morphism $\overline{h}:TX\to A$ which is a homomorphism from $\mu_{X}$ to $a$ satisfying $\overline{h}\circ\eta_{X}=h$. This turns the algebra $\mu_{X}:T^{2}X\to TX$ with $\eta:X\to TX$ into a free Eilenberg-Moore algebra over $X$.

Theorem A.3**.**

Assume $(S,m,e)$ is a monad on $\mathsf{C}$ that lifts to a monad $(\overline{S},\overline{m},\overline{e})$ on the Kleisli category for $(T,\mu,\eta)$ on $\mathsf{C}$ via $\lambda$. This induces a functor $|-|:\mathcal{EM}(\overline{S})\to\mathcal{EM}(S)$ which maps any $\overline{S}$-algebra a:\overline{S}X\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}X=SX\to TX onto

[TABLE]

and any algebra homomorphism h:X\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}Y=X\to TY between the algebras a:\overline{S}X\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}X and b:\overline{S}Y\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}Y onto the map $|h|=TX\stackrel{{\scriptstyle Th}}{{\to}}TTY\stackrel{{\scriptstyle\mu_{Y}}}{{\to}}TY.$

\overline{S}X$$X$$\overline{S}Y$$Y$$h$$a$$b$$\overline{S}h$$\implies$$STX$$TX$$STY$$TY$$\mu_{Y}\circ Th$$\mu_{X}\circ Ta\circ\lambda_{X}$$|b|$$S|h|

Proof A.4**.**

(Theorem A.3) At first we need to show that if a:\overline{S}X\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}X=SX\to TX is an Eilenberg-Moore algebra for $\overline{S}$ then $|a|$ is in $\mathcal{EM}(S)$. This is indeed the case since the following diagrams commute in $\mathsf{C}$:

STX$$TSX$$TX$$TTX$$TX$$\diamond$$\lambda$$e$$Te$$\eta$$Ta$$\mu$$\mathsf{id}

STX$$TSX$$TTX$$TX$$\lambda$$Ta$$\mu$$TTTX$$TTX$$\mu$$\mu$$T\mu$$\diamond$$TTSX$$TSX$$\mu$$T^{2}a$$Ta$$TSSX$$TSTX$$TSa$$T\lambda$$Tm$$SSTX$$STSX$$STTX$$STX$$m$$S\lambda$$STa$$S\mu$$\lambda$$\lambda$$\lambda

The parts denoted by ($\diamond$) commute since a:\overline{S}X\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}X=SX\to TX is in $\mathcal{EM}(\overline{S})$. The proof that $|h|=\mu_{Y}\circ Th$ is a morphism between $|a|$ and $|b|$ in $\mathcal{EM}(S)$ if $h$ is a morphism between $a$ and $b$ in $\mathcal{EM}(\overline{S})$ is straightforward and left to the reader.

A.5 Lawvere theories

Formally, a Lawvere theory, or simply theory, is a category whose objects are natural numbers $n\geq 0$ such that each $n$ is an $n$-fold coproduct of $1$. For any element $i\in n$ let $i_{n}:1\to n$ denote the $i$-th coproduct injection and let the map $[f_{1},\ldots,f_{k}]:n_{1}+\ldots+n_{k}\to n$ be the cotuple of the family $\{f_{l}:n_{l}\to n\}_{l}$. Any morphism $k\to n$ of the form $[i^{1}_{n},\ldots,i^{k}_{n}]:k\to n$ for $i^{j}\in n$ is called base morphism or base map. Finally, let $!:n\to 1$ be defined by $!\triangleq[1_{1},1_{1},\ldots,1_{1}]$. A theory $\mathbb{T}$ is finitary if $\mathbb{T}(m,n)$ is finite for any $n,m\geq 0$.

For any two theories $\mathbb{T}$ and $\mathbb{T}^{\prime}$ a theory morphism $h:\mathbb{T}\to\mathbb{T}^{\prime}$ is an identity-on-objects functor. Let $\mathsf{Law}$ denote the category of theories as objects and theory morphisms as maps.

Any monad $S$ on Set induces a theory $\mathbb{T}_{S}$ associated with it by restricting the Kleisli category $\mathcal{K}\mspace{-1.0mu}l(S)$ to objects $n$ for any $n\geq 0$. Conversely, for any theory $\mathbb{T}$ there is a Set based monad $M_{\mathbb{T}}$ the theory is associated whose theory $\mathbb{T}_{M_{\mathbb{T}}}$ is isomorphic to $\mathbb{T}$ in $\mathsf{Law}$. Hence, without any loss of generality we may assume $M_{\mathbb{T}}$ satisfies $M_{\mathbb{T}}(p)=\mathbb{T}(1,p)$ for any $p\geq 0$. Moreover, the assignments $S\mapsto\mathbb{T}_{S}$ and $\mathbb{T}\mapsto M_{\mathbb{T}}$ extend to functors $\mathsf{Mnd}\to\mathsf{Law}$ and $\mathsf{Law}\to\mathsf{Mnd}$111111Here, $\mathsf{Mnd}$ denotes the category of all monads on Set as objects and monad morphisms as arrows. A natural transformation $h:T\implies T^{\prime}$ is called a monad morphism provided that it preserves unit and multiplication of the monad $T$, \ie$\eta^{\prime}=h\circ\eta$ and $h\circ\mu=\mu^{\prime}\circ hh$. . Any theory morphism $h:\mathbb{T}\to\mathbb{T}^{\prime}$ induces a monad morphism between the associated monads $M_{\mathbb{T}}$ and $M_{\mathbb{T^{\prime}}}$ whose $p$-component equals $h$, \ieit maps any $x\in M_{\mathbb{T}}(p)=\mathbb{T}(1,p)$ to $h(x)\in M_{\mathbb{T^{\prime}}}(p)=\mathbb{T}^{\prime}(1,p)$. Conversely, any monad morphism $h:S\implies S^{\prime}$ gives rise to a theory morphism which maps any $f:k\to Sl\in\mathbb{T}_{S}(k,l)$ to $h_{l}\circ f:k\to S^{\prime}l\in\mathbb{T}_{S^{\prime}}(k,l)$ Since, in general, it is not the case that $M_{\mathbb{T}_{S}}$ is isomorphic to $S$ in $\mathsf{Mnd}$121212 The monad $M_{\mathbb{T}_{S}}$ is isomorphic to $S$ whenever $S$ is finitary, \iewhen for any $x\in TX$ there exists a finite subset $X_{0}\subseteq X$ such that $x\in TX_{0}$. this pair of functors does not form an equilvalence of the categories $\mathsf{Law}$ and $\mathsf{Mnd}$. See \eg[24] for details.

Example A.5**.**

Consider the theory associated with the LTS monad $\mathcal{P}(\Sigma^{\ast}\times\mathcal{I}d):\textnormal{{Set}}\to\textnormal{{Set}}$ from Example 2.1. For any $i\in n$ the morphism $i_{n}:1\to\mathcal{P}(\Sigma^{\ast}\times n)$ in $\mathbb{T}_{\mathcal{P}(\Sigma^{\ast}\times\mathcal{I}d)}$ is given by $i_{n}(1)=\{(\varepsilon,i)\}$ and $!:n\to\mathcal{P}(\Sigma^{\ast}\times 1);i\mapsto\{(\varepsilon,1)\}$. If $\mathbb{T}=\mathbb{T}_{S}$ is a theory associated with a Set-based monad $(S,m,e)$ then $i_{n}:1\to n$ and $!:n\to 1$ in $\mathbb{T}_{S}$ are Set-based maps $i_{n}:1\to Sn;1\mapsto e_{n}(i)$ and $!:n\to S1;i\mapsto e_{1}(1)$. In general, all base morphisms in $\mathbb{T}_{S}$ are of the form $k\stackrel{{\scriptstyle f}}{{\to}}n\stackrel{{\scriptstyle e_{n}}}{{\to}}Sn$ for a Set-map $f$.

Models of Lawvere theory

A model of a theory $\mathbb{T}$ is any product preserving functor $A:\mathbb{T}^{op}\to\textnormal{{Set}}$. The category of models of $\mathbb{T}$ as objects and natural transformations between them as morphisms forms the category $\mathsf{Mod}\mathbb{T}$ of models of $\mathbb{T}$. This category is known to be equivalent to $\mathcal{EM}(M_{\mathbb{T}})$ [24].

Appendix B Omitted proofs

Proof B.1**.**

(Theorem 4.3) Assume $h$ is an algebra homomorphism from $m_{X}$ to $b$. Then we have:

SX$$S^{2}X$$SX$$SY$$Y$$Se$$\mathsf{id}$$h$$m$$b$$Sh$${\implies}$$SX$$S^{2}X$$SX$$SY$$Y$$Se_{-}$$\mathsf{id}$$h_{-}$$m_{-}$$b_{-}$$Sh_{-}

A simple diagram chase gives us:

[TABLE]

Conversely, take $f:Y\to X$ and consider $h:SX\to Y=SX\stackrel{{\scriptstyle Sf_{-}}}{{\to}}SY\stackrel{{\scriptstyle b}}{{\to}}Y$. It is easy to prove that $h$ is an algebra homomorphism from $m_{X}$ to $b$. Moreover, $h_{-}=Sf\circ b_{-}$. This completes the proof.

Proof B.2**.**

(Proposition 4.4) Consider any EM-algebra $a:F^{\ast}X\to X$. Then the map $\underline{a}=a\circ\nu:FX\to X$ satisfies $\nu\circ\underline{a}_{-}=\nu\circ\nu_{-}\circ a_{-}\leq a_{-}$ and, hence, we have:

[TABLE]

By our assumptions the map $(\nu\circ\underline{a}_{-})^{\ast}_{-}:F^{\ast}X\to X$ is an Eilenberg-Moore algebra for the monad $F^{\ast}$. Since by our assumptions $a:F^{\ast}X\to X$ was the least EM-algebra greater than $\underline{a}\circ\nu_{-}=a\circ\nu\circ\nu_{-}$ we have $(\nu\circ a_{-})^{\ast}_{-}=a_{-}$. This completes the proof.

Proof B.3**.**

(Theorem 4.8) Let us first prove the following lemma:

Lemma B.4**.**

Let r_{1},\ldots,r_{p}:1\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{S}q=1\to TSq be regular morphisms. Then the map [r_{1},\ldots,r_{p}]\colon p\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{S}q is of the form [r_{1},\ldots,r_{p}]=p\stackrel{{\scriptstyle\psi}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}m\stackrel{{\scriptstyle\alpha}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}\overline{S}m\stackrel{{\scriptstyle\overline{S}\chi}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}\overline{S}q for $\alpha\in\mathcal{SAT}(\overline{S})$ and $\mathcal{K}\mspace{-1.0mu}l(T)$ map $\chi$ and a base morphism $\psi$ for $T$.

Proof B.5**.**

(Lemma B.4) We take r_{i}=1\stackrel{{\scriptstyle\psi_{i}}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}n_{i}\stackrel{{\scriptstyle\alpha_{i}}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}\overline{S}n_{i}\stackrel{{\scriptstyle\overline{S}\chi_{i}}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}\overline{S}q, where $\alpha_{i}\in\mathcal{SAT}(\overline{S})$ for $i=1,\ldots,p$ and $\psi_{i}$ is a base morphism for $T$ and we show that there is $\alpha\in\mathcal{SAT}(\overline{S})$ such that [r_{1},\ldots,r_{p}]\stackrel{{\scriptstyle\diamond}}{{=}}p\stackrel{{\scriptstyle\psi}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}m\stackrel{{\scriptstyle\alpha}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}\overline{S}m\stackrel{{\scriptstyle\overline{S}\chi}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}\overline{S}q. Define $m=n_{1}+\ldots+n_{p}$ and put $\alpha:m\to\overline{S}m$ to be given by

[TABLE]

By assumption (II) $\alpha$ is a member of $\mathcal{SAT}(\overline{S})$. Moreover, take $\psi=[\psi_{1},\ldots,\psi_{p}]$ and $\chi=[\chi_{1},\ldots,\chi_{p}]$. Then $\chi$ is in $\mathcal{K}\mspace{-1.0mu}l(T)$, $\psi$ is a base morphism and the equality ($\diamond$) holds.

Note that by (I) the identity maps in $\mathbb{T}_{TS}$, i.e. \overline{e}_{n}:n\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{S}n=n\to TSn are regular. Moreover, by Lemma B.4 regular maps are closed under coptupling. Finally, if two maps r_{1}:n\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{S}k and r_{2}:k\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{S}q are regular then their composition in $\mathcal{K}\mspace{-1.0mu}l(\overline{S})=\mathcal{K}\mspace{-1.0mu}l(TS)$ is given by

[TABLE]

and is regular by (III). This completes the proof of Theorem 4.8.

Proof B.6**.**

(Theorem 4.11) In the first part of the proof we show that if a map L:1\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{S}p=1\to\mathcal{P}Sp\in\mathbb{T}_{\mathcal{P}S}(1,p) is regular then set $\{f:1\to Sp\in\mathbb{T}_{S}(1,p)\mid f(1)\subseteq L(1)\}$ is recognizable. We present a construction of a theory morphism $\mathbb{T}_{S}\to\mathbb{T}^{\prime}$ which recognizes a given regular map (REG). We have:

[TABLE]

where $|\mathsf{Alg}(\alpha)|\triangleq S\mathcal{P}n\stackrel{{\scriptstyle\lambda}}{{\to}}\mathcal{P}Sn\stackrel{{\scriptstyle\mathcal{P}\mathsf{Alg}(\alpha)}}{{\to}}\mathcal{P}\mathcal{P}n\stackrel{{\scriptstyle\bigcup}}{{\to}}\mathcal{P}n$. By Theorem A.3 the algebra $|\mathsf{Alg}(\alpha)|$ is, indeed, an Eilenberg-Moore algebra for the monad $S$ on Set. By Subsection A.5 any algebra in $\mathcal{EM}(S)$ induces a model in $\mathsf{Mod}\mathbb{T}_{S}$. So, we continue:

[TABLE]

The explicit recipe for the model $A$ is as follows.

k\to\mathcal{P}n$$k$$A$$f_{A}:(l\to\mathcal{P}n)\to(k\to\mathcal{P}n)$$f:k\to Sl\in\mathbb{T}_{S}(k,l)$$A*where *k\stackrel{{\scriptstyle f}}{{\to}}Sl\stackrel{{\scriptstyle Sx}}{{\to}}S\mathcal{P}n\stackrel{{\scriptstyle|\mathsf{Alg}(\alpha)|}}{{\to}}\mathcal{P}n$$x:l\to\mathcal{P}n$$f_{A}

Now consider the variety $\mathsf{V}(A)$ generated by $A$ which consists of all models of $\mathbb{T}_{S}$ obtained from $A$ by applying three types of operators: $\mathsf{H},\mathsf{S}$ and $\mathsf{P}$. We know that $\mathsf{V}(A)=\mathsf{HSP}(A)$. The category $\mathsf{V}(A)$ admits all free objects $F_{A}(X):\mathbb{T}_{S}^{op}\to\textnormal{{Set}}$ (\eg[13]) with their explicit description left as an exercise for the reader in \eg[13, Exercise 11.5]. Whenever $X=m$ these algebras are described explicitly by:

\{g_{A}:(m\to\mathcal{P}n)\to(k\to\mathcal{P}n)\mid g:k\to Sm\in\mathbb{T}_{S}(k,m)\}$$k$$F_{A}(m)$$F_{A}(m)(l)\to F_{A}(m)(k);g_{A}\mapsto(g\diamond f)_{A}\stackrel{{\scriptstyle\dagger}}{{=}}f_{A}\circ g_{A}$$f:k\to Sl\in\mathbb{T}_{S}(k,l)$$F_{A}(m)

where in the above, $\diamond$ denotes the composition in $\mathbb{T}_{S}$ and the identity marked with $\dagger$ follows by a simple diagram chase and is proven in Theorem B.7. The free algebra functor $F_{A}(-):\textnormal{{Set}}\to\mathsf{V}(A)$ induces a Set-monad which induces a theory. This theory is explicitly described in the following statement.

Theorem B.7**.**

Let $\mathbb{T}_{F_{A}}$ be the category whose objects are $n$ for $n\geq 0$ and morphisms from $k$ to $l$ are $\mathbb{T}_{F_{A}}(k,l)=F_{A}(l)(k)$ with the composition of the morphisms $(h_{1})_{A}\in\mathbb{T}_{F_{A}}(k,l)$ and $(h_{2})_{A}\in\mathbb{T}_{F_{A}}(l,m)$ given by

[TABLE]

Then $\mathbb{T}_{F_{A}}$ is a well defined Lawvere theory.

Proof B.8**.**

At first we will prove that

[TABLE]

For $x:m\to\mathcal{P}n$ the image $(h_{2}\diamond h_{1})_{A}(x)$ equals

[TABLE]

The desired equality follows by commutativity of the diagram below.

k$$Sl$$S^{2}m$$Sm$$S\mathcal{P}n$$\mathcal{P}n$$S^{2}\mathcal{P}n$$S\mathcal{P}n$$h_{1}$$S(|\mathsf{Alg}|\circ Sx\circ h_{2})$$Sh_{2}$$m$$m$$Sx$$S^{2}x$$|\mathsf{Alg}(\alpha)|$$|\mathsf{Alg}(\alpha)|$$S|\mathsf{Alg}(\alpha)|

This proves that $\mathbb{T}_{F_{A}}$ is a well-defined category. A simple verification leads to a conclusion that it admits coproducts and that $n=1+\ldots+1$ for any object $n$. Hence, $\mathbb{T}_{F_{A}}$ is a theory.

Now let us get back to the proof of Theorem 4.11. Note that $\mathbb{T}_{F_{A}}$is a finitary theory which comes with a theory morphism $h:\mathbb{T}_{S}\to\mathbb{T}_{F_{A}}$ mapping $n$ to $n$ and

[TABLE]

Recall that $\chi:n\to\mathcal{P}p$, consider $\chi_{-}:p\to\mathcal{P}n$ and take the set

[TABLE]

defined by $T_{\chi}=\{g_{A}\mid g_{A}(\chi_{-})=i_{n}\},$ where $i_{n}:1\to\mathcal{P}n$ maps the unique element of $1$ onto $\{i\}$ and is the lifting of the Set-map $1\to n;1\mapsto i$ to $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$. For $f:1\to Sp\in\mathbb{T}_{S}(1,p)$ we then have the following chain of equivalences: $f\in h^{-1}(T_{\chi})$ iff $f_{A}(\chi_{-})=i_{n}$ iff

[TABLE]

In the above $\bullet$ denotes the composition in $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$. This completes the first part of the proof of Theorem 4.11.

Now, in order to see the converse assume there is a finitary theory $\mathbb{T}^{\prime}$ and a theory morphism $h:\mathbb{T}_{S}\to\mathbb{T}^{\prime}$. Consider a set $T\subseteq\mathbb{T}^{\prime}(1,p)$. Our aim is to represent $h^{-1}(T)$ in terms of an expression of the form (REG). As mentioned in Subsection A.5, without loss of generality, we may assume that $M_{\mathbb{T}_{S}}p=\mathbb{T}_{S}(1,p)$ and $M_{\mathbb{T^{\prime}}}p=\mathbb{T}^{\prime}(1,p)$. Since $S$ was taken to be finitary, the monad $M_{\mathbb{T}_{S}}$ is isomorphic to $S$ in $\mathsf{Mnd}$. Hence, in what follows we will slightly abuse the notation and denote the multiplication and unit of $M_{\mathbb{T}_{S}}$ by $m$ and $e$ respectively.

The theory morphism $h:\mathbb{T}_{S}\to\mathbb{T}^{\prime}$ induces a monad morphism, which will be denoted by

[TABLE]

Following Subsection A.5, the $p$-component of the morphism $\overline{h}$ is $h_{p}:M_{\mathbb{T}_{S}}p=\mathbb{T}_{S}(1,p)\to M_{\mathbb{T}^{\prime}}p=\mathbb{T}^{\prime}(1,p);f\mapsto h(f)$. Consider the $p$-component of the multiplication $m^{\prime}$ of $M_{\mathbb{T^{\prime}}}$ and note that the $M_{\mathbb{T}_{S}}$-algebra

[TABLE]

is, in fact, a member of $\mathcal{EM}(M_{\mathbb{T}})$. This follows by the properties of the monad morphism $\overline{h}$ and a simple diagram chase. By the same properties we have the following:

M_{\mathbb{T}_{S}}M_{\mathbb{T}_{S}}p=M_{\mathbb{T}_{S}}\mathbb{T}_{S}(1,p)$$M_{\mathbb{T}_{S}}p=\mathbb{T}_{S}(1,p)$$M_{\mathbb{T}_{S}}M_{\mathbb{T}^{\prime}}p=M_{\mathbb{T}_{S}}\mathbb{T}^{\prime}(1,p)$$M_{\mathbb{T}^{\prime}}M_{\mathbb{T}^{\prime}}p=M_{\mathbb{T}^{\prime}}\mathbb{T}^{\prime}(1,p)$$M_{\mathbb{T}^{\prime}}p=\mathbb{T}^{\prime}(1,p)$$M_{\mathbb{T}_{S}}h$$h$$m$$\overline{h}$$m^{\prime}

Consider the lifting $a^{\sharp}\triangleq\{-\}\circ a:M_{\mathbb{T}_{S}}\mathbb{T}^{\prime}(1,p)\to\mathcal{P}\mathbb{T}^{\prime}(1,p)$ of $a$ to $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$. The map $a^{\sharp}$ is an $\overline{M_{\mathbb{T}_{S}}}$-algebra which is a member of $\mathcal{EM}(\overline{M_{\mathbb{T}_{S}}})$. By the diagram above we have:

[TABLE]

Theorem 4.3 implies: $h^{\sharp}_{-}=\overline{M_{\mathbb{T}}}(e^{\sharp}_{-}\bullet h^{\sharp}_{-})\bullet\mathsf{CoAlg}(a^{\sharp})$. Hence, for any $t\in T\subseteq\mathbb{T}^{\prime}(1,p)$ we have

[TABLE]

where $t_{\mathbb{T}^{\prime}}:1\to\mathbb{T}^{\prime}(1,p)$ maps the unique element of $1$ to $t\in\mathbb{T}^{\prime}(1,p)$. This exactly shows that the map $1\to\mathcal{P}Sp$ which assigns to the unique element of $1$ the set $h^{-1}(t)\subseteq 1\to Sp$ is regular. Now, since $T$ is finite we have $h^{-1}(T)=h^{-1}(t_{1})\cup\ldots h^{-1}(t_{n})$ for $T=\{t_{1},\ldots,t_{n}\}$. Hence, by the assumption (I) and (III) we get that maps of the form 1\stackrel{{\scriptstyle\psi}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}n\stackrel{{\scriptstyle\alpha}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}\overline{S}n\stackrel{{\scriptstyle\overline{S}\chi}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}\overline{S}p are regular for any $\psi,\chi$ in $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P})$ and $\alpha\in\mathcal{SAT}(\overline{S})$. This precisely means that regular maps are closed under finite unions. Therefore, we get the desired conclusion. This ends the proof of Theorem 4.11.

Appendix C Examples

In this appendix we illustrate the generality of the results presented by listing some representative examples of models fitting our framework besides our running example of non-deterministic automata and regular languages.

C.1 Tree automata and their languages

Here, we focus on non-deterministic tree automaton, \iea tuple $(Q,\Sigma,\delta,\mathcal{F})$, where $\delta:Q\times\Sigma\to\mathcal{P}(Q\times Q)$ and the rest is as in the case of standard non-deterministic automata (\eg[34]).

Trees

Formally, a binary tree or simply tree with nodes in $A$ is a function $t:P\to A$, where $P$ is a non-empty prefix closed subset of $\{l,r\}^{\ast}$. The set $P\subseteq\{l,r\}^{\ast}$ is called the domain of $t$ and is denoted by $\mathsf{dom}(t)\triangleq P$. Elements of $P$ are called nodes. For a node $w\in P$ any node of the form $wx$ for $x\in\{l,r\}$ is called a child of $w$. A tree is called complete if all nodes have either two children or no children. A height of a tree $t$ is $\max\{|w|\mid w\in\mathsf{dom}(t)\}$. A tree $t$ is finite if it is of a finite height. The frontier of a tree $t$ is $\mathsf{fr}(t)\triangleq\{x\in\mathsf{dom}(t)\mid x\{l,r\}\cap P=\varnothing\}$. Elements of $\mathsf{fr}(t)$ are called leaves. Nodes from $\mathsf{dom}(t)\setminus\mathsf{fr}(t)$ are called inner nodes. The outer frontier of $t$ is defined by $\mathsf{fr}^{+}(t)\triangleq\mathsf{dom}(t)\{l,r\}\setminus\mathsf{dom}(t)$. \ieit consists of all the words $wi\notin\mathsf{dom}(t)$ such that $w\in\mathsf{dom}(t)$ and $i\in\{l,r\}$. Finally, set $\mathsf{dom}^{+}(t)\triangleq\mathsf{dom}^{+}(t)\cup\mathsf{fr}^{+}(t)$.

Let $T_{\Sigma}X$ denote the set of all finite complete trees $t:P\to\Sigma+X$ with inner nodes taking values in $\Sigma$ and which have leaves from the set $X$. Note that trees from $T_{\Sigma}X$ of height [math] can be thought of as elements of $X$. Hence, we may write $X\subseteq T_{\Sigma}X$.

Languages

Let $\mathcal{Q}=(Q,\Sigma,\delta,\mathcal{F})$ be a tree automaton. A run of the automaton $\mathcal{Q}$ on a finite tree $t\in T_{\Sigma}(1)$ starting at the state $s\in Q$ is a map $\mathfrak{r}:\mathsf{dom}^{+}(t)\to Q$ such that $\mathfrak{r}(\varepsilon)=s$ and for any $x\in\mathsf{dom}(t)\setminus\mathsf{fr}(t)$ we have $(\mathfrak{r}(xl),\mathfrak{r}(xr))\in\delta(\mathfrak{r}(x),t(x)).$ We say that the run $\mathfrak{r}$ is successful if $\mathfrak{r}(w)\in\mathcal{F}$ for any $w\in\mathsf{fr}^{+}(t)$ for the tree $t$. The set of finite trees recognized by a state $s$ in $\mathcal{Q}$ is defined as the set of finite trees $t\in T_{\Sigma}(1)$ for which there is a run in $\mathcal{Q}$ starting at $s$ which is succesful on the tree $t$.

Tree automata and regular behaviours

Let $\mathcal{Q}=(Q,\Sigma,\delta,\mathcal{F})$ be a finite non-deterministic tree automaton. Since $Q$ is finite without any loss of generality we may assume $Q=n$ for some $n\geq 0$. Moreover, in this case, $\delta:Q\times\Sigma\to\mathcal{P}(Q\times Q)$ can be given in terms of

[TABLE]

Hence, any non-deterministic tree automaton can be viewed as a pair $(\alpha:n\to\mathcal{P}(n\times\Sigma\times n),\mathcal{F})$. Since $n\times\Sigma\times n$ is, in fact, the set of binary trees from $T_{\Sigma}$ of height one, the pair becomes $(\alpha:n\to\mathcal{P}T_{\Sigma}n,\mathcal{F})$. By [9], the map L(\alpha,\mathcal{F},i):1\to\mathcal{P}T_{\Sigma}1=1\stackrel{{\scriptstyle i_{n}}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}n\stackrel{{\scriptstyle\alpha^{\ast}}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}\overline{T_{\Sigma}}n\stackrel{{\scriptstyle\overline{T_{\Sigma}}\chi_{\mathcal{F}}}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}\overline{T_{\Sigma}}1, where $\chi_{\mathcal{F}}$ is as in Section 3, satisfies:

[TABLE]

The rest of this section will be devoted to considering an example of a regular tree language which we will characterize in terms of Lawvere theory morphism recognition. This characterisation will be given in more details (compared to the sketch presented in Section 5). We assume the reader is familiar with the proof of Theorem 4.11. Let $\Sigma=\{a,b\}$ and consider a two state automaton whose transition map $\alpha:2\to\mathcal{P}(2\times\Sigma\times 2)$ is defined by $1\mapsto\varnothing,2\mapsto\{(2,a,2),(1,b,1)\}$ and $\mathcal{F}=\{1\}$. It is easy to see that $L(\alpha,\mathcal{F},2)(1)\in\mathcal{P}T_{\Sigma}1$ consists of binary trees of height $>0$ whose nodes preceding the leaf nodes are all $b$ and the remaining non-leaf nodes are $a$. Indeed, the saturated map $\alpha^{\ast}:2\to\mathcal{P}(T_{\Sigma}2)$ satisfies $\alpha^{\ast}(1)=\{1\}$ and $\alpha^{\ast}(2)$ contains the trees: $2$, $(1,b,1)$ and satisfies the following implication: if $t,t^{\prime}\in\alpha^{\ast}(2)$ then $(t,a,t^{\prime})$ is in $\alpha^{\ast}(2)$. The morphism L(\alpha,\mathcal{F},2):1\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{T}_{\Sigma}1=1\to\mathcal{P}T_{\Sigma}1 is exactly as stated above since L(\alpha,\mathcal{F},2)=1\stackrel{{\scriptstyle 2_{2}}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}2\stackrel{{\scriptstyle\alpha^{\ast}}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}\overline{T_{\Sigma}}2\stackrel{{\scriptstyle\overline{T_{\Sigma}}\chi_{\{1\}}}}{{\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}}}\overline{T_{\Sigma}}1.

The map $\mathsf{Alg}(\alpha^{\ast})=\alpha^{\ast}_{-}:T_{\Sigma}2\to\mathcal{P}2$ assigns $1\mapsto\{1\}$, $2\mapsto\{2\}$ and for any $t\in\alpha^{\ast}(2)$, $t\mapsto\{2\}$. The remaining trees from $T_{\Sigma}2$ are assigned to $\varnothing$. This yields a $4$-element algebra $|\mathsf{Alg}(\alpha^{\ast})|:T_{\Sigma}\mathcal{P}2\to\mathcal{P}2$ which takes any tree in $T_{\Sigma}\mathcal{P}2$ with a leaf equal $\varnothing$ to $\varnothing$ and any other tree $T\in T_{\Sigma}\mathcal{P}2$ is mapped onto $T\mapsto\bigcup\{\mathsf{Alg}(\alpha^{\ast})(t)=\alpha^{\ast}_{-}(t)\mid t\ll T\},$ where $t\ll T$ means that $t$ is obtained from $T$ by replacing all subset leaves of $T$ by one of their elements. In particular, $(x,a,\{1\}),(\{1\},a,x),(x,\sigma,\varnothing),(\varnothing,\sigma,x),(\{2\},b,\{2\})\mapsto\varnothing$ for any $x,x^{\prime}\in\mathcal{P}2$, $(x,a,x^{\prime})\mapsto\{2\}$ if $2\in x,x^{\prime}$ and $(x,b,x^{\prime})\mapsto\{1\}$ if $1\in x,x^{\prime}$. Since, $|\mathsf{Alg}(\alpha^{\ast})|$ is an Eilenberg-Moore algebra for $T_{\Sigma}$, all other values are uniquely determined by these.

Now, the carrier of the free algebra $F_{A}(1)$ over $1$, \ie$F_{A}(1)(1)$, is a submonoid of the monoid of maps $(1\to\mathcal{P}2)\to(1\to\mathcal{P}2)$ (or equivalently, of maps $\mathcal{P}2\to\mathcal{P}2$) generated by the assignments: $a_{A}:\mathcal{P}2\to\mathcal{P}2$ and $b_{A}:\mathcal{P}2\to\mathcal{P}2$ defined by $a_{A}(x)=(x,a,x)$ and $b_{A}(x)=(x,b,x)$. It turns out that it has $4$ elements which are given in the following table.

Now, in our case, $T_{\chi}$ consists of maps from the above table that assign to $\{1\}$ the value $\{2\}$, \ie$T_{\chi}=\{b_{A}\}$, and the induced Lawvere theory morphism $\mathbb{T}_{T_{\Sigma}}\to\mathbb{T}_{F_{A}}$ restricted to $\mathbb{T}_{T_{\Sigma}}(1,1)$ maps the tree $1$ to $\mathsf{id}$, any tree $t$ such that after the composition with the tree $(1,b,1)$ in $\mathbb{T}_{T_{\Sigma}}$ the result is in $L(\alpha,\mathcal{F},2)$ to $a_{A}$, any tree from $L(\alpha,\mathcal{F},2)$ onto $b_{A}$ and any other to $b^{2}_{A}$. We see that it is a monoid homomorphism131313Note that the composition in $\mathbb{T}_{F_{A}}(1,1)$ is defined to be the composition of $F_{A}(1)(1)$ in the reversed order. (conf. Theorem B.7). and that $L(\alpha,\mathcal{F},2)=h^{-1}(\{b_{A}\})$.

C.2 Weighted automata and their languages

Generalised countable multisets

A semiring $(\mathcal{S},+,0,\cdot,1)$ is said to be positively ordered whenever it can be equipped with a partial order $(\mathcal{S},\leq)$ such that the unit [math] is the bottom element of this ordering and semiring operations are monotonic in both components \ie$x\leq y$ implies $x\mathrel{\diamond}z\leq y\mathrel{\diamond}z$ and $z\mathrel{\diamond}x\leq z\mathrel{\diamond}y$ for $\diamond\in\{+,\cdot\}$ and $x,y,z\in\mathcal{S}$. A semiring is positively ordered if and only if it is zerosumfree \ie$x+y=0$ implies $x=y=0$; the natural order $x\lhd y\iff\exists z.x+z=y$ is the weakest one rendering $\mathcal{S}$ positively ordered.

A positively ordered semiring is said to be $\omega$-complete if it has countable sums given as $\sum_{i\leq\omega}x_{i}=\sup\{\sum_{j\in J}x_{j}\mid J\subset\omega\}$. It is called $\omega$-continuous if suprema of ascending $\omega$-chains exist and are preserved by both operations \ie: $y\mathrel{\diamond}\bigvee_{i}x_{i}=\bigvee_{i}y\mathrel{\diamond}x_{i}$ and $\bigvee_{i}x_{i}\mathrel{\diamond}z=\bigvee_{i}x_{i}\mathrel{\diamond}z$ for $\diamond\in\{+,\cdot\}$ and $x,y,z\in\mathcal{S}$. Examples of such semirings are: the boolean semiring, the arithmetic semiring of non-negative real numbers with infinity and the tropical semiring.

Henceforth we assume $(\mathcal{S},+,0,\cdot,1,\leq)$ to be a positive, $\omega$-complete, $\omega$-continuous semiring.

A countable $\mathcal{S}$-multiset is a pair $(X,\phi)$ where $X$ is a set and $\phi\colon X\to\mathcal{S}$ is a function such that the set $\operatorname*{\rm{supp}}(\phi)=\{x\mid\phi(x)>0\}$ (called support) is countable. We will abuse the notation and simply write $\phi$ for the multiset $(X,\phi)$. We often write $\mathcal{S}$-multiset as formal sums \iesums of expressions of form $s\bullet x$ where $x$ is an element and $s$ its membership degree.

The $\mathcal{S}$-multiset functor $\mathcal{M_{S}}\colon\textnormal{{Set}}\to\textnormal{{Set}}$ assigns to every set $X$ the set $\mathcal{M_{S}}X$ of $\mathcal{S}$-multisets with universe $X$, and to every function $f\colon X\to Y$ the function mapping each $(X,\phi)$ to $(X,\sum_{x\in\operatorname*{\rm{supp}}(\phi)}\phi(x)\bullet f(x))$. This functor carries a monad structure $(\mathcal{M_{S}},\mu,\eta)$ whose multiplication $\mu$ and unit $\eta$ are given on each set $X$ by the mappings:

[TABLE]

The probability distribution monad $\mathcal{D}$ is a submonad of $\mathcal{M}_{[0,\infty]}$ [10].

Weighted languages and automata

Fix an alphabet $\Sigma$ and a semiring $\mathcal{S}$. A weighted language (of finte words) is an $\mathcal{S}$-multiset with universe $\Sigma^{\star}$ and a weighted automaton $\mathcal{A}$ is (up to minor notational changes to the classical presentation [37, 5]) is a tuple $(m,\alpha,\chi)$ where $n$ is the set of states, $\alpha\colon n\to\mathcal{M_{S}}(\Sigma\times n)$ is the transition function (\iea ternary $\mathcal{S}$-relation on $n\times\Sigma\times n$) and $(n,\chi\colon n\to\mathcal{S}$) is the multiset of final states. Given a weighted automaton $\mathcal{A}=(n,\alpha,\chi)$, the language accepted by a state $i$ of $\mathcal{A}$ is the multiset $L(\mathcal{A},i)$ with universe $\Sigma^{\ast}$ and membership function:

[TABLE]

Weighted automata and duality

The multiset monad $\mathcal{M_{S}}$ and its Kleisli category do not meet conditions $(A)-(C)$ because of the cardinality constraint on multisets (which is ultimately due to $\mathcal{S}$ not admitting sums of arbitrary cardinality). There are two workarounds to this problem: one is to extend the definition of $\mathcal{M_{S}}$ to cover functions of arbitrary supports, the other is to realize that when dealing with regular behaviours as in (REG) we actually focus on systems over a finite state space. Hence, we restrict w.l.o.g. to the subcategory identified by finite sets. In this settings, the functor $(-)_{-}$ is readily defined by “swapping columns and rows” (maps in $\mathcal{K}\mspace{-1.0mu}l(\mathcal{M_{S}})$ can be regarded as $\mathcal{S}$):

[TABLE]

If $f$ is in the image of Set then the grade of each $f(x)$ is $1$. It follows that $f\circ f_{-}\leq\mathsf{id}$ and $f_{-}\circ f\geq\mathsf{id}$.

The free monad $\Sigma^{\ast}$ lifts to a monad $\overline{\Sigma^{\ast}}$ on $\mathcal{K}\mspace{-1.0mu}l(\mathcal{M_{S}})$ by the unique extension of the distributive law of the functor $\Sigma\times\mathcal{I}d$ over the monad $\mathcal{M_{S}}$ given by the assignment $\Sigma\times(X,\phi)\mapsto(\Sigma\times X,\sum\phi(x)\bullet(\sigma,x))$ [10]. In this case, if $\Sigma^{\ast}$ is countable then any Eilenberg-Moore algebra a\colon\overline{\Sigma^{\ast}}n\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}n=\Sigma^{\ast}\times n\to\mathcal{M_{S}}n on $\mathcal{K}\mspace{-1.0mu}l(\mathcal{M_{S}})$ yields a saturated system a_{-}\colon n\makebox[1.1pt][l]{\longrightarrow\makebox{\mkern-24.0mu\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\bullet}\mkern 12.0mu}\makebox{$\mkern-21.0mu\circ\mkern 10.0mu$}}\overline{\Sigma^{\ast}}n=n\to\mathcal{M_{S}}({\Sigma^{\ast}\times n}) by simple currying and uncurrying. Since $\overline{\Sigma^{\ast}}$ is the free monad over $\overline{\Sigma}$ on $\mathcal{K}\mspace{-1.0mu}l(\mathcal{M_{S}})$ [8], the Eilenberg-Moore algebra $a$ is uniquely determined by $\underline{a}\colon\Sigma\times n\to\mathcal{M_{S}}n$ (conf Subsec. 4.1). Hence, so is its dual $a_{-}$.

C.3 Fuzzy automata and their languages

Quantales and fuzzy sets

Let $(\mathcal{Q},\cdot,1,\leq)$ be a unital quantale, \ie. a relational structure with the property that:

• •

$(\mathcal{Q},\cdot,1)$ is a monoid,

• •

$(\mathcal{Q},\leq)$ is a complete lattice,

• •

arbitrary suprema are preserved by the monoid multiplication.

In other words, a unital quantale is a monoid in the category Sup of join-preserving homomorphisms between complete join semi-lattices. In the sequel we will often write $\perp_{\mathcal{Q}}$ or simply $\perp$ for the supremum of the empty set and denote a quantale $(\mathcal{Q},\cdot,1,\leq)$ by its carrier set $\mathcal{Q}$, provided the associated structure is clear from the context. Examples are given by booleans $(\{\bot,\top\},\land,\top,\implies)$, the real unit interval $([0,1],\cdot,1,\leq)$. More generally, for a monoid $(M,\odot,e)$ equipped with an order $\leq$ that is preserved by $\cdot$, the set $\mathcal{P}_{\downarrow}M$ of downward closed subsets of $M$ carries a unital quantale structure $(\mathcal{P}_{\downarrow}M,\cdot,1,\subseteq)$ where $1$ is the downward cone with cusp $e$:

[TABLE]

and $\cdot$ is the downward closure of the pointwise extension of $\odot$ to subsets of $M$:

[TABLE]

A $\mathcal{Q}$-fuzzy set is a pair $(X,\phi)$ where $X$ is a set (called universe of discourse and often left implicit) and $\phi\colon X\to\mathcal{Q}$ is a a membership function. The value $\phi(x)$ is called grade of membership of $x$. Taking the boolean quantale as $\mathcal{Q}$ yields ordinary sets and taking the real unit interval interval yields fuzzy sets in the classical sense.

The $\mathcal{Q}$-fuzzy powerset functor $\mathcal{P_{Q}}\colon\textnormal{{Set}}\to\textnormal{{Set}}$ assigns to every set $X$ the set $\mathcal{P_{Q}}X=(X\to\mathcal{Q})$ of all fuzzy sets with universe $X$, and to every function $f\colon X\to Y$ the function mapping each $(X,\phi)$ to $(Y,\lambda y.\bigvee_{x:f(x)=y}\phi(x))$. This functor carries a monad structure $(\mathcal{P_{Q}},\bigcup_{\mathcal{Q}},\{-\}_{\mathcal{Q}})$ when equipped with flattening and embedding into singletons. In particualr, the components of monadic multiplications and unit at $X$ are given by the assignments:

[TABLE]

The powerset monad $\mathcal{P}$ is a special case of the above where $\mathcal{Q}$ is the boolean quantale.

Fuzzy languages and automata

Fix an alphabet $\Sigma$ and a quantale $\mathcal{Q}$. A fuzzy language of (finite words) is a $\mathcal{Q}$-fuzzy set with universe $\Sigma^{\ast}$ and a fuzzy automaton (on finite words over $\Sigma$) is (up to minor notational changes to the classical presentation [31, 15]) a tuple $\mathcal{A}=(n,\alpha,\chi)$ where $n$ is the state space, $\alpha\colon n\to\mathcal{P_{Q}}(\Sigma\times n)$ is the transition function (\iea fuzzy ternary relation on $n\times\Sigma,\times n$), and $(n,\chi\colon n\to\mathcal{Q})$ is the fuzzy set of final states. Given a fuzzy automaton $\mathcal{A}=(n,\alpha,\chi)$, the language accepted by a state $i$ of $\mathcal{A}$ is the fuzzy set $L(\mathcal{A},i)$ with universe $\Sigma^{\ast}$ and membership function:

[TABLE]

Fuzzy automata and duality

The fuzzy powerset monad and its Kleisli category meet conditions $(A)-(C)$ from Section 4 when Set is taken as J. This follows by the simple observation that the Kleisli category of $\mathcal{P_{Q}}$ is isomorphic to the category $\textnormal{{Mat}}-\mathcal{Q}$ of $\mathcal{Q}$-valued matrices. The functor $(-)_{-}$ is readily defined by “swapping columns and rows”:

[TABLE]

If $f$ is in the image of Set then the grade of each $f(x)$ is $1$. It follows that $f\circ f_{-}\leq\mathsf{id}$ and $f_{-}\circ f\geq\mathsf{id}$.

The free monad $\Sigma^{\ast}$ lifts to a monad $\overline{\Sigma^{\ast}}$ on $\mathcal{K}\mspace{-1.0mu}l(\mathcal{P_{Q}})$ by the unique extension of the distributive law of the functor $\Sigma\times\mathcal{I}d$ over the monad $\mathcal{P_{Q}}$ given by the assignment $(\Sigma\times(X,\phi))\mapsto(\Sigma\times X,\lambda(\sigma,x).\phi(x))$. The monad $\overline{\Sigma^{\ast}}$ meets condition $(D)$ from Section 4 [12]. In particular, saturation is defined on every $\alpha$ as $\alpha^{\ast}(x)(y)=\bigvee_{k<\omega}\alpha^{k}$ (where $\alpha^{0}=\mathsf{id}$ and $\alpha^{k+1}=\alpha\circ\alpha^{k}$). It follows from Proposition 4.4 that every Eilenberg-Moore algebra for $\overline{\Sigma^{\ast}}$ is dual to the saturations of morphism of the form $X\to\mathcal{P_{Q}}(\Sigma\times X)\hookrightarrow\mathcal{P_{Q}}(\Sigma^{\ast}\times X)$ and it follows by construction of $\overline{\Sigma^{\ast}}$ that any $\alpha\in\mathcal{SAT}(\overline{\Sigma^{\ast}})$ h map is determined is equivalently defined as a map $\hat{\alpha}\colon n\to\mathcal{P_{Q}}(\Sigma\times n)$ \iethe transition map of a fuzzy automaton. As a consequence, the language $L(\mathcal{A},i)$ accepted by a state $i$ of a fuzzy automaton $\mathcal{A}=(n,\alpha,\chi)$ is given by the regular map:

[TABLE]

where $\nu$ is the canonical embedding of $\mathcal{P_{Q}}(\Sigma\times\mathcal{I}d)$ into $\mathcal{P_{Q}}(\Sigma^{\ast}\times\mathcal{I}d)$.