Guarded Recursion and Mathematical Operational Semantics

Operational semantics gives meaning to terms in a programming language by defining a transition relation which represents execution steps. In structural operational semantics (SOS) this transition relation is given by a set of rules defined on the structure of the terms of the language. But, when is a collec-tion of rules satisfactory, in the sense that it defines a well-behaved operational semantics? Before the introduction of Mathematical Operational Semantics by Turi [2], there were many attempts to conceive a theory of operational semantics in the form of syntactic rule formats. These results were specific to a particular type of transition relation, strongly syntactic, and therefore difficult to generalize and adapt to other settings. Turi stripped operational semantics to its bare bones, ignoring concrete syntax to focus on its structure and, as a result, giving us a clean categorical reformulation of SOS. Under this interpretation, the SOS of a language is given by a distributive law of syntax over behaviour. If the operations in the language are given by a signature functor Σ and the behaviou