论文部分内容阅读
针对共归纳数据类型上的unfold无法描述带参数的共递归操作的问题,证明了笛卡儿封闭范畴上的有限扩展多项式函子的终结共代数在固定参数和累积参数下都是强终结的,并利用该强终结性给出强共归纳数据类型的定义以及带固定参数和累积参数的共递归操作——punfold和aunfold,从而将Pardo对强归纳数据类型及带参数的递归计算pfold和afold的研究扩展到共归纳数据类型上,使得unfold可直接包含额外的参数用于作为计算的输入或者保存临时的计算结果,避免采用高阶函数的方式.从范畴论的角度给出punfold和