论文标题
使用自动差异化评估功能导数的语言
A Language for Evaluating Derivatives of Functionals Using Automatic Differentiation
论文作者
论文摘要
我们提出了一种简单的功能编程语言，称为双PCF，该语言在精确的实际数量计算框架中使用双重数字实现前向模式自动差异化。该语言的主要新功能是能够正确评估用户以简单而直接的方式指定的精度 - 功能和一阶函数的定向导数。与其他可比较的语言相反，双PCF还包括用于定义功能和功能的递归操作员。我们提供了可以在双PCF中定义的Lipschitz函数和功能的广泛示例。我们使用域理论既可以为语言提供典型的语义，又可以使用逻辑关系证明新的衍生算子的正确性。 To be able to differentiate functionals -- including on function spaces equipped with their compact-open topology that do not admit a norm -- we develop a domain-theoretic directional derivative that is Scott continuous and extends Clarke's subgradient of real-valued locally Lipschitz maps on Banach spaces to real-valued continuous maps on Hausdorff topological vector spaces.最后，我们表明我们可以在双PCF中表达任意可计算的线性函数。
We present a simple functional programming language, called Dual PCF, that implements forward mode automatic differentiation using dual numbers in the framework of exact real number computation. The main new feature of this language is the ability to evaluate correctly up to the precision specified by the user -- in a simple and direct way -- the directional derivative of functionals as well as first order functions. In contrast to other comparable languages, Dual PCF also includes the recursive operator for defining functions and functionals. We provide a wide range of examples of Lipschitz functions and functionals that can be defined in Dual PCF. We use domain theory both to give a denotational semantics to the language and to prove the correctness of the new derivative operator using logical relations. To be able to differentiate functionals -- including on function spaces equipped with their compact-open topology that do not admit a norm -- we develop a domain-theoretic directional derivative that is Scott continuous and extends Clarke's subgradient of real-valued locally Lipschitz maps on Banach spaces to real-valued continuous maps on Hausdorff topological vector spaces. Finally, we show that we can express arbitrary computable linear functionals in Dual PCF.
