广义共迭代及其计算律

华南理工大学学报(自然科学版) ›› 2012, Vol. 40 ›› Issue (9): 62-68.

广义共迭代及其计算律

苏锦钿¹余珊珊²

1．华南理工大学计算机科学与工程学院，广东广州 510006; 2．中山大学信息科学与技术学院，广东广州 510275

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

Generalised Coiteration and Its Calculation Laws

Su Jin-dian¹ Yu Shan-shan²

1. School of Computer Science and Engineering,South China University of Technology,Guangzhou 510006,Guangdong,China; 2. School of Information Science and Technology,Sun Yet-Sen University,Guangzhou 510275,Guangdong,China

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

摘要/Abstract

摘要： 针对函数式编程中的共归纳数据类型上的各种共递归操作缺乏统一描述的问题，利用Monads 及其与共代数函子之间的分配律给出了共归纳数据类型上的一种广义共迭代定义——gunfold，证明了gunfold 可以为共迭代、原始共递归和Course-of-Value 共迭代提供一种统一和抽象的描述．在此基础上进一步从范畴论的角度分析了gunfold 上的各种性质和计算律．

关键词: 函数式编程, 共归纳数据类型, 终结共代数, 共递归, Monads, 范畴论

Abstract:

Due to a lack of general descriptions of various corecursion operations defined on coinductive data types in functional programming,gunfold,a definition of generalised coiteration for coinductive data types,is proposed based on Monads and its distributive laws on coalgebraic functors. It is proved that gunfold can offer a general and abstract description of the coiteration,the primitive corecursion and the course-of-value coiteration. Based on the proof,the properties and the relevant calculation laws for gunfold are analyzed from the viewpoint of the category theory.

Key words: functional programming, coinductive data type, final coalgebra, corecursion, Monads, category theory

中图分类号:

TP301.2

苏锦钿余珊珊. 广义共迭代及其计算律[J]. 华南理工大学学报(自然科学版), 2012, 40(9): 62-68.

Su Jin-dian Yu Shan-shan. Generalised Coiteration and Its Calculation Laws[J]. Journal of South China University of Technology(Natural Science Edition), 2012, 40(9): 62-68.

[1]	苏锦钿余珊珊. 带固定参数的 Monadic 递归[J]. 华南理工大学学报（自然科学版）, 2014, 42(7): 33-39,73.
[2]	苏锦钿余珊珊. 强共归纳数据类型上的 Comonadic 共递归[J]. 华南理工大学学报（自然科学版）, 2014, 42(1): 128-134.
[3]	苏锦钿余珊珊. 抽象数据类型的双代数结构[J]. 华南理工大学学报（自然科学版）, 2011, 39(12): 44-50.
[4]	苏锦钿余珊珊. 共归纳数据类型上的共递归操作及其计算定律[J]. 华南理工大学学报（自然科学版）, 2011, 39(10): 90-95.