Corecursive Operations with Parameters and the Associated Calculational Laws

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 abstract sense, and present their implementations by the functional programming language Haskell. We also point out their applications in the fields of reasoning, transformations and optimizations of programs.