A New Foundation for Finitary Corecursion - The Locally Finite Fixpoint and Its Properties
A New Foundation for Finitary Corecursion - The Locally Finite Fixpoint and Its Properties
复制标题
有限核心递归的新基础——局部有限不动点及其性质
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Thorsten Wißmann
中科院分区：
文献类型：
--
作者：
Stefan Milius;D. Pattinson;Thorsten Wißmann
本文有助于理论的行为的“有限状态”系统是通用的系统类型。我们建议，这样的系统被建模为一个局部可表示范畴上的endofunctor的余代数与一个可生成的载体。他们的行为产生了一个新的不动点的coalgebraic型函子称为局部有限不动点（LFF）。我们证明，如果给定的endofunctor保持单态，那么LFF总是存在的，是一个子余代数的最终余代数（不像以前研究的合理不动点Adamek，Milius和Velebil）。此外，我们表明，LFF的特点是由两个普遍的性质：1。作为最后的本地生成的余代数，和2。作为初始FG-迭代代数。作为LFF的实例，我们首先获得了有理不动点的已知实例，例如正则语言，有理流和形式幂级数，正则树等，并且我们获得了一些新的例子，例如（实时确定性的resp.非确定性）上下文无关语言，建设性的S-代数形式幂级数（以及Silva，Bonchi，Bonsangue和Rutten的广义幂集构造的任何其他实例）和Courcelle代数树的单子。
This paper contributes to a theory of the behaviour of “finite-state” 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 Adamek, 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.