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.
翻译:众所周知,Kleisli范畴为副作用建模提供了一种自然语言。例如,在余代数理论中,当非确定性自动机被建模为存在于幂集单子Kleisli范畴中的余代数时,行为等价便与语言等价(而非互模拟)相一致。本文旨在为带/不带升级的条件转移系统建立基于语言等价与就绪等价的装饰迹语义。为此,我们将条件转移系统建模为存在于相对单子Kleisli范畴中的余代数。我们的成果包含两方面:首先,我们将相对单子背景下机器自函子的Kleisli提升问题归结为经典的Kleisli提升概念;其次,我们提出一种基于索引范畴的通用方法,用于为一般自函子构造Kleisli提升。