系统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 }](http://178.128.105.246/content-https-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}](http://178.128.105.246/content-https-wikimedia.org/api/rest_v1/media/math/render/svg/6139985030101ce5b13232a94399e3420d3c6594)
- FALSE :=
![{\displaystyle \Lambda \alpha .\lambda x^{\alpha }\lambda y^{\alpha }.y}](http://178.128.105.246/content-https-wikimedia.org/api/rest_v1/media/math/render/svg/deaafe5c136f577dcb292b44e20ff9dc39fbd655)
接着,通过这两个λ-项,我们可以定义一些逻辑算子:
- AND :=
![{\displaystyle \lambda x^{Boolean}\lambda y^{Boolean}.((x(Boolean))y)FALSE}](http://178.128.105.246/content-https-wikimedia.org/api/rest_v1/media/math/render/svg/4353dee0807fa207531290b9467971ed6d039f91)
- OR :=
![{\displaystyle \lambda x^{Boolean}\lambda y^{Boolean}.((x(Boolean))TRUE)y}](http://178.128.105.246/content-https-wikimedia.org/api/rest_v1/media/math/render/svg/8788fba0968495b9895bcefca6ccc619b371210c)
- NOT :=
![{\displaystyle \lambda x^{Boolean}.((x(Boolean))FALSE)TRUE}](http://178.128.105.246/content-https-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}](http://178.128.105.246/content-https-wikimedia.org/api/rest_v1/media/math/render/svg/658a014928737a5b32e595813c75f68a39789750)
谓词是返回布尔值的函数。最基本的谓词是ISZERO,它返回TRUE当且仅当它的参数是邱奇数 0:
- ISZERO := λ n. n (λ x. FALSE) TRUE
系统F允许以同Martin-Löf类型论有关的自然的方式嵌入递归构造。抽象结构(S)是使用构造子建立的。有函数被定类型为:
![{\displaystyle K_{1}\rightarrow K_{2}\rightarrow \dots \rightarrow S}](http://178.128.105.246/content-https-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 }](http://178.128.105.246/content-https-wikimedia.org/api/rest_v1/media/math/render/svg/c8282f31aa836c15fc19cd221479e4a0f775e082)
例如,自然数可以被定义为使用构造子的归纳数据类型
![{\displaystyle {\mathit {zero}}:\mathrm {N} }](http://178.128.105.246/content-https-wikimedia.org/api/rest_v1/media/math/render/svg/ca4b41d2146ec946cc96c7a66a8383cf889916ac)
![{\displaystyle {\mathit {succ}}:\mathrm {N} \to \mathrm {N} }](http://178.128.105.246/content-https-wikimedia.org/api/rest_v1/media/math/render/svg/cb192e2f581fce6949e9fcf43c5feb80bb7f3658)
对应于这个结构的系统F类型是
。这个类型的项由有类型版本的邱奇数构成,前几个是:
- 0 :=
![{\displaystyle \Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.x}](http://178.128.105.246/content-https-wikimedia.org/api/rest_v1/media/math/render/svg/cbd8056923b49910fe501b55be3dbdedc1c3ea00)
- 1 :=
![{\displaystyle \Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.fx}](http://178.128.105.246/content-https-wikimedia.org/api/rest_v1/media/math/render/svg/eb61d6ee4f6054e18ee75603a4ebf034b2e1a044)
- 2 :=
![{\displaystyle \Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(fx)}](http://178.128.105.246/content-https-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))}](http://178.128.105.246/content-https-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] (页面存档备份,存于互联网档案馆)