终点：把绑定与控制变成可检查的数据 ​

返回学习路线

这一组任务分别检查三个接口：变量还指向原来的绑定器吗，函数改成标签后还执行同样的计算吗，保存控制值后究竟返回到哪里。三组可以分别验收；它们共享“把隐含关系变成数据”的方法，不要求把每种技术硬接进同一条编译流水线。

先学习 de Bruijn 索引理路de Bruijn 索引De Bruijn indices · 德布鲁因索引用到绑定器的距离表示变量，并通过带截断深度的提升和替换，逐步检查 β 收缩没有捕获自由变量。、局部无名表示理路局部无名表示Locally nameless representation · 局部无名称表示用索引表示绑定变量、用原子表示自由变量，以局部闭合与开启关闭条件检查绑定操作的合法性。；第二组使用 去函数化理路去函数化Defunctionalization · 去函数变换把一个已知有限函数族变成标签与捕获字段，再用一阶分派器执行，并区分有限代码形状和任意多个运行时实例。、trampoline理路Trampoline 求值驱动Trampoline · Trampolining · 蹦床式求值让每次用户函数转移先返回一个延迟任务，由外层循环执行，逐项区分宿主调用栈、续延堆空间与实际计算步数。；第三组使用 call/cc理路一等续延与 call/ccFirst-class continuations · Call with current continuation · call/cc把当前剩余计算保存为可传递的值，精确区分普通返回、捕获和恢复时抛弃调用处续延的三种行为。 与 shift/reset理路分界续延与 shift/resetDelimited continuations · Shift and reset · 受限续延用最近的 reset 划定捕获范围，说明 shift 如何重新安装边界、组合式返回并多次恢复同一段纯计算。。命名语法的基础是 无捕获替换理路无捕获替换Capture-avoiding substitution用作用域感知的递归代入替换自由变量，同时保持代入项的自由变量不被捕获。，控制机的普通求值规则沿用 CEK理路CEK 抽象机CEK machine · Control Environment Kontinuation machine以控制项、词法环境和续延帧执行传值 λ 演算的环境式抽象机器。。

一、同一绑定关系的两种表示 ​

任务与核对 ​

在外部表 Γ=[z] 下处理 (λx.λy.x) z。完成以下四件事，再运行脚本核对。

1. 写出 de Bruijn 编码 (λ.λ.1) 0，说明两个数字各指哪里
2. 写出实参初始提升 0→1、穿过内层 λ 后变为 2、最终下降得到 λ.1 的过程
3. 写出局部无名编码 (λ.λ.b(1)) f(z)，开启后为 λ.f(z)
4. 将 de Bruijn 实现最初的提升删去，得到错误结果 λ.0，指出它变成了哪一个命名函数

在索引版本里，数字相同并不总是引用相同。例如 λ.0 中的 0 是内部绑定，而顶层 Γ=[z] 下的 0 是外部 z。良作用域检查必须知道当前深度，不能只检查索引非负。

局部无名版本还要检查逆律。取 b = b(0) f(z)，用新鲜 a 开启，再关闭 a，应还原 b。改用 z 开启再关闭，则两处 z 都变成 b(0)，无法还原。错误来自不同来源被合并，不能用“树看起来仍局部闭合”排除。

结构迁移 ​

把实参改成 λw.z，仍用 Γ=[z]。正确的 de Bruijn 结果是 λ.λ.2，局部无名结果是 λ.λ.f(z)。这次实参自身也有绑定器，不能机械地把实参中的每个数字都加一：cutoff 必须保护实参自己的绑定变量。

再把局部无名实参改成孤立 b(0)。安全开启接口应拒绝它，因为它有悬空绑定索引。请说明这一输入为何与合法的自由 f(z) 不同；只列出函数返回的某棵原始树不算通过。

二、函数标签与逐任务返回 ​

去函数化的终点 ​

源函数为 f = compose(mul(3),add(2))。写出 Compose(Mul(3),Add(2)) 后，手算 twice(f,1)：第一次 1→3→9，第二次 9→11→33。目标 apply 必须按相同顺序访问子函数。

迁移时交换 Compose 的两个字段，结果应为 17。再让外部输入决定建立多少个 Compose 节点，解释为什么标签种类仍只有三种，运行时对象数却能随输入增长。最后指出 Add(c) 应保存创建时的 c，而不是在调用处重新按名字查找。

验收证明只需覆盖这个有限树函数族：叶子的 apply 与源函数相等，Compose 先对 g 用归纳假设，再对 f 用归纳假设。若声称适用于任意高阶语言，还须补变量身份、环境与一般求值关系；本终点不要求这项推广。

trampoline 的终点 ​

对 S(n)=n+S(n-1)，把尚未做的加法保存为 Plus(n,K)，用 Enter/Resume/Halt 三种任务复算 n=3。完整轨迹为

Enter(3,End) → Enter(2,Plus(3,End))
→ Enter(1,Plus(2,Plus(3,End)))
→ Enter(0,Plus(1,Plus(2,Plus(3,End))))
→ Resume(0,Plus(1,Plus(2,Plus(3,End))))
→ Resume(1,Plus(2,Plus(3,End)))
→ Resume(3,Plus(3,End)) → Resume(6,End) → Halt(6)

有 8 次任务转移、峰值 3 个堆续延帧。宿主执行每条转移后返回同一个 while，所以用户函数调用深度有界；续延帧仍占随 n 增长的空间。高阶 Done/More 版创建初任务后有 2n+1 次 thunk 调用，一阶任务循环计 2n+2 次转移，解释两者的计数起点。

结构迁移是删除恢复阶段的 More，只保留下降阶段延迟。判断在哪里会重新连续调用 n 个宿主续延函数。测试不必依赖某个特定的递归上限数字：要说明控制深度为何随 n 增长。再将 Plus 换成乘法帧，重新写出 Resume(v,K) 代表的答案，而不是继续引用求和不变量。

三、保存的控制究竟回到哪里 ​

完整续延与组合式返回 ​

逐项列出捕获时保存的帧与调用时正在等待的帧，检查以下结果：

调用保存的完整续延不是一般函数返回：调用处的后续工作不会接回。调用保存的分界片段则保留调用处，并在恢复片段外建立新的 Mark；片段完成后经过这个 Mark 返回。

两种有区分力的结构迁移 ​

第一种是嵌套 call/cc：

1 + callcc(lambda exit.
      10 + callcc(lambda inner. exit(5)))

exit 保存 1+[]，inner 保存 1+(10+[])。调用 exit(5) 得 6；只把最内层调用改为 inner(5) 得 16。请画两份保存帧链，并解释为何内层捕获保存了更多尚未完成的工作。两个控制值只是都接收整数，并不表示它们指向同一终点。

第二种是保存片段内部再次执行 shift：

reset((shift k. (100 + k(1))) + (shift j. 10))

第一次保存 [] + (shift j.10)。调用 k(1) 时重装 reset，第二次 shift 只捕获片段内的 1+[]，忽略它后返回 10，再由调用处加 100 得 110。若只删掉 Part 调用时新建 Mark 的那一行，第二次 shift 会把 100+[] 也收到片段里，得到 10。

下载执行器中该行是 new=(('mark',),k)。在一份测试副本里将它改为 new=k，运行上述表达式即可区分两套语义；恢复后再运行其它输入。仅测试简单的 106 例不足以发现这类错误。

尚未处理的边界 ​

shift k.1 外面没有 reset 时，本文执行器应报告未处理操作。不要用默认的顶层 reset 偷渡一个结果。保存的片段和完整续延在这里都是不可变、可多次调用的；加入一次性恢复、可变状态、异常清理或多个提示符时，须另定规则。这些扩展不由本终点的整数输出保证。

下载与完成标准 ​

下载 标准库执行器 和 本组确定结果。使用 Python 3 运行：

python foundations-binding-control-checker.py
python -O foundations-binding-control-checker.py

两个命令都应给出相同 JSON。检查用显式异常实现，不依赖 assert。主程序还执行 n=10,000 的高阶 trampoline，核对结果 50,005,000、20,001 次 thunk 调用；控制部分输出捕获、丢弃和恢复的帧标签。这些事件标签是额外日志：完整续延会枚举保存/调用处帧，分界续延恢复还会枚举调用处帧；成本与被枚举的帧数成正比。调用 evaluate(...,record_events=False) 可关闭日志。核心帧指针切换或片段复制的复杂度不包含这项记录，捕获时扩展环境所需的字典复制也单独计费。执行器接收文中构造的良形元组语法，没有文本解析器；步骤上限报错表示本次没有算完，不是发散证明。

完成时应能交出三份东西：绑定替换及逆律反例；函数标签的结构归纳与任务机不变量；两类续延的帧图及恢复边界反例。输出一致是复算结果，论证中的作用域、有限函数族、纯语言和不可变帧条件同样属于答案。