一句话：提出 call-by-silly 退化演算，镜像 call-by-need，合并按名重复与按值擦除的最差行为，并用多类型与抽象机分析。
本文研究 λ 演算中复制与擦除如何结合：call-by-need 将 call-by-name 的“明智擦除”与 call-by-value 的“明智复制”融合，而本文构造一个对称的退化演算 call-by-silly，融合 call-by-name 的愚蠢复制与 call-by-value 的愚蠢擦除。作者通过重写性质和多类型系统验证该设计，证明 call-by-silly 与 call-by-value 诱导相同的上下文等价，从而镜像了 call-by-need 与 call-by-name 操作等价这一主定理；这表明按值调用的上下文等价对效率不敏感。文章还定义 call-by-silly 求值策略与实现该策略的抽象机，并用紧多类型精确测量策略步数，最后证明该策略计算该演算中最长的求值序列。
Call-by-need evaluation for the lambda-calculus can be seen as merging the best of call-by-name and call-by-value, namely the wise erasing behaviour of the former and the wise duplicating behaviour of the latter. To better understand how duplication and erasure can be combined, we design a degenerated calculus, dubbed call-by-silly, that is symmetric to call-by-need in that it merges the worst of call-by-name and call-by-value, namely silly duplications by-name and silly erasures by-value. We validate the design of the call-by-silly calculus via rewriting properties and multi types. In particular, we mirror the main theorem about call-by-need -- that is, its operational equivalence with call-by-name -- showing that call-by-silly and call-by-value induce the same contextual equivalence. This fact shows the blindness with respect to efficiency of call-by-value contextual equivalence. We also define a call-by-silly strategy and a call-by-silly abstract machine implementing the strategy. Moreover, we measure the number of steps taken by the strategy via tight multi types. Lastly, we prove that the call-by-silly strategy computes evaluation sequences of maximal length in the calculus.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{AccattoliL26,
title = {Mirroring Call-by-Need, or Values Acting Silly},
author = {Beniamino Accattoli and Adrienne Lancelot},
journal = {Logical Methods in Computer Science},
volume = {Volume 22, Issue 3},
year = {2026},
doi = {10.46298/lmcs-22(3:3)2026}
}