Skip to Main content Skip to Navigation
Journal articles

Automatic Differentiation in PCF

Abstract : We study the correctness of automatic differentiation (AD) in the context of a higher-order, Turing-complete language (PCF with real numbers), both in forward and reverse mode. Our main result is that, under mild hypotheses on the primitive functions included in the language, AD is almost everywhere correct, that is, it computes the derivative or gradient of the program under consideration except for a set of Lebesgue measure zero. Stated otherwise, there are inputs on which AD is incorrect, but the probability of randomly choosing one such input is zero. Our result is in fact more precise, in that the set of failure points admits a more explicit description: for example, in case the primitive functions are just constants, addition and multiplication, the set of points where AD fails is contained in a countable union of zero sets of polynomials.
Document type :
Journal articles
Complete list of metadata

https://hal.archives-ouvertes.fr/hal-03379031
Contributor : Damiano Mazza Connect in order to contact the contributor
Submitted on : Thursday, October 14, 2021 - 6:16:26 PM
Last modification on : Wednesday, October 27, 2021 - 4:16:42 PM
Long-term archiving on: : Saturday, January 15, 2022 - 8:01:04 PM

File

AutoDiffPCF(1).pdf
Publisher files allowed on an open archive

Identifiers

Citation

Damiano Mazza, Michele Pagani. Automatic Differentiation in PCF. Proceedings of the ACM on Programming Languages, ACM, 2021, 5, pp.1 - 27. ⟨10.1145/3434309⟩. ⟨hal-03379031⟩

Share

Metrics

Les métriques sont temporairement indisponibles