Plotkin [Theor. Comp. Sci. 1975] showed that the lambda calculus is a. good model of the evaluation process for call-by-name functional programs. Reducing programs to constants or lambda. abstractions according to the leftmost-outermost strategy exactly mirrors execution on an abstract machine like Landin's SECD machine. The machine-based evaluator returns a constant or the token closure if and only if the standard reduction sequence starting at the same program will end in the same constant or in some lambda abstraction. However, the calculus does not capture the sharing of the evaluation of arguments that lazy implementations use to speed up the execution. More precisely, a lazy implementation evaluates procedure arguments only when needed and then only once. All other references to the formal procedure para.meter re-use the value of the first argument evaluation.

The mismatch between the operational semantics of the lambda calculus a.nd the actual behavior of the prototypical implementation is a major obstacle for compiler writers. Unlike implementors o( the leftmost-outermost strategy or of a call-by-value language, implementors of lazy systems cannot easily explain the behavior of their evaluator in terms of source level syntax. Hence, they often cannot explain why a certain syntactic transformation "works" and why another doesn't. In this paper we develop an equational characterization of the most popular lazy implementation technique-traditionally called "call-by-need"-a.nd prove it correct with respect to the original lambda. calculus. The theory is a. strictly smaller theory than Plotkin's call-by-name lambda calculus. Immediate applications of the theory concern the correctness proofs of a number of implementation strategies, e.g., the call-by-need continuation passing transformation and the realization of sharing via assignments.