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

第6章

章节6.1

练习6.1.1

题目：

For each of the following combinators

1. \( \text{c}_0 = \lambda \text{s. } \lambda \text{z. } \text{z} \);
2. \( \text{c}_2 = \lambda \text{s. } \lambda \text{z. } \text{s (s z)} \);
3. \( \text{plus} = \lambda \text{m. } \lambda \text{n. } \lambda \text{s. } \lambda \text{z. } \text{m s (n s z)} \)
4. \( \text{fix} = \lambda \text{f. } (\lambda \text{x. } \text{f } (\lambda \text{y. } \text{(x x) y})) \text{ } (\lambda \text{x. } \text{f } (\lambda \text{y. } \text{(x x) y})) \)
5. \( \text{foo} = (\lambda \text{x. } \text{ } (\lambda \text{x. } \text{x})) \text{ } (\lambda \text{x. } \text{x}) \)

解答：

1. \( \text{c}_0 = \lambda \text{. } \lambda \text{. } 0 \);
2. \( \text{c}_2 = \lambda \text{. } \lambda \text{. } \text{1 (1 0)} \);
3. \( \text{plus} = \lambda \text{. } \lambda \text{. } \lambda \text{. } \lambda \text{. } \text{3 1 (2 1 0)} \)
4. \( \text{fix} = \lambda \text{. } (\lambda \text{. } \text{1 } (\lambda \text{. } \text{(1 1) 0})) \text{ } (\lambda \text{. } \text{1 } (\lambda \text{. } \text{(1 1) 0})) \)
5. \( \text{foo} = (\lambda \text{. } \text{ } (\lambda \text{. } \text{0})) \text{ } (\lambda \text{. } \text{0}) \)

练习6.1.4

题目：

Give an alternative construction of the sets of \( n \)-terms in the style of Definition 3.2.3, and show (as we did in Proposition 3.2.6) that it is equivalent to the one above.

解答：

给出定义6.1.2在定义3.2.3风格下的定义：

如果直接仿照定义3.2.3，很容易得到如下有问题的定义：

\[ \begin{aligned} S_0 &= \empty \\ S_{i + 1} &= \{ 0, 1, \dots, i \} \\ &\cup \{ \lambda \text{. } \text{t}_1 \mid \text{t}_1 \in S_{i + 2} \} \\ &\cup \{ \text{t}_1 \text{ } \text{t}_2 \mid \text{t}_1, \text{t}_2 \in S_{i + 1} \} \end{aligned} \]

单看\( \cup \{ \lambda \text{. } \text{t}_1 \mid \text{t}_1 \in S_{i + 2} \} \)这条，可得\( S_{i + 1} \)的定义依赖于\( S_{i + 2} \)的定义，于是我们会想说先定义\( S_{i + 2} \)，而\( S_{i + 2} \)的定义进而依赖于\( S_{i + 3} \)的定义，那就得先定义\( S_{i + 3} \)，以此类推，自然数的数量是无限的，没完没了。这里如果把\( = \)看成赋值而非定义，则从闭包的角度来解释就行得通了。为了避免上述问题，我们采用分层的构建方法，每层均为集合的集合，或者说集族（family of sets）。

首先定义层\( 0 \)的集合，\( \forall i \in \mathbf{N} \)，我们定义\( S_{0i} \)如下：

\[ S_{0i} = \{ 0, 1, \dots, i - 1 \} \]

归纳假设\( \forall i \in \mathbf{N}, S_{ji} \)已定义（注：对\( j \)进行归纳，而不是\( i \)），则\( \forall i \in \mathbf{N} \)，我们定义\( S_{(j + 1)i} \)如下：

\[ \begin{aligned} S_{(j + 1)i} &= S_{ji} \\ &\cup \{ \lambda \text{. } \text{t}_1 \mid \text{t}_1 \in S_{j(i + 1)} \} \\ &\cup \{ \text{t}_1 \text{ } \text{t}_2 \mid \text{t}_1, \text{t}_2 \in S_{ji} \} \end{aligned} \]

综上，\( \forall i, j \in \mathbf{N}, S_{ij} \)均有定义，接下来，我们合并不同层对应的集合：

\( \forall i \in \mathbf{N} \)，令\( C_i = \bigcup_{j \in \mathbf{N}} C_{ji} \)。

最后，我们令\( C = \{ C_0, C_1, \dots \} \)。

我们断言\( C = \mathcal{T} \)（这里\( \mathcal{T} \)为定义6.1.2中的\( \mathcal{T} \)），且\( \forall i \in \mathbf{N}, C_i = \mathcal{T}_i \)。

容易看出上述定义通过分层定义来模拟赋值的过程。

证明两个定义等价：

为了证明两个定义等价，我们需要证明\( C \)为满足定义6.1.2的最小集族，这需要证明两点：

1. \( \forall i \in \mathbf{N}, C_i \)满足定义6.1.2中的3个条件。
2. 针对\( \forall \)集合\( D = \{ D_0, D_1, \dots \} \)，如果\( \forall i \in \mathbf{N}, D_i \)满足定义6.1.2中的3个条件，则我们有\( \forall i \in \mathbf{N}, C_i \subseteq D_i \)。

证明第1点：

考虑条件1，\( \forall i \in \mathbf{N} \)，由于\( S_{0i} = \{ 0, 1, \dots, i - 1 \} \sube C_i \)，因此条件1成立。

考虑条件2，\( \forall i > 0, \text{t}_1 \in C_i \)，我们需要证明\( \lambda \text{. } \text{t}_1 \in C_{i - 1} \)，由于\( \text{t}_1 \in C_i \)，因此根据\( C_i \)的定义，可得\( \exists j \in \mathbf{N}, \text{t}_1 \in S_{ji} \)（这里\( j \)即第几层），进而由\( S_{(j + 1)(i - 1)} \)的定义，可得\( \lambda \text{. } \text{t}_1 \in S_{{j + 1}(i - 1)} \)，进而可得\( \lambda \text{. } \text{t}_1 \in C_{i - 1} \)。

考虑条件3，\( \forall i > 0, \text{t}_1, \text{t}_2 \in C_i \)，我们需要证明\( \text{t}_1 \text{ } \text{t}_2 \in C_i \)，由于\( \text{t}_1, \text{t}_2 \in C_i \)，因此根据\( C_i \)的定义，可得\( \exists j_1, j_2 \in \mathbf{N}, \text{t}_1 \in S_{j_1i}, \text{t}_2 \in S_{j_2i} \)，不妨设\( j_1 \leq j_2 \)，则根据\( S_{j_1i}, S_{(j_1 + 1)i}, \dots, S_{j_2i} \)的定义，可得\( S_{j_1i} \subseteq S_{(j_1 + 1)i} \subseteq \dots \subseteq S_{j_2i} \)，进而可得\( \text{t}_1 \in S_{j_2i} \)，此时根据\( S_{(j_2 + 1)i} \)的定义，可得\( \text{t}_1 \text{ } \text{t}_2 \in S_{(j_2 + 1)i} \)，进而可得\( \text{t}_1 \text{ } \text{t}_2 \in C_i \)。

证明第2点：

\( \forall \)集合\( D = \{ D_0, D_1, \dots \} \)，如果\( \forall i \in \mathbf{N}, D_i \)满足定义6.1.2中的3个条件，则此时我们需要证明\( \forall i \in \mathbf{N}, C_i \subseteq D_i \)，而\( \forall i \in \mathbf{N}, C_i = \bigcup_{j \in \mathbf{N}} C_{ji} \)，因此这等价于证明\( \forall i \in \mathbf{N}, \forall j \in \mathbf{N}, S_{ji} \subseteq D_i \)，也等价于证明\( \forall j \in \mathbf{N}, \forall i \in \mathbf{N}, S_{ji} \subseteq D_i \)，我们对\( j \)（也就是第几层）进行归纳假设，\( i \)不做限制，可以为任意自然数：

当\( j = 0 \)时，\( \forall i \in \mathbf{N} \)，有\( S_{0i} = \{ 0, 1, \dots, i - 1 \} \)，由于\( D_i \)满足定义6.1.2的条件1，因此\( S_{0i} \subseteq D_i \)。

归纳假设当\( j = k \)时命题成立，即\( \forall i \in \mathbf{N}, S_{ki} \subseteq D_i \)，当\( j = k + 1 \)时，我们要证明\( \forall i \in \mathbf{N}, S_{(k + 1)i} \subseteq D_i \)， \( \forall \text{t} \in S_{(k + 1)i} \)，由于\( k + 1 > 0 \)，因此根据\( S_{(k + 1)i} \)的定义，可得如下情况中至少一种成立：

1. \( \text{t} \in S_{ki} \)
2. \( \text{t} = \lambda \text{. } \text{t}_1, \text{t}_1 \in S_{k(i + 1)} \)
3. \( \text{t} = \text{t}_1 \text{ } \text{t}_2, \text{t}_1, \text{t}_2 \in S_{ki} \)

分情况讨论：

1. 如果\( \text{t} \in S_{ki} \)，则根据归纳假设，可得\( S_{ki} \subseteq D_i \)，进而可得\( \text{t} \in D_i \)。
2. 如果\( \text{t} = \lambda \text{. } \text{t}_1, \text{t}_1 \in S_{k(i + 1)} \)，则根据归纳假设，可得\( S_{k(i + 1)} \subseteq D_{i + 1} \) （注意，归纳假设只限制了行下标，没有限制列下标，故列下标可以是任意自然数，当然可以是\( i + 1 \)），于是有\( \text{t}_1 \in D_{i + 1} \)，由于\( D_i, D_{i + 1} \)共同满足定义6.1.2的条件2，因此\( \text{t} = \lambda \text{. } \text{t}_1 \in D_i \)。
3. 如果\( \text{t} = \text{t}_1 \text{ } \text{t}_2, \text{t}_1, \text{t}_2 \in S_{ki} \) 则根据归纳假设，可得\( S_{ki} \subseteq D_i \)，于是有\( \text{t}_1, \text{t}_2 \in D_i \)，由于\( D_i \)满足定义6.1.2的条件3，因此\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \in D_i \)。

综上，当\( j = k + 1 \)时，命题也成立，归纳完毕。

至此，我们得到了\( \forall j \in \mathbf{N}, \forall i \in \mathbf{N}, S_{ji} \subseteq D_i \)，进而可得\( \forall i \in \mathbf{N}, \forall j \in \mathbf{N}, S_{ji} \subseteq D_i \)，最终可得\( \forall i \in \mathbf{N}, C_i \subseteq D_i \)。

总结：

由第1、2点成立，可得\( C \)为满足定义6.1.2的最小集族。

证毕。

练习6.1.5

题目：

1. Define a function \( \mathit{removenames}_{\Gamma}(\text{t}) \) that takes a naming context \( \Gamma \) and an ordinary term \( \text{t} \) (with \( FV(\text{t}) \subseteq dom(\Gamma) \)) and yields the corresponding nameless term.
2. Define a function \( \mathit{restorenames}_{\Gamma}(\text{t}) \) that takes a nameless term \( \text{t} \) and a naming context \( \Gamma \) and produces an ordinary term. (To do this, you will need to “make up” names for the variables bound by abstractions in \( \text{t} \). You may assume that the names in \( \Gamma \) are pairwise distinct and that the set \( \mathcal{V} \) of variable names is ordered, so that it makes sense to say “choose the first variable name that is not already in \( dom(\Gamma ) \).")

This pair of functions should have the property that

\[ \mathit{removenames}_{\Gamma}(\textit{restorenames}_{\Gamma}(\text{t})) = \text{t} \]

for any nameless term \( \text{t} \), and similarly

\[ \mathit{restorenames}_{\Gamma}(\textit{removenames}_{\Gamma}(\text{t})) = \text{t} \]

up to renaming of bound variables, for any ordinary term \( \text{t} \).

解答：

在定义\( \mathit{removenames}_{\Gamma}, \mathit{restorenames}_{\Gamma} \)之前，首先需要理解下命名上下文的作用（虽然书上解释过了，但是过于简略了）。

思考下，针对比较简单的项\( \text{t} = \lambda \text{x. } \text{x} \)，先不考虑怎么机械地进行转换，很容易得到对应的无名项是\( \lambda \text{. } 0 \)，但如果有自由变量呢？该怎么处理？考虑项\( \text{t} = \lambda \text{x. } \text{x y} \)，这里\( \text{y} \)是个自由变量，它的数字该设为多少？肯定不能是\( 0 \)，因为\( \text{y} \)和\( \text{x} \)并不是同一个变量，不能引用同一个绑定者，意义变了，数字设为\( 1 \)则是可以的，至少目前看不出什么问题，OK，那就设为\( 1 \)，那\( \text{t} = \lambda \text{x. } \text{x y} \)对应的无名项就是\( \lambda \text{. } \text{0 1} \)。

那进一步考虑有两个自由变量怎么办？比如\( \text{t} = \lambda \text{x. } \text{x y z} \)，这里\( \text{y} \)取\( 1 \)的话，\( \text{z} \)也能取\( 1 \)吗？假设如果两者都取\( 1 \)，则\( \text{t} = \lambda \text{x. } \text{x y z} \)对应的无名项就是\( \lambda \text{. } \text{0 1 1} \)，我们再在该无名项外层包一层\( \lambda \)-抽象，变成\( \lambda {. } \lambda \text{. } \text{0 1 1} \)，这相当于自由变量\( \text{y}, \text{z} \)变成绑定变量了，这时我们就发现问题了， \( \text{y}, \text{z} \)对应的数字\( 1 \)引用了同一个绑定者，然而它们不是同一个变量，不应该引用同一个绑定者，这和原始有名项\( \lambda \text{x. } \text{x y z} \)的行为不同，比如我们外层包一个\( \lambda \text{y} \)，则\( \lambda \text{x. } \text{x y z} \)会变成 \( \lambda \text{y. } \lambda \text{x. } \text{x y z} \)，这里\( \text{z} \)仍然是自由变量，同理，外层包个\( \lambda \text{z} \)，则\( \text{y} \)仍然是自由变量，这和无名项\( \lambda \text{. } \text{0 1 1} \)的行为不同，故我们得出结论，不同的自由变量不能取相同的数字，那怎么做到给不同的自由变量不同的数字呢？答案是用命名上下文，命名上下文刚好给不同的变量名赋值了不同的数字，举个例子，我们可以定义\( \Gamma \)如下：

\[ \begin{aligned} \Gamma &= \text{x} \mapsto 2 \\ &= \text{y} \mapsto 1 \\ &= \text{z} \mapsto 0 \end{aligned} \]

不过这里针对\( \Gamma \)的使用得小心点，如果不加处理地用\( \Gamma(\text{变量名}) \)取自由变量对应的数字的话，是会出问题的，比如继续之前的例子\( \lambda \text{x. } \text{x y z} \)，这里\( \Gamma(\text{y}) = 1, \Gamma(\text{z}) = 0 \)，如果直接使用这两个映射后的数字的话，则\( \lambda \text{x. } \text{x y z} \) 对应的无名项会是\( \lambda \text{. } \text{0 1 0} \)，这里就出问题了， \( \text{z} \)和\( \text{x} \)引用了同一个绑定者，为了解决这个问题，每进入一层\( \lambda \)-抽象，我们\( \Gamma \)函数映射的每个数字都应该\( + 1 \)，从而避免自由变量像这里一样被意外捕获，具体的，针对\( \lambda \text{x. } \text{x y z} \)，还没有进入\( \lambda \)-抽象之前，\( \Gamma \)的映射如下：

\[ \begin{aligned} \Gamma &= \text{x} \mapsto 2 \\ &= \text{y} \mapsto 1 \\ &= \text{z} \mapsto 0 \end{aligned} \]

进入\( \lambda \text{x} \)后，则每个映射数字都\( + 1 \)，\( \Gamma \)的映射变成：

\[ \begin{aligned} \Gamma &= \text{x} \mapsto 3 \\ &= \text{y} \mapsto 2 \\ &= \text{z} \mapsto 1 \end{aligned} \]

于是\( \Gamma(\text{y}) = 2, \Gamma(\text{z}) = 1 \)，进而可得\( \lambda \text{x. } \text{x y z} \)对应的无名项就是\( \lambda \text{. } \text{0 2 1} \)，这里就对了。

为了简化下面的两个定义，我们对命名上下文\( \Gamma \)的数字映射规则做一些限制：

1. 映射的数字必须是严格单调递增的，这样确保了每个数字都\( + 1 \)后，不会引入重复的数字。
2. 映射的数字必须都\( \geq 0 \)，这样确保了每个数字都\( + 1 \)后，数字\( 0 \)可以空出来。

在做了以上限制后，我们可以引入一个缩写：给定一个命名上下文\( \Gamma \)以及一个变量\( \text{x} \)，则\( \Gamma, \text{x} \)为新的命名上下文\( \Gamma' \)，在\( \Gamma' \)中，除\( \text{x} \)外的所有变量映射的数字都\( + 1 \)，且\( \Gamma'(\text{x}) = 0 \)，更严格一点定义就是：

1. \( dom(\Gamma') = dom(\Gamma) \cup \{ \text{x} \} \)
2. \( \forall \text{v} \in dom(\Gamma) \setminus \{ \text{x} \}, \Gamma'(\text{v}) = \Gamma(\text{v}) + 1 \)
3. \( \Gamma'(\text{x}) = 0 \)

下面，我们可以开始定义了。

定义\( \mathit{removenames}_{\Gamma} \)：

给定项\( \text{t} \)，归纳假设针对\( \forall \text{t} \)的直接子项\( \text{t}' \)，有\( \forall \)满足\( FV(\text{t}) \subseteq dom(\Gamma) \)的命名上下文\( \Gamma \)， \( \mathit{removenames}_{\Gamma}(\text{t}') \)均已定义，则\( \forall \)满足\( FV(\text{t}) \subseteq dom(\Gamma) \)的命名上下文\( \Gamma \)，按如下规则定义\( \mathit{removenames}_{\Gamma}(\text{t}) \)：

1. 如果\( \text{t} = \text{x} \)，即\( \text{t} \)为变量，则由\( FV(\text{t}) = \{ \text{x} \} \subseteq dom(\Gamma) \)，可得\( \Gamma(\text{x}) \)是有定义的，于是我们定义\( \mathit{removenames}_{\Gamma}(\text{t}) = \mathit{removenames}_{\Gamma}(\text{x}) = \Gamma(\text{x}) \)。
2. 如果\( \text{t} = \lambda \text{x. } \text{t}_1 \)，由于\( FV(\text{t}_1) \subseteq FV(\text{t}) \cup \{ \text{x} \} \subseteq dom(\Gamma) \cup \{ \text{x} \} = dom(\Gamma, \text{x}) \)，因此根据归纳假设，\( \mathit{removenames}_{\Gamma, \text{x}}(\text{t}_1) \)已定义（注意，我们归纳假设中，没有限定具体的命名上下文\( \Gamma \)，只要满足 \( FV(\text{t}) \subseteq dom(\Gamma) \)即可），于是我们定义\( \mathit{removenames}_{\Gamma}(\text{t}) = \lambda \text{. } \mathit{removenames}_{\Gamma, \text{x}}(\text{t}_1) \)。
3. 如果\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)，则\( FV(\text{t}_1) \subseteq FV(\text{t}_1) \cup FV(\text{t}_2) = FV(\text{t}) \subseteq dom(\Gamma) \)，同理易得\( FV(\text{t}_2) \subseteq dom(\Gamma) \)，因此根据归纳假设，\( \mathit{removenames}_{\Gamma}(\text{t}_1), \mathit{removenames}_{\Gamma}(\text{t}_2) \)均已定义，于是我们定义\( \mathit{removenames}_{\Gamma}(\text{t}) = \mathit{removenames}_{\Gamma}(\text{t}_1) \text{ } \mathit{removenames}_{\Gamma}(\text{t}_2) \)。

读者可以自己举几个简单的例子，看看上述定义为什么是正确的，通过例子很容易可以看出来为什么\( \mathit{removenames}_{\Gamma}(\text{t}) = \lambda \text{. } \mathit{removenames}_{\Gamma, \text{x}}(\text{t}_1) \)要把\( \text{x} \)映射的数字改成\( 0 \)，如果\( \text{x} \)在函数体\( \text{t}_1 \)中出现在更深层的位置会不会出问题等，由于上述递归定义是通过结构归纳法来定义的，因此通过结构归纳法很容易证明上述定义能正确地给出一个项对应的无名项，这里就省略证明了。

定义\( \mathit{restorenames}_{\Gamma} \)：

前面我们通过命名上下文\( \Gamma \)来找到一个变量对应的数字，这里我们需要为一个数字找其对应的名字，这可以通过命名上下文\( \Gamma \)的逆映射来进行，注意到\( \Gamma \)是 \( dom(\Gamma) \to \Gamma(dom(\Gamma)) \)的双射，因此存在逆映射\( \Gamma^{-1} \)，举个例子，假设\( \Gamma \)的定义如下：

\[ \begin{aligned} \Gamma &= \text{x} \mapsto 2 \\ &= \text{y} \mapsto 1 \\ &= \text{z} \mapsto 0 \end{aligned} \]

则\( \Gamma^{-1} \)的定义如下：

\[ \begin{aligned} \Gamma^{-1} &= 2 \mapsto \text{x} \\ &= 1 \mapsto \text{y} \\ &= 0 \mapsto \text{z} \end{aligned} \]

下面，我们开始定义\( \mathit{restorenames}_{\Gamma} \)。

给定项\( \text{t} \)，归纳假设针对\( \forall \text{t} \)的直接子项\( \text{t}' \)，有\( \forall \)命名上下文\( \Gamma \)， \( \mathit{restorenames}_{\Gamma}(\text{t}') \)均已定义，则\( \forall \)命名上下文\( \Gamma \)，按如下规则定义\( \mathit{restorenames}_{\Gamma}(\text{t}) \)：

1. 如果\( \text{t} = k \)，即\( \text{t} \)为数字，则我们定义\( \mathit{restorenames}_{\Gamma}(\text{t}) = \Gamma^{-1}(k) \)。
2. 如果\( \text{t} = \lambda \text{x. } \text{t}_1 \)，任取\( \text{x} \in \mathcal{V} \setminus dom(\Gamma) \)，或者实在不知道怎么在\( \mathcal{V} \setminus dom(\Gamma) \)取个元素的话，则题目说了，我们可以假设\( \mathcal{V} \)中的变量是有序的，即每个变量都有对应的全局序号，因此\( \exists \)变量名\( \text{x} \)满足\( \text{x} \notin dom(\Gamma) \)且 \( \forall \text{v} \in \mathcal{V}, \text{v} \notin dom(\Gamma) \)，均有\( \text{x} \)的序号\( \leq \text{v} \)的序号，简而言之，\( \text{x} \)为\( \mathcal{V} \)中第一个（按序号算是不是第一个）不在\( dom(\Gamma) \)中的变量名，这里取的第一个满足条件的变量名，实际上取第几个条件的变量名是无所谓的，第二个也行，第三个也行，这里只是为了步骤的确定性随便取了第一个。根据归纳假设，\( \mathit{restorenames}_{\Gamma, \text{x}}(\text{t}_1) \)已定义（注意，我们归纳假设中，没有限定具体的命名上下文\( \Gamma \)），我们定义\( \mathit{restorenames}_{\Gamma}(\text{t}) = \lambda \text{x. } \mathit{restorenames}_{\Gamma, \text{x}}(\text{t}_1) \)，由于\( \text{x} \)为之前\( dom(\Gamma) \)没有的变量名，因此新命名上下文\( \Gamma, \text{x} \)不会丢失/覆盖\( \Gamma \)中的任何一个变量名，注意到我们针对函数体\( \text{t}_1 \)把变量名\( \text{x} \)加到命名上下文中且对应的映射数字为\( 0 \)，其他映射数字则均\( + 1 \)了，考虑到加了一层\( \lambda \)-抽象，函数体\( \text{t}_1 \)中针对绑定者的距离确实应该都\( + 1 \)（新增变量名\( \text{x} \)除外），而针对数字\( 0 \)，函数体\( \text{t}_1 \)中如果出现了\( 0 \)且如果我们不考虑在更深\( \lambda \)-抽象中的\( 0 \)，则该\( 0 \)会被我们前一个针对数字的\( \mathit{restorenames}_{\Gamma} \)定义定义成\( \Gamma^{-1}(0) = \text{x} \)，刚好引用了我们新给的最近一层\( \lambda \)-抽象的变量名\( \text{x} \)，更深层次的函数体以此类推。
3. 如果\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)，则根据归纳假设，\( \mathit{restorenames}_{\Gamma}(\text{t}_1), \mathit{restorenames}_{\Gamma}(\text{t}_2) \)均已定义，于是我们定义\( \mathit{restorenames}_{\Gamma}(\text{t}) = \mathit{restorenames}_{\Gamma}(\text{t}_1) \text{ } \mathit{restorenames}_{\Gamma}(\text{t}_2) \)。

容易通过结构归纳法证明上述定义能正确地给出一个无名项对应的有名项，这里就省略证明了。

关于题目要求定义满足的两个属性：

通过结构归纳法，易证给定任意一个无名项\( \text{t} \)以及一个命名上下文\( \Gamma \)，则下面这个等式成立：

\[ \mathit{removenames}_{\Gamma}(\textit{restorenames}_{\Gamma}(\text{t})) = \text{t} \]

类似的，通过结构归纳法，易证给定任意一个有名项\( \text{t} \)以及一个满足\( FV(\text{t}) \subseteq dom(\Gamma) \)的命名上下文\( \Gamma \)，则下面这个等式成立（这里的\( = \)仅仅是结构上、语义上等价，变量名允许不同，用\( \lambda \)-演算理论的定义/词汇来说，就是两者\( \alpha \)-等价（其他书中有这个定义，本书只是简单带过））：

\[ \mathit{restorenames}_{\Gamma}(\textit{removenames}_{\Gamma}(\text{t})) = \text{t} \]

进一步限制命名上下文数字映射规则：

前面我们限制了命名上下文数字映射规则为：

1. 映射的数字必须是严格单调递增的。
2. 映射的数字必须都\( \geq 0 \)。

可以进一步限制映射的数字必须从\( 0 \)开始且每次都\( + 1 \)，这样能确保如果\( \text{t} \)有\( n \)个自由变量，则\( \mathit{removenames}_{\Gamma}(\text{t}) \)为定义6.1.2中的\( n \)-项，即\( \mathit{removenames}_{\Gamma}(\text{t}) \in \mathcal{T}_n \)。

章节6.2

练习6.2.2

题目：

1. What is \( \uparrow^2 (\lambda \text{. } \lambda \text{. } \text{1 (0 2)}) \)?
2. What is \( \uparrow^2 (\lambda \text{. } \text{0 1} \text{ } (\lambda \text{. } \text{0 1 2})) \)?

解答：

解答1：

\[ \begin{aligned} &\uparrow^2 (\lambda \text{. } \lambda \text{. } \text{1 (0 2)}) \\ &= \lambda \text{. } \uparrow^2_1(\lambda \text{. } \text{1 (0 2)}) \\ &= \lambda \text{. } \lambda \text{. } \uparrow^2_2(\text{1 (0 2)}) \\ &= \lambda \text{. } \lambda \text{. } \uparrow^2_2(\text{1}) \text{ } \uparrow^2_2(\text{0 2}) \\ &= \lambda \text{. } \lambda \text{. } \text{1} \text{ } \uparrow^2_2(\text{0 2}) \\ &= \lambda \text{. } \lambda \text{. } \text{1} \text{ } \uparrow^2_2(\text{0}) \text{ } \uparrow^2_2(\text{2}) \\ &= \lambda \text{. } \lambda \text{. } \text{1} \text{ } \text{0} \text{ } \uparrow^2_2(\text{2}) \\ &= \lambda \text{. } \lambda \text{. } \text{1 0 4} \end{aligned} \]

解答2：

\[ \begin{aligned} &\uparrow^2 (\lambda \text{. } \text{0 1} \text{ } (\lambda \text{. } \text{0 1 2})) \\ &= \lambda \text{. } \uparrow^2_1(\text{0 1} \text{ } (\lambda \text{. } \text{0 1 2})) \\ &= \lambda \text{. } \uparrow^2_1(\text{0 1}) \text{ } \uparrow^2_1(\lambda \text{. } \text{0 1 2}) \\ &= \lambda \text{. } (\uparrow^2_1(\text{0}) \text{ } \uparrow^2_1(\text{1})) \text{ } \uparrow^2_1(\lambda \text{. } \text{0 1 2}) \\ &= \lambda \text{. } (\text{0} \text{ } \uparrow^2_1(\text{1})) \text{ } \uparrow^2_1(\lambda \text{. } \text{0 1 2}) \\ &= \lambda \text{. } (\text{0 3}) \text{ } \uparrow^2_1(\lambda \text{. } \text{0 1 2}) \\ &= \lambda \text{. } (\text{0 3}) \text{ } \lambda \text{. } \uparrow^2_2(\text{0 1 2}) \\ &= \lambda \text{. } (\text{0 3}) \text{ } \lambda \text{. } (\uparrow^2_2(\text{0 1}) \text{ } \uparrow^2_2(\text{2})) \\ &= \lambda \text{. } (\text{0 3}) \text{ } \lambda \text{. } ((\uparrow^2_2(\text{0}) \text{ } \uparrow^2_2(\text{1})) \text{ } \uparrow^2_2(\text{2})) \\ &= \lambda \text{. } (\text{0 3}) \text{ } \lambda \text{. } ((\text{0} \text{ } \uparrow^2_2(\text{1})) \text{ } \uparrow^2_2(\text{2})) \\ &= \lambda \text{. } (\text{0 3}) \text{ } \lambda \text{. } ((\text{0 1}) \text{ } \uparrow^2_2(\text{2})) \\ &= \lambda \text{. } (\text{0 3}) \text{ } \lambda \text{. } ((\text{0 1}) \text{ } \text{4}) \\ &= \lambda \text{. } \text{0 3} \text{ } \lambda \text{. } \text{0 1 4} \end{aligned} \]

练习6.2.3

题目：

Given an \( n \)-term \( \text{t} \) (\( n \) is a natural number), an integral \( d \), and a natural number \( c \), show that:

1. If \( d \geq 0 \), then \( \uparrow^d_c(\text{t}) \) is an \( (n + d) \)-term.
2. If \( d < 0 \) and the free variables of \( \text{t} \) are all at least \( |d| \), then \( \uparrow^d_c(\text{t}) \) is an \( (\max(n + d, 0, c)) \)-term.

关于勘误：

原题目为：

Show that if \( \text{t} \) is an \( n \)-term, then \( \uparrow^d_c(\text{t}) \) is an \( (n + d) \)-term.

但我们在后面的章节会用到\( d < 0 \)的情况，然而针对\( d < 0 \)，上述命题的成立是需要有额外条件的，具体的，在\( d < 0 \)的情况下，我们需要\( \text{t} \)中所有自由变量都\( \geq |d| \)，此时我们才能保证我们每次\( + d \)的时候不会产生负数（注意，\( d > 0 \)时不需要有该限制），不然负数是不满足定义6.1.2的。

作者勘误原文如下：

The statement to be shown is not quite true for \( d < 0 \). To be true for \( n \geq 0 \) and any integral \( d \), it should be “Show that, if \( \text{t} \) is an \( n \)-term and, if \( d < 0 \), the free variables of \( \text{t} \) are all at least \( |d| \), then <shift \( \text{t} \) up by \( d \) above cutoff \( c \)> is a \( (\max(n + d, 0)) \)-term.”

这里为什么要取\( \max(n + d, 0) \)而不直接用\( n + d \)呢？举个例子就知道了，考虑项\( \text{t} = \lambda \text{. } \text{0 5} \)，根据定义6.1.2的1和2，可得\( \text{t} \)为\( (n = 4) \)-项，令\( d = -5, c = 0 \)，此时由\( \text{t} \)中的自由变量均\( \geq |d| \)，满足上述条件，可得\( \uparrow^d_c(\text{t}) = \lambda \text{. } \text{0 0} \)，而\( n + d = 4 - 5 = -1 \)，这和实际\( \uparrow^d_c(\text{t}) = \lambda \text{. } \text{0 0} \)为\( 0 \)-项不符，故需要取\( \max(n + d, 0) \)。

但\( d < 0 \)时限制自由变量\( \geq |d| \)还不够，考虑\( \text{t} = 3 \)是\( 4 \)-项，而\( \uparrow^{-3}_5(\text{t}) = 3 \)是\( 4 \)-项非\( (\max(4 - 3, 0) = 1) \)-项，故不应该是\( (\max(n + d, 0)) \)-项，而应该是\( (\max(n + d, 0, c)) \)-项，这里虽然\( \max(n + d, 0, c) \)会把\( \text{t} \)归类为\( 5 \)-项，不过也是符合定义6.1.2的。

证明：

如果\( \text{t} \)为\( n \)-项，则根据定义6.1.2，可得如下情况中至少一种成立：

1. \( \text{t} = k, k \in \mathbf{N}, 0 \leq k < n \)。
2. \( \text{t} = \lambda \text{. } \text{t}_1 \)，\( \text{t}_1 \)为\( (n + 1) \)-项。
3. \( \text{t} = \text{t}_1 \text{ } \text{t}_2 \) 且\( \text{t}_1, \text{t}_2 \)均为\( n \)-项。

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

1. 如果\( \text{t} = k, k \in \mathbf{N}, 0 \leq k < n \)，
   1. 如果\( k \geq c \)：
      1. 如果\( d \geq 0 \)，则\( 0 \leq \uparrow^d_c(\text{t}) = k + d < n + d \)，根据定义6.1.2的1，可得\( \uparrow^d_c(\text{t}) \)为\( (n + d) \)-项。
      2. 如果\( d < 0 \)，则此时\( k \geq |d| \)，于是有\( k + d \geq 0 \)，此时可得\( 0 \leq \uparrow^d_c(\text{t}) = k + d < n + d \)，根据定义6.1.2的1，可得\( \uparrow^d_c(\text{t}) \)为\( (n + d) \)-项，加上\( \max(n + d, 0, c) = n + d \)，于是有\( \uparrow^d_c(\text{t}) \)为\( (\max(n + d, 0, c)) \)-项。
   2. 如果\( k < c \)：
      1. 如果\( d \geq 0 \)，则\( 0 \leq \uparrow^d_c(\text{t}) = k < n + d \)，根据定义6.1.2的1，可得\( \uparrow^d_c(\text{t}) \)为\( (n + d) \)-项。
      2. 如果\( d < 0 \)，则\( 0 \leq \uparrow^d_c(\text{t}) = k < \max(n + d, 0, c) \)，根据定义6.1.2的1，可得\( \uparrow^d_c(\text{t}) \)为\( (\max(n + d, 0, c)) \)-项。
2. 如果\( \text{t} = \lambda \text{. } \text{t}_1 \)，\( \text{t}_1 \)为\( (n + 1) \)-项，
   1. 如果\( d \geq 0 \)，则根据归纳假设，可得\( \uparrow^d_{c + 1}(\text{t}_1) \)为\( ((n + 1) + d) \)-项，进而根据定义6.2.1的第二项以及定义6.1.2的2，可得\( \uparrow^d_c(\text{t}) \)为\( (n + d) \)-项。
   2. 如果\( d < 0 \)，则此时\( k \geq |d| \)，根据归纳假设，可得\( \uparrow^d_{c + 1}(\text{t}_1) \)为\( (\max((n + 1) + d, 0, c + 1)) \)-项，进而根据定义6.2.1的第二项以及定义6.1.2的2，可得\( \uparrow^d_c(\text{t}) \)为\( (\max((n + 1) + d, 0, c + 1) - 1) \)-项：
      1. 如果\( \max((n + 1) + d, 0, c + 1) = (n + 1) + d \)，则\( (n + 1) + d \geq c + 1 \)，进而\( n + d \geq c \)，加上\( c \in \mathbf{N} \)，有\( c \geq 0 \)，于是也有\( n + d \geq 0 \)，综合可得\( \max(n + d, 0, c) = n + d = \max((n + 1) + d, 0, c + 1) - 1 \)，于是可得\( \uparrow^d_c(\text{t}) \)为\( (\max(n + d, 0, c)) \)-项。
      2. 如果\( \max((n + 1) + d, 0, c + 1) = 0 \)，则\( c + 1 \leq 0 \)，故这种情况不可能，因为这意味着\( c \leq -1 \)不为自然数，矛盾。
      3. 如果\( \max((n + 1) + d, 0, c + 1) = c + 1 \)，则\( c + 1 \geq (n + 1) + d \)，进而\( c \geq n + d \)，加上\( c \in \mathbf{N} \)，有\( c \geq 0 \)，综合可得\( \max(n + d, 0, c) = c = \max((n + 1) + d, 0, c + 1) - 1 \)，于是可得\( \uparrow^d_c(\text{t}) \)为\( (\max(n + d, 0, c)) \)-项。
3. 如果\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)且\( \text{t}_1, \text{t}_2 \)均为\( n \)-项，
   1. 如果\( d \geq 0 \)，则根据归纳假设，可得\( \uparrow^d_{c}(\text{t}_1), \uparrow^d_{c}(\text{t}_2) \)为\( (n + d) \)-项，进而根据定理6.2.1的第三项以及定义6.1.2的3，可得\( \uparrow^d_{c}(\text{t}) \)为\( (n + d) \)-项。
   2. 如果\( d < 0 \)，则根据归纳假设，可得\( \uparrow^d_{c}(\text{t}_1), \uparrow^d_{c}(\text{t}_2) \)为\( (\max(n + d, 0, c)) \)-项，进而根据定理6.2.1的第三项以及定义6.1.2的3，可得\( \uparrow^d_{c}(\text{t}) \)为\( (\max(n + d, 0, c)) \)-项。

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

证毕。

练习6.2.5

Convert the following uses of substitution to nameless form, assuming the global context is \( \Gamma = \text{a}, \text{b} \), and calculate their results using the above definition. Do the answers correspond to the original definition of substitution on ordinary terms from \( \S \text{5.3} \)?

1. \( [\text{b} \mapsto \text{a}](\text{b } (\lambda \text{x. } \lambda \text{y. } \text{b})) \)
2. \( [\text{b} \mapsto \text{a} \text{ } (\lambda \text{z. } \text{a})] (\text{b } (\lambda \text{x. } \text{b})) \)
3. \( [\text{b} \mapsto \text{a}](\lambda \text{b. } \text{b a}) \)
4. \( [\text{b} \mapsto \text{a}](\lambda \text{a. } \text{b a}) \)

解答：

解答1：

针对\( [\text{b} \mapsto \text{a}](\text{b } (\lambda \text{x. } \lambda \text{y. } \text{b})) \)：

\( \text{b } (\lambda \text{x. } \lambda \text{y. } \text{b}) \)转换成无名项后如下：

\[ \text{0 } (\lambda \text{. } \lambda \text{. } \text{2}) \]

进而\( [\text{b} \mapsto \text{a}](\text{b } (\lambda \text{x. } \lambda \text{y. } \text{b})) \)对应的无名项变量代入结果如下：

\[ \begin{aligned} &[\text{0} \mapsto \text{1}](\text{0 } (\lambda \text{. } \lambda \text{. } \text{2})) \\ &= ([\text{0} \mapsto \text{1}](\text{0})) \text{ } ([\text{0} \mapsto \text{1}](\lambda \text{. } \lambda \text{. } \text{2})) \\ &= (\text{1}) \text{ } ([\text{0} \mapsto \text{1}](\lambda \text{. } \lambda \text{. } \text{2})) \\ &= (\text{1}) \text{ } (\lambda \text{. } [\text{1} \mapsto \uparrow^1(\text{1})](\lambda \text{. } \text{2})) \\ &= (\text{1}) \text{ } (\lambda \text{. } [\text{1} \mapsto 2](\lambda \text{. } \text{2})) \\ &= (\text{1}) \text{ } (\lambda \text{. } \lambda \text{. } [\text{2} \mapsto \uparrow^1(2)](\text{2})) \\ &= (\text{1}) \text{ } (\lambda \text{. } \lambda \text{. } [\text{2} \mapsto 3](\text{2})) \\ &= (\text{1}) \text{ } (\lambda \text{. } \lambda \text{. } (\text{3})) \\ &= \text{1 } (\lambda \text{. } \lambda \text{. } \text{3}) \end{aligned} \]

而\( [\text{b} \mapsto \text{a}](\text{b } (\lambda \text{x. } \lambda \text{y. } \text{b})) = \text{a } (\lambda \text{x. } \lambda \text{y. } \text{a}) \)，对应的无名项是\( \text{1 } (\lambda \text{. } \lambda \text{. } \text{3}) \)，和上面无名项变量代入的结果一致。

解答2：

针对\( [\text{b} \mapsto \text{a} \text{ } (\lambda \text{z. } \text{a})] (\text{b } (\lambda \text{x. } \text{b})) \)：

\( \text{b } (\lambda \text{x. } \text{b}) \)转换成无名项后如下：

\[ \text{0 } (\lambda \text{. } \text{1}) \]

\( \text{a } (\lambda \text{z. } \text{a}) \)转换成无名项后如下：

\[ \text{1 } (\lambda \text{. } \text{2}) \]

进而\( [\text{b} \mapsto \text{a}](\text{b } (\lambda \text{x. } \lambda \text{y. } \text{b})) \)对应的无名项变量代入结果如下：

\[ \begin{aligned} &[\text{0} \mapsto \text{1 } (\lambda \text{. } \text{2})](\text{0 } (\lambda \text{. } \text{1})) \\ &= ([\text{0} \mapsto \text{1 } (\lambda \text{. } \text{2})](\text{0})) \text{ } ([\text{0} \mapsto \text{1 } (\lambda \text{. } \text{2})](\lambda \text{. } \text{1})) \\ &= (\text{1 } (\lambda \text{. } \text{2})) \text{ } ([\text{0} \mapsto \text{1 } (\lambda \text{. } \text{2})](\lambda \text{. } \text{1})) \\ &= (\text{1 } (\lambda \text{. } \text{2})) \text{ } (\lambda \text{. } [\text{1} \mapsto \uparrow^1(\text{1 } (\lambda \text{. } \text{2}))](\text{1})) \\ &= (\text{1 } (\lambda \text{. } \text{2})) \text{ } (\lambda \text{. } [\text{1} \mapsto \text{2 } (\lambda \text{. } \text{3})](\text{1})) \\ &= (\text{1 } (\lambda \text{. } \text{2})) \text{ } (\lambda \text{. } (\text{2 } (\lambda \text{. } \text{3}))) \\ &= (\text{1 } (\lambda \text{. } \text{2})) \text{ } (\lambda \text{. } \text{2 } (\lambda \text{. } \text{3})) \end{aligned} \]

而\( [\text{b} \mapsto \text{a} \text{ } (\lambda \text{z. } \text{a})] (\text{b } (\lambda \text{x. } \text{b})) = (\text{a} \text{ } (\lambda \text{z. } \text{a})) \text{ } (\lambda \text{x. } \text{a} \text{ } (\lambda \text{z. } \text{a})) \)，对应的无名项是\( (\text{1} \text{ } (\lambda \text{. } \text{2})) \text{ } (\lambda \text{. } \text{2 } (\lambda \text{. } \text{3})) \)，和上面无名项变量代入的结果一致。

解答3：

针对\( [\text{b} \mapsto \text{a}](\lambda \text{b. } \text{b a}) \)：

\( \lambda \text{b. } \text{b a} \)转换成无名项后如下：

\[ \lambda \text{. } \text{0 2} \]

进而\( [\text{b} \mapsto \text{a}](\lambda \text{b. } \text{b a}) \)对应的无名项变量代入结果如下：

\[ \begin{aligned} &[\text{0} \mapsto \text{1}](\lambda \text{. } \text{0 2}) \\ &= \lambda \text{. } [\text{1} \mapsto \uparrow^1(\text{1})](\text{0 2}) \\ &= \lambda \text{. } [\text{1} \mapsto \text{2}](\text{0 2}) \\ &= \lambda \text{. } [\text{1} \mapsto \text{2}](\text{0}) \text{ } [\text{1} \mapsto \text{2}](\text{2}) \\ &= \lambda \text{. } (\text{0}) \text{ } (\text{2}) \\ &= \lambda \text{. } \text{0 2} \end{aligned} \]

而\( [\text{b} \mapsto \text{a}](\lambda \text{b. } \text{b a}) = \lambda \text{b. } \text{b a} \)，对应的无名项是\( \lambda \text{. } \text{0 2} \)，和上面无名项变量代入的结果一致。

解答4：

针对\( [\text{b} \mapsto \text{a}](\lambda \text{a. } \text{b a}) \)：

\( \lambda \text{a. } \text{b a} \)转换成无名项后如下：

\[ \lambda \text{. } \text{1 0} \]

进而\( [\text{b} \mapsto \text{a}](\lambda \text{a. } \text{b a}) \)对应的无名项变量代入结果如下：

\[ \begin{aligned} &[\text{0} \mapsto \text{1}](\lambda \text{. } \text{1 0}) \\ &= \lambda \text{. } [\text{1} \mapsto \uparrow^1\text{1}](\text{1 0}) \\ &= \lambda \text{. } [\text{1} \mapsto 2](\text{1 0}) \\ &= \lambda \text{. } [\text{1} \mapsto 2](\text{1}) \text{ } [\text{1} \mapsto 2](\text{0}) \\ &= \lambda \text{. } (\text{2}) \text{ } [\text{1} \mapsto 2](\text{0}) \\ &= \lambda \text{. } (\text{2}) \text{ } (\text{0}) \\ &= \lambda \text{. } \text{2 0} \end{aligned} \]

而\( [\text{b} \mapsto \text{a}](\lambda \text{a. } \text{b a}) = \lambda \text{a}' \text{. } \text{a } \text{a}' \) （注：由于这里内层绑定变量\( \text{a} \)和自由变量\( \text{a} \)重名了，因此需要对绑定变量\( \text{a} \)进行改名），对应的无名项是\( \lambda \text{. } \text{2 0} \)，和上面无名项变量代入的结果一致。

练习6.2.6

题目：

Show that if \( \text{s} \) and \( \text{t} \) are \( n \)-terms and \( j \leq n \), then \( [j \mapsto \text{s}]\text{t} \) is an \( n \)-term.

证明：

如果\( \text{t} \)为\( n \)-项，则根据定义6.1.2，可得如下情况中至少一种成立：

1. \( \text{t} = k, k \in \mathbf{N}, 0 \leq k < n \)。
2. \( \text{t} = \lambda \text{. } \text{t}_1 \)，\( \text{t}_1 \)为\( (n + 1) \)-项。
3. \( \text{t} = \text{t}_1 \text{ } \text{t}_2 \) 且\( \text{t}_1, \text{t}_2 \)均为\( n \)-项。

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

1. 如果\( \text{t} = k, k \in \mathbf{N}, 0 \leq k < n \)，
   1. 如果\( j = k \)，则\( [j \mapsto \text{s}]\text{t} = \text{s} \)为\( n \)-项。
   2. 如果\( j \neq k \)，则\( 0 \leq [j \mapsto \text{s}]\text{t} = k < n \)，根据定义6.1.2的1，可得\( [j \mapsto \text{s}]\text{t} \)为\( n \)-项。
2. 如果\( \text{t} = \lambda \text{. } \text{t}_1 \)，\( \text{t}_1 \)为\( (n + 1) \)-项，则根据练习6.2.3，可得\( \uparrow^1(\text{s}) \)为\( (n + 1) \)-项，加上\( j + 1 \leq n + 1 \)，于是根据归纳假设，可得\( [j + 1 \mapsto \uparrow^1(\text{s})]\text{t}_1 \)为\( (n + 1) \)-项，进而根据6.2.4的第二项和定义6.1.2的2，可得\( [j \mapsto \text{s}]\text{t} \)为\( n \)-项。
3. 如果\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)且\( \text{t}_1, \text{t}_2 \)均为\( n \)-项，根据归纳假设，可得\( [j \mapsto \text{s}]\text{t}_1, [j \mapsto \text{s}]\text{t}_2 \)均为\( n \)-项，进而根据6.2.4的第三项和定义6.1.2的3，可得\( [j \mapsto \text{s}]\text{t} \)为\( n \)-项。

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

证毕。

练习6.2.7

题目：

Take a sheet of paper and, without looking at the definitions of substitution and shifting above, regenerate them.

解答：

无名项的变量代入需要用到位移的定义，故我们先定义位移，如下：

给定\( d \in \mathbf{Z}, c \in \mathbf{N} \)，则 \( \forall n \in \mathbf{N}, \forall \text{t} \in \mathcal{T}_n \)，根据如下规则定义\( \uparrow^d_c(\text{t}) \)：

1. 如果\( \text{t} = k \)：
   1. 如果\( k \geq c \)，则\( \uparrow^d_c(\text{t}) = k + d \)。
   2. 如果\( k < c \)，则\( \uparrow^d_c(\text{t}) = k \)。
2. 如果\( \text{t} = \lambda \text{. } \text{t}_1 \)，则\( \uparrow^d_c(\text{t}) = \lambda \text{. } \uparrow^d_{c + 1}(\text{t}_1) \)。
3. 如果\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)，则\( \uparrow^d_c(\text{t}) = \uparrow^d_{c + 1}(\text{t}_1) \text{ } \uparrow^d_{c + 1}(\text{t}_2) \)。

我们定义\( \uparrow^d(\text{t}) = \uparrow^d_0(\text{t}) \)。

最后，我们定义无名项的变量代入，如下：

给定\( j \in \mathbf{N} \)以及无名项\( \text{s}, \text{t} \)，根据如下规则定义\( [j \mapsto \text{s}](\text{t}) \)：

1. 如果\( \text{t} = k \)：
   1. 如果\( k = j \)，则\( [j \mapsto \text{s}](\text{t}) = \text{s} \)。
   2. 如果\( k \neq j \)，则\( [j \mapsto \text{s}](\text{t}) = k \)。
2. 如果\( \text{t} = \lambda \text{. } \text{t}_1 \)，则\( [j \mapsto \text{s}](\text{t}) = \lambda \text{. } ([j + 1 \mapsto \uparrow^1(\text{s})]\text{t}_1) \)。
3. 如果\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)，则\( [j \mapsto \text{s}](\text{t}) = ([j \mapsto \text{s}]\text{t}_1) \text{ } ([j \mapsto \text{s}]\text{t}_2) \)。

练习6.2.8

题目：

The definition of substitution on nameless terms should agree with our informal definition of substitution on ordinary terms.

1. What theorem needs to be proved to justify this correspondence rigorously?
2. Prove it.

解答：

如何描述无名项的变量代入和定义5.3.5定义的有名项变量代入一致呢？

两种变量代入机制一致，即两种变量代入机制代入后得到的项“等价”，但两种变量代入机制代入后得到的项性质不同，一个是有名项，一个是无名项，无法直接进行比较，得进行转换，比如把有名项转换成无名项，然后比较两个无名项，或者反之，这里统一转换成有名项进行比较会麻烦点，比如根据约定5.3.4，我们希望这个有名项比较机制能判断\( \lambda \text{x. } \text{x} = \lambda \text{y. } \text{y} \)，即绑定变量的名字是不重要的，定义这个等价关系不难，但更简单的，就是将两者统一转换成无名项进行比较，比较的都是数字，数字还是根据距离绑定者的层数来取的，固定的，不会有像变量名那样可以随便取的问题，比较好判等。

决定统一转换成无名项进行比较后，对应“无名项的变量代入和定义5.3.5定义的有名项变量代入一致”的描述如下（关键在于使用之前定义的\( \mathit{removenames} \)把有名项转换成无名项）：

给定变量名\( \text{x} \)、对应的代入项\( \text{s} \)以及被代入项\( \text{t} \)，再给定一个命名上下文\( \Gamma \)，要求\( FV(\text{t}) \subseteq dom(\Gamma), x \in dom(\Gamma) \)，我们断言如下等式成立：

\[ \mathit{removenames}_{\Gamma}([\text{x} \mapsto \text{s}](\text{t})) = [\Gamma(\text{x}) \mapsto \mathit{removenames}_{\Gamma}(\text{s})](\mathit{removenames}_{\Gamma}(\text{t})) \]

注：这里\( \Gamma(\text{x}) = \mathit{removenames}_{\Gamma}(\text{x}) \)，故如果读者为了形式更加统一，可以把上面改成：

\[ \mathit{removenames}_{\Gamma}([\text{x} \mapsto \text{s}](\text{t})) = [\mathit{removenames}_{\Gamma}(\text{x}) \mapsto \mathit{removenames}_{\Gamma}(\text{s})](\mathit{removenames}_{\Gamma}(\text{t})) \]

但是意思没有前一个版本直接，可读性会下降一点，故我们还是使用前一个版本。

证明上述的一致性成立：

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

如果\( \text{t} = \text{y} \)，即\( \text{t} \)为变量：

1. 如果\( \text{x} = \text{y} \)，则 \[ \begin{aligned} &[\text{x} \mapsto \text{s}](\text{t}) \\ &= [\text{x} \mapsto \text{s}](\text{y}) \\ &= [\text{x} \mapsto \text{s}](\text{x}) \\ &= \text{s} \end{aligned} \] 进而 \[ \begin{aligned} &\text{等式左边} \\ &= \mathit{removenames}_{\Gamma}([\text{x} \mapsto \text{s}](\text{t})) \\ &= \mathit{removenames}_{\Gamma}(\text{s}) \end{aligned} \] 接着我们考虑等式右边 \[ \begin{aligned} &\mathit{removenames}_{\Gamma}(\text{t}) \\ &= \mathit{removenames}_{\Gamma}(\text{y}) \\ &= \Gamma(\text{y}) \end{aligned} \] 这里由于\( \text{x} = \text{y} \)，因此\( \Gamma(\text{y}) = \Gamma(\text{x}) \)，进而 \[ \begin{aligned} &\text{等式右边} \\ &= [\Gamma(\text{x}) \mapsto \mathit{removenames}_{\Gamma}(\text{s})](\mathit{removenames}_{\Gamma}(\text{t})) \\ &= [\Gamma(\text{x}) \mapsto \mathit{removenames}_{\Gamma}(\text{s})](\Gamma(\text{y})) \\ &= [\Gamma(\text{x}) \mapsto \mathit{removenames}_{\Gamma}(\text{s})](\Gamma(\text{x})) \\ &= \mathit{removenames}_{\Gamma}(\text{s}) \\ &= \text{等式左边} \end{aligned} \]
2. 如果\( \text{x} \neq \text{y} \)，则 \[ \begin{aligned} &[\text{x} \mapsto \text{s}](\text{t}) \\ &= [\text{x} \mapsto \text{s}](\text{y}) \\ &= \text{y} \end{aligned} \] 进而 \[ \begin{aligned} &\text{等式左边} \\ &= \mathit{removenames}_{\Gamma}([\text{x} \mapsto \text{s}](\text{t})) \\ &= \mathit{removenames}_{\Gamma}(\text{y}) \\ &= \Gamma(\text{y}) \end{aligned} \] 接着我们考虑等式右边 \[ \begin{aligned} &\mathit{removenames}_{\Gamma}(\text{t}) \\ &= \mathit{removenames}_{\Gamma}(\text{y}) \\ &= \Gamma(\text{y}) \end{aligned} \] 加上\( \text{x} \neq \text{y} \)，可得\( \Gamma(\text{x}) \neq \Gamma(\text{y}) \)，综合可得 \[ \begin{aligned} &\text{等式右边} \\ &= [\Gamma(\text{x}) \mapsto \mathit{removenames}_{\Gamma}(\text{s})](\mathit{removenames}_{\Gamma}(\text{t})) \\ &= [\Gamma(\text{x}) \mapsto \mathit{removenames}_{\Gamma}(\text{s})](\Gamma(\text{y})) \\ &= \Gamma(\text{y}) \\ &= \text{等式左边} \end{aligned} \]

如果\( \text{t} = \lambda \text{y. } \text{t}_1 \)，此时如果\( \text{x} = \text{y} \)，则根据约定5.3.4，我们可以对\( \lambda \text{y. } \text{t}_1 \)中的绑定变量\( \text{y} \)进行改名（注：改名过程需要保证一致性，函数体\( \text{t}_1 \)中所有引用到最外层绑定变量\( \text{y} \)的都得被改名），故我们可以安全地假设\( \text{x} \neq \text{y} \)，同理，由于绑定变量可以随便改名，故我们也可以安全地假设\( \text{y} \notin FV(\text{s}) \)，此时可得 \[ \begin{aligned} &[\text{x} \mapsto \text{s}](\text{t}) \\ &= [\text{x} \mapsto \text{s}](\lambda \text{y. } \text{t}_1) \\ &= \lambda \text{y. } ([\text{x} \mapsto \text{s}](\text{t}_1)) \end{aligned} \] 根据归纳假设，可得 \[ \begin{aligned} &\mathit{removenames}_{\Gamma, \text{y}}([\text{x} \mapsto \text{s}](\text{t}_1)) \\ &= [(\Gamma, \text{y})(\text{x}) \mapsto \mathit{removenames}_{\Gamma, \text{y}}(\text{s})](\mathit{removenames}_{\Gamma, \text{y}}(\text{t}_1)) \end{aligned} \] 进而可得 \[ \begin{aligned} &\text{等式左边} \\ &= \mathit{removenames}_{\Gamma}([\text{x} \mapsto \text{s}](\text{t})) \\ &= \mathit{removenames}_{\Gamma}(\lambda \text{y. } ([\text{x} \mapsto \text{s}](\text{t}_1))) \\ &= \lambda \text{. } (\mathit{removenames}_{\Gamma, \text{y}}([\text{x} \mapsto \text{s}](\text{t}_1))) \\ &= \lambda \text{. } ([(\Gamma, \text{y})(\text{x}) \mapsto \mathit{removenames}_{\Gamma, \text{y}}(\text{s})](\mathit{removenames}_{\Gamma, \text{y}}(\text{t}_1))) \end{aligned} \] 接着我们考虑等式右边 \[ \begin{aligned} &\mathit{removenames}_{\Gamma}(\text{t}) \\ &= \mathit{removenames}_{\Gamma}(\lambda \text{y. } \text{t}_1) \\ &= \lambda \text{. } \mathit{removenames}_{\Gamma, \text{y}}(\text{t}_1) \end{aligned} \] 进而可得 \[ \begin{aligned} &\text{等式右边} \\ &= [\Gamma(\text{x}) \mapsto \mathit{removenames}_{\Gamma}(\text{s})](\mathit{removenames}_{\Gamma}(\text{t})) \\ &= [\Gamma(\text{x}) \mapsto \mathit{removenames}_{\Gamma}(\text{s})](\lambda \text{. } \mathit{removenames}_{\Gamma, \text{y}}(\text{t}_1)) \\ &= \lambda \text{. } ([\Gamma(\text{x}) + 1 \mapsto \uparrow^1(\mathit{removenames}_{\Gamma}(\text{s}))](\mathit{removenames}_{\Gamma, \text{y}}(\text{t}_1))) \end{aligned} \] 这里为了证明\( \text{等式左边} = \text{等式右边} \)，我们希望证明如下等式 \[ \begin{aligned} &[(\Gamma, \text{y})(\text{x}) \mapsto \mathit{removenames}_{\Gamma, \text{y}}(\text{s})](\mathit{removenames}_{\Gamma, \text{y}}(\text{t}_1)) \\ &= [\Gamma(\text{x}) + 1 \mapsto \uparrow^1(\mathit{removenames}_{\Gamma}(\text{s}))](\mathit{removenames}_{\Gamma, \text{y}}(\text{t}_1)) \end{aligned} \] 根据\( \Gamma, \text{y} \)的定义，很容易得到\( (\Gamma, \text{y})(\text{x}) = \Gamma(\text{x}) + 1 \)，加上直觉上\( \uparrow^1(\mathit{removenames}_{\Gamma}(\text{s})) \)也\( = \mathit{removenames}_{\Gamma, \text{y}}(\text{s}) \)，因此直觉上，上述等式是成立的，但是我们得严格证明这点，为此，我们插入一个引理的证明。

引理1：

给定变量名\( \text{x} \)、对应的代入项\( \text{s} \)以及被代入项\( \text{t} \)，再给定一个命名上下文\( \Gamma \)，要求\( FV(\text{t}) \subseteq dom(\Gamma), x \in dom(\Gamma) \)，最后给定一个额外插入命名上下文的变量名\( \text{y} \)，我们断言如下等式成立：

\[ \begin{aligned} &[(\Gamma, \text{y})(\text{x}) \mapsto \mathit{removenames}_{\Gamma, \text{y}}(\text{s})](\mathit{removenames}_{\Gamma, \text{y}}(\text{t})) \\ &= [\Gamma(\text{x}) + 1 \mapsto \uparrow^1(\mathit{removenames}_{\Gamma}(\text{s}))](\mathit{removenames}_{\Gamma, \text{y}}(\text{t})) \end{aligned} \]

证明引理1：

我们只要证明\( (\Gamma, \text{y})(\text{x}) = \Gamma(\text{x}) + 1 \) 以及\( \mathit{removenames}_{\Gamma, \text{y}}(\text{s}) = \uparrow^1(\mathit{removenames}_{\Gamma}(\text{s})) \)即可。

根据\( \Gamma, \text{y} \)的定义，可得\( (\Gamma, \text{y})(\text{x}) = \Gamma(\text{x}) + 1 \)。

我们用结构归纳法证明\( \mathit{removenames}_{\Gamma, \text{y}}(\text{s}) = \uparrow^1(\mathit{removenames}_{\Gamma}(\text{s})) \)，归纳假设等式对\( \text{s} \)的直接子项均成立，我们要证明等式对\( \text{s} \)成立，对\( \text{s} \)的形式进行分类讨论：

1. 如果\( \text{s} = \text{z} \)，即\( \text{s} \)为变量，则 \[ \begin{aligned} &\text{等式左边} \\ &= \mathit{removenames}_{\Gamma, \text{y}}(\text{s}) \\ &= \mathit{removenames}_{\Gamma, \text{y}}(\text{z}) \\ &= (\Gamma, \text{y})(\text{z}) \end{aligned} \] 而 \[ \begin{aligned} &\text{等式右边} \\ &= \uparrow^1(\mathit{removenames}_{\Gamma}(\text{s})) \\ &= \uparrow^1(\mathit{removenames}_{\Gamma}(\text{z})) \\ &= \uparrow^1(\Gamma(\text{z})) \\ &= \Gamma(\text{z}) + 1 \\ &= (\Gamma, \text{y})(\text{z}) \\ &= \text{等式左边} \end{aligned} \]
2. 如果\( \text{s} = \lambda \text{w. } \text{s}_1 \)，则根据归纳假设，可得 \[ \begin{aligned} & \mathit{removenames}_{\Gamma, \text{y}, \text{w}}(\text{s}_1) \\ &= \uparrow^1(\mathit{removenames}_{\Gamma, \text{y}}(\text{s}_1)) \end{aligned} \] 再次根据归纳假设，可得 \[ \begin{aligned} & \mathit{removenames}_{\Gamma, \text{y}}(\text{s}_1) \\ &= \uparrow^1(\mathit{removenames}_{\Gamma}(\text{s}_1)) \end{aligned} \] 进而可得 \[ \begin{aligned} &\text{等式左边} \\ &= \mathit{removenames}_{\Gamma, \text{y}}(\text{s}) \\ &= \mathit{removenames}_{\Gamma, \text{y}}(\lambda \text{w. } \text{s}_1) \\ &= \lambda \text{. } (\mathit{removenames}_{\Gamma, \text{y}, \text{w}}(\text{s}_1)) \\ &= \lambda \text{. } (\uparrow^1(\mathit{removenames}_{\Gamma, \text{y}}(\text{s}_1))) \\ &= \lambda \text{. } (\uparrow^1(\uparrow^1(\mathit{removenames}_{\Gamma}(\text{s}_1)))) \end{aligned} \] 再次根据归纳假设，可得 \[ \begin{aligned} & \mathit{removenames}_{\Gamma, \text{w}}(\text{s}_1) \\ &= \uparrow^1(\mathit{removenames}_{\Gamma}(\text{s}_1)) \end{aligned} \] 于是可得 \[ \begin{aligned} &\text{等式右边} \\ &= \uparrow^1(\mathit{removenames}_{\Gamma}(\text{s})) \\ &= \uparrow^1(\mathit{removenames}_{\Gamma}(\lambda \text{w. } \text{s}_1)) \\ &= \uparrow^1(\lambda \text{. } (\mathit{removenames}_{\Gamma, \text{w}}(\text{s}_1))) \\ &= \lambda \text{. } \text{ } (\uparrow^1_1(\mathit{removenames}_{\Gamma, \text{w}}(\text{s}_1))) \\ &= \lambda \text{. } \text{ } (\uparrow^1_1(\uparrow^1(\mathit{removenames}_{\Gamma}(\text{s}_1)))) \end{aligned} \] 由于先位移\( 1 \)后再设置个位移下限\( c = 1 \)等于没设置下限，故易证 \[ \begin{aligned} &\uparrow^1(\uparrow^1(\mathit{removenames}_{\Gamma}(\text{s}_1))) \\ &= \uparrow^1_1(\uparrow^1(\mathit{removenames}_{\Gamma}(\text{s}_1))) \end{aligned} \] 于是可得\( \text{等式左边} = \text{等式右边} \)。
3. 如果\( \text{s} = \text{s}_1 \text{ } \text{s}_2 \)，则根据归纳假设，可得 \[ \begin{aligned} & \mathit{removenames}_{\Gamma, \text{y}}(\text{s}_1) \\ &= \uparrow^1(\mathit{removenames}_{\Gamma}(\text{s}_1)) \\ &\mathit{removenames}_{\Gamma, \text{y}}(\text{s}_2) \\ &= \uparrow^1(\mathit{removenames}_{\Gamma}(\text{s}_2)) \end{aligned} \] 进而可得 \[ \begin{aligned} &\text{等式左边} \\ &= \mathit{removenames}_{\Gamma, \text{y}}(\text{s}) \\ &= \mathit{removenames}_{\Gamma, \text{y}}(\text{s}_1 \text{ } \text{s}_2) \\ &= \mathit{removenames}_{\Gamma, \text{y}}(\text{s}_1) \text{ } \mathit{removenames}_{\Gamma, \text{y}}(\text{s}_2) \\ &= \uparrow^1(\mathit{removenames}_{\Gamma}(\text{s}_1)) \text{ } \uparrow^1(\mathit{removenames}_{\Gamma}(\text{s}_2)) \end{aligned} \] 而 \[ \begin{aligned} &\text{等式右边} \\ &= \uparrow^1(\mathit{removenames}_{\Gamma}(\text{s})) \\ &= \uparrow^1(\mathit{removenames}_{\Gamma}(\text{s}_1 \text{ } \text{s}_2)) \\ &= \uparrow^1(\mathit{removenames}_{\Gamma}(\text{s}_1) \text{ } \mathit{removenames}_{\Gamma}(\text{s}_2)) \\ &= \uparrow^1(\mathit{removenames}_{\Gamma}(\text{s}_1)) \text{ } \uparrow^1(\mathit{removenames}_{\Gamma}(\text{s}_2)) \\ &= \text{等式左边} \end{aligned} \]

综上，归纳完毕，有\( \mathit{removenames}_{\Gamma, \text{y}}(\text{s}) = \uparrow^1(\mathit{removenames}_{\Gamma}(\text{s})) \)。

证明引理1完毕。

继续回到前面的证明，根据引理1，可得 \[ \begin{aligned} &[(\Gamma, \text{y})(\text{x}) \mapsto \mathit{removenames}_{\Gamma, \text{y}}(\text{s})](\mathit{removenames}_{\Gamma, \text{y}}(\text{t}_1)) \\ &= [\Gamma(\text{x}) + 1 \mapsto \uparrow^1(\mathit{removenames}_{\Gamma}(\text{s}))](\mathit{removenames}_{\Gamma, \text{y}}(\text{t}_1)) \end{aligned} \] 进而可得 \[ \begin{aligned} &\text{等式左边} \\ &= \lambda \text{. } ([(\Gamma, \text{y})(\text{x}) \mapsto \mathit{removenames}_{\Gamma, \text{y}}(\text{s})](\mathit{removenames}_{\Gamma, \text{y}}(\text{t}_1))) \\ &= \lambda \text{. } ([\Gamma(\text{x}) + 1 \mapsto \uparrow^1(\mathit{removenames}_{\Gamma}(\text{s}))](\mathit{removenames}_{\Gamma, \text{y}}(\text{t}_1))) \\ &= \text{等式右边} \end{aligned} \]

如果\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)，则 \[ \begin{aligned} &[\text{x} \mapsto \text{s}](\text{t}) \\ &= [\text{x} \mapsto \text{s}](\text{t}_1 \text{ } \text{t}_2) \\ &= ([\text{x} \mapsto \text{s}](\text{t}_1)) \text{ } ([\text{x} \mapsto \text{s}](\text{t}_2)) \end{aligned} \] 根据归纳假设，可得 \[ \begin{aligned} &\mathit{removenames}_{\Gamma}([\text{x} \mapsto \text{s}](\text{t}_1)) \\ &= [\Gamma(\text{x}) \mapsto \mathit{removenames}_{\Gamma}(\text{s})](\mathit{removenames}_{\Gamma}(\text{t}_1)) \\ &\mathit{removenames}_{\Gamma}([\text{x} \mapsto \text{s}](\text{t}_2)) \\ &= [\Gamma(\text{x}) \mapsto \mathit{removenames}_{\Gamma}(\text{s})](\mathit{removenames}_{\Gamma}(\text{t}_2)) \end{aligned} \] 进而可得 \[ \begin{aligned} &\text{等式左边} \\ &= \mathit{removenames}_{\Gamma}([\text{x} \mapsto \text{s}](\text{t})) \\ &= \mathit{removenames}_{\Gamma}(([\text{x} \mapsto \text{s}](\text{t}_1)) \text{ } ([\text{x} \mapsto \text{s}](\text{t}_2))) \\ &= \mathit{removenames}_{\Gamma}([\text{x} \mapsto \text{s}](\text{t}_1)) \text{ } \mathit{removenames}_{\Gamma}([\text{x} \mapsto \text{s}](\text{t}_2)) \\ &= [\Gamma(\text{x}) \mapsto \mathit{removenames}_{\Gamma}(\text{s})](\mathit{removenames}_{\Gamma}(\text{t}_1)) \\ &\quad [\Gamma(\text{x}) \mapsto \mathit{removenames}_{\Gamma}(\text{s})](\mathit{removenames}_{\Gamma}(\text{t}_2)) \end{aligned} \] 接着我们考虑等式右边 \[ \begin{aligned} &\mathit{removenames}_{\Gamma}(\text{t}) \\ &= \mathit{removenames}_{\Gamma}(\text{t}_1 \text{ } \text{t}_2) \\ &= \mathit{removenames}_{\Gamma}(\text{t}_1) \text{ } \mathit{removenames}_{\Gamma}(\text{t}_2) \end{aligned} \] 进而可得 \[ \begin{aligned} &\text{等式右边} \\ &= [\Gamma(\text{x}) \mapsto \mathit{removenames}_{\Gamma}(\text{s})](\mathit{removenames}_{\Gamma}(\text{t})) \\ &= [\Gamma(\text{x}) \mapsto \mathit{removenames}_{\Gamma}(\text{s})](\mathit{removenames}_{\Gamma}(\text{t}_1) \text{ } \mathit{removenames}_{\Gamma}(\text{t}_2)) \\ &= [\Gamma(\text{x}) \mapsto \mathit{removenames}_{\Gamma}(\text{s})](\mathit{removenames}_{\Gamma}(\text{t}_1)) \\ &\quad [\Gamma(\text{x}) \mapsto \mathit{removenames}_{\Gamma}(\text{s})](\mathit{removenames}_{\Gamma}(\text{t}_2)) \\ &= \text{等式左边} \end{aligned} \]

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

证毕。

章节6.3

练习6.3.1

题目：

Should we be worried that the negative shift in this rule might create ill-formed terms containing negative indices?

解答：

不需要担心，最简单的，可以使用勘误后的练习6.2.5，如下：

针对\( (\lambda \text{. } \text{t}_{12}) \text{v}_2 \rightarrow \uparrow^{-1}([0 \mapsto \uparrow^1(\text{v}_2)]\text{t}_{12}) \)，假设\( [0 \mapsto \uparrow^1(\text{v}_2)]\text{t}_{12} \)为\( n \)-项（\( n \in \mathbf{N} \)），则根据练习6.2.5中\( d < 0 \)的情况，可得\( \uparrow^{-1}([0 \mapsto \uparrow^1(\text{v}_2)]\text{t}_{12}) \)为 \( (\max(n - 1, 0, 0) = \max(n - 1, 0)) \)-项，不会包含非法的负下标/数字。

更直接的，不用练习6.2.5，则由于\( [0 \mapsto \uparrow^1(\text{v}_2)]\text{t}_{12} \)把\( \text{t}_{12} \)中最外层对\( 0 \)的引用改成了\( \uparrow^1(\text{v}_2) \)，而\( \uparrow^1(\text{v}_2) \)中所有自由变量\( 0 \)都已经被变成\( 1 \)了，加上\( \text{t}_{12} \)内层对最外层绑定变量的引用数字都不会是\( 0 \) （\( 0 \)引用的会是当前层的绑定变量，而不是最外层的绑定变量），再加上\( \uparrow^{-1} \)每移入一层\( \lambda \)-抽象，位移下限\( \text{c} \)都会\( + 1 \)，不会\( = 0 \)，因此内层的\( 0 \)都不会被修改。综上，\( \uparrow^{-1}([0 \mapsto \uparrow^1(\text{v}_2)]\text{t}_{12}) \)不会得到负下标/数字。

练习6.3.2

题目：

De Bruijn’s original article actually contained two different proposals for nameless representations of terms: the deBruijn indices presented here, which number lambda-binders “from the inside out,” and deBruijn levels, which number binders “from the outside in.” For example, the term \( \lambda \text{x. } (\lambda \text{y. } \text{x y}) \text{ x} \) is represented using deBruijn indices as \( \lambda \text{. } (\lambda \text{. } \text{1 0}) \text{ 0} \) and using deBruijn levels as \( \lambda \text{. } (\lambda \text{. } \text{0 1}) \text{ 0} \). Define this variant precisely and show that the representations of a term using indices and levels are isomorphic (i.e., each can be recovered uniquely from the other).

解答：

在给出相关的定义之前，需要注意下，deBruijn levels中，外层项是不应该允许访问内层\( \lambda \)-抽象的绑定变量的，即\( \lambda \text{. } 1 \text{ } (\lambda \text{. } 1) \)应该是非法的，这里外层的\( 1 \)访问了内层\( \lambda \)-抽象的绑定变量，然而内层绑定变量的作用域应该是不包含外层的\( 1 \)的位置的。除此之外，deBruijn levels还需要允许负level，比如deBruijn indices中的项 \( \text{1 0 } (\lambda \text{. } \text{0}) \)在deBruijn levels中对应的项就应该是 \( \text{-2 -1 } (\lambda \text{. } \text{0}) \)。

接着我们想给出deBruijn levels对应的定义6.1.2，思考下会发现有额外要考虑的东西，deBruijn indices针对“在外层包个\( \lambda \)-抽象”的操作，在包完\( \lambda \)-抽象后，项的数字会保持不变，比如对deBruijn indices的\( \text{0 } (\lambda \text{. } 0) \)外层包个\( \lambda \)-抽象会变成\( \lambda \text{. } \text{0 } (\lambda \text{. } 0) \)，这里两个数字\( 0 \)都不需要改变，都访问了正确的绑定者，但是deBruijn levels就不能这样了，比如对deBruijn levels的\( \text{-1 } (\lambda \text{. } 0) \)外层包个\( \lambda \)-抽象需要变成\( \lambda \text{. } \text{0 } (\lambda \text{. } 1) \)，原本的两个数字\( -1, 0 \)都需要\( + 1 \)，结论就是不同于deBruijn indices，deBruijn levels在给出对应定义6.1.2的定义之前就需要定义位移的操作了，不过不同于deBruijn indices的位移操作，我们的位移操作没有cutoff参数\( \text{c} \)，故我们改用符号\( \Uparrow \)，而不用\( \uparrow \)（不过符号\( \uparrow \)等下会用于定义另外一个有cutoff的位移操作，不过cutoff机制跟deBruijn indices的不同），如下：

定义6.3.2.1（无条件位移）：

The unconditional \( d \)-place shift of a term \( \text{t} \), written \( \Uparrow^d(\text{t}) \), is defined as follows:

1. \( \Uparrow^d(k) = k + d \)
2. \( \Uparrow^d(\lambda \text{. } \text{t}_1) = \lambda \text{. } \Uparrow^d(\text{t}_1) \)
3. \( \Uparrow^d(\text{t}_1 \text{ } \text{t}_2) = \Uparrow^d(\text{t}_1) \text{ } \Uparrow^d(\text{t}_2) \)

定义完毕。

下面我们就可以给出deBruijn levels对应定义6.1.2的定义了：

定义6.3.2.2（项）：

Let \( \mathcal{T} \) be the smallest family of sets \( \{ \mathcal{T}_0, \mathcal{T}_1, \dots \} \) such that

1. \( k \in \mathcal{T}_n \) whenever \( -n \leq k \leq -1 \);
2. if \( \text{t}_1 \in \mathcal{T}_n \) and \( n > 0 \), then \( (\lambda \text{. } \Uparrow^1(\text{t}_1)) \in \mathcal{T}_{n - 1} \);
3. if \( \text{t}_1 \in \mathcal{T}_n \) and \( \text{t}_2 \in \mathcal{T}_n \), then \( (\text{t}_1 \text{ } \text{t}_2) \in \mathcal{T}_n \).

The elements of each \( \mathcal{T}_n \) are called \( n \)-terms.

定义完毕。

容易证明上述定义中的所有项均不允许外层子项访问内层\( \lambda \)-抽象的变量（读者可以思考下为什么非法项\( \lambda \text{. } 1 \text{ } (\lambda \text{. } 1) \)不符合上述定义）。

考虑下根据上述定义，怎么得到\( \lambda \text{. } \text{0 } (\lambda \text{. } \text{1 } (\lambda \text{. } \text{0 2 -1})) \)为\( 1 \)-项呢？根据上述定义的1，可得\( -3 \)、\( -1 \)、\( -4 \)均为\( 4 \)-项，进而根据上述定义的2，可得\( \lambda \text{. } \text{-2 0 -3} \)为\( 3 \)-项，再次根据上述定义的1，可得\( -1 \)为\( 3 \)-项，进而根据上述定义的2以及\( \lambda \text{. } \text{-2 0 -3} \)为\( 3 \)-项，可得\( \lambda \text{. } \text{0 } (\lambda \text{. } \text{-1 1 -2}) \)为\( 2 \)-项，再次根据上述定义的1，可得\( -1 \)为\( 2 \)-项，进而根据上述定义的2以及\( \lambda \text{. } \text{0 } (\lambda \text{. } \text{-1 1 -2}) \)为\( 2 \)-项，可得\( \lambda \text{. } \text{0 } (\lambda \text{. } \text{1 } (\lambda \text{. } \text{0 2 -1})) \)为\( 1 \)-项。

继续考虑如何定义deBruijn levels的变量代入，与deBruijn indices的关键不同点在于\( \lambda \)-抽象的处理，即定义6.2.4的第二项，由于是从外到内数level的，因此不同于deBruijn indices，代入直接子项\( \text{t}_1 \)时， \( j \)不需要\( + 1 \)，\( \text{s} \)则非自由变量需要被位移\( 1 \)，自由变量则不用位移，举个例子，令\( j = 0, \text{s} = \lambda \text{. } \text{0 -1 -2 } (\lambda \text{. } \text{0 1 -3 -4}), \text{t} = \lambda \text{. } 0 \)，则我们希望\( [j \mapsto \text{s}]\text{t} = \lambda \text{. } (\lambda \text{. } \text{1 -1 -2 } (\lambda \text{. } \text{1 2 -3 -4})) \)，即将\( \text{s} \)代入到\( \text{t} \)后，\( \text{s} \)中的所有绑定变量仍然引用到了正确的绑定者，且所有自由变量仍然保持为自由变量（没有被意外捕获），同时自由变量的level也不能变（考虑下如果自由变量\( -1 \)变\( -2 \)了，则\( -1 \)根据定义6.3.2.2包一个\( \lambda \)-抽象就能变成绑定变量， \( -2 \)则根据定义6.3.2.2要包两个\( \lambda \)-抽象才能变成绑定变量，两者行为不同，故自由变量\( -1 \)不能随便改成自由变量\( -2 \)）。由于代入后\( \text{s} \)是被移深入一层\( \lambda \)-抽象的，故所有绑定变量\( + 1 \)就能确保代入后绑定变量仍然引用到了正确的绑定者，而自由变量会全部\( < 0 \)（读者可以思考下为什么不可能出现数字为非负数的自由变量），故我们可以定义一个新的位移操作，令cutoff \( c = 0 \)，且要求\( < c = 0 \)时进行位移，这样就能保证自由变量不被改变，这里不同于deBruijn indices是\( \geq c \)时发生位移，我们这里的\( c \)应该叫位移上限，而deBruijn indices的\( c \)应该叫位移下限。新的位移操作的定义如下（由于位移上限一直都是\( 0 \)，故我们不需要额外的参数\( \text{c} \)）：

定义6.3.2.3（有条件位移）：

The conditional \( d \)-place shift of a term \( \text{t} \), written \( \uparrow^d(\text{t}) \), is defined as follows:

1. \( \uparrow^d(k) = \begin{cases} k &\text{if } k \geq 0 \\ k + d &\text{if } k < 0 \end{cases} \)
2. \( \uparrow^d(\lambda \text{. } \text{t}_1) = \lambda \text{. } \uparrow^d(\text{t}_1) \)
3. \( \uparrow^d(\text{t}_1 \text{ } \text{t}_2) = \uparrow^d(\text{t}_1) \text{ } \uparrow^d(\text{t}_2) \)

定义完毕。

现在，我们可以定义变量代入了，如下：

定义6.3.2.4（变量代入）：

The substitution of a term \( \text{s} \) for variable number \( j \) in a term \( \text{t} \), written \( [j \mapsto \text{s}]\text{t} \), is defined as follows:

1. \( [j \mapsto \text{s}]k = \begin{cases} \text{s} &\text{if } k = j \\ k &\text{otherwise} \end{cases} \)
2. \( [j \mapsto \text{s}](\lambda \text{. } \text{t}_1) = \lambda \text{. } [j \mapsto \uparrow^1(\text{s})]\text{t}_1 \)
3. \( [j \mapsto \text{s}](\text{t}_1 \text{ } \text{t}_2) = [j \mapsto \text{s}]\text{t}_1 \text{ } [j \mapsto \text{s}]\text{t}_2 \)

定义完毕。

举个例子，令\( j = 0, \text{s} = \lambda \text{. } \text{0 -1 -2 } (\lambda \text{. } \text{0 1 -3 -4}), \text{t} = \lambda \text{. } 0 \)，则 \[ \begin{aligned} &[j \mapsto \text{s}]\text{t} \\ &= [0 \mapsto \text{s}](\lambda \text{. } 0) \\ &= \lambda \text{. } ([0 \mapsto \uparrow^1(\text{s})](0)) \\ &= \lambda \text{. } ([0 \mapsto \uparrow^1(\lambda \text{. } \text{0 -1 -2 } (\lambda \text{. } \text{0 1 -3 -4}))](0)) \\ &= \lambda \text{. } ([0 \mapsto \lambda \text{. } \text{1 -1 -2 } (\lambda \text{. } \text{1 2 -3 -4})](0)) \\ &= \lambda \text{. } (\lambda \text{. } \text{1 -1 -2 } (\lambda \text{. } \text{1 2 -3 -4})) \end{aligned} \]

接着，我们定义求值规则，除了E-APPABS外的其他规则都和图5-3一样，规则E-APPABS和deBruijn indices一样需要额外考虑求值后\( \lambda \)-抽象消失的问题，故针对\( (\lambda \text{. } \text{t}_1) \text{ } \text{v}_2 \)的求值，我们分阶段处理：

1. 首先不考虑\( \lambda \)-抽象消失的问题，直接\( \text{v}_2 \)作为\( 0 \)代入函数体\( \text{t}_1 \)，这里由于\( \text{v}_2 \)移深入了一层\( \lambda \)-抽象，故需要用定义6.3.2.3对\( \text{v}_2 \)进行位移，即\( [0 \mapsto \uparrow^1(\text{v}_2)]\text{t}_1 \)。
2. 接着，即代入后，我们继续考虑\( \lambda \)-抽象消失的问题，由于少了一层\( \lambda \)-抽象，故第一步的结果项\( [0 \mapsto \uparrow^1(\text{v}_2)]\text{t}_1 \)中的绑定变量均需要位移\( - 1 \)，自由变量则同样不位移，故还是使用定义6.3.2.3对结果项进行位移，只不过这次位移量是\( -1 \)，即\( \uparrow^{-1}([0 \mapsto \uparrow^1(\text{v}_2)]\text{t}_1) \)。

综上，完整的求值规则如下：

定义6.3.2.5（求值规则）：

\[ \begin{aligned} \dfrac{\text{t}_1 \rightarrow \text{t}'_1}{\text{t}_1 \text{ } \text{t}_2 \rightarrow \text{t}'_1 \text{ } \text{t}_2} &\qquad (\text{E-APP1}) \\ \dfrac{\text{t}_2 \rightarrow \text{t}'_2}{\text{v}_1 \text{ } \text{t}_2 \rightarrow \text{v}_1 \text{ } \text{t}'_2} &\qquad (\text{E-APP2}) \\ (\lambda \text{. } \text{t}_1) \text{ } \text{v}_2 \rightarrow \uparrow^{-1}([0 \mapsto \uparrow^1(\text{v}_2)]\text{t}_1) &\qquad (\text{E-APPABS}) \end{aligned} \]

定义完毕。

举个例子，令\( \text{t} = (\lambda \text{. } 0) \text{ } (\lambda \text{. } \text{0 -1 -2 } (\lambda \text{. } \text{0 1 -3 -4})) \)，则 \[ \begin{aligned} &\uparrow^{-1}([0 \mapsto \uparrow^1(\lambda \text{. } \text{0 -1 -2 } (\lambda \text{. } \text{0 1 -3 -4}))](0)) \\ &= \uparrow^{-1}([0 \mapsto \lambda \text{. } \text{1 -1 -2 } (\lambda \text{. } \text{1 2 -3 -4})](0)) \\ &= \uparrow^{-1}(\lambda \text{. } \text{1 -1 -2 } (\lambda \text{. } \text{1 2 -3 -4})) \\ &= \lambda \text{. } \text{0 -1 -2 } (\lambda \text{. } \text{0 1 -3 -4}) \end{aligned} \]

接下来，我们定义deBruijn indices和deBruijn levels间的转换方法，先定义deBruijn indices到deBruijn levels的转换\( \mathcal{deBruijnI2L} \)，如下：

定义6.3.2.6（deBruijn indices转deBruijn levels）：

Given a deBruijn indices term \( \text{t} \), we define \( \mathcal{deBruijnI2L}(\text{t}) \), as follows:

1. \( \mathcal{deBruijnI2L}(k) = -k - 1 \)
2. \( \mathcal{deBruijnI2L}(\lambda \text{. } \text{t}_1) = \lambda \text{. } \Uparrow^1(\mathcal{deBruijnI2L}(\text{t}_1)) \)
3. \( \mathcal{deBruijnI2L}(\text{t}_1 \text{ } \text{t}_2) = \mathcal{deBruijnI2L}(\text{t}_1) \text{ } \mathcal{deBruijnI2L}(\text{t}_2) \)

定义完毕。

举个例子：

\[ \begin{aligned} &\mathcal{deBruijnI2L}(\lambda \text{. } \text{0 1}) \\ &= \lambda \text{. } \Uparrow^1(\mathcal{deBruijnI2L}(\text{0 1})) \\ &= \lambda \text{. } \Uparrow^1(\mathcal{deBruijnI2L}(0) \text{ } \mathcal{deBruijnI2L}(1)) \\ &= \lambda \text{. } \Uparrow^1(\text{-1 -2}) \\ &= \lambda \text{. } \text{0 -1} \end{aligned} \]

继续定义deBruijn levels到deBruijn indices的转换\( \mathcal{deBruijnL2I} \)，不过再在之前，需要额外定义deBruijn indices的无条件位移：

定义6.3.2.7（deBruijn indices的无条件位移）：

同定义6.3.2.1。

定义完毕。

定义6.3.2.8（deBruijn levels转deBruijn indices）：

Given a deBruijn levels term \( \text{t} \), we define \( \mathcal{deBruijnL2I}(\text{t}) \), as follows:

1. \( \mathcal{deBruijnL2I}(k) = -k - 1 \)
2. \( \mathcal{deBruijnL2I}(\lambda \text{. } \text{t}_1) = \lambda \text{. } \Uparrow^1(\mathcal{deBruijnL2I}(\text{t}_1)) \)
3. \( \mathcal{deBruijnL2I}(\text{t}_1 \text{ } \text{t}_2) = \mathcal{deBruijnL2I}(\text{t}_1) \text{ } \mathcal{deBruijnL2I}(\text{t}_2) \)

定义完毕。

举个例子：

\[ \begin{aligned} &\mathcal{deBruijnL2I}(\lambda \text{. } \text{0 -1}) \\ &= \lambda \text{. } \Uparrow^1(\mathcal{deBruijnL2I}(\text{0 -1})) \\ &= \lambda \text{. } \Uparrow^1(\mathcal{deBruijnL2I}(0) \text{ } \mathcal{deBruijnL2I}(-1)) \\ &= \lambda \text{. } \Uparrow^1(\text{-1 0}) \\ &= \lambda \text{. } \text{0 1} \end{aligned} \]

易证：

1. \( \forall \)deBruijn indices项\( \text{t} \)，有\( \mathcal{deBruijnL2I}(\mathcal{deBruijnI2L}(\text{t})) = \text{t} \)。
2. \( \forall \)deBruijn levels项\( \text{t} \)，有\( \mathcal{deBruijnI2L}(\mathcal{deBruijnL2I}(\text{t})) = \text{t} \)。

即deBruijn indices项和deBruijn levels项之间可以自由进行转换且转换是唯一的（双射），易定义deBruijn indices和deBruijn levels之间的同构映射函数，这说明两者是同构的。