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

Corecursion Operations and Its Calculation Laws on Coinductive Data Types

作　　者：苏锦钿[1] 余珊珊[2] 

机构地区：[1]华南理工大学计算机科学与工程学院,广东广州510006 [2]中山大学信息科学与技术学院,广东广州510275

出　　处：《华南理工大学学报（自然科学版）》2011年第10期90-95,共6页Journal of South China University of Technology(Natural Science Edition)

基　　金：2010年高等学校博士点学科专项科研基金资助项目(20100172120043);华南理工大学中央高校基本科研业务费专项资金资助项目(2009ZM0158)

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

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

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]