可以证明惰性求值在所有规约策略中具有最小的渐进时间复杂度吗？

Question

当我阅读 Church Rosser II 定理的时候（链接），我想知道是否存在一些加强版的定理，使其不仅表明外最约简会终止，还能告诉我们渐进时间复杂度？或者，是否可以证明按需调用策略在所有约简策略中具有最小的渐进时间复杂度？

- luochen1990

---

为什么要考虑渐进复杂度？直觉上，按需调用应该在绝对数字上具有最小的复杂度。 - Joachim Breitner

我非常确定在任何合理的成本模型下，按需调用都不是最优的，假设它被理解为不在 lambda 函数体内进行缩减（这可能会被多次应用）。对我来说并不那么明显如何构建一个渐近非最优的案例。 - Reid Barton

我认为这个证明中棘手的部分是“在所有简化策略中”。全局记忆化是否算作评估策略？如果是，它的复杂度是多少？ - Luka Rahne

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。

- luqui

Answer 2

我认为你的问题有些混淆。请让我澄清一些要点。

首先，你提到的定理通常被称为标准化定理，由Curry和Feys（组合逻辑I，1958）提出，由Hindley（Standard and normal reductions）推广到eta约简，然后被许多其他作者修订（例如，参见这个question）。

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

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

                                n 2 I I

其中n和2是Church整数，I是一个恒等式。我在末尾添加了两个I，否则弱规约语言会过早停止计算。

观察该项规约为

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

并且 (2 I) 缩减为 I。因此，通过最内层缩减，您将能够相对于 n 线性时间缩减术语。

另一方面，我邀请您在 Haskell 中执行先前的计算，您会发现缩减时间随着 n 增加呈指数增长。我留给您理解这种现象的原因。

类似的讨论已经在这个thread中进行了。

- Andrea Asperti