Evolving the Incremental {\lambda} Calculus into a Model of Forward Automatic Differentiation (AD)

TL;DR

This paper transforms the incremental λ-calculus into a formal model of forward automatic differentiation, providing machine-checked proofs of correctness for the new differentiation model.

Contribution

It introduces a mutation of the incremental λ-calculus to serve as a formal, verifiable model of forward automatic differentiation.

Findings

The mutated calculus models forward AD effectively.

Machine-checked proofs confirm the correctness of the AD model.

The approach can be extended to proofs for other properties.

Abstract

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 $\lambda$-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.