[科普中国]-Lambda立方体

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

构造演算构造演算(CoC)是高阶有类型 lambda 演算，这里的类型是一级值。因此在 CoC 内有可能定义从整数到类型、从类型到类型的函数，同从整数到整数的函数一样。CoC 是强规范化的。CoC 最初由 Thierry Coquand 开发。CoC 是 Coq 定理证明器早期版本的基础；它后来的版本建造在归纳构造演算之上，这是带有对归纳数据类型的天然支持的 CoC 扩展。在最初的 CoC 中，归纳数据类型必须模拟为它们的多态解构函数。构造演算可以被当作 Curry-Howard同构的扩展。Curry-Howard 同构把在简单类型 lambda 演算中项关联上在直觉命题逻辑中自然演绎证明。构造演算扩展了这个同构为在完全的直觉谓词逻辑中的证明，这包括了量化陈述（它也叫做"命题"）的证明。

Lambda立方体抽象形式Lambda立方体的每个轴都表示一种抽象形式：

值依赖类型，或多态。系统F，即二阶λ-演算（图中写作 λ2）就是通过只加入此性质得到的。

类型依赖类型，或类型构造器。带类型构造器的简单类型 λ-演算（图中为λω）就是通过只加入此性质得到的。它与系统F结合就产生了系统Fω（在图中写作不带下划线的λω）。

类型依赖值，或依赖类型。只加入此性质就得到了λΠ（在图中写作λP），一种与LF紧密相关的类型系统。

所有的八种演算包含了最基本的抽象形式，值依赖值即简单类型 λ-演算中的普通函数。此立方中最丰富的演算即构造演算，它带有所有三种抽象。所有八种演算都是强规范化的。然而子类型并未展示在此立方中，尽管像 这样以高阶有界量化闻名的，结合了子类型和多态的系统具有实际意义，它可被进一步推广为有界类型构造器。进一步扩展到 允许纯函数对象的定义；这些系统通常在λ-立方的论文发表后才被卡发出来： 。此立方的思想来源于Henk Barendregt (1991)。就此立方的所有角而言，纯类型系统的框架涵盖了λ-立方，其它一些系统也可表示为此通用框架的实例。此框架的出现比λ-立方早上几年。在 Barendregt 1991年的论文中，他也在此框架中定义了λ-立方的角。

λ-演算λ-演算(组合逻辑)及函数式语言及程序设计。大多数构造类型论都是用函数式语言实现的，而λ-演算是函数式语言的理论基础，是函数式程序设计语言的纯理论部分的范式，是由函数抽象和函数应用组成的系统，而这两个特点也是程序设计语言所具有的共同之处：抽象与过程定义机制对应，应用与过程调用对应1。

有类型 lambda 演算是使用 lambda 符号（ ）指示匿名函数抽象的一种有类型的形式化。有类型 lambda 演算是基础编程语言并且是有类型的函数式编程语言如 ML 和 Haskell 和更间接的指令式编程语言的基础。它们通过 Curry-Howard同构密切关联于直觉逻辑并可以被认为是范畴的类的内部语言，比如简单类型 lambda 演算是笛卡尔闭范畴（CCC）的语言。有类型 lambda 演算被看作无类型lambda演算的精细化。更现代的观点把有类型 lambda 演算看做更基础的理论，而把无类型 lambda 演算看作它的只有一个类型的特殊情况。

简单类型 lambda 演算( )是连接词只有 (函数类型)的有类型 lambda 演算。这使它成为规范的、在很多方面是最简单的有类型 lambda 演算的例子。简单类型也被用来称呼对简单类型 lambda 演算的扩展比如积、陪积或自然数(系统 T)甚至完全的递归(如PCF)。相反的，介入了多态类型(如系统F)或依赖类型(如逻辑框架)的系统不被当作是简单类型。简单类型 lambda 演算最初由阿隆佐·邱奇在 1940 年介入来尝试避免无类型 lambda 演算的悖论性使用。

简单类型 lambda 演算的类型构造自基本类型(或类型变量) ，给定类型 我们能构造 。邱奇只使用了两个基本类型， 是命题的类型， 是个体的类型。这种演算经常只有一个基本类型，通常考虑为 。

是右结合的：我们读 为 。对每个类型 我们指派一个数字，它是 的阶。对于基本类型，我们设置 ，而对于函数类型我们递归的定义。

依赖类型在计算机科学和逻辑中，依赖类型（或依存类型，dependent type）是指依赖于值的类型，其理论同时包含了数学基础中的类型论和计算机编程中用以减少程序错误的类型系统两方面。在 Per Martin-Löf 的直觉类型论中，依赖类型可对应于谓词逻辑中的全称量词和存在量词；在依赖类型函数式编程语言如 ATS、Agda、Dependent ML、Epigram、F* 和 Idris 中，依赖类型系统通过极其丰富的类型表达能力使得程序规范得以借助类型的形式被检查，从而有效减少程序错误。

依赖类型的两个常见实例是依赖函数类型（又称依赖乘积类型、Π-类型）和依赖值对类型（又称依赖总和类型、Σ-类型）。一个依赖类型函数的返回值类型可以依赖于某个参数的具体值，而非仅仅参数的类型，例如，一个输入参数为整型值n的函数可能返回一个长度为n的数组；一个依赖类型值对中的第二个值可以依赖于第一个值，例如，依赖类型可表示这样的类型：它由一对整数组成，其中的第二个数总是大于第一个数。

依赖类型增加了类型系统的复杂度。由于确定两个依赖于值的类型的等价性需要涉及具体的计算，若允许在依赖类型中使用任意值的话，其类型检查将会成为不可判定问题；换言之，无法确保程序的类型检查一定会停机。由于Curry-Howard同构揭示了程序语言的类型论与证明论的直觉逻辑之间的紧密关联性，以依赖类型系统为基础的编程语言大多同时也作为构造证明与可验证程序的辅助工具而存在，如 Coq 和 Agda（但并非所有证明辅助工具都以类型论为基础）；近年来，一些以通用和系统编程为目的的编程语言被设计出来，如 Idris。

本词条内容贡献者为:

王慧维 - 副研究员 - 西南大学