是否可以证明所有减少策略中的按需调用具有最小的渐近时间复杂度？

Question

当我在这里阅读Church Rosser II定理时

定理(Church Rosser II)

如果有一个终止减少,那么最外面的减少也将终止.

我想知道:是否有一些定理加强了教会Rosser II定理,以便它告诉渐近时间复杂度而不是终止？

或者,是否可以证明所需减少策略在所有减少策略中具有最小的渐近时间复杂度？

Answer 1

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

首先，你提到的定理传统上被称为标准化定理，是由 Curry 和 Feys (组合逻辑 I, 1958) 提出的，被 Hindley 推广到 eta 约简 (标准和正态约简)，然后被许多其他作者修改 (参见例如这个问题）。

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

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

                                n 2 I I

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

观察该术语减少为

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

(2 I) 减少为 I。因此，通过最内层的减少，您将能够减少关于 n 的线性时间项。

另一方面，我邀请你在 Haskell 中执行前面的计算，你会发现归约时间以 n 为指数增长。造成这种现象的原因就留给大家去了解一下吧。

此线程中也进行了类似的讨论。