Document Open Access Logo

A Unified Treatment of the Substitution Tensor for Presheaves, Nominal Sets, Renaming Sets, and so on

Authors Fabian Lenke , Stefan Milius , Henning Urbat

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.65.pdf
  • Filesize: 1.35 MB
  • 27 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation
Keywords
  • Substitution
  • Presheaves
  • Nominal Sets
  • Monoidal Category

Metrics

Abstract

Presheaves and nominal sets provide alternative abstract models of sets of syntactic objects with free and bound variables, such as λ-terms. One distinguishing feature of the presheaf-based perspective is its elegant syntax-free characterization of substitution using a closed monoidal structure. In this paper, we introduce a corresponding closed monoidal structure on nominal sets, in the spirit of Fiore et al.’s substitution tensor for presheaves over finite sets. To this end, we present a general method to derive a closed monoidal structure on a category from a given action of a monoidal category on that category. We demonstrate that this method not only uniformly recovers known substitution tensors for various kinds of presheaf categories but also yields notions of substitution tensor for nominal sets and their relatives, such as renaming sets. In the process, we shed new light on different incarnations of nominal sets and (pre-)sheaf categories and establish a number of correspondences between them.

Cite As Get BibTex

Fabian Lenke, Stefan Milius, and Henning Urbat. A Unified Treatment of the Substitution Tensor for Presheaves, Nominal Sets, Renaming Sets, and so on. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 65:1-65:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.65

Author Details

Fabian Lenke
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
Stefan Milius
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
Henning Urbat
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

Funding

  • Lenke, Fabian: Fabian Lenke is supported by Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - project number 419850228.
  • Milius, Stefan: Stefan Milius is supported by Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - project number 517924115.
  • Urbat, Henning: Henning Urbat are supported by Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - project number 569130867.

Acknowledgements

We thank Nathanael Arkor and the reviewers for the various pointers to the literature, insightful comments and helpful suggestions and simplifications.

References

  1. Jiří Adámek, Stefan Milius, and Jiří Velebil. Semantics of higher-order recursion schemes. Log. Methods Comput. Sci., 7(1:15):43 pp., 2011. URL: https://doi.org/10.2168/LMCS-7(1:15)2011.
  2. Thorsten Altenkirch, James Chapman, and Tarmo Uustalu. Monads need not be endofunctors. Log. Methods Comput. Sci., 11(1), 2015. URL: https://doi.org/10.2168/LMCS-11(1:3)2015.
  3. Mikolaj Bojanczyk, Laurent Braud, Bartek Klin, and Slawomir Lasota. Towards nominal computation. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '12, pages 401-412, New York, NY, USA, 2012. Association for Computing Machinery. URL: https://doi.org/10.1145/2103656.2103704.
  4. Mikolaj Bojanczyk, Bartek Klin, and Slawomir Lasota. Automata theory in nominal sets. Log. Methods Comput. Sci., 10(3), 2014. URL: https://doi.org/10.2168/LMCS-10(3:4)2014.
  5. Francis Borceux and Maria Cristina Pedicchio. A characterization of quasi-toposes. Journal of Algebra, 139(2):505-526, 1991. URL: https://doi.org/10.1016/0021-8693(91)90306-S.
  6. Ranald Clouston. Generalised name abstraction for nominal sets. In Frank Pfenning, editor, Foundations of Software Science and Computation Structures, pages 434-449, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-37075-5_28.
  7. Pierre-Louis Curien. Operads, clones, and distributive laws. Operads and Universal Algebra, 9:25-49, May 2012. URL: https://doi.org/10.1142/9789814365123_0002.
  8. Brian Day. Construction of Biclosed Categories. PhD thesis, Macquarie University, 1970. Google Scholar
  9. Marcelo Fiore. Notes on combinatorial functors. Draft available electronically, 2001. Google Scholar
  10. Marcelo Fiore. Second-order and dependently-sorted abstract syntax. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, pages 57-68. IEEE Computer Society, 2008. URL: https://doi.org/10.1109/LICS.2008.38.
  11. Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. The cartesian closed bicategory of generalised species of structures. Journal of the London Mathematical Society, 77(1):203-220, 2008. URL: https://doi.org/10.1112/jlms/jdm096.
  12. Marcelo Fiore and Matías Menni. Reflective kleisli subcategories of the category of eilenberg-moore algebras for factorization monads. Theory and Applications of Categories [electronic only], 15:40-65, 2005. URL: http://eudml.org/doc/125160.
  13. Marcelo Fiore, Gordon Plotkin, and Daniele Turi. Abstract syntax and variable binding. In Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, LICS '99, page 193, USA, 1999. IEEE Computer Society. Google Scholar
  14. Marcelo Fiore and Sanjiv Ranchod. Substructural abstract syntax with variable binding and single-variable substitution. In 40th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2025, Singapore, June 23-26, 2025, pages 196-208. IEEE, 2025. URL: https://doi.org/10.1109/LICS65433.2025.00022.
  15. Marcelo Fiore and Dmitrij Szamozvancev. Formal metatheory of second-order abstract syntax. Proc. ACM Program. Lang., 6(POPL):1-29, 2022. URL: https://doi.org/10.1145/3498715.
  16. Florian Frank, Daniel Hausmann, Stefan Milius, Lutz Schröder, and Henning Urbat. Alternating nominal automata with name allocation. In 40th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2025, Singapore, June 23-26, 2025, pages 57-70. IEEE, 2025. URL: https://doi.org/10.1109/LICS65433.2025.00012.
  17. Murdoch J. Gabbay. A Theory of Inductive Definitions with alpha-Equivalence. phdthesis, University of Cambridge, UK, 2001. URL: http://www.gabbay.org.uk/papers.html#thesis.
  18. Murdoch J. Gabbay. A study of substitution, using nominal techniques and fraenkel–mostowksi sets. Theoretical Computer Science, 410(12):1159-1189, 2009. URL: https://doi.org/10.1016/j.tcs.2008.11.013.
  19. Murdoch J. Gabbay. Semantics out of context: Nominal absolute denotations for first-order logic and computation. J. ACM, 63(3), 2016. URL: https://doi.org/10.1145/2700819.
  20. Murdoch J. Gabbay and James Cheney. A sequent calculus for nominal logic. In 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings, pages 139-148. IEEE Computer Society, 2004. URL: https://doi.org/10.1109/LICS.2004.1319608.
  21. Murdoch J. Gabbay and Martin Hofmann. Nominal renaming sets. In Iliano Cervesato, Helmut Veith, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings, volume 5330 of Lecture Notes in Computer Science, pages 158-173. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-89439-1_11.
  22. Murdoch J. Gabbay and Aad Mathijssen. Capture-avoiding substitution as a nominal algebra. Form. Asp. Comput., 20(4–5):451-479, 2008. URL: https://doi.org/10.1007/s00165-007-0056-1.
  23. Murdoch J. Gabbay and Aad Mathijssen. Nominal (universal) algebra: Equational logic with names and binding. J. Log. Comput., 19(6):1455-1508, 2009. URL: https://doi.org/10.1093/LOGCOM/EXP033.
  24. Murdoch J. Gabbay and Andrew M. Pitts. A new approach to abstract syntax involving binders. In Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1999), pages 214-224. IEEE Computer Society Press, July 1999. URL: https://doi.org/10.1109/LICS.1999.782617.
  25. Richard Garner and Ignacio López Franco. Commutativity. Journal of Pure and Applied Algebra, 220(5):1707-1751, 2016. URL: https://doi.org/10.1016/j.jpaa.2015.09.003.
  26. Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat. Towards a higher-order mathematical operational semantics. Proceedings of the ACM on Programming Languages, 7(POPL):632-658, 2023. URL: https://doi.org/10.1145/3571215.
  27. Makoto Hamana. Polymorphic abstract syntax via grothendieck construction. In Martin Hofmann, editor, Foundations of Software Science and Computational Structures - 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, volume 6604 of Lecture Notes in Computer Science, pages 381-395. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-19805-2_26.
  28. Geun Bin IM and Max Kelly. A universal property of the convolution monoidal structure. Journal of Pure and Applied Algebra, 43(1):75-88, 1986. URL: https://doi.org/10.1016/0022-4049(86)90005-8.
  29. G. Janelidze and Max Kelly. A note on actions of a monoidal category. Theory and Applications of Categories, 9:61-91, 2001. URL: http://eudml.org/doc/122510.
  30. Peter T. Johnstone. Sketches of an Elephant: A Topos Theory Compendium, Volume 1. Clarendon Press, Oxford, England, 2002. Google Scholar
  31. Peter T. Johnstone and Gavin C. Wraith. Algebraic theories in toposes. In Indexed Categories and Their Applications, pages 141-242, Berlin, Heidelberg, 1978. Springer Berlin Heidelberg. Google Scholar
  32. André Joyal. Une théorie combinatoire des séries formelles. Advances in Mathematics, 42(1):1-82, 1981. URL: https://doi.org/10.1016/0001-8708(81)90052-9.
  33. Max Kelly. Basic concepts of enriched category theory. Reprints in Theory and Applications of Categegories, pages vi+137, 2005. Google Scholar
  34. Max Kelly. On the operads of j.p. may. Reprints in Theory and Applications of Categegories, pages 1-13, 2005. Google Scholar
  35. Alexander Kurz and Daniela Petrisan. On universal algebra over nominal sets. Math. Struct. Comput. Sci., 20(2):285-318, 2010. URL: https://doi.org/10.1017/S0960129509990399.
  36. John M. Li, Jon Aytac, Philip Johnson-Freyd, Amal Ahmed, and Steven Holtzen. A nominal approach to probabilistic separation logic. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '24, New York, NY, USA, 2024. Association for Computing Machinery. URL: https://doi.org/10.1145/3661814.3662135.
  37. Fosco Loregian. (Co)end Calculus. London Mathematical Society Lecture Note Series. Cambridge University Press, 2021. Google Scholar
  38. Saunders Mac Lane. Categories for the Working Mathematician. Springer-Verlag, 1971. URL: https://doi.org/10.1007/978-1-4757-4721-8.
  39. Saunders Mac Lane and Ieke Moerdijk. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Universitext. Springer, New York, 1992. Google Scholar
  40. Fiore Marcelo. Towards a mathematical theory of substitution, 2007. Invited talk for the Annual International Conference on Category Theory, Carvoeiro, Algarve (Portugal). URL: https://www.cl.cam.ac.uk/~mpf23/talks/CT2007.pdf.
  41. Joshua Moerman and Jurriaan Rot. Separation and renaming in nominal sets. In Maribel Fernández and Anca Muscholl, editors, 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain, volume 152 of LIPIcs, pages 31:1-31:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CSL.2020.31.
  42. Andrew M. Pitts. Nominal logic, a first order theory of names and binding. Inf. Comput., 186(2):165-193, 2003. URL: https://doi.org/10.1016/S0890-5401(03)00138-X.
  43. Andrew M. Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge University Press, 2013. Google Scholar
  44. John Power. A unified category theoretic approach to variable binding. In Proceedings of the 2003 ACM SIGPLAN Workshop on Mechanized Reasoning about Languages with Variable Binding, MERLIN '03, pages 1-9, New York, NY, USA, 2003. Association for Computing Machinery. URL: https://doi.org/10.1145/976571.976578.
  45. John Power. Abstract syntax: Substitution and binders: Invited address. In Marcelo Fiore, editor, Proceedings of the 23rd Conference on the Mathematical Foundations of Programming Semantics, MFPS 2007, New Orleans, LA, USA, April 11-14, 2007, volume 173 of Electronic Notes in Theoretical Computer Science, pages 3-16. Elsevier, 2007. URL: https://doi.org/10.1016/J.ENTCS.2007.02.024.
  46. John Power and Miki Tanaka. Category theoretic semantics for typed binding signatures with recursion. Fundam. Inf., 84(2):221-240, April 2008. URL: http://content.iospress.com/articles/fundamenta-informaticae/fi84-2-05.
  47. Pavla Procházková. Skew monoidal structures on actegories. Theory and Applications of Categories [electronic only], 44(38):1282-1315, 2005. URL: http://www.tac.mta.ca/tac/volumes/44/38/44-38abs.html.
  48. Lutz Schröder, Dexter Kozen, Stefan Milius, and Thorsten Wißmann. Nominal automata with name binding. In Javier Esparza and Andrzej S. Murawski, editors, Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10203 of Lecture Notes in Computer Science, pages 124-142, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_8.
  49. Mark R. Shinwell. Fresh o'caml: Nominal abstract syntax for the masses. In Nick Benton and Xavier Leroy, editors, Proceedings of the ACM-SIGPLAN Workshop on ML, ML 2005, Tallinn, Estonia, September 29, 2005, volume 148(2) of Electronic Notes in Theoretical Computer Science, pages 53-77. Elsevier, 2005. URL: https://doi.org/10.1016/J.ENTCS.2005.11.040.
  50. Samuel Staton. Name-passing process calculi : operational models and structural operational semantics. PhD thesis, University of Cambridge, UK, 2007. URL: https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.613115.
  51. Stanislaw Szawiel and Marek W. Zawadowski. Monads of regular theories. Appl. Categorical Struct., 23(3):215-262, 2015. URL: https://doi.org/10.1007/S10485-013-9331-X.
  52. Kornél Szlachányi. On the tensor product of modules over skew monoidal actegories. Journal of Pure and Applied Algebra, 221(1):185-221, 2017. URL: https://doi.org/10.1016/j.jpaa.2016.06.003.
  53. Miki Tanaka. Abstract syntax and variable binding for linear binders. In Mogens Nielsen and Branislav Rovan, editors, Mathematical Foundations of Computer Science 2000, pages 670-679, Berlin, Heidelberg, 2000. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-44612-5_62.
  54. Miki Tanaka. Pseudo-Distributive Laws and a Unified Framework for Variable Binding. PhD thesis, University of Edinburgh, 2004. Google Scholar
  55. S.N. Tronin. Abstract clones and operads. Sibirskij Matematicheskij Zhurnal, 43(4):924-936 (2002); translation in Sib. Math. J. 43, 2002. URL: http://eudml.org/doc/50186.
  56. Henning Urbat, Daniel Hausmann, Stefan Milius, and Lutz Schröder. Nominal Büchi automata with name allocation. In CONCUR 2021, pages 4:1-4:16, 2021. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2021.4.
  57. Berend van Starkenburg, Henning Basold, and Chase Ford. Separation logic of generic resources via sheafeology. CoRR, abs/2508.01866, 2025. URL: https://doi.org/10.48550/arXiv.2508.01866.
  58. Thorsten Wißmann. Supported sets - A new foundation for nominal sets and automata. In Bartek Klin and Elaine Pimentel, editors, 31st EACSL Annual Conference on Computer Science Logic, CSL 2023, February 13-16, 2023, Warsaw, Poland, volume 252 of LIPIcs, pages 38:1-38:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.CSL.2023.38.
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