第21章 章节21.1 练习21.1.7 题目： Suppose a generating function \( E_2 \) on the universe \( \{ a, b, c \} \) is defined by the following inference rules: \[ \dfrac{}{a} \quad \dfrac{c}{b} \quad \dfrac{a \quad b}{c} \] Write out the set of pairs in the relation \( E_2 \) explicitly, as we did

第20章 章节20.1 练习20.1.1 题目： One presentation of labeled binary trees defines a tree to be either a leaf (with no label) or else an interior node with a numeric label and two child trees. Define a type \( \text{NatTree} \) and suitable operations for constructing, destructing, and testing trees. Write a function that

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