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.
翻译:我们提出了一种需求调用 $\lambda$-演算,它实现了强规约(即在抽象体内进行规约)并保证了参数仅在需要且最多一次时才会被评估。这种演算使用显式替换并取代了现有的强力需求策略,但允许更多的规约序列,通常更短,同时仍保持所需性。该演算在强熄定(即任何正则 $\lambda$-项非规约等价时)方面被证明是正则的:无论 $\lambda$-项 t 是否在 $\lambda$-演算中具有正则形式 n,演算中从 t 开始的任何规约序列最终都会到达正则形式 n 的代表。我们还展示了该演算的限制,该限制具有菱形特性且仅执行最短的规约序列,这使其比现有策略更有效。我们使用 Abella 证明辅助工具来部分形式化了该演算,并讨论了此实验对其设计的影响。特别是,它使我们推导出一种基于归纳规则的新的需求调用规约描述。