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

Question

当我读到 Church Rosser II 定理 here

Theorem (Church Rosser II)

If there is one terminating reduction, then outermost reduction will terminate, too.

我想知道:是否有一些定理加强了 Church Rosser II 定理，以便它讲述渐近时间复杂度而不是终止？
或者，能否证明按需调用策略在所有归约策略中具有最小的渐近时间复杂度？

Answer 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 .