本文整理自 Luca Cardelli, Type Systems 的第七章内容。欢迎 star 和 follow。

等价性 (Equivalence)

为了便于讨论，我们此前跳过了一些类型断言。但是在一些复杂的类型系统中以及当需要捕捉程序的语义时这些断言仍然是必要的。我们在本节简要讨论一下。

类型等价(type equivalence)断言，形式为 ，可在类型等价关系并不明显且需要精确描述时使用。例如，某些类型系统将递归类型与其展开视为等价。因此在这种情况下，我们有 ，只要 。另一个例子是具有类型操作符 （从类型到类型的函数）的类型系统，具有以下形式归约规则： (编者: 这里是写错了吗🤔 不是 [X/B]A 吗？)。通常，类型等价断言在重新赋型(retyping)规则中使用，规定如果 且 ，则 。

一个项等价(term equivalence)断言确定了哪些程序的类型是等价的。它具有形式 。通过适当的规则，我们可以确定 。项等价断言可用于为程序提供带类型的语义：如果 是一个不可约表达式(irreducible expression)，那么我们可以将 的类型视为程序 的类型。