Presenting with Quantitative Inequational Theories

TL;DR

This paper explores algebraic presentations of process calculi using quantitative monads in ordered categories, extending the framework beyond sets to include ordered semirings for modeling recursive and probabilistic systems.

Contribution

It introduces conditions for lifting monads on sets to ordered categories, focusing on quantitative monads like free modules over ordered semirings, and discusses their applications.

Findings

Conditions for lifting monads to ordered categories

Examples include ordered probability theory and semilattices

Framework supports modeling recursive and probabilistic processes

Abstract

It came to the attention of myself and the coauthors of (S., Rozowski, Silva, Rot, 2022) that a number of process calculi can be obtained by algebraically presenting the branching structure of the transition systems they specify. Labelled transition systems, for example, branch into sets of transitions, terms in the free semilattice generated by the transitions. Interpreting equational theories in the category of sets has undesirable limitations, and we would like to have more examples of presentations in other categories. In this brief article, I discuss monad presentations in the category of partially ordered sets and monotone maps. I focus on quantitative monads, namely free modules over ordered semirings, and give sufficient conditions for one of these to lift a monad on the category of sets. I also give a description of ordered semirings that are useful for specifying unguarded recursive calls. Examples include ordered probability theory and ordered semilattices.