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

第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} \)的形式进行分类讨论：

1. 如果\( \text{t} = \text{true, false, 0} \)，则\( \text{t} \)没有子项，直接有\( \text{t} \)的所有子项都是类型良好的。
2. 如果\( \text{t} = \text{if } \text{t}_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3 \)，则根据引理8.2.2，可得\( \text{t}_1: \text{Bool}, \text{t}_2: \text{R}, \text{t}_3: \text{R} \)，即\( \text{t} \)的三个子项都是类型良好的。
3. 如果\( \text{t} = \text{succ } \text{t}_1, \text{pred } \text{t}_1, \text{iszero } \text{t}_1 \)，则根据引理8.2.2，可得\( \text{t}_1: \text{Nat} \)，即\( \text{t} \)的唯一子项是类型良好的。

证毕。

章节8.3

练习8.3.4

题目：

Restructure this proof so that it goes by induction on evaluation derivations rather than typing derivations.

注：

题目要求重写定理8.3.3的证明，改写成对求值推导进行归纳（归纳假设命题对所有直接子推导成立）。

定理8.3.3的内容如下：

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

解答：

令\( \mathcal{D} \)为\( \text{t} \rightarrow \text{t}' \)的推导，归纳假设命题对\( \mathcal{D} \)的所有直接子推导成立，我们要证明命题对\( \mathcal{D} \)成立，我们对\( \text{t} \)的形式进行分情况讨论：

1. \( \text{t} \)不可能\( = \{ \text{true, false, 0}, \text{succ } \text{nv}_1 \} \)，因为这些值为范式，和\( \text{t} \rightarrow \text{t}' \)矛盾。
2. 如果\( \text{t} = \text{if } \text{t}_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3 \)，则根据引理8.2.2，可得\( \text{t}_1: \text{Bool}, \text{t}_2: \text{T}, \text{t}_3: \text{T} \)：
   1. 如果\( \text{t}_1 = \text{true} \)，则\( \text{t} \rightarrow \text{t}' \)能使用的求值规则就只有E-IFTRUE了，可得\( \text{t}' = \text{t}_2: \text{T} \)。
   2. 如果\( \text{t}_2 = \text{false} \)，则\( \text{t} \rightarrow \text{t}' \)能使用的求值规则就只有E-IFFALSE了，可得\( \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: \text{Bool}, \text{t}_1 \rightarrow \text{t}'_1 \)以及归纳假设，可得\( \text{t}'_1: \text{Bool} \)，进而由\( \text{t}_2: \text{T}, \text{t}_3: \text{T} \)以及类型规则T-IF，可得\( \text{t}' = \text{if } \text{t}'_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3: \text{T} \)。
3. 如果\( \text{t} = \text{succ } \text{t}_1 \)，则\( \text{t} \rightarrow \text{t}' \)能使用的求值规则就只有E-SUCC了，可得\( \text{t}_1 \rightarrow \text{t}'_1, \text{t}' = \text{succ } \text{t}'_1 \)，根据引理8.2.2，可得\( \text{t}: \text{Nat}, \text{t}_1: \text{Nat} \)，由\( \text{t}_1: \text{Nat}, \text{t}_1 \rightarrow \text{t}'_1 \)，可得\( \text{t}'_1: \text{Nat} \)，进而由类型规则T-SUCC，可得\( \text{t}' = \text{succ } \text{t}'_1: \text{Nat} \)。
4. 如果\( \text{t} = \text{pred } \text{t}_1 \)，则根据引理8.2.2，可得\( \text{t}: \text{Nat}, \text{t}_1: \text{Nat} \)：
   1. 如果\( \text{t}_1 = 0 \)，则\( \text{t} \rightarrow \text{t}' \)能使用的求值规则就只有E-PREDZERO了，可得\( \text{t}' = 0: \text{Nat} \)。
   2. 如果\( \text{t}_1 = \text{succ } \text{nv}_1 \)，则\( \text{t} \rightarrow \text{t}' \)能使用的求值规则就只有E-PREDSUCC了，可得\( \text{t}' = \text{nv}_1 \)，易证\( \text{t}' = \text{nv}_1: \text{Nat} \)（使用类型规则T-ZERO后再使用0次或者多次类型规则T-SUCC）。
   3. 如果\( \text{t}_1 \neq \text{0}, \text{succ } \text{nv}_1 \)，则\( \text{t} \rightarrow \text{t}' \)能使用的求值规则就只有E-PRED了，可得\( \text{t}_1 \rightarrow \text{t}'_1, \text{t}' = \text{pred } \text{t}'_1 \)，由\( \text{t}_1: \text{Nat}, \text{t}_1 \rightarrow \text{t}'_1 \)以及归纳假设，可得\( \text{t}'_1: \text{Nat} \)，进而由类型规则T-PRED，可得\( \text{t}' = \text{pred } \text{t}'_1: \text{Nat} \)。
5. 如果\( \text{t} = \text{iszero } \text{t}_1 \) 则根据引理8.2.2，可得\( \text{t}: \text{Bool}, \text{t}_1: \text{Nat} \)：
   1. 如果\( \text{t}_1 = 0 \)，则\( \text{t} \rightarrow \text{t}' \)能使用的求值规则就只有E-ISZEROZERO了，可得\( \text{t}' = \text{true}: \text{Bool} \)。
   2. 如果\( \text{t}_1 = \text{succ } \text{nv}_1 \)，则\( \text{t} \rightarrow \text{t}' \)能使用的求值规则就只有E-ISZEROSUCC了，可得\( \text{t}' = \text{false}: \text{Bool} \)。
   3. 如果\( \text{t}_1 \neq \text{0}, \text{succ } \text{nv}_1 \)，则\( \text{t} \rightarrow \text{t}' \)能使用的求值规则就只有E-ISZERO了，可得\( \text{t}_1 \rightarrow \text{t}'_1, \text{t}' = \text{iszero } \text{t}'_1 \)，由\( \text{t}_1: \text{Nat}, \text{t}_1 \rightarrow \text{t}'_1 \)以及归纳假设，可得\( \text{t}'_1: \text{Nat} \)，进而由类型规则T-ISZERO，可得\( \text{t}' = \text{iszero } \text{t}'_1: \text{Bool} \)。

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

证毕。

练习8.3.5

题目：

The evaluation rule E-PREDZERO (Figure 3-2) is a bit counterintuitive: we might feel that it makes more sense for the predecessor of zero to be undefined, rather than being defined to be zero. Can we achieve this simply by removing the rule from the definition of single-step evaluation?

解答：

如果只删除求值规则E-PREDZERO，则定理8.3.2（PROGRESS）将不成立，举个例子：\( \text{pred 0} \)为类型良好的项且它明显不是值，但是却无法对它进行求值（为范式）。

故我们不能单纯地删除求值规则E-PREDZERO，还得做出其他改动，比如上面问题出在\( \text{pred 0} \)为类型良好的，我们可以细化类型规则T-PRED，想办法要求\( \text{pred } \text{t}_1 \) 的\( \text{t}_1 \)是个正整数。另外一种处理方法就是保持求值规则E-PREDZERO，但是在运行时检查如果\( \text{pred} \)的参数是\( 0 \)则抛出异常。

练习8.3.6

题目：

Having seen the subject reduction property, it is reasonable to wonder whether the opposite property—subject expansion—also holds. Is it always the case that, if \( \text{t} \rightarrow \text{t}' \) and \( \text{t}': \text{T} \), then \( \text{t}: \text{T} \) If so, prove it. If not, give a counterexample.

解答：

不成立，反例：\( \text{t}' = 1, \text{t} = \text{if true then 1 else true} \)，这里\( \text{t} \rightarrow \text{t}', \text{t}': \text{Nat} \)，但是\( \text{then, else} \)两分支的项的类型不同，类型规则T-IF无法使用，进而\( \text{t} \)非类型良好的（它只能用该规则，该规则又无法使用）。

练习8.3.7

题目：

Suppose our evaluation relation is defined in the big-step style, as in Exercise 3.5.17. How should the intuitive property of type safety be formalized?

解答：

首先看下定理8.3.2（PROGRESS），内容如下：

Suppose \( \text{t} \) is a well-typed term (that is, \( \text{t}: \text{T} \) for some \( \text{T} \)). Then either \( \text{t} \) is a value or else there is some \( \text{t}' \) with \( \text{t} \rightarrow \text{t}' \).

由于big-step风格都是一次性求值到值的，因此上述定理修改成：

Suppose \( \text{t} \) is a well-typed term (that is, \( \text{t}: \text{T} \) for some \( \text{T} \)). Then either \( \text{t} \) is a value or else there is some value \( \text{v} \) with \( \text{t} \Downarrow \text{v} \).

进一步地，由于如果\( \text{t} = \text{v} \)，则\( \text{t} = \text{v} \Downarrow \text{v} \)，于是上述修改定理可以进一步简化成：

Suppose \( \text{t} \) is a well-typed term (that is, \( \text{t}: \text{T} \) for some \( \text{T} \)). Then there is some value \( \text{v} \) with \( \text{t} \Downarrow \text{v} \).

注意到，big-step风格下的PROGRESS定理有非常强的结论：所有类型良好的项都能求值成一个值，即所有类型良好的项的求值过程都是能最终终止的（不会无限循环什么的），目前本章给出的简单语言是满足该要求的，但是如果语言加入递归、循环等机制，就不一定能满足该要求了，此时即使类型良好的项，求值过程仍然可能不终止，对这种语言来说，在big-step风格下无法表达 PROGRESS定理，进而无法区分开错误状态和终止不了的状态，因为这两种状态都无法求值到某个值，而big-step风格只能表达求值到某个值（不修改的话），这是为什么本书倾向于使用small-step风格的原因。当然，为了区分开错误状态和终止不了的状态，你可以对big-step风格进行修改，使其能表达错误状态，比如显式引入一个\( \text{wrong} \)项，在出错的时候求值成\( \text{wrong} \)项。

接着看PRESERVATION定理，有两个版本，，一个要求求值后项的类型和求值前项的类型一样，另外一个更通用的版本则仅要求求值后的项是类型良好的，下面分情况讨论。

先考虑第一个版本，即要求求值后项的类型和求值前项的类型一样，也就是定理8.3.3（PRESERVATION），内容如下：

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

修改成：

If \( \text{t}: \text{T} \) and \( \text{t} \Downarrow \text{v} \), then \( \text{v}: \text{T} \).

最后考虑更通用的版本，即仅要求求值后的项是类型良好的，big-step风格下的表达如下：

If \( \text{t}: \text{T} \) and \( \text{t} \Downarrow \text{v} \), then \( \text{v}: \text{R} \).

练习8.3.8

题目：

Suppose our evaluation relation is augmented with rules for reducing nonsensical terms to an explicit \( \text{wrong} \) state, as in Exercise 3.5.16. Now how should type safety be formalized?

解答：

做出题述改动后，则求值永远不会卡住（stuck），具体的，针对任意除\( \text{wrong} \)外的非值项，它都能进行下一步求值，且它下一步求值要么求值成一个不包含\( \text{wrong} \)的项（此时会跟拓展前的规则求值得到的项一样），要么求值成一个包含\( \text{wrong} \)的项（注：\( \text{wrong} \)本身也算包含\( \text{wrong} \)的项），且该包含\( \text{wrong} \)的项能最终求值成\( \text{wrong} \)，于是PROGRESS定理的后半部分“如果\( \text{t} \)非值，则\( \text{t} \rightarrow \text{t}' \)”变得trivial了（即求值不会卡住这点变得trivial了），但是前半部分仍然重要，前半部分保证了如果类型良好的项是范式，则它必定是值，而不会是\( \text{wrong} \)之类的，再配合PRESERVATION定理，共同保证了类型良好的项永远不会求值成包含\( \text{wrong} \)的项（注：能保证的原因是因为\( \text{wrong} \)非类型良好，进而所有包含\( \text{wrong} \)的项也非类型良好（后者是因为当前语言的类型良好的项的所有子项均是类型良好的））。

综上，不需要修改PRESERVATION定理、PROGRESS定理，但需要额外证明下\( \text{wrong} \)本身以及所有包含\( \text{wrong} \)的项均非类型良好，这样即可保证类型安全性，即类型良好的项永远不会求值成\( \text{wrong} \)本身以及包含\( \text{wrong} \)的项。