带名称的增量计算
Incremental Computation with Names
摘要：
在过去的三十年中，在开发通用的、基于语言的增量计算方法方面取得了重大进展，其目的是在输入改变时有效地更新计算结果。这种方法的一个关键设计挑战是如何为广泛的程序提供有效的增量支持。在本文中，我们认为，一流的名字是一个关键的语言特征，有效的增量计算。名称标识了要在程序的不同运行中重用的计算，使它们成为第一类给了程序员对重用的高度控制。我们展示了名称的好处，提出NOMINAL ADAPTON，ML类语言的增量计算的名称。我们描述了如何使用NOMINAL ADAPTON来有效地递增几个标准编程模式-包括映射，折叠和展开-并展示了如何构建高效的，递增的概率树和尝试。由于NOMINAL ADAPTON的实现是微妙的，我们将其形式化为核心演算，并证明它是从头开始一致的，这意味着它总是产生与简单地重新运行计算相同的答案。最后，我们证明了NOMINAL ADAPTON可以提供大的加速比从头开始计算和ADAPTON，以前的国家的最先进的增量计算系统。
英文摘要：
Over the past thirty years, there has been significant progress in developing general-purpose, language-based approaches to incremental computation, which aims to efficiently update the result of a computation when an input is changed. A key design challenge in such approaches is how to provide efficient incremental support for a broad range of programs. In this paper, we argue that first-class names are a critical linguistic feature for efficient incremental computation. Names identify computations to be reused across differing runs of a program, and making them first class gives programmers a high level of control over reuse. We demonstrate the benefits of names by presenting NOMINAL ADAPTON, an ML-like language for incremental computation with names. We describe how to use NOMINAL ADAPTON to efficiently incrementalize several standard programming patterns -- including maps, folds, and unfolds -- and show how to build efficient, incremental probabilistic trees and tries. Since NOMINAL ADAPTON's implementation is subtle, we formalize it as a core calculus and prove it is from-scratch consistent, meaning it always produces the same answer as simply re-running the computation. Finally, we demonstrate that NOMINAL ADAPTON can provide large speedups over both from-scratch computation and ADAPTON, a previous state-of-the-art incremental computation system.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
