作　　者： ; ;

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

出　　处： 《计算机研究与发展》 2013年第12期2676-2690,共15页

摘　　要： 针对共归纳数据类型上的unfold无法描述带参数的共递归操作的问题,证明了笛卡儿封闭范畴上的有限扩展多项式函子的终结共代数在固定参数和累积参数下都是强终结的,并利用该强终结性给出强共归纳数据类型的定义以及带固定参数和累积参数的共递归操作——punfold和aunfold,从而将Pardo对强归纳数据类型及带参数的递归计算pfold和afold的研究扩展到共归纳数据类型上,使得unfold可直接包含额外的参数用于作为计算的输入或者保存临时的计算结果,避免采用高阶函数的方式.从范畴论的角度给出punfold和aunfold的各种性质、计算律及在函数式程序语言Haskell中的实现,并指出它们在程序推导、转换和优化中的应用. The unfold defined on coinductive datatypes is not able to describe those coinductive operations with parameters. To solve the problem, we prove that the final coalgebras for finitely extended polymonial functors on cartesian closed category are strongly final under the conditions of fixed or accumulating parameters, which yields the definitions of strong coinductive datatypes and coinductive operations with fixed or accumulating parameters-named punfold and aunfold respectively. We extend the researches of Pardo on strong inductive datatypes and recursions with parameters, named pfold and afold, to coinductive datatypes. This unfold can directly carry extra parameters as the inputs of calculations or store temporal values produced by programs, which as a result avoids using higher-order functions. We discuss the properties and the associated calculational laws for punfold and aunfold in a categorical and sense, and present their implementations by the functional programming language Haskell. reasoning, transformations and optimizations We also point out their applications in the fields of of programs.

关 键 词： 共归纳数据类型 终结共代数 共递归 累积计算 范畴论

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