Adding recursive constructs to bialgebraic semantics

AbstractThis paper aims at fitting a general class of recursive equations into the framework of `well-behaved' structural operational semantics, formalized as bialgebraic semantics by Turi and Plotkin. Rather than interpreting recursive constructs by means of operational rules, separate recursive equations are added to semantic descriptions of languages. The equations, together with the remaining rules, are then interpreted in a suitable category and merged by means of certain fixpoint constructions. For a class of recursive equations called regular unfolding rules, this construction yields distributive laws as analyzed by Turi and Plotkin. This means that regular unfolding rules can be merged seamlessly with abstract operational rules