2010/08/29

[facebook digest] 公雞暑校

  1. 差不多可以關掉電腦收起來了。有人要猜明天我會多快遇到障礙嗎？XD    [2010-08-18 23:10:09 +0800]
    • F************ ⇒ 1秒鐘,

      因為電腦打不開    [2010-08-18 23:50:31 +0800]
    • 陳** ⇒ 如果我比你早起，我應該會更快遇到障礙XD    [2010-08-19 00:21:38 +0800]
  2. 傳說中的機場上網。目前為止都順利。等到香港或飛北京再開始寫日記。    [2010-08-19 10:03:02 +0800]   [ 3 人說讚！]
  3. 現在在香港機場免費上網。往北京的班機目前宣布慢 50 分鐘⋯（原本兩點起飛。）    [2010-08-19 13:16:55 +0800]
  4. 一個顯而易見的事實是：香港機場還沒開始鎖 facebook XD。    [2010-08-19 13:24:57 +0800]
    • C*************** ⇒ 香港跟澳門的網路基本上都沒有鎖，畢竟這兩個地方是特區    [2010-08-19 13:28:07 +0800]
    • 陳** ⇒ 所以進入內地就不能用囉? XD    [2010-08-19 13:44:54 +0800]
    • Josh Ko ⇒ 到時候用 VPN 試試看 XD。    [2010-08-19 13:45:56 +0800]
  5. 糟了，現在說 15:45⋯    [2010-08-19 13:46:23 +0800]
  6. 香港現在在下雨了，可是還是有其他班機在登機，所以應該不是天候問題？    [2010-08-19 13:57:17 +0800]
  7. 欸，本來說 60 號閘口，現在又說 29 號。這樣得再坐一次地鐵回去⋯    [2010-08-19 13:59:25 +0800]
    • Josh Ko ⇒ 結果不用 XD。    [2010-08-19 14:15:44 +0800]
    • 陳** ⇒ 學長是用iphone在更新fb嗎? XD 感覺相當即時呀    [2010-08-19 17:20:50 +0800]
    • Josh Ko ⇒ 機場免費無線上網 XD。    [2010-08-19 22:55:35 +0800]
  8. 現在換到 gate 21，幸好啓程時間沒繼續往後延。    [2010-08-19 15:06:22 +0800]   [ 1 人說讚！]
  9. 結果 IIS 的 VPN 似乎沒用，現在是用 NTU 的 VPN（courtesy of 前高中同學、現台大醫科六年級學生帳號 XD）。    [2010-08-19 22:23:57 +0800]
    • L********* ⇒ 我之前是用遠端桌面連回家裡電腦 XD
      不然大陸實在太多網站都不能上了…    [2010-08-19 22:31:05 +0800]
    • 王** ⇒ 八成是 施XG？XD    [2010-08-20 14:11:15 +0800]
    • Josh Ko ⇒ Obviously. XD    [2010-08-21 06:56:50 +0800]
  10. 近春園現在上網免費！（不要 check out 的時候才告訴我是亂講的…）    [2010-08-19 22:25:08 +0800]   [ 2 人說讚！]
    • C*************** ⇒ 我之前去北京清華也是住近春園，但是網路超不順的...不知道你會不會也有同樣的狀況...    [2010-08-19 22:26:07 +0800]
    • Josh Ko ⇒ 現在速度還不錯 XD。    [2010-08-19 22:26:34 +0800]
    • L********* ⇒ 基本上應該都免費吧，還沒聽過上網要收錢的，又不是網咖 XD    [2010-08-19 22:28:37 +0800]
  11. 飛機最後四點登機、五點才起飛，機長甚至一度宣布可能五點半才飛，延誤的理由是內陸航班較多。但為什麼排航班的時候沒檢查會不會塞機啊？難道還有臨時插隊的？    [2010-08-19 22:33:49 +0800]
    • C*************** ⇒ 不意外，大陸的國內班機常常會出現delay的狀況....    [2010-08-19 22:42:39 +0800]
  12. 出關已經過九點，我也不想再跟地鐵耗了，直接坐計程車到近春園門口。司機進西門後問路上學生近春園怎麼走，後者回曰（正北京腔）「有這地方嗎？」顯然和台大的情況差不多 XD。    [2010-08-19 22:36:59 +0800]
  13. 北京腔也不見得比英文好辨識，遇到那種腔調很濃的往往都得請他說第二次（特指司機先生），轉換成語意的速度也沒比英文快太多。    [2010-08-19 22:39:00 +0800]
    • L********* ⇒ 北京腔應該算還好的了，其他有的沒的的地方腔調才真的是難辨識 XD    [2010-08-19 23:01:41 +0800]
  14. 經過的北京都是一派商業區的景象，所以第一印象沒有太好 XD。    [2010-08-19 22:48:50 +0800]
    • 陳** ⇒ 那學長對台北的第一印象? XD
      OS:是個國家。(誤)    [2010-08-19 23:22:26 +0800]
  15. 地鐵大概就看回去時有沒有那個興致了 XD。    [2010-08-19 22:54:58 +0800]
  16. 路上招牌的簡體程度沒我預期的高，但同一個簡體字多看幾次（比方說「橋」— 北京這麼多橋？）之後正體會差點寫不出來，滿恐怖的。    [2010-08-19 23:12:14 +0800]   [ 1 人說讚！]
    • F************ ⇒ 這就是所謂的 洗腦教育...    [2010-08-19 23:33:37 +0800]
    • L************** ⇒ 我可以預定些土產嗎？XD    [2010-08-20 02:12:29 +0800]
  17. 早上好想睡，幸好上的是不用腦的東西。Jean-Pierre 講 first-order logic 和 Max PK — Max 樂勝啊 XD。    [2010-08-20 17:31:45 +0800]
  18. 下午就只是在 Coq 裡寫很像 OCaml 的程式，瞬殺完後剩下時間把未來要講的東西看得差不多了 XD。    [2010-08-20 17:33:29 +0800]
  19. 然後被王柏堯老師認出來！    [2010-08-20 17:33:51 +0800]
  20. 中午的炸醬麵鹹到很恐怖，用兩包調味包泡一碗泡麵也沒那麼鹹吧。勉強吃半碗就不行了⋯    [2010-08-20 17:37:17 +0800]
  21. 對了，下一屆公雞學校要移出北京，辦在蘇州！（FLOLAC 也快移出台北搬到墾丁吧⋯）    [2010-08-20 20:16:22 +0800]   [ 2 人說讚！]
    • S************ ⇒ 蘇州是不錯的地方唷，缺點是很悶很熱。    [2010-08-21 18:06:07 +0800]
  22. 現在可以用 Oxford 的 VPN 了，也能成功翻牆！    [2010-08-21 07:09:57 +0800]
    • L************** ⇒ 剛起床？真早 XD    [2010-08-21 07:10:20 +0800]
    • Josh Ko ⇒ 起床一小時了 XD。    [2010-08-21 07:10:40 +0800]
    • Josh Ko ⇒ 然後才想到今天九點才上課 XD。    [2010-08-21 07:11:00 +0800]
    • L************** ⇒ oh. 酷耶 XD    [2010-08-21 07:13:15 +0800]
  23. 吃完飯回來，還不到上課時間就把今天習題（programming with lists）做完了。最後只好寅吃卯糧，把明天的習題（natural deduction）也做掉 XD。Natural deduction 有些題目很好殺時間，比方說 ~~(P \/ ~P) 又成功把我拖住一陣子 XD。    [2010-08-21 17:39:30 +0800]
    • S************ ⇒ 一般學生的反應呢？應該也是覺得水深火熱吧？    [2010-08-21 18:05:24 +0800]
    • 翁** ⇒ 寅吃卯糧<---幸好不是吃過期商品XD    [2010-08-21 19:16:50 +0800]
    • Josh Ko ⇒ 不知道耶，我都坐在最前面最邊邊⋯    [2010-08-21 19:19:43 +0800]
  24. 北京今天下整天雨。清華大學的路下雨天時積水嚴重，十分難走。    [2010-08-21 17:40:53 +0800]   [ 1 人說讚！]
    • 翁** ⇒ 在北京可以看日記嗎XD    [2010-08-21 19:16:10 +0800]
    • Josh Ko ⇒ 噫，你怎麼知道我剛看完 XD。    [2010-08-21 19:19:02 +0800]
    • 翁** ⇒ 所以是盜版摟XD    [2010-08-21 19:33:43 +0800]
    • Josh Ko ⇒ 就 Youtube 啊 XD。    [2010-08-21 19:50:56 +0800]
    • 翁** ⇒ 喔喔~看是看live好~(茶    [2010-08-21 19:55:47 +0800]
  25. 今天一節課專門講 induction，果然又有人問 induction principle 怎麼證（永遠是個好問題）。    [2010-08-21 19:20:56 +0800]   [ 1 人說讚！]
    • S************ ⇒ 老師怎麼回答呢？    [2010-08-21 20:19:41 +0800]
    • 陳** ⇒ 我也有這個問題(舉手)    [2010-08-21 23:50:47 +0800]
    • Josh Ko ⇒ 他說 induction 是「用 uniform 的方式產生無窮多個證明」。問題丟出來之後他先循他剛才的理路多解釋一點，然後說他可以用很精美的數學理論去證，但在某個階段一定會用到不比 induction 弱的原則，而且也不會比他這樣直覺解釋更具說服力。    [2010-08-22 07:31:22 +0800]
  26. 終於吃到家鄉味了⋯（康師傅香菇燉雞麵）    [2010-08-22 17:05:32 +0800]
    • L********* ⇒ 康師傅應該不算家鄉味唷，除了是從大陸紅回台灣的之外，普遍台灣人都覺得很難吃 XD    [2010-08-22 21:16:19 +0800]
  27. 今天繼續講 structural induction，中間拐到 (N, <) 上的 well-founded induction，最後還把 accessibility 的 general form 貨真價實地寫出來。講者離開一般數學表示、寫出 "Inductive Even : nat -> Prop := E0 : Even 0 | E2 : forall n, Even n -> Even (S (S n))." 和它上面的 induction principle 時一堆人都怒了：哪有把 predicates 硬拗成 datatypes 的道理！    [2010-08-22 17:26:58 +0800]   [ 1 人說讚！]
  28. 剛才用 Agda 寫能過 termination check 的 "merge"（需要在 List A * List A 上造出簡單的 well-founded relation），語法上比想像中討厭很多。    [2010-08-22 19:15:31 +0800]   [ 1 人說讚！]
    • L************** ⇒ 當初 Coq 最麻煩的事情就是記住語法跟 tactic 的用途 ... XD    [2010-08-22 19:18:45 +0800]
    • Josh Ko ⇒ 可是我是用 Agda... Coq 好像簡單一點 XD。    [2010-08-22 19:19:28 +0800]
    • Josh Ko ⇒ Coq 可以隨時做 pattern match (induction) 也可以指定（只）對誰做，在 Agda 裡就得一直把中間的 functions 拉出來寫。像我要先對 xs 做 induction，兩個 cases 裡面再分別對 ys 做 induction，這樣得寫三個 mutually-recursive functions，一個 induction on xs, 去呼叫另外兩個 induction on ys 的 functions。然後 accessibility 的 constructor 拿的參數是個 function，又得再用 where 拉出來寫⋯    [2010-08-22 19:33:14 +0800]
    • L************** ⇒ 但是 Agda 的語法雖然麻煩但是比較單純，但是 Coq 剛好反過來，有些偷吃步但是比較複雜 ...    [2010-08-22 19:41:03 +0800]
    • S************ ⇒ 我以前有試證過這個函數會 terminate:
      f k n with k ≤? n
      ... | yes _ = n
      ... | no _ = f k (f k (suc n))
      超難證的。
      http://www.iis.sinica.edu.tw/~scm/2008/well-founded-recursion-and-accessibility/
      也許在 Coq 裡面會比較簡單？

      所以後來有人改用 coinductive type, 把 termination 分開來證。    [2010-08-22 22:00:24 +0800]
  29. 食堂的餃子是用「兩」為單位，超炫！昨天中午吃二兩有點少，今天中午吃三兩剛好飽。    [2010-08-22 19:39:00 +0800]   [ 1 人說讚！]
    • Josh Ko ⇒ 服務生都是徒手估量，沒有用秤。    [2010-08-22 21:05:06 +0800]
    • 陳** ⇒ 這樣對想減肥的女性同胞或許是好事? XD    [2010-08-23 12:38:25 +0800]
  30. 今天下午又把後天的 first-order logic tautologies 和簡單的 program reasoning 做完了，時間還早，就先離開去逛清大。今天天氣非常好，唯一失算的是我忘記今天星期日，人超多。（不知道週間人會不會比較少就是了。）    [2010-08-22 21:02:30 +0800]
  31. 又有一屆社會役學弟要考試啦：定期會看到從 Yahoo 來的「社會役考題」之類的關鍵字，連到下面這篇。可是這篇明明是 IELTS 的模擬考，頁面右上方的名片也拿掉社會役很久啦，只能說 Yahoo 更新真慢 XD。 ↦ Trek through Pure Reason: 第一次模擬考    [2010-08-22 21:09:44 +0800]
  32. I've got a roommate from Malaysia, who seems to have met Shin for a few times! Later we are going to solve an interesting problem posed by him together.    [2010-08-23 20:19:59 +0800]
    • 陳** ⇒ 這是為了友善室友，所以發英文的嗎XD    [2010-08-23 20:37:33 +0800]
    • Josh Ko ⇒ 因為剛才講很多英文，一時轉不回來 XD。    [2010-08-23 20:58:46 +0800]
    • S************ ⇒ 喔喔？是誰呀？    [2010-08-25 11:32:34 +0800]
    • Josh Ko ⇒ Kim-Ee Yeoh. 不知道有多熟？    [2010-08-25 20:38:47 +0800]
  33. 頤和園還真大，人又多，背著 MBP 15"、KDX、Coq'Art 中文版和其他拉里拉雜的東西走，一下子就累了 XD。    [2010-08-23 21:14:38 +0800]
    • 翁** ⇒ .....去看風景只需要帶相機= ="你帶那麼ˊ多亂七八糟的東西幹嘛    [2010-08-23 21:19:57 +0800]
    • Josh Ko ⇒ 練體力⋯ XD    [2010-08-23 21:53:55 +0800]
    • 翁** ⇒ 長城在等你    [2010-08-23 22:44:57 +0800]
  34. 昨天晚上聚餐，旁邊的人說我的口音很明顯就是南方人，我也這麼覺得。在這裡我就是快樂的小僑生了，身體好、精神好、愛清潔、有禮貌⋯ XD    [2010-08-24 19:22:51 +0800]   [ 2 人說讚！]
  35. Professor Lévy 的 λ-calculus 飆得超快，還有人直接舉手跟他說「我們都跟不上你，不信你叫這裡跟得上的人舉手」。今天證畢 Church-Rosser 定理（用 Martin-Löf 的 parallel reduction），下午想用 Agda 證一遍但又被名字卡住了。    [2010-08-24 20:57:10 +0800]
    • S************ ⇒ 大陸學生上課都那麼嗆呀..?    [2010-08-25 11:30:45 +0800]
    • S************ ⇒ 「證畢 Church-Rosser 定理」是手證還是 Coq 證明呀？    [2010-08-25 11:31:49 +0800]
    • Josh Ko ⇒ 投影片證，刷刷刷就過去了。    [2010-08-25 20:36:34 +0800]
  36. 中午探勘到地鐵站的路。北京的 KFC（不是 ZFC）有專人幫你收盤子耶。    [2010-08-26 18:29:56 +0800]
    • F************ ⇒ 因為在那邊KFC算高級餐廳了!?    [2010-08-26 20:29:38 +0800]
    • Josh Ko ⇒ 有可能，我看到價錢時有嚇到 XD。    [2010-08-26 22:08:43 +0800]
    • F************ ⇒ 鼎泰豐出面聲明: 我們在大陸最大的勁敵就是KFC阿! (嘶吼~    [2010-08-26 22:21:10 +0800]
  37. 現在猶豫到底要自找麻煩坐地鐵到機場還是花大錢坐出租車省事。    [2010-08-26 22:08:08 +0800]
    • L********* ⇒ 北京好像還沒有磁浮？有的話推薦體驗一下，雖然真的頗貴…    [2010-08-26 22:22:24 +0800]
    • F************ ⇒ 租車坐到地鐵站去坐地鐵    [2010-08-26 22:25:31 +0800]
    • Josh Ko ⇒ 其實也是一種可能，坐到「機場快鐵」的起點（可是不知道司機會不會擺臭臉 XD）。    [2010-08-26 22:26:45 +0800]
    • L************** ⇒ 坐個地鐵體驗一下人生。    [2010-08-26 22:50:10 +0800]
    • F************ ⇒ 擺臭臉就說: 你爸讓你這10分鐘有錢賺,還不感激我!?    [2010-08-26 23:29:39 +0800]
    • Josh Ko ⇒ 結果有個講師剛好也是差不多時間的飛機，就搭伙叫車去機場了 XD。    [2010-08-27 18:58:50 +0800]
  38. 原來日本的人已經參考 AoPA 把 equational reasoning syntax 移植到 Coq 上啦。（不過只有 functional derivation，也沒看到什麼非玩具的例子。）從 Coq 的對照觀點來看，Agda 有趣的地方應該是在於寫程式和證明是完全對稱的活動，寫證明有的輔助功能也能很自然套用在寫程式上。在 Coq 裡寫程式就得不到什麼幫助，特別 dependently-typed programs 寫起來極為痛苦。但 Agda 的自動化程度和 Coq 實在相差太遠，如果是走「寫好一般程式再寫證明」這條進路，Coq 很明顯是比較適合的工具。現在我們在 Agda 上做那麼複雜的證明真的是自討苦吃，到時候假設 paper 寫出來，其中一個 review comment 一定是說為什麼不在 Coq 上做吧。 ↦ http://www.univ-orleans.fr/lifo/prodsci/rapports/RR/RR2009/RR-2009-07.pdf    [2010-08-26 22:23:31 +0800]   [ 1 人說讚！]
    • S************ ⇒ 是 Hashimoto 和 Hu 的那個，對嗎？Hashimoto 就是我在日本那年遇到的碩士生。    [2010-08-27 08:47:56 +0800]
    • L*********** ⇒ 我不熟悉證明，但如果寫程式即證明，不是比較省事嗎？ :p 或許只是成熟度問題？    [2010-08-27 16:21:52 +0800]
  39. 公雞暑校結束嘍。    [2010-08-27 18:59:19 +0800]
  40. 最後一天晚上，看了傳說中的新聞聯播。    [2010-08-27 19:31:25 +0800]   [ 1 人說讚！]
  41. 剛才出西門覓食（飯卡被收回去了），過馬路就到圓明園，但怎麼看都沒有能吃的東西，最後回西門南側買到一張煎餅。（還聞到臭豆腐的味道，但來北京吃臭豆腐不對吧 XD。）北京的車不讓行人又猛按喇吧，馬路差點過不去⋯    [2010-08-27 20:53:56 +0800]
  42. 安全抵達香港。在北京飛機等跑道權等好久，跑道上飛機升的升降的降，跑道旁排隊的飛機愈來愈多。半小時後輪到我們，機長把飛機轉上跑道，機頭都還沒對準，引擎就催下去了。這趟飛行好像比來程顛簸一點。（現在馬上又要登機了，其他事到家再補。）    [2010-08-28 17:40:37 +0800]   [ 1 人說讚！]
    • 疏*** ⇒ ＝ ＝ 香港 我在這耶 學弟來給我拜個碼頭喔    [2010-08-29 00:20:16 +0800]
    • Josh Ko ⇒ 我只有到香港轉機啦，現在已經在台灣了 XD。    [2010-08-29 01:45:01 +0800]

--
應該還會有別篇寫公雞暑校。

Labels:

posted by Josh Ko @ 2:27 am   0 項意見