A Bicategorical Model for Finite Nondeterminism

Author Zeinab Galal

Thumbnail PDF


  • Filesize: 0.65 MB
  • 17 pages

Document Identifiers

Author Details

Zeinab Galal
  • IRIF, Université de Paris, France

Cite AsGet BibTex

Zeinab Galal. A Bicategorical Model for Finite Nondeterminism. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 10:1-10:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Finiteness spaces were introduced by Ehrhard as a refinement of the relational model of linear logic. A finiteness space is a set equipped with a class of finitary subsets which can be thought of being subsets that behave like finite sets. A morphism between finiteness spaces is a relation that preserves the finitary structure. This model provided a semantics for finite non-determism and it gave a semantical motivation for differential linear logic and the syntactic notion of Taylor expansion. In this paper, we present a bicategorical extension of this construction where the relational model is replaced with the model of generalized species of structures introduced by Fiore et al. and the finiteness property now relies on finite presentability.

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
  • Theory of computation → Categorical semantics
  • Differential linear logic
  • Species of structures
  • Finiteness
  • Bicategorical semantics


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


  1. Joey Beauvais-Feisthauer, Richard Blute, Ian Dewan, Blair Drummond, and Pierre-Alain Jacqmin. Finiteness spaces, étale groupoids and their convolution algebras. In Semigroup Forum, pages 1-16. Springer, 2020. Google Scholar
  2. Nicolas Behr. On Stochastic Rewriting and Combinatorics via Rule-Algebraic Methods. In Patrick Bahr, editor, Proceedings 11th International Workshop on Computing with Terms and Graphs (TERMGRAPH 2020), volume 334, pages 11-28. Open Publishing Association, 2021. Google Scholar
  3. Jean Bénabou. Distributors at work, 2000. Lecture notes written by Thomas Streicher. URL: https://www2.mathematik.tu-darmstadt.de/~streicher/FIBR/DiWo.pdf.
  4. 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. Translated from the 1994 French original by Margaret Readdy, With a foreword by Gian-Carlo Rota. Google Scholar
  5. Richard Blute, Robin Cockett, Pierre-Alain Jacqmin, and Philip Scott. Finiteness spaces and generalized power series. Electronic Notes in Theoretical Computer Science, 341:5-22, 2018. Google Scholar
  6. Richard F. Blute. Hopf algebras and linear logic. Mathematical Structures in Computer Science, 6(2):189-212, 1996. Google Scholar
  7. Gian Luca Cattani and Glynn Winskel. Profunctors, open maps and bisimulation. Mathematical Structures in Computer Science, 15:553-614, June 2005. Google Scholar
  8. Thomas Ehrhard. On köthe sequence spaces and linear logic. Mathematical. Structures in Comp. Sci., 12(5):579-623, 2002. Google Scholar
  9. Thomas Ehrhard. Finiteness spaces. Mathematical Structures in Computer Science, 15(4):615-646, 2005. 32 pages. Google Scholar
  10. Thomas Ehrhard. An introduction to differential linear logic: proof-nets, models and antiderivatives. Mathematical Structures in Computer Science, 28(7):995–1060, 2018. Google Scholar
  11. Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. Theor. Comput. Sci., 309(1):1-41, 2003. Google Scholar
  12. Marcelo Fiore. Analytic functors between presheaf categories over groupoids. Theor. Comput. Sci., 546:120-131, 2014. Google Scholar
  13. 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. Google Scholar
  14. Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures. Selecta Mathematica, 24(3):2791-2830, 2018. Google Scholar
  15. Nicola Gambino and André Joyal. On Operads, Bimodules and Analytic Functors. Memoirs of the American Mathematical Society. American Mathematical Society, 2017. Google Scholar
  16. Jean-Yves Girard. Normal functors, power series and λ-calculus. Ann. Pure Appl. Logic, 37(2):129-177, 1988. Google Scholar
  17. Jean-Yves Girard. Coherent Banach Spaces: a continuous denotational semantics extended abstract. Electronic Notes in Theoretical Computer Science, 3:81-87, 1996. Linear Logic 96 Tokyo Meeting. Google Scholar
  18. Ryu Hasegawa. Two applications of analytic functors. Theoretical Computer Science, 272(1):113-175, 2002. Theories of Types and Proofs 1997. Google Scholar
  19. Martin Hyland. Some reasons for generalising domain theory. Mathematical Structures in Computer Science, 20(2):239-265, 2010. Google Scholar
  20. Martin Hyland and Andrea Schalk. Glueing and orthogonality for models of linear logic. Theoretical Computer Science, 294(1):183-231, 2003. Category Theory and Computer Science. Google Scholar
  21. André Joyal. Une théorie combinatoire des séries formelles. Adv. in Math., 42(1):1-82, 1981. Google Scholar
  22. 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
  23. Ralph Loader. Linear logic, totality and full completeness. In In Proceedings of LiCS `94, pages 292-298. Press, 1994. Google Scholar
  24. Michele Pagani, Peter Selinger, and Benoît Valiron. Applying quantitative semantics to higher-order quantum computing. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 647-658, 2014. Google Scholar
  25. Michele Pagani, Christine Tasson, and Lionel Vaux. Strong normalizability as a finiteness structure via the Taylor expansion of lambda-terms. In International Conference on Foundations of Software Science and Computation Structures, pages 408-423. Springer, 2016. Google Scholar
  26. Lionel Vaux. A non-uniform finitary relational semantics of system T. RAIRO - Theoretical Informatics and Applications, 47(1):111-132, 2013. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail