MURAL - Maynooth University Research Archive Library

    Evolving the Incremental Lambda Calculus into a Model of Forward Automatic Differentiation (AD)

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

    Download (116kB) | Preview

    Share your research

    Twitter Facebook LinkedIn GooglePlus Email more...

    Add this article to your Mendeley library


    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)
    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)

    View Item Item control page


    Downloads per month over past year

    Origin of downloads