An excursion into Dialectica and Differentiation

TL;DR

This paper analyzes the link between Gödel's Dialectica and differentiation from a program- and geometry-inspired viewpoint. By embedding forward differentiation in Cartesian differential categories and leveraging lenses, it recasts Dialectica as a differentiable program transformation whose reverse-differential behavior arises from lens composition; it further shows that Dialectica factors through Euclidean lenses, providing a coherent categorical bridge between the two concepts. The work clarifies why Dialectica aligns with reverse differentiation at a structural level via $M^\bullet$ and $M_x$ and discusses limits and potential extensions to dependent types and richer reverse-differential frameworks. Overall, it offers a geometric, lens-based interpretation of the Dialectica transformation as a compositional mechanism for reverse-mode differentiation with implications for higher-order program transformation and automatic differentiation.

Abstract

Gödel'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.

Figures (12)

• Figure 1: The Dialectica program transformation for the $\mathrm{ST\lambda C}$ in $\mathbf{P}$.
• Figure 2: Definition \ref{['def:log_rels']} of relations $\sim$ and $\bowtie$, inductive case $B=E\to F$ (this is the only case).
• Figure 3: In $(\mathrm{eval})$, we let $\mathrm{eval}_{\vec{a}}:[{A_1}\to {[{A_2}\to {\cdots\to[{A_n}\to {B}]}]}]\to B$ be the composition $[1,n]\overset{d}{\to}[1,n]\overset{h_1}{\to}[2,n] \to \cdots \to [n,n]\overset{h_n}{\to} B$, where $[i,n]:=[{A_i}\to {[{A_{i+1}}\to {\cdots\to[{A_n}\to {B}]}]}]$ and $h_j:={ \left.\nulldelimiterspace 1_{A_j} \newline \right|_{{{a}^{!}}_{\!\!j}} }$.
• Figure 4: From relations in KerjeanPedrot24 (denoted $\overset{\partial\lambda}{\sim}$, $\overset{\partial\lambda}{\bowtie}$) to ours in Definition \ref{['def:log_rels']}, and vice versa. $S$ is a $\mathrm{ST\partial\lambda C}$-term. The careful reader would notice that, rigorously speaking, one needs to slightly modify the term $M$ when passing from the formulation in KerjeanPedrot24 to ours, because of the modifications mentioned at Figure \ref{['fig:dial']}. We leave it implicit since it is easy to recover by following Figure \ref{['fig:WC']}.
• Figure 5: Dialectica extracted realizers of this proof are not in a "function/differential" relation.

Theorems & Definitions (33)

• Definition 5
• Lemma 6
• proof
• Lemma 7
• theorem 8
• proof
• Corollary 9
• Remark 10
• Remark 11
• Proposition 12