paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Call-by-need is clairvoyant call-by-value

按需调用即是预见性按值调用
ICFP 3(ICFP)2019匹配度 2/10 · 该论文属于纯函数式语言的形式语义研究,讨论惰性求值的替代语义与指称代价语义,未涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析等用户核心方向。虽然与程序语言理论相关,但与研究画像中的交叉方向匹配度很低。引用 14 inbox
Jennifer Hackett, Graham Hutton
crossref: 2026-09-10

AI 速览

一句话:提出用非确定性替代堆状态的预见性求值语义,证明其与标准按需调用语义强等价,并简化推理与给出首个指称代价语义。

按需调用(惰性求值)支持组合式编程与无限数据,但其标准语义(Launchbury 自然语义)依赖堆来记忆延迟求值结果;堆的状态性使惰性程序操作行为的推理复杂。本文提出一种新的惰性求值语义——预见性求值(clairvoyant evaluation),用非确定性取代堆状态效应,并在强意义上证明其与标准语义等价。该语义显著简化了操作推理,使文献中若干结果的证明更简单,并首次为惰性求值给出了指称代价语义(denotational cost semantics)。

问题
惰性求值的标准 Launchbury 语义使用堆状态记忆延迟结果,状态效应使对惰性程序操作行为的推理复杂。
方法
提出预见性求值语义,以非确定性替代堆状态,并证明其与标准语义强等价。
评估
通过语义等价证明,展示该语义可简化操作推理、给出文献结果的更简单证明,并导出首个惰性求值的指称代价语义。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot616,
  title = {Call-by-need is clairvoyant call-by-value},
  author = {Jennifer Hackett and Graham Hutton},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {3},
  number = {ICFP},
  year = {2019},
  doi = {10.1145/3341718}
}