Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Denotational Correctness of Forward-Mode Automatic Differentiation for Iteration and Recursion

Matthijs Vákár

TL;DR

The paper provides a rigorous semantic foundation for forward- mode automatic differentiation in expressive languages that feature partial constructs, iteration, and recursion. It defines a forward- mode AD macro $\overrightarrow{\mathcal{D}}$ and proves its correctness using a denotational semantics in $\mathbf{Diff}$ augmented with a partiality monad, supplemented by a semantic logical-relations argument via subsconing. To handle recursion, the authors introduce $\omega$-diffeological spaces ($\mathbf{\omega Diff}$) and bilimit-compact expansions, enabling a coherent treatment of both differentiation and recursion; forward AD correctness extends from first- order types to recursive types through $\omega$-ds- based logical relations. The approach yields a canonical, adequacy- grounded semantics aligning with operational semantics and offers a principled path toward robust AD integration in real-world functional languages with recursion and higher- order features. Overall, the work advances the mathematical understanding of AD in partial and recursive language features and lays groundwork for future reverse- mode extensions and practical differentiable programming foundations.

Abstract

We present semantic correctness proofs of forward-mode Automatic Differentiation (AD) for languages with sources of partiality such as partial operations, lazy conditionals on real parameters, iteration, and term and type recursion. We first define an AD macro on a standard call-by-value language with some primitive operations for smooth partial functions and constructs for real conditionals and iteration, as a unique structure preserving macro determined by its action on the primitive operations. We define a semantics for the language in terms of diffeological spaces, where the key idea is to make use of a suitable partiality monad. A semantic logical relations argument, constructed through a subsconing construction over diffeological spaces, yields a correctness proof of the defined AD macro. A key insight is that, to reason about differentiation at sum types, we work with relations which form sheaves. Next, we extend our language with term and type recursion. To model this in our semantics, we introduce a new notion of space, suitable for modeling both recursion and differentiation, by equipping a diffeological space with a compatible $ω$cpo-structure. We demonstrate that our whole development extends to this setting. By making use of a semantic, rather than syntactic, logical relations argument, we circumvent the usual technicalities of logical relations techniques for type recursion.

Denotational Correctness of Forward-Mode Automatic Differentiation for Iteration and Recursion

TL;DR

The paper provides a rigorous semantic foundation for forward- mode automatic differentiation in expressive languages that feature partial constructs, iteration, and recursion. It defines a forward- mode AD macro and proves its correctness using a denotational semantics in augmented with a partiality monad, supplemented by a semantic logical-relations argument via subsconing. To handle recursion, the authors introduce -diffeological spaces () and bilimit-compact expansions, enabling a coherent treatment of both differentiation and recursion; forward AD correctness extends from first- order types to recursive types through -ds- based logical relations. The approach yields a canonical, adequacy- grounded semantics aligning with operational semantics and offers a principled path toward robust AD integration in real-world functional languages with recursion and higher- order features. Overall, the work advances the mathematical understanding of AD in partial and recursive language features and lays groundwork for future reverse- mode extensions and practical differentiable programming foundations.

Abstract

We present semantic correctness proofs of forward-mode Automatic Differentiation (AD) for languages with sources of partiality such as partial operations, lazy conditionals on real parameters, iteration, and term and type recursion. We first define an AD macro on a standard call-by-value language with some primitive operations for smooth partial functions and constructs for real conditionals and iteration, as a unique structure preserving macro determined by its action on the primitive operations. We define a semantics for the language in terms of diffeological spaces, where the key idea is to make use of a suitable partiality monad. A semantic logical relations argument, constructed through a subsconing construction over diffeological spaces, yields a correctness proof of the defined AD macro. A key insight is that, to reason about differentiation at sum types, we work with relations which form sheaves. Next, we extend our language with term and type recursion. To model this in our semantics, we introduce a new notion of space, suitable for modeling both recursion and differentiation, by equipping a diffeological space with a compatible cpo-structure. We demonstrate that our whole development extends to this setting. By making use of a semantic, rather than syntactic, logical relations argument, we circumvent the usual technicalities of logical relations techniques for type recursion.

Paper Structure

This paper contains 32 sections, 25 theorems, 48 equations, 6 figures.

Table of Contents

  1. Introduction
  2. Key Ideas
  3. An AD translation for Iteration and Real Conditionals
  4. A simple call-by-value language
  5. A translation for forward-mode Automatic Differentiation
  6. Equational theory
  7. A denotational semantics via diffeological spaces
  8. Preliminaries
  9. Partiality in $\mathbf{Diff}$
  10. Logical Relations and Correct AD for Iteration
  11. Preliminaries
  12. Subsconing for correctness of AD
  13. Correctness of Forward AD
  14. Correctness of forward AD at first-order types
  15. Preliminaries
  16. ...and 17 more sections

Key Result

Theorem 1

For any ${ x}_1:{ \tau}_1,\ldots,{ x}_n:{ \tau}_n\vdash^c{ t}:{ \sigma}$, where ${ \tau}_i,{ \sigma}$ are first-order types, we have that $\llbracket \hbox{$\overrightarrow{\mathcal{D}}$}_{}{}_{\mathcal{C}}({ t})\rrbracket(x, v)=(\llbracket { t}\rrbracket(x), \mathcal{T}^{}_{x}\llbracket { t}\rrbrac

Figures (6)

  • Figure 1: Typing rules for the our fine-grain CBV language with iteration and real conditionals. We use a typing judgement $\vdash^v$ for values and $\vdash^c$ for computations.
  • Figure 2: A forward-mode AD macro defined on types as $\hbox{$\overrightarrow{\mathcal{D}}$}_{}(-)$, values as $\hbox{$\overrightarrow{\mathcal{D}}$}_{}{}_{\mathcal{V}}(-)$, and computations as $\hbox{$\overrightarrow{\mathcal{D}}$}_{}{}_{\mathcal{C}}(-)$. All newly introduced variables are chosen to be fresh. We single out the rule for primitive operations $\mathrm op$, as this is where the interesting work specific to differentiation happens.
  • Figure 3: Standard $\beta\eta$-laws for fine-grain CBV. We write $\stackrel{\# { x}_1,\ldots,{ x}_n}{=}$ to indicate that the variables are fresh in the left hand side. In the top right rule, ${ x}$ may not be free in ${ r}$. Equations hold on pairs of terms of the same type.
  • Figure 4: Typing rules for term and type recursion. As usual, we treat $\mu\alpha.$ as a type level variable binder.
  • Figure 5: Standard $\beta\eta$-laws for recursive types (which imply rules for term recursion and iteration.).
  • ...and 1 more figures

Theorems & Definitions (33)

  • Theorem : Correctness of Fwd AD, Thm. \ref{['thm:fwd-cor-full']}
  • Definition
  • lemma 1: Functorial macro
  • definition 1
  • definition 2
  • proposition 1
  • proposition 2
  • proposition 3
  • lemma 2
  • proposition 4
  • ...and 23 more