2008/04/25

卡塔.莫斐生

今天 MFN meeting 由蔡老師講 Natural Deduction in Coq。有 Agda 的經驗,聽今天的東西就滿輕鬆的。讓我印象深刻的一點是 Coq 可以把證明寫成直直的一串,不過和 Agda 對照的話就不太令人驚訝了,其實應該就是對 interaction points 做 "leftmost derivation"。另外 Coq 拿到一個 inductive definition 就會自動產出一個 elimination rule,那其實就是 catamorphism。例如(用 Agda 的語法)

data _∧_ (A B : Set) : Set where
  conj : A -> B -> A ∧ B
它的 base functor 就是 F(X) = A × B,initial F-algebra 就是 F(A ∧ B) → A ∧ B = A × B → A ∧ B,做個 currying 就是 conj 的型別,引出的 catamorphism (fold) 則是 (A → B → C) → A × B → C。比較有趣的是 ⊤ 和 ⊥,它們的 base functor 分別是 X ↦ 1 和 X ↦ 0。要詳細講恐怕必須把關於邏輯命題的 category 都定義好,所以先算了 XD。

其實我真正想說的重點是「把 initial algebra 那一套學起來很值得」啦 XD。

--
這篇好像應該用英文寫喔 XD。

Labels: ,

Anonymous Anonymous4/25/2008 12:08 pm 說:

這看起來就是打算寫動畫心得的標題嘛

 

<< 回到主頁