Lambda立方体
![](http://upload.wikimedia.org/wikipedia/commons/1/19/Lambda_cube.png)
在数理逻辑和类型论中,λ-立方是探索 Coquand 的构造演算中细化轴的框架,以简单类型 λ-演算(在立方图中写作 λ→)作为原点放在立方体的顶点,而构造演算(即高阶依赖类型化 λ-演算,在图中写作 λPω)则是其空间对顶点。立方体的每个轴都表示一种新的抽象形式:
- 值依赖类型,或多态。系统F,即二阶λ-演算(图中写作 λ2)就是通过只加入此性质得到的。
- 类型依赖类型,或类型构造器。带类型构造器的简单类型 λ-演算(图中为)就是通过只加入此性质得到的。它与系统F结合就产生了系统Fω(在图中写作不带下划线的λω)。
- 类型依赖值,或依赖类型。只加入此性质就得到了λΠ(在图中写作λP),一种与LF紧密相关的类型系统。
所有的八种演算包含了最基本的抽象形式,值依赖值即简单类型 λ-演算中的普通函数。此立方中最丰富的演算即构造演算,它带有所有三种抽象。所有八种演算都是强规范化的。
然而子类型并未展示在此立方中,尽管像 这样以高阶有界量化闻名的,结合了子类型和多态的系统具有实际意义,它可被进一步推广为有界类型构造器。进一步扩展到允许纯函数对象的定义;这些系统通常在λ-立方的论文发表后才被开发出来。[1]
此立方的思想来源于Henk Barendregt (1991)。就此立方的所有角而言,纯类型系统的框架涵盖了λ-立方,其它一些系统也可表示为此通用框架的实例。[2] 此框架的出现比λ-立方早上几年。在 Barendregt 1991年的论文中,他也在此框架中定义了λ-立方的角。
Olivier Ridoux 在他的 Habilitation à diriger les recherches Lambda-Prolog de A à Z... ou presque 中给出了此立方的一个截边角后的模版(p. 70) 的两种表示,一种将此立方表示为一个八面体,其中 8 个顶点以面代替,另一种将它表示为一个十二面体,其中 12 条棱则以面代替。
参见
- Some of the systems included in the cube were first defined in Automath.
- 同伦类型论
注记
参考来源
扩展阅读
- Simon Peyton Jones and Erik Meijer, 1997. Henk: A Typed Intermediate Language (页面存档备份,存于互联网档案馆)
外部链接
- Barendregt's Lambda Cube (页面存档备份,存于互联网档案馆) in the context of pure type systems by Roger Bishop Jones