Bialgebraic Semantics and Recursion
Date
2001Author
Plotkin, Gordon
Metadata
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.