-
系統F
鎖定
系統F簡介
正如同lambda演算有取值於(rang over)函數的變量,和來自它們的粘合子(binder);二階lambda演算取值自類型,和來自它們的粘合子。
作為一個例子,恆等函數有形如A→ A的任何類型的事實可以在系統F中被形式化為如下式判斷:
這裏的α是類型變量。
在Curry-Howard同構下,系統F對應於二階邏輯。
系統F,和甚至更加有表達力的lambda演算一起,可被看作Lambda立方體的一部分。
[1]
系統F邏輯和謂詞
布爾類型被定義為:
,這裏的α是類型變量。這產生了下列對布爾值TRUE和FALSE的兩個定義,如下式:
接着,通過這兩個λ-項,我們可以定義一些邏輯算子:
實際上不需要IFTHENELSE函數,因為你可以只使用原始布爾類型的項作為判定(decision)函數。但是如果需要一個的話:
謂詞是返回布爾值的函數。最基本的謂詞是ISZERO,它返回TRUE當且僅當它的參數是邱奇數0:
系統F系統F結構
系統F允許以同Martin-Löf類型論有關的自然的方式嵌入遞歸構造。抽象結構(S)是使用構造子建立的。有函數被定類型為:
當S自身出現類型
中的一個內的時候遞歸就出現了。如果你有m個這種構造子,你可以定義S為:
例如,自然數可以被定義為使用構造子的歸納數據類型N
對應於這個結構的系統F類型是
。這個類型的項由有類型版本的邱奇數構成,前幾個是:
系統F用在編程語言中
本文用的系統F版本是顯式類型的,或邱奇風格的演算。包含在λ-項內的類型信息使類型檢查直接了當。JoeWells(1994)設立了一個"難為人的公開問題",證明系統 F的Curry-風格的變體是不可判定的,它缺乏明顯的類型提示。
Wells的結果暗含着系統F的類型推論是不可能的。一個限制版本的系統F叫做"Hindley-Milner",或簡稱"HM",有一個容易的類型推論算法,並用於了很多強類型的函數式編程語言,比如Haskell和ML。
[2]
- 參考資料
-
- 1. J. B. Wells. "Typability and type checking in the second-order lambda-calculus are equivalent and undecidable." In Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 176-185, 1994.
- 2. Girard, Lafont and Taylor, 1997. Proofs and Types. Cambridge University Press.
- 詞條統計
-
- 瀏覽次數:次
- 編輯次數:2次歷史版本
- 最近更新: Q宇涵6