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演算不能編碼一個固定點組合器,並且強烈歸一化(即所有良好類型的項減少到一個值),然而,這與所採用的評估策略無關,這是真實的。相反,這是類型系統的結果。