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 novel 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 novel correspondences between them.
翻译:预层与名义集为具有自由变量与约束变量的语法对象集合(如λ项)提供了两种不同的抽象模型。基于预层视角的一个显著特征在于其利用闭幺半结构对替换操作进行了优雅的、独立于语法的刻画。本文在名义集上引入相应的闭幺半结构,以Fiore等人提出的有限集上预层替换张量为范式对替换操作进行建模。为此,我们提出一种通用方法:通过给定幺半范畴在目标范畴上的作用,推导出该范畴上的闭幺半结构。我们证明该方法不仅能统一重构各类预层范畴中已知的替换张量,还能为名义集及其相关范畴(如重命名集)推导出新的替换张量概念。在此过程中,我们为名义集与(预)层范畴的不同表现形式提供了新的理论视角,并在它们之间建立了若干新颖的对应关系。