A cost semantics for self-adjusting computation
A cost semantics for self-adjusting computation
复制标题
自调整计算的成本语义
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
M. Fluet
中科院分区：
文献类型：
--
作者：
Ruy Ley;Umut A. Acar;M. Fluet
自我调整计算是一种评估模型，可以通过使用更改通用机制来有效地对其输入数据进行小小的更改，该机制仅通过重新构建受更改影响的零件来更新计算。 - 调整计算并显示出在许多应用领域有效的方法，但是，由于变化传播的复杂语义和先前提出的语言技术的间接性质，很难理解自我调整程序的效率并改变传播。
在本文中，我们提出了一种自我调整计算的成本语义，使其有效性作为我们的源语言。为了促进不对称分析，我们提出了通过痕量上下文组成和概括具体距离的技术（带有孔的痕迹）。源程序的扩展语义和从划痕的成本运行，（2）确保两个评估之间的变化传播是由它们的相对距离绑定的，我们考虑了几个示例，并通过考虑上限和下限来分析其有效性。
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 self-adjusting 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 first-class mutable references and develop a notion of trace distance for source programs. 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 into a self-adjusting target language such that 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 bounded by their relative distance. We consider several examples and analyze their effectiveness by considering upper and lower bounds.