An Introduction to Different Approaches to Initial Semantics

TL;DR

The paper addresses the fragmentation of approaches to initial semantics for languages with variable binding, notably Fiore–Plotkin–Turi's monoidal-category framework, Hirschowitz–Maggesi's modules over monads, and Matthes–Uustalu's Mendler-style recursion. It proposes a unified introduction that merges Hirschowitz–Maggesi with Fiore's framework via a pushout construction and leverages Matthes and Uustalu's formalism to obtain modular proofs, generalizing to the setting of monoidal categories. The authors present a generalized framework for initial semantics, including fully worked examples of $Set$-based models and $F$-$Set$, $Set^T$-$Set^T$ constructions, and discuss the connections between the three strands of work. The work aims to make the initial semantics literature more accessible, enabling modular proofs and providing a foundation for further unification of these categorical approaches.

Abstract

Characterizing programming languages with variable binding as initial objects, was first achieved by Fiore, Plotkin, and Turi in their seminal paper published at LICS'99. To do so, in particular to prove initiality theorems, they developed a framework based on monoidal categories, functors with strengths, and $Σ$-monoids. An alternative approach using modules over monads was later introduced by Hirschowitz and Maggesi, for endofunctor categories, that is, for particular monoidal categories. This approach has the advantage of providing a more general and abstract definition of signatures and models; however, no general initiality result is known for this notion of signature. Furthermore, Matthes and Uustalu provided a categorical formalism for constructing (initial) monads via Mendler-style recursion, that can also be used for initial semantics. The different approaches have been developed further in several articles. However, in practice, the literature is difficult to access, and links between the different strands of work remain underexplored. In the present work, we give an introduction to initial semantics that encompasses the three different strands. We develop a suitable "pushout" of Hirschowitz and Maggesi's framework with Fiore's, and rely on Matthes and Uustalu's formalism to provide modular proofs. For this purpose, we generalize both Hirschowitz and Maggesi's framework, and Matthes and Uustalu's formalism to the general setting of monoidal categories studied by Fiore and collaborators. Moreover, we provide fully worked out presentation of some basic instances of the literature, and an extensive discussion of related work explaining the links between the different approaches.