Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Monads, Comonads, and Transducers

Rafał Stefański

TL;DR

The paper develops a unified, category-theoretic framework for transducers by defining $M$-recognizable transductions where $M$ is simultaneously a monad and a comonad. It demonstrates that familiar models like Mealy machines and rational transductions arise as instances, and extends recognizability to infinite words and trees via specific comonad structures. A central result shows closure under composition, proven via a generalized wreath product construction and formalized in Coq, provided a set of coherence axioms linking monad and comonad structures. This work advances regularity theory by merging monadic recognizability with transduction theory, offering tools such as contexts and wreath-like constructions for analyzing Eilenberg-Moore algebras and their transductions.

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 arXiv:1502.04898. In this 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. 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.

Monads, Comonads, and Transducers

TL;DR

The paper develops a unified, category-theoretic framework for transducers by defining -recognizable transductions where is simultaneously a monad and a comonad. It demonstrates that familiar models like Mealy machines and rational transductions arise as instances, and extends recognizability to infinite words and trees via specific comonad structures. A central result shows closure under composition, proven via a generalized wreath product construction and formalized in Coq, provided a set of coherence axioms linking monad and comonad structures. This work advances regularity theory by merging monadic recognizability with transduction theory, offering tools such as contexts and wreath-like constructions for analyzing Eilenberg-Moore algebras and their transductions.

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 arXiv:1502.04898. In this 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. 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.
Paper Structure (10 sections, 8 theorems, 31 equations, 2 figures)

This paper contains 10 sections, 8 theorems, 31 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Monads and recognizable languages
  3. Comonads and transducers
  4. Examples of word-to-word transductions
  5. Other examples
  6. Compositions of recognizable transducers
  7. The put-structure and its axioms
  8. Contexts
  9. Composition theorem
  10. Further work

Key Result

Lemma 15

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 depends only on: Moreover, if $A$ is finite then both $M_L$ and $M_R$ are finite as well.

Figures (2)

  • Figure :
  • Figure :

Theorems & Definitions (27)

  • Definition 1
  • Definition 2
  • Example 3
  • Definition 4
  • Example 5
  • Definition 6
  • Example 7
  • Definition 8
  • Example 9: bojanczyk2015recognisable
  • Example 10: bojanczyk2020languages
  • ...and 17 more