Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Fabian Lenke, Stefan Milius, Henning Urbat

TL;DR

This work develops a general method to derive closed monoidal substitution structures from a left action of a monoidal category on a base category and applies it to presheaves and nominal/renaming sets. By instantiating the framework to presheaf categories over various untyped contexts, it yields a uniform, contextually grounded substitution tensor that recovers Fiore–Plotkin–Turi’s original construction and extends it to nominal and renaming settings with simpler, explicit descriptions. It further establishes correspondences between presheaf categories and nominal-type models (e.g., $ ext{PSh}( ext{B})$ with Nom, $ ext{PSh}( ext{S})$ with Ren), and shows that Day convolution encodes uniform substitution across contexts. The resulting nominal substitutions fill a gap in nominal-set theory, enabling a unified semantic treatment of binding and substitution across a spectrum of models, with potential implications for initial semantics of binding signatures and higher-order operational frameworks. Overall, the paper provides a cohesive taxonomy and a robust technical toolkit for connecting presheaf and nominal-style approaches to syntax with binding.

Abstract

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.

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

TL;DR

This work develops a general method to derive closed monoidal substitution structures from a left action of a monoidal category on a base category and applies it to presheaves and nominal/renaming sets. By instantiating the framework to presheaf categories over various untyped contexts, it yields a uniform, contextually grounded substitution tensor that recovers Fiore–Plotkin–Turi’s original construction and extends it to nominal and renaming settings with simpler, explicit descriptions. It further establishes correspondences between presheaf categories and nominal-type models (e.g., with Nom, with Ren), and shows that Day convolution encodes uniform substitution across contexts. The resulting nominal substitutions fill a gap in nominal-set theory, enabling a unified semantic treatment of binding and substitution across a spectrum of models, with potential implications for initial semantics of binding signatures and higher-order operational frameworks. Overall, the paper provides a cohesive taxonomy and a robust technical toolkit for connecting presheaf and nominal-style approaches to syntax with binding.

Abstract

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.
Paper Structure (27 sections, 44 theorems, 142 equations)

This paper contains 27 sections, 44 theorems, 142 equations.

Table of Contents

  1. Introduction
  2. Contributions
  3. Outline
  4. Substitution, Abstractly
  5. Models.
  6. Substitution.
  7. Categorical Preliminaries
  8. Ends and Coends.
  9. Copowers.
  10. The Yoneda Lemma.
  11. Kan Extensions
  12. Day Convolution.
  13. Monoidal Structures from Actions
  14. Substitution in Presheaves
  15. Pullbacks.
  16. ...and 12 more sections

Key Result

Lemma 3.2

For every small category $\mathbf{C}\xspace$ we have the following isomorphisms, natural in $F \in \mathop{\mathrm{\mathbf{PSh}}}\nolimits \mathbf{C}\xspace$ and $C \in \mathbf{C}\xspace$:

Theorems & Definitions (71)

  • Lemma 3.2: Yoneda
  • Remark 3.3
  • Proposition 3.4
  • Remark 3.5
  • Theorem 3.6
  • Definition 4.1: Left action jk01
  • Example 4.2: $\mathop{\mathrm{\mathbf{PSh}}}\nolimits \mathbb{F}\xspace$
  • Example 4.4: $\mathop{\mathrm{\mathbf{PSh}}}\nolimits \mathbb{F}\xspace$
  • Definition 4.5: Well-behaved functor
  • Example 4.6: Well-behaved functors
  • ...and 61 more