[定义]
类型安全
[定义] 类型安全
采用 [定义] 类型与类型判断 的类型关系、 [定义] 多步归约 的运行关系，以及 [定义] 范式与受阻 的受阻判定。称这套语言规则是类型安全（type safety）的，如果对任意项 、 和类型 ：若 且 ，则 没有受阻。