Tensor of Quantitative Equational Theories

Giorgio Bacci, Radu Mardare, Prakash Panangaden, Gordon Plotkin

Research output: Contribution to journalConference article in JournalResearchpeer-review

2 Downloads (Pure)

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.
Original languageEnglish
Article number7
JournalLeibniz International Proceedings in Informatics
Volume211
Pages (from-to)7:1-7:17
Number of pages17
ISSN1868-8969
DOIs
Publication statusPublished - 2021
Event9th Conference on Algebra and Coalgebra in Computer Science - Salzburg, Austria
Duration: 30 Aug 20213 Sep 2021
Conference number: 9
https://www.coalg.org/calco-mfps2021/calco/

Conference

Conference9th Conference on Algebra and Coalgebra in Computer Science
Number9
Country/TerritoryAustria
CitySalzburg
Period30/08/202103/09/2021
Internet address

Keywords

  • Quantitative equational theories
  • Tensor
  • Monads
  • Quantitative Effects

Fingerprint

Dive into the research topics of 'Tensor of Quantitative Equational Theories'. Together they form a unique fingerprint.

Cite this