語言背後的代數學（十）：Curry-Howard-Lambek correspondance

05-03

回顧

上文我們介紹了笛卡爾閉範疇，它給出了簡單類型化 $lambda$ 演算系統 $lambda^{unit, imes, o}$ 的語義，

我們還看到了笛卡爾閉範疇與柯里化之間的關係。

結合《你好，類型》系列文章，

到目前為止我們已經有了，類型理論，邏輯學和範疇論的知識基礎了。

現在我們介紹Curry-Howard-Lambek correspondence，將三者聯繫起來。

1. 類型方面

參考《你好，類型（二）：Lambda calculus》，我們來回顧一下簡單類型化 $lambda$ 演算系統。

1.1 語法

$t::=x|tu|lambda x.t$

例子： $lambda x.x+1$ ， $lambda f.lambda x.fx$

1.2 類型

基本類型（basic types）， $B::=iota|cdots$

一般類型（general types）， $T::=B|T o T|T imes T$

例子： $iota oiota oiota$ ， $(iota oiota) oiota$

1.3 類型推導規則

（1） $frac{~}{Gamma,x:tvdash x:T}$

（2） $frac{Gammavdash t:T~~~~Gammavdash u:U}{Gammavdashleftlangle t,u ight angle:T imes U}$ ， $frac{Gammavdash v:T imes U}{Gammavdashpi_1v:T}$ ， $frac{Gammavdash v:T imes U}{Gammavdashpi_2v:U}$

（3） $frac{Gamma,x:Uvdash t:T}{Gammavdashlambda x.t:U o T}$ ， $frac{Gammavdash t:U o T~~~~Gammavdash u:U}{Gammavdash tu:T}$

其中， $pi_1leftlangle v_1,v_2 ight angle=v_1$ ， $pi_2leftlangle v_1,v_2 ight angle=v_2$ 。

2. 邏輯方面

參考《你好，類型（四）：Propositional logic》，

我們構建一個只包含邏輯聯接詞 $wedge$ 和 $o$ 的命題邏輯系統。

2.1 邏輯推導規則

（1） $frac{~}{Gamma,Avdash A}$

（2） $frac{Gammavdash A~~~~Gammavdash B}{Gammavdash Awedge B}$ ， $frac{Gammavdash Awedge B}{Gammavdash A}$ ， $frac{Gammavdash Awedge B}{Gammavdash B}$

（3） $frac{Gamma,Avdash B}{Gammavdash A o B}$ ， $frac{Gammavdash A o B~~~~Gammavdash A}{Gammavdash B}$

2.2 Curry-Howard correspondence

我們看到，只要將邏輯系統中的 $wedge$ 和 $o$ ，替換成簡單類型化 $lambda$ 演算中的 $imes$ 和 $o$ ，

那麼這兩個系統從推導規則上來看是一致的。

邏輯中的命題，對應了簡單類型化 $lambda$ 演算中的類型，

邏輯中命題的證明，對應了簡單類型化 $lambda$ 演算中的項（的類型斷言）。

命題 $A o B$ ，可以這樣理解，

如果該命題可證，則存在將 $A$ 的證明轉換為 $B$ 的證明的構建過程（construction）。

命題 $Awedge B$ ，可以這樣理解，它是 $A$ 和 $B$ 的證明序對（pair）。

考慮到以上命題邏輯與類型之間的對應關係，

我們可以說，proofs as programs。

3. 範疇論方面

結合《語言背後的代數學（九）：笛卡爾閉範疇》，

我們給出了簡單類型化 $lambda$ 演算的範疇論解釋。

3.1 對象

將簡單類型化 $lambda$ 演算系統的類型，解釋為笛卡爾閉範疇 $C$ 中的對象。

$mathscr{C}[![sigma imes au]!]=mathscr{C}[![sigma]!] imesmathscr{C}[![ au]!]$

$mathscr{C}[![sigma o au]!]=mathscr{C}[![sigma]!] omathscr{C}[![ au]!]$

3.2 箭頭

將帶有自變數項，解釋為從自變數類型到項類型的箭頭。

$mathscr{C}[![Gammavdash M:sigma]!]=mathscr{C}[![Gamma]!] omathscr{C}[![sigma]!]$

3.3 Curry-Howard-Lambek correspondance

根據簡單類型化 $lambda$ 演算系統中的推導規則，

我們可以為範疇 $C$ 添加對象和箭頭之間的約束條件，

（1） $frac{~}{pi_2:Gamma imes A o A}$

（2） $frac{f:Gamma o A~~~~g:Gamma o B}{leftlangle f,g ight angle:Gamma o A imes B}$ ， $frac{f:Gamma o A imes B}{pi_1circ f:Gamma o A}$ ， $frac{f:Gamma o A imes B}{pi_2circ f:Gamma o B}$

（3） $frac{f:Gamma imes A o B}{g_f:Gamma o B^A}$ ， $frac{f_1:Gamma o B^A~~~~f_2:Gamma o A}{ecircleftlangle f_1,f_2 ight angle:Gamma o B}$

$g_f=Gamma o B^A$ 是一個箭頭，和 $e:B^A imes A o B$ 的定義，

可以參考前一篇文章中關於笛卡爾閉範疇的定義。

笛卡爾閉範疇作為簡單類型化 $lambda$ 演算系統的語義模型，

範疇中箭頭之間約束關係，與類型推導規則是一致的，

而根據Curry-Howard correspondence，類型推導規則與命題邏輯又是一致的。

因此，類型理論，邏輯學和範疇論產生了關聯，

這種三者的對應關係，稱為Curry-Howard-Lambek correspondance。

總結

本文介紹了Curry-Howard-Lambek correspondance，

它將本來毫無關係的三個學科聯繫在了一起，

類型理論與程序和計算相關，邏輯學與證明（論）相關，範疇論與模型（論）和代數學相關。

本系列文章到此結束了，與代數學和範疇論相關的內容其實還有很多，

例如，quotient algebra，comonad，adjoint functor，free monoid，等等概念，

書山有路勤為徑，學海無涯苦作舟，讓我們一起努力吧。

參考

你好，類型（一）：開篇

你好，類型（四）：Propositional logic

語言背後的代數學（九）：笛卡爾閉範疇

Curry–Howard correspondence

Curry-Howard-Lambek correspondence

The Curry-Howard Correspondence, and beyond

Lectures on the curry-howard Isomorphism

Intuitionistic logic