pith. sign in

arxiv: 2605.18285 · v1 · pith:P6H2ATK4new · submitted 2026-05-18 · 💻 cs.LO

Compositionality in Coalgebraic Trace Semantics

Robin Jourde , Henning Urbat , Sergey Goncharov , Stelios Tsampas , Jonas Forster This is my paper

Pith reviewed 2026-05-19 23:47 UTC · model grok-4.3

classification 💻 cs.LO
keywords compositionalitycoalgebraic trace semanticsGSOS lawsDe Simone rulesKleisli categoriesprocess algebraprobabilistic systemsrule formats
0
0 comments X

The pith

De Simone laws over Kleisli categories ensure operational models are compositional for coalgebraic trace equivalence.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that a refined form of abstract GSOS can guarantee compositionality for trace equivalence rather than only strong bisimilarity. It introduces De Simone laws as GSOS laws over Kleisli categories and shows that the resulting operational models respect trace equivalence under language constructors. A sympathetic reader would care because trace equivalence is a practical, coarser notion of behavior that observes only external actions, and having a general categorical method to ensure it is a congruence simplifies verification of process languages. The approach recovers the classical De Simone format for labelled transition systems and produces a new rule format for probabilistic systems that is compositional for probabilistic traces.

Core claim

De Simone laws are GSOS laws over Kleisli categories that obey refined naturality conditions. Their operational models are compositional for coalgebraic trace equivalence. This recovers and explains the compositionality of the well-known De Simone rule format for labelled transition systems and yields a novel De Simone-type format for probabilistic systems that is compositional for probabilistic trace equivalence.

What carries the argument

De Simone laws, a type of GSOS laws over Kleisli categories satisfying refined naturality conditions, that carry the compositionality proof for coalgebraic trace semantics.

If this is right

  • Operational models of De Simone laws are compositional for coalgebraic trace equivalence.
  • The classical De Simone rule format for labelled transition systems is compositional for trace equivalence as a special case.
  • A new De Simone-type rule format exists for probabilistic systems that is compositional for probabilistic trace equivalence.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same categorical approach could produce compositional rule formats for other monads and coalgebraic semantics beyond traces and probabilities.
  • The refined naturality conditions might be adapted to derive compositionality results for additional process equivalences such as weak or branching variants.

Load-bearing premise

The refined naturality conditions on GSOS laws are sufficient to make abstract GSOS applicable over Kleisli categories for trace semantics.

What would settle it

A concrete GSOS law over a Kleisli category that meets the refined naturality conditions but whose operational model fails to preserve coalgebraic trace equivalence under composition.

read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper extends Turi and Plotkin's abstract GSOS framework by refining the naturality conditions on GSOS laws to make them applicable over Kleisli categories. It introduces De Simone laws as a specific class of such laws and proves that the induced operational models are compositional for coalgebraic trace equivalence. The main results recover the classical De Simone rule format for labelled transition systems and derive a novel De Simone-type format for probabilistic systems that guarantees compositionality with respect to probabilistic trace equivalence.

Significance. If the results hold, the work provides a uniform bialgebraic account of compositionality for trace semantics, extending beyond strong bisimilarity. It explains existing rule formats categorically and yields a new format for probabilistic processes. The refined presentation of the general compositionality theorem and the explicit construction of De Simone laws over Kleisli categories are clear strengths that could support further applications in coalgebraic process theory.

major comments (1)
  1. [§4, Theorem 4.12] §4, Theorem 4.12: The lifting of the bialgebraic construction to the Kleisli category is claimed to follow directly from the refined naturality conditions on the GSOS law. However, the argument appears to assume without further verification that Kleisli composition preserves the naturality squares for the trace functor and that the final coalgebra exists in the Kleisli category for arbitrary monads. This assumption is load-bearing for the central claim that the operational model is compositional for coalgebraic trace equivalence; a counterexample or additional monad-specific hypothesis would be needed if the lifting fails in general.
minor comments (2)
  1. [§3.2] §3.2: The notation for the Kleisli lift of the GSOS law could be clarified by explicitly distinguishing the base-category and Kleisli-category versions of the naturality diagrams.
  2. The paper would benefit from a short table comparing the original De Simone rules, the categorical De Simone laws, and the probabilistic variant to make the generalization more immediately visible.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful reading of the manuscript and for the constructive major comment. We address it point by point below and will incorporate the suggested clarifications in the revised version.

read point-by-point responses

  1. Referee: [§4, Theorem 4.12] §4, Theorem 4.12: The lifting of the bialgebraic construction to the Kleisli category is claimed to follow directly from the refined naturality conditions on the GSOS law. However, the argument appears to assume without further verification that Kleisli composition preserves the naturality squares for the trace functor and that the final coalgebra exists in the Kleisli category for arbitrary monads. This assumption is load-bearing for the central claim that the operational model is compositional for coalgebraic trace equivalence; a counterexample or additional monad-specific hypothesis would be needed if the lifting fails in general.

    Authors: We agree that the existence of a final coalgebra in the Kleisli category cannot be assumed for arbitrary monads and must be stated explicitly as a hypothesis. The refined naturality conditions on the GSOS law are introduced precisely so that the bialgebraic construction lifts to the Kleisli category while preserving the relevant naturality squares for the trace functor; Kleisli composition is compatible with these squares by the definition of the Kleisli category and the functoriality of the monad. We will revise Theorem 4.12 to include the final-coalgebra hypothesis and expand the proof with an explicit verification that the naturality squares are preserved under Kleisli composition. These changes clarify the argument without affecting the main results or the applications to LTSs and probabilistic systems. revision: yes

Circularity Check

0 steps flagged

No circularity; derivation extends independent categorical framework

full rationale

The paper refines naturality conditions from the external Turi-Plotkin abstract GSOS theory to enable application over Kleisli categories, then defines De Simone laws as a specific instance of GSOS laws in that setting and proves compositionality for coalgebraic trace equivalence. This recovers the classical De Simone format as a special case via standard bialgebraic constructions. No step reduces by construction to a fitted parameter, self-definition, or load-bearing self-citation chain; the central claims rest on independent coalgebraic and Kleisli-category machinery with external grounding.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work relies on standard background from coalgebra, Kleisli categories, and the original abstract GSOS theory; no free parameters, ad-hoc axioms, or invented entities are introduced in the abstract.

axioms (1)
  • domain assumption Naturality conditions on GSOS laws suffice for Kleisli-category applicability
    Invoked to extend the original Turi-Plotkin result to trace semantics.

pith-pipeline@v0.9.0 · 5770 in / 1110 out tokens · 40691 ms · 2026-05-19T23:47:23.938534+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

14 extracted references · 14 canonical work pages

  1. [1]

    2 Faris Abou-Saleh.A coalgebraic semantics for imperative programming languages

    1 Structural operational semantics for stochastic and weighted transition systems.Information and Computation, 227:58–83, 2013.doi:10.1016/j.ic.2013.04.001. 2 Faris Abou-Saleh.A coalgebraic semantics for imperative programming languages. PhD thesis, Imperial College London, UK,

    work page doi:10.1016/j.ic.2013.04.001 2013

  2. [3]

    Springer, 2013.doi:10.1007/978-3-642-37075-5\_9

    Proceedings, volume 7794 ofLecture Notes in Computer Science, pages 129–144. Springer, 2013.doi:10.1007/978-3-642-37075-5\_9. 5 Luca Aceto, Wan J. Fokkink, and Chris Verhoef. Structural operational semantics. In Jan A. Bergstra, Alban Ponse, and Scott A. Smolka, editors,Handbook of Process Algebra, pages 197–292. North-Holland / Elsevier, 2001.doi:10.1016...

    work page doi:10.1007/978-3-642-37075-5 2013

  3. [4]

    GSOS for probabilistic transition systems

    10 Falk Bartels. GSOS for probabilistic transition systems. In Lawrence S. Moss, editor, Coalgebraic Methods in Computer Science, CMCS 2002, Satellite Event of ETAPS 2002, Grenoble, France, April 6-7, 2002, volume 65 ofElectronic Notes in Theoretical Computer Science, pages 29–53. Elsevier, 2002.doi:10.1016/S1571-0661(04)80358-X. 11 Falk Bartels.On genera...

    work page doi:10.1016/s1571-0661(04)80358-x 2002

  4. [5]

    When is partial trace equivalence adequate? 6(3):317–338, 1994.doi:10.1007/ BF01215409

    12 Bard Bloom. When is partial trace equivalence adequate? 6(3):317–338, 1994.doi:10.1007/ BF01215409. 13 Bard Bloom, Sorin Istrail, and Albert R. Meyer. Bisimulation can’t be traced.J. ACM, 42(1):232–268, 1995.doi:10.1145/200836.200876. 14 Filippo Bonchi, Barbara König, and Daniela Petrisan. Up-to techniques for behavioural metrics via fibrations. In Sve...

    work page doi:10.1145/200836.200876 1994

  5. [6]

    16 Valentina Castiglioni, Ruggero Lanotte, and Simone Tini

    doi:10.1016/j.jlamp.2015.09.002. 16 Valentina Castiglioni, Ruggero Lanotte, and Simone Tini. Back to the format: A survey on sos for probabilistic processes.Journal of Logical and Algebraic Methods in Programming, 137:100929, 2024.doi:10.1016/j.jlamp.2023.100929. 17 Kenta Cho and Bart Jacobs. Disintegration and Bayesian inversion via string diagrams. Math...

    work page doi:10.1016/j.jlamp.2015.09.002 2015

  6. [7]

    2013 , isbn =

    arXiv:1709.00322.doi:10.1017/ S0960129518000488. 18 Compositionality in Coalgebraic Trace Semantics 18 Dion Coumans and Bart Jacobs. Scalars, monads, and categories. InQuantum Physics and Linguistics - A Compositional, Diagrammatic Discourse, pages 184–216. Oxford University Press, 2013.doi:10.1093/ACPROF:OSO/9780199646296.003.0007. 19 R. de Simone. Highe...

    work page doi:10.1093/acprof:oso/9780199646296.003.0007 2013

  7. [8]

    Coalgebraic semantics for nominal automata

    21 Florian Frank, Stefan Milius, and Henning Urbat. Coalgebraic semantics for nominal automata. InCoalgebraic Methods in Computer Science - 16th IFIP WG 1.3 International Workshop, CMCS 2022, Colocated with ETAPS 2022, Munich, Germany, April 2-3, 2022, Proceedings, volume 13225 ofLecture Notes in Computer Science, pages 45–66. Springer, 2022.doi: 10.1007/...

    work page doi:10.1007/978-3-031-10736-8 2022

  8. [9]

    23 Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat

    arXiv:1908.07021.doi:10.1016/ j.aim.2020.107239. 23 Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat. Stateful structural operational semantics. In Amy P. Felty, editor,7th International Conference on Formal Structures for Computation and Deduction, FSCD’22, volume 228 ofLIPIcs, pages 30:1–30:19. Schloss Dagstuhl - Leibni...

    work page doi:10.4230/lipics 1908

  9. [10]

    ICFP 2025.arXiv:2503.10955

    To appear in Proc. ICFP 2025.arXiv:2503.10955. 26 Jan Friso Groote and Frits W. Vaandrager. Structured operational semantics and bisimulation as a congruence.Inf. Comput., 100(2):202–260, 1992.doi:10.1016/0890-5401(92)90013-6. 27 Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic trace semantics via coinduction.Logical Methods in Computer Science, 3(4),...

    work page doi:10.1016/0890-5401(92)90013-6 2025

  10. [11]

    Structural operational semantics and modal logic, revisited

    31 Bartek Klin. Structural operational semantics and modal logic, revisited. InProceedings of the Tenth Workshop on Coalgebraic Methods in Computer Science, CMCS@ETAPS 2010, Paphos, Cyprus, March 26-28, 2010, number 2 in Electronic Notes in Theoretical Computer Science, pages 155–175. Elsevier,

    work page 2010

  11. [12]

    Bialgebras for structural operational semantics: An introduction.Theor

    32 Bartek Klin. Bialgebras for structural operational semantics: An introduction.Theor. Comput. Sci., 412(38):5043–5069, 2011.doi:10.1016/j.tcs.2011.03.023. 33 Bartek Klin and Vladimiro Sassone. Structural operational semantics for stochastic process calculi. In Roberto M. Amadio, editor,11th International Conference Foundations of Software Science and Co...

    work page doi:10.1016/j.tcs.2011.03.023 2011

  12. [13]

    19 36 Paul Blain Levy and Sergey Goncharov

    Jourde et al. 19 36 Paul Blain Levy and Sergey Goncharov. Coinductive resumption monads: Guarded iterative and guarded elgot. InProc. 8rd international conference on Algebra and coalgebra in computer science (CALCO 2019), LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,

    work page 2019

  13. [14]

    Chudnovsky and S

    URL: http://link.springer.com/10.1007/ 978-1-4757-4721-8. 39 Marino Miculan and Marco Peressotti. Structural operational semantics for non-deterministic processes with quantitative aspects.Theor. Comput. Sci., 655:135–154, 2016.doi:10.1016/j. tcs.2016.01.012. 40 Philip S. Mulry. Lifting theorems for kleisli categories. InMathematical Foundations of Progra...

    work page doi:10.1016/j 2016

  14. [15]

    45 Henning Urbat

    doi:10.1109/LICS.1997.614955. 45 Henning Urbat. Higher-order behavioural conformances via fibrations.Proc. ACM Program. Lang., 10(POPL), January 2026.doi:10.1145/3776697. 46 R. J. van Glabbeek. The linear time - branching time spectrum. InCONCUR ’90 Theories of Concurrency: Unification and Extension, pages 278–297. Springer,

    work page doi:10.1109/lics.1997.614955 1997