Abstract:
Dualizing the work of Osius, Taylor,
and others on general structured recursion and induction in terms of
recursive and wellfounded coalgebras, we study general structured
corecursion and coinduction. We call an algebra of a functor
corecursive, if from any coalgebra of the same functor there is a unique
map to this algebra, and antifounded, if it admits a certain
bisimulation principle. We show that both of these concepts are
perfectly meaningful and relevant for programming and verification.
However, differently from recursiveness and wellfoundedness, which are
equivalent concepts under mild conditions, they are generally
inequivalent. (Joint work with Venanzio Capretta and Varmo Vene.) |