[問題] 程式語言大部分是 Turing Complete 的嗎？
基本上，好像都認為程式語言必須是 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
推
06/25 10:51, , 1F
06/25 10:51, 1F
→
06/25 10:52, , 2F
06/25 10:52, 2F
→
06/25 11:46, , 3F
06/25 11:46, 3F
→
06/25 11:54, , 4F
06/25 11:54, 4F
討論串 (同標題文章)
以下文章回應了本文：
完整討論串 (本文為第 1 之 6 篇)：
PLT 近期熱門文章
PTT數位生活區 即時熱門文章
