Bialgebraic Semantics and Recursion

In previous work with Turi a unifying framework was given for operational and denotational semantics and (strong) bisimulation. It uses bialgebras, which are combinations of algebras (used for syntax and denotational semantics) and coalgebras (used for operational semantics and solutions to domain equations). We report progress on the problem of adapting that framework to include recursion.

A number of difficulties 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 was not yet completely satisfactory because of well-known difficulties involved in prebisimulations. It seems that a a kind of testing equivalence (already implicit in previous work) works generally, though all details have yet to be verified!