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证明辅助工具对该演算的部分内容进行了形式化，并讨论了这一实验如何影响其设计——特别是，它引导我们基于归纳规则推导出按需调用归约的新描述。