Finite Behaviours and Finitary Corecursion

Author Henning Urbat

Thumbnail PDF


  • Filesize: 493 kB
  • 16 pages

Document Identifiers

Author Details

Henning Urbat

Cite AsGet BibTex

Henning Urbat. Finite Behaviours and Finitary Corecursion. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 24:1-24:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


In the coalgebraic approach to state-based systems, semantics is captured up to behavioural equivalence by special coalgebras such as the final coalgebra, the final locally finitely presentable coalgebra (Adámek, Milius, and Velebil), or the final locally finitely generated coalgebra (Milius, Pattinson, and Wißmann). The choice of the proper semantic domain is determined by finiteness restrictions imposed on the systems of interest. We propose a unifying perspective by introducing the concept of a final locally (I,M)-presentable coalgebra, where the two parameters I and M determine what a "finite" system is. Under suitable conditions on the categories and type functors, we show that the final locally (I,M)-presentable coalgebra exists and coincides with the initial (I,M)-iterative algebra, thereby putting a common roof over several results on iterative, fg-iterative and completely iterative algebras that were given a separate treatment before.
  • Iterative algebra
  • completely iterative algebra
  • fg-iterative algebra
  • rational fixpoint
  • terminal coalgebra
  • iterative monad


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Jiří Adámek, Horst Herrlich, and George E. Strecker. Abstract and Concrete Categories: The Joy of Cats. Dover Publications, 2nd edition, 2009. Google Scholar
  2. Jiří Adámek, Stefan Milius, and Jiří Velebil. Iterative algebras at work. Math. Structures Comput. Sci., 16(6):1085-1131, 2006. Google Scholar
  3. Jiří Adámek, Stefan Milius, and Jiří Velebil. Elgot theories: a new perspective on iteration theories. In Proc. Mathematical Foundations of Programming Science (MFPS XXV), volume 249 of Electron. Notes Theor. Comp. Sci., pages 407-427. Elsevier, 2009. Google Scholar
  4. Jiří Adámek, Stefan Milius, and Jiří Velebil. Equational properties of iterative monads. Inform. and Comput., 208:1306-1348, 2010. URL:
  5. Jiří Adámek, Stefan Milius, and Jiří Velebil. On second-order iterative monads. Theoret. Comput. Sci., 412:4969-4988, 2011. URL:
  6. Jiří Adámek and Jiří Rosický. Locally presentable and accessible categories. Cambridge University Press, 1994. Google Scholar
  7. Jiří Adámek, Jiří Rosický, and Enrico Vitale. Algebraic Theories. Cambridge University Press, 2011. Google Scholar
  8. Jiří Adámek and Hans-E. Porst. On tree coalgebras and coalgebra presentations. Theor. Comput. Sci., 311(1-3):257-283, 2004. Google Scholar
  9. Mikołaj Bojańczyk, Bartek Klin, and Sławomir Lasota. Automata theory in nominal sets. Logical Methods in Computer Science, Volume 10, Issue 3, 2014. Google Scholar
  10. Marcello M. Bonsangue, Stefan Milius, and Alexandra Silva. Sound and complete axiomatizations of coalgebraic language equivalence. ACM Trans. Comput. Log., 14(1:7), 2013. Google Scholar
  11. Calvin C. Elgot. Monadic computation and iterative algebraic theories. In H. E. Rose and J. C. Sheperdson, editors, Logic Colloquium '73, volume 80, pages 175-230, Amsterdam, 1975. North-Holland Publishers. Google Scholar
  12. Calvin C. Elgot, Stephen L. Bloom, and Ralph Tindell. On the algebraic structure of rooted trees. J. Comput. System Sci., 16:362-399, 1978. Google Scholar
  13. Susanna Ginali. Regular trees and the free iterative theory. J. Comput. System Sci., 18:228-242, 1979. Google Scholar
  14. Joachim Lambek. A fixpoint theorem for complete categories. Math. Z., 103:151-161, 1968. Google Scholar
  15. Stefan Milius. Completely iterative algebras and completely iterative monads. Inform. and Comput., 196:1-41, 2005. Google Scholar
  16. Stefan Milius. A sound and complete calculus for finite stream circuits. In Proc. 25th Annual Symposium on Logic in Computer Science (LICS'10), pages 449-458. IEEE Computer Society, 2010. Google Scholar
  17. Stefan Milius. Proper functors and their rational fixed point. In Proc. 7th Conference on Algebra and Coalgebra in Computer Science (CALCO'17), Leibniz International Proceedings in Informatics (LIPIcs), 2017. Google Scholar
  18. Stefan Milius and Lawrence S. Moss. The category theoretic solution of recursive program schemes. Theoret. Comput. Sci., 366:3-59, 2006. Fundamental study. Google Scholar
  19. Stefan Milius, Dirk Pattinson, and Thorsten Wißmann. A new foundation for finitary corecursion: The locally finite fixpoint and its properties. In Proc. 19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'16), volume 9634 of Lecture Notes Comput. Sci. (ARCoSS), pages 107-125, 2016. Google Scholar
  20. Evelyn Nelson. Iterative algebras. Theoret. Comput. Sci., 25:67-94, 1983. Google Scholar
  21. Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theoret. Comput. Sci., 249(1):3-80, 2000. Google Scholar
  22. Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Generalizing determinization from automata to coalgebras. Log. Methods Comput. Sci, 9(1:9), 2013. Google Scholar
  23. Jerzy Tiuryn. Unique fixed points vs. least fixed points. Theoret. Comput. Sci., 12:229-254, 1980. Google Scholar