Re: [心得] Fixed-points, Curry-Howard, etc.

看板PLT (程式語言與理論)作者xcycl (XOO)時間15年前 (2009/06/09 04:07)推噓0(0推 0噓 0→)

留言0則, 0人參與討論串4/4 (看更多)

※ 引述《noctem (noctem)》之銘言： : 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 解 : 不出的問題。）有的，可以參考一下這篇 paper http://www-2.cs.cmu.edu/~lblum/PAPERS/TuringMeetsNewton.pdf 試著將 TM 拓展到一般的 ring 結構上，這樣使得對複數以及實數等系統，也有相對應的計算模型。這篇是很有趣，但是書看起來就很悶了 ... : Turing machine 還是有些無法解的問題。哲學上我們就相信這是 : 人類理性的限制了。不過也有人還是說，剩下的東西就是禪啦， : 或著是神的力量等等的... : * * * : 這一系列研究是跟在 Godel 的 incompleteness theorem 之後而來的。 : Hilbert 等等數學家為了解決懸宕已久的一些數學矛盾，決定把 : 數學以嚴謹的方式重建起來，希望有一套方法能告訴我們任何一個 : 陳述是真或假。Godel 告訴我們不可能。這點有人以為只有人造（？）的問題，才會遇到這種問題，實際產生的問題不會遇到。但很可惜的是，在比較抽象的代數理論，就會遇到了。參見 Whitehead problem： http://en.wikipedia.org/wiki/Whitehead_problem : 但這要看你決定用什麼樣的抽象方式來看世界。如果你關心的問題 : 只用 propositional logic 就可以描述，那沒問題。（有些朋友知 : 道邏輯有很多套時蠻驚訝的。其實數學邏輯也是人發明的，在什麼 : 情境，哪套邏輯合用，就用那套。）Propositional logic : 確實是完備的，任何陳述要不然就有個證明要不然就有個反證。 : 如果你想描述「對所有的x」、「存在某個 y」等等，你就得用 : predicate logic. 那麼情形就沒那麼完美了。所有為真的陳述還是 : 有證明（這其實也是從 Godel 的「完備」定理來的。Godel 有個 : 不完備定理，也有個完備定理 :)）。但這個證明不見得能在有限時 : 間內找得到。你如果一直找某個陳述的證明找不到，你也無法知道它 : 倒底是真是假。 : 如果你需要表達能力更強一點的系統，那情形就更遭。Godel 告訴我 : 們的是，如果一個（consistent的）理論系統強到可以描述算術，那 : 麼它就註定是不完備的。一定會有些陳述是真的，但卻沒有證明。 : （Consistency 是一個要注意的要求。通常不管什麼邏輯，我們會 : 要求 p 和 not p 不可以同時有證明。否則他就 inconsistent。通不希望 inconsistent 有一個理由是，在 natural deduction 系統下，同時存在 p 跟 not p 會使得，會推得 absurdity, \bot，而這可以推出任何的陳述。就算從語意來看，也就是用真值表來看也是，一旦前提為否，接下來的任何陳述不管是什麼，都是真。 : 常這時候我們會覺得是這個系統設計有問題了。前一篇我便提到， : 如果加入 (a -> a) -> a 這個公設，任何東西都證得出來。） : 有了這樣的基礎之後，Turing 等人繼續定義所謂可計算是什麼意思， : 想知道數理系統的限制在哪裡。 : 但不完備定理也不能過度引申。有些東西沒有證明，但並不表示 : 有證明的東西會是錯的。也不表示這個系統不 consistent : (這可能有點回應到 buganini 的一些句子。「因果」如果理解成 : 前提對，結果就會對，那因果還是在的。） : 此外，有些定理沒有證明。但這些定理重不重要呢？早期我們能舉 : 出的沒有證明的定理，其實大多是嘗試「自己講自己」的定理。 : 他們結構都很像，唯一的用處好像也只是當反例而已。直到後來終 : 於有了幾個有趣的例子，例如「polymorphic lambda calculus 會 : 終止」這件事情。 : 而同時我們為了各種需要，也仍在使用各種更複雜的邏輯。可以 : 描述先後的邏輯（p 為真，直到 xxx 時候）啦，可以描述資源 : 使用的邏輯啦（所有前提只能被使用一次），等等... modal logic 嗎？ -- ※ 發信站: 批踢踢實業坊(ptt.cc) ◆ From: 123.193.218.153