Document Open Access Logo

Stabilized Profunctors and Matrix Representation

Authors Takeshi Tsukada , Kazuyuki Asada , Kengo Hirata

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2026.34.pdf
  • Filesize: 0.82 MB
  • 18 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
  • Theory of computation → Linear logic
Keywords
  • Profunctor
  • weighted relational model
  • stability

Metrics

Abstract

The (bi)category of profunctors on groupoids is a categorification of the relational model of linear logic. Its objects are not just sets but rather sets whose elements are equipped with groups encoding their symmetries, and its morphisms carry actions by these symmetries. While detailed information on such symmetries helps with, e.g., adequacy proofs of profunctorial models, it makes operations such as composition more difficult to compute. A way to ease the computation is to transform a profunctor into a matrix. Although the matrix representation is not functorial in general, it is known to behave well for certain subclasses, such as the class of profunctors definable by λ-terms. The mathematical reason behind this phenomenon, however, was not understood.
This paper shows that the key is stability. Stability is a classical concept in domain theory, and has been extended to profunctors in Taylor’s work and further developed by Fiore et al. All λ-definable profunctors are known to be stabilized, and we show that the matrix representation behaves well for stabilized profunctors. We prove that the matrix representation defines a functor from stabilized profunctors to matrices that preserves the linear logic structures.

Cite As Get BibTex

Takeshi Tsukada, Kazuyuki Asada, and Kengo Hirata. Stabilized Profunctors and Matrix Representation. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 34:1-34:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.FSCD.2026.34

Author Details

Takeshi Tsukada
  • Chiba University, Japan
Kazuyuki Asada
  • Tohoku University, Japan
Kengo Hirata
  • University of Edinburgh, United Kingdom
  • Kyoto University, Japan

Acknowledgements

This work was supported by JSPS KAKENHI Grant Numbers JP25H00446 and JP24K14814.

References

  1. Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. Information and Computation, 163(2):409-470, December 2000. URL: https://doi.org/10.1006/inco.2000.2930.
  2. Patrick Baillot, Vincent Danos, Thomas Ehrhard, and Laurent Regnier. Timeless games. In Computer Science Logic, pages 56-77. Springer Berlin Heidelberg, 1998. URL: https://doi.org/10.1007/bfb0028007.
  3. François Bergeron, Gilbert Labelle, and Pierre Leroux. Combinatorial Species and Tree-like Structures. Cambridge University Press, November 1997. URL: https://doi.org/10.1017/cbo9781107325913.
  4. Gérard Berry. Stable models of typed λ-calculi, pages 72-89. Springer Berlin Heidelberg, 1978. URL: https://doi.org/10.1007/3-540-08860-1_7.
  5. Pierre Boudes. Projecting games on hypercoherences. In International Colloquium on Automata, Languages and Programming, pages 257-268. Springer Berlin Heidelberg, 2004. URL: https://doi.org/10.1007/978-3-540-27836-8_24.
  6. Jean Bénabou. Introduction to bicategories, pages 1-77. Springer Berlin Heidelberg, 1967. URL: https://doi.org/10.1007/bfb0074299.
  7. Ana C. Calderon and Guy McCusker. Understanding game semantics through coherence spaces. Electronic Notes in Theoretical Computer Science, 265:231-244, September 2010. URL: https://doi.org/10.1016/j.entcs.2010.08.014.
  8. Pierre Clairambault and Marc de Visme. Full abstraction for the quantum lambda-calculus. Proceedings of the ACM on Programming Languages, 4(POPL):1-28, December 2020. URL: https://doi.org/10.1145/3371131.
  9. Pierre Clairambault and Simon Forest. The cartesian closed bicategory of thin spans of groupoids. In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13. IEEE, June 2023. URL: https://doi.org/10.1109/lics56636.2023.10175754.
  10. Pierre Clairambault and Simon Forest. An analysis of symmetry in quantitative semantics. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’24, pages 1-13. ACM, July 2024. URL: https://doi.org/10.1145/3661814.3662092.
  11. Pierre Clairambault, Marc De Visme, and Glynn Winskel. Game semantics for quantum programming. Proceedings of the ACM on Programming Languages, 3(POPL):1-29, January 2019. URL: https://doi.org/10.1145/3290345.
  12. J.A.B. Cockett, M. Hasegawa, and R.A.G. Seely. Coherence of the double involution on *-autonomous categories. Theory and Applications of Categories, 17:17-29, 2006. URL: http://eudml.org/doc/127888.
  13. Thomas Ehrhard and Laurent Regnier. Uniformity and the taylor expansion of ordinary lambda-terms. Theoretical Computer Science, 403(2-3):347-372, August 2008. URL: https://doi.org/10.1016/j.tcs.2008.06.001.
  14. M. Fiore, N. Gambino, and M. Hyland. Monoidal bicategories, differential linear logic, and analytic functors, 2024. URL: https://doi.org/10.48550/arXiv.2405.05774.
  15. M. Fiore, N. Gambino, M. Hyland, and G. Winskel. The cartesian closed bicategory of generalised species of structures. Journal of the London Mathematical Society, 77(1):203-220, October 2007. URL: https://doi.org/10.1112/jlms/jdm096.
  16. Marcelo Fiore, Zeinab Galal, and Hugo Paquet. A combinatorial approach to higher-order structure for polynomial functors. In FSCD. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.FSCD.2022.31.
  17. Marcelo Fiore, Zeinab Galal, and Hugo Paquet. Stabilized profunctors and stable species of structures. Logical Methods in Computer Science, Volume 20, Issue 1, February 2024. URL: https://doi.org/10.46298/lmcs-20(1:17)2024.
  18. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  19. Jean-Yves Girard. Normal functors, power series and λ-calculus. Annals of Pure and Applied Logic, 37(2):129-177, February 1988. URL: https://doi.org/10.1016/0168-0072(88)90025-5.
  20. J.M.E. Hyland and C.-H.L. Ong. On full abstraction for PCF: I, II, and III. Information and Computation, 163(2):285-408, December 2000. URL: https://doi.org/10.1006/inco.2000.2917.
  21. Martin Hyland. Abstract interpretation of proofs: Classical propositional calculus. In Computer Science Logic (CSL 2004), pages 6-21. Springer Berlin Heidelberg, 2004. URL: https://doi.org/10.1007/978-3-540-30124-0_2.
  22. Martin Hyland and Andrea Schalk. Glueing and orthogonality for models of linear logic. Theoretical Computer Science, 294(1-2):183-231, February 2003. URL: https://doi.org/10.1016/s0304-3975(01)00241-9.
  23. André Joyal. Une théorie combinatoire des séries formelles. Advances in Mathematics, 42(1):1-82, October 1981. URL: https://doi.org/10.1016/0001-8708(81)90052-9.
  24. Jim Laird, Giulio Manzonetto, Guy McCusker, and Michele Pagani. Weighted relational models of typed lambda-calculi. In 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE, June 2013. URL: https://doi.org/10.1109/lics.2013.36.
  25. François Lamarche. Quantitative domains and infinitary algebras. Theoretical Computer Science, 94(1):37-62, March 1992. URL: https://doi.org/10.1016/0304-3975(92)90323-8.
  26. Paul-André Melliès. Asynchronous games 1: Uniformity by group invariance, 2003. URL: http://www.pps.univ-paris-diderot.fr/~mellies/papers/ag1.pdf.
  27. Paul-André Melliès. Sequential algorithms and strongly stable functions. Theoretical Computer Science, 343(1–2):237-281, October 2005. URL: https://doi.org/10.1016/j.tcs.2005.05.015.
  28. Paul-André Melliès. Categorical semantics of linear logic. In Interactive models of computation and program behaviour, panoramas et synthèses, volume 27, pages 1-196. Société Mathématique de France, 2009. Google Scholar
  29. Federico Olimpieri. Intersection type distributors. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-15. IEEE, June 2021. URL: https://doi.org/10.1109/lics52264.2021.9470617.
  30. Christian Retoré. A semantic characterisation of the correctness of a proof net. Mathematical Structures in Computer Science, 7(5):445-452, October 1997. URL: https://doi.org/10.1017/s096012959700234x.
  31. Andrea Schalk. What is a categorical model for linear logic? Available on the author’s web page: https://www.cs.man.ac.uk/~schalk/notes/index.html, 2004.
  32. Paul Taylor. Quantitative domains, groupoids and linear logic. In David H. Pitt, David E. Rydeheard, Peter Dybjer, Andrew M. Pitts, and Axel Poigné, editors, Category Theory and Computer Science, pages 155-181, Berlin, Heidelberg, 1989. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/BFB0018351.
  33. Takeshi Tsukada, Kazuyuki Asada, and Kengo Hirata. Full definability in a profunctorial model, 2026. URL: https://doi.org/10.48550/arXiv.2604.26829.
  34. 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). IEEE, June 2017. URL: https://doi.org/10.1109/lics.2017.8005093.
  35. Takeshi Tsukada, Kazuyuki Asada, and C.-H. Luke Ong. Species, profunctors and taylor expansion weighted by SMCC. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. ACM, July 2018. URL: https://doi.org/10.1145/3209108.3209157.
  36. Takeshi Tsukada and C.-H. Luke Ong. Nondeterminism in game semantics via sheaves. In 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE, July 2015. URL: https://doi.org/10.1109/lics.2015.30.
  37. Takeshi Tsukada and C.-H. Luke Ong. Plays as resource terms via non-idempotent intersection types. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. ACM, July 2016. URL: https://doi.org/10.1145/2933575.2934553.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact