正规性 (类型论)

关于其它含义, 请参见 “正规”.

正规性是重写系统中演化而来的类型论的重要性质 (参见正规性 (重写系统)), 也可以作为典范性在任意语境中的推广.

相比重写系统版本的正规性, 类型论更注重它和语义的关系.

1定义

定义 1.1 (语义正规性). 若类型论存在一个语义解释, 且该语义能正确解释表达式的相等 (注意这里不是指相等类型中的相等), 则该类型论是正规的. 这样的正规性又叫语义正规性. “正确解释表达式的相等” 包含如下要求:

•	相等的表达式的语义解释相同.

•	不相等的表达式的语义解释不同.

•	对于每个语义对象, 存在一个唯一对应的表达式. 从语义对象获取对应表达式的过程叫读回.

语义解释和读回的复合操作可以看作一个对表达式化简的过程, 这代替了重写系统中 “重写” 的过程: $表达式语义解释读回语义对象$

语义正规性的思想可以理解为给类型论中的表达式通过语义解释划分出等价类. 例如在范畴语义中, 构造语义正规性就需要给出将类型论中的研究对象映射到某范畴中的研究对象的函数, 且该函数满足如下性质 (假设表达式被解释为态射, 且该类型论能讨论自然数类型):

•	$(λ x . x) y$ 和 $y$ 被解释为同一个态射, 这同一个态射对应的表达式是 $y$ .

•	$1 + 1$ 和 $2$ 被解释为同一个态射, 这同一个态射对应的表达式是 $2$ .

•	$1 + 2$ 和 $2$ 被解释为不同态射.

当然, 除了范畴论之外, 也可以在其它的理论中构造语义并讨论语义正规性, 这里不多赘述.

注 1.2. 类型论的正规性并不能通过对它的推理规则进行简单地归纳而得到, 而是需要使用更强的工具, 例如 Tait 可计算性.

若类型论满足语义正规性或强正规性, 那么该类型论的类型规则很有可能是可判定的.

•

术语翻译

正规性 • 英文 normalization

语义正规性 • 英文 normalization by evaluation