Document Open Access Logo

Tensor of Quantitative Equational Theories

Authors Giorgio Bacci , Radu Mardare, Prakash Panangaden, Gordon Plotkin

PDF
Thumbnail PDF

File

LIPIcs.CALCO.2021.7.pdf
  • Filesize: 0.79 MB
  • 17 pages

Document Identifiers

Author Details

Giorgio Bacci
  • Department of Computer Science, Aalborg University, Denmark
Radu Mardare
  • Department of Computer & Information Sciences, University of Strathclyde, Glasgow, UK
Prakash Panangaden
  • School of Computer Science, McGill University, Montreal, Canada
Gordon Plotkin
  • LFCS, School of Informatics, University of Edinburgh, UK

Cite AsGet BibTex

Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Tensor of Quantitative Equational Theories. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CALCO.2021.7

Abstract

We develop a theory for the commutative combination of quantitative effects, their tensor, given as a combination of quantitative equational theories that imposes mutual commutation of the operations from each theory. As such, it extends the sum of two theories, which is just their unrestrained combination. Tensors of theories arise in several contexts; in particular, in the semantics of programming languages, the monad transformer for global state is given by a tensor. We show that under certain assumptions on the quantitative theories the free monad that arises from the tensor of two theories is the categorical tensor of the free monads on the theories. As an application, we provide the first algebraic axiomatizations of labelled Markov processes and Markov decision processes. Apart from the intrinsic interest in the axiomatizations, it is pleasing they are obtained compositionally by means of the sum and tensor of simpler quantitative equational theories.

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
Keywords
  • Quantitative equational theories
  • Tensor
  • Monads
  • Quantitative Effects

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. An algebraic theory of markov processes. In LICS, pages 679-688. ACM, 2018. Google Scholar
  2. Jon Beck. Distributive laws. In Seminar on Triples and Categorical Homology Theory, volume 80 of Lect. Notes Math., pages 119-140. Springer, 1966. Google Scholar
  3. Filippo Bonchi and Alessio Santamaria. Combining semilattices and semimodules. CoRR, abs/2012.14778, 2020. Google Scholar
  4. Nathan J. Bowler, Sergey Goncharov, Paul Blain Levy, and Lutz Schr "o der. Exploring the boundaries of monad tensorability on set. Log. Methods Comput. Sci., 9(3), 2013. Google Scholar
  5. Pietro Cenciarelli and Eugenio Moggi. A syntactic approach to modularity in denotational semantics. Technical report, CWI, 1993. Proc. 5th. Biennial Meeting on Category Theory and Computer Science. Google Scholar
  6. Eugenia Cheng. Distributive laws for lawvere theories. Compositionality, 2:1, May 2020. URL: https://doi.org/10.32408/compositionality-2-1.
  7. Josee Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labelled Markov processes. Theoretical Computer Science, 318(3):323-354, 2004. Google Scholar
  8. Peter J. Freyd. Algebra valued functors in general and tensor products in particular. Colloq. Math., 14:89-106, 1966. Google Scholar
  9. Richard Garner. The vietoris monad and weak distributive laws. Appl. Categorical Struct., 28(2):339-354, 2020. Google Scholar
  10. Alexandre Goy and Daniela Petrisan. Combining probabilistic and non-deterministic choice via weak distributive laws. In LICS, pages 454-464. ACM, 2020. Google Scholar
  11. Martin Hyland, Paul Blain Levy, Gordon D. Plotkin, and John Power. Combining algebraic effects with continuations. Theor. Comput. Sci., 375(1-3):20-40, 2007. Google Scholar
  12. Martin Hyland, Gordon D. Plotkin, and John Power. Combining effects: Sum and tensor. Theor. Comput. Sci., 357(1-3):70-99, 2006. URL: https://doi.org/10.1016/j.tcs.2006.03.013.
  13. Martin Hyland and John Power. Discrete lawvere theories and computational effects. Theor. Comput. Sci., 366(1-2):144-162, 2006. Google Scholar
  14. Martin Hyland and John Power. The category theoretic understanding of universal algebra: Lawvere theories and monads. Electronic Notes in Theor. Comp. Sci., 172:437-458, 2007. Google Scholar
  15. Leonid Vitalevich Kantorovich. On the transfer of masses (in Russian). Doklady Akademii Nauk, 5(5-6):1-4, 1942. Translated in Management Science, 1958. Google Scholar
  16. Gregory M. Kelly. Basic concepts of enriched category theory. Theory and Applications of Categories, 1982. Reprinted in 2005. Google Scholar
  17. Anders Kock. Strong functors and monoidal monads. Arch. Math. (Basel), 23:113-120, 1972. Google Scholar
  18. Saunders Mac Lane. Categories for the Working Mathematician. Graduate Texts in Mathematics. Springer New York, 2nd edition, 1998. Google Scholar
  19. William F. Lawvere. Metric spaces, generalized logic, and closed categories. In Seminario Mat. e. Fis. di Milano, volume 43, pages 135-166. Springer, 1973. Google Scholar
  20. Ernest Manes. A Triple Theoretic Construction of Compact Algebras. In Seminar on Triples and Categorical Homology Theory, volume 80 of Lect. Notes Math., pages 91-118. Springer, 1966. Google Scholar
  21. Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. Quantitative Algebraic Reasoning. In LICS, pages 700-709. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934518.
  22. Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. On the axiomatizability of quantitative algebras. In LICS 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005102.
  23. Matteo Mio and Valeria Vignudelli. Monads and quantitative equational theories for nondeterminism and probability. In CONCUR, volume 171 of LIPIcs, pages 28:1-28:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. Google Scholar
  24. Eugenio Moggi. The partial lambda calculus. PhD thesis, University of Edinburgh. College of Science and Engineering. School of Informatics., 1988. Google Scholar
  25. Eugenio Moggi. Notions of computation and monads. Information and computation, 93(1):55-92, 1991. Google Scholar
  26. Gordon Plotkin and John Power. Semantics for algebraic operations. Electronic Notes in Theoretical Computer Science, 45:332-345, 2001. Google Scholar
  27. Gordon Plotkin and John Power. Notions of computation determine monads. In Foundations of Software Science and Computation Structures, pages 342-356. Springer, 2002. Google Scholar
  28. Gordon D. Plotkin and John Power. Semantics for algebraic operations. In MFPS, volume 45 of Electronic Notes in Theoretical Computer Science, pages 332-345. Elsevier, 2001. Google Scholar
  29. Gordon D. Plotkin and John Power. Algebraic operations and generic effects. Appl. Categorical Struct., 11(1):69-94, 2003. Google Scholar
  30. M. L. Puterman. Markov Decision Processes. Wiley, 2005. Google Scholar
  31. Marshall H. Stone. Postulates for the barycentric calculus. Annali di Matematica Pura ed Applicata, 29(1):25-30, 1949. Google Scholar
  32. Franck van Breugel, Claudio Hermida, Michael Makkai, and James Worrell. Recursively defined metric spaces without contraction. Theor. Comput. Sci., 380(1-2):143-163, 2007. URL: https://doi.org/10.1016/j.tcs.2007.02.059.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact