Lazy Evaluation and Delimited Control

摘要

The call-by-need lambda calculus provides an equational frame-work for reasoning syntactically about lazy evaluation. This paperexamines its operational characteristics. By a series of reasoning steps, we systematically unpack thestandard-order reduction relation of the calculus and discover anovel abstract machine definition which, like the calculus, goes"under lambdas." We prove that machine evaluation is equivalentto standard-order evaluation. Unlike traditional abstract machines, delimited control plays asignificant role in the machine's behavior. In particular, the machinereplaces the manipulation of a heap using store-based effects withdisciplined management of the evaluation stack using control-basedeffects. In short, state is replaced with control. To further articulate this observation, we present a simulationof call-by-need in a call-by-value language using delimited controloperations.