An excursion into Dialectica and Differentiation

TL;DR

This paper explores the deep connection between Gödel's Dialectica interpretation and differentiation, using a program-theoretic and geometric approach to clarify their relationship and limitations.

Contribution

It establishes a logical relation between Dialectica transformation and reverse differential within differential categories, framing Dialectica as a differentiable program transformation.

Findings

Dialectica can be modeled as a differentiable program transformation

A logical relation between Dialectica and reverse differential is established

The limits of the Dialectica-differentiation correspondence are clarified

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.