系统F
维基百科,自由的 encyclopedia
系统F,也叫做多态lambda演算或二阶lambda演算,是有类型lambda演算。它由逻辑学家Jean-Yves Girard(英语:Jean-Yves Girard)和计算机科学家John C. Reynolds(英语:John C. Reynolds)独立发现的。系统F形式化了编程语言中的参数多态的概念。
正如同lambda演算有取值于(range over)函数的变量,和来自它们的粘合子(binder);二阶lambda演算取值自类型,和来自它们的粘合子。
作为一个例子,恒等函数有形如A→ A的任何类型的事实可以在系统F中被形式化为判断
这里的α是类型变量(英语:type variable)。
在Curry-Howard同构下,系统F对应于二阶逻辑。
系统F,和甚至更加有表达力的lambda演算一起,可被看作Lambda立方体的一部分。