
arXiv: 2503.10863
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.
Initial semantics, FOS: Computer and information sciences, Computer Science - Programming Languages, [INFO.INFO-CL] Computer Science [cs]/Computation and Language [cs.CL], FOS: Mathematics, Monoidal categories, Mathematics - Category Theory, Category Theory (math.CT), Substitution, Theory of computation→Categorical semantics, Variable binding, Programming Languages (cs.PL)
Initial semantics, FOS: Computer and information sciences, Computer Science - Programming Languages, [INFO.INFO-CL] Computer Science [cs]/Computation and Language [cs.CL], FOS: Mathematics, Monoidal categories, Mathematics - Category Theory, Category Theory (math.CT), Substitution, Theory of computation→Categorical semantics, Variable binding, Programming Languages (cs.PL)
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
