A Unified Framework for Initial Semantics

Initial semantics aims to capture inductive structures and their properties as initial objects in suitable categories. We focus on the initial semantics aiming to model the syntax and substitution structure of programming languages with variable binding as initial objects. Three distinct yet similar approaches to initial semantics have been proposed. An initial semantics result was first proved by Fiore, Plotkin, and Turi using Σ-monoids in their seminal paper published at LICS'99. Alternative frameworks were later introduced by Hirschowitz and Maggesi using modules over monads, and by Matthes and Uustalu using heterogeneous substitution systems. Since then, all approaches have been significantly developed by numerous researchers. While similar, the links between this different approaches remain unclear. This is especially the case as the literature is difficult to access, since it was mostly published in (short) conference papers without proofs, and contains many technical variations and evolutions. In this work, we introduce a framework based on monoidal categories that unifies these three distinct approaches to initial semantics, by suitably generalizing and combining them. Doing so we show that modules over monoids provide an abstract and easy to manipulate framework, that Σ-monoids and strengths naturally arise when stating and proving an initiality theorem, and that heterogeneous substitution systems enable us to prove the initiality theorem modularly. Moreover, to clarify the literature, we provide an extensive overview of related work using our framework as a cornerstone to explain the links between the different approaches and their variations.