※ 引述《xcycl (XOO)》之銘言：
: 且所有的程式都要能夠 typable 的話，就會有些 λ-term 無法在系統下定義，
: 範例如上。所以也就有可計算的函數，無法在該系統下寫出來。
: 對 Haskell 來說，所有的 type 都有一個 undefined 元素，所以並不是一致，
: 但剩下如 C, C++, Java 這些來說呢？
: 不過我不大瞭解 type theory 跟 imperative language 要怎麼能夠
: 學理上的陳述，或許 C\C++, Java 上的 type system 性質並不完全一樣？
Hmm... 一般來說「某語言是 Turing complete」的證明
確實是就用這個語言去模擬 Turing machine。通常也不
難看出這個程式確實模擬了 Turing machine, 所以都還
不至於有什麼 surprise。
不過你說的是 C\Java 是不是一致的。這倒是沒細想過。
一般「不一致」的意思是所有 type (proposition) 都
有一個 term (proof), 連 bottom (false) 都有 term.
但
1. 不知道 C\Java 的 type 裡面有沒有 bottom 這種說法。
2. 另外，在 Haskell 裡
undef = undef
可以有任何 type. 在 C/Java 裡有這種可以有任何
type 的程式嗎？
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 114.183.110.251