作者noctem (noctem)
看板PLT
标题Re: [问题] 程式语言大部分是 Turing Complete 的吗？
时间Thu Jun 25 18:44:45 2009
※ 引述《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