Freely generated categorical structures and automatic differentiation

Abstract

Automatic differentiation (AD) transforms programs into programs that compute derivatives and is a central tool in scientific computing, machine learning and optimisation. Extending AD to expressive programming languages raises a fundamental question: how can differentiation accommodate higher-order functions, rich data types and partial computation while remaining compositional and correct? This thesis addresses that question through categorical semantics, developing both concrete program transformations and mathematical foundations of independent interest. The central approach treats programming languages, modulo their equations, as freely generated categorical structures. AD is then specified as a homomorphic transformation determined by its action on primitive operations. Universal properties organise the construction, while categorical logical relations establish that the transformed programs compute the derivatives prescribed by the semantics. This yields a systematic connection between the structure of a language, the design of its differentiation transformation and its correctness proof. We develop this approach in three settings. First, we give forward- and reverse-mode dual-numbers AD for ML-family languages with recursive types, term recursion and partial operations, together with a reusable logical-relations framework for proving correctness. Second, we develop Combinatory Homomorphic Automatic Differentiation (CHAD) for expressive total languages with products, sums, inductive and coinductive types, and higher-order functions. Extensive indexed categories provide the semantic structure needed to handle sums compositionally. Third, Iterative CHAD extends the reverse-mode construction to first-order languages with general iteration and partial operations. Iteration-extensive indexed categories and iterative folders account for loops in the semantics and target language, supporting a correctness theorem that includes preservation of the domain of definition. The categorical questions arising from these transformations lead to a second group of contributions. We introduce doubly-infinitary distributive categories, capturing distributivity of small products over small coproducts, and prove that the freely generated such categories are cartesian closed. Studying pseudodistributive laws between free completions extends this account to extensive categories, including cartesian closedness of free doubly-infinitary lextensive categories. We also investigate how structure lifts through Grothendieck constructions. Left Kan extensivity provides conditions for constructing colimits, while a Dialectica-inspired account yields sufficient conditions for monoidal closure of the total category. These results connect abstract semantics with practical methods for building reliable program transformations. The CHAD account developed here formed part of the foundation for subsequent efficient implementation work. At the same time, implementation-driven questions led to new results on freeness, extensivity and categorical closure. The thesis thus demonstrates how semantic principles can guide the construction of useful transformations with explicit correctness guarantees, while practical demands stimulate advances in their mathematical foundations.