能否证明 call-by-need 在所有归约策略中具有最小的渐近时间复杂度？答案

【问题标题】：Can it be proved that call-by-need has the minimal asymptotic time complexity among all reduction strategies?能否证明 call-by-need 在所有归约策略中具有最小的渐近时间复杂度？
【发布时间】：2017-07-12 14:56:41
【问题描述】：

当我读到 Church Rosser II 定理时here

定理（Church Rosser II）

如果有一个终止归约，那么最外面的归约也将终止。

我想知道：是否有一些定理加强了 Church Rosser II 定理，使其讲述的是渐近时间复杂度而不是终止？

或者，能否证明按需调用策略在所有归约策略中具有最小的渐近时间复杂度？

【问题讨论】：

为什么选择渐近复杂度？直观地说，按需调用的总体复杂性应该是最低的，在绝对数量上。
我很确定按需调用在任何合理的成本模型下都不是最优的，假设它被理解为不减少 lambda 的内部（可以多次应用）。不过，对我来说，究竟如何证明它是渐近非最优的并不是那么明显。
我认为这个证明中棘手的部分是“在所有归约策略中”。全局记忆是否算作评估策略？如果是，它有什么复杂性？

标签： haskell functional-programming lazy-evaluation asymptotic-complexity lambda-calculus

【解决方案1】：

当然不是。考虑

f x y = sum [1..x] + y
g x = sum (map (f x) [1..x])

按需减少g x 将执行O(x^2) 加法，但实际上只需要O(x)。例如，惰性 HNF 会给我们带来这种复杂性。

-- The definition f3 will get lazily refined.
let f3 y = f 3 y = sum [1,2,3] + y

g 3 = sum (map f3 [1,2,3])
    = sum [f3 1, f3 2, f3 3]

-- Now let's refine f3 to HNF *before* applying it
f3 y = sum [1,2,3] + y
     = 6 + y

-- And continue g 3
g 3 = sum [f3 1, f3 2, f3 3]
    -- no need to compute sum [1..x] three times
    = sum [6 + 1, 6 + 2, 6 + 3]
    = ...

我在这里多次挥动评估顺序，但希望您能理解。我们在应用之前将函数体简化为 HNF，从而共享任何不依赖于参数的计算。

有关这方面的更多信息，请参阅 Michael Jonathan Thyer 的Lazy Specialization。

【讨论】：

【解决方案2】：

我认为你的问题有点混乱。请让我澄清几点。

首先，您提到的定理在传统上被称为标准化定理，是由于 Curry 和 Feys（组合逻辑 I，1958 年），由 Hindley（Standard and normal reductions）推广到 eta 减少，然后由许多其他人修改作者（参见例如question）。

其次，最外层缩减不同于按需调用（按需调用甚至不是传统意义上的缩减策略）。

谈到复杂性问题，即问题的核心，按需调用仅在弱归约方面是最优的。然而，弱归约并不总是减少 lambda 项的最佳方法。一个众所周知的例子是以下术语

                                n 2 I I

其中 n 和 2 是教堂整数，而 I 是一个恒等式。我在最后添加两个 I，否则弱归约语言会过早停止计算。

观察到该术语简化为

                          2 (2 (... (2 I))..) I

和 (2 I) 减少到 I。因此，通过最内层减少，您将能够在线性时间 w.r.t n 中减少项。

另一方面，我邀请你在 Haskell 中执行之前的计算，你会发现归约时间在 n 中呈指数增长。我留给您了解这种现象的原因。

在thread 中进行了类似的讨论。

【讨论】：