基本上，好像都認為程式語言必須是 Turing complete 的， 除了少數比較特別的語言，或是特殊用途的以外。 而一般認為的語言像是 C++, Java, 或是 Haskell 之類的, 都是 Turing complete 的。但有個問題是，這是有證明的嗎？ 疑問來自於，首先知道 Turing machine 跟 lambda calculus 是等價的， 而 lambda calculus 中能夠寫出 fixpoint operator, 也就是 Y combinator, 定義如下 Y = λf·(λx·f (x x)) (λx·f (x x)) 可以經由 β-reduction 得知對任何 λ-term F 而言, 具備 F(YF) = YF 的性質, 所以得到 Y 是一個 fix point 的運算。 然而，若是引入 type system 之後，Y 的型別會變成是 (a -> a) -> a 根據 Curry-Howard isomorphism 來說, 這個系統變成不一致的, 因為從 Y 的 type 跟常數函數, 可以得到 a <-> (a -> a) 這樣的陳述, 將 a 套入 False 之後，會得到 False <-> (False -> False) = True 也就推出矛盾。 所以會得到，如果若程式語言的型別系統要是一致的， 且所有的程式都要能夠 typable 的話，就會有些 λ-term 無法在系統下定義， 範例如上。所以也就有可計算的函數，無法在該系統下寫出來。 對 Haskell 來說，所有的 type 都有一個 undefined 元素，所以並不是一致， 但剩下如 C, C++, Java 這些來說呢？ 不過我不大瞭解 type theory 跟 imperative language 要怎麼能夠 學理上的陳述，或許 C\C++, Java 上的 type system 性質並不完全一樣？ --

※ 發信站: 批踢踢實業坊(ptt.cc) ◆ From: 140.109.16.218