Abstract
We describe the canonical weak distributive law \(\delta :\mathcal S\mathcal P\rightarrow \mathcal P\mathcal S\) of the powerset monad \(\mathcal P\) over the S-left-semimodule monad \(\mathcal S\), for a class of semirings S. We show that the composition of \(\mathcal P\) with \(\mathcal S\) by means of such \(\delta \) yields almost the monad of convex subsets previously introduced by Jacobs: the only difference consists in the absence in Jacobs’s monad of the empty convex set. We provide a handy characterisation of the canonical weak lifting of \(\mathcal P\) to \(\mathbb {EM}(\mathcal S)\) as well as an algebraic theory for the resulting composed monad. Finally, we restrict the composed monad to finitely generated convex subsets and we show that it is presented by an algebraic theory combining semimodules and semilattices with bottom, which are the algebras for the finite powerset monad \(\mathcal P_f\).
Supported by the Ministero dell’Università e della Ricerca of Italy under Grant No. 201784YSZ5, PRIN2017 – ASPRA (Analysis of Program Analyses).
Chapter PDF
Similar content being viewed by others
References
Barlocco, S., Kupke, C., Rot, J.: Coalgebra learning via duality. In: International Conference on Foundations of Software Science and Computation Structures. pp. 62–79. Springer (2019). https://doi.org/10.1007/978-3-030-17127-8_4
Barr, M.: Relational algebras. In: MacLane, S., Applegate, H., Barr, M., Day, B., Dubuc, E., Phreilambud, Pultr, A., Street, R., Tierney, M., Swierczkowski, S. (eds.) Reports of the Midwest Category Seminar IV. pp. 39–55. Lecture Notes in Mathematics, Springer, Berlin, Heidelberg (1970). https://doi.org/10.1007/BFb0060439
Beck, J.: Distributive laws. In: Appelgate, H., Barr, M., Beck, J., Lawvere, F.W., Linton, F.E.J., Manes, E., Tierney, M., Ulmer, F., Eckmann, B. (eds.) Seminar on Triples and Categorical Homology Theory. pp. 119–140. Lecture Notes in Mathematics, Springer, Berlin, Heidelberg (1969). https://doi.org/10.1007/BFb0083084
Bonchi, F., Bonsangue, M.M., Boreale, M., Rutten, J.J.M.M., Silva, A.: A coalgebraic perspective on linear weighted automata. Inf. Comput. 211, 77–105 (2012). https://doi.org/10.1016/j.ic.2011.12.002
Bonchi, F., Ganty, P., Giacobazzi, R., Pavlovic, D.: Sound up-to techniques and complete abstract domains. In: Dawar, A., Grädel, E. (eds.) Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018. pp. 175–184. ACM (2018). https://doi.org/10.1145/3209108.3209169
Bonchi, F., König, B., Petrisan, D.: Up-to techniques for behavioural metrics via fibrations. In: Schewe, S., Zhang, L. (eds.) 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China. LIPIcs, vol. 118, pp. 17:1–17:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018). https://doi.org/10.4230/LIPIcs.CONCUR.2018.17
Bonchi, F., Petrisan, D., Pous, D., Rot, J.: Coinduction up-to in a fibrational setting. In: Henzinger, T.A., Miller, D. (eds.) Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, Vienna, Austria, July 14 - 18, 2014. pp. 20:1–20:9. ACM (2014). https://doi.org/10.1145/2603088.2603149
Bonchi, F., Pous, D.: Hacking nondeterminism with induction and coinduction. Commun. ACM 58(2), 87–95 (2015). https://doi.org/10.1145/2713167
Bonchi, F., Santamaria, A.: Combining Semilattices and Semimodules (Dec 2020), http://arxiv.org/abs/2012.14778
Bonchi, F., Sokolova, A., Vignudelli, V.: The theory of traces for systems with nondeterminism and probability. In: 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). pp. 1–14. IEEE (2019). https://doi.org/10.1109/LICS.2019.8785673
Böhm, G.: The weak theory of monads. Advances in Mathematics 225(1), 1–32 (Sep 2010). https://doi.org/10.1016/j.aim.2010.02.015
Clementino, M.M., Hofmann, D., Janelidze, G.: The monads of classical algebra are seldom weakly cartesian. Journal of Homotopy and Related Structures 9(1), 175–197 (Apr 2014). https://doi.org/10.1007/s40062-013-0063-2
Droste, M., Kuich, W., Vogler, H.: Handbook of weighted automata. Springer Science & Business Media (2009). https://doi.org/10.1007/978-3-642-01492-5
Erkens, R., Rot, J., Luttik, B.: Up-to techniques for branching bisimilarity. In: International Conference on Current Trends in Theory and Practice of Informatics. pp. 285–297. Springer (2020). https://doi.org/10.1007/978-3-030-38919-2_24
Garner, R.: The Vietoris Monad and Weak Distributive Laws. Applied Categorical Structures 28(2), 339–354 (Apr 2020). https://doi.org/10.1007/s10485-019-09582-w
Goy, A., Petrisan, D.: Combining weak distributive laws: Application to up-to techniques (2020), https://arxiv.org/abs/2010.00811
Goy, A., Petrişan, D.: Combining probabilistic and non-deterministic choice via weak distributive laws. In: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science. pp. 454–464. LICS ’20, Association for Computing Machinery, New York, NY, USA (Jul 2020). https://doi.org/10.1145/3373718.3394795
Gumm, H.P., Schröder, T.: Monoid-labeled transition systems. Electronic Notes in Theoretical Computer Science 44(1), 185–204 (May 2001). https://doi.org/10.1016/S1571-0661(04)80908-3
Hasuo, I.: Generic weakest precondition semantics from monads enriched with order. Theoretical Computer Science 604, 2–29 (2015). https://doi.org/10.1016/j.tcs.2015.03.047
Hasuo, I., Jacobs, B., Sokolova, A.: Generic trace semantics via coinduction. Log. Methods Comput. Sci. 3(4) (2007). https://doi.org/10.2168/LMCS-3(4:11)2007
Hasuo, I., Shimizu, S., Cîrstea, C.: Lattice-theoretic progress measures and coalgebraic model checking. In: Bodík, R., Majumdar, R. (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016. pp. 718–732. ACM (2016). https://doi.org/10.1145/2837614.2837673
van Heerdt, G., Kupke, C., Rot, J., Silva, A.: Learning weighted automata over principal ideal domains. In: International Conference on Foundations of Software Science and Computation Structures. pp. 602–621. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45231-5_31
Hyland, M., Nagayama, M., Power, J., Rosolini, G.: A category theoretic formulation for engeler-style models of the untyped lambda. Electron. Notes Theor. Comput. Sci. 161, 43–57 (2006). https://doi.org/10.1016/j.entcs.2006.04.024
Hyland, M., Plotkin, G.D., Power, J.: Combining effects: Sum and tensor. Theor. Comput. Sci. 357(1-3), 70–99 (2006). https://doi.org/10.1016/j.tcs.2006.03.013
Jacobs, B.: Coalgebraic Trace Semantics for Combined Possibilitistic and Probabilistic Systems. Electronic Notes in Theoretical Computer Science 203(5), 131–152 (Jun 2008). https://doi.org/10.1016/j.entcs.2008.05.023
Klin, B.: Bialgebras for structural operational semantics: An introduction. Theor. Comput. Sci. 412(38), 5043–5069 (2011). https://doi.org/10.1016/j.tcs.2011.03.023
Klin, B., Rot, J.: Coalgebraic trace semantics via forgetful logics. In: Pitts, A.M. (ed.) Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. Lecture Notes in Computer Science, vol. 9034, pp. 151–166. Springer (2015). https://doi.org/10.1007/978-3-662-46678-0_10
Klin, B., Salamanca, J.: Iterated covariant powerset is not a monad. In: Staton, S. (ed.) Proceedings of the Thirty-Fourth Conference on the Mathematical Foundations of Programming Semantics, MFPS 2018, Dalhousie University, Halifax, Canada, June 6-9, 2018. Electronic Notes in Theoretical Computer Science, vol. 341, pp. 261–276. Elsevier (2018). https://doi.org/10.1016/j.entcs.2018.11.013
Kurz, A., Velebil, J.: Relation lifting, a survey. Journal of Logical and Algebraic Methods in Programming 85(4), 475–499 (Jun 2016). https://doi.org/10.1016/j.jlamp.2015.08.002
Manes, E.G.: Algebraic Theories, Graduate Texts in Mathematics, vol. 26. Springer, New York, NY (1976). https://doi.org/10.1007/978-1-4612-9860-1
Manes, E., Mulry, P.: Monad compositions I: General constructions and recursive distributive laws. Theory and Applications of Categories [electronic only] 18, 172–208 (2007), http://www.tac.mta.ca/tac/volumes/18/7/18-07abs.html
Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55–92 (1991). https://doi.org/10.1016/0890-5401(91)90052-4
Rutten, J.J.M.M.: Automata and coinduction (an exercise in coalgebra). In: Sangiorgi, D., de Simone, R. (eds.) CONCUR ’98: Concurrency Theory, 9th International Conference, Nice, France, September 8-11, 1998, Proceedings. Lecture Notes in Computer Science, vol. 1466, pp. 194–218. Springer (1998). https://doi.org/10.1007/BFb0055624
Rutten, J.J.M.M.: A tutorial on coinductive stream calculus and signal flow graphs. Theor. Comput. Sci. 343(3), 443–481 (2005). https://doi.org/10.1016/j.tcs.2005.06.019
Silva, A., Bonchi, F., Bonsangue, M.M., Rutten, J.J.M.M.: Generalizing determinization from automata to coalgebras. Log. Methods Comput. Sci. 9(1) (2013). https://doi.org/10.2168/LMCS-9(1:9)2013
Smolka, S., Foster, N., Hsu, J., Kappé, T., Kozen, D., Silva, A.: Guarded kleene algebra with tests: verification of uninterpreted programs in nearly linear time. Proceedings of the ACM on Programming Languages 4(POPL), 1–28 (2019). https://doi.org/10.1145/3371129
Street, R.: Weak Distributive Laws. Theory and Applications of Categories 22(12), 313–320 (2009), http://www.tac.mta.ca/tac/volumes/22/12/22-12abs.html
Turi, D., Plotkin, G.: Towards a mathematical operational semantics. In: Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science. pp. 280–291. IEEE (1997). https://doi.org/10.1109/LICS.1997.614955
Urbat, H., Schröder, L.: Automata learning: An algebraic approach. In: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science. pp. 900–914 (2020). https://doi.org/10.1145/3373718.3394775
Varacca, D., Winskel, G.: Distributing probability over non-determinism. Math. Struct. Comput. Sci. 16(1), 87–113 (2006). https://doi.org/10.1017/S0960129505005074
Zwart, M., Marsden, D.: No-Go Theorems for Distributive Laws. In: 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). pp. 1–13 (Jun 2019). https://doi.org/10.1109/LICS.2019.8785707
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2021 The Author(s)
About this paper
Cite this paper
Bonchi, F., Santamaria, A. (2021). Combining Semilattices and Semimodules. In: Kiefer, S., Tasson, C. (eds) Foundations of Software Science and Computation Structures. FOSSACS 2021. Lecture Notes in Computer Science(), vol 12650. Springer, Cham. https://doi.org/10.1007/978-3-030-71995-1_6
Download citation
DOI: https://doi.org/10.1007/978-3-030-71995-1_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-71994-4
Online ISBN: 978-3-030-71995-1
eBook Packages: Computer ScienceComputer Science (R0)