Knaster-Tarski Theorem

Knaster-Tarski theorem is a simple but powerful fixpoint theorem in order theory. It could give a very elegant proof of Cantor–Bernstein–Schroeder theorem which states that if there are injections and , there exists a bijection between A and B.

烏龜游泳意外迅速

離開台灣即將兩個禮拜，好像沒什麼不一樣，但一切都已經改變了我曉得。對著鏡頭看到的畫面，可能是一年後才有機會再觸摸的，而在這邊的一切，則是我一直追求的另外一半。

雖然待的科系是 Computer Science，但是主題其實很數學很邏輯，正在看得論文是有關於近代 Stone duality 的發展，人們試圖從古典的結果，推廣到近代新的工具上面一旦完成，就會有個統一的理論串起所有古典定理的變形。並且能夠模組化地取得須要的邏輯系統。使用的工具基本上是近三四十年來發展的東西，Category theory 以及數學上經典的工具：代數以及拓樸。我光是在看這之間的函子跟範疇間對偶來對偶去的，就快要昏頭了。

不過很美的是，空間跟代數結構兩者之間，竟然在範疇論的意義下互為對偶相等。

我好像要接觸這領域稍嫌年輕而且學得還不夠，但在這種動力之下，好像什麼都學得特別快，洗個澡就順便畫出 adjunction 了。站著似乎血液循環比較好。希望速度夠快能夠讓我有些進度。

近日概況

Ph.D at University of Birmingham 申請上了，領域是 theoretical computer science 中的 coalgebraic logic，有獎學金大概夠活還能存一點錢。希望能夠順利畢業，做出東西來。

KKBox …

之前聽台北愛樂，很討厭他們的廣告，轉去聽 BBC radio 3，結果今天中午不知道怎樣連不上，一直回報我的頻寬不夠；連院內的 NAXOS 資料庫也只限定某兩個所才能用，極其絕望之下想到還有 KKBox ，試聽 30 秒之後就把信用卡拿出來結帳刷了一個月。曲子雖然不完整，但是選擇的範圍還頗大的，討厭 DRM 還是買來用了 …

北京的交通

這邊捷運叫做地鐵（其實大部份的地方也都叫 subway），從路線圖來看目前總共有 123 個站包括重複的轉運站，在四環（以故宮天安門為中心的環狀道路）以內，配合公交車（公車）大概沒什麼地方去不了。2015 年的規劃圖來看的話，大概喊得出名字的地方以後都去得了。另外，從首都國際機場內，就有機場地鐵直達其中十號線的三元橋站跟二號線東直門站，再轉車出去還滿方便的。除了等車的時間較長，但是速度大概是最快的一個。

費用的話，地鐵不限距離，統一價 2RMB；機場地鐵則是 25RMB；公交車投現 1RMB，用一卡通則是0.4RMB，依照路線不同售價不大一樣。北京的物價跟台北差不了多少，但是換算成台幣來看，便宜的很。使用率頗高，每次去大概都擠滿滿的。計程車起價 10RMB，比台灣便宜滿多的，路上也很好招到。

在這邊雖然汽車很多，但我發現這邊沒有機車，只有電動腳踏車，就是可以充電也可以用腳踩發電的，沒有廢氣問題。在市中心部份的公交車，是用電纜驅動，也沒有廢氣……..。實際上在北京的街頭感覺空氣比台北好很多，查資料才寫以前受空氣污染影響很大，現在做得倒挺好的。台北市街頭的空氣品質則是不敢領教 ……

我只能說，台灣要多加油 …

Asian-Pacific Summer School on Formal Methods

下午剛結束在北京輕學大學的暑期課程之旅，來之前記得最原始 Coq Summer School，但後來叫做 Asian-Pacific Summer School on Formal Methods，顧名思義以正規方法來處理軟體的問題為主，講師們都從法國 INRIA 來。

Coinductive Proof ?

正在看 Coq’Art 最後的 Infinite Objects and Proofs，順便玩一下 coinductive type 到底在 Coq 跟 Agda 這種基於 constructive type theory 的語言到底是怎麼回事，用 Agda 內建的  Data.Conat 寫下了幾個證明。先定義 bisimilar relation：

歸謬證法反證法？

反證法是指用 RAA, 或是證明否逆命命題, 或是排中律證明的。而用 law of contradiction 並不是反證法，因為在構造式證明中， Law of contradiction 是成立的，而 RAA 則是構造式證明中唯一被拿掉的公設。證明如下：

掛病號

半盒褪黑激素跟鎮定劑以及兩個禮拜觀察期 …

回來順便去 Working House 買一個小檯燈，40w 鹵素燈泡八點以後就關掉日光燈管換昏黃的燈泡，希望這次能有效解決這問題。_A_

失眠夜

最近一直都睡不好，晚上到了精神就越來越好，太陽一出來就開始睡到中午。實際的睡眠時間大概只有六個小時左右，接下來就是一直昏昏沉沉到晚上，然後完成一個循環。

試過的辦法有，

1. 看書。不管是看什麼類型的書，都只會讓我更有精神 …昨天晚上還把 monad 複習了一遍，翻了一下 monoidal category 跟 strong monad
2. 聽英文廣播。以前聽不懂的話應該很好用，不過現在 BBC Learning English 區塊都已經不用看 transcript，而 world service 的廣播開始聽懂七成左右，越聽越覺得有進步就越興奮
3. 閉眼釘在床上。然後腦袋就開始想事情，然後就起來寫寫程式，或是上網看資料找找看 …
4. 乾脆不睡，明天早點睡。希望這個有效，我現在準備要去睡 …