一句话：提出基于 clairvoyant call-by-value 的框架与 clairvoyance monad，在 Coq 中机械化推理惰性函数式程序的计算开销。
惰性求值虽能简洁表达按需计算并带来组合性，但其有状态特性使程序计算开销难以进行非形式或形式分析。本文基于一种新的惰性求值模型——clairvoyant call-by-value，提出一个简单框架，用于形式化推理惰性计算开销。核心定义是 clairvoyance monad，仅约 20 行 Coq 即可定义，且易于推理。作者证明该 monad 可有效用于机械化推理用 Coq 编写的惰性函数式程序的计算开销。该工作降低了成本推理的门槛，并展示了在证明助手中处理惰性求值成本的可行路径。
Lazy evaluation is a powerful tool for functional programmers. It enables the concise expression of on-demand computation and a form of compositionality not available under other evaluation strategies. However, the stateful nature of lazy evaluation makes it hard to analyze a program's computational cost, either informally or formally. In this work, we present a novel and simple framework for formally reasoning about lazy computation costs based on a recent model of lazy evaluation: clairvoyant call-by-value. The key feature of our framework is its simplicity, as expressed by our definition of the clairvoyance monad. This monad is both simple to define (around 20 lines of Coq) and simple to reason about. We show that this monad can be effectively used to mechanically reason about the computational cost of lazy functional programs written in Coq.
@article{paperbot1129,
title = {Reasoning about the garden of forking paths},
author = {Yao Li and Li-yao Xia and Stephanie Weirich},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {ICFP},
year = {2021},
doi = {10.1145/3473585}
}