Correspondence between Composite Theories and Distributive Laws
Aloïs Rosset, Maaike Zwart, Helle Hvid Hansen, Jörg Endrullis
TL;DR
The paper establishes a constructive, general bridge between composite theories and distributive laws for finitary Set-monads, clarifying when and how two theories can be composed into a single theory. It develops a separation procedure based on a functorial rewriting system to transform composite terms into TS-separated forms, enabling an explicit construction of the distributive law $\lambda: ST \Rightarrow TS$ from a composite theory, and conversely builds a composite theory from a given distributive law. A key contribution is identifying a minimal, potentially terminating subset $E' \subseteq E_\lambda$ of interaction equations that, together with $E_\mathbb{S}$ and $E_\mathbb{T}$, axiomatizes the composite theory $\mathbb{U}$; termination criteria (SN) guarantee this sufficiency, and a layered-axiom criterion provides practical termination guarantees. The paper also discusses limitations via counterexamples where $E'$ is not sufficient or does not terminate, and applies the framework to concrete presentations (e.g., rings and related monad compositions), offering tools for obtaining elegant, compact presentations of composite monads. It also points toward extensions to weak distributive laws, and outlines future work on broader termination criteria and automated reasoning aspects.
Abstract
Composite theories are the algebraic equivalent of distributive laws. In this paper, we delve into the details of this correspondence and concretely show how to construct a composite theory from a distributive law and vice versa. Using term rewriting methods, we also describe when a minimal set of equations axiomatises the composite theory.