Distributive Laws and Decidable Properties of SOS Specifications
Bartek Klin, Beata Nachy{\l}a
TL;DR
This paper explores the theoretical framework of distributive laws in operational semantics, showing that their generalization does not lead to practical rule formats for combined GSOS and coGSOS specifications.
Contribution
It demonstrates that the generalization to distributive laws offers limited practical benefits for rule formats involving both GSOS and coGSOS rules.
Findings
Distributive laws do not translate into complete rule formats for mixed GSOS and coGSOS specifications.
Theoretical generalizations have limited practical applicability in operational semantics.
No concrete rule format derived from distributive laws covers all specifications with both GSOS and coGSOS rules.
Abstract
Some formats of well-behaved operational specifications, correspond to natural transformations of certain types (for example, GSOS and coGSOS laws). These transformations have a common generalization: distributive laws of monads over comonads. We prove that this elegant theoretical generalization has limited practical benefits: it does not translate to any concrete rule format that would be complete for specifications that contain both GSOS and coGSOS rules. This is shown for the case of labeled transition systems and deterministic stream systems.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.