Kozen, Dexter - Natural Transformations as Rewrite Rules and Monad Composition

lmcs:2609 - Logical Methods in Computer Science, January 9, 2019, Volume 15, Issue 1
Natural Transformations as Rewrite Rules and Monad Composition

Authors: Kozen, Dexter

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.


Source : oai:arXiv.org:1612.07273
DOI : 10.23638/LMCS-15(1:1)2019
Volume: Volume 15, Issue 1
Published on: January 9, 2019
Submitted on: December 22, 2016
Keywords: Computer Science - Logic in Computer Science


Share