Lazy Evaluation and Delimited Control

摘要

The call-by-need lambda calculus provides an equational framework forreasoning syntactically about lazy evaluation. This paper examines itsoperational characteristics. By a series of reasoning steps, we systematically unpack the standard-orderreduction relation of the calculus and discover a novel abstract machinedefinition which, like the calculus, goes "under lambdas." We prove thatmachine evaluation is equivalent to standard-order evaluation. Unlike traditional abstract machines, delimited control plays a significantrole in the machine's behavior. In particular, the machine replaces themanipulation of a heap using store-based effects with disciplined management ofthe evaluation stack using control-based effects. In short, state is replacedwith control. To further articulate this observation, we present a simulation ofcall-by-need in a call-by-value language using delimited control operations.