Daniel Luckhardt ; Harsh Beohar ; Sebastian Küpper - On Kleisli liftings and decorated trace semantics

entics:14751 - Electronic Notes in Theoretical Informatics and Computer Science, December 11, 2024, Volume 4 - Proceedings of MFPS XL - https://doi.org/10.46298/entics.14751
On Kleisli liftings and decorated trace semanticsArticle

Authors: Daniel Luckhardt ; Harsh Beohar ; Sebastian Küpper

    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.


    Volume: Volume 4 - Proceedings of MFPS XL
    Published on: December 11, 2024
    Accepted on: November 18, 2024
    Submitted on: November 14, 2024
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 19 times.
    This article's PDF has been downloaded 8 times.