现代魔法构成论:求值策略

Belleve Invis · 2014-03-28

Call by Value 和 Call by Name 的真正定义是什么呢?实际上是 Lambda 演算里的 betaβ 规约顺序。

考虑表达式 (lambda x . ~x^2)((lambda x . ~x + 1) ~ 2)(λx.x{2})((λx.x+1)2),按照 betaβ 规约的法则,有两种代换次序:

  1. (lambda x . ~x^2)((lambda x . ~x + 1) ~ 2) -> ((lambda x . ~x + 1) ~ 2)^2 -> (2 + 1)^2 -> 9(λx.x{2})((λx.x+1)2)((λx.x+1)2){2}(2+1){2}9
  2. (lambda x . ~x^2)((lambda x . ~x + 1) ~ 2) -> (lambda x . ~x^2)(2 + 1) -> (2 + 1)^2 -> 9(λx.x{2})((λx.x+1)2)(λx.x{2})(2+1)(2+1){2}9

这两种分别叫作「规范次序」和「应用次序」。在规范次序中,我们选择最左最外的可约调用(左项是 lambdaλ 抽象的调用)并规约之,而在规范次序中,则是最左最内的。这两者在常见的编程世界里的名字,就是传名调用与传值调用。

规范次序之所以称为「规范次序」,是因为使用它规约表达式时,要么消除掉所有的可约调用(即规范化),要么出现循环,而应用次序下则不然。考虑可规范化的表达式 (lambda y. ~ lambda x. ~ x)((lambda x. ~ x x )(lambda x. ~ x x ))(λy.λx.x)((λx.xx)(λx.xx)),由于 ((lambda x. ~ x x )(lambda x. ~ x x ))((λx.xx)(λx.xx)) 不可规范化(展开它会得到循环),因此这个表达式在应用次序下不收敛,但是在规范次序下,可以得到 (lambda y. ~ lambda x. ~ x)((lambda x. ~ x x )(lambda x. ~ x x )) -> lambda x. ~ x(λy.λx.x)((λx.xx)(λx.xx))λx.x

然而为什么程序语言普遍使用应用次序(传值调用)呢?因为应用次序有个好处:在每次规约时,调用的后件永远是已规范化的——换言之它永远是个值,这显然更对 CPU 的胃口。