论文标题
较高类型的反向广告：纯，原则性和代表性正确
Reverse AD at Higher Types: Pure, Principled and Denotationally Correct
论文作者
论文摘要
我们展示了如何定义前向模式和反向模式自动分化源代码转换或标准的高阶功能语言。转换产生了纯粹的功能代码，并且它们的定义是由分类通用属性产生的。我们给出了转换正确性的语义证明。在最优雅的配方中，转换生成了线性类型的代码。但是，我们演示了如何在不牺牲正确性的情况下以标准功能语言实施转换。为此，我们利用抽象数据类型来表示所需的线性类型，例如通过使用基本模块系统。
We show how to define forward- and reverse-mode automatic differentiation source-code transformations or on a standard higher-order functional language. The transformations generate purely functional code, and they are principled in the sense that their definition arises from a categorical universal property. We give a semantic proof of correctness of the transformations. In their most elegant formulation, the transformations generate code with linear types. However, we demonstrate how the transformations can be implemented in a standard functional language without sacrificing correctness. To do so, we make use of abstract data types to represent the required linear types, e.g. through the use of a basic module system.
