Sunday, March 19, 2006

Why the CPS simulation of CBV works

Incidentally, it's exactly the common element of call-by-name and call-by-value I mentioned a moment ago that facilitates the CPS simulation of call-by-value in call-by-name. Both reduction rules require that the operator of a redex be a value. In either calculus, reduction relies on instantiating a bound variable within the body of a function; there's no obvious way you could know how to reduce if you don't actually know what the operator is. So both systems force evaluation of an operator in order to evaluate an application. The difference is whether you also force the operand.

The CPS transform just makes it so that all evaluation within an entire program occurs exclusively in operator positions. After the translation, all operands are values and therefore irreducible. This property is also preserved under reduction, so at every step, a CPS'ed program behaves the same in either calculus.

In other words, if every operand is always a value, there's no difference between the β-rule and the βv rule.

No comments: