Distributive Laws for Monotone Specifications

TL;DR

This paper explores how monotone specifications, which exclude negative premises, can be integrated within a categorical framework to ensure unique, compositional semantics through distributive laws.

Contribution

It demonstrates that monotone specifications induce a canonical distributive law, enabling unique and compositional interpretations in the categorical semantics framework.

Findings

Monotone specifications induce a canonical distributive law.

Unique, compositional interpretation is achieved for monotone specifications.

The approach extends the categorical semantics framework to include monotone rules.

Abstract

Turi and Plotkin introduced an elegant approach to structural operational semantics based on universal coalgebra, parametric in the type of syntax and the type of behaviour. Their framework includes abstract GSOS, a categorical generalisation of the classical GSOS rule format, as well as its categorical dual, coGSOS. Both formats are well behaved, in the sense that each specification has a unique model on which behavioural equivalence is a congruence. Unfortunately, the combination of the two formats does not feature these desirable properties. We show that monotone specifications - that disallow negative premises - do induce a canonical distributive law of a monad over a comonad, and therefore a unique, compositional interpretation.