Self-adjusting computation is an evaluation model in which pro-grams can respond efficiently to small changes to their input data byusing a change-propagation mechanism that updates computationby re-building only the parts affected by changes. Previous workhas proposed language techniques for self-adjusting computationand showed the approach to be effective in a number of applicationareas. However, due to the complex semantics of change propaga-tion and the indirect nature of previously proposed language tech-niques, it remains difficult to reason about the efficiency of self-adjusting programs and change propagation. In this paper, we propose a cost semantics for self-adjustingcomputation that enables reasoning about its effectiveness. As oursource language, we consider a direct-style λ-calculus with first-class mutable references and develop a notion of trace distancefor source programs. To facilitate asymptotic analysis, we propose techniques for composing and generalizing concrete distances viatrace contexts (traces with holes). We then show how to translate the source language into a self-adjusting target language such thatthe translation (1) preserves the extensional semantics of the sourceprograms and the cost of from-scratch runs, and (2) ensures thatchange propagation between two evaluations takes time boundedby their relative distance. We consider several examples and ana-lyze their effectiveness by considering upper and lower bounds.
展开▼
