A Recipe for State-and-Effect Triangles

Authors :: Jacobs, B.
Moss, L.
Moss, L.
Source :: Logical Methods in Computer Science, 13, 2, pp. 1-26, Logical Methods in Computer Science, 13, 1-26, Moss, L. (ed.), CALCO 2015 : 6th Conference on Algebra and Coalgebra in Computer Science 24-26 June, 2015, Nijmegen, Netherlands, pp. 116-129, Moss, L. (ed.), CALCO 2015 : 6th Conference on Algebra and Coalgebra in Computer Science 24-26 June, 2015, Nijmegen, Netherlands, 116-129. Dagstuhl : Schloss Dagstuhl, STARTPAGE=116;ENDPAGE=129;ISSN=1868-8969;TITLE=Moss, L. (ed.), CALCO 2015 : 6th Conference on Algebra and Coalgebra in Computer Science 24-26 June, 2015, Nijmegen, Netherlands
Publication Year :: 2017
Abstract: In the semantics of programming languages one can view programs as state transformers, or as predicate transformers. Recently the author has introduced state-and-effect triangles which capture this situation categorically, involving an adjunction between state- and predicate-transformers. The current paper exploits a classical result in category theory, part of Jon Beck's monadicity theorem, to systematically construct such a state-and-effect triangle from an adjunction. The power of this construction is illustrated in many examples, covering many monads occurring in program semantics, including (probabilistic) power domains.<br />Logical Methods in Computer Science ; Volume 13, Issue 2 ; 1860-5974