类型不变性

在类型论中, 类型不变性是指对于两个语法上不一样但相等的表达式一定会拥有相同的类型的性质. 这听起来有些荒唐 (因为看起来显然成立), 但这只是因为这种叙述方式已经高度现代化. 如果站在重写系统的角度, 它听起来就成为了一个重要的性质而不是显然的性质:

考虑表达式 $Γ ⊢ u : A$ , 如果对 $u$ 进行重写 (例如将 $1 + 1$ 重写为 $2$ ), 那么得到的表达式类型依然是 $A$ 或者某个和 $A$ 相等的类型.

1证明手法

类型论的类型不变性一般可以直接通过对它的推理规则进行简单地归纳而得到. 另一个类似的简单性质是 “表达式 $u$ 要么是正规形式, 要么可以进一步重写”, 这两个性质一般放在一起讨论, 且统称为可进性与保型性.

这不像正规性一样需要使用更强的工具, 例如 Tait 可计算性.

几种情况可能导致类型论失去类型不变性:

•	在设计不佳的类型论中可能会遇到对表达式的过度重写的情况, 导致类型同时也被修改, 因此类型变化.
•	部分重写规则可能会将不同类型的表达式关联起来, 这显然会导致类型变化.

除此之外, 类型论可能加了过多的符号导致同一个符号可能在不同的地方含义不同, 并导致看起来相同的表达式有不同的类型. 这严格来说并不违反类型不变性, 但这可能导致类型论 “看起来” 类型变化.

如果类型会变化, 那么某些成立的等式可能在进行重写后就不成立了. 这显然违反等价原理.

术语翻译

类型不变性 • 英文 subject reduction

可进性与保型性 • 英文 progress and preservation