Document Open Access Logo

Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor

Author Niccolò Veltri

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2021.22.pdf
  • Filesize: 0.82 MB
  • 18 pages

Document Identifiers

Author Details

Niccolò Veltri
  • Department of Software Science, Tallinn University of Technology, Estonia

Funding

This work was supported by the Estonian Research Council grant PSG659 and by the ESF funded Estonian IT Academy research measure (project 2014-2020.4.05.19-0001).

Acknowledgements

We thank Henning Basold, Tarmo Uustalu, Andrea Vezzosi and Niels van der Weide for valuable discussions.

Cite AsGet BibTex

Niccolò Veltri. Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.FSCD.2021.22

Abstract

The finite powerset functor is a construct frequently employed for the specification of nondeterministic transition systems as coalgebras. The final coalgebra of the finite powerset functor, whose elements characterize the dynamical behavior of transition systems, is a well-understood object which enjoys many equivalent presentations in set-theoretic foundations based on classical logic. In this paper, we discuss various constructions of the final coalgebra of the finite powerset functor in constructive type theory, and we formalize our results in the Cubical Agda proof assistant. Using setoids, the final coalgebra of the finite powerset functor can be defined from the final coalgebra of the list functor. Using types instead of setoids, as it is common in homotopy type theory, one can specify the finite powerset datatype as a higher inductive type and define its final coalgebra as a coinductive type. Another construction is obtained by quotienting the final coalgebra of the list functor, but the proof of finality requires the assumption of the axiom of choice. We conclude the paper with an analysis of a classical construction by James Worrell, and show that its adaptation to our constructive setting requires the presence of classical axioms such as countable choice and the lesser limited principle of omniscience.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Constructive mathematics
Keywords
  • type theory
  • finite powerset
  • final coalgebra
  • Cubical Agda

Metrics

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

Supplementary Materials

References

  1. Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. Copatterns: programming infinite structures by observations. In Roberto Giacobazzi and Radhia Cousot, editors, Proc. of 40th Ann. ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL'13, pages 27-38. ACM, 2013. URL: https://doi.org/10.1145/2429069.2429075.
  2. Jirí Adámek and Václav Koubek. On the greatest fixed point of a set functor. Theoretical Computer Science, 150(1):57-75, 1995. URL: https://doi.org/10.1016/0304-3975(95)00011-K.
  3. Jirí Adámek, Paul Blain Levy, Stefan Milius, Lawrence S. Moss, and Lurdes Sousa. On final coalgebras of power-set functors and saturated trees. Applied Categorical Structures, 23(4):609-641, 2015. URL: https://doi.org/10.1007/s10485-014-9372-9.
  4. Jiří Adámek, Stefan Milius, and Lawrence S. Moss. Initial algebras, terminal coalgebras, and the theory of fixed points of functors. Draft book, available from http://www.stefan-milius.eu, 2021.
  5. Benedikt Ahrens, Paolo Capriotti, and Régis Spadotti. Non-wellfounded trees in homotopy type theory. In Thorsten Altenkirch, editor, Proc. of 13th Int. Conf. on Typed Lambda Calculi and Applications, TLCA'15, volume 38 of Leibniz International Proceedings in Informatics, pages 17-30. Schloss Dagstuhl, 2015. URL: https://doi.org/10.4230/LIPIcs.TLCA.2015.17.
  6. Michael Barr. Terminal coalgebras in well-founded set theory. Theoretical Computer Science, 114(2):299-315, 1993. URL: https://doi.org/10.1016/0304-3975(93)90076-6.
  7. Gilles Barthe, Venanzio Capretta, and Olivier Pons. Setoids in type theory. Journal of Functional Programming, 13(2):261-293, 2003. URL: https://doi.org/10.1017/S0956796802004501.
  8. Henning Basold, Herman Geuvers, and Niels van der Weide. Higher inductive types in programming. Journal of Universal Computer Science, 23(1):63-88, 2017. URL: https://doi.org/10.3217/jucs-023-01-0063.
  9. Evan Cavallo and Robert Harper. Higher inductive types in cubical computational type theory. PACMPL, 3(POPL):1:1-1:27, 2019. URL: https://doi.org/10.1145/3290314.
  10. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical type theory: A constructive interpretation of the univalence axiom. In Tarmo Uustalu, editor, Proc. of 21st Int. Conf. on Types for Proofs and Programs, TYPES'15, volume 69 of Leibniz International Proceedings in Informatics, pages 5:1-5:34. Schloss Dagstuhl, 2015. URL: https://doi.org/10.4230/LIPIcs.TYPES.2015.5.
  11. Thierry Coquand, Simon Huber, and Anders Mörtberg. On higher inductive types in cubical type theory. In Anuj Dawar and Erich Grädel, editors, Proc. of the 33rd Ann. ACM/IEEE Symp. on Logic in Computer Science, LICS'18, pages 255-264. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209197.
  12. Thierry Coquand and Arnaud Spiwack. Constructively finite? In Laureano Lambàn, Ana Romero, and Julio Rubio, editors, Scientific Contributions in Honor of Mirian Andrés Gómez, pages 217-230. Universidad de La Rioja, 2010. Google Scholar
  13. Nils Anders Danielsson. Bag equivalence via a proof-relevant membership relation. In Lennart Beringer and Amy P. Felty, editors, Proc. of 3rd Int. Conf. on Interactive Theorem Proving, ITP'12, volume 7406 of Lecture Notes in Computer Science, pages 149-165. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-32347-8_11.
  14. Nils Anders Danielsson. Up-to techniques using sized types. PACMPL, 2(POPL):43:1-43:28, 2018. URL: https://doi.org/10.1145/3158131.
  15. Denis Firsov and Tarmo Uustalu. Dependently typed programming with finite sets. In Patrick Bahr and Sebastian Erdweg, editors, Proc. of 11th ACM SIGPLAN Workshop on Generic Programming, WGP'15, pages 33-44. ACM, 2015. URL: https://doi.org/10.1145/2808098.2808102.
  16. Denis Firsov, Tarmo Uustalu, and Niccolò Veltri. Variations on Noetherianness. In Robert Atkey and Neelakantan R. Krishnaswami, editors, Proc. of 6th Wksh. on Mathematically Structured Functional Programming, MSFP'16, volume 207 of Electronic Proceedings in Theoretical Computer Science, pages 76-88, 2016. URL: https://doi.org/10.4204/EPTCS.207.4.
  17. Dan Frumin, Herman Geuvers, Léon Gondelman, and Niels van der Weide. Finite sets in homotopy type theory. In Proc. of 7th ACM SIGPLAN Int. Conf. on Certified Programs and Proofs, CPP'18, pages 201-214. ACM, 2018. URL: https://doi.org/10.1145/3167085.
  18. John Hughes, Lars Pareto, and Amr Sabry. Proving the correctness of reactive systems using sized types. In Proc. of 23rd ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL'96, pages 410-423, 1996. URL: https://doi.org/10.1145/237721.240882.
  19. Yoshiki Kinoshita and John Power. Category theoretic structure of setoids. Theoretical Computer Science, 546:145-163, 2014. URL: https://doi.org/10.1016/j.tcs.2014.03.006.
  20. Magnus Baunsgaard Kristensen, Rasmus Ejlers Møgelberg, and Andrea Vezzosi. A model of clocked cubical type theory, 2021. URL: http://arxiv.org/abs/2102.01969.
  21. Paul Blain Levy. Similarity quotients as final coalgebras. In Martin Hofmann, editor, Proc. of 14th Int. Conf on Foundations of Software Science and Computational Structures, FoSSaCS'11, volume 6604 of Lecture Notes in Computer Science, pages 27-41. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-19805-2_3.
  22. Mark Mandelkern. Constructively complete finite sets. Mathematical Logic Quarterly, 34(2):97-103, 1988. URL: https://doi.org/10.1002/malq.19880340202.
  23. Robin Milner. A calculus of communicating systems, volume 92 of Lecture Notes in Computer Science. Springer, 1980. URL: https://doi.org/10.1007/3-540-10235-3.
  24. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, I. Information and Computation, 100(1):1-40, 1992. URL: https://doi.org/10.1016/0890-5401(92)90008-4.
  25. Erik Parmann. Investigating streamless sets. In Hugo Herbelin, Pierre Letouzey, and Matthieu Sozeau, editors, Proc. of 20th Int. Conf. on Types for Proofs and Programs, TYPES'14, volume 39 of Leibniz International Proceedings in Informatics, pages 187-201. Schloss Dagstuhl, 2014. URL: https://doi.org/10.4230/LIPIcs.TYPES.2014.187.
  26. Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theoretical Computer Science, 249(1):3-80, 2000. URL: https://doi.org/10.1016/S0304-3975(00)00056-6.
  27. The Univalent Foundations Program. Homotopy type theory: Univalent foundations of mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  28. Niccolò Veltri. A type-theoretical study of nontermination. PhD thesis, Tallinn University of Technology, 2017. URL: https://digi.lib.ttu.ee/i/?7631.
  29. Niccolò Veltri and Andrea Vezzosi. Formalizing π-calculus in Guarded Cubical Agda. In Jasmin Blanchette and Catalin Hritcu, editors, Proc. of 9th ACM SIGPLAN Int. Conf. on Certified Programs and Proofs, CPP'20, pages 270-283. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373814.
  30. Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. Cubical Agda: A dependently typed programming language with univalence and higher inductive types. PACMPL, 3(ICFP):87:1-87:29, 2019. URL: https://doi.org/10.1145/3341691.
  31. Niels van der Weide and Herman Geuvers. The construction of set-truncated higher inductive types. In Barbara König, editor, Proc. of 35th Int. Conf. on Mathematical Foundations of Programming Semantics, MFPS'19, volume 347 of Electronic Notes in Theoretical Computer Science, pages 261-280. Elsevier, 2019. URL: https://doi.org/10.1016/j.entcs.2019.09.014.
  32. James Worrell. Terminal sequences for accessible endofunctors. In Bart Jacobs and Jan J. M. M. Rutten, editors, Proc. of 2nd Int. Wksh. on Coalgebraic Methods in Computer Science, CMCS'99, volume 19 of Electronic Notes in Theoretical Computer Science, pages 24-38. Elsevier, 1999. URL: https://doi.org/10.1016/S1571-0661(05)80267-1.
  33. James Worrell. On the final sequence of a finitary set functor. Theoretical Computer Science, 338(1-3):184-199, 2005. URL: https://doi.org/10.1016/j.tcs.2004.12.009.
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 Imprint Privacy Contact