喬波今天學了點定理證明

來自專欄大黃的狗窩3 人贊了文章

寫在前面

這篇是一篇個人總結向的文章，（其實是自己學會了比較開心，然後寫下總結一下）大概作用就類似課後的筆記，而且寫得比較軟（乾貨不多），所以寫得可能不是很好。如果有錯誤的話還希望讀者能指正。

這篇稿子投在大黃的專欄里，感謝一下我們親愛的大黃~

類型即命題？

類型即命題，程序則證明。

其實我一開始看到這句話就發慌了，類型和命題有什麼關係？一開始我百思不得其解，後來是看了這篇文章才慢慢搞懂的。

比如其中的一個例子：

data Equal a b where EqZ :: Equal Z Z EqS :: Equal a b -> Equal (S a) (S b)type a === b = Equal a b

這樣的話這個 Equal 的類型其實就只能讓 a 和 b 保持相等，所以這個類型，啊不，這些類型只能有形如這樣的形式：

EqZ :: Equal Z ZEqS EqZ :: Equal (S Z) (S Z)EqS (EqS EqZ) :: Equal (S (S Z)) (S (S Z))...

而形如

Z === (S Z)

這樣類型是無法構造出來的。所以，這樣一個類型就保證了它帶的兩個小類型是一致的。如果我們取一個在這個類型與自然數的同構的話，這個類型其實就是。這其實就是類型即命題的含義，即你通過一定的方法構造了出一個類型，這個類型就是個命題。好吧這不還是什麼都沒說么……

在Haskell中試著寫第一個證明

證明其實就是一個從已知條件出發，通過推理，得出其結論成立的這個過程。比如簡單的一個例子：

我們知道 表示蘊含關係，即當命題 成立的時候，命題 也成立。既然命題就是類型，那我們只需要構造一個從命題 得到的類型 P ，到 得到的類型 Q 的一個函數即可。構造一個類型為 f :: P -> Q 的函數，這個函數就是 的證明。

反過來說，證明的驗證過程也就是程序的類型檢查。如果通過了類型檢查，那麼這個證明就是合理的；反之則不是。呃，說了這麼多，還沒有真正寫代碼……看來我還是得引用上面說的那篇文章中的例子，比如相等關係的自反性的證明（應該說是相對最簡單的了）。假設我們已經有了類型上的自然數，先把它的類型寫出來：

refl :: Nat n -> n === n

很容易能想到它為零的情況，定義自然數零為 Zero 的話：

refl Zero = EqZrefl (Succ n) = ???

接下來我就不知道怎麼寫了。但是用上遞歸的思想的話很簡單，就是

refl (Succ n) = EqS $ refl n

這樣一來，就完成了對每個自然數的證明，也不會出現Non-exhaustive patterns這樣的問題。當然，這只是個很簡單的例子。因為我其它的也什麼都不會（菜哭）。更加複雜的證明應該還需要用到別的技巧。

嗯……大概就這些，第一次寫文章，也不知道怎麼寫（撓頭）。

推薦閱讀：