Abstract
Motivated by issues in designing practical total functional programming languages, we are interested in structured recursive equations that uniquely describe a function not because of the properties of the coalgebra marshalling the recursive call arguments but thanks to the algebra assembling their results. Dualizing the known notions of recursive and wellfounded coalgebras, 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 bisimilarity principle. Differently from recursiveness and wellfoundedness, which are equivalent conditions under mild assumptions, corecursiveness and antifoundedness turn out to be generally inequivalent.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Adámek, J., Lücke, D., Milius, S.: Recursive coalgebras for finitary functors. Theor. Inform. and Appl. 41(4), 447–462 (2007)
Bove, A., Capretta, V.: Modelling general recursion in type theory. Math. Struct. in Comput. Sci. 14(4), 671–708 (2005)
Buchholz, W.: A term calculus for (co-)recursive definitions on streamlike data structures. Ann. of Pure and Appl. Logic 136(1–2), 75–90 (2005)
Capretta, V., Uustalu, T., Vene, V.: Recursive coalgebras from comonads. Inform. and Comput. 204(4), 437–468 (2006)
Cockett, R., Fukushima, T.: About Charity. Yellow series report 92/480/18, Dept. of Comput. Sci., Univ. of Calgary (1992)
Coquand, T.: Infinite objects in type theory. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 62–78. Springer, Heidelberg (1994)
Di Gianantonio, P., Miculan, M.: A unifying approach to recursive and co-recursive definitions. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 148–161. Springer, Heidelberg (2003)
Doornbos, H., Backhouse, R.: Reductivity. Sci. of Comput. Program 26(1-3), 217–236 (1996)
Eppendahl, A.: Coalgebra-to-algebra morphisms. Electron. Notes in Theor. Comput. Sci. 29, 8 (1999)
Giménez, E.: Codifying guarded definitions with recursion schemes. In: Smith, J., Dybjer, P., Nordström, B. (eds.) TYPES 1994. LNCS, vol. 996, pp. 39–59. Springer, Heidelberg (1995)
Jacobs, B.: The temporal logic of coalgebras via Galois algebras. Math. Struct. in Comput. Sci. 12(6), 875–903 (2002)
Milius, S.: Completely iterative algebras and completely iterative monads. Inform. and Comput. 196(1), 1–41 (2005)
Osius, G.: Categorical set theory: a characterization of the category of sets. J. of Pure and Appl. Algebra 4, 79–119 (1974)
Taylor, P.: Intuitionistic sets and ordinals. J. of Symb. Logic 61(3), 705–744 (1996)
Taylor, P.: Towards a unified treatment of induction, I: The general recursion theorem. Unpublished draft 35 pp (1996); // A short version (1996) of 5 pp was distributed at Gödel 1996 Brno (August 1996), http://www.monad.me.uk/ordinals/
Taylor, P.: Practical foundations of mathematics. Cambridge Studies in Advanced Mathematics, vol. 59, xi+572. Cambridge Univ. Press, Cambridge (1999)
Turner, D.A.: Total functional programming. J. of Univ. Comput. Sci. 10(7), 751–768 (2004)
Uustalu, T., Vene, V.: Primitive (co)recursion and course-of-value (co)iteration, categorically. Informatica 10(1), 5–26 (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Capretta, V., Uustalu, T., Vene, V. (2009). Corecursive Algebras: A Study of General Structured Corecursion. In: Oliveira, M.V.M., Woodcock, J. (eds) Formal Methods: Foundations and Applications. SBMF 2009. Lecture Notes in Computer Science, vol 5902. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-10452-7_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-10452-7_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-10451-0
Online ISBN: 978-3-642-10452-7
eBook Packages: Computer ScienceComputer Science (R0)