A Cost Semantics for Self-Adjusting Computation
Self-adjusting computation is an evaluation model in which programs can respond efficiently to small changes to their input data. The approach relies on a change-propagation mechanism that can update computation by re-building only the parts affected by changes. Previous work has proposed language techniques for self-adjusting computation and showed the approach to be effective in a number of application areas. However, due to the complex semantics of change propagation and the nature of previously proposed language techniques, determining how efficient a self-adjusting program will be under changes remains difficult.
In this paper, we consider a lambda-calculus with first-class mutable references and give this language a cost semantics. We develop a notion of a trace distance for source programs to quantify the differences between concrete evaluations. To facilitate asymptotic analysis, we propose techniques for composing and generalizing concrete distances via trace contexts (traces with holes). We then show how to translate the source language using an adaptive CPS translation into a self-adjusting target language. The translation (1) preserves the extensional semantics of the source programs and the cost of from-scratch runs, and (2) ensures that change propagation between two evaluations takes time proportional to their relative distance. We consider several examples and show them amenable to self-adjusting computation.
Joint work with Ruy Ley-Wild and Umut Acar.