强共归纳数据类型上的 Comonadic 共递归

doi:10.3969/j.issn.1000-565X.2014.01.022

华南理工大学学报（自然科学版） ›› 2014, Vol. 42 ›› Issue (1): 128-134.doi: 10.3969/j.issn.1000-565X.2014.01.022

强共归纳数据类型上的 Comonadic 共递归

苏锦钿¹ 余珊珊²

1．华南理工大学计算机科学与工程学院，广东广州 510006; 2．广东药学院医药信息工程学院，广东广州 510006

收稿日期:2013-07-16 修回日期:2013-09-29 出版日期:2014-01-25 发布日期:2013-12-01
通信作者: 苏锦钿(1980-)，男，博士，副教授，主要从事形式化方法、形式语义、构件技术、共代数与双代数研究 E-mail:SuJD@scut.edu.cn
作者简介:苏锦钿(1980-)，男，博士，副教授，主要从事形式化方法、形式语义、构件技术、共代数与双代数研究．
基金资助:
国家自然科学基金资助项目(61103038);高等学校博士学科点专项科研基金资助项目(20100172120043);华南理工大学中央高校基本科研业务费专项资金资助项目(2013ZZ0055)

Comonadic Corecursions on Strong Coinductive Data Types

Su Jin- dian¹ Yu Shan- shan²

1.School of Computer Science and Engineering,South China University of Technology,Guangzhou 510006,Guangdong,China;2.College of Medical Information Engineering,Guangdong Pharmaceutical University,Guangzhou 510006,Guangdong,China

Received:2013-07-16 Revised:2013-09-29 Online:2014-01-25 Published:2013-12-01
Contact: 苏锦钿(1980-)，男，博士，副教授，主要从事形式化方法、形式语义、构件技术、共代数与双代数研究 E-mail:SuJD@scut.edu.cn
About author:苏锦钿(1980-)，男，博士，副教授，主要从事形式化方法、形式语义、构件技术、共代数与双代数研究
Supported by:
国家自然科学基金资助项目(61103038);高等学校博士学科点专项科研基金资助项目(20100172120043);华南理工大学中央高校基本科研业务费专项资金资助项目(2013ZZ0055)

摘要/Abstract

摘要： 针对共归纳数据类型上的 unfold 无法描述带参数的共递归计算的问题，首先证明了笛卡尔封闭范畴上的终结共代数是强终结的，并给出强共归纳数据类型的范畴论定义及其上一种带固定参数的共递归——punfold，使得共归纳数据类型上的共递归计算可以包含额外的参数作为计算的输入; 然后利用基于 Comonads 的 Comonadic 共递归给出了unfold 和 punfold 的一种统一的描述，并进一步分析了 punfold 上的各种计算律，从而将Pardo 对基于 Comonads 的带参数的递归计算研究扩展到共归纳数据类型．

关键词: 递归函子, 共归纳数据类型, 终结共代数, 共递归, Comonads

Abstract:

As the unfold on coinductive data types can not describe the corecursive functions with parameters,thefinal coalgebras on Cartesian closed category are proved to be strongly final,and a category- theoretical definition ofstrong coinductive data types as well as the corresponding corecursion with fixed parameters,which is called pun-fold,is proposed.As a result,the corecursion defined on coinductive data types may include extra parameters asthe input of calculation.Moreover,the comonadic corecursions based on comonads is used to give a unified de-scription for unfold and punfold,and various calculation laws for punfold are further analyzed.Thus,the researchesof Pardo on the recursions with parameters via Comonads are successfully extended to coinductive data types.

Key words: recursive functor, coinductive data type, final coalgebra, corecursion, comonads

中图分类号:

TP301.2

苏锦钿余珊珊. 强共归纳数据类型上的 Comonadic 共递归[J]. 华南理工大学学报（自然科学版）, 2014, 42(1): 128-134.

Su Jin- dian Yu Shan- shan. Comonadic Corecursions on Strong Coinductive Data Types[J]. Journal of South China University of Technology (Natural Science Edition), 2014, 42(1): 128-134.

[1]	苏锦钿余珊珊. 广义共迭代及其计算律[J]. 华南理工大学学报(自然科学版), 2012, 40(9): 62-68.
[2]	苏锦钿余珊珊. 抽象数据类型的双代数结构[J]. 华南理工大学学报（自然科学版）, 2011, 39(12): 44-50.
[3]	苏锦钿余珊珊. 共归纳数据类型上的共递归操作及其计算定律[J]. 华南理工大学学报（自然科学版）, 2011, 39(10): 90-95.

强共归纳数据类型上的 Comonadic 共递归

Comonadic Corecursions on Strong Coinductive Data Types

PDF

可视化

被引次数

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 3

编辑推荐

Metrics

本文评价