Category of nominal sets has strong local monoidal closed property
The category of nominal sets is locally monoidal closed
Logic in Computer Science
Summary
The paper studies a mathematical setting called nominal sets, useful for modeling syntax with variables. It was already known that each slice category of nominal sets is cartesian-closed, meaning functions behave nicely with context. The authors discovered a stronger property: any monoidal closed structure on nominal sets also applies to all its slices. This advances understanding of how complex structures behave under variable binding and composition in this setting.
What this means in practice
- •For programming language designers: Use stronger local monoidal closed properties of nominal sets to model complex variable-binding constructs more precisely in language semantics.
- •For formal verification engineers: Improve the semantic frameworks for systems with variable binding by applying the newly proven local monoidal structures in nominal sets.
A theory result. No direct application yet.
Authors
Fahimeh Bayeh, Peng Fu, Peter Selinger
Abstract
The category Nom of nominal sets was proposed by Pitts and Gabbay as a setting for the semantics of abstract syntax with variable bindings. It is well-known that Nom is a topos, also known as the Schanuel topos, and in particular it follows that Nom is locally closed, i.e., every slice category Nom/X is cartesian-closed. In this paper, we show that Nom has a much stronger property: every monoidal (closed) structure on Nom induces a monoidal (closed) structure on all slice categories Nom/X. One monoidal closed structure of particular interest on Nom is the separated product A * B, whose right adjoint A -* B is called the separated function space. In particular, it follows that Nom is locally separatedly closed.