Natural Transformations as Rewrite Rules and Monad Composition

Eklund et al. (2002) present a graphical technique aimed at simplifying the verification of various category-theoretic constructions, notably the composition of monads. In this note we take a different approach involving string rewriting. We show that a given tuple $(T,\mu,\eta)$ is a monad if and o...

Full description

Saved in:
Bibliographic Details
Published in:Logical methods in computer science 2019-01, Vol.15, Issue 1
Main Author: Dexter Kozen
Format: Article
Language:English
Subjects:
computer science - logic in computer science
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Eklund et al. (2002) present a graphical technique aimed at simplifying the verification of various category-theoretic constructions, notably the composition of monads. In this note we take a different approach involving string rewriting. We show that a given tuple $(T,\mu,\eta)$ is a monad if and only if $T$ is a terminal object in a certain category of strings and rewrite rules, and that this fact can be established by proving confluence of the rewrite system. We illustrate the technique on the monad composition problem. We also give a characterization of adjunctions in terms of rewrite categories.
ISSN:1860-5974
DOI:10.23638/LMCS-15(1:1)2019