We show how the basic Combinatory Homomorphic Automatic Differentiation (CHAD) algorithm can be optimised, using well-known methods, to yield a simple, composable, and generally applicable reverse-mode automatic differentiation (AD) technique that has the correct computational complexity that we would expect of reverse-mode AD. Specifically, we show that the standard optimisations of sparse vectors and state-passing style code (as well as defunctionalisation/closure conversion, for higher-order languages) give us a purely functional algorithm that is most of the way to the correct complexity, with (functional) mutable updates taking care of the final log-factors. We provide an Agda formalisation of our complexity proof. Finally, we discuss how the techniques apply to differentiating parallel functional array programs: the key observations are 1) that all required mutability is (commutative, associative) accumulation, which lets us preserve task-parallelism and 2) that we can write down data-parallel derivatives for most data-parallel array primitives.

翻译：我们展示了如何利用众所周知的方法优化基本组合同态自动微分（CHAD）算法，从而得到一种简单、可组合且广泛适用的反向模式自动微分（AD）技术，该技术具有与反向模式AD预期相符的正确计算复杂度。具体而言，我们证明了稀疏向量和状态传递风格代码（对于高阶语言还包括反函数化/闭包转换）的标准优化，可以生成一个纯函数式算法，该算法在大多数方面已达到正确复杂度，而（函数式）可变更新则负责解决最终的log因子问题。我们提供了Agda形式化验证的复杂度证明。最后，我们讨论了这些技术如何应用于并行函数式数组程序的微分：关键观察在于1）所有必需的可变性都是（交换、结合）累加性操作，这使我们能够保留任务并行性；2）对于大多数数据并行数组原语，我们可以写出其数据并行导数。