Tracing the evaluation of lazy functional languages: A model and its implementation

We address the problem of producing a trace of the evaluation of a program written in a lazy functional language. To avoid ambiguities and possible misunderstandings it is essential that the trace structure is defined with respect to a formally described model of program evaluation. We provide such a formal semantics for lazy evaluation of a simple lazy language, based closely on the work of Launchbury. The trace corresponds to the sequence of expression reductions defined by the evaluation model. We also present a scheme to generate a concrete trace of the evaluation of programs written in the target language, based on its semantic rules. We employ a two-step transformational approach: first transform the program so that, on execution, it generates a call-by-name trace as result, then further transform this trace to a call-by-need trace