Autodiff refers to the core of the automatic differentiation systems developed in projects like JAX and Dex. Autodiff has recently been formalised in a linear typed calculus by Radul et al in arXiv:2204.10923. Although this formalisation suffices to express the main program transformations of Autodiff, the calculus is very specific to this task, and it is not clear whether the type system yields a substructural logic that has interest on its own. We propose an encoding of Autodiff into a linear $\lambda$-calculus that enjoys a Curry-Howard correspondence with Girard's linear logic. We prove that the encoding is sound both qualitatively (the encoded terms are extensionally equivalent to the original ones) and quantitatively (the encoding preserves the original work cost as described in arXiv:2204.10923). As a byproduct, we show that unzipping, one of the transformations used to implement backpropagation in Autodiff, is, in fact, optional.

翻译：自动微分（Autodiff）是JAX和Dex等项目中开发的自微分系统的核心。Radul等人近期在arXiv:2204.10923中通过线性类型演算对自动微分进行了形式化。尽管该形式化足以表达自动微分的主要程序变换，但该演算高度特化于此任务，且其类型系统是否能产生具有独立研究价值的子结构逻辑尚不明确。我们提出将自动微分编码至一个线性$\lambda$-演算中，该演算与Girard的线性逻辑满足Curry-Howard对应关系。我们证明了该编码在定性（编码项与原始项外延等价）和定量（编码保持arXiv:2204.10923中描述的原始计算代价）上均是可靠的。作为推论，我们表明实现自动微分反向传播的变换之一——解压缩（unzipping）实际上是非必需的。