Document Open Access Logo

Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down

Authors Mayuko Kori , Ichiro Hasuo , Shin-ya Katsumata

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2021.21.pdf
  • Filesize: 0.88 MB
  • 22 pages

Document Identifiers

Author Details

Mayuko Kori
  • The Graduate University for Advanced Studies (SOKENDAI), Hayama, Japan
  • National Institute of Informatics, Tokyo, Japan
Ichiro Hasuo
  • The Graduate University for Advanced Studies (SOKENDAI), Hayama, Japan
  • National Institute of Informatics, Tokyo, Japan
Shin-ya Katsumata
  • National Institute of Informatics, Tokyo, Japan

Funding

  • Hasuo, Ichiro: ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST
  • Katsumata, Shin-ya: ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST

Cite As Get BibTex

Mayuko Kori, Ichiro Hasuo, and Shin-ya Katsumata. Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 21:1-21:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.CONCUR.2021.21

Abstract

The coincidence between initial algebras (IAs) and final coalgebras (FCs) is a phenomenon that underpins various important results in theoretical computer science. In this paper, we identify a general fibrational condition for the IA-FC coincidence, namely in the fiber over an initial algebra in the base category. Identifying (co)algebras in a fiber as (co)inductive predicates, our fibrational IA-FC coincidence allows one to use coinductive witnesses (such as invariants) for verifying inductive properties (such as liveness). Our general fibrational theory features the technical condition of stability of chain colimits; we extend the framework to the presence of a monadic effect, too, restricting to fibrations of complete lattice-valued predicates. Practical benefits of our categorical theory are exemplified by new "upside-down" witness notions for three verification problems: probabilistic liveness, and acceptance and model-checking with respect to bottom-up tree automata.

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
Keywords
  • initial algebra
  • final coalgebra
  • fibration
  • category theory

Metrics

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

Related Versions

References

  1. Jiří Adámek. Free algebras and automata realizations in the language of categories. Commentationes Mathematicae Universitatis Carolinae, 15(4):589-602, 1974. Google Scholar
  2. Jiří Adámek, J Adamek, J Rosicky, et al. Locally presentable and accessible categories, volume 189. Cambridge University Press, 1994. Google Scholar
  3. Jirí Adámek, Stefan Milius, and Lawrence S. Moss. Fixed points of functors. J. Log. Algebraic Methods Program., 95:41-81, 2018. URL: https://doi.org/10.1016/j.jlamp.2017.11.003.
  4. Alejandro Aguirre and Shin-ya Katsumata. Weakest preconditions in fibrations. Electronic Notes in Theoretical Computer Science, 352:5-27, 2020. The 36th Mathematical Foundations of Programming Semantics Conference, 2020. URL: https://doi.org/10.1016/j.entcs.2020.09.002.
  5. Michael Barr. Algebraically compact functors. Journal of Pure and Applied Algebra, 82(3):211-231, 1992. Google Scholar
  6. Richard S. Bird and Oege de Moor. Algebra of programming. Prentice Hall International series in computer science. Prentice Hall, 1997. Google Scholar
  7. Filippo Bonchi, Barbara König, and Daniela Petrisan. Up-to techniques for behavioural metrics via fibrations. CoRR, abs/1806.11064, 2018. URL: http://arxiv.org/abs/1806.11064.
  8. Venanzio Capretta, Tarmo Uustalu, and Varmo Vene. Corecursive algebras: A study of general structured corecursion. In Marcel Vinícius Medeiros Oliveira and Jim Woodcock, editors, Formal Methods: Foundations and Applications, 12th Brazilian Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, August 19-21, 2009, Revised Selected Papers, volume 5902 of Lecture Notes in Computer Science, pages 84-100. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-10452-7_7.
  9. Aurelio Carboni, Stephen Lack, and R.F.C. Walters. Introduction to extensive and distributive categories. Journal of Pure and Applied Algebra, 84(2):145-158, 1993. URL: https://doi.org/10.1016/0022-4049(93)90035-R.
  10. Aleksandar Chakarov and Sriram Sankaranarayanan. Probabilistic program analysis with martingales. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science, pages 511-526. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39799-8_34.
  11. Marcelo P. Fiore. Axiomatic Domain Theory in Categories of Partial Maps. Distinguished Dissertations in Computer Science. Cambridge University Press, 1996. URL: https://doi.org/10.1017/CBO9780511526565.
  12. Peter Freyd. Algebraically complete categories. In Aurelio Carboni, Maria Cristina Pedicchio, and Guiseppe Rosolini, editors, Category Theory, pages 95-104, Berlin, Heidelberg, 1991. Springer Berlin Heidelberg. Google Scholar
  13. Peter J. Freyd. Recursive types reduced to inductive types. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), Philadelphia, Pennsylvania, USA, June 4-7, 1990, pages 498-507. IEEE Computer Society, 1990. URL: https://doi.org/10.1109/LICS.1990.113772.
  14. Ichiro Hasuo, Kenta Cho, Toshiki Kataoka, and Bart Jacobs. Coinductive predicates and final sequences in a fibration. In Dexter Kozen and Michael W. Mislove, editors, Proceedings of the Twenty-ninth Conference on the Mathematical Foundations of Programming Semantics, MFPS 2013, New Orleans, LA, USA, June 23-25, 2013, volume 298 of Electronic Notes in Theoretical Computer Science, pages 197-214. Elsevier, 2013. URL: https://doi.org/10.1016/j.entcs.2013.09.014.
  15. Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic trace semantics via coinduction. Log. Methods Comput. Sci., 3(4), 2007. URL: https://doi.org/10.2168/LMCS-3(4:11)2007.
  16. Tobias Heindel and Pawel Sobocinski. Van kampen colimits as bicolimits in span. 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 335-349. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03741-2_23.
  17. Horst Herrlich. Topological functors. General Topology and its Applications, 4(2):125-142, 1974. Google Scholar
  18. Bart Jacobs. Introduction to Coalgebra: Towards Mathematics of States and Observation, volume 59 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. URL: https://doi.org/10.1017/CBO9781316823187.
  19. Bart P. Jacobs. Categorical Logic and Type Theory, volume 141 of Studies in logic and the foundations of mathematics. North-Holland, 2001. URL: http://www.elsevierdirect.com/product.jsp?isbn=9780444508539.
  20. Yuichi Komorida, Shin-ya Katsumata, Nick Hu, Bartek Klin, and Ichiro Hasuo. Codensity games for bisimilarity. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785691.
  21. Mayuko Kori, Ichiro Hasuo, and Shin ya Katsumata. Fibrational initial algebra-final coalgebra coincidence over initial algebras: Turning verification witnesses upside down, 2021. An extended version with appendices. URL: http://arxiv.org/abs/2105.04817.
  22. Jacob Lurie. Higher Topos Theory (AM-170). Princeton University Press, 2009. URL: http://www.jstor.org/stable/j.ctt7s47v.
  23. E. Moggi. Notions of computation and monads. Inf. & Comp., 93(1):55-92, 1991. Google Scholar
  24. Philip S. Mulry. Lifting theorems for kleisli categories. In Stephen D. Brookes, Michael G. Main, Austin Melton, Michael W. Mislove, and David A. Schmidt, editors, Mathematical Foundations of Programming Semantics, 9th International Conference, New Orleans, LA, USA, April 7-10, 1993, Proceedings, volume 802 of Lecture Notes in Computer Science, pages 304-319. Springer, 1993. URL: https://doi.org/10.1007/3-540-58027-1_15.
  25. Andrew M. Pitts. Relational properties of domains. Inf. Comput., 127(2):66-90, 1996. URL: https://doi.org/10.1006/inco.1996.0052.
  26. J. J. M. M. Rutten. Universal coalgebra: a theory of systems. Theoretical Computer Science, 249:3-80, 2000. Google Scholar
  27. Michael B. Smyth and Gordon D. Plotkin. The category-theoretic solution of recursive domain equations. SIAM J. Comput., 11(4):761-783, 1982. URL: https://doi.org/10.1137/0211062.
  28. David Sprunger, Shin-ya Katsumata, Jérémy Dubut, and Ichiro Hasuo. Fibrational bisimulations and quantitative reasoning. In Corina Cîrstea, editor, Coalgebraic Methods in Computer Science - 14th IFIP WG 1.3 International Workshop, CMCS 2018, Colocated with ETAPS 2018, Thessaloniki, Greece, April 14-15, 2018, Revised Selected Papers, volume 11202 of Lecture Notes in Computer Science, pages 190-213. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-00389-0_11.
  29. Toru Takisaka, Yuichiro Oyabu, Natsuki Urabe, and Ichiro Hasuo. Ranking and repulsing supermartingales for reachability in probabilistic programs. In Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings, pages 476-493, 2018. URL: https://doi.org/10.1007/978-3-030-01090-4_28.
  30. Věra Trnková, Jiří Adámek, Václav Koubek, and Jan Reiterman. Free algebras, input processes and free monads. Commentationes Mathematicae Universitatis Carolinae, 16(2):339-351, 1975. Google Scholar
  31. Natsuki Urabe, Masaki Hara, and Ichiro Hasuo. Categorical liveness checking by corecursive algebras. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005151.
  32. Vladimir Zamdzhiev. Reflecting algebraically compact functors. In John Baez and Bob Coecke, editors, Proceedings Applied Category Theory 2019, ACT 2019, University of Oxford, UK, 15-19 July 2019, volume 323 of EPTCS, pages 15-23, 2019. URL: https://doi.org/10.4204/EPTCS.323.2.
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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact