Martin-Löf 类型论

Martin-Löf 类型论是一种直觉主义依值类型论, 包含多种变体, 由 Per Martin-Löf 设计.

1介绍

(...)

语法

参见: 形式文法

语法 (或者文法) 定义了形式良好的表达式. 如在一般数学中 $1+1$ 是符合语法的, 但是 (仅仅考虑常规数学符号的情况下) $1+{+}_9\int$ 一般认为是不合语法的. 这与后面定义的 “类型良好” 不同, 如一般数学中 $1+1$ 和 ${\mathbb{F}}_p+{\int }_2^{5}x\mathrm{d}x$ 都符合语法, 但是后者一般认为没有意义, 因为加法一般是在交换群上定义的, 而 ${\mathbb{F}}_p$ 与 ${\int }_2^{5}x\mathrm{d}x$ 在没有额外的补充定义时不在同一个交换群中, 因而不是类型良好的.

但是, 在现代类型论的发展中, 语法的管辖范围与类型管辖的一部分范围逐渐变得模糊, 同时一些比较低级冗杂的语法逐渐被抛弃. 如在早期认为表达式是由字符串构成的, 因此需要处理括号与优先级的问题. 现在一般认为表达式本身是树状的, 并非字符串, 因此括号仅仅是为了方便在纸上节省空间而出现的, 不属于形式语法的一部分.

正如大部分依值类型论, Martin-Löf 类型论中类型与类型的元素在语法上是无法分离的, 因此需要一同定义.

类型

Martin-Löf 类型论中的类型都是依值类型.

(...)

变体与演化

•	早期版本中, Martin-Löf 类型论认为类型的类型就是类型, 但这引来了 Girard 悖论.

•	Martin-Löf 类型论有内涵和外延的版本. 外延的版本中无法实现完全自动化的类型检查, 但内涵的版本可以. 两者的具体区别在于相等类型的消去规则不同.

•	Martin-Löf 类型论加入泛等公理和高阶归纳类型后就是同伦类型论.

•	Martin-Löf 类型论的非直谓版本是构造演算. 早期版本的 Martin-Löf 类型论也是非直谓的, 但直接允许类型的非直谓多态也会招致逻辑不一致, 需要加以限制. 构造演算就加上了这些限制.

2规则

这里给出一套完整的规则.

定义 2.1. Martin-Löf 类型论中变量的语法用形式文法定义为$$v::=\mathrm{z}\mid \mathrm{s}v$$

书写时为了方便, 变量的语法占最高优先级, $\mathrm{s}$ 向右结合. 我们用 $M$ 指代表达式. 变量都是表达式. 表达式的其他形式在后文介绍. (... 定义变量替代)

定义语境为表达式的列表, 即$$\Gamma ::=ϵ\mid \Gamma ,M$$书写时为了方便, 将 $(((ϵ,M_1),M_2),\dots ),M_n$ 写作 $M_1,M_2,\dots ,M_n$.

我们引入四种判断:

•	$M_1:M_2$, 表示 $M_1$ 的类型是 $M_2$.
•	$M_1=M_2:M_3$, 表示 $M_1$ 与 $M_2$ 可以判断相等, 并且两者类型是 $M_3$.
•	$M_1\mathsf{type}$, 表示 $M_1$ 是类型.
•	$M_1=M_2\mathsf{type}$.

每个语境中都可以根据推导规则得出不同的判断, 记作 $\Gamma ⊢J$, 其中 $J$ 指代任何一个判断. 当语境明确时, 可以省略 $\Gamma ⊢$.

我们给出关于变量的两条规则:

$$\frac{}{\Gamma ,M⊢\mathrm{z}:M}$$

这条规则没有前置条件, 因此始终可用.

$$\frac{\Gamma ⊢v:M_1}{\Gamma ,M_2⊢\mathrm{s}v:M_1}$$

接下来, 我们将语法、规则、规约关系分成组, 方便阅读.

$\Pi$ 类型

主条目: Pi 类型

语法上, 添加三种构造表达式的方法, 用形式文法定义为:$$\begin{array}{rl}M& ::=\cdots \\ & \mid \Pi (M,M)\\ & \mid \lambda (M,M)\\ & \mid \mathrm{ap}(M,M)\end{array}$$将 $\mathrm{ap}(M_1,M_2)$ 写作 $(M_1{M}_2)$, 并且规定左结合, 优先级仅次于变量. 如 $M_1{M}_2(M_3{M}_4)$ 表示 $\mathrm{ap}(\mathrm{ap}(M_1,M_2),\mathrm{ap}(M_3,M_4))$.

$$\frac{\Gamma ⊢M_1\mathsf{type}\Gamma ,M_1⊢M_2\mathsf{type}}{\Gamma ⊢\Pi (M_1,M_2)\mathsf{type}}$$$$\frac{\Gamma ⊢M_1\mathsf{type}\Gamma ,M_1⊢M_2:M_3}{\Gamma ⊢\lambda (M_1,M_2):\Pi (M_1,M_3)}$$$$\frac{\Gamma ⊢M_1:\Pi (M_3,M_4)\Gamma ⊢M_2:M_3}{\Gamma ⊢(M_1{M}_2):M_4[M_2]}$$

$\Sigma$ 类型

主条目: Sigma 类型

无交并类型

主条目: 无交并类型

相等类型

主条目: 相等类型

有限类型

参见: 空类型; 单位类型

通过对单位类型和它自己取无交并, 就可以得到有两个实例的类型, 不断重复这个过程便可以得到任意有限大小的类型.

自然数类型

主条目: 自然数类型

宇宙类型

主条目: 宇宙 (类型论)

术语翻译

Martin-Löf 类型论 • 英文 Martin-Löf type theory (MLTT) • 德文 Martin-Löf-Typentheorie • 法文 théorie des types de Martin-Löf