针对共归纳数据类型上的 unfold 无法描述带参数的共递归计算的问题，首先证明了笛卡尔封闭范畴上的终结共代数是强终结的，并给出强共归纳数据类型的范畴论定义及其上一种带固定参数的共递归——punfold，使得共归纳数据类型上的共递归计算可以包含额外的参数作为计算的输入; 然后利用基于 Comonads 的 Comonadic 共递归给出了unfold 和 punfold 的一种统一的描述，并进一步分析了 punfold 上的各种计算律，从而将Pardo 对基于 Comonads 的带参数的递归计算研究扩展到共归纳数据类型．

As the unfold on coinductive data types can not describe the corecursive functions with parameters,thefinal coalgebras on Cartesian closed category are proved to be strongly final,and a category- theoretical definition ofstrong 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 asthe 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 researchesof Pardo on the recursions with parameters via Comonads are successfully extended to coinductive data types.