2010/08/05

facebook digest (2010 June - July)

第一集 facebook digest 特別長。我是直接抓 https://graph.facebook.com/Josh.HS.Ko/feed 的內容下來，再用 parsec 解析成 Haskell datatypes 繼續處理（第一次用 parsec!）。回應的人名第二字以後都遮掉，如果有人覺得這樣還不夠請告訴我。這樣似乎沒辦法把所有 comments 和精確誰按讚找出來，如果用 godfat 的方法就可以嗎？

  1. facebook 超恐怖超複雜…    [2010-06-19 23:26:19 +0800]
    • W************ ⇒ 明天開哪家?    [2010-06-19 23:39:08 +0800]
    • Josh Ko ⇒ 我有時候真的會上去看今天開哪家、會計處吃什麼…    [2010-06-19 23:43:37 +0800]
    • 翁** ⇒ 開大苑子!已經決行了!    [2010-06-20 00:45:51 +0800]
  2. 把 scm 的塗鴉牆全部瞄過一遍了。    [2010-06-20 00:31:05 +0800]
  3. 兩年前寫在 blog 上的筆記救了我… http://joshkos.blogspot.com/2008/05/thoughts-on-greedy-theorem.html ↦ Trek through Pure Reason: Thoughts on the Greedy Theorem    [2010-06-21 14:55:11 +0800]
  4. 從 binary search 發現似乎可用 topology 的東西（但其實是在代數導論聽到的），然後好像不行，後來好像又可以而且更簡單。再磨一下 XD。 ↦ Real projective line - Wikipedia, the free encyclopedia    [2010-06-22 18:54:59 +0800]
    • L************** ⇒ http://math.andrej.com/2008/11/21/a-haskell-monad-for-infinite-search-in-finite-time/ 這你大概會有興趣。    [2010-06-22 19:10:03 +0800]
  5. 應該就是把實數線兩端接在一起、剪開握住一端另一邊延長、最後在另一端補一點吧 XD。    [2010-06-22 21:03:00 +0800]
  6. 唔，我被 boundary case 咬到了…    [2010-06-23 00:55:00 +0800]
    • Josh Ko ⇒ 天啊，還有疑似反例的東西…    [2010-06-23 01:07:59 +0800]
  7. 很好，來把變種版 binary search 寫起來。    [2010-06-23 10:45:55 +0800]
    • R********** ⇒ 結果你還是發了很多一行文 XD    [2010-06-23 11:52:23 +0800]
  8. 好久沒寫長文，特別是用英文… ↦ Trek through Pure Reason: Binary search, differently ordered    [2010-06-23 15:49:33 +0800]
  9. 049-2391163 get! XD    [2010-06-23 20:58:37 +0800]
    • 翁** ⇒ 恭喜....    [2010-06-23 21:02:56 +0800]
    • Josh Ko ⇒ 時間近一點我再問你會計處有沒有補到人 XD。    [2010-06-23 21:11:09 +0800]
    • 翁** ⇒ 恩恩    [2010-06-23 21:13:24 +0800]
    • Josh Ko ⇒ 蔡專員又留在辦公室了 XD。    [2010-06-23 21:53:08 +0800]
    • 翁** ⇒ 喔喔~你怎知道0.0    [2010-06-23 22:47:31 +0800]
    • Josh Ko ⇒ 剛才電話被轉給她 XD。    [2010-06-23 22:49:19 +0800]
    • 翁** ⇒ 哈哈~那有講啥嗎XD應該只是問候一下巴    [2010-06-23 22:50:14 +0800]
    • Josh Ko ⇒ 差不多。她問我怎麼還沒換手機 XD。然後我終於問到她兒子的名字了 XD。    [2010-06-23 22:51:32 +0800]
    • Josh Ko ⇒ 我猜我今晚第一次接電話的時候蔡專員有小聲喃喃自語「還真的笨到電話接起來」XD。    [2010-06-23 22:51:55 +0800]
    • 翁** ⇒ XDD他兒子好像叫邱X哲??有點忘記了!他&千莉姐去高雄出差!所以才那麼晚回來    [2010-06-23 22:58:07 +0800]
    • Josh Ko ⇒ 日立昱 XD。我們週二三四中午都會去物理館大廳喝咖啡啦（叫做 Ein's Café，很有情調 XD），只是進出的人沒掛名牌不知道誰是誰呀 XD。    [2010-06-23 23:01:58 +0800]
    • 翁** ⇒ 那還不簡單= ="請蔡姐聯絡一下!約個時間碰面!以後就知道啦~    [2010-06-23 23:06:09 +0800]
    • Josh Ko ⇒ 請他在有咖啡的中午到大廳找一群「所外人士」就對了 XD。    [2010-06-23 23:08:11 +0800]
    • 翁** ⇒ that's right...    [2010-06-23 23:08:53 +0800]
  10. 就是 x <= y, A <= x, y < A 三個條件恰有兩個成立時，x
    就變態地小於等於 y 啦！所以照原本的 binary search 跑的話，每次迴圈最糟要比三次喔。這樣是不是比 two-pass 還差？    [2010-06-23 22:30:57 +0800]
    • Josh Ko ⇒ 喔，可是實際上要比的是 a[m] 和 k，而 k 是定值，所以 k < A 這個相當於不用比！這樣至少和 two-pass 一樣好了 XD。    [2010-06-23 22:45:12 +0800]
    • Josh Ko ⇒ 感覺上比較次數很難再降低了… 可是有辦法證至少要 2 lg n 次嗎 ?!    [2010-06-23 23:21:18 +0800]
    • W************ ⇒ 看的懂有鬼啦 柯向上    [2010-06-23 23:27:10 +0800]
    • Josh Ko ⇒ 這是速記，可以當自言自語 XD。    [2010-06-23 23:29:13 +0800]
    • W************ ⇒ 你的就寢時間 好像已經超過很久了    [2010-06-23 23:30:56 +0800]
    • Josh Ko ⇒ 在想問題呀！最近也睡不太著…    [2010-06-23 23:32:10 +0800]
    • Josh Ko ⇒ 不過我覺得應該差不多又 closed 了，可以試著上床去 XD。    [2010-06-23 23:32:40 +0800]
    • 翁** ⇒ 向上他是在想念中辦!!所以睡不著阿XDD    [2010-06-23 23:50:46 +0800]
    • F************ ⇒ 每天睡前打開你的留言板永遠都是那麼的有效用呢    [2010-06-23 23:53:26 +0800]
    • 賴* ⇒ 我也來說一個 大家看無的東西好了。 發勁 是以單田為中心，由雙腿的底部傳到單田，再經單田發送於全身，配合身用者的意念去帶到想傳達的地方...這為發勁 是一個中國古人的智慧。    [2010-06-24 06:16:08 +0800]
    • Josh Ko ⇒ 結案！XD http://joshkos.blogspot.com/2010/06/binary-search-differently-ordered-ii.html    [2010-06-24 10:14:32 +0800]
  11. 到今天都還看得到白色貓毛出沒…    [2010-06-24 09:01:37 +0800]
    • 廖** ⇒ 原來枕頭 無所不在呀    [2010-06-24 09:07:37 +0800]
  12. 哇，八月可能會去北京一趟，參加第二屆「公雞夏天學校」XD。    [2010-06-24 21:41:50 +0800]   [ 2 人說讚！]
    • Josh Ko ⇒ 補個連結 XD。
      http://formes.asia/cms/coqschool/2010    [2010-06-24 22:22:23 +0800]
    • L************** ⇒ 今年可以住宿嗎？還是一樣要住校內旅館？    [2010-06-24 22:33:55 +0800]
    • Josh Ko ⇒ 只看到大陸學生可以免費住清華宿舍，其他人不知道…    [2010-06-24 22:35:50 +0800]
    • L************** ⇒ 去年只說提供住宿，但是臨時通知只有大陸學生才可以。校內旅館環境不差，但是距離有點遠，走路大約要半小時以上才會到。需要再問我細節吧～    [2010-06-24 22:48:30 +0800]
    • S************ ⇒ 還不知道他們人滿了沒有哩，希望報得上..    [2010-06-24 23:31:23 +0800]
  13. MacBook Pro 15" 把玩中⋯    [2010-06-25 17:54:47 +0800]
    • Josh Ko ⇒ 第一發安裝：Haskell Platform！    [2010-06-25 18:12:06 +0800]
    • R********** ⇒ 這應該要發 blog 才對吧 XD    [2010-06-25 19:34:42 +0800]
    • B*********** ⇒ 你忘了加上 "customized"...lol     [2010-06-25 20:25:38 +0800]
    • Josh Ko ⇒ iTunes 竟然要跳兩下才會開！XD    [2010-06-25 21:01:36 +0800]
    • Josh Ko ⇒ 不過也真的只有 iTunes 敢給我跳兩下而已 XD。    [2010-06-25 22:42:08 +0800]
    • R********** ⇒ 我都要跳三四下以上呢 XD    [2010-06-26 00:22:10 +0800]
  14. iPhoto '09 的人臉辨識功能十分好用。    [2010-06-25 23:13:34 +0800]   [ 1 人說讚！]
  15. 快告一段落了。目前唯一碰到的問題是 XeLaTeX 的 fontspec 抓不到中文字體。    [2010-06-26 08:42:14 +0800]
    • Josh Ko ⇒ 要用 ExternalLocation 指定路徑才行⋯    [2010-06-26 12:57:34 +0800]
    • R********** ⇒ 什麼意思，可以說一下嗎 ，我之前深被這個問題所苦，但是莫名奇妙解決了 ...    [2010-06-26 13:45:47 +0800]
    • Josh Ko ⇒ 要寫像 \fontspec[ExternalLocation=/Library/Fonts/]{DFMing-StdW7} 這樣。    [2010-06-26 15:31:49 +0800]
  16. FLOLAC '10 今年都還沒有人放 slides 上去⋯ ="=    [2010-06-26 11:38:08 +0800]
    • R********** ⇒ 你竟然會用這個表情符號耶 XD    [2010-06-26 13:46:48 +0800]
    • R********** ⇒ 還是說 slides 是由同一個人負責收集，所以還沒放 ?    [2010-06-26 13:47:13 +0800]
    • S************ ⇒ 是我還懶惰沒放...    [2010-06-26 14:48:16 +0800]
    • Josh Ko ⇒ 欸⋯ FP lecture notes 的 link 壞掉了呦！:P    [2010-06-27 22:12:46 +0800]
    • R********** ⇒ Lecture Notes 要不要自己印一印帶過去，還是同往年會印一本啊 ?    [2010-06-27 22:56:07 +0800]
    • Josh Ko ⇒ 有印的樣子 XD。    [2010-06-27 23:00:10 +0800]
    • S************ ⇒ fixed. thanks!    [2010-06-28 06:33:34 +0800]
  17. 是該把 5/13-16 屏東墾丁四日遊寫起來留個紀錄了。不過不會直接寫在 blog 上，因為相片太多上傳很慢⋯ 應該會用 Word 寫，然後輸出 PDF 貼連結到 blog 上吧 XD。    [2010-06-26 18:28:00 +0800]
    • R********** ⇒ 我的 MacBook 沒有 Word ... Orz    [2010-06-26 19:51:26 +0800]
    • 翁** ⇒ 趕快寫!!我在複製你的!貼到我的部落格XDD    [2010-06-28 09:16:17 +0800]
  18. 坐火車回台北，遇到中壢-內壢路段淹水，在埔心停了一陣子。    [2010-06-27 20:57:07 +0800]
    • L********* ⇒ 還好我都坐客運回中壢 XD    [2010-06-27 22:06:25 +0800]
    • R********** ⇒ 我中午坐的時候還沒有說 XD    [2010-06-27 22:07:08 +0800]
  19. Mazurka Op. 50 No. 3 好像練得差不多了，下一首是 Op. 33 No. 4。    [2010-06-27 21:00:21 +0800]
  20. 還沒看出來 balanced typing 是怎麼保證的⋯    [2010-06-28 10:50:21 +0800]
    • Josh Ko ⇒ 唔，為什麼 newChan 不是在 channel typing 裡面多兩個 polarised channels 呀？    [2010-06-28 10:52:27 +0800]
    • Josh Ko ⇒ 其實 newChan 根本沒用到？    [2010-06-28 10:56:19 +0800]
    • Josh Ko ⇒ 要啦，accept & request 撞在一起就會出來了。    [2010-06-28 10:57:55 +0800]
    • Josh Ko ⇒ 所以從 root 往 leaves 看：用 newChan 產生兩個 dual, polarised channels，然後 Conc typing rule 會把兩個 channels 分給並行的兩個 processes，保證 typing 會是 balanced。    [2010-06-28 11:06:44 +0800]
    • Josh Ko ⇒ 不過現在不太知道要讓哪些 types 算是 well-typed 耶⋯    [2010-06-28 11:09:01 +0800]
    • Josh Ko ⇒ 好像應該說哪些 "programs" 算是 well-typed。    [2010-06-28 11:09:35 +0800]
    • Josh Ko ⇒ 再來就是找 "polarity" 到底出現在哪裡⋯    [2010-06-28 11:17:18 +0800]
  21. 在台大進修推廣部 207 教室，FLOLAC '10 即將開始。scm 老師又抓出他的招牌公雞頭⋯    [2010-06-28 13:18:11 +0800]   [ 1 人說讚！]
  22. Max proposes a Chinese character as an equivalent of iff in English. ↦ FLOLAC '10    [2010-06-28 15:47:09 +0800]   [ 1 人說讚！]
    • S************ ⇒ We wonder how it should be pronounced..    [2010-06-28 15:54:31 +0800]
    • Josh Ko ⇒ Has anyone noticed that the color of the character is not exactly black...?    [2010-06-28 19:09:08 +0800]
  23. 邏輯作業 3 (d) 用 calculational logic 證明 ¬(P ∨ Q) ↔ ¬P ∨ ¬Q 是 tautology，如果採用的策略是直接把此式化為 ⊤（得到 ¬(P ∨ Q) ↔ ¬P ∨ ¬Q ⇔ ⊤ 然後由 Theorem 2 知 ⊧ ¬(P ∨ Q) ↔ ¬P ∨ ¬Q），感覺有點像在玩魔法泡泡，把樣式匹配的式子通通消掉 XD。    [2010-06-28 20:32:25 +0800]
    • Josh Ko ⇒ 欸，可是有人特別叮嚀我不要貼答案⋯    [2010-06-28 20:46:50 +0800]
    • 翁** ⇒ 高手!我需要你跟我聊MSN!!    [2010-06-28 20:51:05 +0800]
    • R********** ⇒ 幹，我不想看到，你快刪掉 XD    [2010-06-28 21:47:29 +0800]
    • Josh Ko ⇒ 這只是個方向不是解答呀 XD。    [2010-06-28 23:18:09 +0800]
    • L********* ⇒ 所以這篇算有雷嗎，劇情洩漏？ XD    [2010-06-29 00:05:28 +0800]
    • S************ ⇒ hmmm.. 跟我用的方法完全不同... @_@    [2010-06-29 01:24:48 +0800]
    • Josh Ko ⇒ 應該滿好玩的啦！XD    [2010-06-29 11:16:19 +0800]
  24. 咦，為什麼不要直接讓 newChan 產生兩個 polarised channels，而要先產生一個 neutral channel 再分成兩個 polarised channels 勒？    [2010-06-29 10:07:53 +0800]
    • Josh Ko ⇒ 是因為 runtime 的時候需要有個共同 channel 嗎？    [2010-06-29 11:09:49 +0800]
    • S************ ⇒ 還沒想到那麼多耶，可能只是當時想到的 design choice 而已。    [2010-06-29 11:46:14 +0800]
  25. 莊老師又講到 fixed point of base functors 了，陣亡率有多高呢⋯？XD    [2010-06-29 12:14:46 +0800]
    • Josh Ko ⇒ OCaml 的語法讓整件事變得更難懂了呀 XD。    [2010-06-29 12:15:11 +0800]
    • Josh Ko ⇒ 耶，commutative diagrams 出現了⋯    [2010-06-29 12:20:23 +0800]
    • R********** ⇒ 聽說 efang 聽到睡著了 XD    [2010-06-29 14:05:48 +0800]
    • Josh Ko ⇒ 莊老師會看到這裡耶！XD    [2010-06-29 14:11:50 +0800]
    • R********** ⇒ efang 很認真聽啦，不過她可能有些地方聽不懂 XD (我覺得現在刪掉也來不及了。)    [2010-06-29 14:47:37 +0800]
    • S************ ⇒ 來不及了。（煙）    [2010-06-29 16:16:55 +0800]
  26. 好久沒有聽到 "implementation-dependent" 這種專業的詞了 XD。    [2010-06-29 14:09:50 +0800]
    • L*********** ⇒ 我好想說一點都不想再聽到這種問題了 @@..    [2010-06-29 21:40:22 +0800]
  27. 唔，可是 Semantics with Applications 裡面最後還是定義了 statements 的語意是 State 上的 _partial_ function 呢（pp 31 - 32）。還是說 operational vs. denotational 的區別在於證明的方式？（Judgements vs. ordinary math?）    [2010-06-29 20:28:19 +0800]
    • L************** ⇒ denotational semantics 上的 state 是什麼呢？    [2010-06-29 20:30:27 +0800]
    • Josh Ko ⇒ 簡單的話就是 name 到 value 的 mappings?    [2010-06-29 20:39:54 +0800]
    • L************** ⇒ value 的結構呢？跟 operation semantics 上的 state 比起來呢？    [2010-06-29 20:47:45 +0800]
    • Josh Ko ⇒ value 可以用 flat cpo 就好？    [2010-06-29 21:00:33 +0800]
  28. 就是 ∀ 0 ≤ j < i. a[j] Maj a[0, i) → a[j] = candidate 去加料吧⋯？    [2010-06-29 22:09:24 +0800]
    • Josh Ko ⇒ 嗯，可能要拆兩段⋯    [2010-06-29 22:26:03 +0800]
  29. 以 count = 0 的 indices 分割開來的區間上，除了最後一個區間，每個區間的第一個元素都是 "semi-majority"，即恰好出現「區間長的一半」次。想當整個 array 的 majority，【艸大口】在每個區間當 semi-majority，並在最後一個區間當 majority。以上不對。    [2010-06-29 22:51:41 +0800]
    • Josh Ko ⇒ 重點是什麼時候不是 majority 啦！    [2010-06-29 22:55:42 +0800]
  30. 應該這樣說：沒坐最後一個區間的首席的人，最好最好在前面所有區間也只佔一半。他在最後一個區間頂多也只跟首席拚到平手，所以整個 array 上最多也只有一半而已，不是 majority。    [2010-06-29 23:03:36 +0800]
    • Josh Ko ⇒ 嘿嘿，再來要用 loop invariant 弄喔⋯    [2010-06-29 23:04:28 +0800]
  31. I'll try something like ( ∀ 0 ≤ j < c. a[j] ¬ Maj a[0, c) ) ∧ ( count > 0 → a[c] Maj [c, i) ).    [2010-06-30 07:12:45 +0800]
    • 翁** ⇒ 昨天我嘗試利用資料庫做連結匯入...結果上網查了半天...無功而返= ="看來應該要去買本書來研究XDD    [2010-06-30 07:46:03 +0800]
    • 翁** ⇒ 對那沒啥概念= ="網路上的資料也很模糊XD    [2010-06-30 10:38:39 +0800]
  32. 試這個！
    { GUESSED-INV:
    ∧ ∀ 0 ≤ j < c. a[j] ¬ Maj a[0, c)
    ∧ count = 2 × # a[c] in a[c, i) - # a[c, i)
    ∧ ∀ c ≤ j < i. a[j] Maj a[c, i) → a[j] = a[c] }    [2010-06-30 09:35:21 +0800]
    • Josh Ko ⇒ 再加個 count \geq 0.    [2010-06-30 09:40:31 +0800]
    • Josh Ko ⇒ 決定了，就這個！    [2010-06-30 10:10:27 +0800]
    • Josh Ko ⇒ 定義 v Maj a[i, j) = 2 * # v in a[i, j) - # a[i, j) > 0, where a[i, j) = a[i], a[i+1], ..., a[j-1].    [2010-06-30 10:11:27 +0800]
  33. 邏輯還是要給德國人教才知道符號為什麼長那樣呀 XD。    [2010-06-30 11:13:28 +0800]
  34. 還是覺得 small-step semantics 比較像 operational semantics 呀⋯    [2010-06-30 16:06:39 +0800]
    • 翁** ⇒ 明天宣余要請大家吃雞排+飲料~~~超棒的喔!!(撒花~~~    [2010-06-30 16:59:23 +0800]
    • Josh Ko ⇒ 我後天再打電話給他 XD。    [2010-06-30 20:08:13 +0800]
    • 翁** ⇒ 去聽看看我的新連結!    [2010-06-30 20:09:37 +0800]
    • S************ ⇒ 我後來想起：你現在困惑的可能是 operational semantics 好像也是把程式 map 到（state 到 state 的）函數。但如果有個簡單括衝過的 lambda calculus, 其 operational semantics 講的就是一個 term 怎麼 reduce 成另一個 term, 這和 denotational semantics 的差異就比較明顯了。    [2010-06-30 23:10:00 +0800]
    • Josh Ko ⇒ 是呀，但是這就比較像 small-step？    [2010-06-30 23:36:40 +0800]
  35. Fold 好像總是或高或低構成學習上的門檻啊。    [2010-06-30 22:08:38 +0800]
  36. 感覺上 compositionality 是區分 denotational vs. operational semantics 的重要性質？    [2010-07-01 10:55:37 +0800]
    • Josh Ko ⇒ 畢竟不管 natural semantics 和 structural operational semantics 最後都定義了 semantic functions 把 statements 映到 states 上的函式，只是它們兩者的 semantic functions 的定義是導自 derivation trees/sequences。    [2010-07-01 10:57:30 +0800]
    • Josh Ko ⇒ 然後剛好 operational semantics 證明「semantic function 在某個 statement 上的值是什麼」的方法對應到程式型式的變換（執行）而已。    [2010-07-01 11:01:14 +0800]
  37. 可以去北京了⋯！    [2010-07-01 11:47:49 +0800]   [ 4 人說讚！]
    • Josh Ko ⇒ 好像學生還收不滿，持續招生中 XD。    [2010-07-01 12:06:12 +0800]
    • W************ ⇒ ＯＮＥ　乃　ＩＮ　北京～    [2010-07-01 12:20:10 +0800]
    • 賴* ⇒ 哇 奶 是 白七    [2010-07-01 12:24:50 +0800]
    • R********** ⇒ 記得帶紀念品回來 XD    [2010-07-01 13:18:29 +0800]
    • 王** ⇒ 旅行の写真です ? 私は中国からお土産が欲しい ！！！    [2010-07-01 14:33:27 +0800]
    • 賴* ⇒ 樓上的乃是 你鬨幾　（日文：日本人）    [2010-07-01 15:04:06 +0800]
    • Josh Ko ⇒ 「會有郊遊照片嗎？我要中國土產！！！」此段翻譯是否正確？XD    [2010-07-01 20:03:45 +0800]
    • 賴* ⇒ 差不多!!....我要來自中國的土產..
          [2010-07-01 22:21:15 +0800]
    • L********* ⇒ 中國最有名的東西是…

      黑心貨 XD    [2010-07-01 23:06:22 +0800]
    • 賴* ⇒ 所以二奶也有黑心的?    [2010-07-02 08:18:49 +0800]
  38. 學術界真是暗潮洶湧⋯    [2010-07-01 15:52:25 +0800]
    • 邱** ⇒ 聽起來不像好事...    [2010-07-01 15:54:37 +0800]
    • Josh Ko ⇒ 其實也還好啦，有人偷偷諷刺不在現場的人 XD。    [2010-07-01 15:55:59 +0800]
    • L********* ⇒ 「文人相輕，自古而然。」不是沒有道理的啊！    [2010-07-01 23:04:52 +0800]
  39. Frama-C 真的灌成了！（吧⋯）    [2010-07-01 20:02:28 +0800]
    • L*********** ⇒ 我 plugin Jessie 和 Aorai 好像一直掛不上去... @@    [2010-07-01 21:23:17 +0800]
  40. 早上搭莊老師的車，將轉入大門前的路上，看到路旁有位老先生，長得像 Knuth 和火雲邪神的混合體。然後我發現這裡 transitivity 還可以用，Knuth 也挺像火雲邪神的（特別是 TAOCP 包裝紙上的照片 XD）。    [2010-07-02 09:10:11 +0800]
    • Josh Ko ⇒ 「大門」指中研院的大門。    [2010-07-02 09:10:38 +0800]
    • 賴* ⇒ 可有照片...    [2010-07-02 10:00:42 +0800]
    • W************ ⇒ 上班專心點啦 賴問你很鹹耶.. 沒事情去出納幫一下    [2010-07-02 10:30:52 +0800]
    • 賴* ⇒ 有啊~~出納定便當...    [2010-07-02 10:56:32 +0800]
  41. 標題頁 "Limits of first-order logic" 的下一頁一片空白。Max:「這是說 first-order logic 沒有 limits??」    [2010-07-02 10:32:18 +0800]
  42. 古時候的 great computer scientists 總是有很好的 tastes...    [2010-07-02 16:51:11 +0800]   [ 1 人說讚！]
  43. 馬桶整個塞住好幾天了⋯    [2010-07-03 20:52:18 +0800]   [ 2 人說讚！]
    • 翁** ⇒ 沒有"糟"給我按XDD    [2010-07-03 20:59:09 +0800]
    • Josh Ko ⇒ 很不讚呀，還得跑去資訊所上廁所 XD。    [2010-07-03 21:04:40 +0800]
    • Josh Ko ⇒ 聽說亞欣星期三就要上班了。你知道奕程何時有空嗎？看能不能抓到他⋯    [2010-07-03 21:06:25 +0800]
    • B*********** ⇒ 你不是才剛搬新家嗎?    [2010-07-03 21:07:08 +0800]
    • Josh Ko ⇒ 是呀，沒多久就塞住了。明天找房東看能不能解決 XD。    [2010-07-03 21:10:27 +0800]
    • W********* ⇒ 現在就去找吧?    [2010-07-03 21:28:42 +0800]
    • Josh Ko ⇒ 可是我快睡著了 XD。    [2010-07-03 21:38:25 +0800]
    • 翁** ⇒ 不行稅阿!!!今天有熱血的世足賽!!!    [2010-07-03 21:51:37 +0800]
    • 翁** ⇒ 奕程喔~還是我禮拜一給你電話!你在聯絡他看看    [2010-07-03 21:51:59 +0800]
    • Josh Ko ⇒ 喔好啊 XD。    [2010-07-03 21:53:58 +0800]
    • 翁** ⇒ 他應該跟我一樣14、15要考試!考完就沒事了!    [2010-07-03 21:55:05 +0800]
    • Josh Ko ⇒ 那我來約 20 - 24 那週看看 XD。    [2010-07-03 21:55:43 +0800]
    • 翁** ⇒ 恩恩 看你門吧!    [2010-07-03 21:56:57 +0800]
  44. 屏東遊記寫到小杜包子，看一下照片肚子猛然餓了一下 XD。    [2010-07-03 21:40:14 +0800]   [ 1 人說讚！]
    • 翁** ⇒ 快團購!!!可以分一點到辦公室XD    [2010-07-03 21:57:38 +0800]
    • 翁** ⇒ 不對阿!!才寫到小杜包喔!!那還很前面耶XDD    [2010-07-03 21:58:00 +0800]
    • Josh Ko ⇒ 到小杜包子已經第四頁了，三千多字 XD。    [2010-07-03 21:58:58 +0800]
    • 翁** ⇒ 我看要寫屏東郵記~1萬字都ok    [2010-07-03 21:59:25 +0800]
    • Josh Ko ⇒ 團購不是中辦專有的風景嗎？XD    [2010-07-03 21:59:29 +0800]
    • 翁** ⇒ 我忘記他那時候說團購是幾時了??不過想吃就要趕快!不然要等很久!!    [2010-07-03 22:00:03 +0800]
    • Josh Ko ⇒ 今天至此收工。上 FLOLAC 有助於把時差調整回來 XD。    [2010-07-03 22:05:28 +0800]
  45. 房東帶來長長的竿子進廁所鏘鏘作響一陣，馬桶通了！    [2010-07-04 10:35:01 +0800]   [ 2 人說讚！]
    • 翁** ⇒ 恭喜!    [2010-07-04 10:39:17 +0800]
    • Josh Ko ⇒ 這樣明天交房租才交得心甘情願呀 XD。    [2010-07-04 10:40:07 +0800]
    • 翁** ⇒ 哈哈~我也還沒繳房租    [2010-07-04 10:40:29 +0800]
    • R********** ⇒ 這實在是太強了吧 XDXD    [2010-07-04 10:44:39 +0800]
    • R********** ⇒ 不過也說不定是因為這樣子才容易塞住 ... XD    [2010-07-04 10:47:21 +0800]
    • 賴* ⇒ 難道是傳中的 神竿嗎?    [2010-07-04 11:10:28 +0800]
    • W************ ⇒ 是佐佐木小次郎的    [2010-07-04 11:45:09 +0800]
    • 賴* ⇒ 上...武藏    [2010-07-04 11:53:07 +0800]
    • 王** ⇒ 應該是破了吧    [2010-07-05 04:02:58 +0800]
    • 賴* ⇒ 破馬?    [2010-07-05 08:09:18 +0800]
  46. 訂下傅聰的德布西前奏曲、練習曲全集，可惜蕭邦鋼琴協奏曲沒了。    [2010-07-04 13:20:04 +0800]
    • Josh Ko ⇒ 傅聰的 CD 是不是特別難買⋯？    [2010-07-04 13:20:39 +0800]
  47. （談到去墾丁上 FLOLAC）在白沙灣的沙灘上畫 derivation trees 才畫得下嘛！    [2010-07-05 00:15:31 +0800]
  48. 看完 EWD 611 〈我對「大西洋有兩側」這事實的觀點〉，覺得 Dijkstra 有些點說得還滿準的呀。我果然是激進派⋯ Orz ↦ E. W. Dijkstra Archive: On the fact that the Atlantic Ocean has two sides. (EWD 611)    [2010-07-05 10:29:17 +0800]
    • R********** ⇒ 可是你的臉不像激進派說 XD    [2010-07-05 10:40:20 +0800]
  49. 我把 Pascal 的 Skein library homework 做掉了！    [2010-07-05 20:39:55 +0800]
  50. Pascal 給的解答根本想不到呀！XD    [2010-07-06 00:32:25 +0800]
  51. Denotational semantics 真是美得讓人掉眼淚⋯ XD    [2010-07-06 09:59:09 +0800]   [ 2 人說讚！]
    • A*********** ⇒ : what?! the speaker makes it so beautiful ?!    [2010-07-06 10:47:09 +0800]
    • Josh Ko ⇒ 其實剛才我是重讀幾句 Stoy 的 textbook XD。    [2010-07-06 11:44:54 +0800]
    • A*********** ⇒ : 你真的有傳承到 "夠了" 家族的本領噎!    [2010-07-06 11:57:08 +0800]
  52. 好像法式英語有聽比較習慣一點點了 XD。    [2010-07-06 15:24:33 +0800]
    • 賴* ⇒ 說來聽聽!!!    [2010-07-06 15:25:29 +0800]
  53. 收到 final contract 和 college accommodation 相關文件。覺得 Vogons 一定是以英國人為 model 塑造出來的⋯    [2010-07-06 22:25:31 +0800]
  54. 但其實我對 fixed-points 的論證很不熟呀⋯    [2010-07-07 11:47:14 +0800]
    • W************ ⇒ 你講的我全都不熟    [2010-07-07 11:48:27 +0800]
    • Josh Ko ⇒ 如果 19 號星期一回去你可以嗎？XD    [2010-07-07 11:52:37 +0800]
    • W************ ⇒ 你怎麼不選個放假時間˙＝　＝　這樣有些人工作不能去吧
      像　糟糕顯溢。　　我應該是都ＯＫ，跟我媽說一聲就可以。    [2010-07-07 11:54:39 +0800]
    • Josh Ko ⇒ 因為要看辦公室的人⋯ 顯奕喵說可以請假但是要扣薪水，你可以說服他放棄那天的薪水 XD。    [2010-07-07 11:56:32 +0800]
    • W************ ⇒ 你說服他吧 你可以每小時打給他一次叫他來
      說枕頭想跟他說話...    [2010-07-07 11:57:39 +0800]
    • Josh Ko ⇒ 應該是想咬他吧 XD。他上班不能接電話的樣子，晚點再說 XD。    [2010-07-07 11:58:38 +0800]
    • W************ ⇒ 那就半夜 一人一通 打到天亮說要去為止    [2010-07-07 12:00:32 +0800]
    • Josh Ko ⇒ 這樣他會關機吧⋯ XD    [2010-07-07 12:01:03 +0800]
  55. 所以 seminar 是廣告時間嘛 XD。    [2010-07-07 12:20:03 +0800]   [ 1 人說讚！]
    • R*********** ⇒ yesXD    [2010-07-07 12:40:25 +0800]
    • R********** ⇒ 也有可能是拉人時間 XDXD    [2010-07-07 12:43:14 +0800]
    • Y********** ⇒ 傳教? XD    [2010-07-07 16:38:08 +0800]
  56. Jessie 好玩！    [2010-07-07 15:26:52 +0800]
    • 賴* ⇒ 那啥..    [2010-07-07 16:33:54 +0800]
    • Josh Ko ⇒ http://frama-c.com/jessie.html XD    [2010-07-07 16:35:43 +0800]
    • Y********** ⇒ 確實不錯玩 :p    [2010-07-07 16:37:48 +0800]
    • 賴* ⇒ 如何用?    [2010-07-07 16:41:59 +0800]
    • Josh Ko ⇒ Windows 有安裝檔，然後在程式裡寫很多條件讓它去檢查 XD。    [2010-07-07 16:47:28 +0800]
    • R********** ⇒ 我現在用一用也覺得蠻好玩的，不過聽學弟說不是一堆人的 jessie 掛掉 XD?    [2010-07-07 23:52:41 +0800]
  57. 1. Ohlsson 很「炫」。
    2. 要到焦元溥的簽名！
    3. Blog 稍後才補，因為要考 Frama-C⋯    [2010-07-07 23:03:53 +0800]   [ 1 人說讚！]
  58. ATAS 過了，效率不錯嘛 XD。    [2010-07-09 07:18:00 +0800]   [ 1 人說讚！]
  59. 交卷時間要到了，可以喊「所有人：動．作．停～～～」嗎？XD    [2010-07-09 12:33:31 +0800]
    • W************ ⇒ 停了 還動! 還看! 就是你。    [2010-07-09 12:34:18 +0800]
    • W************ ⇒ 懷疑啊！
          [2010-07-09 12:34:37 +0800]
    • 賴* ⇒ 分隊長:「減你 五分 有沒有問題」。
      菜渣:「報告..沒問題」。
          [2010-07-09 12:40:56 +0800]
    • R********** ⇒ 你真的喊了會笑出來吧 XD    [2010-07-09 14:09:34 +0800]
  60. 好像要交卷的沙沙聲，可是還是沒人交卷！交了就可以吃 pizza 了呀⋯    [2010-07-09 12:37:44 +0800]
  61. 好多人看完 derivation 都會問 automatic search...    [2010-07-09 15:30:51 +0800]
  62. 其實 imperative 程式才真的是把 states 藏起來呀⋯ XD    [2010-07-09 15:53:52 +0800]   [ 2 人說讚！]
    • Y********** ⇒ 何以此說? XD    [2010-07-09 16:07:54 +0800]
    • Josh Ko ⇒ 因為 imperative 程式對應 FP 的 monads 嘛，正常的 FP 不用 monads，states 反而都是明顯的。    [2010-07-09 16:09:04 +0800]
    • Josh Ko ⇒ http://joshkos.blogspot.com/2009/05/on-states.html    [2010-07-09 16:09:33 +0800]
    • R********** ⇒ 所以我們應該把這個討論串寄給蔡老師看嗎 XD    [2010-07-09 16:30:03 +0800]
    • 陳** ⇒ XDDDDDD
          [2010-07-09 16:44:13 +0800]
    • S************ ⇒ 看到蔡老師的 presentation 當時是有驚到：糟糕，我講的東西和他講的彼此矛盾好多。他的學生一定覺得我是異端.. XD    [2010-07-09 19:12:21 +0800]
    • Josh Ko ⇒ 蔡老師今天的主題好像很久以前的 MFN 有講過？    [2010-07-09 22:11:41 +0800]
    • Josh Ko ⇒ 其實友善地鬥鬥嘴也滿好玩的啦 XD。    [2010-07-09 22:26:39 +0800]
    • Y********** ⇒ 關鍵字是"友善" :p    [2010-07-09 23:08:12 +0800]
    • Josh Ko ⇒ 我是覺得兩年前 MFN 的時候蔡老師願意學 FP 這邊的 category-theoretical inductive datatypes，這種態度真的挺不容易見到⋯
      http://joshkos.blogspot.com/2008/11/squiggol.html    [2010-07-10 00:20:20 +0800]
  63. sounds like monotonicity...    [2010-07-09 16:33:19 +0800]
  64. 突然又開始上 FP XD。    [2010-07-09 16:40:29 +0800]
    • Josh Ko ⇒ 而且又是我們親愛的 commutative diagram XD。    [2010-07-09 16:40:55 +0800]
    • R********** ⇒ XD    [2010-07-09 16:47:36 +0800]
    • R*********** ⇒ XDDD    [2010-07-09 16:53:41 +0800]
  65. 火車上把 Frama-C 考卷改完了。0 真是不可或缺的發明⋯    [2010-07-09 22:14:06 +0800]   [ 2 人說讚！]
    • 翁** ⇒ 寫0就對了.....    [2010-07-09 22:20:58 +0800]
    • Josh Ko ⇒ 0 是我在寫的⋯    [2010-07-09 22:23:36 +0800]
    • 翁** ⇒ 舖!!都0分~~~    [2010-07-09 22:32:06 +0800]
    • R********** ⇒ 這太慘了 XD
          [2010-07-09 22:43:39 +0800]
    • Josh Ko ⇒ 初步統計：滿分 55（我考 49），AVG = 10.3, MIN = 0, Q1 = 0, MED = 4, Q3 = 16.5, MAX = 41, DEV = 13.4。    [2010-07-09 22:47:37 +0800]
    • R********** ⇒ 這 XD    [2010-07-09 22:49:42 +0800]
    • 翁** ⇒ 現在是要中位數...4分位數....嗎XD    [2010-07-09 22:50:05 +0800]
    • 翁** ⇒ 可以用盒狀圖呈現!!!    [2010-07-09 22:50:23 +0800]
    • Josh Ko ⇒ 對，但好慘，我不太想畫出來 XD。    [2010-07-09 22:53:21 +0800]
    • Josh Ko ⇒ FREQUENCY 公式：
      0 17
      1 - 5 6
      6 - 10 3
      11 - 15 3
      16 - 20 1
      21 - 25 1
      26 - 30 1
      31 - 35 5
      36 - 40 1
      41 - 45 1
      46 - 50 0
      51 - 55 0
      TOTAL 39    [2010-07-09 22:54:08 +0800]
    • L************** ⇒ 讓我想到我大學下一屆的高微應屆全當的慘況，重修也只有五個過關... XD    [2010-07-09 22:55:28 +0800]
    • Josh Ko ⇒ 比較粗的 FREQUENCY:
      0 17
      1 - 10 9
      11 - 20 4
      21 - 30 2
      31 - 40 6
      41 - 50 1
      51 - 55 0    [2010-07-09 23:07:07 +0800]
    • Y********** ⇒ 看起來有點悽慘呀
      有和Pascal說了嗎? XD    [2010-07-09 23:10:15 +0800]
    • Josh Ko ⇒ 不太敢耶⋯ 我明天再把考卷掃描起來送給他好了 XD    [2010-07-09 23:12:21 +0800]
    • Y********** ⇒ 全部scan起來? 還是只有某個lower bound以上的才要scan? XD    [2010-07-09 23:19:57 +0800]
    • Josh Ko ⇒ 應該會全部吧 XD    [2010-07-09 23:20:16 +0800]
    • Y********** ⇒ 掃到接近白紙的物體的時候不會覺得有股怨念嗎? XD    [2010-07-09 23:31:23 +0800]
    • Josh Ko ⇒ 還有人根本不交勒 XD    [2010-07-09 23:31:55 +0800]
    • Y********** ⇒ ...所以是真的有少呀?
      Pascal今天有針對這點和你說啥嗎? XD    [2010-07-09 23:40:11 +0800]
    • Josh Ko ⇒ 他說反正考試本來就是要區分出會和不會的人嘛⋯ XD    [2010-07-09 23:40:58 +0800]
    • R********** ⇒ 我是有聽到有人根本連期末考都沒來考的 XD    [2010-07-10 08:01:20 +0800]
    • Y********** ⇒ 缺考我記得大約有兩三個吧... @@
      其中一個我還認識勒(嘆)    [2010-07-10 09:37:48 +0800]
    • Y************ ⇒ 我比較喜歡 0 上面有一撇瀏海....    [2010-07-10 22:24:34 +0800]
    • R********** ⇒ 傳說中帶帽子的 0 嗎 XD    [2010-07-10 22:30:55 +0800]
  66. Pascal 已經回到家，也看完我改的考卷了。他說雖然有幾個人表現很好，但是看到那麼多白卷他好傷心⋯ 正在寫信安慰他。    [2010-07-11 20:19:54 +0800]
    • L*********** ⇒ 不知道是不是按 like 的場合 @@    [2010-07-11 20:53:49 +0800]
    • Y********** ⇒ 似乎不是 @@

      希望不會對台灣留下壞印象 Orz    [2010-07-11 21:05:37 +0800]
    • L************** ⇒ 可是我還是忍不住按了 "Like"。    [2010-07-11 21:35:02 +0800]
    • Josh Ko ⇒ 寫完了，寫好久⋯ 跟他說我們英文本來就不太好、交白卷可能只是答題策略、反正 FLOLAC 本來就很難 XD。    [2010-07-11 21:44:44 +0800]
    • Josh Ko ⇒ 成績送啦！    [2010-07-11 21:58:44 +0800]
    • Y********** ⇒ 「FLOLAC 本來就很難」感覺很有說服力 XD    [2010-07-11 22:45:37 +0800]
    • 陳** ⇒ 有那麼多白卷真的很扯/o/    [2010-07-14 21:18:57 +0800]
  67. 昨天突然發現我想錯了。我們沒有要做完整的 pi-calculus interpreter，只有要把 pi-calculus terms 翻譯成 concurrent Haskell terms 而已，所以 interpreter 那邊應該比我想像的輕鬆不少。    [2010-07-12 09:21:33 +0800]
  68. 我這個月的簡訊費大概遠遠超過自從我有手機以來的加總⋯    [2010-07-12 20:59:45 +0800]   [ 1 人說讚！]
    • 翁** ⇒ 人不輕狂枉少年!!!(好像不是用在這...    [2010-07-12 21:06:52 +0800]
    • Josh Ko ⇒ 社發科兩個給你連絡了啦⋯ XD    [2010-07-12 21:09:18 +0800]
    • 翁** ⇒ 嘎嘎!!!我不是主辦人哩XDDD(裝死    [2010-07-12 21:10:15 +0800]
    • Josh Ko ⇒ 舉哥和鋕宏滿常上 fb 的嘛，在 fb 上解決好了 XD。    [2010-07-12 21:11:39 +0800]
    • 翁** ⇒ ㄎㄎ他們有很常上嗎= ="    [2010-07-12 21:17:01 +0800]
    • Josh Ko ⇒ 最近滿常看到的啊，沒有再說⋯    [2010-07-12 21:17:45 +0800]
    • F************ ⇒ 我沒收到簡訊~    [2010-07-12 21:29:58 +0800]
    • Josh Ko ⇒ 你在 fb 上解決了嘛 XD。    [2010-07-12 21:33:18 +0800]
    • Josh Ko ⇒ 益隆說「盡量抽空到」！    [2010-07-12 21:46:37 +0800]
  69. 終於把可惡的鬢角削掉了。    [2010-07-12 21:33:42 +0800]
  70. 我現在覺得去找來 Concurrent Haskell 的 semantics 然後用那證明我們的 type system 有好性質會比較對⋯ 用 Yoshida 那套語言和 operational semantics 始終和最後的 Concurrent Haskell 有 gap 吧？    [2010-07-13 09:35:04 +0800]
  71. 這樣是要做三層 terms，上面是（類似）Yoshida 的 terms，中間是和 Concurrent Haskell 一一對應的 terms，下面翻譯成真正的 (primitive) Concurrent Haskell terms⋯嗎？    [2010-07-13 10:30:13 +0800]
    • S************ ⇒ 好像越來越複雜了。我想可先看看別人做類似的東西是怎麼做的。    [2010-07-13 11:27:34 +0800]
    • Josh Ko ⇒ 很快看過去，他們好像是直接把 interpreter 寫出來，然後說一句他們寫在 paper 上的 operational semantics 和他們寫的 interpreter 直接對應⋯？    [2010-07-13 11:31:16 +0800]
    • S************ ⇒ ㄧ句證明法！    [2010-07-13 11:58:57 +0800]
  72. 還開 --type-in-type 勒⋯ 幸好他們也沒真的證什麼東西 XD。    [2010-07-13 15:40:24 +0800]
    • Josh Ko ⇒ 馬上就辯解說他們有做沒開 --type-in-type 版的，只是沒有 universe polymorphism 就很重複很討厭啦！    [2010-07-13 15:43:13 +0800]
    • S************ ⇒ 在註腳裡，是嗎？    [2010-07-13 15:45:10 +0800]
    • Josh Ko ⇒ Yes.    [2010-07-13 15:46:29 +0800]
  73. 不管怎樣 Chomsky's lecture 先註冊再說啦！    [2010-07-13 16:53:43 +0800]
    • Josh Ko ⇒ 意思是我已經註冊了 XD。    [2010-07-13 16:53:55 +0800]
    • Josh Ko ⇒ 可以選的身分似乎只有 "research specialist" 和 "student"，但前者夾在 "principal investigator" 和 "postdoctoral fellow" 中間，而且看起來好 specialised⋯ 還是選 student 好了 XD。    [2010-07-13 16:56:41 +0800]
    • L*********** ⇒ @@ 這是哪裡的..?    [2010-07-13 17:27:06 +0800]
    • Josh Ko ⇒ 8/9 在中研院，8/10 在清大。
      http://iao.sinica.edu.tw/    [2010-07-13 17:55:53 +0800]
    • L*********** ⇒ 好像跟語言沒什麼關係？ :/ http://www.chomsky.info/articles/199112--.htm    [2010-07-13 18:38:30 +0800]
    • Josh Ko ⇒ 他領域很廣，這次來講的題目很多人都看不懂，只是要去看他本人 XD。計算學界會知道他大概都是因為 Chomsky hierarchy: http://en.wikipedia.org/wiki/Chomsky_hierarchy    [2010-07-13 18:42:29 +0800]
    • L*********** ⇒ OAO 好吧... @@ 害我興奮了一下 XD    [2010-07-13 19:19:43 +0800]
  74. scm 老師要衝一本嗎？XD ↦ Syntactic Structures (2nd Edition)    [2010-07-13 18:35:21 +0800]
    • Josh Ko ⇒ 現在用 expedited shipping 訂的話應該是滿安全的 XD。    [2010-07-14 00:46:31 +0800]
    • L************** ⇒ 原來是為了要簽名 ... XD    [2010-07-14 00:49:05 +0800]
  75. 突然想到兩年前 Oleg 有講過用 Twelf 證明 type safety，可是那時候沒有聽得很懂⋯ ↦ Meta-Theory and Logical Frameworks    [2010-07-14 09:58:30 +0800]
  76. Roadmap 畫不出來⋯    [2010-07-14 10:27:04 +0800]
  77. 能弄的先弄出來就對了 XD。    [2010-07-14 10:46:24 +0800]
  78. 嗯，higher-order 果然討厭 XD。    [2010-07-14 11:44:45 +0800]
    • 陳** ⇒ 為什麼> <    [2010-07-14 21:07:05 +0800]
    • Josh Ko ⇒ 是我們現在在做的東西啦。比方說兩個 processes 之間透過一個 channel 傳東西，我們希望描述這個 channel 上的訊息傳遞模式，像「讀兩個整數寫一個整數」這樣。如果 channel 傳的東西可以是 channel 的話，就可能要說「傳一個『讀兩個整數寫一個整數』的 channel」這種話，事情就變得複雜很多。    [2010-07-14 21:12:24 +0800]
    • 陳** ⇒ 哈哈，higher order function 都是用起來爽，寫起來難（要有efficiency for general purpose...）
      現在我也只會用而已...:P    [2010-07-14 21:16:28 +0800]
  79. Channel 要用 MVar 做，但上面傳的 types 可能不只一種，所以弄了一個生成 sum types 的機制，不知道會不會好用。另外 Vec A (suc n) 好像還是不能取代 non-empty lists。    [2010-07-14 17:03:38 +0800]
    • Josh Ko ⇒ 進入愛睏想吃飯模式了⋯    [2010-07-14 17:04:02 +0800]
  80. 剛剛 P 老師突然跑進來⋯    [2010-07-15 11:42:27 +0800]
  81. (accept a(k) in P₁ | request a(k) in P₂) → (νk) (P₁ | P₂)
    還不用 higher-order channels，這條語意就讓人傷腦筋了。    [2010-07-15 14:50:38 +0800]
    • Josh Ko ⇒ 很好，問題又回到 higher-order channels。現在是 ((νk) P) | Q ≡ (νk) (P | Q) 這條 structural congruence rule 令人討厭。    [2010-07-15 16:08:18 +0800]
    • Josh Ko ⇒ 還真的是 typable...    [2010-07-15 16:36:04 +0800]
    • S************ ⇒ 咦，你現在是在寫 operational semantics 嗎？    [2010-07-15 17:00:41 +0800]
    • Josh Ko ⇒ 目標是寫翻譯成 concurrent Haskell 的 interpreter。Service/name 比我想像中還麻煩，另外就是 channels 實際上怎麼丟的問題。    [2010-07-15 17:02:58 +0800]
  82. Max 要回 Oxford 嘍。    [2010-07-15 15:33:29 +0800]
  83. 莫名其妙地成功把 Vec A (suc n) 當成 non-empty lists 用了。    [2010-07-15 16:56:39 +0800]
  84. 呃，higher-order channels 的 index type 還沒寫⋯ 先準備收工好了 XD。    [2010-07-15 17:00:08 +0800]
  85. 對啊，其實用 unsafeCoerce 也沒差⋯    [2010-07-15 18:13:43 +0800]
    • Josh Ko ⇒ 欸，不過其實我不太會用 unsafeCoerce 耶 XD。比方說 do {m1 :: MVar () <- newEmptyMVar; m2 :: MVar () <- newEmptyMVar; forkIO $ do {m <- readMVar m1; x :: String <- readMVar (unsafeCoerce m); putStrLn x}; putMVar m2 (unsafeCoerce "hello, world"); putMVar m1 (unsafeCoerce m2)} 會跑不好的結果出來⋯    [2010-07-15 18:36:01 +0800]
    • Josh Ko ⇒ 編譯出來倒是 OK...    [2010-07-15 19:26:37 +0800]
    • S************ ⇒ 其實 type 的目的之一也包括：在 compile type 確定 type 不會錯，到 runtime 就可以不用加 label 了.    [2010-07-15 21:53:59 +0800]
  86. 可能還得用兩個 MVars 去做 synchronous channels 呦，可以想像 type safety 證明不會很好做⋯    [2010-07-16 09:53:51 +0800]
    • S************ ⇒ 不用吧，和 concurrent Haskell 一樣做 asynchronous 的就可以了呀...?    [2010-07-16 10:07:10 +0800]
    • Josh Ko ⇒ 我在想比方說 !N. ?N. bot 這種 client，要是沒有跟 server 做 sync 的話，有可能 client 一寫出去馬上拿回來？    [2010-07-16 10:50:53 +0800]
    • S************ ⇒ Arrrgh, you are right.
      What about using this:
      http://hackage.haskell.org/packages/archive/synchronous-channels/0.1/doc/html/Control-Concurrent-Chan-Synchronous.html    [2010-07-16 11:39:06 +0800]
    • Josh Ko ⇒ 好奸詐！就用這個！XD    [2010-07-16 11:45:57 +0800]
    • S************ ⇒ wait wait.. this is perhaps better: http://www.cs.kent.ac.uk/projects/ofa/chp/
      他們有出一些 paper, 比較有在 maintain, 說不定也有比較完整的semantics.    [2010-07-16 11:48:34 +0800]
    • Josh Ko ⇒ 不過我只找到 tutorial 和一篇 '08 的 paper 耶，裡面都沒有特別講 semantics 的樣子。
      Anyway, 我現在有一個 object language 嘍，待會要看一下嗎？    [2010-07-16 13:08:52 +0800]
  87. Urrgh, term does not reduce...    [2010-07-16 10:54:05 +0800]
    • Josh Ko ⇒ 卡得死死的⋯    [2010-07-16 11:14:50 +0800]
    • Josh Ko ⇒ 難怪之前 throw 要註解掉。    [2010-07-16 11:21:18 +0800]
    • Josh Ko ⇒ Yes! 換個 induction variable 就 reduce 了！    [2010-07-16 11:33:43 +0800]
    • 翁** ⇒ 喔~原來是這樣!!(亂入    [2010-07-16 11:46:22 +0800]
    • Josh Ko ⇒ 對啊，induction 還真的不能亂做 XD。    [2010-07-16 11:47:40 +0800]
    • 翁** ⇒ 我忘記帶考卷回來了!不然禮拜天可以研究XDD    [2010-07-16 11:48:10 +0800]
    • Josh Ko ⇒ 不是應該直接撕掉嗎？XD    [2010-07-16 11:48:34 +0800]
    • 翁** ⇒ 已經燒給上帝了....    [2010-07-16 11:49:02 +0800]
    • 翁** ⇒ 喔!!這樣講太不尊敬上帝了= ="請主原諒我....    [2010-07-16 11:49:34 +0800]
  88. Checkpoint reached. Shin I need you!!    [2010-07-16 14:47:52 +0800]
  89. 這就是 typeclass 的奇技淫巧⋯    [2010-07-16 15:48:45 +0800]   [ 1 人說讚！]
    • 翁** ⇒ 奇技淫巧...新成語嗎XD    [2010-07-16 16:08:41 +0800]
    • Josh Ko ⇒ 我常用耶 XD。
      http://dict.idioms.moe.edu.tw/mandarin/fulu/dict/cyd/5/cyd05615.htm    [2010-07-16 16:10:43 +0800]
    • 翁** ⇒ 哇靠= ="還真的...我還以為你打錯字之類的...    [2010-07-16 16:15:25 +0800]
    • S************ ⇒ Andres 有篇 paper 開頭是這樣寫的:

      Most Haskell programmers are hesitant to program with dependent types. It is said ... that dependent types are really, really hard.

      The same Haskell programmers, however, are perfectly happy to program with a ghastly hodgepodge of generalized algebraic data types, multi-parameter type classes with functional dependencies, impredicative higher-ranked types, and even data kinds. They will go to great lengths to avoid dependent types.    [2010-07-16 17:00:40 +0800]
    • Josh Ko ⇒ 這就是原文嘍 XD。    [2010-07-16 17:04:28 +0800]
    • L*********** ⇒ just like c++ templates... hahaha. see those crazy templates reside in boost!!    [2010-07-16 17:22:35 +0800]
    • 賴* ⇒ 淫巧⋯?    [2010-07-17 01:00:12 +0800]
  90. Löh, McBride, 和 Swierstra 的 Simply Easy paper 開場說一堆 Haskell programmers 覺得 dependent types 難到爆，可是這一批 Haskell programmers 又不亦樂乎地搞 GADTs, multi-parameter type classes with functional dependencies, impredicative higher-ranked types, data kinds 這些鬼東西，就是不要用 dependent types。中肯⋯    [2010-07-16 16:45:15 +0800]   [ 3 人說讚！]
  91. 出門，希望趕在護照效力不滿六個月之前辦好台胞證 XD。    [2010-07-17 15:17:58 +0800]
  92. 「出國時護照須有六個月以上效期」似乎真有其事，這下我慘了⋯    [2010-07-17 18:46:39 +0800]
  93. 而且飛北京的機票竟然還要候補！    [2010-07-17 19:03:16 +0800]
    • 王** ⇒ 要自己出錢嗎？？ 還是有補助阿XD    [2010-07-17 19:07:26 +0800]
    • 翁** ⇒ 我先去探路了!感覺下午逛不完!!!!    [2010-07-17 19:08:15 +0800]
    • Josh Ko ⇒ 欸⋯ 難道要現在跳上國光客運嗎？XD    [2010-07-17 19:14:59 +0800]
    • 翁** ⇒ 哈哈~歡迎阿XDD    [2010-07-17 19:15:17 +0800]
    • Josh Ko ⇒ 現在去應該只搭得到九點的車，到那裡就半夜啦⋯ 還是搭明天早上八點的車好了 XD。    [2010-07-17 19:19:50 +0800]
    • 翁** ⇒ 看你瞜~    [2010-07-17 19:20:44 +0800]
    • S************ ⇒ 看來一切難度都很高.. 加油囉..    [2010-07-17 21:03:51 +0800]
    • L************** ⇒ 不要求直飛北京的話，可以轉機啦 ...可以排時間在香港逗留一下下。    [2010-07-19 22:16:31 +0800]
    • Josh Ko ⇒ 旅行社說 19 號沒有直飛，所以只能轉機 XD。    [2010-07-19 23:34:33 +0800]
  94. 我在中興，天氣晴。中興才是適合人居住的地方呀…    [2010-07-18 10:55:10 +0800]   [ 1 人說讚！]
    • 王** ⇒ 驚!那你晚上要住哪裡?    [2010-07-18 17:50:42 +0800]
    • Josh Ko ⇒ 琦皓房間 XD。    [2010-07-18 22:44:37 +0800]
    • 王** ⇒ 嗯嗯    [2010-07-18 23:16:15 +0800]
  95. 多情應笑我，易湧熱淚… ↦ Trek through Pure Reason: 潰堤    [2010-07-19 18:39:11 +0800]   [ 1 人說讚！]
    • L********* ⇒ 真情流露    [2010-07-19 22:07:39 +0800]
  96. 可以先用舊護照辦完簽證再換照！而且去北京的機票候補到了！（不要到時候跟我說旅館訂不到…）    [2010-07-19 18:45:17 +0800]
    • J******************* ⇒ 怎麼覺得你的北京之旅一直都充滿危機...?XD    [2010-07-19 18:51:53 +0800]
  97. 聽說北辦會計處常打電話下來的專門委員在我退伍當天離開後半小時打電話下來指定找我聊天，可惜沒接到。這位專門委員感覺上挺有趣的。    [2010-07-19 23:40:15 +0800]
  98. 「不用向、佳人訴離恨，淚珠先已凝雙睫。」摘自東坡〈滿江紅〉（正月十三日，雪中送文安國還朝）。大四唸東坡詞還無法感同身受東坡離別詞內頻繁出現的淚水，現在似乎是重讀這些詞的好時機了。    [2010-07-19 23:46:07 +0800]
  99. 今天晚上吃得有點晚，回到台北沒車可搭，所以明早才搭車北上。    [2010-07-19 23:46:44 +0800]
  100. 先不要把神奇的新功能加進去好了，照最原始的計畫先走一遍再說。    [2010-07-20 16:05:29 +0800]
    • Y********** ⇒ 我有點好奇「神奇的新功能」是什麼? XD    [2010-07-20 17:48:23 +0800]
    • Josh Ko ⇒ 請期待週五 scm 老師變魔術！XD    [2010-07-20 17:50:15 +0800]
    • Y********** ⇒ 可以把Mac Book變成Mac Book Pro嗎?(OS當然順便變成10.6) XD    [2010-07-20 18:48:34 +0800]
  101. 回中辦被餵得十足飽，現在總算餓了。    [2010-07-20 16:11:18 +0800]
  102. 約週四早上八點辦簽證。簽證費漲到一萬元整了⋯    [2010-07-20 18:33:04 +0800]   [ 2 人說讚！]
    • S************ ⇒ WHAT?!    [2010-07-20 21:17:05 +0800]
    • L************** ⇒ 英鎊明明就跌了 @_@    [2010-07-20 22:06:55 +0800]
  103. 給我一個很差的 CAS number，結尾是 08O0IX，O0 手寫很難分⋯    [2010-07-21 09:33:47 +0800]
    • 翁** ⇒ 數字0的中間可以畫一槓斜線?    [2010-07-21 09:46:10 +0800]
    • Josh Ko ⇒ 我目前是這樣寫沒錯，不過看起來好怪 XD。    [2010-07-21 09:49:04 +0800]
    • 翁** ⇒ 那寫國字吧XD    [2010-07-21 10:07:45 +0800]
    • Josh Ko ⇒ 可惜表是英文的 XD。    [2010-07-21 10:11:00 +0800]
  104. 圖書館的自動饋紙器把紙吐出來的時候好暴力，不像中辦的出來是整齊一疊。    [2010-07-21 10:10:25 +0800]
    • W************ ⇒ 不然是用噴的喔?    [2010-07-21 12:53:42 +0800]
    • Josh Ko ⇒ 對啊，很隨便，可惜沒有影印機管幹可以電它 XD。    [2010-07-21 12:54:22 +0800]
  105. 終於把簽證文件整理完了，耗時一個半鐘頭。    [2010-07-21 10:27:07 +0800]
  106. 剛剛要接螢幕才發現被人換掉了⋯    [2010-07-21 11:09:39 +0800]
    • Josh Ko ⇒ 雖然變成 DVI 接頭很好，可是我沒有 mini displayport to DVI 的轉接器⋯    [2010-07-21 11:13:13 +0800]
    • S************ ⇒ 啊？換到哪去了？    [2010-07-21 14:25:39 +0800]
    • Josh Ko ⇒ 不知道耶，雖然也是 DELL 24"，可是機種不一樣了。    [2010-07-21 14:29:11 +0800]
    • F************ ⇒ 貼張紙條寫 "請再換高級一點的", 也許明天就變HDMI了 :D    [2010-07-21 20:53:13 +0800]
    • 翁** ⇒ 那可以通通都貼嗎XDD!!整個換新的@@"    [2010-07-22 08:42:17 +0800]
  107. 編譯成功！第一階段實驗完成 XD。    [2010-07-21 12:53:42 +0800]
  108. 應該也不需要特別避開 unsafeCoerce 啦，Agda 自己就用得很兇。編出來一個檔案裡面有 1,067 個 unsafeCoerce⋯    [2010-07-21 13:04:24 +0800]
  109. 現在覺得 terms 和 types 分開寫的做法不是很好，可是 terms 和 types 分開考量又是很好的方向。欸，所以要開始做 datatype ornamentation 了？XD    [2010-07-21 14:34:09 +0800]
  110. 還是不能用簡單的 MVar 語意推得目前這種用兩個 MVars 的 synchronous channels 真的是 synchronous。    [2010-07-21 14:53:45 +0800]
    • Josh Ko ⇒ 用三個 MVars 好像就可以了！    [2010-07-21 15:00:29 +0800]
  111. 社工人力案怎麼有點像小強，一直打不死⋯？    [2010-07-21 15:27:33 +0800]
    • 翁** ⇒ 晚上7點過後還是關機吧......    [2010-07-21 15:57:17 +0800]
    • Josh Ko ⇒ 可是已經約好啦，希望這次打得死 XD。    [2010-07-21 16:04:41 +0800]
    • 翁** ⇒ 別忘了boss有兩隻!除了社工人力案!還有一個隱藏女角XDD你可能要拿黃金巨鎚才有辦法!    [2010-07-21 16:34:36 +0800]
    • Josh Ko ⇒ HIKARI NI NARE!!!    [2010-07-21 21:04:38 +0800]
  112. 簽證申請資料交出去了。 ↦ Trek through Pure Reason: 再戰商業區    [2010-07-22 10:10:35 +0800]
  113. 突然想不太通，bound variables 跑到哪裡去了？    [2010-07-22 15:44:15 +0800]
    • Josh Ko ⇒ Evaluate 出來就是啦！    [2010-07-22 15:48:01 +0800]
  114. 所以說不定包一層 extended terms 上去就可以了！    [2010-07-22 16:27:20 +0800]
  115. Universe polymorphism 光現在這樣就已經很讓人滿足啦！    [2010-07-23 09:47:36 +0800]
  116. 既然有了 safe indices，就不用 Vec 啦！把 Vec 全丟了！    [2010-07-23 14:40:36 +0800]
  117. 看來偷懶不得，term 還是只能乖乖裝兩層⋯    [2010-07-23 16:15:46 +0800]
    • Josh Ko ⇒ 嗎？XD    [2010-07-23 16:52:53 +0800]
    • Josh Ko ⇒ 不用耶，binders 根本不用管，本來的計畫還有可能 work XD。    [2010-07-23 16:57:36 +0800]
    • Josh Ko ⇒ 如果沒有 throw 的話⋯    [2010-07-23 16:58:58 +0800]
    • S************ ⇒ 哎哎，我都跟不上... 時間都花在趕國科會報告。 :( 如果有東西可以 summarise 一下的話請寫給我吧，不然下週聊！    [2010-07-23 17:19:16 +0800]
    • Josh Ko ⇒ 離做出來還很遠呢，都在構思階段而已 XD。    [2010-07-23 17:19:55 +0800]
  118. 想到好像很好玩的 trick，不知道會不會變得太複雜。    [2010-07-23 17:07:39 +0800]
    • Josh Ko ⇒ 三種 channels/terms 互相混合！    [2010-07-23 17:11:04 +0800]
    • 翁** ⇒ 會有火花嗎XD    [2010-07-23 17:13:31 +0800]
    • Josh Ko ⇒ 變得太複雜的話我的七竅會爆出火花 XD。    [2010-07-23 17:15:33 +0800]
    • 翁** ⇒ 火雲邪神!!!    [2010-07-23 17:17:43 +0800]
  119. 拿到台胞證，機票也開了。下一步是等 PBS Tier 4 學生簽證回來，馬上去換照。時間應該會剛剛好⋯    [2010-07-24 21:42:37 +0800]   [ 2 人說讚！]
    • Josh Ko ⇒ 應該不會給我來個拒簽吧⋯    [2010-07-24 22:02:52 +0800]
    • 翁** ⇒ 現在正一邊吃麥當當一邊惡補"日記"第4篇XDD
          [2010-07-24 22:14:38 +0800]
  120. 陳錦源很敷衍耶！XD ↦ 班報出刊ㄌ~~~~    [2010-07-25 19:40:50 +0800]
    • R********** ⇒ 可是我覺得很符合他的風格啊 XD 我還有看到小雀雀和周文釗 XD    [2010-07-25 22:29:06 +0800]
  121. 我現在好像在手工做某種 typeclass...    [2010-07-26 10:25:28 +0800]
  122. 我看還是做三組 Terms 好了，Agda 處理這麼複雜的 type indices 好像還是很吃力。    [2010-07-26 11:16:10 +0800]
    • Josh Ko ⇒ 或者也可以說我寫得很吃力 XD。    [2010-07-26 11:16:32 +0800]
  123. 好像兩組就行。    [2010-07-26 11:49:44 +0800]
  124. 哇，爆了！Set 上沒有 decidable equality...    [2010-07-26 14:05:16 +0800]
    • Josh Ko ⇒ 爆得很燦爛⋯    [2010-07-26 14:20:03 +0800]
  125. 拐彎中。    [2010-07-26 14:39:19 +0800]
  126. 好像拐過去了，但後面說不定有更兇猛的 XD。    [2010-07-26 15:03:27 +0800]
  127. 應該要先來測試一下 first-order read/write 寫不寫得出來。    [2010-07-26 15:23:46 +0800]
    • Josh Ko ⇒ 可以的樣子！    [2010-07-26 15:40:33 +0800]
    • 王** ⇒ 用什麼決定優先權?    [2010-07-26 16:13:55 +0800]
    • Josh Ko ⇒ 先確定一下簡單的情況有沒有處理成功再繼續往前 XD。    [2010-07-26 16:20:13 +0800]
  128. 這樣應該可以繼續進攻 higher-order channels。    [2010-07-26 15:51:01 +0800]
  129. Data.List.All 沒改成 universe polymorphic...    [2010-07-26 16:02:11 +0800]
  130. 把 channels 全部改成簡化版。Higher-order free channels 明天吧⋯    [2010-07-26 16:53:23 +0800]
    • Josh Ko ⇒ catch 算是 binder，接進來的 channel 只讓它變成 bound channel。但 throw 好像就得做四個版本⋯    [2010-07-26 16:57:39 +0800]
    • Josh Ko ⇒ 目前看起來是有希望做得出來啦！    [2010-07-26 17:08:00 +0800]
  131. 很好，我現在也覺得不用 +1 好奇怪了。    [2010-07-26 22:35:16 +0800]
    • L********* ⇒ 開始中FB的毒了嗎？還是我會錯+1的意義了 XDD    [2010-07-26 22:39:57 +0800]
    • Josh Ko ⇒ 是跟調整 "De Bruijn index" 有關的東西 XD。
      http://en.wikipedia.org/wiki/De_Bruijn_index    [2010-07-26 22:46:39 +0800]
    • S************ ⇒ 用 \x -> \y -> y x 試試看吧～    [2010-07-26 23:11:39 +0800]
  132. 死了，又撞到一個 undecidable equality！    [2010-07-26 23:40:03 +0800]
  133. "no (λ ())" 翻譯：不可能，不然你做給我看啊！    [2010-07-27 09:06:33 +0800]   [ 4 人說讚！]
    • R********** ⇒ 我笑了 XD    [2010-07-27 14:54:14 +0800]
    • Josh Ko ⇒ 先把「做」改成「變」，最後面可以再加個「變不出來嘛！」XD    [2010-07-27 15:48:30 +0800]
    • R********** ⇒ 翻譯：不可能，不然你變給我看啊！ 變不出來嘛！」 XD    [2010-07-27 16:00:11 +0800]
  134. I have the terms. Now it's time for some magic.    [2010-07-27 09:34:42 +0800]
    • 王** ⇒ 小鐘:magic    [2010-07-27 10:10:11 +0800]
  135. 魔術果然不好變，要證的東西可多了。    [2010-07-27 10:01:56 +0800]
  136. 戰線看來得拉很長了。    [2010-07-27 10:30:19 +0800]
  137. 為「兩個 lists 長度相等」新寫一個 inductive predicate，才不用處理「cong pred (cong suc p) 和 p 一不一樣」的問題⋯    [2010-07-27 12:44:22 +0800]
  138. 最新簽證進度："Processed application in transit"。透露一下結果也沒關係吧⋯    [2010-07-27 15:06:07 +0800]
  139. 扭來扭去還真的扭出來，可是我還真的不知道為什麼扭得出來⋯    [2010-07-27 15:33:47 +0800]
    • Josh Ko ⇒ 簡單說就是「莫名其妙」。    [2010-07-27 15:35:31 +0800]
  140. 命運的 postulate uniq : ∀ {fc a Δ} → (c₁ c₂ : FChannel₁ fc a Δ) → c₁ ≡ c₂ — 看來只好把 FTyping 整修一番了。但整修之前還是先確定關鍵功能寫得出來，不然整修不是什麼小工程⋯    [2010-07-27 15:40:14 +0800]
  141. 聽蕭邦修補一下腦細胞⋯    [2010-07-27 15:57:19 +0800]
  142. Dependently-typed programs 的 reusability 確實不好，到目前為止難解的問題都是新做一個 datatype 就解掉了，原本用 general-purpose datatypes 造出來的東西都十分難證。    [2010-07-27 20:44:50 +0800]
  143. 今晚的夢大概又會在那裡鬼打牆地數 De Bruijn indices 了 XD。    [2010-07-27 20:53:03 +0800]
    • Josh Ko ⇒ Throw 系列四句已成其三，最痛苦的「透過 free channel 丟 free channel」還是留到明早精神好點再弄吧⋯    [2010-07-27 20:55:47 +0800]
  144. 雨停了⋯    [2010-07-28 08:27:53 +0800]   [ 2 人說讚！]
    • Josh Ko ⇒ 出發和 throw 的第四句奮戰 XD。    [2010-07-28 08:30:56 +0800]
  145. 之前還沒發現 higher-order write 的第一個 parameter 是 inductive，所以不能把自己丟出去！    [2010-07-28 09:10:46 +0800]
  146. 結果排除 self-throw 的情況後，也只是依樣畫葫蘆而已。現在開始怕其他 constructs 其實比較難 XD。    [2010-07-28 09:27:52 +0800]
  147. Oh yeah! 剩下 binders。這個要來動一動 typing 裡面 entries 的順序。    [2010-07-28 09:49:24 +0800]
    • Josh Ko ⇒ 需要的應該是「交換任兩個 entries」的能力。    [2010-07-28 10:02:36 +0800]
  148. 只剩下 swap 沒寫出來嘍，這樣算滿順利的吧。    [2010-07-28 13:48:01 +0800]
    • Josh Ko ⇒ 現在的 code 在 MBP 上竟然還 typecheck 到讓人懷疑是不是當掉的境地⋯    [2010-07-28 13:58:48 +0800]
    • Josh Ko ⇒ 不敢想像用 PB typecheck 會變成怎樣 XD。    [2010-07-28 13:59:12 +0800]
  149. 現在 ghc 在一顆 physical core 上面跑 100%，另一顆閒著。這樣一半燙一半涼會裂掉嗎？XD    [2010-07-28 14:04:00 +0800]
  150. Typechecker 整個掛在那邊沒回應。可能是該分成兩個檔案了吧⋯    [2010-07-28 14:10:08 +0800]
  151. 難道我的 code 讓 typechecker 陷入萬劫不復之無窮迴圈⋯ ?!    [2010-07-28 14:16:22 +0800]
    • Josh Ko ⇒ postulate swap 好像會讓 typechecker 爆掉。    [2010-07-28 14:20:07 +0800]
  152. 第三次翻修要開始了。    [2010-07-28 15:03:25 +0800]   [ 1 人說讚！]
  153. 連 strict positivity 都出來參一腳呀⋯    [2010-07-28 16:05:38 +0800]
  154. 今天一口氣把 second pass 衝到告一段落，還有點累⋯    [2010-07-28 17:06:41 +0800]
    • S************ ⇒ 辛苦啦～真是好快唷！    [2010-07-28 19:49:12 +0800]
  155. 還以為關鍵的 uniqueFChannel : ∀ {fc a Δ} → (c₁ c₂ : FChannel fc a Δ) → c₁ ≡ c₂ 證不出來，虛驚一場。（不過得對 a 做 pattern matching 還滿怪的。）    [2010-07-28 19:15:33 +0800]
    • 翁** ⇒ 快去買星海來玩!!!去英國之後可以一起連線XD你的英國同學也一定在玩這個!!(亂入...    [2010-07-28 19:33:45 +0800]
    • Josh Ko ⇒ 玩下去的話我一年就被趕回來了吧 XD。    [2010-07-28 19:42:20 +0800]
    • 翁** ⇒ 應該沒那麼誇張吧XD我相信你自治能力~!    [2010-07-28 19:44:07 +0800]
    • Josh Ko ⇒ 那修正為兩年被趕回來好了 XD。    [2010-07-28 19:44:57 +0800]
    • 翁** ⇒ XDD剛好學成歸國!!!    [2010-07-28 19:47:31 +0800]
    • A*********** ⇒ : ?! did mu told you that we hope you can break max's record... get your ox phd in 2.6 yr!     [2010-07-28 20:08:10 +0800]
    • F************ ⇒ 不,你要達到兩年內因為教授沒東西能教人被趕回來!    [2010-07-28 20:12:40 +0800]
    • 翁** ⇒ 我1月想去澳洲+英國!會不會太拼XDD
      樓上要玩星海嗎~~~    [2010-07-28 20:31:27 +0800]
    • Josh Ko ⇒ @ Andrea: 蛤，我還在想到底能不能畢業耶 XD。
      @ 喵：同上 XD。
      @ 琦皓：會 XD。    [2010-07-28 21:11:35 +0800]
    • 翁** ⇒ 沒畢業就回中辦啦XDD    [2010-07-28 21:43:12 +0800]
    • F************ ⇒ 星海 不在我的範圍內 @@

      (X的星海擋我D3去路!)    [2010-07-28 23:13:55 +0800]
    • W************ ⇒ ==     [2010-07-28 23:20:37 +0800]
  156. 好恐怖，只是寫個 typing update function (fproceed) 就非得用 mutual induction 不可，還要一個反面的 lemma，就和所有反面證明一樣得轉一圈才想得通。chenk 老師說做這行就是 induction 愈做愈神妙，還真是沒說錯。    [2010-07-28 21:02:45 +0800]
    • L************** ⇒ transfinite induction 呢？XD    [2010-08-07 09:37:27 +0800]
  157. 喔，Tier 4 簽證回來了！明早八點去拿，順便換護照。（不要拒簽⋯）    [2010-07-28 21:29:20 +0800]   [ 2 人說讚！]
    • Josh Ko ⇒ 這次要記得搭左側的電梯 XD。    [2010-07-28 21:30:58 +0800]
  158. 有內線消息嗎？ ↦ Book: Pearls of Functional Algorithm Design | Lambda the Ultimate    [2010-07-28 23:43:06 +0800]
    • Y********** ⇒ 想知道內線消息+1 :p    [2010-07-29 00:15:03 +0800]
    • S************ ⇒ 並沒有耶，我只知道他一直在寫這個書有一陣子了，不知道完稿了沒。    [2010-07-29 22:39:42 +0800]
  159. UK entrance clear! 馬上就把護照丟到旅行社去換了。    [2010-07-29 10:12:09 +0800]
  160. 突然想到要動順序（做 swap）的 typing 是 bound typing 而不是 free typing，這樣就不用在那裡橋 freshness proofs 啦，萬歲！    [2010-07-29 15:43:22 +0800]
  161. 目前看來這一階段的魔王還是 swap，「free channel typing 新鮮與否」的影響沒有預期的那麼廣。    [2010-07-29 16:48:59 +0800]
  162. 沙盤推演一下 swap 怎麼寫，還真的滿困難的。繼續推，發現如果把 bound typing 追加成三個的話，應該就寫得出來。可是這代表 intermediate terms 總共會有 4 個 typings（3 個 bound、1 個 free），有點恐怖，還是先看一下前人是怎麼做的吧。如果最後還是要用這種 terms，我決定把它叫做 "troll terms" XD。    [2010-07-29 17:54:42 +0800]
    • Josh Ko ⇒ 想到一個想起來好一點的辦法，應該可以不用去做「山怪項」XD。    [2010-07-29 18:46:21 +0800]
  163. 正在用好久不見的 ≡-Reasoning，突然下起暴雨⋯    [2010-07-29 19:39:33 +0800]
    • Josh Ko ⇒ 修正，是暴雷雨⋯    [2010-07-29 19:46:52 +0800]
  164. Troll terms 實作過程應該滿機械化的，但跑起來慘不忍睹。現在繞經 Fin (length Δ) 則得證不少涉及數字的引理，但寫得出來的話效能應該會滿正常。希望寫得出來⋯    [2010-07-29 20:02:37 +0800]
    • S************ ⇒ 確認一下唷.. 你現在要證的 swapping 是哪個？是 free variable 的 context 內容可以互換，但仍然 well-form 這件事情嗎？    [2010-07-29 22:44:27 +0800]
    • Josh Ko ⇒ 是 bound channels。Free channels 剛好不用換順序，所以省下很多工夫。    [2010-07-30 03:52:05 +0800]
  165. 再退一步，只用 Nat...    [2010-07-30 10:15:39 +0800]
  166. 寫現在這種 "externalist code" 好像又回到 AoPA 時代。    [2010-07-30 11:22:49 +0800]
    • Josh Ko ⇒ 不過現在有 rewrite 有稍微更愉快一點 XD。    [2010-07-30 11:32:23 +0800]
  167. 現在寫起來還算順利，途中需要的性質都變得出來。    [2010-07-30 11:30:51 +0800]
  168. 這樣可能是我的 typing 放反了 XD。    [2010-07-30 14:26:25 +0800]
  169. 喔，死了，new 要多兩個 channels 出來⋯    [2010-07-30 14:58:03 +0800]
    • Josh Ko ⇒ 咦，沒差啦，虛驚一場 XD。    [2010-07-30 14:58:50 +0800]
  170. inject 比我想像中要難很多⋯    [2010-07-30 16:02:10 +0800]
  171. 火車上把 bound write 寫出來了，要證好幾個 lemmas 而且還非得用 subst 明確轉型不可。不知道有沒有好看一點的辦法。    [2010-07-30 21:46:36 +0800]
    • S************ ⇒ 把 index 方向弄對之後有比較好寫嗎？    [2010-07-31 07:29:45 +0800]
    • Josh Ko ⇒ 應該不用寫 swap 了，可是 type 上變得很難，得轉來轉去（因為 channel c 改成 inject c，後面全部的 types 都跟著變）。    [2010-07-31 08:45:30 +0800]
    • S************ ⇒ inject 是什麼呀？    [2010-07-31 08:53:43 +0800]
    • Josh Ko ⇒ 本來 c 是 Δ 的某個 de Bruijn index，inject c 是擴充後的 typing Δ ++ [ t ] 的 de Bruijn index，指的和本來 c 指向的東西一樣。    [2010-07-31 09:47:32 +0800]
  172. Heterogeneous equality to the rescue?!    [2010-07-31 17:33:17 +0800]
  173. 在開放免費下載的 MechWarrior 4 裡組一隻純粹火力沒有裝甲的 Atlas，打開無熱度無敵模式，瞄準就把重型小雷射、脈衝小雷射、大型連發雷射、重擊雷射、粒子砲、輕高斯砲、重高斯砲、和三組長程飛彈（每波發出 55 枚）一股腦地丟過去，打爆了幾十隻 Mechs。 ↦ Mechwarrior 4 Free Release    [2010-07-31 23:08:27 +0800]
    • Josh Ko ⇒ 明天把重高斯砲換成自動加農砲，看對手能不能更快爆掉。    [2010-07-31 23:17:31 +0800]
    • 陳** ⇒ 完了，我看到Atlas就會想到自動最佳化的BLAS....XD    [2010-07-31 23:45:20 +0800]

--
之後應該是每週一次吧，這樣兩個月一次倒出來很恐怖 XD。

發現 scm 老師的 comments 完全沒出現，看來 Graph API 會看各個使用者的隱私權設定。

--
可是這樣就不能收藏 scm 老師的箴言啦⋯

依據 godfat 的指示拿到有 read_stream 權限的 access token 之後，現在看得到全部的 comments 了！不過寫起來複雜一點，得要 feed 和 statuses 兩個檔案互相對照才行。

--
現在還得自己抓檔案下來，以後自動化程度應該會愈來愈高才對 XD。

Labels:

posted by Josh Ko @ 4:52 pm   2 項意見

Blogger Lin Jen-Shin (godfat) 在 8/06/2010 5:39 pm 說：

try https://graph.facebook.com/Josh.HS.Ko/statuses ?

不過我的 comments 好像也沒出現耶？
真奇怪，我個人是全部設成 public 其實..
(除了少數幾個例外)

 
Blogger Josh Ko 在 8/07/2010 3:44 am 說：

喔，真的耶，癥結在於 access tokens!

拿到有 read_stream 的 access token 之後全部資訊就出現了。

 

<< 回到主頁