Homomorphic Reverse Differentiation of Iteration
summary
Claims that CHAD applies to partial programs with iteration by moving CHAD into a categorical target (the free completion on the dual of Vect with ωCPO enrichment), gives a denotational semantics that composes and preserves correctness, and yields an implementation strategy supporting unbounded loops. Key facts: iteration is given by ωCPO structure, partially defined derivatives are modeled so that derivative is zero where undefined, and the construction is both universal (unique functor) and practical for efficient, compositional AD.
AI-written summary · about
related talks
19mEfficient CHAD
30mAutomatic Differentiation in PCF
19mTowards Denotational Semantics of AD for Higher-Order, Recursive, Probabilistic
36mProgramming Languages for Automatic Differentiation: What Now?
29mPartial Evaluation of Automatic Differentiation for Differential-Algebraic Equati...
14mNominal Semantics for First-class Automatic Differentiation
11mPerturbation confusion in forward automatic differentiation of higher-order functions
05mPartial Evaluation of Forward-Mode Automatic Differentiation