卡塔．莫斐生

今天 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。