“有状态语言把判断扩展为 $\langle e,\sigma\rangle\Downarrow\langle v,\sigma'\rangle$。大步语义通常按推导树归纳定义,因此一棵有限推导…”
形式陈述 ​
按需调用(call-by-need)不在绑定建立时求值右侧表达式,而是让环境把变量映到堆地址
let x = e_1 in e_2 时,语义分配新地址
这里的“更新”是运行语义的一部分,不是把声明式表达式改写成一个全局函数缓存。共享单位是一次绑定对应的堆单元;同一函数以不同参数建立的 thunk,或者两个文本相同却分别建立的绑定,通常没有共同缓存项。
在纯 λ 演算的适当观察下,按需调用与传名调用具有相同的终止结果:若传名求值得到一个答案,按需求值通过共享可得到相应答案,反向亦然。这个结论不表示两者逐步相同,也不覆盖堆占用、求值次数或带效果程序的可观察顺序。
直觉 ​
thunk 像一张可兑现一次的提货单。第一次读取变量的人负责完成计算,并把提货单替换成结果;后来的人读取同一地址,只看到已经算好的值。传名调用也会推迟实参,但每次使用都可能重新展开原表达式,因此它保存的是“配方”,按需调用保存的是“有身份、可更新的配方”。
非严格性来自“没有需求就不兑现”,共享来自“兑现后覆盖原单元”。两件事缺一不可:只有推迟而没有更新是传名行为;只有缓存一个已经主动计算的值,也没有解释未使用参数为何能避开发散。
例子与边界 ​
对 let x = expensive() in x + x,建立绑定时只分配一个 thunk。求左侧 x 时运行 expensive() 并把结果写回;求右侧 x 时读取同一个值。因此昂贵计算至多执行一次,而传名调用可能执行两次。若函数体根本不读取 x,这次计算一次也不会发生。
无限列表展示的是另一面:ones = 1 : ones 只要消费者请求有限个表头,就只展开有限段结构。可是惰性不等于恒定空间。若程序在逐步处理输入时仍保留对长链表头或未求值累加表达式的引用,垃圾回收器无法释放整条 thunk 链,形成 space leak;共享减少重复时间,不保证减少驻留内存。
效果构成观察边界。若 expensive() 改为打印一行文字,传名可能打印两次,按需只在第一次用到 x 时打印一次,传值则在进入函数体前打印一次。因而纯演算中的观察等价不能直接移植到 I/O、异常或可变状态语言。black hole 也不是普遍的终止判定器:它只能识别求值过程中立即重新进入同一未完成 thunk 的循环,不能识别所有发散计算。
推论与应用 ​
按需调用是许多惰性函数语言实现非严格语义的核心。堆更新把表达式图而非表达式树作为运行对象,因此常称 graph reduction;编译器还会用严格性分析识别必然需要的表达式,安全地提前求值并减少 thunk 分配。
它与传值调用的差异不只在“早或晚”,还包括堆对象的生命周期、异常触发时刻以及共享身份。按需语义也不自动引入并行:由哪个线程强制 thunk、其他线程是否等待,需要额外的调度与同步规则。实际系统还要用垃圾回收、更新策略和循环检测共同维护这套语义;把“lazy evaluation”泛指延迟容器或异步任务时,不能据此断定语言采用了 call-by-need。
参考资料
- John Launchbury, “A Natural Semantics for Lazy Evaluation,” POPL, 1993,heap-based natural semantics and sharing。
- Zena M. Ariola, Matthias Felleisen, John Maraist, Martin Odersky, and Philip Wadler, “A Call-by-Need Lambda Calculus,” POPL, 1995。
- Simon Peyton Jones, The Implementation of Functional Programming Languages, Prentice Hall, 1987,graph reduction and lazy implementation。