华南理工大学学报（自然科学版）
華南理工大學學報（自然科學版）
화남리공대학학보（자연과학판）
JOURNAL OF SOUTH CHINA UNIVERSITY OF TECHNOLOGY(NATURAL SCIENCE EDITION)
2014年
1期
128-134
,共7页
递归函子%共归纳数据类型%终结共代数%共递归%Comonads
遞歸函子%共歸納數據類型%終結共代數%共遞歸%Comonads
체귀함자%공귀납수거류형%종결공대수%공체귀%Comonads
recursive functor%coinductive data type%final coalgebra%corecursion%comonads
针对共归纳数据类型上的unfold无法描述带参数的共递归计算的问题，首先证明了笛卡尔封闭范畴上的终结共代数是强终结的，并给出强共归纳数据类型的范畴论定义及其上一种带固定参数的共递归---punfold，使得共归纳数据类型上的共递归计算可以包含额外的参数作为计算的输入；然后利用基于Comonads的Comonadic共递归给出了unfold和punfold 的一种统一的描述，并进一步分析了punfold 上的各种计算律，从而将Pardo对基于Comonads的带参数的递归计算研究扩展到共归纳数据类型。
針對共歸納數據類型上的unfold無法描述帶參數的共遞歸計算的問題，首先證明瞭笛卡爾封閉範疇上的終結共代數是彊終結的，併給齣彊共歸納數據類型的範疇論定義及其上一種帶固定參數的共遞歸---punfold，使得共歸納數據類型上的共遞歸計算可以包含額外的參數作為計算的輸入；然後利用基于Comonads的Comonadic共遞歸給齣瞭unfold和punfold 的一種統一的描述，併進一步分析瞭punfold 上的各種計算律，從而將Pardo對基于Comonads的帶參數的遞歸計算研究擴展到共歸納數據類型。
침대공귀납수거류형상적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.
