[問題] 程式語言大部分是 Turing Complete 的嗎？

[xcycl (XOO)]

基本上，好像都認為程式語言必須是 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
推 ykjiang:這個只要來個思想實驗就行了，例如以 C 寫個 TM ，
→ ykjiang:C 寫個 TM 根本毫無困難，故得證
→ xcycl:在 C 裡頭寫個 TM 跟 C 語言是 Turing 完備一樣嗎？
→ yllan:一樣啊，只要可以寫 UTM 就是 Turing-Complete 啊～