关于预层、名义集合、重命名集合等替换的统一处理
A Unified Treatment of Substitution for Presheaves, Nominal Sets, Renaming Sets, and so on
AI总结:
本文通过从幺半范畴作用导出闭幺半结构的方法,统一为预层、名义集合及其变体(如重命名集合)构造替换张量,揭示它们之间的新对应关系。
摘要:
预层和名义集合提供了带自由变量和绑定变量的语法对象集合(如lambda项)的替代抽象模型。基于预层的视角的一个显著特征是其使用闭幺半结构对替换进行的优雅的无语法刻画。在本文中,我们在名义集合上引入了相应的闭幺半结构,以Fiore等人关于有限集上预层的替换张量的精神建模替换。为此,我们提出了一种通用方法,从给定幺半范畴在该范畴上的作用导出该范畴上的闭幺半结构。我们证明该方法不仅统一地恢复了各种预层范畴的已知替换张量,还为名义集合及其相关概念(如重命名集合)产生了替换张量的概念。在此过程中,我们为名义集合和(预)层范畴的不同表现形式提供了新的见解,并建立了它们之间一些已知和新的对应关系。
英文摘要:
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.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。