第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? 解答： 因为我们在语法

第18章 章节18.6 练习18.6.1 题目： Write a subclass of \( \text{resetCounterClass} \) with an additional method \( \text{dec} \) that subtracts one from the current value stored in the counter. Use the \( \text{fullref} \) checker to test your new class. 解答： \[ \begin{aligned} &\text{DecCounter} = \{ \text{get}: \text{Unit} \to \text{Nat}, \text{inc}:

第16章 章节16.1 练习16.1.2 题目： LEMMA: \( \text{S} <: \text{S} \) can be derived for every type \( \text{S} \) without using S-REFL. If \( \text{S} <: \text{T} \) is derivable, then it can be derived without using S-TRANS. 证明： 证明1： 归纳假设命题对\

第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由于在形式

第14章 章节14.1 练习14.1.1 题目： Wouldn’t it be simpler just to require the programmer to annotate error with its intended type in each context where it is used? 解答： 求值规则E-APPERR1、E-APPERR2

第13章 章节13.1 练习13.1.1 题目： Draw a similar diagram showing the effects of evaluating the expressions \( \text{a} = \{ \text{ref } 0, \text{ref } 0 \} \) and \( \text{b} = (\lambda \text{x}: \text{Ref Nat. } \{ \text{x}, \text{x} \}) \text{ } (\text{ref } 0) \). 解答： 练习13