求基于λ演算归约序列的续体传递风格（CPS）非编程语言示例

嘿，我太懂你这种困惑了——网上搜CPS全是Python、JavaScript或者Haskell的例子，满是语法糖，反而把λ演算里最纯粹的续体思想给掩盖了。刚好你在看Wadler的《Monads...》，那咱们就用纯λ演算来拆解CPS，从最基础的例子到归约序列一步步来。

首先明确核心：普通λ演算表达式是直接返回结果，而CPS（续体传递风格）的表达式是把结果传给一个显式的“后续函数”（续体），让这个续体决定接下来要做什么。所有计算步骤的“下一步”都被显式作为参数传递，没有隐式的返回流程。

先看普通的恒等函数：

id = λx. x

它接受一个参数x，直接返回x。

对应的CPS版本是：

id_cps = λx. λk. k x

它接受两个参数：值x，以及续体k（一个函数）。它不直接返回x，而是把x传给k，让k处理x。

归约序列对比：普通 vs CPS #

比如计算id (id 5)（这里的5是邱奇整数，5 = λf.λx.f(f(f(f(f x))))）：

普通归约 #

id (id 5) → id 5 → 5

很直接，每一步直接返回结果。

CPS版本的归约 #

我们要计算同样的结果，但需要把最终的续体（也就是“拿到结果后做什么”）传进去——这里我们用恒等续体λv. v（拿到结果后直接返回它），所以CPS表达式是：

id_cps (id_cps 5 (λv. v)) (λv. v)

现在一步步归约：

1. 先处理内层的id_cps 5 (λv. v)：

   id_cps 5 (λv. v) → (λx.λk. k x) 5 (λv. v) → (λk. k 5) (λv. v) → (λv. v) 5 → 5
   

2. 现在外层表达式变成id_cps 5 (λv. v)，再归约：

   id_cps 5 (λv. v) → (λx.λk. k x) 5 (λv. v) → (λk. k 5) (λv. v) → (λv. v) 5 → 5
   

结果和普通归约一样，但每一步都显式传递了“接下来要做的事情”。

再看加法，普通的邱奇整数加法函数是：

add = λm.λn.λf.λx. m f (n f x)

它接受两个邱奇整数m和n，返回它们的和。

对应的CPS版本的加法函数（简化版）是：

add_cps = λm.λn.λk. k (add m n)

它接受m、n和续体k，把m+n的结果传给k。

带条件的CPS示例 #

再结合λ演算的条件表达式，普通的条件函数是：

if = λb.λt.λe. b t e
true = λt.λe. t
false = λt.λe. e

CPS版本的条件函数需要把续体传给分支：

if_cps = λb.λt.λe.λk. b (t k) (e k)

它的逻辑是：如果b是true，就执行t分支并把续体k传给t；如果是false，执行e分支并把k传给e。

比如我们要计算if true (add 1 2) (add 3 4)的CPS版本，最终续体用λv. v，表达式是：

if_cps true (add_cps 1 2) (add_cps 3 4) (λv. v)

归约序列：

1. 展开if_cps：

   (λb.λt.λe.λk. b (t k) (e k)) true (add_cps 1 2) (add_cps 3 4) (λv. v)
   

2. 应用true（true = λt.λe. t），得到：

   true (add_cps 1 2 (λv. v)) (add_cps 3 4 (λv. v))
   

3. true会返回第一个参数，所以变成：

   add_cps 1 2 (λv. v)
   

4. 展开add_cps并归约：

   (λm.λn.λk. k (add m n)) 1 2 (λv. v) → (λk. k (add 1 2)) (λv. v) → (λv. v) (add 1 2)
   

5. 归约add 1 2得到3，最终：

   (λv. v) 3 → 3
   

改变续体的效果 #

如果我们把最终续体改成“拿到结果后再加4”，也就是λv. add_cps v 4 (λv. v)，表达式变成：

if_cps true (add_cps 1 2) (add_cps 3 4) (λv. add_cps v 4 (λv. v))

归约到第三步还是add_cps 1 2 (λv. add_cps v 4 (λv. v))，继续归约：

(λk. k (add 1 2)) (λv. add_cps v 4 (λv. v)) → (λv. add_cps v 4 (λv. v)) 3 → add_cps 3 4 (λv. v) → 7

这就清晰展示了：续体就是“后续要执行的计算”，我们可以通过传递不同的续体来改变计算的后续流程。

你看的《Monads for Functional Programming》里，Wadler把CPS作为monad的经典实例——CPS monad的上下文就是“等待续体”，bind操作其实就是把两个CPS表达式的续体串起来，让前一个表达式的结果传递给后一个表达式的续体。本质上，monad是对CPS这种“显式传递上下文”模式的抽象。

内容的提问来源于stack exchange，提问作者user65526