LIPIcs.CALCO.2023.15.pdf
- Filesize: 0.68 MB
- 17 pages
Document
Coinductive Control of Inductive Data Types
Authors
-
Part of:
Volume:
10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Conference on Algebra and Coalgebra in Computer Science (CALCO) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-09-02
Cite AsGet BibTex
Paige Randall North and Maximilien Péroux. Coinductive Control of Inductive Data Types. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CALCO.2023.15
https://doi.org/10.4230/LIPIcs.CALCO.2023.15
Abstract
We combine the theory of inductive data types with the theory of universal measurings. By doing so, we find that many categories of algebras of endofunctors are actually enriched in the corresponding category of coalgebras of the same endofunctor. The enrichment captures all possible partial algebra homomorphisms, defined by measuring coalgebras. Thus this enriched category carries more information than the usual category of algebras which captures only total algebra homomorphisms. We specify new algebras besides the initial one using a generalization of the notion of initial algebra.
Subject Classification
ACM Subject Classification
- Theory of computation → Categorical semantics
- Theory of computation → Algebraic semantics
- Theory of computation → Type structures
Keywords
- Inductive types
- enriched category theory
- algebraic data types
- algebra
- coalgebra
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Jiří Adámek and Hans-E. Porst. On varieties and covarieties in a category. Mathematical Structures in Computer Science, 13(2):201-232, 2003. URL: https://doi.org/10.1017/S0960129502003882.
- Jiří Adámek and Jiří Rosický. Locally presentable and accessible categories, volume 189 of London Mathematical Society Lecture Note Series. Cambridge University Press, Cambridge, 1994. URL: https://doi.org/10.1017/CBO9780511600579.
- Martin Hyland, Ignacio López Franco, and Christina Vasilakopoulou. Hopf measuring comonoids and enrichment. Proc. Lond. Math. Soc. (3), 115(5):1118-1148, 2017. URL: https://doi.org/10.1112/plms.12064.
- Jacob Lurie. Higher topos theory, volume 170 of Annals of Mathematics Studies. Princeton University Press, Princeton, NJ, 2009. URL: https://doi.org/10.1515/9781400830558.
-
Per Martin-Löf. Intuitionistic type theory. Naples: Bibliopolis, 1984.
- Dylan McDermott, Exequiel Rivas, and Tarmo Uustalu. Sweedler theory of monads. In Patricia Bouyer and Lutz Schröder, editors, Foundations of Software Science and Computation Structures, pages 428-448, Cham, 2022. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-99253-8_22.
- Paige Randall North and Maximilien Péroux. Coinductive control of inductive data types, 2023. URL: https://arxiv.org/abs/2303.16793.
- Maximilien Péroux. The coalgebraic enrichment of algebras in higher categories. Journal of Pure and Applied Algebra, 226(3):106849, 2022. URL: https://doi.org/10.1016/j.jpaa.2021.106849.
- Jan Rutten. The Method of Coalgebra: exercises in coinduction. C, 2019. URL: https://ir.cwi.nl/pub/28550/.
-
Moss E. Sweedler. Hopf algebras. Mathematics Lecture Note Series. W. A. Benjamin, Inc., New York, 1969.
- Christina Vasilakopoulou. Enriched duality in double categories: 𝒱-categories and 𝒱-cocategories. J. Pure Appl. Algebra, 223(7):2889-2947, 2019. URL: https://doi.org/10.1016/j.jpaa.2018.10.003.