Abstract:
We argue that Ariola and Felleisen's and Maraist, Odersky and Wadler's axiomatization of the call-by-need lambda calculus forms a suitable formal basis for tracing
evaluation in lazy functional languages. In particular, it allows a one-dimensional
textual representation of terms, rather than requiring a two-dimensional graphical
representation using arrows. We describe a program LetTrace, implemented in
Gofer and tracing lazy evaluation of a subset of Gofer.