传名调用 | Codeboy's Blog

形式陈述

弱传名语义究竟在哪一步停下

在纯 λ 演算中，用 $t,u$ 表示项，传名应用的基本规则是

(\lambda x.t)\,u\longrightarrow t[x:=u].

右边是避免变量捕获的替换，不要求 $u$ 已经是值。若采用弱传名小步语义，可用求值上下文精确规定下一步的位置：

E::=[\ ]\mid E\,t, \qquad E[(\lambda x.t)u]\longrightarrow E[t[x:=u]].

上下文只沿应用的函数一侧向下寻找，不先进入实参，也不进入 λ 抽象体。于是，对能够终止的闭项，得到一个 λ 抽象就可以停下；这个抽象的函数体内部仍可能有可约表达式。[1]

这里需要区分弱传名调用与完整正规序归约。正规序也优先选择最左、最外的 β-红式，但为了求完整 β-正规形，还会继续进入 λ 抽象体。例如

\lambda z.((\lambda x.x)y)

在弱传名求值下已经停住；完整正规序会继续化成 $\lambda z.y$ 。标准化定理保证“若 β-正规形存在，正规序能够找到它”，并不意味着弱传名求值会把函数体里的所有红式消掉。Church–Rosser 定理则讨论不同归约路径的可汇合性，也不是指定某一种求值顺序的规则。[3]

直觉

参数是一份计算，而不是已经算好的值

假设函数只返回第一个参数，第二个参数却是一段永远运行下去的程序。必须先把两个参数都算完，才能调用函数吗？传值调用通常这样做；传名调用（call-by-name，CBN）则把尚未求值的实参带进函数体，等函数真正需要它时再计算。没有被使用的参数可以始终不求值。

“以后再算”与“只算一次”是两件事。传名调用保留前一种行为；同一参数使用两次，实参就可能计算两次。按需调用进一步共享第一次计算的结果，才获得通常所说的记忆化惰性求值。

例子与边界

三个表达式看清求值差异

令

\Omega=(\lambda x.xx)(\lambda x.xx).

它每归约一步又回到自己。传名调用却能直接得到

(\lambda x.\lambda z.z)\Omega\longrightarrow\lambda z.z,

因为参数 $x$ 没有出现在函数体中。传值调用会先计算 $\Omega$ ，因而无法进入函数体。这里的差别不是速度快慢，而是一次计算能否结束。

再把语言扩展为含整数和严格加法的表达式。对

(\lambda x.x+x)(1+2),

传名替换得到 $(1+2)+(1+2)$ ，两个副本分别算出 $3$ ；传值调用先求出 $3$ 再代入；按需调用则在第一次需要 $x$ 时算出 $3$ ，第二次读取共享结果。三者结果都是 $6$ ，但计算发生的时间和次数不同。

有副作用时，次数会改变结果。设计数器初值为 $0$ ，next() 返回旧值后加一，并规定加法先求左操作数。把上式实参换成 next()，可得到：

策略	实参执行过程	加法结果	最终计数器
传值	调用前执行一次，得到 $0$	$0+0=0$	1
传名	两次使用分别得到 $0$ 、 $1$	$0+1=1$	2
按需	第一次使用得到 $0$ ，随后共享	$0+0=0$	1

因此，纯语言中“结果相同但工作量不同”的比较，不能原封不动地搬到含状态的语言中。Scala 的 by-name 参数就是一种可以观察到重复求值的语言机制；它本身不承诺缓存结果。[2]

替换必须保住自由变量的含义

“把实参放进函数体”不是盲目的文本替换。考虑

(\lambda x.\lambda y.x)\,y.

实参中的 $y$ 原来是自由变量。若直接得到 $\lambda y.y$ ，这个 $y$ 就被内层绑定了，程序的含义已经改变。正确做法是先把内层绑定变量改成一个新名字，例如

(\lambda x.\lambda z.x)\,y\longrightarrow\lambda z.y.

这里发生的是 α-改名与避免捕获的替换。实际解释器不必反复复制整棵语法树：也可以保存“表达式及其定义时的环境”，在每次使用时重新解释。语义规定何时计算、如何处理绑定；表达式是否物理复制属于实现选择。[1]

推论与应用

上下文等价单元给出带类型版本：在 Bool 与箭头的语言中新增原始常量 $\Omega:\mathsf{Bool}$ 及自环规则。于是 $(\lambda x:\mathsf{Bool}.\mathsf{true})\Omega$ 返回 true，而 $\mathsf{if}\ \Omega\ \mathsf{then}\ \mathsf{true}\ \mathsf{else}\ \mathsf{true}$ 发散。本页前面的无类型自应用 $\Omega$ 无法在纯简单类型系统中定型；两种写法不能当成同一个带类型构造。

从传名到按需，改变的是共享方式

传名调用适合解释短路行为与自定义控制结构：一个参数可以表示尚未执行的计算，函数决定是否使用它。它也暴露一个明确的代价：重复使用可能重复做昂贵工作。

按需调用用可共享的 thunk 表示延迟计算，并在求值后更新其状态。这不是给传名规则换一个名称，而是增加了共享身份与存储更新。讨论纯程序的终止性时，可以把两者放在非严格求值的共同背景下；讨论副作用、内存占用或重复执行时，则必须保留这个区别。

参考资料

[1] Cornell CS 3110，Capture-Avoiding Substitution，传值与传名规则、自由变量和避免捕获的替换。

[2] Scala 官方文档，By-name Parameters，重复求值与按需使用的语言实例。

[3] Robert Harper，Practical Foundations for Programming Languages，第 2 版，2016。参见求值、函数与惰性计算相关章节；作者书籍页面。

形式陈述 ​

弱传名语义究竟在哪一步停下 ​

参数是一份计算，而不是已经算好的值 ​

三个表达式看清求值差异 ​

替换必须保住自由变量的含义 ​