一句话：提出支持强归约的 call-by-need λ-演算，保证按需且至多一次求值，并证明强规范化与最小归约策略。
本文研究如何在 call-by-need 求值中支持强归约，即在抽象体内部继续归约，同时保证参数只在需要时求值且至多一次。作者提出一个使用显式替换的强 call-by-need λ-演算，它包容已有的强 call-by-need 策略，但允许更多、常常更短的归约序列而不破坏按需性。论文证明该演算具有强规范化性质：只要 λ-项 t 在普通 λ-演算中有范式 n，则从 t 出发的任意归约序列最终都会到达 n 的代表。作者还给出一个具有菱形性质且只执行最短归约序列的限制版本，并用 Abella 证明助手形式化部分演算，讨论该实验对设计的影响，得到基于归纳规则的 call-by-need 归约新描述。
We present a call-by-need $\lambda$-calculus that enables strong reduction (that is, reduction inside the body of abstractions) and guarantees that arguments are only evaluated if needed and at most once. This calculus uses explicit substitutions and subsumes the existing strong-call-by-need strategy, but allows for more reduction sequences, and often shorter ones, while preserving the neededness. The calculus is shown to be normalizing in a strong sense: Whenever a $\lambda$-term t admits a normal form n in the $\lambda$-calculus, then any reduction sequence from t in the calculus eventually reaches a representative of the normal form n. We also exhibit a restriction of this calculus that has the diamond property and that only performs reduction sequences of minimal length, which makes it systematically better than the existing strategy. We have used the Abella proof assistant to formalize part of this calculus, and discuss how this experiment affected its design. In particular, it led us to derive a new description of call-by-need reduction based on inductive rules.
@article{paperbot2228,
title = {A strong call-by-need calculus},
author = {Thibaut Balabonski and Antoine Lanco and Guillaume Melquiond},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 1},
year = {2023},
doi = {10.46298/lmcs-19(1:21)2023}
}