No subject

Stephen Chang, Eli Barzilay, John Clements, Matthias Felleisen

Debugging lazy functional programs poses serious challenges. Due to the
 complicated nature of lazy evaluation, some debugging tools abandon laziness
 altogether. Other debuggers preserve laziness but present it in a way that may
 confuse programmers because the focus of evaluation jumps around in a
 seemingly random manner.

In this paper, we introduce the algebraic program stepper as a new debugging
 tool for lazy programs. We conjecture that our tool is suitable for clarifying
 the confusing nature of laziness. Preliminary classroom experiences have
 confirmed a prototype implementation of the stepper as a useful tool for
 novice programmers and programmers new to lazy programming.

Mathematically speaking, our stepper renders lazy computations as the standard
 rewriting sequences of a program rewriting system. Our lazy semantics
 introduces lazy evaluation as a form of parallel program rewriting. The
 semantics resembles graph reduction but remains intuitive for programmers
 because it emphasizes the source syntax. As a syntactic semantics, our
 rewriting system represents a compromise between Launchbury's store-based
 semantics and a simple, axiomatic description of lazy computation as
 sharing-via-parameters.  We prove an equivalence between our system and both
 of these semantics.

The stepper's implementation leverages Racket's continuation marks for stack
 trace generation. We can therefore exploit existing models of continuation
 marks and a correctness proof of Racket's eager algebraic stepper to prove the
 correctness of our lazy stepper.