一句话:提出新抽象机证明强传值调用求值合理,开销线性并以内爆式共享实现指数加速。
在 λ-演算中,β-归约步数能否作为合理的时间代价模型(即与图灵机时间多项式相关)取决于求值策略。弱(抽象之外)传值调用已知合理,而 Lévy 最优并行这一强策略却不合理;强情形的合理性更微妙,2014 年 Accattoli 与 Dal Lago 证明了强传名调用合理,但其抽象机开销为 β-步数的二次方。本文证明强传值调用对时间也是合理的:作者设计了一种新的抽象机,实现 useful sharing 且开销线性,并在此基础上引入一种内爆式共享(implosive sharing),与 useful sharing 混合使用;对某些项族,该机器以 β-步数的对数时间执行,从而获得指数级加速。
Whether the number of β -steps in the λ-calculus can be taken as a reasonable time cost model (that is, polynomially related to the one of Turing machines) is a delicate problem, which depends on the notion of evaluation strategy. Since the nineties, it is known that weak (that is, out of abstractions) call-by-value evaluation is a reasonable strategy while Lévy's optimal parallel strategy, which is strong (that is, it reduces everywhere), is not. The strong case turned out to be subtler than the weak one. In 2014 Accattoli and Dal Lago have shown that strong call-by-name is reasonable, by introducing a new form of useful sharing and, later, an abstract machine with an overhead quadratic in the number of β-steps.Here we show that also strong call-by-value evaluation is reasonable for time, via a new abstract machine realizing useful sharing and having a linear overhead. Moreover, our machine uses a new mix of sharing techniques, adding on top of useful sharing a form of implosive sharing, which on some terms brings an exponential speed-up. We give examples of families that the machine executes in time logarithmic in the number of β-steps.