一句话:提出用非确定性替代堆状态的预见性求值语义,证明其与标准按需调用语义强等价,并简化推理与给出首个指称代价语义。
按需调用(惰性求值)支持组合式编程与无限数据,但其标准语义(Launchbury 自然语义)依赖堆来记忆延迟求值结果;堆的状态性使惰性程序操作行为的推理复杂。本文提出一种新的惰性求值语义——预见性求值(clairvoyant evaluation),用非确定性取代堆状态效应,并在强意义上证明其与标准语义等价。该语义显著简化了操作推理,使文献中若干结果的证明更简单,并首次为惰性求值给出了指称代价语义(denotational cost semantics)。
Call-by-need evaluation, also known as lazy evaluation, provides two key benefits: compositional programming and infinite data. The standard semantics for laziness is Launchbury’s natural semantics DBLP:conf/popl/Launchbury93, which uses a heap to memoise the results of delayed evaluations. However, the stateful nature of this heap greatly complicates reasoning about the operational behaviour of lazy programs. In this article, we propose an alternative semantics for laziness, clairvoyant evaluation , that replaces the state effect with nondeterminism, and prove this semantics equivalent in a strong sense to the standard semantics. We show how this new semantics greatly simplifies operational reasoning, admitting much simpler proofs of a number of results from the literature, and how it leads to the first denotational cost semantics for lazy evaluation.