On Kleisli liftings and decorated trace semantics
Daniel Luckhardt, Harsh Beohar, Sebastian Küpper
TL;DR
The paper addresses decorating trace semantics for conditional transition systems by casting CTSs as coalgebras in the Kleisli category of a relative monad $T^G$ and deriving a coinductive account of language, failure, and ready traces. It introduces two main technical contributions: first, a reduction showing that constructing a Kleisli lifting for the machine endofunctor in the relative-monad setting reduces to the classical Kleisli lifting notion, and second, a general recipe, framed in indexed categories, for building Kleisli liftings of general endofunctors. It then applies the theory to CTS, producing concrete semantics with final coalgebras whose carrier is ${oldsymbol A}^ op imes O$ and showcasing when language, failure, or ready equivalences coincide with behavioural equivalence. The work paves the way for extending decorated trace semantics to other monads and to probabilistic or weighted CTS variants, and connects to Freyd-style results on initial algebras and final coalgebras in Kleisli contexts.
Abstract
It is well known that Kleisli categories provide a natural language to model side effects. For instance, in the theory of coalgebras, behavioural equivalence coincides with language equivalence (instead of bisimilarity) when nondeterministic automata are modelled as coalgebras living in the Kleisli category of the powerset monad. In this paper, our aim is to establish decorated trace semantics based on language and ready equivalences for conditional transition systems (CTSs) with/without upgrades. To this end, we model CTSs as coalgebras living in the Kleisli category of a relative monad. Our results are twofold. First, we reduce the problem of defining a Kleisli lifting for the machine endofunctor in the context of a relative monad to the classical notion of Kleisli lifting. Second, we provide a recipe based on indexed categories to construct a Kleisli lifting for general endofunctors.