作　　者： ; ;

机构地区： 华南理工大学计算机科学与工程学院

出　　处： 《华南理工大学学报（自然科学版）》 2014年第1期128-134,共7页

摘　　要： 针对共归纳数据类型上的unfold无法描述带参数的共递归计算的问题,首先证明了笛卡尔封闭范畴上的终结共代数是强终结的,并给出强共归纳数据类型的范畴论定义及其上一种带固定参数的共递归——punfold,使得共归纳数据类型上的共递归计算可以包含额外的参数作为计算的输入;然后利用基于Comonads的Comonadic共递归给出了unfold和punfold的一种统一的描述,并进一步分析了punfold上的各种计算律,从而将Pardo对基于Comonads的带参数的递归计算研究扩展到共归纳数据类型. As the unfold on coinductive data types can not describe the corecursive functions with parameters,the final coalgebras on Cartesian closed category are proved to be strongly final,and a category-theoretical definition of strong 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 as the 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 researches of Pardo on the recursions with parameters via Comonads are successfully extended to coinductive data types.

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

领　　域： [自动化与计算机技术] [自动化与计算机技术]