2-Functoriality of Initial Semantics, and Applications
Benedikt Ahrens, Ambroise Lafont, Thomas Lamiaux
TL;DR
The paper develops a $2$-categorical framework for initial semantics that is parametrized by the base monoidal category modeling contexts, enabling systematic comparison of models arising from different representations of variable binding (e.g., unscoped, well-scoped with finite/infinite contexts, De Bruijn). It introduces a 2-category of module signatures and proves that the category of models is obtained via a $2$-functor from this category, allowing the lifting of adjunctions, coreflections, and equivalences along base-category relations. This machinery recovers and generalizes known results relating Fiore’s [F,set] and [Set,set], as well as De Bruijn models, by showing coreflections/equivalences lift to models and by deriving a generalized recursion principle for simply-typed languages through Grothendieck constructions. The framework enables translations between languages across different type systems (e.g., PCF to untyped lambda calculus) and yields a unified perspective on initiality across context representations. Overall, the approach scales to more complex languages and polymorphic systems, offering a robust method to relate syntax with binding across diverse semantic foundations.
Abstract
Initial semantics aims to model inductive structures and their properties, and to provide them with recursion principles respecting these properties. An ubiquitous example is the fold operator for lists. We are concerned with initial semantics that model languages with variable binding and their substitution structure, and that provide substitution-safe recursion principles. There are different approaches to implementing languages with variable binding depending on the choice of representation for contexts and free variables, such as unscoped syntax, or well-scoped syntax with finite or infinite contexts. Abstractly, each approach corresponds to choosing a different monoidal category to model contexts and binding, each choice yielding a different notion of "model" for the same abstract specification (or "signature"). In this work, we provide tools to compare and relate the models obtained from a signature for different choices of monoidal category. We do so by showing that initial semantics naturally has a 2-categorical structure when parametrized by the monoidal category modeling contexts. We thus can relate models obtained from different choices of monoidal categories provided the monoidal categories themselves are related. In particular, we use our results to relate the models of the different implementation -- de Bruijn vs locally nameless, finite vs infinite contexts -- , and to provide a generalized recursion principle for simply-typed syntax.