語言背後的代數學（六）：Henkin模型

05-02

回顧

為了解釋簡單類型化演算 $lambda^ o$ 中項，我們介紹了 $Sigma$ 代數，

用 $Sigma$ 代數中的載體 $A^sigma$ 來解釋基本類型 $sigma$ ，

用載體上的函數集 $A^{sigma o au}={f|f:A^sigma o A^ au}$ 來解釋類型為 $sigma o au$ 的所有函數。

但只是做這些對應關係，還是不夠的，

我們還得證明，這樣的解釋是「足夠多的」，

以保證每一個合法 $lambda^ o$ 項的解釋，都在這個 $Sigma$ 代數中。

尤其是使用集合上的函數，來解釋具有不動點的 $lambda$ 項時，

$A^{sigma o au}$ 的條件應當適當放寬一些，它不一定恰好是函數集 ${f|f:A^sigma o A^ au}$ 。

為此我們需要更抽象的，從語義角度定義函數是如何作用到它的參數上的。

1. 作用結構

從形式系統的角度來看， $lambda$ 項的「應用」，是推導規則的一部分，

包括類型推導規則， $frac{Gammavdash t_1:T_1 o T_2~~~~Gammavdash t_2:T_1}{Gammavdash t_1~t_2:T_2}$ ，

還包括求值規則， $(lambda x:T.t)~v o [xmapsto v]t$ 。

項的「應用」，我們可以定義為 $Sigma$ 代數上的一個作用結構（applicative structure）。

假設 $lambda x:sigma.t$ 是一個類型為 $sigma o au$ 的 $lambda$ 項，我們可以把它「應用於」類型為 $sigma$ 的項 $v:sigma$ ，

我們有， $(lambda x:sigma.t)~v=([xmapsto v]t): au$ 。

因此， $Sigma$ 代數上的一個作用結構 $App^{sigma, au}$ ，指的是這樣的一個映射，

$App^{sigma, au}:A^{sigma o au} o A^sigma o A^ au$ ，

它將集合 $A^{sigma o au}$ 中的一個函數，以及集合 $A^sigma$ 中的一個元素，映射成集合 $A^ au$ 中的一個元素。

一個有效的作用結構，必須具有外延性條件（extensional），即， $forall f,gin A^sigma o au$ ，

如果對於任意的 $din A^sigma$ ，都有 $App~f~d=App~g~d$ ，則必有 $f=g$ 。

它指出集合 $A^sigma o au$ 的兩個函數，如果在 $App^{sigma, au}$ 下的作用效果相同，

那麼它們必須是同一個函數。

2. 項的唯一解釋

有了滿足外延性條件的作用結構之後，

我們就可以歸納的定義出含義函數（meaning function） $mathscr{A}[![cdot]!]$ 了，

（1） $mathscr{A}[![varnothingvdash c:sigma]!]eta=Const(c)$

（2） $mathscr{A}[![x:sigmavdash x:sigma]!]eta=eta(x)$

（3） $mathscr{A}[![Gamma,x:sigmavdash M: au]!]eta=mathscr{A}[![Gammavdash M: au]!]eta$

（4） $mathscr{A}[![Gammavdash MN: au]!]eta=App^{sigma, au}~mathscr{A}[![Gammavdash M:sigma o au]!]eta~mathscr{A}[![Gammavdash N:sigma]!]eta$

（5） $mathscr{A}[![Gammavdashlambda x:sigma.M:sigma o au]!]eta=$ ，存在唯一的 $fin A^{sigma o au}$ ，使得，

$forall din A^sigma$ ， $App~f~d=mathscr{A}[![Gamma,x:sigmavdash M: au]!]eta[xmapsto d]$

其中， $eta$ 是滿足指派 $Gamma$ 的環境，

$Const$ 是一個映射，將項常量映射到所有 $A^sigma$ 並集的元素上，

使得，如果 $c:sigma$ ，則 $Const(c)in A^sigma$ 。

由於以上幾個等式覆蓋了所有的 $lambda$ 項，因此這樣定義的含義函數是完全的。

並且由於它為每一個 $lambda$ 項都指定了確定的語義，因此它給出的解釋方式也是唯一的。

它稱為Henkin模型。

Henkin模型是可靠的，設 $mathscr{A}$ 是 $lambda^ o$ 的任意Henkin模型，

$Gammavdash M:sigma$ 是可證的， $eta$ 是一個滿足指派 $Gamma$ 的環境，

則 $mathscr{A}[![Gammavdash M:sigma]!]etain A^sigma$ 。

即，如果一個類型斷言是可證的，則它在語義上也成立。

（關於完全性的討論，略）

3. 例子

我們可以對具有單一類型 $nat$ 的 $lambda$ 演算，定義它的Henkin模型，

令 $A^{nat}$ 為自然數集， $A^{sigma o au}$ 為所有從 $A^sigma$ 到 $A^ au$ 的函數集合，

這稱為自然數上的完全集合論函數體系，

（full set-theoretic function hierarchy over the natural number）。

我們通過 $App~f~x=f(x)$ ，把函數 $fin A^{sigma o au}$ ，作用到參數 $xin A^sigma$ 上。

下面我們得出 $lambda x:nat o nat.lambda y:nat.xy$ 的語義。

由於該項是封閉項，選擇什麼樣的環境 $eta$ 都是無關緊要的。

根據上文「含義函數」 $mathscr{A}[![cdot]!]$ 的歸納定義，我們有，

$mathscr{A}[![varnothingvdashlambda x:nat o nat.lambda y:nat.xy]!]eta=$ ，唯一的 $fin A^{(nat o nat) o nat o nat}$ ，使得，

$forall hin A^{nat o nat}$ ， $App~f~h=mathscr{A}[![x:nat o natvdashlambda y:nat.xy]!]eta[xmapsto h]$ 。

然後我們再來看下，

$mathscr{A}[![x:nat o natvdashlambda y:nat.xy]!]eta[xmapsto h]=$ ，唯一的 $gin A^{nat o nat}$ ，使得，

$forall nin A^{nat}$ ， $App~g~n=[![x:nat o nat,y:natvdash xy]!]eta[xmapsto h][ymapsto n]$ ，

即，唯一的 $gin A^{nat o nat}$ ，使得， $forall nin A^{nat}$ ， $App~g~n=App~h~n$ 。

那麼這個唯一的 $gin A^{nat o nat}$ ，實際上就是 $h$ 了。

其中， $App~g~n=App~h~n$ 是因為， $App~g~n=[![x:nat o nat,y:natvdash xy]!]eta[xmapsto h][ymapsto n]$ $=[![h:nat o nat,n:natvdash hn]!]eta$ $=App~h~n$

綜合以上兩個步驟，

$mathscr{A}[![varnothingvdashlambda x:nat o nat.lambda y:nat.xy]!]eta=$ ，唯一的 $fin A^{(nat o nat) o nat o nat}$ ，使得，

$forall hin A^{nat o nat}$ ， $App~f~h=h$ 。

因此， $fin A^{(nat o nat) o nat o nat}$ 的語義是一個恆等函數。

我們從語義上證明了以下等式，

$varnothingvdashlambda x:nat o nat.lambda y:nat.xy=lambda x:nat o nat.x$ 。

4. 環境模型條件和組合模型條件

以上定義的作用結構 $App^{sigma, au}$ 稱為滿足環境模型條件（enviroment model condition），

依賴了環境 $eta$ 這一附加概念。

它使得每一個合法的 $lambda$ 項，都有模型中一個唯一確定的數學對象與之對應。

由於 $lambda$ 項有 $lambda$ 「抽象」和 $lambda$ 「應用」雙重複雜性，所以，建立一個合理的解釋也比較麻煩。

在《你好，類型》系列文章中，

我們介紹過組合子邏輯，我們知道可以將任意的 $lambda$ 項轉換成對應的 $CL$ 項，反之亦然。

因此，如果存在模型可以解釋所有的 $CL$ 項，那麼使用它也就可以解釋所有 $lambda$ 項了。

$CL$ 項比 $lambda$ 項更為簡潔，它不包含 $lambda$ 「抽象」，只包含 $K$ 和 $S$ 這兩個組合子。

類似於 $lambda$ 項的「應用」，對於 $K$ 和 $S$ 的「組合」，我們同樣可以定義 $Sigma$ 代數上的一個作用結構。

給定 $Sigma$ 代數，對任意類型 $ho,sigma, au$ ，如果存在元素

$K_{sigma, au}in A^{sigma o( au osigma)}$ ， $S_{ ho,sigma, au}in A^{( ho osigma o au) o( ho osigma) o ho au}$ ，

滿足下列對合適類型 $x,y,z$ 的等式條件， $K_{sigma, au}xy=x$ ， $S_{ ho,sigma, au}xyz=(xz)(yz)$ ，

我們就稱，該作用結構滿足組合模型條件（combinatory model condition）。

由於所有 $CL$ 項都可以表示成 $K$ 和 $S$ 的「組合」，

因此，滿足組合模型條件的作用結構，可以唯一解釋所有 $CL$ 項。

可以證明，一個滿足外延性條件的作用結構，

如果它滿足環境模型條件，當且僅當它也同樣滿足組合模型條件。

總結

本文介紹了Henkin模型作用結構所滿足的條件，環境模型條件和組合模型條件，

它們是等價的，有了它們我們才能給出 $lambda$ 項的可靠解釋，

即，任何合法的 $lambda$ 項都有唯一解釋，且在語法上可證的 $lambda$ 項，在語義上也成立。

下文我們開始學習範疇論，為理解笛卡爾閉範疇打好基礎。

參考

你好，類型（三）：Combinatory logic

程序設計語言理論基礎

下一篇：語言背後的代數學（七）：數學結構