A key requirement on any well-behaved process language is its compositionality: behavioural equivalence of processes should be respected by the constructors of the language. Turi and Plotkin's abstract GSOS provides an elegant bialgebraic framework for modelling rule formats that guarantee compositionality from the outset. Their original results, however, are restricted to compositionality of strong bisimilarity, a rather fine-grained notion of process equivalence. In the present paper, we demonstrate that Turi and Plotkin's approach also applies to trace equivalence, which only observes external actions of processes. To this end, we revisit the general compositionality result of their original theory and present it in a refined form with regard to the required naturality conditions. This step makes abstract GSOS applicable over Kleisli categories and thereby enables reasoning about compositionality in the setting of coalgebraic trace semantics. As our main contribution, we introduce De Simone laws, a type of GSOS laws over Kleisli categories, and prove that their operational models are compositional for coalgebraic trace equivalence. This result recovers and explains compositionality of the well-known De Simone rule format for labelled transition systems in a natural categorical setting. As a further application, we derive from our general framework a novel De Simone-type format for probabilistic systems, compositional for probabilistic trace equivalence.

翻译：任何行为良好的进程语言的关键要求是其组合性：进程的行为等价性应被语言构造子所尊重。Turi与Plotkin的抽象GSOS提供了一个优雅的双代数框架，用于建模能从根本上保证组合性的规则格式。然而，他们最初的结果仅限于强互模拟等价（一种粒度较细的进程等价概念）的组合性。本文证明，Turi与Plotkin的方法同样适用于仅观察进程外部行为的迹等价。为此，我们重新审视其原始理论中的一般性组合性结果，并在所需的自然性条件方面以更精细的形式呈现该结果。这一步骤使得抽象GSOS可应用于Kleisli范畴，从而能够在余代数迹语义的设定下对组合性进行推理。作为我们的主要贡献，我们引入了De Simone律（一类在Kleisli范畴上的GSOS律），并证明其操作模型对于余代数迹等价具有组合性。该结果在自然的范畴论设定下恢复并解释了标号变迁系统中著名的De Simone规则格式的组合性。作为另一个应用，我们从一般框架中推导出概率系统的新型De Simone类型格式，该格式对概率迹等价具有组合性。