數學邏輯和電腦程式碼之間的深層聯繫：互為鏡像

一些科學發現被賦予了重要的意義，因為揭示了一些新的東西，例如 DNA 的雙螺旋結構或黑洞的存在。但是，揭示的這些東西還具有更深遠的意義，因為它們表明：兩個之前看起來大不一樣的老舊概念事實上卻是一樣的。例如詹姆斯・克拉克・麥克斯韋發現的方程組表明，電與磁是同一個現象的兩個不同方面，而廣義相對論則把引力和彎曲的時空聯繫到了一起。

柯里- 霍華德對應（Curry-Howard correspondence）也是一樣，並且它關聯的不僅僅是一個領域中的兩個不同概念，而是兩個完整的學科：計算機科學和數學邏輯。這種對應關係也被稱為柯里- 霍華德同構（Curry-Howard isomorphism，同構是指兩個事物之間存在某種一一對應關係），其為數學證明和計算機程式建立了某種關聯。

簡單來說，柯里- 霍華德對應認為：電腦科學中的兩個概念（類型和程式）分別等價於邏輯學中的兩個概念（命題和證明）。

這種對應關係導致的一個結果是程式開發被提升到了理想化的數學層面，而之前人們通常認為程式開發就是個手藝活。程式開發不只是「寫程式」，還變成了證明定理的行為。這能對程式開發的行為進行形式化，並能提供用數學方法推理程式正確性的方法。

而這個對應關係的名稱則來自於兩位研究者，他們各自獨立地發現了這個對應關係。 1934 年，數學家和邏輯學家哈斯凱爾・柯里（Haskell Curry）注意到了數學中的函數和邏輯學中的蘊涵（implication）關係之間的相似性。蘊涵關係的形式是兩個命題之間呈現「if-then（如果 - 那麼）」陳述的形式。

受柯里觀察到的結果的啟發，數理邏輯學家威廉・阿爾文・霍華德（William Alvin Howard）在1969 年發現計算和邏輯之間存在更深度的關聯；他的研究顯示：運行電腦程式非常像是簡化邏輯證明。在運行電腦程式時，每一行程式碼都會被「評估」以產生一個輸出。類似地，在進行證明時，一開始是複雜的陳述，然後對其進行簡化（例如通過消除冗餘步驟或用更簡單的表達式替換複雜表達式），直到得到某個結論—— 從許多過渡陳述推導出一個更簡潔的陳述。

儘管這一描述大致說明了這種對應關係的含義，但要完全理解它，就需要更多地了解計算機科學家口中的「類型論（type theory）」 。

讓我們從一個著名的悖論談起：在一個村莊中有一位理髮師，他為且只為所有不給自己刮鬍子的人刮鬍子。那麼這位理髮師給自己刮鬍子嗎？如果答案為是，那麼他就必定不為自己刮鬍子（因為他只為不給自己刮鬍子的人刮鬍子）。如果答案為否，那麼他就必定為自己刮鬍子（因為他為所有不給自己刮鬍子的人刮鬍子）。這是伯特蘭・羅素（Bertrand Russell）發現的一個悖論的非形式化版本，那時他正嘗試使用名為集合（set）的概念來建構數學的基礎。也即：定義一個包含所有不包含自身的集合的集合是不可能的，這個過程必然會出現矛盾。

羅素的研究表明，為了避免這個悖論，我們可以使用類型（type）。粗略地說，類型是指一些類別，其所含的具體值稱為物件（object）。舉個例子，如果有一個類型 Nat 表示自然數，那麼其物件就是 1、2、3 等等。研究者通常使用冒號來表示物件的類型。例如整數類型的數值 7，可以寫成「7: Integer」。我們可以使用函數將類型 A 的物件轉換成類型 B 的對象，也可以使用函數將類型 A 和 B 的兩個物件組成一個新類型「A×B」的對象。

因此，為了解決這個悖論，一種方法是對這些類型進行分層，讓它們只包含比其自身低一個層級的元素。然後一個類型不能包含自身，這就能避免造成上述悖論的自我指涉。

在類型論的世界中，證明一個陳述為真的過程可能與我們習慣的做法不一樣。如果我們想要證明整數 8 是偶數，那麼問題的關鍵在於證明 8 實際上是「偶數」類型中一個對象，而這個類型定義元素的規則是能被 2 整除。在驗證了 8 能被 2 整除後，我們就能得出結論：8 就是「偶數」類型中的一個「居民」。

柯里與霍華德證明類型在根本上等價於邏輯命題。當一個函數「居留（inhabit）」於某一類型時，也就是該函數是該類型的一個物件時，我們就能有效地證明對應的命題為真。因此，以類型A 的物件為輸入、以類型B 的為輸出的函數（表示成類型A→B）必定對應於一個蘊涵：「如果A，那麼B。」舉個例子，假設有命題「如果下雨，那麼地面是濕的。」在類型論中，這個命題會被建模成類型「下雨→地面濕」的一個函數。這兩種表示方式看起來不一樣，但在數學上卻是一樣的。

儘管這種關聯看起來可能很抽象，但它不僅改變了數學和電腦科學的實踐者思考其工作的方式，也為這兩個領域帶來了一些實用的應用。在電腦科學領域，這種關聯為軟體驗證（即確保軟體正確性的過程）提供了一個理論基礎。透過邏輯命題的方式描述所需行為，程式開發者可以透過數學方式證明一個程式的行為是否符合預期。並且在設計更強大的函數式程式語言方面，這種關聯也提供了堅實的理論基礎。

而在數學領域，這種對應關係已經催生出了證明助手（proof assistant）工具，其也被稱為互動式定理證明器（interactive theorem prover）。這些軟體工具可以輔助建構形式化證明，具體的例子包括 Coq 和 Lean。在 Coq 中，每一步證明本質上都是一個程序，而證明的有效性則會透過類型檢查演算法來檢驗。數學家也已經在使用證明助手（尤其是 Lean 定理證明器）來對數學進行形式化，其中涉及以一種可通過計算機驗證的嚴格格式來表示數學概念、定理和證明。這讓有時候非形式化的數學語言可以用電腦加以檢驗。

研究者也正在探索數學和程式設計之間的這種關聯的潛在成果。原始的柯里 - 霍華德對應將程序開發與某種名為直覺邏輯（intuitionistic logic）的邏輯融合到了一起，但事實證明還有更多邏輯類型可以被統一進來。

康乃爾大學電腦科學家Michael Clarkson 表示：「自柯里得出其見解的這一個世紀裡，我們不斷發現越來越多『邏輯系統X 對應於計算系統Y’的實例。研究者也已經將程式設計和其它類型的邏輯聯繫起來，例如包含「資源」概念的線性邏輯以及涉及可能性和必要性概念的模態邏輯。

而且儘管這個對應關係秉承柯里與霍華德之名，但他們絕不是這種對應關係的唯二發現者。這佐證了​​這個對應關係的一個根本性質：人們一再不斷地一次又一次地註意到它。 Clarkson 說：「計算和邏輯之間存在深度關聯似乎並非偶然。」

#

以上是數學邏輯和電腦程式碼之間的深層聯繫：互為鏡像的詳細內容。更多資訊請關注PHP中文網其他相關文章！