Martin-Löf 依赖类型论

形式陈述

Martin-Löf 依赖类型论不是一张孤立的类型语法表，而是一族由判断及其推导规则组织的形式系统。本文固定一个常见的谓词式、内涵核心：语境由依次依赖的声明组成，基本判断至少包括

\Gamma\;\mathsf{ctx},\qquad \Gamma\vdash A\;\mathsf{type},\qquad \Gamma\vdash a:A,\qquad \Gamma\vdash A\equiv B\;\mathsf{type},\qquad \Gamma\vdash a\equiv b:A.

空语境良构；若 $\Gamma\;\mathsf{ctx}$ 且 $\Gamma\vdash A\;\mathsf{type}$ ，便可扩张为 $\Gamma,x:A\;\mathsf{ctx}$ 。每一种类型构造都要给出 formation、introduction、elimination 与 computation 四类规则。例如依赖函数类型和依赖对类型分别规定如何抽象、应用以及如何成对、拆对；恒等类型以 $\mathsf{refl}$ 引入，并由恒等类型消去子处理依赖相等证明；宇宙类型则把“小类型”作为可量化的对象分层安置。规则中的 $\equiv$ 是定义相等，属于元层判断，不是一个可以任意证明的对象类型。

结构规则必须与依赖性相容。其关键不是文本替换，而是类型保持的代入引理：若 $\Gamma\vdash a:A$ 且 $\Gamma,x:A,\Delta\vdash\mathcal J$ ，则

\Gamma,\Delta[a/x]\vdash\mathcal J[a/x].

$\mathcal J$ 可代表类型良构、项有型或相等判断；代入须避开变量捕获，并同步改写后续语境中的依赖。弱化、交换与收缩也只能在保持语境良构的条件下使用。由这些判断、类型形成子、结构规则和计算规则共同决定一个具体 MLTT；是否加入 η 规则、宇宙累积、商类型或相等反映，必须另行声明，不能从“MLTT”三个字自动推出。

直觉

可以把这套理论看成一门同时描述数据、程序与证据的微型语言。一个类型的意义由“怎样构造它的规范元素、怎样使用这些元素、构造后立即使用会怎样计算”给出，而不是先把类型解释成某个外部集合再开始推理。语境像一份有先后次序的实验记录：后面的假设可以引用前面的变量，所以删去或替换一个早期声明会沿着整条记录传播。

命题即类型的读法提供了重要解释，却不是对象层的字面等号。函数项可承载蕴含证明，依赖函数可承载全称证明，依赖对可承载存在见证；这是规则结构之间的对应，而非声称逻辑公式、运行时数据和类型表达式在所有语义中都是同一个对象。MLTT 的力量恰来自把这些角色放进同一判断框架，同时仍严格区分“计算得到相同项”和“构造了一个相等证明”。

例子与边界

设 $\mathsf{Bool}:\mathcal U_0$ ，并允许在更高一层宇宙中量化小类型。多态恒等项可逐层推出

\mathsf{id} =\lambda(A:\mathcal U_0).\lambda(x:A).x :\Pi(A:\mathcal U_0).\Pi(x:A).A.

在语境 $A:\mathcal U_0,x:A$ 中，变量规则给出 $x:A$ ；两次 Π-引入依次关闭 $x$ 与 $A$ 。把 $\mathsf{Bool}$ 代入 $A$ ，再把 $\mathsf{true}$ 代入 $x$ ，计算规则得到

\mathsf{id}\;\mathsf{Bool}\;\mathsf{true}\equiv\mathsf{true}:\mathsf{Bool}.

这里第一次应用把余类型 $\Pi(x:A).A$ 改为 $\Pi(x:\mathsf{Bool}).\mathsf{Bool}$ ，第二次应用再替换项变量。代入作用于项和类型，是依赖类型计算必须同步维护的约束。

语境也会同步改变。例如在 $n:\mathsf{Nat},v:\mathsf{Vec}(X,n)$ 中，把 $n$ 代入为 $\mathsf{succ}(\mathsf{zero})$ 后，后一个声明必须成为 $v:\mathsf{Vec}(X,1)$ 。不能删掉 $n$ 后仍保留含自由 $n$ 的旧类型。向量连接的依赖消去同样让目标随索引变化，从而把“连接后长度为 $m+n$ ”变成返回类型，而非运行后的注释。

边界首先来自理论选择。若向核心加入无约束的一般递归，闭项可能不再正规化，按计算比较类型的过程也可能失去可判定性；若加入相等反映，则有恒等证明便可改变判断相等，内核的转换问题不再只是规范化计算。1984 年讲义、现代 Agda 风格内涵理论、HoTT 与立方类型论共享谱系却不具有完全相同的规则。也不能把 Lean、Coq、Agda 的表面语言逐字称为本页核心：它们还包含归纳声明、隐式参数、层级多态、终止检查和 elaboration 等工程层。

推论与应用

一旦 formation—introduction—elimination—computation 的规则确定，就能分别研究替换、主体归约、正规化、可判定类型检查与一致性；四类规则齐全并不自动证明这些性质。替换等引理常沿 typing derivation 归纳，正规化通常还需要逻辑关系或可计算性解释等更强工具。内核则把可判定的规则组织成检查过程，并证明接受的核心项确有推导。

强正规化只针对已明确规则的良类型核心项。常见纯内涵 MLTT 的终止结果不能直接覆盖一般递归、未经证明的重写规则或所有额外公理。正规化也要与典范性分开：加入一个没有归约规则的常量 $c:\mathsf{Nat}$ ，它已经是正规形，却不是零或后继形式。因此“闭合自然数项计算到数码”的结论还要求没有这种停滞常量，并有相应规范形式定理。

MLTT 因而同时服务于构造性数学和程序验证：证明的计算内容可以提取，接口不变量可以进入类型，机器只需检查相对很小的核心推导。不过这些收益都相对于明确的规则集合成立。添加新公理时应问它是否有判断式计算规则；添加新类型形成子时应重新证明代入与正规化，而不是把既有元定理当作自动继承的装饰。

参考资料

Robert Harper, Dependent Type Theory for Programming and Proving, CMU 课程讲义，依赖类型的判断、代入与计算。
Per Martin-Löf, Intuitionistic Type Theory, Bibliopolis, 1984，语境判断、Π/Σ 类型、命题相等与宇宙的规则讲义。
Bengt Nordström, Kent Petersson, and Jan M. Smith, Programming in Martin-Löf’s Type Theory, Oxford University Press, 1990，判断式语义、类型构造与程序推导。
Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016，依赖类型、判断与结构规则的现代形式化表述。
The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study, 2013，Ch. 1，内涵依赖类型论核心及其规则约定。

形式陈述 ​

反向链接

形式陈述