Computer Science – Programming Languages
Scientific paper
2012-01-18
Computer Science
Programming Languages
ESOP 2012
Scientific paper
The existing call-by-need lambda calculi describe lazy evaluation via equational logics. A programmer can use these logics to safely ascertain whether one term is behaviorally equivalent to another or to determine the value of a lazy program. However, neither of the existing calculi models evaluation in a way that matches lazy implementations. Both calculi suffer from the same two problems. First, the calculi never discard function calls, even after they are completely resolved. Second, the calculi include re-association axioms even though these axioms are merely administrative steps with no counterpart in any implementation. In this paper, we present an alternative axiomatization of lazy evaluation using a single axiom. It eliminates both the function call retention problem and the extraneous re-association axioms. Our axiom uses a grammar of contexts to describe the exact notion of a needed computation. Like its predecessors, our new calculus satisfies consistency and standardization properties and is thus suitable for reasoning about behavioral equivalence. In addition, we establish a correspondence between our semantics and Launchbury's natural semantics.
Chang Stephen
Felleisen Matthias
No associations
LandOfFree
The Call-by-need Lambda Calculus, Revisited does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with The Call-by-need Lambda Calculus, Revisited, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and The Call-by-need Lambda Calculus, Revisited will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-253280