Unraveling the iterative CHAD

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.

Programming Languages (cs.PL); Artificial Intelligence (cs.AI); Machine Learning (cs.LG); Category Theory (math.CT); Logic (math.LO)

F.3.2; F.3.3; D.3.1; D.3.2; D.2.4; G.4; I.2.3; I.2.6; G.1.10

arXiv:2505.15002 [cs.PL]

(or arXiv:2505.15002v3 [cs.PL] for this version)

https://doi.org/10.48550/arXiv.2505.15002 Focus to learn more arXiv-issued DOI via DataCite

arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.

Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.

Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.