一句话：提出双向需求语义，无需特殊程序逻辑即可外延推理惰性程序成本，并在 Rocq 中机化验证摊销与持久性。
惰性求值能提升函数式程序的组合性与潜在性能，但其计算成本分析颇具挑战：已有工作要么手动标注共享，要么依赖分离逻辑推理可变单元堆。本文提出双向需求语义，无需特殊程序逻辑即可外延推理惰性程序的计算成本。作者将语义用于插入排序、选择排序、Okasaki 银行家队列和隐式队列等案例，并在 Rocq（原 Coq）中形式化证明银行家队列与隐式队列兼具摊销复杂度与持久性。文章还提出反向物理学家方法——经典物理学家方法的变体，使基于需求语义的摊销与持久性推理可机械化、模块化且可组合。
Lazy evaluation is a powerful tool that enables better compositionality and potentially better performance in functional programming, but it is challenging to analyze its computation cost. Existing works either require manually annotating sharing, or rely on separation logic to reason about heaps of mutable cells. In this paper, we propose a bidirectional demand semantics that allows for extrinsic reasoning about the computation cost of lazy programs without relying on special program logics. To show the effectiveness of our approach, we apply the demand semantics to a variety of case studies including insertion sort, selection sort, Okasaki’s banker’s queue, and the implicit queue. We formally prove that the banker’s queue and the implicit queue are both amortized and persistent using the Rocq Prover (formerly known as Coq). We also propose the reverse physicist’s method, a novel variant of the classical physicist’s method, which enables mechanized, modular and compositional reasoning about amortization and persistence with the demand semantics.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2406-14787,
title = {Story of Your Lazy Function’s Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy Programs},
author = {Li-yao Xia and Laura Israel and Maite Kramarz and Nicholas Coltharp and Koen Claessen and Stephanie Weirich and Yao Li},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {ICFP},
year = {2024},
doi = {10.1145/3674626}
}