zh-tw:talks [2012 Formosan Summer School on Logic, Language, and Computation (FLOLAC '12)]

Invited Talk

08/30: 給電腦科學家的邏輯系統

  • Lecturer: 侯昆邦 Kuen-Bang Hou (Favonia). 卡內基美隆大學電腦科學系博士生。
  • Title: 給電腦科學家的邏輯系統
  • Date & Time: 2012/08/30, 1:20 pm.

在二十世紀初的數學基礎論戰之後,古典邏輯與集合論取得數學界正統地位。後來電腦興起,不少數學結果都被重新分析是否適合由電腦計算,許多領域也隨著這股潮流成為當紅領域,包括演算法和計算理論。例如納許早已用古典邏輯證明了非合作賽局中有平衡點,但在電腦上最好的計算方法還在未定之天。這場變遷當中,直覺邏輯與型態論正悄悄的隨著程式語言再次復活。這次講座將介紹直覺邏輯和型態論在電腦科學中的優勢,以及他們可能可以帶來的啟示。

講者表示

這次很高興可以回國演講;演講中有許多人踴躍回應,讓我非常開心。比較遺憾的是,現場很多好問題我都沒有給出好答案。為此我希望這篇文章有點幫助。

此外,我記憶力非常差,所以如果有人沒看到自己問的問題,又不太懂我當時在回答什麼,不要懷疑,是我忘了,請寫信提醒我!我會持續搔擾助教把最新版本擺到網路上。

有些學過微積分甚至高微、複變的同學問我他們以前學的東西是不是要整套丟掉。比較正經的答案是,已經有許多人努力按照直覺邏輯(或構造邏輯)重建部份數學分析,但我不是這方面的專家,不知道目前最新發展如何。我在演講中只有提到一點點最簡單的結果當開胃菜,有興趣的人可以搜尋「constructive analysis」或「computatable reals」。這領域已經有不少有趣的結果:舉例來說,雖然原版的中間值定理不很「構造」,但你可以找到另一個版本的中間值定理,在古典邏輯中等價於原版,在直覺邏輯中又可以證明。由此,我傾向認為如果我們想擁抱構造原則,數學分析確實需要從頭徹底檢視,但不會變得價值全無;至少它可以成為構造版本的理論的嚮導。

啊,是的,直覺主義(廣義上來說)是一種構造主義,然後構造主義不是直覺主義,但兩個主義的支持者大概會支持一樣的(形式化)邏輯系統,所以直覺邏輯也有人叫構造邏輯。如果你只想要學形式化的邏輯系統或程式語言,可以暫時忽略這些主義的差異沒關係。

另外有人問我,在「真的」的程式裡,最終還是要給出一定位數(轉成有限長)不是嗎?其實不是,你可以把逼近演算法本身當作數字的定義,而且早已有人實作可以用的函式庫。有興趣的人可以搜尋「exact real arithmetic」。

還有有人問,給定 0 和 0.01 可以判斷大於 0 或小於 0.01, 但如果 0.01 是以(編碼後可能無限長的)實數給演算法,演算法不是連是否大於零都不知道嗎?這裡有很多解決辦法,不過我想最簡單的方法是 0 和 0.01 (上下界)都用有理數的形式給演算法就好了。

有人問為什麼跟直覺主義呼應的形式系統就有對應關係。撇開我避而不談的各種哲學假設,有幾點我想說清楚:首先這只是我個人經驗膚淺的觀察而已;再來,即使是同一組概念,也可能用(形式上)沒有完美對應的兩個形式系統出現(例如直覺線性邏輯和沒改造過的 process calculus);最後,我所觀察到能對應的形式系統,都是和直覺主義中同樣的概念相呼應。我不覺得和不同組概念呼應的形式系統容易有對應關係。

這次演講主要還是從實用的角度出發,哲學上討論非常少,有點可惜。根本原因是因為我哲學底子不夠,不管看多少資料還是不太敢大放厥詞。不過有一點確定的是,我並不認為 Brouwer 真的全在胡說八道,不然也不會花這麼多力氣幫他平反。如果有人把我演講結束後的玩笑話當真… 先說抱歉了 :P

09/06: Gödel's Incompleteness Theorem

  • Lecturer: 董世平。 中原大學應用數學系, 中原大學理學院院長。
  • Title: Gödel's Incompleteness Theorem
  • Date & Time: 2012/09/06, 1:20 pm.

In this talk we will first introduce the background of Gödel’s Incompleteness Theorem. We then will explain the meaning and the ideas of the proof this theorem. Finally, we talk about it’s impact on Mathematics, Computer Science, and Philosophy.