Approximation of Nested Fixpoints - A Coalgebraic View of Parametric Dataypes
Approximation of Nested Fixpoints - A Coalgebraic View of Parametric Dataypes
复制标题
嵌套不动点的近似 - 参数数据类型的代数视图
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
F. D. Vries
中科院分区：
文献类型：
--
作者：
A. Kurz;Alberto Pardo;Daniela Petrisan;P. Severi;F. D. Vries
本文解决的问题是如何正确地近似同时核心递归定义系统给出的无限数据。我们设计了一个分类框架来推理常规数据类型，即在产品、联产品和固定点下封闭的数据类型。我们认为，正确的方法一方面是余代数的（处理可能的非终止和无限数据），另一方面是二分类的（以严格的方式处理参数）。我们证明了 Beki£ 引理的联合代数版本，它允许我们将同时固定点减少到单个固定点。因此，可能无限的感兴趣对象被视为多排序多项式函子的最终余代数，并且可以被视为有限近似值的极限。作为一个应用程序，我们证明了计算一大类数据类型的近似值的通用函数的正确性。 1998 ACM 学科分类 F.3.2 编程语言的语义
The question addressed in this paper is how to correctly approximate infinite data given by systems of simultaneous corecursive definitions. We devise a categorical framework for reasoning about regular datatypes, that is, datatypes closed under products, coproducts and fixpoints. We argue that the right methodology is on one hand coalgebraic (to deal with possible nontermination and infinite data) and on the other hand 2-categorical (to deal with parameters in a disciplined manner). We prove a coalgebraic version of Beki£ lemma that allows us to reduce simultaneous fixpoints to a single fix point. Thus a possibly infinite object of interest is regarded as a final coalgebra of a many-sorted polynomial functor and can be seen as a limit of finite approximants. As an application, we prove correctness of a generic function that calculates the approximants on a large class of data types. 1998 ACM Subject Classification F.3.2 Semantics of Programming Languages
具有保护递归的高效协同编程
影响因子：
--
作者：
Atkey R
通讯作者：
Atkey R