paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Strong Call-by-Value is Reasonable, Implosively

强传值调用是合理的:内爆式共享
LICS 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2021匹配度 1/10 · 该论文研究强传值调用求值的合理性与抽象机实现,属于纯形式语义与 λ 演算理论,未涉及静态分析、LLM/Agent、浮点或贝叶斯程序分析,与用户画像中 PL 与 AI 交叉及程序分析的核心方向无关。引用 2 inbox
Beniamino Accattoli, Andrea Condoluci, Claudio Sacerdoti Coen
crossref: 2026-09-12

AI 速览

一句话:提出新抽象机证明强传值调用求值合理,开销线性并以内爆式共享实现指数加速。

在 λ-演算中,β-归约步数能否作为合理的时间代价模型(即与图灵机时间多项式相关)取决于求值策略。弱(抽象之外)传值调用已知合理,而 Lévy 最优并行这一强策略却不合理;强情形的合理性更微妙,2014 年 Accattoli 与 Dal Lago 证明了强传名调用合理,但其抽象机开销为 β-步数的二次方。本文证明强传值调用对时间也是合理的:作者设计了一种新的抽象机,实现 useful sharing 且开销线性,并在此基础上引入一种内爆式共享(implosive sharing),与 useful sharing 混合使用;对某些项族,该机器以 β-步数的对数时间执行,从而获得指数级加速。

问题
强(到处归约)传值调用求值是否构成合理的时间代价模型,即其 β-步数是否与图灵机时间多项式相关。
方法
构造一种新的抽象机来实现 useful sharing,并引入内爆式共享(implosive sharing)与 useful sharing 混合,以控制求值开销。
评估
通过理论分析证明新抽象机的开销与 β-步数呈线性关系,并给出项族示例展示机器可在对数时间内执行、获得指数级加速。
原文摘要(Abstract)

Whether the number of β -steps in the λ-calculus can be taken as a reasonable time cost model (that is, polynomially related to the one of Turing machines) is a delicate problem, which depends on the notion of evaluation strategy. Since the nineties, it is known that weak (that is, out of abstractions) call-by-value evaluation is a reasonable strategy while Lévy's optimal parallel strategy, which is strong (that is, it reduces everywhere), is not. The strong case turned out to be subtler than the weak one. In 2014 Accattoli and Dal Lago have shown that strong call-by-name is reasonable, by introducing a new form of useful sharing and, later, an abstract machine with an overhead quadratic in the number of β-steps.Here we show that also strong call-by-value evaluation is reasonable for time, via a new abstract machine realizing useful sharing and having a linear overhead. Moreover, our machine uses a new mix of sharing techniques, adding on top of useful sharing a form of implosive sharing, which on some terms brings an exponential speed-up. We give examples of families that the machine executes in time logarithmic in the number of β-steps.

链接与引用

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

BibTeX
@inproceedings{paperbot6206,
  title = {Strong Call-by-Value is Reasonable, Implosively},
  author = {Beniamino Accattoli and Andrea Condoluci and Claudio Sacerdoti Coen},
  booktitle = {LICS},
  year = {2021},
  doi = {10.1109/lics52264.2021.9470630}
}