A language for evaluating derivatives of functionals using automatic differentiation

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.