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.

翻译：我们提出了一种支持强归约（即在抽象体内部进行归约）的需求调用λ-演算，该演算保证参数仅在需要时被求值，且最多求值一次。该演算使用显式替换，并涵盖了现有的强需求调用策略，但允许更多的归约序列（通常更短），同时保留了需求性。该演算在强意义下被证明是归一化的：只要λ-项t在λ-演算中具有范式n，那么从t出发在该演算中的任何归约序列最终都将到达范式n的一个代表元。我们还展示了该演算的一个具有菱形性质且仅执行最短长度归约序列的限制版本，这使得它在系统上优于现有策略。我们使用Abella证明助手形式化了该演算的一部分，并讨论了这一实验如何影响其设计。特别是，它引导我们基于归纳规则推导出了需求调用归约的一种新描述。