Document Open Access Logo

A Combinatorial Approach to Higher-Order Structure for Polynomial Functors

Authors Marcelo Fiore , Zeinab Galal, Hugo Paquet

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2022.31.pdf
  • Filesize: 0.88 MB
  • 19 pages

Document Identifiers

Author Details

Marcelo Fiore
  • University of Cambridge, UK
Zeinab Galal
  • University of Leeds, UK
Hugo Paquet
  • University of Oxford, UK

Funding

  • Fiore, Marcelo: Research partially supported by EPSRC grant EP/V002309/1.
  • Galal, Zeinab: Research partially supported by EPSRC grant EP/V002309/1 and by ANR grant ANR-20-CE48-0010.
  • Paquet, Hugo: Research supported by a Royal Society University Research Fellowship.

Cite AsGet BibTex

Marcelo Fiore, Zeinab Galal, and Hugo Paquet. A Combinatorial Approach to Higher-Order Structure for Polynomial Functors. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.FSCD.2022.31

Abstract

Polynomial functors are categorical structures used in a variety of applications across theoretical computer science; for instance, in database theory, denotational semantics, functional programming, and type theory. A well-known problem is that the bicategory of finitary polynomial functors between categories of indexed sets is not cartesian closed, despite its success and influence on denotational models and linear logic. This paper introduces a formal bridge between the model of finitary polynomial functors and the combinatorial theory of generalised species of structures. Our approach consists in viewing finitary polynomial functors as free analytic functors, which correspond to free generalised species. In order to systematically consider finitary polynomial functors from this combinatorial perspective, we study a model of groupoids with additional logical structure; this is used to constrain the generalised species between them. The result is a new cartesian closed bicategory that embeds finitary polynomial functors.

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
  • Theory of computation → Lambda calculus
  • Mathematics of computing → Combinatorics
Keywords
  • Bicategorical models
  • denotational semantics
  • stable domain theory
  • linear logic
  • polynomial functors
  • species of structures
  • groupoids

Metrics

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

References

  1. Michael Abbott, Thorsten Altenkirch, and Neil Ghani. Containers: Constructing strictly positive types. Theor. Comput. Sci., 342(1):3-27, 2005. URL: https://doi.org/10.1016/j.tcs.2005.06.002.
  2. Michael Abbott, Thorsten Altenkirch, Conor McBride, and Neil Ghani. ∂ for data: Differentiating data structures. Fundam. Informaticae, 65(1-2):1-28, 2005. Google Scholar
  3. Jiří Adámek. A categorical generalization of Scott domains. Mathematical Structures in Computer Science, 7(5):419-443, 1997. URL: https://doi.org/10.1017/S0960129597002351.
  4. Thorsten Altenkirch, Neil Ghani, Peter G. Hancock, Conor McBride, and Peter Morris. Indexed containers. J. Funct. Program., 25, 2015. URL: https://doi.org/10.1017/S095679681500009X.
  5. Steve Awodey and Clive Newstead. Polynomial pseudomonads and dependent type theory, 2018. URL: https://doi.org/10.48550/ARXIV.1802.00997.
  6. Jean Bénabou. Introduction to bicategories. In Reports of the Midwest Category Seminar, pages 1-77, Berlin, Heidelberg, 1967. Springer Berlin Heidelberg. Google Scholar
  7. Jean Bénabou. Distributors at work, 2000. Lecture notes written by Thomas Streicher. URL: https://www2.mathematik.tu-darmstadt.de/~streicher/FIBR/DiWo.pdf.
  8. F. Bergeron, G. Labelle, and P. Leroux. Combinatorial species and tree-like structures, volume 67 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge, 1998. Google Scholar
  9. Gérard Berry. Stable models of typed lambda-calculi. In Proceedings of the Fifth Colloquium on Automata, Languages and Programming, pages 72-89, Berlin, Heidelberg, 1978. Springer-Verlag. Google Scholar
  10. Thomas Ehrhard. An introduction to differential linear logic: Proof-nets, models and antiderivatives. Mathematical Structures in Computer Science, 28:995-1060, 2018. URL: https://doi.org/10.1017/S0960129516000372.
  11. Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. Theoretical Computer Science, 309(1-3):1-41, 2003. Google Scholar
  12. Eric Finster, Samuel Mimram, Maxime Lucas, and Thomas Seiller. A cartesian bicategory of polynomial functors in homotopy type theory. In Ana Sokolova, editor, Proceedings 37th Conference on Mathematical Foundations of Programming Semantics, MFPS 2021, Hybrid: Salzburg, Austria and Online, 30th August - 2nd September, 2021, volume 351 of EPTCS, pages 67-83, 2021. URL: https://doi.org/10.4204/EPTCS.351.5.
  13. M. Fiore, N. Gambino, M. Hyland, and G. Winskel. Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures. Selecta Mathematica, 24(3):2791-2830, 2018. URL: https://doi.org/10.1007/s00029-017-0361-3.
  14. Marcelo Fiore. Mathematical models of computational and combinatorial structures. In International Conference on Foundations of Software Science and Computation Structures, pages 25-46. Springer, 2005. Google Scholar
  15. Marcelo Fiore. Discrete generalised polynomial functors. In Automata, Languages, and Programming, pages 214-226. Springer, 2012. Google Scholar
  16. Marcelo Fiore. Analytic functors between presheaf categories over groupoids. Theor. Comput. Sci., 546:120-131, 2014. URL: https://doi.org/10.1016/j.tcs.2014.03.004.
  17. Marcelo Fiore. An axiomatics and a combinatorial model of creation/annihilation operators, 2015. URL: https://doi.org/10.48550/ARXIV.1506.06402.
  18. Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. The cartesian closed bicategory of generalised species of structures. J. Lond. Math. Soc. (2), 77(1):203-220, 2008. URL: https://doi.org/10.1112/jlms/jdm096.
  19. Marcelo Fiore and Philip Saville. A type theory for cartesian closed bicategories. In 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13. IEEE, 2019. Google Scholar
  20. Zeinab Galal. A bicategorical model for finite nondeterminism. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2021. Google Scholar
  21. Nicola Gambino and Martin Hyland. Wellfounded trees and dependent polynomial functors. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors, Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers, volume 3085 of Lecture Notes in Computer Science, pages 210-225. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-24849-1_14.
  22. Nicola Gambino and Joachim Kock. Polynomial functors and polynomial monads. Mathematical Proceedings of the Cambridge Philosophical Society, 154(1):153-192, 2013. URL: https://doi.org/10.1017/S0305004112000394.
  23. David Gepner, Rune Haugseng, and Joachim Kock. ∞-Operads as analytic monads. International Mathematics Research Notices, 2021. URL: https://doi.org/10.1093/imrn/rnaa332.
  24. Jean-Yves Girard. The system F of variable types, fifteen years later. Theor. Comput. Sci., 45(2):159-192, 1986. URL: https://doi.org/10.1016/0304-3975(86)90044-7.
  25. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  26. Jean-Yves Girard. Normal functors, power series and λ-calculus. Ann. Pure Appl. Logic, 37(2):129-177, 1988. URL: https://doi.org/10.1016/0168-0072(88)90025-5.
  27. Makoto Hamana and Marcelo Fiore. A foundation for gadts and inductive families: Dependent polynomial functor approach. In Proceedings of the Seventh ACM SIGPLAN Workshop on Generic Programming, WGP '11, pages 59-70. Association for Computing Machinery, 2011. URL: https://doi.org/10.1145/2036918.2036927.
  28. Ryu Hasegawa. Two applications of analytic functors. Theoretical Computer Science, 272(1):113-175, 2002. URL: https://doi.org/10.1016/S0304-3975(00)00349-2.
  29. Martin Hyland. Some reasons for generalising domain theory. Math. Struct. Comput. Sci., 20(2):239-265, 2010. URL: https://doi.org/10.1017/S0960129509990375.
  30. Martin Hyland and Andrea Schalk. Glueing and orthogonality for models of linear logic. Theoretical Computer Science, 294(1):183-231, 2003. URL: https://doi.org/10.1016/S0304-3975(01)00241-9.
  31. André Joyal. Une théorie combinatoire des séries formelles. Adv. in Math., 42(1):1-82, 1981. URL: https://doi.org/10.1016/0001-8708(81)90052-9.
  32. André Joyal. Foncteurs analytiques et espèces de structures. In Gilbert Labelle and Pierre Leroux, editors, Combinatoire énumérative, pages 126-159, Berlin, Heidelberg, 1986. Springer Berlin Heidelberg. Google Scholar
  33. Joachim Kock. Data types with symmetries and polynomial functors over groupoids. Electronic Notes in Theoretical Computer Science, 286:351-365, 2012. Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVIII). URL: https://doi.org/10.1016/j.entcs.2013.01.001.
  34. Gilbert Labelle. Combinatorial integration (Part I, Part II). ACM Commun. Comput. Algebra, 49(1):35, June 2015. URL: https://doi.org/10.1145/2768577.2768653.
  35. François Lamarche. Modelling polymorphism with categories. PhD thesis, McGill University, 1988. Google Scholar
  36. François Lamarche. Quantitative domains and infinitary algebras. Theoretical Computer Science, 94:37-62, 1992. Google Scholar
  37. F. William Lawvere. Metric spaces, generalized logic, and closed categories. Rendiconti del Seminario Matematico e Fisico di Milano, 43:135-166, 1973. Republished in: Reprints in Theory and Applications of Categories, No. 1 (2002) pp 1-37. Google Scholar
  38. P. Leroux and G.X. Viennot. Combinatorial resolution of systems of differential equations. IV. Separation of variables. Discrete Mathematics, 72(1-3):237-250, 1988. URL: https://doi.org/10.1016/0012-365X(88)90213-0.
  39. Conor McBride. The derivative of a regular type is its type of one-hole contexts, 2001. Unpublished manuscript. Google Scholar
  40. Paul-André Melliès. Template games and differential linear logic. In 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13. IEEE, 2019. Google Scholar
  41. Lê Thành Dung Nguyên and Pierre Pradic. From normal functors to logarithmic space queries. In Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi, editors, 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, July 9-12, 2019, Patras, Greece, volume 132 of LIPIcs, pages 123:1-123:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.123.
  42. Federico Olimpieri. Intersection type distributors. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-15. IEEE, 2021. Google Scholar
  43. David Spivak. Poly: An abundant categorical setting for mode-dependent dynamics, 2020. URL: https://doi.org/10.48550/ARXIV.2005.01894.
  44. Ross Street. The petit topos of globular sets. Journal of Pure and Applied Algebra, 154(1):299-315, 2000. URL: https://doi.org/10.1016/S0022-4049(99)00183-8.
  45. Paul Taylor. Quantitative domains, groupoids and linear logic. In Category Theory and Computer Science, pages 155-181. Springer, 1989. Google Scholar
  46. Paul Taylor. An algebraic approach to stable domains. Journal of Pure and Applied Algebra, 64(2):171-203, 1990. URL: https://doi.org/10.1016/0022-4049(90)90156-C.
  47. Takeshi Tsukada, Kazuyuki Asada, and C.-H. Luke Ong. Generalised species of rigid resource terms. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-12. IEEE, 2017. Google Scholar
  48. Tamara Von Glehn. Polynomials and models of type theory. PhD thesis, University of Cambridge, 2015. Google Scholar
  49. Mark Weber. Generic morphisms, parametric representations and weakly cartesian monads. Theory and Applications of Categories, 13(14):191-234, 2004. Google Scholar
  50. Nobuo Yoneda. On Ext and exact sequences. Journal of the Faculty of Science, Imperial University of Tokyo, 8:507-576, 1960. 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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact