[科普中國]-系統(tǒng)F

系統(tǒng)F，也叫做多態(tài)lambda演算或二階lambda演算，是有類型lambda演算。它由邏輯學(xué)家Jean-Yves Girard和計(jì)算機(jī)科學(xué)家John C. Reynolds獨(dú)立發(fā)現(xiàn)的。系統(tǒng)F形式化了編程語言中的參數(shù)多態(tài)的概念。

簡介正如同lambda演算有取值于（rang over）函數(shù)的變量，和來自它們的粘合子（binder）；二階lambda演算取值自類型，和來自它們的粘合子。

作為一個(gè)例子，恒等函數(shù)有形如A→ A的任何類型的事實(shí)可以在系統(tǒng)F中被形式化為如下式判斷：

這里的α是類型變量。

在Curry-Howard同構(gòu)下，系統(tǒng)F對應(yīng)于二階邏輯。

系統(tǒng)F，和甚至更加有表達(dá)力的lambda演算一起，可被看作Lambda立方體的一部分。1

邏輯和謂詞布爾類型被定義為： ，這里的α是類型變量。這產(chǎn)生了下列對布爾值TRUE和FALSE的兩個(gè)定義，如下式：

接著，通過這兩個(gè)λ-項(xiàng)，我們可以定義一些邏輯算子：

實(shí)際上不需要IFTHENELSE函數(shù)，因?yàn)槟憧梢灾皇褂迷疾紶栴愋偷捻?xiàng)作為判定（decision）函數(shù)。但是如果需要一個(gè)的話：

謂詞是返回布爾值的函數(shù)。最基本的謂詞是ISZERO，它返回TRUE當(dāng)且僅當(dāng)它的參數(shù)是邱奇數(shù)0：

系統(tǒng)F結(jié)構(gòu)系統(tǒng)F允許以同Martin-L?f類型論有關(guān)的自然的方式嵌入遞歸構(gòu)造。抽象結(jié)構(gòu)（S）是使用構(gòu)造子建立的。有函數(shù)被定類型為：

當(dāng)S自身出現(xiàn)類型 中的一個(gè)內(nèi)的時(shí)候遞歸就出現(xiàn)了。如果你有m個(gè)這種構(gòu)造子，你可以定義S為：

例如，自然數(shù)可以被定義為使用構(gòu)造子的歸納數(shù)據(jù)類型N

對應(yīng)于這個(gè)結(jié)構(gòu)的系統(tǒng)F類型是 。這個(gè)類型的項(xiàng)由有類型版本的邱奇數(shù)構(gòu)成，前幾個(gè)是：

如果我們反轉(zhuǎn)curried參數(shù)的次序（比如 ），則n的邱奇數(shù)是接受函數(shù)f作為參數(shù)并返回f的n次冪的函數(shù)。就是說，邱奇數(shù)是一個(gè)高階函數(shù)-- 它接受一個(gè)單一參數(shù)函數(shù)f，并返回另一個(gè)單一參數(shù)函數(shù)。2

用在編程語言中本文用的系統(tǒng)F版本是顯式類型的，或邱奇風(fēng)格的演算。包含在λ-項(xiàng)內(nèi)的類型信息使類型檢查直接了當(dāng)。JoeWells（1994）設(shè)立了一個(gè)"難為人的公開問題"，證明系統(tǒng) F的Curry-風(fēng)格的變體是不可判定的，它缺乏明顯的類型提示。

Wells的結(jié)果暗含著系統(tǒng)F的類型推論是不可能的。一個(gè)限制版本的系統(tǒng)F叫做"Hindley-Milner"，或簡稱"HM"，有一個(gè)容易的類型推論算法，并用于了很多強(qiáng)類型的函數(shù)式編程語言，比如Haskell和ML。2

本詞條內(nèi)容貢獻(xiàn)者為:

王慧維 - 副研究員 - 西南大學(xué)