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.

翻译：惰性求值是函数式编程中一项强大的工具，它能够提升组合性并可能带来更好的性能，但其计算成本的分析颇具挑战。现有工作要么需要手动标注共享关系，要么依赖分离逻辑对可变单元堆进行推理。本文提出一种双向需求语义，允许在不依赖特殊程序逻辑的情况下，对惰性程序的计算成本进行外部推理。为展示方法的有效性，我们将需求语义应用于多种案例研究，包括插入排序、选择排序、Okasaki的银行家队列以及隐式队列。我们使用Rocq证明器（原称Coq）形式化证明了银行家队列与隐式队列均满足分摊性与持久性。此外，我们提出了反向物理学家方法——经典物理学家方法的一种新颖变体，该方法结合需求语义，实现了对分摊性与持久性的机械化、模块化及组合式推理。