現在我們要再加入term到type的函數
這樣的系統被稱為CoC(Calculus of Constructions)
來整理一下目前的狀況

變數	lambda	函數調用	函數型別	其它
term(t):
\(\mathbf{var}(x)\)	\(\lambda x:T. t\)	\(t t\)
\(\uparrow(var), (weak_1), (weak_2)\)	\(\uparrow(abst)\)	\(\uparrow(appl)\)
	\(\Lambda X: K. t\)	\(t T\)
	\(\uparrow(abst_2)\)	\(\uparrow(appl_2)\)
type(T):
\(\mathbf{Var}(X)\)	\(\lambda X: K. T\)	\( T T\)	\(T \to T\)
\(\uparrow(var_T)\)	\(\uparrow(abst_T)\)	\(\uparrow(appl_T)\)	\(\uparrow(arrow_T)\)
	\(???_1\)	\(???_2\)	\(\forall X: K. T\)
			\(\uparrow(forall_T)\)
kind(K):
			\(K \to K\)	\(\star\)
			\(\uparrow\)(不用規則)	\(\uparrow\)(不用規則)
			\(???_3\)

我們發現
這所有的結構都能被分成五類

變數
lambda
函數調用
函數型別
其它

\(???_1\)是我們要加入的新lambda(從term到type)
\(???_2\)是新lambda的調用
\(???_3\)則是\(???_1\)的型別

我在介紹system Fω時
是先介紹type的規則
再介紹term的規則
現在讓我換個方式
我不要一列一列介紹
而是一欄一欄介紹

先看看變數的部分
這邊有4條規則
\((var)\), \((weak_1)\), \((weak_2)\), \((var_T)\)
\((var_T)\)事實上只是前3條規則的弱化版
假如我們不需關心型別是否合法
那麼前3條規則就能用1條規則涵蓋完
但當然
到了這時候
我們一定要注意型別是否合法
所以如果不在意階層上的差別
必須的規則至少有2條
一是\((var)\)
二是\((weak)\)
這邊提醒一下
\((weak_1)\)和\((weak_2)\)也很像
只是差在階層上
所以或許能把它當作一條規則

接著是lambda
system Fω中有3種lambda
CoC中多了一種
我們先看看前三種lambda的規則

\[\begin{array}{lcl} (abst) & \dfrac{\Gamma, x: T \vdash t: U \qquad \Gamma \vdash T: \star}{\Gamma \vdash (\lambda x: T. t): T \to U} \\ (abst_2) & \dfrac{\Gamma, X: K \vdash t: T}{\Gamma \vdash (\Lambda X: K. t): \forall X: K. T} \\ (abst_T) & \dfrac{\Gamma, X: K_1 \vdash T_2: K_2 }{\Gamma \vdash (\lambda X: K_1. T_2): K_1 \to K_2} \end{array}\]

這3條規則也很像對不對
同樣都要把約束變數塞到語境的最後端
然後檢查內層是否合法
我也姑且把這3條當作一條規則

然後是函數調用

\[\begin{array}{lcl} (appl) & \dfrac{\Gamma \vdash t_1: T \to U \qquad \Gamma \vdash t_2: T}{\Gamma \vdash t_1 t_2: U} \\ (appl_2) & \dfrac{\Gamma \vdash t: \forall X: K. T \qquad U: K}{\Gamma \vdash t U: T[X := U]} \\ (appl_T) & \dfrac{\Gamma \vdash T_1: K_1 \to K_2 \qquad \Gamma \vdash T_2: K_1}{\Gamma \vdash T_1 T_2: K_2} \end{array}\]

除了\((appl_2)\)要進行取代之外
另外2條很像
我也勉勉強強把這3條當作一條規則

\[\begin{array}{lcl} (arrow_T) & \dfrac{\Gamma \vdash T_1: \star \qquad \Gamma \vdash T_2: \star}{\Gamma \vdash T_1 \to T_2: \star} \\ (forall_T) & \dfrac{\Gamma, X: K_1 \vdash T_2: \star}{\Gamma \vdash \forall X: K_1. T_2} \\ \end{array}\]

呃雖然很不像
但也當作1條規則好了

如果你耐心讀到了這邊
你一定會好奇我到底是在賣啥關子
我想說的是
為何每一欄的規則有時會不像呢？
是因為我們系統外的抽象還不夠高
還記得抽象是什麼嗎？
抽象是把不同的東西看成一樣的
這邊我要把幾個不同的東西看成一樣的

首先
目前我們有三種函數型別
\(\forall\)和\(\to\)不一樣的地方在哪裡呢？
一個有綁定變數
一個沒有
但難道我們不能要求每個函數型別都擁有綁定變數嗎
沒有綁定變數的\(T \to T\)只不過是忽視了它的綁定變數而已
這樣大一統的函數型別被叫作\(\Pi\)-型別
我會在以後把原本的\(\forall X: K. T\)寫成\((X: K) \to T\)
要是綁定變數被忽視了的話
我也會直接寫成\(K \to T\)
注意CoC有term到type的函數
這樣的函數是一個type
因此它也有它的kind \(T \to K\)
既然有了term和type之間的各種型態
你或許可以想像kind和term還有type之間也能有一些互動
例如或許可以加入kind到type的lambda
如果要這麼做的話
最後我們也一定要有kind的型別
然後或許你可以想像kind的型別的型別、kind的型別的型別的型別
依此類推
不過這些以後再說
我先單純加入一個所有kind的型別就好了
這個型別被叫作\(\Box\)
CoC中所有kind的型別都是\(\Box\)
特別注意一點
我們已經能抽象掉\((weak_1)\)和\((weak_2)\)了
它們變成了\((weak)\)：

\[(weak) \quad \dfrac{\Gamma \vdash x: T \qquad \Gamma \vdash U: s }{\Gamma, X: U \vdash x: T} \: \forall s \in \{ \star, \Box \}\]

其實
也不需要什麼term, type, kind的差別了
我們可以把三個階層全部混在一起
全部叫作term

\[\begin{array}{rcl} term(t) ::= & \mathbf{var} (x) \\ | & \lambda x: t. t \\ | & t t \\ | & (x: t) \to t \\ | & \star \\ | & \Box \end{array}\]

事實上
有了以上的抽象
原本system Fω的13條規則
到了CoC可以被簡化成7條
變數2條
lambda1條
函數調用1條
函數型別1條
其它1條
還有\((conv)\)1條
這就是抽象的力量！
以下直接把這7條規則貼出來

\[\begin{array}{lcl} (var) & \dfrac{\Gamma \vdash t_2: s}{\Gamma, t_1: t_2 \vdash t_1: t_2} & \forall s \in \{ \star, \Box \} \\ (weak) & \dfrac{\Gamma \vdash x_1: t_1 \qquad \Gamma \vdash t_2: s }{\Gamma, x_2: t_2 \vdash x_1: t_1} & \forall s \in \{ \star, \Box \} \\ (appl) & \dfrac{\Gamma \vdash t_1: (x: t_3) \to t_4 \qquad t_2: t_3}{\Gamma \vdash t_1 t_2: t_4[x := t_3]} \\ (abst) & \dfrac{\Gamma, x: t_1 \vdash t_2: t_3 \quad \Gamma \vdash (x: t_1) \to t_3: s}{\Gamma \vdash (x: t_1. t_2): (x: t_1) \to t_3} & \forall s \in \{ \star, \Box \} \\ (form) & \dfrac{\Gamma \vdash t_1: s_1 \quad \Gamma, x: t_1 \vdash t_2: s_2}{\Gamma \vdash (x: t_1) \to t_2: s_2} & \forall s_1, s_2 \in \{ \star, \Box \} \\ (sort) & \emptyset \vdash \star: \Box \\ (conv) & \dfrac{\Gamma \vdash t: T \qquad \Gamma \vdash U: \star }{\Gamma \vdash t_2: U} & \mbox{if } T \equiv U \end{array}\]

接著我一條一條規則重新解釋
\((var)\)和\((weak)\)前面解釋過了
\((appl)\)的話
對照上面的\((appl)\), \((appl_2)\), \((appl_T)\)就能讀懂
\((abst)\)的話
你可能會對\(\Gamma \vdash (x: t_1) \to t_3: s\)有點疑惑
難道不能假設\(\Gamma \vdash t_1: s\)就好了嗎？
這只是個小細節
如果你真的想知道為什麼
這邊提供了答案
\((form)\)值得一提
這告訴了我們
term到term的函數的型別是一個type
type到term的函數的型別是一個type
type到type的函數的型別是一個kind
term到type的函數的型別是一個kind
\((sort)\)告訴了我們\(\star\)的型別是\(\Box\)
由\((form)\)我們可以知道\(\star \to \star\)之類的型別也屬於\(\Box\)
\((conv)\)的話
就和以前一樣

CoC的部分就到此結束了

lambda cube

lambda cube要說的是
事實上我們只要限制\((form)\)中\(s_1\)和\(s_2\)的可能性
我們就能讓CoC 退化成較簡單的typed lambda
舉例來說要是\(s_1 = \star\)且\(s_2 = \star\)
CoC就會退化成STLC
要是\(s_1 \in \{\star, \Box \}\)且\(s_2 = \star\)
我們就得到了system F
所以有時候也會把system F寫作\({(\star, \star), (\Box, \star)}\)
system Fω則是\({(\star, \star), (\Box, \star), (\Box, \Box)}\)
當然
原本CoC的其它規則在\((form)\)被限制了之後也會退化
有興趣的話可以自己對照著比較看看
\((\star, \star)\)是一定要有的
要是把\((\Box, \star)\), \((\Box, \Box)\), \((\star, \Box)\)當成3種選項的話
組合起來會有8種系統
也就是上圖的那個方塊的8個角
其中\(\lambda_\to\)代表STLC
\(\lambda 2\)代表system F
\(\lambda \omega\)代表system Fω
至於其它的4個系統
就不在此多加研究了

lambda cube中的每個系統都是強規範化的