Denotational Correctness of Forward-Mode Automatic Differentiation for Iteration and Recursion
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2020
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910459280490496 |
|---|---|
| author | Vákár, Matthijs |
| author_facet | Vákár, Matthijs |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2007_05282 |
| institution | arXiv |
| publishDate | 2020 |
| record_format | arxiv |
| spellingShingle | Denotational Correctness of Forward-Mode Automatic Differentiation for Iteration and Recursion Vákár, Matthijs Programming Languages 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. |
| title | Denotational Correctness of Forward-Mode Automatic Differentiation for Iteration and Recursion |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2007.05282 |