7

我正在阅读一篇关于不同evaluation strategies的文章(我在wiki中链接了文章,但是我正在阅读另一篇不是英文的文章)。并且它说,与call-by-namecall-by-need策略不同,call-by-value策略是而不是Turing complete为什么按价值评估策略不是图灵完整的?

有人可以解释一下,为什么?如果可能的话,添加一个例子。

+0

哪篇文章? _ – kennytm 2010-05-31 15:08:49

+0

@KennyTM:我试图在文章结尾的引用中找到源代码。如果你愿意,我可以给你一个链接,但它是用俄语。 – Roman 2010-05-31 15:13:33

+2

俄罗斯的文章总比没有好。不是我,但有人可能会读俄语。 – kennytm 2010-05-31 15:22:57

回答

10

我在您正在阅读的文章中对索赔提出异议。 (我没有为此付钱,所以我会提供一个暗示性的论点,而不是证明。)

众所周知,至少在正常顺序降低(又名呼叫)的情况下,纯lambda演算是图灵完备的。但是如果我们看看约翰雷诺兹的开创性论文Definitional Interpreters for Higher-Order Programming Languages,我们可以看到雷诺兹详细讨论了名义上的呼叫和价值上的呼叫之间的区别。论证的一个关键部分是,为了做出适当的区分,我们可以将程序转换为延续传球风格。 CPS变换对于按需调用和按值调用是不同的,但可以用任一风格来评估生成的变换术语。

所以这里有一个参数:写一个模拟一个图灵机的lambda-calculus程序,然后CPS使用CBN变换对它进行变换,并且可以使用CBV降低策略评估结果代码。砰!图灵完备。

实际上,我敢打赌,你可以写一个CBV程序来模拟图灵机;例如,选择合适的定点组合器就足够了,例如Θ。 (更有名的Y组合器只能在按名称缩减策略下工作,即正常顺序缩减。)

声明:我没有研究过年龄段的lambda微积分,我确定有在上面的论点中有几个细节是错误的。但我对实质有信心。这不是我第一次发现在线资源中有关编程语言理论的公然错误。

0

没有参考某种特定的语言,您的问题没有多大意义,但我会尽我所能回答关于非类型化Lambda演算。

对于无类型lambda演算,存在按值定值的固定点组合器(即“Y组合器”)似乎反驳了基本的声明(请参阅:Fixed Point Combinator)。这样一个组合器的存在打破了强大的标准化,这表明至少有一种语言是完整的,使用逐个价值评估策略。

更可能影响语言的图灵完备性的是存在(或缺少)类型系统。例如,简单类型的lambda演算不能编码一个固定点组合器,并且强烈归一化(即所有良好类型的项减少到一个值),然而,这与所采用的评估策略无关,这是真实的。相反,这是类型系统的结果。