Invited Talk at PPS seminar, University Paris Diderot.
AlumniPaolo G. Giarrusso delivers an invited talk Incrementalizing
λ-Calculi by Static Differentiation: A Theory of Changes for
Higher-Order Languages and Ongoing Work at the PPS seminar of
the University Paris Diderot (Paris 7). The talk is based on our
PLDI 2014 paper and ongoing work in the “incremental λ-calculus”
project.
Abstract
If the result of an expensive computation is invalidated by a small change to the input, the old result should be updated incrementally instead of reexecuting the whole computation. I’ll give an overview of our approach to this problem, as presented in our recent paper at PLDI 2014, and discuss ongoing work.
We incrementalize programs using derivatives: A derivative maps changes in the program’s input directly to changes in the program’s output, without reexecuting the original program. We present a program transformation taking programs to their derivatives, which is fully static and automatic, supports first-class functions, and produces derivatives amenable to standard optimization.
We proved the program transformation correct in Agda for a family of simply-typed λ-calculi, parameterized by base types and primitives. A precise interface specifies what is required to incrementalize the chosen primitives.
In ongoing work, we are investigating different extensions:
-
simplifying our correctness proofs using category theory and realizability;
-
proving more optimizations correct using abstract types and parametricity;
-
static memoization to improve performance, using a variant of call-by-push-value as an intermediate program representation.
I will briefly mention our progress on these extensions, together with open questions.