Sum and Tensor of Quantitative Effects

TL;DR

This paper develops a theory for combining quantitative algebraic effects using sum and tensor operations, extending categorical and logical frameworks to metric spaces and providing new axiomatizations for probabilistic and automata models.

Contribution

It introduces a novel theory linking sum and tensor of quantitative equational theories to categorical effects, and applies this to axiomatize probabilistic and automata-based structures.

Findings

Sum and tensor of theories correspond to categorical sum and tensor of effects.

Provides quantitative effect transformers analogous to classical monad transformers.

First quantitative axiomatizations for Markov processes, labelled Markov processes, Mealy machines, and MDPs.

Abstract

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.