Bialgebraic Semantics and Recursion
MetadataShow full item record
In  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 . The principal difference is that we aim, following , at a conceptual overview of the area using appropriate categorical tools. The main idea of  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 ). 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.