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

第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} ::= \text{T} \to \text{T} \qquad \textit{type of functions} \]

该语法缺少基础情况，无法生成任何实际类型。

练习9.2.2

题目：

Show (by drawing derivation trees) that the following terms have the indicated types:

1. \( \text{f}: \text{Bool} \to \text{Bool} \vdash \text{f } (\text{if false then true else false}): \text{Bool} \)
2. \( \text{f}: \text{Bool} \to \text{Bool} \vdash \lambda \text{x}: \text{Bool. } \text{f } (\text{if x then false else x}): \text{Bool} \to \text{Bool} \)

解答：

解答1：

\[ \dfrac{\dfrac{\text{f}: \text{Bool} \to \text{Bool} \in \text{f}: \text{Bool} \to \text{Bool}}{ \text{f}: \text{Bool} \to \text{Bool} \vdash \text{f}: \text{Bool} \to \text{Bool}} \text{T-VAR} \quad \dfrac{\dfrac{}{\text{f}: \text{Bool} \to \text{Bool} \vdash \text{false}: \text{Bool}} \text{T-FALSE} \quad \dfrac{}{\text{f}: \text{Bool} \to \text{Bool} \vdash \text{true}: \text{Bool}} \text{T-TRUE} \quad \dfrac{}{\text{f}: \text{Bool} \to \text{Bool} \vdash \text{false}: \text{Bool}} \text{T-FALSE}}{ \text{f}: \text{Bool} \to \text{Bool} \vdash \text{if false then true else false}: \text{Bool}} \text{T-IF}}{ \text{\text{f}}: \text{Bool} \to \text{Bool} \vdash \text{f } (\text{if false then true else false}): \text{Bool}} \text{T-APP} \]

解答2：

\[ \dfrac{\dfrac{\dfrac{\text{f}: \text{Bool} \to \text{Bool} \in \text{f}: \text{Bool} \to \text{Bool}, \text{x}: \text{Bool}}{ \text{f}: \text{Bool} \to \text{Bool}, \text{x}: \text{Bool} \vdash \text{f}: \text{Bool} \to \text{Bool}} \text{T-VAR} \quad \dfrac{\dfrac{\text{x}: \text{Bool} \in \text{f}: \text{Bool} \to \text{Bool}, \text{x}: \text{Bool}}{ \text{f}: \text{Bool} \to \text{Bool}, \text{x}: \text{Bool} \vdash \text{x}: \text{Bool}} \text{T-VAR} \quad \dfrac{}{\text{f}: \text{Bool} \to \text{Bool}, \text{x}: \text{Bool} \vdash \text{false}: \text{Bool}} \text{T-FALSE} \quad \dfrac{\text{x}: \text{Bool} \in \text{f}: \text{Bool} \to \text{Bool}, \text{x}: \text{Bool}}{ \text{f}: \text{Bool} \to \text{Bool}, \text{x}: \text{Bool} \vdash \text{x}: \text{Bool}} \text{T-VAR}}{ \text{f}: \text{Bool} \to \text{Bool}, \text{x}: \text{Bool} \vdash \text{if x then false else x}: \text{Bool}} \text{T-IF}}{ \text{f}: \text{Bool} \to \text{Bool}, \text{x}: \text{Bool} \vdash \text{f } (\text{if x then false else x}): \text{Bool}} \text{T-APP}}{ \text{f}: \text{Bool} \to \text{Bool} \vdash \lambda \text{x}: \text{Bool. } \text{f } (\text{if x then false else x}): \text{Bool} \to \text{Bool}} \text{T-ABS} \]

练习9.2.3

题目：

Find a context \( \Gamma \) under which the term \( \text{f x y} \) has type \( \text{Bool} \). Can you give a simple description of the set of all such contexts?

解答：

所有满足\( \text{f}: \text{T}_1 \to \text{T}_2 \to \text{Bool} \in \Gamma, \text{x}: \text{T}_1 \in \Gamma, \text{y}: \text{T}_2 \in \Gamma \)的环境\( \Gamma \)，这里\( \text{T}_1, \text{T}_2 \)为任意类型。

举两个例子：

1. \( \Gamma = \text{f}: \text{Bool} \to \text{Bool} \to \text{Bool}, \text{x}: \text{Bool}, \text{y}: \text{Bool} \)
2. \( \Gamma = \text{f}: \text{Bool} \to \text{Bool} \to \text{Bool}, \text{x}: \text{Bool}, \text{y}: \text{Bool}, \text{z}: \text{Bool} \)

章节9.3

练习9.3.2

题目：

Is there any context \( \Gamma \) and type \( \text{T} \) such that \( \Gamma \vdash \text{x x}: \text{T} \)? If so, give \( \Gamma \) and \( \text{T} \) and show a typing derivation for \( \Gamma \vdash \text{x x}: \text{T} \); if not, prove it.

证明：

仿照定义3.3.2，易定义类型的大小函数\( \mathit{size} \)。

假设存在类型上下文\( \Gamma \)以及类型\( \text{T} \)满足\( \Gamma \vdash \text{x x}: \text{T} \)，则根据引理9.3.1，可得\( \Gamma \vdash \text{x}: \text{T}_1 \to \text{T}_2, \Gamma \vdash \text{x}: \text{T}_1 \)，由于\( \Gamma \)是函数，针对给定输入\( \text{x} \)只能给出一个输出\( \Gamma(\text{x}) \)，因此\( \text{T}_1 = \text{T}_1 \to \text{T}_2 = \Gamma(\text{x}) \)，但是这意味着\( \mathit{size}(\text{T}_1) = \mathit{size}(\text{T}_1 \to \text{T}_2) = \mathit{size}(\text{T}_1) + \mathit{size}(\text{T}_2) + 1 \)，解得\( \mathit{size}(\text{T}_2) = -1 \)（注意，如果大小允许无限大，则\( \mathit{size}(\text{T}_1) \)等可能不是数，此时不能做减法去解等式，但是目前我们\( \mathit{size} \)的定义下所有项的大小都是有限的），然而\( \text{T}_2 \)的大小不可能\( \leq 0 \)，矛盾，因此假设不成立，不存在满足条件的类型上下文以及类型。

证毕。

练习9.3.3

题目：

证明定理（Uniqueness of Types）：

In a given typing context \( \Gamma \), a term \( \text{t} \) (with free variables all in the domain of \( \Gamma \) ) has at most one type. That is, if a term is typable, then its type is unique. Moreover, there is just one derivation of this typing built from the inference rules that generate the typing relation.

证明：

如果\( \Gamma \vdash \text{t}: \text{T}, \Gamma \vdash \text{t}: \text{S} \)，则我们证明\( \text{T} = \text{S} \)且\( \Gamma \vdash \text{t}: \text{T} \)的推导是唯一的，归纳假设命题对\( \text{t} \)的直接子项成立，我们要证明命题对\( \text{t} \)成立，对\( \text{t} \)的形式分情况进行讨论：

1. 如果\( \text{t} = \text{x} \)，则根据引理9.3.1，可得 \( \text{x}: \text{T}, \text{x}: \text{S} \in \Gamma \)，而\( \Gamma \)为函数，因此\( \text{T} = \text{S} = \Gamma(\text{x}) \)。除此之外，唯一能推导出\( \text{x}: \text{T} \)的规则只有T-VAR，该规则的前提条件固定为\( \text{x}: \text{T} \in \Gamma \)，在给定上下文为\( \Gamma \)的情况下没有变动的空间，因此\( \Gamma \vdash \text{t}: \text{T} \)的推导是唯一的。
2. 如果\( \text{t} = \text{true, false} \)，则根据引理9.3.1，可得\( \text{T} = \text{S} = \text{Bool} \)，除此之外，唯一能推导出\( \Gamma \vdash \text{true}: \text{Bool} \)的规则只有T-TRUE，唯一能推导出\( \Gamma \vdash \text{false}: \text{Bool} \)的规则只有T-FALSE，加上T-TRUE、T-FALSE规则没有前提条件，没有变动的空间，可得\( \Gamma \vdash \text{t}: \text{T} \)的推导是唯一的。
3. 如果\( \text{t} = \text{if } \text{t}_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3 \)，则根据引理9.3.1，可得\( \Gamma \vdash \text{t}_1: \text{Bool}, \Gamma \vdash \text{t}_2: \text{T}, \Gamma \vdash \text{t}_3: \text{T} \)，根据归纳假设，可得\( \text{t}_1, \text{t}_2, \text{t}_3 \)在给定上下文\( \Gamma \)的情况下的类型和类型的推导都是唯一的，进而根据唯一可用的规则T-IF，可得\( \text{t} \)在给定上下文\( \Gamma \)的情况下的类型和推导也都是唯一的。
4. 如果\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)，则根据引理9.3.1，可得\( \Gamma \vdash \text{t}_1: \text{T}_2 \to \text{T}, \Gamma \vdash \text{t}_2: \text{T}_2 \)，根据归纳假设，可得\( \text{t}_1, \text{t}_2 \)在给定上下文\( \Gamma \)的情况下的类型和类型的推导都是唯一的，进而根据唯一可用的规则T-APP，可得\( \text{t} \)在给定上下文\( \Gamma \)的情况下的类型和推导也都是唯一的。
5. 如果\( \text{t} = \lambda \text{x}: \text{T}_1 \text{. } \text{t}_2 \) 则根据引理9.3.1，可得\( \text{T} = \text{T}_1 \to \text{T}_2, \Gamma, \text{x}: \text{T}_1 \vdash \text{t}_2: \text{T}_2 \)，根据归纳假设，可得\( \text{t}_2 \)在给定上下文\( \Gamma, \text{x}: \text{T}_1 \)的情况下的类型和类型的推导都是唯一的（注：我们命题中没有限定上下文，因此在使用归纳假设时，上下文可以是\( \Gamma, \text{x}: \text{T}_1 \)，不一定要是\( \Gamma \)），进而根据唯一可用的规则T-ABS，可得\( \text{t} \)在给定上下文\( \Gamma \)的情况下的类型和推导也都是唯一的。

综上，命题对\( \text{t} \)成立，归纳完毕。

证毕。

练习9.3.9

题目：

证明定理（PRESERVATION）：

If \( \Gamma \vdash \text{t}: \text{T} \) and \( \text{t} \rightarrow \text{t}' \), then \( \Gamma \vdash \text{t}': \text{T} \).

证明：

使用结构归纳法证明，归纳假设命题对\( \text{t} \)的直接子项成立，我们要证明命题对\( \text{t} \)成立，对\( \text{t} \)的形式分情况进行讨论：

1. 首先，\( \text{t} \neq \text{true, false}, \lambda \text{y}: \text{T}_1 \text{. } \text{t}_1, \text{x} \)，因为这几种形式下\( \text{t} \)为范式，和\( \text{t} \rightarrow \text{t}' \)矛盾。
2. 如果\( \text{t} = \text{if } \text{t}_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3 \)，则根据引理9.3.1，可得\( \Gamma \vdash \text{t}_1: \text{Bool}, \Gamma \vdash \text{t}_2: \text{T}, \Gamma \vdash \text{t}_3: \text{T} \)：
   1. 如果\( \text{t}_1 = \text{true} \)，则\( \text{t}' = \text{t}_2 \)，可得\( \Gamma \vdash (\text{t}' = \text{t}_2): \text{T} \)。
   2. 如果\( \text{t}_1 = \text{false} \)，则\( \text{t}' = \text{t}_3 \)，可得\( \Gamma \vdash (\text{t}' = \text{t}_3): \text{T} \)。
   3. 如果\( \text{t}_1 \neq \text{true, false} \)，则\( \text{t} \rightarrow \text{t}' \)能使用的求值规则就只有E-IF了，可得\( \text{t}_1 \rightarrow \text{t}'_1, \text{t}' = \text{if } \text{t}'_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3 \)，由\( \text{t}_1 \rightarrow \text{t}'_1, \Gamma \vdash \text{t}_1: \text{Bool} \)以及归纳假设，可得\( \Gamma \vdash \text{t}'_1: \text{Bool} \)，进而根据类型规则T-IF，可得\( \Gamma \vdash \text{t}': \text{T} \)。
3. 如果\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)，根据引理9.3.1，可得\( \Gamma \vdash \text{t}_1: \text{T}_2 \to \text{T}, \Gamma \vdash \text{t}_2: \text{T}_2 \)：
   1. 如果\( \text{t}_1 \)不为值，则\( \text{t} \rightarrow \text{t}' \)能使用的求值规则就只有E-APP1了，可得\( \text{t}_1 \rightarrow \text{t}'_1, \text{t}' = \text{t}'_1 \text{ } \text{t}_2 \)，由\( \text{t}_1 \rightarrow \text{t}'_1, \Gamma \vdash \text{t}_1: \text{T}_2 \to \text{T} \)以及归纳假设，可得\( \Gamma \vdash \text{t}'_1: \text{T}_2 \to \text{T} \)，进而根据类型规则T-APP，可得\( \Gamma \vdash \text{t}': \text{T} \)。
   2. 如果\( \text{t}_1 \)为值，则由引理9.3.4，可得\( \text{t}_1 = \lambda \text{y}: \text{T}_2 \text{. } \text{t}_{11} \)：
      1. 如果\( \text{t}_2 \)不为值，则\( \text{t} \rightarrow \text{t}' \)能使用的求值规则就只有E-APP2了，可得\( \text{t}_2 \rightarrow \text{t}'_2, \text{t}' = \text{t}_1 \text{ } \text{t}'_2 \)，由\( \text{t}_2 \rightarrow \text{t}'_2, \Gamma \vdash \text{t}_2: \text{T}_2 \)以及归纳假设，可得\( \Gamma \vdash \text{t}'_2: \text{T}_2 \)，进而根据类型规则T-APP，可得\( \Gamma \vdash \text{t}': \text{T} \)。
      2. 如果\( \text{t}_2 \)为值，则\( \text{t} \rightarrow \text{t}' \)能使用的求值规则就只有E-APPABS了，可得\( \text{t}' = [\text{y} \mapsto \text{t}_2]\text{t}_{11} \)，由\( \Gamma \vdash \text{t}_1: \text{T}_2 \to \text{T} \)以及引理9.3.1，可得\( \Gamma, \text{y}: \text{T}_2 \vdash \text{t}_{11}: \text{T} \)，加上\( \Gamma \vdash \text{t}_2: \text{T}_2 \)，根据引理9.3.8，可得\( \Gamma \vdash \text{t}': \text{T} \)。

综上，命题对\( \text{t} \)成立，归纳完毕。

证毕。

练习9.3.10

题目：

In Exercise 8.3.6 we investigated the subject expansion property for our simple calculus of typed arithmetic expressions. Does it hold for the “functional part” of the simply typed lambda-calculus? That is, suppose \( \text{t} \) does not contain any conditional expressions. Do \( \text{t} \rightarrow \text{t}' \) and \( \Gamma \vdash \text{t}': \text{T} \) imply \( \Gamma \vdash \text{t}: \text{T} \)?

解答：

subject expansion性质仍然不成立，反例如下：最简单的，给定任意类型上下文\( \Gamma \)，令\( \text{t}_1 = \lambda \text{x}: \text{Bool. } \text{x} \)，令\( \text{t} = \text{t}_1 \text{ } \text{t}_1 \)，则由于\( \text{t}_1 \)要求它参数的类型是\( \text{Bool} \)，而它接收到的实际参数\( \text{t}_1 \)的类型却是个函数类型，非\( \text{Bool} \)，进而无法使用类型规则T-APP，然而这是\( \text{t} \)这种形式的项唯一能使用的规则，因此\( \text{t} \)不是类型良好的，而\( \text{t} \rightarrow \text{t}' = \text{t}_1, \Gamma \vdash \text{t}': \text{Bool} \to \text{Bool} \)，即求值后的\( \text{t}' \)是类型良好的，违反了subject expansion性质。

章节9.4

练习9.4.1

题目：

Which of the rules for the type \( \text{Bool} \) in Figure 8-1 are introduction rules and which are elimination rules? What about the rules for \( \text{Nat} \) in Figure 8-2?

解答：

回顾书中原文：

The “\( \rightarrow \)” type constructor comes with typing rules of two kinds:

1. an introduction rule (T-ABS) describing how elements of the type can be created, and
2. an elimination rule (T-APP) describing how elements of the type can be used.

书中将T-ABS归类为引入规则，将T-APP归类为消去规则的动机很好理解， T-ABS使用参数类型\( \text{A} \)、返回值类型\( \text{B} \)和类型构造器\( \rightarrow \) 构造/引入 了新类型\( \text{A} \to \text{B} \)， T-APP则在已知函数类型为\( \text{A} \to \text{B} \)以及实际参数的类型为\( \text{A} \)的情况下， 简化/消去 了类型\( \text{A} \)，仅留下类型\( \text{B} \)。但是类似T-IF、T-SUCC、T-PRED这样的规则则不能按这种方法归类为引入规则、消去规则，原因是这些规则中用到的类型\( \text{Bool}, \text{Nat} \)都是固定的实际类型，没有用到类似\( \rightarrow \)这样给类型作为参数构造出新类型的类型构造器，进而没有类似T-ABS、T-APP这样引入类型、消去类型的过程，而且注意到上面给出的书中原文内容，不管是引入规则还是消去规则，都用了"elements of the type"，即类型的元素这个短语，比如\( \text{A} \to \text{B} \) 这个类型的元素，或者说这个类型的组成元素就是\( \text{A} \)和\( \text{B} \)，而\( \text{Bool}, \text{Nat} \)这种不带类型构造器的类型就完全没有“类型的元素”的概念，那作者自己到底是按什么逻辑将T-IF、T-SUCC、T-PRED等规则分类成引入类型或者消去类型的呢？看下书中给出的参考答案，可以发现归类的关键在于书中的下面这句话：

When an introduction form (\( \lambda \)) is an immediate subterm of an elimination form (application), the result is a redex—an opportunity for computation.

即如果一个规则的结论中的项\( \text{t} \)的直接子项为引入规则引入的项时，则\( \text{t} \) 本身 会是redex，也就是计算的机会，则我们视该规则为消去规则，注意下，这里我们视E-IFTRUE、E-IFFALSE等为计算规则，E-IF为相似（congruence）规则，故只有redex使用的是E-IFTRUE、E-IFFALSE等计算规则时，我们才称之为计算的机会。引入规则则比较好识别，基本上就是不带前提条件的公理，比如T-TRUE、T-ZERO等，至于T-SUCC，等下讨论。

综上，T-TRUE、T-FALSE、T-ZERO为引入规则，T-IF、T-ISZERO为消去规则，至于T-SUCC、T-PRED，这里由于T-PRED结论中的项\( \text{t} = \text{pred } \text{t}_1 \)在 \( \text{t}_1 \)为T-SUCC结论中项的形式，即\( \text{t}_1 = \text{succ } \text{t}_{11} \)时，则\( \text{t} \)可以使用计算规则E-PREDSUCC进行求值，故我们将T-PRED归类为消去规则， T-SUCC归类为引入规则。

读到这里，读者可能会觉得有点扯，说实话，以我目前的知识，我也不知道作者这样强行把不含类型构造器的类型归类为引入规则、消去规则有什么用。