OSFVA
所有文章 标签
OSFVA

目录

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

CloseToZero
   约 11135 字   预计阅读 23 分钟 

第15章

章节15.2

练习15.2.1

题目：

Draw a derivation showing that \( \{ \text{x}: \text{Nat}, \text{y}: \text{Nat}, \text{z}: \text{Nat} \} \) is a subtype of \( \{ \text{y}: \text{Nat} \} \).

解答：

需要注意下，S-RCDWIDTH由于在形式上限制只能缺少尾部的域，我们需要先通过S-RCDPERM来更改下域的顺序。

\[ \dfrac{\dfrac{}{\{ \text{x}: \text{Nat}, \text{y}: \text{Nat}, \text{z}: \text{Nat} \} <: \{ \text{y}: \text{Nat}, \text{x}: \text{Nat}, \text{z}: \text{Nat} \}} \text{S-RCDPERM} \quad \dfrac{}{\{ \text{y}: \text{Nat}, \text{x}: \text{Nat}, \text{z}: \text{Nat} \} <: \{ \text{y}: \text{Nat} \}} \text{S-RCDWIDTH} }{\{ \text{x}: \text{Nat}, \text{y}: \text{Nat}, \text{z}: \text{Nat} \} <: \{ \text{y}: \text{Nat} \}} \text{S-TRANS} \]

练习15.2.2

题目：

Let us verify that the example at the beginning of the chapter now typechecks. Using the following abbreviations to avoid running off the edge of the page,

\[ \begin{aligned} \text{Rx} &\stackrel{\text{def}}{=} \{ \text{x}: \text{Nat} \} \\ \text{Rxy} &\stackrel{\text{def}}{=} \{ \text{x}: \text{Nat}, \text{y}: \text{Nat} \} \\ \text{f} &\stackrel{\text{def}}{=} \lambda \text{r}: \text{Rx} \text{. } \text{r.x} \\ \text{xy} &\stackrel{\text{def}}{=} \{ \text{x} = 0, \text{y} = 1 \} \end{aligned} \]

and assuming the usual typing rules for numeric constants, we can construct a derivation for the typing statement \( \vdash \text{f xy}: \text{Nat} \) as follows:

\[ \dfrac{\dfrac{\vdots}{\vdash \text{f}: \text{Rx} \to \text{Nat}} \quad \dfrac{\dfrac{\dfrac{}{\vdash 0: \text{Nat}} \quad \dfrac{}{\vdash 1: \text{Nat}}}{ \vdash \text{xy}: \text{Rxy}} \text{T-RCD} \quad \dfrac{}{\text{Rxy} <: \text{Rx}} \text{S-RCDWIDTH}}{ \vdash \text{xy}: \text{Rx}} \text{T-SUB}}{ \vdash \text{f xy}: \text{Nat}} \text{T-APP} \]

Is this the only derivation of the statement \( \vdash \text{f xy}: \text{Nat} \)?

解答：

明显不是，举个例子，我们可以用S-REFL和T-SUB无限拓展上述推导，简单的例子如下：

\[ \dfrac{\dfrac{\vdots}{\vdash \text{f}: \text{Rx} \to \text{Nat}} \quad \dfrac{\dfrac{\dfrac{\dfrac{}{\vdash 0: \text{Nat}} \quad \dfrac{}{\vdash 1: \text{Nat}}}{ \vdash \text{xy}: \text{Rxy}} \text{T-RCD} \quad \dfrac{}{\text{Rxy} <: \text{Rx}} \text{S-RCDWIDTH}}{ \vdash \text{xy}: \text{Rx}} \text{T-SUB} \quad \dfrac{}{\text{Rx} <: \text{Rx}} \text{S-REFL}}{ \vdash \text{xy}: \text{Rx}} \text{T-SUB}}{ \vdash \text{f xy}: \text{Nat}} \text{T-APP} \]

同理，我们也可以加上对S-TRANS的使用，用S-REFL、S-TRANS和T-SUB无限拓展上述推导，这里就不举例子了。

练习15.2.3

题目：

  1. How many different supertypes does \( \{ \text{a}: \text{Top}, \text{b}: \text{Top} \} \) have?
  2. Can you find an infinite descending chain in the subtype relation—that is, an infinite sequence of types \( \text{S}_0, \text{S}_1 \), etc. such that each \( \text{S}_{i + 1} \) is a subtype of \( \text{S}_i \)?
  3. What about an infinite ascending chain?

解答：

解答1：

一共6个，如下：

  1. \( \{ \text{a}: \text{Top}, \text{b}: \text{Top} \} \)
  2. \( \{ \text{b}: \text{Top}, \text{a}: \text{Top} \} \)
  3. \( \{ \text{a}: \text{Top} \} \)
  4. \( \{ \text{b}: \text{Top} \} \)
  5. \( \{ \} \)
  6. \( \text{Top} \)

解答2：

由于没有要求是proper subtype，因此最简单的就是一直用S-REFL。

不trivial一点的，就是我们可以一直拓展record，增加新域，如下：

  1. \( \text{S}_0 = \{ \} \)
  2. \( \text{S}_1 = \{ \text{a}: \text{Top} \} \)
  3. \( \text{S}_2 = \{ \text{a}: \text{Top}, \text{b}: \text{Top} \} \)
  4. …

解答3：

由于没有要求是proper supertype，因此最简单的同2，也是一直用S-REFL。

至于不trivial的，如果仿照2，我们会想一直删除record的某个域，但是由于域的数量是有限的，一直删，最终会变成\( \{ \} \)，无法再继续，故这样是不行的。不过可以利用S-ARROW的逆变（contravariant）特性，配合2中定义的\( S_i \)，如下：

  1. \( \text{T}_0 = \text{S}_0 \to \text{Top} \)
  2. \( \text{T}_1 = \text{S}_1 \to \text{Top} \)
  3. \( \text{T}_2 = \text{S}_2 \to \text{Top} \)
  4. …

练习15.2.4

题目：

  1. Is there a type that is a subtype of every other type?
  2. Is there an arrow type that is a supertype of every other arrow type?

解答：

解答1：

不存在，首先，该类型肯定不能是\( \text{Top} \)，因为\( \text{Top} \)不是\( \{ \} \)的subtype，排除\( \text{Top} \)后，该类型只能是record类型或函数类型了，如果它是record类型，则没有规则使得record类型是函数类型的subtype，特别的，它不是\( \lambda \text{x}: \text{Top. } \text{x} \)的subtype，函数类型同理，也会产生矛盾。综上，满足条件的类型不存在。

解答2：

不存在。

假设该类型存在，记为\( \text{T} = \text{T}_1 \to \text{T}_2 \)，则由于\( \text{T}_1 \)是所有函数类型的supertype，这意味着所有函数类型都可以替代它，也就意味着它的参数类型必须有最严格的要求，可得\( \text{T}_1 \)必须是所有类型的subtype，然而由1的讨论可得，\( \text{T}_1 \)不存在，进而\( \text{T} \)不存在。

练习15.2.5

题目：

Suppose we extend the calculus with the product type constructor \( \text{T}_1 \times \text{T}_2 \) described in \( \S 11.6 \). It is natural to add a subtyping rule

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

corresponding to S-RCDDEPTH for records. Would it be a good idea to add a width subtyping rule for products

\[ \text{T}_1 \times \text{T}_2 <: \text{T}_1 \qquad (\text{S-PRODWIDTH}) \]

as well?

解答：

不是个好主意，假设我们拓展当前系统以包含自然数和布尔，则如果加上S-PRODWIDTH，那么\( \text{succ } (0, \text{true}) \)将是类型良好的，但是\( \text{succ } (0, \text{true}) \)是个停滞项，无法进一步求值，这违反了PROGRESS定理。如果我们拓展系统以支持coercion语义，那么系统就允许插入额外的类型转换语句，将\( (0, \text{true}) \)转化成\( 0 \)，再丢给\( \text{succ} \)，类似：\( \text{succ } (0, \text{true}) \rightarrow \text{succ } (\text{Nat})(0, \text{true}) \rightarrow \text{succ } 0 \)，此时就没有问题了，但是引入coercion语义可能会使得subtype检查算法不好实现。

章节15.3

练习15.3.1

题目：

Having decided on the definition of the lambda-calculus with subtyping, we now have some work to do to verify that it makes sense—in particular, that the preservation and progress theorems of the simply typed lambda-calculus continue to hold in the presence of subtyping.

Before reading on, try to predict where difficulties might arise. In particular, suppose we had made a mistake in defining the subtype relation and included a bogus subtyping rule in addition to those above. Which properties of the system can fail? On the other hand, suppose we omit one of the subtyping rules—can any properties then break?

解答：

如果添加规则不当，则既可能违反PROGRESS定理，也可能违反PRESERVATION定理。

先举一个添加不当规则导致违反PROGRESS定理的例子，添加如下子类型规则：

\[ \{ \} <: \text{Top} \to \text{Top} \]

则令\( \text{t} = \{ \} \text{ } \{ \} \)，由上述新规则、S-TOP、T-SUB，可得\( \Gamma \vdash \text{t}: \text{Top} \)，即\( \text{t} \)是类型良好的，但\( \text{t} \)是停滞项，无法进一步求值，这违反了PROGRESS定理。

我们再举一个添加不当规则导致违反PRESERVATION定理的例子，添加如下子类型规则：

\[ \{ \text{x}: \{ \} \} <: \{ \text{x}: \text{Top} \to \text{Top} \} \]

则令\( \text{t} = (\{ \text{x} = \{ \} \}.\text{x}) \text{ } \{ \} \)，由上述新规则、T-RCD、S-TOP、T-SUB，可得\( \Gamma \vdash \text{t}: \text{Top} \)，即\( \text{t} \)是类型良好的，但\( \text{t} \rightarrow \{ \} \text{ } \{ \} \)，这里\( \{ \} \text{ } \{ \} \)非类型良好的，这违反了PRESERVATION定理。

至于移除部分子类型规则，则是无害的，因为类型规则和子类型规则是分开的，而我们在PROGRESS定理、PRESERVATION定理以及其他相关引理的证明中，用到的都是类型规则，子类型则是通过T-SUB类型规则来桥接的，而在T-SUB类型规则中，子类型关系是属于前提条件的部分，移除部分子类型规则，相当于从子类型关系中移除部分子类型对，这只会使得前提条件更难成立，进而T-SUB更少用上罢了。

练习15.3.2

题目：

Lemma [Inversion of the subtype relation]:

  1. If \( \text{S} <: \text{T}_1 \to \text{T}_2 \), then \( \text{S} \) has the form \( \text{S}_1 \to \text{S}_2 \), with \( \text{T}_1 <: \text{S}_1 \) and \( \text{S}_2 <: \text{T}_2 \).
  2. If \( \text{S} <: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \), then \( \text{S} \) has the form \( \{ \text{k}_j: \text{S}_j \ ^{j \in 1 \dots m} \} \), with at least the labels \( \{ \text{l}_i \ ^{i \in 1 \dots n} \} \)—i.e., \( \{ \text{l}_i \ ^{i \in 1 \dots n} \} \subseteq \{ \text{k}_j \ ^{j \in 1 \dots m} \} \)—and with \( \text{S}_j <: \text{T}_i \) for each common label \( \text{l}_i = \text{k}_j \).

证明：

证明1：

令\( \mathcal{D} \)为\( \text{S} <: \text{T}_1 \to \text{T}_2 \)对应的子类型推导，归纳假设命题对所有\( \mathcal{D} \)的直接子推导成立，我们要证明命题对\( \mathcal{D} \)成立：

\( \text{S} <: \text{T}_1 \to \text{T}_2 \)最后使用的规则只能是S-REFL、S-TRANS、S-ARROW，分情况讨论：

  1. 如果最后使用的规则是S-REFL，则\( \text{S} = \text{T}_1 \to \text{T}_2 \)，此时有\( \text{S}_1 = \text{T}_1, \text{S}_2 = \text{T}_2 \)，由S-REFL，可得\( \text{T}_1 <: \text{S}_1, \text{S}_2 <: \text{T}_2 \)。
  2. 如果最后使用的规则是S-TRANS，则\( \text{S} <: \text{U}, \text{U} <: \text{T}_1 \to \text{T}_2 \)，由\( \text{U} <: \text{T}_1 \to \text{T}_2 \)以及归纳假设，可得\( \text{U} = \text{U}_1 \to \text{U}_2, \text{T}_1 <: \text{U}_1, \text{U}_2 <: \text{T}_2 \)，而\( \text{S} <: \text{U} = \text{U}_1 \to \text{U}_2 \)，同理根据归纳假设，可得\( \text{S} = \text{S}_1 \to \text{S}_2, \text{U}_1 <: \text{S}_1, \text{S}_2 <: \text{U}_2 \)，最后根据S-TRANS，可得\( \text{T}_1 <: \text{S}_1, \text{S}_2 <: \text{T}_2 \)。
  3. 如果最后使用的规则是S-ARROW，则直接有\( \text{S} = \text{S}_1 \to \text{S}_2, \text{T}_1 <: \text{S}_1, \text{S}_2 <: \text{T}_2 \)。

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

证明1完毕。

证明2：

令\( \mathcal{D} \)为\( \text{S} <: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \)对应的子类型推导，归纳假设命题对所有\( \mathcal{D} \)的直接子推导成立，我们要证明命题对\( \mathcal{D} \)成立：

\( \text{S} <: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \)最后使用的规则只能是S-REFL、S-TRANS、S-RCDWIDTH、S-RCDDEPTH、S-RCDPERM，分情况讨论：

  1. 如果最后使用的规则是S-REFL，则\( \text{S} = \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \)，易得命题成立。
  2. 如果最后使用的规则是S-TRANS，则\( \text{S} <: \text{U}, \text{U} <: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \)，由\( \text{U} <: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \)以及归纳假设，可得\( \text{U} = \{ \text{u}_a: \text{U}_a \ ^{a \in 1 \dots b} \}, \{ \text{l}_i \ ^{i \in 1 \dots n} \} \subseteq \{ \text{u}_a \ ^{a \in 1 \dots b} \} \)，且\( \forall 1 \leq i \leq n, 1 \leq a \leq b \)，如果\( \text{l}_i = \text{u}_a \)，则\( \text{T}_i <: \text{U}_a \)。而\( \text{S} <: \text{U} = \{ \text{u}_a: \text{U}_a \ ^{a \in 1 \dots b} \} \)，同理根据归纳假设，可得\( \text{S} = \{ \text{k}_j: \text{S}_j \ ^{j \in 1 \dots m} \}, \{ \text{u}_a \ ^{a \in 1 \dots b} \} \subseteq \{ \text{k}_j \ ^{j \in 1 \dots m} \} \)，且\( \forall 1 \leq j \leq m, 1 \leq a \leq b \)，如果\( \text{k}_j = \text{u}_a \)，则\( \text{S}_j <: \text{U}_a \)。综合上述结论以及S-TRANS，可得\( \{ \text{l}_i \ ^{i \in 1 \dots n} \} \subseteq \{ \text{k}_j \ ^{j \in 1 \dots m} \} \)，且\( \forall 1 \leq i \leq n, 1 \leq j \leq m \)，如果\( \text{l}_i = \text{k}_j \)，则\( \text{T}_i <: \text{S}_j \)。
  3. 如果最后使用的规则是S-RCDWIDTH，则\( \text{S} = \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n + k} \} \)，易得命题成立。
  4. 如果最后使用的规则是S-RCDDEPTH，则\( \text{S} = \{ \text{l}_i: \text{S}_i \ ^{i \in 1 \dots n} \}, \forall 1 \leq i \leq n, \text{S}_i <: \text{T}_i \)，易得命题成立。
  5. 如果最后使用的规则是S-RCDPERM，则\( \text{S} = \{ \text{k}_j: \text{S}_j \ ^{j \in 1 \dots n} \} \)，其中，\( \{ \text{k}_j: \text{S}_j \ ^{j \in 1 \dots n} \} \)为\( \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \)的某个排列，可得两个类型的标签集相等以及相同标签的对应类型相等，易得命题成立。

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

证明2完毕。

练习15.3.6

题目：

Lemma [Canonical Forms]:

  1. If \( \text{v} \) is a closed value of type \( \text{T}_1 \to \text{T}_2 \), then \( \text{v} \) has the form \( \lambda \text{x}: \text{S}_1 \text{. } \text{t}_2 \).
  2. If \( \text{v} \) is a closed value of type \( \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \), then \( \text{v} \) has the form \( \{ \text{k}_j = \text{v}_j \ ^{j \in 1 \dots m} \} \), with \( \{ \text{l}_i \ ^{i \in 1 \dots n} \} \subseteq \{ \text{k}_j \ ^{j \in 1 \dots m} \} \).

证明：

证明1：

令\( \mathcal{D} \)为\( \Gamma \vdash \text{v}: \text{T}_1 \to \text{T}_2 \)对应的类型推导，归纳假设命题对所有\( \mathcal{D} \)的直接子推导成立，我们要证明命题对\( \mathcal{D} \)成立：

\( \Gamma \vdash \text{v}: \text{T}_1 \to \text{T}_2 \)最后使用的规则只能是T-ABS或T-SUB，分情况讨论：

  1. 如果最后使用的规则是T-ABS，则\( \text{S}_1 = \text{T}_1, \text{v} = \lambda \text{x}: \text{S}_1 \text{. } \text{t}_2 \)。
  2. 如果最后使用的规则是T-SUB，则\( \vdash \text{v}: \text{U}, \text{U} <: \text{T}_1 \to \text{T}_2 \)，由\( \text{U} <: \text{T}_1 \to \text{T}_2 \)以及引理15.3.2的1，可得\( \text{U} = \text{U}_1 \to \text{U}_2 \)，由\( \vdash \text{v}: (\text{U} = \text{U}_1 \to \text{U}_2) \)以及归纳假设，可得\( \text{v} = \lambda \text{x}: \text{S}_1 \text{. } \text{t}_2 \)。

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

证明1完毕。

证明2：

令\( \mathcal{D} \)为\( \Gamma \vdash \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \)对应的类型推导，归纳假设命题对所有\( \mathcal{D} \)的直接子推导成立，我们要证明命题对\( \mathcal{D} \)成立：

\( \Gamma \vdash \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \)最后使用的规则只能是T-RCD、T-SUB，分情况讨论：

  1. 如果最后使用的规则是T-RCD，则\( m = n, \forall 1 \leq i \leq n, \text{l}_i = \text{k}_i, \text{v} = \{ \text{k}_j = \text{v}_j \ ^{j \in 1 \dots m} \} \)，易检验命题成立。
  2. 如果最后使用的规则是T-SUB，则\( \Gamma \vdash \text{v}: \text{U}, \text{U} <: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \)，由\( \text{U} <: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \)以及引理15.3.2的2，可得\( \text{U} = \{ \text{u}_a: \text{U}_a \ ^{a \in 1 \dots b} \}, \{ \text{l}_i \ ^{i \in 1 \dots n} \} \subseteq \{ \text{u}_a \ ^{a \in 1 \dots b} \} \)，由\( \Gamma \vdash \text{v}: (\text{U} = \{ \text{u}_a: \text{U}_a \ ^{a \in 1 \dots b} \}) \)以及归纳假设，可得\( \text{v} = \{ \text{k}_j: \text{v}_j \ ^{j \in 1 \dots m} \}, \{ \text{u}_a \ ^{a \in 1 \dots b} \} \subseteq \{ \text{k}_j \ ^{j \in 1 \dots m} \} \)，再加上前面的\( \{ \text{l}_i \ ^{i \in 1 \dots n} \} \subseteq \{ \text{u}_a \ ^{a \in 1 \dots b} \} \)，可得\( \{ \text{l}_i \ ^{i \in 1 \dots n} \} \subseteq \{ \text{k}_j \ ^{j \in 1 \dots m} \} \)，命题成立。

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

证明2完毕。

章节15.5

练习15.5.1

题目：

A down-cast, on the other hand, allows us to assign types to terms that the typechecker cannot derive statically. To allow down-casts, we make a somewhat surprising change to the typing rule for as:

\[ \dfrac{\Gamma \vdash \text{t}_1: \text{S}}{\Gamma \vdash \text{t}_1 \text{ as } \text{T}: \text{T}} \qquad (\text{T-DOWNCAST}) \]

That is, we check that \( \text{t}_1 \) is well typed (i.e., that it has some type \( \text{S} \)) and then assign it type \( \text{T} \), without making any demand about the relation between \( \text{S} \) and \( \text{T} \). For example, using down-casting we can write a function \( \text{f} \) that takes any argument whatsoever, casts it down to a record with an a field containing a number, and returns this number:

\[ \text{f} = \lambda \text{x}: \text{Top. } (\text{x} \text{ as } \{ \text{a}: \text{Nat} \}).\text{a}; \]

In effect, the programmer is saying to the typechecker, “I know (for reasons that are too complex to explain in terms of the typing rules) that \( \text{f} \) will always be applied to record arguments with numeric a fields; I want you to trust me on this one.”

Of course, blindly trusting such assertions will have a disastrous effect on the safety of our language: if the programmer somehow makes a mistake and applies \( \text{f} \) to a record that does not contain an a field, the results might (depending on the details of the compiler) be completely arbitrary! Instead, our motto should be “trust, but verify.” At compile time, the typechecker simply accepts the type given in the down-cast. However, it inserts a check that, at run time, will verify that the actual value does indeed have the type claimed. In other words, the evaluation rule for ascriptions should not just discard the annotation, as our original evaluation rule for ascriptions did,

\[ \text{v}_1 \text{ as } \text{T} \rightarrow \text{v}_1 \qquad (\text{E-ASCRIBE}) \]

but should first compare the actual (run-time) type of the value with the declared type:

\[ \dfrac{\vdash \text{v}_1: \text{T}}{\text{v}_1 \text{ as } \text{T} \rightarrow \text{v}_1} \qquad (\text{E-DOWNCAST}) \]

For example, if we apply the function \( \text{f} \) above to the argument \( \{ \text{a} = 5, \text{b} = \text{true} \} \), then this rule will check (successfully) that \( \vdash \{ \text{a} = 5, \text{b} = \text{true} \}: \{ \text{a}: \text{Nat} \} \). On the other hand, if we apply \( \text{f} \) to \( \{ \text{b} = \text{true} \} \), then the E-DOWNCAST rule will not apply and evaluation will get stuck at this point. This run-time check recovers the type preservation property, prove this.

附注：

有了T-DOWNCAST、E-DOWNCAST规则，就不需要T-UPCAST、T-ASCRIBE等规则了，不过还需要E-ASCRIBE1规则。

证明：

PRESERVATION定理的证明中需要用到引理15.3.3以及引理15.3.4，而引理15.3.3的证明需要用到引理15.3.2，不过引理15.3.2、引理15.3.3的证明不涉及\( \text{t}_1 \text{ as } \text{T} \)形式的项，也不涉及T-DOWNCAST，故证明不需要修改。至于引理15.3.4的证明，则需要额外考虑T-DOWNCAST情况了，下面，我们证明引理15.3.4，即：如果\( \Gamma, \text{x}: \text{S} \vdash \text{t}: \text{T} \)且\( \Gamma \vdash \text{s}: \text{S} \)，则\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}: \text{T} \)。

证明引理15.3.4：

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

  1. 如果最后使用的规则是T-VAR，则\( \text{t} = \text{y}, \text{y}: \text{T} \in \Gamma, \text{x}: \text{S} \)：
    1. 如果\( \text{y} = \text{x} \)，则由\( \text{y}: \text{T} \in \Gamma, \text{x}: \text{S} \)，可得\( \text{T} = \text{S} \)，而\( [\text{x} \mapsto \text{s}]\text{t} = \text{s} \)，加上\( \Gamma \vdash \text{s}: \text{S} \)，可得\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}: \text{S} \)，即\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}: \text{T} \)。
    2. 如果\( \text{y} \neq \text{x} \)，则由\( \text{y}: \text{T} \in \Gamma, \text{x}: \text{S} \)，可得\( \text{y}: \text{T} \in \Gamma \)，进而由T-VAR，可得\( \Gamma \vdash \text{t}: \text{T} \)，而\( [\text{x} \mapsto \text{s}]\text{t} = \text{t} \)，有\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}: \text{T} \)。
  2. 如果最后使用的规则是T-ABS，则\( \text{t} = \lambda \text{y}: \text{T}_1 \text{. } \text{t}_2, \text{T} = \text{T}_1 \to \text{T}_2, \Gamma, \text{x}: \text{S}, \text{y}: \text{T}_1 \vdash \text{t}_2: \text{T}_2, [\text{x} \mapsto \text{s}]\text{t} = \lambda \text{y}: \text{T}_1 \text{. } [\text{x} \mapsto \text{s}]\text{t}_2 \)，由\( \Gamma, \text{x}: \text{S}, \text{y}: \text{T}_1 \vdash \text{t}_2: \text{T}_2 \)，可得\( \Gamma, \text{y}: \text{T}_1, \text{x}: \text{S} \vdash \text{t}_2: \text{T}_2 \)，进而由\( \Gamma \vdash \text{s}: \text{S} \)以及归纳假设，可得\( \Gamma, \text{y}: \text{T}_1 \vdash [\text{x} \mapsto \text{s}]\text{t}_2: \text{T}_2 \)，进而根据T-ABS，可得\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}: \text{T} \)。
  3. 如果最后使用的规则是T-APP，则\( \text{t} = \text{t}_1 \text{ } \text{t}_2, \Gamma, \text{x}: \text{S} \vdash \text{t}_1: \text{T}_1 \to \text{T}, \Gamma, \text{x}: \text{S} \vdash \text{t}_2: \text{T}_1, [\text{x} \mapsto \text{s}]\text{t} = [\text{x} \mapsto \text{s}]\text{t}_1 \text{ } [\text{x} \mapsto \text{s}]\text{t}_2 \)，由\( \Gamma, \text{x}: \text{S} \vdash \text{t}_1: \text{T}_1 \to \text{T}, \Gamma \vdash \text{s}: \text{S} \)以及归纳假设，可得\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}_1: \text{T}_1 \to \text{T} \)，同理可得\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}_2: \text{T}_1 \)，进而根据T-APP，可得\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}: \text{T} \)。
  4. 如果使用的规则是T-RCD，则\( \text{t} = \{ \text{l}_i = \text{t}_i \ ^{i \in 1 \dots n} \}, \forall 1 \leq i \leq n, \Gamma, \text{x}: \text{S} \vdash \text{t}_i: \text{T}_i, \text{T} = \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \}, [\text{x} \mapsto \text{s}]\text{t} = \{ \text{l}_i = [\text{x} \mapsto \text{s}]\text{t}_i \ ^{i \in 1 \dots n} \} \)，由\( \forall 1 \leq i \leq n, \Gamma, \text{x}: \text{S} \vdash \text{t}_i: \text{T}_i, \Gamma \vdash \text{s}: \text{S} \)以及归纳假设，可得\( \forall 1 \leq i \leq n, \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}_i: \text{T}_i \)，进而根据T-RCD，可得\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}: \text{T} \)。
  5. 如果使用的规则是T-PROJ，则\( \text{t} = \text{t}_1.\text{l}_j, 1 \leq j \leq n, \Gamma, \text{x}: \text{S} \vdash \text{t}_1: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \}, \text{T} = \text{T}_j, [\text{x} \mapsto \text{s}]\text{t} = ([\text{x} \mapsto \text{s}]\text{t}_1).\text{l}_j \)，由\( \Gamma, \text{x}: \text{S} \vdash \text{t}_1: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \}, \Gamma \vdash \text{s}: \text{S} \)以及归纳假设，可得\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}_1: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \)，进而根据T-PROJ，可得\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}: \text{T} \)。
  6. 如果使用的规则是T-SUB，则\( \Gamma, \text{x}: \text{S} \vdash \text{t}: \text{U}, \text{U} <: \text{T} \)，由\( \Gamma, \text{x}: \text{S} \vdash \text{t}: \text{U}, \Gamma \vdash \text{s}: \text{S} \)以及归纳假设，可得\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}: \text{U} \)，进而由T-SUB，可得\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}: \text{T} \)。
  7. 如果使用的规则是T-DOWNCAST，则\( \Gamma, \text{x}: \text{S} \vdash \text{t}_1: \text{U}, \text{t} = \text{t}_1 \text{ as } \text{T}, [\text{x} \mapsto \text{s}]\text{t} = [\text{x} \mapsto \text{s}]\text{t}_1 \text{ as } \text{T} \)，由\( \Gamma, \text{x}: \text{S} \vdash \text{t}_1: \text{U}, \Gamma \vdash \text{s}: \text{S} \)以及归纳假设，可得\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}_1: \text{U} \)，进而由T-DOWNCAST，可得\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}: \text{T} \)。

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

证明引理15.3.4完毕。

现在，我们可以证明PRESERVATION定理了，即：如果\( \Gamma \vdash \text{t}: \text{T} \)且\( \text{t} \rightarrow \text{t}' \)，则\( \Gamma \vdash \text{t}': \text{T} \)。基本和定理15.3.5的证明一样，只不过要增加对T-DOWNCAST情况的讨论。

证明PRESERVATION定理：

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

  1. 如果最后使用的规则是T-VAR，则\( \text{t} = \text{x} \)，此时\( \text{t} \)为范式，这和\( \text{t} \rightarrow \text{t}' \)矛盾。
  2. 如果最后使用的规则是T-ABS，则\( \text{t} = \lambda \text{x}: \text{T}_1 \text{. } \text{t}_2 \)，此时\( \text{t} \)为范式，这和\( \text{t} \rightarrow \text{t}' \)矛盾。
  3. 如果最后使用的规则是T-APP，则\( \text{t} = \text{t}_1 \text{ } \text{t}_2, \Gamma \vdash \text{t}_1: \text{T}_1 \to \text{T}, \Gamma \vdash \text{t}_2: \text{T}_1 \)，此时\( \text{t} \rightarrow \text{t}' \)最后使用的规则只能是E-APP1、E-APP2、E-APPABS，分情况讨论：
    1. 如果使用的规则是E-APP1，则\( \text{t}_1 \rightarrow \text{t}'_1, \text{t}' = \text{t}'_1 \text{t}_2 \)，由\( \Gamma \vdash \text{t}_1: \text{T}_1 \to \text{T}, \text{t}_1 \rightarrow \text{t}'_1 \)以及归纳假设，可得\( \Gamma \vdash \text{t}'_1: \text{T}_1 \to \text{T} \)，进而根据T-APP，可得\( \Gamma \vdash \text{t}': \text{T} \)。
    2. 如果使用的规则是E-APP2，则\( \text{t}_2 \rightarrow \text{t}'_2, \text{t}' = \text{t}_1 \text{t}'_2 \)，由\( \Gamma \vdash \text{t}_2: \text{T}_1, \text{t}_2 \rightarrow \text{t}'_2 \)以及归纳假设，可得\( \Gamma \vdash \text{t}'_2: \text{T}_1 \)，进而根据T-APP，可得\( \Gamma \vdash \text{t}': \text{T} \)。
    3. 如果使用的规则E-APPABS，则\( \text{t} = \lambda \text{x}: \text{S}_1 \text{. } \text{t}_{11}, \text{t}_2 = \text{v}_2, \text{t}' = [\text{x} \mapsto \text{v}_2]\text{t}_{11} \)，根据引理15.3.3的1，可得\( \text{T}_1 <: \text{S}_1, \Gamma, \text{x}: \text{S}_1 \vdash \text{t}_{11}: \text{T} \)，由\( \Gamma \vdash \text{t}_2: \text{T}_1, \text{T}_1 <: \text{S}_1 \)以及T-SUB，可得\( \Gamma \vdash \text{t}_2: \text{S}_1 \)，进而由\( \Gamma, \text{x}: \text{S}_1 \vdash \text{t}_{11}: \text{T} \)以及引理15.3.4，可得\( \Gamma \vdash \text{t}': \text{T} \)。
  4. 如果使用的规则是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} \} \)，此时\( \text{t} \rightarrow \text{t}' \)最后使用的规则只能是E-RCD，可得\( \text{t} = \{ \text{l}_i = \text{v}_i \ ^{i \in 1 \dots j-1}, \text{l}_j = \text{t}_j, \text{l}_k = \text{t}_k \ ^{k \in j+1 \dots n} \}, \text{t}_j \rightarrow \text{t}'_j, \text{t}' = \{ \text{l}_i = \text{v}_i \ ^{i \in 1 \dots j-1}, \text{l}_j = \text{t}'_j, \text{l}_k = \text{t}_k \ ^{k \in j+1 \dots n} \} \)，由\( \Gamma \vdash \text{t}_j: \text{T}_j, \text{t}_j \rightarrow \text{t}'_j \)以及归纳假设，可得\( \Gamma \vdash \text{t}'_j: \text{T}_j \)，进而由T-RCD，可得\( \Gamma \vdash \text{t}': \text{T} \)。
  5. 如果使用的规则是T-PROJ，则\( \text{t} = \text{t}_1.\text{l}_j, 1 \leq j \leq n, \Gamma \vdash \text{t}_1: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \}, \text{T} = \text{T}_j \)，此时\( \text{t} \rightarrow \text{t}' \)最后使用的规则只能是E-PROJ、E-PROJRCD，分情况讨论：
    1. 如果最后使用的规则是E-PROJ，则\( \text{t}_1 \rightarrow \text{t}'_1, \text{t}' = \text{t}'.\text{l}_j \)，则由\( \Gamma \vdash \text{t}_1: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \}, \text{t}_1 \rightarrow \text{t}'_1 \)以及归纳假设，可得\( \Gamma \vdash \text{t}'_1: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \)，进而由T-PROJ，可得\( \Gamma \vdash \text{t}': \text{T} \)。
    2. 如果最后使用的规则是E-PROJRCD，则\( \text{t}_1 = \{ \text{k}_a = \text{v}_a \ ^{a \in 1 \dots m} \}, \exists 1 \leq b \leq m, \text{l}_j = \text{k}_b, \text{t}' = \text{v}_b \)，根据引理15.3.3的2，可得\( \Gamma \vdash \text{t}': \text{T} \)。
  6. 如果使用的规则是T-SUB，则\( \Gamma \vdash \text{t}: \text{S}, \text{S} <: \text{T} \)，由\( \Gamma \vdash \text{t}: \text{S}, \text{t} \rightarrow \text{t}' \)以及归纳假设，可得\( \Gamma \vdash \text{t}': \text{S} \)，进而根据T-SUB，可得\( \Gamma \vdash \text{t}': \text{T} \)。
  7. 如果使用的规则是T-DOWNCAST，则\( \Gamma \vdash \text{t}_1: \text{S}, \text{t} = \text{t}_1 \text{ as } \text{T} \)，此时\( \text{t} \rightarrow \text{t}' \)最后使用的规则只能是E-ASCRIBE1、E-DOWNCAST，分情况讨论：
    1. 如果最后使用的规则是E-ASCRIBE1，则\( \text{t}_1 \rightarrow \text{t}'_1, \text{t}' = \text{t}'_1 \text{ as } \text{T} \)，由\( \Gamma \vdash \text{t}_1: \text{S}, \text{t}_1 \rightarrow \text{t}'_1 \)以及归纳假设，可得\( \Gamma \vdash \text{t}'_1: \text{S} \)，进而由T-DOWNCAST，可得\( \Gamma \vdash \text{t}': \text{T} \)。
    2. 如果最后使用的规则是E-DOWNCAST，则\( \text{t}_1 = \text{v}_1, \Gamma \vdash \text{v}_1: \text{T}, \text{t}' = \text{v}_1 \)，直接有\( \Gamma \vdash \text{t}': \text{T} \)。

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

证明PRESERVATION定理完毕。

练习15.5.2

题目：

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

  1. Write a short program that will fail with a run-time type error (i.e., its evaluation will get stuck) if the first premise of S-REF is dropped.
  2. Write another program that will fail if the second premise is dropped.

解答：

解答1：

\[ \begin{aligned} \text{T}_1 &= \{ \text{a}: \text{Top} \} \\ \text{S}_1 &= \{ \} \\ \text{t} &= (\lambda \text{x}: \text{Ref } \text{T}_1 \text{. } (!\text{x}).\text{a}) \text{ } (\text{ref } \{ \}) \end{aligned} \]

解答2：

\[ \begin{aligned} \text{T}_1 &= \{ \} \\ \text{S}_1 &= \{ \text{a}: \text{Top} \} \\ \text{t} &= (\lambda \text{x}: \text{Ref } \text{S}_1 \text{. } ((\lambda \text{y}: \text{Unit. } (!\text{x}).\text{a}) \text{ } ((\lambda \text{z}: \text{Ref } \text{T}_1 \text{. } \text{z} := \{ \} ) \text{ } \text{x})) \text{ } (\text{ref } \{ \text{a} = \{ \} \}) \end{aligned} \]

练习15.5.3

题目：

Write a short Java program involving arrays that type-checks but fails (by raising an \( \text{ArrayStoreException} \)) at run time.

解答：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10

class A {
    static void test(Object[] array) {
        array[0] = new Object();
    }
    public static void main(String[] args) {
        String[] strs = new String[1];
        strs[0] = "abc";
        test(strs);
    }
}

运行结果：

1
2
3

Exception in thread "main" java.lang.ArrayStoreException: java.lang.Object
	at A.test(A.java:6)
	at A.main(A.java:11)

章节15.6

练习15.6.3

题目：

Modify the translations above to use simply typed lambda-calculus with tuples (instead of records) as a target language. Check that Theorem 15.6.2 still holds.

解答：

我们需要将record翻译成tuple，具体的，给定\( \{ \text{l}_i = \text{t}_i \ ^{i \in 1 \dots n} \} \)，类似C、C++、Rust等语言，我们一律假定第\( i \)个域的项\( \text{t}_i \)位于record首地址偏移\( i \)的位置（不考虑项的大小），用tuple的话来说，就是\( \text{t}_i \)为第\( i \)个分量，也就是我们得把\( \{ \text{l}_i = \text{t}_i \ ^{i \in 1 \dots n} \} \)翻译成\( \{ \text{t}_i \ ^{i \in 1 \dots n} \} \) （注意：本书tuple不是用圆括号作为外围分界符的，而是用大括号）。

类型翻译如下：

\[ \begin{aligned} \llbracket \text{Top} \rrbracket &= \text{Unit} \\ \llbracket \text{T}_1 \to \text{T}_2 \rrbracket &= \llbracket \text{T}_1 \rrbracket \to \llbracket \text{T}_2 \rrbracket \\ \llbracket \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \rrbracket &= \{ \llbracket \text{T}_i \rrbracket \ ^{i \in 1 \dots n} \} \end{aligned} \]

接下来我们考虑子类型推导的翻译，需要注意几点：

  1. 根据类型翻译，可得record翻译后必为tuple，下面规则定义时，会利用到这点。
  2. 给定\( \{ \text{k}_j: \text{S}_j \ ^{j \in 1 \dots n} \} \) 为\( \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \)的排列，由于标签都是不重复的，因此\( \forall 1 \leq i \leq n, \exists \text{唯一的} 1 \leq j_i \leq n, \text{l}_i = \text{k}_{j_i} \)，为了简洁，下面规则定义时，我们直接用到\( \text{j}_i \)，而不会显式写出\( \text{j}_i \)的定义（特别注意，我们的翻译是以完整的子类型推导作为参数的，因此可以拿到\( \text{j}_i \)）。

子类型推导翻译如下：

\[ \begin{aligned} \llbracket \dfrac{}{\text{T} <: \text{T}}(\text{S-REFL}) \rrbracket &= \lambda \text{x}: \llbracket \text{T} \rrbracket \text{. } \text{x} \\ \llbracket \dfrac{}{\text{S} <: \text{Top}}(\text{S-TOP}) \rrbracket &= \lambda \text{x}: \llbracket \text{S} \rrbracket \text{. } \text{unit} \\ \llbracket \dfrac{\mathcal{C}_1 :: \text{T}_1 <: \text{S}_1 \quad \mathcal{C}_2 :: \text{S}_2 <: \text{T}_2}{ \text{S}_1 \to \text{S}_2 <: \text{T}_1 \to \text{T}_2}(\text{S-ARROW}) \rrbracket &= \lambda \text{f}: \llbracket \text{S}_1 \to \text{S}_2 \rrbracket \text{. } \lambda \text{x}: \llbracket \text{T}_1 \rrbracket \text{. } \llbracket \mathcal{C}_2 \rrbracket (\text{f}(\llbracket \mathcal{C}_1 \rrbracket \text{x})) \\ \llbracket \dfrac{}{\{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n+k} \} <: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \}}(\text{S-RCDWIDTH}) \rrbracket &= \lambda \text{t}: \llbracket \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n+k} \} \rrbracket \text{. } \{ \text{t}.\text{i} \ ^{i \in 1 \dots n} \} \\ \llbracket \dfrac{\forall 1 \leq i \leq n, \mathcal{C}_i :: \text{S}_i <: \text{T}_i}{ \{ \text{l}_i: \text{S}_i \ ^{i \in 1 \dots n} \} <: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \}}(\text{S-RCDDEPTH}) \rrbracket &= \lambda \text{t}: \llbracket \{ \text{l}_i: \text{S}_i \ ^{i \in 1 \dots n} \} \rrbracket \text{. } \{ \llbracket \mathcal{C}_i \rrbracket (\text{t}.\text{i}) \ ^{i \in 1 \dots n} \} \\ \llbracket \dfrac{\{ \text{k}_j: \text{S}_j \ ^{j \in 1 \dots n} \} \text{ perm. of } \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \}}{ \{ \text{k}_j: \text{S}_j \ ^{j \in 1 \dots n} \} <: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \}}(\text{S-RCDPERM}) \rrbracket &= \lambda \text{t}: \llbracket \{ \text{k}_j: \text{S}_j \ ^{j \in 1 \dots n} \} \rrbracket \text{. } \{ \text{t}.\text{j}_i \ ^{i \in 1 \dots n} \} \end{aligned} \]

最后考虑类型推导的翻译，和子类型推导的翻译差不多，完整的类型推导翻译如下：

\[ \begin{aligned} \llbracket \dfrac{\text{x}: \text{T} \in \Gamma}{ \Gamma \vdash \text{x}: \text{T}}(\text{T-VAR}) \rrbracket &= \text{x} \\ \llbracket \dfrac{\mathcal{D}_1 :: \Gamma, \text{x}: \text{T}_1 \vdash \text{t}_2: \text{T}_2}{ \Gamma \vdash \lambda \text{x}: \text{T}_1 \text{. } \text{t}_2: \text{T}_1 \to \text{T}_2}(\text{T-ABS}) \rrbracket &= \lambda \text{x}: \llbracket \text{T}_1 \rrbracket \text{. } \llbracket \mathcal{D}_1 \rrbracket \\ \llbracket \dfrac{\mathcal{D}_1 :: \Gamma \vdash \text{t}_1: \text{T}_2 \to \text{T} \quad \mathcal{D}_2 :: \Gamma \vdash \text{t}_2: \text{T}_2}{ \Gamma \vdash \text{t}_1 \text{ } \text{t}_2: \text{T}}(\text{T-APP}) \rrbracket &= \llbracket \mathcal{D}_1 \rrbracket \text{ } \llbracket \mathcal{D}_2 \rrbracket \\ \llbracket \dfrac{\forall 1 \leq i \leq n, \mathcal{D}_i :: \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} \}}(\text{T-RCD}) \rrbracket &= \{ \llbracket \mathcal{D}_i \rrbracket \ ^{i \in 1 \dots n} \} \\ \llbracket \dfrac{\mathcal{D}_1 :: \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}(\text{T-PROJ}) \rrbracket &= \llbracket \mathcal{D}_1 \rrbracket.\text{j} \\ \llbracket \dfrac{\mathcal{D}_1 :: \Gamma \vdash \text{t}: \text{S} \quad \mathcal{C}_1 :: \text{S} <: \text{T}}{ \Gamma \vdash \text{t}: \text{T}}(\text{T-SUB}) \rrbracket &= \llbracket \mathcal{C}_1 \rrbracket \text{ } \llbracket \mathcal{D}_1 \rrbracket \end{aligned} \]

以上就是所有翻译的定义了，现在，我们去证明定理15.6.2仍然成立，不过定理15.6.2的证明需要用到引理15.6.1，故我们先证明引理15.6.1仍然成立。

引理15.6.1的内容：

If \( \mathcal{C} :: \text{S} <: \text{T} \), then \( \vdash \llbracket \mathcal{C} \rrbracket : \llbracket \text{S} \rrbracket \to \llbracket \text{T} \rrbracket \).

证明引理15.6.1：

归纳假设命题对\( \mathcal{C} \)的直接子推导成立，我们证明命题对\( \mathcal{C} \)成立，对\( \mathcal{C} \)最后使用的子类型规则进行分情况讨论：

  1. 如果最后使用的规则是S-REFL，则\( \text{S} = \text{T}, \llbracket \mathcal{C} \rrbracket = \lambda \text{x}: \llbracket \text{T} \rrbracket \text{. } \text{x} \)，明显有\( \vdash \llbracket \mathcal{C} \rrbracket : \llbracket \text{T} \rrbracket \to \llbracket \text{T} \rrbracket \)，即\( \vdash \llbracket \mathcal{C} \rrbracket : \llbracket \text{S} \rrbracket \to \llbracket \text{T} \rrbracket \)。
  2. 如果最后使用的规则是S-TOP，则\( \text{T} = \text{Top}, \llbracket \mathcal{C} \rrbracket = \lambda \text{x}: \llbracket \text{S} \rrbracket \text{. } \text{unit} \)，而\( \llbracket \text{T} \rrbracket = \llbracket \text{Top} \rrbracket = \text{Unit} \)，可得\( \vdash \llbracket \mathcal{C} \rrbracket : \llbracket \text{S} \rrbracket \to \llbracket \text{Unit} \rrbracket \)，即\( \vdash \llbracket \mathcal{C} \rrbracket : \llbracket \text{S} \rrbracket \to \llbracket \text{T} \rrbracket \)。
  3. 如果最后使用的规则是S-ARROW，则\( \text{S} = \text{S}_1 \to \text{S}_2, \text{T} = \text{T}_1 \to \text{T}_2, \mathcal{C}_1 :: \text{T}_1 <: \text{S}_1, \mathcal{C}_2 :: \text{S}_2 <: \text{T}_2, \llbracket \mathcal{C} \rrbracket = \lambda \text{f}: \llbracket \text{S}_1 \to \text{S}_2 \rrbracket \text{. } \lambda \text{x}: \llbracket \text{T}_1 \rrbracket \text{. } \llbracket \mathcal{C}_2 \rrbracket (\text{f}(\llbracket \mathcal{C}_1 \rrbracket \text{x})) \)，由类型翻译的定义，可得\( \llbracket \text{S}_1 \to \text{S}_2 \rrbracket = \llbracket \text{S}_1 \rrbracket \to \llbracket \text{S}_2 \rrbracket, \llbracket \text{T}_1 \to \text{T}_2 \rrbracket = \llbracket \text{T}_1 \rrbracket \to \llbracket \text{T}_2 \rrbracket \)，由\( \mathcal{C}_1 :: \text{T}_1 <: \text{S}_1 \)以及归纳假设，可得\( \vdash \llbracket \mathcal{C}_1 \rrbracket: \llbracket \text{T}_1 \rrbracket \to \llbracket \text{S}_1 \rrbracket \)，同理，可得\( \vdash \llbracket \mathcal{C}_2 \rrbracket: \llbracket \text{S}_2 \rrbracket \to \llbracket \text{T}_2 \rrbracket \)，综上，可得\( \vdash \llbracket \mathcal{C} \rrbracket : \llbracket \text{S} \rrbracket \to \llbracket \text{T} \rrbracket \)。
  4. 如果最后使用的规则是S-RCDWIDTH，则\( \text{S} = \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n+k} \}, \text{T} = \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \}, \llbracket \mathcal{C} \rrbracket = \lambda \text{t}: \llbracket \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n+k} \} \rrbracket \text{. } \{ \text{t}.\text{i} \ ^{i \in 1 \dots n} \} \)，由类型翻译的定义，可得\( \llbracket \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n+k} \} \rrbracket = \{ \llbracket \text{T}_i \rrbracket \ ^{i \in 1 \dots n+k} \}, \llbracket \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \rrbracket = \{ \llbracket \text{T}_i \rrbracket \ ^{i \in 1 \dots n} \} \)，综上，可得\( \vdash \llbracket \mathcal{C} \rrbracket : \llbracket \text{S} \rrbracket \to \llbracket \text{T} \rrbracket \)。
  5. 如果最后使用的规则是S-RCDDEPTH，则\( \text{S} = \{ \text{l}_i: \text{S}_i \ ^{i \in 1 \dots n} \}, \text{T} = \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \}, \forall 1 \leq i \leq n, \mathcal{C}_i :: \text{S}_i <: \text{T}_i, \llbracket \mathcal{C} \rrbracket = \lambda \text{t}: \llbracket \{ \text{l}_i: \text{S}_i \ ^{i \in 1 \dots n} \} \rrbracket \text{. } \{ \llbracket \mathcal{C}_i \rrbracket (\text{t}.\text{i}) \ ^{i \in 1 \dots n} \} \)，由类型翻译的定义，可得\( \llbracket \{ \text{l}_i: \text{S}_i \ ^{i \in 1 \dots n} \} \rrbracket = \{ \llbracket \text{S}_i \rrbracket \ ^{i \in 1 \dots n} \}, \llbracket \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \rrbracket = \{ \llbracket \text{T}_i \rrbracket \ ^{i \in 1 \dots n} \} \)，综上，可得\( \vdash \llbracket \mathcal{C} \rrbracket : \llbracket \text{S} \rrbracket \to \llbracket \text{T} \rrbracket \)。
  6. 如果最后使用的规则是S-RCDPERM，则\( \text{S} = \{ \text{k}_j: \text{S}_j \ ^{j \in 1 \dots n} \}, \text{T} = \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \)， \( \text{S} \)为\( \text{T} \)的排列，且\( \llbracket \mathcal{C} \rrbracket = \lambda \text{t}: \llbracket \{ \text{k}_j: \text{S}_j \ ^{j \in 1 \dots n} \} \rrbracket \text{. } \{ \text{t}.\text{j}_i \ ^{i \in 1 \dots n} \} \)，由类型翻译的定义，可得\( \llbracket \{ \text{k}_j: \text{S}_j \ ^{i \in 1 \dots n} \} \rrbracket = \{ \llbracket \text{S}_j \rrbracket \ ^{j \in 1 \dots n} \}, \llbracket \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \rrbracket = \{ \llbracket \text{T}_i \rrbracket \ ^{i \in 1 \dots n} \} \)，除此之外，\( \forall 1 \leq i \leq n \)，根据\( \text{j}_i \)的定义，有\( \text{T}_i = \text{S}_{j_i} \)，综上，可得\( \vdash \llbracket \mathcal{C} \rrbracket : \llbracket \text{S} \rrbracket \to \llbracket \text{T} \rrbracket \)。

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

证明引理15.6.1完毕。

现在，可以证明定理15.6.2了。

定理15.6.2的内容：

If \( \mathcal{D} :: \Gamma \vdash \text{t}: \text{T} \), then \( \llbracket \Gamma \rrbracket \vdash \llbracket \mathcal{D} \rrbracket : \llbracket \text{T} \rrbracket \), where \( \llbracket \Gamma \rrbracket \) is the point-wise extension of the type translation to contexts: \( \llbracket \empty \rrbracket = \empty \) and \( \llbracket \Gamma, \text{x}: \text{T} \rrbracket = \llbracket \Gamma \rrbracket, \text{x}: \llbracket \text{T} \rrbracket \).

证明定理15.6.2：

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

  1. 如果最后使用的规则是T-VAR，则\( \text{x}: \text{T} \in \Gamma, \llbracket \mathcal{D} \rrbracket = \text{x} \)，由\( \llbracket \Gamma \rrbracket \)的定义，可得\( \text{x}: \llbracket \text{T} \rrbracket \in \llbracket \Gamma \rrbracket \)，进而由T-VAR，可得\( \llbracket \Gamma \rrbracket \vdash \llbracket \mathcal{D} \rrbracket : \llbracket \text{T} \rrbracket \)。
  2. 如果最后使用的规则T-ABS，则\( \text{T} = \text{T}_1 \to \text{T}_2, \mathcal{D}_1 :: \Gamma, \text{x}: \text{T}_1 \vdash \text{t}_2: \text{T}_2, \llbracket \mathcal{D} \rrbracket = \lambda \text{x}: \llbracket \text{T}_1 \rrbracket \text{. } \llbracket \mathcal{D}_1 \rrbracket \)，由\( \mathcal{D}_1 :: \Gamma, \text{x}: \text{T}_1 \vdash \text{t}_2: \text{T}_2 \)以及归纳假设，可得\( \llbracket \Gamma, \text{x}: \text{T}_1 \rrbracket \vdash \llbracket \mathcal{D}_1 \rrbracket : \llbracket \text{T}_2 \rrbracket \)，即\( \llbracket \Gamma \rrbracket, \text{x}: \llbracket \text{T}_1 \rrbracket \vdash \llbracket \mathcal{D}_1 \rrbracket : \llbracket \text{T}_2 \rrbracket \)，而由类型翻译的定义，可得\( \llbracket \text{T}_1 \to \text{T}_2 \rrbracket = \llbracket \text{T}_1 \rrbracket \to \llbracket \text{T}_2 \rrbracket \)，综上以及使用T-ABS，可得\( \llbracket \Gamma \rrbracket \vdash \llbracket \mathcal{D} \rrbracket : \llbracket \text{T} \rrbracket \)。
  3. 如果最后使用的规则是T-APP，则\( \mathcal{D}_1 :: \Gamma \vdash \text{t}_1: \text{T}_2 \to \text{T}, \mathcal{D}_2 :: \Gamma \vdash \text{t}_2: \text{T}_2, \llbracket \mathcal{D} \rrbracket = \llbracket \mathcal{D}_1 \rrbracket \text{ } \llbracket \mathcal{D}_2 \rrbracket \)，由\( \mathcal{D}_1 :: \Gamma \vdash \text{t}_1: \text{T}_2 \to \text{T} \)以及归纳假设，可得\( \llbracket \Gamma \rrbracket \vdash \llbracket \mathcal{D}_1 \rrbracket : \llbracket \text{T}_2 \to \text{T} \rrbracket \)，同理可得，\( \llbracket \Gamma \rrbracket \vdash \llbracket \mathcal{D}_2 \rrbracket : \llbracket \text{T}_2 \rrbracket \)，而由类型翻译的定义，可得\( \llbracket \text{T}_2 \to \text{T} \rrbracket = \llbracket \text{T}_2 \rrbracket \to \llbracket \text{T} \rrbracket \)，综上以及使用T-APP，可得\( \llbracket \Gamma \rrbracket \vdash \llbracket \mathcal{D} \rrbracket : \llbracket \text{T} \rrbracket \)。
  4. 如果最后使用的规则是T-RCD，则\( \text{T} = \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \}, \forall 1 \leq i \leq n, \mathcal{D}_i :: \Gamma \vdash \text{t}_i: \text{T}_i, \llbracket \mathcal{D} \rrbracket = \{ \llbracket \mathcal{D}_i \rrbracket \ ^{i \in 1 \dots n} \} \)，由\( \forall 1 \leq i \leq n, \mathcal{D}_i :: \Gamma \vdash \text{t}_i: \text{T}_i \)以及归纳假设，可得\( \forall 1 \leq i \leq n, \llbracket \Gamma \rrbracket \vdash \llbracket \mathcal{D}_i \rrbracket : \llbracket \text{T}_i \rrbracket \)，而由类型翻译的定义，可得\( \llbracket \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \rrbracket = \{ \llbracket \text{T}_i \rrbracket \ ^{i \in 1 \dots n} \} \)，综上以及使用T-TUPLE，可得\( \llbracket \Gamma \rrbracket \vdash \llbracket \mathcal{D} \rrbracket : \llbracket \text{T} \rrbracket \)。
  5. 如果最后使用的规则是T-PROJ，则\( \text{T} = \text{T}_j, \mathcal{D}_1 :: \Gamma \vdash \text{t}_1 : \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \}, \llbracket \mathcal{D} \rrbracket = \llbracket \mathcal{D}_1 \rrbracket.\text{j} \)，由\( \mathcal{D}_1 :: \Gamma \vdash \text{t}_1 : \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \)以及归纳假设，可得\( \llbracket \Gamma \rrbracket \vdash \llbracket \mathcal{D}_1 \rrbracket : \llbracket \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \rrbracket \)，而由类型翻译的定义，可得\( \llbracket \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \rrbracket = \{ \llbracket \text{T}_i \rrbracket \ ^{i \in 1 \dots n} \} \)，综上以及使用tuple的T-PROJ，可得\( \llbracket \Gamma \rrbracket \vdash \llbracket \mathcal{D} \rrbracket : \llbracket \text{T} \rrbracket \)。
  6. 如果最后使用的规则是T-SUB，则\( \mathcal{D}_1 :: \Gamma \vdash \text{t}: \text{S}, \mathcal{C}_1 :: \text{S} <: \text{T}, \llbracket \mathcal{D} \rrbracket = \llbracket \mathcal{C}_1 \rrbracket \text{ } \llbracket \mathcal{D}_1 \rrbracket \)，由\( \mathcal{D}_1 :: \Gamma \vdash \text{t}: \text{S} \)以及归纳假设，可得\( \llbracket \Gamma \rrbracket \vdash \llbracket \mathcal{D}_1 \rrbracket : \llbracket \text{S} \rrbracket \)，由引理15.6.1，可得\( \vdash \llbracket \mathcal{C}_1 \rrbracket : \llbracket \text{S} \rrbracket \to \llbracket \text{T} \rrbracket \)，综上以及使用T-APP，可得\( \llbracket \Gamma \rrbracket \vdash \llbracket \mathcal{D} \rrbracket : \llbracket \text{T} \rrbracket \)。

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

证明定理15.6.2完毕。

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