A Language for Evaluating Derivatives of Functionals Using Automatic Differentiation

TL;DR

This paper introduces Dual PCF, a functional programming language that implements forward mode automatic differentiation for functionals and functions, supporting recursive definitions and exact real number computations.

Contribution

The paper develops Dual PCF, a language with recursive operators and a domain-theoretic derivative, enabling differentiation of complex functionals on topological vector spaces.

Findings

Correctly evaluates directional derivatives up to user-specified precision

Defines a domain-theoretic directional derivative extending Clarke's subgradient

Expresses arbitrary computable linear functionals in Dual PCF

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.