基本上，好像都认为程式语言必须是 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