[facebook digest] 團購

1. 第一條 accept/request rule 還算簡單地過關了，雖然得回去修正幾條定義⋯    [2010-08-13 14:58:22 +0800]
2. (First-order) communication rule 也過了。有寫 let ... in ... 喔！XD    [2010-08-13 15:42:51 +0800]
3. P -> P' => new P -> new P' 就相當有趣了⋯    [2010-08-13 16:27:20 +0800]
4. 為什麼 Yoshida 證明 subject reduction 性質的時候沒有討論 scope rule?!    [2010-08-13 16:36:03 +0800]   [ 1 人說讚！]
5. 耶！Andreas Abel 在 Agda mailing list 上回我了。可是他（果然）叫我弄個小一點的例子出來⋯    [2010-08-14 00:04:08 +0800]   [ 2 人說讚！]
6. 看到「中選會團購花博票」一時反應不過來，然後才想到其實和「研考會訂便當」是同樣道理嘛。    [2010-08-16 12:42:43 +0800]   [ 1 人說讚！]
   • Josh Ko ⇒ 或是「會計處訂便當」XD。    [2010-08-16 12:47:03 +0800]
7. rename lemma 可以用！再來要煩惱 dual => cotype 怎麼證⋯ 另外就是 new 的 term 不應該放 channel type 上去才對。    [2010-08-16 16:27:24 +0800]
8. 好像無法避免 Type 的 bisimulation 了⋯？    [2010-08-16 17:29:22 +0800]   [ 1 人說讚！]
9. 電梯裡的 Professor C.-C. Jay Kuo 被人畫上牛角 XD。    [2010-08-17 10:08:45 +0800]   [ 1 人說讚！]
10. 閉著眼睛亂寫 induction + coinduction。    [2010-08-17 14:16:13 +0800]
11. 確實，剛剛繞路繞得太遠了。    [2010-08-17 15:43:52 +0800]
12. 打算鎖定練習的 Chopin Mazurki: Op. 50 No. 3, Op. 63 No. 2, Op. 33 No. 4, Op. 17 No. 2, Op. 41 No. 1.    [2010-08-17 23:04:37 +0800]
    • Josh Ko ⇒ 更正：Op. 41 No. 1 應為 No. 2.    [2010-08-17 23:13:39 +0800]
    • Josh Ko ⇒ 結果是各版編號不同所致：把我要練習的 e 小調馬厝卡標為 No. 2 的是德國初版，而波蘭國家版覺得前者的 No. 1 應該擺到最後變成 No. 4，e 小調馬厝卡就變成 No. 1 了。    [2010-08-17 23:32:45 +0800]

--
明天去北京。