高阶函数的高阶自动微分
Higher Order Automatic Differentiation of Higher Order Functions
AI总结：
本文为高阶函数语言中的前向模式自动微分提供了基于微分学空间的语义正确性证明，通过粘合构造和逻辑关系论证，并扩展到高阶导数计算。
摘要：
我们给出了自动微分（AD）的语义正确性证明。我们考虑了一种在具有代数数据类型的高阶语言上的前向模式AD方法，并将其刻画为在给定基本运算导数选择的情况下唯一的结构保持宏。我们描述了一种基于微分学空间的丰富可微编程语义。我们展示了该语义解释我们的语言，并阐述了AD方法相对于该语义正确意味着什么。我们展示了我们的AD刻画如何通过微分学空间上的粘合构造产生一个优雅的语义正确性证明。我们解释了这本质上是一个逻辑关系论证。在整个过程中，我们展示了分析如何扩展到使用泰勒近似计算高阶导数的AD方法。
英文摘要：
We present semantic correctness proofs of automatic differentiation (AD). We consider a forward-mode AD method on a higher order language with algebraic data types, and we characterise it as the unique structure preserving macro given a choice of derivatives for basic operations. We describe a rich semantics for differentiable programming, based on diffeological spaces. We show that it interprets our language, and we phrase what it means for the AD method to be correct with respect to this semantics. We show that our characterisation of AD gives rise to an elegant semantic proof of its correctness based on a gluing construction on diffeological spaces. We explain how this is, in essence, a logical relations argument. Throughout, we show how the analysis extends to AD methods for computing higher order derivatives using a Taylor approximation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
