Reverse AD at higher types: pure, principled and denotationally correct

DOI10.1007/978-3-030-72019-3_22zbMATH Open1473.68058arXiv2007.05283OpenAlexW3148154580MaRDI QIDQ2233481FDOQ2233481

Matthijs Vákár

Publication date: 18 October 2021

Abstract: We show how to define forward- and reverse-mode automatic differentiation source-code transformations or on a standard higher-order functional language. The transformations generate purely functional code, and they are principled in the sense that their definition arises from a categorical universal property. We give a semantic proof of correctness of the transformations. In their most elegant formulation, the transformations generate code with linear types. However, we demonstrate how the transformations can be implemented in a standard functional language without sacrificing correctness. To do so, we make use of abstract data types to represent the required linear types, e.g. through the use of a basic module system.

Full work available at URL: https://arxiv.org/abs/2007.05283

Recommendations

• Functional differentiation of computer programs
• Functional differentiation of computer programs
• Beautiful differentiation
• scientific article; zbMATH DE number 992807
• Nesting forward-mode AD in a functional framework

zbMATH Keywords

semanticsprogram correctnessautomatic differentiation

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Numerical differentiation (65D25) Functional programming and lambda calculus (68N18) Abstract data types; algebraic specification (68Q65)

Cites Work

• Diffeology
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Enriching an Effect Calculus with Linear Types
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Synthetic differential geometry
• Title not available (Why is that?)
• A linear logical framework
• Title not available (Why is that?)
• Categorical combinators
• Quasitoposes, Quasiadhesive Categories and Artin Glueing
• Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear Logic
• An introduction to differential linear logic: proof-nets, models and antiderivatives
• Nesting forward-mode AD in a functional framework
• Title not available (Why is that?)
• A Categorical Semantics for Linear Logical Frameworks
• Title not available (Why is that?)
• Title not available (Why is that?)
• Correctness of automatic differentiation via diffeologies and categorical gluing
• On the Versatility of Open Logical Relations
• Reverse AD at higher types: pure, principled and denotationally correct

Cited In (6)

• CHAD for expressive total languages
• Reverse AD at higher types: pure, principled and denotationally correct
• Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library
• Concrete categories and higher-order recursion. With applications including probability, differentiability, and full abstraction
• On formal certification of AD transformations
• Title not available (Why is that?)

This page was built for publication: Reverse AD at higher types: pure, principled and denotationally correct

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2233481)