Proving compositionality of behavioral equivalence on state-based systems with respect to algebraic operations is a classical and widely studied problem. We study a categorical formulation of this problem, where operations on state-based systems modeled as coalgebras can be elegantly captured through distributive laws between functors. To prove compositionality, it then suffices to show that this distributive law lifts from sets to relations, giving an explanation of how behavioral equivalence on smaller systems can be combined to obtain behavioral equivalence on the composed system. In this paper, we refine this approach by focusing on so-called codensity lifting of functors, which gives a very generic presentation of various notions of (bi)similarity as well as quantitative notions such as behavioral metrics on probabilistic systems. The key idea is to use codensity liftings both at the level of algebras and coalgebras, using a new generalization of the codensity lifting. The problem of lifting distributive laws then reduces to the abstract problem of constructing distributive laws between codensity liftings, for which we propose a simplified sufficient condition. Our sufficient condition instantiates to concrete proof methods for compositionality of algebraic operations on various types of state-based systems. We instantiate our results to prove compositionality of qualitative and quantitative properties of deterministic automata. We also explore the limits of our approach by including an example of probabilistic systems, where it is unclear whether the sufficient condition holds, and instead we use our setting to give a direct proof of compositionality. ...

翻译：关于状态基系统上行为等价性在代数运算下的组合性，这是一个经典且被广泛研究的问题。我们研究该问题的范畴形式化表述，其中通过函子间的分配律可以优雅地捕捉到建模为余代数的状态基系统上的运算。为证明组合性，只需证明该分配律从集合提升到关系，从而解释如何将较小系统上的行为等价性组合以得到复合系统上的行为等价性。在本文中，我们通过聚焦于所谓的函子余密度提升来改进该方法，该提升不仅给出了各种（互）相似性概念的非常通用的表示，还给出了概率系统上行为度量等定量概念。关键思想是同时在代数和余代数层次上使用余密度提升，这依赖于余密度提升的新推广。分配律的提升问题随后简化为构造余密度提升间分配律的抽象问题，为此我们提出一个简化的充分条件。该充分条件可实例化为不同类型状态基系统上代数运算组合性的具体证明方法。我们通过实例化结果证明了确定性自动机定性与定量性质的组合性。此外，我们通过包含一个概率系统的实例来探索该方法的局限性——在该实例中充分条件是否成立尚不明确，转而利用我们的框架给出组合性的直接证明。……