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.

翻译：本文提出一种名为Dual PCF的简单函数式编程语言，该语言在精确实数计算框架下利用对偶数实现了前向模式自动微分。该语言的主要新特性在于能够以简洁直接的方式，按用户指定的精度准确计算泛函及一阶函数的方向导数。与其他同类语言相比，Dual PCF还包含用于定义函数与泛函的递归算子。我们提供了大量可在Dual PCF中定义的Lipschitz函数与泛函示例。本文运用域论为该语言建立指称语义，并通过逻辑关系证明了新导数算子的正确性。为能对泛函求导（包括在具有紧致-开拓扑、无需范数的函数空间上），我们发展了一种斯科特连续且将Banach空间上实值局部Lipschitz映射的Clarke次梯度推广至Hausdorff拓扑向量空间上实值连续映射的域论方向导数。最后，我们证明Dual PCF可表达任意可计算线性泛函。