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.

翻译：初始语义旨在对归纳结构及其性质进行建模，并为这些结构提供保持性质的递归原理。一个典型的例子是列表的折叠算子。我们关注的是为具有变量绑定及其替换结构的语言提供初始语义，并给出替换安全的递归原理。根据上下文和自由变量的表示方式不同，实现具有变量绑定的语言存在多种方法，例如无作用域语法、使用有限或无限上下文的有作用域语法等。抽象来看，每种方法对应选择不同的幺半范畴来对上下文和绑定进行建模，而每种选择又会为相同的抽象规范（或称"签名"）产生不同的"模型"概念。在本工作中，我们提供了工具来比较和关联从同一签名出发因选择不同幺半范畴而得到的模型。其关键在于我们证明了当以建模上下文的幺半范畴为参数时，初始语义自然具有2-范畴结构。因此，只要幺半范畴本身存在关联，我们就能关联从不同幺半范畴选择中获得的模型。特别地，我们利用上述结果关联了不同实现方式（德布鲁因索引与局部无名表示、有限上下文与无限上下文）的模型，并为简单类型化语法提供了泛化的递归原理。