2010/09/14

[facebook digest] 再訪中辦

  1. typing-split-l (pass-cxt s c∈) (Δ !! ∈-inj-l s i ↦ t') ≡ typing-ins c .t (pass-idx s c∈) (typing-split-l s Δ !! i ↦ t') 看起來很難拆成小 lemmas 來證啊⋯    [2010-09-07 16:30:09 +0800]
    • S************ ⇒ typing-ins 是新定義的東西嗎？    [2010-09-07 16:43:35 +0800]
    • Josh Ko ⇒ 對呀，因為本來 typing rules 裡面的 catch 只要求接到的 channel 擺在最前面，但實際上需要的 induction hypothesis 要能擺在任意位置，所以就把 catch rule 改掉了，typing-ins 就是用來把 c : t 插在任意位置的 function。    [2010-09-07 16:48:20 +0800]
    • Josh Ko ⇒ 還有：darcs repository 好像壞掉一陣子了！    [2010-09-07 16:50:03 +0800]
    • S************ ⇒ 啊？怎麼個壞法？    [2010-09-07 22:34:34 +0800]
    • Josh Ko ⇒ darcs failed: Not a repository: agda@pc-scm.iis.sinica.edu.tw:/Users/Shared/Concurrency ((scp) failed to fetch: agda@pc-scm.iis.sinica.edu.tw:/Users/Shared/Concurrency/_darcs/inventory)    [2010-09-07 22:35:06 +0800]
  2. 16 cases are first reduced to 7 by reductio ad absurdum, and then each of the remaining cases requires 4 rewrites before applying the assumption.    [2010-09-07 21:37:30 +0800]
    • Josh Ko ⇒ Perhaps more than that. XD    [2010-09-07 21:44:54 +0800]
    • Josh Ko ⇒ I am shocked by my using such nonsensical with-matchings/rewrites!    [2010-09-07 22:02:27 +0800]
    • Josh Ko ⇒ 有點像遊戲王裡面發動魔法卡陷阱卡怪獸效果大連鎖的感覺 XD。    [2010-09-07 22:03:31 +0800]
    • Josh Ko ⇒ More reductio ad absurdum!    [2010-09-07 22:09:17 +0800]
    • Josh Ko ⇒ 3 cases remain; others are closed by reductio ad absurdum.    [2010-09-07 22:34:37 +0800]
  3. 我猜今天海苔飯捲沒開，緊急全部改訂兄弟 XD。    [2010-09-08 12:47:48 +0800]
    • 賴* ⇒ 錯．．．．．．．他今天人手少　沒辦法外送．．    [2010-09-08 13:58:28 +0800]
    • Josh Ko ⇒ 也差不多啦 XD。    [2010-09-08 15:03:58 +0800]
    • 賴* ⇒ 向上　你這預言是怎麼算出的．．．．    [2010-09-08 15:33:53 +0800]
    • Josh Ko ⇒ 我十點多看到兄弟超時還開著，便當量還在增加，之後海苔飯捲被刪掉了 XD。現在看兄弟的明細的話可以看到 10:07 到 10:23 之間有空檔，之後幾個科室突然灌進來，模式就像是集體改訂 XD。    [2010-09-08 15:57:34 +0800]
    • 賴* ⇒ 你還去訂便當系統喔　    [2010-09-08 16:12:20 +0800]
    • Josh Ko ⇒ 習慣了，把它當 blog 看 XD。    [2010-09-08 16:17:14 +0800]
    • Josh Ko ⇒ 如果你們用那個「群組熱線」成立一個中辦新聞台就完美了 XD。    [2010-09-08 16:19:09 +0800]
    • 賴* ⇒ 我會跟　未民說的　哈哈    [2010-09-08 16:19:57 +0800]
  4. postulate cotype-idem : ∀ {t} → t ≡ cotype (cotype t) -- in fact problematic (due to intensionality)    [2010-09-08 17:37:36 +0800]
    • Josh Ko ⇒ 不知道這會帶來多大問題耶。    [2010-09-08 18:31:23 +0800]
    • S************ ⇒ 沒關係啦...    [2010-09-08 22:34:10 +0800]
    • Josh Ko ⇒ 假裝有 observational equality 嗎？XD    [2010-09-08 22:37:21 +0800]
    • S************ ⇒ 我們可以宣告一個 datatype, 定一個像 bisimulation 的 equality: (0 = 0, & f = & g if f x = g x for all x), 然後把所有用在 Type 的 ≡ 都換成這個 equality. 有些 substitution 定裡可能要自己證，我想應該是證得出來的。但有優先性更高的事情要做啦...    [2010-09-09 18:35:05 +0800]
  5. 為了找不到官方文字的規定去照一張胸腔 X 光片（一週後還要去拿診斷書），超大一張，到時候難拿了。    [2010-09-09 15:48:41 +0800]
    • L************** ⇒ 可以用製圖筒裝。    [2010-09-09 16:27:19 +0800]
    • Josh Ko ⇒ 現在另一個疑問是膠片可以過機場安檢的 X 光機嗎？好像可以但又怕到時拿出來一片模糊 XD。    [2010-09-09 16:29:33 +0800]
    • 陳** ⇒ 就順便做個胸腔檢查也不錯啦XD    [2010-09-09 17:06:11 +0800]
    • L************** ⇒ 你可以問他底片可不可以過 X 光，還是要人工檢查。    [2010-09-09 17:07:19 +0800]
  6. 昨天拿到鄧泰山新錄的蕭邦馬厝卡全集。目前聽到的幾首都挺柔的，但有可能是因為聽慣了傅聰的強勁版吧。    [2010-09-09 16:42:59 +0800]
  7. 剛才成功解決 pass rule，整個 type preservation theorem 只剩下 structural congruence 啦。（我現在覺得 Distinct xs 這樣散在各處似乎帶來不必要的困擾。）    [2010-09-09 19:49:49 +0800]   [ 1 人說讚！]
    • Josh Ko ⇒ 所以下一步是把 structural congruence rules 老老實實全部寫出來嗎⋯？    [2010-09-09 19:55:30 +0800]
    • S************ ⇒ Hmm... Run.agda 有沒有更新呀？先弄那邊好了.. structural congruence 也是很 routine 的工作..    [2010-09-09 23:08:25 +0800]
  8. 一直到剛剛才發現 Jeremy 的 college 名字譯成中文是家樂氏學院！（供應的餐點都是麥片？）    [2010-09-09 20:31:03 +0800]   [ 2 人說讚！]
    • L********* ⇒ 每天吃麥片、看麥片、玩麥片 XD    [2010-09-09 23:40:43 +0800]
  9. 國際學生證寄到了，上面有一層膠膜，直覺要把它撕掉，才發現上面有防撕防偽的設計。    [2010-09-11 10:12:52 +0800]   [ 2 人說讚！]
    • C*********** ⇒ 好像只有買學生機票的功能    [2010-09-11 10:39:28 +0800]
    • Josh Ko ⇒ 就是為了買機票做這張的 XD。    [2010-09-11 10:47:03 +0800]
  10. Typeless7 可以編譯了，不過 Run.agda 只是拿一個 typeless term 編譯成 IO term，和先前狂證的 subject reduction (type preservation) 那堆東西全無關係，覺得挺奇怪的。    [2010-09-12 18:24:08 +0800]
  11. 好像還沒想到要怎麼處理 io_⟫_ 的 operational semantics 呴⋯    [2010-09-12 22:03:18 +0800]
    • Josh Ko ⇒ Repository 又連不上啦！    [2010-09-12 22:07:04 +0800]
    • S************ ⇒ 因為所上停電，我的電腦關了就沒人去開機了...
      請你把最後版本寄給我好囉...    [2010-09-12 23:07:45 +0800]
  12. MBP 好像壞了…（現在用 PB 上網。）    [2010-09-13 18:35:03 +0800]
    • Josh Ko ⇒ 用光碟也開不起來，蘋果標誌下的花朵只轉個不停…    [2010-09-13 19:03:18 +0800]
    • Josh Ko ⇒ 看來只能後天離職後帶去丟給台大電腦先生。    [2010-09-13 19:10:57 +0800]
    • Josh Ko ⇒ 喔等等，光碟開機進入下一階段了！    [2010-09-13 19:11:45 +0800]
    • Josh Ko ⇒ 結果觸控板只能移動指標不能按…    [2010-09-13 19:13:47 +0800]
    • Josh Ko ⇒ 看來還是只能找電腦先生了…    [2010-09-13 19:29:12 +0800]
    • Josh Ko ⇒ 比較令人不慌張的是今早出門前才手動讓 Time Machine 備份一次；比較令人慌張的是出國前發生這種事情怕時間拖太久。    [2010-09-13 19:34:36 +0800]
    • Josh Ko ⇒ 換一套回來時間比較晚的週三火車票，當天早上先到中研院辦離職，中午回台大吃飯送修電腦。如果現場三、四個小時修不好的話應該就是沒辦法即時修好了吧，反正最後拿不到修好的東西的話就請他們寄回來。    [2010-09-13 19:51:32 +0800]
    • 王** ⇒ 怎麼個壞掉法阿？？    [2010-09-13 20:09:57 +0800]
    • Josh Ko ⇒ 回來用幾分鐘突然整個凍住，然後重開機失敗，找不到開機檔案（出現閃爍的問號資料夾圖示）。目前最新癥狀是用安裝光碟開機時回應異常緩慢，好不容易等到有回應進入主畫面，磁碟工具程式裡卻只列出光碟機沒有硬碟機。（SSD 有這麼 fragile…？或者只是排線鬆脫？讓電腦先生去決定吧。）    [2010-09-13 20:15:40 +0800]
    • 王** ⇒ @@    [2010-09-13 20:16:59 +0800]
    • L********* ⇒ 拍拍，只能說… 還在保固內是不幸中的大幸！
      相對於傳統硬碟來說，SSD的壽命真的很短！當然這跟作業系統的快取方式有很大的關係，特別是同區塊頻繁有寫入動作的時候…。    [2010-09-13 20:23:16 +0800]
    • Josh Ko ⇒ 最新癥狀：「系統描述」的 "Serial-ATA" 頁裡只顯示「掃描 Serial-ATA 設備時發生錯誤。」

      @Thundermyth: 根本是才剛買吧 XD。    [2010-09-13 20:26:17 +0800]
    • L********* ⇒ 也過了快要一季了吧，剩下75%的保固 XD
      目前所有的證據都指向犯人是SSD    [2010-09-13 20:40:38 +0800]
    • Josh Ko ⇒ 改用精技線上報修，台北行改循原計畫。    [2010-09-13 20:55:51 +0800]
    • L********* ⇒ 會到府收件？
      光華或敦南優仕也是可以考慮的維修地點    [2010-09-13 21:02:04 +0800]
    • Josh Ko ⇒ 對啊，到府收件，感覺上方便一點。    [2010-09-13 21:03:45 +0800]
  13. 宣余這麼晚還在上課…    [2010-09-13 21:50:20 +0800]
    • Josh Ko ⇒ 夭壽，上到十一點…    [2010-09-13 23:03:13 +0800]
  14. 在不時會嗶嗶嗶叫起來的會計處傳真機前假裝和學弟交接。

    （傳真機是你的好朋友，主要是和北部辦公室交換具時效性的公文，以及收所屬十四家傳來的調查表和月報表等資料。　——《會計便車指南》） ↦ http://www.facebook.com/photo.php?pid=181708&fbid=126799954039217&id=100001276392360    [2010-09-13 22:00:28 +0800]
    • 廖** ⇒ 蛤~~~~~
      快快快 幫他驅虫    [2010-09-13 23:29:39 +0800]
    • 賴* ⇒ 明天要帶他去了.........    [2010-09-13 23:40:56 +0800]
  15. 其實 PB 的鍵盤比 MBP 好打耶 XD。    [2010-09-13 22:43:07 +0800]   [ 1 人說讚！]
    • 王** ⇒ 是的 我也覺得我的iBook鍵盤比MB(鋁)好打XDD    [2010-09-13 23:10:19 +0800]
    • 陳** ⇒ 可以去找hhkb（勸敗）XD    [2010-09-13 23:20:51 +0800]
  16. 今天剛好舉行幹部選舉（是我在場的第四次），本來很想聽政見發表，但幫他們拿個便當再到出納讓阿姨看一下，回去就開始投票了，有點可惜。    [2010-09-13 23:21:38 +0800]
    • Josh Ko ⇒ 還有，本來想在選舉期間用力拍照的！    [2010-09-13 23:22:44 +0800]
  17. 今天差點就接到專門委員的電話（現在都直接從總機轉她要找的人的分機，所以接到的機率變小了），也很可惜最後沒接到。不過還是有接到兩通別人的電話啦 XD。    [2010-09-13 23:30:13 +0800]
  18. 現在還是記得不少店家電話和分機號碼，但已經有稍微錯亂了，比方說把嘉萱姐的分機記成 352，發現錯了之後又忘記 352 其實是慧崋姐的。稍後出納美珍姐找嘉萱姐的時候自然不會再記錯 XD。    [2010-09-13 23:34:04 +0800]
  19. 下班時蔡專員幫我找到共乘機會，駕駛是台大心理系 85 級學長，竟然剛好就住我家外面而已！    [2010-09-13 23:39:23 +0800]
  20. 出國前或許有機會把 Mazurkas Op 50 整套練起來。    [2010-09-14 10:50:03 +0800]
    • C*********** ⇒ 還沒開學@@    [2010-09-14 10:51:42 +0800]
    • Josh Ko ⇒ 英國十月才開學呀 XD。    [2010-09-14 10:54:09 +0800]
    • Y********** ⇒ 我一直以為你已經在英國惹... Orz    [2010-09-14 19:49:01 +0800]
    • Josh Ko ⇒ 在英國的是 scm 老師啦 XD。    [2010-09-14 19:50:47 +0800]
    • Y********** ⇒ 這我知道, 不過為啥我一直以為你在英國了? :p
      難怪常常看到你說訂便當的事情
      還想說「Josh在英國也在訂便當呀~」XD    [2010-09-14 19:52:43 +0800]
  21. MBP 被收走了，望之早歸。    [2010-09-14 15:37:25 +0800]
  22. iCal Events 已經出現「飛倫敦 Fly to London (Heathrow)」，在台時間倒數兩週。    [2010-09-14 15:40:09 +0800]
    • B********* ⇒ 加油~祝你一路順風~    [2010-09-14 17:06:40 +0800]
    • Josh Ko ⇒ 程哥出現了！星期四晚上回去烤肉吧！XD    [2010-09-14 17:09:02 +0800]
  23. 用 PB 錄音好像就是會比較模糊。    [2010-09-14 17:10:53 +0800]

Labels:

posted by Josh Ko @ 1:08 pm   0 項意見