Girard悖論是什麼？

01-08

「帶有所有類型的一個類型（Type : Type）的依賴類型 lambda 演算由於Girard悖論而不是強規範化的」

我來給莎莎喵補充一些理論相關.

0：什麼是Russell"s paradox?
在公理化集合論中, 對於任意集合 $A$ 它不能包含自身冪集, 若 $mathcal{P}(A)subseteq A$ , 構造 $Delta ={a in A;|;a otin a}$ , 那麼有 $Delta in Delta Leftrightarrow Delta otin Delta$ . 矛盾.

Cantor"s theorem從一個更弱的條件下構造出悖論.
令 $f:A o {mathcal {P}}(A)$ 為 $A$ 至 ${mathcal {P}}(A)$ 的映射, 則 $f$ 不為滿射, 即對於任意集合 $A$ 均有 ${displaystyle mathrm {card} (A)<mathrm {card} ({mathcal {P}}(A))}$ .
若 $f$ 為滿射, 構造 $Delta ={a in A;|;a otin f(a)}$ , 選取 $ain A$ 使得 $f(a)=Delta$ , 那麼有 $Delta in Delta Leftrightarrow Delta otin Delta$ . 矛盾.

上面的結論簡單來理解即是"所有集合的集合不是集合".

1：什麼是Lambda cube和Pure type system(PTS)?
要理解Girard"s paradox首先需要理解PTS. 作為PTS的一個非常典型的例子是Lambda cube.
PTS是一個三元組 $langle mathcal{S}, mathcal{A}, mathcal{R} angle$ :

$mathcal{S}$ 為類(sorts)集合.
$mathcal{A}subseteq mathcal{S} imesmathcal{S}$ 為公理(axioms)集合.
$mathcal{R}subseteq mathcal{S} imesmathcal{S} imesmathcal{S}$ 為規則(rules)集合.

一般將 $(s_1,s_2,s_2)in mathcal{R}$ 記作 $(s_1,s_2)in mathcal{R}$ .

對於每個 $sin mathcal{R}$ , 其對應的標識符名稱(variables)集合為 $mathcal{V}_{s}$ 並且滿足不同sorts的名稱不相交即當 $s_1 e s_2$ 有 $mathcal{V}_{s_1}capmathcal{V}_{s_2}=emptyset$ . 記 $mathcal{V}=igcup_{sin mathcal{S}}^{} mathcal{V}_{s}$ .

定義λ-表達式為:

$Lambda^{-}=mathcal{V};|;mathcal{S};|;Lambda^{-}Lambda^{-};|;lambda mathcal{V}:Lambda^{-}.Lambda^{-};|;Pi mathcal{V}:Lambda^{-}.Lambda^{-}$

在λ-表達式上的α-等價商集為λ-term定義為:

$egin{align} [M]_{alpha}={NinLambda^{-};|;M=_{alpha}N}\ Lambda =Lambda^{-}/_{=_{alpha}}={[M]_{alpha};|;MinLambda^{-}} end{align}$

若 $Pi x:M.N$ 其中 $x otin FV(N)$ 則記作為 $M o N$ , 這裡乘積類型 $Pi$ 可以看作是蘊涵的一種抽象.

β-規約定義為:

$(lambda x:A.M)Nquad riangleright_{eta}quad M{x:=N}$

同理可以定義β-多步規約 $riangleright_{eta}^{*}$ 與β-等價 $=_{eta}$ .

上下文環境(contexts) $mathcal{C}$ 定義為序列的集合:

$mathcal{C}={x_1:A_1,dots, x_n:A_n}$

一般記假設(assumption)為 $Gamma in mathcal{C}$ , 其域(domain)定義為 $dom(Gamma)={x;|;x:AinGamma}$ .

推導規則如下:

很明顯地, PTS為帶類型λ-calculus的高階抽象. 一個非常典型的例子即是Lambda cube.

$egin{align} mathcal{S}={ast ,square}\ mathcal{A}={(ast ,square)}\ {(ast, ast)}subseteq mathcal{R}subseteq {(ast, ast),(ast, square),(square, ast),(square, square)}\ end{align}$

$ast$ 理解為所有的合法類型, 其為一個kind(類型的類型), $square$ 理解為所有的合法kind.

根據rules的不同組合衍生出的八個λ-calculus系統分別為:

規則的可以理解如下:

$(ast, ast)$ 項依賴於項.
$(ast, square)$ 類型依賴於項.
$(square, ast)$ 項依賴於類型.
$(square, square)$ 類型依賴於類型.

即是: $(ast, ast)$ 為SLTC, $(ast, square)$ 為依值類型(dependent types), $(square, ast)$ 為類型多態, $(square, square)$ 為高階類型多態.

以上的系統構成了一個包含關係的偏序集, 使用有向圖表示出來即是Lambda cube了.

可以證明的是, 以上所有的系統具有Church-Rosser property且均是強規範化的(strongly normalizing). 即其對應的邏輯系統是一致的(consistent). 如 $lambda_{ ightarrow }$ 對應的直覺邏輯(Implicational intuitionistic fragment, $mathrm{IPC}( o)$ ), $lambda P$ 對應的一階邏輯(First-order minimal logic), $lambda 2$ 對應的二階邏輯(Second-order intuitionistic logic fragment).

2：那PTS中存不存在非一致的邏輯系統呢?

Girard"s paradox揭示了在PTS中存在這樣的系統, 即 $Gamma vdash M:ot$ .

$System U^{-}$ 定義為:

$egin{align} mathcal{S}={ast ,square, riangle}\ mathcal{A}={(ast ,square), (square, riangle)}\ mathcal{R}={(ast, ast),(square, ast),(square, square),(square, riangle)}\ end{align}$

$System U$ 為 $System U^{-}$ 添加上 $( riangle,ast)$ 這條rule.

$System F^{+}_{omega }$ 為 $System F_{omega }$ 添加上 $riangle$ 和axiom $(square, riangle)$ .

顯然 $System U$ 與 $System U^{-}$ 為 $System F^{+}_{omega }$ 與 $System F_{omega }$ 的拓展.

Girard"s paradox: $System U$ 與 $System U^{-}$ 非一致.

證明Girard"s paradox的思路類似於Cantor"s theorem, 在類型系統中構造一個與冪集與滿射等價的概念.

使用一個kind $kappa$ 代表"集合", 使用 $mathcal{P}(kappa)=kappa o ast$ 代表"冪集". 顯然地有 $vdash kappa:squarequadvdash mathcal{P}(kappa):square$ .

接下來需要一個引理:

$egin{align} Gamma={k:square,;el:mathcal{P}(k) oast,;set:ast omathcal{P}(k)\ quad V:forall X^{mathcal{P}(k)}.forall alpha^{k}.(set(el(X))alphaleftrightarrow exists eta^{k}(Xetawedge alpha =^{k}el(set(eta))) )} end{align}$

其中 $forall gamma ^{k oast}. (gammaalpha o gammaeta)$ 記作 $alpha =^{k}eta$ .

則在 $System F^{+}_{omega }$ 中有 $Gamma vdash M:ot$ .

注: 為表達簡略使用的邏輯符號 $forall$ 表示乘積類型 $Pi$ , $leftrightarrow$ 表示 $ightarrow$ 與 $leftarrow$ 的並( $wedge$ ), $ot=forall alpha: ast. alpha$ , 並省略了具體的證明構造, 即 $Gamma vdash alpha$ 表示存在 $Gamma vdash M:alpha$ .

簡略的證明步驟如下:

定義 $Equ=lambda R^{k o k o ast}.forall alpha^{k}eta^{k}gamma^{k}(Ralphaalphawedge (Ralphaeta o Retaalpha)wedge (Ralphaeta o Retagamma o Ralphagamma))$

使用以下記號:

$egin{align} alpha^{$

依次證明:

$egin{align} ullet quadGamma, alpha:k,eta:kvdash setalphaeta o setalpha^{$

若有 $Gamma, eta:kvdash etain Delta leftrightarrow eta otin eta$ , 取 $eta=Delta$ 即有 $Gammavdash Delta in Delta leftrightarrow Delta otin Delta$ , 即可得 $Gamma vdash ot$ .

Girard"s paradox: $System U$ 與 $System U^{-}$ 中有 $vdash ot$ .

簡略的證明步驟如下:

構造 $k, set, el$ 使得 $mathcal{V}=forall X^{mathcal{P}(k)}.forall alpha^{k}.(set(el(X))alphaleftrightarrow exists eta^{k}(Xetawedge alpha =^{k}el(set(eta)))$ 是可居留的, 即存在 $V:mathcal{V}$ .

令:

$egin{align} k=forall kappa^{square}(forall iota^{square}((iota okappa) o mathcal{P}(iota) o kappa) o kappa)\ el=lambda X^{mathcal{P}(k)}.lambda kappa^{square}.lambda y^{forall iota^{square}(iota okappa) o mathcal{P}(iota) o kappa}.yk(lambda eta^{k}.etakappa y)X\ set=lambda eta^{k}.eta(mathcal{P}(k))psi \ psi=lambda iota^{square}.lambda f^{iota o mathcal{P}(k)}.lambda X^{mathcal{P}(iota)}.lambda alpha^{k}. exists eta^{iota}(Xetawedge alpha =^{k}el(f(eta))) end{align}$

注意 $k$ 與inductive type具有相同的形式.

於是有
$egin{align} set(el(X))alpha=_{eta}(lambda eta.eta(mathcal{P}(k))psi )(el(X))alpha\ =_{eta}(el(X)(mathcal{P}(k))psi )alpha\ =_{eta}psi k(lambda eta.eta(mathcal{P}(k))psi )Xalpha\ =psi k;set(X)alpha\ =_{eta}exists eta(Xetawedge alpha =^{k}el(set(eta)))\ end{align}$

那麼顯然 $mathcal{V}$ 是可居留的.

由上面的引理可得 $vdash ot$ .

注: 留意引理中的構造與Cantor"s theorem的相似性.

由Girard"s paradox可以立即得到推論: 具有axiom $(ast, ast)$ 與rule $(ast, ast)$ 的系統不一致, 即 $vdash ot$ . 構造很簡單, 將以上 $System U^{-}$ 中的構造里的所有 $square$ 和 $riangle$ 替換為 $ast$ 即可得 $vdash ot$ .

另外, 不一致的系統不具有強規範性, 理由是所有正規化項 $M$ 具有形式 $M=lambda vec{z}. xvec{R} quad(vec{R} in NF_{eta})$ , 那麼顯然 $ot vdash M:ot$ , 即若 $vdash M:ot$ 由Subject reduction theorem得其不具有正規化項.

3：Type theory perspective

由Girard"s paradox和器推論揭示了在類型系統中類似於集合論有"所有類型的類型不是類型", 否則該系統是不一致即非強規範化的, 由爆炸原理(Ex falso quodlibet) $ot=forall alpha: ast alpha$ 亦使得任意類型均是可居留的. 因此Girard"s paradox可以理解為類型論里的Russell"s paradox.

題目中的所有類型的一個類型(Type : Type)即PTS里的axiom $(ast, ast)$ , 依賴類型即PTS里的rule $(ast, ast)$ . 上文給出了回答如果具有這兩個屬性, 那麼這個系統( $lambda ast$ )是非強規範化的.

值得留意的是在 $System U$ 即使沒有顯式給出"所有類型的類型是類型"這一假設, 看起來是一致的, 但kind多態的引入使得這樣的類型構造成為了可能.

0：什麼是強規範化（Strong Normalization Property？）

對於一個rewrite system來說，Strong Normalization Property是說任何term用任意方法rewrite（用編程語言的話來說就是無論用那種reduction strategy，如Call By Value（CBV）/Call By Name（CBV））等，都會終止計算。如果任何term都有一種rewrite方法，可以使之停機，就叫Weak Normalization Property。如果一個rewrite system符合Strong Normalization，很明顯也符合Weak Normalization，但是反之不一定。對於（排除特例）編程語言來說，都只有一個定好的reduction strategy，於是Strong/Weak Normalization重合。

1：如果一個語言有不停機的程序，會怎麼樣？

這會給equational reasoning搞麻煩事-然而因為IO大部分語言equational reasoning基本上不存在，所以影響就沒那末大。

在CBV語言中，這代表let x := func() in 0 end跟0不一定相等，編譯器/人類不能前者優化到後者（func可能不停機）。

在CBN語言中，這代表一個datatype中會多出莫名其妙的值，於是State就不是Monad。Haskell has no state monad

在帶eval的語言中，這代表伺服器不能接受用戶的程序-否則死循環侍候。（當然，可以timeout，但是這從某種意義上是搞出一個停機的語言，正好證明了我這點）

在Dependent Type（DT）PL中這導致了我們可以寫出bad (x: Unit): Bottom := bad x，而從Bottom我們可以得出任意Type的值，包括0=1這個類型。這導致了在該Dependent Type PL中可以證明出一切事物。這會造成死循環，於是強規範化不復存在。

2：什麼是Girard Paradox？

Girard Paradox是Russell Paradox的變種，在這用Type可以模擬Set，最後搞出個Set of Type(Set)，Paradox Set，Paradox。

在Coq中我們可以通過-type-in-type flag開啟Type：Type，於是就可以搞出這個問題，代碼如下：

Inductive SET := set T (F : T -&> SET).

SET的值由一個類型，跟該類型到SET的函數組成。

這個類型，是個索引類型，這個函數可能返回的SET，則是這個SET包含的SET。

Definition T S := match S with set t _ =&> t end.

T S取得一個S:SET的類型。

Definition F S : T S -&> SET := match S with set _ f =&> f end.

F S取得一個S:SET的函數。

Definition Contain L R : Prop := exists t : T L, F L t = R.

如果SET L包含SET R，存在一個索引t，使得該函數在t之上返回R。

Definition NCSS : SET := set { s | ~~~Contain s s } (@proj1_sig _ _).

NCSS是所有不包含自己的集合。更具體的講，set是SET的constructor，{ s | ~~~Contain s s }是一個類型-這個類型是一個『帶有證明』的SET。至於是什麼的證明？s不不不包含s。這裡之所以要用三重否定，是因為Coq核心沒排中律，所以要用在~Contain s s上加入Double Negation模擬-如果我們引入排中律，就變成我們證明了-type-in-type下（排中律是錯的）成立，而不是一切都成立了。如果沒有開-type-in-type，這一行就會出錯-至於為什麼，先不表。至於proj1_sig是啥？我們從『帶證明的SET』中取出raw SET。

註：在這，~X就是X -&> False：給我一個X，我就能給你一個False。既然False不存在，我就不能給你一個False，換句話說你就不能給我一個X，換句話說X也不存在了。

Definition NCSNCSS : ~~~Contain NCSS NCSS := fun H =&> H ltac:(destruct 1 as [[]]; simpl in *; subst; intuition).

我們證明NCSS不包含自己。首先，我們引入~~Contain NCSS NCSS，然後試圖證明False（這就是~X的定義：引入X，能證明False）。然後，我們試圖證明~Contain NCSS NCSS：證出來後作為~~Contain NCSS NCSS的參數就能得出False。然後，我們引入Contain NCSS NCSS：存在t:{ s | ~~~Contain s s },並等於NCSS，試圖證明False。既然這等於NCSS，我們就得出NCSS不不不包含自己，並且以前引入過NCSS不不包含自己，於是我們得出了False，大功告成。

Definition CSNCSS : Contain NCSS NCSS := ex_intro _ (exist _ NCSS NCSNCSS) eq_refl.

因為「NCSS包含一切不包含自己的SET」跟「NCSS不包含自己」，所以NCSS包含自己。

Definition FALSE : False := NCSNCSS (fun x =&> x CSNCSS).

因為NCSS不包含自己又包含自己，邏輯系統是inconsistent的：我們可以證明任意事物。

註：這並不是真正的Girard Paradox，而是一個Coq中的近似物。歡迎看過Girard原論文的人補充。見System U - Wikipedia

3：那都是怎麼處理的？

核心問題是：只要一個東西能引用自己，就很容易造成paradox。解決方法就是防止這樣的自指出現。

當年羅素（Ruseell）發現羅素悖論後，發現給予object/proposition/n-arity predicate of different type不同的類型，就可以防止羅素悖論（自指不了了，類型不一樣）。在這，把predicate限制成一維，並且改成function（於是，要代表一參predicate就是function to proposition，多參predicate就用currying），就會有Simply Typed Lambda Calculus - 而事實上STLC就是因為Untyped Lambda Calculus不停機，引起悖論，於是魔改一下，這樣誕生的。Godel則從Set, Set of Set, Set of Set of Set出發，並用Set theory的標準方法定義function/relation，於是類型就是自然數。在這之後，羅素髮現自己的predicate可以用forall引入自己等級的predicate，於是擔心自引用的坑還會回來，加入了order - 一個order (S n)的predicate只能引用order n的forall，order 0的predicate不能引用任何predicate的forall。然後，由於因為在這樣的系統做數學研究很坑，order的破事一大推，羅素引入了reducibility axiom：對於任何高階predicate，都有等價的一階predicate。然而加入這個公理後，羅素的系統就變成了STLC/Godel的。這就是各種邏輯系統的，極為簡陋的，處理方法。如你所見，這是個天坑，可以自己看Type Theory (Stanford Encyclopedia of Philosophy)。（3）開始的這段話到這就是這東西的一個簡介。

Coq之中做法正是如此：Type的類型是Type 1，Type 1的類型是Type 2，低階的Type是高階的Type的subtype，低階的Type的term不能用高階的Type。。。詳情見Universes

4：還有沒有其他不停機的坑？

Unbounded Recursion，Negative Data Type，CoInductive Data Type，都有微妙的坑。見（Total Functional Programming）http://sblp2004.ic.uff.br/papers/turner.pdf

5：如何證明Simply Typed Lambda Calculus是停機的？

logical relationinduction on type structure，可以看Normalization of STLC

如果用SKI/BCKW的話因為沒Variable證明簡單很多，可以自己玩玩