Λ立方 📖 Wikipedia

在数理逻辑和类型论中，λ立方是探索Coquand的构造演算中细化轴的框架，以简单类型λ演算（在立方图中写作λ→）作为原点放在立方体的顶点，而构造演算（即高阶依赖类型化λ演算，在图中写作λPω）则是其空间对顶点。立方体的每个轴都表示一种新的抽象形式：

• 值依赖类型，或多态。系统F，即二阶λ演算（图中写作λ2）就是通过只加入此性质得到的。
• 类型依赖类型，或类型构造器。带类型构造器的简单类型λ演算（图中为${\displaystyle \lambda {\underline {\omega }}}$）就是通过只加入此性质得到的。它与系统F结合就产生了系统Fω（在图中写作不带下划线的λω）。
• 类型依赖值，或依赖类型。只加入此性质就得到了λΠ（在图中写作λP），一种与LF紧密相关的类型系统。

所有的八种演算包含了最基本的抽象形式，值依赖值即简单类型λ演算中的普通函数。此立方中最丰富的演算即构造演算，它带有所有三种抽象。所有八种演算都是强规范化的。

然而子类型并未展示在此立方中，尽管像${\displaystyle F_{<:}^{\omega }}$这样以高阶有界量化闻名的，结合了子类型和多态的系统具有实际意义，它可被进一步推广为有界类型构造器。进一步扩展到${\displaystyle F_{<:}^{\omega }}$允许纯函数对象的定义；这些系统通常在λ立方的论文发表后才被开发出来。${\displaystyle F_{<:}^{\omega }}$^[1]

此立方的思想来源于Henk Barendregt (1991)。就此立方的所有角而言，纯类型系统的框架涵盖了λ立方，其它一些系统也可表示为此通用框架的实例。^[2]此框架的出现比λ立方早上几年。在Barendregt 1991年的论文中，他也在此框架中定义了λ立方的角。

Olivier Ridoux在他的Habilitation à diriger les recherches Lambda-Prolog de A à Z... ou presque中给出了此立方的一个截边角后的模版(p. 70)的两种表示，一种将此立方表示为一个八面体，其中8个顶点以面代替，另一种将它表示为一个十二面体，其中12条棱则以面代替。