无类型lambda演算的无名称表示与实现

### 无类型 lambda 演算的无名称表示与实现 #### 1. 无名称项的表示 在无类型 lambda 演算中，为了更方便地处理变量绑定和替换，引入了无名称表示法。 ##### 1.1 命名上下文与 De Bruijn 索引 假设 $x_0$ 到 $x_n$ 是来自集合 $V$ 的变量名。命名上下文 $\Gamma = x_n, x_{n - 1}, \cdots, x_1, x_0$ 为每个 $x_i$ 分配 De Bruijn 索引 $i$。注意，序列中最右边的变量索引为 0，这与将命名项转换为无名称形式时从右到左计数 $\lambda$ 绑定器的方式一致。我们用 $dom(\Gamma)$ 表示 $\Gamma$ 中提到的变量名集合 $\{x_n, \cdots, x_0\}$。 ##### 1.2 相关练习 - **练习 1**：以特定风格给出 $n$ - 项集合的另一种构造，并证明其与上述定义等价。 - **练习 2**： 1. 定义函数 $removenames_{\Gamma}(t)$，它接受命名上下文 $\Gamma$ 和普通项 $t$（其中 $FV(t) \subseteq dom(\Gamma)$），并生成相应的无名称项。 2. 定义函数 $restorenames_{\Gamma}(t)$，它接受无名称项 $t$ 和命名上下文 $\Gamma$，并生成普通项。这需要为 $t$ 中抽象绑定的变量“编造”名称。假设 $\Gamma$ 中的名称两两不同，且变量名集合 $V$ 是有序的，以便可以选择不在 $dom(\Gamma)$ 中的第一个变量名。这两个函数应满足：对于任何无名称项 $t$，$removenames_{\Gamma}(restorenames_{\Gamma}(t)) = t$；对于任何普通项 $t$，$restorenames_{\Gamma}(removenames_{\Gamma}(t)) = t$（至多重命名绑定变量）。 #### 2. 移位和替换 在无名称项上定义替换操作 $[k, s]t$ 之前，需要一个辅助操作“移位”，用于重新编号项中自由变量的索引。 ##### 2.1 移位操作 移位操作 $\uparrow_d^c(t)$ 定义如下： - $\uparrow_d^c(k) = \begin{cases} k, & \text{if } k < c \\ k + d, & \text{if } k \geq c \end{cases}$ - $\uparrow_d^c(\lambda.t_1) = \lambda.\uparrow_d^{c + 1}(t_1)$ - $\uparrow_d^c(t_1 t_2) = \uparrow_d^c(t_1) \uparrow_d^c(t_2)$ 我们用 $\uparrow_d(t)$ 表示 $\uparrow_d^0(t)$。 ##### 2.2 相关练习 - **练习 1**：计算 $\uparrow_2(\lambda.\lambda. 1 (0 2))$ 和 $\uparrow_2(\lambda. 0 1 (\lambda. 0 1 2))$。 - **练习 2**：证明如果 $t$ 是 $n$ - 项，则 $\uparrow_d^c(t)$ 是 $(n + d)$ - 项。 ##### 2.3 替换操作 项 $s$ 替换项 $t$ 中编号为 $j$ 的变量，记为 $[j, s]t$，定义如下： - $[j, s]k = \begin{cases} s, & \text{if } k = j \\ k, & \text{otherwise } \end{cases}$ - $[j, s](\lambda.t_1) = \lambda. [j + 1, \uparrow_1(s)]t_1$ - $[j, s](t_1 t_2) = ([j, s]t_1 [j, s]t_2)$ ##### 2.4 更多练习 - **练习 1**：假设全局上下文 $\Gamma = a, b$，将以下替换操作转换为无名称形式，并使用上述定义计算结果。检查答案是否与普通项替换的原始定义一致。 1. $[b, a] (b (\lambda x.\lambda y.b))$ 2. $[b, a (\lambda z.a)] (b (\lambda x.b))$ 3. $[b, a] (\lambda b. b a)$ 4. $[b, a] (\lambda a. b a)$ - **练习 2**：证明如果 $s$ 和 $t$ 是 $n$ - 项且 $j \leq n$，则 $[j, s]t$ 是 $n$ - 项。 - *