中文摘要：

针对共归纳数据类型上的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.