Stefan Milius ; Lawrence S Moss ; Daniel Schwencke - Abstract GSOS Rules and a Modular Treatment of Recursive Definitions

lmcs:1180 - Logical Methods in Computer Science, September 30, 2013, Volume 9, Issue 3 - https://doi.org/10.2168/LMCS-9(3:28)2013
Abstract GSOS Rules and a Modular Treatment of Recursive Definitions

Authors: Stefan Milius ; Lawrence S Moss ; Daniel Schwencke

    Terminal coalgebras for a functor serve as semantic domains for state-based systems of various types. For example, behaviors of CCS processes, streams, infinite trees, formal languages and non-well-founded sets form terminal coalgebras. We present a uniform account of the semantics of recursive definitions in terminal coalgebras by combining two ideas: (1) abstract GSOS rules l specify additional algebraic operations on a terminal coalgebra; (2) terminal coalgebras are also initial completely iterative algebras (cias). We also show that an abstract GSOS rule leads to new extended cia structures on the terminal coalgebra. Then we formalize recursive function definitions involving given operations specified by l as recursive program schemes for l, and we prove that unique solutions exist in the extended cias. From our results it follows that the solutions of recursive (function) definitions in terminal coalgebras may be used in subsequent recursive definitions which still have unique solutions. We call this principle modularity. We illustrate our results by the five concrete terminal coalgebras mentioned above, e.\,g., a finite stream circuit defines a unique stream function.


    Volume: Volume 9, Issue 3
    Published on: September 30, 2013
    Accepted on: June 25, 2015
    Submitted on: December 8, 2010
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Category Theory

    Linked data

    Source : ScholeXplorer IsReferencedBy DOI 10.1007/978-3-319-66167-4_1
    Source : ScholeXplorer IsReferencedBy DOI 10.5281/zenodo.3228083
    Source : ScholeXplorer IsReferencedBy DOI 10.5281/zenodo.3228084
    Source : ScholeXplorer IsReferencedBy HANDLE 1871.1/bda0766d-256c-487b-ba33-935c32a65336
    • 1871.1/bda0766d-256c-487b-ba33-935c32a65336
    • 10.5281/zenodo.3228084
    • 10.1007/978-3-319-66167-4_1
    • 10.1007/978-3-319-66167-4_1
    • 10.1007/978-3-319-66167-4_1
    • 10.5281/zenodo.3228083
    Foundational (co)datatypes and (co)recursion for higher-order logic
    Biendarra, Julian ; Blanchette, Jasmin Christian ; Bouzy, Aymeric ; Desharnais, Martin ; Fleury, Mathias ; Hölzl, Johannes ; Kunčar, Ondřej ; Lochbihler, Andreas ; Meier, Fabian ; Panny, Lorenz ; Popescu, Andrei ; Sternagel, Christian ; Thiemann, René ; Traytel, Dmitriy ; Dixon, C. ; Finger, M. ;

    14 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 391 times.
    This article's PDF has been downloaded 275 times.