一句话：证明以 monoidal 范畴为参数的初始语义具有 2-范畴结构，并据此关联不同变量绑定表示下的模型。
初始语义为归纳结构及其性质提供递归原理，但对带变量绑定与替换的语言，不同上下文与自由变量表示（如 unscoped、well-scoped、de Bruijn、locally nameless、有限或无限上下文）对应不同的 monoidal 范畴，从而对同一签名给出不同模型，难以比较。本文证明：以 monoidal 范畴为参数的初始语义自然具有 2-范畴结构；当这些范畴之间存在关系时，可诱导相应初始模型之间的关系。作者据此关联 de Bruijn 与 locally nameless、有限与无限上下文等实现所得到的模型，并给出 simply-typed 语法的广义递归原理。
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.
@article{paperbot3042,
title = {2-Functoriality of Initial Semantics, and Applications},
author = {Benedikt Ahrens and Ambroise Lafont and Thomas Lamiaux},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {ICFP},
year = {2025},
doi = {10.1145/3747527}
}