论文标题
用于高阶反向模式自动差异的差分形式回调编程语言
A Differential-form Pullback Programming Language for Higher-order Reverse-mode Automatic Differentiation
论文作者
论文摘要
在观察到反向模式自动分化（AD）的基础上，反向传播的概括可以自然表示为差异1形式的回溯，我们设计了一种具有一流的差分运算符的简单高阶编程语言，并提供了一个还原策略，并呈现一个精确模拟反向模式广告的降低策略。我们通过在满足Hahn-Banach分离定理的任何差分$λ$类别中解释我们的语言来证明我们的还原策略是合理的，并表明还原策略精确地捕获了在真正的高阶设置中捕获反向模式广告。
Building on the observation that reverse-mode automatic differentiation (AD) -- a generalisation of backpropagation -- can naturally be expressed as pullbacks of differential 1-forms, we design a simple higher-order programming language with a first-class differential operator, and present a reduction strategy which exactly simulates reverse-mode AD. We justify our reduction strategy by interpreting our language in any differential $λ$-category that satisfies the Hahn-Banach Separation Theorem, and show that the reduction strategy precisely captures reverse-mode AD in a truly higher-order setting.
