典范性

典范性是类型论的一种性质, 指空语境下的表达式都是由构造规则生成的.

这往往是在说类型论中所有 “函数应用” 都可以被消除, 因为函数应用是一种消去规则. 比如, 有公理的类型论就不满足典范性, 因为公理往往被视为一种函数, 而这些函数无法进一步展开.

典范性可以认为是空语境中的正规性加上对正规形式的形式要求.

一些观点认为, 满足典范性的类型论就可以被称为编程语言.

1定义

定义 1.1. 在类型论中, 完全由构造规则导出的表达式叫做典范形式, 或者说这个表达式是典范的.

注意该定义并不局限于空语境.

定义 1.2. 若在某类型论的空语境中, 任何类型的值均有典范形式 (或者说, 任何值均等价于一个典范形式), 那么这个类型论满足典范性.

定义 1.3. 若在某类型论的空语境中, 任何类型的值的正规形式也是典范形式, 那么这个类型论满足典范性.

注意, 1.3 没有假设值的典范形式的存在性, 仅讨论它们存在的情况下应该满足的性质. 而 1.2 要求了正规形式必须存在, 且满足这些性质.

定义 1.4. 考虑一个有自然数类型的类型论. 如果在空语境中, $N$ 类型的值均由 $0$ 和 $s$ 生成, 那么这个类型论满足典范性.

定义 1.5. 考虑一个立方类型论. 如果在仅包含 $I$ 类型的语境中, 任何类型的值的正规形式都是典范形式, 那么这个类型论满足立方典范性.

注 1.6. 类似 1.3, 我们可以给出 1.5 的弱化版本.

引理 2.1. 典范性蕴涵逻辑一致性.

证明. 如果类型论不一致, 那么存在值

u

使得

⊢ u : \emptyset

, 而空类型没有构造规则, 引起矛盾.

$□$

典范 (且正规) 的类型论:

•	简单类型论
•	立方类型论

不典范的类型论:

•	同伦类型论, 因为泛等公理的存在.

术语翻译

典范性 • 英文 canonicity • 法文 canonicité (f) • 拉丁文 canonitas (f) • 古希腊文 κανονικοσύνη (f)

典范 • 英文 canonical