OSFVA
所有文章 标签
OSFVA

目录

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

CloseToZero
   约 18046 字   预计阅读 37 分钟 

第3章

章节3.2

练习3.2.4

题目：

How many elements does \( S_3 \) have?

解答：

根据\( S_{i + 1} \)的定义，\( |S_{i + 1}| = 3 + 3|S_i| + |S_i|^3 \)，于是从\( |S_0| = 0 \)开始慢慢算，可得\( |S_3| = 59439 \)。

练习3.2.5

题目：

Show that the sets \( S_i \) are cumulative—that is, that for each \( i \) we have \( S_i \subseteq S_{i + 1} \).

证明：

使用数学归纳法证明，当\( i = 0 \)时，根据定义，明显有\( S_0 \subseteq S_1 \)，归纳假设当\( i = k \)时成立，当\( i = k + 1 \)时：

\[ \begin{aligned} S_i = S_{k + 1} &= \{ \text{true }, \text{ false }, 0 \} \\ &\cup \{ \text{succ } \text{t}_1, \text{ pred } \text{t}_1, \text{ iszero } \text{t}_1 \mid \text{t}_1 \in S_k \} \\ &\cup \{ \text{if } \text{t}_1 \text{ then } \text{t}_3 \text{ else } \text{t}_3 \mid \text{t}_1, \text{t}_2, \text{t}_3 \in S_k \} \end{aligned} \]

\[ \begin{aligned} S_{i + 1} = S_{k + 2} &= \{ \text{true }, \text{ false }, 0 \} \\ &\cup \{ \text{succ } \text{t}_1, \text{ pred } \text{t}_1, \text{ iszero } \text{t}_1 \mid \text{t}_1 \in S_{k + 1} \} \\ &\cup \{ \text{if } \text{t}_1 \text{ then } \text{t}_3 \text{ else } \text{t}_3 \mid \text{t}_1, \text{t}_2, \text{t}_3 \in S_{k + 1} \} \end{aligned} \]

于是\( \forall \text{t} \in S_i \)，有\( \text{t} \in \{ \text{true }, \text{ false }, 0 \} \) 或\( \text{t} \in \{ \text{succ } \text{t}_1, \text{ pred } \text{t}_1, \text{ iszero } \text{t}_1 \mid \text{t}_1 \in S_k \} \) 或\( \text{t} \in \{ \text{if } \text{t}_1 \text{ then } \text{t}_3 \text{ else } \text{t}_3 \mid \text{t}_1, \text{t}_2, \text{t}_3 \in S_k \} \)，分情况讨论：

  1. 如果\( \text{t} \in \{ \text{true }, \text{ false }, 0 \} \)，则也有\( \text{t} \in S_{i + 1} \)。
  2. 如果\( \text{t} \in \{ \text{succ } \text{t}_1, \text{ pred } \text{t}_1, \text{ iszero } \text{t}_1 \mid \text{t}_1 \in S_k \} \)，则\( \exists \text{t}_1 \in S_k, \text{t} = \text{ succ } \text{t}_1 \)或 \( \text{t} = \text{ pred } \text{t}_1 \)或 \( \text{t} = \text{ iszero } \text{t}_1 \)，根据归纳假设可得，\( S_k \subseteq S_{k + 1} \)，因此\( \text{t}_1 \in S_{k + 1} \)，进而根据\( S_{i + 1} \)的定义，可得\( \text{t} \in S_{i + 1} \)。
  3. 如果\( \text{t} \in \{ \text{if } \text{t}_1 \text{ then } \text{t}_3 \text{ else } \text{t}_3 \mid \text{t}_1, \text{t}_2, \text{t}_3 \in S_k \} \)，则\( \exists \text{t}_1, \text{t}_2, \text{t}_3 \in S_k, \text{t} = \text{ if } \text{t}_1 \text{ then } \text{t}_3 \text{ else } \text{t}_3 \)，根据归纳假设可得，\( S_k \subseteq S_{k + 1} \)，因此\( \text{t}_1, \text{t}_2, \text{t}_3 \in S_{k + 1} \)，进而根据\( S_{i + 1} \)的定义，可得\( \text{t} \in S_{i + 1} \)。

综上，有\( S_i \subseteq S_{i + 1} \)，归纳完毕。

证毕。

章节3.3

练习3.3.4

题目：

Theorem [Principles of induction on terms]: Suppose \( P \) is a predicate on terms.

Induction on depth: If, for each term \( \text{s} \), given \( P(\text{r}) \) for all \( \text{r} \) such that \( \mathit{depth}(\text{r}) < \mathit{depth}(s) \) we can show \( P(\text{s}) \), then \( P(\text{s}) \) holds for all \( \text{s} \).

Induction on size: If, for each term \( \text{s} \), given \( P(\text{r}) \) for all \( \text{r} \) such that \( \mathit{size}(\text{r}) < \mathit{size}(\text{s}) \) we can show \( P(\text{s}) \), then \( P(\text{s}) \) holds for all \( \text{s} \).

Structural induction: If, for each term \( \text{s} \), given \( P(\text{r}) \) for all immediate subterms \( \text{r} \) of \( \text{s} \) we can show \( P(\text{s}) \), then \( P(\text{s}) \) holds for all \( \text{s} \).

证明：

证明深度归纳法：

令\( Q(n) = \)“\( \forall \)项\( \text{s} \)满足\( \mathit{depth}(\text{s}) = n \)，有\( P(\text{s}) \)”，将\( Q(n) \)代入完全数学归纳法/强数学归纳法（2.4.2）中，可得深度归纳法是成立的。

证明大小归纳法：

令\( Q(n) = \)“\( \forall \)项\( \text{s} \)满足\( \mathit{size}(\text{s}) = n \)，有\( P(\text{s}) \)”，将\( Q(n) \)代入完全数学归纳法/强数学归纳法（2.4.2）中，可得大小归纳法是成立的。

证明结构归纳法：

注： 注意到一个项\( \text{s} \)的所有直接子项以及间接子项\( \text{r} \)的深度均\( < \text{s} \)，而结构归纳法要求仅在假设\( P \)对直接子项成立的情况下（不包含间接子项）就要推出\( P \)对\( \text{s} \)成立，可以看出一般结构归纳法的归纳假设中能用的信息量比深度归纳法的归纳假设中能用的信息量更少（当然，你可以在结构归纳法中取结论更强的判别式来增加能用的信息量），特别的，这意味着，如果结构归纳法走得通，也就是如果真的仅在假设\( P \)对直接子项成立的情况下就可以推出\( P \)对\( \text{s} \)成立，那么此时换成深度归纳法也必走得通，进一步的，我们可以用深度归纳法来证明结构归纳法（同理，用大小归纳法也可以）。

下面开始证明：

给定一个关于项判别式\( P \)，如果\( \forall \)项\( \text{s} \)，能做到在假设“\( P \)针对\( \text{s} \)的所有直接子项\( \text{r} \)均有\( P(\text{r}) \)”的情况下，能证明\( P(\text{s}) \)（注：即结构归纳法能走得通） (a) ，那么我们改成假设“\( \forall \)项\( \text{r} \)满足\( \mathit{depth}(\text{r}) < \mathit{depth}(\text{s}) \)，均有\( P(\text{r}) \)” (b) ，根据深度归纳法，此时如果我们能证明\( P(\text{s}) \)，则\( P \)对任意项均成立，由于针对\( \text{s} \)的所有直接子项\( \text{r} \)，均有\( \mathit{depth}(\text{r}) < \mathit{depth}(\text{s}) \)，因此根据(b)处的假设，有\( P(\text{r}) \)，进而根据(a)，即结构归纳法能走得通这点，可得\( P(\text{s}) \)，至此，深度归纳法归纳完毕，可得\( P \)对任意项均成立。

证毕。

章节3.5

练习3.5.5

题目：

Spell out the induction principle used in the preceding proof, in the style of Theorem 3.3.4.

解答：

给定\( P \)为关于求值语句推导的判别式， \( \forall \)推导\( \mathcal{D} \)，归纳假设\( P \)对\( \mathcal{D} \)的所有直接子推导\( \mathcal{D_s} \)都成立，在此归纳假设下，如果我们能证明\( P(\mathcal{D}) \)，则\( P \)对所有推导都成立。

或者定义推导中使用的规则的每个前提条件以及结论都是一个节点（注：一个结论可能同时也是下一个使用规则的前提条件，这时只算一个节点），则我们也可以对推导树的大小，即节点数量进行归纳，这是一个更强的归纳假设，此时能用的信息更多。

练习3.5.10

题目：

Rephrase Definition 3.5.9 as a set of inference rules.

解答：

\[ \dfrac{\text{t} \rightarrow \text{t}'}{\text{t} \rightarrow^* \text{t}'} \]

\[ \text{t} \rightarrow^* \text{t} \]

\[ \dfrac{\text{t} \rightarrow^* \text{t}' \quad \text{t}' \rightarrow^* \text{t}''}{\text{t} \rightarrow^* \text{t}''} \]

练习3.5.13

题目：

  1. Suppose we add a new rule \[ \text{if } \text{true } \text{then } \text{t}_2 \text{ else } \text{t}_3 \rightarrow \text{t}_3 \qquad \text{(E-FUNNY1)} \] to the ones in Figure 3-1. Which of the above theorems (3.5.4, 3.5.7, 3.5.8, 3.5.11, and 3.5.12) remain valid?
  2. Suppose instead that we add this rule: \[ \dfrac{\text{t}_2 \rightarrow \text{t}'_2}{\text{if } \text{t}_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3 \rightarrow \text{ if } \text{t}_1 \text{ then } \text{t}'_2 \text{ else } \text{t}_3} \qquad \text{(E-FUNNY2)} \] Now which of the above theorems remain valid? Do any of the proofs need to change?

解答1：

定理3.5.4不成立，因为使用规则E-IFTRUE，可得\( \text{if true then true else false } \rightarrow \text{ true} \)，而使用规则E-FUNNY1，可得\( \text{if true then true else false } \rightarrow \text{ false} \)，这里\( \text{true } \neq \text{ false} \)。

定理3.5.7仍然成立，证明不需要修改，因为增加新规则后，还是没有规则能求值值\( \text{true, false} \)。

定理3.5.8仍然成立，证明不需要修改。

定理3.5.11不成立，上面定理3.5.4给出的反例就可以证明这点。

定理3.5.12仍然成立，证明不需要修改。

解答2：

定理3.5.4不成立，因为使用规则E-IFTRUE，可得\( \text{if true then if true then false else true else false } \rightarrow \text{ if true then false else true} \)，而使用规则E-FUNNY2加上\( \text{if true then false else true } \rightarrow \text{ false} \)，可得\( \text{if true then if true then false else true else false } \rightarrow \text{ if true then false else false} \)，这里\( \text{if true then false else true} \neq \text{ if true then false else false} \)。

定理3.5.7仍然成立，证明不需要修改，因为增加新规则后，还是没有规则能求值值\( \text{true, false} \)。

定理3.5.8仍然成立，证明不需要修改。

定理3.5.11仍然成立，证明需要修改，比较长，放在后面。

定理3.5.12仍然成立，证明不需要修改。

现在我们证明定理3.5.11仍然成立：

首先，我们证明一个引理。

引理1：

如果\( \text{s} \rightarrow \text{t}, \text{s} \rightarrow \text{t}', \text{t} \neq \text{t}' \)，则\( \exists \text{u}, \text{t} \rightarrow^* \text{u}, \text{t}' \rightarrow^* \text{u} \) （注意，这里前面是单步求值，后面是多步求值）。

证明引理1：

使用结构归纳法证明，归纳假设引理对所有\( \text{s} \)的直接子项成立，我们要证明引理对\( \text{s} \)成立：

如果\( \text{s} \rightarrow \text{t}, \text{s} \rightarrow \text{t}', \text{t} \neq \text{t}' \)，则此时\( \text{s} \)具有形式\( \text{if } \text{s}_1 \text{ then } \text{s}_2 \text{ else } \text{s}_3 \)，分情况讨论：

  1. 如果\( \text{s} \rightarrow \text{t} \)使用的规则是E-IFTRUE，则此时\( \text{s} = \text{if } \text{true } \text{then } \text{s}_2 \text{ else } \text{s}_3, \text{s}_1 = \text{ true}, \text{t} = \text{s}_2 \)，而\( \text{s} \rightarrow \text{t}' \)且\( \text{t} \neq \text{t}' \)，唯一的可能就是\( \text{s} \rightarrow \text{t}' \) 使用了规则E-FUNNY2，可得\( \text{s}_2 \rightarrow \text{s}'_2, \text{t}' = \text{if } \text{true } \text{then } \text{s}'_2 \text{ else } \text{s}_3 \)，令\( \text{u} = \text{s}'_2 \)，则使用规则E-IFTRUE，可得\( \text{t}' \rightarrow \text{u} \)，加上\( \text{t} = \text{s}_2 \rightarrow \text{s}'_2 = \text{u} \)，基本上就得到我们想要的了，再考虑到多步求值关系包含单步求值关系，因此有\( \text{t} \rightarrow^* \text{u}, \text{t}' \rightarrow^* \text{u} \)。
  2. 如果\( \text{s} \rightarrow \text{t} \)使用的规则是E-IFFALSE，则此时\( \text{s} = \text{if } \text{false } \text{then } \text{s}_2 \text{ else } \text{s}_3, \text{s}_1 = \text{ false}, \text{t} = \text{s}_3 \)，而\( \text{s} \rightarrow \text{t}' \)且\( \text{t} \neq \text{t}' \)，唯一的可能就是\( \text{s} \rightarrow \text{t}' \) 使用了规则E-FUNNY2，可得\( \text{s}_2 \rightarrow \text{s}'_2, \text{t}' = \text{if } \text{false } \text{then } \text{s}'_2 \text{ else } \text{s}_3 \)，令\( \text{u} = \text{s}_3 \)，则使用规则E-IFFALSE，可得\( \text{t}' \rightarrow \text{u} \)，进而有\( \text{t}' \rightarrow^* \text{u} \)，加上\( \text{t} = \text{s}_3 \rightarrow^* \text{s}_3 = \text{u} \)，就得到所有我们想要的了。
  3. 如果\( \text{s} \rightarrow \text{t}, \text{s} \rightarrow \text{t}' \)使用的规则均是E-IF，此时可得\( \text{t} = \text{if } \text{s}'_1 \text{ then } \text{s}_2 \text{ else } \text{s}_3, \text{s}_1 \rightarrow \text{s}'_1 \) 以及\( \text{t}' = \text{if } \text{s}''_1 \text{ then } \text{s}_2 \text{ else } \text{s}_3, \text{s}_1 \rightarrow \text{s}''_1 \)，由于\( \text{t} \neq \text{t}' \)，因此\( \text{s}'_1 \neq \text{s}''_1 \)，再加上\( \text{s}_1 \)是\( \text{s} \)的直接子项且\( \text{s}_1 \rightarrow \text{s}'_1, \text{s}_1 \rightarrow \text{s}''_1 \)，可以使用归纳假设，根据归纳假设， \( \exists \text{u}', \text{s}'_1 \rightarrow^* \text{u}', \text{s}''_1 \rightarrow^* \text{u}' \)，令\( \text{u} = \text{ if } \text{u}' \text{ then } \text{s}_2 \text{ else } \text{s}_3 \)，由于\( \text{s}'_1 \rightarrow^* \text{u}' \)当且仅当\( \exists n \in \mathbf{N} \) 以及\( n + 1 \)个项\( \text{w}_0, \text{w}_1, \dots, \text{w}_n \) 满足\( \text{w}_0 = \text{s}'_1, \text{w}_n = \text{u}', \forall 0 \leq i < n, \text{w}_i \rightarrow \text{w}_{i + 1} \)，即多步求值实际上就是连续单步求值0次或者多次，因此我们可以对连续单步求值次数\( n \)进行数学归纳，易得连续使用规则E-IF，有\( \text{t} \rightarrow^* \text{u} \)，同理易得\( \text{t}' \rightarrow^* \text{u}' \)。
  4. 如果\( \text{s} \rightarrow \text{t}, \text{s} \rightarrow \text{t}' \)使用的规则均是E-FUNNY2，此时可得\( \text{t} = \text{if } \text{s}_1 \text{ then } \text{s}'_2 \text{ else } \text{s}_3, \text{s}_2 \rightarrow \text{s}'_2 \) 以及\( \text{t}' = \text{if } \text{s}_1 \text{ then } \text{s}''_2 \text{ else } \text{s}_3, \text{s}_2 \rightarrow \text{s}''_2 \)，由于\( \text{t} \neq \text{t}' \)，因此\( \text{s}'_2 \neq \text{s}''_2 \)，再加上\( \text{s}_2 \)是\( \text{s} \)的直接子项且\( \text{s}_2 \rightarrow \text{s}'_2, \text{s}_2 \rightarrow \text{s}''_2 \)，可以使用归纳假设，根据归纳假设， \( \exists \text{u}', \text{s}'_2 \rightarrow^* \text{u}', \text{s}''_2 \rightarrow^* \text{u}' \)，令\( \text{u} = \text{ if } \text{s}_1 \text{ then } \text{u}' \text{ else } \text{s}_3 \)，同情况3，对连续单步求值的次数进行数学归纳，易得连续使用规则E-FUNNY2，有\( \text{t} \rightarrow^* \text{u} \)，同理易得\( \text{t}' \rightarrow^* \text{u}' \)。
  5. 如果\( \text{s} \rightarrow \text{t}, \text{s} \rightarrow \text{t}' \)使用的规则分别是E-IF和E-FUNNY2，不妨设\( \text{s} \rightarrow \text{t} \)使用规则E-IF，\( \text{s} \rightarrow \text{t}' \)使用规则E-FUNNY2，此时可得\( \text{t} = \text{if } \text{s}'_1 \text{ then } \text{s}_2 \text{ else } \text{s}_3, \text{s}_1 \rightarrow \text{s}'_1 \) 以及\( \text{t}' = \text{if } \text{s}_1 \text{ then } \text{s}'_2 \text{ else } \text{s}_3, \text{s}_2 \rightarrow \text{s}'_2 \)，令\( \text{u} = \text{if } \text{s}'_1 \text{ then } \text{s}'_2 \text{ else } \text{s}_3 \)，则使用规则E-FUNNY2，可得\( \text{t} \rightarrow \text{u} \)，进而有\( \text{t} \rightarrow^* \text{u} \)，同理使用规则E-IF，易得\( \text{t}' \rightarrow^* \text{u} \)。

至此，归纳完毕，引理对所有项均成立。

证毕。

接下来，我们打算拓展上面的引理到多步求值的情况，为此我们需要一个额外的引理。

引理2：

如果\( \text{s} \rightarrow \text{t} \)，则\( \mathit{size}(\text{t}) < \mathit{size}(\text{s}) \)。

证明引理2：

使用结构归纳法证明，归纳假设引理对所有\( \text{s} \)的直接子项成立，我们要证明引理对\( \text{s} \)成立：

由于\( \text{s} \)不为范式，因此也不为值\( \text{true, false} \)，可得\( \text{s} \)具有形式\( \text{if } \text{s}_1 \text{ then } \text{s}_2 \text{ else } \text{s}_3 \)，我们对\( \text{s} \rightarrow \text{t} \)使用的规则进行分类讨论：

  1. 如果使用的规则是E-IFTRUE，则\( \text{s}_1 = \text{true} \)，可得\( \text{t} = \text{s}_2 \)，根据\( \mathit{size} \)的定义，可得\( \mathit{size}(\text{t}) = \mathit{size}(\text{s}_2) < \mathit{size}(\text{s}) \)。
  2. 如果使用的规则是E-IFFALSE，则\( \text{s}_1 = \text{false} \)，可得\( \text{t} = \text{s}_3 \)，根据\( \mathit{size} \)的定义，可得\( \mathit{size}(\text{t}) = \mathit{size}(\text{s}_3) < \mathit{size}(\text{s}) \)。
  3. 如果使用的规则是E-IF，则\( \text{t} = \text{if } \text{s}'_1 \text{ then } \text{s}_2 \text{ else } \text{s}_3, \text{s}_1 \rightarrow \text{s}'_1 \)，这里\( \text{s}_1 \)为\( \text{s} \)的直接子项，可以使用归纳假设，根据归纳假设以及\( \text{s}_1 \rightarrow \text{s}'_1 \)，可得\( \mathit{size}(\text{s}'_1) < \text{s}_1 \)，进而根据\( \mathit{size} \)的定义，可得\( \mathit{size}(\text{t}) < \mathit{size}(\text{s}) \)。
  4. 如果使用的规则是E-FUNNY2，则\( \text{t} = \text{if } \text{s}_1 \text{ then } \text{s}'_2 \text{ else } \text{s}_3, \text{s}_2 \rightarrow \text{s}'_2 \)，这里\( \text{s}_2 \)为\( \text{s} \)的直接子项，可以使用归纳假设，根据归纳假设以及\( \text{s}_2 \rightarrow \text{s}'_2 \)，可得\( \mathit{size}(\text{s}'_2) < \text{s}_2 \)，进而根据\( \mathit{size} \)的定义，可得\( \mathit{size}(\text{t}) < \mathit{size}(\text{s}) \)。

归纳完毕，引理对所有项均成立。

证毕。

现在，我们可以引理1到多步求值的情况了。

引理3：

如果\( \text{s} \rightarrow^* \text{t}, \text{s} \rightarrow^* \text{t}' \)，则\( \exists \text{u}, \text{t} \rightarrow^* \text{u}, \text{t}' \rightarrow^* \text{u} \) （注意，这里我们不要求\( \text{t} \neq \text{t}' \)）。

证明引理3：

使用大小归纳法证明，归纳假设引理对所有\( \mathit{size}(\text{r}) < \mathit{size}(\text{s}) \)的项\( \text{r} \)成立，我们要证明引理对\( \text{s} \)成立：

如果\( \text{t} = \text{t}' \)，则令\( \text{u} = \text{t} = \text{t}' \)，直接有\( \text{t} \rightarrow^* \text{u}, \text{t}' \rightarrow^* \text{u} \)，接下来考虑\( \text{t} \neq \text{t}' \)的情况即可。

如果\( \text{t} = \text{s} \)或\( \text{t}' = \text{s} \)，不妨设\( \text{t} = \text{s} \)，则令\( \text{u} = \text{t}' \)，可得\( \text{t} = \text{s} \rightarrow^* \text{t}' = \text{u} \)以及\( \text{t}' \rightarrow^* \text{t}' = \text{u} \)，因此接下来可以进一步排除\( \text{t} = \text{s} \)或\( \text{t}' = \text{s} \)的情况，直接默认\( \text{t} \neq \text{s} \)且\( \text{t}' \neq \text{s} \)。

由于\( \text{t} \neq \text{s}, \text{t}' \neq \text{s} \)，因此如果把两个多步求值\( \text{s} \rightarrow^* \text{t}, \text{s} \rightarrow^* \text{t}' \)分解成多次单步求值，则单步求值次数至少为1，设两者的第1次单步求值分别为\( \text{s} \rightarrow \text{w}, \text{s} \rightarrow \text{w}' \)，分情况讨论：

  1. 如果\( \text{w} = \text{w}' \)，则\( \text{w} \rightarrow^* \text{t}, \text{w} \rightarrow^* \text{t}' \)，根据引理2以及\( \text{s} \rightarrow \text{w} \)，可得\( \mathit{size}(\text{w}) = \mathit{size}(\text{w}') < \mathit{size}(\text{s}) \)，因此可以用归纳假设，根据归纳假设，\( \exists \text{u}, \text{t} \rightarrow^* \text{u}, \text{t}' \rightarrow^* \text{u} \)。
  2. 如果\( \text{w} \neq \text{w}' \)，则根据引理1， \( \exists \text{u}', \text{w} \rightarrow^* \text{u}', \text{w}' \rightarrow^* \text{u}' \)，根据引理2以及\( \text{s} \rightarrow \text{w}, \text{s} \rightarrow \text{w}' \)，可得\( \mathit{size}(\text{w}) < \mathit{size}(\text{s}), \mathit{size}(\text{w}') < \mathit{size}(\text{s}) \)，因此\( \text{w}, \text{w}' \)均可以用归纳假设，根据归纳假设以及\( \text{w} \rightarrow^* \text{u}', \text{w} \rightarrow^* \text{t} \)，可得\( \exists \text{u}'', \text{u}' \rightarrow^* \text{u}'', \text{t} \rightarrow^* \text{u}'' \)，同理可得\( \exists \text{u}''', \text{u}' \rightarrow^* \text{u}''', \text{t}' \rightarrow^* \text{u}''' \)，由于\( \mathit{size}(\text{u}') \leq \mathit{size}(\text{w}) < \mathit{size}(\text{s})\)，因此可以用归纳假设，根据归纳假设以及\( \text{u}' \rightarrow^* \text{u}'', \text{u}' \rightarrow^* \text{u}''' \)，可得\( \exists \text{u}, \text{u}'' \rightarrow^* \text{u}, \text{u}''' \rightarrow^* \text{u} \)，加上\( \text{t} \rightarrow^* \text{u}'', \text{t}' \rightarrow^* \text{u}''' \)，可得\( \text{t} \rightarrow^* \text{u}, \text{t}' \rightarrow^* \text{u} \)。

归纳完毕，引理对所有项均成立。

证毕。

最后，我们回去证明定理3.5.11仍然成立。

证明定理3.5.11：

如果\( \text{t} \rightarrow^* \text{u}, \text{t} \rightarrow^* \text{u}' \)且\( \text{u}, \text{u}' \)均为范式，则根据引理3，可得\( \exists \text{u}'', \text{u} \rightarrow^* \text{u}'', \text{u}' \rightarrow^* \text{u}'' \)，由于\( \text{u}, \text{u}' \)均为范式，因此唯一的可能就是\( \text{u} = \text{u}' = \text{u}'' \)。

证毕。

练习3.5.14

题目：

Show that Theorem 3.5.4 is also valid for the evaluation relation on arithmetic expressions: if \( \text{t} \rightarrow \text{t}' \) and \( \text{t} \rightarrow \text{t}'' \), then \( \text{t}' = \text{t}'' \).

证明：

使用结构归纳法，易证明如果一个项具有形式\( \text{succ } \text{nv}_1 \)，则它是范式。

下面使用结构归纳法来证明，归纳假设命题对所有\( \text{t} \)的直接子项成立，我们要证明命题对\( \text{t} \)成立：

由于\( \text{t} \)可以进行单步求值，因此\( \text{t} \)不是范式，下面我们对\( \text{t} \)的形式分情况进行讨论：

  1. 如果\( \text{t} = \text{ if } \text{t}_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3 \)：
    1. 如果\( \text{t}_1 = \text{ true} \)，则能使用的规则只有E-IFTRUE，可得\( \text{t}' = \text{t}'' = \text{t}_2 \)。
    2. 如果\( \text{t}_1 = \text{ false} \)，则能使用的规则只有E-IFFALSE，可得\( \text{t}' = \text{t}'' = \text{t}_3 \)。
    3. 如果\( \text{t}_1 \neq \text{ true, false} \)，则能使用的规则只有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, \text{t}'' = \text{ if } \text{t}''_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3 \)，这里\( \text{t}_1 \)为\( \text{t} \)的直接子项，因此可以用归纳假设，根据归纳假设以及\( \text{t}_1 \rightarrow \text{t}'_1, \text{t}_1 \rightarrow \text{t}''_1 \)，可得\( \text{t}'_1 = \text{t}''_1 \)，进一步可得\( \text{t}' = \text{t}'' \)。
  2. 如果\( \text{t} = \text{ succ } \text{t}_1 \)，则能使用的规则只有E-SUCC，可得\( \text{t}_1 \rightarrow \text{t}'_1, \text{t}' = \text{ succ } \text{t}'_1 \) 以及\( \text{t}_1 \rightarrow \text{t}''_1, \text{t}'' = \text{ succ } \text{t}''_1 \)，这里\( \text{t}_1 \)为\( \text{t} \)的直接子项，因此可以用归纳假设，根据归纳假设以及\( \text{t}_1 \rightarrow \text{t}'_1, \text{t}_1 \rightarrow \text{t}''_1 \)，可得\( \text{t}'_1 = \text{t}''_1 \)，进一步可得\( \text{t}' = \text{t}'' \)。
  3. 如果\( \text{t} = \text{ pred } \text{t}_1 \)：
    1. 如果\( \text{t}_1 = 0 \)，则能使用的规则只有E-PREDZERO，可得\( \text{t}' = \text{t}'' = 0 \)。
    2. 如果\( \text{t}_1 = \text{succ } \text{nv}_1 \)，则能使用的规则只有E-PREDSUCC（前面说了，\( \text{succ } \text{nv}_1 \)是范式），可得\( \text{t}' = \text{t}'' = \text{nv}_1 \)。
    3. 如果\( \text{t}_1 \neq 0, \text{ succ } \text{nv}_1 \)，则能使用的规则只有E-PRED，可得\( \text{t}_1 \rightarrow \text{t}'_1, \text{t}' = \text{ pred } \text{t}'_1 \) 以及\( \text{t}_1 \rightarrow \text{t}''_1, \text{t}'' = \text{ pred } \text{t}''_1 \)，这里\( \text{t}_1 \)为\( \text{t} \)的直接子项，因此可以用归纳假设，根据归纳假设以及\( \text{t}_1 \rightarrow \text{t}'_1, \text{t}_1 \rightarrow \text{t}''_1 \)，可得\( \text{t}'_1 = \text{t}''_1 \)，进一步可得\( \text{t}' = \text{t}'' \)。
  4. 如果\( \text{t} = \text{ iszero } \text{t}_1 \)：
    1. 如果\( \text{t}_1 = 0 \)，则能使用的规则只有E-ISZEROZERO，可得\( \text{t}' = \text{t}'' = \text{ true} \)。
    2. 如果\( \text{t}_1 = \text{succ } \text{nv}_1 \)，则能使用的规则只有E-ISZEROSUCC，可得\( \text{t}' = \text{t}'' = \text{ false} \)。
    3. 如果\( \text{t}_1 \neq 0, \text{ succ } \text{nv}_1 \)，则能使用的规则只有E-ISZERO，可得\( \text{t}_1 \rightarrow \text{t}'_1, \text{t}' = \text{ iszero } \text{t}'_1 \) 以及\( \text{t}_1 \rightarrow \text{t}''_1, \text{t}'' = \text{ iszero } \text{t}''_1 \)，这里\( \text{t}_1 \)为\( \text{t} \)的直接子项，因此可以用归纳假设，根据归纳假设以及\( \text{t}_1 \rightarrow \text{t}'_1, \text{t}_1 \rightarrow \text{t}''_1 \)，可得\( \text{t}'_1 = \text{t}''_1 \)，进一步可得\( \text{t}' = \text{t}'' \)。

归纳完毕，命题对所有项均成立。

证毕。

练习3.5.16

题目：

A different way of formalizing meaningless states of the abstract machine is to introduce a new term called \( \text{wrong} \) and augment the operational semantics with rules that explicitly generate \( \text{wrong} \) in all the situations where the present semantics gets stuck. To do this in detail, we introduce two new syntactic categories

\[ \begin{aligned} \text{badnat} &::= &\qquad \textit{non-numeric normal forms:} \\ &\text{wrong} &\qquad \textit{run-time error} \\ &\text{true} &\qquad \textit{constant true} \\ &\text{false} &\qquad \textit{constant false} \\ \text{badbool} &::= &\qquad \textit{non-boolean normal forms:} \\ &\text{wrong} &\qquad \textit{run-time error} \\ &\text{nv} &\qquad \textit{numeric value} \end{aligned} \]

and we augment the evaluation relation with the following rules:

\[ \begin{aligned} \text{if badbool then } \text{t}_1 \text{ else } \text{t}_2 \rightarrow \text{ wrong} &\qquad \text{(E-IF-WRONG)} \\ \text{succ badnat} \rightarrow \text{ wrong} &\qquad \text{(E-SUCC-WRONG)} \\ \text{pred badnat} \rightarrow \text{ wrong} &\qquad \text{(E-PRED-WRONG)} \\ \text{iszero badnat} \rightarrow \text{ wrong} &\qquad \text{(E-ISZERO-WRONG)} \end{aligned} \]

Show that these two treatments of run-time errors agree by (1) finding a precise way of stating the intuition that “the two treatments agree,” and (2) proving it. As is often the case when proving things about programming languages, the tricky part here is formulating a precise statement to be proved — the proof itself should be straightforward.

解答：

符号约定：

我们使用符号\( \text{g} \)以及类似的符号变种如\( \text{g}', \text{g}'', \text{g}_1, \text{g}'_1 \)等等来代表原始语法中的项，即不包含\( \text{wrong} \)的项（也就是好的项，\( \text{g} \)表示good），使用\( \text{t} \)以及类似的符号变种来代表拓展语法中的项，避免我们要在多个地方强调某个项不包含\( \text{wrong} \)。

如何准确地表达两种处理运行时错误的方法是一致的：

我们用\( \xrightarrow{o} \)表示原始的求值关系，使用\( \xrightarrow{e} \)来表示上述拓展\( \text{wrong} \)后的求值关系，则两种求值关系一致的准确表述为： \( \text{g} \xrightarrow{o}^* \text{u} \)且\( \text{u} \)为停滞（stuck）项当且仅当\( \text{g} \xrightarrow{e}^* \text{wrong} \) (a) ，与此同时，\( \forall \text{v} \)为值，\( \text{g} \xrightarrow{o}^* \text{v} \)当且仅当\( \text{g} \xrightarrow{e}^* \text{v} \) (b) 。简而言之：我发生运行时错误，你也得发生运行时错误，反之亦然。我没发生运行时错误，你也不能发生运行时错误，且我们最终求得的值得相同，反之亦然（注意：(b)的逆命题中，拓展求值关系也是从一个不包含运行时错误的项\( \text{g} \)开始求值，而不是任意项\( \text{t} \)）。

为了证明(a)，我们先证明一个引理，即拓展后的求值关系仍然具有确定性。

引理1：

如果\( \text{t} \xrightarrow{e} \text{t}', \text{t} \xrightarrow{e} \text{t}'' \)，则\( \text{t}' = \text{t}'' \)。

证明引理1：

类似练习3.5.14的证明，复制过来修改下即可。

使用结构归纳法来证明，归纳假设引理对所有\( \text{t} \)的直接子项成立，我们要证明引理对\( \text{t} \)成立：

由于\( \text{t} \)在拓展后的求值关系下可以进行单步求值，因此\( \text{t} \)在拓展后的求值关系下不是范式，下面我们对\( \text{t} \)的形式分情况进行讨论：

  1. 如果\( \text{t} = \text{ if } \text{t}_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3 \)：
    1. 如果\( \text{t}_1 = \text{ true} \)，则能使用的规则只有E-IFTRUE，可得\( \text{t}' = \text{t}'' = \text{t}_2 \)。
    2. 如果\( \text{t}_1 = \text{ false} \)，则能使用的规则只有E-IFFALSE，可得\( \text{t}' = \text{t}'' = \text{t}_3 \)。
    3. 如果\( \text{t}_1 = \text{ wrong}, \text{nv}_1 \)，则能使用的规则只有E-IF-WRONG，可得\( \text{t}' = \text{t}'' = \text{ wrong} \)。
    4. 如果\( \text{t}_1 \neq \text{ true, false, wrong}, \text{nv}_1 \)，则能使用的规则只有E-IF，可得\( \text{t}_1 \xrightarrow{e} \text{t}'_1, \text{t}' = \text{ if } \text{t}'_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3 \) 以及\( \text{t}_1 \xrightarrow{e} \text{t}''_1, \text{t}'' = \text{ if } \text{t}''_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3 \)，这里\( \text{t}_1 \)为\( \text{t} \)的直接子项，因此可以用归纳假设，根据归纳假设以及\( \text{t}_1 \xrightarrow{e} \text{t}'_1, \text{t}_1 \xrightarrow{e} \text{t}''_1 \)，可得\( \text{t}'_1 = \text{t}''_1 \)，进一步可得\( \text{t}' = \text{t}'' \)。
  2. 如果\( \text{t} = \text{ succ } \text{t}_1 \)：
    1. 如果\( \text{t}_1 = \text{ wrong, true, false} \)，则能使用的规则只有E-SUCC-WRONG，可得\( \text{t}' = \text{t}'' = \text{ wrong} \)。
    2. 如果\( \text{t}_1 \neq \text{ wrong, true, false} \)，则能使用的规则只有E-SUCC，可得\( \text{t}_1 \xrightarrow{e} \text{t}'_1, \text{t}' = \text{ succ } \text{t}'_1 \) 以及\( \text{t}_1 \xrightarrow{e} \text{t}''_1, \text{t}'' = \text{ succ } \text{t}''_1 \)，这里\( \text{t}_1 \)为\( \text{t} \)的直接子项，因此可以用归纳假设，根据归纳假设以及\( \text{t}_1 \xrightarrow{e} \text{t}'_1, \text{t}_1 \xrightarrow{e} \text{t}''_1 \)，可得\( \text{t}'_1 = \text{t}''_1 \)，进一步可得\( \text{t}' = \text{t}'' \)。
  3. 如果\( \text{t} = \text{ pred } \text{t}_1 \)：
    1. 如果\( \text{t}_1 = 0 \)，则能使用的规则只有E-PREDZERO，可得\( \text{t}' = \text{t}'' = 0 \)。
    2. 如果\( \text{t}_1 = \text{succ } \text{nv}_1 \)，则能使用的规则只有E-PREDSUCC，可得\( \text{t}' = \text{t}'' = \text{nv}_1 \)。
    3. 如果\( \text{t}_1 = \text{ wrong, true, false} \)，则能使用的规则只有E-PRED-WRONG，可得\( \text{t}' = \text{t}'' = \text{ wrong} \)。
    4. 如果\( \text{t}_1 \neq 0, \text{ succ } \text{nv}_1, \text{ wrong, true, false} \)，则能使用的规则只有E-PRED，可得\( \text{t}_1 \xrightarrow{e} \text{t}'_1, \text{t}' = \text{ pred } \text{t}'_1 \) 以及\( \text{t}_1 \xrightarrow{e} \text{t}''_1, \text{t}'' = \text{ pred } \text{t}''_1 \)，这里\( \text{t}_1 \)为\( \text{t} \)的直接子项，因此可以用归纳假设，根据归纳假设以及\( \text{t}_1 \xrightarrow{e} \text{t}'_1, \text{t}_1 \xrightarrow{e} \text{t}''_1 \)，可得\( \text{t}'_1 = \text{t}''_1 \)，进一步可得\( \text{t}' = \text{t}'' \)。
  4. 如果\( \text{t} = \text{ iszero } \text{t}_1 \)：
    1. 如果\( \text{t}_1 = 0 \)，则能使用的规则只有E-ISZEROZERO，可得\( \text{t}' = \text{t}'' = \text{ true} \)。
    2. 如果\( \text{t}_1 = \text{succ } \text{nv}_1 \)，则能使用的规则只有E-ISZEROSUCC，可得\( \text{t}' = \text{t}'' = \text{ false} \)。
    3. 如果\( \text{t}_1 = \text{ wrong, true, false} \)，则能使用的规则只有E-ISZERO-WRONG，可得\( \text{t}' = \text{t}'' = \text{ wrong} \)。
    4. 如果\( \text{t}_1 \neq 0, \text{ succ } \text{nv}_1, \text{ wrong, true, false} \)，则能使用的规则只有E-ISZERO，可得\( \text{t}_1 \xrightarrow{e} \text{t}'_1, \text{t}' = \text{ iszero } \text{t}'_1 \) 以及\( \text{t}_1 \xrightarrow{e} \text{t}''_1, \text{t}'' = \text{ iszero } \text{t}''_1 \)，这里\( \text{t}_1 \)为\( \text{t} \)的直接子项，因此可以用归纳假设，根据归纳假设以及\( \text{t}_1 \xrightarrow{e} \text{t}'_1, \text{t}_1 \xrightarrow{e} \text{t}''_1 \)，可得\( \text{t}'_1 = \text{t}''_1 \)，进一步可得\( \text{t}' = \text{t}'' \)。

归纳完毕，引理对所有项均成立。

证毕。

如何证明(a)的必要性，即“\( \text{g} \xrightarrow{o}^* \text{u} \)且\( \text{u} \)为停滞（stuck）项 \( \Rightarrow \text{g} \xrightarrow{e}^* \text{wrong} \)”？考虑到\( \text{g} \)在原始求值关系中最终会求值得到停滞项\( \text{u} \)，加上拓展求值关系仍具有确定性且包含原始求值关系的所有求值规则，故拓展求值关系一开始每步求值得到的项，均会和原始求值关系中每步求值得到的项相同，因此终有一步也会得到停滞项\( \text{u} \)，只不过原始求值关系停在\( \text{u} \)了，而拓展求值关系可以进一步求值，既然如此，如果我们能证明原始语法中的所有停滞项（不包含\( \text{wrong} \)的停滞项），在拓展求值关系中均能多步求值为\( \text{wrong} \)，则我们便能证明(a)的必要性，故我们证明如下的引理2。

引理2：

如果\( \text{g} \)为停滞项，则\( \text{g} \xrightarrow{e}^* \text{wrong} \)。

证明引理2：

使用结构归纳法来证明，归纳假设引理对所有\( \text{t} \)的直接子项成立，我们要证明引理对\( \text{t} \)成立：

由于\( \text{g} \)为停滞项，因此\( \text{g} \)不可能为值，下面分情况讨论：

  1. 如果\( \text{g} = \text{if } \text{g}_1 \text{ else } \text{g}_2 \text{ then } \text{g}_3 \)，由于\( \text{g} \)为停滞项，因此\( \text{g}_1 \)必须为范式，否则E-IF规则就能使用，从而与\( \text{g} \)为停滞项矛盾，除此之外，\( \text{g}_1 \)也不能为\( \text{true, false} \)，否则，E-IFTRUE,E-IFFALSE就能使用，接下来继续分情况讨论：
    1. 如果\( \text{g}_1 = \text{wrong} \)，则使用规则E-IF-WRONG，可得\( \text{g} \xrightarrow{e}^* \text{wrong} \)。
    2. 如果\( \text{g}_1 = \text{if } \text{g}_{11} \text{ else } \text{g}_{12} \text{ then } \text{g}_{13} \)，此时\( \text{g}_1 \)明显不是值，加上它是范式，可得它是停滞项，又\( \text{g}_1 \)是\( \text{g} \)的直接子项，可以使用归纳假设，根据归纳假设，\( \text{g}_1 \xrightarrow{e}^* \text{wrong} \)，对\( \text{g}_1 \)求值得到\( \text{wrong} \)的步数进行归纳以及使用规则E-IF，易得\( \text{g} \xrightarrow{e}^* \text{ if } \text{wrong} \text{ else } \text{g}_2 \text{ then } \text{g}_3 \)，进而使用规则E-IF-WRONG，可得\( \text{g} \xrightarrow{e}^* \text{wrong} \)。
    3. 如果\( \text{g}_1 = \text{succ } \text{g}_{11} \)，对\( \text{g}_{11} \)分情况进行讨论：
      1. 如果\( \text{g}_{11} = \text{nv}_{11} \)，即它是数值，则\( \text{g}_1 \)也是数值，属于\( \text{badbool} \)的范畴，因此\( \text{g} \)可以使用E-IF-WRONG，有\( \text{g} \xrightarrow{e}^* \text{wrong} \)。
      2. 如果\( \text{g}_{11} \)不是数值，则\( \text{g}_1 \)为停滞项，根据归纳假设，\( \text{g}_1 \xrightarrow{e}^* \text{wrong} \)，易得\( \text{g} \xrightarrow{e}^* \text{ if } \text{wrong} \text{ else } \text{g}_2 \text{ then } \text{g}_3 \xrightarrow{e}^* \text{wrong} \)。
    4. 如果\( \text{g}_1 = \text{pred } \text{g}_{11}, \text{ iszero } \text{g}_{11} \)，此时\( \text{g}_1 \)明显不是值，加上它是范式，可得它是停滞项，根据归纳假设，\( \text{g}_1 \xrightarrow{e}^* \text{wrong} \)，易得\( \text{g} \xrightarrow{e}^* \text{ if } \text{wrong} \text{ else } \text{g}_2 \text{ then } \text{g}_3 \xrightarrow{e}^* \text{wrong} \)。
  2. 如果\( \text{g} = \text{succ } \text{g}_1 \)，由于\( \text{g} \)为停滞项，因此\( \text{g}_1 \)必须为范式，否则E-SUCC规则就能使用，从而与\( \text{g} \)为停滞项矛盾，除此之外，\( \text{g}_1 \)也不能是数值，否则\( \text{g} \)就会是数值，也和\( \text{g} \)为停滞项矛盾，接下来继续分情况讨论：
    1. 如果\( \text{g}_1 = \text{wrong, true, false} \)，则使用规则E-SUCC-WRONG，可得\( \text{g} \xrightarrow{e}^* \text{wrong} \)。
    2. 如果\( \text{g}_1 = \text{if } \text{g}_{11} \text{ else } \text{g}_{12} \text{ then } \text{g}_{13}, \text{ pred } \text{g}_{11}, \text{ iszero } \text{g}_{11} \)，此时\( \text{g}_1 \)明显不是值，加上它是范式，可得它是停滞项，根据归纳假设，\( \text{g}_1 \xrightarrow{e}^* \text{wrong} \)，易得\( \text{g} \xrightarrow{e}^* \text{ succ } \text{wrong} \xrightarrow{e}^* \text{wrong} \)。
    3. 如果\( \text{g}_1 = \text{succ } \text{g}_{11} \)，由于\( \text{g}_1 \)不能是数值，可得\( \text{g}_1 \)不是值，加上它是范式，可得它是停滞项，根据归纳假设，\( \text{g}_1 \xrightarrow{e}^* \text{wrong} \)，易得\( \text{g} \xrightarrow{e}^* \text{ succ } \text{wrong} \xrightarrow{e}^* \text{wrong} \)。
  3. 如果\( \text{g} = \text{pred } \text{g}_1 \)，由于\( \text{g} \)为停滞项，因此\( \text{g}_1 \)必须为范式，否则E-PRED规则就能使用，除此之外，\( \text{g}_1 \)也不能是数值，否则E-PREDZERO或E-PREDSUCC就可以使用，接下来继续分情况讨论：
    1. 如果\( \text{g}_1 = \text{wrong, true, false} \)，则使用规则E-PRED-WRONG，可得\( \text{g} \xrightarrow{e}^* \text{wrong} \)。
    2. 如果\( \text{g}_1 = \text{if } \text{g}_{11} \text{ else } \text{g}_{12} \text{ then } \text{g}_{13}, \text{ pred } \text{g}_{11}, \text{ iszero } \text{g}_{11} \)，此时\( \text{g}_1 \)明显不是值，加上它是范式，可得它是停滞项，根据归纳假设，\( \text{g}_1 \xrightarrow{e}^* \text{wrong} \)，易得\( \text{g} \xrightarrow{e}^* \text{ pred } \text{wrong} \xrightarrow{e}^* \text{wrong} \)。
    3. 如果\( \text{g}_1 = \text{succ } \text{g}_{11} \)，由于\( \text{g}_1 \)不能是数值，可得\( \text{g}_1 \)不是值，加上它是范式，可得它是停滞项，根据归纳假设，\( \text{g}_1 \xrightarrow{e}^* \text{wrong} \)，易得\( \text{g} \xrightarrow{e}^* \text{ pred } \text{wrong} \xrightarrow{e}^* \text{wrong} \)。
  4. 如果\( \text{g} = \text{iszero } \text{g}_1 \)，由于\( \text{g} \)为停滞项，因此\( \text{g}_1 \)必须为范式，否则E-ISZERO规则就能使用，除此之外，\( \text{g}_1 \)也不能是数值，否则E-ISZEROZERO或E-ISZEROSUCC就可以使用，接下来继续分情况讨论：
    1. 如果\( \text{g}_1 = \text{wrong, true, false} \)，则使用规则E-ISZERO-WRONG，可得\( \text{g} \xrightarrow{e}^* \text{wrong} \)。
    2. 如果\( \text{g}_1 = \text{if } \text{g}_{11} \text{ else } \text{g}_{12} \text{ then } \text{g}_{13}, \text{ pred } \text{g}_{11}, \text{ iszero } \text{g}_{11} \)，此时\( \text{g}_1 \)明显不是值，加上它是范式，可得它是停滞项，根据归纳假设，\( \text{g}_1 \xrightarrow{e}^* \text{wrong} \)，易得\( \text{g} \xrightarrow{e}^* \text{ iszero } \text{wrong} \xrightarrow{e}^* \text{wrong} \)。
    3. 如果\( \text{g}_1 = \text{succ } \text{g}_{11} \)，由于\( \text{g}_1 \)不能是数值，可得\( \text{g}_1 \)不是值，加上它是范式，可得它是停滞项，根据归纳假设，\( \text{g}_1 \xrightarrow{e}^* \text{wrong} \)，易得\( \text{g} \xrightarrow{e}^* \text{ iszero } \text{wrong} \xrightarrow{e}^* \text{wrong} \)。

归纳完毕，引理对所有项均成立。

证毕。

现在可以证明(a)的必要性了。

证明(a)的必要性：

如果\( \text{g} \xrightarrow{o}^* \text{u} \)且\( \text{u} \)为停滞（stuck）项，则由引理1以及拓展求值关系包含原始求值关系的所有求值规则，可得\( \text{g} \xrightarrow{e}^* \text{u} \)，再由引理2，可得\( \text{u} \xrightarrow{e}^* \text{wrong} \)，连起来，可得\( \text{g} \xrightarrow{e}^* \text{wrong} \)。

证毕。

如何证明(a)的充分性，即“\( \text{g} \xrightarrow{e}^* \text{wrong} \Rightarrow \text{g} \xrightarrow{o}^* \text{u} \)且\( \text{u} \)为停滞（stuck）项”？前面说了，由于拓展求值关系仍具有确定性且包含原始求值关系的所有求值规则，因此拓展求值关系一开始每步求值得到的项，均会和原始求值关系中每步求值得到的项相同，直到得到一个停滞项\( \text{u} \)，两者才开始分歧，原始求值关系会停在\( \text{u} \)，而拓展求值关系则会进一步求值，直到得到最终的\( \text{wrong} \)，故我们可以证明如果一个项\( \text{g} \)在拓展求值关系中即将发生错误了，即该项原本没错（也就是不包含\( \text{wrong} \)，这也是为什么选用\( \text{g} \) 代表该项的原因），但继续单步求值一次就发生错误了（也就是包含\( \text{wrong} \)了），那么\( \text{g} \)在原始求值关系中为停滞项，严格表述就是如下引理3。

引理3：

如果\( \text{g} \xrightarrow{e} \text{t} \)且\( \text{t} \)中包含\( \text{wrong} \)，则\( \text{g} \)在原始求值关系中为停滞项。

证明引理3：

使用结构归纳法来证明，归纳假设引理对所有\( \text{g} \)的直接子项成立，我们要证明引理对\( \text{g} \)成立：

根据\( \text{g} \)的符号，我们知道它不包含\( \text{wrong} \)，加上\( \text{g} \)在拓展求值关系中可以单步求值，因此\( \text{g} \)在拓展求值关系中不为范式，特别的，它不为值，其余的我们分情况讨论：

  1. \( \text{g} = \text{ if } \text{g}_1 \text{ else } \text{g}_2 \text{ then } \text{g}_3 \)，单步求值得到的\( \text{t} \)包含\( \text{wrong} \)，能引入\( \text{wrong} \)的规则只有 E-IF、E-IF-WRONG，分情况讨论\( \text{g} \xrightarrow{e} \text{t} \)使用的规则：
    1. 如果使用的规则是E-IF，则\( \text{g}_1 \xrightarrow{e} \text{t}_{11} \) 且\( \text{t}_{11} \)包含\( \text{wrong} \)（注：这样\( \text{t} \)才能包含\( \text{wrong} \)），这里\( \text{g}_1 \)为\( \text{g} \)的直接子项，可以使用归纳假设，根据归纳假设， \( \text{g}_1 \)在原始求值关系中为停滞项，进而可得在原求值关系中，\( \text{g} \)的单步求值不能用规则E-IF，而在原求值关系中，E-IFTRUE、E-IFFALSE规则也必不可用，否则会违反拓展求值关系的确定性（引理1），可得\( \text{g} \)在原始求值关系中为停滞项。
    2. 如果使用的规则是E-IF-WRONG，则\( \text{g}_1 = \text{badbool} \)，此时\( \text{g} \)在原始求值关系明显没有可用的规则，为范式，也明显不是值，可得\( \text{g} \)在原始求值关系中为停滞项。
  2. 如果\( \text{g} = \text{ succ } \text{g}_1 \)，能引入\( \text{wrong} \)的规则只有E-SUCC、E-SUCC-WRONG，分情况讨论\( \text{g} \xrightarrow{e} \text{t} \)使用的规则：
    1. 如果使用的规则是E-SUCC，则\( \text{g}_1 \xrightarrow{e} \text{t}_{11} \) 且\( \text{t}_{11} \)包含\( \text{wrong} \)，这里\( \text{g}_1 \)为\( \text{g} \)的直接子项，根据归纳假设，\( \text{g}_1 \)在原始求值关系中为停滞项，进而可得在原求值关系中，\( \text{g} \)的单步求值不能用规则E-SUCC，没有其他可用的规则了，可得\( \text{g} \)在原始求值关系中为停滞项。
    2. 如果使用的规则是E-SUCC-WRONG，则\( \text{g}_1 = \text{badnat} \)，此时\( \text{g} \)在原始求值关系明显没有可用的规则，为范式，也明显不是值，可得\( \text{g} \)在原始求值关系中为停滞项。
  3. 如果\( \text{g} = \text{ pred } \text{g}_1 \)，能引入\( \text{wrong} \)的规则只有E-PRED、E-PRED-WRONG，分情况讨论\( \text{g} \xrightarrow{e} \text{t} \)使用的规则：
    1. 如果使用的规则是E-PRED，则\( \text{g}_1 \xrightarrow{e} \text{t}_{11} \) 且\( \text{t}_{11} \)包含\( \text{wrong} \)，这里\( \text{g}_1 \)为\( \text{g} \)的直接子项，根据归纳假设，\( \text{g}_1 \)在原始求值关系中为停滞项，进而可得在原求值关系中，\( \text{g} \)的单步求值不能用规则E-PRED，由于在拓展求值关系中数值均是范式，而\( \text{g}_1 \)在拓展求值关系中不是范式，因此\( \text{g}_1 \)不为数值，进而在原始求值关系中E-PREDZERO、E-PREDSUCC规则均不可用，没有其他可用的规则了，可得\( \text{g} \)在原始求值关系中为停滞项。
    2. 如果使用的规则是E-PRED-WRONG，则\( \text{g}_1 = \text{badnat} \)，此时\( \text{g} \)在原始求值关系明显没有可用的规则，为范式，也明显不是值，可得\( \text{g} \)在原始求值关系中为停滞项。
  4. 如果\( \text{g} = \text{ iszero } \text{g}_1 \)，能引入\( \text{wrong} \)的规则只有E-ISZERO、E-ISZERO-WRONG，分情况讨论\( \text{g} \xrightarrow{e} \text{t} \)使用的规则：
    1. 如果使用的规则是E-ISZERO，则\( \text{g}_1 \xrightarrow{e} \text{t}_{11} \) 且\( \text{t}_{11} \)包含\( \text{wrong} \)，这里\( \text{g}_1 \)为\( \text{g} \)的直接子项，根据归纳假设，\( \text{g}_1 \)在原始求值关系中为停滞项，进而可得在原求值关系中，\( \text{g} \)的单步求值不能用规则E-ISZERO，由于在拓展求值关系中数值均是范式，而\( \text{g}_1 \)在拓展求值关系中不是范式，因此\( \text{g}_1 \)不为数值，进而在原始求值关系中E-ISZEROZERO、E-ISZEROSUCC规则均不可用，没有其他可用的规则了，可得\( \text{g} \)在原始求值关系中为停滞项。
    2. 如果使用的规则是E-ISZERO-WRONG，则\( \text{g}_1 = \text{badnat} \)，此时\( \text{g} \)在原始求值关系明显没有可用的规则，为范式，也明显不是值，可得\( \text{g} \)在原始求值关系中为停滞项。

归纳完毕，引理对所有项均成立。

证毕。

现在可以证明(a)的充分性了。

证明(a)的充分性：

如果\( \text{g} \xrightarrow{e}^* \text{wrong} \)，可得\( \exists n > 0 \in \mathbf{N} \) 以及\( n + 1 \)个项\( \text{t}_0, \text{t}_1, \dots, \text{t}_n \) 满足\( \text{t}_0 = \text{g}, \text{t}_n = \text{wrong}, \forall 0 \leq i < n, \text{t}_i \xrightarrow{e} \text{t}_{i + 1} \)（注意，这里\( n \)必须\( > 0 \)，因为\( \text{g} \)不包含\( \text{wrong} \)），且\( \exists k < n \in \mathbf{N} \)满足\( \forall 0 \leq i \leq k, \text{t}_i \)不包含\( \text{wrong} \)，而\( \text{t}_{k + 1} \)包含\( \text{wrong} \)，也就是前\( k + 1 \)项均为不包含运行时错误的项，第\( k + 2 \)项（注：这里算\( t_0 \)为第1项，以此类推，\( \text{t}_{k + 1} \)为第k + 2项）为第一个出现运行时错误的项，由于\( \text{t}_k \xrightarrow{e} \text{t}_{k + 1} \)， \( \text{t}_k \)不包含\( \text{wrong} \)，\( \text{t}_{k + 1} \)包含\( \text{wrong} \)，根据引理3，可得\( \text{t}_{k} \)在原始求值关系中为停滞项，由于拓展求值关系仍具有确定性且包含原始求值关系的所有求值规则，加上前\( k + 1 \)项均不包含\( \text{wrong} \)，可得\( \forall 0 \leq i < k, \text{t}_i \xrightarrow{o} \text{t}_{i + 1} \)，进而有\( \text{g} \xrightarrow{o}^* \text{t}_k \)且\( \text{t}_{k} \)为停滞项。

证毕。

至此，我们证明完(a)了，我们接着证明(b)。

证明(b)：

必要性：

\( \forall \text{v} \)为值，如果\( \text{g} \xrightarrow{o}^* \text{v} \)，由于拓展求值关系仍具有确定性且包含原始求值关系的所有求值规则，可得\( \text{g} \xrightarrow{e}^* \text{v} \)。

充分性：

\( \forall \text{v} \)为值，如果\( \text{g} \xrightarrow{e}^* \text{v} \)，我们使用结构归纳法来证明，归纳假设命题对所有\( \text{g} \)的直接子项成立，我们要证明命题对\( \text{g} \)成立：

下面对\( \text{g} \)的形式进行分类讨论：

  1. 如果\( \text{g} \)为值，则由于所有值在拓展求值关系中均为范式，因此唯一的可能就是\( \text{g} = \text{v} \)，此时直接有\( \text{g} = \text{v} \xrightarrow{o}^* \text{v} \)。
  2. 如果\( \text{g} = \text{if } \text{g}_1 \text{ else } \text{g}_2 \text{ then } \text{g}_3 \)，此时\( \text{g} \)不是值，得进一步求值，不然得不到值\( \text{v} \)，而为了得到值，\( \text{g} \)必须摆脱当前的\( \text{if} \)项形式，只有规则IF-TRUE和IF-FALSE有可能摆脱当前的\( \text{if} \)项形式，这里如果\( \text{g}_1 \)为\( \text{true} \)或者\( \text{false} \)，则直接可以用规则IF-TRUE或IF-FALSE，否则我们就必须连续使用规则E-IF，直到\( \text{if} \)的条件项变成\( \text{true} \)或者\( \text{false} \)，总结就是必须\( \text{g}_1 \xrightarrow{e}^* \text{true} \)或\( \text{g}_1 \xrightarrow{e}^* \text{false} \)，进而\( \text{g} \xrightarrow{e}^* \text{if } \text{true} \text{ else } \text{g}_2 \text{ then } \text{g}_3 \xrightarrow{e} \text{g}_2 \xrightarrow{e}^* \text{v} \) 或\( \text{g} \xrightarrow{e}^* \text{if } \text{false} \text{ else } \text{g}_2 \text{ then } \text{g}_3 \xrightarrow{e} \text{g}_3 \xrightarrow{e}^* \text{v} \)，我们仅讨论\( \text{g}_1 \xrightarrow{e}^* \text{true}, \text{g} \xrightarrow{e}^* \text{if } \text{true} \text{ else } \text{g}_2 \text{ then } \text{g}_3 \xrightarrow{e} \text{g}_2 \xrightarrow{e}^* \text{v} \)的情况，另外一种情况类似，这里\( \text{g}_1 \)为\( \text{g} \)的直接子项，可以使用归纳假设，根据\( \text{g}_1 \xrightarrow{e}^* \text{true} \)以及归纳假设，可得\( \text{g}_1 \xrightarrow{o}^* \text{true} \)， \( \text{g}_2 \)也为\( \text{g} \)的直接子项，可以使用归纳假设，根据\( \text{g}_2 \xrightarrow{e}^* \text{v} \)以及归纳假设，可得\( \text{g}_2 \xrightarrow{o}^* \text{v} \)，由\( \text{g}_1 \xrightarrow{o}^* \text{true}, \text{g}_2 \xrightarrow{o}^* \text{v} \)，易得\( \text{g} \xrightarrow{o}^* \text{if } \text{true} \text{ else } \text{g}_2 \text{ then } \text{g}_3 \xrightarrow{o} \text{g}_2 \xrightarrow{o}^* \text{v} \)，进而可得\( \text{g} \xrightarrow{o}^* \text{v} \)。
  3. 如果\( \text{g} = \text{succ } \text{g}_1 \)且\( \text{g} \)不为值，此时\( \text{g}_1 \)不为数值（否则\( \text{g} \)就会是数值，进而为值，矛盾），这种形式的\( \text{g} \)能使用的规则就E-SUCC以及E-SUCC-WRONG，后者不能使用，否则多步求值不到值\( \text{v} \)，使用规则E-SUCC后，得到的仍是\( \text{succ} \)形式的项，此时如果不是值，就得进一步使用E-SUCC形式求值，简而言之，必须连续使用规则E-SUCC，直到得到一个值，这意味着\( \text{g}_1 \xrightarrow{e}^* \text{nv}_1, \text{g} \xrightarrow{e}^* \text{succ } \text{nv}_1 = \text{v} \)，这里\( \text{g}_1 \)为\( \text{g} \)的直接子项，可以使用归纳假设，根据\( \text{g}_1 \xrightarrow{e}^* \text{nv}_1 \)以及归纳假设，可得\( \text{g}_1 \xrightarrow{o}^* \text{nv}_1 \)，进而易得\( \text{g} \xrightarrow{o}^* \text{succ } \text{nv}_1 = \text{v} \)。
  4. 如果\( \text{g} = \text{pred } \text{g}_1 \)，此时\( \text{g} \)不是值，得进一步求值得到\( \text{v} \)，为了求值得到\( \text{v} \)，\( \text{g} \)必须摆脱当前的\( \text{pred} \)项形式，唯一的可能就是使用规则E-PREDZERO或E-PREDSUCC，这意味着必须从\( \text{g} \)开始，连续使用0次或者多次使用E-PRED，紧接着使用E-PREDZERO或E-PREDSUCC，即必须\( \text{g}_1 \xrightarrow{e}^* 0 \) 或\( \text{g}_1 \xrightarrow{e}^* \text{succ } \text{nv}_1 \)，进而\( \text{g} \xrightarrow{e}^* \text{pred } 0 \xrightarrow{e} 0 = \text{v} \) 或\( \text{g} \xrightarrow{e}^* \text{pred }(\text{succ } \text{nv}_1) \xrightarrow{e} \text{nv}_1 = \text{v} \)，我们仅讨论\( \text{g}_1 \xrightarrow{e}^* 0, \text{g} \xrightarrow{e}^* \text{pred } 0 \xrightarrow{e} 0 = \text{v} \)的情况，另外一种情况类似，这里\( \text{g}_1 \)为\( \text{g} \)的直接子项，可以使用归纳假设，根据\( \text{g}_1 \xrightarrow{e}^* 0 \)以及归纳假设，可得\( \text{g}_1 \xrightarrow{o}^* 0 \)，进而易得\( \text{g} \xrightarrow{o}^* \text{pred } 0 \xrightarrow{o} 0 = \text{v} \)。
  5. 如果\( \text{g} = \text{iszero } \text{g}_1 \)，此时\( \text{g} \)不是值，得进一步求值得到\( \text{v} \)，为了求值得到\( \text{v} \)，\( \text{g} \)必须摆脱当前的\( \text{iszero} \)项形式，唯一的可能就是使用规则E-ISZEROZERO或E-ISZEROSUCC，这意味着必须从\( \text{g} \)开始，连续使用0次或者多次使用E-ISZERO，紧接着使用E-ISZEROZERO或E-ISZEROSUCC，即必须\( \text{g}_1 \xrightarrow{e}^* 0 \) 或\( \text{g}_1 \xrightarrow{e}^* \text{succ } \text{nv}_1 \)，进而\( \text{g} \xrightarrow{e}^* \text{iszero } 0 \xrightarrow{e} \text{true} = \text{v} \) 或\( \text{g} \xrightarrow{e}^* \text{iszero }(\text{succ } \text{nv}_1) \xrightarrow{e} \text{false} = \text{v} \)，我们仅讨论\( \text{g}_1 \xrightarrow{e}^* 0, \text{g} \xrightarrow{e}^* \text{iszero } 0 \xrightarrow{e} \text{true} = \text{v} \)的情况，另外一种情况类似，这里\( \text{g}_1 \)为\( \text{g} \)的直接子项，可以使用归纳假设，根据\( \text{g}_1 \xrightarrow{e}^* 0 \)以及归纳假设，可得\( \text{g}_1 \xrightarrow{o}^* 0 \)，进而易得\( \text{g} \xrightarrow{o}^* \text{iszero } 0 \xrightarrow{o} \text{true} = \text{v} \)。

归纳完毕，命题对所有项均成立。

证毕。

练习3.5.17

题目：

Two styles of operational semantics are in common use. The one used in this book is called the small-step style, because the definition of the evaluation relation shows how individual steps of computation are used to rewrite a term, bit by bit, until it eventually becomes a value. On top of this, we define a multi-step evaluation relation that allows us to talk about terms evaluating (in many steps) to values. An alternative style, called big-step semantics (or sometimes natural semantics), directly formulates the notion of “this term evaluates to that final value,” written \( \text{t} \Downarrow \text{v} \). The big-step evaluation rules for our language of boolean and arithmetic expressions look like this:

\[ \begin{aligned} \text{v} \Downarrow \text{v} &\qquad \text{(B-VALUE)} \\ \dfrac{\text{t}_1 \Downarrow \text{true} \quad \text{t}_2 \Downarrow \text{v}_2}{ \text{if } \text{t}_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3 \Downarrow \text{v}_2} &\qquad \text{(B-IFTRUE)} \\ \dfrac{\text{t}_1 \Downarrow \text{false} \quad \text{t}_3 \Downarrow \text{v}_3}{ \text{if } \text{t}_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3 \Downarrow \text{v}_3} &\qquad \text{(B-IFFALSE)} \\ \dfrac{\text{t}_1 \Downarrow \text{nv}_1}{\text{succ } \text{t}_1 \Downarrow \text{succ } \text{nv}_1} &\qquad \text{(B-SUCC)} \\ \dfrac{\text{t}_1 \Downarrow 0}{\text{pred } \text{t}_1 \Downarrow 0} &\qquad \text{(B-PREDZERO)} \\ \dfrac{\text{t}_1 \Downarrow \text{succ } \text{nv}_1}{\text{pred } \text{t}_1 \Downarrow \text{nv}_1} &\qquad \text{(B-PREDSUCC)} \\ \dfrac{\text{t}_1 \Downarrow 0}{\text{iszero } \text{t}_1 \Downarrow \text{true}} &\qquad \text{(B-ISZEROZERO)} \\ \dfrac{\text{t}_1 \Downarrow \text{succ } \text{nv}_1}{\text{iszero } \text{t}_1 \Downarrow \text{false}} &\qquad \text{(B-ISZEROSUCC)} \end{aligned} \]

Show that the small-step and big-step semantics for this language coincide, i.e. \( \text{t} \rightarrow^* \text{v} \) iff \( \text{t} \Downarrow \text{v} \).

解答：

首先，我们需要一个引理。

引理1：

  1. 如果\( \text{t}_1 \rightarrow^* \text{t}'_1 \)，则\( \text{if } \text{t}_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3 \rightarrow^* \text{if } \text{t}'_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3 \)。
  2. 如果\( \text{t}_1 \rightarrow^* \text{t}'_1 \)，则\( \text{succ } \text{t}_1 \rightarrow^* \text{succ } \text{t}'_1 \)。
  3. 如果\( \text{t}_1 \rightarrow^* \text{t}'_1 \)，则\( \text{pred } \text{t}_1 \rightarrow^* \text{pred } \text{t}'_1 \)。
  4. 如果\( \text{t}_1 \rightarrow^* \text{t}'_1 \)，则\( \text{iszero } \text{t}_1 \rightarrow^* \text{iszero } \text{t}'_1 \)。

引理中的这几个结论实际上在前面几个练习的证明中是有用到的，不过没有写证明，要么直接类似地说“由于\( \text{t}_1 \rightarrow^* \text{t}'_1 \)当且仅当\( \exists n \in \mathbf{N} \) 以及\( n + 1 \)个项\( \text{w}_0, \text{w}_1, \dots, \text{w}_n \) 满足\( \text{w}_0 = \text{t}_1, \text{w}_n = \text{t}'_1, \forall 0 \leq i < n, \text{w}_i \rightarrow \text{w}_{i + 1} \)，即多步求值实际上就是连续单步求值0次或者多次，对连续单步求值次数\( n \)进行数学归纳，易得\( \text{if } \text{t}_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3 \rightarrow^* \text{if } \text{t}'_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3 \)”，要么直接写“易得”。

不过引理中的这几个结论，确实对连续单步求值次数\( n \)进行数学归纳一下就证出来了，非常好证，这里就省略证明了。

还需要另外一个引理。

引理2：

  1. 如果\( \text{t} = \text{if } \text{t}_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3 \) 且\( \text{t} \rightarrow^* \text{v} \)，则\( \text{t}_1 \rightarrow^* \text{true} \)或\( \text{t}_1 \rightarrow^* \text{false} \)，进而\( \text{t} \rightarrow^* \text{if } \text{true} \text{ then } \text{t}_2 \text{ else } \text{t}_3 \rightarrow \text{t}_2 \rightarrow^* \text{v} \) 或\( \text{t} \rightarrow^* \text{if } \text{false} \text{ then } \text{t}_2 \text{ else } \text{t}_3 \rightarrow \text{t}_3 \rightarrow^* \text{v} \)。
  2. 如果\( \text{t} = \text{succ } \text{t}_1 \) 且\( \text{t} \rightarrow^* \text{v} \)，则\( \text{t}_1 \rightarrow^* \text{nv}_1, \text{t} \rightarrow^* \text{succ } \text{nv}_1 = \text{v} \)。
  3. 如果\( \text{t} = \text{pred } \text{t}_1 \) 且\( \text{t} \rightarrow^* \text{v} \)，则\( \text{t}_1 \rightarrow^* 0 \)或\( \text{t}_1 \rightarrow^* \text{succ } \text{nv}_1 \)，进而\( \text{t} \rightarrow^* \text{pred } 0 \rightarrow 0 = \text{v} \) 或\( \text{t} \rightarrow^* \text{pred } (\text{succ } \text{nv}_1) \rightarrow \text{nv}_1 = \text{v} \)。
  4. 如果\( \text{t} = \text{iszero } \text{t}_1 \) 且\( \text{t} \rightarrow^* \text{v} \)，则\( \text{t}_1 \rightarrow^* 0 \)或\( \text{t}_1 \rightarrow^* \text{succ } \text{nv}_1 \)，进而\( \text{t} \rightarrow \text{iszero } 0 \rightarrow \text{true} = \text{v} \) 或\( \text{t} \rightarrow \text{iszero } (\text{succ } \text{nv}_1) \rightarrow \text{false} = \text{v} \)。

同引理1，引理2的这几个结论也在之前练习的证明中用到过，具体的，在证明练习3.5.16中命题(b)的充分性时，我们用到了这几个结论，不过那边的说明是比较口语化的。

同引理1，针对这几个结论，对连续单步求值次数\( n \)进行数学归纳一下就证出来了（基础情况是\( n = 1 \)，而不是\( n = 0 \)，因为不可能不求值，就从非值\( \text{t} \)变成值\( \text{v} \)），非常好证，这里同引理1也省略证明。

现在，我们可以证明必要性了。

证明必要性：

如果\( \text{t} \rightarrow^* \text{v} \)，我们要证明\( \text{t} \Downarrow \text{v} \)，使用结构归纳法，归纳假设命题对所有\( \text{t} \)的直接子项成立，我们要证明命题对\( \text{t} \)成立，对\( \text{t} \)的形式进行分类讨论：

  1. 如果\( \text{t} \)为值，则\( \text{t} = \text{v} \)，此时使用B-VALUE，可得\( \text{t} = \text{v} \Downarrow \text{v} \)。
  2. 如果\( \text{t} = \text{if } \text{t}_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3 \)，则由\( \text{t} \rightarrow^* \text{v} \)以及引理2的1，可得\( \text{t}_1 \rightarrow^* \text{true} \)或\( \text{t}_1 \rightarrow^* \text{false} \)，进而\( \text{t} \rightarrow^* \text{if } \text{true} \text{ then } \text{t}_2 \text{ else } \text{t}_3 \rightarrow \text{t}_2 \rightarrow^* \text{v} \) 或\( \text{t} \rightarrow^* \text{if } \text{false} \text{ then } \text{t}_2 \text{ else } \text{t}_3 \rightarrow \text{t}_3 \rightarrow^* \text{v} \)，我们仅讨论\( \text{t}_1 \rightarrow^* \text{true}, \text{t} \rightarrow^* \text{if } \text{true} \text{ then } \text{t}_2 \text{ else } \text{t}_3 \rightarrow \text{t}_2 \rightarrow^* \text{v} \)，另外一种情况类似，这里\( \text{t}_1 \)是\( \text{t} \)的直接子项，可以使用归纳假设，根据\( \text{t}_1 \rightarrow^* \text{true} \)以及归纳假设，可得\( \text{t}_1 \Downarrow \text{true} \)， \( \text{t}_2 \)也是\( \text{t} \)的直接子项，由\( \text{t}_2 \rightarrow^* \text{v} \)以及归纳假设，可得\( \text{t}_2 \Downarrow \text{v} \)，进而使用B-IFTRUE，可得\( \text{t} \Downarrow \text{v} \)。
  3. 如果\( \text{t} = \text{succ } \text{t}_1 \)，则由\( \text{t} \rightarrow^* \text{v} \)以及引理2的2，可得\( \text{t}_1 \rightarrow^* \text{nv}_1, \text{t} \rightarrow^* \text{succ } \text{nv}_1 = \text{v} \)，这里\( \text{t}_1 \)是\( \text{t} \)的直接子项，根据\( \text{t}_1 \rightarrow^* \text{nv}_1 \)以及归纳假设，可得\( \text{t}_1 \Downarrow \text{nv}_1 \)，进而使用E-SUCC，可得\( \text{t} \Downarrow \text{succ } \text{nv}_1 = \text{v} \)。
  4. 如果\( \text{t} = \text{pred } \text{t}_1 \)，则由\( \text{t} \rightarrow^* \text{v} \)以及引理2的3，可得\( \text{t}_1 \rightarrow^* 0 \)或\( \text{t}_1 \rightarrow^* \text{succ } \text{nv}_1 \)，进而\( \text{t} \rightarrow^* \text{pred } 0 \rightarrow 0 = \text{v} \) 或\( \text{t} \rightarrow^* \text{pred } (\text{succ } \text{nv}_1) \rightarrow \text{nv}_1 = \text{v} \) 我们仅讨论\( \text{t}_1 \rightarrow^* 0, \text{t} \rightarrow^* \text{pred } 0 \rightarrow 0 = \text{v} \)，另外一种情况类似，这里\( \text{t}_1 \)是\( \text{t} \)的直接子项，根据\( \text{t}_1 \rightarrow^* 0 \)以及归纳假设，可得\( \text{t}_1 \Downarrow 0 \)，进而使用E-PREDZERO，可得\( \text{t} \Downarrow 0 = \text{v} \)。
  5. 如果\( \text{t} = \text{iszero } \text{t}_1 \)，则由\( \text{t} \rightarrow^* \text{v} \)以及引理2的4，可得\( \text{t}_1 \rightarrow^* 0 \)或\( \text{t}_1 \rightarrow^* \text{succ } \text{nv}_1 \)，进而\( \text{t} \rightarrow^* \text{iszero } 0 \rightarrow \text{true} = \text{v} \) 或\( \text{t} \rightarrow^* \text{iszero } (\text{succ } \text{nv}_1) \rightarrow \text{false} = \text{v} \) 我们仅讨论\( \text{t}_1 \rightarrow^* 0, \text{t} \rightarrow^* \text{iszero } 0 \rightarrow \text{true} = \text{v} \)，另外一种情况类似，这里\( \text{t}_1 \)是\( \text{t} \)的直接子项，根据\( \text{t}_1 \rightarrow^* 0 \)以及归纳假设，可得\( \text{t}_1 \Downarrow 0 \)，进而使用E-ISZEROZERO，可得\( \text{t} \Downarrow \text{true} = \text{v} \)。

归纳完毕，命题对所有项均成立。

证毕。

接着，证明充分性。

证明充分性：

如果\( \text{t} \Downarrow \text{v} \)，我们要证明\( \text{t} \rightarrow^* \text{v} \)，使用结构归纳法，归纳假设命题对所有\( \text{t} \)的直接子项成立，我们要证明命题对\( \text{t} \)成立，对\( \text{t} \Downarrow \text{v} \)使用的规则进行分类讨论：

  1. 如果使用的规则是B-VALUE，则\( \text{t} = \text{v} \)，此时直接有\( \text{t} = \text{v} \rightarrow^* \text{v} \)。
  2. 如果使用的规则是B-IFTRUE，则\( \text{t} = \text{if } \text{t}_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3， \text{t}_1 \Downarrow \text{true}, \text{t}_2 \Downarrow \text{v}, \text{t} \Downarrow \text{v} \)，这里\( \text{t}_2 \)为\( \text{t} \)的直接子项，根据\( \text{t}_2 \Downarrow \text{v} \)以及归纳假设，可得\( \text{t}_2 \rightarrow^* \text{v} \)， \( \text{t}_1 \)也为\( \text{t} \)的直接子项，根据\( \text{t}_1 \Downarrow \text{true} \)以及归纳假设，可得\( \text{t}_1 \rightarrow^* \text{true} \)，进而根据引理1的1，可得\( \text{t} \rightarrow^* \text{if } \text{true} \text{ then } \text{t}_2 \text{ else } \text{t}_3 \rightarrow \text{t}_2 \rightarrow^* \text{v} \)，进而可得\( \text{t} \rightarrow^* \text{v} \)。
  3. 如果使用的规则是B-IFFALSE，则\( \text{t} = \text{if } \text{t}_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3， \text{t}_1 \Downarrow \text{false}, \text{t}_3 \Downarrow \text{v}, \text{t} \Downarrow \text{v} \)，这里\( \text{t}_3 \)为\( \text{t} \)的直接子项，根据\( \text{t}_3 \Downarrow \text{v} \)以及归纳假设，可得\( \text{t}_3 \rightarrow^* \text{v} \)， \( \text{t}_1 \)也为\( \text{t} \)的直接子项，根据\( \text{t}_1 \Downarrow \text{false} \)以及归纳假设，可得\( \text{t}_1 \rightarrow^* \text{false} \)，进而根据引理1的1，可得\( \text{t} \rightarrow^* \text{if } \text{false} \text{ then } \text{t}_2 \text{ else } \text{t}_3 \rightarrow \text{t}_3 \rightarrow^* \text{v} \)，进而可得\( \text{t} \rightarrow^* \text{v} \)。
  4. 如果使用的规则是B-SUCC，则\( \text{t} = \text{succ } \text{t}_1, \text{t}_1 \Downarrow \text{nv}_1, \text{t} \Downarrow \text{succ } \text{nv}_1 = \text{v} \)，这里\( \text{t}_1 \)为\( \text{t} \)的直接子项，根据\( \text{t}_1 \Downarrow \text{nv}_1 \)以及归纳假设，可得\( \text{t}_1 \rightarrow^* \text{nv}_1 \)，进而根据引理1的2，可得\( \text{t} \rightarrow^* \text{succ } \text{nv}_1 = \text{v} \)。
  5. 如果使用的规则是B-PREDZERO，则\( \text{t} = \text{pred } \text{t}_1, \text{t}_1 \Downarrow 0, \text{t} \Downarrow 0 = \text{v} \)，这里\( \text{t}_1 \)为\( \text{t} \)的直接子项，根据\( \text{t}_1 \Downarrow 0 \)以及归纳假设，可得\( \text{t}_1 \rightarrow^* 0 \)，进而根据引理1的3，可得\( \text{t} \rightarrow^* \text{pred } 0 \rightarrow 0 = \text{v} \)，进而可得\( \text{t} \rightarrow^* \text{v} \)。
  6. 如果使用的规则是B-PREDSUCC，则\( \text{t} = \text{pred } \text{t}_1, \text{t}_1 \Downarrow \text{succ } \text{nv}_1, \text{t} \Downarrow \text{nv}_1 = \text{v} \)，这里\( \text{t}_1 \)为\( \text{t} \)的直接子项，根据\( \text{t}_1 \Downarrow \text{succ } \text{nv}_1 \)以及归纳假设，可得\( \text{t}_1 \rightarrow^* \text{succ } \text{nv}_1 \)，进而根据引理1的3，可得\( \text{t} \rightarrow^* \text{pred } (\text{succ } \text{nv}_1) \rightarrow \text{nv}_1 = \text{v} \)，进而可得\( \text{t} \rightarrow^* \text{v} \)。
  7. 如果使用的规则是B-ISZEROZERO，则\( \text{t} = \text{iszero } \text{t}_1, \text{t}_1 \Downarrow 0, \text{t} \Downarrow \text{true} = \text{v} \)，这里\( \text{t}_1 \)为\( \text{t} \)的直接子项，根据\( \text{t}_1 \Downarrow 0 \)以及归纳假设，可得\( \text{t}_1 \rightarrow^* 0 \)，进而根据引理1的4，可得\( \text{t} \rightarrow^* \text{iszero } 0 \rightarrow \text{true} = \text{v} \)，进而可得\( \text{t} \rightarrow^* \text{v} \)。
  8. 如果使用的规则是B-ISZEROSUCC，则\( \text{t} = \text{iszero } \text{t}_1, \text{t}_1 \Downarrow \text{succ } \text{nv}_1, \text{t} \Downarrow \text{false} = \text{v} \)，这里\( \text{t}_1 \)为\( \text{t} \)的直接子项，根据\( \text{t}_1 \Downarrow \text{succ } \text{nv}_1 \)以及归纳假设，可得\( \text{t}_1 \rightarrow^* \text{succ } \text{nv}_1 \)，进而根据引理1的4，可得\( \text{t} \rightarrow^* \text{iszero } (\text{succ } \text{nv}_1) \rightarrow \text{false} = \text{v} \)，进而可得\( \text{t} \rightarrow^* \text{v} \)。

归纳完毕，命题对所有项均成立。

证毕。

练习3.5.18

题目：

Suppose we want to change the evaluation strategy of our language so that the \( \text{then} \) and \( \text{else} \) branches of an \( \text{if} \) expression are evaluated (in that order) before the guard is evaluated. Show how the evaluation rules need to change to achieve this effect.

解答：

删掉E-IFTRUE、E-IFFALSE、E-IF规则，增加如下规则：

\[ \begin{aligned} \dfrac{\text{t}_2 \rightarrow \text{t}'_2}{ \text{if } \text{t}_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3 \rightarrow \text{if } \text{t}_1 \text{ then } \text{t}'_2 \text{ else } \text{t}_3} &\qquad \text{(E-IF-THEN)} \\ \dfrac{\text{t}_3 \rightarrow \text{t}'_3}{ \text{if } \text{t}_1 \text{ then } \text{v}_2 \text{ else } \text{t}_3 \rightarrow \text{if } \text{t}_1 \text{ then } \text{v}_2 \text{ else } \text{t}'_3} &\qquad \text{(E-IF-THENVALUE-ELSE)} \\ \dfrac{\text{t}_1 \rightarrow \text{t}'_1}{ \text{if } \text{t}_1 \text{ then } \text{v}_2 \text{ else } \text{v}_3 \rightarrow \text{if } \text{t}'_1 \text{ then } \text{v}_2 \text{ else } \text{v}_3} &\qquad \text{(E-IF-THENVALUE-ELSEVALUE)} \\ \text{if } \text{true} \text{ then } \text{v}_2 \text{ else } \text{v}_3 \rightarrow \text{v}_2 &\qquad \text{(E-IF-TRUE-THENVALUE-ELSEVALUE)} \\ \text{if } \text{false} \text{ then } \text{v}_2 \text{ else } \text{v}_3 \rightarrow \text{v}_3 &\qquad \text{(E-IF-FALSE-THENVALUE-ELSEVALUE)} \end{aligned} \]

规则E-IF-THENVALUE-ELSE要求对\( \text{else} \)分支求值时， \( \text{then} \)分支必须已经求值成某个值了，即限制了\( \text{else} \)分支必须在\( \text{then} \)分支后求值。规则E-IF-THENVALUE-ELSEVALUE要求对条件项（guard）求值时， \( \text{then} \)分支和\( \text{else} \)分支必须均已经求值成某个值了，即限制了条件项必须在\( \text{then} \)分支和\( \text{else} \)分支后求值。最后的计算规则E-IF-TRUE-THENVALUE-ELSEVALUE和E-IF-FALSE-THENVALUE-ELSEVALUE 则确保了在\( \text{then} \)分支、\( \text{else} \)分支，条件项均求值成值后，且条件项类型正确，为\( \text{bool} \)类型的值时，我们可以计算/化简\( \text{if} \)语句。综上，上述的规则修改实现了题目的要求。

更新于 2022-11-05
 数学, 类型理论
返回 | 主页