×

Combining a monad and a comonad. (English) Zbl 1002.68059

Summary: We give a systematic treatment of distributivity for a monad and a comonad as arises in giving category theoretic accounts of operational and denotational semantics, and in giving an intensional denotational semantics. We do this axiomatically, in terms of a monad and a comonad in a 2-category, giving accounts of the Eilenberg–Moore and Kleisli constructions. We analyse the eight possible relationships, deducing that two pairs are isomorphic, but that the other pairs are all distinct. We develop those 2-categorical definitions necessary to support this analysis.

MSC:

68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68Q55 Semantics in the theory of computing
Full Text: DOI

References:

[1] Barr, M.; Wells, C., Toposes, Triples and Theories. Toposes, Triples and Theories, Grundlagen der Mathematischen Wissenschaften, Vol. 278 (1985), Springer: Springer Berlin · Zbl 0567.18001
[2] S. Brookes, S. Geva, Computational comonads and intensional semantics, Proc. Durham Conf. Categories in Computer Science 1991, 1993.; S. Brookes, S. Geva, Computational comonads and intensional semantics, Proc. Durham Conf. Categories in Computer Science 1991, 1993. · Zbl 0797.18004
[3] M.P. Fiore, Axiomatic domain theory in categories of partial maps, Cambridge University Press Distinguished Dissertations in Computer Science, 1996.; M.P. Fiore, Axiomatic domain theory in categories of partial maps, Cambridge University Press Distinguished Dissertations in Computer Science, 1996. · Zbl 0979.68549
[4] Goguen, J. A.; Thatcher, J. W.; Wagner, E. G., An initial algebra approach to the specification, correctness and implementation of abstract data types, (Yet, R. T., Current Trends in Programming Methodology, Vol. 4 (1978), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ), 80-149
[5] Jacobs, B.; Rutten, J., A tutorial on (Co)algebras and (Co)induction, EATCS Bull., 62, 222-259 (1997) · Zbl 0880.68070
[6] Johnstone, P. T., Adjoint lifting theorems for categories of algebras, Bull. London Math. Soc., 7, 294-297 (1975) · Zbl 0315.18004
[7] P.T. Johnstone, A.J. Power, T. Tsujishita, H. Watanabe, J. Worrell, Proceedings, Lecture Notes in Computer Science, Vol. 98, IEEE Press, 1998, pp. 207-213.; P.T. Johnstone, A.J. Power, T. Tsujishita, H. Watanabe, J. Worrell, Proceedings, Lecture Notes in Computer Science, Vol. 98, IEEE Press, 1998, pp. 207-213.
[8] G.M. Kelly, R. Street, Review of the elements of 2-categories, Sydney Category Seminar, Lecture Notes in Mathematics, Vol. 420, Springer, Berlin, 1974, pp. 75-103.; G.M. Kelly, R. Street, Review of the elements of 2-categories, Sydney Category Seminar, Lecture Notes in Mathematics, Vol. 420, Springer, Berlin, 1974, pp. 75-103. · Zbl 0334.18016
[9] J. MacDonald, Liftings and Kleisli extensions, Foundational Methods in Computer Science ’98 Lecture, 1998.; J. MacDonald, Liftings and Kleisli extensions, Foundational Methods in Computer Science ’98 Lecture, 1998.
[10] J. MacDonald, A. Stone, Foundational Methods in Computer Science ’95 Lecture, 1995.; J. MacDonald, A. Stone, Foundational Methods in Computer Science ’95 Lecture, 1995.
[11] Moggi, E., Notions of computation and monads, Inform. and Comput., 93, 55-92 (1991) · Zbl 0723.68073
[12] P.S. Mulry, Lifting theorems for Kleisli categories, Proc. 9th Mathematical Foundations of Programming Semantics, Lecture Notes in Computer Science, Vol. 802, Springer, Berlin, 1994, pp. 304-319.; P.S. Mulry, Lifting theorems for Kleisli categories, Proc. 9th Mathematical Foundations of Programming Semantics, Lecture Notes in Computer Science, Vol. 802, Springer, Berlin, 1994, pp. 304-319. · Zbl 1509.18004
[13] Power, J.; Turi, D., A coalgebraic foundation for linear time semantics. A coalgebraic foundation for linear time semantics, Proc. CTCS’99, Electric Notes in Theoretical Computer Science, Vol. 24 (1999), Springer: Springer Berlin · Zbl 0967.68102
[14] Rutten, J.; Turi, D., Initial algebra and final coalgebra semantics for concurrency, (de Bakker, J.; etal., Proc. REX Workshop A Decade of Concurrency - Reflections and Perspectives. Proc. REX Workshop A Decade of Concurrency - Reflections and Perspectives, Lecture Notes in Computer Science, Vol. 803 (1994), Springer: Springer Berlin), 530-582
[15] Street, R., The formal theory of monads, J. Pure Appl. Algebra, 2, 149-168 (1972) · Zbl 0241.18003
[16] D. Turi, G. Plotkin, Towards a mathematical operational semantics, Proceedings, Lecture Notes in Computer Science, Vol. 97, IEEE Press, 1997, pp. 280-291.; D. Turi, G. Plotkin, Towards a mathematical operational semantics, Proceedings, Lecture Notes in Computer Science, Vol. 97, IEEE Press, 1997, pp. 280-291.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.