为什么按价值调用的评估策略不是完全的？

Question

我正在读一篇关于不同评价策略的文章(我用wiki链接了一篇文章，但我正在读另一篇不是英文的文章)。它说，与call-by-name和call-by-need战略不同的是，call-by-value策略不是图灵完备。

有谁能解释一下，为什么会这样？如果可能的话，请添加一个例子。

Answer 1

I在您正在阅读的文章中对的声明提出了质疑。(我不会为此得到报酬，所以我要提供一个有暗示性的论点，而不是证据。)

众所周知，至少在正规降阶(又名)下，纯lambda演算是图灵全的。但是，如果我们看约翰·雷诺兹的开创性论文“高级程序设计语言的定义解释器”，我们可以看到，雷诺兹详细地讨论了名字呼唤和价值呼唤之间的区别。论点的一个关键部分是，为了做出适当的区分，我们可以将程序转换为延拓传递样式。CPS转换对于按需要调用和按值调用是不同的，但结果转换后的术语可以在任何一种样式下进行计算。

这里有一个论点:编写一个模拟图灵机的lambda演算程序，然后用CBN变换对它进行CPS转换，您可以使用CBV缩减策略来评估结果代码。太棒了！图灵-完成。

在实践中，我敢打赌你可以编写一个CBV程序来模拟图灵机；选择一个合适的固定点组合器就足够了，比如Θ。(比较著名的Y组合器只在一种按名称调用的减少策略下工作，即正常降阶。)

免责声明：--我已经很久没学过lambda微积分了，而且我确信上面的论点中有几个细节是错误的。但我对物质很有信心。这不是我第一次在在线资源中发现编程语言理论方面的一些明显错误。

Answer 2

如果没有特定的语言，你的问题就没有多大意义，但是我会尽我最大的努力来回答关于非类型化的Lambda微积分。

一个逐值不动点组合子的存在性。( "Y“)用于非类型化的lambda演算，似乎驳斥了基本的断言(参见：不动点组合器)。这种组合器的存在打破了强大的规范化，这意味着至少有一种语言是图灵完整的，它使用的是按值调用的评估策略。

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