Edinburgh Research Archive logo

Edinburgh Research Archive

University of Edinburgh homecrest
View Item 
  •   ERA Home
  • Informatics, School of
  • Informatics Publications
  • View Item
  •   ERA Home
  • Informatics, School of
  • Informatics Publications
  • View Item
  • Login
JavaScript is disabled for your browser. Some features of this site may not work without it.

Bialgebraic Semantics and Recursion

View/Open
Recursion_Math_Op_Sems_Abstract.pdf (100.7Kb)
Date
2001
Author
Plotkin, Gordon
Metadata
Show full item record
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.
URI
http://hdl.handle.net/1842/194
Collections
  • Informatics Publications

Library & University Collections HomeUniversity of Edinburgh Information Services Home
Privacy & Cookies | Takedown Policy | Accessibility | Contact
Privacy & Cookies
Takedown Policy
Accessibility
Contact
feed RSS Feeds

RSS Feed not available for this page

 

 

All of ERACommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsPublication TypeSponsorSupervisorsThis CollectionBy Issue DateAuthorsTitlesSubjectsPublication TypeSponsorSupervisors
LoginRegister

Library & University Collections HomeUniversity of Edinburgh Information Services Home
Privacy & Cookies | Takedown Policy | Accessibility | Contact
Privacy & Cookies
Takedown Policy
Accessibility
Contact
feed RSS Feeds

RSS Feed not available for this page