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.) |