Programming language structures enable reliable automatic differentiation
Freely Generated Categorical Structures and Automatic Differentiation, PhD Thesis (Introduction and Conclusion)
Programming LanguagesLogic in Computer Science
Summary
The thesis looks at how programming languages can be understood as structures in mathematics called categories. By using these structures, the author studies ways to automatically compute derivatives of programs—important for things like machine learning—in a reliable and correct way. They focus on commonly used differentiation methods that work even for complex programs with functions inside functions and loops. The research connects deep theories in math with practical ways to transform and analyze computer programs.
What this means in practice
- •For software developers: Design program transformations that correctly implement automatic differentiation for complex functional languages.
- •For programming language designers: Develop programming languages with built-in support for efficient and mathematically sound differentiation techniques.
A theory result. No direct application yet.
Authors
Fernando Lucatelli Nunes
Abstract
This version contains the introduction and conclusion of my PhD thesis, "Freely Generated Categorical Structures and Automatic Differentiation", together with its English and Dutch summaries. The full thesis consists of an introductory chapter, six joint research papers, and a concluding chapter, developed during my PhD studies at Utrecht University under the supervision of Gabriele Keller and Matthijs Vákár. The research papers are available separately and are not reproduced here. The introduction presents the scope of the thesis, explains the contributions of the six papers and their connections, and introduces the categorical foundations of our approach. The guiding idea is that programming languages, viewed as freely generated categorical structures, provide a principled setting for constructing structure-preserving program transformations and proving their correctness. Automatic differentiation supplies the central application: we study forward- and reverse-mode differentiation for expressive typed languages, including higher-order functions, recursive types, iteration and partiality. The semantic requirements of these transformations also motivate independent mathematical results on free distributive and extensive categories, cartesian closedness, and Grothendieck constructions. The conclusion brings these contributions together, discusses their limitations, and outlines further directions. Throughout, the thesis develops a dialogue between theory and practice: categorical semantics guides the construction of reliable and practically useful program transformations, while the demands of computation lead to new categorical structures and results.