Kelly, Robert and Pearlmutter, Barak A. and Siskind, Jeffrey Mark (2016) Evolving the Incremental Lambda Calculus into a Model of Forward Automatic Differentiation (AD). In: AD 2016 Conference: 7th International Conference on Algorithmic Differentiation, September 12-15, 2016, Oxford, U.K..

Preview

Download (116kB) | Preview

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 λ-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.

Item Type:	Conference or Workshop Item (Paper)
Additional Information:	Extended abstract presented at the AD 2016 Conference, Sep 2016, Oxford UK. Cite as: arXiv:1611.03429 [cs.PL]
Keywords:	Incremental Lambda Calculus; Forward Automatic Differentiation (AD);
Academic Unit:	Faculty of Science and Engineering > Computer Science
Item ID:	8116
Depositing User:	Barak Pearlmutter
Date Deposited:	03 Apr 2017 14:55
Refereed:	Yes
Funders:	Science Foundation Ireland (SFI)
URI:	https://arxiv.org/abs/1611.03429
Use Licence:	This item is available under a Creative Commons Attribution Non Commercial Share Alike Licence (CC BY-NC-SA). Details of this licence are available here

Repository Staff Only(login required)

Item control page

Downloads

Origin of downloads