作者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)