卡塔．莫斐生

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

Constructive?

剛開始看主教與橋的《Constructive Analysis》，在 p.19 有一個論證步驟是

其中 x_n 和 y_n 是有理數。這一句應該是從下面這個命題證得：

要證明這個命題，應該是論述「如果 a > 0，則…」，這個論述在形式上是

但這在 intuitionistic logic 裡面並非 tautology！還是說那個命題有別種證法，或是說 Bishop and Bridges 採用的是某種比較寬鬆的 constructive logic？

--
在基礎上就遇到問題 XD。