Document Open Access Logo

Final Coalgebras from Corecursive Algebras

Author Paul Blain Levy

PDF

File

Thumbnail PDF
PDF
LIPIcs.CALCO.2015.221.pdf
  • Filesize: 486 kB
  • 17 pages

Document Identifiers

Subject Classification

Keywords
  • coalgebra
  • modal logic
  • bisimulation
  • category theory
  • factorization system

Metrics

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

Abstract

We give a technique to construct a final coalgebra in which each element is a set of formulas of modal logic. The technique works for both the finite and the countable powerset functors. Starting with an injectively structured, corecursive algebra, we coinductively obtain a suitable subalgebra called the "co-founded part". We see—first with an example, and then in the general setting of modal logic on a dual adjunction—that modal theories form an injectively structured, corecursive algebra, so that this construction may be applied. We also obtain an initial algebra in a similar way.

We generalize the framework beyond Set to categories equipped with a suitable factorization system, and look at the examples of Poset and Set-op .

Cite As Get BibTex

Paul Blain Levy. Final Coalgebras from Corecursive Algebras. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 221-237, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CALCO.2015.221

Author Details

Paul Blain Levy

References

  1. Samson Abramsky. A cook’s tour of the finitary non-well-founded sets. In Sergei N. Artëmov, Howard Barringer, Artur S. d'Avila Garcez, Luís C. Lamb, and John Woods, editors, We Will Show Them! Essays in Honour of Dov Gabbay, Volume One, pages 1-18. College Publications, 2005. Google Scholar
  2. Jiří Adámek, Mahdieh Haddadi, and Stefan Milius. Corecursive algebras, corecursive monads and bloom monads. Logical Methods in Computer Science, 10(3), 2014. Google Scholar
  3. Jiří Adamek, Horst Herrlich, and George Strecker. Abstract and Concrete Categories - The Joy of Cats. Wiley, 1990. Google Scholar
  4. Jiř\'ıAdámek, Paul B. Levy, Stefan Milius, Lawrence S. Moss, and Lurdes Sousa. On final coalgebras of power-set functors and saturated trees. Applied Categorical Structures, June 2014. Google Scholar
  5. Alexandru Baltag. A logic for coalgebraic simulation. Electronic Nptes in Theoretical Computer Science, 33, 2000. Google Scholar
  6. Nick Bezhanishvili, Clemens Kupke, and Prakash Panangaden. Minimization via duality, volume 7456 LNCS of Lecture notes in computer science / Theoretical Computer Science and General Issues, pages 191-205. Springer, 2012. Google Scholar
  7. Patrick Blackburn, Maarten de Rijke, and Yde Venema. Modal Logic. Cambridge University Press, 2002. Google Scholar
  8. Filippo Bonchi, Marcello M. Bonsangue, Helle H. Hansen, Prakash Panangaden, Jan J. M. M. Rutten, and Alexandra Silva. Algebra-coalgebra duality in Brzozowski’s minimization algorithm. ACM Transactions on Computational Logic, 15(1):3:1-3:29, March 2014. Google Scholar
  9. Marcello Bonsangue and Alexander Kurz. Duality for logics of transition systems. In FOSSACS: International Conference on Foundations of Software Science and Computation Structures. Lecture Notes in Computer Science, 2005. Google Scholar
  10. Venanzio Capretta, Tarmo Uustalu, and Varmo Vene. Recursive coalgebras from comonads. INFCTRL: Information and Computation (formerly Information and Control), 204, 2006. Google Scholar
  11. Venanzio Capretta, Tarmo Uustalu, and Varmo Vene. Corecursive algebras: A study of general structured corecursion. In M. Oliveira and J. Woodcock, editors, Formal Methods: Foundations and Applications, 12th Brazilian Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, Revised Selected Papers, volume 5902 of LNCS, pages 84-100. Springer, 2009. Google Scholar
  12. Liang-Ting Chen and Achim Jung. On a categorical framework for coalgebraic modal logic. Electronic Notes in Theoretical Computer Science, 308:109-128, 2014. Google Scholar
  13. Corina Cîrstea. A modular approach to defining and characterising notions of simulation. Information and Computation, 204(4):469-502, 2006. Google Scholar
  14. Adam Eppendahl. Coalgebra-to-algebra morphisms. Electronic Notes in Theoretical Computer Science, 29:42-49, 1999. Google Scholar
  15. Robert Goldblatt. Final coalgebras and the hennessy-milner property. Annals of Pure and Applied Logic, 138(1-3):77-93, 2006. Google Scholar
  16. Wim H. Hesselink and Albert Thijs. Fixpoint semantics and simulation. Theoretical Computer Science, 238(1-2):275-311, 2000. Google Scholar
  17. Ralf Hinze, Nicolas Wu, and Jeremy Gibbons. Conjugate hylomorphisms - or: The mother of all structured recursion schemes. In Sriram K. Rajamani and David Walker, editors, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 527-538. ACM, 2015. Google Scholar
  18. Jesse Hughes and Bart Jacobs. Simulations in coalgebra. Theoretical Computer Science, 327(1-2):71-108, 2004. Google Scholar
  19. Bart Jacobs and Ana Sokolova. Exemplaric expressivity of modal logics. Journal of Logic and Computation, 20(5):1041-1068, 2010. Google Scholar
  20. Bartek Klin. Coalgebraic modal logic beyond sets. Electronic Notes in Theoretical Computer Science, 173:177-201, 2007. Google Scholar
  21. Bartek Klin and Jurriaan Rot. Coalgebraic trace semantics via forgetful logics. In Andrew M. Pitts, editor, Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, volume 9034 of Lecture Notes in Computer Science, pages 151-166. Springer, 2015. Google Scholar
  22. Clemens Kupke and Raul Andres Leal. Characterising behavioural equivalence: Three sides of one coin. In Alexander Kurz, Marina Lenisa, and Andrzej Tarlecki, editors, Algebra and Coalgebra in Computer Science, Third International Conference, CALCO 2009, Udine, Italy, September 7-10, 2009. Proceedings, volume 5728 of Lecture Notes in Computer Science, pages 97-112. Springer, 2009. Google Scholar
  23. Alexander Kurz and Dirk Pattinson. Coalgebraic modal logic of finite rank. Mathematical Structures in Computer Science, 15(3):453-473, 2005. Google Scholar
  24. Paul B. Levy. Similarity quotients as final coalgebras. In Martin Hofmann, editor, Proceedings, 14th International Conference on Foundations of Software Science and Computational Structures, Saarbrücken, Germany, volume 6604 of Lecture Notes in Computer Science, pages 27-41. Springer, 2011. Google Scholar
  25. Robin Milner. Communication and Concurrency. Prentice-Hall, 1989. Google Scholar
  26. Pierluigi Minari. Infinitary modal logic and generalized Kripke semantics. Annali del Dipartimento di Filosofia, 17(1), 2012. Google Scholar
  27. Dusko Pavlovic, Michael W. Mislove, and James Worrell. Testing semantics: Connecting processes and process logics. In Michael Johnson and Varmo Vene, editors, Algebraic Methodology and Software Technology, 11th International Conference, AMAST 2006, Kuressaare, Estonia, July 5-8, 2006, Proceedings, volume 4019 of Lecture Notes in Computer Science, pages 308-322. Springer, 2006. Google Scholar
  28. Slavian Radev. Infinitary propositional normal modal logic. Studia Logica, 46(4):291-309, 1987. Google Scholar
  29. Jan J. M. M. Rutten. A calculus of transition systems (towards universal coalgebra). In 97, page 25. Centrum voor Wiskunde en Informatica (CWI), ISSN 0169-118X, January 31 1995. CS-R9503. Google Scholar
  30. Lutz Schröder and Dirk Pattinson. Strong completeness of coalgebraic modal logics. In S. Albers and J.-Y. Marion, editors, Proc. STACS 2009, volume 09001 of Dagstuhl Seminar Proceedings, pages 673-684. Schloss Dagstuhl, 2009. Google Scholar
  31. Yoshihito Tanaka and Hiroakira Ono. Rasiowa-Sikorski lemma, Kripke completeness of predicate and infinitary modal logics. In Michael Zakharyaschev, Krister Segerberg, Maarten de Rijke, and Heinrich Wansing, editors, Advances in Modal Logic, pages 401-420. CSLI Publications, 1998. Google Scholar
  32. Paul Taylor. Towards a unified treatment of induction i: the general recursion theorem. preprint, 1996. Google Scholar
  33. Paul Taylor. Practical Foundations of Mathematics. Cambridge Studies in Advanced Mathematics. Cambridge University Press, Cambridge, 1999. Google Scholar
  34. Vera Trnková, Jiří Adámek, Václav Koubek, and Jan Reiterman. Free algebras, input processes and free monads. Commentationes Mathematicae Universitatis Carolinae, 016(2):339-351, 1975. Google Scholar
  35. Toby Wilkinson. A characterisation of expressivity for coalgebraic bisimulation and simulation. Electronic Notes in Theoretical Computer Science, 286:323-336, 2012. Google Scholar
  36. James Worrell. Coinduction for recursive data types: partial orders, metric spaces and ω-categories. Electronic Notes in Theoretical Computer Science, 33, 2000. Google Scholar
  37. James Worrell. On the final sequence of a finitary set functor. Theoretical Computer Science, 338(1-3):184-199, June 2005. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact