Contextual source code AD transformations for sum types
summary
Provides context-based source-code transformations that implement forward AD, reverse AD and transposition for a first-order language with products and sums, and proves the transforms form a commuting diagram so reverse = transpose ∘ forward on the source code. Targets a mixed linear/non-linear target with dependent types that represent sum-type tangent spaces; uses a "bunch" elimination and structural-recursive generation of code. Delivers runtime and space bounds and shows efficiency except for extra cost when deep case-branching forces large tuple accumulation. Dependent tangent types appear essential.
AI-written summary · about
chapters (15)
- 0:00Intro
- 1:26Our source code transformations
- 2:36Their advantages
- 3:19Efficiency
- 4:58Typing Environment Contexts
- 6:46Typing reverse differentiation (without sum types)
- 8:20Using contexts
- 11:02Target language
- 13:42Typing the linear language
- 16:12Type translation
- 17:09Forward differentiation translation
- 17:52Reverse differentiation translation
- 19:18Transposition translation
- 20:01Cases: forward differentiation
- 21:17Sums: Reverse differentiation
related talks
01h 21mNon-local compiler transformations in the presence of dynamic dispatch
25mYou Only Linearize Once: Tangents Transpose to Gradients
36mProgramming Languages for Automatic Differentiation: What Now?
56mOn Type-Based Techniques for Program Manipulation
23mEfficient Dual-Numbers Reverse AD via Well-Known Program Transformations
19mEfficient CHAD
29mStaging Automatic Differentiation with Fusion
27mProvably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic