第12章 章节12.1 练习12.1.1 题目： Where do we fail if we attempt to prove normalization by a straightforward induction on the size of a well-typed term? 解答： 在处理使用求值规则E-APPABS的情况会出问题，

第11章 章节11.2 练习11.2.1 题目： Is there a way of constructing a sequence of terms \( \text{t}_1, \text{t}_2, \dots \), in the simply typed lambda-calculus with only the base type Unit, such that, for each \( n \), the term \( \text{t}_n \) as size at most \( O(n) \) but requires at least

第9章 章节9.2 练习9.2.1 题目： The pure simply typed lambda-calculus with no base types is actually degenerate, in the sense that it has no well-typed terms at all. Why? 解答： 去掉基础类型后，类型\( \text{T} \)的语法只剩下： \[ \text{T} ::=

第8章 章节8.2 练习8.2.3 题目： Prove that every subterm of a well-typed term is well typed. 证明： \( \forall \)类型良好的项\( \text{t}: \text{R} \)，我们对\( \text{t} \)的形式进行分类讨论： 如果\

第6章 章节6.1 练习6.1.1 题目： For each of the following combinators \( \text{c}_0 = \lambda \text{s. } \lambda \text{z. } \text{z} \); \( \text{c}_2 = \lambda \text{s. } \lambda \text{z. } \text{s (s z)} \); \( \text{plus} = \lambda \text{m. } \lambda \text{n. } \lambda \text{s. } \lambda \text{z. } \text{m s (n s z)} \) \(

第5章 章节5.2 练习5.2.1 题目： Define logical \( \text{or} \) and \( \text{not} \) functions. 解答： 逻辑或函数：\( \text{or} = \lambda \text{b. } \lambda \text{c. } \text{b tru c} \) 逻辑非函数：\( \text{not} = \lambda \text{b. } \text{b fls tru} \) 练习