关于分叉路径花园的推理

惰性求值（lazy evaluation）是函数式程序员的强大工具。它使得按需计算的简洁表达以及在其他求值策略下无法获得的某种组合性成为可能。然而，惰性求值的含状态本质使得无论非正式还是正式地分析程序的计算代价都十分困难。本工作中，我们基于一种近期的惰性求值模型——先知式按值调用（clairvoyant call-by-value），提出一个新颖且简洁的框架，用于正式推理惰性计算代价。我们框架的关键特征在于其简洁性，这体现在我们对先知单子（clairvoyance monad）的定义中。该单子既易于定义（约 20 行 Coq），也易于推理。我们展示该单子可有效用于机械式推理 Coq 中编写的惰性函数式程序的计算代价。