2009/02/21

OTT

今天和 Weijin 到花蓮拜訪高中同學。因為三人只有一輛機車,所以長距離移動時必須分兩趟,我在等的時候就拿預先準備好的 HOAS paper 和 OTT paper 出來看。HOAS paper 看來並不特別難,只超出我目前的 category theory 知識一點點,最關鍵的 machinery 似乎就是 Yoneda lemma,所以先搞懂 Yoneda lemma 再繼續嘍。至於 OTT paper 還真如 scm 老師所說,是看得懂的耶!而且前幾天用 W-types 模映 lists,試圖把 W-elimination 特化成完整的 dependent foldr 時遇到了問題 ─ 沒辦法證明 [] 只可能有一種實作(intensionally)。讀了 OTT paper 才發現這正是其中一個懸疑點,paper 裡面也沒辦法從 W-elimination 特化出 induction on natural numbers,正是同一個問題,而稍後 OTT 將提供解答!這下我對 OTT 更有興趣了 XD。

--
我會試著在我的系統裡面為(我認知的)慈濟大學的精神找個位置的…

Labels:

Anonymous 小Nate2/24/2009 3:05 am 說:

花蓮?慈濟?
那不就是Nate嗎 XDD

 
Blogger Josh Ko2/24/2009 11:20 am 說:

Nate 在花蓮很寂寞,有空去看他吧 XD。

 
Anonymous 小Nate2/25/2009 1:21 pm 說:

當然ok XD

 

<< 回到主頁