Unraveling the iterative CHAD
TL;DR
This work extends CHAD to programs with partial operations, data-dependent conditionals, and while-loops, preserving its defining principle of structure-preserving semantics and introduces iteration-extensive indexed categories, which integrate iteration into dependently typed programming languages.
Abstract
Combinatory Homomorphic Automatic Differentiation (CHAD) was originally formulated as a semantics-driven source-to-source transformation for reverse-mode automatic differentiation of total functional programs. We extend CHAD to programs with partial operations, data-dependent conditionals, and while-loops, preserving its defining principle of structure-preserving semantics. Our main contribution is the introduction of iteration-extensive indexed categories, which integrate iteration into dependently typed programming languages. Iteration in the base category lifts to parameterized initial algebras in the indexed category, yielding fibred iteration on the op-Grothendieck construction. Its total category is the category of containers associated with the dependently typed target language. This framework characterizes iterative CHAD as the unique iterative Freyd category morphism from the source language's syntactic category to the target language's category of containers that maps each primitive operation to its transposed derivative. Using the universal property of the syntactic model, we prove that the transformed programs compute the reverse-mode derivatives of the original programs. The resulting theory connects fixpoint operators in indexed categories with a structure-preserving construction and correctness proof for iterative CHAD.
