A Unified Treatment of Substitution for Presheaves, Nominal Sets, Renaming Sets, and so on
For researchers in semantics of programming languages and categorical logic, this provides a unified categorical treatment of substitution across different models of syntax with binding, though the results are largely theoretical and incremental.
The paper introduces a closed monoidal structure on nominal sets to model substitution, using a general method that derives such structures from monoidal category actions. This method uniformly recovers known substitution tensors for presheaf categories and yields new ones for nominal and renaming sets, establishing correspondences between these frameworks.
Presheaves and nominal sets provide alternative abstract models of sets of syntactic objects with free and bound variables, such as lambda-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, modeling substitution 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 doing so, we shed new light on different incarnations of nominal sets and (pre-)sheaf categories and establish a number of known and new correspondences between them.