OSFVA
所有文章 标签
OSFVA

目录

Types and Programming Languages习题的参考解答及思考（第16章）

CloseToZero
   约 17683 字   预计阅读 36 分钟 

第16章

章节16.1

练习16.1.2

题目：

LEMMA:

  1. \( \text{S} <: \text{S} \) can be derived for every type \( \text{S} \) without using S-REFL.
  2. If \( \text{S} <: \text{T} \) is derivable, then it can be derived without using S-TRANS.

证明：

证明1：

归纳假设命题对\( \text{S} \)的直接子类型都成立，我们要证明命题对\( \text{S} \)成立，对\( \text{S} \)的形式进行分类讨论：

  1. 如果\( \text{S} = \text{Top} \)，则使用S-TOP就可以直接得到\( \text{S} <: \text{S} \)，不需要使用S-REFL。
  2. 如果\( \text{S} = \text{S}_1 \to \text{S}_2 \)，则由归纳假设可得，\( \text{S}_1 <: \text{S}_1, \text{S}_2 <: \text{S}_2 \)，且两者的推导均不需要用到S-REFL，再由S-ARROW，可得\( \text{S} <: \text{S} \)且推导不需要用到S-REFL。
  3. 如果\( \text{S} = \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \)，则由归纳假设，可得\( \forall 1 \leq i \leq n, \text{T}_i <: \text{T}_i \)，且它们的推导均不需要用到S-REFL，再由S-RCD，可得\( \text{S} <: \text{S} \)且推导不需要用到S-REFL。

综上，归纳完毕，命题成立。

证明1完毕。

证明2：

在证明之前，我们需要注意，S-REFL是之后会删除的规则，因此我们在证明中应该确保不使用规则S-REFL，由1，可得假设规则S-REFL已经被删除是安全的，故我们这里假设规则S-REFL已经被删除，特别的，这意味着推导中使用的规则均不包含S-REFL。

令\( \mathcal{C} \)为\( \text{S} <: \text{T} \)对应的子类型推导，令\( d \)为\( \mathcal{C} \)的深度，归纳假设命题对任意深度\( d' < d \)的子类型推导都成立，我们要证明命题对\( \mathcal{C} \)成立，对\( \mathcal{C} \)最后使用的子类型规则进行分情况讨论：

  1. 如果最后使用的规则是S-TOP，则\( \text{T} = \text{Top} \)，这种情况下，直接使用S-TOP，不需要使用其他任何规则，便可得到\( \text{S} <: \text{T} \)，特别的，不需要用到S-TRANS。
  2. 如果最后使用的规则是S-ARROW，则\( \text{S} = \text{S}_1 \to \text{S}_2, \text{T} = \text{T}_1 \to \text{T}_2, \text{T}_1 <: \text{S}_1, \text{S}_2 <: \text{T}_2 \)，根据\( \text{T}_1 <: \text{S}_1, \text{S}_2 <: \text{T}_2 \)以及归纳假设，可得\( \text{T}_1 <: \text{S}_1, \text{S}_2 <: \text{T}_2 \)均是可推导的且推导不需要用到S-TRANS，进而由S-ARROW，可得\( \text{S} <: \text{T} \)是可推导的且推导不需要用到S-TRANS。
  3. 如果最后使用的规则是S-RCD，则\( \text{S} = \{ \text{k}_j: \text{S}_j \ ^{j \in 1 \dots m} \}, \text{T} = \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \}, \{ \text{l}_i \ ^{i \in 1 \dots n} \} \subseteq \{ \text{k}_j \ ^{j \in 1 \dots m} \}, \forall \text{k}_j = \text{l}_i, \text{S}_j <: \text{T}_i \)，根据\( \forall \text{k}_j = \text{l}_i, \text{S}_j <: \text{T}_i \)以及归纳假设，可得\( \forall \text{k}_j = \text{l}_i, \text{S}_j <: \text{T}_i \)均是可推导的且推导不需要用到S-TRANS，进而由S-RCD，可得\( \text{S} <: \text{T} \)是可推导的且推导不需要用到S-TRANS。
  4. 如果最后使用的规则是S-TRANS，则\( \text{S} <: \text{U}, \text{U} <: \text{T} \)，此时情况复杂点，由\( \text{S} <: \text{U}, \text{U} <: \text{T} \)以及归纳假设，可得\( \text{S} <: \text{U}, \text{U} <: \text{T} \)均是可推导的且推导不需要用到S-TRANS，令\( \mathcal{C}_1, \mathcal{C}_2 \)分别为\( \text{S} <: \text{U}, \text{U} <: \text{T} \)对应的不需要用到S-TRANS的子类型推导，我们对\( \mathcal{C}_1 \)最后使用的规则进行分情况讨论：
    1. 如果\( \mathcal{C}_1 \)最后使用的规则为S-TOP，则\( \text{U} = \text{Top} \)，而\( \text{U} <: \text{T} \)，\( \mathcal{C}_2 \)最后使用的规则可能是S-TOP、S-ARROW、S-RCD，后两者不适用于\( \text{U} = \text{Top} \)的情况，可得此时\( \mathcal{C}_2 \)最后使用的规则只能是S-TOP，于是有\( \text{T} = \text{Top} \)，进而可得使用S-TOP即可得到\( \text{S} <: \text{T} \)，不需要使用其他任何规则，特别的，不需要用到S-TRANS。
    2. 如果\( \mathcal{C}_1 \)最后使用的规则为S-ARROW，则\( \text{S} = \text{S}_1 \to \text{S}_2, \text{U} = \text{U}_1 \to \text{U}_2, \text{U}_1 <: \text{S}_1, \text{S}_2 <: \text{U}_2 \)，而\( \text{U} <: \text{T} \)，\( \mathcal{C}_2 \)最后使用的规则可能是S-TOP、S-ARROW、S-RCD， S-RCD不适用于\( \text{U} = \text{U}_1 \to \text{U}_2 \)的情况，可得\( \mathcal{C}_2 \)最后使用的规则只能是S-TOP、S-ARROW，分情况讨论：
      1. 如果\( \mathcal{C}_2 \)最后使用的规则是S-TOP，则\( \text{T} = \text{Top} \)，可得使用S-TOP即可得到\( \text{S} <: \text{T} \)，不需要使用其他任何规则，特别的，不需要用到S-TRANS。
      2. 如果\( \mathcal{C}_2 \)最后使用的规则是S-ARROW，则\( \text{T} = \text{T}_1 \to \text{T}_2, \text{T}_1 <: \text{U}_1, \text{U}_2 <: \text{T}_2 \)。令\( \mathcal{C}_{11} \)为\( \text{U}_1 <: \text{S}_1 \)对应的子类型推导，有\( d(\mathcal{C}_{11}) = d(\mathcal{C}_1) - 1 \)，令\( \mathcal{C}_{12} \)为\( \text{S}_2 <: \text{U}_2 \)对应的子类型推导，有\( d(\mathcal{C}_{12}) = d(\mathcal{C}_1) - 1 \)。同理，令\( \mathcal{C}_{21} \)为\( \text{T}_1 <: \text{U}_1 \)对应的子类型推导，有\( d(\mathcal{C}_{21}) = d(\mathcal{C}_2) - 1 \)，令\( \mathcal{C}_{22} \)为\( \text{U}_2 <: \text{T}_2 \)对应的子类型推导，有\( d(\mathcal{C}_{22}) = d(\mathcal{C}_2) - 1 \)。在\( \mathcal{C}_{21}, \mathcal{C}_{11} \)的基础上使用S-TRANS，可得到推导\( \mathcal{C}_{111} \)，它的结论是\( \text{T}_1 <: \text{S}_1 \)，除此之外，还有\( d(\mathcal{C}_{111}) = \max(d(\mathcal{C}_{21}), d(\mathcal{C}_{11})) + 1 \)，而\( d(\mathcal{C}_{21}) = d(\mathcal{C}_2) - 1 < d(\mathcal{C}) - 1, d(\mathcal{C}_{11}) = d(\mathcal{C}_1) - 1 < d(\mathcal{C}) - 1 \)，可得\( \max(d(\mathcal{C}_{21}), d(\mathcal{C}_{11})) < d(\mathcal{C}) - 1 \)，进而可得\( d(\mathcal{C}_{111}) = \max(d(\mathcal{C}_{21}), d(\mathcal{C}_{11})) + 1 < d(\mathcal{C}) \)，可以使用归纳假设，根据归纳假设，可得\( \text{T}_1 <: \text{S}_1 \)是可推导的且推导不需要用到S-TRANS，令\( \mathcal{C}_{112} \)为该不需要S-TRANS的推导。在\( \mathcal{C}_{12}, \mathcal{C}_{22} \)的基础上使用S-TRANS，可得到推导\( \mathcal{C}_{211} \)，它的结论是\( \text{S}_2 <: \text{T}_2 \)，同理，可得\( \text{S}_2 <: \text{T}_2 \)是可推导的且推导不需要用到S-TRANS，令\( \mathcal{C}_{212} \)为该不需要S-TRANS的推导。最终在\( \mathcal{C}_{112}, \mathcal{C}_{212} \)的基础上使用S-ARROW，可得\( \text{S} <: \text{T} \)是可推导的且推导不需要用到S-TRANS。
    3. 如果\( \mathcal{C}_1 \)最后使用的规则为S-RCD，则\( \text{S} = \{ \text{k}_j: \text{S}_j \ ^{j \in 1 \dots m} \}, \text{U} = \{ \text{u}_a: \text{U}_a \ ^{a \in 1 \dots b} \}, \{ \text{u}_a \ ^{a \in 1 \dots b} \} \subseteq \{ \text{k}_j \ ^{j \in 1 \dots m} \}, \forall \text{k}_j = \text{u}_a, \text{S}_j <: \text{U}_a \)，而\( \text{U} <: \text{T} \)，\( \mathcal{C}_2 \)最后使用的规则可能是S-TOP、S-ARROW、S-RCD， S-ARROW不适用于\( \text{U} = \{ \text{u}_a: \text{U}_a \ ^{a \in 1 \dots b} \} \)的情况，可得\( \mathcal{C}_2 \)最后使用的规则只能是S-TOP、S-RCD，分情况讨论：
      1. 如果\( \mathcal{C}_2 \)最后使用的规则是S-TOP，则\( \text{T} = \text{Top} \)，可得使用S-TOP即可得到\( \text{S} <: \text{T} \)，不需要使用其他任何规则，特别的，不需要用到S-TRANS。
      2. 如果\( \mathcal{C}_2 \)最后使用的规则是S-RCD，则\( \text{T} = \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \}, \{ \text{l}_i \ ^{i \in 1 \dots n} \} \subseteq \{ \text{u}_a \ ^{a \in 1 \dots b} \}, \forall \text{u}_a = \text{l}_i, \text{U}_a <: \text{T}_i \)。 \( \forall \text{k}_j = \text{u}_a \), 令\( \mathcal{C}_{1ja} \)为\( \text{S}_j <: \text{U}_a \)对应的子类型推导，有\( d(\mathcal{C}_{1ja}) = d(\mathcal{C}_1) - 1 \)。同理，\( \forall \text{u}_a = \text{l}_i \)，令\( \mathcal{C}_{2ai} \)为\( \text{U}_a <: \text{T}_i \)对应的子类型推导，有\( d(\mathcal{C}_{2ai}) = d(\mathcal{C}_2) - 1 \)。 \( \forall 1 \leq i \leq n, \exists 1 \leq a \leq b, 1 \leq j \leq m \)满足\( \text{l}_i = \text{u}_a = \text{k}_j, \text{S}_j <: \text{U}_a, \text{U}_a <: \text{T}_i \)，在\( \mathcal{C}_{1ja}, \mathcal{C}_{2ai} \)的基础上使用S-TRANS，可得到推导\( \mathcal{C}_{ji} \)，它的结论是\( \text{S}_j <: \text{T}_i \)，除此之外，还有\( d(\mathcal{C}_{ji}) = \max(d(\mathcal{C}_{1ja}), d(\mathcal{C}_{2ai})) + 1 \)，而\( d(\mathcal{C}_{1ja}) = d(\mathcal{C}_1) - 1 < d(\mathcal{C}) - 1, d(\mathcal{C}_{2ai}) = d(\mathcal{C}_2) - 1 < d(\mathcal{C}) - 1 \)，可得\( \max(d(\mathcal{C}_{1ja}), d(\mathcal{C}_{2ai})) < d(\mathcal{C}) - 1 \)，进而可得\( d(\mathcal{C}_{ji}) = \max(d(\mathcal{C}_{1ja}), d(\mathcal{C}_{2ai})) + 1 < d(\mathcal{C}) \)，可以使用归纳假设，根据归纳假设，可得\( \text{S}_j <: \text{T}_i \)是可推导的且推导不需要用到S-TRANS，令\( \mathcal{C}'_{ji} \)为该不需要S-TRANS的推导。综上，\( \forall 1 \leq i \leq n, \exists 1 \leq j \leq m \)满足\( \text{l}_i = \text{k}_j \)，以及\( \exists \)推导\( \mathcal{C}'_{ji} \)，它的结论是\( \text{S}_j <: \text{T}_i \)且该推导不需要用到S-TRANS，在这些\( \mathcal{C}'_{ji} \)推导以及易得的\( \{ \text{l}_i \ ^{i \in 1 \dots n} \} \subseteq \{ \text{k}_j \ ^{j \in 1 \dots m} \} \)的基础上使用S-RCD，可得\( \text{S} <: \text{T} \)是可推导的且推导不需要用到S-TRANS。

综上，归纳完毕，命题成立。

证明2完毕。

练习16.1.3

题目：

If we add the type \( \text{Bool} \), how do these properties change?

解答：

首先，S-REFL，不再是非必要的了，观察对引理16.1.2的1的证明，可以看到在\( \text{S} \)为函数类型、record类型时的证明都依赖于归纳假设，基础情况只有\( \text{S} = \text{Top} \)，此时用的规则是S-TOP，故引理16.1.2的1的成立十分依赖于基础类型只有\( \text{Top} \)的这一点，如果加上\( \text{Bool} \)，则引理16.1.2的1不再成立。解决方法有两种：

  1. 修改引理16.1.2的陈述，改成： “\( \text{S} <: \text{S} \) can be derived for every type \( \text{S} \) without using S-REFL except the type \( \text{Bool} \)"。
  2. 添加额外的规则\( \text{Bool} <: \text{Bool} \)。

引理16.1.2的2则仍然成立，证明也是差不多的，得修改下证明，修改量取决于你采取了上面1、2中的哪一种解决方法，选择第2种解决方案修改量是比较小的。

章节16.2

练习16.2.1

题目：

To finish the experiment, show how to perform similar rearrangements on derivations in which T-SUB is used before T-RCD or T-PROJ.

解答：

T-SUB在T-RCD之前：

T-RCD规则如下：

\[ \dfrac{\forall 1 \leq i \leq n, \Gamma \vdash \text{t}_i : \text{T}_i}{ \Gamma \vdash \{ \text{l}_i: \text{t}_i \ ^{i \in 1 \dots n} \}: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \}} \qquad (\text{T-RCD}) \]

给定最后使用的规则为T-RCD的推导\( \mathcal{D} \)，如果\( \exists \)唯一的\( j \)满足\( 1 \leq j \leq n, \Gamma \vdash \text{t}_j: \text{T}_j \)且最后使用的规则为T-SUB，则\( \mathcal{D} \)如下：

\[ \dfrac{\dfrac{\vdots}{\Gamma \vdash \text{t}_1 : \text{T}_1} \quad \dfrac{\vdots}{\Gamma \vdash \text{t}_2 : \text{T}_2} \quad \dots \quad \dfrac{\dfrac{\vdots}{\Gamma \vdash \text{t}_j : \text{S}_j} \quad \dfrac{\vdots}{\text{S}_j <: \text{T}_j}}{ \Gamma \vdash \text{t}_j : \text{T}_j}(\text{T-SUB}) \quad \dots \quad \dfrac{\vdots}{\Gamma \vdash \text{t}_n : \text{T}_n} \quad}{ \Gamma \vdash \{ \text{l}_i: \text{t}_i \ ^{i \in 1 \dots n} \}: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \}}(\text{T-RCD}) \]

我们可以把\( \mathcal{D} \)调整成如下：

\[ \dfrac{\dfrac{\dfrac{\vdots}{\Gamma \vdash \text{t}_1 : \text{T}_1} \quad \dfrac{\vdots}{\Gamma \vdash \text{t}_2 : \text{T}_2} \quad \dots \quad \dfrac{\vdots}{\Gamma \vdash \text{t}_j : \text{S}_j} \quad \dots \quad \dfrac{\vdots}{\Gamma \vdash \text{t}_n : \text{T}_n}}{ \Gamma \vdash \{ \text{l}_i: \text{t}_i \ ^{i \in 1 \dots n} \}: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots j - 1} \quad \text{l}_j: \text{S}_j \quad \text{l}_k: \text{T}_k \ ^{k \in j + 1 \dots n} \}}(\text{T-RCD}) \quad \dfrac{\dfrac{}{\text{T}_1 <: \text{T}_1}(\text{S-REFL}) \quad \dfrac{}{\text{T}_2 <: \text{T}_2}(\text{S-REFL}) \quad \dfrac{\vdots}{\text{S}_j <: \text{T}_j} \quad \dfrac{}{\text{T}_n <: \text{T}_n}(\text{S-REFL})}{ \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots j - 1} \quad \text{l}_j: \text{S}_j \quad \text{l}_k: \text{T}_k \ ^{k \in j + 1 \dots n} \} <: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \}}(\text{S-RCDDEPTH})}{ \Gamma \vdash \{ \text{l}_i: \text{t}_i \ ^{i \in 1 \dots n} \}: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \}}(\text{T-SUB}) \]

如果\( \mathcal{D} \)有不止一个直接子推导最后使用的规则为T-SUB，则调整方式也类似上面，这里就不举例子了。

T-SUB在T-PROJ之前：

T-PROJ规则如下：

\[ \dfrac{\Gamma \vdash \text{t}_1: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \}}{ \Gamma \vdash \text{t}_1.\text{l}_j: \text{T}_j} \qquad (\text{T-PROJ}) \]

给定最后使用的规则为T-PROJ的推导\( \mathcal{D} \)，如果\( \mathcal{D} \)的直接子推导最后使用的规则为T-SUB，则\( \mathcal{D} \)如下：

\[ \dfrac{\dfrac{\dfrac{\vdots}{\Gamma \vdash \text{t}_1: \{ \text{k}_a: \text{S}_a \ ^{a \in 1 \dots b} \}} \quad \dfrac{\vdots}{\{ \text{k}_a: \text{S}_a \ ^{a \in 1 \dots b} \} <: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \}}}{ \Gamma \vdash \text{t}_1: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \}}(\text{T-SUB})}{ \Gamma \vdash \text{t}_1.\text{l}_j: \text{T}_j}(\text{T-PROJ}) \]

易得\( \{ \text{l}_i \ ^{i \in 1 \dots n} \} \subseteq \{ \text{k}_a \ ^{a \in 1 \dots b} \}, \forall \text{k}_a = \text{l}_i, \text{S}_a <: \text{T}_i \)，特别的，有\( \exists 1 \leq j_a \leq b, \text{k}_{j_a} = \text{l}_j \)，在下面我们会使用\( \text{j}_a \)而不再定义它。

我们可以把\( \mathcal{D} \)调整成如下：

\[ \dfrac{\dfrac{\dfrac{\vdots}{\Gamma \vdash \text{t}_1: \{ \text{k}_a: \text{S}_a \ ^{a \in 1 \dots b} \}}}{ \Gamma \vdash \text{t}_1.\text{l}_j: \text{S}_{j_a}}(\text{T-PROJ}) \quad \dfrac{\vdots}{\text{S}_{j_a} <: \text{T}_j}}{ \Gamma \vdash \text{t}_1.\text{l}_j: \text{T}_j}(\text{T-SUB}) \]

练习16.2.3

题目：

Show that the type assigned to a term by the algorithmic rules can decrease during evaluation by finding two terms \( \text{s} \) and \( \text{t} \) with algorithmic types \( \text{S} \) and \( \text{T} \) such that \( \text{s} \rightarrow^* \text{t} \) and \( \text{T} <: \text{S} \), but \( \text{S} \nless: \text{T} \).

解答：

\[ \begin{aligned} \text{s} &= (\lambda \text{x}: \text{Top. } \text{x}) \text{ } \{ \} \\ \text{t} &= \{ \} \\ \text{S} &= \text{Top} \\ \text{T} &= \{ \} \end{aligned} \]

注意，类型可能在求值过程中变得更精确（更“小”）不是算法性规则的特性，在之前普通的规则下也可以达到同样的效果。

练习16.2.5

题目：

Theorem [Completeness, or Minimal Typing]: If \( \Gamma \vdash \text{t}: \text{T} \), then \( \Gamma \mapsto \text{t}: \text{S} \) for some \( \text{S} <: \text{T} \).

证明：

令\( \mathcal{D} \)为\( \Gamma \vdash \text{t}: \text{T} \)对应的类型推导，归纳假设命题对\( \mathcal{D} \)的直接子推导成立，我们要证明命题对\( \mathcal{D} \)成立，对\( \mathcal{D} \)最后使用的规则进行分情况讨论：

  1. 如果最后使用的规则是T-VAR，则\( \text{t} = \text{x}, \text{x}: \text{T} \in \Gamma \)，此时令\( \text{S} = \text{T} \)，有\( \text{S} <: \text{T} \)，根据TA-VAR，可得\( \Gamma \mapsto \text{t}: \text{S} \)。
  2. 如果最后使用的规则是T-ABS，则\( \text{t} = \lambda \text{x}: \text{T}_1 \text{. } \text{t}_2, \Gamma, \text{x}: \text{T}_1 \vdash \text{t}_2: \text{T}_2, \text{T} = \text{T}_1 \to \text{T}_2 \)，由\( \Gamma, \text{x}: \text{T}_1 \vdash \text{t}_2: \text{T}_2 \)以及归纳假设，可得\( \Gamma, \text{x}: \text{T}_1 \mapsto \text{t}_2: \text{S}_2, \text{S}_2 <: \text{T}_2 \)，令\( \text{S} = \text{T}_1 \to \text{S}_2 \)，则根据TA-ABS，可得\( \Gamma \mapsto \text{t}: \text{S} \)，由\( \text{T}_1 <: \text{T}_1, \text{S}_2 <: \text{T}_2 \)以及S-ARROW，可得\( \text{S} <: \text{T} \)。
  3. 如果最后使用的规则是T-APP，则\( \text{t} = \text{t}_1 \text{ } \text{t}_2, \Gamma \vdash \text{t}_1: \text{T}_2 \to \text{T}, \Gamma \vdash \text{t}_2: \text{T}_2 \)，由\( \Gamma \vdash \text{t}_1: \text{T}_2 \to \text{T}, \Gamma \vdash \text{t}_2: \text{T}_2 \)以及归纳假设，可得\( \Gamma \mapsto \text{t}_1: \text{S}_1, \text{S}_1 <: \text{T}_2 \to \text{T} \)，以及\( \Gamma \mapsto \text{t}_2: \text{S}_2, \text{S}_2 <: \text{T}_2 \)，由\( \text{S}_1 <: \text{T}_2 \to \text{T} \)以及引理15.3.2的1，可得\( \text{S}_1 = \text{S}_{11} \to \text{S}, \text{T}_2 <: \text{S}_{11}, \text{S} <: \text{T} \)，由\( \text{S}_2 <: \text{T}_2, \text{T}_2 <: \text{S}_{11} \)以及S-TRANS，可得\( \text{S}_2 <: \text{S}_{11} \)，再由定理16.1.5，可得\( \mapsto \text{S}_2 <: \text{S}_{11} \)，进而由TA-APP，可得\( \Gamma \mapsto \text{t}: \text{S} \)，加上\( \text{S} <: \text{T} \)，可得\( \text{S} \)满足命题要求。
  4. 如果最后使用的规则是T-SUB，则\( \Gamma \vdash \text{t}: \text{S}_1, \text{S}_1 <: \text{T} \)，由\( \Gamma \vdash \text{t}: \text{S}_1 \)以及归纳假设，可得\( \Gamma \mapsto \text{t}: \text{S}, \text{S} <: \text{S}_1 \)，由\( \text{S} <: \text{S}_1, \text{S}_1 <: \text{T} \)以及S-TRANS，可得\( \text{S} <: \text{T} \)。
  5. 如果最后使用的规则是T-RCD，则\( \text{t} = \{ \text{l}_i = \text{t}_i \ ^{i \in 1 \dots n} \}, \forall 1 \leq i \leq n, \Gamma \vdash \text{t}_i: \text{T}_i, \text{T} = \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \)，由\( \forall 1 \leq i \leq n, \Gamma \vdash \text{t}_i: \text{T}_i \)以及归纳假设，可得\( \forall 1 \leq i \leq n, \Gamma \mapsto \text{t}_i: \text{S}_i, \text{S}_i <: \text{T}_i \)，令\( \text{S} = \{ \text{l}_i: \text{S}_i \ ^{i \in 1 \dots n} \} \)，则由TA-RCD，可得\( \Gamma \mapsto \text{t}: \text{S} \)，进而由S-RCDDEPTH，可得\( \text{S} <: \text{T} \)。
  6. 如果最后使用的规则是T-PROJ，则\( \text{t} = \text{t}_1.\text{l}_j, \Gamma \vdash \text{t}_1: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \}, \text{T} = \text{T}_j \)，由\( \Gamma \vdash \text{t}_1: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \)以及归纳假设，可得\( \Gamma \mapsto \text{t}_1: \text{S}_1, \text{S}_1 <: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \)，此时由引理15.3.2的2，可得\( \text{S}_1 = \{ \text{k}_a: \text{S}_a \ ^{a \in 1 \dots b} \}, \{ \text{l}_i \ ^{i \in 1 \dots n} \} \subseteq \{ \text{k}_a \ ^{a \in 1 \dots b} \}, \forall \text{l}_i = \text{k}_a, \text{S}_a <: \text{T}_i \)，除此之外，还有\( \exists 1 \leq j_a \leq b, \text{k}_{j_a} = \text{l}_j \)，于是由TA-PROJ，可得\( \Gamma \mapsto \text{t}: \text{S}_{j_a} \)，令\( \text{S} = \text{S}_{j_a} \)，有\( \text{S} <: \text{T}_j \)，即\( \text{S} <: \text{T} \)。

练习16.2.6

题目：

If we dropped the arrow subtyping rule S-ARROW but kept the rest of the declarative subtyping and typing rules the same, would the system still have the minimal typing property? If so, prove it. If not, give an example of a typable term with no minimal type.

解答：

丢弃S-ARROW规则后，最小类型属性不再成立，举个例子，令\( \text{t} = \lambda \text{x}: \{ \text{l}_1: \{ \} \} \text{. } \text{x} \)，则\( \text{t} \)同时具有类型\( \{ \text{l}_1: \{ \} \} \to \{ \text{l}_1: \{ \} \} \)以及\( \{ \text{l}_1: \{ \} \} \to \text{Top} \)，但是由于缺少S-ARROW规则，我们无法比较两个函数类型（谁是谁的子类型），特别的，不存在类型\( \text{S} \)满足\( \text{S} <: \{ \text{l}_1: \{ \} \} \to \{ \text{l}_1: \{ \} \}, \text{S} <: \{ \text{l}_1: \text{Top} \} \to \text{Top} \)，进而不存在\( \text{t} \)的最小类型（因为该最小类型得是\( \text{t} \)所有类型的子类型，特别的，它得是上述两个类型的子类型，但满足条件的类型不存在）。

章节16.3

练习16.3.2

题目：

Proposition [Existence of joins and bounded meets]:

  1. For every pair of types \( \text{S} \) and \( \text{T} \), there is some type \( \text{J} \) such that \( \text{S} \vee \text{T} = \text{J} \).
  2. For every pair of types \( \text{S} \) and \( \text{T} \) with a common subtype, there is some type \( \text{M} \) such that \( \text{S} \wedge \text{T} = \text{M} \).

证明：

再证明存在性之前，我们先考虑给定类型\( \text{S}, \text{T} \)，它们的join会是什么？

假设\( \text{S}, \text{T} \)均为函数类型，即\( \text{S} = \text{S}_1 \to \text{S}_2, \text{T} = \text{T}_1 \to \text{T}_2 \)，则既然\( \text{S} \vee \text{T} = \text{J} \)是两类型最精确的共同父类型， 那么直觉上，\( \text{J} \)得满足以下几点：

  1. \( \text{J} \)也是函数类型，即\( \text{J} = \text{J}_1 \to \text{J}_2 \)。
  2. 由于\( \text{J} \)是\( \text{S}, \text{T} \)最精确的共同父类型，因此\( \text{J} \)的返回值类型\( \text{J}_2 \)得是\( \text{S}_2, \text{T}_2 \)最精确的共同父类型，用join的话来说，就是\( \text{J}_2 = \text{S}_2 \vee \text{T}_2 \)。同理，参数类型\( \text{J}_1 \)得是\( \text{S}_1, \text{T}_1 \)最精确的共同子类型，此时得用meet表达，即\( \text{J}_1 = \text{S}_1 \wedge \text{T}_1 \)。由于\( \text{J}_1 \)是两者的meet，故我们改用符号\( \text{M}_1 \)，令\( \text{M}_1 = \text{J}_1 \)，则\( \text{J} = \text{M}_1 \to \text{J}_2 \)。

当然，命题中已经说了，\( \text{S}_1 \wedge \text{T}_1 \)不一定存在，即\( \text{S}_1 \wedge \text{T}_1 \)是个偏函数，我们得考虑\( \text{S}_1 \wedge \text{T}_1 \)未定义的情况， \( \text{S}_1 \wedge \text{T}_1 \)未定义时，我们缺少最精确的共同参数类型，此时\( \text{J} \)就肯定不能是函数类型了（函数类型需要参数类型），那么直觉上，唯一的可能就是fallback到\( \text{J} = \text{Top} \)了，毕竟record、Bool等八竿子打不着的类型是肯定不能选的。

类似的，考虑\( \text{S} \wedge \text{T} = \text{M} \)，它得是两类型的最精确的共同子类型，直觉上，\( \text{M} \)得满足以下几点（和上面是对称的）：

  1. \( \text{M} \)也是函数类型，即\( \text{M} = \text{J}_1 \to \text{M}_2 \)。
  2. 由于\( \text{M} \)是\( \text{S}, \text{T} \)最精确的共同子类型，因此\( \text{M} \)的返回值类型\( \text{M}_2 \)得是\( \text{S}_2, \text{T}_2 \)最精确的共同子类型，即\( \text{M}_2 = \text{S}_2 \wedge \text{T}_2 \)。同理，参数类型\( \text{J}_1 \)得是\( \text{S}_1, \text{T}_1 \)最精确的共同父类型，即\( \text{J}_1 = \text{S}_1 \vee \text{T}_1 \)。

同理，我们也得考虑\( \text{S}_2 \wedge \text{T}_2 \)未定义的情况，此时缺少最精确的共同返回值类型，由于\( \text{S} \wedge \text{T} \)允许未定义，故此时我们直接让\( \text{S} \wedge \text{T} \)未定义，用\( \text{S} \wedge \text{T} = \text{ud} \)表示。

接着， 我们考虑\( \text{S}, \text{T} \)均为record的情况，即\( \text{S} = \{ \text{k}_j: \text{S}_j \ ^{j \in 1 \dots m} \}, \text{T} = \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \)。先考虑join，令\( \text{J} = \text{S} \vee \text{T} \)，则直觉上，\( \text{J} \)得满足以下几点：

  1. \( \text{J} \)也是record，即\( \text{J} = \{ \text{u}_a: \text{U}_a \ ^{a \in 1 \dots b} \} \)。
  2. 由于\( \text{J} \)是\( \text{S}, \text{T} \)最精确的共同父类型，因此\( \text{J} \)得包含两者完整的共同标签（不能更少），即\( \{ \text{u}_a \ ^{a \in 1 \dots b} \} = \{ \text{k}_j \ ^{j \in 1 \dots m} \} \cap \{ \text{l}_i \ ^{i \in 1 \dots n} \} \)，除此之外，共同标签对应的类型也得是最精确的共同父类型，即\( \forall \text{u}_a = \text{k}_j = \text{l}_i, \text{U}_a = \text{S}_j \vee \text{T}_i \)。

由于没有用到meet操作，故不像函数类型，这里不用考虑未定义的情况。

再考虑meet，令\( \text{M} = \text{S} \wedge \text{T} \)，则直觉上，\( \text{M} \)得满足以下几点：

  1. \( \text{M} \)也是record，即\( \text{M} = \{ \text{m}_a: \text{M}_a \ ^{a \in 1 \dots b} \} \)。
  2. 由于\( \text{M} \)是\( \text{S}, \text{T} \)最精确的共同子类型，因此\( \text{M} \)得包含两者的全部标签，即\( \{ \text{m}_a \ ^{a \in 1 \dots b} \} = \{ \text{k}_j \ ^{j \in 1 \dots m} \} \cup \{ \text{l}_i \ ^{i \in 1 \dots n} \} \)，除此之外，共同标签对应的类型也得是最精确的共同子类型，即\( \forall \text{m}_a = \text{k}_j = \text{l}_i, \text{M}_a = \text{S}_j \wedge \text{T}_i \)，那等下，针对非共同标签呢？我们知道，这些非共同标签对应的类型不管取什么类型， \( \text{M} \)始终是\( \text{S}, \text{T} \)的共同子类型（因为record的子类型规则只考虑共同标签），关键我们得是最精确的，故我们直接取这些非共同标签在\( \text{S} \)或\( \text{T} \)中对应的类型，这是最精确的，即\( \forall \text{S} \)独有的标签\( \text{m}_a = \text{k}_j \)，令\( \text{M}_a = \text{S}_j \)， \( \forall \text{T} \)独有的标签\( \text{m}_a = \text{l}_i \)，令\( \text{M}_a = \text{T}_i \)。

同理，我们也得考虑\( \exists \text{k}_j = \text{l}_i, \text{S}_j \wedge \text{T}_i \)未定义的情况，此时缺少最精确的共同标签类型，故我们直接让\( \text{S} \wedge \text{T} \)未定义。

至于\( \text{S} = \text{T} = \text{Bool} \)这种两类型都是原子类型，即没有结构的类型的情况，则明显\( \text{S} \vee \text{T} = \text{Bool}, \text{S} \wedge \text{T} = \text{Bool} \)。

继续考虑\( \text{S}, \text{T} \)类型不同的情况，比如\( \text{S} = \text{S}_1 \to \text{S}_2, \text{T} = \text{Bool} \)，则明显的，两者唯一可能的最精确共同父类型就是\( \text{Top} \)，即\( \text{S} \vee \text{T} = \text{Top} \)，且由于两者没有共同子类型，进而没有最精确的共同子类型，即\( \text{S} \wedge \text{T} \)未定义，其他类型不同的情况同理。

最后考虑\( \text{S}, \text{T} \)其中一个为\( \text{Top} \)的情况，不妨设\( \text{T} = \text{Top} \)，则明显的\( \text{S} \vee \text{T} = \text{Top} \)，至于\( \text{S} \wedge \text{T} \)，两者最精确的共同子类型明显就是 可能 非\( \text{Top} \)的\( \text{S} \)了，即\( \text{S} \wedge \text{T} = \text{S} \)。

综上，\( \text{S} \vee \text{T}, \text{S} \wedge \text{T} \)函数的定义明显可以通过算法的方式表达，且两者会是相互递归的函数，这是因为函数类型的join会用到meet，meet则会用到join。

下面，我们给出\( \text{S} \vee \text{T}, \text{S} \wedge \text{T} \)的定义，之后再证明它们的正确性：

\[ \text{S} \vee \text{T} = \begin{cases} \text{Bool} &\text{如果} \text{S} = \text{T} = \text{Bool} \\ \text{M}_1 \to \text{J}_2 &\text{如果} \text{S} = \text{S}_1 \to \text{S}_2 \quad \text{T} = \text{T}_1 \to \text{T}_2 \\ &\hphantom{如果} \text{M}_1 = \text{S}_1 \wedge \text{T}_1 \text{且} \text{M}_1 \neq \text{ud} \\ &\hphantom{如果} \text{J}_2 = \text{S}_2 \vee \text{T}_2 \\ \{ \text{u}_a: \text{U}_a \ ^{a \in 1 \dots b} \} &\text{如果} \text{S} = \{ \text{k}_j: \text{S}_j \ ^{j \in 1 \dots m} \} \\ &\hphantom{如果} \text{T} = \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \\ &\hphantom{如果} \{ \text{u}_a \ ^{a \in 1 \dots b} \} = \{ \text{k}_j \ ^{j \in 1 \dots m} \} \cap \{ \text{l}_i \ ^{i \in 1 \dots n} \} \\ &\hphantom{如果} \forall \text{u}_a = \text{k}_j = \text{l}_i, \text{U}_a = \text{S}_j \vee \text{T}_i \\ \text{Top} &\text{不满足上述情况} \end{cases} \]

\[ \text{S} \wedge \text{T} = \begin{cases} \text{S} &\text{如果} \text{T} = \text{Top} \\ \text{T} &\text{如果} \text{S} = \text{Top} \\ \text{Bool} &\text{如果} \text{S} = \text{T} = \text{Bool} \\ \text{J}_1 \to \text{M}_2 &\text{如果} \text{S} = \text{S}_1 \to \text{S}_2 \quad \text{T} = \text{T}_1 \to \text{T}_2 \\ &\hphantom{如果} \text{J}_1 = \text{S}_1 \vee \text{T}_1 \\ &\hphantom{如果} \text{M}_2 = \text{S}_2 \wedge \text{T}_2 \text{且} \text{M}_2 \neq \text{ud} \\ \{ \text{m}_a: \text{M}_a \ ^{a \in 1 \dots b} \} &\text{如果} \text{S} = \{ \text{k}_j: \text{S}_j \ ^{j \in 1 \dots m} \} \\ &\hphantom{如果} \text{T} = \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \\ &\hphantom{如果} \{ \text{m}_a \ ^{a \in 1 \dots b} \} = \{ \text{k}_j \ ^{j \in 1 \dots m} \} \cup \{ \text{l}_i \ ^{i \in 1 \dots n} \} \\ &\hphantom{如果} \forall \text{m}_a = \text{k}_j = \text{l}_i, \text{M}_a = \text{S}_j \wedge \text{T}_i \text{且} \text{M}_a \neq \text{ud} \\ &\hphantom{如果} \forall \text{S} \text{独有的标签} \text{m}_a = \text{k}_j, \text{M}_a = \text{S}_j \\ &\hphantom{如果} \forall \text{T} \text{独有的标签} \text{m}_a = \text{l}_i, \text{M}_a = \text{T}_i \\ \text{ud} &\text{不满足上述情况} \end{cases} \]

接下来，我们打算去证明上述针对join、meet的算法性定义是正确的，即上述定义的计算结果确实是join、meet，需要注意的是，由于上述定义/算法是相互递归的，故我们在证明1、2时，得一起证明。

在证明1、2前，我们得先证明几个引理，首先是一个比较简单的引理。

引理1：

\( \forall \text{S}, \text{T}, \text{S} \vee \text{T} \)均是有定义的。

证明引理1：

由\( \text{S} \vee \text{T} \)的定义可以直接看出来。

证明引理1完毕。

还需要一个引理，确保如果\( \text{S}, \text{T} \)有共同子类型的情况下，上述meet算法给出的结果是有定义的，即\( \text{S} \wedge \text{T} \neq \text{ud} \)。

引理2：

如果\( \exists \text{L} \)满足\( \text{L} <: \text{S}, \text{L} <: \text{T} \)，则\( \text{S} \wedge \text{T} \neq \text{ud} \)。

证明引理2：

归纳假设命题对\( \text{S} \)的直接子类型成立，我们要证明命题对\( \text{S} \)成立：

如果\( \text{S}, \text{T} \)中有一个为\( \text{Top} \)，则\( \text{S} \wedge \text{T} = \text{Top} \neq \text{ud} \)。

如果\( \text{S}, \text{T} \)两者均不为\( \text{Top} \)，且\( \text{S}, \text{T} \)具有不同的形式（比如\( \text{S} \)为record，而\( \text{T} \)却为函数类型），则由\( \text{L} <: \text{S}, \text{L} <: \text{T} \)以及引理15.3.2（拓展到\( \text{Bool} \)的情况），可得\( \text{L} \)具有不同的形式，然而单个类型不可能具有两种形式（一个类型不能即是record又是函数类型），故\( \text{S}, \text{T} \)不可能具有不同的形式，因此接下来我们只要考虑\( \text{S}, \text{T} \)具有相同形式的情况即可，分情况讨论：

  1. 如果\( \text{S} = \text{T} = \text{Bool} \)，则\( \text{S} \wedge \text{T} = \text{Bool} \neq \text{ud} \)。

  2. 如果\( \text{S} = \text{S}_1 \to \text{S}_2, \text{T} = \text{T}_1 \to \text{T}_2 \)，则由引理1，可得\( \text{S}_1 \vee \text{T}_1 \)是有定义的，为了使用算法的情况4，我们还得证明\( \text{S}_2 \wedge \text{T}_2 \neq \text{ud} \)，由\( \text{L} <: \text{S}, \text{L} <: \text{T} \)以及引理15.3.2的1，可得\( \text{L} = \text{L}_1 \to \text{L}_2, \text{S}_1 <: \text{L}_1, \text{L}_2 <: \text{S}_2, \text{T}_1 <: \text{L}_1, \text{L}_2 <: \text{T}_2 \)，由\( \text{L}_2 <: \text{S}_2, \text{L}_2 <: \text{T}_2 \)以及归纳假设，可得\( \text{S}_2 \wedge \text{T}_2 \neq \text{ud} \)，此时就满足算法情况4的使用条件了，由算法的情况4，可得\( \text{S} \wedge \text{T} \neq \text{ud} \)。

  3. 如果\( \text{S} = \{ \text{k}_j: \text{S}_j \ ^{j \in 1 \dots m} \}, \text{T} = \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \)，则由\( \text{L} <: \text{S}, \text{L} <: \text{T} \)以及引理15.3.2的2，可得\( \text{L} = \{ \text{m}_a: \text{M}_a \ ^{a \in 1 \dots b} \}, \{ \text{k}_j \ ^{j \in 1 \dots m} \} \subseteq \{ \text{m}_a \ ^{a \in 1 \dots b} \}, \{ \text{l}_i \ ^{i \in 1 \dots n} \} \subseteq \{ \text{m}_a \ ^{a \in 1 \dots b} \}, \forall \text{m}_a = \text{k}_j, \text{M}_a <: \text{S}_j, \forall \text{m}_a = \text{l}_i, \text{M}_a <: \text{T}_i \)，由\( \{ \text{k}_j \ ^{j \in 1 \dots m} \} \subseteq \{ \text{m}_a \ ^{a \in 1 \dots b} \}, \{ \text{l}_i \ ^{i \in 1 \dots n} \} \subseteq \{ \text{m}_a \ ^{a \in 1 \dots b} \} \)，可得\( \forall \text{k}_j = \text{l}_i, \exists \text{m}_a = \text{k}_j = \text{l}_i, \text{M}_a <: \text{S}_j, \text{M}_a <: \text{T}_i \)，进而由归纳假设，可得\( \forall \text{k}_j = \text{l}_i, \text{S}_j \wedge \text{T}_i \neq \text{ud} \)，我们构造类型\( \{ \text{m}'_a: \text{M}'_a \ ^{a \in 1 \dots b'} \} \)：

    1. 令\( \{ \text{m}'_a \ ^{a \in 1 \dots b'} \} = \{ \text{k}_j \ ^{j \in 1 \dots m} \} \cup \{ \text{l}_i \ ^{i \in 1 \dots n} \} \)。
    2. \( \forall \text{k}_j = \text{l}_i \)，我们知道\( \exists \text{m}_a = \text{k}_j = \text{l}_i \)，此时令\( \text{m}'_a = \text{m}_a, \text{M}'_a = \text{M}_a \)。
    3. \( \forall \text{m}'_a \in \{ \text{k}_j \ ^{j \in 1 \dots m} \} \setminus \{ \text{l}_i \ ^{i \in 1 \dots n} \} \)，即\( \text{S} \)独有的标签\( \text{m}'_a \)，我们知道\( \exists \text{k}_j = \text{m}'_a \)，此时令\( \text{M}'_a = \text{S}_j \)。
    4. \( \forall \text{m}'_a \in \{ \text{l}_i \ ^{i \in 1 \dots n} \} \setminus \{ \text{k}_j \ ^{j \in 1 \dots m} \} \)，即\( \text{T} \)独有的标签\( \text{m}'_a \)，我们知道\( \exists \text{l}_i = \text{m}'_a \)，此时令\( \text{M}'_a = \text{T}_i \)。

    易验证算法的情况5满足，有\( \text{S} \wedge \text{T} = \{ \text{m}'_a: \text{M}'_a \ ^{a \in 1 \dots b'} \} \neq \text{ud} \)。

综上，归纳完毕，命题成立。

证明引理2完毕。

注：下面我们均直接默认\( \text{S} \vee \text{T} \)有定义，不再显式提及引理1。

接下来，我们分两步证明1、2成立，先证明\( \text{S} \vee \text{T}, \text{S} \wedge \text{T} \)分别是\( \text{S}, \text{T} \)的共同父类型、共同子类型，在此基础上再证明\( \text{S} \vee \text{T}, \text{S} \wedge \text{T} \)是共同父类型、共同子类型中 最精确的 类型。

定理3：

  1. 如果\( \text{S} \vee \text{T} = \text{J} \)，则\( \text{S} <: \text{J}, \text{T} <: \text{J} \)。
  2. 如果\( \text{S} \wedge \text{T} = \text{M} \neq \text{ud} \)，则\( \text{M} <: \text{S}, \text{M} <: \text{T} \)。

证明定理3：

归纳假设命题对\( \text{S} \)的直接子类型成立，我们要证明命题对\( \text{S} \)成立：

针对1，对\( \text{S} \vee \text{T} \)算法的情况几成立进行分类讨论：

  1. 如果情况1成立，则\( \text{S} = \text{T} = \text{J} = \text{Bool} \)，由S-REFL，可得\( \text{S} <: \text{J}, \text{T} <: \text{J} \)。
  2. 如果情况2成立，则\( \text{S} = \text{S}_1 \to \text{S}_2, \text{T} = \text{T}_1 \to \text{T}_2, \text{M}_1 = \text{S}_1 \wedge \text{T}_1, \text{M}_1 \neq \text{ud}, \text{J}_2 = \text{S}_2 \vee \text{T}_2, \text{J} = \text{M}_1 \to \text{J}_2 \)，由\( \text{M}_1 = \text{S}_1 \wedge \text{T}_1, \text{M}_1 \neq \text{ud} \)以及归纳假设，可得\( \text{M}_1 <: \text{S}_1, \text{M}_1 <: \text{T}_1 \)，由\( \text{J}_2 = \text{S}_2 \vee \text{T}_2 \)以及归纳假设，可得\( \text{S}_2 <: \text{J}_2, \text{T}_2 <: \text{J}_2 \)，由\( \text{M}_1 <: \text{S}_1, \text{S}_2 <: \text{J}_2 \)以及S-ARROW，可得\( \text{S} <: \text{J} \)，同理可得\( \text{T} <: \text{J} \)。
  3. 如果情况3成立，则\( \text{S} = \{ \text{k}_j: \text{S}_j \ ^{j \in 1 \dots m} \}, \text{T} = \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \}, \text{J} = \{ \text{u}_a: \text{U}_a \ ^{a \in 1 \dots b} \}, \{ \text{u}_a \ ^{a \in 1 \dots b} \} = \{ \text{k}_j \ ^{j \in 1 \dots m} \} \cap \{ \text{l}_i \ ^{i \in 1 \dots n} \}, \forall \text{u}_a = \text{k}_j = \text{l}_i, \text{U}_a = \text{S}_j \vee \text{T}_i \)，由\( \forall \text{u}_a = \text{k}_j = \text{l}_i, \text{U}_a = \text{S}_j \vee \text{T}_i \)以及归纳假设，可得\( \forall \text{u}_a = \text{k}_j = \text{l}_i, \text{S}_j <: \text{U}_a, \text{T}_i <: \text{U}_a \) (a) ，易得\( \{ \text{u}_a \ ^{a \in 1 \dots b} \} \subseteq \{ \text{k}_j \ ^{j \in 1 \dots m} \} \)，为了证明\( \text{S} <: \text{J} \)，我们还得证明\( \forall \text{u}_a = \text{k}_j, \text{S}_j <: \text{U}_a \)，针对\( \forall \text{u}_a = \text{k}_j \)，由\( \{ \text{u}_a \ ^{a \in 1 \dots b} \} = \{ \text{k}_j \ ^{j \in 1 \dots m} \} \cap \{ \text{l}_i \ ^{i \in 1 \dots n} \} \)，可得\( \exists \text{l}_i = \text{u}_a \)，于是有\( \text{u}_a = \text{k}_j = \text{l}_i \)，进而结合(a)，可得\( \text{S}_j <: \text{U}_a \)（注：虽然用不到\( i \)下标，但是(a)处的描述方式使得我们需要保证满足\( \text{u}_a = \text{k}_j = \text{l}_i \)的标签\( \text{l}_i \)的存在性，仅仅写\( \text{u}_a = \text{k}_j \)容易造成误解），进而由S-RCD以及引理16.1.1，可得\( \text{S} <: \text{J} \)，同理可得\( \text{T} <: \text{J} \)。
  4. 如果情况4成立，则\( \text{J} = \text{Top} \)，此时由S-TOP，可得\( \text{S} <: \text{J}, \text{T} <: \text{J} \)。

针对2，对\( \text{S} \wedge \text{T} \)算法的情况几成立进行分类讨论：

  1. 如果情况1成立，则\( \text{T} = \text{Top}, \text{M} = \text{S} \)，此时由S-REFL，可得\( \text{M} <: \text{S} \)，由S-TOP，可得\( \text{M} <: \text{T} \)。

  2. 如果情况2成立，则\( \text{S} = \text{Top}, \text{M} = \text{T} \)，此时由S-TOP，可得\( \text{M} <: \text{S} \)，由S-REFL，可得\( \text{M} <: \text{T} \)。

  3. 如果情况3成立，则\( \text{S} = \text{T} = \text{M} = \text{Bool} \)，由S-REFL，可得\( \text{M} <: \text{S}, \text{M} <: \text{T} \)。

  4. 如果情况4成立，则\( \text{S} = \text{S}_1 \to \text{S}_2, \text{T} = \text{T}_1 \to \text{T}_2, \text{J}_1 = \text{S}_1 \vee \text{T}_1, \text{M}_2 = \text{S}_2 \wedge \text{T}_2, \text{M}_2 \neq \text{ud}, \text{M} = \text{J}_1 \to \text{M}_2 \)，由\( \text{J}_1 = \text{S}_1 \vee \text{T}_1 \)以及归纳假设，可得\( \text{S}_1 <: \text{J}_1, \text{T}_1 <: \text{S}_1 \)，由\( \text{M}_2 = \text{S}_2 \wedge \text{T}_2, \text{M}_2 \neq \text{ud} \)以及归纳假设，可得\( \text{M}_2 <: \text{S}_2, \text{M}_2 <: \text{T}_2 \)，由\( \text{S}_1 <: \text{J}_1, \text{M}_2 <: \text{S}_2 \)以及S-ARROW，可得\( \text{M} <: \text{S} \)，同理可得\( \text{M} <: \text{T} \)。

  5. 如果情况5成立，则\( \text{S} = \{ \text{k}_j: \text{S}_j \ ^{j \in 1 \dots m} \}, \text{T} = \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \}, \text{M} = \{ \text{m}_a: \text{M}_a \ ^{a \in 1 \dots b} \}, \{ \text{m}_a \ ^{a \in 1 \dots b} \} = \{ \text{k}_j \ ^{j \in 1 \dots m} \} \cup \{ \text{l}_i \ ^{i \in 1 \dots n} \}, \forall \text{m}_a = \text{k}_j = \text{l}_i, \text{M}_a = \text{S}_j \wedge \text{T}_i, \text{M}_a \neq \text{ud}, \forall \text{S} \text{独有的标签} \text{m}_a = \text{k}_j, \text{M}_a = \text{S}_j, \forall \text{T} \text{独有的标签} \text{m}_a = \text{l}_i, \text{M}_a = \text{T}_i \)，由\( \forall \text{m}_a = \text{k}_j = \text{l}_i, \text{M}_a = \text{S}_j \wedge \text{T}_i, \text{M}_a \neq \text{ud} \)以及归纳假设，可得\( \forall \text{m}_a = \text{k}_j = \text{l}_i, \text{M}_a <: \text{S}_j, \text{M}_a <: \text{T}_i \) (b) ，由S-REFL，可得\( \forall \text{S} \text{独有的标签} \text{m}_a = \text{k}_j, \text{M}_a <: \text{S}_j \) (c) , \( \forall \text{T} \text{独有的标签} \text{m}_a = \text{l}_i, \text{M}_a <: \text{T}_i \)，易得\( \{ \text{k}_j \ ^{j \in 1 \dots m} \} \subseteq \{ \text{m}_a \ ^{a \in 1 \dots b} \} \)，为了证明\( \text{M} <: \text{S} \)，我们还得证明\( \forall \text{m}_a = \text{k}_j, \text{M}_a <: \text{S}_j \)，针对\( \forall \text{m}_a = \text{k}_j \)，分两种情况：

    1. \( \exists \text{l}_i = \text{m}_a \)，则\( \text{m}_a = \text{k}_j = \text{l}_i \)，进而由(b)，可得\( \text{M}_a <: \text{S}_j \)。
    2. \( \nexists \text{l}_i \)满足\( \text{l}_i = \text{m}_a \)，加上\( \{ \text{m}_a \ ^{a \in 1 \dots b} \} = \{ \text{k}_j \ ^{j \in 1 \dots m} \} \cup \{ \text{l}_i \ ^{i \in 1 \dots n} \} \)，可得\( \text{m}_a \in \{ \text{k}_j \ ^{j \in 1 \dots m} \} \setminus \{ \text{l}_i \ ^{i \in 1 \dots n} \} \)，即\( \text{m}_a \)为\( \text{S} \)独有的标签，进而由(c)，可得\( \text{M}_a <: \text{S}_j \)。

    综上以及使用S-RCD、引理16.1.1，可得\( \text{M} <: \text{S} \)，同理可得\( \text{M} <: \text{T} \)。

  6. 情况6不可能成立，因为\( \text{M} \neq \text{ud} \)。

综上，归纳完毕，命题成立。

证明定理3完毕。

最后，我们证明\( \text{S} \vee \text{T}, \text{S} \wedge \text{T} \)是 最精确的 共同父类型、共同子类型。

定理4：

  1. 如果\( \text{S} \vee \text{T} = \text{J} \)，则\( \forall \text{U} \)满足\( \text{S} <: \text{U}, \text{T} <: \text{U} \)，我们有\( \text{J} <: \text{U} \)。
  2. 如果\( \text{S} \wedge \text{T} = \text{M} \neq \text{ud} \)，则\( \forall \text{L} \)满足\( \text{L} <: \text{S}, \text{L} <: \text{T} \)，我们有\( \text{L} <: \text{M} \)。

证明定理4：

归纳假设命题对\( \text{S} \)的直接子类型成立，我们要证明命题对\( \text{S} \)成立。

针对1，我们对\( \text{U} \)的形式进行分类讨论：

  1. 如果\( \text{U} = \text{Top} \)，则由S-TOP，可得\( \text{J} <: \text{U} \)。
  2. 如果\( \text{U} = \text{Bool} \)，则由引理15.3.2（拓展到\( \text{Bool} \)的情况），可得\( \text{S} = \text{T} = \text{Bool} \)，此时由\( \text{S} \vee \text{T} \)算法的情况1，可得\( \text{J} = \text{Bool} \)，进而由S-REFL，可得\( \text{J} <: \text{U} \)。
  3. 如果\( \text{U} = \text{U}_1 \to \text{U}_2 \)，则由引理15.3.2的1，可得\( \text{S} = \text{S}_1 \to \text{S}_2, \text{U}_1 <: \text{S}_1, \text{S}_2 <: \text{U}_2, \text{T} = \text{T}_1 \to \text{T}_2, \text{U}_1 <: \text{T}_1, \text{T}_2 <: \text{U}_2 \)，由\( \text{U}_1 <: \text{S}_1, \text{U}_1 <: \text{T}_1 \)以及引理2，可得\( \text{S}_1 \wedge \text{T}_1 \neq \text{ud} \)，进而由归纳假设，可得\( \text{U}_1 <: \text{S}_1 \wedge \text{T}_1 \)，而由\( \text{S}_2 <: \text{U}_2, \text{T}_2 <: \text{U}_2 \)以及归纳假设，可得\( \text{S}_2 \vee \text{T}_2 <: \text{U}_2 \)，令\( \text{M}_1 = \text{S}_1 \wedge \text{T}_1, \text{J}_2 = \text{S}_2 \vee \text{T}_2 \)，由\( \text{S} \vee \text{T} \)算法的情况2，可得\( \text{J} = \text{M}_1 \to \text{J}_2 \)，由S-ARROW，可得\( \text{M}_1 \to \text{J}_2 <: \text{U} \)，也就是\( \text{J} <: \text{U} \)。
  4. 如果\( \text{U} = \{ \text{o}_c: \text{O}_c \ ^{c \in 1 \dots d} \} \)，则由引理15.3.2的2，可得\( \text{S} = \{ \text{k}_j: \text{S}_j \ ^{j \in 1 \dots m} \}, \text{T} = \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \}, \{ \text{o}_c \ ^{c \in 1 \dots d} \} \subseteq \{ \text{k}_j \ ^{j \in 1 \dots m} \}, \{ \text{o}_c \ ^{c \in 1 \dots d} \} \subseteq \{ \text{l}_i \ ^{i \in 1 \dots n} \}, \forall \text{o}_c = \text{k}_j, \text{S}_j <: \text{O}_c, \forall \text{o}_c = \text{l}_i, \text{T}_i <: \text{O}_c \)，进而由归纳假设，可得\( \forall \text{o}_c = \text{k}_j = \text{l}_i, \text{S}_j \vee \text{T}_i <: \text{O}_c \) (d) ，令\( \{ \text{u}_a \ ^{a \in 1 \dots b} \} = \{ \text{k}_j \ ^{j \in 1 \dots m} \} \cap \{ \text{l}_i \ ^{i \in 1 \dots n} \} \)， \( \forall \text{u}_a = \text{k}_j = \text{l}_i \)，令\( \text{U}_a = \text{S}_j \vee \text{T}_i \) (e) ，则由\( \text{S} \vee \text{T} \)算法的情况3，可得\( \text{J} = \{ \text{u}_a: \text{U}_a \ ^{a \in 1 \dots b} \} \)，易得\( \{ \text{o}_c \ ^{c \in 1 \dots d} \} \subseteq \{ \text{u}_a \ ^{a \in 1 \dots b} \} \)，为了证明\( \text{J} <: \text{U} \)，我们还得证明\( \forall \text{o}_c = \text{u}_a, \text{U}_a <: \text{O}_c \)，针对\( \forall \text{o}_c = \text{u}_a \)，由\( \{ \text{u}_a \ ^{a \in 1 \dots b} \} = \{ \text{k}_j \ ^{j \in 1 \dots m} \} \cap \{ \text{l}_i \ ^{i \in 1 \dots n} \} \)，可得\( \exists \text{k}_j, \text{l}_i, \text{k}_j = \text{l}_i = \text{o}_c \)，进而由(e)以及(d)，可得\( \text{U}_a = \text{S}_j \vee \text{T}_i <: \text{O}_c \)，综上以及使用S-RCD、引理16.1.1，可得\( \text{J} <: \text{U} \)。

针对2，对\( \text{S} \wedge \text{T} \)算法的情况几成立进行分类讨论：

  1. 如果情况1成立，则\( \text{T} = \text{Top}, \text{M} = \text{S} \)，此时由S-REFL，可得\( \text{S} <: \text{M} \)，再由\( \text{L} <: \text{S} \)以及S-TRANS，可得\( \text{L} <: \text{M} \)。

  2. 如果情况2成立，则\( \text{S} = \text{Top}, \text{M} = \text{T} \)，此时由S-REFL，可得\( \text{T} <: \text{M} \)，再由\( \text{L} <: \text{T} \)以及S-TRANS，可得\( \text{L} <: \text{M} \)。

  3. 如果情况3成立，则\( \text{S} = \text{T} = \text{M} = \text{Bool} \)，此时由\( \text{L} <: \text{S} \)以及引理15.3.2（拓展到\( \text{Bool} \)的情况），可得\( \text{L} = \text{Bool} \)，进而由S-REFL，可得\( \text{L} <: \text{M} \)。

  4. 如果情况4成立，则\( \text{S} = \text{S}_1 \to \text{S}_2, \text{T} = \text{T}_1 \to \text{T}_2, \text{J}_1 = \text{S}_1 \vee \text{T}_1, \text{M}_2 = \text{S}_2 \wedge \text{T}_2, \text{M}_2 \neq \text{ud}, \text{M} = \text{J}_1 \to \text{M}_2 \)，由\( \text{L} <: \text{S}, \text{L} <: \text{T} \)以及引理15.3.2的1，可得\( \text{L} = \text{L}_1 \to \text{L}_2, \text{S}_1 <: \text{L}_1, \text{L}_2 <: \text{S}_2, \text{T}_1 <: \text{L}_1, \text{L}_2 <: \text{T}_2 \)，由\( \text{S}_1 <: \text{L}_1, \text{T}_1 <: \text{L}_1 \)以及归纳假设，可得\( \text{J}_1 <: \text{L}_1 \)，由\( \text{M}_2 \neq \text{ud}, \text{L}_2 <: \text{S}_2, \text{L}_2 <: \text{T}_2 \)以及归纳假设，可得\( \text{L}_2 <: \text{M}_2 \)，综上以及使用S-ARROW，可得\( \text{L} <: \text{M} \)。

  5. 如果情况5成立，则\( \text{S} = \{ \text{k}_j: \text{S}_j \ ^{j \in 1 \dots m} \}, \text{T} = \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \}, \text{M} = \{ \text{m}_a: \text{M}_a \ ^{a \in 1 \dots b} \}, \{ \text{m}_a \ ^{a \in 1 \dots b} \} = \{ \text{k}_j \ ^{j \in 1 \dots m} \} \cup \{ \text{l}_i \ ^{i \in 1 \dots n} \}, \forall \text{m}_a = \text{k}_j = \text{l}_i, \text{M}_a = \text{S}_j \wedge \text{T}_i, \text{M}_a \neq \text{ud} \) (f) ， \( \forall \text{S} \text{独有的标签} \text{m}_a = \text{k}_j, \text{M}_a = \text{S}_j \) (g) ， \( \forall \text{T} \text{独有的标签} \text{m}_a = \text{l}_i, \text{M}_a = \text{T}_i \)，由\( \text{L} <: \text{S}, \text{L} <: \text{T} \)以及引理15.3.2的2，可得\( \text{L} = \{ \text{o}_c: \text{O}_c \ ^{c \in 1 \dots d} \}, \{ \text{k}_j \ ^{j \in 1 \dots m} \} \subseteq \{ \text{o}_c \ ^{c \in 1 \dots d} \}, \{ \text{l}_i \ ^{i \in 1 \dots n} \} \subseteq \{ \text{o}_c \ ^{c \in 1 \dots d} \}, \forall \text{o}_c = \text{k}_j, \text{O}_c <: \text{S}_j, \forall \text{o}_c = \text{l}_i, \text{O}_c <: \text{T}_i \) (h) ，易得\( \{ \text{m}_a \ ^{a \in 1 \dots b} \} \subseteq \{ \text{o}_c \ ^{c \in 1 \dots d} \} \)，为了证明\( \text{L} <: \text{M} \)，我们还得证明\( \forall \text{o}_c = \text{m}_a, \text{O}_c <: \text{M}_a \)，针对\( \forall \text{o}_c = \text{m}_a \)，由\( \{ \text{m}_a \ ^{a \in 1 \dots b} \} = \{ \text{k}_j \ ^{j \in 1 \dots m} \} \cup \{ \text{l}_i \ ^{i \in 1 \dots n} \} \)，可得\( \exists \text{k}_j = \text{m}_a \)或\( \exists \text{l}_i = \text{m}_a \)：

    1. 如果\( \exists \text{k}_j = \text{m}_a \)，继续分两种情况：
      1. 如果\( \exists \text{l}_i = \text{m}_a \)，则\( \text{m}_a = \text{k}_j = \text{l}_i \)，此时由(f)，可得\( \text{M}_a = \text{S}_j \wedge \text{T}_i, \text{M}_a \neq \text{ud} \)，再由\( \text{o}_c = \text{m}_a = \text{k}_j, \text{o}_c = \text{m}_a = \text{l}_i \)以及(h)，可得\( \text{O}_c <: \text{S}_j, \text{O}_c <: \text{T}_i \)，进而由归纳假设，可得\( \text{O}_c <: \text{S}_j \wedge \text{T}_i = \text{M}_a \)。
      2. 如果\( \nexists \text{l}_i = \text{m}_a \)，则\( \text{m}_a \in \{ \text{k}_j \ ^{j \in 1 \dots m} \} \setminus \{ \text{l}_i \ ^{i \in 1 \dots n} \} \)，即\( \text{m}_a \)为\( \text{S} \)独有的标签，此时由(g)，可得\( \text{M}_a = \text{S}_j \)，再由\( \text{o}_c = \text{m}_a = \text{k}_j \)以及(h)，可得\( \text{O}_c <: \text{S}_j = \text{M}_a \)。
    2. 如果\( \exists \text{l}_i = \text{m}_a \)，则同上，继续分两种情况讨论，易得\( \text{O}_c <: \text{M}_a \)。

    综上以及使用S-RCD、引理16.1.1，可得\( \text{L} <: \text{M} \)。

  6. 情况6不可能成立，因为\( \text{M} \neq \text{ud} \)。

综上，归纳完毕，命题成立。

证明定理4完毕。

综上，由定理3、定理4，可得算法给出的\( \text{S} \vee \text{T}, \text{S} \wedge \text{T} \)分别是\( \text{S}, \text{T} \)的共同父类型、共同子类型，且是共同父类型、共同子类型中 最精确的 类型，即1、2成立。

证毕。

练习16.3.3

题目：

What is the minimal type of \( \text{if true then false else } \{ \} \)? Is this what we want?

解答：

易得\( \Gamma \vdash \text{true}: \text{Bool}, \Gamma \vdash \text{false}: \text{Bool}, \Gamma \vdash \{ \}: \{ \} \)，而\( \text{Bool} \vee \{ \} = \text{Top} \)，于是由TA-IF，可得\( \Gamma \vdash \text{if true then false else } \{ \}: \text{Top} \)。然而类型\( \text{Top} \)不是我们想要的，没有操作可作用于类型为\( \text{Top} \)的值，故这种情况下\( \text{if true then false else } \{ \} \)是类型良好的对程序员来说几乎没用，有几种可选的处理方法：

  1. 让类型检查器在推导出类型为\( \text{Top} \)的项时，给个警告。
  2. 直接将\( \text{Top} \)从类型系统中移除，此时\( \vee \)操作会变成偏函数（不再对所有\( \text{S}, \text{T} \)均有定义），同时上述的\( \text{if true then false else } \{ \} \)也不再是类型良好的了。

练习16.3.4

题目：

  1. Is it easy to extend the algorithms for calculating joins and meets to an imperative language with references, as described in \( \S \text{15.5} \)?
  2. What about the treatment of references in \( \S \text{15.5} \), where we refine the invariant \( \text{Ref} \) with covariant \( \text{Source} \) and contravariant \( \text{Sink} \)?

解答：

解答1：

是的，不过得注意，我们仍然要求引用的基础类型之间的关系是invariant，即只允许record改变域顺序之类的简单改动。

下面，我们拓展练习16.3.2的证明中给出的算法，增加引用对应的情况，如下：

\[ \text{S} \vee \text{T} = \begin{cases} \dots &\dots \\ \text{Ref } \text{T}_1 &\text{如果} \text{S} = \text{Ref } \text{S}_1 \quad \text{T} = \text{Ref } \text{T}_1 \\ &\hphantom{如果} \text{S}_1 <: \text{T}_1 \quad \text{T}_1 <: \text{S}_1 \\ \dots &\dots \end{cases} \]

\[ \text{S} \wedge \text{T} = \begin{cases} \dots &\dots \\ \text{Ref } \text{T}_1 &\text{如果} \text{S} = \text{Ref } \text{S}_1 \quad \text{T} = \text{Ref } \text{T}_1 \\ &\hphantom{如果} \text{S}_1 <: \text{T}_1 \quad \text{T}_1 <: \text{S}_1 \\ \dots &\dots \end{cases} \]

解答2：

此时就无法拓展练习16.3.2的证明中给出的算法以覆盖引用的情况了，举个例子：令\( \text{S} = \text{Ref } \{ \text{l}_1: \text{Bool}, \text{l}_2: \text{Bool} \}, \text{T} = \text{Ref } \{ \text{l}_1: \text{Bool} \} \)，则\( \text{S}, \text{T} \)有共同父类型\( \text{Source} \{ \text{l}_1: \text{Bool} \} \)以及 \( \text{Sink} \{ \text{l}_1: \text{Bool}, \text{l}_2: \text{Bool} \} \)，那么\( \text{S} \vee \text{T} \)作为\( \text{S}, \text{T} \)最精确的共同父类型，它得是\( \text{Source} \{ \text{l}_1: \text{Bool} \}, \text{Sink} \{ \text{l}_1: \text{Bool}, \text{l}_2: \text{Bool} \} \)的子类型，但是\( \text{Source} \{ \text{l}_1: \text{Bool} \}, \text{Sink} \{ \text{l}_1: \text{Bool}, \text{l}_2: \text{Bool} \} \)并没有共同子类型， \( \wedge \)同理也未定义。

第一种方案，我们可以选择仅保留\( \text{Source}, \text{Sink} \)的其中之一，\( \text{Ref} \)则仍然保留，它仍然同时具有读和写的能力，只不过由于类型系统中只剩\( \text{Source} \)或只剩\( \text{Sink} \)了，因此\( \text{Ref} \)也就只能转换成\( \text{Source} \)或者只能转换成\( \text{Sink} \)了。可以这样做的原因是因为很多情况下，我们只需要\( \text{Source}, \text{Sink} \)的其中之一即可，不需要两个都有，举个例子，在章节18.12中，我们会通过引用来避免每次使用\( \text{self} \)的时候都会重新计算一遍对象的方法的问题，提高运行效率，这种情况下，我们只需要用到\( \text{Source} \)的covariant特性，不需要用到\( \text{Sink} \)。再举个例子，在章节15.5中，我们通过channel来实现并发编程的通讯，而并发编程一个典型的场景就是single receiver multiple sender，比如我们只有一个服务器，但是有多个客户端就是这一场景，这种情况下，我们只需要能将\( \text{Ref} \)转换成\( \text{Sink} \)，然后传播\( \text{Sink} \)给多个客户端，让每个客户端持有一个\( \text{Sink} \)用于发送数据给服务器即可，而服务器持有\( \text{Ref} \)，同时具有读写能力。这种方案下就很容易拓展拓展练习16.3.2的证明中给出的算法了，比如仅保留\( \text{Ref}, \text{Source} \)，则按如下规则拓展算法：

\[ \text{S} \vee \text{T} = \begin{cases} \dots &\dots \\ \text{Source } \text{J}_1 &\text{如果} \text{S} = \text{Ref } \text{S}_1 \text{或} \text{S} = \text{Source } \text{S}_1 \\ &\hphantom{如果} \text{T} = \text{Ref } \text{T}_1 \text{或} \text{T} = \text{Source } \text{T}_1 \\ &\hphantom{如果} \text{J}_1 = \text{S}_1 \vee \text{T}_1 \\ \dots &\dots \end{cases} \]

\[ \text{S} \wedge \text{T} = \begin{cases} \dots &\dots \\ \text{Source } \text{M}_1 &\text{如果} \text{S} = \text{Ref } \text{S}_1 \text{或} \text{S} = \text{Source } \text{S}_1 \\ &\hphantom{如果} \text{T} = \text{Ref } \text{T}_1 \text{或} \text{T} = \text{Source } \text{T}_1 \\ &\hphantom{如果} \text{M}_1 = \text{S}_1 \wedge \text{T}_1 \\ \dots &\dots \end{cases} \]

需要注意的是，如果\( \text{S}, \text{T} \)都是引用，即\( \text{S} = \text{Ref } \text{S}_1, \text{T} = \text{Ref } \text{T}_1 \)的情况下，则我们不能令\( \text{S} \vee \text{T} = \text{Ref } \text{J}_1, \text{S} \wedge \text{T} = \text{Ref } \text{M}_1 \)，虽然这看起来像是更精确的共同父/子类型，还是之前的问题，\( \text{Ref} \)的子类型规则对读和写有不同的要求，如果令\( \text{S} \vee \text{T} = \text{Ref } \text{J}_1, \text{S} \wedge \text{T} = \text{Ref } \text{M}_1 \)，则同一个引用可能在不同地方被转换成互不兼容的类型，这是上面我们一律在这种情况下令\( \text{S} \vee \text{T}, \text{S} \wedge \text{T} \)均为\( \text{Source} \)的原因。

第二种方案，就是让\( \text{Ref} \)类型构造器从接收一个类型参数改成接收两个类型参数，区分开读和写的能力，如类型\( \text{Ref } \text{T}_1 \text{ } \text{T}_2 \)，我们能对该类型的引用读取出类型为\( \text{T}_1 \)的值、写入类型为\( \text{T}_2 \)的值，其中在子类型规则中，第一个类型参数类似\( \text{Source} \)，遵循covariant，第二个类型参数类似\( \text{Sink} \)，遵循contravariant，整体子类型规则类似函数类型（不过顺序是反的），如下：

\[ \dfrac{\text{S}_1 <: \text{T}_1 \quad \text{T}_2 <: \text{S}_2}{ \text{Ref } \text{S}_1 \text{ } \text{S}_2 <: \text{Ref } \text{T}_1 \text{ } \text{T}_2} \qquad (\text{S-REF}) \]

此时令\( \text{S} = \text{Ref } \text{S}_1 \text{ } \text{S}_2, \text{T} = \text{Ref } \text{T}_1 \text{ } \text{T}_2 \)，则针对\( \text{S} \vee \text{T} \)，我们希望第一个类型参数，即读类型，为\( \text{S}_1, \text{T}_1 \)最精确的共同父类型，第二个类型参数，即写类型，则为\( \text{S}_2, \text{T}_2 \)最精确的共同子类型， \( \text{S} \wedge \text{T} \)则类似，是对称的，因此，我们按如下规则拓展练习16.3.2的证明中给出的算法：

\[ \text{S} \vee \text{T} = \begin{cases} \dots &\dots \\ \text{Ref } \text{J}_1 \text{ } \text{M}_2 &\text{如果} \text{S} = \text{Ref } \text{S}_1 \text{ } \text{S}_2 \quad \text{T} = \text{Ref } \text{T}_1 \text{ } \text{T}_2 \\ &\hphantom{如果} \text{J}_1 = \text{S}_1 \vee \text{T}_1 \\ &\hphantom{如果} \text{M}_2 = \text{S}_2 \wedge \text{T}_2 \text{且} \text{M}_2 \neq \text{ud} \\ \dots &\dots \end{cases} \]

\[ \text{S} \wedge \text{T} = \begin{cases} \dots &\dots \\ \text{Ref } \text{M}_1 \text{ } \text{J}_2 &\text{如果} \text{S} = \text{Ref } \text{S}_1 \text{ } \text{S}_2 \quad \text{T} = \text{Ref } \text{T}_1 \text{ } \text{T}_2 \\ &\hphantom{如果} \text{M}_1 = \text{S}_1 \wedge \text{T}_1 \text{且} \text{M}_1 \neq \text{ud} \\ &\hphantom{如果} \text{J}_2 = \text{S}_2 \vee \text{T}_2 \\ \dots &\dots \end{cases} \]

这种方案下，\( \text{Source} \)和\( \text{Sink} \)仍可以保留，不过得添加\( \text{Bot} \)类型，添加\( \text{Bot} \)类型以及拓展练习16.3.2的证明中给出的算法后（怎么拓展算法以覆盖\( \text{Bot} \)等下讲，不过读者在直觉上应该容易猜测大概该怎么做），将\( \text{Source } \text{T}_1 \)定义成\( \text{Ref } \text{T}_1 \text{ } \text{Bot} \)的缩写，而\( \text{Sink } \text{T}_1 \)则定义成\( \text{Ref } \text{Top} \text{ } \text{T}_1 \)的缩写。读者可能会有疑问，为什么\( \text{Source } \text{T}_1 \)要定义成\( \text{Ref } \text{T}_1 \text{ } \text{Bot} \)的缩写，而不定义成\( \text{Ref } \text{T}_1 \text{ } \text{Top} \)的缩写，这样似乎不用额外增加\( \text{Bot} \)类型了，这是因为我们希望\( \text{S} = \text{Source } \text{S}_1 \)和任意类型\( \text{T}_1 \)的共同父类型都是不具备写能力的，而和任意类型\( \text{T}_2 \)的共同子类型的写能力的 上限 则完全取决于\( \text{T}_2 \)本身的写能力，不受\( \text{S} \)的影响，由于\( \text{Ref} \)的第二个类型参数遵循contravariant，因此为了达到上述要求，我们需要把\( \text{Source } \text{T}_1 \)定义成\( \text{Ref } \text{T}_1 \text{ } \text{Bot} \)的缩写，这样的话，举个例子，令\( \text{S} = \text{Source } \text{S}_1 \)，令\( \text{T} = \text{Ref } \text{T}_1 \text{ } \text{T}_2 \)，则假设存在\( \text{S}, \text{T} \)的共同父类型\( \text{U} \)，也就是\( \text{S} <: \text{U}, \text{T} <: \text{U} \)，则\( \text{S} \vee \text{T} <: \text{U} \)，易得\( \text{S} \vee \text{T} = \text{Ref } (\text{S}_1 \vee \text{T}_1) \text{ } (\text{Bot} \wedge \text{T}_2) = \text{Ref } (\text{S}_1 \vee \text{T}_1) \text{ } \text{Bot} = \text{Source } (\text{S}_1 \vee \text{T}_1) \)，进而易得\( \text{U} = \text{Top} \)或\( \text{U} = \text{Ref } \text{U}_1 \text{ } \text{U}_2 \)，如果\( \text{U} = \text{Top} \)，则\( \text{U} \)明显不具备写能力，如果\( \text{U} = \text{Ref } \text{U}_1 \text{ } \text{U}_2 \)，则由引理15.3.2（拓展到\( \text{Ref} \)的情况），可得\( \text{U} = \text{Ref } \text{U}_1 \text{ } \text{Bot} = \text{Source } \text{U}_1 \)，也就是共同父类型\( \text{U} \)不具备写能力，假设存在\( \text{S}, \text{T} \)的共同子类型\( \text{L} \)，也就是\( \text{L} <: \text{S}, \text{L} <: \text{T} \)，则\( \text{L} <: \text{S} \wedge \text{T} \)，易得\( \text{S} \wedge \text{L} = \text{Ref } (\text{S}_1 \wedge \text{T}_1) \text{ } (\text{Bot} \vee \text{T}_2) = \text{Ref } (\text{S}_1 \wedge \text{T}_1) \text{ } \text{T}_2 = \text{Ref } (\text{S}_1 \wedge \text{T}_1) \text{ } \text{T}_2 \)，进而由引理15.3.2（拓展到\( \text{Ref} \)的情况），可得\( \text{L} = \text{Ref } \text{L}_1 \text{ } \text{L}_2, \text{T}_2 <: \text{L}_2 \)，也就是共同子类型\( \text{L} \)的写能力的上限完全取决于\( \text{T} \)本身的写能力（注：能写入越精细的类型，写能力越强，所以叫上限，而不叫下限），不受\( \text{S} \)的影响。 \( \text{Sink } \text{T}_1 \)定义成\( \text{Ref } \text{Top} \text{ } \text{T}_1 \)的原因同理。

引入\( \text{Source}, \text{Sink} \)的缩写前，我们需要引入\( \text{Bot} \)类型，首先需要引入如下子类型规则：

\[ \text{Bot} <: \text{T} \qquad (\text{S-BOT}) \]

除此之外，还得拓展T-APP、T-PROJ（或者说TA-APP、TA-PROJ）等多个规则，详细请参考章节16.4，这里就不完整写了。

接着，需要拓展练习16.3.2的证明中给出的算法，需要注意的是，引入\( \text{Bot} \)后，\( \text{S} \wedge \text{T} \)就不再是偏函数了，其他情况都可以fallback到\( \text{Bot} \)，也不用考虑\( \text{S} \wedge \text{T} \)未定义的情况了，完整算法定义如下：

\[ \text{S} \vee \text{T} = \begin{cases} \text{Bool} &\text{如果} \text{S} = \text{T} = \text{Bool} \\ \text{M}_1 \to \text{J}_2 &\text{如果} \text{S} = \text{S}_1 \to \text{S}_2 \quad \text{T} = \text{T}_1 \to \text{T}_2 \\ &\hphantom{如果} \text{M}_1 = \text{S}_1 \wedge \text{T}_1 \\ &\hphantom{如果} \text{J}_2 = \text{S}_2 \vee \text{T}_2 \\ \{ \text{u}_a: \text{U}_a \ ^{a \in 1 \dots b} \} &\text{如果} \text{S} = \{ \text{k}_j: \text{S}_j \ ^{j \in 1 \dots m} \} \\ &\hphantom{如果} \text{T} = \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \\ &\hphantom{如果} \{ \text{u}_a \ ^{a \in 1 \dots b} \} = \{ \text{k}_j \ ^{j \in 1 \dots m} \} \cap \{ \text{l}_i \ ^{i \in 1 \dots n} \} \\ &\hphantom{如果} \forall \text{u}_a = \text{k}_j = \text{l}_i, \text{U}_a = \text{S}_j \vee \text{T}_i \\ \text{Ref } \text{J}_1 \text{ } \text{M}_2 &\text{如果} \text{S} = \text{Ref } \text{S}_1 \text{ } \text{S}_2 \quad \text{T} = \text{Ref } \text{T}_1 \text{ } \text{T}_2 \\ &\hphantom{如果} \text{J}_1 = \text{S}_1 \vee \text{T}_1 \\ &\hphantom{如果} \text{M}_2 = \text{S}_2 \wedge \text{T}_2 \\ \text{Top} &\text{不满足上述情况} \end{cases} \]

\[ \text{S} \wedge \text{T} = \begin{cases} \text{S} &\text{如果} \text{T} = \text{Top} \\ \text{T} &\text{如果} \text{S} = \text{Top} \\ \text{Bool} &\text{如果} \text{S} = \text{T} = \text{Bool} \\ \text{J}_1 \to \text{M}_2 &\text{如果} \text{S} = \text{S}_1 \to \text{S}_2 \quad \text{T} = \text{T}_1 \to \text{T}_2 \\ &\hphantom{如果} \text{J}_1 = \text{S}_1 \vee \text{T}_1 \\ &\hphantom{如果} \text{M}_2 = \text{S}_2 \wedge \text{T}_2 \\ \{ \text{m}_a: \text{M}_a \ ^{a \in 1 \dots b} \} &\text{如果} \text{S} = \{ \text{k}_j: \text{S}_j \ ^{j \in 1 \dots m} \} \\ &\hphantom{如果} \text{T} = \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \\ &\hphantom{如果} \{ \text{m}_a \ ^{a \in 1 \dots b} \} = \{ \text{k}_j \ ^{j \in 1 \dots m} \} \cup \{ \text{l}_i \ ^{i \in 1 \dots n} \} \\ &\hphantom{如果} \forall \text{m}_a = \text{k}_j = \text{l}_i, \text{M}_a = \text{S}_j \wedge \text{T}_i \\ &\hphantom{如果} \forall \text{S} \text{独有的标签} \text{m}_a = \text{k}_j, \text{M}_a = \text{S}_j \\ &\hphantom{如果} \forall \text{T} \text{独有的标签} \text{m}_a = \text{l}_i, \text{M}_a = \text{T}_i \\ \text{Ref } \text{M}_1 \text{ } \text{J}_2 &\text{如果} \text{S} = \text{Ref } \text{S}_1 \text{ } \text{S}_2 \quad \text{T} = \text{Ref } \text{T}_1 \text{ } \text{T}_2 \\ &\hphantom{如果} \text{M}_1 = \text{S}_1 \wedge \text{T}_1 \\ &\hphantom{如果} \text{J}_2 = \text{S}_2 \vee \text{T}_2 \\ \text{Bot} &\text{不满足上述情况} \end{cases} \]

章节16.4

练习16.4.1

题目：

Suppose we also have conditionals in the language. Do we need to add another algorithmic typing rule for \( \text{if} \)?

解答：

需要的，因为算法性类型规则中缺乏T-SUB。

最简单的，我们直接把\( \text{Bot} \)当作\( \text{Bool} \)，其他部分和TA-IF一样，如下：

\[ \dfrac{\begin{aligned} &\Gamma \mapsto \text{t}_1: \text{T}_1 \quad \text{T}_1 = \text{Bot} \\ &\Gamma \mapsto \text{t}_2: \text{T}_2 \quad \Gamma \mapsto \text{t}_3: \text{T}_3 \quad \text{T}_2 \vee \text{T}_3 = \text{T} \end{aligned}}{\Gamma \mapsto \text{if } \text{t}_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3: \text{T}} \qquad (\text{TA-IFBOT}) \]

或者可以仿照TA-APP，要求条件项的类型为\( \text{Bool} \)的子类型，然后利用SA-BOT这个算法性子类型规则，这种情况下旧的TA-IF规则就不需要了，直接去掉，如下：

\[ \dfrac{\begin{aligned} &\Gamma \mapsto \text{t}_1: \text{T}_1 \quad \mapsto \text{T}_1 <: \text{Bool} \\ &\Gamma \mapsto \text{t}_2: \text{T}_2 \quad \Gamma \mapsto \text{t}_3: \text{T}_3 \quad \text{T}_2 \vee \text{T}_3 = \text{T} \end{aligned}}{\Gamma \mapsto \text{if } \text{t}_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3: \text{T}} \qquad (\text{TA-IF}) \]

更新于 2023-01-07
 数学, 类型理论
返回 | 主页