Call-by-need evaluation for the lambda-calculus can be seen as merging the best of call-by-name and call-by-value, namely the wise erasing behaviour of the former and the wise duplicating behaviour of the latter. To better understand how duplication and erasure can be combined, we design a degenerated calculus, dubbed call-by-silly, that is symmetric to call-by-need in that it merges the worst of call-by-name and call-by-value, namely silly duplications by-name and silly erasures by-value. We validate the design of the call-by-silly calculus via rewriting properties and multi types. In particular, we mirror the main theorem about call-by-need -- that is, its operational equivalence with call-by-name -- showing that call-by-silly and call-by-value induce the same contextual equivalence. This fact shows the blindness with respect to efficiency of call-by-value contextual equivalence. We also define a call-by-silly strategy and a call-by-silly abstract machine implementing the strategy. Moreover, we measure the number of steps taken by the strategy via tight multi types. Lastly, we prove that the call-by-silly strategy computes evaluation sequences of maximal length in the calculus.
翻译:λ演算的按需求值可视为融合了按名调用与按值调用的最佳特性,即前者明智的擦除行为与后者明智的复制行为。为深入理解复制与擦除如何结合,我们设计了一个退化演算,称之为按愚蠢调用。该演算与按需求值形成对称关系,它融合了按名调用与按值调用中最糟糕的特性,即按名调用的愚蠢复制与按值调用的愚蠢擦除。通过重写性质与多类型系统,我们验证了按愚蠢调用演算的设计合理性。特别地,我们镜像了关于按需求值的主要定理——即其与按名调用的操作等价性——证明按愚蠢调用与按值调用诱导出相同的上下文等价关系。这一事实揭示了按值调用上下文等价性在效率上的盲目性。我们还定义了按愚蠢调用策略及实现该策略的抽象机。此外,我们通过紧多类型系统度量了该策略所需的步骤数。最后,我们证明按愚蠢调用策略在演算中计算出最大长度的求值序列。