We present a simple functional programming language, called Dual PCF, that implements forward mode automatic differentiation using dual numbers. The main new feature of this language is the ability to evaluate - in a simple and direct way - the directional derivative of 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 Scott 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 topological vector spaces. Finally, we show that we can express arbitrary computable linear functionals in Dual PCF.

翻译：我们提出了一种简单的函数式编程语言——Dual PCF，它利用对偶数实现前向模式自动微分。该语言的主要新特性在于能够以简单直接的方式计算泛函的方向导数。我们提供了大量可在Dual PCF中定义的Lipschitz函数与泛函示例。我们运用域论为该语言赋予指称语义，并通过逻辑关系证明新导数算子的正确性。为了能够对泛函（包括定义在Scott拓扑下、不承认范数的函数空间上的泛函）求导，我们发展了一种域论方向导数，该导数具有Scott连续性，并将Banach空间上实值局部Lipschitz映射的Clarke次梯度推广至拓扑向量空间上的实值连续映射。最后，我们证明可在Dual PCF中表达任意可计算线性泛函。