We instantiate the general comonad-based construction of recursion schemes for the initial algebra of a functor F to the cofree recursive comonad on F. Differently from the scheme based on the cofree comonad on F in a similar fashion, this scheme allows not only recursive calls on elements structurally smaller than the given argument, but also subsidiary recursions. We develop a Mendler formulation of the scheme via a generalized Yoneda lemma for initial algebras involving strong dinaturality and hint a relation to circular proofs à la Cockett, Santocanale. © 2011 Elsevier B.V. All rights reserved.
Uustalu, T., & Vene, V. (2011). The recursion scheme from the cofree recursive comonad. Electronic Notes in Theoretical Computer Science, 229(5), 135–157. https://doi.org/10.1016/j.entcs.2011.02.020