OSFVA
所有文章 标签
OSFVA

目录

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

CloseToZero
   约 19858 字   预计阅读 40 分钟 

第11章

章节11.2

练习11.2.1

题目：

Is there a way of constructing a sequence of terms \( \text{t}_1, \text{t}_2, \dots \), in the simply typed lambda-calculus with only the base type Unit, such that, for each \( n \), the term \( \text{t}_n \) as size at most \( O(n) \) but requires at least \( O(2^n) \) steps of evaluation to reach a normal form?

解答：

定义\( \text{t}_1 \)如下：

\[ \text{t}_1 = (\lambda \text{x}: \text{Unit. } \text{x}) \text{ } \text{unit} \]

归纳假设\( \forall n = k, \text{t}_k \)已定义，我们定义\( \text{t}_{k + 1} \)如下：

\[ \text{t}_{k + 1} = (\lambda \text{f}: \text{Unit} \to \text{Unit. } \text{f } (\text{f unit})) \text{ } (\lambda \text{x}: \text{Unit. } \text{t}_k) \]

我们首先证明\( \text{t}_n \)的大小为\( O(n) \)，注意到\( \forall k \geq 1, \text{t}_{k + 1} \)均在\( \text{t}_k \)的基础上增加固定数量的节点（这里的节点是指抽象语法树的节点），且每次的增加的节点数量都是一样的，比如\( \text{t}_2 \)相对\( \text{t}_1 \)增加的节点数量和\( \text{t}_3 \)相对\( \text{t}_2 \)增加的节点数量一样，我们记这个固定增加的节点数量为\( d \)，则\( \forall k \geq 1, \mathit{size}(\text{t}_{k + 1}) = \mathit{size}(\text{t}_k) + d \)，于是给定\( n \geq 1 \)，有\( \mathit{size}(\text{t}_n) = \mathit{size}(\text{t}_1) + (n - 1)d \)，这里\( d \)为常数，加上\( \mathit{size}(\text{t}_1) \)为常数，可得\( \mathit{size}(\text{t}_n) \)为\( O(n) \) （这里“\( \mathit{size}(\text{t}_n) \)为\( O(n) \)”这句话对\( O(n) \)的用法是不严谨的，不过读者应该能理解什么意思）。

最后，我们证明\( \text{t}_n \)求值到范式所需的步骤为\( O(2^n) \)，给定一个项\( \text{t} \)，我们记\( \mathit{steps}(\text{t}) \)为\( \text{t} \)求值到范式所需的步骤，注意到\( \text{t}_2 \)把\( \text{t}_1 \)的计算重复了两遍，因此\( \mathit{steps}(\text{t}_2) = 2 * \mathit{steps}(\text{t}_1) \)，以此类推，易得\( \forall k \geq 1, \mathit{steps}(\text{t}_{k + 1}) = 2 * \mathit{steps}(\text{t}_k) \)，进而可得给定\( n \geq 1 \)，有\( \mathit{steps}(\text{t}_n) = 2^{n - 1} * \mathit{steps}(\text{t}_1) \)，这里\( \mathit{steps}(\text{t}_1) \)是个常数，可得\( \mathit{steps}(\text{t}_n) \)为\( O(2^n) \) （同上，这里对\( O \)符号的用法不严谨）。

附注：上面\( \text{t}_n \)大小实际为\( \Theta(n) \)、求值到范式的步骤数实际为\( \Theta(2^n) \)，而不仅仅是\( O(n) \)、\( O(2^n) \)。

章节11.3

练习11.3.2

题目：

Give typing and evaluation rules for wildcard abstractions, and prove that they can be derived from the abbreviation stated above.

注：

这题不难，就是要严格点说很麻烦，细节很多。

解答：

注意下，在拓展项中，我们会将形如\( \lambda \text{\_}: \text{T}_1 \text{. } \text{t}_{11} \)的项也视为值。

首先是求值规则，由于函数体中不会用到\( \lambda \)-抽象的参数，因此求值不需要进行变量代入，如下：

\[ (\lambda \text{\_}: \text{T}_1 \text{. } \text{t}_{11}) \text{ } \text{v}_2 \rightarrow \text{t}_{11} \quad (\text{E-WILDCARD}) \]

接着是类型规则，同理，由于函数体中不会用到\( \lambda \)-抽象的参数，因此不需要拓展类型上下文，如下：

\[ \dfrac{\Gamma \vdash \text{t}_{11}: \text{T}_{11}}{ \Gamma \vdash \lambda \text{\_}: \text{T}_1 \text{. } \text{t}_{11}: \text{T}_{11}} \quad (\text{T-WILDCARD}) \]

我们递归定义通配符的elaboration函数\( e \)，\( \forall \)拓展项\( \text{t} \)，按如下规则定义\( e(\text{t}) \)：

  1. 如果\( \text{t} = \lambda \text{\_}: \text{T}_1 \text{. } \text{t}_{11} \)，则令\( e(\text{t}) = \lambda \text{x}: \text{T}_1 \text{. } e(\text{t}_{11}) \)，这里\( \text{x} \)为没有出现在\( e(\text{t}_{11}) \)中的新变量。
  2. 如果\( \text{t} = \lambda \text{x}: \text{T}_1 \text{. } \text{t}_{11} \)，则令\( e(\text{t}) = \lambda \text{x}: \text{T}_1 \text{. } e(\text{t}_{11}) \)。
  3. 如果\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)，则令\( e(\text{t}) = e(\text{t}_1) \text{ } e(\text{t}_2) \)。
  4. 如果\( \text{t} = \text{x} \)，则\( e(\text{t}) = \text{x} \)。

我们证明该派生形式是合法的，即\( \forall \)拓展项\( \text{t} \)：

  1. 如果\( \text{t} \rightarrow^E \text{t}' \)，则\( e(\text{t}) \rightarrow^I e(\text{t}') \)。
  2. 如果\( e(\text{t}) \rightarrow^I \text{u} \)，则\( \exists \text{t}', e(\text{t}') = \text{u}, \text{t} \rightarrow^E \text{t}' \)。
  3. \( \Gamma \vdash^E \text{t}: \text{T} \)当且即当\( \Gamma \vdash^I e(\text{t}): \text{T} \)。

首先需要证明多个引理：

引理1：

\( \forall \)变量名\( \text{x} \)，\( \forall \)拓展项中的值\( \text{v} \)，\( \forall \)拓展项\( \text{t} \)，我们有\( e([\text{x} \mapsto \text{v}]\text{t}) = [\text{x} \mapsto e(\text{v})]e(\text{t}) \)。

证明引理1：

用结构归纳法，对\( \text{t} \)的形式进行分情况讨论，很容易证明，这里省略。

证明引理1完毕。

引理2：

\( \forall \)拓展项中的值\( \text{v} \)，有\( e(\text{v}) \)仍为值。

证明引理2：

通过\( e \)函数的定义可直接发现引理2成立。

证明引理2完毕。

引理3：

\( \forall \)拓展项中的非值\( \text{t} \)，有\( e(\text{t}) \)仍不为值。

证明引理3：

通过\( e \)函数的定义可直接发现引理3成立。

证明引理3完毕。

引理4：

\( \forall \)变量名\( \text{x} \)，\( \forall \)拓展项\( \text{t} \)，如果\( \text{x} \)没有出现在\( \text{t} \)中，则\( \text{x} \)也不会出现在\( e(\text{t}) \)中。

证明引理4：

用结构归纳法，对\( \text{t} \)的形式进行分情况讨论，很容易证明，这里省略。

证明引理4完毕。

证明第1点：

\( \forall \)拓展项\( \text{t} \)，归纳假设命题对\( \text{t} \)的直接子项成立，我们证明命题对\( \text{t} \)成立，对\( \text{t} \rightarrow^E \text{t}' \)使用的规则进行分情况讨论：

  1. 如果\( \text{t} \rightarrow^E \text{t}' \)使用的规则是E-APP1，则\( \text{t} = \text{t}_1 \text{ } \text{t}_2, \text{t}' = \text{t}'_1 \text{ } \text{t}_2, \text{t}_1 \rightarrow^E \text{t}'_1 \)，于是有\( e(\text{t}) = e(\text{t}_1) \text{ } e(\text{t}_2), e(\text{t}') = e(\text{t}'_1) \text{ } e(\text{t}_2) \)，进而根据\( \text{t}_1 \rightarrow^E \text{t}'_1 \)以及归纳假设，可得\( e(\text{t}_1) \rightarrow^I e(\text{t}'_1) \)，再使用规则E-APP可得，\( e(\text{t}) \rightarrow^I e(\text{t}') \)。
  2. 如果\( \text{t} \rightarrow^E \text{t}' \)使用的规则是E-APP2，则\( \text{t} = \text{v}_1 \text{ } \text{t}_2, \text{t}' = \text{v}_1 \text{ } \text{t}'_2, \text{t}_2 \rightarrow^E \text{t}'_2 \)，于是有\( e(\text{t}) = e(\text{v}_1) \text{ } e(\text{t}_2), e(\text{t}') = e(\text{v}_1) \text{ } e(\text{t}'_2) \)，进而根据\( \text{t}_2 \rightarrow^E \text{t}'_2 \)以及归纳假设，可得\( e(\text{t}_2) \rightarrow^I e(\text{t}'_2) \)，再使用规则E-APP2可得，\( e(\text{t}) \rightarrow^I e(\text{t}') \)。
  3. 如果\( \text{t} \rightarrow^E \text{t}' \)使用的规则是E-APPABS，则\( \text{t} = (\lambda \text{x}: \text{T}_1 \text{. } \text{t}_{11}) \text{ } \text{v}_2, \text{t}' = [\text{x} \mapsto \text{v}_2]\text{t}_{11} \)，于是有\( e(\text{t}) = e(\lambda \text{x}: \text{T}_1 \text{. } \text{t}_{11}) \text{ } e(\text{v}_2) = (\lambda \text{x}: \text{T}_1 \text{. } e(\text{t}_{11})) \text{ } e(\text{v}_2), e(\text{t}') = e([\text{x} \mapsto \text{v}_2]\text{t}_{11}) \)，通过E-APPABS，可得\( e(\text{t}) \rightarrow^I [\text{x} \mapsto e(\text{v}_2)]e(\text{t}_{11}) \)，根据引理1，可得\( [\text{x} \mapsto e(\text{v}_2)]e(\text{t}_{11}) = e(\text{t}') \)，于是有\( e(\text{t}) \rightarrow^I e(\text{t}') \)。
  4. 如果\( \text{t} \rightarrow^E \text{t}' \)使用的规则是E-WILDCARD，则\( \text{t} = (\lambda \text{\_}: \text{T}_1 \text{. } \text{t}_{11}) \text{ } \text{v}_2, \text{t}' = \text{t}_{11} \)，于是有\( e(\text{t}) = e(\lambda \text{\_}: \text{T}_1 \text{. } \text{t}_{11}) \text{ } e(\text{v}_2) = (\lambda \text{x}: \text{T}_1 \text{. } e(\text{t}_{11})) \text{ } e(\text{v}_2) \)，这里\( \text{x} \)为没有出现在\( e(\text{t}_{11}) \)中的新变量，还可得\( e(\text{t}') = e(\text{t}_{11}) \)，通过E-APPABS，可得\( e(\text{t}) \rightarrow^I [\text{x} \mapsto e(\text{v}_2)]e(\text{t}_{11}) \)，这里由于\( \text{x} \)没有出现在\( \text{t}_{11} \)中，进而根据引理4，可得\( \text{x} \)也没有出现在\( e(\text{t}_{11}) \)中，因此\( [\text{x} \mapsto e(\text{v}_2)]e(\text{t}_{11}) = e(\text{t}_{11}) = e(\text{t}') \)，进而可得\( e(\text{t}) \rightarrow^I e(\text{t}') \)。

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

证明第1点完毕。

证明第2点：

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

  1. 如果\( \text{t} = \text{x} \)，则\( e(\text{t}) = \text{x} \)为范式，这和\( e(\text{t}) \rightarrow^I \text{u} \)矛盾，因此这种情况不可能。
  2. 如果\( \text{t} = \lambda \text{x}: \text{T}_1 \text{. } \text{t}_{11} \)，则\( e(\text{t}) = \lambda \text{x}: \text{T}_1 \text{. } e(\text{t}_{11}) \)为范式，这和\( e(\text{t}) \rightarrow_I \text{u} \)矛盾，因此这种情况不可能。
  3. 如果\( \text{t} = \lambda \text{\_}: \text{T}_1 \text{. } \text{t}_{11} \)，则\( e(\text{t}) = \lambda \text{x}: \text{T}_1 \text{. } e(\text{t}_{11}) \)，这里\( \text{x} \)为没有出现在\( e(\text{t}_{11}) \)中的新变量，可得\( e(\text{t}) \)为范式，这和\( e(\text{t}) \rightarrow_I \text{u} \)矛盾，因此这种情况不可能。
  4. 如果\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)：
    1. 如果\( \text{t}_1 \)为值，则\( \text{t}_1 = \lambda \text{x}: \text{T}_1 \text{. } \text{t}_{11} \)或 \( \text{t}_1 = \lambda \text{\_}: \text{T}_1 \text{. } \text{t}_{11} \)：
      1. 如果\( \text{t}_1 = \lambda \text{x}: \text{T}_1 \text{. } \text{t}_{11} \)：
        1. 如果\( \text{t}_2 \)为值，则令\( \text{v}_2 = \text{t}_2 \)，有\( e(\text{t}) = e(\lambda \text{x}: \text{T}_1 \text{. } \text{t}_{11}) \text{ } e(\text{v}_2) = (\lambda \text{x}: \text{T}_1 \text{. } e(\text{t}_{11})) \text{ } e(\text{v}_2) \)，根据引理2，可得\( e(\text{v}_2) \)仍然为值，进而可得\( e(\text{t}) \rightarrow^I \text{u} \)使用的规则是E-APPABS，有\( \text{u} = [\text{x} \mapsto e(\text{v}_2)]e(\text{t}_{11}) \)，进而根据引理1，可得\( \text{u} = [\text{x} \mapsto e(\text{v}_2)]e(\text{t}_{11}) = e([\text{x} \mapsto \text{v}_2]\text{t}_{11}) \)，令\( \text{t}' = [\text{x} \mapsto \text{v}_2]\text{t}_{11} \)，有\( e(\text{t}') = \text{u} \)，同时根据E-APPABS，有\( \text{t} \rightarrow^E \text{t}' \)。
        2. 如果\( \text{t}_2 \)不为值，则\( e(\text{t}) = e(\lambda \text{x}: \text{T}_1 \text{. } \text{t}_{11}) \text{ } e(\text{t}_2) = (\lambda \text{x}: \text{T}_1 \text{. } e(\text{t}_{11})) \text{ } e(\text{t}_2) \)，根据引理3，可得\( e(\text{t}_2) \)仍然不为值，进而可得\( e(\text{t}) \rightarrow^I \text{u} \)使用的规则是E-APP2，有\( e(\text{t}_2) \rightarrow^I \text{u}_2, \text{u} = (\lambda \text{x}: \text{T}_1 \text{. } e(\text{t}_{11})) \text{ } \text{u}_2 \)，根据\( e(\text{t}_2) \rightarrow^I \text{u}_2 \)以及归纳假设，可得\( \exists \text{t}'_2, e(\text{t}'_2) = \text{u}_2, \text{t}_2 \rightarrow^E \text{t}'_2 \)，令\( \text{t}' = (\lambda \text{x}: \text{T}_1 \text{. } \text{t}_{11}) \text{ } \text{t}'_2 \)，则可得\( e(\text{t}') = \text{u} \)，且根据\( \text{t}_2 \rightarrow^E \text{t}'_2 \)以及E-APP2，可得\( \text{t} \rightarrow^E \text{t}' \)。
      2. 如果\( \text{t}_1 = \lambda \text{\_}: \text{T}_1 \text{. } \text{t}_{11} \)：
        1. 如果\( \text{t}_2 \)为值，则令\( \text{v}_2 = \text{t}_2 \)，有\( e(\text{t}) = e(\lambda \text{\_}: \text{T}_1 \text{. } \text{t}_{11}) \text{ } e(\text{v}_2) = (\lambda \text{x}: \text{T}_1 \text{. } e(\text{t}_{11})) \text{ } e(\text{v}_2) \)，这里\( \text{x} \)为没有出现在\( e(\text{t}_{11}) \)中的新变量，根据引理2，可得\( e(\text{v}_2) \)仍然为值，进而可得\( e(\text{t}) \rightarrow^I \text{u} \)使用的规则是E-APPABS，有\( \text{u} = [\text{x} \mapsto e(\text{v}_2)]e(\text{t}_{11}) \)，这里由于\( \text{x} \)没有出现在\( \text{t}_{11} \)中，进而根据引理4，可得\( \text{x} \)也没有出现在\( e(\text{t}_{11}) \)中，因此\( \text{u} = [\text{x} \mapsto e(\text{v}_2)]e(\text{t}_{11}) = e(\text{t}_{11}) \)，于是令\( \text{t}' = \text{t}_{11} \)，有\( e(\text{t}') = \text{u} \)，同时根据E-WILDCARD，有\( \text{t} \rightarrow^E \text{t}' \)。
        2. 如果\( \text{t}_2 \)不为值，则\( e(\text{t}) = e(\lambda \text{\_}: \text{T}_1 \text{. } \text{t}_{11}) \text{ } e(\text{t}_2) = (\lambda \text{x}: \text{T}_1 \text{. } e(\text{t}_{11})) \text{ } e(\text{t}_2) \)，这里\( \text{x} \)为没有出现在\( e(\text{t}_{11}) \)中的新变量，根据引理3，可得\( e(\text{t}_2) \)仍然不为值，进而可得\( e(\text{t}) \rightarrow^I \text{u} \)使用的规则是E-APP2，有\( e(\text{t}_2) \rightarrow^I \text{u}_2, \text{u} = (\lambda \text{x}: \text{T}_1 \text{. } e(\text{t}_{11})) \text{ } \text{u}_2 \)，根据\( e(\text{t}_2) \rightarrow^I \text{u}_2 \)以及归纳假设，可得\( \exists \text{t}'_2, e(\text{t}'_2) = \text{u}_2, \text{t}_2 \rightarrow^E \text{t}'_2 \)，令\( \text{t}' = (\lambda \text{\_}: \text{T}_1 \text{. } \text{t}_{11}) \text{ } \text{t}'_2 \)，则可得\( e(\text{t}') = \text{u} \)（取同样的新变量\( \text{x} \)），且根据\( \text{t}_2 \rightarrow^E \text{t}'_2 \)以及E-APP2，可得\( \text{t} \rightarrow^E \text{t}' \)。
    2. 如果\( \text{t}_1 \)不为值，则\( e(\text{t}) = e(\text{t}_1) \text{ } e(\text{t}_2) \)，根据引理3，可得\( e(\text{t}_1) \)仍然不为值，进而可得\( e(\text{t}) \rightarrow^I \text{u} \)使用的规则是E-APP1，有\( e(\text{t}_1) \rightarrow^I \text{u}_1, \text{u} = \text{u}_1 \text{ } e(\text{t}_2) \)，根据\( e(\text{t}_1) \rightarrow^I \text{u}_1 \)以及归纳假设，可得\( \exists \text{t}'_1, e(\text{t}'_1) = \text{u}_1, \text{t}_1 \rightarrow^E \text{t}'_1 \)，令\( \text{t}' = \text{t}'_1 \text{ } \text{t}_2 \)，则可得\( e(\text{t}') = \text{u} \)，且根据\( \text{t}_1 \rightarrow^E \text{t}'_1 \)以及E-APP1，可得\( \text{t} \rightarrow^E \text{t}' \)。

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

证明第2点完毕。

证明第3点：

充分性：

如果\( \Gamma \vdash^E \text{t}: \text{T} \)，我们要证明\( \Gamma \vdash^I e(\text{t}): \text{T} \)：

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

  1. 如果\( \text{t} = \text{x} \)，则\( \Gamma \vdash^E \text{t}: \text{T} \)使用的规则是T-VAR，有\( \text{x}: \text{T} \in \Gamma \)，可得\( e(\text{t}) = e(\text{x}) = \text{x} \in \Gamma \)，进而可得\( \Gamma \vdash^I e(\text{t}): \text{T} \)。
  2. 如果\( \text{t} = \lambda \text{x}: \text{T}_1 \text{. } \text{t}_{11} \)，则\( e(\text{t}) = \lambda \text{x}: \text{T}_1 \text{. } e(\text{t}_{11}) \)，可得\( \Gamma \vdash^E \text{t}: \text{T} \)使用的规则是T-ABS，于是有\( \Gamma, \text{x}: \text{T}_1 \vdash^E \text{t}_{11}: \text{T} \)，根据归纳假设，可得\( \Gamma, \text{x}: \text{T}_1 \vdash^I e(\text{t}_{11}): \text{T} \)，进而根据T-ABS，可得\( \Gamma \vdash^I e(\text{t}): \text{T} \)。
  3. 如果\( \text{t} = \lambda \text{\_}: \text{T}_1 \text{. } \text{t}_{11} \)，则\( e(\text{t}) = \lambda \text{x}: \text{T}_1 \text{. } e(\text{t}_{11}) \)，这里\( \text{x} \)为没有出现在\( e(\text{t}_{11}) \)中的新变量，可得\( \Gamma \vdash^E \text{t}: \text{T} \)使用的规则是T-WILDCARD，于是有\( \Gamma \vdash^E \text{t}_{11}: \text{T} \)，根据归纳假设，可得\( \Gamma \vdash^I e(\text{t}_{11}): \text{T} \)，这里由于\( \text{x} \)为没有出现在\( e(\text{t}_{11}) \)中的新变量，进而根据引理4，可得\( \text{x} \)也没有出现在\( e(\text{t}_{11}) \)中，于是在类型上下文\( \Gamma \)中额外添加\( \text{x} \)的类型不会影响到\( e(\text{t}_{11}) \)的类型，因此\( \Gamma, \text{x}: \text{T}_1 \vdash^I e(\text{t}_{11}): \text{T} \)，进而根据T-ABS，可得\( \Gamma \vdash^I e(\text{t}): \text{T} \)。
  4. 如果\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)，则\( e(\text{t}) = e(\text{t}_1) \text{ } e(\text{t}_2) \)，可得\( \Gamma \vdash^E \text{t}: \text{T} \)使用的规则是T-APP，于是有\( \Gamma \vdash^E \text{t}_1: \text{T}_1 \to \text{T}, \Gamma \vdash^E \text{t}_2: \text{T}_1 \)，根据归纳假设，可得\( \Gamma \vdash^I e(\text{t}_1): \text{T}_1 \to \text{T}, \Gamma \vdash^I e(\text{t}_2): \text{T}_1 \)，进而根据T-APP，可得\( \Gamma \vdash^I e(\text{t}): \text{T} \)。

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

必要性：

如果\( \Gamma \vdash^I e(\text{t}): \text{T} \)，我们要证明\( \Gamma \vdash^E \text{t}: \text{T} \)：

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

  1. 如果\( \text{t} = \text{x} \)，则\( e(\text{t}) = e(\text{x}) = \text{x} \)，可得\( \Gamma \vdash^I e(\text{t}): \text{T} \)使用的规则是T-VAR，有\( \text{x}: \text{T} \in \Gamma \)，进而可得\( \Gamma \vdash^E \text{t}: \text{T} \)。
  2. 如果\( \text{t} = \lambda \text{x}: \text{T}_1 \text{. } \text{t}_{11} \)，则\( e(\text{t}) = \lambda \text{x}: \text{T}_1 \text{. } e(\text{t}_{11}) \)，可得\( \Gamma \vdash^I e(\text{t}): \text{T} \)使用的规则是T-ABS，于是有\( \Gamma, \text{x}: \text{T}_1 \vdash^I e(\text{t}_{11}): \text{T} \)，根据归纳假设，可得\( \Gamma, \text{x}: \text{T}_1 \vdash^E \text{t}_{11}: \text{T} \)，进而根据T-ABS，可得\( \Gamma \vdash^E \text{t}: \text{T} \)。
  3. 如果\( \text{t} = \lambda \text{\_}: \text{T}_1 \text{. } \text{t}_{11} \)，则\( e(\text{t}) = \lambda \text{x}: \text{T}_1 \text{. } e(\text{t}_{11}) \)，这里\( \text{x} \)为没有出现在\( e(\text{t}_{11}) \)中的新变量，可得\( \Gamma \vdash^I e(\text{t}): \text{T} \)使用的规则是T-ABS，于是有\( \Gamma, \text{x}: \text{T}_1 \vdash^I e(\text{t}_{11}): \text{T} \)，根据归纳假设，可得\( \Gamma, \text{x}: \text{T}_1 \vdash^E \text{t}_{11}: \text{T} \)，进而根据T-ABS，可得\( \Gamma \vdash^E \text{t}: \text{T} \)。
  4. 如果\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)，则\( e(\text{t}) = e(\text{t}_1) \text{ } e(\text{t}_2) \)，可得\( \Gamma \vdash^I e(\text{t}): \text{T} \)使用的规则是T-APP，于是有\( \Gamma \vdash^I e(\text{t}_1): \text{T}_1 \to \text{T}, \Gamma \vdash^I e(\text{t}_2): \text{T}_1 \)，根据归纳假设，可得\( \Gamma \vdash^E \text{t}_1: \text{T}_1 \to \text{T}, \Gamma \vdash^E \text{t}_2: \text{T}_1 \)，进而根据T-APP，可得\( \Gamma \vdash^E \text{t}: \text{T} \)。

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

证明第3点完毕。

章节11.4

练习11.4.1

题目：

  1. Show how to formulate ascription as a derived form. Prove that the “official” typing and evaluation rules given here correspond to your definition in a suitable sense.
  2. Suppose that, instead of the pair of evaluation rules E-ASCRIBE and E-ASCRIBE1, we had given an “eager” rule \[ \text{t}_1 \text{ as } \text{T} \to \text{t}_1 \quad (\text{E-ASCRIBEEAGER}) \] that throws away an ascription as soon as it is reached. Can ascription still be considered as a derived form?

解答：

解答1：

容易想到使用\( \lambda \)-抽象，让它的参数类型为ascription中写明的类型，这样就可以通过T-APP来检验类型是否真的正确了，具体的，我们递归定义ascription的elaboration函数\( e \)， \( \forall \)拓展项\( \text{t} \)，按如下规则定义\( e(\text{t}) \)：

  1. 如果\( \text{t} = \text{t}_1 \text{ as } \text{T} \)，则令\( e(\text{t}) = (\lambda \text{x}: \text{T} \text{. } \text{x}) \text{ } e(\text{t}_1) \)，这里\( \lambda \)-抽象的变量名可以随便取，我们取了\( \text{x} \)。
  2. 如果\( \text{t} = \lambda \text{x}: \text{T}_1 \text{. } \text{t}_{11} \)，则令\( e(\text{t}) = \lambda \text{x}: \text{T}_1 \text{. } e(\text{t}_{11}) \)。
  3. 如果\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)，则令\( e(\text{t}) = e(\text{t}_1) \text{ } e(\text{t}_2) \)。
  4. 如果\( \text{t} = \text{x} \)，则\( e(\text{t}) = \text{x} \)。

注意到，由于我们使用的是call-by-value的求值策略，因此在把\( \text{t} = \text{t}_1 \text{ as } \text{T} \)翻译成 \( e(\text{t}) = (\lambda \text{x}: \text{T} \text{. } \text{x}) \text{ } e(\text{t}_1) \)后，我们是先将\( e(\text{t}_1) \)多步求值成值，最后才使用E-APPABS消耗掉左侧的\( \lambda \text{x}: \text{T} \text{. } \text{x} \)，此时ascription中写明的类型\( \text{T} \)才消失，简而言之，翻译后的项，\( \text{T} \)是保留到最后才消耗掉的，这和E-ASCRIBE1一直保留\( \text{as } \text{T} \)，直到\( \text{t}_1 \)求值成值，最后才用E-ASCRIBE消耗掉\( \text{as } \text{T} \)是一致的。等下在对2的解答中我们会看到，如果去掉求值规则E-ASCRIBE、E-ASCRIBE1，增加求值规则E-ASCRIBEEAGER，则\( \text{as } \text{T} \)会被立刻消耗掉，为了保持一致，我们的elaboration函数\( e \)也得保证\( \text{T} \)被立刻消耗掉，此时上面的翻译策略就不能再用了，得修改下，这个问题在2的解答中再继续讨论。

下面，我们证明上述派生形式是合法的，即\( \forall \)拓展项\( \text{t} \)：

  1. 如果\( \text{t} \rightarrow_E \text{t}' \)，则\( e(\text{t}) \rightarrow_I e(\text{t}') \)。
  2. 如果\( e(\text{t}) \rightarrow_I \text{u} \)，则\( \exists \text{t}', e(\text{t}') = \text{u}, \text{t} \rightarrow_E \text{t}' \)。
  3. \( \Gamma \vdash_E \text{t}: \text{T} \)当且即当\( \Gamma \vdash_I e(\text{t}): \text{T} \)。

同练习11.3.2，我们得先证明一些引理：

引理1：

\( \forall \)变量名\( \text{x} \)，\( \forall \)拓展项中的值\( \text{v} \)，\( \forall \)拓展项\( \text{t} \)，我们有\( e([\text{x} \mapsto \text{v}]\text{t}) = [\text{x} \mapsto e(\text{v})]e(\text{t}) \)。

证明引理1：

用结构归纳法，对\( \text{t} \)的形式进行分情况讨论，很容易证明，这里省略。

证明引理1完毕。

引理2：

\( \forall \)拓展项中的值\( \text{v} \)，有\( e(\text{v}) \)仍为值。

证明引理2：

通过\( e \)函数的定义可直接发现引理2成立。

证明引理2完毕。

引理3：

\( \forall \)拓展项中的非值\( \text{t} \)，有\( e(\text{t}) \)仍不为值。

证明引理3：

通过\( e \)函数的定义可直接发现引理3成立。

证明引理3完毕。

证明第1点：

\( \forall \)拓展项\( \text{t} \)，归纳假设命题对\( \text{t} \)的直接子项成立，我们证明命题对\( \text{t} \)成立，对\( \text{t} \rightarrow_E \text{t}' \)使用的规则进行分情况讨论：

  1. 如果\( \text{t} \rightarrow_E \text{t}' \)使用的规则是E-APP1，则\( \text{t} = \text{t}_1 \text{ } \text{t}_2, \text{t}' = \text{t}'_1 \text{ } \text{t}_2, \text{t}_1 \rightarrow_E \text{t}'_1 \)，于是有\( e(\text{t}) = e(\text{t}_1) \text{ } e(\text{t}_2), e(\text{t}') = e(\text{t}'_1) \text{ } e(\text{t}_2) \)，进而根据\( \text{t}_1 \rightarrow_E \text{t}'_1 \)以及归纳假设，可得\( e(\text{t}_1) \rightarrow_I e(\text{t}'_1) \)，再使用规则E-APP可得，\( e(\text{t}) \rightarrow_I e(\text{t}') \)。
  2. 如果\( \text{t} \rightarrow_E \text{t}' \)使用的规则是E-APP2，则\( \text{t} = \text{v}_1 \text{ } \text{t}_2, \text{t}' = \text{v}_1 \text{ } \text{t}'_2, \text{t}_2 \rightarrow_E \text{t}'_2 \)，于是有\( e(\text{t}) = e(\text{v}_1) \text{ } e(\text{t}_2), e(\text{t}') = e(\text{v}_1) \text{ } e(\text{t}'_2) \)，进而根据\( \text{t}_2 \rightarrow_E \text{t}'_2 \)以及归纳假设，可得\( e(\text{t}_2) \rightarrow_I e(\text{t}'_2) \)，再使用规则E-APP2可得，\( e(\text{t}) \rightarrow_I e(\text{t}') \)。
  3. 如果\( \text{t} \rightarrow_E \text{t}' \)使用的规则是E-APPABS，则\( \text{t} = (\lambda \text{x}: \text{T}_1 \text{. } \text{t}_{11}) \text{ } \text{v}_2, \text{t}' = [\text{x} \mapsto \text{v}_2]\text{t}_{11} \)，于是有\( e(\text{t}) = e(\lambda \text{x}: \text{T}_1 \text{. } \text{t}_{11}) \text{ } e(\text{v}_2) = (\lambda \text{x}: \text{T}_1 \text{. } e(\text{t}_{11})) \text{ } e(\text{v}_2), e(\text{t}') = e([\text{x} \mapsto \text{v}_2]\text{t}_{11}) \)，通过E-APPABS，可得\( e(\text{t}) \rightarrow_I [\text{x} \mapsto e(\text{v}_2)]e(\text{t}_{11}) \)，根据引理1，可得\( [\text{x} \mapsto e(\text{v}_2)]e(\text{t}_{11}) = e(\text{t}') \)，于是有\( e(\text{t}) \rightarrow_I e(\text{t}') \)。
  4. 如果\( \text{t} \rightarrow_E \text{t}' \)使用的规则是E-ASCRIBE1，则\( \text{t} = \text{t}_1 \text{ as } \text{T}, \text{t}' = \text{t}'_1 \text{ as } \text{T}, \text{t}_1 \rightarrow_E \text{t}'_1 \)，于是有\( e(\text{t}) = e(\text{t}_1 \text{ as } \text{T}) = (\lambda \text{x}: \text{T} \text{. } \text{x}) \text{ } e(\text{t}_1), e(\text{t}') = e(\text{t}'_1 \text{ as } \text{T}) = (\lambda \text{x}: \text{T} \text{. } \text{x}) \text{ } e(\text{t}'_1) \)，进而根据\( \text{t}_1 \rightarrow_E \text{t}'_1 \)以及归纳假设，可得\( e(\text{t}_1) \rightarrow_I e(\text{t}'_1) \)，再使用规则E-APP2，可得\( e(\text{t}) \rightarrow^I e(\text{t}') \)。
  5. 如果\( \text{t} \rightarrow_E \text{t}' \)使用的规则是E-ASCRIBE，则\( \text{t} = \text{v}_1 \text{ as } \text{T}, \text{t}' = \text{v}_1 \)，于是有\( e(\text{t}) = (\lambda \text{x}: \text{T} \text{. } \text{x}) \text{ } e(\text{v}_1), e(\text{t}') = e(\text{v}_1) \)，根据引理2，可得\( e(\text{v}_1) \)仍然是值，于是可用规则E-APPABS得到\( e(\text{t}) \rightarrow^I e(\text{t}') \)。

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

证明第1点完毕。

证明第2点：

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

  1. 如果\( \text{t} = \text{x} \)，则\( e(\text{t}) = \text{x} \)为范式，这和\( e(\text{t}) \rightarrow_I \text{u} \)矛盾，因此这种情况不可能。
  2. 如果\( \text{t} = \lambda \text{x}: \text{T}_1 \text{. } \text{t}_{11} \)，则\( e(\text{t}) = \lambda \text{x}: \text{T}_1 \text{. } e(\text{t}_{11}) \)为范式，这和\( e(\text{t}) \rightarrow_I \text{u} \)矛盾，因此这种情况不可能。
  3. 如果\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)：
    1. 如果\( \text{t}_1 \)为值，则\( \text{t}_1 = \lambda \text{x}: \text{T}_1 \text{. } \text{t}_{11} \)：
      1. 如果\( \text{t}_2 \)为值，则令\( \text{v}_2 = \text{t}_2 \)，有\( e(\text{t}) = e(\lambda \text{x}: \text{T}_1 \text{. } \text{t}_{11}) \text{ } e(\text{v}_2) = (\lambda \text{x}: \text{T}_1 \text{. } e(\text{t}_{11})) \text{ } e(\text{v}_2) \)，根据引理2，可得\( e(\text{v}_2) \)仍然为值，进而可得\( e(\text{t}) \rightarrow_I \text{u} \)使用的规则是E-APPABS，有\( \text{u} = [\text{x} \mapsto e(\text{v}_2)]e(\text{t}_{11}) \)，进而根据引理1，可得\( \text{u} = [\text{x} \mapsto e(\text{v}_2)]e(\text{t}_{11}) = e([\text{x} \mapsto \text{v}_2]\text{t}_{11}) \)，令\( \text{t}' = [\text{x} \mapsto \text{v}_2]\text{t}_{11} \)，有\( e(\text{t}') = \text{u} \)，同时根据E-APPABS，有\( \text{t} \rightarrow_E \text{t}' \)。
      2. 如果\( \text{t}_2 \)不为值，则\( e(\text{t}) = e(\lambda \text{x}: \text{T}_1 \text{. } \text{t}_{11}) \text{ } e(\text{t}_2) = (\lambda \text{x}: \text{T}_1 \text{. } e(\text{t}_{11})) \text{ } e(\text{t}_2) \)，根据引理3，可得\( e(\text{t}_2) \)仍然不为值，进而可得\( e(\text{t}) \rightarrow_I \text{u} \)使用的规则是E-APP2，有\( e(\text{t}_2) \rightarrow_I \text{u}_2, \text{u} = (\lambda \text{x}: \text{T}_1 \text{. } e(\text{t}_{11})) \text{ } \text{u}_2 \)，根据\( e(\text{t}_2) \rightarrow_I \text{u}_2 \)以及归纳假设，可得\( \exists \text{t}'_2, e(\text{t}'_2) = \text{u}_2, \text{t}_2 \rightarrow_E \text{t}'_2 \)，令\( \text{t}' = (\lambda \text{x}: \text{T}_1 \text{. } \text{t}_{11}) \text{ } \text{t}'_2 \)，则可得\( e(\text{t}') = \text{u} \)，且根据\( \text{t}_2 \rightarrow_E \text{t}'_2 \)以及E-APP2，可得\( \text{t} \rightarrow_E \text{t}' \)。
    2. 如果\( \text{t}_1 \)不为值，则\( e(\text{t}) = e(\text{t}_1) \text{ } e(\text{t}_2) \)，根据引理3，可得\( e(\text{t}_1) \)仍然不为值，进而可得\( e(\text{t}) \rightarrow_I \text{u} \)使用的规则是E-APP1，有\( e(\text{t}_1) \rightarrow_I \text{u}_1, \text{u} = \text{u}_1 \text{ } e(\text{t}_2) \)，根据\( e(\text{t}_1) \rightarrow_I \text{u}_1 \)以及归纳假设，可得\( \exists \text{t}'_1, e(\text{t}'_1) = \text{u}_1, \text{t}_1 \rightarrow_E \text{t}'_1 \)，令\( \text{t}' = \text{t}'_1 \text{ } \text{t}_2 \)，则可得\( e(\text{t}') = \text{u} \)，且根据\( \text{t}_1 \rightarrow_E \text{t}'_1 \)以及E-APP1，可得\( \text{t} \rightarrow_E \text{t}' \)。
  4. 如果\( \text{t} = \text{t}_1 \text{ as } \text{T} \)：
    1. 如果\( \text{t}_1 \)为值，则令\( \text{v}_1 = \text{t}_1 \)，有\( e(\text{t}) = (\lambda \text{x}: \text{T} \text{. } \text{x}) \text{ } e(\text{v}_1) \)，根据引理2，可得\( e(\text{v}_1) \)仍然为值，进而可得\( e(\text{t}) \rightarrow_I \text{u} \)使用的规则是E-APPABS，有\( \text{u} = [\text{x} \mapsto e(\text{v}_1)]\text{x} = e(\text{v}_1) \)，令\( \text{t}' = \text{v}_1 \)，则\( e(\text{t}') = \text{u} \)，同时根据E-ASCRIBE，有\( \text{t} \rightarrow_E \text{t}' \)。
    2. 如果\( \text{t}_1 \)不为值，则\( e(\text{t}) = (\lambda \text{x}: \text{T} \text{. } \text{x}) \text{ } e(\text{t}_1) \)，根据引理3，可得\( e(\text{t}_1) \)仍然不为值，进而可得\( e(\text{t}) \rightarrow_I \text{u} \)使用的规则是E-APP2，有\( e(\text{t}_1) \rightarrow_I \text{u}_1, \text{u} = (\lambda \text{x}: \text{T} \text{. } \text{x}) \text{ } \text{u}_1 \)，根据\( e(\text{t}_1) \rightarrow_I \text{u}_1 \)以及归纳假设，可得\( \exists \text{t}'_1, e(\text{t}'_1) = \text{u}_1, \text{t}_1 \rightarrow_E \text{t}'_1 \)，令\( \text{t}' = \text{t}'_1 \text{ as } \text{T} \)，则可得\( e(\text{t}') = \text{u} \)，且根据\( \text{t}_1 \rightarrow_E \text{t}'_1 \)以及E-ASCRIBE1，可得\( \text{t} \rightarrow_E \text{t}' \)。

证明第2点完毕。

证明第3点：

充分性：

如果\( \Gamma \vdash_E \text{t}: \text{T} \)，我们要证明\( \Gamma \vdash_I e(\text{t}): \text{T} \)：

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

  1. 如果\( \text{t} = \text{x} \)，则\( \Gamma \vdash_E \text{t}: \text{T} \)使用的规则是T-VAR，有\( \text{x}: \text{T} \in \Gamma \)，可得\( e(\text{t}) = e(\text{x}) = \text{x} \in \Gamma \)，进而可得\( \Gamma \vdash_I e(\text{t}): \text{T} \)。
  2. 如果\( \text{t} = \lambda \text{x}: \text{T}_1 \text{. } \text{t}_{11} \)，则\( e(\text{t}) = \lambda \text{x}: \text{T}_1 \text{. } e(\text{t}_{11}) \)，可得\( \Gamma \vdash_E \text{t}: \text{T} \)使用的规则是T-ABS，于是有\( \Gamma, \text{x}: \text{T}_1 \vdash_E \text{t}_{11}: \text{T} \)，根据归纳假设，可得\( \Gamma, \text{x}: \text{T}_1 \vdash_I e(\text{t}_{11}): \text{T} \)，进而根据T-ABS，可得\( \Gamma \vdash_I e(\text{t}): \text{T} \)。
  3. 如果\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)，则\( e(\text{t}) = e(\text{t}_1) \text{ } e(\text{t}_2) \)，可得\( \Gamma \vdash_E \text{t}: \text{T} \)使用的规则是T-APP，于是有\( \Gamma \vdash_E \text{t}_1: \text{T}_1 \to \text{T}, \Gamma \vdash_E \text{t}_2: \text{T}_1 \)，根据归纳假设，可得\( \Gamma \vdash_I e(\text{t}_1): \text{T}_1 \to \text{T}, \Gamma \vdash_I e(\text{t}_2): \text{T}_1 \)，进而根据T-APP，可得\( \Gamma \vdash_I e(\text{t}): \text{T} \)。
  4. 如果\( \text{t} = \text{t}_1 \text{ as } \text{T}_1 \)，则\( e(\text{t}) = (\lambda \text{x}: \text{T}_1 \text{. } \text{x}) \text{ } e(\text{t}_1) \)，可得\( \Gamma \vdash_E \text{t}: \text{T} \)使用的规则是T-ASCRIBE，于是有\( \Gamma \vdash_E \text{t}_1: \text{T}_1, \text{T} = \text{T}_1 \)，根据归纳假设，可得\( \Gamma \vdash_I e(\text{t}_1): \text{T}_1 \)，易得\( \Gamma \vdash_I (\lambda \text{x}: \text{T}_1 \text{. } \text{x}): \text{T}_1 \to \text{T}_1 \)，进而根据T-APP，可得\( \Gamma \vdash_I e(\text{t}): \text{T}_1 \)，加上\( \text{T} = \text{T}_1 \)，可得\( \Gamma \vdash_I e(\text{t}): \text{T} \)。

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

必要性：

如果\( \Gamma \vdash_I e(\text{t}): \text{T} \)，我们要证明\( \Gamma \vdash_E \text{t}: \text{T} \)：

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

  1. 如果\( \text{t} = \text{x} \)，则\( e(\text{t}) = e(\text{x}) = \text{x} \)，可得\( \Gamma \vdash_I e(\text{t}): \text{T} \)使用的规则是T-VAR，有\( \text{x}: \text{T} \in \Gamma \)，进而可得\( \Gamma \vdash_E \text{t}: \text{T} \)。
  2. 如果\( \text{t} = \lambda \text{x}: \text{T}_1 \text{. } \text{t}_{11} \)，则\( e(\text{t}) = \lambda \text{x}: \text{T}_1 \text{. } e(\text{t}_{11}) \)，可得\( \Gamma \vdash_I e(\text{t}): \text{T} \)使用的规则是T-ABS，于是有\( \Gamma, \text{x}: \text{T}_1 \vdash_I e(\text{t}_{11}): \text{T} \)，根据归纳假设，可得\( \Gamma, \text{x}: \text{T}_1 \vdash_E \text{t}_{11}: \text{T} \)，进而根据T-ABS，可得\( \Gamma \vdash_E \text{t}: \text{T} \)。
  3. 如果\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)，则\( e(\text{t}) = e(\text{t}_1) \text{ } e(\text{t}_2) \)，可得\( \Gamma \vdash_I e(\text{t}): \text{T} \)使用的规则是T-APP，于是有\( \Gamma \vdash_I e(\text{t}_1): \text{T}_1 \to \text{T}, \Gamma \vdash_I e(\text{t}_2): \text{T}_1 \)，根据归纳假设，可得\( \Gamma \vdash_E \text{t}_1: \text{T}_1 \to \text{T}, \Gamma \vdash_E \text{t}_2: \text{T}_1 \)，进而根据T-APP，可得\( \Gamma \vdash_E \text{t}: \text{T} \)。
  4. 如果\( \text{t} = \text{t}_1 \text{ as } \text{T}_1 \)，则\( e(\text{t}) = (\lambda \text{x}: \text{T}_1 \text{. } \text{x}) \text{ } e(\text{t}_1) \)，可得\( \Gamma \vdash_I e(\text{t}): \text{T} \)使用的规则是T-APP，加上易得的\( \Gamma \vdash_I (\lambda \text{x}: \text{T}_1 \text{. } \text{x}): \text{T}_1 \to \text{T}_1 \)，可得\( \Gamma \vdash_I e(\text{t}_1): \text{T}_1, \text{T} = \text{T}_1 \)，根据归纳假设，可得\( \Gamma \vdash_E \text{t}_1: \text{T}_1 \)，进而根据T-ASCRIBE，可得\( \Gamma \vdash_E \text{t}: \text{T}_1 \)，加上\( \text{T} = \text{T}_1 \)，可得\( \Gamma \vdash_E \text{t}: \text{T} \)。

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

证明第3点完毕。

解答2：

前面说了，如果去掉求值规则E-ASCRIBE、E-ASCRIBE1，增加求值规则E-ASCRIBEEAGER，则\( \text{as } \text{T} \)会被立刻消耗掉，为了保持一致，我们的elaboration函数\( e \)也得保证\( \text{T} \)被立刻消耗掉，故不能再使用前面的翻译策略了，这里的问题在于之前把\( \text{t} = \text{t}_1 \text{ as } \text{T} \) 翻译成\( e(\text{t}) = (\lambda \text{x}: \text{T} \text{. } \text{x}) \text{ } e(\text{t}_1) \)，加上我们使用的是call-by-value的求值策略，因此我们会先将\( e(\text{t}_1) \)多步求值成值，最后才使用E-APPABS消耗掉\( \text{T} \)，而我们希望改成\( \text{T} \)被立刻消耗掉，为此，我们要延后\( e(\text{t}_1) \)的求值，优先消耗掉\( \text{T} \)，要实现这点，我们可以把\( e(\text{t}_1) \)保护在一个\( \lambda \)-抽象里面，具体的，我们递归定义ascription的elaboration函数\( e \)， \( \forall \)拓展项\( \text{t} \)，按如下规则定义\( e(\text{t}) \)：

  1. 如果\( \text{t} = \text{t}_1 \text{ as } \text{T} \)，则令\( e(\text{t}) = (\lambda \text{f}: \text{Unit} \to \text{T} \text{. } \text{f unit}) \text{ } (\lambda \text{x}: \text{Unit. } e(\text{t}_1)) \)，这里前一个\( \lambda \)-抽象的变量名可以随便取，我们取了\( \text{f} \)，后一个\( \lambda \)-抽象的变量名不能随便取，得取一个没有出现在\( e(\text{t}_1) \)中的新变量\( \text{x} \)，至于延后求值用的\( \lambda \)-抽象的参数类型\( \text{Unit} \)以及对应的值\( \text{unit} \)，则是不重要的，可以取其他的类型和值。
  2. 如果\( \text{t} = \lambda \text{x}: \text{T}_1 \text{. } \text{t}_{11} \)，则令\( e(\text{t}) = \lambda \text{x}: \text{T}_1 \text{. } e(\text{t}_{11}) \)。
  3. 如果\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)，则令\( e(\text{t}) = e(\text{t}_1) \text{ } e(\text{t}_2) \)。
  4. 如果\( \text{t} = \text{x} \)，则\( e(\text{t}) = \text{x} \)。

那么，如何说明上述修改后的派生形式是合法的呢？跟之前列出的3点一样吗？即\( \forall \)拓展项\( \text{t} \)：

  1. 如果\( \text{t} \rightarrow_E \text{t}' \)，则\( e(\text{t}) \rightarrow_I e(\text{t}') \)。
  2. 如果\( e(\text{t}) \rightarrow_I \text{u} \)，则\( \exists \text{t}', e(\text{t}') = \text{u}, \text{t} \rightarrow_E \text{t}' \)。
  3. \( \Gamma \vdash_E \text{t}: \text{T} \)当且即当\( \Gamma \vdash_I e(\text{t}): \text{T} \)。

容易看出第1点就不成立了，原本高层语言的项\( \text{t} \)单步就能求值得到的\( \text{t}' \)，翻译后的项\( e(\text{t}) \)却需要两步才能求值得到对应的\( e(\text{t}') \)，故第1点得修改下，放松下要求，变成：如果\( \text{t} \rightarrow_E \text{t}' \)，则\( e(\text{t}) \rightarrow^*_I e(\text{t}') \)。这种情况很常见，我们日常使用的编程语言，基本上一个表达式都会被翻译成多条底层的汇编代码或者机器码，进而底层需要多步求值才对应高层的单步求值。

同理，上述的第2点也不成立，给定一个拓展项\( \text{t} \)， \( e(\text{t}) \)需要两步求值才对应\( \text{t} \)的单步求值，故第2点也得修改下，变成：\( e(\text{t}) \rightarrow_I \text{u} \)，则\( \exists \text{t}', \text{t} \rightarrow_E \text{t}', \text{u} \rightarrow_I^* e(\text{t}') \)，即翻译后的项\( e(\text{t}) \)单步求值得到的\( \text{u} \)，能继续求值以得到\( \text{t} \)单步求值得到的\( \text{t}' \)对应的翻译项\( e(\text{t}') \)。

综上，对修改后派生形式的合法性描述改成：

  1. 如果\( \text{t} \rightarrow_E \text{t}' \)，则\( e(\text{t}) \rightarrow^*_I e(\text{t}') \)。
  2. 如果\( e(\text{t}) \rightarrow_I \text{u} \)，则\( \exists \text{t}', \text{t} \rightarrow_E \text{t}', \text{u} \rightarrow_I^* e(\text{t}') \)。
  3. \( \Gamma \vdash_E \text{t}: \text{T} \)当且即当\( \Gamma \vdash_I e(\text{t}): \text{T} \)。

章节11.5

练习11.5.1

题目：

The \( \text{letexercise} \) typechecker (available at the book’s web site) is an incomplete implementation of \( \text{let} \) expressions: basic parsing and printing functions are provided, but the clauses for \( \text{TmLet} \) are missing from the \( \text{eval1} \) and \( \text{typeof} \) functions (in their place, you’ll find dummy clauses that match everything and crash the program with an assertion failure). Finish it.

解答：

ML相关的内容一律跳过。

练习11.5.2

题目：

Another way of defining \( \text{let} \) as a derived form might be to desugar it by “executing” it immediately—i.e., to regard \( \text{let } \text{x} = \text{t}_1 \text{ in } \text{t}_2 \) as an abbreviation for the substituted body \( [\text{x} \mapsto \text{t}_1]\text{t}_2 \). Is this a good idea?

解答：

这个一看就不是好主意，几点问题：

  1. 如果\( \text{t}_2 \)中有多个自由变量\( \text{x} \)，则代入后的\( \text{t}_2 \)会包含多份\( \text{t}_1 \)，进而导致\( \text{t}_1 \)重复计算多次，如果语言没副作用还好，顶多效率低点，如果语言是有副作用的，则语义都错了。
  2. 翻译后的\( [\text{x} \mapsto \text{t}_1]\text{t}_2 \)的求值顺序和原始项\( \text{let } \text{x} = \text{t}_1 \text{ in } \text{t}_2 \)的求值顺序可能不同，后者会永远先求值\( \text{t}_1 \)，前者则不一定，取决于自由变量\( \text{x} \)的位置。
  3. 可能出现一个项在翻译前是非类型良好的，但是翻译后却变成类型良好的情况，比如\( \text{let } \text{x} = \text{true true} \text{ in } \text{true} \)，该项会被翻译成\( [\text{x} \mapsto \text{true true}]\text{true} = \text{true} \)，翻译后是类型良好的，但翻译前不是，这是因为\( \text{x} \)没有被用到，翻译应该保证非类型良好的项在翻译后仍然是非类型良好的项。

章节11.8

练习11.8.1

题目：

Write E-PROJRCD more explicitly, for comparison.

解答：

\( \dfrac{\exists 1 \leq j \leq n, \text{l} = \text{l}_j}{ \{ \text{l}_i = \text{v}_i \ ^{i \in 1 \dots n} \}.\text{l} \rightarrow \text{v}_j} \)

练习11.8.2

题目：

In our presentation of records, the projection operation is used to extract the fields of a record one at a time. Many high-level programming languages provide an alternative pattern matching syntax that extracts all the fields at the same time, allowing some programs to be expressed much more concisely. Patterns can also typically be nested, allowing parts to be extracted easily from complex nested data structures. We can add a simple form of pattern matching to an untyped lambda calculus with records by adding a new syntactic category of patterns, plus one new case (for the pattern matching construct itself) to the syntax of terms. (See Figure 11-8.)

/ox-hugo/types_and_programming_languages习题的参考解答及思考_第11章-figure_11_8.png The computation rule for pattern matching generalizes the let-binding rule from Figure 11-4. It relies on an auxiliary “matching” function that, given a pattern \( \text{p} \) and a value \( \text{v} \), either fails (indicating that \( \text{v} \) does not match \( \text{p} \)) or else yields a substitution that maps variables appearing in \( \text{p} \) to the corresponding parts of \( \text{v} \). For example, \( match(\{ \text{x}, \text{y} \}, \{ 5, \text{true} \}) \) yields the substitution \( [\text{x} \mapsto 5, \text{y} \mapsto \text{true}] \) and \( match(\text{x}, \{ 5, \text{true} \}) \) yields \( [\text{x} \mapsto \{5, \text{true} \}] \), while \( match(\{ \text{x} \}, \{ 5, \text{true} \}) \) fails. E-LETV uses \( match \) to calculate an appropriate substitution for the variables in \( \text{p} \).

The \( match \) function itself is defined by a separate set of inference rules. The rule M-VAR says that a variable pattern always succeeds, returning a substitution mapping the variable to the whole value being matched against. The rule M-RCD says that, to match a record pattern \( \{ \text{l}_i = \text{p}_i \ ^{i \in 1 \dots n} \} \) against a record value \( \{ \text{l}_i = \text{v}_i \ ^{i \in 1 \dots n} \} \) (of the same length, with the same labels), we individually match each sub-pattern \( \text{p}_i \) against the corresponding value \( \text{v}_i \) to obtain a substitution \( \sigma_i \), and build the final result substitution by composing all these substitutions. (We require that no variable should appear more than once in a pattern, so this composition of substitutions is just their union.)

Show how to add types to this system.

  1. Give typing rules for the new constructs (making any changes to the syntax you feel are necessary in the process).
  2. Sketch a proof of type preservation and progress for the whole calculus. (You do not need to show full proofs—just the statements of the required lemmas in the correct order.)

解答：

解答1：

首先，我们需要一个类似\( match \)的函数，不过它不解构（destructuring）值，而是解构类型，并把解构的结果以类型上下文的形式返回，我们将这个函数命名为\( matchtype \)，接收两个参数，第一个参数是模式\( \text{p} \)，第二个参数是待解构的类型\( \text{T} \)，举个例子，\( matchtype(\{ \text{foo} = \text{x}, \text{bar} = \text{y} \}, \{ \text{foo}: \text{Bool}, \text{bar}: \text{Nat} \}) \)应该返回类型上下文\( \Delta = \text{x}: \text{Bool}, \text{y}: \text{Nat} \)。

在定义函数\( matchtype \)之前，我们需要定义合并两个类型上下文的操作，给定两个类型上下文\( \Gamma_1 \)和\( \Gamma_2 \)，我们假定两个类型上下文绑定的变量是不相交的，即\( dom(\Gamma_1) \cap dom(\Gamma_2) = \empty \)，则我们定义\( \Gamma_1, \Gamma_2 \)为两个类型上下文合并后的类型上下文，具体的\( \forall \text{x} \in dom(\Gamma_1) \cup dom(\Gamma_2) \)，如果\( \text{x} \in dom(\Gamma_1) \)，则令\( (\Gamma_1, \Gamma_2)(\text{x}) = \Gamma_1(\text{x}) \)，否则令\( (\Gamma_1, \Gamma_2)(\text{x}) = \Gamma_2(\text{x}) \)。

OK，现在可以开始定义解构类型函数\( matchtype \)了，我们用\( \text{ud} \)（注：undefine的缩写）作为返回值来代表匹配失败， \( \forall \)模式\( \text{p} \)，\( \forall \)类型\( \text{T} \)，归纳假设所有大小比\( \text{T} \)小的类型\( \text{T}' \)，均有\( \forall \)模式\( \text{p}' \)，\( matchtype(\text{p}', \text{T}') \)已定义，则我们需要定义\( matchtype(\text{p}, \text{T}) \)：

  1. 如果\( \text{p} = \text{x} \)，即模式为单个变量，则我们令\( matchtype(\text{p}, \text{T}) = x: \text{T} \)，即单个变量作为模式时，永远能匹配成功，直接匹配整个类型。
  2. 如果\( \text{p} = \{ \text{l}_i = \text{p}_i \ ^{i \in 1 \dots n} \} \)：
    1. 如果\( \text{T} \)具有形式\( \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \) （注意，这里用了相同的符号\( \text{n}, \text{l}_i \)，因此要求\( \text{p} \)和\( \text{T} \)的\( n \)和所有标签\( \text{l}_i \)都要一样，可以描述得更严格点，但会比较长，这里就不这么干了），根据归纳假设，可得\( \forall 1 \leq i \leq n, matchtype(\text{p}_i, \text{T}_i) \)均已定义，于是\( \forall 1 \leq i \leq n \)，我们令\( \Delta_i = matchtype(\text{p}_i, \text{T}_i) \)：
      1. 如果\( \forall 1 \leq i \leq n, \Delta_i \neq \text{ud} \)，即任意一个子模式\( \text{p}_i \)都没有匹配失败，则我们令\( matchtype(\text{p}, \text{T}) = \Delta_1, \Delta_2, \dots, \Delta_n \) （注：这里我们假定模式中用到的变量名都不一样，进而\( \Delta_1, \Delta_2, \dots, \Delta_n \)是合法的）。
      2. 如果\( \exists 1 \leq i_0 \leq n, \Delta_{i_0} = \text{ud} \)，即存在匹配失败的子模式，则我们令\( matchtype(\text{p}, \text{T}) = \text{ud} \)。
    2. 如果\( \text{T} \)不具有形式\( \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n} \} \)，则我们直接令\( matchtype(\text{p}, \text{T}) = \text{ud} \)。

根据上面的定义，读者容易验证下面几个等式是正确的：

  1. \( matchtype(\{ \text{foo} = \text{x}, \text{bar} = \text{y} \}, \{ \text{foo}: \text{Bool}, \text{bar}: \text{Nat} \}) = \text{x}: \text{Bool}, \text{y}: \text{Nat} \)
  2. \( matchtype(\{ \text{foo} = \{ \text{foo1} = \text{x}, \text{foo2} = \text{y} \}, \text{bar} = \text{z} \}, \{ \text{foo}: \{ \text{foo1}: \text{Bool}, \text{foo2}: \text{Unit} \}, \text{bar}: \text{Nat} \}) = \text{x}: \text{Bool}, \text{y}: \text{Unit}, \text{z}: \text{Nat} \)
  3. \( matchtype(\{ \text{foo1} = \text{x}, \text{bar} = \text{y} \}, \{ \text{foo}: \text{Bool}, \text{bar}: \text{Nat} \}) = \text{ud} \)，这里是因为标签\( \text{foo1} \)不存在。
  4. \( matchtype(\{ \text{foo} = \text{x} \}, \{ \text{foo}: \text{Bool}, \text{bar}: \text{Nat} \}) = \text{ud} \)，这里是因为缺少标签\( \text{bar} \)对应的模式。
  5. \( matchtype(\{ \text{bar} = \text{x}, \text{foo} = \text{y} \}, \{ \text{foo}: \text{Bool}, \text{bar}: \text{Nat} \}) = \text{ud} \)，这里是因为子模式的顺序不对。

于是，给定一个项\( \text{let } \text{p} = \text{t}_1 \text{ in } \text{t}_2 \)且我们知道\( \Gamma \vdash \text{t}_1: \text{T}_1 \)的情况下，我们可以调用\( matchtype \)去解构模式\( \text{p} \)以及对应的类型\( \text{T}_1 \)，令\( \Delta = matchtype(\text{p}, \text{T}_1) \)，这里类型上下文\( \Delta \)就代表了解构后的结果，如果解构成功，即\( \Delta \neq \text{ud} \)，则我们用它去拓展当前类型上下文\( \Gamma \)，进而在该拓展后的上下文中去推导出\( \text{t}_2 \)的类型为\( \text{T}_2 \)，即\( \Gamma, \Delta \vdash \text{t}_2: \text{T}_2 \)，此时，我们就可以断言\( \Gamma \vdash \text{let } \text{p} = \text{t}_1 \text{ in } \text{t}_2: \text{T}_2 \)了。综上，我们定义模式匹配对应的类型规则T-LET如下：

\[ \dfrac{\Gamma \vdash \text{t}_1: \text{T}_1 \quad \Delta = matchtype(\text{p}, \text{T}_1) \text{ and } \Delta \neq \text{ud} \quad \Gamma, \Delta \vdash \text{t}_2: \text{T}_2}{ \Gamma \vdash \text{let } \text{p} = \text{t}_1 \text{ in } \text{t}_2: \text{T}_2} \qquad (\text{T-LET}) \]

书后面的参考解答中谈到一个值得考虑的拓展：允许模式中只使用部分标签且不限制标签顺序。如果要做到这点，则我们需要修改\( matchtype \)，我们称修改后的函数为\( matchtype' \)，如下：

\( \forall \)模式\( \text{p} \)，\( \forall \)类型\( \text{T} \)，归纳假设所有大小比\( \text{T} \)小的类型\( \text{T}' \)，均有\( \forall \)模式\( \text{p}' \)，\( matchtype'(\text{p}', \text{T}') \)已定义，则我们需要定义\( matchtype'(\text{p}, \text{T}) \)：

  1. 如果\( \text{p} = \text{x} \)，则我们令\( matchtype'(\text{p}, \text{T}) = x: \text{T} \)。
  2. 如果\( \text{p} = \{ \text{l}_i = \text{p}_i \ ^{i \in 1 \dots n_1} \} \)：
    1. 如果\( \text{T} \)具有形式\( \{ \text{k}_i: \text{T}_i \ ^{i \in 1 \dots n_2} \} \)，且\( \forall 1 \leq i \leq n_1, \exists 1 \leq j_i \leq n_2, \text{l}_i = \text{k}_{j_i} \)，根据归纳假设，可得\( \forall 1 \leq i \leq n_1, matchtype'(\text{p}_i, \text{T}_{j_i}) \)均已定义，于是\( \forall 1 \leq i \leq n_1 \)，我们令\( \Delta_i = matchtype'(\text{p}_i, \text{T}_{j_i}) \)：
      1. 如果\( \forall 1 \leq i \leq n_1, \Delta_i \neq \text{ud} \)，则我们令\( matchtype'(\text{p}, \text{T}) = \Delta_1, \Delta_2, \dots, \Delta_{n_1} \)。
      2. 如果\( \exists 1 \leq i_0 \leq n_1, \Delta_{i_0} = \text{ud} \)，则我们令\( matchtype'(\text{p}, \text{T}) = \text{ud} \)。
    2. 如果\( \text{T} \)不具有形式\( \{ \text{k}_i: \text{T}_i \ ^{i \in 1 \dots n_1} \} \)或者 \( \exists 1 \leq i_0 \leq n_1, \forall 1 \leq j \leq n_2, \text{l}_i \neq \text{k}_j \)，则我们直接令\( matchtype'(\text{p}, \text{T}) = \text{ud} \)。

容易验证如下等式是正确的：

\[ matchtype(\{ \text{bar} = \text{x}, \text{foo} = \text{y} \}, \{ \text{foo}: \text{Bool}, \text{bar}: \text{Nat}, \text{baz}: \text{Unit} \}) = \newline \text{x}: \text{Nat}, \text{y}: \text{Bool} \]

T-LET也得相应修改成调用\( matchtype' \)，得到新规则T-LET2，如下：

\[ \dfrac{\Gamma \vdash \text{t}_1: \text{T}_1 \quad \Delta = matchtype'(\text{p}, \text{T}_1) \text{ and } \Delta \neq \text{ud} \quad \Gamma, \Delta \vdash \text{t}_2: \text{T}_2}{ \Gamma \vdash \text{let } \text{p} = \text{t}_1 \text{ in } \text{t}_2: \text{T}_2} \qquad (\text{T-LET2}) \]

有了上述拓展后，投影操作\( \text{t}.\text{l} \)就可以很容易作为派生形式实现了，假设\( e \)为elaboration函数，则投影操作的翻译如下：

\[ e(\text{t}.\text{l}) = \text{let } \{ \text{l} = \text{x} \} = e(\text{t}) \text{ in } \text{x} \]

解答2：

PRESERVATION定理的证明方式和练习9.3.9类似，使用结构归纳法，对\( \text{t} \)的形式进行分情况讨论（或者对\( \text{t} \rightarrow \text{t}' \)使用的规则进行分情况讨论，进而根据使用的规则反推出\( \text{t} \)的形式），唯一需要注意的就是使用求值规则E-LETV的情况，我们需要表达“\( match(\text{p}, \text{v}) \)解构后各变量的绑定值具有正确的类型，这里正确的类型是指\( matchtype(\text{p}, \text{T}) \)中指定的类型”，严格表述如下：

引理1：

\( \forall \)上下文\( \Gamma \)，\( \forall \)值\( \text{v} \)，\( \forall \)模式\( \text{p} \)，如果\( \Gamma \vdash \text{v}: \text{T}, matchtype(\text{p}, \text{T}) = \Delta \neq \text{ud}, match(\text{p}, \text{v}) = \sigma \)，则\( dom(\Delta) = dom(\sigma) \)且\( \forall \text{x} \in dom(\Delta), \Gamma \vdash \sigma(\text{x}): \Delta(\text{x}) \)。

引理1完毕。

额外的，我们还需要表达“如果\( match(\text{p}, \text{v}) \)解构后得到复合代入函数\( \sigma \)，则代入后的结果\( \sigma(\text{t}) \)具有正确的类型”，严格表述如下：

引理2：

\( \forall \)上下文\( \Gamma \)，\( \forall \)项\( \text{t} \)， \( \forall \)值\( \text{v} \)，\( \forall \)模式\( \text{p} \)，如果\( \Gamma \vdash \text{v}: \text{T}, matchtype(\text{p}, \text{T}) = \Delta \neq \text{ud}, match(\text{p}, \text{v}) = \sigma \)，以及\( \Gamma, \Delta \vdash \text{t}: \text{T} \)，则我们有\( \Gamma \vdash \sigma(\text{t}): \text{T} \)。

引理2完毕。

注意，上面我们重载了\( \sigma(\dots) \)的用法，参数可以为变量或者项，为变量时代表该变量对应的代入值，为项时代表进行复合变量代入，举个例子，如果\( \sigma = [x \mapsto \lambda \text{x}: \text{Unit. } \text{x}][y \mapsto \text{unit}][z \mapsto \text{true}] \)，则\( \sigma(\text{x}) = \lambda \text{x}: \text{Unit. } \text{x} \)，而\( \sigma(\text{x y}) = [x \mapsto \lambda \text{x}: \text{Unit. } \text{x}]([y \mapsto \text{unit}](\text{x y})) = (\lambda \text{x}: \text{Unit. } \text{x}) \text{ } \text{unit} \)。不过注意到，当项\( \text{t} \)为变量时，两种解释是一致的，比如\( \text{t} = \text{x} \)，则\( \sigma(\text{t}) = \sigma(\text{x}) = \lambda \text{x}: \text{Unit. } \text{x} \)，同时，\( \sigma(\text{t}) = [x \mapsto \lambda \text{x}: \text{Unit. } \text{x}]\text{t} = [x \mapsto \lambda \text{x}: \text{Unit. } \text{x}]\text{x} = \lambda \text{x}: \text{Unit. } \text{x} \)。

至于PROGRESS定理的证明，则一样使用结构归纳法即可，对\( \text{t} \)的形式进行分情况讨论，唯一需要注意的就是\( \text{t} \)具有形式\( \text{let } \text{p} = \text{v}_1 \text{ in } \text{t}_2 \)的情况，我们需要引理保证在成功解构类型的情况下，值也应该可以成功解构，严格表述如下：

引理3：

\( \forall \)上下文\( \Gamma \)，\( \forall \)值\( \text{v} \)，\( \forall \)模式\( \text{p} \)，如果\( \Gamma \vdash \text{v}: \text{T}, matchtype(\text{p}, \text{T}) = \Delta \neq \text{ud} \)，则\( match(\text{p}, \text{v}) \)是有定义的。

引理3完毕。

章节11.9

练习11.9.1

题目：

Note the similarity between the typing rule for \( \text{case} \) and the rule for \( \text{if} \) in Figure 8-1: \( \text{if} \) can be regarded as a sort of degenerate form of \( \text{case} \) where no information is passed to the branches. Formalize this intuition by defining \( \text{true} \), \( \text{false} \), and \( \text{if} \) as derived forms using sums and \( \text{Unit} \).

解答：

既然要用和类型来模拟布尔类型，那么首先得考虑和类型\( \text{T}_1 + \text{T}_2 \)中的\( \text{T}_1, \text{T}_2 \)要取什么类型，这里由于我们目前是纯\( \lambda \)系统+基础类型\( \text{Unit} \)，因此可选的类型只有函数类型和\( \text{Unit} \)，这里选择比较简单的\( \text{Unit} \)，那还得选一个类型，选函数类型？还是可以两个类型都选\( \text{Unit} \)？如果两个类型都选\( \text{Unit} \)，那我们怎么区分\( \text{true, false} \)，想到我们会给项加上标签\( \text{inl, inr} \)，因此我们可以通过\( \text{inl, inr} \)来区分两个\( \text{Unit} \)类型，具体的，\( \text{inl unit} \)代表\( \text{true} \)，\( \text{inr unit} \)代表\( \text{false} \)，剩下的就简单了，假设\( e \)为elaboration函数，则完整定义如下：

  1. \( \text{Bool} = \text{Unit} + \text{Unit} \)
  2. \( e(\text{true}) = \text{inl unit} \)
  3. \( e(\text{false}) = \text{inr unit} \)
  4. \( e(\text{if } \text{t}_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3) = \text{case } e(\text{t}_1) \text{ of } \text{inl } \text{x}_2 \Rightarrow e(\text{t}_2) \mid \text{inr } \text{x}_3 \Rightarrow e(\text{t}_3) \)，这里\( \text{x}_2, \text{x}_3 \)分别为没有出现在\( e(\text{t}_{2}), e(\text{t}_3) \)中的新变量。

章节11.11

练习11.11.1

题目：

Define \( \text{equal} \), \( \text{plus} \), \( \text{times} \), and \( \text{factorial} \) using \( \text{fix} \).

解答：

使用\( \text{fix} \)定义\( \text{equal} \)：

\[ \begin{aligned} \text{equal} = \text{fix } (&\lambda \text{f}: \text{Nat} \to \text{Nat} \to \text{Bool} \text{. } \\ &\quad \lambda \text{m}: \text{Nat. } \lambda \text{n}: \text{Nat. } \\ &\quad \quad \text{if } (\text{iszero } \text{m}) \text{ then } (\text{iszero } \text{n}) \\ &\quad \quad \text{else } (\text{if } (\text{iszero } \text{n}) \text{ then } \text{false} \\ &\quad \quad \text{else } (\text{f } (\text{pred } \text{m}) \text{ } (\text{pred } \text{n})))) \end{aligned} \]

使用\( \text{fix} \)定义\( \text{plus} \)：

\[ \begin{aligned} \text{plus} = \text{fix } (&\lambda \text{f}: \text{Nat} \to \text{Nat} \to \text{Nat} \text{. } \\ &\quad \lambda \text{m}: \text{Nat. } \lambda \text{n}: \text{Nat. } \\ &\quad \quad \text{if } (\text{iszero } \text{m}) \text{ then } \text{n} \\ &\quad \quad \text{else } (\text{f } (\text{pred } \text{m}) \text{ } (\text{succ } \text{n}))) \end{aligned} \]

使用\( \text{fix} \)定义\( \text{times} \)：

该定义用到了上面\( \text{plus} \)的定义。

\[ \begin{aligned} \text{times} = \text{fix } (&\lambda \text{f}: \text{Nat} \to \text{Nat} \to \text{Nat} \text{. } \\ &\quad \lambda \text{m}: \text{Nat. } \lambda \text{n}: \text{Nat. } \\ &\quad \quad \text{if } (\text{iszero } \text{m}) \text{ then } 0 \\ &\quad \quad \text{else } (\text{plus } \text{n } (\text{f } (\text{pred } \text{m}) \text{ } \text{n}))) \end{aligned} \]

使用\( \text{fix} \)定义\( \text{factorial} \)：

该定义用到了上面\( \text{times} \)的定义。

\[ \begin{aligned} \text{factorial} = \text{fix } (&\lambda \text{f}: \text{Nat} \to \text{Nat} \text{. } \\ &\quad \lambda \text{n}: \text{Nat. } \\ &\quad \quad \text{if } (\text{iszero } \text{n}) \text{ then } 1 \\ &\quad \quad \text{else } (\text{times } \text{n } (\text{f } (\text{pred } \text{n})))) \end{aligned} \]

练习11.11.2

题目：

Rewrite your definitions of \( \text{plus} \), \( \text{times} \), and \( \text{factorial} \) from Exercise 11.11.1 using \( \text{letrec} \) instead of \( \text{fix} \).

使用\( \text{letrec} \)定义\( \text{plus} \)：

\[ \begin{aligned} \text{plus} =\ &\text{letrec } \text{plus}: \text{Nat} \to \text{Nat} \to \text{Nat} = \\ &\quad \lambda \text{m}: \text{Nat. } \lambda \text{n}: \text{Nat. } \\ &\quad \quad \text{if } (\text{iszero } \text{m}) \text{ then } \text{n} \\ &\quad \quad \text{else } (\text{plus } (\text{pred } \text{m}) \text{ } (\text{succ } \text{n})) \\ &\text{in } \text{plus} \end{aligned} \]

使用\( \text{letrec} \)定义\( \text{times} \)：

该定义用到了上面\( \text{plus} \)的定义。

\[ \begin{aligned} \text{times} =\ &\text{letrec } \lambda \text{times}: \text{Nat} \to \text{Nat} \to \text{Nat} = \\ &\quad \lambda \text{m}: \text{Nat. } \lambda \text{n}: \text{Nat. } \\ &\quad \quad \text{if } (\text{iszero } \text{m}) \text{ then } 0 \\ &\quad \quad \text{else } (\text{plus } \text{n } (\text{times } (\text{pred } \text{m}) \text{ } \text{n})) \\ &\text{in } \text{times} \end{aligned} \]

使用\( \text{letrec} \)定义\( \text{factorial} \)：

该定义用到了上面\( \text{times} \)的定义。

\[ \begin{aligned} \text{factorial} =\ &\text{letrec } \lambda \text{factorial}: \text{Nat} \to \text{Nat} = \\ &\quad \lambda \text{n}: \text{Nat. } \\ &\quad \quad \text{if } (\text{iszero } \text{n}) \text{ then } 1 \\ &\quad \quad \text{else } (\text{times } \text{n } (\text{factorial } (\text{pred } \text{n}))) \\ &\text{in } \text{factorial} \end{aligned} \]

章节11.12

练习11.12.1

题目：

Verify that the progress and preservation theorems hold for the simply typed lambda-calculus with booleans and lists.

解答：

首先，PROGRESS定理是不成立的，比如，\( \text{head}[\text{Bool}] \text{ } \text{nil}[\text{Bool}] \)以及 \( \text{tail}[\text{Bool}] \text{ } \text{nil}[\text{Bool}] \) 均是closed、类型良好的项，但是它们均既不是值，也不能进一步求值，违反了PROGRESS定理。有多种方法来处理这个问题，常见的如下：

  1. 给定这些情况特殊的求值结果，如令\( \text{head}[\text{Bool}] \text{ } \text{nil}[\text{Bool}] \rightarrow \text{nil}[\text{Bool}], \text{tail}[\text{Bool}] \text{ } \text{nil}[\text{Bool}] \rightarrow \text{nil}[\text{Bool}] \)，即空列表的头元素和尾列表均为空列表，但这种处理方式会迫使我们放弃类型的唯一性，要求\( \text{nil}[\text{Bool}] \)同时属于类型\( \text{Bool} \)以及类型\( \text{List Bool} \) （这是由T-HEAD、T-TAIL决定的），不过由于这里空列表只是其中一种特殊值，可以取其他的特殊值来代表fallback或者失败（具体语义上是否应视为失败得看情况），故我们可以分别为\( \text{head}[\text{Bool}] \text{ } \text{nil}[\text{Bool}], \text{tail}[\text{Bool}] \text{ } \text{nil}[\text{Bool}] \)选择不同的特殊值，以避免类型不唯一的问题。
  2. 遇到这些情况时抛出异常，或者使用和异常对应的机制，比如Common Lisp的condition系统。

PRESERVATION定理则仍然是成立的，在下面证明，证明中会显式或者隐式用到一些比较容易证明的引理（比如引理9.3.4拓展到列表的版本），由于证明比较简单，就省略了。

首先，为了处理E-APPABS的情况，得证明引理9.3.8成立。

证明引理9.3.8：

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

  1. 如果\( \text{t} = \text{y} \)：
    1. 如果\( \text{y} = \text{x} \)，则\( [\text{x} \mapsto \text{s}]\text{t} = [\text{x} \mapsto \text{s}]\text{x} = \text{s} \)，再由\( \Gamma \vdash \text{s}: \text{S} \)，可得\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}: \text{T} \)。
    2. 如果\( \text{y} \neq \text{x} \)，则\( [\text{x} \mapsto \text{s}]\text{t} = [\text{x} \mapsto \text{s}]\text{y} = \text{y} = \text{t} \)，再由\( \Gamma, \text{x}: \text{S} \vdash \text{t}: \text{T} \)，可得\( \Gamma, \text{x}: \text{S} \vdash [\text{x} \mapsto \text{s}]\text{t}: \text{T} \)，又\( \text{x} \)没有出现在\( \text{t} \)中，可得\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}: \text{T} \)。
  2. 如果\( \text{t} = \lambda \text{y}: \text{T}_1 \text{. } \text{t}_2 \)，则\( [\text{x} \mapsto \text{s}]\text{t} = [\text{x} \mapsto \text{s}](\lambda \text{y}: \text{T}_1 \text{. } \text{t}_2) = \lambda \text{y}: \text{T}_1 \text{. } [\text{x} \mapsto \text{s}]\text{t}_2 \)，由于此时\( \Gamma, \text{x}: \text{S} \vdash \text{t}: \text{T} \)使用的规则只能是T-ABS，可得\( \text{T} = \text{T}_1 \to \text{T}_2, \Gamma, \text{x}: \text{S}, \text{y}: \text{T}_1 \vdash \text{t}_2: \text{T}_2 \)，进而可得\( \Gamma, \text{y}: \text{T}_1, \text{x}: \text{S} \vdash \text{t}_2: \text{T}_2 \) (a) ，而由\( \Gamma \vdash \text{s}: \text{S} \)，可得\( \Gamma, \text{y}: \text{T}_1 \vdash \text{s}: \text{S} \)，进而由(a)以及归纳假设，可得\( \Gamma, \text{y}: \text{T}_1 \vdash [\text{x} \mapsto \text{s}]\text{t}_2: \text{T}_2 \)，进而由T-ABS，可得\( \Gamma \vdash \lambda \text{y}: \text{T}_1 \text{. } [\text{x} \mapsto \text{s}]\text{t}_2: \text{T}_1 \to \text{T}_2 \)，即\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}: \text{T} \)。
  3. 如果\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)，则\( [\text{x} \mapsto \text{s}]\text{t} = [\text{x} \mapsto \text{s}]\text{t}_1 \text{ } [\text{x} \mapsto \text{s}]\text{t}_2 \)，由于此时\( \Gamma, \text{x}: \text{S} \vdash \text{t}: \text{T} \)使用的规则只能是T-APP，可得\( \Gamma, \text{x}: \text{S} \vdash \text{t}_1: \text{T}_2 \to \text{T}, \Gamma, \text{x}: \text{S} \vdash \text{t}_2: \text{T}_2 \)，进一步由\( \Gamma \vdash \text{s}: \text{S} \)以及归纳假设，可得\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}_1: \text{T}_2 \to \text{T}, \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}_2: \text{T}_2 \)，进而由T-APP，可得\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}_1 \text{ } [\text{x} \mapsto \text{s}]\text{t}_2: \text{T} \)，即\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}: \text{T} \)。
  4. 如果\( \text{t} = \text{true, false}, \text{nil}[\text{T}_1] \)，则\( [\text{x} \mapsto \text{s}]\text{t} = \text{t} \)，再由\( \Gamma, \text{x}: \text{S} \vdash \text{t}: \text{T} \)，可得\( \Gamma, \text{x}: \text{S} \vdash [\text{x} \mapsto \text{s}]\text{t}: \text{T} \)，又\( \text{x} \)没有出现在\( \text{t} \)中，可得\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}: \text{T} \)。
  5. 如果\( \text{t} = \text{if } \text{t}_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3 \)，则\( [\text{x} \mapsto \text{s}]\text{t} = \text{if } [\text{x} \mapsto \text{s}]\text{t}_1 \text{ then } [\text{x} \mapsto \text{s}]\text{t}_2 \text{ else } [\text{x} \mapsto \text{s}]\text{t}_3 \)，由于此时\( \Gamma, \text{x}: \text{S} \vdash \text{t}: \text{T} \)使用的规则只能是T-IF，可得\( \Gamma, \text{x}: \text{S} \vdash \text{t}_1: \text{Bool}, \Gamma, \text{x}: \text{S} \vdash \text{t}_2: \text{T}, \Gamma, \text{x}: \text{S} \vdash \text{t}_3: \text{T} \)，进一步由\( \Gamma \vdash \text{s}: \text{S} \)以及归纳假设，可得\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}_1: \text{Bool}, \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}_2: \text{T}, \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}_3: \text{T} \)，进而由T-IF，可得\( \Gamma \vdash \text{if } [\text{x} \mapsto \text{s}]\text{t}_1 \text{ then } [\text{x} \mapsto \text{s}]\text{t}_2 \text{ else } [\text{x} \mapsto \text{s}]\text{t}_3: \text{T} \)，即\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}: \text{T} \)。
  6. 如果\( \text{t} = \text{cons}[\text{T}_1] \text{ } \text{t}_1 \text{ } \text{t}_2 \)，则\( [\text{x} \mapsto \text{s}]\text{t} = \text{cons}[\text{T}_1] \text{ } [\text{x} \mapsto \text{s}]\text{t}_1 \text{ } [\text{x} \mapsto \text{s}]\text{t}_2 \)，由于此时\( \Gamma, \text{x}: \text{S} \vdash \text{t}: \text{T} \)使用的规则只能是T-CONS，可得\( \text{T} = \text{List T}_1, \Gamma, \text{x}: \text{S} \vdash \text{t}_1: \text{T}_1, \Gamma, \text{x}: \text{S} \vdash \text{t}_2: \text{List T}_1 \)，进一步由\( \Gamma \vdash \text{s}: \text{S} \)以及归纳假设，可得\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}_1: \text{T}_1, \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}_2: \text{List T}_1 \)，进而由T-CONS，可得\( \Gamma \vdash \text{cons}[\text{T}_1] \text{ } [\text{x} \mapsto \text{s}]\text{t}_1 \text{ } [\text{x} \mapsto \text{s}]\text{t}_2: \text{List T}_1 \)，即\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}: \text{T} \)。
  7. 如果\( \text{t} = \text{head}[\text{T}_1] \text{ } \text{t}_1 \)，则\( [\text{x} \mapsto \text{s}]\text{t} = \text{head}[\text{T}_1] \text{ } [\text{x} \mapsto \text{s}]\text{t}_1 \)，由于此时\( \Gamma, \text{x}: \text{S} \vdash \text{t}: \text{T} \)使用的规则只能是T-HEAD，可得\( \text{T} = \text{T}_1, \Gamma, \text{x}: \text{S} \vdash \text{t}_1: \text{List T}_1 \)，进一步由\( \Gamma \vdash \text{s}: \text{S} \)以及归纳假设，可得\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}_1: \text{List T}_1 \)，进而由T-HEAD，可得\( \Gamma \vdash \text{head}[\text{T}_1] \text{ } [\text{x} \mapsto \text{s}]\text{t}_1 : \text{T}_1 \)，即\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}: \text{T} \)。
  8. 如果\( \text{t} = \text{tail}[\text{T}_1] \text{ } \text{t}_1 \)，则\( [\text{x} \mapsto \text{s}]\text{t} = \text{tail}[\text{T}_1] \text{ } [\text{x} \mapsto \text{s}]\text{t}_1 \)，由于此时\( \Gamma, \text{x}: \text{S} \vdash \text{t}: \text{T} \)使用的规则只能是T-TAIL，可得\( \text{T} = \text{List T}_1, \Gamma, \text{x}: \text{S} \vdash \text{t}_1: \text{List T}_1 \)，进一步由\( \Gamma \vdash \text{s}: \text{S} \)以及归纳假设，可得\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}_1: \text{List T}_1 \)，进而由T-TAIL，可得\( \Gamma \vdash \text{tail}[\text{T}_1] \text{ } [\text{x} \mapsto \text{s}]\text{t}_1 : \text{List T}_1 \)，即\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}: \text{T} \)。
  9. 如果\( \text{t} = \text{isnil}[\text{T}_1] \text{ } \text{t}_1 \)，则\( [\text{x} \mapsto \text{s}]\text{t} = \text{isnil}[\text{T}_1] \text{ } [\text{x} \mapsto \text{s}]\text{t}_1 \)，由于此时\( \Gamma, \text{x}: \text{S} \vdash \text{t}: \text{T} \)使用的规则只能是T-ISNIL，可得\( \text{T} = \text{Bool}, \Gamma, \text{x}: \text{S} \vdash \text{t}_1: \text{List T}_1 \)，进一步由\( \Gamma \vdash \text{s}: \text{S} \)以及归纳假设，可得\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}_1: \text{List T}_1 \)，进而由T-ISNIL，可得\( \Gamma \vdash \text{isnil}[\text{T}_1] \text{ } [\text{x} \mapsto \text{s}]\text{t}_1 : \text{Bool} \)，即\( \Gamma \vdash [\text{x} \mapsto \text{s}]\text{t}: \text{T} \)。

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

证明引理9.3.8完毕。

现在，可以去证明PRESERVATION定理了。

证明PRESERVATION定理：

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

  1. 如果\( \text{t} = \text{true, false, x}, \lambda \text{x}: \text{T}_1 \text{. } \text{t}_2, \text{nil}[\text{T}_1] \)，则\( \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 \)，则\( \Gamma \vdash \text{t}: \text{T} \)使用的规则只能是T-IF，可得\( \Gamma \vdash \text{t}_1: \text{Bool}, \Gamma \vdash \text{t}_2: \text{T}, \Gamma \vdash \text{t}_3: \text{T} \)：
    1. 如果\( \text{t} = \text{true} \)，则\( \text{t} \rightarrow \text{t}' \)使用的求值规则只能是E-IFTRUE，可得\( \text{t}' = \text{t}_2 \)，加上\( \Gamma \vdash \text{t}_2: \text{T} \)，有\( \Gamma \vdash \text{t}': \text{T} \)。
    2. 如果\( \text{t} = \text{false} \)，则\( \text{t} \rightarrow \text{t}' \)使用的求值规则只能是E-IFTRUE，可得\( \text{t}' = \text{t}_3 \)，加上\( \Gamma \vdash \text{t}_3: \text{T} \)，有\( \Gamma \vdash \text{t}': \text{T} \)。
    3. 如果\( \text{t} \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 \)，根据\( \Gamma \vdash \text{t}_1: \text{Bool}, \text{t}_1 \rightarrow \text{t}'_1 \)以及归纳假设，可得\( \Gamma \vdash \text{t}'_1: \text{Bool} \)，进而根据\( \Gamma \vdash \text{t}_2: \text{T}, \Gamma \vdash \text{t}_3: \text{T} \)以及T-IF，可得\( \Gamma \vdash \text{t}': \text{T} \)。
  3. 如果\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)，则\( \Gamma \vdash \text{t}: \text{T} \)使用的规则只能是T-APP，可得\( \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 \)，根据\( \Gamma \vdash \text{t}_1: \text{T}_2 \to \text{T}, \text{t}_1 \rightarrow \text{t}'_1 \)以及归纳假设，可得\( \Gamma \vdash \text{t}'_1: \text{T}_2 \to \text{T} \)，进而根据\( \Gamma \vdash \text{t}_2: \text{T}_2 \)以及T-APP，可得\( \Gamma \vdash \text{t}': \text{T} \)。
    2. 如果\( \text{t}_1 \)为值，此时根据\( \Gamma \vdash \text{t}_1: \text{T}_2 \to \text{T} \)以及引理9.3.4，可得\( \text{t}_1 = \lambda \text{x}: \text{T}_2: \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 \)，根据\( \Gamma \vdash \text{t}_1: \text{T}_2 \to \text{T}, \text{t}_2 \rightarrow \text{t}'_2 \)以及归纳假设，可得\( \Gamma \vdash \text{t}'_2: \text{T}_2 \)，进而根据\( \Gamma \vdash \text{t}_1: \text{T}_2 \to \text{T} \)以及T-APP，可得\( \Gamma \vdash \text{t}': \text{T} \)。
      2. 如果\( \text{t}_2 \)为值，则\( \text{t} \rightarrow \text{t}' \)使用的求值规则只能是E-APPABS，可得\( \text{t}' = [\text{x} \mapsto \text{t}_2]\text{t}_{11} \)，除此之外，\( \Gamma \vdash \text{t}_1: \text{T}_2 \to \text{T} \)使用的规则只能是T-ABS，可得\( \Gamma, \text{x}: \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} \)。
  4. 如果\( \text{t} = \text{cons}[\text{T}_1] \text{ } \text{t}_1 \text{ } \text{t}_2 \)，则\( \Gamma \vdash \text{t}: \text{T} \)使用的规则只能是T-CONS，可得\( \text{T} = \text{List T}_1, \Gamma \vdash \text{t}_1: \text{T}_1, \Gamma \vdash \text{t}_2: \text{List T}_1 \)：
    1. 如果\( \text{t}_1 \)不为值，则\( \text{t} \rightarrow \text{t}' \)使用的求值规则只能是E-CONS1，可得\( \text{t}_1 \rightarrow \text{t}'_1, \text{t}' = \text{cons}[\text{T}_1] \text{ } \text{t}'_1 \text{ } \text{t}_2 \)，根据\( \Gamma \vdash \text{t}_1: \text{T}_1, \text{t}_1 \rightarrow \text{t}'_1 \)以及归纳假设，可得\( \Gamma \vdash \text{t}'_1: \text{T}_1 \)，进而根据\( \Gamma \vdash \text{t}_2: \text{List T}_1 \)以及T-CONS，可得\( \Gamma \vdash \text{t}': \text{List T}_1 \)，即\( \Gamma \vdash \text{t}': \text{T} \)。
    2. 如果\( \text{t}_1 \)为值：
      1. 如果\( \text{t}_2 \)不为值，则\( \text{t} \rightarrow \text{t}' \)使用的求值规则只能是E-CONS2，可得\( \text{t}_2 \rightarrow \text{t}'_2, \text{t}' = \text{cons}[\text{T}_1] \text{ } \text{t}_1 \text{ } \text{t}'_2 \)，根据\( \Gamma \vdash \text{t}_2: \text{List T}_1, \text{t}_2 \rightarrow \text{t}'_2 \)以及归纳假设，可得\( \Gamma \vdash \text{t}'_2: \text{List T}_1 \)，进而根据\( \Gamma \vdash \text{t}_1: \text{T}_1 \)以及T-CONS，可得\( \Gamma \vdash \text{t}': \text{List T}_1 \)，即\( \Gamma \vdash \text{t}': \text{T} \)。
      2. 如果\( \text{t}_2 \)也为值，则\( \text{t} \)为范式，这和\( \text{t} \rightarrow \text{t}' \)矛盾。
  5. 如果\( \text{t} = \text{head}[\text{T}_1] \text{ } \text{t}_1 \)，则\( \Gamma \vdash \text{t}: \text{T} \)使用的规则只能是T-HEAD，可得\( \text{T} = \text{T}_1, \Gamma \vdash \text{t}_1: \text{List T}_1 \)：
    1. 如果\( \text{t}_1 \)不为值，则\( \text{t} \rightarrow \text{t}' \)使用的求值规则只能是E-HEAD，可得\( \text{t}_1 \rightarrow \text{t}'_1, \text{t}' = \text{head}[\text{T}_1] \text{ } \text{t}'_1 \)，根据\( \Gamma \vdash \text{t}_1: \text{List T}_1, \text{t}_1 \rightarrow \text{t}'_1 \)以及归纳假设，可得\( \Gamma \vdash \text{t}'_1: \text{List T}_1 \)，进而根据T-HEAD，可得\( \Gamma \vdash \text{t}': \text{T}_1 \)，即\( \Gamma \vdash \text{t}': \text{T} \)。
    2. 如果\( \text{t}_1 \)为值，则由引理9.3.4，可得\( \text{t}_1 = \text{nil}[\text{T}_1] \)或 \( \text{t}_1 = \text{cons}[\text{T}_1] \text{ } \text{v}_1 \text{ } \text{v}_2 \)：
      1. 如果\( \text{t}_1 = \text{nil}[\text{T}_1] \)，则\( \text{t} \)为范式，这和\( \text{t} \rightarrow \text{t}' \)矛盾。
      2. 如果\( \text{t}_1 = \text{cons}[\text{T}_1] \text{ } \text{v}_1 \text{ } \text{v}_2 \)，则\( \text{t} \rightarrow \text{t}' \)使用的求值规则只能是E-HEADCONS，可得\( \text{t}' = \text{v}_1 \)，除此之外， \( \Gamma \vdash \text{t}_1: \text{List T}_1 \)使用的规则只能是T-CONS，可得\( \Gamma \vdash \text{v}_1: \text{T}_1 \)，即\( \Gamma \vdash \text{t}': \text{T} \)。
  6. 如果\( \text{t} = \text{tail}[\text{T}_1] \text{ } \text{t}_1 \)，则\( \Gamma \vdash \text{t}: \text{T} \)使用的规则只能是T-TAIL，可得\( \text{T} = \text{List T}_1, \Gamma \vdash \text{t}_1: \text{List T}_1 \)：
    1. 如果\( \text{t}_1 \)不为值，则\( \text{t} \rightarrow \text{t}' \)使用的求值规则只能是E-TAIL，可得\( \text{t}_1 \rightarrow \text{t}'_1, \text{t}' = \text{tail}[\text{T}_1] \text{ } \text{t}'_1 \)，根据\( \Gamma \vdash \text{t}_1: \text{List T}_1, \text{t}_1 \rightarrow \text{t}'_1 \)以及归纳假设，可得\( \Gamma \vdash \text{t}'_1: \text{List T}_1 \)，进而根据T-TAIL，可得\( \Gamma \vdash \text{t}': \text{List T}_1 \)，即\( \Gamma \vdash \text{t}': \text{T} \)。
    2. 如果\( \text{t}_1 \)为值，则由引理9.3.4，可得\( \text{t}_1 = \text{nil}[\text{T}_1] \)或 \( \text{t}_1 = \text{cons}[\text{T}_1] \text{ } \text{v}_1 \text{ } \text{v}_2 \)：
      1. 如果\( \text{t}_1 = \text{nil}[\text{T}_1] \)，则\( \text{t} \)为范式，这和\( \text{t} \rightarrow \text{t}' \)矛盾。
      2. 如果\( \text{t}_1 = \text{cons}[\text{T}_1] \text{ } \text{v}_1 \text{ } \text{v}_2 \)，则\( \text{t} \rightarrow \text{t}' \)使用的求值规则只能是E-TAILCONS，可得\( \text{t}' = \text{v}_2 \)，除此之外， \( \Gamma \vdash \text{t}_1: \text{List T}_1 \)使用的规则只能是T-CONS，可得\( \Gamma \vdash \text{v}_2: \text{List T}_1 \)，即\( \Gamma \vdash \text{t}': \text{T} \)。
  7. 如果\( \text{t} = \text{isnil}[\text{T}_1] \text{ } \text{t}_1 \)，则\( \Gamma \vdash \text{t}: \text{T} \)使用的规则只能是T-ISNIL，可得\( \text{T} = \text{Bool}, \Gamma \vdash \text{t}_1: \text{List T}_1 \)：
    1. 如果\( \text{t}_1 \)不为值，则\( \text{t} \rightarrow \text{t}' \)使用的求值规则只能是E-ISNIL，可得\( \text{t}_1 \rightarrow \text{t}'_1, \text{t}' = \text{isnil}[\text{T}_1] \text{ } \text{t}'_1 \)，根据\( \Gamma \vdash \text{t}_1: \text{List T}_1, \text{t}_1 \rightarrow \text{t}'_1 \)以及归纳假设，可得\( \Gamma \vdash \text{t}'_1: \text{List T}_1 \)，进而根据T-ISNIL，可得\( \Gamma \vdash \text{t}': \text{T}_1 \)，即\( \Gamma \vdash \text{t}': \text{T} \)。
    2. 如果\( \text{t}_1 \)为值，则由引理9.3.4，可得\( \text{t}_1 = \text{nil}[\text{T}_1] \)或 \( \text{t}_1 = \text{cons}[\text{T}_1] \text{ } \text{v}_1 \text{ } \text{v}_2 \)：
      1. 如果\( \text{t}_1 = \text{nil}[\text{T}_1] \)，则\( \text{t} \rightarrow \text{t}' \)使用的求值规则只能是E-ISNILNIL，可得\( \text{t}' = \text{true} \)，进而根据T-TRUE，可得\( \Gamma \vdash \text{t}': \text{Bool} \)，即\( \Gamma \vdash \text{t}': \text{T} \)。
      2. 如果\( \text{t}_1 = \text{cons}[\text{T}_1] \text{ } \text{v}_1 \text{ } \text{v}_2 \)，则\( \text{t} \rightarrow \text{t}' \)使用的求值规则只能是E-ISNILCONS，可得\( \text{t}' = \text{false} \)，进而根据T-FALSE，可得\( \Gamma \vdash \text{t}': \text{Bool} \)，即\( \Gamma \vdash \text{t}': \text{T} \)。

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

证明PRESERVATION定理完毕。

练习11.12.2

题目：

The presentation of lists here includes many type annotations that are not really needed, in the sense that the typing rules can easily derive the annotations from context. Can all the type annotations be deleted?

解答：

举个例子，\( \text{t}_1 = \text{cons}[\text{Bool}] \text{ } \text{true} \text{ } \text{nil}[\text{Bool}] \)，这里由列表\( \text{t}_1 \)的头元素为类型是\( \text{Bool} \)的\( \text{true} \)、尾列表类型为\( \text{List Bool} \)，就可以推出\( \text{t}_1 \)的类型为\( \text{List Bool} \)了，不需要在\( \text{cons} \)本身加上类型标签\( [\text{Bool}] \)，可以简化成\( \text{t}_1 = \text{cons} \text{ } \text{true} \text{ } \text{nil}[\text{Bool}] \)，进一步的，\( \text{t}_2 = \text{cons} \text{ } \text{false} \text{ } \text{t}_1 \)，同理，这里由列表\( \text{t}_2 \)的头元素为类型是\( \text{Bool} \)的\( \text{false} \)、尾列表\( \text{t}_1 \)类型为\( \text{List Bool} \)（之前得到的），就可以推出\( \text{t}_2 \)的类型为\( \text{List Bool} \)了，也不需要在\( \text{cons} \)本身加上类型标签\( [\text{Bool}] \)，可以简化成\( \text{t}_1 = \text{cons} \text{ } \text{false} \text{ } \text{t}_1 = \text{cons} \text{ } \text{false} \text{ } (\text{cons} \text{ } \text{true} \text{ } \text{nil}[\text{Bool}]) \)。综上，T-CONS可以简化成如下：

\[ \dfrac{\Gamma \vdash \text{t}_1: \text{T}_1 \quad \Gamma \vdash \text{t}_2: \text{List T}_1}{ \Gamma \vdash \text{cons} \text{ } \text{t}_1 \text{ } \text{t}_2: \text{List T}_1} \]

求值规则、语法等也得对应修改，这里省略。

同理，T-HEAD、T-TAIL、T-ISNIL都可以对应省略\( \text{head}, \text{tail}, \text{isnil} \)的类型标签，求值规则、语法等同样对应修改。

但是\( \text{nil}[\text{T}_1] \)的类型标签不能去掉，否则，给定一个不带类型标签的\( \text{nil} \)，我们无法确定\( \text{nil} \)的类型，或者换个角度说，\( \forall \)类型\( \text{T}_1 \)，\( \text{nil} \)均具有类型\( \text{List T}_1 \)，这违反了类型的唯一性，当然，编译器可以设计算法利用上下文来进一步猜测\( \text{nil} \)的类型\( \text{List T}_1 \)中的\( \text{T}_1 \)该取什么类型。

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