×

Combining semilattices and semimodules. (English) Zbl 07410421

Kiefer, Stefan (ed.) et al., Foundations of software science and computation structures. 24th international conference, FOSSACS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12650, 102-123 (2021).
Summary: 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}\).
For the entire collection see [Zbl 1471.68019].

MSC:

68Nxx Theory of software
68Qxx Theory of computing
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] 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). doi:10.1007/978-3-030-17127-8_4 · Zbl 1524.68158
[2] 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). doi:10.1007/BFb0060439 · Zbl 0198.00201
[3] 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). doi:10.1007/BFb0083084
[4] 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). doi:10.1016/j.ic.2011.12.002 · Zbl 1279.68235
[5] 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). doi:10.1145/3209108.3209169 · Zbl 1497.68107
[6] 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). doi:10.4230/LIPIcs.CONCUR.2018.17 · Zbl 1520.68089
[7] 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). doi:10.1145/2603088.2603149 · Zbl 1395.68195
[8] Bonchi, F., Pous, D.: Hacking nondeterminism with induction and coinduction. Commun. ACM 58(2), 87-95 (2015). doi:10.1145/2713167
[9] Bonchi, F., Santamaria, A.: Combining Semilattices and Semimodules (Dec 2020), http://arxiv.org/abs/2012.14778 · Zbl 07410421
[10] 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). doi:10.1109/LICS.2019.8785673
[11] Böhm, G.: The weak theory of monads. Advances in Mathematics 225(1), 1-32 (Sep 2010). doi:10.1016/j.aim.2010.02.015 · Zbl 1206.18004
[12] 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). doi:10.1007/s40062-013-0063-2 · Zbl 1309.18004
[13] Droste, M., Kuich, W., Vogler, H.: Handbook of weighted automata. Springer Science & Business Media (2009). doi:10.1007/978-3-642-01492-5 · Zbl 1200.68001
[14] 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). doi:10.1007/978-3-030-38919-2_24 · Zbl 1440.68176
[15] Garner, R.: The Vietoris Monad and Weak Distributive Laws. Applied Categorical Structures 28(2), 339-354 (Apr 2020). doi:10.1007/s10485-019-09582-w · Zbl 1442.18010
[16] Goy, A., Petrisan, D.: Combining weak distributive laws: Application to up-to techniques (2020), https://arxiv.org/abs/2010.00811 · Zbl 1502.68171
[17] 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). doi:10.1145/3373718.3394795 · Zbl 1502.68171
[18] Gumm, H.P., Schröder, T.: Monoid-labeled transition systems. Electronic Notes in Theoretical Computer Science 44(1), 185-204 (May 2001). doi:10.1016/S1571-0661(04)80908-3 · Zbl 1260.68240
[19] Hasuo, I.: Generic weakest precondition semantics from monads enriched with order. Theoretical Computer Science 604, 2-29 (2015). doi:10.1016/j.tcs.2015.03.047 · Zbl 1330.68046
[20] Hasuo, I., Jacobs, B., Sokolova, A.: Generic trace semantics via coinduction. Log. Methods Comput. Sci. 3(4) (2007). doi:10.2168/LMCS-3(4:11)2007 · Zbl 1131.68058
[21] 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). doi:10.1145/2837614.2837673 · Zbl 1347.68227
[22] 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). doi:10.1007/978-3-030-45231-5_31 · Zbl 1461.68093
[23] 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). doi:10.1016/j.entcs.2006.04.024 · Zbl 1276.03016
[24] Hyland, M., Plotkin, G.D., Power, J.: Combining effects: Sum and tensor. Theor. Comput. Sci. 357(1-3), 70-99 (2006). doi:10.1016/j.tcs.2006.03.013 · Zbl 1096.68088
[25] Jacobs, B.: Coalgebraic Trace Semantics for Combined Possibilitistic and Probabilistic Systems. Electronic Notes in Theoretical Computer Science 203(5), 131-152 (Jun 2008). doi:10.1016/j.entcs.2008.05.023 · Zbl 1279.68232
[26] Klin, B.: Bialgebras for structural operational semantics: An introduction. Theor. Comput. Sci. 412(38), 5043-5069 (2011). doi:10.1016/j.tcs.2011.03.023 · Zbl 1246.68150
[27] 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). doi:10.1007/978-3-662-46678-0_10 · Zbl 1459.68114
[28] 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). doi:10.1016/j.entcs.2018.11.013 · Zbl 1528.18007
[29] Kurz, A., Velebil, J.: Relation lifting, a survey. Journal of Logical and Algebraic Methods in Programming 85(4), 475-499 (Jun 2016). doi:10.1016/j.jlamp.2015.08.002 · Zbl 1344.68167
[30] Manes, E.G.: Algebraic Theories, Graduate Texts in Mathematics, vol. 26. Springer, New York, NY (1976). doi:10.1007/978-1-4612-9860-1 · Zbl 0353.18007
[31] 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 · Zbl 1131.18003
[32] Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55-92 (1991). doi:10.1016/0890-5401(91)90052-4 · Zbl 0723.68073
[33] 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). doi:10.1007/BFb0055624 · Zbl 0940.68085
[34] Rutten, J.J.M.M.: A tutorial on coinductive stream calculus and signal flow graphs. Theor. Comput. Sci. 343(3), 443-481 (2005). doi:10.1016/j.tcs.2005.06.019 · Zbl 1077.68032
[35] 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). doi:10.2168/LMCS-9(1:9)2013 · Zbl 1262.18002
[36] 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). doi:10.1145/3371129
[37] 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 · Zbl 1201.18004
[38] 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). doi:10.1109/LICS.1997.614955
[39] 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). doi:10.1145/3373718.3394775 · Zbl 07299521
[40] Varacca, D., Winskel, G.: Distributing probability over non-determinism. Math. Struct. Comput. Sci. 16(1), 87-113 (2006). doi:10.1017/S0960129505005074 · Zbl 1093.18002
[41] 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). doi:10.1109/LICS.2019.8785707
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.