局部无名表示

为什么这里不用提升实参 ​

合法实参 u 中的索引都已由 u 自己的 λ 绑定；u 的外部引用全部是自由原子。把整个 u 放到另一个 λ 下面，其内部索引仍由原来的内部 λ 负责，自由原子又不会被无名 λ 绑定。因此开启可以直接放入 u，不必改变任何数字。

这依赖 ${\mathrm{lc}}_0(u)$。把有悬空 $\mathrm{bvar}(0)$ 的原始项当作 u 塞进一个 λ，0 会突然指向那个 λ；“局部无名不需要提升”不能脱离合法实参条件使用。若处理多个尚未打开的外层绑定器，需要更一般的操作或先把外层开启成新鲜原子，不能直接套本文单绑定器接口。

同一无捕获收缩，两种表示 ​

对 $(\lambda x.\lambda y.x)z$，表示为

开启外层函数体 $b=\lambda .\mathrm{bvar}(1)$ 时，进入内层 λ 后目标索引由 0 变成 1，于是得到 $\lambda .\mathrm{fvar}(z)$。没有先后提升，但仍然准确数过了绑定器。最后一项是常返回自由 z 的函数，不是恒等函数 $\lambda .\mathrm{bvar}(0)$。

不新鲜的关闭会合并两种来源 ​

令 $b=\mathrm{bvar}(0)\mathrm{fvar}(z)$。用新鲜 a 开启，得到 $\mathrm{fvar}(a)\mathrm{fvar}(z)$；再关闭 a，正好恢复 b。若改用已有自由原子 z 开启，则得到 $\mathrm{fvar}(z)\mathrm{fvar}(z)$，关闭 z 后变成 $\mathrm{bvar}(0)\mathrm{bvar}(0)$。第二个 z 原本自由，现在也被绑定了，所以第二条逆律的 freshness 条件不可省。

局部闭合的反例是 $\lambda .\mathrm{bvar}(1)$：内部深度只有 1，合法索引只能是 0。另一方面 $\lambda .\mathrm{fvar}(z)$ 虽含自由名，却局部闭合。把“局部闭合”翻译成“整个程序没有自由变量”，会错误排除后者并破坏开启操作的接口。

自由原子的替换 ​

将自由 a 替换为局部闭合 u 时，只改 $\mathrm{fvar}(a)$；遇到 λ 无须改名或提升，继续递归即可。以 $\lambda .(\mathrm{bvar}(0)\mathrm{fvar}(a))$ 为例，代入 $u=\lambda .\mathrm{bvar}(0)$ 得 $\lambda .(\mathrm{bvar}(0)(\lambda .\mathrm{bvar}(0)))$。两处 0 分别由各自最近的 λ 绑定，没有互相干扰。

逆律怎样证明，怎样用于绑定证明 ​

按树结构同时跟踪当前深度。自由原子分支直接判等；绑定索引分支检查是否等于当前开启深度；λ 分支将深度加一后使用归纳假设。第一条逆律中局部闭合保证原来没有“恰好指向将被新建的外层 λ”的悬空索引；第二条中 freshness 保证关闭时只找回刚开启的原子，而不误收旧的自由出现。这给出逆律条件的实际作用，不只是把条件列在公式旁。

在带绑定的归纳证明中，可以先选不在一个有限禁用集里的原子 a，把函数体开启成普通自由变量，再对开启项推理。文献还使用“除有限集合外所有 a”的余有限量化，使归纳假设能选择适合后续上下文的新鲜原子；这种组织方式让归纳假设有足够的新鲜名字可选，具体使用时仍须给出有限禁用集。[1, §4.2]

开启与关闭各遍历函数体一次。不可变树共享被放入的 u 时，开启有 B 个体节点的工作为 $O(B)$；若必须完整复制每处实参，含 q 个目标出现、实参大小 S 的结果需 $O(B+qS)$ 空间与构造时间。表示上的无提升减少了某类重编号工作，并不消除替换造成的结果增长。

迁移练习：把上例已有自由原子 z 改成 a，再尝试“总使用名字 a 开启”的实现。写出失败树，并改成从 $\mathrm{FV}(b)$ 以外选择原子。然后把实参换成悬空 $\mathrm{bvar}(0)$，检查接口应先拒绝，而非生成一个看似可用的捕获结果。终点任务提供两种逆律与非法参数的复算。