查看“︁Lambda立方体”︁的源代码

[[File:Lambda_cube.png|有框|λ-立方。箭头的方向展示了包含关系。]]
在[[数理逻辑]]和[[类型论]]中，'''λ-立方'''是探索''' '''[[Coquand |Coquand]] 的[[构造演算]]中细化轴的框架，以[[简单类型λ演算|简单类型 λ-演算]]（在立方图中写作 λ→）作为原点放在立方体的顶点，而构造演算（即高阶依赖类型化 λ-演算，在图中写作 λPω）则是其空间对顶点。立方体的每个轴都表示一种新的抽象形式：
* 值依赖类型，或[[多态 (计算机科学)|多态]]。[[系统F]]，即二阶λ-演算（图中写作 λ2）就是通过只加入此性质得到的。
* 类型依赖类型，或[[型別構造器|类型构造器]]。带类型构造器的[[简单类型λ演算|简单类型 λ-演算]]（图中为<math>\lambda\underline{\omega}</math>）就是通过只加入此性质得到的。它与[[系统F]]结合就产生了系统Fω（在图中写作不带下划线的λω）。
* 类型依赖值，或[[依赖类型]]。只加入此性质就得到了[[依赖类型|λΠ]]（在图中写作λP），一种与[[逻辑框架|LF]]紧密相关的类型系统。
所有的八种演算包含了最基本的抽象形式，值依赖值即[[简单类型λ演算|简单类型 λ-演算]]中的普通函数。此立方中最丰富的演算即[[构造演算]]，它带有所有三种抽象。所有八种演算都是[[强规范化]]的。

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

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

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

== 参见 ==
* Some of the systems included in the cube were first defined in Automath.
* 同伦类型论

== 注记 ==
{{reflist}}

== 参考来源 ==

== 扩展阅读 ==
* Simon Peyton Jones and Erik Meijer, 1997. ''[https://www.microsoft.com/en-us/research/wp-content/uploads/1997/01/henk.pdf Henk: A Typed Intermediate Language] {{Wayback|url=https://www.microsoft.com/en-us/research/wp-content/uploads/1997/01/henk.pdf |date=20201112033900 }}''

== 外部链接 ==
* [http://www.rbjones.com/rbjpub/logic/cl/tlc001.htm Barendregt's Lambda Cube] {{Wayback|url=http://www.rbjones.com/rbjpub/logic/cl/tlc001.htm |date=20201109094050 }} in the context of pure type systems by Roger Bishop Jones
[[Category:Lambda演算]]
[[Category:类型论]]