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.

翻译：懒惰评估是功能程序员的有力工具,它能够简明地表达需求计算和在其他评价战略下无法提供的构成形式。 但是,懒惰评估的典型性质使得很难以非正式或正式的方式分析一个方案的计算成本。在这项工作中,我们提出了一个新颖而简单的框架,用于根据最近的懒惰评估模式(Clairvoyant call-culity-value)正式推理懒惰计算成本。我们框架的主要特征是其简单性,正如我们对“阴暗蒙达”的定义所表现的那样。这道寺既简单易定义(约20行 Coq ),又易于解释。我们表明,这道寺可以有效地用于机械地解释在 Coq 书写的懒惰功能方案中的计算成本。