Bialgebraic Semantics and Recursion

Abstract

In [9] a unifying framework was given for operational and denotational semantics. It uses bialgebras, which are combinations of algebras (used for syn- tax and denotational semantics) and coalgebras (used for operational semantics and solutions to domain equations). Here we report progress on the problem of adapting that framework to include recursion. A number of di culties were encountered. An expected one was the need to treat orders in the general theory; much less expected was the need to give up defining bisimulations in terms of spans of functional bisimulations, and move to a relational view. Even so the outcome is not yet satisfactory because of well-known diffculties involved in prebisimulations. Our work can be compared to, e.g., that of [2]. The principal difference is that we aim, following [9], at a conceptual overview of the area using appropriate categorical tools. The main idea of [9] is to represent rules for operational semantics by a natural transformation: : (X BX) ! BTX where is the signature functor associated to an algebraic signature of the same name, B is a behaviour functor and T is the term monad associated to . For suitable 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 X ! X ! BX satisfying a suitable pentagonal condition. The category of these models has an initial object consisting of the programming language L = L and its op- erational semantics L ! BL. Every model gives an adequate compositional denotational semantics for the language L. Suppose now that the final coalgebra M = 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 object which incorporates a semantic algebra M ! M. One can model bisimulation by spans of coalgebra maps (first done in [3]). With this, under mild conditions, one has that the semantics given by the final coalgebra is fully abstract and that there is a greatest bisimulation which is a congruence. These conditions are that kernel pairs exist and that weak kernel pairs are preserved by B.