能否证明 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。

Answer 2

我觉得你的问题有点混乱。请让我澄清几点。

首先，您提到的定理传统上被称为标准化定理，归功于 Curry 和 Feys（组合逻辑 I，1958），由 Hindley 推广到 eta 约简（Standard and normal reductions), and then revised by many other authors (see e.g. this question）。

其次，最外层归约与call by need不同（call by need甚至不是传统意义上的归约策略）。

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

                                n 2 I I

其中 n 和 2 是教会整数，而 I 是身份。我在最后加了两个 I，否则弱约简语言会过早地停止计算。

观察到术语减少到

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

and (2 I) 化简为 I。因此，通过最内层的化简，您可以在线性时间 w.r.t n 中化简项。

另一边，请你在Haskell中进行前面的计算，你会发现还原时间在n呈指数增长。造成这种现象的原因就留给你们去了解了。

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

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

Can it be proved that call-by-need has the minimal asymptotic time complexity among all reduction strategies?

haskell

functional-programming

lazy-evaluation

asymptotic-complexity

lambda-calculus