递归类型 (Recursive Types)

Leasier · 2026-08-01 20:45:32 · 算法·理论

观察两个习以为常的递归类型 list 和 nat：

它们都有一些 引入形式 (introduction forms)，告诉我们如何 构造 (construct) 这种类型的值：nil、cons t t、zero、succ t。\ 它们都有一些 消除形式 (elimination forms)，告诉我们如何 破除 (destruct) 这种类型的值：isnil t、head t、tail t、iszero t、pred t。

引入与消除形式的一般化

通过和类型与积类型，考虑将引入形式的类型规则统一如下：

进一步地，我们尝试将所有递归类型的 fold 规则整合为统一的形式。留意到在同构意义下，我们可以认为：

或者说，\text{List}_A 是不动点方程

的一个解。引入递归符号 \mu，我们记：

类似地，记：

然后得到统一的 fold 规则：

其中 T 是一个关于“类型变元” X 的（有限）表达式。

从这个规则可见，每个递归类型的值无非是把具有类型 [X \mapsto \mu X.T] T 的 展开形式 (unfolding) 折叠 (folding) 为具有类型 \mu X.T 所得的结果。

接下来给出对偶的 unfold 规则：

上面的设计将 fold 和 unfold 视为“一对互逆的函数”，它们被 定义 为类型间的“同构”：

这种设计被称为 同构递归 (iso-recursive)。

递归类型举隅

下面通过 元组 (tuple)、选项 (variant) 和 不动点组合子 (fixed-point combinator) 的语法略举几例。

元组：用 \{T_1, T_2\} 代表积类型 T_1 \times T_2，其项写作 \{t_1, t_2\} \ (t_1 \in T_1, t_2 \in T_2)。可以扩展到带标签 n 元组的形式。\ 选项：用 \langle T_1, T_2 \rangle 代表和类型 T_1 + T_2，其项写作 \text{inl } t_1, \text{inr } t_2 \ (t_1 \in T_1, t_2 \in T_2)。可以扩展到带标签 n 选项的形式。\ 不动点组合子：用 \text{fix } (\lambda f : T_1 \to T_2. \ t) 代表以 t 为函数体的递归函数 f : T_1 \to T_2。

1. \text{List}_A = \mu X. \langle \text{Unit}, \{A, X\} \rangle

2. \text{Hungry}_A = \mu X. A \to X

这个递归类型被称作“饥饿类型”，是因为无论你给它传入多少（有限）次参数，它只会返回一个“还想要你传入参数”的函数。

则有：

3. \text{Stream}_A = \mu X. \text{Unit} \to \{A, X\}

4. 纯函数式的“对象”

在 OOP 中，对于一个“对象”，我们的操作往往可以分为如下两类：

• 查询一些信息。
• 改变一些信息，采取原地更新或者构造新的对象的方式。

（暂时可以理解为）在纯函数式编程中，任何对象一经创建后都是 不可变 (immutable‌)，因此我们假定改变信息统一为构造新的对象。

例如下面这个计数器对象：

5. 发散项 (divergence)

在无类型 Lambda 演算中，我们构造了如下 \omega 组合子：

这个项会 发散 (diverge)，因为对它进行一次 \beta-约简会得到自身，导致求值会无限进行下去而不会终止。

现在我们希望给 \omega 赋予类型 T，这无非是期待一个类型 \text{Div}_T 使得：

这导出类型等式 \text{Div}_T = \text{Div}_T \to T，也就是说：

在此基础上，我们可以构造具有 任意 类型 T 的项 \omega_T：

经过一次 \beta-约简和 unfold-fold 相消，\omega_T 将重新得到自身。

这意味着 STLC 的 强约简 (strong normalization) 性质被打破了：我们没有使用不动点组合子，但构造出了一个具有类型却不能终止的项。

6. 不动点组合子

仿照 \omega_T，我们来构造经典的 Y 组合子：

接着在 OCaml 中实现之并尝试构造一个阶乘函数：

type 't div = Fold of ('t div -> 't)

let fix_fail (f : 't -> 't) : 't =
  let inner x = 
    let Fold x_unfolded =
      x
    in
      f (x_unfolded x)
  in
    inner (Fold inner)

let factorial_step (self : int -> int) (n : int) : int =
  if n = 0 then 1 
  else n * self (n - 1)

let factorial = fix_fail factorial_step

……然后却发现运行到最后一行时（尽管我们没有给 factorial 传入任何参数！）报错了：

Stack overflow during evaluation (looping recursion?).

这是因为在定义 let factorial = fix_fail factorial_step 时会进行求值，经过一次 \beta-约简得到 factorial_step (fix_fail factorial_step)，但此时内部的 fix_fail factorial_step 仍不是值，而 OCaml 是 严格求值 (strict evaluation) 的，因此会继续化简。

因此在 OCaml 中实现时，我们需要推迟内部的求值。由于我们知道代码中 't 是函数类型，且 \lambda-抽象是值，故采取一些 \eta-展开的小技巧即可：

type 't div = Fold of ('t div -> 't)

let fix (f : ('a -> 'b) -> ('a -> 'b)) : 'a -> 'b =
  let inner x = 
    let Fold x_unfolded =
      x
    in
      f (fun arg -> x_unfolded x arg)
  in
    inner (Fold inner)

let fact_step (self : int -> int) (n : int) : int =
  if n = 0 then 1 
  else n * self (n - 1)

let factorial = fix fact_step

let _ = Printf.printf "5! = %d\n" (factorial 5)

7. 无类型 \lambda 演算的嵌入

回忆无类型 \lambda 演算的语法形式：

定义递归类型 D 表示所有无类型 \lambda 演算的项，并辅以相关函数 \text{lam}, \text{app}：

则可以递归地将所有无类型 \lambda 演算的项 t 嵌入为有递归类型的有类型 \lambda 演算的项 t^*：

• 这里假定 D 中包含所有 t 中可能包含的（至多可数个）变量名。

同构递归类型 (iso-recursive types, \lambda \mu) 的形式化

1. 语法形式

2. 类型规则

3. 计算规则（严格求值）

除同构递归外，还有一种描述思路称为 等价递归 (equi-recursive)，即直接将 \mu X.T 和 [X \mapsto \mu X.T] T 等同、而不需要通过显式的 fold 和 unfold 加以转换、区分。

这样做意在强调二者展开后作为一棵“（无穷）类型树”是同构的，但这一思路下类型检查的实现更加复杂。

正类型算子 (positive type operators)

1. 问题一：逻辑不一致？

前面我们给发散项 \omega_T 也赋予了类型 T，但这会使我们的类型系统与经典的 柯里-霍华德对应 (Curry-Howard correspondance) 不再相容：

• C-H 对应指出 命题即类型：只要我们能够给出某个命题对应的类型的一个值，就可以认为我们给出了这个命题的一个证明。
• 但如果允许发散项的存在，这意味着我们能够给出任何一个命题的证明，这与（直觉主义）逻辑并不相容！

2. 问题二：无法确保语言的性质？

设计类型系统的初衷之一就是 确保程序在通过类型检查时具有某种良好的性质，但前面我们已经知道递归类型会破坏语言（假定没有不动点组合子作为原语）的强化简性。

总之，为使这套类型系统更加实用，我们有必要对递归类型加以限制。观察下面四个递归类型：

在不允许使用不动点组合子的前提下，\text{List}_A, \text{Stream}_A 看上去不会破坏强化简性，\text{Div}_T 我们已知会破坏，而将 \omega 组合子原样嵌入到有递归类型的有类型 \lambda 演算中就得到了一个类型为 D 的发散项。

由此猜想 逆变 (contravariant) 位的递归定义（即类型变量 X 出现在箭头左侧）会破坏强化简性。

由此考虑定义正类型算子，表示没有违反这样的规定的递归类型 X.T \text{ pos}：

归纳类型与余归纳类型 (inductive types and coinductive types)

我们将归纳类型和余归纳类型限制在正类型算子导出的递归类型上：

并规定归纳类型对应满足不动点方程的 最小解，余归纳类型对应满足不动点方程的 最大解。

• “最小”“最大”两个前缀将在后面展开解释和证明。

为了保证语言的表达能力——即某些“常见为正确”的递归模式仍然成立——、并期待强化简性也成立，我们有必要讨论哪些递归是我们可以允许的。

归纳类型的良基递归 (well-founded recursion)

考虑一个常见的情形：我们需要求一个序列的长度、又或者一个自然数序列的和。此时 OCaml 中一个正常的递归实现形如：

type intlist =
    Nil
  | Cons of int * intlist

let rec len (l : intlist) : int =
  match l with
    Nil -> 0
  | Cons (a, l') -> 1 + len l'

let rec sum (l : intlist) : int =
  match l with
    Nil -> 0
  | Cons (a, l') -> a + sum l'

• 注：OCaml 中可以不用写 Nil unit 而直接写 Nil，这是等价的。

可以发现此时我们总是在通过 match ... with ... 语法拆出 \text{unfold } [\text{List}_{\text{Int}}] \ l 的 \text{Unit} + \text{Int} \times \text{List}_{\text{Int}} 的两种情况，而剩余部分 l' 的长度总是比 l 小，所以对于一个（有限长的）序列 l 来说，递归总是会终止。

这种“结构规整”的递归函数的类型规则和求值规则可以对 \text{List}_A 一般化如下：

其中：

例如对于上面的 sum 来说就是：

一般化到归纳类型 \text{ind}(X.T) 中，得到 iter 的类型规则：

而对于求值规则，可以发现这与 X.T 的结构有关：相当于是维持 T 中不是 X 的部分不变、是 X 的部分替换为递归求值。因此有必要定义一个 泛型映射 (generic mapping) 来沿着 T 的结构完成替换：

借由 map 得到 iter 最终的求值规则：

余归纳类型的良基递归

直觉上讲，与归纳类型的良基递归——“遍历有限的结构”——不同，余归纳类型的结构本身允许无限，则对应的有限步操作就是——“生成有限的部分项”。

考察 \text{Stream}_A = \mu X. A \times X，我们有一个类型为 S 的“数据生成器”，你“挤它一次”就给你流中的第一项 a : A、以及剩下一个新的类型为 S 的生成器，再“挤它一次”就能生成下一项，依此类推。如此，这个生成器就唯一确定了这个流。

形式化地，写出如下类型规则和求值规则：

其中 \lambda x : S. \ t_2 : S \to A \times S 就是上面所说的“数据生成器”。

通过 gen，我们可以定义这样的流：

类比 iter，我们可以最终写出余归纳类型的类型规则与求值规则：

归纳类型与余归纳类型的语法形式

• 可以发现 fold 和 gen 分别作为归纳类型和余归纳类型的生成子、被视作值。

一般递归类型的两种语义

1. 急切语义 (eager semantics) / 归纳类型风格

(i) 语法形式

(ii) 计算规则

在这一语义下，可以模拟余归纳类型：使用 \lambda-抽象推迟内部的化简操作即可。OCaml 使用的是这种风格。

2. 惰性语义 (lazy semantics) / 余归纳类型风格

(i) 语法形式

• 也就是说，现在 \text{fold } [X.T] 像 \lambda-抽象一样，不允许在不调用 unfold 时化简其内部。

(ii) 计算规则

在这一语义下，不能模拟归纳类型。Haskell 使用的是这种风格。

\mu-类型及其子类关系

下面默认讨论的是 等价递归 设定下的子类关系：此时我们将 \mu X.T 与 [X \mapsto \mu X.T] T 完全等同，而不要求通过 fold 和 unfold 等进行类型转换。

首先考虑一个问题：若 \text{Even} <: \text{Nat}，是否成立 \mu X. \text{Nat} \to (\text{Even} \times X) <: \mu X. \text{Even} \to (\text{Nat} \times X)？

如果直接把无限的类型树画出来，可以发现对应位置的 \text{Nat}, \text{Even} 满足逆变与协变的相关要求，因此直觉上我们认为这个子类关系成立。下面对递归类型的子类关系加以讨论。

定义 原始 \mu-类型 (raw \mu-types) 为如下定义的表达式集合：

• 这里为简洁起见，只引入了 顶类型 \text{Top}，它被定义为所有类型的父类型。

其中类型变量 X 取值于一个固定的可数集 X_1, X_2, \cdots, X_n, \cdots 中。

称原始 \mu-类型 T 收缩 (contractive)，若对于 T 的所有形如 \mu X. \mu X_1. \cdots \mu X_n. S 的子表达式，S \neq X；也即诸如 \mu X. X, \mu X. \mu Y. \mu Z. Y 的类型不收缩。进一步地，称收缩的原始 \mu-类型为 \mu-类型，记所有 \mu-类型的集合为 \mathcal{T}_m。

• 这里相当于排除了直觉上“不构成一棵无限的类型树”的情况。

首先尝试一种归纳定义 \mu-类型的子类关系的方法：

但尝试通过原有的 归纳定义 思路进行子类检查时会——如我们所料的那般（因为类型树是无限的）——发生无限循环。

例如 S = \mu X. \text{Top} \times X, T = \mu X. \text{Top} \times (\text{Top} \times X)：

因此考虑将子类关系改为“余归纳定义”的，即直觉上允许“循环论证”；在操作上，我们直觉地引入下面的 假设子类推导 (hypothetical subtyping)。

称 \Sigma \vdash S <: T，若可以在假设 \Sigma 中子类关系成立的前提下推导出 S <: T。然后给出一个符合直觉的推导规则：

……不过事实上这个推导规则在实现方面是存在一些问题的。我们将在后面加以阐述。

归纳类型与余归纳类型的元理论

从现在开始，我们的主要任务为：将上面理论的“直觉”部分加以更严格的规约，并给出一些关键命题的证明；以及在此基础上给出相应的算法等。

一般的归纳与余归纳原理

下面的讨论皆在给定论域 \mathcal{U} 的前提下进行。

称函数 F : \mathcal{P}(\mathcal{U}) \to \mathcal{P}(\mathcal{U}) 单调 (monotone)，若 X \subset Y \subset \mathcal{U} \Rightarrow F(X) \subset F(Y)。

在下面的讨论中，我们总是假设 F 单调。

设函数 F : \mathcal{P}(\mathcal{U}) \to \mathcal{P}(\mathcal{U})，对于 X \subset \mathcal{U}：\ (1) 称 X 是 F-闭 (F-closed) 的，若 F(X) \subset X。\ (2) 称 X 是 F-保持 (F-consistent) 的，若 X \subset F(X)。\ (3) 称 X 是 F 的一个不动点，若 F(X) = X。

一个实用的看法是：将 \mathcal{U} 视作一族命题，函数 F 将一族命题映射到其所能推导出的命题；若 X 是 F-闭的，则再次使用推导规则族 F 不会让能推导出的命题变多；若 X 是 F-保持的，则任何一个推导出的命题都可以使用推导规则族 F 给出证明（允许循环论证）。

下面的“最小”“最大”都是在子集关系定义的偏序集 (\mathcal{P}(\mathcal{U}), \subset) 中讨论的。

Knaster-Tarski 定理 (1955)

(1) 所有 F-闭的集合的交为 F 的最小不动点，记作 \mu F。\ (2) 所以 F-保持的集合的并为 F 的最大不动点，记作 \nu F。

Proof. 下面只证明 (1)，(2) 是同理的。\ 记 C = \{X \subset \mathcal{U} \mid F(X) \subset X\}，由 F(\mathcal{U}) \subset \mathcal{U} 可知 C 非空，故可令 P 为 C 中所有集合的交。\

再由 $F$ 单调可知 $F(F(P)) \subset F(P)$，则 $F(P) \in C$，故 $P \subset F(P)$。\ 总之 $F(P) = P$，故 $P$ 为 $F$ 的不动点；最后交的性质指出其为 $F$ 的最小不动点 $\mu F$。 **推论：归纳与余归纳原理** > (1) 归纳原理：若 $X$ 是 $F$-闭的，则 $\mu F \subset X$。\ > (2) 余归纳原理：若 $X$ 是 $F$-保持的，则 $X \subset \nu F$。

上面这样说起来可能比较抽象，我们来看一个简单的例子——自然数。

令 \mathcal{U} = \omega \sqcup \{\omega\}，F(X) = \{\emptyset\} \sqcup \{n \cup \{n\} \mid n \in X \backslash \{\omega\}\} \sqcup (X \cap \omega)，则：

• 所有 F-闭的集合一定满足 0 \in X，进而自然数上的归纳法指出 \omega \subset X，因而 \mu F = \omega。
• 留意到 \omega 是 F-保持的，故 \nu F = \omega \sqcup \{\omega\}。

前者构造出的就是归纳类型 \text{Nat}，后者构造出的则是余归纳类型 \text{CoNat}。下面演示在 Rocq 中定义嵌入 \text{Nat} \to \text{CoNat} 并证明其单而不满：

Require Import Setoid.

Inductive nat : Set :=
  | zero
  | succ (n : nat).

CoInductive conat : Set :=
  | cozero
  | cosucc (n : conat).

Fixpoint embed (n : nat) : conat :=
  match n with
  | zero => cozero
  | succ n' => cosucc (embed n')
  end.

CoFixpoint omega : conat :=
  cosucc omega.

Theorem embed_injective : forall (n m : nat), n <> m -> embed n <> embed m.
Proof.
  intros n m Hneq Heq. apply Hneq. clear Hneq.
  generalize dependent m. induction n as [| n' IHn']; intros m Heq.
  - (* n = zero *)
    destruct m as [| m'].
    + (* m = zero *)
      reflexivity.
    + (* m = succ m' *)
      simpl in Heq. discriminate.
  - (* n = succ n' *)
    destruct m as [| m'].
    + (* m = zero *)
      simpl in Heq. discriminate.
    + (* m = succ m' *)
      simpl in Heq. inversion Heq. apply IHn' in H0. rewrite -> H0. reflexivity.
Qed.

Lemma conat_unfold : forall (c : conat), 
  c = match c with
      | cozero => cozero
      | cosucc c' => cosucc c'
      end.
Proof.
  intro c. destruct c; reflexivity.
Qed.

(* 这里是解决一个技术问题：omega 的定义为 cofix omega : conat := cosucc omega 而非 cosucc omega，需要用一次 match 去除 cofix 成分得到直觉上的定义式。 *)
Lemma omega_unfold : omega = cosucc omega.
Proof.
  rewrite (conat_unfold omega) at 1. reflexivity.
Qed.

Theorem embed_not_surjective : exists (cn : conat), forall (n : nat), cn <> embed n.
Proof.
  exists omega. intros n. induction n as [| n' IHn'];
  intros Hn; rewrite omega_unfold in Hn.
  - (* n = zero *)
    simpl in Hn. discriminate.
  - (* n = succ n' *)
    simpl in Hn. inversion Hn. apply IHn'. apply H0.
Qed.

有限与无限类型

首先形式化地定义前面提到的 类型树 的概念：我们将二叉树建模为一个 偏函数 (partial function)。简洁起见，我们只考虑 \text{Top} 这一种基础类型。

下面用 \pi, \sigma 指代一个任意有限长的字符串 \{L, R\}^*，并用 \emptyset 指代空串。

类型树指偏函数 T \in \{L, R\}^* \to \{\text{Top}, \to, \times\}，满足如下条件：

(1) T(\emptyset) 有定义。\ (2) 若 T(\pi \sigma) 有定义，则 T(\pi) 也有定义。\ (3) 若 T(\pi) = \text{Top}，则 T(\pi L), T(\pi R) 没有定义。\ (4) 若 T(\pi) = \to 或 T(\pi) = \times，则 T(\pi L), T(\pi R) 有定义。

称类型树 T 有限，若定义域 \text{dom}(T) \subset \{L, R\}^* 有限。\ 记所有类型树组成的集合为 \mathcal{T}，其中所有有限类型树组成的集合为 \mathcal{T}_f。

例如：

在这一定义的基础上，下面的语法描述：

就可以定义为论域 \mathcal{T} 上的单调函数 F：

其中 T = \text{rooted}(c, T_1, T_2) 定义为这样一个偏函数：

• (i) T(\emptyset) = c。
• (ii) T(L \pi) 有定义当且仅当 T_1(\pi) 有定义，此时 T(L \pi) = T_1(\pi)。
• (iii) T(R \pi) 有定义当且仅当 T_2(\pi) 有定义，此时 T(R \pi) = T_2(\pi)。

由此 F 便具有最小不动点 \mu F：容易验证这无非是 \mathcal{T}_f；同时也有最大不动点 \nu F：可能稍显出人意料地，容易验证这就是 \mathcal{T}。

• 下面再出现 \text{rooted}(\to, T_1, T_2), \text{rooted}(\times, T_1, T_2) 时，简洁起见就写成 T_1 \to T_2, T_1 \times T_2。

基于类型树的子类理论

1. 有限子类理论

用上面的思路牛刀小试：对 有限类型 而言，所谓子类关系的定义无非是指定一个单调函数 S_f : \mathcal{P}(\mathcal{T}_f \times \mathcal{T}_f) \to \mathcal{P}(\mathcal{T}_f \times \mathcal{T}_f)：

这正是子类理论中 \text{S-Top}, \text{S-Arrow}, \text{S-Prod} 的直接翻译。

设 S, T \in \mathcal{T}_f，我们称 S 为 T 的子类，若 (S, T) \in \mu S_f，记作 S <: T。

2. 无限子类理论

现在将论域从 \mathcal{T}_f 扩大到 \mathcal{T}。对这之中的（有限或无限）类型而言，指定一个单调函数 S : \mathcal{P}(\mathcal{T} \times \mathcal{T}) \to \mathcal{P}(\mathcal{T} \times \mathcal{T})：

设 S, T \in \mathcal{T}_f，与上次取 最小不动点 不同，手动处理 \mu-类型的子类关系的经验驱使我们取 最大不动点：我们称 T_1 为 T_2 的子类，若 (T_1, T_2) \in \nu S，记作 T_1 <: T_2。

接下来简单验证一下这种取法的有效性：我们不希望取最大不动点使得 \nu S = \mathcal{T} \times \mathcal{T}，要不然子类关系退化为恒真命题。举例则是简单的：容易验证 \forall T \neq \mathcal{T} \backslash \{\text{Top}\}, \text{Top} <: T 不成立。

在 Chapter 16 中我们已经证明了有限子类理论中的子类关系具有自反性和传递性，这是类型系统的保持性成立的关键所在；因此有必要证明无限子类理论中的子类关系仍具有这两个性质。

首先用集合的语言重述自反性和传递性的定义：

称关系 R \subset \mathcal{U} \times \mathcal{U} 自反，若 \mathcal{I}_{\mathcal{U}} \triangleq \{(x, x) \mid x \in \mathcal{U}\} \subset R。 称关系 R \subset \mathcal{U} \times \mathcal{U} 传递，若 R 在单调函数 TR(R) = \{(x, y) \mid \exists z \in \mathcal{U}, \text{s.t. } (x, z), (z, y) \in R\} 下封闭。

自反性的证明是简明的：

定理：无限子类关系自反

Proof. 由余归纳原理可知只需证明 \mathcal{I}_{\mathcal{F}} 是 S-保持的：考察所有 (T, T), T \in \mathcal{F}，讨论 T 的形态即可。

对于传递性的证明，首先陈述下面的引理：

引理：最大不动点传递的充分条件

设 F 为 \mathcal{U} 上的单调函数，若 \forall R \subset \mathcal{U} \times \mathcal{U}, TR(F(R)) \subset T(FR(R))，则 \nu F 传递。

Proof. 由 \nu F 为不动点可知 \nu F = F(\nu F)，则有 TR(\nu F) = TR(F(\nu F))，由条件可知 TR(\nu F) \subset F(TR(\nu F))。由余归纳原理可知 TR(\nu F) \subset \nu F，此即传递性的定义。

最终得到如下定理：

定理：无限子类关系传递

Proof. 由引理可知只需证明 \forall R \subset \mathcal{T} \times \mathcal{T}, TR(S(R)) \subset S(TR(R))。\ 设 (S, T) \in TR(S(R))，则 \exists U \in \mathcal{T}, \text{s.t. } (S, U), (U, T) \in S(R)，下面对 U 的形态分类讨论：\ (i) 若 U = \text{Top}，易见只能是 T = \text{Top}，由 S 的定义可知 (S, T) = (S, \text{Top}) \in S(TR(R))。\ (ii) 若 U = U_1 \to U_2，当 T = \text{Top} 同 (i) 显然，否则只能为 T = T_1 \to T_2，此时有 (T_1, U_1), (U_2, T_2) \in R；同时只能为 S = S_1 \to S_2，此时有 (U_1, S_1), (S_2, U_2) \in R。\ 由 TR 的定义可知 (T_1, S_1), (S_2, T_2) \in TR(R)，进而即有 (S, T) = (S_1 \to S_2, T_1 \to T_2) \in S(TR(R))。\ (iii) 若 U = U_1 \times U_2，同 (ii) 理可得。

在这段讨论的最后有必要解释一下：为什么在无限子类关系关系的讨论中，我们不能像先前讨论有限子类关系时那样，自然地添加上自反性和传递性这两条。

——最关键的区别在于有限子类关系是 最小不动点、或者说是由 归纳关系 定义的，而无限子类关系是 最大不动点、或者说是由 余归纳关系 定义的。

命题：并集归纳关系的最小不动点

设 F, G 为 \mathcal{U} 上的单调函数，令 H(X) = F(X) \cup G(x)，则 \mu H 为同时满足 F-闭和 G-闭的最小解。

Proof. 由定义可知 \mu H = H(\mu H) = F(\mu H) \cup G(\mu H) \Rightarrow \mu H \subset F(\mu H), G(\mu H)，故 \mu H 同时满足 F-闭和 G-闭。\ 设 X 也同时满足 F-闭和 G-闭，则 F(X) \subset X, G(X) \subset X \Rightarrow H(X) = F(X) \cup G(X) \subset X，由余归纳原理即得 \mu H \subset X，再由 X 的任意性即得 \mu H 的最小性。

命题：与传递性并集所得余归纳关系的最小不动点

设 F 为 \mathcal{U} \times \mathcal{U} 上的单调函数，令 F^{TR}(X) = F(X) \cup TR(X)，则 \nu F^{TR} = \mathcal{U} \times \mathcal{U}。

Proof. 显见 \mathcal{U} \times \mathcal{U} 确为 \nu F^{TR} 的不动点，进而也为其最大不动点。

不动点的成员判定

子类判断等关系判定问题可以一般化为：

给定论域 \mathcal{U}、其上的单调函数 F 和 x \in \mathcal{U}，如何判定 x \in \mu / \nu F 是否成立？

对于这样的一个 x，我们可能有很多生成它的方法：即存在多个 X 使得 x \in F(X)，此时称 X 为 x 的一个 生成集 (generating set)。进一步地，由 F 的单调性可以想见应当存在一些 极小 的生成集；我们此处将讨论的 F 则是满足进一步的条件。

称 \mathcal{U} 上的单调函数 F 可逆 (invertible)，若 \forall x \in \mathcal{U}，集族

要么为空、要么 G_x 中存在唯一集合使得其为 G_x 中所有集合的子集。

当 F 可逆，定义偏函数 支撑集 (supporting set) \text{support}_F : \mathcal{U} \to \mathcal{P}(\mathcal{U})：

并将其延拓到 \mathcal{P}(\mathcal{U}) 上：

容易验证 S_f, S 可逆，并有支撑集为：

称 x \in \mathcal{U} 是 F-支撑 (F-supported) 的，若 \text{support}_F(x) 有定义。\ 特别地，称一个 F-支撑元素 x 是 F-基本 (F-ground) 的，若 \text{support}_F(x) = \varnothing。

显见非 F-支撑的元素不会出现在任何 F(X) 中，而 F-基本的元素会出现在任一 F(X) 中。

下面给出用于进行 最大不动点 成员判定的（偏）函数 \text{gfp}_F : \mathcal{P}(\mathcal{U}) \to \text{Bool}：

直观地说，\text{gfp}_F(X) 从 X 开始，当 \text{support}_F(X) \not\subset X 就把它加入 X 中，直到其 F-一致，又或者出现了不受支撑的元素。

• 方便起见，记 \text{gfp}_F(x) = \text{gfp}_F(\{x\})。

余下的任务就是说明 \text{gfp} 的正确性和（对于某些 F 的）终止性。

引理：受支撑的充要条件

Proof. 只需证明 x \in F(Y) 当且仅当 \text{support}_F(x) 有定义且 \text{support}_F(x) \subset Y。\ 必要性：由 x \in F(Y) 可知 Y \in G_x，故 G_x \neq \varnothing，进而 \text{support}_F(X) 有定义且 \text{support}_F(X) \subset Y。\ 充分性：由 \text{support}_F(X) 有定义且 \text{support}_F(X) \subset Y，据 F 的单调性可知 F(\text{support}_F(X)) \subset F(Y)，而由定义有 x \in F(\text{support}(x))，故 x \in F(Y)。

推论：受不动点支撑的充要条件

设 P 为 F 的一个不动点，则 X \subset P 当且仅当 \text{support}_F(X) 有定义且 \text{support}_F(X) \subset P。

Proof. 在上面的引理中取 Y = P = F(P) 即得。

定理：\text{gfp} 的正确性

当 \text{gfp}_F(X) 的计算过程终止，\text{gfp}_F(X) = \text{true} 当且仅当 X \subset \nu F。

Proof. 考虑对 \text{gfp}_F(X) 的计算过程归纳：\ (i) 若走了第一分支，此时 \text{support}_F(X) 无定义、返回 \text{false}，由上述推论可知 X \not\subset \nu F。\ (ii) 若走了第二分支，此时 \text{support}_F(X) 有定义且 \text{support}_F(X) \subset X、返回 \text{true}，由上述引理可知 X \subset F(X)，由余归纳原理可知 X \subset \nu F。\ (iii) 若走了第三分支，讨论 \text{gfp}_F(X \cup \text{support}_F(X)) 的返回值：

I. 若返回 \text{true}，则由归纳假设可知 X \cup \text{support}_F(X) \subset \nu F，进而有 X \subset \nu F。\ II. 若返回 \text{false}，则由归纳假设可知 X \cup \text{support}_F(X) \not\subset \nu F，此时要么 X \not\subset \nu F；又要么 \text{support}_F(X) \not\subset \nu F，由推论可知 X \not\subset F。

为了分析 \text{gfp} 的终止性，记：

则递归终止前，所能访问到的点集不会超出：

这无非是说 \text{reachable}_F 是 归纳定义 的。

• 方便起见，记 \text{reachable}_F(x) = \text{reachable}_F(\{x\})。

这就足以让我们推出下面这个看上去并不很强的条件。

称可逆的 \mathcal{U} 上的单调函数 F 状态有限 (finite state)，若 \forall x \in \mathcal{U}, \text{reachable}_F(x) 为有限集。

定理：\text{gfp} 的条件终止性

若 F 状态有限，则任给有限集 X \subset \mathcal{U}，\text{gfp}_F(X) 终止。

Proof. 在终止前参数集合大小单调递增、同时有上界 |\text{reachable}_F(X)| \leq \displaystyle\sum_{x \in X} |\text{reachable}_F(x)| \in \mathbb{N}，故必然终止。

类似地，给出用于进行 最小不动点 成员判定的（偏）函数 \text{lfp}_F : \mathcal{P}(\mathcal{U}) \to \text{Bool}：

定理：\text{lfp} 的正确性

当 \text{lfp}_F(X) 的计算过程终止，\text{lfp}_F(X) = \text{true} 当且仅当 X \subset \mu F。

Proof. 对 \text{lfp}_F(X) 的计算过程归纳即可。

当从 x \in X 出发可以走出一条无限长的路径——这可能意味着可以走得“无限远”、也可能意味着走进了环。排除这一情况后我们将得到最终的定理。

定理：\text{lfp} 的条件终止性

若 F 状态有限，则任给不能到达任何环的有限集 X \subset \mathcal{U}，\text{lfp}_F(X) 终止。

Proof. 在终止前诸次参数集合的并集的大小单调递增、同时有上界 |\text{reachable}_F(X)| \leq \displaystyle\sum_{x \in X} |\text{reachable}_F(x)| \in \mathbb{N}，故必然终止。

最大不动点的假设判定算法

在上面 \text{gfp} 的计算过程中，观察到终止前 X 中的元素只会不断增加，如果每次都要继承原有已经考虑过的元素属实有些低效了。能不能消除这些重复的计算呢？

下面给出基于这一思路的偏函数 \text{gfp}^a_F : \mathcal{P}(\mathcal{U}) \times \mathcal{P}(\mathcal{U}) \to \text{Bool}：

• 此处的 A 可以说就是前面讨论的“假设子类推导”的 \sigma。

为检查 x \in \nu F 是否成立，我们断言只需计算 \text{gfp}^a_F(\varnothing, \{x\})。下面给出算法正确性的陈述和证明。

定理：\text{gfp}^a 的正确性\ 当 \text{gfp}^a_F(X) 的计算过程终止：

(1) 若 \text{support}_F(A) \subset A \cup X 且 \text{gfp}^a_F(A, X) = \text{true}，则 A \cup X \subset \nu F。\ (2) 若 \text{gfp}^a_F(A, X) = \text{false}，则 X \not\in \nu F。

Proof. 对计算过程归纳即可。

这一算法（及后面的算法）具有与 \text{gfp} 一致的终止条件，证明略去。

上面算法的一个变体是 逐个考虑每个新并入的元素，并通过返回值的形式追踪假设集 A 的变化。说起来可能有些抽象，还是照例给出偏函数 \text{gfp}^t_F : \mathcal{P}(\mathcal{U}) \times \mathcal{U} \to \mathcal{P}(\mathcal{U}) 的伪代码：

• 为便叙述，我们规定当 let x = t1 in t2 中 t1 求值失败时，整个语句求值也失败。

由于这里不再是 \text{gfp}^a 那样的 尾递归 (tail-recursive) 形式，我们需要考虑每一步 A_i = \text{gfp}_F^t(A_{i - 1}, x_i) 时的增量：原本有一些“待办事项” X，这一步成功将 x_i 加入假设，且剩余的支撑义务不出 X 之外。这一思路推出了下面这个引理。

引理：单步 \text{gfp}^t 的性质

(1) A \cup \{x\} \subset \text{gfp}_F^t(A, x)。\ (2) 若 \text{support}_F(A) \subset A \cup X \cup \{x\} 且 \text{gfp}^t_F(A, x) = A'，则 \text{support}_F(A') \subset A' \cup X。

Proof. (1) 对计算过程归纳即可。\ (2) 对 \text{gfp}^t_F(A, x) 的计算过程归纳，若 x \in A 则 A' = A，命题显然成立。\ 下面讨论 \text{support}_F(x) = \{x_1, \cdots, x_n\} 的情形，考虑对 k = \{0, \cdots, n\} 归纳，则只需证明 \text{support}_F(A_k) \subset A_k \cup X \cup \{x_{k + 1}, \cdots, x_n\}。\ 若 k = 0 命题显然成立，而当 0 < k \leq n 由内层归纳假设可知 \text{support}_F(A_{k - 1}) \subset A_{k - 1} \cup X \cup \{x_k, \cdots, x_n\} = A_{k - 1} \cup (X \cup \{x_{k + 1}, \cdots, x_n\}) \cup \{x_k\}，由外层归纳假设即得 \text{support}_F(A_k) \subset A_k \cup X \cup \{x_{k + 1}, \cdots, x_n\}。

定理：\text{gfp}^t 的正确性

(1) 若 \text{gfp}^t_F(\varnothing, x) = A'，则 x \in \nu F。\ (2) 若 \text{gfp}^t_F(\varnothing, x) 失败，则 x \not\in \nu F。

Proof. (1) 由上面引理 (1) 可知 x \in A'，由上面引理 (2) 可知 \text{support}_F(A') \subset A'，再由余归纳原理可知 A' \subset \nu F，故 x \in \nu F。\ (2) 对计算过程归纳，\text{support}_F(x) 未定义的情形是显然的，对逐步增量的情形则讨论失败在哪一步，结合由上面引理 (2) 可以证得。

规范树 (regular trees) 与 \mu-类型

上面所有计算最大不动点的算法工作的前提都是 F 状态有限，下面我们从类型树的角度给出一个使得子类关系状态有限的论域。

称类型树 S 为类型树 T 的子类型，若存在 \pi \in \{L, R\}^* 使得 S : \sigma \mapsto T(\pi \sigma)。记 \text{subtrees}(T) 为 T 的所有子类型的集合。\ 称类型树 T 规范，若 \text{subtrees}(T) 为有限集。记 \mathcal{T}_r 为所有规范树的集合。

例如：所有有限类型树都是规范的，T = \text{Top} \times (\text{Top} \times \cdots) 是规范的，T = A \times (B \times (A \times (B \times (B \times (A \times (B \times (B \times (B \times (B \times (A \times \cdots)))))))))) 不是规范的。

命题：规范树上的子类关系状态有限

限制 S_r = S|_{\mathcal{T}_r} 状态有限。

Proof. 只需证明对于 S, T \in \mathcal{T}_r 有 \text{reachable}_{S_r}(S, T) 状态有限，但注意到 \text{reachable}_{S_r}(S, T) \subset \text{subtrees}(S) \times \text{subtrees}(T)，而后两者都是有限集。明所欲证。

直观地想，规范树总是能由 \text{Top}, \to, \times 以及若干局部或全局的“重复结构”生成，我们考虑将其与先前归纳定义的 \mu-类型关联起来，即归纳定义 \text{treeof} : \mathcal{T}_m \to \mathcal{T}：

我们急需说明 \text{treeof} 是良定义的，这归于两点：

• (i) 对任意给定的 T, \pi，\text{treeof}(T)(\pi) 递归终止：\pi 这边倒好说，无非是 L \pi, R \pi \mapsto \pi 时长度减小 1；那 T 的变式怎么找？
• (ii) 对于 \mu X.T \in \mathcal{T}_m，有 [X \mapsto \mu X.T] T \in \mathcal{T}_m：这无非是说后者仍为闭式——这是显然的；且仍收缩——对生成 T 的过程归纳即可。

对于 (i) 中提出的 T 的变式问题，留意到当 T 不收缩时递归不会终止：如 \mu X.X 经过一次替换后仍为 [X \mapsto \mu X.X] X = \mu X.X；而随意举一个 T 收缩的例子：如 \mu X. \text{Unit} + X 经过一次替换后为 [X \mapsto \mu X. \text{Unit} + X] (\text{Unit} + X) = \text{Unit} + \mu X. (\text{Unit} + X)，无论向左还是向右递归，\pi 都会减小。

由此想到我们期待 \mu X.T 替换后得到的新类型的根部不是另一个 \mu，这样就能确保 \pi 减小了；但有反例：如 \mu X. \mu Y. X + Y 经过一次替换后为 [X \mapsto \mu X. \mu Y. X + Y] X = \mu Y. ((\mu X. \mu Y. X + Y) + Y)，再经过一次替换后为 [Y \mapsto \mu Y. ((\mu X. \mu Y. X + Y) + Y)] X = (\mu X. \mu Y. X + Y) + \mu Y. ((\mu X. \mu Y. X + Y) + Y)，这样的话无论向左还是向右递归，\pi 也都会减小。

稍加一般化，定义一个 \mu-类型的 \mu-高度 (\mu-height) 为其最外面包着的 \mu 数量：

引理：\mu-高度构成 \mu-类型在 unfold 下的变式

设 \mu X.T \in \mathcal{T}_m，则 \mu\text{-height}([X \mapsto \mu X.T] T) < \mu\text{-height}(\mu X.T)。

Proof. 设 \mu X.T = \mu X. \mu X_1. \cdots \mu X_n. S，其中 S 不由 \mu 所构造，则 \mu\text{-height}(\mu X.T) = n + 1。\ 由收缩性可知 S \neq X，故 [X \mapsto S] 不由 \mu 所构造，则 \mu\text{-height}([X \mapsto \mu X.T] T) = \mu\text{-height}(\mu X_1. \cdots \mu X_n. [X \mapsto \mu X.T] S) = n。明所欲证。

总之 (|\pi|, \mu\text{-height}(T)) 的字典序构成递归过程的变式。由此 \text{treeof} 确是良定义的。

• 方便起见，下面记 \text{treeof}(S, T) = (\text{treeof}(S), \text{treeof}(T))。

现在将 \text{HS-Top}, \text{HS-Arrow}, \text{HS-Prod}, \text{HS-Mu-Right}, \text{HS-Mu-Left} 五条规则，仿照上面对 S, S_f 的讨论，搬到 \mathcal{T}_m 中构成单调函数 S_m：

……其中最后要求先展开第二个参数、再展开第一个参数是为了确保 S_m 可逆。此时有支撑集：

其余情况下未定义。接下来我们只需证明规范树与 \mu-类型及二者之上的子类关系确实是相对应的。

引理

设 R \subset \mathcal{T}_m \times \mathcal{T}_m 是 S_m-保持的，则任给 (S, T) \in R，有 (S', T') \in R 使得 \text{treeof}(S', T') = \text{treeof}(S, T) 且 S', T' 都不以 \mu 开头。

Proof. 对 (\mu\text{-height}(T), \mu\text{-height}(S)) 按字典序归纳。\ (i) 当 \mu\text{-height}(T) = \mu\text{-height}(S) = 0，取 (S', T') = (S, T) 即可。\ (ii) 当 \mu\text{-height}(T) > 0，设 T = \mu X. T_1，由 R 是 S_m-保持的可知 (S, T') \triangleq (S, [X \mapsto \mu X. T_1] T_1) \in R，再由前一引理可知 \mu\text{-height}(T') = \mu\text{-height}(T) - 1。\ 由 \text{treeof} 的定义可知 \text{treeof}(S, T') = \text{treeof}(S, T)，而由归纳假设可知有 (S'', T'') \in R 使得 \text{treeof}(S'', T'') = \text{treeof}(S, T') 且 S'', T'' 都不以 \mu 开头。则 (S'', T'') \in R 也证得了 (S, T) 的命题。\ (iii) 当 \mu\text{-height}(T) = 0, \mu\text{-height}(S) > 0，同 (2) 理可证。

定理：规范树与 \mu-类型上的子类关系一致

设 (T_1, T_2) \in \mathcal{T}_m \times \mathcal{T}_m，则 (T_1, T_2) \in \nu S_m 当且仅当 \text{treeof}(T_1, T_2) \in \nu S。

Proof. (i) 必要性：由余归纳原理可知只需给出 S-保持的集合 Q \subset \mathcal{T} \times \mathcal{T}，使得 \text{treeof}(T_1, T_2) \in Q。我们断言 Q = \text{treeof}(\nu S_m) 满足条件。\

> I. 若 $T'_2 = \text{Top}$，则 $(A, B) \in S(Q)$。\ > II. 若 $(T'_1, T'_2) = (U_1 \to U_2, V_1 \to V_2)$，则 $A = A_1 \to A_2, B = B_1 \to B_2$，其中 $A_i = \text{treeof}(U_i), B_i = \text{treeof}(V_i)$ 且 $(V_1, U_1), (U_2, V_2) \in \nu S_m$，则 $(B_1, A_1), (A_2, B_2) \in Q$，进而得到 $(A, B) \in S(Q)$。\ > III. 若 $(T'_1, T'_2) = (U_1 \times U_2, V_1 \times V_2)$，同 II 理可证。 (ii) 充分性：由余归纳原理可知只需给出 $S_m$-保持的集合 $R \subset \mathcal{T}_m \times \mathcal{T}_m$，使得 $(T_1, T_2) \in R$。我们断言 $R = \{(T_1, T_2) \in \mathcal{T}_m \times \mathcal{T}_m \mid \text{treeof}(T_1, T_2) \in \nu S\}$ 满足条件。\ 后面的证明无非是与上面相似的分类讨论，略。

\mu-类型的子类型判断

实例化 \text{gfp}^t_{\text{support}_{S_m}} 得到下面的算法：

为证明其终止性，我们只需证明 \forall (S, T) \in \mathcal{T}_m \times \mathcal{T}_m, \text{reachable}_{S_m}(S, T) 为有限集。

称 \mu-类型 S 为 T 的一个 自顶向下子表达式 (top-down subexpression)，若 (S, T) \in \mu \text{TD}，记作 S \sqsubseteq T。\ 其中 \mathcal{T}_m \times \mathcal{T}_m 上的单调函数 \text{TD} 的定义如下：

引理：\sqsubseteq 与支撑集的关系

若 (S', T') \in \text{support}_{S_m}(S, T)，则 S' \sqsubseteq S \lor T' \sqsubseteq S 且 S' \sqsubseteq T \lor T' \sqsubseteq T。

Proof. 由 \text{support}_{S_m} 的定义立即可得。

引理：\sqsubseteq 的传递性

若 S \sqsubseteq U, U \sqsubseteq T，则 S \sqsubseteq T。

Proof. 对 U \sqsubseteq T 的推导过程归纳即可。

命题：\sqsubseteq 与可达集的关系

若 (S', T') \in \text{reachable}_{S_m}(S, T)，则 S' \sqsubseteq S \lor T' \sqsubseteq S 且 S' \sqsubseteq T \lor T' \sqsubseteq T。

Proof. 对 \text{reachable}_{S_m} 的定义归纳，再由上面两个引理即得。

因此只需证明任一 \mu-类型的自顶向下子表达式数量有限，但由于 [X \mapsto \mu X.T] T 既不是结构递归、又不会减小深度等，直接归纳似乎较为困难。

上面的思路可以总结为：先将 \mu X.T 替换为 [X \mapsto \mu X.T] T、再找子类 S；下面考虑另一种思路：先对 非闭合式 T 找子类 S、再套上 \mu 的皮。

称 \mu-类型 S 为 T 的一个 自底向上子表达式 (bottom-up subexpression)，若 (S, T) \in \mu \text{BU}，记作 S \preceq T。\ 其中 \mathcal{T}_m \times \mathcal{T}_m 上的单调函数 \text{BU} 的定义如下：

引理：自底向上子表达式有限

Proof. 对 T 归纳即得。

为证明自底向上表达式包含于自顶向下表达式，为处理与 \mu 相关的形式，给出下面的引理。

Rmk. 下面默认使用 Barendregt 约定：同一上下文中绑定变量与自由变量的名称不会冲突。

引理：若 S \preceq [X \mapsto Q] T，则要么 S \preceq Q，要么存在 S' 使得 S = [X \mapsto Q] S' 且 S' \preceq T。\ Proof. 考虑对 T 归纳。\ (i) 若 T = \text{Top}，有 S \preceq \text{Top}，推知 S = \text{Top}。故取后者并令 S' = \text{Top} 即可。\ (ii) 若 T = X，有 S \preceq Q，此即前者。\ (iii) 若 T = Y \ (Y \neq X)，有 S \preceq Y，故取后者并令 S' = Y 即可。\ (iv) 若 T = T_1 \to T_2，有 S \preceq [X \mapsto Q] T_1 \to [X \mapsto Q] T_2，对 S 分类讨论：

I. 当 S = [X \mapsto Q] T，取后者并令 S' = T 即可。\ II. 当 S \preceq [X \mapsto Q] T_1，由归纳假设可知：要么 S \preceq Q，此即前者；要么存在 S' 使得 S = [X \mapsto Q] S' 且 S' \preceq T_1，由 BU 的定义即得 S' \preceq T。\ III. 当 S \preceq [X \mapsto Q] T_2，同 II 理可证。

(v) 若 T = T_1 \times T_2，同 (iv) 理可证。\ (vi) 若 T = \mu Y. T_1，要么 S = [X \mapsto Q] T，取后者并令 S' = T 即可。\ 要么存在 S_1 使得 S = [Y \mapsto \mu Y. T_1] S_1 且 S_1 \preceq [X \mapsto Q] T_1，对归纳假设的结果分类讨论：

I. 若 S_1 \preceq Q，据 Y \not\in \text{FV}(Q) 可知 Y \not\in \text{FV}(S_1)，则 S = S_1，故前者成立。 \ II. 若存在 S' 使得 S_1 = [X \mapsto Q] S' 且 S' \preceq T_1，则 S = [Y \mapsto \mu Y. T_1] ([X \mapsto Q] S') = [X \mapsto Q] ([Y \mapsto \mu Y. T_1] S') 且 [Y \mapsto \mu Y. T_1] S'\preceq \mu Y. T_1，明所欲证。

命题：自底向上子表达式包含于自顶向下子表达式中

若 S \sqsubseteq T，则 S \preceq T。

Proof. 只需证明 \mu \text{TD} \subset \mu \text{BU}，由归纳原理可知只需证明 \text{TD}(\mu \text{BU}) \subset \mu \text{BU}，这无非是说 \forall (A, B) \in \mu \text{BU}，\text{TD}(\{A, B\}) 中的项都能通过 \text{BU} 的规则消除。\ 显然只需考虑第六条：设 (S, [X \mapsto \mu X.T] T) \in \mu \text{BU}, (S, \mu X.T) \in \text{TD}(\mu \text{BU})。\ 由引理可知：要么 S \preceq \mu X.T，也即 (S, \mu X.T) \in \mu \text{BU}；要么存在 S' 使得 S = [X \mapsto \mu X.T] S' 且 S' \preceq T，则 (S, \mu X.T) = ([X \mapsto \mu X.T] S', \mu X.T) \in \mu \text{BU}。明所欲证。

命题：可达集有限

设 S, T \in \mathcal{T}_m，则 \text{reachable}_{S_m}(S, T) 为有限集。

Proof. 记 \text{TDS}, \text{BUS} 分别为 S, T 的自顶向下子表达式和自底向上表达式的集合，则 \text{reachable}_{S_m}(S, T) \subset \text{TDS} \times \text{TDS}、\text{BUS} 为有限集且 \text{TDS} \subset \text{BUS}，总之可见 \text{reachable}_{S_m}(S, T) 为有限集。

设 S, T 的表达式树大小是 O(n) 的，则可见上述算法的时间复杂度为 \tilde{O}(n^2)。

对比一下我们一开始从直觉上给出的假设子类推导对应的算法 \text{subtype}^{\text{ac}} : \mathcal{P}(\mathcal{T}_m \times \mathcal{T}_m) \times \mathcal{T}_m \times \mathcal{T}_m \to \textbf{bool}：

一方面可以发现参数 A 并非按照调用的时间顺序逐渐扩张，另一方面上述算法也有显然的时间复杂度上界为 \tilde{O}(2^n)。事实上的确可以卡满这个上界：

• 归纳定义 S_n, T_n 如下：

• 现对 n > 0 检查 S_n <: T_n：

• 其中：

• 可见上面两处下划线的调用过程分别跟 \text{subtype}^{\text{ac}}(\varnothing, S_{n - 1}, T_{n - 1}), \text{subtype}^{\text{ac}}(\varnothing, T_{n - 1}, S_{n - 1}) 无异：因为 A_3, A_6 并无 S_{n - 1}, T_{n - 1} 子结构的信息。
• 由此，一次 n 的调用触发两次 n - 1 的调用，归纳即得这一调用的时间复杂度是 \tilde{O}(2^n) 的。明所欲证。

最后补充一下 同构递归 设定下，\mu-类型的子类型的假设子类推导：

照此实现的算法的终止性与时间复杂度是显然的。

Reference

指我抄的 slides 和教材（

• 北京大学 2026 年春《编程语言的设计原理》中 Recursive Types 一讲的 slides。
• Types and Programming Languages, Chapter 21 Metatheory of Recursive Types。