Hostname: page-component-586b7cd67f-2brh9 Total loading time: 0 Render date: 2024-11-25T00:50:15.676Z Has data issue: false hasContentIssue false

The costructure–cosemantics adjunction for comodels for computational effects

Published online by Cambridge University Press:  06 December 2021

Richard Garner*
Affiliation:
Department of Mathematics, Macquarie University, NSW 2109, Australia
*
*Corresponding author. Email: [email protected]

Abstract

It is well established that equational algebraic theories and the monads they generate can be used to encode computational effects. An important insight of Power and Shkaravska is that comodels of an algebraic theory $\mathbb{T}$ – i.e., models in the opposite category $\mathcal{S}\mathrm{et}^{\mathrm{op}}$ – provide a suitable environment for evaluating the computational effects encoded by $\mathbb{T}$ . As already noted by Power and Shkaravska, taking comodels yields a functor from accessible monads to accessible comonads on $\mathcal{S}\mathrm{et}$ . In this paper, we show that this functor is part of an adjunction – the “costructure–cosemantics adjunction” of the title – and undertake a thorough investigation of its properties. We show that, on the one hand, the cosemantics functor takes its image in what we term the presheaf comonads induced by small categories; and that, on the other, costructure takes its image in the presheaf monads induced by small categories. In particular, the cosemantics comonad of an accessible monad will be induced by an explicitly-described category called its behaviour category that encodes the static and dynamic properties of the comodels. Similarly, the costructure monad of an accessible comonad will be induced by a behaviour category encoding static and dynamic properties of the comonad coalgebras. We tie these results together by showing that the costructure–cosemantics adjunction is idempotent, with fixpoints to either side given precisely by the presheaf monads and comonads. Along the way, we illustrate the value of our results with numerous examples drawn from computation and mathematics.

Type
Special Issue: The Power Festschrift
Copyright
© The Author(s), 2021. Published by Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abbott, M., Altenkirch, T. and Ghani, N. (2005) Containers: Constructing strictly positive types. Theoretical Computer Science 342 327.CrossRefGoogle Scholar
Adámek, J., Levy, P. B., Milius, S., Moss, L. S. and Sousa, L. (2015) On final coalgebras of power-set functors and saturated trees. Applied Categorical Structures 23(4) 609641.CrossRefGoogle Scholar
Aguiar, M. (1997) Internal Categories and Quantum Groups. PhD thesis, Cornell University.Google Scholar
Ahman, D. and Bauer, A. (2020) Runners in action. In: Programming Languages and Systems, vol. 12075, Lecture Notes in Computer Science, Springer, 29–55.CrossRefGoogle Scholar
Ahman, D., Chapman, J. and Uustalu, T. (2012) When is a container a comonad? In: Foundations of Software Science and Computational Structures, vol. 7213, Lecture Notes in Computer Science, Heidelberg: Springer, 74–88.Google Scholar
Ahman, D. and Uustalu, T. (2014) Coalgebraic update lenses. In : Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXX), vol. 308, Electron. Notes Theor. Comput. Sci. Amsterdam: Elsevier Sci. B. V., 25–48.CrossRefGoogle Scholar
Ahman, D. and Uustalu, T. (2014) Update monads: Cointerpreting directed containers. In: 19th International Conference on Types for Proofs and Programs, vol. 26 LIPIcs, Leibniz Int. Proc. Inform., Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 1–23.Google Scholar
Ahman, D. and Uustalu, T. (2017) Taking updates seriously. In: Proceedings of the 6th International Workshop on Bidirectional Transformations (2017), CEUR Workshop Proceedings, 59–73.Google Scholar
Barr, M. and Wells, C. (1985) Toposes, Triples and Theories, vol. 278, Grundlehren der Mathematischen Wissenschaften. Springer.CrossRefGoogle Scholar
Diers, Y. (1978) Spectres et localisations relatifs à un foncteur. Comptes rendus hebdomadaires des séances de l’Académie des sciences 287 985988.Google Scholar
Dubuc, E. J. (1970) Kan extensions in enriched category theory, vol. 145, Lecture Notes in Mathematics. Springer.CrossRefGoogle Scholar
Foster, J. N., Greenwald, M. B., Moore, J. T., Pierce, B. C. and Schmitt, A. (2007) Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem. ACM Transactions on Programming Languages and Systems 29 17–es.CrossRefGoogle Scholar
Goncharov, S. (2013) Trace semantics via generic observations. In: Algebra and Coalgebra in Computer Science, vol. 8089, Lecture Notes in Computer Science, Heidelberg: Springer, 158–174.CrossRefGoogle Scholar
Goncharov, S., Milius, S. and Silva, A. (2014) Towards a coalgebraic chomsky hierarchy. In: TCS 2014, Rome (2014), vol. 8705, Lecture Notes in Computer Science, Springer, 265–280.Google Scholar
Goncharov, S., Milius, S. and Silva, A. (2020) Toward a uniform theory of effectful state machines. ACM Transactions on Computational Logic 21.Google Scholar
Higgins, P. J. and Mackenzie, K. C. H. (1993) Duality for base-changing morphisms of vector bundles, modules, Lie algebroids and Poisson structures. Mathematical Proceedings of the Cambridge Philosophical Society 114 471488.CrossRefGoogle Scholar
Johnstone, P. T. (1990) Collapsed toposes and Cartesian closed varieties. Journal of Algebra 129 446480.CrossRefGoogle Scholar
Jónsson, B. and Tarski, A. (1961) On two properties of free algebras. Mathematica Scandinavica 9 95101.CrossRefGoogle Scholar
Katsumata, S., Rivas, E. and Uustalu, T. (2019) Interaction laws of monads and comonads. Preprint, available as arXiv:1912.13477.Google Scholar
Kelly, G. M. and Power, A. J. (1993) Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads. Journal of Pure and Applied Algebra 89 163179.CrossRefGoogle Scholar
Kupke, C. and Leal, R. A. (2009) Characterising behavioural equivalence: Three sides of one coin. In: Algebra and Coalgebra in Computer Science, vol. 5728, Lecture Notes in Computer Science. Springer, 97–112.CrossRefGoogle Scholar
Lawvere, F. W. (1963) Functorial Semantics of Algebraic Theories. PhD thesis, Columbia University.CrossRefGoogle Scholar
Manes, E. (1976) Algebraic Theories, vol. 26. Graduate Texts in Mathematics. Springer.CrossRefGoogle Scholar
Møgelberg, R. E. and Staton, S. (2014) Linear usage of state. Logical Methods in Computer Science 10 1:17, 52.CrossRefGoogle Scholar
Moggi, E. (1991) Notions of computation and monads. Information and Computation 93 5592.CrossRefGoogle Scholar
Pattinson, D. and Schröder, L. (2015) Sound and complete equational reasoning over comodels. In: The 31st Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXI), vol. 319, Electronic Notes in Theoretical Computer Science. Elsevier, 315–331.CrossRefGoogle Scholar
Pattinson, D. and Schröder, L. (2016) Program equivalence is coinductive. In: Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science (LICS 2016) (2016), ACM, 10.Google Scholar
Plotkin, G. and Power, J. (2001) Adequacy for algebraic effects. In: Foundations of Software Science and Computation Structures (Genova, 2001), vol. 2030, Lecture Notes in Computer Science, Berlin: Springer, 1–24.CrossRefGoogle Scholar
Plotkin, G. and Power, J. (2002) Notions of computation determine monads. In: Foundations of Software Science and Computation Structures (Grenoble, 2002), vol. 2303, Lecture Notes in Computer Science. Springer, Berlin, 2002, pp. 342356.Google Scholar
Plotkin, G. and Power, J. (2003) Algebraic operations and generic effects. Applied Categorical Structures 11 6994.CrossRefGoogle Scholar
Plotkin, G. and Power, J. (2008) Tensors of comodels and models for operational semantics. Electronic Notes in Theoretical Computer Science 218 295311.CrossRefGoogle Scholar
Power, J. and Shkaravska, O. (2004) From comodels to coalgebras: State and arrays. In: Proceedings of the Workshop on Coalgebraic Methods in Computer Science (2004), vol. 106. Electronic Notes in Theoretical Computer Science, Elsevier, 297–314.Google Scholar
Renault, J. (1980) A Groupoid Approach to $C^{\ast} $ -Algebras. vol. 793. Lecture Notes in Mathematics, Berlin: Springer.CrossRefGoogle Scholar
Rutten, J. J. M. M. (2000) Universal coalgebra: A theory of systems. Theoretical Computer Science 249 380.CrossRefGoogle Scholar
Rutten, J. J. M. M. and Turi, D. (1993) On the foundations of final semantics: nonstandard sets, metric spaces, partial orders. In: Semantics: Foundations and Applications (Beekbergen, 1992), vol. 666, Lecture Notes in Computer Science, Berlin: Springer, 477–530.CrossRefGoogle Scholar
Thielecke, H. (1997) Categorical Structure of Continuation Passing Style. PhD thesis, University of Edinburgh.Google Scholar
Uustalu, T. (2015) Stateful runners of effectful computations. In: The 31st Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXI), vol. 319, Electron. Notes Theor. Comput. Sci. Elsevier Sci. B. V., Amsterdam, 403–421.CrossRefGoogle Scholar