Exploring the Boundaries of Monad Tensorability on Set

Bowler N, Goncharov S, Levy P, Schröder L (2013)


Publication Language: English

Publication Type: Journal article, Original article

Publication year: 2013

Journal

Publisher: IfCoLog (International Federation of Computational Logic) / Technical University of Braunschweig

Book Volume: 9

Pages Range: 1-18

Journal Issue: 3:22

DOI: 10.2168/LMCS-9(3:22)2013

Open Access Link: http://www.lmcs-online.org/ojs/viewarticle.php?id=1185

Abstract

We study a composition operation on monads, equivalently presented as large equational theories. Specifically, we discuss the existence of tensors, which are combinations of theories that impose mutual commutation of the operations from the component theories. As such, they extend the sum of two theories, which is just their unrestrained combination. Tensors of theories arise in several contexts; in particular, in the semantics of programming languages, the monad transformer for global state is given by a tensor. We present two main results: we show that the tensor of two monads need not in general exist by presenting two counterexamples, one of them involving finite powerset (i.e. the theory of join semilattices); this solves a somewhat long-standing open problem, and contrasts with recent results that had ruled out previously expected counterexamples. On the other hand, we show that tensors with bounded powerset monads do exist from countable powerset upwards. © N. Bowler, S. Goncharov, P. B. Levy, and L. Schröder.

Authors with CRIS profile

Related research project(s)

Involved external institutions

How to cite

APA:

Bowler, N., Goncharov, S., Levy, P., & Schröder, L. (2013). Exploring the Boundaries of Monad Tensorability on Set. Logical Methods in Computer Science, 9(3:22), 1-18. https://dx.doi.org/10.2168/LMCS-9(3:22)2013

MLA:

Bowler, Nathan, et al. "Exploring the Boundaries of Monad Tensorability on Set." Logical Methods in Computer Science 9.3:22 (2013): 1-18.

BibTeX: Download