系統F,也叫做多態lambda演算或二階lambda演算,是有類型lambda演算。它由邏輯學家Jean-Yves Girard和計算機科學家John C. Reynolds獨立發現的。系統F形式化了程式語言中的參數多態的概念。
正如同lambda演算有取值於(range over)函數的變量,和來自它們的粘合子(binder);二階lambda演算取值自類型,和來自它們的粘合子。
作為一個例子,恆等函數有形如A→ A的任何類型的事實可以在系統F中被形式化為判斷
![{\displaystyle \vdash \Lambda \alpha .\lambda x^{\alpha }.x:\forall \alpha .\alpha \to \alpha }](//wikimedia.org/api/rest_v1/media/math/render/svg/bab222ec55b643ab9a78516f599eeda09ed614f4)
這裏的α是類型變量。
在Curry-Howard同構下,系統F對應於二階邏輯。
系統F,和甚至更加有表達力的lambda演算一起,可被看作Lambda立方體的一部分。
邏輯和謂詞
布爾類型被定義為:
,這裏的α是類型變量。這產生了下列對布爾值TRUE和FALSE的兩個定義:
- TRUE :=
![{\displaystyle \Lambda \alpha .\lambda x^{\alpha }\lambda y^{\alpha }.x}](//wikimedia.org/api/rest_v1/media/math/render/svg/6139985030101ce5b13232a94399e3420d3c6594)
- FALSE :=
![{\displaystyle \Lambda \alpha .\lambda x^{\alpha }\lambda y^{\alpha }.y}](//wikimedia.org/api/rest_v1/media/math/render/svg/deaafe5c136f577dcb292b44e20ff9dc39fbd655)
接着,通過這兩個λ-項,我們可以定義一些邏輯算子:
- AND :=
![{\displaystyle \lambda x^{Boolean}\lambda y^{Boolean}.((x(Boolean))y)FALSE}](//wikimedia.org/api/rest_v1/media/math/render/svg/4353dee0807fa207531290b9467971ed6d039f91)
- OR :=
![{\displaystyle \lambda x^{Boolean}\lambda y^{Boolean}.((x(Boolean))TRUE)y}](//wikimedia.org/api/rest_v1/media/math/render/svg/8788fba0968495b9895bcefca6ccc619b371210c)
- NOT :=
![{\displaystyle \lambda x^{Boolean}.((x(Boolean))FALSE)TRUE}](//wikimedia.org/api/rest_v1/media/math/render/svg/ee216a0cf66ccfb5ee829028feaff2c1a4101dad)
實際上不需要IFTHENELSE函數,因為你可以只使用原始布爾類型的項作為判定(decision)函數。但是如果需要一個的話:
- IFTHENELSE :=
![{\displaystyle \Lambda \alpha .\lambda x^{Boolean}\lambda y^{\alpha }\lambda z^{\alpha }.((x(\alpha ))y)z}](//wikimedia.org/api/rest_v1/media/math/render/svg/658a014928737a5b32e595813c75f68a39789750)
謂詞是返回布爾值的函數。最基本的謂詞是ISZERO,它返回TRUE若且唯若它的參數是邱奇數 0:
- ISZERO := λ n. n (λ x. FALSE) TRUE
系統F結構
系統F允許以同Martin-Löf類型論有關的自然的方式嵌入遞歸構造。抽象結構(S)是使用構造子建立的。有函數被定類型為:
![{\displaystyle K_{1}\rightarrow K_{2}\rightarrow \dots \rightarrow S}](//wikimedia.org/api/rest_v1/media/math/render/svg/a951049251cc10c03dd452dbf06be57e3df2a286)
當
自身出現類型
中的一個內的時候遞歸就出現了。如果你有
個這種構造子,你可以定義
為:
![{\displaystyle \forall \alpha .(K_{1}^{1}[\alpha /S]\rightarrow \dots \rightarrow \alpha )\dots \rightarrow (K_{1}^{m}[\alpha /S]\rightarrow \dots \rightarrow \alpha )\rightarrow \alpha }](//wikimedia.org/api/rest_v1/media/math/render/svg/c8282f31aa836c15fc19cd221479e4a0f775e082)
例如,自然數可以被定義為使用構造子的歸納數據類型
![{\displaystyle {\mathit {zero}}:\mathrm {N} }](//wikimedia.org/api/rest_v1/media/math/render/svg/ca4b41d2146ec946cc96c7a66a8383cf889916ac)
![{\displaystyle {\mathit {succ}}:\mathrm {N} \to \mathrm {N} }](//wikimedia.org/api/rest_v1/media/math/render/svg/cb192e2f581fce6949e9fcf43c5feb80bb7f3658)
對應於這個結構的系統F類型是
。這個類型的項由有類型版本的邱奇數構成,前幾個是:
- 0 :=
![{\displaystyle \Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.x}](//wikimedia.org/api/rest_v1/media/math/render/svg/cbd8056923b49910fe501b55be3dbdedc1c3ea00)
- 1 :=
![{\displaystyle \Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.fx}](//wikimedia.org/api/rest_v1/media/math/render/svg/eb61d6ee4f6054e18ee75603a4ebf034b2e1a044)
- 2 :=
![{\displaystyle \Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(fx)}](//wikimedia.org/api/rest_v1/media/math/render/svg/a410423fa10354e5e4564c80da8851a4873ee7e2)
- 3 :=
![{\displaystyle \Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(f(fx))}](//wikimedia.org/api/rest_v1/media/math/render/svg/dc488317bc3d2b0b8f75c2cd8fa1575c8aea464b)
如果我們反轉curried參數的次序(比如
),則
的邱奇數是接受函數f作為參數並返回f的n次冪的函數。就是說,邱奇數是一個高階函數 -- 它接受一個單一參數函數f,並返回另一個單一參數函數。
用在程式語言中
本文用的系統F版本是顯式類型的,或邱奇風格的演算。包含在λ-項內的類型信息使類型檢查直接了當。Joe Wells(1994)設立了一個"難為人的公開問題",證明系統 F的Curry-風格的變體是不可判定的,它缺乏明顯的類型提示。[1] [2]
Wells的結果暗含着系統F的類型推論是不可能的。一個限制版本的系統F叫做"Hindley-Milner",或簡稱"HM",有一個容易的類型推論算法,並用於了很多強類型的函數式程式語言,比如Haskell和ML。
參考文獻
- Girard, Lafont and Taylor, 1997. Proofs and Types. Cambridge University Press.
- 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. [3] (頁面存檔備份,存於互聯網檔案館)
外部連結