Bialgebraic Semantics and Recursion

The main idea of [9] is to represent rules for operational semantics by anatural transformation: ae: \Sigma (X * BX) ! BT X where \Sigma is the signature functor associated to an algebraic signature of the samename, B is a behaviour functor and T is the term monad associated to \Sigma. Forsuitable choices of these over the category of sets, image-finite sets of rules in GSOS format yield such natural transformations.Models of such rules are bialgebras \Sigma X ff! X fl! BX satisfying a suitable pentagonal condition. The category of these models has an initial object consisting of the programming language \Sigma L ', = L and its operational semantics L fl! BL. Every model gives an adequate compositionaldenotational semantics for the language L. Suppose now that the final coalgebra M oe, = BM exists; it can be thought of as the solution to the "domain equation" X, = BX in the category at hand. Then it automatically gives a final objectwhich incorporates a semantic algebra \Sigma M ff! M.One can model bisimulation by spans of coalgebra maps (first done in [3])