A Unified Treatment of the Substitution Tensor for Presheaves, Nominal Sets, Renaming Sets, and so on
Lenke F, Milius S, Urbat H (2026)
Publication Type: Conference contribution
Publication year: 2026
Journal
Publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Book Volume: 380
Conference Proceedings Title: Leibniz International Proceedings in Informatics, LIPIcs
Event location: Lisbon
ISBN: 9783959774345
DOI: 10.4230/LIPIcs.LICS.2026.65
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.
Authors with CRIS profile
Fabian Lenke
Lehrstuhl für Informatik 8 (Theoretische Informatik)
Stefan Milius
Lehrstuhl für Informatik 8 (Theoretische Informatik)
Henning Urbat
Lehrstuhl für Informatik 8 (Theoretische Informatik)
How to cite
APA:
Lenke, F., Milius, S., & Urbat, H. (2026). A Unified Treatment of the Substitution Tensor for Presheaves, Nominal Sets, Renaming Sets, and so on. In Faggian Claudia, Katoen Joost-Pieter, Katoen Joost-Pieter (Eds.), Leibniz International Proceedings in Informatics, LIPIcs. Lisbon, PT: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing.
MLA:
Lenke, Fabian, Stefan Milius, and Henning Urbat. "A Unified Treatment of the Substitution Tensor for Presheaves, Nominal Sets, Renaming Sets, and so on." Proceedings of the 41st Annual Symposium on Logic in Computer Science, LICS 2026, Lisbon Ed. Faggian Claudia, Katoen Joost-Pieter, Katoen Joost-Pieter, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2026.
BibTeX: Download