A Language for Evaluating Derivatives of Functionals Using Automatic Differentiation
Pietro Di Gianantonio, Abbas Edalat, Ran Gutin
TL;DR
This work addresses the challenge of differentiating a broad class of functionals, including higher-order and Lipschitz-but-non-differentiable maps, within a rigorous computational setting. It introduces Dual PCF, a functional language that combines forward-mode automatic differentiation via dual numbers with a domain-theoretic directional derivative defined on Hausdorff topological vector spaces, supported by a denotational-operational adequacy framework. Key contributions include a sound and complete semantics for differentiating functionals, a domain-theoretic generalization of Lebourg/Clarke derivatives, and definability results showing that all computable linear functionals on function spaces are expressible in Dual PCF, along with extensive examples (IVP solving, Lagrangian functionals, and more). The approach enables exact real-number computation and rigorous derivative evaluation of functionals, with potential impact on calculus of variations, optimal control, and quantum-chemical modeling, and lays groundwork for practical implementations and extensions to nested differentiation.
Abstract
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.