Monads, Comonads, and Transducers

TL;DR

This paper introduces a framework for recognizable transducers over monads and comonads, unifying various classes of transductions and proving their closure under composition with formal proof assistance.

Contribution

It defines a new class of recognizable transducers over monads and comonads, generalizing existing models like Mealy machines and rational transductions, with formal proofs in Coq.

Findings

The class of recognizable transductions is closed under composition.

Examples include transducers for infinite words and tree structures.

The framework unifies multiple transducer classes under a common theory.

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.