Recursive coalgebras from comonads

The concept of recursive coalgebra of a functor was introduced in the 1970s by Osius in his work on categorical set theory to discuss the relationship between wellfounded induction and recursively specified functions. In this paper, we motivate the use of recursive coalgebras as a paradigm of structured recursion in programming semantics, list some basic facts about recursive coalgebras and, centrally, give new conditions for the recursiveness of a coalgebra based on comonads, comonad-coalgebras and distributive laws of functors over comonads. We also present an alternative construction using countable products instead of cofree comonads.

Authors

• Venanzio Capretta
• Tarmo Uustalu
• Varmo Vene

Keywords

• Structured recursion
• Recursive coalgebras
• Wellfounded coalgebras
• Comonads
• Distributive laws