Bialgebras for structural operational semantics: an introduction (Q639646)

As indicated in the title, this work provides an introduction to the use of bialgebras in structural operational semantics (SOS). Starting from very basic examples, it arrives at giving an up-to-date overview of the state of the art in the field. The underlying principle of bialgebraic semantics [\textit{D. Turi} and \textit{G. Plotkin}, ``Towards a mathematical operational semantics'', in: Proceedings of the twelfth annual IEEE symposium on logic in computer science, LICS '97. Los Alamitos, CA: IEEE Computer Society Press. 280--291 (1997)] is to formulate structural operational rules categorically as various types of distributive laws between a syntax functor on the one hand and a behaviour functor on the other hand; the syntax functor essentially describes the language of a process algebra, while the behaviour functor encodes a coalgebraic model of the denotational semantics. The distribute law induces a denotational semantics for the associated process algebra and guarantees that behavioural equivalence is a congruence. The material is organized in ascending order of the expressive strength of such laws, corresponding, on the categorical side, to the use of functors with more structure (such as monads instead of plain functors), and, on the SOS side, to increasingly permissive rule formats. The exposition begins with distributive laws among plain functors, and culminates with GSOS (generalized structural operational semantics) and coGSOS laws, in which the syntax functor is promoted to a monad and the behaviour functor to a comonad, respectively. Intermediate stages involve pointed and copointed functors. Most examples use the simplest possible behaviour functor, the functor \(\lambda X.X\times A\) describing infinite streams over \(A\); additionally, GSOS laws for Mealy machines, labelled transition systems, and reactive probabilistic transition systems are discussed.