Skip to Main content Skip to Navigation
Conference papers

Incremental λ-Calculus in Cache-Transfer Style Static Memoization by Program Transformation

Paolo Giarrusso 1 Yann Régis-Gianas 2, 3 Philipp Schuster 4
3 PI.R2 - Design, study and implementation of languages for proofs and programs
Inria de Paris, CNRS - Centre National de la Recherche Scientifique, IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale, UPD7 - Université Paris Diderot - Paris 7
Abstract : Incremental computation requires propagating changes and reusing intermediate results of base computations. Derivatives, as produced by static differentiation [7], propagate changes but do not reuse intermediate results, leading to wasteful recomputation. As a solution, we introduce conversion to Cache-Transfer-Style, an additional program transformations producing purely incremental functional programs that create and maintain nested tuples of intermediate results. To prove CTS conversion correct, we extend the correctness proof of static differentiation from STLC to untyped λ-calculus via step-indexed logical relations, and prove sound the additional transformation via simulation theorems. To show ILC-based languages can improve performance relative to from-scratch recomputation, and that CTS conversion can extend its applicability , we perform an initial performance case study. We provide derivatives of primitives for operations on collections and incrementalize selected example programs using those primitives, confirming expected asymptotic speedups.
Document type :
Conference papers
Complete list of metadata

Cited literature [29 references]  Display  Hide  Download

https://hal.inria.fr/hal-02405864
Contributor : Yann Regis-Gianas <>
Submitted on : Wednesday, December 11, 2019 - 9:10:58 PM
Last modification on : Friday, April 10, 2020 - 5:28:53 PM
Long-term archiving on: : Thursday, March 12, 2020 - 10:34:39 PM

File

giarusso19incremental.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02405864, version 1

Citation

Paolo Giarrusso, Yann Régis-Gianas, Philipp Schuster. Incremental λ-Calculus in Cache-Transfer Style Static Memoization by Program Transformation. ESOP 2019 - European Symposium on Programming, Apr 2019, Prague, Czech Republic. ⟨hal-02405864⟩

Share

Metrics

Record views

361

Files downloads

212