<Reference List> | |
Type: | Preprint |
National /International: | International |
Title: | Unraveling the iterative CHAD |
Publication Date: | 2025-05-20 |
Authors: |
- Fernando Lucatelli Nunes
- Gordon Plotkin - Matthijs Vákár |
Abstract: | Combinatory Homomorphic Automatic Differentiation (CHAD) was originally formulated as a semantics-driven source transformation for reverse-mode AD in total (terminating) programming languages. We extend this framework to partial languages with features like partial (potentially non-terminating) operations, data-dependent conditionals (e.g. real-valued tests), and iteration constructs (e.g. while-loops), while preserving the structure-preserving semantics principle of CHAD. A key contribution is the introduction of iteration-extensive indexed categories, which allow us to incorporate iteration into the target language's Grothendieck construction in a principled way - by requiring that the iteration construct in the base category lift to parameterized initial algebras in the indexed category. This yields a fibred iterative structure that cleanly models while-loops/iteration constructs in the categorical semantics. As a result, the extended CHAD transformation can still be described as the unique structure-preserving functor (an iterative Freyd category morphism) from the freely generated (iterative distributive) Freyd categorical structure on the source language to the (Grothendieck construction of the) syntactic semantics of the target language, mapping each primitive operation to its derivative. We establish the correctness of this extended transformation via the universal property of the syntactic categorical semantics of the source language, a categorical logical-relations-like argument, showing that the differentiated programs indeed compute proper reverse-mode derivatives of the originals. In summary, our work sheds light to the study of iteration constructs in dependently typed languages visa the study of iteration in Grothendieck constructions. As our main motivation and application, we bridge category theory and differentiable programming by generalizing CHAD to languages with data types, partial features, and while-loops, providing the first rigorous categorical semantics for reverse-mode CHAD in such settings and guaranteeing the correctness of the source-to-source CHAD technique. |
Institution: | DMUC 25-20 |
Online version: | http://www.mat.uc.pt...prints/eng_2025.html |
Download: | Not available |