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 函数与泛函示例。通过域理论，我们为该语言赋予指称语义，并利用逻辑关系证明新导数算子的正确性。为能对泛函（包括定义在无范数的紧开拓扑函数空间上的泛函）进行微分，我们发展了一种 Scott 连续的域理论方向导数，该导数将 Banach 空间上实值局部 Lipschitz 映射的 Clarke 次梯度推广到 Hausdorff 拓扑向量空间上的实值连续映射。最后，我们证明可在 Dual PCF 中表达任意可计算线性泛函。