共归纳数据类型上的共递归操作及其计算定律

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

华南理工大学学报（自然科学版） ›› 2011, Vol. 39 ›› Issue (10): 90-95.doi: 10.3969/j.issn.1000-565X.2011.10.016

共归纳数据类型上的共递归操作及其计算定律

苏锦钿¹余珊珊²

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

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

Corecursion Operations and Its Calculation Laws on 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. School of Information Science and Technology,Sun Yet-Sen University,Guangzhou 510275,Guangdong,China

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

摘要/Abstract

摘要： 范畴论框架下的共归纳数据类型可以看成是某个共代数函子下的终结共代数中的载体，针对该特点，结合范畴论给出程序语言中共归纳数据类型的共代数描述，并根据终结共代数的终结性给出相应的共递归操作的定义及其共代数计算定律; 同时，利用双函子及类型函子对参数化共归纳数据类型进行抽象描述，并结合自然转换给出类型函子上的单元和融合等计算定律，证明这些计算定律可用于简化共递归数据类型上的计算，从而提高程序语言对数据类型的动态行为描述能力．

关键词: 范畴论, 共归纳数据类型, 共递归, 终结共代数

Abstract:

As the coinductive data types in the framework of the category theory can be regarded as the carriers of final coalgebras for some coalgebraic functors,this paper presents the coalgebraic descriptions of the coinductive data types in programming languages from the viewpoint of the category theory and proposes the definitions and coalgebraic calculation laws of corecursion operations based on the finality of final coalgebras. Meanwhile,bifunctors and type functors are used to abstractly describe parametric coinductive data types,and such calculation laws on type functors as unit and fusion ones are put forward via natural transformations. It is proved that these laws can be used to simplify the calculations on coinductive data types,thus improving the dynamic behavior description ability of programming languages for various data types.

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

中图分类号:

TP301.2

苏锦钿余珊珊. 共归纳数据类型上的共递归操作及其计算定律[J]. 华南理工大学学报（自然科学版）, 2011, 39(10): 90-95.

Su Jin-dian Yu Shan-shan. Corecursion Operations and Its Calculation Laws on Coinductive Data Types[J]. Journal of South China University of Technology (Natural Science Edition), 2011, 39(10): 90-95.

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

共归纳数据类型上的共递归操作及其计算定律

Corecursion Operations and Its Calculation Laws on Coinductive Data Types

PDF

可视化

被引次数

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 4

编辑推荐

Metrics

本文评价