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

第19章

章节19.4

练习19.4.1

题目：

By analogy with the S-TOP rule in our lambda-calculus with subtyping, one might expect to see a rule stating that \( \text{Object} \) is a supertype of every class. Why don’t we need it here?

解答：

因为我们在语法上强制要求每个新声明的类必须继承于一个现有的类，一开始我们仅有类\( \text{Object} \)，因此针对第一个声明的类，它唯一能继承的类就是\( \text{Object} \)，后续声明的类要么直接继承于\( \text{Object} \)，要么继承于之前声明的类，进而间接继承于\( \text{Object} \)，综上，类似\( \text{Top} \)，我们有\( \forall \text{C}, \text{C} <: \text{Object} \)，故不需要S-TOP规则。

上述是最直观、最容易理解的说法，实际上，我们的规则并没有“新声明的类”、“现有的类”的概念，故严格点的表述应该是：\( \forall \text{C} \)，我们要证明\( \text{C} <: \text{Object} \)，如果\( \text{C} = \text{Object} \)，则由自反性子类型规则，可得\( \text{C} <: \text{Object} \)，如果\( \text{C} \neq \text{Object} \)，则\( \text{C} \)是用户声明的类，可得\( CT(\text{C}) = \text{class C extends D } \{ \dots \} \)，于是由子类型规则，可得\( \text{C} <: \text{D} \)，如果\( \text{D} = \text{Object} \)，则我们就有了想要的\( \text{C} <: \text{Object} \)，否则，\( \text{D} \)也是用户声明的类，可得\( CT(\text{D}) = \text{class D extends E } \{ \dots \} \)，此时可以继续仿照上面进行下去，由于我们要求类的数量是有限的且子类型关系是无环的，可得上述过程必定会终止于唯一的非用户声明的类\( \text{Object} \)，有\( \text{C} <: \text{D} <: \dots <: \text{Object} \)。综上，\( \forall \text{C}, \text{C} <: \text{Object} \)，故不需要S-TOP规则。

练习19.4.2

题目：

A number of design decisions in FJ are dictated by the desire to make it a subset of Java, in the sense that every well- or ill-typed FJ program is well- or ill-typed as a Java program, and the well-typed programs behave the same. Suppose this requirement were dropped—i.e., suppose all we wanted was a Java-like core calculus. How would you change the design of FJ to make it simpler or more elegant?

解答：

第一个容易注意到的异常点就是，既然我们无法从类型上完全避免错误的类型转换，且E-CASTNEW在运行时可以确保类型转换的安全性，那为什么分成T-UCAST、T-DCAST、T-SCAST三个类型转换规则，而不像章节15.5一样，引入一个万能的T-DOWNCAST？答案是可以的，我们可以引入如下规则T-CAST，这里选择不像章节15.5一样叫T-DOWNCAST，因为该名字不太符合其性质：

\[ \dfrac{\Gamma \vdash \text{t}: \text{D}}{\Gamma \vdash (\text{C})\text{t}: \text{C}} \qquad (\text{T-CAST}) \]

然后由E-CASTNEW在运行时确保类型转换的安全性。

第二个可以改进的点就是，我们可以发现，所有类的构造函数做的事情都是固定的，初始化父类的域和自己的域，其他什么事情都没做，这点是在语法上限定的，具体看书上图19-1中\( \text{K} \)的定义，实际上，我们完全可以直接去掉构造函数相关的规则，且不用添加其他额外的规则，因为T-NEW已经能帮我们确保所有的域都初始化且类型正确了。

练习19.4.3

题目：

The operation of assigning a new value to the field of an object is omitted from FJ to simplify its presentation, but it can be added without changing the basic character of the calculus very much. Do this, using the treatment of references in Chapter 13 as a model.

解答：

我们以书上图13-1为参考，这里FJ的语法、规则等有点多，我就不完整抄下来了，仅在书上图19-1、19-2、19-3、19-4的基础上说明如何进行修改。

首先语法得添加\( \text{unit} \)，引用的创建、解引用、赋值，存储位置，如下：

\[ \begin{aligned} \text{t} &::= &\qquad \textit{terms:} \\ &\hphantom{::=} \dots &\qquad \dots \\ &\hphantom{::=} \text{unit} &\qquad \textit{constant } \text{unit} \\ &\hphantom{::=} \text{ref t} &\qquad \textit{reference creation} \\ &\hphantom{::=} !\text{t} &\qquad \textit{dereference} \\ &\hphantom{::=} \text{t} := \text{t} &\qquad \textit{assignment} \\ &\hphantom{::=} l &\qquad \textit{store location} \end{aligned} \]

值得添加\( \text{unit} \)和存储位置，如下：

\[ \begin{aligned} \text{v} &::= &\qquad \textit{values:} \\ &\hphantom{::=} \dots &\qquad \dots \\ &\hphantom{::=} \text{unit} &\qquad \textit{constant } \text{unit} \\ &\hphantom{::=} l &\qquad \textit{store location} \end{aligned} \]

类型需要在类的基础上添加\( \text{Unit} \)和引用类型，如下：

\[ \begin{aligned} \text{T} &::= &\qquad \textit{types:} \\ &\hphantom{::=} \text{C} &\qquad \textit{class} \\ &\hphantom{::=} \text{Unit} &\qquad \textit{unit type} \\ &\hphantom{::=} \text{Ref T} &\qquad \textit{type of reference cells} \end{aligned} \]

详细点的话，还得添加store和store typing的语法，如下：

\[ \begin{aligned} \mu &::= &\qquad \textit{stores:} \\ &\hphantom{::=} \empty &\qquad \textit{empty store} \\ &\hphantom{::=} \mu, l = \text{v} &\qquad \textit{location binding} \\ \Sigma &::= &\qquad \textit{store typings:} \\ &\hphantom{::=} \empty &\qquad \textit{empty store typing} \\ &\hphantom{::=} \Sigma, l: \text{T} &\qquad \textit{location typing} \end{aligned} \]

子类型规则得改下，前两个规则使用的元变量得改成\( \text{S}, \text{T} \)之类的，这是因为我们引入了\( \text{Unit} \)、引用类型，它们不是类，具体如下：

\[ \text{T} <: \text{T} \newline \dfrac{\text{S} <: \text{U} \quad \text{U} <: \text{T}}{ \text{S} <: \text{T}} \newline \dfrac{CT(\text{C}) = \text{class C extends D } \{ \dots \}}{ \text{C} <: \text{D}} \]

同理，类声明、构造函数声明、方法声明语法使用的元变量也得修改，得允许域、参数、返回等的类型是\( \text{Unit} \)、引用类型，具体如下：

\[ \begin{aligned} \text{CL} &::= \qquad \textit{class declarations} \\ &\hphantom{::=} \text{class C extends C } \{ \overline{\text{T}} \text{ } \overline{\text{f}}; \text{K} \text{ } \overline{\text{M}} \} \\ \text{K} &::= \qquad \textit{constructor declarations} \\ &\hphantom{::=} \text{C}(\overline{\text{T}} \text{ } \overline{\text{f}}) \text{ } \{ \text{super}(\overline{\text{f}}); \text{this}.\overline{\text{f}} = \overline{\text{f}} \} \\ \text{M} &::= \qquad \textit{method declarations} \\ &\hphantom{::=} \text{T m}(\overline{\text{T}} \text{ } \overline{\text{x}}) \text{ } \{ \text{return t}; \} \end{aligned} \]

几个辅助函数也得改元变量的使用，首先是\( \textit{fields} \)：

\[ \textit{fields}(\text{Object}) = \bullet \]

\[ \dfrac{\begin{aligned} CT(\text{C}) &= \text{class C extends D } \{ \overline{\text{T}} \text{ } \overline{\text{f}}; \text{K} \text{ } \overline{\text{M}} \} \\ &\hphantom{aaaa} \textit{fields}(\text{D}) = \overline{\text{S}} \text{ } \overline{\text{g}} \end{aligned}}{ \textit{fields}(\text{C}) = \overline{\text{S}} \text{ } \overline{\text{g}}, \overline{\text{T}} \text{ } \overline{\text{f}}} \]

接着是\( \textit{mtype} \)：

\[ \dfrac{\begin{aligned} CT(\text{C}) &= \text{class C extends D } \{ \overline{\text{T}} \text{ } \overline{\text{f}}; \text{K} \text{ } \overline{\text{M}} \} \\ &\text{T m}(\overline{\text{T}} \text{ } \overline{\text{x}}) \text{ } \{ \text{return t}; \} \in \overline{\text{M}} \end{aligned}}{\textit{mtype}(\text{m}, \text{C}) = \overline{\text{T}} \to \text{T}} \]

\[ \dfrac{\begin{aligned} CT(\text{C}) &= \text{class C extends D } \{ \overline{\text{T}} \text{ } \overline{\text{f}}; \text{K} \text{ } \overline{\text{M}} \} \\ &\hphantom{aa} \text{m is not defined in } \overline{\text{M}} \end{aligned}}{\textit{mtype}(\text{m}, \text{C}) = \textit{mtype}(\text{m}, \text{D})} \]

然后是\( \textit{mbody} \)：

\[ \dfrac{\begin{aligned} CT(\text{C}) &= \text{class C extends D } \{ \overline{\text{T}} \text{ } \overline{\text{f}}; \text{K} \text{ } \overline{\text{M}} \} \\ &\text{T m}(\overline{\text{T}} \text{ } \overline{\text{x}}) \text{ } \{ \text{return t}; \} \in \overline{\text{M}} \end{aligned}}{\textit{mbody}(\text{m}, \text{C}) = (\overline{\text{x}}, \text{t})} \]

\[ \dfrac{\begin{aligned} CT(\text{C}) &= \text{class C extends D } \{ \overline{\text{T}} \text{ } \overline{\text{f}}; \text{K} \text{ } \overline{\text{M}} \} \\ &\hphantom{aa} \text{m is not defined in } \overline{\text{M}} \end{aligned}}{\textit{mbody}(\text{m}, \text{C}) = \textit{mbody}(\text{m}, \text{D})} \]

最后是\( \textit{override} \)：

\[ \dfrac{\textit{mtype}(\text{m}, \text{D}) = \overline{\text{S}} \to \text{S}_0 \text{ implies } \overline{\text{T}} = \overline{\text{S}} \text{ and } \text{T}_0 = \text{S}_0}{ \textit{override}(\text{m}, \text{D}, \overline{\text{T}} \to \text{T}_0)} \]

接下来就是求值规则了，都得加上store，部分规则的元变量也得改下，如下：

\[ \begin{aligned} \dfrac{\textit{fields}(\text{C}) = \overline{\text{T}} \text{ } \overline{\text{f}}}{ (\text{new } \text{C}(\overline{\text{v}})).\text{f}_i \mid \mu \rightarrow \text{v}_i \mid \mu} &\qquad (\text{E-PROJNEW}) \\ \dfrac{\textit{mbody}(\text{m}, \text{C}) = (\overline{\text{x}}, \text{t}_0)}{ (\text{new } \text{C}(\overline{\text{v}})).\text{m}(\overline{\text{u}}) \mid \mu \rightarrow [\overline{\text{x}} \mapsto \overline{\text{u}}, \text{this} \mapsto \text{new } \text{C}(\overline{\text{v}})]\text{t}_0 \mid \mu} &\qquad (\text{E-INVKNEW}) \\ \dfrac{\text{C} <: \text{D}}{ (\text{D})(\text{new } \text{C}(\overline{\text{v}})) \mid \mu \rightarrow \text{new } \text{C}(\overline{\text{v}}) \mid \mu} &\qquad (\text{E-CASTNEW}) \\ \dfrac{\text{t}_0 \mid \mu \rightarrow \text{t}'_0 \mid \mu'}{ \text{t}_0.\text{f} \mid \mu \rightarrow \text{t}'_0.\text{f} \mid \mu'} &\qquad (\text{E-FIELD}) \\ \dfrac{\text{t}_0 \mid \mu \rightarrow \text{t}'_0 \mid \mu'}{ \text{t}_0.\text{m}(\overline{\text{t}}) \mid \mu \rightarrow \text{t}'_0.\text{m}(\overline{\text{t}}) \mid \mu'} &\qquad (\text{E-INVK-RECV}) \\ \dfrac{\text{t}_i \mid \mu \rightarrow \text{t}'_i \mid \mu'}{ \text{v}_0.\text{m}(\overline{\text{v}}, \text{t}_i, \overline{\text{t}}) \mid \mu \rightarrow \text{v}_0.\text{m}(\overline{\text{v}}, \text{t}'_i, \overline{\text{t}}) \mid \mu'} &\qquad (\text{E-INVK-ARG}) \\ \dfrac{\text{t}_i \mid \mu \rightarrow \text{t}'_i \mid \mu'}{ \text{new } \text{C}(\overline{\text{v}}, \text{t}_i, \overline{\text{t}}) \mid \mu \rightarrow \text{new } \text{C}(\overline{\text{v}}, \text{t}'_i, \overline{\text{t}}) \mid \mu'} &\qquad (\text{E-INVK-ARG}) \\ \dfrac{\text{t}_0 \mid \mu \rightarrow \text{t}'_0 \mid \mu'}{ (\text{C})\text{t}_0 \mid \mu \rightarrow (\text{C})\text{t}'_0 \mid \mu'} &\qquad (\text{E-CAST}) \\ \dfrac{l \notin dom(\mu)}{ \text{ref } \text{v}_1 \mid \mu \rightarrow l \mid (\mu, l \mapsto \text{v}_1)} &\qquad (\text{E-REFV}) \\ \dfrac{\text{t}_1 \mid \mu \rightarrow \text{t}'_1 \mid \mu'}{ \text{ref } \text{t}_1 \mid \mu \rightarrow \text{ref } \text{t}'_1 \mid \mu'} &\qquad (\text{E-REF}) \\ \dfrac{\mu(l) = \text{v}}{ !l \mid \mu \rightarrow \text{v} \mid \mu} &\qquad (\text{E-DEREFLOC}) \\ \dfrac{\text{t}_1 \mid \mu \rightarrow \text{t}'_1 \mid \mu'}{ !\text{t}_1 \mid \mu \rightarrow \ !\text{t}'_1 \mid \mu'} &\qquad (\text{E-DEREF}) \\ l := \text{v}_2 \mid \mu \rightarrow \text{unit} \mid [l \mapsto \text{v}_2]\mu &\qquad (\text{E-ASSIGN}) \\ \dfrac{\text{t}_1 \mid \mu \rightarrow \text{t}'_1 \mid \mu'}{ \text{t}_1 := \text{t}_2 \mid \mu \rightarrow \text{t}'_1 := \text{t}_2 \mid \mu'} &\qquad (\text{E-ASSIGN1}) \\ \dfrac{\text{t}_2 \mid \mu \rightarrow \text{t}'_2 \mid \mu'}{ \text{v}_1 := \text{t}_2 \mid \mu \rightarrow \text{v}_1 := \text{t}'_2 \mid \mu'} &\qquad (\text{E-ASSIGN2}) \end{aligned} \]

需要注意的是，有些求值没有副作用，此时求值前后的store不变，都是\( \mu \)，比如上面的E-PROJNEW、E-INVKNEW、E-CASTNEW等。

另外一个需要注意的是，我们不允许\( \text{Unit} \)、引用类型用于类型转换，如果想允许的话，那首先得知道，单靠E-CASTNEW是无法确保类型转换的安全性的，得添加其他规则，除此之外，还得加入引用类型的子类型规则，遵循invariant，等等，要改的东西比较多，同时带来的价值不大。看起来似乎允许引用类型进行向上转换还是挺有价值的，但是还是之前的问题，引用类型的子类型规则遵循invariant，直接允许向上转换是有风险的，除非引入\( \text{Source}, \text{Sink} \)，或者\( \text{Ref} \)接受两个类型参数，区分开读和写的能力。综上，我们这里选择不允许\( \text{Unit} \)、引用类型用于类型转换。

最后是类型规则，除了\( \text{C OK} \)，都得加上store typing，部分规则的元变量也得改下，如下：

\[ \begin{aligned} \dfrac{\text{x}: \text{T} \in \Gamma}{ \Gamma \mid \Sigma \vdash \text{x}: \text{T}} &\qquad (\text{T-VAR}) \\ \dfrac{\Gamma \mid \Sigma \vdash \text{t}_0: \text{C}_0 \quad \textit{fields}(\text{C}_0) = \overline{\text{T}} \text{ } \overline{\text{f}}}{ \Gamma \mid \Sigma \vdash \text{t}_0.\text{f}_i: \text{T}_i} &\qquad (\text{T-FIELD}) \\ \dfrac{\begin{aligned} \Gamma \mid \Sigma \vdash \text{t}_0 &: \text{C}_0 \\ \textit{mtype}(\text{m}, \text{C}_0) &= \overline{\text{T}} \rightarrow \text{T} \\ \Gamma \mid \Sigma \vdash \overline{\text{t}}: \overline{\text{S}} &\quad \overline{\text{S}} <: \overline{\text{T}} \end{aligned}}{\Gamma \mid \Sigma \vdash \text{t}_0.\text{m}(\overline{\text{t}}): \text{T}} &\qquad (\text{T-INVK}) \\ \dfrac{\begin{aligned} \textit{fields}(\text{C}) &= \overline{\text{T}} \text{ } \overline{\text{f}} \\ \Gamma \mid \Sigma \vdash \overline{\text{t}}: \overline{\text{S}} &\quad \overline{\text{S}} <: \overline{\text{T}} \end{aligned}}{\Gamma \mid \Sigma \vdash \text{new } \text{C}(\overline{\text{t}}): \text{C}} &\qquad (\text{T-NEW}) \\ \dfrac{\Gamma \mid \Sigma \vdash \text{t}_0: \text{D} \quad \text{D} <: \text{C}}{ \Gamma \mid \Sigma \vdash (\text{C})\text{t}_0: \text{C}} &\qquad (\text{T-UCAST}) \\ \dfrac{\Gamma \mid \Sigma \vdash \text{t}_0: \text{D} \quad \text{C} <: \text{D} \quad \text{C} \neq \text{D}}{ \Gamma \mid \Sigma \vdash (\text{C})\text{t}_0: \text{C}} &\qquad (\text{T-DCAST}) \\ \dfrac{\begin{aligned} \Gamma \mid \Sigma \vdash \text{t}_0 &: \text{D} \quad \text{C} \nless: \text{D} \quad \text{D} \nless: \text{C} \\ &\textit{stupid warning} \end{aligned}}{ \Gamma \mid \Sigma \vdash (\text{C})\text{t}_0: \text{C}} &\qquad (\text{T-SCAST}) \\ \dfrac{\begin{aligned} &\overline{\text{x}}: \overline{\text{T}}, \text{this}: \text{C} \mid \Sigma \vdash \text{t}_0: \text{S}_0 \quad \text{S}_0 <: \text{T}_0 \\ &CT(\text{C}) = \text{class C extends D } \{ \dots \} \\ &\hphantom{CT(\text{C})} \textit{override}(\text{m}, \text{D}, \overline{\text{T}} \to \text{T}_0) \end{aligned}}{\text{T}_0 \text{ } \text{m}(\overline{\text{T}} \text{ } \overline{\text{x}}) \{ \text{return } \text{t}_0; \} \text{ OK in C}} &\qquad (\text{M OK in C}) \\ \dfrac{\begin{aligned} \text{K} &= \text{C}(\overline{\text{S}} \text{ } \overline{\text{g}}, \overline{\text{T}} \text{ } \overline{\text{f}}) \text{ } \{ \text{super}(\overline{\text{g}}); \text{this}.\overline{\text{f}} = \overline{\text{f}}; \} \\ &\textit{fields}(\text{D}) = \overline{\text{S}} \text{ } \overline{\text{g}} \quad \overline{\text{M}} \text{ OK in C} \end{aligned}}{ \text{class C extends D } \{ \overline{\text{T}} \text{ } \overline{\text{f}}; \text{K } \overline{\text{M}} \} \text{ OK}} &\qquad (\text{C OK}) \\ \Gamma \mid \Sigma \vdash \text{unit}: \text{Unit} &\qquad (\text{T-UNIT}) \\ \dfrac{\Sigma(l) = \text{T}_1}{ \Gamma \mid \Sigma \vdash l: \text{Ref } \text{T}_1} &\qquad (\text{T-LOC}) \\ \dfrac{\Gamma \mid \Sigma \vdash \text{t}_1: \text{T}_1}{ \Gamma \mid \Sigma \vdash \text{ref } \text{t}_1: \text{Ref } \text{T}_1} &\qquad (\text{T-REF}) \\ \dfrac{\Gamma \mid \Sigma \vdash \text{t}_1: \text{Ref } \text{T}_{11}}{ \Gamma \mid \Sigma \vdash \ !\text{t}_1: \text{T}_{11}} &\qquad (\text{T-DEREF}) \\ \dfrac{\Gamma \mid \Sigma \vdash \text{t}_1: \text{Ref } \text{T}_{11} \quad \Gamma \mid \Sigma \vdash \text{t}_2: \text{T}_{11}}{ \Gamma \mid \Sigma \vdash \text{t}_1 := \text{t}_2: \text{Unit}} &\qquad (\text{T-ASSIGN}) \end{aligned} \]

\( \text{C OK} \)不用加store typing是因为在类型推导方面，它仅涉及方法的类型推导，而方法的类型推导\( \text{M OK in C} \)有加store typing，相当于间接给\( \text{C OK} \)加上了store typing。

练习19.4.4

题目：

Extend FJ with analogs of Java’s \( \text{raise} \) and \( \text{try} \) forms, using the treatment of exceptions in Chapter 14 as a model.

解答：

我们以书上图14-3为参考，类似练习19.4.3，由于FJ的语法、规则等有点多，我就不完整抄下来了，仅在书上图19-1、19-2、19-3、19-4的基础上说明如何进行修改。

首先语法得添加异常的抛出和处理，如下：

\[ \begin{aligned} \text{t} &::= &\qquad \textit{terms:} \\ &\hphantom{::=} \dots &\qquad \dots \\ &\hphantom{::=} \text{raise t} &\qquad \textit{raise exception} \\ &\hphantom{::=} \text{try t with } (\text{C } \text{x}) \text{ } \text{t} &\qquad \textit{handle exceptions} \end{aligned} \]

不同于章节14.3，我们这里允许\( \text{with} \)后面声明能处理的异常类型为指定的类\( \text{C} \)或者其子类，当有异常抛出且异常值的类型为\( \text{C} \)的子类时，则该异常的值会绑定到\( \text{x} \)供后面的\( \text{t} \)处理异常使用。

接下来是求值规则，如下：

\[ \begin{aligned} \dots &\qquad \dots \\ (\text{raise } \text{v}_{11}) \text{ } \text{t}_2 \rightarrow \text{raise } \text{v}_{11} &\qquad (\text{E-APPRAISE1}) \\ \text{v}_1 \text{ } (\text{raise } \text{v}_{21}) \rightarrow \text{raise } \text{v}_{21} &\qquad (\text{E-APPRAISE2}) \\ \dfrac{\text{t}_1 \rightarrow \text{t}'_1}{ \text{raise } \text{t}_1 \rightarrow \text{raise } \text{t}'_1} &\qquad (\text{E-RAISE}) \\ \text{raise } (\text{raise } \text{v}_{11}) \rightarrow \text{raise } \text{v}_{11} &\qquad (\text{E-RAISERAISE}) \\ \text{try } \text{v}_1 \text{ with } (\text{C } \text{x}) \text{ } \text{t}_2 \rightarrow \text{v}_1 &\qquad (\text{E-TRYV}) \\ \dfrac{\text{D} <: \text{C}}{ \text{try } \text{raise } (\text{new } \text{D}(\overline{\text{v}})) \text{ with } (\text{C } \text{x}) \text{ } \text{t}_2 \rightarrow [\text{x} \mapsto \text{v}_{11}]\text{t}_2} &\qquad (\text{E-TRYRAISE}) \\ \dfrac{\text{t}_1 \rightarrow \text{t}'_1}{ \text{try } \text{t}_1 \text{ with } (\text{C } \text{x}) \text{ } \text{t}_2 \rightarrow \text{try } \text{t}'_1 \text{ with } (\text{C } \text{x}) \text{ } \text{t}_2} &\qquad (\text{E-TRY}) \end{aligned} \]

注意到E-TRYRAISE确保了\( \text{t}_2 \)只处理异常的值类型为\( \text{C} \)的子类的异常。

最后是类型规则，如下：

\[ \begin{aligned} \dots &\qquad \dots \\ \dfrac{\Gamma \vdash \text{t}_1: \text{C}}{ \Gamma \vdash \text{raise } \text{t}_1: \text{D}} &\qquad (\text{T-EXN}) \\ \dfrac{\Gamma \vdash \text{t}_1: \text{D} \quad \Gamma, \text{x}: \text{C} \vdash \text{t}_2: \text{D}}{ \Gamma \vdash \text{try } \text{t}_1 \text{ with } (\text{C } \text{x}) \text{ } \text{t}_2: \text{D}} &\qquad (\text{T-TRY}) \end{aligned} \]

练习19.4.5

题目：

FJ, like full Java, presents the typing relation in algorithmic form. There is no subsumption rule; instead, several of the other rules include subtyping checks among their premises. Can the system be reformulated in a more declarative style, dropping most or all of these premises in favor of a single subsumption rule?

解答：

可以形式化成更声明式的风格，但是无法丢弃所有的算法性子类型前提条件（只能丢弃部分），特别的，T-DCAST和T-SCAST的无法丢弃。

具体修改如下：

首先，添加规则T-SUB，如下：

\[ \dfrac{\Gamma \vdash \text{t}: \text{S} \quad \text{S} <: \text{T}}{ \Gamma \vdash \text{t}: \text{T}} \qquad (\text{T-SUB}) \]

接下来，丢弃T-INVK、T-NEW、T-UCAST、M OK in C中的算法性子类型前提条件，修改后如下：

\[ \begin{aligned} \dfrac{\begin{aligned} \Gamma \vdash \text{t}_0 &: \text{C}_0 \\ \textit{mtype}(\text{m}, \text{C}_0) &= \overline{\text{D}} \rightarrow \text{C} \\ \Gamma \vdash \overline{\text{t}} &: \overline{\text{D}} \end{aligned}}{\Gamma \vdash \text{t}_0.\text{m}(\overline{\text{t}}): \text{C}} &\qquad (\text{T-INVK}) \\ \dfrac{\begin{aligned} \textit{fields}(\text{C}) &= \overline{\text{D}} \text{ } \overline{\text{f}} \\ \Gamma \vdash \overline{\text{t}} &: \overline{\text{D}} \end{aligned}}{\Gamma \vdash \text{new } \text{C}(\overline{\text{t}}): \text{C}} &\qquad (\text{T-NEW}) \\ \dfrac{\Gamma \vdash \text{t}_0: \text{C}}{ \Gamma \vdash (\text{C})\text{t}_0: \text{C}} &\qquad (\text{T-UCAST}) \\ \dfrac{\begin{aligned} &\hphantom{CT} \overline{\text{x}}: \overline{\text{C}}, \text{this}: \text{C} \vdash \text{t}_0: \text{C}_0 \\ &CT(\text{C}) = \text{class C extends D } \{ \dots \} \\ &\hphantom{CT} \textit{override}(\text{m}, \text{D}, \overline{\text{C}} \to \text{C}_0) \end{aligned}}{\text{C}_0 \text{ } \text{m}(\overline{\text{C}} \text{ } \overline{\text{x}}) \{ \text{return } \text{t}_0; \} \text{ OK in C}} &\qquad (\text{M OK in C}) \end{aligned} \]

T-DCAST和T-SCAST的算法性子类型前提条件则仍然保留，因为T-SUB不适用于它们对应的情况。

练习19.4.6

题目：

Full Java provides both classes and interfaces, which specify the types of methods, but not their implementations. Interfaces are useful because they permit a richer, non-tree-structured, subtype relation: each class has a single superclass (from which it inherits instance variables and method bodies), but may additionally implement any number of interfaces.

The presence of interfaces in Java actually forces the choice of an algorithmic presentation of the typing relation, which gives each typable term a unique (minimal) type. The reason is an interaction between conditional expressions (written \( \text{t}_1 \mathop{?} \text{t}_2 : \text{t}_3 \) in Java) and interfaces.

1. Show how to extend FJ with interfaces in the style of Java.
2. Show that, in the presence of interfaces, the subtype relation is not necessarily closed under joins. (Recall from \( \S \text{16.3} \) that the existence of joins played a critical role in the minimal typing property for conditionals.)
3. What is Java’s typing rule for conditional expressions? Is it reasonable?

解答：

解答1：

注：当一个类实现多个接口的时候，我们假设多个接口间均没有同名的方法，同理，当一个接口继承多个接口的时候，我们则假设该接口和它继承的多个接口间一律没有同名方法。

首先，我们要引入接口声明的语法，如下：

\[ \begin{aligned} \text{IFD} &::= \qquad \textit{interface declarations} \\ &\hphantom{::=} \text{interface I } \{ \overline{\text{MT}} \} \\ &\hphantom{::=} \text{interface I extends } \overline{\text{I}} \text{ } \{ \overline{\text{MT}} \} \end{aligned} \]

一个接口可以什么接口都不继承，也可以继承于多个接口\( \overline{\text{I}} \)， \( \overline{\text{I}} \)是\( \text{I}_1, \text{I}_2, \dots, \text{I}_n \)的缩写，这里类似\( \text{class} \)，我们假设\( \forall \text{I}_j \in \overline{\text{I}}, \text{I} \neq \text{I}_j \)，即一个接口不能继承自己。

上面的语法还用到了方法的类型声明\( \text{MT} \)，不同于\( \text{M} \)，它不包含实现，语法如下：

\[ \begin{aligned} \text{MT} &::= \qquad \textit{method type declarations} \\ &\hphantom{::=} \text{CI m} (\overline{\text{CI}} \text{ } \overline{\text{x}}); \end{aligned} \]

上面用到的元变量\( \text{CI} \)代表类或者接口，定义如下：

\[ \begin{aligned} \text{CI} &::= \qquad \textit{class or interface} \\ &\hphantom{::=} \text{C} \\ &\hphantom{::=} \text{I} \end{aligned} \]

类的语法得拓展下，允许一个类实现多个接口或者不实现接口，同时，域的类型得允许是接口或类，如下：

\[ \begin{aligned} \text{CL} &::= \qquad \textit{class declarations} \\ &\hphantom{::=} \text{class C extends C } \{ \overline{\text{CI}} \text{ } \overline{\text{f}}; \text{K} \text{ } \overline{\text{M}} \} \\ &\hphantom{::=} \text{class C extends C implements } \overline{\text{I}} \text{ } \{ \overline{\text{CI}} \text{ } \overline{\text{f}}; \text{K} \text{ } \overline{\text{M}} \} \end{aligned} \]

同样的，构造函数声明和方法声明的语法也得改下，允许类型是类或接口，如下：

\[ \begin{aligned} \text{K} &::= \qquad \textit{constructor declarations} \\ &\hphantom{::=} \text{C} (\overline{\text{CI}} \text{ } \overline{\text{f}}) \text{ } \{ \text{super}(\overline{\text{f}}); \text{this}.\overline{\text{f}} = \overline{\text{f}}; \} \end{aligned} \]

\[ \begin{aligned} \text{M} &::= \qquad \textit{method declarations} \\ &\hphantom{::=} \text{CI m} (\overline{\text{CI}} \text{ } \overline{\text{x}}) \text{ } \{ \text{return t}; \} \end{aligned} \]

类型转换的语法也得修改下，目标转换类型允许是类或者接口，如下：

\[ \begin{aligned} \text{t} &::= &\qquad \textit{terms} \\ &\hphantom{::=} \dots &\qquad \dots \\ &\hphantom{::=} (\text{CI}) \text{t} &\qquad \text{cast} \end{aligned} \]

接下来修改子类型规则，自反性和传递性的规则不用改，类的要改，如下：

\[ \dfrac{CT( C) = \text{class C extends D } \{ \dots \}}{\text{C} <: \text{D}} \]

\[ \dfrac{CT( C) = \text{class C extends D implements } \overline{\text{I}} \text{ } \{ \dots \}}{\text{C} <: \text{D}} \]

\[ \dfrac{CT( C) = \text{class C extends D implements } \text{I}_1, \dots, \text{I}_j, \dots, \text{I}_n \text{ } \{ \dots \}}{ \text{C} <: \text{I}_j} \]

还得处理接口间的继承，如下：

\[ \dfrac{IT(\text{I}) = \text{interface I extends } \text{I}_1, \dots, \text{I}_j, \dots, \text{I}_n \text{ } \{ \dots \}}{ \text{I} <: \text{I}_j} \]

这里\( IT \)类似\( CT \)，为接口名\( \text{I} \)到接口声明\( \text{IFD} \)间的映射，程序原本是二元组\( (CT, t) \)，现在变成\( (CT, IT, t) \)，且同\( CT \)，我们也假设\( IT \)表是固定的。

辅助函数\( \text{fields} \)得考虑域类型不仅可能是类，也可能是接口， \( \text{mtype}, \text{override} \)则也得拓展以处理接口的情况，如下：

先是\( \textit{fields} \)：

\[ \textit{fields}(\text{Object}) = \bullet \]

\[ \dfrac{\begin{aligned} CT(\text{C}) &= \text{class C extends D } \{ \overline{\text{CI}} \text{ } \overline{\text{f}}; \text{K} \text{ } \overline{\text{M}} \} \\ &\hphantom{aaa} \textit{fields}(\text{D}) = \overline{\text{DI}} \text{ } \overline{\text{g}} \end{aligned}}{ \textit{fields}(\text{C}) = \overline{\text{DI}} \text{ } \overline{\text{g}}, \overline{\text{CI}} \text{ } \overline{\text{f}}} \]

\[ \dfrac{\begin{aligned} CT(\text{C}) = &\text{class C extends D implements } \overline{\text{I}} \text{ } \{ \overline{\text{CI}} \text{ } \overline{\text{f}}; \text{K} \text{ } \overline{\text{M}} \} \\ &\hphantom{aaaaaa} \textit{fields}(\text{D}) = \overline{\text{DI}} \text{ } \overline{\text{g}} \end{aligned}}{ \textit{fields}(\text{C}) = \overline{\text{DI}} \text{ } \overline{\text{g}}, \overline{\text{CI}} \text{ } \overline{\text{f}}} \]

这里元变量\( \text{DI} \)和\( \text{CI} \)一样，都是代表类或者接口。

然后是\( \textit{mtype} \)：

\[ \dfrac{\begin{aligned} IT(\text{I}) &= \text{interface I } \{ \overline{\text{MT}} \} \\ &\text{CI m}(\overline{\text{CI}} \text{ } \overline{\text{x}}); \in \overline{\text{MT}} \end{aligned}}{\textit{mtype}(\text{m}, \text{I}) = \overline{\text{CI}} \to \text{CI}} \]

\[ \dfrac{\begin{aligned} IT(\text{I}) &= \text{interface I extends } \overline{\text{I}} \text{ } \{ \overline{\text{MT}} \} \\ &\text{CI m}(\overline{\text{CI}} \text{ } \overline{\text{x}}); \in \overline{\text{MT}} \end{aligned}}{\textit{mtype}(\text{m}, \text{I}) = \overline{\text{CI}} \to \text{CI}} \]

\[ \dfrac{\begin{aligned} IT(\text{I}) &= \text{interface I extends } \overline{\text{I}} \text{ } \{ \overline{\text{MT}} \} \\ &\hphantom{aa} \text{m is not defined in } \overline{\text{MT}} \\ &\exists \text{I}_j \in \overline{\text{I}}, \textit{mtype}(\text{m}, \text{I}_j) \text{ is defined} \end{aligned}}{\textit{mtype}(\text{m}, \text{I}) = \textit{mtype}(\text{m}, \text{I}_j)} \]

(注：由于我们假设接口与它继承的多个接口间没有同名方法，因此在上述规则下， \( \textit{mtype}(\text{m}, \text{I}) \)是良好定义的，不会出现诸如继承的两个接口分别给同一个方法名两个不同的方法类型的情况。)

\[ \dfrac{\begin{aligned} CT(\text{C}) &= \text{class C extends D } \{ \overline{\text{CI}} \text{ } \overline{\text{f}}; \text{K} \text{ } \overline{\text{M}} \} \\ &\text{DI m}(\overline{\text{DI}} \text{ } \overline{\text{x}}) \text{ } \{ \text{return t}; \} \in \overline{\text{M}} \end{aligned}}{\textit{mtype}(\text{m}, \text{C}) = \overline{\text{DI}} \to \text{DI}} \]

\[ \dfrac{\begin{aligned} CT(\text{C}) &= \text{class C extends D } \{ \overline{\text{CI}} \text{ } \overline{\text{f}}; \text{K} \text{ } \overline{\text{M}} \} \\ &\hphantom{aa} \text{m is not defined in } \overline{\text{M}} \end{aligned}}{\textit{mtype}(\text{m}, \text{C}) = \textit{mtype}(\text{m}, \text{D})} \]

\[ \dfrac{\begin{aligned} CT(\text{C}) &= \text{class C extends D implements } \overline{\text{I}} \text{ } \{ \overline{\text{CI}} \text{ } \overline{\text{f}}; \text{K} \text{ } \overline{\text{M}} \} \\ &\hphantom{aaaa}\text{DI m}(\overline{\text{DI}} \text{ } \overline{\text{x}}) \text{ } \{ \text{return t}; \} \in \overline{\text{M}} \end{aligned}}{\textit{mtype}(\text{m}, \text{C}) = \overline{\text{DI}} \to \text{DI}} \]

\[ \dfrac{\begin{aligned} CT(\text{C}) &= \text{class C extends D implements } \overline{\text{I}} \text{ } \{ \overline{\text{CI}} \text{ } \overline{\text{f}}; \text{K} \text{ } \overline{\text{M}} \} \\ &\hphantom{aaaaa} \text{m is not defined in } \overline{\text{M}} \end{aligned}}{\textit{mtype}(\text{m}, \text{C}) = \textit{mtype}(\text{m}, \text{D})} \]

最后是\( \textit{override} \)：

\[ \dfrac{\textit{mtype}(\text{m}, \text{CI}) = \overline{\text{DI}} \to \text{DI}_0 \text{ implies } \overline{\text{CI}} = \overline{\text{DI}} \text{ and } \text{CI}_0 = \text{DI}_0}{ \textit{override}(\text{m}, \text{CI}, \overline{\text{CI}} \to \text{CI}_0)} \]

这里得注意下，我们前提条件中用了“implies”的字眼，即前提条件为“如果\( \dots \)，就\( \dots \)”的形式，因此如果\( \textit{mtype}(\text{m}, \text{CI}) \)未定义，则前提条件直接成立，直接有\( \textit{override}(\text{m}, \text{CI}, \overline{\text{CI}} \to \text{CI}_0) \)。

接下来考虑求值规则，E-CASTNEW和E-CAST使用的元变量得改下，得允许类型转换的目标类型是类或者接口，如下：

\[ \dfrac{\text{C} <: \text{CI}}{ (\text{CI})(\text{new } \text{C}(\overline{\text{v}})) \rightarrow \text{new } \text{C}(\overline{\text{v}})} \qquad (\text{E-CASTNEW}) \]

\[ \dfrac{\text{t}_0 \rightarrow \text{t}'_0}{ (\text{CI})\text{t}_0 \rightarrow (\text{CI})\text{t}'_0} \qquad (\text{E-CAST}) \]

最后是类型规则，大部分修改和前面的类似，不过需要注意的是接口没有域，故不用考虑\( \textit{fields} \)参数为接口的情况。

\[ \dfrac{\text{x}: \text{CI} \in \Gamma}{ \Gamma \vdash \text{x}: \text{CI}} \qquad (\text{T-VAR}) \]

\[ \dfrac{\Gamma \vdash \text{t}_0: \text{C}_0 \quad \textit{fields}(\text{C}_0) = \overline{\text{CI}} \text{ } \overline{\text{f}}}{ \Gamma \vdash \text{t}_0.\text{f}_i: \text{CI}_i} \qquad (\text{T-FIELD}) \]

\[ \dfrac{\begin{aligned} \Gamma \vdash \text{t}_0 &: \text{I}_0 \\ \textit{mtype}(\text{m}, \text{I}_0) &= \overline{\text{DI}} \rightarrow \text{CI} \\ \Gamma \vdash \overline{\text{t}}: \overline{\text{CI}} &\quad \overline{\text{CI}} <: \overline{\text{DI}} \end{aligned}}{\Gamma \vdash \text{t}_0.\text{m}(\overline{\text{t}}): \text{CI}} \qquad (\text{T-INVK}) \]

\[ \dfrac{\begin{aligned} \textit{fields}(\text{C}) &= \overline{\text{DI}} \text{ } \overline{\text{f}} \\ \Gamma \vdash \overline{\text{t}}: \overline{\text{CI}} &\quad \overline{\text{CI}} <: \overline{\text{DI}} \end{aligned}}{\Gamma \vdash \text{new } \text{C}(\overline{\text{t}}): \text{C}} \qquad (\text{T-NEW}) \]

\[ \dfrac{\Gamma \vdash \text{t}_0: \text{DI} \quad \text{DI} <: \text{CI}}{ \Gamma \vdash (\text{CI})\text{t}_0: \text{CI}} \qquad (\text{T-UCAST}) \]

\[ \dfrac{\Gamma \vdash \text{t}_0: \text{DI} \quad \text{CI} <: \text{DI} \quad \text{CI} \neq \text{DI}}{ \Gamma \vdash (\text{CI})\text{t}_0: \text{CI}} \qquad (\text{T-DCAST}) \]

\[ \dfrac{\begin{aligned} \Gamma \vdash \text{t}_0 : \text{DI} &\quad \text{CI} \nless: \text{DI} \quad \text{DI} \nless: \text{CI} \\ &\textit{stupid warning} \end{aligned}}{ \Gamma \vdash (\text{CI})\text{t}_0: \text{CI}} \qquad (\text{T-SCAST}) \]

\( \text{M OK in C} \)则如下：

\[ \dfrac{\begin{aligned} &\overline{\text{x}}: \overline{\text{CI}}, \text{this}: \text{C} \vdash \text{t}_0: \text{EI}_0 \quad \text{EI}_0 <: \text{CI}_0 \\ &CT(\text{C}) = \text{class C extends D } \{ \dots \} \\ &\hphantom{CT(\text{C})} \textit{override}(\text{m}, \text{D}, \overline{\text{CI}} \to \text{CI}_0) \end{aligned}}{\text{CI}_0 \text{ } \text{m}(\overline{\text{CI}} \text{ } \overline{\text{x}}) \{ \text{return } \text{t}_0; \} \text{ OK in C}} \]

\[ \dfrac{\begin{aligned} &\overline{\text{x}}: \overline{\text{CI}}, \text{this}: \text{C} \vdash \text{t}_0: \text{EI}_0 \quad \text{EI}_0 <: \text{CI}_0 \\ CT(\text{C}) &= \text{class C extends D implements } \overline{\text{I}} \text{ } \{ \dots \} \\ &\hphantom{CT} \textit{override}(\text{m}, \text{D}, \overline{\text{CI}} \to \text{CI}_0) \\ &\forall \text{I} \in \overline{\text{I}}, \textit{override}(\text{m}, \text{I}, \overline{\text{CI}} \to \text{CI}_0) \end{aligned}}{\text{CI}_0 \text{ } \text{m}(\overline{\text{CI}} \text{ } \overline{\text{x}}) \{ \text{return } \text{t}_0; \} \text{ OK in C}} \]

最后是\( \text{C OK} \)，如下：

\[ \dfrac{\begin{aligned} \text{K} &= \text{C}(\overline{\text{DI}} \text{ } \overline{\text{g}}, \overline{\text{CI}} \text{ } \overline{\text{f}}) \text{ } \{ \text{super}(\overline{\text{g}}); \text{this}.\overline{\text{f}} = \overline{\text{f}}; \} \\ &\hphantom{aa} \textit{fields}(\text{D}) = \overline{\text{DI}} \text{ } \overline{\text{g}} \quad \overline{\text{M}} \text{ OK in C} \end{aligned}}{ \text{class C extends D } \{ \overline{\text{CI}} \text{ } \overline{\text{f}}; \text{K } \overline{\text{M}} \} \text{ OK}} \]

\[ \dfrac{\begin{aligned} \text{K} &= \text{C}(\overline{\text{DI}} \text{ } \overline{\text{g}}, \overline{\text{CI}} \text{ } \overline{\text{f}}) \text{ } \{ \text{super}(\overline{\text{g}}); \text{this}.\overline{\text{f}} = \overline{\text{f}}; \} \\ &\hphantom{aa} \textit{fields}(\text{D}) = \overline{\text{DI}} \text{ } \overline{\text{g}} \quad \overline{\text{M}} \text{ OK in C} \end{aligned}}{ \text{class C extends D implements } \overline{\text{I}} \text{ } \{ \overline{\text{CI}} \text{ } \overline{\text{f}}; \text{K } \overline{\text{M}} \} \text{ OK}} \]

解答2：

举个例子：

\[ \begin{aligned} &\text{interface A } \{ \} \\ &\text{interface B } \{ \} \\ &\text{interface C } \text{extends } \text{A}, \text{B } \{ \} \\ &\text{interface D } \text{extends } \text{A}, \text{B } \{ \} \end{aligned} \]

这里有\( \text{C}, \text{D} \)有两个共同父类型\( \text{A}, \text{B} \)，但是由于\( \text{A}, \text{B} \)之间无法比较，因此无法确认哪个是更精确的共同父类型，进而\( \text{C} \vee \text{D} \)是未定义的。

解答3：

仿照之前的做法，条件表达式的算法性类型规则应该如下：

\[ \dfrac{\Gamma \vdash \text{t}_1: \text{boolean} \quad \Gamma \vdash \text{t}_2: \text{CI}_2 \quad \Gamma \vdash \text{t}_3: \text{CI}_3}{ \Gamma \vdash (\text{t}_1 \mathop{?} \text{t}_2 : \text{t}_3): \text{CI}_2 \vee \text{CI}_3 } \]

但是根据2中的讨论，\( \text{CI}_2 \vee \text{CI}_3 \)可能是未定义的，因此不能这样做。

Java使用了一个更受限但符合直觉的规则，如下：

\[ \dfrac{\Gamma \vdash \text{t}_1: \text{boolean} \quad \Gamma \vdash \text{t}_2: \text{CI}_2 \quad \Gamma \vdash \text{t}_3: \text{CI}_3 \quad \text{CI}_2 <: \text{CI}_3}{ \Gamma \vdash (\text{t}_1 \mathop{?} \text{t}_2 : \text{t}_3): \text{CI}_2 } \]

\[ \dfrac{\Gamma \vdash \text{t}_1: \text{boolean} \quad \Gamma \vdash \text{t}_2: \text{CI}_2 \quad \Gamma \vdash \text{t}_3: \text{CI}_3 \quad \text{CI}_3 <: \text{CI}_2}{ \Gamma \vdash (\text{t}_1 \mathop{?} \text{t}_2 : \text{t}_3): \text{CI}_3 } \]

但上述两个规则不太适合于small-step风格的操作语义，特别的，PRESERVATION定理不再成立，举个例子：

\[ \begin{aligned} &\text{class A extends Object } \{ \} \\ &\text{class B extends A } \{ \text{Object b}() \text{ } \{ \text{return new Object}(); \} \} \\ &\text{t}_1 = \text{true} \\ &\text{t}_2 = \text{new A}() \\ &\text{t}_3 = \text{new B}() \\ &\text{t} = (\text{t}_1 \mathop{?} \text{t}_2 : \text{t}_3).\text{b}() \end{aligned} \]

则\( \Gamma \vdash \text{t}: \text{B}, \text{t} \rightarrow \text{t}_2.\text{b}() \)，但\( \text{t}_2.\text{b}() \)非类型良好的。

不过如果换成big-step风格的操作语义，则不会有上述问题，具体的：不存在值\( \text{v} \)使得\( \text{t} \Downarrow \text{v} \)，可得\( \text{t} \)直接为停滞项，进而不需要保证其进一步求值后的项类型良好，因为它根本不能进一步求值。

练习19.4.7

题目：

FJ includes Java’s \( \text{this} \) keyword, but omits \( \text{super} \). Show how to add it.

解答：

在考虑如何加\( \text{super} \)关键字之前，先看一个例子：

\[ \begin{aligned} &\text{class A extends Object } \{ \text{Object a}() \text{ } \{ \text{return new Object}(); \} \} \\ &\text{class B extends A } \{ \text{Object b}() \text{ } \{ \text{return super}.\text{a}(); \} \} \\ &\text{class C extends B } \{ \} \\ &(\text{new C()}).\text{b}(); \end{aligned} \]

这里我们通过\( \text{C} \)类的实例\( \text{new C}() \)调用\( \text{B} \)的\( \text{b} \)方法，在\( \text{b} \)方法的方法体中使用\( \text{super} \)关键字，虽然我们是通过\( \text{C} \)的实例调用的\( \text{b} \)，但这里\( \text{super} \)是类型为\( \text{A} \)的对象，而不是类型为\( \text{B} \)的对象，即使\( \text{C} \)的父类为\( \text{B} \)。

也就是说\( \text{super} \)关键字是依据方法所处的类在的，而不是调用方法的实例的类来的，这要求我们有办法在调用一个方法时，知道该方法所处的类，一种最直接的方法就是，要求调用方法时，显式指定方法所处的类，然后我们再在类型检查中验证该方法是否真的处于那个类以及该类是否是当前实例的类的祖先类，类似：

\[ (\text{new C()}).\text{B::b}() \]

此时我们就知道\( \text{b} \)所处的类为\( \text{B} \)，进而通过查询表\( CT \)就可以得到\( \text{B} \)的父类为\( \text{A} \)，于是就知道了\( \text{b} \)中的\( \text{super} \)应该是\( \text{A} \)类型的对象了。当然，我们还得在类型检查过程中验证\( \text{b} \)是否真的处于\( \text{B} \)以及 \( \text{B} \)是否为实例\( \text{new C}() \)的类\( \text{C} \)的祖先类，类似：

\[ \dfrac{\begin{aligned} &\Gamma \vdash \text{t}_0: \text{C}_0 \\ &\textit{mtype}(\text{m}, \text{C}_0) = \overline{\text{D}} \rightarrow \text{C} \\ &\Gamma \vdash \overline{\text{t}}: \overline{\text{C}} \quad \overline{\text{C}} <: \overline{\text{D}} \\ &\text{C}_0 <: \text{E}_0 \quad \textit{mdeclared}(\text{m}, \text{E}_0) \end{aligned}}{\Gamma \vdash \text{t}_0.\text{E}_0 \text{::m}(\overline{\text{t}}): \text{C}} \qquad (\text{T-INVK}) \]

\( \textit{mdeclared} \)的定义如下：

\[ \dfrac{\begin{aligned} CT(\text{C}) &= \text{class C extends D } \{ \overline{\text{C}} \text{ } \overline{\text{f}}; \text{K} \text{ } \overline{\text{M}} \} \\ &\hphantom{aa} \text{m is defined in } \overline{\text{M}} \end{aligned}}{mdeclared(\text{m}, \text{C})} \]

\( \textit{mtype} \)不用改，因为\( \textit{override} \)会确保整个继承链中所有同名方法的参数类型和返回值类型都是一样的。

M OK in C要修改，类型上下文得添加\( \text{super} \)，如下：

\[ \dfrac{\begin{aligned} \overline{\text{x}}: \overline{\text{C}}, &\text{this}: \text{C}, \text{super}: \text{D} \vdash \text{t}_0: \text{E}_0 \quad \text{E}_0 <: \text{C}_0 \\ &CT(\text{C}) = \text{class C extends D } \{ \dots \} \\ &\hphantom{CT} \textit{override}(\text{m}, \text{D}, \overline{\text{C}} \to \text{C}_0) \end{aligned}}{\text{C}_0 \text{ } \text{m}(\overline{\text{C}} \text{ } \overline{\text{x}}) \{ \text{return } \text{t}_0; \} \text{ OK in C}} \]

E-INVKNEW规则也要修改，方法体得从目标类\( \text{E} \)查，变量代入不仅得代入\( \text{this} \)，也得代入\( \text{super} \)，如下：

\[ \dfrac{\textit{mbody}(\text{m}, \text{E}) = (\overline{\text{x}}, \text{t}_0)}{ (\text{new } \text{C}(\overline{\text{v}})).\text{E::m}(\overline{\text{u}}) \rightarrow [\overline{\text{x}} \mapsto \overline{\text{u}}, \text{this} \mapsto \text{new } \text{C}(\overline{\text{v}}), \text{super} \mapsto \text{new } \text{C}(\overline{\text{v}})]\text{t}_0} \qquad (\text{E-INVKNEW}) \]

上面我们\( \text{super} \)也代入成\( \text{new } \text{C}(\overline{\text{v}}) \)，即类型为\( \text{C} \)的对象，而没有代入类型为\( \text{E} \)的对象，这是不要紧的，因为我们是从\( \text{E} \)中查找方法体，而M OK in E限制了\( \text{super} \)的类型为\( \text{E} \)的父类，故在类型良好的情况下，方法体中通过\( \text{super} \)只能引用到\( \text{E} \)以及它祖先类中的东西，而无法引用到\( \text{C} \)中的东西，等等。

方法调用的语法得修改下，E-INVK-RECV、E-INVK-ARG也得修改，不过仅仅是语法上的修改，这些修改就不列出来了。

章节19.5

练习19.5.1

题目：

Theorem [Preservation]: If \( \Gamma \vdash \text{t}: \text{C} \) and \( \text{t} \rightarrow \text{t}' \), then \( \Gamma \vdash \text{t}': \text{C}' \) for some \( \text{C}' <: \text{C} \).

证明：

类似之前对PRESERVATION定理的证明，我们需要先证明一些引理。

第一个引理就是之前练习中提到的，一条继承链中所有类的同名方法都是一致的，即参数类型和返回值类型完全一样。

引理1：

如果\( \textit{mtype}(\text{m}, \text{D}) = \overline{\text{C}} \to \text{C}_0 \)，则\( \forall \text{C} <: \text{D}, \textit{mtype}(\text{m}, \text{C}) = \overline{\text{C}} \to \text{C}_0 \)。

证明引理1:

引理1的成立容易直接从\( \textit{override} \)的定义以及\( \text{M OK in C} \)的定义看出来，证明也很简单。

由每个类有且仅有一个父类、继承关系是无环的、用户声明的类的数量是有限的，故给定\( \text{C} <: \text{D} \)，可得\( \exists \)一条有限的继承链\( \text{E}_1 <: \text{E}_2 <: \dots <: \text{E}_n, \text{E}_1 = \text{C}, \text{E}_n = \text{D} \)，我们称\( \text{C} \)为\( \text{D} \)的\( n \)级子类，故引理1等价于：如果\( \textit{mtype}(\text{m}, \text{D}) = \overline{\text{C}} \to \text{C}_0 \)，则\( \forall n \geq 1 \)，如果\( \text{C} \)为\( \text{D} \)的\( n \)级子类，则\( \textit{mtype}(\text{m}, \text{C}) = \overline{\text{C}} \to \text{C}_0 \)。我们转证这个等价的引理。

对\( n \)进行归纳，当\( n = 1 \)时， \( \forall \text{D} \)的\( n \)级子类\( \text{C} \)，假设\( \textit{mtype}(\text{m}, \text{C}) \neq \overline{\text{C}} \to \text{C}_0 \)，则由于\( \text{C} \)为\( \text{D} \)的\( n = 1 \)级子类，可得\( \text{C} \)直接继承于\( \text{D} \)，于是有\( CT( C) = \text{class C extends D } \{ \dots \} \)，由\( \textit{mtype}(\text{m}, \text{C}) \neq \overline{\text{C}} \to \text{C}_0 \)，可得\( \textit{override}(\text{m}, \text{D}, \textit{mtype}(\text{m}, \text{C})) \)不成立，进而可得\( \text{M OK in } \text{C} \)不成立，即\( \text{C} \)非良好定义的类，矛盾，因此假设不成立，有\( \textit{mtype}(\text{m}, \text{C}) = \overline{\text{C}} \to \text{C}_0 \)。

归纳假设当\( n = k \)时引理成立，当\( n = k + 1 \)时， \( \forall \text{D} \)的\( n \)级子类\( \text{C} \)，令\( \text{C}' \)为\( \text{C} \)的直接父类，有\( \text{C}' \)为\( \text{D} \)的\( k \)级子类，根据归纳假设，可得\( \textit{mtype}(\text{m}, \text{C}') = \overline{\text{C}} \to \text{C}_0 \)，此时假设\( \textit{mtype}(\text{m}, \text{C}) \neq \overline{\text{C}} \to \text{C}_0 \)，则\( \textit{override}(\text{m}, \text{C}', \textit{mtype}(\text{m}, \text{C})) \)不成立，进而可得\( \text{M OK in } \text{C} \)不成立，即\( \text{C} \)非良好定义的类，矛盾，因此假设不成立，有\( \textit{mtype}(\text{m}, \text{C}) = \overline{\text{C}} \to \text{C}_0 \)。

综上，归纳完毕，引理成立。

证明引理1完毕。

证毕。

还需要另外一个比较简单的引理，即我们可以随意拓展类型上下文而不影响一个项的类型。

引理2：

如果\( \Gamma \vdash \text{t}: \text{C} \)，则\( \Gamma, \text{x}: \text{D} \vdash \text{t}: \text{C} \)。

证明引理2：

归纳假设引理对\( \Gamma \vdash \text{t}: \text{C} \)推导的直接子推导成立，易证引理成立，这里省略。

证明引理2完毕。

同之前，我们需要一个引理保证代入类型匹配的项不会影响类型。

引理3：

如果\( \Gamma, \overline{\text{x}}: \overline{\text{B}} \vdash \text{t}: \text{D} \)，且\( \Gamma \vdash \overline{\text{s}}: \overline{\text{A}}, \overline{\text{A}} <: \overline{\text{B}} \)，则\( \exists \text{C} <: \text{D}, \Gamma \vdash [\overline{\text{x}} \mapsto \overline{\text{s}}]\text{t}: \text{C} \)。

证明引理3：

令\( \mathcal{C} \)为\( \Gamma, \overline{\text{x}}: \overline{\text{B}} \vdash \text{t}: \text{D} \)的推导，归纳假设引理对\( \mathcal{C} \)的直接子推导成立，我们要证明引理对\( \mathcal{C} \)成立，对\( \mathcal{C} \)最后使用的类型规则进行分类讨论：

1. 如果最后使用的规则为T-VAR，则\( \text{t} = \text{x} \quad \text{x}: \text{D} \in \Gamma, \overline{\text{x}}: \overline{\text{B}} \)：
   1. 如果\( \exists \text{x}_i \in \overline{\text{x}} \)满足\( \text{x}_i = \text{x} \)，则\( \text{D} = \text{B}_i \)，且\( [\overline{\text{x}} \mapsto \overline{\text{s}}]\text{t} = \text{s}_i \)，加上\( \Gamma \vdash \overline{\text{s}}: \overline{\text{A}}, \overline{\text{A}} <: \overline{\text{B}} \)，可得\( \Gamma \vdash [\overline{\text{x}} \mapsto \overline{\text{s}}]\text{t}: \text{A}_i, \text{A}_i <: \text{B}_i = \text{D} \)。
   2. 如果\( \nexists \text{x}_i \in \overline{\text{x}} \)满足\( \text{x}_i = \text{x} \)，则\( \text{x}: \text{D} \in \Gamma \)，且\( [\overline{\text{x}} \mapsto \overline{\text{s}}]\text{t} = \text{x} \)，进而由T-VAR，可得\( \Gamma \vdash [\overline{\text{x}} \mapsto \overline{\text{s}}]\text{t}: \text{D} \)。
2. 如果最后使用的规则为T-FIELD，则\( \text{t} = \text{t}_0.\text{g}_i \quad \Gamma, \overline{\text{x}}: \overline{\text{B}} \vdash \text{t}_0: \text{D}_0 \quad \textit{fields}(\text{D}_0) = \overline{\text{D}} \text{ } \overline{\text{g}} \quad \text{D} = \text{D}_i \)，由\( \Gamma, \overline{\text{x}}: \overline{\text{B}} \vdash \text{t}_0: \text{D}_0 \)以及归纳假设，可得\( \Gamma \vdash [\overline{\text{x}} \mapsto \overline{\text{s}}]\text{t}_0: \text{C}_0, \text{C}_0 <: \text{D}_0 \)，易得\( \textit{fields}(\text{C}_0) = (\textit{fields}(\text{D}_0), \overline{\text{C}} \text{ } \overline{\text{f}}) \)，进而由T-FIELD，可得\( \Gamma \vdash [\overline{\text{x}} \mapsto \overline{\text{s}}]\text{t}: (\text{D}_i = \text{D}) \)。
3. 如果最后使用的规则为T-INVK，则\( \text{t} = \text{t}_0.\text{m}(\overline{\text{t}}) \quad \Gamma, \overline{\text{x}}: \overline{\text{B}} \vdash \text{t}_0: \text{C}_0 \quad \textit{mtype}(\text{m}, \text{C}_0) = \overline{\text{D}} \to \text{C} \quad \Gamma, \overline{\text{x}}: \overline{\text{B}} \vdash \overline{\text{t}}: \overline{\text{C}} \quad \overline{\text{C}} <: \overline{\text{D}} \quad \text{D} = \text{C} \)，由\( \Gamma, \overline{\text{x}}: \overline{\text{B}} \vdash \text{t}_0: \text{C}_0 \)以及归纳假设，可得\( \Gamma \vdash [\overline{\text{x}} \mapsto \overline{\text{s}}]\text{t}_0: \text{D}_0, \text{D}_0 <: \text{C}_0 \)，由\( \Gamma, \overline{\text{x}}: \overline{\text{B}} \vdash \overline{\text{t}}: \overline{\text{C}} \)以及归纳假设，可得\( \Gamma \vdash [\overline{\text{x}} \mapsto \overline{\text{s}}]\overline{\text{t}}: \overline{\text{E}}, \overline{\text{E}} <: \overline{\text{C}} \)，加上\( \overline{\text{C}} <: \overline{\text{D}} \)以及子类型关系的传递性，可得\( \overline{\text{E}} <: \overline{\text{D}} \)，由\( \text{D}_0 <: \text{C}_0 \)以及引理1，可得\( \textit{mtype}(\text{m}, \text{D}_0) = \textit{mtype}(\text{m}, \text{C}_0) = \overline{\text{D}} \to \text{C} \)，进而由T-INVK，可得\( \Gamma \vdash ([\overline{\text{x}} \mapsto \overline{\text{s}}]\text{t}_0).\text{m}([\overline{\text{x}} \mapsto \overline{\text{s}}]\overline{\text{t}}): \text{D}_0 \)，即\( \Gamma \vdash [\overline{\text{x}} \mapsto \overline{\text{s}}]\text{t}: (\text{C} = \text{D}) \)。
4. 如果最后使用的规则为T-NEW，则\( \text{t} = \text{new D}(\overline{\text{t}}) \quad \textit{fields}(\text{D}) = \overline{\text{D}} \text{ } \overline{\text{f}} \quad \Gamma, \overline{\text{x}}: \overline{\text{B}} \vdash \overline{\text{t}}: \overline{\text{C}} \quad \overline{\text{C}} <: \overline{\text{D}} \)，由\( \Gamma, \overline{\text{x}}: \overline{\text{B}} \vdash \overline{\text{t}}: \overline{\text{C}} \)以及归纳假设，可得\( \Gamma \vdash [\overline{\text{x}} \mapsto \overline{\text{s}}]\overline{\text{t}}: \overline{\text{E}}, \overline{\text{E}} <: \overline{\text{C}} \)，加上\( \overline{\text{C}} <: \overline{\text{D}} \)以及子类型关系的传递性，可得\( \overline{\text{E}} <: \overline{\text{D}} \)，进而由T-NEW，可得\( \Gamma \vdash [\overline{\text{x}} \mapsto \overline{\text{s}}]\text{t}: \text{D} \)。
5. 如果最后使用的规则为T-UCAST，则\( \text{t} = (\text{D})\text{t}_0 \quad \Gamma, \overline{\text{x}}: \overline{\text{B}} \vdash \text{t}_0: \text{C} \quad \text{C} <: \text{D} \)，由\( \Gamma, \overline{\text{x}}: \overline{\text{B}} \vdash \text{t}_0: \text{C} \)以及归纳假设，可得\( \Gamma \vdash [\overline{\text{x}} \mapsto \overline{\text{s}}]\text{t}_0: \text{E}, \text{E} <: \text{C} \)，加上\( \text{C} <: \text{D} \)以及子类型关系的传递性，可得\( \text{E} <: \text{D} \)，进而由T-UCAST，可得\( \Gamma \vdash [\overline{\text{x}} \mapsto \overline{\text{s}}]\text{t}: \text{D} \)。
6. 如果最后使用的规则为T-DCAST，则\( \text{t} = (\text{D})\text{t}_0 \quad \Gamma, \overline{\text{x}}: \overline{\text{B}} \vdash \text{t}_0: \text{C} \quad \text{D} <: \text{C} \quad \text{D} \neq \text{C} \)，由\( \Gamma, \overline{\text{x}}: \overline{\text{B}} \vdash \text{t}_0: \text{C} \)以及归纳假设，可得\( \Gamma \vdash [\overline{\text{x}} \mapsto \overline{\text{s}}]\text{t}_0: \text{E}, \text{E} <: \text{C} \)：
   1. 如果\( \text{E} <: \text{D} \)，则由T-UCAST，可得\( \Gamma \vdash [\overline{\text{x}} \mapsto \overline{\text{s}}]\text{t}: \text{D} \)。
   2. 如果\( \text{D} <: \text{E} \)，则由T-DCAST，可得\( \Gamma \vdash [\overline{\text{x}} \mapsto \overline{\text{s}}]\text{t}: \text{D} \)。
   3. 如果\( \text{E} \nless: \text{D}, \text{D} \nless: \text{E} \)，则由T-SCAST，可得\( \Gamma \vdash [\overline{\text{x}} \mapsto \overline{\text{s}}]\text{t}: \text{D} \)。
7. 如果最后使用的规则为T-SCAST，则\( \text{t} = (\text{D})\text{t}_0 \quad \Gamma, \overline{\text{x}}: \overline{\text{B}} \vdash \text{t}_0: \text{C} \quad \text{D} \nless: \text{C} \quad \text{C} \nless: \text{D} \)，由\( \Gamma, \overline{\text{x}}: \overline{\text{B}} \vdash \text{t}_0: \text{C} \)以及归纳假设，可得\( \Gamma \vdash [\overline{\text{x}} \mapsto \overline{\text{s}}]\text{t}_0: \text{E}, \text{E} <: \text{C} \)，容易证明\( \text{E} \nless: \text{D} \)，假设\( \text{E} <: \text{D} \)，则由于一个类有且仅有一个父类，易得针对\( \text{E} \)的两个祖先类\( \text{C}, \text{D} \)，要么有\( \text{C} <: \text{D} \)，要么有\( \text{D} <: \text{C} \)，两种情况均矛盾，因此假设不成立，有\( \text{E} \nless: \text{D} \)，也容易证明\( \text{D} \nless: \text{E} \)，假设\( \text{D} <: \text{E} \)，则由\( \text{E} <: \text{C} \)以及子类型关系的传递性，可得\( \text{D} <: \text{C} \)，矛盾，因此假设不成立，有\( \text{D} \nless: \text{E} \)，进而由T-SCAST，可得\( \Gamma \vdash [\overline{\text{x}} \mapsto \overline{\text{s}}]\text{t}: \text{D} \)。

综上，归纳完毕，引理成立。

证明引理3完毕。

为了处理E-INVKNEW的情况，我们还需要一个引理保证方法调用的类型推导有特定的、符合直觉的性质，这包括两点：

1. 方法体的类型允许是声明的返回值类型的子类型。
2. 方法体中\( \text{this} \)的类型应该是定义该方法的类，而定义方法的可能是当前类或者当前类的祖先类，因此\( \text{this} \)的类型不一定是当前类，只能保证\( \text{this} \)的类型是当前类的祖先类（这包括当前类本身）。

引理4：

如果\( \textit{mtype}(\text{m}, \text{C}_0) = \overline{\text{D}} \to \text{D}, \textit{mbody}(\text{m}, \text{C}_0) = (\overline{\text{x}}, \text{t}) \)，则\( \exists \text{D}_0, \text{C} \)满足\( \text{C}_0 <: \text{D}_0, \text{C} <: \text{D} \)，且\( \overline{\text{x}}: \overline{\text{D}}, \text{this}: \text{D}_0 \vdash \text{t}: \text{C} \)。

证明引理4：

归纳假设引理对\( \text{C} \)的直接父类成立，我们证明引理对\( \text{C} \)成立：

\( CT(\text{C}_0) = \text{class } \text{C}_0 \text{ extends E } \{ \overline{\text{C}} \text{ } \overline{\text{f}}; \text{K} \overline{\text{M}} \} \)，由\( \textit{mtype}(\text{m}, \text{C}_0) = \overline{\text{D}} \to \text{D}, \textit{mbody}(\text{m}, \text{C}_0) = (\overline{\text{x}}, \text{t}) \)，可得方法的定义为\( \text{D m}(\overline{\text{D}} \text{ } \overline{\text{x}}) \text{ } \{ \text{return } \text{t} \} \)，分情况讨论：

1. 如果\( \text{D m}(\overline{\text{D}} \text{ } \overline{\text{x}}) \text{ } \{ \text{return } \text{t} \} \in \overline{\text{M}} \)，则由\( \text{M OK in } \text{D}_0 \)，可得\( \overline{\text{x}}: \overline{\text{D}}, \text{this}: \text{C}_0 \vdash \text{t}: \text{C}, \text{C} <: \text{D} \)，令\( \text{D}_0 = \text{C}_0, \text{C} = \text{D} \)，可得引理成立。
2. 如果\( \text{m} \notin \overline{\text{M}} \)，则\( \textit{mtype}(\text{m}, \text{C}_0) = \textit{mtype}(\text{m}, \text{E}), \textit{mbody}(\text{m}, \text{C}_0) = \textit{mbody}(\text{m}, \text{E}) \)，进而由归纳假设，可得\( \exists \text{D}_0, \text{C} \)满足\( \text{E} <: \text{D}_0, \text{C} <: \text{D} \)，且\( \overline{\text{x}}: \overline{\text{D}}, \text{this}: \text{D}_0 \vdash \text{t}: \text{C} \)，由\( \text{C} <: \text{E}, \text{E} <: \text{D}_0 \)以及子类型关系的传递性，可得\( \text{C} <: \text{D}_0 \)，至此有引理成立。

综上，归纳完毕，引理成立。

证明引理4完毕。

现在，我们可以开始证明PRESERVATION定理了：

令\( \mathcal{D} \)为\( \text{t} \rightarrow \text{t}' \)的推导，归纳假设定理对\( \mathcal{D} \)的直接子推导成立，我们要证明定理对\( \mathcal{D} \)成立，对\( \text{t} \rightarrow \text{t}' \)最后使用的求值规则进行分类讨论：

1. 如果最后使用的规则为E-PROJNEW，则\( \text{t} = (\text{new D}(\overline{\text{v}})).\text{f}_i \quad \textit{fields}(\text{D}) = \overline{\text{D}} \text{ } \overline{\text{f}} \quad \text{t}' = \text{v}_i \)，此时\( \Gamma \vdash \text{t}: \text{C} \)最后使用的规则只能是T-FIELD，可得\( \Gamma \vdash \text{new D}(\overline{\text{v}}): \text{E} \quad \textit{fields}(\text{E}) = \overline{\text{E}} \text{ } \overline{\text{g}} \quad \text{f}_i \in \overline{\text{g}} \quad \text{C} = \text{E}_i \)，而\( \Gamma \vdash \text{new D}(\overline{\text{v}}): \text{E} \)最后使用的规则只能是T-NEW，可得\( \text{E} = \text{D} \quad \Gamma \vdash \overline{\text{v}}: \overline{\text{C}} \quad \overline{\text{C}} <: \overline{\text{D}} \)，可得\( \Gamma \vdash (\text{t}' = \text{v}_i): \text{C}_i \quad \text{C}' = \text{C}_i \)，而由\( \text{E} = \text{D} \)，可得\( \textit{fields}(\text{E}) = \overline{\text{E}} \text{ } \overline{\text{g}} = \textit{fields}(\text{D}) = \overline{\text{D}} \text{ } \overline{\text{f}} \quad \text{C} = \text{E}_i = \text{D}_i \)，于是有\( (\text{C}' = \text{C}_i) <: (\text{D}_i = \text{C}) \)。
2. 如果最后使用的规则为E-INVKNEW，则\( \text{t} = (\text{new D}(\overline{\text{v}})).\text{m}(\overline{\text{u}}) \quad \textit{mbody}(\text{m}, \text{D}) = (\overline{\text{x}}, \text{t}_0) \quad \text{t}' = [\overline{\text{x}} \mapsto \overline{\text{u}}, \text{this} \mapsto \text{new D}(\overline{\text{v}})]\text{t}_0 \)，此时\( \Gamma \vdash \text{t}: \text{C} \)最后使用的规则只能是T-INVK，可得\( \Gamma \vdash \text{new D}(\overline{\text{v}}): \text{E} \quad \textit{mtype}(\text{m}, \text{E}) = \overline{\text{D}} \to \text{C} \quad \Gamma \vdash \overline{\text{u}}: \overline{\text{C}} \quad \overline{\text{C}} <: \overline{\text{D}} \)，而\( \Gamma \vdash \text{new D}(\overline{\text{v}}): \text{E} \)最后使用的规则只能是T-NEW，可得\( \text{E} = \text{D} \quad \Gamma \vdash \overline{\text{v}}: \overline{\text{E}} \quad \overline{\text{E}} <: \overline{\text{D}} \)，由\( \textit{mtype}(\text{m}, \text{D}) = \textit{mtype}(\text{m}, \text{E}) = \overline{\text{D}} \to \text{C} \quad \textit{mbody}(\text{m}, \text{D}) = (\overline{\text{x}}, \text{t}_0) \)以及引理4，可得\( \exists \text{D}_0, \text{F} \)满足\( \text{D} <: \text{D}_0 \quad \text{F} <: \text{C} \quad \overline{\text{x}}: \overline{\text{D}}, \text{this}: \text{D}_0 \vdash \text{t}_0: \text{F} \)，进而由引理2，可得\( \overline{\text{x}}: \overline{\text{D}}, \text{this}: \text{D}_0, \Gamma \vdash \text{t}_0: \text{F} \)，进一步可得，\( \Gamma, \overline{\text{x}}: \overline{\text{D}}, \text{this}: \text{D}_0 \vdash \text{t}_0: \text{F} \)，接着由\( \Gamma \vdash \overline{\text{u}}: \overline{\text{C}} \quad (\overline{\text{C}}, \text{D}) <: (\overline{\text{D}}, \text{D}_0) \)以及引理3，可得\( \exists \text{C}' <: \text{F} \quad \Gamma \vdash [\overline{\text{x}} \mapsto \overline{\text{u}}, \text{this} \mapsto \text{new D}(\overline{\text{v}})]\text{t}_0: \text{C}' \)，即\( \Gamma \vdash \text{t}': \text{C}' \)，由\( \text{C}' <: \text{F}, \text{F} <: \text{C} \)以及子类型关系的传递性，可得\( \text{C}' <: \text{C} \)。
3. 如果最后使用的规则为E-CASTNEW，则\( \text{t} = (\text{E})(\text{new } \text{D}(\overline{\text{v}})) \quad \text{D} <: \text{E} \quad \text{t}' = \text{new } \text{D}(\overline{\text{v}}) \)，从形式来看，\( \Gamma \vdash \text{t}: \text{C} \)最后使用的规则可能是T-UCAST、T-DCAST、T-SCAST，但是如果最后使用的规则是T-DCAST或者T-SCAST，则会违反\( \text{D} <: \text{E} \)，故最后使用的规则只能是T-UCAST，可得\( \Gamma \vdash (\text{t}' = \text{new } \text{D}(\overline{\text{v}})): \text{C}' \quad \text{C}' <: \text{E} \quad \text{C} = \text{E} \)，而\( \Gamma \vdash (\text{t}' = \text{new } \text{D}(\overline{\text{v}})): \text{C}' \)最后使用的规则只能是T-NEW，可得\( \text{C}' = \text{D} \)，于是有\( (\text{C}' = \text{D}) <: (\text{E} = \text{C}) \)。
4. 如果最后使用的规则为E-FIELD，则\( \text{t} = \text{t}_0.\text{f} \quad \text{t}_0 \rightarrow \text{t}'_0 \quad \text{t}' = \text{t}'_0.\text{f} \)，此时\( \Gamma \vdash \text{t}: \text{C} \)最后使用的规则只能是T-FIELD，可得\( \Gamma \vdash \text{t}_0: \text{E} \quad \textit{fields}(\text{E}) = \overline{\text{E}} \text{ } \overline{\text{g}} \quad \exists \text{g}_i \in \overline{\text{g}}, \text{g}_i = \text{f} \quad \text{C} = \text{E}_i \)，由\( \Gamma \vdash \text{t}_0: \text{E} \quad \text{t}_0 \rightarrow \text{t}'_0 \)以及归纳假设，可得\( \Gamma \vdash \text{t}'_0: \text{F} \quad \text{F} <: \text{E} \)，易得\( \textit{fields}(\text{F}) = (\textit{fields}(\text{E}), \overline{\text{G}} \text{ } \overline{\text{h}}) \)，进而由T-FIELD，可得\( \Gamma \vdash \text{t}': (\text{E}_i = \text{C}) \)。
5. 如果最后使用的规则是E-INVK-RECV，则\( \text{t} = \text{t}_0.\text{m}(\overline{\text{t}}) \quad \text{t}_0 \rightarrow \text{t}'_0 \quad \text{t}' = \text{t}'_0.\text{m}(\overline{\text{t}}) \)，此时\( \Gamma \vdash \text{t}: \text{C} \)最后使用的规则只能是T-INVK，可得\( \Gamma \vdash \text{t}_0: \text{E} \quad \textit{mtype}(\text{m}, \text{E}) = \overline{\text{D}} \to \text{C} \quad \Gamma \vdash \overline{\text{t}}: \overline{\text{C}} \quad \overline{\text{C}} <: \overline{\text{D}} \)，由\( \Gamma \vdash \text{t}_0: \text{E} \quad \text{t}_0 \rightarrow \text{t}'_0 \)以及归纳假设，可得\( \Gamma \vdash \text{t}'_0: \text{F} \quad \text{F} <: \text{E} \)，由\( \text{F} <: \text{E} \)以及引理1，可得\( \textit{mtype}(\text{m}, \text{F}) = \textit{mtype}(\text{m}, \text{E}) \)，进而由T-INVK，可得\( \Gamma \vdash \text{t}': \text{C} \)。
6. 如果最后使用的规则是E-INVK-ARG，则\( \text{t} = \text{v}_0.\text{m}(\overline{\text{v}}, \text{t}_i, \overline{\text{t}}) \quad \text{t}_i \rightarrow \text{t}'_i \quad \text{t}' = \text{v}_0.\text{m}(\overline{\text{v}}, \text{t}'_i, \overline{\text{t}}) \)，此时\( \Gamma \vdash \text{t}: \text{C} \)最后使用的规则只能是T-INVK，可得\( \Gamma \vdash \text{v}_0: \text{E} \quad \textit{mtype}(\text{m}, \text{E}) = \overline{\text{D}} \to \text{C} \quad \Gamma \vdash (\overline{\text{v}}, \text{t}_i, \overline{\text{t}}): (\overline{\text{D}}, \text{F}, \overline{\text{C}}) \quad (\overline{\text{D}}, \text{F}, \overline{\text{C}}) <: \overline{\text{D}} \)，由\( \Gamma \vdash (\overline{\text{v}}, \text{t}_i, \overline{\text{t}}): (\overline{\text{D}}, \text{F}, \overline{\text{C}}) \)，有\( \Gamma \vdash \text{t}_i: \text{F} \)，由\( \Gamma \vdash \text{t}_i: \text{F} \quad \text{t}_i \rightarrow \text{t}'_i \)以及归纳假设，可得\( \Gamma \vdash \text{t}'_i: \text{G} \quad \text{G} <: \text{F} \)，再由\( \text{F} <: \text{D}_i \)以及子类型关系的传递性，可得\( \text{G} <: \text{D}_i \)，于是有\( \Gamma \vdash (\overline{\text{v}}, \text{t}'_i, \overline{\text{t}}): (\overline{\text{D}}, \text{G}, \overline{\text{C}}) \quad (\overline{\text{D}}, \text{G}, \overline{\text{C}}) <: \overline{\text{D}} \)，进而由T-INVK，可得\( \Gamma \vdash \text{t}': \text{C} \)。
7. 如果最后使用的规则是E-NEW-ARG，则\( \text{t} = \text{new D}(\overline{\text{v}}, \text{t}_i, \overline{\text{t}}) \quad \text{t}_i \rightarrow \text{t}'_i \quad \text{t}' = \text{new D}(\overline{\text{v}}, \text{t}'_i, \overline{\text{t}}) \)，此时\( \Gamma \vdash \text{t}: \text{C} \)最后使用的规则只能是T-NEW，可得\( \textit{fields}(\text{D}) = \overline{\text{D}} \text{ } \overline{\text{f}} \quad \Gamma \vdash (\overline{\text{v}}, \text{t}'_i, \overline{\text{t}}): (\overline{\text{E}}, \text{F}, \overline{\text{C}}) \quad (\overline{\text{E}}, \text{F}, \overline{\text{C}}) <: \overline{\text{D}} \quad \text{C} = \text{D} \)，由\( \Gamma \vdash (\overline{\text{v}}, \text{t}_i, \overline{\text{t}}): (\overline{\text{E}}, \text{F}, \overline{\text{C}}) \)，有\( \Gamma \vdash \text{t}_i: \text{F} \)，由\( \Gamma \vdash \text{t}_i: \text{F} \quad \text{t}_i \rightarrow \text{t}'_i \)以及归纳假设，可得\( \Gamma \vdash \text{t}'_i: \text{G} \quad \text{G} <: \text{F} \)，再由\( \text{F} <: \text{D}_i \)以及子类型关系的传递性，可得\( \text{G} <: \text{D}_i \)，于是有\( \Gamma \vdash (\overline{\text{v}}, \text{t}'_i, \overline{\text{t}}): (\overline{\text{E}}, \text{G}, \overline{\text{C}}) \quad (\overline{\text{E}}, \text{G}, \overline{\text{C}}) <: \overline{\text{D}} \)，进而由T-NEW，可得\( \Gamma \vdash \text{t}': (\text{D} = \text{C}) \)。
8. 如果最后使用的规则为E-CAST，则\( \text{t} = (\text{D})\text{t}_0 \quad \text{t}_0 \rightarrow \text{t}'_0 \quad \text{t}' = (\text{D})\text{t}'_0 \)，此时\( \Gamma \vdash \text{t}: \text{C} \)最后使用的规则可能是T-UCAST、T-DCAST、T-SCAST：
   1. 如果\( \Gamma \vdash \text{t}: \text{C} \)最后使用的规则是T-UCAST，则\( \Gamma \vdash \text{t}_0: \text{E} \quad \text{E} <: \text{D} \quad \text{D} = \text{C} \)，由\( \Gamma \vdash \text{t}_0: \text{E} \quad \text{t}_0 \rightarrow \text{t}'_0 \)以及归纳假设，可得\( \Gamma \vdash \text{t}'_0: \text{F} \quad \text{F} <: \text{E} \)，再由\( \text{E} <: \text{D} \)以及子类型关系的传递性，可得\( \text{F} <: \text{D} \)，进而由T-UCAST，可得\( \Gamma \vdash \text{t}': (\text{D} = \text{C}) \)。
   2. 如果\( \Gamma \vdash \text{t}: \text{C} \)最后使用的规则是T-DCAST，则\( \Gamma \vdash \text{t}_0: \text{E} \quad \text{D} <: \text{E} \quad \text{D} = \text{C} \)，由\( \Gamma \vdash \text{t}_0: \text{E} \quad \text{t}_0 \rightarrow \text{t}'_0 \)以及归纳假设，可得\( \Gamma \vdash \text{t}'_0: \text{F} \quad \text{F} <: \text{E} \)：
      1. 如果\( \text{F} <: \text{D} \)，则由T-UCAST，可得\( \Gamma \vdash \text{t}': (\text{D} = \text{C}) \)。
      2. 如果\( \text{D} <: \text{F} \)，则由T-DCAST，可得\( \Gamma \vdash \text{t}': (\text{D} = \text{C}) \)。
      3. 如果\( \text{F} \nless: \text{D} \quad \text{D} \nless: \text{F} \)，则由T-SCAST，可得\( \Gamma \vdash \text{t}': (\text{D} = \text{C}) \)。
   3. 如果\( \Gamma \vdash \text{t}: \text{C} \)最后使用的规则是T-SCAST，则\( \Gamma \vdash \text{t}_0: \text{E} \quad \text{E} \nless: \text{D} \quad \text{D} \nless: \text{E} \quad \text{D} = \text{C} \)，由\( \Gamma \vdash \text{t}_0: \text{E} \quad \text{t}_0 \rightarrow \text{t}'_0 \)以及归纳假设，可得\( \Gamma \vdash \text{t}'_0: \text{F} \quad \text{F} <: \text{E} \)，假设\( \text{F} <: \text{D} \)，则由于一个类有且仅有一个父类，易得针对\( \text{F} \)的两个祖先类\( \text{D}, \text{E} \)，要么有\( \text{D} <: \text{E} \)，要么有\( \text{E} <: \text{D} \)，两种情况均矛盾，因此假设不成立，有\( \text{F} \nless: \text{D} \)，假设\( \text{D} <: \text{F} \)，则由\( \text{F} <: \text{E} \)以及子类型关系的传递性，可得\( \text{D} <: \text{E} \)，矛盾，综上，有\( \text{F} \nless: \text{D} \quad \text{D} \nless: \text{F} \)，进而由T-SCAST，可得\( \Gamma \vdash \text{t}': (\text{D} = \text{C}) \)。

综上，归纳完毕，定理成立。

证毕。

练习19.5.5

题目：

Starting from one of the lambda-calculus typecheckers, build a typechecker and interpreter for Featherweight Java.

解答：

跳过。

练习19.5.6

题目：

The original FJ paper (Igarashi, Pierce, and Wadler, 1999) also formalizes polymorphic types in the style of GJ. Extend the typechecker and interpreter from Exercise 19.5.5 to include these features. (You will need to read Chapters 23, 25, 26, and 28 before attempting this exercise.)

解答：

跳过。