递归类型的元理论：从子类型到成员检查

# 递归类型的元理论：从子类型到成员检查 ## 1. 递归类型概述 递归类型在类型理论中占据着重要地位，它涉及到类型的自我引用和嵌套结构。例如，像 `(Top × Top) → Top` 和 `Top → (Top → (Top → ...))` 这样的类型表达式，展示了递归类型的复杂性和多样性。 ## 2. 子类型关系 ### 2.1 有限子类型 对于有限树类型，子类型关系被定义为单调函数的最小不动点。具体来说，两个有限树类型 `S` 和 `T` 存在子类型关系（即 `S` 是 `T` 的子类型），当且仅当 `(S, T) ∈ µSf`，其中单调函数 `Sf` 定义如下： ```plaintext Sf (R) = {(T, Top) | T ∈ Tf } ∪ {(S1 × S2, T1 × T2) | (S1, T1), (S2, T2) ∈ R} ∪ {(S1 → S2, T1 → T2) | (T1, S1), (S2, T2) ∈ R} ``` 这一函数对应着一系列推理规则： - `T <: Top` - `S1 <: T1`，`S2 <: T2` 则 `S1 × S2 <: T1 × T2` - `T1 <: S1`，`S2 <: T2` 则 `S1 → S2 <: T1 → T2` ### 2.2 无限子类型 对于有限或无限的树类型，子类型关系被定义为单调函数的最大不动点。两个树类型 `S` 和 `T` 存在子类型关系，当且仅当 `(S, T) ∈ νS`，其中函数 `S` 的定义与 `Sf` 类似： ```plaintext S(R) = {(T, Top) | T ∈ T } ∪ {(S1 × S2, T1 × T2) | (S1, T1), (S2, T2) ∈ R} ∪ {(S1 → S2, T1 → T2) | (T1, S1), (S2, T2) ∈ R} ``` 推理规则与有限子类型的规则相同，只是考虑的类型范围更广，并且取最大不动点。 ### 2.3 子类型关系的性质 #### 2.3.1 传递性 子类型关系的传递性是一个基本性质。如果子类型关系不具有传递性，那么在求值过程中类型的保持性这一关键性质将会失效。例如，假设存在类型 `S`、`T` 和 `U`，满足 `S <: T` 和 `T <: U`，但 `S` 不是 `U` 的子类型。设 `s` 是类型 `S` 的值，`f` 是类型 `U → Top` 的函数，那么项 `(λx:T. f x) s` 可以被类型化，但它会一步归约为类型错误的项 `f s`。 为了证明无限树类型的子类型关系 `νS` 是传递的，我们使用了如下引理： 设 `F ∈ P(U × U) → P(U × U)` 是单调函数。如果对于任何 `R ⊆ U × U`，都有 `TR(F(R)) ⊆ F(TR(R))`，那么 `νF` 是传递的。 证明过程如下： 因为 `νF` 是不动点，所以 `νF = F(νF)`，这意味着 `TR(νF) = TR(F(νF))`。根据引理的假设，`TR(νF) ⊆ F(TR(νF))`，即 `TR(νF)` 是 `F` - 一致的，根据共归纳原理，`TR(νF) ⊆ νF`，所以 `νF` 是传递的。 #### 2.3.2 自反性 练习建议证明无限树类型的子类型关系也是自反的。 ### 2.4 传递性的不同处理方式 在标准的归纳定义的子类型关系中，通常有两种呈现形式：声明式和算法式。声明式呈现包含显式的传递性规则（如果 `S <: U` 且 `U <: T`，则 `S <: T`），而算法式系统则不包含。传递性规则在声明式系统中有两个作用：一是让读者清楚地看到子类型关系是传递的；二是允许其他规则以更简单、更原始的形式陈述。 然而，对于共归纳定义的子类型关系，添加传递性规则会得到一个退化的关系。例如，对于生成函数 `FTR(R) = F(R) ∪ TR(R)`，其最大不动点 `νFTR` 是 `U × U` 上的全关系。因此，在共归纳设置中，我们通常只使用算法式呈现。 ## 3. 成员检查 ### 3.1 可逆生成函数 为了判断一个元素 `x` 是否属于生成函数 `F` 的最大不动点，我们引入了可逆生成函数的概念。一个生成函数 `F` 被称为可逆的，如果对于所有 `x ∈ U`，集合 `Gx = {X ⊆ U | x ∈ F(X)}` 要么为空，要么包含一个唯一的子集，该子集是所有其他子集的子集。 当 `F` 是可逆的时，部分函数 `supportF` 定义如下： ```plaintext supportF(x) = X if X ∈ Gx and ∀ ```