License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CALCO.2021.7
URN: urn:nbn:de:0030-drops-153628
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/15362/
Bacci, Giorgio ;
Mardare, Radu ;
Panangaden, Prakash ;
Plotkin, Gordon
Tensor of Quantitative Equational Theories
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.
BibTeX - Entry
@InProceedings{bacci_et_al:LIPIcs.CALCO.2021.7,
author = {Bacci, Giorgio and Mardare, Radu and Panangaden, Prakash and Plotkin, Gordon},
title = {{Tensor of Quantitative Equational Theories}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {7:1--7:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/15362},
URN = {urn:nbn:de:0030-drops-153628},
doi = {10.4230/LIPIcs.CALCO.2021.7},
annote = {Keywords: Quantitative equational theories, Tensor, Monads, Quantitative Effects}
}
Keywords: |
|
Quantitative equational theories, Tensor, Monads, Quantitative Effects |
Collection: |
|
9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021) |
Issue Date: |
|
2021 |
Date of publication: |
|
08.11.2021 |