| ชื่อเรื่อง | : | Bialgebraic Semantics and Recursion , Bialgebraic Semantics and Recursion (Extended Abstract) |
| นักวิจัย | : | Plotkin, Gordon |
| คำค้น | : | Laboratory for Foundations of Computer Science |
| หน่วยงาน | : | Edinburgh Research Archive, United Kingdom |
| ผู้ร่วมงาน | : | - |
| ปีพิมพ์ | : | 2544 |
| อ้างอิง | : | Electronic Notes in Theoretical Computer Science 44 No. 1 (2001) , http://hdl.handle.net/1842/194 |
| ที่มา | : | - |
| ความเชี่ยวชาญ | : | - |
| ความสัมพันธ์ | : | - |
| ขอบเขตของเนื้อหา | : | - |
| บทคัดย่อ/คำอธิบาย | : | 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. |
| บรรณานุกรม | : |
Plotkin, Gordon . (2544). Bialgebraic Semantics and Recursion.
กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom . Plotkin, Gordon . 2544. "Bialgebraic Semantics and Recursion".
กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom . Plotkin, Gordon . "Bialgebraic Semantics and Recursion."
กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom , 2544. Print. Plotkin, Gordon . Bialgebraic Semantics and Recursion. กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom ; 2544.
|
