A new foundation for finitary corecursion the locally finite fixpoint and its properties

Stefan Milius, Dirk Pattinson, Thorsten Wißmann*

*Corresponding author for this work

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    10 Citations (Scopus)

    Abstract

    This paper contributes to a theory of the behaviour of “finitestate” systems that is generic in the system type. We propose that such systems are modeled as coalgebras with a finitely generated carrier for an endofunctor on a locally finitely presentable category. Their behaviour gives rise to a new fixpoint of the coalgebraic type functor called locally finite fixpoint (LFF). We prove that if the given endofunctor preserves monomorphisms then the LFF always exists and is a subcoalgebra of the final coalgebra (unlike the rational fixpoint previously studied by Adámek, Milius and Velebil). Moreover, we show that the LFF is characterized by two universal properties: 1. as the final locally finitely generated coalgebra, and 2. as the initial fg-iterative algebra. As instances of the LFF we first obtain the known instances of the rational fixpoint, e.g. regular languages, rational streams and formal power-series, regular trees etc. And we obtain a number of new examples, e.g. (realtime deterministic resp. non-deterministic) context-free languages, constructively S-algebraic formal power-series (and any other instance of the generalized powerset construction by Silva, Bonchi, Bonsangue, and Rutten) and the monad of Courcelle’s algebraic trees.

    Original languageEnglish
    Title of host publicationFoundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Proceedings
    EditorsChristof Löding, Bart Jacobs
    PublisherSpringer Verlag
    Pages107-125
    Number of pages19
    ISBN (Print)9783662496299
    DOIs
    Publication statusPublished - 2016
    Event19th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016 - Eindhoven, Netherlands
    Duration: 2 Apr 20168 Apr 2016

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume9634
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference19th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016
    Country/TerritoryNetherlands
    CityEindhoven
    Period2/04/168/04/16

    Fingerprint

    Dive into the research topics of 'A new foundation for finitary corecursion the locally finite fixpoint and its properties'. Together they form a unique fingerprint.

    Cite this