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

第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的情况会出问题，假设我们需要证明类型良好的项\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)是终止的，由于\( \text{t}_1, \text{t}_2 \)的大小均比\( \text{t} \)小且均是类型良好的，可以使用归纳假设，根据归纳假设，可得\( \text{t}_1, \text{t}_2 \)均是终止的，加上\( \text{t}_1, \text{t}_2 \)是类型良好的，可得\( \text{t}_1 \rightarrow^* \text{v}_1, \text{t}_2 \rightarrow^* \text{v}_2 \)，这里由引理9.3.4，可得\( \text{v}_1 = \lambda \text{x}: \text{T}_1 \text{. } \text{t}_2 \)，进而可以使用E-APPABS进行求值，有\( \text{t} \rightarrow^* [\text{x} \mapsto \text{v}_2]\text{t}_2 \)，于是我们需要进一步证明\( [\text{x} \mapsto \text{v}_2]\text{t}_2 \)是终止的，但是自由变量\( \text{x} \)可能在函数体\( \text{t}_2 \)中出现多次，进而变量代入后可能产生多份\( \text{v}_2 \)的拷贝，因此\( [\text{x} \mapsto \text{v}_2]\text{t}_2 \)的大小可能会比\( \text{t} \)大，无法使用归纳假设。

练习12.1.7

题目：

Extend the proof technique from this chapter to show that the simply typed lambda-calculus remains normalizing when extended with booleans (Figure 8-1) and products (Figure 11-5).

解答：

证明过程、思路是基本一样的，只不过要多考虑布尔、乘积的情况，这里剔除假想的基础类型\( \text{A} \)，因为我们已经有可用的基础类型了。

先拓展定义12.1.2，增加布尔、乘积的情况（剔除基础类型\( \text{A} \)，下文不再赘述），完整如下：

拓展后的定义12.1.2：

给定类型良好的、closed的项\( \text{t} \)，令\( \text{T} \)为\( \text{t} \)的类型（即\( \vdash \text{t}: \text{T} \)），则：

1. 如果\( \text{T} = \text{Bool} \)，则\( R_{\text{T}}(\text{t}) \)当且仅当\( \text{t} \)是终止的。
2. 如果\( \text{T} = \text{T}_1 \times \text{T}_2 \)，则\( R_{\text{T}}(\text{t}) \)当且仅当\( \text{t} \)是终止的，且\( R_{\text{T}_1}(\text{t}.1), R_{\text{T}_2}(\text{t}.2) \)。
3. 如果\( \text{T} = \text{T}_1 \to \text{T}_2 \)，则\( R_{\text{T}_1 \to \text{T}_2}(\text{t}) \)当且仅当\( \text{t} \)终止，且\( \forall \)closed的项\( \text{s} \)，如果\( \vdash \text{s}: \text{T}_1, R_{\text{T}_1}(\text{s}) \)，则我们有\( R_{\text{T}_2}(\text{t s}) \)。

定义完毕。

引理12.1.3成立同样可以直接从拓展后的定义12.1.2直接看出来。

引理12.1.4的证明需要额外处理布尔、乘积的情况，完整引理内容和证明如下。

引理12.1.4的内容：

给定类型良好的、closed的项\( \text{t} \)，令\( \text{T} \)为\( \text{t} \)的类型，如果\( \text{t} \rightarrow \text{t}' \)，则\( R_{\text{T}}(\text{t}) \)当且仅当\( R_{\text{T}}(\text{t}') \)。

证明引理12.1.4：

对类型\( \text{T} \)的结构进行归纳，归纳假设命题对\( \text{T} \)的直接子类型成立，我们需要证明命题对\( \text{T} \)成立：

明显的，\( \text{t} \)终止当且仅当\( \text{t}' \)终止 (a) ，理由：如果\( \text{t} \)终止，此时假设\( \text{t}' \)不终止，则由\( \text{t} \rightarrow \text{t}' \)，可得\( \text{t} \)也无法终止（注意，这里我们需要用到求值关系的确定性，否则\( \text{t} \)有可能终止），矛盾。如果\( \text{t}' \)终止，则由\( \text{t} \rightarrow \text{t}' \)，可得\( \text{t} \)也终止。

接着，我们回去证明\( R_{\text{T}}(\text{t}) \)当且仅当\( R_{\text{T}}(\text{t}') \)。

必要性：

如果\( R_{\text{T}}(\text{t}) \)，则我们要证明\( R_{\text{T}}(\text{t}') \)：

如果\( \text{T} = \text{Bool} \)，则由\( R_{\text{T}}(\text{t}) \)，可得\( \text{t} \)是终止的，进而由(a)，可得\( \text{t}' \)也是终止的，于是有\( R_{\text{T}}(\text{t}') \)。

如果\( \text{T} = \text{T}_1 \times \text{T}_2 \)，则由\( R_{\text{T}}(\text{t}) \)，可得\( \text{t} \)是终止的且\( R_{\text{T}_1}(\text{t}.1), R_{\text{T}_2}(\text{t}.2) \)，进而由(a)，可得\( \text{t}' \)也是终止的，我们还需要证明\( R_{\text{T}_1}(\text{t}'.1), R_{\text{T}_2}(\text{t}'.2) \)，由\( \text{t} \rightarrow \text{t}' \)以及E-PROJ1，可得\( \text{t}.1 \rightarrow \text{t}'.1 \)，进而由\( R_{\text{T}_1}(\text{t}.1) \)以及归纳假设，可得\( R_{\text{T}_1}(\text{t}'.1) \)，由\( \text{t} \rightarrow \text{t}' \)以及E-PROJ2，可得\( \text{t}.2 \rightarrow \text{t}'.2 \)，进而由\( R_{\text{T}_2}(\text{t}.2) \)以及归纳假设，可得\( R_{\text{T}_2}(\text{t}'.2) \)，综上，有\( R_{\text{T}}(\text{t}') \)。

如果\( \text{T} = \text{T}_1 \to \text{T}_2 \)，则由\( R_{\text{T}}(\text{t}) \)，可得\( \text{t} \)是终止的，进而由(a)，可得\( \text{t}' \)也是终止的，还需要证明\( \forall \)closed的项\( \text{s} \)，如果\( \vdash \text{s}: \text{T}_1, R_{\text{T}_1}(\text{s}) \)，则我们有\( R_{\text{T}_2}(\text{t}' \text{ } \text{s}) \)：由\( R_{\text{T}}(\text{t}) \)，可得\( R_{\text{T}_2}(\text{t} \text{ } \text{s}) \)，而由\( \text{t} \rightarrow \text{t}' \)以及E-APP1，可得\( \text{t s} \rightarrow \text{t}' \text{ } \text{s} \)，进而由\( R_{\text{T}_2}(\text{t} \text{ } \text{s}) \)以及归纳假设，可得\( R_{\text{T}_2}(\text{t}' \text{ } \text{s}) \)，综上，有\( R_{\text{T}}(\text{t}') \)。

充分性：

如果\( R_{\text{T}}(\text{t}') \)，则我们要证明\( R_{\text{T}}(\text{t}) \)：

如果\( \text{T} = \text{Bool} \)，则由\( R_{\text{T}}(\text{t}') \)，可得\( \text{t}' \)是终止的，进而由(a)，可得\( \text{t} \)也是终止的，于是有\( R_{\text{T}}(\text{t}) \)。

如果\( \text{T} = \text{T}_1 \times \text{T}_2 \)，则由\( R_{\text{T}}(\text{t}') \)，可得\( \text{t}' \)是终止的且\( R_{\text{T}_1}(\text{t}'.1), R_{\text{T}_2}(\text{t}'.2) \)，进而由(a)，可得\( \text{t} \)也是终止的，我们还需要证明\( R_{\text{T}_1}(\text{t}.1), R_{\text{T}_2}(\text{t}.2) \)，由\( \text{t} \rightarrow \text{t}' \)以及E-PROJ1，可得\( \text{t}.1 \rightarrow \text{t}'.1 \)，进而由\( R_{\text{T}_1}(\text{t}'.1) \)以及归纳假设，可得\( R_{\text{T}_1}(\text{t}.1) \)，由\( \text{t} \rightarrow \text{t}' \)以及E-PROJ2，可得\( \text{t}.2 \rightarrow \text{t}'.2 \)，进而由\( R_{\text{T}_2}(\text{t}'.2) \)以及归纳假设，可得\( R_{\text{T}_2}(\text{t}.2) \)，综上，有\( R_{\text{T}}(\text{t}) \)。

如果\( \text{T} = \text{T}_1 \to \text{T}_2 \)，则由\( R_{\text{T}}(\text{t}') \)，可得\( \text{t}' \)是终止的，进而由(a)，可得\( \text{t} \)也是终止的，还需要证明\( \forall \)closed的项\( \text{s} \)，如果\( \vdash \text{s}: \text{T}_1, R_{\text{T}_1}(\text{s}) \)，则我们有\( R_{\text{T}_2}(\text{t} \text{ } \text{s}) \)：由\( R_{\text{T}}(\text{t}') \)，可得\( R_{\text{T}_2}(\text{t}' \text{ } \text{s}) \)，而由\( \text{t} \rightarrow \text{t}' \)以及E-APP1，可得\( \text{t s} \rightarrow \text{t}' \text{ } \text{s} \)，进而由\( R_{\text{T}_2}(\text{t}' \text{ } \text{s}) \)以及归纳假设，可得\( R_{\text{T}_2}(\text{t} \text{ } \text{s}) \)，综上，有\( R_{\text{T}}(\text{t}) \)。

总结：

综上，归纳完毕，命题成立。

证明引理12.1.4完毕。

附注：

引理12.1.4的证明中对类型的结构进行归纳之所以可行是因为，在我们目前的简单类型系统中，\( \forall \)类型\( \text{T} \)，均有\( \text{T} \)的结构为树形，进而从类型根节点开始不断取直接子类型可最终到达叶子节点，整个过程是保证可终止的，简而言之，类型的树形结构可作为termination measure，但假设我们允许类型引用自身，比如\( \text{T} = \text{T}_1 \to \text{T} \)，则类型的结构不再是树，而是图了，且该图可能包含环，此时类型的结构就不一定能作为termination measure了，比如从\( \text{T} \)开始，不断取“直接子类型”，可能又会回到\( \text{T} \)，无法终止。

附注完毕。

引理12.1.5的证明同样需要额外处理布尔、乘积的情况，完整引理内容和证明如下。

引理12.1.5的内容：

给定类型良好的、closed的\( n \)个值\( \text{v}_1, \text{v}_2, \dots, \text{v}_n \)，其中，\( \text{T}_1, \text{T}_2, \dots, \text{T}_n \)分别为\( \text{v}_1, \text{v}_2, \dots, \text{v}_n \)的类型且\( \forall 1 \leq i \leq n \)，有\( R_{\text{T}_i}(\text{v}_i) \)，给定项\( \text{t} \)，如果\( \text{x}_1: \text{T}_1, \text{x}_2: \text{T}_2, \dots, \text{x}_n: \text{T}_n \vdash \text{t}: \text{T} \)，则\( R_{\text{T}}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}) \)。

证明引理12.1.5：

归纳假设命题对\( \text{t} \)的直接子项均成立，我们要证明命题对\( \text{t} \)成立，下面对\( \text{x}_1: \text{T}_1, \text{x}_2: \text{T}_2, \dots, \text{x}_n: \text{T}_n \vdash \text{t}: \text{T} \)使用的规则进行分情况讨论：

1. 如果使用的规则是T-VAR，则\( \exists 1 \leq i \leq n, \text{t} = \text{x}_\text{i}, \text{T} = \text{T}_i \)，此时有\( [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t} = \text{v}_i \)，加上\( R_{\text{T}_i}(\text{v}_i) \)，可得 \( R_{\text{T}}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}) \)。
2. 如果使用的规则是T-ABS，则\( \text{t} = \lambda \text{x}: \text{S}_1 \text{. } \text{s}_2, \text{x}_1: \text{T}_1, \text{x}_2: \text{T}_2, \dots, \text{x}_n: \text{T}_n, x: \text{S}_1 \vdash \text{t}: \text{S}_2, \text{T} = \text{S}_1 \to \text{S}_2 \)，于是有\( [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t} = \lambda \text{x}: \text{S}_1 \text{. } [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{s}_2 \)，这里明显\( [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t} \)可以求值成一个值，因为它本身已经是个值了，进而可得它是终止的，不过由于它的类型是\( \text{T} = \text{S}_1 \to \text{S}_2 \)，故为了证明\( R_{\text{T}}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}) \)，我们还得证明\( \forall \)closed的项\( \text{s} \)，如果\( \vdash \text{s}: \text{S}_1, R_{\text{S}_1}(\text{s}) \)，则我们有\( R_{\text{S}_2}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t} \text{ } \text{s}) \)：由\( R_{\text{S}_1}(\text{s}) \)，可得\( \text{s} \)是终止的，加上\( \text{s} \)是类型良好的，可得\( \exists \text{v}, \text{s} \rightarrow^* \text{v} \)，反复使用引理12.1.4，可得\( R_{\text{S}_1}(\text{v}) \)，此时根据归纳假设，可得\( R_{\text{S}_2}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n][\text{x} \mapsto \text{v}]\text{s}_2) \)，而\( [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t} \text{ } \text{s} = (\lambda \text{x}: \text{S}_1 \text{. } [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{s}_2) \text{ } \text{s} \rightarrow^* [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n][\text{x} \mapsto \text{v}]\text{s}_2 \)，根据引理12.1.4（反方向），可得\( R_{\text{S}_2}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t} \text{ } \text{s}) \)，综上，有\( R_{\text{T}}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}) \)。
3. 如果使用的规则是T-APP，则\( \text{t} = \text{t}_1 \text{ } \text{t}_2, \text{x}_1: \text{T}_1, \text{x}_2: \text{T}_2, \dots, \text{x}_n: \text{T}_n \vdash \text{t}_1: \text{T}_{11} \to \text{T}_{12}, \text{x}_1: \text{T}_1, \text{x}_2: \text{T}_2, \dots, \text{x}_n: \text{T}_n \vdash \text{t}_1: \text{T}_{11}, \text{T} = \text{T}_{12} \)，根据归纳假设，可得\( R_{\text{T}_{11} \to \text{T}_{12}}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_1), R_{\text{T}_{11}}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_2) \)，此时根据\( R_{\text{T}_{11} \to \text{T}_{12}}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_1) \)的定义，可得\( R_{\text{T}_{12}}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_1 \text{ } [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_2) \)，即\( R_{\text{T}}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}) \)。
4. 如果使用的规则是T-TRUE，则\( \text{t} = \text{true}, \text{T} = \text{Bool} \)，此时有\( [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t} = \text{true} \)，可得\( [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t} \)是终止的，进而可得\( R_{\text{T}}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}) \)。
5. 如果使用的规则是T-FALSE，则\( \text{t} = \text{false}, \text{T} = \text{Bool} \)，此时有\( [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t} = \text{false} \)，可得\( [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t} \)是终止的，进而可得\( R_{\text{T}}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}) \)。
6. 如果使用的规则是T-IF，则\( \text{t} = \text{if } \text{t}_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3, \text{x}_1: \text{T}_1, \text{x}_2: \text{T}_2, \dots, \text{x}_n: \text{T}_n \vdash \text{t}_1: \text{Bool}, \text{x}_1: \text{T}_1, \text{x}_2: \text{T}_2, \dots, \text{x}_n: \text{T}_n \vdash \text{t}_2: \text{T}, \text{x}_1: \text{T}_1, \text{x}_2: \text{T}_2, \dots, \text{x}_n: \text{T}_n \vdash \text{t}_3: \text{T} \)，根据归纳假设，可得\( R_{\text{Bool}}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_1), R_{\text{T}}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_2), R_{\text{T}}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_3) \)，由\( R_{\text{Bool}}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_1) \)，可得\( [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_1 \)是终止的，加上它是类型良好的，可得\( \exists \text{v}_{11}, [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_1 \rightarrow^* \text{v}_{11} \)，根据CANONICAL FORMS引理，可得\( \text{v}_{11} = \text{true} \)或\( \text{v}_{11} = \text{false} \)：
   1. 如果\( \text{v}_{11} = \text{true} \)，则 \( [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t} = \text{if } [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_1 \text{ then } [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_2 \text{ else } [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_3 \rightarrow^* \text{if } \text{v}_{11} \text{ then } [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_2 \text{ else } [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_3 \rightarrow [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_2 \)，根据\( R_{\text{T}}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_2) \)以及引理12.1.4（反方向），可得\( R_{\text{T}}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}) \)。
   2. 如果\( \text{v}_{11} = \text{false} \)，则 \( [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t} = \text{if } [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_1 \text{ then } [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_2 \text{ else } [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_3 \rightarrow^* \text{if } \text{v}_{11} \text{ then } [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_2 \text{ else } [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_3 \rightarrow [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_3 \)，根据\( R_{\text{T}}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_3) \)以及引理12.1.4（反方向），可得\( R_{\text{T}}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}) \)。
7. 如果使用的规则是T-PAIR，则\( \text{t} = \{ \text{t}_1, \text{t}_2 \}, \text{x}_1: \text{T}_1, \text{x}_2: \text{T}_2, \dots, \text{x}_n: \text{T}_n \vdash \text{t}_1: \text{S}_1, \text{x}_1: \text{T}_1, \text{x}_2: \text{T}_2, \dots, \text{x}_n: \text{T}_n \vdash \text{t}_2: \text{S}_2, \text{T} = \text{S}_1 \times \text{S}_2 \)，根据归纳假设，可得\( R_{\text{S}_1}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_1), R_{\text{S}_2}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_2) \)，由\( R_{\text{S}_1}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_1) \)，可得\( [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_1 \)是终止的，加上它是类型良好的，可得\( \exists \text{v}_{11}, [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_1 \rightarrow^* \text{v}_{11} \)，同理可得\( [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_2 \)是终止的且\( \exists \text{v}_{12}, [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_2 \rightarrow^* \text{v}_{12} \)，于是可得\( [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t} = \{ [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_1, [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_2 \} \rightarrow^* \{ \text{v}_{11}, [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_2 \} \rightarrow^* \{ \text{v}_{11}, \text{v}_{12} \} \)，这意味着\( [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t} \)是终止的，我们还得证明\( R_{\text{S}_1}(([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}).1), R_{\text{S}_2}(([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}).2) \)：由\( R_{\text{S}_1}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_1), [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_1 \rightarrow^* \text{v}_{11} \)以及引理12.1.4，可得\( R_{\text{S}_1}(\text{v}_{11}) \)，而\( [\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t} \rightarrow^* \{ \text{v}_{11}, \text{v}_{12} \} \)，可得\( ([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}).1 \rightarrow^* \text{v}_{11} \)，根据\( R_{\text{S}_1}(\text{v}_{11}) \)以及引理12.1.4（反方向），可得\( R_{\text{S}_1}(([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}).1) \)，同理可得，\( R_{\text{S}_2}(([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}).2) \)，综上，有\( R_{\text{T}}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}) \)。
8. 如果使用的规则是T-PROJ1，则\( \text{t} = \text{t}_1.1, \text{x}_1: \text{T}_1, \text{x}_2: \text{T}_2, \dots, \text{x}_n: \text{T}_n \vdash \text{t}_1: \text{S}_1 \times \text{S}_2, \text{T} = \text{S}_1 \)，根据归纳假设，可得\( R_{\text{S}_1 \times \text{S}_2}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_1) \)，根据\( R_{\text{S}_1 \times \text{S}_2}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_1) \)的定义，可得\( R_{\text{S}_1}(([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_1).1) \)，即\( R_{\text{T}}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}) \)。
9. 如果使用的规则是T-PROJ2，则\( \text{t} = \text{t}_1.2, \text{x}_1: \text{T}_1, \text{x}_2: \text{T}_2, \dots, \text{x}_n: \text{T}_n \vdash \text{t}_1: \text{S}_1 \times \text{S}_2, \text{T} = \text{S}_2 \)，根据归纳假设，可得\( R_{\text{S}_1 \times \text{S}_2}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_1) \)，根据\( R_{\text{S}_1 \times \text{S}_2}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_1) \)的定义，可得\( R_{\text{S}_2}(([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}_1).2) \)，即\( R_{\text{T}}([\text{x}_1 \mapsto \text{v}_1][\text{x}_2 \mapsto \text{v}_2] \dots [\text{x}_n \mapsto \text{v}_n]\text{t}) \)。

综上，归纳完毕，命题成立。

证明引理12.1.5完毕。

最后，我们可以证明定理12.1.6了，完整引理内容和证明如下。

定理12.1.6的内容：

如果\( \vdash \text{t}: \text{T} \)，则\( \text{t} \)是终止的。

证明定理12.1.6：

根据引理12.1.5（注：使用\( n = 0 \)，即不进行变量代入的情况），可得\( R_{\text{T}}(\text{t}) \)，进而根据引理12.1.3（注：该引理是trivial的，可以直接隐式使用该引理，就像前面一样），进而可得\( \text{t} \)是终止的。

证明定理12.1.6完毕。