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$-calut t 的计算方法,可以进行大幅削减(即在抽象体中进行削减),并且保证只有在需要时才对参数进行评估,而且最多一次。这种微积分使用明确的替代方法,并分解现有的按需强烈呼叫的战略,但允许进行更多的削减序列,而且往往更短的顺序,同时保持需要。微积分在一种强烈的意义上被证明是正常化的:当美元-lumbda$-termt在 $lumbda$-calulus中加入一种正常的表格时,那么从微积分中得出的任何削减序列最终都会达到正常形式的代表。我们还展示了对这种具有钻石特性的微积分过程的限制,这种微积分只能进行最短的削减序列,这比现有战略系统化得更好。我们用Abella证据助理来将部分的微积分解量,并讨论这一实验如何影响其设计。特别是它导致我们根据缩缩写规则对按键递减要求作出新的描述。</s>