类型论 · aiwiki.page

类型论是一类形式系统，其中表达式被赋予类型，类型规定了表达式可以如何构造和使用。它为数学提供基础，为逻辑学推理提供表达语言，也为研究计算提供框架。类型论并非单一、固定的理论，而是涵盖了对函数、相等性、量化和数据采用不同规则的多种系统。其核心判断通常写作 $a:A$ ，表示项 $a$ 具有类型 $A$ 。在某些系统中，项表示数学对象；在另一些系统中，项还表示程序和证明。(archive-pml.github.io)

起源与发展

早期类型论旨在解决不受限制的定义和自指所引发的悖论。伯特兰·罗素于1908年提出的理论将表达式分成不同层级，限制哪些对象可以作为哪些函数的参数。这一方法通过区分类型，以及在其分支类型论中区分定义的阶，阻止了会引发问题的自应用。这是为数学建立一致的逻辑基础这一努力的一部分。(upload.wikimedia.org)

阿隆佐·丘奇在1940年的论文《简单类型论的一种表述》中，提出了一个围绕函数抽象与应用构建的、更为简单的有类型逻辑框架。该框架将有类型的λ演算与逻辑常量结合起来，给出了高阶逻辑的一种表述。此后，马丁-洛夫的直觉主义类型论发展出一个包含依赖类型的构造性框架，使数学命题及其证明可以与对象和计算一并表达。(classes.cs.uchicago.edu)

判断、项与规则

类型判断通常写作

\Gamma\vdash a:A,

其中， $\Gamma$ 是列出 $x:A$ 等假设的上下文。该判断表示，在这些假设下， $a$ 具有类型 $A$ 。类型论通过规定推理规则来推导有效判断，而不是将类型赋予视为一种非形式化的分类。依赖类型论还可以包含断言某个类型是良构的，或两个表达式在定义上相等的判断。(archive-pml.github.io)

函数类型 $A\to B$ 描述接受类型为 $A$ 的参数、返回类型为 $B$ 的结果的函数。若 $f:A\to B$ 且 $a:A$ ，则通过应用可得 $f(a):B$ 。抽象用于构造函数：一个依赖于 $x:A$ 的表达式 $b:B$ 可以构成 $\lambda x.b:A\to B$ 。将这一抽象应用于某个参数时，计算通过代换进行，这一规则称为β归约。(leanprover.github.io)

积类型表示有序对，和类型则表示由构造子区分的不同选项。这些构造类似于笛卡尔积和不交并，但类型论直接规定了它们的引入、消去和计算规则。归纳类型通过构造子定义对象；例如，自然数可以由零和后继构造子生成，并配有相应的递归原理和数学归纳法原理。(docs.lean-lang.org)

命题与证明

柯里—霍华德对应将命题与类型、证明与项联系起来。在其基本的构造性解释中， $P\to Q$ 的证明是一个将 $P$ 的证明转换为 $Q$ 的证明的函数。合取命题的证明包含两个分命题各自的证明，而析取命题的证明则指明其中一个选项，并提供该选项的证明。因此，自然演绎的规则在有类型项的构造中都有对应形式。(docs.lean-lang.org)

这一联系使构造形式证明与构造类型正确的表达式密切相关。它也解释了计算型类型论与直觉主义逻辑之间的关系：存在命题和析取命题都带有明确的证据。不过，类型论并不一定是直觉主义的。包括排中律在内的经典逻辑原则，可以通过附加公理或其他逻辑机制引入。(docs.lean-lang.org)

依赖类型与宇宙

在依赖类型论中，类型可以依赖于项。例如， $\mathrm{Vec}(A,n)$ 可以描述由 $A$ 的元素组成、长度为 $n$ 的序列。这样，长度就成为类型的一部分，而不再只是外部陈述的性质。依赖函数类型写作 $\prod_{x:A}B(x)$ ，其输出类型可以随输入而变化；普通函数类型则是输出类型不随输入变化的特例。(archive-pml.github.io)

依赖对类型写作 $\sum_{x:A}B(x)$ ，其中包含一个对象 $a:A$ 以及一个类型为 $B(a)$ 的对象。在“命题即类型”的解释下，依赖函数表达全称量化，而依赖对则通过提供见证及其支持证据来表达存在性。(archive-pml.github.io)

类型宇宙允许类型本身作为对象出现。许多系统将宇宙组织为层级，例如 $\mathcal U_0:\mathcal U_1:\mathcal U_2:\cdots$ ，而不是允许一个不受限制、包含自身且囊括所有类型的宇宙。不同理论采用的宇宙形成规则和包含规则各不相同。(leanprover.github.io)

相等性与同伦解释

许多依赖类型论区分定义相等与命题相等：前者由计算规则决定，后者通过恒等类型表达，该类型的项就是相等性的证明。因此，两个表达式可能计算出相同的结果，而无须单独证明；其他相等关系则必须通过构造证据来确立。(archive-pml.github.io)

同伦类型论将类型解释为空间，将相等性的证明解释为路径。相等性证明之间的相等关系于是类似于路径之间的同伦，从而产生高维结构。其单价公理断言，从类型之间的相等关系到类型之间的等价关系的典范映射，本身也是一个等价。这将基于类型的数学基础与拓扑学联系起来，并允许通过宇宙中的相等关系，将等价的结构视为相同。(homotopytypetheory.org)

计算与证明检查

在计算机科学中，类型论为设计编程语言和确立求值过程的性质提供数学工具。标准的类型安全性论证结合了保持性与进展性：保持性意味着求值保持类型，进展性意味着一个类型正确的闭表达式要么是值，要么可以执行一步求值。这些保证针对的是规定的操作行为，并不意味着每个程序都会终止或实现其预期目的。(cs.cmu.edu)

包括Lean证明助手在内的、基于类型论的证明助手，利用类型检查来核验数学证明。其核心检查器核验各个证明项是否具有它们所声称证明的命题对应的类型。这为形式验证提供了支持，但所选规约是否正确、所假设的公理是否可接受，仍是需要另行考察的问题。(lean-lang.org)