Giorgio Bacci ; Radu Mardare ; Prakash Panangaden ; Gordon Plotkin - Sum and Tensor of Quantitative Effects

lmcs:10761 - Logical Methods in Computer Science, October 29, 2024, Volume 20, Issue 4 - https://doi.org/10.46298/lmcs-20(4:9)2024
Sum and Tensor of Quantitative EffectsArticle

Authors: Giorgio Bacci ORCID; Radu Mardare ORCID; Prakash Panangaden ; Gordon Plotkin

    Inspired by the seminal work of Hyland, Plotkin, and Power on the combination of algebraic computational effects via sum and tensor, we develop an analogous theory for the combination of quantitative algebraic effects. Quantitative algebraic effects are monadic computational effects on categories of metric spaces, which, moreover, have an algebraic presentation in the form of quantitative equational theories, a logical framework introduced by Mardare, Panangaden, and Plotkin that generalises equational logic to account for a concept of approximate equality. As our main result, we show that the sum and tensor of two quantitative equational theories correspond to the categorical sum (i.e., coproduct) and tensor, respectively, of their effects qua monads. We further give a theory of quantitative effect transformers based on these two operations, essentially providing quantitative analogues to the following monad transformers due to Moggi: exception, resumption, reader, and writer transformers. Finally, as an application, we provide the first quantitative algebraic axiomatizations to the following coalgebraic structures: Markov processes, labelled Markov processes, Mealy machines, and Markov decision processes, each endowed with their respective bisimilarity metrics. Apart from the intrinsic interest in these axiomatizations, it is pleasing they have been obtained as the composition, via sum and tensor, of simpler quantitative equational theories.


    Volume: Volume 20, Issue 4
    Published on: October 29, 2024
    Accepted on: August 23, 2024
    Submitted on: January 3, 2023
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 446 times.
    This article's PDF has been downloaded 250 times.