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. ...

翻译：在基于状态的系统上证明行为等价关于代数运算的组合性是一个经典且被广泛研究的问题。我们研究了该问题的范畴论表述，其中通过函子间的分配律可以优雅地捕捉以余代数建模的基于状态系统上的运算。为证明组合性，只需证明该分配律可从集合提升至关系，从而解释如何组合较小系统上的行为等价以获得复合系统上的行为等价。在本文中，我们通过聚焦于函子的所谓密度提升来改进此方法，这为各种（双）相似性概念以及定量概念（如概率系统上的行为度量）提供了非常通用的表述。关键思想是在代数和余代数两个层面均使用密度提升，这借助于一种新的密度提升推广。分配律的提升问题于是简化为在密度提升间构造分配律的抽象问题，对此我们提出了一个简化的充分条件。我们的充分条件可实例化为针对各类基于状态系统上代数运算组合性的具体证明方法。我们将结果实例化，以证明确定性自动机的定性与定量性质的组合性。我们还通过包含一个概率系统的例子来探索我们方法的边界，在该例中尚不清楚充分条件是否成立；相反，我们利用我们的框架直接给出了组合性的证明。...