設計模式奏鳴曲(八):要不要相信類型
來自專欄業餘程序員的個人修養23 人贊了文章
1. 一致性
直覺主義邏輯不承認經典邏輯中的排中律——對於任意命題P,或者P真,或者?P為真。
但是和經典邏輯一樣,接受無矛盾律——任何命題P,P和?P不能同時為真。無矛盾的邏輯系統,稱為一致的,或者協調的。
一個有用的邏輯系統不能包含矛盾。
2. 完備性
上文關於一致性的討論中,我們並沒有區分邏輯公式的證明和語義,
所謂證明,就是一串符號推導序列,從一些合法的公式經過一步或多步,推導出另一些合法的公式。而公式的語義則是人為選擇的,人們傾向於為公式選擇可靠的語義,
即,所有可證的公式,在語義上都為真。但是可靠性並不意味著完備性,
即,所有語義上為真的命題,並不一定總是可證的。3. 第一第二不完備性定理
人們在研究邏輯系統的時候,對一致性和完備性有著很強烈的追求,
誰都希望自己發明的邏輯系統中沒有矛盾,而且所有為真的命題都可證。但是1931年,哥德爾發現了兩個定理,粉碎了這個幻想,
任何相容的形式系統,只要蘊涵皮亞諾算術公理,就可以在其中構造在體系中不能被證明的真命題,因此通過推演不能得到所有真命題(即體系是不完備的)。
—— 哥德爾第一不完備性定理
哥德爾定理,給出了符號推導方法的局限性,
如果要求系統無矛盾,那麼某些事實可能是不可證的。此外,哥德爾第二不完備性定理指出,
任何邏輯自洽的形式系統,只要蘊涵皮亞諾算術公理,它就不能用於證明它本身的相容性。
好吧,連自身的一致性,也不能在系統之內證明了。
所以,在軟體開發過程中,檢查一個軟體系統是否符合設計要求,所使用的方法就是對它進行測試,在這個軟體系統之外進行證明。
4. 排除錯誤
在使用編程語言的時候,我們都或多或少的接觸過類型這個概念。
類型系統的一個重要作用就是,通過類型檢查排除可能會發生的錯誤。和邏輯系統一樣,如果類型系統保證所有良類型的程序都按預期正常表現,
我們就說它是可靠的,
這是一個很好的性質,如果A成立,則B成立,建立了符號和行為之間的聯繫。不幸的是,程序即使經過了類型檢查,
也保證不了那些不在預期範圍之內的特性,即,如果A成立,則C是否成立,我們是不確定的。例如,對除法表達式進行簡單的類型檢查,能保證除法操作數的類型合法,
但無法避免除0
錯誤,這可能需要更強大的類型系統才行。
另一方面,上面提到良類型的程序,預期會表現正常。
但是,類型不合法的程序,卻未必會出錯。如果A不成立,那麼B是否成立也是不確定的。這兩件事和停機問題是一脈相承的,
對於圖靈完備的編程語言來說,要想判定一段程序的所有運行時特徵,唯一的辦法運行它,僅依賴靜態檢查是行不通的。不存在通用的過程,來判斷一段程序是否停機。
5. Believe the type
那麼我們還要相信類型嗎?
要相信。我們要相信類型系統,可以幫我們排除那些已被證明的錯誤。
相信類型系統,能指導我們設計出一致的軟體。
Show me your type, and Ill show you your language.
然而,類型信息卻不等同於文檔,它只能提供一些輔助信息,
它不是用來傳遞知識的,真是如有雷同,實屬巧合,這恰恰反映了在知識傳遞方面,所做的工作還不夠。結語
本文從邏輯系統出發,介紹了人們經常提及的一些特性,
包括一致性,完備性,可靠性,進而還介紹了哥德爾不完備性定理。類型檢查可看做是一種邏輯推導,
它可以排除某些已知的錯誤,但也不是萬能的。要想寫出高質量的代碼,除了在設計方面多花一些心思之外,
更好的辦法就是對它進行測試,不論是靜態檢查還是運行時檢查,不論是自動化的單元測試,還是人工測試。
完全依賴設計和檢查是行不通的,有時候唯一可以發現錯誤的方法就是運行它。
參考
計算機科學中的現代邏輯學
離散數學教程數理邏輯Type SystemsType-driven Development with Idris直覺主義邏輯
排中律無矛盾律可靠性
完備性哥德爾不完備性定理停機問題推薦閱讀:
※數據證明:德國已經是一個移民國家
※著名「心靈雞湯理論」被證明不可重複:面帶微笑不見得讓你更開心
※25張不必言語就能證明讓毛小孩陪在小孩身邊是最正確決定的照片
※房屋權屬證明書範本
※車禍現場?汪峰在鳥巢用3小時證明這是純屬無稽之談