An excursion into Dialectica and Differentiation

Abstract

G\"odel's Dialectica has been introduced and developed in the tradition of the so-called functional interpretations. Only recently has it been related with the a priori unrelated notion of differentiation, by taking a program-theoretic approach. We revisit the deep connection between these two notions in order to understand its structural reasons, as well as to express it in an arguably more natural way by following a geometric intuition. More specifically, we give a logical relation between a Dialectica transformed term and its reverse differential in a differential category and, then, we phrase the Dialectica program transformation in the language of lenses, often used indeed in Automatic Differentiation in order to model reverse differentiation. We illustrate how this clarifies why Dialectica behaves as a differentiable program transformation, and what the limits of this correspondence are.