Incrementalization speeds up computations by avoiding unnecessary recomputations and by efficiently reusing previous results. While domain-specific techniques achieve impressive speedups, e.g., in the context of database queries, they are difficult to generalize. Meanwhile, general approaches offer little support for incrementalizing domain-specific operations. In this work, we present DeCo, a novel core calculus for incremental functional programming with support for a wide range of user-defined data types. Despite its generic nature, our approach statically incrementalizes domain-specific operations on user-defined data types. It is, hence, more fine-grained than other generic techniques which resort to treating domain-specific operations as black boxes. We mechanized our work in Lean and proved it sound, meaning incrementalized execution computes the same result as full reevaluation. We also provide an executable implementation with case studies featuring examples from linear algebra, relational algebra, dictionaries, trees, and conflict-free replicated data types, plus a brief performance evaluation on linear and relational algebra and on trees.

翻译：增量计算通过避免不必要的重复计算并高效复用先前结果来加速运算。尽管领域特定技术（例如在数据库查询场景中）已实现显著的加速效果，但这些方法难以推广。与此同时，通用方法对领域特定操作的增量化支持有限。本文提出DeCo——一种支持广泛用户自定义数据类型的增量函数式编程新型核心演算。尽管具有通用性，我们的方法能静态地对用户自定义数据类型上的领域特定操作进行增量优化。因此，相较于其他将领域特定操作视为黑盒的通用技术，本方法具有更细粒度的优化能力。我们在Lean中形式化实现了该演算并证明了其可靠性，即增量执行与完全重评估的计算结果一致。同时提供了可执行实现及案例研究，涵盖线性代数、关系代数、字典、树及无冲突复制数据类型等示例，并对线性代数、关系代数及树结构进行了简要的性能评估。