ridm@nrct.go.th   ระบบคลังข้อมูลงานวิจัยไทย   รายการโปรดที่คุณเลือกไว้

Bialgebraic Semantics and Recursion

หน่วยงาน Edinburgh Research Archive, United Kingdom

รายละเอียด

ชื่อเรื่อง : 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.