为什么按值调用评估策略不是图灵完备的？答案

【问题标题】：Why call-by-value evaluation strategy is not Turing complete?为什么按值调用评估策略不是图灵完备的？
【发布时间】：2011-02-26 00:37:09
【问题描述】：

我正在阅读一篇关于不同 evaluation strategies 的文章（我在 wiki 中链接了文章，但我正在阅读另一篇不是英文的文章）。它说与call-by-name 和call-by-need 策略不同，call-by-value 策略不是 Turing complete。

谁能解释一下，为什么会这样？如果可能，请添加示例。

【问题讨论】：

@KennyTM：我试图在文章末尾的参考资料中找到来源。如果你愿意，我可以给你一个链接，但它是俄文的。
一篇俄语文章总比没有好。不是我，但有人可能会读俄语。
当然有许多使用按值调用的语言是图灵完备的。我怀疑这篇文章讨论的是一种特定的语言，如果它使用按值调用，它就不会完整（尽管我无法完全想象这种语言会是什么样子）。
所谓的按值调用语言并不完全是按值调用：它们使用特殊形式的控制结构。我不知道任何基于 CBV lambda-calculus 没有特殊形式的语言。有吗？

标签： compiler-construction programming-languages computer-science turing-complete

【解决方案1】：

如果不参考某些特定语言，您的问题没有多大意义，但我会尽力回答关于无类型 Lambda 演算的问题。

无类型 lambda 演算的按值调用定点组合器（即“Y 组合器”）的存在似乎驳斥了基本主张（参见：Fixed Point Combinator）。这种组合器的存在打破了强规范化，这表明至少存在一种使用按值调用评估策略的图灵完备语言。

更可能影响语言的图灵完整性的是类型系统的存在（或缺乏）。例如，简单类型的 lambda 演算不能编码定点组合器，并且是强归一化的（即所有类型良好的项都归约为一个值），然而，无论采用何种评估策略，这都是正确的。相反，它是类型系统的结果。

【讨论】：

【解决方案2】：

我对您正在阅读的文章中的主张提出异议。（我没有为此获得报酬，所以我将提供一个暗示性的论点，而不是证明。）

众所周知，至少在正常阶归约（又称按名称调用）下，纯 lambda 演算是图灵完备的。但是，如果我们查看 John Reynolds 的开创性论文Definitional Interpreters for Higher-Order Programming Languages，我们可以看到 Reynolds 详细讨论了按名称调用和按值调用之间的区别。该论点的一个关键部分是，为了做出适当的区分，我们可以将程序转换为 continuation-passing 样式。 CPS 转换对于按需调用和按值调用是不同的，但转换后的术语可以在任何一种样式中进行评估。

所以论点来了：编写一个模拟图灵机的 lambda 演算程序，然后使用 CBN 变换对其进行 CPS 变换，然后您可以使用 CBV 缩减策略评估生成的代码。砰!图灵完备。

在实践中，我敢打赌你可以编写一个 CBV 程序来模拟图灵机；选择一个合适的定点组合器可能就足够了，例如 Θ。（更著名的 Y 组合器仅在按名称减少策略下工作，即正常顺序减少。）

免责声明：我已经很久没有研究过 lambda 演算了，我确信上面的论点中有几个细节是错误的。但我对内容很有信心。这不是我第一次在有关编程语言理论的在线资源中发现明显错误的地方。

【讨论】：