作者noctem (noctem)
看板PLT
标题Re: [心得] Fixed-points, Curry-Howard, etc.
时间Fri Apr 27 22:01:54 2007
Hmm... 我不是很确定懂了buganini的意思啦。讲些可能相关的好了。
不过对於这些东西,我知道的大概也是多看几遍 wikipedia 的程度
而已。请先进指正。
首先是 Church-Turing Thesis. 一般的版本是:
任何可计算的(computable)函数都可用 Turing machine 算出来。
但其实「可计算」这个概念本来就是模糊的,现在我们其实是用
Turing machine 当作它的定义: 「可计算的函数」的定义就是
「Turing machine 可以模拟的。」Church-Turing thesis 其实是
说:这样的定义是合理的,和我们的直觉相符。人类可以计算出来
的东西,就是有个演算法、在有限的步数里面,用 Turing machine
可以算的东西。使用参禅等等方式得到的就不算了。 :)
(有比 Turing machine 更强的计算 model 吗?有的,比如说
如果我们可以有真正的 real number, 或着每一步可以得到一些
oracle 等等。但这些都是假想中才存在的机器。即使是量子电脑,
也仅能比较快地解出一些问题,而不能解出 Turing machine 解
不出的问题。)
Turing machine 还是有些无法解的问题。哲学上我们就相信这是
人类理性的限制了。不过也有人还是说,剩下的东西就是禅啦,
或着是神的力量等等的...
* * *
这一系列研究是跟在 Godel 的 incompleteness theorem 之後而来的。
Hilbert 等等数学家为了解决悬宕已久的一些数学矛盾,决定把
数学以严谨的方式重建起来,希望有一套方法能告诉我们任何一个
陈述是真或假。Godel 告诉我们不可能。
但这要看你决定用什麽样的抽象方式来看世界。如果你关心的问题
只用 propositional logic 就可以描述,那没问题。(有些朋友知
道逻辑有很多套时蛮惊讶的。其实数学逻辑也是人发明的,在什麽
情境,哪套逻辑合用,就用那套。)Propositional logic
确实是完备的,任何陈述要不然就有个证明要不然就有个反证。
如果你想描述「对所有的x」、「存在某个 y」等等,你就得用
predicate logic. 那麽情形就没那麽完美了。所有为真的陈述还是
有证明(这其实也是从 Godel 的「完备」定理来的。Godel 有个
不完备定理,也有个完备定理 :))。但这个证明不见得能在有限时
间内找得到。你如果一直找某个陈述的证明找不到,你也无法知道它
倒底是真是假。
如果你需要表达能力更强一点的系统,那情形就更遭。Godel 告诉我
们的是,如果一个(consistent的)理论系统强到可以描述算术,那
麽它就注定是不完备的。一定会有些陈述是真的,但却没有证明。
(Consistency 是一个要注意的要求。通常不管什麽逻辑,我们会
要求 p 和 not p 不可以同时有证明。否则他就 inconsistent。通
常这时候我们会觉得是这个系统设计有问题了。前一篇我便提到,
如果加入 (a -> a) -> a 这个公设,任何东西都证得出来。)
有了这样的基础之後,Turing 等人继续定义所谓可计算是什麽意思,
想知道数理系统的限制在哪里。
但不完备定理也不能过度引申。有些东西没有证明,但并不表示
有证明的东西会是错的。也不表示这个系统不 consistent
(这可能有点回应到 buganini 的一些句子。「因果」如果理解成
前提对,结果就会对,那因果还是在的。)
此外,有些定理没有证明。但这些定理重不重要呢?早期我们能举
出的没有证明的定理,其实大多是尝试「自己讲自己」的定理。
他们结构都很像,唯一的用处好像也只是当反例而已。直到後来终
於有了几个有趣的例子,例如「polymorphic lambda calculus 会
终止」这件事情。
而同时我们为了各种需要,也仍在使用各种更复杂的逻辑。可以
描述先後的逻辑(p 为真,直到 xxx 时候)啦,可以描述资源
使用的逻辑啦(所有前提只能被使用一次),等等...
--
※ 发信站: 批踢踢实业坊(ptt.cc)
◆ From: 123.192.157.71
※ 编辑: noctem 来自: 123.192.157.71 (04/27 22:08)