续延传递风格变换

形式陈述 ​

固定一个左到右传值调用公理库传值调用Call by value · CBV仅当实参先求值为值后才进行函数体替换的求值策略。源语言和答案类型 $R$。对源项 $e$，写 $\mathcal{C}[[e]]k$ 表示“求值 $e$ 后把结果交给续延公理库续延Continuation表示计算余下部分、接收当前结果并产生最终结果的对象。 $k$”。一个标准语法导向变换为

$$\begin{array}{rl}\mathcal{C}[[x]]k& =kx,\\ \mathcal{C}[[\lambda x.e]]k& =k(\lambda x.\lambda k^{\prime }.\mathcal{C}[[e]]k^{\prime }),\\ \mathcal{C}[[e_1{e}_2]]k& =\mathcal{C}[[e_1]](\lambda f.\mathcal{C}[[e_2]](\lambda v.fvk)).\end{array}$$

$k^{\prime },f,v$ 必须对当前源项和目标上下文新鲜；否则翻译会捕获自由变量，破坏无捕获替换公理库无捕获替换Capture-avoiding substitution把项代入自由变量时通过重命名避免自由变量被意外绑定。所保持的绑定。应用条款先翻译函数位置，再翻译参数位置，因而把选定的左到右顺序编码进目标项。换成传名或右到左源语义，条款也必须改变。

类型翻译可取基础类型 $o^{\ast }=o$，并令

$$(A\to B{)}^{\ast }=A^{\ast }\to (B^{\ast }\to R)\to R.$$

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

对闭合、纯、确定的源语言，一种语义保持陈述是：若 $e{\Downarrow }_{v}v$，则对合适目标续延 $k$，$\mathcal{C}[[e]]k{\Downarrow }_{v}k{v}^{\ast }$。反向充分性或发散保持还需要明确源、目标观察及翻译后的值关系。源语言一步通常对应目标语言若干 β 步，不能宣称两边逐步相同。

直觉 ​

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

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

例子与边界 ​

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

$$\begin{array}{rl}\mathcal{C}[[\mathsf{square}3+1]]k& =\mathcal{C}[[\mathsf{square}3]](\lambda u.\mathcal{C}[[1]](\lambda w.k(u+w)))\\ & {⟶}^{\ast }{\mathsf{square}}^{\ast }3(\lambda u.k(u+1))\\ & {⟶}^{\ast }k(10).\end{array}$$

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

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

推论与应用 ​

CPS 使异常、非局部跳转和一等控制成为显式函数调用，也常用作编译器中间表示。对有限种续延函数做 defunctionalization，可把它们变成抽象机器公理库抽象机器Abstract machine · Operational abstract machine把程序执行写成显式配置与局部转移规则，并通过解码或模拟关系连接源语言语义的操作模型。的帧；这解释了显式控制栈如何由高阶求值器导出。

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

参考资料

• 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。