Journal of Functional Programming



The call-by-need lambda calculus


JOHN MARAIST a1, MARTIN ODERSKY a1 and PHILIP WADLER a2
a1 School of Computer and Information Science, University of South Australia, Warrendi Road, The Levels, Adelaide, SA 5095, Australia; e-mail: maraist@cis.unisa.edu.au odersky@cis.unisa.edu.au
a2 Bell Laboratories, Lucent Technologies, 700 Mountain Ave., Room 2T-304, Murray Hill, NJ 07974-0636, USA; e-mail: wadler@research.bell-labs.com

Abstract

We present a calculus that captures the operational semantics of call-by-need. The call-by-need lambda calculus is confluent, has a notion of standard reduction, and entails the same observational equivalence relation as the call-by-name calculus. The system can be formulated with or without explicit let bindings, admits useful notions of marking and developments, and has a straightforward operational interpretation.