∂ is for Dialectica: Typing Differentiable Programming - Université Sorbonne Paris Nord Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2021

∂ is for Dialectica: Typing Differentiable Programming

Résumé

Differentiable programming is a recent research area: its objective is to express differentiation as a modular algorithmic transformation on rich programming languages. It is in particular motivated by the various applications of automatic differentiation in machine learning or formal calculus. This work focuses on the typing system used to express differentiation. The first part of this paper is devoted to expressing the Dialectica transformation as a reverse automated differentiation transformation on a higher-order lambda-calculus with positive types. The second part builds on the intuitions provided by Dialectica to provide a lambda-calculus with an internal differentiation operator, with a typing system inspired by Differential Linear Logic, allowing to express backward automatic differentiation as a callby-name strategy and forward automatic differentiation as a call-by-value strategy. The target language of Dialectica is then given a semantics in smooth models of Differential Linear Logic.
Fichier principal
Vignette du fichier
main_hal_version.pdf (451.94 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03123968 , version 1 (28-01-2021)
hal-03123968 , version 2 (04-02-2021)
hal-03123968 , version 3 (24-01-2022)

Identifiants

  • HAL Id : hal-03123968 , version 1

Citer

Marie Kerjean, Pierre-Marie Pédrot. ∂ is for Dialectica: Typing Differentiable Programming. 2021. ⟨hal-03123968v1⟩
242 Consultations
794 Téléchargements

Partager

Gmail Facebook X LinkedIn More