Presenting Distributive Laws

TL;DR

This paper explores how to derive distributive laws for monads with equations from those of free monads, aiding in the analysis of context-free languages and algebra-coalgebra interactions.

Contribution

It introduces a method to obtain distributive laws for non-free monads from free monads, facilitating their use in language and semantics analysis.

Findings

Established a construction for distributive laws with equations

Applied the method to show equivalence of context-free language representations

Enhanced understanding of algebra-coalgebra interactions in categorical semantics

Abstract

Distributive laws of a monad T over a functor F are categorical tools for specifying algebra-coalgebra interaction. They proved to be important for solving systems of corecursive equations, for the specification of well-behaved structural operational semantics and, more recently, also for enhancements of the bisimulation proof method. If T is a free monad, then such distributive laws correspond to simple natural transformations. However, when T is not free it can be rather difficult to prove the defining axioms of a distributive law. In this paper we describe how to obtain a distributive law for a monad with an equational presentation from a distributive law for the underlying free monad. We apply this result to show the equivalence between two different representations of context-free languages.