第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}$ 练习