续延传递风格变换 | Codeboy's Blog

形式陈述

固定一个以λ 演算为核心的左到右传值调用源语言，以及答案类型 $R$ 。对源项 $e$ ，写 $\mathcal C\llbracket e\rrbracket k$ 表示“求值 $e$ 后把结果交给续延 $k$ ”。一个标准语法导向变换为

\begin{aligned} \mathcal C\llbracket x\rrbracket k &=k\,x,\\ \mathcal C\llbracket \lambda x.e\rrbracket k &=k\,(\lambda x.\lambda k'. \mathcal C\llbracket e\rrbracket k'),\\ \mathcal C\llbracket e_1\,e_2\rrbracket k &=\mathcal C\llbracket e_1\rrbracket (\lambda f. \mathcal C\llbracket e_2\rrbracket (\lambda v.f\,v\,k)). \end{aligned}

$k',f,v$ 必须对当前源项和目标上下文新鲜；否则翻译会捕获自由变量，破坏无捕获替换所保持的绑定。应用条款先翻译函数位置，再翻译参数位置，因而把选定的左到右顺序编码进目标项。换成传名或右到左源语义，条款也必须改变。

类型翻译可取基础类型 $o^*=o$ ，并令

(A\to B)^*=A^*\to(B^*\to R)\to R.

若源项有 $\Gamma\vdash e:A$ ，完整 CPS 计算的目标类型为 $(A^*\to R)\to R$ ；翻译后的函数值则接收 $A^*$ 参数和 $B^*\to R$ 续延。答案类型固定、可多态或随控制算子变化，是不同 CPS 系统的设计选择。

对闭合、纯、确定的源语言，一种语义保持陈述是：若 $e\Downarrow_v v$ ，则对类型相容的目标续延值 $k$ ， $\mathcal C\llbracket e\rrbracket k\to_v^* k\,v^*$ 。右边仍是待执行的续延应用，不是大步判断的最终值；若再有 $k\,v^*\Downarrow_v w$ ，才可推出整个翻译结果也求值到 $w$ 。源表达式终止不保证任意给定续延也终止。反向充分性或发散保持还需要明确源、目标观察及翻译后的值关系。源语言一步通常对应目标语言若干 β 步，不能宣称两边逐步相同。

直觉

直接风格函数“返回”结果，CPS 函数则收到一份结果去向，并在完成时调用它。原本藏在宿主调用栈中的“接下来做什么”变成普通函数参数。每个中间结果都立刻交给下一段控制，因此翻译后的核心项可整理成尾调用形式。

左侧直接风格经 square、加一后返回 10，右侧把结果去向写成 k₁ 参数并沿 k₁(9)、k(10) 的尾调用链传递 — CPS 将返回显式化为续延调用

CPS 是系统变换，不只是把某个回调手写出来。语法的每一种构造都必须有条款，条款共同保存源语言的求值顺序、作用域与控制效果。翻译后出现的 λf、λv 以及“立即构造再立即调用”的小函数，是变换制造的行政结构，不代表源程序新增业务计算。

例子与边界

令 $\mathsf{square}^*=\lambda x.\lambda k'.k'(x\times x)$ 。对源表达式 square 3 + 1，把加法也按左到右翻译，有

\begin{aligned} \mathcal C\llbracket \mathsf{square}\;3+1\rrbracket k &=\mathcal C\llbracket \mathsf{square}\;3\rrbracket (\lambda u. \mathcal C\llbracket 1\rrbracket(\lambda w.k(u+w)))\\ &\longrightarrow^* \mathsf{square}^*\;3\;(\lambda u.k(u+1))\\ &\longrightarrow^* k(10). \end{aligned}

中间的 λw.k(u+w) 接到常量 $1$ 后立即约简为 k(u+1)；消除这类 administrative redex 可缩短目标程序，但必须保持绑定和求值顺序。

异常可翻译成同时接收成功续延与失败续延的双续延程序，抛出时调用失败续延。这只是特定源语言的一种 CPS 实例。带状态、受限控制、调用名或不同答案类型的语言会产生不同翻译；不存在一套脱离源/目标语义仍“完全保序”的唯一公式。

推论与应用

CPS 使异常、非局部跳转和一等控制成为显式函数调用，也常用作编译器中间表示。对有限种续延函数做 defunctionalization，可把它们变成抽象机器的帧；这解释了显式控制栈如何由高阶求值器导出。

去函数化从有限函数抽象位置产生构造子和apply分派，普通Add/Mul/Compose函数族也适用。trampoline则把用户函数和续延的尾调用都延迟成返回任务，由while逐个执行；n=3求和的一阶任务机走8步，宿主调用深度有界而堆续延仍有3帧。

正确的编译器证明还需区分类型保持、终止结果保持、发散反射与上下文等价等目标。单看生成项“能运行”不足以证明变换正确；行政归约和优化也必须在已声明的源—目标观察关系下验证。

行政正规形（ANF）也显式安排左到右求值，但目标函数仍普通返回，中间结果由 let 命名，并未把续延作为目标程序参数。其编译算法用一个高阶函数组织输出，不构成输出已经是 CPS 的证明；两种变换的相邻接口应按各自目标文法核对。

参考资料

Gordon D. Plotkin, “Call-by-Name, Call-by-Value and the λ-Calculus,” Theoretical Computer Science 1, 1975。
Olivier Danvy and Andrzej Filinski, “Representing Control: A Study of the CPS Transformation,” Mathematical Structures in Computer Science 2(4), 1992。
Andrew W. Appel, Compiling with Continuations, Cambridge University Press, 1992。

形式陈述 ​

反向链接

形式陈述