我正在阅读一篇关于不同评估策略的文章（我在 wiki 中链接了文章，但我正在阅读另一篇不是英文的文章）。它说，与 tocall-by-name和strategy 不同call-by-need，call-by-valuestrategy不是 图灵完备的。
谁能解释一下，为什么会这样？如果可能，请添加一个示例。
问问题
702 次
2 回答
10
我对您正在阅读的文章中的主张提出异议。（我没有为此获得报酬，所以我将提供一个暗示性的论点，而不是证明。）
众所周知，至少在正常阶归约（又称按名称调用）下，纯 lambda 演算是图灵完备的。但是，如果我们查看 John Reynolds 的开创性论文Definitional Interpreters for Higher-Order Programming Languages，我们可以看到 Reynolds 详细讨论了名称调用和值调用之间的区别。该论点的一个关键部分是，为了做出适当的区分，我们可以将程序转换为continuation-passing style。CPS 变换对于按需调用和按值调用是不同的，但可以以任何一种样式评估生成的转换项。
因此，争论出现了：编写一个模拟图灵机的 lambda 演算程序，然后使用 CBN 变换对其进行 CPS 变换，然后您可以使用 CBV 缩减策略评估生成的代码。砰! 图灵完备。
在实践中，我敢打赌你可以编写一个 CBV 程序来模拟图灵机；选择一个合适的定点组合器可能就足够了，例如 Θ。（更著名的 Y 组合器仅在按名称减少策略下工作，即正常顺序减少。）
免责声明：我已经很久没有研究过 lambda 演算了，我确信上面的论点中有几个细节是错误的。但我对内容很有信心。这不是我第一次在有关编程语言理论的在线资源中发现明显错误的地方。
于 2010-05-31T20:26:15.437 回答
0
如果不参考某些特定语言，您的问题没有多大意义，但我会尽力回答关于无类型 Lambda 演算的问题。
无类型 lambda 演算的按值调用定点组合器（即“Y 组合器”）的存在似乎驳斥了基本主张（参见：定点组合器）。这种组合器的存在打破了强规范化，这表明至少存在一种使用按值调用评估策略的图灵完备语言。
更可能影响语言的图灵完整性的是类型系统的存在（或缺乏）。例如，简单类型的 lambda 演算不能编码定点组合子，并且是强归一化的（即所有类型良好的项都归约为一个值），然而，无论采用何种评估策略，这都是正确的。相反，它是类型系统的结果。
于 2010-06-01T11:40:39.323 回答