2016/11/10 by Robert Kelly, Barak A. Pearlmutter, Kelly, Robert +3
Computer Science · #Advanced Database Systems and Queries #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.1611.03429
openalex publication_date 2016/11/10 · openalex created_date 2024/04/11 · openalex updated_date 2026/07/28
Formal transformations somehow resembling the usual derivative are surprisingly common in computer science, with two notable examples being derivatives of regular expressions and derivatives of types. A newcomer to this list is the incremental λ-calculus, or ILC, a "theory of changes" that deploys a formal apparatus allowing the automatic generation of efficient update functions which perform incremental computation. The ILC is not only defined, but given a formal machine-understandable definition---accompanied by mechanically verifiable proofs of various properties, including in particular correctness of various sorts. Here, we show how the ILC can be mutated into propagating tangents, thus serving as a model of Forward Accumulation Mode Automatic Differentiation. This mutation is done in several steps. These steps can also be applied to the proofs, resulting in machine-checked proofs of the correctness of this model of forward AD.