Self-adjusting computation is an evaluation model in which programs can respond efficiently to small changes to their input data by using a change-propagation mechanism that updates 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 indirect nature of previously proposed language techniques, it remains difficult to reason about the efficiency of selfadjusting programs and change propagation. In this paper, we propose a cost semantics for self-adjusting computation that enables reasoning about its effectiveness. As our source language, we consider a direct-style -calculus with firstclass mutable references and develop a notion of trace distance for source programs. To facilitate asymptotic analysis, we propose techniques for composing and generalizing concre...
Ruy Ley-Wild, Umut A. Acar, Matthew Fluet