University of Warsaw,
Polandrafal.stefanski@mimuw.edu.plhttps://orcid.org/0000-0002-8439-4056 Rafał
Stefański [500]Theory of computation Transducers John Q. Open and Joan R.
Access 2 42nd Conference on Very Important Topics (CVIT 2016) CVIT 2016 CVIT
2016 December 24–27, 2016 Little Whinging, United Kingdom 42 23

# Monads, Comonads, and Transducers

Rafał Stefański

###### Abstract

This paper proposes a definition of _recognizable transducers over monads and
comonads_ , which bridges two important ongoing efforts in the current
research on regularity. The first effort is the study of regular
transductions, which extends the notion of regularity from languages into
word-to-word functions. The other important effort is generalizing the notion
of regular languages from words to arbitrary monads, introduced in [2] and
further developed in [3, 6]. In the paper, we present a number of examples of
transducer classes that fit the proposed framework. In particular we show that
our class generalizes the classes of Mealy machines and rational
transductions. We also present examples of recognizable transducers for
infinite words and a specific type of trees called terms. The main result of
this paper is a theorem, which states the class of recognizable transductions
is closed under composition, subject to some _coherence_ axioms between the
structure of a monad and the structure of a comonad. Due to its complexity, we
formalize the proof of the theorem in _Coq Proof Assistant_ [26]. In the
proof, we introduce the concepts of a _context_ and a _generalized wreath
product_ for Eilenberg-Moore algebras, which could be valuable tools for
studying these algebras.

###### keywords:

Monad, Comonad, Transdcuer, Algebra, Composition, Wreath Product, Regular
Languages, Regular Transductions, Mealy Machines, Rational Transductions

###### category:

##  1 Introduction

The study of transductions plays an important role in studying and
understanding the theory of regularity. Although this idea is not new, and its
importance has been known for decades (see the first paragraph of [25, Section
V]), it seems to have been gaining momentum in the recent years (e.g. see [10,
12, 14, 11]). This paper aims to extend the concept of _languages recognized
over monads_ , introduced by [2], to transductions. Interestingly, this
requires studying functors that are simultaneously equipped with the
structures of both a monad and a comonad.

Although, this work is clearly inspired by category theory, our primary focus
lies within the domain of formal languages and transducers. For this reason,
we do not assume any prior knowledge of category theory on the part of the
reader. We will provide all necessary definitions and limit our discussion to
the basic category Set, which consists of sets and functions between them. For
a discussion about extending this work to other categories, see Section D.1.

The paper is structured as follows: In Section 2, we summarize the results on
_languages recognizable over monads_ (based on [2, 3, 6]), which serves as a
context for this paper. In Section 3, we introduce _transductions recognizable
over monads and comonads_ , which is the main contribution of this paper. In
Section 4, we show that our proposed classes of transducers are closed under
compositions, subject to certain _coherence axioms_. This serves two purposes:
First, it serves as a validation for our class of transductions. Second, it
facilitates a deeper understanding of the structure of the monad/comonad
functors and their Eilenberg-Moore algebras. Finally, in Section 5, we outline
the potential directions for further work.

Let us also mention that some of the proofs (including the proof of the
compositions theorem) are verified in the _Coq Proof Assistant_ [26] (see
Appendix E).

#### Related work

A recently published work [7] also presents a categorical framework for
defining transductions over monads. Our paper differs from [7] in two
important ways: First, [7] focuses on generalizing the class of regular
functions (i.e. those recognized by two-way transducers), whereas this paper
concentrates on generalizations of Mealy machines and rational functions (see
also Item 1 in Section 5). Second, the two papers present different approaches
to the problem. In particular, our paper develops a comonadic framework that
does not appear in [7]. We believe that both the approaches are valuable and
warrant further investigation. Future research could explore potential
connections and synergies between the two methodologies.

##  2 Monads and recognizable languages

In this section we present a brief summary of the existing research on
_recognizable languages over monads_ , which is the starting point for this
paper. This line of research was initiated in [2], and then continued in [3]
and in [6]. The main idea is to approach regular languages from the algebraic
perspective, and then use Eilenberg-Moore algebras to generalize their
definition from languages over words to languages over arbitrary monads (such
as infinite words, trees, or even graphs). We start the summary with the
following, well-established definition of monoid recognizability:

######  Definition 2.1.

A monoid is a set equipped with a transitive binary operation and an identity
element. We say that a language $L\subseteq\Sigma^{*}$ is _recognizable by a
monoid_ if there exist:

$\underbrace{M}_{\textrm{Monoid}}$ | $\underbrace{h:\Sigma\to M}_{\textrm{Input function}}$ |  $\underbrace{F\subseteq M}_{\textrm{Accepting set}}$,
---|---|---

such that a word $w_{1}\ldots w_{n}\in\Sigma^{*}$ belongs to $L$, if and only
if:

$h(w_{1})\cdot h(w_{2})\cdot\ldots\cdot h(w_{n})\in F$

It is a well-know fact, that the class of languages that can be recognized by
_finite_ monoids is equal to regular languages (see [23, Theorem 3.21] for
details).

As mentioned before, the key idea presented by [2] is extending Definition 2.1
from languages of words, to languages of arbitrary monads. Before we show how
to do this, we need to define _monads_. However, since monads are a special
kind of functors, we need to start by giving a definition of a _functor_ 111We
only define a special case endofunctors in Set, as those are the only type of
functors that we are going to use. See [1, Definition 41] for a general
definition.:

######  Definition 2.2.

A _functor_ $M$ consists two parts. The first part is a mapping from sets to
sets, i.e. for every set $X$, the functor $M$ assigns another set denoted as
$MX$. The other part is a mapping from functions to functions, i.e. for every
function $f:X\to Y$, the functor $M$ assigns a function $Mf:MX\to MY$.
Moreover, the function mapping needs to satisfy the following axioms (where
$\textrm{id}_{X}$ is the identity function on $X$, and $\circ$ is function
composition):

$M\textrm{id}_{X}=\textrm{id}_{MX}$ |  $M(f\circ g)=(Mf)\circ(Mg)$,
---|---

For example, let us show how to apply this definition to _finite lists_ :

######  Example 2.3.

The _finite lists_ functor maps every set $X$ into $X^{*}$ (i.e. the set of
finite lists over $X$), and it maps every function $f:X\to Y$ into a function
$f^{*}:X^{*}\to Y^{*}$ that applies $f$ element by element. It is not hard to
see that this satisfies the axioms from Definition 2.2.

We are now ready to give the definition of a _monad_ :

######  Definition 2.4.

A _monad_ is a functor $M$ equipped with two operations;

$\eta_{X}:X\to MX$ | and | $\mu_{X}:MMX\to X$
---|---|---

We are going to refer to $\eta$ as the _singleton_ operation, and to $\mu$ as
the _flatten_ operation. The two operations need to satisfy the axioms of a
monad, which can be found in Section A.1 of the appendix.

Let us now show how to apply this definition to _finite lists_ :

######  Example 2.5.

The functor of _finite lists_ can be equipped with the following monad
structure. The singleton operation $\eta:X\to X^{*}$ returns a singleton list
with the argument, and the flatten operation $\mu:MMX\to MX$ flattens the list
of lists into a single list. For example:

$\eta(3)=[3]$ | and | $\mu([[1,2,3],[4,5,6],[],[7,8],[9]])=[1,2,3,4,5,6,7,8,9]$
---|---|---

From the perspective of [2], the most important feature of monads is that they
can be used to define _Eilenberg-Moore algebras_ , which can be seen as a
generalization of monoids:

######  Definition 2.6.

An _Eilenberg-Moore algebra_ for a monad $M$ is a set $S$ together with a
multiplication function $\alpha:MS\to S$, that makes the following diagrams
commute222 We hope that the notation of commutative diagrams is intuitively
clear. See [1, Section 1.1.3] for more explanation. :

${{M\,M\,S}}$${{M\,S}}$${S}$${{M\,S}}$${{M\,S}}$${S}$${S}$$\scriptstyle{\mu_{S}}$$\scriptstyle{M\,\alpha}$$\scriptstyle{\alpha}$$\scriptstyle{\alpha}$$\scriptstyle{\textrm{id}_{S}}$$\scriptstyle{\eta_{S}}$$\scriptstyle{\alpha}$

To understand the intuition behind this definition, let us show that there is
a bijective correspondence between Eilenberg-Moore algebras for finite lists
and monoids:

######  Example 2.7.

Let $(X,\alpha)$ be an Eilenberg-Moore algebra for the finite list monad. We
can use $\alpha$ to define a binary operation and an identity element on $X$,
obtaining a monoid structure on $X$:

$x\cdot y=\alpha([x,y])$ | and |  $1_{X}=\alpha([\,])$,
---|---|---

To see that this is a valid monoid observe that:

$x\cdot(y\cdot
z)\stackrel{{\scriptstyle\textrm{def}}}{{=}}\alpha([x,\alpha([y,z])])\stackrel{{\scriptstyle\textrm{Ax.}\eta}}{{=}}\alpha([\alpha([x]),\alpha([y,z])])\stackrel{{\scriptstyle\textrm{Ax.}\mu}}{{=}}\alpha(\mu[[x],[y,z]])=\alpha([x,y,z])\textrm{,}$

where Ax.$\mu$ and Ax.$\eta$ denote the Eilenberg-Moore axioms from Definition
2.6. Using a similar reasoning one can show that $(x\cdot y)\cdot
z=\alpha([x,y,z])$, which means that the new binary operation is associative.
Similarly, one can show that $1_{X}$ is indeed an identity element.

To see that this defines a bijection between monoids and Eilenberg-Moore
algebras for finite lists, we define an inverse mapping that defines $\alpha$
in terms of the monoid structure:

$\alpha([x_{1},x_{2},\ldots,x_{n}])=x_{1}\cdot x_{2}\cdot\ldots\cdot x_{n}$ | and | $\alpha([\,])=1_{X}$
---|---|---

We are now ready to present the key definition from [2], i.e. a _recognizable
language for a monad $M$_:

######  Definition 2.8.

Let $M$ be a monad. We define an $M$-language over an alphabet $\Sigma$ to be
a subset of $M\Sigma$. We say that a language $L\subseteq M\Sigma$ is
$M$-definable if there exist:

$\underbrace{(A,\alpha)}_{\textrm{Finite }M\textrm{-algebra}}$ | $\underbrace{h:\Sigma\to A}_{\textrm{Input function}}$ |  $\underbrace{\lambda:\Sigma\to\\{\textrm{Yes},\textrm{No}\\}}_{\textrm{Acceptance function}}$,
---|---|---

such that the characteristic function of $L$ is equal to the following
composition:

$M\Sigma\stackrel{{\scriptstyle
M\,h}}{{\longrightarrow}}MA\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}A\stackrel{{\scriptstyle\lambda}}{{\longrightarrow}}\\{\textrm{Yes},\textrm{No}\\}$

Thanks to Example 2.7, it is not hard to see that for $M$ equal to the monad
of finite lists, the definition of $M$-recognizability is equivalent to
Definition 2.1, which further means that finite-list recognizability is
equivalent to regularity. There are many other examples of monads, which
define important classes of $M$-definable languages (e.g. see [3, Section
4.3]). In this paper, let us define two more, the _countable order monad_ and
the _terms monad_ :

######  Example 2.9 ([2, Example 15]).

Define a _countable chain_ over a set $X$, to be a countable linear order
where every position is labelled with an element of $X$. We say that two
chains are equal if there is an isomorphism between them that preserves both
the order and the labels333 It is worth noting that the set of all countable
sets is not, strictly speaking, a set. However, because we equate all chains
modulo isomorphism, the set of all chains over any given $X$ forms a set. This
is because, we can select an arbitrary infinite countable set and assume that
all positions in every chain are elements of that set. . Let us denote the set
of all countable chains over $X$ as $CX$, and let us show that $C$ is a monad.
First, let us define the functor structure on $C$. If $f$ is a function of
type $X\to Y$, then $Cf:CX\to CY$ is a function that applies $f$ to every
label of a chain (and does not modify the linear order). This leaves with
defining the monad structure: The _singleton_ operation $\eta:X\to CX$ returns
a one element chain, whose only position is labelled by the input letter. The
_flatten_ operation $\mu_{X}:CCX\to CX$ is defined in terms of the
lexicographic product: Let $w:C(CX)$ be a chain of chains, then $\mu w$ is
defined as follows:

  1. 1.

Its positions are pairs $(x,y)$ where $x$ is a position in $w$ and $y$ is a
position in $w_{x}$ (i.e. the label of $x$ in $w$);

  2. 2.

The label of $(x,y)$ is equal to the label of $y$;

  3. 3.

The pairs are ordered lexicographically, i.e. $(x_{1},y_{1})\leq(x_{2},y_{2})$
if $x_{1}<x_{2}$ or if $x_{1}=x_{2}$ and $y_{1}\leq y_{2}$.

It is not hard to verify that this construction satisfies the monad axioms
(see [2, Example 15] for details). It follows that we can apply Definition 2.8
and to define the class of $C$-recognizable languages. Interestingly, it turns
out that this class is equal to the class of languages that can be recognized
by the mso-logic (see [9, Theorem 5.1] or [3, Theorems 3.12 and 3.21] for
details), which is a strong argument for the intuition that
$C$-recognizability corresponds to the intuitive notion of regularity. In
particular, if we only consider those $C$-recognizable languages that only
contain $\omega$-words, we obtain the class of $\omega$-regular languages.

######  Example 2.10 ([3, Example 21]).

Fix a ranked set $\mathcal{S}$, i.e. a set where every element has an
associated arity from the set $\\{0,1,2,\ldots\\}$. For every set $X$, we
define $T_{\mathcal{S}}X$ to be the set of all finite trees where all leaves
are labelled with elements from $X$, and all inner nodes are labelled with
elements from $\mathcal{S}$, in such a way that the number of children of each
inner node is equal to the arity of its label. Here is an example for
$X=\\{x,y,z\\}$ and $\mathcal{S}=\\{\underbrace{a}_{\textrm{arity
2}},\underbrace{b}_{\textrm{arity 1}},\underbrace{c}_{\textrm{arity 0}}\\}$:

(Observe that the leaves labelled with elements of arity $0$ from
$\mathcal{S}$ are treated as inner nodes.) The set $T_{\mathcal{S}}X$ can also
be seen as the set of terms over the signature $\mathcal{S}$, with variables
from $X$. For example, for the following $\mathcal{S}$, elements of
$T_{\mathcal{S}}X$ are terms of propositional logic:

$\\{\underbrace{\vee}_{\textrm{arity 2}},\underbrace{\wedge}_{\textrm{arity
2}},\underbrace{\neg}_{\textrm{arity
1}},\underbrace{\mathtt{true}}_{\textrm{arity
0}},\underbrace{\mathtt{false}}_{\textrm{arity 0}}\\}$

For every fixed $\mathcal{S}$, we define a monad structure for
$T_{\mathcal{S}}$ called _the term monad_. The function mapping
$T_{\mathcal{S}}f$ applies $f$ to every leaf, and does not modify the inner
nodes. The _singleton_ operation returns a tree that consists of a single
leaf, labelled by the input argument. Finally, the _flatten_ operation simply
unpacks the trees from the leaves, as presented in the following figure:

Since $T_{\mathcal{S}}$ is a monad, we can use Definition 2.8 and define the
class of $T_{\mathcal{S}}$-recognizable languages. It turns out that this
class coincides with the usual notion of regularity for finite-tree languages
– this is because $T_{\mathcal{S}}$-algebras turn out to be practically the
same as deterministic bottom-up tree automata (but without distinguished
initial and accepting states – which are replaced by the input and output
functions from Definition 2.8). See [3, Example 21] for details.

Examples 2.9 and 2.10 (together with all the examples from [2, Sections 4.2,
5.1, and 6.2]) show that Definition 2.8 is abstract enough to capture the
notion of regularity for many different types of objects. On the other hand,
it is also concrete enough to allow for an interesting general theory of
$M$-recognizability. Examples of theorems include existence of syntactic
algebras ([3, Theorem 4.19]) and equivalence of algebra and language varieties
([3, Theorem 4.26]). There is also an ongoing quest for relating mso-
definability and $M$-recognizability (see [6]).

##  3 Comonads and transducers

In this section, we extend the theory of $M$-recognizability to transducers.
We start by presenting the definition of a _comonad_ , which is the dual
notion to a monad. Then, we show that for every functor $M$, that is both a
monad and a comonad, we can define the notion of $M$-recognizable
transductions. Finally, we provide some examples of such functors $M$, and
discuss their $M$-recognizable transduction classes. Let us start with the
definition:

######  Definition 3.1.

A _comonad_ is a functor $M$ equipped with two operations:

$\varepsilon_{X}:MX\to X$ | and | $\delta_{X}:MX\to MMX$
---|---|---

We are going to refer to $\varepsilon$ as the _extract_ operation, and to
$\delta$ as the _expand_ operation. The axioms of a comonad are dual to the
axioms of a monad, and can be found in Section B.1 of the appendix.

######  Example 3.2.

For example, let us consider the functor $X^{+}$ of non-empty lists (where the
lifting operation $f^{+}$ is defined as applying $f$ to every element of the
list). For this functor, we can define the comonad structure in the following
way. The _extract_ operation returns the last element of a list, and the
_extend_ operation transforms a list into a list of all its prefixes:

$\varepsilon([x_{1},\ldots,x_{n}])=x_{n}$ | $\delta([x_{1},\ldots,x_{n}])=[[x_{1}],[x_{1},x_{2}],\ldots,[x_{1},\ldots x_{n}]]$
---|---

(Observe that the definition of $\varepsilon$ crucially depends on the input
being a non-empty list.) It is not hard to verify that such $\delta$ and
$\varepsilon$ satisfy the axioms of a comonad.

This is not the only comonad structure one can define for $X^{+}$.
Symmetrically, _extract_ could return the first element, and _extend_ could
compute the list of all suffixes:

$\varepsilon([x_{1},\ldots,x_{n}])=x_{1}$ | $\delta([x_{1},\ldots,x_{n}])=[[x_{1},\ldots,x_{n}],[x_{2},\ldots,x_{n}],\ldots,[x_{n}]]$
---|---

To tell those two comonads apart, we denote the _prefix comonad_ as
$\overrightarrow{L}X$, and the _suffix comonad_ as $\overleftarrow{L}X$.

Next, let us observe that $X^{+}$ also exhibits the structure of a monad. The
structure is the same as the one for $X^{*}$ – the _flatten_ operation
flattens a list into a list of lists (note that this preserves nonemptiness),
and the _unit_ operation returns a singleton list. This means that functors
$\overrightarrow{L}X$ and $\overleftarrow{L}X$ are at the same time both
monads and comonads. The key observation made in this paper is that for such
functors one can define a natural class of transductions:

######  Definition 3.3.

Let $M$ be a functor that is both a monad and a comonad. We say that a
function $f:M\Sigma\to M\Gamma$ is an $M$-recognizable transduction if there
exist:

$\underbrace{(A,\alpha)}_{\begin{subarray}{c}\textrm{a finite }M\textrm{-algebra}\\\ (\textrm{with respect the monad structure of }M)\end{subarray}}$ | $\underbrace{h:\Sigma\to A}_{\textrm{an input function}}$ |  $\underbrace{\lambda:A\to\Gamma}_{\textrm{an output function}}$,
---|---|---

such that $f$ is equal to the following composition:

$M\,\Sigma\stackrel{{\scriptstyle
M\,h}}{{\longrightarrow}}M\,A\stackrel{{\scriptstyle\delta}}{{\longrightarrow}}M\,M\,A\stackrel{{\scriptstyle
M\,\alpha}}{{\longrightarrow}}M\,A\stackrel{{\scriptstyle
M\,\lambda}}{{\longrightarrow}}M\,\Gamma$

As it turns out, many interesting classes of transductions can be defined as
$M$-recognizable transducers for a suitable $M$. In Subsections 3.1 and 3.2,
we present some examples.

###  3.1 Examples of word-to-word transductions

We start by studying $\overrightarrow{L}$-recognizable transductions. After
unfolding the definition, we obtain that each such transduction is defined by
a finite semigroup444A semigroup is a monoid that might not have the identity
element. A reasoning similar to Example 2.7 demonstrates that semigroups are
the Eilenberg-Moore algebras for the monad $X^{+}$. $S$, an input function
$h:\Sigma\to S$, and an output function $\lambda:S\to\Gamma$. The transduction
is then defined in the following way:

$\underbrace{a_{1}\ a_{2}\ \ldots\ a_{n}}_{\Sigma^{+}}$ | $\mapsto$ | $\underbrace{\lambda\left(h(a_{1})\right),\ \lambda\left(h(a_{1})\cdot h(a_{2})\right),\ \ldots,\ \lambda\left(h(a_{1})\cdot\ldots\cdot h(a_{n})\right)}_{\Gamma^{+}}$
---|---|---

In other words, we obtain the $i$-th letter of the output, by taking the
$i$-th prefix of the input, computing the $S$-product of its $h$-values, and
applying the output function $\lambda$. By comparing this with Definition 2.1,
we see that this means that the $i$-th letter of the output is computed based
on regular properties of the $i$-th prefix. This means that
$\overrightarrow{L}$-recognizable transductions are equivalent to a well-
studied transducer model called _Mealy machines_. (See Section B.2 for the
exact definition of Mealy machines and the proof of equivalence.) Similarly,
one can show that the class of $\overleftarrow{L}$-recognizable transductions
is equivalent to the right-to-left variant of Mealy machines.

Next, we consider _length-preserving rational functions_ , which can be
defined as the class of transductions recognized by unambiguous Mealy machines
(see Section B.3 for the definition), or more abstractly as the class of
transductions where the $i$-th letter of the output depends on the $i$-th
letter of the input and on regular properties of the $(i-1)$-st prefix and
$(i+1)$-st suffix. Below we define a monad/comonad functor of _pointed list_
555 This is a well-known functor and both its monad [8, Section 8] and its
comonad [22, Section 3.2.3] structures have been studied in the past.
(Although, rarely together.)  that recognizes this class:

######  Definition 3.4.

We define $\overline{L}X$ to be the set of all non-empty lists over $X$ with
exactly one underlined element. For example, $[a,\underline{b},b,c]$ is an
element of $\overline{L}\\{a,b,c\\}$. This is clearly a functor, with
$\overline{L}f$ defined as simply applying $f$ to every element of the list
(and keeping the underline where it was). The monadic and comonadic operations
work as follows:

  1. 1.

The _singleton_ operation returns a list with one underlined element, e.g.:
$\eta(a)=[\underline{a}]$.

  2. 2.

The _flatten_ operation, flattens a list of list, while keeping the double-
underlined element:

$\mu\left(\left[[a,\ \underline{b},\ c],\ \underline{[\underline{d},\ e,\
f]},\ [g,\ \underline{h}]\right]\right)=[a,\ b,\ c,\ \underline{d},\ e,\ f,\
g,\ h]$

  3. 3.

The _extract_ operation extracts the underlined element, e.g.:
$\varepsilon([a,\ \underline{b},\ c])=b$.

  4. 4.

The _extend_ operation generates a series of new lists, each being a copy of
the original list, but with a different, consecutive element underlined in
each of the copies. Finally, it underlines the copy that is exactly equal to
the input list (including the underlined element):

$\delta([a,\ \underline{b},\
c])=\left[[\underline{a},b,c],\underline{[a,\underline{b},c]},[a,b,\underline{c}]\right]$

Before we discuss $\overline{L}$-definable transducers, let us formulate a
lemma about $\overline{L}$-algebras. The lemma is based on [8, Section 8.1]
and shows that computing products in $\overline{L}$-algebras, boils down to
computing two monoid products (for proof, see Section B.3 of the appendix):

######  Lemma 3.5.

For every $\overline{L}$-algebra $(A,\alpha)$, there are two monoids $M_{L}$
and $M_{R}$, together with functions $h_{L}:A\to M_{L}$, $h_{R}:A\to M_{R}$,
such that the value of every $A$-product

$\alpha([a_{1},\ldots,\underline{a_{i}},\ldots,a_{n}])$

depends only on:

  1. 1.

the $M_{L}$-product of the prefix (i.e. $h_{L}(a_{1})\cdot\ldots\cdot
h_{L}(a_{i-1})$),

  2. 2.

the $M_{R}$-product of the suffix (i.e. $h_{R}(a_{i+1})\cdot\ldots\cdot
h_{R}(a_{n})$), and

  3. 3.

the exact $A$-value of the underlined element ($a_{i}$).

Moreover, if $A$ is finite then both $M_{L}$ and $M_{R}$ are finite as well.

We are now ready to discuss $\overline{L}$-definable transductions. Each such
transduction is, by definition, given by a finite $\bar{L}$-algebra
$(A,\alpha)$, an input function $h:\Sigma\to A$, and an output function
$\lambda:A\to\Gamma$. A transduction given in this way computes its $i$-th
output letter as:

$\lambda(\alpha([h(a_{1}),\ldots,\underline{h(a_{i})},\ldots,h(a_{n})]))$

Thanks to Lemma 3.5, we know that we know that there are two monoids $M_{L}$
and $M_{R}$, such that we can compute this value based on the $M_{L}$-product
of the prefix, $M_{R}$-product of the suffix and the value of $h(a_{i})$. It
follows, by Definition 2.1 of regularity, that we can compute the $i$-th
letter of the output based on some regular properties of the prefix, some
regular properties of the suffix, and on the $i$-th input letter. This means
that every $\overline{L}$-definable transduction is also a rational length-
preserving function666 It might be worth mentioning that there is a slight
type mismatch between the types of rational length-preserving transductions
and $\overline{L}$-definable transductions. The former are of the type
$\Sigma^{+}\to\Gamma^{+}$, and the latter of type
$\bar{L}(\Sigma)\to\bar{L}(\Gamma)$. We can deal with this mismatch, by
observing that for the $\bar{L}$-definable transducers, the position of the
underlined element does not influence the underlying output word. See Appendix
B.3 for more details. . To prove the other inclusion, we use a similar idea to
transform an unambiguous Mealy machine into $\bar{L}$-algebra. (See Appendix
B.3 for a more detailed proof.)

Here is a table that summarizes all classes of $M$-definable transductions, we
have seen so far:

Transduction class | Machine model | Functor
---|---|---
Sequential left-to-right | Mealy machines | $\overrightarrow{L}$
Sequential right-to-left | Right-to-left Mealy machines | $\overleftarrow{L}$
Rational lenght-preserving | Unambigous Mealy machines | $\overline{L}$

Observe that all those examples are length-preserving. This is a consequence
of a more general principle, which can be stated using the _shape_ of a
functor:

######  Definition 3.6.

Let $1=\\{\bullet\\}$ be a singleton set. For every functor $F$ and every
$l\in FX$, we define the _shape_ of $l$ as the element of $F\,1$, obtained by
replacing every element of $X$ by $\bullet$:

$\mathtt{shape}(l)=(F(x\mapsto\bullet))\;l$

For example, the shapes of both $\overrightarrow{L}$ and $\overleftarrow{L}$
are their lengths, and the shape $\bar{L}$ is its length and the position of
its underlined element. It is not hard to see that all $M$-definable
transductions are shape-preserving:

######  Lemma 3.7.

For every $M$-definable transduction $F:M\Sigma\to M\Gamma$, and for every
$w\in M\Sigma$, it holds that $\mathtt{shape}(F(w))=\mathtt{shape}(w)$.

###  3.2 Other examples

#### Infinite words

In this section we extend the monad $C$ from Example 2.9 with three different
comonad structures $\overrightarrow{C}$, $\overleftarrow{C}$, and $\bar{C}$
(which are analogous to $\overrightarrow{L}$, $\overleftarrow{L}$ and
$\bar{L}$ from Section 3.1), and we briefly characterize the resulting classes
of transducers.

We define $\overrightarrow{C}X\subsetneq CX$, to be the set of all elements of
$CX$ that have a maximal element. To see that this is a monad (with the
_singleton_ and _flatten_ operations inherited from $C$), we observe that
_flatten_ preserves the property of having maximal elements. Next, we define a
comonad structure on $\overrightarrow{X}$: _extract_ returns the label of the
maximal element, and _expand_ labels each position with its prefix, i.e. the
position $i$ of $\delta(l)$ is labelled with: $\\{x\ |\ x\in l\;\wedge\;x\leq
i\\}$. Observe that all such labels contain maximal elements – the maximal
element in the label of $i$ is $i$ itself. As it turns out, the class of
$\overrightarrow{C}$-definable transductions admits a logical
characterization: One can show777The proof follows from the fact that
$C$-recognisability is equivalent to mso-definability. However, since mso-
transductions fall slightly out of scope for this paper, we are not going to
give a precise proof. For other transducer classes in this section, we use a
similar mso-recognisability argument. that it is equivalent to the class of
transductions, that preserve the underlying order (see Lemma 3.7), and compute
the new label for each position $i$ based on mso-formulas that only see the
positions $\leq i$. The definition of $\overleftarrow{C}$ and the
characterization of $\overleftarrow{C}$-definable transduction are analogous.

Next, we define $\bar{C}X$ to be the set of all elements of $CX$ where exactly
one position is underlined. The monad structure of $\bar{C}X$ is a
generalization of the monad structure of $\bar{L}$: _singleton_ returns a
single underlined element, and _flatten_ flattens the input and underlines the
doubly underlined position. Similarly, the comonad structure of $\bar{C}X$
generalizes the comonad structure of $\bar{L}$: _extract_ returns the label of
the underlined element, and _expand_ labels every position $i$ of its input
with a copy of the input where $i$ is the underlined position, and underlines
the copy that corresponds to the underlined position of the input. The class
of $\bar{C}$-definable transduction also admits a logical characterization: It
is equivalent to the class of transductions that preserve the underlying order
and the position of the underline, and compute the output labels based on mso-
formulas that see the entire input.

#### Terms

Finally we define $\bar{T}_{\mathcal{S}}$ to be _pointed_ version of the term
functor from Example 2.10, and we equip it with structures of a monad and a
comonad. The construction is analogous888 It seems that the _pointing_
construction is a general way of equipping a monad with a comonad structure.
to $\bar{L}$ and $\bar{C}$. We define $\bar{T}_{\mathcal{S}}X$, to be the set
of trees (from $\bar{T_{\mathcal{S}}}X$) with exactly one underlined leaf. The
monadic and comonadic operations are defined analogously as for $\bar{L}$ and
$\bar{C}$.

As it turns out, the class of $\bar{T_{\mathcal{S}}}$ definable transductions,
also admits a logical characterization: it is equivalent to the class of tree-
to-tree transductions that only modify the labels of the leaves (this is a
consequence of Lemma 3.7) and calculate the output label for each leaf based
on mso-formulas that have access to the entire input tree.

##  4 Compositions of recognizable transducers

So far we have introduced, and presented a few examples of $M$-recognizable
transductions. In this section we are going to prove Theorem 4.8 which states
that $M$-recognizable transductions are closed under compositions, i.e. if
$f:M\,\Sigma\to M\,\Gamma$ and $g:M\,\Gamma\to M\,\Delta$ both are
$M$-recognizable transductions, then so is their composition $g\circ
f:M\,\Sigma\to M\,\Delta$. In addition to the axioms of a functor, monad, and
comonad, we have seen so far, the proof of the theorem requires some
additional _coherence axioms_ which relate the monadic and the comonadic
structures of $M$. Here are three examples of such axioms respectively called
_flatten-extract_ , _singleton-expand_ , and _singleton-extract_ 999 To the
best of our knowledge, this axiom has not appeared so far in the literature. :

${{M\,M\,X}}$${{M\,X}}$${X}$${{MX}}$${X}$${{MX}}$${{M\,X}}$${X}$${{MX}}$${{MMX}}$${X}$$\scriptstyle{\mu_{X}}$$\scriptstyle{\varepsilon_{X}}$$\scriptstyle{\varepsilon_{MX}}$$\scriptstyle{\varepsilon_{X}}$$\scriptstyle{\eta_{X}}$$\scriptstyle{\eta_{X}}$$\scriptstyle{M\eta_{X}}$$\scriptstyle{\delta_{X}}$$\scriptstyle{\eta_{X}}$$\scriptstyle{\varepsilon_{X}}$$\scriptstyle{id}$

The other axioms postulate the existence of an additional structure on $M$.

###  4.1 The put-structure and its axioms

For a comonad $M$, let us consider the following operation101010The operation
$\mathtt{put}$ has already been studied in the context of functional
programming. In this context, $M$ does not need to be a (full) comonad, it is,
however, required to implement the operation $\mathtt{get}:MX\to X$, which in
our case is equal to $\varepsilon$. In this context, the pair
($\mathtt{get},\mathtt{put}$) is usually referred to as a lens. See [15,
Section 1] for details. See [16, Section 3.1] for the original reference.:

$\mathtt{put}_{A}\ :\ M\,A\times A\to MA$

The intuition behind $\mathtt{put}$ is that it replaces the _focused element_
of $MA$ with the given element from $A$. The intuition behind the _focused
element_ is that this is the element that is going to be returned by the
_extract_ operation. For example, the focused element in $\bar{L}$ is the
underlined element, and in $\overrightarrow{L}$ it is the last element of the
list. Here are two examples of $\mathtt{put}$:

$\underbrace{\mathtt{put}([1,\underline{2},3,4],7)=[1,7,3,4]}_{\bar{L}}$ | $\underbrace{\mathtt{put}([1,2,3],5)=[1,2,5]}_{\overrightarrow{L}}$
---|---

The goal of this subsection is to formalize this intuition in terms of axioms.
First, we assume that $\mathtt{put}$ is a natural transformation (see Section
C.1 for details). Next, we assume the following axioms that relate
$\mathtt{put}$ and $\varepsilon$. They are called _get-put_ , _put-get_ , and
_put-put_ 111111The axioms and their names come from the _lens_ -related
research. See [15, Section 1].:

${{M\,A}}$${{M\,A\times A}}$${{MA\times A}}$${{MA}}$${{(MA\times A)\times
A}}$${{MA\times A}}$${{M\,A}}$${A}$${{MA\times
A}}$${{MA}}$$\scriptstyle{id}$$\scriptstyle{\langle
id,\,\varepsilon_{A}\rangle}$$\scriptstyle{\texttt{put}_{A}}$$\scriptstyle{\pi_{2}}$$\scriptstyle{\varepsilon_{A}}$$\scriptstyle{\mathtt{put}_{A}}$$\scriptstyle{\mathtt{put}_{A}}$$\scriptstyle{\mathtt{put}_{A}}$$\scriptstyle{\pi_{2}\times\mathtt{id}}$$\scriptstyle{\mathtt{put}_{A}\times
id}$

Here the functions $\langle f,g\rangle$, $f\times g$, $\pi_{2}$ are defined as
follows:

$\langle f,g\rangle(x)=(f(x),\ g(x))$ | $(f\times g)(x_{1},\ x_{2})=(f(x_{1}),\ g(x_{2}))$ | $\pi_{2}(x,y)=y$
---|---|---

The following axioms called _put-associativity_ and _singleton-put_ relate
$\mathtt{put}$ with the structure of a monad121212To the best of our knowledge
this axiom has not appeared previously in the literature.:

${{MMA\times MA\times A}}$${{MMA\times MA}}$${{MMA}}$${{A\times
A}}$${{MA\times A}}$${{MMA\times A}}$${{MA\times
A}}$${{MA}}$${A}$${{MA}}$$\scriptstyle{\mathtt{put}_{A}}$$\scriptstyle{\mu_{A}\times
id}$$\scriptstyle{\mathtt{put}_{MA}\times
id}$$\scriptstyle{id\times\mathtt{put}_{A}}$$\scriptstyle{\mathtt{put}_{MA}}$$\scriptstyle{\mu_{A}}$$\scriptstyle{\pi_{2}}$$\scriptstyle{\eta_{A}}$$\scriptstyle{\eta_{A}\times
id}$$\scriptstyle{\mathtt{put}_{A}}$

The final axiom relates all the structures studied in this paper: monad,
comonad, and $\mathtt{put}$. Before we present it, we need to define the
_strength of a functor_ 131313 This definition of $\mathtt{strength}$ is
specific to Set. We briefly discuss other categories in Section D.1. .

######  Definition 4.1.

For every functor $F$, we define $\mathtt{strength}_{(A,B)}:A\times MB\to
M(A\times B)$:

$\mathtt{strength}(a,l)=F(x\mapsto(a,x))\ l$

Intuitively, the function $\mathtt{strength}_{(A,B)}$ equips each element $B$
under the functor $F$ with a copy of $a\in A$. Here is an example, for $F$
equal to the list functor:

$\mathtt{strength}(c,[a,b,a,b])=[(c,a),(c,b),(c,a),(c,b)]$

We are now ready to present the final coherence axiom, called _flatten-expand_
141414To the best of our knowledge the axiom has not appeared before in the
literature.:

${{MMMA}}$${{MMMA}}$${{MMA}}$${{MMA}}$${{MA}}$$\scriptstyle{\mu_{A}}$$\scriptstyle{\delta_{A}}$$\scriptstyle{\mu_{MA}}$$\scriptstyle{\delta_{MA}}$$\scriptstyle{M\mathtt{work}}$

where the function $\mathtt{work}$ is defined as the following composition:

$MMA\stackrel{{\scriptstyle\langle\textrm{id},\varepsilon\rangle}}{{\longrightarrow}}MMA\times
MA\stackrel{{\scriptstyle\textrm{id}\times\delta}}{{\longrightarrow}}MMA\times
MMA\stackrel{{\scriptstyle\mathtt{strength}}}{{\longrightarrow}}M(MMA\times
MA)\stackrel{{\scriptstyle
M\mathtt{put}}}{{\longrightarrow}}MMMA\stackrel{{\scriptstyle
M\mu}}{{\longrightarrow}}MA$

Let us now briefly present the intuition behind the flatten-expand axiom. The
starting point $MMX$ represents a structure partitioned into substructures
(e.g. a list partitioned into sublists), which we would like to expand using
$\delta$. The bottom path of the diagram represents the straightforward
approach: First, it flattens the input using $\mu_{A}$ (forgetting about the
substructure partitions), and then it applies the $\delta_{A}$ function. The
flatten-expand axiom asserts that this can be done in a way that respects the
initial partitions. This way is represented by the top path of the diagram:
First, it applies the $\delta_{MA}$ function to expand the top structure; then
it applies the $\mathtt{work}$ function independently to each of the
substructures using $M\,\mathtt{work}$ (this can also be seen as a concurrent
computation); and finally it aggregates the results of $\mathtt{work}$ using
$\mu_{MA}$. (See Section C.2 for a step-by-step example.) It might also be
worth mentioning that the flatten-expand axiom has an alternative formulation
in terms of a _bialgebra_ (see Section C.3).

Finally, let us mention that it is not hard to all the examples of
monad/comonad functors from Section 3 with the natural $\mathtt{put}$
operation, and show that they satisfy all the axioms we have introduced.

###  4.2 Contexts

In this section we use the $\mathtt{put}$ structure to introduce _contexts_
for Eilenberg-Moore algebras. This concept plays an important role in the
proof of Theorem 4.8. Additionally, we would like to highlight the potential
of contexts as an independently interesting tool for studying Eilenberg-Moore
algebras – this point is illustrated by Definition 4.7. In this subsection, we
only assume that $M$ is a monad equipped with the $\mathtt{put}$ structure –
it does not depend on the comonad structure of $M$.

######  Definition 4.2.

Let $(A,\alpha)$ be an $M$-algebra. For every element $l\in MA$, we define its
_context_ to be the following function $\mathtt{ctx}_{l}:A\to A$:

$\mathtt{ctx}_{l}(x)=\alpha(\mathtt{put}(l,x))$

In other words, the context of $l$ takes an element $x\in A$, replaces the
focused element of $l$ with $x$, and calculates the product of the resulting
$MA$.

Let us now discuss some properties of the contexts. Thanks to the put-put
axiom one can show that the context of $l$ does not depend on its focused
element (the formal proof is verified in Coq as ctxPutInvariant, see Section
E.3).

######  Lemma 4.3.

For every $l\in MA$, and every $a\in A$, the context of $l$ is equal to the
context of $\mathtt{put}(l,a)$, i.e.
$\mathtt{ctx}_{l}=\mathtt{ctx}_{\mathtt{put}(l,a)}$.

Similarly, using the singleton-put axiom, one can show that the context of
every singleton is the identity function (the formal proof is verified in Coq
as ctxUnitId, see Section E.3).

######  Lemma 4.4.

For every $a\in A$, it holds that $\mathtt{ctx}_{(\eta_{A}\,a)}=\textrm{id}$.

Now, let us consider the set of all contexts:

######  Definition 4.5.

For every $M$-algebra $(A,\alpha)$, we define the set $C_{A}\subseteq(A\to A)$
to be the set of all possible contexts, i.e. $C_{A}=\\{\mathtt{ctx}_{l}\ |\
l\in MA\\}$.

The important property of $C_{A}$ is that it is closed under compositions:

######  Lemma 4.6.

For every $f,g\in C_{A}$, it holds that $f\circ g\in C_{A}$.

It follows that $C_{A}$ is a transformation monoid of $A$. It follows that the
mapping $A\mapsto C_{A}$ allows us to transform an arbitrary $M$-algebra into
a monoid. This is why, we believe that contexts, are an interesting tool for
studying Eilenberg-Moore algebras. To illustrate this point let us show how to
generalize the definition of a _group_ :

######  Definition 4.7.

We say that an $M$-algebra $A$ is an _$M$ -group_ if $C_{A}$ is a group (i.e.
for every function $f\in C_{A}$, its inverse $f^{-1}$ also belongs to
$C_{A}$).

In order to validate this definition, let us show that for
$M=\overrightarrow{L}$ the definition of $M$-group coincides with the usual
definition of a group151515 If we only consider the monad structure then
$\overrightarrow{L}$ is equal to $X^{+}$ (i.e. the monad of non-empty lists).
However, we point out that we consider $\overrightarrow{L}$, because the
definition of $\mathtt{put}$ depends on whether we consider
$\overrightarrow{L}$ or $\overleftarrow{L}$. (The proof for
$\overleftarrow{L}$ is, however, analogous).  (remember that
$\overrightarrow{L}$-algebras are semigroups). For this, let us fix an
$\overrightarrow{L}$-algebra $S$ (i.e. a semigroup). Observe now that, by
definition, the context of an element $[s_{1},\ldots,s_{n}]$ is equal to the
following function:

$x\mapsto s_{1}\cdot\ldots\cdot s_{n-1}\cdot x$

It follows that every element of $C_{S}$ is of the form $x\mapsto sx$, where
$s$ is an element of $S^{1}$, where $S^{1}$ is the smallest monoid that
contains $S$, i.e.:

$S^{1}=\begin{cases}S&\textrm{if $S$ already contains and identity element}\\\
S+\\{1\\}&\textrm{otherwise}\end{cases}$

Here $1$ denotes the _formal identity element_ whose operations are defined as
$1\cdot x=x\cdot 1=x$. Moreover $C_{S}$ is isomorphic to $S^{1}$:

$(x\mapsto s_{1}\cdot x)\circ(x\mapsto s_{2}\cdot x)=(x\mapsto s_{1}\cdot
s_{2}\cdot x)$

This finishes the proof, as it is not hard to see that $S$ is a group if and
only if $S^{1}$ is a group.

###  4.3 Composition theorem

We are now ready to formulate and prove the main theorem of this article:

######  Theorem 4.8.

Let $M$ be a functor that is both a monad and a comonad, for which there
exists a $\mathtt{put}:MA\times A\to MA$, that satisfies the axioms mentioned
in this section, i.e.: flatten-extract, get-put, put-get, put-associativity,
and flatten-expand. Then, the class of $M$-definable transductions is closed
under compositions.

The reminding part of this section is dedicated to proving Theorem 4.8. After
unfolding the definitions, this boils down to showing that for each pair of
$M$-algebras $(S_{1},\alpha_{1})$, $(S_{2},\alpha_{2})$, and for every
$h_{1}:\Sigma\to S_{1}$, $h_{2}:\Gamma\to S_{2}$,
$\lambda_{1}:S_{1}\to\Gamma$, $\lambda_{2}:S_{2}\to\Delta$, there exists an
$M$-algebra $(S_{3},\alpha_{3})$ and functions $h_{3}:\Sigma\to S_{3}$,
$\lambda_{3}:S_{3}\to\Delta$, that make the following diagram commute:

${{M\Sigma}}$${{MS_{1}}}$${{MMS_{1}}}$${{MS_{1}}}$${{M\Gamma}}$${{MS_{3}}}$${{MS_{2}}}$${{MMS_{3}}}$${{MMS_{2}}}$${{MS_{3}}}$${{MS_{2}}}$${{M\Delta}}$$\scriptstyle{Mh_{1}}$$\scriptstyle{\delta}$$\scriptstyle{M\alpha_{1}}$$\scriptstyle{M\lambda_{1}}$$\scriptstyle{Mh_{2}}$$\scriptstyle{\delta}$$\scriptstyle{M\alpha_{2}}$$\scriptstyle{M\lambda_{2}}$$\scriptstyle{Mh_{3}}$$\scriptstyle{\delta}$$\scriptstyle{M\alpha_{3}}$$\scriptstyle{M\lambda_{3}}$

As our $S_{3}$ we are going to use the following set:

$S_{3}=S_{1}\times(S_{1}^{S_{1}}\to S_{2})$

(Note that $S_{1}^{S_{1}}$ is a notation for $S_{1}\to S_{1}$ – we mix the
arrow notation and the exponent notation for visual clarity.) Because of its
similarities with the _wreath product_ for semigroups, we call our
construction for $(S_{3},\alpha_{3})$ as the _generalized wreath product_ , or
_$M$ -wreath product_ of $(S_{1},\alpha_{1})$ and $(S_{2},\alpha_{2})$. (In
the appendix we give a definition of the classical wreath product and compare
it with the generalized wreath product – reading this part of the appendix
could make it easier to understand the construction presented below.) Before
we define $\alpha_{3}$, $h_{3}$ and $\lambda_{3}$, we describe what we would
like the composition161616 By [3, Lemma 4.7], this composition could be used
to define the product operation on $S_{3}$. However, since the lemma has extra
assumptions, we show this function only for intuition.
$M\Sigma\stackrel{{\scriptstyle
Mh_{3}}}{{\longrightarrow}}MS_{3}\stackrel{{\scriptstyle\alpha_{3}}}{{\longrightarrow}}S_{3}$
to do – this way we can present some intuitions behind $S_{3}$. We start with
a $w\in M\Sigma$ and we would like to produce a pair
$S_{1}\times(S_{1}^{S_{1}}\to S_{2})$. The first component (i.e. $S_{1}$) is
simply defined as the $S_{1}$-product of the input:

$M\Sigma\stackrel{{\scriptstyle
Mh_{1}}}{{\longrightarrow}}MS_{1}\stackrel{{\scriptstyle\alpha_{1}}}{{\longrightarrow}}S_{1}$

The interesting part is the second component (i.e. $S_{1}^{S_{1}}\to S_{2}$),
which represents the $S_{2}$ product of the input. In order to compute it, we
first apply the first $M$-transduction (i.e. ($S_{1}$, $h_{1}$,
$\lambda_{1}$)), and then we compute the $S_{2}$-product of the result. This
means that the $S_{2}$ product depends on the $S_{1}$-context in which we
evaluate the input, so we provide it as the $S_{1}^{S_{1}}$ argument
(intuitively we are only interested in the functions from $C_{S_{1}}$, as
defined in Section 4.2, but the definition makes formal sense for all
functions $S_{1}^{S_{1}}$). Here is how to compute the $S_{2}$-value based on
the input word $w\in M\Sigma$ and the context $c\in S_{1}^{S_{1}}$: We start
by computing the $S_{1}$-products of the views (while, for now, ignoring the
context $c$):

$S_{1}^{S_{1}}\times M\Sigma\stackrel{{\scriptstyle\textrm{id}\times
Mh_{1}}}{{\longrightarrow}}S_{1}^{S_{1}}\times
MS_{1}\stackrel{{\scriptstyle\textrm{id}\times\delta}}{{\longrightarrow}}S_{1}^{S_{1}}\times
MMS_{1}\stackrel{{\scriptstyle\textrm{id}\times
M\alpha_{1}}}{{\longrightarrow}}S_{1}^{S_{1}}\times MS_{1}$

Next, we apply the context $c$ to each of the prefix products, and compute its
$\Gamma$-value:

$S_{1}^{S_{1}}\times
MS_{1}\stackrel{{\scriptstyle\mathtt{strength}}}{{\longrightarrow}}M(S_{1}^{S_{1}}\times
S_{1})\stackrel{{\scriptstyle
M\mathtt{app}}}{{\longrightarrow}}MS_{1}\stackrel{{\scriptstyle
M\lambda_{1}}}{{\longrightarrow}}M\Gamma$

Finally, we compute the $S_{2}$-product of the result:

$M\Gamma\stackrel{{\scriptstyle
Mh_{2}}}{{\longrightarrow}}MS_{2}\stackrel{{\scriptstyle\alpha_{2}}}{{\longrightarrow}}S_{2}$

We are now ready to define $\lambda_{3}$, $h_{3}$, and $\alpha_{3}$. In order
to compute $\lambda_{3}$, we compute the $S_{2}$-value in the empty context
(represented by $\textrm{id}\in S_{1}^{S_{1}}$), and then apply $\lambda_{2}$:

$\lambda_{3}((v_{1},v_{2}))=\lambda_{2}(v_{2}(\textrm{id}))$

The function $h_{3}:\Sigma\to S_{1}\times(S_{1}^{S_{1}}\to S_{2})$ is defined
as follows: In order to compute the $S_{1}$ value we simply apply $h_{1}$ to
the input letter, and in order to compute the $S_{2}$ value given the context
$c\in S_{1}^{S_{1}}$, we apply $h_{1}$, $c$, $\lambda_{1}$ and $h_{2}$:

$h_{3}(a)=\left(h_{1}(a),\ \ c\mapsto
h_{2}\left(\lambda_{1}(c(h_{1}(a)))\right)\ \right)$

Finally, we define the product operation:

$\alpha_{3}:M(S_{1}\times(S_{1}^{S_{1}}\to
S_{2}))\to(S_{1}\times(S_{1}^{S_{1}}\to S_{2}))$

We define $\alpha_{3}$ using two auxiliary functions $f_{1}$ and $f_{2}$:

$\alpha_{3}(l)=\left(\,f_{1}(l),\ c\;\mapsto\;f_{2}(c,l)\,\right)$

The first function $f_{1}:M(S_{1}\times(S_{1}^{S_{1}}\to S_{2}))\to S_{1}$
computes the product of the $S_{1}$-values:

$M(S_{1}\times(S_{1}^{S_{1}}\to S_{2}))\stackrel{{\scriptstyle
M\pi_{1}}}{{\longrightarrow}}MS_{1}\stackrel{{\scriptstyle\alpha_{1}}}{{\longrightarrow}}S_{1}$

The second function $f_{2}:S_{1}^{S_{1}}\times M(S_{1}\times(S_{1}^{S_{1}}\to
S_{2}))\to S_{2}$ is more complicated. We start by computing for each element,
its view on the $S_{1}$-values while keeping its $(S_{1}^{S_{1}}\to
S_{2})$-value:

$S_{1}^{S_{1}}\times M(S_{1}\times(S_{1}^{S_{1}}\to
S_{2}))\stackrel{{\scriptstyle\textrm{id}\times\delta}}{{\longrightarrow}}S_{1}^{S_{1}}\times
MM(S_{1}\times(S_{1}^{S_{1}}\to
S_{2}))\stackrel{{\scriptstyle\textrm{id}\times\langle
M\pi_{1},\pi_{2}\circ\varepsilon\rangle}}{{\longrightarrow}}S_{1}^{S_{1}}\times
M((MS_{1})\times(S_{1}^{S_{1}}\to S_{2}))$

Then we compute the context for each of those $S_{1}$-views:

$S_{1}^{S_{1}}\times M((MS_{1})\times(S_{1}^{S_{1}}\to
S_{2}))\stackrel{{\scriptstyle\textrm{id}\times
M(\mathtt{ctx}\times\textrm{id})}}{{\longrightarrow}}S_{1}^{S_{1}}\times
M(S_{1}^{S_{1}}\times(S_{1}^{S_{1}}\to S_{2}))$

Next, we compose the initial context with each of the intermediate contexts:

$S_{1}^{S_{1}}\times M(S_{1}^{S_{1}}\times(S_{1}^{S_{1}}\to
S_{2}))\stackrel{{\scriptstyle\mathtt{strength}}}{{\longrightarrow}}M(S_{1}^{S_{1}}\times
S_{1}^{S_{1}}\times(S_{1}^{S_{1}}\to S_{2}))\stackrel{{\scriptstyle
M((\circ)\times\textrm{id})}}{{\longrightarrow}}M(S_{1}^{S_{1}}\times(S_{1}^{S_{1}}\to
S_{2}))$

Now, in each position, we apply the function to the argument:

$M(S_{1}^{S_{1}}\times(S_{1}^{S_{1}}\to S_{2}))\stackrel{{\scriptstyle
M((x,f)\mapsto f(x))}}{{\longrightarrow}}MS_{2}$

Finally, we compute the product of the $S_{2}$ values:

$MS_{2}\stackrel{{\scriptstyle\alpha_{2}}}{{\longrightarrow}}S_{2}$

This finishes the construction of $(S_{3},\alpha_{3})$. Now we need to show
that it is indeed an $M$-algebra:

######  Lemma 4.9.

The generalized wreath product $(S_{3},\alpha_{3})$, as defined above, is a
valid $M$-algebra, i.e. for every $l\in MMS_{3}$, and every $x\in S_{3}$ it
satisfies the following axioms (see Definition 2.6):

$\alpha_{3}(\mu(l))=\alpha_{3}((M\alpha_{3})(l))$ | and | $\alpha_{3}(\eta(x))=x$
---|---|---

The proof of Lemma 4.4 is quite complex – the main reason for this is that the
definition of $(S,\alpha_{3})$ is rather involved. In contrast, the idea
behind the proof is straightforward: we unfold all definition and perform
equational reasoning using the axioms. For this reason, we decided to
formalize the proof in the Coq theorem prover – it can be found as theorems
S3Associative and S3UnitInvariant in the attached Coq file, see Section E.2.
Finally, we show that the $M$-transduction $(S_{3},h_{3},\lambda_{3})$
computes the required compositions:

######  Lemma 4.10.

The $M$-transduction $(S_{3},h_{3},\lambda_{3})$ is equivalent to the
composition of $M$-transductions $(S_{1},h_{1},\lambda_{1})$ and
$(S_{2},h_{2},\lambda_{2})$.

Similarly as for Lemma 4.9, we prove Lemma 4.10 by unfolding the definitions
and applying the equational reasoning. It is called compositionCorrect in the
formalization, see Section E.2. The proof of Lemma 4.10 finishes the proof of
Theorem 4.8.

##  5 Further work

1\. Shape-modifying transductions.

Many important classes of transduction can modify the shape of their inputs.
Examples of such classes for word-to-word transductions include _regular
transductions_ (defined, for example, by _two-way transducers_ , or _mso
-transductions)_ or _polyregular transductions_ (defined, for example, by _for
programs_ or _mso -interpretations_ [5]). Extending the definitions of
$M$-definable transductions to capture those classes is, in our opinion, an
interesting research direction. As a first step towards this goal, let us
propose the following relaxation of $M$-definable transduction. The output
function $\lambda$ is of type $A\to M\Gamma$ (rather than $A\to\Gamma$), and
the transduction is defined as follows:

$M\Gamma\stackrel{{\scriptstyle
Mh}}{{\longrightarrow}}MA\stackrel{{\scriptstyle\delta}}{{\longrightarrow}}MMA\stackrel{{\scriptstyle
M\alpha}}{{\longrightarrow}}MA\stackrel{{\scriptstyle
M\lambda}}{{\longrightarrow}}MMA\stackrel{{\scriptstyle\mu}}{{\longrightarrow}}MA$

For example, for $M=\overrightarrow{L}$ this new class corresponds where the
transitions are allowed to output more than one letter (but have to output at
least one letter).

2\. Aperiodicity.

We say that a semigroup $S$ is _aperiodic_ , if there is no monomorphism $G\to
S$, where $G$ is a non-trivial group. This is an importation notion in the
theory of regular languages and transducers. For example, it very often
coincides with _first-order definability_ (e.g. [24]). Thanks to Definition
4.7, we can extend the definition of aperiodicity to arbitrary $M$-algebras
(for $M$s that are monads and comonads, and are equipped with the
$\mathtt{put}$). Studying this new notion of _generalized aperiodicity_ could
be an interesting research direction.

3\. Krohn-Rhodes decompositons.

The Krohn-Rhodes decomposition theorem ([18, Theorem (ii)]) shows how to
present every semigroup with wreath products of groups and a $3$-element
monoid called _flip-flop monoid_. Its original proof starts by decomposing
Mealy machines, and then it shows how to decompose monoids. Since in our
paper, we generalize the definitions of a group, a wreath product, and a Mealy
machine, we believe that there is potential for generalizing the original
Krohn-Rhodes theorem to $M$-algebras.

4\. Other categories.

A natural follow-up of this paper would be generalizing it from the category
Set to arbitrary Cartesian closed categories. For now the biggest obstacle to
such a generalization seems to be the $\mathtt{strength}$ function from
Definition 4.1. See Section D.1 for more details.

## References

  * [1] Samson Abramsky and Nikos Tzevelekos.  Introduction to categories and categorical logic.  New structures for physics, pages 3–94, 2011.
  * [2] Mikołaj Bojańczyk.  Recognisable languages over monads.  In International Conference on Developments in Language Theory, pages 1–13. Springer, 2015.
  * [3] Mikołaj Bojańczyk.  Languages recognised by finite semigroups, and their generalisations to objects such as trees and graphs, with an emphasis on definability in monadic second-order logic.  arXiv e-prints, pages arXiv–2008, 2020.
  * [4] Mikołaj Bojańczyk and Wojciech Czerwiński.  An automata toolbox.  URL: https://www. mimuw. edu. pl/~ bojan/papers/toolbox.pdf, 2018\.
  * [5] Mikołaj Bojańczyk, Sandra Kiefer, and Nathan Lhote.  String-to-string interpretations with polynomial-size output.  arXiv preprint arXiv:1905.13190, 2019.
  * [6] Mikołaj Bojańczyk, Bartek Klin, and Julian Salamanca.  Monadic monadic second order logic.  In Samson Abramsky on Logic and Structure in Computer Science and Beyond, pages 701–754. Springer, 2023.
  * [7] Mikołaj Bojańczyk and Lê Thành Dũng Nguyên.  Algebraic recognition of regular functions.  In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023), number 261, pages 117–1. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2023.
  * [8] Mikołaj Bojańczyk.  Recognisable languages over monads, 2015.  arXiv:1502.04898.
  * [9] Olivier Carton, Thomas Colcombet, and Gabriele Puppis.  An algebraic approach to mso-definability on countable linear orderings.  The Journal of Symbolic Logic, 83(3):1147–1189, 2018.
  * [10] Thomas Colcombet, Gaëtan Douéneau-Tabot, and Aliaume Lopez.  Z-polyregular functions.  In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–13. IEEE, 2023.
  * [11] Luc Dartois, Paulin Fournier, Ismaël Jecker, and Nathan Lhote.  On reversible transducers.  arXiv preprint arXiv:1702.07157, 2017.
  * [12] Hossep Dolatian and Jeffrey Heinz.  Learning reduplication with 2-way finite-state transducers.  In International Conference on Grammatical Inference, pages 67–80. PMLR, 2019.
  * [13] Samuel Eilenberg.  Automata, languages, and machines, volume A.  Academic press, 1974.
  * [14] Emmanuel Filiot, Ismaël Jecker, Christof Löding, and Sarah Winter.  A rational and complete notion of delay for streaming string transducers.  arXiv preprint arXiv:2205.04287, 2022.
  * [15] Sebastian Fischer, Zhenjiang Hu, and Hugo Pacheco.  A clear picture of lens laws: Functional pearl.  In Mathematics of Program Construction: 12th International Conference, MPC 2015, Königswinter, Germany, June 29–July 1, 2015. Proceedings 12, pages 215–223. Springer, 2015.
  * [16] J Nathan Foster, Michael B Greenwald, Jonathan T Moore, Benjamin C Pierce, and Alan Schmitt.  Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem.  ACM Transactions on Programming Languages and Systems (TOPLAS), 29(3):17–es, 2007.
  * [17] Bartek Klin.  Bialgebras for structural operational semantics: An introduction.  Theoretical Computer Science, 412(38):5043–5069, 2011.
  * [18] Kenneth Krohn and John Rhodes.  Algebraic theory of machines. i. prime decomposition theorem for finite semigroups and machines.  Transactions of the American Mathematical Society, 116:450–464, 1965.
  * [19] George H Mealy.  A method for synthesizing sequential circuits.  The Bell System Technical Journal, 34(5):1045–1079, 1955.
  * [20] Bartosz Milewski.  Category theory for programmers.  Blurb, 2018.
  * [21] Eugenio Moggi.  Notions of computation and monads.  Information and computation, 93(1):55–92, 1991.
  * [22] Dominic Orchard.  Programming contextual computations.  Technical report, University of Cambridge, Computer Laboratory, 2014.
  * [23] Jean-Éric Pin.  Mathematical foundations of automata theory.  Lecture notes LIAFA, Université Paris, 7:73, 2010.
  * [24] Marcel Paul Schützenberger.  On finite monoids having only trivial subgroups.  Inf. Control., 8(2):190–194, 1965.
  * [25] Dana Scott.  Some definitional suggestions for automata theory.  Journal of Computer and System Sciences, 1(2):187–212, 1967.
  * [26] The Coq Development Team.  The Coq reference manual – release 8.18.0.  https://coq.inria.fr/doc/V8.18.0/refman, 2023.
  * [27] Daniele Turi and Gordon Plotkin.  Towards a mathematical operational semantics.  In Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, pages 280–291. IEEE, 1997.

##  Appendix A Omitted details from Section 2

###  A.1 Monad axioms

Let us present the omitted axioms of a monad: First, both $\eta$ and $\mu$
should be natural. In this particular case, this means that the following two
diagrams should commute171717 We hope that the notation of commutative
diagrams is self-explanatory. See [1, Section 1.1.3] for a formal description.
: for every function $f:X\to Y$ (for the general definition of naturality, see
[1, Definition 1.4.1] or [20, Section 10]):

${{M\,M\,X}}$${{M\,X}}$${X}$${{M\,X}}$${{M\,M\,Y}}$${{M\,Y}}$${Y}$${{M\,Y}}$$\scriptstyle{\mu_{X}}$$\scriptstyle{M(M\,f)}$$\scriptstyle{M\,f}$$\scriptstyle{\mu_{Y}}$$\scriptstyle{f}$$\scriptstyle{M\,f}$$\scriptstyle{\eta_{X}}$$\scriptstyle{\eta_{Y}}$

In addition to being natural, $\eta$ and $\mu$ should make the following
diagrams commute:

${{M\,M\,M\,X}}$${{M\,M\,X}}$${{M\,X}}$${{M\,M\,X}}$${{M\,M\,X}}$${{M\,X}}$${{M\,M\,X}}$${{M\,X}}$$\scriptstyle{\mu_{MX}}$$\scriptstyle{\mu_{X}}$$\scriptstyle{\mu_{X}}$$\scriptstyle{M\mu_{X}}$$\scriptstyle{\eta_{MX}}$$\scriptstyle{\mu_{X}}$id$\scriptstyle{M\,\eta_{X}}$$\scriptstyle{\mu_{X}}$

##  Appendix B Omitted details from Section 3

###  B.1 Comonad axioms

Let us present the omitted axioms of a comonad. First, both $\varepsilon$ and
$\delta$ have to be natural, i.e. for every $f:X\to Y$ they have to satisfy
the following commutative equations:

${{M\,X}}$${{M\,M\,X}}$${{M\,X}}$${X}$${{M\,Y}}$${{M\,M\,Y}}$${{M\,Y}}$${Y}$$\scriptstyle{Mf}$$\scriptstyle{M(Mf)}$$\scriptstyle{\delta_{X}}$$\scriptstyle{\delta_{Y}}$$\scriptstyle{M\,f}$$\scriptstyle{\varepsilon_{X}}$$\scriptstyle{\varepsilon_{Y}}$$\scriptstyle{f}$

In addition to being natural, $\delta$ and $\varepsilon$ should make the
following diagrams commute:

${{M\,X}}$${{M\,M\,X}}$${{M\,X}}$${{M\,M\,X}}$${{M\,M\,X}}$${{M\,M\,M\,X}}$${{M\,M\,X}}$${{M\,X}}$$\scriptstyle{\delta_{X}}$$\scriptstyle{\delta_{X}}$$\scriptstyle{\delta_{MX}}$$\scriptstyle{M\,\delta_{X}}$$\scriptstyle{\delta_{X}}$$\scriptstyle{\delta_{X}}$$\scriptstyle{M\,\varepsilon_{X}}$$\scriptstyle{\varepsilon_{MX}}$id

###  B.2 Mealy machines

Mealy machines are one of the most basic, and very well-studied models of
transducers. They were introduced by [19]. In this section, we give a full
definition of Mealy machines, and show that they are equivalent to
$\overrightarrow{L}$-definable transductions.

######  Definition B.1.

Let $\Sigma$ and $\Gamma$ be finite alphabets. A _Mealy machine_ of type
$\Sigma^{+}\to\Gamma^{+}$ consists of:

  1. 1.

a finite set of states $Q$;

  2. 2.

an initial state $q_{0}\in Q$; and

  3. 3.

a transition function:

$\delta:\underbrace{Q}_{\textrm{current
state}}\times\underbrace{\Sigma}_{\textrm{input
letter}}\to\underbrace{Q}_{\textrm{new
state}}\times\underbrace{\Gamma}_{\textrm{output letter}}$

(Observe that contrary to a deterministic Mealy machine does not have
accepting states.)

A Mealy machine defines the following function181818 Usually the type of a
Mealy machine’s function is defined as $\Sigma^{*}\to\Gamma^{*}$. However,
this does not make much difference. This is because Mealy machines are a
length preserving model, so for the empty input they always return the empty
output, and for a non-empty input they always return a non-empty output. It
follows that the function $\Sigma^{*}\to\Gamma^{*}$ is uniquely defined by the
function $\Sigma^{+}\to\Gamma^{+}$.  $\Sigma^{+}\rightarrow\Gamma^{+}$. It
starts in the initial state, and processes the input word letter by letter.
For each symbol $w_{i}$, the machine transitions to a new state $q^{\prime}$
and outputs a symbol $x\in\Gamma$, as directed by the transition function
$\delta(q,w_{i})=(q^{\prime},x)$. When the machine has processed it entire
input, the output word is obtained as the sequence of all letters from
$\Gamma$ calculated by the machine.

For example, here is a Mealy machine of type $\\{a,b\\}^{+}\to\\{c,d\\}^{+}$
that calculates the function “Change the first $a$ to $c$, and all other
letters to $d$”:

######  Lemma B.2.

The class of transductions recognized by Mealy machines is equivalent to
$\overrightarrow{L}$-recognizable transductions.

######  Proof B.3.

$\subseteq$: As explained in Section 3.1, every
$\overrightarrow{L}$-recognizable transduction is given by a semigroup $S$, an
input function $h:\Sigma\to S$ and an output function $S\to\Gamma$. Such a
transduction computes the following function:

$\underbrace{a_{1}\ a_{2}\ \ldots\ a_{n}}_{\Sigma^{+}}$ | $\mapsto$ | $\underbrace{\lambda\left(h(a_{1})\right),\ \lambda\left(h(a_{1})\cdot h(a_{2})\right),\ \ldots,\ \lambda\left(h(a_{1})\cdot\ldots\cdot h(a_{n})\right)}_{\Gamma^{+}}$
---|---|---

Let us show how to translate such a transduction into a Mealy machine: We
start by extending the semigroup $S$ to a monoid $S^{I}=S\cup\\{1\\}$, where
$1$ the formal identity element (i.e. $1\cdot x=x\cdot 1=x$ for every $x\in
S^{I}$). Now we say the set of states of the Mealy machine is equal to
$S^{\prime}$, its initial state is $1$, and its transition function is given
by the following formula:

$\delta(s,a)=(s\cdot h(a),\lambda(s\cdot h(a)))$

This way the Mealy machine computes the $S$-products of the $h$-values of the
input prefixes, and outputs their $\lambda$-values, computing the same
function as the original $\overrightarrow{L}$-recognizable transduction.

$\supseteq$: Now, we are given a Mealy machine of type
$\Sigma^{+}\to\Gamma^{+}$ given by $(Q,q_{0},\delta)$, and we want to
construct $(S,h,\lambda)$, such that the $\overrightarrow{L}$-transduction
given by $(S,h,\lambda)$ is equivalent to the initial Mealy machine. For this
purpose let us define the behaviour of an infix $w\in\Sigma^{+}$, which is an
element from the following set:

$S=\underbrace{Q}_{\begin{subarray}{c}\textrm{The state in which}\\\
\textrm{the Mealy machine enters}\\\ \textrm{the infix from the
left}\end{subarray}}\to\underbrace{Q}_{\begin{subarray}{c}\textrm{The state in
which}\\\ \textrm{the Mealy machine exists}\\\ \textrm{the infix from the
right}\end{subarray}}\times\underbrace{\Gamma}_{\begin{subarray}{c}\textrm{The
letter that}\\\ \textrm{the Mealy machine outputs}\\\ \textrm{while exiting
the infix}\end{subarray}}$

Observe that those behaviours are compositional, if we know that the
behaviours of words $w,v\in\Sigma^{+}$ are equal respectively to $f_{w}$ and
$f_{v}$, then we know that the behaviour of $wv$ is equal to the following
function:

$f_{wv}(q)=f_{v}(\pi_{1}(f_{w}(q)))\textrm{,}$

where $\pi_{1}:X\times Y\to X$ represents the projection to the first
coordinate. This gives us a semigroup structure on the set of behaviours
(where $f\cdot g$ is defined as $g\circ\pi_{1}\circ f$). We take this monoid
of behaviours as our semigroup $S$. Then, we define $h:\Sigma\to S$ and
$\lambda:S\to\Gamma$ in the following way:

$h(a)=q\mapsto\delta(q,a)$ | $\lambda(f)=\pi_{2}(f(q_{0}))$
---|---

This way, the $\overrightarrow{L}$ transduction given by $(S,h,\lambda)$
computes the behaviour of each prefix, and outputs the letter that the machine
would output if it entered the prefix in $q_{0}$. It is not hard to see that
this computes the same function as the original Mealy machine.

###  B.3 Rational length-preserving transductions

In this section, we present the definition of _rational length-preserving_
transductions. We define them using _unambiguous Mealy machines_
191919Although, we could not find a reference to this exact model in the
literature, we believe that it belongs to the field’s folklore, as it can be
seen as a length-preserving version of the functional NFA with output (see
[13, Chapter 25], or [4, Section 13.2]). and show that they are equivalent to
$\bar{L}$-definable transductions.

######  Definition B.4.

Let $\Sigma$ and $\Gamma$ be finite alphabets. A _nondeterministic Mealy
machine_ of type $\Sigma^{+}\to\Gamma^{+}$ consists of:

  1. 1.

A finite set of states $Q$.

  2. 2.

A subset $I\subseteq Q$ of initial states, and a subset $F\subseteq Q$ of
final (i.e. accepting) states.

  3. 3.

A transition relation:

$\delta:\underbrace{Q}_{\textrm{current
state}}\times\underbrace{\Sigma}_{\textrm{input
letter}}\times\underbrace{Q}_{\textrm{new
state}}\times\underbrace{\Gamma}_{\textrm{output letter}}$

A _run_ of a nondeterministic Mealy machine over an input word
$w\in\Sigma^{+}$ is a sequence of states, starting from an initial state
$q_{0}\in I$, and ending in a final state $q_{n}\in F$, such that for each
symbol $w_{i}$ of $w$, there is a transition in $\delta$ that reads $w_{i}$
and takes the machine from state $q_{i-1}$ to state $q_{i}$. Observe that each
run produces an output word in $\Gamma^{+}$. The machine is called
_unambiguous_ if, for every input word $w\in\Sigma^{+}$, there exists
_exactly_ one run. The transduction defined by an unambiguous Mealy machine is
a function $\Sigma^{+}\to\Gamma^{+}$ that maps a word $w\in\Sigma^{+}$ to the
output of the machine’s only run for $w$. (Observe that the unambiguity of the
machine guarantees that for every input, there is exactly one output, despite
the machine’s nondeterministic transition relation.)

For example, here is an unambiguous Mealy machine of type
$\\{a,b\\}^{+}\to\\{a,b\\}^{+}$ that computes the function “replace the first
letter with the last one”:

Observe now that there is a slight type mismatch between the types of rational
length-preserving transductions and $\overline{L}$-definable transductions.
The former are of the type $\Sigma^{+}\to\Gamma^{+}$, and the latter of type
$\bar{L}(\Sigma)\to\bar{L}(\Gamma)$. To deal with this mismatch, we notice
that all $\overline{L}$-definable transductions satisfy the following property
(this is an immediate consequence of the definition of $\bar{L}$-definable
transductions):

######  Definition B.5.

We say that a length-preserving function $f:\bar{L}X\to\bar{L}Y$ is
_underline-independent_ if:

  1. 1.

For every $v\in\bar{L}$, the underlying word of $f(v)$ does not depend on the
position of the underline in $w$, i.e. for every $w\in X^{+}$:

$\mathtt{forget}(f(\mathtt{underline}_{i}(w)))=\mathtt{forget}(f(\mathtt{underline}_{j}(w)))\textrm{,}$

where $\mathtt{underline}_{i}$ is the function that underlines the $i$th
element of the input, and $\mathtt{forget}$ is the function that casts a
pointed list into a normal list (by erasing the underline).

  2. 2.

For every $v\in\bar{L}$ the index of the underlined position in $v$ is equal
to the index of the underlined position in $f(v)$.

Observe now that the following function is a bijection between length-
preserving, underline-independent functions
$\bar{L}(\Sigma)\to\bar{L}(\Gamma)$ and length-preserving functions
$\Sigma^{+}\to\Gamma^{+}$:

$\phi(f)=\mathtt{forget}\circ f\circ\mathtt{underline}_{1}$

From now on, we are going to use this bijection implicitly, equating the two
types of functions.

Next, let us show that unambiguous Mealy machines are equivalent to
$\bar{L}$-definable transductions. We start with the proof of Lemma 3.5 (the
lemma and its proof are based on [8, Section 8.1]):

######  Lemma 3.5.

For every $\bar{L}$-algebra $(A,\alpha)$, there are two monoids $M_{L}$ and
$M_{R}$, together with functions $h_{L}:A\to M_{L}$, $h_{R}:A\to M_{R}$, such
that the value of every $A$-product

$\alpha([a_{1},\ldots,\underline{a_{i}},\ldots,a_{n}])$

depends only on:

  1. 1.

the $M_{L}$-product of the prefix (i.e. $h_{L}(a_{1})\cdot\ldots\cdot
h_{L}(a_{i-1})$),

  2. 2.

the $M_{R}$-product of the suffix (i.e. $h_{R}(a_{i+1})\cdot\ldots\cdot
h_{R}(a_{n})$), and

  3. 3.

the exact $A$-value of the underlined element ($a_{i}$).

Moreover, if $A$ is finite then both $M_{L}$ and $M_{R}$ are finite as well.

######  Proof B.6.

For every element $a\in A$, we define its _left transformation_ to be the
following function of type $A\to A$:

$x\mapsto\alpha([a,\underline{x}])$

Observe that the set of all left transformations equipped with function
composition forms a monoid. This is because, thanks to the associativity
axiom, the left behaviour of $\alpha{[x,\underline{y}]}$ is equal to the
composition of left behaviours of $x$ and $y$. We define $M_{L}$ to be the
monoid of left transformations, and $h_{L}$ to be the function that maps
elements of $A$ to their left behaviours. Values $M_{R}$ and $h_{L}$ are
defined analogously, but for _right behaviours_. Observe that the value

$\alpha[a_{1},\ldots,\underline{a_{i}},\ldots,a_{n}]$

can be computed as $s(p(a_{i}))$, where $p$ is the $M_{L}$ product of the
prefix, and $s$ is the $M_{R}$ product of the suffix (as defined in the
statement).

We are now ready to prove the equivalence of nondeterministic Mealy-machines
and $\bar{L}$-definable transductions:

######  Lemma B.7.

The class of transductions computed by unambiguous Mealy machines is equal to
$\bar{L}$-definable transductions.

######  Proof B.8.

$\subseteq$: A $\bar{L}$ definable transduction is given by a
$\bar{L}$-algebra $(A,\alpha)$, an input function $h:\Sigma\to S$ and an
output function $\lambda:A\to\Gamma$. The $i$-th letter of the output is then
computed as
$\lambda(\alpha([h(w_{1}),\ldots,\underline{h(w_{i})},\ldots,w_{n}]])$. By
Lemma 3.5, we know that there are two monoids $M_{R}$, $M_{L}$, and functions
$h_{R}$, $h_{L}$, $g$, such that this can be computed as
$g(p_{L},h(w_{i}),s_{R})$, where $p_{L}=h^{\prime}_{L}(w_{1})\cdot\ldots
s_{R}=h^{\prime}_{L}(w_{i-1})$ and
$p_{R}=h^{\prime}_{R}(w_{i+1})\cdot\ldots\cdot h^{\prime}_{R}(w_{n})$, for
$h^{\prime}_{L}=h_{L}\circ h$ and $h^{\prime}_{R}=h_{R}\circ h$. Based on this
observation we can define an unambiguous Mealy machine. Intuitively the
machine is going to remember in its state the $M_{L}$-product of the prefix
and the $M_{R}$-product of the suffix, and it is going to use $g$ to compute
the output letters. Formally, the machine’s set of states is equal to
$M_{L}\times M_{R}$, its initial states are $\\{1\\}\times M_{R}$ and its
final states are $M_{L}\times\\{1\\}$. Finally, its transition function
consists of the following tuples, for every $m_{L}\in M_{L}$, $m_{R}\in
M_{R}$, and $x\in\Sigma$:

$(\underbrace{(m_{L},\,m_{R}\cdot h^{\prime}_{R}(x))}_{\textrm{previous
state}},\underbrace{x}_{\textrm{input letter}},\underbrace{(m_{L}\cdot
h^{\prime}_{L}(x),\,m_{R})}_{\textrm{next state}},\
\underbrace{g(m_{L},\,h(x),\,m_{R})}_{\textrm{output letter}})$

Thanks to this definition, we know that the only correct run for an input
$w\in\Sigma^{*}$ is the run that correctly evaluates the monoid products for
all prefixes and suffixes. It follows that the machine is unambiguous, and
correctly computes the output of the original $\bar{L}$-transduction.

$\supseteq$: Now, we are given an unambiguous Mealy machine
$\Sigma^{+}\to\Gamma^{+}$ defined by some $(Q,I,F,\delta)$, and we show how to
transform it into a $\bar{L}$-definable transduction. We start by defining the
transition semigroup for the Mealy machine. It consists of behaviours, which
are analogous to the deterministic behaviours from Lemma B.2, but are
relations instead of functions, and they ignore the output letter (in other
words, it is the transition monoid for the underlying NFA, as defined e.g. in
[23, IV.3.2]):

$M=\underbrace{Q}_{\begin{subarray}{c}\textrm{The state in which}\\\
\textrm{the Mealy machine enters}\\\ \textrm{the infix from the
left}\end{subarray}}\times\underbrace{Q}_{\begin{subarray}{c}\textrm{The state
in which}\\\ \textrm{the Mealy machine exists}\\\ \textrm{the infix from the
right}\end{subarray}}$

The product operation in $M$ is simply the composition of relations: $f\cdot
g=g\circ f$. Let us now use $M$ to define the $\bar{L}$-algebra $(A,\alpha)$.
We start with the underlying set $A=M\times\Sigma\times M$. Before we define
the product operation, let us show how to cast element of $A$ to $M$:

$t(m_{1},a,m_{2})=m_{1}\cdot\delta(a)\cdot m_{2}\textrm{,}$

where $\delta(a):Q\times Q$ is the partial application of the transition
relation (which computes the behaviour for the single letter $a$). We are now
ready to define the product:

$\alpha([(p_{1},a_{1},s_{1}),\ldots,\underline{(p_{i},a_{i},s_{i})},\ldots(p_{n},a_{n},s_{n})])$
---
$=$
$\left(t(p_{1},a_{1},s_{1})\cdot\ldots\cdot t(p_{i-1},a_{i-1},s_{i-1})\cdot
p_{i},\ \ a_{i},\ \ s_{i}\cdot t(p_{i+1},a_{i+1},s_{i+1})\cdot
t(p_{n},a_{n},s_{n})\right)$

It is not hard that this $\alpha$ satisfies the algebra axioms (the singleton-
mult axiom is straightforward, and the associativity axiom follows from the
associativity of $M$). Next, we define $h:\Sigma\to A$ as $h(a)=(1,a,1)$.
Finally, we define $\lambda:A\to\Gamma$, in the following way:
$\lambda(p,a,s)=b$, if there is a transition $q\stackrel{{\scriptstyle
a/b}}{{\longrightarrow}}q^{\prime}$, an initial state $q_{0}$ and a final
state $q_{n}$ such that $(q_{0},q)\in p$ and $(q^{\prime},q_{n})\in s$. Thanks
to the unambiguity of the Mealy machine, we know that $\lambda$ is well-
defined. We finish the proof by noting that the $\bar{L}$-transduction defined
by $(A,\alpha)$, $h$ and $\lambda$ is by design equivalent to the original
Mealy machine.

##  Appendix C Omitted details from Section 4

###  C.1 Naturality of $\mathtt{put}$

The naturality of $\mathtt{put}$ means that for every function $f:X\to Y$, the
following diagram commutes (for the general definition of naturality, see [1,
Definition 1.4.1] or [20, Section 10]):

${{MX\times X}}$${{MX}}$${{MY\times
Y}}$${{MY}}$$\scriptstyle{\mathtt{put}}$$\scriptstyle{(Mf)\times
f}$$\scriptstyle{\mathtt{put}}$$\scriptstyle{Mf}$

###  C.2 The flatten-expand axiom

In this section we give a step-by-step example of the flatten-expand axiom for
$M=\overrightarrow{L}$, we start by restating the axiom:

${{MMMA}}$${{MMMA}}$${{MMA}}$${{MMA}}$${{MA}}$$\scriptstyle{\mu_{A}}$$\scriptstyle{\delta_{A}}$$\scriptstyle{\mu_{MA}}$$\scriptstyle{\delta_{MA}}$$\scriptstyle{M\mathtt{work}}$

where $\mathtt{work}$ is defined as the following composition:

$MMA\stackrel{{\scriptstyle\langle\textrm{id},\varepsilon\rangle}}{{\longrightarrow}}MMA\times
MA\stackrel{{\scriptstyle\textrm{id}\times\delta}}{{\longrightarrow}}MMA\times
MMA\stackrel{{\scriptstyle\mathtt{strength}}}{{\longrightarrow}}M(MMA\times
MA)\stackrel{{\scriptstyle
M\mathtt{put}}}{{\longrightarrow}}MMMA\stackrel{{\scriptstyle
M\mu}}{{\longrightarrow}}MA$

For the purpose of our example, let us consider $A=\\{1,\ldots,7\\}$, and let
us consider the following input
$[[1,2],[3,4],[5,6,7]]\in\overrightarrow{L}\overrightarrow{L}A$. The bottom
path works as follows:

$[[1,2],[3,4],[5,6,7]]$
---
$\rotatebox[origin={c}]{-90.0}{$\scriptstyle\mapsto$}\mkern 2.0mu\,\mu$
$[1,2,3,4,5,6]$
$\rotatebox[origin={c}]{-90.0}{$\scriptstyle\mapsto$}\mkern 2.0mu\,\delta$
$[[1],[1,2],[1,2,3],[1,2,3,4],[1,2,3,4,5],[1,2,3,4,5,6],[1,2,3,4,5,6,7]]$

Now let us focus on the top path. Here is the first step:

$[[1,2],[3,4],[5,6,7]]\stackrel{{\scriptstyle\delta}}{{\longmapsto}}\left[[[1,2]],\
[[1,2],\,[3,4]],\ [[1,2],\,[3,4],\,[5,6,7]]\right]$

The next step in the top path is $M\,\mathtt{work}$ which applies the work
function in parallel to all elements of the top list. Let us show, how it
works on the last element, i.e. on $[[1,2],[3,4],[5,6,7]]$:

$\Big{[}[1,2],[3,4],[5,6,7]\Big{]}$
---
$\rotatebox[origin={c}]{-90.0}{$\scriptstyle\mapsto$}\mkern 2.0mu\,\langle
id,\varepsilon\rangle$
$\left(\Big{[}[1,2],[3,4],[5,6,7]\Big{]},[5,6,7]\right)$
$\rotatebox[origin={c}]{-90.0}{$\scriptstyle\mapsto$}\mkern
2.0mu\,id\times\delta$
$\left(\Big{[}[1,2],[3,4],[5,6,7]\Big{]},\Big{[}[5],[5,6],[5,6,7]\Big{]}\right)$
$\rotatebox[origin={c}]{-90.0}{$\scriptstyle\mapsto$}\mkern
2.0mu\,\mathtt{strength}$
$\left[\biggl{(}\bigl{[}[1,2],[3,4],[5,6,7]\bigr{]},[5]\biggr{)},\biggl{(}\bigl{[}[1,2],[3,4],[5,6,7]\bigr{]},[5,6]\biggr{)},\biggl{(}\bigl{[}[1,2],[3,4],[5,6,7]\bigr{]},[5,6,7]\biggr{)}\right]$
$\rotatebox[origin={c}]{-90.0}{$\scriptstyle\mapsto$}\mkern
2.0mu\,M\mathtt{put}$
$\biggl{[}\Bigl{[}[1,2],[3,4],[5]\Bigr{]},\Bigl{[}[1,2],[3,4],[5,6]\Bigr{]},\Bigl{[}[1,2],[3,4],[5,6,7]\Bigr{]}\biggr{]}$
$\rotatebox[origin={c}]{-90.0}{$\scriptstyle\mapsto$}\mkern 2.0mu\,M\mu$
$\Bigl{[}[1,2,3,4,5],[1,2,3,4,5,6],[1,2,3,4,5,6,7]\Bigr{]}$

In a similar fashion one can compute $\mathtt{work}$ for the other sublists:

$[[1,2]]$ | $\stackrel{{\scriptstyle\mathtt{work}}}{{\longmapsto}}$ | $[[1],[1,2]]$
---|---|---
$[[1,2],[3,4]]$ | $\stackrel{{\scriptstyle\mathtt{work}}}{{\longmapsto}}$ | $[[1,2,3],[1,2,3,4]]$
$[[1,2],[3,4],[5,6,7]]$ | $\stackrel{{\scriptstyle\mathtt{work}}}{{\longmapsto}}$ | $[[1,2,3,4,5],[1,2,3,4,5,6],[1,2,3,4,5,6,7]]$

Using those results of $\mathtt{work}$, we can trace the top path of the
diagram:

$\Bigl{[}[1,2],[3,4],[5,6,7]\Bigr{]}$
---
$\rotatebox[origin={c}]{-90.0}{$\scriptstyle\mapsto$}\mkern 2.0mu\,\delta$
$\Bigl{[}\bigl{[}[1,2]\bigr{]},\bigl{[}[1,2],[3,4]\bigr{]},\bigl{[}[1,2],[3,4],[5,6,7]\bigr{]}\Bigr{]}$
$\rotatebox[origin={c}]{-90.0}{$\scriptstyle\mapsto$}\mkern
2.0mu\,M\mathtt{work}$
$\Bigl{[}\bigl{[}[1],[1,2]\bigr{]},\ \bigl{[}[1,2,3],[1,2,3,4]\bigr{]},\
\bigl{[}[1,2,3,4,5],[1,2,3,4,5,6],[1,2,3,4,5,6,7]\bigr{]}\Bigr{]}$
$\rotatebox[origin={c}]{-90.0}{$\scriptstyle\mapsto$}\mkern 2.0mu\,\mu$
$\Bigl{[}[1],[1,2],[1,2,3],[1,2,3,4],[1,2,3,4,5],[1,2,3,4,5,6],[1,2,3,4,5,6,7]\Bigr{]}$

Which means that both in the top and in the bottom path, we obtain the same
result.

###  C.3 Flatten-expand axiom as bialgebra

In this section, we show how to describe the flatten-expand axiom in the
language of _bialgebras_. We start with the definition of _coalgebras_ for a
comonad (which is the dual of Definition 2.6):

######  Definition C.1.

A _coalgebra_ for a comonad $W$ is a set $S$ together with a multiplication
function $\beta:S\to WS$, that makes the following diagrams commute:

${S}$${{WWS}}$${S}$${{WS}}$${WS}$${{WWS}}$${{S}}$$\scriptstyle{\beta}$$\scriptstyle{\beta}$$\scriptstyle{W\beta}$$\scriptstyle{\delta}$$\scriptstyle{\beta}$$\scriptstyle{\varepsilon}$$\scriptstyle{id}$

We are now ready to present the definition of a bialgebra202020 Defined in
[27, Section 7.2]. See also [17]. :

######  Definition C.2.

Let $M$ be a monad, and $W$ be a comonad. A $(M,W)$-bialgebra is a set $S$
equipped with three functions:

$\alpha:MS\to S$ | $\beta:S\to MS$ | $\gamma:MWS\to WMS$
---|---|---

Such that $(S,\alpha)$ is an $M$-algebra, $(S,\beta)$ is a $W$-coalgebra, and
the following diagram commutes:

${{MWS}}$${{WMS}}$${{MS}}$${{WS}}$${S}$$\scriptstyle{\alpha}$$\scriptstyle{\beta}$$\scriptstyle{M\beta}$$\scriptstyle{M\alpha}$$\scriptstyle{\gamma}$

We are going to be intereseted in the case where the monad and the comonad is
the same functor $M$.

Observe now, that for every set $X$, the set $MX$ equipped with the $\mu$
operation forms an $M$-algebra, called the _free algebra_ over $X$. (In this
case the axioms of an algebra coincide with the axioms of a monad). Similarly,
the set $MX$ equipped with the $\delta$ operation, forms an $M$-coalgebra,
called _the free coalgebra_.

We are now ready to specify the flatten-expand axiom in terms of a bialgebra.
It states that for every $X$, the set $MX$ equipped with $\mu$ (i.e. the free
algebra structure), $\delta$ (i.e. the free coalgebra structure), and $\gamma$
defined as the following composition, is a bialgebra:

$\gamma:MMMX\stackrel{{\scriptstyle\delta}}{{\longrightarrow}}MMMMX\stackrel{{\scriptstyle
M\langle M\varepsilon,\varepsilon\rangle}}{{\longrightarrow}}M(MMX\times
MMX)\stackrel{{\scriptstyle
M\mathtt{strength}}}{{\longrightarrow}}MM(MMX\times MX)\stackrel{{\scriptstyle
MM\mathtt{put}}}{{\longrightarrow}}$ $\stackrel{{\scriptstyle
MM\mathtt{put}}}{{\longrightarrow}}MMMMX\stackrel{{\scriptstyle\mu}}{{\longrightarrow}}MMMX$

After unfolding the bialgebra definition, this means that the following
diagram commutes:

${{MMMX}}$${{MMMX}}$${{MMX}}$${{MMX}}$${{MX}}$$\scriptstyle{\mu}$$\scriptstyle{\delta}$$\scriptstyle{M\delta}$$\scriptstyle{M\mu}$$\scriptstyle{\gamma}$

Using basic equational reasoning, we can show that the top path in this
diagram is equal to the top path in the flatten-expand axiom. (This is
formalized as flattenExpandAltThm, see Section E.4.) It follows that the
bialgebraic formulation is equivalent to the flatten-expand axiom.

###  C.4 Omitted proofs from Section 4.2

######  Lemma 4.6.

For every $f,g\in C_{A}$, it holds that $f\circ g\in C_{A}$.

######  Proof C.3.

We start the proof by defining the following operation
$\mathtt{concat}:MA\times MA\to MA$:

$MA\times MA\stackrel{{\scriptstyle
M\eta_{A}\times\textrm{id}}}{{\longrightarrow}}MMA\times
MA\stackrel{{\scriptstyle\mathtt{put}_{MA}}}{{\longrightarrow}}MMA\stackrel{{\scriptstyle\mu_{A}}}{{\longrightarrow}}MA$

The intuition behind this operation is that it overrides the focused element,
with the given element of $MA$.

For more intuition, consider the following example in $\overrightarrow{L}$ and
observe that the element $3$ disappears:

$\mathtt{concat}([1,2,3],[4,5,6])=[1,2,4,5,6]$

In the setting of lists this _overriding_ behaviour might seem counter-
intuitive, as there already is a more natural definition of concatenation.
However, the overriding behaviour is clearly defined for all $M$s, and the
usual definition of concatenation does not seem to be generalizable (for
example for $M$’s such as $\bar{L}$ and $T_{\mathcal{S}}$). For example, in
$\bar{L}$, $\mathtt{concat}$ works as follows:

$\mathtt{concat}([1,\underline{2},3],[4,5,\underline{6}])=[1,4,5,\underline{6},2,3]$

Using the put-assoc axiom, one can show the context of concatenation is equal
to the composition of contexts (this is verified as concatCtx in Coq, see
Section E.3):

######  Lemma C.4.

For every $k,l\in MA$, it holds that:

$\mathtt{ctx}_{k}\circ\mathtt{ctx}_{l}=\mathtt{ctx}_{\mathtt{concat}(k,l)}$

This finishes the proof of the Lemma 4.6.

###  C.5 Wreath Product

In this section, we show how to compose two $\overrightarrow{L}$-transductions
using the usual definition of a _wreath product_ [18, Defnition 1.7]. This
serves two purposes: the first one is to relate the _generalized wreath
product_ from Section 4.3 with the classical wreath product, the second one is
to give more intuitions about the proof of Theorem 4.8.

Remember that a $\overrightarrow{L}$-transduction of type
$\Sigma^{+}\to\Gamma^{+}$ is given by a semigroup $S$, and functions
$h:\Sigma\to S$, $\lambda:S\to\Gamma$, and is computed according to the
following formula:

$w_{1}\ldots w_{n}\to\lambda(h(w_{1})),\ \ldots,\
\lambda(h(w_{1})\cdot\ldots\cdot h(w_{n}))$

We are given two $\overrightarrow{L}$-transductions
$F_{1}:\Sigma^{*}\to\Gamma^{*}$ and $F_{2}:\Gamma^{*}\to\Delta^{*}$, given by
$(S_{1},h_{1},\lambda_{1})$ and $(S_{2},h_{2},\lambda_{2})$, and we would like
to construct $(S_{3},h_{3},\lambda_{3})$, such that their
$\overrightarrow{L}$-transduction computes the composition
$\Sigma^{*}\stackrel{{\scriptstyle
F_{1}}}{{\longrightarrow}}\Gamma^{*}\stackrel{{\scriptstyle
F_{2}}}{{\longrightarrow}}\Delta^{*}$. As mentioned before, for $S_{3}$, we
are going to use the wreath product of $S_{1}$ and $S_{2}$.

The intuition behind $S_{3}$ is that it represents the $S_{1}$\- and
$S_{2}$-products for every possible infix. Before we define $S_{3}$, let us
show what it means to compute the $S_{2}$-product of an infix from
$\Sigma^{*}$. For example, consider the following infix $w\in\Sigma^{*}$:

unknown preffix | $a_{1}$ | $a_{2}$ | $a_{3}$ | $a_{4}$ | unknown suffix
---|---|---|---|---|---

In order to compute the $S_{2}$-product of $w$, we need to first transform it
using $F_{1}$. This is slightly problematic, as the output of $F_{1}$ will
usually depend on the unknown prefix that comes before $w$. However, the only
information we need about that prefix is its $S_{1}$-product. For example, if
we know that $S_{1}$-product of the prefix is equal to $s$, we can compute the
output of $F_{1}$ on $w$ as follows (where $s_{i}:=h_{1}(a_{i})$):

unknown preffix | $\lambda_{1}(s\cdot s_{1})$ | $\lambda_{1}(s\cdot s_{1}\cdot s_{2})$ | $\lambda_{1}(s\cdot s_{1}\cdot s_{2}\cdot s_{3})$ | $\lambda_{1}(s\cdot s_{1}\cdot s_{2}\cdot s_{3}\cdot s_{4})$ | unknown suffix
---|---|---|---|---|---

Now we can compute the $S_{2}$-product of $w$ by applying $h_{2}$ to each
letter and multiplying the results (in $S_{2}$):

$h_{2}(\lambda_{1}(s\cdot s_{1}))\cdot h_{2}(\lambda_{1}(s\cdot s_{1}\cdot
s_{2}))\cdot h_{2}(\lambda_{1}(s\cdot s_{1}\cdot s_{2}\cdot s_{3}))\cdot
h_{2}(\lambda_{1}(s\cdot s_{1}\cdot s_{2}\cdot s_{3}\cdot s_{4}))$

According to this reasoning, the $S_{2}$ value of an infix can be represented
as a function of the following type (where $S_{1}^{1}$ denotes $S_{1}$
adjoined with a formal identity element):

$\underbrace{S_{1}^{1}}_{\begin{subarray}{c}\textrm{Given the $S_{1}$-product
of the preffix}\\\ \textrm{(where $1$ represents the empty
preffix)}\end{subarray}}\to\underbrace{S_{2}}_{\begin{subarray}{c}\textrm{What
is the $S_{2}$-product of the infix?}\end{subarray}}$

We are now ready to define $S_{3}$ as the following set:

$\underbrace{S_{1}}_{\begin{subarray}{c}\textrm{The $S_{1}$-value of the
infix}\end{subarray}}\times\underbrace{S_{1}^{1}\to
S_{2}}_{\begin{subarray}{c}\textrm{The $S_{2}$-value of the infix}\\\
\textrm{as explained above}\end{subarray}}$

The product operation on $S_{3}$ is defined with the following formula, which
follows from our definition of the $S_{2}$-values:

$(s,f)\cdot(t,h)=(s\cdot t,\ x\mapsto f(x)\cdot g(x\cdot s))$

It is now not hard to see that $S_{3}$ equipped with the following $h_{3}$ and
$\lambda_{3}$ recognizes the composition $F_{2}\circ F_{1}$:

$h(a)=\left(\;h_{1}(a),\ x\mapsto h_{2}\left(\lambda_{1}\bigl{(}x\cdot
h_{1}(a)\bigr{)}\right)\;\right)$
---
$\lambda(x,f)=\lambda_{2}(f(1))$

Let us finish this section by comparing this definition of a wreath product,
with our definition of the _generalized wreath product_ from Section 4.3,
where it is defined as:

$S_{1}\times(S_{1}^{S_{1}}\to S_{2})$

Remember that the set $S_{1}^{S_{1}}$ is meant to represent $S_{1}$-contexts,
so we can think of this type as $S_{1}\times(C_{S_{1}}\to S_{2})$. (Actually,
this is how we could have defined the _generalized wreath product_ from the
beginning. We used the more general definition for the sake of simplifying the
definition of the product, and the (formal) proof of associativity, but we
believe that this finer definition would work as well). Since, as explained in
Section 4.2, for $M=\overrightarrow{L}$ the set of contexts $C_{S}$ is
isomorphic to $S^{1}$, this can be further simplified to
$S_{1}\times(S_{1}^{1}\to S_{2})$, which coincides with the definition of the
_wreath product_ presented in this section.

##  Appendix D Omitted details from Section 5

###  D.1 General Cartesian closed categories

In this section we discuss possible strategies and obstacles for generalizing
the results of this paper from Set to arbitrary _Cartesian closed categories_.
We say that a category is called _Cartesian closed_ if it admits products
$X\times Y$ and function spaces $X\Rightarrow Y$ (see [1, Definition 78] for
the full definition).

As it turns out, our Coq-formalization of the results mostly uses a subset of
$\lambda$-calculus that can be automatically translated into morphism in every
Cartesian closed category (see [1, Section 1.6.5]). The only exception is the
function $\mathtt{strength}$, which is defined in the following way:

$\mathtt{strength}(x,l)=\left(M\,(\lambda y.(x,y))\right)\ l$

This causes problems, because in the Cartesian closed categories, the functor
$M$ can only be applied to arrows of the category (i.e. $X\to Y$) and not to
the exponent objects (i.e. $X\Rightarrow Y$). (In particular, not every
functor in every Cartesian closed category has a _strength_.)

One way to deal with this problem is to require that the functor $M$ should
come equipped with a $\mathtt{strength}$ (smilarly to how it comes equipped
with a $\mathtt{put}$ function), and axiomatize its expected behaviour. We
have tried this approach with the usual axioms of a _strong functor_ , _strong
monad_ , and a _strong comonad_ 212121We took the axioms of a strong functor
and a strong monad from [21, Definition 3.2]. For the axioms of a strong
comonad, we took the duals of the axioms for a strong monad., but we were not
able to prove Theorem 4.8 within this axiomatization. Here is an example of a
rather basic property, that does not seem to follow from this usual set of
axioms:

${{MX}}$${{(X\Rightarrow X)\times MX}}$${{M((X\Rightarrow X)\times
X)}}$${{MX}}$$\scriptstyle{id}$$\scriptstyle{\langle\mathtt{const_{id}},id\rangle}$$\scriptstyle{\mathtt{strength}}$$\scriptstyle{M\mathtt{eval}}$

In the diagram $\mathtt{eval}:(Y\Rightarrow X)\times Y\to X$ denotes the
function application (from the definition of a Cartesian closed category), and
$\mathtt{const_{id}}:Z\to(X\Rightarrow X)$ denotes an arrow that maps every
argument to the identity function (formally, this is defined as
$\mathtt{const_{id}}=\Lambda(\pi_{2})$, where $\Lambda$ comes from the
definition of a Cartesian closed category and $\pi_{2}:Z\times X\to X$ is the
second projection).

Next, we tried adding this diagram as one of the axioms and proving Theorem
4.8. However we have encountered other problems. So, for the sake of
simplicity, we have decided to restrict the scope of this paper to Set.
However, we believe that it should be possible to find an axiomatization of
$\mathtt{strength}$ that would admit a proof of Theorem 4.8. Moreover, it is
possible that such an axiomatization already exists in the literature and we
were simply not able to find it. We would welcome any suggestion of such an
axiomatization.

##  Appendix E Formalization in Coq

In this section, we present the framework of our Coq formalization, focusing
on key definitions and the statements of main lemmas. To streamline our
exposition, we exclude the formal proofs, and certain auxiliary lemmas deemed
peripheral to our core arguments. The entire Coq file is available under the
following link222222 https://github.com/ravst/MonadsComonadsTransducersCoq .

###  E.1 Modelling

In this section, we show how we have modelled our theory in Coq. We start by
fixing the functor $M$:

⬇

Parameter M : Type $\rightarrow\;$ Type.

Parameter mapM : forall {A} {B}, (A $\rightarrow\;$ B) $\rightarrow\;$ M A
$\rightarrow\;$ M B.

Notation " # f " := (mapM f).

Here mapM is the mapping on sets, and mapM is the mapping on functions. We
also introduce a notation for the mapping on sets, where $Mf$ is written as
$\mathtt{\\#f}$. Next, we assert the axioms of a functor:

⬇

Axiom mapCompose : forall {A} {B} {C} (f : B $\rightarrow\;$ C) (g : A
$\rightarrow\;$ B) (mx : M A),

(#f)((#g) mx) = (#(compose f g)) mx.

Axiom mapId : forall {A} (x : M A), (# id) x = x.

In a similar fashion, we assert the monad structure on $M$:

⬇

(*Flatten operation*)

Parameter mult : forall {A}, M (M A) $\rightarrow\;$ M A.

(*Singleton operation*)

Parameter unit : forall {A}, A $\rightarrow\;$ M A.

(*Monad operations are natural*)

Axiom multNatural : forall A B, forall f : A $\rightarrow\;$ B, forall x,

mult((#(#f)) x) = (#f)(mult x).

Axiom unitNatural : forall A B, forall f : A $\rightarrow\;$ B, forall x,

unit(f x) = (#f)(unit x).

(*Monad operations satisfy monad axioms*)

Axiom multAx : forall A (x : M (M (M A))),

mult (mult x) = mult ((#mult) x).

Axiom multMapUnitAx : forall A (x : M A),

mult ((# unit) x) = x.

Axiom multUnitAx : forall A (x : M A),

mult (unit x) = x.

Next, we assert the comonad structure on $M$:

⬇

(*Expand*)

Parameter coMult : forall {A}, M A $\rightarrow\;$ (M (M A)).

(*Extract*)

Parameter coUnit : forall {A}, M A $\rightarrow\;$ A.

(*Comonad operations are natural*)

Axiom coUnitNatural : forall A B, forall f : A $\rightarrow\;$ B, forall x,

f (coUnit x) = (coUnit ((#f) x)).

Axiom coMultNatural : forall A B, forall f : A $\rightarrow\;$ B, forall m,

coMult ((#f) m) = (#(#f)) (coMult m).

(*Comonad operations satisfy comonad axioms*)

Axiom coMultAx : forall A (x : M A),

coMult (coMult x) = (#coMult) (coMult x).

Axiom coUnitCoMultAx : forall A (x : M A),

coUnit (coMult x) = x.

Axiom mapCoUnitComultAx : forall A (x : M A),

(#coUnit) (coMult x) = x.

Next, we introduce the $\mathtt{put}$ operation, and assert that it is
natural:

⬇

Parameter put : forall {A}, ((M A) * A) $\rightarrow\;$ M A.

(*Put is natural*)

Axiom putNatural : forall {A} {B} (f : A $\rightarrow\;$ B) (xs : M A) (x :
A),

(#f) (put (xs, x)) = put ((#f) xs, f x).

Then, we introduce the coherence axioms. In the following code, we use the
notation $\mathtt{<\\!|f,\ g|\\!>}$ for the pairing of two functions $\langle
f,g\rangle$, defined as $\langle f,g\rangle x=(fx,gx)$, and the notation
$\mathtt{*}$ for function composition.

⬇

Axiom flattenExtract : forall A, forall (x : M (M A)),

coUnit (mult x) = coUnit (coUnit x).

Axiom singletonExpand : forall A, forall (x : A),

coMult (unit x) = (#unit) (unit x).

Axiom singletonExtract : forall A, forall (x : A),

coUnit (unit x) = x.

Axiom getPut : forall A, forall (x : M A) (y : A),

coUnit (put (x, y)) = y.

Axiom putGet : forall A, forall (x : M A),

put (x, coUnit x) = x.

Axiom putPut : forall {A} l (x : A) y,

put (put(l, x), y) = put (l, y).

Axiom putAssoc : forall A, forall (x : M (M A)) (y: M A) (z : A),

put ((mult (put (x, y))), z) = mult (put (x, put (y, z))).

Axiom singletonPut : forall A (x : A) y,

put(unit x, y) = unit y.

(*The Set-specific definition of strength*)

Definition str {X} {Y} (x : X * (M Y)) : (M (X*Y)) :=

match x with

(x1, x2) $\Rightarrow\;$ (#(fun y $\Rightarrow\;$ (x1, y))) x2

end.

Axiom flattenExpand : forall {A} (x : M (M A)),

coMult (mult x) =

mult ( (#(# mult)) ( ((#(#put)) ((# str) ((#<| id, coMult * coUnit|>) (coMult
x)))))).

Next, we define the properties of an algebra:

⬇

Definition associative {S} (alpha : M S $\rightarrow\;$ S) : Prop :=

forall l, alpha ((#alpha) l) = alpha (mult l).

Definition unitInvariant {S} (alpha : M S $\rightarrow\;$ S) : Prop :=

forall s, alpha (unit s) = s.

Finally, we define an $M$-definable transduction:

⬇

Definition mTransduction {X Y S} (alpha : M S $\rightarrow\;$ S) (h : X
$\rightarrow\;$ S) (lambda : S $\rightarrow\;$ Y) : M X $\rightarrow\;$ M Y :=

(#lambda) * (#alpha) * coMult * (#h).

###  E.2 The composition theorem

In this section, we present the formal statement of the composition theorem.
We start with the context: two $M$-definable transduction $F:MX\to MY$ and
$G:MY\to MZ$:

⬇

(*We are given three alphabets *)

Variable X : Set.

Variable Y : Set.

Variable Z : Set.

(*We are given and M-transduction F : M X $\rightarrow\;$ M Y*)

Variable S1 : Set.

Variable prod1 : M S1 $\rightarrow\;$ S1.

Variable h1 : X $\rightarrow\;$ S1.

Variable lambda1 : S1 $\rightarrow\;$ Y.

Axiom assoc1 : associative prod1.

Axiom unitInvariant : unitInvariant prod1.

Definition F := mTransduction prod1 h1 lambda1.

(*And we are given an M-transduction G : MY $\rightarrow\;$ M Z*)

Variable S2 : Set.

Variable prod2 : M S2 $\rightarrow\;$ S2.

Variable h2 : Y $\rightarrow\;$ S2.

Variable lambda2 : S2 $\rightarrow\;$ Z.

Axiom assoc2 : associative prod2.

Axiom unitInvariant2 : unitInvariant prod2.

Definition G := mTransduction prod2 h2 lambda2.

Next, we define the generalized wreath product of $S1$ and $S2$, and use it to
define a new $M$-definable transduction $GF:MX\to MZ$:

⬇

Definition S3 : Type := S1 * ((S1 $\rightarrow\;$ S1) $\rightarrow\;$ S2).

Definition prod3 (l : M S3) : S3 :=

let ctx1 (l : M S1) (x : S1) : S1 := prod1 (put (l, x)) in

let tmp1 (l : M S3) : ((S1 $\rightarrow\;$ S1) $\rightarrow\;$ S2) := proj2
(coUnit l) in

let tmp2 (c : S1 $\rightarrow\;$ S1) (l : M S3) : (S1 $\rightarrow\;$ S1) := c
* (ctx1 ((#proj1)(l))) in

(prod1 ((#proj1) (l)), fun c $\Rightarrow\;$ prod2 ( (#app2) (((#<|tmp1, tmp2
c |>) (coMult l))))).

Definition h3 (x : X) : S3 :=

(h1 x, fun c $\Rightarrow\;$ h2 (lambda1 (c (h1 x)))).

Definition lambda3 (s : S3) : Z :=

match s with

| (_, f) $\Rightarrow\;$ lambda2 (f (fun a $\Rightarrow\;$ a))

end.

Definition GF := mTransduction prod3 h3 lambda3.

Next, we prove that $GF$ is equal to $G\circ F$. (As mentioned before, we omit
the proof in this paper, but it is available in the Coq file.)

⬇

Theorem compositionCorrect : GF = G * F.

Finally, we prove that $S3$ is a valid algebra (again, we omit the proofs):

⬇

Theorem S3Associative : associative prod3.

Theorem S3UnitInvariant : unitInvariant prod3.

###  E.3 Contexts

In this section, we present the formalization of the results from Section 4.2.
We start with an algebra $S$:

⬇

Variable S : Set.

Variable prod : M S $\rightarrow\;$ S.

Axiom prodAssoc : associative prod.

Axiom prodUnit : unitInvariant prod.

We define contexts:

⬇

Definition ctx (l : M S) (x : S) : S := prod (put (l, x)).

And we prove the required lemmas, respectively Lemmas 4.3, 4.4, and C.4. Here
$\mathtt{<\\!*f,\ g*\\!>}$ denotes the function $f\times g$, defined as
$(f\times g)(x,y)=(fx,\ gy)$.

⬇

Lemma ctxPutInvariant : forall l a, ctx l = ctx (put (l, a)).

Lemma ctxUnitId : forall x, ctx (unit x) = id.

Definition concat : M S * M S $\rightarrow\;$ M S :=

mult * put * <* (#unit), id *>.

Lemma concatCtx : forall (v w : M S),

ctx v * ctx w = ctx (concat (v, w)).

###  E.4 Flatten-expand axiom

Finally, we formalize the equivalence of the flatten-expand axiom and the
bialgebraic formulation (see Section C.3). The left-hand side of the equality
is the top path in the flatten-expand axiom, and the right-hand side is the
top path in the bialgebraic formulation:

⬇

Theorem flattenExpandAltThm : forall A, forall (x : M (M A)),

mult ( (#(# mult)) ( ((#(#put)) ((# str) ((#<| id, coMult * coUnit|>) (coMult
x)))))) =

((#mult) * mult * (#(# put)) * (# str) * (#<| #coUnit, coUnit|>) * coMult *
(#coMult)) x.